----- Prover9 July-2005E-work, 18 July 2005 -----
Process 31031 was started by mccune on theorem.mcs.anl.gov,
Tue Aug  9 14:15:34 2005
The command was "prover9 -f andrews-0.in".

% Reading from file andrews-0.in

set(auto).
    % set(auto) -> set(auto1).
    % set(auto1) -> set(auto_inference).
    % set(auto1) -> set(fof_reduction).
    % set(auto1) -> set(predicate_elimination).
    % set(auto1) -> set(unfold_eq).
    % set(unfold_eq) -> assign(unfold_eq_limit, 2147483647).
    % set(unfold_eq) -> clear(fold_eq).
    % set(auto1) -> set(inverse_order).
    % set(auto1) -> assign(new_constants, 1).
    % assign(new_constants, 1) -> clear(x_proofs).
    % assign(new_constants, 1) -> clear(rx_proofs).
    % set(auto1) -> assign(lex_dep_demod_lim, 11).
    % set(auto1) -> set(lex_dep_demod_sane).
    % set(auto1) -> assign(max_weight, 100).
    % set(auto1) -> assign(age_part, 1).
    % set(auto1) -> assign(weight_part, 2).
    % set(auto1) -> assign(weight_neg_part, 2).
    % set(auto1) -> assign(sos_limit, 10000).
    % set(auto1) -> clear(x_proofs).
    % set(auto1) -> assign(stats, lots).
    % set(auto1) -> assign(max_megs, 200).
    % set(auto1) -> clear(clocks).
clear(fof_reduction).

formulas(sos).
- (((exists x all y (p(x) <-> p(y))) <-> ((exists u (q(u))) <-> (all v (p(v))))) <-> ((exists w all z (q(z) <-> q(w))) <-> ((exists x1 (p(x1))) <-> (all x2 (q(x2)))))).
end_of_list.

% Finished reading the input.

% Entering prover search function.
% Assigned IDs to 128 clauses.

% Predicate elimination: (none).
% Relation symbol precedence:  lex([ p, q ]).
% Function symbol precedence:  lex([ $c11, $c16, $c3, $c8, $c1, $c10, $c12, $c13, $c14, $c17, $c18, $c19, $c2, $c4, $c5, $c6, $c7, $c9, $c15, $c20, $f1, $f2, $f3, $f4 ]).
% After inverse_order: % Function symbol precedence:  lex([ $c11, $c16, $c3, $c8, $c1, $c10, $c12, $c13, $c14, $c17, $c18, $c19, $c2, $c4, $c5, $c6, $c7, $c9, $c15, $c20, $f1, $f2, $f3, $f4 ]).
% Unfolding symbols: (none).

% Auto inference settings:
  % set(binary_resolution).  % (non-Horn)

% Reasonable options, based on the structure of the clauses:
  % set(factor), because non-Horn
  % set(back_unit_deletion), because non-Horn
    % set(back_unit_deletion) -> set(unit_deletion).

% Clauses after input processing:

clauses(usable).
end_of_list.

clauses(sos).
474 p(x) | p($f3(x)) | q($c14) | q($f4(y)) | q(y) | - p(z) | - q($c20).  [factor (222 a d)]
478 p(x) | p($f3(x)) | q($c14) | - q($f4(y)) | - q(y) | - p(z) | - q($c20).  [factor (224 a d)]
491 p(x) | p($f3(x)) | - q(y) | - p($c15) | q($f4(z)) | q(z) | p($c19).  [factor (229 e h)]
495 p(x) | p($f3(x)) | - q($f4(y)) | - p($c15) | - q(y) | p($c19) | q(z).  [factor (231 c e)]
509 - p(x) | - p($f3(x)) | q($c14) | p(y) | q($f4(z)) | q(z) | - q($c20).  [factor (238 a g)]
513 - p(x) | - p($f3(x)) | q($c14) | p(y) | - q($f4(z)) | - q(z) | - q($c20).  [factor (240 a g)]
528 - p(x) | - p($f3(x)) | - q(y) | - p($c15) | q($f4(z)) | q(z) | p($c19).  [factor (245 e h)]
533 - p(x) | - p($f3(x)) | - q($f4(y)) | - p($c15) | - q(y) | p($c19) | q(z).  [factor (247 c e)]
537 p(x) | p($f1(x)) | - q(y) | q($f2(z)) | q(z) | - p(u).  [factor (249 d g)]
539 p(x) | p($f1(x)) | - q($c7) | q($f2(y)) | q(y) | p($c6).  [factor (251 c g)]
540 p(x) | p($f1(x)) | - q($f2(y)) | - q(y) | - p(z) | q(u).  [factor (253 c d)]
542 p(x) | p($f1(x)) | - q($f2(y)) | - q(y) | p($c6) | - q($c7).  [factor (255 c d)]
554 p(x) | p($f1(x)) | - q($c8) | q(y) | - p(z) | - q($c10).  [factor (265 c e)]
557 p(x) | p($f1(x)) | q($c1) | - p($c2) | q($f2(y)) | q(y).  [factor (268 d g)]
562 - p(x) | - p($f1(x)) | - q(y) | p(z) | q($f2(u)) | q(u).  [factor (280 e g)]
563 - p(x) | - p($f1(x)) | - q($f2(y)) | p(z) | - q(y) | q(u).  [factor (284 c e)]
564 - p(x) | - p($f1(x)) | - q($f2(y)) | p($c6) | - q(y) | - q($c7).  [factor (286 d f)]
574 - p(x) | - p($f1(x)) | - q($c8) | p(y) | q(z) | - q($c10).  [factor (296 c f)]
579 - p(x) | - p($f1(x)) | q($c1) | - p($c2) | q($f2(y)) | q(y).  [factor (299 c g)]
583 - p(x) | - p($f1(x)) | q($c1) | - p($c2) | - q($f2(y)) | - q(y).  [factor (303 c g)]
586 - p(x) | - p($f1(x)) | q($c1) | - p($c2) | - q($c10) | q($c8).  [factor (308 e g)]
590 - p(x) | - p($f1(x)) | q($c1) | - p($c2) | - q($c8) | - q($c10).  [factor (313 c e)]
614 - p($c3) | p(x) | - q(y) | - p($c5) | q($f2(z)) | q(z).  [factor (336 e g)]
615 - p($c3) | p(x) | - q($f2(y)) | - p($c5) | - q(y) | q(z).  [factor (340 c e)]
616 - p($c3) | p($c6) | - q($f2(x)) | - p($c5) | - q(x) | - q($c7).  [factor (342 c e)]
626 - p($c3) | p(x) | - q($c8) | - p($c5) | q(y) | - q($c10).  [factor (352 c f)]
637 p($c3) | - p(x) | q($c4) | - q(y) | q($c8) | p($c9).  [factor (365 c g)]
651 p($c3) | - p($c5) | - q($f2(x)) | - q(x) | p($c6) | - q($c7).  [factor (381 c d)]
692 - p($c11) | p($c19) | q($c12) | - p($c13) | q($f4(x)) | q(x).  [factor (419 c g)]
709 p($c11) | - p(x) | - q(y) | q($f4(z)) | q(z) | p($c19).  [factor (440 d g)]
713 p($c11) | - p(x) | - q($f4(y)) | - q(y) | p($c19) | q(z).  [factor (445 c d)]
722 p($c11) | - p($c13) | q($c12) | q($f4(x)) | q(x) | p($c19).  [factor (454 c g)]
727 p(x) | p($f3(x)) | q($c14) | - q(y) | q($c16) | - p(z).  [factor (463 c g)]
729 p(x) | p($f3(x)) | q($c14) | - q($c18) | q($c16) | p($c17).  [factor (465 d g)]
733 p(x) | p($f3(x)) | q($c14) | - q($c16) | p($c17) | - q($c18).  [factor (469 c d)]
736 p(x) | p($f3(x)) | q($c14) | q($f4(y)) | q(y) | p($c19).  [factor (471 c g)]
738 p(x) | p($f3(x)) | q($c14) | q($f4($c14)) | - p(y) | - q($c20).  [factor (474 c e)]
740 p(x) | p($f3(x)) | q($c14) | - q($f4(y)) | - q(y) | p($c19).  [factor (476 c g)]
741 p(x) | p($f3(x)) | q($c14) | - q($f4($c20)) | - q($c20) | - p(y).  [factor (478 e g)]
749 p($c19) | p($f3($c19)) | - q(x) | - p($c15) | q($f4(y)) | q(y).  [factor (490 e g)]
750 p(x) | p($f3(x)) | - q($c20) | - p($c15) | q($f4(y)) | q(y).  [factor (492 d g)]
751 p($c19) | p($f3($c19)) | - q($f4(x)) | - p($c15) | - q(x) | q(y).  [factor (494 c e)]
752 p(x) | p($f3(x)) | - q($f4(y)) | - p($c15) | - q(y) | - q($c20).  [factor (496 d f)]
754 - p(x) | - p($f3(x)) | q($c14) | p(y) | - q(z) | q($c16).  [factor (498 c g)]
760 - p(x) | - p($f3(x)) | q($c14) | p($c19) | q($f4(y)) | q(y).  [factor (507 d g)]
761 - p(x) | - p($f3(x)) | q($c14) | p(y) | q($f4($c14)) | - q($c20).  [factor (509 c f)]
762 - p(x) | - p($f3(x)) | q($c14) | p($c19) | - q($f4(y)) | - q(y).  [factor (511 d g)]
763 - p(x) | - p($f3(x)) | q($c14) | p(y) | - q($f4($c20)) | - q($c20).  [factor (513 f g)]
779 - p($c15) | - p($f3($c15)) | - q(x) | q($f4(y)) | q(y) | p($c19).  [factor (527 d g)]
782 - p(x) | - p($f3(x)) | - q($c20) | - p($c15) | q($f4(y)) | q(y).  [factor (530 c g)]
783 - p($c15) | - p($f3($c15)) | - q($f4(x)) | - q(x) | p($c19) | q(y).  [factor (532 c d)]
786 - p(x) | - p($f3(x)) | - q($f4(y)) | - p($c15) | - q(y) | - q($c20).  [factor (535 c e)]
788 p($c6) | p($f1($c6)) | - q($c7) | q($f2(x)) | q(x).  [factor (538 c f)]
789 p($c6) | p($f1($c6)) | - q($f2(x)) | - q(x) | - q($c7).  [factor (541 c d)]
790 p(x) | p($f1(x)) | - q($f2($c7)) | - q($c7) | p($c6).  [factor (542 d f)]
793 p(x) | p($f1(x)) | - q(y) | q($c8) | p($c9).  [factor (545 d f)]
794 p(x) | p($f1(x)) | - q($c10) | q($c8) | - p(y).  [factor (548 c f)]
797 p(x) | p($f1(x)) | - q($c8) | q(y) | p($c9).  [factor (551 d f)]
798 p(x) | p($f1(x)) | q($c1) | - p($c2) | q($f2($c1)).  [factor (555 d f)]
800 - p(x) | - p($f1(x)) | - q($f2($c7)) | p($c6) | - q($c7).  [factor (564 e f)]
801 - p(x) | - p($f1(x)) | - q(y) | p($c9) | q($c8).  [factor (566 e f)]
802 - p(x) | - p($f1(x)) | - q($c10) | p(y) | q($c8).  [factor (569 c f)]
803 - p(x) | - p($f1(x)) | - q($c8) | p($c9) | q(y).  [factor (571 e f)]
805 - p($c2) | - p($f1($c2)) | q($c1) | q($f2(x)) | q(x).  [factor (575 c f)]
807 - p(x) | - p($f1(x)) | q($c1) | - p($c2) | q($f2($c1)).  [factor (578 c f)]
808 - p($c2) | - p($f1($c2)) | q($c1) | - q($f2(x)) | - q(x).  [factor (581 c f)]
809 - p($c2) | - p($f1($c2)) | q($c1) | - q($c10) | q($c8).  [factor (584 d f)]
810 - p($c2) | - p($f1($c2)) | q($c1) | - q($c8) | - q($c10).  [factor (588 c d)]
812 - p($c3) | p(x) | q($c4) | q($f2(y)) | q(y).  [factor (591 c f)]
816 - p($c3) | p(x) | q($c4) | - q($f2(y)) | - q(y).  [factor (599 c f)]
817 - p($c3) | p($c9) | q($c4) | - q(x) | q($c8).  [factor (603 c f)]
818 - p($c3) | p(x) | q($c4) | - q($c10) | q($c8).  [factor (605 d f)]
821 - p($c3) | p(x) | q($c4) | - q($c8) | - q($c10).  [factor (611 c d)]
822 - p($c3) | p($c6) | - q($f2($c7)) | - p($c5) | - q($c7).  [factor (616 e f)]
823 - p($c3) | p($c9) | - q(x) | - p($c5) | q($c8).  [factor (618 e f)]
824 - p($c3) | p(x) | - q($c10) | - p($c5) | q($c8).  [factor (621 c f)]
825 - p($c3) | p($c9) | - q($c8) | - p($c5) | q(x).  [factor (623 e f)]
827 p($c3) | - p(x) | q($c4) | q($f2(y)) | q(y).  [factor (627 c f)]
830 p($c3) | - p(x) | q($c4) | - q($f2(y)) | - q(y).  [factor (634 c f)]
831 p($c3) | - p(x) | q($c4) | - q($c10) | q($c8).  [factor (638 d f)]
832 p($c3) | - p(x) | q($c4) | - q($c8) | p($c9).  [factor (641 c f)]
833 p($c3) | - p(x) | q($c4) | - q($c8) | - q($c10).  [factor (643 c d)]
834 p($c3) | - p($c5) | - q(x) | q($f2(y)) | q(y).  [factor (646 d f)]
835 p($c3) | - p($c5) | - q($f2(x)) | - q(x) | q(y).  [factor (649 c d)]
836 p($c3) | - p($c5) | - q($f2($c7)) | - q($c7) | p($c6).  [factor (651 d f)]
837 p($c3) | - p($c5) | - q(x) | q($c8) | p($c9).  [factor (653 d f)]
840 p($c3) | - p($c5) | - q($c8) | q(x) | p($c9).  [factor (659 d f)]
841 p($c3) | - p($c5) | - q($c8) | q(x) | - q($c10).  [factor (662 c e)]
850 - p($c11) | p($c19) | - q(x) | q($f4(y)) | q(y).  [factor (679 d f)]
851 - p($c11) | p(x) | - q($c20) | q($f4(y)) | q(y).  [factor (681 c f)]
852 - p($c11) | p($c19) | - q($f4(x)) | - q(x) | q(y).  [factor (684 c d)]
853 - p($c11) | p(x) | - q($f4(y)) | - q(y) | - q($c20).  [factor (686 c d)]
856 - p($c11) | p($c19) | q($c12) | - p($c13) | q($f4($c12)).  [factor (691 c f)]
865 p($c11) | - p(x) | - q($c20) | q($f4(y)) | q(y).  [factor (710 c f)]
866 p($c11) | - p(x) | - q($f4(y)) | - q(y) | - q($c20).  [factor (714 c d)]
869 p($c11) | - p($c13) | q($c12) | q($f4($c12)) | p($c19).  [factor (721 c f)]
871 p($c17) | p($f3($c17)) | q($c14) | - q($c18) | q($c16).  [factor (728 d f)]
872 p(x) | p($f3(x)) | q($c14) | - q($c16) | - p(y).  [factor (730 c f)]
873 p($c17) | p($f3($c17)) | q($c14) | - q($c16) | - q($c18).  [factor (732 c d)]
875 p($c19) | p($f3($c19)) | q($c14) | q($f4(x)) | q(x).  [factor (734 c f)]
876 p(x) | p($f3(x)) | q($c14) | q($f4($c14)) | p($c19).  [factor (735 c f)]
877 p($c19) | p($f3($c19)) | q($c14) | - q($f4(x)) | - q(x).  [factor (739 c f)]
878 p(x) | p($f3(x)) | - q(y) | - p($c15) | q($c16).  [factor (742 e f)]
879 p(x) | p($f3(x)) | - q($c16) | - p($c15) | q(y).  [factor (746 e f)]
880 p(x) | p($f3(x)) | - q($f4($c20)) | - p($c15) | - q($c20).  [factor (752 e f)]
881 - p(x) | - p($f3(x)) | q($c14) | p(y) | - q($c16).  [factor (755 c f)]
882 - p(x) | - p($f3(x)) | q($c14) | p($c19) | q($f4($c14)).  [factor (758 d f)]
886 - p(x) | - p($f3(x)) | - q(y) | - p($c15) | q($c16).  [factor (767 e f)]
891 - p(x) | - p($f3(x)) | - q($c16) | - p($c15) | q(y).  [factor (775 e f)]
892 - p($c15) | - p($f3($c15)) | - q($c20) | q($f4(x)) | q(x).  [factor (780 c f)]
893 - p($c15) | - p($f3($c15)) | - q($f4(x)) | - q(x) | - q($c20).  [factor (784 c d)]
895 - p(x) | - p($f3(x)) | - q($f4($c20)) | - p($c15) | - q($c20).  [factor (786 e f)]
896 p($c6) | p($f1($c6)) | - q($f2($c7)) | - q($c7).  [factor (789 d e)]
897 p($c9) | p($f1($c9)) | - q(x) | q($c8).  [factor (791 d e)]
898 p($c9) | p($f1($c9)) | - q($c8) | q(x).  [factor (795 d e)]
899 - p($c2) | - p($f1($c2)) | q($c1) | q($f2($c1)).  [factor (804 c e)]
900 - p($c3) | p(x) | q($c4) | q($f2($c4)).  [factor (811 c e)]
901 - p($c3) | p($c9) | q($c4) | - q($c8).  [factor (819 c e)]
902 p($c3) | - p(x) | q($c4) | q($f2($c4)).  [factor (826 c e)]
903 p($c3) | - p($c5) | - q($c10) | q($c8).  [factor (838 c e)]
904 - p($c11) | p(x) | - q(y) | q($c16).  [factor (842 d e)]
905 - p($c11) | p(x) | - q($c16) | q(y).  [factor (846 d e)]
906 - p($c11) | p(x) | - q($f4($c20)) | - q($c20).  [factor (853 d e)]
907 p($c11) | - p(x) | - q(y) | q($c16).  [factor (857 d e)]
908 p($c11) | - p(x) | - q($c16) | q(y).  [factor (861 d e)]
909 p($c11) | - p(x) | - q($f4($c20)) | - q($c20).  [factor (866 d e)]
910 p($c19) | p($f3($c19)) | q($c14) | q($f4($c14)).  [factor (874 c e)]
911 - p($c15) | - p($f3($c15)) | - q(x) | q($c16).  [factor (883 d e)]
912 - p($c15) | - p($f3($c15)) | - q($c16) | q(x).  [factor (888 d e)]
913 - p($c15) | - p($f3($c15)) | - q($f4($c20)) | - q($c20).  [factor (893 d e)]
end_of_list.

