%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : ALG110+1 : TPTP v5.0.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art05.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 : Sat Dec 25 03:54:22 EST 2010
% Result : Theorem 1.08s
% Output : CNFRefutation 1.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 20
% Syntax : Number of formulae : 386 ( 126 unt; 0 def)
% Number of atoms : 4371 (4085 equ)
% Maximal formula atoms : 1280 ( 11 avg)
% Number of connectives : 6458 (2473 ~;3278 |; 703 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 84 ( 6 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,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/tmpJUyMAT/sel_ALG110+1.p_1',ax2) ).
fof(2,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/tmpJUyMAT/sel_ALG110+1.p_1',ax3) ).
fof(3,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/tmpJUyMAT/sel_ALG110+1.p_1',ax1) ).
fof(4,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/tmpJUyMAT/sel_ALG110+1.p_1',ax6) ).
fof(5,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/tmp/tmpJUyMAT/sel_ALG110+1.p_1',ax7) ).
fof(6,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/tmpJUyMAT/sel_ALG110+1.p_1',ax4) ).
fof(7,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/tmpJUyMAT/sel_ALG110+1.p_1',ax5) ).
fof(8,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/tmp/tmpJUyMAT/sel_ALG110+1.p_1',ax8) ).
fof(10,axiom,
( h1(e12) = e20
& h1(e10) = op2(op2(e20,e20),op2(e20,e20))
& h1(e11) = op2(op2(op2(e20,e20),op2(e20,e20)),op2(e20,e20))
& h1(e13) = op2(e20,e20) ),
file('/tmp/tmpJUyMAT/sel_ALG110+1.p_1',ax14) ).
fof(11,axiom,
( h2(e12) = e21
& h2(e10) = op2(op2(e21,e21),op2(e21,e21))
& h2(e11) = op2(op2(op2(e21,e21),op2(e21,e21)),op2(e21,e21))
& h2(e13) = op2(e21,e21) ),
file('/tmp/tmpJUyMAT/sel_ALG110+1.p_1',ax15) ).
fof(13,axiom,
( h4(e12) = e23
& h4(e10) = op2(op2(e23,e23),op2(e23,e23))
& h4(e11) = op2(op2(op2(e23,e23),op2(e23,e23)),op2(e23,e23))
& h4(e13) = op2(e23,e23) ),
file('/tmp/tmpJUyMAT/sel_ALG110+1.p_1',ax17) ).
fof(14,axiom,
( ( ( op1(e10,e10) = e10
& op1(e10,e10) != e10 )
| ( op1(e11,e10) = e11
& op1(e10,e11) != e10 )
| ( op1(e12,e10) = e12
& op1(e10,e12) != e10 )
| ( op1(e13,e10) = e13
& op1(e10,e13) != e10 ) )
& ( ( op1(e10,e11) = e10
& op1(e11,e10) != e11 )
| ( op1(e11,e11) = e11
& op1(e11,e11) != e11 )
| ( op1(e12,e11) = e12
& op1(e11,e12) != e11 )
| ( op1(e13,e11) = e13
& op1(e11,e13) != e11 ) )
& ( ( op1(e10,e12) = e10
& op1(e12,e10) != e12 )
| ( op1(e11,e12) = e11
& op1(e12,e11) != e12 )
| ( op1(e12,e12) = e12
& op1(e12,e12) != e12 )
| ( op1(e13,e12) = e13
& op1(e12,e13) != e12 ) )
& ( ( op1(e10,e13) = e10
& op1(e13,e10) != e13 )
| ( op1(e11,e13) = e11
& op1(e13,e11) != e13 )
| ( op1(e12,e13) = e12
& op1(e13,e12) != e13 )
| ( op1(e13,e13) = e13
& op1(e13,e13) != e13 ) ) ),
file('/tmp/tmpJUyMAT/sel_ALG110+1.p_1',ax10) ).
fof(15,axiom,
( ( ( op2(e20,e20) = e20
& op2(e20,e20) != e20 )
| ( op2(e21,e20) = e21
& op2(e20,e21) != e20 )
| ( op2(e22,e20) = e22
& op2(e20,e22) != e20 )
| ( op2(e23,e20) = e23
& op2(e20,e23) != e20 ) )
& ( ( op2(e20,e21) = e20
& op2(e21,e20) != e21 )
| ( op2(e21,e21) = e21
& op2(e21,e21) != e21 )
| ( op2(e22,e21) = e22
& op2(e21,e22) != e21 )
| ( op2(e23,e21) = e23
& op2(e21,e23) != e21 ) )
& ( ( op2(e20,e22) = e20
& op2(e22,e20) != e22 )
| ( op2(e21,e22) = e21
& op2(e22,e21) != e22 )
| ( op2(e22,e22) = e22
& op2(e22,e22) != e22 )
| ( op2(e23,e22) = e23
& op2(e22,e23) != e22 ) )
& ( ( op2(e20,e23) = e20
& op2(e23,e20) != e23 )
| ( op2(e21,e23) = e21
& op2(e23,e21) != e23 )
| ( op2(e22,e23) = e22
& op2(e23,e22) != e23 )
| ( op2(e23,e23) = e23
& op2(e23,e23) != e23 ) ) ),
file('/tmp/tmpJUyMAT/sel_ALG110+1.p_1',ax11) ).
fof(16,axiom,
( e10 = op1(op1(e12,e12),op1(e12,e12))
& e11 = op1(op1(op1(e12,e12),op1(e12,e12)),op1(e12,e12))
& e13 = op1(e12,e12) ),
file('/tmp/tmpJUyMAT/sel_ALG110+1.p_1',ax12) ).
fof(17,axiom,
( e20 = op2(op2(e22,e22),op2(e22,e22))
& e21 = op2(op2(op2(e22,e22),op2(e22,e22)),op2(e22,e22))
& e23 = op2(e22,e22) ),
file('/tmp/tmpJUyMAT/sel_ALG110+1.p_1',ax13) ).
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/tmpJUyMAT/sel_ALG110+1.p_1',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(25,plain,
( op1(e13,e13) = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| op1(e10,e13) = e13 ),
inference(split_conjunct,[status(thm)],[1]) ).
cnf(28,plain,
( op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 ),
inference(split_conjunct,[status(thm)],[1]) ).
cnf(35,plain,
( op1(e13,e12) = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(split_conjunct,[status(thm)],[1]) ).
cnf(37,plain,
( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(split_conjunct,[status(thm)],[1]) ).
cnf(38,plain,
( op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 ),
inference(split_conjunct,[status(thm)],[1]) ).
cnf(39,plain,
( op1(e13,e12) = e10
| op1(e12,e12) = e10
| op1(e11,e12) = e10
| op1(e10,e12) = e10 ),
inference(split_conjunct,[status(thm)],[1]) ).
cnf(40,plain,
( op1(e12,e13) = e10
| op1(e12,e12) = e10
| op1(e12,e11) = e10
| op1(e12,e10) = e10 ),
inference(split_conjunct,[status(thm)],[1]) ).
cnf(41,plain,
( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| op1(e10,e11) = e13 ),
inference(split_conjunct,[status(thm)],[1]) ).
cnf(50,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 ),
inference(split_conjunct,[status(thm)],[1]) ).
cnf(52,plain,
( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 ),
inference(split_conjunct,[status(thm)],[1]) ).
cnf(58,plain,
( op2(e23,e22) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21
| op2(e23,e22) = e20 ),
inference(split_conjunct,[status(thm)],[2]) ).
cnf(60,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 ),
inference(split_conjunct,[status(thm)],[2]) ).
cnf(83,plain,
( op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e11) = e10 ),
inference(split_conjunct,[status(thm)],[3]) ).
cnf(89,plain,
op2(e23,e22) != op2(e23,e23),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(92,plain,
op2(e23,e20) != op2(e23,e23),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(93,plain,
op2(e23,e20) != op2(e23,e22),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(94,plain,
op2(e23,e20) != op2(e23,e21),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(95,plain,
op2(e22,e22) != op2(e22,e23),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(96,plain,
op2(e22,e21) != op2(e22,e23),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(98,plain,
op2(e22,e20) != op2(e22,e23),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(108,plain,
op2(e20,e21) != op2(e20,e23),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(109,plain,
op2(e20,e21) != op2(e20,e22),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(119,plain,
op2(e22,e22) != op2(e23,e22),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(123,plain,
op2(e20,e22) != op2(e22,e22),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(124,plain,
op2(e20,e22) != op2(e21,e22),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(128,plain,
op2(e20,e21) != op2(e23,e21),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(132,plain,
op2(e21,e20) != op2(e23,e20),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(134,plain,
op2(e20,e20) != op2(e23,e20),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(137,plain,
e12 != e13,
inference(split_conjunct,[status(thm)],[5]) ).
cnf(138,plain,
e11 != e13,
inference(split_conjunct,[status(thm)],[5]) ).
cnf(139,plain,
e11 != e12,
inference(split_conjunct,[status(thm)],[5]) ).
cnf(140,plain,
e10 != e13,
inference(split_conjunct,[status(thm)],[5]) ).
cnf(141,plain,
e10 != e12,
inference(split_conjunct,[status(thm)],[5]) ).
cnf(142,plain,
e10 != e11,
inference(split_conjunct,[status(thm)],[5]) ).
cnf(143,plain,
( op2(e23,e23) = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| op2(e20,e23) = e23 ),
inference(split_conjunct,[status(thm)],[6]) ).
cnf(153,plain,
( op2(e23,e22) = e22
| op2(e22,e22) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(split_conjunct,[status(thm)],[6]) ).
cnf(157,plain,
( op2(e23,e22) = e20
| op2(e22,e22) = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 ),
inference(split_conjunct,[status(thm)],[6]) ).
cnf(158,plain,
( op2(e22,e23) = e20
| op2(e22,e22) = e20
| op2(e22,e21) = e20
| op2(e22,e20) = e20 ),
inference(split_conjunct,[status(thm)],[6]) ).
cnf(163,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| op2(e21,e21) = e21
| op2(e20,e21) = e21 ),
inference(split_conjunct,[status(thm)],[6]) ).
cnf(166,plain,
( op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20
| op2(e21,e20) = e20 ),
inference(split_conjunct,[status(thm)],[6]) ).
cnf(168,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 ),
inference(split_conjunct,[status(thm)],[6]) ).
cnf(170,plain,
( op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| op2(e20,e20) = e22 ),
inference(split_conjunct,[status(thm)],[6]) ).
cnf(175,plain,
op1(e13,e12) != op1(e13,e13),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(180,plain,
op1(e13,e10) != op1(e13,e11),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(182,plain,
op1(e12,e11) != op1(e12,e13),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(183,plain,
op1(e12,e11) != op1(e12,e12),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(184,plain,
op1(e12,e10) != op1(e12,e13),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(188,plain,
op1(e11,e11) != op1(e11,e13),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(191,plain,
op1(e11,e10) != op1(e11,e12),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(192,plain,
op1(e11,e10) != op1(e11,e11),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(193,plain,
op1(e10,e12) != op1(e10,e13),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(204,plain,
op1(e10,e13) != op1(e11,e13),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(209,plain,
op1(e10,e12) != op1(e12,e12),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(214,plain,
op1(e10,e11) != op1(e13,e11),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(216,plain,
op1(e10,e11) != op1(e11,e11),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(219,plain,
op1(e11,e10) != op1(e12,e10),
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]) ).
cnf(245,plain,
h1(e13) = op2(e20,e20),
inference(split_conjunct,[status(thm)],[10]) ).
cnf(249,plain,
h2(e13) = op2(e21,e21),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(250,plain,
h2(e11) = op2(op2(op2(e21,e21),op2(e21,e21)),op2(e21,e21)),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(251,plain,
h2(e10) = op2(op2(e21,e21),op2(e21,e21)),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(252,plain,
h2(e12) = e21,
inference(split_conjunct,[status(thm)],[11]) ).
cnf(257,plain,
h4(e13) = op2(e23,e23),
inference(split_conjunct,[status(thm)],[13]) ).
cnf(258,plain,
h4(e11) = op2(op2(op2(e23,e23),op2(e23,e23)),op2(e23,e23)),
inference(split_conjunct,[status(thm)],[13]) ).
fof(261,plain,
( ( op1(e13,e10) = e13
| op1(e12,e10) = e12
| op1(e11,e10) = e11
| op1(e10,e10) = e10 )
& ( op1(e10,e13) != e10
| op1(e12,e10) = e12
| op1(e11,e10) = e11
| op1(e10,e10) = e10 )
& ( op1(e13,e10) = e13
| op1(e10,e12) != e10
| op1(e11,e10) = e11
| op1(e10,e10) = e10 )
& ( op1(e10,e13) != e10
| op1(e10,e12) != e10
| op1(e11,e10) = e11
| op1(e10,e10) = e10 )
& ( op1(e13,e10) = e13
| op1(e12,e10) = e12
| op1(e10,e11) != e10
| op1(e10,e10) = e10 )
& ( op1(e10,e13) != e10
| op1(e12,e10) = e12
| op1(e10,e11) != e10
| op1(e10,e10) = e10 )
& ( op1(e13,e10) = e13
| op1(e10,e12) != e10
| op1(e10,e11) != e10
| op1(e10,e10) = e10 )
& ( op1(e10,e13) != e10
| op1(e10,e12) != e10
| op1(e10,e11) != e10
| op1(e10,e10) = e10 )
& ( op1(e13,e10) = e13
| op1(e12,e10) = e12
| op1(e11,e10) = e11
| op1(e10,e10) != e10 )
& ( op1(e10,e13) != e10
| op1(e12,e10) = e12
| op1(e11,e10) = e11
| op1(e10,e10) != e10 )
& ( op1(e13,e10) = e13
| op1(e10,e12) != e10
| op1(e11,e10) = e11
| op1(e10,e10) != e10 )
& ( op1(e10,e13) != e10
| op1(e10,e12) != e10
| op1(e11,e10) = e11
| op1(e10,e10) != e10 )
& ( op1(e13,e10) = e13
| op1(e12,e10) = e12
| op1(e10,e11) != e10
| op1(e10,e10) != e10 )
& ( op1(e10,e13) != e10
| op1(e12,e10) = e12
| op1(e10,e11) != e10
| op1(e10,e10) != e10 )
& ( op1(e13,e10) = e13
| op1(e10,e12) != e10
| op1(e10,e11) != e10
| op1(e10,e10) != e10 )
& ( op1(e10,e13) != e10
| op1(e10,e12) != e10
| op1(e10,e11) != e10
| op1(e10,e10) != e10 )
& ( op1(e13,e11) = e13
| op1(e12,e11) = e12
| op1(e11,e11) = e11
| op1(e10,e11) = e10 )
& ( op1(e11,e13) != e11
| op1(e12,e11) = e12
| op1(e11,e11) = e11
| op1(e10,e11) = e10 )
& ( op1(e13,e11) = e13
| op1(e11,e12) != e11
| op1(e11,e11) = e11
| op1(e10,e11) = e10 )
& ( op1(e11,e13) != e11
| op1(e11,e12) != e11
| 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(e11,e13) != e11
| op1(e12,e11) = e12
| op1(e11,e11) != e11
| op1(e10,e11) = e10 )
& ( op1(e13,e11) = e13
| op1(e11,e12) != e11
| op1(e11,e11) != e11
| op1(e10,e11) = e10 )
& ( op1(e11,e13) != e11
| op1(e11,e12) != e11
| op1(e11,e11) != e11
| op1(e10,e11) = e10 )
& ( op1(e13,e11) = e13
| op1(e12,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e10) != e11 )
& ( op1(e11,e13) != e11
| op1(e12,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e10) != e11 )
& ( op1(e13,e11) = e13
| op1(e11,e12) != e11
| op1(e11,e11) = e11
| op1(e11,e10) != e11 )
& ( op1(e11,e13) != e11
| op1(e11,e12) != e11
| op1(e11,e11) = e11
| op1(e11,e10) != e11 )
& ( op1(e13,e11) = e13
| op1(e12,e11) = e12
| op1(e11,e11) != e11
| op1(e11,e10) != e11 )
& ( op1(e11,e13) != e11
| op1(e12,e11) = e12
| op1(e11,e11) != e11
| op1(e11,e10) != e11 )
& ( op1(e13,e11) = e13
| op1(e11,e12) != e11
| op1(e11,e11) != e11
| op1(e11,e10) != e11 )
& ( op1(e11,e13) != e11
| op1(e11,e12) != e11
| op1(e11,e11) != e11
| op1(e11,e10) != e11 )
& ( op1(e13,e12) = e13
| op1(e12,e12) = e12
| op1(e11,e12) = e11
| op1(e10,e12) = e10 )
& ( op1(e12,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(e12,e13) != e12
| op1(e12,e12) != e12
| op1(e11,e12) = e11
| op1(e10,e12) = e10 )
& ( op1(e13,e12) = e13
| op1(e12,e12) = e12
| op1(e12,e11) != e12
| op1(e10,e12) = e10 )
& ( op1(e12,e13) != e12
| op1(e12,e12) = e12
| op1(e12,e11) != e12
| op1(e10,e12) = e10 )
& ( op1(e13,e12) = e13
| op1(e12,e12) != e12
| op1(e12,e11) != e12
| op1(e10,e12) = e10 )
& ( op1(e12,e13) != e12
| op1(e12,e12) != e12
| op1(e12,e11) != e12
| op1(e10,e12) = e10 )
& ( op1(e13,e12) = e13
| op1(e12,e12) = e12
| op1(e11,e12) = e11
| op1(e12,e10) != e12 )
& ( op1(e12,e13) != e12
| op1(e12,e12) = e12
| op1(e11,e12) = e11
| op1(e12,e10) != e12 )
& ( op1(e13,e12) = e13
| op1(e12,e12) != e12
| op1(e11,e12) = e11
| op1(e12,e10) != e12 )
& ( op1(e12,e13) != e12
| op1(e12,e12) != e12
| op1(e11,e12) = e11
| op1(e12,e10) != e12 )
& ( op1(e13,e12) = e13
| op1(e12,e12) = e12
| op1(e12,e11) != e12
| op1(e12,e10) != e12 )
& ( op1(e12,e13) != e12
| op1(e12,e12) = e12
| op1(e12,e11) != e12
| op1(e12,e10) != e12 )
& ( op1(e13,e12) = e13
| op1(e12,e12) != e12
| op1(e12,e11) != e12
| op1(e12,e10) != e12 )
& ( op1(e12,e13) != e12
| op1(e12,e12) != e12
| op1(e12,e11) != e12
| op1(e12,e10) != e12 )
& ( 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 )
& ( op1(e13,e13) = e13
| op1(e13,e12) != e13
| op1(e11,e13) = e11
| op1(e10,e13) = e10 )
& ( op1(e13,e13) != e13
| op1(e13,e12) != e13
| op1(e11,e13) = e11
| op1(e10,e13) = e10 )
& ( op1(e13,e13) = e13
| op1(e12,e13) = e12
| op1(e13,e11) != e13
| op1(e10,e13) = e10 )
& ( op1(e13,e13) != e13
| op1(e12,e13) = e12
| op1(e13,e11) != e13
| op1(e10,e13) = e10 )
& ( op1(e13,e13) = e13
| op1(e13,e12) != e13
| op1(e13,e11) != e13
| op1(e10,e13) = e10 )
& ( op1(e13,e13) != e13
| op1(e13,e12) != e13
| op1(e13,e11) != e13
| op1(e10,e13) = e10 )
& ( op1(e13,e13) = e13
| op1(e12,e13) = e12
| op1(e11,e13) = e11
| op1(e13,e10) != e13 )
& ( op1(e13,e13) != e13
| op1(e12,e13) = e12
| op1(e11,e13) = e11
| op1(e13,e10) != e13 )
& ( op1(e13,e13) = e13
| op1(e13,e12) != e13
| op1(e11,e13) = e11
| op1(e13,e10) != e13 )
& ( op1(e13,e13) != e13
| op1(e13,e12) != e13
| op1(e11,e13) = e11
| op1(e13,e10) != e13 )
& ( op1(e13,e13) = e13
| op1(e12,e13) = e12
| op1(e13,e11) != e13
| op1(e13,e10) != e13 )
& ( op1(e13,e13) != e13
| op1(e12,e13) = e12
| op1(e13,e11) != e13
| op1(e13,e10) != e13 )
& ( op1(e13,e13) = e13
| op1(e13,e12) != e13
| op1(e13,e11) != e13
| op1(e13,e10) != e13 )
& ( op1(e13,e13) != e13
| op1(e13,e12) != e13
| op1(e13,e11) != e13
| op1(e13,e10) != e13 ) ),
inference(distribute,[status(thm)],[14]) ).
cnf(277,plain,
( op1(e10,e13) = e10
| op1(e11,e13) = e11
| op1(e12,e13) = e12
| op1(e13,e13) = e13 ),
inference(split_conjunct,[status(thm)],[261]) ).
cnf(292,plain,
( op1(e10,e12) = e10
| op1(e11,e12) = e11
| op1(e12,e12) = e12
| op1(e12,e13) != e12 ),
inference(split_conjunct,[status(thm)],[261]) ).
cnf(305,plain,
( op1(e10,e11) = e10
| op1(e12,e11) = e12
| op1(e13,e11) = e13
| op1(e11,e11) != e11 ),
inference(split_conjunct,[status(thm)],[261]) ).
cnf(309,plain,
( op1(e10,e11) = e10
| op1(e11,e11) = e11
| op1(e12,e11) = e12
| op1(e13,e11) = e13 ),
inference(split_conjunct,[status(thm)],[261]) ).
cnf(317,plain,
( op1(e11,e10) = e11
| op1(e12,e10) = e12
| op1(e13,e10) = e13
| op1(e10,e10) != e10 ),
inference(split_conjunct,[status(thm)],[261]) ).
cnf(325,plain,
( op1(e10,e10) = e10
| op1(e11,e10) = e11
| op1(e12,e10) = e12
| op1(e13,e10) = e13 ),
inference(split_conjunct,[status(thm)],[261]) ).
fof(326,plain,
( ( op2(e23,e20) = e23
| op2(e22,e20) = e22
| op2(e21,e20) = e21
| op2(e20,e20) = e20 )
& ( op2(e20,e23) != e20
| op2(e22,e20) = e22
| op2(e21,e20) = e21
| op2(e20,e20) = e20 )
& ( op2(e23,e20) = e23
| op2(e20,e22) != e20
| op2(e21,e20) = e21
| op2(e20,e20) = e20 )
& ( op2(e20,e23) != e20
| op2(e20,e22) != e20
| op2(e21,e20) = e21
| op2(e20,e20) = e20 )
& ( op2(e23,e20) = e23
| op2(e22,e20) = e22
| op2(e20,e21) != e20
| op2(e20,e20) = e20 )
& ( op2(e20,e23) != e20
| op2(e22,e20) = e22
| op2(e20,e21) != e20
| op2(e20,e20) = e20 )
& ( op2(e23,e20) = e23
| op2(e20,e22) != e20
| op2(e20,e21) != e20
| op2(e20,e20) = e20 )
& ( op2(e20,e23) != e20
| op2(e20,e22) != e20
| op2(e20,e21) != e20
| op2(e20,e20) = e20 )
& ( op2(e23,e20) = e23
| op2(e22,e20) = e22
| op2(e21,e20) = e21
| op2(e20,e20) != e20 )
& ( op2(e20,e23) != e20
| op2(e22,e20) = e22
| op2(e21,e20) = e21
| op2(e20,e20) != e20 )
& ( op2(e23,e20) = e23
| op2(e20,e22) != e20
| op2(e21,e20) = e21
| op2(e20,e20) != e20 )
& ( op2(e20,e23) != e20
| op2(e20,e22) != e20
| op2(e21,e20) = e21
| op2(e20,e20) != e20 )
& ( op2(e23,e20) = e23
| op2(e22,e20) = e22
| op2(e20,e21) != e20
| op2(e20,e20) != e20 )
& ( op2(e20,e23) != e20
| op2(e22,e20) = e22
| op2(e20,e21) != e20
| op2(e20,e20) != e20 )
& ( op2(e23,e20) = e23
| op2(e20,e22) != e20
| op2(e20,e21) != e20
| op2(e20,e20) != e20 )
& ( op2(e20,e23) != e20
| op2(e20,e22) != e20
| op2(e20,e21) != e20
| op2(e20,e20) != e20 )
& ( op2(e23,e21) = e23
| op2(e22,e21) = e22
| op2(e21,e21) = e21
| op2(e20,e21) = e20 )
& ( op2(e21,e23) != e21
| op2(e22,e21) = e22
| op2(e21,e21) = e21
| op2(e20,e21) = e20 )
& ( op2(e23,e21) = e23
| op2(e21,e22) != e21
| op2(e21,e21) = e21
| op2(e20,e21) = e20 )
& ( op2(e21,e23) != e21
| op2(e21,e22) != e21
| 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(e21,e23) != e21
| op2(e22,e21) = e22
| op2(e21,e21) != e21
| op2(e20,e21) = e20 )
& ( op2(e23,e21) = e23
| op2(e21,e22) != e21
| op2(e21,e21) != e21
| op2(e20,e21) = e20 )
& ( op2(e21,e23) != e21
| op2(e21,e22) != e21
| op2(e21,e21) != e21
| op2(e20,e21) = e20 )
& ( op2(e23,e21) = e23
| op2(e22,e21) = e22
| op2(e21,e21) = e21
| op2(e21,e20) != e21 )
& ( op2(e21,e23) != e21
| op2(e22,e21) = e22
| op2(e21,e21) = e21
| op2(e21,e20) != e21 )
& ( op2(e23,e21) = e23
| op2(e21,e22) != e21
| op2(e21,e21) = e21
| op2(e21,e20) != e21 )
& ( op2(e21,e23) != e21
| op2(e21,e22) != e21
| op2(e21,e21) = e21
| op2(e21,e20) != e21 )
& ( op2(e23,e21) = e23
| op2(e22,e21) = e22
| op2(e21,e21) != e21
| op2(e21,e20) != e21 )
& ( op2(e21,e23) != e21
| op2(e22,e21) = e22
| op2(e21,e21) != e21
| op2(e21,e20) != e21 )
& ( op2(e23,e21) = e23
| op2(e21,e22) != e21
| op2(e21,e21) != e21
| op2(e21,e20) != e21 )
& ( op2(e21,e23) != e21
| op2(e21,e22) != e21
| op2(e21,e21) != e21
| op2(e21,e20) != e21 )
& ( op2(e23,e22) = e23
| op2(e22,e22) = e22
| op2(e21,e22) = e21
| op2(e20,e22) = e20 )
& ( op2(e22,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(e22,e23) != e22
| op2(e22,e22) != e22
| op2(e21,e22) = e21
| op2(e20,e22) = e20 )
& ( op2(e23,e22) = e23
| op2(e22,e22) = e22
| op2(e22,e21) != e22
| op2(e20,e22) = e20 )
& ( op2(e22,e23) != e22
| op2(e22,e22) = e22
| op2(e22,e21) != e22
| op2(e20,e22) = e20 )
& ( op2(e23,e22) = e23
| op2(e22,e22) != e22
| op2(e22,e21) != e22
| op2(e20,e22) = e20 )
& ( op2(e22,e23) != e22
| op2(e22,e22) != e22
| op2(e22,e21) != e22
| op2(e20,e22) = e20 )
& ( op2(e23,e22) = e23
| op2(e22,e22) = e22
| op2(e21,e22) = e21
| op2(e22,e20) != e22 )
& ( op2(e22,e23) != e22
| op2(e22,e22) = e22
| op2(e21,e22) = e21
| op2(e22,e20) != e22 )
& ( op2(e23,e22) = e23
| op2(e22,e22) != e22
| op2(e21,e22) = e21
| op2(e22,e20) != e22 )
& ( op2(e22,e23) != e22
| op2(e22,e22) != e22
| op2(e21,e22) = e21
| op2(e22,e20) != e22 )
& ( op2(e23,e22) = e23
| op2(e22,e22) = e22
| op2(e22,e21) != e22
| op2(e22,e20) != e22 )
& ( op2(e22,e23) != e22
| op2(e22,e22) = e22
| op2(e22,e21) != e22
| op2(e22,e20) != e22 )
& ( op2(e23,e22) = e23
| op2(e22,e22) != e22
| op2(e22,e21) != e22
| op2(e22,e20) != e22 )
& ( op2(e22,e23) != e22
| op2(e22,e22) != e22
| op2(e22,e21) != e22
| op2(e22,e20) != e22 )
& ( 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 )
& ( op2(e23,e23) = e23
| op2(e23,e22) != e23
| op2(e21,e23) = e21
| op2(e20,e23) = e20 )
& ( op2(e23,e23) != e23
| op2(e23,e22) != e23
| op2(e21,e23) = e21
| op2(e20,e23) = e20 )
& ( op2(e23,e23) = e23
| op2(e22,e23) = e22
| op2(e23,e21) != e23
| op2(e20,e23) = e20 )
& ( op2(e23,e23) != e23
| op2(e22,e23) = e22
| op2(e23,e21) != e23
| op2(e20,e23) = e20 )
& ( op2(e23,e23) = e23
| op2(e23,e22) != e23
| op2(e23,e21) != e23
| op2(e20,e23) = e20 )
& ( op2(e23,e23) != e23
| op2(e23,e22) != e23
| op2(e23,e21) != e23
| op2(e20,e23) = e20 )
& ( op2(e23,e23) = e23
| op2(e22,e23) = e22
| op2(e21,e23) = e21
| op2(e23,e20) != e23 )
& ( op2(e23,e23) != e23
| op2(e22,e23) = e22
| op2(e21,e23) = e21
| op2(e23,e20) != e23 )
& ( op2(e23,e23) = e23
| op2(e23,e22) != e23
| op2(e21,e23) = e21
| op2(e23,e20) != e23 )
& ( op2(e23,e23) != e23
| op2(e23,e22) != e23
| op2(e21,e23) = e21
| op2(e23,e20) != e23 )
& ( op2(e23,e23) = e23
| op2(e22,e23) = e22
| op2(e23,e21) != e23
| op2(e23,e20) != e23 )
& ( op2(e23,e23) != e23
| op2(e22,e23) = e22
| op2(e23,e21) != e23
| op2(e23,e20) != e23 )
& ( op2(e23,e23) = e23
| op2(e23,e22) != e23
| op2(e23,e21) != e23
| op2(e23,e20) != e23 )
& ( op2(e23,e23) != e23
| op2(e23,e22) != e23
| op2(e23,e21) != e23
| op2(e23,e20) != e23 ) ),
inference(distribute,[status(thm)],[15]) ).
cnf(342,plain,
( op2(e20,e23) = e20
| op2(e21,e23) = e21
| op2(e22,e23) = e22
| op2(e23,e23) = e23 ),
inference(split_conjunct,[status(thm)],[326]) ).
cnf(358,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e21
| op2(e22,e22) = e22
| op2(e23,e22) = e23 ),
inference(split_conjunct,[status(thm)],[326]) ).
cnf(370,plain,
( op2(e20,e21) = e20
| op2(e22,e21) = e22
| op2(e23,e21) = e23
| op2(e21,e21) != e21 ),
inference(split_conjunct,[status(thm)],[326]) ).
cnf(374,plain,
( op2(e20,e21) = e20
| op2(e21,e21) = e21
| op2(e22,e21) = e22
| op2(e23,e21) = e23 ),
inference(split_conjunct,[status(thm)],[326]) ).
cnf(380,plain,
( op2(e21,e20) = e21
| op2(e23,e20) = e23
| op2(e20,e20) != e20
| op2(e20,e22) != e20 ),
inference(split_conjunct,[status(thm)],[326]) ).
cnf(382,plain,
( op2(e21,e20) = e21
| op2(e22,e20) = e22
| op2(e23,e20) = e23
| op2(e20,e20) != e20 ),
inference(split_conjunct,[status(thm)],[326]) ).
cnf(388,plain,
( op2(e20,e20) = e20
| op2(e21,e20) = e21
| op2(e23,e20) = e23
| op2(e20,e22) != e20 ),
inference(split_conjunct,[status(thm)],[326]) ).
cnf(390,plain,
( op2(e20,e20) = e20
| op2(e21,e20) = e21
| op2(e22,e20) = e22
| op2(e23,e20) = e23 ),
inference(split_conjunct,[status(thm)],[326]) ).
cnf(391,plain,
e13 = op1(e12,e12),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(392,plain,
e11 = op1(op1(op1(e12,e12),op1(e12,e12)),op1(e12,e12)),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(393,plain,
e10 = op1(op1(e12,e12),op1(e12,e12)),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(394,plain,
e23 = op2(e22,e22),
inference(split_conjunct,[status(thm)],[17]) ).
cnf(395,plain,
e21 = op2(op2(op2(e22,e22),op2(e22,e22)),op2(e22,e22)),
inference(split_conjunct,[status(thm)],[17]) ).
cnf(396,plain,
e20 = op2(op2(e22,e22),op2(e22,e22)),
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(410,negated_conjecture,
( ~ epred2_0
| h2(e10) != e23 ),
inference(split_conjunct,[status(thm)],[398]) ).
fof(481,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 ),
inference(fof_nnf,[status(thm)],[21]) ).
fof(482,plain,
( ( h2(e10) != e22
| h2(e10) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e10) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e10) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e10) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e11) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e11) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e11) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e11) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e12) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e12) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e12) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e12) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e13) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e13) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e13) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e13) != e21
| h2(e10) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e10) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e10) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e10) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e10) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e11) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e11) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e11) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e11) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e12) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e12) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e12) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e12) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e13) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e13) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e13) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e13) != e21
| h2(e11) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e10) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e10) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e10) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e10) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e11) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e11) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e11) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e11) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e12) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e12) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e12) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e12) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e13) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e13) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e13) != e21
| h2(e12) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e10) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e10) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e10) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e10) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e11) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e11) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e11) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e11) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e12) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e12) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e12) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e12) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e10) != e22
| h2(e13) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e11) != e22
| h2(e13) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e12) != e22
| h2(e13) != e21
| h2(e13) != e20
| 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))
| epred2_0 )
& ( h2(e13) != e22
| h2(e13) != e21
| h2(e13) != e20
| 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))
| epred2_0 ) ),
inference(distribute,[status(thm)],[481]) ).
cnf(489,plain,
( epred2_0
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(e13) != e20
| h2(e12) != e21
| h2(e11) != e22 ),
inference(split_conjunct,[status(thm)],[482]) ).
cnf(680,plain,
op1(e13,e13) = e10,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[393,391,theory(equality)]),391,theory(equality)]) ).
cnf(682,plain,
h4(e13) = e20,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[396,394,theory(equality)]),394,theory(equality)]),257,theory(equality)]) ).
cnf(688,plain,
op2(h2(e13),h2(e13)) = h2(e10),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[251,249,theory(equality)]),249,theory(equality)]) ).
cnf(691,plain,
op1(e10,e13) = e11,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[392,391,theory(equality)]),391,theory(equality)]),680,theory(equality)]),391,theory(equality)]) ).
cnf(692,plain,
op2(h1(e13),e20) = h4(e11),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[258,257,theory(equality)]),682,theory(equality)]),257,theory(equality)]),682,theory(equality)]),245,theory(equality)]),257,theory(equality)]),682,theory(equality)]) ).
cnf(719,plain,
e11 != op1(e10,e12),
inference(rw,[status(thm)],[193,691,theory(equality)]) ).
cnf(721,plain,
( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12
| e11 = e12 ),
inference(rw,[status(thm)],[52,691,theory(equality)]) ).
cnf(722,plain,
( op1(e10,e10) = e12
| op1(e10,e11) = e12
| op1(e10,e12) = e12 ),
inference(sr,[status(thm)],[721,139,theory(equality)]) ).
cnf(730,plain,
( op1(e10,e10) = e13
| op1(e10,e11) = e13
| op1(e10,e12) = e13
| e11 = e13 ),
inference(rw,[status(thm)],[50,691,theory(equality)]) ).
cnf(731,plain,
( op1(e10,e10) = e13
| op1(e10,e11) = e13
| op1(e10,e12) = e13 ),
inference(sr,[status(thm)],[730,138,theory(equality)]) ).
cnf(739,plain,
op1(e11,e13) != e11,
inference(rw,[status(thm)],[204,691,theory(equality)]) ).
cnf(782,plain,
e13 != op1(e10,e12),
inference(rw,[status(thm)],[209,391,theory(equality)]) ).
cnf(785,plain,
( op1(e10,e11) = e13
| op1(e10,e10) = e13 ),
inference(sr,[status(thm)],[731,782,theory(equality)]) ).
cnf(792,plain,
e13 != op1(e12,e11),
inference(rw,[status(thm)],[183,391,theory(equality)]) ).
cnf(798,plain,
( op1(e10,e11) = e13
| op1(e11,e11) = e13
| op1(e13,e11) = e13 ),
inference(sr,[status(thm)],[41,792,theory(equality)]) ).
cnf(811,plain,
( op1(e10,e12) = e10
| op1(e11,e12) = e10
| e13 = e10
| op1(e13,e12) = e10 ),
inference(rw,[status(thm)],[39,391,theory(equality)]) ).
cnf(812,plain,
( op1(e10,e12) = e10
| op1(e11,e12) = e10
| op1(e13,e12) = e10 ),
inference(sr,[status(thm)],[811,140,theory(equality)]) ).
cnf(835,plain,
( op1(e10,e12) = e11
| op1(e11,e12) = e11
| e13 = e11
| op1(e13,e12) = e11 ),
inference(rw,[status(thm)],[37,391,theory(equality)]) ).
cnf(836,plain,
( op1(e11,e12) = e11
| e11 = e13
| op1(e13,e12) = e11 ),
inference(sr,[status(thm)],[835,719,theory(equality)]) ).
cnf(837,plain,
( op1(e11,e12) = e11
| op1(e13,e12) = e11 ),
inference(sr,[status(thm)],[836,138,theory(equality)]) ).
cnf(845,plain,
( op1(e10,e12) = e12
| op1(e11,e12) = e12
| e13 = e12
| op1(e13,e12) = e12 ),
inference(rw,[status(thm)],[35,391,theory(equality)]) ).
cnf(846,plain,
( op1(e10,e12) = e12
| op1(e11,e12) = e12
| op1(e13,e12) = e12 ),
inference(sr,[status(thm)],[845,137,theory(equality)]) ).
cnf(886,plain,
( e11 = e10
| op1(e11,e13) = e11
| op1(e12,e13) = e12
| op1(e13,e13) = e13 ),
inference(rw,[status(thm)],[277,691,theory(equality)]) ).
cnf(887,plain,
( e11 = e10
| op1(e11,e13) = e11
| op1(e12,e13) = e12
| e10 = e13 ),
inference(rw,[status(thm)],[886,680,theory(equality)]) ).
cnf(888,plain,
( op1(e11,e13) = e11
| op1(e12,e13) = e12
| e10 = e13 ),
inference(sr,[status(thm)],[887,142,theory(equality)]) ).
cnf(889,plain,
( op1(e12,e13) = e12
| e10 = e13 ),
inference(sr,[status(thm)],[888,739,theory(equality)]) ).
cnf(890,plain,
op1(e12,e13) = e12,
inference(sr,[status(thm)],[889,140,theory(equality)]) ).
cnf(892,plain,
op1(e12,e11) != e12,
inference(rw,[status(thm)],[182,890,theory(equality)]) ).
cnf(893,plain,
op1(e12,e10) != e12,
inference(rw,[status(thm)],[184,890,theory(equality)]) ).
cnf(908,plain,
e10 != op1(e13,e12),
inference(rw,[status(thm)],[175,680,theory(equality)]) ).
cnf(909,plain,
( op1(e11,e12) = e10
| op1(e10,e12) = e10 ),
inference(sr,[status(thm)],[812,908,theory(equality)]) ).
cnf(912,plain,
( e11 = e13
| op1(e11,e13) = e13
| op1(e12,e13) = e13
| op1(e13,e13) = e13 ),
inference(rw,[status(thm)],[25,691,theory(equality)]) ).
cnf(913,plain,
( e11 = e13
| op1(e11,e13) = e13
| e12 = e13
| op1(e13,e13) = e13 ),
inference(rw,[status(thm)],[912,890,theory(equality)]) ).
cnf(914,plain,
( e11 = e13
| op1(e11,e13) = e13
| e12 = e13
| e10 = e13 ),
inference(rw,[status(thm)],[913,680,theory(equality)]) ).
cnf(915,plain,
( op1(e11,e13) = e13
| e12 = e13
| e10 = e13 ),
inference(sr,[status(thm)],[914,138,theory(equality)]) ).
cnf(916,plain,
( op1(e11,e13) = e13
| e10 = e13 ),
inference(sr,[status(thm)],[915,137,theory(equality)]) ).
cnf(917,plain,
op1(e11,e13) = e13,
inference(sr,[status(thm)],[916,140,theory(equality)]) ).
cnf(920,plain,
op1(e11,e11) != e13,
inference(rw,[status(thm)],[188,917,theory(equality)]) ).
cnf(942,plain,
e20 != op2(e23,e20),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[92,257,theory(equality)]),682,theory(equality)]) ).
cnf(944,plain,
e20 != op2(e23,e22),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[89,257,theory(equality)]),682,theory(equality)]) ).
cnf(1005,plain,
( op1(e12,e10) = e10
| op1(e12,e11) = e10
| e13 = e10
| op1(e12,e13) = e10 ),
inference(rw,[status(thm)],[40,391,theory(equality)]) ).
cnf(1006,plain,
( op1(e12,e10) = e10
| op1(e12,e11) = e10
| e13 = e10
| e12 = e10 ),
inference(rw,[status(thm)],[1005,890,theory(equality)]) ).
cnf(1007,plain,
( op1(e12,e10) = e10
| op1(e12,e11) = e10
| e12 = e10 ),
inference(sr,[status(thm)],[1006,140,theory(equality)]) ).
cnf(1008,plain,
( op1(e12,e10) = e10
| op1(e12,e11) = e10 ),
inference(sr,[status(thm)],[1007,141,theory(equality)]) ).
cnf(1020,plain,
( op1(e12,e10) = e11
| op1(e12,e11) = e11
| e13 = e11
| op1(e12,e13) = e11 ),
inference(rw,[status(thm)],[38,391,theory(equality)]) ).
cnf(1021,plain,
( op1(e12,e10) = e11
| op1(e12,e11) = e11
| e13 = e11
| e12 = e11 ),
inference(rw,[status(thm)],[1020,890,theory(equality)]) ).
cnf(1022,plain,
( op1(e12,e10) = e11
| op1(e12,e11) = e11
| e12 = e11 ),
inference(sr,[status(thm)],[1021,138,theory(equality)]) ).
cnf(1023,plain,
( op1(e12,e10) = e11
| op1(e12,e11) = e11 ),
inference(sr,[status(thm)],[1022,139,theory(equality)]) ).
cnf(1031,plain,
( e11 = e10
| op1(e12,e10) = e10
| op1(e12,e10) = e11 ),
inference(spm,[status(thm)],[1008,1023,theory(equality)]) ).
cnf(1034,plain,
( op1(e12,e10) = e10
| op1(e12,e10) = e11 ),
inference(sr,[status(thm)],[1031,142,theory(equality)]) ).
cnf(1037,plain,
op2(e22,e23) != e23,
inference(rw,[status(thm)],[95,394,theory(equality)]) ).
cnf(1057,plain,
op2(e23,e20) != h1(e13),
inference(rw,[status(thm)],[134,245,theory(equality)]) ).
cnf(1079,plain,
( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12
| e10 = e12 ),
inference(rw,[status(thm)],[28,680,theory(equality)]) ).
cnf(1080,plain,
( op1(e13,e10) = e12
| op1(e13,e11) = e12
| op1(e13,e12) = e12 ),
inference(sr,[status(thm)],[1079,141,theory(equality)]) ).
cnf(1088,plain,
op2(e23,e22) != e23,
inference(rw,[status(thm)],[119,394,theory(equality)]) ).
cnf(1111,plain,
e23 != op2(e20,e22),
inference(rw,[status(thm)],[123,394,theory(equality)]) ).
cnf(1127,plain,
op2(e20,e23) = e21,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[395,394,theory(equality)]),394,theory(equality)]),257,theory(equality)]),682,theory(equality)]),394,theory(equality)]) ).
cnf(1129,plain,
op2(e20,e21) != e21,
inference(rw,[status(thm)],[108,1127,theory(equality)]) ).
cnf(1151,plain,
( op1(e10,e11) = e10
| op1(e12,e11) = e12
| op1(e13,e11) = e13 ),
inference(csr,[status(thm)],[305,309]) ).
cnf(1163,plain,
( op1(e10,e12) = e10
| op1(e11,e12) = e11
| e13 = e12
| op1(e12,e13) != e12 ),
inference(rw,[status(thm)],[292,391,theory(equality)]) ).
cnf(1164,plain,
( op1(e10,e12) = e10
| op1(e11,e12) = e11
| e13 = e12
| $false ),
inference(rw,[status(thm)],[1163,890,theory(equality)]) ).
cnf(1165,plain,
( op1(e10,e12) = e10
| op1(e11,e12) = e11
| e13 = e12 ),
inference(cn,[status(thm)],[1164,theory(equality)]) ).
cnf(1166,plain,
( op1(e10,e12) = e10
| op1(e11,e12) = e11 ),
inference(sr,[status(thm)],[1165,137,theory(equality)]) ).
cnf(1213,plain,
( op1(e11,e10) = e11
| op1(e12,e10) = e12
| op1(e13,e10) = e13 ),
inference(csr,[status(thm)],[317,325]) ).
cnf(1242,plain,
op2(h2(e10),h2(e13)) = h2(e11),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[250,249,theory(equality)]),249,theory(equality)]),688,theory(equality)]),249,theory(equality)]) ).
cnf(1276,plain,
( h1(e13) = e20
| op2(e21,e20) = e21
| op2(e22,e20) = e22
| op2(e23,e20) = e23 ),
inference(rw,[status(thm)],[390,245,theory(equality)]) ).
cnf(1363,plain,
( h1(e13) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| op2(e20,e23) = e22 ),
inference(rw,[status(thm)],[170,245,theory(equality)]) ).
cnf(1364,plain,
( h1(e13) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22
| e21 = e22 ),
inference(rw,[status(thm)],[1363,1127,theory(equality)]) ).
cnf(1365,plain,
( h1(e13) = e22
| op2(e20,e21) = e22
| op2(e20,e22) = e22 ),
inference(sr,[status(thm)],[1364,225,theory(equality)]) ).
cnf(1395,plain,
( h1(e13) = e23
| op2(e20,e21) = e23
| op2(e20,e22) = e23
| op2(e20,e23) = e23 ),
inference(rw,[status(thm)],[168,245,theory(equality)]) ).
cnf(1396,plain,
( h1(e13) = e23
| op2(e20,e21) = e23
| op2(e20,e22) = e23
| e21 = e23 ),
inference(rw,[status(thm)],[1395,1127,theory(equality)]) ).
cnf(1397,plain,
( h1(e13) = e23
| op2(e20,e21) = e23
| e21 = e23 ),
inference(sr,[status(thm)],[1396,1111,theory(equality)]) ).
cnf(1398,plain,
( h1(e13) = e23
| op2(e20,e21) = e23 ),
inference(sr,[status(thm)],[1397,224,theory(equality)]) ).
cnf(1401,plain,
( h1(e13) = e23
| e23 != op2(e23,e21) ),
inference(spm,[status(thm)],[128,1398,theory(equality)]) ).
cnf(1457,plain,
( e21 = e23
| op2(e21,e23) = e23
| op2(e22,e23) = e23
| op2(e23,e23) = e23 ),
inference(rw,[status(thm)],[143,1127,theory(equality)]) ).
cnf(1458,plain,
( e21 = e23
| op2(e21,e23) = e23
| op2(e22,e23) = e23
| e20 = e23 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[1457,257,theory(equality)]),682,theory(equality)]) ).
cnf(1459,plain,
( op2(e21,e23) = e23
| op2(e22,e23) = e23
| e20 = e23 ),
inference(sr,[status(thm)],[1458,224,theory(equality)]) ).
cnf(1460,plain,
( op2(e21,e23) = e23
| e20 = e23 ),
inference(sr,[status(thm)],[1459,1037,theory(equality)]) ).
cnf(1461,plain,
op2(e21,e23) = e23,
inference(sr,[status(thm)],[1460,226,theory(equality)]) ).
cnf(1477,plain,
( op2(e20,e21) = e20
| h2(e13) = e21
| op2(e22,e21) = e22
| op2(e23,e21) = e23 ),
inference(rw,[status(thm)],[374,249,theory(equality)]) ).
cnf(1486,plain,
( op2(e20,e21) = e21
| h2(e13) = e21
| op2(e22,e21) = e21
| op2(e23,e21) = e21 ),
inference(rw,[status(thm)],[163,249,theory(equality)]) ).
cnf(1569,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e20
| e23 = e20
| op2(e23,e22) = e20 ),
inference(rw,[status(thm)],[157,394,theory(equality)]) ).
cnf(1570,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e20
| op2(e23,e22) = e20 ),
inference(sr,[status(thm)],[1569,226,theory(equality)]) ).
cnf(1571,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e20 ),
inference(sr,[status(thm)],[1570,944,theory(equality)]) ).
cnf(1590,plain,
( e21 = e20
| op2(e21,e23) = e21
| op2(e22,e23) = e22
| op2(e23,e23) = e23 ),
inference(rw,[status(thm)],[342,1127,theory(equality)]) ).
cnf(1591,plain,
( e21 = e20
| e23 = e21
| op2(e22,e23) = e22
| op2(e23,e23) = e23 ),
inference(rw,[status(thm)],[1590,1461,theory(equality)]) ).
cnf(1592,plain,
( e21 = e20
| e23 = e21
| op2(e22,e23) = e22
| e20 = e23 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[1591,257,theory(equality)]),682,theory(equality)]) ).
cnf(1593,plain,
( e21 = e23
| op2(e22,e23) = e22
| e20 = e23 ),
inference(sr,[status(thm)],[1592,228,theory(equality)]) ).
cnf(1594,plain,
( op2(e22,e23) = e22
| e20 = e23 ),
inference(sr,[status(thm)],[1593,224,theory(equality)]) ).
cnf(1595,plain,
op2(e22,e23) = e22,
inference(sr,[status(thm)],[1594,226,theory(equality)]) ).
cnf(1597,plain,
op2(e22,e21) != e22,
inference(rw,[status(thm)],[96,1595,theory(equality)]) ).
cnf(1598,plain,
op2(e22,e20) != e22,
inference(rw,[status(thm)],[98,1595,theory(equality)]) ).
cnf(1611,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e21
| e23 = e22
| op2(e23,e22) = e23 ),
inference(rw,[status(thm)],[358,394,theory(equality)]) ).
cnf(1612,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e21
| op2(e23,e22) = e23 ),
inference(sr,[status(thm)],[1611,223,theory(equality)]) ).
cnf(1613,plain,
( op2(e20,e22) = e20
| op2(e21,e22) = e21 ),
inference(sr,[status(thm)],[1612,1088,theory(equality)]) ).
cnf(1619,plain,
( e21 = e20
| op2(e20,e22) = e20 ),
inference(spm,[status(thm)],[1571,1613,theory(equality)]) ).
cnf(1620,plain,
op2(e20,e22) = e20,
inference(sr,[status(thm)],[1619,228,theory(equality)]) ).
cnf(1654,plain,
( op2(e20,e22) = e22
| op2(e21,e22) = e22
| e23 = e22
| op2(e23,e22) = e22 ),
inference(rw,[status(thm)],[153,394,theory(equality)]) ).
cnf(1655,plain,
( op2(e20,e22) = e22
| op2(e21,e22) = e22
| op2(e23,e22) = e22 ),
inference(sr,[status(thm)],[1654,223,theory(equality)]) ).
cnf(1675,plain,
( op2(e23,e20) = e21
| op2(e23,e20) = e22
| op2(e23,e20) = e23 ),
inference(sr,[status(thm)],[60,942,theory(equality)]) ).
cnf(1703,plain,
( op2(e23,e22) = e21
| op2(e23,e22) = e22
| op2(e23,e22) = e23 ),
inference(sr,[status(thm)],[58,944,theory(equality)]) ).
cnf(1704,plain,
( op2(e23,e22) = e21
| op2(e23,e22) = e22 ),
inference(sr,[status(thm)],[1703,1088,theory(equality)]) ).
cnf(1712,plain,
( h1(e13) = e20
| op2(e21,e20) = e21
| op2(e23,e20) = e23
| op2(e20,e22) != e20 ),
inference(rw,[status(thm)],[388,245,theory(equality)]) ).
cnf(1718,plain,
( op2(e21,e20) = e20
| h2(e13) = e20
| op2(e21,e22) = e20
| op2(e21,e23) = e20 ),
inference(rw,[status(thm)],[166,249,theory(equality)]) ).
cnf(1719,plain,
( op2(e21,e20) = e20
| h2(e13) = e20
| op2(e21,e22) = e20
| e23 = e20 ),
inference(rw,[status(thm)],[1718,1461,theory(equality)]) ).
cnf(1720,plain,
( op2(e21,e20) = e20
| h2(e13) = e20
| op2(e21,e22) = e20 ),
inference(sr,[status(thm)],[1719,226,theory(equality)]) ).
cnf(1762,plain,
( op2(e20,e21) = e20
| op2(e22,e21) = e22
| op2(e23,e21) = e23
| h2(e13) != e21 ),
inference(rw,[status(thm)],[370,249,theory(equality)]) ).
cnf(1763,plain,
( op2(e20,e21) = e20
| op2(e22,e21) = e22
| op2(e23,e21) = e23 ),
inference(csr,[status(thm)],[1762,1477]) ).
cnf(1783,plain,
( op2(e21,e20) = e21
| op2(e22,e20) = e22
| op2(e23,e20) = e23
| h1(e13) != e20 ),
inference(rw,[status(thm)],[382,245,theory(equality)]) ).
cnf(1784,plain,
( op2(e21,e20) = e21
| op2(e22,e20) = e22
| op2(e23,e20) = e23 ),
inference(csr,[status(thm)],[1783,1276]) ).
cnf(1858,plain,
( op2(e21,e20) = e21
| op2(e23,e20) = e23
| h1(e13) != e20
| op2(e20,e22) != e20 ),
inference(rw,[status(thm)],[380,245,theory(equality)]) ).
cnf(1859,plain,
( op2(e21,e20) = e21
| op2(e23,e20) = e23
| op2(e20,e22) != e20 ),
inference(csr,[status(thm)],[1858,1712]) ).
cnf(1957,plain,
( op2(e22,e20) = e20
| op2(e22,e21) = e20
| e23 = e20
| op2(e22,e23) = e20 ),
inference(rw,[status(thm)],[158,394,theory(equality)]) ).
cnf(1958,plain,
( op2(e22,e20) = e20
| op2(e22,e21) = e20
| e23 = e20
| e22 = e20 ),
inference(rw,[status(thm)],[1957,1595,theory(equality)]) ).
cnf(1959,plain,
( op2(e22,e20) = e20
| op2(e22,e21) = e20
| e22 = e20 ),
inference(sr,[status(thm)],[1958,226,theory(equality)]) ).
cnf(1960,plain,
( op2(e22,e20) = e20
| op2(e22,e21) = e20 ),
inference(sr,[status(thm)],[1959,227,theory(equality)]) ).
cnf(3954,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e13)) != h2(op1(e12,e13))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[489,252,theory(equality)]) ).
cnf(3955,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e13)) != h2(op1(e12,e13))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[3954,252,theory(equality)]) ).
cnf(3956,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| h2(e11) != h2(op1(e10,e13))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e13)) != h2(op1(e12,e13))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[3955,1242,theory(equality)]) ).
cnf(3957,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| $false
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e13)) != h2(op1(e12,e13))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[3956,691,theory(equality)]) ).
cnf(3958,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| $false
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),e21) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e13)) != h2(op1(e12,e13))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[3957,252,theory(equality)]) ).
cnf(3959,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| $false
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),e21) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e13)) != h2(op1(e12,e13))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[3958,917,theory(equality)]) ).
cnf(3960,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| $false
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),e21) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e10)) != h2(op1(e12,e10))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e13)) != h2(op1(e12,e13))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[3959,252,theory(equality)]) ).
cnf(3961,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| $false
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),e21) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e10)) != h2(op1(e12,e10))
| op2(e21,h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e13)) != h2(op1(e12,e13))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[3960,252,theory(equality)]) ).
cnf(3962,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| $false
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),e21) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e10)) != h2(op1(e12,e10))
| op2(e21,h2(e11)) != h2(op1(e12,e11))
| h2(e13) != h2(op1(e12,e12))
| op2(h2(e12),h2(e13)) != h2(op1(e12,e13))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[3961,252,theory(equality)]),252,theory(equality)]),249,theory(equality)]) ).
cnf(3963,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| $false
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),e21) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e10)) != h2(op1(e12,e10))
| op2(e21,h2(e11)) != h2(op1(e12,e11))
| $false
| op2(h2(e12),h2(e13)) != h2(op1(e12,e13))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[3962,391,theory(equality)]) ).
cnf(3964,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| $false
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),e21) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e10)) != h2(op1(e12,e10))
| op2(e21,h2(e11)) != h2(op1(e12,e11))
| $false
| op2(e21,h2(e13)) != h2(op1(e12,e13))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[3963,252,theory(equality)]) ).
cnf(3965,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| $false
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),e21) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e10)) != h2(op1(e12,e10))
| op2(e21,h2(e11)) != h2(op1(e12,e11))
| $false
| op2(e21,h2(e13)) != e21
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e12)) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[3964,890,theory(equality)]),252,theory(equality)]) ).
cnf(3966,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| $false
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),e21) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e10)) != h2(op1(e12,e10))
| op2(e21,h2(e11)) != h2(op1(e12,e11))
| $false
| op2(e21,h2(e13)) != e21
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),e21) != h2(op1(e13,e12))
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[3965,252,theory(equality)]) ).
cnf(3967,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| $false
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),e21) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e10)) != h2(op1(e12,e10))
| op2(e21,h2(e11)) != h2(op1(e12,e11))
| $false
| op2(e21,h2(e13)) != e21
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),e21) != h2(op1(e13,e12))
| h2(e10) != h2(op1(e13,e13)) ),
inference(rw,[status(thm)],[3966,688,theory(equality)]) ).
cnf(3968,plain,
( epred2_0
| h2(e11) != e22
| $false
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| $false
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),e21) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e10)) != h2(op1(e12,e10))
| op2(e21,h2(e11)) != h2(op1(e12,e11))
| $false
| op2(e21,h2(e13)) != e21
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),e21) != h2(op1(e13,e12))
| $false ),
inference(rw,[status(thm)],[3967,680,theory(equality)]) ).
cnf(3969,plain,
( epred2_0
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),e21) != h2(op1(e10,e12))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),e21) != h2(op1(e11,e12))
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e10)) != h2(op1(e12,e10))
| op2(e21,h2(e11)) != h2(op1(e12,e11))
| op2(e21,h2(e13)) != e21
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),e21) != h2(op1(e13,e12)) ),
inference(cn,[status(thm)],[3968,theory(equality)]) ).
cnf(7272,plain,
op2(e21,e22) != e20,
inference(rw,[status(thm)],[124,1620,theory(equality)]) ).
cnf(7273,plain,
e20 != op2(e20,e21),
inference(rw,[status(thm)],[109,1620,theory(equality)]) ).
cnf(7278,plain,
( op2(e23,e20) = e23
| op2(e21,e20) = e21
| $false ),
inference(rw,[status(thm)],[1859,1620,theory(equality)]) ).
cnf(7279,plain,
( op2(e23,e20) = e23
| op2(e21,e20) = e21 ),
inference(cn,[status(thm)],[7278,theory(equality)]) ).
cnf(7281,plain,
( op2(e23,e22) = e22
| op2(e21,e22) = e22
| e20 = e22 ),
inference(rw,[status(thm)],[1655,1620,theory(equality)]) ).
cnf(7282,plain,
( op2(e23,e22) = e22
| op2(e21,e22) = e22 ),
inference(sr,[status(thm)],[7281,227,theory(equality)]) ).
cnf(7290,plain,
( e20 = e22
| op2(e20,e21) = e22
| h1(e13) = e22 ),
inference(rw,[status(thm)],[1365,1620,theory(equality)]) ).
cnf(7291,plain,
( op2(e20,e21) = e22
| h1(e13) = e22 ),
inference(sr,[status(thm)],[7290,227,theory(equality)]) ).
cnf(7322,plain,
( op1(e13,e11) = e13
| op1(e10,e11) = e10 ),
inference(sr,[status(thm)],[1151,892,theory(equality)]) ).
cnf(7327,plain,
( op1(e13,e10) = e13
| op1(e11,e10) = e11 ),
inference(sr,[status(thm)],[1213,893,theory(equality)]) ).
cnf(7333,plain,
( op1(e13,e11) = e13
| op1(e10,e11) = e13 ),
inference(sr,[status(thm)],[798,920,theory(equality)]) ).
cnf(7334,plain,
( op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e11) = e10 ),
inference(sr,[status(thm)],[83,920,theory(equality)]) ).
cnf(7364,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| h2(e13) = e21 ),
inference(sr,[status(thm)],[1486,1129,theory(equality)]) ).
cnf(7401,plain,
( e13 = e10
| op1(e13,e11) = e13 ),
inference(spm,[status(thm)],[7322,7333,theory(equality)]) ).
cnf(7402,plain,
op1(e13,e11) = e13,
inference(sr,[status(thm)],[7401,140,theory(equality)]) ).
cnf(7405,plain,
e13 != op1(e13,e10),
inference(rw,[status(thm)],[180,7402,theory(equality)]) ).
cnf(7408,plain,
op1(e10,e11) != e13,
inference(rw,[status(thm)],[214,7402,theory(equality)]) ).
cnf(7412,plain,
( epred2_0
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(e13)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[3969,7402,theory(equality)]) ).
cnf(7435,plain,
( op1(e13,e12) = e12
| e13 = e12
| op1(e13,e10) = e12 ),
inference(rw,[status(thm)],[1080,7402,theory(equality)]) ).
cnf(7436,plain,
( op1(e13,e12) = e12
| op1(e13,e10) = e12 ),
inference(sr,[status(thm)],[7435,137,theory(equality)]) ).
cnf(7452,plain,
( e10 = e11
| op1(e10,e12) = e10 ),
inference(spm,[status(thm)],[1166,909,theory(equality)]) ).
cnf(7457,plain,
op1(e10,e12) = e10,
inference(sr,[status(thm)],[7452,142,theory(equality)]) ).
cnf(7469,plain,
( op1(e13,e12) = e12
| op1(e11,e12) = e12
| e10 = e12 ),
inference(rw,[status(thm)],[846,7457,theory(equality)]) ).
cnf(7470,plain,
( op1(e13,e12) = e12
| op1(e11,e12) = e12 ),
inference(sr,[status(thm)],[7469,141,theory(equality)]) ).
cnf(7473,plain,
( e10 = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 ),
inference(rw,[status(thm)],[722,7457,theory(equality)]) ).
cnf(7474,plain,
( op1(e10,e11) = e12
| op1(e10,e10) = e12 ),
inference(sr,[status(thm)],[7473,141,theory(equality)]) ).
cnf(7487,plain,
op1(e11,e10) = e11,
inference(sr,[status(thm)],[7327,7405,theory(equality)]) ).
cnf(7491,plain,
op1(e10,e10) = e13,
inference(sr,[status(thm)],[785,7408,theory(equality)]) ).
cnf(7499,plain,
( e13 = e12
| op1(e10,e11) = e12 ),
inference(rw,[status(thm)],[7474,7491,theory(equality)]) ).
cnf(7500,plain,
op1(e10,e11) = e12,
inference(sr,[status(thm)],[7499,137,theory(equality)]) ).
cnf(7505,plain,
op1(e12,e10) != e11,
inference(rw,[status(thm)],[219,7487,theory(equality)]) ).
cnf(7506,plain,
op1(e11,e12) != e11,
inference(rw,[status(thm)],[191,7487,theory(equality)]) ).
cnf(7507,plain,
op1(e11,e11) != e11,
inference(rw,[status(thm)],[192,7487,theory(equality)]) ).
cnf(7523,plain,
op1(e11,e11) != e12,
inference(rw,[status(thm)],[216,7500,theory(equality)]) ).
cnf(7533,plain,
( op2(e23,e21) = e23
| op2(e20,e21) = e20 ),
inference(sr,[status(thm)],[1763,1597,theory(equality)]) ).
cnf(7552,plain,
( op2(e23,e20) = e23
| op2(e21,e20) = e21 ),
inference(sr,[status(thm)],[1784,1598,theory(equality)]) ).
cnf(7575,plain,
( op2(e21,e20) = e20
| h2(e13) = e20 ),
inference(sr,[status(thm)],[1720,7272,theory(equality)]) ).
cnf(7582,plain,
op1(e12,e11) = e11,
inference(sr,[status(thm)],[1023,7505,theory(equality)]) ).
cnf(7583,plain,
op1(e12,e10) = e10,
inference(sr,[status(thm)],[1034,7505,theory(equality)]) ).
cnf(7607,plain,
op1(e13,e12) = e11,
inference(sr,[status(thm)],[837,7506,theory(equality)]) ).
cnf(7672,plain,
( e21 = e20
| h2(e13) = e20
| op2(e23,e20) = e23 ),
inference(spm,[status(thm)],[7575,7279,theory(equality)]) ).
cnf(7673,plain,
( h2(e13) = e20
| op2(e23,e20) = e23 ),
inference(sr,[status(thm)],[7672,228,theory(equality)]) ).
cnf(7676,plain,
( h2(e13) = e20
| e23 != h1(e13) ),
inference(spm,[status(thm)],[1057,7673,theory(equality)]) ).
cnf(7677,plain,
( op2(e20,e20) = h2(e10)
| h1(e13) != e23 ),
inference(spm,[status(thm)],[688,7676,theory(equality)]) ).
cnf(7683,plain,
( h1(e13) = h2(e10)
| h1(e13) != e23 ),
inference(rw,[status(thm)],[7677,245,theory(equality)]) ).
cnf(7685,negated_conjecture,
( h1(e13) != e23
| ~ epred2_0 ),
inference(spm,[status(thm)],[410,7683,theory(equality)]) ).
cnf(7768,plain,
( e11 = e12
| op1(e13,e10) = e12 ),
inference(rw,[status(thm)],[7436,7607,theory(equality)]) ).
cnf(7769,plain,
op1(e13,e10) = e12,
inference(sr,[status(thm)],[7768,139,theory(equality)]) ).
cnf(7791,plain,
( e11 = e12
| op1(e11,e12) = e12 ),
inference(rw,[status(thm)],[7470,7607,theory(equality)]) ).
cnf(7792,plain,
op1(e11,e12) = e12,
inference(sr,[status(thm)],[7791,139,theory(equality)]) ).
cnf(7802,plain,
( op1(e11,e11) = e10
| op1(e11,e11) = e12 ),
inference(sr,[status(thm)],[7334,7507,theory(equality)]) ).
cnf(7803,plain,
op1(e11,e11) = e10,
inference(sr,[status(thm)],[7802,7523,theory(equality)]) ).
cnf(7845,plain,
op2(e23,e21) = e23,
inference(sr,[status(thm)],[7533,7273,theory(equality)]) ).
cnf(7850,plain,
e23 != op2(e23,e20),
inference(rw,[status(thm)],[94,7845,theory(equality)]) ).
cnf(7855,plain,
( h1(e13) = e23
| $false ),
inference(rw,[status(thm)],[1401,7845,theory(equality)]) ).
cnf(7856,plain,
h1(e13) = e23,
inference(cn,[status(thm)],[7855,theory(equality)]) ).
cnf(7868,plain,
( e23 = e21
| op2(e22,e21) = e21
| h2(e13) = e21 ),
inference(rw,[status(thm)],[7364,7845,theory(equality)]) ).
cnf(7869,plain,
( op2(e22,e21) = e21
| h2(e13) = e21 ),
inference(sr,[status(thm)],[7868,224,theory(equality)]) ).
cnf(7883,plain,
op2(e23,e20) = h4(e11),
inference(rw,[status(thm)],[692,7856,theory(equality)]) ).
cnf(7898,negated_conjecture,
( $false
| ~ epred2_0 ),
inference(rw,[status(thm)],[7685,7856,theory(equality)]) ).
cnf(7899,negated_conjecture,
~ epred2_0,
inference(cn,[status(thm)],[7898,theory(equality)]) ).
cnf(7900,plain,
( h2(e10) = e23
| h1(e13) != e23 ),
inference(rw,[status(thm)],[7683,7856,theory(equality)]) ).
cnf(7901,plain,
( h2(e10) = e23
| $false ),
inference(rw,[status(thm)],[7900,7856,theory(equality)]) ).
cnf(7902,plain,
h2(e10) = e23,
inference(cn,[status(thm)],[7901,theory(equality)]) ).
cnf(7903,plain,
( h2(e13) = e20
| $false ),
inference(rw,[status(thm)],[7676,7856,theory(equality)]) ).
cnf(7904,plain,
h2(e13) = e20,
inference(cn,[status(thm)],[7903,theory(equality)]) ).
cnf(7912,plain,
( op2(e20,e21) = e22
| e23 = e22 ),
inference(rw,[status(thm)],[7291,7856,theory(equality)]) ).
cnf(7913,plain,
op2(e20,e21) = e22,
inference(sr,[status(thm)],[7912,223,theory(equality)]) ).
cnf(7919,plain,
op2(e23,h2(e13)) = h2(e11),
inference(rw,[status(thm)],[1242,7902,theory(equality)]) ).
cnf(7936,plain,
( op2(e22,e21) = e21
| e20 = e21 ),
inference(rw,[status(thm)],[7869,7904,theory(equality)]) ).
cnf(7937,plain,
op2(e22,e21) = e21,
inference(sr,[status(thm)],[7936,228,theory(equality)]) ).
cnf(7983,plain,
( epred2_0
| e20 != h2(op1(e10,e10))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(e13)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[7412,7902,theory(equality)]),7902,theory(equality)]),257,theory(equality)]),682,theory(equality)]) ).
cnf(7984,plain,
( epred2_0
| $false
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(e13)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[7983,7491,theory(equality)]),7904,theory(equality)]) ).
cnf(7985,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != h2(op1(e10,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(e13)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[7984,7902,theory(equality)]) ).
cnf(7986,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(e13)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[7985,7500,theory(equality)]),252,theory(equality)]) ).
cnf(7987,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(op1(e11,e10))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(e13)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[7986,7902,theory(equality)]) ).
cnf(7988,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(e13)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[7987,7487,theory(equality)]) ).
cnf(7989,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(e13)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[7988,7803,theory(equality)]),7902,theory(equality)]) ).
cnf(7990,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| e21 != h2(op1(e13,e10))
| op2(h2(e13),h2(e11)) != h2(e13)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[7989,7904,theory(equality)]),7902,theory(equality)]),1127,theory(equality)]) ).
cnf(7991,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(h2(e13),h2(e11)) != h2(e13)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[7990,7769,theory(equality)]),252,theory(equality)]) ).
cnf(7992,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != h2(e13)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[7991,7904,theory(equality)]) ).
cnf(7993,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != e20
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[7992,7904,theory(equality)]) ).
cnf(7994,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != e20
| e23 != op2(h2(e10),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[7993,7457,theory(equality)]),7902,theory(equality)]) ).
cnf(7995,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != e20
| $false
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[7994,7902,theory(equality)]),7845,theory(equality)]) ).
cnf(7996,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != e20
| $false
| e21 != op2(h2(e11),e21)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[7995,7792,theory(equality)]),252,theory(equality)]) ).
cnf(7997,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != e20
| $false
| e21 != op2(h2(e11),e21)
| e23 != op2(e21,h2(e10))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[7996,7583,theory(equality)]),7902,theory(equality)]) ).
cnf(7998,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != e20
| $false
| e21 != op2(h2(e11),e21)
| $false
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[7997,7902,theory(equality)]),1461,theory(equality)]) ).
cnf(7999,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != e20
| $false
| e21 != op2(h2(e11),e21)
| $false
| h2(e11) != op2(e21,h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[7998,7582,theory(equality)]) ).
cnf(8000,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != e20
| $false
| e21 != op2(h2(e11),e21)
| $false
| h2(e11) != op2(e21,h2(e11))
| h2(e11) != op2(h2(e13),e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[7999,7607,theory(equality)]) ).
cnf(8001,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != e20
| $false
| e21 != op2(h2(e11),e21)
| $false
| h2(e11) != op2(e21,h2(e11))
| h2(e11) != op2(e20,e21)
| op2(h2(e11),h2(e13)) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[8000,7904,theory(equality)]) ).
cnf(8002,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != e20
| $false
| e21 != op2(h2(e11),e21)
| $false
| h2(e11) != op2(e21,h2(e11))
| h2(e11) != op2(e20,e21)
| op2(h2(e11),e20) != h2(e13)
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[8001,7904,theory(equality)]) ).
cnf(8003,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != e20
| $false
| e21 != op2(h2(e11),e21)
| $false
| h2(e11) != op2(e21,h2(e11))
| h2(e11) != op2(e20,e21)
| op2(h2(e11),e20) != e20
| op2(e21,h2(e13)) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[8002,7904,theory(equality)]) ).
cnf(8004,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != e20
| $false
| e21 != op2(h2(e11),e21)
| $false
| h2(e11) != op2(e21,h2(e11))
| h2(e11) != op2(e20,e21)
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21
| h2(e11) != e22
| h2(e13) != e20 ),
inference(rw,[status(thm)],[8003,7904,theory(equality)]) ).
cnf(8005,plain,
( epred2_0
| $false
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| $false
| op2(e20,h2(e11)) != e20
| $false
| e21 != op2(h2(e11),e21)
| $false
| h2(e11) != op2(e21,h2(e11))
| h2(e11) != op2(e20,e21)
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21
| h2(e11) != e22
| $false ),
inference(rw,[status(thm)],[8004,7904,theory(equality)]) ).
cnf(8006,plain,
( epred2_0
| op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| op2(e20,h2(e11)) != e20
| e21 != op2(h2(e11),e21)
| h2(e11) != op2(e21,h2(e11))
| h2(e11) != op2(e20,e21)
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21
| h2(e11) != e22 ),
inference(cn,[status(thm)],[8005,theory(equality)]) ).
cnf(8007,plain,
( op2(e23,h2(e11)) != e21
| op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| op2(e20,h2(e11)) != e20
| op2(h2(e11),e21) != e21
| op2(e21,h2(e11)) != h2(e11)
| op2(e20,e21) != h2(e11)
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21
| h2(e11) != e22 ),
inference(sr,[status(thm)],[8006,7899,theory(equality)]) ).
cnf(8014,plain,
op2(e21,e20) != h4(e11),
inference(rw,[status(thm)],[132,7883,theory(equality)]) ).
cnf(8015,plain,
op2(e23,e22) != h4(e11),
inference(rw,[status(thm)],[93,7883,theory(equality)]) ).
cnf(8021,plain,
( h4(e11) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21 ),
inference(rw,[status(thm)],[1675,7883,theory(equality)]) ).
cnf(8022,plain,
( h4(e11) = e23
| op2(e23,e20) = e22
| h4(e11) = e21 ),
inference(rw,[status(thm)],[8021,7883,theory(equality)]) ).
cnf(8023,plain,
( h4(e11) = e23
| h4(e11) = e22
| h4(e11) = e21 ),
inference(rw,[status(thm)],[8022,7883,theory(equality)]) ).
cnf(8024,plain,
h4(e11) = h2(e11),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[7919,7904,theory(equality)]),7883,theory(equality)]) ).
cnf(8054,plain,
h2(e11) != e23,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[7850,7883,theory(equality)]),8024,theory(equality)]) ).
cnf(8059,plain,
( op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| op2(e21,h2(e11)) != h2(e11)
| op2(e23,h2(e11)) != e21
| op2(e20,h2(e11)) != e20
| op2(h2(e11),e21) != e21
| e22 != h2(e11)
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21
| h2(e11) != e22 ),
inference(rw,[status(thm)],[8007,7913,theory(equality)]) ).
cnf(8060,plain,
( op2(h2(e11),e23) != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| op2(e21,h2(e11)) != h2(e11)
| op2(e23,h2(e11)) != e21
| op2(e20,h2(e11)) != e20
| op2(h2(e11),e21) != e21
| h2(e11) != e22
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21 ),
inference(cn,[status(thm)],[8059,theory(equality)]) ).
cnf(8068,plain,
( e21 = e20
| op2(e22,e20) = e20 ),
inference(rw,[status(thm)],[1960,7937,theory(equality)]) ).
cnf(8069,plain,
op2(e22,e20) = e20,
inference(sr,[status(thm)],[8068,228,theory(equality)]) ).
cnf(8100,plain,
( h2(e11) = e23
| h4(e11) = e22
| h4(e11) = e21 ),
inference(rw,[status(thm)],[8023,8024,theory(equality)]) ).
cnf(8101,plain,
( h2(e11) = e23
| h2(e11) = e22
| h4(e11) = e21 ),
inference(rw,[status(thm)],[8100,8024,theory(equality)]) ).
cnf(8102,plain,
( h2(e11) = e23
| h2(e11) = e22
| h2(e11) = e21 ),
inference(rw,[status(thm)],[8101,8024,theory(equality)]) ).
cnf(8103,plain,
( h2(e11) = e22
| h2(e11) = e21 ),
inference(sr,[status(thm)],[8102,8054,theory(equality)]) ).
cnf(8135,plain,
op2(e23,e22) != h2(e11),
inference(rw,[status(thm)],[8015,8024,theory(equality)]) ).
cnf(8136,plain,
( op2(e23,e22) = e21
| e22 != h2(e11) ),
inference(spm,[status(thm)],[8135,1704,theory(equality)]) ).
cnf(8226,plain,
( h2(e11) = e23
| op2(e21,e20) = e21 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[7552,7883,theory(equality)]),8024,theory(equality)]) ).
cnf(8227,plain,
op2(e21,e20) = e21,
inference(sr,[status(thm)],[8226,8054,theory(equality)]) ).
cnf(8261,plain,
e21 != h4(e11),
inference(rw,[status(thm)],[8014,8227,theory(equality)]) ).
cnf(8262,plain,
e21 != h2(e11),
inference(rw,[status(thm)],[8261,8024,theory(equality)]) ).
cnf(8263,plain,
h2(e11) = e22,
inference(sr,[status(thm)],[8103,8262,theory(equality)]) ).
cnf(8273,plain,
( op2(e23,e22) = e21
| $false ),
inference(rw,[status(thm)],[8136,8263,theory(equality)]) ).
cnf(8274,plain,
op2(e23,e22) = e21,
inference(cn,[status(thm)],[8273,theory(equality)]) ).
cnf(8280,plain,
( op2(e21,e22) = e22
| e21 = e22 ),
inference(rw,[status(thm)],[7282,8274,theory(equality)]) ).
cnf(8281,plain,
op2(e21,e22) = e22,
inference(sr,[status(thm)],[8280,225,theory(equality)]) ).
cnf(8439,plain,
( e22 != h2(e11)
| op2(h2(e11),h2(e11)) != e23
| op2(e21,h2(e11)) != h2(e11)
| op2(e23,h2(e11)) != e21
| op2(e20,h2(e11)) != e20
| op2(h2(e11),e21) != e21
| h2(e11) != e22
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[8060,8263,theory(equality)]),1595,theory(equality)]) ).
cnf(8440,plain,
( $false
| op2(h2(e11),h2(e11)) != e23
| op2(e21,h2(e11)) != h2(e11)
| op2(e23,h2(e11)) != e21
| op2(e20,h2(e11)) != e20
| op2(h2(e11),e21) != e21
| h2(e11) != e22
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21 ),
inference(rw,[status(thm)],[8439,8263,theory(equality)]) ).
cnf(8441,plain,
( $false
| $false
| op2(e21,h2(e11)) != h2(e11)
| op2(e23,h2(e11)) != e21
| op2(e20,h2(e11)) != e20
| op2(h2(e11),e21) != e21
| h2(e11) != e22
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[8440,8263,theory(equality)]),8263,theory(equality)]),394,theory(equality)]) ).
cnf(8442,plain,
( $false
| $false
| e22 != h2(e11)
| op2(e23,h2(e11)) != e21
| op2(e20,h2(e11)) != e20
| op2(h2(e11),e21) != e21
| h2(e11) != e22
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[8441,8263,theory(equality)]),8281,theory(equality)]) ).
cnf(8443,plain,
( $false
| $false
| $false
| op2(e23,h2(e11)) != e21
| op2(e20,h2(e11)) != e20
| op2(h2(e11),e21) != e21
| h2(e11) != e22
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21 ),
inference(rw,[status(thm)],[8442,8263,theory(equality)]) ).
cnf(8444,plain,
( $false
| $false
| $false
| $false
| op2(e20,h2(e11)) != e20
| op2(h2(e11),e21) != e21
| h2(e11) != e22
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[8443,8263,theory(equality)]),8274,theory(equality)]) ).
cnf(8445,plain,
( $false
| $false
| $false
| $false
| $false
| op2(h2(e11),e21) != e21
| h2(e11) != e22
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[8444,8263,theory(equality)]),1620,theory(equality)]) ).
cnf(8446,plain,
( $false
| $false
| $false
| $false
| $false
| $false
| h2(e11) != e22
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[8445,8263,theory(equality)]),7937,theory(equality)]) ).
cnf(8447,plain,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| op2(h2(e11),e20) != e20
| op2(e21,e20) != e21 ),
inference(rw,[status(thm)],[8446,8263,theory(equality)]) ).
cnf(8448,plain,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| op2(e21,e20) != e21 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[8447,8263,theory(equality)]),8069,theory(equality)]) ).
cnf(8449,plain,
( $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[8448,8227,theory(equality)]) ).
cnf(8450,plain,
$false,
inference(cn,[status(thm)],[8449,theory(equality)]) ).
cnf(8451,plain,
$false,
8450,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/ALG/ALG110+1.p
% --creating new selector for []
% -running prover on /tmp/tmpJUyMAT/sel_ALG110+1.p_1 with time limit 29
% -prover status Theorem
% Problem ALG110+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/ALG/ALG110+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/ALG/ALG110+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above