-
Notifications
You must be signed in to change notification settings - Fork 35
/
ex0930_participation1_14.p9.out
1101 lines (1012 loc) · 67.3 KB
/
ex0930_participation1_14.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 15898 was started by cchui on stl-ws4.mie.utoronto.ca,
Mon Sep 30 23:52:00 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_14.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_14.p9
formulas(goals).
(all x all l (point1(x) & line1(l) & in1(x,l) -> part1(x,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 all l (point1(x) & line1(l) & in1(x,l) -> part1(x,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)].
85 point1(c1). [deny(82)].
Derived: T(c1). [resolve(85,a,84,a)].
Eliminating line1/1
86 line1(x) | -PD(x). [clausify(7)].
87 -line1(x) | PD(x). [clausify(7)].
88 line1(c2). [deny(82)].
Derived: PD(c2). [resolve(88,a,87,a)].
Eliminating plane1/1
89 plane1(x) | -ED(x). [clausify(8)].
90 -plane1(x) | ED(x). [clausify(8)].
Eliminating in1/2
91 in1(x,y) | -PRE(x,y) | -T(y) | -ED(x). [clausify(9)].
92 -in1(x,y) | PRE(x,y) | PRE(y,x) | y = x. [clausify(9)].
93 -in1(x,y) | PRE(x,y) | T(x) | y = x. [clausify(9)].
94 -in1(x,y) | PRE(x,y) | ED(y) | PD(y) | Q(y) | y = x. [clausify(9)].
95 -in1(x,y) | T(y) | PRE(y,x) | y = x. [clausify(9)].
96 -in1(x,y) | T(y) | T(x) | y = x. [clausify(9)].
97 -in1(x,y) | T(y) | ED(y) | PD(y) | Q(y). [clausify(9)].
98 -in1(x,y) | ED(x) | PD(x) | Q(x) | PRE(y,x) | y = x. [clausify(9)].
99 -in1(x,y) | ED(x) | PD(x) | Q(x) | T(x) | y = x. [clausify(9)].
100 -in1(x,y) | ED(x) | PD(x) | Q(x) | ED(y) | PD(y) | Q(y) | y = x. [clausify(9)].
101 in1(x,y) | -PRE(x,y) | -T(y) | -PD(x). [clausify(9)].
102 in1(x,y) | -PRE(x,y) | -T(y) | -Q(x). [clausify(9)].
103 in1(x,y) | -PRE(y,x) | -T(x) | -ED(y). [clausify(9)].
104 in1(x,y) | -PRE(y,x) | -T(x) | -PD(y). [clausify(9)].
105 in1(x,y) | -PRE(y,x) | -T(x) | -Q(y). [clausify(9)].
106 in1(x,y) | y != x | -ED(y). [clausify(9)].
107 in1(x,y) | y != x | -PD(y). [clausify(9)].
108 in1(x,y) | y != x | -Q(y). [clausify(9)].
109 in1(x,y) | y != x | -T(y). [clausify(9)].
110 in1(c1,c2). [deny(82)].
Derived: PRE(c1,c2) | PRE(c2,c1) | c2 = c1. [resolve(110,a,92,a)].
Derived: T(c2) | PRE(c2,c1) | c2 = c1. [resolve(110,a,95,a)].
Derived: ED(c1) | PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1. [resolve(110,a,98,a)].
Eliminating ED/1
111 -ED(x) | PC(x,f2(x),f3(x)). [clausify(3)].
112 -PC(x,y,z) | ED(x). [clausify(1)].
Derived: PC(x,f2(x),f3(x)) | -PC(x,y,z). [resolve(111,a,112,b)].
113 -L_1(x) | ED(x). [clausify(12)].
Derived: -L_1(x) | PC(x,f2(x),f3(x)). [resolve(113,b,111,a)].
114 L_1(x) | -ED(x). [clausify(12)].
Derived: L_1(x) | -PC(x,y,z). [resolve(114,b,112,b)].
115 -ED(x) | PRE(x,f5(x)). [clausify(15)].
Derived: PRE(x,f5(x)) | -PC(x,y,z). [resolve(115,a,112,b)].
Derived: PRE(x,f5(x)) | -L_1(x). [resolve(115,a,113,b)].
116 -ED(x) | PT(x). [clausify(34)].
Derived: PT(x) | -PC(x,y,z). [resolve(116,a,112,b)].
Derived: PT(x) | -L_1(x). [resolve(116,a,113,b)].
117 -PED(x) | ED(x). [clausify(35)].
Derived: -PED(x) | PC(x,f2(x),f3(x)). [resolve(117,b,111,a)].
Derived: -PED(x) | L_1(x). [resolve(117,b,114,b)].
Derived: -PED(x) | PRE(x,f5(x)). [resolve(117,b,115,a)].
Derived: -PED(x) | PT(x). [resolve(117,b,116,a)].
118 -NPED(x) | ED(x). [clausify(35)].
Derived: -NPED(x) | PC(x,f2(x),f3(x)). [resolve(118,b,111,a)].
Derived: -NPED(x) | L_1(x). [resolve(118,b,114,b)].
Derived: -NPED(x) | PRE(x,f5(x)). [resolve(118,b,115,a)].
Derived: -NPED(x) | PT(x). [resolve(118,b,116,a)].
119 -AS(x) | ED(x). [clausify(35)].
Derived: -AS(x) | PC(x,f2(x),f3(x)). [resolve(119,b,111,a)].
Derived: -AS(x) | L_1(x). [resolve(119,b,114,b)].
Derived: -AS(x) | PRE(x,f5(x)). [resolve(119,b,115,a)].
Derived: -AS(x) | PT(x). [resolve(119,b,116,a)].
120 -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(120,b,111,a)].
Derived: -PT(x) | PD(x) | Q(x) | AB(x) | L_1(x). [resolve(120,b,114,b)].
Derived: -PT(x) | PD(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(120,b,115,a)].
121 PT(x) | -ED(x). [clausify(52)].
122 -ED(x) | -PD(x). [clausify(53)].
Derived: -PD(x) | -PC(x,y,z). [resolve(122,a,112,b)].
Derived: -PD(x) | -L_1(x). [resolve(122,a,113,b)].
Derived: -PD(x) | -PED(x). [resolve(122,a,117,b)].
Derived: -PD(x) | -NPED(x). [resolve(122,a,118,b)].
Derived: -PD(x) | -AS(x). [resolve(122,a,119,b)].
123 -ED(x) | -Q(x). [clausify(53)].
Derived: -Q(x) | -PC(x,y,z). [resolve(123,a,112,b)].
Derived: -Q(x) | -L_1(x). [resolve(123,a,113,b)].
Derived: -Q(x) | -PED(x). [resolve(123,a,117,b)].
Derived: -Q(x) | -NPED(x). [resolve(123,a,118,b)].
Derived: -Q(x) | -AS(x). [resolve(123,a,119,b)].
124 -ED(x) | -AB(x). [clausify(53)].
Derived: -AB(x) | -PC(x,y,z). [resolve(124,a,112,b)].
Derived: -AB(x) | -L_1(x). [resolve(124,a,113,b)].
Derived: -AB(x) | -PED(x). [resolve(124,a,117,b)].
Derived: -AB(x) | -NPED(x). [resolve(124,a,118,b)].
Derived: -AB(x) | -AS(x). [resolve(124,a,119,b)].
125 -ED(x) | PED(x) | NPED(x) | AS(x). [clausify(56)].
Derived: PED(x) | NPED(x) | AS(x) | -PC(x,y,z). [resolve(125,a,112,b)].
Derived: PED(x) | NPED(x) | AS(x) | -L_1(x). [resolve(125,a,113,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | PD(x) | Q(x) | AB(x). [resolve(125,a,120,b)].
126 ED(x) | -PED(x). [clausify(56)].
127 ED(x) | -NPED(x). [clausify(56)].
128 ED(x) | -AS(x). [clausify(56)].
129 ED(c1) | PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1. [resolve(110,a,98,a)].
Derived: PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(129,a,111,a)].
Derived: PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(129,a,114,b)].
Derived: PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PRE(c1,f5(c1)). [resolve(129,a,115,a)].
Derived: PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PT(c1). [resolve(129,a,116,a)].
Derived: PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | -AB(c1). [resolve(129,a,124,a)].
Derived: PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1). [resolve(129,a,125,a)].
Eliminating PD/1
130 -PD(x) | -PRE(x,y) | PC(f1(x,y),x,y). [clausify(2)].
131 -PC(x,y,z) | PD(y). [clausify(1)].
Derived: -PRE(x,y) | PC(f1(x,y),x,y) | -PC(z,x,u). [resolve(130,a,131,b)].
132 -L_2(x) | PD(x). [clausify(13)].
Derived: -L_2(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(132,b,130,a)].
133 L_2(x) | -PD(x). [clausify(13)].
Derived: L_2(x) | -PC(y,x,z). [resolve(133,b,131,b)].
134 -PD(x) | PRE(x,f5(x)). [clausify(15)].
Derived: PRE(x,f5(x)) | -PC(y,x,z). [resolve(134,a,131,b)].
Derived: PRE(x,f5(x)) | -L_2(x). [resolve(134,a,132,b)].
135 -PD(x) | PT(x). [clausify(34)].
Derived: PT(x) | -PC(y,x,z). [resolve(135,a,131,b)].
Derived: PT(x) | -L_2(x). [resolve(135,a,132,b)].
136 -EV(x) | PD(x). [clausify(36)].
Derived: -EV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(136,b,130,a)].
Derived: -EV(x) | L_2(x). [resolve(136,b,133,b)].
Derived: -EV(x) | PRE(x,f5(x)). [resolve(136,b,134,a)].
Derived: -EV(x) | PT(x). [resolve(136,b,135,a)].
137 -STV(x) | PD(x). [clausify(36)].
Derived: -STV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(137,b,130,a)].
Derived: -STV(x) | L_2(x). [resolve(137,b,133,b)].
Derived: -STV(x) | PRE(x,f5(x)). [resolve(137,b,134,a)].
Derived: -STV(x) | PT(x). [resolve(137,b,135,a)].
138 PT(x) | -PD(x). [clausify(52)].
139 -PD(x) | -Q(x). [clausify(54)].
Derived: -Q(x) | -PC(y,x,z). [resolve(139,a,131,b)].
Derived: -Q(x) | -L_2(x). [resolve(139,a,132,b)].
Derived: -Q(x) | -EV(x). [resolve(139,a,136,b)].
Derived: -Q(x) | -STV(x). [resolve(139,a,137,b)].
140 -PD(x) | -AB(x). [clausify(54)].
Derived: -AB(x) | -PC(y,x,z). [resolve(140,a,131,b)].
Derived: -AB(x) | -L_2(x). [resolve(140,a,132,b)].
Derived: -AB(x) | -EV(x). [resolve(140,a,136,b)].
Derived: -AB(x) | -STV(x). [resolve(140,a,137,b)].
141 -PD(x) | EV(x) | STV(x). [clausify(59)].
Derived: EV(x) | STV(x) | -PC(y,x,z). [resolve(141,a,131,b)].
Derived: EV(x) | STV(x) | -L_2(x). [resolve(141,a,132,b)].
142 PD(x) | -EV(x). [clausify(59)].
143 PD(x) | -STV(x). [clausify(59)].
144 PD(c2). [resolve(88,a,87,a)].
Derived: -PRE(c2,x) | PC(f1(c2,x),c2,x). [resolve(144,a,130,a)].
Derived: L_2(c2). [resolve(144,a,133,b)].
Derived: PRE(c2,f5(c2)). [resolve(144,a,134,a)].
Derived: PT(c2). [resolve(144,a,135,a)].
Derived: -Q(c2). [resolve(144,a,139,a)].
Derived: -AB(c2). [resolve(144,a,140,a)].
Derived: EV(c2) | STV(c2). [resolve(144,a,141,a)].
145 -PT(x) | PD(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(120,b,111,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(145,b,130,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x). [resolve(145,b,133,b)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)). [resolve(145,b,134,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x). [resolve(145,b,141,a)].
146 -PT(x) | PD(x) | Q(x) | AB(x) | L_1(x). [resolve(120,b,114,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(146,b,130,a)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | L_2(x). [resolve(146,b,133,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | PRE(x,f5(x)). [resolve(146,b,134,a)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | EV(x) | STV(x). [resolve(146,b,141,a)].
147 -PT(x) | PD(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(120,b,115,a)].
Derived: -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(147,b,130,a)].
Derived: -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)) | L_2(x). [resolve(147,b,133,b)].
Derived: -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)) | PRE(x,f5(x)). [resolve(147,b,134,a)].
148 -PD(x) | -PC(x,y,z). [resolve(122,a,112,b)].
Derived: -PC(x,y,z) | -PC(u,x,w). [resolve(148,a,131,b)].
Derived: -PC(x,y,z) | -L_2(x). [resolve(148,a,132,b)].
Derived: -PC(x,y,z) | -EV(x). [resolve(148,a,136,b)].
Derived: -PC(x,y,z) | -STV(x). [resolve(148,a,137,b)].
Derived: -PC(c2,x,y). [resolve(148,a,144,a)].
Derived: -PC(x,y,z) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(148,a,145,b)].
Derived: -PC(x,y,z) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(148,a,146,b)].
149 -PD(x) | -L_1(x). [resolve(122,a,113,b)].
Derived: -L_1(x) | -PC(y,x,z). [resolve(149,a,131,b)].
Derived: -L_1(x) | -L_2(x). [resolve(149,a,132,b)].
Derived: -L_1(x) | -EV(x). [resolve(149,a,136,b)].
Derived: -L_1(x) | -STV(x). [resolve(149,a,137,b)].
Derived: -L_1(c2). [resolve(149,a,144,a)].
Derived: -L_1(x) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(149,a,145,b)].
150 -PD(x) | -PED(x). [resolve(122,a,117,b)].
Derived: -PED(x) | -PC(y,x,z). [resolve(150,a,131,b)].
Derived: -PED(x) | -L_2(x). [resolve(150,a,132,b)].
Derived: -PED(x) | -EV(x). [resolve(150,a,136,b)].
Derived: -PED(x) | -STV(x). [resolve(150,a,137,b)].
Derived: -PED(c2). [resolve(150,a,144,a)].
Derived: -PED(x) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(150,a,145,b)].
Derived: -PED(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(150,a,146,b)].
151 -PD(x) | -NPED(x). [resolve(122,a,118,b)].
Derived: -NPED(x) | -PC(y,x,z). [resolve(151,a,131,b)].
Derived: -NPED(x) | -L_2(x). [resolve(151,a,132,b)].
Derived: -NPED(x) | -EV(x). [resolve(151,a,136,b)].
Derived: -NPED(x) | -STV(x). [resolve(151,a,137,b)].
Derived: -NPED(c2). [resolve(151,a,144,a)].
Derived: -NPED(x) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(151,a,145,b)].
Derived: -NPED(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(151,a,146,b)].
152 -PD(x) | -AS(x). [resolve(122,a,119,b)].
Derived: -AS(x) | -PC(y,x,z). [resolve(152,a,131,b)].
Derived: -AS(x) | -L_2(x). [resolve(152,a,132,b)].
Derived: -AS(x) | -EV(x). [resolve(152,a,136,b)].
Derived: -AS(x) | -STV(x). [resolve(152,a,137,b)].
Derived: -AS(c2). [resolve(152,a,144,a)].
Derived: -AS(x) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(152,a,145,b)].
Derived: -AS(x) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(152,a,146,b)].
153 PED(x) | NPED(x) | AS(x) | -PT(x) | PD(x) | Q(x) | AB(x). [resolve(125,a,120,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(153,e,130,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | L_2(x). [resolve(153,e,133,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | EV(x) | STV(x). [resolve(153,e,141,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -PC(x,y,z). [resolve(153,e,148,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -L_1(x). [resolve(153,e,149,a)].
154 PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(129,a,111,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(154,a,130,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | L_2(c1). [resolve(154,a,133,b)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | PRE(c1,f5(c1)). [resolve(154,a,134,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | PT(c1). [resolve(154,a,135,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -AB(c1). [resolve(154,a,140,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | EV(c1) | STV(c1). [resolve(154,a,141,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -PC(c1,x,y). [resolve(154,a,148,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -L_1(c1). [resolve(154,a,149,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -PED(c1). [resolve(154,a,150,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -NPED(c1). [resolve(154,a,151,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -AS(c1). [resolve(154,a,152,a)].
155 PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(129,a,114,b)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(155,a,130,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | L_2(c1). [resolve(155,a,133,b)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | PRE(c1,f5(c1)). [resolve(155,a,134,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | PT(c1). [resolve(155,a,135,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | -AB(c1). [resolve(155,a,140,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | EV(c1) | STV(c1). [resolve(155,a,141,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | -PC(c1,x,y). [resolve(155,a,148,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | -PED(c1). [resolve(155,a,150,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | -NPED(c1). [resolve(155,a,151,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | -AS(c1). [resolve(155,a,152,a)].
156 PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PRE(c1,f5(c1)). [resolve(129,a,115,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PRE(c1,f5(c1)) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(156,a,130,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PRE(c1,f5(c1)) | L_2(c1). [resolve(156,a,133,b)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PRE(c1,f5(c1)) | PRE(c1,f5(c1)). [resolve(156,a,134,a)].
157 PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PT(c1). [resolve(129,a,116,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PT(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(157,a,130,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PT(c1) | L_2(c1). [resolve(157,a,133,b)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PT(c1) | PT(c1). [resolve(157,a,135,a)].
158 PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | -AB(c1). [resolve(129,a,124,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | -AB(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(158,a,130,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | -AB(c1) | L_2(c1). [resolve(158,a,133,b)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | -AB(c1) | -AB(c1). [resolve(158,a,140,a)].
159 PD(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1). [resolve(129,a,125,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(159,a,130,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | L_2(c1). [resolve(159,a,133,b)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | EV(c1) | STV(c1). [resolve(159,a,141,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | -PC(c1,x,y). [resolve(159,a,148,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | -L_1(c1). [resolve(159,a,149,a)].
Eliminating tin1/3
160 tin1(x,y,z) | -PC(x,y,z). [clausify(10)].
161 -tin1(x,y,z) | PC(x,y,z). [clausify(10)].
Eliminating L_3/1
162 L_3(x) | -Q(x). [clausify(14)].
163 -L_3(x) | Q(x). [clausify(14)].
Eliminating SUM/3
164 -T(x) | -T(y) | -T(z) | SUM(z,x,y) | T(f13(x,y,z)). [clausify(33)].
165 -PRE(x,y) | -PRE(x,z) | -SUM(u,y,z) | PRE(x,u). [clausify(18)].
166 -T(x) | -T(y) | -T(z) | -SUM(z,x,y) | -T(u) | -O(u,z) | O(u,x) | O(u,y). [clausify(33)].
167 -T(x) | -T(y) | -T(z) | -SUM(z,x,y) | -T(u) | O(u,z) | -O(u,x). [clausify(33)].
168 -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(164,d,165,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(164,d,166,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(164,d,167,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(164,d,168,d)].
169 -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(169,d,165,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(169,d,166,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(169,d,167,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(169,d,168,d)].
170 -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(170,d,165,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(170,d,166,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(170,d,167,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(170,d,168,d)].
171 -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(171,d,165,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(171,d,166,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(171,d,167,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(171,d,168,d)].
Eliminating DJ/2
172 -T(x) | -T(y) | -DJ(x,y) | -O(x,y). [clausify(28)].
173 -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(172,c,173,d)].
174 -T(x) | -T(y) | DJ(x,y) | O(x,y). [clausify(28)].
Eliminating U/2
175 -T(x) | -T(y) | U(x,y) | -P(x,z) | -P(y,z) | -T(z). [clausify(29)].
176 -T(x) | -T(y) | -U(x,y) | P(x,f9(x,y)). [clausify(29)].
177 -T(x) | -T(y) | -U(x,y) | P(y,f9(x,y)). [clausify(29)].
178 -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(175,c,176,c)].
Derived: -T(x) | -T(y) | -P(x,z) | -P(y,z) | -T(z) | -T(x) | -T(y) | P(y,f9(x,y)). [resolve(175,c,177,c)].
Derived: -T(x) | -T(y) | -P(x,z) | -P(y,z) | -T(z) | -T(x) | -T(y) | T(f9(x,y)). [resolve(175,c,178,c)].
179 -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(179,c,175,c)].
180 -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(180,c,175,c)].
181 -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(181,c,175,c)].
182 -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(182,c,175,c)].
Eliminating AtP/1
183 AtP(x) | -T(x) | T(f10(x)). [clausify(30)].
184 -AtP(x) | T(x). [clausify(30)].
185 -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(183,a,185,a)].
186 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(186,a,185,a)].
187 AtP(x) | -T(x) | f10(x) != x. [clausify(30)].
Derived: -T(x) | f10(x) != x | -T(y) | -P(y,x) | y = x. [resolve(187,a,185,a)].
Eliminating TQ/1
188 -TL(x) | TQ(x). [clausify(43)].
189 -TQ(x) | Q(x). [clausify(37)].
Derived: -TL(x) | Q(x). [resolve(188,b,189,a)].
190 -Q(x) | TQ(x) | PQ(x) | AQ(x). [clausify(61)].
191 Q(x) | -TQ(x). [clausify(61)].
192 -TQ(x) | -PQ(x). [clausify(62)].
Derived: -PQ(x) | -TL(x). [resolve(192,a,188,b)].
193 -TQ(x) | -AQ(x). [clausify(62)].
Derived: -AQ(x) | -TL(x). [resolve(193,a,188,b)].
Eliminating PQ/1
194 -SL(x) | PQ(x). [clausify(44)].
195 -PQ(x) | Q(x). [clausify(37)].
Derived: -SL(x) | Q(x). [resolve(194,b,195,a)].
196 Q(x) | -PQ(x). [clausify(61)].
197 -PQ(x) | -AQ(x). [clausify(63)].
Derived: -AQ(x) | -SL(x). [resolve(197,a,194,b)].
198 -PQ(x) | -TL(x). [resolve(192,a,188,b)].
Derived: -TL(x) | -SL(x). [resolve(198,a,194,b)].
Eliminating AQ/1
Eliminating R/1
199 -TR(x) | R(x). [clausify(45)].
200 -R(x) | AB(x). [clausify(38)].
Derived: -TR(x) | AB(x). [resolve(199,b,200,a)].
201 -PR(x) | R(x). [clausify(45)].
Derived: -PR(x) | AB(x). [resolve(201,b,200,a)].
202 -AR(x) | R(x). [clausify(45)].
Derived: -AR(x) | AB(x). [resolve(202,b,200,a)].
203 -R(x) | TR(x) | PR(x) | AR(x). [clausify(71)].
204 R(x) | -TR(x). [clausify(71)].
205 R(x) | -PR(x). [clausify(71)].
206 R(x) | -AR(x). [clausify(71)].
Eliminating M/1
207 -PED(x) | M(x) | F(x) | POB(x). [clausify(64)].
208 -M(x) | PED(x). [clausify(39)].
209 PED(x) | -M(x). [clausify(64)].
210 -M(x) | -F(x). [clausify(65)].
211 -M(x) | -POB(x). [clausify(65)].
Eliminating F/1
Eliminating POB/1
212 -APO(x) | POB(x). [clausify(46)].
213 -POB(x) | PED(x). [clausify(39)].
Derived: -APO(x) | PED(x). [resolve(212,b,213,a)].
214 -NAPO(x) | POB(x). [clausify(46)].
Derived: -NAPO(x) | PED(x). [resolve(214,b,213,a)].
215 PED(x) | -POB(x). [clausify(64)].
216 -POB(x) | APO(x) | NAPO(x). [clausify(74)].
217 POB(x) | -APO(x). [clausify(74)].
218 POB(x) | -NAPO(x). [clausify(74)].
Eliminating NPOB/1
219 -MOB(x) | NPOB(x). [clausify(47)].
220 -NPOB(x) | NPED(x). [clausify(40)].
Derived: -MOB(x) | NPED(x). [resolve(219,b,220,a)].
221 -SOB(x) | NPOB(x). [clausify(47)].
Derived: -SOB(x) | NPED(x). [resolve(221,b,220,a)].
222 -NPOB(x) | MOB(x) | SOB(x). [clausify(76)].
223 NPOB(x) | -MOB(x). [clausify(76)].
224 NPOB(x) | -SOB(x). [clausify(76)].
Eliminating ACH/1
225 -EV(x) | ACH(x) | ACC(x). [clausify(67)].
226 -ACH(x) | EV(x). [clausify(41)].
227 EV(x) | -ACH(x). [clausify(67)].
228 -ACH(x) | -ACC(x). [clausify(68)].
Eliminating ACC/1
Eliminating ST/1
229 -STV(x) | ST(x) | PRO(x). [clausify(69)].
230 -ST(x) | STV(x). [clausify(42)].
231 STV(x) | -ST(x). [clausify(69)].
232 -ST(x) | -PRO(x). [clausify(70)].
Eliminating PRO/1
Eliminating TR/1
233 -TR(x) | -PR(x). [clausify(72)].
234 -T(x) | TR(x). [clausify(48)].
Derived: -PR(x) | -T(x). [resolve(233,a,234,b)].
235 -TR(x) | -AR(x). [clausify(72)].
Derived: -AR(x) | -T(x). [resolve(235,a,234,b)].
236 -TR(x) | AB(x). [resolve(199,b,200,a)].
Derived: AB(x) | -T(x). [resolve(236,a,234,b)].
Eliminating S/1
Eliminating ASO/1
237 -SAG(x) | ASO(x). [clausify(51)].
238 -ASO(x) | SOB(x). [clausify(50)].
Derived: -SAG(x) | SOB(x). [resolve(237,b,238,a)].
239 -SC(x) | ASO(x). [clausify(51)].
Derived: -SC(x) | SOB(x). [resolve(239,b,238,a)].
240 -SOB(x) | ASO(x) | NASO(x). [clausify(78)].
241 SOB(x) | -ASO(x). [clausify(78)].
242 -ASO(x) | -NASO(x). [clausify(79)].
Derived: -NASO(x) | -SAG(x). [resolve(242,a,237,b)].
Derived: -NASO(x) | -SC(x). [resolve(242,a,239,b)].
243 -ASO(x) | SAG(x) | SC(x). [clausify(80)].
Derived: SAG(x) | SC(x) | -SOB(x) | NASO(x). [resolve(243,a,240,b)].
244 ASO(x) | -SAG(x). [clausify(80)].
245 ASO(x) | -SC(x). [clausify(80)].
Eliminating NASO/1
246 SAG(x) | SC(x) | -SOB(x) | NASO(x). [resolve(243,a,240,b)].
247 -NASO(x) | SOB(x). [clausify(50)].
248 SOB(x) | -NASO(x). [clausify(78)].
249 -NASO(x) | -SAG(x). [resolve(242,a,237,b)].
250 -NASO(x) | -SC(x). [resolve(242,a,239,b)].
Eliminating EV/1
251 EV(x) | STV(x) | -PC(y,x,z). [resolve(141,a,131,b)].
252 -EV(x) | -STV(x). [clausify(60)].
253 -EV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(136,b,130,a)].
254 -EV(x) | L_2(x). [resolve(136,b,133,b)].
255 -EV(x) | PRE(x,f5(x)). [resolve(136,b,134,a)].
256 -EV(x) | PT(x). [resolve(136,b,135,a)].
257 -Q(x) | -EV(x). [resolve(139,a,136,b)].
258 -AB(x) | -EV(x). [resolve(140,a,136,b)].
Derived: STV(x) | -PC(y,x,z) | -PRE(x,u) | PC(f1(x,u),x,u). [resolve(251,a,253,a)].
Derived: STV(x) | -PC(y,x,z) | L_2(x). [resolve(251,a,254,a)].
Derived: STV(x) | -PC(y,x,z) | PRE(x,f5(x)). [resolve(251,a,255,a)].
Derived: STV(x) | -PC(y,x,z) | PT(x). [resolve(251,a,256,a)].
Derived: STV(x) | -PC(y,x,z) | -Q(x). [resolve(251,a,257,b)].
Derived: STV(x) | -PC(y,x,z) | -AB(x). [resolve(251,a,258,b)].
259 EV(x) | STV(x) | -L_2(x). [resolve(141,a,132,b)].
Derived: STV(x) | -L_2(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(259,a,253,a)].
Derived: STV(x) | -L_2(x) | PRE(x,f5(x)). [resolve(259,a,255,a)].
Derived: STV(x) | -L_2(x) | PT(x). [resolve(259,a,256,a)].
Derived: STV(x) | -L_2(x) | -Q(x). [resolve(259,a,257,b)].
Derived: STV(x) | -L_2(x) | -AB(x). [resolve(259,a,258,b)].
260 EV(c2) | STV(c2). [resolve(144,a,141,a)].
Derived: STV(c2) | -PRE(c2,x) | PC(f1(c2,x),c2,x). [resolve(260,a,253,a)].
Derived: STV(c2) | L_2(c2). [resolve(260,a,254,a)].
Derived: STV(c2) | PRE(c2,f5(c2)). [resolve(260,a,255,a)].
Derived: STV(c2) | PT(c2). [resolve(260,a,256,a)].
Derived: STV(c2) | -Q(c2). [resolve(260,a,257,b)].
Derived: STV(c2) | -AB(c2). [resolve(260,a,258,b)].
261 -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | EV(x) | STV(x). [resolve(145,b,141,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(261,e,253,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | L_2(x). [resolve(261,e,254,a)].
262 -PT(x) | Q(x) | AB(x) | L_1(x) | EV(x) | STV(x). [resolve(146,b,141,a)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | STV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(262,e,253,a)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | STV(x) | L_2(x). [resolve(262,e,254,a)].
263 -PC(x,y,z) | -EV(x). [resolve(148,a,136,b)].
Derived: -PC(x,y,z) | STV(x) | -PC(u,x,w). [resolve(263,b,251,a)].
Derived: -PC(x,y,z) | STV(x) | -L_2(x). [resolve(263,b,259,a)].
264 -L_1(x) | -EV(x). [resolve(149,a,136,b)].
Derived: -L_1(x) | STV(x) | -PC(y,x,z). [resolve(264,b,251,a)].
Derived: -L_1(x) | STV(x) | -L_2(x). [resolve(264,b,259,a)].
265 -PED(x) | -EV(x). [resolve(150,a,136,b)].
Derived: -PED(x) | STV(x) | -PC(y,x,z). [resolve(265,b,251,a)].
Derived: -PED(x) | STV(x) | -L_2(x). [resolve(265,b,259,a)].
266 -NPED(x) | -EV(x). [resolve(151,a,136,b)].
Derived: -NPED(x) | STV(x) | -PC(y,x,z). [resolve(266,b,251,a)].
Derived: -NPED(x) | STV(x) | -L_2(x). [resolve(266,b,259,a)].
267 -AS(x) | -EV(x). [resolve(152,a,136,b)].
Derived: -AS(x) | STV(x) | -PC(y,x,z). [resolve(267,b,251,a)].
Derived: -AS(x) | STV(x) | -L_2(x). [resolve(267,b,259,a)].
268 PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | EV(x) | STV(x). [resolve(153,e,141,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | STV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(268,g,253,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | STV(x) | L_2(x). [resolve(268,g,254,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | STV(x) | PRE(x,f5(x)). [resolve(268,g,255,a)].
269 Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | EV(c1) | STV(c1). [resolve(154,a,141,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | STV(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(269,e,253,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | STV(c1) | L_2(c1). [resolve(269,e,254,a)].
270 Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | EV(c1) | STV(c1). [resolve(155,a,141,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | STV(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(270,e,253,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | STV(c1) | L_2(c1). [resolve(270,e,254,a)].
271 Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | EV(c1) | STV(c1). [resolve(159,a,141,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | STV(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(271,g,253,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | STV(c1) | L_2(c1). [resolve(271,g,254,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | STV(c1) | PRE(c1,f5(c1)). [resolve(271,g,255,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | STV(c1) | PT(c1). [resolve(271,g,256,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | STV(c1) | -AB(c1). [resolve(271,g,258,b)].
Eliminating PR/1
Eliminating APO/1
Eliminating MOB/1
Eliminating SAG/1
Eliminating L_2/1
272 L_2(x) | -PC(y,x,z). [resolve(133,b,131,b)].
273 -L_2(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(132,b,130,a)].
Derived: -PC(x,y,z) | -PRE(y,u) | PC(f1(y,u),y,u). [resolve(272,a,273,a)].
274 PRE(x,f5(x)) | -L_2(x). [resolve(134,a,132,b)].
Derived: PRE(x,f5(x)) | -PC(y,x,z). [resolve(274,b,272,a)].
275 PT(x) | -L_2(x). [resolve(135,a,132,b)].
Derived: PT(x) | -PC(y,x,z). [resolve(275,b,272,a)].
276 -STV(x) | L_2(x). [resolve(137,b,133,b)].
Derived: -STV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(276,b,273,a)].
277 -Q(x) | -L_2(x). [resolve(139,a,132,b)].
Derived: -Q(x) | -PC(y,x,z). [resolve(277,b,272,a)].
278 -AB(x) | -L_2(x). [resolve(140,a,132,b)].
Derived: -AB(x) | -PC(y,x,z). [resolve(278,b,272,a)].
279 L_2(c2). [resolve(144,a,133,b)].
Derived: -PRE(c2,x) | PC(f1(c2,x),c2,x). [resolve(279,a,273,a)].
280 -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | L_2(x). [resolve(145,b,133,b)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(280,e,273,a)].
281 -PT(x) | Q(x) | AB(x) | L_1(x) | L_2(x). [resolve(146,b,133,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(281,e,273,a)].
282 -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)) | L_2(x). [resolve(147,b,133,b)].
283 -PC(x,y,z) | -L_2(x). [resolve(148,a,132,b)].
Derived: -PC(x,y,z) | -PC(u,x,w). [resolve(283,b,272,a)].
Derived: -PC(x,y,z) | -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(283,b,282,e)].
284 -L_1(x) | -L_2(x). [resolve(149,a,132,b)].
Derived: -L_1(x) | -PC(y,x,z). [resolve(284,b,272,a)].
Derived: -L_1(x) | -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(284,b,282,e)].
285 -PED(x) | -L_2(x). [resolve(150,a,132,b)].
Derived: -PED(x) | -PC(y,x,z). [resolve(285,b,272,a)].
Derived: -PED(x) | -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(285,b,282,e)].
286 -NPED(x) | -L_2(x). [resolve(151,a,132,b)].
Derived: -NPED(x) | -PC(y,x,z). [resolve(286,b,272,a)].
Derived: -NPED(x) | -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(286,b,282,e)].
287 -AS(x) | -L_2(x). [resolve(152,a,132,b)].
Derived: -AS(x) | -PC(y,x,z). [resolve(287,b,272,a)].
Derived: -AS(x) | -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(287,b,282,e)].
288 PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | L_2(x). [resolve(153,e,133,b)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(288,g,273,a)].
Derived: PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(288,g,274,b)].
289 Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | L_2(c1). [resolve(154,a,133,b)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(289,e,273,a)].
290 Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | L_2(c1). [resolve(155,a,133,b)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(290,e,273,a)].
291 Q(c1) | PRE(c2,c1) | c2 = c1 | PRE(c1,f5(c1)) | L_2(c1). [resolve(156,a,133,b)].
292 Q(c1) | PRE(c2,c1) | c2 = c1 | PT(c1) | L_2(c1). [resolve(157,a,133,b)].
293 Q(c1) | PRE(c2,c1) | c2 = c1 | -AB(c1) | L_2(c1). [resolve(158,a,133,b)].
294 Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | L_2(c1). [resolve(159,a,133,b)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(294,g,273,a)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | PRE(c1,f5(c1)). [resolve(294,g,274,b)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | PT(c1). [resolve(294,g,275,b)].
Derived: Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | -AB(c1). [resolve(294,g,278,b)].
295 STV(x) | -PC(y,x,z) | L_2(x). [resolve(251,a,254,a)].
296 STV(x) | -L_2(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(259,a,253,a)].
Derived: STV(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(296,b,282,e)].
Derived: STV(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x) | Q(c1) | PRE(c2,c1) | c2 = c1 | PRE(c1,f5(c1)). [resolve(296,b,291,e)].
Derived: STV(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x) | Q(c1) | PRE(c2,c1) | c2 = c1 | PT(c1). [resolve(296,b,292,e)].
Derived: STV(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x) | Q(c1) | PRE(c2,c1) | c2 = c1 | -AB(c1). [resolve(296,b,293,e)].
297 STV(x) | -L_2(x) | PRE(x,f5(x)). [resolve(259,a,255,a)].
Derived: STV(x) | PRE(x,f5(x)) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(297,b,280,e)].
Derived: STV(x) | PRE(x,f5(x)) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(297,b,281,e)].
Derived: STV(x) | PRE(x,f5(x)) | -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(297,b,282,e)].
Derived: STV(c1) | PRE(c1,f5(c1)) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(297,b,289,e)].
Derived: STV(c1) | PRE(c1,f5(c1)) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(297,b,290,e)].
Derived: STV(c1) | PRE(c1,f5(c1)) | Q(c1) | PRE(c2,c1) | c2 = c1 | PRE(c1,f5(c1)). [resolve(297,b,291,e)].
298 STV(x) | -L_2(x) | PT(x). [resolve(259,a,256,a)].
Derived: STV(c1) | PT(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(298,b,289,e)].
Derived: STV(c1) | PT(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(298,b,290,e)].
Derived: STV(c1) | PT(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PT(c1). [resolve(298,b,292,e)].
299 STV(x) | -L_2(x) | -Q(x). [resolve(259,a,257,b)].
300 STV(x) | -L_2(x) | -AB(x). [resolve(259,a,258,b)].
Derived: STV(c1) | -AB(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(300,b,289,e)].
Derived: STV(c1) | -AB(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(300,b,290,e)].
Derived: STV(c1) | -AB(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | -AB(c1). [resolve(300,b,293,e)].
301 STV(c2) | L_2(c2). [resolve(260,a,254,a)].
Derived: STV(c2) | -PC(c2,x,y). [resolve(301,b,283,b)].
Derived: STV(c2) | -L_1(c2). [resolve(301,b,284,b)].
Derived: STV(c2) | -PED(c2). [resolve(301,b,285,b)].
Derived: STV(c2) | -NPED(c2). [resolve(301,b,286,b)].
Derived: STV(c2) | -AS(c2). [resolve(301,b,287,b)].
302 -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | L_2(x). [resolve(261,e,254,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | -PC(x,y,z). [resolve(302,f,283,b)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | -L_1(x). [resolve(302,f,284,b)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | -PED(x). [resolve(302,f,285,b)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | -NPED(x). [resolve(302,f,286,b)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | -AS(x). [resolve(302,f,287,b)].
303 -PT(x) | Q(x) | AB(x) | L_1(x) | STV(x) | L_2(x). [resolve(262,e,254,a)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | STV(x) | -PC(x,y,z). [resolve(303,f,283,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | STV(x) | -PED(x). [resolve(303,f,285,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | STV(x) | -NPED(x). [resolve(303,f,286,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | STV(x) | -AS(x). [resolve(303,f,287,b)].
304 -PC(x,y,z) | STV(x) | -L_2(x). [resolve(263,b,259,a)].
Derived: -PC(x,y,z) | STV(x) | PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x). [resolve(304,c,288,g)].
Derived: -PC(c1,x,y) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(304,c,289,e)].
Derived: -PC(c1,x,y) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(304,c,290,e)].
Derived: -PC(c1,x,y) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1). [resolve(304,c,294,g)].
305 -L_1(x) | STV(x) | -L_2(x). [resolve(264,b,259,a)].
Derived: -L_1(x) | STV(x) | PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x). [resolve(305,c,288,g)].
Derived: -L_1(c1) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(305,c,289,e)].
Derived: -L_1(c1) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1). [resolve(305,c,294,g)].
306 -PED(x) | STV(x) | -L_2(x). [resolve(265,b,259,a)].
Derived: -PED(c1) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(306,c,289,e)].
Derived: -PED(c1) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(306,c,290,e)].
307 -NPED(x) | STV(x) | -L_2(x). [resolve(266,b,259,a)].
Derived: -NPED(c1) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(307,c,289,e)].
Derived: -NPED(c1) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(307,c,290,e)].
308 -AS(x) | STV(x) | -L_2(x). [resolve(267,b,259,a)].
Derived: -AS(c1) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(308,c,289,e)].
Derived: -AS(c1) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(308,c,290,e)].
309 PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | STV(x) | L_2(x). [resolve(268,g,254,a)].
310 Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | STV(c1) | L_2(c1). [resolve(269,e,254,a)].
311 Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | STV(c1) | L_2(c1). [resolve(270,e,254,a)].
312 Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | STV(c1) | L_2(c1). [resolve(271,g,254,a)].
Eliminating STV/1
313 STV(x) | -PC(y,x,z) | -PRE(x,u) | PC(f1(x,u),x,u). [resolve(251,a,253,a)].
314 -STV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(137,b,130,a)].
315 -STV(x) | PRE(x,f5(x)). [resolve(137,b,134,a)].
316 -STV(x) | PT(x). [resolve(137,b,135,a)].
317 -Q(x) | -STV(x). [resolve(139,a,137,b)].
318 -AB(x) | -STV(x). [resolve(140,a,137,b)].
319 -PC(x,y,z) | -STV(x). [resolve(148,a,137,b)].
320 -L_1(x) | -STV(x). [resolve(149,a,137,b)].
321 -PED(x) | -STV(x). [resolve(150,a,137,b)].
322 -NPED(x) | -STV(x). [resolve(151,a,137,b)].
323 -AS(x) | -STV(x). [resolve(152,a,137,b)].
324 STV(x) | -PC(y,x,z) | PRE(x,f5(x)). [resolve(251,a,255,a)].
325 STV(x) | -PC(y,x,z) | PT(x). [resolve(251,a,256,a)].
326 STV(x) | -PC(y,x,z) | -Q(x). [resolve(251,a,257,b)].
327 STV(x) | -PC(y,x,z) | -AB(x). [resolve(251,a,258,b)].
328 STV(c2) | -PRE(c2,x) | PC(f1(c2,x),c2,x). [resolve(260,a,253,a)].
329 STV(c2) | PRE(c2,f5(c2)). [resolve(260,a,255,a)].
Derived: PRE(c2,f5(c2)) | PRE(c2,f5(c2)). [resolve(329,a,315,a)].
330 STV(c2) | PT(c2). [resolve(260,a,256,a)].
Derived: PT(c2) | PT(c2). [resolve(330,a,316,a)].
331 STV(c2) | -Q(c2). [resolve(260,a,257,b)].
Derived: -Q(c2) | -Q(c2). [resolve(331,a,317,b)].
332 STV(c2) | -AB(c2). [resolve(260,a,258,b)].
Derived: -AB(c2) | -AB(c2). [resolve(332,a,318,b)].
333 -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(261,e,253,a)].
334 -PT(x) | Q(x) | AB(x) | L_1(x) | STV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(262,e,253,a)].
335 -PC(x,y,z) | STV(x) | -PC(u,x,w). [resolve(263,b,251,a)].
336 -L_1(x) | STV(x) | -PC(y,x,z). [resolve(264,b,251,a)].
337 -PED(x) | STV(x) | -PC(y,x,z). [resolve(265,b,251,a)].
338 -NPED(x) | STV(x) | -PC(y,x,z). [resolve(266,b,251,a)].
339 -AS(x) | STV(x) | -PC(y,x,z). [resolve(267,b,251,a)].
340 PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | STV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(268,g,253,a)].
341 PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | STV(x) | PRE(x,f5(x)). [resolve(268,g,255,a)].
342 Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | STV(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(269,e,253,a)].
343 Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | STV(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(270,e,253,a)].
344 Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | STV(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(271,g,253,a)].
345 Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | STV(c1) | PRE(c1,f5(c1)). [resolve(271,g,255,a)].
346 Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | STV(c1) | PT(c1). [resolve(271,g,256,a)].
347 Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | STV(c1) | -AB(c1). [resolve(271,g,258,b)].
348 -STV(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(276,b,273,a)].
Derived: -PRE(x,y) | PC(f1(x,y),x,y) | -PC(z,x,u) | -PRE(x,w) | PC(f1(x,w),x,w). [resolve(348,a,313,a)].
349 STV(x) | -PRE(x,y) | PC(f1(x,y),x,y) | -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(296,b,282,e)].
Derived: -PRE(x,y) | PC(f1(x,y),x,y) | -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)) | -PRE(x,z) | PC(f1(x,z),x,z). [resolve(349,a,314,a)].
350 STV(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x) | Q(c1) | PRE(c2,c1) | c2 = c1 | PRE(c1,f5(c1)). [resolve(296,b,291,e)].
Derived: -PRE(c1,x) | PC(f1(c1,x),c1,x) | Q(c1) | PRE(c2,c1) | c2 = c1 | PRE(c1,f5(c1)) | -PRE(c1,y) | PC(f1(c1,y),c1,y). [resolve(350,a,314,a)].
351 STV(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x) | Q(c1) | PRE(c2,c1) | c2 = c1 | PT(c1). [resolve(296,b,292,e)].
Derived: -PRE(c1,x) | PC(f1(c1,x),c1,x) | Q(c1) | PRE(c2,c1) | c2 = c1 | PT(c1) | -PRE(c1,y) | PC(f1(c1,y),c1,y). [resolve(351,a,314,a)].
352 STV(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x) | Q(c1) | PRE(c2,c1) | c2 = c1 | -AB(c1). [resolve(296,b,293,e)].
Derived: -PRE(c1,x) | PC(f1(c1,x),c1,x) | Q(c1) | PRE(c2,c1) | c2 = c1 | -AB(c1) | -PRE(c1,y) | PC(f1(c1,y),c1,y). [resolve(352,a,314,a)].
353 STV(x) | PRE(x,f5(x)) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)). [resolve(297,b,280,e)].
Derived: PRE(x,f5(x)) | -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | PRE(x,f5(x)). [resolve(353,a,315,a)].
354 STV(x) | PRE(x,f5(x)) | -PT(x) | Q(x) | AB(x) | L_1(x). [resolve(297,b,281,e)].
Derived: PRE(x,f5(x)) | -PT(x) | Q(x) | AB(x) | L_1(x) | PRE(x,f5(x)). [resolve(354,a,315,a)].
355 STV(x) | PRE(x,f5(x)) | -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)). [resolve(297,b,282,e)].
Derived: PRE(x,f5(x)) | -PT(x) | Q(x) | AB(x) | PRE(x,f5(x)) | PRE(x,f5(x)). [resolve(355,a,315,a)].
356 STV(c1) | PRE(c1,f5(c1)) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(297,b,289,e)].
Derived: PRE(c1,f5(c1)) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | PRE(c1,f5(c1)). [resolve(356,a,315,a)].
357 STV(c1) | PRE(c1,f5(c1)) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(297,b,290,e)].
Derived: PRE(c1,f5(c1)) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | PRE(c1,f5(c1)). [resolve(357,a,315,a)].
358 STV(c1) | PRE(c1,f5(c1)) | Q(c1) | PRE(c2,c1) | c2 = c1 | PRE(c1,f5(c1)). [resolve(297,b,291,e)].
Derived: PRE(c1,f5(c1)) | Q(c1) | PRE(c2,c1) | c2 = c1 | PRE(c1,f5(c1)) | PRE(c1,f5(c1)). [resolve(358,a,315,a)].
359 STV(c1) | PT(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(298,b,289,e)].
Derived: PT(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | PT(c1). [resolve(359,a,316,a)].
360 STV(c1) | PT(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(298,b,290,e)].
Derived: PT(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | PT(c1). [resolve(360,a,316,a)].
361 STV(c1) | PT(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PT(c1). [resolve(298,b,292,e)].
Derived: PT(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PT(c1) | PT(c1). [resolve(361,a,316,a)].
362 STV(c1) | -AB(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(300,b,289,e)].
Derived: -AB(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -AB(c1). [resolve(362,a,318,b)].
363 STV(c1) | -AB(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(300,b,290,e)].
Derived: -AB(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | -AB(c1). [resolve(363,a,318,b)].
364 STV(c1) | -AB(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | -AB(c1). [resolve(300,b,293,e)].
Derived: -AB(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | -AB(c1) | -AB(c1). [resolve(364,a,318,b)].
365 STV(c2) | -PC(c2,x,y). [resolve(301,b,283,b)].
Derived: -PC(c2,x,y) | -PRE(c2,z) | PC(f1(c2,z),c2,z). [resolve(365,a,314,a)].
Derived: -PC(c2,x,y) | -PC(c2,z,u). [resolve(365,a,319,b)].
366 STV(c2) | -L_1(c2). [resolve(301,b,284,b)].
Derived: -L_1(c2) | -PRE(c2,x) | PC(f1(c2,x),c2,x). [resolve(366,a,314,a)].
Derived: -L_1(c2) | -L_1(c2). [resolve(366,a,320,b)].
367 STV(c2) | -PED(c2). [resolve(301,b,285,b)].
Derived: -PED(c2) | -PRE(c2,x) | PC(f1(c2,x),c2,x). [resolve(367,a,314,a)].
Derived: -PED(c2) | -PED(c2). [resolve(367,a,321,b)].
368 STV(c2) | -NPED(c2). [resolve(301,b,286,b)].
Derived: -NPED(c2) | -PRE(c2,x) | PC(f1(c2,x),c2,x). [resolve(368,a,314,a)].
Derived: -NPED(c2) | -NPED(c2). [resolve(368,a,322,b)].
369 STV(c2) | -AS(c2). [resolve(301,b,287,b)].
Derived: -AS(c2) | -PRE(c2,x) | PC(f1(c2,x),c2,x). [resolve(369,a,314,a)].
Derived: -AS(c2) | -AS(c2). [resolve(369,a,323,b)].
370 -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | -PC(x,y,z). [resolve(302,f,283,b)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -PC(x,y,z) | -PRE(x,u) | PC(f1(x,u),x,u). [resolve(370,e,314,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -PC(x,y,z) | -PC(x,u,w). [resolve(370,e,319,b)].
371 -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | -L_1(x). [resolve(302,f,284,b)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -L_1(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(371,e,314,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -L_1(x) | -L_1(x). [resolve(371,e,320,b)].
372 -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | -PED(x). [resolve(302,f,285,b)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -PED(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(372,e,314,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -PED(x) | -PED(x). [resolve(372,e,321,b)].
373 -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | -NPED(x). [resolve(302,f,286,b)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -NPED(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(373,e,314,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -NPED(x) | -NPED(x). [resolve(373,e,322,b)].
374 -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | STV(x) | -AS(x). [resolve(302,f,287,b)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -AS(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(374,e,314,a)].
Derived: -PT(x) | Q(x) | AB(x) | PC(x,f2(x),f3(x)) | -AS(x) | -AS(x). [resolve(374,e,323,b)].
375 -PT(x) | Q(x) | AB(x) | L_1(x) | STV(x) | -PC(x,y,z). [resolve(303,f,283,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | -PC(x,y,z) | -PRE(x,u) | PC(f1(x,u),x,u). [resolve(375,e,314,a)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | -PC(x,y,z) | -PC(x,u,w). [resolve(375,e,319,b)].
376 -PT(x) | Q(x) | AB(x) | L_1(x) | STV(x) | -PED(x). [resolve(303,f,285,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | -PED(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(376,e,314,a)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | -PED(x) | -PED(x). [resolve(376,e,321,b)].
377 -PT(x) | Q(x) | AB(x) | L_1(x) | STV(x) | -NPED(x). [resolve(303,f,286,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | -NPED(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(377,e,314,a)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | -NPED(x) | -NPED(x). [resolve(377,e,322,b)].
378 -PT(x) | Q(x) | AB(x) | L_1(x) | STV(x) | -AS(x). [resolve(303,f,287,b)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | -AS(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(378,e,314,a)].
Derived: -PT(x) | Q(x) | AB(x) | L_1(x) | -AS(x) | -AS(x). [resolve(378,e,323,b)].
379 -PC(x,y,z) | STV(x) | PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x). [resolve(304,c,288,g)].
Derived: -PC(x,y,z) | PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -PRE(x,u) | PC(f1(x,u),x,u). [resolve(379,b,314,a)].
Derived: -PC(x,y,z) | PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -PC(x,u,w). [resolve(379,b,319,b)].
380 -PC(c1,x,y) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(304,c,289,e)].
Derived: -PC(c1,x,y) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -PRE(c1,z) | PC(f1(c1,z),c1,z). [resolve(380,b,314,a)].
Derived: -PC(c1,x,y) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -PC(c1,z,u). [resolve(380,b,319,b)].
381 -PC(c1,x,y) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(304,c,290,e)].
Derived: -PC(c1,x,y) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | -PRE(c1,z) | PC(f1(c1,z),c1,z). [resolve(381,b,314,a)].
Derived: -PC(c1,x,y) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | -PC(c1,z,u). [resolve(381,b,319,b)].
382 -PC(c1,x,y) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1). [resolve(304,c,294,g)].
Derived: -PC(c1,x,y) | Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | -PRE(c1,z) | PC(f1(c1,z),c1,z). [resolve(382,b,314,a)].
Derived: -PC(c1,x,y) | Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | -PC(c1,z,u). [resolve(382,b,319,b)].
383 -L_1(x) | STV(x) | PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x). [resolve(305,c,288,g)].
Derived: -L_1(x) | PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -PRE(x,y) | PC(f1(x,y),x,y). [resolve(383,b,314,a)].
Derived: -L_1(x) | PED(x) | NPED(x) | AS(x) | -PT(x) | Q(x) | AB(x) | -L_1(x). [resolve(383,b,320,b)].
384 -L_1(c1) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(305,c,289,e)].
Derived: -L_1(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(384,b,314,a)].
Derived: -L_1(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -L_1(c1). [resolve(384,b,320,b)].
385 -L_1(c1) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1). [resolve(305,c,294,g)].
Derived: -L_1(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(385,b,314,a)].
Derived: -L_1(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PED(c1) | NPED(c1) | AS(c1) | -L_1(c1). [resolve(385,b,320,b)].
386 -PED(c1) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)). [resolve(306,c,289,e)].
Derived: -PED(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(386,b,314,a)].
Derived: -PED(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | PC(c1,f2(c1),f3(c1)) | -PED(c1). [resolve(386,b,321,b)].
387 -PED(c1) | STV(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1). [resolve(306,c,290,e)].
Derived: -PED(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | -PRE(c1,x) | PC(f1(c1,x),c1,x). [resolve(387,b,314,a)].
Derived: -PED(c1) | Q(c1) | PRE(c2,c1) | c2 = c1 | L_1(c1) | -PED(c1). [resolve(387,b,321,b)].