clauses(demodulators).
end_of_list.

clauses(goals).
end_of_list.

% Starting search at 0.07 seconds.

given #1 (wt=16): 474 p(x) | p($f3(x)) | q($c14) | q($f4(y)) | q(y) | - p(z) | - q($c20).  [factor (222 a d)]

given #2 (wt=16): 478 p(x) | p($f3(x)) | q($c14) | - q($f4(y)) | - q(y) | - p(z) | - q($c20).  [factor (224 a d)]

given #3 (wt=16): 491 p(x) | p($f3(x)) | - q(y) | - p($c15) | q($f4(z)) | q(z) | p($c19).  [factor (229 e h)]

given #4 (wt=16): 495 p(x) | p($f3(x)) | - q($f4(y)) | - p($c15) | - q(y) | p($c19) | q(z).  [factor (231 c e)]

given #5 (wt=16): 509 - p(x) | - p($f3(x)) | q($c14) | p(y) | q($f4(z)) | q(z) | - q($c20).  [factor (238 a g)]

given #6 (wt=16): 513 - p(x) | - p($f3(x)) | q($c14) | p(y) | - q($f4(z)) | - q(z) | - q($c20).  [factor (240 a g)]

given #7 (wt=16): 528 - p(x) | - p($f3(x)) | - q(y) | - p($c15) | q($f4(z)) | q(z) | p($c19).  [factor (245 e h)]

given #8 (wt=16): 533 - p(x) | - p($f3(x)) | - q($f4(y)) | - p($c15) | - q(y) | p($c19) | q(z).  [factor (247 c e)]

given #9 (wt=14): 537 p(x) | p($f1(x)) | - q(y) | q($f2(z)) | q(z) | - p(u).  [factor (249 d g)]

given #10 (wt=14): 539 p(x) | p($f1(x)) | - q($c7) | q($f2(y)) | q(y) | p($c6).  [factor (251 c g)]

given #11 (wt=14): 540 p(x) | p($f1(x)) | - q($f2(y)) | - q(y) | - p(z) | q(u).  [factor (253 c d)]

given #12 (wt=14): 542 p(x) | p($f1(x)) | - q($f2(y)) | - q(y) | p($c6) | - q($c7).  [factor (255 c d)]

given #13 (wt=13): 554 p(x) | p($f1(x)) | - q($c8) | q(y) | - p(z) | - q($c10).  [factor (265 c e)]

given #14 (wt=14): 557 p(x) | p($f1(x)) | q($c1) | - p($c2) | q($f2(y)) | q(y).  [factor (268 d g)]

given #15 (wt=14): 562 - p(x) | - p($f1(x)) | - q(y) | p(z) | q($f2(u)) | q(u).  [factor (280 e g)]

given #16 (wt=14): 563 - p(x) | - p($f1(x)) | - q($f2(y)) | p(z) | - q(y) | q(u).  [factor (284 c e)]

given #17 (wt=14): 564 - p(x) | - p($f1(x)) | - q($f2(y)) | p($c6) | - q(y) | - q($c7).  [factor (286 d f)]

given #18 (wt=13): 574 - p(x) | - p($f1(x)) | - q($c8) | p(y) | q(z) | - q($c10).  [factor (296 c f)]

given #19 (wt=14): 579 - p(x) | - p($f1(x)) | q($c1) | - p($c2) | q($f2(y)) | q(y).  [factor (299 c g)]

given #20 (wt=14): 583 - p(x) | - p($f1(x)) | q($c1) | - p($c2) | - q($f2(y)) | - q(y).  [factor (303 c g)]

given #21 (wt=13): 586 - p(x) | - p($f1(x)) | q($c1) | - p($c2) | - q($c10) | q($c8).  [factor (308 e g)]

given #22 (wt=13): 590 - p(x) | - p($f1(x)) | q($c1) | - p($c2) | - q($c8) | - q($c10).  [factor (313 c e)]

given #23 (wt=13): 614 - p($c3) | p(x) | - q(y) | - p($c5) | q($f2(z)) | q(z).  [factor (336 e g)]

given #24 (wt=13): 615 - p($c3) | p(x) | - q($f2(y)) | - p($c5) | - q(y) | q(z).  [factor (340 c e)]

given #25 (wt=13): 616 - p($c3) | p($c6) | - q($f2(x)) | - p($c5) | - q(x) | - q($c7).  [factor (342 c e)]

given #26 (wt=12): 626 - p($c3) | p(x) | - q($c8) | - p($c5) | q(y) | - q($c10).  [factor (352 c f)]

given #27 (wt=12): 637 p($c3) | - p(x) | q($c4) | - q(y) | q($c8) | p($c9).  [factor (365 c g)]

given #28 (wt=13): 651 p($c3) | - p($c5) | - q($f2(x)) | - q(x) | p($c6) | - q($c7).  [factor (381 c d)]

given #29 (wt=13): 692 - p($c11) | p($c19) | q($c12) | - p($c13) | q($f4(x)) | q(x).  [factor (419 c g)]

given #30 (wt=13): 709 p($c11) | - p(x) | - q(y) | q($f4(z)) | q(z) | p($c19).  [factor (440 d g)]

given #31 (wt=13): 713 p($c11) | - p(x) | - q($f4(y)) | - q(y) | p($c19) | q(z).  [factor (445 c d)]

given #32 (wt=13): 722 p($c11) | - p($c13) | q($c12) | q($f4(x)) | q(x) | p($c19).  [factor (454 c g)]

given #33 (wt=13): 727 p(x) | p($f3(x)) | q($c14) | - q(y) | q($c16) | - p(z).  [factor (463 c g)]

given #34 (wt=13): 729 p(x) | p($f3(x)) | q($c14) | - q($c18) | q($c16) | p($c17).  [factor (465 d g)]

given #35 (wt=13): 733 p(x) | p($f3(x)) | q($c14) | - q($c16) | p($c17) | - q($c18).  [factor (469 c d)]

given #36 (wt=14): 736 p(x) | p($f3(x)) | q($c14) | q($f4(y)) | q(y) | p($c19).  [factor (471 c g)]

given #37 (wt=14): 738 p(x) | p($f3(x)) | q($c14) | q($f4($c14)) | - p(y) | - q($c20).  [factor (474 c e)]

given #38 (wt=14): 740 p(x) | p($f3(x)) | q($c14) | - q($f4(y)) | - q(y) | p($c19).  [factor (476 c g)]

given #39 (wt=14): 741 p(x) | p($f3(x)) | q($c14) | - q($f4($c20)) | - q($c20) | - p(y).  [factor (478 e g)]

given #40 (wt=14): 749 p($c19) | p($f3($c19)) | - q(x) | - p($c15) | q($f4(y)) | q(y).  [factor (490 e g)]

given #41 (wt=14): 750 p(x) | p($f3(x)) | - q($c20) | - p($c15) | q($f4(y)) | q(y).  [factor (492 d g)]

given #42 (wt=14): 751 p($c19) | p($f3($c19)) | - q($f4(x)) | - p($c15) | - q(x) | q(y).  [factor (494 c e)]

given #43 (wt=14): 752 p(x) | p($f3(x)) | - q($f4(y)) | - p($c15) | - q(y) | - q($c20).  [factor (496 d f)]

given #44 (wt=13): 754 - p(x) | - p($f3(x)) | q($c14) | p(y) | - q(z) | q($c16).  [factor (498 c g)]

given #45 (wt=14): 760 - p(x) | - p($f3(x)) | q($c14) | p($c19) | q($f4(y)) | q(y).  [factor (507 d g)]

given #46 (wt=14): 761 - p(x) | - p($f3(x)) | q($c14) | p(y) | q($f4($c14)) | - q($c20).  [factor (509 c f)]

given #47 (wt=14): 762 - p(x) | - p($f3(x)) | q($c14) | p($c19) | - q($f4(y)) | - q(y).  [factor (511 d g)]

given #48 (wt=14): 763 - p(x) | - p($f3(x)) | q($c14) | p(y) | - q($f4($c20)) | - q($c20).  [factor (513 f g)]

given #49 (wt=14): 779 - p($c15) | - p($f3($c15)) | - q(x) | q($f4(y)) | q(y) | p($c19).  [factor (527 d g)]

given #50 (wt=14): 782 - p(x) | - p($f3(x)) | - q($c20) | - p($c15) | q($f4(y)) | q(y).  [factor (530 c g)]

given #51 (wt=14): 783 - p($c15) | - p($f3($c15)) | - q($f4(x)) | - q(x) | p($c19) | q(y).  [factor (532 c d)]

given #52 (wt=14): 786 - p(x) | - p($f3(x)) | - q($f4(y)) | - p($c15) | - q(y) | - q($c20).  [factor (535 c e)]

given #53 (wt=12): 788 p($c6) | p($f1($c6)) | - q($c7) | q($f2(x)) | q(x).  [factor (538 c f)]

given #54 (wt=12): 789 p($c6) | p($f1($c6)) | - q($f2(x)) | - q(x) | - q($c7).  [factor (541 c d)]

given #55 (wt=12): 790 p(x) | p($f1(x)) | - q($f2($c7)) | - q($c7) | p($c6).  [factor (542 d f)]

given #56 (wt=11): 793 p(x) | p($f1(x)) | - q(y) | q($c8) | p($c9).  [factor (545 d f)]

given #57 (wt=11): 794 p(x) | p($f1(x)) | - q($c10) | q($c8) | - p(y).  [factor (548 c f)]

given #58 (wt=11): 797 p(x) | p($f1(x)) | - q($c8) | q(y) | p($c9).  [factor (551 d f)]

given #59 (wt=12): 798 p(x) | p($f1(x)) | q($c1) | - p($c2) | q($f2($c1)).  [factor (555 d f)]

given #60 (wt=12): 800 - p(x) | - p($f1(x)) | - q($f2($c7)) | p($c6) | - q($c7).  [factor (564 e f)]

given #61 (wt=11): 801 - p(x) | - p($f1(x)) | - q(y) | p($c9) | q($c8).  [factor (566 e f)]

given #62 (wt=11): 802 - p(x) | - p($f1(x)) | - q($c10) | p(y) | q($c8).  [factor (569 c f)]

given #63 (wt=11): 803 - p(x) | - p($f1(x)) | - q($c8) | p($c9) | q(y).  [factor (571 e f)]

given #64 (wt=12): 805 - p($c2) | - p($f1($c2)) | q($c1) | q($f2(x)) | q(x).  [factor (575 c f)]

given #65 (wt=12): 807 - p(x) | - p($f1(x)) | q($c1) | - p($c2) | q($f2($c1)).  [factor (578 c f)]

given #66 (wt=12): 808 - p($c2) | - p($f1($c2)) | q($c1) | - q($f2(x)) | - q(x).  [factor (581 c f)]

given #67 (wt=11): 809 - p($c2) | - p($f1($c2)) | q($c1) | - q($c10) | q($c8).  [factor (584 d f)]

given #68 (wt=11): 810 - p($c2) | - p($f1($c2)) | q($c1) | - q($c8) | - q($c10).  [factor (588 c d)]

given #69 (wt=11): 812 - p($c3) | p(x) | q($c4) | q($f2(y)) | q(y).  [factor (591 c f)]

given #70 (wt=11): 816 - p($c3) | p(x) | q($c4) | - q($f2(y)) | - q(y).  [factor (599 c f)]

given #71 (wt=10): 817 - p($c3) | p($c9) | q($c4) | - q(x) | q($c8).  [factor (603 c f)]

given #72 (wt=10): 818 - p($c3) | p(x) | q($c4) | - q($c10) | q($c8).  [factor (605 d f)]

given #73 (wt=10): 821 - p($c3) | p(x) | q($c4) | - q($c8) | - q($c10).  [factor (611 c d)]

given #74 (wt=11): 822 - p($c3) | p($c6) | - q($f2($c7)) | - p($c5) | - q($c7).  [factor (616 e f)]

given #75 (wt=10): 823 - p($c3) | p($c9) | - q(x) | - p($c5) | q($c8).  [factor (618 e f)]

given #76 (wt=10): 824 - p($c3) | p(x) | - q($c10) | - p($c5) | q($c8).  [factor (621 c f)]

given #77 (wt=10): 825 - p($c3) | p($c9) | - q($c8) | - p($c5) | q(x).  [factor (623 e f)]

