%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG115+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:49:32 AM UTC 2026
% Result : Theorem 20.11s 16.04s
% Output : CNFRefutation 20.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 123
% Number of leaves : 14
% Syntax : Number of formulae : 420 ( 121 unt; 0 def)
% Number of atoms : 3655 (3654 equ)
% Maximal formula atoms : 288 ( 8 avg)
% Number of connectives : 5119 (1884 ~;2462 |; 773 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 72 ( 7 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,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e13) = e13 )
| ( op1(e13,e12) = e13
& op1(e12,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e13) = e13 )
| ( op1(e13,e11) = e13
& op1(e11,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e13) = e13 )
| ( op1(e13,e10) = e13
& op1(e10,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e13) = e13 )
| ( op1(e12,e13) = e12
& op1(e13,e12) = e12
& op1(e12,e13) = e13
& op1(e13,e12) = e13 )
| ( op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e13) = e13
& op1(e13,e12) = e13 )
| ( op1(e12,e11) = e12
& op1(e11,e12) = e12
& op1(e12,e13) = e13
& op1(e13,e12) = e13 )
| ( op1(e12,e10) = e12
& op1(e10,e12) = e12
& op1(e12,e13) = e13
& op1(e13,e12) = e13 )
| ( op1(e11,e13) = e11
& op1(e13,e11) = e11
& op1(e11,e13) = e13
& op1(e13,e11) = e13 )
| ( op1(e11,e12) = e11
& op1(e12,e11) = e11
& op1(e11,e13) = e13
& op1(e13,e11) = e13 )
| ( op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e13) = e13
& op1(e13,e11) = e13 )
| ( op1(e11,e10) = e11
& op1(e10,e11) = e11
& op1(e11,e13) = e13
& op1(e13,e11) = e13 )
| ( op1(e10,e13) = e10
& op1(e13,e10) = e10
& op1(e10,e13) = e13
& op1(e13,e10) = e13 )
| ( op1(e10,e12) = e10
& op1(e12,e10) = e10
& op1(e10,e13) = e13
& op1(e13,e10) = e13 )
| ( op1(e10,e11) = e10
& op1(e11,e10) = e10
& op1(e10,e13) = e13
& op1(e13,e10) = e13 )
| ( op1(e10,e10) = e10
& op1(e10,e10) = e10
& op1(e10,e13) = e13
& op1(e13,e10) = e13 )
| ( op1(e13,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e12) = e12
& op1(e12,e13) = e12 )
| ( op1(e13,e12) = e13
& op1(e12,e13) = e13
& op1(e13,e12) = e12
& op1(e12,e13) = e12 )
| ( op1(e13,e11) = e13
& op1(e11,e13) = e13
& op1(e13,e12) = e12
& op1(e12,e13) = e12 )
| ( op1(e13,e10) = e13
& op1(e10,e13) = e13
& op1(e13,e12) = e12
& op1(e12,e13) = e12 )
| ( op1(e12,e13) = e12
& op1(e13,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e12) = e12 )
| ( op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e12) = e12 )
| ( op1(e12,e11) = e12
& op1(e11,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e12) = e12 )
| ( op1(e12,e10) = e12
& op1(e10,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e12) = e12 )
| ( op1(e11,e13) = e11
& op1(e13,e11) = e11
& op1(e11,e12) = e12
& op1(e12,e11) = e12 )
| ( op1(e11,e12) = e11
& op1(e12,e11) = e11
& op1(e11,e12) = e12
& op1(e12,e11) = e12 )
| ( op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e12) = e12
& op1(e12,e11) = e12 )
| ( op1(e11,e10) = e11
& op1(e10,e11) = e11
& op1(e11,e12) = e12
& op1(e12,e11) = e12 )
| ( op1(e10,e13) = e10
& op1(e13,e10) = e10
& op1(e10,e12) = e12
& op1(e12,e10) = e12 )
| ( op1(e10,e12) = e10
& op1(e12,e10) = e10
& op1(e10,e12) = e12
& op1(e12,e10) = e12 )
| ( op1(e10,e11) = e10
& op1(e11,e10) = e10
& op1(e10,e12) = e12
& op1(e12,e10) = e12 )
| ( op1(e10,e10) = e10
& op1(e10,e10) = e10
& op1(e10,e12) = e12
& op1(e12,e10) = e12 )
| ( op1(e13,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e11) = e11
& op1(e11,e13) = e11 )
| ( op1(e13,e12) = e13
& op1(e12,e13) = e13
& op1(e13,e11) = e11
& op1(e11,e13) = e11 )
| ( op1(e13,e11) = e13
& op1(e11,e13) = e13
& op1(e13,e11) = e11
& op1(e11,e13) = e11 )
| ( op1(e13,e10) = e13
& op1(e10,e13) = e13
& op1(e13,e11) = e11
& op1(e11,e13) = e11 )
| ( op1(e12,e13) = e12
& op1(e13,e12) = e12
& op1(e12,e11) = e11
& op1(e11,e12) = e11 )
| ( op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e11) = e11
& op1(e11,e12) = e11 )
| ( op1(e12,e11) = e12
& op1(e11,e12) = e12
& op1(e12,e11) = e11
& op1(e11,e12) = e11 )
| ( op1(e12,e10) = e12
& op1(e10,e12) = e12
& op1(e12,e11) = e11
& op1(e11,e12) = e11 )
| ( op1(e11,e13) = e11
& op1(e13,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e11) = e11 )
| ( op1(e11,e12) = e11
& op1(e12,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e11) = e11 )
| ( op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e11) = e11 )
| ( op1(e11,e10) = e11
& op1(e10,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e11) = e11 )
| ( op1(e10,e13) = e10
& op1(e13,e10) = e10
& op1(e10,e11) = e11
& op1(e11,e10) = e11 )
| ( op1(e10,e12) = e10
& op1(e12,e10) = e10
& op1(e10,e11) = e11
& op1(e11,e10) = e11 )
| ( op1(e10,e11) = e10
& op1(e11,e10) = e10
& op1(e10,e11) = e11
& op1(e11,e10) = e11 )
| ( op1(e10,e10) = e10
& op1(e10,e10) = e10
& op1(e10,e11) = e11
& op1(e11,e10) = e11 )
| ( op1(e13,e13) = e13
& op1(e13,e13) = e13
& op1(e13,e10) = e10
& op1(e10,e13) = e10 )
| ( op1(e13,e12) = e13
& op1(e12,e13) = e13
& op1(e13,e10) = e10
& op1(e10,e13) = e10 )
| ( op1(e13,e11) = e13
& op1(e11,e13) = e13
& op1(e13,e10) = e10
& op1(e10,e13) = e10 )
| ( op1(e13,e10) = e13
& op1(e10,e13) = e13
& op1(e13,e10) = e10
& op1(e10,e13) = e10 )
| ( op1(e12,e13) = e12
& op1(e13,e12) = e12
& op1(e12,e10) = e10
& op1(e10,e12) = e10 )
| ( op1(e12,e12) = e12
& op1(e12,e12) = e12
& op1(e12,e10) = e10
& op1(e10,e12) = e10 )
| ( op1(e12,e11) = e12
& op1(e11,e12) = e12
& op1(e12,e10) = e10
& op1(e10,e12) = e10 )
| ( op1(e12,e10) = e12
& op1(e10,e12) = e12
& op1(e12,e10) = e10
& op1(e10,e12) = e10 )
| ( op1(e11,e13) = e11
& op1(e13,e11) = e11
& op1(e11,e10) = e10
& op1(e10,e11) = e10 )
| ( op1(e11,e12) = e11
& op1(e12,e11) = e11
& op1(e11,e10) = e10
& op1(e10,e11) = e10 )
| ( op1(e11,e11) = e11
& op1(e11,e11) = e11
& op1(e11,e10) = e10
& op1(e10,e11) = e10 )
| ( op1(e11,e10) = e11
& op1(e10,e11) = e11
& op1(e11,e10) = e10
& op1(e10,e11) = e10 )
| ( op1(e10,e13) = e10
& op1(e13,e10) = e10
& op1(e10,e10) = e10
& op1(e10,e10) = e10 )
| ( op1(e10,e12) = e10
& op1(e12,e10) = e10
& op1(e10,e10) = e10
& op1(e10,e10) = e10 )
| ( op1(e10,e11) = e10
& op1(e11,e10) = e10
& op1(e10,e10) = e10
& op1(e10,e10) = e10 )
| ( op1(e10,e10) = e10
& op1(e10,e10) = e10
& op1(e10,e10) = e10
& op1(e10,e10) = e10 ) )
& ( ( op1(e13,op1(e13,e13)) != e13
& op1(e13,op1(e13,e12)) != e12
& op1(e13,op1(e13,e11)) != e11
& op1(e13,op1(e13,e10)) != e10 )
| ( op1(e12,op1(e12,e13)) != e13
& op1(e12,op1(e12,e12)) != e12
& op1(e12,op1(e12,e11)) != e11
& op1(e12,op1(e12,e10)) != e10 )
| ( op1(e11,op1(e11,e13)) != e13
& op1(e11,op1(e11,e12)) != e12
& op1(e11,op1(e11,e11)) != e11
& op1(e11,op1(e11,e10)) != e10 )
| ( op1(e10,op1(e10,e13)) != e13
& op1(e10,op1(e10,e12)) != e12
& op1(e10,op1(e10,e11)) != e11
& op1(e10,op1(e10,e10)) != e10 ) )
& ( op1(e13,e13) = e13
| op1(e12,e12) = e13
| op1(e11,e11) = e13
| op1(e10,e10) = e13 )
& ( op1(e13,e13) = e12
| op1(e12,e12) = e12
| op1(e11,e11) = e12
| op1(e10,e10) = e12 )
& ( op1(e13,e13) = e11
| op1(e12,e12) = e11
| op1(e11,e11) = e11
| op1(e10,e10) = e11 )
& ( op1(e13,e13) = e10
| op1(e12,e12) = e10
| op1(e11,e11) = e10
| op1(e10,e10) = e10 ) ),
file('theBenchmark.p',ax10) ).
fof(ax11,axiom,
( ( ( op2(e23,e23) = e23
& op2(e23,e23) = e23
& op2(e23,e23) = e23
& op2(e23,e23) = e23 )
| ( op2(e23,e22) = e23
& op2(e22,e23) = e23
& op2(e23,e23) = e23
& op2(e23,e23) = e23 )
| ( op2(e23,e21) = e23
& op2(e21,e23) = e23
& op2(e23,e23) = e23
& op2(e23,e23) = e23 )
| ( op2(e23,e20) = e23
& op2(e20,e23) = e23
& op2(e23,e23) = e23
& op2(e23,e23) = e23 )
| ( op2(e22,e23) = e22
& op2(e23,e22) = e22
& op2(e22,e23) = e23
& op2(e23,e22) = e23 )
| ( op2(e22,e22) = e22
& op2(e22,e22) = e22
& op2(e22,e23) = e23
& op2(e23,e22) = e23 )
| ( op2(e22,e21) = e22
& op2(e21,e22) = e22
& op2(e22,e23) = e23
& op2(e23,e22) = e23 )
| ( op2(e22,e20) = e22
& op2(e20,e22) = e22
& op2(e22,e23) = e23
& op2(e23,e22) = e23 )
| ( op2(e21,e23) = e21
& op2(e23,e21) = e21
& op2(e21,e23) = e23
& op2(e23,e21) = e23 )
| ( op2(e21,e22) = e21
& op2(e22,e21) = e21
& op2(e21,e23) = e23
& op2(e23,e21) = e23 )
| ( op2(e21,e21) = e21
& op2(e21,e21) = e21
& op2(e21,e23) = e23
& op2(e23,e21) = e23 )
| ( op2(e21,e20) = e21
& op2(e20,e21) = e21
& op2(e21,e23) = e23
& op2(e23,e21) = e23 )
| ( op2(e20,e23) = e20
& op2(e23,e20) = e20
& op2(e20,e23) = e23
& op2(e23,e20) = e23 )
| ( op2(e20,e22) = e20
& op2(e22,e20) = e20
& op2(e20,e23) = e23
& op2(e23,e20) = e23 )
| ( op2(e20,e21) = e20
& op2(e21,e20) = e20
& op2(e20,e23) = e23
& op2(e23,e20) = e23 )
| ( op2(e20,e20) = e20
& op2(e20,e20) = e20
& op2(e20,e23) = e23
& op2(e23,e20) = e23 )
| ( op2(e23,e23) = e23
& op2(e23,e23) = e23
& op2(e23,e22) = e22
& op2(e22,e23) = e22 )
| ( op2(e23,e22) = e23
& op2(e22,e23) = e23
& op2(e23,e22) = e22
& op2(e22,e23) = e22 )
| ( op2(e23,e21) = e23
& op2(e21,e23) = e23
& op2(e23,e22) = e22
& op2(e22,e23) = e22 )
| ( op2(e23,e20) = e23
& op2(e20,e23) = e23
& op2(e23,e22) = e22
& op2(e22,e23) = e22 )
| ( op2(e22,e23) = e22
& op2(e23,e22) = e22
& op2(e22,e22) = e22
& op2(e22,e22) = e22 )
| ( op2(e22,e22) = e22
& op2(e22,e22) = e22
& op2(e22,e22) = e22
& op2(e22,e22) = e22 )
| ( op2(e22,e21) = e22
& op2(e21,e22) = e22
& op2(e22,e22) = e22
& op2(e22,e22) = e22 )
| ( op2(e22,e20) = e22
& op2(e20,e22) = e22
& op2(e22,e22) = e22
& op2(e22,e22) = e22 )
| ( op2(e21,e23) = e21
& op2(e23,e21) = e21
& op2(e21,e22) = e22
& op2(e22,e21) = e22 )
| ( op2(e21,e22) = e21
& op2(e22,e21) = e21
& op2(e21,e22) = e22
& op2(e22,e21) = e22 )
| ( op2(e21,e21) = e21
& op2(e21,e21) = e21
& op2(e21,e22) = e22
& op2(e22,e21) = e22 )
| ( op2(e21,e20) = e21
& op2(e20,e21) = e21
& op2(e21,e22) = e22
& op2(e22,e21) = e22 )
| ( op2(e20,e23) = e20
& op2(e23,e20) = e20
& op2(e20,e22) = e22
& op2(e22,e20) = e22 )
| ( op2(e20,e22) = e20
& op2(e22,e20) = e20
& op2(e20,e22) = e22
& op2(e22,e20) = e22 )
| ( op2(e20,e21) = e20
& op2(e21,e20) = e20
& op2(e20,e22) = e22
& op2(e22,e20) = e22 )
| ( op2(e20,e20) = e20
& op2(e20,e20) = e20
& op2(e20,e22) = e22
& op2(e22,e20) = e22 )
| ( op2(e23,e23) = e23
& op2(e23,e23) = e23
& op2(e23,e21) = e21
& op2(e21,e23) = e21 )
| ( op2(e23,e22) = e23
& op2(e22,e23) = e23
& op2(e23,e21) = e21
& op2(e21,e23) = e21 )
| ( op2(e23,e21) = e23
& op2(e21,e23) = e23
& op2(e23,e21) = e21
& op2(e21,e23) = e21 )
| ( op2(e23,e20) = e23
& op2(e20,e23) = e23
& op2(e23,e21) = e21
& op2(e21,e23) = e21 )
| ( op2(e22,e23) = e22
& op2(e23,e22) = e22
& op2(e22,e21) = e21
& op2(e21,e22) = e21 )
| ( op2(e22,e22) = e22
& op2(e22,e22) = e22
& op2(e22,e21) = e21
& op2(e21,e22) = e21 )
| ( op2(e22,e21) = e22
& op2(e21,e22) = e22
& op2(e22,e21) = e21
& op2(e21,e22) = e21 )
| ( op2(e22,e20) = e22
& op2(e20,e22) = e22
& op2(e22,e21) = e21
& op2(e21,e22) = e21 )
| ( op2(e21,e23) = e21
& op2(e23,e21) = e21
& op2(e21,e21) = e21
& op2(e21,e21) = e21 )
| ( op2(e21,e22) = e21
& op2(e22,e21) = e21
& op2(e21,e21) = e21
& op2(e21,e21) = e21 )
| ( op2(e21,e21) = e21
& op2(e21,e21) = e21
& op2(e21,e21) = e21
& op2(e21,e21) = e21 )
| ( op2(e21,e20) = e21
& op2(e20,e21) = e21
& op2(e21,e21) = e21
& op2(e21,e21) = e21 )
| ( op2(e20,e23) = e20
& op2(e23,e20) = e20
& op2(e20,e21) = e21
& op2(e21,e20) = e21 )
| ( op2(e20,e22) = e20
& op2(e22,e20) = e20
& op2(e20,e21) = e21
& op2(e21,e20) = e21 )
| ( op2(e20,e21) = e20
& op2(e21,e20) = e20
& op2(e20,e21) = e21
& op2(e21,e20) = e21 )
| ( op2(e20,e20) = e20
& op2(e20,e20) = e20
& op2(e20,e21) = e21
& op2(e21,e20) = e21 )
| ( op2(e23,e23) = e23
& op2(e23,e23) = e23
& op2(e23,e20) = e20
& op2(e20,e23) = e20 )
| ( op2(e23,e22) = e23
& op2(e22,e23) = e23
& op2(e23,e20) = e20
& op2(e20,e23) = e20 )
| ( op2(e23,e21) = e23
& op2(e21,e23) = e23
& op2(e23,e20) = e20
& op2(e20,e23) = e20 )
| ( op2(e23,e20) = e23
& op2(e20,e23) = e23
& op2(e23,e20) = e20
& op2(e20,e23) = e20 )
| ( op2(e22,e23) = e22
& op2(e23,e22) = e22
& op2(e22,e20) = e20
& op2(e20,e22) = e20 )
| ( op2(e22,e22) = e22
& op2(e22,e22) = e22
& op2(e22,e20) = e20
& op2(e20,e22) = e20 )
| ( op2(e22,e21) = e22
& op2(e21,e22) = e22
& op2(e22,e20) = e20
& op2(e20,e22) = e20 )
| ( op2(e22,e20) = e22
& op2(e20,e22) = e22
& op2(e22,e20) = e20
& op2(e20,e22) = e20 )
| ( op2(e21,e23) = e21
& op2(e23,e21) = e21
& op2(e21,e20) = e20
& op2(e20,e21) = e20 )
| ( op2(e21,e22) = e21
& op2(e22,e21) = e21
& op2(e21,e20) = e20
& op2(e20,e21) = e20 )
| ( op2(e21,e21) = e21
& op2(e21,e21) = e21
& op2(e21,e20) = e20
& op2(e20,e21) = e20 )
| ( op2(e21,e20) = e21
& op2(e20,e21) = e21
& op2(e21,e20) = e20
& op2(e20,e21) = e20 )
| ( op2(e20,e23) = e20
& op2(e23,e20) = e20
& op2(e20,e20) = e20
& op2(e20,e20) = e20 )
| ( op2(e20,e22) = e20
& op2(e22,e20) = e20
& op2(e20,e20) = e20
& op2(e20,e20) = e20 )
| ( op2(e20,e21) = e20
& op2(e21,e20) = e20
& op2(e20,e20) = e20
& op2(e20,e20) = e20 )
| ( op2(e20,e20) = e20
& op2(e20,e20) = e20
& op2(e20,e20) = e20
& op2(e20,e20) = e20 ) )
& ( ( op2(e23,op2(e23,e23)) != e23
& op2(e23,op2(e23,e22)) != e22
& op2(e23,op2(e23,e21)) != e21
& op2(e23,op2(e23,e20)) != e20 )
| ( op2(e22,op2(e22,e23)) != e23
& op2(e22,op2(e22,e22)) != e22
& op2(e22,op2(e22,e21)) != e21
& op2(e22,op2(e22,e20)) != e20 )
| ( op2(e21,op2(e21,e23)) != e23
& op2(e21,op2(e21,e22)) != e22
& op2(e21,op2(e21,e21)) != e21
& op2(e21,op2(e21,e20)) != e20 )
| ( op2(e20,op2(e20,e23)) != e23
& op2(e20,op2(e20,e22)) != e22
& op2(e20,op2(e20,e21)) != e21
& op2(e20,op2(e20,e20)) != e20 ) )
& ( op2(e23,e23) = e23
| op2(e22,e22) = e23
| op2(e21,e21) = e23
| op2(e20,e20) = e23 )
& ( op2(e23,e23) = e22
| op2(e22,e22) = e22
| op2(e21,e21) = e22
| op2(e20,e20) = e22 )
& ( op2(e23,e23) = e21
| op2(e22,e22) = e21
| op2(e21,e21) = e21
| op2(e20,e20) = e21 )
& ( op2(e23,e23) = e20
| op2(e22,e22) = e20
| op2(e21,e21) = e20
| op2(e20,e20) = e20 ) ),
file('theBenchmark.p',ax11) ).
fof(ax12,axiom,
( e12 = op1(op1(e13,e13),e13)
& e11 = op1(e13,e13)
& e10 = op1(op1(e13,e13),op1(op1(e13,e13),e13)) ),
file('theBenchmark.p',ax12) ).
fof(ax13,axiom,
( e22 = op2(op2(e23,e23),e23)
& e21 = op2(e23,e23)
& e20 = op2(op2(e23,e23),op2(op2(e23,e23),e23)) ),
file('theBenchmark.p',ax13) ).
fof(ax17,axiom,
( h4(e12) = op2(op2(e23,e23),e23)
& h4(e11) = op2(e23,e23)
& h4(e10) = op2(op2(e23,e23),op2(op2(e23,e23),e23))
& h4(e13) = e23 ),
file('theBenchmark.p',ax17) ).
fof(co1,conjecture,
( ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ( ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_22,plain,
( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_39,plain,
( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_42,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| op1(e10,e10) = e13 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_45,plain,
( op1(e11,e13) = e11
| op1(e11,e12) = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_46,plain,
( op1(e13,e11) = e11
| op1(e12,e11) = e11
| op1(e11,e11) = e11
| op1(e10,e11) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_54,plain,
( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_58,plain,
( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| op1(e10,e12) = 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_60,plain,
( op1(e13,e13) = e10
| op1(e12,e13) = e10
| op1(e11,e13) = e10
| op1(e10,e13) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_63,plain,
( op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_70,plain,
( op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_87,plain,
( op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| op2(e20,e20) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_90,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| op2(e20,e20) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_93,plain,
( op2(e21,e23) = e21
| op2(e21,e22) = e21
| op2(e21,e21) = e21
| op2(e21,e20) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_94,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| op2(e21,e21) = e21
| op2(e20,e21) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_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_106,plain,
( op2(e23,e22) = e23
| op2(e22,e22) = e23
| op2(e21,e22) = e23
| op2(e20,e22) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_107,plain,
( op2(e23,e23) = e20
| op2(e23,e22) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_108,plain,
( op2(e23,e23) = e20
| op2(e22,e23) = e20
| op2(e21,e23) = e20
| op2(e20,e23) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_111,plain,
( op2(e23,e23) = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_119,plain,
op1(e13,e10) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_136,plain,
op1(e12,e12) != op1(e11,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_137,plain,
op1(e13,e12) != op1(e11,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(e10,e13) != op1(e11,e13),
inference(copy,[status(thm)],[c_139]) ).
cnf(c_143,plain,
op1(e13,e13) != op1(e10,e13),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_151,plain,
op1(e10,e13) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_160,plain,
op1(e11,e12) != op1(e11,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_161,plain,
op1(e11,e13) != op1(e11,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_177,plain,
op1(e13,e13) != op1(e13,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_178,plain,
op1(e13,e13) != op1(e13,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_183,plain,
op2(e23,e20) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_200,plain,
op2(e22,e22) != op2(e21,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_201,plain,
op2(e23,e22) != op2(e21,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(e20,e23) != op2(e21,e23),
inference(copy,[status(thm)],[c_203]) ).
cnf(c_207,plain,
op2(e23,e23) != op2(e20,e23),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_215,plain,
op2(e20,e23) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_224,plain,
op2(e21,e22) != op2(e21,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_225,plain,
op2(e21,e23) != op2(e21,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_241,plain,
op2(e23,e23) != op2(e23,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_242,plain,
op2(e23,e23) != op2(e23,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_243,plain,
e11 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_244,plain,
e10 != e11,
inference(copy,[status(thm)],[c_243]) ).
cnf(c_245,plain,
e12 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_246,plain,
e10 != e12,
inference(copy,[status(thm)],[c_245]) ).
cnf(c_247,plain,
e13 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_248,plain,
e12 != e11,
inference(clausify,[status(thm)],[ax7]) ).
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,
e20 != e21,
inference(copy,[status(thm)],[c_251]) ).
cnf(c_253,plain,
e22 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_254,plain,
e20 != e22,
inference(copy,[status(thm)],[c_253]) ).
cnf(c_255,plain,
e23 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_256,plain,
e22 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_257,plain,
e23 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_258,plain,
e23 != e22,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_287,plain,
( op1(e13,e13) = e10
| op1(e12,e12) = e10
| op1(e11,e11) = e10
| op1(e10,e10) = e10 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_289,plain,
( op1(e13,e13) = e12
| op1(e12,e12) = e12
| op1(e11,e11) = e12
| op1(e10,e10) = e12 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_290,plain,
( op1(e13,e13) = e13
| op1(e12,e12) = e13
| op1(e11,e11) = e13
| op1(e10,e10) = e13 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_687,plain,
( op2(e23,e23) = e20
| op2(e22,e22) = e20
| op2(e21,e21) = e20
| op2(e20,e20) = e20 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_689,plain,
( op2(e23,e23) = e22
| op2(e22,e22) = e22
| op2(e21,e21) = e22
| op2(e20,e20) = e22 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_690,plain,
( op2(e23,e23) = e23
| op2(e22,e22) = e23
| op2(e21,e21) = e23
| op2(e20,e20) = e23 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_1087,plain,
op1(op1(e13,e13),op1(op1(e13,e13),e13)) = e10,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_1088,plain,
op1(e13,e13) = e11,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_1089,plain,
op1(op1(e13,e13),e13) = e12,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_1090,plain,
op1(e11,e13) = e12,
inference(paramod,[status(thm)],[c_1088,c_1089]) ).
cnf(c_1091,plain,
op2(op2(e23,e23),op2(op2(e23,e23),e23)) = e20,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_1092,plain,
op2(e23,e23) = e21,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_1093,plain,
op2(op2(e23,e23),e23) = e22,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_1094,plain,
op2(e21,e23) = e22,
inference(paramod,[status(thm)],[c_1092,c_1093]) ).
cnf(c_1107,plain,
h4(e13) = e23,
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_1108,plain,
h4(e10) = op2(op2(e23,e23),op2(op2(e23,e23),e23)),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_2980,plain,
h4(e10) = op2(e21,op2(op2(e23,e23),e23)),
inference(paramod,[status(thm)],[c_1092,c_1108]) ).
cnf(c_2981,plain,
h4(e10) = op2(e21,op2(e21,e23)),
inference(paramod,[status(thm)],[c_1092,c_2980]) ).
cnf(c_1109,plain,
h4(e10) = op2(e21,e22),
inference(paramod,[status(thm)],[c_1094,c_2981]) ).
cnf(c_1110,plain,
h4(e11) = op2(e23,e23),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_1111,plain,
h4(e11) = e21,
inference(paramod,[status(thm)],[c_1092,c_1110]) ).
cnf(c_1112,plain,
h4(e12) = op2(op2(e23,e23),e23),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_2982,plain,
h4(e12) = op2(e21,e23),
inference(paramod,[status(thm)],[c_1092,c_1112]) ).
cnf(c_1113,plain,
h4(e12) = e22,
inference(paramod,[status(thm)],[c_1094,c_2982]) ).
cnf(c_2240,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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)) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_2983,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(op2(e21,e22),h4(e10)) ),
inference(paramod,[status(thm)],[c_1109,c_2240]) ).
cnf(c_2984,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1109,c_2983]) ).
cnf(c_2985,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(op2(e21,e22),h4(e11))
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1109,c_2984]) ).
cnf(c_2986,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1111,c_2985]) ).
cnf(c_2987,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(op2(e21,e22),h4(e12))
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1109,c_2986]) ).
cnf(c_2988,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1113,c_2987]) ).
cnf(c_2989,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(op2(e21,e22),h4(e13))
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1109,c_2988]) ).
cnf(c_2990,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1107,c_2989]) ).
cnf(c_2991,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e21,h4(e10))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1111,c_2990]) ).
cnf(c_2992,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1109,c_2991]) ).
cnf(c_2993,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e21,h4(e11))
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1111,c_2992]) ).
cnf(c_2994,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1111,c_2993]) ).
cnf(c_2995,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e21,h4(e12))
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1111,c_2994]) ).
cnf(c_2996,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1113,c_2995]) ).
cnf(c_2997,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e12) != op2(h4(e11),h4(e13))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1090,c_2996]) ).
cnf(c_2998,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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))
| e22 != op2(h4(e11),h4(e13))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1113,c_2997]) ).
cnf(c_2999,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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))
| e22 != op2(e21,h4(e13))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1111,c_2998]) ).
cnf(c_3000,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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))
| e22 != op2(e21,e23)
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1107,c_2999]) ).
cnf(c_3001,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1094,c_3000]) ).
cnf(c_3002,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e22,h4(e10))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1113,c_3001]) ).
cnf(c_3003,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1109,c_3002]) ).
cnf(c_3004,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e22,h4(e11))
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1113,c_3003]) ).
cnf(c_3005,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1111,c_3004]) ).
cnf(c_3006,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e22,h4(e12))
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1113,c_3005]) ).
cnf(c_3007,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1113,c_3006]) ).
cnf(c_3008,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e22,h4(e13))
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1113,c_3007]) ).
cnf(c_3009,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1107,c_3008]) ).
cnf(c_3010,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e23,h4(e10))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1107,c_3009]) ).
cnf(c_3011,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1109,c_3010]) ).
cnf(c_3012,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e23,h4(e11))
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1107,c_3011]) ).
cnf(c_3013,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| 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(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1111,c_3012]) ).
cnf(c_3014,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| h4(e10) != e20
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| h4(op1(e13,e12)) != op2(e23,h4(e12))
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1107,c_3013]) ).
cnf(c_3015,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| h4(e10) != e20
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1113,c_3014]) ).
cnf(c_3016,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| h4(e10) != e20
| h4(e11) != op2(h4(e13),h4(e13))
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1088,c_3015]) ).
cnf(c_3017,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| h4(e10) != e20
| e21 != op2(h4(e13),h4(e13))
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1111,c_3016]) ).
cnf(c_3018,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| h4(e10) != e20
| e21 != op2(e23,h4(e13))
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1107,c_3017]) ).
cnf(c_3019,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| h4(e10) != e20
| e21 != op2(e23,e23)
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1107,c_3018]) ).
cnf(c_3020,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| h4(e10) != e20
| e21 != e21
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1092,c_3019]) ).
cnf(c_3021,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| op2(e21,e22) != e20
| e21 != e21
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1109,c_3020]) ).
cnf(c_3022,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| e21 != e21
| op2(e21,e22) != e20
| e21 != e21
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1111,c_3021]) ).
cnf(c_3023,negated_conjecture,
( h4(e13) != e23
| e22 != e22
| e21 != e21
| op2(e21,e22) != e20
| e21 != e21
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1113,c_3022]) ).
cnf(c_3024,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| op2(e21,e22) != e20
| e21 != e21
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e22 != e22
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_1107,c_3023]) ).
cnf(c_3025,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| op2(e21,e22) != e20
| e21 != e21
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(copy,[status(thm)],[c_3024]) ).
cnf(c_3026,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(copy,[status(thm)],[c_3025]) ).
cnf(c_3027,negated_conjecture,
( e23 != e23
| e22 != e22
| op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(copy,[status(thm)],[c_3026]) ).
cnf(c_3028,negated_conjecture,
( e23 != e23
| op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(copy,[status(thm)],[c_3027]) ).
cnf(c_2241,negated_conjecture,
( op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(op2(e21,e22),op2(e21,e22)) ),
inference(copy,[status(thm)],[c_3028]) ).
cnf(c_3029,plain,
op1(e11,op1(op1(e13,e13),e13)) = e10,
inference(paramod,[status(thm)],[c_1088,c_1087]) ).
cnf(c_3030,plain,
op1(e11,op1(e11,e13)) = e10,
inference(paramod,[status(thm)],[c_1088,c_3029]) ).
cnf(c_2470,plain,
op1(e11,e12) = e10,
inference(paramod,[status(thm)],[c_1090,c_3030]) ).
cnf(c_3031,plain,
( e11 = e13
| op1(e12,e12) = e13
| op1(e11,e11) = e13
| op1(e10,e10) = e13 ),
inference(paramod,[status(thm)],[c_1088,c_290]) ).
cnf(c_3032,plain,
( e13 = e11
| op1(e12,e12) = e13
| op1(e11,e11) = e13
| op1(e10,e10) = e13 ),
inference(copy,[status(thm)],[c_3031]) ).
cnf(c_2537,plain,
( op1(e12,e12) = e13
| op1(e11,e11) = e13
| op1(e10,e10) = e13 ),
inference(resolve,[status(thm)],[c_249,c_3032]) ).
cnf(c_3033,plain,
( e11 = e12
| op1(e12,e12) = e12
| op1(e11,e11) = e12
| op1(e10,e10) = e12 ),
inference(paramod,[status(thm)],[c_1088,c_289]) ).
cnf(c_3034,plain,
( e12 = e11
| op1(e12,e12) = e12
| op1(e11,e11) = e12
| op1(e10,e10) = e12 ),
inference(copy,[status(thm)],[c_3033]) ).
cnf(c_2538,plain,
( op1(e12,e12) = e12
| op1(e11,e11) = e12
| op1(e10,e10) = e12 ),
inference(resolve,[status(thm)],[c_248,c_3034]) ).
cnf(c_3035,plain,
( e11 = e10
| op1(e12,e12) = e10
| op1(e11,e11) = e10
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_1088,c_287]) ).
cnf(c_3036,plain,
( e10 = e11
| op1(e12,e12) = e10
| op1(e11,e11) = e10
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_3035]) ).
cnf(c_2539,plain,
( op1(e12,e12) = e10
| op1(e11,e11) = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_244,c_3036]) ).
cnf(c_3037,plain,
e11 != op1(e13,e12),
inference(paramod,[status(thm)],[c_1088,c_178]) ).
cnf(c_2540,plain,
op1(e13,e12) != e11,
inference(copy,[status(thm)],[c_3037]) ).
cnf(c_3038,plain,
e11 != op1(e13,e11),
inference(paramod,[status(thm)],[c_1088,c_177]) ).
cnf(c_2541,plain,
op1(e13,e11) != e11,
inference(copy,[status(thm)],[c_3038]) ).
cnf(c_3039,plain,
e11 != op1(e10,e13),
inference(paramod,[status(thm)],[c_1088,c_143]) ).
cnf(c_2544,plain,
op1(e10,e13) != e11,
inference(copy,[status(thm)],[c_3039]) ).
cnf(c_3040,plain,
( e11 = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 ),
inference(paramod,[status(thm)],[c_1088,c_63]) ).
cnf(c_3041,plain,
( e12 = e11
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 ),
inference(copy,[status(thm)],[c_3040]) ).
cnf(c_2547,plain,
( op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 ),
inference(resolve,[status(thm)],[c_248,c_3041]) ).
cnf(c_3042,plain,
( op1(e13,e13) = e10
| op1(e12,e13) = e10
| e12 = e10
| op1(e10,e13) = e10 ),
inference(paramod,[status(thm)],[c_1090,c_60]) ).
cnf(c_3043,plain,
( e11 = e10
| op1(e12,e13) = e10
| e12 = e10
| op1(e10,e13) = e10 ),
inference(paramod,[status(thm)],[c_1088,c_3042]) ).
cnf(c_3044,plain,
( e11 = e10
| op1(e12,e13) = e10
| e10 = e12
| op1(e10,e13) = e10 ),
inference(copy,[status(thm)],[c_3043]) ).
cnf(c_3045,plain,
( e10 = e11
| op1(e12,e13) = e10
| e10 = e12
| op1(e10,e13) = e10 ),
inference(copy,[status(thm)],[c_3044]) ).
cnf(c_3046,plain,
( e10 = e11
| op1(e12,e13) = e10
| op1(e10,e13) = e10 ),
inference(resolve,[status(thm)],[c_246,c_3045]) ).
cnf(c_2548,plain,
( op1(e12,e13) = e10
| op1(e10,e13) = e10 ),
inference(resolve,[status(thm)],[c_244,c_3046]) ).
cnf(c_3047,plain,
( e11 = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 ),
inference(paramod,[status(thm)],[c_1088,c_59]) ).
cnf(c_3048,plain,
( e10 = e11
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 ),
inference(copy,[status(thm)],[c_3047]) ).
cnf(c_2549,plain,
( op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 ),
inference(resolve,[status(thm)],[c_244,c_3048]) ).
cnf(c_3049,plain,
e12 != op1(e11,e11),
inference(paramod,[status(thm)],[c_1090,c_161]) ).
cnf(c_2557,plain,
op1(e11,e11) != e12,
inference(copy,[status(thm)],[c_3049]) ).
cnf(c_2560,plain,
op1(e10,e13) != e12,
inference(paramod,[status(thm)],[c_1090,c_140]) ).
cnf(c_3050,plain,
( op1(e11,e13) = e11
| e10 = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 ),
inference(paramod,[status(thm)],[c_2470,c_45]) ).
cnf(c_3051,plain,
( e12 = e11
| e10 = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 ),
inference(paramod,[status(thm)],[c_1090,c_3050]) ).
cnf(c_3052,plain,
( e12 = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 ),
inference(resolve,[status(thm)],[c_244,c_3051]) ).
cnf(c_2562,plain,
( op1(e11,e11) = e11
| op1(e11,e10) = e11 ),
inference(resolve,[status(thm)],[c_248,c_3052]) ).
cnf(c_3053,plain,
op2(e21,op2(op2(e23,e23),e23)) = e20,
inference(paramod,[status(thm)],[c_1092,c_1091]) ).
cnf(c_3054,plain,
op2(e21,op2(e21,e23)) = e20,
inference(paramod,[status(thm)],[c_1092,c_3053]) ).
cnf(c_2563,plain,
op2(e21,e22) = e20,
inference(paramod,[status(thm)],[c_1094,c_3054]) ).
cnf(c_3055,plain,
( e21 = e23
| op2(e22,e22) = e23
| op2(e21,e21) = e23
| op2(e20,e20) = e23 ),
inference(paramod,[status(thm)],[c_1092,c_690]) ).
cnf(c_3056,plain,
( e23 = e21
| op2(e22,e22) = e23
| op2(e21,e21) = e23
| op2(e20,e20) = e23 ),
inference(copy,[status(thm)],[c_3055]) ).
cnf(c_2630,plain,
( op2(e22,e22) = e23
| op2(e21,e21) = e23
| op2(e20,e20) = e23 ),
inference(resolve,[status(thm)],[c_257,c_3056]) ).
cnf(c_3057,plain,
( e21 = e22
| op2(e22,e22) = e22
| op2(e21,e21) = e22
| op2(e20,e20) = e22 ),
inference(paramod,[status(thm)],[c_1092,c_689]) ).
cnf(c_3058,plain,
( e22 = e21
| op2(e22,e22) = e22
| op2(e21,e21) = e22
| op2(e20,e20) = e22 ),
inference(copy,[status(thm)],[c_3057]) ).
cnf(c_2631,plain,
( op2(e22,e22) = e22
| op2(e21,e21) = e22
| op2(e20,e20) = e22 ),
inference(resolve,[status(thm)],[c_256,c_3058]) ).
cnf(c_3059,plain,
( e21 = e20
| op2(e22,e22) = e20
| op2(e21,e21) = e20
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_1092,c_687]) ).
cnf(c_3060,plain,
( e20 = e21
| op2(e22,e22) = e20
| op2(e21,e21) = e20
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_3059]) ).
cnf(c_2632,plain,
( op2(e22,e22) = e20
| op2(e21,e21) = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_252,c_3060]) ).
cnf(c_3061,plain,
e21 != op2(e23,e22),
inference(paramod,[status(thm)],[c_1092,c_242]) ).
cnf(c_2633,plain,
op2(e23,e22) != e21,
inference(copy,[status(thm)],[c_3061]) ).
cnf(c_3062,plain,
e21 != op2(e23,e21),
inference(paramod,[status(thm)],[c_1092,c_241]) ).
cnf(c_2634,plain,
op2(e23,e21) != e21,
inference(copy,[status(thm)],[c_3062]) ).
cnf(c_3063,plain,
e21 != op2(e20,e23),
inference(paramod,[status(thm)],[c_1092,c_207]) ).
cnf(c_2637,plain,
op2(e20,e23) != e21,
inference(copy,[status(thm)],[c_3063]) ).
cnf(c_3064,plain,
( e21 = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(paramod,[status(thm)],[c_1092,c_111]) ).
cnf(c_3065,plain,
( e22 = e21
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(copy,[status(thm)],[c_3064]) ).
cnf(c_2640,plain,
( op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(resolve,[status(thm)],[c_256,c_3065]) ).
cnf(c_3066,plain,
( op2(e23,e23) = e20
| op2(e22,e23) = e20
| e22 = e20
| op2(e20,e23) = e20 ),
inference(paramod,[status(thm)],[c_1094,c_108]) ).
cnf(c_3067,plain,
( e21 = e20
| op2(e22,e23) = e20
| e22 = e20
| op2(e20,e23) = e20 ),
inference(paramod,[status(thm)],[c_1092,c_3066]) ).
cnf(c_3068,plain,
( e21 = e20
| op2(e22,e23) = e20
| e20 = e22
| op2(e20,e23) = e20 ),
inference(copy,[status(thm)],[c_3067]) ).
cnf(c_3069,plain,
( e20 = e21
| op2(e22,e23) = e20
| e20 = e22
| op2(e20,e23) = e20 ),
inference(copy,[status(thm)],[c_3068]) ).
cnf(c_3070,plain,
( e20 = e21
| op2(e22,e23) = e20
| op2(e20,e23) = e20 ),
inference(resolve,[status(thm)],[c_254,c_3069]) ).
cnf(c_2641,plain,
( op2(e22,e23) = e20
| op2(e20,e23) = e20 ),
inference(resolve,[status(thm)],[c_252,c_3070]) ).
cnf(c_3071,plain,
( e21 = e20
| op2(e23,e22) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 ),
inference(paramod,[status(thm)],[c_1092,c_107]) ).
cnf(c_3072,plain,
( e20 = e21
| op2(e23,e22) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 ),
inference(copy,[status(thm)],[c_3071]) ).
cnf(c_2642,plain,
( op2(e23,e22) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 ),
inference(resolve,[status(thm)],[c_252,c_3072]) ).
cnf(c_3073,plain,
e22 != op2(e21,e21),
inference(paramod,[status(thm)],[c_1094,c_225]) ).
cnf(c_2650,plain,
op2(e21,e21) != e22,
inference(copy,[status(thm)],[c_3073]) ).
cnf(c_2653,plain,
op2(e20,e23) != e22,
inference(paramod,[status(thm)],[c_1094,c_204]) ).
cnf(c_3074,plain,
( op2(e21,e23) = e21
| e20 = e21
| op2(e21,e21) = e21
| op2(e21,e20) = e21 ),
inference(paramod,[status(thm)],[c_2563,c_93]) ).
cnf(c_3075,plain,
( e22 = e21
| e20 = e21
| op2(e21,e21) = e21
| op2(e21,e20) = e21 ),
inference(paramod,[status(thm)],[c_1094,c_3074]) ).
cnf(c_3076,plain,
( e22 = e21
| op2(e21,e21) = e21
| op2(e21,e20) = e21 ),
inference(resolve,[status(thm)],[c_252,c_3075]) ).
cnf(c_2655,plain,
( op2(e21,e21) = e21
| op2(e21,e20) = e21 ),
inference(resolve,[status(thm)],[c_256,c_3076]) ).
cnf(c_3077,negated_conjecture,
( op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(e20,op2(e21,e22)) ),
inference(paramod,[status(thm)],[c_2563,c_2241]) ).
cnf(c_3078,negated_conjecture,
( op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(op2(e21,e22),e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2563,c_3077]) ).
cnf(c_3079,negated_conjecture,
( op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(op2(e21,e22),e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2563,c_3078]) ).
cnf(c_3080,negated_conjecture,
( op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(op2(e21,e22),e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2563,c_3079]) ).
cnf(c_3081,negated_conjecture,
( op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,op2(e21,e22))
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2563,c_3080]) ).
cnf(c_3082,negated_conjecture,
( op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h4(op1(e11,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2563,c_3081]) ).
cnf(c_3083,negated_conjecture,
( op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| h4(e10) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2470,c_3082]) ).
cnf(c_3084,negated_conjecture,
( op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| op2(e21,e22) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1109,c_3083]) ).
cnf(c_3085,negated_conjecture,
( op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e20 != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2563,c_3084]) ).
cnf(c_3086,negated_conjecture,
( op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,op2(e21,e22))
| e20 != e20
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2563,c_3085]) ).
cnf(c_3087,negated_conjecture,
( op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,op2(e21,e22))
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e20 != e20
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2563,c_3086]) ).
cnf(c_3088,negated_conjecture,
( op2(e21,e22) != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e20 != e20
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2563,c_3087]) ).
cnf(c_3089,negated_conjecture,
( e20 != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e20 != e20
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2563,c_3088]) ).
cnf(c_3090,negated_conjecture,
( e20 != e20
| h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_3089]) ).
cnf(c_2656,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_3090]) ).
cnf(c_3091,plain,
e10 != op1(e11,e11),
inference(paramod,[status(thm)],[c_2470,c_160]) ).
cnf(c_2735,plain,
op1(e11,e11) != e10,
inference(copy,[status(thm)],[c_3091]) ).
cnf(c_2737,plain,
op1(e13,e12) != e10,
inference(paramod,[status(thm)],[c_2470,c_137]) ).
cnf(c_2738,plain,
op1(e12,e12) != e10,
inference(paramod,[status(thm)],[c_2470,c_136]) ).
cnf(c_3092,plain,
( op1(e13,e12) = e13
| op1(e12,e12) = e13
| e10 = e13
| op1(e10,e12) = e13 ),
inference(paramod,[status(thm)],[c_2470,c_58]) ).
cnf(c_3093,plain,
( op1(e13,e12) = e13
| op1(e12,e12) = e13
| e13 = e10
| op1(e10,e12) = e13 ),
inference(copy,[status(thm)],[c_3092]) ).
cnf(c_2740,plain,
( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e10,e12) = e13 ),
inference(resolve,[status(thm)],[c_247,c_3093]) ).
cnf(c_3094,plain,
( op1(e13,e12) = e11
| op1(e12,e12) = e11
| e10 = e11
| op1(e10,e12) = e11 ),
inference(paramod,[status(thm)],[c_2470,c_54]) ).
cnf(c_3095,plain,
( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e10,e12) = e11 ),
inference(resolve,[status(thm)],[c_244,c_3094]) ).
cnf(c_2742,plain,
( op1(e12,e12) = e11
| op1(e10,e12) = e11 ),
inference(resolve,[status(thm)],[c_2540,c_3095]) ).
cnf(c_2744,plain,
( op1(e12,e11) = e11
| op1(e11,e11) = e11
| op1(e10,e11) = e11 ),
inference(resolve,[status(thm)],[c_2541,c_46]) ).
cnf(c_3096,plain,
( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e10 ),
inference(resolve,[status(thm)],[c_2544,c_22]) ).
cnf(c_2751,plain,
( op1(e10,e13) = e13
| op1(e10,e13) = e10 ),
inference(resolve,[status(thm)],[c_2560,c_3096]) ).
cnf(c_2756,plain,
( op1(e12,e12) = e12
| op1(e10,e10) = e12 ),
inference(resolve,[status(thm)],[c_2557,c_2538]) ).
cnf(c_2765,plain,
( op1(e10,e12) = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 ),
inference(resolve,[status(thm)],[c_2560,c_39]) ).
cnf(c_2766,plain,
h4(e10) = e20,
inference(paramod,[status(thm)],[c_2563,c_1109]) ).
cnf(c_3097,plain,
e20 != op2(e21,e21),
inference(paramod,[status(thm)],[c_2563,c_224]) ).
cnf(c_2773,plain,
op2(e21,e21) != e20,
inference(copy,[status(thm)],[c_3097]) ).
cnf(c_2775,plain,
op2(e23,e22) != e20,
inference(paramod,[status(thm)],[c_2563,c_201]) ).
cnf(c_2776,plain,
op2(e22,e22) != e20,
inference(paramod,[status(thm)],[c_2563,c_200]) ).
cnf(c_3098,plain,
( op2(e23,e22) = e23
| op2(e22,e22) = e23
| e20 = e23
| op2(e20,e22) = e23 ),
inference(paramod,[status(thm)],[c_2563,c_106]) ).
cnf(c_3099,plain,
( op2(e23,e22) = e23
| op2(e22,e22) = e23
| e23 = e20
| op2(e20,e22) = e23 ),
inference(copy,[status(thm)],[c_3098]) ).
cnf(c_2778,plain,
( op2(e23,e22) = e23
| op2(e22,e22) = e23
| op2(e20,e22) = e23 ),
inference(resolve,[status(thm)],[c_255,c_3099]) ).
cnf(c_3100,plain,
( op2(e23,e22) = e21
| op2(e22,e22) = e21
| e20 = e21
| op2(e20,e22) = e21 ),
inference(paramod,[status(thm)],[c_2563,c_102]) ).
cnf(c_3101,plain,
( op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e20,e22) = e21 ),
inference(resolve,[status(thm)],[c_252,c_3100]) ).
cnf(c_2780,plain,
( op2(e22,e22) = e21
| op2(e20,e22) = e21 ),
inference(resolve,[status(thm)],[c_2633,c_3101]) ).
cnf(c_2782,plain,
( op2(e22,e21) = e21
| op2(e21,e21) = e21
| op2(e20,e21) = e21 ),
inference(resolve,[status(thm)],[c_2634,c_94]) ).
cnf(c_3102,plain,
( op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e20 ),
inference(resolve,[status(thm)],[c_2637,c_70]) ).
cnf(c_2789,plain,
( op2(e20,e23) = e23
| op2(e20,e23) = e20 ),
inference(resolve,[status(thm)],[c_2653,c_3102]) ).
cnf(c_2794,plain,
( op2(e22,e22) = e22
| op2(e20,e20) = e22 ),
inference(resolve,[status(thm)],[c_2650,c_2631]) ).
cnf(c_2803,plain,
( op2(e20,e22) = e22
| op2(e20,e21) = e22
| op2(e20,e20) = e22 ),
inference(resolve,[status(thm)],[c_2653,c_87]) ).
cnf(c_3103,plain,
( op1(e12,e12) = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_2735,c_2539]) ).
cnf(c_2804,plain,
op1(e10,e10) = e10,
inference(resolve,[status(thm)],[c_2738,c_3103]) ).
cnf(c_2809,plain,
( op1(e13,e11) = e10
| op1(e13,e10) = e10 ),
inference(resolve,[status(thm)],[c_2737,c_2549]) ).
cnf(c_3104,plain,
( op2(e22,e22) = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_2773,c_2632]) ).
cnf(c_2816,plain,
op2(e20,e20) = e20,
inference(resolve,[status(thm)],[c_2776,c_3104]) ).
cnf(c_2821,plain,
( op2(e23,e21) = e20
| op2(e23,e20) = e20 ),
inference(resolve,[status(thm)],[c_2775,c_2642]) ).
cnf(c_3105,plain,
( op1(e10,e12) = e12
| op1(e10,e11) = e12
| e10 = e12 ),
inference(paramod,[status(thm)],[c_2804,c_2765]) ).
cnf(c_2828,plain,
( op1(e10,e12) = e12
| op1(e10,e11) = e12 ),
inference(resolve,[status(thm)],[c_246,c_3105]) ).
cnf(c_3106,plain,
( op1(e12,e12) = e12
| e10 = e12 ),
inference(paramod,[status(thm)],[c_2804,c_2756]) ).
cnf(c_2830,plain,
op1(e12,e12) = e12,
inference(resolve,[status(thm)],[c_246,c_3106]) ).
cnf(c_3107,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| h4(e10) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2804,c_2656]) ).
cnf(c_3108,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_2766,c_3107]) ).
cnf(c_3109,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2816,c_3108]) ).
cnf(c_3110,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(e12) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2830,c_3109]) ).
cnf(c_3111,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| e22 != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_1113,c_3110]) ).
cnf(c_3112,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| op2(e22,e22) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e20 != e20 ),
inference(copy,[status(thm)],[c_3111]) ).
cnf(c_2863,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| op2(e22,e22) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(copy,[status(thm)],[c_3112]) ).
cnf(c_3113,plain,
( op1(e12,e12) = e13
| op1(e11,e11) = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_2804,c_2537]) ).
cnf(c_3114,plain,
( e12 = e13
| op1(e11,e11) = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_2830,c_3113]) ).
cnf(c_3115,plain,
( e12 = e13
| op1(e11,e11) = e13
| e13 = e10 ),
inference(copy,[status(thm)],[c_3114]) ).
cnf(c_3116,plain,
( e13 = e12
| op1(e11,e11) = e13
| e13 = e10 ),
inference(copy,[status(thm)],[c_3115]) ).
cnf(c_3117,plain,
( e13 = e12
| op1(e11,e11) = e13 ),
inference(resolve,[status(thm)],[c_247,c_3116]) ).
cnf(c_2864,plain,
op1(e11,e11) = e13,
inference(resolve,[status(thm)],[c_250,c_3117]) ).
cnf(c_2874,plain,
op1(e10,e13) != e10,
inference(paramod,[status(thm)],[c_2804,c_151]) ).
cnf(c_2876,plain,
op1(e13,e10) != e10,
inference(paramod,[status(thm)],[c_2804,c_119]) ).
cnf(c_3118,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_2804,c_42]) ).
cnf(c_3119,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| e13 = e10 ),
inference(copy,[status(thm)],[c_3118]) ).
cnf(c_2878,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13 ),
inference(resolve,[status(thm)],[c_247,c_3119]) ).
cnf(c_3120,plain,
( op2(e20,e22) = e22
| op2(e20,e21) = e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_2816,c_2803]) ).
cnf(c_2880,plain,
( op2(e20,e22) = e22
| op2(e20,e21) = e22 ),
inference(resolve,[status(thm)],[c_254,c_3120]) ).
cnf(c_3121,plain,
( op2(e22,e22) = e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_2816,c_2794]) ).
cnf(c_2882,plain,
op2(e22,e22) = e22,
inference(resolve,[status(thm)],[c_254,c_3121]) ).
cnf(c_3122,plain,
( op2(e22,e22) = e23
| op2(e21,e21) = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_2816,c_2630]) ).
cnf(c_3123,plain,
( e22 = e23
| op2(e21,e21) = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_2882,c_3122]) ).
cnf(c_3124,plain,
( e22 = e23
| op2(e21,e21) = e23
| e23 = e20 ),
inference(copy,[status(thm)],[c_3123]) ).
cnf(c_3125,plain,
( e23 = e22
| op2(e21,e21) = e23
| e23 = e20 ),
inference(copy,[status(thm)],[c_3124]) ).
cnf(c_3126,plain,
( e23 = e22
| op2(e21,e21) = e23 ),
inference(resolve,[status(thm)],[c_255,c_3125]) ).
cnf(c_2885,plain,
op2(e21,e21) = e23,
inference(resolve,[status(thm)],[c_258,c_3126]) ).
cnf(c_2898,plain,
op2(e20,e23) != e20,
inference(paramod,[status(thm)],[c_2816,c_215]) ).
cnf(c_2900,plain,
op2(e23,e20) != e20,
inference(paramod,[status(thm)],[c_2816,c_183]) ).
cnf(c_3127,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_2816,c_90]) ).
cnf(c_3128,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| e23 = e20 ),
inference(copy,[status(thm)],[c_3127]) ).
cnf(c_2902,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23 ),
inference(resolve,[status(thm)],[c_255,c_3128]) ).
cnf(c_3129,plain,
( e12 = e11
| op1(e10,e12) = e11 ),
inference(paramod,[status(thm)],[c_2830,c_2742]) ).
cnf(c_2905,plain,
op1(e10,e12) = e11,
inference(resolve,[status(thm)],[c_248,c_3129]) ).
cnf(c_3130,plain,
( op1(e13,e12) = e13
| op1(e12,e12) = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_2905,c_2740]) ).
cnf(c_3131,plain,
( op1(e13,e12) = e13
| e12 = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_2830,c_3130]) ).
cnf(c_3132,plain,
( op1(e13,e12) = e13
| e12 = e13
| e13 = e11 ),
inference(copy,[status(thm)],[c_3131]) ).
cnf(c_3133,plain,
( op1(e13,e12) = e13
| e13 = e12
| e13 = e11 ),
inference(copy,[status(thm)],[c_3132]) ).
cnf(c_3134,plain,
( op1(e13,e12) = e13
| e13 = e12 ),
inference(resolve,[status(thm)],[c_249,c_3133]) ).
cnf(c_2906,plain,
op1(e13,e12) = e13,
inference(resolve,[status(thm)],[c_250,c_3134]) ).
cnf(c_3135,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| op2(e22,e22) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(e11) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2905,c_2863]) ).
cnf(c_3136,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| op2(e22,e22) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| e21 != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_1111,c_3135]) ).
cnf(c_3137,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| op2(e22,e22) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(e13) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| e21 != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2864,c_3136]) ).
cnf(c_3138,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| op2(e22,e22) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e23 != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| e21 != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_1107,c_3137]) ).
cnf(c_3139,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| op2(e22,e22) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e23 != e23
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| e21 != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2885,c_3138]) ).
cnf(c_3140,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| e22 != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e23 != e23
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| e21 != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2882,c_3139]) ).
cnf(c_3141,negated_conjecture,
( h4(e13) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| e22 != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e23 != e23
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| e21 != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2906,c_3140]) ).
cnf(c_3142,negated_conjecture,
( e23 != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| e22 != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e23 != e23
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| e21 != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_1107,c_3141]) ).
cnf(c_3143,negated_conjecture,
( e23 != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| e22 != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e23 != e23
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| op2(e20,e22) != e21
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(copy,[status(thm)],[c_3142]) ).
cnf(c_3144,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| e22 != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e23 != e23
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| op2(e20,e22) != e21
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(copy,[status(thm)],[c_3143]) ).
cnf(c_3145,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| e22 != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| op2(e20,e22) != e21
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(copy,[status(thm)],[c_3144]) ).
cnf(c_2910,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| op2(e20,e22) != e21
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(copy,[status(thm)],[c_3145]) ).
cnf(c_3146,plain,
( op1(e12,e11) = e11
| e13 = e11
| op1(e10,e11) = e11 ),
inference(paramod,[status(thm)],[c_2864,c_2744]) ).
cnf(c_2919,plain,
( op1(e12,e11) = e11
| op1(e10,e11) = e11 ),
inference(resolve,[status(thm)],[c_249,c_3146]) ).
cnf(c_3147,plain,
( e13 = e11
| op1(e11,e10) = e11 ),
inference(paramod,[status(thm)],[c_2864,c_2562]) ).
cnf(c_2920,plain,
op1(e11,e10) = e11,
inference(resolve,[status(thm)],[c_249,c_3147]) ).
cnf(c_2924,plain,
op1(e10,e13) = e13,
inference(resolve,[status(thm)],[c_2874,c_2751]) ).
cnf(c_3148,plain,
( op1(e12,e13) = e10
| e13 = e10 ),
inference(paramod,[status(thm)],[c_2924,c_2548]) ).
cnf(c_2925,plain,
op1(e12,e13) = e10,
inference(resolve,[status(thm)],[c_247,c_3148]) ).
cnf(c_2932,plain,
op1(e13,e11) = e10,
inference(resolve,[status(thm)],[c_2876,c_2809]) ).
cnf(c_3149,plain,
( e22 = e21
| op2(e20,e22) = e21 ),
inference(paramod,[status(thm)],[c_2882,c_2780]) ).
cnf(c_2936,plain,
op2(e20,e22) = e21,
inference(resolve,[status(thm)],[c_256,c_3149]) ).
cnf(c_3150,plain,
( op2(e23,e22) = e23
| op2(e22,e22) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_2936,c_2778]) ).
cnf(c_3151,plain,
( op2(e23,e22) = e23
| e22 = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_2882,c_3150]) ).
cnf(c_3152,plain,
( op2(e23,e22) = e23
| e22 = e23
| e23 = e21 ),
inference(copy,[status(thm)],[c_3151]) ).
cnf(c_3153,plain,
( op2(e23,e22) = e23
| e23 = e22
| e23 = e21 ),
inference(copy,[status(thm)],[c_3152]) ).
cnf(c_3154,plain,
( op2(e23,e22) = e23
| e23 = e22 ),
inference(resolve,[status(thm)],[c_257,c_3153]) ).
cnf(c_2937,plain,
op2(e23,e22) = e23,
inference(resolve,[status(thm)],[c_258,c_3154]) ).
cnf(c_3155,plain,
( op2(e22,e21) = e21
| e23 = e21
| op2(e20,e21) = e21 ),
inference(paramod,[status(thm)],[c_2885,c_2782]) ).
cnf(c_2944,plain,
( op2(e22,e21) = e21
| op2(e20,e21) = e21 ),
inference(resolve,[status(thm)],[c_257,c_3155]) ).
cnf(c_3156,plain,
( e23 = e21
| op2(e21,e20) = e21 ),
inference(paramod,[status(thm)],[c_2885,c_2655]) ).
cnf(c_2945,plain,
op2(e21,e20) = e21,
inference(resolve,[status(thm)],[c_257,c_3156]) ).
cnf(c_2952,plain,
op2(e20,e23) = e23,
inference(resolve,[status(thm)],[c_2898,c_2789]) ).
cnf(c_3157,plain,
( op2(e22,e23) = e20
| e23 = e20 ),
inference(paramod,[status(thm)],[c_2952,c_2641]) ).
cnf(c_2953,plain,
op2(e22,e23) = e20,
inference(resolve,[status(thm)],[c_255,c_3157]) ).
cnf(c_2960,plain,
op2(e23,e21) = e20,
inference(resolve,[status(thm)],[c_2900,c_2821]) ).
cnf(c_3158,plain,
( e11 = e12
| op1(e10,e11) = e12 ),
inference(paramod,[status(thm)],[c_2905,c_2828]) ).
cnf(c_3159,plain,
( e12 = e11
| op1(e10,e11) = e12 ),
inference(copy,[status(thm)],[c_3158]) ).
cnf(c_2963,plain,
op1(e10,e11) = e12,
inference(resolve,[status(thm)],[c_248,c_3159]) ).
cnf(c_3160,plain,
( op1(e13,e12) = e12
| e10 = e12
| op1(e13,e10) = e12 ),
inference(paramod,[status(thm)],[c_2932,c_2547]) ).
cnf(c_3161,plain,
( e13 = e12
| e10 = e12
| op1(e13,e10) = e12 ),
inference(paramod,[status(thm)],[c_2906,c_3160]) ).
cnf(c_3162,plain,
( e13 = e12
| op1(e13,e10) = e12 ),
inference(resolve,[status(thm)],[c_246,c_3161]) ).
cnf(c_2964,plain,
op1(e13,e10) = e12,
inference(resolve,[status(thm)],[c_250,c_3162]) ).
cnf(c_3163,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| op2(e20,e22) != e21
| h4(e12) != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2963,c_2910]) ).
cnf(c_3164,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| op2(e20,e22) != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_1113,c_3163]) ).
cnf(c_3165,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2936,c_3164]) ).
cnf(c_3166,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(e13) != op2(e20,e23)
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2924,c_3165]) ).
cnf(c_3167,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e10)) != op2(e21,e20)
| e23 != op2(e20,e23)
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_1107,c_3166]) ).
cnf(c_3168,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(op1(e11,e10)) != op2(e21,e20)
| e23 != e23
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2952,c_3167]) ).
cnf(c_3169,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| h4(e11) != op2(e21,e20)
| e23 != e23
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2920,c_3168]) ).
cnf(c_3170,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != op2(e21,e20)
| e23 != e23
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_1111,c_3169]) ).
cnf(c_3171,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| e23 != e23
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2945,c_3170]) ).
cnf(c_3172,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| h4(e10) != op2(e22,e23)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| e23 != e23
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2925,c_3171]) ).
cnf(c_3173,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| e20 != op2(e22,e23)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| e23 != e23
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2766,c_3172]) ).
cnf(c_3174,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e13,e10)) != op2(e23,e20)
| e20 != e20
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| e23 != e23
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2953,c_3173]) ).
cnf(c_3175,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(e12) != op2(e23,e20)
| e20 != e20
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| e23 != e23
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2964,c_3174]) ).
cnf(c_3176,negated_conjecture,
( op2(e23,e22) != e23
| h4(op1(e13,e11)) != op2(e23,e21)
| e22 != op2(e23,e20)
| e20 != e20
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| e23 != e23
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_1113,c_3175]) ).
cnf(c_3177,negated_conjecture,
( op2(e23,e22) != e23
| h4(e10) != op2(e23,e21)
| e22 != op2(e23,e20)
| e20 != e20
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| e23 != e23
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2932,c_3176]) ).
cnf(c_3178,negated_conjecture,
( op2(e23,e22) != e23
| e20 != op2(e23,e21)
| e22 != op2(e23,e20)
| e20 != e20
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| e23 != e23
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2766,c_3177]) ).
cnf(c_3179,negated_conjecture,
( op2(e23,e22) != e23
| e20 != e20
| e22 != op2(e23,e20)
| e20 != e20
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| e23 != e23
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2960,c_3178]) ).
cnf(c_3180,negated_conjecture,
( e23 != e23
| e20 != e20
| e22 != op2(e23,e20)
| e20 != e20
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| e23 != e23
| e21 != e21
| e22 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2937,c_3179]) ).
cnf(c_3181,negated_conjecture,
( e23 != e23
| e20 != e20
| e22 != op2(e23,e20)
| e20 != e20
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| e23 != e23
| e21 != e21
| op2(e20,e21) != e22 ),
inference(copy,[status(thm)],[c_3180]) ).
cnf(c_3182,negated_conjecture,
( e23 != e23
| e20 != e20
| op2(e23,e20) != e22
| e20 != e20
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| e23 != e23
| e21 != e21
| op2(e20,e21) != e22 ),
inference(copy,[status(thm)],[c_3181]) ).
cnf(c_3183,negated_conjecture,
( e23 != e23
| e20 != e20
| op2(e23,e20) != e22
| e20 != e20
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| e23 != e23
| op2(e20,e21) != e22 ),
inference(copy,[status(thm)],[c_3182]) ).
cnf(c_3184,negated_conjecture,
( e23 != e23
| e20 != e20
| op2(e23,e20) != e22
| e20 != e20
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e21 != e21
| op2(e20,e21) != e22 ),
inference(copy,[status(thm)],[c_3183]) ).
cnf(c_3185,negated_conjecture,
( e23 != e23
| e20 != e20
| op2(e23,e20) != e22
| e20 != e20
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| op2(e20,e21) != e22 ),
inference(copy,[status(thm)],[c_3184]) ).
cnf(c_3186,negated_conjecture,
( e23 != e23
| e20 != e20
| op2(e23,e20) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| op2(e20,e21) != e22 ),
inference(copy,[status(thm)],[c_3185]) ).
cnf(c_3187,negated_conjecture,
( e23 != e23
| op2(e23,e20) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| op2(e20,e21) != e22 ),
inference(copy,[status(thm)],[c_3186]) ).
cnf(c_2967,negated_conjecture,
( op2(e23,e20) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| op2(e20,e21) != e22 ),
inference(copy,[status(thm)],[c_3187]) ).
cnf(c_3188,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_2920,c_2878]) ).
cnf(c_3189,plain,
( e12 = e13
| op1(e12,e10) = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_2964,c_3188]) ).
cnf(c_3190,plain,
( e12 = e13
| op1(e12,e10) = e13
| e13 = e11 ),
inference(copy,[status(thm)],[c_3189]) ).
cnf(c_3191,plain,
( e13 = e12
| op1(e12,e10) = e13
| e13 = e11 ),
inference(copy,[status(thm)],[c_3190]) ).
cnf(c_3192,plain,
( e13 = e12
| op1(e12,e10) = e13 ),
inference(resolve,[status(thm)],[c_249,c_3191]) ).
cnf(c_2968,plain,
op1(e12,e10) = e13,
inference(resolve,[status(thm)],[c_250,c_3192]) ).
cnf(c_3193,plain,
( e21 = e22
| op2(e20,e21) = e22 ),
inference(paramod,[status(thm)],[c_2936,c_2880]) ).
cnf(c_3194,plain,
( e22 = e21
| op2(e20,e21) = e22 ),
inference(copy,[status(thm)],[c_3193]) ).
cnf(c_2970,plain,
op2(e20,e21) = e22,
inference(resolve,[status(thm)],[c_256,c_3194]) ).
cnf(c_3195,plain,
( op2(e23,e22) = e22
| e20 = e22
| op2(e23,e20) = e22 ),
inference(paramod,[status(thm)],[c_2960,c_2640]) ).
cnf(c_3196,plain,
( e23 = e22
| e20 = e22
| op2(e23,e20) = e22 ),
inference(paramod,[status(thm)],[c_2937,c_3195]) ).
cnf(c_3197,plain,
( e23 = e22
| op2(e23,e20) = e22 ),
inference(resolve,[status(thm)],[c_254,c_3196]) ).
cnf(c_2971,plain,
op2(e23,e20) = e22,
inference(resolve,[status(thm)],[c_258,c_3197]) ).
cnf(c_3198,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_2945,c_2902]) ).
cnf(c_3199,plain,
( e22 = e23
| op2(e22,e20) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_2971,c_3198]) ).
cnf(c_3200,plain,
( e22 = e23
| op2(e22,e20) = e23
| e23 = e21 ),
inference(copy,[status(thm)],[c_3199]) ).
cnf(c_3201,plain,
( e23 = e22
| op2(e22,e20) = e23
| e23 = e21 ),
inference(copy,[status(thm)],[c_3200]) ).
cnf(c_3202,plain,
( e23 = e22
| op2(e22,e20) = e23 ),
inference(resolve,[status(thm)],[c_257,c_3201]) ).
cnf(c_2973,plain,
op2(e22,e20) = e23,
inference(resolve,[status(thm)],[c_258,c_3202]) ).
cnf(c_3203,plain,
( op1(e12,e11) = e11
| e12 = e11 ),
inference(paramod,[status(thm)],[c_2963,c_2919]) ).
cnf(c_2977,plain,
op1(e12,e11) = e11,
inference(resolve,[status(thm)],[c_248,c_3203]) ).
cnf(c_3204,negated_conjecture,
( op2(e23,e20) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(op1(e12,e10)) != op2(e22,e20)
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2970,c_2967]) ).
cnf(c_3205,negated_conjecture,
( op2(e23,e20) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(e13) != op2(e22,e20)
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2968,c_3204]) ).
cnf(c_3206,negated_conjecture,
( op2(e23,e20) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| e23 != op2(e22,e20)
| e22 != e22 ),
inference(paramod,[status(thm)],[c_1107,c_3205]) ).
cnf(c_3207,negated_conjecture,
( op2(e23,e20) != e22
| h4(op1(e12,e11)) != op2(e22,e21)
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2973,c_3206]) ).
cnf(c_3208,negated_conjecture,
( op2(e23,e20) != e22
| h4(e11) != op2(e22,e21)
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2977,c_3207]) ).
cnf(c_3209,negated_conjecture,
( op2(e23,e20) != e22
| e21 != op2(e22,e21)
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_1111,c_3208]) ).
cnf(c_3210,negated_conjecture,
( e22 != e22
| e21 != op2(e22,e21)
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2971,c_3209]) ).
cnf(c_3211,negated_conjecture,
( e22 != e22
| op2(e22,e21) != e21
| e23 != e23
| e22 != e22 ),
inference(copy,[status(thm)],[c_3210]) ).
cnf(c_3212,negated_conjecture,
( e22 != e22
| op2(e22,e21) != e21
| e23 != e23 ),
inference(copy,[status(thm)],[c_3211]) ).
cnf(c_3213,negated_conjecture,
( e22 != e22
| op2(e22,e21) != e21 ),
inference(copy,[status(thm)],[c_3212]) ).
cnf(c_2978,negated_conjecture,
op2(e22,e21) != e21,
inference(copy,[status(thm)],[c_3213]) ).
cnf(c_3214,plain,
( op2(e22,e21) = e21
| e22 = e21 ),
inference(paramod,[status(thm)],[c_2970,c_2944]) ).
cnf(c_3215,plain,
op2(e22,e21) = e21,
inference(resolve,[status(thm)],[c_256,c_3214]) ).
cnf(c_2979,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_2978,c_3215]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG115+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n018.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sat Sep 26 21:12:37 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.34 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.34 % Process 1420729 was started by sandbox2 on n018,
% 0.07/0.34 % Sat Sep 26 21:12:37 2026
% 0.07/0.34 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 14.66/14.99
% 14.66/14.99 % From the command line: assign(max_seconds, 300).
% 20.11/16.04
% 20.11/16.04 % SZS status Theorem for theBenchmark
% 20.11/16.04
% 20.11/16.04 % Proof 1 at 0.93 (+ 0.04) seconds.
% 20.11/16.04 % Length of proof is 183.
% 20.11/16.04 % Level of proof is 12.
% 20.11/16.04 % Maximum clause weight is 133.000.
% 20.11/16.04 % Given clauses 0.
% 20.11/16.04
% 20.11/16.04 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------