%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG038+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 : n019.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:19 AM UTC 2026
% Result : Theorem 33.91s 14.65s
% Output : CNFRefutation 33.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 147
% Number of leaves : 12
% Syntax : Number of formulae : 505 ( 138 unt; 0 def)
% Number of atoms : 3585 (3584 equ)
% Maximal formula atoms : 128 ( 7 avg)
% Number of connectives : 5433 (2353 ~;2739 |; 341 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 7 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax2,axiom,
( ( unit1 = e13
| unit1 = e12
| unit1 = e11
| unit1 = e10 )
& op1(e13,unit1) = e13
& op1(unit1,e13) = e13
& op1(e12,unit1) = e12
& op1(unit1,e12) = e12
& op1(e11,unit1) = e11
& op1(unit1,e11) = e11
& op1(e10,unit1) = e10
& op1(unit1,e10) = e10 ),
file('theBenchmark.p',ax2) ).
fof(ax3,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',ax3) ).
fof(ax5,axiom,
( ( unit2 = e23
| unit2 = e22
| unit2 = e21
| unit2 = e20 )
& op2(e23,unit2) = e23
& op2(unit2,e23) = e23
& op2(e22,unit2) = e22
& op2(unit2,e22) = e22
& op2(e21,unit2) = e21
& op2(unit2,e21) = e21
& op2(e20,unit2) = e20
& op2(unit2,e20) = e20 ),
file('theBenchmark.p',ax5) ).
fof(ax6,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',ax6) ).
fof(ax7,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',ax7) ).
fof(ax8,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',ax8) ).
fof(ax9,axiom,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('theBenchmark.p',ax9) ).
fof(ax10,axiom,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('theBenchmark.p',ax10) ).
fof(ax14,axiom,
( e13 = op1(e11,e11)
& e12 = op1(e11,op1(e11,e11))
& e10 = op1(e11,op1(e11,op1(e11,e11))) ),
file('theBenchmark.p',ax14) ).
fof(ax15,axiom,
( e23 = op2(e21,e21)
& e22 = op2(e21,op2(e21,e21))
& e20 = op2(e21,op2(e21,op2(e21,e21))) ),
file('theBenchmark.p',ax15) ).
fof(ax17,axiom,
( h2(e13) = op2(e21,e21)
& h2(e12) = op2(e21,op2(e21,e21))
& h2(e10) = op2(e21,op2(e21,op2(e21,e21)))
& h2(e11) = e21 ),
file('theBenchmark.p',ax17) ).
fof(co1,conjecture,
( ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ( ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_37,plain,
op1(unit1,e10) = e10,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_38,plain,
op1(e10,unit1) = e10,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_39,plain,
op1(unit1,e11) = e11,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_40,plain,
op1(e11,unit1) = e11,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_41,plain,
op1(unit1,e12) = e12,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_42,plain,
op1(e12,unit1) = e12,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_43,plain,
op1(unit1,e13) = e13,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_44,plain,
op1(e13,unit1) = e13,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_45,plain,
( unit1 = e13
| unit1 = e12
| unit1 = e11
| unit1 = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_48,plain,
( op1(e10,e13) = e11
| op1(e10,e12) = e11
| op1(e10,e11) = e11
| op1(e10,e10) = e11 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_52,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_53,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| op1(e10,e10) = e13 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_56,plain,
( op1(e11,e13) = e11
| op1(e11,e12) = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_62,plain,
( op1(e12,e13) = e10
| op1(e12,e12) = e10
| op1(e12,e11) = e10
| op1(e12,e10) = e10 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_64,plain,
( op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_65,plain,
( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_68,plain,
( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_69,plain,
( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| op1(e10,e12) = e13 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_70,plain,
( op1(e13,e13) = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_74,plain,
( op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_94,plain,
op2(unit2,e20) = e20,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_95,plain,
op2(e20,unit2) = e20,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_96,plain,
op2(unit2,e21) = e21,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_97,plain,
op2(e21,unit2) = e21,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_98,plain,
op2(unit2,e22) = e22,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_99,plain,
op2(e22,unit2) = e22,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_100,plain,
op2(unit2,e23) = e23,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_101,plain,
op2(e23,unit2) = e23,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_102,plain,
( unit2 = e23
| unit2 = e22
| unit2 = e21
| unit2 = e20 ),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_105,plain,
( op2(e20,e23) = e21
| op2(e20,e22) = e21
| op2(e20,e21) = e21
| op2(e20,e20) = e21 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_109,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_110,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| op2(e20,e20) = e23 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_113,plain,
( op2(e21,e23) = e21
| op2(e21,e22) = e21
| op2(e21,e21) = e21
| op2(e21,e20) = e21 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_119,plain,
( op2(e22,e23) = e20
| op2(e22,e22) = e20
| op2(e22,e21) = e20
| op2(e22,e20) = e20 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_121,plain,
( op2(e22,e23) = e21
| op2(e22,e22) = e21
| op2(e22,e21) = e21
| op2(e22,e20) = e21 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_122,plain,
( op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_125,plain,
( op2(e22,e23) = e23
| op2(e22,e22) = e23
| op2(e22,e21) = e23
| op2(e22,e20) = e23 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_126,plain,
( op2(e23,e22) = e23
| op2(e22,e22) = e23
| op2(e21,e22) = e23
| op2(e20,e22) = e23 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_127,plain,
( op2(e23,e23) = e20
| op2(e23,e22) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_131,plain,
( op2(e23,e23) = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_135,plain,
op1(e11,e10) != op1(e10,e10),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_136,plain,
op1(e10,e10) != op1(e11,e10),
inference(copy,[status(thm)],[c_135]) ).
cnf(c_139,plain,
op1(e12,e10) != op1(e11,e10),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_142,plain,
op1(e11,e11) != op1(e10,e11),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_143,plain,
op1(e10,e11) != op1(e11,e11),
inference(copy,[status(thm)],[c_142]) ).
cnf(c_144,plain,
op1(e12,e11) != op1(e10,e11),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_146,plain,
op1(e12,e11) != op1(e11,e11),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_149,plain,
op1(e11,e12) != op1(e10,e12),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_150,plain,
op1(e10,e12) != op1(e11,e12),
inference(copy,[status(thm)],[c_149]) ).
cnf(c_152,plain,
op1(e13,e12) != op1(e10,e12),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_153,plain,
op1(e12,e12) != op1(e11,e12),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_154,plain,
op1(e13,e12) != op1(e11,e12),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_158,plain,
op1(e12,e13) != op1(e10,e13),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_161,plain,
op1(e13,e13) != op1(e11,e13),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_170,plain,
op1(e11,e11) != op1(e11,e10),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_171,plain,
op1(e11,e10) != op1(e11,e11),
inference(copy,[status(thm)],[c_170]) ).
cnf(c_186,plain,
op1(e13,e12) != op1(e13,e10),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_191,plain,
op2(e21,e20) != op2(e20,e20),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_192,plain,
op2(e20,e20) != op2(e21,e20),
inference(copy,[status(thm)],[c_191]) ).
cnf(c_195,plain,
op2(e22,e20) != op2(e21,e20),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_198,plain,
op2(e21,e21) != op2(e20,e21),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_199,plain,
op2(e20,e21) != op2(e21,e21),
inference(copy,[status(thm)],[c_198]) ).
cnf(c_200,plain,
op2(e22,e21) != op2(e20,e21),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_202,plain,
op2(e22,e21) != op2(e21,e21),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_205,plain,
op2(e21,e22) != op2(e20,e22),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_206,plain,
op2(e20,e22) != op2(e21,e22),
inference(copy,[status(thm)],[c_205]) ).
cnf(c_208,plain,
op2(e23,e22) != op2(e20,e22),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_209,plain,
op2(e22,e22) != op2(e21,e22),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_210,plain,
op2(e23,e22) != op2(e21,e22),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_214,plain,
op2(e22,e23) != op2(e20,e23),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_217,plain,
op2(e23,e23) != op2(e21,e23),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_226,plain,
op2(e21,e21) != op2(e21,e20),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_227,plain,
op2(e21,e20) != op2(e21,e21),
inference(copy,[status(thm)],[c_226]) ).
cnf(c_242,plain,
op2(e23,e22) != op2(e23,e20),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_247,plain,
e11 != e10,
inference(clausify,[status(thm)],[ax9]) ).
cnf(c_248,plain,
e10 != e11,
inference(copy,[status(thm)],[c_247]) ).
cnf(c_249,plain,
e12 != e10,
inference(clausify,[status(thm)],[ax9]) ).
cnf(c_250,plain,
e13 != e10,
inference(clausify,[status(thm)],[ax9]) ).
cnf(c_251,plain,
e12 != e11,
inference(clausify,[status(thm)],[ax9]) ).
cnf(c_252,plain,
e13 != e11,
inference(clausify,[status(thm)],[ax9]) ).
cnf(c_253,plain,
e13 != e12,
inference(clausify,[status(thm)],[ax9]) ).
cnf(c_254,plain,
e21 != e20,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_255,plain,
e20 != e21,
inference(copy,[status(thm)],[c_254]) ).
cnf(c_256,plain,
e22 != e20,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_257,plain,
e23 != e20,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_258,plain,
e22 != e21,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_259,plain,
e23 != e21,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_260,plain,
e23 != e22,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_298,plain,
op1(e11,op1(e11,op1(e11,e11))) = e10,
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_299,plain,
op1(e11,op1(e11,e11)) = e12,
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_300,plain,
op1(e11,e11) = e13,
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_301,plain,
op2(e21,op2(e21,op2(e21,e21))) = e20,
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_302,plain,
op2(e21,op2(e21,e21)) = e22,
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_303,plain,
op2(e21,e21) = e23,
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_308,plain,
h2(e11) = e21,
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_309,plain,
h2(e10) = op2(e21,op2(e21,op2(e21,e21))),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_310,plain,
h2(e10) = op2(e21,op2(e21,e23)),
inference(paramod,[status(thm)],[c_303,c_309]) ).
cnf(c_311,plain,
h2(e12) = op2(e21,op2(e21,e21)),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_312,plain,
h2(e12) = op2(e21,e23),
inference(paramod,[status(thm)],[c_303,c_311]) ).
cnf(c_313,plain,
h2(e13) = op2(e21,e21),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_314,plain,
h2(e13) = e23,
inference(paramod,[status(thm)],[c_303,c_313]) ).
cnf(c_671,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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)) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_2914,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,op2(e21,e23)),h2(e10)) ),
inference(paramod,[status(thm)],[c_310,c_671]) ).
cnf(c_2915,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_310,c_2914]) ).
cnf(c_2916,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,op2(e21,e23)),h2(e11))
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_310,c_2915]) ).
cnf(c_2917,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_308,c_2916]) ).
cnf(c_2918,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,op2(e21,e23)),h2(e12))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_310,c_2917]) ).
cnf(c_2919,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_312,c_2918]) ).
cnf(c_2920,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,op2(e21,e23)),h2(e13))
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_310,c_2919]) ).
cnf(c_2921,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_314,c_2920]) ).
cnf(c_2922,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(e21,h2(e10))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_308,c_2921]) ).
cnf(c_2923,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_310,c_2922]) ).
cnf(c_2924,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(e13) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_300,c_2923]) ).
cnf(c_2925,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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))
| e23 != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_314,c_2924]) ).
cnf(c_2926,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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))
| e23 != op2(e21,h2(e11))
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_308,c_2925]) ).
cnf(c_2927,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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))
| e23 != op2(e21,e21)
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_308,c_2926]) ).
cnf(c_2928,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_303,c_2927]) ).
cnf(c_2929,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(e21,h2(e12))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_308,c_2928]) ).
cnf(c_2930,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_312,c_2929]) ).
cnf(c_2931,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(e21,h2(e13))
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_308,c_2930]) ).
cnf(c_2932,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_314,c_2931]) ).
cnf(c_2933,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,e23),h2(e10))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_312,c_2932]) ).
cnf(c_2934,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_310,c_2933]) ).
cnf(c_2935,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,e23),h2(e11))
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_312,c_2934]) ).
cnf(c_2936,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_308,c_2935]) ).
cnf(c_2937,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,e23),h2(e12))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_312,c_2936]) ).
cnf(c_2938,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_312,c_2937]) ).
cnf(c_2939,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,e23),h2(e13))
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_312,c_2938]) ).
cnf(c_2940,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_314,c_2939]) ).
cnf(c_2941,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(e23,h2(e10))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_314,c_2940]) ).
cnf(c_2942,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_310,c_2941]) ).
cnf(c_2943,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(e23,h2(e11))
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_314,c_2942]) ).
cnf(c_2944,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| 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(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_308,c_2943]) ).
cnf(c_2945,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| h2(e10) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(e23,h2(e12))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_314,c_2944]) ).
cnf(c_2946,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| h2(e10) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_312,c_2945]) ).
cnf(c_2947,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| h2(e10) != e20
| h2(op1(e13,e13)) != op2(e23,h2(e13))
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_314,c_2946]) ).
cnf(c_2948,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| h2(e10) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_314,c_2947]) ).
cnf(c_2949,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| h2(e11) != e21
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_310,c_2948]) ).
cnf(c_2950,negated_conjecture,
( h2(e13) != e23
| h2(e12) != e22
| e21 != e21
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_308,c_2949]) ).
cnf(c_2951,negated_conjecture,
( h2(e13) != e23
| op2(e21,e23) != e22
| e21 != e21
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_312,c_2950]) ).
cnf(c_2952,negated_conjecture,
( e23 != e23
| op2(e21,e23) != e22
| e21 != e21
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| e23 != e23
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_314,c_2951]) ).
cnf(c_2953,negated_conjecture,
( e23 != e23
| op2(e21,e23) != e22
| e21 != e21
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(copy,[status(thm)],[c_2952]) ).
cnf(c_2954,negated_conjecture,
( e23 != e23
| op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(copy,[status(thm)],[c_2953]) ).
cnf(c_672,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,op2(e21,e23)),op2(e21,op2(e21,e23))) ),
inference(copy,[status(thm)],[c_2954]) ).
cnf(c_1533,plain,
op1(e11,op1(e11,e13)) = e10,
inference(paramod,[status(thm)],[c_300,c_298]) ).
cnf(c_1534,plain,
op1(e11,e13) = e12,
inference(paramod,[status(thm)],[c_300,c_299]) ).
cnf(c_1537,plain,
op1(e11,e10) != e13,
inference(paramod,[status(thm)],[c_300,c_171]) ).
cnf(c_1539,plain,
op1(e12,e11) != e13,
inference(paramod,[status(thm)],[c_300,c_146]) ).
cnf(c_1540,plain,
op1(e10,e11) != e13,
inference(paramod,[status(thm)],[c_300,c_143]) ).
cnf(c_2955,plain,
( op1(e11,e13) = e11
| op1(e11,e12) = e11
| e13 = e11
| op1(e11,e10) = e11 ),
inference(paramod,[status(thm)],[c_300,c_56]) ).
cnf(c_2956,plain,
( e12 = e11
| op1(e11,e12) = e11
| e13 = e11
| op1(e11,e10) = e11 ),
inference(paramod,[status(thm)],[c_1534,c_2955]) ).
cnf(c_2957,plain,
( e12 = e11
| op1(e11,e12) = e11
| op1(e11,e10) = e11 ),
inference(resolve,[status(thm)],[c_252,c_2956]) ).
cnf(c_1543,plain,
( op1(e11,e12) = e11
| op1(e11,e10) = e11 ),
inference(resolve,[status(thm)],[c_251,c_2957]) ).
cnf(c_1546,plain,
op2(e21,op2(e21,e23)) = e20,
inference(paramod,[status(thm)],[c_303,c_301]) ).
cnf(c_1547,plain,
op2(e21,e23) = e22,
inference(paramod,[status(thm)],[c_303,c_302]) ).
cnf(c_1550,plain,
op2(e21,e20) != e23,
inference(paramod,[status(thm)],[c_303,c_227]) ).
cnf(c_1552,plain,
op2(e22,e21) != e23,
inference(paramod,[status(thm)],[c_303,c_202]) ).
cnf(c_1553,plain,
op2(e20,e21) != e23,
inference(paramod,[status(thm)],[c_303,c_199]) ).
cnf(c_2958,plain,
( op2(e21,e23) = e21
| op2(e21,e22) = e21
| e23 = e21
| op2(e21,e20) = e21 ),
inference(paramod,[status(thm)],[c_303,c_113]) ).
cnf(c_2959,plain,
( e22 = e21
| op2(e21,e22) = e21
| e23 = e21
| op2(e21,e20) = e21 ),
inference(paramod,[status(thm)],[c_1547,c_2958]) ).
cnf(c_2960,plain,
( e22 = e21
| op2(e21,e22) = e21
| op2(e21,e20) = e21 ),
inference(resolve,[status(thm)],[c_259,c_2959]) ).
cnf(c_1556,plain,
( op2(e21,e22) = e21
| op2(e21,e20) = e21 ),
inference(resolve,[status(thm)],[c_258,c_2960]) ).
cnf(c_1559,plain,
op1(e11,e12) = e10,
inference(paramod,[status(thm)],[c_1534,c_1533]) ).
cnf(c_2961,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,op2(e21,e23))) ),
inference(paramod,[status(thm)],[c_1547,c_672]) ).
cnf(c_2962,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,op2(e21,e23)),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2961]) ).
cnf(c_2963,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,op2(e21,e23)),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2962]) ).
cnf(c_2964,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),op2(e21,e23))
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2963]) ).
cnf(c_2965,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,op2(e21,e23)),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2964]) ).
cnf(c_2966,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| h2(op1(e11,e10)) != op2(e21,op2(e21,op2(e21,e23)))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2965]) ).
cnf(c_2967,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(op1(e11,e12)) != op2(e21,op2(e21,e23))
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2966]) ).
cnf(c_2968,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| h2(e10) != op2(e21,op2(e21,e23))
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1559,c_2967]) ).
cnf(c_2969,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| op2(e21,op2(e21,e23)) != op2(e21,op2(e21,e23))
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_310,c_2968]) ).
cnf(c_2970,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != op2(e21,op2(e21,e23))
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2969]) ).
cnf(c_2971,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2970]) ).
cnf(c_2972,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| h2(e12) != op2(e21,e23)
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1534,c_2971]) ).
cnf(c_2973,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| op2(e21,e23) != op2(e21,e23)
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_312,c_2972]) ).
cnf(c_2974,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| e22 != op2(e21,e23)
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2973]) ).
cnf(c_2975,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(op2(e21,e23),op2(e21,op2(e21,e23)))
| e22 != e22
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2974]) ).
cnf(c_2976,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,op2(e21,e23)))
| e22 != e22
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2975]) ).
cnf(c_2977,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(op2(e21,e23),e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2976]) ).
cnf(c_2978,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(op2(e21,e23),op2(e21,e23))
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2977]) ).
cnf(c_2979,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(e22,op2(e21,e23))
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2978]) ).
cnf(c_2980,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(op2(e21,e23),e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2979]) ).
cnf(c_2981,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,op2(e21,e23)))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2980]) ).
cnf(c_2982,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,op2(e21,e23))
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2981]) ).
cnf(c_2983,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,op2(e21,e23)) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2982]) ).
cnf(c_2984,negated_conjecture,
( op2(e21,e23) != e22
| op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2983]) ).
cnf(c_2985,negated_conjecture,
( e22 != e22
| op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| op2(e21,e22) != op2(e21,e22)
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1547,c_2984]) ).
cnf(c_2986,negated_conjecture,
( e22 != e22
| op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(copy,[status(thm)],[c_2985]) ).
cnf(c_2987,negated_conjecture,
( e22 != e22
| op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(copy,[status(thm)],[c_2986]) ).
cnf(c_1614,negated_conjecture,
( op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(copy,[status(thm)],[c_2987]) ).
cnf(c_1643,plain,
op1(e13,e13) != e12,
inference(paramod,[status(thm)],[c_1534,c_161]) ).
cnf(c_2988,plain,
( op1(e13,e12) = e13
| op1(e12,e12) = e13
| e10 = e13
| op1(e10,e12) = e13 ),
inference(paramod,[status(thm)],[c_1559,c_69]) ).
cnf(c_2989,plain,
( op1(e13,e12) = e13
| op1(e12,e12) = e13
| e13 = e10
| op1(e10,e12) = e13 ),
inference(copy,[status(thm)],[c_2988]) ).
cnf(c_1649,plain,
( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e10,e12) = e13 ),
inference(resolve,[status(thm)],[c_250,c_2989]) ).
cnf(c_1650,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e10,e10) = e13 ),
inference(resolve,[status(thm)],[c_1537,c_53]) ).
cnf(c_1654,plain,
( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e10) = e13 ),
inference(resolve,[status(thm)],[c_1539,c_68]) ).
cnf(c_1656,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e10) = e13 ),
inference(resolve,[status(thm)],[c_1540,c_52]) ).
cnf(c_1658,plain,
h2(e10) = op2(e21,e22),
inference(paramod,[status(thm)],[c_1547,c_310]) ).
cnf(c_1659,plain,
op2(e21,e22) = e20,
inference(paramod,[status(thm)],[c_1547,c_1546]) ).
cnf(c_1660,plain,
h2(e12) = e22,
inference(paramod,[status(thm)],[c_1547,c_312]) ).
cnf(c_1662,plain,
op2(e23,e23) != e22,
inference(paramod,[status(thm)],[c_1547,c_217]) ).
cnf(c_2990,plain,
( op2(e23,e22) = e23
| op2(e22,e22) = e23
| e20 = e23
| op2(e20,e22) = e23 ),
inference(paramod,[status(thm)],[c_1659,c_126]) ).
cnf(c_2991,plain,
( op2(e23,e22) = e23
| op2(e22,e22) = e23
| e23 = e20
| op2(e20,e22) = e23 ),
inference(copy,[status(thm)],[c_2990]) ).
cnf(c_1668,plain,
( op2(e23,e22) = e23
| op2(e22,e22) = e23
| op2(e20,e22) = e23 ),
inference(resolve,[status(thm)],[c_257,c_2991]) ).
cnf(c_1669,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e20,e20) = e23 ),
inference(resolve,[status(thm)],[c_1550,c_110]) ).
cnf(c_1673,plain,
( op2(e22,e23) = e23
| op2(e22,e22) = e23
| op2(e22,e20) = e23 ),
inference(resolve,[status(thm)],[c_1552,c_125]) ).
cnf(c_1675,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e20) = e23 ),
inference(resolve,[status(thm)],[c_1553,c_109]) ).
cnf(c_2992,plain,
( e10 = e11
| op1(e11,e10) = e11 ),
inference(paramod,[status(thm)],[c_1559,c_1543]) ).
cnf(c_1677,plain,
op1(e11,e10) = e11,
inference(resolve,[status(thm)],[c_248,c_2992]) ).
cnf(c_1678,plain,
op1(e13,e12) != e10,
inference(paramod,[status(thm)],[c_1559,c_154]) ).
cnf(c_1679,plain,
op1(e12,e12) != e10,
inference(paramod,[status(thm)],[c_1559,c_153]) ).
cnf(c_1680,plain,
op1(e10,e12) != e10,
inference(paramod,[status(thm)],[c_1559,c_150]) ).
cnf(c_2993,plain,
( op1(e13,e12) = e11
| op1(e12,e12) = e11
| e10 = e11
| op1(e10,e12) = e11 ),
inference(paramod,[status(thm)],[c_1559,c_65]) ).
cnf(c_1682,plain,
( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e10,e12) = e11 ),
inference(resolve,[status(thm)],[c_248,c_2993]) ).
cnf(c_1684,plain,
( op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 ),
inference(resolve,[status(thm)],[c_1643,c_74]) ).
cnf(c_1690,plain,
h2(e10) = e20,
inference(paramod,[status(thm)],[c_1659,c_1658]) ).
cnf(c_2994,negated_conjecture,
( op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(e20,op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1659,c_1614]) ).
cnf(c_2995,negated_conjecture,
( op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1659,c_2994]) ).
cnf(c_2996,negated_conjecture,
( op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1659,c_2995]) ).
cnf(c_2997,negated_conjecture,
( op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1659,c_2996]) ).
cnf(c_2998,negated_conjecture,
( op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h2(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1659,c_2997]) ).
cnf(c_2999,negated_conjecture,
( op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h2(e11) != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1677,c_2998]) ).
cnf(c_3000,negated_conjecture,
( op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e21 != op2(e21,op2(e21,e22))
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_308,c_2999]) ).
cnf(c_3001,negated_conjecture,
( op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e21 != op2(e21,e20)
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1659,c_3000]) ).
cnf(c_3002,negated_conjecture,
( op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| e21 != op2(e21,e20)
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1659,c_3001]) ).
cnf(c_3003,negated_conjecture,
( op2(e21,e22) != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| e21 != op2(e21,e20)
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1659,c_3002]) ).
cnf(c_3004,negated_conjecture,
( e20 != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| e21 != op2(e21,e20)
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1659,c_3003]) ).
cnf(c_3005,negated_conjecture,
( e20 != e20
| h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| op2(e21,e20) != e21
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_3004]) ).
cnf(c_1691,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| op2(e21,e20) != e21
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_3005]) ).
cnf(c_3006,plain,
( e20 = e21
| op2(e21,e20) = e21 ),
inference(paramod,[status(thm)],[c_1659,c_1556]) ).
cnf(c_1692,plain,
op2(e21,e20) = e21,
inference(resolve,[status(thm)],[c_255,c_3006]) ).
cnf(c_1693,plain,
op2(e23,e22) != e20,
inference(paramod,[status(thm)],[c_1659,c_210]) ).
cnf(c_1694,plain,
op2(e22,e22) != e20,
inference(paramod,[status(thm)],[c_1659,c_209]) ).
cnf(c_1695,plain,
op2(e20,e22) != e20,
inference(paramod,[status(thm)],[c_1659,c_206]) ).
cnf(c_3007,plain,
( op2(e23,e22) = e21
| op2(e22,e22) = e21
| e20 = e21
| op2(e20,e22) = e21 ),
inference(paramod,[status(thm)],[c_1659,c_122]) ).
cnf(c_1697,plain,
( op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e20,e22) = e21 ),
inference(resolve,[status(thm)],[c_255,c_3007]) ).
cnf(c_1699,plain,
( op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(resolve,[status(thm)],[c_1662,c_131]) ).
cnf(c_1769,plain,
op1(e12,e10) != e11,
inference(paramod,[status(thm)],[c_1677,c_139]) ).
cnf(c_1770,plain,
op1(e10,e10) != e11,
inference(paramod,[status(thm)],[c_1677,c_136]) ).
cnf(c_1772,plain,
( op1(e13,e13) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 ),
inference(resolve,[status(thm)],[c_1678,c_70]) ).
cnf(c_1774,plain,
( op1(e12,e13) = e10
| op1(e12,e11) = e10
| op1(e12,e10) = e10 ),
inference(resolve,[status(thm)],[c_1679,c_62]) ).
cnf(c_3008,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1692,c_1691]) ).
cnf(c_1778,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_3008]) ).
cnf(c_1780,plain,
op2(e22,e20) != e21,
inference(paramod,[status(thm)],[c_1692,c_195]) ).
cnf(c_1781,plain,
op2(e20,e20) != e21,
inference(paramod,[status(thm)],[c_1692,c_192]) ).
cnf(c_1783,plain,
( op2(e23,e23) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 ),
inference(resolve,[status(thm)],[c_1693,c_127]) ).
cnf(c_1785,plain,
( op2(e22,e23) = e20
| op2(e22,e21) = e20
| op2(e22,e20) = e20 ),
inference(resolve,[status(thm)],[c_1694,c_119]) ).
cnf(c_1791,plain,
( op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11 ),
inference(resolve,[status(thm)],[c_1769,c_64]) ).
cnf(c_1793,plain,
( op1(e10,e13) = e11
| op1(e10,e12) = e11
| op1(e10,e11) = e11 ),
inference(resolve,[status(thm)],[c_1770,c_48]) ).
cnf(c_1797,plain,
( op2(e22,e23) = e21
| op2(e22,e22) = e21
| op2(e22,e21) = e21 ),
inference(resolve,[status(thm)],[c_1780,c_121]) ).
cnf(c_1799,plain,
( op2(e20,e23) = e21
| op2(e20,e22) = e21
| op2(e20,e21) = e21 ),
inference(resolve,[status(thm)],[c_1781,c_105]) ).
cnf(c_3009,plain,
( op1(e11,e10) = e10
| unit1 = e13
| unit1 = e12
| unit1 = e10 ),
inference(paramod,[status(thm)],[c_45,c_37]) ).
cnf(c_3010,plain,
( e11 = e10
| unit1 = e13
| unit1 = e12
| unit1 = e10 ),
inference(paramod,[status(thm)],[c_1677,c_3009]) ).
cnf(c_3011,plain,
( e10 = e11
| unit1 = e13
| unit1 = e12
| unit1 = e10 ),
inference(copy,[status(thm)],[c_3010]) ).
cnf(c_1802,plain,
( unit1 = e13
| unit1 = e12
| unit1 = e10 ),
inference(resolve,[status(thm)],[c_248,c_3011]) ).
cnf(c_3012,plain,
( op2(e21,e20) = e20
| unit2 = e23
| unit2 = e22
| unit2 = e20 ),
inference(paramod,[status(thm)],[c_102,c_94]) ).
cnf(c_3013,plain,
( e21 = e20
| unit2 = e23
| unit2 = e22
| unit2 = e20 ),
inference(paramod,[status(thm)],[c_1692,c_3012]) ).
cnf(c_3014,plain,
( e20 = e21
| unit2 = e23
| unit2 = e22
| unit2 = e20 ),
inference(copy,[status(thm)],[c_3013]) ).
cnf(c_1815,plain,
( unit2 = e23
| unit2 = e22
| unit2 = e20 ),
inference(resolve,[status(thm)],[c_255,c_3014]) ).
cnf(c_3015,plain,
( e13 != op1(e13,e10)
| op1(e12,e12) = e13
| op1(e10,e12) = e13 ),
inference(paramod,[status(thm)],[c_1649,c_186]) ).
cnf(c_1913,plain,
( op1(e13,e10) != e13
| op1(e12,e12) = e13
| op1(e10,e12) = e13 ),
inference(copy,[status(thm)],[c_3015]) ).
cnf(c_1973,plain,
( op1(e12,e13) != e13
| op1(e10,e12) = e13
| op1(e10,e10) = e13 ),
inference(paramod,[status(thm)],[c_1656,c_158]) ).
cnf(c_3016,plain,
( e23 != op2(e23,e20)
| op2(e22,e22) = e23
| op2(e20,e22) = e23 ),
inference(paramod,[status(thm)],[c_1668,c_242]) ).
cnf(c_2027,plain,
( op2(e23,e20) != e23
| op2(e22,e22) = e23
| op2(e20,e22) = e23 ),
inference(copy,[status(thm)],[c_3016]) ).
cnf(c_2095,plain,
( op2(e22,e23) != e23
| op2(e20,e22) = e23
| op2(e20,e20) = e23 ),
inference(paramod,[status(thm)],[c_1675,c_214]) ).
cnf(c_3017,plain,
( e12 != op1(e10,e12)
| op1(e13,e11) = e12
| op1(e13,e10) = e12 ),
inference(paramod,[status(thm)],[c_1684,c_152]) ).
cnf(c_2156,plain,
( op1(e10,e12) != e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 ),
inference(copy,[status(thm)],[c_3017]) ).
cnf(c_3018,plain,
( e22 != op2(e20,e22)
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(paramod,[status(thm)],[c_1699,c_208]) ).
cnf(c_2279,plain,
( op2(e20,e22) != e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(copy,[status(thm)],[c_3018]) ).
cnf(c_3019,plain,
( e10 = e13
| op1(e12,e10) = e13
| op1(e10,e10) = e13
| op1(e13,e13) = e10
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_1772,c_1650]) ).
cnf(c_3020,plain,
( e13 = e10
| op1(e12,e10) = e13
| op1(e10,e10) = e13
| op1(e13,e13) = e10
| op1(e13,e11) = e10 ),
inference(copy,[status(thm)],[c_3019]) ).
cnf(c_2391,plain,
( op1(e12,e10) = e13
| op1(e10,e10) = e13
| op1(e13,e13) = e10
| op1(e13,e11) = e10 ),
inference(resolve,[status(thm)],[c_250,c_3020]) ).
cnf(c_3021,plain,
( e20 = e23
| op2(e22,e20) = e23
| op2(e20,e20) = e23
| op2(e23,e23) = e20
| op2(e23,e21) = e20 ),
inference(paramod,[status(thm)],[c_1783,c_1669]) ).
cnf(c_3022,plain,
( e23 = e20
| op2(e22,e20) = e23
| op2(e20,e20) = e23
| op2(e23,e23) = e20
| op2(e23,e21) = e20 ),
inference(copy,[status(thm)],[c_3021]) ).
cnf(c_2501,plain,
( op2(e22,e20) = e23
| op2(e20,e20) = e23
| op2(e23,e23) = e20
| op2(e23,e21) = e20 ),
inference(resolve,[status(thm)],[c_257,c_3022]) ).
cnf(c_3023,plain,
( op1(e12,e13) = e13
| e11 = e13
| op1(e12,e10) = e13
| op1(e12,e13) = e11
| op1(e12,e11) = e11 ),
inference(paramod,[status(thm)],[c_1791,c_1654]) ).
cnf(c_3024,plain,
( op1(e12,e13) = e13
| e13 = e11
| op1(e12,e10) = e13
| op1(e12,e13) = e11
| op1(e12,e11) = e11 ),
inference(copy,[status(thm)],[c_3023]) ).
cnf(c_2628,plain,
( op1(e12,e13) = e13
| op1(e12,e10) = e13
| op1(e12,e13) = e11
| op1(e12,e11) = e11 ),
inference(resolve,[status(thm)],[c_252,c_3024]) ).
cnf(c_3025,plain,
( e11 = e10
| op1(e12,e11) = e10
| op1(e12,e10) = e10
| op1(e12,e12) = e11
| op1(e12,e11) = e11 ),
inference(paramod,[status(thm)],[c_1791,c_1774]) ).
cnf(c_3026,plain,
( e10 = e11
| op1(e12,e11) = e10
| op1(e12,e10) = e10
| op1(e12,e12) = e11
| op1(e12,e11) = e11 ),
inference(copy,[status(thm)],[c_3025]) ).
cnf(c_2634,plain,
( op1(e12,e11) = e10
| op1(e12,e10) = e10
| op1(e12,e12) = e11
| op1(e12,e11) = e11 ),
inference(resolve,[status(thm)],[c_248,c_3026]) ).
cnf(c_2647,plain,
( op1(e12,e11) != e11
| op1(e10,e13) = e11
| op1(e10,e12) = e11 ),
inference(paramod,[status(thm)],[c_1793,c_144]) ).
cnf(c_3027,plain,
( op2(e22,e23) = e23
| e21 = e23
| op2(e22,e20) = e23
| op2(e22,e23) = e21
| op2(e22,e21) = e21 ),
inference(paramod,[status(thm)],[c_1797,c_1673]) ).
cnf(c_3028,plain,
( op2(e22,e23) = e23
| e23 = e21
| op2(e22,e20) = e23
| op2(e22,e23) = e21
| op2(e22,e21) = e21 ),
inference(copy,[status(thm)],[c_3027]) ).
cnf(c_2729,plain,
( op2(e22,e23) = e23
| op2(e22,e20) = e23
| op2(e22,e23) = e21
| op2(e22,e21) = e21 ),
inference(resolve,[status(thm)],[c_259,c_3028]) ).
cnf(c_3029,plain,
( e21 = e20
| op2(e22,e21) = e20
| op2(e22,e20) = e20
| op2(e22,e22) = e21
| op2(e22,e21) = e21 ),
inference(paramod,[status(thm)],[c_1797,c_1785]) ).
cnf(c_3030,plain,
( e20 = e21
| op2(e22,e21) = e20
| op2(e22,e20) = e20
| op2(e22,e22) = e21
| op2(e22,e21) = e21 ),
inference(copy,[status(thm)],[c_3029]) ).
cnf(c_2735,plain,
( op2(e22,e21) = e20
| op2(e22,e20) = e20
| op2(e22,e22) = e21
| op2(e22,e21) = e21 ),
inference(resolve,[status(thm)],[c_255,c_3030]) ).
cnf(c_2748,plain,
( op2(e22,e21) != e21
| op2(e20,e23) = e21
| op2(e20,e22) = e21 ),
inference(paramod,[status(thm)],[c_1799,c_200]) ).
cnf(c_3031,plain,
( op1(e10,e12) = e10
| unit1 = e13
| unit1 = e10 ),
inference(paramod,[status(thm)],[c_1802,c_38]) ).
cnf(c_2804,plain,
( unit1 = e13
| unit1 = e10 ),
inference(resolve,[status(thm)],[c_1680,c_3031]) ).
cnf(c_2813,plain,
( op1(e10,e10) = e10
| unit1 = e13 ),
inference(paramod,[status(thm)],[c_2804,c_37]) ).
cnf(c_2816,plain,
( op1(e10,e11) = e11
| unit1 = e13 ),
inference(paramod,[status(thm)],[c_2804,c_39]) ).
cnf(c_3032,plain,
( op1(e11,e13) = e11
| unit1 = e10 ),
inference(paramod,[status(thm)],[c_2804,c_40]) ).
cnf(c_3033,plain,
( e12 = e11
| unit1 = e10 ),
inference(paramod,[status(thm)],[c_1534,c_3032]) ).
cnf(c_2818,plain,
unit1 = e10,
inference(resolve,[status(thm)],[c_251,c_3033]) ).
cnf(c_3034,plain,
( op1(e10,e12) = e12
| unit1 = e13 ),
inference(paramod,[status(thm)],[c_2804,c_41]) ).
cnf(c_3035,plain,
( op1(e10,e12) = e12
| e10 = e13 ),
inference(paramod,[status(thm)],[c_2818,c_3034]) ).
cnf(c_3036,plain,
( op1(e10,e12) = e12
| e13 = e10 ),
inference(copy,[status(thm)],[c_3035]) ).
cnf(c_2819,plain,
op1(e10,e12) = e12,
inference(resolve,[status(thm)],[c_250,c_3036]) ).
cnf(c_3037,plain,
( op1(e12,e10) = e12
| unit1 = e13 ),
inference(paramod,[status(thm)],[c_2804,c_42]) ).
cnf(c_3038,plain,
( op1(e12,e10) = e12
| e10 = e13 ),
inference(paramod,[status(thm)],[c_2818,c_3037]) ).
cnf(c_3039,plain,
( op1(e12,e10) = e12
| e13 = e10 ),
inference(copy,[status(thm)],[c_3038]) ).
cnf(c_2820,plain,
op1(e12,e10) = e12,
inference(resolve,[status(thm)],[c_250,c_3039]) ).
cnf(c_3040,plain,
( op1(e10,e13) = e13
| unit1 = e13 ),
inference(paramod,[status(thm)],[c_2804,c_43]) ).
cnf(c_3041,plain,
( op1(e10,e13) = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_2818,c_3040]) ).
cnf(c_3042,plain,
( op1(e10,e13) = e13
| e13 = e10 ),
inference(copy,[status(thm)],[c_3041]) ).
cnf(c_2821,plain,
op1(e10,e13) = e13,
inference(resolve,[status(thm)],[c_250,c_3042]) ).
cnf(c_3043,plain,
( op1(e13,e10) = e13
| unit1 = e13 ),
inference(paramod,[status(thm)],[c_2804,c_44]) ).
cnf(c_3044,plain,
( op1(e13,e10) = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_2818,c_3043]) ).
cnf(c_3045,plain,
( op1(e13,e10) = e13
| e13 = e10 ),
inference(copy,[status(thm)],[c_3044]) ).
cnf(c_2822,plain,
op1(e13,e10) = e13,
inference(resolve,[status(thm)],[c_250,c_3045]) ).
cnf(c_3046,plain,
( op1(e10,e11) = e11
| e10 = e13 ),
inference(paramod,[status(thm)],[c_2818,c_2816]) ).
cnf(c_3047,plain,
( op1(e10,e11) = e11
| e13 = e10 ),
inference(copy,[status(thm)],[c_3046]) ).
cnf(c_2823,plain,
op1(e10,e11) = e11,
inference(resolve,[status(thm)],[c_250,c_3047]) ).
cnf(c_3048,plain,
( op1(e10,e10) = e10
| e10 = e13 ),
inference(paramod,[status(thm)],[c_2818,c_2813]) ).
cnf(c_3049,plain,
( op1(e10,e10) = e10
| e13 = e10 ),
inference(copy,[status(thm)],[c_3048]) ).
cnf(c_2824,plain,
op1(e10,e10) = e10,
inference(resolve,[status(thm)],[c_250,c_3049]) ).
cnf(c_3050,plain,
( op1(e12,e11) != e11
| op1(e10,e13) = e11
| e12 = e11 ),
inference(paramod,[status(thm)],[c_2819,c_2647]) ).
cnf(c_3051,plain,
( op1(e12,e11) != e11
| e13 = e11
| e12 = e11 ),
inference(paramod,[status(thm)],[c_2821,c_3050]) ).
cnf(c_3052,plain,
( op1(e12,e11) != e11
| e13 = e11 ),
inference(resolve,[status(thm)],[c_251,c_3051]) ).
cnf(c_2828,plain,
op1(e12,e11) != e11,
inference(resolve,[status(thm)],[c_252,c_3052]) ).
cnf(c_3053,plain,
( op1(e10,e12) != e12
| op1(e13,e11) = e12
| e13 = e12 ),
inference(paramod,[status(thm)],[c_2822,c_2156]) ).
cnf(c_3054,plain,
( e12 != e12
| op1(e13,e11) = e12
| e13 = e12 ),
inference(paramod,[status(thm)],[c_2819,c_3053]) ).
cnf(c_3055,plain,
( op1(e13,e11) = e12
| e13 = e12 ),
inference(copy,[status(thm)],[c_3054]) ).
cnf(c_2837,plain,
op1(e13,e11) = e12,
inference(resolve,[status(thm)],[c_253,c_3055]) ).
cnf(c_3056,plain,
( op1(e12,e13) != e13
| op1(e10,e12) = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_2824,c_1973]) ).
cnf(c_3057,plain,
( op1(e12,e13) != e13
| e12 = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_2819,c_3056]) ).
cnf(c_3058,plain,
( op1(e12,e13) != e13
| e12 = e13
| e13 = e10 ),
inference(copy,[status(thm)],[c_3057]) ).
cnf(c_3059,plain,
( op1(e12,e13) != e13
| e13 = e12
| e13 = e10 ),
inference(copy,[status(thm)],[c_3058]) ).
cnf(c_3060,plain,
( op1(e12,e13) != e13
| e13 = e12 ),
inference(resolve,[status(thm)],[c_250,c_3059]) ).
cnf(c_2844,plain,
op1(e12,e13) != e13,
inference(resolve,[status(thm)],[c_253,c_3060]) ).
cnf(c_3061,plain,
( op1(e13,e10) != e13
| op1(e12,e12) = e13
| e12 = e13 ),
inference(paramod,[status(thm)],[c_2819,c_1913]) ).
cnf(c_3062,plain,
( e13 != e13
| op1(e12,e12) = e13
| e12 = e13 ),
inference(paramod,[status(thm)],[c_2822,c_3061]) ).
cnf(c_3063,plain,
( e13 != e13
| op1(e12,e12) = e13
| e13 = e12 ),
inference(copy,[status(thm)],[c_3062]) ).
cnf(c_3064,plain,
( op1(e12,e12) = e13
| e13 = e12 ),
inference(copy,[status(thm)],[c_3063]) ).
cnf(c_2845,plain,
op1(e12,e12) = e13,
inference(resolve,[status(thm)],[c_253,c_3064]) ).
cnf(c_3065,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| h2(e10) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2824,c_1778]) ).
cnf(c_3066,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(op1(e10,e11)) != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1690,c_3065]) ).
cnf(c_3067,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| h2(e11) != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2823,c_3066]) ).
cnf(c_3068,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(op1(e10,e12)) != op2(e20,e22)
| e21 != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_308,c_3067]) ).
cnf(c_3069,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| h2(op1(e10,e13)) != op2(e20,e23)
| h2(e12) != op2(e20,e22)
| e21 != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2819,c_3068]) ).
cnf(c_3070,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| h2(op1(e10,e13)) != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1660,c_3069]) ).
cnf(c_3071,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| h2(e13) != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2821,c_3070]) ).
cnf(c_3072,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(op1(e12,e10)) != op2(e22,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_314,c_3071]) ).
cnf(c_3073,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| h2(e12) != op2(e22,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2820,c_3072]) ).
cnf(c_3074,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(op1(e12,e12)) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| e22 != op2(e22,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1660,c_3073]) ).
cnf(c_3075,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| h2(e13) != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| e22 != op2(e22,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2845,c_3074]) ).
cnf(c_3076,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(op1(e13,e10)) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| e23 != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| e22 != op2(e22,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_314,c_3075]) ).
cnf(c_3077,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| h2(e13) != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| e23 != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| e22 != op2(e22,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2822,c_3076]) ).
cnf(c_3078,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(op1(e13,e11)) != op2(e23,e21)
| e23 != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| e23 != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| e22 != op2(e22,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_314,c_3077]) ).
cnf(c_3079,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| h2(e12) != op2(e23,e21)
| e23 != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| e23 != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| e22 != op2(e22,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2837,c_3078]) ).
cnf(c_3080,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| e22 != op2(e23,e21)
| e23 != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| e23 != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| e22 != op2(e22,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1660,c_3079]) ).
cnf(c_3081,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| e22 != op2(e23,e21)
| e23 != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| e23 != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| e22 != op2(e22,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21)
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_3080]) ).
cnf(c_3082,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| e22 != op2(e23,e21)
| e23 != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| e23 != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| e22 != op2(e22,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_3081]) ).
cnf(c_3083,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| e22 != op2(e23,e21)
| e23 != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| e23 != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| e22 != op2(e22,e20)
| e23 != op2(e20,e23)
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_3082]) ).
cnf(c_3084,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| e22 != op2(e23,e21)
| e23 != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| e23 != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| e22 != op2(e22,e20)
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_3083]) ).
cnf(c_3085,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| e22 != op2(e23,e21)
| e23 != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| e23 != op2(e22,e22)
| h2(op1(e12,e11)) != op2(e22,e21)
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_3084]) ).
cnf(c_3086,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| e22 != op2(e23,e21)
| e23 != op2(e23,e20)
| h2(op1(e12,e13)) != op2(e22,e23)
| op2(e22,e22) != e23
| h2(op1(e12,e11)) != op2(e22,e21)
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_3085]) ).
cnf(c_3087,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| e22 != op2(e23,e21)
| op2(e23,e20) != e23
| h2(op1(e12,e13)) != op2(e22,e23)
| op2(e22,e22) != e23
| h2(op1(e12,e11)) != op2(e22,e21)
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_3086]) ).
cnf(c_2846,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| h2(op1(e12,e13)) != op2(e22,e23)
| op2(e22,e22) != e23
| h2(op1(e12,e11)) != op2(e22,e21)
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_3087]) ).
cnf(c_3088,plain,
( op1(e13,e12) = e11
| op1(e12,e12) = e11
| e12 = e11 ),
inference(paramod,[status(thm)],[c_2819,c_1682]) ).
cnf(c_3089,plain,
( op1(e13,e12) = e11
| e13 = e11
| e12 = e11 ),
inference(paramod,[status(thm)],[c_2845,c_3088]) ).
cnf(c_3090,plain,
( op1(e13,e12) = e11
| e13 = e11 ),
inference(resolve,[status(thm)],[c_251,c_3089]) ).
cnf(c_2847,plain,
op1(e13,e12) = e11,
inference(resolve,[status(thm)],[c_252,c_3090]) ).
cnf(c_3091,plain,
( op1(e12,e11) = e10
| op1(e12,e10) = e10
| e13 = e11
| op1(e12,e11) = e11 ),
inference(paramod,[status(thm)],[c_2845,c_2634]) ).
cnf(c_3092,plain,
( op1(e12,e11) = e10
| e12 = e10
| e13 = e11
| op1(e12,e11) = e11 ),
inference(paramod,[status(thm)],[c_2820,c_3091]) ).
cnf(c_3093,plain,
( op1(e12,e11) = e10
| e12 = e10
| e13 = e11 ),
inference(resolve,[status(thm)],[c_2828,c_3092]) ).
cnf(c_3094,plain,
( op1(e12,e11) = e10
| e12 = e10 ),
inference(resolve,[status(thm)],[c_252,c_3093]) ).
cnf(c_2849,plain,
op1(e12,e11) = e10,
inference(resolve,[status(thm)],[c_249,c_3094]) ).
cnf(c_3095,plain,
( op1(e12,e13) = e13
| op1(e12,e10) = e13
| op1(e12,e13) = e11
| e10 = e11 ),
inference(paramod,[status(thm)],[c_2849,c_2628]) ).
cnf(c_3096,plain,
( op1(e12,e13) = e13
| e12 = e13
| op1(e12,e13) = e11
| e10 = e11 ),
inference(paramod,[status(thm)],[c_2820,c_3095]) ).
cnf(c_3097,plain,
( op1(e12,e13) = e13
| e13 = e12
| op1(e12,e13) = e11
| e10 = e11 ),
inference(copy,[status(thm)],[c_3096]) ).
cnf(c_3098,plain,
( op1(e12,e13) = e13
| e13 = e12
| op1(e12,e13) = e11 ),
inference(resolve,[status(thm)],[c_248,c_3097]) ).
cnf(c_3099,plain,
( op1(e12,e13) = e13
| op1(e12,e13) = e11 ),
inference(resolve,[status(thm)],[c_253,c_3098]) ).
cnf(c_2851,plain,
op1(e12,e13) = e11,
inference(resolve,[status(thm)],[c_2844,c_3099]) ).
cnf(c_3100,plain,
( op1(e12,e10) = e13
| op1(e10,e10) = e13
| op1(e13,e13) = e10
| e12 = e10 ),
inference(paramod,[status(thm)],[c_2837,c_2391]) ).
cnf(c_3101,plain,
( op1(e12,e10) = e13
| e10 = e13
| op1(e13,e13) = e10
| e12 = e10 ),
inference(paramod,[status(thm)],[c_2824,c_3100]) ).
cnf(c_3102,plain,
( e12 = e13
| e10 = e13
| op1(e13,e13) = e10
| e12 = e10 ),
inference(paramod,[status(thm)],[c_2820,c_3101]) ).
cnf(c_3103,plain,
( e12 = e13
| e13 = e10
| op1(e13,e13) = e10
| e12 = e10 ),
inference(copy,[status(thm)],[c_3102]) ).
cnf(c_3104,plain,
( e13 = e12
| e13 = e10
| op1(e13,e13) = e10
| e12 = e10 ),
inference(copy,[status(thm)],[c_3103]) ).
cnf(c_3105,plain,
( e13 = e12
| e13 = e10
| op1(e13,e13) = e10 ),
inference(resolve,[status(thm)],[c_249,c_3104]) ).
cnf(c_3106,plain,
( e13 = e12
| op1(e13,e13) = e10 ),
inference(resolve,[status(thm)],[c_250,c_3105]) ).
cnf(c_2852,plain,
op1(e13,e13) = e10,
inference(resolve,[status(thm)],[c_253,c_3106]) ).
cnf(c_3107,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| h2(op1(e12,e13)) != op2(e22,e23)
| op2(e22,e22) != e23
| h2(e10) != op2(e22,e21)
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(paramod,[status(thm)],[c_2849,c_2846]) ).
cnf(c_3108,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| h2(op1(e12,e13)) != op2(e22,e23)
| op2(e22,e22) != e23
| e20 != op2(e22,e21)
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(paramod,[status(thm)],[c_1690,c_3107]) ).
cnf(c_3109,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| h2(e11) != op2(e22,e23)
| op2(e22,e22) != e23
| e20 != op2(e22,e21)
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(paramod,[status(thm)],[c_2851,c_3108]) ).
cnf(c_3110,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(op1(e13,e12)) != op2(e23,e22)
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| e21 != op2(e22,e23)
| op2(e22,e22) != e23
| e20 != op2(e22,e21)
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(paramod,[status(thm)],[c_308,c_3109]) ).
cnf(c_3111,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| h2(e11) != op2(e23,e22)
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| e21 != op2(e22,e23)
| op2(e22,e22) != e23
| e20 != op2(e22,e21)
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(paramod,[status(thm)],[c_2847,c_3110]) ).
cnf(c_3112,negated_conjecture,
( h2(op1(e13,e13)) != op2(e23,e23)
| e21 != op2(e23,e22)
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| e21 != op2(e22,e23)
| op2(e22,e22) != e23
| e20 != op2(e22,e21)
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(paramod,[status(thm)],[c_308,c_3111]) ).
cnf(c_3113,negated_conjecture,
( h2(e10) != op2(e23,e23)
| e21 != op2(e23,e22)
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| e21 != op2(e22,e23)
| op2(e22,e22) != e23
| e20 != op2(e22,e21)
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(paramod,[status(thm)],[c_2852,c_3112]) ).
cnf(c_3114,negated_conjecture,
( e20 != op2(e23,e23)
| e21 != op2(e23,e22)
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| e21 != op2(e22,e23)
| op2(e22,e22) != e23
| e20 != op2(e22,e21)
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(paramod,[status(thm)],[c_1690,c_3113]) ).
cnf(c_3115,negated_conjecture,
( e20 != op2(e23,e23)
| e21 != op2(e23,e22)
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| e21 != op2(e22,e23)
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_3114]) ).
cnf(c_3116,negated_conjecture,
( e20 != op2(e23,e23)
| e21 != op2(e23,e22)
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_3115]) ).
cnf(c_3117,negated_conjecture,
( e20 != op2(e23,e23)
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_3116]) ).
cnf(c_2853,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_3117]) ).
cnf(c_3118,plain,
( op2(e20,e22) = e20
| unit2 = e23
| unit2 = e20 ),
inference(paramod,[status(thm)],[c_1815,c_95]) ).
cnf(c_2857,plain,
( unit2 = e23
| unit2 = e20 ),
inference(resolve,[status(thm)],[c_1695,c_3118]) ).
cnf(c_2866,plain,
( op2(e20,e20) = e20
| unit2 = e23 ),
inference(paramod,[status(thm)],[c_2857,c_94]) ).
cnf(c_2869,plain,
( op2(e20,e21) = e21
| unit2 = e23 ),
inference(paramod,[status(thm)],[c_2857,c_96]) ).
cnf(c_3119,plain,
( op2(e21,e23) = e21
| unit2 = e20 ),
inference(paramod,[status(thm)],[c_2857,c_97]) ).
cnf(c_3120,plain,
( e22 = e21
| unit2 = e20 ),
inference(paramod,[status(thm)],[c_1547,c_3119]) ).
cnf(c_2871,plain,
unit2 = e20,
inference(resolve,[status(thm)],[c_258,c_3120]) ).
cnf(c_3121,plain,
( op2(e20,e22) = e22
| unit2 = e23 ),
inference(paramod,[status(thm)],[c_2857,c_98]) ).
cnf(c_3122,plain,
( op2(e20,e22) = e22
| e20 = e23 ),
inference(paramod,[status(thm)],[c_2871,c_3121]) ).
cnf(c_3123,plain,
( op2(e20,e22) = e22
| e23 = e20 ),
inference(copy,[status(thm)],[c_3122]) ).
cnf(c_2872,plain,
op2(e20,e22) = e22,
inference(resolve,[status(thm)],[c_257,c_3123]) ).
cnf(c_3124,plain,
( op2(e22,e20) = e22
| unit2 = e23 ),
inference(paramod,[status(thm)],[c_2857,c_99]) ).
cnf(c_3125,plain,
( op2(e22,e20) = e22
| e20 = e23 ),
inference(paramod,[status(thm)],[c_2871,c_3124]) ).
cnf(c_3126,plain,
( op2(e22,e20) = e22
| e23 = e20 ),
inference(copy,[status(thm)],[c_3125]) ).
cnf(c_2873,plain,
op2(e22,e20) = e22,
inference(resolve,[status(thm)],[c_257,c_3126]) ).
cnf(c_3127,plain,
( op2(e20,e23) = e23
| unit2 = e23 ),
inference(paramod,[status(thm)],[c_2857,c_100]) ).
cnf(c_3128,plain,
( op2(e20,e23) = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_2871,c_3127]) ).
cnf(c_3129,plain,
( op2(e20,e23) = e23
| e23 = e20 ),
inference(copy,[status(thm)],[c_3128]) ).
cnf(c_2874,plain,
op2(e20,e23) = e23,
inference(resolve,[status(thm)],[c_257,c_3129]) ).
cnf(c_3130,plain,
( op2(e23,e20) = e23
| unit2 = e23 ),
inference(paramod,[status(thm)],[c_2857,c_101]) ).
cnf(c_3131,plain,
( op2(e23,e20) = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_2871,c_3130]) ).
cnf(c_3132,plain,
( op2(e23,e20) = e23
| e23 = e20 ),
inference(copy,[status(thm)],[c_3131]) ).
cnf(c_2875,plain,
op2(e23,e20) = e23,
inference(resolve,[status(thm)],[c_257,c_3132]) ).
cnf(c_3133,plain,
( op2(e20,e21) = e21
| e20 = e23 ),
inference(paramod,[status(thm)],[c_2871,c_2869]) ).
cnf(c_3134,plain,
( op2(e20,e21) = e21
| e23 = e20 ),
inference(copy,[status(thm)],[c_3133]) ).
cnf(c_2876,plain,
op2(e20,e21) = e21,
inference(resolve,[status(thm)],[c_257,c_3134]) ).
cnf(c_3135,plain,
( op2(e20,e20) = e20
| e20 = e23 ),
inference(paramod,[status(thm)],[c_2871,c_2866]) ).
cnf(c_3136,plain,
( op2(e20,e20) = e20
| e23 = e20 ),
inference(copy,[status(thm)],[c_3135]) ).
cnf(c_2877,plain,
op2(e20,e20) = e20,
inference(resolve,[status(thm)],[c_257,c_3136]) ).
cnf(c_3137,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2877,c_2853]) ).
cnf(c_3138,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| e21 != e21
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2876,c_3137]) ).
cnf(c_3139,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| op2(e22,e20) != e22
| op2(e20,e23) != e23
| e22 != e22
| e21 != e21
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2872,c_3138]) ).
cnf(c_3140,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| op2(e22,e20) != e22
| e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2874,c_3139]) ).
cnf(c_3141,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| e22 != e22
| e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2873,c_3140]) ).
cnf(c_3142,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| e23 != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| e22 != e22
| e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2875,c_3141]) ).
cnf(c_3143,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| e23 != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| e22 != e22
| e23 != e23
| e22 != e22
| e21 != e21 ),
inference(copy,[status(thm)],[c_3142]) ).
cnf(c_3144,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| e23 != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| e22 != e22
| e23 != e23
| e22 != e22 ),
inference(copy,[status(thm)],[c_3143]) ).
cnf(c_3145,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| e23 != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| e22 != e22
| e23 != e23 ),
inference(copy,[status(thm)],[c_3144]) ).
cnf(c_3146,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| e23 != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20
| e22 != e22 ),
inference(copy,[status(thm)],[c_3145]) ).
cnf(c_3147,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| e23 != e23
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20 ),
inference(copy,[status(thm)],[c_3146]) ).
cnf(c_2878,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| op2(e22,e21) != e20 ),
inference(copy,[status(thm)],[c_3147]) ).
cnf(c_3148,plain,
( op2(e22,e21) != e21
| op2(e20,e23) = e21
| e22 = e21 ),
inference(paramod,[status(thm)],[c_2872,c_2748]) ).
cnf(c_3149,plain,
( op2(e22,e21) != e21
| e23 = e21
| e22 = e21 ),
inference(paramod,[status(thm)],[c_2874,c_3148]) ).
cnf(c_3150,plain,
( op2(e22,e21) != e21
| e23 = e21 ),
inference(resolve,[status(thm)],[c_258,c_3149]) ).
cnf(c_2882,plain,
op2(e22,e21) != e21,
inference(resolve,[status(thm)],[c_259,c_3150]) ).
cnf(c_3151,plain,
( op2(e20,e22) != e22
| op2(e23,e21) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_2875,c_2279]) ).
cnf(c_3152,plain,
( e22 != e22
| op2(e23,e21) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_2872,c_3151]) ).
cnf(c_3153,plain,
( op2(e23,e21) = e22
| e23 = e22 ),
inference(copy,[status(thm)],[c_3152]) ).
cnf(c_2891,plain,
op2(e23,e21) = e22,
inference(resolve,[status(thm)],[c_260,c_3153]) ).
cnf(c_3154,plain,
( op2(e22,e23) != e23
| op2(e20,e22) = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_2877,c_2095]) ).
cnf(c_3155,plain,
( op2(e22,e23) != e23
| e22 = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_2872,c_3154]) ).
cnf(c_3156,plain,
( op2(e22,e23) != e23
| e22 = e23
| e23 = e20 ),
inference(copy,[status(thm)],[c_3155]) ).
cnf(c_3157,plain,
( op2(e22,e23) != e23
| e23 = e22
| e23 = e20 ),
inference(copy,[status(thm)],[c_3156]) ).
cnf(c_3158,plain,
( op2(e22,e23) != e23
| e23 = e22 ),
inference(resolve,[status(thm)],[c_257,c_3157]) ).
cnf(c_2900,plain,
op2(e22,e23) != e23,
inference(resolve,[status(thm)],[c_260,c_3158]) ).
cnf(c_3159,plain,
( op2(e23,e20) != e23
| op2(e22,e22) = e23
| e22 = e23 ),
inference(paramod,[status(thm)],[c_2872,c_2027]) ).
cnf(c_3160,plain,
( e23 != e23
| op2(e22,e22) = e23
| e22 = e23 ),
inference(paramod,[status(thm)],[c_2875,c_3159]) ).
cnf(c_3161,plain,
( e23 != e23
| op2(e22,e22) = e23
| e23 = e22 ),
inference(copy,[status(thm)],[c_3160]) ).
cnf(c_3162,plain,
( op2(e22,e22) = e23
| e23 = e22 ),
inference(copy,[status(thm)],[c_3161]) ).
cnf(c_2903,plain,
op2(e22,e22) = e23,
inference(resolve,[status(thm)],[c_260,c_3162]) ).
cnf(c_3163,plain,
( op2(e23,e22) = e21
| op2(e22,e22) = e21
| e22 = e21 ),
inference(paramod,[status(thm)],[c_2872,c_1697]) ).
cnf(c_3164,plain,
( op2(e23,e22) = e21
| e23 = e21
| e22 = e21 ),
inference(paramod,[status(thm)],[c_2903,c_3163]) ).
cnf(c_3165,plain,
( op2(e23,e22) = e21
| e23 = e21 ),
inference(resolve,[status(thm)],[c_258,c_3164]) ).
cnf(c_2904,plain,
op2(e23,e22) = e21,
inference(resolve,[status(thm)],[c_259,c_3165]) ).
cnf(c_3166,plain,
( op2(e22,e21) = e20
| op2(e22,e20) = e20
| e23 = e21
| op2(e22,e21) = e21 ),
inference(paramod,[status(thm)],[c_2903,c_2735]) ).
cnf(c_3167,plain,
( op2(e22,e21) = e20
| e22 = e20
| e23 = e21
| op2(e22,e21) = e21 ),
inference(paramod,[status(thm)],[c_2873,c_3166]) ).
cnf(c_3168,plain,
( op2(e22,e21) = e20
| e22 = e20
| e23 = e21 ),
inference(resolve,[status(thm)],[c_2882,c_3167]) ).
cnf(c_3169,plain,
( op2(e22,e21) = e20
| e22 = e20 ),
inference(resolve,[status(thm)],[c_259,c_3168]) ).
cnf(c_2906,plain,
op2(e22,e21) = e20,
inference(resolve,[status(thm)],[c_256,c_3169]) ).
cnf(c_3170,plain,
( op2(e22,e23) = e23
| op2(e22,e20) = e23
| op2(e22,e23) = e21
| e20 = e21 ),
inference(paramod,[status(thm)],[c_2906,c_2729]) ).
cnf(c_3171,plain,
( op2(e22,e23) = e23
| e22 = e23
| op2(e22,e23) = e21
| e20 = e21 ),
inference(paramod,[status(thm)],[c_2873,c_3170]) ).
cnf(c_3172,plain,
( op2(e22,e23) = e23
| e23 = e22
| op2(e22,e23) = e21
| e20 = e21 ),
inference(copy,[status(thm)],[c_3171]) ).
cnf(c_3173,plain,
( op2(e22,e23) = e23
| e23 = e22
| op2(e22,e23) = e21 ),
inference(resolve,[status(thm)],[c_255,c_3172]) ).
cnf(c_3174,plain,
( op2(e22,e23) = e23
| op2(e22,e23) = e21 ),
inference(resolve,[status(thm)],[c_260,c_3173]) ).
cnf(c_2908,plain,
op2(e22,e23) = e21,
inference(resolve,[status(thm)],[c_2900,c_3174]) ).
cnf(c_3175,plain,
( op2(e22,e20) = e23
| op2(e20,e20) = e23
| op2(e23,e23) = e20
| e22 = e20 ),
inference(paramod,[status(thm)],[c_2891,c_2501]) ).
cnf(c_3176,plain,
( op2(e22,e20) = e23
| e20 = e23
| op2(e23,e23) = e20
| e22 = e20 ),
inference(paramod,[status(thm)],[c_2877,c_3175]) ).
cnf(c_3177,plain,
( e22 = e23
| e20 = e23
| op2(e23,e23) = e20
| e22 = e20 ),
inference(paramod,[status(thm)],[c_2873,c_3176]) ).
cnf(c_3178,plain,
( e22 = e23
| e23 = e20
| op2(e23,e23) = e20
| e22 = e20 ),
inference(copy,[status(thm)],[c_3177]) ).
cnf(c_3179,plain,
( e23 = e22
| e23 = e20
| op2(e23,e23) = e20
| e22 = e20 ),
inference(copy,[status(thm)],[c_3178]) ).
cnf(c_3180,plain,
( e23 = e22
| e23 = e20
| op2(e23,e23) = e20 ),
inference(resolve,[status(thm)],[c_256,c_3179]) ).
cnf(c_3181,plain,
( e23 = e22
| op2(e23,e23) = e20 ),
inference(resolve,[status(thm)],[c_257,c_3180]) ).
cnf(c_2909,plain,
op2(e23,e23) = e20,
inference(resolve,[status(thm)],[c_260,c_3181]) ).
cnf(c_3182,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e22,e23) != e21
| op2(e22,e22) != e23
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2906,c_2878]) ).
cnf(c_3183,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e22,e23) != e21
| e23 != e23
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2903,c_3182]) ).
cnf(c_3184,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| op2(e23,e21) != e22
| e21 != e21
| e23 != e23
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2908,c_3183]) ).
cnf(c_3185,negated_conjecture,
( op2(e23,e23) != e20
| op2(e23,e22) != e21
| e22 != e22
| e21 != e21
| e23 != e23
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2891,c_3184]) ).
cnf(c_3186,negated_conjecture,
( op2(e23,e23) != e20
| e21 != e21
| e22 != e22
| e21 != e21
| e23 != e23
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2904,c_3185]) ).
cnf(c_3187,negated_conjecture,
( e20 != e20
| e21 != e21
| e22 != e22
| e21 != e21
| e23 != e23
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2909,c_3186]) ).
cnf(c_3188,negated_conjecture,
( e20 != e20
| e21 != e21
| e22 != e22
| e21 != e21
| e23 != e23 ),
inference(copy,[status(thm)],[c_3187]) ).
cnf(c_3189,negated_conjecture,
( e20 != e20
| e21 != e21
| e22 != e22
| e21 != e21 ),
inference(copy,[status(thm)],[c_3188]) ).
cnf(c_3190,negated_conjecture,
( e20 != e20
| e21 != e21
| e22 != e22 ),
inference(copy,[status(thm)],[c_3189]) ).
cnf(c_3191,negated_conjecture,
( e20 != e20
| e21 != e21 ),
inference(copy,[status(thm)],[c_3190]) ).
cnf(c_3192,negated_conjecture,
e20 != e20,
inference(copy,[status(thm)],[c_3191]) ).
cnf(c_2913,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_3192]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG038+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 21:01:03 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 2191694 was started by sandbox on n019,
% 0.09/0.36 % Sat Sep 26 21:01:03 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 11.34/11.63
% 11.34/11.63 % From the command line: assign(max_seconds, 300).
% 33.91/14.65
% 33.91/14.65 % SZS status Theorem for theBenchmark
% 33.91/14.65
% 33.91/14.65 % Proof 1 at 1.72 (+ 0.20) seconds.
% 33.91/14.65 % Length of proof is 225.
% 33.91/14.65 % Level of proof is 14.
% 33.91/14.65 % Maximum clause weight is 325.000.
% 33.91/14.65 % Given clauses 289.
% 33.91/14.65
% 33.91/14.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------