given #78 (wt=11): 827 p($c3) | - p(x) | q($c4) | q($f2(y)) | q(y).  [factor (627 c f)]

given #79 (wt=11): 830 p($c3) | - p(x) | q($c4) | - q($f2(y)) | - q(y).  [factor (634 c f)]

given #80 (wt=10): 831 p($c3) | - p(x) | q($c4) | - q($c10) | q($c8).  [factor (638 d f)]

given #81 (wt=10): 832 p($c3) | - p(x) | q($c4) | - q($c8) | p($c9).  [factor (641 c f)]

given #82 (wt=10): 833 p($c3) | - p(x) | q($c4) | - q($c8) | - q($c10).  [factor (643 c d)]

given #83 (wt=11): 834 p($c3) | - p($c5) | - q(x) | q($f2(y)) | q(y).  [factor (646 d f)]

given #84 (wt=11): 835 p($c3) | - p($c5) | - q($f2(x)) | - q(x) | q(y).  [factor (649 c d)]

given #85 (wt=11): 836 p($c3) | - p($c5) | - q($f2($c7)) | - q($c7) | p($c6).  [factor (651 d f)]

given #86 (wt=10): 837 p($c3) | - p($c5) | - q(x) | q($c8) | p($c9).  [factor (653 d f)]

given #87 (wt=10): 840 p($c3) | - p($c5) | - q($c8) | q(x) | p($c9).  [factor (659 d f)]

given #88 (wt=10): 841 p($c3) | - p($c5) | - q($c8) | q(x) | - q($c10).  [factor (662 c e)]

given #89 (wt=11): 850 - p($c11) | p($c19) | - q(x) | q($f4(y)) | q(y).  [factor (679 d f)]

given #90 (wt=11): 851 - p($c11) | p(x) | - q($c20) | q($f4(y)) | q(y).  [factor (681 c f)]

given #91 (wt=11): 852 - p($c11) | p($c19) | - q($f4(x)) | - q(x) | q(y).  [factor (684 c d)]

given #92 (wt=11): 853 - p($c11) | p(x) | - q($f4(y)) | - q(y) | - q($c20).  [factor (686 c d)]

given #93 (wt=11): 856 - p($c11) | p($c19) | q($c12) | - p($c13) | q($f4($c12)).  [factor (691 c f)]

given #94 (wt=11): 865 p($c11) | - p(x) | - q($c20) | q($f4(y)) | q(y).  [factor (710 c f)]

given #95 (wt=11): 866 p($c11) | - p(x) | - q($f4(y)) | - q(y) | - q($c20).  [factor (714 c d)]

given #96 (wt=11): 869 p($c11) | - p($c13) | q($c12) | q($f4($c12)) | p($c19).  [factor (721 c f)]

given #97 (wt=11): 871 p($c17) | p($f3($c17)) | q($c14) | - q($c18) | q($c16).  [factor (728 d f)]

given #98 (wt=11): 872 p(x) | p($f3(x)) | q($c14) | - q($c16) | - p(y).  [factor (730 c f)]

given #99 (wt=11): 873 p($c17) | p($f3($c17)) | q($c14) | - q($c16) | - q($c18).  [factor (732 c d)]

given #100 (wt=12): 875 p($c19) | p($f3($c19)) | q($c14) | q($f4(x)) | q(x).  [factor (734 c f)]

given #101 (wt=12): 876 p(x) | p($f3(x)) | q($c14) | q($f4($c14)) | p($c19).  [factor (735 c f)]

given #102 (wt=12): 877 p($c19) | p($f3($c19)) | q($c14) | - q($f4(x)) | - q(x).  [factor (739 c f)]

given #103 (wt=11): 878 p(x) | p($f3(x)) | - q(y) | - p($c15) | q($c16).  [factor (742 e f)]

given #104 (wt=11): 879 p(x) | p($f3(x)) | - q($c16) | - p($c15) | q(y).  [factor (746 e f)]

given #105 (wt=12): 880 p(x) | p($f3(x)) | - q($f4($c20)) | - p($c15) | - q($c20).  [factor (752 e f)]

given #106 (wt=11): 881 - p(x) | - p($f3(x)) | q($c14) | p(y) | - q($c16).  [factor (755 c f)]

given #107 (wt=12): 882 - p(x) | - p($f3(x)) | q($c14) | p($c19) | q($f4($c14)).  [factor (758 d f)]

given #108 (wt=11): 886 - p(x) | - p($f3(x)) | - q(y) | - p($c15) | q($c16).  [factor (767 e f)]

given #109 (wt=11): 891 - p(x) | - p($f3(x)) | - q($c16) | - p($c15) | q(y).  [factor (775 e f)]

given #110 (wt=12): 892 - p($c15) | - p($f3($c15)) | - q($c20) | q($f4(x)) | q(x).  [factor (780 c f)]

given #111 (wt=12): 893 - p($c15) | - p($f3($c15)) | - q($f4(x)) | - q(x) | - q($c20).  [factor (784 c d)]

given #112 (wt=12): 895 - p(x) | - p($f3(x)) | - q($f4($c20)) | - p($c15) | - q($c20).  [factor (786 e f)]

given #113 (wt=10): 896 p($c6) | p($f1($c6)) | - q($f2($c7)) | - q($c7).  [factor (789 d e)]

given #114 (wt=9): 897 p($c9) | p($f1($c9)) | - q(x) | q($c8).  [factor (791 d e)]

given #115 (wt=9): 898 p($c9) | p($f1($c9)) | - q($c8) | q(x).  [factor (795 d e)]

given #116 (wt=10): 899 - p($c2) | - p($f1($c2)) | q($c1) | q($f2($c1)).  [factor (804 c e)]

given #117 (wt=9): 900 - p($c3) | p(x) | q($c4) | q($f2($c4)).  [factor (811 c e)]

given #118 (wt=8): 901 - p($c3) | p($c9) | q($c4) | - q($c8).  [factor (819 c e)]

given #119 (wt=9): 902 p($c3) | - p(x) | q($c4) | q($f2($c4)).  [factor (826 c e)]

given #120 (wt=8): 903 p($c3) | - p($c5) | - q($c10) | q($c8).  [factor (838 c e)]

given #121 (wt=8): 904 - p($c11) | p(x) | - q(y) | q($c16).  [factor (842 d e)]

given #122 (wt=8): 905 - p($c11) | p(x) | - q($c16) | q(y).  [factor (846 d e)]

given #123 (wt=9): 906 - p($c11) | p(x) | - q($f4($c20)) | - q($c20).  [factor (853 d e)]

given #124 (wt=8): 907 p($c11) | - p(x) | - q(y) | q($c16).  [factor (857 d e)]

given #125 (wt=8): 908 p($c11) | - p(x) | - q($c16) | q(y).  [factor (861 d e)]

given #126 (wt=9): 909 p($c11) | - p(x) | - q($f4($c20)) | - q($c20).  [factor (866 d e)]

given #127 (wt=10): 910 p($c19) | p($f3($c19)) | q($c14) | q($f4($c14)).  [factor (874 c e)]

given #128 (wt=9): 911 - p($c15) | - p($f3($c15)) | - q(x) | q($c16).  [factor (883 d e)]

given #129 (wt=9): 912 - p($c15) | - p($f3($c15)) | - q($c16) | q(x).  [factor (888 d e)]

given #130 (wt=10): 913 - p($c15) | - p($f3($c15)) | - q($f4($c20)) | - q($c20).  [factor (893 d e)]

given #131 (wt=19): 925 p(x) | p($f3(x)) | q($c14) | p($c19) | p($c3) | - p(y) | q($c4) | q($c8) | p($c9).  [factor (915 c d)]

given #132 (wt=11): 961 p($c19) | p($f3($c19)) | q($c14) | q($c16) | - p(x).  [factor (938 c d)]

given #133 (wt=13): 940 p(x) | p($f3(x)) | q($c14) | p($c19) | q($c16) | - p(y).  [factor (920 c d)]

given #134 (wt=14): 976 p($c19) | p($f3($c19)) | q($c14) | - p($c3) | - p($c5) | q($f2($c14)).  [factor (962 c g)]

given #135 (wt=14): 1005 p($c9) | p($f1($c9)) | q($c8) | p($f3($c9)) | q($c14) | p($c19).  [factor (990 c f)]

given #136 (wt=21): 936 p(x) | p($f3(x)) | q($c14) | p($c19) | p(y) | p($f1(y)) | q($f2(z)) | q(z) | - p(u).  [factor (918 c d)]

given #137 (wt=12): 1051 p($c9) | p($f1($c9)) | q($c8) | p($f3($c9)) | p($c19).  [resolve (1005 e 897 c) merge f merge g merge h]

given #138 (wt=12): 1056 p($c9) | p($f1($c9)) | p($f3($c9)) | p($c19) | q(x).  [resolve (1051 c 898 c) merge e merge f]

given #139 (wt=14): 1007 p($c9) | p($f1($c9)) | q($c8) | p($c19) | p($f3($c19)) | q($c14).  [factor (992 d g)]

given #140 (wt=12): 1073 p($c9) | p($f1($c9)) | q($c8) | p($c19) | p($f3($c19)).  [resolve (1007 f 897 c) merge f merge g merge h]

given #141 (wt=17): 941 p($c19) | p($f3($c19)) | q($c14) | p($c3) | - p(x) | q($c4) | q($c8) | p($c9).  [factor (922 c d)]

given #142 (wt=12): 1078 p($c9) | p($f1($c9)) | p($c19) | p($f3($c19)) | q(x).  [resolve (1073 c 898 c) merge e merge f]

given #143 (wt=14): 1008 p($c19) | p($f1($c19)) | q($c8) | p($c9) | p($f3($c19)) | q($c14).  [factor (994 c g)]

given #144 (wt=12): 1111 p($c19) | p($f1($c19)) | q($c8) | p($c9) | p($f3($c19)).  [factor (1103 a f) merge f]

given #145 (wt=12): 1129 p($c19) | p($f1($c19)) | p($c9) | p($f3($c19)) | q(x).  [factor (1123 a e) merge e]

given #146 (wt=17): 942 p($c3) | p($f3($c3)) | q($c14) | p($c19) | - p(x) | q($c4) | q($c8) | p($c9).  [factor (923 c d)]

given #147 (wt=14): 1012 p($c19) | p($f1($c19)) | q($c8) | p($c9) | p($f3($c9)) | q($c14).  [factor (1000 d e)]

given #148 (wt=12): 1163 p($c19) | p($f1($c19)) | q($c8) | p($c9) | p($f3($c9)).  [factor (1153 a f) merge f]

given #149 (wt=12): 1183 p($c19) | p($f1($c19)) | p($c9) | p($f3($c9)) | q(x).  [factor (1175 a e) merge e]

given #150 (wt=14): 1038 p($c3) | - p($c5) | q($f2($c14)) | q($c14) | p($f3($c3)) | p($c19).  [factor (1035 d f)]

given #151 (wt=17): 943 p($c9) | p($f3($c9)) | q($c14) | p($c19) | p($c3) | - p(x) | q($c4) | q($c8).  [factor (924 c d)]

given #152 (wt=14): 1039 p($c3) | - p($c5) | q($f2($c14)) | q($c14) | p($c19) | p($f3($c19)).  [factor (1036 e g)]

given #153 (wt=14): 1067 p($c9) | p($f1($c9)) | p($f3($c9)) | p($c19) | - p($c11) | - q($c20).  [factor (1059 a f)]

given #154 (wt=12): 1200 p($c9) | p($f1($c9)) | p($f3($c9)) | p($c19) | - p($c11).  [resolve (1067 f 1056 e) merge f merge g merge h merge i]

given #155 (wt=14): 1068 p($c9) | p($f1($c9)) | p($f3($c9)) | p($c19) | - p($c15) | - q($c20).  [factor (1062 a e) merge e]

given #156 (wt=18): 946 p(x) | p($f3(x)) | q($c14) | p($c19) | - p($c3) | - p($c5) | q($f2(y)) | q(y).  [factor (927 c d)]

given #157 (wt=12): 1203 p($c9) | p($f1($c9)) | p($f3($c9)) | p($c19) | - p($c15).  [resolve (1068 f 1056 e) merge f merge g merge h merge i]

given #158 (wt=14): 1069 p($c9) | p($f1($c9)) | p($f3($c9)) | p($c19) | - q($c7) | p($c6).  [factor (1066 a e) merge e]

given #159 (wt=12): 1206 p($c9) | p($f1($c9)) | p($f3($c9)) | p($c19) | p($c6).  [resolve (1069 e 1056 e) merge f merge g merge h merge i]

given #160 (wt=14): 1089 p($c9) | p($f1($c9)) | p($c19) | p($f3($c19)) | - p($c11) | - q($c20).  [factor (1081 a f)]

given #161 (wt=19): 950 p(x) | p($f3(x)) | q($c14) | p($c19) | - p(y) | - p($f1(y)) | q($f2(z)) | q(z).  [factor (930 c d)]

given #162 (wt=12): 1221 p($c9) | p($f1($c9)) | p($c19) | p($f3($c19)) | - p($c11).  [resolve (1089 f 1078 e) merge f merge g merge h merge i]

given #163 (wt=14): 1091 p($c9) | p($f1($c9)) | p($c19) | p($f3($c19)) | - p($c15) | - q($c20).  [factor (1084 c e) merge e]

given #164 (wt=12): 1223 p($c9) | p($f1($c9)) | p($c19) | p($f3($c19)) | - p($c15).  [resolve (1091 f 1078 e) merge f merge g merge h merge i]

given #165 (wt=14): 1092 p($c9) | p($f1($c9)) | p($c19) | p($f3($c19)) | - q($c7) | p($c6).  [factor (1088 a e) merge e]

given #166 (wt=19): 954 p($c19) | p($f3($c19)) | q($c14) | p(x) | p($f1(x)) | q($f2(y)) | q(y) | - p(z).  [factor (932 c d)]

given #167 (wt=12): 1225 p($c9) | p($f1($c9)) | p($c19) | p($f3($c19)) | p($c6).  [resolve (1092 e 1078 e) merge f merge g merge h merge i]

given #168 (wt=14): 1140 p($c19) | p($f1($c19)) | p($c9) | p($f3($c19)) | - p($c11) | - q($c20).  [factor (1132 a f)]

given #169 (wt=12): 1227 p($c19) | p($f1($c19)) | p($c9) | p($f3($c19)) | - p($c11).  [resolve (1140 f 1129 e) merge f merge g merge h merge i]

given #170 (wt=14): 1141 p($c19) | p($f1($c19)) | p($c9) | p($f3($c19)) | - p($c15) | - q($c20).  [factor (1135 a e) merge e]

given #171 (wt=19): 955 p(x) | p($f3(x)) | q($c14) | p($c19) | p($f1(x)) | q($f2(y)) | q(y) | - p(z).  [factor (933 c d)]

given #172 (wt=12): 1229 p($c19) | p($f1($c19)) | p($c9) | p($f3($c19)) | - p($c15).  [resolve (1141 f 1129 e) merge f merge g merge h merge i]

given #173 (wt=14): 1142 p($c19) | p($f1($c19)) | p($c9) | p($f3($c19)) | - q($c7) | p($c6).  [factor (1139 a e) merge e]

given #174 (wt=12): 1231 p($c19) | p($f1($c19)) | p($c9) | p($f3($c19)) | p($c6).  [resolve (1142 e 1129 e) merge f merge g merge h merge i]

given #175 (wt=14): 1194 p($c19) | p($f1($c19)) | p($c9) | p($f3($c9)) | - p($c11) | - q($c20).  [factor (1186 a f)]

