%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : ALG117+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 : 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 : Tue Dec 28 20:53:16 EST 2010
% Result : Theorem 1.77s
% Output : Solution 1.77s
% 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/SystemOnTPTP7966/ALG117+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP7966/ALG117+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP7966/ALG117+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 8062
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.113 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,((((((((((((((((((op1(e10,e10)=e10|op1(e10,e10)=e11)|op1(e10,e10)=e12)|op1(e10,e10)=e13)&(((op1(e10,e11)=e10|op1(e10,e11)=e11)|op1(e10,e11)=e12)|op1(e10,e11)=e13))&(((op1(e10,e12)=e10|op1(e10,e12)=e11)|op1(e10,e12)=e12)|op1(e10,e12)=e13))&(((op1(e10,e13)=e10|op1(e10,e13)=e11)|op1(e10,e13)=e12)|op1(e10,e13)=e13))&(((op1(e11,e10)=e10|op1(e11,e10)=e11)|op1(e11,e10)=e12)|op1(e11,e10)=e13))&(((op1(e11,e11)=e10|op1(e11,e11)=e11)|op1(e11,e11)=e12)|op1(e11,e11)=e13))&(((op1(e11,e12)=e10|op1(e11,e12)=e11)|op1(e11,e12)=e12)|op1(e11,e12)=e13))&(((op1(e11,e13)=e10|op1(e11,e13)=e11)|op1(e11,e13)=e12)|op1(e11,e13)=e13))&(((op1(e12,e10)=e10|op1(e12,e10)=e11)|op1(e12,e10)=e12)|op1(e12,e10)=e13))&(((op1(e12,e11)=e10|op1(e12,e11)=e11)|op1(e12,e11)=e12)|op1(e12,e11)=e13))&(((op1(e12,e12)=e10|op1(e12,e12)=e11)|op1(e12,e12)=e12)|op1(e12,e12)=e13))&(((op1(e12,e13)=e10|op1(e12,e13)=e11)|op1(e12,e13)=e12)|op1(e12,e13)=e13))&(((op1(e13,e10)=e10|op1(e13,e10)=e11)|op1(e13,e10)=e12)|op1(e13,e10)=e13))&(((op1(e13,e11)=e10|op1(e13,e11)=e11)|op1(e13,e11)=e12)|op1(e13,e11)=e13))&(((op1(e13,e12)=e10|op1(e13,e12)=e11)|op1(e13,e12)=e12)|op1(e13,e12)=e13))&(((op1(e13,e13)=e10|op1(e13,e13)=e11)|op1(e13,e13)=e12)|op1(e13,e13)=e13)),file('/tmp/SRASS.s.p', ax1)).
% fof(2, axiom,((((((((((((((((((((((((((((((((((op1(e10,e10)=e10|op1(e10,e11)=e10)|op1(e10,e12)=e10)|op1(e10,e13)=e10)&(((op1(e10,e10)=e10|op1(e11,e10)=e10)|op1(e12,e10)=e10)|op1(e13,e10)=e10))&(((op1(e10,e10)=e11|op1(e10,e11)=e11)|op1(e10,e12)=e11)|op1(e10,e13)=e11))&(((op1(e10,e10)=e11|op1(e11,e10)=e11)|op1(e12,e10)=e11)|op1(e13,e10)=e11))&(((op1(e10,e10)=e12|op1(e10,e11)=e12)|op1(e10,e12)=e12)|op1(e10,e13)=e12))&(((op1(e10,e10)=e12|op1(e11,e10)=e12)|op1(e12,e10)=e12)|op1(e13,e10)=e12))&(((op1(e10,e10)=e13|op1(e10,e11)=e13)|op1(e10,e12)=e13)|op1(e10,e13)=e13))&(((op1(e10,e10)=e13|op1(e11,e10)=e13)|op1(e12,e10)=e13)|op1(e13,e10)=e13))&(((op1(e11,e10)=e10|op1(e11,e11)=e10)|op1(e11,e12)=e10)|op1(e11,e13)=e10))&(((op1(e10,e11)=e10|op1(e11,e11)=e10)|op1(e12,e11)=e10)|op1(e13,e11)=e10))&(((op1(e11,e10)=e11|op1(e11,e11)=e11)|op1(e11,e12)=e11)|op1(e11,e13)=e11))&(((op1(e10,e11)=e11|op1(e11,e11)=e11)|op1(e12,e11)=e11)|op1(e13,e11)=e11))&(((op1(e11,e10)=e12|op1(e11,e11)=e12)|op1(e11,e12)=e12)|op1(e11,e13)=e12))&(((op1(e10,e11)=e12|op1(e11,e11)=e12)|op1(e12,e11)=e12)|op1(e13,e11)=e12))&(((op1(e11,e10)=e13|op1(e11,e11)=e13)|op1(e11,e12)=e13)|op1(e11,e13)=e13))&(((op1(e10,e11)=e13|op1(e11,e11)=e13)|op1(e12,e11)=e13)|op1(e13,e11)=e13))&(((op1(e12,e10)=e10|op1(e12,e11)=e10)|op1(e12,e12)=e10)|op1(e12,e13)=e10))&(((op1(e10,e12)=e10|op1(e11,e12)=e10)|op1(e12,e12)=e10)|op1(e13,e12)=e10))&(((op1(e12,e10)=e11|op1(e12,e11)=e11)|op1(e12,e12)=e11)|op1(e12,e13)=e11))&(((op1(e10,e12)=e11|op1(e11,e12)=e11)|op1(e12,e12)=e11)|op1(e13,e12)=e11))&(((op1(e12,e10)=e12|op1(e12,e11)=e12)|op1(e12,e12)=e12)|op1(e12,e13)=e12))&(((op1(e10,e12)=e12|op1(e11,e12)=e12)|op1(e12,e12)=e12)|op1(e13,e12)=e12))&(((op1(e12,e10)=e13|op1(e12,e11)=e13)|op1(e12,e12)=e13)|op1(e12,e13)=e13))&(((op1(e10,e12)=e13|op1(e11,e12)=e13)|op1(e12,e12)=e13)|op1(e13,e12)=e13))&(((op1(e13,e10)=e10|op1(e13,e11)=e10)|op1(e13,e12)=e10)|op1(e13,e13)=e10))&(((op1(e10,e13)=e10|op1(e11,e13)=e10)|op1(e12,e13)=e10)|op1(e13,e13)=e10))&(((op1(e13,e10)=e11|op1(e13,e11)=e11)|op1(e13,e12)=e11)|op1(e13,e13)=e11))&(((op1(e10,e13)=e11|op1(e11,e13)=e11)|op1(e12,e13)=e11)|op1(e13,e13)=e11))&(((op1(e13,e10)=e12|op1(e13,e11)=e12)|op1(e13,e12)=e12)|op1(e13,e13)=e12))&(((op1(e10,e13)=e12|op1(e11,e13)=e12)|op1(e12,e13)=e12)|op1(e13,e13)=e12))&(((op1(e13,e10)=e13|op1(e13,e11)=e13)|op1(e13,e12)=e13)|op1(e13,e13)=e13))&(((op1(e10,e13)=e13|op1(e11,e13)=e13)|op1(e12,e13)=e13)|op1(e13,e13)=e13)),file('/tmp/SRASS.s.p', ax2)).
% fof(3, axiom,((((((((((((((((((op2(e20,e20)=e20|op2(e20,e20)=e21)|op2(e20,e20)=e22)|op2(e20,e20)=e23)&(((op2(e20,e21)=e20|op2(e20,e21)=e21)|op2(e20,e21)=e22)|op2(e20,e21)=e23))&(((op2(e20,e22)=e20|op2(e20,e22)=e21)|op2(e20,e22)=e22)|op2(e20,e22)=e23))&(((op2(e20,e23)=e20|op2(e20,e23)=e21)|op2(e20,e23)=e22)|op2(e20,e23)=e23))&(((op2(e21,e20)=e20|op2(e21,e20)=e21)|op2(e21,e20)=e22)|op2(e21,e20)=e23))&(((op2(e21,e21)=e20|op2(e21,e21)=e21)|op2(e21,e21)=e22)|op2(e21,e21)=e23))&(((op2(e21,e22)=e20|op2(e21,e22)=e21)|op2(e21,e22)=e22)|op2(e21,e22)=e23))&(((op2(e21,e23)=e20|op2(e21,e23)=e21)|op2(e21,e23)=e22)|op2(e21,e23)=e23))&(((op2(e22,e20)=e20|op2(e22,e20)=e21)|op2(e22,e20)=e22)|op2(e22,e20)=e23))&(((op2(e22,e21)=e20|op2(e22,e21)=e21)|op2(e22,e21)=e22)|op2(e22,e21)=e23))&(((op2(e22,e22)=e20|op2(e22,e22)=e21)|op2(e22,e22)=e22)|op2(e22,e22)=e23))&(((op2(e22,e23)=e20|op2(e22,e23)=e21)|op2(e22,e23)=e22)|op2(e22,e23)=e23))&(((op2(e23,e20)=e20|op2(e23,e20)=e21)|op2(e23,e20)=e22)|op2(e23,e20)=e23))&(((op2(e23,e21)=e20|op2(e23,e21)=e21)|op2(e23,e21)=e22)|op2(e23,e21)=e23))&(((op2(e23,e22)=e20|op2(e23,e22)=e21)|op2(e23,e22)=e22)|op2(e23,e22)=e23))&(((op2(e23,e23)=e20|op2(e23,e23)=e21)|op2(e23,e23)=e22)|op2(e23,e23)=e23)),file('/tmp/SRASS.s.p', ax3)).
% fof(4, axiom,((((((((((((((((((((((((((((((((((op2(e20,e20)=e20|op2(e20,e21)=e20)|op2(e20,e22)=e20)|op2(e20,e23)=e20)&(((op2(e20,e20)=e20|op2(e21,e20)=e20)|op2(e22,e20)=e20)|op2(e23,e20)=e20))&(((op2(e20,e20)=e21|op2(e20,e21)=e21)|op2(e20,e22)=e21)|op2(e20,e23)=e21))&(((op2(e20,e20)=e21|op2(e21,e20)=e21)|op2(e22,e20)=e21)|op2(e23,e20)=e21))&(((op2(e20,e20)=e22|op2(e20,e21)=e22)|op2(e20,e22)=e22)|op2(e20,e23)=e22))&(((op2(e20,e20)=e22|op2(e21,e20)=e22)|op2(e22,e20)=e22)|op2(e23,e20)=e22))&(((op2(e20,e20)=e23|op2(e20,e21)=e23)|op2(e20,e22)=e23)|op2(e20,e23)=e23))&(((op2(e20,e20)=e23|op2(e21,e20)=e23)|op2(e22,e20)=e23)|op2(e23,e20)=e23))&(((op2(e21,e20)=e20|op2(e21,e21)=e20)|op2(e21,e22)=e20)|op2(e21,e23)=e20))&(((op2(e20,e21)=e20|op2(e21,e21)=e20)|op2(e22,e21)=e20)|op2(e23,e21)=e20))&(((op2(e21,e20)=e21|op2(e21,e21)=e21)|op2(e21,e22)=e21)|op2(e21,e23)=e21))&(((op2(e20,e21)=e21|op2(e21,e21)=e21)|op2(e22,e21)=e21)|op2(e23,e21)=e21))&(((op2(e21,e20)=e22|op2(e21,e21)=e22)|op2(e21,e22)=e22)|op2(e21,e23)=e22))&(((op2(e20,e21)=e22|op2(e21,e21)=e22)|op2(e22,e21)=e22)|op2(e23,e21)=e22))&(((op2(e21,e20)=e23|op2(e21,e21)=e23)|op2(e21,e22)=e23)|op2(e21,e23)=e23))&(((op2(e20,e21)=e23|op2(e21,e21)=e23)|op2(e22,e21)=e23)|op2(e23,e21)=e23))&(((op2(e22,e20)=e20|op2(e22,e21)=e20)|op2(e22,e22)=e20)|op2(e22,e23)=e20))&(((op2(e20,e22)=e20|op2(e21,e22)=e20)|op2(e22,e22)=e20)|op2(e23,e22)=e20))&(((op2(e22,e20)=e21|op2(e22,e21)=e21)|op2(e22,e22)=e21)|op2(e22,e23)=e21))&(((op2(e20,e22)=e21|op2(e21,e22)=e21)|op2(e22,e22)=e21)|op2(e23,e22)=e21))&(((op2(e22,e20)=e22|op2(e22,e21)=e22)|op2(e22,e22)=e22)|op2(e22,e23)=e22))&(((op2(e20,e22)=e22|op2(e21,e22)=e22)|op2(e22,e22)=e22)|op2(e23,e22)=e22))&(((op2(e22,e20)=e23|op2(e22,e21)=e23)|op2(e22,e22)=e23)|op2(e22,e23)=e23))&(((op2(e20,e22)=e23|op2(e21,e22)=e23)|op2(e22,e22)=e23)|op2(e23,e22)=e23))&(((op2(e23,e20)=e20|op2(e23,e21)=e20)|op2(e23,e22)=e20)|op2(e23,e23)=e20))&(((op2(e20,e23)=e20|op2(e21,e23)=e20)|op2(e22,e23)=e20)|op2(e23,e23)=e20))&(((op2(e23,e20)=e21|op2(e23,e21)=e21)|op2(e23,e22)=e21)|op2(e23,e23)=e21))&(((op2(e20,e23)=e21|op2(e21,e23)=e21)|op2(e22,e23)=e21)|op2(e23,e23)=e21))&(((op2(e23,e20)=e22|op2(e23,e21)=e22)|op2(e23,e22)=e22)|op2(e23,e23)=e22))&(((op2(e20,e23)=e22|op2(e21,e23)=e22)|op2(e22,e23)=e22)|op2(e23,e23)=e22))&(((op2(e23,e20)=e23|op2(e23,e21)=e23)|op2(e23,e22)=e23)|op2(e23,e23)=e23))&(((op2(e20,e23)=e23|op2(e21,e23)=e23)|op2(e22,e23)=e23)|op2(e23,e23)=e23)),file('/tmp/SRASS.s.p', ax4)).
% fof(5, axiom,(((((((((((((((((((((((((((((((((((((((((((((((~(op1(e10,e10)=op1(e11,e10))&~(op1(e10,e10)=op1(e12,e10)))&~(op1(e10,e10)=op1(e13,e10)))&~(op1(e11,e10)=op1(e12,e10)))&~(op1(e11,e10)=op1(e13,e10)))&~(op1(e12,e10)=op1(e13,e10)))&~(op1(e10,e11)=op1(e11,e11)))&~(op1(e10,e11)=op1(e12,e11)))&~(op1(e10,e11)=op1(e13,e11)))&~(op1(e11,e11)=op1(e12,e11)))&~(op1(e11,e11)=op1(e13,e11)))&~(op1(e12,e11)=op1(e13,e11)))&~(op1(e10,e12)=op1(e11,e12)))&~(op1(e10,e12)=op1(e12,e12)))&~(op1(e10,e12)=op1(e13,e12)))&~(op1(e11,e12)=op1(e12,e12)))&~(op1(e11,e12)=op1(e13,e12)))&~(op1(e12,e12)=op1(e13,e12)))&~(op1(e10,e13)=op1(e11,e13)))&~(op1(e10,e13)=op1(e12,e13)))&~(op1(e10,e13)=op1(e13,e13)))&~(op1(e11,e13)=op1(e12,e13)))&~(op1(e11,e13)=op1(e13,e13)))&~(op1(e12,e13)=op1(e13,e13)))&~(op1(e10,e10)=op1(e10,e11)))&~(op1(e10,e10)=op1(e10,e12)))&~(op1(e10,e10)=op1(e10,e13)))&~(op1(e10,e11)=op1(e10,e12)))&~(op1(e10,e11)=op1(e10,e13)))&~(op1(e10,e12)=op1(e10,e13)))&~(op1(e11,e10)=op1(e11,e11)))&~(op1(e11,e10)=op1(e11,e12)))&~(op1(e11,e10)=op1(e11,e13)))&~(op1(e11,e11)=op1(e11,e12)))&~(op1(e11,e11)=op1(e11,e13)))&~(op1(e11,e12)=op1(e11,e13)))&~(op1(e12,e10)=op1(e12,e11)))&~(op1(e12,e10)=op1(e12,e12)))&~(op1(e12,e10)=op1(e12,e13)))&~(op1(e12,e11)=op1(e12,e12)))&~(op1(e12,e11)=op1(e12,e13)))&~(op1(e12,e12)=op1(e12,e13)))&~(op1(e13,e10)=op1(e13,e11)))&~(op1(e13,e10)=op1(e13,e12)))&~(op1(e13,e10)=op1(e13,e13)))&~(op1(e13,e11)=op1(e13,e12)))&~(op1(e13,e11)=op1(e13,e13)))&~(op1(e13,e12)=op1(e13,e13))),file('/tmp/SRASS.s.p', ax5)).
% fof(6, axiom,(((((((((((((((((((((((((((((((((((((((((((((((~(op2(e20,e20)=op2(e21,e20))&~(op2(e20,e20)=op2(e22,e20)))&~(op2(e20,e20)=op2(e23,e20)))&~(op2(e21,e20)=op2(e22,e20)))&~(op2(e21,e20)=op2(e23,e20)))&~(op2(e22,e20)=op2(e23,e20)))&~(op2(e20,e21)=op2(e21,e21)))&~(op2(e20,e21)=op2(e22,e21)))&~(op2(e20,e21)=op2(e23,e21)))&~(op2(e21,e21)=op2(e22,e21)))&~(op2(e21,e21)=op2(e23,e21)))&~(op2(e22,e21)=op2(e23,e21)))&~(op2(e20,e22)=op2(e21,e22)))&~(op2(e20,e22)=op2(e22,e22)))&~(op2(e20,e22)=op2(e23,e22)))&~(op2(e21,e22)=op2(e22,e22)))&~(op2(e21,e22)=op2(e23,e22)))&~(op2(e22,e22)=op2(e23,e22)))&~(op2(e20,e23)=op2(e21,e23)))&~(op2(e20,e23)=op2(e22,e23)))&~(op2(e20,e23)=op2(e23,e23)))&~(op2(e21,e23)=op2(e22,e23)))&~(op2(e21,e23)=op2(e23,e23)))&~(op2(e22,e23)=op2(e23,e23)))&~(op2(e20,e20)=op2(e20,e21)))&~(op2(e20,e20)=op2(e20,e22)))&~(op2(e20,e20)=op2(e20,e23)))&~(op2(e20,e21)=op2(e20,e22)))&~(op2(e20,e21)=op2(e20,e23)))&~(op2(e20,e22)=op2(e20,e23)))&~(op2(e21,e20)=op2(e21,e21)))&~(op2(e21,e20)=op2(e21,e22)))&~(op2(e21,e20)=op2(e21,e23)))&~(op2(e21,e21)=op2(e21,e22)))&~(op2(e21,e21)=op2(e21,e23)))&~(op2(e21,e22)=op2(e21,e23)))&~(op2(e22,e20)=op2(e22,e21)))&~(op2(e22,e20)=op2(e22,e22)))&~(op2(e22,e20)=op2(e22,e23)))&~(op2(e22,e21)=op2(e22,e22)))&~(op2(e22,e21)=op2(e22,e23)))&~(op2(e22,e22)=op2(e22,e23)))&~(op2(e23,e20)=op2(e23,e21)))&~(op2(e23,e20)=op2(e23,e22)))&~(op2(e23,e20)=op2(e23,e23)))&~(op2(e23,e21)=op2(e23,e22)))&~(op2(e23,e21)=op2(e23,e23)))&~(op2(e23,e22)=op2(e23,e23))),file('/tmp/SRASS.s.p', ax6)).
% fof(7, axiom,(((((~(e10=e11)&~(e10=e12))&~(e10=e13))&~(e11=e12))&~(e11=e13))&~(e12=e13)),file('/tmp/SRASS.s.p', ax7)).
% fof(8, axiom,(((((~(e20=e21)&~(e20=e22))&~(e20=e23))&~(e21=e22))&~(e21=e23))&~(e22=e23)),file('/tmp/SRASS.s.p', ax8)).
% fof(10, axiom,(((((((op1(e10,e10)=e10&~(op1(e10,e10)=e10))|(op1(e11,e11)=e10&~(op1(e11,e10)=e11)))|(op1(e12,e12)=e10&~(op1(e12,e10)=e12)))|(op1(e13,e13)=e10&~(op1(e13,e10)=e13)))&((((op1(e10,e10)=e11&~(op1(e10,e11)=e10))|(op1(e11,e11)=e11&~(op1(e11,e11)=e11)))|(op1(e12,e12)=e11&~(op1(e12,e11)=e12)))|(op1(e13,e13)=e11&~(op1(e13,e11)=e13))))&((((op1(e10,e10)=e12&~(op1(e10,e12)=e10))|(op1(e11,e11)=e12&~(op1(e11,e12)=e11)))|(op1(e12,e12)=e12&~(op1(e12,e12)=e12)))|(op1(e13,e13)=e12&~(op1(e13,e12)=e13))))&((((op1(e10,e10)=e13&~(op1(e10,e13)=e10))|(op1(e11,e11)=e13&~(op1(e11,e13)=e11)))|(op1(e12,e12)=e13&~(op1(e12,e13)=e12)))|(op1(e13,e13)=e13&~(op1(e13,e13)=e13)))),file('/tmp/SRASS.s.p', ax10)).
% fof(11, axiom,(((((((op2(e20,e20)=e20&~(op2(e20,e20)=e20))|(op2(e21,e21)=e20&~(op2(e21,e20)=e21)))|(op2(e22,e22)=e20&~(op2(e22,e20)=e22)))|(op2(e23,e23)=e20&~(op2(e23,e20)=e23)))&((((op2(e20,e20)=e21&~(op2(e20,e21)=e20))|(op2(e21,e21)=e21&~(op2(e21,e21)=e21)))|(op2(e22,e22)=e21&~(op2(e22,e21)=e22)))|(op2(e23,e23)=e21&~(op2(e23,e21)=e23))))&((((op2(e20,e20)=e22&~(op2(e20,e22)=e20))|(op2(e21,e21)=e22&~(op2(e21,e22)=e21)))|(op2(e22,e22)=e22&~(op2(e22,e22)=e22)))|(op2(e23,e23)=e22&~(op2(e23,e22)=e23))))&((((op2(e20,e20)=e23&~(op2(e20,e23)=e20))|(op2(e21,e21)=e23&~(op2(e21,e23)=e21)))|(op2(e22,e22)=e23&~(op2(e22,e23)=e22)))|(op2(e23,e23)=e23&~(op2(e23,e23)=e23)))),file('/tmp/SRASS.s.p', ax11)).
% fof(12, axiom,((e10=op1(e13,op1(e13,e13))&e11=op1(op1(e13,e13),e13))&e12=op1(e13,e13)),file('/tmp/SRASS.s.p', ax12)).
% fof(13, axiom,((e20=op2(e23,op2(e23,e23))&e21=op2(op2(e23,e23),e23))&e22=op2(e23,e23)),file('/tmp/SRASS.s.p', ax13)).
% fof(17, axiom,(((h4(e13)=e23&h4(e10)=op2(e23,op2(e23,e23)))&h4(e11)=op2(op2(e23,e23),e23))&h4(e12)=op2(e23,e23)),file('/tmp/SRASS.s.p', ax17)).
% fof(18, conjecture,((((((((((((((((((((((h1(op1(e10,e10))=op2(h1(e10),h1(e10))&h1(op1(e10,e11))=op2(h1(e10),h1(e11)))&h1(op1(e10,e12))=op2(h1(e10),h1(e12)))&h1(op1(e10,e13))=op2(h1(e10),h1(e13)))&h1(op1(e11,e10))=op2(h1(e11),h1(e10)))&h1(op1(e11,e11))=op2(h1(e11),h1(e11)))&h1(op1(e11,e12))=op2(h1(e11),h1(e12)))&h1(op1(e11,e13))=op2(h1(e11),h1(e13)))&h1(op1(e12,e10))=op2(h1(e12),h1(e10)))&h1(op1(e12,e11))=op2(h1(e12),h1(e11)))&h1(op1(e12,e12))=op2(h1(e12),h1(e12)))&h1(op1(e12,e13))=op2(h1(e12),h1(e13)))&h1(op1(e13,e10))=op2(h1(e13),h1(e10)))&h1(op1(e13,e11))=op2(h1(e13),h1(e11)))&h1(op1(e13,e12))=op2(h1(e13),h1(e12)))&h1(op1(e13,e13))=op2(h1(e13),h1(e13)))&(((h1(e10)=e20|h1(e11)=e20)|h1(e12)=e20)|h1(e13)=e20))&(((h1(e10)=e21|h1(e11)=e21)|h1(e12)=e21)|h1(e13)=e21))&(((h1(e10)=e22|h1(e11)=e22)|h1(e12)=e22)|h1(e13)=e22))&(((h1(e10)=e23|h1(e11)=e23)|h1(e12)=e23)|h1(e13)=e23))|(((((((((((((((((((h2(op1(e10,e10))=op2(h2(e10),h2(e10))&h2(op1(e10,e11))=op2(h2(e10),h2(e11)))&h2(op1(e10,e12))=op2(h2(e10),h2(e12)))&h2(op1(e10,e13))=op2(h2(e10),h2(e13)))&h2(op1(e11,e10))=op2(h2(e11),h2(e10)))&h2(op1(e11,e11))=op2(h2(e11),h2(e11)))&h2(op1(e11,e12))=op2(h2(e11),h2(e12)))&h2(op1(e11,e13))=op2(h2(e11),h2(e13)))&h2(op1(e12,e10))=op2(h2(e12),h2(e10)))&h2(op1(e12,e11))=op2(h2(e12),h2(e11)))&h2(op1(e12,e12))=op2(h2(e12),h2(e12)))&h2(op1(e12,e13))=op2(h2(e12),h2(e13)))&h2(op1(e13,e10))=op2(h2(e13),h2(e10)))&h2(op1(e13,e11))=op2(h2(e13),h2(e11)))&h2(op1(e13,e12))=op2(h2(e13),h2(e12)))&h2(op1(e13,e13))=op2(h2(e13),h2(e13)))&(((h2(e10)=e20|h2(e11)=e20)|h2(e12)=e20)|h2(e13)=e20))&(((h2(e10)=e21|h2(e11)=e21)|h2(e12)=e21)|h2(e13)=e21))&(((h2(e10)=e22|h2(e11)=e22)|h2(e12)=e22)|h2(e13)=e22))&(((h2(e10)=e23|h2(e11)=e23)|h2(e12)=e23)|h2(e13)=e23)))|(((((((((((((((((((h3(op1(e10,e10))=op2(h3(e10),h3(e10))&h3(op1(e10,e11))=op2(h3(e10),h3(e11)))&h3(op1(e10,e12))=op2(h3(e10),h3(e12)))&h3(op1(e10,e13))=op2(h3(e10),h3(e13)))&h3(op1(e11,e10))=op2(h3(e11),h3(e10)))&h3(op1(e11,e11))=op2(h3(e11),h3(e11)))&h3(op1(e11,e12))=op2(h3(e11),h3(e12)))&h3(op1(e11,e13))=op2(h3(e11),h3(e13)))&h3(op1(e12,e10))=op2(h3(e12),h3(e10)))&h3(op1(e12,e11))=op2(h3(e12),h3(e11)))&h3(op1(e12,e12))=op2(h3(e12),h3(e12)))&h3(op1(e12,e13))=op2(h3(e12),h3(e13)))&h3(op1(e13,e10))=op2(h3(e13),h3(e10)))&h3(op1(e13,e11))=op2(h3(e13),h3(e11)))&h3(op1(e13,e12))=op2(h3(e13),h3(e12)))&h3(op1(e13,e13))=op2(h3(e13),h3(e13)))&(((h3(e10)=e20|h3(e11)=e20)|h3(e12)=e20)|h3(e13)=e20))&(((h3(e10)=e21|h3(e11)=e21)|h3(e12)=e21)|h3(e13)=e21))&(((h3(e10)=e22|h3(e11)=e22)|h3(e12)=e22)|h3(e13)=e22))&(((h3(e10)=e23|h3(e11)=e23)|h3(e12)=e23)|h3(e13)=e23)))|(((((((((((((((((((h4(op1(e10,e10))=op2(h4(e10),h4(e10))&h4(op1(e10,e11))=op2(h4(e10),h4(e11)))&h4(op1(e10,e12))=op2(h4(e10),h4(e12)))&h4(op1(e10,e13))=op2(h4(e10),h4(e13)))&h4(op1(e11,e10))=op2(h4(e11),h4(e10)))&h4(op1(e11,e11))=op2(h4(e11),h4(e11)))&h4(op1(e11,e12))=op2(h4(e11),h4(e12)))&h4(op1(e11,e13))=op2(h4(e11),h4(e13)))&h4(op1(e12,e10))=op2(h4(e12),h4(e10)))&h4(op1(e12,e11))=op2(h4(e12),h4(e11)))&h4(op1(e12,e12))=op2(h4(e12),h4(e12)))&h4(op1(e12,e13))=op2(h4(e12),h4(e13)))&h4(op1(e13,e10))=op2(h4(e13),h4(e10)))&h4(op1(e13,e11))=op2(h4(e13),h4(e11)))&h4(op1(e13,e12))=op2(h4(e13),h4(e12)))&h4(op1(e13,e13))=op2(h4(e13),h4(e13)))&(((h4(e10)=e20|h4(e11)=e20)|h4(e12)=e20)|h4(e13)=e20))&(((h4(e10)=e21|h4(e11)=e21)|h4(e12)=e21)|h4(e13)=e21))&(((h4(e10)=e22|h4(e11)=e22)|h4(e12)=e22)|h4(e13)=e22))&(((h4(e10)=e23|h4(e11)=e23)|h4(e12)=e23)|h4(e13)=e23))),file('/tmp/SRASS.s.p', co1)).
% fof(19, negated_conjecture,~(((((((((((((((((((((((h1(op1(e10,e10))=op2(h1(e10),h1(e10))&h1(op1(e10,e11))=op2(h1(e10),h1(e11)))&h1(op1(e10,e12))=op2(h1(e10),h1(e12)))&h1(op1(e10,e13))=op2(h1(e10),h1(e13)))&h1(op1(e11,e10))=op2(h1(e11),h1(e10)))&h1(op1(e11,e11))=op2(h1(e11),h1(e11)))&h1(op1(e11,e12))=op2(h1(e11),h1(e12)))&h1(op1(e11,e13))=op2(h1(e11),h1(e13)))&h1(op1(e12,e10))=op2(h1(e12),h1(e10)))&h1(op1(e12,e11))=op2(h1(e12),h1(e11)))&h1(op1(e12,e12))=op2(h1(e12),h1(e12)))&h1(op1(e12,e13))=op2(h1(e12),h1(e13)))&h1(op1(e13,e10))=op2(h1(e13),h1(e10)))&h1(op1(e13,e11))=op2(h1(e13),h1(e11)))&h1(op1(e13,e12))=op2(h1(e13),h1(e12)))&h1(op1(e13,e13))=op2(h1(e13),h1(e13)))&(((h1(e10)=e20|h1(e11)=e20)|h1(e12)=e20)|h1(e13)=e20))&(((h1(e10)=e21|h1(e11)=e21)|h1(e12)=e21)|h1(e13)=e21))&(((h1(e10)=e22|h1(e11)=e22)|h1(e12)=e22)|h1(e13)=e22))&(((h1(e10)=e23|h1(e11)=e23)|h1(e12)=e23)|h1(e13)=e23))|(((((((((((((((((((h2(op1(e10,e10))=op2(h2(e10),h2(e10))&h2(op1(e10,e11))=op2(h2(e10),h2(e11)))&h2(op1(e10,e12))=op2(h2(e10),h2(e12)))&h2(op1(e10,e13))=op2(h2(e10),h2(e13)))&h2(op1(e11,e10))=op2(h2(e11),h2(e10)))&h2(op1(e11,e11))=op2(h2(e11),h2(e11)))&h2(op1(e11,e12))=op2(h2(e11),h2(e12)))&h2(op1(e11,e13))=op2(h2(e11),h2(e13)))&h2(op1(e12,e10))=op2(h2(e12),h2(e10)))&h2(op1(e12,e11))=op2(h2(e12),h2(e11)))&h2(op1(e12,e12))=op2(h2(e12),h2(e12)))&h2(op1(e12,e13))=op2(h2(e12),h2(e13)))&h2(op1(e13,e10))=op2(h2(e13),h2(e10)))&h2(op1(e13,e11))=op2(h2(e13),h2(e11)))&h2(op1(e13,e12))=op2(h2(e13),h2(e12)))&h2(op1(e13,e13))=op2(h2(e13),h2(e13)))&(((h2(e10)=e20|h2(e11)=e20)|h2(e12)=e20)|h2(e13)=e20))&(((h2(e10)=e21|h2(e11)=e21)|h2(e12)=e21)|h2(e13)=e21))&(((h2(e10)=e22|h2(e11)=e22)|h2(e12)=e22)|h2(e13)=e22))&(((h2(e10)=e23|h2(e11)=e23)|h2(e12)=e23)|h2(e13)=e23)))|(((((((((((((((((((h3(op1(e10,e10))=op2(h3(e10),h3(e10))&h3(op1(e10,e11))=op2(h3(e10),h3(e11)))&h3(op1(e10,e12))=op2(h3(e10),h3(e12)))&h3(op1(e10,e13))=op2(h3(e10),h3(e13)))&h3(op1(e11,e10))=op2(h3(e11),h3(e10)))&h3(op1(e11,e11))=op2(h3(e11),h3(e11)))&h3(op1(e11,e12))=op2(h3(e11),h3(e12)))&h3(op1(e11,e13))=op2(h3(e11),h3(e13)))&h3(op1(e12,e10))=op2(h3(e12),h3(e10)))&h3(op1(e12,e11))=op2(h3(e12),h3(e11)))&h3(op1(e12,e12))=op2(h3(e12),h3(e12)))&h3(op1(e12,e13))=op2(h3(e12),h3(e13)))&h3(op1(e13,e10))=op2(h3(e13),h3(e10)))&h3(op1(e13,e11))=op2(h3(e13),h3(e11)))&h3(op1(e13,e12))=op2(h3(e13),h3(e12)))&h3(op1(e13,e13))=op2(h3(e13),h3(e13)))&(((h3(e10)=e20|h3(e11)=e20)|h3(e12)=e20)|h3(e13)=e20))&(((h3(e10)=e21|h3(e11)=e21)|h3(e12)=e21)|h3(e13)=e21))&(((h3(e10)=e22|h3(e11)=e22)|h3(e12)=e22)|h3(e13)=e22))&(((h3(e10)=e23|h3(e11)=e23)|h3(e12)=e23)|h3(e13)=e23)))|(((((((((((((((((((h4(op1(e10,e10))=op2(h4(e10),h4(e10))&h4(op1(e10,e11))=op2(h4(e10),h4(e11)))&h4(op1(e10,e12))=op2(h4(e10),h4(e12)))&h4(op1(e10,e13))=op2(h4(e10),h4(e13)))&h4(op1(e11,e10))=op2(h4(e11),h4(e10)))&h4(op1(e11,e11))=op2(h4(e11),h4(e11)))&h4(op1(e11,e12))=op2(h4(e11),h4(e12)))&h4(op1(e11,e13))=op2(h4(e11),h4(e13)))&h4(op1(e12,e10))=op2(h4(e12),h4(e10)))&h4(op1(e12,e11))=op2(h4(e12),h4(e11)))&h4(op1(e12,e12))=op2(h4(e12),h4(e12)))&h4(op1(e12,e13))=op2(h4(e12),h4(e13)))&h4(op1(e13,e10))=op2(h4(e13),h4(e10)))&h4(op1(e13,e11))=op2(h4(e13),h4(e11)))&h4(op1(e13,e12))=op2(h4(e13),h4(e12)))&h4(op1(e13,e13))=op2(h4(e13),h4(e13)))&(((h4(e10)=e20|h4(e11)=e20)|h4(e12)=e20)|h4(e13)=e20))&(((h4(e10)=e21|h4(e11)=e21)|h4(e12)=e21)|h4(e13)=e21))&(((h4(e10)=e22|h4(e11)=e22)|h4(e12)=e22)|h4(e13)=e22))&(((h4(e10)=e23|h4(e11)=e23)|h4(e12)=e23)|h4(e13)=e23)))),inference(assume_negation,[status(cth)],[18])).
% fof(20, plain,(((((((((((((((((((h1(op1(e10,e10))=op2(h1(e10),h1(e10))&h1(op1(e10,e11))=op2(h1(e10),h1(e11)))&h1(op1(e10,e12))=op2(h1(e10),h1(e12)))&h1(op1(e10,e13))=op2(h1(e10),h1(e13)))&h1(op1(e11,e10))=op2(h1(e11),h1(e10)))&h1(op1(e11,e11))=op2(h1(e11),h1(e11)))&h1(op1(e11,e12))=op2(h1(e11),h1(e12)))&h1(op1(e11,e13))=op2(h1(e11),h1(e13)))&h1(op1(e12,e10))=op2(h1(e12),h1(e10)))&h1(op1(e12,e11))=op2(h1(e12),h1(e11)))&h1(op1(e12,e12))=op2(h1(e12),h1(e12)))&h1(op1(e12,e13))=op2(h1(e12),h1(e13)))&h1(op1(e13,e10))=op2(h1(e13),h1(e10)))&h1(op1(e13,e11))=op2(h1(e13),h1(e11)))&h1(op1(e13,e12))=op2(h1(e13),h1(e12)))&h1(op1(e13,e13))=op2(h1(e13),h1(e13)))&(((h1(e10)=e20|h1(e11)=e20)|h1(e12)=e20)|h1(e13)=e20))&(((h1(e10)=e21|h1(e11)=e21)|h1(e12)=e21)|h1(e13)=e21))&(((h1(e10)=e22|h1(e11)=e22)|h1(e12)=e22)|h1(e13)=e22))=>epred1_0),introduced(definition)).
% fof(21, plain,(((((((((((((((((((h2(op1(e10,e10))=op2(h2(e10),h2(e10))&h2(op1(e10,e11))=op2(h2(e10),h2(e11)))&h2(op1(e10,e12))=op2(h2(e10),h2(e12)))&h2(op1(e10,e13))=op2(h2(e10),h2(e13)))&h2(op1(e11,e10))=op2(h2(e11),h2(e10)))&h2(op1(e11,e11))=op2(h2(e11),h2(e11)))&h2(op1(e11,e12))=op2(h2(e11),h2(e12)))&h2(op1(e11,e13))=op2(h2(e11),h2(e13)))&h2(op1(e12,e10))=op2(h2(e12),h2(e10)))&h2(op1(e12,e11))=op2(h2(e12),h2(e11)))&h2(op1(e12,e12))=op2(h2(e12),h2(e12)))&h2(op1(e12,e13))=op2(h2(e12),h2(e13)))&h2(op1(e13,e10))=op2(h2(e13),h2(e10)))&h2(op1(e13,e11))=op2(h2(e13),h2(e11)))&h2(op1(e13,e12))=op2(h2(e13),h2(e12)))&h2(op1(e13,e13))=op2(h2(e13),h2(e13)))&(((h2(e10)=e20|h2(e11)=e20)|h2(e12)=e20)|h2(e13)=e20))&(((h2(e10)=e21|h2(e11)=e21)|h2(e12)=e21)|h2(e13)=e21))&(((h2(e10)=e22|h2(e11)=e22)|h2(e12)=e22)|h2(e13)=e22))=>epred2_0),introduced(definition)).
% fof(22, plain,(((((((((((((((((((h3(op1(e10,e10))=op2(h3(e10),h3(e10))&h3(op1(e10,e11))=op2(h3(e10),h3(e11)))&h3(op1(e10,e12))=op2(h3(e10),h3(e12)))&h3(op1(e10,e13))=op2(h3(e10),h3(e13)))&h3(op1(e11,e10))=op2(h3(e11),h3(e10)))&h3(op1(e11,e11))=op2(h3(e11),h3(e11)))&h3(op1(e11,e12))=op2(h3(e11),h3(e12)))&h3(op1(e11,e13))=op2(h3(e11),h3(e13)))&h3(op1(e12,e10))=op2(h3(e12),h3(e10)))&h3(op1(e12,e11))=op2(h3(e12),h3(e11)))&h3(op1(e12,e12))=op2(h3(e12),h3(e12)))&h3(op1(e12,e13))=op2(h3(e12),h3(e13)))&h3(op1(e13,e10))=op2(h3(e13),h3(e10)))&h3(op1(e13,e11))=op2(h3(e13),h3(e11)))&h3(op1(e13,e12))=op2(h3(e13),h3(e12)))&h3(op1(e13,e13))=op2(h3(e13),h3(e13)))&(((h3(e10)=e20|h3(e11)=e20)|h3(e12)=e20)|h3(e13)=e20))&(((h3(e10)=e21|h3(e11)=e21)|h3(e12)=e21)|h3(e13)=e21))&(((h3(e10)=e22|h3(e11)=e22)|h3(e12)=e22)|h3(e13)=e22))=>epred3_0),introduced(definition)).
% fof(23, plain,(((((((((((((((((((h4(op1(e10,e10))=op2(h4(e10),h4(e10))&h4(op1(e10,e11))=op2(h4(e10),h4(e11)))&h4(op1(e10,e12))=op2(h4(e10),h4(e12)))&h4(op1(e10,e13))=op2(h4(e10),h4(e13)))&h4(op1(e11,e10))=op2(h4(e11),h4(e10)))&h4(op1(e11,e11))=op2(h4(e11),h4(e11)))&h4(op1(e11,e12))=op2(h4(e11),h4(e12)))&h4(op1(e11,e13))=op2(h4(e11),h4(e13)))&h4(op1(e12,e10))=op2(h4(e12),h4(e10)))&h4(op1(e12,e11))=op2(h4(e12),h4(e11)))&h4(op1(e12,e12))=op2(h4(e12),h4(e12)))&h4(op1(e12,e13))=op2(h4(e12),h4(e13)))&h4(op1(e13,e10))=op2(h4(e13),h4(e10)))&h4(op1(e13,e11))=op2(h4(e13),h4(e11)))&h4(op1(e13,e12))=op2(h4(e13),h4(e12)))&h4(op1(e13,e13))=op2(h4(e13),h4(e13)))&(((h4(e10)=e20|h4(e11)=e20)|h4(e12)=e20)|h4(e13)=e20))&(((h4(e10)=e21|h4(e11)=e21)|h4(e12)=e21)|h4(e13)=e21))&(((h4(e10)=e22|h4(e11)=e22)|h4(e12)=e22)|h4(e13)=e22))=>epred4_0),introduced(definition)).
% fof(24, negated_conjecture,~(((((epred1_0&(((h1(e10)=e23|h1(e11)=e23)|h1(e12)=e23)|h1(e13)=e23))|(epred2_0&(((h2(e10)=e23|h2(e11)=e23)|h2(e12)=e23)|h2(e13)=e23)))|(epred3_0&(((h3(e10)=e23|h3(e11)=e23)|h3(e12)=e23)|h3(e13)=e23)))|(epred4_0&(((h4(e10)=e23|h4(e11)=e23)|h4(e12)=e23)|h4(e13)=e23)))),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[19,20,theory(equality)]),21,theory(equality)]),22,theory(equality)]),23,theory(equality)])).
% cnf(28,plain,(op1(e13,e10)=e13|op1(e13,e10)=e12|op1(e13,e10)=e11|op1(e13,e10)=e10),inference(split_conjunct,[status(thm)],[1])).
% cnf(41,plain,(op1(e13,e13)=e13|op1(e12,e13)=e13|op1(e11,e13)=e13|op1(e10,e13)=e13),inference(split_conjunct,[status(thm)],[2])).
% cnf(46,plain,(op1(e13,e13)=e11|op1(e13,e12)=e11|op1(e13,e11)=e11|op1(e13,e10)=e11),inference(split_conjunct,[status(thm)],[2])).
% cnf(51,plain,(op1(e13,e12)=e12|op1(e12,e12)=e12|op1(e11,e12)=e12|op1(e10,e12)=e12),inference(split_conjunct,[status(thm)],[2])).
% cnf(52,plain,(op1(e12,e13)=e12|op1(e12,e12)=e12|op1(e12,e11)=e12|op1(e12,e10)=e12),inference(split_conjunct,[status(thm)],[2])).
% cnf(57,plain,(op1(e13,e11)=e13|op1(e12,e11)=e13|op1(e11,e11)=e13|op1(e10,e11)=e13),inference(split_conjunct,[status(thm)],[2])).
% cnf(60,plain,(op1(e11,e13)=e12|op1(e11,e12)=e12|op1(e11,e11)=e12|op1(e11,e10)=e12),inference(split_conjunct,[status(thm)],[2])).
% cnf(62,plain,(op1(e11,e13)=e11|op1(e11,e12)=e11|op1(e11,e11)=e11|op1(e11,e10)=e11),inference(split_conjunct,[status(thm)],[2])).
% cnf(71,plain,(op1(e13,e10)=e10|op1(e12,e10)=e10|op1(e11,e10)=e10|op1(e10,e10)=e10),inference(split_conjunct,[status(thm)],[2])).
% cnf(72,plain,(op1(e10,e13)=e10|op1(e10,e12)=e10|op1(e10,e11)=e10|op1(e10,e10)=e10),inference(split_conjunct,[status(thm)],[2])).
% cnf(76,plain,(op2(e23,e20)=e23|op2(e23,e20)=e22|op2(e23,e20)=e21|op2(e23,e20)=e20),inference(split_conjunct,[status(thm)],[3])).
% cnf(84,plain,(op2(e21,e20)=e23|op2(e21,e20)=e22|op2(e21,e20)=e21|op2(e21,e20)=e20),inference(split_conjunct,[status(thm)],[3])).
% cnf(89,plain,(op2(e23,e23)=e23|op2(e22,e23)=e23|op2(e21,e23)=e23|op2(e20,e23)=e23),inference(split_conjunct,[status(thm)],[4])).
% cnf(94,plain,(op2(e23,e23)=e21|op2(e23,e22)=e21|op2(e23,e21)=e21|op2(e23,e20)=e21),inference(split_conjunct,[status(thm)],[4])).
% cnf(99,plain,(op2(e23,e22)=e22|op2(e22,e22)=e22|op2(e21,e22)=e22|op2(e20,e22)=e22),inference(split_conjunct,[status(thm)],[4])).
% cnf(100,plain,(op2(e22,e23)=e22|op2(e22,e22)=e22|op2(e22,e21)=e22|op2(e22,e20)=e22),inference(split_conjunct,[status(thm)],[4])).
% cnf(104,plain,(op2(e22,e23)=e20|op2(e22,e22)=e20|op2(e22,e21)=e20|op2(e22,e20)=e20),inference(split_conjunct,[status(thm)],[4])).
% cnf(110,plain,(op2(e21,e23)=e21|op2(e21,e22)=e21|op2(e21,e21)=e21|op2(e21,e20)=e21),inference(split_conjunct,[status(thm)],[4])).
% cnf(114,plain,(op2(e20,e23)=e23|op2(e20,e22)=e23|op2(e20,e21)=e23|op2(e20,e20)=e23),inference(split_conjunct,[status(thm)],[4])).
% cnf(120,plain,(op2(e20,e23)=e20|op2(e20,e22)=e20|op2(e20,e21)=e20|op2(e20,e20)=e20),inference(split_conjunct,[status(thm)],[4])).
% cnf(124,plain,(op1(e13,e10)!=op1(e13,e13)),inference(split_conjunct,[status(thm)],[5])).
% cnf(125,plain,(op1(e13,e10)!=op1(e13,e12)),inference(split_conjunct,[status(thm)],[5])).
% cnf(127,plain,(op1(e12,e12)!=op1(e12,e13)),inference(split_conjunct,[status(thm)],[5])).
% cnf(146,plain,(op1(e11,e13)!=op1(e13,e13)),inference(split_conjunct,[status(thm)],[5])).
% cnf(147,plain,(op1(e11,e13)!=op1(e12,e13)),inference(split_conjunct,[status(thm)],[5])).
% cnf(151,plain,(op1(e12,e12)!=op1(e13,e12)),inference(split_conjunct,[status(thm)],[5])).
% cnf(154,plain,(op1(e10,e12)!=op1(e13,e12)),inference(split_conjunct,[status(thm)],[5])).
% cnf(166,plain,(op1(e10,e10)!=op1(e13,e10)),inference(split_conjunct,[status(thm)],[5])).
% cnf(172,plain,(op2(e23,e20)!=op2(e23,e23)),inference(split_conjunct,[status(thm)],[6])).
% cnf(173,plain,(op2(e23,e20)!=op2(e23,e22)),inference(split_conjunct,[status(thm)],[6])).
% cnf(175,plain,(op2(e22,e22)!=op2(e22,e23)),inference(split_conjunct,[status(thm)],[6])).
% cnf(186,plain,(op2(e21,e20)!=op2(e21,e21)),inference(split_conjunct,[status(thm)],[6])).
% cnf(195,plain,(op2(e21,e23)!=op2(e22,e23)),inference(split_conjunct,[status(thm)],[6])).
% cnf(199,plain,(op2(e22,e22)!=op2(e23,e22)),inference(split_conjunct,[status(thm)],[6])).
% cnf(202,plain,(op2(e20,e22)!=op2(e23,e22)),inference(split_conjunct,[status(thm)],[6])).
% cnf(207,plain,(op2(e21,e21)!=op2(e22,e21)),inference(split_conjunct,[status(thm)],[6])).
% cnf(212,plain,(op2(e21,e20)!=op2(e23,e20)),inference(split_conjunct,[status(thm)],[6])).
% cnf(214,plain,(op2(e20,e20)!=op2(e23,e20)),inference(split_conjunct,[status(thm)],[6])).
% cnf(217,plain,(e12!=e13),inference(split_conjunct,[status(thm)],[7])).
% cnf(218,plain,(e11!=e13),inference(split_conjunct,[status(thm)],[7])).
% cnf(219,plain,(e11!=e12),inference(split_conjunct,[status(thm)],[7])).
% cnf(220,plain,(e10!=e13),inference(split_conjunct,[status(thm)],[7])).
% cnf(221,plain,(e10!=e12),inference(split_conjunct,[status(thm)],[7])).
% cnf(222,plain,(e10!=e11),inference(split_conjunct,[status(thm)],[7])).
% cnf(223,plain,(e22!=e23),inference(split_conjunct,[status(thm)],[8])).
% cnf(224,plain,(e21!=e23),inference(split_conjunct,[status(thm)],[8])).
% cnf(225,plain,(e21!=e22),inference(split_conjunct,[status(thm)],[8])).
% cnf(226,plain,(e20!=e23),inference(split_conjunct,[status(thm)],[8])).
% cnf(227,plain,(e20!=e22),inference(split_conjunct,[status(thm)],[8])).
% cnf(228,plain,(e20!=e21),inference(split_conjunct,[status(thm)],[8])).
% fof(245, plain,((((((((op1(e13,e13)=e10|(op1(e12,e12)=e10|(op1(e11,e11)=e10|op1(e10,e10)=e10)))&(~(op1(e13,e10)=e13)|(op1(e12,e12)=e10|(op1(e11,e11)=e10|op1(e10,e10)=e10))))&((op1(e13,e13)=e10|(~(op1(e12,e10)=e12)|(op1(e11,e11)=e10|op1(e10,e10)=e10)))&(~(op1(e13,e10)=e13)|(~(op1(e12,e10)=e12)|(op1(e11,e11)=e10|op1(e10,e10)=e10)))))&(((op1(e13,e13)=e10|(op1(e12,e12)=e10|(~(op1(e11,e10)=e11)|op1(e10,e10)=e10)))&(~(op1(e13,e10)=e13)|(op1(e12,e12)=e10|(~(op1(e11,e10)=e11)|op1(e10,e10)=e10))))&((op1(e13,e13)=e10|(~(op1(e12,e10)=e12)|(~(op1(e11,e10)=e11)|op1(e10,e10)=e10)))&(~(op1(e13,e10)=e13)|(~(op1(e12,e10)=e12)|(~(op1(e11,e10)=e11)|op1(e10,e10)=e10))))))&((((op1(e13,e13)=e10|(op1(e12,e12)=e10|(op1(e11,e11)=e10|~(op1(e10,e10)=e10))))&(~(op1(e13,e10)=e13)|(op1(e12,e12)=e10|(op1(e11,e11)=e10|~(op1(e10,e10)=e10)))))&((op1(e13,e13)=e10|(~(op1(e12,e10)=e12)|(op1(e11,e11)=e10|~(op1(e10,e10)=e10))))&(~(op1(e13,e10)=e13)|(~(op1(e12,e10)=e12)|(op1(e11,e11)=e10|~(op1(e10,e10)=e10))))))&(((op1(e13,e13)=e10|(op1(e12,e12)=e10|(~(op1(e11,e10)=e11)|~(op1(e10,e10)=e10))))&(~(op1(e13,e10)=e13)|(op1(e12,e12)=e10|(~(op1(e11,e10)=e11)|~(op1(e10,e10)=e10)))))&((op1(e13,e13)=e10|(~(op1(e12,e10)=e12)|(~(op1(e11,e10)=e11)|~(op1(e10,e10)=e10))))&(~(op1(e13,e10)=e13)|(~(op1(e12,e10)=e12)|(~(op1(e11,e10)=e11)|~(op1(e10,e10)=e10))))))))&(((((op1(e13,e13)=e11|(op1(e12,e12)=e11|(op1(e11,e11)=e11|op1(e10,e10)=e11)))&(~(op1(e13,e11)=e13)|(op1(e12,e12)=e11|(op1(e11,e11)=e11|op1(e10,e10)=e11))))&((op1(e13,e13)=e11|(~(op1(e12,e11)=e12)|(op1(e11,e11)=e11|op1(e10,e10)=e11)))&(~(op1(e13,e11)=e13)|(~(op1(e12,e11)=e12)|(op1(e11,e11)=e11|op1(e10,e10)=e11)))))&(((op1(e13,e13)=e11|(op1(e12,e12)=e11|(~(op1(e11,e11)=e11)|op1(e10,e10)=e11)))&(~(op1(e13,e11)=e13)|(op1(e12,e12)=e11|(~(op1(e11,e11)=e11)|op1(e10,e10)=e11))))&((op1(e13,e13)=e11|(~(op1(e12,e11)=e12)|(~(op1(e11,e11)=e11)|op1(e10,e10)=e11)))&(~(op1(e13,e11)=e13)|(~(op1(e12,e11)=e12)|(~(op1(e11,e11)=e11)|op1(e10,e10)=e11))))))&((((op1(e13,e13)=e11|(op1(e12,e12)=e11|(op1(e11,e11)=e11|~(op1(e10,e11)=e10))))&(~(op1(e13,e11)=e13)|(op1(e12,e12)=e11|(op1(e11,e11)=e11|~(op1(e10,e11)=e10)))))&((op1(e13,e13)=e11|(~(op1(e12,e11)=e12)|(op1(e11,e11)=e11|~(op1(e10,e11)=e10))))&(~(op1(e13,e11)=e13)|(~(op1(e12,e11)=e12)|(op1(e11,e11)=e11|~(op1(e10,e11)=e10))))))&(((op1(e13,e13)=e11|(op1(e12,e12)=e11|(~(op1(e11,e11)=e11)|~(op1(e10,e11)=e10))))&(~(op1(e13,e11)=e13)|(op1(e12,e12)=e11|(~(op1(e11,e11)=e11)|~(op1(e10,e11)=e10)))))&((op1(e13,e13)=e11|(~(op1(e12,e11)=e12)|(~(op1(e11,e11)=e11)|~(op1(e10,e11)=e10))))&(~(op1(e13,e11)=e13)|(~(op1(e12,e11)=e12)|(~(op1(e11,e11)=e11)|~(op1(e10,e11)=e10)))))))))&(((((op1(e13,e13)=e12|(op1(e12,e12)=e12|(op1(e11,e11)=e12|op1(e10,e10)=e12)))&(~(op1(e13,e12)=e13)|(op1(e12,e12)=e12|(op1(e11,e11)=e12|op1(e10,e10)=e12))))&((op1(e13,e13)=e12|(~(op1(e12,e12)=e12)|(op1(e11,e11)=e12|op1(e10,e10)=e12)))&(~(op1(e13,e12)=e13)|(~(op1(e12,e12)=e12)|(op1(e11,e11)=e12|op1(e10,e10)=e12)))))&(((op1(e13,e13)=e12|(op1(e12,e12)=e12|(~(op1(e11,e12)=e11)|op1(e10,e10)=e12)))&(~(op1(e13,e12)=e13)|(op1(e12,e12)=e12|(~(op1(e11,e12)=e11)|op1(e10,e10)=e12))))&((op1(e13,e13)=e12|(~(op1(e12,e12)=e12)|(~(op1(e11,e12)=e11)|op1(e10,e10)=e12)))&(~(op1(e13,e12)=e13)|(~(op1(e12,e12)=e12)|(~(op1(e11,e12)=e11)|op1(e10,e10)=e12))))))&((((op1(e13,e13)=e12|(op1(e12,e12)=e12|(op1(e11,e11)=e12|~(op1(e10,e12)=e10))))&(~(op1(e13,e12)=e13)|(op1(e12,e12)=e12|(op1(e11,e11)=e12|~(op1(e10,e12)=e10)))))&((op1(e13,e13)=e12|(~(op1(e12,e12)=e12)|(op1(e11,e11)=e12|~(op1(e10,e12)=e10))))&(~(op1(e13,e12)=e13)|(~(op1(e12,e12)=e12)|(op1(e11,e11)=e12|~(op1(e10,e12)=e10))))))&(((op1(e13,e13)=e12|(op1(e12,e12)=e12|(~(op1(e11,e12)=e11)|~(op1(e10,e12)=e10))))&(~(op1(e13,e12)=e13)|(op1(e12,e12)=e12|(~(op1(e11,e12)=e11)|~(op1(e10,e12)=e10)))))&((op1(e13,e13)=e12|(~(op1(e12,e12)=e12)|(~(op1(e11,e12)=e11)|~(op1(e10,e12)=e10))))&(~(op1(e13,e12)=e13)|(~(op1(e12,e12)=e12)|(~(op1(e11,e12)=e11)|~(op1(e10,e12)=e10)))))))))&(((((op1(e13,e13)=e13|(op1(e12,e12)=e13|(op1(e11,e11)=e13|op1(e10,e10)=e13)))&(~(op1(e13,e13)=e13)|(op1(e12,e12)=e13|(op1(e11,e11)=e13|op1(e10,e10)=e13))))&((op1(e13,e13)=e13|(~(op1(e12,e13)=e12)|(op1(e11,e11)=e13|op1(e10,e10)=e13)))&(~(op1(e13,e13)=e13)|(~(op1(e12,e13)=e12)|(op1(e11,e11)=e13|op1(e10,e10)=e13)))))&(((op1(e13,e13)=e13|(op1(e12,e12)=e13|(~(op1(e11,e13)=e11)|op1(e10,e10)=e13)))&(~(op1(e13,e13)=e13)|(op1(e12,e12)=e13|(~(op1(e11,e13)=e11)|op1(e10,e10)=e13))))&((op1(e13,e13)=e13|(~(op1(e12,e13)=e12)|(~(op1(e11,e13)=e11)|op1(e10,e10)=e13)))&(~(op1(e13,e13)=e13)|(~(op1(e12,e13)=e12)|(~(op1(e11,e13)=e11)|op1(e10,e10)=e13))))))&((((op1(e13,e13)=e13|(op1(e12,e12)=e13|(op1(e11,e11)=e13|~(op1(e10,e13)=e10))))&(~(op1(e13,e13)=e13)|(op1(e12,e12)=e13|(op1(e11,e11)=e13|~(op1(e10,e13)=e10)))))&((op1(e13,e13)=e13|(~(op1(e12,e13)=e12)|(op1(e11,e11)=e13|~(op1(e10,e13)=e10))))&(~(op1(e13,e13)=e13)|(~(op1(e12,e13)=e12)|(op1(e11,e11)=e13|~(op1(e10,e13)=e10))))))&(((op1(e13,e13)=e13|(op1(e12,e12)=e13|(~(op1(e11,e13)=e11)|~(op1(e10,e13)=e10))))&(~(op1(e13,e13)=e13)|(op1(e12,e12)=e13|(~(op1(e11,e13)=e11)|~(op1(e10,e13)=e10)))))&((op1(e13,e13)=e13|(~(op1(e12,e13)=e12)|(~(op1(e11,e13)=e11)|~(op1(e10,e13)=e10))))&(~(op1(e13,e13)=e13)|(~(op1(e12,e13)=e12)|(~(op1(e11,e13)=e11)|~(op1(e10,e13)=e10))))))))),inference(distribute,[status(thm)],[10])).
% cnf(253,plain,(op1(e11,e11)=e13|op1(e12,e12)=e13|op1(e13,e13)=e13|op1(e10,e13)!=e10),inference(split_conjunct,[status(thm)],[245])).
% cnf(281,plain,(op1(e12,e12)=e11|op1(e13,e13)=e11|op1(e10,e11)!=e10|op1(e11,e11)!=e11),inference(split_conjunct,[status(thm)],[245])).
% cnf(285,plain,(op1(e11,e11)=e11|op1(e12,e12)=e11|op1(e13,e13)=e11|op1(e10,e11)!=e10),inference(split_conjunct,[status(thm)],[245])).
% cnf(289,plain,(op1(e10,e10)=e11|op1(e12,e12)=e11|op1(e13,e13)=e11|op1(e11,e11)!=e11),inference(split_conjunct,[status(thm)],[245])).
% cnf(293,plain,(op1(e10,e10)=e11|op1(e11,e11)=e11|op1(e12,e12)=e11|op1(e13,e13)=e11),inference(split_conjunct,[status(thm)],[245])).
% cnf(297,plain,(op1(e12,e12)=e10|op1(e13,e13)=e10|op1(e10,e10)!=e10|op1(e11,e10)!=e11),inference(split_conjunct,[status(thm)],[245])).
% cnf(305,plain,(op1(e10,e10)=e10|op1(e12,e12)=e10|op1(e13,e13)=e10|op1(e11,e10)!=e11),inference(split_conjunct,[status(thm)],[245])).
% cnf(309,plain,(op1(e10,e10)=e10|op1(e11,e11)=e10|op1(e12,e12)=e10|op1(e13,e13)=e10),inference(split_conjunct,[status(thm)],[245])).
% fof(310, plain,((((((((op2(e23,e23)=e20|(op2(e22,e22)=e20|(op2(e21,e21)=e20|op2(e20,e20)=e20)))&(~(op2(e23,e20)=e23)|(op2(e22,e22)=e20|(op2(e21,e21)=e20|op2(e20,e20)=e20))))&((op2(e23,e23)=e20|(~(op2(e22,e20)=e22)|(op2(e21,e21)=e20|op2(e20,e20)=e20)))&(~(op2(e23,e20)=e23)|(~(op2(e22,e20)=e22)|(op2(e21,e21)=e20|op2(e20,e20)=e20)))))&(((op2(e23,e23)=e20|(op2(e22,e22)=e20|(~(op2(e21,e20)=e21)|op2(e20,e20)=e20)))&(~(op2(e23,e20)=e23)|(op2(e22,e22)=e20|(~(op2(e21,e20)=e21)|op2(e20,e20)=e20))))&((op2(e23,e23)=e20|(~(op2(e22,e20)=e22)|(~(op2(e21,e20)=e21)|op2(e20,e20)=e20)))&(~(op2(e23,e20)=e23)|(~(op2(e22,e20)=e22)|(~(op2(e21,e20)=e21)|op2(e20,e20)=e20))))))&((((op2(e23,e23)=e20|(op2(e22,e22)=e20|(op2(e21,e21)=e20|~(op2(e20,e20)=e20))))&(~(op2(e23,e20)=e23)|(op2(e22,e22)=e20|(op2(e21,e21)=e20|~(op2(e20,e20)=e20)))))&((op2(e23,e23)=e20|(~(op2(e22,e20)=e22)|(op2(e21,e21)=e20|~(op2(e20,e20)=e20))))&(~(op2(e23,e20)=e23)|(~(op2(e22,e20)=e22)|(op2(e21,e21)=e20|~(op2(e20,e20)=e20))))))&(((op2(e23,e23)=e20|(op2(e22,e22)=e20|(~(op2(e21,e20)=e21)|~(op2(e20,e20)=e20))))&(~(op2(e23,e20)=e23)|(op2(e22,e22)=e20|(~(op2(e21,e20)=e21)|~(op2(e20,e20)=e20)))))&((op2(e23,e23)=e20|(~(op2(e22,e20)=e22)|(~(op2(e21,e20)=e21)|~(op2(e20,e20)=e20))))&(~(op2(e23,e20)=e23)|(~(op2(e22,e20)=e22)|(~(op2(e21,e20)=e21)|~(op2(e20,e20)=e20))))))))&(((((op2(e23,e23)=e21|(op2(e22,e22)=e21|(op2(e21,e21)=e21|op2(e20,e20)=e21)))&(~(op2(e23,e21)=e23)|(op2(e22,e22)=e21|(op2(e21,e21)=e21|op2(e20,e20)=e21))))&((op2(e23,e23)=e21|(~(op2(e22,e21)=e22)|(op2(e21,e21)=e21|op2(e20,e20)=e21)))&(~(op2(e23,e21)=e23)|(~(op2(e22,e21)=e22)|(op2(e21,e21)=e21|op2(e20,e20)=e21)))))&(((op2(e23,e23)=e21|(op2(e22,e22)=e21|(~(op2(e21,e21)=e21)|op2(e20,e20)=e21)))&(~(op2(e23,e21)=e23)|(op2(e22,e22)=e21|(~(op2(e21,e21)=e21)|op2(e20,e20)=e21))))&((op2(e23,e23)=e21|(~(op2(e22,e21)=e22)|(~(op2(e21,e21)=e21)|op2(e20,e20)=e21)))&(~(op2(e23,e21)=e23)|(~(op2(e22,e21)=e22)|(~(op2(e21,e21)=e21)|op2(e20,e20)=e21))))))&((((op2(e23,e23)=e21|(op2(e22,e22)=e21|(op2(e21,e21)=e21|~(op2(e20,e21)=e20))))&(~(op2(e23,e21)=e23)|(op2(e22,e22)=e21|(op2(e21,e21)=e21|~(op2(e20,e21)=e20)))))&((op2(e23,e23)=e21|(~(op2(e22,e21)=e22)|(op2(e21,e21)=e21|~(op2(e20,e21)=e20))))&(~(op2(e23,e21)=e23)|(~(op2(e22,e21)=e22)|(op2(e21,e21)=e21|~(op2(e20,e21)=e20))))))&(((op2(e23,e23)=e21|(op2(e22,e22)=e21|(~(op2(e21,e21)=e21)|~(op2(e20,e21)=e20))))&(~(op2(e23,e21)=e23)|(op2(e22,e22)=e21|(~(op2(e21,e21)=e21)|~(op2(e20,e21)=e20)))))&((op2(e23,e23)=e21|(~(op2(e22,e21)=e22)|(~(op2(e21,e21)=e21)|~(op2(e20,e21)=e20))))&(~(op2(e23,e21)=e23)|(~(op2(e22,e21)=e22)|(~(op2(e21,e21)=e21)|~(op2(e20,e21)=e20)))))))))&(((((op2(e23,e23)=e22|(op2(e22,e22)=e22|(op2(e21,e21)=e22|op2(e20,e20)=e22)))&(~(op2(e23,e22)=e23)|(op2(e22,e22)=e22|(op2(e21,e21)=e22|op2(e20,e20)=e22))))&((op2(e23,e23)=e22|(~(op2(e22,e22)=e22)|(op2(e21,e21)=e22|op2(e20,e20)=e22)))&(~(op2(e23,e22)=e23)|(~(op2(e22,e22)=e22)|(op2(e21,e21)=e22|op2(e20,e20)=e22)))))&(((op2(e23,e23)=e22|(op2(e22,e22)=e22|(~(op2(e21,e22)=e21)|op2(e20,e20)=e22)))&(~(op2(e23,e22)=e23)|(op2(e22,e22)=e22|(~(op2(e21,e22)=e21)|op2(e20,e20)=e22))))&((op2(e23,e23)=e22|(~(op2(e22,e22)=e22)|(~(op2(e21,e22)=e21)|op2(e20,e20)=e22)))&(~(op2(e23,e22)=e23)|(~(op2(e22,e22)=e22)|(~(op2(e21,e22)=e21)|op2(e20,e20)=e22))))))&((((op2(e23,e23)=e22|(op2(e22,e22)=e22|(op2(e21,e21)=e22|~(op2(e20,e22)=e20))))&(~(op2(e23,e22)=e23)|(op2(e22,e22)=e22|(op2(e21,e21)=e22|~(op2(e20,e22)=e20)))))&((op2(e23,e23)=e22|(~(op2(e22,e22)=e22)|(op2(e21,e21)=e22|~(op2(e20,e22)=e20))))&(~(op2(e23,e22)=e23)|(~(op2(e22,e22)=e22)|(op2(e21,e21)=e22|~(op2(e20,e22)=e20))))))&(((op2(e23,e23)=e22|(op2(e22,e22)=e22|(~(op2(e21,e22)=e21)|~(op2(e20,e22)=e20))))&(~(op2(e23,e22)=e23)|(op2(e22,e22)=e22|(~(op2(e21,e22)=e21)|~(op2(e20,e22)=e20)))))&((op2(e23,e23)=e22|(~(op2(e22,e22)=e22)|(~(op2(e21,e22)=e21)|~(op2(e20,e22)=e20))))&(~(op2(e23,e22)=e23)|(~(op2(e22,e22)=e22)|(~(op2(e21,e22)=e21)|~(op2(e20,e22)=e20)))))))))&(((((op2(e23,e23)=e23|(op2(e22,e22)=e23|(op2(e21,e21)=e23|op2(e20,e20)=e23)))&(~(op2(e23,e23)=e23)|(op2(e22,e22)=e23|(op2(e21,e21)=e23|op2(e20,e20)=e23))))&((op2(e23,e23)=e23|(~(op2(e22,e23)=e22)|(op2(e21,e21)=e23|op2(e20,e20)=e23)))&(~(op2(e23,e23)=e23)|(~(op2(e22,e23)=e22)|(op2(e21,e21)=e23|op2(e20,e20)=e23)))))&(((op2(e23,e23)=e23|(op2(e22,e22)=e23|(~(op2(e21,e23)=e21)|op2(e20,e20)=e23)))&(~(op2(e23,e23)=e23)|(op2(e22,e22)=e23|(~(op2(e21,e23)=e21)|op2(e20,e20)=e23))))&((op2(e23,e23)=e23|(~(op2(e22,e23)=e22)|(~(op2(e21,e23)=e21)|op2(e20,e20)=e23)))&(~(op2(e23,e23)=e23)|(~(op2(e22,e23)=e22)|(~(op2(e21,e23)=e21)|op2(e20,e20)=e23))))))&((((op2(e23,e23)=e23|(op2(e22,e22)=e23|(op2(e21,e21)=e23|~(op2(e20,e23)=e20))))&(~(op2(e23,e23)=e23)|(op2(e22,e22)=e23|(op2(e21,e21)=e23|~(op2(e20,e23)=e20)))))&((op2(e23,e23)=e23|(~(op2(e22,e23)=e22)|(op2(e21,e21)=e23|~(op2(e20,e23)=e20))))&(~(op2(e23,e23)=e23)|(~(op2(e22,e23)=e22)|(op2(e21,e21)=e23|~(op2(e20,e23)=e20))))))&(((op2(e23,e23)=e23|(op2(e22,e22)=e23|(~(op2(e21,e23)=e21)|~(op2(e20,e23)=e20))))&(~(op2(e23,e23)=e23)|(op2(e22,e22)=e23|(~(op2(e21,e23)=e21)|~(op2(e20,e23)=e20)))))&((op2(e23,e23)=e23|(~(op2(e22,e23)=e22)|(~(op2(e21,e23)=e21)|~(op2(e20,e23)=e20))))&(~(op2(e23,e23)=e23)|(~(op2(e22,e23)=e22)|(~(op2(e21,e23)=e21)|~(op2(e20,e23)=e20))))))))),inference(distribute,[status(thm)],[11])).
% cnf(326,plain,(op2(e20,e20)=e23|op2(e21,e21)=e23|op2(e22,e22)=e23|op2(e23,e23)=e23),inference(split_conjunct,[status(thm)],[310])).
% cnf(346,plain,(op2(e22,e22)=e21|op2(e23,e23)=e21|op2(e20,e21)!=e20|op2(e21,e21)!=e21),inference(split_conjunct,[status(thm)],[310])).
% cnf(350,plain,(op2(e21,e21)=e21|op2(e22,e22)=e21|op2(e23,e23)=e21|op2(e20,e21)!=e20),inference(split_conjunct,[status(thm)],[310])).
% cnf(354,plain,(op2(e20,e20)=e21|op2(e22,e22)=e21|op2(e23,e23)=e21|op2(e21,e21)!=e21),inference(split_conjunct,[status(thm)],[310])).
% cnf(358,plain,(op2(e20,e20)=e21|op2(e21,e21)=e21|op2(e22,e22)=e21|op2(e23,e23)=e21),inference(split_conjunct,[status(thm)],[310])).
% cnf(370,plain,(op2(e20,e20)=e20|op2(e22,e22)=e20|op2(e23,e23)=e20|op2(e21,e20)!=e21),inference(split_conjunct,[status(thm)],[310])).
% cnf(374,plain,(op2(e20,e20)=e20|op2(e21,e21)=e20|op2(e22,e22)=e20|op2(e23,e23)=e20),inference(split_conjunct,[status(thm)],[310])).
% cnf(375,plain,(e12=op1(e13,e13)),inference(split_conjunct,[status(thm)],[12])).
% cnf(376,plain,(e11=op1(op1(e13,e13),e13)),inference(split_conjunct,[status(thm)],[12])).
% cnf(377,plain,(e10=op1(e13,op1(e13,e13))),inference(split_conjunct,[status(thm)],[12])).
% cnf(378,plain,(e22=op2(e23,e23)),inference(split_conjunct,[status(thm)],[13])).
% cnf(379,plain,(e21=op2(op2(e23,e23),e23)),inference(split_conjunct,[status(thm)],[13])).
% cnf(380,plain,(e20=op2(e23,op2(e23,e23))),inference(split_conjunct,[status(thm)],[13])).
% cnf(393,plain,(h4(e12)=op2(e23,e23)),inference(split_conjunct,[status(thm)],[17])).
% cnf(394,plain,(h4(e11)=op2(op2(e23,e23),e23)),inference(split_conjunct,[status(thm)],[17])).
% cnf(395,plain,(h4(e10)=op2(e23,op2(e23,e23))),inference(split_conjunct,[status(thm)],[17])).
% cnf(396,plain,(h4(e13)=e23),inference(split_conjunct,[status(thm)],[17])).
% fof(397, negated_conjecture,((((~(epred1_0)|(((~(h1(e10)=e23)&~(h1(e11)=e23))&~(h1(e12)=e23))&~(h1(e13)=e23)))&(~(epred2_0)|(((~(h2(e10)=e23)&~(h2(e11)=e23))&~(h2(e12)=e23))&~(h2(e13)=e23))))&(~(epred3_0)|(((~(h3(e10)=e23)&~(h3(e11)=e23))&~(h3(e12)=e23))&~(h3(e13)=e23))))&(~(epred4_0)|(((~(h4(e10)=e23)&~(h4(e11)=e23))&~(h4(e12)=e23))&~(h4(e13)=e23)))),inference(fof_nnf,[status(thm)],[24])).
% fof(398, negated_conjecture,(((((((~(h1(e10)=e23)|~(epred1_0))&(~(h1(e11)=e23)|~(epred1_0)))&(~(h1(e12)=e23)|~(epred1_0)))&(~(h1(e13)=e23)|~(epred1_0)))&((((~(h2(e10)=e23)|~(epred2_0))&(~(h2(e11)=e23)|~(epred2_0)))&(~(h2(e12)=e23)|~(epred2_0)))&(~(h2(e13)=e23)|~(epred2_0))))&((((~(h3(e10)=e23)|~(epred3_0))&(~(h3(e11)=e23)|~(epred3_0)))&(~(h3(e12)=e23)|~(epred3_0)))&(~(h3(e13)=e23)|~(epred3_0))))&((((~(h4(e10)=e23)|~(epred4_0))&(~(h4(e11)=e23)|~(epred4_0)))&(~(h4(e12)=e23)|~(epred4_0)))&(~(h4(e13)=e23)|~(epred4_0)))),inference(distribute,[status(thm)],[397])).
% cnf(399,negated_conjecture,(~epred4_0|h4(e13)!=e23),inference(split_conjunct,[status(thm)],[398])).
% fof(613, plain,(((((((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13))))|(((~(h4(e10)=e20)&~(h4(e11)=e20))&~(h4(e12)=e20))&~(h4(e13)=e20)))|(((~(h4(e10)=e21)&~(h4(e11)=e21))&~(h4(e12)=e21))&~(h4(e13)=e21)))|(((~(h4(e10)=e22)&~(h4(e11)=e22))&~(h4(e12)=e22))&~(h4(e13)=e22)))|epred4_0),inference(fof_nnf,[status(thm)],[23])).
% fof(614, plain,(((((((((((~(h4(e10)=e22)|(~(h4(e10)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e10)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e10)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e10)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&(((((~(h4(e10)=e22)|(~(h4(e11)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e11)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e11)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e11)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)))&(((((~(h4(e10)=e22)|(~(h4(e12)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e12)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e12)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e12)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)))&(((((~(h4(e10)=e22)|(~(h4(e13)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e13)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e13)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e13)=e21)|(~(h4(e10)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)))&((((((((~(h4(e10)=e22)|(~(h4(e10)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e10)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e10)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e10)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&(((((~(h4(e10)=e22)|(~(h4(e11)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e11)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e11)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e11)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)))&(((((~(h4(e10)=e22)|(~(h4(e12)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e12)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e12)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e12)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)))&(((((~(h4(e10)=e22)|(~(h4(e13)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e13)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e13)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e13)=e21)|(~(h4(e11)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))))&((((((((~(h4(e10)=e22)|(~(h4(e10)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e10)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e10)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e10)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&(((((~(h4(e10)=e22)|(~(h4(e11)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e11)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e11)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e11)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)))&(((((~(h4(e10)=e22)|(~(h4(e12)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e12)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e12)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e12)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)))&(((((~(h4(e10)=e22)|(~(h4(e13)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e13)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e13)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e13)=e21)|(~(h4(e12)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))))&((((((((~(h4(e10)=e22)|(~(h4(e10)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e10)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e10)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e10)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&(((((~(h4(e10)=e22)|(~(h4(e11)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e11)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e11)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e11)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)))&(((((~(h4(e10)=e22)|(~(h4(e12)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e12)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e12)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e12)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)))&(((((~(h4(e10)=e22)|(~(h4(e13)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)&((~(h4(e11)=e22)|(~(h4(e13)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e12)=e22)|(~(h4(e13)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0))&((~(h4(e13)=e22)|(~(h4(e13)=e21)|(~(h4(e13)=e20)|(((((((((((((((~(h4(op1(e10,e10))=op2(h4(e10),h4(e10)))|~(h4(op1(e10,e11))=op2(h4(e10),h4(e11))))|~(h4(op1(e10,e12))=op2(h4(e10),h4(e12))))|~(h4(op1(e10,e13))=op2(h4(e10),h4(e13))))|~(h4(op1(e11,e10))=op2(h4(e11),h4(e10))))|~(h4(op1(e11,e11))=op2(h4(e11),h4(e11))))|~(h4(op1(e11,e12))=op2(h4(e11),h4(e12))))|~(h4(op1(e11,e13))=op2(h4(e11),h4(e13))))|~(h4(op1(e12,e10))=op2(h4(e12),h4(e10))))|~(h4(op1(e12,e11))=op2(h4(e12),h4(e11))))|~(h4(op1(e12,e12))=op2(h4(e12),h4(e12))))|~(h4(op1(e12,e13))=op2(h4(e12),h4(e13))))|~(h4(op1(e13,e10))=op2(h4(e13),h4(e10))))|~(h4(op1(e13,e11))=op2(h4(e13),h4(e11))))|~(h4(op1(e13,e12))=op2(h4(e13),h4(e12))))|~(h4(op1(e13,e13))=op2(h4(e13),h4(e13)))))))|epred4_0)))),inference(distribute,[status(thm)],[613])).
% cnf(672,plain,(epred4_0|h4(op1(e13,e13))!=op2(h4(e13),h4(e13))|h4(op1(e13,e12))!=op2(h4(e13),h4(e12))|h4(op1(e13,e11))!=op2(h4(e13),h4(e11))|h4(op1(e13,e10))!=op2(h4(e13),h4(e10))|h4(op1(e12,e13))!=op2(h4(e12),h4(e13))|h4(op1(e12,e12))!=op2(h4(e12),h4(e12))|h4(op1(e12,e11))!=op2(h4(e12),h4(e11))|h4(op1(e12,e10))!=op2(h4(e12),h4(e10))|h4(op1(e11,e13))!=op2(h4(e11),h4(e13))|h4(op1(e11,e12))!=op2(h4(e11),h4(e12))|h4(op1(e11,e11))!=op2(h4(e11),h4(e11))|h4(op1(e11,e10))!=op2(h4(e11),h4(e10))|h4(op1(e10,e13))!=op2(h4(e10),h4(e13))|h4(op1(e10,e12))!=op2(h4(e10),h4(e12))|h4(op1(e10,e11))!=op2(h4(e10),h4(e11))|h4(op1(e10,e10))!=op2(h4(e10),h4(e10))|h4(e10)!=e20|h4(e11)!=e21|h4(e12)!=e22),inference(split_conjunct,[status(thm)],[614])).
% cnf(679,plain,(e22=h4(e12)),inference(rw,[status(thm)],[393,378,theory(equality)])).
% cnf(680,plain,(op1(e13,e12)=e10),inference(rw,[status(thm)],[377,375,theory(equality)])).
% cnf(681,plain,(op1(e12,e13)=e11),inference(rw,[status(thm)],[376,375,theory(equality)])).
% cnf(682,plain,(op2(e23,e22)=e20),inference(rw,[status(thm)],[380,378,theory(equality)])).
% cnf(683,plain,(op2(e22,e23)=e21),inference(rw,[status(thm)],[379,378,theory(equality)])).
% cnf(684,plain,(e20=h4(e10)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[395,378,theory(equality)]),682,theory(equality)])).
% cnf(687,plain,(e21=h4(e11)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[394,378,theory(equality)]),683,theory(equality)])).
% cnf(695,negated_conjecture,($false|~epred4_0),inference(rw,[status(thm)],[399,396,theory(equality)])).
% cnf(696,negated_conjecture,(~epred4_0),inference(cn,[status(thm)],[695,theory(equality)])).
% cnf(697,plain,(op1(e10,e10)=e10|op1(e11,e11)=e10|op1(e12,e12)=e10|e12=e10),inference(rw,[status(thm)],[309,375,theory(equality)])).
% cnf(698,plain,(op1(e10,e10)=e10|op1(e11,e11)=e10|op1(e12,e12)=e10),inference(sr,[status(thm)],[697,221,theory(equality)])).
% cnf(699,plain,(op1(e10,e10)=e11|op1(e11,e11)=e11|op1(e12,e12)=e11|e12=e11),inference(rw,[status(thm)],[293,375,theory(equality)])).
% cnf(700,plain,(op1(e10,e10)=e11|op1(e11,e11)=e11|op1(e12,e12)=e11),inference(sr,[status(thm)],[699,219,theory(equality)])).
% cnf(706,plain,(e11!=op1(e11,e13)),inference(rw,[status(thm)],[147,681,theory(equality)])).
% cnf(710,plain,(e11!=op1(e12,e12)),inference(rw,[status(thm)],[127,681,theory(equality)])).
% cnf(711,plain,(op1(e11,e11)=e11|op1(e10,e10)=e11),inference(sr,[status(thm)],[700,710,theory(equality)])).
% cnf(713,plain,(e10!=op1(e10,e12)),inference(rw,[status(thm)],[154,680,theory(equality)])).
% cnf(714,plain,(op1(e10,e13)=e10|op1(e10,e11)=e10|op1(e10,e10)=e10),inference(sr,[status(thm)],[72,713,theory(equality)])).
% cnf(718,plain,(e10!=op1(e12,e12)),inference(rw,[status(thm)],[151,680,theory(equality)])).
% cnf(719,plain,(op1(e11,e11)=e10|op1(e10,e10)=e10),inference(sr,[status(thm)],[698,718,theory(equality)])).
% cnf(720,plain,(e10!=op1(e13,e10)),inference(rw,[status(thm)],[125,680,theory(equality)])).
% cnf(721,plain,(op1(e12,e10)=e10|op1(e11,e10)=e10|op1(e10,e10)=e10),inference(sr,[status(thm)],[71,720,theory(equality)])).
% cnf(726,plain,(e12!=op1(e11,e13)),inference(rw,[status(thm)],[146,375,theory(equality)])).
% cnf(730,plain,(op1(e10,e12)=e12|op1(e11,e12)=e12|op1(e12,e12)=e12|e10=e12),inference(rw,[status(thm)],[51,680,theory(equality)])).
% cnf(731,plain,(op1(e10,e12)=e12|op1(e11,e12)=e12|op1(e12,e12)=e12),inference(sr,[status(thm)],[730,221,theory(equality)])).
% cnf(736,plain,(e12!=op1(e13,e10)),inference(rw,[status(thm)],[124,375,theory(equality)])).
% cnf(754,plain,(e22!=op2(e23,e20)),inference(rw,[status(thm)],[172,378,theory(equality)])).
% cnf(760,plain,(op1(e10,e13)=e13|op1(e11,e13)=e13|e11=e13|op1(e13,e13)=e13),inference(rw,[status(thm)],[41,681,theory(equality)])).
% cnf(761,plain,(op1(e10,e13)=e13|op1(e11,e13)=e13|e11=e13|e12=e13),inference(rw,[status(thm)],[760,375,theory(equality)])).
% cnf(762,plain,(op1(e10,e13)=e13|op1(e11,e13)=e13|e12=e13),inference(sr,[status(thm)],[761,218,theory(equality)])).
% cnf(763,plain,(op1(e10,e13)=e13|op1(e11,e13)=e13),inference(sr,[status(thm)],[762,217,theory(equality)])).
% cnf(765,plain,(e21!=op2(e21,e23)),inference(rw,[status(thm)],[195,683,theory(equality)])).
% cnf(767,plain,(op1(e11,e10)=e11|op1(e11,e11)=e11|op1(e11,e12)=e11),inference(sr,[status(thm)],[62,706,theory(equality)])).
% cnf(768,plain,(op1(e11,e10)=e12|op1(e11,e11)=e12|op1(e11,e12)=e12),inference(sr,[status(thm)],[60,726,theory(equality)])).
% cnf(769,plain,(e20!=op2(e23,e20)),inference(rw,[status(thm)],[173,682,theory(equality)])).
% cnf(774,plain,(e21!=op2(e22,e22)),inference(rw,[status(thm)],[175,683,theory(equality)])).
% cnf(782,plain,(op1(e12,e10)=e12|op1(e12,e11)=e12|op1(e12,e12)=e12|e11=e12),inference(rw,[status(thm)],[52,681,theory(equality)])).
% cnf(783,plain,(op1(e12,e10)=e12|op1(e12,e11)=e12|op1(e12,e12)=e12),inference(sr,[status(thm)],[782,219,theory(equality)])).
% cnf(786,plain,(e20!=op2(e20,e22)),inference(rw,[status(thm)],[202,682,theory(equality)])).
% cnf(795,plain,(e20!=op2(e22,e22)),inference(rw,[status(thm)],[199,682,theory(equality)])).
% cnf(796,plain,(op1(e13,e10)=e11|op1(e13,e10)=e12|op1(e13,e10)=e13),inference(sr,[status(thm)],[28,720,theory(equality)])).
% cnf(797,plain,(op1(e13,e10)=e11|op1(e13,e10)=e13),inference(sr,[status(thm)],[796,736,theory(equality)])).
% cnf(800,plain,(op1(e13,e10)=e11|op1(e13,e11)=e11|e10=e11|op1(e13,e13)=e11),inference(rw,[status(thm)],[46,680,theory(equality)])).
% cnf(801,plain,(op1(e13,e10)=e11|op1(e13,e11)=e11|e10=e11|e12=e11),inference(rw,[status(thm)],[800,375,theory(equality)])).
% cnf(802,plain,(op1(e13,e10)=e11|op1(e13,e11)=e11|e11=e12),inference(sr,[status(thm)],[801,222,theory(equality)])).
% cnf(803,plain,(op1(e13,e10)=e11|op1(e13,e11)=e11),inference(sr,[status(thm)],[802,219,theory(equality)])).
% cnf(820,plain,(op2(e20,e20)=e20|op2(e20,e21)=e20|op2(e20,e23)=e20),inference(sr,[status(thm)],[120,786,theory(equality)])).
% cnf(824,plain,(op1(e10,e10)=e10|op1(e12,e12)=e10|e12=e10|op1(e11,e10)!=e11),inference(rw,[status(thm)],[305,375,theory(equality)])).
% cnf(825,plain,(op1(e10,e10)=e10|e10=e12|op1(e11,e10)!=e11),inference(sr,[status(thm)],[824,718,theory(equality)])).
% cnf(826,plain,(op1(e10,e10)=e10|op1(e11,e10)!=e11),inference(sr,[status(thm)],[825,221,theory(equality)])).
% cnf(830,plain,(op1(e10,e10)=e11|op1(e12,e12)=e11|e12=e11|op1(e11,e11)!=e11),inference(rw,[status(thm)],[289,375,theory(equality)])).
% cnf(831,plain,(op1(e10,e10)=e11|e11=e12|op1(e11,e11)!=e11),inference(sr,[status(thm)],[830,710,theory(equality)])).
% cnf(832,plain,(op1(e10,e10)=e11|op1(e11,e11)!=e11),inference(sr,[status(thm)],[831,219,theory(equality)])).
% cnf(835,plain,(op2(e20,e20)=e20|op2(e21,e21)=e20|op2(e22,e22)=e20|e22=e20),inference(rw,[status(thm)],[374,378,theory(equality)])).
% cnf(836,plain,(op2(e20,e20)=e20|op2(e21,e21)=e20|e22=e20),inference(sr,[status(thm)],[835,795,theory(equality)])).
% cnf(837,plain,(op2(e20,e20)=e20|op2(e21,e21)=e20),inference(sr,[status(thm)],[836,227,theory(equality)])).
% cnf(850,plain,(op1(e11,e11)=e11|op1(e12,e12)=e11|e12=e11|op1(e10,e11)!=e10),inference(rw,[status(thm)],[285,375,theory(equality)])).
% cnf(851,plain,(op1(e11,e11)=e11|e11=e12|op1(e10,e11)!=e10),inference(sr,[status(thm)],[850,710,theory(equality)])).
% cnf(852,plain,(op1(e11,e11)=e11|op1(e10,e11)!=e10),inference(sr,[status(thm)],[851,219,theory(equality)])).
% cnf(856,plain,(op1(e11,e11)=e13|op1(e12,e12)=e13|e12=e13|op1(e10,e13)!=e10),inference(rw,[status(thm)],[253,375,theory(equality)])).
% cnf(857,plain,(op1(e11,e11)=e13|op1(e12,e12)=e13|op1(e10,e13)!=e10),inference(sr,[status(thm)],[856,217,theory(equality)])).
% cnf(869,plain,(op2(e20,e20)=e21|op2(e21,e21)=e21|op2(e22,e22)=e21|e22=e21),inference(rw,[status(thm)],[358,378,theory(equality)])).
% cnf(870,plain,(op2(e20,e20)=e21|op2(e21,e21)=e21|e22=e21),inference(sr,[status(thm)],[869,774,theory(equality)])).
% cnf(871,plain,(op2(e20,e20)=e21|op2(e21,e21)=e21),inference(sr,[status(thm)],[870,225,theory(equality)])).
% cnf(904,plain,(op1(e12,e12)=e10|e12=e10|op1(e10,e10)!=e10|op1(e11,e10)!=e11),inference(rw,[status(thm)],[297,375,theory(equality)])).
% cnf(905,plain,(e10=e12|op1(e10,e10)!=e10|op1(e11,e10)!=e11),inference(sr,[status(thm)],[904,718,theory(equality)])).
% cnf(906,plain,(op1(e10,e10)!=e10|op1(e11,e10)!=e11),inference(sr,[status(thm)],[905,221,theory(equality)])).
% cnf(907,plain,(op1(e11,e10)!=e11),inference(csr,[status(thm)],[906,826])).
% cnf(909,plain,(op1(e11,e12)=e11|op1(e11,e11)=e11),inference(sr,[status(thm)],[767,907,theory(equality)])).
% cnf(910,plain,(op1(e12,e12)=e11|e12=e11|op1(e10,e11)!=e10|op1(e11,e11)!=e11),inference(rw,[status(thm)],[281,375,theory(equality)])).
% cnf(911,plain,(e11=e12|op1(e10,e11)!=e10|op1(e11,e11)!=e11),inference(sr,[status(thm)],[910,710,theory(equality)])).
% cnf(912,plain,(op1(e10,e11)!=e10|op1(e11,e11)!=e11),inference(sr,[status(thm)],[911,219,theory(equality)])).
% cnf(913,plain,(op1(e10,e11)!=e10),inference(csr,[status(thm)],[912,852])).
% cnf(922,plain,(op2(e20,e20)=e23|op2(e21,e21)=e23|op2(e22,e22)=e23|e22=e23),inference(rw,[status(thm)],[326,378,theory(equality)])).
% cnf(923,plain,(op2(e20,e20)=e23|op2(e21,e21)=e23|op2(e22,e22)=e23),inference(sr,[status(thm)],[922,223,theory(equality)])).
% cnf(958,plain,(op2(e20,e23)=e23|op2(e21,e23)=e23|e21=e23|op2(e23,e23)=e23),inference(rw,[status(thm)],[89,683,theory(equality)])).
% cnf(959,plain,(op2(e20,e23)=e23|op2(e21,e23)=e23|e21=e23|e22=e23),inference(rw,[status(thm)],[958,378,theory(equality)])).
% cnf(960,plain,(op2(e20,e23)=e23|op2(e21,e23)=e23|e23=e22),inference(sr,[status(thm)],[959,224,theory(equality)])).
% cnf(961,plain,(op2(e20,e23)=e23|op2(e21,e23)=e23),inference(sr,[status(thm)],[960,223,theory(equality)])).
% cnf(990,plain,(op2(e20,e22)=e22|op2(e21,e22)=e22|op2(e22,e22)=e22|e20=e22),inference(rw,[status(thm)],[99,682,theory(equality)])).
% cnf(991,plain,(op2(e20,e22)=e22|op2(e21,e22)=e22|op2(e22,e22)=e22),inference(sr,[status(thm)],[990,227,theory(equality)])).
% cnf(1030,plain,(op2(e23,e20)=e21|op2(e23,e20)=e22|op2(e23,e20)=e23),inference(sr,[status(thm)],[76,769,theory(equality)])).
% cnf(1031,plain,(op2(e23,e20)=e21|op2(e23,e20)=e23),inference(sr,[status(thm)],[1030,754,theory(equality)])).
% cnf(1034,plain,(op2(e23,e20)=e21|op2(e23,e21)=e21|e20=e21|op2(e23,e23)=e21),inference(rw,[status(thm)],[94,682,theory(equality)])).
% cnf(1035,plain,(op2(e23,e20)=e21|op2(e23,e21)=e21|e20=e21|e22=e21),inference(rw,[status(thm)],[1034,378,theory(equality)])).
% cnf(1036,plain,(op2(e23,e20)=e21|op2(e23,e21)=e21|e22=e21),inference(sr,[status(thm)],[1035,228,theory(equality)])).
% cnf(1037,plain,(op2(e23,e20)=e21|op2(e23,e21)=e21),inference(sr,[status(thm)],[1036,225,theory(equality)])).
% cnf(1046,plain,(op2(e21,e20)=e21|op2(e21,e21)=e21|op2(e21,e22)=e21),inference(sr,[status(thm)],[110,765,theory(equality)])).
% cnf(1053,plain,(op2(e20,e20)=e20|op2(e22,e22)=e20|e22=e20|op2(e21,e20)!=e21),inference(rw,[status(thm)],[370,378,theory(equality)])).
% cnf(1054,plain,(op2(e20,e20)=e20|e22=e20|op2(e21,e20)!=e21),inference(sr,[status(thm)],[1053,795,theory(equality)])).
% cnf(1055,plain,(op2(e20,e20)=e20|op2(e21,e20)!=e21),inference(sr,[status(thm)],[1054,227,theory(equality)])).
% cnf(1061,plain,(op2(e20,e20)=e21|op2(e22,e22)=e21|e22=e21|op2(e21,e21)!=e21),inference(rw,[status(thm)],[354,378,theory(equality)])).
% cnf(1062,plain,(op2(e20,e20)=e21|e22=e21|op2(e21,e21)!=e21),inference(sr,[status(thm)],[1061,774,theory(equality)])).
% cnf(1063,plain,(op2(e20,e20)=e21|op2(e21,e21)!=e21),inference(sr,[status(thm)],[1062,225,theory(equality)])).
% cnf(1064,plain,(op2(e20,e20)=e21),inference(csr,[status(thm)],[1063,871])).
% cnf(1065,plain,(e21=e20|op2(e21,e20)!=e21),inference(rw,[status(thm)],[1055,1064,theory(equality)])).
% cnf(1066,plain,(op2(e21,e20)!=e21),inference(sr,[status(thm)],[1065,228,theory(equality)])).
% cnf(1067,plain,(op2(e22,e22)=e23|op2(e21,e21)=e23|e21=e23),inference(rw,[status(thm)],[923,1064,theory(equality)])).
% cnf(1068,plain,(op2(e22,e22)=e23|op2(e21,e21)=e23),inference(sr,[status(thm)],[1067,224,theory(equality)])).
% cnf(1071,plain,(op2(e20,e23)=e23|op2(e20,e22)=e23|op2(e20,e21)=e23|e21=e23),inference(rw,[status(thm)],[114,1064,theory(equality)])).
% cnf(1072,plain,(op2(e20,e23)=e23|op2(e20,e22)=e23|op2(e20,e21)=e23),inference(sr,[status(thm)],[1071,224,theory(equality)])).
% cnf(1080,plain,(op2(e21,e21)=e20|e21=e20),inference(rw,[status(thm)],[837,1064,theory(equality)])).
% cnf(1081,plain,(op2(e21,e21)=e20),inference(sr,[status(thm)],[1080,228,theory(equality)])).
% cnf(1084,plain,(op2(e20,e23)=e20|op2(e20,e21)=e20|e21=e20),inference(rw,[status(thm)],[820,1064,theory(equality)])).
% cnf(1085,plain,(op2(e20,e23)=e20|op2(e20,e21)=e20),inference(sr,[status(thm)],[1084,228,theory(equality)])).
% cnf(1091,plain,(op2(e23,e20)!=e21),inference(rw,[status(thm)],[214,1064,theory(equality)])).
% cnf(1111,plain,(op2(e21,e21)=e21|op2(e22,e22)=e21|e22=e21|op2(e20,e21)!=e20),inference(rw,[status(thm)],[350,378,theory(equality)])).
% cnf(1112,plain,(op2(e21,e21)=e21|e22=e21|op2(e20,e21)!=e20),inference(sr,[status(thm)],[1111,774,theory(equality)])).
% cnf(1113,plain,(op2(e21,e21)=e21|op2(e20,e21)!=e20),inference(sr,[status(thm)],[1112,225,theory(equality)])).
% cnf(1121,plain,(op2(e22,e20)=e20|op2(e22,e21)=e20|op2(e22,e22)=e20|e21=e20),inference(rw,[status(thm)],[104,683,theory(equality)])).
% cnf(1122,plain,(op2(e22,e20)=e20|op2(e22,e21)=e20|e21=e20),inference(sr,[status(thm)],[1121,795,theory(equality)])).
% cnf(1123,plain,(op2(e22,e20)=e20|op2(e22,e21)=e20),inference(sr,[status(thm)],[1122,228,theory(equality)])).
% cnf(1141,plain,(op2(e22,e20)=e22|op2(e22,e21)=e22|op2(e22,e22)=e22|e21=e22),inference(rw,[status(thm)],[100,683,theory(equality)])).
% cnf(1142,plain,(op2(e22,e20)=e22|op2(e22,e21)=e22|op2(e22,e22)=e22),inference(sr,[status(thm)],[1141,225,theory(equality)])).
% cnf(1162,plain,(op2(e22,e22)=e21|e22=e21|op2(e20,e21)!=e20|op2(e21,e21)!=e21),inference(rw,[status(thm)],[346,378,theory(equality)])).
% cnf(1163,plain,(e22=e21|op2(e20,e21)!=e20|op2(e21,e21)!=e21),inference(sr,[status(thm)],[1162,774,theory(equality)])).
% cnf(1164,plain,(op2(e20,e21)!=e20|op2(e21,e21)!=e21),inference(sr,[status(thm)],[1163,225,theory(equality)])).
% cnf(1165,plain,(op2(e20,e21)!=e20),inference(csr,[status(thm)],[1164,1113])).
% cnf(4758,plain,(epred4_0|$false|h4(e11)!=e21|h4(e12)!=e22|op2(h4(e10),h4(e10))!=h4(op1(e10,e10))|op2(h4(e10),h4(e11))!=h4(op1(e10,e11))|op2(h4(e10),h4(e12))!=h4(op1(e10,e12))|op2(h4(e10),h4(e13))!=h4(op1(e10,e13))|op2(h4(e11),h4(e10))!=h4(op1(e11,e10))|op2(h4(e11),h4(e11))!=h4(op1(e11,e11))|op2(h4(e11),h4(e12))!=h4(op1(e11,e12))|op2(h4(e11),h4(e13))!=h4(op1(e11,e13))|op2(h4(e12),h4(e10))!=h4(op1(e12,e10))|op2(h4(e12),h4(e11))!=h4(op1(e12,e11))|op2(h4(e12),h4(e12))!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[672,684,theory(equality)])).
% cnf(4759,plain,(epred4_0|$false|$false|h4(e12)!=e22|op2(h4(e10),h4(e10))!=h4(op1(e10,e10))|op2(h4(e10),h4(e11))!=h4(op1(e10,e11))|op2(h4(e10),h4(e12))!=h4(op1(e10,e12))|op2(h4(e10),h4(e13))!=h4(op1(e10,e13))|op2(h4(e11),h4(e10))!=h4(op1(e11,e10))|op2(h4(e11),h4(e11))!=h4(op1(e11,e11))|op2(h4(e11),h4(e12))!=h4(op1(e11,e12))|op2(h4(e11),h4(e13))!=h4(op1(e11,e13))|op2(h4(e12),h4(e10))!=h4(op1(e12,e10))|op2(h4(e12),h4(e11))!=h4(op1(e12,e11))|op2(h4(e12),h4(e12))!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[4758,687,theory(equality)])).
% cnf(4760,plain,(epred4_0|$false|$false|$false|op2(h4(e10),h4(e10))!=h4(op1(e10,e10))|op2(h4(e10),h4(e11))!=h4(op1(e10,e11))|op2(h4(e10),h4(e12))!=h4(op1(e10,e12))|op2(h4(e10),h4(e13))!=h4(op1(e10,e13))|op2(h4(e11),h4(e10))!=h4(op1(e11,e10))|op2(h4(e11),h4(e11))!=h4(op1(e11,e11))|op2(h4(e11),h4(e12))!=h4(op1(e11,e12))|op2(h4(e11),h4(e13))!=h4(op1(e11,e13))|op2(h4(e12),h4(e10))!=h4(op1(e12,e10))|op2(h4(e12),h4(e11))!=h4(op1(e12,e11))|op2(h4(e12),h4(e12))!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[4759,679,theory(equality)])).
% cnf(4761,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(h4(e10),h4(e11))!=h4(op1(e10,e11))|op2(h4(e10),h4(e12))!=h4(op1(e10,e12))|op2(h4(e10),h4(e13))!=h4(op1(e10,e13))|op2(h4(e11),h4(e10))!=h4(op1(e11,e10))|op2(h4(e11),h4(e11))!=h4(op1(e11,e11))|op2(h4(e11),h4(e12))!=h4(op1(e11,e12))|op2(h4(e11),h4(e13))!=h4(op1(e11,e13))|op2(h4(e12),h4(e10))!=h4(op1(e12,e10))|op2(h4(e12),h4(e11))!=h4(op1(e12,e11))|op2(h4(e12),h4(e12))!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[4760,684,theory(equality)]),684,theory(equality)]),1064,theory(equality)])).
% cnf(4762,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(h4(e10),h4(e12))!=h4(op1(e10,e12))|op2(h4(e10),h4(e13))!=h4(op1(e10,e13))|op2(h4(e11),h4(e10))!=h4(op1(e11,e10))|op2(h4(e11),h4(e11))!=h4(op1(e11,e11))|op2(h4(e11),h4(e12))!=h4(op1(e11,e12))|op2(h4(e11),h4(e13))!=h4(op1(e11,e13))|op2(h4(e12),h4(e10))!=h4(op1(e12,e10))|op2(h4(e12),h4(e11))!=h4(op1(e12,e11))|op2(h4(e12),h4(e12))!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4761,684,theory(equality)]),687,theory(equality)])).
% cnf(4763,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(h4(e10),h4(e13))!=h4(op1(e10,e13))|op2(h4(e11),h4(e10))!=h4(op1(e11,e10))|op2(h4(e11),h4(e11))!=h4(op1(e11,e11))|op2(h4(e11),h4(e12))!=h4(op1(e11,e12))|op2(h4(e11),h4(e13))!=h4(op1(e11,e13))|op2(h4(e12),h4(e10))!=h4(op1(e12,e10))|op2(h4(e12),h4(e11))!=h4(op1(e12,e11))|op2(h4(e12),h4(e12))!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4762,684,theory(equality)]),679,theory(equality)])).
% cnf(4764,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(h4(e11),h4(e10))!=h4(op1(e11,e10))|op2(h4(e11),h4(e11))!=h4(op1(e11,e11))|op2(h4(e11),h4(e12))!=h4(op1(e11,e12))|op2(h4(e11),h4(e13))!=h4(op1(e11,e13))|op2(h4(e12),h4(e10))!=h4(op1(e12,e10))|op2(h4(e12),h4(e11))!=h4(op1(e12,e11))|op2(h4(e12),h4(e12))!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4763,684,theory(equality)]),396,theory(equality)])).
% cnf(4765,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(h4(e11),h4(e11))!=h4(op1(e11,e11))|op2(h4(e11),h4(e12))!=h4(op1(e11,e12))|op2(h4(e11),h4(e13))!=h4(op1(e11,e13))|op2(h4(e12),h4(e10))!=h4(op1(e12,e10))|op2(h4(e12),h4(e11))!=h4(op1(e12,e11))|op2(h4(e12),h4(e12))!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4764,687,theory(equality)]),684,theory(equality)])).
% cnf(4766,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(h4(e11),h4(e12))!=h4(op1(e11,e12))|op2(h4(e11),h4(e13))!=h4(op1(e11,e13))|op2(h4(e12),h4(e10))!=h4(op1(e12,e10))|op2(h4(e12),h4(e11))!=h4(op1(e12,e11))|op2(h4(e12),h4(e12))!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4765,687,theory(equality)]),687,theory(equality)])).
% cnf(4767,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(h4(e11),h4(e13))!=h4(op1(e11,e13))|op2(h4(e12),h4(e10))!=h4(op1(e12,e10))|op2(h4(e12),h4(e11))!=h4(op1(e12,e11))|op2(h4(e12),h4(e12))!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4766,687,theory(equality)]),679,theory(equality)])).
% cnf(4768,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(e21,e23)!=h4(op1(e11,e13))|op2(h4(e12),h4(e10))!=h4(op1(e12,e10))|op2(h4(e12),h4(e11))!=h4(op1(e12,e11))|op2(h4(e12),h4(e12))!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4767,687,theory(equality)]),396,theory(equality)])).
% cnf(4769,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(e21,e23)!=h4(op1(e11,e13))|op2(e22,e20)!=h4(op1(e12,e10))|op2(h4(e12),h4(e11))!=h4(op1(e12,e11))|op2(h4(e12),h4(e12))!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4768,679,theory(equality)]),684,theory(equality)])).
% cnf(4770,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(e21,e23)!=h4(op1(e11,e13))|op2(e22,e20)!=h4(op1(e12,e10))|op2(e22,e21)!=h4(op1(e12,e11))|op2(h4(e12),h4(e12))!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4769,679,theory(equality)]),687,theory(equality)])).
% cnf(4771,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(e21,e23)!=h4(op1(e11,e13))|op2(e22,e20)!=h4(op1(e12,e10))|op2(e22,e21)!=h4(op1(e12,e11))|op2(e22,e22)!=h4(op1(e12,e12))|op2(h4(e12),h4(e13))!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4770,679,theory(equality)]),679,theory(equality)])).
% cnf(4772,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(e21,e23)!=h4(op1(e11,e13))|op2(e22,e20)!=h4(op1(e12,e10))|op2(e22,e21)!=h4(op1(e12,e11))|op2(e22,e22)!=h4(op1(e12,e12))|e21!=h4(op1(e12,e13))|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[4771,679,theory(equality)]),396,theory(equality)]),683,theory(equality)])).
% cnf(4773,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(e21,e23)!=h4(op1(e11,e13))|op2(e22,e20)!=h4(op1(e12,e10))|op2(e22,e21)!=h4(op1(e12,e11))|op2(e22,e22)!=h4(op1(e12,e12))|$false|op2(h4(e13),h4(e10))!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4772,681,theory(equality)]),687,theory(equality)])).
% cnf(4774,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(e21,e23)!=h4(op1(e11,e13))|op2(e22,e20)!=h4(op1(e12,e10))|op2(e22,e21)!=h4(op1(e12,e11))|op2(e22,e22)!=h4(op1(e12,e12))|$false|op2(e23,e20)!=h4(op1(e13,e10))|op2(h4(e13),h4(e11))!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4773,396,theory(equality)]),684,theory(equality)])).
% cnf(4775,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(e21,e23)!=h4(op1(e11,e13))|op2(e22,e20)!=h4(op1(e12,e10))|op2(e22,e21)!=h4(op1(e12,e11))|op2(e22,e22)!=h4(op1(e12,e12))|$false|op2(e23,e20)!=h4(op1(e13,e10))|op2(e23,e21)!=h4(op1(e13,e11))|op2(h4(e13),h4(e12))!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4774,396,theory(equality)]),687,theory(equality)])).
% cnf(4776,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(e21,e23)!=h4(op1(e11,e13))|op2(e22,e20)!=h4(op1(e12,e10))|op2(e22,e21)!=h4(op1(e12,e11))|op2(e22,e22)!=h4(op1(e12,e12))|$false|op2(e23,e20)!=h4(op1(e13,e10))|op2(e23,e21)!=h4(op1(e13,e11))|e20!=h4(op1(e13,e12))|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[4775,396,theory(equality)]),679,theory(equality)]),682,theory(equality)])).
% cnf(4777,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(e21,e23)!=h4(op1(e11,e13))|op2(e22,e20)!=h4(op1(e12,e10))|op2(e22,e21)!=h4(op1(e12,e11))|op2(e22,e22)!=h4(op1(e12,e12))|$false|op2(e23,e20)!=h4(op1(e13,e10))|op2(e23,e21)!=h4(op1(e13,e11))|$false|op2(h4(e13),h4(e13))!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4776,680,theory(equality)]),684,theory(equality)])).
% cnf(4778,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(e21,e23)!=h4(op1(e11,e13))|op2(e22,e20)!=h4(op1(e12,e10))|op2(e22,e21)!=h4(op1(e12,e11))|op2(e22,e22)!=h4(op1(e12,e12))|$false|op2(e23,e20)!=h4(op1(e13,e10))|op2(e23,e21)!=h4(op1(e13,e11))|$false|e22!=h4(op1(e13,e13))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[4777,396,theory(equality)]),396,theory(equality)]),378,theory(equality)])).
% cnf(4779,plain,(epred4_0|$false|$false|$false|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(e21,e23)!=h4(op1(e11,e13))|op2(e22,e20)!=h4(op1(e12,e10))|op2(e22,e21)!=h4(op1(e12,e11))|op2(e22,e22)!=h4(op1(e12,e12))|$false|op2(e23,e20)!=h4(op1(e13,e10))|op2(e23,e21)!=h4(op1(e13,e11))|$false|$false),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4778,375,theory(equality)]),679,theory(equality)])).
% cnf(4780,plain,(epred4_0|e21!=h4(op1(e10,e10))|op2(e20,e21)!=h4(op1(e10,e11))|op2(e20,e22)!=h4(op1(e10,e12))|op2(e20,e23)!=h4(op1(e10,e13))|op2(e21,e20)!=h4(op1(e11,e10))|op2(e21,e21)!=h4(op1(e11,e11))|op2(e21,e22)!=h4(op1(e11,e12))|op2(e21,e23)!=h4(op1(e11,e13))|op2(e22,e20)!=h4(op1(e12,e10))|op2(e22,e21)!=h4(op1(e12,e11))|op2(e22,e22)!=h4(op1(e12,e12))|op2(e23,e20)!=h4(op1(e13,e10))|op2(e23,e21)!=h4(op1(e13,e11))),inference(cn,[status(thm)],[4779,theory(equality)])).
% cnf(4781,plain,(h4(op1(e10,e10))!=e21|h4(op1(e10,e11))!=op2(e20,e21)|h4(op1(e10,e12))!=op2(e20,e22)|h4(op1(e10,e13))!=op2(e20,e23)|h4(op1(e11,e10))!=op2(e21,e20)|h4(op1(e11,e11))!=op2(e21,e21)|h4(op1(e11,e12))!=op2(e21,e22)|h4(op1(e11,e13))!=op2(e21,e23)|h4(op1(e12,e10))!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)),inference(sr,[status(thm)],[4780,696,theory(equality)])).
% cnf(6242,plain,(h4(op1(e10,e11))!=op2(e20,e21)|h4(op1(e10,e12))!=op2(e20,e22)|h4(op1(e10,e13))!=op2(e20,e23)|h4(op1(e11,e10))!=op2(e21,e20)|h4(op1(e11,e11))!=e20|h4(op1(e11,e12))!=op2(e21,e22)|h4(op1(e11,e13))!=op2(e21,e23)|h4(op1(e12,e10))!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[4781,1081,theory(equality)])).
% cnf(6307,plain,(op2(e21,e22)=e21|e20=e21|op2(e21,e20)=e21),inference(rw,[status(thm)],[1046,1081,theory(equality)])).
% cnf(6308,plain,(op2(e21,e22)=e21|op2(e21,e20)=e21),inference(sr,[status(thm)],[6307,228,theory(equality)])).
% cnf(6319,plain,(op2(e22,e21)!=e20),inference(rw,[status(thm)],[207,1081,theory(equality)])).
% cnf(6322,plain,(e20!=op2(e21,e20)),inference(rw,[status(thm)],[186,1081,theory(equality)])).
% cnf(6328,plain,(op1(e10,e10)=e11),inference(csr,[status(thm)],[711,832])).
% cnf(6354,plain,(e11!=op1(e13,e10)),inference(rw,[status(thm)],[166,6328,theory(equality)])).
% cnf(6360,plain,(op1(e11,e11)=e10|e11=e10),inference(rw,[status(thm)],[719,6328,theory(equality)])).
% cnf(6361,plain,(op1(e11,e11)=e10),inference(sr,[status(thm)],[6360,222,theory(equality)])).
% cnf(6371,plain,(op2(e21,e20)=e23|op2(e21,e20)=e22|op2(e21,e20)=e20),inference(sr,[status(thm)],[84,1066,theory(equality)])).
% cnf(6373,plain,(op1(e13,e10)=e13),inference(sr,[status(thm)],[797,6354,theory(equality)])).
% cnf(6374,plain,(op1(e13,e11)=e11),inference(sr,[status(thm)],[803,6354,theory(equality)])).
% cnf(6385,plain,(e11=e13|op1(e12,e11)=e13|op1(e11,e11)=e13|op1(e10,e11)=e13),inference(rw,[status(thm)],[57,6374,theory(equality)])).
% cnf(6386,plain,(op1(e12,e11)=e13|op1(e11,e11)=e13|op1(e10,e11)=e13),inference(sr,[status(thm)],[6385,218,theory(equality)])).
% cnf(6387,plain,(op1(e12,e11)=e13|e10=e13|op1(e10,e11)=e13),inference(rw,[status(thm)],[6386,6361,theory(equality)])).
% cnf(6388,plain,(op1(e12,e11)=e13|op1(e10,e11)=e13),inference(sr,[status(thm)],[6387,220,theory(equality)])).
% cnf(6394,plain,(op1(e11,e12)=e11|e10=e11),inference(rw,[status(thm)],[909,6361,theory(equality)])).
% cnf(6395,plain,(op1(e11,e12)=e11),inference(sr,[status(thm)],[6394,222,theory(equality)])).
% cnf(6405,plain,(e11=e12|op1(e11,e11)=e12|op1(e11,e10)=e12),inference(rw,[status(thm)],[768,6395,theory(equality)])).
% cnf(6406,plain,(op1(e11,e11)=e12|op1(e11,e10)=e12),inference(sr,[status(thm)],[6405,219,theory(equality)])).
% cnf(6407,plain,(e10=e12|op1(e11,e10)=e12),inference(rw,[status(thm)],[6406,6361,theory(equality)])).
% cnf(6408,plain,(op1(e11,e10)=e12),inference(sr,[status(thm)],[6407,221,theory(equality)])).
% cnf(6414,plain,(op1(e10,e13)=e10|op1(e10,e11)=e10|e11=e10),inference(rw,[status(thm)],[714,6328,theory(equality)])).
% cnf(6415,plain,(op1(e10,e13)=e10|e11=e10),inference(sr,[status(thm)],[6414,913,theory(equality)])).
% cnf(6416,plain,(op1(e10,e13)=e10),inference(sr,[status(thm)],[6415,222,theory(equality)])).
% cnf(6417,plain,(op1(e12,e12)=e13|op1(e11,e11)=e13|$false),inference(rw,[status(thm)],[857,6416,theory(equality)])).
% cnf(6418,plain,(op1(e12,e12)=e13|op1(e11,e11)=e13),inference(cn,[status(thm)],[6417,theory(equality)])).
% cnf(6419,plain,(op1(e12,e12)=e13|e10=e13),inference(rw,[status(thm)],[6418,6361,theory(equality)])).
% cnf(6420,plain,(op1(e12,e12)=e13),inference(sr,[status(thm)],[6419,220,theory(equality)])).
% cnf(6421,plain,(op1(e11,e13)=e13|e10=e13),inference(rw,[status(thm)],[763,6416,theory(equality)])).
% cnf(6422,plain,(op1(e11,e13)=e13),inference(sr,[status(thm)],[6421,220,theory(equality)])).
% cnf(6437,plain,(e13=e12|op1(e12,e11)=e12|op1(e12,e10)=e12),inference(rw,[status(thm)],[783,6420,theory(equality)])).
% cnf(6438,plain,(op1(e12,e11)=e12|op1(e12,e10)=e12),inference(sr,[status(thm)],[6437,217,theory(equality)])).
% cnf(6440,plain,(e13=e12|op1(e11,e12)=e12|op1(e10,e12)=e12),inference(rw,[status(thm)],[731,6420,theory(equality)])).
% cnf(6441,plain,(op1(e11,e12)=e12|op1(e10,e12)=e12),inference(sr,[status(thm)],[6440,217,theory(equality)])).
% cnf(6442,plain,(e11=e12|op1(e10,e12)=e12),inference(rw,[status(thm)],[6441,6395,theory(equality)])).
% cnf(6443,plain,(op1(e10,e12)=e12),inference(sr,[status(thm)],[6442,219,theory(equality)])).
% cnf(6453,plain,(op1(e12,e10)=e10|e12=e10|op1(e10,e10)=e10),inference(rw,[status(thm)],[721,6408,theory(equality)])).
% cnf(6454,plain,(op1(e12,e10)=e10|e12=e10|e11=e10),inference(rw,[status(thm)],[6453,6328,theory(equality)])).
% cnf(6455,plain,(op1(e12,e10)=e10|e11=e10),inference(sr,[status(thm)],[6454,221,theory(equality)])).
% cnf(6456,plain,(op1(e12,e10)=e10),inference(sr,[status(thm)],[6455,222,theory(equality)])).
% cnf(6477,plain,(op1(e12,e11)=e12|e10=e12),inference(rw,[status(thm)],[6438,6456,theory(equality)])).
% cnf(6478,plain,(op1(e12,e11)=e12),inference(sr,[status(thm)],[6477,221,theory(equality)])).
% cnf(6481,plain,(op1(e10,e11)=e13|e12=e13),inference(rw,[status(thm)],[6388,6478,theory(equality)])).
% cnf(6482,plain,(op1(e10,e11)=e13),inference(sr,[status(thm)],[6481,217,theory(equality)])).
% cnf(6496,plain,(op2(e23,e20)=e23),inference(sr,[status(thm)],[1031,1091,theory(equality)])).
% cnf(6497,plain,(op2(e23,e21)=e21),inference(sr,[status(thm)],[1037,1091,theory(equality)])).
% cnf(6512,plain,(e23!=op2(e21,e20)),inference(rw,[status(thm)],[212,6496,theory(equality)])).
% cnf(6519,plain,(op2(e22,e22)=e23|e20=e23),inference(rw,[status(thm)],[1068,1081,theory(equality)])).
% cnf(6520,plain,(op2(e22,e22)=e23),inference(sr,[status(thm)],[6519,226,theory(equality)])).
% cnf(6540,plain,(op2(e20,e23)=e20),inference(sr,[status(thm)],[1085,1165,theory(equality)])).
% cnf(6541,plain,(op2(e21,e23)=e23|e20=e23),inference(rw,[status(thm)],[961,6540,theory(equality)])).
% cnf(6542,plain,(op2(e21,e23)=e23),inference(sr,[status(thm)],[6541,226,theory(equality)])).
% cnf(6563,plain,(e20=e23|op2(e20,e22)=e23|op2(e20,e21)=e23),inference(rw,[status(thm)],[1072,6540,theory(equality)])).
% cnf(6564,plain,(op2(e20,e22)=e23|op2(e20,e21)=e23),inference(sr,[status(thm)],[6563,226,theory(equality)])).
% cnf(6569,plain,(op2(e21,e22)=e21),inference(sr,[status(thm)],[6308,1066,theory(equality)])).
% cnf(6572,plain,(op2(e22,e22)=e22|e21=e22|op2(e20,e22)=e22),inference(rw,[status(thm)],[991,6569,theory(equality)])).
% cnf(6573,plain,(op2(e22,e22)=e22|op2(e20,e22)=e22),inference(sr,[status(thm)],[6572,225,theory(equality)])).
% cnf(6574,plain,(e23=e22|op2(e20,e22)=e22),inference(rw,[status(thm)],[6573,6520,theory(equality)])).
% cnf(6575,plain,(op2(e20,e22)=e22),inference(sr,[status(thm)],[6574,223,theory(equality)])).
% cnf(6766,plain,(op2(e22,e20)=e20),inference(sr,[status(thm)],[1123,6319,theory(equality)])).
% cnf(6773,plain,(op2(e22,e22)=e22|op2(e22,e21)=e22|e20=e22),inference(rw,[status(thm)],[1142,6766,theory(equality)])).
% cnf(6774,plain,(op2(e22,e22)=e22|op2(e22,e21)=e22),inference(sr,[status(thm)],[6773,227,theory(equality)])).
% cnf(6775,plain,(e23=e22|op2(e22,e21)=e22),inference(rw,[status(thm)],[6774,6520,theory(equality)])).
% cnf(6776,plain,(op2(e22,e21)=e22),inference(sr,[status(thm)],[6775,223,theory(equality)])).
% cnf(6874,plain,(e23!=op2(e20,e21)|h4(op1(e10,e12))!=op2(e20,e22)|h4(op1(e10,e13))!=op2(e20,e23)|h4(op1(e11,e10))!=op2(e21,e20)|h4(op1(e11,e11))!=e20|h4(op1(e11,e12))!=op2(e21,e22)|h4(op1(e11,e13))!=op2(e21,e23)|h4(op1(e12,e10))!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6242,6482,theory(equality)]),396,theory(equality)])).
% cnf(6875,plain,(e23!=op2(e20,e21)|e22!=op2(e20,e22)|h4(op1(e10,e13))!=op2(e20,e23)|h4(op1(e11,e10))!=op2(e21,e20)|h4(op1(e11,e11))!=e20|h4(op1(e11,e12))!=op2(e21,e22)|h4(op1(e11,e13))!=op2(e21,e23)|h4(op1(e12,e10))!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6874,6443,theory(equality)]),679,theory(equality)])).
% cnf(6876,plain,(e23!=op2(e20,e21)|$false|h4(op1(e10,e13))!=op2(e20,e23)|h4(op1(e11,e10))!=op2(e21,e20)|h4(op1(e11,e11))!=e20|h4(op1(e11,e12))!=op2(e21,e22)|h4(op1(e11,e13))!=op2(e21,e23)|h4(op1(e12,e10))!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[6875,6575,theory(equality)])).
% cnf(6877,plain,(e23!=op2(e20,e21)|$false|e20!=op2(e20,e23)|h4(op1(e11,e10))!=op2(e21,e20)|h4(op1(e11,e11))!=e20|h4(op1(e11,e12))!=op2(e21,e22)|h4(op1(e11,e13))!=op2(e21,e23)|h4(op1(e12,e10))!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6876,6416,theory(equality)]),684,theory(equality)])).
% cnf(6878,plain,(e23!=op2(e20,e21)|$false|$false|h4(op1(e11,e10))!=op2(e21,e20)|h4(op1(e11,e11))!=e20|h4(op1(e11,e12))!=op2(e21,e22)|h4(op1(e11,e13))!=op2(e21,e23)|h4(op1(e12,e10))!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[6877,6540,theory(equality)])).
% cnf(6879,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|h4(op1(e11,e11))!=e20|h4(op1(e11,e12))!=op2(e21,e22)|h4(op1(e11,e13))!=op2(e21,e23)|h4(op1(e12,e10))!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6878,6408,theory(equality)]),679,theory(equality)])).
% cnf(6880,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|h4(op1(e11,e12))!=op2(e21,e22)|h4(op1(e11,e13))!=op2(e21,e23)|h4(op1(e12,e10))!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6879,6361,theory(equality)]),684,theory(equality)])).
% cnf(6881,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|e21!=op2(e21,e22)|h4(op1(e11,e13))!=op2(e21,e23)|h4(op1(e12,e10))!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6880,6395,theory(equality)]),687,theory(equality)])).
% cnf(6882,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|h4(op1(e11,e13))!=op2(e21,e23)|h4(op1(e12,e10))!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[6881,6569,theory(equality)])).
% cnf(6883,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|e23!=op2(e21,e23)|h4(op1(e12,e10))!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6882,6422,theory(equality)]),396,theory(equality)])).
% cnf(6884,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|$false|h4(op1(e12,e10))!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[6883,6542,theory(equality)])).
% cnf(6885,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|$false|e20!=op2(e22,e20)|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6884,6456,theory(equality)]),684,theory(equality)])).
% cnf(6886,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|$false|$false|h4(op1(e12,e11))!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[6885,6766,theory(equality)])).
% cnf(6887,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|$false|$false|e22!=op2(e22,e21)|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6886,6478,theory(equality)]),679,theory(equality)])).
% cnf(6888,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|$false|$false|$false|h4(op1(e12,e12))!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[6887,6776,theory(equality)])).
% cnf(6889,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|$false|$false|$false|e23!=op2(e22,e22)|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6888,6420,theory(equality)]),396,theory(equality)])).
% cnf(6890,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|$false|$false|$false|$false|h4(op1(e13,e10))!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[6889,6520,theory(equality)])).
% cnf(6891,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|$false|$false|$false|$false|e23!=op2(e23,e20)|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6890,6373,theory(equality)]),396,theory(equality)])).
% cnf(6892,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|$false|$false|$false|$false|$false|h4(op1(e13,e11))!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[6891,6496,theory(equality)])).
% cnf(6893,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|$false|$false|$false|$false|$false|e21!=op2(e23,e21)|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6892,6374,theory(equality)]),687,theory(equality)])).
% cnf(6894,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|$false|$false|$false|$false|$false|$false|h4(op1(e10,e10))!=e21),inference(rw,[status(thm)],[6893,6497,theory(equality)])).
% cnf(6895,plain,(e23!=op2(e20,e21)|$false|$false|e22!=op2(e21,e20)|$false|$false|$false|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[inference(rw,[status(thm)],[6894,6328,theory(equality)]),687,theory(equality)])).
% cnf(6896,plain,(e23!=op2(e20,e21)|e22!=op2(e21,e20)),inference(cn,[status(thm)],[6895,theory(equality)])).
% cnf(6899,plain,(op2(e21,e20)=e20|op2(e21,e20)=e22),inference(sr,[status(thm)],[6371,6512,theory(equality)])).
% cnf(6960,plain,(op2(e21,e20)=e22),inference(sr,[status(thm)],[6899,6322,theory(equality)])).
% cnf(6965,plain,(op2(e20,e21)!=e23|$false),inference(rw,[status(thm)],[6896,6960,theory(equality)])).
% cnf(6966,plain,(op2(e20,e21)!=e23),inference(cn,[status(thm)],[6965,theory(equality)])).
% cnf(7021,plain,(op2(e20,e22)=e23),inference(sr,[status(thm)],[6564,6966,theory(equality)])).
% cnf(7022,plain,(e22=e23),inference(rw,[status(thm)],[7021,6575,theory(equality)])).
% cnf(7023,plain,($false),inference(sr,[status(thm)],[7022,223,theory(equality)])).
% cnf(7024,plain,($false),7023,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 823
% # ...of these trivial : 55
% # ...subsumed : 375
% # ...remaining for further processing: 393
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 68
% # Backward-rewritten : 215
% # Generated clauses : 28
% # ...of the previous two non-trivial : 203
% # Contextual simplify-reflections : 181
% # Paramodulations : 0
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 82
% # Positive orientable unit clauses: 47
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 33
% # Non-unit-clauses : 2
% # Current number of unprocessed clauses: 22
% # ...number of literals in the above : 119
% # Clause-clause subsumption calls (NU) : 4766
% # Rec. Clause-clause subsumption calls : 363
% # Unit Clause-clause subsumption calls : 286
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 31
% # Indexed BW rewrite successes : 31
% # Backwards rewriting index: 60 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-from index: 47 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 58 leaves, 1.00+/-0.000 terms/leaf
% # -------------------------------------------------
% # User time : 0.314 s
% # System time : 0.016 s
% # Total time : 0.330 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.84 CPU 0.96 WC
% FINAL PrfWatch: 0.84 CPU 0.96 WC
% SZS output end Solution for /tmp/SystemOnTPTP7966/ALG117+1.tptp
%
%------------------------------------------------------------------------------