%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG107+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:31 AM UTC 2026
% Result : Theorem 67.80s 19.83s
% Output : CNFRefutation 67.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 121
% Number of leaves : 14
% Syntax : Number of formulae : 757 ( 180 unt; 0 def)
% Number of atoms : 4177 (4176 equ)
% Maximal formula atoms : 128 ( 5 avg)
% Number of connectives : 5483 (2063 ~;3041 |; 379 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
( ( op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e13,e13) = e10 )
& ( op1(e13,e12) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11
| op1(e13,e12) = e10 )
& ( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e13,e11) = e10 )
& ( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 )
& ( op1(e12,e13) = e13
| op1(e12,e13) = e12
| op1(e12,e13) = e11
| op1(e12,e13) = e10 )
& ( op1(e12,e12) = e13
| op1(e12,e12) = e12
| op1(e12,e12) = e11
| op1(e12,e12) = e10 )
& ( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 )
& ( op1(e12,e10) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 )
& ( op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11
| op1(e11,e13) = e10 )
& ( op1(e11,e12) = e13
| op1(e11,e12) = e12
| op1(e11,e12) = e11
| op1(e11,e12) = e10 )
& ( op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e11) = e10 )
& ( op1(e11,e10) = e13
| op1(e11,e10) = e12
| op1(e11,e10) = e11
| op1(e11,e10) = e10 )
& ( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 )
& ( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 )
& ( op1(e10,e11) = e13
| op1(e10,e11) = e12
| op1(e10,e11) = e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e11
| op1(e10,e10) = e10 ) ),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
( ( op1(e13,e13) = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| op1(e10,e13) = e13 )
& ( op1(e13,e13) = e13
| op1(e13,e12) = e13
| op1(e13,e11) = e13
| op1(e13,e10) = e13 )
& ( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 )
& ( op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 )
& ( op1(e13,e13) = e11
| op1(e12,e13) = e11
| op1(e11,e13) = e11
| op1(e10,e13) = e11 )
& ( op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 )
& ( op1(e13,e13) = e10
| op1(e12,e13) = e10
| op1(e11,e13) = e10
| op1(e10,e13) = e10 )
& ( op1(e13,e13) = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 )
& ( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| op1(e10,e12) = e13 )
& ( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 )
& ( op1(e13,e12) = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 )
& ( op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 )
& ( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 )
& ( op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 )
& ( op1(e13,e12) = e10
| op1(e12,e12) = e10
| op1(e11,e12) = e10
| op1(e10,e12) = e10 )
& ( op1(e12,e13) = e10
| op1(e12,e12) = e10
| op1(e12,e11) = e10
| op1(e12,e10) = e10 )
& ( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| op1(e10,e11) = e13 )
& ( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e11) = e13
| op1(e11,e10) = e13 )
& ( op1(e13,e11) = e12
| op1(e12,e11) = e12
| op1(e11,e11) = e12
| op1(e10,e11) = e12 )
& ( op1(e11,e13) = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 )
& ( op1(e13,e11) = e11
| op1(e12,e11) = e11
| op1(e11,e11) = e11
| op1(e10,e11) = e11 )
& ( op1(e11,e13) = e11
| op1(e11,e12) = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 )
& ( op1(e13,e11) = e10
| op1(e12,e11) = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 )
& ( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 )
& ( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| op1(e10,e10) = e13 )
& ( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 )
& ( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| op1(e10,e10) = e12 )
& ( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 )
& ( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11
| op1(e10,e10) = e11 )
& ( op1(e10,e13) = e11
| op1(e10,e12) = e11
| op1(e10,e11) = e11
| op1(e10,e10) = e11 )
& ( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 )
& ( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ) ),
file('theBenchmark.p',ax2) ).
fof(ax3,axiom,
( ( op2(e23,e23) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e23,e23) = e20 )
& ( op2(e23,e22) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21
| op2(e23,e22) = e20 )
& ( op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e23,e21) = e21
| op2(e23,e21) = e20 )
& ( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 )
& ( op2(e22,e23) = e23
| op2(e22,e23) = e22
| op2(e22,e23) = e21
| op2(e22,e23) = e20 )
& ( op2(e22,e22) = e23
| op2(e22,e22) = e22
| op2(e22,e22) = e21
| op2(e22,e22) = e20 )
& ( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 )
& ( op2(e22,e20) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 )
& ( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| op2(e21,e23) = e20 )
& ( op2(e21,e22) = e23
| op2(e21,e22) = e22
| op2(e21,e22) = e21
| op2(e21,e22) = e20 )
& ( op2(e21,e21) = e23
| op2(e21,e21) = e22
| op2(e21,e21) = e21
| op2(e21,e21) = e20 )
& ( op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e21
| op2(e21,e20) = e20 )
& ( op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 )
& ( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| op2(e20,e22) = e20 )
& ( op2(e20,e21) = e23
| op2(e20,e21) = e22
| op2(e20,e21) = e21
| op2(e20,e21) = e20 )
& ( op2(e20,e20) = e23
| op2(e20,e20) = e22
| op2(e20,e20) = e21
| op2(e20,e20) = e20 ) ),
file('theBenchmark.p',ax3) ).
fof(ax4,axiom,
( ( op2(e23,e23) = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| op2(e20,e23) = e23 )
& ( op2(e23,e23) = e23
| op2(e23,e22) = e23
| op2(e23,e21) = e23
| op2(e23,e20) = e23 )
& ( op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 )
& ( op2(e23,e23) = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 )
& ( op2(e23,e23) = e21
| op2(e22,e23) = e21
| op2(e21,e23) = e21
| op2(e20,e23) = e21 )
& ( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 )
& ( op2(e23,e23) = e20
| op2(e22,e23) = e20
| op2(e21,e23) = e20
| op2(e20,e23) = e20 )
& ( op2(e23,e23) = e20
| op2(e23,e22) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 )
& ( op2(e23,e22) = e23
| op2(e22,e22) = e23
| op2(e21,e22) = e23
| op2(e20,e22) = e23 )
& ( op2(e22,e23) = e23
| op2(e22,e22) = e23
| op2(e22,e21) = e23
| op2(e22,e20) = e23 )
& ( op2(e23,e22) = e22
| op2(e22,e22) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 )
& ( op2(e22,e23) = e22
| op2(e22,e22) = e22
| op2(e22,e21) = e22
| op2(e22,e20) = e22 )
& ( op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 )
& ( op2(e22,e23) = e21
| op2(e22,e22) = e21
| op2(e22,e21) = e21
| op2(e22,e20) = e21 )
& ( op2(e23,e22) = e20
| op2(e22,e22) = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 )
& ( op2(e22,e23) = e20
| op2(e22,e22) = e20
| op2(e22,e21) = e20
| op2(e22,e20) = e20 )
& ( op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e21,e21) = e23
| op2(e20,e21) = e23 )
& ( op2(e21,e23) = e23
| op2(e21,e22) = e23
| op2(e21,e21) = e23
| op2(e21,e20) = e23 )
& ( op2(e23,e21) = e22
| op2(e22,e21) = e22
| op2(e21,e21) = e22
| op2(e20,e21) = e22 )
& ( op2(e21,e23) = e22
| op2(e21,e22) = e22
| op2(e21,e21) = e22
| op2(e21,e20) = e22 )
& ( op2(e23,e21) = e21
| op2(e22,e21) = e21
| op2(e21,e21) = e21
| op2(e20,e21) = e21 )
& ( op2(e21,e23) = e21
| op2(e21,e22) = e21
| op2(e21,e21) = e21
| op2(e21,e20) = e21 )
& ( op2(e23,e21) = e20
| op2(e22,e21) = e20
| op2(e21,e21) = e20
| op2(e20,e21) = e20 )
& ( op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20
| op2(e21,e20) = e20 )
& ( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| op2(e20,e20) = e23 )
& ( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 )
& ( op2(e23,e20) = e22
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| op2(e20,e20) = e22 )
& ( op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| op2(e20,e20) = e22 )
& ( op2(e23,e20) = e21
| op2(e22,e20) = e21
| op2(e21,e20) = e21
| op2(e20,e20) = e21 )
& ( op2(e20,e23) = e21
| op2(e20,e22) = e21
| op2(e20,e21) = e21
| op2(e20,e20) = e21 )
& ( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| op2(e20,e20) = e20 )
& ( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ) ),
file('theBenchmark.p',ax4) ).
fof(ax5,axiom,
( op1(e13,e12) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e11)
& op1(e12,e12) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e11)
& op1(e11,e12) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e11)
& op1(e10,e12) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e11)
& op1(e12,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e11,e13)
& op1(e12,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e11,e12)
& op1(e12,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e11,e11)
& op1(e12,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e11,e10) ),
file('theBenchmark.p',ax5) ).
fof(ax6,axiom,
( op2(e23,e22) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e21)
& op2(e22,e22) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e21)
& op2(e21,e22) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e21)
& op2(e20,e22) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e21)
& op2(e22,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e21,e23)
& op2(e22,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e21,e22)
& op2(e22,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e21,e21)
& op2(e22,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e21,e20) ),
file('theBenchmark.p',ax6) ).
fof(ax7,axiom,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('theBenchmark.p',ax7) ).
fof(ax8,axiom,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('theBenchmark.p',ax8) ).
fof(ax10,axiom,
( ( op1(e13,op1(e13,e13)) = e13
& op1(e12,op1(e13,e12)) = e12
& op1(e11,op1(e13,e11)) = e11
& op1(e10,op1(e13,e10)) = e10 )
| ( op1(e13,op1(e12,e13)) = e13
& op1(e12,op1(e12,e12)) = e12
& op1(e11,op1(e12,e11)) = e11
& op1(e10,op1(e12,e10)) = e10 )
| ( op1(e13,op1(e11,e13)) = e13
& op1(e12,op1(e11,e12)) = e12
& op1(e11,op1(e11,e11)) = e11
& op1(e10,op1(e11,e10)) = e10 )
| ( op1(e13,op1(e10,e13)) = e13
& op1(e12,op1(e10,e12)) = e12
& op1(e11,op1(e10,e11)) = e11
& op1(e10,op1(e10,e10)) = e10 ) ),
file('theBenchmark.p',ax10) ).
fof(ax11,axiom,
( ( op2(e23,op2(e23,e23)) = e23
& op2(e22,op2(e23,e22)) = e22
& op2(e21,op2(e23,e21)) = e21
& op2(e20,op2(e23,e20)) = e20 )
| ( op2(e23,op2(e22,e23)) = e23
& op2(e22,op2(e22,e22)) = e22
& op2(e21,op2(e22,e21)) = e21
& op2(e20,op2(e22,e20)) = e20 )
| ( op2(e23,op2(e21,e23)) = e23
& op2(e22,op2(e21,e22)) = e22
& op2(e21,op2(e21,e21)) = e21
& op2(e20,op2(e21,e20)) = e20 )
| ( op2(e23,op2(e20,e23)) = e23
& op2(e22,op2(e20,e22)) = e22
& op2(e21,op2(e20,e21)) = e21
& op2(e20,op2(e20,e20)) = e20 ) ),
file('theBenchmark.p',ax11) ).
fof(ax12,axiom,
( e13 = op1(op1(e12,op1(e12,e12)),op1(e12,e12))
& e11 = op1(e12,op1(e12,e12))
& e10 = op1(e12,e12) ),
file('theBenchmark.p',ax12) ).
fof(ax13,axiom,
( e23 = op2(op2(e22,op2(e22,e22)),op2(e22,e22))
& e21 = op2(e22,op2(e22,e22))
& e20 = op2(e22,e22) ),
file('theBenchmark.p',ax13) ).
fof(ax16,axiom,
( h3(e13) = op2(op2(e22,op2(e22,e22)),op2(e22,e22))
& h3(e11) = op2(e22,op2(e22,e22))
& h3(e10) = op2(e22,e22)
& h3(e12) = e22 ),
file('theBenchmark.p',ax16) ).
fof(co1,conjecture,
( ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ( ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_19,plain,
( op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e11
| op1(e10,e10) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_21,plain,
( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_22,plain,
( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_25,plain,
( op1(e11,e12) = e13
| op1(e11,e12) = e12
| op1(e11,e12) = e11
| op1(e11,e12) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_28,plain,
( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_31,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_33,plain,
( op1(e13,e12) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11
| op1(e13,e12) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_35,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_36,plain,
( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_40,plain,
( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| op1(e10,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_41,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_43,plain,
( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_44,plain,
( op1(e13,e11) = e10
| op1(e12,e11) = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_47,plain,
( op1(e11,e13) = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_50,plain,
( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| op1(e10,e11) = e13 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_54,plain,
( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_55,plain,
( op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_57,plain,
( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_59,plain,
( op1(e13,e13) = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_61,plain,
( op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_64,plain,
( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_67,plain,
( op2(e20,e20) = e23
| op2(e20,e20) = e22
| op2(e20,e20) = e21
| op2(e20,e20) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_69,plain,
( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| op2(e20,e22) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_70,plain,
( op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_73,plain,
( op2(e21,e22) = e23
| op2(e21,e22) = e22
| op2(e21,e22) = e21
| op2(e21,e22) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_76,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_79,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_81,plain,
( op2(e23,e22) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21
| op2(e23,e22) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_82,plain,
( op2(e23,e23) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e23,e23) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_83,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_84,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| op2(e20,e20) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_88,plain,
( op2(e23,e20) = e22
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| op2(e20,e20) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_89,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_91,plain,
( op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20
| op2(e21,e20) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_92,plain,
( op2(e23,e21) = e20
| op2(e22,e21) = e20
| op2(e21,e21) = e20
| op2(e20,e21) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_95,plain,
( op2(e21,e23) = e22
| op2(e21,e22) = e22
| op2(e21,e21) = e22
| op2(e21,e20) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_98,plain,
( op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e21,e21) = e23
| op2(e20,e21) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_102,plain,
( op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_103,plain,
( op2(e22,e23) = e22
| op2(e22,e22) = e22
| op2(e22,e21) = e22
| op2(e22,e20) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_105,plain,
( op2(e22,e23) = e23
| op2(e22,e22) = e23
| op2(e22,e21) = e23
| op2(e22,e20) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_109,plain,
( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_112,plain,
( op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_115,plain,
op1(e11,e10) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_116,plain,
op1(e12,e10) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_117,plain,
op1(e10,e10) != op1(e12,e10),
inference(copy,[status(thm)],[c_116]) ).
cnf(c_118,plain,
op1(e13,e10) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_121,plain,
op1(e13,e10) != op1(e11,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_122,plain,
op1(e13,e10) != op1(e12,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_127,plain,
op1(e12,e11) != op1(e11,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_128,plain,
op1(e11,e11) != op1(e12,e11),
inference(copy,[status(thm)],[c_127]) ).
cnf(c_130,plain,
op1(e13,e11) != op1(e12,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_132,plain,
op1(e12,e12) != op1(e10,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_133,plain,
op1(e10,e12) != op1(e12,e12),
inference(copy,[status(thm)],[c_132]) ).
cnf(c_134,plain,
op1(e13,e12) != op1(e10,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_135,plain,
op1(e12,e12) != op1(e11,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_136,plain,
op1(e11,e12) != op1(e12,e12),
inference(copy,[status(thm)],[c_135]) ).
cnf(c_137,plain,
op1(e13,e12) != op1(e11,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_138,plain,
op1(e13,e12) != op1(e12,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_139,plain,
op1(e11,e13) != op1(e10,e13),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_140,plain,
op1(e12,e13) != op1(e10,e13),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_141,plain,
op1(e10,e13) != op1(e12,e13),
inference(copy,[status(thm)],[c_140]) ).
cnf(c_142,plain,
op1(e13,e13) != op1(e10,e13),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_145,plain,
op1(e13,e13) != op1(e11,e13),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_150,plain,
op1(e10,e13) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_153,plain,
op1(e10,e13) != op1(e10,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_155,plain,
op1(e11,e11) != op1(e11,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_156,plain,
op1(e11,e12) != op1(e11,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_157,plain,
op1(e11,e10) != op1(e11,e12),
inference(copy,[status(thm)],[c_156]) ).
cnf(c_162,plain,
op1(e11,e13) != op1(e11,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_163,plain,
op1(e12,e11) != op1(e12,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_167,plain,
op1(e12,e12) != op1(e12,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_168,plain,
op1(e12,e11) != op1(e12,e12),
inference(copy,[status(thm)],[c_167]) ).
cnf(c_171,plain,
op1(e13,e11) != op1(e13,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_172,plain,
op1(e13,e12) != op1(e13,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_173,plain,
op1(e13,e10) != op1(e13,e12),
inference(copy,[status(thm)],[c_172]) ).
cnf(c_174,plain,
op1(e13,e13) != op1(e13,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_175,plain,
op1(e13,e12) != op1(e13,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_176,plain,
op1(e13,e11) != op1(e13,e12),
inference(copy,[status(thm)],[c_175]) ).
cnf(c_179,plain,
op2(e21,e20) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_180,plain,
op2(e22,e20) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_181,plain,
op2(e20,e20) != op2(e22,e20),
inference(copy,[status(thm)],[c_180]) ).
cnf(c_182,plain,
op2(e23,e20) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_185,plain,
op2(e23,e20) != op2(e21,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_186,plain,
op2(e23,e20) != op2(e22,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_191,plain,
op2(e22,e21) != op2(e21,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_192,plain,
op2(e21,e21) != op2(e22,e21),
inference(copy,[status(thm)],[c_191]) ).
cnf(c_194,plain,
op2(e23,e21) != op2(e22,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_196,plain,
op2(e22,e22) != op2(e20,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_197,plain,
op2(e20,e22) != op2(e22,e22),
inference(copy,[status(thm)],[c_196]) ).
cnf(c_198,plain,
op2(e23,e22) != op2(e20,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_199,plain,
op2(e22,e22) != op2(e21,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_200,plain,
op2(e21,e22) != op2(e22,e22),
inference(copy,[status(thm)],[c_199]) ).
cnf(c_201,plain,
op2(e23,e22) != op2(e21,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_202,plain,
op2(e23,e22) != op2(e22,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_203,plain,
op2(e21,e23) != op2(e20,e23),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_204,plain,
op2(e22,e23) != op2(e20,e23),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_205,plain,
op2(e20,e23) != op2(e22,e23),
inference(copy,[status(thm)],[c_204]) ).
cnf(c_206,plain,
op2(e23,e23) != op2(e20,e23),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_209,plain,
op2(e23,e23) != op2(e21,e23),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_210,plain,
op2(e23,e23) != op2(e22,e23),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_214,plain,
op2(e20,e23) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_217,plain,
op2(e20,e23) != op2(e20,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_219,plain,
op2(e21,e21) != op2(e21,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_220,plain,
op2(e21,e22) != op2(e21,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_221,plain,
op2(e21,e20) != op2(e21,e22),
inference(copy,[status(thm)],[c_220]) ).
cnf(c_226,plain,
op2(e21,e23) != op2(e21,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_227,plain,
op2(e22,e21) != op2(e22,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_231,plain,
op2(e22,e22) != op2(e22,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_232,plain,
op2(e22,e21) != op2(e22,e22),
inference(copy,[status(thm)],[c_231]) ).
cnf(c_235,plain,
op2(e23,e21) != op2(e23,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_236,plain,
op2(e23,e22) != op2(e23,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_237,plain,
op2(e23,e20) != op2(e23,e22),
inference(copy,[status(thm)],[c_236]) ).
cnf(c_238,plain,
op2(e23,e23) != op2(e23,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_239,plain,
op2(e23,e22) != op2(e23,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_240,plain,
op2(e23,e21) != op2(e23,e22),
inference(copy,[status(thm)],[c_239]) ).
cnf(c_243,plain,
e11 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_244,plain,
e12 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_245,plain,
e10 != e12,
inference(copy,[status(thm)],[c_244]) ).
cnf(c_246,plain,
e13 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_247,plain,
e12 != e11,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_248,plain,
e11 != e12,
inference(copy,[status(thm)],[c_247]) ).
cnf(c_249,plain,
e13 != e11,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_250,plain,
e13 != e12,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_251,plain,
e21 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_252,plain,
e22 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_253,plain,
e20 != e22,
inference(copy,[status(thm)],[c_252]) ).
cnf(c_254,plain,
e23 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_255,plain,
e22 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_256,plain,
e21 != e22,
inference(copy,[status(thm)],[c_255]) ).
cnf(c_257,plain,
e23 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_258,plain,
e23 != e22,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_360,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e12,op1(e12,e12)) = e12
| op1(e10,op1(e11,e10)) = e10
| op1(e11,op1(e10,e11)) = e11 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_424,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e12,op1(e12,e12)) = e12
| op1(e10,op1(e11,e10)) = e10
| op1(e12,op1(e10,e12)) = e12 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_440,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e12,op1(e12,e12)) = e12
| op1(e11,op1(e11,e11)) = e11
| op1(e12,op1(e10,e12)) = e12 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_488,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e12,op1(e12,e12)) = e12
| op1(e10,op1(e11,e10)) = e10
| op1(e13,op1(e10,e13)) = e13 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_504,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e12,op1(e12,e12)) = e12
| op1(e11,op1(e11,e11)) = e11
| op1(e13,op1(e10,e13)) = e13 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_616,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e22,op2(e22,e22)) = e22
| op2(e20,op2(e21,e20)) = e20
| op2(e21,op2(e20,e21)) = e21 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_680,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e22,op2(e22,e22)) = e22
| op2(e20,op2(e21,e20)) = e20
| op2(e22,op2(e20,e22)) = e22 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_696,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e22,op2(e22,e22)) = e22
| op2(e21,op2(e21,e21)) = e21
| op2(e22,op2(e20,e22)) = e22 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_744,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e22,op2(e22,e22)) = e22
| op2(e20,op2(e21,e20)) = e20
| op2(e23,op2(e20,e23)) = e23 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_760,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e22,op2(e22,e22)) = e22
| op2(e21,op2(e21,e21)) = e21
| op2(e23,op2(e20,e23)) = e23 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_800,plain,
op1(e12,e12) = e10,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_801,plain,
op1(e12,op1(e12,e12)) = e11,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_802,plain,
op1(e12,e10) = e11,
inference(paramod,[status(thm)],[c_800,c_801]) ).
cnf(c_803,plain,
op1(op1(e12,op1(e12,e12)),op1(e12,e12)) = e13,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_9044,plain,
op1(op1(e12,e10),op1(e12,e12)) = e13,
inference(paramod,[status(thm)],[c_800,c_803]) ).
cnf(c_9045,plain,
op1(e11,op1(e12,e12)) = e13,
inference(paramod,[status(thm)],[c_802,c_9044]) ).
cnf(c_804,plain,
op1(e11,e10) = e13,
inference(paramod,[status(thm)],[c_800,c_9045]) ).
cnf(c_805,plain,
op2(e22,e22) = e20,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_806,plain,
op2(e22,op2(e22,e22)) = e21,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_807,plain,
op2(e22,e20) = e21,
inference(paramod,[status(thm)],[c_805,c_806]) ).
cnf(c_808,plain,
op2(op2(e22,op2(e22,e22)),op2(e22,e22)) = e23,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_9046,plain,
op2(op2(e22,e20),op2(e22,e22)) = e23,
inference(paramod,[status(thm)],[c_805,c_808]) ).
cnf(c_9047,plain,
op2(e21,op2(e22,e22)) = e23,
inference(paramod,[status(thm)],[c_807,c_9046]) ).
cnf(c_809,plain,
op2(e21,e20) = e23,
inference(paramod,[status(thm)],[c_805,c_9047]) ).
cnf(c_818,plain,
h3(e12) = e22,
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_819,plain,
h3(e10) = op2(e22,e22),
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_820,plain,
h3(e10) = e20,
inference(paramod,[status(thm)],[c_805,c_819]) ).
cnf(c_821,plain,
h3(e11) = op2(e22,op2(e22,e22)),
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_9048,plain,
h3(e11) = op2(e22,e20),
inference(paramod,[status(thm)],[c_805,c_821]) ).
cnf(c_822,plain,
h3(e11) = e21,
inference(paramod,[status(thm)],[c_807,c_9048]) ).
cnf(c_823,plain,
h3(e13) = op2(op2(e22,op2(e22,e22)),op2(e22,e22)),
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_9049,plain,
h3(e13) = op2(op2(e22,e20),op2(e22,e22)),
inference(paramod,[status(thm)],[c_805,c_823]) ).
cnf(c_9050,plain,
h3(e13) = op2(e21,op2(e22,e22)),
inference(paramod,[status(thm)],[c_807,c_9049]) ).
cnf(c_9051,plain,
h3(e13) = op2(e21,e20),
inference(paramod,[status(thm)],[c_805,c_9050]) ).
cnf(c_824,plain,
h3(e13) = e23,
inference(paramod,[status(thm)],[c_809,c_9051]) ).
cnf(c_1530,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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)) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_9052,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e20,h3(e10)) ),
inference(paramod,[status(thm)],[c_820,c_1530]) ).
cnf(c_9053,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e20,e20) ),
inference(paramod,[status(thm)],[c_820,c_9052]) ).
cnf(c_9054,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e20,h3(e11))
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_820,c_9053]) ).
cnf(c_9055,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_822,c_9054]) ).
cnf(c_9056,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e20,h3(e12))
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_820,c_9055]) ).
cnf(c_9057,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_818,c_9056]) ).
cnf(c_9058,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e20,h3(e13))
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_820,c_9057]) ).
cnf(c_9059,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_824,c_9058]) ).
cnf(c_9060,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e13) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_804,c_9059]) ).
cnf(c_9061,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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))
| e23 != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_824,c_9060]) ).
cnf(c_9062,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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))
| e23 != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_822,c_9061]) ).
cnf(c_9063,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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))
| e23 != op2(e21,e20)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_820,c_9062]) ).
cnf(c_9064,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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))
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_809,c_9063]) ).
cnf(c_9065,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e21,h3(e11))
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_822,c_9064]) ).
cnf(c_9066,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_822,c_9065]) ).
cnf(c_9067,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e21,h3(e12))
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_822,c_9066]) ).
cnf(c_9068,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_818,c_9067]) ).
cnf(c_9069,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e21,h3(e13))
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_822,c_9068]) ).
cnf(c_9070,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_824,c_9069]) ).
cnf(c_9071,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e11) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_802,c_9070]) ).
cnf(c_9072,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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))
| e21 != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_822,c_9071]) ).
cnf(c_9073,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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))
| e21 != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_818,c_9072]) ).
cnf(c_9074,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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))
| e21 != op2(e22,e20)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_820,c_9073]) ).
cnf(c_9075,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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))
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_807,c_9074]) ).
cnf(c_9076,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e22,h3(e11))
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_818,c_9075]) ).
cnf(c_9077,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_822,c_9076]) ).
cnf(c_9078,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e10) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_800,c_9077]) ).
cnf(c_9079,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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))
| e20 != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_820,c_9078]) ).
cnf(c_9080,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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))
| e20 != op2(e22,h3(e12))
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_818,c_9079]) ).
cnf(c_9081,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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))
| e20 != op2(e22,e22)
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_818,c_9080]) ).
cnf(c_9082,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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))
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_805,c_9081]) ).
cnf(c_9083,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e22,h3(e13))
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_818,c_9082]) ).
cnf(c_9084,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_824,c_9083]) ).
cnf(c_9085,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_824,c_9084]) ).
cnf(c_9086,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_820,c_9085]) ).
cnf(c_9087,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_824,c_9086]) ).
cnf(c_9088,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| 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(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_822,c_9087]) ).
cnf(c_9089,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(e23,h3(e12))
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_824,c_9088]) ).
cnf(c_9090,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_818,c_9089]) ).
cnf(c_9091,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(e23,h3(e13))
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_824,c_9090]) ).
cnf(c_9092,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_824,c_9091]) ).
cnf(c_9093,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| e20 != e20
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_820,c_9092]) ).
cnf(c_9094,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| e21 != e21
| e20 != e20
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_822,c_9093]) ).
cnf(c_9095,negated_conjecture,
( h3(e13) != e23
| e22 != e22
| e21 != e21
| e20 != e20
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_818,c_9094]) ).
cnf(c_9096,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e23 != e23
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_824,c_9095]) ).
cnf(c_9097,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_9096]) ).
cnf(c_9098,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_9097]) ).
cnf(c_9099,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_9098]) ).
cnf(c_9100,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_9099]) ).
cnf(c_9101,negated_conjecture,
( e23 != e23
| e22 != e22
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_9100]) ).
cnf(c_9102,negated_conjecture,
( e23 != e23
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_9101]) ).
cnf(c_1531,negated_conjecture,
( h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_9102]) ).
cnf(c_9103,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e12,e10) = e12
| op1(e11,op1(e11,e11)) = e11
| op1(e13,op1(e10,e13)) = e13 ),
inference(paramod,[status(thm)],[c_800,c_504]) ).
cnf(c_9104,plain,
( op1(e10,op1(e13,e10)) = e10
| e11 = e12
| op1(e11,op1(e11,e11)) = e11
| op1(e13,op1(e10,e13)) = e13 ),
inference(paramod,[status(thm)],[c_802,c_9103]) ).
cnf(c_2108,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e11,op1(e11,e11)) = e11
| op1(e13,op1(e10,e13)) = e13 ),
inference(resolve,[status(thm)],[c_248,c_9104]) ).
cnf(c_9105,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e12,op1(e12,e12)) = e12
| op1(e10,e13) = e10
| op1(e13,op1(e10,e13)) = e13 ),
inference(paramod,[status(thm)],[c_804,c_488]) ).
cnf(c_9106,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e12,e10) = e12
| op1(e10,e13) = e10
| op1(e13,op1(e10,e13)) = e13 ),
inference(paramod,[status(thm)],[c_800,c_9105]) ).
cnf(c_9107,plain,
( op1(e10,op1(e13,e10)) = e10
| e11 = e12
| op1(e10,e13) = e10
| op1(e13,op1(e10,e13)) = e13 ),
inference(paramod,[status(thm)],[c_802,c_9106]) ).
cnf(c_2112,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e10,e13) = e10
| op1(e13,op1(e10,e13)) = e13 ),
inference(resolve,[status(thm)],[c_248,c_9107]) ).
cnf(c_9108,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e12,e10) = e12
| op1(e11,op1(e11,e11)) = e11
| op1(e12,op1(e10,e12)) = e12 ),
inference(paramod,[status(thm)],[c_800,c_440]) ).
cnf(c_9109,plain,
( op1(e10,op1(e13,e10)) = e10
| e11 = e12
| op1(e11,op1(e11,e11)) = e11
| op1(e12,op1(e10,e12)) = e12 ),
inference(paramod,[status(thm)],[c_802,c_9108]) ).
cnf(c_2124,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e11,op1(e11,e11)) = e11
| op1(e12,op1(e10,e12)) = e12 ),
inference(resolve,[status(thm)],[c_248,c_9109]) ).
cnf(c_9110,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e12,op1(e12,e12)) = e12
| op1(e10,e13) = e10
| op1(e12,op1(e10,e12)) = e12 ),
inference(paramod,[status(thm)],[c_804,c_424]) ).
cnf(c_9111,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e12,e10) = e12
| op1(e10,e13) = e10
| op1(e12,op1(e10,e12)) = e12 ),
inference(paramod,[status(thm)],[c_800,c_9110]) ).
cnf(c_9112,plain,
( op1(e10,op1(e13,e10)) = e10
| e11 = e12
| op1(e10,e13) = e10
| op1(e12,op1(e10,e12)) = e12 ),
inference(paramod,[status(thm)],[c_802,c_9111]) ).
cnf(c_2128,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e10,e13) = e10
| op1(e12,op1(e10,e12)) = e12 ),
inference(resolve,[status(thm)],[c_248,c_9112]) ).
cnf(c_9113,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e12,op1(e12,e12)) = e12
| op1(e10,e13) = e10
| op1(e11,op1(e10,e11)) = e11 ),
inference(paramod,[status(thm)],[c_804,c_360]) ).
cnf(c_9114,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e12,e10) = e12
| op1(e10,e13) = e10
| op1(e11,op1(e10,e11)) = e11 ),
inference(paramod,[status(thm)],[c_800,c_9113]) ).
cnf(c_9115,plain,
( op1(e10,op1(e13,e10)) = e10
| e11 = e12
| op1(e10,e13) = e10
| op1(e11,op1(e10,e11)) = e11 ),
inference(paramod,[status(thm)],[c_802,c_9114]) ).
cnf(c_2144,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e10,e13) = e10
| op1(e11,op1(e10,e11)) = e11 ),
inference(resolve,[status(thm)],[c_248,c_9115]) ).
cnf(c_2162,plain,
op1(e12,e11) != e10,
inference(paramod,[status(thm)],[c_800,c_168]) ).
cnf(c_2163,plain,
op1(e13,e12) != e10,
inference(paramod,[status(thm)],[c_800,c_138]) ).
cnf(c_2164,plain,
op1(e11,e12) != e10,
inference(paramod,[status(thm)],[c_800,c_136]) ).
cnf(c_2165,plain,
op1(e10,e12) != e10,
inference(paramod,[status(thm)],[c_800,c_133]) ).
cnf(c_9116,plain,
( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e11) = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_802,c_57]) ).
cnf(c_9117,plain,
( op1(e12,e13) = e13
| e10 = e13
| op1(e12,e11) = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_800,c_9116]) ).
cnf(c_9118,plain,
( op1(e12,e13) = e13
| e10 = e13
| op1(e12,e11) = e13
| e13 = e11 ),
inference(copy,[status(thm)],[c_9117]) ).
cnf(c_9119,plain,
( op1(e12,e13) = e13
| e13 = e10
| op1(e12,e11) = e13
| e13 = e11 ),
inference(copy,[status(thm)],[c_9118]) ).
cnf(c_9120,plain,
( op1(e12,e13) = e13
| e13 = e10
| op1(e12,e11) = e13 ),
inference(resolve,[status(thm)],[c_249,c_9119]) ).
cnf(c_2167,plain,
( op1(e12,e13) = e13
| op1(e12,e11) = e13 ),
inference(resolve,[status(thm)],[c_246,c_9120]) ).
cnf(c_9121,plain,
( op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e11) = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_802,c_55]) ).
cnf(c_9122,plain,
( op1(e12,e13) = e12
| e10 = e12
| op1(e12,e11) = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_800,c_9121]) ).
cnf(c_9123,plain,
( op1(e12,e13) = e12
| e10 = e12
| op1(e12,e11) = e12 ),
inference(resolve,[status(thm)],[c_248,c_9122]) ).
cnf(c_2169,plain,
( op1(e12,e13) = e12
| op1(e12,e11) = e12 ),
inference(resolve,[status(thm)],[c_245,c_9123]) ).
cnf(c_9124,plain,
( op1(e13,e12) = e11
| e10 = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(paramod,[status(thm)],[c_800,c_54]) ).
cnf(c_9125,plain,
( op1(e13,e12) = e11
| e11 = e10
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(copy,[status(thm)],[c_9124]) ).
cnf(c_2170,plain,
( op1(e13,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(resolve,[status(thm)],[c_243,c_9125]) ).
cnf(c_2172,plain,
op1(e12,e11) != e11,
inference(paramod,[status(thm)],[c_802,c_163]) ).
cnf(c_2173,plain,
op1(e13,e10) != e11,
inference(paramod,[status(thm)],[c_802,c_122]) ).
cnf(c_2174,plain,
op1(e10,e10) != e11,
inference(paramod,[status(thm)],[c_802,c_117]) ).
cnf(c_9126,plain,
( op1(e13,e10) = e12
| op1(e12,e10) = e12
| e13 = e12
| op1(e10,e10) = e12 ),
inference(paramod,[status(thm)],[c_804,c_40]) ).
cnf(c_9127,plain,
( op1(e13,e10) = e12
| e11 = e12
| e13 = e12
| op1(e10,e10) = e12 ),
inference(paramod,[status(thm)],[c_802,c_9126]) ).
cnf(c_9128,plain,
( op1(e13,e10) = e12
| e11 = e12
| op1(e10,e10) = e12 ),
inference(resolve,[status(thm)],[c_250,c_9127]) ).
cnf(c_2175,plain,
( op1(e13,e10) = e12
| op1(e10,e10) = e12 ),
inference(resolve,[status(thm)],[c_248,c_9128]) ).
cnf(c_9129,plain,
( op1(e13,e10) = e10
| op1(e12,e10) = e10
| e13 = e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_804,c_36]) ).
cnf(c_9130,plain,
( op1(e13,e10) = e10
| e11 = e10
| e13 = e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_802,c_9129]) ).
cnf(c_9131,plain,
( op1(e13,e10) = e10
| e11 = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_246,c_9130]) ).
cnf(c_2176,plain,
( op1(e13,e10) = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_243,c_9131]) ).
cnf(c_9132,plain,
e13 != op1(e11,e12),
inference(paramod,[status(thm)],[c_804,c_157]) ).
cnf(c_2178,plain,
op1(e11,e12) != e13,
inference(copy,[status(thm)],[c_9132]) ).
cnf(c_2179,plain,
op1(e11,e11) != e13,
inference(paramod,[status(thm)],[c_804,c_155]) ).
cnf(c_2180,plain,
op1(e13,e10) != e13,
inference(paramod,[status(thm)],[c_804,c_121]) ).
cnf(c_9133,plain,
e13 != op1(e10,e10),
inference(paramod,[status(thm)],[c_804,c_115]) ).
cnf(c_2181,plain,
op1(e10,e10) != e13,
inference(copy,[status(thm)],[c_9133]) ).
cnf(c_9134,plain,
( op1(e11,e13) = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12
| e13 = e12 ),
inference(paramod,[status(thm)],[c_804,c_47]) ).
cnf(c_2182,plain,
( op1(e11,e13) = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12 ),
inference(resolve,[status(thm)],[c_250,c_9134]) ).
cnf(c_9135,plain,
( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| e13 = e10 ),
inference(paramod,[status(thm)],[c_804,c_43]) ).
cnf(c_9136,plain,
( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10 ),
inference(resolve,[status(thm)],[c_246,c_9135]) ).
cnf(c_2184,plain,
( op1(e11,e13) = e10
| op1(e11,e11) = e10 ),
inference(resolve,[status(thm)],[c_2164,c_9136]) ).
cnf(c_9137,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e22,e20) = e22
| op2(e21,op2(e21,e21)) = e21
| op2(e23,op2(e20,e23)) = e23 ),
inference(paramod,[status(thm)],[c_805,c_760]) ).
cnf(c_9138,plain,
( op2(e20,op2(e23,e20)) = e20
| e21 = e22
| op2(e21,op2(e21,e21)) = e21
| op2(e23,op2(e20,e23)) = e23 ),
inference(paramod,[status(thm)],[c_807,c_9137]) ).
cnf(c_2196,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e21,op2(e21,e21)) = e21
| op2(e23,op2(e20,e23)) = e23 ),
inference(resolve,[status(thm)],[c_256,c_9138]) ).
cnf(c_9139,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e22,op2(e22,e22)) = e22
| op2(e20,e23) = e20
| op2(e23,op2(e20,e23)) = e23 ),
inference(paramod,[status(thm)],[c_809,c_744]) ).
cnf(c_9140,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e22,e20) = e22
| op2(e20,e23) = e20
| op2(e23,op2(e20,e23)) = e23 ),
inference(paramod,[status(thm)],[c_805,c_9139]) ).
cnf(c_9141,plain,
( op2(e20,op2(e23,e20)) = e20
| e21 = e22
| op2(e20,e23) = e20
| op2(e23,op2(e20,e23)) = e23 ),
inference(paramod,[status(thm)],[c_807,c_9140]) ).
cnf(c_2200,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e20,e23) = e20
| op2(e23,op2(e20,e23)) = e23 ),
inference(resolve,[status(thm)],[c_256,c_9141]) ).
cnf(c_9142,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e22,e20) = e22
| op2(e21,op2(e21,e21)) = e21
| op2(e22,op2(e20,e22)) = e22 ),
inference(paramod,[status(thm)],[c_805,c_696]) ).
cnf(c_9143,plain,
( op2(e20,op2(e23,e20)) = e20
| e21 = e22
| op2(e21,op2(e21,e21)) = e21
| op2(e22,op2(e20,e22)) = e22 ),
inference(paramod,[status(thm)],[c_807,c_9142]) ).
cnf(c_2212,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e21,op2(e21,e21)) = e21
| op2(e22,op2(e20,e22)) = e22 ),
inference(resolve,[status(thm)],[c_256,c_9143]) ).
cnf(c_9144,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e22,op2(e22,e22)) = e22
| op2(e20,e23) = e20
| op2(e22,op2(e20,e22)) = e22 ),
inference(paramod,[status(thm)],[c_809,c_680]) ).
cnf(c_9145,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e22,e20) = e22
| op2(e20,e23) = e20
| op2(e22,op2(e20,e22)) = e22 ),
inference(paramod,[status(thm)],[c_805,c_9144]) ).
cnf(c_9146,plain,
( op2(e20,op2(e23,e20)) = e20
| e21 = e22
| op2(e20,e23) = e20
| op2(e22,op2(e20,e22)) = e22 ),
inference(paramod,[status(thm)],[c_807,c_9145]) ).
cnf(c_2216,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e20,e23) = e20
| op2(e22,op2(e20,e22)) = e22 ),
inference(resolve,[status(thm)],[c_256,c_9146]) ).
cnf(c_9147,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e22,op2(e22,e22)) = e22
| op2(e20,e23) = e20
| op2(e21,op2(e20,e21)) = e21 ),
inference(paramod,[status(thm)],[c_809,c_616]) ).
cnf(c_9148,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e22,e20) = e22
| op2(e20,e23) = e20
| op2(e21,op2(e20,e21)) = e21 ),
inference(paramod,[status(thm)],[c_805,c_9147]) ).
cnf(c_9149,plain,
( op2(e20,op2(e23,e20)) = e20
| e21 = e22
| op2(e20,e23) = e20
| op2(e21,op2(e20,e21)) = e21 ),
inference(paramod,[status(thm)],[c_807,c_9148]) ).
cnf(c_2232,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e20,e23) = e20
| op2(e21,op2(e20,e21)) = e21 ),
inference(resolve,[status(thm)],[c_256,c_9149]) ).
cnf(c_2250,plain,
op2(e22,e21) != e20,
inference(paramod,[status(thm)],[c_805,c_232]) ).
cnf(c_2251,plain,
op2(e23,e22) != e20,
inference(paramod,[status(thm)],[c_805,c_202]) ).
cnf(c_2252,plain,
op2(e21,e22) != e20,
inference(paramod,[status(thm)],[c_805,c_200]) ).
cnf(c_2253,plain,
op2(e20,e22) != e20,
inference(paramod,[status(thm)],[c_805,c_197]) ).
cnf(c_9150,plain,
( op2(e22,e23) = e23
| op2(e22,e22) = e23
| op2(e22,e21) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_807,c_105]) ).
cnf(c_9151,plain,
( op2(e22,e23) = e23
| e20 = e23
| op2(e22,e21) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_805,c_9150]) ).
cnf(c_9152,plain,
( op2(e22,e23) = e23
| e20 = e23
| op2(e22,e21) = e23
| e23 = e21 ),
inference(copy,[status(thm)],[c_9151]) ).
cnf(c_9153,plain,
( op2(e22,e23) = e23
| e23 = e20
| op2(e22,e21) = e23
| e23 = e21 ),
inference(copy,[status(thm)],[c_9152]) ).
cnf(c_9154,plain,
( op2(e22,e23) = e23
| e23 = e20
| op2(e22,e21) = e23 ),
inference(resolve,[status(thm)],[c_257,c_9153]) ).
cnf(c_2255,plain,
( op2(e22,e23) = e23
| op2(e22,e21) = e23 ),
inference(resolve,[status(thm)],[c_254,c_9154]) ).
cnf(c_9155,plain,
( op2(e22,e23) = e22
| op2(e22,e22) = e22
| op2(e22,e21) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_807,c_103]) ).
cnf(c_9156,plain,
( op2(e22,e23) = e22
| e20 = e22
| op2(e22,e21) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_805,c_9155]) ).
cnf(c_9157,plain,
( op2(e22,e23) = e22
| e20 = e22
| op2(e22,e21) = e22 ),
inference(resolve,[status(thm)],[c_256,c_9156]) ).
cnf(c_2257,plain,
( op2(e22,e23) = e22
| op2(e22,e21) = e22 ),
inference(resolve,[status(thm)],[c_253,c_9157]) ).
cnf(c_9158,plain,
( op2(e23,e22) = e21
| e20 = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 ),
inference(paramod,[status(thm)],[c_805,c_102]) ).
cnf(c_9159,plain,
( op2(e23,e22) = e21
| e21 = e20
| op2(e21,e22) = e21
| op2(e20,e22) = e21 ),
inference(copy,[status(thm)],[c_9158]) ).
cnf(c_2258,plain,
( op2(e23,e22) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 ),
inference(resolve,[status(thm)],[c_251,c_9159]) ).
cnf(c_2260,plain,
op2(e22,e21) != e21,
inference(paramod,[status(thm)],[c_807,c_227]) ).
cnf(c_2261,plain,
op2(e23,e20) != e21,
inference(paramod,[status(thm)],[c_807,c_186]) ).
cnf(c_2262,plain,
op2(e20,e20) != e21,
inference(paramod,[status(thm)],[c_807,c_181]) ).
cnf(c_9160,plain,
( op2(e23,e20) = e22
| op2(e22,e20) = e22
| e23 = e22
| op2(e20,e20) = e22 ),
inference(paramod,[status(thm)],[c_809,c_88]) ).
cnf(c_9161,plain,
( op2(e23,e20) = e22
| e21 = e22
| e23 = e22
| op2(e20,e20) = e22 ),
inference(paramod,[status(thm)],[c_807,c_9160]) ).
cnf(c_9162,plain,
( op2(e23,e20) = e22
| e21 = e22
| op2(e20,e20) = e22 ),
inference(resolve,[status(thm)],[c_258,c_9161]) ).
cnf(c_2263,plain,
( op2(e23,e20) = e22
| op2(e20,e20) = e22 ),
inference(resolve,[status(thm)],[c_256,c_9162]) ).
cnf(c_9163,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| e23 = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_809,c_84]) ).
cnf(c_9164,plain,
( op2(e23,e20) = e20
| e21 = e20
| e23 = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_807,c_9163]) ).
cnf(c_9165,plain,
( op2(e23,e20) = e20
| e21 = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_254,c_9164]) ).
cnf(c_2264,plain,
( op2(e23,e20) = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_251,c_9165]) ).
cnf(c_9166,plain,
e23 != op2(e21,e22),
inference(paramod,[status(thm)],[c_809,c_221]) ).
cnf(c_2266,plain,
op2(e21,e22) != e23,
inference(copy,[status(thm)],[c_9166]) ).
cnf(c_2267,plain,
op2(e21,e21) != e23,
inference(paramod,[status(thm)],[c_809,c_219]) ).
cnf(c_2268,plain,
op2(e23,e20) != e23,
inference(paramod,[status(thm)],[c_809,c_185]) ).
cnf(c_9167,plain,
e23 != op2(e20,e20),
inference(paramod,[status(thm)],[c_809,c_179]) ).
cnf(c_2269,plain,
op2(e20,e20) != e23,
inference(copy,[status(thm)],[c_9167]) ).
cnf(c_9168,plain,
( op2(e21,e23) = e22
| op2(e21,e22) = e22
| op2(e21,e21) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_809,c_95]) ).
cnf(c_2270,plain,
( op2(e21,e23) = e22
| op2(e21,e22) = e22
| op2(e21,e21) = e22 ),
inference(resolve,[status(thm)],[c_258,c_9168]) ).
cnf(c_9169,plain,
( op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20
| e23 = e20 ),
inference(paramod,[status(thm)],[c_809,c_91]) ).
cnf(c_9170,plain,
( op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20 ),
inference(resolve,[status(thm)],[c_254,c_9169]) ).
cnf(c_2272,plain,
( op2(e21,e23) = e20
| op2(e21,e21) = e20 ),
inference(resolve,[status(thm)],[c_2252,c_9170]) ).
cnf(c_2275,plain,
( op1(e13,e11) = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 ),
inference(resolve,[status(thm)],[c_2162,c_44]) ).
cnf(c_9171,plain,
( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11 ),
inference(resolve,[status(thm)],[c_2162,c_28]) ).
cnf(c_2276,plain,
( op1(e12,e11) = e13
| op1(e12,e11) = e12 ),
inference(resolve,[status(thm)],[c_2172,c_9171]) ).
cnf(c_2277,plain,
( op1(e13,e13) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 ),
inference(resolve,[status(thm)],[c_2163,c_59]) ).
cnf(c_2278,plain,
( op1(e13,e12) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11 ),
inference(resolve,[status(thm)],[c_2163,c_33]) ).
cnf(c_9172,plain,
( op1(e11,e12) = e13
| op1(e11,e12) = e12
| op1(e11,e12) = e11 ),
inference(resolve,[status(thm)],[c_2164,c_25]) ).
cnf(c_2279,plain,
( op1(e11,e12) = e12
| op1(e11,e12) = e11 ),
inference(resolve,[status(thm)],[c_2178,c_9172]) ).
cnf(c_2280,plain,
( op1(e10,e13) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_2165,c_35]) ).
cnf(c_2281,plain,
( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11 ),
inference(resolve,[status(thm)],[c_2165,c_21]) ).
cnf(c_2284,plain,
( op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11 ),
inference(resolve,[status(thm)],[c_2173,c_61]) ).
cnf(c_9173,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e10 ),
inference(resolve,[status(thm)],[c_2173,c_31]) ).
cnf(c_2285,plain,
( op1(e13,e10) = e12
| op1(e13,e10) = e10 ),
inference(resolve,[status(thm)],[c_2180,c_9173]) ).
cnf(c_9174,plain,
( op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_2174,c_19]) ).
cnf(c_2287,plain,
( op1(e10,e10) = e12
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_2181,c_9174]) ).
cnf(c_2291,plain,
( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e10,e11) = e13 ),
inference(resolve,[status(thm)],[c_2179,c_50]) ).
cnf(c_2294,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13 ),
inference(resolve,[status(thm)],[c_2181,c_41]) ).
cnf(c_2297,plain,
( op2(e23,e21) = e20
| op2(e21,e21) = e20
| op2(e20,e21) = e20 ),
inference(resolve,[status(thm)],[c_2250,c_92]) ).
cnf(c_9175,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21 ),
inference(resolve,[status(thm)],[c_2250,c_76]) ).
cnf(c_2298,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22 ),
inference(resolve,[status(thm)],[c_2260,c_9175]) ).
cnf(c_2300,plain,
( op2(e23,e22) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21 ),
inference(resolve,[status(thm)],[c_2251,c_81]) ).
cnf(c_9176,plain,
( op2(e21,e22) = e23
| op2(e21,e22) = e22
| op2(e21,e22) = e21 ),
inference(resolve,[status(thm)],[c_2252,c_73]) ).
cnf(c_2301,plain,
( op2(e21,e22) = e22
| op2(e21,e22) = e21 ),
inference(resolve,[status(thm)],[c_2266,c_9176]) ).
cnf(c_2302,plain,
( op2(e20,e23) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_2253,c_83]) ).
cnf(c_2303,plain,
( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21 ),
inference(resolve,[status(thm)],[c_2253,c_69]) ).
cnf(c_2306,plain,
( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21 ),
inference(resolve,[status(thm)],[c_2261,c_109]) ).
cnf(c_9177,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e20 ),
inference(resolve,[status(thm)],[c_2261,c_79]) ).
cnf(c_2307,plain,
( op2(e23,e20) = e22
| op2(e23,e20) = e20 ),
inference(resolve,[status(thm)],[c_2268,c_9177]) ).
cnf(c_9178,plain,
( op2(e20,e20) = e23
| op2(e20,e20) = e22
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_2262,c_67]) ).
cnf(c_2309,plain,
( op2(e20,e20) = e22
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_2269,c_9178]) ).
cnf(c_2313,plain,
( op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_2267,c_98]) ).
cnf(c_2316,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_2269,c_89]) ).
cnf(c_2324,plain,
( op1(e13,e13) != e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 ),
inference(paramod,[status(thm)],[c_22,c_142]) ).
cnf(c_2352,plain,
( op2(e23,e23) != e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 ),
inference(paramod,[status(thm)],[c_70,c_206]) ).
cnf(c_9179,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e10,e13) = e10
| op1(e13,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 ),
inference(paramod,[status(thm)],[c_22,c_2112]) ).
cnf(c_2406,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e13,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 ),
inference(copy,[status(thm)],[c_9179]) ).
cnf(c_2450,plain,
( op1(e10,e13) != e13
| op1(e12,e11) = e13 ),
inference(paramod,[status(thm)],[c_2167,c_141]) ).
cnf(c_2464,plain,
( op1(e10,e13) != e12
| op1(e12,e11) = e12 ),
inference(paramod,[status(thm)],[c_2169,c_141]) ).
cnf(c_9180,plain,
( e12 != op1(e13,e12)
| op1(e10,e10) = e12 ),
inference(paramod,[status(thm)],[c_2175,c_173]) ).
cnf(c_2479,plain,
( op1(e13,e12) != e12
| op1(e10,e10) = e12 ),
inference(copy,[status(thm)],[c_9180]) ).
cnf(c_2480,plain,
( op1(e13,e13) != e12
| op1(e10,e10) = e12 ),
inference(paramod,[status(thm)],[c_2175,c_174]) ).
cnf(c_9181,plain,
( op1(e10,e12) = e10
| op1(e10,e13) = e10
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e12 ),
inference(paramod,[status(thm)],[c_2175,c_2128]) ).
cnf(c_2483,plain,
( op1(e10,e13) = e10
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e12 ),
inference(resolve,[status(thm)],[c_2165,c_9181]) ).
cnf(c_9182,plain,
( op1(e10,e12) = e10
| op1(e10,e13) = e10
| op1(e11,op1(e10,e11)) = e11
| op1(e10,e10) = e12 ),
inference(paramod,[status(thm)],[c_2175,c_2144]) ).
cnf(c_2486,plain,
( op1(e10,e13) = e10
| op1(e11,op1(e10,e11)) = e11
| op1(e10,e10) = e12 ),
inference(resolve,[status(thm)],[c_2165,c_9182]) ).
cnf(c_2490,plain,
( op1(e13,e11) != e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_2176,c_171]) ).
cnf(c_9183,plain,
( op1(e10,e10) = e10
| op1(e11,op1(e11,e11)) = e11
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_2176,c_2124]) ).
cnf(c_2493,plain,
( op1(e11,op1(e11,e11)) = e11
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_9183]) ).
cnf(c_9184,plain,
( op1(e10,e10) = e10
| op1(e10,e13) = e10
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_2176,c_2128]) ).
cnf(c_2494,plain,
( op1(e10,e13) = e10
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_9184]) ).
cnf(c_9185,plain,
( op1(e10,e10) = e10
| op1(e10,e13) = e10
| op1(e11,op1(e10,e11)) = e11
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_2176,c_2144]) ).
cnf(c_2497,plain,
( op1(e10,e13) = e10
| op1(e11,op1(e10,e11)) = e11
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_9185]) ).
cnf(c_9186,plain,
( e12 != op1(e10,e13)
| op1(e11,e12) = e12
| op1(e11,e11) = e12 ),
inference(paramod,[status(thm)],[c_2182,c_139]) ).
cnf(c_2501,plain,
( op1(e10,e13) != e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12 ),
inference(copy,[status(thm)],[c_9186]) ).
cnf(c_9187,plain,
( e10 != op1(e10,e13)
| op1(e11,e11) = e10 ),
inference(paramod,[status(thm)],[c_2184,c_139]) ).
cnf(c_2530,plain,
( op1(e10,e13) != e10
| op1(e11,e11) = e10 ),
inference(copy,[status(thm)],[c_9187]) ).
cnf(c_9188,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e20,e23) = e20
| op2(e23,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 ),
inference(paramod,[status(thm)],[c_70,c_2200]) ).
cnf(c_2574,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e23,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 ),
inference(copy,[status(thm)],[c_9188]) ).
cnf(c_2630,plain,
( op2(e20,e23) != e23
| op2(e22,e21) = e23 ),
inference(paramod,[status(thm)],[c_2255,c_205]) ).
cnf(c_2631,plain,
( op2(e23,e23) != e23
| op2(e22,e21) = e23 ),
inference(paramod,[status(thm)],[c_2255,c_210]) ).
cnf(c_2644,plain,
( op2(e20,e23) != e22
| op2(e22,e21) = e22 ),
inference(paramod,[status(thm)],[c_2257,c_205]) ).
cnf(c_9189,plain,
( e22 != op2(e23,e22)
| op2(e20,e20) = e22 ),
inference(paramod,[status(thm)],[c_2263,c_237]) ).
cnf(c_2659,plain,
( op2(e23,e22) != e22
| op2(e20,e20) = e22 ),
inference(copy,[status(thm)],[c_9189]) ).
cnf(c_2660,plain,
( op2(e23,e23) != e22
| op2(e20,e20) = e22 ),
inference(paramod,[status(thm)],[c_2263,c_238]) ).
cnf(c_9190,plain,
( op2(e20,e22) = e20
| op2(e20,e23) = e20
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e22 ),
inference(paramod,[status(thm)],[c_2263,c_2216]) ).
cnf(c_2663,plain,
( op2(e20,e23) = e20
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e22 ),
inference(resolve,[status(thm)],[c_2253,c_9190]) ).
cnf(c_9191,plain,
( op2(e20,e22) = e20
| op2(e20,e23) = e20
| op2(e21,op2(e20,e21)) = e21
| op2(e20,e20) = e22 ),
inference(paramod,[status(thm)],[c_2263,c_2232]) ).
cnf(c_2666,plain,
( op2(e20,e23) = e20
| op2(e21,op2(e20,e21)) = e21
| op2(e20,e20) = e22 ),
inference(resolve,[status(thm)],[c_2253,c_9191]) ).
cnf(c_2670,plain,
( op2(e23,e21) != e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_2264,c_235]) ).
cnf(c_9192,plain,
( op2(e20,e20) = e20
| op2(e21,op2(e21,e21)) = e21
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_2264,c_2212]) ).
cnf(c_2673,plain,
( op2(e21,op2(e21,e21)) = e21
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_9192]) ).
cnf(c_9193,plain,
( op2(e20,e20) = e20
| op2(e20,e23) = e20
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_2264,c_2216]) ).
cnf(c_2674,plain,
( op2(e20,e23) = e20
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_9193]) ).
cnf(c_9194,plain,
( op2(e20,e20) = e20
| op2(e20,e23) = e20
| op2(e21,op2(e20,e21)) = e21
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_2264,c_2232]) ).
cnf(c_2677,plain,
( op2(e20,e23) = e20
| op2(e21,op2(e20,e21)) = e21
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_9194]) ).
cnf(c_9195,plain,
( e22 != op2(e20,e23)
| op2(e21,e22) = e22
| op2(e21,e21) = e22 ),
inference(paramod,[status(thm)],[c_2270,c_203]) ).
cnf(c_2681,plain,
( op2(e20,e23) != e22
| op2(e21,e22) = e22
| op2(e21,e21) = e22 ),
inference(copy,[status(thm)],[c_9195]) ).
cnf(c_9196,plain,
( e20 != op2(e20,e23)
| op2(e21,e21) = e20 ),
inference(paramod,[status(thm)],[c_2272,c_203]) ).
cnf(c_2710,plain,
( op2(e20,e23) != e20
| op2(e21,e21) = e20 ),
inference(copy,[status(thm)],[c_9196]) ).
cnf(c_2761,plain,
( op1(e13,e11) != e13
| op1(e12,e11) = e12 ),
inference(paramod,[status(thm)],[c_2276,c_130]) ).
cnf(c_2783,plain,
( op1(e13,e11) != e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11 ),
inference(paramod,[status(thm)],[c_2278,c_176]) ).
cnf(c_2795,plain,
( op1(e13,e12) != e11
| op1(e11,e12) = e12 ),
inference(paramod,[status(thm)],[c_2279,c_137]) ).
cnf(c_9197,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e11,op1(e11,e11)) = e11
| op1(e13,e10) = e13
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_2280,c_2108]) ).
cnf(c_2804,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e11,op1(e11,e11)) = e11
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_2180,c_9197]) ).
cnf(c_9198,plain,
( e11 != op1(e11,e13)
| op1(e13,e12) = e11
| op1(e13,e11) = e11 ),
inference(paramod,[status(thm)],[c_2284,c_145]) ).
cnf(c_2846,plain,
( op1(e11,e13) != e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11 ),
inference(copy,[status(thm)],[c_9198]) ).
cnf(c_9199,plain,
( e10 != op1(e10,e10)
| op1(e13,e10) = e12 ),
inference(paramod,[status(thm)],[c_2285,c_118]) ).
cnf(c_2865,plain,
( op1(e10,e10) != e10
| op1(e13,e10) = e12 ),
inference(copy,[status(thm)],[c_9199]) ).
cnf(c_2883,plain,
( op1(e10,e13) != e10
| op1(e10,e10) = e12 ),
inference(paramod,[status(thm)],[c_2287,c_150]) ).
cnf(c_9200,plain,
( e13 != op1(e13,e12)
| op1(e12,e11) = e13
| op1(e10,e11) = e13 ),
inference(paramod,[status(thm)],[c_2291,c_176]) ).
cnf(c_2920,plain,
( op1(e13,e12) != e13
| op1(e12,e11) = e13
| op1(e10,e11) = e13 ),
inference(copy,[status(thm)],[c_9200]) ).
cnf(c_2995,plain,
( op2(e23,e21) != e23
| op2(e22,e21) = e22 ),
inference(paramod,[status(thm)],[c_2298,c_194]) ).
cnf(c_3020,plain,
( op2(e23,e21) != e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21 ),
inference(paramod,[status(thm)],[c_2300,c_240]) ).
cnf(c_3032,plain,
( op2(e23,e22) != e21
| op2(e21,e22) = e22 ),
inference(paramod,[status(thm)],[c_2301,c_201]) ).
cnf(c_9201,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e21,op2(e21,e21)) = e21
| op2(e23,e20) = e23
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_2302,c_2196]) ).
cnf(c_3041,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e21,op2(e21,e21)) = e21
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_2268,c_9201]) ).
cnf(c_9202,plain,
( e21 != op2(e21,e23)
| op2(e23,e22) = e21
| op2(e23,e21) = e21 ),
inference(paramod,[status(thm)],[c_2306,c_209]) ).
cnf(c_3086,plain,
( op2(e21,e23) != e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21 ),
inference(copy,[status(thm)],[c_9202]) ).
cnf(c_9203,plain,
( e20 != op2(e20,e20)
| op2(e23,e20) = e22 ),
inference(paramod,[status(thm)],[c_2307,c_182]) ).
cnf(c_3108,plain,
( op2(e20,e20) != e20
| op2(e23,e20) = e22 ),
inference(copy,[status(thm)],[c_9203]) ).
cnf(c_3126,plain,
( op2(e20,e23) != e20
| op2(e20,e20) = e22 ),
inference(paramod,[status(thm)],[c_2309,c_214]) ).
cnf(c_9204,plain,
( e23 != op2(e23,e22)
| op2(e22,e21) = e23
| op2(e20,e21) = e23 ),
inference(paramod,[status(thm)],[c_2313,c_240]) ).
cnf(c_3169,plain,
( op2(e23,e22) != e23
| op2(e22,e21) = e23
| op2(e20,e21) = e23 ),
inference(copy,[status(thm)],[c_9204]) ).
cnf(c_3213,plain,
( op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e12,e11) = e13 ),
inference(resolve,[status(thm)],[c_2450,c_2294]) ).
cnf(c_3223,plain,
( op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12
| op1(e10,e10) = e12 ),
inference(resolve,[status(thm)],[c_2480,c_64]) ).
cnf(c_3224,plain,
( op1(e11,e11) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_2490,c_2275]) ).
cnf(c_3228,plain,
( op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e22,e21) = e23 ),
inference(resolve,[status(thm)],[c_2630,c_2316]) ).
cnf(c_3231,plain,
( op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e23,e23) = e20
| op2(e22,e21) = e23 ),
inference(resolve,[status(thm)],[c_2631,c_82]) ).
cnf(c_3237,plain,
( op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22
| op2(e20,e20) = e22 ),
inference(resolve,[status(thm)],[c_2660,c_112]) ).
cnf(c_3239,plain,
( op2(e21,e21) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_2670,c_2297]) ).
cnf(c_3303,plain,
( op1(e12,e11) = e13
| op1(e10,e11) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11 ),
inference(resolve,[status(thm)],[c_2783,c_2291]) ).
cnf(c_3320,plain,
( op2(e22,e21) = e23
| op2(e20,e21) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21 ),
inference(resolve,[status(thm)],[c_3020,c_2313]) ).
cnf(c_9205,plain,
( op1(e10,e10) = e12
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e12 ),
inference(resolve,[status(thm)],[c_2483,c_2883]) ).
cnf(c_3702,plain,
( op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e12 ),
inference(copy,[status(thm)],[c_9205]) ).
cnf(c_3711,plain,
( op1(e10,e13) = e10
| op1(e11,e13) = e11
| op1(e10,e10) = e12
| op1(e10,e12) = e13
| op1(e12,e11) = e13 ),
inference(paramod,[status(thm)],[c_3213,c_2486]) ).
cnf(c_3715,plain,
( op1(e11,e11) = e10
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_2494,c_2530]) ).
cnf(c_9206,plain,
( op2(e20,e20) = e22
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e22 ),
inference(resolve,[status(thm)],[c_2663,c_3126]) ).
cnf(c_3724,plain,
( op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e22 ),
inference(copy,[status(thm)],[c_9206]) ).
cnf(c_3742,plain,
( op2(e20,e23) = e20
| op2(e21,e23) = e21
| op2(e20,e20) = e22
| op2(e20,e22) = e23
| op2(e22,e21) = e23 ),
inference(paramod,[status(thm)],[c_3228,c_2666]) ).
cnf(c_3745,plain,
( op2(e21,e21) = e20
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_2674,c_2710]) ).
cnf(c_9207,plain,
( op1(e11,e10) = e11
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e10
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_3715,c_2493]) ).
cnf(c_9208,plain,
( e13 = e11
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e10
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_804,c_9207]) ).
cnf(c_9209,plain,
( e13 = e11
| op1(e12,op1(e10,e12)) = e12
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_9208]) ).
cnf(c_9210,plain,
( e13 = e11
| op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_9209]) ).
cnf(c_3857,plain,
( op1(e12,op1(e10,e12)) = e12
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_249,c_9210]) ).
cnf(c_9211,plain,
( op1(e12,op1(e10,e12)) = e12
| e10 = e12
| op1(e12,op1(e10,e12)) = e12 ),
inference(paramod,[status(thm)],[c_3857,c_3702]) ).
cnf(c_9212,plain,
( e10 = e12
| op1(e12,op1(e10,e12)) = e12 ),
inference(copy,[status(thm)],[c_9211]) ).
cnf(c_3863,plain,
op1(e12,op1(e10,e12)) = e12,
inference(resolve,[status(thm)],[c_245,c_9212]) ).
cnf(c_3864,plain,
( op1(e12,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e12) = e11 ),
inference(paramod,[status(thm)],[c_2281,c_3863]) ).
cnf(c_3867,plain,
( op1(e13,e12) != e11
| op1(e12,e13) = e12
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_3864,c_134]) ).
cnf(c_9213,plain,
( op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10
| op1(e10,op1(e13,e10)) = e10
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 ),
inference(resolve,[status(thm)],[c_2406,c_2324]) ).
cnf(c_9214,plain,
( op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,op1(e13,e10)) = e10
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 ),
inference(copy,[status(thm)],[c_9213]) ).
cnf(c_9215,plain,
( op1(e10,e13) = e12
| op1(e10,op1(e13,e10)) = e10
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 ),
inference(copy,[status(thm)],[c_9214]) ).
cnf(c_3873,plain,
( op1(e10,op1(e13,e10)) = e10
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 ),
inference(copy,[status(thm)],[c_9215]) ).
cnf(c_9216,plain,
( op2(e21,e20) = e21
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e20
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_3745,c_2673]) ).
cnf(c_9217,plain,
( e23 = e21
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e20
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_809,c_9216]) ).
cnf(c_9218,plain,
( e23 = e21
| op2(e22,op2(e20,e22)) = e22
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_9217]) ).
cnf(c_9219,plain,
( e23 = e21
| op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_9218]) ).
cnf(c_4021,plain,
( op2(e22,op2(e20,e22)) = e22
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_257,c_9219]) ).
cnf(c_9220,plain,
( op2(e22,op2(e20,e22)) = e22
| e20 = e22
| op2(e22,op2(e20,e22)) = e22 ),
inference(paramod,[status(thm)],[c_4021,c_3724]) ).
cnf(c_9221,plain,
( e20 = e22
| op2(e22,op2(e20,e22)) = e22 ),
inference(copy,[status(thm)],[c_9220]) ).
cnf(c_4030,plain,
op2(e22,op2(e20,e22)) = e22,
inference(resolve,[status(thm)],[c_253,c_9221]) ).
cnf(c_4031,plain,
( op2(e22,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e22) = e21 ),
inference(paramod,[status(thm)],[c_2303,c_4030]) ).
cnf(c_4034,plain,
( op2(e23,e22) != e21
| op2(e22,e23) = e22
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_4031,c_198]) ).
cnf(c_9222,plain,
( e12 != op1(e11,e12)
| op1(e12,e13) = e12
| op1(e10,e13) = e12
| op1(e10,e10) = e12 ),
inference(paramod,[status(thm)],[c_3223,c_162]) ).
cnf(c_4706,plain,
( op1(e11,e12) != e12
| op1(e12,e13) = e12
| op1(e10,e13) = e12
| op1(e10,e10) = e12 ),
inference(copy,[status(thm)],[c_9222]) ).
cnf(c_9223,plain,
( e21 != op2(e21,e23)
| op2(e23,e23) = e22
| op2(e23,e23) = e20
| op2(e22,e21) = e23 ),
inference(paramod,[status(thm)],[c_3231,c_209]) ).
cnf(c_4755,plain,
( op2(e21,e23) != e21
| op2(e23,e23) = e22
| op2(e23,e23) = e20
| op2(e22,e21) = e23 ),
inference(copy,[status(thm)],[c_9223]) ).
cnf(c_9224,plain,
( e22 != op2(e21,e22)
| op2(e22,e23) = e22
| op2(e20,e23) = e22
| op2(e20,e20) = e22 ),
inference(paramod,[status(thm)],[c_3237,c_226]) ).
cnf(c_4800,plain,
( op2(e21,e22) != e22
| op2(e22,e23) = e22
| op2(e20,e23) = e22
| op2(e20,e20) = e22 ),
inference(copy,[status(thm)],[c_9224]) ).
cnf(c_5081,plain,
( op1(e12,e13) = e12
| op1(e10,e12) = e12
| op1(e12,e11) = e13
| op1(e10,e11) = e13
| op1(e13,e12) = e12 ),
inference(resolve,[status(thm)],[c_3303,c_3867]) ).
cnf(c_5200,plain,
( op2(e22,e23) = e22
| op2(e20,e22) = e22
| op2(e22,e21) = e23
| op2(e20,e21) = e23
| op2(e23,e22) = e22 ),
inference(resolve,[status(thm)],[c_3320,c_4034]) ).
cnf(c_9225,plain,
( op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20
| op2(e20,op2(e23,e20)) = e20
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 ),
inference(resolve,[status(thm)],[c_2574,c_2352]) ).
cnf(c_9226,plain,
( op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,op2(e23,e20)) = e20
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 ),
inference(copy,[status(thm)],[c_9225]) ).
cnf(c_9227,plain,
( op2(e20,e23) = e22
| op2(e20,op2(e23,e20)) = e20
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 ),
inference(copy,[status(thm)],[c_9226]) ).
cnf(c_5971,plain,
( op2(e20,op2(e23,e20)) = e20
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 ),
inference(copy,[status(thm)],[c_9227]) ).
cnf(c_9228,plain,
( op1(e10,e10) = e10
| op1(e11,op1(e11,e11)) = e11
| op1(e10,e11) = e10
| op1(e10,e10) = e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_2176,c_2804]) ).
cnf(c_9229,plain,
( op1(e10,e10) = e10
| op1(e11,op1(e11,e11)) = e11
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_9228]) ).
cnf(c_7324,plain,
( op1(e11,op1(e11,e11)) = e11
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_9229]) ).
cnf(c_9230,plain,
( op1(e11,e10) = e11
| op1(e10,e11) = e10
| op1(e10,e10) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_3224,c_7324]) ).
cnf(c_9231,plain,
( e13 = e11
| op1(e10,e11) = e10
| op1(e10,e10) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_804,c_9230]) ).
cnf(c_9232,plain,
( e13 = e11
| op1(e10,e11) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_9231]) ).
cnf(c_9233,plain,
( e13 = e11
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_9232]) ).
cnf(c_7387,plain,
( op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_249,c_9233]) ).
cnf(c_7390,plain,
( op1(e10,e13) != e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_7387,c_153]) ).
cnf(c_9234,plain,
( op1(e10,e13) = e10
| op1(e11,e10) = e11
| op1(e10,e10) = e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_7387,c_2497]) ).
cnf(c_9235,plain,
( op1(e10,e13) = e10
| e13 = e11
| op1(e10,e10) = e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_804,c_9234]) ).
cnf(c_9236,plain,
( op1(e10,e13) = e10
| e13 = e11
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_9235]) ).
cnf(c_7393,plain,
( op1(e10,e13) = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_249,c_9236]) ).
cnf(c_9237,plain,
( op1(e10,e10) = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_7393,c_7390]) ).
cnf(c_7401,plain,
op1(e10,e10) = e10,
inference(copy,[status(thm)],[c_9237]) ).
cnf(c_9238,plain,
( op1(e11,e12) != e12
| op1(e12,e13) = e12
| op1(e10,e13) = e12
| e10 = e12 ),
inference(paramod,[status(thm)],[c_7401,c_4706]) ).
cnf(c_7471,plain,
( op1(e11,e12) != e12
| op1(e12,e13) = e12
| op1(e10,e13) = e12 ),
inference(resolve,[status(thm)],[c_245,c_9238]) ).
cnf(c_9239,plain,
( op1(e10,e13) = e10
| op1(e11,e13) = e11
| e10 = e12
| op1(e10,e12) = e13
| op1(e12,e11) = e13 ),
inference(paramod,[status(thm)],[c_7401,c_3711]) ).
cnf(c_7490,plain,
( op1(e10,e13) = e10
| op1(e11,e13) = e11
| op1(e10,e12) = e13
| op1(e12,e11) = e13 ),
inference(resolve,[status(thm)],[c_245,c_9239]) ).
cnf(c_9240,plain,
( op1(e10,e13) != e10
| e10 = e12 ),
inference(paramod,[status(thm)],[c_7401,c_2883]) ).
cnf(c_7498,plain,
op1(e10,e13) != e10,
inference(resolve,[status(thm)],[c_245,c_9240]) ).
cnf(c_9241,plain,
( e10 != e10
| op1(e13,e10) = e12 ),
inference(paramod,[status(thm)],[c_7401,c_2865]) ).
cnf(c_7502,plain,
op1(e13,e10) = e12,
inference(copy,[status(thm)],[c_9241]) ).
cnf(c_9242,plain,
( op1(e10,e13) = e10
| op1(e11,op1(e10,e11)) = e11
| e10 = e12 ),
inference(paramod,[status(thm)],[c_7401,c_2486]) ).
cnf(c_9243,plain,
( op1(e10,e13) = e10
| op1(e11,op1(e10,e11)) = e11 ),
inference(resolve,[status(thm)],[c_245,c_9242]) ).
cnf(c_7503,plain,
op1(e11,op1(e10,e11)) = e11,
inference(resolve,[status(thm)],[c_7498,c_9243]) ).
cnf(c_9244,plain,
( op1(e13,e12) != e12
| e10 = e12 ),
inference(paramod,[status(thm)],[c_7401,c_2479]) ).
cnf(c_7505,plain,
op1(e13,e12) != e12,
inference(resolve,[status(thm)],[c_245,c_9244]) ).
cnf(c_9245,negated_conjecture,
( h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(e10) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_7401,c_1531]) ).
cnf(c_9246,negated_conjecture,
( h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_820,c_9245]) ).
cnf(c_9247,negated_conjecture,
( h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(e12) != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_7502,c_9246]) ).
cnf(c_9248,negated_conjecture,
( h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| e22 != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_818,c_9247]) ).
cnf(c_9249,negated_conjecture,
( h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| e22 != op2(e23,e20)
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_9248]) ).
cnf(c_7508,negated_conjecture,
( h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20 ),
inference(copy,[status(thm)],[c_9249]) ).
cnf(c_7511,plain,
( op1(e11,e13) = e11
| op1(e10,e12) = e13
| op1(e12,e11) = e13 ),
inference(resolve,[status(thm)],[c_7498,c_7490]) ).
cnf(c_9250,plain,
( op1(e10,e12) = e10
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 ),
inference(paramod,[status(thm)],[c_7502,c_3873]) ).
cnf(c_9251,plain,
( op1(e10,e12) = e10
| op1(e10,e13) = e12
| op1(e10,e13) = e11 ),
inference(resolve,[status(thm)],[c_7498,c_9250]) ).
cnf(c_7596,plain,
( op1(e10,e13) = e12
| op1(e10,e13) = e11 ),
inference(resolve,[status(thm)],[c_2165,c_9251]) ).
cnf(c_9252,plain,
( op1(e10,e12) = e10
| op1(e10,e13) = e10
| op1(e13,op1(e10,e13)) = e13 ),
inference(paramod,[status(thm)],[c_7502,c_2112]) ).
cnf(c_9253,plain,
( op1(e10,e12) = e10
| op1(e13,op1(e10,e13)) = e13 ),
inference(resolve,[status(thm)],[c_7498,c_9252]) ).
cnf(c_7613,plain,
op1(e13,op1(e10,e13)) = e13,
inference(resolve,[status(thm)],[c_2165,c_9253]) ).
cnf(c_9254,plain,
( op1(e13,e13) = e10
| op1(e13,e11) = e10
| e12 = e10 ),
inference(paramod,[status(thm)],[c_7502,c_2277]) ).
cnf(c_9255,plain,
( op1(e13,e13) = e10
| op1(e13,e11) = e10
| e10 = e12 ),
inference(copy,[status(thm)],[c_9254]) ).
cnf(c_7683,plain,
( op1(e13,e13) = e10
| op1(e13,e11) = e10 ),
inference(resolve,[status(thm)],[c_245,c_9255]) ).
cnf(c_7727,plain,
( op1(e12,e13) = e12
| op1(e10,e12) = e12
| op1(e12,e11) = e13
| op1(e10,e11) = e13 ),
inference(resolve,[status(thm)],[c_7505,c_5081]) ).
cnf(c_7736,plain,
( op1(e13,e11) != e13
| op1(e13,e12) = e11 ),
inference(resolve,[status(thm)],[c_7505,c_2783]) ).
cnf(c_7772,plain,
( op1(e13,e11) = e13
| op1(e10,e13) = e12 ),
inference(paramod,[status(thm)],[c_7596,c_7613]) ).
cnf(c_9256,plain,
( h3(e10) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_7683,c_7508]) ).
cnf(c_9257,plain,
( e20 != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_820,c_9256]) ).
cnf(c_7776,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(copy,[status(thm)],[c_9257]) ).
cnf(c_7807,plain,
( op1(e13,e12) = e11
| op1(e10,e13) = e12 ),
inference(resolve,[status(thm)],[c_7772,c_7736]) ).
cnf(c_7811,plain,
( op1(e12,e11) = e12
| op1(e10,e13) = e12 ),
inference(resolve,[status(thm)],[c_7772,c_2761]) ).
cnf(c_7818,plain,
( op1(e11,e12) = e12
| op1(e10,e13) = e12 ),
inference(resolve,[status(thm)],[c_7807,c_2795]) ).
cnf(c_9258,plain,
( op1(e12,e11) = e12
| op1(e12,e11) = e12 ),
inference(resolve,[status(thm)],[c_7811,c_2464]) ).
cnf(c_7830,plain,
op1(e12,e11) = e12,
inference(copy,[status(thm)],[c_9258]) ).
cnf(c_9259,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(e12) != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_7830,c_7776]) ).
cnf(c_9260,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| h3(op1(e12,e13)) != op2(e22,e23)
| e22 != op2(e22,e21)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_818,c_9259]) ).
cnf(c_7831,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| h3(op1(e12,e13)) != op2(e22,e23)
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(copy,[status(thm)],[c_9260]) ).
cnf(c_9261,plain,
( op1(e12,e13) = e12
| op1(e10,e12) = e12
| e12 = e13
| op1(e10,e11) = e13 ),
inference(paramod,[status(thm)],[c_7830,c_7727]) ).
cnf(c_9262,plain,
( op1(e12,e13) = e12
| op1(e10,e12) = e12
| e13 = e12
| op1(e10,e11) = e13 ),
inference(copy,[status(thm)],[c_9261]) ).
cnf(c_7834,plain,
( op1(e12,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e13 ),
inference(resolve,[status(thm)],[c_250,c_9262]) ).
cnf(c_9263,plain,
( op1(e11,e13) = e11
| op1(e10,e12) = e13
| e12 = e13 ),
inference(paramod,[status(thm)],[c_7830,c_7511]) ).
cnf(c_9264,plain,
( op1(e11,e13) = e11
| op1(e10,e12) = e13
| e13 = e12 ),
inference(copy,[status(thm)],[c_9263]) ).
cnf(c_7859,plain,
( op1(e11,e13) = e11
| op1(e10,e12) = e13 ),
inference(resolve,[status(thm)],[c_250,c_9264]) ).
cnf(c_9265,plain,
( op1(e13,e12) != e13
| e12 = e13
| op1(e10,e11) = e13 ),
inference(paramod,[status(thm)],[c_7830,c_2920]) ).
cnf(c_9266,plain,
( op1(e13,e12) != e13
| e13 = e12
| op1(e10,e11) = e13 ),
inference(copy,[status(thm)],[c_9265]) ).
cnf(c_7873,plain,
( op1(e13,e12) != e13
| op1(e10,e11) = e13 ),
inference(resolve,[status(thm)],[c_250,c_9266]) ).
cnf(c_9267,plain,
( op1(e12,e13) = e13
| e12 = e13 ),
inference(paramod,[status(thm)],[c_7830,c_2167]) ).
cnf(c_9268,plain,
( op1(e12,e13) = e13
| e13 = e12 ),
inference(copy,[status(thm)],[c_9267]) ).
cnf(c_7877,plain,
op1(e12,e13) = e13,
inference(resolve,[status(thm)],[c_250,c_9268]) ).
cnf(c_7878,plain,
op1(e11,e11) != e12,
inference(paramod,[status(thm)],[c_7830,c_128]) ).
cnf(c_9269,plain,
( e13 = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e13 ),
inference(paramod,[status(thm)],[c_7877,c_7834]) ).
cnf(c_7881,plain,
( op1(e10,e12) = e12
| op1(e10,e11) = e13 ),
inference(resolve,[status(thm)],[c_250,c_9269]) ).
cnf(c_9270,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| h3(e13) != op2(e22,e23)
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_7877,c_7831]) ).
cnf(c_9271,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| e23 != op2(e22,e23)
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_824,c_9270]) ).
cnf(c_7883,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(copy,[status(thm)],[c_9271]) ).
cnf(c_9272,plain,
( op1(e11,e12) != e12
| e13 = e12
| op1(e10,e13) = e12 ),
inference(paramod,[status(thm)],[c_7877,c_7471]) ).
cnf(c_7886,plain,
( op1(e11,e12) != e12
| op1(e10,e13) = e12 ),
inference(resolve,[status(thm)],[c_250,c_9272]) ).
cnf(c_7909,plain,
( op1(e10,e13) != e12
| op1(e11,e12) = e12 ),
inference(resolve,[status(thm)],[c_7878,c_2501]) ).
cnf(c_7978,plain,
( op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e10,e12) = e13 ),
inference(resolve,[status(thm)],[c_7859,c_2846]) ).
cnf(c_9273,plain,
( e11 = e10
| op1(e11,e11) = e10
| op1(e10,e12) = e13 ),
inference(paramod,[status(thm)],[c_7859,c_2184]) ).
cnf(c_7983,plain,
( op1(e11,e11) = e10
| op1(e10,e12) = e13 ),
inference(resolve,[status(thm)],[c_243,c_9273]) ).
cnf(c_8015,plain,
( op1(e11,e13) = e11
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_7881,c_7503]) ).
cnf(c_9274,plain,
( op1(e10,e13) = e12
| op1(e10,e13) = e12 ),
inference(resolve,[status(thm)],[c_7886,c_7818]) ).
cnf(c_8017,plain,
op1(e10,e13) = e12,
inference(copy,[status(thm)],[c_9274]) ).
cnf(c_9275,plain,
( e12 != e12
| op1(e11,e12) = e12 ),
inference(paramod,[status(thm)],[c_8017,c_7909]) ).
cnf(c_8026,plain,
op1(e11,e12) = e12,
inference(copy,[status(thm)],[c_9275]) ).
cnf(c_9276,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(e12) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_8017,c_7883]) ).
cnf(c_9277,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e22 != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_818,c_9276]) ).
cnf(c_9278,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e12) != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e22 != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_8026,c_9277]) ).
cnf(c_9279,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| e22 != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| e22 != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_818,c_9278]) ).
cnf(c_9280,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| e22 != op2(e21,e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| op2(e20,e23) != e22
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(copy,[status(thm)],[c_9279]) ).
cnf(c_8027,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != e22
| h3(op1(e11,e11)) != op2(e21,e21)
| op2(e20,e23) != e22
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(copy,[status(thm)],[c_9280]) ).
cnf(c_8034,plain,
op1(e13,e12) = e13,
inference(paramod,[status(thm)],[c_8017,c_7613]) ).
cnf(c_9281,plain,
( op1(e13,e12) = e11
| e12 = e11
| op1(e10,e12) = e11 ),
inference(paramod,[status(thm)],[c_8026,c_2170]) ).
cnf(c_9282,plain,
( e13 = e11
| e12 = e11
| op1(e10,e12) = e11 ),
inference(paramod,[status(thm)],[c_8034,c_9281]) ).
cnf(c_9283,plain,
( e13 = e11
| e11 = e12
| op1(e10,e12) = e11 ),
inference(copy,[status(thm)],[c_9282]) ).
cnf(c_9284,plain,
( e13 = e11
| op1(e10,e12) = e11 ),
inference(resolve,[status(thm)],[c_248,c_9283]) ).
cnf(c_8065,plain,
op1(e10,e12) = e11,
inference(resolve,[status(thm)],[c_249,c_9284]) ).
cnf(c_9285,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != e22
| h3(op1(e11,e11)) != op2(e21,e21)
| op2(e20,e23) != e22
| h3(e11) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_8065,c_8027]) ).
cnf(c_9286,plain,
( op2(e23,e23) != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != e22
| h3(op1(e11,e11)) != op2(e21,e21)
| op2(e20,e23) != e22
| e21 != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_822,c_9285]) ).
cnf(c_9287,plain,
( op2(e23,e23) != e20
| h3(e13) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != e22
| h3(op1(e11,e11)) != op2(e21,e21)
| op2(e20,e23) != e22
| e21 != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_8034,c_9286]) ).
cnf(c_9288,plain,
( op2(e23,e23) != e20
| e23 != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != e22
| h3(op1(e11,e11)) != op2(e21,e21)
| op2(e20,e23) != e22
| e21 != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(paramod,[status(thm)],[c_824,c_9287]) ).
cnf(c_9289,plain,
( op2(e23,e23) != e20
| e23 != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != e22
| h3(op1(e11,e11)) != op2(e21,e21)
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(copy,[status(thm)],[c_9288]) ).
cnf(c_8068,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != e22
| h3(op1(e11,e11)) != op2(e21,e21)
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| op1(e13,e11) = e10 ),
inference(copy,[status(thm)],[c_9289]) ).
cnf(c_9290,plain,
( op1(e13,e12) = e11
| op1(e13,e11) = e11
| e11 = e13 ),
inference(paramod,[status(thm)],[c_8065,c_7978]) ).
cnf(c_9291,plain,
( e13 = e11
| op1(e13,e11) = e11
| e11 = e13 ),
inference(paramod,[status(thm)],[c_8034,c_9290]) ).
cnf(c_9292,plain,
( e13 = e11
| op1(e13,e11) = e11
| e13 = e11 ),
inference(copy,[status(thm)],[c_9291]) ).
cnf(c_9293,plain,
( op1(e13,e11) = e11
| e13 = e11 ),
inference(copy,[status(thm)],[c_9292]) ).
cnf(c_8069,plain,
op1(e13,e11) = e11,
inference(resolve,[status(thm)],[c_249,c_9293]) ).
cnf(c_9294,plain,
( e13 != e13
| op1(e10,e11) = e13 ),
inference(paramod,[status(thm)],[c_8034,c_7873]) ).
cnf(c_8070,plain,
op1(e10,e11) = e13,
inference(copy,[status(thm)],[c_9294]) ).
cnf(c_9295,plain,
( op1(e11,e13) = e11
| e11 = e12 ),
inference(paramod,[status(thm)],[c_8065,c_8015]) ).
cnf(c_8073,plain,
op1(e11,e13) = e11,
inference(resolve,[status(thm)],[c_248,c_9295]) ).
cnf(c_9296,plain,
( op1(e11,e11) = e10
| e11 = e13 ),
inference(paramod,[status(thm)],[c_8065,c_7983]) ).
cnf(c_9297,plain,
( op1(e11,e11) = e10
| e13 = e11 ),
inference(copy,[status(thm)],[c_9296]) ).
cnf(c_8077,plain,
op1(e11,e11) = e10,
inference(resolve,[status(thm)],[c_249,c_9297]) ).
cnf(c_9298,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != e22
| h3(op1(e11,e11)) != op2(e21,e21)
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| h3(op1(e10,e11)) != op2(e20,e21)
| op2(e20,e20) != e20
| e11 = e10 ),
inference(paramod,[status(thm)],[c_8069,c_8068]) ).
cnf(c_9299,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != e22
| h3(op1(e11,e11)) != op2(e21,e21)
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| h3(e13) != op2(e20,e21)
| op2(e20,e20) != e20
| e11 = e10 ),
inference(paramod,[status(thm)],[c_8070,c_9298]) ).
cnf(c_9300,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != e22
| h3(op1(e11,e11)) != op2(e21,e21)
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| e23 != op2(e20,e21)
| op2(e20,e20) != e20
| e11 = e10 ),
inference(paramod,[status(thm)],[c_824,c_9299]) ).
cnf(c_9301,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != e22
| h3(e10) != op2(e21,e21)
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| e23 != op2(e20,e21)
| op2(e20,e20) != e20
| e11 = e10 ),
inference(paramod,[status(thm)],[c_8077,c_9300]) ).
cnf(c_9302,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(op1(e11,e13)) != op2(e21,e23)
| op2(e21,e22) != e22
| e20 != op2(e21,e21)
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| e23 != op2(e20,e21)
| op2(e20,e20) != e20
| e11 = e10 ),
inference(paramod,[status(thm)],[c_820,c_9301]) ).
cnf(c_9303,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| h3(e11) != op2(e21,e23)
| op2(e21,e22) != e22
| e20 != op2(e21,e21)
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| e23 != op2(e20,e21)
| op2(e20,e20) != e20
| e11 = e10 ),
inference(paramod,[status(thm)],[c_8073,c_9302]) ).
cnf(c_9304,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| h3(op1(e13,e11)) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| e21 != op2(e21,e23)
| op2(e21,e22) != e22
| e20 != op2(e21,e21)
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| e23 != op2(e20,e21)
| op2(e20,e20) != e20
| e11 = e10 ),
inference(paramod,[status(thm)],[c_822,c_9303]) ).
cnf(c_9305,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| h3(e11) != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| e21 != op2(e21,e23)
| op2(e21,e22) != e22
| e20 != op2(e21,e21)
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| e23 != op2(e20,e21)
| op2(e20,e20) != e20
| e11 = e10 ),
inference(paramod,[status(thm)],[c_8069,c_9304]) ).
cnf(c_9306,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| e21 != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| e21 != op2(e21,e23)
| op2(e21,e22) != e22
| e20 != op2(e21,e21)
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| e23 != op2(e20,e21)
| op2(e20,e20) != e20
| e11 = e10 ),
inference(paramod,[status(thm)],[c_822,c_9305]) ).
cnf(c_9307,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| e21 != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| e21 != op2(e21,e23)
| op2(e21,e22) != e22
| e20 != op2(e21,e21)
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23
| op2(e20,e20) != e20
| e11 = e10 ),
inference(copy,[status(thm)],[c_9306]) ).
cnf(c_9308,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| e21 != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| e21 != op2(e21,e23)
| op2(e21,e22) != e22
| op2(e21,e21) != e20
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23
| op2(e20,e20) != e20
| e11 = e10 ),
inference(copy,[status(thm)],[c_9307]) ).
cnf(c_9309,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| e21 != op2(e23,e21)
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| op2(e21,e23) != e21
| op2(e21,e22) != e22
| op2(e21,e21) != e20
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23
| op2(e20,e20) != e20
| e11 = e10 ),
inference(copy,[status(thm)],[c_9308]) ).
cnf(c_9310,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| op2(e21,e23) != e21
| op2(e21,e22) != e22
| op2(e21,e21) != e20
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23
| op2(e20,e20) != e20
| e11 = e10 ),
inference(copy,[status(thm)],[c_9309]) ).
cnf(c_8079,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| op2(e21,e23) != e21
| op2(e21,e22) != e22
| op2(e21,e21) != e20
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23
| op2(e20,e20) != e20 ),
inference(resolve,[status(thm)],[c_243,c_9310]) ).
cnf(c_9311,plain,
( op2(e20,e20) = e20
| op2(e21,op2(e21,e21)) = e21
| op2(e20,e21) = e20
| op2(e20,e20) = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_2264,c_3041]) ).
cnf(c_9312,plain,
( op2(e20,e20) = e20
| op2(e21,op2(e21,e21)) = e21
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_9311]) ).
cnf(c_8252,plain,
( op2(e21,op2(e21,e21)) = e21
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_9312]) ).
cnf(c_9313,plain,
( op2(e21,e20) = e21
| op2(e20,e21) = e20
| op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_3239,c_8252]) ).
cnf(c_9314,plain,
( e23 = e21
| op2(e20,e21) = e20
| op2(e20,e20) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_809,c_9313]) ).
cnf(c_9315,plain,
( e23 = e21
| op2(e20,e21) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_9314]) ).
cnf(c_9316,plain,
( e23 = e21
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_9315]) ).
cnf(c_8314,plain,
( op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_257,c_9316]) ).
cnf(c_8317,plain,
( op2(e20,e23) != e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_8314,c_217]) ).
cnf(c_9317,plain,
( op2(e20,e23) = e20
| op2(e21,e20) = e21
| op2(e20,e20) = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_8314,c_2677]) ).
cnf(c_9318,plain,
( op2(e20,e23) = e20
| e23 = e21
| op2(e20,e20) = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_809,c_9317]) ).
cnf(c_9319,plain,
( op2(e20,e23) = e20
| e23 = e21
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_9318]) ).
cnf(c_8320,plain,
( op2(e20,e23) = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_257,c_9319]) ).
cnf(c_9320,plain,
( op2(e20,e20) = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_8320,c_8317]) ).
cnf(c_8336,plain,
op2(e20,e20) = e20,
inference(copy,[status(thm)],[c_9320]) ).
cnf(c_9321,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| op2(e21,e23) != e21
| op2(e21,e22) != e22
| op2(e21,e21) != e20
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23
| e20 != e20 ),
inference(paramod,[status(thm)],[c_8336,c_8079]) ).
cnf(c_8346,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| op2(e23,e20) != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| op2(e21,e23) != e21
| op2(e21,e22) != e22
| op2(e21,e21) != e20
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23 ),
inference(copy,[status(thm)],[c_9321]) ).
cnf(c_9322,plain,
( op2(e21,e22) != e22
| op2(e22,e23) = e22
| op2(e20,e23) = e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_8336,c_4800]) ).
cnf(c_8423,plain,
( op2(e21,e22) != e22
| op2(e22,e23) = e22
| op2(e20,e23) = e22 ),
inference(resolve,[status(thm)],[c_253,c_9322]) ).
cnf(c_9323,plain,
( op2(e20,e23) = e20
| op2(e21,e23) = e21
| e20 = e22
| op2(e20,e22) = e23
| op2(e22,e21) = e23 ),
inference(paramod,[status(thm)],[c_8336,c_3742]) ).
cnf(c_8440,plain,
( op2(e20,e23) = e20
| op2(e21,e23) = e21
| op2(e20,e22) = e23
| op2(e22,e21) = e23 ),
inference(resolve,[status(thm)],[c_253,c_9323]) ).
cnf(c_9324,plain,
( op2(e20,e23) != e20
| e20 = e22 ),
inference(paramod,[status(thm)],[c_8336,c_3126]) ).
cnf(c_8448,plain,
op2(e20,e23) != e20,
inference(resolve,[status(thm)],[c_253,c_9324]) ).
cnf(c_9325,plain,
( e20 != e20
| op2(e23,e20) = e22 ),
inference(paramod,[status(thm)],[c_8336,c_3108]) ).
cnf(c_8452,plain,
op2(e23,e20) = e22,
inference(copy,[status(thm)],[c_9325]) ).
cnf(c_9326,plain,
( op2(e20,e23) = e20
| op2(e21,op2(e20,e21)) = e21
| e20 = e22 ),
inference(paramod,[status(thm)],[c_8336,c_2666]) ).
cnf(c_9327,plain,
( op2(e20,e23) = e20
| op2(e21,op2(e20,e21)) = e21 ),
inference(resolve,[status(thm)],[c_253,c_9326]) ).
cnf(c_8453,plain,
op2(e21,op2(e20,e21)) = e21,
inference(resolve,[status(thm)],[c_8448,c_9327]) ).
cnf(c_9328,plain,
( op2(e23,e23) != e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_8336,c_2660]) ).
cnf(c_8454,plain,
op2(e23,e23) != e22,
inference(resolve,[status(thm)],[c_253,c_9328]) ).
cnf(c_9329,plain,
( op2(e23,e22) != e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_8336,c_2659]) ).
cnf(c_8455,plain,
op2(e23,e22) != e22,
inference(resolve,[status(thm)],[c_253,c_9329]) ).
cnf(c_8463,plain,
( op2(e21,e23) = e21
| op2(e20,e22) = e23
| op2(e22,e21) = e23 ),
inference(resolve,[status(thm)],[c_8448,c_8440]) ).
cnf(c_9330,plain,
( op2(e20,e22) = e20
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 ),
inference(paramod,[status(thm)],[c_8452,c_5971]) ).
cnf(c_9331,plain,
( op2(e20,e22) = e20
| op2(e20,e23) = e22
| op2(e20,e23) = e21 ),
inference(resolve,[status(thm)],[c_8448,c_9330]) ).
cnf(c_8512,plain,
( op2(e20,e23) = e22
| op2(e20,e23) = e21 ),
inference(resolve,[status(thm)],[c_2253,c_9331]) ).
cnf(c_9332,plain,
( op2(e20,e22) = e20
| op2(e20,e23) = e20
| op2(e23,op2(e20,e23)) = e23 ),
inference(paramod,[status(thm)],[c_8452,c_2200]) ).
cnf(c_9333,plain,
( op2(e20,e22) = e20
| op2(e23,op2(e20,e23)) = e23 ),
inference(resolve,[status(thm)],[c_8448,c_9332]) ).
cnf(c_8597,plain,
op2(e23,op2(e20,e23)) = e23,
inference(resolve,[status(thm)],[c_2253,c_9333]) ).
cnf(c_9334,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| e22 != e22
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| op2(e21,e23) != e21
| op2(e21,e22) != e22
| op2(e21,e21) != e20
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23 ),
inference(paramod,[status(thm)],[c_8452,c_8346]) ).
cnf(c_8683,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| op2(e22,e23) != e23
| op2(e22,e21) != e22
| op2(e21,e23) != e21
| op2(e21,e22) != e22
| op2(e21,e21) != e20
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23 ),
inference(copy,[status(thm)],[c_9334]) ).
cnf(c_8712,plain,
( op2(e21,e23) != e21
| op2(e23,e23) = e20
| op2(e22,e21) = e23 ),
inference(resolve,[status(thm)],[c_8454,c_4755]) ).
cnf(c_8749,plain,
( op2(e22,e23) = e22
| op2(e20,e22) = e22
| op2(e22,e21) = e23
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_8455,c_5200]) ).
cnf(c_8758,plain,
( op2(e23,e21) != e23
| op2(e23,e22) = e21 ),
inference(resolve,[status(thm)],[c_8455,c_3020]) ).
cnf(c_8790,plain,
( op2(e23,e21) = e23
| op2(e20,e23) = e22 ),
inference(paramod,[status(thm)],[c_8512,c_8597]) ).
cnf(c_8801,plain,
( op2(e23,e22) = e21
| op2(e20,e23) = e22 ),
inference(resolve,[status(thm)],[c_8790,c_8758]) ).
cnf(c_8805,plain,
( op2(e22,e21) = e22
| op2(e20,e23) = e22 ),
inference(resolve,[status(thm)],[c_8790,c_2995]) ).
cnf(c_8814,plain,
( op2(e21,e22) = e22
| op2(e20,e23) = e22 ),
inference(resolve,[status(thm)],[c_8801,c_3032]) ).
cnf(c_9335,plain,
( op2(e22,e21) = e22
| op2(e22,e21) = e22 ),
inference(resolve,[status(thm)],[c_8805,c_2644]) ).
cnf(c_8826,plain,
op2(e22,e21) = e22,
inference(copy,[status(thm)],[c_9335]) ).
cnf(c_9336,plain,
( op2(e22,e23) = e22
| op2(e20,e22) = e22
| e22 = e23
| op2(e20,e21) = e23 ),
inference(paramod,[status(thm)],[c_8826,c_8749]) ).
cnf(c_9337,plain,
( op2(e22,e23) = e22
| op2(e20,e22) = e22
| e23 = e22
| op2(e20,e21) = e23 ),
inference(copy,[status(thm)],[c_9336]) ).
cnf(c_8828,plain,
( op2(e22,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_258,c_9337]) ).
cnf(c_9338,plain,
( op2(e21,e23) != e21
| op2(e23,e23) = e20
| e22 = e23 ),
inference(paramod,[status(thm)],[c_8826,c_8712]) ).
cnf(c_9339,plain,
( op2(e21,e23) != e21
| op2(e23,e23) = e20
| e23 = e22 ),
inference(copy,[status(thm)],[c_9338]) ).
cnf(c_8839,plain,
( op2(e21,e23) != e21
| op2(e23,e23) = e20 ),
inference(resolve,[status(thm)],[c_258,c_9339]) ).
cnf(c_9340,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| op2(e22,e23) != e23
| e22 != e22
| op2(e21,e23) != e21
| op2(e21,e22) != e22
| op2(e21,e21) != e20
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23 ),
inference(paramod,[status(thm)],[c_8826,c_8683]) ).
cnf(c_8847,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| op2(e22,e23) != e23
| op2(e21,e23) != e21
| op2(e21,e22) != e22
| op2(e21,e21) != e20
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23 ),
inference(copy,[status(thm)],[c_9340]) ).
cnf(c_9341,plain,
( op2(e21,e23) = e21
| op2(e20,e22) = e23
| e22 = e23 ),
inference(paramod,[status(thm)],[c_8826,c_8463]) ).
cnf(c_9342,plain,
( op2(e21,e23) = e21
| op2(e20,e22) = e23
| e23 = e22 ),
inference(copy,[status(thm)],[c_9341]) ).
cnf(c_8859,plain,
( op2(e21,e23) = e21
| op2(e20,e22) = e23 ),
inference(resolve,[status(thm)],[c_258,c_9342]) ).
cnf(c_9343,plain,
( op2(e23,e22) != e23
| e22 = e23
| op2(e20,e21) = e23 ),
inference(paramod,[status(thm)],[c_8826,c_3169]) ).
cnf(c_9344,plain,
( op2(e23,e22) != e23
| e23 = e22
| op2(e20,e21) = e23 ),
inference(copy,[status(thm)],[c_9343]) ).
cnf(c_8875,plain,
( op2(e23,e22) != e23
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_258,c_9344]) ).
cnf(c_9345,plain,
( op2(e22,e23) = e23
| e22 = e23 ),
inference(paramod,[status(thm)],[c_8826,c_2255]) ).
cnf(c_9346,plain,
( op2(e22,e23) = e23
| e23 = e22 ),
inference(copy,[status(thm)],[c_9345]) ).
cnf(c_8879,plain,
op2(e22,e23) = e23,
inference(resolve,[status(thm)],[c_258,c_9346]) ).
cnf(c_8880,plain,
op2(e21,e21) != e22,
inference(paramod,[status(thm)],[c_8826,c_192]) ).
cnf(c_9347,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| e23 != e23
| op2(e21,e23) != e21
| op2(e21,e22) != e22
| op2(e21,e21) != e20
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23 ),
inference(paramod,[status(thm)],[c_8879,c_8847]) ).
cnf(c_8884,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| op2(e21,e23) != e21
| op2(e21,e22) != e22
| op2(e21,e21) != e20
| op2(e20,e23) != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23 ),
inference(copy,[status(thm)],[c_9347]) ).
cnf(c_9348,plain,
( e23 = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e23 ),
inference(paramod,[status(thm)],[c_8879,c_8828]) ).
cnf(c_8885,plain,
( op2(e20,e22) = e22
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_258,c_9348]) ).
cnf(c_9349,plain,
( op2(e21,e22) != e22
| e23 = e22
| op2(e20,e23) = e22 ),
inference(paramod,[status(thm)],[c_8879,c_8423]) ).
cnf(c_8888,plain,
( op2(e21,e22) != e22
| op2(e20,e23) = e22 ),
inference(resolve,[status(thm)],[c_258,c_9349]) ).
cnf(c_8930,plain,
( op2(e20,e23) != e22
| op2(e21,e22) = e22 ),
inference(resolve,[status(thm)],[c_8880,c_2681]) ).
cnf(c_8956,plain,
( op2(e23,e23) = e20
| op2(e20,e22) = e23 ),
inference(resolve,[status(thm)],[c_8859,c_8839]) ).
cnf(c_8958,plain,
( op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e20,e22) = e23 ),
inference(resolve,[status(thm)],[c_8859,c_3086]) ).
cnf(c_9350,plain,
( e21 = e20
| op2(e21,e21) = e20
| op2(e20,e22) = e23 ),
inference(paramod,[status(thm)],[c_8859,c_2272]) ).
cnf(c_8963,plain,
( op2(e21,e21) = e20
| op2(e20,e22) = e23 ),
inference(resolve,[status(thm)],[c_251,c_9350]) ).
cnf(c_8976,plain,
( op2(e21,e23) = e21
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_8885,c_8453]) ).
cnf(c_9351,plain,
( op2(e20,e23) = e22
| op2(e20,e23) = e22 ),
inference(resolve,[status(thm)],[c_8888,c_8814]) ).
cnf(c_8980,plain,
op2(e20,e23) = e22,
inference(copy,[status(thm)],[c_9351]) ).
cnf(c_9352,plain,
( e22 != e22
| op2(e21,e22) = e22 ),
inference(paramod,[status(thm)],[c_8980,c_8930]) ).
cnf(c_8989,plain,
op2(e21,e22) = e22,
inference(copy,[status(thm)],[c_9352]) ).
cnf(c_9353,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| op2(e21,e23) != e21
| op2(e21,e22) != e22
| op2(e21,e21) != e20
| e22 != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23 ),
inference(paramod,[status(thm)],[c_8980,c_8884]) ).
cnf(c_9354,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| op2(e21,e23) != e21
| e22 != e22
| op2(e21,e21) != e20
| e22 != e22
| op2(e20,e22) != e21
| op2(e20,e21) != e23 ),
inference(paramod,[status(thm)],[c_8989,c_9353]) ).
cnf(c_9355,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| op2(e21,e23) != e21
| e22 != e22
| op2(e21,e21) != e20
| op2(e20,e22) != e21
| op2(e20,e21) != e23 ),
inference(copy,[status(thm)],[c_9354]) ).
cnf(c_8990,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| op2(e21,e23) != e21
| op2(e21,e21) != e20
| op2(e20,e22) != e21
| op2(e20,e21) != e23 ),
inference(copy,[status(thm)],[c_9355]) ).
cnf(c_8999,plain,
op2(e23,e22) = e23,
inference(paramod,[status(thm)],[c_8980,c_8597]) ).
cnf(c_9356,plain,
( op2(e23,e22) = e21
| e22 = e21
| op2(e20,e22) = e21 ),
inference(paramod,[status(thm)],[c_8989,c_2258]) ).
cnf(c_9357,plain,
( e23 = e21
| e22 = e21
| op2(e20,e22) = e21 ),
inference(paramod,[status(thm)],[c_8999,c_9356]) ).
cnf(c_9358,plain,
( e23 = e21
| e21 = e22
| op2(e20,e22) = e21 ),
inference(copy,[status(thm)],[c_9357]) ).
cnf(c_9359,plain,
( e23 = e21
| op2(e20,e22) = e21 ),
inference(resolve,[status(thm)],[c_256,c_9358]) ).
cnf(c_9032,plain,
op2(e20,e22) = e21,
inference(resolve,[status(thm)],[c_257,c_9359]) ).
cnf(c_9360,plain,
( op2(e23,e23) != e20
| op2(e23,e22) != e23
| op2(e23,e21) != e21
| op2(e21,e23) != e21
| op2(e21,e21) != e20
| e21 != e21
| op2(e20,e21) != e23 ),
inference(paramod,[status(thm)],[c_9032,c_8990]) ).
cnf(c_9361,plain,
( op2(e23,e23) != e20
| e23 != e23
| op2(e23,e21) != e21
| op2(e21,e23) != e21
| op2(e21,e21) != e20
| e21 != e21
| op2(e20,e21) != e23 ),
inference(paramod,[status(thm)],[c_8999,c_9360]) ).
cnf(c_9362,plain,
( op2(e23,e23) != e20
| e23 != e23
| op2(e23,e21) != e21
| op2(e21,e23) != e21
| op2(e21,e21) != e20
| op2(e20,e21) != e23 ),
inference(copy,[status(thm)],[c_9361]) ).
cnf(c_9035,plain,
( op2(e23,e23) != e20
| op2(e23,e21) != e21
| op2(e21,e23) != e21
| op2(e21,e21) != e20
| op2(e20,e21) != e23 ),
inference(copy,[status(thm)],[c_9362]) ).
cnf(c_9363,plain,
( op2(e23,e22) = e21
| op2(e23,e21) = e21
| e21 = e23 ),
inference(paramod,[status(thm)],[c_9032,c_8958]) ).
cnf(c_9364,plain,
( e23 = e21
| op2(e23,e21) = e21
| e21 = e23 ),
inference(paramod,[status(thm)],[c_8999,c_9363]) ).
cnf(c_9365,plain,
( e23 = e21
| op2(e23,e21) = e21
| e23 = e21 ),
inference(copy,[status(thm)],[c_9364]) ).
cnf(c_9366,plain,
( op2(e23,e21) = e21
| e23 = e21 ),
inference(copy,[status(thm)],[c_9365]) ).
cnf(c_9036,plain,
op2(e23,e21) = e21,
inference(resolve,[status(thm)],[c_257,c_9366]) ).
cnf(c_9367,plain,
( e23 != e23
| op2(e20,e21) = e23 ),
inference(paramod,[status(thm)],[c_8999,c_8875]) ).
cnf(c_9037,plain,
op2(e20,e21) = e23,
inference(copy,[status(thm)],[c_9367]) ).
cnf(c_9368,plain,
( op2(e21,e23) = e21
| e21 = e22 ),
inference(paramod,[status(thm)],[c_9032,c_8976]) ).
cnf(c_9040,plain,
op2(e21,e23) = e21,
inference(resolve,[status(thm)],[c_256,c_9368]) ).
cnf(c_9369,plain,
( op2(e21,e21) = e20
| e21 = e23 ),
inference(paramod,[status(thm)],[c_9032,c_8963]) ).
cnf(c_9370,plain,
( op2(e21,e21) = e20
| e23 = e21 ),
inference(copy,[status(thm)],[c_9369]) ).
cnf(c_9041,plain,
op2(e21,e21) = e20,
inference(resolve,[status(thm)],[c_257,c_9370]) ).
cnf(c_9371,plain,
( op2(e23,e23) = e20
| e21 = e23 ),
inference(paramod,[status(thm)],[c_9032,c_8956]) ).
cnf(c_9372,plain,
( op2(e23,e23) = e20
| e23 = e21 ),
inference(copy,[status(thm)],[c_9371]) ).
cnf(c_9042,plain,
op2(e23,e23) = e20,
inference(resolve,[status(thm)],[c_257,c_9372]) ).
cnf(c_9373,plain,
( op2(e23,e23) != e20
| op2(e23,e21) != e21
| op2(e21,e23) != e21
| op2(e21,e21) != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_9037,c_9035]) ).
cnf(c_9374,plain,
( op2(e23,e23) != e20
| op2(e23,e21) != e21
| op2(e21,e23) != e21
| e20 != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_9041,c_9373]) ).
cnf(c_9375,plain,
( op2(e23,e23) != e20
| op2(e23,e21) != e21
| e21 != e21
| e20 != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_9040,c_9374]) ).
cnf(c_9376,plain,
( op2(e23,e23) != e20
| e21 != e21
| e21 != e21
| e20 != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_9036,c_9375]) ).
cnf(c_9377,plain,
( e20 != e20
| e21 != e21
| e21 != e21
| e20 != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_9042,c_9376]) ).
cnf(c_9378,plain,
( e20 != e20
| e21 != e21
| e21 != e21
| e20 != e20 ),
inference(copy,[status(thm)],[c_9377]) ).
cnf(c_9379,plain,
( e20 != e20
| e21 != e21
| e21 != e21 ),
inference(copy,[status(thm)],[c_9378]) ).
cnf(c_9380,plain,
( e20 != e20
| e21 != e21 ),
inference(copy,[status(thm)],[c_9379]) ).
cnf(c_9381,plain,
e20 != e20,
inference(copy,[status(thm)],[c_9380]) ).
cnf(c_9043,plain,
$false,
inference(copy,[status(thm)],[c_9381]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG107+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n006.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 21:09:30 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 2115641 was started by sandbox on n006,
% 0.09/0.36 % Sat Sep 26 21:09:30 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 11.24/11.52
% 11.24/11.52 % From the command line: assign(max_seconds, 300).
% 67.80/19.83
% 67.80/19.83 % given #500 (T,wt=15): 2632 op2(e20,e22) = e22 | op2(e21,e22) = e22 | op2(e23,e20) != e22. [para(2256(c,1),237(a,2))].
% 67.80/19.83
% 67.80/19.83 % given #1000 (T,wt=20): 3259 op2(e22,e21) = e22 | op2(e20,e21) = e20 | op2(e20,e21) = e21 | op2(e20,e21) = e22. [resolve(2994,b,68,d)].
% 67.80/19.83
% 67.80/19.83 % given #1500 (T,wt=20): 5226 op2(e20,e23) = e21 | op2(e20,e21) = e21 | op2(e21,e21) = e21 | op2(e21,e22) != e21. [para(3328(b,1),226(a,1)),flip(d)].
% 67.80/19.83
% 67.80/19.83 % SZS status Theorem for theBenchmark
% 67.80/19.83
% 67.80/19.83 % Proof 1 at 7.38 (+ 0.86) seconds.
% 67.80/19.83 % Length of proof is 418.
% 67.80/19.83 % Level of proof is 28.
% 67.80/19.83 % Maximum clause weight is 104.000.
% 67.80/19.83 % Given clauses 1953.
% 67.80/19.83
% 67.80/19.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------