%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LCL686+1.015 : 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:28 EST 2010
% Result : Theorem 1.10s
% Output : Solution 1.10s
% 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/SystemOnTPTP2632/LCL686+1.015.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP2632/LCL686+1.015.tptp
% SZS output start Solution for /tmp/SystemOnTPTP2632/LCL686+1.015.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 2728
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.054 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))|~(p45(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))|![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))|~($true)))|~(![X2]:(~(r1(X1,X2))|~(((p44(X2)&~(p43(X2)))|(~(p44(X2))&p43(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p43(X1)&~(p42(X1)))|(~(p43(X1))&p42(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p42(X2)&~(p41(X2)))|(~(p42(X2))&p41(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p41(X1)&~(p40(X1)))|(~(p41(X1))&p40(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p40(X2)&~(p39(X2)))|(~(p40(X2))&p39(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p39(X1)&~(p38(X1)))|(~(p39(X1))&p38(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p38(X2)&~(p37(X2)))|(~(p38(X2))&p37(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p37(X1)&~(p36(X1)))|(~(p37(X1))&p36(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p36(X2)&~(p35(X2)))|(~(p36(X2))&p35(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p35(X1)&~(p34(X1)))|(~(p35(X1))&p34(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p34(X2)&~(p33(X2)))|(~(p34(X2))&p33(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p33(X1)&~(p32(X1)))|(~(p33(X1))&p32(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p32(X2)&~(p31(X2)))|(~(p32(X2))&p31(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p31(X1)&~(p30(X1)))|(~(p31(X1))&p30(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p30(X2)&~(p29(X2)))|(~(p30(X2))&p29(X2))))))))|~(![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))|p45(X2)))|![X2]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~(r1(X1,X2))|(~(p43(X2))&~(p44(X2))))|(p44(X2)&p43(X2)))|(~(p42(X2))&~(p43(X2))))|(p43(X2)&p42(X2)))|(~(p41(X2))&~(p42(X2))))|(p42(X2)&p41(X2)))|(~(p40(X2))&~(p41(X2))))|(p41(X2)&p40(X2)))|(~(p39(X2))&~(p40(X2))))|(p40(X2)&p39(X2)))|(~(p38(X2))&~(p39(X2))))|(p39(X2)&p38(X2)))|(~(p37(X2))&~(p38(X2))))|(p38(X2)&p37(X2)))|(~(p36(X2))&~(p37(X2))))|(p37(X2)&p36(X2)))|(~(p35(X2))&~(p36(X2))))|(p36(X2)&p35(X2)))|(~(p34(X2))&~(p35(X2))))|(p35(X2)&p34(X2)))|(~(p33(X2))&~(p34(X2))))|(p34(X2)&p33(X2)))|(~(p32(X2))&~(p33(X2))))|(p33(X2)&p32(X2)))|(~(p31(X2))&~(p32(X2))))|(p32(X2)&p31(X2)))|(~(p30(X2))&~(p31(X2))))|(p31(X2)&p30(X2)))|(~(p29(X2))&~(p30(X2))))|(p30(X2)&p29(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))|~(p45(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))|![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))|~($true)))|~(![X2]:(~(r1(X1,X2))|~(((p44(X2)&~(p43(X2)))|(~(p44(X2))&p43(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p43(X1)&~(p42(X1)))|(~(p43(X1))&p42(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p42(X2)&~(p41(X2)))|(~(p42(X2))&p41(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p41(X1)&~(p40(X1)))|(~(p41(X1))&p40(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p40(X2)&~(p39(X2)))|(~(p40(X2))&p39(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p39(X1)&~(p38(X1)))|(~(p39(X1))&p38(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p38(X2)&~(p37(X2)))|(~(p38(X2))&p37(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p37(X1)&~(p36(X1)))|(~(p37(X1))&p36(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p36(X2)&~(p35(X2)))|(~(p36(X2))&p35(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p35(X1)&~(p34(X1)))|(~(p35(X1))&p34(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p34(X2)&~(p33(X2)))|(~(p34(X2))&p33(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p33(X1)&~(p32(X1)))|(~(p33(X1))&p32(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p32(X2)&~(p31(X2)))|(~(p32(X2))&p31(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p31(X1)&~(p30(X1)))|(~(p31(X1))&p30(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p30(X2)&~(p29(X2)))|(~(p30(X2))&p29(X2))))))))|~(![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))|p45(X2)))|![X2]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~(r1(X1,X2))|(~(p43(X2))&~(p44(X2))))|(p44(X2)&p43(X2)))|(~(p42(X2))&~(p43(X2))))|(p43(X2)&p42(X2)))|(~(p41(X2))&~(p42(X2))))|(p42(X2)&p41(X2)))|(~(p40(X2))&~(p41(X2))))|(p41(X2)&p40(X2)))|(~(p39(X2))&~(p40(X2))))|(p40(X2)&p39(X2)))|(~(p38(X2))&~(p39(X2))))|(p39(X2)&p38(X2)))|(~(p37(X2))&~(p38(X2))))|(p38(X2)&p37(X2)))|(~(p36(X2))&~(p37(X2))))|(p37(X2)&p36(X2)))|(~(p35(X2))&~(p36(X2))))|(p36(X2)&p35(X2)))|(~(p34(X2))&~(p35(X2))))|(p35(X2)&p34(X2)))|(~(p33(X2))&~(p34(X2))))|(p34(X2)&p33(X2)))|(~(p32(X2))&~(p33(X2))))|(p33(X2)&p32(X2)))|(~(p31(X2))&~(p32(X2))))|(p32(X2)&p31(X2)))|(~(p30(X2))&~(p31(X2))))|(p31(X2)&p30(X2)))|(~(p29(X2))&~(p30(X2))))|(p30(X2)&p29(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))|~(p45(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))|![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)))|~(![X2]:(~(r1(X1,X2))|~(((p44(X2)&~(p43(X2)))|(~(p44(X2))&p43(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p43(X1)&~(p42(X1)))|(~(p43(X1))&p42(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p42(X2)&~(p41(X2)))|(~(p42(X2))&p41(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p41(X1)&~(p40(X1)))|(~(p41(X1))&p40(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p40(X2)&~(p39(X2)))|(~(p40(X2))&p39(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p39(X1)&~(p38(X1)))|(~(p39(X1))&p38(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p38(X2)&~(p37(X2)))|(~(p38(X2))&p37(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p37(X1)&~(p36(X1)))|(~(p37(X1))&p36(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p36(X2)&~(p35(X2)))|(~(p36(X2))&p35(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p35(X1)&~(p34(X1)))|(~(p35(X1))&p34(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p34(X2)&~(p33(X2)))|(~(p34(X2))&p33(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p33(X1)&~(p32(X1)))|(~(p33(X1))&p32(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p32(X2)&~(p31(X2)))|(~(p32(X2))&p31(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p31(X1)&~(p30(X1)))|(~(p31(X1))&p30(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p30(X2)&~(p29(X2)))|(~(p30(X2))&p29(X2))))))))|~(![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))|p45(X2)))|![X2]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~(r1(X1,X2))|(~(p43(X2))&~(p44(X2))))|(p44(X2)&p43(X2)))|(~(p42(X2))&~(p43(X2))))|(p43(X2)&p42(X2)))|(~(p41(X2))&~(p42(X2))))|(p42(X2)&p41(X2)))|(~(p40(X2))&~(p41(X2))))|(p41(X2)&p40(X2)))|(~(p39(X2))&~(p40(X2))))|(p40(X2)&p39(X2)))|(~(p38(X2))&~(p39(X2))))|(p39(X2)&p38(X2)))|(~(p37(X2))&~(p38(X2))))|(p38(X2)&p37(X2)))|(~(p36(X2))&~(p37(X2))))|(p37(X2)&p36(X2)))|(~(p35(X2))&~(p36(X2))))|(p36(X2)&p35(X2)))|(~(p34(X2))&~(p35(X2))))|(p35(X2)&p34(X2)))|(~(p33(X2))&~(p34(X2))))|(p34(X2)&p33(X2)))|(~(p32(X2))&~(p33(X2))))|(p33(X2)&p32(X2)))|(~(p31(X2))&~(p32(X2))))|(p32(X2)&p31(X2)))|(~(p30(X2))&~(p31(X2))))|(p31(X2)&p30(X2)))|(~(p29(X2))&~(p30(X2))))|(p30(X2)&p29(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))|![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)))|~(![X2]:(~(r1(X1,X2))|~(((p44(X2)&~(p43(X2)))|(~(p44(X2))&p43(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p43(X1)&~(p42(X1)))|(~(p43(X1))&p42(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p42(X2)&~(p41(X2)))|(~(p42(X2))&p41(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p41(X1)&~(p40(X1)))|(~(p41(X1))&p40(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p40(X2)&~(p39(X2)))|(~(p40(X2))&p39(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p39(X1)&~(p38(X1)))|(~(p39(X1))&p38(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p38(X2)&~(p37(X2)))|(~(p38(X2))&p37(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p37(X1)&~(p36(X1)))|(~(p37(X1))&p36(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p36(X2)&~(p35(X2)))|(~(p36(X2))&p35(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p35(X1)&~(p34(X1)))|(~(p35(X1))&p34(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p34(X2)&~(p33(X2)))|(~(p34(X2))&p33(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p33(X1)&~(p32(X1)))|(~(p33(X1))&p32(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p32(X2)&~(p31(X2)))|(~(p32(X2))&p31(X2))))))))|~(![X1]:(~(r1(X2,X1))|~(((p31(X1)&~(p30(X1)))|(~(p31(X1))&p30(X1))))))))|~(![X2]:(~(r1(X1,X2))|~(((p30(X2)&~(p29(X2)))|(~(p30(X2))&p29(X2))))))))|~(![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))|p45(X2)))|![X2]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~(r1(X1,X2))|(~(p43(X2))&~(p44(X2))))|(p44(X2)&p43(X2)))|(~(p42(X2))&~(p43(X2))))|(p43(X2)&p42(X2)))|(~(p41(X2))&~(p42(X2))))|(p42(X2)&p41(X2)))|(~(p40(X2))&~(p41(X2))))|(p41(X2)&p40(X2)))|(~(p39(X2))&~(p40(X2))))|(p40(X2)&p39(X2)))|(~(p38(X2))&~(p39(X2))))|(p39(X2)&p38(X2)))|(~(p37(X2))&~(p38(X2))))|(p38(X2)&p37(X2)))|(~(p36(X2))&~(p37(X2))))|(p37(X2)&p36(X2)))|(~(p35(X2))&~(p36(X2))))|(p36(X2)&p35(X2)))|(~(p34(X2))&~(p35(X2))))|(p35(X2)&p34(X2)))|(~(p33(X2))&~(p34(X2))))|(p34(X2)&p33(X2)))|(~(p32(X2))&~(p33(X2))))|(p33(X2)&p32(X2)))|(~(p31(X2))&~(p32(X2))))|(p32(X2)&p31(X2)))|(~(p30(X2))&~(p31(X2))))|(p31(X2)&p30(X2)))|(~(p29(X2))&~(p30(X2))))|(p30(X2)&p29(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))|~(p45(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)&p45(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)&p45(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)&p45(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)&p45(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)&?[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))&![X2]:(~(r1(X1,X2))|((~(p44(X2))|p43(X2))&(p44(X2)|~(p43(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p43(X1))|p42(X1))&(p43(X1)|~(p42(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p42(X2))|p41(X2))&(p42(X2)|~(p41(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p41(X1))|p40(X1))&(p41(X1)|~(p40(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p40(X2))|p39(X2))&(p40(X2)|~(p39(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p39(X1))|p38(X1))&(p39(X1)|~(p38(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p38(X2))|p37(X2))&(p38(X2)|~(p37(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p37(X1))|p36(X1))&(p37(X1)|~(p36(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p36(X2))|p35(X2))&(p36(X2)|~(p35(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p35(X1))|p34(X1))&(p35(X1)|~(p34(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p34(X2))|p33(X2))&(p34(X2)|~(p33(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p33(X1))|p32(X1))&(p33(X1)|~(p32(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p32(X2))|p31(X2))&(p32(X2)|~(p31(X2)))))))&![X1]:(~(r1(X2,X1))|((~(p31(X1))|p30(X1))&(p31(X1)|~(p30(X1)))))))&![X2]:(~(r1(X1,X2))|((~(p30(X2))|p29(X2))&(p30(X2)|~(p29(X2)))))))&![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)&~(p45(X2))))&?[X2]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X1,X2)&(p43(X2)|p44(X2)))&(~(p44(X2))|~(p43(X2))))&(p42(X2)|p43(X2)))&(~(p43(X2))|~(p42(X2))))&(p41(X2)|p42(X2)))&(~(p42(X2))|~(p41(X2))))&(p40(X2)|p41(X2)))&(~(p41(X2))|~(p40(X2))))&(p39(X2)|p40(X2)))&(~(p40(X2))|~(p39(X2))))&(p38(X2)|p39(X2)))&(~(p39(X2))|~(p38(X2))))&(p37(X2)|p38(X2)))&(~(p38(X2))|~(p37(X2))))&(p36(X2)|p37(X2)))&(~(p37(X2))|~(p36(X2))))&(p35(X2)|p36(X2)))&(~(p36(X2))|~(p35(X2))))&(p34(X2)|p35(X2)))&(~(p35(X2))|~(p34(X2))))&(p33(X2)|p34(X2)))&(~(p34(X2))|~(p33(X2))))&(p32(X2)|p33(X2)))&(~(p33(X2))|~(p32(X2))))&(p31(X2)|p32(X2)))&(~(p32(X2))|~(p31(X2))))&(p30(X2)|p31(X2)))&(~(p31(X2))|~(p30(X2))))&(p29(X2)|p30(X2)))&(~(p30(X2))|~(p29(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(X31,X32)&?[X33]:((r1(X32,X33)&?[X34]:((r1(X33,X34)&?[X35]:((r1(X34,X35)&?[X36]:((r1(X35,X36)&?[X37]:((r1(X36,X37)&?[X38]:((r1(X37,X38)&?[X39]:((r1(X38,X39)&?[X40]:((r1(X39,X40)&?[X41]:((r1(X40,X41)&?[X42]:((r1(X41,X42)&?[X43]:((r1(X42,X43)&?[X44]:((r1(X43,X44)&?[X45]:((r1(X44,X45)&?[X46]:r1(X45,X46))&![X47]:(~(r1(X45,X47))|((~(p44(X47))|p43(X47))&(p44(X47)|~(p43(X47)))))))&![X48]:(~(r1(X44,X48))|((~(p43(X48))|p42(X48))&(p43(X48)|~(p42(X48)))))))&![X49]:(~(r1(X43,X49))|((~(p42(X49))|p41(X49))&(p42(X49)|~(p41(X49)))))))&![X50]:(~(r1(X42,X50))|((~(p41(X50))|p40(X50))&(p41(X50)|~(p40(X50)))))))&![X51]:(~(r1(X41,X51))|((~(p40(X51))|p39(X51))&(p40(X51)|~(p39(X51)))))))&![X52]:(~(r1(X40,X52))|((~(p39(X52))|p38(X52))&(p39(X52)|~(p38(X52)))))))&![X53]:(~(r1(X39,X53))|((~(p38(X53))|p37(X53))&(p38(X53)|~(p37(X53)))))))&![X54]:(~(r1(X38,X54))|((~(p37(X54))|p36(X54))&(p37(X54)|~(p36(X54)))))))&![X55]:(~(r1(X37,X55))|((~(p36(X55))|p35(X55))&(p36(X55)|~(p35(X55)))))))&![X56]:(~(r1(X36,X56))|((~(p35(X56))|p34(X56))&(p35(X56)|~(p34(X56)))))))&![X57]:(~(r1(X35,X57))|((~(p34(X57))|p33(X57))&(p34(X57)|~(p33(X57)))))))&![X58]:(~(r1(X34,X58))|((~(p33(X58))|p32(X58))&(p33(X58)|~(p32(X58)))))))&![X59]:(~(r1(X33,X59))|((~(p32(X59))|p31(X59))&(p32(X59)|~(p31(X59)))))))&![X60]:(~(r1(X32,X60))|((~(p31(X60))|p30(X60))&(p31(X60)|~(p30(X60)))))))&![X61]:(~(r1(X31,X61))|((~(p30(X61))|p29(X61))&(p30(X61)|~(p29(X61)))))))&![X62]:(~(r1(X30,X62))|((~(p29(X62))|p28(X62))&(p29(X62)|~(p28(X62)))))))&![X63]:(~(r1(X29,X63))|((~(p28(X63))|p27(X63))&(p28(X63)|~(p27(X63)))))))&![X64]:(~(r1(X28,X64))|((~(p27(X64))|p26(X64))&(p27(X64)|~(p26(X64)))))))&![X65]:(~(r1(X27,X65))|((~(p26(X65))|p25(X65))&(p26(X65)|~(p25(X65)))))))&![X66]:(~(r1(X26,X66))|((~(p25(X66))|p24(X66))&(p25(X66)|~(p24(X66)))))))&![X67]:(~(r1(X25,X67))|((~(p24(X67))|p23(X67))&(p24(X67)|~(p23(X67)))))))&![X68]:(~(r1(X24,X68))|((~(p23(X68))|p22(X68))&(p23(X68)|~(p22(X68)))))))&![X69]:(~(r1(X23,X69))|((~(p22(X69))|p21(X69))&(p22(X69)|~(p21(X69)))))))&![X70]:(~(r1(X22,X70))|((~(p21(X70))|p20(X70))&(p21(X70)|~(p20(X70)))))))&![X71]:(~(r1(X21,X71))|((~(p20(X71))|p19(X71))&(p20(X71)|~(p19(X71)))))))&![X72]:(~(r1(X20,X72))|((~(p19(X72))|p18(X72))&(p19(X72)|~(p18(X72)))))))&![X73]:(~(r1(X19,X73))|((~(p18(X73))|p17(X73))&(p18(X73)|~(p17(X73)))))))&![X74]:(~(r1(X18,X74))|((~(p17(X74))|p16(X74))&(p17(X74)|~(p16(X74)))))))&![X75]:(~(r1(X17,X75))|((~(p16(X75))|p15(X75))&(p16(X75)|~(p15(X75)))))))&![X76]:(~(r1(X16,X76))|((~(p15(X76))|p14(X76))&(p15(X76)|~(p14(X76)))))))&![X77]:(~(r1(X15,X77))|((~(p14(X77))|p13(X77))&(p14(X77)|~(p13(X77)))))))&![X78]:(~(r1(X14,X78))|((~(p13(X78))|p12(X78))&(p13(X78)|~(p12(X78)))))))&![X79]:(~(r1(X13,X79))|((~(p12(X79))|p11(X79))&(p12(X79)|~(p11(X79)))))))&![X80]:(~(r1(X12,X80))|((~(p11(X80))|p10(X80))&(p11(X80)|~(p10(X80)))))))&![X81]:(~(r1(X11,X81))|((~(p10(X81))|p9(X81))&(p10(X81)|~(p9(X81)))))))&![X82]:(~(r1(X10,X82))|((~(p9(X82))|p8(X82))&(p9(X82)|~(p8(X82)))))))&![X83]:(~(r1(X9,X83))|((~(p8(X83))|p7(X83))&(p8(X83)|~(p7(X83)))))))&![X84]:(~(r1(X8,X84))|((~(p7(X84))|p6(X84))&(p7(X84)|~(p6(X84)))))))&![X85]:(~(r1(X7,X85))|((~(p6(X85))|p5(X85))&(p6(X85)|~(p5(X85)))))))&![X86]:(~(r1(X6,X86))|((~(p5(X86))|p4(X86))&(p5(X86)|~(p4(X86)))))))&![X87]:(~(r1(X5,X87))|((~(p4(X87))|p3(X87))&(p4(X87)|~(p3(X87)))))))&![X88]:(~(r1(X4,X88))|((~(p3(X88))|p2(X88))&(p3(X88)|~(p2(X88))))))&![X89]:(~(r1(X3,X89))|((~(p2(X89))|p1(X89))&(p2(X89)|~(p1(X89))))))&?[X90]:(r1(X3,X90)&~(p45(X90))))&?[X91]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X3,X91)&(p43(X91)|p44(X91)))&(~(p44(X91))|~(p43(X91))))&(p42(X91)|p43(X91)))&(~(p43(X91))|~(p42(X91))))&(p41(X91)|p42(X91)))&(~(p42(X91))|~(p41(X91))))&(p40(X91)|p41(X91)))&(~(p41(X91))|~(p40(X91))))&(p39(X91)|p40(X91)))&(~(p40(X91))|~(p39(X91))))&(p38(X91)|p39(X91)))&(~(p39(X91))|~(p38(X91))))&(p37(X91)|p38(X91)))&(~(p38(X91))|~(p37(X91))))&(p36(X91)|p37(X91)))&(~(p37(X91))|~(p36(X91))))&(p35(X91)|p36(X91)))&(~(p36(X91))|~(p35(X91))))&(p34(X91)|p35(X91)))&(~(p35(X91))|~(p34(X91))))&(p33(X91)|p34(X91)))&(~(p34(X91))|~(p33(X91))))&(p32(X91)|p33(X91)))&(~(p33(X91))|~(p32(X91))))&(p31(X91)|p32(X91)))&(~(p32(X91))|~(p31(X91))))&(p30(X91)|p31(X91)))&(~(p31(X91))|~(p30(X91))))&(p29(X91)|p30(X91)))&(~(p30(X91))|~(p29(X91))))&(p28(X91)|p29(X91)))&(~(p29(X91))|~(p28(X91))))&(p27(X91)|p28(X91)))&(~(p28(X91))|~(p27(X91))))&(p26(X91)|p27(X91)))&(~(p27(X91))|~(p26(X91))))&(p25(X91)|p26(X91)))&(~(p26(X91))|~(p25(X91))))&(p24(X91)|p25(X91)))&(~(p25(X91))|~(p24(X91))))&(p23(X91)|p24(X91)))&(~(p24(X91))|~(p23(X91))))&(p22(X91)|p23(X91)))&(~(p23(X91))|~(p22(X91))))&(p21(X91)|p22(X91)))&(~(p22(X91))|~(p21(X91))))&(p20(X91)|p21(X91)))&(~(p21(X91))|~(p20(X91))))&(p19(X91)|p20(X91)))&(~(p20(X91))|~(p19(X91))))&(p18(X91)|p19(X91)))&(~(p19(X91))|~(p18(X91))))&(p17(X91)|p18(X91)))&(~(p18(X91))|~(p17(X91))))&(p16(X91)|p17(X91)))&(~(p17(X91))|~(p16(X91))))&(p15(X91)|p16(X91)))&(~(p16(X91))|~(p15(X91))))&(p14(X91)|p15(X91)))&(~(p15(X91))|~(p14(X91))))&(p13(X91)|p14(X91)))&(~(p14(X91))|~(p13(X91))))&(p12(X91)|p13(X91)))&(~(p13(X91))|~(p12(X91))))&(p11(X91)|p12(X91)))&(~(p12(X91))|~(p11(X91))))&(p10(X91)|p11(X91)))&(~(p11(X91))|~(p10(X91))))&(p9(X91)|p10(X91)))&(~(p10(X91))|~(p9(X91))))&(p8(X91)|p9(X91)))&(~(p9(X91))|~(p8(X91))))&(p7(X91)|p8(X91)))&(~(p8(X91))|~(p7(X91))))&(p6(X91)|p7(X91)))&(~(p7(X91))|~(p6(X91))))&(p5(X91)|p6(X91)))&(~(p6(X91))|~(p5(X91))))&(p4(X91)|p5(X91)))&(~(p5(X91))|~(p4(X91))))&(p3(X91)|p4(X91)))&(~(p4(X91))|~(p3(X91))))&(p2(X91)|p3(X91)))&(~(p3(X91))|~(p2(X91))))&(p1(X91)|p2(X91)))&(~(p2(X91))|~(p1(X91)))))),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))&((r1(esk32_1(X3),esk33_1(X3))&((r1(esk33_1(X3),esk34_1(X3))&((r1(esk34_1(X3),esk35_1(X3))&((r1(esk35_1(X3),esk36_1(X3))&((r1(esk36_1(X3),esk37_1(X3))&((r1(esk37_1(X3),esk38_1(X3))&((r1(esk38_1(X3),esk39_1(X3))&((r1(esk39_1(X3),esk40_1(X3))&((r1(esk40_1(X3),esk41_1(X3))&((r1(esk41_1(X3),esk42_1(X3))&((r1(esk42_1(X3),esk43_1(X3))&((r1(esk43_1(X3),esk44_1(X3))&((r1(esk44_1(X3),esk45_1(X3))&((r1(esk45_1(X3),esk46_1(X3))&r1(esk46_1(X3),esk47_1(X3)))&![X47]:(~(r1(esk46_1(X3),X47))|((~(p44(X47))|p43(X47))&(p44(X47)|~(p43(X47)))))))&![X48]:(~(r1(esk45_1(X3),X48))|((~(p43(X48))|p42(X48))&(p43(X48)|~(p42(X48)))))))&![X49]:(~(r1(esk44_1(X3),X49))|((~(p42(X49))|p41(X49))&(p42(X49)|~(p41(X49)))))))&![X50]:(~(r1(esk43_1(X3),X50))|((~(p41(X50))|p40(X50))&(p41(X50)|~(p40(X50)))))))&![X51]:(~(r1(esk42_1(X3),X51))|((~(p40(X51))|p39(X51))&(p40(X51)|~(p39(X51)))))))&![X52]:(~(r1(esk41_1(X3),X52))|((~(p39(X52))|p38(X52))&(p39(X52)|~(p38(X52)))))))&![X53]:(~(r1(esk40_1(X3),X53))|((~(p38(X53))|p37(X53))&(p38(X53)|~(p37(X53)))))))&![X54]:(~(r1(esk39_1(X3),X54))|((~(p37(X54))|p36(X54))&(p37(X54)|~(p36(X54)))))))&![X55]:(~(r1(esk38_1(X3),X55))|((~(p36(X55))|p35(X55))&(p36(X55)|~(p35(X55)))))))&![X56]:(~(r1(esk37_1(X3),X56))|((~(p35(X56))|p34(X56))&(p35(X56)|~(p34(X56)))))))&![X57]:(~(r1(esk36_1(X3),X57))|((~(p34(X57))|p33(X57))&(p34(X57)|~(p33(X57)))))))&![X58]:(~(r1(esk35_1(X3),X58))|((~(p33(X58))|p32(X58))&(p33(X58)|~(p32(X58)))))))&![X59]:(~(r1(esk34_1(X3),X59))|((~(p32(X59))|p31(X59))&(p32(X59)|~(p31(X59)))))))&![X60]:(~(r1(esk33_1(X3),X60))|((~(p31(X60))|p30(X60))&(p31(X60)|~(p30(X60)))))))&![X61]:(~(r1(esk32_1(X3),X61))|((~(p30(X61))|p29(X61))&(p30(X61)|~(p29(X61)))))))&![X62]:(~(r1(esk31_1(X3),X62))|((~(p29(X62))|p28(X62))&(p29(X62)|~(p28(X62)))))))&![X63]:(~(r1(esk30_1(X3),X63))|((~(p28(X63))|p27(X63))&(p28(X63)|~(p27(X63)))))))&![X64]:(~(r1(esk29_1(X3),X64))|((~(p27(X64))|p26(X64))&(p27(X64)|~(p26(X64)))))))&![X65]:(~(r1(esk28_1(X3),X65))|((~(p26(X65))|p25(X65))&(p26(X65)|~(p25(X65)))))))&![X66]:(~(r1(esk27_1(X3),X66))|((~(p25(X66))|p24(X66))&(p25(X66)|~(p24(X66)))))))&![X67]:(~(r1(esk26_1(X3),X67))|((~(p24(X67))|p23(X67))&(p24(X67)|~(p23(X67)))))))&![X68]:(~(r1(esk25_1(X3),X68))|((~(p23(X68))|p22(X68))&(p23(X68)|~(p22(X68)))))))&![X69]:(~(r1(esk24_1(X3),X69))|((~(p22(X69))|p21(X69))&(p22(X69)|~(p21(X69)))))))&![X70]:(~(r1(esk23_1(X3),X70))|((~(p21(X70))|p20(X70))&(p21(X70)|~(p20(X70)))))))&![X71]:(~(r1(esk22_1(X3),X71))|((~(p20(X71))|p19(X71))&(p20(X71)|~(p19(X71)))))))&![X72]:(~(r1(esk21_1(X3),X72))|((~(p19(X72))|p18(X72))&(p19(X72)|~(p18(X72)))))))&![X73]:(~(r1(esk20_1(X3),X73))|((~(p18(X73))|p17(X73))&(p18(X73)|~(p17(X73)))))))&![X74]:(~(r1(esk19_1(X3),X74))|((~(p17(X74))|p16(X74))&(p17(X74)|~(p16(X74)))))))&![X75]:(~(r1(esk18_1(X3),X75))|((~(p16(X75))|p15(X75))&(p16(X75)|~(p15(X75)))))))&![X76]:(~(r1(esk17_1(X3),X76))|((~(p15(X76))|p14(X76))&(p15(X76)|~(p14(X76)))))))&![X77]:(~(r1(esk16_1(X3),X77))|((~(p14(X77))|p13(X77))&(p14(X77)|~(p13(X77)))))))&![X78]:(~(r1(esk15_1(X3),X78))|((~(p13(X78))|p12(X78))&(p13(X78)|~(p12(X78)))))))&![X79]:(~(r1(esk14_1(X3),X79))|((~(p12(X79))|p11(X79))&(p12(X79)|~(p11(X79)))))))&![X80]:(~(r1(esk13_1(X3),X80))|((~(p11(X80))|p10(X80))&(p11(X80)|~(p10(X80)))))))&![X81]:(~(r1(esk12_1(X3),X81))|((~(p10(X81))|p9(X81))&(p10(X81)|~(p9(X81)))))))&![X82]:(~(r1(esk11_1(X3),X82))|((~(p9(X82))|p8(X82))&(p9(X82)|~(p8(X82)))))))&![X83]:(~(r1(esk10_1(X3),X83))|((~(p8(X83))|p7(X83))&(p8(X83)|~(p7(X83)))))))&![X84]:(~(r1(esk9_1(X3),X84))|((~(p7(X84))|p6(X84))&(p7(X84)|~(p6(X84)))))))&![X85]:(~(r1(esk8_1(X3),X85))|((~(p6(X85))|p5(X85))&(p6(X85)|~(p5(X85)))))))&![X86]:(~(r1(esk7_1(X3),X86))|((~(p5(X86))|p4(X86))&(p5(X86)|~(p4(X86)))))))&![X87]:(~(r1(esk6_1(X3),X87))|((~(p4(X87))|p3(X87))&(p4(X87)|~(p3(X87)))))))&![X88]:(~(r1(esk5_1(X3),X88))|((~(p3(X88))|p2(X88))&(p3(X88)|~(p2(X88))))))&![X89]:(~(r1(X3,X89))|((~(p2(X89))|p1(X89))&(p2(X89)|~(p1(X89))))))&(r1(X3,esk48_1(X3))&~(p45(esk48_1(X3)))))&((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X3,esk49_1(X3))&(p43(esk49_1(X3))|p44(esk49_1(X3))))&(~(p44(esk49_1(X3)))|~(p43(esk49_1(X3)))))&(p42(esk49_1(X3))|p43(esk49_1(X3))))&(~(p43(esk49_1(X3)))|~(p42(esk49_1(X3)))))&(p41(esk49_1(X3))|p42(esk49_1(X3))))&(~(p42(esk49_1(X3)))|~(p41(esk49_1(X3)))))&(p40(esk49_1(X3))|p41(esk49_1(X3))))&(~(p41(esk49_1(X3)))|~(p40(esk49_1(X3)))))&(p39(esk49_1(X3))|p40(esk49_1(X3))))&(~(p40(esk49_1(X3)))|~(p39(esk49_1(X3)))))&(p38(esk49_1(X3))|p39(esk49_1(X3))))&(~(p39(esk49_1(X3)))|~(p38(esk49_1(X3)))))&(p37(esk49_1(X3))|p38(esk49_1(X3))))&(~(p38(esk49_1(X3)))|~(p37(esk49_1(X3)))))&(p36(esk49_1(X3))|p37(esk49_1(X3))))&(~(p37(esk49_1(X3)))|~(p36(esk49_1(X3)))))&(p35(esk49_1(X3))|p36(esk49_1(X3))))&(~(p36(esk49_1(X3)))|~(p35(esk49_1(X3)))))&(p34(esk49_1(X3))|p35(esk49_1(X3))))&(~(p35(esk49_1(X3)))|~(p34(esk49_1(X3)))))&(p33(esk49_1(X3))|p34(esk49_1(X3))))&(~(p34(esk49_1(X3)))|~(p33(esk49_1(X3)))))&(p32(esk49_1(X3))|p33(esk49_1(X3))))&(~(p33(esk49_1(X3)))|~(p32(esk49_1(X3)))))&(p31(esk49_1(X3))|p32(esk49_1(X3))))&(~(p32(esk49_1(X3)))|~(p31(esk49_1(X3)))))&(p30(esk49_1(X3))|p31(esk49_1(X3))))&(~(p31(esk49_1(X3)))|~(p30(esk49_1(X3)))))&(p29(esk49_1(X3))|p30(esk49_1(X3))))&(~(p30(esk49_1(X3)))|~(p29(esk49_1(X3)))))&(p28(esk49_1(X3))|p29(esk49_1(X3))))&(~(p29(esk49_1(X3)))|~(p28(esk49_1(X3)))))&(p27(esk49_1(X3))|p28(esk49_1(X3))))&(~(p28(esk49_1(X3)))|~(p27(esk49_1(X3)))))&(p26(esk49_1(X3))|p27(esk49_1(X3))))&(~(p27(esk49_1(X3)))|~(p26(esk49_1(X3)))))&(p25(esk49_1(X3))|p26(esk49_1(X3))))&(~(p26(esk49_1(X3)))|~(p25(esk49_1(X3)))))&(p24(esk49_1(X3))|p25(esk49_1(X3))))&(~(p25(esk49_1(X3)))|~(p24(esk49_1(X3)))))&(p23(esk49_1(X3))|p24(esk49_1(X3))))&(~(p24(esk49_1(X3)))|~(p23(esk49_1(X3)))))&(p22(esk49_1(X3))|p23(esk49_1(X3))))&(~(p23(esk49_1(X3)))|~(p22(esk49_1(X3)))))&(p21(esk49_1(X3))|p22(esk49_1(X3))))&(~(p22(esk49_1(X3)))|~(p21(esk49_1(X3)))))&(p20(esk49_1(X3))|p21(esk49_1(X3))))&(~(p21(esk49_1(X3)))|~(p20(esk49_1(X3)))))&(p19(esk49_1(X3))|p20(esk49_1(X3))))&(~(p20(esk49_1(X3)))|~(p19(esk49_1(X3)))))&(p18(esk49_1(X3))|p19(esk49_1(X3))))&(~(p19(esk49_1(X3)))|~(p18(esk49_1(X3)))))&(p17(esk49_1(X3))|p18(esk49_1(X3))))&(~(p18(esk49_1(X3)))|~(p17(esk49_1(X3)))))&(p16(esk49_1(X3))|p17(esk49_1(X3))))&(~(p17(esk49_1(X3)))|~(p16(esk49_1(X3)))))&(p15(esk49_1(X3))|p16(esk49_1(X3))))&(~(p16(esk49_1(X3)))|~(p15(esk49_1(X3)))))&(p14(esk49_1(X3))|p15(esk49_1(X3))))&(~(p15(esk49_1(X3)))|~(p14(esk49_1(X3)))))&(p13(esk49_1(X3))|p14(esk49_1(X3))))&(~(p14(esk49_1(X3)))|~(p13(esk49_1(X3)))))&(p12(esk49_1(X3))|p13(esk49_1(X3))))&(~(p13(esk49_1(X3)))|~(p12(esk49_1(X3)))))&(p11(esk49_1(X3))|p12(esk49_1(X3))))&(~(p12(esk49_1(X3)))|~(p11(esk49_1(X3)))))&(p10(esk49_1(X3))|p11(esk49_1(X3))))&(~(p11(esk49_1(X3)))|~(p10(esk49_1(X3)))))&(p9(esk49_1(X3))|p10(esk49_1(X3))))&(~(p10(esk49_1(X3)))|~(p9(esk49_1(X3)))))&(p8(esk49_1(X3))|p9(esk49_1(X3))))&(~(p9(esk49_1(X3)))|~(p8(esk49_1(X3)))))&(p7(esk49_1(X3))|p8(esk49_1(X3))))&(~(p8(esk49_1(X3)))|~(p7(esk49_1(X3)))))&(p6(esk49_1(X3))|p7(esk49_1(X3))))&(~(p7(esk49_1(X3)))|~(p6(esk49_1(X3)))))&(p5(esk49_1(X3))|p6(esk49_1(X3))))&(~(p6(esk49_1(X3)))|~(p5(esk49_1(X3)))))&(p4(esk49_1(X3))|p5(esk49_1(X3))))&(~(p5(esk49_1(X3)))|~(p4(esk49_1(X3)))))&(p3(esk49_1(X3))|p4(esk49_1(X3))))&(~(p4(esk49_1(X3)))|~(p3(esk49_1(X3)))))&(p2(esk49_1(X3))|p3(esk49_1(X3))))&(~(p3(esk49_1(X3)))|~(p2(esk49_1(X3)))))&(p1(esk49_1(X3))|p2(esk49_1(X3))))&(~(p2(esk49_1(X3)))|~(p1(esk49_1(X3))))))),inference(skolemize,[status(esa)],[24])).
% fof(26, plain,![X3]:![X47]:![X48]:![X49]:![X50]:![X51]:![X52]:![X53]:![X54]:![X55]:![X56]:![X57]:![X58]:![X59]:![X60]:![X61]:![X62]:![X63]:![X64]:![X65]:![X66]:![X67]:![X68]:![X69]:![X70]:![X71]:![X72]:![X73]:![X74]:![X75]:![X76]:![X77]:![X78]:![X79]:![X80]:![X81]:![X82]:![X83]:![X84]:![X85]:![X86]:![X87]:![X88]:![X89]:(((((~(r1(X3,X89))|((~(p2(X89))|p1(X89))&(p2(X89)|~(p1(X89)))))&((~(r1(esk5_1(X3),X88))|((~(p3(X88))|p2(X88))&(p3(X88)|~(p2(X88)))))&(((~(r1(esk6_1(X3),X87))|((~(p4(X87))|p3(X87))&(p4(X87)|~(p3(X87)))))&(((~(r1(esk7_1(X3),X86))|((~(p5(X86))|p4(X86))&(p5(X86)|~(p4(X86)))))&(((~(r1(esk8_1(X3),X85))|((~(p6(X85))|p5(X85))&(p6(X85)|~(p5(X85)))))&(((~(r1(esk9_1(X3),X84))|((~(p7(X84))|p6(X84))&(p7(X84)|~(p6(X84)))))&(((~(r1(esk10_1(X3),X83))|((~(p8(X83))|p7(X83))&(p8(X83)|~(p7(X83)))))&(((~(r1(esk11_1(X3),X82))|((~(p9(X82))|p8(X82))&(p9(X82)|~(p8(X82)))))&(((~(r1(esk12_1(X3),X81))|((~(p10(X81))|p9(X81))&(p10(X81)|~(p9(X81)))))&(((~(r1(esk13_1(X3),X80))|((~(p11(X80))|p10(X80))&(p11(X80)|~(p10(X80)))))&(((~(r1(esk14_1(X3),X79))|((~(p12(X79))|p11(X79))&(p12(X79)|~(p11(X79)))))&(((~(r1(esk15_1(X3),X78))|((~(p13(X78))|p12(X78))&(p13(X78)|~(p12(X78)))))&(((~(r1(esk16_1(X3),X77))|((~(p14(X77))|p13(X77))&(p14(X77)|~(p13(X77)))))&(((~(r1(esk17_1(X3),X76))|((~(p15(X76))|p14(X76))&(p15(X76)|~(p14(X76)))))&(((~(r1(esk18_1(X3),X75))|((~(p16(X75))|p15(X75))&(p16(X75)|~(p15(X75)))))&(((~(r1(esk19_1(X3),X74))|((~(p17(X74))|p16(X74))&(p17(X74)|~(p16(X74)))))&(((~(r1(esk20_1(X3),X73))|((~(p18(X73))|p17(X73))&(p18(X73)|~(p17(X73)))))&(((~(r1(esk21_1(X3),X72))|((~(p19(X72))|p18(X72))&(p19(X72)|~(p18(X72)))))&(((~(r1(esk22_1(X3),X71))|((~(p20(X71))|p19(X71))&(p20(X71)|~(p19(X71)))))&(((~(r1(esk23_1(X3),X70))|((~(p21(X70))|p20(X70))&(p21(X70)|~(p20(X70)))))&(((~(r1(esk24_1(X3),X69))|((~(p22(X69))|p21(X69))&(p22(X69)|~(p21(X69)))))&(((~(r1(esk25_1(X3),X68))|((~(p23(X68))|p22(X68))&(p23(X68)|~(p22(X68)))))&(((~(r1(esk26_1(X3),X67))|((~(p24(X67))|p23(X67))&(p24(X67)|~(p23(X67)))))&(((~(r1(esk27_1(X3),X66))|((~(p25(X66))|p24(X66))&(p25(X66)|~(p24(X66)))))&(((~(r1(esk28_1(X3),X65))|((~(p26(X65))|p25(X65))&(p26(X65)|~(p25(X65)))))&(((~(r1(esk29_1(X3),X64))|((~(p27(X64))|p26(X64))&(p27(X64)|~(p26(X64)))))&(((~(r1(esk30_1(X3),X63))|((~(p28(X63))|p27(X63))&(p28(X63)|~(p27(X63)))))&(((~(r1(esk31_1(X3),X62))|((~(p29(X62))|p28(X62))&(p29(X62)|~(p28(X62)))))&(((~(r1(esk32_1(X3),X61))|((~(p30(X61))|p29(X61))&(p30(X61)|~(p29(X61)))))&(((~(r1(esk33_1(X3),X60))|((~(p31(X60))|p30(X60))&(p31(X60)|~(p30(X60)))))&(((~(r1(esk34_1(X3),X59))|((~(p32(X59))|p31(X59))&(p32(X59)|~(p31(X59)))))&(((~(r1(esk35_1(X3),X58))|((~(p33(X58))|p32(X58))&(p33(X58)|~(p32(X58)))))&(((~(r1(esk36_1(X3),X57))|((~(p34(X57))|p33(X57))&(p34(X57)|~(p33(X57)))))&(((~(r1(esk37_1(X3),X56))|((~(p35(X56))|p34(X56))&(p35(X56)|~(p34(X56)))))&(((~(r1(esk38_1(X3),X55))|((~(p36(X55))|p35(X55))&(p36(X55)|~(p35(X55)))))&(((~(r1(esk39_1(X3),X54))|((~(p37(X54))|p36(X54))&(p37(X54)|~(p36(X54)))))&(((~(r1(esk40_1(X3),X53))|((~(p38(X53))|p37(X53))&(p38(X53)|~(p37(X53)))))&(((~(r1(esk41_1(X3),X52))|((~(p39(X52))|p38(X52))&(p39(X52)|~(p38(X52)))))&(((~(r1(esk42_1(X3),X51))|((~(p40(X51))|p39(X51))&(p40(X51)|~(p39(X51)))))&(((~(r1(esk43_1(X3),X50))|((~(p41(X50))|p40(X50))&(p41(X50)|~(p40(X50)))))&(((~(r1(esk44_1(X3),X49))|((~(p42(X49))|p41(X49))&(p42(X49)|~(p41(X49)))))&(((~(r1(esk45_1(X3),X48))|((~(p43(X48))|p42(X48))&(p43(X48)|~(p42(X48)))))&(((~(r1(esk46_1(X3),X47))|((~(p44(X47))|p43(X47))&(p44(X47)|~(p43(X47)))))&(r1(esk45_1(X3),esk46_1(X3))&r1(esk46_1(X3),esk47_1(X3))))&r1(esk44_1(X3),esk45_1(X3))))&r1(esk43_1(X3),esk44_1(X3))))&r1(esk42_1(X3),esk43_1(X3))))&r1(esk41_1(X3),esk42_1(X3))))&r1(esk40_1(X3),esk41_1(X3))))&r1(esk39_1(X3),esk40_1(X3))))&r1(esk38_1(X3),esk39_1(X3))))&r1(esk37_1(X3),esk38_1(X3))))&r1(esk36_1(X3),esk37_1(X3))))&r1(esk35_1(X3),esk36_1(X3))))&r1(esk34_1(X3),esk35_1(X3))))&r1(esk33_1(X3),esk34_1(X3))))&r1(esk32_1(X3),esk33_1(X3))))&r1(esk31_1(X3),esk32_1(X3))))&r1(esk30_1(X3),esk31_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,esk48_1(X3))&~(p45(esk48_1(X3)))))&((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X3,esk49_1(X3))&(p43(esk49_1(X3))|p44(esk49_1(X3))))&(~(p44(esk49_1(X3)))|~(p43(esk49_1(X3)))))&(p42(esk49_1(X3))|p43(esk49_1(X3))))&(~(p43(esk49_1(X3)))|~(p42(esk49_1(X3)))))&(p41(esk49_1(X3))|p42(esk49_1(X3))))&(~(p42(esk49_1(X3)))|~(p41(esk49_1(X3)))))&(p40(esk49_1(X3))|p41(esk49_1(X3))))&(~(p41(esk49_1(X3)))|~(p40(esk49_1(X3)))))&(p39(esk49_1(X3))|p40(esk49_1(X3))))&(~(p40(esk49_1(X3)))|~(p39(esk49_1(X3)))))&(p38(esk49_1(X3))|p39(esk49_1(X3))))&(~(p39(esk49_1(X3)))|~(p38(esk49_1(X3)))))&(p37(esk49_1(X3))|p38(esk49_1(X3))))&(~(p38(esk49_1(X3)))|~(p37(esk49_1(X3)))))&(p36(esk49_1(X3))|p37(esk49_1(X3))))&(~(p37(esk49_1(X3)))|~(p36(esk49_1(X3)))))&(p35(esk49_1(X3))|p36(esk49_1(X3))))&(~(p36(esk49_1(X3)))|~(p35(esk49_1(X3)))))&(p34(esk49_1(X3))|p35(esk49_1(X3))))&(~(p35(esk49_1(X3)))|~(p34(esk49_1(X3)))))&(p33(esk49_1(X3))|p34(esk49_1(X3))))&(~(p34(esk49_1(X3)))|~(p33(esk49_1(X3)))))&(p32(esk49_1(X3))|p33(esk49_1(X3))))&(~(p33(esk49_1(X3)))|~(p32(esk49_1(X3)))))&(p31(esk49_1(X3))|p32(esk49_1(X3))))&(~(p32(esk49_1(X3)))|~(p31(esk49_1(X3)))))&(p30(esk49_1(X3))|p31(esk49_1(X3))))&(~(p31(esk49_1(X3)))|~(p30(esk49_1(X3)))))&(p29(esk49_1(X3))|p30(esk49_1(X3))))&(~(p30(esk49_1(X3)))|~(p29(esk49_1(X3)))))&(p28(esk49_1(X3))|p29(esk49_1(X3))))&(~(p29(esk49_1(X3)))|~(p28(esk49_1(X3)))))&(p27(esk49_1(X3))|p28(esk49_1(X3))))&(~(p28(esk49_1(X3)))|~(p27(esk49_1(X3)))))&(p26(esk49_1(X3))|p27(esk49_1(X3))))&(~(p27(esk49_1(X3)))|~(p26(esk49_1(X3)))))&(p25(esk49_1(X3))|p26(esk49_1(X3))))&(~(p26(esk49_1(X3)))|~(p25(esk49_1(X3)))))&(p24(esk49_1(X3))|p25(esk49_1(X3))))&(~(p25(esk49_1(X3)))|~(p24(esk49_1(X3)))))&(p23(esk49_1(X3))|p24(esk49_1(X3))))&(~(p24(esk49_1(X3)))|~(p23(esk49_1(X3)))))&(p22(esk49_1(X3))|p23(esk49_1(X3))))&(~(p23(esk49_1(X3)))|~(p22(esk49_1(X3)))))&(p21(esk49_1(X3))|p22(esk49_1(X3))))&(~(p22(esk49_1(X3)))|~(p21(esk49_1(X3)))))&(p20(esk49_1(X3))|p21(esk49_1(X3))))&(~(p21(esk49_1(X3)))|~(p20(esk49_1(X3)))))&(p19(esk49_1(X3))|p20(esk49_1(X3))))&(~(p20(esk49_1(X3)))|~(p19(esk49_1(X3)))))&(p18(esk49_1(X3))|p19(esk49_1(X3))))&(~(p19(esk49_1(X3)))|~(p18(esk49_1(X3)))))&(p17(esk49_1(X3))|p18(esk49_1(X3))))&(~(p18(esk49_1(X3)))|~(p17(esk49_1(X3)))))&(p16(esk49_1(X3))|p17(esk49_1(X3))))&(~(p17(esk49_1(X3)))|~(p16(esk49_1(X3)))))&(p15(esk49_1(X3))|p16(esk49_1(X3))))&(~(p16(esk49_1(X3)))|~(p15(esk49_1(X3)))))&(p14(esk49_1(X3))|p15(esk49_1(X3))))&(~(p15(esk49_1(X3)))|~(p14(esk49_1(X3)))))&(p13(esk49_1(X3))|p14(esk49_1(X3))))&(~(p14(esk49_1(X3)))|~(p13(esk49_1(X3)))))&(p12(esk49_1(X3))|p13(esk49_1(X3))))&(~(p13(esk49_1(X3)))|~(p12(esk49_1(X3)))))&(p11(esk49_1(X3))|p12(esk49_1(X3))))&(~(p12(esk49_1(X3)))|~(p11(esk49_1(X3)))))&(p10(esk49_1(X3))|p11(esk49_1(X3))))&(~(p11(esk49_1(X3)))|~(p10(esk49_1(X3)))))&(p9(esk49_1(X3))|p10(esk49_1(X3))))&(~(p10(esk49_1(X3)))|~(p9(esk49_1(X3)))))&(p8(esk49_1(X3))|p9(esk49_1(X3))))&(~(p9(esk49_1(X3)))|~(p8(esk49_1(X3)))))&(p7(esk49_1(X3))|p8(esk49_1(X3))))&(~(p8(esk49_1(X3)))|~(p7(esk49_1(X3)))))&(p6(esk49_1(X3))|p7(esk49_1(X3))))&(~(p7(esk49_1(X3)))|~(p6(esk49_1(X3)))))&(p5(esk49_1(X3))|p6(esk49_1(X3))))&(~(p6(esk49_1(X3)))|~(p5(esk49_1(X3)))))&(p4(esk49_1(X3))|p5(esk49_1(X3))))&(~(p5(esk49_1(X3)))|~(p4(esk49_1(X3)))))&(p3(esk49_1(X3))|p4(esk49_1(X3))))&(~(p4(esk49_1(X3)))|~(p3(esk49_1(X3)))))&(p2(esk49_1(X3))|p3(esk49_1(X3))))&(~(p3(esk49_1(X3)))|~(p2(esk49_1(X3)))))&(p1(esk49_1(X3))|p2(esk49_1(X3))))&(~(p2(esk49_1(X3)))|~(p1(esk49_1(X3))))))|~(epred1_1(X3))),inference(shift_quantors,[status(thm)],[25])).
% fof(27, plain,![X3]:![X47]:![X48]:![X49]:![X50]:![X51]:![X52]:![X53]:![X54]:![X55]:![X56]:![X57]:![X58]:![X59]:![X60]:![X61]:![X62]:![X63]:![X64]:![X65]:![X66]:![X67]:![X68]:![X69]:![X70]:![X71]:![X72]:![X73]:![X74]:![X75]:![X76]:![X77]:![X78]:![X79]:![X80]:![X81]:![X82]:![X83]:![X84]:![X85]:![X86]:![X87]:![X88]:![X89]:(((((((~(p2(X89))|p1(X89))|~(r1(X3,X89)))|~(epred1_1(X3)))&(((p2(X89)|~(p1(X89)))|~(r1(X3,X89)))|~(epred1_1(X3))))&(((((~(p3(X88))|p2(X88))|~(r1(esk5_1(X3),X88)))|~(epred1_1(X3)))&(((p3(X88)|~(p2(X88)))|~(r1(esk5_1(X3),X88)))|~(epred1_1(X3))))&((((((~(p4(X87))|p3(X87))|~(r1(esk6_1(X3),X87)))|~(epred1_1(X3)))&(((p4(X87)|~(p3(X87)))|~(r1(esk6_1(X3),X87)))|~(epred1_1(X3))))&((((((~(p5(X86))|p4(X86))|~(r1(esk7_1(X3),X86)))|~(epred1_1(X3)))&(((p5(X86)|~(p4(X86)))|~(r1(esk7_1(X3),X86)))|~(epred1_1(X3))))&((((((~(p6(X85))|p5(X85))|~(r1(esk8_1(X3),X85)))|~(epred1_1(X3)))&(((p6(X85)|~(p5(X85)))|~(r1(esk8_1(X3),X85)))|~(epred1_1(X3))))&((((((~(p7(X84))|p6(X84))|~(r1(esk9_1(X3),X84)))|~(epred1_1(X3)))&(((p7(X84)|~(p6(X84)))|~(r1(esk9_1(X3),X84)))|~(epred1_1(X3))))&((((((~(p8(X83))|p7(X83))|~(r1(esk10_1(X3),X83)))|~(epred1_1(X3)))&(((p8(X83)|~(p7(X83)))|~(r1(esk10_1(X3),X83)))|~(epred1_1(X3))))&((((((~(p9(X82))|p8(X82))|~(r1(esk11_1(X3),X82)))|~(epred1_1(X3)))&(((p9(X82)|~(p8(X82)))|~(r1(esk11_1(X3),X82)))|~(epred1_1(X3))))&((((((~(p10(X81))|p9(X81))|~(r1(esk12_1(X3),X81)))|~(epred1_1(X3)))&(((p10(X81)|~(p9(X81)))|~(r1(esk12_1(X3),X81)))|~(epred1_1(X3))))&((((((~(p11(X80))|p10(X80))|~(r1(esk13_1(X3),X80)))|~(epred1_1(X3)))&(((p11(X80)|~(p10(X80)))|~(r1(esk13_1(X3),X80)))|~(epred1_1(X3))))&((((((~(p12(X79))|p11(X79))|~(r1(esk14_1(X3),X79)))|~(epred1_1(X3)))&(((p12(X79)|~(p11(X79)))|~(r1(esk14_1(X3),X79)))|~(epred1_1(X3))))&((((((~(p13(X78))|p12(X78))|~(r1(esk15_1(X3),X78)))|~(epred1_1(X3)))&(((p13(X78)|~(p12(X78)))|~(r1(esk15_1(X3),X78)))|~(epred1_1(X3))))&((((((~(p14(X77))|p13(X77))|~(r1(esk16_1(X3),X77)))|~(epred1_1(X3)))&(((p14(X77)|~(p13(X77)))|~(r1(esk16_1(X3),X77)))|~(epred1_1(X3))))&((((((~(p15(X76))|p14(X76))|~(r1(esk17_1(X3),X76)))|~(epred1_1(X3)))&(((p15(X76)|~(p14(X76)))|~(r1(esk17_1(X3),X76)))|~(epred1_1(X3))))&((((((~(p16(X75))|p15(X75))|~(r1(esk18_1(X3),X75)))|~(epred1_1(X3)))&(((p16(X75)|~(p15(X75)))|~(r1(esk18_1(X3),X75)))|~(epred1_1(X3))))&((((((~(p17(X74))|p16(X74))|~(r1(esk19_1(X3),X74)))|~(epred1_1(X3)))&(((p17(X74)|~(p16(X74)))|~(r1(esk19_1(X3),X74)))|~(epred1_1(X3))))&((((((~(p18(X73))|p17(X73))|~(r1(esk20_1(X3),X73)))|~(epred1_1(X3)))&(((p18(X73)|~(p17(X73)))|~(r1(esk20_1(X3),X73)))|~(epred1_1(X3))))&((((((~(p19(X72))|p18(X72))|~(r1(esk21_1(X3),X72)))|~(epred1_1(X3)))&(((p19(X72)|~(p18(X72)))|~(r1(esk21_1(X3),X72)))|~(epred1_1(X3))))&((((((~(p20(X71))|p19(X71))|~(r1(esk22_1(X3),X71)))|~(epred1_1(X3)))&(((p20(X71)|~(p19(X71)))|~(r1(esk22_1(X3),X71)))|~(epred1_1(X3))))&((((((~(p21(X70))|p20(X70))|~(r1(esk23_1(X3),X70)))|~(epred1_1(X3)))&(((p21(X70)|~(p20(X70)))|~(r1(esk23_1(X3),X70)))|~(epred1_1(X3))))&((((((~(p22(X69))|p21(X69))|~(r1(esk24_1(X3),X69)))|~(epred1_1(X3)))&(((p22(X69)|~(p21(X69)))|~(r1(esk24_1(X3),X69)))|~(epred1_1(X3))))&((((((~(p23(X68))|p22(X68))|~(r1(esk25_1(X3),X68)))|~(epred1_1(X3)))&(((p23(X68)|~(p22(X68)))|~(r1(esk25_1(X3),X68)))|~(epred1_1(X3))))&((((((~(p24(X67))|p23(X67))|~(r1(esk26_1(X3),X67)))|~(epred1_1(X3)))&(((p24(X67)|~(p23(X67)))|~(r1(esk26_1(X3),X67)))|~(epred1_1(X3))))&((((((~(p25(X66))|p24(X66))|~(r1(esk27_1(X3),X66)))|~(epred1_1(X3)))&(((p25(X66)|~(p24(X66)))|~(r1(esk27_1(X3),X66)))|~(epred1_1(X3))))&((((((~(p26(X65))|p25(X65))|~(r1(esk28_1(X3),X65)))|~(epred1_1(X3)))&(((p26(X65)|~(p25(X65)))|~(r1(esk28_1(X3),X65)))|~(epred1_1(X3))))&((((((~(p27(X64))|p26(X64))|~(r1(esk29_1(X3),X64)))|~(epred1_1(X3)))&(((p27(X64)|~(p26(X64)))|~(r1(esk29_1(X3),X64)))|~(epred1_1(X3))))&((((((~(p28(X63))|p27(X63))|~(r1(esk30_1(X3),X63)))|~(epred1_1(X3)))&(((p28(X63)|~(p27(X63)))|~(r1(esk30_1(X3),X63)))|~(epred1_1(X3))))&((((((~(p29(X62))|p28(X62))|~(r1(esk31_1(X3),X62)))|~(epred1_1(X3)))&(((p29(X62)|~(p28(X62)))|~(r1(esk31_1(X3),X62)))|~(epred1_1(X3))))&((((((~(p30(X61))|p29(X61))|~(r1(esk32_1(X3),X61)))|~(epred1_1(X3)))&(((p30(X61)|~(p29(X61)))|~(r1(esk32_1(X3),X61)))|~(epred1_1(X3))))&((((((~(p31(X60))|p30(X60))|~(r1(esk33_1(X3),X60)))|~(epred1_1(X3)))&(((p31(X60)|~(p30(X60)))|~(r1(esk33_1(X3),X60)))|~(epred1_1(X3))))&((((((~(p32(X59))|p31(X59))|~(r1(esk34_1(X3),X59)))|~(epred1_1(X3)))&(((p32(X59)|~(p31(X59)))|~(r1(esk34_1(X3),X59)))|~(epred1_1(X3))))&((((((~(p33(X58))|p32(X58))|~(r1(esk35_1(X3),X58)))|~(epred1_1(X3)))&(((p33(X58)|~(p32(X58)))|~(r1(esk35_1(X3),X58)))|~(epred1_1(X3))))&((((((~(p34(X57))|p33(X57))|~(r1(esk36_1(X3),X57)))|~(epred1_1(X3)))&(((p34(X57)|~(p33(X57)))|~(r1(esk36_1(X3),X57)))|~(epred1_1(X3))))&((((((~(p35(X56))|p34(X56))|~(r1(esk37_1(X3),X56)))|~(epred1_1(X3)))&(((p35(X56)|~(p34(X56)))|~(r1(esk37_1(X3),X56)))|~(epred1_1(X3))))&((((((~(p36(X55))|p35(X55))|~(r1(esk38_1(X3),X55)))|~(epred1_1(X3)))&(((p36(X55)|~(p35(X55)))|~(r1(esk38_1(X3),X55)))|~(epred1_1(X3))))&((((((~(p37(X54))|p36(X54))|~(r1(esk39_1(X3),X54)))|~(epred1_1(X3)))&(((p37(X54)|~(p36(X54)))|~(r1(esk39_1(X3),X54)))|~(epred1_1(X3))))&((((((~(p38(X53))|p37(X53))|~(r1(esk40_1(X3),X53)))|~(epred1_1(X3)))&(((p38(X53)|~(p37(X53)))|~(r1(esk40_1(X3),X53)))|~(epred1_1(X3))))&((((((~(p39(X52))|p38(X52))|~(r1(esk41_1(X3),X52)))|~(epred1_1(X3)))&(((p39(X52)|~(p38(X52)))|~(r1(esk41_1(X3),X52)))|~(epred1_1(X3))))&((((((~(p40(X51))|p39(X51))|~(r1(esk42_1(X3),X51)))|~(epred1_1(X3)))&(((p40(X51)|~(p39(X51)))|~(r1(esk42_1(X3),X51)))|~(epred1_1(X3))))&((((((~(p41(X50))|p40(X50))|~(r1(esk43_1(X3),X50)))|~(epred1_1(X3)))&(((p41(X50)|~(p40(X50)))|~(r1(esk43_1(X3),X50)))|~(epred1_1(X3))))&((((((~(p42(X49))|p41(X49))|~(r1(esk44_1(X3),X49)))|~(epred1_1(X3)))&(((p42(X49)|~(p41(X49)))|~(r1(esk44_1(X3),X49)))|~(epred1_1(X3))))&((((((~(p43(X48))|p42(X48))|~(r1(esk45_1(X3),X48)))|~(epred1_1(X3)))&(((p43(X48)|~(p42(X48)))|~(r1(esk45_1(X3),X48)))|~(epred1_1(X3))))&((((((~(p44(X47))|p43(X47))|~(r1(esk46_1(X3),X47)))|~(epred1_1(X3)))&(((p44(X47)|~(p43(X47)))|~(r1(esk46_1(X3),X47)))|~(epred1_1(X3))))&((r1(esk45_1(X3),esk46_1(X3))|~(epred1_1(X3)))&(r1(esk46_1(X3),esk47_1(X3))|~(epred1_1(X3)))))&(r1(esk44_1(X3),esk45_1(X3))|~(epred1_1(X3)))))&(r1(esk43_1(X3),esk44_1(X3))|~(epred1_1(X3)))))&(r1(esk42_1(X3),esk43_1(X3))|~(epred1_1(X3)))))&(r1(esk41_1(X3),esk42_1(X3))|~(epred1_1(X3)))))&(r1(esk40_1(X3),esk41_1(X3))|~(epred1_1(X3)))))&(r1(esk39_1(X3),esk40_1(X3))|~(epred1_1(X3)))))&(r1(esk38_1(X3),esk39_1(X3))|~(epred1_1(X3)))))&(r1(esk37_1(X3),esk38_1(X3))|~(epred1_1(X3)))))&(r1(esk36_1(X3),esk37_1(X3))|~(epred1_1(X3)))))&(r1(esk35_1(X3),esk36_1(X3))|~(epred1_1(X3)))))&(r1(esk34_1(X3),esk35_1(X3))|~(epred1_1(X3)))))&(r1(esk33_1(X3),esk34_1(X3))|~(epred1_1(X3)))))&(r1(esk32_1(X3),esk33_1(X3))|~(epred1_1(X3)))))&(r1(esk31_1(X3),esk32_1(X3))|~(epred1_1(X3)))))&(r1(esk30_1(X3),esk31_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,esk48_1(X3))|~(epred1_1(X3)))&(~(p45(esk48_1(X3)))|~(epred1_1(X3)))))&(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X3,esk49_1(X3))|~(epred1_1(X3)))&((p43(esk49_1(X3))|p44(esk49_1(X3)))|~(epred1_1(X3))))&((~(p44(esk49_1(X3)))|~(p43(esk49_1(X3))))|~(epred1_1(X3))))&((p42(esk49_1(X3))|p43(esk49_1(X3)))|~(epred1_1(X3))))&((~(p43(esk49_1(X3)))|~(p42(esk49_1(X3))))|~(epred1_1(X3))))&((p41(esk49_1(X3))|p42(esk49_1(X3)))|~(epred1_1(X3))))&((~(p42(esk49_1(X3)))|~(p41(esk49_1(X3))))|~(epred1_1(X3))))&((p40(esk49_1(X3))|p41(esk49_1(X3)))|~(epred1_1(X3))))&((~(p41(esk49_1(X3)))|~(p40(esk49_1(X3))))|~(epred1_1(X3))))&((p39(esk49_1(X3))|p40(esk49_1(X3)))|~(epred1_1(X3))))&((~(p40(esk49_1(X3)))|~(p39(esk49_1(X3))))|~(epred1_1(X3))))&((p38(esk49_1(X3))|p39(esk49_1(X3)))|~(epred1_1(X3))))&((~(p39(esk49_1(X3)))|~(p38(esk49_1(X3))))|~(epred1_1(X3))))&((p37(esk49_1(X3))|p38(esk49_1(X3)))|~(epred1_1(X3))))&((~(p38(esk49_1(X3)))|~(p37(esk49_1(X3))))|~(epred1_1(X3))))&((p36(esk49_1(X3))|p37(esk49_1(X3)))|~(epred1_1(X3))))&((~(p37(esk49_1(X3)))|~(p36(esk49_1(X3))))|~(epred1_1(X3))))&((p35(esk49_1(X3))|p36(esk49_1(X3)))|~(epred1_1(X3))))&((~(p36(esk49_1(X3)))|~(p35(esk49_1(X3))))|~(epred1_1(X3))))&((p34(esk49_1(X3))|p35(esk49_1(X3)))|~(epred1_1(X3))))&((~(p35(esk49_1(X3)))|~(p34(esk49_1(X3))))|~(epred1_1(X3))))&((p33(esk49_1(X3))|p34(esk49_1(X3)))|~(epred1_1(X3))))&((~(p34(esk49_1(X3)))|~(p33(esk49_1(X3))))|~(epred1_1(X3))))&((p32(esk49_1(X3))|p33(esk49_1(X3)))|~(epred1_1(X3))))&((~(p33(esk49_1(X3)))|~(p32(esk49_1(X3))))|~(epred1_1(X3))))&((p31(esk49_1(X3))|p32(esk49_1(X3)))|~(epred1_1(X3))))&((~(p32(esk49_1(X3)))|~(p31(esk49_1(X3))))|~(epred1_1(X3))))&((p30(esk49_1(X3))|p31(esk49_1(X3)))|~(epred1_1(X3))))&((~(p31(esk49_1(X3)))|~(p30(esk49_1(X3))))|~(epred1_1(X3))))&((p29(esk49_1(X3))|p30(esk49_1(X3)))|~(epred1_1(X3))))&((~(p30(esk49_1(X3)))|~(p29(esk49_1(X3))))|~(epred1_1(X3))))&((p28(esk49_1(X3))|p29(esk49_1(X3)))|~(epred1_1(X3))))&((~(p29(esk49_1(X3)))|~(p28(esk49_1(X3))))|~(epred1_1(X3))))&((p27(esk49_1(X3))|p28(esk49_1(X3)))|~(epred1_1(X3))))&((~(p28(esk49_1(X3)))|~(p27(esk49_1(X3))))|~(epred1_1(X3))))&((p26(esk49_1(X3))|p27(esk49_1(X3)))|~(epred1_1(X3))))&((~(p27(esk49_1(X3)))|~(p26(esk49_1(X3))))|~(epred1_1(X3))))&((p25(esk49_1(X3))|p26(esk49_1(X3)))|~(epred1_1(X3))))&((~(p26(esk49_1(X3)))|~(p25(esk49_1(X3))))|~(epred1_1(X3))))&((p24(esk49_1(X3))|p25(esk49_1(X3)))|~(epred1_1(X3))))&((~(p25(esk49_1(X3)))|~(p24(esk49_1(X3))))|~(epred1_1(X3))))&((p23(esk49_1(X3))|p24(esk49_1(X3)))|~(epred1_1(X3))))&((~(p24(esk49_1(X3)))|~(p23(esk49_1(X3))))|~(epred1_1(X3))))&((p22(esk49_1(X3))|p23(esk49_1(X3)))|~(epred1_1(X3))))&((~(p23(esk49_1(X3)))|~(p22(esk49_1(X3))))|~(epred1_1(X3))))&((p21(esk49_1(X3))|p22(esk49_1(X3)))|~(epred1_1(X3))))&((~(p22(esk49_1(X3)))|~(p21(esk49_1(X3))))|~(epred1_1(X3))))&((p20(esk49_1(X3))|p21(esk49_1(X3)))|~(epred1_1(X3))))&((~(p21(esk49_1(X3)))|~(p20(esk49_1(X3))))|~(epred1_1(X3))))&((p19(esk49_1(X3))|p20(esk49_1(X3)))|~(epred1_1(X3))))&((~(p20(esk49_1(X3)))|~(p19(esk49_1(X3))))|~(epred1_1(X3))))&((p18(esk49_1(X3))|p19(esk49_1(X3)))|~(epred1_1(X3))))&((~(p19(esk49_1(X3)))|~(p18(esk49_1(X3))))|~(epred1_1(X3))))&((p17(esk49_1(X3))|p18(esk49_1(X3)))|~(epred1_1(X3))))&((~(p18(esk49_1(X3)))|~(p17(esk49_1(X3))))|~(epred1_1(X3))))&((p16(esk49_1(X3))|p17(esk49_1(X3)))|~(epred1_1(X3))))&((~(p17(esk49_1(X3)))|~(p16(esk49_1(X3))))|~(epred1_1(X3))))&((p15(esk49_1(X3))|p16(esk49_1(X3)))|~(epred1_1(X3))))&((~(p16(esk49_1(X3)))|~(p15(esk49_1(X3))))|~(epred1_1(X3))))&((p14(esk49_1(X3))|p15(esk49_1(X3)))|~(epred1_1(X3))))&((~(p15(esk49_1(X3)))|~(p14(esk49_1(X3))))|~(epred1_1(X3))))&((p13(esk49_1(X3))|p14(esk49_1(X3)))|~(epred1_1(X3))))&((~(p14(esk49_1(X3)))|~(p13(esk49_1(X3))))|~(epred1_1(X3))))&((p12(esk49_1(X3))|p13(esk49_1(X3)))|~(epred1_1(X3))))&((~(p13(esk49_1(X3)))|~(p12(esk49_1(X3))))|~(epred1_1(X3))))&((p11(esk49_1(X3))|p12(esk49_1(X3)))|~(epred1_1(X3))))&((~(p12(esk49_1(X3)))|~(p11(esk49_1(X3))))|~(epred1_1(X3))))&((p10(esk49_1(X3))|p11(esk49_1(X3)))|~(epred1_1(X3))))&((~(p11(esk49_1(X3)))|~(p10(esk49_1(X3))))|~(epred1_1(X3))))&((p9(esk49_1(X3))|p10(esk49_1(X3)))|~(epred1_1(X3))))&((~(p10(esk49_1(X3)))|~(p9(esk49_1(X3))))|~(epred1_1(X3))))&((p8(esk49_1(X3))|p9(esk49_1(X3)))|~(epred1_1(X3))))&((~(p9(esk49_1(X3)))|~(p8(esk49_1(X3))))|~(epred1_1(X3))))&((p7(esk49_1(X3))|p8(esk49_1(X3)))|~(epred1_1(X3))))&((~(p8(esk49_1(X3)))|~(p7(esk49_1(X3))))|~(epred1_1(X3))))&((p6(esk49_1(X3))|p7(esk49_1(X3)))|~(epred1_1(X3))))&((~(p7(esk49_1(X3)))|~(p6(esk49_1(X3))))|~(epred1_1(X3))))&((p5(esk49_1(X3))|p6(esk49_1(X3)))|~(epred1_1(X3))))&((~(p6(esk49_1(X3)))|~(p5(esk49_1(X3))))|~(epred1_1(X3))))&((p4(esk49_1(X3))|p5(esk49_1(X3)))|~(epred1_1(X3))))&((~(p5(esk49_1(X3)))|~(p4(esk49_1(X3))))|~(epred1_1(X3))))&((p3(esk49_1(X3))|p4(esk49_1(X3)))|~(epred1_1(X3))))&((~(p4(esk49_1(X3)))|~(p3(esk49_1(X3))))|~(epred1_1(X3))))&((p2(esk49_1(X3))|p3(esk49_1(X3)))|~(epred1_1(X3))))&((~(p3(esk49_1(X3)))|~(p2(esk49_1(X3))))|~(epred1_1(X3))))&((p1(esk49_1(X3))|p2(esk49_1(X3)))|~(epred1_1(X3))))&((~(p2(esk49_1(X3)))|~(p1(esk49_1(X3))))|~(epred1_1(X3))))),inference(distribute,[status(thm)],[26])).
% cnf(28,plain,(~epred1_1(X1)|~p1(esk49_1(X1))|~p2(esk49_1(X1))),inference(split_conjunct,[status(thm)],[27])).
% cnf(29,plain,(p2(esk49_1(X1))|p1(esk49_1(X1))|~epred1_1(X1)),inference(split_conjunct,[status(thm)],[27])).
% cnf(114,plain,(r1(X1,esk49_1(X1))|~epred1_1(X1)),inference(split_conjunct,[status(thm)],[27])).
% cnf(244,plain,(p2(X2)|~epred1_1(X1)|~r1(X1,X2)|~p1(X2)),inference(split_conjunct,[status(thm)],[27])).
% cnf(245,plain,(p1(X2)|~epred1_1(X1)|~r1(X1,X2)|~p2(X2)),inference(split_conjunct,[status(thm)],[27])).
% cnf(246,negated_conjecture,(epred1_1(esk4_0)),inference(spm,[status(thm)],[22,9,theory(equality)])).
% cnf(254,plain,(p1(esk49_1(X1))|~epred1_1(X1)|~p2(esk49_1(X1))),inference(spm,[status(thm)],[245,114,theory(equality)])).
% cnf(263,plain,(p2(esk49_1(X1))|~epred1_1(X1)|~p1(esk49_1(X1))),inference(spm,[status(thm)],[244,114,theory(equality)])).
% cnf(1089,plain,(p1(esk49_1(X1))|~epred1_1(X1)),inference(csr,[status(thm)],[254,29])).
% cnf(1091,plain,(~epred1_1(X1)|~p2(esk49_1(X1))),inference(spm,[status(thm)],[28,1089,theory(equality)])).
% cnf(1218,plain,(p2(esk49_1(X1))|~epred1_1(X1)),inference(csr,[status(thm)],[263,1089])).
% cnf(1219,plain,(~epred1_1(X1)),inference(csr,[status(thm)],[1218,1091])).
% cnf(1220,negated_conjecture,($false),inference(sr,[status(thm)],[246,1219,theory(equality)])).
% cnf(1221,negated_conjecture,($false),1220,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 522
% # ...of these trivial : 0
% # ...subsumed : 6
% # ...remaining for further processing: 516
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 46
% # Backward-rewritten : 0
% # Generated clauses : 951
% # ...of the previous two non-trivial : 878
% # Contextual simplify-reflections : 4
% # Paramodulations : 947
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 240
% # Positive orientable unit clauses: 7
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 1
% # Non-unit-clauses : 232
% # Current number of unprocessed clauses: 806
% # ...number of literals in the above : 3092
% # Clause-clause subsumption calls (NU) : 17281
% # Rec. Clause-clause subsumption calls : 14010
% # Unit Clause-clause subsumption calls : 401
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 6
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 255 leaves, 1.20+/-0.455 terms/leaf
% # Paramod-from index: 94 leaves, 1.01+/-0.103 terms/leaf
% # Paramod-into index: 201 leaves, 1.24+/-0.438 terms/leaf
% # -------------------------------------------------
% # User time : 0.120 s
% # System time : 0.007 s
% # Total time : 0.127 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.23 CPU 0.33 WC
% FINAL PrfWatch: 0.23 CPU 0.33 WC
% SZS output end Solution for /tmp/SystemOnTPTP2632/LCL686+1.015.tptp
%
%------------------------------------------------------------------------------