%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG110+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:49:31 AM UTC 2026
% Result : Theorem 9.75s 10.53s
% Output : CNFRefutation 9.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 118
% Number of leaves : 17
% Syntax : Number of formulae : 491 ( 182 unt; 0 def)
% Number of atoms : 3043 (3042 equ)
% Maximal formula atoms : 128 ( 6 avg)
% Number of connectives : 4310 (1758 ~;2150 |; 402 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 6 avg)
% Maximal term depth : 4 ( 2 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,e12) != e13
& op1(e12,e13) = e12 )
| ( op1(e13,e11) != e13
& op1(e11,e13) = e11 )
| ( op1(e13,e10) != e13
& op1(e10,e13) = e10 ) )
& ( ( op1(e12,e13) != e12
& op1(e13,e12) = e13 )
| ( op1(e12,e12) != e12
& op1(e12,e12) = e12 )
| ( op1(e12,e11) != e12
& op1(e11,e12) = e11 )
| ( op1(e12,e10) != e12
& op1(e10,e12) = e10 ) )
& ( ( op1(e11,e13) != e11
& op1(e13,e11) = e13 )
| ( op1(e11,e12) != e11
& op1(e12,e11) = e12 )
| ( op1(e11,e11) != e11
& op1(e11,e11) = e11 )
| ( op1(e11,e10) != e11
& op1(e10,e11) = e10 ) )
& ( ( op1(e10,e13) != e10
& op1(e13,e10) = e13 )
| ( op1(e10,e12) != e10
& op1(e12,e10) = e12 )
| ( op1(e10,e11) != e10
& op1(e11,e10) = e11 )
| ( op1(e10,e10) != e10
& op1(e10,e10) = e10 ) ) ),
file('theBenchmark.p',ax10) ).
fof(ax11,axiom,
( ( ( op2(e23,e23) != e23
& op2(e23,e23) = e23 )
| ( op2(e23,e22) != e23
& op2(e22,e23) = e22 )
| ( op2(e23,e21) != e23
& op2(e21,e23) = e21 )
| ( op2(e23,e20) != e23
& op2(e20,e23) = e20 ) )
& ( ( op2(e22,e23) != e22
& op2(e23,e22) = e23 )
| ( op2(e22,e22) != e22
& op2(e22,e22) = e22 )
| ( op2(e22,e21) != e22
& op2(e21,e22) = e21 )
| ( op2(e22,e20) != e22
& op2(e20,e22) = e20 ) )
& ( ( op2(e21,e23) != e21
& op2(e23,e21) = e23 )
| ( op2(e21,e22) != e21
& op2(e22,e21) = e22 )
| ( op2(e21,e21) != e21
& op2(e21,e21) = e21 )
| ( op2(e21,e20) != e21
& op2(e20,e21) = e20 ) )
& ( ( op2(e20,e23) != e20
& op2(e23,e20) = e23 )
| ( op2(e20,e22) != e20
& op2(e22,e20) = e22 )
| ( op2(e20,e21) != e20
& op2(e21,e20) = e21 )
| ( op2(e20,e20) != e20
& op2(e20,e20) = e20 ) ) ),
file('theBenchmark.p',ax11) ).
fof(ax12,axiom,
( e13 = op1(e12,e12)
& e11 = op1(op1(op1(e12,e12),op1(e12,e12)),op1(e12,e12))
& e10 = op1(op1(e12,e12),op1(e12,e12)) ),
file('theBenchmark.p',ax12) ).
fof(ax13,axiom,
( e23 = op2(e22,e22)
& e21 = op2(op2(op2(e22,e22),op2(e22,e22)),op2(e22,e22))
& e20 = op2(op2(e22,e22),op2(e22,e22)) ),
file('theBenchmark.p',ax13) ).
fof(ax14,axiom,
( h1(e13) = op2(e20,e20)
& h1(e11) = op2(op2(op2(e20,e20),op2(e20,e20)),op2(e20,e20))
& h1(e10) = op2(op2(e20,e20),op2(e20,e20))
& h1(e12) = e20 ),
file('theBenchmark.p',ax14) ).
fof(ax15,axiom,
( h2(e13) = op2(e21,e21)
& h2(e11) = op2(op2(op2(e21,e21),op2(e21,e21)),op2(e21,e21))
& h2(e10) = op2(op2(e21,e21),op2(e21,e21))
& h2(e12) = e21 ),
file('theBenchmark.p',ax15) ).
fof(ax16,axiom,
( h3(e13) = op2(e22,e22)
& h3(e11) = op2(op2(op2(e22,e22),op2(e22,e22)),op2(e22,e22))
& h3(e10) = op2(op2(e22,e22),op2(e22,e22))
& h3(e12) = e22 ),
file('theBenchmark.p',ax16) ).
fof(ax17,axiom,
( h4(e13) = op2(e23,e23)
& h4(e11) = op2(op2(op2(e23,e23),op2(e23,e23)),op2(e23,e23))
& h4(e10) = op2(op2(e23,e23),op2(e23,e23))
& h4(e12) = 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_20,plain,
( op1(e10,e11) = e13
| op1(e10,e11) = e12
| op1(e10,e11) = e11
| op1(e10,e11) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_21,plain,
( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_36,plain,
( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_40,plain,
( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| op1(e10,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_41,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_43,plain,
( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_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_47,plain,
( op1(e11,e13) = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_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_61,plain,
( op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_64,plain,
( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_66,plain,
( op1(e13,e13) = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| op1(e10,e13) = e13 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_69,plain,
( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| op2(e20,e22) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_84,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| op2(e20,e20) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_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_89,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_91,plain,
( op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20
| op2(e21,e20) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_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_95,plain,
( op2(e21,e23) = e22
| op2(e21,e22) = e22
| op2(e21,e21) = e22
| op2(e21,e20) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_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_109,plain,
( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_112,plain,
( op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_114,plain,
( op2(e23,e23) = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| op2(e20,e23) = e23 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_123,plain,
op1(e11,e11) != op1(e10,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_126,plain,
op1(e13,e11) != op1(e10,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_131,plain,
op1(e11,e12) != op1(e10,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_132,plain,
op1(e12,e12) != op1(e10,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_133,plain,
op1(e10,e12) != op1(e12,e12),
inference(copy,[status(thm)],[c_132]) ).
cnf(c_138,plain,
op1(e13,e12) != op1(e12,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_148,plain,
op1(e10,e12) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_149,plain,
op1(e10,e10) != op1(e10,e12),
inference(copy,[status(thm)],[c_148]) ).
cnf(c_151,plain,
op1(e10,e12) != op1(e10,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_152,plain,
op1(e10,e11) != op1(e10,e12),
inference(copy,[status(thm)],[c_151]) ).
cnf(c_153,plain,
op1(e10,e13) != op1(e10,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_154,plain,
op1(e10,e13) != op1(e10,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_166,plain,
op1(e12,e13) != op1(e12,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_169,plain,
op1(e12,e13) != op1(e12,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_170,plain,
op1(e12,e13) != op1(e12,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_171,plain,
op1(e13,e11) != op1(e13,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_174,plain,
op1(e13,e13) != op1(e13,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_178,plain,
op1(e13,e13) != op1(e13,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_182,plain,
op2(e23,e20) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_187,plain,
op2(e21,e21) != op2(e20,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_190,plain,
op2(e23,e21) != op2(e20,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_195,plain,
op2(e21,e22) != op2(e20,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_196,plain,
op2(e22,e22) != op2(e20,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_197,plain,
op2(e20,e22) != op2(e22,e22),
inference(copy,[status(thm)],[c_196]) ).
cnf(c_202,plain,
op2(e23,e22) != op2(e22,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_212,plain,
op2(e20,e22) != op2(e20,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_213,plain,
op2(e20,e20) != op2(e20,e22),
inference(copy,[status(thm)],[c_212]) ).
cnf(c_215,plain,
op2(e20,e22) != op2(e20,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_216,plain,
op2(e20,e21) != op2(e20,e22),
inference(copy,[status(thm)],[c_215]) ).
cnf(c_217,plain,
op2(e20,e23) != op2(e20,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_218,plain,
op2(e20,e23) != op2(e20,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_230,plain,
op2(e22,e23) != op2(e22,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_233,plain,
op2(e22,e23) != op2(e22,e21),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_234,plain,
op2(e22,e23) != op2(e22,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_238,plain,
op2(e23,e23) != op2(e23,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_242,plain,
op2(e23,e23) != op2(e23,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_243,plain,
e11 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_244,plain,
e12 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_245,plain,
e10 != e12,
inference(copy,[status(thm)],[c_244]) ).
cnf(c_246,plain,
e13 != e10,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_247,plain,
e12 != e11,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_248,plain,
e11 != e12,
inference(copy,[status(thm)],[c_247]) ).
cnf(c_249,plain,
e13 != e11,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_250,plain,
e13 != e12,
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_251,plain,
e21 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_252,plain,
e22 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_253,plain,
e20 != e22,
inference(copy,[status(thm)],[c_252]) ).
cnf(c_254,plain,
e23 != e20,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_255,plain,
e22 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_256,plain,
e21 != e22,
inference(copy,[status(thm)],[c_255]) ).
cnf(c_257,plain,
e23 != e21,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_258,plain,
e23 != e22,
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_288,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e12
| op1(e11,e10) = e11 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_296,plain,
( op1(e13,e11) = e13
| op1(e12,e11) = e12
| op1(e10,e11) = e10 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_304,plain,
( op1(e13,e12) = e13
| op1(e11,e12) = e11
| op1(e10,e12) = e10 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_320,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e22
| op2(e21,e20) = e21 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_328,plain,
( op2(e23,e21) = e23
| op2(e22,e21) = e22
| op2(e20,e21) = e20 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_336,plain,
( op2(e23,e22) = e23
| op2(e21,e22) = e21
| op2(e20,e22) = e20 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_352,plain,
op1(op1(e12,e12),op1(e12,e12)) = e10,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_353,plain,
op1(op1(op1(e12,e12),op1(e12,e12)),op1(e12,e12)) = e11,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_354,plain,
op1(e10,op1(e12,e12)) = e11,
inference(paramod,[status(thm)],[c_352,c_353]) ).
cnf(c_355,plain,
op1(e12,e12) = e13,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_356,plain,
op2(op2(e22,e22),op2(e22,e22)) = e20,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_357,plain,
op2(op2(op2(e22,e22),op2(e22,e22)),op2(e22,e22)) = e21,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_358,plain,
op2(e20,op2(e22,e22)) = e21,
inference(paramod,[status(thm)],[c_356,c_357]) ).
cnf(c_359,plain,
op2(e22,e22) = e23,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_365,plain,
h1(e13) = op2(e20,e20),
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_366,plain,
op2(e20,e20) = h1(e13),
inference(copy,[status(thm)],[c_365]) ).
cnf(c_372,plain,
h2(e13) = op2(e21,e21),
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_373,plain,
op2(e21,e21) = h2(e13),
inference(copy,[status(thm)],[c_372]) ).
cnf(c_374,plain,
h3(e12) = e22,
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_375,plain,
h3(e10) = op2(op2(e22,e22),op2(e22,e22)),
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_2181,plain,
h3(e10) = op2(e23,op2(e22,e22)),
inference(paramod,[status(thm)],[c_359,c_375]) ).
cnf(c_2182,plain,
h3(e10) = op2(e23,e23),
inference(paramod,[status(thm)],[c_359,c_2181]) ).
cnf(c_376,plain,
op2(e23,e23) = h3(e10),
inference(copy,[status(thm)],[c_2182]) ).
cnf(c_377,plain,
h3(e11) = op2(op2(op2(e22,e22),op2(e22,e22)),op2(e22,e22)),
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_2183,plain,
h3(e11) = op2(op2(e23,op2(e22,e22)),op2(e22,e22)),
inference(paramod,[status(thm)],[c_359,c_377]) ).
cnf(c_2184,plain,
h3(e11) = op2(op2(e23,e23),op2(e22,e22)),
inference(paramod,[status(thm)],[c_359,c_2183]) ).
cnf(c_2185,plain,
h3(e11) = op2(h3(e10),op2(e22,e22)),
inference(paramod,[status(thm)],[c_376,c_2184]) ).
cnf(c_2186,plain,
h3(e11) = op2(h3(e10),e23),
inference(paramod,[status(thm)],[c_359,c_2185]) ).
cnf(c_378,plain,
op2(h3(e10),e23) = h3(e11),
inference(copy,[status(thm)],[c_2186]) ).
cnf(c_379,plain,
h3(e13) = op2(e22,e22),
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_380,plain,
h3(e13) = e23,
inference(paramod,[status(thm)],[c_359,c_379]) ).
cnf(c_382,plain,
h4(e10) = op2(op2(e23,e23),op2(e23,e23)),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_2187,plain,
h4(e10) = op2(h3(e10),op2(e23,e23)),
inference(paramod,[status(thm)],[c_376,c_382]) ).
cnf(c_2188,plain,
h4(e10) = op2(h3(e10),h3(e10)),
inference(paramod,[status(thm)],[c_376,c_2187]) ).
cnf(c_383,plain,
op2(h3(e10),h3(e10)) = h4(e10),
inference(copy,[status(thm)],[c_2188]) ).
cnf(c_384,plain,
h4(e11) = op2(op2(op2(e23,e23),op2(e23,e23)),op2(e23,e23)),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_2189,plain,
h4(e11) = op2(op2(h3(e10),op2(e23,e23)),op2(e23,e23)),
inference(paramod,[status(thm)],[c_376,c_384]) ).
cnf(c_2190,plain,
h4(e11) = op2(op2(h3(e10),h3(e10)),op2(e23,e23)),
inference(paramod,[status(thm)],[c_376,c_2189]) ).
cnf(c_2191,plain,
h4(e11) = op2(h4(e10),op2(e23,e23)),
inference(paramod,[status(thm)],[c_383,c_2190]) ).
cnf(c_2192,plain,
h4(e11) = op2(h4(e10),h3(e10)),
inference(paramod,[status(thm)],[c_376,c_2191]) ).
cnf(c_385,plain,
op2(h4(e10),h3(e10)) = h4(e11),
inference(copy,[status(thm)],[c_2192]) ).
cnf(c_1106,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_2193,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_383,c_1106]) ).
cnf(c_2194,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_374,c_2193]) ).
cnf(c_2195,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_380,c_2194]) ).
cnf(c_2196,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_378,c_2195]) ).
cnf(c_2197,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_374,c_2196]) ).
cnf(c_2198,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_380,c_2197]) ).
cnf(c_2199,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_374,c_2198]) ).
cnf(c_2200,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_374,c_2199]) ).
cnf(c_2201,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(e13) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_355,c_2200]) ).
cnf(c_2202,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| e23 != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_380,c_2201]) ).
cnf(c_2203,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| e23 != op2(e22,h3(e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_374,c_2202]) ).
cnf(c_2204,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| e23 != op2(e22,e22)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_374,c_2203]) ).
cnf(c_2205,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_359,c_2204]) ).
cnf(c_2206,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(e22,h3(e13))
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_374,c_2205]) ).
cnf(c_2207,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_380,c_2206]) ).
cnf(c_2208,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_380,c_2207]) ).
cnf(c_2209,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_380,c_2208]) ).
cnf(c_2210,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(e23,h3(e12))
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_380,c_2209]) ).
cnf(c_2211,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_374,c_2210]) ).
cnf(c_2212,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(e23,h3(e13))
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_380,c_2211]) ).
cnf(c_2213,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_380,c_2212]) ).
cnf(c_2214,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_376,c_2213]) ).
cnf(c_2215,negated_conjecture,
( h3(e13) != e23
| e22 != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_374,c_2214]) ).
cnf(c_2216,negated_conjecture,
( e23 != e23
| e22 != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_380,c_2215]) ).
cnf(c_2217,negated_conjecture,
( e23 != e23
| e22 != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(copy,[status(thm)],[c_2216]) ).
cnf(c_2218,negated_conjecture,
( e23 != e23
| e22 != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(copy,[status(thm)],[c_2217]) ).
cnf(c_2219,negated_conjecture,
( e23 != e23
| e22 != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(copy,[status(thm)],[c_2218]) ).
cnf(c_2220,negated_conjecture,
( e23 != e23
| e22 != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(copy,[status(thm)],[c_2219]) ).
cnf(c_2221,negated_conjecture,
( e23 != e23
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(copy,[status(thm)],[c_2220]) ).
cnf(c_1107,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(copy,[status(thm)],[c_2221]) ).
cnf(c_1691,plain,
op1(e10,e13) = e11,
inference(paramod,[status(thm)],[c_355,c_354]) ).
cnf(c_2222,plain,
op1(e13,op1(e12,e12)) = e10,
inference(paramod,[status(thm)],[c_355,c_352]) ).
cnf(c_1692,plain,
op1(e13,e13) = e10,
inference(paramod,[status(thm)],[c_355,c_2222]) ).
cnf(c_1693,plain,
op1(e12,e13) != e13,
inference(paramod,[status(thm)],[c_355,c_170]) ).
cnf(c_1696,plain,
op1(e13,e12) != e13,
inference(paramod,[status(thm)],[c_355,c_138]) ).
cnf(c_1698,plain,
op1(e10,e12) != e13,
inference(paramod,[status(thm)],[c_355,c_133]) ).
cnf(c_2223,plain,
( op1(e13,e12) = e10
| e13 = e10
| op1(e11,e12) = e10
| op1(e10,e12) = e10 ),
inference(paramod,[status(thm)],[c_355,c_52]) ).
cnf(c_1703,plain,
( op1(e13,e12) = e10
| op1(e11,e12) = e10
| op1(e10,e12) = e10 ),
inference(resolve,[status(thm)],[c_246,c_2223]) ).
cnf(c_1705,plain,
op2(e20,e23) = e21,
inference(paramod,[status(thm)],[c_359,c_358]) ).
cnf(c_2224,plain,
op2(e23,op2(e22,e22)) = e20,
inference(paramod,[status(thm)],[c_359,c_356]) ).
cnf(c_2225,plain,
op2(e23,e23) = e20,
inference(paramod,[status(thm)],[c_359,c_2224]) ).
cnf(c_1706,plain,
h3(e10) = e20,
inference(paramod,[status(thm)],[c_376,c_2225]) ).
cnf(c_1707,plain,
op2(e22,e23) != e23,
inference(paramod,[status(thm)],[c_359,c_234]) ).
cnf(c_1710,plain,
op2(e23,e22) != e23,
inference(paramod,[status(thm)],[c_359,c_202]) ).
cnf(c_1712,plain,
op2(e20,e22) != e23,
inference(paramod,[status(thm)],[c_359,c_197]) ).
cnf(c_2226,plain,
( op2(e23,e22) = e20
| e23 = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 ),
inference(paramod,[status(thm)],[c_359,c_100]) ).
cnf(c_1717,plain,
( op2(e23,e22) = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 ),
inference(resolve,[status(thm)],[c_254,c_2226]) ).
cnf(c_2227,plain,
h1(e13) != op2(e20,e22),
inference(paramod,[status(thm)],[c_366,c_213]) ).
cnf(c_1722,plain,
op2(e20,e22) != h1(e13),
inference(copy,[status(thm)],[c_2227]) ).
cnf(c_1724,plain,
op2(e23,e20) != h1(e13),
inference(paramod,[status(thm)],[c_366,c_182]) ).
cnf(c_2228,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| h1(e13) = e23 ),
inference(paramod,[status(thm)],[c_366,c_89]) ).
cnf(c_2229,plain,
( e21 = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| h1(e13) = e23 ),
inference(paramod,[status(thm)],[c_1705,c_2228]) ).
cnf(c_2230,plain,
( e23 = e21
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| h1(e13) = e23 ),
inference(copy,[status(thm)],[c_2229]) ).
cnf(c_2231,plain,
( e23 = e21
| op2(e20,e21) = e23
| h1(e13) = e23 ),
inference(resolve,[status(thm)],[c_1712,c_2230]) ).
cnf(c_1728,plain,
( op2(e20,e21) = e23
| h1(e13) = e23 ),
inference(resolve,[status(thm)],[c_257,c_2231]) ).
cnf(c_1729,plain,
( op2(e23,e20) = e22
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| h1(e13) = e22 ),
inference(paramod,[status(thm)],[c_366,c_88]) ).
cnf(c_2232,plain,
( op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| h1(e13) = e22 ),
inference(paramod,[status(thm)],[c_366,c_87]) ).
cnf(c_2233,plain,
( e21 = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| h1(e13) = e22 ),
inference(paramod,[status(thm)],[c_1705,c_2232]) ).
cnf(c_1730,plain,
( op2(e20,e22) = e22
| op2(e20,e21) = e22
| h1(e13) = e22 ),
inference(resolve,[status(thm)],[c_256,c_2233]) ).
cnf(c_1732,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| h1(e13) = e20 ),
inference(paramod,[status(thm)],[c_366,c_84]) ).
cnf(c_2234,plain,
h2(e13) != op2(e20,e21),
inference(paramod,[status(thm)],[c_373,c_187]) ).
cnf(c_1742,plain,
op2(e20,e21) != h2(e13),
inference(copy,[status(thm)],[c_2234]) ).
cnf(c_1746,plain,
( op2(e21,e23) = e22
| op2(e21,e22) = e22
| h2(e13) = e22
| op2(e21,e20) = e22 ),
inference(paramod,[status(thm)],[c_373,c_95]) ).
cnf(c_1747,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| h2(e13) = e21
| op2(e20,e21) = e21 ),
inference(paramod,[status(thm)],[c_373,c_94]) ).
cnf(c_1750,plain,
( op2(e21,e23) = e20
| op2(e21,e22) = e20
| h2(e13) = e20
| op2(e21,e20) = e20 ),
inference(paramod,[status(thm)],[c_373,c_91]) ).
cnf(c_2235,plain,
h3(e10) != op2(e23,e22),
inference(paramod,[status(thm)],[c_376,c_242]) ).
cnf(c_2236,plain,
e20 != op2(e23,e22),
inference(paramod,[status(thm)],[c_1706,c_2235]) ).
cnf(c_1752,plain,
op2(e23,e22) != e20,
inference(copy,[status(thm)],[c_2236]) ).
cnf(c_2237,plain,
h3(e10) != op2(e23,e20),
inference(paramod,[status(thm)],[c_376,c_238]) ).
cnf(c_2238,plain,
e20 != op2(e23,e20),
inference(paramod,[status(thm)],[c_1706,c_2237]) ).
cnf(c_1754,plain,
op2(e23,e20) != e20,
inference(copy,[status(thm)],[c_2238]) ).
cnf(c_2239,plain,
( op2(e23,e23) = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_1705,c_114]) ).
cnf(c_2240,plain,
( h3(e10) = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_376,c_2239]) ).
cnf(c_2241,plain,
( e20 = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_1706,c_2240]) ).
cnf(c_2242,plain,
( e20 = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| e23 = e21 ),
inference(copy,[status(thm)],[c_2241]) ).
cnf(c_2243,plain,
( e23 = e20
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| e23 = e21 ),
inference(copy,[status(thm)],[c_2242]) ).
cnf(c_2244,plain,
( e23 = e20
| op2(e22,e23) = e23
| op2(e21,e23) = e23 ),
inference(resolve,[status(thm)],[c_257,c_2243]) ).
cnf(c_2245,plain,
( e23 = e20
| op2(e21,e23) = e23 ),
inference(resolve,[status(thm)],[c_1707,c_2244]) ).
cnf(c_1757,plain,
op2(e21,e23) = e23,
inference(resolve,[status(thm)],[c_254,c_2245]) ).
cnf(c_2246,plain,
( op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_1705,c_112]) ).
cnf(c_2247,plain,
( op2(e23,e23) = e22
| op2(e22,e23) = e22
| e23 = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_1757,c_2246]) ).
cnf(c_2248,plain,
( h3(e10) = e22
| op2(e22,e23) = e22
| e23 = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_376,c_2247]) ).
cnf(c_2249,plain,
( e20 = e22
| op2(e22,e23) = e22
| e23 = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_1706,c_2248]) ).
cnf(c_2250,plain,
( e20 = e22
| op2(e22,e23) = e22
| e23 = e22 ),
inference(resolve,[status(thm)],[c_256,c_2249]) ).
cnf(c_2251,plain,
( e20 = e22
| op2(e22,e23) = e22 ),
inference(resolve,[status(thm)],[c_258,c_2250]) ).
cnf(c_1759,plain,
op2(e22,e23) = e22,
inference(resolve,[status(thm)],[c_253,c_2251]) ).
cnf(c_2252,plain,
( h3(e10) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(paramod,[status(thm)],[c_376,c_109]) ).
cnf(c_2253,plain,
( e20 = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(paramod,[status(thm)],[c_1706,c_2252]) ).
cnf(c_2254,plain,
( e21 = e20
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(copy,[status(thm)],[c_2253]) ).
cnf(c_1761,plain,
( op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(resolve,[status(thm)],[c_251,c_2254]) ).
cnf(c_2255,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(e20,h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_1706,c_1107]) ).
cnf(c_2256,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != h3(e11)
| h3(op1(e10,e12)) != op2(e20,e22)
| op2(e20,h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_1706,c_2255]) ).
cnf(c_2257,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != op2(e20,e22)
| op2(e20,h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_1691,c_2256]) ).
cnf(c_2258,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),e20) != h3(op1(e11,e10))
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != op2(e20,e22)
| op2(e20,h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_1706,c_2257]) ).
cnf(c_2259,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),e20) != h3(op1(e11,e10))
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != op2(e20,e22)
| op2(e20,h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_1706,c_2258]) ).
cnf(c_2260,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),e20) != h3(op1(e11,e10))
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != op2(e20,e22)
| op2(e20,h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_1759,c_2259]) ).
cnf(c_2261,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),e20) != h3(op1(e11,e10))
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != op2(e20,e22)
| op2(e20,h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_1706,c_2260]) ).
cnf(c_2262,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(e10) != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),e20) != h3(op1(e11,e10))
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != op2(e20,e22)
| op2(e20,h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_1692,c_2261]) ).
cnf(c_2263,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| e20 != h3(e10)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),e20) != h3(op1(e11,e10))
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != op2(e20,e22)
| op2(e20,h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_1706,c_2262]) ).
cnf(c_2264,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| e20 != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),e20) != h3(op1(e11,e10))
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != op2(e20,e22)
| op2(e20,h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_1706,c_2263]) ).
cnf(c_2265,negated_conjecture,
( h3(e11) != e21
| e20 != e20
| e20 != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),e20) != h3(op1(e11,e10))
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != op2(e20,e22)
| op2(e20,h3(e11)) != h3(op1(e10,e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(paramod,[status(thm)],[c_1706,c_2264]) ).
cnf(c_2266,negated_conjecture,
( h3(e11) != e21
| e20 != e20
| e20 != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),e20) != h3(op1(e11,e10))
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(copy,[status(thm)],[c_2265]) ).
cnf(c_2267,negated_conjecture,
( h3(e11) != e21
| e20 != e20
| e20 != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(h3(e11),e20)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(copy,[status(thm)],[c_2266]) ).
cnf(c_2268,negated_conjecture,
( h3(e11) != e21
| e20 != e20
| e20 != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(h3(e11),e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(copy,[status(thm)],[c_2267]) ).
cnf(c_2269,negated_conjecture,
( h3(e11) != e21
| e20 != e20
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(h3(e11),e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(copy,[status(thm)],[c_2268]) ).
cnf(c_1767,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(h3(e11),e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,h3(e11))
| h3(op1(e10,e10)) != h4(e10) ),
inference(copy,[status(thm)],[c_2269]) ).
cnf(c_2270,plain,
e11 != op1(e10,e12),
inference(paramod,[status(thm)],[c_1691,c_154]) ).
cnf(c_1815,plain,
op1(e10,e12) != e11,
inference(copy,[status(thm)],[c_2270]) ).
cnf(c_2271,plain,
e11 != op1(e10,e11),
inference(paramod,[status(thm)],[c_1691,c_153]) ).
cnf(c_1816,plain,
op1(e10,e11) != e11,
inference(copy,[status(thm)],[c_2271]) ).
cnf(c_2272,plain,
( op1(e13,e13) = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_1691,c_66]) ).
cnf(c_2273,plain,
( e10 = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_1692,c_2272]) ).
cnf(c_2274,plain,
( e10 = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| e13 = e11 ),
inference(copy,[status(thm)],[c_2273]) ).
cnf(c_2275,plain,
( e13 = e10
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| e13 = e11 ),
inference(copy,[status(thm)],[c_2274]) ).
cnf(c_2276,plain,
( e13 = e10
| op1(e12,e13) = e13
| op1(e11,e13) = e13 ),
inference(resolve,[status(thm)],[c_249,c_2275]) ).
cnf(c_2277,plain,
( e13 = e10
| op1(e11,e13) = e13 ),
inference(resolve,[status(thm)],[c_1693,c_2276]) ).
cnf(c_1820,plain,
op1(e11,e13) = e13,
inference(resolve,[status(thm)],[c_246,c_2277]) ).
cnf(c_2278,plain,
( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_1691,c_64]) ).
cnf(c_2279,plain,
( op1(e13,e13) = e12
| op1(e12,e13) = e12
| e13 = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_1820,c_2278]) ).
cnf(c_2280,plain,
( e10 = e12
| op1(e12,e13) = e12
| e13 = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_1692,c_2279]) ).
cnf(c_2281,plain,
( e10 = e12
| op1(e12,e13) = e12
| e13 = e12 ),
inference(resolve,[status(thm)],[c_248,c_2280]) ).
cnf(c_2282,plain,
( e10 = e12
| op1(e12,e13) = e12 ),
inference(resolve,[status(thm)],[c_250,c_2281]) ).
cnf(c_1821,plain,
op1(e12,e13) = e12,
inference(resolve,[status(thm)],[c_245,c_2282]) ).
cnf(c_2283,plain,
( e11 = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 ),
inference(paramod,[status(thm)],[c_1691,c_41]) ).
cnf(c_2284,plain,
( e13 = e11
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 ),
inference(copy,[status(thm)],[c_2283]) ).
cnf(c_2285,plain,
( e13 = e11
| op1(e10,e11) = e13
| op1(e10,e10) = e13 ),
inference(resolve,[status(thm)],[c_1698,c_2284]) ).
cnf(c_1822,plain,
( op1(e10,e11) = e13
| op1(e10,e10) = e13 ),
inference(resolve,[status(thm)],[c_249,c_2285]) ).
cnf(c_2286,plain,
e10 != op1(e13,e12),
inference(paramod,[status(thm)],[c_1692,c_178]) ).
cnf(c_1825,plain,
op1(e13,e12) != e10,
inference(copy,[status(thm)],[c_2286]) ).
cnf(c_2287,plain,
e10 != op1(e13,e10),
inference(paramod,[status(thm)],[c_1692,c_174]) ).
cnf(c_1827,plain,
op1(e13,e10) != e10,
inference(copy,[status(thm)],[c_2287]) ).
cnf(c_2288,plain,
( e10 = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 ),
inference(paramod,[status(thm)],[c_1692,c_61]) ).
cnf(c_2289,plain,
( e11 = e10
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 ),
inference(copy,[status(thm)],[c_2288]) ).
cnf(c_1830,plain,
( op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 ),
inference(resolve,[status(thm)],[c_243,c_2289]) ).
cnf(c_1838,plain,
( op1(e11,e12) = e11
| op1(e10,e12) = e10 ),
inference(resolve,[status(thm)],[c_1696,c_304]) ).
cnf(c_2290,plain,
( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e10 ),
inference(resolve,[status(thm)],[c_1815,c_21]) ).
cnf(c_1841,plain,
( op1(e10,e12) = e12
| op1(e10,e12) = e10 ),
inference(resolve,[status(thm)],[c_1698,c_2290]) ).
cnf(c_2291,plain,
e21 != op2(e20,e22),
inference(paramod,[status(thm)],[c_1705,c_218]) ).
cnf(c_1842,plain,
op2(e20,e22) != e21,
inference(copy,[status(thm)],[c_2291]) ).
cnf(c_2292,plain,
e21 != op2(e20,e21),
inference(paramod,[status(thm)],[c_1705,c_217]) ).
cnf(c_1843,plain,
op2(e20,e21) != e21,
inference(copy,[status(thm)],[c_2292]) ).
cnf(c_1845,plain,
op2(h4(e10),e20) = h4(e11),
inference(paramod,[status(thm)],[c_1706,c_385]) ).
cnf(c_2293,plain,
op2(e20,h3(e10)) = h4(e10),
inference(paramod,[status(thm)],[c_1706,c_383]) ).
cnf(c_2294,plain,
op2(e20,e20) = h4(e10),
inference(paramod,[status(thm)],[c_1706,c_2293]) ).
cnf(c_2295,plain,
h1(e13) = h4(e10),
inference(paramod,[status(thm)],[c_366,c_2294]) ).
cnf(c_1846,plain,
h4(e10) = h1(e13),
inference(copy,[status(thm)],[c_2295]) ).
cnf(c_2296,plain,
op2(e20,e23) = h3(e11),
inference(paramod,[status(thm)],[c_1706,c_378]) ).
cnf(c_2297,plain,
e21 = h3(e11),
inference(paramod,[status(thm)],[c_1705,c_2296]) ).
cnf(c_1847,plain,
h3(e11) = e21,
inference(copy,[status(thm)],[c_2297]) ).
cnf(c_1854,plain,
( op2(e21,e22) = e21
| op2(e20,e22) = e20 ),
inference(resolve,[status(thm)],[c_1710,c_336]) ).
cnf(c_2298,plain,
( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e20 ),
inference(resolve,[status(thm)],[c_1842,c_69]) ).
cnf(c_1857,plain,
( op2(e20,e22) = e22
| op2(e20,e22) = e20 ),
inference(resolve,[status(thm)],[c_1712,c_2298]) ).
cnf(c_1858,plain,
( op2(e21,e22) = e20
| op2(e20,e22) = e20 ),
inference(resolve,[status(thm)],[c_1752,c_1717]) ).
cnf(c_1861,plain,
( op2(e22,e20) = e20
| op2(e21,e20) = e20
| h1(e13) = e20 ),
inference(resolve,[status(thm)],[c_1754,c_1732]) ).
cnf(c_2299,plain,
( e23 = e20
| op2(e21,e22) = e20
| h2(e13) = e20
| op2(e21,e20) = e20 ),
inference(paramod,[status(thm)],[c_1757,c_1750]) ).
cnf(c_1864,plain,
( op2(e21,e22) = e20
| h2(e13) = e20
| op2(e21,e20) = e20 ),
inference(resolve,[status(thm)],[c_254,c_2299]) ).
cnf(c_2300,plain,
( e23 = e22
| op2(e21,e22) = e22
| h2(e13) = e22
| op2(e21,e20) = e22 ),
inference(paramod,[status(thm)],[c_1757,c_1746]) ).
cnf(c_1866,plain,
( op2(e21,e22) = e22
| h2(e13) = e22
| op2(e21,e20) = e22 ),
inference(resolve,[status(thm)],[c_258,c_2300]) ).
cnf(c_2301,plain,
e22 != op2(e22,e21),
inference(paramod,[status(thm)],[c_1759,c_233]) ).
cnf(c_1870,plain,
op2(e22,e21) != e22,
inference(copy,[status(thm)],[c_2301]) ).
cnf(c_2302,plain,
e22 != op2(e22,e20),
inference(paramod,[status(thm)],[c_1759,c_230]) ).
cnf(c_1871,plain,
op2(e22,e20) != e22,
inference(copy,[status(thm)],[c_2302]) ).
cnf(c_1873,plain,
( op1(e13,e11) = e11
| op1(e12,e11) = e11
| op1(e11,e11) = e11 ),
inference(resolve,[status(thm)],[c_1816,c_46]) ).
cnf(c_1874,plain,
( op1(e10,e11) = e13
| op1(e10,e11) = e12
| op1(e10,e11) = e10 ),
inference(resolve,[status(thm)],[c_1816,c_20]) ).
cnf(c_2303,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(h3(e11),e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,h3(e11))
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_1846,c_1767]) ).
cnf(c_2304,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(h3(e11),e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_1847,c_2303]) ).
cnf(c_2305,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_1847,c_2304]) ).
cnf(c_2306,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(e21,h3(e11)) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_1847,c_2305]) ).
cnf(c_2307,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(e21,e21) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_1847,c_2306]) ).
cnf(c_2308,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h2(e13) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_373,c_2307]) ).
cnf(c_2309,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h2(e13) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_1847,c_2308]) ).
cnf(c_2310,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(e13) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h2(e13) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_1820,c_2309]) ).
cnf(c_2311,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| e23 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h2(e13) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_380,c_2310]) ).
cnf(c_2312,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| e23 != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h2(e13) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_1847,c_2311]) ).
cnf(c_2313,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,e20)
| e23 != e23
| h3(op1(e11,e12)) != op2(e21,e22)
| h2(e13) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_1757,c_2312]) ).
cnf(c_2314,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e13)) != e22
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| e23 != e23
| h3(op1(e11,e12)) != op2(e21,e22)
| h2(e13) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_1847,c_2313]) ).
cnf(c_2315,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(e12) != e22
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| e23 != e23
| h3(op1(e11,e12)) != op2(e21,e22)
| h2(e13) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_1821,c_2314]) ).
cnf(c_2316,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,e20)
| e22 != e22
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| e23 != e23
| h3(op1(e11,e12)) != op2(e21,e22)
| h2(e13) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_374,c_2315]) ).
cnf(c_2317,negated_conjecture,
( h3(e11) != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| e22 != e22
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| e23 != e23
| h3(op1(e11,e12)) != op2(e21,e22)
| h2(e13) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_1847,c_2316]) ).
cnf(c_2318,negated_conjecture,
( e21 != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| e22 != e22
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| e23 != e23
| h3(op1(e11,e12)) != op2(e21,e22)
| h2(e13) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_1847,c_2317]) ).
cnf(c_2319,negated_conjecture,
( e21 != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| e22 != e22
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| e23 != e23
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(copy,[status(thm)],[c_2318]) ).
cnf(c_2320,negated_conjecture,
( e21 != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| e22 != e22
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(copy,[status(thm)],[c_2319]) ).
cnf(c_2321,negated_conjecture,
( e21 != e21
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(copy,[status(thm)],[c_2320]) ).
cnf(c_1915,negated_conjecture,
( h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(copy,[status(thm)],[c_2321]) ).
cnf(c_2322,plain,
( e13 = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 ),
inference(paramod,[status(thm)],[c_1820,c_47]) ).
cnf(c_1920,plain,
( op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 ),
inference(resolve,[status(thm)],[c_250,c_2322]) ).
cnf(c_2323,plain,
( e13 = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 ),
inference(paramod,[status(thm)],[c_1820,c_43]) ).
cnf(c_1921,plain,
( op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 ),
inference(resolve,[status(thm)],[c_246,c_2323]) ).
cnf(c_2324,plain,
e12 != op1(e12,e11),
inference(paramod,[status(thm)],[c_1821,c_169]) ).
cnf(c_1923,plain,
op1(e12,e11) != e12,
inference(copy,[status(thm)],[c_2324]) ).
cnf(c_2325,plain,
e12 != op1(e12,e10),
inference(paramod,[status(thm)],[c_1821,c_166]) ).
cnf(c_1924,plain,
op1(e12,e10) != e12,
inference(copy,[status(thm)],[c_2325]) ).
cnf(c_1925,plain,
( op1(e11,e12) = e10
| op1(e10,e12) = e10 ),
inference(resolve,[status(thm)],[c_1825,c_1703]) ).
cnf(c_1928,plain,
( op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_1827,c_36]) ).
cnf(c_1931,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| h2(e13) = e21 ),
inference(resolve,[status(thm)],[c_1843,c_1747]) ).
cnf(c_1933,plain,
op2(h1(e13),e20) = h4(e11),
inference(paramod,[status(thm)],[c_1846,c_1845]) ).
cnf(c_1941,plain,
( op2(e23,e21) = e23
| op2(e20,e21) = e20 ),
inference(resolve,[status(thm)],[c_1870,c_328]) ).
cnf(c_1943,plain,
( op2(e23,e20) = e22
| op2(e21,e20) = e22
| h1(e13) = e22 ),
inference(resolve,[status(thm)],[c_1871,c_1729]) ).
cnf(c_1945,plain,
( op2(e23,e20) = e23
| op2(e21,e20) = e21 ),
inference(resolve,[status(thm)],[c_1871,c_320]) ).
cnf(c_1952,plain,
( op1(e13,e11) = e13
| op1(e10,e11) = e10 ),
inference(resolve,[status(thm)],[c_1923,c_296]) ).
cnf(c_1956,plain,
( op1(e13,e10) = e13
| op1(e11,e10) = e11 ),
inference(resolve,[status(thm)],[c_1924,c_288]) ).
cnf(c_1957,plain,
( op1(e13,e10) = e12
| op1(e11,e10) = e12
| op1(e10,e10) = e12 ),
inference(resolve,[status(thm)],[c_1924,c_40]) ).
cnf(c_1980,plain,
( op2(e23,e21) != e23
| h1(e13) = e23 ),
inference(paramod,[status(thm)],[c_1728,c_190]) ).
cnf(c_2326,plain,
( e22 != h2(e13)
| op2(e20,e22) = e22
| h1(e13) = e22 ),
inference(paramod,[status(thm)],[c_1730,c_1742]) ).
cnf(c_1992,plain,
( h2(e13) != e22
| op2(e20,e22) = e22
| h1(e13) = e22 ),
inference(copy,[status(thm)],[c_2326]) ).
cnf(c_2001,plain,
( op1(e13,e11) != e13
| op1(e10,e10) = e13 ),
inference(paramod,[status(thm)],[c_1822,c_126]) ).
cnf(c_2024,plain,
( op1(e11,e12) != e10
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_1841,c_131]) ).
cnf(c_2025,plain,
( op1(e10,e10) != e10
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_1841,c_149]) ).
cnf(c_2026,plain,
( op1(e10,e11) != e10
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_1841,c_152]) ).
cnf(c_2036,plain,
( op2(e21,e22) != e20
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_1857,c_195]) ).
cnf(c_2037,plain,
( op2(e20,e21) != e20
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_1857,c_216]) ).
cnf(c_2327,plain,
( e20 != h1(e13)
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_1857,c_1722]) ).
cnf(c_2038,plain,
( h1(e13) != e20
| op2(e20,e22) = e22 ),
inference(copy,[status(thm)],[c_2327]) ).
cnf(c_2328,plain,
( e20 = e21
| op2(e20,e22) = e20
| op2(e20,e22) = e20 ),
inference(paramod,[status(thm)],[c_1858,c_1854]) ).
cnf(c_2329,plain,
( e21 = e20
| op2(e20,e22) = e20
| op2(e20,e22) = e20 ),
inference(copy,[status(thm)],[c_2328]) ).
cnf(c_2330,plain,
( e21 = e20
| op2(e20,e22) = e20 ),
inference(copy,[status(thm)],[c_2329]) ).
cnf(c_2041,plain,
op2(e20,e22) = e20,
inference(resolve,[status(thm)],[c_251,c_2330]) ).
cnf(c_2331,plain,
( h1(e13) != e20
| e20 = e22 ),
inference(paramod,[status(thm)],[c_2041,c_2038]) ).
cnf(c_2042,plain,
h1(e13) != e20,
inference(resolve,[status(thm)],[c_253,c_2331]) ).
cnf(c_2332,plain,
( op2(e20,e21) != e20
| e20 = e22 ),
inference(paramod,[status(thm)],[c_2041,c_2037]) ).
cnf(c_2043,plain,
op2(e20,e21) != e20,
inference(resolve,[status(thm)],[c_253,c_2332]) ).
cnf(c_2333,plain,
( op2(e21,e22) != e20
| e20 = e22 ),
inference(paramod,[status(thm)],[c_2041,c_2036]) ).
cnf(c_2044,plain,
op2(e21,e22) != e20,
inference(resolve,[status(thm)],[c_253,c_2333]) ).
cnf(c_2334,plain,
( h2(e13) != e22
| e20 = e22
| h1(e13) = e22 ),
inference(paramod,[status(thm)],[c_2041,c_1992]) ).
cnf(c_2045,plain,
( h2(e13) != e22
| h1(e13) = e22 ),
inference(resolve,[status(thm)],[c_253,c_2334]) ).
cnf(c_2050,negated_conjecture,
( h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != e20
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_2041,c_1915]) ).
cnf(c_2335,plain,
( e20 = e22
| op2(e20,e21) = e22
| h1(e13) = e22 ),
inference(paramod,[status(thm)],[c_2041,c_1730]) ).
cnf(c_2051,plain,
( op2(e20,e21) = e22
| h1(e13) = e22 ),
inference(resolve,[status(thm)],[c_253,c_2335]) ).
cnf(c_2058,plain,
( op2(e22,e20) = e20
| op2(e21,e20) = e20 ),
inference(resolve,[status(thm)],[c_2042,c_1861]) ).
cnf(c_2059,plain,
op2(e23,e21) = e23,
inference(resolve,[status(thm)],[c_2043,c_1941]) ).
cnf(c_2065,plain,
( h2(e13) = e20
| op2(e21,e20) = e20 ),
inference(resolve,[status(thm)],[c_2044,c_1864]) ).
cnf(c_2067,negated_conjecture,
( h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != e20
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(paramod,[status(thm)],[c_2059,c_2050]) ).
cnf(c_2336,plain,
( e23 != e23
| h1(e13) = e23 ),
inference(paramod,[status(thm)],[c_2059,c_1980]) ).
cnf(c_2068,plain,
h1(e13) = e23,
inference(copy,[status(thm)],[c_2336]) ).
cnf(c_2337,plain,
( e23 = e21
| op2(e22,e21) = e21
| h2(e13) = e21 ),
inference(paramod,[status(thm)],[c_2059,c_1931]) ).
cnf(c_2070,plain,
( op2(e22,e21) = e21
| h2(e13) = e21 ),
inference(resolve,[status(thm)],[c_257,c_2337]) ).
cnf(c_2338,plain,
( op2(e23,e22) = e21
| e23 = e21
| op2(e23,e20) = e21 ),
inference(paramod,[status(thm)],[c_2059,c_1761]) ).
cnf(c_2071,plain,
( op2(e23,e22) = e21
| op2(e23,e20) = e21 ),
inference(resolve,[status(thm)],[c_257,c_2338]) ).
cnf(c_2075,negated_conjecture,
( h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != e20
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_2068,c_2067]) ).
cnf(c_2339,plain,
( op2(e20,e21) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_2068,c_2051]) ).
cnf(c_2078,plain,
op2(e20,e21) = e22,
inference(resolve,[status(thm)],[c_258,c_2339]) ).
cnf(c_2340,plain,
( h2(e13) != e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_2068,c_2045]) ).
cnf(c_2079,plain,
h2(e13) != e22,
inference(resolve,[status(thm)],[c_258,c_2340]) ).
cnf(c_2341,plain,
( op2(e23,e20) = e22
| op2(e21,e20) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_2068,c_1943]) ).
cnf(c_2080,plain,
( op2(e23,e20) = e22
| op2(e21,e20) = e22 ),
inference(resolve,[status(thm)],[c_258,c_2341]) ).
cnf(c_2081,plain,
op2(e23,e20) = h4(e11),
inference(paramod,[status(thm)],[c_2068,c_1933]) ).
cnf(c_2342,plain,
h4(e11) != h1(e13),
inference(paramod,[status(thm)],[c_2081,c_1724]) ).
cnf(c_2083,plain,
h4(e11) != e23,
inference(paramod,[status(thm)],[c_2068,c_2342]) ).
cnf(c_2343,plain,
( h4(e11) = e23
| op2(e21,e20) = e21 ),
inference(paramod,[status(thm)],[c_2081,c_1945]) ).
cnf(c_2086,plain,
op2(e21,e20) = e21,
inference(resolve,[status(thm)],[c_2083,c_2343]) ).
cnf(c_2344,negated_conjecture,
( h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e12)) != e20
| h3(op1(e10,e11)) != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_2078,c_2075]) ).
cnf(c_2345,negated_conjecture,
( h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e12)) != e20
| h3(op1(e10,e11)) != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_2086,c_2344]) ).
cnf(c_2088,negated_conjecture,
( h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != h4(e11)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e12)) != e20
| h3(op1(e10,e11)) != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_2081,c_2345]) ).
cnf(c_2346,plain,
( op2(e21,e22) = e22
| h2(e13) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_2086,c_1866]) ).
cnf(c_2347,plain,
( op2(e21,e22) = e22
| h2(e13) = e22 ),
inference(resolve,[status(thm)],[c_256,c_2346]) ).
cnf(c_2090,plain,
op2(e21,e22) = e22,
inference(resolve,[status(thm)],[c_2079,c_2347]) ).
cnf(c_2348,plain,
( op2(e23,e20) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_2086,c_2080]) ).
cnf(c_2349,plain,
( h4(e11) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_2081,c_2348]) ).
cnf(c_2091,plain,
h4(e11) = e22,
inference(resolve,[status(thm)],[c_256,c_2349]) ).
cnf(c_2350,plain,
( op2(e23,e22) = e21
| h4(e11) = e21 ),
inference(paramod,[status(thm)],[c_2081,c_2071]) ).
cnf(c_2351,plain,
( op2(e23,e22) = e21
| e22 = e21 ),
inference(paramod,[status(thm)],[c_2091,c_2350]) ).
cnf(c_2352,plain,
( op2(e23,e22) = e21
| e21 = e22 ),
inference(copy,[status(thm)],[c_2351]) ).
cnf(c_2092,plain,
op2(e23,e22) = e21,
inference(resolve,[status(thm)],[c_256,c_2352]) ).
cnf(c_2353,plain,
( h2(e13) = e20
| e21 = e20 ),
inference(paramod,[status(thm)],[c_2086,c_2065]) ).
cnf(c_2093,plain,
h2(e13) = e20,
inference(resolve,[status(thm)],[c_251,c_2353]) ).
cnf(c_2354,plain,
( op2(e22,e20) = e20
| e21 = e20 ),
inference(paramod,[status(thm)],[c_2086,c_2058]) ).
cnf(c_2094,plain,
op2(e22,e20) = e20,
inference(resolve,[status(thm)],[c_251,c_2354]) ).
cnf(c_2355,negated_conjecture,
( h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != h4(e11)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e12)) != e20
| h3(op1(e10,e11)) != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_2093,c_2088]) ).
cnf(c_2356,negated_conjecture,
( h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != h4(e11)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e12)) != e20
| h3(op1(e10,e11)) != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_2090,c_2355]) ).
cnf(c_2357,negated_conjecture,
( h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != h4(e11)
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e12)) != e20
| h3(op1(e10,e11)) != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_2094,c_2356]) ).
cnf(c_2358,negated_conjecture,
( h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e12)) != e20
| h3(op1(e10,e11)) != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_2091,c_2357]) ).
cnf(c_2095,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != op2(e22,e21)
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e12)) != e20
| h3(op1(e10,e11)) != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_2092,c_2358]) ).
cnf(c_2359,plain,
( op2(e22,e21) = e21
| e20 = e21 ),
inference(paramod,[status(thm)],[c_2093,c_2070]) ).
cnf(c_2360,plain,
( op2(e22,e21) = e21
| e21 = e20 ),
inference(copy,[status(thm)],[c_2359]) ).
cnf(c_2097,plain,
op2(e22,e21) = e21,
inference(resolve,[status(thm)],[c_251,c_2360]) ).
cnf(c_2101,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e12)) != e20
| h3(op1(e10,e11)) != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_2097,c_2095]) ).
cnf(c_2109,plain,
( op1(e13,e11) != e13
| op1(e10,e11) = e12
| op1(e10,e11) = e10 ),
inference(paramod,[status(thm)],[c_1874,c_126]) ).
cnf(c_2361,plain,
( e12 != op1(e10,e11)
| op1(e11,e12) = e12
| op1(e11,e10) = e12 ),
inference(paramod,[status(thm)],[c_1920,c_123]) ).
cnf(c_2118,plain,
( op1(e10,e11) != e12
| op1(e11,e12) = e12
| op1(e11,e10) = e12 ),
inference(copy,[status(thm)],[c_2361]) ).
cnf(c_2362,plain,
( e10 = e11
| op1(e10,e12) = e10
| op1(e10,e12) = e10 ),
inference(paramod,[status(thm)],[c_1925,c_1838]) ).
cnf(c_2363,plain,
( e11 = e10
| op1(e10,e12) = e10
| op1(e10,e12) = e10 ),
inference(copy,[status(thm)],[c_2362]) ).
cnf(c_2364,plain,
( e11 = e10
| op1(e10,e12) = e10 ),
inference(copy,[status(thm)],[c_2363]) ).
cnf(c_2129,plain,
op1(e10,e12) = e10,
inference(resolve,[status(thm)],[c_243,c_2364]) ).
cnf(c_2365,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| h3(e10) != e20
| h3(op1(e10,e11)) != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_2129,c_2101]) ).
cnf(c_2366,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| e20 != e20
| h3(op1(e10,e11)) != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_1706,c_2365]) ).
cnf(c_2131,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e11)) != e22
| h3(op1(e10,e10)) != e23 ),
inference(copy,[status(thm)],[c_2366]) ).
cnf(c_2367,plain,
( op1(e10,e11) != e10
| e10 = e12 ),
inference(paramod,[status(thm)],[c_2129,c_2026]) ).
cnf(c_2132,plain,
op1(e10,e11) != e10,
inference(resolve,[status(thm)],[c_245,c_2367]) ).
cnf(c_2368,plain,
( op1(e10,e10) != e10
| e10 = e12 ),
inference(paramod,[status(thm)],[c_2129,c_2025]) ).
cnf(c_2133,plain,
op1(e10,e10) != e10,
inference(resolve,[status(thm)],[c_245,c_2368]) ).
cnf(c_2369,plain,
( op1(e11,e12) != e10
| e10 = e12 ),
inference(paramod,[status(thm)],[c_2129,c_2024]) ).
cnf(c_2134,plain,
op1(e11,e12) != e10,
inference(resolve,[status(thm)],[c_245,c_2369]) ).
cnf(c_2143,plain,
( op1(e13,e11) != e13
| op1(e10,e11) = e12 ),
inference(resolve,[status(thm)],[c_2132,c_2109]) ).
cnf(c_2144,plain,
op1(e13,e11) = e13,
inference(resolve,[status(thm)],[c_2132,c_1952]) ).
cnf(c_2149,plain,
( op1(e12,e10) = e10
| op1(e11,e10) = e10 ),
inference(resolve,[status(thm)],[c_2133,c_1928]) ).
cnf(c_2156,plain,
( op1(e11,e11) = e10
| op1(e11,e10) = e10 ),
inference(resolve,[status(thm)],[c_2134,c_1921]) ).
cnf(c_2370,plain,
( e13 != e13
| op1(e10,e11) = e12 ),
inference(paramod,[status(thm)],[c_2144,c_2143]) ).
cnf(c_2157,plain,
op1(e10,e11) = e12,
inference(copy,[status(thm)],[c_2370]) ).
cnf(c_2371,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| h3(e12) != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_2157,c_2131]) ).
cnf(c_2372,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e13,e11)) != e23
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| e22 != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_374,c_2371]) ).
cnf(c_2373,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(e13) != e23
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| e22 != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_2144,c_2372]) ).
cnf(c_2374,negated_conjecture,
( h3(op1(e13,e12)) != e21
| e23 != e23
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| e22 != e22
| h3(op1(e10,e10)) != e23 ),
inference(paramod,[status(thm)],[c_380,c_2373]) ).
cnf(c_2375,negated_conjecture,
( h3(op1(e13,e12)) != e21
| e23 != e23
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e10)) != e23 ),
inference(copy,[status(thm)],[c_2374]) ).
cnf(c_2158,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e10)) != e23 ),
inference(copy,[status(thm)],[c_2375]) ).
cnf(c_2376,plain,
( e13 != e13
| op1(e10,e10) = e13 ),
inference(paramod,[status(thm)],[c_2144,c_2001]) ).
cnf(c_2159,plain,
op1(e10,e10) = e13,
inference(copy,[status(thm)],[c_2376]) ).
cnf(c_2377,plain,
( e13 = e11
| op1(e12,e11) = e11
| op1(e11,e11) = e11 ),
inference(paramod,[status(thm)],[c_2144,c_1873]) ).
cnf(c_2160,plain,
( op1(e12,e11) = e11
| op1(e11,e11) = e11 ),
inference(resolve,[status(thm)],[c_249,c_2377]) ).
cnf(c_2378,plain,
( op1(e13,e12) = e11
| e13 = e11
| op1(e13,e10) = e11 ),
inference(paramod,[status(thm)],[c_2144,c_1830]) ).
cnf(c_2161,plain,
( op1(e13,e12) = e11
| op1(e13,e10) = e11 ),
inference(resolve,[status(thm)],[c_249,c_2378]) ).
cnf(c_2379,plain,
e13 != op1(e13,e10),
inference(paramod,[status(thm)],[c_2144,c_171]) ).
cnf(c_2163,plain,
op1(e13,e10) != e13,
inference(copy,[status(thm)],[c_2379]) ).
cnf(c_2380,plain,
( e12 != e12
| op1(e11,e12) = e12
| op1(e11,e10) = e12 ),
inference(paramod,[status(thm)],[c_2157,c_2118]) ).
cnf(c_2164,plain,
( op1(e11,e12) = e12
| op1(e11,e10) = e12 ),
inference(copy,[status(thm)],[c_2380]) ).
cnf(c_2381,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| h3(e13) != e23 ),
inference(paramod,[status(thm)],[c_2159,c_2158]) ).
cnf(c_2382,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21
| e23 != e23 ),
inference(paramod,[status(thm)],[c_380,c_2381]) ).
cnf(c_2166,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(op1(e11,e10)) != e21 ),
inference(copy,[status(thm)],[c_2382]) ).
cnf(c_2383,plain,
( op1(e13,e10) = e12
| op1(e11,e10) = e12
| e13 = e12 ),
inference(paramod,[status(thm)],[c_2159,c_1957]) ).
cnf(c_2167,plain,
( op1(e13,e10) = e12
| op1(e11,e10) = e12 ),
inference(resolve,[status(thm)],[c_250,c_2383]) ).
cnf(c_2168,plain,
op1(e11,e10) = e11,
inference(resolve,[status(thm)],[c_2163,c_1956]) ).
cnf(c_2384,plain,
( op1(e13,e10) = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_2168,c_2167]) ).
cnf(c_2171,plain,
op1(e13,e10) = e12,
inference(resolve,[status(thm)],[c_248,c_2384]) ).
cnf(c_2385,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| h3(e11) != e21 ),
inference(paramod,[status(thm)],[c_2168,c_2166]) ).
cnf(c_2386,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e13,e10)) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1847,c_2385]) ).
cnf(c_2387,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(e12) != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_2171,c_2386]) ).
cnf(c_2388,negated_conjecture,
( h3(op1(e13,e12)) != e21
| e22 != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_374,c_2387]) ).
cnf(c_2389,negated_conjecture,
( h3(op1(e13,e12)) != e21
| e22 != e22
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20 ),
inference(copy,[status(thm)],[c_2388]) ).
cnf(c_2172,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(op1(e11,e11)) != e20 ),
inference(copy,[status(thm)],[c_2389]) ).
cnf(c_2390,plain,
( op1(e11,e12) = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_2168,c_2164]) ).
cnf(c_2173,plain,
op1(e11,e12) = e12,
inference(resolve,[status(thm)],[c_248,c_2390]) ).
cnf(c_2391,plain,
( op1(e11,e11) = e10
| e11 = e10 ),
inference(paramod,[status(thm)],[c_2168,c_2156]) ).
cnf(c_2174,plain,
op1(e11,e11) = e10,
inference(resolve,[status(thm)],[c_243,c_2391]) ).
cnf(c_2392,plain,
( op1(e12,e10) = e10
| e11 = e10 ),
inference(paramod,[status(thm)],[c_2168,c_2149]) ).
cnf(c_2176,plain,
op1(e12,e10) = e10,
inference(resolve,[status(thm)],[c_243,c_2392]) ).
cnf(c_2393,plain,
( op1(e13,e12) = e11
| e12 = e11 ),
inference(paramod,[status(thm)],[c_2171,c_2161]) ).
cnf(c_2394,plain,
( op1(e13,e12) = e11
| e11 = e12 ),
inference(copy,[status(thm)],[c_2393]) ).
cnf(c_2177,plain,
op1(e13,e12) = e11,
inference(resolve,[status(thm)],[c_248,c_2394]) ).
cnf(c_2395,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| h3(e10) != e20 ),
inference(paramod,[status(thm)],[c_2174,c_2172]) ).
cnf(c_2396,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(op1(e11,e12)) != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_1706,c_2395]) ).
cnf(c_2397,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| h3(e12) != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2173,c_2396]) ).
cnf(c_2398,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e12,e11)) != e21
| h3(op1(e12,e10)) != e20
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_374,c_2397]) ).
cnf(c_2399,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e12,e11)) != e21
| h3(e10) != e20
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2176,c_2398]) ).
cnf(c_2400,negated_conjecture,
( h3(op1(e13,e12)) != e21
| h3(op1(e12,e11)) != e21
| e20 != e20
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_1706,c_2399]) ).
cnf(c_2401,negated_conjecture,
( h3(e11) != e21
| h3(op1(e12,e11)) != e21
| e20 != e20
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2177,c_2400]) ).
cnf(c_2402,negated_conjecture,
( e21 != e21
| h3(op1(e12,e11)) != e21
| e20 != e20
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_1847,c_2401]) ).
cnf(c_2403,negated_conjecture,
( e21 != e21
| h3(op1(e12,e11)) != e21
| e20 != e20
| e22 != e22 ),
inference(copy,[status(thm)],[c_2402]) ).
cnf(c_2404,negated_conjecture,
( e21 != e21
| h3(op1(e12,e11)) != e21
| e20 != e20 ),
inference(copy,[status(thm)],[c_2403]) ).
cnf(c_2405,negated_conjecture,
( e21 != e21
| h3(op1(e12,e11)) != e21 ),
inference(copy,[status(thm)],[c_2404]) ).
cnf(c_2178,negated_conjecture,
h3(op1(e12,e11)) != e21,
inference(copy,[status(thm)],[c_2405]) ).
cnf(c_2406,plain,
( op1(e12,e11) = e11
| e10 = e11 ),
inference(paramod,[status(thm)],[c_2174,c_2160]) ).
cnf(c_2407,plain,
( op1(e12,e11) = e11
| e11 = e10 ),
inference(copy,[status(thm)],[c_2406]) ).
cnf(c_2179,plain,
op1(e12,e11) = e11,
inference(resolve,[status(thm)],[c_243,c_2407]) ).
cnf(c_2408,negated_conjecture,
h3(e11) != e21,
inference(paramod,[status(thm)],[c_2179,c_2178]) ).
cnf(c_2409,negated_conjecture,
e21 != e21,
inference(paramod,[status(thm)],[c_1847,c_2408]) ).
cnf(c_2180,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_2409]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG110+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.08/5.37 % Computer : n006.cluster.edu
% 0.08/5.37 % Model : x86_64 x86_64
% 0.08/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.37 % Memory : 8046.5625MB
% 0.08/5.37 % OS : Linux 6.8.0-71-generic
% 0.08/5.37 % CPULimit : 300
% 0.08/5.37 % WCLimit : 300
% 0.08/5.37 % DateTime : Sat Sep 26 21:10:05 UTC 2026
% 0.08/5.37 % CPUTime :
% 0.08/5.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/5.37 % Process 2116177 was started by sandbox on n006,
% 0.08/5.37 % Sat Sep 26 21:10:05 2026
% 0.08/5.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 4.55/9.83
% 4.55/9.83 % From the command line: assign(max_seconds, 300).
% 9.75/10.53
% 9.75/10.53 % SZS status Theorem for theBenchmark
% 9.75/10.53
% 9.75/10.53 % Proof 1 at 0.59 (+ 0.06) seconds.
% 9.75/10.53 % Length of proof is 261.
% 9.75/10.53 % Level of proof is 22.
% 9.75/10.53 % Maximum clause weight is 153.000.
% 9.75/10.53 % Given clauses 165.
% 9.75/10.53
% 9.75/10.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------