%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LCL686+1.010 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art05.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 15:52:10 EST 2010
% Result : Theorem 1.01s
% Output : Solution 1.01s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP2373/LCL686+1.010.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP2373/LCL686+1.010.tptp
% SZS output start Solution for /tmp/SystemOnTPTP2373/LCL686+1.010.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 2469
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.029 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:r1(X1,X1),file('/tmp/SRASS.s.p', reflexivity)).
% fof(3, conjecture,~(?[X1]:~((![X2]:((~(r1(X1,X2))|~(p30(X2)))|![X1]:(~(r1(X2,X1))|~(p1(X1))))|![X2]:(~(r1(X1,X2))|~(![X1]:(~(r1(X2,X1))|~((((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|~($true)))|~(![X1]:(~(r1(X2,X1))|~(((p29(X1)&~(p28(X1)))|(~(p29(X1))&p28(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p28(X2)&~(p27(X2)))|(~(p28(X2))&p27(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p27(X1)&~(p26(X1)))|(~(p27(X1))&p26(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p26(X2)&~(p25(X2)))|(~(p26(X2))&p25(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p25(X1)&~(p24(X1)))|(~(p25(X1))&p24(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p24(X2)&~(p23(X2)))|(~(p24(X2))&p23(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p23(X1)&~(p22(X1)))|(~(p23(X1))&p22(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p22(X2)&~(p21(X2)))|(~(p22(X2))&p21(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p21(X1)&~(p20(X1)))|(~(p21(X1))&p20(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p20(X2)&~(p19(X2)))|(~(p20(X2))&p19(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p19(X1)&~(p18(X1)))|(~(p19(X1))&p18(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p18(X2)&~(p17(X2)))|(~(p18(X2))&p17(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p17(X1)&~(p16(X1)))|(~(p17(X1))&p16(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p16(X2)&~(p15(X2)))|(~(p16(X2))&p15(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p15(X1)&~(p14(X1)))|(~(p15(X1))&p14(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p14(X2)&~(p13(X2)))|(~(p14(X2))&p13(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p13(X1)&~(p12(X1)))|(~(p13(X1))&p12(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p12(X2)&~(p11(X2)))|(~(p12(X2))&p11(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p11(X1)&~(p10(X1)))|(~(p11(X1))&p10(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p10(X2)&~(p9(X2)))|(~(p10(X2))&p9(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p9(X1)&~(p8(X1)))|(~(p9(X1))&p8(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p8(X2)&~(p7(X2)))|(~(p8(X2))&p7(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p7(X1)&~(p6(X1)))|(~(p7(X1))&p6(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p6(X2)&~(p5(X2)))|(~(p6(X2))&p5(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p5(X1)&~(p4(X1)))|(~(p5(X1))&p4(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p4(X2)&~(p3(X2)))|(~(p4(X2))&p3(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p3(X1)&~(p2(X1)))|(~(p3(X1))&p2(X1)))))))|~(![X2]:(~(r1(X1,X2))|~(((p2(X2)&~(p1(X2)))|(~(p2(X2))&p1(X2)))))))|![X2]:(~(r1(X1,X2))|p30(X2)))|![X2]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((~(r1(X1,X2))|(~(p28(X2))&~(p29(X2))))|(p29(X2)&p28(X2)))|(~(p27(X2))&~(p28(X2))))|(p28(X2)&p27(X2)))|(~(p26(X2))&~(p27(X2))))|(p27(X2)&p26(X2)))|(~(p25(X2))&~(p26(X2))))|(p26(X2)&p25(X2)))|(~(p24(X2))&~(p25(X2))))|(p25(X2)&p24(X2)))|(~(p23(X2))&~(p24(X2))))|(p24(X2)&p23(X2)))|(~(p22(X2))&~(p23(X2))))|(p23(X2)&p22(X2)))|(~(p21(X2))&~(p22(X2))))|(p22(X2)&p21(X2)))|(~(p20(X2))&~(p21(X2))))|(p21(X2)&p20(X2)))|(~(p19(X2))&~(p20(X2))))|(p20(X2)&p19(X2)))|(~(p18(X2))&~(p19(X2))))|(p19(X2)&p18(X2)))|(~(p17(X2))&~(p18(X2))))|(p18(X2)&p17(X2)))|(~(p16(X2))&~(p17(X2))))|(p17(X2)&p16(X2)))|(~(p15(X2))&~(p16(X2))))|(p16(X2)&p15(X2)))|(~(p14(X2))&~(p15(X2))))|(p15(X2)&p14(X2)))|(~(p13(X2))&~(p14(X2))))|(p14(X2)&p13(X2)))|(~(p12(X2))&~(p13(X2))))|(p13(X2)&p12(X2)))|(~(p11(X2))&~(p12(X2))))|(p12(X2)&p11(X2)))|(~(p10(X2))&~(p11(X2))))|(p11(X2)&p10(X2)))|(~(p9(X2))&~(p10(X2))))|(p10(X2)&p9(X2)))|(~(p8(X2))&~(p9(X2))))|(p9(X2)&p8(X2)))|(~(p7(X2))&~(p8(X2))))|(p8(X2)&p7(X2)))|(~(p6(X2))&~(p7(X2))))|(p7(X2)&p6(X2)))|(~(p5(X2))&~(p6(X2))))|(p6(X2)&p5(X2)))|(~(p4(X2))&~(p5(X2))))|(p5(X2)&p4(X2)))|(~(p3(X2))&~(p4(X2))))|(p4(X2)&p3(X2)))|(~(p2(X2))&~(p3(X2))))|(p3(X2)&p2(X2)))|(~(p1(X2))&~(p2(X2))))|(p2(X2)&p1(X2))))))))))),file('/tmp/SRASS.s.p', main)).
% fof(4, negated_conjecture,~(~(?[X1]:~((![X2]:((~(r1(X1,X2))|~(p30(X2)))|![X1]:(~(r1(X2,X1))|~(p1(X1))))|![X2]:(~(r1(X1,X2))|~(![X1]:(~(r1(X2,X1))|~((((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:(~(r1(X2,X1))|~($true)))|~(![X1]:(~(r1(X2,X1))|~(((p29(X1)&~(p28(X1)))|(~(p29(X1))&p28(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p28(X2)&~(p27(X2)))|(~(p28(X2))&p27(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p27(X1)&~(p26(X1)))|(~(p27(X1))&p26(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p26(X2)&~(p25(X2)))|(~(p26(X2))&p25(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p25(X1)&~(p24(X1)))|(~(p25(X1))&p24(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p24(X2)&~(p23(X2)))|(~(p24(X2))&p23(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p23(X1)&~(p22(X1)))|(~(p23(X1))&p22(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p22(X2)&~(p21(X2)))|(~(p22(X2))&p21(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p21(X1)&~(p20(X1)))|(~(p21(X1))&p20(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p20(X2)&~(p19(X2)))|(~(p20(X2))&p19(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p19(X1)&~(p18(X1)))|(~(p19(X1))&p18(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p18(X2)&~(p17(X2)))|(~(p18(X2))&p17(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p17(X1)&~(p16(X1)))|(~(p17(X1))&p16(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p16(X2)&~(p15(X2)))|(~(p16(X2))&p15(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p15(X1)&~(p14(X1)))|(~(p15(X1))&p14(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p14(X2)&~(p13(X2)))|(~(p14(X2))&p13(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p13(X1)&~(p12(X1)))|(~(p13(X1))&p12(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p12(X2)&~(p11(X2)))|(~(p12(X2))&p11(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p11(X1)&~(p10(X1)))|(~(p11(X1))&p10(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p10(X2)&~(p9(X2)))|(~(p10(X2))&p9(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p9(X1)&~(p8(X1)))|(~(p9(X1))&p8(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p8(X2)&~(p7(X2)))|(~(p8(X2))&p7(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p7(X1)&~(p6(X1)))|(~(p7(X1))&p6(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p6(X2)&~(p5(X2)))|(~(p6(X2))&p5(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p5(X1)&~(p4(X1)))|(~(p5(X1))&p4(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p4(X2)&~(p3(X2)))|(~(p4(X2))&p3(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p3(X1)&~(p2(X1)))|(~(p3(X1))&p2(X1)))))))|~(![X2]:(~(r1(X1,X2))|~(((p2(X2)&~(p1(X2)))|(~(p2(X2))&p1(X2)))))))|![X2]:(~(r1(X1,X2))|p30(X2)))|![X2]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((~(r1(X1,X2))|(~(p28(X2))&~(p29(X2))))|(p29(X2)&p28(X2)))|(~(p27(X2))&~(p28(X2))))|(p28(X2)&p27(X2)))|(~(p26(X2))&~(p27(X2))))|(p27(X2)&p26(X2)))|(~(p25(X2))&~(p26(X2))))|(p26(X2)&p25(X2)))|(~(p24(X2))&~(p25(X2))))|(p25(X2)&p24(X2)))|(~(p23(X2))&~(p24(X2))))|(p24(X2)&p23(X2)))|(~(p22(X2))&~(p23(X2))))|(p23(X2)&p22(X2)))|(~(p21(X2))&~(p22(X2))))|(p22(X2)&p21(X2)))|(~(p20(X2))&~(p21(X2))))|(p21(X2)&p20(X2)))|(~(p19(X2))&~(p20(X2))))|(p20(X2)&p19(X2)))|(~(p18(X2))&~(p19(X2))))|(p19(X2)&p18(X2)))|(~(p17(X2))&~(p18(X2))))|(p18(X2)&p17(X2)))|(~(p16(X2))&~(p17(X2))))|(p17(X2)&p16(X2)))|(~(p15(X2))&~(p16(X2))))|(p16(X2)&p15(X2)))|(~(p14(X2))&~(p15(X2))))|(p15(X2)&p14(X2)))|(~(p13(X2))&~(p14(X2))))|(p14(X2)&p13(X2)))|(~(p12(X2))&~(p13(X2))))|(p13(X2)&p12(X2)))|(~(p11(X2))&~(p12(X2))))|(p12(X2)&p11(X2)))|(~(p10(X2))&~(p11(X2))))|(p11(X2)&p10(X2)))|(~(p9(X2))&~(p10(X2))))|(p10(X2)&p9(X2)))|(~(p8(X2))&~(p9(X2))))|(p9(X2)&p8(X2)))|(~(p7(X2))&~(p8(X2))))|(p8(X2)&p7(X2)))|(~(p6(X2))&~(p7(X2))))|(p7(X2)&p6(X2)))|(~(p5(X2))&~(p6(X2))))|(p6(X2)&p5(X2)))|(~(p4(X2))&~(p5(X2))))|(p5(X2)&p4(X2)))|(~(p3(X2))&~(p4(X2))))|(p4(X2)&p3(X2)))|(~(p2(X2))&~(p3(X2))))|(p3(X2)&p2(X2)))|(~(p1(X2))&~(p2(X2))))|(p2(X2)&p1(X2)))))))))))),inference(assume_negation,[status(cth)],[3])).
% fof(5, negated_conjecture,~(~(?[X1]:~((![X2]:((~(r1(X1,X2))|~(p30(X2)))|![X1]:(~(r1(X2,X1))|~(p1(X1))))|![X2]:(~(r1(X1,X2))|~(![X1]:(~(r1(X2,X1))|~((((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:~(r1(X2,X1)))|~(![X1]:(~(r1(X2,X1))|~(((p29(X1)&~(p28(X1)))|(~(p29(X1))&p28(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p28(X2)&~(p27(X2)))|(~(p28(X2))&p27(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p27(X1)&~(p26(X1)))|(~(p27(X1))&p26(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p26(X2)&~(p25(X2)))|(~(p26(X2))&p25(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p25(X1)&~(p24(X1)))|(~(p25(X1))&p24(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p24(X2)&~(p23(X2)))|(~(p24(X2))&p23(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p23(X1)&~(p22(X1)))|(~(p23(X1))&p22(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p22(X2)&~(p21(X2)))|(~(p22(X2))&p21(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p21(X1)&~(p20(X1)))|(~(p21(X1))&p20(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p20(X2)&~(p19(X2)))|(~(p20(X2))&p19(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p19(X1)&~(p18(X1)))|(~(p19(X1))&p18(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p18(X2)&~(p17(X2)))|(~(p18(X2))&p17(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p17(X1)&~(p16(X1)))|(~(p17(X1))&p16(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p16(X2)&~(p15(X2)))|(~(p16(X2))&p15(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p15(X1)&~(p14(X1)))|(~(p15(X1))&p14(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p14(X2)&~(p13(X2)))|(~(p14(X2))&p13(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p13(X1)&~(p12(X1)))|(~(p13(X1))&p12(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p12(X2)&~(p11(X2)))|(~(p12(X2))&p11(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p11(X1)&~(p10(X1)))|(~(p11(X1))&p10(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p10(X2)&~(p9(X2)))|(~(p10(X2))&p9(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p9(X1)&~(p8(X1)))|(~(p9(X1))&p8(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p8(X2)&~(p7(X2)))|(~(p8(X2))&p7(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p7(X1)&~(p6(X1)))|(~(p7(X1))&p6(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p6(X2)&~(p5(X2)))|(~(p6(X2))&p5(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p5(X1)&~(p4(X1)))|(~(p5(X1))&p4(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p4(X2)&~(p3(X2)))|(~(p4(X2))&p3(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p3(X1)&~(p2(X1)))|(~(p3(X1))&p2(X1)))))))|~(![X2]:(~(r1(X1,X2))|~(((p2(X2)&~(p1(X2)))|(~(p2(X2))&p1(X2)))))))|![X2]:(~(r1(X1,X2))|p30(X2)))|![X2]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((~(r1(X1,X2))|(~(p28(X2))&~(p29(X2))))|(p29(X2)&p28(X2)))|(~(p27(X2))&~(p28(X2))))|(p28(X2)&p27(X2)))|(~(p26(X2))&~(p27(X2))))|(p27(X2)&p26(X2)))|(~(p25(X2))&~(p26(X2))))|(p26(X2)&p25(X2)))|(~(p24(X2))&~(p25(X2))))|(p25(X2)&p24(X2)))|(~(p23(X2))&~(p24(X2))))|(p24(X2)&p23(X2)))|(~(p22(X2))&~(p23(X2))))|(p23(X2)&p22(X2)))|(~(p21(X2))&~(p22(X2))))|(p22(X2)&p21(X2)))|(~(p20(X2))&~(p21(X2))))|(p21(X2)&p20(X2)))|(~(p19(X2))&~(p20(X2))))|(p20(X2)&p19(X2)))|(~(p18(X2))&~(p19(X2))))|(p19(X2)&p18(X2)))|(~(p17(X2))&~(p18(X2))))|(p18(X2)&p17(X2)))|(~(p16(X2))&~(p17(X2))))|(p17(X2)&p16(X2)))|(~(p15(X2))&~(p16(X2))))|(p16(X2)&p15(X2)))|(~(p14(X2))&~(p15(X2))))|(p15(X2)&p14(X2)))|(~(p13(X2))&~(p14(X2))))|(p14(X2)&p13(X2)))|(~(p12(X2))&~(p13(X2))))|(p13(X2)&p12(X2)))|(~(p11(X2))&~(p12(X2))))|(p12(X2)&p11(X2)))|(~(p10(X2))&~(p11(X2))))|(p11(X2)&p10(X2)))|(~(p9(X2))&~(p10(X2))))|(p10(X2)&p9(X2)))|(~(p8(X2))&~(p9(X2))))|(p9(X2)&p8(X2)))|(~(p7(X2))&~(p8(X2))))|(p8(X2)&p7(X2)))|(~(p6(X2))&~(p7(X2))))|(p7(X2)&p6(X2)))|(~(p5(X2))&~(p6(X2))))|(p6(X2)&p5(X2)))|(~(p4(X2))&~(p5(X2))))|(p5(X2)&p4(X2)))|(~(p3(X2))&~(p4(X2))))|(p4(X2)&p3(X2)))|(~(p2(X2))&~(p3(X2))))|(p3(X2)&p2(X2)))|(~(p1(X2))&~(p2(X2))))|(p2(X2)&p1(X2)))))))))))),inference(fof_simplification,[status(thm)],[4,theory(equality)])).
% fof(6, plain,![X1]:(epred1_1(X1)=>~((((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:~(r1(X2,X1)))|~(![X1]:(~(r1(X2,X1))|~(((p29(X1)&~(p28(X1)))|(~(p29(X1))&p28(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p28(X2)&~(p27(X2)))|(~(p28(X2))&p27(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p27(X1)&~(p26(X1)))|(~(p27(X1))&p26(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p26(X2)&~(p25(X2)))|(~(p26(X2))&p25(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p25(X1)&~(p24(X1)))|(~(p25(X1))&p24(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p24(X2)&~(p23(X2)))|(~(p24(X2))&p23(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p23(X1)&~(p22(X1)))|(~(p23(X1))&p22(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p22(X2)&~(p21(X2)))|(~(p22(X2))&p21(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p21(X1)&~(p20(X1)))|(~(p21(X1))&p20(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p20(X2)&~(p19(X2)))|(~(p20(X2))&p19(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p19(X1)&~(p18(X1)))|(~(p19(X1))&p18(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p18(X2)&~(p17(X2)))|(~(p18(X2))&p17(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p17(X1)&~(p16(X1)))|(~(p17(X1))&p16(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p16(X2)&~(p15(X2)))|(~(p16(X2))&p15(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p15(X1)&~(p14(X1)))|(~(p15(X1))&p14(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p14(X2)&~(p13(X2)))|(~(p14(X2))&p13(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p13(X1)&~(p12(X1)))|(~(p13(X1))&p12(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p12(X2)&~(p11(X2)))|(~(p12(X2))&p11(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p11(X1)&~(p10(X1)))|(~(p11(X1))&p10(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p10(X2)&~(p9(X2)))|(~(p10(X2))&p9(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p9(X1)&~(p8(X1)))|(~(p9(X1))&p8(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p8(X2)&~(p7(X2)))|(~(p8(X2))&p7(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p7(X1)&~(p6(X1)))|(~(p7(X1))&p6(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p6(X2)&~(p5(X2)))|(~(p6(X2))&p5(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p5(X1)&~(p4(X1)))|(~(p5(X1))&p4(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p4(X2)&~(p3(X2)))|(~(p4(X2))&p3(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p3(X1)&~(p2(X1)))|(~(p3(X1))&p2(X1)))))))|~(![X2]:(~(r1(X1,X2))|~(((p2(X2)&~(p1(X2)))|(~(p2(X2))&p1(X2)))))))|![X2]:(~(r1(X1,X2))|p30(X2)))|![X2]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((~(r1(X1,X2))|(~(p28(X2))&~(p29(X2))))|(p29(X2)&p28(X2)))|(~(p27(X2))&~(p28(X2))))|(p28(X2)&p27(X2)))|(~(p26(X2))&~(p27(X2))))|(p27(X2)&p26(X2)))|(~(p25(X2))&~(p26(X2))))|(p26(X2)&p25(X2)))|(~(p24(X2))&~(p25(X2))))|(p25(X2)&p24(X2)))|(~(p23(X2))&~(p24(X2))))|(p24(X2)&p23(X2)))|(~(p22(X2))&~(p23(X2))))|(p23(X2)&p22(X2)))|(~(p21(X2))&~(p22(X2))))|(p22(X2)&p21(X2)))|(~(p20(X2))&~(p21(X2))))|(p21(X2)&p20(X2)))|(~(p19(X2))&~(p20(X2))))|(p20(X2)&p19(X2)))|(~(p18(X2))&~(p19(X2))))|(p19(X2)&p18(X2)))|(~(p17(X2))&~(p18(X2))))|(p18(X2)&p17(X2)))|(~(p16(X2))&~(p17(X2))))|(p17(X2)&p16(X2)))|(~(p15(X2))&~(p16(X2))))|(p16(X2)&p15(X2)))|(~(p14(X2))&~(p15(X2))))|(p15(X2)&p14(X2)))|(~(p13(X2))&~(p14(X2))))|(p14(X2)&p13(X2)))|(~(p12(X2))&~(p13(X2))))|(p13(X2)&p12(X2)))|(~(p11(X2))&~(p12(X2))))|(p12(X2)&p11(X2)))|(~(p10(X2))&~(p11(X2))))|(p11(X2)&p10(X2)))|(~(p9(X2))&~(p10(X2))))|(p10(X2)&p9(X2)))|(~(p8(X2))&~(p9(X2))))|(p9(X2)&p8(X2)))|(~(p7(X2))&~(p8(X2))))|(p8(X2)&p7(X2)))|(~(p6(X2))&~(p7(X2))))|(p7(X2)&p6(X2)))|(~(p5(X2))&~(p6(X2))))|(p6(X2)&p5(X2)))|(~(p4(X2))&~(p5(X2))))|(p5(X2)&p4(X2)))|(~(p3(X2))&~(p4(X2))))|(p4(X2)&p3(X2)))|(~(p2(X2))&~(p3(X2))))|(p3(X2)&p2(X2)))|(~(p1(X2))&~(p2(X2))))|(p2(X2)&p1(X2)))))),introduced(definition)).
% fof(7, negated_conjecture,~(~(?[X1]:~((![X2]:((~(r1(X1,X2))|~(p30(X2)))|![X1]:(~(r1(X2,X1))|~(p1(X1))))|![X2]:(~(r1(X1,X2))|~(![X1]:(~(r1(X2,X1))|epred1_1(X1)))))))),inference(apply_def,[status(esa)],[5,6,theory(equality)])).
% fof(8, plain,![X2]:r1(X2,X2),inference(variable_rename,[status(thm)],[1])).
% cnf(9,plain,(r1(X1,X1)),inference(split_conjunct,[status(thm)],[8])).
% fof(13, negated_conjecture,?[X1]:(?[X2]:((r1(X1,X2)&p30(X2))&?[X1]:(r1(X2,X1)&p1(X1)))&?[X2]:(r1(X1,X2)&![X1]:(~(r1(X2,X1))|epred1_1(X1)))),inference(fof_nnf,[status(thm)],[7])).
% fof(14, negated_conjecture,?[X3]:(?[X4]:((r1(X3,X4)&p30(X4))&?[X5]:(r1(X4,X5)&p1(X5)))&?[X6]:(r1(X3,X6)&![X7]:(~(r1(X6,X7))|epred1_1(X7)))),inference(variable_rename,[status(thm)],[13])).
% fof(15, negated_conjecture,(((r1(esk1_0,esk2_0)&p30(esk2_0))&(r1(esk2_0,esk3_0)&p1(esk3_0)))&(r1(esk1_0,esk4_0)&![X7]:(~(r1(esk4_0,X7))|epred1_1(X7)))),inference(skolemize,[status(esa)],[14])).
% fof(16, negated_conjecture,![X7]:(((~(r1(esk4_0,X7))|epred1_1(X7))&r1(esk1_0,esk4_0))&((r1(esk1_0,esk2_0)&p30(esk2_0))&(r1(esk2_0,esk3_0)&p1(esk3_0)))),inference(shift_quantors,[status(thm)],[15])).
% cnf(22,negated_conjecture,(epred1_1(X1)|~r1(esk4_0,X1)),inference(split_conjunct,[status(thm)],[16])).
% fof(23, plain,![X1]:(~(epred1_1(X1))|(((?[X2]:((r1(X1,X2)&?[X1]:((r1(X2,X1)&?[X2]:((r1(X1,X2)&?[X1]:((r1(X2,X1)&?[X2]:((r1(X1,X2)&?[X1]:((r1(X2,X1)&?[X2]:((r1(X1,X2)&?[X1]:((r1(X2,X1)&?[X2]:((r1(X1,X2)&?[X1]:((r1(X2,X1)&?[X2]:((r1(X1,X2)&?[X1]:((r1(X2,X1)&?[X2]:((r1(X1,X2)&?[X1]:((r1(X2,X1)&?[X2]:((r1(X1,X2)&?[X1]:((r1(X2,X1)&?[X2]:((r1(X1,X2)&?[X1]:((r1(X2,X1)&?[X2]:((r1(X1,X2)&?[X1]:((r1(X2,X1)&?[X2]:((r1(X1,X2)&?[X1]:((r1(X2,X1)&?[X2]:((r1(X1,X2)&?[X1]:((r1(X2,X1)&?[X2]:((r1(X1,X2)&?[X1]:((r1(X2,X1)&?[X2]:((r1(X1,X2)&?[X1]:r1(X2,X1))&![X1]:(~(r1(X2,X1))|((~(p29(X1))|p28(X1))&(p29(X1)|~(p28(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p28(X2))|p27(X2))&(p28(X2)|~(p27(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p27(X1))|p26(X1))&(p27(X1)|~(p26(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p26(X2))|p25(X2))&(p26(X2)|~(p25(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p25(X1))|p24(X1))&(p25(X1)|~(p24(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p24(X2))|p23(X2))&(p24(X2)|~(p23(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p23(X1))|p22(X1))&(p23(X1)|~(p22(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p22(X2))|p21(X2))&(p22(X2)|~(p21(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p21(X1))|p20(X1))&(p21(X1)|~(p20(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p20(X2))|p19(X2))&(p20(X2)|~(p19(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p19(X1))|p18(X1))&(p19(X1)|~(p18(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p18(X2))|p17(X2))&(p18(X2)|~(p17(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p17(X1))|p16(X1))&(p17(X1)|~(p16(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p16(X2))|p15(X2))&(p16(X2)|~(p15(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p15(X1))|p14(X1))&(p15(X1)|~(p14(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p14(X2))|p13(X2))&(p14(X2)|~(p13(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p13(X1))|p12(X1))&(p13(X1)|~(p12(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p12(X2))|p11(X2))&(p12(X2)|~(p11(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p11(X1))|p10(X1))&(p11(X1)|~(p10(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p10(X2))|p9(X2))&(p10(X2)|~(p9(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p9(X1))|p8(X1))&(p9(X1)|~(p8(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p8(X2))|p7(X2))&(p8(X2)|~(p7(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p7(X1))|p6(X1))&(p7(X1)|~(p6(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p6(X2))|p5(X2))&(p6(X2)|~(p5(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p5(X1))|p4(X1))&(p5(X1)|~(p4(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p4(X2))|p3(X2))&(p4(X2)|~(p3(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p3(X1))|p2(X1))&(p3(X1)|~(p2(X1))))))&![X2]:(~(r1(X1,X2))|((~(p2(X2))|p1(X2))&(p2(X2)|~(p1(X2))))))&?[X2]:(r1(X1,X2)&~(p30(X2))))&?[X2]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X1,X2)&(p28(X2)|p29(X2)))&(~(p29(X2))|~(p28(X2))))&(p27(X2)|p28(X2)))&(~(p28(X2))|~(p27(X2))))&(p26(X2)|p27(X2)))&(~(p27(X2))|~(p26(X2))))&(p25(X2)|p26(X2)))&(~(p26(X2))|~(p25(X2))))&(p24(X2)|p25(X2)))&(~(p25(X2))|~(p24(X2))))&(p23(X2)|p24(X2)))&(~(p24(X2))|~(p23(X2))))&(p22(X2)|p23(X2)))&(~(p23(X2))|~(p22(X2))))&(p21(X2)|p22(X2)))&(~(p22(X2))|~(p21(X2))))&(p20(X2)|p21(X2)))&(~(p21(X2))|~(p20(X2))))&(p19(X2)|p20(X2)))&(~(p20(X2))|~(p19(X2))))&(p18(X2)|p19(X2)))&(~(p19(X2))|~(p18(X2))))&(p17(X2)|p18(X2)))&(~(p18(X2))|~(p17(X2))))&(p16(X2)|p17(X2)))&(~(p17(X2))|~(p16(X2))))&(p15(X2)|p16(X2)))&(~(p16(X2))|~(p15(X2))))&(p14(X2)|p15(X2)))&(~(p15(X2))|~(p14(X2))))&(p13(X2)|p14(X2)))&(~(p14(X2))|~(p13(X2))))&(p12(X2)|p13(X2)))&(~(p13(X2))|~(p12(X2))))&(p11(X2)|p12(X2)))&(~(p12(X2))|~(p11(X2))))&(p10(X2)|p11(X2)))&(~(p11(X2))|~(p10(X2))))&(p9(X2)|p10(X2)))&(~(p10(X2))|~(p9(X2))))&(p8(X2)|p9(X2)))&(~(p9(X2))|~(p8(X2))))&(p7(X2)|p8(X2)))&(~(p8(X2))|~(p7(X2))))&(p6(X2)|p7(X2)))&(~(p7(X2))|~(p6(X2))))&(p5(X2)|p6(X2)))&(~(p6(X2))|~(p5(X2))))&(p4(X2)|p5(X2)))&(~(p5(X2))|~(p4(X2))))&(p3(X2)|p4(X2)))&(~(p4(X2))|~(p3(X2))))&(p2(X2)|p3(X2)))&(~(p3(X2))|~(p2(X2))))&(p1(X2)|p2(X2)))&(~(p2(X2))|~(p1(X2)))))),inference(fof_nnf,[status(thm)],[6])).
% fof(24, plain,![X3]:(~(epred1_1(X3))|(((?[X4]:((r1(X3,X4)&?[X5]:((r1(X4,X5)&?[X6]:((r1(X5,X6)&?[X7]:((r1(X6,X7)&?[X8]:((r1(X7,X8)&?[X9]:((r1(X8,X9)&?[X10]:((r1(X9,X10)&?[X11]:((r1(X10,X11)&?[X12]:((r1(X11,X12)&?[X13]:((r1(X12,X13)&?[X14]:((r1(X13,X14)&?[X15]:((r1(X14,X15)&?[X16]:((r1(X15,X16)&?[X17]:((r1(X16,X17)&?[X18]:((r1(X17,X18)&?[X19]:((r1(X18,X19)&?[X20]:((r1(X19,X20)&?[X21]:((r1(X20,X21)&?[X22]:((r1(X21,X22)&?[X23]:((r1(X22,X23)&?[X24]:((r1(X23,X24)&?[X25]:((r1(X24,X25)&?[X26]:((r1(X25,X26)&?[X27]:((r1(X26,X27)&?[X28]:((r1(X27,X28)&?[X29]:((r1(X28,X29)&?[X30]:((r1(X29,X30)&?[X31]:r1(X30,X31))&![X32]:(~(r1(X30,X32))|((~(p29(X32))|p28(X32))&(p29(X32)|~(p28(X32)))))))&![X33]:(~(r1(X29,X33))|((~(p28(X33))|p27(X33))&(p28(X33)|~(p27(X33)))))))&![X34]:(~(r1(X28,X34))|((~(p27(X34))|p26(X34))&(p27(X34)|~(p26(X34)))))))&![X35]:(~(r1(X27,X35))|((~(p26(X35))|p25(X35))&(p26(X35)|~(p25(X35)))))))&![X36]:(~(r1(X26,X36))|((~(p25(X36))|p24(X36))&(p25(X36)|~(p24(X36)))))))&![X37]:(~(r1(X25,X37))|((~(p24(X37))|p23(X37))&(p24(X37)|~(p23(X37)))))))&![X38]:(~(r1(X24,X38))|((~(p23(X38))|p22(X38))&(p23(X38)|~(p22(X38)))))))&![X39]:(~(r1(X23,X39))|((~(p22(X39))|p21(X39))&(p22(X39)|~(p21(X39)))))))&![X40]:(~(r1(X22,X40))|((~(p21(X40))|p20(X40))&(p21(X40)|~(p20(X40)))))))&![X41]:(~(r1(X21,X41))|((~(p20(X41))|p19(X41))&(p20(X41)|~(p19(X41)))))))&![X42]:(~(r1(X20,X42))|((~(p19(X42))|p18(X42))&(p19(X42)|~(p18(X42)))))))&![X43]:(~(r1(X19,X43))|((~(p18(X43))|p17(X43))&(p18(X43)|~(p17(X43)))))))&![X44]:(~(r1(X18,X44))|((~(p17(X44))|p16(X44))&(p17(X44)|~(p16(X44)))))))&![X45]:(~(r1(X17,X45))|((~(p16(X45))|p15(X45))&(p16(X45)|~(p15(X45)))))))&![X46]:(~(r1(X16,X46))|((~(p15(X46))|p14(X46))&(p15(X46)|~(p14(X46)))))))&![X47]:(~(r1(X15,X47))|((~(p14(X47))|p13(X47))&(p14(X47)|~(p13(X47)))))))&![X48]:(~(r1(X14,X48))|((~(p13(X48))|p12(X48))&(p13(X48)|~(p12(X48)))))))&![X49]:(~(r1(X13,X49))|((~(p12(X49))|p11(X49))&(p12(X49)|~(p11(X49)))))))&![X50]:(~(r1(X12,X50))|((~(p11(X50))|p10(X50))&(p11(X50)|~(p10(X50)))))))&![X51]:(~(r1(X11,X51))|((~(p10(X51))|p9(X51))&(p10(X51)|~(p9(X51)))))))&![X52]:(~(r1(X10,X52))|((~(p9(X52))|p8(X52))&(p9(X52)|~(p8(X52)))))))&![X53]:(~(r1(X9,X53))|((~(p8(X53))|p7(X53))&(p8(X53)|~(p7(X53)))))))&![X54]:(~(r1(X8,X54))|((~(p7(X54))|p6(X54))&(p7(X54)|~(p6(X54)))))))&![X55]:(~(r1(X7,X55))|((~(p6(X55))|p5(X55))&(p6(X55)|~(p5(X55)))))))&![X56]:(~(r1(X6,X56))|((~(p5(X56))|p4(X56))&(p5(X56)|~(p4(X56)))))))&![X57]:(~(r1(X5,X57))|((~(p4(X57))|p3(X57))&(p4(X57)|~(p3(X57)))))))&![X58]:(~(r1(X4,X58))|((~(p3(X58))|p2(X58))&(p3(X58)|~(p2(X58))))))&![X59]:(~(r1(X3,X59))|((~(p2(X59))|p1(X59))&(p2(X59)|~(p1(X59))))))&?[X60]:(r1(X3,X60)&~(p30(X60))))&?[X61]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X3,X61)&(p28(X61)|p29(X61)))&(~(p29(X61))|~(p28(X61))))&(p27(X61)|p28(X61)))&(~(p28(X61))|~(p27(X61))))&(p26(X61)|p27(X61)))&(~(p27(X61))|~(p26(X61))))&(p25(X61)|p26(X61)))&(~(p26(X61))|~(p25(X61))))&(p24(X61)|p25(X61)))&(~(p25(X61))|~(p24(X61))))&(p23(X61)|p24(X61)))&(~(p24(X61))|~(p23(X61))))&(p22(X61)|p23(X61)))&(~(p23(X61))|~(p22(X61))))&(p21(X61)|p22(X61)))&(~(p22(X61))|~(p21(X61))))&(p20(X61)|p21(X61)))&(~(p21(X61))|~(p20(X61))))&(p19(X61)|p20(X61)))&(~(p20(X61))|~(p19(X61))))&(p18(X61)|p19(X61)))&(~(p19(X61))|~(p18(X61))))&(p17(X61)|p18(X61)))&(~(p18(X61))|~(p17(X61))))&(p16(X61)|p17(X61)))&(~(p17(X61))|~(p16(X61))))&(p15(X61)|p16(X61)))&(~(p16(X61))|~(p15(X61))))&(p14(X61)|p15(X61)))&(~(p15(X61))|~(p14(X61))))&(p13(X61)|p14(X61)))&(~(p14(X61))|~(p13(X61))))&(p12(X61)|p13(X61)))&(~(p13(X61))|~(p12(X61))))&(p11(X61)|p12(X61)))&(~(p12(X61))|~(p11(X61))))&(p10(X61)|p11(X61)))&(~(p11(X61))|~(p10(X61))))&(p9(X61)|p10(X61)))&(~(p10(X61))|~(p9(X61))))&(p8(X61)|p9(X61)))&(~(p9(X61))|~(p8(X61))))&(p7(X61)|p8(X61)))&(~(p8(X61))|~(p7(X61))))&(p6(X61)|p7(X61)))&(~(p7(X61))|~(p6(X61))))&(p5(X61)|p6(X61)))&(~(p6(X61))|~(p5(X61))))&(p4(X61)|p5(X61)))&(~(p5(X61))|~(p4(X61))))&(p3(X61)|p4(X61)))&(~(p4(X61))|~(p3(X61))))&(p2(X61)|p3(X61)))&(~(p3(X61))|~(p2(X61))))&(p1(X61)|p2(X61)))&(~(p2(X61))|~(p1(X61)))))),inference(variable_rename,[status(thm)],[23])).
% fof(25, plain,![X3]:(~(epred1_1(X3))|(((((r1(X3,esk5_1(X3))&((r1(esk5_1(X3),esk6_1(X3))&((r1(esk6_1(X3),esk7_1(X3))&((r1(esk7_1(X3),esk8_1(X3))&((r1(esk8_1(X3),esk9_1(X3))&((r1(esk9_1(X3),esk10_1(X3))&((r1(esk10_1(X3),esk11_1(X3))&((r1(esk11_1(X3),esk12_1(X3))&((r1(esk12_1(X3),esk13_1(X3))&((r1(esk13_1(X3),esk14_1(X3))&((r1(esk14_1(X3),esk15_1(X3))&((r1(esk15_1(X3),esk16_1(X3))&((r1(esk16_1(X3),esk17_1(X3))&((r1(esk17_1(X3),esk18_1(X3))&((r1(esk18_1(X3),esk19_1(X3))&((r1(esk19_1(X3),esk20_1(X3))&((r1(esk20_1(X3),esk21_1(X3))&((r1(esk21_1(X3),esk22_1(X3))&((r1(esk22_1(X3),esk23_1(X3))&((r1(esk23_1(X3),esk24_1(X3))&((r1(esk24_1(X3),esk25_1(X3))&((r1(esk25_1(X3),esk26_1(X3))&((r1(esk26_1(X3),esk27_1(X3))&((r1(esk27_1(X3),esk28_1(X3))&((r1(esk28_1(X3),esk29_1(X3))&((r1(esk29_1(X3),esk30_1(X3))&((r1(esk30_1(X3),esk31_1(X3))&r1(esk31_1(X3),esk32_1(X3)))&![X32]:(~(r1(esk31_1(X3),X32))|((~(p29(X32))|p28(X32))&(p29(X32)|~(p28(X32)))))))&![X33]:(~(r1(esk30_1(X3),X33))|((~(p28(X33))|p27(X33))&(p28(X33)|~(p27(X33)))))))&![X34]:(~(r1(esk29_1(X3),X34))|((~(p27(X34))|p26(X34))&(p27(X34)|~(p26(X34)))))))&![X35]:(~(r1(esk28_1(X3),X35))|((~(p26(X35))|p25(X35))&(p26(X35)|~(p25(X35)))))))&![X36]:(~(r1(esk27_1(X3),X36))|((~(p25(X36))|p24(X36))&(p25(X36)|~(p24(X36)))))))&![X37]:(~(r1(esk26_1(X3),X37))|((~(p24(X37))|p23(X37))&(p24(X37)|~(p23(X37)))))))&![X38]:(~(r1(esk25_1(X3),X38))|((~(p23(X38))|p22(X38))&(p23(X38)|~(p22(X38)))))))&![X39]:(~(r1(esk24_1(X3),X39))|((~(p22(X39))|p21(X39))&(p22(X39)|~(p21(X39)))))))&![X40]:(~(r1(esk23_1(X3),X40))|((~(p21(X40))|p20(X40))&(p21(X40)|~(p20(X40)))))))&![X41]:(~(r1(esk22_1(X3),X41))|((~(p20(X41))|p19(X41))&(p20(X41)|~(p19(X41)))))))&![X42]:(~(r1(esk21_1(X3),X42))|((~(p19(X42))|p18(X42))&(p19(X42)|~(p18(X42)))))))&![X43]:(~(r1(esk20_1(X3),X43))|((~(p18(X43))|p17(X43))&(p18(X43)|~(p17(X43)))))))&![X44]:(~(r1(esk19_1(X3),X44))|((~(p17(X44))|p16(X44))&(p17(X44)|~(p16(X44)))))))&![X45]:(~(r1(esk18_1(X3),X45))|((~(p16(X45))|p15(X45))&(p16(X45)|~(p15(X45)))))))&![X46]:(~(r1(esk17_1(X3),X46))|((~(p15(X46))|p14(X46))&(p15(X46)|~(p14(X46)))))))&![X47]:(~(r1(esk16_1(X3),X47))|((~(p14(X47))|p13(X47))&(p14(X47)|~(p13(X47)))))))&![X48]:(~(r1(esk15_1(X3),X48))|((~(p13(X48))|p12(X48))&(p13(X48)|~(p12(X48)))))))&![X49]:(~(r1(esk14_1(X3),X49))|((~(p12(X49))|p11(X49))&(p12(X49)|~(p11(X49)))))))&![X50]:(~(r1(esk13_1(X3),X50))|((~(p11(X50))|p10(X50))&(p11(X50)|~(p10(X50)))))))&![X51]:(~(r1(esk12_1(X3),X51))|((~(p10(X51))|p9(X51))&(p10(X51)|~(p9(X51)))))))&![X52]:(~(r1(esk11_1(X3),X52))|((~(p9(X52))|p8(X52))&(p9(X52)|~(p8(X52)))))))&![X53]:(~(r1(esk10_1(X3),X53))|((~(p8(X53))|p7(X53))&(p8(X53)|~(p7(X53)))))))&![X54]:(~(r1(esk9_1(X3),X54))|((~(p7(X54))|p6(X54))&(p7(X54)|~(p6(X54)))))))&![X55]:(~(r1(esk8_1(X3),X55))|((~(p6(X55))|p5(X55))&(p6(X55)|~(p5(X55)))))))&![X56]:(~(r1(esk7_1(X3),X56))|((~(p5(X56))|p4(X56))&(p5(X56)|~(p4(X56)))))))&![X57]:(~(r1(esk6_1(X3),X57))|((~(p4(X57))|p3(X57))&(p4(X57)|~(p3(X57)))))))&![X58]:(~(r1(esk5_1(X3),X58))|((~(p3(X58))|p2(X58))&(p3(X58)|~(p2(X58))))))&![X59]:(~(r1(X3,X59))|((~(p2(X59))|p1(X59))&(p2(X59)|~(p1(X59))))))&(r1(X3,esk33_1(X3))&~(p30(esk33_1(X3)))))&((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X3,esk34_1(X3))&(p28(esk34_1(X3))|p29(esk34_1(X3))))&(~(p29(esk34_1(X3)))|~(p28(esk34_1(X3)))))&(p27(esk34_1(X3))|p28(esk34_1(X3))))&(~(p28(esk34_1(X3)))|~(p27(esk34_1(X3)))))&(p26(esk34_1(X3))|p27(esk34_1(X3))))&(~(p27(esk34_1(X3)))|~(p26(esk34_1(X3)))))&(p25(esk34_1(X3))|p26(esk34_1(X3))))&(~(p26(esk34_1(X3)))|~(p25(esk34_1(X3)))))&(p24(esk34_1(X3))|p25(esk34_1(X3))))&(~(p25(esk34_1(X3)))|~(p24(esk34_1(X3)))))&(p23(esk34_1(X3))|p24(esk34_1(X3))))&(~(p24(esk34_1(X3)))|~(p23(esk34_1(X3)))))&(p22(esk34_1(X3))|p23(esk34_1(X3))))&(~(p23(esk34_1(X3)))|~(p22(esk34_1(X3)))))&(p21(esk34_1(X3))|p22(esk34_1(X3))))&(~(p22(esk34_1(X3)))|~(p21(esk34_1(X3)))))&(p20(esk34_1(X3))|p21(esk34_1(X3))))&(~(p21(esk34_1(X3)))|~(p20(esk34_1(X3)))))&(p19(esk34_1(X3))|p20(esk34_1(X3))))&(~(p20(esk34_1(X3)))|~(p19(esk34_1(X3)))))&(p18(esk34_1(X3))|p19(esk34_1(X3))))&(~(p19(esk34_1(X3)))|~(p18(esk34_1(X3)))))&(p17(esk34_1(X3))|p18(esk34_1(X3))))&(~(p18(esk34_1(X3)))|~(p17(esk34_1(X3)))))&(p16(esk34_1(X3))|p17(esk34_1(X3))))&(~(p17(esk34_1(X3)))|~(p16(esk34_1(X3)))))&(p15(esk34_1(X3))|p16(esk34_1(X3))))&(~(p16(esk34_1(X3)))|~(p15(esk34_1(X3)))))&(p14(esk34_1(X3))|p15(esk34_1(X3))))&(~(p15(esk34_1(X3)))|~(p14(esk34_1(X3)))))&(p13(esk34_1(X3))|p14(esk34_1(X3))))&(~(p14(esk34_1(X3)))|~(p13(esk34_1(X3)))))&(p12(esk34_1(X3))|p13(esk34_1(X3))))&(~(p13(esk34_1(X3)))|~(p12(esk34_1(X3)))))&(p11(esk34_1(X3))|p12(esk34_1(X3))))&(~(p12(esk34_1(X3)))|~(p11(esk34_1(X3)))))&(p10(esk34_1(X3))|p11(esk34_1(X3))))&(~(p11(esk34_1(X3)))|~(p10(esk34_1(X3)))))&(p9(esk34_1(X3))|p10(esk34_1(X3))))&(~(p10(esk34_1(X3)))|~(p9(esk34_1(X3)))))&(p8(esk34_1(X3))|p9(esk34_1(X3))))&(~(p9(esk34_1(X3)))|~(p8(esk34_1(X3)))))&(p7(esk34_1(X3))|p8(esk34_1(X3))))&(~(p8(esk34_1(X3)))|~(p7(esk34_1(X3)))))&(p6(esk34_1(X3))|p7(esk34_1(X3))))&(~(p7(esk34_1(X3)))|~(p6(esk34_1(X3)))))&(p5(esk34_1(X3))|p6(esk34_1(X3))))&(~(p6(esk34_1(X3)))|~(p5(esk34_1(X3)))))&(p4(esk34_1(X3))|p5(esk34_1(X3))))&(~(p5(esk34_1(X3)))|~(p4(esk34_1(X3)))))&(p3(esk34_1(X3))|p4(esk34_1(X3))))&(~(p4(esk34_1(X3)))|~(p3(esk34_1(X3)))))&(p2(esk34_1(X3))|p3(esk34_1(X3))))&(~(p3(esk34_1(X3)))|~(p2(esk34_1(X3)))))&(p1(esk34_1(X3))|p2(esk34_1(X3))))&(~(p2(esk34_1(X3)))|~(p1(esk34_1(X3))))))),inference(skolemize,[status(esa)],[24])).
% fof(26, plain,![X3]:![X32]:![X33]:![X34]:![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:![X42]:![X43]:![X44]:![X45]:![X46]:![X47]:![X48]:![X49]:![X50]:![X51]:![X52]:![X53]:![X54]:![X55]:![X56]:![X57]:![X58]:![X59]:(((((~(r1(X3,X59))|((~(p2(X59))|p1(X59))&(p2(X59)|~(p1(X59)))))&((~(r1(esk5_1(X3),X58))|((~(p3(X58))|p2(X58))&(p3(X58)|~(p2(X58)))))&(((~(r1(esk6_1(X3),X57))|((~(p4(X57))|p3(X57))&(p4(X57)|~(p3(X57)))))&(((~(r1(esk7_1(X3),X56))|((~(p5(X56))|p4(X56))&(p5(X56)|~(p4(X56)))))&(((~(r1(esk8_1(X3),X55))|((~(p6(X55))|p5(X55))&(p6(X55)|~(p5(X55)))))&(((~(r1(esk9_1(X3),X54))|((~(p7(X54))|p6(X54))&(p7(X54)|~(p6(X54)))))&(((~(r1(esk10_1(X3),X53))|((~(p8(X53))|p7(X53))&(p8(X53)|~(p7(X53)))))&(((~(r1(esk11_1(X3),X52))|((~(p9(X52))|p8(X52))&(p9(X52)|~(p8(X52)))))&(((~(r1(esk12_1(X3),X51))|((~(p10(X51))|p9(X51))&(p10(X51)|~(p9(X51)))))&(((~(r1(esk13_1(X3),X50))|((~(p11(X50))|p10(X50))&(p11(X50)|~(p10(X50)))))&(((~(r1(esk14_1(X3),X49))|((~(p12(X49))|p11(X49))&(p12(X49)|~(p11(X49)))))&(((~(r1(esk15_1(X3),X48))|((~(p13(X48))|p12(X48))&(p13(X48)|~(p12(X48)))))&(((~(r1(esk16_1(X3),X47))|((~(p14(X47))|p13(X47))&(p14(X47)|~(p13(X47)))))&(((~(r1(esk17_1(X3),X46))|((~(p15(X46))|p14(X46))&(p15(X46)|~(p14(X46)))))&(((~(r1(esk18_1(X3),X45))|((~(p16(X45))|p15(X45))&(p16(X45)|~(p15(X45)))))&(((~(r1(esk19_1(X3),X44))|((~(p17(X44))|p16(X44))&(p17(X44)|~(p16(X44)))))&(((~(r1(esk20_1(X3),X43))|((~(p18(X43))|p17(X43))&(p18(X43)|~(p17(X43)))))&(((~(r1(esk21_1(X3),X42))|((~(p19(X42))|p18(X42))&(p19(X42)|~(p18(X42)))))&(((~(r1(esk22_1(X3),X41))|((~(p20(X41))|p19(X41))&(p20(X41)|~(p19(X41)))))&(((~(r1(esk23_1(X3),X40))|((~(p21(X40))|p20(X40))&(p21(X40)|~(p20(X40)))))&(((~(r1(esk24_1(X3),X39))|((~(p22(X39))|p21(X39))&(p22(X39)|~(p21(X39)))))&(((~(r1(esk25_1(X3),X38))|((~(p23(X38))|p22(X38))&(p23(X38)|~(p22(X38)))))&(((~(r1(esk26_1(X3),X37))|((~(p24(X37))|p23(X37))&(p24(X37)|~(p23(X37)))))&(((~(r1(esk27_1(X3),X36))|((~(p25(X36))|p24(X36))&(p25(X36)|~(p24(X36)))))&(((~(r1(esk28_1(X3),X35))|((~(p26(X35))|p25(X35))&(p26(X35)|~(p25(X35)))))&(((~(r1(esk29_1(X3),X34))|((~(p27(X34))|p26(X34))&(p27(X34)|~(p26(X34)))))&(((~(r1(esk30_1(X3),X33))|((~(p28(X33))|p27(X33))&(p28(X33)|~(p27(X33)))))&(((~(r1(esk31_1(X3),X32))|((~(p29(X32))|p28(X32))&(p29(X32)|~(p28(X32)))))&(r1(esk30_1(X3),esk31_1(X3))&r1(esk31_1(X3),esk32_1(X3))))&r1(esk29_1(X3),esk30_1(X3))))&r1(esk28_1(X3),esk29_1(X3))))&r1(esk27_1(X3),esk28_1(X3))))&r1(esk26_1(X3),esk27_1(X3))))&r1(esk25_1(X3),esk26_1(X3))))&r1(esk24_1(X3),esk25_1(X3))))&r1(esk23_1(X3),esk24_1(X3))))&r1(esk22_1(X3),esk23_1(X3))))&r1(esk21_1(X3),esk22_1(X3))))&r1(esk20_1(X3),esk21_1(X3))))&r1(esk19_1(X3),esk20_1(X3))))&r1(esk18_1(X3),esk19_1(X3))))&r1(esk17_1(X3),esk18_1(X3))))&r1(esk16_1(X3),esk17_1(X3))))&r1(esk15_1(X3),esk16_1(X3))))&r1(esk14_1(X3),esk15_1(X3))))&r1(esk13_1(X3),esk14_1(X3))))&r1(esk12_1(X3),esk13_1(X3))))&r1(esk11_1(X3),esk12_1(X3))))&r1(esk10_1(X3),esk11_1(X3))))&r1(esk9_1(X3),esk10_1(X3))))&r1(esk8_1(X3),esk9_1(X3))))&r1(esk7_1(X3),esk8_1(X3))))&r1(esk6_1(X3),esk7_1(X3))))&r1(esk5_1(X3),esk6_1(X3))))&r1(X3,esk5_1(X3)))))&(r1(X3,esk33_1(X3))&~(p30(esk33_1(X3)))))&((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X3,esk34_1(X3))&(p28(esk34_1(X3))|p29(esk34_1(X3))))&(~(p29(esk34_1(X3)))|~(p28(esk34_1(X3)))))&(p27(esk34_1(X3))|p28(esk34_1(X3))))&(~(p28(esk34_1(X3)))|~(p27(esk34_1(X3)))))&(p26(esk34_1(X3))|p27(esk34_1(X3))))&(~(p27(esk34_1(X3)))|~(p26(esk34_1(X3)))))&(p25(esk34_1(X3))|p26(esk34_1(X3))))&(~(p26(esk34_1(X3)))|~(p25(esk34_1(X3)))))&(p24(esk34_1(X3))|p25(esk34_1(X3))))&(~(p25(esk34_1(X3)))|~(p24(esk34_1(X3)))))&(p23(esk34_1(X3))|p24(esk34_1(X3))))&(~(p24(esk34_1(X3)))|~(p23(esk34_1(X3)))))&(p22(esk34_1(X3))|p23(esk34_1(X3))))&(~(p23(esk34_1(X3)))|~(p22(esk34_1(X3)))))&(p21(esk34_1(X3))|p22(esk34_1(X3))))&(~(p22(esk34_1(X3)))|~(p21(esk34_1(X3)))))&(p20(esk34_1(X3))|p21(esk34_1(X3))))&(~(p21(esk34_1(X3)))|~(p20(esk34_1(X3)))))&(p19(esk34_1(X3))|p20(esk34_1(X3))))&(~(p20(esk34_1(X3)))|~(p19(esk34_1(X3)))))&(p18(esk34_1(X3))|p19(esk34_1(X3))))&(~(p19(esk34_1(X3)))|~(p18(esk34_1(X3)))))&(p17(esk34_1(X3))|p18(esk34_1(X3))))&(~(p18(esk34_1(X3)))|~(p17(esk34_1(X3)))))&(p16(esk34_1(X3))|p17(esk34_1(X3))))&(~(p17(esk34_1(X3)))|~(p16(esk34_1(X3)))))&(p15(esk34_1(X3))|p16(esk34_1(X3))))&(~(p16(esk34_1(X3)))|~(p15(esk34_1(X3)))))&(p14(esk34_1(X3))|p15(esk34_1(X3))))&(~(p15(esk34_1(X3)))|~(p14(esk34_1(X3)))))&(p13(esk34_1(X3))|p14(esk34_1(X3))))&(~(p14(esk34_1(X3)))|~(p13(esk34_1(X3)))))&(p12(esk34_1(X3))|p13(esk34_1(X3))))&(~(p13(esk34_1(X3)))|~(p12(esk34_1(X3)))))&(p11(esk34_1(X3))|p12(esk34_1(X3))))&(~(p12(esk34_1(X3)))|~(p11(esk34_1(X3)))))&(p10(esk34_1(X3))|p11(esk34_1(X3))))&(~(p11(esk34_1(X3)))|~(p10(esk34_1(X3)))))&(p9(esk34_1(X3))|p10(esk34_1(X3))))&(~(p10(esk34_1(X3)))|~(p9(esk34_1(X3)))))&(p8(esk34_1(X3))|p9(esk34_1(X3))))&(~(p9(esk34_1(X3)))|~(p8(esk34_1(X3)))))&(p7(esk34_1(X3))|p8(esk34_1(X3))))&(~(p8(esk34_1(X3)))|~(p7(esk34_1(X3)))))&(p6(esk34_1(X3))|p7(esk34_1(X3))))&(~(p7(esk34_1(X3)))|~(p6(esk34_1(X3)))))&(p5(esk34_1(X3))|p6(esk34_1(X3))))&(~(p6(esk34_1(X3)))|~(p5(esk34_1(X3)))))&(p4(esk34_1(X3))|p5(esk34_1(X3))))&(~(p5(esk34_1(X3)))|~(p4(esk34_1(X3)))))&(p3(esk34_1(X3))|p4(esk34_1(X3))))&(~(p4(esk34_1(X3)))|~(p3(esk34_1(X3)))))&(p2(esk34_1(X3))|p3(esk34_1(X3))))&(~(p3(esk34_1(X3)))|~(p2(esk34_1(X3)))))&(p1(esk34_1(X3))|p2(esk34_1(X3))))&(~(p2(esk34_1(X3)))|~(p1(esk34_1(X3))))))|~(epred1_1(X3))),inference(shift_quantors,[status(thm)],[25])).
% fof(27, plain,![X3]:![X32]:![X33]:![X34]:![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:![X42]:![X43]:![X44]:![X45]:![X46]:![X47]:![X48]:![X49]:![X50]:![X51]:![X52]:![X53]:![X54]:![X55]:![X56]:![X57]:![X58]:![X59]:(((((((~(p2(X59))|p1(X59))|~(r1(X3,X59)))|~(epred1_1(X3)))&(((p2(X59)|~(p1(X59)))|~(r1(X3,X59)))|~(epred1_1(X3))))&(((((~(p3(X58))|p2(X58))|~(r1(esk5_1(X3),X58)))|~(epred1_1(X3)))&(((p3(X58)|~(p2(X58)))|~(r1(esk5_1(X3),X58)))|~(epred1_1(X3))))&((((((~(p4(X57))|p3(X57))|~(r1(esk6_1(X3),X57)))|~(epred1_1(X3)))&(((p4(X57)|~(p3(X57)))|~(r1(esk6_1(X3),X57)))|~(epred1_1(X3))))&((((((~(p5(X56))|p4(X56))|~(r1(esk7_1(X3),X56)))|~(epred1_1(X3)))&(((p5(X56)|~(p4(X56)))|~(r1(esk7_1(X3),X56)))|~(epred1_1(X3))))&((((((~(p6(X55))|p5(X55))|~(r1(esk8_1(X3),X55)))|~(epred1_1(X3)))&(((p6(X55)|~(p5(X55)))|~(r1(esk8_1(X3),X55)))|~(epred1_1(X3))))&((((((~(p7(X54))|p6(X54))|~(r1(esk9_1(X3),X54)))|~(epred1_1(X3)))&(((p7(X54)|~(p6(X54)))|~(r1(esk9_1(X3),X54)))|~(epred1_1(X3))))&((((((~(p8(X53))|p7(X53))|~(r1(esk10_1(X3),X53)))|~(epred1_1(X3)))&(((p8(X53)|~(p7(X53)))|~(r1(esk10_1(X3),X53)))|~(epred1_1(X3))))&((((((~(p9(X52))|p8(X52))|~(r1(esk11_1(X3),X52)))|~(epred1_1(X3)))&(((p9(X52)|~(p8(X52)))|~(r1(esk11_1(X3),X52)))|~(epred1_1(X3))))&((((((~(p10(X51))|p9(X51))|~(r1(esk12_1(X3),X51)))|~(epred1_1(X3)))&(((p10(X51)|~(p9(X51)))|~(r1(esk12_1(X3),X51)))|~(epred1_1(X3))))&((((((~(p11(X50))|p10(X50))|~(r1(esk13_1(X3),X50)))|~(epred1_1(X3)))&(((p11(X50)|~(p10(X50)))|~(r1(esk13_1(X3),X50)))|~(epred1_1(X3))))&((((((~(p12(X49))|p11(X49))|~(r1(esk14_1(X3),X49)))|~(epred1_1(X3)))&(((p12(X49)|~(p11(X49)))|~(r1(esk14_1(X3),X49)))|~(epred1_1(X3))))&((((((~(p13(X48))|p12(X48))|~(r1(esk15_1(X3),X48)))|~(epred1_1(X3)))&(((p13(X48)|~(p12(X48)))|~(r1(esk15_1(X3),X48)))|~(epred1_1(X3))))&((((((~(p14(X47))|p13(X47))|~(r1(esk16_1(X3),X47)))|~(epred1_1(X3)))&(((p14(X47)|~(p13(X47)))|~(r1(esk16_1(X3),X47)))|~(epred1_1(X3))))&((((((~(p15(X46))|p14(X46))|~(r1(esk17_1(X3),X46)))|~(epred1_1(X3)))&(((p15(X46)|~(p14(X46)))|~(r1(esk17_1(X3),X46)))|~(epred1_1(X3))))&((((((~(p16(X45))|p15(X45))|~(r1(esk18_1(X3),X45)))|~(epred1_1(X3)))&(((p16(X45)|~(p15(X45)))|~(r1(esk18_1(X3),X45)))|~(epred1_1(X3))))&((((((~(p17(X44))|p16(X44))|~(r1(esk19_1(X3),X44)))|~(epred1_1(X3)))&(((p17(X44)|~(p16(X44)))|~(r1(esk19_1(X3),X44)))|~(epred1_1(X3))))&((((((~(p18(X43))|p17(X43))|~(r1(esk20_1(X3),X43)))|~(epred1_1(X3)))&(((p18(X43)|~(p17(X43)))|~(r1(esk20_1(X3),X43)))|~(epred1_1(X3))))&((((((~(p19(X42))|p18(X42))|~(r1(esk21_1(X3),X42)))|~(epred1_1(X3)))&(((p19(X42)|~(p18(X42)))|~(r1(esk21_1(X3),X42)))|~(epred1_1(X3))))&((((((~(p20(X41))|p19(X41))|~(r1(esk22_1(X3),X41)))|~(epred1_1(X3)))&(((p20(X41)|~(p19(X41)))|~(r1(esk22_1(X3),X41)))|~(epred1_1(X3))))&((((((~(p21(X40))|p20(X40))|~(r1(esk23_1(X3),X40)))|~(epred1_1(X3)))&(((p21(X40)|~(p20(X40)))|~(r1(esk23_1(X3),X40)))|~(epred1_1(X3))))&((((((~(p22(X39))|p21(X39))|~(r1(esk24_1(X3),X39)))|~(epred1_1(X3)))&(((p22(X39)|~(p21(X39)))|~(r1(esk24_1(X3),X39)))|~(epred1_1(X3))))&((((((~(p23(X38))|p22(X38))|~(r1(esk25_1(X3),X38)))|~(epred1_1(X3)))&(((p23(X38)|~(p22(X38)))|~(r1(esk25_1(X3),X38)))|~(epred1_1(X3))))&((((((~(p24(X37))|p23(X37))|~(r1(esk26_1(X3),X37)))|~(epred1_1(X3)))&(((p24(X37)|~(p23(X37)))|~(r1(esk26_1(X3),X37)))|~(epred1_1(X3))))&((((((~(p25(X36))|p24(X36))|~(r1(esk27_1(X3),X36)))|~(epred1_1(X3)))&(((p25(X36)|~(p24(X36)))|~(r1(esk27_1(X3),X36)))|~(epred1_1(X3))))&((((((~(p26(X35))|p25(X35))|~(r1(esk28_1(X3),X35)))|~(epred1_1(X3)))&(((p26(X35)|~(p25(X35)))|~(r1(esk28_1(X3),X35)))|~(epred1_1(X3))))&((((((~(p27(X34))|p26(X34))|~(r1(esk29_1(X3),X34)))|~(epred1_1(X3)))&(((p27(X34)|~(p26(X34)))|~(r1(esk29_1(X3),X34)))|~(epred1_1(X3))))&((((((~(p28(X33))|p27(X33))|~(r1(esk30_1(X3),X33)))|~(epred1_1(X3)))&(((p28(X33)|~(p27(X33)))|~(r1(esk30_1(X3),X33)))|~(epred1_1(X3))))&((((((~(p29(X32))|p28(X32))|~(r1(esk31_1(X3),X32)))|~(epred1_1(X3)))&(((p29(X32)|~(p28(X32)))|~(r1(esk31_1(X3),X32)))|~(epred1_1(X3))))&((r1(esk30_1(X3),esk31_1(X3))|~(epred1_1(X3)))&(r1(esk31_1(X3),esk32_1(X3))|~(epred1_1(X3)))))&(r1(esk29_1(X3),esk30_1(X3))|~(epred1_1(X3)))))&(r1(esk28_1(X3),esk29_1(X3))|~(epred1_1(X3)))))&(r1(esk27_1(X3),esk28_1(X3))|~(epred1_1(X3)))))&(r1(esk26_1(X3),esk27_1(X3))|~(epred1_1(X3)))))&(r1(esk25_1(X3),esk26_1(X3))|~(epred1_1(X3)))))&(r1(esk24_1(X3),esk25_1(X3))|~(epred1_1(X3)))))&(r1(esk23_1(X3),esk24_1(X3))|~(epred1_1(X3)))))&(r1(esk22_1(X3),esk23_1(X3))|~(epred1_1(X3)))))&(r1(esk21_1(X3),esk22_1(X3))|~(epred1_1(X3)))))&(r1(esk20_1(X3),esk21_1(X3))|~(epred1_1(X3)))))&(r1(esk19_1(X3),esk20_1(X3))|~(epred1_1(X3)))))&(r1(esk18_1(X3),esk19_1(X3))|~(epred1_1(X3)))))&(r1(esk17_1(X3),esk18_1(X3))|~(epred1_1(X3)))))&(r1(esk16_1(X3),esk17_1(X3))|~(epred1_1(X3)))))&(r1(esk15_1(X3),esk16_1(X3))|~(epred1_1(X3)))))&(r1(esk14_1(X3),esk15_1(X3))|~(epred1_1(X3)))))&(r1(esk13_1(X3),esk14_1(X3))|~(epred1_1(X3)))))&(r1(esk12_1(X3),esk13_1(X3))|~(epred1_1(X3)))))&(r1(esk11_1(X3),esk12_1(X3))|~(epred1_1(X3)))))&(r1(esk10_1(X3),esk11_1(X3))|~(epred1_1(X3)))))&(r1(esk9_1(X3),esk10_1(X3))|~(epred1_1(X3)))))&(r1(esk8_1(X3),esk9_1(X3))|~(epred1_1(X3)))))&(r1(esk7_1(X3),esk8_1(X3))|~(epred1_1(X3)))))&(r1(esk6_1(X3),esk7_1(X3))|~(epred1_1(X3)))))&(r1(esk5_1(X3),esk6_1(X3))|~(epred1_1(X3)))))&(r1(X3,esk5_1(X3))|~(epred1_1(X3))))))&((r1(X3,esk33_1(X3))|~(epred1_1(X3)))&(~(p30(esk33_1(X3)))|~(epred1_1(X3)))))&(((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X3,esk34_1(X3))|~(epred1_1(X3)))&((p28(esk34_1(X3))|p29(esk34_1(X3)))|~(epred1_1(X3))))&((~(p29(esk34_1(X3)))|~(p28(esk34_1(X3))))|~(epred1_1(X3))))&((p27(esk34_1(X3))|p28(esk34_1(X3)))|~(epred1_1(X3))))&((~(p28(esk34_1(X3)))|~(p27(esk34_1(X3))))|~(epred1_1(X3))))&((p26(esk34_1(X3))|p27(esk34_1(X3)))|~(epred1_1(X3))))&((~(p27(esk34_1(X3)))|~(p26(esk34_1(X3))))|~(epred1_1(X3))))&((p25(esk34_1(X3))|p26(esk34_1(X3)))|~(epred1_1(X3))))&((~(p26(esk34_1(X3)))|~(p25(esk34_1(X3))))|~(epred1_1(X3))))&((p24(esk34_1(X3))|p25(esk34_1(X3)))|~(epred1_1(X3))))&((~(p25(esk34_1(X3)))|~(p24(esk34_1(X3))))|~(epred1_1(X3))))&((p23(esk34_1(X3))|p24(esk34_1(X3)))|~(epred1_1(X3))))&((~(p24(esk34_1(X3)))|~(p23(esk34_1(X3))))|~(epred1_1(X3))))&((p22(esk34_1(X3))|p23(esk34_1(X3)))|~(epred1_1(X3))))&((~(p23(esk34_1(X3)))|~(p22(esk34_1(X3))))|~(epred1_1(X3))))&((p21(esk34_1(X3))|p22(esk34_1(X3)))|~(epred1_1(X3))))&((~(p22(esk34_1(X3)))|~(p21(esk34_1(X3))))|~(epred1_1(X3))))&((p20(esk34_1(X3))|p21(esk34_1(X3)))|~(epred1_1(X3))))&((~(p21(esk34_1(X3)))|~(p20(esk34_1(X3))))|~(epred1_1(X3))))&((p19(esk34_1(X3))|p20(esk34_1(X3)))|~(epred1_1(X3))))&((~(p20(esk34_1(X3)))|~(p19(esk34_1(X3))))|~(epred1_1(X3))))&((p18(esk34_1(X3))|p19(esk34_1(X3)))|~(epred1_1(X3))))&((~(p19(esk34_1(X3)))|~(p18(esk34_1(X3))))|~(epred1_1(X3))))&((p17(esk34_1(X3))|p18(esk34_1(X3)))|~(epred1_1(X3))))&((~(p18(esk34_1(X3)))|~(p17(esk34_1(X3))))|~(epred1_1(X3))))&((p16(esk34_1(X3))|p17(esk34_1(X3)))|~(epred1_1(X3))))&((~(p17(esk34_1(X3)))|~(p16(esk34_1(X3))))|~(epred1_1(X3))))&((p15(esk34_1(X3))|p16(esk34_1(X3)))|~(epred1_1(X3))))&((~(p16(esk34_1(X3)))|~(p15(esk34_1(X3))))|~(epred1_1(X3))))&((p14(esk34_1(X3))|p15(esk34_1(X3)))|~(epred1_1(X3))))&((~(p15(esk34_1(X3)))|~(p14(esk34_1(X3))))|~(epred1_1(X3))))&((p13(esk34_1(X3))|p14(esk34_1(X3)))|~(epred1_1(X3))))&((~(p14(esk34_1(X3)))|~(p13(esk34_1(X3))))|~(epred1_1(X3))))&((p12(esk34_1(X3))|p13(esk34_1(X3)))|~(epred1_1(X3))))&((~(p13(esk34_1(X3)))|~(p12(esk34_1(X3))))|~(epred1_1(X3))))&((p11(esk34_1(X3))|p12(esk34_1(X3)))|~(epred1_1(X3))))&((~(p12(esk34_1(X3)))|~(p11(esk34_1(X3))))|~(epred1_1(X3))))&((p10(esk34_1(X3))|p11(esk34_1(X3)))|~(epred1_1(X3))))&((~(p11(esk34_1(X3)))|~(p10(esk34_1(X3))))|~(epred1_1(X3))))&((p9(esk34_1(X3))|p10(esk34_1(X3)))|~(epred1_1(X3))))&((~(p10(esk34_1(X3)))|~(p9(esk34_1(X3))))|~(epred1_1(X3))))&((p8(esk34_1(X3))|p9(esk34_1(X3)))|~(epred1_1(X3))))&((~(p9(esk34_1(X3)))|~(p8(esk34_1(X3))))|~(epred1_1(X3))))&((p7(esk34_1(X3))|p8(esk34_1(X3)))|~(epred1_1(X3))))&((~(p8(esk34_1(X3)))|~(p7(esk34_1(X3))))|~(epred1_1(X3))))&((p6(esk34_1(X3))|p7(esk34_1(X3)))|~(epred1_1(X3))))&((~(p7(esk34_1(X3)))|~(p6(esk34_1(X3))))|~(epred1_1(X3))))&((p5(esk34_1(X3))|p6(esk34_1(X3)))|~(epred1_1(X3))))&((~(p6(esk34_1(X3)))|~(p5(esk34_1(X3))))|~(epred1_1(X3))))&((p4(esk34_1(X3))|p5(esk34_1(X3)))|~(epred1_1(X3))))&((~(p5(esk34_1(X3)))|~(p4(esk34_1(X3))))|~(epred1_1(X3))))&((p3(esk34_1(X3))|p4(esk34_1(X3)))|~(epred1_1(X3))))&((~(p4(esk34_1(X3)))|~(p3(esk34_1(X3))))|~(epred1_1(X3))))&((p2(esk34_1(X3))|p3(esk34_1(X3)))|~(epred1_1(X3))))&((~(p3(esk34_1(X3)))|~(p2(esk34_1(X3))))|~(epred1_1(X3))))&((p1(esk34_1(X3))|p2(esk34_1(X3)))|~(epred1_1(X3))))&((~(p2(esk34_1(X3)))|~(p1(esk34_1(X3))))|~(epred1_1(X3))))),inference(distribute,[status(thm)],[26])).
% cnf(28,plain,(~epred1_1(X1)|~p1(esk34_1(X1))|~p2(esk34_1(X1))),inference(split_conjunct,[status(thm)],[27])).
% cnf(29,plain,(p2(esk34_1(X1))|p1(esk34_1(X1))|~epred1_1(X1)),inference(split_conjunct,[status(thm)],[27])).
% cnf(84,plain,(r1(X1,esk34_1(X1))|~epred1_1(X1)),inference(split_conjunct,[status(thm)],[27])).
% cnf(169,plain,(p2(X2)|~epred1_1(X1)|~r1(X1,X2)|~p1(X2)),inference(split_conjunct,[status(thm)],[27])).
% cnf(170,plain,(p1(X2)|~epred1_1(X1)|~r1(X1,X2)|~p2(X2)),inference(split_conjunct,[status(thm)],[27])).
% cnf(171,negated_conjecture,(epred1_1(esk4_0)),inference(spm,[status(thm)],[22,9,theory(equality)])).
% cnf(182,plain,(p1(esk34_1(X1))|~epred1_1(X1)|~p2(esk34_1(X1))),inference(spm,[status(thm)],[170,84,theory(equality)])).
% cnf(194,plain,(p2(esk34_1(X1))|~epred1_1(X1)|~p1(esk34_1(X1))),inference(spm,[status(thm)],[169,84,theory(equality)])).
% cnf(776,plain,(p1(esk34_1(X1))|~epred1_1(X1)),inference(csr,[status(thm)],[182,29])).
% cnf(778,plain,(~epred1_1(X1)|~p2(esk34_1(X1))),inference(spm,[status(thm)],[28,776,theory(equality)])).
% cnf(930,plain,(p2(esk34_1(X1))|~epred1_1(X1)),inference(csr,[status(thm)],[194,776])).
% cnf(931,plain,(~epred1_1(X1)),inference(csr,[status(thm)],[930,778])).
% cnf(932,negated_conjecture,($false),inference(sr,[status(thm)],[171,931,theory(equality)])).
% cnf(933,negated_conjecture,($false),932,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 386
% # ...of these trivial : 0
% # ...subsumed : 6
% # ...remaining for further processing: 380
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 41
% # Backward-rewritten : 0
% # Generated clauses : 732
% # ...of the previous two non-trivial : 661
% # Contextual simplify-reflections : 5
% # Paramodulations : 725
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 181
% # Positive orientable unit clauses: 7
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 1
% # Non-unit-clauses : 173
% # Current number of unprocessed clauses: 575
% # ...number of literals in the above : 2270
% # Clause-clause subsumption calls (NU) : 5952
% # Rec. Clause-clause subsumption calls : 5002
% # Unit Clause-clause subsumption calls : 421
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 6
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 192 leaves, 1.20+/-0.470 terms/leaf
% # Paramod-from index: 70 leaves, 1.03+/-0.167 terms/leaf
% # Paramod-into index: 145 leaves, 1.24+/-0.444 terms/leaf
% # -------------------------------------------------
% # User time : 0.069 s
% # System time : 0.008 s
% # Total time : 0.077 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.19 CPU 0.27 WC
% FINAL PrfWatch: 0.19 CPU 0.27 WC
% SZS output end Solution for /tmp/SystemOnTPTP2373/LCL686+1.010.tptp
%
%------------------------------------------------------------------------------