%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG121+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:34 AM UTC 2026
% Result : Theorem 9.97s 6.52s
% Output : CNFRefutation 9.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 108
% Number of leaves : 14
% Syntax : Number of formulae : 415 ( 142 unt; 0 def)
% Number of atoms : 3051 (3050 equ)
% Maximal formula atoms : 128 ( 7 avg)
% Number of connectives : 4419 (1783 ~;2183 |; 453 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 6 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(e12,e12) != e12
& op1(e12,e13) = e13
& op1(e13,e12) = e13 )
| ( op1(e11,e11) != e11
& op1(e11,e13) = e13
& op1(e13,e11) = e13 )
| ( op1(e10,e10) != e10
& op1(e10,e13) = e13
& op1(e13,e10) = e13 )
| ( op1(e13,e13) != e13
& op1(e13,e12) = e12
& op1(e12,e13) = e12 )
| ( op1(e12,e12) != e12
& op1(e12,e12) = e12
& op1(e12,e12) = e12 )
| ( op1(e11,e11) != e11
& op1(e11,e12) = e12
& op1(e12,e11) = e12 )
| ( op1(e10,e10) != e10
& op1(e10,e12) = e12
& op1(e12,e10) = e12 )
| ( op1(e13,e13) != e13
& op1(e13,e11) = e11
& op1(e11,e13) = e11 )
| ( op1(e12,e12) != e12
& op1(e12,e11) = e11
& op1(e11,e12) = e11 )
| ( op1(e11,e11) != e11
& op1(e11,e11) = e11
& op1(e11,e11) = e11 )
| ( op1(e10,e10) != e10
& op1(e10,e11) = e11
& op1(e11,e10) = e11 )
| ( op1(e13,e13) != e13
& op1(e13,e10) = e10
& op1(e10,e13) = e10 )
| ( op1(e12,e12) != e12
& op1(e12,e10) = e10
& op1(e10,e12) = e10 )
| ( op1(e11,e11) != e11
& op1(e11,e10) = e10
& op1(e10,e11) = e10 )
| ( op1(e10,e10) != e10
& op1(e10,e10) = e10
& op1(e10,e10) = e10 ) )
& ( op1(e13,e13) = e13
| op1(e13,e13) != e13 )
& ( op1(e13,e12) = e13
| op1(e13,e13) != e12 )
& ( op1(e13,e11) = e13
| op1(e13,e13) != e11 )
& ( op1(e13,e10) = e13
| op1(e13,e13) != e10 )
& ( op1(e12,e13) = e12
| op1(e12,e12) != e13 )
& ( op1(e12,e12) = e12
| op1(e12,e12) != e12 )
& ( op1(e12,e11) = e12
| op1(e12,e12) != e11 )
& ( op1(e12,e10) = e12
| op1(e12,e12) != e10 )
& ( op1(e11,e13) = e11
| op1(e11,e11) != e13 )
& ( op1(e11,e12) = e11
| op1(e11,e11) != e12 )
& ( op1(e11,e11) = e11
| op1(e11,e11) != e11 )
& ( op1(e11,e10) = e11
| op1(e11,e11) != e10 )
& ( op1(e10,e13) = e10
| op1(e10,e10) != e13 )
& ( op1(e10,e12) = e10
| op1(e10,e10) != e12 )
& ( op1(e10,e11) = e10
| op1(e10,e10) != e11 )
& ( op1(e10,e10) = e10
| op1(e10,e10) != e10 )
& ( op1(e13,e13) = e13
| op1(e12,e12) = e12
| op1(e11,e11) = e11
| op1(e10,e10) = e10 ) ),
file('theBenchmark.p',ax10) ).
fof(ax11,axiom,
( ( ( op2(e23,e23) != e23
& op2(e23,e23) = e23
& op2(e23,e23) = e23 )
| ( op2(e22,e22) != e22
& op2(e22,e23) = e23
& op2(e23,e22) = e23 )
| ( op2(e21,e21) != e21
& op2(e21,e23) = e23
& op2(e23,e21) = e23 )
| ( op2(e20,e20) != e20
& op2(e20,e23) = e23
& op2(e23,e20) = e23 )
| ( op2(e23,e23) != e23
& op2(e23,e22) = e22
& op2(e22,e23) = e22 )
| ( op2(e22,e22) != e22
& op2(e22,e22) = e22
& op2(e22,e22) = e22 )
| ( op2(e21,e21) != e21
& op2(e21,e22) = e22
& op2(e22,e21) = e22 )
| ( op2(e20,e20) != e20
& op2(e20,e22) = e22
& op2(e22,e20) = e22 )
| ( op2(e23,e23) != e23
& op2(e23,e21) = e21
& op2(e21,e23) = e21 )
| ( op2(e22,e22) != e22
& op2(e22,e21) = e21
& op2(e21,e22) = e21 )
| ( op2(e21,e21) != e21
& op2(e21,e21) = e21
& op2(e21,e21) = e21 )
| ( op2(e20,e20) != e20
& op2(e20,e21) = e21
& op2(e21,e20) = e21 )
| ( op2(e23,e23) != e23
& op2(e23,e20) = e20
& op2(e20,e23) = e20 )
| ( op2(e22,e22) != e22
& op2(e22,e20) = e20
& op2(e20,e22) = e20 )
| ( op2(e21,e21) != e21
& op2(e21,e20) = e20
& op2(e20,e21) = e20 )
| ( op2(e20,e20) != e20
& op2(e20,e20) = e20
& op2(e20,e20) = e20 ) )
& ( op2(e23,e23) = e23
| op2(e23,e23) != e23 )
& ( op2(e23,e22) = e23
| op2(e23,e23) != e22 )
& ( op2(e23,e21) = e23
| op2(e23,e23) != e21 )
& ( op2(e23,e20) = e23
| op2(e23,e23) != e20 )
& ( op2(e22,e23) = e22
| op2(e22,e22) != e23 )
& ( op2(e22,e22) = e22
| op2(e22,e22) != e22 )
& ( op2(e22,e21) = e22
| op2(e22,e22) != e21 )
& ( op2(e22,e20) = e22
| op2(e22,e22) != e20 )
& ( op2(e21,e23) = e21
| op2(e21,e21) != e23 )
& ( op2(e21,e22) = e21
| op2(e21,e21) != e22 )
& ( op2(e21,e21) = e21
| op2(e21,e21) != e21 )
& ( op2(e21,e20) = e21
| op2(e21,e21) != e20 )
& ( op2(e20,e23) = e20
| op2(e20,e20) != e23 )
& ( op2(e20,e22) = e20
| op2(e20,e20) != e22 )
& ( op2(e20,e21) = e20
| op2(e20,e20) != e21 )
& ( op2(e20,e20) = e20
| op2(e20,e20) != e20 )
& ( op2(e23,e23) = e23
| op2(e22,e22) = e22
| op2(e21,e21) = e21
| op2(e20,e20) = e20 ) ),
file('theBenchmark.p',ax11) ).
fof(ax12,axiom,
( e12 = op1(op1(op1(e13,e13),op1(e13,e13)),e13)
& e11 = op1(op1(e13,e13),op1(e13,e13))
& e10 = op1(e13,e13) ),
file('theBenchmark.p',ax12) ).
fof(ax13,axiom,
( e22 = op2(op2(op2(e23,e23),op2(e23,e23)),e23)
& e21 = op2(op2(e23,e23),op2(e23,e23))
& e20 = op2(e23,e23) ),
file('theBenchmark.p',ax13) ).
fof(ax17,axiom,
( h4(e12) = op2(op2(op2(e23,e23),op2(e23,e23)),e23)
& h4(e11) = op2(op2(e23,e23),op2(e23,e23))
& h4(e10) = op2(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_23,plain,
( op1(e11,e10) = e13
| op1(e11,e10) = e12
| op1(e11,e10) = e11
| op1(e11,e10) = 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_40,plain,
( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| op1(e10,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_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_48,plain,
( op1(e13,e11) = e12
| op1(e12,e11) = e12
| op1(e11,e11) = e12
| op1(e10,e11) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_50,plain,
( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| op1(e10,e11) = e13 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_52,plain,
( op1(e13,e12) = e10
| op1(e12,e12) = e10
| op1(e11,e12) = e10
| op1(e10,e12) = e10 ),
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_61,plain,
( op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_62,plain,
( op1(e13,e13) = e11
| op1(e12,e13) = e11
| op1(e11,e13) = e11
| op1(e10,e13) = e11 ),
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_71,plain,
( op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e21
| op2(e21,e20) = 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_88,plain,
( op2(e23,e20) = e22
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| op2(e20,e20) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_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_96,plain,
( op2(e23,e21) = e22
| op2(e22,e21) = e22
| op2(e21,e21) = e22
| op2(e20,e21) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_98,plain,
( op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e21,e21) = e23
| op2(e20,e21) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_100,plain,
( op2(e23,e22) = e20
| op2(e22,e22) = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 ),
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_109,plain,
( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_110,plain,
( op2(e23,e23) = e21
| op2(e22,e23) = e21
| op2(e21,e23) = e21
| op2(e20,e23) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_115,plain,
op1(e11,e10) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_122,plain,
op1(e13,e10) != op1(e11,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_123,plain,
op1(e11,e10) != op1(e13,e10),
inference(copy,[status(thm)],[c_122]) ).
cnf(c_148,plain,
op1(e11,e13) != op1(e10,e13),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_151,plain,
op1(e13,e13) != op1(e10,e13),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_152,plain,
op1(e10,e13) != op1(e13,e13),
inference(copy,[status(thm)],[c_151]) ).
cnf(c_162,plain,
op1(e10,e13) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_163,plain,
op1(e10,e10) != op1(e10,e13),
inference(copy,[status(thm)],[c_162]) ).
cnf(c_173,plain,
op1(e11,e13) != op1(e11,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_174,plain,
op1(e11,e10) != op1(e11,e13),
inference(copy,[status(thm)],[c_173]) ).
cnf(c_177,plain,
op1(e11,e13) != op1(e11,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_178,plain,
op1(e11,e11) != op1(e11,e13),
inference(copy,[status(thm)],[c_177]) ).
cnf(c_192,plain,
op1(e13,e11) != op1(e13,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_193,plain,
op1(e13,e12) != op1(e13,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_194,plain,
op1(e13,e10) != op1(e13,e12),
inference(copy,[status(thm)],[c_193]) ).
cnf(c_201,plain,
op1(e13,e13) != op1(e13,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_202,plain,
op1(e13,e12) != op1(e13,e13),
inference(copy,[status(thm)],[c_201]) ).
cnf(c_203,plain,
op2(e21,e20) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_210,plain,
op2(e23,e20) != op2(e21,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_211,plain,
op2(e21,e20) != op2(e23,e20),
inference(copy,[status(thm)],[c_210]) ).
cnf(c_236,plain,
op2(e21,e23) != op2(e20,e23),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_239,plain,
op2(e23,e23) != op2(e20,e23),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_240,plain,
op2(e20,e23) != op2(e23,e23),
inference(copy,[status(thm)],[c_239]) ).
cnf(c_250,plain,
op2(e20,e23) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_251,plain,
op2(e20,e20) != op2(e20,e23),
inference(copy,[status(thm)],[c_250]) ).
cnf(c_261,plain,
op2(e21,e23) != op2(e21,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_262,plain,
op2(e21,e20) != op2(e21,e23),
inference(copy,[status(thm)],[c_261]) ).
cnf(c_265,plain,
op2(e21,e23) != op2(e21,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_266,plain,
op2(e21,e21) != op2(e21,e23),
inference(copy,[status(thm)],[c_265]) ).
cnf(c_280,plain,
op2(e23,e21) != op2(e23,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_281,plain,
op2(e23,e22) != op2(e23,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_282,plain,
op2(e23,e20) != op2(e23,e22),
inference(copy,[status(thm)],[c_281]) ).
cnf(c_289,plain,
op2(e23,e23) != op2(e23,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_290,plain,
op2(e23,e22) != op2(e23,e23),
inference(copy,[status(thm)],[c_289]) ).
cnf(c_291,plain,
e11 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_292,plain,
e12 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_293,plain,
e10 != e12,
inference(copy,[status(thm)],[c_292]) ).
cnf(c_294,plain,
e13 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_295,plain,
e10 != e13,
inference(copy,[status(thm)],[c_294]) ).
cnf(c_296,plain,
e12 != e11,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_297,plain,
e11 != e12,
inference(copy,[status(thm)],[c_296]) ).
cnf(c_298,plain,
e13 != e11,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_299,plain,
e11 != e13,
inference(copy,[status(thm)],[c_298]) ).
cnf(c_300,plain,
e13 != e12,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_301,plain,
e12 != e13,
inference(copy,[status(thm)],[c_300]) ).
cnf(c_302,plain,
e21 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_303,plain,
e22 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_304,plain,
e20 != e22,
inference(copy,[status(thm)],[c_303]) ).
cnf(c_305,plain,
e23 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_306,plain,
e20 != e23,
inference(copy,[status(thm)],[c_305]) ).
cnf(c_307,plain,
e22 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_308,plain,
e21 != e22,
inference(copy,[status(thm)],[c_307]) ).
cnf(c_309,plain,
e23 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_310,plain,
e21 != e23,
inference(copy,[status(thm)],[c_309]) ).
cnf(c_311,plain,
e23 != e22,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_312,plain,
e22 != e23,
inference(copy,[status(thm)],[c_311]) ).
cnf(c_341,plain,
( op1(e10,e11) = e10
| op1(e10,e10) != e11 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_346,plain,
( op1(e11,e13) = e11
| op1(e11,e11) != e13 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_349,plain,
( op1(e12,e13) = e12
| op1(e12,e12) != e13 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_350,plain,
( op1(e13,e10) = e13
| op1(e13,e13) != e10 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_597,plain,
( op2(e20,e21) = e20
| op2(e20,e20) != e21 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_602,plain,
( op2(e21,e23) = e21
| op2(e21,e21) != e23 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_605,plain,
( op2(e22,e23) = e22
| op2(e22,e22) != e23 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_606,plain,
( op2(e23,e20) = e23
| op2(e23,e23) != e20 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_852,plain,
op1(e13,e13) = e10,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_853,plain,
op1(op1(e13,e13),op1(e13,e13)) = e11,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_2361,plain,
op1(e10,op1(e13,e13)) = e11,
inference(paramod,[status(thm)],[c_852,c_853]) ).
cnf(c_854,plain,
op1(e10,e10) = e11,
inference(paramod,[status(thm)],[c_852,c_2361]) ).
cnf(c_855,plain,
op1(op1(op1(e13,e13),op1(e13,e13)),e13) = e12,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_2362,plain,
op1(op1(e10,op1(e13,e13)),e13) = e12,
inference(paramod,[status(thm)],[c_852,c_855]) ).
cnf(c_2363,plain,
op1(op1(e10,e10),e13) = e12,
inference(paramod,[status(thm)],[c_852,c_2362]) ).
cnf(c_856,plain,
op1(e11,e13) = e12,
inference(paramod,[status(thm)],[c_854,c_2363]) ).
cnf(c_857,plain,
op2(e23,e23) = e20,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_858,plain,
op2(op2(e23,e23),op2(e23,e23)) = e21,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_2364,plain,
op2(e20,op2(e23,e23)) = e21,
inference(paramod,[status(thm)],[c_857,c_858]) ).
cnf(c_859,plain,
op2(e20,e20) = e21,
inference(paramod,[status(thm)],[c_857,c_2364]) ).
cnf(c_860,plain,
op2(op2(op2(e23,e23),op2(e23,e23)),e23) = e22,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_2365,plain,
op2(op2(e20,op2(e23,e23)),e23) = e22,
inference(paramod,[status(thm)],[c_857,c_860]) ).
cnf(c_2366,plain,
op2(op2(e20,e20),e23) = e22,
inference(paramod,[status(thm)],[c_857,c_2365]) ).
cnf(c_861,plain,
op2(e21,e23) = e22,
inference(paramod,[status(thm)],[c_859,c_2366]) ).
cnf(c_877,plain,
h4(e13) = e23,
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_878,plain,
h4(e10) = op2(e23,e23),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_879,plain,
h4(e10) = e20,
inference(paramod,[status(thm)],[c_857,c_878]) ).
cnf(c_880,plain,
h4(e11) = op2(op2(e23,e23),op2(e23,e23)),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_2367,plain,
h4(e11) = op2(e20,op2(e23,e23)),
inference(paramod,[status(thm)],[c_857,c_880]) ).
cnf(c_2368,plain,
h4(e11) = op2(e20,e20),
inference(paramod,[status(thm)],[c_857,c_2367]) ).
cnf(c_881,plain,
h4(e11) = e21,
inference(paramod,[status(thm)],[c_859,c_2368]) ).
cnf(c_882,plain,
h4(e12) = op2(op2(op2(e23,e23),op2(e23,e23)),e23),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_2369,plain,
h4(e12) = op2(op2(e20,op2(e23,e23)),e23),
inference(paramod,[status(thm)],[c_857,c_882]) ).
cnf(c_2370,plain,
h4(e12) = op2(op2(e20,e20),e23),
inference(paramod,[status(thm)],[c_857,c_2369]) ).
cnf(c_2371,plain,
h4(e12) = op2(e21,e23),
inference(paramod,[status(thm)],[c_859,c_2370]) ).
cnf(c_883,plain,
h4(e12) = e22,
inference(paramod,[status(thm)],[c_861,c_2371]) ).
cnf(c_1907,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_2372,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(e11) != op2(h4(e10),h4(e10)) ),
inference(paramod,[status(thm)],[c_854,c_1907]) ).
cnf(c_2373,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))
| e21 != op2(h4(e10),h4(e10)) ),
inference(paramod,[status(thm)],[c_881,c_2372]) ).
cnf(c_2374,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))
| e21 != op2(e20,h4(e10)) ),
inference(paramod,[status(thm)],[c_879,c_2373]) ).
cnf(c_2375,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))
| e21 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_879,c_2374]) ).
cnf(c_2376,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))
| e21 != e21 ),
inference(paramod,[status(thm)],[c_859,c_2375]) ).
cnf(c_2377,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(e20,h4(e11))
| e21 != e21 ),
inference(paramod,[status(thm)],[c_879,c_2376]) ).
cnf(c_2378,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(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_881,c_2377]) ).
cnf(c_2379,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(e20,h4(e12))
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_879,c_2378]) ).
cnf(c_2380,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(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_883,c_2379]) ).
cnf(c_2381,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(e20,h4(e13))
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_879,c_2380]) ).
cnf(c_2382,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(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_877,c_2381]) ).
cnf(c_2383,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(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_881,c_2382]) ).
cnf(c_2384,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,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_879,c_2383]) ).
cnf(c_2385,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,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_881,c_2384]) ).
cnf(c_2386,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,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_881,c_2385]) ).
cnf(c_2387,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,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_881,c_2386]) ).
cnf(c_2388,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,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_883,c_2387]) ).
cnf(c_2389,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,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_856,c_2388]) ).
cnf(c_2390,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,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_883,c_2389]) ).
cnf(c_2391,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,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_881,c_2390]) ).
cnf(c_2392,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,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_877,c_2391]) ).
cnf(c_2393,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,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_861,c_2392]) ).
cnf(c_2394,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,e20)
| h4(op1(e10,e13)) != op2(e20,e23)
| h4(op1(e10,e12)) != op2(e20,e22)
| h4(op1(e10,e11)) != op2(e20,e21)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_883,c_2393]) ).
cnf(c_2395,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,e20)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_879,c_2394]) ).
cnf(c_2396,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,e20)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_883,c_2395]) ).
cnf(c_2397,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,e20)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_881,c_2396]) ).
cnf(c_2398,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,e20)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_883,c_2397]) ).
cnf(c_2399,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,e20)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_883,c_2398]) ).
cnf(c_2400,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,e20)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_883,c_2399]) ).
cnf(c_2401,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,e20)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_877,c_2400]) ).
cnf(c_2402,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,e20)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_877,c_2401]) ).
cnf(c_2403,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,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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_879,c_2402]) ).
cnf(c_2404,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,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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_877,c_2403]) ).
cnf(c_2405,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,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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_881,c_2404]) ).
cnf(c_2406,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,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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_877,c_2405]) ).
cnf(c_2407,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,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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_883,c_2406]) ).
cnf(c_2408,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| h4(e10) != e20
| h4(e10) != 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,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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_852,c_2407]) ).
cnf(c_2409,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| h4(e10) != e20
| e20 != 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,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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_879,c_2408]) ).
cnf(c_2410,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| h4(e10) != e20
| e20 != op2(e23,h4(e13))
| 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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_877,c_2409]) ).
cnf(c_2411,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| h4(e10) != e20
| e20 != op2(e23,e23)
| 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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_877,c_2410]) ).
cnf(c_2412,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| h4(e10) != e20
| 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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_857,c_2411]) ).
cnf(c_2413,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| h4(e11) != e21
| e20 != e20
| 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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_879,c_2412]) ).
cnf(c_2414,negated_conjecture,
( h4(e13) != e23
| h4(e12) != e22
| e21 != e21
| e20 != e20
| 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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_881,c_2413]) ).
cnf(c_2415,negated_conjecture,
( h4(e13) != e23
| e22 != e22
| e21 != e21
| e20 != e20
| 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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_883,c_2414]) ).
cnf(c_2416,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20
| 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)
| e22 != 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)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_877,c_2415]) ).
cnf(c_2417,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20
| 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)
| e22 != 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) ),
inference(copy,[status(thm)],[c_2416]) ).
cnf(c_2418,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20
| 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,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) ),
inference(copy,[status(thm)],[c_2417]) ).
cnf(c_2419,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| 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,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) ),
inference(copy,[status(thm)],[c_2418]) ).
cnf(c_2420,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| 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,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) ),
inference(copy,[status(thm)],[c_2419]) ).
cnf(c_2421,negated_conjecture,
( e23 != e23
| e22 != e22
| 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,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) ),
inference(copy,[status(thm)],[c_2420]) ).
cnf(c_2422,negated_conjecture,
( e23 != e23
| 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,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) ),
inference(copy,[status(thm)],[c_2421]) ).
cnf(c_1908,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,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) ),
inference(copy,[status(thm)],[c_2422]) ).
cnf(c_2423,plain,
( op1(e13,e10) = e13
| e10 != e10 ),
inference(paramod,[status(thm)],[c_852,c_350]) ).
cnf(c_2137,plain,
op1(e13,e10) = e13,
inference(copy,[status(thm)],[c_2423]) ).
cnf(c_2139,plain,
op1(e13,e12) != e10,
inference(paramod,[status(thm)],[c_852,c_202]) ).
cnf(c_2142,plain,
op1(e10,e13) != e10,
inference(paramod,[status(thm)],[c_852,c_152]) ).
cnf(c_2424,plain,
( op1(e13,e13) = e11
| op1(e12,e13) = e11
| e12 = e11
| op1(e10,e13) = e11 ),
inference(paramod,[status(thm)],[c_856,c_62]) ).
cnf(c_2425,plain,
( e10 = e11
| op1(e12,e13) = e11
| e12 = e11
| op1(e10,e13) = e11 ),
inference(paramod,[status(thm)],[c_852,c_2424]) ).
cnf(c_2426,plain,
( e10 = e11
| op1(e12,e13) = e11
| e11 = e12
| op1(e10,e13) = e11 ),
inference(copy,[status(thm)],[c_2425]) ).
cnf(c_2427,plain,
( e11 = e10
| op1(e12,e13) = e11
| e11 = e12
| op1(e10,e13) = e11 ),
inference(copy,[status(thm)],[c_2426]) ).
cnf(c_2428,plain,
( e11 = e10
| op1(e12,e13) = e11
| op1(e10,e13) = e11 ),
inference(resolve,[status(thm)],[c_297,c_2427]) ).
cnf(c_2145,plain,
( op1(e12,e13) = e11
| op1(e10,e13) = e11 ),
inference(resolve,[status(thm)],[c_291,c_2428]) ).
cnf(c_2429,plain,
( op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| e13 = e11 ),
inference(paramod,[status(thm)],[c_2137,c_61]) ).
cnf(c_2430,plain,
( e10 = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| e13 = e11 ),
inference(paramod,[status(thm)],[c_852,c_2429]) ).
cnf(c_2431,plain,
( e10 = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| e11 = e13 ),
inference(copy,[status(thm)],[c_2430]) ).
cnf(c_2432,plain,
( e11 = e10
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| e11 = e13 ),
inference(copy,[status(thm)],[c_2431]) ).
cnf(c_2433,plain,
( e11 = e10
| op1(e13,e12) = e11
| op1(e13,e11) = e11 ),
inference(resolve,[status(thm)],[c_299,c_2432]) ).
cnf(c_2146,plain,
( op1(e13,e12) = e11
| op1(e13,e11) = e11 ),
inference(resolve,[status(thm)],[c_291,c_2433]) ).
cnf(c_2434,plain,
( op1(e10,e11) = e10
| e11 != e11 ),
inference(paramod,[status(thm)],[c_854,c_341]) ).
cnf(c_2147,plain,
op1(e10,e11) = e10,
inference(copy,[status(thm)],[c_2434]) ).
cnf(c_2435,plain,
e11 != op1(e10,e13),
inference(paramod,[status(thm)],[c_854,c_163]) ).
cnf(c_2148,plain,
op1(e10,e13) != e11,
inference(copy,[status(thm)],[c_2435]) ).
cnf(c_2151,plain,
op1(e11,e10) != e11,
inference(paramod,[status(thm)],[c_854,c_115]) ).
cnf(c_2436,plain,
( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_854,c_40]) ).
cnf(c_2437,plain,
( e13 = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_2137,c_2436]) ).
cnf(c_2438,plain,
( e12 = e13
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| e11 = e12 ),
inference(copy,[status(thm)],[c_2437]) ).
cnf(c_2439,plain,
( e12 = e13
| op1(e12,e10) = e12
| op1(e11,e10) = e12 ),
inference(resolve,[status(thm)],[c_297,c_2438]) ).
cnf(c_2153,plain,
( op1(e12,e10) = e12
| op1(e11,e10) = e12 ),
inference(resolve,[status(thm)],[c_301,c_2439]) ).
cnf(c_2440,plain,
( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_854,c_39]) ).
cnf(c_2441,plain,
( op1(e10,e13) = e12
| op1(e10,e12) = e12
| e10 = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_2147,c_2440]) ).
cnf(c_2442,plain,
( op1(e10,e13) = e12
| op1(e10,e12) = e12
| e10 = e12 ),
inference(resolve,[status(thm)],[c_297,c_2441]) ).
cnf(c_2154,plain,
( op1(e10,e13) = e12
| op1(e10,e12) = e12 ),
inference(resolve,[status(thm)],[c_293,c_2442]) ).
cnf(c_2443,plain,
( e12 = e11
| op1(e11,e11) != e13 ),
inference(paramod,[status(thm)],[c_856,c_346]) ).
cnf(c_2444,plain,
( e11 = e12
| op1(e11,e11) != e13 ),
inference(copy,[status(thm)],[c_2443]) ).
cnf(c_2173,plain,
op1(e11,e11) != e13,
inference(resolve,[status(thm)],[c_297,c_2444]) ).
cnf(c_2175,plain,
op1(e11,e11) != e12,
inference(paramod,[status(thm)],[c_856,c_178]) ).
cnf(c_2176,plain,
op1(e11,e10) != e12,
inference(paramod,[status(thm)],[c_856,c_174]) ).
cnf(c_2445,plain,
e12 != op1(e10,e13),
inference(paramod,[status(thm)],[c_856,c_148]) ).
cnf(c_2178,plain,
op1(e10,e13) != e12,
inference(copy,[status(thm)],[c_2445]) ).
cnf(c_2446,plain,
( op2(e23,e20) = e23
| e20 != e20 ),
inference(paramod,[status(thm)],[c_857,c_606]) ).
cnf(c_2182,plain,
op2(e23,e20) = e23,
inference(copy,[status(thm)],[c_2446]) ).
cnf(c_2184,plain,
op2(e23,e22) != e20,
inference(paramod,[status(thm)],[c_857,c_290]) ).
cnf(c_2187,plain,
op2(e20,e23) != e20,
inference(paramod,[status(thm)],[c_857,c_240]) ).
cnf(c_2447,plain,
( op2(e23,e23) = e21
| op2(e22,e23) = e21
| e22 = e21
| op2(e20,e23) = e21 ),
inference(paramod,[status(thm)],[c_861,c_110]) ).
cnf(c_2448,plain,
( e20 = e21
| op2(e22,e23) = e21
| e22 = e21
| op2(e20,e23) = e21 ),
inference(paramod,[status(thm)],[c_857,c_2447]) ).
cnf(c_2449,plain,
( e20 = e21
| op2(e22,e23) = e21
| e21 = e22
| op2(e20,e23) = e21 ),
inference(copy,[status(thm)],[c_2448]) ).
cnf(c_2450,plain,
( e21 = e20
| op2(e22,e23) = e21
| e21 = e22
| op2(e20,e23) = e21 ),
inference(copy,[status(thm)],[c_2449]) ).
cnf(c_2451,plain,
( e21 = e20
| op2(e22,e23) = e21
| op2(e20,e23) = e21 ),
inference(resolve,[status(thm)],[c_308,c_2450]) ).
cnf(c_2190,plain,
( op2(e22,e23) = e21
| op2(e20,e23) = e21 ),
inference(resolve,[status(thm)],[c_302,c_2451]) ).
cnf(c_2452,plain,
( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| e23 = e21 ),
inference(paramod,[status(thm)],[c_2182,c_109]) ).
cnf(c_2453,plain,
( e20 = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| e23 = e21 ),
inference(paramod,[status(thm)],[c_857,c_2452]) ).
cnf(c_2454,plain,
( e20 = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| e21 = e23 ),
inference(copy,[status(thm)],[c_2453]) ).
cnf(c_2455,plain,
( e21 = e20
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| e21 = e23 ),
inference(copy,[status(thm)],[c_2454]) ).
cnf(c_2456,plain,
( e21 = e20
| op2(e23,e22) = e21
| op2(e23,e21) = e21 ),
inference(resolve,[status(thm)],[c_310,c_2455]) ).
cnf(c_2191,plain,
( op2(e23,e22) = e21
| op2(e23,e21) = e21 ),
inference(resolve,[status(thm)],[c_302,c_2456]) ).
cnf(c_2457,plain,
( op2(e20,e21) = e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_859,c_597]) ).
cnf(c_2192,plain,
op2(e20,e21) = e20,
inference(copy,[status(thm)],[c_2457]) ).
cnf(c_2458,plain,
e21 != op2(e20,e23),
inference(paramod,[status(thm)],[c_859,c_251]) ).
cnf(c_2193,plain,
op2(e20,e23) != e21,
inference(copy,[status(thm)],[c_2458]) ).
cnf(c_2196,plain,
op2(e21,e20) != e21,
inference(paramod,[status(thm)],[c_859,c_203]) ).
cnf(c_2459,plain,
( op2(e23,e20) = e22
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_859,c_88]) ).
cnf(c_2460,plain,
( e23 = e22
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_2182,c_2459]) ).
cnf(c_2461,plain,
( e22 = e23
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| e21 = e22 ),
inference(copy,[status(thm)],[c_2460]) ).
cnf(c_2462,plain,
( e22 = e23
| op2(e22,e20) = e22
| op2(e21,e20) = e22 ),
inference(resolve,[status(thm)],[c_308,c_2461]) ).
cnf(c_2198,plain,
( op2(e22,e20) = e22
| op2(e21,e20) = e22 ),
inference(resolve,[status(thm)],[c_312,c_2462]) ).
cnf(c_2463,plain,
( op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_859,c_87]) ).
cnf(c_2464,plain,
( op2(e20,e23) = e22
| op2(e20,e22) = e22
| e20 = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_2192,c_2463]) ).
cnf(c_2465,plain,
( op2(e20,e23) = e22
| op2(e20,e22) = e22
| e20 = e22 ),
inference(resolve,[status(thm)],[c_308,c_2464]) ).
cnf(c_2199,plain,
( op2(e20,e23) = e22
| op2(e20,e22) = e22 ),
inference(resolve,[status(thm)],[c_304,c_2465]) ).
cnf(c_2466,plain,
( e22 = e21
| op2(e21,e21) != e23 ),
inference(paramod,[status(thm)],[c_861,c_602]) ).
cnf(c_2467,plain,
( e21 = e22
| op2(e21,e21) != e23 ),
inference(copy,[status(thm)],[c_2466]) ).
cnf(c_2218,plain,
op2(e21,e21) != e23,
inference(resolve,[status(thm)],[c_308,c_2467]) ).
cnf(c_2220,plain,
op2(e21,e21) != e22,
inference(paramod,[status(thm)],[c_861,c_266]) ).
cnf(c_2221,plain,
op2(e21,e20) != e22,
inference(paramod,[status(thm)],[c_861,c_262]) ).
cnf(c_2468,plain,
e22 != op2(e20,e23),
inference(paramod,[status(thm)],[c_861,c_236]) ).
cnf(c_2223,plain,
op2(e20,e23) != e22,
inference(copy,[status(thm)],[c_2468]) ).
cnf(c_2469,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,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(e10) != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_2147,c_1908]) ).
cnf(c_2470,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,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)
| e20 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_879,c_2469]) ).
cnf(c_2471,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,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)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2192,c_2470]) ).
cnf(c_2472,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(e13) != 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,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)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2137,c_2471]) ).
cnf(c_2473,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| e23 != 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,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)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_877,c_2472]) ).
cnf(c_2474,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| e23 != e23
| 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,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)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2182,c_2473]) ).
cnf(c_2475,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| e23 != e23
| 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,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) ),
inference(copy,[status(thm)],[c_2474]) ).
cnf(c_2227,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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,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) ),
inference(copy,[status(thm)],[c_2475]) ).
cnf(c_2476,plain,
e13 != op1(e13,e12),
inference(paramod,[status(thm)],[c_2137,c_194]) ).
cnf(c_2269,plain,
op1(e13,e12) != e13,
inference(copy,[status(thm)],[c_2476]) ).
cnf(c_2270,plain,
op1(e13,e11) != e13,
inference(paramod,[status(thm)],[c_2137,c_192]) ).
cnf(c_2272,plain,
op1(e11,e10) != e13,
inference(paramod,[status(thm)],[c_2137,c_123]) ).
cnf(c_2273,plain,
( op1(e12,e12) = e10
| op1(e11,e12) = e10
| op1(e10,e12) = e10 ),
inference(resolve,[status(thm)],[c_2139,c_52]) ).
cnf(c_2477,plain,
( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11 ),
inference(resolve,[status(thm)],[c_2142,c_22]) ).
cnf(c_2478,plain,
( op1(e10,e13) = e13
| op1(e10,e13) = e12 ),
inference(resolve,[status(thm)],[c_2148,c_2477]) ).
cnf(c_2278,plain,
op1(e10,e13) = e13,
inference(resolve,[status(thm)],[c_2178,c_2478]) ).
cnf(c_2479,plain,
( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_2147,c_50]) ).
cnf(c_2480,plain,
( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13 ),
inference(resolve,[status(thm)],[c_295,c_2479]) ).
cnf(c_2481,plain,
( op1(e13,e11) = e13
| op1(e12,e11) = e13 ),
inference(resolve,[status(thm)],[c_2173,c_2480]) ).
cnf(c_2283,plain,
op1(e12,e11) = e13,
inference(resolve,[status(thm)],[c_2270,c_2481]) ).
cnf(c_2482,plain,
( op1(e13,e11) = e12
| op1(e12,e11) = e12
| op1(e11,e11) = e12
| e10 = e12 ),
inference(paramod,[status(thm)],[c_2147,c_48]) ).
cnf(c_2483,plain,
( op1(e13,e11) = e12
| e13 = e12
| op1(e11,e11) = e12
| e10 = e12 ),
inference(paramod,[status(thm)],[c_2283,c_2482]) ).
cnf(c_2484,plain,
( op1(e13,e11) = e12
| e12 = e13
| op1(e11,e11) = e12
| e10 = e12 ),
inference(copy,[status(thm)],[c_2483]) ).
cnf(c_2485,plain,
( op1(e13,e11) = e12
| e12 = e13
| op1(e11,e11) = e12 ),
inference(resolve,[status(thm)],[c_293,c_2484]) ).
cnf(c_2486,plain,
( op1(e13,e11) = e12
| e12 = e13 ),
inference(resolve,[status(thm)],[c_2175,c_2485]) ).
cnf(c_2284,plain,
op1(e13,e11) = e12,
inference(resolve,[status(thm)],[c_301,c_2486]) ).
cnf(c_2487,plain,
( op1(e13,e11) = e11
| op1(e12,e11) = e11
| op1(e11,e11) = e11
| e10 = e11 ),
inference(paramod,[status(thm)],[c_2147,c_46]) ).
cnf(c_2488,plain,
( op1(e13,e11) = e11
| e13 = e11
| op1(e11,e11) = e11
| e10 = e11 ),
inference(paramod,[status(thm)],[c_2283,c_2487]) ).
cnf(c_2489,plain,
( e12 = e11
| e13 = e11
| op1(e11,e11) = e11
| e10 = e11 ),
inference(paramod,[status(thm)],[c_2284,c_2488]) ).
cnf(c_2490,plain,
( e12 = e11
| e13 = e11
| op1(e11,e11) = e11
| e11 = e10 ),
inference(copy,[status(thm)],[c_2489]) ).
cnf(c_2491,plain,
( e12 = e11
| e11 = e13
| op1(e11,e11) = e11
| e11 = e10 ),
inference(copy,[status(thm)],[c_2490]) ).
cnf(c_2492,plain,
( e11 = e12
| e11 = e13
| op1(e11,e11) = e11
| e11 = e10 ),
inference(copy,[status(thm)],[c_2491]) ).
cnf(c_2493,plain,
( e11 = e12
| e11 = e13
| op1(e11,e11) = e11 ),
inference(resolve,[status(thm)],[c_291,c_2492]) ).
cnf(c_2494,plain,
( e11 = e12
| op1(e11,e11) = e11 ),
inference(resolve,[status(thm)],[c_299,c_2493]) ).
cnf(c_2285,plain,
op1(e11,e11) = e11,
inference(resolve,[status(thm)],[c_297,c_2494]) ).
cnf(c_2495,plain,
( op1(e12,e13) = e11
| e13 = e11 ),
inference(paramod,[status(thm)],[c_2278,c_2145]) ).
cnf(c_2496,plain,
( op1(e12,e13) = e11
| e11 = e13 ),
inference(copy,[status(thm)],[c_2495]) ).
cnf(c_2286,plain,
op1(e12,e13) = e11,
inference(resolve,[status(thm)],[c_299,c_2496]) ).
cnf(c_2497,plain,
( op1(e11,e10) = e13
| op1(e11,e10) = e12
| op1(e11,e10) = e10 ),
inference(resolve,[status(thm)],[c_2151,c_23]) ).
cnf(c_2498,plain,
( op1(e11,e10) = e13
| op1(e11,e10) = e10 ),
inference(resolve,[status(thm)],[c_2176,c_2497]) ).
cnf(c_2290,plain,
op1(e11,e10) = e10,
inference(resolve,[status(thm)],[c_2272,c_2498]) ).
cnf(c_2499,plain,
( op1(e12,e10) = e12
| e10 = e12 ),
inference(paramod,[status(thm)],[c_2290,c_2153]) ).
cnf(c_2293,plain,
op1(e12,e10) = e12,
inference(resolve,[status(thm)],[c_293,c_2499]) ).
cnf(c_2500,plain,
( e11 = e12
| op1(e12,e12) != e13 ),
inference(paramod,[status(thm)],[c_2286,c_349]) ).
cnf(c_2294,plain,
op1(e12,e12) != e13,
inference(resolve,[status(thm)],[c_297,c_2500]) ).
cnf(c_2501,plain,
( e13 = e12
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_2278,c_2154]) ).
cnf(c_2502,plain,
( e12 = e13
| op1(e10,e12) = e12 ),
inference(copy,[status(thm)],[c_2501]) ).
cnf(c_2295,plain,
op1(e10,e12) = e12,
inference(resolve,[status(thm)],[c_301,c_2502]) ).
cnf(c_2503,plain,
e23 != op2(e23,e22),
inference(paramod,[status(thm)],[c_2182,c_282]) ).
cnf(c_2297,plain,
op2(e23,e22) != e23,
inference(copy,[status(thm)],[c_2503]) ).
cnf(c_2298,plain,
op2(e23,e21) != e23,
inference(paramod,[status(thm)],[c_2182,c_280]) ).
cnf(c_2300,plain,
op2(e21,e20) != e23,
inference(paramod,[status(thm)],[c_2182,c_211]) ).
cnf(c_2301,plain,
( op2(e22,e22) = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 ),
inference(resolve,[status(thm)],[c_2184,c_100]) ).
cnf(c_2504,plain,
( op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21 ),
inference(resolve,[status(thm)],[c_2187,c_70]) ).
cnf(c_2505,plain,
( op2(e20,e23) = e23
| op2(e20,e23) = e22 ),
inference(resolve,[status(thm)],[c_2193,c_2504]) ).
cnf(c_2306,plain,
op2(e20,e23) = e23,
inference(resolve,[status(thm)],[c_2223,c_2505]) ).
cnf(c_2506,plain,
( op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e21,e21) = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_2192,c_98]) ).
cnf(c_2507,plain,
( op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e21,e21) = e23 ),
inference(resolve,[status(thm)],[c_306,c_2506]) ).
cnf(c_2508,plain,
( op2(e23,e21) = e23
| op2(e22,e21) = e23 ),
inference(resolve,[status(thm)],[c_2218,c_2507]) ).
cnf(c_2311,plain,
op2(e22,e21) = e23,
inference(resolve,[status(thm)],[c_2298,c_2508]) ).
cnf(c_2509,plain,
( op2(e23,e21) = e22
| op2(e22,e21) = e22
| op2(e21,e21) = e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_2192,c_96]) ).
cnf(c_2510,plain,
( op2(e23,e21) = e22
| e23 = e22
| op2(e21,e21) = e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_2311,c_2509]) ).
cnf(c_2511,plain,
( op2(e23,e21) = e22
| e22 = e23
| op2(e21,e21) = e22
| e20 = e22 ),
inference(copy,[status(thm)],[c_2510]) ).
cnf(c_2512,plain,
( op2(e23,e21) = e22
| e22 = e23
| op2(e21,e21) = e22 ),
inference(resolve,[status(thm)],[c_304,c_2511]) ).
cnf(c_2513,plain,
( op2(e23,e21) = e22
| e22 = e23 ),
inference(resolve,[status(thm)],[c_2220,c_2512]) ).
cnf(c_2312,plain,
op2(e23,e21) = e22,
inference(resolve,[status(thm)],[c_312,c_2513]) ).
cnf(c_2514,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| op2(e21,e21) = e21
| e20 = e21 ),
inference(paramod,[status(thm)],[c_2192,c_94]) ).
cnf(c_2515,plain,
( op2(e23,e21) = e21
| e23 = e21
| op2(e21,e21) = e21
| e20 = e21 ),
inference(paramod,[status(thm)],[c_2311,c_2514]) ).
cnf(c_2516,plain,
( e22 = e21
| e23 = e21
| op2(e21,e21) = e21
| e20 = e21 ),
inference(paramod,[status(thm)],[c_2312,c_2515]) ).
cnf(c_2517,plain,
( e22 = e21
| e23 = e21
| op2(e21,e21) = e21
| e21 = e20 ),
inference(copy,[status(thm)],[c_2516]) ).
cnf(c_2518,plain,
( e22 = e21
| e21 = e23
| op2(e21,e21) = e21
| e21 = e20 ),
inference(copy,[status(thm)],[c_2517]) ).
cnf(c_2519,plain,
( e21 = e22
| e21 = e23
| op2(e21,e21) = e21
| e21 = e20 ),
inference(copy,[status(thm)],[c_2518]) ).
cnf(c_2520,plain,
( e21 = e22
| e21 = e23
| op2(e21,e21) = e21 ),
inference(resolve,[status(thm)],[c_302,c_2519]) ).
cnf(c_2521,plain,
( e21 = e22
| op2(e21,e21) = e21 ),
inference(resolve,[status(thm)],[c_310,c_2520]) ).
cnf(c_2313,plain,
op2(e21,e21) = e21,
inference(resolve,[status(thm)],[c_308,c_2521]) ).
cnf(c_2522,plain,
( op2(e22,e23) = e21
| e23 = e21 ),
inference(paramod,[status(thm)],[c_2306,c_2190]) ).
cnf(c_2523,plain,
( op2(e22,e23) = e21
| e21 = e23 ),
inference(copy,[status(thm)],[c_2522]) ).
cnf(c_2314,plain,
op2(e22,e23) = e21,
inference(resolve,[status(thm)],[c_310,c_2523]) ).
cnf(c_2524,plain,
( op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e20 ),
inference(resolve,[status(thm)],[c_2196,c_71]) ).
cnf(c_2525,plain,
( op2(e21,e20) = e23
| op2(e21,e20) = e20 ),
inference(resolve,[status(thm)],[c_2221,c_2524]) ).
cnf(c_2318,plain,
op2(e21,e20) = e20,
inference(resolve,[status(thm)],[c_2300,c_2525]) ).
cnf(c_2526,plain,
( op2(e22,e20) = e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_2318,c_2198]) ).
cnf(c_2321,plain,
op2(e22,e20) = e22,
inference(resolve,[status(thm)],[c_304,c_2526]) ).
cnf(c_2527,plain,
( e21 = e22
| op2(e22,e22) != e23 ),
inference(paramod,[status(thm)],[c_2314,c_605]) ).
cnf(c_2322,plain,
op2(e22,e22) != e23,
inference(resolve,[status(thm)],[c_308,c_2527]) ).
cnf(c_2528,plain,
( e23 = e22
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_2306,c_2199]) ).
cnf(c_2529,plain,
( e22 = e23
| op2(e20,e22) = e22 ),
inference(copy,[status(thm)],[c_2528]) ).
cnf(c_2323,plain,
op2(e20,e22) = e22,
inference(resolve,[status(thm)],[c_312,c_2529]) ).
cnf(c_2530,plain,
( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| e12 = e13 ),
inference(paramod,[status(thm)],[c_2295,c_58]) ).
cnf(c_2531,plain,
( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13 ),
inference(resolve,[status(thm)],[c_301,c_2530]) ).
cnf(c_2532,plain,
( op1(e13,e12) = e13
| op1(e11,e12) = e13 ),
inference(resolve,[status(thm)],[c_2294,c_2531]) ).
cnf(c_2324,plain,
op1(e11,e12) = e13,
inference(resolve,[status(thm)],[c_2269,c_2532]) ).
cnf(c_2533,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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,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(e12) != op2(e20,e22) ),
inference(paramod,[status(thm)],[c_2295,c_2227]) ).
cnf(c_2534,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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,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)
| e22 != op2(e20,e22) ),
inference(paramod,[status(thm)],[c_883,c_2533]) ).
cnf(c_2535,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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,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)
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2323,c_2534]) ).
cnf(c_2536,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| h4(e13) != op2(e20,e23)
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2278,c_2535]) ).
cnf(c_2537,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| e23 != op2(e20,e23)
| e22 != e22 ),
inference(paramod,[status(thm)],[c_877,c_2536]) ).
cnf(c_2538,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(op1(e11,e10)) != op2(e21,e20)
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2306,c_2537]) ).
cnf(c_2539,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| h4(e10) != op2(e21,e20)
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2290,c_2538]) ).
cnf(c_2540,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| e20 != op2(e21,e20)
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_879,c_2539]) ).
cnf(c_2541,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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,e12)) != op2(e21,e22)
| h4(op1(e11,e11)) != op2(e21,e21)
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2318,c_2540]) ).
cnf(c_2542,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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,e12)) != op2(e21,e22)
| h4(e11) != op2(e21,e21)
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2285,c_2541]) ).
cnf(c_2543,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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,e12)) != op2(e21,e22)
| e21 != op2(e21,e21)
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_881,c_2542]) ).
cnf(c_2544,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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,e12)) != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2313,c_2543]) ).
cnf(c_2545,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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(e13) != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2324,c_2544]) ).
cnf(c_2546,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| 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)
| e23 != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_877,c_2545]) ).
cnf(c_2547,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| h4(e12) != op2(e22,e20)
| e23 != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2293,c_2546]) ).
cnf(c_2548,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| e22 != op2(e22,e20)
| e23 != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_883,c_2547]) ).
cnf(c_2549,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(op1(e12,e11)) != op2(e22,e21)
| e22 != e22
| e23 != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2321,c_2548]) ).
cnf(c_2550,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| h4(e13) != op2(e22,e21)
| e22 != e22
| e23 != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2283,c_2549]) ).
cnf(c_2551,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != op2(e22,e21)
| e22 != e22
| e23 != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_877,c_2550]) ).
cnf(c_2552,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(op1(e12,e13)) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23
| e22 != e22
| e23 != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2311,c_2551]) ).
cnf(c_2553,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| h4(e11) != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23
| e22 != e22
| e23 != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2286,c_2552]) ).
cnf(c_2554,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| e21 != op2(e22,e23)
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23
| e22 != e22
| e23 != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_881,c_2553]) ).
cnf(c_2555,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e13,e11)) != op2(e23,e21)
| e21 != e21
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23
| e22 != e22
| e23 != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2314,c_2554]) ).
cnf(c_2556,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(e12) != op2(e23,e21)
| e21 != e21
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23
| e22 != e22
| e23 != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2284,c_2555]) ).
cnf(c_2557,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| e22 != op2(e23,e21)
| e21 != e21
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23
| e22 != e22
| e23 != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_883,c_2556]) ).
cnf(c_2558,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| e21 != e21
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23
| e22 != e22
| e23 != op2(e21,e22)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(paramod,[status(thm)],[c_2312,c_2557]) ).
cnf(c_2559,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| e21 != e21
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23
| e22 != e22
| op2(e21,e22) != e23
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22 ),
inference(copy,[status(thm)],[c_2558]) ).
cnf(c_2560,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| e21 != e21
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23
| e22 != e22
| op2(e21,e22) != e23
| e21 != e21
| e20 != e20
| e23 != e23 ),
inference(copy,[status(thm)],[c_2559]) ).
cnf(c_2561,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| e21 != e21
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23
| e22 != e22
| op2(e21,e22) != e23
| e21 != e21
| e20 != e20 ),
inference(copy,[status(thm)],[c_2560]) ).
cnf(c_2562,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| e21 != e21
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23
| e22 != e22
| op2(e21,e22) != e23
| e21 != e21 ),
inference(copy,[status(thm)],[c_2561]) ).
cnf(c_2563,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| e21 != e21
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23
| e22 != e22
| op2(e21,e22) != e23 ),
inference(copy,[status(thm)],[c_2562]) ).
cnf(c_2564,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| e21 != e21
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23
| op2(e21,e22) != e23 ),
inference(copy,[status(thm)],[c_2563]) ).
cnf(c_2565,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| e21 != e21
| h4(op1(e12,e12)) != op2(e22,e22)
| op2(e21,e22) != e23 ),
inference(copy,[status(thm)],[c_2564]) ).
cnf(c_2566,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| h4(op1(e12,e12)) != op2(e22,e22)
| op2(e21,e22) != e23 ),
inference(copy,[status(thm)],[c_2565]) ).
cnf(c_2343,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e12,e12)) != op2(e22,e22)
| op2(e21,e22) != e23 ),
inference(copy,[status(thm)],[c_2566]) ).
cnf(c_2567,plain,
( op1(e12,e12) = e10
| op1(e11,e12) = e10
| e12 = e10 ),
inference(paramod,[status(thm)],[c_2295,c_2273]) ).
cnf(c_2568,plain,
( op1(e12,e12) = e10
| e13 = e10
| e12 = e10 ),
inference(paramod,[status(thm)],[c_2324,c_2567]) ).
cnf(c_2569,plain,
( op1(e12,e12) = e10
| e13 = e10
| e10 = e12 ),
inference(copy,[status(thm)],[c_2568]) ).
cnf(c_2570,plain,
( op1(e12,e12) = e10
| e10 = e13
| e10 = e12 ),
inference(copy,[status(thm)],[c_2569]) ).
cnf(c_2571,plain,
( op1(e12,e12) = e10
| e10 = e13 ),
inference(resolve,[status(thm)],[c_293,c_2570]) ).
cnf(c_2344,plain,
op1(e12,e12) = e10,
inference(resolve,[status(thm)],[c_295,c_2571]) ).
cnf(c_2572,plain,
( op1(e13,e12) = e11
| e12 = e11 ),
inference(paramod,[status(thm)],[c_2284,c_2146]) ).
cnf(c_2573,plain,
( op1(e13,e12) = e11
| e11 = e12 ),
inference(copy,[status(thm)],[c_2572]) ).
cnf(c_2347,plain,
op1(e13,e12) = e11,
inference(resolve,[status(thm)],[c_297,c_2573]) ).
cnf(c_2574,plain,
( op2(e23,e22) = e23
| op2(e22,e22) = e23
| op2(e21,e22) = e23
| e22 = e23 ),
inference(paramod,[status(thm)],[c_2323,c_106]) ).
cnf(c_2575,plain,
( op2(e23,e22) = e23
| op2(e22,e22) = e23
| op2(e21,e22) = e23 ),
inference(resolve,[status(thm)],[c_312,c_2574]) ).
cnf(c_2576,plain,
( op2(e23,e22) = e23
| op2(e21,e22) = e23 ),
inference(resolve,[status(thm)],[c_2322,c_2575]) ).
cnf(c_2349,plain,
op2(e21,e22) = e23,
inference(resolve,[status(thm)],[c_2297,c_2576]) ).
cnf(c_2577,plain,
( op2(e22,e22) = e20
| op2(e21,e22) = e20
| e22 = e20 ),
inference(paramod,[status(thm)],[c_2323,c_2301]) ).
cnf(c_2578,plain,
( op2(e22,e22) = e20
| e23 = e20
| e22 = e20 ),
inference(paramod,[status(thm)],[c_2349,c_2577]) ).
cnf(c_2579,plain,
( op2(e22,e22) = e20
| e23 = e20
| e20 = e22 ),
inference(copy,[status(thm)],[c_2578]) ).
cnf(c_2580,plain,
( op2(e22,e22) = e20
| e20 = e23
| e20 = e22 ),
inference(copy,[status(thm)],[c_2579]) ).
cnf(c_2581,plain,
( op2(e22,e22) = e20
| e20 = e23 ),
inference(resolve,[status(thm)],[c_304,c_2580]) ).
cnf(c_2350,plain,
op2(e22,e22) = e20,
inference(resolve,[status(thm)],[c_306,c_2581]) ).
cnf(c_2582,plain,
( op2(e23,e22) = e21
| e22 = e21 ),
inference(paramod,[status(thm)],[c_2312,c_2191]) ).
cnf(c_2583,plain,
( op2(e23,e22) = e21
| e21 = e22 ),
inference(copy,[status(thm)],[c_2582]) ).
cnf(c_2353,plain,
op2(e23,e22) = e21,
inference(resolve,[status(thm)],[c_308,c_2583]) ).
cnf(c_2584,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(op1(e12,e12)) != op2(e22,e22)
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2349,c_2343]) ).
cnf(c_2585,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| h4(e10) != op2(e22,e22)
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2344,c_2584]) ).
cnf(c_2586,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| e20 != op2(e22,e22)
| e23 != e23 ),
inference(paramod,[status(thm)],[c_879,c_2585]) ).
cnf(c_2587,negated_conjecture,
( h4(op1(e13,e12)) != op2(e23,e22)
| e20 != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2350,c_2586]) ).
cnf(c_2588,negated_conjecture,
( h4(e11) != op2(e23,e22)
| e20 != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2347,c_2587]) ).
cnf(c_2589,negated_conjecture,
( e21 != op2(e23,e22)
| e20 != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_881,c_2588]) ).
cnf(c_2590,negated_conjecture,
( e21 != e21
| e20 != e20
| e23 != e23 ),
inference(paramod,[status(thm)],[c_2353,c_2589]) ).
cnf(c_2591,negated_conjecture,
( e21 != e21
| e20 != e20 ),
inference(copy,[status(thm)],[c_2590]) ).
cnf(c_2592,negated_conjecture,
e21 != e21,
inference(copy,[status(thm)],[c_2591]) ).
cnf(c_2360,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_2592]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG121+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 21:10:54 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 483865 was started by sandbox on n007,
% 0.09/0.36 % Sat Sep 26 21:10:54 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 5.55/5.86
% 5.55/5.86 % From the command line: assign(max_seconds, 300).
% 9.97/6.52
% 9.97/6.52 % SZS status Theorem for theBenchmark
% 9.97/6.52
% 9.97/6.52 % Proof 1 at 0.58 (+ 0.04) seconds.
% 9.97/6.52 % Length of proof is 182.
% 9.97/6.52 % Level of proof is 10.
% 9.97/6.52 % Maximum clause weight is 110.000.
% 9.97/6.52 % Given clauses 0.
% 9.97/6.52
% 9.97/6.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------