%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : ALG206+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 21:08:53 EST 2010
% Result : Theorem 1.24s
% Output : Solution 1.24s
% 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/SystemOnTPTP22474/ALG206+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP22474/ALG206+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP22474/ALG206+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 22606
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.020 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,((((((((((((((((((((~(e10=e11)&~(e10=e12))&~(e10=e13))&~(e10=e14))&~(e10=e15))&~(e10=e16))&~(e11=e12))&~(e11=e13))&~(e11=e14))&~(e11=e15))&~(e11=e16))&~(e12=e13))&~(e12=e14))&~(e12=e15))&~(e12=e16))&~(e13=e14))&~(e13=e15))&~(e13=e16))&~(e14=e15))&~(e14=e16))&~(e15=e16)),file('/tmp/SRASS.s.p', ax1)).
% fof(2, axiom,((((((((((((((((((((~(e20=e21)&~(e20=e22))&~(e20=e23))&~(e20=e24))&~(e20=e25))&~(e20=e26))&~(e21=e22))&~(e21=e23))&~(e21=e24))&~(e21=e25))&~(e21=e26))&~(e22=e23))&~(e22=e24))&~(e22=e25))&~(e22=e26))&~(e23=e24))&~(e23=e25))&~(e23=e26))&~(e24=e25))&~(e24=e26))&~(e25=e26)),file('/tmp/SRASS.s.p', ax2)).
% fof(4, axiom,((((((((((((((((((((((((((((((((((((((((((((((((op1(e10,e10)=e10&op1(e10,e11)=e13)&op1(e10,e12)=e11)&op1(e10,e13)=e12)&op1(e10,e14)=e16)&op1(e10,e15)=e14)&op1(e10,e16)=e15)&op1(e11,e10)=e13)&op1(e11,e11)=e11)&op1(e11,e12)=e16)&op1(e11,e13)=e15)&op1(e11,e14)=e12)&op1(e11,e15)=e10)&op1(e11,e16)=e14)&op1(e12,e10)=e11)&op1(e12,e11)=e16)&op1(e12,e12)=e12)&op1(e12,e13)=e14)&op1(e12,e14)=e15)&op1(e12,e15)=e13)&op1(e12,e16)=e10)&op1(e13,e10)=e12)&op1(e13,e11)=e15)&op1(e13,e12)=e14)&op1(e13,e13)=e13)&op1(e13,e14)=e10)&op1(e13,e15)=e16)&op1(e13,e16)=e11)&op1(e14,e10)=e16)&op1(e14,e11)=e12)&op1(e14,e12)=e15)&op1(e14,e13)=e10)&op1(e14,e14)=e14)&op1(e14,e15)=e11)&op1(e14,e16)=e13)&op1(e15,e10)=e14)&op1(e15,e11)=e10)&op1(e15,e12)=e13)&op1(e15,e13)=e16)&op1(e15,e14)=e11)&op1(e15,e15)=e15)&op1(e15,e16)=e12)&op1(e16,e10)=e15)&op1(e16,e11)=e14)&op1(e16,e12)=e10)&op1(e16,e13)=e11)&op1(e16,e14)=e13)&op1(e16,e15)=e12)&op1(e16,e16)=e16),file('/tmp/SRASS.s.p', ax4)).
% fof(5, axiom,((((((((((((((((((((((((((((((((((((((((((((((((op2(e20,e20)=e22&op2(e20,e21)=e20)&op2(e20,e22)=e21)&op2(e20,e23)=e25)&op2(e20,e24)=e23)&op2(e20,e25)=e24)&op2(e20,e26)=e26)&op2(e21,e20)=e20)&op2(e21,e21)=e26)&op2(e21,e22)=e24)&op2(e21,e23)=e21)&op2(e21,e24)=e25)&op2(e21,e25)=e22)&op2(e21,e26)=e23)&op2(e22,e20)=e21)&op2(e22,e21)=e24)&op2(e22,e22)=e23)&op2(e22,e23)=e26)&op2(e22,e24)=e20)&op2(e22,e25)=e25)&op2(e22,e26)=e22)&op2(e23,e20)=e25)&op2(e23,e21)=e21)&op2(e23,e22)=e26)&op2(e23,e23)=e20)&op2(e23,e24)=e22)&op2(e23,e25)=e23)&op2(e23,e26)=e24)&op2(e24,e20)=e23)&op2(e24,e21)=e25)&op2(e24,e22)=e20)&op2(e24,e23)=e22)&op2(e24,e24)=e24)&op2(e24,e25)=e26)&op2(e24,e26)=e21)&op2(e25,e20)=e24)&op2(e25,e21)=e22)&op2(e25,e22)=e25)&op2(e25,e23)=e23)&op2(e25,e24)=e26)&op2(e25,e25)=e21)&op2(e25,e26)=e20)&op2(e26,e20)=e26)&op2(e26,e21)=e23)&op2(e26,e22)=e22)&op2(e26,e23)=e24)&op2(e26,e24)=e21)&op2(e26,e25)=e20)&op2(e26,e26)=e25),file('/tmp/SRASS.s.p', ax5)).
% fof(6, conjecture,((((((((((((((((((((h(e10)=e20|h(e10)=e21)|h(e10)=e22)|h(e10)=e23)|h(e10)=e24)|h(e10)=e25)|h(e10)=e26)&((((((h(e11)=e20|h(e11)=e21)|h(e11)=e22)|h(e11)=e23)|h(e11)=e24)|h(e11)=e25)|h(e11)=e26))&((((((h(e12)=e20|h(e12)=e21)|h(e12)=e22)|h(e12)=e23)|h(e12)=e24)|h(e12)=e25)|h(e12)=e26))&((((((h(e13)=e20|h(e13)=e21)|h(e13)=e22)|h(e13)=e23)|h(e13)=e24)|h(e13)=e25)|h(e13)=e26))&((((((h(e14)=e20|h(e14)=e21)|h(e14)=e22)|h(e14)=e23)|h(e14)=e24)|h(e14)=e25)|h(e14)=e26))&((((((h(e15)=e20|h(e15)=e21)|h(e15)=e22)|h(e15)=e23)|h(e15)=e24)|h(e15)=e25)|h(e15)=e26))&((((((h(e16)=e20|h(e16)=e21)|h(e16)=e22)|h(e16)=e23)|h(e16)=e24)|h(e16)=e25)|h(e16)=e26))&((((((j(e20)=e10|j(e20)=e11)|j(e20)=e12)|j(e20)=e13)|j(e20)=e14)|j(e20)=e15)|j(e20)=e16))&((((((j(e21)=e10|j(e21)=e11)|j(e21)=e12)|j(e21)=e13)|j(e21)=e14)|j(e21)=e15)|j(e21)=e16))&((((((j(e22)=e10|j(e22)=e11)|j(e22)=e12)|j(e22)=e13)|j(e22)=e14)|j(e22)=e15)|j(e22)=e16))&((((((j(e23)=e10|j(e23)=e11)|j(e23)=e12)|j(e23)=e13)|j(e23)=e14)|j(e23)=e15)|j(e23)=e16))&((((((j(e24)=e10|j(e24)=e11)|j(e24)=e12)|j(e24)=e13)|j(e24)=e14)|j(e24)=e15)|j(e24)=e16))&((((((j(e25)=e10|j(e25)=e11)|j(e25)=e12)|j(e25)=e13)|j(e25)=e14)|j(e25)=e15)|j(e25)=e16))&((((((j(e26)=e10|j(e26)=e11)|j(e26)=e12)|j(e26)=e13)|j(e26)=e14)|j(e26)=e15)|j(e26)=e16))=>~((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((h(op1(e10,e10))=op2(h(e10),h(e10))&h(op1(e10,e11))=op2(h(e10),h(e11)))&h(op1(e10,e12))=op2(h(e10),h(e12)))&h(op1(e10,e13))=op2(h(e10),h(e13)))&h(op1(e10,e14))=op2(h(e10),h(e14)))&h(op1(e10,e15))=op2(h(e10),h(e15)))&h(op1(e10,e16))=op2(h(e10),h(e16)))&h(op1(e11,e10))=op2(h(e11),h(e10)))&h(op1(e11,e11))=op2(h(e11),h(e11)))&h(op1(e11,e12))=op2(h(e11),h(e12)))&h(op1(e11,e13))=op2(h(e11),h(e13)))&h(op1(e11,e14))=op2(h(e11),h(e14)))&h(op1(e11,e15))=op2(h(e11),h(e15)))&h(op1(e11,e16))=op2(h(e11),h(e16)))&h(op1(e12,e10))=op2(h(e12),h(e10)))&h(op1(e12,e11))=op2(h(e12),h(e11)))&h(op1(e12,e12))=op2(h(e12),h(e12)))&h(op1(e12,e13))=op2(h(e12),h(e13)))&h(op1(e12,e14))=op2(h(e12),h(e14)))&h(op1(e12,e15))=op2(h(e12),h(e15)))&h(op1(e12,e16))=op2(h(e12),h(e16)))&h(op1(e13,e10))=op2(h(e13),h(e10)))&h(op1(e13,e11))=op2(h(e13),h(e11)))&h(op1(e13,e12))=op2(h(e13),h(e12)))&h(op1(e13,e13))=op2(h(e13),h(e13)))&h(op1(e13,e14))=op2(h(e13),h(e14)))&h(op1(e13,e15))=op2(h(e13),h(e15)))&h(op1(e13,e16))=op2(h(e13),h(e16)))&h(op1(e14,e10))=op2(h(e14),h(e10)))&h(op1(e14,e11))=op2(h(e14),h(e11)))&h(op1(e14,e12))=op2(h(e14),h(e12)))&h(op1(e14,e13))=op2(h(e14),h(e13)))&h(op1(e14,e14))=op2(h(e14),h(e14)))&h(op1(e14,e15))=op2(h(e14),h(e15)))&h(op1(e14,e16))=op2(h(e14),h(e16)))&h(op1(e15,e10))=op2(h(e15),h(e10)))&h(op1(e15,e11))=op2(h(e15),h(e11)))&h(op1(e15,e12))=op2(h(e15),h(e12)))&h(op1(e15,e13))=op2(h(e15),h(e13)))&h(op1(e15,e14))=op2(h(e15),h(e14)))&h(op1(e15,e15))=op2(h(e15),h(e15)))&h(op1(e15,e16))=op2(h(e15),h(e16)))&h(op1(e16,e10))=op2(h(e16),h(e10)))&h(op1(e16,e11))=op2(h(e16),h(e11)))&h(op1(e16,e12))=op2(h(e16),h(e12)))&h(op1(e16,e13))=op2(h(e16),h(e13)))&h(op1(e16,e14))=op2(h(e16),h(e14)))&h(op1(e16,e15))=op2(h(e16),h(e15)))&h(op1(e16,e16))=op2(h(e16),h(e16)))&j(op2(e20,e20))=op1(j(e20),j(e20)))&j(op2(e20,e21))=op1(j(e20),j(e21)))&j(op2(e20,e22))=op1(j(e20),j(e22)))&j(op2(e20,e23))=op1(j(e20),j(e23)))&j(op2(e20,e24))=op1(j(e20),j(e24)))&j(op2(e20,e25))=op1(j(e20),j(e25)))&j(op2(e20,e26))=op1(j(e20),j(e26)))&j(op2(e21,e20))=op1(j(e21),j(e20)))&j(op2(e21,e21))=op1(j(e21),j(e21)))&j(op2(e21,e22))=op1(j(e21),j(e22)))&j(op2(e21,e23))=op1(j(e21),j(e23)))&j(op2(e21,e24))=op1(j(e21),j(e24)))&j(op2(e21,e25))=op1(j(e21),j(e25)))&j(op2(e21,e26))=op1(j(e21),j(e26)))&j(op2(e22,e20))=op1(j(e22),j(e20)))&j(op2(e22,e21))=op1(j(e22),j(e21)))&j(op2(e22,e22))=op1(j(e22),j(e22)))&j(op2(e22,e23))=op1(j(e22),j(e23)))&j(op2(e22,e24))=op1(j(e22),j(e24)))&j(op2(e22,e25))=op1(j(e22),j(e25)))&j(op2(e22,e26))=op1(j(e22),j(e26)))&j(op2(e23,e20))=op1(j(e23),j(e20)))&j(op2(e23,e21))=op1(j(e23),j(e21)))&j(op2(e23,e22))=op1(j(e23),j(e22)))&j(op2(e23,e23))=op1(j(e23),j(e23)))&j(op2(e23,e24))=op1(j(e23),j(e24)))&j(op2(e23,e25))=op1(j(e23),j(e25)))&j(op2(e23,e26))=op1(j(e23),j(e26)))&j(op2(e24,e20))=op1(j(e24),j(e20)))&j(op2(e24,e21))=op1(j(e24),j(e21)))&j(op2(e24,e22))=op1(j(e24),j(e22)))&j(op2(e24,e23))=op1(j(e24),j(e23)))&j(op2(e24,e24))=op1(j(e24),j(e24)))&j(op2(e24,e25))=op1(j(e24),j(e25)))&j(op2(e24,e26))=op1(j(e24),j(e26)))&j(op2(e25,e20))=op1(j(e25),j(e20)))&j(op2(e25,e21))=op1(j(e25),j(e21)))&j(op2(e25,e22))=op1(j(e25),j(e22)))&j(op2(e25,e23))=op1(j(e25),j(e23)))&j(op2(e25,e24))=op1(j(e25),j(e24)))&j(op2(e25,e25))=op1(j(e25),j(e25)))&j(op2(e25,e26))=op1(j(e25),j(e26)))&j(op2(e26,e20))=op1(j(e26),j(e20)))&j(op2(e26,e21))=op1(j(e26),j(e21)))&j(op2(e26,e22))=op1(j(e26),j(e22)))&j(op2(e26,e23))=op1(j(e26),j(e23)))&j(op2(e26,e24))=op1(j(e26),j(e24)))&j(op2(e26,e25))=op1(j(e26),j(e25)))&j(op2(e26,e26))=op1(j(e26),j(e26)))&h(j(e20))=e20)&h(j(e21))=e21)&h(j(e22))=e22)&h(j(e23))=e23)&h(j(e24))=e24)&h(j(e25))=e25)&h(j(e26))=e26)&j(h(e10))=e10)&j(h(e11))=e11)&j(h(e12))=e12)&j(h(e13))=e13)&j(h(e14))=e14)&j(h(e15))=e15)&j(h(e16))=e16))),file('/tmp/SRASS.s.p', co1)).
% fof(7, negated_conjecture,~(((((((((((((((((((((h(e10)=e20|h(e10)=e21)|h(e10)=e22)|h(e10)=e23)|h(e10)=e24)|h(e10)=e25)|h(e10)=e26)&((((((h(e11)=e20|h(e11)=e21)|h(e11)=e22)|h(e11)=e23)|h(e11)=e24)|h(e11)=e25)|h(e11)=e26))&((((((h(e12)=e20|h(e12)=e21)|h(e12)=e22)|h(e12)=e23)|h(e12)=e24)|h(e12)=e25)|h(e12)=e26))&((((((h(e13)=e20|h(e13)=e21)|h(e13)=e22)|h(e13)=e23)|h(e13)=e24)|h(e13)=e25)|h(e13)=e26))&((((((h(e14)=e20|h(e14)=e21)|h(e14)=e22)|h(e14)=e23)|h(e14)=e24)|h(e14)=e25)|h(e14)=e26))&((((((h(e15)=e20|h(e15)=e21)|h(e15)=e22)|h(e15)=e23)|h(e15)=e24)|h(e15)=e25)|h(e15)=e26))&((((((h(e16)=e20|h(e16)=e21)|h(e16)=e22)|h(e16)=e23)|h(e16)=e24)|h(e16)=e25)|h(e16)=e26))&((((((j(e20)=e10|j(e20)=e11)|j(e20)=e12)|j(e20)=e13)|j(e20)=e14)|j(e20)=e15)|j(e20)=e16))&((((((j(e21)=e10|j(e21)=e11)|j(e21)=e12)|j(e21)=e13)|j(e21)=e14)|j(e21)=e15)|j(e21)=e16))&((((((j(e22)=e10|j(e22)=e11)|j(e22)=e12)|j(e22)=e13)|j(e22)=e14)|j(e22)=e15)|j(e22)=e16))&((((((j(e23)=e10|j(e23)=e11)|j(e23)=e12)|j(e23)=e13)|j(e23)=e14)|j(e23)=e15)|j(e23)=e16))&((((((j(e24)=e10|j(e24)=e11)|j(e24)=e12)|j(e24)=e13)|j(e24)=e14)|j(e24)=e15)|j(e24)=e16))&((((((j(e25)=e10|j(e25)=e11)|j(e25)=e12)|j(e25)=e13)|j(e25)=e14)|j(e25)=e15)|j(e25)=e16))&((((((j(e26)=e10|j(e26)=e11)|j(e26)=e12)|j(e26)=e13)|j(e26)=e14)|j(e26)=e15)|j(e26)=e16))=>~((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((h(op1(e10,e10))=op2(h(e10),h(e10))&h(op1(e10,e11))=op2(h(e10),h(e11)))&h(op1(e10,e12))=op2(h(e10),h(e12)))&h(op1(e10,e13))=op2(h(e10),h(e13)))&h(op1(e10,e14))=op2(h(e10),h(e14)))&h(op1(e10,e15))=op2(h(e10),h(e15)))&h(op1(e10,e16))=op2(h(e10),h(e16)))&h(op1(e11,e10))=op2(h(e11),h(e10)))&h(op1(e11,e11))=op2(h(e11),h(e11)))&h(op1(e11,e12))=op2(h(e11),h(e12)))&h(op1(e11,e13))=op2(h(e11),h(e13)))&h(op1(e11,e14))=op2(h(e11),h(e14)))&h(op1(e11,e15))=op2(h(e11),h(e15)))&h(op1(e11,e16))=op2(h(e11),h(e16)))&h(op1(e12,e10))=op2(h(e12),h(e10)))&h(op1(e12,e11))=op2(h(e12),h(e11)))&h(op1(e12,e12))=op2(h(e12),h(e12)))&h(op1(e12,e13))=op2(h(e12),h(e13)))&h(op1(e12,e14))=op2(h(e12),h(e14)))&h(op1(e12,e15))=op2(h(e12),h(e15)))&h(op1(e12,e16))=op2(h(e12),h(e16)))&h(op1(e13,e10))=op2(h(e13),h(e10)))&h(op1(e13,e11))=op2(h(e13),h(e11)))&h(op1(e13,e12))=op2(h(e13),h(e12)))&h(op1(e13,e13))=op2(h(e13),h(e13)))&h(op1(e13,e14))=op2(h(e13),h(e14)))&h(op1(e13,e15))=op2(h(e13),h(e15)))&h(op1(e13,e16))=op2(h(e13),h(e16)))&h(op1(e14,e10))=op2(h(e14),h(e10)))&h(op1(e14,e11))=op2(h(e14),h(e11)))&h(op1(e14,e12))=op2(h(e14),h(e12)))&h(op1(e14,e13))=op2(h(e14),h(e13)))&h(op1(e14,e14))=op2(h(e14),h(e14)))&h(op1(e14,e15))=op2(h(e14),h(e15)))&h(op1(e14,e16))=op2(h(e14),h(e16)))&h(op1(e15,e10))=op2(h(e15),h(e10)))&h(op1(e15,e11))=op2(h(e15),h(e11)))&h(op1(e15,e12))=op2(h(e15),h(e12)))&h(op1(e15,e13))=op2(h(e15),h(e13)))&h(op1(e15,e14))=op2(h(e15),h(e14)))&h(op1(e15,e15))=op2(h(e15),h(e15)))&h(op1(e15,e16))=op2(h(e15),h(e16)))&h(op1(e16,e10))=op2(h(e16),h(e10)))&h(op1(e16,e11))=op2(h(e16),h(e11)))&h(op1(e16,e12))=op2(h(e16),h(e12)))&h(op1(e16,e13))=op2(h(e16),h(e13)))&h(op1(e16,e14))=op2(h(e16),h(e14)))&h(op1(e16,e15))=op2(h(e16),h(e15)))&h(op1(e16,e16))=op2(h(e16),h(e16)))&j(op2(e20,e20))=op1(j(e20),j(e20)))&j(op2(e20,e21))=op1(j(e20),j(e21)))&j(op2(e20,e22))=op1(j(e20),j(e22)))&j(op2(e20,e23))=op1(j(e20),j(e23)))&j(op2(e20,e24))=op1(j(e20),j(e24)))&j(op2(e20,e25))=op1(j(e20),j(e25)))&j(op2(e20,e26))=op1(j(e20),j(e26)))&j(op2(e21,e20))=op1(j(e21),j(e20)))&j(op2(e21,e21))=op1(j(e21),j(e21)))&j(op2(e21,e22))=op1(j(e21),j(e22)))&j(op2(e21,e23))=op1(j(e21),j(e23)))&j(op2(e21,e24))=op1(j(e21),j(e24)))&j(op2(e21,e25))=op1(j(e21),j(e25)))&j(op2(e21,e26))=op1(j(e21),j(e26)))&j(op2(e22,e20))=op1(j(e22),j(e20)))&j(op2(e22,e21))=op1(j(e22),j(e21)))&j(op2(e22,e22))=op1(j(e22),j(e22)))&j(op2(e22,e23))=op1(j(e22),j(e23)))&j(op2(e22,e24))=op1(j(e22),j(e24)))&j(op2(e22,e25))=op1(j(e22),j(e25)))&j(op2(e22,e26))=op1(j(e22),j(e26)))&j(op2(e23,e20))=op1(j(e23),j(e20)))&j(op2(e23,e21))=op1(j(e23),j(e21)))&j(op2(e23,e22))=op1(j(e23),j(e22)))&j(op2(e23,e23))=op1(j(e23),j(e23)))&j(op2(e23,e24))=op1(j(e23),j(e24)))&j(op2(e23,e25))=op1(j(e23),j(e25)))&j(op2(e23,e26))=op1(j(e23),j(e26)))&j(op2(e24,e20))=op1(j(e24),j(e20)))&j(op2(e24,e21))=op1(j(e24),j(e21)))&j(op2(e24,e22))=op1(j(e24),j(e22)))&j(op2(e24,e23))=op1(j(e24),j(e23)))&j(op2(e24,e24))=op1(j(e24),j(e24)))&j(op2(e24,e25))=op1(j(e24),j(e25)))&j(op2(e24,e26))=op1(j(e24),j(e26)))&j(op2(e25,e20))=op1(j(e25),j(e20)))&j(op2(e25,e21))=op1(j(e25),j(e21)))&j(op2(e25,e22))=op1(j(e25),j(e22)))&j(op2(e25,e23))=op1(j(e25),j(e23)))&j(op2(e25,e24))=op1(j(e25),j(e24)))&j(op2(e25,e25))=op1(j(e25),j(e25)))&j(op2(e25,e26))=op1(j(e25),j(e26)))&j(op2(e26,e20))=op1(j(e26),j(e20)))&j(op2(e26,e21))=op1(j(e26),j(e21)))&j(op2(e26,e22))=op1(j(e26),j(e22)))&j(op2(e26,e23))=op1(j(e26),j(e23)))&j(op2(e26,e24))=op1(j(e26),j(e24)))&j(op2(e26,e25))=op1(j(e26),j(e25)))&j(op2(e26,e26))=op1(j(e26),j(e26)))&h(j(e20))=e20)&h(j(e21))=e21)&h(j(e22))=e22)&h(j(e23))=e23)&h(j(e24))=e24)&h(j(e25))=e25)&h(j(e26))=e26)&j(h(e10))=e10)&j(h(e11))=e11)&j(h(e12))=e12)&j(h(e13))=e13)&j(h(e14))=e14)&j(h(e15))=e15)&j(h(e16))=e16)))),inference(assume_negation,[status(cth)],[6])).
% fof(8, plain,(epred1_0=>(((((((((((((((((((h(e10)=e20|h(e10)=e21)|h(e10)=e22)|h(e10)=e23)|h(e10)=e24)|h(e10)=e25)|h(e10)=e26)&((((((h(e11)=e20|h(e11)=e21)|h(e11)=e22)|h(e11)=e23)|h(e11)=e24)|h(e11)=e25)|h(e11)=e26))&((((((h(e12)=e20|h(e12)=e21)|h(e12)=e22)|h(e12)=e23)|h(e12)=e24)|h(e12)=e25)|h(e12)=e26))&((((((h(e13)=e20|h(e13)=e21)|h(e13)=e22)|h(e13)=e23)|h(e13)=e24)|h(e13)=e25)|h(e13)=e26))&((((((h(e14)=e20|h(e14)=e21)|h(e14)=e22)|h(e14)=e23)|h(e14)=e24)|h(e14)=e25)|h(e14)=e26))&((((((h(e15)=e20|h(e15)=e21)|h(e15)=e22)|h(e15)=e23)|h(e15)=e24)|h(e15)=e25)|h(e15)=e26))&((((((h(e16)=e20|h(e16)=e21)|h(e16)=e22)|h(e16)=e23)|h(e16)=e24)|h(e16)=e25)|h(e16)=e26))&((((((j(e20)=e10|j(e20)=e11)|j(e20)=e12)|j(e20)=e13)|j(e20)=e14)|j(e20)=e15)|j(e20)=e16))&((((((j(e21)=e10|j(e21)=e11)|j(e21)=e12)|j(e21)=e13)|j(e21)=e14)|j(e21)=e15)|j(e21)=e16))&((((((j(e22)=e10|j(e22)=e11)|j(e22)=e12)|j(e22)=e13)|j(e22)=e14)|j(e22)=e15)|j(e22)=e16))&((((((j(e23)=e10|j(e23)=e11)|j(e23)=e12)|j(e23)=e13)|j(e23)=e14)|j(e23)=e15)|j(e23)=e16))&((((((j(e24)=e10|j(e24)=e11)|j(e24)=e12)|j(e24)=e13)|j(e24)=e14)|j(e24)=e15)|j(e24)=e16))&((((((j(e25)=e10|j(e25)=e11)|j(e25)=e12)|j(e25)=e13)|j(e25)=e14)|j(e25)=e15)|j(e25)=e16))&((((((j(e26)=e10|j(e26)=e11)|j(e26)=e12)|j(e26)=e13)|j(e26)=e14)|j(e26)=e15)|j(e26)=e16))),introduced(definition)).
% fof(9, negated_conjecture,~((epred1_0=>~((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((h(op1(e10,e10))=op2(h(e10),h(e10))&h(op1(e10,e11))=op2(h(e10),h(e11)))&h(op1(e10,e12))=op2(h(e10),h(e12)))&h(op1(e10,e13))=op2(h(e10),h(e13)))&h(op1(e10,e14))=op2(h(e10),h(e14)))&h(op1(e10,e15))=op2(h(e10),h(e15)))&h(op1(e10,e16))=op2(h(e10),h(e16)))&h(op1(e11,e10))=op2(h(e11),h(e10)))&h(op1(e11,e11))=op2(h(e11),h(e11)))&h(op1(e11,e12))=op2(h(e11),h(e12)))&h(op1(e11,e13))=op2(h(e11),h(e13)))&h(op1(e11,e14))=op2(h(e11),h(e14)))&h(op1(e11,e15))=op2(h(e11),h(e15)))&h(op1(e11,e16))=op2(h(e11),h(e16)))&h(op1(e12,e10))=op2(h(e12),h(e10)))&h(op1(e12,e11))=op2(h(e12),h(e11)))&h(op1(e12,e12))=op2(h(e12),h(e12)))&h(op1(e12,e13))=op2(h(e12),h(e13)))&h(op1(e12,e14))=op2(h(e12),h(e14)))&h(op1(e12,e15))=op2(h(e12),h(e15)))&h(op1(e12,e16))=op2(h(e12),h(e16)))&h(op1(e13,e10))=op2(h(e13),h(e10)))&h(op1(e13,e11))=op2(h(e13),h(e11)))&h(op1(e13,e12))=op2(h(e13),h(e12)))&h(op1(e13,e13))=op2(h(e13),h(e13)))&h(op1(e13,e14))=op2(h(e13),h(e14)))&h(op1(e13,e15))=op2(h(e13),h(e15)))&h(op1(e13,e16))=op2(h(e13),h(e16)))&h(op1(e14,e10))=op2(h(e14),h(e10)))&h(op1(e14,e11))=op2(h(e14),h(e11)))&h(op1(e14,e12))=op2(h(e14),h(e12)))&h(op1(e14,e13))=op2(h(e14),h(e13)))&h(op1(e14,e14))=op2(h(e14),h(e14)))&h(op1(e14,e15))=op2(h(e14),h(e15)))&h(op1(e14,e16))=op2(h(e14),h(e16)))&h(op1(e15,e10))=op2(h(e15),h(e10)))&h(op1(e15,e11))=op2(h(e15),h(e11)))&h(op1(e15,e12))=op2(h(e15),h(e12)))&h(op1(e15,e13))=op2(h(e15),h(e13)))&h(op1(e15,e14))=op2(h(e15),h(e14)))&h(op1(e15,e15))=op2(h(e15),h(e15)))&h(op1(e15,e16))=op2(h(e15),h(e16)))&h(op1(e16,e10))=op2(h(e16),h(e10)))&h(op1(e16,e11))=op2(h(e16),h(e11)))&h(op1(e16,e12))=op2(h(e16),h(e12)))&h(op1(e16,e13))=op2(h(e16),h(e13)))&h(op1(e16,e14))=op2(h(e16),h(e14)))&h(op1(e16,e15))=op2(h(e16),h(e15)))&h(op1(e16,e16))=op2(h(e16),h(e16)))&j(op2(e20,e20))=op1(j(e20),j(e20)))&j(op2(e20,e21))=op1(j(e20),j(e21)))&j(op2(e20,e22))=op1(j(e20),j(e22)))&j(op2(e20,e23))=op1(j(e20),j(e23)))&j(op2(e20,e24))=op1(j(e20),j(e24)))&j(op2(e20,e25))=op1(j(e20),j(e25)))&j(op2(e20,e26))=op1(j(e20),j(e26)))&j(op2(e21,e20))=op1(j(e21),j(e20)))&j(op2(e21,e21))=op1(j(e21),j(e21)))&j(op2(e21,e22))=op1(j(e21),j(e22)))&j(op2(e21,e23))=op1(j(e21),j(e23)))&j(op2(e21,e24))=op1(j(e21),j(e24)))&j(op2(e21,e25))=op1(j(e21),j(e25)))&j(op2(e21,e26))=op1(j(e21),j(e26)))&j(op2(e22,e20))=op1(j(e22),j(e20)))&j(op2(e22,e21))=op1(j(e22),j(e21)))&j(op2(e22,e22))=op1(j(e22),j(e22)))&j(op2(e22,e23))=op1(j(e22),j(e23)))&j(op2(e22,e24))=op1(j(e22),j(e24)))&j(op2(e22,e25))=op1(j(e22),j(e25)))&j(op2(e22,e26))=op1(j(e22),j(e26)))&j(op2(e23,e20))=op1(j(e23),j(e20)))&j(op2(e23,e21))=op1(j(e23),j(e21)))&j(op2(e23,e22))=op1(j(e23),j(e22)))&j(op2(e23,e23))=op1(j(e23),j(e23)))&j(op2(e23,e24))=op1(j(e23),j(e24)))&j(op2(e23,e25))=op1(j(e23),j(e25)))&j(op2(e23,e26))=op1(j(e23),j(e26)))&j(op2(e24,e20))=op1(j(e24),j(e20)))&j(op2(e24,e21))=op1(j(e24),j(e21)))&j(op2(e24,e22))=op1(j(e24),j(e22)))&j(op2(e24,e23))=op1(j(e24),j(e23)))&j(op2(e24,e24))=op1(j(e24),j(e24)))&j(op2(e24,e25))=op1(j(e24),j(e25)))&j(op2(e24,e26))=op1(j(e24),j(e26)))&j(op2(e25,e20))=op1(j(e25),j(e20)))&j(op2(e25,e21))=op1(j(e25),j(e21)))&j(op2(e25,e22))=op1(j(e25),j(e22)))&j(op2(e25,e23))=op1(j(e25),j(e23)))&j(op2(e25,e24))=op1(j(e25),j(e24)))&j(op2(e25,e25))=op1(j(e25),j(e25)))&j(op2(e25,e26))=op1(j(e25),j(e26)))&j(op2(e26,e20))=op1(j(e26),j(e20)))&j(op2(e26,e21))=op1(j(e26),j(e21)))&j(op2(e26,e22))=op1(j(e26),j(e22)))&j(op2(e26,e23))=op1(j(e26),j(e23)))&j(op2(e26,e24))=op1(j(e26),j(e24)))&j(op2(e26,e25))=op1(j(e26),j(e25)))&j(op2(e26,e26))=op1(j(e26),j(e26)))&h(j(e20))=e20)&h(j(e21))=e21)&h(j(e22))=e22)&h(j(e23))=e23)&h(j(e24))=e24)&h(j(e25))=e25)&h(j(e26))=e26)&j(h(e10))=e10)&j(h(e11))=e11)&j(h(e12))=e12)&j(h(e13))=e13)&j(h(e14))=e14)&j(h(e15))=e15)&j(h(e16))=e16)))),inference(apply_def,[status(esa)],[7,8,theory(equality)])).
% cnf(30,plain,(e10!=e11),inference(split_conjunct,[status(thm)],[1])).
% cnf(31,plain,(e25!=e26),inference(split_conjunct,[status(thm)],[2])).
% cnf(40,plain,(e22!=e23),inference(split_conjunct,[status(thm)],[2])).
% cnf(41,plain,(e21!=e26),inference(split_conjunct,[status(thm)],[2])).
% cnf(42,plain,(e21!=e25),inference(split_conjunct,[status(thm)],[2])).
% cnf(49,plain,(e20!=e23),inference(split_conjunct,[status(thm)],[2])).
% cnf(50,plain,(e20!=e22),inference(split_conjunct,[status(thm)],[2])).
% cnf(141,plain,(op1(e11,e11)=e11),inference(split_conjunct,[status(thm)],[4])).
% cnf(149,plain,(op1(e10,e10)=e10),inference(split_conjunct,[status(thm)],[4])).
% cnf(150,plain,(op2(e26,e26)=e25),inference(split_conjunct,[status(thm)],[5])).
% cnf(158,plain,(op2(e25,e25)=e21),inference(split_conjunct,[status(thm)],[5])).
% cnf(174,plain,(op2(e23,e23)=e20),inference(split_conjunct,[status(thm)],[5])).
% cnf(182,plain,(op2(e22,e22)=e23),inference(split_conjunct,[status(thm)],[5])).
% cnf(190,plain,(op2(e21,e21)=e26),inference(split_conjunct,[status(thm)],[5])).
% cnf(198,plain,(op2(e20,e20)=e22),inference(split_conjunct,[status(thm)],[5])).
% fof(199, negated_conjecture,(epred1_0&(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((h(op1(e10,e10))=op2(h(e10),h(e10))&h(op1(e10,e11))=op2(h(e10),h(e11)))&h(op1(e10,e12))=op2(h(e10),h(e12)))&h(op1(e10,e13))=op2(h(e10),h(e13)))&h(op1(e10,e14))=op2(h(e10),h(e14)))&h(op1(e10,e15))=op2(h(e10),h(e15)))&h(op1(e10,e16))=op2(h(e10),h(e16)))&h(op1(e11,e10))=op2(h(e11),h(e10)))&h(op1(e11,e11))=op2(h(e11),h(e11)))&h(op1(e11,e12))=op2(h(e11),h(e12)))&h(op1(e11,e13))=op2(h(e11),h(e13)))&h(op1(e11,e14))=op2(h(e11),h(e14)))&h(op1(e11,e15))=op2(h(e11),h(e15)))&h(op1(e11,e16))=op2(h(e11),h(e16)))&h(op1(e12,e10))=op2(h(e12),h(e10)))&h(op1(e12,e11))=op2(h(e12),h(e11)))&h(op1(e12,e12))=op2(h(e12),h(e12)))&h(op1(e12,e13))=op2(h(e12),h(e13)))&h(op1(e12,e14))=op2(h(e12),h(e14)))&h(op1(e12,e15))=op2(h(e12),h(e15)))&h(op1(e12,e16))=op2(h(e12),h(e16)))&h(op1(e13,e10))=op2(h(e13),h(e10)))&h(op1(e13,e11))=op2(h(e13),h(e11)))&h(op1(e13,e12))=op2(h(e13),h(e12)))&h(op1(e13,e13))=op2(h(e13),h(e13)))&h(op1(e13,e14))=op2(h(e13),h(e14)))&h(op1(e13,e15))=op2(h(e13),h(e15)))&h(op1(e13,e16))=op2(h(e13),h(e16)))&h(op1(e14,e10))=op2(h(e14),h(e10)))&h(op1(e14,e11))=op2(h(e14),h(e11)))&h(op1(e14,e12))=op2(h(e14),h(e12)))&h(op1(e14,e13))=op2(h(e14),h(e13)))&h(op1(e14,e14))=op2(h(e14),h(e14)))&h(op1(e14,e15))=op2(h(e14),h(e15)))&h(op1(e14,e16))=op2(h(e14),h(e16)))&h(op1(e15,e10))=op2(h(e15),h(e10)))&h(op1(e15,e11))=op2(h(e15),h(e11)))&h(op1(e15,e12))=op2(h(e15),h(e12)))&h(op1(e15,e13))=op2(h(e15),h(e13)))&h(op1(e15,e14))=op2(h(e15),h(e14)))&h(op1(e15,e15))=op2(h(e15),h(e15)))&h(op1(e15,e16))=op2(h(e15),h(e16)))&h(op1(e16,e10))=op2(h(e16),h(e10)))&h(op1(e16,e11))=op2(h(e16),h(e11)))&h(op1(e16,e12))=op2(h(e16),h(e12)))&h(op1(e16,e13))=op2(h(e16),h(e13)))&h(op1(e16,e14))=op2(h(e16),h(e14)))&h(op1(e16,e15))=op2(h(e16),h(e15)))&h(op1(e16,e16))=op2(h(e16),h(e16)))&j(op2(e20,e20))=op1(j(e20),j(e20)))&j(op2(e20,e21))=op1(j(e20),j(e21)))&j(op2(e20,e22))=op1(j(e20),j(e22)))&j(op2(e20,e23))=op1(j(e20),j(e23)))&j(op2(e20,e24))=op1(j(e20),j(e24)))&j(op2(e20,e25))=op1(j(e20),j(e25)))&j(op2(e20,e26))=op1(j(e20),j(e26)))&j(op2(e21,e20))=op1(j(e21),j(e20)))&j(op2(e21,e21))=op1(j(e21),j(e21)))&j(op2(e21,e22))=op1(j(e21),j(e22)))&j(op2(e21,e23))=op1(j(e21),j(e23)))&j(op2(e21,e24))=op1(j(e21),j(e24)))&j(op2(e21,e25))=op1(j(e21),j(e25)))&j(op2(e21,e26))=op1(j(e21),j(e26)))&j(op2(e22,e20))=op1(j(e22),j(e20)))&j(op2(e22,e21))=op1(j(e22),j(e21)))&j(op2(e22,e22))=op1(j(e22),j(e22)))&j(op2(e22,e23))=op1(j(e22),j(e23)))&j(op2(e22,e24))=op1(j(e22),j(e24)))&j(op2(e22,e25))=op1(j(e22),j(e25)))&j(op2(e22,e26))=op1(j(e22),j(e26)))&j(op2(e23,e20))=op1(j(e23),j(e20)))&j(op2(e23,e21))=op1(j(e23),j(e21)))&j(op2(e23,e22))=op1(j(e23),j(e22)))&j(op2(e23,e23))=op1(j(e23),j(e23)))&j(op2(e23,e24))=op1(j(e23),j(e24)))&j(op2(e23,e25))=op1(j(e23),j(e25)))&j(op2(e23,e26))=op1(j(e23),j(e26)))&j(op2(e24,e20))=op1(j(e24),j(e20)))&j(op2(e24,e21))=op1(j(e24),j(e21)))&j(op2(e24,e22))=op1(j(e24),j(e22)))&j(op2(e24,e23))=op1(j(e24),j(e23)))&j(op2(e24,e24))=op1(j(e24),j(e24)))&j(op2(e24,e25))=op1(j(e24),j(e25)))&j(op2(e24,e26))=op1(j(e24),j(e26)))&j(op2(e25,e20))=op1(j(e25),j(e20)))&j(op2(e25,e21))=op1(j(e25),j(e21)))&j(op2(e25,e22))=op1(j(e25),j(e22)))&j(op2(e25,e23))=op1(j(e25),j(e23)))&j(op2(e25,e24))=op1(j(e25),j(e24)))&j(op2(e25,e25))=op1(j(e25),j(e25)))&j(op2(e25,e26))=op1(j(e25),j(e26)))&j(op2(e26,e20))=op1(j(e26),j(e20)))&j(op2(e26,e21))=op1(j(e26),j(e21)))&j(op2(e26,e22))=op1(j(e26),j(e22)))&j(op2(e26,e23))=op1(j(e26),j(e23)))&j(op2(e26,e24))=op1(j(e26),j(e24)))&j(op2(e26,e25))=op1(j(e26),j(e25)))&j(op2(e26,e26))=op1(j(e26),j(e26)))&h(j(e20))=e20)&h(j(e21))=e21)&h(j(e22))=e22)&h(j(e23))=e23)&h(j(e24))=e24)&h(j(e25))=e25)&h(j(e26))=e26)&j(h(e10))=e10)&j(h(e11))=e11)&j(h(e12))=e12)&j(h(e13))=e13)&j(h(e14))=e14)&j(h(e15))=e15)&j(h(e16))=e16)),inference(fof_nnf,[status(thm)],[9])).
% cnf(205,negated_conjecture,(j(h(e11))=e11),inference(split_conjunct,[status(thm)],[199])).
% cnf(206,negated_conjecture,(j(h(e10))=e10),inference(split_conjunct,[status(thm)],[199])).
% cnf(303,negated_conjecture,(h(op1(e11,e11))=op2(h(e11),h(e11))),inference(split_conjunct,[status(thm)],[199])).
% cnf(311,negated_conjecture,(h(op1(e10,e10))=op2(h(e10),h(e10))),inference(split_conjunct,[status(thm)],[199])).
% cnf(312,negated_conjecture,(epred1_0),inference(split_conjunct,[status(thm)],[199])).
% fof(313, plain,(~(epred1_0)|(((((((((((((((((((h(e10)=e20|h(e10)=e21)|h(e10)=e22)|h(e10)=e23)|h(e10)=e24)|h(e10)=e25)|h(e10)=e26)&((((((h(e11)=e20|h(e11)=e21)|h(e11)=e22)|h(e11)=e23)|h(e11)=e24)|h(e11)=e25)|h(e11)=e26))&((((((h(e12)=e20|h(e12)=e21)|h(e12)=e22)|h(e12)=e23)|h(e12)=e24)|h(e12)=e25)|h(e12)=e26))&((((((h(e13)=e20|h(e13)=e21)|h(e13)=e22)|h(e13)=e23)|h(e13)=e24)|h(e13)=e25)|h(e13)=e26))&((((((h(e14)=e20|h(e14)=e21)|h(e14)=e22)|h(e14)=e23)|h(e14)=e24)|h(e14)=e25)|h(e14)=e26))&((((((h(e15)=e20|h(e15)=e21)|h(e15)=e22)|h(e15)=e23)|h(e15)=e24)|h(e15)=e25)|h(e15)=e26))&((((((h(e16)=e20|h(e16)=e21)|h(e16)=e22)|h(e16)=e23)|h(e16)=e24)|h(e16)=e25)|h(e16)=e26))&((((((j(e20)=e10|j(e20)=e11)|j(e20)=e12)|j(e20)=e13)|j(e20)=e14)|j(e20)=e15)|j(e20)=e16))&((((((j(e21)=e10|j(e21)=e11)|j(e21)=e12)|j(e21)=e13)|j(e21)=e14)|j(e21)=e15)|j(e21)=e16))&((((((j(e22)=e10|j(e22)=e11)|j(e22)=e12)|j(e22)=e13)|j(e22)=e14)|j(e22)=e15)|j(e22)=e16))&((((((j(e23)=e10|j(e23)=e11)|j(e23)=e12)|j(e23)=e13)|j(e23)=e14)|j(e23)=e15)|j(e23)=e16))&((((((j(e24)=e10|j(e24)=e11)|j(e24)=e12)|j(e24)=e13)|j(e24)=e14)|j(e24)=e15)|j(e24)=e16))&((((((j(e25)=e10|j(e25)=e11)|j(e25)=e12)|j(e25)=e13)|j(e25)=e14)|j(e25)=e15)|j(e25)=e16))&((((((j(e26)=e10|j(e26)=e11)|j(e26)=e12)|j(e26)=e13)|j(e26)=e14)|j(e26)=e15)|j(e26)=e16))),inference(fof_nnf,[status(thm)],[8])).
% fof(314, plain,((((((((((((((((((((h(e10)=e20|h(e10)=e21)|h(e10)=e22)|h(e10)=e23)|h(e10)=e24)|h(e10)=e25)|h(e10)=e26)|~(epred1_0))&(((((((h(e11)=e20|h(e11)=e21)|h(e11)=e22)|h(e11)=e23)|h(e11)=e24)|h(e11)=e25)|h(e11)=e26)|~(epred1_0)))&(((((((h(e12)=e20|h(e12)=e21)|h(e12)=e22)|h(e12)=e23)|h(e12)=e24)|h(e12)=e25)|h(e12)=e26)|~(epred1_0)))&(((((((h(e13)=e20|h(e13)=e21)|h(e13)=e22)|h(e13)=e23)|h(e13)=e24)|h(e13)=e25)|h(e13)=e26)|~(epred1_0)))&(((((((h(e14)=e20|h(e14)=e21)|h(e14)=e22)|h(e14)=e23)|h(e14)=e24)|h(e14)=e25)|h(e14)=e26)|~(epred1_0)))&(((((((h(e15)=e20|h(e15)=e21)|h(e15)=e22)|h(e15)=e23)|h(e15)=e24)|h(e15)=e25)|h(e15)=e26)|~(epred1_0)))&(((((((h(e16)=e20|h(e16)=e21)|h(e16)=e22)|h(e16)=e23)|h(e16)=e24)|h(e16)=e25)|h(e16)=e26)|~(epred1_0)))&(((((((j(e20)=e10|j(e20)=e11)|j(e20)=e12)|j(e20)=e13)|j(e20)=e14)|j(e20)=e15)|j(e20)=e16)|~(epred1_0)))&(((((((j(e21)=e10|j(e21)=e11)|j(e21)=e12)|j(e21)=e13)|j(e21)=e14)|j(e21)=e15)|j(e21)=e16)|~(epred1_0)))&(((((((j(e22)=e10|j(e22)=e11)|j(e22)=e12)|j(e22)=e13)|j(e22)=e14)|j(e22)=e15)|j(e22)=e16)|~(epred1_0)))&(((((((j(e23)=e10|j(e23)=e11)|j(e23)=e12)|j(e23)=e13)|j(e23)=e14)|j(e23)=e15)|j(e23)=e16)|~(epred1_0)))&(((((((j(e24)=e10|j(e24)=e11)|j(e24)=e12)|j(e24)=e13)|j(e24)=e14)|j(e24)=e15)|j(e24)=e16)|~(epred1_0)))&(((((((j(e25)=e10|j(e25)=e11)|j(e25)=e12)|j(e25)=e13)|j(e25)=e14)|j(e25)=e15)|j(e25)=e16)|~(epred1_0)))&(((((((j(e26)=e10|j(e26)=e11)|j(e26)=e12)|j(e26)=e13)|j(e26)=e14)|j(e26)=e15)|j(e26)=e16)|~(epred1_0))),inference(distribute,[status(thm)],[313])).
% cnf(327,plain,(h(e11)=e26|h(e11)=e25|h(e11)=e24|h(e11)=e23|h(e11)=e22|h(e11)=e21|h(e11)=e20|~epred1_0),inference(split_conjunct,[status(thm)],[314])).
% cnf(328,plain,(h(e10)=e26|h(e10)=e25|h(e10)=e24|h(e10)=e23|h(e10)=e22|h(e10)=e21|h(e10)=e20|~epred1_0),inference(split_conjunct,[status(thm)],[314])).
% cnf(331,plain,(h(e10)=e20|h(e10)=e21|h(e10)=e22|h(e10)=e23|h(e10)=e24|h(e10)=e25|h(e10)=e26|$false),inference(rw,[status(thm)],[328,312,theory(equality)])).
% cnf(332,plain,(h(e10)=e20|h(e10)=e21|h(e10)=e22|h(e10)=e23|h(e10)=e24|h(e10)=e25|h(e10)=e26),inference(cn,[status(thm)],[331,theory(equality)])).
% cnf(341,plain,(h(e11)=e20|h(e11)=e21|h(e11)=e22|h(e11)=e23|h(e11)=e24|h(e11)=e25|h(e11)=e26|$false),inference(rw,[status(thm)],[327,312,theory(equality)])).
% cnf(342,plain,(h(e11)=e20|h(e11)=e21|h(e11)=e22|h(e11)=e23|h(e11)=e24|h(e11)=e25|h(e11)=e26),inference(cn,[status(thm)],[341,theory(equality)])).
% cnf(390,negated_conjecture,(op2(h(e10),h(e10))=h(e10)),inference(rw,[status(thm)],[311,149,theory(equality)])).
% cnf(400,negated_conjecture,(op2(h(e11),h(e11))=h(e11)),inference(rw,[status(thm)],[303,141,theory(equality)])).
% cnf(462,negated_conjecture,(op2(e26,e26)=e26|h(e10)=e20|h(e10)=e21|h(e10)=e22|h(e10)=e23|h(e10)=e24|h(e10)=e25),inference(spm,[status(thm)],[390,332,theory(equality)])).
% cnf(475,negated_conjecture,(e25=e26|h(e10)=e20|h(e10)=e21|h(e10)=e22|h(e10)=e23|h(e10)=e24|h(e10)=e25),inference(rw,[status(thm)],[462,150,theory(equality)])).
% cnf(476,negated_conjecture,(h(e10)=e20|h(e10)=e21|h(e10)=e22|h(e10)=e23|h(e10)=e24|h(e10)=e25),inference(sr,[status(thm)],[475,31,theory(equality)])).
% cnf(486,negated_conjecture,(op2(e26,e26)=e26|h(e11)=e20|h(e11)=e21|h(e11)=e22|h(e11)=e23|h(e11)=e24|h(e11)=e25),inference(spm,[status(thm)],[400,342,theory(equality)])).
% cnf(497,negated_conjecture,(e25=e26|h(e11)=e20|h(e11)=e21|h(e11)=e22|h(e11)=e23|h(e11)=e24|h(e11)=e25),inference(rw,[status(thm)],[486,150,theory(equality)])).
% cnf(498,negated_conjecture,(h(e11)=e20|h(e11)=e21|h(e11)=e22|h(e11)=e23|h(e11)=e24|h(e11)=e25),inference(sr,[status(thm)],[497,31,theory(equality)])).
% cnf(762,negated_conjecture,(op2(e25,e25)=e25|h(e10)=e24|h(e10)=e23|h(e10)=e22|h(e10)=e21|h(e10)=e20),inference(spm,[status(thm)],[390,476,theory(equality)])).
% cnf(775,negated_conjecture,(e21=e25|h(e10)=e24|h(e10)=e23|h(e10)=e22|h(e10)=e21|h(e10)=e20),inference(rw,[status(thm)],[762,158,theory(equality)])).
% cnf(776,negated_conjecture,(h(e10)=e24|h(e10)=e23|h(e10)=e22|h(e10)=e21|h(e10)=e20),inference(sr,[status(thm)],[775,42,theory(equality)])).
% cnf(781,negated_conjecture,(j(e24)=e10|h(e10)=e20|h(e10)=e21|h(e10)=e22|h(e10)=e23),inference(spm,[status(thm)],[206,776,theory(equality)])).
% cnf(800,negated_conjecture,(op2(e23,e23)=e23|h(e10)=e22|h(e10)=e21|h(e10)=e20|j(e24)=e10),inference(spm,[status(thm)],[390,781,theory(equality)])).
% cnf(813,negated_conjecture,(e20=e23|h(e10)=e22|h(e10)=e21|h(e10)=e20|j(e24)=e10),inference(rw,[status(thm)],[800,174,theory(equality)])).
% cnf(814,negated_conjecture,(h(e10)=e22|h(e10)=e21|h(e10)=e20|j(e24)=e10),inference(sr,[status(thm)],[813,49,theory(equality)])).
% cnf(818,negated_conjecture,(op2(e22,e22)=e22|j(e24)=e10|h(e10)=e20|h(e10)=e21),inference(spm,[status(thm)],[390,814,theory(equality)])).
% cnf(831,negated_conjecture,(e23=e22|j(e24)=e10|h(e10)=e20|h(e10)=e21),inference(rw,[status(thm)],[818,182,theory(equality)])).
% cnf(832,negated_conjecture,(j(e24)=e10|h(e10)=e20|h(e10)=e21),inference(sr,[status(thm)],[831,40,theory(equality)])).
% cnf(835,negated_conjecture,(op2(e21,e21)=e21|h(e10)=e20|j(e24)=e10),inference(spm,[status(thm)],[390,832,theory(equality)])).
% cnf(848,negated_conjecture,(e26=e21|h(e10)=e20|j(e24)=e10),inference(rw,[status(thm)],[835,190,theory(equality)])).
% cnf(849,negated_conjecture,(h(e10)=e20|j(e24)=e10),inference(sr,[status(thm)],[848,41,theory(equality)])).
% cnf(851,negated_conjecture,(op2(e20,e20)=e20|j(e24)=e10),inference(spm,[status(thm)],[390,849,theory(equality)])).
% cnf(864,negated_conjecture,(e22=e20|j(e24)=e10),inference(rw,[status(thm)],[851,198,theory(equality)])).
% cnf(865,negated_conjecture,(j(e24)=e10),inference(sr,[status(thm)],[864,50,theory(equality)])).
% cnf(1004,negated_conjecture,(op2(e25,e25)=e25|h(e11)=e24|h(e11)=e23|h(e11)=e22|h(e11)=e21|h(e11)=e20),inference(spm,[status(thm)],[400,498,theory(equality)])).
% cnf(1017,negated_conjecture,(e21=e25|h(e11)=e24|h(e11)=e23|h(e11)=e22|h(e11)=e21|h(e11)=e20),inference(rw,[status(thm)],[1004,158,theory(equality)])).
% cnf(1018,negated_conjecture,(h(e11)=e24|h(e11)=e23|h(e11)=e22|h(e11)=e21|h(e11)=e20),inference(sr,[status(thm)],[1017,42,theory(equality)])).
% cnf(1023,negated_conjecture,(j(e24)=e11|h(e11)=e20|h(e11)=e21|h(e11)=e22|h(e11)=e23),inference(spm,[status(thm)],[205,1018,theory(equality)])).
% cnf(1037,negated_conjecture,(e10=e11|h(e11)=e20|h(e11)=e21|h(e11)=e22|h(e11)=e23),inference(rw,[status(thm)],[1023,865,theory(equality)])).
% cnf(1038,negated_conjecture,(h(e11)=e20|h(e11)=e21|h(e11)=e22|h(e11)=e23),inference(sr,[status(thm)],[1037,30,theory(equality)])).
% cnf(1058,negated_conjecture,(op2(e23,e23)=e23|h(e11)=e22|h(e11)=e21|h(e11)=e20),inference(spm,[status(thm)],[400,1038,theory(equality)])).
% cnf(1071,negated_conjecture,(e20=e23|h(e11)=e22|h(e11)=e21|h(e11)=e20),inference(rw,[status(thm)],[1058,174,theory(equality)])).
% cnf(1072,negated_conjecture,(h(e11)=e22|h(e11)=e21|h(e11)=e20),inference(sr,[status(thm)],[1071,49,theory(equality)])).
% cnf(1078,negated_conjecture,(op2(e22,e22)=e22|h(e11)=e20|h(e11)=e21),inference(spm,[status(thm)],[400,1072,theory(equality)])).
% cnf(1091,negated_conjecture,(e23=e22|h(e11)=e20|h(e11)=e21),inference(rw,[status(thm)],[1078,182,theory(equality)])).
% cnf(1092,negated_conjecture,(h(e11)=e20|h(e11)=e21),inference(sr,[status(thm)],[1091,40,theory(equality)])).
% cnf(1097,negated_conjecture,(op2(e21,e21)=e21|h(e11)=e20),inference(spm,[status(thm)],[400,1092,theory(equality)])).
% cnf(1110,negated_conjecture,(e26=e21|h(e11)=e20),inference(rw,[status(thm)],[1097,190,theory(equality)])).
% cnf(1111,negated_conjecture,(h(e11)=e20),inference(sr,[status(thm)],[1110,41,theory(equality)])).
% cnf(1128,negated_conjecture,(e22=h(e11)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[400,1111,theory(equality)]),1111,theory(equality)]),198,theory(equality)])).
% cnf(1129,negated_conjecture,(e22=e20),inference(rw,[status(thm)],[1128,1111,theory(equality)])).
% cnf(1130,negated_conjecture,($false),inference(sr,[status(thm)],[1129,50,theory(equality)])).
% cnf(1131,negated_conjecture,($false),1130,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 688
% # ...of these trivial : 0
% # ...subsumed : 6
% # ...remaining for further processing: 682
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 10
% # Backward-rewritten : 64
% # Generated clauses : 512
% # ...of the previous two non-trivial : 561
% # Contextual simplify-reflections : 0
% # Paramodulations : 398
% # Factorizations : 114
% # Equation resolutions : 0
% # Current number of processed clauses: 292
% # Positive orientable unit clauses: 190
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 91
% # Non-unit-clauses : 11
% # Current number of unprocessed clauses: 214
% # ...number of literals in the above : 1403
% # Clause-clause subsumption calls (NU) : 10
% # Rec. Clause-clause subsumption calls : 10
% # Unit Clause-clause subsumption calls : 0
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 3
% # Indexed BW rewrite successes : 3
% # Backwards rewriting index: 216 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-from index: 201 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 215 leaves, 1.00+/-0.000 terms/leaf
% # -------------------------------------------------
% # User time : 0.040 s
% # System time : 0.011 s
% # Total time : 0.051 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.17 CPU 0.23 WC
% FINAL PrfWatch: 0.17 CPU 0.23 WC
% SZS output end Solution for /tmp/SystemOnTPTP22474/ALG206+1.tptp
%
%------------------------------------------------------------------------------