given #176 (wt=20): 956 p($f1(x)) | p($f3($f1(x))) | q($c14) | p($c19) | p(x) | q($f2(y)) | q(y) | - p(z).  [factor (934 c d)]

given #177 (wt=12): 1251 p($c19) | p($f1($c19)) | p($c9) | p($f3($c9)) | - p($c11).  [resolve (1194 f 1183 e) merge f merge g merge h merge i]

given #178 (wt=14): 1196 p($c19) | p($f1($c19)) | p($c9) | p($f3($c9)) | - p($c15) | - q($c20).  [factor (1189 c e) merge e]

given #179 (wt=12): 1252 p($c19) | p($f1($c19)) | p($c9) | p($f3($c9)) | - p($c15).  [resolve (1196 f 1183 e) merge f merge g merge h merge i]

given #180 (wt=14): 1197 p($c19) | p($f1($c19)) | p($c9) | p($f3($c9)) | - q($c7) | p($c6).  [factor (1193 a e) merge e]

given #181 (wt=20): 958 p(x) | p($f3(x)) | q($c14) | p($c19) | p($f1($f3(x))) | q($f2(y)) | q(y) | - p(z).  [factor (935 c d)]

given #182 (wt=12): 1253 p($c19) | p($f1($c19)) | p($c9) | p($f3($c9)) | p($c6).  [resolve (1197 e 1183 e) merge f merge g merge h merge i]

given #183 (wt=15): 977 p($c19) | p($f3($c19)) | q($c14) | - p(x) | - p($f1(x)) | q($f2($c14)).  [factor (965 c g)]

given #184 (wt=15): 978 p($c19) | p($f3($c19)) | q($c14) | p($f1($c19)) | q($f2($c14)) | - p(x).  [factor (968 c f)]

given #185 (wt=15): 1006 p($c9) | p($f1($c9)) | q($c8) | p($f3($f1($c9))) | q($c14) | p($c19).  [factor (991 c f)]

given #186 (wt=19): 959 p(x) | p($f3(x)) | q($c14) | p($c19) | p(y) | p($f1(y)) | q($f2($c14)) | - p(z).  [factor (936 c h)]

given #187 (wt=13): 1257 p($c9) | p($f1($c9)) | q($c8) | p($f3($f1($c9))) | p($c19).  [resolve (1006 e 897 c) merge f merge g merge h]

given #188 (wt=13): 1262 p($c9) | p($f1($c9)) | p($f3($f1($c9))) | p($c19) | q(x).  [resolve (1257 c 898 c) merge e merge f]

given #189 (wt=15): 1009 p($f3($c9)) | p($f1($f3($c9))) | q($c8) | p($c9) | q($c14) | p($c19).  [factor (996 d e)]

given #190 (wt=13): 1297 p($f3($c9)) | p($f1($f3($c9))) | q($c8) | p($c9) | p($c19).  [factor (1286 a f) merge f]

given #191 (wt=19): 960 p(x) | p($f3(x)) | q($c14) | p($c19) | p($f1($c19)) | q($f2(y)) | q(y) | - p(z).  [factor (936 d e)]

given #192 (wt=13): 1318 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | q(x).  [factor (1309 a e) merge e]

given #193 (wt=15): 1010 p($f3($c19)) | p($f1($f3($c19))) | q($c8) | p($c9) | p($c19) | q($c14).  [factor (996 e g)]

given #194 (wt=13): 1352 p($f3($c19)) | p($f1($f3($c19))) | q($c8) | p($c9) | p($c19).  [factor (1343 a f) merge f]

given #195 (wt=13): 1371 p($f3($c19)) | p($f1($f3($c19))) | p($c9) | p($c19) | q(x).  [factor (1364 a e) merge e]

given #196 (wt=16): 962 p($c19) | p($f3($c19)) | q($c14) | - p($c3) | - p($c5) | q($f2(x)) | q(x).  [factor (944 c d)]

given #197 (wt=15): 1011 p($c19) | p($f1($c19)) | q($c8) | p($c9) | p($f3($f1($c19))) | q($c14).  [factor (999 c g)]

given #198 (wt=13): 1406 p($c19) | p($f1($c19)) | q($c8) | p($c9) | p($f3($f1($c19))).  [factor (1397 a f) merge f]

given #199 (wt=13): 1426 p($c19) | p($f1($c19)) | p($c9) | p($f3($f1($c19))) | q(x).  [factor (1419 a e) merge e]

given #200 (wt=15): 1023 - p($c3) | p($c9) | q($c4) | q($c8) | p($f3($c9)) | q($c14) | p($c19).  [factor (1020 c g)]

given #201 (wt=16): 964 p(x) | p($f3(x)) | q($c14) | p($c19) | - p($c3) | - p($c5) | q($f2($c14)).  [factor (946 c h)]

given #202 (wt=15): 1024 - p($c3) | p($c9) | q($c4) | q($c8) | p($c19) | p($f3($c19)) | q($c14).  [factor (1021 e h)]

given #203 (wt=15): 1029 - p($c3) | p($c9) | - p($c5) | q($c8) | p($f3($c9)) | q($c14) | p($c19).  [factor (1026 d g)]

given #204 (wt=15): 1030 - p($c3) | p($c9) | - p($c5) | q($c8) | p($c19) | p($f3($c19)) | q($c14).  [factor (1027 e h)]

given #205 (wt=15): 1045 p($c3) | - p($c5) | q($c8) | p($c9) | p($f3($c3)) | q($c14) | p($c19).  [factor (1041 c g)]

given #206 (wt=17): 965 p($c19) | p($f3($c19)) | q($c14) | - p(x) | - p($f1(x)) | q($f2(y)) | q(y).  [factor (948 c d)]

given #207 (wt=15): 1046 p($c3) | - p($c5) | q($c8) | p($c9) | p($f3($c9)) | q($c14) | p($c19).  [factor (1042 d e)]

given #208 (wt=15): 1047 p($c3) | - p($c5) | q($c8) | p($c9) | p($c19) | p($f3($c19)) | q($c14).  [factor (1042 e h)]

given #209 (wt=15): 1273 p($c9) | p($f1($c9)) | p($f3($f1($c9))) | p($c19) | - p($c11) | - q($c20).  [factor (1265 a f)]

given #210 (wt=13): 1441 p($c9) | p($f1($c9)) | p($f3($f1($c9))) | p($c19) | - p($c11).  [resolve (1273 f 1262 e) merge f merge g merge h merge i]

given #211 (wt=17): 967 p(x) | p($f3(x)) | q($c14) | p($c19) | - p(y) | - p($f1(y)) | q($f2($c14)).  [factor (950 c h)]

given #212 (wt=15): 1274 p($c9) | p($f1($c9)) | p($f3($f1($c9))) | p($c19) | - p($c15) | - q($c20).  [factor (1268 b e) merge e]

given #213 (wt=13): 1443 p($c9) | p($f1($c9)) | p($f3($f1($c9))) | p($c19) | - p($c15).  [resolve (1274 f 1262 e) merge f merge g merge h merge i]

given #214 (wt=15): 1275 p($c9) | p($f1($c9)) | p($f3($f1($c9))) | p($c19) | - q($c7) | p($c6).  [factor (1272 a e) merge e]

given #215 (wt=13): 1445 p($c9) | p($f1($c9)) | p($f3($f1($c9))) | p($c19) | p($c6).  [resolve (1275 e 1262 e) merge f merge g merge h merge i]

given #216 (wt=17): 968 p($c19) | p($f3($c19)) | q($c14) | p($f1($c19)) | q($f2(x)) | q(x) | - p(y).  [factor (952 c d)]

given #217 (wt=15): 1329 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | - p($c11) | - q($c20).  [factor (1321 a f)]

given #218 (wt=13): 1447 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | - p($c11).  [resolve (1329 f 1318 e) merge f merge g merge h merge i]

given #219 (wt=15): 1331 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | - p($c15) | - q($c20).  [factor (1324 a f) merge e]

given #220 (wt=13): 1449 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | - p($c15).  [resolve (1331 f 1318 e) merge f merge g merge h merge i]

given #221 (wt=18): 969 p($c19) | p($f3($c19)) | q($c14) | p($f1($f3($c19))) | q($f2(x)) | q(x) | - p(y).  [factor (953 c d)]

given #222 (wt=15): 1332 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | - q($c7) | p($c6).  [factor (1328 a e) merge e]

given #223 (wt=13): 1451 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | p($c6).  [resolve (1332 e 1318 e) merge f merge g merge h merge i]

given #224 (wt=13): 1471 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c14) | q($c16).  [factor (1459 a f) merge e]

given #225 (wt=13): 1493 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | - p($c11).  [factor (1478 a g)]

given #226 (wt=17): 970 p($c19) | p($f3($c19)) | q($c14) | p(x) | p($f1(x)) | q($f2($c14)) | - p(y).  [factor (954 c g)]

given #227 (wt=13): 1495 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | - p($c15).  [factor (1480 a g) merge f]

given #228 (wt=15): 1382 p($f3($c19)) | p($f1($f3($c19))) | p($c9) | p($c19) | - p($c11) | - q($c20).  [factor (1374 a f)]

given #229 (wt=13): 1507 p($f3($c19)) | p($f1($f3($c19))) | p($c9) | p($c19) | - p($c11).  [resolve (1382 f 1371 e) merge f merge g merge h merge i]

given #230 (wt=15): 1384 p($f3($c19)) | p($f1($f3($c19))) | p($c9) | p($c19) | - p($c15) | - q($c20).  [factor (1377 a f) merge e]

given #231 (wt=17): 971 p(x) | p($f3(x)) | q($c14) | p($c19) | p($f1(x)) | q($f2($c14)) | - p(y).  [factor (955 c g)]

given #232 (wt=13): 1508 p($f3($c19)) | p($f1($f3($c19))) | p($c9) | p($c19) | - p($c15).  [resolve (1384 f 1371 e) merge f merge g merge h merge i]

given #233 (wt=15): 1385 p($f3($c19)) | p($f1($f3($c19))) | p($c9) | p($c19) | - q($c7) | p($c6).  [factor (1381 a e) merge e]

given #234 (wt=13): 1509 p($f3($c19)) | p($f1($f3($c19))) | p($c9) | p($c19) | p($c6).  [resolve (1385 e 1371 e) merge f merge g merge h merge i]

given #235 (wt=13): 1512 p($f3($c19)) | p($c9) | p($c19) | p($c6) | q($c14) | q($c16).  [resolve (1509 b 961 e) merge e merge f]

given #236 (wt=18): 972 p($f1(x)) | p($f3($f1(x))) | q($c14) | p($c19) | p(x) | q($f2($c14)) | - p(y).  [factor (956 c g)]

given #237 (wt=13): 1540 p($f3($c19)) | p($c9) | p($c19) | p($c6) | q($c16) | - p($c11).  [factor (1525 a g)]

given #238 (wt=13): 1542 p($f3($c19)) | p($c9) | p($c19) | p($c6) | q($c16) | - p($c15).  [factor (1527 a g) merge f]

given #239 (wt=15): 1437 p($c19) | p($f1($c19)) | p($c9) | p($f3($f1($c19))) | - p($c11) | - q($c20).  [factor (1429 a f)]

given #240 (wt=13): 1554 p($c19) | p($f1($c19)) | p($c9) | p($f3($f1($c19))) | - p($c11).  [resolve (1437 f 1426 e) merge f merge g merge h merge i]

given #241 (wt=18): 973 p($f1($c19)) | p($f3($f1($c19))) | q($c14) | p($c19) | q($f2(x)) | q(x) | - p(y).  [factor (956 d e)]

given #242 (wt=15): 1438 p($c19) | p($f1($c19)) | p($c9) | p($f3($f1($c19))) | - p($c15) | - q($c20).  [factor (1432 b e) merge e]

given #243 (wt=13): 1555 p($c19) | p($f1($c19)) | p($c9) | p($f3($f1($c19))) | - p($c15).  [resolve (1438 f 1426 e) merge f merge g merge h merge i]

given #244 (wt=15): 1439 p($c19) | p($f1($c19)) | p($c9) | p($f3($f1($c19))) | - q($c7) | p($c6).  [factor (1436 a e) merge e]

given #245 (wt=13): 1556 p($c19) | p($f1($c19)) | p($c9) | p($f3($f1($c19))) | p($c6).  [resolve (1439 e 1426 e) merge f merge g merge h merge i]

given #246 (wt=18): 974 p(x) | p($f3(x)) | q($c14) | p($c19) | p($f1($f3(x))) | q($f2($c14)) | - p(y).  [factor (958 c g)]

given #247 (wt=15): 1477 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | p($c11) | - p(x).  [resolve (1471 e 907 c) merge h]

given #248 (wt=13): 1558 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | p($c11).  [resolve (1477 g 1451 b) merge g merge h merge i merge j]

given #249 (wt=15): 1524 p($f3($c19)) | p($c9) | p($c19) | p($c6) | q($c16) | p($c11) | - p(x).  [resolve (1512 e 907 c) merge h]

given #250 (wt=13): 1564 p($f3($c19)) | p($c9) | p($c19) | p($c6) | q($c16) | p($c11).  [resolve (1524 g 1509 b) merge g merge h merge i merge j]

given #251 (wt=17): 975 p(x) | p($f3(x)) | q($c14) | p($c19) | p($f1($c19)) | q($f2($c14)) | - p(y).  [factor (959 d e)]

given #252 (wt=15): 1560 p($f3($c9)) | p($c9) | p($c19) | p($c6) | p($c11) | - p(x) | q(y).  [resolve (1558 e 908 c) merge f]

given #253 (wt=13): 1571 p($f3($c9)) | p($c9) | p($c19) | p($c6) | p($c11) | q(x).  [resolve (1560 f 1451 b) merge g merge h merge i merge j]

given #254 (wt=15): 1566 p($f3($c19)) | p($c9) | p($c19) | p($c6) | p($c11) | - p(x) | q(y).  [resolve (1564 e 908 c) merge f]

given #255 (wt=13): 1580 p($f3($c19)) | p($c9) | p($c19) | p($c6) | p($c11) | q(x).  [resolve (1566 f 1509 b) merge g merge h merge i merge j]

given #256 (wt=16): 979 p($c19) | p($f3($c19)) | q($c14) | p($f1($f3($c19))) | q($f2($c14)) | - p(x).  [factor (969 c f)]

given #257 (wt=15): 1573 p($f3($c9)) | p($c9) | p($c19) | p($c6) | p($c11) | - p(x) | - q($c20).  [resolve (1571 f 909 c) merge f]

given #258 (wt=13): 1590 p($f3($c9)) | p($c9) | p($c19) | p($c6) | p($c11) | - p(x).  [resolve (1573 g 1571 f) merge g merge h merge i merge j merge k]

given #259 (wt=11): 1592 p($f3($c9)) | p($c9) | p($c19) | p($c6) | p($c11).  [resolve (1590 f 1451 b) merge f merge g merge h merge i]

given #260 (wt=15): 1582 p($f3($c19)) | p($c9) | p($c19) | p($c6) | p($c11) | - p(x) | - q($c20).  [resolve (1580 f 909 c) merge f]

given #261 (wt=16): 980 p($f1($c19)) | p($f3($f1($c19))) | q($c14) | p($c19) | q($f2($c14)) | - p(x).  [factor (972 d e)]

given #262 (wt=13): 1634 p($f3($c19)) | p($c9) | p($c19) | p($c6) | p($c11) | - p(x).  [resolve (1582 g 1580 f) merge g merge h merge i merge j merge k]

given #263 (wt=11): 1635 p($f3($c19)) | p($c9) | p($c19) | p($c6) | p($c11).  [resolve (1634 f 1592 a) merge f merge g merge h merge i]

