%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : ALG071+1 : TPTP v5.0.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Tue Dec 28 20:52:14 EST 2010
% Result : Theorem 25.00s
% Output : Solution 25.00s
% 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/SystemOnTPTP12111/ALG071+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP12111/ALG071+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP12111/ALG071+1.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 12243
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.95 CPU 2.03 WC
% PrfWatch: 3.95 CPU 4.03 WC
% PrfWatch: 5.93 CPU 6.04 WC
% PrfWatch: 7.93 CPU 8.05 WC
% PrfWatch: 9.92 CPU 10.05 WC
% PrfWatch: 11.92 CPU 12.06 WC
% PrfWatch: 13.90 CPU 14.07 WC
% PrfWatch: 15.90 CPU 16.07 WC
% # Preprocessing time : 0.011 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 17.90 CPU 18.08 WC
% PrfWatch: 19.89 CPU 20.09 WC
% PrfWatch: 21.89 CPU 22.09 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:(sorti1(X1)=>![X2]:(sorti1(X2)=>sorti1(op1(X1,X2)))),file('/tmp/SRASS.s.p', ax1)).
% fof(2, axiom,![X1]:(sorti2(X1)=>![X2]:(sorti2(X2)=>sorti2(op2(X1,X2)))),file('/tmp/SRASS.s.p', ax2)).
% fof(3, axiom,![X1]:(sorti1(X1)=>?[X2]:((sorti1(X2)&~(op1(X2,op1(X2,X1))=X1))&op1(X1,op1(X2,X1))=X2)),file('/tmp/SRASS.s.p', ax3)).
% fof(4, axiom,~(![X1]:(sorti2(X1)=>?[X2]:((sorti2(X2)&~(op2(X2,op2(X2,X1))=X1))&op2(X1,op2(X2,X1))=X2))),file('/tmp/SRASS.s.p', ax4)).
% fof(5, conjecture,((![X1]:(sorti1(X1)=>sorti2(h(X1)))&![X2]:(sorti2(X2)=>sorti1(j(X2))))=>~((((![X3]:(sorti1(X3)=>![X4]:(sorti1(X4)=>h(op1(X3,X4))=op2(h(X3),h(X4))))&![X5]:(sorti2(X5)=>![X6]:(sorti2(X6)=>j(op2(X5,X6))=op1(j(X5),j(X6)))))&![X7]:(sorti2(X7)=>h(j(X7))=X7))&![X8]:(sorti1(X8)=>j(h(X8))=X8)))),file('/tmp/SRASS.s.p', co1)).
% fof(6, negated_conjecture,~(((![X1]:(sorti1(X1)=>sorti2(h(X1)))&![X2]:(sorti2(X2)=>sorti1(j(X2))))=>~((((![X3]:(sorti1(X3)=>![X4]:(sorti1(X4)=>h(op1(X3,X4))=op2(h(X3),h(X4))))&![X5]:(sorti2(X5)=>![X6]:(sorti2(X6)=>j(op2(X5,X6))=op1(j(X5),j(X6)))))&![X7]:(sorti2(X7)=>h(j(X7))=X7))&![X8]:(sorti1(X8)=>j(h(X8))=X8))))),inference(assume_negation,[status(cth)],[5])).
% fof(7, plain,![X1]:(~(sorti1(X1))|![X2]:(~(sorti1(X2))|sorti1(op1(X1,X2)))),inference(fof_nnf,[status(thm)],[1])).
% fof(8, plain,![X3]:(~(sorti1(X3))|![X4]:(~(sorti1(X4))|sorti1(op1(X3,X4)))),inference(variable_rename,[status(thm)],[7])).
% fof(9, plain,![X3]:![X4]:((~(sorti1(X4))|sorti1(op1(X3,X4)))|~(sorti1(X3))),inference(shift_quantors,[status(thm)],[8])).
% cnf(10,plain,(sorti1(op1(X1,X2))|~sorti1(X1)|~sorti1(X2)),inference(split_conjunct,[status(thm)],[9])).
% fof(11, plain,![X1]:(~(sorti2(X1))|![X2]:(~(sorti2(X2))|sorti2(op2(X1,X2)))),inference(fof_nnf,[status(thm)],[2])).
% fof(12, plain,![X3]:(~(sorti2(X3))|![X4]:(~(sorti2(X4))|sorti2(op2(X3,X4)))),inference(variable_rename,[status(thm)],[11])).
% fof(13, plain,![X3]:![X4]:((~(sorti2(X4))|sorti2(op2(X3,X4)))|~(sorti2(X3))),inference(shift_quantors,[status(thm)],[12])).
% cnf(14,plain,(sorti2(op2(X1,X2))|~sorti2(X1)|~sorti2(X2)),inference(split_conjunct,[status(thm)],[13])).
% fof(15, plain,![X1]:(~(sorti1(X1))|?[X2]:((sorti1(X2)&~(op1(X2,op1(X2,X1))=X1))&op1(X1,op1(X2,X1))=X2)),inference(fof_nnf,[status(thm)],[3])).
% fof(16, plain,![X3]:(~(sorti1(X3))|?[X4]:((sorti1(X4)&~(op1(X4,op1(X4,X3))=X3))&op1(X3,op1(X4,X3))=X4)),inference(variable_rename,[status(thm)],[15])).
% fof(17, plain,![X3]:(~(sorti1(X3))|((sorti1(esk1_1(X3))&~(op1(esk1_1(X3),op1(esk1_1(X3),X3))=X3))&op1(X3,op1(esk1_1(X3),X3))=esk1_1(X3))),inference(skolemize,[status(esa)],[16])).
% fof(18, plain,![X3]:(((sorti1(esk1_1(X3))|~(sorti1(X3)))&(~(op1(esk1_1(X3),op1(esk1_1(X3),X3))=X3)|~(sorti1(X3))))&(op1(X3,op1(esk1_1(X3),X3))=esk1_1(X3)|~(sorti1(X3)))),inference(distribute,[status(thm)],[17])).
% cnf(19,plain,(op1(X1,op1(esk1_1(X1),X1))=esk1_1(X1)|~sorti1(X1)),inference(split_conjunct,[status(thm)],[18])).
% cnf(20,plain,(~sorti1(X1)|op1(esk1_1(X1),op1(esk1_1(X1),X1))!=X1),inference(split_conjunct,[status(thm)],[18])).
% cnf(21,plain,(sorti1(esk1_1(X1))|~sorti1(X1)),inference(split_conjunct,[status(thm)],[18])).
% fof(22, plain,?[X1]:(sorti2(X1)&![X2]:((~(sorti2(X2))|op2(X2,op2(X2,X1))=X1)|~(op2(X1,op2(X2,X1))=X2))),inference(fof_nnf,[status(thm)],[4])).
% fof(23, plain,?[X3]:(sorti2(X3)&![X4]:((~(sorti2(X4))|op2(X4,op2(X4,X3))=X3)|~(op2(X3,op2(X4,X3))=X4))),inference(variable_rename,[status(thm)],[22])).
% fof(24, plain,(sorti2(esk2_0)&![X4]:((~(sorti2(X4))|op2(X4,op2(X4,esk2_0))=esk2_0)|~(op2(esk2_0,op2(X4,esk2_0))=X4))),inference(skolemize,[status(esa)],[23])).
% fof(25, plain,![X4]:(((~(sorti2(X4))|op2(X4,op2(X4,esk2_0))=esk2_0)|~(op2(esk2_0,op2(X4,esk2_0))=X4))&sorti2(esk2_0)),inference(shift_quantors,[status(thm)],[24])).
% cnf(26,plain,(sorti2(esk2_0)),inference(split_conjunct,[status(thm)],[25])).
% cnf(27,plain,(op2(X1,op2(X1,esk2_0))=esk2_0|op2(esk2_0,op2(X1,esk2_0))!=X1|~sorti2(X1)),inference(split_conjunct,[status(thm)],[25])).
% fof(28, negated_conjecture,((![X1]:(~(sorti1(X1))|sorti2(h(X1)))&![X2]:(~(sorti2(X2))|sorti1(j(X2))))&(((![X3]:(~(sorti1(X3))|![X4]:(~(sorti1(X4))|h(op1(X3,X4))=op2(h(X3),h(X4))))&![X5]:(~(sorti2(X5))|![X6]:(~(sorti2(X6))|j(op2(X5,X6))=op1(j(X5),j(X6)))))&![X7]:(~(sorti2(X7))|h(j(X7))=X7))&![X8]:(~(sorti1(X8))|j(h(X8))=X8))),inference(fof_nnf,[status(thm)],[6])).
% fof(29, negated_conjecture,((![X9]:(~(sorti1(X9))|sorti2(h(X9)))&![X10]:(~(sorti2(X10))|sorti1(j(X10))))&(((![X11]:(~(sorti1(X11))|![X12]:(~(sorti1(X12))|h(op1(X11,X12))=op2(h(X11),h(X12))))&![X13]:(~(sorti2(X13))|![X14]:(~(sorti2(X14))|j(op2(X13,X14))=op1(j(X13),j(X14)))))&![X15]:(~(sorti2(X15))|h(j(X15))=X15))&![X16]:(~(sorti1(X16))|j(h(X16))=X16))),inference(variable_rename,[status(thm)],[28])).
% fof(30, negated_conjecture,![X9]:![X10]:![X11]:![X12]:![X13]:![X14]:![X15]:![X16]:(((~(sorti1(X16))|j(h(X16))=X16)&((~(sorti2(X15))|h(j(X15))=X15)&(((~(sorti2(X14))|j(op2(X13,X14))=op1(j(X13),j(X14)))|~(sorti2(X13)))&((~(sorti1(X12))|h(op1(X11,X12))=op2(h(X11),h(X12)))|~(sorti1(X11))))))&((~(sorti2(X10))|sorti1(j(X10)))&(~(sorti1(X9))|sorti2(h(X9))))),inference(shift_quantors,[status(thm)],[29])).
% cnf(31,negated_conjecture,(sorti2(h(X1))|~sorti1(X1)),inference(split_conjunct,[status(thm)],[30])).
% cnf(32,negated_conjecture,(sorti1(j(X1))|~sorti2(X1)),inference(split_conjunct,[status(thm)],[30])).
% cnf(33,negated_conjecture,(h(op1(X1,X2))=op2(h(X1),h(X2))|~sorti1(X1)|~sorti1(X2)),inference(split_conjunct,[status(thm)],[30])).
% cnf(34,negated_conjecture,(j(op2(X1,X2))=op1(j(X1),j(X2))|~sorti2(X1)|~sorti2(X2)),inference(split_conjunct,[status(thm)],[30])).
% cnf(35,negated_conjecture,(h(j(X1))=X1|~sorti2(X1)),inference(split_conjunct,[status(thm)],[30])).
% cnf(36,negated_conjecture,(j(h(X1))=X1|~sorti1(X1)),inference(split_conjunct,[status(thm)],[30])).
% cnf(41,negated_conjecture,(op1(j(X1),X2)=j(op2(X1,h(X2)))|~sorti2(h(X2))|~sorti2(X1)|~sorti1(X2)),inference(spm,[status(thm)],[34,36,theory(equality)])).
% cnf(42,negated_conjecture,(op1(X1,j(X2))=j(op2(h(X1),X2))|~sorti2(X2)|~sorti2(h(X1))|~sorti1(X1)),inference(spm,[status(thm)],[34,36,theory(equality)])).
% cnf(43,negated_conjecture,(sorti2(h(op1(X1,X2)))|~sorti2(h(X2))|~sorti2(h(X1))|~sorti1(X2)|~sorti1(X1)),inference(spm,[status(thm)],[14,33,theory(equality)])).
% cnf(44,negated_conjecture,(op2(h(X1),X2)=h(op1(X1,j(X2)))|~sorti1(j(X2))|~sorti1(X1)|~sorti2(X2)),inference(spm,[status(thm)],[33,35,theory(equality)])).
% cnf(45,negated_conjecture,(op2(X1,h(X2))=h(op1(j(X1),X2))|~sorti1(X2)|~sorti1(j(X1))|~sorti2(X1)),inference(spm,[status(thm)],[33,35,theory(equality)])).
% cnf(47,negated_conjecture,(j(op2(X1,h(X2)))=op1(j(X1),X2)|~sorti2(X1)|~sorti1(X2)),inference(csr,[status(thm)],[41,31])).
% cnf(48,negated_conjecture,(sorti1(op1(j(X1),X2))|~sorti2(op2(X1,h(X2)))|~sorti2(X1)|~sorti1(X2)),inference(spm,[status(thm)],[32,47,theory(equality)])).
% cnf(53,negated_conjecture,(j(h(op1(X1,X2)))=op1(j(h(X1)),X2)|~sorti2(h(X1))|~sorti1(X2)|~sorti1(X1)),inference(spm,[status(thm)],[47,33,theory(equality)])).
% cnf(56,negated_conjecture,(sorti1(op1(j(X1),X2))|~sorti2(X1)|~sorti1(X2)|~sorti2(h(X2))),inference(spm,[status(thm)],[48,14,theory(equality)])).
% cnf(57,negated_conjecture,(sorti1(op1(j(X1),X2))|~sorti2(X1)|~sorti1(X2)),inference(csr,[status(thm)],[56,31])).
% cnf(59,negated_conjecture,(sorti1(op1(op1(j(X1),X2),X3))|~sorti2(op2(X1,h(X2)))|~sorti1(X3)|~sorti2(X1)|~sorti1(X2)),inference(spm,[status(thm)],[57,47,theory(equality)])).
% cnf(60,negated_conjecture,(sorti1(esk1_1(j(X1)))|~sorti2(X1)|~sorti1(op1(esk1_1(j(X1)),j(X1)))|~sorti1(j(X1))),inference(spm,[status(thm)],[57,19,theory(equality)])).
% cnf(61,negated_conjecture,(sorti1(j(op2(X1,X2)))|~sorti2(X1)|~sorti1(j(X2))|~sorti2(X2)),inference(spm,[status(thm)],[57,34,theory(equality)])).
% cnf(62,negated_conjecture,(sorti1(j(op2(X1,X2)))|~sorti2(X2)|~sorti2(X1)),inference(csr,[status(thm)],[61,32])).
% cnf(63,negated_conjecture,(sorti1(j(h(op1(X1,X2))))|~sorti2(h(X1))|~sorti2(h(X2))|~sorti1(X2)|~sorti1(X1)),inference(spm,[status(thm)],[62,33,theory(equality)])).
% cnf(69,negated_conjecture,(sorti2(h(op1(X1,X2)))|~sorti2(h(X2))|~sorti1(X2)|~sorti1(X1)),inference(csr,[status(thm)],[43,31])).
% cnf(70,negated_conjecture,(sorti2(h(op1(X1,X2)))|~sorti1(X2)|~sorti1(X1)),inference(csr,[status(thm)],[69,31])).
% cnf(71,negated_conjecture,(sorti2(h(j(op2(X1,X2))))|~sorti1(j(X2))|~sorti1(j(X1))|~sorti2(X2)|~sorti2(X1)),inference(spm,[status(thm)],[70,34,theory(equality)])).
% cnf(72,negated_conjecture,(sorti2(h(esk1_1(X1)))|~sorti1(op1(esk1_1(X1),X1))|~sorti1(X1)),inference(spm,[status(thm)],[70,19,theory(equality)])).
% cnf(73,negated_conjecture,(j(op2(h(X1),X2))=op1(X1,j(X2))|~sorti2(X2)|~sorti1(X1)),inference(csr,[status(thm)],[42,31])).
% cnf(80,negated_conjecture,(sorti1(op1(X1,j(X2)))|~sorti2(h(X1))|~sorti2(X2)|~sorti1(X1)),inference(spm,[status(thm)],[62,73,theory(equality)])).
% cnf(82,negated_conjecture,(j(h(op1(X1,X2)))=op1(X1,j(h(X2)))|~sorti2(h(X2))|~sorti1(X1)|~sorti1(X2)),inference(spm,[status(thm)],[73,33,theory(equality)])).
% cnf(83,negated_conjecture,(sorti1(op1(X1,j(X2)))|~sorti2(X2)|~sorti1(X1)),inference(csr,[status(thm)],[80,31])).
% cnf(91,negated_conjecture,(sorti1(j(h(op1(X1,X2))))|~sorti2(h(X1))|~sorti1(X2)|~sorti1(X1)),inference(csr,[status(thm)],[63,31])).
% cnf(92,negated_conjecture,(sorti1(j(h(op1(X1,X2))))|~sorti1(X2)|~sorti1(X1)),inference(csr,[status(thm)],[91,31])).
% cnf(94,negated_conjecture,(sorti1(j(h(esk1_1(X1))))|~sorti1(op1(esk1_1(X1),X1))|~sorti1(X1)),inference(spm,[status(thm)],[92,19,theory(equality)])).
% cnf(96,negated_conjecture,(sorti2(h(j(op2(X1,X2))))|~sorti2(X2)|~sorti2(X1)|~sorti1(j(X2))),inference(csr,[status(thm)],[71,32])).
% cnf(97,negated_conjecture,(sorti2(h(j(op2(X1,X2))))|~sorti2(X2)|~sorti2(X1)),inference(csr,[status(thm)],[96,32])).
% cnf(98,negated_conjecture,(sorti2(h(j(h(op1(X1,X2)))))|~sorti2(h(X2))|~sorti2(h(X1))|~sorti1(X2)|~sorti1(X1)),inference(spm,[status(thm)],[97,33,theory(equality)])).
% cnf(100,negated_conjecture,(sorti2(h(op1(j(X1),X2)))|~sorti2(h(X2))|~sorti2(X1)|~sorti1(X2)),inference(spm,[status(thm)],[97,47,theory(equality)])).
% cnf(108,negated_conjecture,(sorti2(h(esk1_1(X1)))|~sorti1(X1)|~sorti1(esk1_1(X1))),inference(spm,[status(thm)],[72,10,theory(equality)])).
% cnf(109,negated_conjecture,(h(op1(X1,j(X2)))=op2(h(X1),X2)|~sorti2(X2)|~sorti1(X1)),inference(csr,[status(thm)],[44,32])).
% cnf(114,negated_conjecture,(op2(h(X1),op2(h(X2),X3))=h(op1(X1,op1(X2,j(X3))))|~sorti1(op1(X2,j(X3)))|~sorti1(X1)|~sorti2(X3)|~sorti1(X2)),inference(spm,[status(thm)],[33,109,theory(equality)])).
% cnf(117,negated_conjecture,(sorti1(j(op2(h(X1),X2)))|~sorti1(j(X2))|~sorti1(X1)|~sorti2(X2)),inference(spm,[status(thm)],[92,109,theory(equality)])).
% cnf(126,negated_conjecture,(sorti2(h(esk1_1(X1)))|~sorti1(X1)),inference(csr,[status(thm)],[108,21])).
% cnf(131,negated_conjecture,(sorti2(h(op1(j(X1),X2)))|~sorti2(X1)|~sorti1(X2)),inference(csr,[status(thm)],[100,31])).
% cnf(139,negated_conjecture,(sorti1(j(h(esk1_1(X1))))|~sorti1(X1)|~sorti1(esk1_1(X1))),inference(spm,[status(thm)],[94,10,theory(equality)])).
% cnf(140,negated_conjecture,(h(op1(j(X1),X2))=op2(X1,h(X2))|~sorti2(X1)|~sorti1(X2)),inference(csr,[status(thm)],[45,32])).
% cnf(148,negated_conjecture,(op2(X1,h(j(X2)))=op2(h(j(X1)),X2)|~sorti2(X2)|~sorti1(j(X1))|~sorti2(X1)|~sorti1(j(X2))),inference(spm,[status(thm)],[109,140,theory(equality)])).
% cnf(152,negated_conjecture,(sorti2(op2(X1,h(X2)))|~sorti2(X1)|~sorti1(X2)),inference(spm,[status(thm)],[131,140,theory(equality)])).
% cnf(162,negated_conjecture,(sorti1(j(h(esk1_1(X1))))|~sorti1(X1)),inference(csr,[status(thm)],[139,21])).
% cnf(169,negated_conjecture,(sorti1(j(op2(h(X1),X2)))|~sorti2(X2)|~sorti1(X1)),inference(csr,[status(thm)],[117,32])).
% cnf(171,negated_conjecture,(sorti1(j(op2(op2(X1,h(X2)),X3)))|~sorti2(X3)|~sorti1(op1(j(X1),X2))|~sorti2(X1)|~sorti1(X2)),inference(spm,[status(thm)],[169,140,theory(equality)])).
% cnf(221,negated_conjecture,(sorti1(esk1_1(j(X1)))|~sorti2(X1)|~sorti1(op1(esk1_1(j(X1)),j(X1)))),inference(csr,[status(thm)],[60,32])).
% cnf(278,negated_conjecture,(j(h(op1(X1,X2)))=op1(j(h(X1)),X2)|~sorti1(X2)|~sorti1(X1)),inference(csr,[status(thm)],[53,31])).
% cnf(292,negated_conjecture,(op1(j(h(X1)),X2)=op1(X1,X2)|~sorti1(op1(X1,X2))|~sorti1(X2)|~sorti1(X1)),inference(spm,[status(thm)],[36,278,theory(equality)])).
% cnf(298,negated_conjecture,(j(op2(h(X1),X2))=op1(j(h(X1)),j(X2))|~sorti1(j(X2))|~sorti1(X1)|~sorti2(X2)),inference(spm,[status(thm)],[278,109,theory(equality)])).
% cnf(313,negated_conjecture,(sorti1(op1(op1(j(X1),X2),X3))|~sorti2(X1)|~sorti1(X3)|~sorti1(X2)),inference(csr,[status(thm)],[59,152])).
% cnf(315,negated_conjecture,(sorti1(op1(op1(X1,X2),X3))|~sorti2(h(X1))|~sorti1(X3)|~sorti1(X2)|~sorti1(X1)),inference(spm,[status(thm)],[313,36,theory(equality)])).
% cnf(323,negated_conjecture,(op1(j(h(X1)),X2)=op1(X1,X2)|~sorti1(X2)|~sorti1(X1)),inference(csr,[status(thm)],[292,10])).
% cnf(347,negated_conjecture,(sorti1(op1(op1(X1,X2),X3))|~sorti1(X3)|~sorti1(X2)|~sorti1(X1)),inference(csr,[status(thm)],[315,31])).
% cnf(350,negated_conjecture,(sorti1(op1(esk1_1(X1),X2))|~sorti1(X2)|~sorti1(op1(esk1_1(X1),X1))|~sorti1(X1)),inference(spm,[status(thm)],[347,19,theory(equality)])).
% cnf(354,negated_conjecture,(j(h(op1(X1,X2)))=op1(X1,j(h(X2)))|~sorti1(X1)|~sorti1(X2)),inference(csr,[status(thm)],[82,31])).
% cnf(373,negated_conjecture,(op1(X1,j(h(X2)))=op1(j(h(X1)),X2)|~sorti1(X2)|~sorti1(X1)),inference(spm,[status(thm)],[278,354,theory(equality)])).
% cnf(379,negated_conjecture,(j(op2(h(X1),X2))=op1(X1,j(h(j(X2))))|~sorti1(X1)|~sorti1(j(X2))|~sorti2(X2)),inference(spm,[status(thm)],[354,109,theory(equality)])).
% cnf(397,negated_conjecture,(op1(X1,j(h(X2)))=op1(X1,X2)|~sorti1(X2)|~sorti1(X1)),inference(spm,[status(thm)],[323,373,theory(equality)])).
% cnf(412,negated_conjecture,(h(op1(j(X1),X2))=op2(X1,h(j(h(X2))))|~sorti2(X1)|~sorti1(j(h(X2)))|~sorti1(X2)|~sorti1(j(X1))),inference(spm,[status(thm)],[140,397,theory(equality)])).
% cnf(597,negated_conjecture,(sorti1(op1(esk1_1(X1),X2))|~sorti1(X2)|~sorti1(X1)|~sorti1(esk1_1(X1))),inference(spm,[status(thm)],[350,10,theory(equality)])).
% cnf(648,negated_conjecture,(sorti1(op1(esk1_1(X1),X2))|~sorti1(X2)|~sorti1(X1)),inference(csr,[status(thm)],[597,21])).
% cnf(649,negated_conjecture,(sorti1(esk1_1(j(X1)))|~sorti2(X1)|~sorti1(j(X1))),inference(spm,[status(thm)],[221,648,theory(equality)])).
% cnf(669,negated_conjecture,(sorti1(esk1_1(j(X1)))|~sorti2(X1)),inference(csr,[status(thm)],[649,32])).
% cnf(718,negated_conjecture,(sorti2(h(j(h(op1(X1,X2)))))|~sorti2(h(X2))|~sorti1(X2)|~sorti1(X1)),inference(csr,[status(thm)],[98,31])).
% cnf(719,negated_conjecture,(sorti2(h(j(h(op1(X1,X2)))))|~sorti1(X2)|~sorti1(X1)),inference(csr,[status(thm)],[718,31])).
% cnf(724,negated_conjecture,(sorti2(h(j(h(esk1_1(X1)))))|~sorti1(op1(esk1_1(X1),X1))|~sorti1(X1)),inference(spm,[status(thm)],[719,19,theory(equality)])).
% cnf(839,negated_conjecture,(sorti2(h(j(h(esk1_1(X1)))))|~sorti1(X1)),inference(spm,[status(thm)],[724,648,theory(equality)])).
% cnf(1040,negated_conjecture,(h(op1(X1,op1(X2,j(X3))))=op2(h(X1),op2(h(X2),X3))|~sorti2(X3)|~sorti1(X1)|~sorti1(X2)),inference(csr,[status(thm)],[114,83])).
% cnf(1094,negated_conjecture,(h(op1(X1,j(h(op1(X2,j(X3))))))=op2(h(j(h(X1))),op2(h(X2),X3))|~sorti2(X3)|~sorti1(j(h(X1)))|~sorti1(X2)|~sorti1(op1(X2,j(X3)))|~sorti1(X1)),inference(spm,[status(thm)],[1040,373,theory(equality)])).
% cnf(1095,negated_conjecture,(h(esk1_1(j(X1)))=op2(h(j(X1)),op2(h(esk1_1(j(X1))),X1))|~sorti2(X1)|~sorti1(j(X1))|~sorti1(esk1_1(j(X1)))),inference(spm,[status(thm)],[1040,19,theory(equality)])).
% cnf(1975,negated_conjecture,(op2(h(j(X1)),X2)=op2(X1,h(j(X2)))|~sorti2(X2)|~sorti2(X1)|~sorti1(j(X1))),inference(csr,[status(thm)],[148,32])).
% cnf(1976,negated_conjecture,(op2(h(j(X1)),X2)=op2(X1,h(j(X2)))|~sorti2(X1)|~sorti2(X2)),inference(csr,[status(thm)],[1975,32])).
% cnf(1977,negated_conjecture,(op2(h(j(X1)),op2(X1,h(j(esk2_0))))=esk2_0|op2(esk2_0,op2(X1,h(j(esk2_0))))!=h(j(X1))|~sorti2(h(j(X1)))|~sorti2(esk2_0)|~sorti2(X1)),inference(spm,[status(thm)],[27,1976,theory(equality)])).
% cnf(2027,negated_conjecture,(op2(h(j(X1)),op2(X1,h(j(esk2_0))))=esk2_0|op2(esk2_0,op2(X1,h(j(esk2_0))))!=h(j(X1))|~sorti2(h(j(X1)))|$false|~sorti2(X1)),inference(rw,[status(thm)],[1977,26,theory(equality)])).
% cnf(2028,negated_conjecture,(op2(h(j(X1)),op2(X1,h(j(esk2_0))))=esk2_0|op2(esk2_0,op2(X1,h(j(esk2_0))))!=h(j(X1))|~sorti2(h(j(X1)))|~sorti2(X1)),inference(cn,[status(thm)],[2027,theory(equality)])).
% cnf(2458,negated_conjecture,(sorti1(j(op2(op2(X1,h(X2)),X3)))|~sorti2(X1)|~sorti2(X3)|~sorti1(X2)),inference(csr,[status(thm)],[171,57])).
% cnf(2469,negated_conjecture,(sorti1(j(op2(h(op1(X1,X2)),X3)))|~sorti2(X3)|~sorti2(h(X1))|~sorti1(X2)|~sorti1(X1)),inference(spm,[status(thm)],[2458,33,theory(equality)])).
% cnf(10774,negated_conjecture,(op1(j(h(X1)),j(X2))=j(op2(h(X1),X2))|~sorti2(X2)|~sorti1(X1)),inference(csr,[status(thm)],[298,32])).
% cnf(17011,negated_conjecture,(op1(X1,j(h(j(X2))))=j(op2(h(X1),X2))|~sorti2(X2)|~sorti1(X1)),inference(csr,[status(thm)],[379,32])).
% cnf(17015,negated_conjecture,(op1(esk1_1(j(h(j(X1)))),j(op2(h(esk1_1(j(h(j(X1))))),X1)))!=j(h(j(X1)))|~sorti1(j(h(j(X1))))|~sorti2(X1)|~sorti1(esk1_1(j(h(j(X1)))))),inference(spm,[status(thm)],[20,17011,theory(equality)])).
% cnf(17632,negated_conjecture,(op1(esk1_1(j(h(j(X1)))),j(op2(h(esk1_1(j(h(j(X1))))),X1)))!=j(h(j(X1)))|~sorti2(X1)|~sorti1(j(h(j(X1))))),inference(csr,[status(thm)],[17015,21])).
% cnf(17644,negated_conjecture,(op1(esk1_1(j(X1)),j(op2(h(esk1_1(j(X1))),X1)))!=j(X1)|~sorti2(X1)|~sorti1(j(X1))),inference(spm,[status(thm)],[17632,35,theory(equality)])).
% cnf(17665,negated_conjecture,(op1(esk1_1(j(X1)),j(op2(h(esk1_1(j(X1))),X1)))!=j(X1)|~sorti2(X1)),inference(csr,[status(thm)],[17644,32])).
% cnf(17668,negated_conjecture,(op1(esk1_1(X1),j(op2(h(esk1_1(X1)),h(X1))))!=X1|~sorti2(h(X1))|~sorti1(X1)),inference(spm,[status(thm)],[17665,36,theory(equality)])).
% cnf(17690,negated_conjecture,(op1(esk1_1(X1),j(op2(h(esk1_1(X1)),h(X1))))!=X1|~sorti1(X1)),inference(csr,[status(thm)],[17668,31])).
% cnf(21528,negated_conjecture,(op2(X1,h(j(h(X2))))=h(op1(j(X1),X2))|~sorti2(X1)|~sorti1(j(h(X2)))|~sorti1(X2)),inference(csr,[status(thm)],[412,32])).
% cnf(21568,negated_conjecture,(op1(esk1_1(j(h(X1))),j(h(op1(j(h(esk1_1(j(h(X1))))),X1))))!=j(h(X1))|~sorti1(j(h(X1)))|~sorti2(h(esk1_1(j(h(X1)))))|~sorti1(X1)),inference(spm,[status(thm)],[17690,21528,theory(equality)])).
% cnf(23050,negated_conjecture,(op1(esk1_1(j(h(X1))),j(h(op1(j(h(esk1_1(j(h(X1))))),X1))))!=j(h(X1))|~sorti1(j(h(X1)))|~sorti1(X1)),inference(csr,[status(thm)],[21568,126])).
% cnf(23078,negated_conjecture,(op1(esk1_1(X1),j(h(op1(j(h(esk1_1(X1))),X1))))!=X1|~sorti1(X1)),inference(spm,[status(thm)],[23050,36,theory(equality)])).
% cnf(23158,negated_conjecture,(op1(esk1_1(j(X1)),j(h(j(op2(h(esk1_1(j(X1))),X1)))))!=j(X1)|~sorti1(j(X1))|~sorti2(X1)|~sorti1(esk1_1(j(X1)))),inference(spm,[status(thm)],[23078,10774,theory(equality)])).
% cnf(27184,negated_conjecture,(op1(esk1_1(j(X1)),j(h(j(op2(h(esk1_1(j(X1))),X1)))))!=j(X1)|~sorti2(X1)|~sorti1(j(X1))),inference(csr,[status(thm)],[23158,21])).
% cnf(27185,negated_conjecture,(op1(esk1_1(j(X1)),j(h(j(op2(h(esk1_1(j(X1))),X1)))))!=j(X1)|~sorti2(X1)),inference(csr,[status(thm)],[27184,32])).
% cnf(27199,negated_conjecture,(op1(esk1_1(j(h(X1))),j(h(j(h(op1(esk1_1(j(h(X1))),X1))))))!=j(h(X1))|~sorti2(h(X1))|~sorti1(X1)|~sorti1(esk1_1(j(h(X1))))),inference(spm,[status(thm)],[27185,33,theory(equality)])).
% cnf(33871,negated_conjecture,(op1(esk1_1(j(h(X1))),j(h(j(h(op1(esk1_1(j(h(X1))),X1))))))!=j(h(X1))|~sorti2(h(X1))|~sorti1(X1)),inference(csr,[status(thm)],[27199,669])).
% cnf(33872,negated_conjecture,(op1(esk1_1(j(h(X1))),j(h(j(h(op1(esk1_1(j(h(X1))),X1))))))!=j(h(X1))|~sorti1(X1)),inference(csr,[status(thm)],[33871,31])).
% cnf(33964,negated_conjecture,(j(op2(h(esk1_1(j(h(X1)))),h(op1(esk1_1(j(h(X1))),X1))))!=j(h(X1))|~sorti1(X1)|~sorti2(h(op1(esk1_1(j(h(X1))),X1)))|~sorti1(esk1_1(j(h(X1))))),inference(spm,[status(thm)],[33872,17011,theory(equality)])).
% cnf(56067,negated_conjecture,(j(op2(h(esk1_1(j(h(X1)))),h(op1(esk1_1(j(h(X1))),X1))))!=j(h(X1))|~sorti1(esk1_1(j(h(X1))))|~sorti1(X1)),inference(csr,[status(thm)],[33964,70])).
% cnf(56102,negated_conjecture,(j(op2(h(esk1_1(X1)),h(op1(esk1_1(X1),X1))))!=X1|~sorti1(esk1_1(X1))|~sorti1(X1)),inference(spm,[status(thm)],[56067,36,theory(equality)])).
% cnf(56161,negated_conjecture,(j(op2(h(esk1_1(X1)),h(op1(esk1_1(X1),X1))))!=X1|~sorti1(X1)),inference(csr,[status(thm)],[56102,21])).
% cnf(56170,negated_conjecture,(j(op2(h(esk1_1(j(X1))),op2(h(esk1_1(j(X1))),X1)))!=j(X1)|~sorti1(j(X1))|~sorti2(X1)|~sorti1(esk1_1(j(X1)))),inference(spm,[status(thm)],[56161,109,theory(equality)])).
% cnf(56287,negated_conjecture,(j(op2(h(esk1_1(j(X1))),op2(h(esk1_1(j(X1))),X1)))!=j(X1)|~sorti2(X1)|~sorti1(j(X1))),inference(csr,[status(thm)],[56170,21])).
% cnf(56288,negated_conjecture,(j(op2(h(esk1_1(j(X1))),op2(h(esk1_1(j(X1))),X1)))!=j(X1)|~sorti2(X1)),inference(csr,[status(thm)],[56287,32])).
% cnf(56294,negated_conjecture,(j(op2(h(esk1_1(X1)),op2(h(esk1_1(X1)),h(X1))))!=X1|~sorti2(h(X1))|~sorti1(X1)),inference(spm,[status(thm)],[56288,36,theory(equality)])).
% cnf(56385,negated_conjecture,(j(op2(h(esk1_1(X1)),op2(h(esk1_1(X1)),h(X1))))!=X1|~sorti1(X1)),inference(csr,[status(thm)],[56294,31])).
% cnf(56416,negated_conjecture,(j(op2(h(esk1_1(j(h(X1)))),h(op1(j(h(esk1_1(j(h(X1))))),X1))))!=j(h(X1))|~sorti1(j(h(X1)))|~sorti2(h(esk1_1(j(h(X1)))))|~sorti1(X1)),inference(spm,[status(thm)],[56385,21528,theory(equality)])).
% cnf(56829,negated_conjecture,(sorti1(j(op2(h(op1(X1,X2)),X3)))|~sorti2(X3)|~sorti1(X2)|~sorti1(X1)),inference(csr,[status(thm)],[2469,31])).
% cnf(56882,negated_conjecture,(sorti1(j(op2(h(esk1_1(X1)),X2)))|~sorti2(X2)|~sorti1(op1(esk1_1(X1),X1))|~sorti1(X1)),inference(spm,[status(thm)],[56829,19,theory(equality)])).
% cnf(65208,negated_conjecture,(j(op2(h(esk1_1(j(h(X1)))),h(op1(j(h(esk1_1(j(h(X1))))),X1))))!=j(h(X1))|~sorti1(j(h(X1)))|~sorti1(X1)),inference(csr,[status(thm)],[56416,126])).
% cnf(65243,negated_conjecture,(j(op2(h(esk1_1(X1)),h(op1(j(h(esk1_1(X1))),X1))))!=X1|~sorti1(X1)),inference(spm,[status(thm)],[65208,36,theory(equality)])).
% cnf(65343,negated_conjecture,(j(op2(h(esk1_1(j(X1))),h(j(op2(h(esk1_1(j(X1))),X1)))))!=j(X1)|~sorti1(j(X1))|~sorti2(X1)|~sorti1(esk1_1(j(X1)))),inference(spm,[status(thm)],[65243,10774,theory(equality)])).
% cnf(65806,negated_conjecture,(j(op2(h(esk1_1(j(X1))),h(j(op2(h(esk1_1(j(X1))),X1)))))!=j(X1)|~sorti2(X1)|~sorti1(j(X1))),inference(csr,[status(thm)],[65343,21])).
% cnf(65807,negated_conjecture,(j(op2(h(esk1_1(j(X1))),h(j(op2(h(esk1_1(j(X1))),X1)))))!=j(X1)|~sorti2(X1)),inference(csr,[status(thm)],[65806,32])).
% cnf(65813,negated_conjecture,(j(op2(h(esk1_1(X1)),h(j(op2(h(esk1_1(X1)),h(X1))))))!=X1|~sorti2(h(X1))|~sorti1(X1)),inference(spm,[status(thm)],[65807,36,theory(equality)])).
% cnf(65852,negated_conjecture,(j(op2(h(esk1_1(X1)),h(j(op2(h(esk1_1(X1)),h(X1))))))!=X1|~sorti1(X1)),inference(csr,[status(thm)],[65813,31])).
% cnf(65892,negated_conjecture,(j(h(op1(esk1_1(X1),j(op2(h(esk1_1(X1)),h(X1))))))!=X1|~sorti1(X1)|~sorti1(j(op2(h(esk1_1(X1)),h(X1))))|~sorti1(esk1_1(X1))),inference(spm,[status(thm)],[65852,33,theory(equality)])).
% cnf(70869,negated_conjecture,(sorti1(j(op2(h(esk1_1(X1)),X2)))|~sorti2(X2)|~sorti1(X1)),inference(spm,[status(thm)],[56882,648,theory(equality)])).
% cnf(72032,negated_conjecture,(j(h(op1(esk1_1(X1),j(op2(h(esk1_1(X1)),h(X1))))))!=X1|~sorti1(j(op2(h(esk1_1(X1)),h(X1))))|~sorti1(X1)),inference(csr,[status(thm)],[65892,21])).
% cnf(72035,negated_conjecture,(j(h(op1(esk1_1(j(X1)),j(op2(h(esk1_1(j(X1))),X1)))))!=j(X1)|~sorti1(j(op2(h(esk1_1(j(X1))),X1)))|~sorti1(j(X1))|~sorti2(X1)),inference(spm,[status(thm)],[72032,35,theory(equality)])).
% cnf(97194,negated_conjecture,(j(h(op1(esk1_1(j(X1)),j(op2(h(esk1_1(j(X1))),X1)))))!=j(X1)|~sorti2(X1)|~sorti1(j(op2(h(esk1_1(j(X1))),X1)))),inference(csr,[status(thm)],[72035,32])).
% cnf(97200,negated_conjecture,(j(h(op1(esk1_1(X1),j(op2(h(esk1_1(X1)),h(X1))))))!=X1|~sorti2(h(X1))|~sorti1(j(op2(h(esk1_1(X1)),h(X1))))|~sorti1(X1)),inference(spm,[status(thm)],[97194,36,theory(equality)])).
% cnf(97603,negated_conjecture,(j(h(op1(esk1_1(X1),j(op2(h(esk1_1(X1)),h(X1))))))!=X1|~sorti2(h(X1))|~sorti1(X1)),inference(csr,[status(thm)],[97200,70869])).
% cnf(97604,negated_conjecture,(j(h(op1(esk1_1(X1),j(op2(h(esk1_1(X1)),h(X1))))))!=X1|~sorti1(X1)),inference(csr,[status(thm)],[97603,31])).
% cnf(97643,negated_conjecture,(j(h(op1(esk1_1(X1),j(h(op1(esk1_1(X1),X1))))))!=X1|~sorti1(X1)|~sorti1(esk1_1(X1))),inference(spm,[status(thm)],[97604,33,theory(equality)])).
% cnf(97653,negated_conjecture,(j(h(op1(esk1_1(X1),j(h(op1(esk1_1(X1),X1))))))!=X1|~sorti1(X1)),inference(csr,[status(thm)],[97643,21])).
% cnf(114902,negated_conjecture,(h(op1(X1,j(h(op1(X2,j(X3))))))=op2(h(j(h(X1))),op2(h(X2),X3))|~sorti2(X3)|~sorti1(j(h(X1)))|~sorti1(X1)|~sorti1(X2)),inference(csr,[status(thm)],[1094,83])).
% cnf(115479,negated_conjecture,(j(op2(h(j(h(esk1_1(j(X1))))),op2(h(esk1_1(j(X1))),X1)))!=j(X1)|~sorti1(j(X1))|~sorti2(X1)|~sorti1(j(h(esk1_1(j(X1)))))|~sorti1(esk1_1(j(X1)))),inference(spm,[status(thm)],[97653,114902,theory(equality)])).
% cnf(115849,negated_conjecture,(op2(h(j(X1)),op2(h(esk1_1(j(X1))),X1))=h(esk1_1(j(X1)))|~sorti2(X1)|~sorti1(j(X1))),inference(csr,[status(thm)],[1095,21])).
% cnf(115850,negated_conjecture,(op2(h(j(X1)),op2(h(esk1_1(j(X1))),X1))=h(esk1_1(j(X1)))|~sorti2(X1)),inference(csr,[status(thm)],[115849,32])).
% cnf(116171,negated_conjecture,(op2(X1,op2(h(esk1_1(j(X1))),X1))=h(esk1_1(j(X1)))|~sorti2(X1)),inference(spm,[status(thm)],[115850,35,theory(equality)])).
% cnf(247873,negated_conjecture,(j(op2(h(j(h(esk1_1(j(X1))))),op2(h(esk1_1(j(X1))),X1)))!=j(X1)|~sorti2(X1)|~sorti1(j(h(esk1_1(j(X1)))))|~sorti1(j(X1))),inference(csr,[status(thm)],[115479,21])).
% cnf(247874,negated_conjecture,(j(op2(h(j(h(esk1_1(j(X1))))),op2(h(esk1_1(j(X1))),X1)))!=j(X1)|~sorti2(X1)|~sorti1(j(X1))),inference(csr,[status(thm)],[247873,162])).
% cnf(247875,negated_conjecture,(j(op2(h(j(h(esk1_1(j(X1))))),op2(h(esk1_1(j(X1))),X1)))!=j(X1)|~sorti2(X1)),inference(csr,[status(thm)],[247874,32])).
% cnf(247881,negated_conjecture,(j(op2(h(j(h(esk1_1(X1)))),op2(h(esk1_1(X1)),h(X1))))!=X1|~sorti2(h(X1))|~sorti1(X1)),inference(spm,[status(thm)],[247875,36,theory(equality)])).
% cnf(248019,negated_conjecture,(j(op2(h(j(h(esk1_1(X1)))),op2(h(esk1_1(X1)),h(X1))))!=X1|~sorti1(X1)),inference(csr,[status(thm)],[247881,31])).
% cnf(343172,negated_conjecture,(~sorti1(j(esk2_0))|op2(esk2_0,op2(h(esk1_1(j(esk2_0))),h(j(esk2_0))))!=h(j(h(esk1_1(j(esk2_0)))))|~sorti2(h(j(h(esk1_1(j(esk2_0))))))|~sorti2(h(esk1_1(j(esk2_0))))),inference(spm,[status(thm)],[248019,2028,theory(equality)])).
% cnf(370771,negated_conjecture,(op2(esk2_0,op2(h(esk1_1(j(esk2_0))),h(j(esk2_0))))!=h(j(h(esk1_1(j(esk2_0)))))|~sorti2(h(j(h(esk1_1(j(esk2_0))))))|~sorti1(j(esk2_0))),inference(csr,[status(thm)],[343172,126])).
% cnf(370772,negated_conjecture,(op2(esk2_0,op2(h(esk1_1(j(esk2_0))),h(j(esk2_0))))!=h(j(h(esk1_1(j(esk2_0)))))|~sorti1(j(esk2_0))),inference(csr,[status(thm)],[370771,839])).
% cnf(370773,negated_conjecture,(op2(esk2_0,op2(h(esk1_1(j(esk2_0))),esk2_0))!=h(j(h(esk1_1(j(esk2_0)))))|~sorti1(j(esk2_0))|~sorti2(esk2_0)),inference(spm,[status(thm)],[370772,35,theory(equality)])).
% cnf(370776,negated_conjecture,(op2(esk2_0,op2(h(esk1_1(j(esk2_0))),esk2_0))!=h(j(h(esk1_1(j(esk2_0)))))|~sorti1(j(esk2_0))|$false),inference(rw,[status(thm)],[370773,26,theory(equality)])).
% cnf(370777,negated_conjecture,(op2(esk2_0,op2(h(esk1_1(j(esk2_0))),esk2_0))!=h(j(h(esk1_1(j(esk2_0)))))|~sorti1(j(esk2_0))),inference(cn,[status(thm)],[370776,theory(equality)])).
% cnf(370780,negated_conjecture,(h(esk1_1(j(esk2_0)))!=op2(esk2_0,op2(h(esk1_1(j(esk2_0))),esk2_0))|~sorti1(j(esk2_0))|~sorti1(esk1_1(j(esk2_0)))),inference(spm,[status(thm)],[370777,36,theory(equality)])).
% cnf(370782,negated_conjecture,(op2(esk2_0,op2(h(esk1_1(j(esk2_0))),esk2_0))!=h(esk1_1(j(esk2_0)))|~sorti1(j(esk2_0))),inference(csr,[status(thm)],[370780,21])).
% cnf(370783,negated_conjecture,(~sorti1(j(esk2_0))|~sorti2(esk2_0)),inference(spm,[status(thm)],[370782,116171,theory(equality)])).
% cnf(370784,negated_conjecture,(~sorti1(j(esk2_0))|$false),inference(rw,[status(thm)],[370783,26,theory(equality)])).
% cnf(370785,negated_conjecture,(~sorti1(j(esk2_0))),inference(cn,[status(thm)],[370784,theory(equality)])).
% cnf(370969,negated_conjecture,(~sorti2(esk2_0)),inference(spm,[status(thm)],[370785,32,theory(equality)])).
% cnf(370970,negated_conjecture,($false),inference(rw,[status(thm)],[370969,26,theory(equality)])).
% cnf(370971,negated_conjecture,($false),inference(cn,[status(thm)],[370970,theory(equality)])).
% cnf(370972,negated_conjecture,($false),370971,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 10511
% # ...of these trivial : 0
% # ...subsumed : 8631
% # ...remaining for further processing: 1880
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 221
% # Backward-rewritten : 0
% # Generated clauses : 359283
% # ...of the previous two non-trivial : 358931
% # Contextual simplify-reflections : 11549
% # Paramodulations : 359283
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 1646
% # Positive orientable unit clauses: 1
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 1
% # Non-unit-clauses : 1644
% # Current number of unprocessed clauses: 332048
% # ...number of literals in the above : 2459297
% # Clause-clause subsumption calls (NU) : 650693
% # Rec. Clause-clause subsumption calls : 229501
% # Unit Clause-clause subsumption calls : 3
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 0
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 315 leaves, 10.17+/-16.848 terms/leaf
% # Paramod-from index: 108 leaves, 10.06+/-18.776 terms/leaf
% # Paramod-into index: 301 leaves, 10.20+/-17.053 terms/leaf
% # -------------------------------------------------
% # User time : 16.709 s
% # System time : 0.483 s
% # Total time : 17.192 s
% # Maximum resident set size: 0 pages
% PrfWatch: 23.87 CPU 24.10 WC
% PrfWatch: 23.89 CPU 24.14 WC
% FINAL PrfWatch: 23.89 CPU 24.14 WC
% SZS output end Solution for /tmp/SystemOnTPTP12111/ALG071+1.tptp
%
%------------------------------------------------------------------------------