/
ex0718_present_27.p9.out
1512 lines (1424 loc) · 108 KB
/
ex0718_present_27.p9.out
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
============================== Prover9 ===============================
Prover9 (64) version 2009-11A, November 2009.
Process 8408 was started by cchui on stl-ws4.mie.utoronto.ca,
Fri Jul 19 01:58:39 2013
The command was "prover9 -t 600 -f test/p9/dolce_present.p9 test/p9/dolce_present2ideal_cem_wmg.p9 test/p9/dolce_time_mereology.p9 test/p9/dolce_taxonomy.p9 test/p9/options.txt test/p9/ex0718_present_27.p9".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file test/p9/dolce_present.p9
formulas(sos).
(all x (ED(x) | PD(x) | Q(x) -> (exists t PRE(x,t)))).
(all x all t all t1 (PRE(x,t) & P(t1,t) -> PRE(x,t1))).
(all x all t (PRE(x,t) -> T(t))).
(all x all t all t1 all t2 (PRE(x,t1) & PRE(x,t2) & SUM(t,t1,t2) -> PRE(x,t))).
end_of_list.
% Reading from file test/p9/dolce_present2ideal_cem_wmg.p9
formulas(sos).
(all x all y (in(x,y) <-> PRE(x,y) & T(y) & (ED(x) | PD(x) | Q(x)) | PRE(y,x) & T(x) & (ED(y) | PD(y) | Q(y)) | x = y & (ED(y) | PD(y) | Q(y) | T(y)))).
(all x (line(x) <-> ED(x) | PD(x) | Q(x))).
(all x (point(x) <-> T(x))).
(all x all y (part(x,y) <-> P(x,y) & T(x) & T(y))).
(all x (L_1(x) <-> ED(x))).
(all x (L_2(x) <-> PD(x))).
(all x (L_3(x) <-> Q(x))).
(all x (L_4(x) <-> PED(x))).
(all x (L_5(x) <-> NPED(x))).
(all x all y (ppart(x,y) <-> PP(x,y) & T(x) & T(y))).
(all x all y (overlaps(x,y) <-> O(x,y) & T(x) & T(y))).
(all x all y (underlaps(x,y) <-> U(x,y) & T(x) & T(y))).
(all x all y (disjoint(x,y) <-> DJ(x,y) & T(x) & T(y))).
(all x all y all z (sum(x,y,z) <-> SUM(z,x,y) & T(z) & T(x) & T(y))).
(all x all y all z (sum(x,y,z) <-> (all w (overlaps(w,z) <-> overlaps(w,x) | overlaps(w,y))))).
end_of_list.
% Reading from file test/p9/dolce_time_mereology.p9
formulas(sos).
(all x all y (P(x,y) -> T(y) & T(y))).
(all x all y (P(x,y) -> (T(x) <-> T(y)))).
(all x all y (T(x) -> P(x,x))).
(all x all y (T(x) & T(y) & P(x,y) & P(y,x) -> x = y)).
(all x all y all z (T(x) & T(y) & P(x,y) & P(y,z) -> P(x,z))).
(all x all y (T(x) & T(y) & -P(x,y) -> (exists z (T(z) & P(z,x) & -O(z,y))))).
(all x all y (T(x) & T(y) & -P(x,y) -> (exists z (P(z,x) & DJ(z,y) & T(z))))).
(all x all y (T(x) & T(y) -> (PP(x,y) <-> P(x,y) & -P(y,x)))).
(all x all y (T(x) & T(y) -> (O(x,y) <-> (exists z (P(z,x) & P(z,y) & T(z)))))).
(all x all y (T(x) & T(y) -> (DJ(x,y) <-> -O(x,y)))).
(all x all y (T(x) & T(y) -> (U(x,y) <-> (exists z (P(x,z) & P(y,z) & T(z)))))).
(all x (AtP(x) <-> T(x) & (all y (T(y) & P(y,x) -> y = x)))).
(all x all y (T(x) & T(y) & U(x,y) -> (exists z (T(z) & (all w (T(w) -> (O(w,z) <-> O(w,x) | O(w,y)))))))).
(all x all y (T(x) & T(y) & O(x,y) -> (exists z (T(z) & (all w (T(w) -> (PP(w,z) <-> PP(w,x) & PP(w,y)))))))).
(all x all y all z (T(x) & T(y) & T(z) -> (SUM(z,x,y) <-> (all w (T(w) -> (O(w,z) <-> O(w,x) | O(w,y))))))).
end_of_list.
% Reading from file test/p9/dolce_taxonomy.p9
formulas(sos).
(all x (ED(x) | PD(x) | Q(x) | AB(x) -> PT(x))).
(all x (PED(x) | NPED(x) | AS(x) -> ED(x))).
(all x (EV(x) | STV(x) -> PD(x))).
(all x (TQ(x) | PQ(x) | AQ(x) -> Q(x))).
(all x (R(x) -> AB(x))).
(all x (M(x) | F(x) | POB(x) -> PED(x))).
(all x (NPOB(x) -> NPED(x))).
(all x (ACH(x) | ACC(x) -> EV(x))).
(all x (ST(x) | PRO(x) -> STV(x))).
(all x (TL(x) -> TQ(x))).
(all x (SL(x) -> PQ(x))).
(all x (TR(x) | PR(x) | AR(x) -> R(x))).
(all x (APO(x) | NAPO(x) -> POB(x))).
(all x (MOB(x) | SOB(x) -> NPOB(x))).
(all x (T(x) -> TR(x))).
(all x (S(x) -> PR(x))).
(all x (ASO(x) | NASO(x) -> SOB(x))).
(all x (SAG(x) | SC(x) -> ASO(x))).
(all x (PT(x) <-> ED(x) | PD(x) | Q(x) | AB(x))).
(all x (ED(x) -> -PD(x) & -Q(x) & -AB(x))).
(all x (PD(x) -> -Q(x) & -AB(x))).
(all x (Q(x) -> -AB(x))).
(all x (ED(x) <-> PED(x) | NPED(x) | AS(x))).
(all x (PED(x) -> -NPED(x) & -AS(x))).
(all x (NPED(x) -> -AS(x))).
(all x (PD(x) <-> EV(x) | STV(x))).
(all x (EV(x) -> -STV(x))).
(all x (Q(x) <-> TQ(x) | PQ(x) | AQ(x))).
(all x (TQ(x) -> -PQ(x) & -AQ(x))).
(all x (PQ(x) -> -AQ(x))).
(all x (PED(x) <-> M(x) | F(x) | POB(x))).
(all x (M(x) -> -F(x) & -POB(x))).
(all x (F(x) -> -POB(x))).
(all x (EV(x) <-> ACH(x) | ACC(x))).
(all x (ACH(x) -> -ACC(x))).
(all x (STV(x) <-> ST(x) | PRO(x))).
(all x (ST(x) -> -PRO(x))).
(all x (R(x) <-> TR(x) | PR(x) | AR(x))).
(all x (TR(x) -> -PR(x) & -AR(x))).
(all x (PR(x) -> -AR(x))).
(all x (POB(x) <-> APO(x) | NAPO(x))).
(all x (APO(x) -> -NAPO(x))).
(all x (NPOB(x) <-> MOB(x) | SOB(x))).
(all x (MOB(x) -> -SOB(x))).
(all x (SOB(x) <-> ASO(x) | NASO(x))).
(all x (ASO(x) -> -NASO(x))).
(all x (ASO(x) <-> SAG(x) | SC(x))).
(all x (SAG(x) -> -SC(x))).
end_of_list.
% Reading from file test/p9/options.txt
clear(auto_denials).
clear(print_initial_clauses).
clear(print_kept).
clear(print_given).
% Reading from file test/p9/ex0718_present_27.p9
formulas(goals).
(all x all y all z (point(x) & point(y) & point(z) & part(x,y) & part(y,z) -> part(x,z))).
end_of_list.
============================== end of input ==========================
% From the command line: assign(max_seconds, 600).
============================== PROCESS NON-CLAUSAL FORMULAS ==========
% Formulas that are not ordinary clauses:
1 (all x (ED(x) | PD(x) | Q(x) -> (exists t PRE(x,t)))) # label(non_clause). [assumption].
2 (all x all t all t1 (PRE(x,t) & P(t1,t) -> PRE(x,t1))) # label(non_clause). [assumption].
3 (all x all t (PRE(x,t) -> T(t))) # label(non_clause). [assumption].
4 (all x all t all t1 all t2 (PRE(x,t1) & PRE(x,t2) & SUM(t,t1,t2) -> PRE(x,t))) # label(non_clause). [assumption].
5 (all x all y (in(x,y) <-> PRE(x,y) & T(y) & (ED(x) | PD(x) | Q(x)) | PRE(y,x) & T(x) & (ED(y) | PD(y) | Q(y)) | x = y & (ED(y) | PD(y) | Q(y) | T(y)))) # label(non_clause). [assumption].
6 (all x (line(x) <-> ED(x) | PD(x) | Q(x))) # label(non_clause). [assumption].
7 (all x (point(x) <-> T(x))) # label(non_clause). [assumption].
8 (all x all y (part(x,y) <-> P(x,y) & T(x) & T(y))) # label(non_clause). [assumption].
9 (all x (L_1(x) <-> ED(x))) # label(non_clause). [assumption].
10 (all x (L_2(x) <-> PD(x))) # label(non_clause). [assumption].
11 (all x (L_3(x) <-> Q(x))) # label(non_clause). [assumption].
12 (all x (L_4(x) <-> PED(x))) # label(non_clause). [assumption].
13 (all x (L_5(x) <-> NPED(x))) # label(non_clause). [assumption].
14 (all x all y (ppart(x,y) <-> PP(x,y) & T(x) & T(y))) # label(non_clause). [assumption].
15 (all x all y (overlaps(x,y) <-> O(x,y) & T(x) & T(y))) # label(non_clause). [assumption].
16 (all x all y (underlaps(x,y) <-> U(x,y) & T(x) & T(y))) # label(non_clause). [assumption].
17 (all x all y (disjoint(x,y) <-> DJ(x,y) & T(x) & T(y))) # label(non_clause). [assumption].
18 (all x all y all z (sum(x,y,z) <-> SUM(z,x,y) & T(z) & T(x) & T(y))) # label(non_clause). [assumption].
19 (all x all y all z (sum(x,y,z) <-> (all w (overlaps(w,z) <-> overlaps(w,x) | overlaps(w,y))))) # label(non_clause). [assumption].
20 (all x all y (P(x,y) -> T(y) & T(y))) # label(non_clause). [assumption].
21 (all x all y (P(x,y) -> (T(x) <-> T(y)))) # label(non_clause). [assumption].
22 (all x all y (T(x) -> P(x,x))) # label(non_clause). [assumption].
23 (all x all y (T(x) & T(y) & P(x,y) & P(y,x) -> x = y)) # label(non_clause). [assumption].
24 (all x all y all z (T(x) & T(y) & P(x,y) & P(y,z) -> P(x,z))) # label(non_clause). [assumption].
25 (all x all y (T(x) & T(y) & -P(x,y) -> (exists z (T(z) & P(z,x) & -O(z,y))))) # label(non_clause). [assumption].
26 (all x all y (T(x) & T(y) & -P(x,y) -> (exists z (P(z,x) & DJ(z,y) & T(z))))) # label(non_clause). [assumption].
27 (all x all y (T(x) & T(y) -> (PP(x,y) <-> P(x,y) & -P(y,x)))) # label(non_clause). [assumption].
28 (all x all y (T(x) & T(y) -> (O(x,y) <-> (exists z (P(z,x) & P(z,y) & T(z)))))) # label(non_clause). [assumption].
29 (all x all y (T(x) & T(y) -> (DJ(x,y) <-> -O(x,y)))) # label(non_clause). [assumption].
30 (all x all y (T(x) & T(y) -> (U(x,y) <-> (exists z (P(x,z) & P(y,z) & T(z)))))) # label(non_clause). [assumption].
31 (all x (AtP(x) <-> T(x) & (all y (T(y) & P(y,x) -> y = x)))) # label(non_clause). [assumption].
32 (all x all y (T(x) & T(y) & U(x,y) -> (exists z (T(z) & (all w (T(w) -> (O(w,z) <-> O(w,x) | O(w,y)))))))) # label(non_clause). [assumption].
33 (all x all y (T(x) & T(y) & O(x,y) -> (exists z (T(z) & (all w (T(w) -> (PP(w,z) <-> PP(w,x) & PP(w,y)))))))) # label(non_clause). [assumption].
34 (all x all y all z (T(x) & T(y) & T(z) -> (SUM(z,x,y) <-> (all w (T(w) -> (O(w,z) <-> O(w,x) | O(w,y))))))) # label(non_clause). [assumption].
35 (all x (ED(x) | PD(x) | Q(x) | AB(x) -> PT(x))) # label(non_clause). [assumption].
36 (all x (PED(x) | NPED(x) | AS(x) -> ED(x))) # label(non_clause). [assumption].
37 (all x (EV(x) | STV(x) -> PD(x))) # label(non_clause). [assumption].
38 (all x (TQ(x) | PQ(x) | AQ(x) -> Q(x))) # label(non_clause). [assumption].
39 (all x (R(x) -> AB(x))) # label(non_clause). [assumption].
40 (all x (M(x) | F(x) | POB(x) -> PED(x))) # label(non_clause). [assumption].
41 (all x (NPOB(x) -> NPED(x))) # label(non_clause). [assumption].
42 (all x (ACH(x) | ACC(x) -> EV(x))) # label(non_clause). [assumption].
43 (all x (ST(x) | PRO(x) -> STV(x))) # label(non_clause). [assumption].
44 (all x (TL(x) -> TQ(x))) # label(non_clause). [assumption].
45 (all x (SL(x) -> PQ(x))) # label(non_clause). [assumption].
46 (all x (TR(x) | PR(x) | AR(x) -> R(x))) # label(non_clause). [assumption].
47 (all x (APO(x) | NAPO(x) -> POB(x))) # label(non_clause). [assumption].
48 (all x (MOB(x) | SOB(x) -> NPOB(x))) # label(non_clause). [assumption].
49 (all x (T(x) -> TR(x))) # label(non_clause). [assumption].
50 (all x (S(x) -> PR(x))) # label(non_clause). [assumption].
51 (all x (ASO(x) | NASO(x) -> SOB(x))) # label(non_clause). [assumption].
52 (all x (SAG(x) | SC(x) -> ASO(x))) # label(non_clause). [assumption].
53 (all x (PT(x) <-> ED(x) | PD(x) | Q(x) | AB(x))) # label(non_clause). [assumption].
54 (all x (ED(x) -> -PD(x) & -Q(x) & -AB(x))) # label(non_clause). [assumption].
55 (all x (PD(x) -> -Q(x) & -AB(x))) # label(non_clause). [assumption].
56 (all x (Q(x) -> -AB(x))) # label(non_clause). [assumption].
57 (all x (ED(x) <-> PED(x) | NPED(x) | AS(x))) # label(non_clause). [assumption].
58 (all x (PED(x) -> -NPED(x) & -AS(x))) # label(non_clause). [assumption].
59 (all x (NPED(x) -> -AS(x))) # label(non_clause). [assumption].
60 (all x (PD(x) <-> EV(x) | STV(x))) # label(non_clause). [assumption].
61 (all x (EV(x) -> -STV(x))) # label(non_clause). [assumption].
62 (all x (Q(x) <-> TQ(x) | PQ(x) | AQ(x))) # label(non_clause). [assumption].
63 (all x (TQ(x) -> -PQ(x) & -AQ(x))) # label(non_clause). [assumption].
64 (all x (PQ(x) -> -AQ(x))) # label(non_clause). [assumption].
65 (all x (PED(x) <-> M(x) | F(x) | POB(x))) # label(non_clause). [assumption].
66 (all x (M(x) -> -F(x) & -POB(x))) # label(non_clause). [assumption].
67 (all x (F(x) -> -POB(x))) # label(non_clause). [assumption].
68 (all x (EV(x) <-> ACH(x) | ACC(x))) # label(non_clause). [assumption].
69 (all x (ACH(x) -> -ACC(x))) # label(non_clause). [assumption].
70 (all x (STV(x) <-> ST(x) | PRO(x))) # label(non_clause). [assumption].
71 (all x (ST(x) -> -PRO(x))) # label(non_clause). [assumption].
72 (all x (R(x) <-> TR(x) | PR(x) | AR(x))) # label(non_clause). [assumption].
73 (all x (TR(x) -> -PR(x) & -AR(x))) # label(non_clause). [assumption].
74 (all x (PR(x) -> -AR(x))) # label(non_clause). [assumption].
75 (all x (POB(x) <-> APO(x) | NAPO(x))) # label(non_clause). [assumption].
76 (all x (APO(x) -> -NAPO(x))) # label(non_clause). [assumption].
77 (all x (NPOB(x) <-> MOB(x) | SOB(x))) # label(non_clause). [assumption].
78 (all x (MOB(x) -> -SOB(x))) # label(non_clause). [assumption].
79 (all x (SOB(x) <-> ASO(x) | NASO(x))) # label(non_clause). [assumption].
80 (all x (ASO(x) -> -NASO(x))) # label(non_clause). [assumption].
81 (all x (ASO(x) <-> SAG(x) | SC(x))) # label(non_clause). [assumption].
82 (all x (SAG(x) -> -SC(x))) # label(non_clause). [assumption].
83 (all x all y all z (point(x) & point(y) & point(z) & part(x,y) & part(y,z) -> part(x,z))) # label(non_clause) # label(goal). [goal].
============================== end of process non-clausal formulas ===
============================== PROCESS INITIAL CLAUSES ===============
============================== PREDICATE ELIMINATION =================
Eliminating SUM/3
84 -sum(x,y,z) | SUM(z,x,y). [clausify(18)].
85 -PRE(x,y) | -PRE(x,z) | -SUM(u,y,z) | PRE(x,u). [clausify(4)].
Derived: -sum(x,y,z) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(84,b,85,c)].
86 sum(x,y,z) | -SUM(z,x,y) | -T(z) | -T(x) | -T(y). [clausify(18)].
87 -T(x) | -T(y) | -T(z) | -SUM(z,x,y) | -T(u) | -O(u,z) | O(u,x) | O(u,y). [clausify(34)].
Derived: -T(x) | -T(y) | -T(z) | -T(u) | -O(u,z) | O(u,x) | O(u,y) | -sum(x,y,z). [resolve(87,d,84,b)].
88 -T(x) | -T(y) | -T(z) | -SUM(z,x,y) | -T(u) | O(u,z) | -O(u,x). [clausify(34)].
Derived: -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,x) | -sum(x,y,z). [resolve(88,d,84,b)].
89 -T(x) | -T(y) | -T(z) | -SUM(z,x,y) | -T(u) | O(u,z) | -O(u,y). [clausify(34)].
Derived: -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,y) | -sum(x,y,z). [resolve(89,d,84,b)].
90 -T(x) | -T(y) | -T(z) | SUM(z,x,y) | T(f10(x,y,z)). [clausify(34)].
Derived: -T(x) | -T(y) | -T(z) | T(f10(x,y,z)) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(90,d,85,c)].
Derived: -T(x) | -T(y) | -T(z) | T(f10(x,y,z)) | sum(x,y,z) | -T(z) | -T(x) | -T(y). [resolve(90,d,86,b)].
Derived: -T(x) | -T(y) | -T(z) | T(f10(x,y,z)) | -T(x) | -T(y) | -T(z) | -T(u) | -O(u,z) | O(u,x) | O(u,y). [resolve(90,d,87,d)].
Derived: -T(x) | -T(y) | -T(z) | T(f10(x,y,z)) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,x). [resolve(90,d,88,d)].
Derived: -T(x) | -T(y) | -T(z) | T(f10(x,y,z)) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,y). [resolve(90,d,89,d)].
91 -T(x) | -T(y) | -T(z) | SUM(z,x,y) | O(f10(x,y,z),z) | O(f10(x,y,z),x) | O(f10(x,y,z),y). [clausify(34)].
Derived: -T(x) | -T(y) | -T(z) | O(f10(x,y,z),z) | O(f10(x,y,z),x) | O(f10(x,y,z),y) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(91,d,85,c)].
Derived: -T(x) | -T(y) | -T(z) | O(f10(x,y,z),z) | O(f10(x,y,z),x) | O(f10(x,y,z),y) | sum(x,y,z) | -T(z) | -T(x) | -T(y). [resolve(91,d,86,b)].
Derived: -T(x) | -T(y) | -T(z) | O(f10(x,y,z),z) | O(f10(x,y,z),x) | O(f10(x,y,z),y) | -T(x) | -T(y) | -T(z) | -T(u) | -O(u,z) | O(u,x) | O(u,y). [resolve(91,d,87,d)].
Derived: -T(x) | -T(y) | -T(z) | O(f10(x,y,z),z) | O(f10(x,y,z),x) | O(f10(x,y,z),y) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,x). [resolve(91,d,88,d)].
Derived: -T(x) | -T(y) | -T(z) | O(f10(x,y,z),z) | O(f10(x,y,z),x) | O(f10(x,y,z),y) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,y). [resolve(91,d,89,d)].
92 -T(x) | -T(y) | -T(z) | SUM(z,x,y) | -O(f10(x,y,z),z) | -O(f10(x,y,z),x). [clausify(34)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),x) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(92,d,85,c)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),x) | sum(x,y,z) | -T(z) | -T(x) | -T(y). [resolve(92,d,86,b)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),x) | -T(x) | -T(y) | -T(z) | -T(u) | -O(u,z) | O(u,x) | O(u,y). [resolve(92,d,87,d)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),x) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,x). [resolve(92,d,88,d)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),x) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,y). [resolve(92,d,89,d)].
93 -T(x) | -T(y) | -T(z) | SUM(z,x,y) | -O(f10(x,y,z),z) | -O(f10(x,y,z),y). [clausify(34)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),y) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(93,d,85,c)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),y) | sum(x,y,z) | -T(z) | -T(x) | -T(y). [resolve(93,d,86,b)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),y) | -T(x) | -T(y) | -T(z) | -T(u) | -O(u,z) | O(u,x) | O(u,y). [resolve(93,d,87,d)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),y) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,x). [resolve(93,d,88,d)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),y) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,y). [resolve(93,d,89,d)].
Eliminating in/2
94 in(x,y) | -PRE(x,y) | -T(y) | -ED(x). [clausify(5)].
95 -in(x,y) | PRE(x,y) | PRE(y,x) | y = x. [clausify(5)].
96 -in(x,y) | PRE(x,y) | T(x) | y = x. [clausify(5)].
97 -in(x,y) | PRE(x,y) | ED(y) | PD(y) | Q(y) | y = x. [clausify(5)].
98 -in(x,y) | T(y) | PRE(y,x) | y = x. [clausify(5)].
99 -in(x,y) | T(y) | T(x) | y = x. [clausify(5)].
100 -in(x,y) | T(y) | ED(y) | PD(y) | Q(y). [clausify(5)].
101 -in(x,y) | ED(x) | PD(x) | Q(x) | PRE(y,x) | y = x. [clausify(5)].
102 -in(x,y) | ED(x) | PD(x) | Q(x) | T(x) | y = x. [clausify(5)].
103 -in(x,y) | ED(x) | PD(x) | Q(x) | ED(y) | PD(y) | Q(y) | y = x. [clausify(5)].
104 in(x,y) | -PRE(x,y) | -T(y) | -PD(x). [clausify(5)].
105 in(x,y) | -PRE(x,y) | -T(y) | -Q(x). [clausify(5)].
106 in(x,y) | -PRE(y,x) | -T(x) | -ED(y). [clausify(5)].
107 in(x,y) | -PRE(y,x) | -T(x) | -PD(y). [clausify(5)].
108 in(x,y) | -PRE(y,x) | -T(x) | -Q(y). [clausify(5)].
109 in(x,y) | y != x | -ED(y). [clausify(5)].
110 in(x,y) | y != x | -PD(y). [clausify(5)].
111 in(x,y) | y != x | -Q(y). [clausify(5)].
112 in(x,y) | y != x | -T(y). [clausify(5)].
Eliminating ED/1
113 -line(x) | ED(x) | PD(x) | Q(x). [clausify(6)].
114 -ED(x) | PRE(x,f1(x)). [clausify(1)].
Derived: -line(x) | PD(x) | Q(x) | PRE(x,f1(x)). [resolve(113,b,114,a)].
115 line(x) | -ED(x). [clausify(6)].
116 -L_1(x) | ED(x). [clausify(9)].
Derived: -L_1(x) | PRE(x,f1(x)). [resolve(116,b,114,a)].
Derived: -L_1(x) | line(x). [resolve(116,b,115,b)].
117 L_1(x) | -ED(x). [clausify(9)].
Derived: L_1(x) | -line(x) | PD(x) | Q(x). [resolve(117,b,113,b)].
118 -ED(x) | PT(x). [clausify(35)].
Derived: PT(x) | -line(x) | PD(x) | Q(x). [resolve(118,a,113,b)].
Derived: PT(x) | -L_1(x). [resolve(118,a,116,b)].
119 -PED(x) | ED(x). [clausify(36)].
Derived: -PED(x) | PRE(x,f1(x)). [resolve(119,b,114,a)].
Derived: -PED(x) | line(x). [resolve(119,b,115,b)].
Derived: -PED(x) | L_1(x). [resolve(119,b,117,b)].
Derived: -PED(x) | PT(x). [resolve(119,b,118,a)].
120 -NPED(x) | ED(x). [clausify(36)].
Derived: -NPED(x) | PRE(x,f1(x)). [resolve(120,b,114,a)].
Derived: -NPED(x) | line(x). [resolve(120,b,115,b)].
Derived: -NPED(x) | L_1(x). [resolve(120,b,117,b)].
Derived: -NPED(x) | PT(x). [resolve(120,b,118,a)].
121 -AS(x) | ED(x). [clausify(36)].
Derived: -AS(x) | PRE(x,f1(x)). [resolve(121,b,114,a)].
Derived: -AS(x) | line(x). [resolve(121,b,115,b)].
Derived: -AS(x) | L_1(x). [resolve(121,b,117,b)].
Derived: -AS(x) | PT(x). [resolve(121,b,118,a)].
122 -PT(x) | ED(x) | PD(x) | Q(x) | AB(x). [clausify(53)].
Derived: -PT(x) | PD(x) | Q(x) | AB(x) | PRE(x,f1(x)). [resolve(122,b,114,a)].
Derived: -PT(x) | PD(x) | Q(x) | AB(x) | line(x). [resolve(122,b,115,b)].
Derived: -PT(x) | PD(x) | Q(x) | AB(x) | L_1(x). [resolve(122,b,117,b)].
123 PT(x) | -ED(x). [clausify(53)].
124 -ED(x) | -PD(x). [clausify(54)].
Derived: -PD(x) | -L_1(x). [resolve(124,a,116,b)].
Derived: -PD(x) | -PED(x). [resolve(124,a,119,b)].
Derived: -PD(x) | -NPED(x). [resolve(124,a,120,b)].
Derived: -PD(x) | -AS(x). [resolve(124,a,121,b)].
125 -ED(x) | -Q(x). [clausify(54)].
Derived: -Q(x) | -L_1(x). [resolve(125,a,116,b)].
Derived: -Q(x) | -PED(x). [resolve(125,a,119,b)].
Derived: -Q(x) | -NPED(x). [resolve(125,a,120,b)].
Derived: -Q(x) | -AS(x). [resolve(125,a,121,b)].
126 -ED(x) | -AB(x). [clausify(54)].
Derived: -AB(x) | -line(x) | PD(x) | Q(x). [resolve(126,a,113,b)].
Derived: -AB(x) | -L_1(x). [resolve(126,a,116,b)].
Derived: -AB(x) | -PED(x). [resolve(126,a,119,b)].
Derived: -AB(x) | -NPED(x). [resolve(126,a,120,b)].
Derived: -AB(x) | -AS(x). [resolve(126,a,121,b)].
127 -ED(x) | PED(x) | NPED(x) | AS(x). [clausify(57)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | PD(x) | Q(x). [resolve(127,a,113,b)].
Derived: PED(x) | NPED(x) | AS(x) | -L_1(x). [resolve(127,a,116,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | PD(x) | Q(x) | AB(x). [resolve(127,a,122,b)].
128 ED(x) | -PED(x). [clausify(57)].
129 ED(x) | -NPED(x). [clausify(57)].
130 ED(x) | -AS(x). [clausify(57)].
Eliminating PD/1
131 -L_2(x) | PD(x). [clausify(10)].
132 -PD(x) | PRE(x,f1(x)). [clausify(1)].
133 line(x) | -PD(x). [clausify(6)].
Derived: -L_2(x) | PRE(x,f1(x)). [resolve(131,b,132,a)].
Derived: -L_2(x) | line(x). [resolve(131,b,133,b)].
134 L_2(x) | -PD(x). [clausify(10)].
135 -PD(x) | PT(x). [clausify(35)].
Derived: PT(x) | -L_2(x). [resolve(135,a,131,b)].
136 -EV(x) | PD(x). [clausify(37)].
Derived: -EV(x) | PRE(x,f1(x)). [resolve(136,b,132,a)].
Derived: -EV(x) | line(x). [resolve(136,b,133,b)].
Derived: -EV(x) | L_2(x). [resolve(136,b,134,b)].
Derived: -EV(x) | PT(x). [resolve(136,b,135,a)].
137 -STV(x) | PD(x). [clausify(37)].
Derived: -STV(x) | PRE(x,f1(x)). [resolve(137,b,132,a)].
Derived: -STV(x) | line(x). [resolve(137,b,133,b)].
Derived: -STV(x) | L_2(x). [resolve(137,b,134,b)].
Derived: -STV(x) | PT(x). [resolve(137,b,135,a)].
138 PT(x) | -PD(x). [clausify(53)].
139 -PD(x) | -Q(x). [clausify(55)].
Derived: -Q(x) | -L_2(x). [resolve(139,a,131,b)].
Derived: -Q(x) | -EV(x). [resolve(139,a,136,b)].
Derived: -Q(x) | -STV(x). [resolve(139,a,137,b)].
140 -PD(x) | -AB(x). [clausify(55)].
Derived: -AB(x) | -L_2(x). [resolve(140,a,131,b)].
Derived: -AB(x) | -EV(x). [resolve(140,a,136,b)].
Derived: -AB(x) | -STV(x). [resolve(140,a,137,b)].
141 -PD(x) | EV(x) | STV(x). [clausify(60)].
Derived: EV(x) | STV(x) | -L_2(x). [resolve(141,a,131,b)].
142 PD(x) | -EV(x). [clausify(60)].
143 PD(x) | -STV(x). [clausify(60)].
144 -line(x) | PD(x) | Q(x) | PRE(x,f1(x)). [resolve(113,b,114,a)].
Derived: -line(x) | Q(x) | PRE(x,f1(x)) | PRE(x,f1(x)). [resolve(144,b,132,a)].
145 L_1(x) | -line(x) | PD(x) | Q(x). [resolve(117,b,113,b)].
Derived: L_1(x) | -line(x) | Q(x) | L_2(x). [resolve(145,c,134,b)].
Derived: L_1(x) | -line(x) | Q(x) | PT(x). [resolve(145,c,135,a)].
Derived: L_1(x) | -line(x) | Q(x) | -AB(x). [resolve(145,c,140,a)].
Derived: L_1(x) | -line(x) | Q(x) | EV(x) | STV(x). [resolve(145,c,141,a)].
146 PT(x) | -line(x) | PD(x) | Q(x). [resolve(118,a,113,b)].
Derived: PT(x) | -line(x) | Q(x) | L_2(x). [resolve(146,c,134,b)].
Derived: PT(x) | -line(x) | Q(x) | PT(x). [resolve(146,c,135,a)].
147 -PT(x) | PD(x) | Q(x) | AB(x) | PRE(x,f1(x)). [resolve(122,b,114,a)].
Derived: -PT(x) | Q(x) | AB(x) | PRE(x,f1(x)) | PRE(x,f1(x)). [resolve(147,b,132,a)].
148 -PT(x) | PD(x) | Q(x) | AB(x) | line(x). [resolve(122,b,115,b)].
Derived: -PT(x) | Q(x) | AB(x) | line(x) | line(x). [resolve(148,b,133,b)].
149 -PT(x) | PD(x) | Q(x) | AB(x) | L_1(x). [resolve(122,b,117,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | L_2(x). [resolve(149,b,134,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | EV(x) | STV(x). [resolve(149,b,141,a)].
150 -PD(x) | -L_1(x). [resolve(124,a,116,b)].
Derived: -L_1(x) | -L_2(x). [resolve(150,a,131,b)].
Derived: -L_1(x) | -EV(x). [resolve(150,a,136,b)].
Derived: -L_1(x) | -STV(x). [resolve(150,a,137,b)].
151 -PD(x) | -PED(x). [resolve(124,a,119,b)].
Derived: -PED(x) | -L_2(x). [resolve(151,a,131,b)].
Derived: -PED(x) | -EV(x). [resolve(151,a,136,b)].
Derived: -PED(x) | -STV(x). [resolve(151,a,137,b)].
Derived: -PED(x) | L_1(x) | -line(x) | Q(x). [resolve(151,a,145,c)].
Derived: -PED(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(151,a,149,b)].
152 -PD(x) | -NPED(x). [resolve(124,a,120,b)].
Derived: -NPED(x) | -L_2(x). [resolve(152,a,131,b)].
Derived: -NPED(x) | -EV(x). [resolve(152,a,136,b)].
Derived: -NPED(x) | -STV(x). [resolve(152,a,137,b)].
Derived: -NPED(x) | L_1(x) | -line(x) | Q(x). [resolve(152,a,145,c)].
Derived: -NPED(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(152,a,149,b)].
153 -PD(x) | -AS(x). [resolve(124,a,121,b)].
Derived: -AS(x) | -L_2(x). [resolve(153,a,131,b)].
Derived: -AS(x) | -EV(x). [resolve(153,a,136,b)].
Derived: -AS(x) | -STV(x). [resolve(153,a,137,b)].
Derived: -AS(x) | L_1(x) | -line(x) | Q(x). [resolve(153,a,145,c)].
Derived: -AS(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(153,a,149,b)].
154 -AB(x) | -line(x) | PD(x) | Q(x). [resolve(126,a,113,b)].
Derived: -AB(x) | -line(x) | Q(x) | L_2(x). [resolve(154,c,134,b)].
Derived: -AB(x) | -line(x) | Q(x) | -AB(x). [resolve(154,c,140,a)].
155 PED(x) | NPED(x) | AS(x) | -line(x) | PD(x) | Q(x). [resolve(127,a,113,b)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | Q(x) | L_2(x). [resolve(155,e,134,b)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | Q(x) | EV(x) | STV(x). [resolve(155,e,141,a)].
156 PED(x) | NPED(x) | AS(x) | -PT(x) | PD(x) | Q(x) | AB(x). [resolve(127,a,122,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | L_2(x). [resolve(156,e,134,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | EV(x) | STV(x). [resolve(156,e,141,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -L_1(x). [resolve(156,e,150,a)].
Eliminating Q/1
157 -L_3(x) | Q(x). [clausify(11)].
158 -Q(x) | PRE(x,f1(x)). [clausify(1)].
159 line(x) | -Q(x). [clausify(6)].
Derived: -L_3(x) | PRE(x,f1(x)). [resolve(157,b,158,a)].
Derived: -L_3(x) | line(x). [resolve(157,b,159,b)].
160 L_3(x) | -Q(x). [clausify(11)].
161 -Q(x) | PT(x). [clausify(35)].
Derived: PT(x) | -L_3(x). [resolve(161,a,157,b)].
162 -TQ(x) | Q(x). [clausify(38)].
Derived: -TQ(x) | PRE(x,f1(x)). [resolve(162,b,158,a)].
Derived: -TQ(x) | line(x). [resolve(162,b,159,b)].
Derived: -TQ(x) | L_3(x). [resolve(162,b,160,b)].
Derived: -TQ(x) | PT(x). [resolve(162,b,161,a)].
163 -PQ(x) | Q(x). [clausify(38)].
Derived: -PQ(x) | PRE(x,f1(x)). [resolve(163,b,158,a)].
Derived: -PQ(x) | line(x). [resolve(163,b,159,b)].
Derived: -PQ(x) | L_3(x). [resolve(163,b,160,b)].
Derived: -PQ(x) | PT(x). [resolve(163,b,161,a)].
164 -AQ(x) | Q(x). [clausify(38)].
Derived: -AQ(x) | PRE(x,f1(x)). [resolve(164,b,158,a)].
Derived: -AQ(x) | line(x). [resolve(164,b,159,b)].
Derived: -AQ(x) | L_3(x). [resolve(164,b,160,b)].
Derived: -AQ(x) | PT(x). [resolve(164,b,161,a)].
165 PT(x) | -Q(x). [clausify(53)].
166 -Q(x) | -AB(x). [clausify(56)].
Derived: -AB(x) | -L_3(x). [resolve(166,a,157,b)].
Derived: -AB(x) | -TQ(x). [resolve(166,a,162,b)].
Derived: -AB(x) | -PQ(x). [resolve(166,a,163,b)].
Derived: -AB(x) | -AQ(x). [resolve(166,a,164,b)].
167 -Q(x) | TQ(x) | PQ(x) | AQ(x). [clausify(62)].
Derived: TQ(x) | PQ(x) | AQ(x) | -L_3(x). [resolve(167,a,157,b)].
168 Q(x) | -TQ(x). [clausify(62)].
169 Q(x) | -PQ(x). [clausify(62)].
170 Q(x) | -AQ(x). [clausify(62)].
171 -Q(x) | -L_1(x). [resolve(125,a,116,b)].
Derived: -L_1(x) | -L_3(x). [resolve(171,a,157,b)].
Derived: -L_1(x) | -TQ(x). [resolve(171,a,162,b)].
Derived: -L_1(x) | -PQ(x). [resolve(171,a,163,b)].
Derived: -L_1(x) | -AQ(x). [resolve(171,a,164,b)].
172 -Q(x) | -PED(x). [resolve(125,a,119,b)].
Derived: -PED(x) | -L_3(x). [resolve(172,a,157,b)].
Derived: -PED(x) | -TQ(x). [resolve(172,a,162,b)].
Derived: -PED(x) | -PQ(x). [resolve(172,a,163,b)].
Derived: -PED(x) | -AQ(x). [resolve(172,a,164,b)].
173 -Q(x) | -NPED(x). [resolve(125,a,120,b)].
Derived: -NPED(x) | -L_3(x). [resolve(173,a,157,b)].
Derived: -NPED(x) | -TQ(x). [resolve(173,a,162,b)].
Derived: -NPED(x) | -PQ(x). [resolve(173,a,163,b)].
Derived: -NPED(x) | -AQ(x). [resolve(173,a,164,b)].
174 -Q(x) | -AS(x). [resolve(125,a,121,b)].
Derived: -AS(x) | -L_3(x). [resolve(174,a,157,b)].
Derived: -AS(x) | -TQ(x). [resolve(174,a,162,b)].
Derived: -AS(x) | -PQ(x). [resolve(174,a,163,b)].
Derived: -AS(x) | -AQ(x). [resolve(174,a,164,b)].
175 -Q(x) | -L_2(x). [resolve(139,a,131,b)].
Derived: -L_2(x) | -L_3(x). [resolve(175,a,157,b)].
Derived: -L_2(x) | -TQ(x). [resolve(175,a,162,b)].
Derived: -L_2(x) | -PQ(x). [resolve(175,a,163,b)].
Derived: -L_2(x) | -AQ(x). [resolve(175,a,164,b)].
176 -Q(x) | -EV(x). [resolve(139,a,136,b)].
Derived: -EV(x) | -L_3(x). [resolve(176,a,157,b)].
Derived: -EV(x) | -TQ(x). [resolve(176,a,162,b)].
Derived: -EV(x) | -PQ(x). [resolve(176,a,163,b)].
Derived: -EV(x) | -AQ(x). [resolve(176,a,164,b)].
177 -Q(x) | -STV(x). [resolve(139,a,137,b)].
Derived: -STV(x) | -L_3(x). [resolve(177,a,157,b)].
Derived: -STV(x) | -TQ(x). [resolve(177,a,162,b)].
Derived: -STV(x) | -PQ(x). [resolve(177,a,163,b)].
Derived: -STV(x) | -AQ(x). [resolve(177,a,164,b)].
178 -line(x) | Q(x) | PRE(x,f1(x)) | PRE(x,f1(x)). [resolve(144,b,132,a)].
Derived: -line(x) | PRE(x,f1(x)) | PRE(x,f1(x)) | PRE(x,f1(x)). [resolve(178,b,158,a)].
179 L_1(x) | -line(x) | Q(x) | L_2(x). [resolve(145,c,134,b)].
Derived: L_1(x) | -line(x) | L_2(x) | L_3(x). [resolve(179,c,160,b)].
Derived: L_1(x) | -line(x) | L_2(x) | PT(x). [resolve(179,c,161,a)].
Derived: L_1(x) | -line(x) | L_2(x) | -AB(x). [resolve(179,c,166,a)].
Derived: L_1(x) | -line(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x). [resolve(179,c,167,a)].
Derived: L_1(x) | -line(x) | L_2(x) | -PED(x). [resolve(179,c,172,a)].
Derived: L_1(x) | -line(x) | L_2(x) | -NPED(x). [resolve(179,c,173,a)].
Derived: L_1(x) | -line(x) | L_2(x) | -AS(x). [resolve(179,c,174,a)].
Derived: L_1(x) | -line(x) | L_2(x) | -EV(x). [resolve(179,c,176,a)].
Derived: L_1(x) | -line(x) | L_2(x) | -STV(x). [resolve(179,c,177,a)].
180 L_1(x) | -line(x) | Q(x) | PT(x). [resolve(145,c,135,a)].
Derived: L_1(x) | -line(x) | PT(x) | L_3(x). [resolve(180,c,160,b)].
Derived: L_1(x) | -line(x) | PT(x) | PT(x). [resolve(180,c,161,a)].
181 L_1(x) | -line(x) | Q(x) | -AB(x). [resolve(145,c,140,a)].
Derived: L_1(x) | -line(x) | -AB(x) | L_3(x). [resolve(181,c,160,b)].
Derived: L_1(x) | -line(x) | -AB(x) | -AB(x). [resolve(181,c,166,a)].
182 L_1(x) | -line(x) | Q(x) | EV(x) | STV(x). [resolve(145,c,141,a)].
Derived: L_1(x) | -line(x) | EV(x) | STV(x) | L_3(x). [resolve(182,c,160,b)].
Derived: L_1(x) | -line(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x). [resolve(182,c,167,a)].
Derived: L_1(x) | -line(x) | EV(x) | STV(x) | -PED(x). [resolve(182,c,172,a)].
Derived: L_1(x) | -line(x) | EV(x) | STV(x) | -NPED(x). [resolve(182,c,173,a)].
Derived: L_1(x) | -line(x) | EV(x) | STV(x) | -AS(x). [resolve(182,c,174,a)].
Derived: L_1(x) | -line(x) | EV(x) | STV(x) | -L_2(x). [resolve(182,c,175,a)].
183 PT(x) | -line(x) | Q(x) | L_2(x). [resolve(146,c,134,b)].
Derived: PT(x) | -line(x) | L_2(x) | L_3(x). [resolve(183,c,160,b)].
Derived: PT(x) | -line(x) | L_2(x) | PT(x). [resolve(183,c,161,a)].
184 PT(x) | -line(x) | Q(x) | PT(x). [resolve(146,c,135,a)].
Derived: PT(x) | -line(x) | PT(x) | L_3(x). [resolve(184,c,160,b)].
Derived: PT(x) | -line(x) | PT(x) | PT(x). [resolve(184,c,161,a)].
185 -PT(x) | Q(x) | AB(x) | PRE(x,f1(x)) | PRE(x,f1(x)). [resolve(147,b,132,a)].
Derived: -PT(x) | AB(x) | PRE(x,f1(x)) | PRE(x,f1(x)) | PRE(x,f1(x)). [resolve(185,b,158,a)].
186 -PT(x) | Q(x) | AB(x) | line(x) | line(x). [resolve(148,b,133,b)].
Derived: -PT(x) | AB(x) | line(x) | line(x) | line(x). [resolve(186,b,159,b)].
187 -PT(x) | Q(x) | AB(x) | L_1(x) | L_2(x). [resolve(149,b,134,b)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | L_3(x). [resolve(187,b,160,b)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x). [resolve(187,b,167,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | -PED(x). [resolve(187,b,172,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | -NPED(x). [resolve(187,b,173,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | -AS(x). [resolve(187,b,174,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | -EV(x). [resolve(187,b,176,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | -STV(x). [resolve(187,b,177,a)].
188 -PT(x) | Q(x) | AB(x) | L_1(x) | EV(x) | STV(x). [resolve(149,b,141,a)].
Derived: -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | L_3(x). [resolve(188,b,160,b)].
Derived: -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x). [resolve(188,b,167,a)].
Derived: -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -PED(x). [resolve(188,b,172,a)].
Derived: -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -NPED(x). [resolve(188,b,173,a)].
Derived: -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -AS(x). [resolve(188,b,174,a)].
Derived: -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -L_2(x). [resolve(188,b,175,a)].
189 -PED(x) | L_1(x) | -line(x) | Q(x). [resolve(151,a,145,c)].
Derived: -PED(x) | L_1(x) | -line(x) | L_3(x). [resolve(189,d,160,b)].
Derived: -PED(x) | L_1(x) | -line(x) | TQ(x) | PQ(x) | AQ(x). [resolve(189,d,167,a)].
Derived: -PED(x) | L_1(x) | -line(x) | -PED(x). [resolve(189,d,172,a)].
190 -PED(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(151,a,149,b)].
Derived: -PED(x) | -PT(x) | AB(x) | L_1(x) | L_3(x). [resolve(190,c,160,b)].
Derived: -PED(x) | -PT(x) | AB(x) | L_1(x) | TQ(x) | PQ(x) | AQ(x). [resolve(190,c,167,a)].
Derived: -PED(x) | -PT(x) | AB(x) | L_1(x) | -PED(x). [resolve(190,c,172,a)].
191 -NPED(x) | L_1(x) | -line(x) | Q(x). [resolve(152,a,145,c)].
Derived: -NPED(x) | L_1(x) | -line(x) | L_3(x). [resolve(191,d,160,b)].
Derived: -NPED(x) | L_1(x) | -line(x) | TQ(x) | PQ(x) | AQ(x). [resolve(191,d,167,a)].
Derived: -NPED(x) | L_1(x) | -line(x) | -NPED(x). [resolve(191,d,173,a)].
192 -NPED(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(152,a,149,b)].
Derived: -NPED(x) | -PT(x) | AB(x) | L_1(x) | L_3(x). [resolve(192,c,160,b)].
Derived: -NPED(x) | -PT(x) | AB(x) | L_1(x) | TQ(x) | PQ(x) | AQ(x). [resolve(192,c,167,a)].
Derived: -NPED(x) | -PT(x) | AB(x) | L_1(x) | -NPED(x). [resolve(192,c,173,a)].
193 -AS(x) | L_1(x) | -line(x) | Q(x). [resolve(153,a,145,c)].
Derived: -AS(x) | L_1(x) | -line(x) | L_3(x). [resolve(193,d,160,b)].
Derived: -AS(x) | L_1(x) | -line(x) | TQ(x) | PQ(x) | AQ(x). [resolve(193,d,167,a)].
Derived: -AS(x) | L_1(x) | -line(x) | -AS(x). [resolve(193,d,174,a)].
194 -AS(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(153,a,149,b)].
Derived: -AS(x) | -PT(x) | AB(x) | L_1(x) | L_3(x). [resolve(194,c,160,b)].
Derived: -AS(x) | -PT(x) | AB(x) | L_1(x) | TQ(x) | PQ(x) | AQ(x). [resolve(194,c,167,a)].
Derived: -AS(x) | -PT(x) | AB(x) | L_1(x) | -AS(x). [resolve(194,c,174,a)].
195 -AB(x) | -line(x) | Q(x) | L_2(x). [resolve(154,c,134,b)].
Derived: -AB(x) | -line(x) | L_2(x) | L_3(x). [resolve(195,c,160,b)].
Derived: -AB(x) | -line(x) | L_2(x) | -AB(x). [resolve(195,c,166,a)].
196 -AB(x) | -line(x) | Q(x) | -AB(x). [resolve(154,c,140,a)].
Derived: -AB(x) | -line(x) | -AB(x) | L_3(x). [resolve(196,c,160,b)].
Derived: -AB(x) | -line(x) | -AB(x) | -AB(x). [resolve(196,c,166,a)].
197 PED(x) | NPED(x) | AS(x) | -line(x) | Q(x) | L_2(x). [resolve(155,e,134,b)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | L_2(x) | L_3(x). [resolve(197,e,160,b)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x). [resolve(197,e,167,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | L_2(x) | -L_1(x). [resolve(197,e,171,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | L_2(x) | -EV(x). [resolve(197,e,176,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | L_2(x) | -STV(x). [resolve(197,e,177,a)].
198 PED(x) | NPED(x) | AS(x) | -line(x) | Q(x) | EV(x) | STV(x). [resolve(155,e,141,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | EV(x) | STV(x) | L_3(x). [resolve(198,e,160,b)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x). [resolve(198,e,167,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | EV(x) | STV(x) | -L_1(x). [resolve(198,e,171,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | EV(x) | STV(x) | -L_2(x). [resolve(198,e,175,a)].
199 PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | L_2(x). [resolve(156,e,134,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | L_3(x). [resolve(199,e,160,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x). [resolve(199,e,167,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | -L_1(x). [resolve(199,e,171,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | -EV(x). [resolve(199,e,176,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | -STV(x). [resolve(199,e,177,a)].
200 PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | EV(x) | STV(x). [resolve(156,e,141,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | EV(x) | STV(x) | L_3(x). [resolve(200,e,160,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x). [resolve(200,e,167,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | EV(x) | STV(x) | -L_1(x). [resolve(200,e,171,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | EV(x) | STV(x) | -L_2(x). [resolve(200,e,175,a)].
201 PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -L_1(x). [resolve(156,e,150,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -L_1(x) | L_3(x). [resolve(201,e,160,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -L_1(x) | TQ(x) | PQ(x) | AQ(x). [resolve(201,e,167,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -L_1(x) | -L_1(x). [resolve(201,e,171,a)].
Eliminating point/1
202 point(x) | -T(x). [clausify(7)].
203 -point(x) | T(x). [clausify(7)].
204 point(c1). [deny(83)].
Derived: T(c1). [resolve(204,a,203,a)].
205 point(c2). [deny(83)].
Derived: T(c2). [resolve(205,a,203,a)].
206 point(c3). [deny(83)].
Derived: T(c3). [resolve(206,a,203,a)].
Eliminating L_4/1
207 L_4(x) | -PED(x). [clausify(12)].
208 -L_4(x) | PED(x). [clausify(12)].
Eliminating L_5/1
209 L_5(x) | -NPED(x). [clausify(13)].
210 -L_5(x) | NPED(x). [clausify(13)].
Eliminating ppart/2
211 ppart(x,y) | -PP(x,y) | -T(x) | -T(y). [clausify(14)].
212 -ppart(x,y) | PP(x,y). [clausify(14)].
213 -ppart(x,y) | T(x). [clausify(14)].
214 -ppart(x,y) | T(y). [clausify(14)].
Eliminating underlaps/2
215 underlaps(x,y) | -U(x,y) | -T(x) | -T(y). [clausify(16)].
216 -underlaps(x,y) | U(x,y). [clausify(16)].
217 -underlaps(x,y) | T(x). [clausify(16)].
218 -underlaps(x,y) | T(y). [clausify(16)].
Eliminating disjoint/2
219 disjoint(x,y) | -DJ(x,y) | -T(x) | -T(y). [clausify(17)].
220 -disjoint(x,y) | DJ(x,y). [clausify(17)].
221 -disjoint(x,y) | T(x). [clausify(17)].
222 -disjoint(x,y) | T(y). [clausify(17)].
Eliminating sum/3
223 sum(x,y,z) | overlaps(f2(x,y,z),z) | overlaps(f2(x,y,z),x) | overlaps(f2(x,y,z),y). [clausify(19)].
224 -sum(x,y,z) | T(z). [clausify(18)].
225 -sum(x,y,z) | T(x). [clausify(18)].
226 -sum(x,y,z) | T(y). [clausify(18)].
227 -sum(x,y,z) | -overlaps(u,z) | overlaps(u,x) | overlaps(u,y). [clausify(19)].
228 -sum(x,y,z) | overlaps(u,z) | -overlaps(u,x). [clausify(19)].
229 -sum(x,y,z) | overlaps(u,z) | -overlaps(u,y). [clausify(19)].
Derived: overlaps(f2(x,y,z),z) | overlaps(f2(x,y,z),x) | overlaps(f2(x,y,z),y) | T(z). [resolve(223,a,224,a)].
Derived: overlaps(f2(x,y,z),z) | overlaps(f2(x,y,z),x) | overlaps(f2(x,y,z),y) | T(x). [resolve(223,a,225,a)].
Derived: overlaps(f2(x,y,z),z) | overlaps(f2(x,y,z),x) | overlaps(f2(x,y,z),y) | T(y). [resolve(223,a,226,a)].
Derived: overlaps(f2(x,y,z),z) | overlaps(f2(x,y,z),x) | overlaps(f2(x,y,z),y) | -overlaps(u,z) | overlaps(u,x) | overlaps(u,y). [resolve(223,a,227,a)].
Derived: overlaps(f2(x,y,z),z) | overlaps(f2(x,y,z),x) | overlaps(f2(x,y,z),y) | overlaps(u,z) | -overlaps(u,x). [resolve(223,a,228,a)].
Derived: overlaps(f2(x,y,z),z) | overlaps(f2(x,y,z),x) | overlaps(f2(x,y,z),y) | overlaps(u,z) | -overlaps(u,y). [resolve(223,a,229,a)].
230 sum(x,y,z) | -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),x). [clausify(19)].
Derived: -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),x) | T(z). [resolve(230,a,224,a)].
Derived: -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),x) | T(x). [resolve(230,a,225,a)].
Derived: -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),x) | T(y). [resolve(230,a,226,a)].
Derived: -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),x) | -overlaps(u,z) | overlaps(u,x) | overlaps(u,y). [resolve(230,a,227,a)].
Derived: -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),x) | overlaps(u,z) | -overlaps(u,x). [resolve(230,a,228,a)].
Derived: -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),x) | overlaps(u,z) | -overlaps(u,y). [resolve(230,a,229,a)].
231 sum(x,y,z) | -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),y). [clausify(19)].
Derived: -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),y) | T(z). [resolve(231,a,224,a)].
Derived: -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),y) | T(x). [resolve(231,a,225,a)].
Derived: -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),y) | T(y). [resolve(231,a,226,a)].
Derived: -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),y) | -overlaps(u,z) | overlaps(u,x) | overlaps(u,y). [resolve(231,a,227,a)].
Derived: -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),y) | overlaps(u,z) | -overlaps(u,x). [resolve(231,a,228,a)].
Derived: -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),y) | overlaps(u,z) | -overlaps(u,y). [resolve(231,a,229,a)].
232 -sum(x,y,z) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(84,b,85,c)].
Derived: -PRE(x,y) | -PRE(x,z) | PRE(x,u) | overlaps(f2(y,z,u),u) | overlaps(f2(y,z,u),y) | overlaps(f2(y,z,u),z). [resolve(232,a,223,a)].
Derived: -PRE(x,y) | -PRE(x,z) | PRE(x,u) | -overlaps(f2(y,z,u),u) | -overlaps(f2(y,z,u),y). [resolve(232,a,230,a)].
Derived: -PRE(x,y) | -PRE(x,z) | PRE(x,u) | -overlaps(f2(y,z,u),u) | -overlaps(f2(y,z,u),z). [resolve(232,a,231,a)].
233 -T(x) | -T(y) | -T(z) | -T(u) | -O(u,z) | O(u,x) | O(u,y) | -sum(x,y,z). [resolve(87,d,84,b)].
Derived: -T(x) | -T(y) | -T(z) | -T(u) | -O(u,z) | O(u,x) | O(u,y) | overlaps(f2(x,y,z),z) | overlaps(f2(x,y,z),x) | overlaps(f2(x,y,z),y). [resolve(233,h,223,a)].
Derived: -T(x) | -T(y) | -T(z) | -T(u) | -O(u,z) | O(u,x) | O(u,y) | -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),x). [resolve(233,h,230,a)].
Derived: -T(x) | -T(y) | -T(z) | -T(u) | -O(u,z) | O(u,x) | O(u,y) | -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),y). [resolve(233,h,231,a)].
234 -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,x) | -sum(x,y,z). [resolve(88,d,84,b)].
Derived: -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,x) | overlaps(f2(x,y,z),z) | overlaps(f2(x,y,z),x) | overlaps(f2(x,y,z),y). [resolve(234,g,223,a)].
Derived: -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,x) | -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),x). [resolve(234,g,230,a)].
Derived: -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,x) | -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),y). [resolve(234,g,231,a)].
235 -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,y) | -sum(x,y,z). [resolve(89,d,84,b)].
Derived: -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,y) | overlaps(f2(x,y,z),z) | overlaps(f2(x,y,z),x) | overlaps(f2(x,y,z),y). [resolve(235,g,223,a)].
Derived: -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,y) | -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),x). [resolve(235,g,230,a)].
Derived: -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,y) | -overlaps(f2(x,y,z),z) | -overlaps(f2(x,y,z),y). [resolve(235,g,231,a)].
236 -T(x) | -T(y) | -T(z) | T(f10(x,y,z)) | sum(x,y,z) | -T(z) | -T(x) | -T(y). [resolve(90,d,86,b)].
Derived: -T(x) | -T(y) | -T(z) | T(f10(x,y,z)) | -T(z) | -T(x) | -T(y) | -overlaps(u,z) | overlaps(u,x) | overlaps(u,y). [resolve(236,e,227,a)].
Derived: -T(x) | -T(y) | -T(z) | T(f10(x,y,z)) | -T(z) | -T(x) | -T(y) | overlaps(u,z) | -overlaps(u,x). [resolve(236,e,228,a)].
Derived: -T(x) | -T(y) | -T(z) | T(f10(x,y,z)) | -T(z) | -T(x) | -T(y) | overlaps(u,z) | -overlaps(u,y). [resolve(236,e,229,a)].
Derived: -T(x) | -T(y) | -T(z) | T(f10(x,y,z)) | -T(z) | -T(x) | -T(y) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(236,e,232,a)].
237 -T(x) | -T(y) | -T(z) | O(f10(x,y,z),z) | O(f10(x,y,z),x) | O(f10(x,y,z),y) | sum(x,y,z) | -T(z) | -T(x) | -T(y). [resolve(91,d,86,b)].
Derived: -T(x) | -T(y) | -T(z) | O(f10(x,y,z),z) | O(f10(x,y,z),x) | O(f10(x,y,z),y) | -T(z) | -T(x) | -T(y) | -overlaps(u,z) | overlaps(u,x) | overlaps(u,y). [resolve(237,g,227,a)].
Derived: -T(x) | -T(y) | -T(z) | O(f10(x,y,z),z) | O(f10(x,y,z),x) | O(f10(x,y,z),y) | -T(z) | -T(x) | -T(y) | overlaps(u,z) | -overlaps(u,x). [resolve(237,g,228,a)].
Derived: -T(x) | -T(y) | -T(z) | O(f10(x,y,z),z) | O(f10(x,y,z),x) | O(f10(x,y,z),y) | -T(z) | -T(x) | -T(y) | overlaps(u,z) | -overlaps(u,y). [resolve(237,g,229,a)].
Derived: -T(x) | -T(y) | -T(z) | O(f10(x,y,z),z) | O(f10(x,y,z),x) | O(f10(x,y,z),y) | -T(z) | -T(x) | -T(y) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(237,g,232,a)].
238 -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),x) | sum(x,y,z) | -T(z) | -T(x) | -T(y). [resolve(92,d,86,b)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),x) | -T(z) | -T(x) | -T(y) | -overlaps(u,z) | overlaps(u,x) | overlaps(u,y). [resolve(238,f,227,a)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),x) | -T(z) | -T(x) | -T(y) | overlaps(u,z) | -overlaps(u,x). [resolve(238,f,228,a)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),x) | -T(z) | -T(x) | -T(y) | overlaps(u,z) | -overlaps(u,y). [resolve(238,f,229,a)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),x) | -T(z) | -T(x) | -T(y) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(238,f,232,a)].
239 -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),y) | sum(x,y,z) | -T(z) | -T(x) | -T(y). [resolve(93,d,86,b)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),y) | -T(z) | -T(x) | -T(y) | -overlaps(u,z) | overlaps(u,x) | overlaps(u,y). [resolve(239,f,227,a)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),y) | -T(z) | -T(x) | -T(y) | overlaps(u,z) | -overlaps(u,x). [resolve(239,f,228,a)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),y) | -T(z) | -T(x) | -T(y) | overlaps(u,z) | -overlaps(u,y). [resolve(239,f,229,a)].
Derived: -T(x) | -T(y) | -T(z) | -O(f10(x,y,z),z) | -O(f10(x,y,z),y) | -T(z) | -T(x) | -T(y) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(239,f,232,a)].
Eliminating DJ/2
240 -T(x) | -T(y) | -DJ(x,y) | -O(x,y). [clausify(29)].
241 -T(x) | -T(y) | P(x,y) | DJ(f4(x,y),y). [clausify(26)].
Derived: -T(f4(x,y)) | -T(y) | -O(f4(x,y),y) | -T(x) | -T(y) | P(x,y). [resolve(240,c,241,d)].
242 -T(x) | -T(y) | DJ(x,y) | O(x,y). [clausify(29)].
Eliminating U/2
243 -T(x) | -T(y) | U(x,y) | -P(x,z) | -P(y,z) | -T(z). [clausify(30)].
244 -T(x) | -T(y) | -U(x,y) | P(x,f6(x,y)). [clausify(30)].
245 -T(x) | -T(y) | -U(x,y) | P(y,f6(x,y)). [clausify(30)].
246 -T(x) | -T(y) | -U(x,y) | T(f6(x,y)). [clausify(30)].
Derived: -T(x) | -T(y) | -P(x,z) | -P(y,z) | -T(z) | -T(x) | -T(y) | P(x,f6(x,y)). [resolve(243,c,244,c)].
Derived: -T(x) | -T(y) | -P(x,z) | -P(y,z) | -T(z) | -T(x) | -T(y) | P(y,f6(x,y)). [resolve(243,c,245,c)].
Derived: -T(x) | -T(y) | -P(x,z) | -P(y,z) | -T(z) | -T(x) | -T(y) | T(f6(x,y)). [resolve(243,c,246,c)].
247 -T(x) | -T(y) | -U(x,y) | T(f8(x,y)). [clausify(32)].
Derived: -T(x) | -T(y) | T(f8(x,y)) | -T(x) | -T(y) | -P(x,z) | -P(y,z) | -T(z). [resolve(247,c,243,c)].
248 -T(x) | -T(y) | -U(x,y) | -T(z) | -O(z,f8(x,y)) | O(z,x) | O(z,y). [clausify(32)].
Derived: -T(x) | -T(y) | -T(z) | -O(z,f8(x,y)) | O(z,x) | O(z,y) | -T(x) | -T(y) | -P(x,u) | -P(y,u) | -T(u). [resolve(248,c,243,c)].
249 -T(x) | -T(y) | -U(x,y) | -T(z) | O(z,f8(x,y)) | -O(z,x). [clausify(32)].
Derived: -T(x) | -T(y) | -T(z) | O(z,f8(x,y)) | -O(z,x) | -T(x) | -T(y) | -P(x,u) | -P(y,u) | -T(u). [resolve(249,c,243,c)].
250 -T(x) | -T(y) | -U(x,y) | -T(z) | O(z,f8(x,y)) | -O(z,y). [clausify(32)].
Derived: -T(x) | -T(y) | -T(z) | O(z,f8(x,y)) | -O(z,y) | -T(x) | -T(y) | -P(x,u) | -P(y,u) | -T(u). [resolve(250,c,243,c)].
Eliminating AtP/1
251 AtP(x) | -T(x) | T(f7(x)). [clausify(31)].
252 -AtP(x) | T(x). [clausify(31)].
253 -AtP(x) | -T(y) | -P(y,x) | y = x. [clausify(31)].
Derived: -T(x) | T(f7(x)) | -T(y) | -P(y,x) | y = x. [resolve(251,a,253,a)].
254 AtP(x) | -T(x) | P(f7(x),x). [clausify(31)].
Derived: -T(x) | P(f7(x),x) | -T(y) | -P(y,x) | y = x. [resolve(254,a,253,a)].
255 AtP(x) | -T(x) | f7(x) != x. [clausify(31)].
Derived: -T(x) | f7(x) != x | -T(y) | -P(y,x) | y = x. [resolve(255,a,253,a)].
Eliminating R/1
256 -TR(x) | R(x). [clausify(46)].
257 -R(x) | AB(x). [clausify(39)].
Derived: -TR(x) | AB(x). [resolve(256,b,257,a)].
258 -PR(x) | R(x). [clausify(46)].
Derived: -PR(x) | AB(x). [resolve(258,b,257,a)].
259 -AR(x) | R(x). [clausify(46)].
Derived: -AR(x) | AB(x). [resolve(259,b,257,a)].
260 -R(x) | TR(x) | PR(x) | AR(x). [clausify(72)].
261 R(x) | -TR(x). [clausify(72)].
262 R(x) | -PR(x). [clausify(72)].
263 R(x) | -AR(x). [clausify(72)].
Eliminating M/1
264 -PED(x) | M(x) | F(x) | POB(x). [clausify(65)].
265 -M(x) | PED(x). [clausify(40)].
266 PED(x) | -M(x). [clausify(65)].
267 -M(x) | -F(x). [clausify(66)].
268 -M(x) | -POB(x). [clausify(66)].
Eliminating F/1
Eliminating POB/1
269 -APO(x) | POB(x). [clausify(47)].
270 -POB(x) | PED(x). [clausify(40)].
Derived: -APO(x) | PED(x). [resolve(269,b,270,a)].
271 -NAPO(x) | POB(x). [clausify(47)].
Derived: -NAPO(x) | PED(x). [resolve(271,b,270,a)].
272 PED(x) | -POB(x). [clausify(65)].
273 -POB(x) | APO(x) | NAPO(x). [clausify(75)].
274 POB(x) | -APO(x). [clausify(75)].
275 POB(x) | -NAPO(x). [clausify(75)].
Eliminating NPOB/1
276 -MOB(x) | NPOB(x). [clausify(48)].
277 -NPOB(x) | NPED(x). [clausify(41)].
Derived: -MOB(x) | NPED(x). [resolve(276,b,277,a)].
278 -SOB(x) | NPOB(x). [clausify(48)].
Derived: -SOB(x) | NPED(x). [resolve(278,b,277,a)].
279 -NPOB(x) | MOB(x) | SOB(x). [clausify(77)].
280 NPOB(x) | -MOB(x). [clausify(77)].
281 NPOB(x) | -SOB(x). [clausify(77)].
Eliminating ACH/1
282 -EV(x) | ACH(x) | ACC(x). [clausify(68)].
283 -ACH(x) | EV(x). [clausify(42)].
284 EV(x) | -ACH(x). [clausify(68)].
285 -ACH(x) | -ACC(x). [clausify(69)].
Eliminating ACC/1
Eliminating ST/1
286 -STV(x) | ST(x) | PRO(x). [clausify(70)].
287 -ST(x) | STV(x). [clausify(43)].
288 STV(x) | -ST(x). [clausify(70)].
289 -ST(x) | -PRO(x). [clausify(71)].
Eliminating PRO/1
Eliminating TL/1
Eliminating SL/1
Eliminating TR/1
290 -TR(x) | -PR(x). [clausify(73)].
291 -T(x) | TR(x). [clausify(49)].
Derived: -PR(x) | -T(x). [resolve(290,a,291,b)].
292 -TR(x) | -AR(x). [clausify(73)].
Derived: -AR(x) | -T(x). [resolve(292,a,291,b)].
293 -TR(x) | AB(x). [resolve(256,b,257,a)].
Derived: AB(x) | -T(x). [resolve(293,a,291,b)].
Eliminating S/1
Eliminating ASO/1
294 -SAG(x) | ASO(x). [clausify(52)].
295 -ASO(x) | SOB(x). [clausify(51)].
Derived: -SAG(x) | SOB(x). [resolve(294,b,295,a)].
296 -SC(x) | ASO(x). [clausify(52)].
Derived: -SC(x) | SOB(x). [resolve(296,b,295,a)].
297 -SOB(x) | ASO(x) | NASO(x). [clausify(79)].
298 SOB(x) | -ASO(x). [clausify(79)].
299 -ASO(x) | -NASO(x). [clausify(80)].
Derived: -NASO(x) | -SAG(x). [resolve(299,a,294,b)].
Derived: -NASO(x) | -SC(x). [resolve(299,a,296,b)].
300 -ASO(x) | SAG(x) | SC(x). [clausify(81)].
Derived: SAG(x) | SC(x) | -SOB(x) | NASO(x). [resolve(300,a,297,b)].
301 ASO(x) | -SAG(x). [clausify(81)].
302 ASO(x) | -SC(x). [clausify(81)].
Eliminating NASO/1
303 SAG(x) | SC(x) | -SOB(x) | NASO(x). [resolve(300,a,297,b)].
304 -NASO(x) | SOB(x). [clausify(51)].
305 SOB(x) | -NASO(x). [clausify(79)].
306 -NASO(x) | -SAG(x). [resolve(299,a,294,b)].
307 -NASO(x) | -SC(x). [resolve(299,a,296,b)].
Eliminating EV/1
308 EV(x) | STV(x) | -L_2(x). [resolve(141,a,131,b)].
309 -EV(x) | -STV(x). [clausify(61)].
310 -EV(x) | PRE(x,f1(x)). [resolve(136,b,132,a)].
311 -EV(x) | line(x). [resolve(136,b,133,b)].
312 -EV(x) | L_2(x). [resolve(136,b,134,b)].
313 -EV(x) | PT(x). [resolve(136,b,135,a)].
314 -AB(x) | -EV(x). [resolve(140,a,136,b)].
Derived: STV(x) | -L_2(x) | PRE(x,f1(x)). [resolve(308,a,310,a)].
Derived: STV(x) | -L_2(x) | line(x). [resolve(308,a,311,a)].
Derived: STV(x) | -L_2(x) | PT(x). [resolve(308,a,313,a)].
Derived: STV(x) | -L_2(x) | -AB(x). [resolve(308,a,314,b)].
315 -L_1(x) | -EV(x). [resolve(150,a,136,b)].
Derived: -L_1(x) | STV(x) | -L_2(x). [resolve(315,b,308,a)].
316 -PED(x) | -EV(x). [resolve(151,a,136,b)].
Derived: -PED(x) | STV(x) | -L_2(x). [resolve(316,b,308,a)].
317 -NPED(x) | -EV(x). [resolve(152,a,136,b)].
Derived: -NPED(x) | STV(x) | -L_2(x). [resolve(317,b,308,a)].
318 -AS(x) | -EV(x). [resolve(153,a,136,b)].
Derived: -AS(x) | STV(x) | -L_2(x). [resolve(318,b,308,a)].
319 -EV(x) | -L_3(x). [resolve(176,a,157,b)].
Derived: -L_3(x) | STV(x) | -L_2(x). [resolve(319,a,308,a)].
320 -EV(x) | -TQ(x). [resolve(176,a,162,b)].
Derived: -TQ(x) | STV(x) | -L_2(x). [resolve(320,a,308,a)].
321 -EV(x) | -PQ(x). [resolve(176,a,163,b)].
Derived: -PQ(x) | STV(x) | -L_2(x). [resolve(321,a,308,a)].
322 -EV(x) | -AQ(x). [resolve(176,a,164,b)].
Derived: -AQ(x) | STV(x) | -L_2(x). [resolve(322,a,308,a)].
323 L_1(x) | -line(x) | L_2(x) | -EV(x). [resolve(179,c,176,a)].
324 L_1(x) | -line(x) | EV(x) | STV(x) | L_3(x). [resolve(182,c,160,b)].
Derived: L_1(x) | -line(x) | STV(x) | L_3(x) | PRE(x,f1(x)). [resolve(324,c,310,a)].
Derived: L_1(x) | -line(x) | STV(x) | L_3(x) | L_2(x). [resolve(324,c,312,a)].
Derived: L_1(x) | -line(x) | STV(x) | L_3(x) | -TQ(x). [resolve(324,c,320,a)].
Derived: L_1(x) | -line(x) | STV(x) | L_3(x) | -PQ(x). [resolve(324,c,321,a)].
Derived: L_1(x) | -line(x) | STV(x) | L_3(x) | -AQ(x). [resolve(324,c,322,a)].
325 L_1(x) | -line(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x). [resolve(182,c,167,a)].
Derived: L_1(x) | -line(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | PRE(x,f1(x)). [resolve(325,c,310,a)].
Derived: L_1(x) | -line(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | L_2(x). [resolve(325,c,312,a)].
Derived: L_1(x) | -line(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -L_3(x). [resolve(325,c,319,a)].
326 L_1(x) | -line(x) | EV(x) | STV(x) | -PED(x). [resolve(182,c,172,a)].
327 L_1(x) | -line(x) | EV(x) | STV(x) | -NPED(x). [resolve(182,c,173,a)].
328 L_1(x) | -line(x) | EV(x) | STV(x) | -AS(x). [resolve(182,c,174,a)].
329 L_1(x) | -line(x) | EV(x) | STV(x) | -L_2(x). [resolve(182,c,175,a)].
330 -PT(x) | AB(x) | L_1(x) | L_2(x) | -EV(x). [resolve(187,b,176,a)].
331 -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | L_3(x). [resolve(188,b,160,b)].
Derived: -PT(x) | AB(x) | L_1(x) | STV(x) | L_3(x) | PRE(x,f1(x)). [resolve(331,d,310,a)].
Derived: -PT(x) | AB(x) | L_1(x) | STV(x) | L_3(x) | line(x). [resolve(331,d,311,a)].
Derived: -PT(x) | AB(x) | L_1(x) | STV(x) | L_3(x) | L_2(x). [resolve(331,d,312,a)].
Derived: -PT(x) | AB(x) | L_1(x) | STV(x) | L_3(x) | -TQ(x). [resolve(331,d,320,a)].
Derived: -PT(x) | AB(x) | L_1(x) | STV(x) | L_3(x) | -PQ(x). [resolve(331,d,321,a)].
Derived: -PT(x) | AB(x) | L_1(x) | STV(x) | L_3(x) | -AQ(x). [resolve(331,d,322,a)].
332 -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x). [resolve(188,b,167,a)].
Derived: -PT(x) | AB(x) | L_1(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | PRE(x,f1(x)). [resolve(332,d,310,a)].
Derived: -PT(x) | AB(x) | L_1(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | line(x). [resolve(332,d,311,a)].
Derived: -PT(x) | AB(x) | L_1(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | L_2(x). [resolve(332,d,312,a)].
Derived: -PT(x) | AB(x) | L_1(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -L_3(x). [resolve(332,d,319,a)].
333 -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -PED(x). [resolve(188,b,172,a)].
334 -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -NPED(x). [resolve(188,b,173,a)].
335 -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -AS(x). [resolve(188,b,174,a)].
336 -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -L_2(x). [resolve(188,b,175,a)].
337 PED(x) | NPED(x) | AS(x) | -line(x) | L_2(x) | -EV(x). [resolve(197,e,176,a)].
338 PED(x) | NPED(x) | AS(x) | -line(x) | EV(x) | STV(x) | L_3(x). [resolve(198,e,160,b)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | L_3(x) | PRE(x,f1(x)). [resolve(338,e,310,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | L_3(x) | L_2(x). [resolve(338,e,312,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | L_3(x) | PT(x). [resolve(338,e,313,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | L_3(x) | -AB(x). [resolve(338,e,314,b)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | L_3(x) | -L_1(x). [resolve(338,e,315,b)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | L_3(x) | -TQ(x). [resolve(338,e,320,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | L_3(x) | -PQ(x). [resolve(338,e,321,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | L_3(x) | -AQ(x). [resolve(338,e,322,a)].
339 PED(x) | NPED(x) | AS(x) | -line(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x). [resolve(198,e,167,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | PRE(x,f1(x)). [resolve(339,e,310,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | L_2(x). [resolve(339,e,312,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | PT(x). [resolve(339,e,313,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -AB(x). [resolve(339,e,314,b)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -L_1(x). [resolve(339,e,315,b)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -L_3(x). [resolve(339,e,319,a)].
340 PED(x) | NPED(x) | AS(x) | -line(x) | EV(x) | STV(x) | -L_1(x). [resolve(198,e,171,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | -L_1(x) | PRE(x,f1(x)). [resolve(340,e,310,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | -L_1(x) | L_2(x). [resolve(340,e,312,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | -L_1(x) | PT(x). [resolve(340,e,313,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | -L_1(x) | -AB(x). [resolve(340,e,314,b)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | STV(x) | -L_1(x) | -L_1(x). [resolve(340,e,315,b)].
341 PED(x) | NPED(x) | AS(x) | -line(x) | EV(x) | STV(x) | -L_2(x). [resolve(198,e,175,a)].
342 PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | -EV(x). [resolve(199,e,176,a)].
343 PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | EV(x) | STV(x) | L_3(x). [resolve(200,e,160,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | STV(x) | L_3(x) | PRE(x,f1(x)). [resolve(343,f,310,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | STV(x) | L_3(x) | line(x). [resolve(343,f,311,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | STV(x) | L_3(x) | L_2(x). [resolve(343,f,312,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | STV(x) | L_3(x) | -TQ(x). [resolve(343,f,320,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | STV(x) | L_3(x) | -PQ(x). [resolve(343,f,321,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | STV(x) | L_3(x) | -AQ(x). [resolve(343,f,322,a)].
344 PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x). [resolve(200,e,167,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | PRE(x,f1(x)). [resolve(344,f,310,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | line(x). [resolve(344,f,311,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | L_2(x). [resolve(344,f,312,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -L_3(x). [resolve(344,f,319,a)].
345 PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | EV(x) | STV(x) | -L_1(x). [resolve(200,e,171,a)].
346 PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | EV(x) | STV(x) | -L_2(x). [resolve(200,e,175,a)].
Eliminating TQ/1
347 TQ(x) | PQ(x) | AQ(x) | -L_3(x). [resolve(167,a,157,b)].
348 -TQ(x) | -PQ(x). [clausify(63)].
349 -TQ(x) | -AQ(x). [clausify(63)].
350 -TQ(x) | PRE(x,f1(x)). [resolve(162,b,158,a)].
351 -TQ(x) | line(x). [resolve(162,b,159,b)].
352 -TQ(x) | L_3(x). [resolve(162,b,160,b)].
353 -TQ(x) | PT(x). [resolve(162,b,161,a)].
354 -AB(x) | -TQ(x). [resolve(166,a,162,b)].
Derived: PQ(x) | AQ(x) | -L_3(x) | PRE(x,f1(x)). [resolve(347,a,350,a)].
Derived: PQ(x) | AQ(x) | -L_3(x) | line(x). [resolve(347,a,351,a)].
Derived: PQ(x) | AQ(x) | -L_3(x) | PT(x). [resolve(347,a,353,a)].
Derived: PQ(x) | AQ(x) | -L_3(x) | -AB(x). [resolve(347,a,354,b)].
355 -L_1(x) | -TQ(x). [resolve(171,a,162,b)].
Derived: -L_1(x) | PQ(x) | AQ(x) | -L_3(x). [resolve(355,b,347,a)].
356 -PED(x) | -TQ(x). [resolve(172,a,162,b)].
Derived: -PED(x) | PQ(x) | AQ(x) | -L_3(x). [resolve(356,b,347,a)].
357 -NPED(x) | -TQ(x). [resolve(173,a,162,b)].
Derived: -NPED(x) | PQ(x) | AQ(x) | -L_3(x). [resolve(357,b,347,a)].
358 -AS(x) | -TQ(x). [resolve(174,a,162,b)].
Derived: -AS(x) | PQ(x) | AQ(x) | -L_3(x). [resolve(358,b,347,a)].
359 -L_2(x) | -TQ(x). [resolve(175,a,162,b)].
Derived: -L_2(x) | PQ(x) | AQ(x) | -L_3(x). [resolve(359,b,347,a)].
360 -STV(x) | -TQ(x). [resolve(177,a,162,b)].
Derived: -STV(x) | PQ(x) | AQ(x) | -L_3(x). [resolve(360,b,347,a)].
361 L_1(x) | -line(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x). [resolve(179,c,167,a)].
Derived: L_1(x) | -line(x) | L_2(x) | PQ(x) | AQ(x) | PRE(x,f1(x)). [resolve(361,d,350,a)].
Derived: L_1(x) | -line(x) | L_2(x) | PQ(x) | AQ(x) | L_3(x). [resolve(361,d,352,a)].
362 -PT(x) | AB(x) | L_1(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x). [resolve(187,b,167,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | PQ(x) | AQ(x) | PRE(x,f1(x)). [resolve(362,e,350,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | PQ(x) | AQ(x) | line(x). [resolve(362,e,351,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | PQ(x) | AQ(x) | L_3(x). [resolve(362,e,352,a)].
363 -PED(x) | L_1(x) | -line(x) | TQ(x) | PQ(x) | AQ(x). [resolve(189,d,167,a)].
364 -PED(x) | -PT(x) | AB(x) | L_1(x) | TQ(x) | PQ(x) | AQ(x). [resolve(190,c,167,a)].
365 -NPED(x) | L_1(x) | -line(x) | TQ(x) | PQ(x) | AQ(x). [resolve(191,d,167,a)].
366 -NPED(x) | -PT(x) | AB(x) | L_1(x) | TQ(x) | PQ(x) | AQ(x). [resolve(192,c,167,a)].
367 -AS(x) | L_1(x) | -line(x) | TQ(x) | PQ(x) | AQ(x). [resolve(193,d,167,a)].
368 -AS(x) | -PT(x) | AB(x) | L_1(x) | TQ(x) | PQ(x) | AQ(x). [resolve(194,c,167,a)].
369 PED(x) | NPED(x) | AS(x) | -line(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x). [resolve(197,e,167,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | L_2(x) | PQ(x) | AQ(x) | PRE(x,f1(x)). [resolve(369,f,350,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | L_2(x) | PQ(x) | AQ(x) | L_3(x). [resolve(369,f,352,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | L_2(x) | PQ(x) | AQ(x) | PT(x). [resolve(369,f,353,a)].
Derived: PED(x) | NPED(x) | AS(x) | -line(x) | L_2(x) | PQ(x) | AQ(x) | -AB(x). [resolve(369,f,354,b)].
370 PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x). [resolve(199,e,167,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | PQ(x) | AQ(x) | PRE(x,f1(x)). [resolve(370,g,350,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | PQ(x) | AQ(x) | line(x). [resolve(370,g,351,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | PQ(x) | AQ(x) | L_3(x). [resolve(370,g,352,a)].
371 PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -L_1(x) | TQ(x) | PQ(x) | AQ(x). [resolve(201,e,167,a)].
372 -TQ(x) | STV(x) | -L_2(x). [resolve(320,a,308,a)].
Derived: STV(x) | -L_2(x) | -PED(x) | L_1(x) | -line(x) | PQ(x) | AQ(x). [resolve(372,a,363,d)].
Derived: STV(x) | -L_2(x) | -PED(x) | -PT(x) | AB(x) | L_1(x) | PQ(x) | AQ(x). [resolve(372,a,364,e)].
Derived: STV(x) | -L_2(x) | -NPED(x) | L_1(x) | -line(x) | PQ(x) | AQ(x). [resolve(372,a,365,d)].
Derived: STV(x) | -L_2(x) | -NPED(x) | -PT(x) | AB(x) | L_1(x) | PQ(x) | AQ(x). [resolve(372,a,366,e)].
Derived: STV(x) | -L_2(x) | -AS(x) | L_1(x) | -line(x) | PQ(x) | AQ(x). [resolve(372,a,367,d)].
Derived: STV(x) | -L_2(x) | -AS(x) | -PT(x) | AB(x) | L_1(x) | PQ(x) | AQ(x). [resolve(372,a,368,e)].
Derived: STV(x) | -L_2(x) | PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -L_1(x) | PQ(x) | AQ(x). [resolve(372,a,371,g)].
373 L_1(x) | -line(x) | STV(x) | L_3(x) | -TQ(x). [resolve(324,c,320,a)].
Derived: L_1(x) | -line(x) | STV(x) | L_3(x) | -PED(x) | L_1(x) | -line(x) | PQ(x) | AQ(x). [resolve(373,e,363,d)].
Derived: L_1(x) | -line(x) | STV(x) | L_3(x) | -NPED(x) | L_1(x) | -line(x) | PQ(x) | AQ(x). [resolve(373,e,365,d)].
Derived: L_1(x) | -line(x) | STV(x) | L_3(x) | -AS(x) | L_1(x) | -line(x) | PQ(x) | AQ(x). [resolve(373,e,367,d)].
374 L_1(x) | -line(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | PRE(x,f1(x)). [resolve(325,c,310,a)].
Derived: L_1(x) | -line(x) | STV(x) | PQ(x) | AQ(x) | PRE(x,f1(x)) | PRE(x,f1(x)). [resolve(374,d,350,a)].
375 L_1(x) | -line(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | L_2(x). [resolve(325,c,312,a)].
Derived: L_1(x) | -line(x) | STV(x) | PQ(x) | AQ(x) | L_2(x) | PT(x). [resolve(375,d,353,a)].
Derived: L_1(x) | -line(x) | STV(x) | PQ(x) | AQ(x) | L_2(x) | -AB(x). [resolve(375,d,354,b)].
Derived: L_1(x) | -line(x) | STV(x) | PQ(x) | AQ(x) | L_2(x) | -PED(x). [resolve(375,d,356,b)].
Derived: L_1(x) | -line(x) | STV(x) | PQ(x) | AQ(x) | L_2(x) | -NPED(x). [resolve(375,d,357,b)].
Derived: L_1(x) | -line(x) | STV(x) | PQ(x) | AQ(x) | L_2(x) | -AS(x). [resolve(375,d,358,b)].
376 L_1(x) | -line(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -L_3(x). [resolve(325,c,319,a)].
377 -PT(x) | AB(x) | L_1(x) | STV(x) | L_3(x) | -TQ(x). [resolve(331,d,320,a)].