%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG117+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:49:33 AM UTC 2026
% Result : Theorem 15.81s 12.09s
% Output : CNFRefutation 15.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 129
% Number of leaves : 17
% Syntax : Number of formulae : 486 ( 181 unt; 0 def)
% Number of atoms : 3352 (3351 equ)
% Maximal formula atoms : 128 ( 6 avg)
% Number of connectives : 4958 (2092 ~;2464 |; 402 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 6 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 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(ax1,axiom,
( ( op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e13,e13) = e10 )
& ( op1(e13,e12) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11
| op1(e13,e12) = e10 )
& ( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e13,e11) = e10 )
& ( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 )
& ( op1(e12,e13) = e13
| op1(e12,e13) = e12
| op1(e12,e13) = e11
| op1(e12,e13) = e10 )
& ( op1(e12,e12) = e13
| op1(e12,e12) = e12
| op1(e12,e12) = e11
| op1(e12,e12) = e10 )
& ( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 )
& ( op1(e12,e10) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 )
& ( op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11
| op1(e11,e13) = e10 )
& ( op1(e11,e12) = e13
| op1(e11,e12) = e12
| op1(e11,e12) = e11
| op1(e11,e12) = e10 )
& ( op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e11) = e10 )
& ( op1(e11,e10) = e13
| op1(e11,e10) = e12
| op1(e11,e10) = e11
| op1(e11,e10) = e10 )
& ( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 )
& ( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 )
& ( op1(e10,e11) = e13
| op1(e10,e11) = e12
| op1(e10,e11) = e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e11
| op1(e10,e10) = e10 ) ),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
( ( op1(e13,e13) = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| op1(e10,e13) = e13 )
& ( op1(e13,e13) = e13
| op1(e13,e12) = e13
| op1(e13,e11) = e13
| op1(e13,e10) = e13 )
& ( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 )
& ( op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 )
& ( op1(e13,e13) = e11
| op1(e12,e13) = e11
| op1(e11,e13) = e11
| op1(e10,e13) = e11 )
& ( op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 )
& ( op1(e13,e13) = e10
| op1(e12,e13) = e10
| op1(e11,e13) = e10
| op1(e10,e13) = e10 )
& ( op1(e13,e13) = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 )
& ( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| op1(e10,e12) = e13 )
& ( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 )
& ( op1(e13,e12) = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 )
& ( op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 )
& ( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 )
& ( op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 )
& ( op1(e13,e12) = e10
| op1(e12,e12) = e10
| op1(e11,e12) = e10
| op1(e10,e12) = e10 )
& ( op1(e12,e13) = e10
| op1(e12,e12) = e10
| op1(e12,e11) = e10
| op1(e12,e10) = e10 )
& ( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| op1(e10,e11) = e13 )
& ( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e11) = e13
| op1(e11,e10) = e13 )
& ( op1(e13,e11) = e12
| op1(e12,e11) = e12
| op1(e11,e11) = e12
| op1(e10,e11) = e12 )
& ( op1(e11,e13) = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 )
& ( op1(e13,e11) = e11
| op1(e12,e11) = e11
| op1(e11,e11) = e11
| op1(e10,e11) = e11 )
& ( op1(e11,e13) = e11
| op1(e11,e12) = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 )
& ( op1(e13,e11) = e10
| op1(e12,e11) = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 )
& ( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 )
& ( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| op1(e10,e10) = e13 )
& ( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 )
& ( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| op1(e10,e10) = e12 )
& ( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 )
& ( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11
| op1(e10,e10) = e11 )
& ( op1(e10,e13) = e11
| op1(e10,e12) = e11
| op1(e10,e11) = e11
| op1(e10,e10) = e11 )
& ( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 )
& ( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ) ),
file('theBenchmark.p',ax2) ).
fof(ax3,axiom,
( ( op2(e23,e23) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e23,e23) = e20 )
& ( op2(e23,e22) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21
| op2(e23,e22) = e20 )
& ( op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e23,e21) = e21
| op2(e23,e21) = e20 )
& ( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 )
& ( op2(e22,e23) = e23
| op2(e22,e23) = e22
| op2(e22,e23) = e21
| op2(e22,e23) = e20 )
& ( op2(e22,e22) = e23
| op2(e22,e22) = e22
| op2(e22,e22) = e21
| op2(e22,e22) = e20 )
& ( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 )
& ( op2(e22,e20) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 )
& ( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| op2(e21,e23) = e20 )
& ( op2(e21,e22) = e23
| op2(e21,e22) = e22
| op2(e21,e22) = e21
| op2(e21,e22) = e20 )
& ( op2(e21,e21) = e23
| op2(e21,e21) = e22
| op2(e21,e21) = e21
| op2(e21,e21) = e20 )
& ( op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e21
| op2(e21,e20) = e20 )
& ( op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 )
& ( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| op2(e20,e22) = e20 )
& ( op2(e20,e21) = e23
| op2(e20,e21) = e22
| op2(e20,e21) = e21
| op2(e20,e21) = e20 )
& ( op2(e20,e20) = e23
| op2(e20,e20) = e22
| op2(e20,e20) = e21
| op2(e20,e20) = e20 ) ),
file('theBenchmark.p',ax3) ).
fof(ax4,axiom,
( ( op2(e23,e23) = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| op2(e20,e23) = e23 )
& ( op2(e23,e23) = e23
| op2(e23,e22) = e23
| op2(e23,e21) = e23
| op2(e23,e20) = e23 )
& ( op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 )
& ( op2(e23,e23) = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 )
& ( op2(e23,e23) = e21
| op2(e22,e23) = e21
| op2(e21,e23) = e21
| op2(e20,e23) = e21 )
& ( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 )
& ( op2(e23,e23) = e20
| op2(e22,e23) = e20
| op2(e21,e23) = e20
| op2(e20,e23) = e20 )
& ( op2(e23,e23) = e20
| op2(e23,e22) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 )
& ( op2(e23,e22) = e23
| op2(e22,e22) = e23
| op2(e21,e22) = e23
| op2(e20,e22) = e23 )
& ( op2(e22,e23) = e23
| op2(e22,e22) = e23
| op2(e22,e21) = e23
| op2(e22,e20) = e23 )
& ( op2(e23,e22) = e22
| op2(e22,e22) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 )
& ( op2(e22,e23) = e22
| op2(e22,e22) = e22
| op2(e22,e21) = e22
| op2(e22,e20) = e22 )
& ( op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 )
& ( op2(e22,e23) = e21
| op2(e22,e22) = e21
| op2(e22,e21) = e21
| op2(e22,e20) = e21 )
& ( op2(e23,e22) = e20
| op2(e22,e22) = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 )
& ( op2(e22,e23) = e20
| op2(e22,e22) = e20
| op2(e22,e21) = e20
| op2(e22,e20) = e20 )
& ( op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e21,e21) = e23
| op2(e20,e21) = e23 )
& ( op2(e21,e23) = e23
| op2(e21,e22) = e23
| op2(e21,e21) = e23
| op2(e21,e20) = e23 )
& ( op2(e23,e21) = e22
| op2(e22,e21) = e22
| op2(e21,e21) = e22
| op2(e20,e21) = e22 )
& ( op2(e21,e23) = e22
| op2(e21,e22) = e22
| op2(e21,e21) = e22
| op2(e21,e20) = e22 )
& ( op2(e23,e21) = e21
| op2(e22,e21) = e21
| op2(e21,e21) = e21
| op2(e20,e21) = e21 )
& ( op2(e21,e23) = e21
| op2(e21,e22) = e21
| op2(e21,e21) = e21
| op2(e21,e20) = e21 )
& ( op2(e23,e21) = e20
| op2(e22,e21) = e20
| op2(e21,e21) = e20
| op2(e20,e21) = e20 )
& ( op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20
| op2(e21,e20) = e20 )
& ( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| op2(e20,e20) = e23 )
& ( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 )
& ( op2(e23,e20) = e22
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| op2(e20,e20) = e22 )
& ( op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| op2(e20,e20) = e22 )
& ( op2(e23,e20) = e21
| op2(e22,e20) = e21
| op2(e21,e20) = e21
| op2(e20,e20) = e21 )
& ( op2(e20,e23) = e21
| op2(e20,e22) = e21
| op2(e20,e21) = e21
| op2(e20,e20) = e21 )
& ( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| op2(e20,e20) = e20 )
& ( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ) ),
file('theBenchmark.p',ax4) ).
fof(ax5,axiom,
( op1(e13,e12) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e11)
& op1(e12,e12) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e11)
& op1(e11,e12) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e11)
& op1(e10,e12) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e11)
& op1(e12,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e11,e13)
& op1(e12,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e11,e12)
& op1(e12,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e11,e11)
& op1(e12,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e11,e10) ),
file('theBenchmark.p',ax5) ).
fof(ax6,axiom,
( op2(e23,e22) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e21)
& op2(e22,e22) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e21)
& op2(e21,e22) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e21)
& op2(e20,e22) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e21)
& op2(e22,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e21,e23)
& op2(e22,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e21,e22)
& op2(e22,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e21,e21)
& op2(e22,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e21,e20) ),
file('theBenchmark.p',ax6) ).
fof(ax7,axiom,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('theBenchmark.p',ax7) ).
fof(ax8,axiom,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('theBenchmark.p',ax8) ).
fof(ax10,axiom,
( ( ( op1(e13,e13) != e13
& op1(e13,e13) = e13 )
| ( op1(e12,e13) != e12
& op1(e12,e12) = e13 )
| ( op1(e11,e13) != e11
& op1(e11,e11) = e13 )
| ( op1(e10,e13) != e10
& op1(e10,e10) = e13 ) )
& ( ( op1(e13,e12) != e13
& op1(e13,e13) = e12 )
| ( op1(e12,e12) != e12
& op1(e12,e12) = e12 )
| ( op1(e11,e12) != e11
& op1(e11,e11) = e12 )
| ( op1(e10,e12) != e10
& op1(e10,e10) = e12 ) )
& ( ( op1(e13,e11) != e13
& op1(e13,e13) = e11 )
| ( op1(e12,e11) != e12
& op1(e12,e12) = e11 )
| ( op1(e11,e11) != e11
& op1(e11,e11) = e11 )
| ( op1(e10,e11) != e10
& op1(e10,e10) = e11 ) )
& ( ( op1(e13,e10) != e13
& op1(e13,e13) = e10 )
| ( op1(e12,e10) != e12
& op1(e12,e12) = e10 )
| ( op1(e11,e10) != e11
& op1(e11,e11) = e10 )
| ( op1(e10,e10) != e10
& op1(e10,e10) = e10 ) ) ),
file('theBenchmark.p',ax10) ).
fof(ax11,axiom,
( ( ( op2(e23,e23) != e23
& op2(e23,e23) = e23 )
| ( op2(e22,e23) != e22
& op2(e22,e22) = e23 )
| ( op2(e21,e23) != e21
& op2(e21,e21) = e23 )
| ( op2(e20,e23) != e20
& op2(e20,e20) = e23 ) )
& ( ( op2(e23,e22) != e23
& op2(e23,e23) = e22 )
| ( op2(e22,e22) != e22
& op2(e22,e22) = e22 )
| ( op2(e21,e22) != e21
& op2(e21,e21) = e22 )
| ( op2(e20,e22) != e20
& op2(e20,e20) = e22 ) )
& ( ( op2(e23,e21) != e23
& op2(e23,e23) = e21 )
| ( op2(e22,e21) != e22
& op2(e22,e22) = e21 )
| ( op2(e21,e21) != e21
& op2(e21,e21) = e21 )
| ( op2(e20,e21) != e20
& op2(e20,e20) = e21 ) )
& ( ( op2(e23,e20) != e23
& op2(e23,e23) = e20 )
| ( op2(e22,e20) != e22
& op2(e22,e22) = e20 )
| ( op2(e21,e20) != e21
& op2(e21,e21) = e20 )
| ( op2(e20,e20) != e20
& op2(e20,e20) = e20 ) ) ),
file('theBenchmark.p',ax11) ).
fof(ax12,axiom,
( e12 = op1(e13,e13)
& e11 = op1(op1(e13,e13),e13)
& e10 = op1(e13,op1(e13,e13)) ),
file('theBenchmark.p',ax12) ).
fof(ax13,axiom,
( e22 = op2(e23,e23)
& e21 = op2(op2(e23,e23),e23)
& e20 = op2(e23,op2(e23,e23)) ),
file('theBenchmark.p',ax13) ).
fof(ax14,axiom,
( h1(e12) = op2(e20,e20)
& h1(e11) = op2(op2(e20,e20),e20)
& h1(e10) = op2(e20,op2(e20,e20))
& h1(e13) = e20 ),
file('theBenchmark.p',ax14) ).
fof(ax15,axiom,
( h2(e12) = op2(e21,e21)
& h2(e11) = op2(op2(e21,e21),e21)
& h2(e10) = op2(e21,op2(e21,e21))
& h2(e13) = e21 ),
file('theBenchmark.p',ax15) ).
fof(ax16,axiom,
( h3(e12) = op2(e22,e22)
& h3(e11) = op2(op2(e22,e22),e22)
& h3(e10) = op2(e22,op2(e22,e22))
& h3(e13) = e22 ),
file('theBenchmark.p',ax16) ).
fof(ax17,axiom,
( h4(e12) = op2(e23,e23)
& h4(e11) = op2(op2(e23,e23),e23)
& h4(e10) = op2(e23,op2(e23,e23))
& h4(e13) = e23 ),
file('theBenchmark.p',ax17) ).
fof(co1,conjecture,
( ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& 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)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ( ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& 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)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_28,plain,
( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_31,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_35,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_36,plain,
( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_41,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_45,plain,
( op1(e11,e13) = e11
| op1(e11,e12) = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_46,plain,
( op1(e13,e11) = e11
| op1(e12,e11) = e11
| op1(e11,e11) = e11
| op1(e10,e11) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_47,plain,
( op1(e11,e13) = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_49,plain,
( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e11) = e13
| op1(e11,e10) = e13 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_56,plain,
( op1(e13,e12) = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_76,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_79,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_83,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_84,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| op2(e20,e20) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_89,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_93,plain,
( op2(e21,e23) = e21
| op2(e21,e22) = e21
| op2(e21,e21) = e21
| op2(e21,e20) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_95,plain,
( op2(e21,e23) = e22
| op2(e21,e22) = e22
| op2(e21,e21) = e22
| op2(e21,e20) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_97,plain,
( op2(e21,e23) = e23
| op2(e21,e22) = e23
| op2(e21,e21) = e23
| op2(e21,e20) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_104,plain,
( op2(e23,e22) = e22
| op2(e22,e22) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_109,plain,
( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_117,plain,
op1(e13,e10) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_118,plain,
op1(e10,e10) != op1(e13,e10),
inference(copy,[status(thm)],[c_117]) ).
cnf(c_128,plain,
op1(e12,e11) != op1(e11,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_135,plain,
op1(e13,e12) != op1(e10,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_136,plain,
op1(e10,e12) != op1(e13,e12),
inference(copy,[status(thm)],[c_135]) ).
cnf(c_140,plain,
op1(e13,e12) != op1(e12,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_141,plain,
op1(e12,e12) != op1(e13,e12),
inference(copy,[status(thm)],[c_140]) ).
cnf(c_146,plain,
op1(e12,e13) != op1(e11,e13),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_147,plain,
op1(e13,e13) != op1(e11,e13),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_148,plain,
op1(e11,e13) != op1(e13,e13),
inference(copy,[status(thm)],[c_147]) ).
cnf(c_151,plain,
op1(e10,e11) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_173,plain,
op1(e12,e12) != op1(e12,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_174,plain,
op1(e12,e13) != op1(e12,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_175,plain,
op1(e12,e11) != op1(e12,e13),
inference(copy,[status(thm)],[c_174]) ).
cnf(c_176,plain,
op1(e12,e13) != op1(e12,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_177,plain,
op1(e12,e12) != op1(e12,e13),
inference(copy,[status(thm)],[c_176]) ).
cnf(c_179,plain,
op1(e13,e12) != op1(e13,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_180,plain,
op1(e13,e13) != op1(e13,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_181,plain,
op1(e13,e10) != op1(e13,e13),
inference(copy,[status(thm)],[c_180]) ).
cnf(c_189,plain,
op2(e23,e20) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_190,plain,
op2(e20,e20) != op2(e23,e20),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_200,plain,
op2(e22,e21) != op2(e21,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_207,plain,
op2(e23,e22) != op2(e20,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_208,plain,
op2(e20,e22) != op2(e23,e22),
inference(copy,[status(thm)],[c_207]) ).
cnf(c_212,plain,
op2(e23,e22) != op2(e22,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_213,plain,
op2(e22,e22) != op2(e23,e22),
inference(copy,[status(thm)],[c_212]) ).
cnf(c_218,plain,
op2(e22,e23) != op2(e21,e23),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_219,plain,
op2(e23,e23) != op2(e21,e23),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_220,plain,
op2(e21,e23) != op2(e23,e23),
inference(copy,[status(thm)],[c_219]) ).
cnf(c_245,plain,
op2(e22,e22) != op2(e22,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_246,plain,
op2(e22,e23) != op2(e22,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_247,plain,
op2(e22,e21) != op2(e22,e23),
inference(copy,[status(thm)],[c_246]) ).
cnf(c_248,plain,
op2(e22,e23) != op2(e22,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_249,plain,
op2(e22,e22) != op2(e22,e23),
inference(copy,[status(thm)],[c_248]) ).
cnf(c_251,plain,
op2(e23,e22) != op2(e23,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_252,plain,
op2(e23,e23) != op2(e23,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_253,plain,
op2(e23,e20) != op2(e23,e23),
inference(copy,[status(thm)],[c_252]) ).
cnf(c_259,plain,
e11 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_260,plain,
e12 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_261,plain,
e13 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_262,plain,
e10 != e13,
inference(copy,[status(thm)],[c_261]) ).
cnf(c_263,plain,
e12 != e11,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_264,plain,
e13 != e11,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_265,plain,
e11 != e13,
inference(copy,[status(thm)],[c_264]) ).
cnf(c_266,plain,
e13 != e12,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_267,plain,
e12 != e13,
inference(copy,[status(thm)],[c_266]) ).
cnf(c_268,plain,
e21 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_269,plain,
e22 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_270,plain,
e23 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_271,plain,
e20 != e23,
inference(copy,[status(thm)],[c_270]) ).
cnf(c_272,plain,
e22 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_273,plain,
e23 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_274,plain,
e21 != e23,
inference(copy,[status(thm)],[c_273]) ).
cnf(c_275,plain,
e23 != e22,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_276,plain,
e22 != e23,
inference(copy,[status(thm)],[c_275]) ).
cnf(c_306,plain,
( op1(e13,e13) = e10
| op1(e12,e12) = e10
| op1(e11,e11) = e10 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_310,plain,
( op1(e13,e13) = e10
| op1(e12,e12) = e10
| op1(e11,e10) != e11 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_314,plain,
( op1(e13,e13) = e11
| op1(e12,e12) = e11
| op1(e10,e10) = e11 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_318,plain,
( op1(e13,e13) = e11
| op1(e12,e12) = e11
| op1(e10,e11) != e10 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_330,plain,
( op1(e12,e12) = e13
| op1(e11,e11) = e13
| op1(e10,e10) = e13 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_338,plain,
( op2(e23,e23) = e20
| op2(e22,e22) = e20
| op2(e21,e21) = e20 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_342,plain,
( op2(e23,e23) = e20
| op2(e22,e22) = e20
| op2(e21,e20) != e21 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_346,plain,
( op2(e23,e23) = e21
| op2(e22,e22) = e21
| op2(e20,e20) = e21 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_350,plain,
( op2(e23,e23) = e21
| op2(e22,e22) = e21
| op2(e20,e21) != e20 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_362,plain,
( op2(e22,e22) = e23
| op2(e21,e21) = e23
| op2(e20,e20) = e23 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_370,plain,
op1(e13,op1(e13,e13)) = e10,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_371,plain,
op1(op1(e13,e13),e13) = e11,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_372,plain,
op1(e13,e13) = e12,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_373,plain,
op2(e23,op2(e23,e23)) = e20,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_374,plain,
op2(op2(e23,e23),e23) = e21,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_375,plain,
op2(e23,e23) = e22,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_377,plain,
h1(e10) = op2(e20,op2(e20,e20)),
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_378,plain,
op2(e20,op2(e20,e20)) = h1(e10),
inference(copy,[status(thm)],[c_377]) ).
cnf(c_379,plain,
h1(e11) = op2(op2(e20,e20),e20),
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_380,plain,
op2(op2(e20,e20),e20) = h1(e11),
inference(copy,[status(thm)],[c_379]) ).
cnf(c_381,plain,
h1(e12) = op2(e20,e20),
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_382,plain,
op2(e20,e20) = h1(e12),
inference(copy,[status(thm)],[c_381]) ).
cnf(c_383,plain,
h2(e13) = e21,
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_384,plain,
h2(e10) = op2(e21,op2(e21,e21)),
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_385,plain,
op2(e21,op2(e21,e21)) = h2(e10),
inference(copy,[status(thm)],[c_384]) ).
cnf(c_386,plain,
h2(e11) = op2(op2(e21,e21),e21),
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_387,plain,
op2(op2(e21,e21),e21) = h2(e11),
inference(copy,[status(thm)],[c_386]) ).
cnf(c_388,plain,
h2(e12) = op2(e21,e21),
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_389,plain,
op2(e21,e21) = h2(e12),
inference(copy,[status(thm)],[c_388]) ).
cnf(c_395,plain,
h3(e12) = op2(e22,e22),
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_396,plain,
op2(e22,e22) = h3(e12),
inference(copy,[status(thm)],[c_395]) ).
cnf(c_398,plain,
h4(e10) = op2(e23,op2(e23,e23)),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_2117,plain,
h4(e10) = op2(e23,e22),
inference(paramod,[status(thm)],[c_375,c_398]) ).
cnf(c_399,plain,
op2(e23,e22) = h4(e10),
inference(copy,[status(thm)],[c_2117]) ).
cnf(c_400,plain,
h4(e11) = op2(op2(e23,e23),e23),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_2118,plain,
h4(e11) = op2(e22,e23),
inference(paramod,[status(thm)],[c_375,c_400]) ).
cnf(c_401,plain,
op2(e22,e23) = h4(e11),
inference(copy,[status(thm)],[c_2118]) ).
cnf(c_1045,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| 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)) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_2119,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| 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),e21)
| 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)) ),
inference(paramod,[status(thm)],[c_383,c_1045]) ).
cnf(c_2120,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| 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),e21)
| 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),e21)
| 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)) ),
inference(paramod,[status(thm)],[c_383,c_2119]) ).
cnf(c_2121,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| 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),e21)
| 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),e21)
| 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),e21)
| 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)) ),
inference(paramod,[status(thm)],[c_383,c_2120]) ).
cnf(c_2122,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| 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(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| 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),e21)
| 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)) ),
inference(paramod,[status(thm)],[c_383,c_2121]) ).
cnf(c_2123,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| 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),e21)
| 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)) ),
inference(paramod,[status(thm)],[c_383,c_2122]) ).
cnf(c_2124,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| 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),e21)
| 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)) ),
inference(paramod,[status(thm)],[c_383,c_2123]) ).
cnf(c_2125,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| h2(e12) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| 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),e21)
| 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)) ),
inference(paramod,[status(thm)],[c_372,c_2124]) ).
cnf(c_2126,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| h2(e12) != op2(e21,h2(e13))
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| 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),e21)
| 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)) ),
inference(paramod,[status(thm)],[c_383,c_2125]) ).
cnf(c_2127,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| h2(e12) != op2(e21,e21)
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| 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),e21)
| 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)) ),
inference(paramod,[status(thm)],[c_383,c_2126]) ).
cnf(c_2128,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| h2(e12) != h2(e12)
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| 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),e21)
| 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)) ),
inference(paramod,[status(thm)],[c_389,c_2127]) ).
cnf(c_2129,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e12) != h2(e12)
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| 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),e21)
| 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)) ),
inference(paramod,[status(thm)],[c_383,c_2128]) ).
cnf(c_2130,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e12) != h2(e12)
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| 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),e21)
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2129]) ).
cnf(c_2131,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e12) != h2(e12)
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| 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),e21)
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2130]) ).
cnf(c_2132,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e12) != h2(e12)
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| 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),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2131]) ).
cnf(c_2133,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e12) != h2(e12)
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2132]) ).
cnf(c_2134,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e12) != h2(e12)
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2133]) ).
cnf(c_2135,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e12) != h2(e12)
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| 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),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2134]) ).
cnf(c_2136,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e12) != h2(e12)
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2135]) ).
cnf(c_2137,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e12) != h2(e12)
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2136]) ).
cnf(c_2138,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e12) != h2(e12)
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2137]) ).
cnf(c_2139,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2138]) ).
cnf(c_1046,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2139]) ).
cnf(c_1788,plain,
op1(e12,e13) = e11,
inference(paramod,[status(thm)],[c_372,c_371]) ).
cnf(c_1789,plain,
op1(e13,e12) = e10,
inference(paramod,[status(thm)],[c_372,c_370]) ).
cnf(c_2140,plain,
( e12 = e11
| op1(e12,e12) = e11
| op1(e10,e11) != e10 ),
inference(paramod,[status(thm)],[c_372,c_318]) ).
cnf(c_1791,plain,
( op1(e12,e12) = e11
| op1(e10,e11) != e10 ),
inference(resolve,[status(thm)],[c_263,c_2140]) ).
cnf(c_2141,plain,
( e12 = e11
| op1(e12,e12) = e11
| op1(e10,e10) = e11 ),
inference(paramod,[status(thm)],[c_372,c_314]) ).
cnf(c_1793,plain,
( op1(e12,e12) = e11
| op1(e10,e10) = e11 ),
inference(resolve,[status(thm)],[c_263,c_2141]) ).
cnf(c_2142,plain,
( e12 = e10
| op1(e12,e12) = e10
| op1(e11,e10) != e11 ),
inference(paramod,[status(thm)],[c_372,c_310]) ).
cnf(c_1795,plain,
( op1(e12,e12) = e10
| op1(e11,e10) != e11 ),
inference(resolve,[status(thm)],[c_260,c_2142]) ).
cnf(c_2143,plain,
( e12 = e10
| op1(e12,e12) = e10
| op1(e11,e11) = e10 ),
inference(paramod,[status(thm)],[c_372,c_306]) ).
cnf(c_1797,plain,
( op1(e12,e12) = e10
| op1(e11,e11) = e10 ),
inference(resolve,[status(thm)],[c_260,c_2143]) ).
cnf(c_1799,plain,
op1(e13,e10) != e12,
inference(paramod,[status(thm)],[c_372,c_181]) ).
cnf(c_1800,plain,
op1(e11,e13) != e12,
inference(paramod,[status(thm)],[c_372,c_148]) ).
cnf(c_2144,plain,
op2(e22,e23) = e21,
inference(paramod,[status(thm)],[c_375,c_374]) ).
cnf(c_1806,plain,
h4(e11) = e21,
inference(paramod,[status(thm)],[c_401,c_2144]) ).
cnf(c_2145,plain,
op2(e23,e22) = e20,
inference(paramod,[status(thm)],[c_375,c_373]) ).
cnf(c_1807,plain,
h4(e10) = e20,
inference(paramod,[status(thm)],[c_399,c_2145]) ).
cnf(c_2146,plain,
( op2(e23,e23) = e21
| h3(e12) = e21
| op2(e20,e21) != e20 ),
inference(paramod,[status(thm)],[c_396,c_350]) ).
cnf(c_2147,plain,
( e22 = e21
| h3(e12) = e21
| op2(e20,e21) != e20 ),
inference(paramod,[status(thm)],[c_375,c_2146]) ).
cnf(c_1809,plain,
( h3(e12) = e21
| op2(e20,e21) != e20 ),
inference(resolve,[status(thm)],[c_272,c_2147]) ).
cnf(c_2148,plain,
( op2(e23,e23) = e21
| op2(e22,e22) = e21
| h1(e12) = e21 ),
inference(paramod,[status(thm)],[c_382,c_346]) ).
cnf(c_2149,plain,
( op2(e23,e23) = e21
| h3(e12) = e21
| h1(e12) = e21 ),
inference(paramod,[status(thm)],[c_396,c_2148]) ).
cnf(c_2150,plain,
( e22 = e21
| h3(e12) = e21
| h1(e12) = e21 ),
inference(paramod,[status(thm)],[c_375,c_2149]) ).
cnf(c_1811,plain,
( h3(e12) = e21
| h1(e12) = e21 ),
inference(resolve,[status(thm)],[c_272,c_2150]) ).
cnf(c_2151,plain,
( op2(e23,e23) = e20
| h3(e12) = e20
| op2(e21,e20) != e21 ),
inference(paramod,[status(thm)],[c_396,c_342]) ).
cnf(c_2152,plain,
( e22 = e20
| h3(e12) = e20
| op2(e21,e20) != e21 ),
inference(paramod,[status(thm)],[c_375,c_2151]) ).
cnf(c_1813,plain,
( h3(e12) = e20
| op2(e21,e20) != e21 ),
inference(resolve,[status(thm)],[c_269,c_2152]) ).
cnf(c_2153,plain,
( op2(e23,e23) = e20
| op2(e22,e22) = e20
| h2(e12) = e20 ),
inference(paramod,[status(thm)],[c_389,c_338]) ).
cnf(c_2154,plain,
( op2(e23,e23) = e20
| h3(e12) = e20
| h2(e12) = e20 ),
inference(paramod,[status(thm)],[c_396,c_2153]) ).
cnf(c_2155,plain,
( e22 = e20
| h3(e12) = e20
| h2(e12) = e20 ),
inference(paramod,[status(thm)],[c_375,c_2154]) ).
cnf(c_1815,plain,
( h3(e12) = e20
| h2(e12) = e20 ),
inference(resolve,[status(thm)],[c_269,c_2155]) ).
cnf(c_1817,plain,
op2(e23,e20) != e22,
inference(paramod,[status(thm)],[c_375,c_253]) ).
cnf(c_1818,plain,
op2(e21,e23) != e22,
inference(paramod,[status(thm)],[c_375,c_220]) ).
cnf(c_2156,plain,
( op2(e23,e23) = e21
| h4(e10) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(paramod,[status(thm)],[c_399,c_109]) ).
cnf(c_2157,plain,
( op2(e23,e23) = e21
| e20 = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(paramod,[status(thm)],[c_1807,c_2156]) ).
cnf(c_2158,plain,
( e22 = e21
| e20 = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(paramod,[status(thm)],[c_375,c_2157]) ).
cnf(c_2159,plain,
( e22 = e21
| e21 = e20
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(copy,[status(thm)],[c_2158]) ).
cnf(c_2160,plain,
( e22 = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(resolve,[status(thm)],[c_268,c_2159]) ).
cnf(c_1822,plain,
( op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(resolve,[status(thm)],[c_272,c_2160]) ).
cnf(c_1824,plain,
op2(h1(e12),e20) = h1(e11),
inference(paramod,[status(thm)],[c_382,c_380]) ).
cnf(c_1825,plain,
op2(e20,h1(e12)) = h1(e10),
inference(paramod,[status(thm)],[c_382,c_378]) ).
cnf(c_2161,plain,
( op2(e22,e22) = e23
| op2(e21,e21) = e23
| h1(e12) = e23 ),
inference(paramod,[status(thm)],[c_382,c_362]) ).
cnf(c_2162,plain,
( op2(e22,e22) = e23
| h2(e12) = e23
| h1(e12) = e23 ),
inference(paramod,[status(thm)],[c_389,c_2161]) ).
cnf(c_1827,plain,
( h3(e12) = e23
| h2(e12) = e23
| h1(e12) = e23 ),
inference(paramod,[status(thm)],[c_396,c_2162]) ).
cnf(c_2163,plain,
h1(e12) != op2(e23,e20),
inference(paramod,[status(thm)],[c_382,c_190]) ).
cnf(c_1831,plain,
op2(e23,e20) != h1(e12),
inference(copy,[status(thm)],[c_2163]) ).
cnf(c_1835,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| h1(e12) = e23 ),
inference(paramod,[status(thm)],[c_382,c_89]) ).
cnf(c_1840,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| h1(e12) = e20 ),
inference(paramod,[status(thm)],[c_382,c_84]) ).
cnf(c_1841,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| h1(e12) = e20 ),
inference(paramod,[status(thm)],[c_382,c_83]) ).
cnf(c_1843,plain,
op2(h2(e12),e21) = h2(e11),
inference(paramod,[status(thm)],[c_389,c_387]) ).
cnf(c_1844,plain,
op2(e21,h2(e12)) = h2(e10),
inference(paramod,[status(thm)],[c_389,c_385]) ).
cnf(c_1850,plain,
op2(e22,e21) != h2(e12),
inference(paramod,[status(thm)],[c_389,c_200]) ).
cnf(c_1853,plain,
( op2(e21,e23) = e23
| op2(e21,e22) = e23
| h2(e12) = e23
| op2(e21,e20) = e23 ),
inference(paramod,[status(thm)],[c_389,c_97]) ).
cnf(c_2164,plain,
( op2(e21,e23) = e22
| op2(e21,e22) = e22
| h2(e12) = e22
| op2(e21,e20) = e22 ),
inference(paramod,[status(thm)],[c_389,c_95]) ).
cnf(c_1855,plain,
( op2(e21,e22) = e22
| h2(e12) = e22
| op2(e21,e20) = e22 ),
inference(resolve,[status(thm)],[c_1818,c_2164]) ).
cnf(c_1857,plain,
( op2(e21,e23) = e21
| op2(e21,e22) = e21
| h2(e12) = e21
| op2(e21,e20) = e21 ),
inference(paramod,[status(thm)],[c_389,c_93]) ).
cnf(c_2165,plain,
h3(e12) != op2(e22,e23),
inference(paramod,[status(thm)],[c_396,c_249]) ).
cnf(c_2166,plain,
h3(e12) != h4(e11),
inference(paramod,[status(thm)],[c_401,c_2165]) ).
cnf(c_1864,plain,
h3(e12) != e21,
inference(paramod,[status(thm)],[c_1806,c_2166]) ).
cnf(c_2167,plain,
h3(e12) != op2(e22,e21),
inference(paramod,[status(thm)],[c_396,c_245]) ).
cnf(c_1865,plain,
op2(e22,e21) != h3(e12),
inference(copy,[status(thm)],[c_2167]) ).
cnf(c_2168,plain,
h3(e12) != op2(e23,e22),
inference(paramod,[status(thm)],[c_396,c_213]) ).
cnf(c_2169,plain,
h3(e12) != h4(e10),
inference(paramod,[status(thm)],[c_399,c_2168]) ).
cnf(c_1867,plain,
h3(e12) != e20,
inference(paramod,[status(thm)],[c_1807,c_2169]) ).
cnf(c_2170,plain,
( op2(e23,e22) = e22
| h3(e12) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_396,c_104]) ).
cnf(c_2171,plain,
( h4(e10) = e22
| h3(e12) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_399,c_2170]) ).
cnf(c_2172,plain,
( e20 = e22
| h3(e12) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_1807,c_2171]) ).
cnf(c_2173,plain,
( e22 = e20
| h3(e12) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(copy,[status(thm)],[c_2172]) ).
cnf(c_1872,plain,
( h3(e12) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(resolve,[status(thm)],[c_269,c_2173]) ).
cnf(c_2174,plain,
h4(e10) != op2(e23,e20),
inference(paramod,[status(thm)],[c_399,c_251]) ).
cnf(c_2175,plain,
e20 != op2(e23,e20),
inference(paramod,[status(thm)],[c_1807,c_2174]) ).
cnf(c_1878,plain,
op2(e23,e20) != e20,
inference(copy,[status(thm)],[c_2175]) ).
cnf(c_2176,plain,
op2(e20,e22) != h4(e10),
inference(paramod,[status(thm)],[c_399,c_208]) ).
cnf(c_1880,plain,
op2(e20,e22) != e20,
inference(paramod,[status(thm)],[c_1807,c_2176]) ).
cnf(c_2177,plain,
op2(e22,e21) != h4(e11),
inference(paramod,[status(thm)],[c_401,c_247]) ).
cnf(c_1881,plain,
op2(e22,e21) != e21,
inference(paramod,[status(thm)],[c_1806,c_2177]) ).
cnf(c_2178,plain,
h4(e11) != op2(e21,e23),
inference(paramod,[status(thm)],[c_401,c_218]) ).
cnf(c_2179,plain,
e21 != op2(e21,e23),
inference(paramod,[status(thm)],[c_1806,c_2178]) ).
cnf(c_1883,plain,
op2(e21,e23) != e21,
inference(copy,[status(thm)],[c_2179]) ).
cnf(c_2180,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(e11) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1788,c_1046]) ).
cnf(c_2181,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(e11) != h2(e11)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1843,c_2180]) ).
cnf(c_2182,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(e10) != op2(e21,h2(e12))
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(e11) != h2(e11)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1789,c_2181]) ).
cnf(c_2183,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(e10) != h2(e10)
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(e11) != h2(e11)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1844,c_2182]) ).
cnf(c_2184,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(e10) != h2(e10)
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2183]) ).
cnf(c_1905,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2184]) ).
cnf(c_1952,plain,
op1(e12,e12) != e11,
inference(paramod,[status(thm)],[c_1788,c_177]) ).
cnf(c_1953,plain,
op1(e12,e11) != e11,
inference(paramod,[status(thm)],[c_1788,c_175]) ).
cnf(c_2185,plain,
e11 != op1(e11,e13),
inference(paramod,[status(thm)],[c_1788,c_146]) ).
cnf(c_1955,plain,
op1(e11,e13) != e11,
inference(copy,[status(thm)],[c_2185]) ).
cnf(c_2186,plain,
e10 != op1(e13,e10),
inference(paramod,[status(thm)],[c_1789,c_179]) ).
cnf(c_1961,plain,
op1(e13,e10) != e10,
inference(copy,[status(thm)],[c_2186]) ).
cnf(c_1962,plain,
op1(e12,e12) != e10,
inference(paramod,[status(thm)],[c_1789,c_141]) ).
cnf(c_1964,plain,
op1(e10,e12) != e10,
inference(paramod,[status(thm)],[c_1789,c_136]) ).
cnf(c_2187,plain,
( e10 = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_1789,c_56]) ).
cnf(c_2188,plain,
( e12 = e10
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(copy,[status(thm)],[c_2187]) ).
cnf(c_1966,plain,
( op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(resolve,[status(thm)],[c_260,c_2188]) ).
cnf(c_2189,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11 ),
inference(resolve,[status(thm)],[c_1961,c_31]) ).
cnf(c_1971,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e11 ),
inference(resolve,[status(thm)],[c_1799,c_2189]) ).
cnf(c_1972,plain,
( op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 ),
inference(resolve,[status(thm)],[c_1800,c_47]) ).
cnf(c_1976,plain,
op2(e22,e23) = e21,
inference(paramod,[status(thm)],[c_1806,c_401]) ).
cnf(c_1977,plain,
op2(e23,e22) = e20,
inference(paramod,[status(thm)],[c_1807,c_399]) ).
cnf(c_2190,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21 ),
inference(resolve,[status(thm)],[c_1878,c_79]) ).
cnf(c_1979,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e21 ),
inference(resolve,[status(thm)],[c_1817,c_2190]) ).
cnf(c_1982,plain,
h1(e12) = e21,
inference(resolve,[status(thm)],[c_1864,c_1811]) ).
cnf(c_1983,plain,
op2(e20,e21) != e20,
inference(resolve,[status(thm)],[c_1864,c_1809]) ).
cnf(c_1984,plain,
h2(e12) = e20,
inference(resolve,[status(thm)],[c_1867,c_1815]) ).
cnf(c_1985,plain,
op2(e21,e20) != e21,
inference(resolve,[status(thm)],[c_1867,c_1813]) ).
cnf(c_2191,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| e21 = e20 ),
inference(paramod,[status(thm)],[c_1982,c_1840]) ).
cnf(c_2192,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20 ),
inference(resolve,[status(thm)],[c_268,c_2191]) ).
cnf(c_1986,plain,
( op2(e22,e20) = e20
| op2(e21,e20) = e20 ),
inference(resolve,[status(thm)],[c_1878,c_2192]) ).
cnf(c_2193,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| e21 = e20 ),
inference(paramod,[status(thm)],[c_1982,c_1841]) ).
cnf(c_2194,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20 ),
inference(resolve,[status(thm)],[c_268,c_2193]) ).
cnf(c_2195,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20 ),
inference(resolve,[status(thm)],[c_1983,c_2194]) ).
cnf(c_1988,plain,
op2(e20,e23) = e20,
inference(resolve,[status(thm)],[c_1880,c_2195]) ).
cnf(c_1991,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e20 ),
inference(resolve,[status(thm)],[c_1881,c_76]) ).
cnf(c_2196,plain,
( op2(e21,e23) = e21
| op2(e21,e22) = e21
| e20 = e21
| op2(e21,e20) = e21 ),
inference(paramod,[status(thm)],[c_1984,c_1857]) ).
cnf(c_2197,plain,
( op2(e21,e23) = e21
| op2(e21,e22) = e21
| e21 = e20
| op2(e21,e20) = e21 ),
inference(copy,[status(thm)],[c_2196]) ).
cnf(c_2198,plain,
( op2(e21,e23) = e21
| op2(e21,e22) = e21
| e21 = e20 ),
inference(resolve,[status(thm)],[c_1985,c_2197]) ).
cnf(c_2199,plain,
( op2(e21,e23) = e21
| op2(e21,e22) = e21 ),
inference(resolve,[status(thm)],[c_268,c_2198]) ).
cnf(c_1993,plain,
op2(e21,e22) = e21,
inference(resolve,[status(thm)],[c_1883,c_2199]) ).
cnf(c_1994,plain,
op1(e10,e10) = e11,
inference(resolve,[status(thm)],[c_1952,c_1793]) ).
cnf(c_1995,plain,
op1(e10,e11) != e10,
inference(resolve,[status(thm)],[c_1952,c_1791]) ).
cnf(c_1997,plain,
( op1(e13,e11) = e11
| op1(e11,e11) = e11
| op1(e10,e11) = e11 ),
inference(resolve,[status(thm)],[c_1953,c_46]) ).
cnf(c_1998,plain,
( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e10 ),
inference(resolve,[status(thm)],[c_1953,c_28]) ).
cnf(c_2000,plain,
( op1(e11,e12) = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 ),
inference(resolve,[status(thm)],[c_1955,c_45]) ).
cnf(c_2200,plain,
( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| e11 = e10 ),
inference(paramod,[status(thm)],[c_1994,c_36]) ).
cnf(c_2201,plain,
( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10 ),
inference(resolve,[status(thm)],[c_259,c_2200]) ).
cnf(c_2002,plain,
( op1(e12,e10) = e10
| op1(e11,e10) = e10 ),
inference(resolve,[status(thm)],[c_1961,c_2201]) ).
cnf(c_2004,plain,
op1(e11,e11) = e10,
inference(resolve,[status(thm)],[c_1962,c_1797]) ).
cnf(c_2005,plain,
op1(e11,e10) != e11,
inference(resolve,[status(thm)],[c_1962,c_1795]) ).
cnf(c_2202,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| e11 = e10 ),
inference(paramod,[status(thm)],[c_1994,c_35]) ).
cnf(c_2203,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10 ),
inference(resolve,[status(thm)],[c_259,c_2202]) ).
cnf(c_2204,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10 ),
inference(resolve,[status(thm)],[c_1995,c_2203]) ).
cnf(c_2007,plain,
op1(e10,e13) = e10,
inference(resolve,[status(thm)],[c_1964,c_2204]) ).
cnf(c_2205,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_1982,c_1835]) ).
cnf(c_2206,plain,
( e20 = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_1988,c_2205]) ).
cnf(c_2207,plain,
( e20 = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_274,c_2206]) ).
cnf(c_2024,plain,
( op2(e20,e22) = e23
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_271,c_2207]) ).
cnf(c_2026,plain,
op2(e23,e20) != e21,
inference(paramod,[status(thm)],[c_1982,c_1831]) ).
cnf(c_2208,plain,
( h3(e12) = e23
| h2(e12) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_1982,c_1827]) ).
cnf(c_2209,plain,
( h3(e12) = e23
| e20 = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_1984,c_2208]) ).
cnf(c_2210,plain,
( h3(e12) = e23
| e20 = e23 ),
inference(resolve,[status(thm)],[c_274,c_2209]) ).
cnf(c_2029,plain,
h3(e12) = e23,
inference(resolve,[status(thm)],[c_271,c_2210]) ).
cnf(c_2030,plain,
op2(e20,e21) = h1(e10),
inference(paramod,[status(thm)],[c_1982,c_1825]) ).
cnf(c_2031,plain,
op2(e21,e20) = h1(e11),
inference(paramod,[status(thm)],[c_1982,c_1824]) ).
cnf(c_2032,plain,
op2(e20,e20) = e21,
inference(paramod,[status(thm)],[c_1982,c_382]) ).
cnf(c_2211,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(paramod,[status(thm)],[c_1994,c_1905]) ).
cnf(c_2212,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),e20) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(paramod,[status(thm)],[c_1984,c_2211]) ).
cnf(c_2213,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(e10) != op2(h2(e10),e21)
| op2(h2(e10),e20) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(paramod,[status(thm)],[c_2007,c_2212]) ).
cnf(c_2214,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e12)) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(e10) != op2(h2(e10),e21)
| op2(h2(e10),e20) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(paramod,[status(thm)],[c_2004,c_2213]) ).
cnf(c_2215,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),e20) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(e10) != op2(h2(e10),e21)
| op2(h2(e10),e20) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(paramod,[status(thm)],[c_1984,c_2214]) ).
cnf(c_2216,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),h2(e11)) != h2(op1(e12,e11))
| op2(e20,h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),e20) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(e10) != op2(h2(e10),e21)
| op2(h2(e10),e20) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(paramod,[status(thm)],[c_1984,c_2215]) ).
cnf(c_2217,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(e20,h2(e11)) != h2(op1(e12,e11))
| op2(e20,h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),e20) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(e10) != op2(h2(e10),e21)
| op2(h2(e10),e20) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(paramod,[status(thm)],[c_1984,c_2216]) ).
cnf(c_2218,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| op2(e20,h2(e12)) != h2(op1(e12,e12))
| op2(e20,h2(e11)) != h2(op1(e12,e11))
| op2(e20,h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),e20) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(e10) != op2(h2(e10),e21)
| op2(h2(e10),e20) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(paramod,[status(thm)],[c_1984,c_2217]) ).
cnf(c_2219,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| op2(e20,e20) != h2(op1(e12,e12))
| op2(e20,h2(e11)) != h2(op1(e12,e11))
| op2(e20,h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),e20) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(e10) != op2(h2(e10),e21)
| op2(h2(e10),e20) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(paramod,[status(thm)],[c_1984,c_2218]) ).
cnf(c_2220,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| e21 != h2(op1(e12,e12))
| op2(e20,h2(e11)) != h2(op1(e12,e11))
| op2(e20,h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),e20) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(e10) != op2(h2(e10),e21)
| op2(h2(e10),e20) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(paramod,[status(thm)],[c_2032,c_2219]) ).
cnf(c_2221,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e20 != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| e21 != h2(op1(e12,e12))
| op2(e20,h2(e11)) != h2(op1(e12,e11))
| op2(e20,h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),e20) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(e10) != op2(h2(e10),e21)
| op2(h2(e10),e20) != h2(op1(e10,e12))
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(paramod,[status(thm)],[c_1984,c_2220]) ).
cnf(c_2222,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e20 != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| e21 != h2(op1(e12,e12))
| op2(e20,h2(e11)) != h2(op1(e12,e11))
| op2(e20,h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),e20) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(e10) != op2(h2(e10),e21)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(copy,[status(thm)],[c_2221]) ).
cnf(c_2223,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e20 != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| e21 != h2(op1(e12,e12))
| op2(e20,h2(e11)) != h2(op1(e12,e11))
| op2(e20,h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| op2(h2(e11),e20) != h2(op1(e11,e12))
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(copy,[status(thm)],[c_2222]) ).
cnf(c_2224,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e20 != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| e21 != h2(op1(e12,e12))
| op2(e20,h2(e11)) != h2(op1(e12,e11))
| op2(e20,h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(copy,[status(thm)],[c_2223]) ).
cnf(c_2225,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e20 != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| e21 != h2(op1(e12,e12))
| op2(e20,h2(e11)) != h2(op1(e12,e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(copy,[status(thm)],[c_2224]) ).
cnf(c_2226,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e20 != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| e21 != h2(op1(e12,e12))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(copy,[status(thm)],[c_2225]) ).
cnf(c_2227,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e20 != e20
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(copy,[status(thm)],[c_2226]) ).
cnf(c_2043,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e11) ),
inference(copy,[status(thm)],[c_2227]) ).
cnf(c_2228,plain,
( op2(e21,e22) = e22
| h2(e12) = e22
| h1(e11) = e22 ),
inference(paramod,[status(thm)],[c_2031,c_1855]) ).
cnf(c_2229,plain,
( op2(e21,e22) = e22
| e20 = e22
| h1(e11) = e22 ),
inference(paramod,[status(thm)],[c_1984,c_2228]) ).
cnf(c_2230,plain,
( e21 = e22
| e20 = e22
| h1(e11) = e22 ),
inference(paramod,[status(thm)],[c_1993,c_2229]) ).
cnf(c_2231,plain,
( e21 = e22
| e22 = e20
| h1(e11) = e22 ),
inference(copy,[status(thm)],[c_2230]) ).
cnf(c_2232,plain,
( e22 = e21
| e22 = e20
| h1(e11) = e22 ),
inference(copy,[status(thm)],[c_2231]) ).
cnf(c_2233,plain,
( e22 = e21
| h1(e11) = e22 ),
inference(resolve,[status(thm)],[c_269,c_2232]) ).
cnf(c_2046,plain,
h1(e11) = e22,
inference(resolve,[status(thm)],[c_272,c_2233]) ).
cnf(c_2234,plain,
( op2(e21,e23) = e23
| op2(e21,e22) = e23
| h2(e12) = e23
| h1(e11) = e23 ),
inference(paramod,[status(thm)],[c_2031,c_1853]) ).
cnf(c_2235,plain,
( op2(e21,e23) = e23
| op2(e21,e22) = e23
| h2(e12) = e23
| e22 = e23 ),
inference(paramod,[status(thm)],[c_2046,c_2234]) ).
cnf(c_2236,plain,
( op2(e21,e23) = e23
| op2(e21,e22) = e23
| e20 = e23
| e22 = e23 ),
inference(paramod,[status(thm)],[c_1984,c_2235]) ).
cnf(c_2237,plain,
( op2(e21,e23) = e23
| e21 = e23
| e20 = e23
| e22 = e23 ),
inference(paramod,[status(thm)],[c_1993,c_2236]) ).
cnf(c_2238,plain,
( op2(e21,e23) = e23
| e21 = e23
| e20 = e23 ),
inference(resolve,[status(thm)],[c_276,c_2237]) ).
cnf(c_2239,plain,
( op2(e21,e23) = e23
| e21 = e23 ),
inference(resolve,[status(thm)],[c_271,c_2238]) ).
cnf(c_2048,plain,
op2(e21,e23) = e23,
inference(resolve,[status(thm)],[c_274,c_2239]) ).
cnf(c_2051,plain,
op2(e22,e21) != e20,
inference(paramod,[status(thm)],[c_1984,c_1850]) ).
cnf(c_2240,plain,
op2(e21,e20) = h2(e10),
inference(paramod,[status(thm)],[c_1984,c_1844]) ).
cnf(c_2241,plain,
h1(e11) = h2(e10),
inference(paramod,[status(thm)],[c_2031,c_2240]) ).
cnf(c_2242,plain,
e22 = h2(e10),
inference(paramod,[status(thm)],[c_2046,c_2241]) ).
cnf(c_2052,plain,
h2(e10) = e22,
inference(copy,[status(thm)],[c_2242]) ).
cnf(c_2243,plain,
op2(e20,e21) = h2(e11),
inference(paramod,[status(thm)],[c_1984,c_1843]) ).
cnf(c_2244,plain,
h1(e10) = h2(e11),
inference(paramod,[status(thm)],[c_2030,c_2243]) ).
cnf(c_2053,plain,
h2(e11) = h1(e10),
inference(copy,[status(thm)],[c_2244]) ).
cnf(c_2245,plain,
( h3(e12) = e22
| e21 = e22
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_1993,c_1872]) ).
cnf(c_2246,plain,
( e23 = e22
| e21 = e22
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_2029,c_2245]) ).
cnf(c_2247,plain,
( e23 = e22
| e22 = e21
| op2(e20,e22) = e22 ),
inference(copy,[status(thm)],[c_2246]) ).
cnf(c_2248,plain,
( e22 = e23
| e22 = e21
| op2(e20,e22) = e22 ),
inference(copy,[status(thm)],[c_2247]) ).
cnf(c_2249,plain,
( e22 = e23
| op2(e20,e22) = e22 ),
inference(resolve,[status(thm)],[c_272,c_2248]) ).
cnf(c_2055,plain,
op2(e20,e22) = e22,
inference(resolve,[status(thm)],[c_276,c_2249]) ).
cnf(c_2250,plain,
( op1(e12,e12) = e13
| op1(e11,e11) = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_1994,c_330]) ).
cnf(c_2251,plain,
( op1(e12,e12) = e13
| e10 = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_2004,c_2250]) ).
cnf(c_2252,plain,
( op1(e12,e12) = e13
| e10 = e13 ),
inference(resolve,[status(thm)],[c_265,c_2251]) ).
cnf(c_2070,plain,
op1(e12,e12) = e13,
inference(resolve,[status(thm)],[c_262,c_2252]) ).
cnf(c_2072,plain,
op1(e10,e11) != e11,
inference(paramod,[status(thm)],[c_1994,c_151]) ).
cnf(c_2253,plain,
e11 != op1(e13,e10),
inference(paramod,[status(thm)],[c_1994,c_118]) ).
cnf(c_2073,plain,
op1(e13,e10) != e11,
inference(copy,[status(thm)],[c_2253]) ).
cnf(c_2254,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_1994,c_41]) ).
cnf(c_2255,plain,
( e10 = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_2007,c_2254]) ).
cnf(c_2256,plain,
( e10 = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13 ),
inference(resolve,[status(thm)],[c_265,c_2255]) ).
cnf(c_2075,plain,
( op1(e10,e12) = e13
| op1(e10,e11) = e13 ),
inference(resolve,[status(thm)],[c_262,c_2256]) ).
cnf(c_2257,plain,
( op1(e11,e12) = e11
| e10 = e11
| op1(e11,e10) = e11 ),
inference(paramod,[status(thm)],[c_2004,c_2000]) ).
cnf(c_2258,plain,
( op1(e11,e12) = e11
| e11 = e10
| op1(e11,e10) = e11 ),
inference(copy,[status(thm)],[c_2257]) ).
cnf(c_2259,plain,
( op1(e11,e12) = e11
| e11 = e10 ),
inference(resolve,[status(thm)],[c_2005,c_2258]) ).
cnf(c_2077,plain,
op1(e11,e12) = e11,
inference(resolve,[status(thm)],[c_259,c_2259]) ).
cnf(c_2260,plain,
( op1(e13,e11) = e11
| e10 = e11
| op1(e10,e11) = e11 ),
inference(paramod,[status(thm)],[c_2004,c_1997]) ).
cnf(c_2261,plain,
( op1(e13,e11) = e11
| e11 = e10
| op1(e10,e11) = e11 ),
inference(copy,[status(thm)],[c_2260]) ).
cnf(c_2262,plain,
( op1(e13,e11) = e11
| e11 = e10 ),
inference(resolve,[status(thm)],[c_2072,c_2261]) ).
cnf(c_2078,plain,
op1(e13,e11) = e11,
inference(resolve,[status(thm)],[c_259,c_2262]) ).
cnf(c_2263,plain,
( op1(e11,e12) = e12
| e10 = e12
| op1(e11,e10) = e12 ),
inference(paramod,[status(thm)],[c_2004,c_1972]) ).
cnf(c_2264,plain,
( e11 = e12
| e10 = e12
| op1(e11,e10) = e12 ),
inference(paramod,[status(thm)],[c_2077,c_2263]) ).
cnf(c_2265,plain,
( e11 = e12
| e12 = e10
| op1(e11,e10) = e12 ),
inference(copy,[status(thm)],[c_2264]) ).
cnf(c_2266,plain,
( e12 = e11
| e12 = e10
| op1(e11,e10) = e12 ),
inference(copy,[status(thm)],[c_2265]) ).
cnf(c_2267,plain,
( e12 = e11
| op1(e11,e10) = e12 ),
inference(resolve,[status(thm)],[c_260,c_2266]) ).
cnf(c_2079,plain,
op1(e11,e10) = e12,
inference(resolve,[status(thm)],[c_263,c_2267]) ).
cnf(c_2082,plain,
op1(e12,e11) != e10,
inference(paramod,[status(thm)],[c_2004,c_128]) ).
cnf(c_2268,plain,
( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e11) = e13
| e12 = e13 ),
inference(paramod,[status(thm)],[c_2079,c_49]) ).
cnf(c_2269,plain,
( op1(e11,e13) = e13
| op1(e11,e12) = e13
| e10 = e13
| e12 = e13 ),
inference(paramod,[status(thm)],[c_2004,c_2268]) ).
cnf(c_2270,plain,
( op1(e11,e13) = e13
| e11 = e13
| e10 = e13
| e12 = e13 ),
inference(paramod,[status(thm)],[c_2077,c_2269]) ).
cnf(c_2271,plain,
( op1(e11,e13) = e13
| e11 = e13
| e10 = e13 ),
inference(resolve,[status(thm)],[c_267,c_2270]) ).
cnf(c_2272,plain,
( op1(e11,e13) = e13
| e11 = e13 ),
inference(resolve,[status(thm)],[c_262,c_2271]) ).
cnf(c_2084,plain,
op1(e11,e13) = e13,
inference(resolve,[status(thm)],[c_265,c_2272]) ).
cnf(c_2085,plain,
op2(e23,e20) = e23,
inference(resolve,[status(thm)],[c_2026,c_1979]) ).
cnf(c_2273,plain,
( op2(e23,e21) = e21
| e23 = e21 ),
inference(paramod,[status(thm)],[c_2085,c_1822]) ).
cnf(c_2274,plain,
( op2(e23,e21) = e21
| e21 = e23 ),
inference(copy,[status(thm)],[c_2273]) ).
cnf(c_2086,plain,
op2(e23,e21) = e21,
inference(resolve,[status(thm)],[c_274,c_2274]) ).
cnf(c_2090,plain,
op2(e22,e21) != e23,
inference(paramod,[status(thm)],[c_2029,c_1865]) ).
cnf(c_2093,plain,
op2(e22,e22) = e23,
inference(paramod,[status(thm)],[c_2029,c_396]) ).
cnf(c_2275,plain,
( op2(e20,e22) = e23
| h1(e10) = e23 ),
inference(paramod,[status(thm)],[c_2030,c_2024]) ).
cnf(c_2276,plain,
( e22 = e23
| h1(e10) = e23 ),
inference(paramod,[status(thm)],[c_2055,c_2275]) ).
cnf(c_2095,plain,
h1(e10) = e23,
inference(resolve,[status(thm)],[c_276,c_2276]) ).
cnf(c_2277,plain,
( op2(e22,e20) = e20
| h1(e11) = e20 ),
inference(paramod,[status(thm)],[c_2031,c_1986]) ).
cnf(c_2278,plain,
( op2(e22,e20) = e20
| e22 = e20 ),
inference(paramod,[status(thm)],[c_2046,c_2277]) ).
cnf(c_2096,plain,
op2(e22,e20) = e20,
inference(resolve,[status(thm)],[c_269,c_2278]) ).
cnf(c_2279,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22 ),
inference(resolve,[status(thm)],[c_2051,c_1991]) ).
cnf(c_2099,plain,
op2(e22,e21) = e22,
inference(resolve,[status(thm)],[c_2090,c_2279]) ).
cnf(c_2280,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(e22,h2(e10)) != h2(e11) ),
inference(paramod,[status(thm)],[c_2052,c_2043]) ).
cnf(c_2281,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(e22,e22) != h2(e11) ),
inference(paramod,[status(thm)],[c_2052,c_2280]) ).
cnf(c_2282,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| e23 != h2(e11) ),
inference(paramod,[status(thm)],[c_2093,c_2281]) ).
cnf(c_2283,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| e23 != h1(e10) ),
inference(paramod,[status(thm)],[c_2053,c_2282]) ).
cnf(c_2284,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2095,c_2283]) ).
cnf(c_2285,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(e22,h2(e11)) != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2052,c_2284]) ).
cnf(c_2286,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(e22,h1(e10)) != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2053,c_2285]) ).
cnf(c_2287,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(e22,e23) != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2095,c_2286]) ).
cnf(c_2288,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_1976,c_2287]) ).
cnf(c_2289,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != op2(e22,e20)
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2052,c_2288]) ).
cnf(c_2290,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e21) != h2(e10)
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2096,c_2289]) ).
cnf(c_2291,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(e22,e21) != h2(e10)
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2052,c_2290]) ).
cnf(c_2292,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| e22 != h2(e10)
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2099,c_2291]) ).
cnf(c_2293,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2052,c_2292]) ).
cnf(c_2294,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(h1(e10),h2(e10)) != h2(op1(e11,e10))
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2053,c_2293]) ).
cnf(c_2295,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(e23,h2(e10)) != h2(op1(e11,e10))
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2095,c_2294]) ).
cnf(c_2296,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| op2(e23,e22) != h2(op1(e11,e10))
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2052,c_2295]) ).
cnf(c_2297,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| e20 != h2(op1(e11,e10))
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_1977,c_2296]) ).
cnf(c_2298,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| e20 != h2(e12)
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2079,c_2297]) ).
cnf(c_2299,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e10)
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_1984,c_2298]) ).
cnf(c_2300,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h1(e10),h2(e11)) != h2(e10)
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2053,c_2299]) ).
cnf(c_2301,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(e23,h2(e11)) != h2(e10)
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2095,c_2300]) ).
cnf(c_2302,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(e23,h1(e10)) != h2(e10)
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2053,c_2301]) ).
cnf(c_2303,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(e23,e23) != h2(e10)
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2095,c_2302]) ).
cnf(c_2304,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| e22 != h2(e10)
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_375,c_2303]) ).
cnf(c_2305,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2052,c_2304]) ).
cnf(c_2306,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h2(e11) != op2(h2(e11),e20)
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2077,c_2305]) ).
cnf(c_2307,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| h1(e10) != op2(h2(e11),e20)
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2053,c_2306]) ).
cnf(c_2308,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| e23 != op2(h2(e11),e20)
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2095,c_2307]) ).
cnf(c_2309,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| e23 != op2(h1(e10),e20)
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2053,c_2308]) ).
cnf(c_2310,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| e23 != op2(e23,e20)
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2095,c_2309]) ).
cnf(c_2311,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e21)
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2085,c_2310]) ).
cnf(c_2312,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(e13) != op2(h2(e11),e21)
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2084,c_2311]) ).
cnf(c_2313,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| e21 != op2(h2(e11),e21)
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_383,c_2312]) ).
cnf(c_2314,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| e21 != op2(h1(e10),e21)
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2053,c_2313]) ).
cnf(c_2315,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| e21 != op2(e23,e21)
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2095,c_2314]) ).
cnf(c_2316,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2086,c_2315]) ).
cnf(c_2317,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,e22)
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2052,c_2316]) ).
cnf(c_2318,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2055,c_2317]) ).
cnf(c_2319,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,h1(e10))
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2053,c_2318]) ).
cnf(c_2320,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != op2(e20,e23)
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2095,c_2319]) ).
cnf(c_2321,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(op1(e12,e12)) != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_1988,c_2320]) ).
cnf(c_2322,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| h2(e13) != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2070,c_2321]) ).
cnf(c_2323,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,h2(e10))
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_383,c_2322]) ).
cnf(c_2324,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != op2(e21,e22)
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2052,c_2323]) ).
cnf(c_2325,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(op1(e13,e11)) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_1993,c_2324]) ).
cnf(c_2326,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e11) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2078,c_2325]) ).
cnf(c_2327,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h1(e10) != op2(e21,h2(e11))
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2053,c_2326]) ).
cnf(c_2328,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e23 != op2(e21,h2(e11))
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2095,c_2327]) ).
cnf(c_2329,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e23 != op2(e21,h1(e10))
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2053,c_2328]) ).
cnf(c_2330,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e23 != op2(e21,e23)
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2095,c_2329]) ).
cnf(c_2331,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e23 != e23
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2048,c_2330]) ).
cnf(c_2332,negated_conjecture,
( h2(e11) != e23
| e22 != e22
| e23 != e23
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2052,c_2331]) ).
cnf(c_2333,negated_conjecture,
( h1(e10) != e23
| e22 != e22
| e23 != e23
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2053,c_2332]) ).
cnf(c_2334,negated_conjecture,
( e23 != e23
| e22 != e22
| e23 != e23
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| e21 != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2095,c_2333]) ).
cnf(c_2335,negated_conjecture,
( e23 != e23
| e22 != e22
| e23 != e23
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| h2(op1(e10,e11)) != e21
| e23 != e23 ),
inference(copy,[status(thm)],[c_2334]) ).
cnf(c_2336,negated_conjecture,
( e23 != e23
| e22 != e22
| e23 != e23
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e10,e12)) != e20
| h2(op1(e10,e11)) != e21 ),
inference(copy,[status(thm)],[c_2335]) ).
cnf(c_2337,negated_conjecture,
( e23 != e23
| e22 != e22
| e23 != e23
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| e20 != e20
| h2(op1(e10,e12)) != e20
| h2(op1(e10,e11)) != e21 ),
inference(copy,[status(thm)],[c_2336]) ).
cnf(c_2338,negated_conjecture,
( e23 != e23
| e22 != e22
| e23 != e23
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e22 != e22
| h2(op1(e10,e12)) != e20
| h2(op1(e10,e11)) != e21 ),
inference(copy,[status(thm)],[c_2337]) ).
cnf(c_2339,negated_conjecture,
( e23 != e23
| e22 != e22
| e23 != e23
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| h2(op1(e10,e12)) != e20
| h2(op1(e10,e11)) != e21 ),
inference(copy,[status(thm)],[c_2338]) ).
cnf(c_2340,negated_conjecture,
( e23 != e23
| e22 != e22
| e23 != e23
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e21 != e21
| h2(op1(e10,e12)) != e20
| h2(op1(e10,e11)) != e21 ),
inference(copy,[status(thm)],[c_2339]) ).
cnf(c_2341,negated_conjecture,
( e23 != e23
| e22 != e22
| e23 != e23
| h2(op1(e13,e10)) != e21
| e21 != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| h2(op1(e10,e12)) != e20
| h2(op1(e10,e11)) != e21 ),
inference(copy,[status(thm)],[c_2340]) ).
cnf(c_2342,negated_conjecture,
( e23 != e23
| e22 != e22
| e23 != e23
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| h2(op1(e10,e12)) != e20
| h2(op1(e10,e11)) != e21 ),
inference(copy,[status(thm)],[c_2341]) ).
cnf(c_2343,negated_conjecture,
( e23 != e23
| e22 != e22
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| h2(op1(e10,e12)) != e20
| h2(op1(e10,e11)) != e21 ),
inference(copy,[status(thm)],[c_2342]) ).
cnf(c_2344,negated_conjecture,
( e23 != e23
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| h2(op1(e10,e12)) != e20
| h2(op1(e10,e11)) != e21 ),
inference(copy,[status(thm)],[c_2343]) ).
cnf(c_2100,negated_conjecture,
( h2(op1(e13,e10)) != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| h2(op1(e10,e12)) != e20
| h2(op1(e10,e11)) != e21 ),
inference(copy,[status(thm)],[c_2344]) ).
cnf(c_2345,plain,
( op1(e12,e12) = e12
| e11 = e12
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_2077,c_1966]) ).
cnf(c_2346,plain,
( e13 = e12
| e11 = e12
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_2070,c_2345]) ).
cnf(c_2347,plain,
( e13 = e12
| e12 = e11
| op1(e10,e12) = e12 ),
inference(copy,[status(thm)],[c_2346]) ).
cnf(c_2348,plain,
( e12 = e13
| e12 = e11
| op1(e10,e12) = e12 ),
inference(copy,[status(thm)],[c_2347]) ).
cnf(c_2349,plain,
( e12 = e13
| op1(e10,e12) = e12 ),
inference(resolve,[status(thm)],[c_263,c_2348]) ).
cnf(c_2102,plain,
op1(e10,e12) = e12,
inference(resolve,[status(thm)],[c_267,c_2349]) ).
cnf(c_2350,plain,
e13 != op1(e12,e11),
inference(paramod,[status(thm)],[c_2070,c_173]) ).
cnf(c_2104,plain,
op1(e12,e11) != e13,
inference(copy,[status(thm)],[c_2350]) ).
cnf(c_2106,plain,
op1(e13,e10) = e13,
inference(resolve,[status(thm)],[c_2073,c_1971]) ).
cnf(c_2351,plain,
( op1(e12,e10) = e10
| e12 = e10 ),
inference(paramod,[status(thm)],[c_2079,c_2002]) ).
cnf(c_2107,plain,
op1(e12,e10) = e10,
inference(resolve,[status(thm)],[c_260,c_2351]) ).
cnf(c_2352,plain,
( op1(e12,e11) = e13
| op1(e12,e11) = e12 ),
inference(resolve,[status(thm)],[c_2082,c_1998]) ).
cnf(c_2108,plain,
op1(e12,e11) = e12,
inference(resolve,[status(thm)],[c_2104,c_2352]) ).
cnf(c_2353,negated_conjecture,
( h2(op1(e13,e10)) != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| h2(e12) != e20
| h2(op1(e10,e11)) != e21 ),
inference(paramod,[status(thm)],[c_2102,c_2100]) ).
cnf(c_2354,negated_conjecture,
( h2(op1(e13,e10)) != e21
| h2(op1(e12,e11)) != e20
| h2(op1(e12,e10)) != e22
| e20 != e20
| h2(op1(e10,e11)) != e21 ),
inference(paramod,[status(thm)],[c_1984,c_2353]) ).
cnf(c_2355,negated_conjecture,
( h2(op1(e13,e10)) != e21
| h2(op1(e12,e11)) != e20
| h2(e10) != e22
| e20 != e20
| h2(op1(e10,e11)) != e21 ),
inference(paramod,[status(thm)],[c_2107,c_2354]) ).
cnf(c_2356,negated_conjecture,
( h2(op1(e13,e10)) != e21
| h2(op1(e12,e11)) != e20
| e22 != e22
| e20 != e20
| h2(op1(e10,e11)) != e21 ),
inference(paramod,[status(thm)],[c_2052,c_2355]) ).
cnf(c_2357,negated_conjecture,
( h2(op1(e13,e10)) != e21
| h2(e12) != e20
| e22 != e22
| e20 != e20
| h2(op1(e10,e11)) != e21 ),
inference(paramod,[status(thm)],[c_2108,c_2356]) ).
cnf(c_2358,negated_conjecture,
( h2(op1(e13,e10)) != e21
| e20 != e20
| e22 != e22
| e20 != e20
| h2(op1(e10,e11)) != e21 ),
inference(paramod,[status(thm)],[c_1984,c_2357]) ).
cnf(c_2359,negated_conjecture,
( h2(e13) != e21
| e20 != e20
| e22 != e22
| e20 != e20
| h2(op1(e10,e11)) != e21 ),
inference(paramod,[status(thm)],[c_2106,c_2358]) ).
cnf(c_2360,negated_conjecture,
( e21 != e21
| e20 != e20
| e22 != e22
| e20 != e20
| h2(op1(e10,e11)) != e21 ),
inference(paramod,[status(thm)],[c_383,c_2359]) ).
cnf(c_2361,negated_conjecture,
( e21 != e21
| e20 != e20
| e22 != e22
| h2(op1(e10,e11)) != e21 ),
inference(copy,[status(thm)],[c_2360]) ).
cnf(c_2362,negated_conjecture,
( e21 != e21
| e20 != e20
| h2(op1(e10,e11)) != e21 ),
inference(copy,[status(thm)],[c_2361]) ).
cnf(c_2363,negated_conjecture,
( e21 != e21
| h2(op1(e10,e11)) != e21 ),
inference(copy,[status(thm)],[c_2362]) ).
cnf(c_2114,negated_conjecture,
h2(op1(e10,e11)) != e21,
inference(copy,[status(thm)],[c_2363]) ).
cnf(c_2364,plain,
( e12 = e13
| op1(e10,e11) = e13 ),
inference(paramod,[status(thm)],[c_2102,c_2075]) ).
cnf(c_2115,plain,
op1(e10,e11) = e13,
inference(resolve,[status(thm)],[c_267,c_2364]) ).
cnf(c_2365,negated_conjecture,
h2(e13) != e21,
inference(paramod,[status(thm)],[c_2115,c_2114]) ).
cnf(c_2366,negated_conjecture,
e21 != e21,
inference(paramod,[status(thm)],[c_383,c_2365]) ).
cnf(c_2116,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_2366]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG117+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.38 % Computer : n011.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sat Sep 26 21:11:15 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.38 % Process 1551362 was started by sandbox2 on n011,
% 0.10/0.38 % Sat Sep 26 21:11:15 2026
% 0.10/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 11.15/11.45
% 11.15/11.45 % From the command line: assign(max_seconds, 300).
% 15.81/12.09
% 15.81/12.09 % SZS status Theorem for theBenchmark
% 15.81/12.09
% 15.81/12.09 % Proof 1 at 0.55 (+ 0.04) seconds.
% 15.81/12.09 % Length of proof is 235.
% 15.81/12.09 % Level of proof is 11.
% 15.81/12.09 % Maximum clause weight is 171.000.
% 15.81/12.09 % Given clauses 0.
% 15.81/12.09
% 15.81/12.09 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------