given #264 (wt=15): 1604 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | q($c4) | q($f2($c4)).  [resolve (1592 a 902 b)]

given #265 (wt=15): 1622 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c6)) | q($c14) | q($c16).  [factor (1601 c e)]

given #266 (wt=18): 987 p(x) | p($f1(x)) | q($c8) | p($c9) | p(y) | p($f3(y)) | q($c14) | p($c19).  [factor (981 c h)]

given #267 (wt=14): 1698 p($c9) | p($f1($c9)) | q($c8) | p(x) | p($f3(x)) | p($c19).  [factor (1662 a d) merge g]

given #268 (wt=14): 1791 p(x) | p($f1(x)) | q($c8) | p($c9) | p($f3(x)) | p($c19).  [factor (1745 a g) merge g]

given #269 (wt=14): 1793 p($c19) | p($f1($c19)) | q($c8) | p($c9) | p(x) | p($f3(x)).  [factor (1747 a g) merge g]

given #270 (wt=14): 1795 p(x) | p($f1(x)) | q($c8) | p($c9) | p($f3($c9)) | p($c19).  [factor (1748 d e)]

given #271 (wt=18): 1015 - p(x) | - p($f1(x)) | p($c9) | q($c8) | p(y) | p($f3(y)) | q($c14) | p($c19).  [factor (1013 d h)]

given #272 (wt=14): 1796 p(x) | p($f1(x)) | q($c8) | p($c9) | p($c19) | p($f3($c19)).  [factor (1748 e g)]

given #273 (wt=14): 1801 p($c9) | p($f1($c9)) | p(x) | p($f3(x)) | p($c19) | q(y).  [resolve (1698 c 898 c) merge f merge g]

given #274 (wt=14): 1824 p(x) | p($f1(x)) | p($c9) | p($f3(x)) | p($c19) | q(y).  [factor (1813 a f) merge f]

given #275 (wt=14): 1846 p($c19) | p($f1($c19)) | p($c9) | p(x) | p($f3(x)) | q(y).  [factor (1836 a f) merge f]

given #276 (wt=16): 1017 - p(x) | - p($f1(x)) | p($c9) | q($c8) | p($f3($c9)) | q($c14) | p($c19).  [factor (1014 d g)]

given #277 (wt=14): 1871 p(x) | p($f1(x)) | p($c9) | p($f3($c9)) | p($c19) | q(y).  [factor (1858 a f) merge f]

given #278 (wt=14): 1894 p(x) | p($f1(x)) | p($c9) | p($c19) | p($f3($c19)) | q(y).  [factor (1883 a f) merge f]

given #279 (wt=14): 1915 p($c9) | p($f1($c9)) | p($c6) | p($f3($c6)) | p($c19) | - q($c7).  [factor (1914 c g)]

given #280 (wt=12): 1994 p($c9) | p($f1($c9)) | p($c6) | p($f3($c6)) | p($c19).  [factor (1991 c f) merge f]

given #281 (wt=16): 1018 - p(x) | - p($f1(x)) | p($c9) | q($c8) | p($c19) | p($f3($c19)) | q($c14).  [factor (1015 e h)]

given #282 (wt=14): 1928 p($c6) | p($f1($c6)) | p($c9) | p($f3($c6)) | p($c19) | - q($c7).  [factor (1919 a f) merge f]

given #283 (wt=12): 2002 p($c6) | p($f1($c6)) | p($c9) | p($f3($c6)) | p($c19).  [factor (1998 a f) merge f merge g]

given #284 (wt=14): 1952 p($c19) | p($f1($c19)) | p($c9) | p($c6) | p($f3($c6)) | - q($c7).  [factor (1951 d g)]

given #285 (wt=12): 2022 p($c19) | p($f1($c19)) | p($c9) | p($c6) | p($f3($c6)).  [factor (2021 d f) merge f]

given #286 (wt=17): 1021 - p($c3) | p($c9) | q($c4) | q($c8) | p(x) | p($f3(x)) | q($c14) | p($c19).  [factor (1019 c h)]

given #287 (wt=14): 1965 p($c6) | p($f1($c6)) | p($c9) | p($f3($c9)) | p($c19) | - q($c7).  [factor (1956 a f) merge f]

given #288 (wt=12): 2026 p($c6) | p($f1($c6)) | p($c9) | p($f3($c9)) | p($c19).  [factor (2024 a f) merge f]

given #289 (wt=14): 1983 p($c6) | p($f1($c6)) | p($c9) | p($c19) | p($f3($c19)) | - q($c7).  [factor (1974 a f) merge f]

given #290 (wt=12): 2028 p($c6) | p($f1($c6)) | p($c9) | p($c19) | p($f3($c19)).  [factor (2027 a f) merge f]

given #291 (wt=17): 1027 - p($c3) | p($c9) | - p($c5) | q($c8) | p(x) | p($f3(x)) | q($c14) | p($c19).  [factor (1025 d h)]

given #292 (wt=15): 1623 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c11)) | q($c14) | q($c16).  [factor (1601 d e)]

given #293 (wt=15): 1652 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c6)) | q($c16) | - p(x).  [resolve (1622 f 907 c) merge g merge i]

given #294 (wt=13): 2031 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c6)) | q($c16).  [resolve (1652 g 1635 a) merge g merge h merge i merge j]

given #295 (wt=15): 1792 p($f3(x)) | p($f1($f3(x))) | q($c8) | p($c9) | p(x) | p($c19).  [factor (1746 a g) merge g]

given #296 (wt=18): 1033 p($c3) | - p($c5) | q($f2(x)) | q(x) | p(y) | p($f3(y)) | q($c14) | p($c19).  [factor (1031 c h)]

given #297 (wt=15): 1794 p(x) | p($f1(x)) | q($c8) | p($c9) | p($f3($f1(x))) | p($c19).  [factor (1748 b e)]

given #298 (wt=15): 2030 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c11)) | q($c16) | - p(x).  [resolve (1623 f 907 c) merge g merge i]

given #299 (wt=13): 2079 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c11)) | q($c16).  [resolve (2030 g 1635 a) merge g merge h merge i merge j]

given #300 (wt=15): 2033 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c6)) | - p(x) | q(y).  [resolve (2031 f 908 c) merge f]

given #301 (wt=16): 1035 p($c3) | - p($c5) | q($f2(x)) | q(x) | p($f3($c3)) | q($c14) | p($c19).  [factor (1032 c g)]

given #302 (wt=13): 2082 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c6)) | q(x).  [resolve (2033 f 1635 a) merge g merge h merge i merge j]

given #303 (wt=15): 2055 p($f3(x)) | p($f1($f3(x))) | p($c9) | p(x) | p($c19) | q(y).  [factor (2045 a f) merge f]

given #304 (wt=15): 2077 p(x) | p($f1(x)) | p($c9) | p($f3($f1(x))) | p($c19) | q(y).  [factor (2067 a f) merge f]

given #305 (wt=15): 2081 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c11)) | - p(x) | q(y).  [resolve (2079 f 908 c) merge f]

given #306 (wt=16): 1036 p($c3) | - p($c5) | q($f2($c14)) | q($c14) | p(x) | p($f3(x)) | p($c19).  [factor (1033 d g)]

given #307 (wt=13): 2129 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c11)) | q(x).  [resolve (2081 f 1635 a) merge g merge h merge i merge j]

given #308 (wt=15): 2084 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c6)) | - p(x) | - q($c20).  [resolve (2082 f 909 c) merge f]

given #309 (wt=13): 2138 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c6)) | - p(x).  [resolve (2084 g 2082 f) merge g merge h merge i merge j merge k]

given #310 (wt=11): 2139 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c6)).  [resolve (2138 f 1635 a) merge f merge g merge h merge i]

given #311 (wt=16): 1037 p($c3) | - p($c5) | q($f2(x)) | q(x) | p($c19) | p($f3($c19)) | q($c14).  [factor (1033 e h)]

given #312 (wt=15): 2110 p($f3($c6)) | p($f1($f3($c6))) | p($c9) | p($c6) | p($c19) | - q($c7).  [factor (2109 d g)]

given #313 (wt=13): 2147 p($f3($c6)) | p($f1($f3($c6))) | p($c9) | p($c6) | p($c19).  [factor (2141 a f) merge f merge g]

given #314 (wt=13): 2158 p($f3($c6)) | p($c9) | p($c6) | p($c19) | q($c14) | q($c16).  [factor (2150 a f) merge e]

given #315 (wt=13): 2177 p($f3($c6)) | p($c9) | p($c6) | p($c19) | q($c16) | - p($c11).  [factor (2164 a g)]

given #316 (wt=17): 1042 p($c3) | - p($c5) | q($c8) | p($c9) | p(x) | p($f3(x)) | q($c14) | p($c19).  [factor (1040 c h)]

given #317 (wt=13): 2179 p($f3($c6)) | p($c9) | p($c6) | p($c19) | q($c16) | - p($c15).  [factor (2166 a g) merge f]

given #318 (wt=15): 2123 p($c6) | p($f1($c6)) | p($c9) | p($f3($f1($c6))) | p($c19) | - q($c7).  [factor (2114 a f) merge f]

given #319 (wt=13): 2194 p($c6) | p($f1($c6)) | p($c9) | p($f3($f1($c6))) | p($c19).  [factor (2189 a f) merge f merge g]

given #320 (wt=15): 2131 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c11)) | - p(x) | - q($c20).  [resolve (2129 f 909 c) merge f]

given #321 (wt=16): 1058 p($c9) | p($f1($c9)) | p($f3($c9)) | p($c19) | p($c11) | - p(x) | - q($c20).  [resolve (1056 e 909 c)]

given #322 (wt=13): 2195 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c11)) | - p(x).  [resolve (2131 g 2129 f) merge g merge h merge i merge j merge k]

given #323 (wt=11): 2207 p($c9) | p($c19) | p($c6) | p($c11) | p($f3($c11)).  [resolve (2195 f 2139 e) merge f merge g merge h merge i]

given #324 (wt=14): 2205 p($c9) | p($f1($c9)) | p($f3($c9)) | p($c19) | p($c11) | - p(x).  [resolve (1058 g 1056 e) merge g merge h merge i merge j]

given #325 (wt=16): 1080 p($c9) | p($f1($c9)) | p($c19) | p($f3($c19)) | p($c11) | - p(x) | - q($c20).  [resolve (1078 e 909 c)]

given #326 (wt=16): 1131 p($c19) | p($f1($c19)) | p($c9) | p($f3($c19)) | p($c11) | - p(x) | - q($c20).  [resolve (1129 e 909 c)]

given #327 (wt=14): 2215 p($c9) | p($f1($c9)) | p($c19) | p($f3($c19)) | p($c11) | - p(x).  [resolve (1080 g 1078 e) merge g merge h merge i merge j]

given #328 (wt=14): 2223 p($c19) | p($f1($c19)) | p($c9) | p($f3($c19)) | p($c11) | - p(x).  [resolve (1131 g 1129 e) merge g merge h merge i merge j]

given #329 (wt=16): 1185 p($c19) | p($f1($c19)) | p($c9) | p($f3($c9)) | p($c11) | - p(x) | - q($c20).  [resolve (1183 e 909 c)]

given #330 (wt=14): 2230 p($c19) | p($f1($c19)) | p($c9) | p($f3($c9)) | p($c11) | - p(x).  [resolve (1185 g 1183 e) merge g merge h merge i merge j]

given #331 (wt=16): 1209 p($c9) | p($f1($c9)) | p($c19) | p($c6) | p($c3) | q($c4) | q($f2($c4)).  [resolve (1206 c 902 b)]

given #332 (wt=15): 2233 p($c9) | p($f1($c9)) | p($c19) | p($c6) | p($c3) | q($c4) | q($c8).  [resolve (1209 g 897 c) merge g merge h]

given #333 (wt=13): 2247 p($c9) | p($f1($c9)) | p($c19) | p($c6) | p($c3) | q($c8).  [resolve (2233 f 897 c) merge g merge h merge i]

given #334 (wt=13): 2251 p($c9) | p($f1($c9)) | p($c19) | p($c6) | p($c3) | q(x).  [resolve (2247 f 898 c) merge f merge g]

given #335 (wt=13): 2261 p($c9) | p($f1($c9)) | p($c19) | p($c6) | p($c3) | - q($c7).  [factor (2259 a f) merge f]

given #336 (wt=16): 1235 p($c19) | p($f1($c19)) | p($c9) | p($c6) | p($c3) | q($c4) | q($f2($c4)).  [resolve (1231 d 902 b)]

given #337 (wt=11): 2262 p($c9) | p($f1($c9)) | p($c19) | p($c6) | p($c3).  [resolve (2261 f 2251 f) merge f merge g merge h merge i merge j]

given #338 (wt=13): 2285 p($c9) | p($c19) | p($c6) | p($c3) | q($c4) | q($f2($c4)).  [resolve (2262 b 902 b) merge e]

given #339 (wt=14): 2303 p($c9) | p($c19) | p($c6) | p($c3) | q($c4) | - p(x) | q($c8).  [resolve (2285 f 637 d) merge f merge h merge j]

given #340 (wt=12): 2322 p($c9) | p($c19) | p($c6) | p($c3) | q($c4) | q($c8).  [resolve (2303 f 2262 b) merge g merge h merge i merge j]

given #341 (wt=17): 1264 p($c9) | p($f1($c9)) | p($f3($f1($c9))) | p($c19) | p($c11) | - p(x) | - q($c20).  [resolve (1262 e 909 c)]

given #342 (wt=12): 2329 p($c9) | p($c19) | p($c6) | p($c3) | q($c8) | - p($c5).  [resolve (2322 e 837 c) merge f merge h merge i]

given #343 (wt=13): 2341 p($c9) | p($c19) | p($c6) | p($c3) | q($c8) | p($f1($c19)).  [factor (2331 b f)]

given #344 (wt=13): 2342 p($c9) | p($c19) | p($c6) | p($c3) | q($c8) | p($f1($c6)).  [factor (2331 c f)]

given #345 (wt=13): 2343 p($c9) | p($c19) | p($c6) | p($c3) | q($c8) | p($f1($c3)).  [factor (2331 d f)]

given #346 (wt=17): 1320 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | p($c11) | - p(x) | - q($c20).  [resolve (1318 e 909 c)]

given #347 (wt=13): 2376 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c19)) | q(x).  [factor (2370 b f) merge f]

given #348 (wt=13): 2394 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c6)) | q(x).  [factor (2386 c f) merge f]

given #349 (wt=13): 2411 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c3)) | q(x).  [factor (2404 d f) merge f]

given #350 (wt=13): 2426 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c19)) | - q($c7).  [factor (2424 b f) merge f]

given #351 (wt=17): 1373 p($f3($c19)) | p($f1($f3($c19))) | p($c9) | p($c19) | p($c11) | - p(x) | - q($c20).  [resolve (1371 e 909 c)]

given #352 (wt=11): 2448 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c19)).  [resolve (2426 f 2376 f) merge f merge g merge h merge i merge j]

given #353 (wt=13): 2430 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c6)) | - q($c7).  [resolve (2394 f 896 c) merge f merge g]

given #354 (wt=11): 2454 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c6)).  [resolve (2430 f 2394 f) merge f merge g merge h merge i merge j]

given #355 (wt=13): 2445 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c3)) | - q($c7).  [factor (2442 d f) merge f]

given #356 (wt=17): 1428 p($c19) | p($f1($c19)) | p($c9) | p($f3($f1($c19))) | p($c11) | - p(x) | - q($c20).  [resolve (1426 e 909 c)]

given #357 (wt=11): 2455 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c3)).  [resolve (2445 f 2411 f) merge f merge g merge h merge i merge j]

