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