%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LCL674+1.005 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art07.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:24:58 EST 2010
% Result : Theorem 0.92s
% Output : Solution 0.92s
% 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/SystemOnTPTP26910/LCL674+1.005.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP26910/LCL674+1.005.tptp
% SZS output start Solution for /tmp/SystemOnTPTP26910/LCL674+1.005.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 27006
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.014 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))|p3(X2)))|~(((![X2]:(~(r1(X1,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))|~(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))))&(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))|p3(X2)))|~(((![X2]:(~(r1(X1,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))|~(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))))&(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))|p3(X2)))|~(((![X2]:(~(r1(X1,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))|~(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))))&(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))|~(((~(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))|~(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))))&(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))|p3(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))|p3(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))|p3(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))|p3(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))|p3(X4))),inference(shift_quantors,[status(thm)],[15])).
% cnf(17,negated_conjecture,(p3(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)&((~(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))|~(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))))&(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)&((~(p6(X4))&~(p106(X4)))&p105(X4)))&?[X5]:(r1(X3,X5)&((p6(X5)&~(p106(X5)))&p105(X5))))|(p105(X3)|~(p104(X3))))&((?[X6]:(r1(X3,X6)&((~(p5(X6))&~(p105(X6)))&p104(X6)))&?[X7]:(r1(X3,X7)&((p5(X7)&~(p105(X7)))&p104(X7))))|(p104(X3)|~(p103(X3)))))&((?[X8]:(r1(X3,X8)&((~(p4(X8))&~(p104(X8)))&p103(X8)))&?[X9]:(r1(X3,X9)&((p4(X9)&~(p104(X9)))&p103(X9))))|(p103(X3)|~(p102(X3)))))&((?[X10]:(r1(X3,X10)&((~(p3(X10))&~(p103(X10)))&p102(X10)))&?[X11]:(r1(X3,X11)&((p3(X11)&~(p103(X11)))&p102(X11))))|(p102(X3)|~(p101(X3)))))&((?[X12]:(r1(X3,X12)&((~(p2(X12))&~(p102(X12)))&p101(X12)))&?[X13]:(r1(X3,X13)&((p2(X13)&~(p102(X13)))&p101(X13))))|(p101(X3)|~(p100(X3)))))&(((![X14]:((~(r1(X3,X14))|~(p6(X14)))|~(p105(X14)))|p6(X3))&(![X15]:((~(r1(X3,X15))|p6(X15))|~(p105(X15)))|~(p6(X3))))|~(p105(X3))))&(((![X16]:((~(r1(X3,X16))|~(p5(X16)))|~(p104(X16)))|p5(X3))&(![X17]:((~(r1(X3,X17))|p5(X17))|~(p104(X17)))|~(p5(X3))))|~(p104(X3))))&(((![X18]:((~(r1(X3,X18))|~(p4(X18)))|~(p103(X18)))|p4(X3))&(![X19]:((~(r1(X3,X19))|p4(X19))|~(p103(X19)))|~(p4(X3))))|~(p103(X3))))&(((![X20]:((~(r1(X3,X20))|~(p3(X20)))|~(p102(X20)))|p3(X3))&(![X21]:((~(r1(X3,X21))|p3(X21))|~(p102(X21)))|~(p3(X3))))|~(p102(X3))))&(((![X22]:((~(r1(X3,X22))|~(p2(X22)))|~(p101(X22)))|p2(X3))&(![X23]:((~(r1(X3,X23))|p2(X23))|~(p101(X23)))|~(p2(X3))))|~(p101(X3))))&(((![X24]:((~(r1(X3,X24))|~(p1(X24)))|~(p100(X24)))|p1(X3))&(![X25]:((~(r1(X3,X25))|p1(X25))|~(p100(X25)))|~(p1(X3))))|~(p100(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))&((~(p6(esk2_1(X3)))&~(p106(esk2_1(X3))))&p105(esk2_1(X3))))&(r1(X3,esk3_1(X3))&((p6(esk3_1(X3))&~(p106(esk3_1(X3))))&p105(esk3_1(X3)))))|(p105(X3)|~(p104(X3))))&(((r1(X3,esk4_1(X3))&((~(p5(esk4_1(X3)))&~(p105(esk4_1(X3))))&p104(esk4_1(X3))))&(r1(X3,esk5_1(X3))&((p5(esk5_1(X3))&~(p105(esk5_1(X3))))&p104(esk5_1(X3)))))|(p104(X3)|~(p103(X3)))))&(((r1(X3,esk6_1(X3))&((~(p4(esk6_1(X3)))&~(p104(esk6_1(X3))))&p103(esk6_1(X3))))&(r1(X3,esk7_1(X3))&((p4(esk7_1(X3))&~(p104(esk7_1(X3))))&p103(esk7_1(X3)))))|(p103(X3)|~(p102(X3)))))&(((r1(X3,esk8_1(X3))&((~(p3(esk8_1(X3)))&~(p103(esk8_1(X3))))&p102(esk8_1(X3))))&(r1(X3,esk9_1(X3))&((p3(esk9_1(X3))&~(p103(esk9_1(X3))))&p102(esk9_1(X3)))))|(p102(X3)|~(p101(X3)))))&(((r1(X3,esk10_1(X3))&((~(p2(esk10_1(X3)))&~(p102(esk10_1(X3))))&p101(esk10_1(X3))))&(r1(X3,esk11_1(X3))&((p2(esk11_1(X3))&~(p102(esk11_1(X3))))&p101(esk11_1(X3)))))|(p101(X3)|~(p100(X3)))))&(((![X14]:((~(r1(X3,X14))|~(p6(X14)))|~(p105(X14)))|p6(X3))&(![X15]:((~(r1(X3,X15))|p6(X15))|~(p105(X15)))|~(p6(X3))))|~(p105(X3))))&(((![X16]:((~(r1(X3,X16))|~(p5(X16)))|~(p104(X16)))|p5(X3))&(![X17]:((~(r1(X3,X17))|p5(X17))|~(p104(X17)))|~(p5(X3))))|~(p104(X3))))&(((![X18]:((~(r1(X3,X18))|~(p4(X18)))|~(p103(X18)))|p4(X3))&(![X19]:((~(r1(X3,X19))|p4(X19))|~(p103(X19)))|~(p4(X3))))|~(p103(X3))))&(((![X20]:((~(r1(X3,X20))|~(p3(X20)))|~(p102(X20)))|p3(X3))&(![X21]:((~(r1(X3,X21))|p3(X21))|~(p102(X21)))|~(p3(X3))))|~(p102(X3))))&(((![X22]:((~(r1(X3,X22))|~(p2(X22)))|~(p101(X22)))|p2(X3))&(![X23]:((~(r1(X3,X23))|p2(X23))|~(p101(X23)))|~(p2(X3))))|~(p101(X3))))&(((![X24]:((~(r1(X3,X24))|~(p1(X24)))|~(p100(X24)))|p1(X3))&(![X25]:((~(r1(X3,X25))|p1(X25))|~(p100(X25)))|~(p1(X3))))|~(p100(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]:![X14]:![X15]:![X16]:![X17]:![X18]:![X19]:![X20]:![X21]:![X22]:![X23]:![X24]:![X25]:(((((((((((((~(r1(X3,X25))|p1(X25))|~(p100(X25)))|~(p1(X3)))&(((~(r1(X3,X24))|~(p1(X24)))|~(p100(X24)))|p1(X3)))|~(p100(X3)))&((((((~(r1(X3,X23))|p2(X23))|~(p101(X23)))|~(p2(X3)))&(((~(r1(X3,X22))|~(p2(X22)))|~(p101(X22)))|p2(X3)))|~(p101(X3)))&((((((~(r1(X3,X21))|p3(X21))|~(p102(X21)))|~(p3(X3)))&(((~(r1(X3,X20))|~(p3(X20)))|~(p102(X20)))|p3(X3)))|~(p102(X3)))&((((((~(r1(X3,X19))|p4(X19))|~(p103(X19)))|~(p4(X3)))&(((~(r1(X3,X18))|~(p4(X18)))|~(p103(X18)))|p4(X3)))|~(p103(X3)))&((((((~(r1(X3,X17))|p5(X17))|~(p104(X17)))|~(p5(X3)))&(((~(r1(X3,X16))|~(p5(X16)))|~(p104(X16)))|p5(X3)))|~(p104(X3)))&((((((~(r1(X3,X15))|p6(X15))|~(p105(X15)))|~(p6(X3)))&(((~(r1(X3,X14))|~(p6(X14)))|~(p105(X14)))|p6(X3)))|~(p105(X3)))&(((((((r1(X3,esk2_1(X3))&((~(p6(esk2_1(X3)))&~(p106(esk2_1(X3))))&p105(esk2_1(X3))))&(r1(X3,esk3_1(X3))&((p6(esk3_1(X3))&~(p106(esk3_1(X3))))&p105(esk3_1(X3)))))|(p105(X3)|~(p104(X3))))&(((r1(X3,esk4_1(X3))&((~(p5(esk4_1(X3)))&~(p105(esk4_1(X3))))&p104(esk4_1(X3))))&(r1(X3,esk5_1(X3))&((p5(esk5_1(X3))&~(p105(esk5_1(X3))))&p104(esk5_1(X3)))))|(p104(X3)|~(p103(X3)))))&(((r1(X3,esk6_1(X3))&((~(p4(esk6_1(X3)))&~(p104(esk6_1(X3))))&p103(esk6_1(X3))))&(r1(X3,esk7_1(X3))&((p4(esk7_1(X3))&~(p104(esk7_1(X3))))&p103(esk7_1(X3)))))|(p103(X3)|~(p102(X3)))))&(((r1(X3,esk8_1(X3))&((~(p3(esk8_1(X3)))&~(p103(esk8_1(X3))))&p102(esk8_1(X3))))&(r1(X3,esk9_1(X3))&((p3(esk9_1(X3))&~(p103(esk9_1(X3))))&p102(esk9_1(X3)))))|(p102(X3)|~(p101(X3)))))&(((r1(X3,esk10_1(X3))&((~(p2(esk10_1(X3)))&~(p102(esk10_1(X3))))&p101(esk10_1(X3))))&(r1(X3,esk11_1(X3))&((p2(esk11_1(X3))&~(p102(esk11_1(X3))))&p101(esk11_1(X3)))))|(p101(X3)|~(p100(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]:![X14]:![X15]:![X16]:![X17]:![X18]:![X19]:![X20]:![X21]:![X22]:![X23]:![X24]:![X25]:(((((((((((((~(r1(X3,X25))|p1(X25))|~(p100(X25)))|~(p1(X3)))|~(p100(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X24))|~(p1(X24)))|~(p100(X24)))|p1(X3))|~(p100(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X23))|p2(X23))|~(p101(X23)))|~(p2(X3)))|~(p101(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X22))|~(p2(X22)))|~(p101(X22)))|p2(X3))|~(p101(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X21))|p3(X21))|~(p102(X21)))|~(p3(X3)))|~(p102(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X20))|~(p3(X20)))|~(p102(X20)))|p3(X3))|~(p102(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X19))|p4(X19))|~(p103(X19)))|~(p4(X3)))|~(p103(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X18))|~(p4(X18)))|~(p103(X18)))|p4(X3))|~(p103(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X17))|p5(X17))|~(p104(X17)))|~(p5(X3)))|~(p104(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X16))|~(p5(X16)))|~(p104(X16)))|p5(X3))|~(p104(X3)))|~(epred1_1(X3))))&(((((((~(r1(X3,X15))|p6(X15))|~(p105(X15)))|~(p6(X3)))|~(p105(X3)))|~(epred1_1(X3)))&(((((~(r1(X3,X14))|~(p6(X14)))|~(p105(X14)))|p6(X3))|~(p105(X3)))|~(epred1_1(X3))))&((((((((r1(X3,esk2_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))&((((~(p6(esk2_1(X3)))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))&((~(p106(esk2_1(X3)))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3))))&((p105(esk2_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk3_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))&((((p6(esk3_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3)))&((~(p106(esk3_1(X3)))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3))))&((p105(esk3_1(X3))|(p105(X3)|~(p104(X3))))|~(epred1_1(X3))))))&((((r1(X3,esk4_1(X3))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3)))&((((~(p5(esk4_1(X3)))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3)))&((~(p105(esk4_1(X3)))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3))))&((p104(esk4_1(X3))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk5_1(X3))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3)))&((((p5(esk5_1(X3))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3)))&((~(p105(esk5_1(X3)))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3))))&((p104(esk5_1(X3))|(p104(X3)|~(p103(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk6_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))&((((~(p4(esk6_1(X3)))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))&((~(p104(esk6_1(X3)))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3))))&((p103(esk6_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk7_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))&((((p4(esk7_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))&((~(p104(esk7_1(X3)))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3))))&((p103(esk7_1(X3))|(p103(X3)|~(p102(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk8_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))&((((~(p3(esk8_1(X3)))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))&((~(p103(esk8_1(X3)))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3))))&((p102(esk8_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk9_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))&((((p3(esk9_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))&((~(p103(esk9_1(X3)))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3))))&((p102(esk9_1(X3))|(p102(X3)|~(p101(X3))))|~(epred1_1(X3)))))))&((((r1(X3,esk10_1(X3))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3)))&((((~(p2(esk10_1(X3)))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3)))&((~(p102(esk10_1(X3)))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3))))&((p101(esk10_1(X3))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3)))))&(((r1(X3,esk11_1(X3))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3)))&((((p2(esk11_1(X3))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3)))&((~(p102(esk11_1(X3)))|(p101(X3)|~(p100(X3))))|~(epred1_1(X3))))&((p101(esk11_1(X3))|(p101(X3)|~(p100(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(32,plain,(p101(X1)|p101(esk11_1(X1))|~epred1_1(X1)|~p100(X1)),inference(split_conjunct,[status(thm)],[25])).
% cnf(33,plain,(p101(X1)|~epred1_1(X1)|~p100(X1)|~p102(esk11_1(X1))),inference(split_conjunct,[status(thm)],[25])).
% cnf(35,plain,(p101(X1)|r1(X1,esk11_1(X1))|~epred1_1(X1)|~p100(X1)),inference(split_conjunct,[status(thm)],[25])).
% cnf(46,plain,(p102(X1)|~epred1_1(X1)|~p101(X1)|~p3(esk8_1(X1))),inference(split_conjunct,[status(thm)],[25])).
% cnf(47,plain,(p102(X1)|r1(X1,esk8_1(X1))|~epred1_1(X1)|~p101(X1)),inference(split_conjunct,[status(thm)],[25])).
% cnf(85,negated_conjecture,(epred1_1(esk1_0)),inference(spm,[status(thm)],[20,9,theory(equality)])).
% cnf(105,negated_conjecture,(epred1_1(esk11_1(esk1_0))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[20,35,theory(equality)])).
% cnf(110,negated_conjecture,(epred1_1(esk11_1(esk1_0))|p101(esk1_0)|~epred1_1(esk1_0)|$false),inference(rw,[status(thm)],[105,18,theory(equality)])).
% cnf(111,negated_conjecture,(epred1_1(esk11_1(esk1_0))|p101(esk1_0)|~epred1_1(esk1_0)),inference(cn,[status(thm)],[110,theory(equality)])).
% cnf(112,negated_conjecture,(epred1_1(esk11_1(esk1_0))|~epred1_1(esk1_0)),inference(sr,[status(thm)],[111,19,theory(equality)])).
% cnf(120,plain,(r1(X1,esk8_1(X2))|p102(X2)|~r1(X1,X2)|~epred1_1(X2)|~p101(X2)),inference(spm,[status(thm)],[12,47,theory(equality)])).
% cnf(295,negated_conjecture,(epred1_1(esk11_1(esk1_0))|$false),inference(rw,[status(thm)],[112,85,theory(equality)])).
% cnf(296,negated_conjecture,(epred1_1(esk11_1(esk1_0))),inference(cn,[status(thm)],[295,theory(equality)])).
% cnf(581,negated_conjecture,(p3(esk8_1(X1))|p102(X1)|~epred1_1(X1)|~p101(X1)|~r1(esk1_0,X1)),inference(spm,[status(thm)],[17,120,theory(equality)])).
% cnf(698,negated_conjecture,(p102(X1)|p3(esk8_1(X1))|~p101(X1)|~r1(esk1_0,X1)),inference(csr,[status(thm)],[581,20])).
% cnf(699,plain,(p102(esk11_1(esk1_0))|p3(esk8_1(esk11_1(esk1_0)))|p101(esk1_0)|~p101(esk11_1(esk1_0))|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[698,35,theory(equality)])).
% cnf(716,plain,(p102(esk11_1(esk1_0))|p3(esk8_1(esk11_1(esk1_0)))|p101(esk1_0)|~p101(esk11_1(esk1_0))|$false|~p100(esk1_0)),inference(rw,[status(thm)],[699,85,theory(equality)])).
% cnf(717,plain,(p102(esk11_1(esk1_0))|p3(esk8_1(esk11_1(esk1_0)))|p101(esk1_0)|~p101(esk11_1(esk1_0))|$false|$false),inference(rw,[status(thm)],[716,18,theory(equality)])).
% cnf(718,plain,(p102(esk11_1(esk1_0))|p3(esk8_1(esk11_1(esk1_0)))|p101(esk1_0)|~p101(esk11_1(esk1_0))),inference(cn,[status(thm)],[717,theory(equality)])).
% cnf(719,plain,(p102(esk11_1(esk1_0))|p3(esk8_1(esk11_1(esk1_0)))|~p101(esk11_1(esk1_0))),inference(sr,[status(thm)],[718,19,theory(equality)])).
% cnf(749,plain,(p102(esk11_1(esk1_0))|~epred1_1(esk11_1(esk1_0))|~p101(esk11_1(esk1_0))),inference(spm,[status(thm)],[46,719,theory(equality)])).
% cnf(750,plain,(p102(esk11_1(esk1_0))|$false|~p101(esk11_1(esk1_0))),inference(rw,[status(thm)],[749,296,theory(equality)])).
% cnf(751,plain,(p102(esk11_1(esk1_0))|~p101(esk11_1(esk1_0))),inference(cn,[status(thm)],[750,theory(equality)])).
% cnf(753,plain,(p102(esk11_1(esk1_0))|p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[751,32,theory(equality)])).
% cnf(756,plain,(p102(esk11_1(esk1_0))|p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[753,85,theory(equality)])).
% cnf(757,plain,(p102(esk11_1(esk1_0))|p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[756,18,theory(equality)])).
% cnf(758,plain,(p102(esk11_1(esk1_0))|p101(esk1_0)),inference(cn,[status(thm)],[757,theory(equality)])).
% cnf(759,plain,(p102(esk11_1(esk1_0))),inference(sr,[status(thm)],[758,19,theory(equality)])).
% cnf(781,plain,(p101(esk1_0)|~epred1_1(esk1_0)|~p100(esk1_0)),inference(spm,[status(thm)],[33,759,theory(equality)])).
% cnf(786,plain,(p101(esk1_0)|$false|~p100(esk1_0)),inference(rw,[status(thm)],[781,85,theory(equality)])).
% cnf(787,plain,(p101(esk1_0)|$false|$false),inference(rw,[status(thm)],[786,18,theory(equality)])).
% cnf(788,plain,(p101(esk1_0)),inference(cn,[status(thm)],[787,theory(equality)])).
% cnf(789,plain,($false),inference(sr,[status(thm)],[788,19,theory(equality)])).
% cnf(790,plain,($false),789,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 181
% # ...of these trivial : 0
% # ...subsumed : 51
% # ...remaining for further processing: 130
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 1
% # Backward-rewritten : 4
% # Generated clauses : 404
% # ...of the previous two non-trivial : 367
% # Contextual simplify-reflections : 5
% # Paramodulations : 404
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 125
% # Positive orientable unit clauses: 11
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 5
% # Non-unit-clauses : 109
% # Current number of unprocessed clauses: 249
% # ...number of literals in the above : 1828
% # Clause-clause subsumption calls (NU) : 165
% # Rec. Clause-clause subsumption calls : 119
% # Unit Clause-clause subsumption calls : 72
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 2
% # Indexed BW rewrite successes : 2
% # Backwards rewriting index: 135 leaves, 1.18+/-0.485 terms/leaf
% # Paramod-from index: 52 leaves, 1.13+/-0.341 terms/leaf
% # Paramod-into index: 112 leaves, 1.09+/-0.367 terms/leaf
% # -------------------------------------------------
% # User time : 0.032 s
% # System time : 0.005 s
% # Total time : 0.037 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.13 CPU 0.21 WC
% FINAL PrfWatch: 0.13 CPU 0.21 WC
% SZS output end Solution for /tmp/SystemOnTPTP26910/LCL674+1.005.tptp
%
%------------------------------------------------------------------------------