given #358 (wt=14): 2306 p($c9) | p($c19) | p($c6) | p($c3) | q($c4) | - p($c11) | q($c16).  [factor (2293 a g)]

given #359 (wt=14): 2338 p($c9) | p($c19) | p($c6) | p($c3) | q($c8) | - p($c11) | q($c16).  [factor (2325 a g)]

given #360 (wt=15): 2286 p($c9) | p($c19) | p($c6) | p($c3) | q($c4) | q($f2(x)) | q(x).  [resolve (2262 b 827 b) merge e]

given #361 (wt=20): 1483 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | p($c3) | - p($c5) | q($f2(x)) | q(x).  [resolve (1471 e 834 c)]

given #362 (wt=15): 2289 p($c9) | p($c19) | p($c6) | p($c3) | p($f3($c3)) | q($c14) | q($c16).  [factor (2282 d e)]

given #363 (wt=15): 2308 p($c9) | p($c19) | p($c6) | p($c3) | q($c4) | - p($c11) | q($f4($c4)).  [factor (2296 e h)]

given #364 (wt=15): 2330 p($c9) | p($c19) | p($c6) | p($c3) | q($c8) | - p(x) | - p($f1(x)).  [resolve (2322 e 801 c) merge h merge i]

given #365 (wt=15): 2331 p($c9) | p($c19) | p($c6) | p($c3) | q($c8) | p(x) | p($f1(x)).  [resolve (2322 e 793 c) merge h merge i]

given #366 (wt=17): 1484 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | - p($c3) | - p($c5) | q($c8).  [resolve (1471 e 823 c) merge g]

given #367 (wt=15): 2340 p($c9) | p($c19) | p($c6) | p($c3) | q($c8) | - p($c11) | q($f4($c8)).  [factor (2328 e h)]

given #368 (wt=15): 2361 p($c9) | p($f1($c9)) | p($f3($f1($c9))) | p($c19) | p($c11) | - p(x).  [resolve (1264 g 1262 e) merge g merge h merge i merge j]

given #369 (wt=15): 2416 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | p($c11) | - p(x).  [resolve (1320 g 1318 e) merge g merge h merge i merge j]

given #370 (wt=15): 2452 p($f3($c19)) | p($f1($f3($c19))) | p($c9) | p($c19) | p($c11) | - p(x).  [resolve (1373 g 1371 e) merge g merge h merge i merge j]

given #371 (wt=17): 1485 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | - p($c3) | q($c4) | q($c8).  [resolve (1471 e 817 d) merge g]

given #372 (wt=15): 2459 p($c19) | p($f1($c19)) | p($c9) | p($f3($f1($c19))) | p($c11) | - p(x).  [resolve (1428 g 1426 e) merge g merge h merge i merge j]

given #373 (wt=15): 2469 p($c9) | p($c19) | p($c6) | p($c3) | p($f3($c3)) | q($c16) | - p($c11).  [factor (2462 a h)]

given #374 (wt=15): 2470 p($c9) | p($c19) | p($c6) | p($c3) | p($f3($c3)) | q($c16) | - p($c15).  [factor (2464 d g) merge g]

given #375 (wt=15): 2493 p($c9) | p($c19) | p($c6) | p($c3) | p(x) | p($f1(x)) | q(y).  [factor (2485 e g) merge g]

given #376 (wt=18): 1486 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | - p(x) | - p($f1(x)) | q($c8).  [resolve (1471 e 801 c) merge h]

given #377 (wt=15): 2506 p($c9) | p($c19) | p($c6) | p($c3) | p(x) | p($f1(x)) | - q($c7).  [factor (2501 e g) merge g]

given #378 (wt=13): 2508 p($c9) | p($c19) | p($c6) | p($c3) | p(x) | p($f1(x)).  [factor (2507 e g) merge g]

given #379 (wt=16): 1637 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | q($c4) | - p(x) | q($c16).  [resolve (1604 g 907 c) merge g]

given #380 (wt=14): 2510 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | q($c4) | q($c16).  [resolve (1637 g 2455 e) merge h merge i merge j merge k]

given #381 (wt=18): 1496 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | p($c3) | - p($c5) | q($f2($c16)).  [factor (1483 e i)]

given #382 (wt=14): 2512 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | q($c16) | - p(x).  [resolve (2510 f 907 c) merge g merge i]

given #383 (wt=12): 2514 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | q($c16).  [resolve (2512 g 2455 e) merge g merge h merge i merge j]

given #384 (wt=14): 2516 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | - p(x) | q(y).  [resolve (2514 f 908 c) merge f]

given #385 (wt=12): 2518 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | q(x).  [resolve (2516 f 2455 e) merge g merge h merge i merge j]

given #386 (wt=20): 1498 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | - p($c3) | - p($c5) | q($f2(x)) | q(x).  [factor (1490 a g)]

given #387 (wt=14): 2520 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | - p(x) | - q($c20).  [resolve (2518 f 909 c) merge f]

given #388 (wt=12): 2523 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | - p(x).  [resolve (2520 g 2518 f) merge g merge h merge i merge j merge k]

given #389 (wt=10): 2525 p($c9) | p($c19) | p($c6) | p($c11) | p($c3).  [resolve (2523 f 2455 e) merge f merge g merge h merge i]

given #390 (wt=13): 2546 p($c19) | p($c6) | p($c11) | p($c3) | q($c4) | q($f2($c4)).  [resolve (2525 a 902 b) merge e]

given #391 (wt=21): 1500 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | - p(x) | - p($f1(x)) | q($f2(y)) | q(y).  [factor (1491 a h)]

given #392 (wt=14): 2606 p($c19) | p($c6) | p($c11) | p($c3) | q($c4) | - p(x) | q($c16).  [resolve (2546 f 907 c) merge f]

given #393 (wt=12): 2613 p($c19) | p($c6) | p($c11) | p($c3) | q($c4) | q($c16).  [resolve (2606 f 2525 a) merge g merge h merge i merge j]

given #394 (wt=12): 2615 p($c19) | p($c6) | p($c11) | p($c3) | q($c16) | - p(x).  [resolve (2613 e 907 c) merge f merge h]

given #395 (wt=10): 2616 p($c19) | p($c6) | p($c11) | p($c3) | q($c16).  [resolve (2615 f 2525 a) merge f merge g merge h merge i]

given #396 (wt=18): 1504 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | - p($c3) | - p($c5) | q($f2($c16)).  [factor (1498 e i)]

given #397 (wt=12): 2618 p($c19) | p($c6) | p($c11) | p($c3) | - p(x) | q(y).  [resolve (2616 e 908 c) merge e]

given #398 (wt=10): 2619 p($c19) | p($c6) | p($c11) | p($c3) | q(x).  [resolve (2618 e 2525 a) merge f merge g merge h merge i]

given #399 (wt=12): 2621 p($c19) | p($c6) | p($c11) | p($c3) | - p(x) | - q($c20).  [resolve (2619 e 909 c) merge e]

given #400 (wt=10): 2629 p($c19) | p($c6) | p($c11) | p($c3) | - p(x).  [resolve (2621 f 2619 e) merge f merge g merge h merge i]

given #401 (wt=19): 1505 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | - p(x) | - p($f1(x)) | q($f2($c16)).  [factor (1500 e i)]

given #402 (wt=8): 2630 p($c19) | p($c6) | p($c11) | p($c3).  [resolve (2629 e 2525 a) merge e merge f merge g merge h]

given #403 (wt=11): 2663 p($c19) | p($c11) | p($c3) | q($c4) | q($f2($c4)).  [resolve (2630 b 902 b) merge d]

given #404 (wt=12): 2701 p($c19) | p($c11) | p($c3) | q($c4) | - p(x) | q($c16).  [resolve (2663 e 907 c) merge e]

given #405 (wt=10): 2716 p($c19) | p($c11) | p($c3) | q($c4) | q($c16).  [resolve (2701 e 2630 b) merge f merge g merge h]

given #406 (wt=20): 1530 p($f3($c19)) | p($c9) | p($c19) | p($c6) | q($c16) | p($c3) | - p($c5) | q($f2(x)) | q(x).  [resolve (1512 e 834 c)]

given #407 (wt=10): 2718 p($c19) | p($c11) | p($c3) | q($c16) | - p(x).  [resolve (2716 d 907 c) merge e merge g]

given #408 (wt=8): 2724 p($c19) | p($c11) | p($c3) | q($c16).  [resolve (2718 e 2630 b) merge e merge f merge g]

given #409 (wt=10): 2726 p($c19) | p($c11) | p($c3) | - p(x) | q(y).  [resolve (2724 d 908 c) merge d]

given #410 (wt=8): 2732 p($c19) | p($c11) | p($c3) | q(x).  [resolve (2726 d 2630 b) merge e merge f merge g]

given #411 (wt=17): 1531 p($f3($c19)) | p($c9) | p($c19) | p($c6) | q($c16) | - p($c3) | - p($c5) | q($c8).  [resolve (1512 e 823 c) merge g]

given #412 (wt=10): 2734 p($c19) | p($c11) | p($c3) | - p(x) | - q($c20).  [resolve (2732 d 909 c) merge d]

given #413 (wt=8): 2735 p($c19) | p($c11) | p($c3) | - p(x).  [resolve (2734 e 2732 d) merge e merge f merge g]

given #414 (wt=6): 2736 p($c19) | p($c11) | p($c3).  [resolve (2735 d 2630 b) merge d merge e merge f]

given #415 (wt=9): 2737 p($c11) | p($c3) | q($c4) | q($f2($c4)).  [resolve (2736 a 902 b) merge c]

given #416 (wt=17): 1532 p($f3($c19)) | p($c9) | p($c19) | p($c6) | q($c16) | - p($c3) | q($c4) | q($c8).  [resolve (1512 e 817 d) merge g]

given #417 (wt=10): 2740 p($c11) | p($c3) | q($c4) | - p(x) | q($c16).  [resolve (2737 d 907 c) merge d]

given #418 (wt=8): 2748 p($c11) | p($c3) | q($c4) | q($c16).  [resolve (2740 d 2736 a) merge e merge f]

given #419 (wt=8): 2750 p($c11) | p($c3) | q($c16) | - p(x).  [resolve (2748 c 907 c) merge d merge f]

given #420 (wt=6): 2755 p($c11) | p($c3) | q($c16).  [resolve (2750 d 2736 a) merge d merge e]

given #421 (wt=18): 1533 p($f3($c19)) | p($c9) | p($c19) | p($c6) | q($c16) | - p(x) | - p($f1(x)) | q($c8).  [resolve (1512 e 801 c) merge h]

given #422 (wt=8): 2757 p($c11) | p($c3) | - p(x) | q(y).  [resolve (2755 c 908 c) merge c]

given #423 (wt=6): 2762 p($c11) | p($c3) | q(x).  [resolve (2757 c 2736 a) merge d merge e]

given #424 (wt=8): 2764 p($c11) | p($c3) | - p(x) | - q($c20).  [resolve (2762 c 909 c) merge c]

given #425 (wt=6): 2771 p($c11) | p($c3) | - p(x).  [resolve (2764 d 2762 c) merge d merge e]

given #426 (wt=18): 1543 p($f3($c19)) | p($c9) | p($c19) | p($c6) | q($c16) | p($c3) | - p($c5) | q($f2($c16)).  [factor (1530 e i)]

given #427 (wt=4): 2772 p($c11) | p($c3).  [resolve (2771 c 2736 a) merge c merge d]

given #428 (wt=7): 2822 p($c11) | q($c4) | q($f2($c4)).  [factor (2804 a b)]

given #429 (wt=8): 2825 p($c11) | q($c4) | - p(x) | q($c16).  [resolve (2822 c 907 c) merge c]

given #430 (wt=6): 2838 p($c11) | q($c4) | q($c16).  [resolve (2825 c 2772 b) merge d]

given #431 (wt=20): 1545 p($f3($c19)) | p($c9) | p($c19) | p($c6) | q($c16) | - p($c3) | - p($c5) | q($f2(x)) | q(x).  [factor (1537 a g)]

given #432 (wt=6): 2840 p($c11) | q($c16) | - p(x).  [resolve (2838 b 907 c) merge c merge e]

given #433 (wt=4): 2844 p($c11) | q($c16).  [resolve (2840 c 2772 b) merge c]

given #434 (wt=6): 2846 p($c11) | - p(x) | q(y).  [resolve (2844 b 908 c) merge b]

given #435 (wt=4): 2850 p($c11) | q(x).  [resolve (2846 b 2772 b) merge c]

given #436 (wt=21): 1547 p($f3($c19)) | p($c9) | p($c19) | p($c6) | q($c16) | - p(x) | - p($f1(x)) | q($f2(y)) | q(y).  [factor (1538 a h)]

given #437 (wt=6): 2852 p($c11) | - p(x) | - q($c20).  [resolve (2850 b 909 c) merge b]

given #438 (wt=4): 2858 p($c11) | - p(x).  [resolve (2852 c 2850 b) merge c]

given #439 (wt=2): 2859 p($c11).  [resolve (2858 b 2772 b) merge b]

given #440 (wt=6): 2886 p(x) | - q($c16) | q(y).  [back_unit_del 905 unit_del (a 2859)]

given #441 (wt=16): 1748 p(x) | p($f1(x)) | q($c8) | p($c9) | p(y) | p($f3(y)) | p($c19).  [factor (1670 a h) merge h]

given #442 (wt=6): 2887 p(x) | - q(y) | q($c16).  [back_unit_del 904 unit_del (a 2859)]

given #443 (wt=7): 2885 p(x) | - q($f4($c20)) | - q($c20).  [back_unit_del 906 unit_del (a 2859)]

given #444 (wt=7): 2918 p($c3) | q($c4) | q($f2($c4)).  [resolve (2859 a 902 b)]

given #445 (wt=6): 2941 p($c3) | q($c4) | q($c16).  [factor (2933 a c)]

given #446 (wt=16): 1914 p($c9) | p($f1($c9)) | p(x) | p($f3(x)) | p($c19) | - q($c7) | p($c6).  [factor (1904 a f) merge f]

given #447 (wt=4): 2947 p($c3) | q($c16).  [factor (2943 a c)]

given #448 (wt=4): 2962 p($c3) | q(x).  [factor (2958 a b)]

given #449 (wt=4): 2970 p($c3) | - q($c20).  [factor (2963 a b)]

given #450 (wt=2): 2972 p($c3).  [resolve (2970 b 2962 b) merge b]

given #451 (wt=16): 1932 p(x) | p($f1(x)) | p($c9) | p($f3(x)) | p($c19) | - q($c7) | p($c6).  [factor (1925 a f) merge f]

given #452 (wt=6): 2983 p($c9) | q($c4) | - q($c8).  [back_unit_del 901 unit_del (a 2972)]

given #453 (wt=7): 2984 p(x) | q($c4) | q($f2($c4)).  [back_unit_del 900 unit_del (a 2972)]

given #454 (wt=6): 3022 p(x) | q($c4) | q($c16).  [factor (3016 a c)]

given #455 (wt=4): 3029 p(x) | q($c16).  [factor (3026 a c)]

given #456 (wt=16): 1951 p($c19) | p($f1($c19)) | p($c9) | p(x) | p($f3(x)) | - q($c7) | p($c6).  [factor (1942 a f) merge f]

given #457 (wt=4): 3033 p(x) | q(y).  [factor (3030 a b)]

given #458 (wt=4): 3041 p(x) | - q($c20).  [factor (3034 a b)]

given #459 (wt=2): 3047 p(x).  [factor (3046 a b)]

given #460 (wt=4): 3049 - q($c16) | q(x).  [back_unit_del 912 unit_del (a 3047) unit_del (b 3047)]

