%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG113+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 : n017.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 58.58s 55.82s
% Output : CNFRefutation 58.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 113
% Number of leaves : 23
% Syntax : Number of formulae : 457 ( 183 unt; 0 def)
% Number of atoms : 3538 (3537 equ)
% Maximal formula atoms : 384 ( 7 avg)
% Number of connectives : 4886 (1805 ~;2391 |; 690 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 6 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 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(e12,e12) = e12
& op1(e11,e11) = e11
& op1(e10,e10) = e10 ),
file('theBenchmark.p',ax10) ).
fof(ax11,axiom,
( op2(e23,e23) = e23
& op2(e22,e22) = e22
& op2(e21,e21) = e21
& op2(e20,e20) = e20 ),
file('theBenchmark.p',ax11) ).
fof(ax12,axiom,
( e11 = op1(op1(e12,e13),e13)
& e10 = op1(e12,e13) ),
file('theBenchmark.p',ax12) ).
fof(ax13,axiom,
( e21 = op2(op2(e22,e23),e23)
& e20 = op2(e22,e23) ),
file('theBenchmark.p',ax13) ).
fof(ax14,axiom,
( h1(e11) = op2(op2(e20,e21),e21)
& h1(e10) = op2(e20,e21)
& h1(e13) = e21
& h1(e12) = e20 ),
file('theBenchmark.p',ax14) ).
fof(ax15,axiom,
( h2(e11) = op2(op2(e20,e22),e22)
& h2(e10) = op2(e20,e22)
& h2(e13) = e22
& h2(e12) = e20 ),
file('theBenchmark.p',ax15) ).
fof(ax16,axiom,
( h3(e11) = op2(op2(e20,e23),e23)
& h3(e10) = op2(e20,e23)
& h3(e13) = e23
& h3(e12) = e20 ),
file('theBenchmark.p',ax16) ).
fof(ax17,axiom,
( h4(e11) = op2(op2(e21,e20),e20)
& h4(e10) = op2(e21,e20)
& h4(e13) = e20
& h4(e12) = e21 ),
file('theBenchmark.p',ax17) ).
fof(ax18,axiom,
( h5(e11) = op2(op2(e21,e22),e22)
& h5(e10) = op2(e21,e22)
& h5(e13) = e22
& h5(e12) = e21 ),
file('theBenchmark.p',ax18) ).
fof(ax20,axiom,
( h7(e11) = op2(op2(e22,e20),e20)
& h7(e10) = op2(e22,e20)
& h7(e13) = e20
& h7(e12) = e22 ),
file('theBenchmark.p',ax20) ).
fof(ax21,axiom,
( h8(e11) = op2(op2(e22,e21),e21)
& h8(e10) = op2(e22,e21)
& h8(e13) = e21
& h8(e12) = e22 ),
file('theBenchmark.p',ax21) ).
fof(ax23,axiom,
( h10(e11) = op2(op2(e23,e20),e20)
& h10(e10) = op2(e23,e20)
& h10(e13) = e20
& h10(e12) = e23 ),
file('theBenchmark.p',ax23) ).
fof(ax24,axiom,
( h11(e11) = op2(op2(e23,e21),e21)
& h11(e10) = op2(e23,e21)
& h11(e13) = e21
& h11(e12) = e23 ),
file('theBenchmark.p',ax24) ).
fof(ax25,axiom,
( h12(e11) = op2(op2(e23,e22),e22)
& h12(e10) = op2(e23,e22)
& h12(e13) = e22
& h12(e12) = e23 ),
file('theBenchmark.p',ax25) ).
fof(co1,conjecture,
( ( ( h12(e13) = e23
| h12(e12) = e23
| h12(e11) = e23
| h12(e10) = e23 )
& ( h12(e13) = e22
| h12(e12) = e22
| h12(e11) = e22
| h12(e10) = e22 )
& ( h12(e13) = e21
| h12(e12) = e21
| h12(e11) = e21
| h12(e10) = e21 )
& ( h12(e13) = e20
| h12(e12) = e20
| h12(e11) = e20
| h12(e10) = e20 )
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e10)) = op2(h12(e10),h12(e10)) )
| ( ( h11(e13) = e23
| h11(e12) = e23
| h11(e11) = e23
| h11(e10) = e23 )
& ( h11(e13) = e22
| h11(e12) = e22
| h11(e11) = e22
| h11(e10) = e22 )
& ( h11(e13) = e21
| h11(e12) = e21
| h11(e11) = e21
| h11(e10) = e21 )
& ( h11(e13) = e20
| h11(e12) = e20
| h11(e11) = e20
| h11(e10) = e20 )
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e10)) = op2(h11(e10),h11(e10)) )
| ( ( h10(e13) = e23
| h10(e12) = e23
| h10(e11) = e23
| h10(e10) = e23 )
& ( h10(e13) = e22
| h10(e12) = e22
| h10(e11) = e22
| h10(e10) = e22 )
& ( h10(e13) = e21
| h10(e12) = e21
| h10(e11) = e21
| h10(e10) = e21 )
& ( h10(e13) = e20
| h10(e12) = e20
| h10(e11) = e20
| h10(e10) = e20 )
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e10)) = op2(h10(e10),h10(e10)) )
| ( ( h9(e13) = e23
| h9(e12) = e23
| h9(e11) = e23
| h9(e10) = e23 )
& ( h9(e13) = e22
| h9(e12) = e22
| h9(e11) = e22
| h9(e10) = e22 )
& ( h9(e13) = e21
| h9(e12) = e21
| h9(e11) = e21
| h9(e10) = e21 )
& ( h9(e13) = e20
| h9(e12) = e20
| h9(e11) = e20
| h9(e10) = e20 )
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e10)) = op2(h9(e10),h9(e10)) )
| ( ( h8(e13) = e23
| h8(e12) = e23
| h8(e11) = e23
| h8(e10) = e23 )
& ( h8(e13) = e22
| h8(e12) = e22
| h8(e11) = e22
| h8(e10) = e22 )
& ( h8(e13) = e21
| h8(e12) = e21
| h8(e11) = e21
| h8(e10) = e21 )
& ( h8(e13) = e20
| h8(e12) = e20
| h8(e11) = e20
| h8(e10) = e20 )
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e10)) = op2(h8(e10),h8(e10)) )
| ( ( h7(e13) = e23
| h7(e12) = e23
| h7(e11) = e23
| h7(e10) = e23 )
& ( h7(e13) = e22
| h7(e12) = e22
| h7(e11) = e22
| h7(e10) = e22 )
& ( h7(e13) = e21
| h7(e12) = e21
| h7(e11) = e21
| h7(e10) = e21 )
& ( h7(e13) = e20
| h7(e12) = e20
| h7(e11) = e20
| h7(e10) = e20 )
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e10)) = op2(h7(e10),h7(e10)) )
| ( ( h6(e13) = e23
| h6(e12) = e23
| h6(e11) = e23
| h6(e10) = e23 )
& ( h6(e13) = e22
| h6(e12) = e22
| h6(e11) = e22
| h6(e10) = e22 )
& ( h6(e13) = e21
| h6(e12) = e21
| h6(e11) = e21
| h6(e10) = e21 )
& ( h6(e13) = e20
| h6(e12) = e20
| h6(e11) = e20
| h6(e10) = e20 )
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e10)) = op2(h6(e10),h6(e10)) )
| ( ( h5(e13) = e23
| h5(e12) = e23
| h5(e11) = e23
| h5(e10) = e23 )
& ( h5(e13) = e22
| h5(e12) = e22
| h5(e11) = e22
| h5(e10) = e22 )
& ( h5(e13) = e21
| h5(e12) = e21
| h5(e11) = e21
| h5(e10) = e21 )
& ( h5(e13) = e20
| h5(e12) = e20
| h5(e11) = e20
| h5(e10) = e20 )
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e10)) = op2(h5(e10),h5(e10)) )
| ( ( 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,
~ ( ( ( h12(e13) = e23
| h12(e12) = e23
| h12(e11) = e23
| h12(e10) = e23 )
& ( h12(e13) = e22
| h12(e12) = e22
| h12(e11) = e22
| h12(e10) = e22 )
& ( h12(e13) = e21
| h12(e12) = e21
| h12(e11) = e21
| h12(e10) = e21 )
& ( h12(e13) = e20
| h12(e12) = e20
| h12(e11) = e20
| h12(e10) = e20 )
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e10)) = op2(h12(e10),h12(e10)) )
| ( ( h11(e13) = e23
| h11(e12) = e23
| h11(e11) = e23
| h11(e10) = e23 )
& ( h11(e13) = e22
| h11(e12) = e22
| h11(e11) = e22
| h11(e10) = e22 )
& ( h11(e13) = e21
| h11(e12) = e21
| h11(e11) = e21
| h11(e10) = e21 )
& ( h11(e13) = e20
| h11(e12) = e20
| h11(e11) = e20
| h11(e10) = e20 )
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e10)) = op2(h11(e10),h11(e10)) )
| ( ( h10(e13) = e23
| h10(e12) = e23
| h10(e11) = e23
| h10(e10) = e23 )
& ( h10(e13) = e22
| h10(e12) = e22
| h10(e11) = e22
| h10(e10) = e22 )
& ( h10(e13) = e21
| h10(e12) = e21
| h10(e11) = e21
| h10(e10) = e21 )
& ( h10(e13) = e20
| h10(e12) = e20
| h10(e11) = e20
| h10(e10) = e20 )
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e10)) = op2(h10(e10),h10(e10)) )
| ( ( h9(e13) = e23
| h9(e12) = e23
| h9(e11) = e23
| h9(e10) = e23 )
& ( h9(e13) = e22
| h9(e12) = e22
| h9(e11) = e22
| h9(e10) = e22 )
& ( h9(e13) = e21
| h9(e12) = e21
| h9(e11) = e21
| h9(e10) = e21 )
& ( h9(e13) = e20
| h9(e12) = e20
| h9(e11) = e20
| h9(e10) = e20 )
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e10)) = op2(h9(e10),h9(e10)) )
| ( ( h8(e13) = e23
| h8(e12) = e23
| h8(e11) = e23
| h8(e10) = e23 )
& ( h8(e13) = e22
| h8(e12) = e22
| h8(e11) = e22
| h8(e10) = e22 )
& ( h8(e13) = e21
| h8(e12) = e21
| h8(e11) = e21
| h8(e10) = e21 )
& ( h8(e13) = e20
| h8(e12) = e20
| h8(e11) = e20
| h8(e10) = e20 )
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e10)) = op2(h8(e10),h8(e10)) )
| ( ( h7(e13) = e23
| h7(e12) = e23
| h7(e11) = e23
| h7(e10) = e23 )
& ( h7(e13) = e22
| h7(e12) = e22
| h7(e11) = e22
| h7(e10) = e22 )
& ( h7(e13) = e21
| h7(e12) = e21
| h7(e11) = e21
| h7(e10) = e21 )
& ( h7(e13) = e20
| h7(e12) = e20
| h7(e11) = e20
| h7(e10) = e20 )
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e10)) = op2(h7(e10),h7(e10)) )
| ( ( h6(e13) = e23
| h6(e12) = e23
| h6(e11) = e23
| h6(e10) = e23 )
& ( h6(e13) = e22
| h6(e12) = e22
| h6(e11) = e22
| h6(e10) = e22 )
& ( h6(e13) = e21
| h6(e12) = e21
| h6(e11) = e21
| h6(e10) = e21 )
& ( h6(e13) = e20
| h6(e12) = e20
| h6(e11) = e20
| h6(e10) = e20 )
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e10)) = op2(h6(e10),h6(e10)) )
| ( ( h5(e13) = e23
| h5(e12) = e23
| h5(e11) = e23
| h5(e10) = e23 )
& ( h5(e13) = e22
| h5(e12) = e22
| h5(e11) = e22
| h5(e10) = e22 )
& ( h5(e13) = e21
| h5(e12) = e21
| h5(e11) = e21
| h5(e10) = e21 )
& ( h5(e13) = e20
| h5(e12) = e20
| h5(e11) = e20
| h5(e10) = e20 )
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e10)) = op2(h5(e10),h5(e10)) )
| ( ( 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_29,plain,
( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_36,plain,
( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_47,plain,
( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_48,plain,
( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| op1(e10,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_50,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| op1(e10,e10) = e13 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_51,plain,
( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_52,plain,
( op1(e13,e11) = e10
| op1(e12,e11) = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_61,plain,
( op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_62,plain,
( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_72,plain,
( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_77,plain,
( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| op2(e20,e22) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_79,plain,
( op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e21
| op2(e21,e20) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_84,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_87,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_95,plain,
( op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| op2(e20,e20) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_99,plain,
( op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20
| op2(e21,e20) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_100,plain,
( op2(e23,e21) = e20
| op2(e22,e21) = e20
| op2(e21,e21) = e20
| op2(e20,e21) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_109,plain,
( op2(e22,e23) = e21
| op2(e22,e22) = e21
| op2(e22,e21) = e21
| op2(e22,e20) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_110,plain,
( op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_120,plain,
( op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_123,plain,
op1(e11,e10) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_139,plain,
op1(e12,e11) != op1(e11,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_140,plain,
op1(e11,e11) != op1(e12,e11),
inference(copy,[status(thm)],[c_139]) ).
cnf(c_146,plain,
op1(e12,e12) != op1(e10,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_147,plain,
op1(e10,e12) != op1(e12,e12),
inference(copy,[status(thm)],[c_146]) ).
cnf(c_167,plain,
op1(e10,e11) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_168,plain,
op1(e10,e12) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_169,plain,
op1(e10,e10) != op1(e10,e12),
inference(copy,[status(thm)],[c_168]) ).
cnf(c_176,plain,
op1(e10,e13) != op1(e10,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_177,plain,
op1(e10,e12) != op1(e10,e13),
inference(copy,[status(thm)],[c_176]) ).
cnf(c_183,plain,
op1(e11,e12) != op1(e11,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_184,plain,
op1(e11,e11) != op1(e11,e12),
inference(copy,[status(thm)],[c_183]) ).
cnf(c_194,plain,
op1(e12,e12) != op1(e12,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_195,plain,
op1(e12,e11) != op1(e12,e12),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_196,plain,
op1(e12,e13) != op1(e12,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_197,plain,
op1(e12,e11) != op1(e12,e13),
inference(copy,[status(thm)],[c_196]) ).
cnf(c_203,plain,
op1(e13,e13) != op1(e13,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_204,plain,
op1(e13,e10) != op1(e13,e13),
inference(copy,[status(thm)],[c_203]) ).
cnf(c_211,plain,
op2(e21,e20) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_214,plain,
op2(e23,e20) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_215,plain,
op2(e20,e20) != op2(e23,e20),
inference(copy,[status(thm)],[c_214]) ).
cnf(c_220,plain,
op2(e23,e20) != op2(e22,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_221,plain,
op2(e22,e20) != op2(e23,e20),
inference(copy,[status(thm)],[c_220]) ).
cnf(c_227,plain,
op2(e22,e21) != op2(e21,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_228,plain,
op2(e21,e21) != op2(e22,e21),
inference(copy,[status(thm)],[c_227]) ).
cnf(c_234,plain,
op2(e22,e22) != op2(e20,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_235,plain,
op2(e20,e22) != op2(e22,e22),
inference(copy,[status(thm)],[c_234]) ).
cnf(c_255,plain,
op2(e20,e21) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_256,plain,
op2(e20,e22) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_257,plain,
op2(e20,e20) != op2(e20,e22),
inference(copy,[status(thm)],[c_256]) ).
cnf(c_264,plain,
op2(e20,e23) != op2(e20,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_265,plain,
op2(e20,e22) != op2(e20,e23),
inference(copy,[status(thm)],[c_264]) ).
cnf(c_266,plain,
op2(e21,e21) != op2(e21,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_269,plain,
op2(e21,e23) != op2(e21,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_270,plain,
op2(e21,e20) != op2(e21,e23),
inference(copy,[status(thm)],[c_269]) ).
cnf(c_271,plain,
op2(e21,e22) != op2(e21,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_272,plain,
op2(e21,e21) != op2(e21,e22),
inference(copy,[status(thm)],[c_271]) ).
cnf(c_282,plain,
op2(e22,e22) != op2(e22,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_283,plain,
op2(e22,e21) != op2(e22,e22),
inference(copy,[status(thm)],[c_282]) ).
cnf(c_284,plain,
op2(e22,e23) != op2(e22,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_285,plain,
op2(e22,e21) != op2(e22,e23),
inference(copy,[status(thm)],[c_284]) ).
cnf(c_291,plain,
op2(e23,e23) != op2(e23,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_292,plain,
op2(e23,e20) != op2(e23,e23),
inference(copy,[status(thm)],[c_291]) ).
cnf(c_299,plain,
e11 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_300,plain,
e12 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_301,plain,
e10 != e12,
inference(copy,[status(thm)],[c_300]) ).
cnf(c_302,plain,
e13 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_303,plain,
e10 != e13,
inference(copy,[status(thm)],[c_302]) ).
cnf(c_304,plain,
e12 != e11,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_305,plain,
e11 != e12,
inference(copy,[status(thm)],[c_304]) ).
cnf(c_306,plain,
e13 != e11,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_307,plain,
e11 != e13,
inference(copy,[status(thm)],[c_306]) ).
cnf(c_308,plain,
e13 != e12,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_309,plain,
e12 != e13,
inference(copy,[status(thm)],[c_308]) ).
cnf(c_310,plain,
e21 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_311,plain,
e22 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_312,plain,
e20 != e22,
inference(copy,[status(thm)],[c_311]) ).
cnf(c_313,plain,
e23 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_314,plain,
e20 != e23,
inference(copy,[status(thm)],[c_313]) ).
cnf(c_315,plain,
e22 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_316,plain,
e21 != e22,
inference(copy,[status(thm)],[c_315]) ).
cnf(c_317,plain,
e23 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_318,plain,
e21 != e23,
inference(copy,[status(thm)],[c_317]) ).
cnf(c_319,plain,
e23 != e22,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_320,plain,
e22 != e23,
inference(copy,[status(thm)],[c_319]) ).
cnf(c_353,plain,
op1(e10,e10) = e10,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_354,plain,
op1(e11,e11) = e11,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_355,plain,
op1(e12,e12) = e12,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_356,plain,
op1(e13,e13) = e13,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_357,plain,
op2(e20,e20) = e20,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_358,plain,
op2(e21,e21) = e21,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_359,plain,
op2(e22,e22) = e22,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_360,plain,
op2(e23,e23) = e23,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_361,plain,
op1(e12,e13) = e10,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_362,plain,
op1(op1(e12,e13),e13) = e11,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_363,plain,
op1(e10,e13) = e11,
inference(paramod,[status(thm)],[c_361,c_362]) ).
cnf(c_364,plain,
op2(e22,e23) = e20,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_365,plain,
op2(op2(e22,e23),e23) = e21,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_366,plain,
op2(e20,e23) = e21,
inference(paramod,[status(thm)],[c_364,c_365]) ).
cnf(c_369,plain,
h1(e10) = op2(e20,e21),
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_370,plain,
op2(e20,e21) = h1(e10),
inference(copy,[status(thm)],[c_369]) ).
cnf(c_373,plain,
h2(e12) = e20,
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_374,plain,
h2(e13) = e22,
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_375,plain,
h2(e10) = op2(e20,e22),
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_376,plain,
op2(e20,e22) = h2(e10),
inference(copy,[status(thm)],[c_375]) ).
cnf(c_377,plain,
h2(e11) = op2(op2(e20,e22),e22),
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_4049,plain,
h2(e11) = op2(h2(e10),e22),
inference(paramod,[status(thm)],[c_376,c_377]) ).
cnf(c_378,plain,
op2(h2(e10),e22) = h2(e11),
inference(copy,[status(thm)],[c_4049]) ).
cnf(c_383,plain,
h3(e11) = op2(op2(e20,e23),e23),
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_4050,plain,
h3(e11) = op2(e21,e23),
inference(paramod,[status(thm)],[c_366,c_383]) ).
cnf(c_384,plain,
op2(e21,e23) = h3(e11),
inference(copy,[status(thm)],[c_4050]) ).
cnf(c_387,plain,
h4(e10) = op2(e21,e20),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_388,plain,
op2(e21,e20) = h4(e10),
inference(copy,[status(thm)],[c_387]) ).
cnf(c_393,plain,
h5(e10) = op2(e21,e22),
inference(clausify,[status(thm)],[ax18]) ).
cnf(c_394,plain,
op2(e21,e22) = h5(e10),
inference(copy,[status(thm)],[c_393]) ).
cnf(c_405,plain,
h7(e10) = op2(e22,e20),
inference(clausify,[status(thm)],[ax20]) ).
cnf(c_406,plain,
op2(e22,e20) = h7(e10),
inference(copy,[status(thm)],[c_405]) ).
cnf(c_411,plain,
h8(e10) = op2(e22,e21),
inference(clausify,[status(thm)],[ax21]) ).
cnf(c_412,plain,
op2(e22,e21) = h8(e10),
inference(copy,[status(thm)],[c_411]) ).
cnf(c_423,plain,
h10(e10) = op2(e23,e20),
inference(clausify,[status(thm)],[ax23]) ).
cnf(c_424,plain,
op2(e23,e20) = h10(e10),
inference(copy,[status(thm)],[c_423]) ).
cnf(c_429,plain,
h11(e10) = op2(e23,e21),
inference(clausify,[status(thm)],[ax24]) ).
cnf(c_430,plain,
op2(e23,e21) = h11(e10),
inference(copy,[status(thm)],[c_429]) ).
cnf(c_435,plain,
h12(e10) = op2(e23,e22),
inference(clausify,[status(thm)],[ax25]) ).
cnf(c_436,plain,
op2(e23,e22) = h12(e10),
inference(copy,[status(thm)],[c_435]) ).
cnf(c_921,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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_4051,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_353,c_921]) ).
cnf(c_4052,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_373,c_4051]) ).
cnf(c_4053,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e11) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_363,c_4052]) ).
cnf(c_4054,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e11) != op2(h2(e10),e22)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_374,c_4053]) ).
cnf(c_4055,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_378,c_4054]) ).
cnf(c_4056,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_354,c_4055]) ).
cnf(c_4057,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_373,c_4056]) ).
cnf(c_4058,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_374,c_4057]) ).
cnf(c_4059,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_373,c_4058]) ).
cnf(c_4060,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_373,c_4059]) ).
cnf(c_4061,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e12) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_355,c_4060]) ).
cnf(c_4062,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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))
| e20 != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_373,c_4061]) ).
cnf(c_4063,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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))
| e20 != op2(e20,h2(e12))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_373,c_4062]) ).
cnf(c_4064,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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))
| e20 != op2(e20,e20)
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_373,c_4063]) ).
cnf(c_4065,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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))
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_357,c_4064]) ).
cnf(c_4066,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e10) != op2(h2(e12),h2(e13))
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_361,c_4065]) ).
cnf(c_4067,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e10) != op2(e20,h2(e13))
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_373,c_4066]) ).
cnf(c_4068,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e10) != op2(e20,e22)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_374,c_4067]) ).
cnf(c_4069,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_376,c_4068]) ).
cnf(c_4070,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_374,c_4069]) ).
cnf(c_4071,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != 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(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_374,c_4070]) ).
cnf(c_4072,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != e21
| h2(e12) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(e22,h2(e12))
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_374,c_4071]) ).
cnf(c_4073,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != e21
| h2(e12) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(e22,e20)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_373,c_4072]) ).
cnf(c_4074,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != e21
| h2(e12) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_406,c_4073]) ).
cnf(c_4075,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != e21
| h2(e12) != e20
| h2(e13) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_356,c_4074]) ).
cnf(c_4076,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != e21
| h2(e12) != e20
| e22 != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_374,c_4075]) ).
cnf(c_4077,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != e21
| h2(e12) != e20
| e22 != op2(e22,h2(e13))
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_374,c_4076]) ).
cnf(c_4078,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != e21
| h2(e12) != e20
| e22 != op2(e22,e22)
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_374,c_4077]) ).
cnf(c_4079,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != e21
| h2(e12) != e20
| e22 != e22
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_359,c_4078]) ).
cnf(c_4080,negated_conjecture,
( h2(e10) != e23
| h2(e13) != e22
| h2(e11) != e21
| e20 != e20
| e22 != e22
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_373,c_4079]) ).
cnf(c_4081,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| h2(e11) != e21
| e20 != e20
| e22 != e22
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(e10) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_374,c_4080]) ).
cnf(c_4082,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| h2(e11) != e21
| e20 != e20
| e22 != e22
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| op2(h2(e10),h2(e10)) != h2(e10) ),
inference(copy,[status(thm)],[c_4081]) ).
cnf(c_4083,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| h2(e11) != e21
| e20 != e20
| e22 != e22
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e10) ),
inference(copy,[status(thm)],[c_4082]) ).
cnf(c_4084,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| h2(e11) != e21
| e20 != e20
| e22 != e22
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| h2(e11) != op2(h2(e11),h2(e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e10) ),
inference(copy,[status(thm)],[c_4083]) ).
cnf(c_4085,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| h2(e11) != e21
| e20 != e20
| e22 != e22
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(e11) != h2(e11)
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e10) ),
inference(copy,[status(thm)],[c_4084]) ).
cnf(c_4086,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| h2(e11) != e21
| e20 != e20
| e22 != e22
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| e20 != e20
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e10) ),
inference(copy,[status(thm)],[c_4085]) ).
cnf(c_4087,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| h2(e11) != e21
| e20 != e20
| e22 != e22
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e10) != h2(e10)
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e10) ),
inference(copy,[status(thm)],[c_4086]) ).
cnf(c_4088,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| h2(e11) != e21
| e20 != e20
| e22 != e22
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e10) ),
inference(copy,[status(thm)],[c_4087]) ).
cnf(c_4089,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| h2(e11) != e21
| e20 != e20
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e10) ),
inference(copy,[status(thm)],[c_4088]) ).
cnf(c_4090,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e10) ),
inference(copy,[status(thm)],[c_4089]) ).
cnf(c_922,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(e10) ),
inference(copy,[status(thm)],[c_4090]) ).
cnf(c_4091,plain,
e10 != op1(e10,e12),
inference(paramod,[status(thm)],[c_353,c_169]) ).
cnf(c_3876,plain,
op1(e10,e12) != e10,
inference(copy,[status(thm)],[c_4091]) ).
cnf(c_3877,plain,
op1(e10,e11) != e10,
inference(paramod,[status(thm)],[c_353,c_167]) ).
cnf(c_3880,plain,
op1(e11,e10) != e10,
inference(paramod,[status(thm)],[c_353,c_123]) ).
cnf(c_4092,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_353,c_50]) ).
cnf(c_3881,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13 ),
inference(resolve,[status(thm)],[c_303,c_4092]) ).
cnf(c_4093,plain,
( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| e10 = e12 ),
inference(paramod,[status(thm)],[c_353,c_48]) ).
cnf(c_3883,plain,
( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12 ),
inference(resolve,[status(thm)],[c_301,c_4093]) ).
cnf(c_4094,plain,
( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| e10 = e12 ),
inference(paramod,[status(thm)],[c_353,c_47]) ).
cnf(c_4095,plain,
( e11 = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| e10 = e12 ),
inference(paramod,[status(thm)],[c_363,c_4094]) ).
cnf(c_4096,plain,
( e11 = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12 ),
inference(resolve,[status(thm)],[c_301,c_4095]) ).
cnf(c_3884,plain,
( op1(e10,e12) = e12
| op1(e10,e11) = e12 ),
inference(resolve,[status(thm)],[c_305,c_4096]) ).
cnf(c_4097,plain,
e11 != op1(e11,e12),
inference(paramod,[status(thm)],[c_354,c_184]) ).
cnf(c_3887,plain,
op1(e11,e12) != e11,
inference(copy,[status(thm)],[c_4097]) ).
cnf(c_4098,plain,
e11 != op1(e12,e11),
inference(paramod,[status(thm)],[c_354,c_140]) ).
cnf(c_3890,plain,
op1(e12,e11) != e11,
inference(copy,[status(thm)],[c_4098]) ).
cnf(c_4099,plain,
( op1(e13,e11) = e10
| op1(e12,e11) = e10
| e11 = e10
| op1(e10,e11) = e10 ),
inference(paramod,[status(thm)],[c_354,c_52]) ).
cnf(c_4100,plain,
( op1(e13,e11) = e10
| op1(e12,e11) = e10
| e11 = e10 ),
inference(resolve,[status(thm)],[c_3877,c_4099]) ).
cnf(c_3896,plain,
( op1(e13,e11) = e10
| op1(e12,e11) = e10 ),
inference(resolve,[status(thm)],[c_299,c_4100]) ).
cnf(c_4101,plain,
( op1(e11,e13) = e10
| op1(e11,e12) = e10
| e11 = e10
| op1(e11,e10) = e10 ),
inference(paramod,[status(thm)],[c_354,c_51]) ).
cnf(c_4102,plain,
( op1(e11,e13) = e10
| op1(e11,e12) = e10
| e11 = e10 ),
inference(resolve,[status(thm)],[c_3880,c_4101]) ).
cnf(c_3897,plain,
( op1(e11,e13) = e10
| op1(e11,e12) = e10 ),
inference(resolve,[status(thm)],[c_299,c_4102]) ).
cnf(c_3898,plain,
op1(e12,e11) != e12,
inference(paramod,[status(thm)],[c_355,c_195]) ).
cnf(c_3902,plain,
op1(e10,e12) != e12,
inference(paramod,[status(thm)],[c_355,c_147]) ).
cnf(c_4103,plain,
( op1(e13,e12) = e11
| e12 = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(paramod,[status(thm)],[c_355,c_62]) ).
cnf(c_4104,plain,
( op1(e13,e12) = e11
| e11 = e12
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(copy,[status(thm)],[c_4103]) ).
cnf(c_4105,plain,
( op1(e13,e12) = e11
| e11 = e12
| op1(e10,e12) = e11 ),
inference(resolve,[status(thm)],[c_3887,c_4104]) ).
cnf(c_3905,plain,
( op1(e13,e12) = e11
| op1(e10,e12) = e11 ),
inference(resolve,[status(thm)],[c_305,c_4105]) ).
cnf(c_4106,plain,
( op1(e12,e13) = e11
| e12 = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 ),
inference(paramod,[status(thm)],[c_355,c_61]) ).
cnf(c_4107,plain,
( e10 = e11
| e12 = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 ),
inference(paramod,[status(thm)],[c_361,c_4106]) ).
cnf(c_4108,plain,
( e10 = e11
| e11 = e12
| op1(e12,e11) = e11
| op1(e12,e10) = e11 ),
inference(copy,[status(thm)],[c_4107]) ).
cnf(c_4109,plain,
( e11 = e10
| e11 = e12
| op1(e12,e11) = e11
| op1(e12,e10) = e11 ),
inference(copy,[status(thm)],[c_4108]) ).
cnf(c_4110,plain,
( e11 = e10
| e11 = e12
| op1(e12,e10) = e11 ),
inference(resolve,[status(thm)],[c_3890,c_4109]) ).
cnf(c_4111,plain,
( e11 = e10
| op1(e12,e10) = e11 ),
inference(resolve,[status(thm)],[c_305,c_4110]) ).
cnf(c_3906,plain,
op1(e12,e10) = e11,
inference(resolve,[status(thm)],[c_299,c_4111]) ).
cnf(c_3910,plain,
op1(e13,e10) != e13,
inference(paramod,[status(thm)],[c_356,c_204]) ).
cnf(c_4112,plain,
( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_363,c_72]) ).
cnf(c_4113,plain,
( op1(e13,e13) = e12
| e10 = e12
| op1(e11,e13) = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_361,c_4112]) ).
cnf(c_4114,plain,
( e13 = e12
| e10 = e12
| op1(e11,e13) = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_356,c_4113]) ).
cnf(c_4115,plain,
( e12 = e13
| e10 = e12
| op1(e11,e13) = e12
| e11 = e12 ),
inference(copy,[status(thm)],[c_4114]) ).
cnf(c_4116,plain,
( e12 = e13
| e10 = e12
| op1(e11,e13) = e12 ),
inference(resolve,[status(thm)],[c_305,c_4115]) ).
cnf(c_4117,plain,
( e12 = e13
| op1(e11,e13) = e12 ),
inference(resolve,[status(thm)],[c_301,c_4116]) ).
cnf(c_3912,plain,
op1(e11,e13) = e12,
inference(resolve,[status(thm)],[c_309,c_4117]) ).
cnf(c_4118,plain,
e20 != op2(e20,e22),
inference(paramod,[status(thm)],[c_357,c_257]) ).
cnf(c_4119,plain,
e20 != h2(e10),
inference(paramod,[status(thm)],[c_376,c_4118]) ).
cnf(c_3916,plain,
h2(e10) != e20,
inference(copy,[status(thm)],[c_4119]) ).
cnf(c_4120,plain,
h1(e10) != op2(e20,e20),
inference(paramod,[status(thm)],[c_370,c_255]) ).
cnf(c_3917,plain,
h1(e10) != e20,
inference(paramod,[status(thm)],[c_357,c_4120]) ).
cnf(c_4121,plain,
e20 != op2(e23,e20),
inference(paramod,[status(thm)],[c_357,c_215]) ).
cnf(c_4122,plain,
e20 != h10(e10),
inference(paramod,[status(thm)],[c_424,c_4121]) ).
cnf(c_3918,plain,
h10(e10) != e20,
inference(copy,[status(thm)],[c_4122]) ).
cnf(c_4123,plain,
h4(e10) != op2(e20,e20),
inference(paramod,[status(thm)],[c_388,c_211]) ).
cnf(c_3920,plain,
h4(e10) != e20,
inference(paramod,[status(thm)],[c_357,c_4123]) ).
cnf(c_4124,plain,
( op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_357,c_95]) ).
cnf(c_4125,plain,
( op2(e20,e23) = e22
| op2(e20,e22) = e22
| h1(e10) = e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_370,c_4124]) ).
cnf(c_4126,plain,
( op2(e20,e23) = e22
| h2(e10) = e22
| h1(e10) = e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_376,c_4125]) ).
cnf(c_4127,plain,
( e21 = e22
| h2(e10) = e22
| h1(e10) = e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_366,c_4126]) ).
cnf(c_4128,plain,
( e21 = e22
| h2(e10) = e22
| h1(e10) = e22 ),
inference(resolve,[status(thm)],[c_312,c_4127]) ).
cnf(c_3924,plain,
( h2(e10) = e22
| h1(e10) = e22 ),
inference(resolve,[status(thm)],[c_316,c_4128]) ).
cnf(c_4129,plain,
e21 != op2(e21,e22),
inference(paramod,[status(thm)],[c_358,c_272]) ).
cnf(c_4130,plain,
e21 != h5(e10),
inference(paramod,[status(thm)],[c_394,c_4129]) ).
cnf(c_3927,plain,
h5(e10) != e21,
inference(copy,[status(thm)],[c_4130]) ).
cnf(c_4131,plain,
e21 != op2(e21,e20),
inference(paramod,[status(thm)],[c_358,c_266]) ).
cnf(c_4132,plain,
e21 != h4(e10),
inference(paramod,[status(thm)],[c_388,c_4131]) ).
cnf(c_3928,plain,
h4(e10) != e21,
inference(copy,[status(thm)],[c_4132]) ).
cnf(c_4133,plain,
e21 != op2(e22,e21),
inference(paramod,[status(thm)],[c_358,c_228]) ).
cnf(c_4134,plain,
e21 != h8(e10),
inference(paramod,[status(thm)],[c_412,c_4133]) ).
cnf(c_3930,plain,
h8(e10) != e21,
inference(copy,[status(thm)],[c_4134]) ).
cnf(c_4135,plain,
( op2(e23,e21) = e20
| op2(e22,e21) = e20
| op2(e21,e21) = e20
| h1(e10) = e20 ),
inference(paramod,[status(thm)],[c_370,c_100]) ).
cnf(c_4136,plain,
( op2(e23,e21) = e20
| op2(e22,e21) = e20
| e21 = e20
| h1(e10) = e20 ),
inference(paramod,[status(thm)],[c_358,c_4135]) ).
cnf(c_4137,plain,
( op2(e23,e21) = e20
| h8(e10) = e20
| e21 = e20
| h1(e10) = e20 ),
inference(paramod,[status(thm)],[c_412,c_4136]) ).
cnf(c_4138,plain,
( h11(e10) = e20
| h8(e10) = e20
| e21 = e20
| h1(e10) = e20 ),
inference(paramod,[status(thm)],[c_430,c_4137]) ).
cnf(c_4139,plain,
( h11(e10) = e20
| h8(e10) = e20
| e21 = e20 ),
inference(resolve,[status(thm)],[c_3917,c_4138]) ).
cnf(c_3936,plain,
( h11(e10) = e20
| h8(e10) = e20 ),
inference(resolve,[status(thm)],[c_310,c_4139]) ).
cnf(c_4140,plain,
( op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20
| h4(e10) = e20 ),
inference(paramod,[status(thm)],[c_388,c_99]) ).
cnf(c_4141,plain,
( op2(e21,e23) = e20
| op2(e21,e22) = e20
| e21 = e20
| h4(e10) = e20 ),
inference(paramod,[status(thm)],[c_358,c_4140]) ).
cnf(c_4142,plain,
( op2(e21,e23) = e20
| h5(e10) = e20
| e21 = e20
| h4(e10) = e20 ),
inference(paramod,[status(thm)],[c_394,c_4141]) ).
cnf(c_4143,plain,
( h3(e11) = e20
| h5(e10) = e20
| e21 = e20
| h4(e10) = e20 ),
inference(paramod,[status(thm)],[c_384,c_4142]) ).
cnf(c_4144,plain,
( h3(e11) = e20
| h5(e10) = e20
| e21 = e20 ),
inference(resolve,[status(thm)],[c_3920,c_4143]) ).
cnf(c_3937,plain,
( h3(e11) = e20
| h5(e10) = e20 ),
inference(resolve,[status(thm)],[c_310,c_4144]) ).
cnf(c_4145,plain,
h8(e10) != op2(e22,e22),
inference(paramod,[status(thm)],[c_412,c_283]) ).
cnf(c_3938,plain,
h8(e10) != e22,
inference(paramod,[status(thm)],[c_359,c_4145]) ).
cnf(c_4146,plain,
h2(e10) != op2(e22,e22),
inference(paramod,[status(thm)],[c_376,c_235]) ).
cnf(c_3942,plain,
h2(e10) != e22,
inference(paramod,[status(thm)],[c_359,c_4146]) ).
cnf(c_4147,plain,
( op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e21,e22) = e21
| h2(e10) = e21 ),
inference(paramod,[status(thm)],[c_376,c_110]) ).
cnf(c_4148,plain,
( op2(e23,e22) = e21
| op2(e22,e22) = e21
| h5(e10) = e21
| h2(e10) = e21 ),
inference(paramod,[status(thm)],[c_394,c_4147]) ).
cnf(c_4149,plain,
( op2(e23,e22) = e21
| e22 = e21
| h5(e10) = e21
| h2(e10) = e21 ),
inference(paramod,[status(thm)],[c_359,c_4148]) ).
cnf(c_4150,plain,
( h12(e10) = e21
| e22 = e21
| h5(e10) = e21
| h2(e10) = e21 ),
inference(paramod,[status(thm)],[c_436,c_4149]) ).
cnf(c_4151,plain,
( h12(e10) = e21
| e21 = e22
| h5(e10) = e21
| h2(e10) = e21 ),
inference(copy,[status(thm)],[c_4150]) ).
cnf(c_4152,plain,
( h12(e10) = e21
| e21 = e22
| h2(e10) = e21 ),
inference(resolve,[status(thm)],[c_3927,c_4151]) ).
cnf(c_3945,plain,
( h12(e10) = e21
| h2(e10) = e21 ),
inference(resolve,[status(thm)],[c_316,c_4152]) ).
cnf(c_4153,plain,
( op2(e22,e23) = e21
| op2(e22,e22) = e21
| op2(e22,e21) = e21
| h7(e10) = e21 ),
inference(paramod,[status(thm)],[c_406,c_109]) ).
cnf(c_4154,plain,
( op2(e22,e23) = e21
| op2(e22,e22) = e21
| h8(e10) = e21
| h7(e10) = e21 ),
inference(paramod,[status(thm)],[c_412,c_4153]) ).
cnf(c_4155,plain,
( op2(e22,e23) = e21
| e22 = e21
| h8(e10) = e21
| h7(e10) = e21 ),
inference(paramod,[status(thm)],[c_359,c_4154]) ).
cnf(c_4156,plain,
( e20 = e21
| e22 = e21
| h8(e10) = e21
| h7(e10) = e21 ),
inference(paramod,[status(thm)],[c_364,c_4155]) ).
cnf(c_4157,plain,
( e20 = e21
| e21 = e22
| h8(e10) = e21
| h7(e10) = e21 ),
inference(copy,[status(thm)],[c_4156]) ).
cnf(c_4158,plain,
( e21 = e20
| e21 = e22
| h8(e10) = e21
| h7(e10) = e21 ),
inference(copy,[status(thm)],[c_4157]) ).
cnf(c_4159,plain,
( e21 = e20
| e21 = e22
| h7(e10) = e21 ),
inference(resolve,[status(thm)],[c_3930,c_4158]) ).
cnf(c_4160,plain,
( e21 = e20
| h7(e10) = e21 ),
inference(resolve,[status(thm)],[c_316,c_4159]) ).
cnf(c_3946,plain,
h7(e10) = e21,
inference(resolve,[status(thm)],[c_310,c_4160]) ).
cnf(c_4161,plain,
h10(e10) != op2(e23,e23),
inference(paramod,[status(thm)],[c_424,c_292]) ).
cnf(c_3950,plain,
h10(e10) != e23,
inference(paramod,[status(thm)],[c_360,c_4161]) ).
cnf(c_4162,plain,
( op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_366,c_120]) ).
cnf(c_4163,plain,
( op2(e23,e23) = e22
| op2(e22,e23) = e22
| h3(e11) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_384,c_4162]) ).
cnf(c_4164,plain,
( op2(e23,e23) = e22
| e20 = e22
| h3(e11) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_364,c_4163]) ).
cnf(c_4165,plain,
( e23 = e22
| e20 = e22
| h3(e11) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_360,c_4164]) ).
cnf(c_4166,plain,
( e22 = e23
| e20 = e22
| h3(e11) = e22
| e21 = e22 ),
inference(copy,[status(thm)],[c_4165]) ).
cnf(c_4167,plain,
( e22 = e23
| e20 = e22
| h3(e11) = e22 ),
inference(resolve,[status(thm)],[c_316,c_4166]) ).
cnf(c_4168,plain,
( e22 = e23
| h3(e11) = e22 ),
inference(resolve,[status(thm)],[c_312,c_4167]) ).
cnf(c_3952,plain,
h3(e11) = e22,
inference(resolve,[status(thm)],[c_320,c_4168]) ).
cnf(c_3956,plain,
op1(e12,e11) != e10,
inference(paramod,[status(thm)],[c_361,c_197]) ).
cnf(c_3957,plain,
op1(e10,e12) != e11,
inference(paramod,[status(thm)],[c_363,c_177]) ).
cnf(c_4169,plain,
h8(e10) != op2(e22,e23),
inference(paramod,[status(thm)],[c_412,c_285]) ).
cnf(c_3958,plain,
h8(e10) != e20,
inference(paramod,[status(thm)],[c_364,c_4169]) ).
cnf(c_4170,plain,
h2(e10) != op2(e20,e23),
inference(paramod,[status(thm)],[c_376,c_265]) ).
cnf(c_3959,plain,
h2(e10) != e21,
inference(paramod,[status(thm)],[c_366,c_4170]) ).
cnf(c_4171,plain,
( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| h2(e10) = e20 ),
inference(paramod,[status(thm)],[c_376,c_77]) ).
cnf(c_4172,plain,
( op2(e20,e22) = e23
| op2(e20,e22) = e22
| h2(e10) = e21
| h2(e10) = e20 ),
inference(paramod,[status(thm)],[c_376,c_4171]) ).
cnf(c_4173,plain,
( op2(e20,e22) = e23
| h2(e10) = e22
| h2(e10) = e21
| h2(e10) = e20 ),
inference(paramod,[status(thm)],[c_376,c_4172]) ).
cnf(c_4174,plain,
( h2(e10) = e23
| h2(e10) = e22
| h2(e10) = e21
| h2(e10) = e20 ),
inference(paramod,[status(thm)],[c_376,c_4173]) ).
cnf(c_4175,plain,
( h2(e10) = e23
| h2(e10) = e22
| h2(e10) = e21 ),
inference(resolve,[status(thm)],[c_3916,c_4174]) ).
cnf(c_4176,plain,
( h2(e10) = e23
| h2(e10) = e22 ),
inference(resolve,[status(thm)],[c_3959,c_4175]) ).
cnf(c_3966,plain,
h2(e10) = e23,
inference(resolve,[status(thm)],[c_3942,c_4176]) ).
cnf(c_4177,plain,
h4(e10) != op2(e21,e23),
inference(paramod,[status(thm)],[c_388,c_270]) ).
cnf(c_4178,plain,
h4(e10) != h3(e11),
inference(paramod,[status(thm)],[c_384,c_4177]) ).
cnf(c_3967,plain,
h4(e10) != e22,
inference(paramod,[status(thm)],[c_3952,c_4178]) ).
cnf(c_4179,plain,
( op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e21
| h4(e10) = e20 ),
inference(paramod,[status(thm)],[c_388,c_79]) ).
cnf(c_4180,plain,
( op2(e21,e20) = e23
| op2(e21,e20) = e22
| h4(e10) = e21
| h4(e10) = e20 ),
inference(paramod,[status(thm)],[c_388,c_4179]) ).
cnf(c_4181,plain,
( op2(e21,e20) = e23
| h4(e10) = e22
| h4(e10) = e21
| h4(e10) = e20 ),
inference(paramod,[status(thm)],[c_388,c_4180]) ).
cnf(c_4182,plain,
( h4(e10) = e23
| h4(e10) = e22
| h4(e10) = e21
| h4(e10) = e20 ),
inference(paramod,[status(thm)],[c_388,c_4181]) ).
cnf(c_4183,plain,
( h4(e10) = e23
| h4(e10) = e22
| h4(e10) = e21 ),
inference(resolve,[status(thm)],[c_3920,c_4182]) ).
cnf(c_4184,plain,
( h4(e10) = e23
| h4(e10) = e22 ),
inference(resolve,[status(thm)],[c_3928,c_4183]) ).
cnf(c_3970,plain,
h4(e10) = e23,
inference(resolve,[status(thm)],[c_3967,c_4184]) ).
cnf(c_4185,plain,
h7(e10) != op2(e23,e20),
inference(paramod,[status(thm)],[c_406,c_221]) ).
cnf(c_4186,plain,
e21 != op2(e23,e20),
inference(paramod,[status(thm)],[c_3946,c_4185]) ).
cnf(c_4187,plain,
e21 != h10(e10),
inference(paramod,[status(thm)],[c_424,c_4186]) ).
cnf(c_3973,plain,
h10(e10) != e21,
inference(copy,[status(thm)],[c_4187]) ).
cnf(c_4188,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| h8(e10) = e20 ),
inference(paramod,[status(thm)],[c_412,c_84]) ).
cnf(c_4189,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22
| h8(e10) = e21
| h8(e10) = e20 ),
inference(paramod,[status(thm)],[c_412,c_4188]) ).
cnf(c_4190,plain,
( op2(e22,e21) = e23
| h8(e10) = e22
| h8(e10) = e21
| h8(e10) = e20 ),
inference(paramod,[status(thm)],[c_412,c_4189]) ).
cnf(c_4191,plain,
( h8(e10) = e23
| h8(e10) = e22
| h8(e10) = e21
| h8(e10) = e20 ),
inference(paramod,[status(thm)],[c_412,c_4190]) ).
cnf(c_4192,plain,
( h8(e10) = e23
| h8(e10) = e22
| h8(e10) = e21 ),
inference(resolve,[status(thm)],[c_3958,c_4191]) ).
cnf(c_4193,plain,
( h8(e10) = e23
| h8(e10) = e22 ),
inference(resolve,[status(thm)],[c_3930,c_4192]) ).
cnf(c_3975,plain,
h8(e10) = e23,
inference(resolve,[status(thm)],[c_3938,c_4193]) ).
cnf(c_4194,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| h10(e10) = e20 ),
inference(paramod,[status(thm)],[c_424,c_87]) ).
cnf(c_4195,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| h10(e10) = e21
| h10(e10) = e20 ),
inference(paramod,[status(thm)],[c_424,c_4194]) ).
cnf(c_4196,plain,
( op2(e23,e20) = e23
| h10(e10) = e22
| h10(e10) = e21
| h10(e10) = e20 ),
inference(paramod,[status(thm)],[c_424,c_4195]) ).
cnf(c_4197,plain,
( h10(e10) = e23
| h10(e10) = e22
| h10(e10) = e21
| h10(e10) = e20 ),
inference(paramod,[status(thm)],[c_424,c_4196]) ).
cnf(c_4198,plain,
( h10(e10) = e23
| h10(e10) = e22
| h10(e10) = e21 ),
inference(resolve,[status(thm)],[c_3918,c_4197]) ).
cnf(c_4199,plain,
( h10(e10) = e23
| h10(e10) = e22 ),
inference(resolve,[status(thm)],[c_3973,c_4198]) ).
cnf(c_3978,plain,
h10(e10) = e22,
inference(resolve,[status(thm)],[c_3950,c_4199]) ).
cnf(c_4200,plain,
( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11 ),
inference(resolve,[status(thm)],[c_3876,c_29]) ).
cnf(c_4201,plain,
( op1(e10,e12) = e13
| op1(e10,e12) = e12 ),
inference(resolve,[status(thm)],[c_3957,c_4200]) ).
cnf(c_3982,plain,
op1(e10,e12) = e13,
inference(resolve,[status(thm)],[c_3902,c_4201]) ).
cnf(c_4202,plain,
( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11 ),
inference(resolve,[status(thm)],[c_3956,c_36]) ).
cnf(c_4203,plain,
( op1(e12,e11) = e13
| op1(e12,e11) = e12 ),
inference(resolve,[status(thm)],[c_3890,c_4202]) ).
cnf(c_3988,plain,
op1(e12,e11) = e13,
inference(resolve,[status(thm)],[c_3898,c_4203]) ).
cnf(c_4204,plain,
( op1(e13,e10) = e12
| e11 = e12
| op1(e11,e10) = e12 ),
inference(paramod,[status(thm)],[c_3906,c_3883]) ).
cnf(c_3990,plain,
( op1(e13,e10) = e12
| op1(e11,e10) = e12 ),
inference(resolve,[status(thm)],[c_305,c_4204]) ).
cnf(c_4205,plain,
( e13 = e12
| op1(e10,e11) = e12 ),
inference(paramod,[status(thm)],[c_3982,c_3884]) ).
cnf(c_4206,plain,
( e12 = e13
| op1(e10,e11) = e12 ),
inference(copy,[status(thm)],[c_4205]) ).
cnf(c_3992,plain,
op1(e10,e11) = e12,
inference(resolve,[status(thm)],[c_309,c_4206]) ).
cnf(c_4207,plain,
( op1(e13,e10) = e13
| e11 = e13
| op1(e11,e10) = e13 ),
inference(paramod,[status(thm)],[c_3906,c_3881]) ).
cnf(c_4208,plain,
( op1(e13,e10) = e13
| op1(e11,e10) = e13 ),
inference(resolve,[status(thm)],[c_307,c_4207]) ).
cnf(c_3993,plain,
op1(e11,e10) = e13,
inference(resolve,[status(thm)],[c_3910,c_4208]) ).
cnf(c_4209,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(e23,h2(e10)) != h2(e10) ),
inference(paramod,[status(thm)],[c_3966,c_922]) ).
cnf(c_4210,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(e23,e23) != h2(e10) ),
inference(paramod,[status(thm)],[c_3966,c_4209]) ).
cnf(c_4211,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| e23 != h2(e10) ),
inference(paramod,[status(thm)],[c_360,c_4210]) ).
cnf(c_4212,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3966,c_4211]) ).
cnf(c_4213,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(e23,h2(e11)) != h2(op1(e10,e11))
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3966,c_4212]) ).
cnf(c_4214,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(e23,h2(e11)) != h2(e12)
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3992,c_4213]) ).
cnf(c_4215,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e12)) != op2(h2(e10),e20)
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_373,c_4214]) ).
cnf(c_4216,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| h2(e13) != op2(h2(e10),e20)
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3982,c_4215]) ).
cnf(c_4217,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| e22 != op2(h2(e10),e20)
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_374,c_4216]) ).
cnf(c_4218,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| e22 != op2(e23,e20)
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3966,c_4217]) ).
cnf(c_4219,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| e22 != h10(e10)
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_424,c_4218]) ).
cnf(c_4220,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3978,c_4219]) ).
cnf(c_4221,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != h2(op1(e11,e10))
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3966,c_4220]) ).
cnf(c_4222,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != h2(e13)
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3993,c_4221]) ).
cnf(c_4223,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_374,c_4222]) ).
cnf(c_4224,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| h2(e12) != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3912,c_4223]) ).
cnf(c_4225,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(op1(e12,e10)) != op2(e20,h2(e10))
| e20 != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_373,c_4224]) ).
cnf(c_4226,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(e11) != op2(e20,h2(e10))
| e20 != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3906,c_4225]) ).
cnf(c_4227,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(e11) != op2(e20,e23)
| e20 != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3966,c_4226]) ).
cnf(c_4228,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(op1(e12,e11)) != op2(e20,h2(e11))
| h2(e11) != e21
| e20 != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_366,c_4227]) ).
cnf(c_4229,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| h2(e13) != op2(e20,h2(e11))
| h2(e11) != e21
| e20 != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3988,c_4228]) ).
cnf(c_4230,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,h2(e10))
| e22 != op2(e20,h2(e11))
| h2(e11) != e21
| e20 != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_374,c_4229]) ).
cnf(c_4231,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != op2(e22,e23)
| e22 != op2(e20,h2(e11))
| h2(e11) != e21
| e20 != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3966,c_4230]) ).
cnf(c_4232,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != h7(e10)
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| e22 != op2(e20,h2(e11))
| h2(e11) != e21
| e20 != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_364,c_4231]) ).
cnf(c_4233,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| e22 != op2(e20,h2(e11))
| h2(e11) != e21
| e20 != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3946,c_4232]) ).
cnf(c_4234,negated_conjecture,
( e23 != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| e22 != op2(e20,h2(e11))
| h2(e11) != e21
| e20 != op2(h2(e11),e22)
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_3966,c_4233]) ).
cnf(c_4235,negated_conjecture,
( e23 != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| e22 != op2(e20,h2(e11))
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(copy,[status(thm)],[c_4234]) ).
cnf(c_4236,negated_conjecture,
( e23 != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20
| e23 != e23 ),
inference(copy,[status(thm)],[c_4235]) ).
cnf(c_4237,negated_conjecture,
( e23 != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e22 != e22
| op2(e23,h2(e11)) != e20 ),
inference(copy,[status(thm)],[c_4236]) ).
cnf(c_4238,negated_conjecture,
( e23 != e23
| h2(e11) != e21
| h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| op2(e23,h2(e11)) != e20 ),
inference(copy,[status(thm)],[c_4237]) ).
cnf(c_4239,negated_conjecture,
( h2(e11) != e21
| h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| op2(e23,h2(e11)) != e20 ),
inference(copy,[status(thm)],[c_4238]) ).
cnf(c_4019,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| op2(e23,h2(e11)) != e20 ),
inference(copy,[status(thm)],[c_4239]) ).
cnf(c_4240,plain,
( e12 = e10
| op1(e11,e12) = e10 ),
inference(paramod,[status(thm)],[c_3912,c_3897]) ).
cnf(c_4241,plain,
( e10 = e12
| op1(e11,e12) = e10 ),
inference(copy,[status(thm)],[c_4240]) ).
cnf(c_4025,plain,
op1(e11,e12) = e10,
inference(resolve,[status(thm)],[c_301,c_4241]) ).
cnf(c_4242,plain,
( e23 = e22
| h1(e10) = e22 ),
inference(paramod,[status(thm)],[c_3966,c_3924]) ).
cnf(c_4243,plain,
( e22 = e23
| h1(e10) = e22 ),
inference(copy,[status(thm)],[c_4242]) ).
cnf(c_4027,plain,
h1(e10) = e22,
inference(resolve,[status(thm)],[c_320,c_4243]) ).
cnf(c_4244,plain,
( e22 = e20
| h5(e10) = e20 ),
inference(paramod,[status(thm)],[c_3952,c_3937]) ).
cnf(c_4245,plain,
( e20 = e22
| h5(e10) = e20 ),
inference(copy,[status(thm)],[c_4244]) ).
cnf(c_4030,plain,
h5(e10) = e20,
inference(resolve,[status(thm)],[c_312,c_4245]) ).
cnf(c_4033,plain,
op2(e21,e23) = e22,
inference(paramod,[status(thm)],[c_3952,c_384]) ).
cnf(c_4246,plain,
( op1(e13,e11) = e10
| e13 = e10 ),
inference(paramod,[status(thm)],[c_3988,c_3896]) ).
cnf(c_4247,plain,
( op1(e13,e11) = e10
| e10 = e13 ),
inference(copy,[status(thm)],[c_4246]) ).
cnf(c_4034,plain,
op1(e13,e11) = e10,
inference(resolve,[status(thm)],[c_303,c_4247]) ).
cnf(c_4248,plain,
( op1(e13,e12) = e11
| e13 = e11 ),
inference(paramod,[status(thm)],[c_3982,c_3905]) ).
cnf(c_4249,plain,
( op1(e13,e12) = e11
| e11 = e13 ),
inference(copy,[status(thm)],[c_4248]) ).
cnf(c_4035,plain,
op1(e13,e12) = e11,
inference(resolve,[status(thm)],[c_307,c_4249]) ).
cnf(c_4250,plain,
( h11(e10) = e20
| e23 = e20 ),
inference(paramod,[status(thm)],[c_3975,c_3936]) ).
cnf(c_4251,plain,
( h11(e10) = e20
| e20 = e23 ),
inference(copy,[status(thm)],[c_4250]) ).
cnf(c_4036,plain,
h11(e10) = e20,
inference(resolve,[status(thm)],[c_314,c_4251]) ).
cnf(c_4252,plain,
( h12(e10) = e21
| e23 = e21 ),
inference(paramod,[status(thm)],[c_3966,c_3945]) ).
cnf(c_4253,plain,
( h12(e10) = e21
| e21 = e23 ),
inference(copy,[status(thm)],[c_4252]) ).
cnf(c_4037,plain,
h12(e10) = e21,
inference(resolve,[status(thm)],[c_318,c_4253]) ).
cnf(c_4254,plain,
op2(e23,e22) = h2(e11),
inference(paramod,[status(thm)],[c_3966,c_378]) ).
cnf(c_4255,plain,
h12(e10) = h2(e11),
inference(paramod,[status(thm)],[c_436,c_4254]) ).
cnf(c_4256,plain,
e21 = h2(e11),
inference(paramod,[status(thm)],[c_4037,c_4255]) ).
cnf(c_4038,plain,
h2(e11) = e21,
inference(copy,[status(thm)],[c_4256]) ).
cnf(c_4041,plain,
op2(e21,e20) = e23,
inference(paramod,[status(thm)],[c_3970,c_388]) ).
cnf(c_4043,plain,
op2(e22,e21) = e23,
inference(paramod,[status(thm)],[c_3975,c_412]) ).
cnf(c_4257,plain,
( op1(e13,e10) = e12
| e13 = e12 ),
inference(paramod,[status(thm)],[c_3993,c_3990]) ).
cnf(c_4258,plain,
( op1(e13,e10) = e12
| e12 = e13 ),
inference(copy,[status(thm)],[c_4257]) ).
cnf(c_4046,plain,
op1(e13,e10) = e12,
inference(resolve,[status(thm)],[c_309,c_4258]) ).
cnf(c_4259,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| op2(e23,e21) != e20 ),
inference(paramod,[status(thm)],[c_4038,c_4019]) ).
cnf(c_4260,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| h11(e10) != e20 ),
inference(paramod,[status(thm)],[c_430,c_4259]) ).
cnf(c_4261,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(h2(e11),e23) != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4036,c_4260]) ).
cnf(c_4262,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| op2(e21,e23) != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4038,c_4261]) ).
cnf(c_4263,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(h2(e11),h2(e11)) != h2(e11)
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4033,c_4262]) ).
cnf(c_4264,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(e21,h2(e11)) != h2(e11)
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4038,c_4263]) ).
cnf(c_4265,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| op2(e21,e21) != h2(e11)
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4038,c_4264]) ).
cnf(c_4266,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| e21 != h2(e11)
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_358,c_4265]) ).
cnf(c_4267,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(op1(e11,e12)) != op2(h2(e11),e20)
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4038,c_4266]) ).
cnf(c_4268,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| h2(e10) != op2(h2(e11),e20)
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4025,c_4267]) ).
cnf(c_4269,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| e23 != op2(h2(e11),e20)
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_3966,c_4268]) ).
cnf(c_4270,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| e23 != op2(e21,e20)
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4038,c_4269]) ).
cnf(c_4271,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(h2(e11),e22) != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4041,c_4270]) ).
cnf(c_4272,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| op2(e21,e22) != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4038,c_4271]) ).
cnf(c_4273,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| h5(e10) != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_394,c_4272]) ).
cnf(c_4274,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| h2(e11) != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4030,c_4273]) ).
cnf(c_4275,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,h2(e11)) != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4038,c_4274]) ).
cnf(c_4276,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| op2(e20,e21) != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4038,c_4275]) ).
cnf(c_4277,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| h1(e10) != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_370,c_4276]) ).
cnf(c_4278,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(op1(e13,e10)) != e20
| e22 != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4027,c_4277]) ).
cnf(c_4279,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| h2(e12) != e20
| e22 != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4046,c_4278]) ).
cnf(c_4280,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(op1(e13,e11)) != op2(e22,h2(e11))
| e20 != e20
| e22 != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_373,c_4279]) ).
cnf(c_4281,negated_conjecture,
( h2(op1(e13,e12)) != e21
| h2(e10) != op2(e22,h2(e11))
| e20 != e20
| e22 != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4034,c_4280]) ).
cnf(c_4282,negated_conjecture,
( h2(op1(e13,e12)) != e21
| e23 != op2(e22,h2(e11))
| e20 != e20
| e22 != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_3966,c_4281]) ).
cnf(c_4283,negated_conjecture,
( h2(op1(e13,e12)) != e21
| e23 != op2(e22,e21)
| e20 != e20
| e22 != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4038,c_4282]) ).
cnf(c_4284,negated_conjecture,
( h2(op1(e13,e12)) != e21
| e23 != e23
| e20 != e20
| e22 != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4043,c_4283]) ).
cnf(c_4285,negated_conjecture,
( h2(e11) != e21
| e23 != e23
| e20 != e20
| e22 != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4035,c_4284]) ).
cnf(c_4286,negated_conjecture,
( e21 != e21
| e23 != e23
| e20 != e20
| e22 != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4038,c_4285]) ).
cnf(c_4287,negated_conjecture,
( e21 != e21
| e23 != e23
| e20 != e20
| e22 != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21
| e22 != e22 ),
inference(copy,[status(thm)],[c_4286]) ).
cnf(c_4288,negated_conjecture,
( e21 != e21
| e23 != e23
| e20 != e20
| e22 != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e21 != e21 ),
inference(copy,[status(thm)],[c_4287]) ).
cnf(c_4289,negated_conjecture,
( e21 != e21
| e23 != e23
| e20 != e20
| e22 != e22
| e21 != e21
| e20 != e20
| e23 != e23 ),
inference(copy,[status(thm)],[c_4288]) ).
cnf(c_4290,negated_conjecture,
( e21 != e21
| e23 != e23
| e20 != e20
| e22 != e22
| e21 != e21
| e20 != e20 ),
inference(copy,[status(thm)],[c_4289]) ).
cnf(c_4291,negated_conjecture,
( e21 != e21
| e23 != e23
| e20 != e20
| e22 != e22
| e21 != e21 ),
inference(copy,[status(thm)],[c_4290]) ).
cnf(c_4292,negated_conjecture,
( e21 != e21
| e23 != e23
| e20 != e20
| e22 != e22 ),
inference(copy,[status(thm)],[c_4291]) ).
cnf(c_4293,negated_conjecture,
( e21 != e21
| e23 != e23
| e20 != e20 ),
inference(copy,[status(thm)],[c_4292]) ).
cnf(c_4294,negated_conjecture,
( e21 != e21
| e23 != e23 ),
inference(copy,[status(thm)],[c_4293]) ).
cnf(c_4295,negated_conjecture,
e21 != e21,
inference(copy,[status(thm)],[c_4294]) ).
cnf(c_4048,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_4295]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG113+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.18/0.44 % Computer : n017.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sat Sep 26 21:06:18 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.45 % Process 1638371 was started by sandbox on n017,
% 0.18/0.45 % Sat Sep 26 21:06:18 2026
% 0.18/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 52.47/53.91
% 52.47/53.91 % From the command line: assign(max_seconds, 300).
% 58.58/55.82
% 58.58/55.82 % SZS status Theorem for theBenchmark
% 58.58/55.82
% 58.58/55.82 % Proof 1 at 0.74 (+ 0.07) seconds.
% 58.58/55.82 % Length of proof is 209.
% 58.58/55.82 % Level of proof is 8.
% 58.58/55.82 % Maximum clause weight is 129.000.
% 58.58/55.82 % Given clauses 0.
% 58.58/55.82
% 58.58/55.82 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------