%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG105+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:30 AM UTC 2026
% Result : Theorem 62.95s 70.55s
% Output : CNFRefutation 62.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 125
% Number of leaves : 23
% Syntax : Number of formulae : 522 ( 184 unt; 0 def)
% Number of atoms : 3764 (3763 equ)
% Maximal formula atoms : 384 ( 7 avg)
% Number of connectives : 5091 (1849 ~;2526 |; 716 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 6 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax2,axiom,
( ( op1(e13,e13) = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| op1(e10,e13) = e13 )
& ( op1(e13,e13) = e13
| op1(e13,e12) = e13
| op1(e13,e11) = e13
| op1(e13,e10) = e13 )
& ( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 )
& ( op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 )
& ( op1(e13,e13) = e11
| op1(e12,e13) = e11
| op1(e11,e13) = e11
| op1(e10,e13) = e11 )
& ( op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 )
& ( op1(e13,e13) = e10
| op1(e12,e13) = e10
| op1(e11,e13) = e10
| op1(e10,e13) = e10 )
& ( op1(e13,e13) = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 )
& ( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| op1(e10,e12) = e13 )
& ( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 )
& ( op1(e13,e12) = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 )
& ( op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 )
& ( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 )
& ( op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 )
& ( op1(e13,e12) = e10
| op1(e12,e12) = e10
| op1(e11,e12) = e10
| op1(e10,e12) = e10 )
& ( op1(e12,e13) = e10
| op1(e12,e12) = e10
| op1(e12,e11) = e10
| op1(e12,e10) = e10 )
& ( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| op1(e10,e11) = e13 )
& ( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e11) = e13
| op1(e11,e10) = e13 )
& ( op1(e13,e11) = e12
| op1(e12,e11) = e12
| op1(e11,e11) = e12
| op1(e10,e11) = e12 )
& ( op1(e11,e13) = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 )
& ( op1(e13,e11) = e11
| op1(e12,e11) = e11
| op1(e11,e11) = e11
| op1(e10,e11) = e11 )
& ( op1(e11,e13) = e11
| op1(e11,e12) = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 )
& ( op1(e13,e11) = e10
| op1(e12,e11) = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 )
& ( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 )
& ( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| op1(e10,e10) = e13 )
& ( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 )
& ( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| op1(e10,e10) = e12 )
& ( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 )
& ( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11
| op1(e10,e10) = e11 )
& ( op1(e10,e13) = e11
| op1(e10,e12) = e11
| op1(e10,e11) = e11
| op1(e10,e10) = e11 )
& ( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 )
& ( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ) ),
file('theBenchmark.p',ax2) ).
fof(ax4,axiom,
( ( op2(e23,e23) = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| op2(e20,e23) = e23 )
& ( op2(e23,e23) = e23
| op2(e23,e22) = e23
| op2(e23,e21) = e23
| op2(e23,e20) = e23 )
& ( op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 )
& ( op2(e23,e23) = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 )
& ( op2(e23,e23) = e21
| op2(e22,e23) = e21
| op2(e21,e23) = e21
| op2(e20,e23) = e21 )
& ( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 )
& ( op2(e23,e23) = e20
| op2(e22,e23) = e20
| op2(e21,e23) = e20
| op2(e20,e23) = e20 )
& ( op2(e23,e23) = e20
| op2(e23,e22) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 )
& ( op2(e23,e22) = e23
| op2(e22,e22) = e23
| op2(e21,e22) = e23
| op2(e20,e22) = e23 )
& ( op2(e22,e23) = e23
| op2(e22,e22) = e23
| op2(e22,e21) = e23
| op2(e22,e20) = e23 )
& ( op2(e23,e22) = e22
| op2(e22,e22) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 )
& ( op2(e22,e23) = e22
| op2(e22,e22) = e22
| op2(e22,e21) = e22
| op2(e22,e20) = e22 )
& ( op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 )
& ( op2(e22,e23) = e21
| op2(e22,e22) = e21
| op2(e22,e21) = e21
| op2(e22,e20) = e21 )
& ( op2(e23,e22) = e20
| op2(e22,e22) = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 )
& ( op2(e22,e23) = e20
| op2(e22,e22) = e20
| op2(e22,e21) = e20
| op2(e22,e20) = e20 )
& ( op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e21,e21) = e23
| op2(e20,e21) = e23 )
& ( op2(e21,e23) = e23
| op2(e21,e22) = e23
| op2(e21,e21) = e23
| op2(e21,e20) = e23 )
& ( op2(e23,e21) = e22
| op2(e22,e21) = e22
| op2(e21,e21) = e22
| op2(e20,e21) = e22 )
& ( op2(e21,e23) = e22
| op2(e21,e22) = e22
| op2(e21,e21) = e22
| op2(e21,e20) = e22 )
& ( op2(e23,e21) = e21
| op2(e22,e21) = e21
| op2(e21,e21) = e21
| op2(e20,e21) = e21 )
& ( op2(e21,e23) = e21
| op2(e21,e22) = e21
| op2(e21,e21) = e21
| op2(e21,e20) = e21 )
& ( op2(e23,e21) = e20
| op2(e22,e21) = e20
| op2(e21,e21) = e20
| op2(e20,e21) = e20 )
& ( op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20
| op2(e21,e20) = e20 )
& ( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| op2(e20,e20) = e23 )
& ( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 )
& ( op2(e23,e20) = e22
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| op2(e20,e20) = e22 )
& ( op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| op2(e20,e20) = e22 )
& ( op2(e23,e20) = e21
| op2(e22,e20) = e21
| op2(e21,e20) = e21
| op2(e20,e20) = e21 )
& ( op2(e20,e23) = e21
| op2(e20,e22) = e21
| op2(e20,e21) = e21
| op2(e20,e20) = e21 )
& ( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| op2(e20,e20) = e20 )
& ( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ) ),
file('theBenchmark.p',ax4) ).
fof(ax5,axiom,
( op1(e13,e12) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e11)
& op1(e12,e12) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e11)
& op1(e11,e12) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e11)
& op1(e10,e12) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e11)
& op1(e12,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e11,e13)
& op1(e12,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e11,e12)
& op1(e12,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e11,e11)
& op1(e12,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e11,e10) ),
file('theBenchmark.p',ax5) ).
fof(ax6,axiom,
( op2(e23,e22) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e21)
& op2(e22,e22) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e21)
& op2(e21,e22) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e21)
& op2(e20,e22) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e21)
& op2(e22,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e21,e23)
& op2(e22,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e21,e22)
& op2(e22,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e21,e21)
& op2(e22,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e21,e20) ),
file('theBenchmark.p',ax6) ).
fof(ax7,axiom,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('theBenchmark.p',ax7) ).
fof(ax8,axiom,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('theBenchmark.p',ax8) ).
fof(ax10,axiom,
( ( ( op1(e13,op1(e13,e13)) = op1(e13,e13)
& op1(e13,op1(e12,e13)) = op1(e12,e13)
& op1(e13,op1(e11,e13)) = op1(e11,e13)
& op1(e13,op1(e10,e13)) = op1(e10,e13) )
| ( op1(e12,op1(e13,e12)) = op1(e13,e12)
& op1(e12,op1(e12,e12)) = op1(e12,e12)
& op1(e12,op1(e11,e12)) = op1(e11,e12)
& op1(e12,op1(e10,e12)) = op1(e10,e12) )
| ( op1(e11,op1(e13,e11)) = op1(e13,e11)
& op1(e11,op1(e12,e11)) = op1(e12,e11)
& op1(e11,op1(e11,e11)) = op1(e11,e11)
& op1(e11,op1(e10,e11)) = op1(e10,e11) )
| ( op1(e10,op1(e13,e10)) = op1(e13,e10)
& op1(e10,op1(e12,e10)) = op1(e12,e10)
& op1(e10,op1(e11,e10)) = op1(e11,e10)
& op1(e10,op1(e10,e10)) = op1(e10,e10) ) )
& op1(op1(e13,e13),e13) = e13
& op1(op1(e13,e12),e13) = e12
& op1(op1(e13,e11),e13) = e11
& op1(op1(e13,e10),e13) = e10
& op1(op1(e12,e13),e12) = e13
& op1(op1(e12,e12),e12) = e12
& op1(op1(e12,e11),e12) = e11
& op1(op1(e12,e10),e12) = e10
& op1(op1(e11,e13),e11) = e13
& op1(op1(e11,e12),e11) = e12
& op1(op1(e11,e11),e11) = e11
& op1(op1(e11,e10),e11) = e10
& op1(op1(e10,e13),e10) = e13
& op1(op1(e10,e12),e10) = e12
& op1(op1(e10,e11),e10) = e11
& op1(op1(e10,e10),e10) = e10 ),
file('theBenchmark.p',ax10) ).
fof(ax11,axiom,
( ( ( op2(e23,op2(e23,e23)) = op2(e23,e23)
& op2(e23,op2(e22,e23)) = op2(e22,e23)
& op2(e23,op2(e21,e23)) = op2(e21,e23)
& op2(e23,op2(e20,e23)) = op2(e20,e23) )
| ( op2(e22,op2(e23,e22)) = op2(e23,e22)
& op2(e22,op2(e22,e22)) = op2(e22,e22)
& op2(e22,op2(e21,e22)) = op2(e21,e22)
& op2(e22,op2(e20,e22)) = op2(e20,e22) )
| ( op2(e21,op2(e23,e21)) = op2(e23,e21)
& op2(e21,op2(e22,e21)) = op2(e22,e21)
& op2(e21,op2(e21,e21)) = op2(e21,e21)
& op2(e21,op2(e20,e21)) = op2(e20,e21) )
| ( op2(e20,op2(e23,e20)) = op2(e23,e20)
& op2(e20,op2(e22,e20)) = op2(e22,e20)
& op2(e20,op2(e21,e20)) = op2(e21,e20)
& op2(e20,op2(e20,e20)) = op2(e20,e20) ) )
& op2(op2(e23,e23),e23) = e23
& op2(op2(e23,e22),e23) = e22
& op2(op2(e23,e21),e23) = e21
& op2(op2(e23,e20),e23) = e20
& op2(op2(e22,e23),e22) = e23
& op2(op2(e22,e22),e22) = e22
& op2(op2(e22,e21),e22) = e21
& op2(op2(e22,e20),e22) = e20
& op2(op2(e21,e23),e21) = e23
& op2(op2(e21,e22),e21) = e22
& op2(op2(e21,e21),e21) = e21
& op2(op2(e21,e20),e21) = e20
& op2(op2(e20,e23),e20) = e23
& op2(op2(e20,e22),e20) = e22
& op2(op2(e20,e21),e20) = e21
& op2(op2(e20,e20),e20) = e20 ),
file('theBenchmark.p',ax11) ).
fof(ax12,axiom,
( e13 = op1(e12,e11)
& e10 = op1(op1(e12,e11),op1(e12,e11)) ),
file('theBenchmark.p',ax12) ).
fof(ax13,axiom,
( e23 = op2(e22,e21)
& e20 = op2(op2(e22,e21),op2(e22,e21)) ),
file('theBenchmark.p',ax13) ).
fof(ax14,axiom,
( h1(e13) = op2(e21,e20)
& h1(e10) = op2(op2(e21,e20),op2(e21,e20))
& h1(e12) = e21
& h1(e11) = e20 ),
file('theBenchmark.p',ax14) ).
fof(ax15,axiom,
( h2(e13) = op2(e22,e20)
& h2(e10) = op2(op2(e22,e20),op2(e22,e20))
& h2(e12) = e22
& h2(e11) = e20 ),
file('theBenchmark.p',ax15) ).
fof(ax16,axiom,
( h3(e13) = op2(e23,e20)
& h3(e10) = op2(op2(e23,e20),op2(e23,e20))
& h3(e12) = e23
& h3(e11) = e20 ),
file('theBenchmark.p',ax16) ).
fof(ax17,axiom,
( h4(e13) = op2(e20,e21)
& h4(e10) = op2(op2(e20,e21),op2(e20,e21))
& h4(e12) = e20
& h4(e11) = e21 ),
file('theBenchmark.p',ax17) ).
fof(ax18,axiom,
( h5(e13) = op2(e22,e21)
& h5(e10) = op2(op2(e22,e21),op2(e22,e21))
& h5(e12) = e22
& h5(e11) = e21 ),
file('theBenchmark.p',ax18) ).
fof(ax19,axiom,
( h6(e13) = op2(e23,e21)
& h6(e10) = op2(op2(e23,e21),op2(e23,e21))
& h6(e12) = e23
& h6(e11) = e21 ),
file('theBenchmark.p',ax19) ).
fof(ax20,axiom,
( h7(e13) = op2(e20,e22)
& h7(e10) = op2(op2(e20,e22),op2(e20,e22))
& h7(e12) = e20
& h7(e11) = e22 ),
file('theBenchmark.p',ax20) ).
fof(ax21,axiom,
( h8(e13) = op2(e21,e22)
& h8(e10) = op2(op2(e21,e22),op2(e21,e22))
& h8(e12) = e21
& h8(e11) = e22 ),
file('theBenchmark.p',ax21) ).
fof(ax22,axiom,
( h9(e13) = op2(e23,e22)
& h9(e10) = op2(op2(e23,e22),op2(e23,e22))
& h9(e12) = e23
& h9(e11) = e22 ),
file('theBenchmark.p',ax22) ).
fof(ax23,axiom,
( h10(e13) = op2(e20,e23)
& h10(e10) = op2(op2(e20,e23),op2(e20,e23))
& h10(e12) = e20
& h10(e11) = e23 ),
file('theBenchmark.p',ax23) ).
fof(ax24,axiom,
( h11(e13) = op2(e21,e23)
& h11(e10) = op2(op2(e21,e23),op2(e21,e23))
& h11(e12) = e21
& h11(e11) = e23 ),
file('theBenchmark.p',ax24) ).
fof(ax25,axiom,
( h12(e13) = op2(e22,e23)
& h12(e10) = op2(op2(e22,e23),op2(e22,e23))
& h12(e12) = e22
& h12(e11) = e23 ),
file('theBenchmark.p',ax25) ).
fof(co1,conjecture,
( ( ( h12(e13) = e23
| h12(e12) = e23
| h12(e11) = e23
| h12(e10) = e23 )
& ( h12(e13) = e22
| h12(e12) = e22
| h12(e11) = e22
| h12(e10) = e22 )
& ( h12(e13) = e21
| h12(e12) = e21
| h12(e11) = e21
| h12(e10) = e21 )
& ( h12(e13) = e20
| h12(e12) = e20
| h12(e11) = e20
| h12(e10) = e20 )
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e10)) = op2(h12(e10),h12(e10)) )
| ( ( h11(e13) = e23
| h11(e12) = e23
| h11(e11) = e23
| h11(e10) = e23 )
& ( h11(e13) = e22
| h11(e12) = e22
| h11(e11) = e22
| h11(e10) = e22 )
& ( h11(e13) = e21
| h11(e12) = e21
| h11(e11) = e21
| h11(e10) = e21 )
& ( h11(e13) = e20
| h11(e12) = e20
| h11(e11) = e20
| h11(e10) = e20 )
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e10)) = op2(h11(e10),h11(e10)) )
| ( ( h10(e13) = e23
| h10(e12) = e23
| h10(e11) = e23
| h10(e10) = e23 )
& ( h10(e13) = e22
| h10(e12) = e22
| h10(e11) = e22
| h10(e10) = e22 )
& ( h10(e13) = e21
| h10(e12) = e21
| h10(e11) = e21
| h10(e10) = e21 )
& ( h10(e13) = e20
| h10(e12) = e20
| h10(e11) = e20
| h10(e10) = e20 )
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e10)) = op2(h10(e10),h10(e10)) )
| ( ( h9(e13) = e23
| h9(e12) = e23
| h9(e11) = e23
| h9(e10) = e23 )
& ( h9(e13) = e22
| h9(e12) = e22
| h9(e11) = e22
| h9(e10) = e22 )
& ( h9(e13) = e21
| h9(e12) = e21
| h9(e11) = e21
| h9(e10) = e21 )
& ( h9(e13) = e20
| h9(e12) = e20
| h9(e11) = e20
| h9(e10) = e20 )
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e10)) = op2(h9(e10),h9(e10)) )
| ( ( h8(e13) = e23
| h8(e12) = e23
| h8(e11) = e23
| h8(e10) = e23 )
& ( h8(e13) = e22
| h8(e12) = e22
| h8(e11) = e22
| h8(e10) = e22 )
& ( h8(e13) = e21
| h8(e12) = e21
| h8(e11) = e21
| h8(e10) = e21 )
& ( h8(e13) = e20
| h8(e12) = e20
| h8(e11) = e20
| h8(e10) = e20 )
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e10)) = op2(h8(e10),h8(e10)) )
| ( ( h7(e13) = e23
| h7(e12) = e23
| h7(e11) = e23
| h7(e10) = e23 )
& ( h7(e13) = e22
| h7(e12) = e22
| h7(e11) = e22
| h7(e10) = e22 )
& ( h7(e13) = e21
| h7(e12) = e21
| h7(e11) = e21
| h7(e10) = e21 )
& ( h7(e13) = e20
| h7(e12) = e20
| h7(e11) = e20
| h7(e10) = e20 )
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e10)) = op2(h7(e10),h7(e10)) )
| ( ( h6(e13) = e23
| h6(e12) = e23
| h6(e11) = e23
| h6(e10) = e23 )
& ( h6(e13) = e22
| h6(e12) = e22
| h6(e11) = e22
| h6(e10) = e22 )
& ( h6(e13) = e21
| h6(e12) = e21
| h6(e11) = e21
| h6(e10) = e21 )
& ( h6(e13) = e20
| h6(e12) = e20
| h6(e11) = e20
| h6(e10) = e20 )
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e10)) = op2(h6(e10),h6(e10)) )
| ( ( h5(e13) = e23
| h5(e12) = e23
| h5(e11) = e23
| h5(e10) = e23 )
& ( h5(e13) = e22
| h5(e12) = e22
| h5(e11) = e22
| h5(e10) = e22 )
& ( h5(e13) = e21
| h5(e12) = e21
| h5(e11) = e21
| h5(e10) = e21 )
& ( h5(e13) = e20
| h5(e12) = e20
| h5(e11) = e20
| h5(e10) = e20 )
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e10)) = op2(h5(e10),h5(e10)) )
| ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ( ( ( h12(e13) = e23
| h12(e12) = e23
| h12(e11) = e23
| h12(e10) = e23 )
& ( h12(e13) = e22
| h12(e12) = e22
| h12(e11) = e22
| h12(e10) = e22 )
& ( h12(e13) = e21
| h12(e12) = e21
| h12(e11) = e21
| h12(e10) = e21 )
& ( h12(e13) = e20
| h12(e12) = e20
| h12(e11) = e20
| h12(e10) = e20 )
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e10)) = op2(h12(e10),h12(e10)) )
| ( ( h11(e13) = e23
| h11(e12) = e23
| h11(e11) = e23
| h11(e10) = e23 )
& ( h11(e13) = e22
| h11(e12) = e22
| h11(e11) = e22
| h11(e10) = e22 )
& ( h11(e13) = e21
| h11(e12) = e21
| h11(e11) = e21
| h11(e10) = e21 )
& ( h11(e13) = e20
| h11(e12) = e20
| h11(e11) = e20
| h11(e10) = e20 )
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e10)) = op2(h11(e10),h11(e10)) )
| ( ( h10(e13) = e23
| h10(e12) = e23
| h10(e11) = e23
| h10(e10) = e23 )
& ( h10(e13) = e22
| h10(e12) = e22
| h10(e11) = e22
| h10(e10) = e22 )
& ( h10(e13) = e21
| h10(e12) = e21
| h10(e11) = e21
| h10(e10) = e21 )
& ( h10(e13) = e20
| h10(e12) = e20
| h10(e11) = e20
| h10(e10) = e20 )
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e10)) = op2(h10(e10),h10(e10)) )
| ( ( h9(e13) = e23
| h9(e12) = e23
| h9(e11) = e23
| h9(e10) = e23 )
& ( h9(e13) = e22
| h9(e12) = e22
| h9(e11) = e22
| h9(e10) = e22 )
& ( h9(e13) = e21
| h9(e12) = e21
| h9(e11) = e21
| h9(e10) = e21 )
& ( h9(e13) = e20
| h9(e12) = e20
| h9(e11) = e20
| h9(e10) = e20 )
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e10)) = op2(h9(e10),h9(e10)) )
| ( ( h8(e13) = e23
| h8(e12) = e23
| h8(e11) = e23
| h8(e10) = e23 )
& ( h8(e13) = e22
| h8(e12) = e22
| h8(e11) = e22
| h8(e10) = e22 )
& ( h8(e13) = e21
| h8(e12) = e21
| h8(e11) = e21
| h8(e10) = e21 )
& ( h8(e13) = e20
| h8(e12) = e20
| h8(e11) = e20
| h8(e10) = e20 )
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e10)) = op2(h8(e10),h8(e10)) )
| ( ( h7(e13) = e23
| h7(e12) = e23
| h7(e11) = e23
| h7(e10) = e23 )
& ( h7(e13) = e22
| h7(e12) = e22
| h7(e11) = e22
| h7(e10) = e22 )
& ( h7(e13) = e21
| h7(e12) = e21
| h7(e11) = e21
| h7(e10) = e21 )
& ( h7(e13) = e20
| h7(e12) = e20
| h7(e11) = e20
| h7(e10) = e20 )
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e10)) = op2(h7(e10),h7(e10)) )
| ( ( h6(e13) = e23
| h6(e12) = e23
| h6(e11) = e23
| h6(e10) = e23 )
& ( h6(e13) = e22
| h6(e12) = e22
| h6(e11) = e22
| h6(e10) = e22 )
& ( h6(e13) = e21
| h6(e12) = e21
| h6(e11) = e21
| h6(e10) = e21 )
& ( h6(e13) = e20
| h6(e12) = e20
| h6(e11) = e20
| h6(e10) = e20 )
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e10)) = op2(h6(e10),h6(e10)) )
| ( ( h5(e13) = e23
| h5(e12) = e23
| h5(e11) = e23
| h5(e10) = e23 )
& ( h5(e13) = e22
| h5(e12) = e22
| h5(e11) = e22
| h5(e10) = e22 )
& ( h5(e13) = e21
| h5(e12) = e21
| h5(e11) = e21
| h5(e10) = e21 )
& ( h5(e13) = e20
| h5(e12) = e20
| h5(e11) = e20
| h5(e10) = e20 )
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e10)) = op2(h5(e10),h5(e10)) )
| ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_43,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_45,plain,
( op1(e10,e13) = e11
| op1(e10,e12) = e11
| op1(e10,e11) = e11
| op1(e10,e10) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_52,plain,
( op1(e13,e11) = e10
| op1(e12,e11) = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_59,plain,
( op1(e12,e13) = e10
| op1(e12,e12) = e10
| op1(e12,e11) = e10
| op1(e12,e10) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_63,plain,
( op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_64,plain,
( op1(e13,e12) = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_66,plain,
( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| op1(e10,e12) = e13 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_71,plain,
( op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_73,plain,
( op1(e13,e13) = e13
| op1(e13,e12) = e13
| op1(e13,e11) = e13
| op1(e13,e10) = e13 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_91,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_93,plain,
( op2(e20,e23) = e21
| op2(e20,e22) = e21
| op2(e20,e21) = e21
| op2(e20,e20) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_95,plain,
( op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| op2(e20,e20) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_100,plain,
( op2(e23,e21) = e20
| op2(e22,e21) = e20
| op2(e21,e21) = e20
| op2(e20,e21) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_108,plain,
( op2(e23,e22) = e20
| op2(e22,e22) = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_119,plain,
( op2(e23,e23) = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_121,plain,
( op2(e23,e23) = e23
| op2(e23,e22) = e23
| op2(e23,e21) = e23
| op2(e23,e20) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_125,plain,
op1(e12,e10) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_126,plain,
op1(e10,e10) != op1(e12,e10),
inference(copy,[status(thm)],[c_125]) ).
cnf(c_138,plain,
op1(e13,e11) != op1(e12,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_143,plain,
op1(e13,e12) != op1(e10,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_154,plain,
op1(e13,e13) != op1(e12,e13),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_155,plain,
op1(e10,e11) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_156,plain,
op1(e10,e10) != op1(e10,e11),
inference(copy,[status(thm)],[c_155]) ).
cnf(c_162,plain,
op1(e10,e13) != op1(e10,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_176,plain,
op1(e12,e12) != op1(e12,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_199,plain,
op2(e23,e21) != op2(e20,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_202,plain,
op2(e23,e21) != op2(e22,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_207,plain,
op2(e23,e22) != op2(e20,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_219,plain,
op2(e20,e21) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_220,plain,
op2(e20,e20) != op2(e20,e21),
inference(copy,[status(thm)],[c_219]) ).
cnf(c_221,plain,
op2(e20,e22) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_222,plain,
op2(e20,e20) != op2(e20,e22),
inference(copy,[status(thm)],[c_221]) ).
cnf(c_251,plain,
e11 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_252,plain,
e10 != e11,
inference(copy,[status(thm)],[c_251]) ).
cnf(c_253,plain,
e12 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_254,plain,
e10 != e12,
inference(copy,[status(thm)],[c_253]) ).
cnf(c_255,plain,
e13 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_256,plain,
e12 != e11,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_257,plain,
e13 != e11,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_258,plain,
e13 != e12,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_259,plain,
e21 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_260,plain,
e20 != e21,
inference(copy,[status(thm)],[c_259]) ).
cnf(c_261,plain,
e22 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_262,plain,
e20 != e22,
inference(copy,[status(thm)],[c_261]) ).
cnf(c_263,plain,
e23 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_264,plain,
e22 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_265,plain,
e23 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_266,plain,
e23 != e22,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_300,plain,
op1(op1(e10,e11),e10) = e11,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_308,plain,
op1(op1(e12,e11),e12) = e11,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_312,plain,
op1(op1(e13,e11),e13) = e11,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_313,plain,
op1(op1(e13,e12),e13) = e12,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_314,plain,
op1(op1(e13,e13),e13) = e13,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_379,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| op1(e13,e12) = op1(e12,op1(e13,e12))
| op1(e12,e11) = op1(e11,op1(e12,e11))
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_5233,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| op1(e13,e12) = op1(e12,op1(e13,e12))
| op1(e11,op1(e12,e11)) = op1(e12,e11)
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(copy,[status(thm)],[c_379]) ).
cnf(c_380,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| op1(e12,op1(e13,e12)) = op1(e13,e12)
| op1(e11,op1(e12,e11)) = op1(e12,e11)
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(copy,[status(thm)],[c_5233]) ).
cnf(c_635,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| op1(e13,e12) = op1(e12,op1(e13,e12))
| op1(e12,e11) = op1(e11,op1(e12,e11))
| op1(e12,e10) = op1(e10,op1(e12,e10)) ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_5234,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| op1(e13,e12) = op1(e12,op1(e13,e12))
| op1(e12,e11) = op1(e11,op1(e12,e11))
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(copy,[status(thm)],[c_635]) ).
cnf(c_5235,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| op1(e13,e12) = op1(e12,op1(e13,e12))
| op1(e11,op1(e12,e11)) = op1(e12,e11)
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(copy,[status(thm)],[c_5234]) ).
cnf(c_636,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| op1(e12,op1(e13,e12)) = op1(e13,e12)
| op1(e11,op1(e12,e11)) = op1(e12,e11)
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(copy,[status(thm)],[c_5235]) ).
cnf(c_804,plain,
op2(op2(e20,e21),e20) = e21,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_805,plain,
op2(op2(e20,e22),e20) = e22,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_812,plain,
op2(op2(e22,e21),e22) = e21,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_814,plain,
op2(op2(e22,e23),e22) = e23,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_816,plain,
op2(op2(e23,e21),e23) = e21,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_817,plain,
op2(op2(e23,e22),e23) = e22,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_818,plain,
op2(op2(e23,e23),e23) = e23,
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_883,plain,
( op2(e23,op2(e20,e23)) = op2(e20,e23)
| op2(e23,e22) = op2(e22,op2(e23,e22))
| op2(e22,e21) = op2(e21,op2(e22,e21))
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_5236,plain,
( op2(e23,op2(e20,e23)) = op2(e20,e23)
| op2(e23,e22) = op2(e22,op2(e23,e22))
| op2(e21,op2(e22,e21)) = op2(e22,e21)
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(copy,[status(thm)],[c_883]) ).
cnf(c_884,plain,
( op2(e23,op2(e20,e23)) = op2(e20,e23)
| op2(e22,op2(e23,e22)) = op2(e23,e22)
| op2(e21,op2(e22,e21)) = op2(e22,e21)
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(copy,[status(thm)],[c_5236]) ).
cnf(c_1307,plain,
op1(op1(e12,e11),op1(e12,e11)) = e10,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_1308,plain,
op1(e12,e11) = e13,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_1309,plain,
op2(op2(e22,e21),op2(e22,e21)) = e20,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_1310,plain,
op2(e22,e21) = e23,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_1315,plain,
h1(e13) = op2(e21,e20),
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_1316,plain,
op2(e21,e20) = h1(e13),
inference(copy,[status(thm)],[c_1315]) ).
cnf(c_1321,plain,
h2(e13) = op2(e22,e20),
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_1322,plain,
op2(e22,e20) = h2(e13),
inference(copy,[status(thm)],[c_1321]) ).
cnf(c_1327,plain,
h3(e13) = op2(e23,e20),
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_1328,plain,
op2(e23,e20) = h3(e13),
inference(copy,[status(thm)],[c_1327]) ).
cnf(c_1333,plain,
h4(e13) = op2(e20,e21),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_1334,plain,
op2(e20,e21) = h4(e13),
inference(copy,[status(thm)],[c_1333]) ).
cnf(c_1337,plain,
h5(e10) = op2(op2(e22,e21),op2(e22,e21)),
inference(clausify,[status(thm)],[ax18]) ).
cnf(c_5237,plain,
h5(e10) = op2(e23,op2(e22,e21)),
inference(paramod,[status(thm)],[c_1310,c_1337]) ).
cnf(c_5238,plain,
h5(e10) = op2(e23,e23),
inference(paramod,[status(thm)],[c_1310,c_5237]) ).
cnf(c_1338,plain,
op2(e23,e23) = h5(e10),
inference(copy,[status(thm)],[c_5238]) ).
cnf(c_1343,plain,
h6(e10) = op2(op2(e23,e21),op2(e23,e21)),
inference(clausify,[status(thm)],[ax19]) ).
cnf(c_1344,plain,
op2(op2(e23,e21),op2(e23,e21)) = h6(e10),
inference(copy,[status(thm)],[c_1343]) ).
cnf(c_1345,plain,
h6(e13) = op2(e23,e21),
inference(clausify,[status(thm)],[ax19]) ).
cnf(c_1346,plain,
op2(e23,e21) = h6(e13),
inference(copy,[status(thm)],[c_1345]) ).
cnf(c_1351,plain,
h7(e13) = op2(e20,e22),
inference(clausify,[status(thm)],[ax20]) ).
cnf(c_1352,plain,
op2(e20,e22) = h7(e13),
inference(copy,[status(thm)],[c_1351]) ).
cnf(c_1353,plain,
h8(e11) = e22,
inference(clausify,[status(thm)],[ax21]) ).
cnf(c_1354,plain,
h8(e12) = e21,
inference(clausify,[status(thm)],[ax21]) ).
cnf(c_1355,plain,
h8(e10) = op2(op2(e21,e22),op2(e21,e22)),
inference(clausify,[status(thm)],[ax21]) ).
cnf(c_1356,plain,
op2(op2(e21,e22),op2(e21,e22)) = h8(e10),
inference(copy,[status(thm)],[c_1355]) ).
cnf(c_1357,plain,
h8(e13) = op2(e21,e22),
inference(clausify,[status(thm)],[ax21]) ).
cnf(c_1358,plain,
op2(e21,e22) = h8(e13),
inference(copy,[status(thm)],[c_1357]) ).
cnf(c_1361,plain,
h9(e10) = op2(op2(e23,e22),op2(e23,e22)),
inference(clausify,[status(thm)],[ax22]) ).
cnf(c_1362,plain,
op2(op2(e23,e22),op2(e23,e22)) = h9(e10),
inference(copy,[status(thm)],[c_1361]) ).
cnf(c_1363,plain,
h9(e13) = op2(e23,e22),
inference(clausify,[status(thm)],[ax22]) ).
cnf(c_1364,plain,
op2(e23,e22) = h9(e13),
inference(copy,[status(thm)],[c_1363]) ).
cnf(c_1369,plain,
h10(e13) = op2(e20,e23),
inference(clausify,[status(thm)],[ax23]) ).
cnf(c_1370,plain,
op2(e20,e23) = h10(e13),
inference(copy,[status(thm)],[c_1369]) ).
cnf(c_1373,plain,
h11(e10) = op2(op2(e21,e23),op2(e21,e23)),
inference(clausify,[status(thm)],[ax24]) ).
cnf(c_1374,plain,
op2(op2(e21,e23),op2(e21,e23)) = h11(e10),
inference(copy,[status(thm)],[c_1373]) ).
cnf(c_1375,plain,
h11(e13) = op2(e21,e23),
inference(clausify,[status(thm)],[ax24]) ).
cnf(c_1376,plain,
op2(e21,e23) = h11(e13),
inference(copy,[status(thm)],[c_1375]) ).
cnf(c_1379,plain,
h12(e10) = op2(op2(e22,e23),op2(e22,e23)),
inference(clausify,[status(thm)],[ax25]) ).
cnf(c_1380,plain,
op2(op2(e22,e23),op2(e22,e23)) = h12(e10),
inference(copy,[status(thm)],[c_1379]) ).
cnf(c_1381,plain,
h12(e13) = op2(e22,e23),
inference(clausify,[status(thm)],[ax25]) ).
cnf(c_1382,plain,
op2(e22,e23) = h12(e13),
inference(copy,[status(thm)],[c_1381]) ).
cnf(c_3325,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| h8(op1(e11,e10)) != op2(h8(e11),h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),h8(e12))
| h8(op1(e10,e11)) != op2(h8(e10),h8(e11))
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_5239,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| h8(op1(e11,e10)) != op2(h8(e11),h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),h8(e12))
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1353,c_3325]) ).
cnf(c_5240,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| h8(op1(e11,e10)) != op2(h8(e11),h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1354,c_5239]) ).
cnf(c_5241,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1353,c_5240]) ).
cnf(c_5242,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e11)) != op2(e22,h8(e11))
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1353,c_5241]) ).
cnf(c_5243,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1353,c_5242]) ).
cnf(c_5244,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e11,e12)) != op2(e22,h8(e12))
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1353,c_5243]) ).
cnf(c_5245,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e11,e12)) != op2(e22,e21)
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1354,c_5244]) ).
cnf(c_5246,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1310,c_5245]) ).
cnf(c_5247,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1353,c_5246]) ).
cnf(c_5248,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1354,c_5247]) ).
cnf(c_5249,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(e13) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1308,c_5248]) ).
cnf(c_5250,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(e13) != op2(e21,h8(e11))
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1354,c_5249]) ).
cnf(c_5251,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(e13) != op2(e21,e22)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1353,c_5250]) ).
cnf(c_5252,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(e13) != h8(e13)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1358,c_5251]) ).
cnf(c_5253,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(e21,h8(e12))
| h8(e13) != h8(e13)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1354,c_5252]) ).
cnf(c_5254,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(e13) != h8(e13)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1354,c_5253]) ).
cnf(c_5255,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(e13) != h8(e13)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1354,c_5254]) ).
cnf(c_5256,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(e13) != h8(e13)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1353,c_5255]) ).
cnf(c_5257,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| h8(e12) != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(e13) != h8(e13)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1354,c_5256]) ).
cnf(c_5258,negated_conjecture,
( h8(e13) != e23
| h8(e11) != e22
| e21 != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(e13) != h8(e13)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1354,c_5257]) ).
cnf(c_5259,negated_conjecture,
( h8(e13) != e23
| e22 != e22
| e21 != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(e13) != h8(e13)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) ),
inference(paramod,[status(thm)],[c_1353,c_5258]) ).
cnf(c_5260,negated_conjecture,
( h8(e13) != e23
| e22 != e22
| e21 != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(e13) != h8(e13)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_5259]) ).
cnf(c_5261,negated_conjecture,
( h8(e13) != e23
| e22 != e22
| e21 != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(e13) != h8(e13)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),h8(e13)) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_5260]) ).
cnf(c_5262,negated_conjecture,
( h8(e13) != e23
| e22 != e22
| e21 != e21
| h8(e10) != e20
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(e13) != h8(e13)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),h8(e13)) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_5261]) ).
cnf(c_5263,negated_conjecture,
( h8(e13) != e23
| e22 != e22
| e21 != e21
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(e13) != h8(e13)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),h8(e13)) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_5262]) ).
cnf(c_5264,negated_conjecture,
( h8(e13) != e23
| e22 != e22
| e21 != e21
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),h8(e13)) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_5263]) ).
cnf(c_5265,negated_conjecture,
( h8(e13) != e23
| e22 != e22
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),h8(e13)) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_5264]) ).
cnf(c_3326,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),h8(e13)) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_5265]) ).
cnf(c_5266,plain,
op1(e13,op1(e12,e11)) = e10,
inference(paramod,[status(thm)],[c_1308,c_1307]) ).
cnf(c_4639,plain,
op1(e13,e13) = e10,
inference(paramod,[status(thm)],[c_1308,c_5266]) ).
cnf(c_5267,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| op1(e12,op1(e13,e12)) = op1(e13,e12)
| op1(e11,e13) = op1(e12,e11)
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(paramod,[status(thm)],[c_1308,c_636]) ).
cnf(c_4659,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| op1(e12,op1(e13,e12)) = op1(e13,e12)
| op1(e11,e13) = e13
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(paramod,[status(thm)],[c_1308,c_5267]) ).
cnf(c_5268,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| op1(e12,op1(e13,e12)) = op1(e13,e12)
| op1(e11,e13) = op1(e12,e11)
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(paramod,[status(thm)],[c_1308,c_380]) ).
cnf(c_4691,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| op1(e12,op1(e13,e12)) = op1(e13,e12)
| op1(e11,e13) = e13
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(paramod,[status(thm)],[c_1308,c_5268]) ).
cnf(c_4704,plain,
op1(e13,e12) = e11,
inference(paramod,[status(thm)],[c_1308,c_308]) ).
cnf(c_4706,plain,
op1(e12,e12) != e13,
inference(paramod,[status(thm)],[c_1308,c_176]) ).
cnf(c_4708,plain,
op1(e13,e11) != e13,
inference(paramod,[status(thm)],[c_1308,c_138]) ).
cnf(c_5269,plain,
( op1(e12,e13) = e12
| op1(e12,e12) = e12
| e13 = e12
| op1(e12,e10) = e12 ),
inference(paramod,[status(thm)],[c_1308,c_63]) ).
cnf(c_4711,plain,
( op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e10) = e12 ),
inference(resolve,[status(thm)],[c_258,c_5269]) ).
cnf(c_5270,plain,
( op1(e12,e13) = e10
| op1(e12,e12) = e10
| e13 = e10
| op1(e12,e10) = e10 ),
inference(paramod,[status(thm)],[c_1308,c_59]) ).
cnf(c_4713,plain,
( op1(e12,e13) = e10
| op1(e12,e12) = e10
| op1(e12,e10) = e10 ),
inference(resolve,[status(thm)],[c_255,c_5270]) ).
cnf(c_5271,plain,
( op1(e13,e11) = e10
| e13 = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 ),
inference(paramod,[status(thm)],[c_1308,c_52]) ).
cnf(c_4716,plain,
( op1(e13,e11) = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 ),
inference(resolve,[status(thm)],[c_255,c_5271]) ).
cnf(c_5272,plain,
op2(e23,op2(e22,e21)) = e20,
inference(paramod,[status(thm)],[c_1310,c_1309]) ).
cnf(c_5273,plain,
op2(e23,e23) = e20,
inference(paramod,[status(thm)],[c_1310,c_5272]) ).
cnf(c_4717,plain,
h5(e10) = e20,
inference(paramod,[status(thm)],[c_1338,c_5273]) ).
cnf(c_5274,plain,
( op2(e23,op2(e20,e23)) = op2(e20,e23)
| op2(e22,op2(e23,e22)) = op2(e23,e22)
| op2(e21,e23) = op2(e22,e21)
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1310,c_884]) ).
cnf(c_5275,plain,
( op2(e23,op2(e20,e23)) = op2(e20,e23)
| op2(e22,op2(e23,e22)) = op2(e23,e22)
| h11(e13) = op2(e22,e21)
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1376,c_5274]) ).
cnf(c_5276,plain,
( op2(e23,op2(e20,e23)) = op2(e20,e23)
| op2(e22,op2(e23,e22)) = op2(e23,e22)
| h11(e13) = e23
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1310,c_5275]) ).
cnf(c_5277,plain,
( op2(e23,op2(e20,e23)) = op2(e20,e23)
| op2(e22,h9(e13)) = op2(e23,e22)
| h11(e13) = e23
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1364,c_5276]) ).
cnf(c_5278,plain,
( op2(e23,op2(e20,e23)) = op2(e20,e23)
| op2(e22,h9(e13)) = h9(e13)
| h11(e13) = e23
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1364,c_5277]) ).
cnf(c_5279,plain,
( op2(e23,h10(e13)) = op2(e20,e23)
| op2(e22,h9(e13)) = h9(e13)
| h11(e13) = e23
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1370,c_5278]) ).
cnf(c_4769,plain,
( op2(e23,h10(e13)) = h10(e13)
| op2(e22,h9(e13)) = h9(e13)
| h11(e13) = e23
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1370,c_5279]) ).
cnf(c_5280,plain,
op2(e23,e22) = e21,
inference(paramod,[status(thm)],[c_1310,c_812]) ).
cnf(c_4782,plain,
h9(e13) = e21,
inference(paramod,[status(thm)],[c_1364,c_5280]) ).
cnf(c_5281,plain,
h6(e13) != op2(e22,e21),
inference(paramod,[status(thm)],[c_1346,c_202]) ).
cnf(c_4786,plain,
h6(e13) != e23,
inference(paramod,[status(thm)],[c_1310,c_5281]) ).
cnf(c_5282,plain,
( op2(e23,e21) = e20
| op2(e22,e21) = e20
| op2(e21,e21) = e20
| h4(e13) = e20 ),
inference(paramod,[status(thm)],[c_1334,c_100]) ).
cnf(c_5283,plain,
( op2(e23,e21) = e20
| e23 = e20
| op2(e21,e21) = e20
| h4(e13) = e20 ),
inference(paramod,[status(thm)],[c_1310,c_5282]) ).
cnf(c_5284,plain,
( h6(e13) = e20
| e23 = e20
| op2(e21,e21) = e20
| h4(e13) = e20 ),
inference(paramod,[status(thm)],[c_1346,c_5283]) ).
cnf(c_4794,plain,
( h6(e13) = e20
| op2(e21,e21) = e20
| h4(e13) = e20 ),
inference(resolve,[status(thm)],[c_263,c_5284]) ).
cnf(c_5285,plain,
( op2(e23,e23) = e23
| op2(e23,e22) = e23
| op2(e23,e21) = e23
| h3(e13) = e23 ),
inference(paramod,[status(thm)],[c_1328,c_121]) ).
cnf(c_5286,plain,
( op2(e23,e23) = e23
| op2(e23,e22) = e23
| h6(e13) = e23
| h3(e13) = e23 ),
inference(paramod,[status(thm)],[c_1346,c_5285]) ).
cnf(c_5287,plain,
( op2(e23,e23) = e23
| h9(e13) = e23
| h6(e13) = e23
| h3(e13) = e23 ),
inference(paramod,[status(thm)],[c_1364,c_5286]) ).
cnf(c_5288,plain,
( op2(e23,e23) = e23
| e21 = e23
| h6(e13) = e23
| h3(e13) = e23 ),
inference(paramod,[status(thm)],[c_4782,c_5287]) ).
cnf(c_5289,plain,
( h5(e10) = e23
| e21 = e23
| h6(e13) = e23
| h3(e13) = e23 ),
inference(paramod,[status(thm)],[c_1338,c_5288]) ).
cnf(c_5290,plain,
( e20 = e23
| e21 = e23
| h6(e13) = e23
| h3(e13) = e23 ),
inference(paramod,[status(thm)],[c_4717,c_5289]) ).
cnf(c_5291,plain,
( e20 = e23
| e23 = e21
| h6(e13) = e23
| h3(e13) = e23 ),
inference(copy,[status(thm)],[c_5290]) ).
cnf(c_5292,plain,
( e23 = e20
| e23 = e21
| h6(e13) = e23
| h3(e13) = e23 ),
inference(copy,[status(thm)],[c_5291]) ).
cnf(c_5293,plain,
( e23 = e20
| e23 = e21
| h3(e13) = e23 ),
inference(resolve,[status(thm)],[c_4786,c_5292]) ).
cnf(c_5294,plain,
( e23 = e20
| h3(e13) = e23 ),
inference(resolve,[status(thm)],[c_265,c_5293]) ).
cnf(c_4861,plain,
h3(e13) = e23,
inference(resolve,[status(thm)],[c_263,c_5294]) ).
cnf(c_5295,plain,
( op2(e23,e23) = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| h3(e13) = e22 ),
inference(paramod,[status(thm)],[c_1328,c_119]) ).
cnf(c_5296,plain,
( op2(e23,e23) = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_4861,c_5295]) ).
cnf(c_5297,plain,
( op2(e23,e23) = e22
| op2(e23,e22) = e22
| h6(e13) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_1346,c_5296]) ).
cnf(c_5298,plain,
( op2(e23,e23) = e22
| h9(e13) = e22
| h6(e13) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_1364,c_5297]) ).
cnf(c_5299,plain,
( op2(e23,e23) = e22
| e21 = e22
| h6(e13) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_4782,c_5298]) ).
cnf(c_5300,plain,
( h5(e10) = e22
| e21 = e22
| h6(e13) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_1338,c_5299]) ).
cnf(c_5301,plain,
( e20 = e22
| e21 = e22
| h6(e13) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_4717,c_5300]) ).
cnf(c_5302,plain,
( e20 = e22
| e22 = e21
| h6(e13) = e22
| e23 = e22 ),
inference(copy,[status(thm)],[c_5301]) ).
cnf(c_5303,plain,
( e20 = e22
| e22 = e21
| h6(e13) = e22 ),
inference(resolve,[status(thm)],[c_266,c_5302]) ).
cnf(c_5304,plain,
( e20 = e22
| h6(e13) = e22 ),
inference(resolve,[status(thm)],[c_264,c_5303]) ).
cnf(c_4862,plain,
h6(e13) = e22,
inference(resolve,[status(thm)],[c_262,c_5304]) ).
cnf(c_4865,plain,
op2(h4(e13),e20) = e21,
inference(paramod,[status(thm)],[c_1334,c_804]) ).
cnf(c_4868,plain,
op2(e20,e20) != h4(e13),
inference(paramod,[status(thm)],[c_1334,c_220]) ).
cnf(c_5305,plain,
h6(e13) != op2(e20,e21),
inference(paramod,[status(thm)],[c_1346,c_199]) ).
cnf(c_5306,plain,
e22 != op2(e20,e21),
inference(paramod,[status(thm)],[c_4862,c_5305]) ).
cnf(c_5307,plain,
e22 != h4(e13),
inference(paramod,[status(thm)],[c_1334,c_5306]) ).
cnf(c_4869,plain,
h4(e13) != e22,
inference(copy,[status(thm)],[c_5307]) ).
cnf(c_5308,plain,
( op2(e20,e23) = e22
| op2(e20,e22) = e22
| h4(e13) = e22
| op2(e20,e20) = e22 ),
inference(paramod,[status(thm)],[c_1334,c_95]) ).
cnf(c_5309,plain,
( op2(e20,e23) = e22
| h7(e13) = e22
| h4(e13) = e22
| op2(e20,e20) = e22 ),
inference(paramod,[status(thm)],[c_1352,c_5308]) ).
cnf(c_5310,plain,
( h10(e13) = e22
| h7(e13) = e22
| h4(e13) = e22
| op2(e20,e20) = e22 ),
inference(paramod,[status(thm)],[c_1370,c_5309]) ).
cnf(c_4872,plain,
( h10(e13) = e22
| h7(e13) = e22
| op2(e20,e20) = e22 ),
inference(resolve,[status(thm)],[c_4869,c_5310]) ).
cnf(c_5311,plain,
( op2(e20,e23) = e21
| op2(e20,e22) = e21
| h4(e13) = e21
| op2(e20,e20) = e21 ),
inference(paramod,[status(thm)],[c_1334,c_93]) ).
cnf(c_5312,plain,
( op2(e20,e23) = e21
| h7(e13) = e21
| h4(e13) = e21
| op2(e20,e20) = e21 ),
inference(paramod,[status(thm)],[c_1352,c_5311]) ).
cnf(c_4873,plain,
( h10(e13) = e21
| h7(e13) = e21
| h4(e13) = e21
| op2(e20,e20) = e21 ),
inference(paramod,[status(thm)],[c_1370,c_5312]) ).
cnf(c_5313,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| h4(e13) = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_1334,c_91]) ).
cnf(c_5314,plain,
( op2(e20,e23) = e20
| h7(e13) = e20
| h4(e13) = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_1352,c_5313]) ).
cnf(c_4874,plain,
( h10(e13) = e20
| h7(e13) = e20
| h4(e13) = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_1370,c_5314]) ).
cnf(c_5315,plain,
op2(h5(e10),e23) = e23,
inference(paramod,[status(thm)],[c_1338,c_818]) ).
cnf(c_5316,plain,
op2(e20,e23) = e23,
inference(paramod,[status(thm)],[c_4717,c_5315]) ).
cnf(c_4878,plain,
h10(e13) = e23,
inference(paramod,[status(thm)],[c_1370,c_5316]) ).
cnf(c_5317,plain,
op2(h6(e13),op2(e23,e21)) = h6(e10),
inference(paramod,[status(thm)],[c_1346,c_1344]) ).
cnf(c_5318,plain,
op2(e22,op2(e23,e21)) = h6(e10),
inference(paramod,[status(thm)],[c_4862,c_5317]) ).
cnf(c_5319,plain,
op2(e22,h6(e13)) = h6(e10),
inference(paramod,[status(thm)],[c_1346,c_5318]) ).
cnf(c_4883,plain,
op2(e22,e22) = h6(e10),
inference(paramod,[status(thm)],[c_4862,c_5319]) ).
cnf(c_5320,plain,
op2(h6(e13),e23) = e21,
inference(paramod,[status(thm)],[c_1346,c_816]) ).
cnf(c_5321,plain,
op2(e22,e23) = e21,
inference(paramod,[status(thm)],[c_4862,c_5320]) ).
cnf(c_4884,plain,
h12(e13) = e21,
inference(paramod,[status(thm)],[c_1382,c_5321]) ).
cnf(c_4887,plain,
op2(h7(e13),e20) = e22,
inference(paramod,[status(thm)],[c_1352,c_805]) ).
cnf(c_4889,plain,
op2(e20,e20) != h7(e13),
inference(paramod,[status(thm)],[c_1352,c_222]) ).
cnf(c_5322,plain,
h9(e13) != op2(e20,e22),
inference(paramod,[status(thm)],[c_1364,c_207]) ).
cnf(c_5323,plain,
e21 != op2(e20,e22),
inference(paramod,[status(thm)],[c_4782,c_5322]) ).
cnf(c_5324,plain,
e21 != h7(e13),
inference(paramod,[status(thm)],[c_1352,c_5323]) ).
cnf(c_4890,plain,
h7(e13) != e21,
inference(copy,[status(thm)],[c_5324]) ).
cnf(c_5325,plain,
( op2(e23,e22) = e20
| op2(e22,e22) = e20
| op2(e21,e22) = e20
| h7(e13) = e20 ),
inference(paramod,[status(thm)],[c_1352,c_108]) ).
cnf(c_5326,plain,
( op2(e23,e22) = e20
| op2(e22,e22) = e20
| h8(e13) = e20
| h7(e13) = e20 ),
inference(paramod,[status(thm)],[c_1358,c_5325]) ).
cnf(c_5327,plain,
( op2(e23,e22) = e20
| h6(e10) = e20
| h8(e13) = e20
| h7(e13) = e20 ),
inference(paramod,[status(thm)],[c_4883,c_5326]) ).
cnf(c_5328,plain,
( h9(e13) = e20
| h6(e10) = e20
| h8(e13) = e20
| h7(e13) = e20 ),
inference(paramod,[status(thm)],[c_1364,c_5327]) ).
cnf(c_5329,plain,
( e21 = e20
| h6(e10) = e20
| h8(e13) = e20
| h7(e13) = e20 ),
inference(paramod,[status(thm)],[c_4782,c_5328]) ).
cnf(c_5330,plain,
( e20 = e21
| h6(e10) = e20
| h8(e13) = e20
| h7(e13) = e20 ),
inference(copy,[status(thm)],[c_5329]) ).
cnf(c_4895,plain,
( h6(e10) = e20
| h8(e13) = e20
| h7(e13) = e20 ),
inference(resolve,[status(thm)],[c_260,c_5330]) ).
cnf(c_5331,plain,
op2(h8(e13),op2(e21,e22)) = h8(e10),
inference(paramod,[status(thm)],[c_1358,c_1356]) ).
cnf(c_4897,plain,
op2(h8(e13),h8(e13)) = h8(e10),
inference(paramod,[status(thm)],[c_1358,c_5331]) ).
cnf(c_5332,plain,
op2(h9(e13),op2(e23,e22)) = h9(e10),
inference(paramod,[status(thm)],[c_1364,c_1362]) ).
cnf(c_5333,plain,
op2(e21,op2(e23,e22)) = h9(e10),
inference(paramod,[status(thm)],[c_4782,c_5332]) ).
cnf(c_5334,plain,
op2(e21,h9(e13)) = h9(e10),
inference(paramod,[status(thm)],[c_1364,c_5333]) ).
cnf(c_4904,plain,
op2(e21,e21) = h9(e10),
inference(paramod,[status(thm)],[c_4782,c_5334]) ).
cnf(c_5335,plain,
op2(h9(e13),e23) = e22,
inference(paramod,[status(thm)],[c_1364,c_817]) ).
cnf(c_5336,plain,
op2(e21,e23) = e22,
inference(paramod,[status(thm)],[c_4782,c_5335]) ).
cnf(c_4906,plain,
h11(e13) = e22,
inference(paramod,[status(thm)],[c_1376,c_5336]) ).
cnf(c_5337,plain,
op2(h11(e13),op2(e21,e23)) = h11(e10),
inference(paramod,[status(thm)],[c_1376,c_1374]) ).
cnf(c_5338,plain,
op2(e22,op2(e21,e23)) = h11(e10),
inference(paramod,[status(thm)],[c_4906,c_5337]) ).
cnf(c_5339,plain,
op2(e22,h11(e13)) = h11(e10),
inference(paramod,[status(thm)],[c_1376,c_5338]) ).
cnf(c_5340,plain,
op2(e22,e22) = h11(e10),
inference(paramod,[status(thm)],[c_4906,c_5339]) ).
cnf(c_4910,plain,
h6(e10) = h11(e10),
inference(paramod,[status(thm)],[c_4883,c_5340]) ).
cnf(c_5341,plain,
op2(h12(e13),op2(e22,e23)) = h12(e10),
inference(paramod,[status(thm)],[c_1382,c_1380]) ).
cnf(c_5342,plain,
op2(e21,op2(e22,e23)) = h12(e10),
inference(paramod,[status(thm)],[c_4884,c_5341]) ).
cnf(c_5343,plain,
op2(e21,h12(e13)) = h12(e10),
inference(paramod,[status(thm)],[c_1382,c_5342]) ).
cnf(c_5344,plain,
op2(e21,e21) = h12(e10),
inference(paramod,[status(thm)],[c_4884,c_5343]) ).
cnf(c_4912,plain,
h9(e10) = h12(e10),
inference(paramod,[status(thm)],[c_4904,c_5344]) ).
cnf(c_5345,plain,
op2(h12(e13),e22) = e23,
inference(paramod,[status(thm)],[c_1382,c_814]) ).
cnf(c_5346,plain,
op2(e21,e22) = e23,
inference(paramod,[status(thm)],[c_4884,c_5345]) ).
cnf(c_4914,plain,
h8(e13) = e23,
inference(paramod,[status(thm)],[c_1358,c_5346]) ).
cnf(c_5347,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != op2(e22,e22)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4914,c_3326]) ).
cnf(c_5348,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h6(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4883,c_5347]) ).
cnf(c_5349,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,h8(e13))
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4910,c_5348]) ).
cnf(c_5350,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != op2(e22,e23)
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4914,c_5349]) ).
cnf(c_5351,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != h12(e13)
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1382,c_5350]) ).
cnf(c_5352,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != op2(e21,e21)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4884,c_5351]) ).
cnf(c_5353,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != h9(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4904,c_5352]) ).
cnf(c_5354,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,h8(e13))
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4912,c_5353]) ).
cnf(c_5355,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != op2(e21,e23)
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4914,c_5354]) ).
cnf(c_5356,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != h11(e13)
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1376,c_5355]) ).
cnf(c_5357,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(h8(e13),h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4906,c_5356]) ).
cnf(c_5358,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(h8(e13),e22)
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4914,c_5357]) ).
cnf(c_5359,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != op2(e23,e22)
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4914,c_5358]) ).
cnf(c_5360,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != h9(e13)
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1364,c_5359]) ).
cnf(c_5361,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(op1(e13,e12)) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != e21
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4782,c_5360]) ).
cnf(c_5362,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| h8(e11) != op2(h8(e13),e21)
| h8(op1(e13,e11)) != e21
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4704,c_5361]) ).
cnf(c_5363,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| e22 != op2(h8(e13),e21)
| h8(op1(e13,e11)) != e21
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1353,c_5362]) ).
cnf(c_5364,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| e22 != op2(e23,e21)
| h8(op1(e13,e11)) != e21
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4914,c_5363]) ).
cnf(c_5365,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| e22 != h6(e13)
| h8(op1(e13,e11)) != e21
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1346,c_5364]) ).
cnf(c_5366,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(h8(e13),h8(e13)) != h8(op1(e13,e13))
| e22 != e22
| h8(op1(e13,e11)) != e21
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4862,c_5365]) ).
cnf(c_5367,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(e23,h8(e13)) != h8(op1(e13,e13))
| e22 != e22
| h8(op1(e13,e11)) != e21
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4914,c_5366]) ).
cnf(c_5368,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| op2(e23,e23) != h8(op1(e13,e13))
| e22 != e22
| h8(op1(e13,e11)) != e21
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4914,c_5367]) ).
cnf(c_5369,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| h5(e10) != h8(op1(e13,e13))
| e22 != e22
| h8(op1(e13,e11)) != e21
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1338,c_5368]) ).
cnf(c_5370,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| e20 != h8(op1(e13,e13))
| e22 != e22
| h8(op1(e13,e11)) != e21
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4717,c_5369]) ).
cnf(c_5371,negated_conjecture,
( h8(e13) != e23
| h8(e10) != e20
| e20 != h8(e10)
| e22 != e22
| h8(op1(e13,e11)) != e21
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4639,c_5370]) ).
cnf(c_5372,negated_conjecture,
( e23 != e23
| h8(e10) != e20
| e20 != h8(e10)
| e22 != e22
| h8(op1(e13,e11)) != e21
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| op2(h8(e10),e23) != h8(op1(e10,e13))
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4914,c_5371]) ).
cnf(c_5373,negated_conjecture,
( e23 != e23
| h8(e10) != e20
| e20 != h8(e10)
| e22 != e22
| h8(op1(e13,e11)) != e21
| op2(e23,h8(e10)) != h8(op1(e13,e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),e23)
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_5372]) ).
cnf(c_5374,negated_conjecture,
( e23 != e23
| h8(e10) != e20
| e20 != h8(e10)
| e22 != e22
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),e23)
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_5373]) ).
cnf(c_5375,negated_conjecture,
( e23 != e23
| h8(e10) != e20
| h8(e10) != e20
| e22 != e22
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),e23)
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_5374]) ).
cnf(c_5376,negated_conjecture,
( e23 != e23
| h8(e10) != e20
| h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),e23)
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_5375]) ).
cnf(c_5377,negated_conjecture,
( h8(e10) != e20
| h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),e23)
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_5376]) ).
cnf(c_4919,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),e23)
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(h8(e10),h8(e10)) != h8(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_5377]) ).
cnf(c_4943,plain,
op1(e10,e13) = e13,
inference(paramod,[status(thm)],[c_4639,c_314]) ).
cnf(c_5378,plain,
e10 != op1(e12,e13),
inference(paramod,[status(thm)],[c_4639,c_154]) ).
cnf(c_4946,plain,
op1(e12,e13) != e10,
inference(copy,[status(thm)],[c_5378]) ).
cnf(c_5379,plain,
( op1(e13,e13) = e13
| e11 = e13
| op1(e13,e11) = e13
| op1(e13,e10) = e13 ),
inference(paramod,[status(thm)],[c_4704,c_73]) ).
cnf(c_5380,plain,
( e10 = e13
| e11 = e13
| op1(e13,e11) = e13
| op1(e13,e10) = e13 ),
inference(paramod,[status(thm)],[c_4639,c_5379]) ).
cnf(c_5381,plain,
( e10 = e13
| e13 = e11
| op1(e13,e11) = e13
| op1(e13,e10) = e13 ),
inference(copy,[status(thm)],[c_5380]) ).
cnf(c_5382,plain,
( e13 = e10
| e13 = e11
| op1(e13,e11) = e13
| op1(e13,e10) = e13 ),
inference(copy,[status(thm)],[c_5381]) ).
cnf(c_5383,plain,
( e13 = e10
| e13 = e11
| op1(e13,e10) = e13 ),
inference(resolve,[status(thm)],[c_4708,c_5382]) ).
cnf(c_5384,plain,
( e13 = e10
| op1(e13,e10) = e13 ),
inference(resolve,[status(thm)],[c_257,c_5383]) ).
cnf(c_4948,plain,
op1(e13,e10) = e13,
inference(resolve,[status(thm)],[c_255,c_5384]) ).
cnf(c_5385,plain,
( op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| e13 = e12 ),
inference(paramod,[status(thm)],[c_4948,c_71]) ).
cnf(c_5386,plain,
( op1(e13,e13) = e12
| e11 = e12
| op1(e13,e11) = e12
| e13 = e12 ),
inference(paramod,[status(thm)],[c_4704,c_5385]) ).
cnf(c_5387,plain,
( e10 = e12
| e11 = e12
| op1(e13,e11) = e12
| e13 = e12 ),
inference(paramod,[status(thm)],[c_4639,c_5386]) ).
cnf(c_5388,plain,
( e10 = e12
| e12 = e11
| op1(e13,e11) = e12
| e13 = e12 ),
inference(copy,[status(thm)],[c_5387]) ).
cnf(c_5389,plain,
( e10 = e12
| e12 = e11
| op1(e13,e11) = e12 ),
inference(resolve,[status(thm)],[c_258,c_5388]) ).
cnf(c_5390,plain,
( e10 = e12
| op1(e13,e11) = e12 ),
inference(resolve,[status(thm)],[c_256,c_5389]) ).
cnf(c_4950,plain,
op1(e13,e11) = e12,
inference(resolve,[status(thm)],[c_254,c_5390]) ).
cnf(c_5391,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| op1(e12,e11) = op1(e13,e12)
| op1(e11,e13) = e13
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(paramod,[status(thm)],[c_4704,c_4691]) ).
cnf(c_5392,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| e13 = op1(e13,e12)
| op1(e11,e13) = e13
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(paramod,[status(thm)],[c_1308,c_5391]) ).
cnf(c_5393,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| e13 = e11
| op1(e11,e13) = e13
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(paramod,[status(thm)],[c_4704,c_5392]) ).
cnf(c_5394,plain,
( op1(e13,e13) = op1(e10,e13)
| e13 = e11
| op1(e11,e13) = e13
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(paramod,[status(thm)],[c_4943,c_5393]) ).
cnf(c_5395,plain,
( e10 = op1(e10,e13)
| e13 = e11
| op1(e11,e13) = e13
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(paramod,[status(thm)],[c_4639,c_5394]) ).
cnf(c_5396,plain,
( e10 = e13
| e13 = e11
| op1(e11,e13) = e13
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(paramod,[status(thm)],[c_4943,c_5395]) ).
cnf(c_5397,plain,
( e13 = e10
| e13 = e11
| op1(e11,e13) = e13
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(copy,[status(thm)],[c_5396]) ).
cnf(c_5398,plain,
( e13 = e10
| op1(e11,e13) = e13
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(resolve,[status(thm)],[c_257,c_5397]) ).
cnf(c_4952,plain,
( op1(e11,e13) = e13
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(resolve,[status(thm)],[c_255,c_5398]) ).
cnf(c_5399,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| op1(e12,e11) = op1(e13,e12)
| op1(e11,e13) = e13
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(paramod,[status(thm)],[c_4704,c_4659]) ).
cnf(c_5400,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| e13 = op1(e13,e12)
| op1(e11,e13) = e13
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(paramod,[status(thm)],[c_1308,c_5399]) ).
cnf(c_5401,plain,
( op1(e13,op1(e10,e13)) = op1(e10,e13)
| e13 = e11
| op1(e11,e13) = e13
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(paramod,[status(thm)],[c_4704,c_5400]) ).
cnf(c_5402,plain,
( op1(e13,e13) = op1(e10,e13)
| e13 = e11
| op1(e11,e13) = e13
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(paramod,[status(thm)],[c_4943,c_5401]) ).
cnf(c_5403,plain,
( e10 = op1(e10,e13)
| e13 = e11
| op1(e11,e13) = e13
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(paramod,[status(thm)],[c_4639,c_5402]) ).
cnf(c_5404,plain,
( e10 = e13
| e13 = e11
| op1(e11,e13) = e13
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(paramod,[status(thm)],[c_4943,c_5403]) ).
cnf(c_5405,plain,
( e13 = e10
| e13 = e11
| op1(e11,e13) = e13
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(copy,[status(thm)],[c_5404]) ).
cnf(c_5406,plain,
( e13 = e10
| op1(e11,e13) = e13
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(resolve,[status(thm)],[c_257,c_5405]) ).
cnf(c_4954,plain,
( op1(e11,e13) = e13
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(resolve,[status(thm)],[c_255,c_5406]) ).
cnf(c_4982,plain,
op1(e11,e13) = e12,
inference(paramod,[status(thm)],[c_4704,c_313]) ).
cnf(c_5407,plain,
e11 != op1(e10,e12),
inference(paramod,[status(thm)],[c_4704,c_143]) ).
cnf(c_4985,plain,
op1(e10,e12) != e11,
inference(copy,[status(thm)],[c_5407]) ).
cnf(c_5408,plain,
( e11 = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| op1(e10,e12) = e13 ),
inference(paramod,[status(thm)],[c_4704,c_66]) ).
cnf(c_5409,plain,
( e13 = e11
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| op1(e10,e12) = e13 ),
inference(copy,[status(thm)],[c_5408]) ).
cnf(c_5410,plain,
( e13 = e11
| op1(e11,e12) = e13
| op1(e10,e12) = e13 ),
inference(resolve,[status(thm)],[c_4706,c_5409]) ).
cnf(c_4986,plain,
( op1(e11,e12) = e13
| op1(e10,e12) = e13 ),
inference(resolve,[status(thm)],[c_257,c_5410]) ).
cnf(c_5411,plain,
( e11 = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_4704,c_64]) ).
cnf(c_5412,plain,
( e12 = e11
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(copy,[status(thm)],[c_5411]) ).
cnf(c_4987,plain,
( op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(resolve,[status(thm)],[c_256,c_5412]) ).
cnf(c_4995,plain,
op2(e23,e23) = e20,
inference(paramod,[status(thm)],[c_4717,c_1338]) ).
cnf(c_5413,plain,
( op2(e23,h10(e13)) = h10(e13)
| op2(e22,h9(e13)) = h9(e13)
| e22 = e23
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_4906,c_4769]) ).
cnf(c_5414,plain,
( op2(e23,h10(e13)) = h10(e13)
| op2(e22,e21) = h9(e13)
| e22 = e23
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_4782,c_5413]) ).
cnf(c_5415,plain,
( op2(e23,h10(e13)) = h10(e13)
| e23 = h9(e13)
| e22 = e23
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1310,c_5414]) ).
cnf(c_5416,plain,
( op2(e23,h10(e13)) = h10(e13)
| e23 = e21
| e22 = e23
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_4782,c_5415]) ).
cnf(c_5417,plain,
( op2(e23,e23) = h10(e13)
| e23 = e21
| e22 = e23
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_4878,c_5416]) ).
cnf(c_5418,plain,
( e20 = h10(e13)
| e23 = e21
| e22 = e23
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_4995,c_5417]) ).
cnf(c_5419,plain,
( e20 = e23
| e23 = e21
| e22 = e23
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(paramod,[status(thm)],[c_4878,c_5418]) ).
cnf(c_5420,plain,
( e20 = e23
| e23 = e21
| e23 = e22
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(copy,[status(thm)],[c_5419]) ).
cnf(c_5421,plain,
( e23 = e20
| e23 = e21
| e23 = e22
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(copy,[status(thm)],[c_5420]) ).
cnf(c_5422,plain,
( e23 = e20
| e23 = e21
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(resolve,[status(thm)],[c_266,c_5421]) ).
cnf(c_5423,plain,
( e23 = e20
| op2(e20,op2(e20,e20)) = op2(e20,e20) ),
inference(resolve,[status(thm)],[c_265,c_5422]) ).
cnf(c_4996,plain,
op2(e20,op2(e20,e20)) = op2(e20,e20),
inference(resolve,[status(thm)],[c_263,c_5423]) ).
cnf(c_5007,plain,
op2(e23,e20) = e23,
inference(paramod,[status(thm)],[c_4861,c_1328]) ).
cnf(c_5424,plain,
( h6(e13) = e20
| h9(e10) = e20
| h4(e13) = e20 ),
inference(paramod,[status(thm)],[c_4904,c_4794]) ).
cnf(c_5425,plain,
( h6(e13) = e20
| h12(e10) = e20
| h4(e13) = e20 ),
inference(paramod,[status(thm)],[c_4912,c_5424]) ).
cnf(c_5426,plain,
( e22 = e20
| h12(e10) = e20
| h4(e13) = e20 ),
inference(paramod,[status(thm)],[c_4862,c_5425]) ).
cnf(c_5427,plain,
( e20 = e22
| h12(e10) = e20
| h4(e13) = e20 ),
inference(copy,[status(thm)],[c_5426]) ).
cnf(c_5008,plain,
( h12(e10) = e20
| h4(e13) = e20 ),
inference(resolve,[status(thm)],[c_262,c_5427]) ).
cnf(c_5428,plain,
( e23 = e20
| h7(e13) = e20
| h4(e13) = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_4878,c_4874]) ).
cnf(c_5011,plain,
( h7(e13) = e20
| h4(e13) = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_263,c_5428]) ).
cnf(c_5429,plain,
( e23 = e21
| h7(e13) = e21
| h4(e13) = e21
| op2(e20,e20) = e21 ),
inference(paramod,[status(thm)],[c_4878,c_4873]) ).
cnf(c_5430,plain,
( e23 = e21
| h4(e13) = e21
| op2(e20,e20) = e21 ),
inference(resolve,[status(thm)],[c_4890,c_5429]) ).
cnf(c_5012,plain,
( h4(e13) = e21
| op2(e20,e20) = e21 ),
inference(resolve,[status(thm)],[c_265,c_5430]) ).
cnf(c_5431,plain,
( e23 = e22
| h7(e13) = e22
| op2(e20,e20) = e22 ),
inference(paramod,[status(thm)],[c_4878,c_4872]) ).
cnf(c_5013,plain,
( h7(e13) = e22
| op2(e20,e20) = e22 ),
inference(resolve,[status(thm)],[c_266,c_5431]) ).
cnf(c_5014,plain,
op2(e20,e23) = e23,
inference(paramod,[status(thm)],[c_4878,c_1370]) ).
cnf(c_5432,plain,
( h6(e10) = e20
| e23 = e20
| h7(e13) = e20 ),
inference(paramod,[status(thm)],[c_4914,c_4895]) ).
cnf(c_5433,plain,
( h11(e10) = e20
| e23 = e20
| h7(e13) = e20 ),
inference(paramod,[status(thm)],[c_4910,c_5432]) ).
cnf(c_5032,plain,
( h11(e10) = e20
| h7(e13) = e20 ),
inference(resolve,[status(thm)],[c_263,c_5433]) ).
cnf(c_5434,plain,
op2(e23,h8(e13)) = h8(e10),
inference(paramod,[status(thm)],[c_4914,c_4897]) ).
cnf(c_5435,plain,
op2(e23,e23) = h8(e10),
inference(paramod,[status(thm)],[c_4914,c_5434]) ).
cnf(c_5436,plain,
e20 = h8(e10),
inference(paramod,[status(thm)],[c_4995,c_5435]) ).
cnf(c_5037,plain,
h8(e10) = e20,
inference(copy,[status(thm)],[c_5436]) ).
cnf(c_5437,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),e23)
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(e20,h8(e10)) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_5037,c_4919]) ).
cnf(c_5438,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),e23)
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(h8(e10),e22)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_5037,c_5437]) ).
cnf(c_5439,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),e23)
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != op2(e20,e22)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_5037,c_5438]) ).
cnf(c_5440,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),e23)
| h8(op1(e10,e12)) != op2(h8(e10),e21)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1352,c_5439]) ).
cnf(c_5441,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),e23)
| h8(op1(e10,e12)) != op2(e20,e21)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_5037,c_5440]) ).
cnf(c_5442,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),e23)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1334,c_5441]) ).
cnf(c_5443,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| h8(e13) != op2(h8(e10),e23)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4943,c_5442]) ).
cnf(c_5444,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| e23 != op2(h8(e10),e23)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4914,c_5443]) ).
cnf(c_5445,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| e23 != op2(e20,e23)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_5037,c_5444]) ).
cnf(c_5446,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,h8(e10))
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_5014,c_5445]) ).
cnf(c_5447,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != op2(e22,e20)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_5037,c_5446]) ).
cnf(c_5448,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(op1(e11,e13)) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1322,c_5447]) ).
cnf(c_5449,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| h8(e12) != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4982,c_5448]) ).
cnf(c_5450,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,h8(e10))
| e21 != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1354,c_5449]) ).
cnf(c_5451,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != op2(e21,e20)
| e21 != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_5037,c_5450]) ).
cnf(c_5452,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(op1(e13,e10)) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| e21 != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1316,c_5451]) ).
cnf(c_5453,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| h8(e13) != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| e21 != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4948,c_5452]) ).
cnf(c_5454,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| e23 != op2(e23,h8(e10))
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| e21 != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4914,c_5453]) ).
cnf(c_5455,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| e23 != op2(e23,e20)
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| e21 != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_5037,c_5454]) ).
cnf(c_5456,negated_conjecture,
( h8(e10) != e20
| h8(op1(e13,e11)) != e21
| e23 != e23
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| e21 != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_5007,c_5455]) ).
cnf(c_5457,negated_conjecture,
( h8(e10) != e20
| h8(e12) != e21
| e23 != e23
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| e21 != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_4950,c_5456]) ).
cnf(c_5458,negated_conjecture,
( h8(e10) != e20
| e21 != e21
| e23 != e23
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| e21 != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1354,c_5457]) ).
cnf(c_5459,negated_conjecture,
( e20 != e20
| e21 != e21
| e23 != e23
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| e21 != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| op2(e20,e20) != h8(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_5037,c_5458]) ).
cnf(c_5460,negated_conjecture,
( e20 != e20
| e21 != e21
| e23 != e23
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| e21 != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| e23 != e23
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_5459]) ).
cnf(c_5461,negated_conjecture,
( e20 != e20
| e21 != e21
| e23 != e23
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| e21 != e21
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_5460]) ).
cnf(c_5462,negated_conjecture,
( e20 != e20
| e21 != e21
| e23 != e23
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_5461]) ).
cnf(c_5463,negated_conjecture,
( e20 != e20
| e21 != e21
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_5462]) ).
cnf(c_5464,negated_conjecture,
( e20 != e20
| h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_5463]) ).
cnf(c_5045,negated_conjecture,
( h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| h8(op1(e11,e12)) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_5464]) ).
cnf(c_5465,plain,
e13 != op1(e10,e12),
inference(paramod,[status(thm)],[c_4943,c_162]) ).
cnf(c_5058,plain,
op1(e10,e12) != e13,
inference(copy,[status(thm)],[c_5465]) ).
cnf(c_5466,plain,
( e13 = e11
| op1(e10,e12) = e11
| op1(e10,e11) = e11
| op1(e10,e10) = e11 ),
inference(paramod,[status(thm)],[c_4943,c_45]) ).
cnf(c_5467,plain,
( e13 = e11
| op1(e10,e11) = e11
| op1(e10,e10) = e11 ),
inference(resolve,[status(thm)],[c_4985,c_5466]) ).
cnf(c_5061,plain,
( op1(e10,e11) = e11
| op1(e10,e10) = e11 ),
inference(resolve,[status(thm)],[c_257,c_5467]) ).
cnf(c_5468,plain,
( e13 = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_4943,c_43]) ).
cnf(c_5062,plain,
( op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_255,c_5468]) ).
cnf(c_5469,plain,
( e12 = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 ),
inference(paramod,[status(thm)],[c_4950,c_4716]) ).
cnf(c_5470,plain,
( e10 = e12
| op1(e11,e11) = e10
| op1(e10,e11) = e10 ),
inference(copy,[status(thm)],[c_5469]) ).
cnf(c_5063,plain,
( op1(e11,e11) = e10
| op1(e10,e11) = e10 ),
inference(resolve,[status(thm)],[c_254,c_5470]) ).
cnf(c_5065,plain,
( op1(e12,e12) = e10
| op1(e12,e10) = e10 ),
inference(resolve,[status(thm)],[c_4946,c_4713]) ).
cnf(c_5071,plain,
op1(e12,e13) = e11,
inference(paramod,[status(thm)],[c_4950,c_312]) ).
cnf(c_5471,plain,
( e12 = e13
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(paramod,[status(thm)],[c_4982,c_4954]) ).
cnf(c_5472,plain,
( e13 = e12
| op1(e10,op1(e12,e10)) = op1(e12,e10) ),
inference(copy,[status(thm)],[c_5471]) ).
cnf(c_5074,plain,
op1(e10,op1(e12,e10)) = op1(e12,e10),
inference(resolve,[status(thm)],[c_258,c_5472]) ).
cnf(c_5473,plain,
( e12 = e13
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(paramod,[status(thm)],[c_4982,c_4952]) ).
cnf(c_5474,plain,
( e13 = e12
| op1(e10,op1(e10,e10)) = op1(e10,e10) ),
inference(copy,[status(thm)],[c_5473]) ).
cnf(c_5076,plain,
op1(e10,op1(e10,e10)) = op1(e10,e10),
inference(resolve,[status(thm)],[c_258,c_5474]) ).
cnf(c_5088,plain,
op1(e11,e12) = e13,
inference(resolve,[status(thm)],[c_5058,c_4986]) ).
cnf(c_5475,negated_conjecture,
( h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| h8(e13) != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_5088,c_5045]) ).
cnf(c_5476,negated_conjecture,
( h8(op1(e12,e13)) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| e23 != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_4914,c_5475]) ).
cnf(c_5477,negated_conjecture,
( h8(e11) != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| e23 != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_5071,c_5476]) ).
cnf(c_5478,negated_conjecture,
( e22 != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| e23 != e23
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1353,c_5477]) ).
cnf(c_5479,negated_conjecture,
( e22 != e22
| h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_5478]) ).
cnf(c_5094,negated_conjecture,
( h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != h4(e13)
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_5479]) ).
cnf(c_5480,plain,
( e11 = e12
| op1(e12,e12) = e12
| op1(e12,e10) = e12 ),
inference(paramod,[status(thm)],[c_5071,c_4711]) ).
cnf(c_5481,plain,
( e12 = e11
| op1(e12,e12) = e12
| op1(e12,e10) = e12 ),
inference(copy,[status(thm)],[c_5480]) ).
cnf(c_5101,plain,
( op1(e12,e12) = e12
| op1(e12,e10) = e12 ),
inference(resolve,[status(thm)],[c_256,c_5481]) ).
cnf(c_5482,plain,
( op1(e12,e12) = e12
| e13 = e12
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_5088,c_4987]) ).
cnf(c_5106,plain,
( op1(e12,e12) = e12
| op1(e10,e12) = e12 ),
inference(resolve,[status(thm)],[c_258,c_5482]) ).
cnf(c_5483,plain,
( op2(e20,e21) = op2(e20,e20)
| h4(e13) = e21 ),
inference(paramod,[status(thm)],[c_5012,c_4996]) ).
cnf(c_5484,plain,
( h4(e13) = op2(e20,e20)
| h4(e13) = e21 ),
inference(paramod,[status(thm)],[c_1334,c_5483]) ).
cnf(c_5485,plain,
( op2(e20,e20) = h4(e13)
| h4(e13) = e21 ),
inference(copy,[status(thm)],[c_5484]) ).
cnf(c_5136,plain,
h4(e13) = e21,
inference(resolve,[status(thm)],[c_4868,c_5485]) ).
cnf(c_5141,negated_conjecture,
( h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != h1(e13)
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != e21
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_5136,c_5094]) ).
cnf(c_5486,plain,
( h7(e13) = e20
| e21 = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_5136,c_5011]) ).
cnf(c_5487,plain,
( h7(e13) = e20
| e20 = e21
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_5486]) ).
cnf(c_5143,plain,
( h7(e13) = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_260,c_5487]) ).
cnf(c_5488,plain,
( h12(e10) = e20
| e21 = e20 ),
inference(paramod,[status(thm)],[c_5136,c_5008]) ).
cnf(c_5489,plain,
( h12(e10) = e20
| e20 = e21 ),
inference(copy,[status(thm)],[c_5488]) ).
cnf(c_5144,plain,
h12(e10) = e20,
inference(resolve,[status(thm)],[c_260,c_5489]) ).
cnf(c_5490,plain,
op2(e21,e20) = e21,
inference(paramod,[status(thm)],[c_5136,c_4865]) ).
cnf(c_5146,plain,
h1(e13) = e21,
inference(paramod,[status(thm)],[c_1316,c_5490]) ).
cnf(c_5491,negated_conjecture,
( h8(op1(e12,e12)) != h12(e10)
| h8(op1(e12,e10)) != e21
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != e21
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_5146,c_5141]) ).
cnf(c_5149,negated_conjecture,
( h8(op1(e12,e12)) != e20
| h8(op1(e12,e10)) != e21
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != e21
| h8(op1(e10,e11)) != h7(e13)
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_5144,c_5491]) ).
cnf(c_5492,plain,
( op2(e20,e22) = op2(e20,e20)
| h7(e13) = e22 ),
inference(paramod,[status(thm)],[c_5013,c_4996]) ).
cnf(c_5493,plain,
( h7(e13) = op2(e20,e20)
| h7(e13) = e22 ),
inference(paramod,[status(thm)],[c_1352,c_5492]) ).
cnf(c_5494,plain,
( op2(e20,e20) = h7(e13)
| h7(e13) = e22 ),
inference(copy,[status(thm)],[c_5493]) ).
cnf(c_5164,plain,
h7(e13) = e22,
inference(resolve,[status(thm)],[c_4889,c_5494]) ).
cnf(c_5168,negated_conjecture,
( h8(op1(e12,e12)) != e20
| h8(op1(e12,e10)) != e21
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != e21
| h8(op1(e10,e11)) != e22
| h8(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_5164,c_5149]) ).
cnf(c_5495,plain,
( e22 = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_5164,c_5143]) ).
cnf(c_5496,plain,
( e20 = e22
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_5495]) ).
cnf(c_5169,plain,
op2(e20,e20) = e20,
inference(resolve,[status(thm)],[c_262,c_5496]) ).
cnf(c_5497,plain,
( h11(e10) = e20
| e22 = e20 ),
inference(paramod,[status(thm)],[c_5164,c_5032]) ).
cnf(c_5498,plain,
( h11(e10) = e20
| e20 = e22 ),
inference(copy,[status(thm)],[c_5497]) ).
cnf(c_5172,plain,
h11(e10) = e20,
inference(resolve,[status(thm)],[c_262,c_5498]) ).
cnf(c_5499,plain,
op2(e22,e20) = e22,
inference(paramod,[status(thm)],[c_5164,c_4887]) ).
cnf(c_5173,plain,
h2(e13) = e22,
inference(paramod,[status(thm)],[c_1322,c_5499]) ).
cnf(c_5500,negated_conjecture,
( h8(op1(e12,e12)) != e20
| h8(op1(e12,e10)) != e21
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != h2(e13)
| h8(op1(e10,e12)) != e21
| h8(op1(e10,e11)) != e22
| h8(op1(e10,e10)) != e20 ),
inference(paramod,[status(thm)],[c_5169,c_5168]) ).
cnf(c_5501,negated_conjecture,
( h8(op1(e12,e12)) != e20
| h8(op1(e12,e10)) != e21
| h8(op1(e11,e11)) != h11(e10)
| h8(op1(e11,e10)) != e22
| h8(op1(e10,e12)) != e21
| h8(op1(e10,e11)) != e22
| h8(op1(e10,e10)) != e20 ),
inference(paramod,[status(thm)],[c_5173,c_5500]) ).
cnf(c_5176,negated_conjecture,
( h8(op1(e12,e12)) != e20
| h8(op1(e12,e10)) != e21
| h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| h8(op1(e10,e12)) != e21
| h8(op1(e10,e11)) != e22
| h8(op1(e10,e10)) != e20 ),
inference(paramod,[status(thm)],[c_5172,c_5501]) ).
cnf(c_5502,plain,
( op1(e10,e10) = op1(e12,e10)
| op1(e12,e12) = e10 ),
inference(paramod,[status(thm)],[c_5065,c_5074]) ).
cnf(c_5198,plain,
op1(e12,e12) = e10,
inference(resolve,[status(thm)],[c_126,c_5502]) ).
cnf(c_5503,negated_conjecture,
( h8(e10) != e20
| h8(op1(e12,e10)) != e21
| h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| h8(op1(e10,e12)) != e21
| h8(op1(e10,e11)) != e22
| h8(op1(e10,e10)) != e20 ),
inference(paramod,[status(thm)],[c_5198,c_5176]) ).
cnf(c_5504,negated_conjecture,
( e20 != e20
| h8(op1(e12,e10)) != e21
| h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| h8(op1(e10,e12)) != e21
| h8(op1(e10,e11)) != e22
| h8(op1(e10,e10)) != e20 ),
inference(paramod,[status(thm)],[c_5037,c_5503]) ).
cnf(c_5204,negated_conjecture,
( h8(op1(e12,e10)) != e21
| h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| h8(op1(e10,e12)) != e21
| h8(op1(e10,e11)) != e22
| h8(op1(e10,e10)) != e20 ),
inference(copy,[status(thm)],[c_5504]) ).
cnf(c_5505,plain,
( e10 = e12
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_5198,c_5106]) ).
cnf(c_5207,plain,
op1(e10,e12) = e12,
inference(resolve,[status(thm)],[c_254,c_5505]) ).
cnf(c_5506,plain,
( e10 = e12
| op1(e12,e10) = e12 ),
inference(paramod,[status(thm)],[c_5198,c_5101]) ).
cnf(c_5208,plain,
op1(e12,e10) = e12,
inference(resolve,[status(thm)],[c_254,c_5506]) ).
cnf(c_5507,plain,
( e12 = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_5207,c_5062]) ).
cnf(c_5508,plain,
( e10 = e12
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_5507]) ).
cnf(c_5212,plain,
( op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_254,c_5508]) ).
cnf(c_5509,negated_conjecture,
( h8(op1(e12,e10)) != e21
| h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| h8(e12) != e21
| h8(op1(e10,e11)) != e22
| h8(op1(e10,e10)) != e20 ),
inference(paramod,[status(thm)],[c_5207,c_5204]) ).
cnf(c_5510,negated_conjecture,
( h8(op1(e12,e10)) != e21
| h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| e21 != e21
| h8(op1(e10,e11)) != e22
| h8(op1(e10,e10)) != e20 ),
inference(paramod,[status(thm)],[c_1354,c_5509]) ).
cnf(c_5511,negated_conjecture,
( h8(e12) != e21
| h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| e21 != e21
| h8(op1(e10,e11)) != e22
| h8(op1(e10,e10)) != e20 ),
inference(paramod,[status(thm)],[c_5208,c_5510]) ).
cnf(c_5512,negated_conjecture,
( e21 != e21
| h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| e21 != e21
| h8(op1(e10,e11)) != e22
| h8(op1(e10,e10)) != e20 ),
inference(paramod,[status(thm)],[c_1354,c_5511]) ).
cnf(c_5513,negated_conjecture,
( e21 != e21
| h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| h8(op1(e10,e11)) != e22
| h8(op1(e10,e10)) != e20 ),
inference(copy,[status(thm)],[c_5512]) ).
cnf(c_5213,negated_conjecture,
( h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| h8(op1(e10,e11)) != e22
| h8(op1(e10,e10)) != e20 ),
inference(copy,[status(thm)],[c_5513]) ).
cnf(c_5514,plain,
( op1(e10,e11) = op1(e10,e10)
| op1(e10,e11) = e11 ),
inference(paramod,[status(thm)],[c_5061,c_5076]) ).
cnf(c_5515,plain,
( op1(e10,e10) = op1(e10,e11)
| op1(e10,e11) = e11 ),
inference(copy,[status(thm)],[c_5514]) ).
cnf(c_5221,plain,
op1(e10,e11) = e11,
inference(resolve,[status(thm)],[c_156,c_5515]) ).
cnf(c_5516,negated_conjecture,
( h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| h8(e11) != e22
| h8(op1(e10,e10)) != e20 ),
inference(paramod,[status(thm)],[c_5221,c_5213]) ).
cnf(c_5517,negated_conjecture,
( h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| e22 != e22
| h8(op1(e10,e10)) != e20 ),
inference(paramod,[status(thm)],[c_1353,c_5516]) ).
cnf(c_5227,negated_conjecture,
( h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| h8(op1(e10,e10)) != e20 ),
inference(copy,[status(thm)],[c_5517]) ).
cnf(c_5518,plain,
( e11 = e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_5221,c_5212]) ).
cnf(c_5519,plain,
( e10 = e11
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_5518]) ).
cnf(c_5228,plain,
op1(e10,e10) = e10,
inference(resolve,[status(thm)],[c_252,c_5519]) ).
cnf(c_5520,plain,
( op1(e11,e11) = e10
| e11 = e10 ),
inference(paramod,[status(thm)],[c_5221,c_5063]) ).
cnf(c_5521,plain,
( op1(e11,e11) = e10
| e10 = e11 ),
inference(copy,[status(thm)],[c_5520]) ).
cnf(c_5230,plain,
op1(e11,e11) = e10,
inference(resolve,[status(thm)],[c_252,c_5521]) ).
cnf(c_5231,plain,
op1(e11,e10) = e11,
inference(paramod,[status(thm)],[c_5221,c_300]) ).
cnf(c_5522,negated_conjecture,
( h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| h8(e10) != e20 ),
inference(paramod,[status(thm)],[c_5228,c_5227]) ).
cnf(c_5523,negated_conjecture,
( h8(op1(e11,e11)) != e20
| h8(op1(e11,e10)) != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_5037,c_5522]) ).
cnf(c_5524,negated_conjecture,
( h8(op1(e11,e11)) != e20
| h8(e11) != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_5231,c_5523]) ).
cnf(c_5525,negated_conjecture,
( h8(op1(e11,e11)) != e20
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_1353,c_5524]) ).
cnf(c_5526,negated_conjecture,
( h8(e10) != e20
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_5230,c_5525]) ).
cnf(c_5527,negated_conjecture,
( e20 != e20
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_5037,c_5526]) ).
cnf(c_5528,negated_conjecture,
( e20 != e20
| e22 != e22 ),
inference(copy,[status(thm)],[c_5527]) ).
cnf(c_5529,negated_conjecture,
e20 != e20,
inference(copy,[status(thm)],[c_5528]) ).
cnf(c_5232,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_5529]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG105+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.06/15.41 % CPULimit : 300
% 0.06/15.41 % WCLimit : 300
% 0.06/15.41 % DateTime : Sat Sep 26 21:09:14 UTC 2026
% 0.06/15.42 % CPUTime :
% 0.06/15.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.06/15.42 % Process 3574404 was started by sandbox2 on n013,
% 0.06/15.42 % Sat Sep 26 21:09:14 2026
% 0.06/15.42 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 54.19/69.33
% 54.19/69.33 % From the command line: assign(max_seconds, 300).
% 62.95/70.55
% 62.95/70.55 % SZS status Theorem for theBenchmark
% 62.95/70.55
% 62.95/70.55 % Proof 1 at 1.00 (+ 0.12) seconds.
% 62.95/70.55 % Length of proof is 224.
% 62.95/70.55 % Level of proof is 18.
% 62.95/70.55 % Maximum clause weight is 157.000.
% 62.95/70.55 % Given clauses 159.
% 62.95/70.55
% 62.95/70.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------