given #461 (wt=5): 3048 - q($f4($c20)) | - q($c20).  [back_unit_del 913 unit_del (a 3047) unit_del (b 3047)]

given #462 (wt=7): 3052 - q($f4(x)) | - q(x) | - q($c20).  [back_unit_del 893 unit_del (a 3047) unit_del (b 3047)]

given #463 (wt=4): 3050 - q(x) | q($c16).  [back_unit_del 911 unit_del (a 3047) unit_del (b 3047)]

given #464 (wt=5): 3051 q($c1) | q($f2($c1)).  [back_unit_del 899 unit_del (a 3047) unit_del (b 3047)]

given #465 (wt=4): 3058 q($c1) | q($c16).  [resolve (3051 b 3050 a)]

-------- Proof 1 -------- (0.60 + 0.01 seconds) 

-------- PROOF --------
Length of proof is 235.
Maximum clause weight is 20.
4 p(x) | p($f1(x)) | - q(y) | p(z) | - q($f2(u)) | - q(u) | p($c6) | - q($c7).  [clausify]
5 p(x) | p($f1(x)) | - q(y) | p(z) | - q(u) | q($c8) | p($c9) | q(v).  [clausify]
7 p(x) | p($f1(x)) | - q(y) | p(z) | q(u) | - q($c8) | p($c9) | q(v).  [clausify]
25 - p(x) | - p($f1(x)) | q($c1) | - p($c2) | q($f2(y)) | q(y) | - p(z) | q(u).  [clausify]
33 - p($c3) | p(x) | q($c4) | p(y) | q($f2(z)) | q(z) | - p(u) | q(v).  [clausify]
49 p($c3) | - p(x) | q($c4) | p(y) | q($f2(z)) | q(z) | - p(u) | q(v).  [clausify]
53 p($c3) | - p(x) | q($c4) | p(y) | - q(z) | q($c8) | p($c9) | q(u).  [clausify]
65 - p($c11) | p(x) | - q(y) | p(z) | - q(u) | q($c16) | - p(v) | q(w).  [clausify]
67 - p($c11) | p(x) | - q(y) | p(z) | q(u) | - q($c16) | - p(v) | q(w).  [clausify]
72 - p($c11) | p(x) | - q(y) | p(z) | - q($f4(u)) | - q(u) | - p(v) | - q($c20).  [clausify]
81 p($c11) | - p(x) | - q(y) | p(z) | - q(u) | q($c16) | - p(v) | q(w).  [clausify]
83 p($c11) | - p(x) | - q(y) | p(z) | q(u) | - q($c16) | - p(v) | q(w).  [clausify]
88 p($c11) | - p(x) | - q(y) | p(z) | - q($f4(u)) | - q(u) | - p(v) | - q($c20).  [clausify]
97 p(x) | p($f3(x)) | q($c14) | p(y) | - q(z) | q($c16) | - p(u) | q(v).  [clausify]
101 p(x) | p($f3(x)) | q($c14) | p(y) | q($f4(z)) | q(z) | p($c19) | q(u).  [clausify]
121 - p(x) | - p($f3(x)) | - q(y) | - p($c15) | - q(z) | q($c16) | - p(u) | q(v).  [clausify]
123 - p(x) | - p($f3(x)) | - q(y) | - p($c15) | q(z) | - q($c16) | - p(u) | q(v).  [clausify]
128 - p(x) | - p($f3(x)) | - q(y) | - p($c15) | - q($f4(z)) | - q(z) | - p(u) | - q($c20).  [clausify]
132 p(x) | p($f1(x)) | - q(y) | p(z) | - q($f2(u)) | - q(u) | p($c6) | - q($c7).  [copy 4]
133 p(x) | p($f1(x)) | - q(y) | p(z) | - q(u) | q($c8) | p($c9) | q(v).  [copy 5]
135 p(x) | p($f1(x)) | - q(y) | p(z) | q(u) | - q($c8) | p($c9) | q(v).  [copy 7]
151 - p(x) | - p($f1(x)) | q($c1) | - p($c2) | q($f2(y)) | q(y) | - p(z) | q(u).  [copy 25]
157 - p($c3) | p(x) | q($c4) | p(y) | q($f2(z)) | q(z) | - p(u) | q(v).  [copy 33]
173 p($c3) | - p(x) | q($c4) | p(y) | q($f2(z)) | q(z) | - p(u) | q(v).  [copy 49]
177 p($c3) | - p(x) | q($c4) | p(y) | - q(z) | q($c8) | p($c9) | q(u).  [copy 53]
189 - p($c11) | p(x) | - q(y) | p(z) | - q(u) | q($c16) | - p(v) | q(w).  [copy 65]
191 - p($c11) | p(x) | - q(y) | p(z) | q(u) | - q($c16) | - p(v) | q(w).  [copy 67]
196 - p($c11) | p(x) | - q(y) | p(z) | - q($f4(u)) | - q(u) | - p(v) | - q($c20).  [copy 72]
203 p($c11) | - p(x) | - q(y) | p(z) | - q(u) | q($c16) | - p(v) | q(w).  [copy 81]
205 p($c11) | - p(x) | - q(y) | p(z) | q(u) | - q($c16) | - p(v) | q(w).  [copy 83]
210 p($c11) | - p(x) | - q(y) | p(z) | - q($f4(u)) | - q(u) | - p(v) | - q($c20).  [copy 88]
217 p(x) | p($f3(x)) | q($c14) | p(y) | - q(z) | q($c16) | - p(u) | q(v).  [copy 97]
221 p(x) | p($f3(x)) | q($c14) | p(y) | q($f4(z)) | q(z) | p($c19) | q(u).  [copy 101]
241 - p(x) | - p($f3(x)) | - q(y) | - p($c15) | - q(z) | q($c16) | - p(u) | q(v).  [copy 121]
243 - p(x) | - p($f3(x)) | - q(y) | - p($c15) | q(z) | - q($c16) | - p(u) | q(v).  [copy 123]
248 - p(x) | - p($f3(x)) | - q(y) | - p($c15) | - q($f4(z)) | - q(z) | - p(u) | - q($c20).  [copy 128]
255 p(x) | p($f1(x)) | - q(y) | - q($f2(z)) | - q(z) | p($c6) | - q($c7).  [factor (132 a d)]
257 p(x) | p($f1(x)) | - q(y) | - q(z) | q($c8) | p($c9) | q(u).  [factor (133 a d)]
262 p(x) | p($f1(x)) | - q(y) | q(z) | - q($c8) | p($c9) | q(u).  [factor (135 a d)]
298 - p($c2) | - p($f1($c2)) | q($c1) | q($f2(x)) | q(x) | - p(y) | q(z).  [factor (151 a d)]
315 - p($c3) | p(x) | q($c4) | p(y) | q($f2(z)) | q(z) | q(u).  [factor (157 a g)]
354 p($c3) | - p(x) | q($c4) | q($f2(y)) | q(y) | - p(z) | q(u).  [factor (173 a d)]
365 p($c3) | - p(x) | q($c4) | - q(y) | q($c8) | p($c9) | q(z).  [factor (177 a d)]
393 - p($c11) | p(x) | - q(y) | p(z) | - q(u) | q($c16) | q(v).  [factor (189 a g)]
399 - p($c11) | p(x) | - q(y) | p(z) | q(u) | - q($c16) | q(v).  [factor (191 a g)]
412 - p($c11) | p(x) | - q(y) | p(z) | - q($f4(u)) | - q(u) | - q($c20).  [factor (196 a g)]
428 p($c11) | - p(x) | - q(y) | - q(z) | q($c16) | - p(u) | q(v).  [factor (203 a d)]
434 p($c11) | - p(x) | - q(y) | q(z) | - q($c16) | - p(u) | q(v).  [factor (205 a d)]
447 p($c11) | - p(x) | - q(y) | - q($f4(z)) | - q(z) | - p(u) | - q($c20).  [factor (210 a d)]
463 p(x) | p($f3(x)) | q($c14) | - q(y) | q($c16) | - p(z) | q(u).  [factor (217 a d)]
471 p(x) | p($f3(x)) | q($c14) | q($f4(y)) | q(y) | p($c19) | q(z).  [factor (221 a d)]
515 - p($c15) | - p($f3($c15)) | - q(x) | - q(y) | q($c16) | - p(z) | q(u).  [factor (241 a d)]
521 - p($c15) | - p($f3($c15)) | - q(x) | q(y) | - q($c16) | - p(z) | q(u).  [factor (243 a d)]
534 - p($c15) | - p($f3($c15)) | - q(x) | - q($f4(y)) | - q(y) | - p(z) | - q($c20).  [factor (248 a d)]
542 p(x) | p($f1(x)) | - q($f2(y)) | - q(y) | p($c6) | - q($c7).  [factor (255 c d)]
544 p($c9) | p($f1($c9)) | - q(x) | - q(y) | q($c8) | q(z).  [factor (257 a f)]
545 p(x) | p($f1(x)) | - q(y) | q($c8) | p($c9) | q(z).  [factor (257 c d)]
550 p($c9) | p($f1($c9)) | - q(x) | q(y) | - q($c8) | q(z).  [factor (262 a f)]
551 p(x) | p($f1(x)) | - q($c8) | q(y) | p($c9) | q(z).  [factor (262 c e)]
575 - p($c2) | - p($f1($c2)) | q($c1) | q($f2(x)) | q(x) | q(y).  [factor (298 a f)]
591 - p($c3) | p(x) | q($c4) | q($f2(y)) | q(y) | q(z).  [factor (315 b d)]
627 p($c3) | - p(x) | q($c4) | q($f2(y)) | q(y) | q(z).  [factor (354 b f)]
637 p($c3) | - p(x) | q($c4) | - q(y) | q($c8) | p($c9).  [factor (365 c g)]
664 - p($c11) | p(x) | - q(y) | - q(z) | q($c16) | q(u).  [factor (393 b d)]
672 - p($c11) | p(x) | - q(y) | q(z) | - q($c16) | q(u).  [factor (399 b d)]
686 - p($c11) | p(x) | - q(y) | - q($f4(z)) | - q(z) | - q($c20).  [factor (412 b d)]
696 p($c11) | - p(x) | - q(y) | - q(z) | q($c16) | q(u).  [factor (428 b f)]
703 p($c11) | - p(x) | - q(y) | q(z) | - q($c16) | q(u).  [factor (434 b f)]
714 p($c11) | - p(x) | - q(y) | - q($f4(z)) | - q(z) | - q($c20).  [factor (447 b f)]
727 p(x) | p($f3(x)) | q($c14) | - q(y) | q($c16) | - p(z).  [factor (463 c g)]
736 p(x) | p($f3(x)) | q($c14) | q($f4(y)) | q(y) | p($c19).  [factor (471 c g)]
764 - p($c15) | - p($f3($c15)) | - q(x) | - q(y) | q($c16) | q(z).  [factor (515 a f)]
772 - p($c15) | - p($f3($c15)) | - q(x) | q(y) | - q($c16) | q(z).  [factor (521 a f)]
784 - p($c15) | - p($f3($c15)) | - q(x) | - q($f4(y)) | - q(y) | - q($c20).  [factor (534 a f)]
790 p(x) | p($f1(x)) | - q($f2($c7)) | - q($c7) | p($c6).  [factor (542 d f)]
791 p($c9) | p($f1($c9)) | - q(x) | q($c8) | q(y).  [factor (544 c d)]
793 p(x) | p($f1(x)) | - q(y) | q($c8) | p($c9).  [factor (545 d f)]
795 p($c9) | p($f1($c9)) | - q($c8) | q(x) | q(y).  [factor (550 c e)]
797 p(x) | p($f1(x)) | - q($c8) | q(y) | p($c9).  [factor (551 d f)]
804 - p($c2) | - p($f1($c2)) | q($c1) | q($f2($c1)) | q(x).  [factor (575 c e)]
811 - p($c3) | p(x) | q($c4) | q($f2($c4)) | q(y).  [factor (591 c e)]
826 p($c3) | - p(x) | q($c4) | q($f2($c4)) | q(y).  [factor (627 c e)]
842 - p($c11) | p(x) | - q(y) | q($c16) | q(z).  [factor (664 c d)]
846 - p($c11) | p(x) | - q($c16) | q(y) | q(z).  [factor (672 c e)]
853 - p($c11) | p(x) | - q($f4(y)) | - q(y) | - q($c20).  [factor (686 c d)]
857 p($c11) | - p(x) | - q(y) | q($c16) | q(z).  [factor (696 c d)]
861 p($c11) | - p(x) | - q($c16) | q(y) | q(z).  [factor (703 c e)]
866 p($c11) | - p(x) | - q($f4(y)) | - q(y) | - q($c20).  [factor (714 c d)]
883 - p($c15) | - p($f3($c15)) | - q(x) | q($c16) | q(y).  [factor (764 c d)]
888 - p($c15) | - p($f3($c15)) | - q($c16) | q(x) | q(y).  [factor (772 c e)]
893 - p($c15) | - p($f3($c15)) | - q($f4(x)) | - q(x) | - q($c20).  [factor (784 c d)]
897 p($c9) | p($f1($c9)) | - q(x) | q($c8).  [factor (791 d e)]
898 p($c9) | p($f1($c9)) | - q($c8) | q(x).  [factor (795 d e)]
899 - p($c2) | - p($f1($c2)) | q($c1) | q($f2($c1)).  [factor (804 c e)]
900 - p($c3) | p(x) | q($c4) | q($f2($c4)).  [factor (811 c e)]
902 p($c3) | - p(x) | q($c4) | q($f2($c4)).  [factor (826 c e)]
904 - p($c11) | p(x) | - q(y) | q($c16).  [factor (842 d e)]
905 - p($c11) | p(x) | - q($c16) | q(y).  [factor (846 d e)]
906 - p($c11) | p(x) | - q($f4($c20)) | - q($c20).  [factor (853 d e)]
907 p($c11) | - p(x) | - q(y) | q($c16).  [factor (857 d e)]
908 p($c11) | - p(x) | - q($c16) | q(y).  [factor (861 d e)]
909 p($c11) | - p(x) | - q($f4($c20)) | - q($c20).  [factor (866 d e)]
911 - p($c15) | - p($f3($c15)) | - q(x) | q($c16).  [factor (883 d e)]
912 - p($c15) | - p($f3($c15)) | - q($c16) | q(x).  [factor (888 d e)]
914 p(x) | p($f3(x)) | q($c14) | q(y) | p($c19) | p(z) | p($f3(z)) | q($c16) | - p(u).  [resolve (736 d 727 d) merge h]
920 p(x) | p($f3(x)) | q($c14) | q(y) | p($c19) | q($c16) | - p(z).  [factor (914 a f) merge f]
940 p(x) | p($f3(x)) | q($c14) | p($c19) | q($c16) | - p(y).  [factor (920 c d)]
981 p(x) | p($f1(x)) | q($c8) | p($c9) | p(y) | p($f3(y)) | q($c14) | q(z) | p($c19).  [resolve (793 c 736 d)]
982 p($c9) | p($f1($c9)) | q($c8) | p(x) | p($f3(x)) | q($c14) | q(y) | p($c19).  [factor (981 a d)]
984 p($f3(x)) | p($f1($f3(x))) | q($c8) | p($c9) | p(x) | q($c14) | q(y) | p($c19).  [factor (981 a f)]
990 p($c9) | p($f1($c9)) | q($c8) | p($f3($c9)) | q($c14) | q(x) | p($c19).  [factor (982 a d)]
996 p($f3(x)) | p($f1($f3(x))) | q($c8) | p($c9) | p(x) | q($c14) | p($c19).  [factor (984 c g)]
1005 p($c9) | p($f1($c9)) | q($c8) | p($f3($c9)) | q($c14) | p($c19).  [factor (990 c f)]
1009 p($f3($c9)) | p($f1($f3($c9))) | q($c8) | p($c9) | q($c14) | p($c19).  [factor (996 d e)]
1051 p($c9) | p($f1($c9)) | q($c8) | p($f3($c9)) | p($c19).  [resolve (1005 e 897 c) merge f merge g merge h]
1056 p($c9) | p($f1($c9)) | p($f3($c9)) | p($c19) | q(x).  [resolve (1051 c 898 c) merge e merge f]
1066 p($c9) | p($f1($c9)) | p($f3($c9)) | p($c19) | p(x) | p($f1(x)) | - q($c7) | p($c6).  [resolve (1056 e 790 c)]
1069 p($c9) | p($f1($c9)) | p($f3($c9)) | p($c19) | - q($c7) | p($c6).  [factor (1066 a e) merge e]
1206 p($c9) | p($f1($c9)) | p($f3($c9)) | p($c19) | p($c6).  [resolve (1069 e 1056 e) merge f merge g merge h merge i]
1209 p($c9) | p($f1($c9)) | p($c19) | p($c6) | p($c3) | q($c4) | q($f2($c4)).  [resolve (1206 c 902 b)]
1286 p($f3($c9)) | p($f1($f3($c9))) | q($c8) | p($c9) | p($c19) | p(x) | p($f1(x)).  [resolve (1009 e 793 c) merge h merge i]
1297 p($f3($c9)) | p($f1($f3($c9))) | q($c8) | p($c9) | p($c19).  [factor (1286 a f) merge f]
1309 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | p(x) | p($f1(x)) | q(y).  [resolve (1297 c 797 c) merge h]
1318 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | q(x).  [factor (1309 a e) merge e]
1328 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | p(x) | p($f1(x)) | - q($c7) | p($c6).  [resolve (1318 e 790 c)]
1332 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | - q($c7) | p($c6).  [factor (1328 a e) merge e]
1451 p($f3($c9)) | p($f1($f3($c9))) | p($c9) | p($c19) | p($c6).  [resolve (1332 e 1318 e) merge f merge g merge h merge i]
1459 p($f3($c9)) | p($c9) | p($c19) | p($c6) | p(x) | p($f3(x)) | q($c14) | q($c16).  [resolve (1451 b 940 f) merge h]
1471 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c14) | q($c16).  [factor (1459 a f) merge e]
1477 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | p($c11) | - p(x).  [resolve (1471 e 907 c) merge h]
1558 p($f3($c9)) | p($c9) | p($c19) | p($c6) | q($c16) | p($c11).  [resolve (1477 g 1451 b) merge g merge h merge i merge j]
1560 p($f3($c9)) | p($c9) | p($c19) | p($c6) | p($c11) | - p(x) | q(y).  [resolve (1558 e 908 c) merge f]
1571 p($f3($c9)) | p($c9) | p($c19) | p($c6) | p($c11) | q(x).  [resolve (1560 f 1451 b) merge g merge h merge i merge j]
1573 p($f3($c9)) | p($c9) | p($c19) | p($c6) | p($c11) | - p(x) | - q($c20).  [resolve (1571 f 909 c) merge f]
1590 p($f3($c9)) | p($c9) | p($c19) | p($c6) | p($c11) | - p(x).  [resolve (1573 g 1571 f) merge g merge h merge i merge j merge k]
1592 p($f3($c9)) | p($c9) | p($c19) | p($c6) | p($c11).  [resolve (1590 f 1451 b) merge f merge g merge h merge i]
1604 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | q($c4) | q($f2($c4)).  [resolve (1592 a 902 b)]
1637 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | q($c4) | - p(x) | q($c16).  [resolve (1604 g 907 c) merge g]
2233 p($c9) | p($f1($c9)) | p($c19) | p($c6) | p($c3) | q($c4) | q($c8).  [resolve (1209 g 897 c) merge g merge h]
2247 p($c9) | p($f1($c9)) | p($c19) | p($c6) | p($c3) | q($c8).  [resolve (2233 f 897 c) merge g merge h merge i]
2251 p($c9) | p($f1($c9)) | p($c19) | p($c6) | p($c3) | q(x).  [resolve (2247 f 898 c) merge f merge g]
2259 p($c9) | p($f1($c9)) | p($c19) | p($c6) | p($c3) | p(x) | p($f1(x)) | - q($c7).  [resolve (2251 f 790 c) merge i]
2261 p($c9) | p($f1($c9)) | p($c19) | p($c6) | p($c3) | - q($c7).  [factor (2259 a f) merge f]
2262 p($c9) | p($f1($c9)) | p($c19) | p($c6) | p($c3).  [resolve (2261 f 2251 f) merge f merge g merge h merge i merge j]
2285 p($c9) | p($c19) | p($c6) | p($c3) | q($c4) | q($f2($c4)).  [resolve (2262 b 902 b) merge e]
2303 p($c9) | p($c19) | p($c6) | p($c3) | q($c4) | - p(x) | q($c8).  [resolve (2285 f 637 d) merge f merge h merge j]
2322 p($c9) | p($c19) | p($c6) | p($c3) | q($c4) | q($c8).  [resolve (2303 f 2262 b) merge g merge h merge i merge j]
2331 p($c9) | p($c19) | p($c6) | p($c3) | q($c8) | p(x) | p($f1(x)).  [resolve (2322 e 793 c) merge h merge i]
2343 p($c9) | p($c19) | p($c6) | p($c3) | q($c8) | p($f1($c3)).  [factor (2331 d f)]
2404 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c3)) | p(x) | p($f1(x)) | q(y).  [resolve (2343 e 797 c) merge i]
2411 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c3)) | q(x).  [factor (2404 d f) merge f]
2442 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c3)) | p(x) | p($f1(x)) | - q($c7).  [resolve (2411 f 790 c) merge i]
2445 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c3)) | - q($c7).  [factor (2442 d f) merge f]
2455 p($c9) | p($c19) | p($c6) | p($c3) | p($f1($c3)).  [resolve (2445 f 2411 f) merge f merge g merge h merge i merge j]
2510 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | q($c4) | q($c16).  [resolve (1637 g 2455 e) merge h merge i merge j merge k]
2512 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | q($c16) | - p(x).  [resolve (2510 f 907 c) merge g merge i]
2514 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | q($c16).  [resolve (2512 g 2455 e) merge g merge h merge i merge j]
2516 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | - p(x) | q(y).  [resolve (2514 f 908 c) merge f]
2518 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | q(x).  [resolve (2516 f 2455 e) merge g merge h merge i merge j]
2520 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | - p(x) | - q($c20).  [resolve (2518 f 909 c) merge f]
2523 p($c9) | p($c19) | p($c6) | p($c11) | p($c3) | - p(x).  [resolve (2520 g 2518 f) merge g merge h merge i merge j merge k]
2525 p($c9) | p($c19) | p($c6) | p($c11) | p($c3).  [resolve (2523 f 2455 e) merge f merge g merge h merge i]
2546 p($c19) | p($c6) | p($c11) | p($c3) | q($c4) | q($f2($c4)).  [resolve (2525 a 902 b) merge e]
2606 p($c19) | p($c6) | p($c11) | p($c3) | q($c4) | - p(x) | q($c16).  [resolve (2546 f 907 c) merge f]
2613 p($c19) | p($c6) | p($c11) | p($c3) | q($c4) | q($c16).  [resolve (2606 f 2525 a) merge g merge h merge i merge j]
2615 p($c19) | p($c6) | p($c11) | p($c3) | q($c16) | - p(x).  [resolve (2613 e 907 c) merge f merge h]
2616 p($c19) | p($c6) | p($c11) | p($c3) | q($c16).  [resolve (2615 f 2525 a) merge f merge g merge h merge i]
2618 p($c19) | p($c6) | p($c11) | p($c3) | - p(x) | q(y).  [resolve (2616 e 908 c) merge e]
2619 p($c19) | p($c6) | p($c11) | p($c3) | q(x).  [resolve (2618 e 2525 a) merge f merge g merge h merge i]
2621 p($c19) | p($c6) | p($c11) | p($c3) | - p(x) | - q($c20).  [resolve (2619 e 909 c) merge e]
2629 p($c19) | p($c6) | p($c11) | p($c3) | - p(x).  [resolve (2621 f 2619 e) merge f merge g merge h merge i]
2630 p($c19) | p($c6) | p($c11) | p($c3).  [resolve (2629 e 2525 a) merge e merge f merge g merge h]
2663 p($c19) | p($c11) | p($c3) | q($c4) | q($f2($c4)).  [resolve (2630 b 902 b) merge d]
2701 p($c19) | p($c11) | p($c3) | q($c4) | - p(x) | q($c16).  [resolve (2663 e 907 c) merge e]
2716 p($c19) | p($c11) | p($c3) | q($c4) | q($c16).  [resolve (2701 e 2630 b) merge f merge g merge h]
2718 p($c19) | p($c11) | p($c3) | q($c16) | - p(x).  [resolve (2716 d 907 c) merge e merge g]
2724 p($c19) | p($c11) | p($c3) | q($c16).  [resolve (2718 e 2630 b) merge e merge f merge g]
2726 p($c19) | p($c11) | p($c3) | - p(x) | q(y).  [resolve (2724 d 908 c) merge d]
2732 p($c19) | p($c11) | p($c3) | q(x).  [resolve (2726 d 2630 b) merge e merge f merge g]
2734 p($c19) | p($c11) | p($c3) | - p(x) | - q($c20).  [resolve (2732 d 909 c) merge d]
2735 p($c19) | p($c11) | p($c3) | - p(x).  [resolve (2734 e 2732 d) merge e merge f merge g]
2736 p($c19) | p($c11) | p($c3).  [resolve (2735 d 2630 b) merge d merge e merge f]
2737 p($c11) | p($c3) | q($c4) | q($f2($c4)).  [resolve (2736 a 902 b) merge c]
2740 p($c11) | p($c3) | q($c4) | - p(x) | q($c16).  [resolve (2737 d 907 c) merge d]
2748 p($c11) | p($c3) | q($c4) | q($c16).  [resolve (2740 d 2736 a) merge e merge f]
2750 p($c11) | p($c3) | q($c16) | - p(x).  [resolve (2748 c 907 c) merge d merge f]
2755 p($c11) | p($c3) | q($c16).  [resolve (2750 d 2736 a) merge d merge e]
2757 p($c11) | p($c3) | - p(x) | q(y).  [resolve (2755 c 908 c) merge c]
2762 p($c11) | p($c3) | q(x).  [resolve (2757 c 2736 a) merge d merge e]
2764 p($c11) | p($c3) | - p(x) | - q($c20).  [resolve (2762 c 909 c) merge c]
2771 p($c11) | p($c3) | - p(x).  [resolve (2764 d 2762 c) merge d merge e]
2772 p($c11) | p($c3).  [resolve (2771 c 2736 a) merge c merge d]
2804 p($c11) | p(x) | q($c4) | q($f2($c4)).  [resolve (2772 b 900 a)]
2822 p($c11) | q($c4) | q($f2($c4)).  [factor (2804 a b)]
2825 p($c11) | q($c4) | - p(x) | q($c16).  [resolve (2822 c 907 c) merge c]
2838 p($c11) | q($c4) | q($c16).  [resolve (2825 c 2772 b) merge d]
2840 p($c11) | q($c16) | - p(x).  [resolve (2838 b 907 c) merge c merge e]
2844 p($c11) | q($c16).  [resolve (2840 c 2772 b) merge c]
2846 p($c11) | - p(x) | q(y).  [resolve (2844 b 908 c) merge b]
2850 p($c11) | q(x).  [resolve (2846 b 2772 b) merge c]
2852 p($c11) | - p(x) | - q($c20).  [resolve (2850 b 909 c) merge b]
2858 p($c11) | - p(x).  [resolve (2852 c 2850 b) merge c]
2859 p($c11).  [resolve (2858 b 2772 b) merge b]
2885 p(x) | - q($f4($c20)) | - q($c20).  [back_unit_del 906 unit_del (a 2859)]
2886 p(x) | - q($c16) | q(y).  [back_unit_del 905 unit_del (a 2859)]
2887 p(x) | - q(y) | q($c16).  [back_unit_del 904 unit_del (a 2859)]
2918 p($c3) | q($c4) | q($f2($c4)).  [resolve (2859 a 902 b)]
2933 p($c3) | q($c4) | p(x) | q($c16).  [resolve (2918 c 2887 b)]
2941 p($c3) | q($c4) | q($c16).  [factor (2933 a c)]
2943 p($c3) | q($c16) | p(x).  [resolve (2941 b 2887 b) merge d]
2947 p($c3) | q($c16).  [factor (2943 a c)]
2958 p($c3) | p(x) | q(y).  [resolve (2947 b 2886 b)]
2962 p($c3) | q(x).  [factor (2958 a b)]
2963 p($c3) | p(x) | - q($c20).  [resolve (2962 b 2885 b)]
2970 p($c3) | - q($c20).  [factor (2963 a b)]
2972 p($c3).  [resolve (2970 b 2962 b) merge b]
2984 p(x) | q($c4) | q($f2($c4)).  [back_unit_del 900 unit_del (a 2972)]
3016 p(x) | q($c4) | p(y) | q($c16).  [resolve (2984 c 2887 b)]
3022 p(x) | q($c4) | q($c16).  [factor (3016 a c)]
3026 p(x) | q($c16) | p(y).  [resolve (3022 b 2887 b) merge d]
3029 p(x) | q($c16).  [factor (3026 a c)]
3030 p(x) | p(y) | q(z).  [resolve (3029 b 2886 b)]
3033 p(x) | q(y).  [factor (3030 a b)]
3034 p(x) | p(y) | - q($c20).  [resolve (3033 b 2885 b)]
3041 p(x) | - q($c20).  [factor (3034 a b)]
3046 p(x) | p(y).  [resolve (3041 b 3033 b)]
3047 p(x).  [factor (3046 a b)]
3049 - q($c16) | q(x).  [back_unit_del 912 unit_del (a 3047) unit_del (b 3047)]
3050 - q(x) | q($c16).  [back_unit_del 911 unit_del (a 3047) unit_del (b 3047)]
3051 q($c1) | q($f2($c1)).  [back_unit_del 899 unit_del (a 3047) unit_del (b 3047)]
3052 - q($f4(x)) | - q(x) | - q($c20).  [back_unit_del 893 unit_del (a 3047) unit_del (b 3047)]
3058 q($c1) | q($c16).  [resolve (3051 b 3050 a)]
3059 q($c16).  [resolve (3058 a 3050 a) merge b]
3060 q(x).  [back_unit_del 3049 unit_del (a 3059)]
3061 $F.  [back_unit_del 3052 unit_del (a 3060) unit_del (b 3060) unit_del (c 3060)]

-------- end of proof  -------

Given=465. Generated=14297. Kept=2932. Proofs=1.
Usable=2. Sos=0. Demods=0. Goals=0. Limbo=1, Disabled=3057. Hints=0.
Weight_deleted=0. Literals_deleted=0.
Forward_subsumed=11364. Back_subsumed=2848.
Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=81.
Demod_attempts=0. Demod_rewrites=0.
Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
Nonunit_fsub_feature_tests=16763. Nonunit_bsub_feature_tests=6559.
Megabytes=1.08.
User_CPU=0.60, System_CPU=0.01, Wall_clock=0.

THEOREM PROVED

Exiting with 1 proof.

Process 31031 exit (max_proofs) Tue Aug  9 14:15:34 2005