%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG111+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:32 AM UTC 2026
% Result : Theorem 11.37s 12.01s
% Output : CNFRefutation 11.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 123
% Number of leaves : 17
% Syntax : Number of formulae : 453 ( 154 unt; 0 def)
% Number of atoms : 3348 (3347 equ)
% Maximal formula atoms : 128 ( 7 avg)
% Number of connectives : 5061 (2166 ~;2405 |; 490 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 66 ( 7 avg)
% Maximal term depth : 4 ( 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,e12) != e13
| op1(e13,e13) != e13 )
& ( op1(e11,e11) != e13
| op1(e13,e13) != e13 )
& ( op1(e10,e10) != e13
| op1(e13,e13) != e13 )
& ( op1(e13,e13) != e12
| op1(e13,e12) != e13 )
& ( op1(e12,e12) != e12
| op1(e13,e12) != e13 )
& ( op1(e11,e11) != e12
| op1(e13,e12) != e13 )
& ( op1(e10,e10) != e12
| op1(e13,e12) != e13 )
& ( op1(e13,e13) != e11
| op1(e13,e11) != e13 )
& ( op1(e12,e12) != e11
| op1(e13,e11) != e13 )
& ( op1(e11,e11) != e11
| op1(e13,e11) != e13 )
& ( op1(e10,e10) != e11
| op1(e13,e11) != e13 )
& ( op1(e13,e13) != e10
| op1(e13,e10) != e13 )
& ( op1(e12,e12) != e10
| op1(e13,e10) != e13 )
& ( op1(e11,e11) != e10
| op1(e13,e10) != e13 )
& ( op1(e10,e10) != e10
| op1(e13,e10) != e13 )
& ( op1(e13,e13) != e13
| op1(e12,e13) != e12 )
& ( op1(e12,e12) != e13
| op1(e12,e13) != e12 )
& ( op1(e11,e11) != e13
| op1(e12,e13) != e12 )
& ( op1(e10,e10) != e13
| op1(e12,e13) != e12 )
& ( op1(e13,e13) != e12
| op1(e12,e12) != e12 )
& ( op1(e12,e12) != e12
| op1(e12,e12) != e12 )
& ( op1(e11,e11) != e12
| op1(e12,e12) != e12 )
& ( op1(e10,e10) != e12
| op1(e12,e12) != e12 )
& ( op1(e13,e13) != e11
| op1(e12,e11) != e12 )
& ( op1(e12,e12) != e11
| op1(e12,e11) != e12 )
& ( op1(e11,e11) != e11
| op1(e12,e11) != e12 )
& ( op1(e10,e10) != e11
| op1(e12,e11) != e12 )
& ( op1(e13,e13) != e10
| op1(e12,e10) != e12 )
& ( op1(e12,e12) != e10
| op1(e12,e10) != e12 )
& ( op1(e11,e11) != e10
| op1(e12,e10) != e12 )
& ( op1(e10,e10) != e10
| op1(e12,e10) != e12 )
& ( op1(e13,e13) != e13
| op1(e11,e13) != e11 )
& ( op1(e12,e12) != e13
| op1(e11,e13) != e11 )
& ( op1(e11,e11) != e13
| op1(e11,e13) != e11 )
& ( op1(e10,e10) != e13
| op1(e11,e13) != e11 )
& ( op1(e13,e13) != e12
| op1(e11,e12) != e11 )
& ( op1(e12,e12) != e12
| op1(e11,e12) != e11 )
& ( op1(e11,e11) != e12
| op1(e11,e12) != e11 )
& ( op1(e10,e10) != e12
| op1(e11,e12) != e11 )
& ( op1(e13,e13) != e11
| op1(e11,e11) != e11 )
& ( op1(e12,e12) != e11
| op1(e11,e11) != e11 )
& ( op1(e11,e11) != e11
| op1(e11,e11) != e11 )
& ( op1(e10,e10) != e11
| op1(e11,e11) != e11 )
& ( op1(e13,e13) != e10
| op1(e11,e10) != e11 )
& ( op1(e12,e12) != e10
| op1(e11,e10) != e11 )
& ( op1(e11,e11) != e10
| op1(e11,e10) != e11 )
& ( op1(e10,e10) != e10
| op1(e11,e10) != e11 )
& ( op1(e13,e13) != e13
| op1(e10,e13) != e10 )
& ( op1(e12,e12) != e13
| op1(e10,e13) != e10 )
& ( op1(e11,e11) != e13
| op1(e10,e13) != e10 )
& ( op1(e10,e10) != e13
| op1(e10,e13) != e10 )
& ( op1(e13,e13) != e12
| op1(e10,e12) != e10 )
& ( op1(e12,e12) != e12
| op1(e10,e12) != e10 )
& ( op1(e11,e11) != e12
| op1(e10,e12) != e10 )
& ( op1(e10,e10) != e12
| op1(e10,e12) != e10 )
& ( op1(e13,e13) != e11
| op1(e10,e11) != e10 )
& ( op1(e12,e12) != e11
| op1(e10,e11) != e10 )
& ( op1(e11,e11) != e11
| op1(e10,e11) != e10 )
& ( op1(e10,e10) != e11
| op1(e10,e11) != e10 )
& ( op1(e13,e13) != e10
| op1(e10,e10) != e10 )
& ( op1(e12,e12) != e10
| op1(e10,e10) != e10 )
& ( op1(e11,e11) != e10
| op1(e10,e10) != 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,e22) != e23
| op2(e23,e23) != e23 )
& ( op2(e21,e21) != e23
| op2(e23,e23) != e23 )
& ( op2(e20,e20) != e23
| op2(e23,e23) != e23 )
& ( op2(e23,e23) != e22
| op2(e23,e22) != e23 )
& ( op2(e22,e22) != e22
| op2(e23,e22) != e23 )
& ( op2(e21,e21) != e22
| op2(e23,e22) != e23 )
& ( op2(e20,e20) != e22
| op2(e23,e22) != e23 )
& ( op2(e23,e23) != e21
| op2(e23,e21) != e23 )
& ( op2(e22,e22) != e21
| op2(e23,e21) != e23 )
& ( op2(e21,e21) != e21
| op2(e23,e21) != e23 )
& ( op2(e20,e20) != e21
| op2(e23,e21) != e23 )
& ( op2(e23,e23) != e20
| op2(e23,e20) != e23 )
& ( op2(e22,e22) != e20
| op2(e23,e20) != e23 )
& ( op2(e21,e21) != e20
| op2(e23,e20) != e23 )
& ( op2(e20,e20) != e20
| op2(e23,e20) != e23 )
& ( op2(e23,e23) != e23
| op2(e22,e23) != e22 )
& ( op2(e22,e22) != e23
| op2(e22,e23) != e22 )
& ( op2(e21,e21) != e23
| op2(e22,e23) != e22 )
& ( op2(e20,e20) != e23
| op2(e22,e23) != e22 )
& ( op2(e23,e23) != e22
| op2(e22,e22) != e22 )
& ( op2(e22,e22) != e22
| op2(e22,e22) != e22 )
& ( op2(e21,e21) != e22
| op2(e22,e22) != e22 )
& ( op2(e20,e20) != e22
| op2(e22,e22) != e22 )
& ( op2(e23,e23) != e21
| op2(e22,e21) != e22 )
& ( op2(e22,e22) != e21
| op2(e22,e21) != e22 )
& ( op2(e21,e21) != e21
| op2(e22,e21) != e22 )
& ( op2(e20,e20) != e21
| op2(e22,e21) != e22 )
& ( op2(e23,e23) != e20
| op2(e22,e20) != e22 )
& ( op2(e22,e22) != e20
| op2(e22,e20) != e22 )
& ( op2(e21,e21) != e20
| op2(e22,e20) != e22 )
& ( op2(e20,e20) != e20
| op2(e22,e20) != e22 )
& ( op2(e23,e23) != e23
| op2(e21,e23) != e21 )
& ( op2(e22,e22) != e23
| op2(e21,e23) != e21 )
& ( op2(e21,e21) != e23
| op2(e21,e23) != e21 )
& ( op2(e20,e20) != e23
| op2(e21,e23) != e21 )
& ( op2(e23,e23) != e22
| op2(e21,e22) != e21 )
& ( op2(e22,e22) != e22
| op2(e21,e22) != e21 )
& ( op2(e21,e21) != e22
| op2(e21,e22) != e21 )
& ( op2(e20,e20) != e22
| op2(e21,e22) != e21 )
& ( op2(e23,e23) != e21
| op2(e21,e21) != e21 )
& ( op2(e22,e22) != e21
| op2(e21,e21) != e21 )
& ( op2(e21,e21) != e21
| op2(e21,e21) != e21 )
& ( op2(e20,e20) != e21
| op2(e21,e21) != e21 )
& ( op2(e23,e23) != e20
| op2(e21,e20) != e21 )
& ( op2(e22,e22) != e20
| op2(e21,e20) != e21 )
& ( op2(e21,e21) != e20
| op2(e21,e20) != e21 )
& ( op2(e20,e20) != e20
| op2(e21,e20) != e21 )
& ( op2(e23,e23) != e23
| op2(e20,e23) != e20 )
& ( op2(e22,e22) != e23
| op2(e20,e23) != e20 )
& ( op2(e21,e21) != e23
| op2(e20,e23) != e20 )
& ( op2(e20,e20) != e23
| op2(e20,e23) != e20 )
& ( op2(e23,e23) != e22
| op2(e20,e22) != e20 )
& ( op2(e22,e22) != e22
| op2(e20,e22) != e20 )
& ( op2(e21,e21) != e22
| op2(e20,e22) != e20 )
& ( op2(e20,e20) != e22
| op2(e20,e22) != e20 )
& ( op2(e23,e23) != e21
| op2(e20,e21) != e20 )
& ( op2(e22,e22) != e21
| op2(e20,e21) != e20 )
& ( op2(e21,e21) != e21
| op2(e20,e21) != e20 )
& ( op2(e20,e20) != e21
| op2(e20,e21) != e20 )
& ( op2(e23,e23) != e20
| op2(e20,e20) != e20 )
& ( op2(e22,e22) != e20
| op2(e20,e20) != e20 )
& ( op2(e21,e21) != e20
| op2(e20,e20) != e20 )
& ( op2(e20,e20) != e20
| op2(e20,e20) != e20 ) ),
file('theBenchmark.p',ax11) ).
fof(ax12,axiom,
( e12 = op1(op1(e13,op1(e13,e13)),op1(e13,e13))
& e11 = op1(e13,e13)
& e10 = op1(e13,op1(e13,e13)) ),
file('theBenchmark.p',ax12) ).
fof(ax13,axiom,
( e22 = op2(op2(e23,op2(e23,e23)),op2(e23,e23))
& e21 = op2(e23,e23)
& e20 = op2(e23,op2(e23,e23)) ),
file('theBenchmark.p',ax13) ).
fof(ax14,axiom,
( h1(e12) = op2(op2(e20,op2(e20,e20)),op2(e20,e20))
& h1(e11) = op2(e20,e20)
& h1(e10) = op2(e20,op2(e20,e20))
& h1(e13) = e20 ),
file('theBenchmark.p',ax14) ).
fof(ax15,axiom,
( h2(e12) = op2(op2(e21,op2(e21,e21)),op2(e21,e21))
& h2(e11) = op2(e21,e21)
& h2(e10) = op2(e21,op2(e21,e21))
& h2(e13) = e21 ),
file('theBenchmark.p',ax15) ).
fof(ax16,axiom,
( h3(e12) = op2(op2(e22,op2(e22,e22)),op2(e22,e22))
& h3(e11) = op2(e22,e22)
& h3(e10) = op2(e22,op2(e22,e22))
& h3(e13) = e22 ),
file('theBenchmark.p',ax16) ).
fof(ax17,axiom,
( h4(e12) = op2(op2(e23,op2(e23,e23)),op2(e23,e23))
& h4(e11) = op2(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_22,plain,
( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_24,plain,
( op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e11,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_37,plain,
( op1(e10,e13) = e11
| op1(e10,e12) = e11
| op1(e10,e11) = e11
| op1(e10,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_54,plain,
( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_55,plain,
( op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 ),
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_57,plain,
( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_60,plain,
( op1(e13,e13) = e10
| op1(e12,e13) = e10
| op1(e11,e13) = e10
| op1(e10,e13) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_64,plain,
( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_70,plain,
( op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = 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_85,plain,
( op2(e20,e23) = e21
| op2(e20,e22) = e21
| op2(e20,e21) = e21
| op2(e20,e20) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_90,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| op2(e20,e20) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_94,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| op2(e21,e21) = e21
| op2(e20,e21) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_98,plain,
( op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e21,e21) = e23
| op2(e20,e21) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_102,plain,
( op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_103,plain,
( op2(e22,e23) = e22
| op2(e22,e22) = e22
| op2(e22,e21) = e22
| op2(e22,e20) = e22 ),
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_105,plain,
( op2(e22,e23) = e23
| op2(e22,e22) = e23
| op2(e22,e21) = e23
| op2(e22,e20) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_108,plain,
( op2(e23,e23) = e20
| op2(e22,e23) = e20
| op2(e21,e23) = e20
| op2(e20,e23) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_112,plain,
( op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_122,plain,
op1(e13,e10) != op1(e12,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_123,plain,
op1(e12,e10) != op1(e13,e10),
inference(copy,[status(thm)],[c_122]) ).
cnf(c_124,plain,
op1(e11,e11) != op1(e10,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_129,plain,
op1(e13,e11) != op1(e11,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_130,plain,
op1(e11,e11) != op1(e13,e11),
inference(copy,[status(thm)],[c_129]) ).
cnf(c_144,plain,
op1(e13,e13) != op1(e10,e13),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_145,plain,
op1(e10,e13) != op1(e13,e13),
inference(copy,[status(thm)],[c_144]) ).
cnf(c_155,plain,
op1(e10,e12) != op1(e10,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_156,plain,
op1(e10,e13) != op1(e10,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_157,plain,
op1(e10,e11) != op1(e10,e13),
inference(copy,[status(thm)],[c_156]) ).
cnf(c_173,plain,
op1(e12,e12) != op1(e12,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_178,plain,
op1(e13,e11) != 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_185,plain,
op1(e13,e13) != op1(e13,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_186,plain,
op1(e13,e12) != op1(e13,e13),
inference(copy,[status(thm)],[c_185]) ).
cnf(c_216,plain,
op2(e23,e23) != op2(e20,e23),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_217,plain,
op2(e20,e23) != op2(e23,e23),
inference(copy,[status(thm)],[c_216]) ).
cnf(c_227,plain,
op2(e20,e22) != op2(e20,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_228,plain,
op2(e20,e23) != op2(e20,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_229,plain,
op2(e20,e21) != op2(e20,e23),
inference(copy,[status(thm)],[c_228]) ).
cnf(c_232,plain,
op2(e21,e21) != op2(e21,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_245,plain,
op2(e22,e22) != op2(e22,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_250,plain,
op2(e23,e21) != op2(e23,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_257,plain,
op2(e23,e23) != op2(e23,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_258,plain,
op2(e23,e22) != op2(e23,e23),
inference(copy,[status(thm)],[c_257]) ).
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(e10,e10) != e10,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_314,plain,
( op1(e11,e11) != e13
| op1(e10,e13) != e10 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_319,plain,
op1(e11,e11) != e11,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_331,plain,
( op1(e13,e13) != e11
| op1(e12,e11) != e12 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_332,plain,
op1(e12,e12) != e12,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_334,plain,
( op1(e11,e11) != e13
| op1(e12,e13) != e12 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_346,plain,
op2(e20,e20) != e20,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_354,plain,
( op2(e21,e21) != e23
| op2(e20,e23) != e20 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_359,plain,
op2(e21,e21) != e21,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_372,plain,
op2(e22,e22) != e22,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_374,plain,
( op2(e21,e21) != e23
| op2(e22,e23) != e22 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_386,plain,
op1(e13,op1(e13,e13)) = e10,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_387,plain,
op1(e13,e13) = e11,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_388,plain,
op1(op1(e13,op1(e13,e13)),op1(e13,e13)) = e12,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_2224,plain,
op1(op1(e13,e11),op1(e13,e13)) = e12,
inference(paramod,[status(thm)],[c_387,c_388]) ).
cnf(c_389,plain,
op1(op1(e13,e11),e11) = e12,
inference(paramod,[status(thm)],[c_387,c_2224]) ).
cnf(c_390,plain,
op2(e23,op2(e23,e23)) = e20,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_391,plain,
op2(e23,e23) = e21,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_392,plain,
op2(op2(e23,op2(e23,e23)),op2(e23,e23)) = e22,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_2225,plain,
op2(op2(e23,e21),op2(e23,e23)) = e22,
inference(paramod,[status(thm)],[c_391,c_392]) ).
cnf(c_393,plain,
op2(op2(e23,e21),e21) = e22,
inference(paramod,[status(thm)],[c_391,c_2225]) ).
cnf(c_397,plain,
h1(e11) = op2(e20,e20),
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_398,plain,
op2(e20,e20) = h1(e11),
inference(copy,[status(thm)],[c_397]) ).
cnf(c_401,plain,
h2(e13) = e21,
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_402,plain,
h2(e10) = op2(e21,op2(e21,e21)),
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_403,plain,
op2(e21,op2(e21,e21)) = h2(e10),
inference(copy,[status(thm)],[c_402]) ).
cnf(c_404,plain,
h2(e11) = op2(e21,e21),
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_405,plain,
op2(e21,e21) = h2(e11),
inference(copy,[status(thm)],[c_404]) ).
cnf(c_406,plain,
h2(e12) = op2(op2(e21,op2(e21,e21)),op2(e21,e21)),
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_2226,plain,
h2(e12) = op2(op2(e21,h2(e11)),op2(e21,e21)),
inference(paramod,[status(thm)],[c_405,c_406]) ).
cnf(c_2227,plain,
h2(e12) = op2(op2(e21,h2(e11)),h2(e11)),
inference(paramod,[status(thm)],[c_405,c_2226]) ).
cnf(c_407,plain,
op2(op2(e21,h2(e11)),h2(e11)) = h2(e12),
inference(copy,[status(thm)],[c_2227]) ).
cnf(c_411,plain,
h3(e11) = op2(e22,e22),
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_412,plain,
op2(e22,e22) = h3(e11),
inference(copy,[status(thm)],[c_411]) ).
cnf(c_416,plain,
h4(e10) = op2(e23,op2(e23,e23)),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_2228,plain,
h4(e10) = op2(e23,e21),
inference(paramod,[status(thm)],[c_391,c_416]) ).
cnf(c_417,plain,
op2(e23,e21) = h4(e10),
inference(copy,[status(thm)],[c_2228]) ).
cnf(c_1063,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_2229,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_401,c_1063]) ).
cnf(c_2230,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_401,c_2229]) ).
cnf(c_2231,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_401,c_2230]) ).
cnf(c_2232,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_401,c_2231]) ).
cnf(c_2233,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_401,c_2232]) ).
cnf(c_2234,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_401,c_2233]) ).
cnf(c_2235,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| h2(e11) != 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_387,c_2234]) ).
cnf(c_2236,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| h2(e11) != 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_401,c_2235]) ).
cnf(c_2237,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| h2(e11) != 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_401,c_2236]) ).
cnf(c_2238,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e13) != e21
| h2(e12) != e20
| h2(e11) != h2(e11)
| 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_405,c_2237]) ).
cnf(c_2239,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e11) != h2(e11)
| 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_401,c_2238]) ).
cnf(c_2240,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e11) != h2(e11)
| 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_2239]) ).
cnf(c_2241,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e11) != h2(e11)
| 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_2240]) ).
cnf(c_2242,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e11) != h2(e11)
| 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_2241]) ).
cnf(c_2243,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e11) != h2(e11)
| 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_2242]) ).
cnf(c_2244,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e11) != h2(e11)
| 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_2243]) ).
cnf(c_2245,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e11) != h2(e11)
| 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_2244]) ).
cnf(c_2246,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e11) != h2(e11)
| 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_2245]) ).
cnf(c_2247,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e11) != h2(e11)
| 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_2246]) ).
cnf(c_2248,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| e21 != e21
| h2(e12) != e20
| h2(e11) != h2(e11)
| 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_2247]) ).
cnf(c_2249,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_2248]) ).
cnf(c_1064,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_2249]) ).
cnf(c_1794,plain,
( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10 ),
inference(resolve,[status(thm)],[c_306,c_36]) ).
cnf(c_1795,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10 ),
inference(resolve,[status(thm)],[c_306,c_35]) ).
cnf(c_1797,plain,
( op1(e13,e11) = e11
| op1(e12,e11) = e11
| op1(e10,e11) = e11 ),
inference(resolve,[status(thm)],[c_319,c_46]) ).
cnf(c_1799,plain,
( op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e10 ),
inference(resolve,[status(thm)],[c_319,c_24]) ).
cnf(c_1800,plain,
( op1(e13,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(resolve,[status(thm)],[c_332,c_56]) ).
cnf(c_1801,plain,
( op1(e12,e13) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 ),
inference(resolve,[status(thm)],[c_332,c_55]) ).
cnf(c_1805,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| h1(e11) = e20 ),
inference(paramod,[status(thm)],[c_398,c_84]) ).
cnf(c_1806,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| h1(e11) = e20 ),
inference(paramod,[status(thm)],[c_398,c_83]) ).
cnf(c_2250,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| h2(e11) = e21
| op2(e20,e21) = e21 ),
inference(paramod,[status(thm)],[c_405,c_94]) ).
cnf(c_1808,plain,
( h4(e10) = e21
| op2(e22,e21) = e21
| h2(e11) = e21
| op2(e20,e21) = e21 ),
inference(paramod,[status(thm)],[c_417,c_2250]) ).
cnf(c_1811,plain,
( op2(e23,e22) = e22
| h3(e11) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_412,c_104]) ).
cnf(c_1812,plain,
( op2(e22,e23) = e22
| h3(e11) = e22
| op2(e22,e21) = e22
| op2(e22,e20) = e22 ),
inference(paramod,[status(thm)],[c_412,c_103]) ).
cnf(c_1816,plain,
op1(e13,e11) = e10,
inference(paramod,[status(thm)],[c_387,c_386]) ).
cnf(c_2251,plain,
( e11 != e11
| op1(e12,e11) != e12 ),
inference(paramod,[status(thm)],[c_387,c_331]) ).
cnf(c_1817,plain,
op1(e12,e11) != e12,
inference(copy,[status(thm)],[c_2251]) ).
cnf(c_1819,plain,
op1(e13,e12) != e11,
inference(paramod,[status(thm)],[c_387,c_186]) ).
cnf(c_1820,plain,
op1(e13,e10) != e11,
inference(paramod,[status(thm)],[c_387,c_181]) ).
cnf(c_1823,plain,
op1(e10,e13) != e11,
inference(paramod,[status(thm)],[c_387,c_145]) ).
cnf(c_2252,plain,
( e11 = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(paramod,[status(thm)],[c_387,c_64]) ).
cnf(c_2253,plain,
( e12 = e11
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(copy,[status(thm)],[c_2252]) ).
cnf(c_1824,plain,
( op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(resolve,[status(thm)],[c_263,c_2253]) ).
cnf(c_2254,plain,
( e11 = e10
| op1(e12,e13) = e10
| op1(e11,e13) = e10
| op1(e10,e13) = e10 ),
inference(paramod,[status(thm)],[c_387,c_60]) ).
cnf(c_1826,plain,
( op1(e12,e13) = e10
| op1(e11,e13) = e10
| op1(e10,e13) = e10 ),
inference(resolve,[status(thm)],[c_259,c_2254]) ).
cnf(c_2255,plain,
op2(e23,e21) = e20,
inference(paramod,[status(thm)],[c_391,c_390]) ).
cnf(c_1827,plain,
h4(e10) = e20,
inference(paramod,[status(thm)],[c_417,c_2255]) ).
cnf(c_1830,plain,
op2(e23,e22) != e21,
inference(paramod,[status(thm)],[c_391,c_258]) ).
cnf(c_1834,plain,
op2(e20,e23) != e21,
inference(paramod,[status(thm)],[c_391,c_217]) ).
cnf(c_2256,plain,
( e21 = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 ),
inference(paramod,[status(thm)],[c_391,c_112]) ).
cnf(c_2257,plain,
( e22 = e21
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 ),
inference(copy,[status(thm)],[c_2256]) ).
cnf(c_1835,plain,
( op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 ),
inference(resolve,[status(thm)],[c_272,c_2257]) ).
cnf(c_2258,plain,
( e21 = e20
| op2(e22,e23) = e20
| op2(e21,e23) = e20
| op2(e20,e23) = e20 ),
inference(paramod,[status(thm)],[c_391,c_108]) ).
cnf(c_1837,plain,
( op2(e22,e23) = e20
| op2(e21,e23) = e20
| op2(e20,e23) = e20 ),
inference(resolve,[status(thm)],[c_268,c_2258]) ).
cnf(c_1844,plain,
h1(e11) != e20,
inference(paramod,[status(thm)],[c_398,c_346]) ).
cnf(c_1851,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| h1(e11) = e23 ),
inference(paramod,[status(thm)],[c_398,c_90]) ).
cnf(c_2259,plain,
( op2(e20,e23) = e21
| op2(e20,e22) = e21
| op2(e20,e21) = e21
| h1(e11) = e21 ),
inference(paramod,[status(thm)],[c_398,c_85]) ).
cnf(c_1856,plain,
( op2(e20,e22) = e21
| op2(e20,e21) = e21
| h1(e11) = e21 ),
inference(resolve,[status(thm)],[c_1834,c_2259]) ).
cnf(c_1857,plain,
op2(e21,h2(e11)) = h2(e10),
inference(paramod,[status(thm)],[c_405,c_403]) ).
cnf(c_1860,plain,
( h2(e11) != e23
| op2(e22,e23) != e22 ),
inference(paramod,[status(thm)],[c_405,c_374]) ).
cnf(c_1863,plain,
h2(e11) != e21,
inference(paramod,[status(thm)],[c_405,c_359]) ).
cnf(c_1865,plain,
( h2(e11) != e23
| op2(e20,e23) != e20 ),
inference(paramod,[status(thm)],[c_405,c_354]) ).
cnf(c_2260,plain,
h2(e11) != op2(e21,e20),
inference(paramod,[status(thm)],[c_405,c_232]) ).
cnf(c_1869,plain,
op2(e21,e20) != h2(e11),
inference(copy,[status(thm)],[c_2260]) ).
cnf(c_2261,plain,
( op2(e23,e21) = e23
| op2(e22,e21) = e23
| h2(e11) = e23
| op2(e20,e21) = e23 ),
inference(paramod,[status(thm)],[c_405,c_98]) ).
cnf(c_2262,plain,
( h4(e10) = e23
| op2(e22,e21) = e23
| h2(e11) = e23
| op2(e20,e21) = e23 ),
inference(paramod,[status(thm)],[c_417,c_2261]) ).
cnf(c_2263,plain,
( e20 = e23
| op2(e22,e21) = e23
| h2(e11) = e23
| op2(e20,e21) = e23 ),
inference(paramod,[status(thm)],[c_1827,c_2262]) ).
cnf(c_1873,plain,
( op2(e22,e21) = e23
| h2(e11) = e23
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_271,c_2263]) ).
cnf(c_1881,plain,
h3(e11) != e22,
inference(paramod,[status(thm)],[c_412,c_372]) ).
cnf(c_2264,plain,
h3(e11) != op2(e22,e21),
inference(paramod,[status(thm)],[c_412,c_245]) ).
cnf(c_1886,plain,
op2(e22,e21) != h3(e11),
inference(copy,[status(thm)],[c_2264]) ).
cnf(c_1892,plain,
( op2(e22,e23) = e23
| h3(e11) = e23
| op2(e22,e21) = e23
| op2(e22,e20) = e23 ),
inference(paramod,[status(thm)],[c_412,c_105]) ).
cnf(c_2265,plain,
( op2(e23,e22) = e21
| h3(e11) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 ),
inference(paramod,[status(thm)],[c_412,c_102]) ).
cnf(c_1893,plain,
( h3(e11) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 ),
inference(resolve,[status(thm)],[c_1830,c_2265]) ).
cnf(c_2266,plain,
op2(h4(e10),e21) = e22,
inference(paramod,[status(thm)],[c_417,c_393]) ).
cnf(c_1897,plain,
op2(e20,e21) = e22,
inference(paramod,[status(thm)],[c_1827,c_2266]) ).
cnf(c_2267,plain,
h4(e10) != op2(e23,e20),
inference(paramod,[status(thm)],[c_417,c_250]) ).
cnf(c_2268,plain,
e20 != op2(e23,e20),
inference(paramod,[status(thm)],[c_1827,c_2267]) ).
cnf(c_1899,plain,
op2(e23,e20) != e20,
inference(copy,[status(thm)],[c_2268]) ).
cnf(c_2269,plain,
( e10 = e11
| op1(e12,e11) = e11
| op1(e10,e11) = e11 ),
inference(paramod,[status(thm)],[c_1816,c_1797]) ).
cnf(c_2270,plain,
( e11 = e10
| op1(e12,e11) = e11
| op1(e10,e11) = e11 ),
inference(copy,[status(thm)],[c_2269]) ).
cnf(c_1902,plain,
( op1(e12,e11) = e11
| op1(e10,e11) = e11 ),
inference(resolve,[status(thm)],[c_259,c_2270]) ).
cnf(c_2271,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(e10) != 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(paramod,[status(thm)],[c_1816,c_1064]) ).
cnf(c_2272,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(e10) != h2(e10)
| 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(paramod,[status(thm)],[c_1857,c_2271]) ).
cnf(c_1939,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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_2272]) ).
cnf(c_1977,plain,
op1(e10,e11) = e12,
inference(paramod,[status(thm)],[c_1816,c_389]) ).
cnf(c_2273,plain,
e10 != op1(e13,e10),
inference(paramod,[status(thm)],[c_1816,c_178]) ).
cnf(c_1979,plain,
op1(e13,e10) != e10,
inference(copy,[status(thm)],[c_2273]) ).
cnf(c_1981,plain,
op1(e11,e11) != e10,
inference(paramod,[status(thm)],[c_1816,c_130]) ).
cnf(c_1983,plain,
( op1(e12,e13) = e12
| op1(e12,e10) = e12 ),
inference(resolve,[status(thm)],[c_1817,c_1801]) ).
cnf(c_2274,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10
| e12 = e10 ),
inference(paramod,[status(thm)],[c_1977,c_1795]) ).
cnf(c_1985,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10 ),
inference(resolve,[status(thm)],[c_260,c_2274]) ).
cnf(c_1986,plain,
( op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(resolve,[status(thm)],[c_1819,c_54]) ).
cnf(c_2275,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11 ),
inference(resolve,[status(thm)],[c_1979,c_31]) ).
cnf(c_1989,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e12 ),
inference(resolve,[status(thm)],[c_1820,c_2275]) ).
cnf(c_2276,plain,
( op1(e10,e13) = e11
| op1(e10,e12) = e11
| e12 = e11
| op1(e10,e10) = e11 ),
inference(paramod,[status(thm)],[c_1977,c_37]) ).
cnf(c_2277,plain,
( op1(e10,e13) = e11
| op1(e10,e12) = e11
| op1(e10,e10) = e11 ),
inference(resolve,[status(thm)],[c_263,c_2276]) ).
cnf(c_1994,plain,
( op1(e10,e12) = e11
| op1(e10,e10) = e11 ),
inference(resolve,[status(thm)],[c_1823,c_2277]) ).
cnf(c_1995,plain,
( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e10 ),
inference(resolve,[status(thm)],[c_1823,c_22]) ).
cnf(c_2278,plain,
( h4(e10) = e21
| op2(e22,e21) = e21
| h2(e11) = e21
| e22 = e21 ),
inference(paramod,[status(thm)],[c_1897,c_1808]) ).
cnf(c_2279,plain,
( e20 = e21
| op2(e22,e21) = e21
| h2(e11) = e21
| e22 = e21 ),
inference(paramod,[status(thm)],[c_1827,c_2278]) ).
cnf(c_2280,plain,
( e21 = e20
| op2(e22,e21) = e21
| h2(e11) = e21
| e22 = e21 ),
inference(copy,[status(thm)],[c_2279]) ).
cnf(c_2281,plain,
( e21 = e20
| op2(e22,e21) = e21
| h2(e11) = e21 ),
inference(resolve,[status(thm)],[c_272,c_2280]) ).
cnf(c_2282,plain,
( e21 = e20
| op2(e22,e21) = e21 ),
inference(resolve,[status(thm)],[c_1863,c_2281]) ).
cnf(c_1997,plain,
op2(e22,e21) = e21,
inference(resolve,[status(thm)],[c_268,c_2282]) ).
cnf(c_1999,plain,
op2(e23,e21) = e20,
inference(paramod,[status(thm)],[c_1827,c_417]) ).
cnf(c_2283,plain,
( op2(e22,e23) = e22
| h3(e11) = e22
| e21 = e22
| op2(e22,e20) = e22 ),
inference(paramod,[status(thm)],[c_1997,c_1812]) ).
cnf(c_2284,plain,
( op2(e22,e23) = e22
| h3(e11) = e22
| e22 = e21
| op2(e22,e20) = e22 ),
inference(copy,[status(thm)],[c_2283]) ).
cnf(c_2285,plain,
( op2(e22,e23) = e22
| h3(e11) = e22
| op2(e22,e20) = e22 ),
inference(resolve,[status(thm)],[c_272,c_2284]) ).
cnf(c_2000,plain,
( op2(e22,e23) = e22
| op2(e22,e20) = e22 ),
inference(resolve,[status(thm)],[c_1881,c_2285]) ).
cnf(c_2286,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| e22 = e20
| h1(e11) = e20 ),
inference(paramod,[status(thm)],[c_1897,c_1806]) ).
cnf(c_2287,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| e22 = e20 ),
inference(resolve,[status(thm)],[c_1844,c_2286]) ).
cnf(c_2001,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20 ),
inference(resolve,[status(thm)],[c_269,c_2287]) ).
cnf(c_2007,plain,
( op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e20 ),
inference(resolve,[status(thm)],[c_1834,c_70]) ).
cnf(c_2288,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20 ),
inference(resolve,[status(thm)],[c_1844,c_1805]) ).
cnf(c_2010,plain,
( op2(e22,e20) = e20
| op2(e21,e20) = e20 ),
inference(resolve,[status(thm)],[c_1899,c_2288]) ).
cnf(c_2011,plain,
op2(h2(e10),h2(e11)) = h2(e12),
inference(paramod,[status(thm)],[c_1857,c_407]) ).
cnf(c_2015,plain,
( op2(e23,e22) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(resolve,[status(thm)],[c_1881,c_1811]) ).
cnf(c_2289,plain,
( op2(e22,e21) = e23
| h2(e11) = e23
| e22 = e23 ),
inference(paramod,[status(thm)],[c_1897,c_1873]) ).
cnf(c_2290,plain,
( e21 = e23
| h2(e11) = e23
| e22 = e23 ),
inference(paramod,[status(thm)],[c_1997,c_2289]) ).
cnf(c_2291,plain,
( e21 = e23
| h2(e11) = e23 ),
inference(resolve,[status(thm)],[c_276,c_2290]) ).
cnf(c_2016,plain,
h2(e11) = e23,
inference(resolve,[status(thm)],[c_274,c_2291]) ).
cnf(c_2292,plain,
( op2(e20,e22) = e21
| e22 = e21
| h1(e11) = e21 ),
inference(paramod,[status(thm)],[c_1897,c_1856]) ).
cnf(c_2017,plain,
( op2(e20,e22) = e21
| h1(e11) = e21 ),
inference(resolve,[status(thm)],[c_272,c_2292]) ).
cnf(c_2293,plain,
e22 != op2(e20,e23),
inference(paramod,[status(thm)],[c_1897,c_229]) ).
cnf(c_2020,plain,
op2(e20,e23) != e22,
inference(copy,[status(thm)],[c_2293]) ).
cnf(c_2021,plain,
op2(e20,e22) != e22,
inference(paramod,[status(thm)],[c_1897,c_227]) ).
cnf(c_2294,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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),e23) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2016,c_1939]) ).
cnf(c_2295,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1977,c_2294]) ).
cnf(c_2296,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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(e23,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),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2016,c_2295]) ).
cnf(c_2297,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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(e23,h2(e11)) != h2(op1(e11,e11))
| op2(e23,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),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2016,c_2296]) ).
cnf(c_2298,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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(e23,e23) != h2(op1(e11,e11))
| op2(e23,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),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2016,c_2297]) ).
cnf(c_2299,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| e21 != h2(op1(e11,e11))
| op2(e23,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),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_391,c_2298]) ).
cnf(c_2300,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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(e23,h2(e12)) != h2(op1(e11,e12))
| e21 != h2(op1(e11,e11))
| op2(e23,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),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2016,c_2299]) ).
cnf(c_2301,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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(e23,e21)
| op2(e23,h2(e12)) != h2(op1(e11,e12))
| e21 != h2(op1(e11,e11))
| op2(e23,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),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2016,c_2300]) ).
cnf(c_2302,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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)) != e20
| op2(e23,h2(e12)) != h2(op1(e11,e12))
| e21 != h2(op1(e11,e11))
| op2(e23,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),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1999,c_2301]) ).
cnf(c_2303,negated_conjecture,
( h2(e11) != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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),e23) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| op2(e23,h2(e12)) != h2(op1(e11,e12))
| e21 != h2(op1(e11,e11))
| op2(e23,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),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2016,c_2302]) ).
cnf(c_2304,negated_conjecture,
( e23 != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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),e23) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| op2(e23,h2(e12)) != h2(op1(e11,e12))
| e21 != h2(op1(e11,e11))
| op2(e23,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),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2016,c_2303]) ).
cnf(c_2305,negated_conjecture,
( e23 != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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),e23) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| op2(e23,h2(e12)) != h2(op1(e11,e12))
| e21 != h2(op1(e11,e11))
| h2(op1(e11,e10)) != op2(e23,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2304]) ).
cnf(c_2306,negated_conjecture,
( e23 != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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),e23) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| op2(e23,h2(e12)) != h2(op1(e11,e12))
| h2(op1(e11,e11)) != e21
| h2(op1(e11,e10)) != op2(e23,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2305]) ).
cnf(c_2307,negated_conjecture,
( e23 != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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),e23) != h2(op1(e12,e11))
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e11)) != e21
| h2(op1(e11,e10)) != op2(e23,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2306]) ).
cnf(c_2308,negated_conjecture,
( e23 != e23
| h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(op1(e12,e11)) != op2(h2(e12),e23)
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e11)) != e21
| h2(op1(e11,e10)) != op2(e23,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2307]) ).
cnf(c_2047,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(op1(e12,e11)) != op2(h2(e12),e23)
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e11)) != e21
| h2(op1(e11,e10)) != op2(e23,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),e23) != h2(e12)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2308]) ).
cnf(c_2309,plain,
( op1(e12,e11) = e11
| e12 = e11 ),
inference(paramod,[status(thm)],[c_1977,c_1902]) ).
cnf(c_2078,plain,
op1(e12,e11) = e11,
inference(resolve,[status(thm)],[c_263,c_2309]) ).
cnf(c_2310,plain,
e12 != op1(e10,e13),
inference(paramod,[status(thm)],[c_1977,c_157]) ).
cnf(c_2079,plain,
op1(e10,e13) != e12,
inference(copy,[status(thm)],[c_2310]) ).
cnf(c_2080,plain,
op1(e10,e12) != e12,
inference(paramod,[status(thm)],[c_1977,c_155]) ).
cnf(c_2082,plain,
op1(e11,e11) != e12,
inference(paramod,[status(thm)],[c_1977,c_124]) ).
cnf(c_2085,plain,
( op1(e12,e10) = e10
| op1(e11,e10) = e10 ),
inference(resolve,[status(thm)],[c_1979,c_1794]) ).
cnf(c_2311,plain,
( op1(e11,e11) = e13
| op1(e11,e11) = e12 ),
inference(resolve,[status(thm)],[c_1981,c_1799]) ).
cnf(c_2087,plain,
op1(e11,e11) = e13,
inference(resolve,[status(thm)],[c_2082,c_2311]) ).
cnf(c_2312,plain,
( op2(e22,e23) = e23
| h3(e11) = e23
| e21 = e23
| op2(e22,e20) = e23 ),
inference(paramod,[status(thm)],[c_1997,c_1892]) ).
cnf(c_2089,plain,
( op2(e22,e23) = e23
| h3(e11) = e23
| op2(e22,e20) = e23 ),
inference(resolve,[status(thm)],[c_274,c_2312]) ).
cnf(c_2313,plain,
e21 != h3(e11),
inference(paramod,[status(thm)],[c_1997,c_1886]) ).
cnf(c_2090,plain,
h3(e11) != e21,
inference(copy,[status(thm)],[c_2313]) ).
cnf(c_2092,plain,
op2(h2(e10),e23) = h2(e12),
inference(paramod,[status(thm)],[c_2016,c_2011]) ).
cnf(c_2094,plain,
op2(e21,e20) != e23,
inference(paramod,[status(thm)],[c_2016,c_1869]) ).
cnf(c_2314,plain,
( e23 != e23
| op2(e20,e23) != e20 ),
inference(paramod,[status(thm)],[c_2016,c_1865]) ).
cnf(c_2097,plain,
op2(e20,e23) != e20,
inference(copy,[status(thm)],[c_2314]) ).
cnf(c_2315,plain,
( e23 != e23
| op2(e22,e23) != e22 ),
inference(paramod,[status(thm)],[c_2016,c_1860]) ).
cnf(c_2098,plain,
op2(e22,e23) != e22,
inference(copy,[status(thm)],[c_2315]) ).
cnf(c_2099,plain,
op2(e21,e23) = h2(e10),
inference(paramod,[status(thm)],[c_2016,c_1857]) ).
cnf(c_2316,plain,
( op2(e20,e23) = e23
| op2(e20,e23) = e22 ),
inference(resolve,[status(thm)],[c_2097,c_2007]) ).
cnf(c_2103,plain,
op2(e20,e23) = e23,
inference(resolve,[status(thm)],[c_2020,c_2316]) ).
cnf(c_2317,plain,
( op2(e22,e23) = e22
| op2(e21,e23) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_2103,c_1835]) ).
cnf(c_2318,plain,
( op2(e22,e23) = e22
| h2(e10) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_2099,c_2317]) ).
cnf(c_2319,plain,
( op2(e22,e23) = e22
| h2(e10) = e22
| e22 = e23 ),
inference(copy,[status(thm)],[c_2318]) ).
cnf(c_2320,plain,
( op2(e22,e23) = e22
| h2(e10) = e22 ),
inference(resolve,[status(thm)],[c_276,c_2319]) ).
cnf(c_2104,plain,
h2(e10) = e22,
inference(resolve,[status(thm)],[c_2098,c_2320]) ).
cnf(c_2105,plain,
( op2(e23,e22) = e22
| op2(e21,e22) = e22 ),
inference(resolve,[status(thm)],[c_2021,c_2015]) ).
cnf(c_2321,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(op1(e12,e11)) != op2(h2(e12),e23)
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e11)) != e21
| h2(op1(e11,e10)) != op2(e23,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),e23) != h2(e12)
| op2(e22,h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2104,c_2047]) ).
cnf(c_2322,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(op1(e12,e11)) != op2(h2(e12),e23)
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e11)) != e21
| h2(op1(e11,e10)) != op2(e23,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),e23) != h2(e12)
| op2(e22,e22) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2104,c_2321]) ).
cnf(c_2323,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(op1(e12,e11)) != op2(h2(e12),e23)
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e11)) != e21
| h2(op1(e11,e10)) != op2(e23,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(h2(e10),e23) != h2(e12)
| h3(e11) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_412,c_2322]) ).
cnf(c_2324,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(op1(e12,e11)) != op2(h2(e12),e23)
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e11)) != e21
| h2(op1(e11,e10)) != op2(e23,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e12)) != h2(op1(e10,e12))
| op2(e22,e23) != h2(e12)
| h3(e11) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2104,c_2323]) ).
cnf(c_2325,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(op1(e12,e11)) != op2(h2(e12),e23)
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e11)) != e21
| h2(op1(e11,e10)) != op2(e23,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e21)
| op2(e22,h2(e12)) != h2(op1(e10,e12))
| op2(e22,e23) != h2(e12)
| h3(e11) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2104,c_2324]) ).
cnf(c_2326,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(op1(e12,e11)) != op2(h2(e12),e23)
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e11)) != e21
| h2(op1(e11,e10)) != op2(e23,h2(e10))
| h2(op1(e10,e13)) != op2(e22,e21)
| op2(e22,h2(e12)) != h2(op1(e10,e12))
| op2(e22,e23) != h2(e12)
| h3(e11) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2104,c_2325]) ).
cnf(c_2327,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(op1(e12,e11)) != op2(h2(e12),e23)
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e11)) != e21
| h2(op1(e11,e10)) != op2(e23,h2(e10))
| h2(op1(e10,e13)) != e21
| op2(e22,h2(e12)) != h2(op1(e10,e12))
| op2(e22,e23) != h2(e12)
| h3(e11) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1997,c_2326]) ).
cnf(c_2328,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(op1(e12,e11)) != op2(h2(e12),e23)
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e11)) != e21
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| op2(e22,h2(e12)) != h2(op1(e10,e12))
| op2(e22,e23) != h2(e12)
| h3(e11) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2104,c_2327]) ).
cnf(c_2329,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(op1(e12,e11)) != op2(h2(e12),e23)
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(e13) != e21
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| op2(e22,h2(e12)) != h2(op1(e10,e12))
| op2(e22,e23) != h2(e12)
| h3(e11) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2087,c_2328]) ).
cnf(c_2330,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(op1(e12,e11)) != op2(h2(e12),e23)
| op2(h2(e12),h2(e10)) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| e21 != e21
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| op2(e22,h2(e12)) != h2(op1(e10,e12))
| op2(e22,e23) != h2(e12)
| h3(e11) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_401,c_2329]) ).
cnf(c_2331,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(op1(e12,e11)) != op2(h2(e12),e23)
| op2(h2(e12),e22) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| e21 != e21
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| op2(e22,h2(e12)) != h2(op1(e10,e12))
| op2(e22,e23) != h2(e12)
| h3(e11) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2104,c_2330]) ).
cnf(c_2332,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| h2(e11) != op2(h2(e12),e23)
| op2(h2(e12),e22) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| e21 != e21
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| op2(e22,h2(e12)) != h2(op1(e10,e12))
| op2(e22,e23) != h2(e12)
| h3(e11) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2078,c_2331]) ).
cnf(c_2333,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| 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))
| e23 != op2(h2(e12),e23)
| op2(h2(e12),e22) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| e21 != e21
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| op2(e22,h2(e12)) != h2(op1(e10,e12))
| op2(e22,e23) != h2(e12)
| h3(e11) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2016,c_2332]) ).
cnf(c_2334,negated_conjecture,
( h2(e10) != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| e23 != op2(h2(e12),e23)
| op2(h2(e12),e22) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| e21 != e21
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| op2(e22,h2(e12)) != h2(op1(e10,e12))
| op2(e22,e23) != h2(e12)
| h3(e11) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2104,c_2333]) ).
cnf(c_2335,negated_conjecture,
( e22 != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| e23 != op2(h2(e12),e23)
| op2(h2(e12),e22) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| e21 != e21
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| op2(e22,h2(e12)) != h2(op1(e10,e12))
| op2(e22,e23) != h2(e12)
| h3(e11) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_2104,c_2334]) ).
cnf(c_2336,negated_conjecture,
( e22 != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| e23 != op2(h2(e12),e23)
| op2(h2(e12),e22) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| e21 != e21
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| op2(e22,h2(e12)) != h2(op1(e10,e12))
| op2(e22,e23) != h2(e12)
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2335]) ).
cnf(c_2337,negated_conjecture,
( e22 != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| e23 != op2(h2(e12),e23)
| op2(h2(e12),e22) != h2(op1(e12,e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| e21 != e21
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| h2(op1(e10,e12)) != op2(e22,h2(e12))
| op2(e22,e23) != h2(e12)
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2336]) ).
cnf(c_2338,negated_conjecture,
( e22 != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| e23 != op2(h2(e12),e23)
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| e21 != e21
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| h2(op1(e10,e12)) != op2(e22,h2(e12))
| op2(e22,e23) != h2(e12)
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2337]) ).
cnf(c_2339,negated_conjecture,
( e22 != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| e21 != e21
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| h2(op1(e10,e12)) != op2(e22,h2(e12))
| op2(e22,e23) != h2(e12)
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2338]) ).
cnf(c_2340,negated_conjecture,
( e22 != e22
| h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| h2(op1(e10,e12)) != op2(e22,h2(e12))
| op2(e22,e23) != h2(e12)
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2339]) ).
cnf(c_2127,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| h2(op1(e10,e12)) != op2(e22,h2(e12))
| op2(e22,e23) != h2(e12)
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2340]) ).
cnf(c_2146,plain,
op1(e12,e12) != e11,
inference(paramod,[status(thm)],[c_2078,c_173]) ).
cnf(c_2341,plain,
( op1(e12,e13) = e13
| op1(e12,e12) = e13
| e11 = e13
| op1(e12,e10) = e13 ),
inference(paramod,[status(thm)],[c_2078,c_57]) ).
cnf(c_2148,plain,
( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e10) = e13 ),
inference(resolve,[status(thm)],[c_265,c_2341]) ).
cnf(c_2149,plain,
( op1(e10,e13) = e13
| op1(e10,e13) = e10 ),
inference(resolve,[status(thm)],[c_2079,c_1995]) ).
cnf(c_2150,plain,
( op1(e12,e13) = e12
| op1(e11,e13) = e12 ),
inference(resolve,[status(thm)],[c_2079,c_1824]) ).
cnf(c_2151,plain,
( op1(e13,e12) = e12
| op1(e11,e12) = e12 ),
inference(resolve,[status(thm)],[c_2080,c_1800]) ).
cnf(c_2342,plain,
( e13 != e13
| op1(e12,e13) != e12 ),
inference(paramod,[status(thm)],[c_2087,c_334]) ).
cnf(c_2156,plain,
op1(e12,e13) != e12,
inference(copy,[status(thm)],[c_2342]) ).
cnf(c_2343,plain,
( e13 != e13
| op1(e10,e13) != e10 ),
inference(paramod,[status(thm)],[c_2087,c_314]) ).
cnf(c_2157,plain,
op1(e10,e13) != e10,
inference(copy,[status(thm)],[c_2343]) ).
cnf(c_2162,plain,
( op2(e21,e22) = e21
| op2(e20,e22) = e21 ),
inference(resolve,[status(thm)],[c_2090,c_1893]) ).
cnf(c_2165,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| h1(e11) = e23 ),
inference(resolve,[status(thm)],[c_2094,c_1851]) ).
cnf(c_2344,plain,
( e23 = e20
| op2(e20,e22) = e20 ),
inference(paramod,[status(thm)],[c_2103,c_2001]) ).
cnf(c_2345,plain,
( e20 = e23
| op2(e20,e22) = e20 ),
inference(copy,[status(thm)],[c_2344]) ).
cnf(c_2169,plain,
op2(e20,e22) = e20,
inference(resolve,[status(thm)],[c_271,c_2345]) ).
cnf(c_2346,plain,
( op2(e22,e23) = e20
| op2(e21,e23) = e20
| e23 = e20 ),
inference(paramod,[status(thm)],[c_2103,c_1837]) ).
cnf(c_2347,plain,
( op2(e22,e23) = e20
| h2(e10) = e20
| e23 = e20 ),
inference(paramod,[status(thm)],[c_2099,c_2346]) ).
cnf(c_2348,plain,
( op2(e22,e23) = e20
| e22 = e20
| e23 = e20 ),
inference(paramod,[status(thm)],[c_2104,c_2347]) ).
cnf(c_2349,plain,
( op2(e22,e23) = e20
| e22 = e20
| e20 = e23 ),
inference(copy,[status(thm)],[c_2348]) ).
cnf(c_2350,plain,
( op2(e22,e23) = e20
| e22 = e20 ),
inference(resolve,[status(thm)],[c_271,c_2349]) ).
cnf(c_2170,plain,
op2(e22,e23) = e20,
inference(resolve,[status(thm)],[c_269,c_2350]) ).
cnf(c_2351,plain,
( e20 = e22
| op2(e22,e20) = e22 ),
inference(paramod,[status(thm)],[c_2170,c_2000]) ).
cnf(c_2352,plain,
( e22 = e20
| op2(e22,e20) = e22 ),
inference(copy,[status(thm)],[c_2351]) ).
cnf(c_2171,plain,
op2(e22,e20) = e22,
inference(resolve,[status(thm)],[c_269,c_2352]) ).
cnf(c_2353,plain,
op2(e22,e23) = h2(e12),
inference(paramod,[status(thm)],[c_2104,c_2092]) ).
cnf(c_2354,plain,
e20 = h2(e12),
inference(paramod,[status(thm)],[c_2170,c_2353]) ).
cnf(c_2177,plain,
h2(e12) = e20,
inference(copy,[status(thm)],[c_2354]) ).
cnf(c_2178,plain,
( op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(resolve,[status(thm)],[c_2146,c_1986]) ).
cnf(c_2182,plain,
op1(e11,e13) = e12,
inference(resolve,[status(thm)],[c_2156,c_2150]) ).
cnf(c_2184,plain,
op1(e12,e10) = e12,
inference(resolve,[status(thm)],[c_2156,c_1983]) ).
cnf(c_2185,plain,
op1(e10,e13) = e13,
inference(resolve,[status(thm)],[c_2157,c_2149]) ).
cnf(c_2355,plain,
( e13 = e10
| op1(e10,e12) = e10 ),
inference(paramod,[status(thm)],[c_2185,c_1985]) ).
cnf(c_2356,plain,
( e10 = e13
| op1(e10,e12) = e10 ),
inference(copy,[status(thm)],[c_2355]) ).
cnf(c_2186,plain,
op1(e10,e12) = e10,
inference(resolve,[status(thm)],[c_262,c_2356]) ).
cnf(c_2357,plain,
( op1(e12,e13) = e10
| op1(e11,e13) = e10
| e13 = e10 ),
inference(paramod,[status(thm)],[c_2185,c_1826]) ).
cnf(c_2358,plain,
( op1(e12,e13) = e10
| e12 = e10
| e13 = e10 ),
inference(paramod,[status(thm)],[c_2182,c_2357]) ).
cnf(c_2359,plain,
( op1(e12,e13) = e10
| e12 = e10
| e10 = e13 ),
inference(copy,[status(thm)],[c_2358]) ).
cnf(c_2360,plain,
( op1(e12,e13) = e10
| e12 = e10 ),
inference(resolve,[status(thm)],[c_262,c_2359]) ).
cnf(c_2187,plain,
op1(e12,e13) = e10,
inference(resolve,[status(thm)],[c_260,c_2360]) ).
cnf(c_2361,plain,
( op2(e21,e22) = e21
| e20 = e21 ),
inference(paramod,[status(thm)],[c_2169,c_2162]) ).
cnf(c_2362,plain,
( op2(e21,e22) = e21
| e21 = e20 ),
inference(copy,[status(thm)],[c_2361]) ).
cnf(c_2193,plain,
op2(e21,e22) = e21,
inference(resolve,[status(thm)],[c_268,c_2362]) ).
cnf(c_2363,plain,
( e20 = e21
| h1(e11) = e21 ),
inference(paramod,[status(thm)],[c_2169,c_2017]) ).
cnf(c_2364,plain,
( e21 = e20
| h1(e11) = e21 ),
inference(copy,[status(thm)],[c_2363]) ).
cnf(c_2195,plain,
h1(e11) = e21,
inference(resolve,[status(thm)],[c_268,c_2364]) ).
cnf(c_2365,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| h2(op1(e10,e12)) != op2(e22,h2(e12))
| e20 != h2(e12)
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2170,c_2127]) ).
cnf(c_2366,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| h2(op1(e10,e12)) != op2(e22,h2(e12))
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2177,c_2365]) ).
cnf(c_2367,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| h2(e10) != op2(e22,h2(e12))
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2186,c_2366]) ).
cnf(c_2368,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| e22 != op2(e22,h2(e12))
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2104,c_2367]) ).
cnf(c_2369,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| e22 != op2(e22,e20)
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2177,c_2368]) ).
cnf(c_2370,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e13)) != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2171,c_2369]) ).
cnf(c_2371,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(e13) != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2185,c_2370]) ).
cnf(c_2372,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,h2(e12))
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_401,c_2371]) ).
cnf(c_2373,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2177,c_2372]) ).
cnf(c_2374,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| h2(e12) != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2182,c_2373]) ).
cnf(c_2375,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(op1(e12,e10)) != op2(h2(e12),e22)
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2177,c_2374]) ).
cnf(c_2376,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| h2(e12) != op2(h2(e12),e22)
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2184,c_2375]) ).
cnf(c_2377,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| e20 != op2(h2(e12),e22)
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2177,c_2376]) ).
cnf(c_2378,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| e20 != op2(e20,e22)
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2177,c_2377]) ).
cnf(c_2379,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(h2(e12),e23) != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2169,c_2378]) ).
cnf(c_2380,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| op2(e20,e23) != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2177,c_2379]) ).
cnf(c_2381,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(h2(e12),h2(e12)) != h2(op1(e12,e12))
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2103,c_2380]) ).
cnf(c_2382,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(e20,h2(e12)) != h2(op1(e12,e12))
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2177,c_2381]) ).
cnf(c_2383,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| op2(e20,e20) != h2(op1(e12,e12))
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2177,c_2382]) ).
cnf(c_2384,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| h1(e11) != h2(op1(e12,e12))
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_398,c_2383]) ).
cnf(c_2385,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(op1(e12,e13)) != op2(h2(e12),e21)
| e21 != h2(op1(e12,e12))
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2195,c_2384]) ).
cnf(c_2386,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| h2(e10) != op2(h2(e12),e21)
| e21 != h2(op1(e12,e12))
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2187,c_2385]) ).
cnf(c_2387,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| e22 != op2(h2(e12),e21)
| e21 != h2(op1(e12,e12))
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2104,c_2386]) ).
cnf(c_2388,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| e22 != op2(e20,e21)
| e21 != h2(op1(e12,e12))
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2177,c_2387]) ).
cnf(c_2389,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != op2(e21,e22)
| e22 != e22
| e21 != h2(op1(e12,e12))
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_1897,c_2388]) ).
cnf(c_2390,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,h2(e12))
| h2(op1(e13,e10)) != e21
| e22 != e22
| e21 != h2(op1(e12,e12))
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2193,c_2389]) ).
cnf(c_2391,negated_conjecture,
( h2(e12) != e20
| h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| e22 != e22
| e21 != h2(op1(e12,e12))
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2177,c_2390]) ).
cnf(c_2392,negated_conjecture,
( e20 != e20
| h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| e22 != e22
| e21 != h2(op1(e12,e12))
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(paramod,[status(thm)],[c_2177,c_2391]) ).
cnf(c_2393,negated_conjecture,
( e20 != e20
| h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| e22 != e22
| h2(op1(e12,e12)) != e21
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| e20 != e20
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2392]) ).
cnf(c_2394,negated_conjecture,
( e20 != e20
| h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| e22 != e22
| h2(op1(e12,e12)) != e21
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| e22 != e22
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2393]) ).
cnf(c_2395,negated_conjecture,
( e20 != e20
| h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| e22 != e22
| h2(op1(e12,e12)) != e21
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e21 != e21
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2394]) ).
cnf(c_2396,negated_conjecture,
( e20 != e20
| h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| e22 != e22
| h2(op1(e12,e12)) != e21
| e23 != e23
| e20 != e20
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2395]) ).
cnf(c_2397,negated_conjecture,
( e20 != e20
| h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| e22 != e22
| h2(op1(e12,e12)) != e21
| e23 != e23
| e20 != e20
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2396]) ).
cnf(c_2398,negated_conjecture,
( e20 != e20
| h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| e22 != e22
| h2(op1(e12,e12)) != e21
| e23 != e23
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2397]) ).
cnf(c_2399,negated_conjecture,
( e20 != e20
| h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| e22 != e22
| h2(op1(e12,e12)) != e21
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2398]) ).
cnf(c_2400,negated_conjecture,
( e20 != e20
| h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e12)) != e21
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2399]) ).
cnf(c_2197,negated_conjecture,
( h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e12)) != e21
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(op1(e10,e10)) != h3(e11) ),
inference(copy,[status(thm)],[c_2400]) ).
cnf(c_2401,plain,
( op2(e22,e23) = e23
| h3(e11) = e23
| e22 = e23 ),
inference(paramod,[status(thm)],[c_2171,c_2089]) ).
cnf(c_2402,plain,
( e20 = e23
| h3(e11) = e23
| e22 = e23 ),
inference(paramod,[status(thm)],[c_2170,c_2401]) ).
cnf(c_2403,plain,
( e20 = e23
| h3(e11) = e23 ),
inference(resolve,[status(thm)],[c_276,c_2402]) ).
cnf(c_2198,plain,
h3(e11) = e23,
inference(resolve,[status(thm)],[c_271,c_2403]) ).
cnf(c_2404,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_2195,c_2165]) ).
cnf(c_2405,plain,
( op2(e23,e20) = e23
| e22 = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_2171,c_2404]) ).
cnf(c_2406,plain,
( op2(e23,e20) = e23
| e22 = e23 ),
inference(resolve,[status(thm)],[c_274,c_2405]) ).
cnf(c_2199,plain,
op2(e23,e20) = e23,
inference(resolve,[status(thm)],[c_276,c_2406]) ).
cnf(c_2407,plain,
( e22 = e20
| op2(e21,e20) = e20 ),
inference(paramod,[status(thm)],[c_2171,c_2010]) ).
cnf(c_2200,plain,
op2(e21,e20) = e20,
inference(resolve,[status(thm)],[c_269,c_2407]) ).
cnf(c_2408,plain,
( op2(e23,e22) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_2193,c_2105]) ).
cnf(c_2409,plain,
( op2(e23,e22) = e22
| e22 = e21 ),
inference(copy,[status(thm)],[c_2408]) ).
cnf(c_2201,plain,
op2(e23,e22) = e22,
inference(resolve,[status(thm)],[c_272,c_2409]) ).
cnf(c_2410,plain,
( op1(e12,e13) = e13
| op1(e12,e12) = e13
| e12 = e13 ),
inference(paramod,[status(thm)],[c_2184,c_2148]) ).
cnf(c_2411,plain,
( e10 = e13
| op1(e12,e12) = e13
| e12 = e13 ),
inference(paramod,[status(thm)],[c_2187,c_2410]) ).
cnf(c_2412,plain,
( e10 = e13
| op1(e12,e12) = e13 ),
inference(resolve,[status(thm)],[c_267,c_2411]) ).
cnf(c_2205,plain,
op1(e12,e12) = e13,
inference(resolve,[status(thm)],[c_262,c_2412]) ).
cnf(c_2413,plain,
( e12 = e10
| op1(e11,e10) = e10 ),
inference(paramod,[status(thm)],[c_2184,c_2085]) ).
cnf(c_2206,plain,
op1(e11,e10) = e10,
inference(resolve,[status(thm)],[c_260,c_2413]) ).
cnf(c_2414,plain,
e12 != op1(e13,e10),
inference(paramod,[status(thm)],[c_2184,c_123]) ).
cnf(c_2207,plain,
op1(e13,e10) != e12,
inference(copy,[status(thm)],[c_2414]) ).
cnf(c_2415,plain,
( op1(e11,e12) = e11
| e10 = e11 ),
inference(paramod,[status(thm)],[c_2186,c_2178]) ).
cnf(c_2416,plain,
( op1(e11,e12) = e11
| e11 = e10 ),
inference(copy,[status(thm)],[c_2415]) ).
cnf(c_2209,plain,
op1(e11,e12) = e11,
inference(resolve,[status(thm)],[c_259,c_2416]) ).
cnf(c_2417,plain,
( e10 = e11
| op1(e10,e10) = e11 ),
inference(paramod,[status(thm)],[c_2186,c_1994]) ).
cnf(c_2418,plain,
( e11 = e10
| op1(e10,e10) = e11 ),
inference(copy,[status(thm)],[c_2417]) ).
cnf(c_2210,plain,
op1(e10,e10) = e11,
inference(resolve,[status(thm)],[c_259,c_2418]) ).
cnf(c_2419,negated_conjecture,
( h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e12)) != e21
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| h2(e11) != h3(e11) ),
inference(paramod,[status(thm)],[c_2210,c_2197]) ).
cnf(c_2420,negated_conjecture,
( h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e12)) != e21
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e23 != h3(e11) ),
inference(paramod,[status(thm)],[c_2016,c_2419]) ).
cnf(c_2421,negated_conjecture,
( h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e12)) != e21
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(op1(e11,e10)) != op2(e23,e22)
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2198,c_2420]) ).
cnf(c_2422,negated_conjecture,
( h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e12)) != e21
| h2(op1(e11,e12)) != op2(e23,e20)
| h2(e10) != op2(e23,e22)
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2206,c_2421]) ).
cnf(c_2423,negated_conjecture,
( h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e12)) != e21
| h2(op1(e11,e12)) != op2(e23,e20)
| e22 != op2(e23,e22)
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2104,c_2422]) ).
cnf(c_2424,negated_conjecture,
( h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e12)) != e21
| h2(op1(e11,e12)) != op2(e23,e20)
| e22 != e22
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2201,c_2423]) ).
cnf(c_2425,negated_conjecture,
( h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e12)) != e21
| h2(e11) != op2(e23,e20)
| e22 != e22
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2209,c_2424]) ).
cnf(c_2426,negated_conjecture,
( h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e12)) != e21
| e23 != op2(e23,e20)
| e22 != e22
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2016,c_2425]) ).
cnf(c_2427,negated_conjecture,
( h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| h2(op1(e12,e12)) != e21
| e23 != e23
| e22 != e22
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2199,c_2426]) ).
cnf(c_2428,negated_conjecture,
( h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| h2(e13) != e21
| e23 != e23
| e22 != e22
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2205,c_2427]) ).
cnf(c_2429,negated_conjecture,
( h2(op1(e13,e12)) != op2(e21,e20)
| h2(op1(e13,e10)) != e21
| e21 != e21
| e23 != e23
| e22 != e22
| e23 != e23 ),
inference(paramod,[status(thm)],[c_401,c_2428]) ).
cnf(c_2430,negated_conjecture,
( h2(op1(e13,e12)) != e20
| h2(op1(e13,e10)) != e21
| e21 != e21
| e23 != e23
| e22 != e22
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2200,c_2429]) ).
cnf(c_2431,negated_conjecture,
( h2(op1(e13,e12)) != e20
| h2(op1(e13,e10)) != e21
| e21 != e21
| e23 != e23
| e22 != e22 ),
inference(copy,[status(thm)],[c_2430]) ).
cnf(c_2432,negated_conjecture,
( h2(op1(e13,e12)) != e20
| h2(op1(e13,e10)) != e21
| e21 != e21
| e23 != e23 ),
inference(copy,[status(thm)],[c_2431]) ).
cnf(c_2433,negated_conjecture,
( h2(op1(e13,e12)) != e20
| h2(op1(e13,e10)) != e21
| e21 != e21 ),
inference(copy,[status(thm)],[c_2432]) ).
cnf(c_2215,negated_conjecture,
( h2(op1(e13,e12)) != e20
| h2(op1(e13,e10)) != e21 ),
inference(copy,[status(thm)],[c_2433]) ).
cnf(c_2434,plain,
( op1(e13,e12) = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_2209,c_2151]) ).
cnf(c_2435,plain,
( op1(e13,e12) = e12
| e12 = e11 ),
inference(copy,[status(thm)],[c_2434]) ).
cnf(c_2219,plain,
op1(e13,e12) = e12,
inference(resolve,[status(thm)],[c_263,c_2435]) ).
cnf(c_2220,plain,
op1(e13,e10) = e13,
inference(resolve,[status(thm)],[c_2207,c_1989]) ).
cnf(c_2436,negated_conjecture,
( h2(op1(e13,e12)) != e20
| h2(e13) != e21 ),
inference(paramod,[status(thm)],[c_2220,c_2215]) ).
cnf(c_2437,negated_conjecture,
( h2(op1(e13,e12)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_401,c_2436]) ).
cnf(c_2438,negated_conjecture,
( h2(e12) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_2219,c_2437]) ).
cnf(c_2439,negated_conjecture,
( e20 != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_2177,c_2438]) ).
cnf(c_2440,negated_conjecture,
e20 != e20,
inference(copy,[status(thm)],[c_2439]) ).
cnf(c_2223,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_2440]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG111+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n015.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 26 21:13:15 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 776932 was started by sandbox on n015,
% 0.11/0.37 % Sat Sep 26 21:13:15 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 11.26/11.59
% 11.26/11.59 % From the command line: assign(max_seconds, 300).
% 11.37/12.01
% 11.37/12.01 % SZS status Theorem for theBenchmark
% 11.37/12.01
% 11.37/12.01 % Proof 1 at 0.36 (+ 0.03) seconds.
% 11.37/12.01 % Length of proof is 235.
% 11.37/12.01 % Level of proof is 14.
% 11.37/12.01 % Maximum clause weight is 171.000.
% 11.37/12.01 % Given clauses 0.
% 11.37/12.01
% 11.37/12.01 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------