-
Notifications
You must be signed in to change notification settings - Fork 35
/
ex0930_participation2_1.p9.out
1548 lines (1453 loc) · 113 KB
/
ex0930_participation2_1.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 3444 was started by cchui on stl-ws4.mie.utoronto.ca,
Tue Oct 1 09:31:25 2013
The command was "prover9 -t 120 -f test/p9/dolce_participation.p9 test/p9/dolce_participation2ideal_cem_line_downward_in_foliation.p9 test/p9/dolce_present.p9 test/p9/dolce_time_mereology.p9 test/p9/dolce_taxonomy.p9 test/p9/options.txt test/p9/ex0930_participation2_1.p9".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file test/p9/dolce_participation.p9
formulas(sos).
(all x all y all t (PC(x,y,t) -> ED(x) & PD(y) & T(t))).
(all x all t (PD(x) & PRE(x,t) -> (exists y PC(y,x,t)))).
(all x (ED(x) -> (exists y exists t PC(x,y,t)))).
(all x all y all t (PC(x,y,t) -> PRE(x,t) & PRE(y,t))).
(all x all y all t (PC(x,y,t) <-> (all t1 (P(t1,t) -> PC(x,y,t1))))).
end_of_list.
% Reading from file test/p9/dolce_participation2ideal_cem_line_downward_in_foliation.p9
formulas(sos).
(all x (point2(x) <-> T(x))).
(all x (line2(x) <-> ED(x))).
(all x (plane2(x) <-> PD(x))).
(all x all y (in2(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 all y all z (tin2(x,y,z) <-> PC(x,y,z))).
(all x all y (part2(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 (atomic_part(x) <-> AtP(x) & T(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))).
end_of_list.
% 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_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/ex0930_participation2_1.p9
formulas(goals).
(all x (L_1(x) -> -L_2(x))).
end_of_list.
============================== end of input ==========================
% From the command line: assign(max_seconds, 120).
============================== PROCESS NON-CLAUSAL FORMULAS ==========
% Formulas that are not ordinary clauses:
1 (all x all y all t (PC(x,y,t) -> ED(x) & PD(y) & T(t))) # label(non_clause). [assumption].
2 (all x all t (PD(x) & PRE(x,t) -> (exists y PC(y,x,t)))) # label(non_clause). [assumption].
3 (all x (ED(x) -> (exists y exists t PC(x,y,t)))) # label(non_clause). [assumption].
4 (all x all y all t (PC(x,y,t) -> PRE(x,t) & PRE(y,t))) # label(non_clause). [assumption].
5 (all x all y all t (PC(x,y,t) <-> (all t1 (P(t1,t) -> PC(x,y,t1))))) # label(non_clause). [assumption].
6 (all x (point2(x) <-> T(x))) # label(non_clause). [assumption].
7 (all x (line2(x) <-> ED(x))) # label(non_clause). [assumption].
8 (all x (plane2(x) <-> PD(x))) # label(non_clause). [assumption].
9 (all x all y (in2(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].
10 (all x all y all z (tin2(x,y,z) <-> PC(x,y,z))) # label(non_clause). [assumption].
11 (all x all y (part2(x,y) <-> P(x,y) & T(x) & T(y))) # label(non_clause). [assumption].
12 (all x (L_1(x) <-> ED(x))) # label(non_clause). [assumption].
13 (all x (L_2(x) <-> PD(x))) # label(non_clause). [assumption].
14 (all x (L_3(x) <-> Q(x))) # label(non_clause). [assumption].
15 (all x (atomic_part(x) <-> AtP(x) & T(x))) # label(non_clause). [assumption].
16 (all x all y (ppart(x,y) <-> PP(x,y) & T(x) & T(y))) # label(non_clause). [assumption].
17 (all x all y (overlaps(x,y) <-> O(x,y) & T(x) & T(y))) # label(non_clause). [assumption].
18 (all x all y (underlaps(x,y) <-> U(x,y) & T(x) & T(y))) # label(non_clause). [assumption].
19 (all x all y (disjoint(x,y) <-> DJ(x,y) & T(x) & T(y))) # label(non_clause). [assumption].
20 (all x all y all z (sum(x,y,z) <-> SUM(z,x,y) & T(z) & T(x) & T(y))) # label(non_clause). [assumption].
21 (all x (ED(x) | PD(x) | Q(x) -> (exists t PRE(x,t)))) # label(non_clause). [assumption].
22 (all x all t all t1 (PRE(x,t) & P(t1,t) -> PRE(x,t1))) # label(non_clause). [assumption].
23 (all x all t (PRE(x,t) -> T(t))) # label(non_clause). [assumption].
24 (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].
25 (all x all y (P(x,y) -> T(y) & T(y))) # label(non_clause). [assumption].
26 (all x all y (P(x,y) -> (T(x) <-> T(y)))) # label(non_clause). [assumption].
27 (all x all y (T(x) -> P(x,x))) # label(non_clause). [assumption].
28 (all x all y (T(x) & T(y) & P(x,y) & P(y,x) -> x = y)) # label(non_clause). [assumption].
29 (all x all y all z (T(x) & T(y) & P(x,y) & P(y,z) -> P(x,z))) # label(non_clause). [assumption].
30 (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].
31 (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].
32 (all x all y (T(x) & T(y) -> (PP(x,y) <-> P(x,y) & -P(y,x)))) # label(non_clause). [assumption].
33 (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].
34 (all x all y (T(x) & T(y) -> (DJ(x,y) <-> -O(x,y)))) # label(non_clause). [assumption].
35 (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].
36 (all x (AtP(x) <-> T(x) & (all y (T(y) & P(y,x) -> y = x)))) # label(non_clause). [assumption].
37 (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].
38 (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].
39 (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].
40 (all x (ED(x) | PD(x) | Q(x) | AB(x) -> PT(x))) # label(non_clause). [assumption].
41 (all x (PED(x) | NPED(x) | AS(x) -> ED(x))) # label(non_clause). [assumption].
42 (all x (EV(x) | STV(x) -> PD(x))) # label(non_clause). [assumption].
43 (all x (TQ(x) | PQ(x) | AQ(x) -> Q(x))) # label(non_clause). [assumption].
44 (all x (R(x) -> AB(x))) # label(non_clause). [assumption].
45 (all x (M(x) | F(x) | POB(x) -> PED(x))) # label(non_clause). [assumption].
46 (all x (NPOB(x) -> NPED(x))) # label(non_clause). [assumption].
47 (all x (ACH(x) | ACC(x) -> EV(x))) # label(non_clause). [assumption].
48 (all x (ST(x) | PRO(x) -> STV(x))) # label(non_clause). [assumption].
49 (all x (TL(x) -> TQ(x))) # label(non_clause). [assumption].
50 (all x (SL(x) -> PQ(x))) # label(non_clause). [assumption].
51 (all x (TR(x) | PR(x) | AR(x) -> R(x))) # label(non_clause). [assumption].
52 (all x (APO(x) | NAPO(x) -> POB(x))) # label(non_clause). [assumption].
53 (all x (MOB(x) | SOB(x) -> NPOB(x))) # label(non_clause). [assumption].
54 (all x (T(x) -> TR(x))) # label(non_clause). [assumption].
55 (all x (S(x) -> PR(x))) # label(non_clause). [assumption].
56 (all x (ASO(x) | NASO(x) -> SOB(x))) # label(non_clause). [assumption].
57 (all x (SAG(x) | SC(x) -> ASO(x))) # label(non_clause). [assumption].
58 (all x (PT(x) <-> ED(x) | PD(x) | Q(x) | AB(x))) # label(non_clause). [assumption].
59 (all x (ED(x) -> -PD(x) & -Q(x) & -AB(x))) # label(non_clause). [assumption].
60 (all x (PD(x) -> -Q(x) & -AB(x))) # label(non_clause). [assumption].
61 (all x (Q(x) -> -AB(x))) # label(non_clause). [assumption].
62 (all x (ED(x) <-> PED(x) | NPED(x) | AS(x))) # label(non_clause). [assumption].
63 (all x (PED(x) -> -NPED(x) & -AS(x))) # label(non_clause). [assumption].
64 (all x (NPED(x) -> -AS(x))) # label(non_clause). [assumption].
65 (all x (PD(x) <-> EV(x) | STV(x))) # label(non_clause). [assumption].
66 (all x (EV(x) -> -STV(x))) # label(non_clause). [assumption].
67 (all x (Q(x) <-> TQ(x) | PQ(x) | AQ(x))) # label(non_clause). [assumption].
68 (all x (TQ(x) -> -PQ(x) & -AQ(x))) # label(non_clause). [assumption].
69 (all x (PQ(x) -> -AQ(x))) # label(non_clause). [assumption].
70 (all x (PED(x) <-> M(x) | F(x) | POB(x))) # label(non_clause). [assumption].
71 (all x (M(x) -> -F(x) & -POB(x))) # label(non_clause). [assumption].
72 (all x (F(x) -> -POB(x))) # label(non_clause). [assumption].
73 (all x (EV(x) <-> ACH(x) | ACC(x))) # label(non_clause). [assumption].
74 (all x (ACH(x) -> -ACC(x))) # label(non_clause). [assumption].
75 (all x (STV(x) <-> ST(x) | PRO(x))) # label(non_clause). [assumption].
76 (all x (ST(x) -> -PRO(x))) # label(non_clause). [assumption].
77 (all x (R(x) <-> TR(x) | PR(x) | AR(x))) # label(non_clause). [assumption].
78 (all x (TR(x) -> -PR(x) & -AR(x))) # label(non_clause). [assumption].
79 (all x (PR(x) -> -AR(x))) # label(non_clause). [assumption].
80 (all x (POB(x) <-> APO(x) | NAPO(x))) # label(non_clause). [assumption].
81 (all x (APO(x) -> -NAPO(x))) # label(non_clause). [assumption].
82 (all x (NPOB(x) <-> MOB(x) | SOB(x))) # label(non_clause). [assumption].
83 (all x (MOB(x) -> -SOB(x))) # label(non_clause). [assumption].
84 (all x (SOB(x) <-> ASO(x) | NASO(x))) # label(non_clause). [assumption].
85 (all x (ASO(x) -> -NASO(x))) # label(non_clause). [assumption].
86 (all x (ASO(x) <-> SAG(x) | SC(x))) # label(non_clause). [assumption].
87 (all x (SAG(x) -> -SC(x))) # label(non_clause). [assumption].
88 (all x (L_1(x) -> -L_2(x))) # label(non_clause) # label(goal). [goal].
============================== end of process non-clausal formulas ===
============================== PROCESS INITIAL CLAUSES ===============
============================== PREDICATE ELIMINATION =================
Eliminating point2/1
89 point2(x) | -T(x). [clausify(6)].
90 -point2(x) | T(x). [clausify(6)].
Eliminating line2/1
91 line2(x) | -ED(x). [clausify(7)].
92 -line2(x) | ED(x). [clausify(7)].
Eliminating plane2/1
93 plane2(x) | -PD(x). [clausify(8)].
94 -plane2(x) | PD(x). [clausify(8)].
Eliminating in2/2
95 in2(x,y) | -PRE(x,y) | -T(y) | -ED(x). [clausify(9)].
96 -in2(x,y) | PRE(x,y) | PRE(y,x) | y = x. [clausify(9)].
97 -in2(x,y) | PRE(x,y) | T(x) | y = x. [clausify(9)].
98 -in2(x,y) | PRE(x,y) | ED(y) | PD(y) | Q(y) | y = x. [clausify(9)].
99 -in2(x,y) | T(y) | PRE(y,x) | y = x. [clausify(9)].
100 -in2(x,y) | T(y) | T(x) | y = x. [clausify(9)].
101 -in2(x,y) | T(y) | ED(y) | PD(y) | Q(y). [clausify(9)].
102 -in2(x,y) | ED(x) | PD(x) | Q(x) | PRE(y,x) | y = x. [clausify(9)].
103 -in2(x,y) | ED(x) | PD(x) | Q(x) | T(x) | y = x. [clausify(9)].
104 -in2(x,y) | ED(x) | PD(x) | Q(x) | ED(y) | PD(y) | Q(y) | y = x. [clausify(9)].
105 in2(x,y) | -PRE(x,y) | -T(y) | -PD(x). [clausify(9)].
106 in2(x,y) | -PRE(x,y) | -T(y) | -Q(x). [clausify(9)].
107 in2(x,y) | -PRE(y,x) | -T(x) | -ED(y). [clausify(9)].
108 in2(x,y) | -PRE(y,x) | -T(x) | -PD(y). [clausify(9)].
109 in2(x,y) | -PRE(y,x) | -T(x) | -Q(y). [clausify(9)].
110 in2(x,y) | y != x | -ED(y). [clausify(9)].
111 in2(x,y) | y != x | -PD(y). [clausify(9)].
112 in2(x,y) | y != x | -Q(y). [clausify(9)].
113 in2(x,y) | y != x | -T(y). [clausify(9)].
Eliminating ED/1
114 -ED(x) | PC(x,f2(x),f3(x)). [clausify(3)].
115 -PC(x,y,z) | ED(x). [clausify(1)].
Derived: PC(x,f2(x),f3(x)) | -PC(x,y,z). [resolve(114,a,115,b)].
116 -L_1(x) | ED(x). [clausify(12)].
Derived: -L_1(x) | PC(x,f2(x),f3(x)). [resolve(116,b,114,a)].
117 L_1(x) | -ED(x). [clausify(12)].
Derived: L_1(x) | -PC(x,y,z). [resolve(117,b,115,b)].
118 -ED(x) | PRE(x,f5(x)). [clausify(21)].
Derived: PRE(x,f5(x)) | -PC(x,y,z). [resolve(118,a,115,b)].
Derived: PRE(x,f5(x)) | -L_1(x). [resolve(118,a,116,b)].
119 -ED(x) | PT(x). [clausify(40)].
Derived: PT(x) | -PC(x,y,z). [resolve(119,a,115,b)].
Derived: PT(x) | -L_1(x). [resolve(119,a,116,b)].
120 -PED(x) | ED(x). [clausify(41)].
Derived: -PED(x) | PC(x,f2(x),f3(x)). [resolve(120,b,114,a)].
Derived: -PED(x) | L_1(x). [resolve(120,b,117,b)].
Derived: -PED(x) | PRE(x,f5(x)). [resolve(120,b,118,a)].
Derived: -PED(x) | PT(x). [resolve(120,b,119,a)].
121 -NPED(x) | ED(x). [clausify(41)].
Derived: -NPED(x) | PC(x,f2(x),f3(x)). [resolve(121,b,114,a)].
Derived: -NPED(x) | L_1(x). [resolve(121,b,117,b)].
Derived: -NPED(x) | PRE(x,f5(x)). [resolve(121,b,118,a)].
Derived: -NPED(x) | PT(x). [resolve(121,b,119,a)].
122 -AS(x) | ED(x). [clausify(41)].
Derived: -AS(x) | PC(x,f2(x),f3(x)). [resolve(122,b,114,a)].
Derived: -AS(x) | L_1(x). [resolve(122,b,117,b)].
Derived: -AS(x) | PRE(x,f5(x)). [resolve(122,b,118,a)].
Derived: -AS(x) | PT(x). [resolve(122,b,119,a)].
123 -PT(x) | ED(x) | PD(x) | Q(x) | AB(x). [clausify(58)].
Derived: -PT(x) | PD(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(123,b,114,a)].
Derived: -PT(x) | PD(x) | Q(x) | AB(x) | L_1(x). [resolve(123,b,117,b)].
Derived: -PT(x) | PD(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(123,b,118,a)].
124 PT(x) | -ED(x). [clausify(58)].
125 -ED(x) | -PD(x). [clausify(59)].
Derived: -PD(x) | -PC(x,y,z). [resolve(125,a,115,b)].
Derived: -PD(x) | -L_1(x). [resolve(125,a,116,b)].
Derived: -PD(x) | -PED(x). [resolve(125,a,120,b)].
Derived: -PD(x) | -NPED(x). [resolve(125,a,121,b)].
Derived: -PD(x) | -AS(x). [resolve(125,a,122,b)].
126 -ED(x) | -Q(x). [clausify(59)].
Derived: -Q(x) | -PC(x,y,z). [resolve(126,a,115,b)].
Derived: -Q(x) | -L_1(x). [resolve(126,a,116,b)].
Derived: -Q(x) | -PED(x). [resolve(126,a,120,b)].
Derived: -Q(x) | -NPED(x). [resolve(126,a,121,b)].
Derived: -Q(x) | -AS(x). [resolve(126,a,122,b)].
127 -ED(x) | -AB(x). [clausify(59)].
Derived: -AB(x) | -PC(x,y,z). [resolve(127,a,115,b)].
Derived: -AB(x) | -L_1(x). [resolve(127,a,116,b)].
Derived: -AB(x) | -PED(x). [resolve(127,a,120,b)].
Derived: -AB(x) | -NPED(x). [resolve(127,a,121,b)].
Derived: -AB(x) | -AS(x). [resolve(127,a,122,b)].
128 -ED(x) | PED(x) | NPED(x) | AS(x). [clausify(62)].
Derived: PED(x) | NPED(x) | AS(x) | -PC(x,y,z). [resolve(128,a,115,b)].
Derived: PED(x) | NPED(x) | AS(x) | -L_1(x). [resolve(128,a,116,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | PD(x) | Q(x) | AB(x). [resolve(128,a,123,b)].
129 ED(x) | -PED(x). [clausify(62)].
130 ED(x) | -NPED(x). [clausify(62)].
131 ED(x) | -AS(x). [clausify(62)].
Eliminating PD/1
132 -PD(x) | -PRE(x,y) | PC(f1(x,y),x,y). [clausify(2)].
133 -PC(x,y,z) | PD(y). [clausify(1)].
Derived: -PRE(x,y) | PC(f1(x,y),x,y) | -PC(z,x,u). [resolve(132,a,133,b)].
134 -L_2(x) | PD(x). [clausify(13)].
Derived: -L_2(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(134,b,132,a)].
135 L_2(x) | -PD(x). [clausify(13)].
Derived: L_2(x) | -PC(y,x,z). [resolve(135,b,133,b)].
136 -PD(x) | PRE(x,f5(x)). [clausify(21)].
Derived: PRE(x,f5(x)) | -PC(y,x,z). [resolve(136,a,133,b)].
Derived: PRE(x,f5(x)) | -L_2(x). [resolve(136,a,134,b)].
137 -PD(x) | PT(x). [clausify(40)].
Derived: PT(x) | -PC(y,x,z). [resolve(137,a,133,b)].
Derived: PT(x) | -L_2(x). [resolve(137,a,134,b)].
138 -EV(x) | PD(x). [clausify(42)].
Derived: -EV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(138,b,132,a)].
Derived: -EV(x) | L_2(x). [resolve(138,b,135,b)].
Derived: -EV(x) | PRE(x,f5(x)). [resolve(138,b,136,a)].
Derived: -EV(x) | PT(x). [resolve(138,b,137,a)].
139 -STV(x) | PD(x). [clausify(42)].
Derived: -STV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(139,b,132,a)].
Derived: -STV(x) | L_2(x). [resolve(139,b,135,b)].
Derived: -STV(x) | PRE(x,f5(x)). [resolve(139,b,136,a)].
Derived: -STV(x) | PT(x). [resolve(139,b,137,a)].
140 PT(x) | -PD(x). [clausify(58)].
141 -PD(x) | -Q(x). [clausify(60)].
Derived: -Q(x) | -PC(y,x,z). [resolve(141,a,133,b)].
Derived: -Q(x) | -L_2(x). [resolve(141,a,134,b)].
Derived: -Q(x) | -EV(x). [resolve(141,a,138,b)].
Derived: -Q(x) | -STV(x). [resolve(141,a,139,b)].
142 -PD(x) | -AB(x). [clausify(60)].
Derived: -AB(x) | -PC(y,x,z). [resolve(142,a,133,b)].
Derived: -AB(x) | -L_2(x). [resolve(142,a,134,b)].
Derived: -AB(x) | -EV(x). [resolve(142,a,138,b)].
Derived: -AB(x) | -STV(x). [resolve(142,a,139,b)].
143 -PD(x) | EV(x) | STV(x). [clausify(65)].
Derived: EV(x) | STV(x) | -PC(y,x,z). [resolve(143,a,133,b)].
Derived: EV(x) | STV(x) | -L_2(x). [resolve(143,a,134,b)].
144 PD(x) | -EV(x). [clausify(65)].
145 PD(x) | -STV(x). [clausify(65)].
146 -PT(x) | PD(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(123,b,114,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(146,b,132,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x). [resolve(146,b,135,b)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)). [resolve(146,b,136,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x). [resolve(146,b,143,a)].
147 -PT(x) | PD(x) | Q(x) | AB(x) | L_1(x). [resolve(123,b,117,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(147,b,132,a)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | L_2(x). [resolve(147,b,135,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | PRE(x,f5(x)). [resolve(147,b,136,a)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | EV(x) | STV(x). [resolve(147,b,143,a)].
148 -PT(x) | PD(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(123,b,118,a)].
Derived: -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(148,b,132,a)].
Derived: -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)) | L_2(x). [resolve(148,b,135,b)].
Derived: -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)) | PRE(x,f5(x)). [resolve(148,b,136,a)].
149 -PD(x) | -PC(x,y,z). [resolve(125,a,115,b)].
Derived: -PC(x,y,z) | -PC(u,x,w). [resolve(149,a,133,b)].
Derived: -PC(x,y,z) | -L_2(x). [resolve(149,a,134,b)].
Derived: -PC(x,y,z) | -EV(x). [resolve(149,a,138,b)].
Derived: -PC(x,y,z) | -STV(x). [resolve(149,a,139,b)].
Derived: -PC(x,y,z) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(149,a,146,b)].
Derived: -PC(x,y,z) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(149,a,147,b)].
150 -PD(x) | -L_1(x). [resolve(125,a,116,b)].
Derived: -L_1(x) | -PC(y,x,z). [resolve(150,a,133,b)].
Derived: -L_1(x) | -L_2(x). [resolve(150,a,134,b)].
Derived: -L_1(x) | -EV(x). [resolve(150,a,138,b)].
Derived: -L_1(x) | -STV(x). [resolve(150,a,139,b)].
Derived: -L_1(x) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(150,a,146,b)].
151 -PD(x) | -PED(x). [resolve(125,a,120,b)].
Derived: -PED(x) | -PC(y,x,z). [resolve(151,a,133,b)].
Derived: -PED(x) | -L_2(x). [resolve(151,a,134,b)].
Derived: -PED(x) | -EV(x). [resolve(151,a,138,b)].
Derived: -PED(x) | -STV(x). [resolve(151,a,139,b)].
Derived: -PED(x) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(151,a,146,b)].
Derived: -PED(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(151,a,147,b)].
152 -PD(x) | -NPED(x). [resolve(125,a,121,b)].
Derived: -NPED(x) | -PC(y,x,z). [resolve(152,a,133,b)].
Derived: -NPED(x) | -L_2(x). [resolve(152,a,134,b)].
Derived: -NPED(x) | -EV(x). [resolve(152,a,138,b)].
Derived: -NPED(x) | -STV(x). [resolve(152,a,139,b)].
Derived: -NPED(x) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(152,a,146,b)].
Derived: -NPED(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(152,a,147,b)].
153 -PD(x) | -AS(x). [resolve(125,a,122,b)].
Derived: -AS(x) | -PC(y,x,z). [resolve(153,a,133,b)].
Derived: -AS(x) | -L_2(x). [resolve(153,a,134,b)].
Derived: -AS(x) | -EV(x). [resolve(153,a,138,b)].
Derived: -AS(x) | -STV(x). [resolve(153,a,139,b)].
Derived: -AS(x) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(153,a,146,b)].
Derived: -AS(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(153,a,147,b)].
154 PED(x) | NPED(x) | AS(x) | -PT(x) | PD(x) | Q(x) | AB(x). [resolve(128,a,123,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(154,e,132,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | L_2(x). [resolve(154,e,135,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | EV(x) | STV(x). [resolve(154,e,143,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -PC(x,y,z). [resolve(154,e,149,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -L_1(x). [resolve(154,e,150,a)].
Eliminating tin2/3
155 tin2(x,y,z) | -PC(x,y,z). [clausify(10)].
156 -tin2(x,y,z) | PC(x,y,z). [clausify(10)].
Eliminating part2/2
157 part2(x,y) | -P(x,y) | -T(x) | -T(y). [clausify(11)].
158 -part2(x,y) | P(x,y). [clausify(11)].
159 -part2(x,y) | T(x). [clausify(11)].
160 -part2(x,y) | T(y). [clausify(11)].
Eliminating L_3/1
161 L_3(x) | -Q(x). [clausify(14)].
162 -L_3(x) | Q(x). [clausify(14)].
Eliminating atomic_part/1
163 atomic_part(x) | -AtP(x) | -T(x). [clausify(15)].
164 -atomic_part(x) | AtP(x). [clausify(15)].
165 -atomic_part(x) | T(x). [clausify(15)].
Eliminating ppart/2
166 ppart(x,y) | -PP(x,y) | -T(x) | -T(y). [clausify(16)].
167 -ppart(x,y) | PP(x,y). [clausify(16)].
168 -ppart(x,y) | T(x). [clausify(16)].
169 -ppart(x,y) | T(y). [clausify(16)].
Eliminating overlaps/2
170 overlaps(x,y) | -O(x,y) | -T(x) | -T(y). [clausify(17)].
171 -overlaps(x,y) | O(x,y). [clausify(17)].
172 -overlaps(x,y) | T(x). [clausify(17)].
173 -overlaps(x,y) | T(y). [clausify(17)].
Eliminating underlaps/2
174 underlaps(x,y) | -U(x,y) | -T(x) | -T(y). [clausify(18)].
175 -underlaps(x,y) | U(x,y). [clausify(18)].
176 -underlaps(x,y) | T(x). [clausify(18)].
177 -underlaps(x,y) | T(y). [clausify(18)].
Eliminating disjoint/2
178 disjoint(x,y) | -DJ(x,y) | -T(x) | -T(y). [clausify(19)].
179 -disjoint(x,y) | DJ(x,y). [clausify(19)].
180 -disjoint(x,y) | T(x). [clausify(19)].
181 -disjoint(x,y) | T(y). [clausify(19)].
Eliminating sum/3
182 sum(x,y,z) | -SUM(z,x,y) | -T(z) | -T(x) | -T(y). [clausify(20)].
183 -sum(x,y,z) | SUM(z,x,y). [clausify(20)].
184 -sum(x,y,z) | T(z). [clausify(20)].
185 -sum(x,y,z) | T(x). [clausify(20)].
186 -sum(x,y,z) | T(y). [clausify(20)].
Eliminating Q/1
187 -TQ(x) | Q(x). [clausify(43)].
188 -Q(x) | PRE(x,f5(x)). [clausify(21)].
189 -Q(x) | PT(x). [clausify(40)].
Derived: -TQ(x) | PRE(x,f5(x)). [resolve(187,b,188,a)].
Derived: -TQ(x) | PT(x). [resolve(187,b,189,a)].
190 -PQ(x) | Q(x). [clausify(43)].
Derived: -PQ(x) | PRE(x,f5(x)). [resolve(190,b,188,a)].
Derived: -PQ(x) | PT(x). [resolve(190,b,189,a)].
191 -AQ(x) | Q(x). [clausify(43)].
Derived: -AQ(x) | PRE(x,f5(x)). [resolve(191,b,188,a)].
Derived: -AQ(x) | PT(x). [resolve(191,b,189,a)].
192 PT(x) | -Q(x). [clausify(58)].
193 -Q(x) | -AB(x). [clausify(61)].
Derived: -AB(x) | -TQ(x). [resolve(193,a,187,b)].
Derived: -AB(x) | -PQ(x). [resolve(193,a,190,b)].
Derived: -AB(x) | -AQ(x). [resolve(193,a,191,b)].
194 -Q(x) | TQ(x) | PQ(x) | AQ(x). [clausify(67)].
195 Q(x) | -TQ(x). [clausify(67)].
196 Q(x) | -PQ(x). [clausify(67)].
197 Q(x) | -AQ(x). [clausify(67)].
198 -Q(x) | -PC(x,y,z). [resolve(126,a,115,b)].
Derived: -PC(x,y,z) | -TQ(x). [resolve(198,a,187,b)].
Derived: -PC(x,y,z) | -PQ(x). [resolve(198,a,190,b)].
Derived: -PC(x,y,z) | -AQ(x). [resolve(198,a,191,b)].
199 -Q(x) | -L_1(x). [resolve(126,a,116,b)].
Derived: -L_1(x) | -TQ(x). [resolve(199,a,187,b)].
Derived: -L_1(x) | -PQ(x). [resolve(199,a,190,b)].
Derived: -L_1(x) | -AQ(x). [resolve(199,a,191,b)].
200 -Q(x) | -PED(x). [resolve(126,a,120,b)].
Derived: -PED(x) | -TQ(x). [resolve(200,a,187,b)].
Derived: -PED(x) | -PQ(x). [resolve(200,a,190,b)].
Derived: -PED(x) | -AQ(x). [resolve(200,a,191,b)].
201 -Q(x) | -NPED(x). [resolve(126,a,121,b)].
Derived: -NPED(x) | -TQ(x). [resolve(201,a,187,b)].
Derived: -NPED(x) | -PQ(x). [resolve(201,a,190,b)].
Derived: -NPED(x) | -AQ(x). [resolve(201,a,191,b)].
202 -Q(x) | -AS(x). [resolve(126,a,122,b)].
Derived: -AS(x) | -TQ(x). [resolve(202,a,187,b)].
Derived: -AS(x) | -PQ(x). [resolve(202,a,190,b)].
Derived: -AS(x) | -AQ(x). [resolve(202,a,191,b)].
203 -Q(x) | -PC(y,x,z). [resolve(141,a,133,b)].
Derived: -PC(x,y,z) | -TQ(y). [resolve(203,a,187,b)].
Derived: -PC(x,y,z) | -PQ(y). [resolve(203,a,190,b)].
Derived: -PC(x,y,z) | -AQ(y). [resolve(203,a,191,b)].
204 -Q(x) | -L_2(x). [resolve(141,a,134,b)].
Derived: -L_2(x) | -TQ(x). [resolve(204,a,187,b)].
Derived: -L_2(x) | -PQ(x). [resolve(204,a,190,b)].
Derived: -L_2(x) | -AQ(x). [resolve(204,a,191,b)].
205 -Q(x) | -EV(x). [resolve(141,a,138,b)].
Derived: -EV(x) | -TQ(x). [resolve(205,a,187,b)].
Derived: -EV(x) | -PQ(x). [resolve(205,a,190,b)].
Derived: -EV(x) | -AQ(x). [resolve(205,a,191,b)].
206 -Q(x) | -STV(x). [resolve(141,a,139,b)].
Derived: -STV(x) | -TQ(x). [resolve(206,a,187,b)].
Derived: -STV(x) | -PQ(x). [resolve(206,a,190,b)].
Derived: -STV(x) | -AQ(x). [resolve(206,a,191,b)].
207 -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(146,b,132,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)). [resolve(207,b,188,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x). [resolve(207,b,194,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(x,z,u). [resolve(207,b,198,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -L_1(x). [resolve(207,b,199,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -PED(x). [resolve(207,b,200,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -NPED(x). [resolve(207,b,201,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -AS(x). [resolve(207,b,202,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(z,x,u). [resolve(207,b,203,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -L_2(x). [resolve(207,b,204,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -EV(x). [resolve(207,b,205,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -STV(x). [resolve(207,b,206,a)].
208 -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x). [resolve(146,b,135,b)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | PRE(x,f5(x)). [resolve(208,b,188,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | TQ(x) | PQ(x) | AQ(x). [resolve(208,b,194,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -PC(x,y,z). [resolve(208,b,198,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -L_1(x). [resolve(208,b,199,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -PED(x). [resolve(208,b,200,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -NPED(x). [resolve(208,b,201,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -AS(x). [resolve(208,b,202,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -PC(y,x,z). [resolve(208,b,203,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -EV(x). [resolve(208,b,205,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -STV(x). [resolve(208,b,206,a)].
209 -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)). [resolve(146,b,136,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)). [resolve(209,b,188,a)].
210 -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x). [resolve(146,b,143,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x). [resolve(210,b,194,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -PC(x,y,z). [resolve(210,b,198,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -L_1(x). [resolve(210,b,199,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -PED(x). [resolve(210,b,200,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -NPED(x). [resolve(210,b,201,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -AS(x). [resolve(210,b,202,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -PC(y,x,z). [resolve(210,b,203,a)].
Derived: -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -L_2(x). [resolve(210,b,204,a)].
211 -PT(x) | Q(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(147,b,132,a)].
Derived: -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)). [resolve(211,b,188,a)].
Derived: -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x). [resolve(211,b,194,a)].
Derived: -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(x,z,u). [resolve(211,b,198,a)].
Derived: -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -PED(x). [resolve(211,b,200,a)].
Derived: -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -NPED(x). [resolve(211,b,201,a)].
Derived: -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -AS(x). [resolve(211,b,202,a)].
Derived: -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(z,x,u). [resolve(211,b,203,a)].
Derived: -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -L_2(x). [resolve(211,b,204,a)].
Derived: -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -EV(x). [resolve(211,b,205,a)].
Derived: -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -STV(x). [resolve(211,b,206,a)].
212 -PT(x) | Q(x) | AB(x) | L_1(x) | L_2(x). [resolve(147,b,135,b)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | PRE(x,f5(x)). [resolve(212,b,188,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x). [resolve(212,b,194,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | -PC(x,y,z). [resolve(212,b,198,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | -PED(x). [resolve(212,b,200,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | -NPED(x). [resolve(212,b,201,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | -AS(x). [resolve(212,b,202,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | -PC(y,x,z). [resolve(212,b,203,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | -EV(x). [resolve(212,b,205,a)].
Derived: -PT(x) | AB(x) | L_1(x) | L_2(x) | -STV(x). [resolve(212,b,206,a)].
213 -PT(x) | Q(x) | AB(x) | L_1(x) | PRE(x,f5(x)). [resolve(147,b,136,a)].
Derived: -PT(x) | AB(x) | L_1(x) | PRE(x,f5(x)) | PRE(x,f5(x)). [resolve(213,b,188,a)].
214 -PT(x) | Q(x) | AB(x) | L_1(x) | EV(x) | STV(x). [resolve(147,b,143,a)].
Derived: -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x). [resolve(214,b,194,a)].
Derived: -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -PC(x,y,z). [resolve(214,b,198,a)].
Derived: -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -PED(x). [resolve(214,b,200,a)].
Derived: -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -NPED(x). [resolve(214,b,201,a)].
Derived: -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -AS(x). [resolve(214,b,202,a)].
Derived: -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -PC(y,x,z). [resolve(214,b,203,a)].
Derived: -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -L_2(x). [resolve(214,b,204,a)].
215 -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(148,b,132,a)].
Derived: -PT(x) | AB(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)). [resolve(215,b,188,a)].
216 -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)) | L_2(x). [resolve(148,b,135,b)].
Derived: -PT(x) | AB(x) | PRE(x,f5(x)) | L_2(x) | PRE(x,f5(x)). [resolve(216,b,188,a)].
217 -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)) | PRE(x,f5(x)). [resolve(148,b,136,a)].
Derived: -PT(x) | AB(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | PRE(x,f5(x)). [resolve(217,b,188,a)].
218 -PC(x,y,z) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(149,a,146,b)].
Derived: -PC(x,y,z) | -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | TQ(x) | PQ(x) | AQ(x). [resolve(218,c,194,a)].
Derived: -PC(x,y,z) | -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PC(x,u,w). [resolve(218,c,198,a)].
219 -PC(x,y,z) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(149,a,147,b)].
Derived: -PC(x,y,z) | -PT(x) | AB(x) | L_1(x) | TQ(x) | PQ(x) | AQ(x). [resolve(219,c,194,a)].
Derived: -PC(x,y,z) | -PT(x) | AB(x) | L_1(x) | -PC(x,u,w). [resolve(219,c,198,a)].
220 -L_1(x) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(150,a,146,b)].
Derived: -L_1(x) | -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | TQ(x) | PQ(x) | AQ(x). [resolve(220,c,194,a)].
Derived: -L_1(x) | -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -L_1(x). [resolve(220,c,199,a)].
221 -PED(x) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(151,a,146,b)].
Derived: -PED(x) | -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | TQ(x) | PQ(x) | AQ(x). [resolve(221,c,194,a)].
Derived: -PED(x) | -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PED(x). [resolve(221,c,200,a)].
222 -PED(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(151,a,147,b)].
Derived: -PED(x) | -PT(x) | AB(x) | L_1(x) | TQ(x) | PQ(x) | AQ(x). [resolve(222,c,194,a)].
Derived: -PED(x) | -PT(x) | AB(x) | L_1(x) | -PED(x). [resolve(222,c,200,a)].
223 -NPED(x) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(152,a,146,b)].
Derived: -NPED(x) | -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | TQ(x) | PQ(x) | AQ(x). [resolve(223,c,194,a)].
Derived: -NPED(x) | -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -NPED(x). [resolve(223,c,201,a)].
224 -NPED(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(152,a,147,b)].
Derived: -NPED(x) | -PT(x) | AB(x) | L_1(x) | TQ(x) | PQ(x) | AQ(x). [resolve(224,c,194,a)].
Derived: -NPED(x) | -PT(x) | AB(x) | L_1(x) | -NPED(x). [resolve(224,c,201,a)].
225 -AS(x) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(153,a,146,b)].
Derived: -AS(x) | -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | TQ(x) | PQ(x) | AQ(x). [resolve(225,c,194,a)].
Derived: -AS(x) | -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -AS(x). [resolve(225,c,202,a)].
226 -AS(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(153,a,147,b)].
Derived: -AS(x) | -PT(x) | AB(x) | L_1(x) | TQ(x) | PQ(x) | AQ(x). [resolve(226,c,194,a)].
Derived: -AS(x) | -PT(x) | AB(x) | L_1(x) | -AS(x). [resolve(226,c,202,a)].
227 PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(154,e,132,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x). [resolve(227,e,194,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(x,z,u). [resolve(227,e,198,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -L_1(x). [resolve(227,e,199,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(z,x,u). [resolve(227,e,203,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -L_2(x). [resolve(227,e,204,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -EV(x). [resolve(227,e,205,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -STV(x). [resolve(227,e,206,a)].
228 PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | L_2(x). [resolve(154,e,135,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x). [resolve(228,e,194,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | -PC(x,y,z). [resolve(228,e,198,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | -L_1(x). [resolve(228,e,199,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | -PC(y,x,z). [resolve(228,e,203,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | -EV(x). [resolve(228,e,205,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | L_2(x) | -STV(x). [resolve(228,e,206,a)].
229 PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | EV(x) | STV(x). [resolve(154,e,143,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x). [resolve(229,e,194,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | EV(x) | STV(x) | -PC(x,y,z). [resolve(229,e,198,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | EV(x) | STV(x) | -L_1(x). [resolve(229,e,199,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | EV(x) | STV(x) | -PC(y,x,z). [resolve(229,e,203,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | EV(x) | STV(x) | -L_2(x). [resolve(229,e,204,a)].
230 PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -PC(x,y,z). [resolve(154,e,149,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -PC(x,y,z) | TQ(x) | PQ(x) | AQ(x). [resolve(230,e,194,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -PC(x,y,z) | -PC(x,u,w). [resolve(230,e,198,a)].
231 PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -L_1(x). [resolve(154,e,150,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -L_1(x) | TQ(x) | PQ(x) | AQ(x). [resolve(231,e,194,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | AB(x) | -L_1(x) | -L_1(x). [resolve(231,e,199,a)].
Eliminating SUM/3
232 -T(x) | -T(y) | -T(z) | SUM(z,x,y) | T(f13(x,y,z)). [clausify(39)].
233 -PRE(x,y) | -PRE(x,z) | -SUM(u,y,z) | PRE(x,u). [clausify(24)].
234 -T(x) | -T(y) | -T(z) | -SUM(z,x,y) | -T(u) | -O(u,z) | O(u,x) | O(u,y). [clausify(39)].
235 -T(x) | -T(y) | -T(z) | -SUM(z,x,y) | -T(u) | O(u,z) | -O(u,x). [clausify(39)].
236 -T(x) | -T(y) | -T(z) | -SUM(z,x,y) | -T(u) | O(u,z) | -O(u,y). [clausify(39)].
Derived: -T(x) | -T(y) | -T(z) | T(f13(x,y,z)) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(232,d,233,c)].
Derived: -T(x) | -T(y) | -T(z) | T(f13(x,y,z)) | -T(x) | -T(y) | -T(z) | -T(u) | -O(u,z) | O(u,x) | O(u,y). [resolve(232,d,234,d)].
Derived: -T(x) | -T(y) | -T(z) | T(f13(x,y,z)) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,x). [resolve(232,d,235,d)].
Derived: -T(x) | -T(y) | -T(z) | T(f13(x,y,z)) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,y). [resolve(232,d,236,d)].
237 -T(x) | -T(y) | -T(z) | SUM(z,x,y) | O(f13(x,y,z),z) | O(f13(x,y,z),x) | O(f13(x,y,z),y). [clausify(39)].
Derived: -T(x) | -T(y) | -T(z) | O(f13(x,y,z),z) | O(f13(x,y,z),x) | O(f13(x,y,z),y) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(237,d,233,c)].
Derived: -T(x) | -T(y) | -T(z) | O(f13(x,y,z),z) | O(f13(x,y,z),x) | O(f13(x,y,z),y) | -T(x) | -T(y) | -T(z) | -T(u) | -O(u,z) | O(u,x) | O(u,y). [resolve(237,d,234,d)].
Derived: -T(x) | -T(y) | -T(z) | O(f13(x,y,z),z) | O(f13(x,y,z),x) | O(f13(x,y,z),y) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,x). [resolve(237,d,235,d)].
Derived: -T(x) | -T(y) | -T(z) | O(f13(x,y,z),z) | O(f13(x,y,z),x) | O(f13(x,y,z),y) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,y). [resolve(237,d,236,d)].
238 -T(x) | -T(y) | -T(z) | SUM(z,x,y) | -O(f13(x,y,z),z) | -O(f13(x,y,z),x). [clausify(39)].
Derived: -T(x) | -T(y) | -T(z) | -O(f13(x,y,z),z) | -O(f13(x,y,z),x) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(238,d,233,c)].
Derived: -T(x) | -T(y) | -T(z) | -O(f13(x,y,z),z) | -O(f13(x,y,z),x) | -T(x) | -T(y) | -T(z) | -T(u) | -O(u,z) | O(u,x) | O(u,y). [resolve(238,d,234,d)].
Derived: -T(x) | -T(y) | -T(z) | -O(f13(x,y,z),z) | -O(f13(x,y,z),x) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,x). [resolve(238,d,235,d)].
Derived: -T(x) | -T(y) | -T(z) | -O(f13(x,y,z),z) | -O(f13(x,y,z),x) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,y). [resolve(238,d,236,d)].
239 -T(x) | -T(y) | -T(z) | SUM(z,x,y) | -O(f13(x,y,z),z) | -O(f13(x,y,z),y). [clausify(39)].
Derived: -T(x) | -T(y) | -T(z) | -O(f13(x,y,z),z) | -O(f13(x,y,z),y) | -PRE(u,x) | -PRE(u,y) | PRE(u,z). [resolve(239,d,233,c)].
Derived: -T(x) | -T(y) | -T(z) | -O(f13(x,y,z),z) | -O(f13(x,y,z),y) | -T(x) | -T(y) | -T(z) | -T(u) | -O(u,z) | O(u,x) | O(u,y). [resolve(239,d,234,d)].
Derived: -T(x) | -T(y) | -T(z) | -O(f13(x,y,z),z) | -O(f13(x,y,z),y) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,x). [resolve(239,d,235,d)].
Derived: -T(x) | -T(y) | -T(z) | -O(f13(x,y,z),z) | -O(f13(x,y,z),y) | -T(x) | -T(y) | -T(z) | -T(u) | O(u,z) | -O(u,y). [resolve(239,d,236,d)].
Eliminating DJ/2
240 -T(x) | -T(y) | -DJ(x,y) | -O(x,y). [clausify(34)].
241 -T(x) | -T(y) | P(x,y) | DJ(f7(x,y),y). [clausify(31)].
Derived: -T(f7(x,y)) | -T(y) | -O(f7(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(34)].
Eliminating U/2
243 -T(x) | -T(y) | U(x,y) | -P(x,z) | -P(y,z) | -T(z). [clausify(35)].
244 -T(x) | -T(y) | -U(x,y) | P(x,f9(x,y)). [clausify(35)].
245 -T(x) | -T(y) | -U(x,y) | P(y,f9(x,y)). [clausify(35)].
246 -T(x) | -T(y) | -U(x,y) | T(f9(x,y)). [clausify(35)].
Derived: -T(x) | -T(y) | -P(x,z) | -P(y,z) | -T(z) | -T(x) | -T(y) | P(x,f9(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,f9(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(f9(x,y)). [resolve(243,c,246,c)].
247 -T(x) | -T(y) | -U(x,y) | T(f11(x,y)). [clausify(37)].
Derived: -T(x) | -T(y) | T(f11(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,f11(x,y)) | O(z,x) | O(z,y). [clausify(37)].
Derived: -T(x) | -T(y) | -T(z) | -O(z,f11(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,f11(x,y)) | -O(z,x). [clausify(37)].
Derived: -T(x) | -T(y) | -T(z) | O(z,f11(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,f11(x,y)) | -O(z,y). [clausify(37)].
Derived: -T(x) | -T(y) | -T(z) | O(z,f11(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(f10(x)). [clausify(36)].
252 -AtP(x) | T(x). [clausify(36)].
253 -AtP(x) | -T(y) | -P(y,x) | y = x. [clausify(36)].
Derived: -T(x) | T(f10(x)) | -T(y) | -P(y,x) | y = x. [resolve(251,a,253,a)].
254 AtP(x) | -T(x) | P(f10(x),x). [clausify(36)].
Derived: -T(x) | P(f10(x),x) | -T(y) | -P(y,x) | y = x. [resolve(254,a,253,a)].
255 AtP(x) | -T(x) | f10(x) != x. [clausify(36)].
Derived: -T(x) | f10(x) != x | -T(y) | -P(y,x) | y = x. [resolve(255,a,253,a)].
Eliminating AB/1
256 -R(x) | AB(x). [clausify(44)].
257 -AB(x) | PT(x). [clausify(40)].
Derived: -R(x) | PT(x). [resolve(256,b,257,a)].
258 PT(x) | -AB(x). [clausify(58)].
259 -AB(x) | -PC(x,y,z). [resolve(127,a,115,b)].
Derived: -PC(x,y,z) | -R(x). [resolve(259,a,256,b)].
260 -AB(x) | -L_1(x). [resolve(127,a,116,b)].
Derived: -L_1(x) | -R(x). [resolve(260,a,256,b)].
261 -AB(x) | -PED(x). [resolve(127,a,120,b)].
Derived: -PED(x) | -R(x). [resolve(261,a,256,b)].
262 -AB(x) | -NPED(x). [resolve(127,a,121,b)].
Derived: -NPED(x) | -R(x). [resolve(262,a,256,b)].
263 -AB(x) | -AS(x). [resolve(127,a,122,b)].
Derived: -AS(x) | -R(x). [resolve(263,a,256,b)].
264 -AB(x) | -PC(y,x,z). [resolve(142,a,133,b)].
Derived: -PC(x,y,z) | -R(y). [resolve(264,a,256,b)].
265 -AB(x) | -L_2(x). [resolve(142,a,134,b)].
Derived: -L_2(x) | -R(x). [resolve(265,a,256,b)].
266 -AB(x) | -EV(x). [resolve(142,a,138,b)].
Derived: -EV(x) | -R(x). [resolve(266,a,256,b)].
267 -AB(x) | -STV(x). [resolve(142,a,139,b)].
Derived: -STV(x) | -R(x). [resolve(267,a,256,b)].
268 -AB(x) | -TQ(x). [resolve(193,a,187,b)].
Derived: -TQ(x) | -R(x). [resolve(268,a,256,b)].
269 -AB(x) | -PQ(x). [resolve(193,a,190,b)].
Derived: -PQ(x) | -R(x). [resolve(269,a,256,b)].
270 -AB(x) | -AQ(x). [resolve(193,a,191,b)].
Derived: -AQ(x) | -R(x). [resolve(270,a,256,b)].
271 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)). [resolve(207,b,188,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -PC(x,z,u). [resolve(271,b,259,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -L_1(x). [resolve(271,b,260,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -PED(x). [resolve(271,b,261,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -NPED(x). [resolve(271,b,262,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -AS(x). [resolve(271,b,263,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -PC(z,x,u). [resolve(271,b,264,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -L_2(x). [resolve(271,b,265,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -EV(x). [resolve(271,b,266,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -STV(x). [resolve(271,b,267,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -TQ(x). [resolve(271,b,268,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -PQ(x). [resolve(271,b,269,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -AQ(x). [resolve(271,b,270,a)].
272 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x). [resolve(207,b,194,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -PC(x,z,u). [resolve(272,b,259,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -L_1(x). [resolve(272,b,260,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -PED(x). [resolve(272,b,261,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -NPED(x). [resolve(272,b,262,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -AS(x). [resolve(272,b,263,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -PC(z,x,u). [resolve(272,b,264,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -L_2(x). [resolve(272,b,265,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -EV(x). [resolve(272,b,266,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -STV(x). [resolve(272,b,267,a)].
273 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(x,z,u). [resolve(207,b,198,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(x,z,u) | -PC(x,w,v5). [resolve(273,b,259,a)].
274 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -L_1(x). [resolve(207,b,199,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -L_1(x) | -L_1(x). [resolve(274,b,260,a)].
275 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -PED(x). [resolve(207,b,200,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -PED(x) | -PED(x). [resolve(275,b,261,a)].
276 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -NPED(x). [resolve(207,b,201,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -NPED(x) | -NPED(x). [resolve(276,b,262,a)].
277 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -AS(x). [resolve(207,b,202,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -AS(x) | -AS(x). [resolve(277,b,263,a)].
278 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(z,x,u). [resolve(207,b,203,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(z,x,u) | -PC(w,x,v5). [resolve(278,b,264,a)].
279 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -L_2(x). [resolve(207,b,204,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -L_2(x) | -L_2(x). [resolve(279,b,265,a)].
280 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -EV(x). [resolve(207,b,205,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -EV(x) | -EV(x). [resolve(280,b,266,a)].
281 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -STV(x). [resolve(207,b,206,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | -STV(x) | -STV(x). [resolve(281,b,267,a)].
282 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | PRE(x,f5(x)). [resolve(208,b,188,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | PRE(x,f5(x)) | -PC(x,y,z). [resolve(282,b,259,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | PRE(x,f5(x)) | -L_1(x). [resolve(282,b,260,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | PRE(x,f5(x)) | -PED(x). [resolve(282,b,261,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | PRE(x,f5(x)) | -NPED(x). [resolve(282,b,262,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | PRE(x,f5(x)) | -AS(x). [resolve(282,b,263,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | PRE(x,f5(x)) | -PC(y,x,z). [resolve(282,b,264,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | PRE(x,f5(x)) | -EV(x). [resolve(282,b,266,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | PRE(x,f5(x)) | -STV(x). [resolve(282,b,267,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | PRE(x,f5(x)) | -TQ(x). [resolve(282,b,268,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | PRE(x,f5(x)) | -PQ(x). [resolve(282,b,269,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | PRE(x,f5(x)) | -AQ(x). [resolve(282,b,270,a)].
283 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | TQ(x) | PQ(x) | AQ(x). [resolve(208,b,194,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -PC(x,y,z). [resolve(283,b,259,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -L_1(x). [resolve(283,b,260,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -PED(x). [resolve(283,b,261,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -NPED(x). [resolve(283,b,262,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -AS(x). [resolve(283,b,263,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -PC(y,x,z). [resolve(283,b,264,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -EV(x). [resolve(283,b,266,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -STV(x). [resolve(283,b,267,a)].
284 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -PC(x,y,z). [resolve(208,b,198,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | -PC(x,y,z) | -PC(x,u,w). [resolve(284,b,259,a)].
285 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -L_1(x). [resolve(208,b,199,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | -L_1(x) | -L_1(x). [resolve(285,b,260,a)].
286 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -PED(x). [resolve(208,b,200,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | -PED(x) | -PED(x). [resolve(286,b,261,a)].
287 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -NPED(x). [resolve(208,b,201,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | -NPED(x) | -NPED(x). [resolve(287,b,262,a)].
288 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -AS(x). [resolve(208,b,202,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | -AS(x) | -AS(x). [resolve(288,b,263,a)].
289 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -PC(y,x,z). [resolve(208,b,203,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | -PC(y,x,z) | -PC(u,x,w). [resolve(289,b,264,a)].
290 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -EV(x). [resolve(208,b,205,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | -EV(x) | -EV(x). [resolve(290,b,266,a)].
291 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x) | -STV(x). [resolve(208,b,206,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | L_2(x) | -STV(x) | -STV(x). [resolve(291,b,267,a)].
292 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)). [resolve(209,b,188,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -PC(x,y,z). [resolve(292,b,259,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -L_1(x). [resolve(292,b,260,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -PED(x). [resolve(292,b,261,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -NPED(x). [resolve(292,b,262,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -AS(x). [resolve(292,b,263,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -PC(y,x,z). [resolve(292,b,264,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -L_2(x). [resolve(292,b,265,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -EV(x). [resolve(292,b,266,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -STV(x). [resolve(292,b,267,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -TQ(x). [resolve(292,b,268,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -PQ(x). [resolve(292,b,269,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -AQ(x). [resolve(292,b,270,a)].
293 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x). [resolve(210,b,194,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -PC(x,y,z). [resolve(293,b,259,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -L_1(x). [resolve(293,b,260,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -PED(x). [resolve(293,b,261,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -NPED(x). [resolve(293,b,262,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -AS(x). [resolve(293,b,263,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -PC(y,x,z). [resolve(293,b,264,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -L_2(x). [resolve(293,b,265,a)].
294 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -PC(x,y,z). [resolve(210,b,198,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -PC(x,y,z) | -PC(x,u,w). [resolve(294,b,259,a)].
295 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -L_1(x). [resolve(210,b,199,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -L_1(x) | -L_1(x). [resolve(295,b,260,a)].
296 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -PED(x). [resolve(210,b,200,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -PED(x) | -PED(x). [resolve(296,b,261,a)].
297 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -NPED(x). [resolve(210,b,201,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -NPED(x) | -NPED(x). [resolve(297,b,262,a)].
298 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -AS(x). [resolve(210,b,202,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -AS(x) | -AS(x). [resolve(298,b,263,a)].
299 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -PC(y,x,z). [resolve(210,b,203,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -PC(y,x,z) | -PC(u,x,w). [resolve(299,b,264,a)].
300 -PT(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -L_2(x). [resolve(210,b,204,a)].
Derived: -PT(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x) | -L_2(x) | -L_2(x). [resolve(300,b,265,a)].
301 -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)). [resolve(211,b,188,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -PC(x,z,u). [resolve(301,b,259,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -PED(x). [resolve(301,b,261,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -NPED(x). [resolve(301,b,262,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -AS(x). [resolve(301,b,263,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -PC(z,x,u). [resolve(301,b,264,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -L_2(x). [resolve(301,b,265,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -EV(x). [resolve(301,b,266,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -STV(x). [resolve(301,b,267,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -TQ(x). [resolve(301,b,268,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -PQ(x). [resolve(301,b,269,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -AQ(x). [resolve(301,b,270,a)].
302 -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x). [resolve(211,b,194,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -PC(x,z,u). [resolve(302,b,259,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -PED(x). [resolve(302,b,261,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -NPED(x). [resolve(302,b,262,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -AS(x). [resolve(302,b,263,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -PC(z,x,u). [resolve(302,b,264,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -L_2(x). [resolve(302,b,265,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -EV(x). [resolve(302,b,266,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | TQ(x) | PQ(x) | AQ(x) | -STV(x). [resolve(302,b,267,a)].
303 -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(x,z,u). [resolve(211,b,198,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(x,z,u) | -PC(x,w,v5). [resolve(303,b,259,a)].
304 -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -PED(x). [resolve(211,b,200,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -PED(x) | -PED(x). [resolve(304,b,261,a)].
305 -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -NPED(x). [resolve(211,b,201,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -NPED(x) | -NPED(x). [resolve(305,b,262,a)].
306 -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -AS(x). [resolve(211,b,202,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -AS(x) | -AS(x). [resolve(306,b,263,a)].
307 -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(z,x,u). [resolve(211,b,203,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -PC(z,x,u) | -PC(w,x,v5). [resolve(307,b,264,a)].
308 -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -L_2(x). [resolve(211,b,204,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -L_2(x) | -L_2(x). [resolve(308,b,265,a)].
309 -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -EV(x). [resolve(211,b,205,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -EV(x) | -EV(x). [resolve(309,b,266,a)].
310 -PT(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -STV(x). [resolve(211,b,206,a)].
Derived: -PT(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -STV(x) | -STV(x). [resolve(310,b,267,a)].
311 -PT(x) | AB(x) | L_1(x) | L_2(x) | PRE(x,f5(x)). [resolve(212,b,188,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | PRE(x,f5(x)) | -PC(x,y,z). [resolve(311,b,259,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | PRE(x,f5(x)) | -PED(x). [resolve(311,b,261,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | PRE(x,f5(x)) | -NPED(x). [resolve(311,b,262,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | PRE(x,f5(x)) | -AS(x). [resolve(311,b,263,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | PRE(x,f5(x)) | -PC(y,x,z). [resolve(311,b,264,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | PRE(x,f5(x)) | -EV(x). [resolve(311,b,266,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | PRE(x,f5(x)) | -STV(x). [resolve(311,b,267,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | PRE(x,f5(x)) | -TQ(x). [resolve(311,b,268,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | PRE(x,f5(x)) | -PQ(x). [resolve(311,b,269,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | PRE(x,f5(x)) | -AQ(x). [resolve(311,b,270,a)].
312 -PT(x) | AB(x) | L_1(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x). [resolve(212,b,194,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -PC(x,y,z). [resolve(312,b,259,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -PED(x). [resolve(312,b,261,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -NPED(x). [resolve(312,b,262,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -AS(x). [resolve(312,b,263,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -PC(y,x,z). [resolve(312,b,264,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -EV(x). [resolve(312,b,266,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | TQ(x) | PQ(x) | AQ(x) | -STV(x). [resolve(312,b,267,a)].
313 -PT(x) | AB(x) | L_1(x) | L_2(x) | -PC(x,y,z). [resolve(212,b,198,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | -PC(x,y,z) | -PC(x,u,w). [resolve(313,b,259,a)].
314 -PT(x) | AB(x) | L_1(x) | L_2(x) | -PED(x). [resolve(212,b,200,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | -PED(x) | -PED(x). [resolve(314,b,261,a)].
315 -PT(x) | AB(x) | L_1(x) | L_2(x) | -NPED(x). [resolve(212,b,201,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | -NPED(x) | -NPED(x). [resolve(315,b,262,a)].
316 -PT(x) | AB(x) | L_1(x) | L_2(x) | -AS(x). [resolve(212,b,202,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | -AS(x) | -AS(x). [resolve(316,b,263,a)].
317 -PT(x) | AB(x) | L_1(x) | L_2(x) | -PC(y,x,z). [resolve(212,b,203,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | -PC(y,x,z) | -PC(u,x,w). [resolve(317,b,264,a)].
318 -PT(x) | AB(x) | L_1(x) | L_2(x) | -EV(x). [resolve(212,b,205,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | -EV(x) | -EV(x). [resolve(318,b,266,a)].
319 -PT(x) | AB(x) | L_1(x) | L_2(x) | -STV(x). [resolve(212,b,206,a)].
Derived: -PT(x) | L_1(x) | L_2(x) | -STV(x) | -STV(x). [resolve(319,b,267,a)].
320 -PT(x) | AB(x) | L_1(x) | PRE(x,f5(x)) | PRE(x,f5(x)). [resolve(213,b,188,a)].
Derived: -PT(x) | L_1(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | -PC(x,y,z). [resolve(320,b,259,a)].
Derived: -PT(x) | L_1(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | -PED(x). [resolve(320,b,261,a)].
Derived: -PT(x) | L_1(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | -NPED(x). [resolve(320,b,262,a)].
Derived: -PT(x) | L_1(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | -AS(x). [resolve(320,b,263,a)].
Derived: -PT(x) | L_1(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | -PC(y,x,z). [resolve(320,b,264,a)].
Derived: -PT(x) | L_1(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | -L_2(x). [resolve(320,b,265,a)].
Derived: -PT(x) | L_1(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | -EV(x). [resolve(320,b,266,a)].
Derived: -PT(x) | L_1(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | -STV(x). [resolve(320,b,267,a)].
Derived: -PT(x) | L_1(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | -TQ(x). [resolve(320,b,268,a)].
Derived: -PT(x) | L_1(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | -PQ(x). [resolve(320,b,269,a)].
Derived: -PT(x) | L_1(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | -AQ(x). [resolve(320,b,270,a)].
321 -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x). [resolve(214,b,194,a)].
Derived: -PT(x) | L_1(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -PC(x,y,z). [resolve(321,b,259,a)].
Derived: -PT(x) | L_1(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -PED(x). [resolve(321,b,261,a)].
Derived: -PT(x) | L_1(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -NPED(x). [resolve(321,b,262,a)].
Derived: -PT(x) | L_1(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -AS(x). [resolve(321,b,263,a)].
Derived: -PT(x) | L_1(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -PC(y,x,z). [resolve(321,b,264,a)].
Derived: -PT(x) | L_1(x) | EV(x) | STV(x) | TQ(x) | PQ(x) | AQ(x) | -L_2(x). [resolve(321,b,265,a)].
322 -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -PC(x,y,z). [resolve(214,b,198,a)].
Derived: -PT(x) | L_1(x) | EV(x) | STV(x) | -PC(x,y,z) | -PC(x,u,w). [resolve(322,b,259,a)].
323 -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -PED(x). [resolve(214,b,200,a)].
Derived: -PT(x) | L_1(x) | EV(x) | STV(x) | -PED(x) | -PED(x). [resolve(323,b,261,a)].
324 -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -NPED(x). [resolve(214,b,201,a)].
Derived: -PT(x) | L_1(x) | EV(x) | STV(x) | -NPED(x) | -NPED(x). [resolve(324,b,262,a)].
325 -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -AS(x). [resolve(214,b,202,a)].
Derived: -PT(x) | L_1(x) | EV(x) | STV(x) | -AS(x) | -AS(x). [resolve(325,b,263,a)].
326 -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -PC(y,x,z). [resolve(214,b,203,a)].
Derived: -PT(x) | L_1(x) | EV(x) | STV(x) | -PC(y,x,z) | -PC(u,x,w). [resolve(326,b,264,a)].
327 -PT(x) | AB(x) | L_1(x) | EV(x) | STV(x) | -L_2(x). [resolve(214,b,204,a)].
Derived: -PT(x) | L_1(x) | EV(x) | STV(x) | -L_2(x) | -L_2(x). [resolve(327,b,265,a)].
328 -PT(x) | AB(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)). [resolve(215,b,188,a)].
Derived: -PT(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -PC(x,z,u). [resolve(328,b,259,a)].
Derived: -PT(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -L_1(x). [resolve(328,b,260,a)].
Derived: -PT(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -PED(x). [resolve(328,b,261,a)].
Derived: -PT(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -NPED(x). [resolve(328,b,262,a)].
Derived: -PT(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -AS(x). [resolve(328,b,263,a)].
Derived: -PT(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -PC(z,x,u). [resolve(328,b,264,a)].
Derived: -PT(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -L_2(x). [resolve(328,b,265,a)].
Derived: -PT(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -EV(x). [resolve(328,b,266,a)].
Derived: -PT(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -STV(x). [resolve(328,b,267,a)].
Derived: -PT(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -TQ(x). [resolve(328,b,268,a)].
Derived: -PT(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -PQ(x). [resolve(328,b,269,a)].
Derived: -PT(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y) | PRE(x,f5(x)) | -AQ(x). [resolve(328,b,270,a)].
329 -PT(x) | AB(x) | PRE(x,f5(x)) | L_2(x) | PRE(x,f5(x)). [resolve(216,b,188,a)].
Derived: -PT(x) | PRE(x,f5(x)) | L_2(x) | PRE(x,f5(x)) | -PC(x,y,z). [resolve(329,b,259,a)].
Derived: -PT(x) | PRE(x,f5(x)) | L_2(x) | PRE(x,f5(x)) | -L_1(x). [resolve(329,b,260,a)].
Derived: -PT(x) | PRE(x,f5(x)) | L_2(x) | PRE(x,f5(x)) | -PED(x). [resolve(329,b,261,a)].
Derived: -PT(x) | PRE(x,f5(x)) | L_2(x) | PRE(x,f5(x)) | -NPED(x). [resolve(329,b,262,a)].
Derived: -PT(x) | PRE(x,f5(x)) | L_2(x) | PRE(x,f5(x)) | -AS(x). [resolve(329,b,263,a)].
Derived: -PT(x) | PRE(x,f5(x)) | L_2(x) | PRE(x,f5(x)) | -PC(y,x,z). [resolve(329,b,264,a)].
Derived: -PT(x) | PRE(x,f5(x)) | L_2(x) | PRE(x,f5(x)) | -EV(x). [resolve(329,b,266,a)].
Derived: -PT(x) | PRE(x,f5(x)) | L_2(x) | PRE(x,f5(x)) | -STV(x). [resolve(329,b,267,a)].
Derived: -PT(x) | PRE(x,f5(x)) | L_2(x) | PRE(x,f5(x)) | -TQ(x). [resolve(329,b,268,a)].
Derived: -PT(x) | PRE(x,f5(x)) | L_2(x) | PRE(x,f5(x)) | -PQ(x). [resolve(329,b,269,a)].
Derived: -PT(x) | PRE(x,f5(x)) | L_2(x) | PRE(x,f5(x)) | -AQ(x). [resolve(329,b,270,a)].
330 -PT(x) | AB(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | PRE(x,f5(x)). [resolve(217,b,188,a)].
Derived: -PT(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -PC(x,y,z). [resolve(330,b,259,a)].
Derived: -PT(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -L_1(x). [resolve(330,b,260,a)].
Derived: -PT(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -PED(x). [resolve(330,b,261,a)].
Derived: -PT(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -NPED(x). [resolve(330,b,262,a)].
Derived: -PT(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -AS(x). [resolve(330,b,263,a)].
Derived: -PT(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -PC(y,x,z). [resolve(330,b,264,a)].
Derived: -PT(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -L_2(x). [resolve(330,b,265,a)].
Derived: -PT(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -EV(x). [resolve(330,b,266,a)].
Derived: -PT(x) | PRE(x,f5(x)) | PRE(x,f5(x)) | PRE(x,f5(x)) | -STV(x). [resolve(330,b,267,a)].