%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LCL674+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 : art03.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:25:04 EST 2010
% Result : Theorem 1.88s
% Output : Solution 1.88s
% 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/SystemOnTPTP6722/LCL674+1.010.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP6722/LCL674+1.010.tptp
% SZS output start Solution for /tmp/SystemOnTPTP6722/LCL674+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 6818
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.023 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(2, axiom,![X1]:![X2]:![X3]:((r1(X1,X2)&r1(X2,X3))=>r1(X1,X3)),file('/tmp/SRASS.s.p', transitivity)).
% fof(3, conjecture,~(?[X1]:~((~(![X2]:(~(r1(X1,X2))|p5(X2)))|~(((![X2]:(~(r1(X1,X2))|(((((((((((((((((((((((((((((((((~(![X1]:(~(r1(X2,X1))|~(((~(p11(X1))&~(p111(X1)))&p110(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p11(X1)&~(p111(X1)))&p110(X1))))))|~((~(p110(X2))&p109(X2))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p10(X1))&~(p110(X1)))&p109(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p10(X1)&~(p110(X1)))&p109(X1))))))|~((~(p109(X2))&p108(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p9(X1))&~(p109(X1)))&p108(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p9(X1)&~(p109(X1)))&p108(X1))))))|~((~(p108(X2))&p107(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p8(X1))&~(p108(X1)))&p107(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p8(X1)&~(p108(X1)))&p107(X1))))))|~((~(p107(X2))&p106(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p7(X1))&~(p107(X1)))&p106(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p7(X1)&~(p107(X1)))&p106(X1))))))|~((~(p106(X2))&p105(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p6(X1))&~(p106(X1)))&p105(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p6(X1)&~(p106(X1)))&p105(X1))))))|~((~(p105(X2))&p104(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p5(X1))&~(p105(X1)))&p104(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p5(X1)&~(p105(X1)))&p104(X1))))))|~((~(p104(X2))&p103(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p4(X1))&~(p104(X1)))&p103(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p4(X1)&~(p104(X1)))&p103(X1))))))|~((~(p103(X2))&p102(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p3(X1))&~(p103(X1)))&p102(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p3(X1)&~(p103(X1)))&p102(X1))))))|~((~(p102(X2))&p101(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p2(X1))&~(p102(X1)))&p101(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p2(X1)&~(p102(X1)))&p101(X1))))))|~((~(p101(X2))&p100(X2)))))&(((![X1]:((~(r1(X2,X1))|~(p11(X1)))|~(p110(X1)))|p11(X2))&(![X1]:((~(r1(X2,X1))|p11(X1))|~(p110(X1)))|~(p11(X2))))|~(p110(X2))))&(((![X1]:((~(r1(X2,X1))|~(p10(X1)))|~(p109(X1)))|p10(X2))&(![X1]:((~(r1(X2,X1))|p10(X1))|~(p109(X1)))|~(p10(X2))))|~(p109(X2))))&(((![X1]:((~(r1(X2,X1))|~(p9(X1)))|~(p108(X1)))|p9(X2))&(![X1]:((~(r1(X2,X1))|p9(X1))|~(p108(X1)))|~(p9(X2))))|~(p108(X2))))&(((![X1]:((~(r1(X2,X1))|~(p8(X1)))|~(p107(X1)))|p8(X2))&(![X1]:((~(r1(X2,X1))|p8(X1))|~(p107(X1)))|~(p8(X2))))|~(p107(X2))))&(((![X1]:((~(r1(X2,X1))|~(p7(X1)))|~(p106(X1)))|p7(X2))&(![X1]:((~(r1(X2,X1))|p7(X1))|~(p106(X1)))|~(p7(X2))))|~(p106(X2))))&(((![X1]:((~(r1(X2,X1))|~(p6(X1)))|~(p105(X1)))|p6(X2))&(![X1]:((~(r1(X2,X1))|p6(X1))|~(p105(X1)))|~(p6(X2))))|~(p105(X2))))&(((![X1]:((~(r1(X2,X1))|~(p5(X1)))|~(p104(X1)))|p5(X2))&(![X1]:((~(r1(X2,X1))|p5(X1))|~(p104(X1)))|~(p5(X2))))|~(p104(X2))))&(((![X1]:((~(r1(X2,X1))|~(p4(X1)))|~(p103(X1)))|p4(X2))&(![X1]:((~(r1(X2,X1))|p4(X1))|~(p103(X1)))|~(p4(X2))))|~(p103(X2))))&(((![X1]:((~(r1(X2,X1))|~(p3(X1)))|~(p102(X1)))|p3(X2))&(![X1]:((~(r1(X2,X1))|p3(X1))|~(p102(X1)))|~(p3(X2))))|~(p102(X2))))&(((![X1]:((~(r1(X2,X1))|~(p2(X1)))|~(p101(X1)))|p2(X2))&(![X1]:((~(r1(X2,X1))|p2(X1))|~(p101(X1)))|~(p2(X2))))|~(p101(X2))))&(((![X1]:((~(r1(X2,X1))|~(p1(X1)))|~(p100(X1)))|p1(X2))&(![X1]:((~(r1(X2,X1))|p1(X1))|~(p100(X1)))|~(p1(X2))))|~(p100(X2))))&(p110(X2)|~(p111(X2))))&(p109(X2)|~(p110(X2))))&(p108(X2)|~(p109(X2))))&(p107(X2)|~(p108(X2))))&(p106(X2)|~(p107(X2))))&(p105(X2)|~(p106(X2))))&(p104(X2)|~(p105(X2))))&(p103(X2)|~(p104(X2))))&(p102(X2)|~(p103(X2))))&(p101(X2)|~(p102(X2))))&(p100(X2)|~(p101(X2)))))&~(p101(X1)))&p100(X1)))))),file('/tmp/SRASS.s.p', main)).
% fof(4, negated_conjecture,~(~(?[X1]:~((~(![X2]:(~(r1(X1,X2))|p5(X2)))|~(((![X2]:(~(r1(X1,X2))|(((((((((((((((((((((((((((((((((~(![X1]:(~(r1(X2,X1))|~(((~(p11(X1))&~(p111(X1)))&p110(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p11(X1)&~(p111(X1)))&p110(X1))))))|~((~(p110(X2))&p109(X2))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p10(X1))&~(p110(X1)))&p109(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p10(X1)&~(p110(X1)))&p109(X1))))))|~((~(p109(X2))&p108(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p9(X1))&~(p109(X1)))&p108(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p9(X1)&~(p109(X1)))&p108(X1))))))|~((~(p108(X2))&p107(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p8(X1))&~(p108(X1)))&p107(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p8(X1)&~(p108(X1)))&p107(X1))))))|~((~(p107(X2))&p106(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p7(X1))&~(p107(X1)))&p106(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p7(X1)&~(p107(X1)))&p106(X1))))))|~((~(p106(X2))&p105(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p6(X1))&~(p106(X1)))&p105(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p6(X1)&~(p106(X1)))&p105(X1))))))|~((~(p105(X2))&p104(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p5(X1))&~(p105(X1)))&p104(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p5(X1)&~(p105(X1)))&p104(X1))))))|~((~(p104(X2))&p103(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p4(X1))&~(p104(X1)))&p103(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p4(X1)&~(p104(X1)))&p103(X1))))))|~((~(p103(X2))&p102(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p3(X1))&~(p103(X1)))&p102(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p3(X1)&~(p103(X1)))&p102(X1))))))|~((~(p102(X2))&p101(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p2(X1))&~(p102(X1)))&p101(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p2(X1)&~(p102(X1)))&p101(X1))))))|~((~(p101(X2))&p100(X2)))))&(((![X1]:((~(r1(X2,X1))|~(p11(X1)))|~(p110(X1)))|p11(X2))&(![X1]:((~(r1(X2,X1))|p11(X1))|~(p110(X1)))|~(p11(X2))))|~(p110(X2))))&(((![X1]:((~(r1(X2,X1))|~(p10(X1)))|~(p109(X1)))|p10(X2))&(![X1]:((~(r1(X2,X1))|p10(X1))|~(p109(X1)))|~(p10(X2))))|~(p109(X2))))&(((![X1]:((~(r1(X2,X1))|~(p9(X1)))|~(p108(X1)))|p9(X2))&(![X1]:((~(r1(X2,X1))|p9(X1))|~(p108(X1)))|~(p9(X2))))|~(p108(X2))))&(((![X1]:((~(r1(X2,X1))|~(p8(X1)))|~(p107(X1)))|p8(X2))&(![X1]:((~(r1(X2,X1))|p8(X1))|~(p107(X1)))|~(p8(X2))))|~(p107(X2))))&(((![X1]:((~(r1(X2,X1))|~(p7(X1)))|~(p106(X1)))|p7(X2))&(![X1]:((~(r1(X2,X1))|p7(X1))|~(p106(X1)))|~(p7(X2))))|~(p106(X2))))&(((![X1]:((~(r1(X2,X1))|~(p6(X1)))|~(p105(X1)))|p6(X2))&(![X1]:((~(r1(X2,X1))|p6(X1))|~(p105(X1)))|~(p6(X2))))|~(p105(X2))))&(((![X1]:((~(r1(X2,X1))|~(p5(X1)))|~(p104(X1)))|p5(X2))&(![X1]:((~(r1(X2,X1))|p5(X1))|~(p104(X1)))|~(p5(X2))))|~(p104(X2))))&(((![X1]:((~(r1(X2,X1))|~(p4(X1)))|~(p103(X1)))|p4(X2))&(![X1]:((~(r1(X2,X1))|p4(X1))|~(p103(X1)))|~(p4(X2))))|~(p103(X2))))&(((![X1]:((~(r1(X2,X1))|~(p3(X1)))|~(p102(X1)))|p3(X2))&(![X1]:((~(r1(X2,X1))|p3(X1))|~(p102(X1)))|~(p3(X2))))|~(p102(X2))))&(((![X1]:((~(r1(X2,X1))|~(p2(X1)))|~(p101(X1)))|p2(X2))&(![X1]:((~(r1(X2,X1))|p2(X1))|~(p101(X1)))|~(p2(X2))))|~(p101(X2))))&(((![X1]:((~(r1(X2,X1))|~(p1(X1)))|~(p100(X1)))|p1(X2))&(![X1]:((~(r1(X2,X1))|p1(X1))|~(p100(X1)))|~(p1(X2))))|~(p100(X2))))&(p110(X2)|~(p111(X2))))&(p109(X2)|~(p110(X2))))&(p108(X2)|~(p109(X2))))&(p107(X2)|~(p108(X2))))&(p106(X2)|~(p107(X2))))&(p105(X2)|~(p106(X2))))&(p104(X2)|~(p105(X2))))&(p103(X2)|~(p104(X2))))&(p102(X2)|~(p103(X2))))&(p101(X2)|~(p102(X2))))&(p100(X2)|~(p101(X2)))))&~(p101(X1)))&p100(X1))))))),inference(assume_negation,[status(cth)],[3])).
% fof(5, negated_conjecture,~(~(?[X1]:~((~(![X2]:(~(r1(X1,X2))|p5(X2)))|~(((![X2]:(~(r1(X1,X2))|(((((((((((((((((((((((((((((((((~(![X1]:(~(r1(X2,X1))|~(((~(p11(X1))&~(p111(X1)))&p110(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p11(X1)&~(p111(X1)))&p110(X1))))))|~((~(p110(X2))&p109(X2))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p10(X1))&~(p110(X1)))&p109(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p10(X1)&~(p110(X1)))&p109(X1))))))|~((~(p109(X2))&p108(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p9(X1))&~(p109(X1)))&p108(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p9(X1)&~(p109(X1)))&p108(X1))))))|~((~(p108(X2))&p107(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p8(X1))&~(p108(X1)))&p107(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p8(X1)&~(p108(X1)))&p107(X1))))))|~((~(p107(X2))&p106(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p7(X1))&~(p107(X1)))&p106(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p7(X1)&~(p107(X1)))&p106(X1))))))|~((~(p106(X2))&p105(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p6(X1))&~(p106(X1)))&p105(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p6(X1)&~(p106(X1)))&p105(X1))))))|~((~(p105(X2))&p104(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p5(X1))&~(p105(X1)))&p104(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p5(X1)&~(p105(X1)))&p104(X1))))))|~((~(p104(X2))&p103(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p4(X1))&~(p104(X1)))&p103(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p4(X1)&~(p104(X1)))&p103(X1))))))|~((~(p103(X2))&p102(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p3(X1))&~(p103(X1)))&p102(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p3(X1)&~(p103(X1)))&p102(X1))))))|~((~(p102(X2))&p101(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p2(X1))&~(p102(X1)))&p101(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p2(X1)&~(p102(X1)))&p101(X1))))))|~((~(p101(X2))&p100(X2)))))&(((![X1]:((~(r1(X2,X1))|~(p11(X1)))|~(p110(X1)))|p11(X2))&(![X1]:((~(r1(X2,X1))|p11(X1))|~(p110(X1)))|~(p11(X2))))|~(p110(X2))))&(((![X1]:((~(r1(X2,X1))|~(p10(X1)))|~(p109(X1)))|p10(X2))&(![X1]:((~(r1(X2,X1))|p10(X1))|~(p109(X1)))|~(p10(X2))))|~(p109(X2))))&(((![X1]:((~(r1(X2,X1))|~(p9(X1)))|~(p108(X1)))|p9(X2))&(![X1]:((~(r1(X2,X1))|p9(X1))|~(p108(X1)))|~(p9(X2))))|~(p108(X2))))&(((![X1]:((~(r1(X2,X1))|~(p8(X1)))|~(p107(X1)))|p8(X2))&(![X1]:((~(r1(X2,X1))|p8(X1))|~(p107(X1)))|~(p8(X2))))|~(p107(X2))))&(((![X1]:((~(r1(X2,X1))|~(p7(X1)))|~(p106(X1)))|p7(X2))&(![X1]:((~(r1(X2,X1))|p7(X1))|~(p106(X1)))|~(p7(X2))))|~(p106(X2))))&(((![X1]:((~(r1(X2,X1))|~(p6(X1)))|~(p105(X1)))|p6(X2))&(![X1]:((~(r1(X2,X1))|p6(X1))|~(p105(X1)))|~(p6(X2))))|~(p105(X2))))&(((![X1]:((~(r1(X2,X1))|~(p5(X1)))|~(p104(X1)))|p5(X2))&(![X1]:((~(r1(X2,X1))|p5(X1))|~(p104(X1)))|~(p5(X2))))|~(p104(X2))))&(((![X1]:((~(r1(X2,X1))|~(p4(X1)))|~(p103(X1)))|p4(X2))&(![X1]:((~(r1(X2,X1))|p4(X1))|~(p103(X1)))|~(p4(X2))))|~(p103(X2))))&(((![X1]:((~(r1(X2,X1))|~(p3(X1)))|~(p102(X1)))|p3(X2))&(![X1]:((~(r1(X2,X1))|p3(X1))|~(p102(X1)))|~(p3(X2))))|~(p102(X2))))&(((![X1]:((~(r1(X2,X1))|~(p2(X1)))|~(p101(X1)))|p2(X2))&(![X1]:((~(r1(X2,X1))|p2(X1))|~(p101(X1)))|~(p2(X2))))|~(p101(X2))))&(((![X1]:((~(r1(X2,X1))|~(p1(X1)))|~(p100(X1)))|p1(X2))&(![X1]:((~(r1(X2,X1))|p1(X1))|~(p100(X1)))|~(p1(X2))))|~(p100(X2))))&(p110(X2)|~(p111(X2))))&(p109(X2)|~(p110(X2))))&(p108(X2)|~(p109(X2))))&(p107(X2)|~(p108(X2))))&(p106(X2)|~(p107(X2))))&(p105(X2)|~(p106(X2))))&(p104(X2)|~(p105(X2))))&(p103(X2)|~(p104(X2))))&(p102(X2)|~(p103(X2))))&(p101(X2)|~(p102(X2))))&(p100(X2)|~(p101(X2)))))&~(p101(X1)))&p100(X1))))))),inference(fof_simplification,[status(thm)],[4,theory(equality)])).
% fof(6, plain,![X2]:(epred1_1(X2)=>(((((((((((((((((((((((((((((((((~(![X1]:(~(r1(X2,X1))|~(((~(p11(X1))&~(p111(X1)))&p110(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p11(X1)&~(p111(X1)))&p110(X1))))))|~((~(p110(X2))&p109(X2))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p10(X1))&~(p110(X1)))&p109(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p10(X1)&~(p110(X1)))&p109(X1))))))|~((~(p109(X2))&p108(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p9(X1))&~(p109(X1)))&p108(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p9(X1)&~(p109(X1)))&p108(X1))))))|~((~(p108(X2))&p107(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p8(X1))&~(p108(X1)))&p107(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p8(X1)&~(p108(X1)))&p107(X1))))))|~((~(p107(X2))&p106(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p7(X1))&~(p107(X1)))&p106(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p7(X1)&~(p107(X1)))&p106(X1))))))|~((~(p106(X2))&p105(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p6(X1))&~(p106(X1)))&p105(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p6(X1)&~(p106(X1)))&p105(X1))))))|~((~(p105(X2))&p104(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p5(X1))&~(p105(X1)))&p104(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p5(X1)&~(p105(X1)))&p104(X1))))))|~((~(p104(X2))&p103(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p4(X1))&~(p104(X1)))&p103(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p4(X1)&~(p104(X1)))&p103(X1))))))|~((~(p103(X2))&p102(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p3(X1))&~(p103(X1)))&p102(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p3(X1)&~(p103(X1)))&p102(X1))))))|~((~(p102(X2))&p101(X2)))))&((~(![X1]:(~(r1(X2,X1))|~(((~(p2(X1))&~(p102(X1)))&p101(X1)))))&~(![X1]:(~(r1(X2,X1))|~(((p2(X1)&~(p102(X1)))&p101(X1))))))|~((~(p101(X2))&p100(X2)))))&(((![X1]:((~(r1(X2,X1))|~(p11(X1)))|~(p110(X1)))|p11(X2))&(![X1]:((~(r1(X2,X1))|p11(X1))|~(p110(X1)))|~(p11(X2))))|~(p110(X2))))&(((![X1]:((~(r1(X2,X1))|~(p10(X1)))|~(p109(X1)))|p10(X2))&(![X1]:((~(r1(X2,X1))|p10(X1))|~(p109(X1)))|~(p10(X2))))|~(p109(X2))))&(((![X1]:((~(r1(X2,X1))|~(p9(X1)))|~(p108(X1)))|p9(X2))&(![X1]:((~(r1(X2,X1))|p9(X1))|~(p108(X1)))|~(p9(X2))))|~(p108(X2))))&(((![X1]:((~(r1(X2,X1))|~(p8(X1)))|~(p107(X1)))|p8(X2))&(![X1]:((~(r1(X2,X1))|p8(X1))|~(p107(X1)))|~(p8(X2))))|~(p107(X2))))&(((![X1]:((~(r1(X2,X1))|~(p7(X1)))|~(p106(X1)))|p7(X2))&(![X1]:((~(r1(X2,X1))|p7(X1))|~(p106(X1)))|~(p7(X2))))|~(p106(X2))))&(((![X1]:((~(r1(X2,X1))|~(p6(X1)))|~(p105(X1)))|p6(X2))&(![X1]:((~(r1(X2,X1))|p6(X1))|~(p105(X1)))|~(p6(X2))))|~(p105(X2))))&(((![X1]:((~(r1(X2,X1))|~(p5(X1)))|~(p104(X1)))|p5(X2))&(![X1]:((~(r1(X2,X1))|p5(X1))|~(p104(X1)))|~(p5(X2))))|~(p104(X2))))&(((![X1]:((~(r1(X2,X1))|~(p4(X1)))|~(p103(X1)))|p4(X2))&(![X1]:((~(r1(X2,X1))|p4(X1))|~(p103(X1)))|~(p4(X2))))|~(p103(X2))))&(((![X1]:((~(r1(X2,X1))|~(p3(X1)))|~(p102(X1)))|p3(X2))&(![X1]:((~(r1(X2,X1))|p3(X1))|~(p102(X1)))|~(p3(X2))))|~(p102(X2))))&(((![X1]:((~(r1(X2,X1))|~(p2(X1)))|~(p101(X1)))|p2(X2))&(![X1]:((~(r1(X2,X1))|p2(X1))|~(p101(X1)))|~(p2(X2))))|~(p101(X2))))&(((![X1]:((~(r1(X2,X1))|~(p1(X1)))|~(p100(X1)))|p1(X2))&(![X1]:((~(r1(X2,X1))|p1(X1))|~(p100(X1)))|~(p1(X2))))|~(p100(X2))))&(p110(X2)|~(p111(X2))))&(p109(X2)|~(p110(X2))))&(p108(X2)|~(p109(X2))))&(p107(X2)|~(p108(X2))))&(p106(X2)|~(p107(X2))))&(p105(X2)|~(p106(X2))))&(p104(X2)|~(p105(X2))))&(p103(X2)|~(p104(X2))))&(p102(X2)|~(p103(X2))))&(p101(X2)|~(p102(X2))))&(p100(X2)|~(p101(X2))))),introduced(definition)).
% fof(7, negated_conjecture,~(~(?[X1]:~((~(![X2]:(~(r1(X1,X2))|p5(X2)))|~(((![X2]:(~(r1(X1,X2))|epred1_1(X2))&~(p101(X1)))&p100(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(10, plain,![X1]:![X2]:![X3]:((~(r1(X1,X2))|~(r1(X2,X3)))|r1(X1,X3)),inference(fof_nnf,[status(thm)],[2])).
% fof(11, plain,![X4]:![X5]:![X6]:((~(r1(X4,X5))|~(r1(X5,X6)))|r1(X4,X6)),inference(variable_rename,[status(thm)],[10])).
% cnf(12,plain,(r1(X1,X2)|~r1(X3,X2)|~r1(X1,X3)),inference(split_conjunct,[status(thm)],[11])).
% fof(13, negated_conjecture,?[X1]:(![X2]:(~(r1(X1,X2))|p5(X2))&((![X2]:(~(r1(X1,X2))|epred1_1(X2))&~(p101(X1)))&p100(X1))),inference(fof_nnf,[status(thm)],[7])).
% fof(14, negated_conjecture,?[X3]:(![X4]:(~(r1(X3,X4))|p5(X4))&((![X5]:(~(r1(X3,X5))|epred1_1(X5))&~(p101(X3)))&p100(X3))),inference(variable_rename,[status(thm)],[13])).
% fof(15, negated_conjecture,(![X4]:(~(r1(esk1_0,X4))|p5(X4))&((![X5]:(~(r1(esk1_0,X5))|epred1_1(X5))&~(p101(esk1_0)))&p100(esk1_0))),inference(skolemize,[status(esa)],[14])).
% fof(16, negated_conjecture,![X4]:![X5]:((((~(r1(esk1_0,X5))|epred1_1(X5))&~(p101(esk1_0)))&p100(esk1_0))&(~(r1(esk1_0,X4))|p5(X4))),inference(shift_quantors,[status(thm)],[15])).
% cnf(17,negated_conjecture,(p5(X1)|~r1(esk1_0,X1)),inference(split_conjunct,[status(thm)],[16])).
% cnf(18,negated_conjecture,(p100(esk1_0)),inference(split_conjunct,[status(thm)],[16])).
% cnf(19,negated_conjecture,(~p101(esk1_0)),inference(split_conjunct,[status(thm)],[16])).
% cnf(20,negated_conjecture,(epred1_1(X1)|~r1(esk1_0,X1)),inference(split_conjunct,[status(thm)],[16])).
% fof(21, plain,![X2]:(~(epred1_1(X2))|(((((((((((((((((((((((((((((((((?[X1]:(r1(X2,X1)&((~(p11(X1))&~(p111(X1)))&p110(X1)))&?[X1]:(r1(X2,X1)&((p11(X1)&~(p111(X1)))&p110(X1))))|(p110(X2)|~(p109(X2))))&((?[X1]:(r1(X2,X1)&((~(p10(X1))&~(p110(X1)))&p109(X1)))&?[X1]:(r1(X2,X1)&((p10(X1)&~(p110(X1)))&p109(X1))))|(p109(X2)|~(p108(X2)))))&((?[X1]:(r1(X2,X1)&((~(p9(X1))&~(p109(X1)))&p108(X1)))&?[X1]:(r1(X2,X1)&((p9(X1)&~(p109(X1)))&p108(X1))))|(p108(X2)|~(p107(X2)))))&((?[X1]:(r1(X2,X1)&((~(p8(X1))&~(p108(X1)))&p107(X1)))&?[X1]:(r1(X2,X1)&((p8(X1)&~(p108(X1)))&p107(X1))))|(p107(X2)|~(p106(X2)))))&((?[X1]:(r1(X2,X1)&((~(p7(X1))&~(p107(X1)))&p106(X1)))&?[X1]:(r1(X2,X1)&((p7(X1)&~(p107(X1)))&p106(X1))))|(p106(X2)|~(p105(X2)))))&((?[X1]:(r1(X2,X1)&((~(p6(X1))&~(p106(X1)))&p105(X1)))&?[X1]:(r1(X2,X1)&((p6(X1)&~(p106(X1)))&p105(X1))))|(p105(X2)|~(p104(X2)))))&((?[X1]:(r1(X2,X1)&((~(p5(X1))&~(p105(X1)))&p104(X1)))&?[X1]:(r1(X2,X1)&((p5(X1)&~(p105(X1)))&p104(X1))))|(p104(X2)|~(p103(X2)))))&((?[X1]:(r1(X2,X1)&((~(p4(X1))&~(p104(X1)))&p103(X1)))&?[X1]:(r1(X2,X1)&((p4(X1)&~(p104(X1)))&p103(X1))))|(p103(X2)|~(p102(X2)))))&((?[X1]:(r1(X2,X1)&((~(p3(X1))&~(p103(X1)))&p102(X1)))&?[X1]:(r1(X2,X1)&((p3(X1)&~(p103(X1)))&p102(X1))))|(p102(X2)|~(p101(X2)))))&((?[X1]:(r1(X2,X1)&((~(p2(X1))&~(p102(X1)))&p101(X1)))&?[X1]:(r1(X2,X1)&((p2(X1)&~(p102(X1)))&p101(X1))))|(p101(X2)|~(p100(X2)))))&(((![X1]:((~(r1(X2,X1))|~(p11(X1)))|~(p110(X1)))|p11(X2))&(![X1]:((~(r1(X2,X1))|p11(X1))|~(p110(X1)))|~(p11(X2))))|~(p110(X2))))&(((![X1]:((~(r1(X2,X1))|~(p10(X1)))|~(p109(X1)))|p10(X2))&(![X1]:((~(r1(X2,X1))|p10(X1))|~(p109(X1)))|~(p10(X2))))|~(p109(X2))))&(((![X1]:((~(r1(X2,X1))|~(p9(X1)))|~(p108(X1)))|p9(X2))&(![X1]:((~(r1(X2,X1))|p9(X1))|~(p108(X1)))|~(p9(X2))))|~(p108(X2))))&(((![X1]:((~(r1(X2,X1))|~(p8(X1)))|~(p107(X1)))|p8(X2))&(![X1]:((~(r1(X2,X1))|p8(X1))|~(p107(X1)))|~(p8(X2))))|~(p107(X2))))&(((![X1]:((~(r1(X2,X1))|~(p7(X1)))|~(p106(X1)))|p7(X2))&(![X1]:((~(r1(X2,X1))|p7(X1))|~(p106(X1)))|~(p7(X2))))|~(p106(X2))))&(((![X1]:((~(r1(X2,X1))|~(p6(X1)))|~(p105(X1)))|p6(X2))&(![X1]:((~(r1(X2,X1))|p6(X1))|~(p105(X1)))|~(p6(X2))))|~(p105(X2))))&(((![X1]:((~(r1(X2,X1))|~(p5(X1)))|~(p104(X1)))|p5(X2))&(![X1]:((~(r1(X2,X1))|p5(X1))|~(p104(X1)))|~(p5(X2))))|~(p104(X2))))&(((![X1]:((~(r1(X2,X1))|~(p4(X1)))|~(p103(X1)))|p4(X2))&(![X1]:((~(r1(X2,X1))|p4(X1))|~(p103(X1)))|~(p4(X2))))|~(p103(X2))))&(((![X1]:((~(r1(X2,X1))|~(p3(X1)))|~(p102(X1)))|p3(X2))&(![X1]:((~(r1(X2,X1))|p3(X1))|~(p102(X1)))|~(p3(X2))))|~(p102(X2))))&(((![X1]:((~(r1(X2,X1))|~(p2(X1)))|~(p101(X1)))|p2(X2))&(![X1]:((~(r1(X2,X1))|p2(X1))|~(p101(X1)))|~(p2(X2))))|~(p101(X2))))&(((![X1]:((~(r1(X2,X1))|~(p1(X1)))|~(p100(X1)))|p1(X2))&(![X1]:((~(r1(X2,X1))|p1(X1))|~(p100(X1)))|~(p1(X2))))|~(p100(X2))))&(p110(X2)|~(p111(X2))))&(p109(X2)|~(p110(X2))))&(p108(X2)|~(p109(X2))))&(p107(X2)|~(p108(X2))))&(p106(X2)|~(p107(X2))))&(p105(X2)|~(p106(X2))))&(p104(X2)|~(p105(X2))))&(p103(X2)|~(p104(X2))))&(p102(X2)|~(p103(X2))))&(p101(X2)|~(p102(X2))))&(p100(X2)|~(p101(X2))))),inference(fof_nnf,[status(thm)],[6])).
% fof(22, plain,![X3]:(~(epred1_1(X3))|(((((((((((((((((((((((((((((((((?[X4]:(r1(X3,X4)&((~(p11(X4))&~(p111(X4)))&p110(X4)))&?[X5]:(r1(X3,X5)&((p11(X5)&~(p111(X5)))&p110(X5))))|(p110(X3)|~(p109(X3))))&((?[X6]:(r1(X3,X6)&((~(p10(X6))&~(p110(X6)))&p109(X6)))&?[X7]:(r1(X3,X7)&((p10(X7)&~(p110(X7)))&p109(X7))))|(p109(X3)|~(p108(X3)))))&((?[X8]:(r1(X3,X8)&((~(p9(X8))&~(p109(X8)))&p108(X8)))&?[X9]:(r1(X3,X9)&((p9(X9)&~(p109(X9)))&p108(X9))))|(p108(X3)|~(p107(X3)))))&((?[X10]:(r1(X3,X10)&((~(p8(X10))&~(p108(X10)))&p107(X10)))&?[X11]:(r1(X3,X11)&((p8(X11)&~(p108(X11)))&p107(X11))))|(p107(X3)|~(p106(X3)))))&((?[X12]:(r1(X3,X12)&((~(p7(X12))&~(p107(X12)))&p106(X12)))&?[X13]:(r1(X3,X13)&((p7(X13)&~(p107(X13)))&p106(X13))))|(p106(X3)|~(p105(X3)))))&((?[X14]:(r1(X3,X14)&((~(p6(X14))&~(p106(X14)))&p105(X14)))&?[X15]:(r1(X3,X15)&((p6(X15)&~(p106(X15)))&p105(X15))))|(p105(X3)|~(p104(X3)))))&((?[X16]:(r1(X3,X16)&((~(p5(X16))&~(p105(X16)))&p104(X16)))&?[X17]:(r1(X3,X17)&((p5(X17)&~(p105(X17)))&p104(X17))))|(p104(X3)|~(p103(X3)))))&((?[X18]:(r1(X3,X18)&((~(p4(X18))&~(p104(X18)))&p103(X18)))&?[X19]:(r1(X3,X19)&((p4(X19)&~(p104(X19)))&p103(X19))))|(p103(X3)|~(p102(X3)))))&((?[X20]:(r1(X3,X20)&((~(p3(X20))&~(p103(X20)))&p102(X20)))&?[X21]:(r1(X3,X21)&((p3(X21)&~(p103(X21)))&p102(X21))))|(p102(X3)|~(p101(X3)))))&((?[X22]:(r1(X3,X22)&((~(p2(X22))&~(p102(X22)))&p101(X22)))&?[X23]:(r1(X3,X23)&((p2(X23)&~(p102(X23)))&p101(X23))))|(p101(X3)|~(p100(X3)))))&(((![X24]:((~(r1(X3,X24))|~(p11(X24)))|~(p110(X24)))|p11(X3))&(![X25]:((~(r1(X3,X25))|p11(X25))|~(p110(X25)))|~(p11(X3))))|~(p110(X3))))&(((![X26]:((~(r1(X3,X26))|~(p10(X26)))|~(p109(X26)))|p10(X3))&(![X27]:((~(r1(X3,X27))|p10(X27))|~(p109(X27)))|~(p10(X3))))|~(p109(X3))))&(((![X28]:((~(r1(X3,X28))|~(p9(X28)))|~(p108(X28)))|p9(X3))&(![X29]:((~(r1(X3,X29))|p9(X29))|~(p108(X29)))|~(p9(X3))))|~(p108(X3))))&(((![X30]:((~(r1(X3,X30))|~(p8(X30)))|~(p107(X30)))|p8(X3))&(![X31]:((~(r1(X3,X31))|p8(X31))|~(p107(X31)))|~(p8(X3))))|~(p107(X3))))&(((![X32]:((~(r1(X3,X32))|~(p7(X32)))|~(p106(X32)))|p7(X3))&(![X33]:((~(r1(X3,X33))|p7(X33))|~(p106(X33)))|~(p7(X3))))|~(p106(X3))))&(((![X34]:((~(r1(X3,X34))|~(p6(X34)))|~(p105(X34)))|p6(X3))&(![X35]:((~(r1(X3,X35))|p6(X35))|~(p105(X35)))|~(p6(X3))))|~(p105(X3))))&(((![X36]:((~(r1(X3,X36))|~(p5(X36)))|~(p104(X36)))|p5(X3))&(![X37]:((~(r1(X3,X37))|p5(X37))|~(p104(X37)))|~(p5(X3))))|~(p104(X3))))&(((![X38]:((~(r1(X3,X38))|~(p4(X38)))|~(p103(X38)))|p4(X3))&(![X39]:((~(r1(X3,X39))|p4(X39))|~(p103(X39)))|~(p4(X3))))|~(p103(X3))))&(((![X40]:((~(r1(X3,X40))|~(p3(X40)))|~(p102(X40)))|p3(X3))&(![X41]:((~(r1(X3,X41))|p3(X41))|~(p102(X41)))|~(p3(X3))))|~(p102(X3))))&(((![X42]:((~(r1(X3,X42))|~(p2(X42)))|~(p101(X42)))|p2(X3))&(![X43]:((~(r1(X3,X43))|p2(X43))|~(p101(X43)))|~(p2(X3))))|~(p101(X3))))&(((![X44]:((~(r1(X3,X44))|~(p1(X44)))|~(p100(X44)))|p1(X3))&(![X45]:((~(r1(X3,X45))|p1(X45))|~(p100(X45)))|~(p1(X3))))|~(p100(X3))))&(p110(X3)|~(p111(X3))))&(p109(X3)|~(p110(X3))))&(p108(X3)|~(p109(X3))))&(p107(X3)|~(p108(X3))))&(p106(X3)|~(p107(X3))))&(p105(X3)|~(p106(X3))))&(p104(X3)|~(p105(X3))))&(p103(X3)|~(p104(X3))))&(p102(X3)|~(p103(X3))))&(p101(X3)|~(p102(X3))))&(p100(X3)|~(p101(X3))))),inference(variable_rename,[status(thm)],[21])).
% fof(23, plain,![X3]:(~(epred1_1(X3))|((((((((((((((((((((((((((((((((((r1(X3,esk2_1(X3))&((~(p11(esk2_1(X3)))&~(p111(esk2_1(X3))))&p110(esk2_1(X3))))&(r1(X3,esk3_1(X3))&((p11(esk3_1(X3))&~(p111(esk3_1(X3))))&p110(esk3_1(X3)))))|(p110(X3)|~(p109(X3))))&(((r1(X3,esk4_1(X3))&((~(p10(esk4_1(X3)))&~(p110(esk4_1(X3))))&p109(esk4_1(X3))))&(r1(X3,esk5_1(X3))&((p10(esk5_1(X3))&~(p110(esk5_1(X3))))&p109(esk5_1(X3)))))|(p109(X3)|~(p108(X3)))))&(((r1(X3,esk6_1(X3))&((~(p9(esk6_1(X3)))&~(p109(esk6_1(X3))))&p108(esk6_1(X3))))&(r1(X3,esk7_1(X3))&((p9(esk7_1(X3))&~(p109(esk7_1(X3))))&p108(esk7_1(X3)))))|(p108(X3)|~(p107(X3)))))&(((r1(X3,esk8_1(X3))&((~(p8(esk8_1(X3)))&~(p108(esk8_1(X3))))&p107(esk8_1(X3))))&(r1(X3,esk9_1(X3))&((p8(esk9_1(X3))&~(p108(esk9_1(X3))))&p107(esk9_1(X3)))))|(p107(X3)|~(p106(X3)))))&(((r1(X3,esk10_1(X3))&((~(p7(esk10_1(X3)))&~(p107(esk10_1(X3))))&p106(esk10_1(X3))))&(r1(X3,esk11_1(X3))&((p7(esk11_1(X3))&~(p107(esk11_1(X3))))&p106(esk11_1(X3)))))|(p106(X3)|~(p105(X3)))))&(((r1(X3,esk12_1(X3))&((~(p6(esk12_1(X3)))&~(p106(esk12_1(X3))))&p105(esk12_1(X3))))&(r1(X3,esk13_1(X3))&((p6(esk13_1(X3))&~(p106(esk13_1(X3))))&p105(esk13_1(X3)))))|(p105(X3)|~(p104(X3)))))&(((r1(X3,esk14_1(X3))&((~(p5(esk14_1(X3)))&~(p105(esk14_1(X3))))&p104(esk14_1(X3))))&(r1(X3,esk15_1(X3))&((p5(esk15_1(X3))&~(p105(esk15_1(X3))))&p104(esk15_1(X3)))))|(p104(X3)|~(p103(X3)))))&(((r1(X3,esk16_1(X3))&((~(p4(esk16_1(X3)))&~(p104(esk16_1(X3))))&p103(esk16_1(X3))))&(r1(X3,esk17_1(X3))&((p4(esk17_1(X3))&~(p104(esk17_1(X3))))&p103(esk17_1(X3)))))|(p103(X3)|~(p102(X3)))))&(((r1(X3,esk18_1(X3))&((~(p3(esk18_1(X3)))&~(p103(esk18_1(X3))))&p102(esk18_1(X3))))&(r1(X3,esk19_1(X3))&((p3(esk19_1(X3))&~(p103(esk19_1(X3))))&p102(esk19_1(X3)))))|(p102(X3)|~(p101(X3)))))&(((r1(X3,esk20_1(X3))&((~(p2(esk20_1(X3)))&~(p102(esk20_1(X3))))&p101(esk20_1(X3))))&(r1(X3,esk21_1(X3))&((p2(esk21_1(X3))&~(p102(esk21_1(X3))))&p101(esk21_1(X3)))))|(p101(X3)|~(p100(X3)))))&(((![X24]:((~(r1(X3,X24))|~(p11(X24)))|~(p110(X24)))|p11(X3))&(![X25]:((~(r1(X3,X25))|p11(X25))|~(p110(X25)))|~(p11(X3))))|~(p110(X3))))&(((![X26]:((~(r1(X3,X26))|~(p10(X26)))|~(p109(X26)))|p10(X3))&(![X27]:((~(r1(X3,X27))|p10(X27))|~(p109(X27)))|~(p10(X3))))|~(p109(X3))))&(((![X28]:((~(r1(X3,X28))|~(p9(X28)))|~(p108(X28)))|p9(X3))&(![X29]:((~(r1(X3,X29))|p9(X29))|~(p108(X29)))|~(p9(X3))))|~(p108(X3))))&(((![X30]:((~(r1(X3,X30))|~(p8(X30)))|~(p107(X30)))|p8(X3))&(![X31]:((~(r1(X3,X31))|p8(X31))|~(p107(X31)))|~(p8(X3))))|~(p107(X3))))&(((![X32]:((~(r1(X3,X32))|~(p7(X32)))|~(p106(X32)))|p7(X3))&(![X33]:((~(r1(X3,X33))|p7(X33))|~(p106(X33)))|~(p7(X3))))|~(p106(X3))))&(((![X34]:((~(r1(X3,X34))|~(p6(X34)))|~(p105(X34)))|p6(X3))&(![X35]:((~(r1(X3,X35))|p6(X35))|~(p105(X35)))|~(p6(X3))))|~(p105(X3))))&(((![X36]:((~(r1(X3,X36))|~(p5(X36)))|~(p104(X36)))|p5(X3))&(![X37]:((~(r1(X3,X37))|p5(X37))|~(p104(X37)))|~(p5(X3))))|~(p104(X3))))&(((![X38]:((~(r1(X3,X38))|~(p4(X38)))|~(p103(X38)))|p4(X3))&(![X39]:((~(r1(X3,X39))|p4(X39))|~(p103(X39)))|~(p4(X3))))|~(p103(X3))))&(((![X40]:((~(r1(X3,X40))|~(p3(X40)))|~(p102(X40)))|p3(X3))&(![X41]:((~(r1(X3,X41))|p3(X41))|~(p102(X41)))|~(p3(X3))))|~(p102(X3))))&(((![X42]:((~(r1(X3,X42))|~(p2(X42)))|~(p101(X42)))|p2(X3))&(![X43]:((~(r1(X3,X43))|p2(X43))|~(p101(X43)))|~(p2(X3))))|~(p101(X3))))&(((![X44]:((~(r1(X3,X44))|~(p1(X44)))|~(p100(X44)))|p1(X3))&(![X45]:((~(r1(X3,X45))|p1(X45))|~(p100(X45)))|~(p1(X3))))|~(p100(X3))))&(p110(X3)|~(p111(X3))))&(p109(X3)|~(p110(X3))))&(p108(X3)|~(p109(X3))))&(p107(X3)|~(p108(X3))))&(p106(X3)|~(p107(X3))))&(p105(X3)|~(p106(X3))))&(p104(X3)|~(p105(X3))))&(p103(X3)|~(p104(X3))))&(p102(X3)|~(p103(X3))))&(p101(X3)|~(p102(X3))))&(p100(X3)|~(p101(X3))))),inference(skolemize,[status(esa)],[22])).
% fof(24, plain,![X3]:![X24]:![X25]:![X26]:![X27]:![X28]:![X29]:![X30]:![X31]:![X32]:![X33]:![X34]:![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:![X42]:![X43]:![X44]:![X45]:((((((((((((((((((~(r1(X3,X45))|p1(X45))|~(p100(X45)))|~(p1(X3)))&(((~(r1(X3,X44))|~(p1(X44)))|~(p100(X44)))|p1(X3)))|~(p100(X3)))&((((((~(r1(X3,X43))|p2(X43))|~(p101(X43)))|~(p2(X3)))&(((~(r1(X3,X42))|~(p2(X42)))|~(p101(X42)))|p2(X3)))|~(p101(X3)))&((((((~(r1(X3,X41))|p3(X41))|~(p102(X41)))|~(p3(X3)))&(((~(r1(X3,X40))|~(p3(X40)))|~(p102(X40)))|p3(X3)))|~(p102(X3)))&((((((~(r1(X3,X39))|p4(X39))|~(p103(X39)))|~(p4(X3)))&(((~(r1(X3,X38))|~(p4(X38)))|~(p103(X38)))|p4(X3)))|~(p103(X3)))&((((((~(r1(X3,X37))|p5(X37))|~(p104(X37)))|~(p5(X3)))&(((~(r1(X3,X36))|~(p5(X36)))|~(p104(X36)))|p5(X3)))|~(p104(X3)))&((((((~(r1(X3,X35))|p6(X35))|~(p105(X35)))|~(p6(X3)))&(((~(r1(X3,X34))|~(p6(X34)))|~(p105(X34)))|p6(X3)))|~(p105(X3)))&((((((~(r1(X3,X33))|p7(X33))|~(p106(X33)))|~(p7(X3)))&(((~(r1(X3,X32))|~(p7(X32)))|~(p106(X32)))|p7(X3)))|~(p106(X3)))&((((((~(r1(X3,X31))|p8(X31))|~(p107(X31)))|~(p8(X3)))&(((~(r1(X3,X30))|~(p8(X30)))|~(p107(X30)))|p8(X3)))|~(p107(X3)))&((((((~(r1(X3,X29))|p9(X29))|~(p108(X29)))|~(p9(X3)))&(((~(r1(X3,X28))|~(p9(X28)))|~(p108(X28)))|p9(X3)))|~(p108(X3)))&((((((~(r1(X3,X27))|p10(X27))|~(p109(X27)))|~(p10(X3)))&(((~(r1(X3,X26))|~(p10(X26)))|~(p109(X26)))|p10(X3)))|~(p109(X3)))&((((((~(r1(X3,X25))|p11(X25))|~(p110(X25)))|~(p11(X3)))&(((~(r1(X3,X24))|~(p11(X24)))|~(p110(X24)))|p11(X3)))|~(p110(X3)))&((((((((((((r1(X3,esk2_1(X3))&((~(p11(esk2_1(X3)))&~(p111(esk2_1(X3))))&p110(esk2_1(X3))))&(r1(X3,esk3_1(X3))&((p11(esk3_1(X3))&~(p111(esk3_1(X3))))&p110(esk3_1(X3)))))|(p110(X3)|~(p109(X3))))&(((r1(X3,esk4_1(X3))&((~(p10(esk4_1(X3)))&~(p110(esk4_1(X3))))&p109(esk4_1(X3))))&(r1(X3,esk5_1(X3))&((p10(esk5_1(X3))&~(p110(esk5_1(X3))))&p109(esk5_1(X3)))))|(p109(X3)|~(p108(X3)))))&(((r1(X3,esk6_1(X3))&((~(p9(esk6_1(X3)))&~(p109(esk6_1(X3))))&p108(esk6_1(X3))))&(r1(X3,esk7_1(X3))&((p9(esk7_1(X3))&~(p109(esk7_1(X3))))&p108(esk7_1(X3)))))|(p108(X3)|~(p107(X3)))))&(((r1(X3,esk8_1(X3))&((~(p8(esk8_1(X3)))&~(p108(esk8_1(X3))))&p107(esk8_1(X3))))&(r1(X3,esk9_1(X3))&((p8(esk9_1(X3))&~(p108(esk9_1(X3))))&p107(esk9_1(X3)))))|(p107(X3)|~(p106(X3)))))&(((r1(X3,esk10_1(X3))&((~(p7(esk10_1(X3)))&~(p107(esk10_1(X3))))&p106(esk10_1(X3))))&(r1(X3,esk11_1(X3))&((p7(esk11_1(X3))&~(p107(esk11_1(X3))))&p106(esk11_1(X3)))))|(p106(X3)|~(p105(X3)))))&(((r1(X3,esk12_1(X3))&((~(p6(esk12_1(X3)))&~(p106(esk12_1(X3))))&p105(esk12_1(X3))))&(r1(X3,esk13_1(X3))&((p6(esk13_1(X3))&~(p106(esk13_1(X3))))&p105(esk13_1(X3)))))|(p105(X3)|~(p104(X3)))))&(((r1(X3,esk14_1(X3))&((~(p5(esk14_1(X3)))&~(p105(esk14_1(X3))))&p104(esk14_1(X3))))&(r1(X3,esk15_1(X3))&((p5(esk15_1(X3))&~(p105(esk15_1(X3))))&p104(esk15_1(X3)))))|(p104(X3)|~(p103(X3)))))&(((r1(X3,esk16_1(X3))&((~(p4(esk16_1(X3)))&~(p104(esk16_1(X3))))&p103(esk16_1(X3))))&(r1(X3,esk17_1(X3))&((p4(esk17_1(X3))&~(p104(esk17_1(X3))))&p103(esk17_1(X3)))))|(p103(X3)|~(p102(X3)))))&(((r1(X3,esk18_1(X3))&((~(p3(esk18_1(X3)))&~(p103(esk18_1(X3))))&p102(esk18_1(X3))))&(r1(X3,esk19_1(X3))&((p3(esk19_1(X3))&~(p103(esk19_1(X3))))&p102(esk19_1(X3)))))|(p102(X3)|~(p101(X3)))))&(((r1(X3,esk20_1(X3))&((~(p2(esk20_1(X3)))&~(p102(esk20_1(X3))))&p101(esk20_1(X3))))&(r1(X3,esk21_1(X3))&((p2(esk21_1(X3))&~(p102(esk21_1(X3))))&p101(esk21_1(X3)))))|(p101(X3)|~(p100(X3))))))))))))))))&(p110(X3)|~(p111(X3))))&(p109(X3)|~(p110(X3))))&(p108(X3)|~(p109(X3))))&(p107(X3)|~(p108(X3))))&(p106(X3)|~(p107(X3))))&(p105(X3)|~(p106(X3))))&(p104(X3)|~(p105(X3))))&(p103(X3)|~(p104(X3))))&(p102(X3)|~(p103(X3))))&(p101(X3)|~(p102(X3))))&(p100(X3)|~(p101(X3))))|~(epred1_1(X3))),inference(shift_quantors,[status(thm)],[23])).
% fof(25, plain,![X3]:![X24]:![X25]:![X26]:![X27]:![X28]:![X29]:![X30]:![X31]:![X32]:![X33]:![X34]:![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:![X41]:![X42]:![X43]:![X44]:![X45]:((((((((((((((((((~(r1(X3,X45))|p1(X45))|~(p100(X45)))|~(p1(X3)))|~(p100(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X44))|~(p1(X44)))|~(p100(X44)))|p1(X3))|~(p100(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X43))|p2(X43))|~(p101(X43)))|~(p2(X3)))|~(p101(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X42))|~(p2(X42)))|~(p101(X42)))|p2(X3))|~(p101(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X41))|p3(X41))|~(p102(X41)))|~(p3(X3)))|~(p102(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X40))|~(p3(X40)))|~(p102(X40)))|p3(X3))|~(p102(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X39))|p4(X39))|~(p103(X39)))|~(p4(X3)))|~(p103(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X38))|~(p4(X38)))|~(p103(X38)))|p4(X3))|~(p103(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X37))|p5(X37))|~(p104(X37)))|~(p5(X3)))|~(p104(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X36))|~(p5(X36)))|~(p104(X36)))|p5(X3))|~(p104(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X35))|p6(X35))|~(p105(X35)))|~(p6(X3)))|~(p105(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X34))|~(p6(X34)))|~(p105(X34)))|p6(X3))|~(p105(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X33))|p7(X33))|~(p106(X33)))|~(p7(X3)))|~(p106(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X32))|~(p7(X32)))|~(p106(X32)))|p7(X3))|~(p106(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X31))|p8(X31))|~(p107(X31)))|~(p8(X3)))|~(p107(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X30))|~(p8(X30)))|~(p107(X30)))|p8(X3))|~(p107(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X29))|p9(X29))|~(p108(X29)))|~(p9(X3)))|~(p108(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X28))|~(p9(X28)))|~(p108(X28)))|p9(X3))|~(p108(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X27))|p10(X27))|~(p109(X27)))|~(p10(X3)))|~(p109(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X26))|~(p10(X26)))|~(p109(X26)))|p10(X3))|~(p109(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X25))|p11(X25))|~(p110(X25)))|~(p11(X3)))|~(p110(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X24))|~(p11(X24)))|~(p110(X24)))|p11(X3))|~(p110(X3)))|~(epred1_1(X3))))&(((((((((((((r1(X3,esk2_1(X3))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3)))&((((~(p11(esk2_1(X3)))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3)))&((~(p111(esk2_1(X3)))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3))))&((p110(esk2_1(X3))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk3_1(X3))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3)))&((((p11(esk3_1(X3))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3)))&((~(p111(esk3_1(X3)))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3))))&((p110(esk3_1(X3))|(p110(X3)|~(p109(X3))))|~(epred1_1(X3))))))&((((r1(X3,esk4_1(X3))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3)))&((((~(p10(esk4_1(X3)))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3)))&((~(p110(esk4_1(X3)))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3))))&((p109(esk4_1(X3))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk5_1(X3))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3)))&((((p10(esk5_1(X3))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3)))&((~(p110(esk5_1(X3)))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3))))&((p109(esk5_1(X3))|(p109(X3)|~(p108(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk6_1(X3))|(p108(X3)|~(p107(X3))))|~(epred1_1(X3)))&((((~(p9(esk6_1(X3)))|(p108(X3)|~(p107(X3))))|~(epred1_1(X3)))&((~(p109(esk6_1(X3)))|(p108(X3)|~(p107(X3))))|~(epred1_1(X3))))&((p108(esk6_1(X3))|(p108(X3)|~(p107(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk7_1(X3))|(p108(X3)|~(p107(X3))))|~(epred1_1(X3)))&((((p9(esk7_1(X3))|(p108(X3)|~(p107(X3))))|~(epred1_1(X3)))&((~(p109(esk7_1(X3)))|(p108(X3)|~(p107(X3))))|~(epred1_1(X3))))&((p108(esk7_1(X3))|(p108(X3)|~(p107(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk8_1(X3))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3)))&((((~(p8(esk8_1(X3)))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3)))&((~(p108(esk8_1(X3)))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3))))&((p107(esk8_1(X3))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk9_1(X3))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3)))&((((p8(esk9_1(X3))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3)))&((~(p108(esk9_1(X3)))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3))))&((p107(esk9_1(X3))|(p107(X3)|~(p106(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk10_1(X3))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3)))&((((~(p7(esk10_1(X3)))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3)))&((~(p107(esk10_1(X3)))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3))))&((p106(esk10_1(X3))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk11_1(X3))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3)))&((((p7(esk11_1(X3))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3)))&((~(p107(esk11_1(X3)))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3))))&((p106(esk11_1(X3))|(p106(X3)|~(p105(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk12_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))&((((~(p6(esk12_1(X3)))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))&((~(p106(esk12_1(X3)))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3))))&((p105(esk12_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk13_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))&((((p6(esk13_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))&((~(p106(esk13_1(X3)))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3))))&((p105(esk13_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk14_1(X3))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3)))&((((~(p5(esk14_1(X3)))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3)))&((~(p105(esk14_1(X3)))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3))))&((p104(esk14_1(X3))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk15_1(X3))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3)))&((((p5(esk15_1(X3))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3)))&((~(p105(esk15_1(X3)))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3))))&((p104(esk15_1(X3))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk16_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))&((((~(p4(esk16_1(X3)))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))&((~(p104(esk16_1(X3)))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3))))&((p103(esk16_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk17_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))&((((p4(esk17_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))&((~(p104(esk17_1(X3)))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3))))&((p103(esk17_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk18_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))&((((~(p3(esk18_1(X3)))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))&((~(p103(esk18_1(X3)))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3))))&((p102(esk18_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk19_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))&((((p3(esk19_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))&((~(p103(esk19_1(X3)))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3))))&((p102(esk19_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk20_1(X3))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3)))&((((~(p2(esk20_1(X3)))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3)))&((~(p102(esk20_1(X3)))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3))))&((p101(esk20_1(X3))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk21_1(X3))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3)))&((((p2(esk21_1(X3))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3)))&((~(p102(esk21_1(X3)))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3))))&((p101(esk21_1(X3))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3))))))))))))))))))&((p110(X3)|~(p111(X3)))|~(epred1_1(X3))))&((p109(X3)|~(p110(X3)))|~(epred1_1(X3))))&((p108(X3)|~(p109(X3)))|~(epred1_1(X3))))&((p107(X3)|~(p108(X3)))|~(epred1_1(X3))))&((p106(X3)|~(p107(X3)))|~(epred1_1(X3))))&((p105(X3)|~(p106(X3)))|~(epred1_1(X3))))&((p104(X3)|~(p105(X3)))|~(epred1_1(X3))))&((p103(X3)|~(p104(X3)))|~(epred1_1(X3))))&((p102(X3)|~(p103(X3)))|~(epred1_1(X3))))&((p101(X3)|~(p102(X3)))|~(epred1_1(X3))))&((p100(X3)|~(p101(X3)))|~(epred1_1(X3)))),inference(distribute,[status(thm)],[24])).
% cnf(37,plain,(p101(X1)|p101(esk21_1(X1))|~epred1_1(X1)|~p100(X1)),inference(split_conjunct,[status(thm)],[25])).
% cnf(38,plain,(p101(X1)|~epred1_1(X1)|~p100(X1)|~p102(esk21_1(X1))),inference(split_conjunct,[status(thm)],[25])).
% cnf(40,plain,(p101(X1)|r1(X1,esk21_1(X1))|~epred1_1(X1)|~p100(X1)),inference(split_conjunct,[status(thm)],[25])).
% cnf(45,plain,(p102(X1)|p102(esk19_1(X1))|~epred1_1(X1)|~p101(X1)),inference(split_conjunct,[status(thm)],[25])).
% cnf(46,plain,(p102(X1)|~epred1_1(X1)|~p101(X1)|~p103(esk19_1(X1))),inference(split_conjunct,[status(thm)],[25])).
% cnf(48,plain,(p102(X1)|r1(X1,esk19_1(X1))|~epred1_1(X1)|~p101(X1)),inference(split_conjunct,[status(thm)],[25])).
% cnf(53,plain,(p103(X1)|p103(esk17_1(X1))|~epred1_1(X1)|~p102(X1)),inference(split_conjunct,[status(thm)],[25])).
% cnf(54,plain,(p103(X1)|~epred1_1(X1)|~p102(X1)|~p104(esk17_1(X1))),inference(split_conjunct,[status(thm)],[25])).
% cnf(56,plain,(p103(X1)|r1(X1,esk17_1(X1))|~epred1_1(X1)|~p102(X1)),inference(split_conjunct,[status(thm)],[25])).
% cnf(67,plain,(p104(X1)|~epred1_1(X1)|~p103(X1)|~p5(esk14_1(X1))),inference(split_conjunct,[status(thm)],[25])).
% cnf(68,plain,(p104(X1)|r1(X1,esk14_1(X1))|~epred1_1(X1)|~p103(X1)),inference(split_conjunct,[status(thm)],[25])).
% cnf(140,negated_conjecture,(epred1_1(esk1_0)),inference(spm,[status(thm)],[20,9,theory(equality)])).
% cnf(153,negated_conjecture,(epred1_1(esk21_1(esk1_0))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[20,40,theory(equality)])).
% cnf(158,negated_conjecture,(epred1_1(esk21_1(esk1_0))|p101(esk1_0)|~epred1_1(esk1_0)|$false),inference(rw,[status(thm)],[153,18,theory(equality)])).
% cnf(159,negated_conjecture,(epred1_1(esk21_1(esk1_0))|p101(esk1_0)|~epred1_1(esk1_0)),inference(cn,[status(thm)],[158,theory(equality)])).
% cnf(160,negated_conjecture,(epred1_1(esk21_1(esk1_0))|~epred1_1(esk1_0)),inference(sr,[status(thm)],[159,19,theory(equality)])).
% cnf(168,plain,(r1(X1,esk19_1(X2))|p102(X2)|~r1(X1,X2)|~epred1_1(X2)|~p101(X2)),inference(spm,[status(thm)],[12,48,theory(equality)])).
% cnf(211,plain,(r1(X1,esk14_1(X2))|p104(X2)|~r1(X1,X2)|~epred1_1(X2)|~p103(X2)),inference(spm,[status(thm)],[12,68,theory(equality)])).
% cnf(220,plain,(r1(X1,esk17_1(X2))|p103(X2)|~r1(X1,X2)|~epred1_1(X2)|~p102(X2)),inference(spm,[status(thm)],[12,56,theory(equality)])).
% cnf(716,negated_conjecture,(epred1_1(esk21_1(esk1_0))|$false),inference(rw,[status(thm)],[160,140,theory(equality)])).
% cnf(717,negated_conjecture,(epred1_1(esk21_1(esk1_0))),inference(cn,[status(thm)],[716,theory(equality)])).
% cnf(898,plain,(p102(esk21_1(X1))|r1(X1,esk19_1(esk21_1(X1)))|p101(X1)|~epred1_1(esk21_1(X1))|~p101(esk21_1(X1))|~epred1_1(X1)|~p100(X1)),inference(spm,[status(thm)],[168,40,theory(equality)])).
% cnf(1214,plain,(p104(esk17_1(X1))|r1(X1,esk14_1(esk17_1(X1)))|p103(X1)|~epred1_1(esk17_1(X1))|~p103(esk17_1(X1))|~epred1_1(X1)|~p102(X1)),inference(spm,[status(thm)],[211,56,theory(equality)])).
% cnf(1275,plain,(p103(esk19_1(X1))|r1(X1,esk17_1(esk19_1(X1)))|p102(X1)|~epred1_1(esk19_1(X1))|~p102(esk19_1(X1))|~epred1_1(X1)|~p101(X1)),inference(spm,[status(thm)],[220,48,theory(equality)])).
% cnf(1973,plain,(p101(X1)|p102(esk21_1(X1))|r1(X1,esk19_1(esk21_1(X1)))|~epred1_1(esk21_1(X1))|~epred1_1(X1)|~p100(X1)),inference(csr,[status(thm)],[898,37])).
% cnf(1974,plain,(p101(X1)|r1(X1,esk19_1(esk21_1(X1)))|~epred1_1(esk21_1(X1))|~epred1_1(X1)|~p100(X1)),inference(csr,[status(thm)],[1973,38])).
% cnf(1975,negated_conjecture,(p101(esk1_0)|r1(esk1_0,esk19_1(esk21_1(esk1_0)))|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[1974,717,theory(equality)])).
% cnf(1976,negated_conjecture,(p101(esk1_0)|r1(esk1_0,esk19_1(esk21_1(esk1_0)))|$false|~p100(esk1_0)),inference(rw,[status(thm)],[1975,140,theory(equality)])).
% cnf(1977,negated_conjecture,(p101(esk1_0)|r1(esk1_0,esk19_1(esk21_1(esk1_0)))|$false|$false),inference(rw,[status(thm)],[1976,18,theory(equality)])).
% cnf(1978,negated_conjecture,(p101(esk1_0)|r1(esk1_0,esk19_1(esk21_1(esk1_0)))),inference(cn,[status(thm)],[1977,theory(equality)])).
% cnf(1979,negated_conjecture,(r1(esk1_0,esk19_1(esk21_1(esk1_0)))),inference(sr,[status(thm)],[1978,19,theory(equality)])).
% cnf(2024,negated_conjecture,(epred1_1(esk19_1(esk21_1(esk1_0)))),inference(spm,[status(thm)],[20,1979,theory(equality)])).
% cnf(6855,plain,(p102(X1)|p103(esk19_1(X1))|r1(X1,esk17_1(esk19_1(X1)))|~epred1_1(esk19_1(X1))|~epred1_1(X1)|~p101(X1)),inference(csr,[status(thm)],[1275,45])).
% cnf(6856,plain,(p102(X1)|r1(X1,esk17_1(esk19_1(X1)))|~epred1_1(esk19_1(X1))|~epred1_1(X1)|~p101(X1)),inference(csr,[status(thm)],[6855,46])).
% cnf(6857,negated_conjecture,(p102(esk21_1(esk1_0))|r1(esk21_1(esk1_0),esk17_1(esk19_1(esk21_1(esk1_0))))|~epred1_1(esk21_1(esk1_0))|~p101(esk21_1(esk1_0))),inference(spm,[status(thm)],[6856,2024,theory(equality)])).
% cnf(6859,negated_conjecture,(p102(esk21_1(esk1_0))|r1(esk21_1(esk1_0),esk17_1(esk19_1(esk21_1(esk1_0))))|$false|~p101(esk21_1(esk1_0))),inference(rw,[status(thm)],[6857,717,theory(equality)])).
% cnf(6860,negated_conjecture,(p102(esk21_1(esk1_0))|r1(esk21_1(esk1_0),esk17_1(esk19_1(esk21_1(esk1_0))))|~p101(esk21_1(esk1_0))),inference(cn,[status(thm)],[6859,theory(equality)])).
% cnf(6864,plain,(p102(esk21_1(esk1_0))|r1(esk21_1(esk1_0),esk17_1(esk19_1(esk21_1(esk1_0))))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[6860,37,theory(equality)])).
% cnf(6867,plain,(p102(esk21_1(esk1_0))|r1(esk21_1(esk1_0),esk17_1(esk19_1(esk21_1(esk1_0))))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[6864,140,theory(equality)])).
% cnf(6868,plain,(p102(esk21_1(esk1_0))|r1(esk21_1(esk1_0),esk17_1(esk19_1(esk21_1(esk1_0))))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[6867,18,theory(equality)])).
% cnf(6869,plain,(p102(esk21_1(esk1_0))|r1(esk21_1(esk1_0),esk17_1(esk19_1(esk21_1(esk1_0))))|p101(esk1_0)),inference(cn,[status(thm)],[6868,theory(equality)])).
% cnf(6870,plain,(p102(esk21_1(esk1_0))|r1(esk21_1(esk1_0),esk17_1(esk19_1(esk21_1(esk1_0))))),inference(sr,[status(thm)],[6869,19,theory(equality)])).
% cnf(6882,plain,(r1(X1,esk17_1(esk19_1(esk21_1(esk1_0))))|p102(esk21_1(esk1_0))|~r1(X1,esk21_1(esk1_0))),inference(spm,[status(thm)],[12,6870,theory(equality)])).
% cnf(7070,plain,(p102(esk21_1(esk1_0))|r1(esk1_0,esk17_1(esk19_1(esk21_1(esk1_0))))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[6882,40,theory(equality)])).
% cnf(7071,plain,(p102(esk21_1(esk1_0))|r1(esk1_0,esk17_1(esk19_1(esk21_1(esk1_0))))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[7070,140,theory(equality)])).
% cnf(7072,plain,(p102(esk21_1(esk1_0))|r1(esk1_0,esk17_1(esk19_1(esk21_1(esk1_0))))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[7071,18,theory(equality)])).
% cnf(7073,plain,(p102(esk21_1(esk1_0))|r1(esk1_0,esk17_1(esk19_1(esk21_1(esk1_0))))|p101(esk1_0)),inference(cn,[status(thm)],[7072,theory(equality)])).
% cnf(7074,plain,(p102(esk21_1(esk1_0))|r1(esk1_0,esk17_1(esk19_1(esk21_1(esk1_0))))),inference(sr,[status(thm)],[7073,19,theory(equality)])).
% cnf(7119,negated_conjecture,(epred1_1(esk17_1(esk19_1(esk21_1(esk1_0))))|p102(esk21_1(esk1_0))),inference(spm,[status(thm)],[20,7074,theory(equality)])).
% cnf(8833,plain,(p103(X1)|p104(esk17_1(X1))|r1(X1,esk14_1(esk17_1(X1)))|~epred1_1(esk17_1(X1))|~epred1_1(X1)|~p102(X1)),inference(csr,[status(thm)],[1214,53])).
% cnf(8834,plain,(p103(X1)|r1(X1,esk14_1(esk17_1(X1)))|~epred1_1(esk17_1(X1))|~epred1_1(X1)|~p102(X1)),inference(csr,[status(thm)],[8833,54])).
% cnf(8835,negated_conjecture,(p103(esk19_1(esk21_1(esk1_0)))|r1(esk19_1(esk21_1(esk1_0)),esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))|p102(esk21_1(esk1_0))|~epred1_1(esk19_1(esk21_1(esk1_0)))|~p102(esk19_1(esk21_1(esk1_0)))),inference(spm,[status(thm)],[8834,7119,theory(equality)])).
% cnf(8839,negated_conjecture,(p103(esk19_1(esk21_1(esk1_0)))|r1(esk19_1(esk21_1(esk1_0)),esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))|p102(esk21_1(esk1_0))|$false|~p102(esk19_1(esk21_1(esk1_0)))),inference(rw,[status(thm)],[8835,2024,theory(equality)])).
% cnf(8840,negated_conjecture,(p103(esk19_1(esk21_1(esk1_0)))|r1(esk19_1(esk21_1(esk1_0)),esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))|p102(esk21_1(esk1_0))|~p102(esk19_1(esk21_1(esk1_0)))),inference(cn,[status(thm)],[8839,theory(equality)])).
% cnf(9002,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|r1(esk19_1(esk21_1(esk1_0)),esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))|~epred1_1(esk21_1(esk1_0))|~p101(esk21_1(esk1_0))),inference(spm,[status(thm)],[8840,45,theory(equality)])).
% cnf(9005,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|r1(esk19_1(esk21_1(esk1_0)),esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))|$false|~p101(esk21_1(esk1_0))),inference(rw,[status(thm)],[9002,717,theory(equality)])).
% cnf(9006,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|r1(esk19_1(esk21_1(esk1_0)),esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))|~p101(esk21_1(esk1_0))),inference(cn,[status(thm)],[9005,theory(equality)])).
% cnf(9010,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|r1(esk19_1(esk21_1(esk1_0)),esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[9006,37,theory(equality)])).
% cnf(9013,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|r1(esk19_1(esk21_1(esk1_0)),esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[9010,140,theory(equality)])).
% cnf(9014,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|r1(esk19_1(esk21_1(esk1_0)),esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[9013,18,theory(equality)])).
% cnf(9015,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|r1(esk19_1(esk21_1(esk1_0)),esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))|p101(esk1_0)),inference(cn,[status(thm)],[9014,theory(equality)])).
% cnf(9016,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|r1(esk19_1(esk21_1(esk1_0)),esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))),inference(sr,[status(thm)],[9015,19,theory(equality)])).
% cnf(9028,plain,(r1(X1,esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))|p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|~r1(X1,esk19_1(esk21_1(esk1_0)))),inference(spm,[status(thm)],[12,9016,theory(equality)])).
% cnf(9106,negated_conjecture,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|r1(esk1_0,esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))),inference(spm,[status(thm)],[9028,1979,theory(equality)])).
% cnf(9154,negated_conjecture,(p5(esk14_1(esk17_1(esk19_1(esk21_1(esk1_0)))))|p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))),inference(spm,[status(thm)],[17,9106,theory(equality)])).
% cnf(9204,plain,(p104(esk17_1(esk19_1(esk21_1(esk1_0))))|p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|~epred1_1(esk17_1(esk19_1(esk21_1(esk1_0))))|~p103(esk17_1(esk19_1(esk21_1(esk1_0))))),inference(spm,[status(thm)],[67,9154,theory(equality)])).
% cnf(14527,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p104(esk17_1(esk19_1(esk21_1(esk1_0))))|~p103(esk17_1(esk19_1(esk21_1(esk1_0))))),inference(csr,[status(thm)],[9204,7119])).
% cnf(14529,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p104(esk17_1(esk19_1(esk21_1(esk1_0))))|~epred1_1(esk19_1(esk21_1(esk1_0)))|~p102(esk19_1(esk21_1(esk1_0)))),inference(spm,[status(thm)],[14527,53,theory(equality)])).
% cnf(14530,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p104(esk17_1(esk19_1(esk21_1(esk1_0))))|$false|~p102(esk19_1(esk21_1(esk1_0)))),inference(rw,[status(thm)],[14529,2024,theory(equality)])).
% cnf(14531,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p104(esk17_1(esk19_1(esk21_1(esk1_0))))|~p102(esk19_1(esk21_1(esk1_0)))),inference(cn,[status(thm)],[14530,theory(equality)])).
% cnf(14535,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p104(esk17_1(esk19_1(esk21_1(esk1_0))))|~epred1_1(esk21_1(esk1_0))|~p101(esk21_1(esk1_0))),inference(spm,[status(thm)],[14531,45,theory(equality)])).
% cnf(14538,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p104(esk17_1(esk19_1(esk21_1(esk1_0))))|$false|~p101(esk21_1(esk1_0))),inference(rw,[status(thm)],[14535,717,theory(equality)])).
% cnf(14539,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p104(esk17_1(esk19_1(esk21_1(esk1_0))))|~p101(esk21_1(esk1_0))),inference(cn,[status(thm)],[14538,theory(equality)])).
% cnf(14541,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p104(esk17_1(esk19_1(esk21_1(esk1_0))))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[14539,37,theory(equality)])).
% cnf(14544,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p104(esk17_1(esk19_1(esk21_1(esk1_0))))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[14541,140,theory(equality)])).
% cnf(14545,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p104(esk17_1(esk19_1(esk21_1(esk1_0))))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[14544,18,theory(equality)])).
% cnf(14546,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p104(esk17_1(esk19_1(esk21_1(esk1_0))))|p101(esk1_0)),inference(cn,[status(thm)],[14545,theory(equality)])).
% cnf(14547,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p104(esk17_1(esk19_1(esk21_1(esk1_0))))),inference(sr,[status(thm)],[14546,19,theory(equality)])).
% cnf(14548,plain,(p103(esk19_1(esk21_1(esk1_0)))|p102(esk21_1(esk1_0))|~epred1_1(esk19_1(esk21_1(esk1_0)))|~p102(esk19_1(esk21_1(esk1_0)))),inference(spm,[status(thm)],[54,14547,theory(equality)])).
% cnf(14550,plain,(p103(esk19_1(esk21_1(esk1_0)))|p102(esk21_1(esk1_0))|$false|~p102(esk19_1(esk21_1(esk1_0)))),inference(rw,[status(thm)],[14548,2024,theory(equality)])).
% cnf(14551,plain,(p103(esk19_1(esk21_1(esk1_0)))|p102(esk21_1(esk1_0))|~p102(esk19_1(esk21_1(esk1_0)))),inference(cn,[status(thm)],[14550,theory(equality)])).
% cnf(14553,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|~epred1_1(esk21_1(esk1_0))|~p101(esk21_1(esk1_0))),inference(spm,[status(thm)],[14551,45,theory(equality)])).
% cnf(14556,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|$false|~p101(esk21_1(esk1_0))),inference(rw,[status(thm)],[14553,717,theory(equality)])).
% cnf(14557,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|~p101(esk21_1(esk1_0))),inference(cn,[status(thm)],[14556,theory(equality)])).
% cnf(14559,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[14557,37,theory(equality)])).
% cnf(14562,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[14559,140,theory(equality)])).
% cnf(14563,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[14562,18,theory(equality)])).
% cnf(14564,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))|p101(esk1_0)),inference(cn,[status(thm)],[14563,theory(equality)])).
% cnf(14565,plain,(p102(esk21_1(esk1_0))|p103(esk19_1(esk21_1(esk1_0)))),inference(sr,[status(thm)],[14564,19,theory(equality)])).
% cnf(14566,plain,(p102(esk21_1(esk1_0))|~epred1_1(esk21_1(esk1_0))|~p101(esk21_1(esk1_0))),inference(spm,[status(thm)],[46,14565,theory(equality)])).
% cnf(14570,plain,(p102(esk21_1(esk1_0))|$false|~p101(esk21_1(esk1_0))),inference(rw,[status(thm)],[14566,717,theory(equality)])).
% cnf(14571,plain,(p102(esk21_1(esk1_0))|~p101(esk21_1(esk1_0))),inference(cn,[status(thm)],[14570,theory(equality)])).
% cnf(14573,plain,(p102(esk21_1(esk1_0))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[14571,37,theory(equality)])).
% cnf(14576,plain,(p102(esk21_1(esk1_0))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[14573,140,theory(equality)])).
% cnf(14577,plain,(p102(esk21_1(esk1_0))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[14576,18,theory(equality)])).
% cnf(14578,plain,(p102(esk21_1(esk1_0))|p101(esk1_0)),inference(cn,[status(thm)],[14577,theory(equality)])).
% cnf(14579,plain,(p102(esk21_1(esk1_0))),inference(sr,[status(thm)],[14578,19,theory(equality)])).
% cnf(14581,plain,(p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[38,14579,theory(equality)])).
% cnf(14806,plain,(p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[14581,140,theory(equality)])).
% cnf(14807,plain,(p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[14806,18,theory(equality)])).
% cnf(14808,plain,(p101(esk1_0)),inference(cn,[status(thm)],[14807,theory(equality)])).
% cnf(14809,plain,($false),inference(sr,[status(thm)],[14808,19,theory(equality)])).
% cnf(14810,plain,($false),14809,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 3115
% # ...of these trivial : 4
% # ...subsumed : 888
% # ...remaining for further processing: 2223
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 337
% # Backward-rewritten : 224
% # Generated clauses : 6481
% # ...of the previous two non-trivial : 5932
% # Contextual simplify-reflections : 1374
% # Paramodulations : 6481
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 1543
% # Positive orientable unit clauses: 21
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 23
% # Non-unit-clauses : 1499
% # Current number of unprocessed clauses: 1402
% # ...number of literals in the above : 8778
% # Clause-clause subsumption calls (NU) : 187191
% # Rec. Clause-clause subsumption calls : 55615
% # Unit Clause-clause subsumption calls : 646
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1
% # Indexed BW rewrite successes : 1
% # Backwards rewriting index: 1496 leaves, 1.09+/-0.305 terms/leaf
% # Paramod-from index: 123 leaves, 1.13+/-0.336 terms/leaf
% # Paramod-into index: 520 leaves, 1.04+/-0.232 terms/leaf
% # -------------------------------------------------
% # User time : 0.758 s
% # System time : 0.019 s
% # Total time : 0.777 s
% # Maximum resident set size: 0 pages
% PrfWatch: 1.05 CPU 1.15 WC
% FINAL PrfWatch: 1.05 CPU 1.15 WC
% SZS output end Solution for /tmp/SystemOnTPTP6722/LCL674+1.010.tptp
%
%------------------------------------------------------------------------------