%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG114+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:49:32 AM UTC 2026
% Result : Theorem 4.77s 5.32s
% Output : CNFRefutation 4.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 122
% Number of leaves : 17
% Syntax : Number of formulae : 457 ( 158 unt; 0 def)
% Number of atoms : 3220 (3219 equ)
% Maximal formula atoms : 128 ( 7 avg)
% Number of connectives : 4704 (1941 ~;2361 |; 402 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 6 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
( ( op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e13,e13) = e10 )
& ( op1(e13,e12) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11
| op1(e13,e12) = e10 )
& ( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e13,e11) = e10 )
& ( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 )
& ( op1(e12,e13) = e13
| op1(e12,e13) = e12
| op1(e12,e13) = e11
| op1(e12,e13) = e10 )
& ( op1(e12,e12) = e13
| op1(e12,e12) = e12
| op1(e12,e12) = e11
| op1(e12,e12) = e10 )
& ( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 )
& ( op1(e12,e10) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 )
& ( op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11
| op1(e11,e13) = e10 )
& ( op1(e11,e12) = e13
| op1(e11,e12) = e12
| op1(e11,e12) = e11
| op1(e11,e12) = e10 )
& ( op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e11) = e10 )
& ( op1(e11,e10) = e13
| op1(e11,e10) = e12
| op1(e11,e10) = e11
| op1(e11,e10) = e10 )
& ( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 )
& ( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 )
& ( op1(e10,e11) = e13
| op1(e10,e11) = e12
| op1(e10,e11) = e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e11
| op1(e10,e10) = e10 ) ),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
( ( op1(e13,e13) = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| op1(e10,e13) = e13 )
& ( op1(e13,e13) = e13
| op1(e13,e12) = e13
| op1(e13,e11) = e13
| op1(e13,e10) = e13 )
& ( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 )
& ( op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 )
& ( op1(e13,e13) = e11
| op1(e12,e13) = e11
| op1(e11,e13) = e11
| op1(e10,e13) = e11 )
& ( op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 )
& ( op1(e13,e13) = e10
| op1(e12,e13) = e10
| op1(e11,e13) = e10
| op1(e10,e13) = e10 )
& ( op1(e13,e13) = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 )
& ( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| op1(e10,e12) = e13 )
& ( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 )
& ( op1(e13,e12) = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 )
& ( op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 )
& ( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 )
& ( op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 )
& ( op1(e13,e12) = e10
| op1(e12,e12) = e10
| op1(e11,e12) = e10
| op1(e10,e12) = e10 )
& ( op1(e12,e13) = e10
| op1(e12,e12) = e10
| op1(e12,e11) = e10
| op1(e12,e10) = e10 )
& ( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| op1(e10,e11) = e13 )
& ( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e11) = e13
| op1(e11,e10) = e13 )
& ( op1(e13,e11) = e12
| op1(e12,e11) = e12
| op1(e11,e11) = e12
| op1(e10,e11) = e12 )
& ( op1(e11,e13) = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 )
& ( op1(e13,e11) = e11
| op1(e12,e11) = e11
| op1(e11,e11) = e11
| op1(e10,e11) = e11 )
& ( op1(e11,e13) = e11
| op1(e11,e12) = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 )
& ( op1(e13,e11) = e10
| op1(e12,e11) = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 )
& ( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 )
& ( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| op1(e10,e10) = e13 )
& ( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 )
& ( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| op1(e10,e10) = e12 )
& ( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 )
& ( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11
| op1(e10,e10) = e11 )
& ( op1(e10,e13) = e11
| op1(e10,e12) = e11
| op1(e10,e11) = e11
| op1(e10,e10) = e11 )
& ( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 )
& ( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ) ),
file('theBenchmark.p',ax2) ).
fof(ax3,axiom,
( ( op2(e23,e23) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e23,e23) = e20 )
& ( op2(e23,e22) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21
| op2(e23,e22) = e20 )
& ( op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e23,e21) = e21
| op2(e23,e21) = e20 )
& ( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 )
& ( op2(e22,e23) = e23
| op2(e22,e23) = e22
| op2(e22,e23) = e21
| op2(e22,e23) = e20 )
& ( op2(e22,e22) = e23
| op2(e22,e22) = e22
| op2(e22,e22) = e21
| op2(e22,e22) = e20 )
& ( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 )
& ( op2(e22,e20) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 )
& ( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| op2(e21,e23) = e20 )
& ( op2(e21,e22) = e23
| op2(e21,e22) = e22
| op2(e21,e22) = e21
| op2(e21,e22) = e20 )
& ( op2(e21,e21) = e23
| op2(e21,e21) = e22
| op2(e21,e21) = e21
| op2(e21,e21) = e20 )
& ( op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e21
| op2(e21,e20) = e20 )
& ( op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 )
& ( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| op2(e20,e22) = e20 )
& ( op2(e20,e21) = e23
| op2(e20,e21) = e22
| op2(e20,e21) = e21
| op2(e20,e21) = e20 )
& ( op2(e20,e20) = e23
| op2(e20,e20) = e22
| op2(e20,e20) = e21
| op2(e20,e20) = e20 ) ),
file('theBenchmark.p',ax3) ).
fof(ax4,axiom,
( ( op2(e23,e23) = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| op2(e20,e23) = e23 )
& ( op2(e23,e23) = e23
| op2(e23,e22) = e23
| op2(e23,e21) = e23
| op2(e23,e20) = e23 )
& ( op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 )
& ( op2(e23,e23) = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 )
& ( op2(e23,e23) = e21
| op2(e22,e23) = e21
| op2(e21,e23) = e21
| op2(e20,e23) = e21 )
& ( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 )
& ( op2(e23,e23) = e20
| op2(e22,e23) = e20
| op2(e21,e23) = e20
| op2(e20,e23) = e20 )
& ( op2(e23,e23) = e20
| op2(e23,e22) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 )
& ( op2(e23,e22) = e23
| op2(e22,e22) = e23
| op2(e21,e22) = e23
| op2(e20,e22) = e23 )
& ( op2(e22,e23) = e23
| op2(e22,e22) = e23
| op2(e22,e21) = e23
| op2(e22,e20) = e23 )
& ( op2(e23,e22) = e22
| op2(e22,e22) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 )
& ( op2(e22,e23) = e22
| op2(e22,e22) = e22
| op2(e22,e21) = e22
| op2(e22,e20) = e22 )
& ( op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 )
& ( op2(e22,e23) = e21
| op2(e22,e22) = e21
| op2(e22,e21) = e21
| op2(e22,e20) = e21 )
& ( op2(e23,e22) = e20
| op2(e22,e22) = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 )
& ( op2(e22,e23) = e20
| op2(e22,e22) = e20
| op2(e22,e21) = e20
| op2(e22,e20) = e20 )
& ( op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e21,e21) = e23
| op2(e20,e21) = e23 )
& ( op2(e21,e23) = e23
| op2(e21,e22) = e23
| op2(e21,e21) = e23
| op2(e21,e20) = e23 )
& ( op2(e23,e21) = e22
| op2(e22,e21) = e22
| op2(e21,e21) = e22
| op2(e20,e21) = e22 )
& ( op2(e21,e23) = e22
| op2(e21,e22) = e22
| op2(e21,e21) = e22
| op2(e21,e20) = e22 )
& ( op2(e23,e21) = e21
| op2(e22,e21) = e21
| op2(e21,e21) = e21
| op2(e20,e21) = e21 )
& ( op2(e21,e23) = e21
| op2(e21,e22) = e21
| op2(e21,e21) = e21
| op2(e21,e20) = e21 )
& ( op2(e23,e21) = e20
| op2(e22,e21) = e20
| op2(e21,e21) = e20
| op2(e20,e21) = e20 )
& ( op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20
| op2(e21,e20) = e20 )
& ( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| op2(e20,e20) = e23 )
& ( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 )
& ( op2(e23,e20) = e22
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| op2(e20,e20) = e22 )
& ( op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| op2(e20,e20) = e22 )
& ( op2(e23,e20) = e21
| op2(e22,e20) = e21
| op2(e21,e20) = e21
| op2(e20,e20) = e21 )
& ( op2(e20,e23) = e21
| op2(e20,e22) = e21
| op2(e20,e21) = e21
| op2(e20,e20) = e21 )
& ( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| op2(e20,e20) = e20 )
& ( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ) ),
file('theBenchmark.p',ax4) ).
fof(ax5,axiom,
( op1(e13,e12) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e11)
& op1(e12,e12) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e11)
& op1(e11,e12) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e11)
& op1(e10,e12) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e11)
& op1(e12,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e11,e13)
& op1(e12,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e11,e12)
& op1(e12,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e11,e11)
& op1(e12,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e11,e10) ),
file('theBenchmark.p',ax5) ).
fof(ax6,axiom,
( op2(e23,e22) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e21)
& op2(e22,e22) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e21)
& op2(e21,e22) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e21)
& op2(e20,e22) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e21)
& op2(e22,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e21,e23)
& op2(e22,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e21,e22)
& op2(e22,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e21,e21)
& op2(e22,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e21,e20) ),
file('theBenchmark.p',ax6) ).
fof(ax7,axiom,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('theBenchmark.p',ax7) ).
fof(ax8,axiom,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('theBenchmark.p',ax8) ).
fof(ax10,axiom,
( ( ( op1(e13,e13) != e13
& op1(e13,e13) = e13 )
| ( op1(e13,e13) != e12
& op1(e12,e12) = e13 )
| ( op1(e13,e13) != e11
& op1(e11,e11) = e13 )
| ( op1(e13,e13) != e10
& op1(e10,e10) = e13 ) )
& ( ( op1(e12,e12) != e13
& op1(e13,e13) = e12 )
| ( op1(e12,e12) != e12
& op1(e12,e12) = e12 )
| ( op1(e12,e12) != e11
& op1(e11,e11) = e12 )
| ( op1(e12,e12) != e10
& op1(e10,e10) = e12 ) )
& ( ( op1(e11,e11) != e13
& op1(e13,e13) = e11 )
| ( op1(e11,e11) != e12
& op1(e12,e12) = e11 )
| ( op1(e11,e11) != e11
& op1(e11,e11) = e11 )
| ( op1(e11,e11) != e10
& op1(e10,e10) = e11 ) )
& ( ( op1(e10,e10) != e13
& op1(e13,e13) = e10 )
| ( op1(e10,e10) != e12
& op1(e12,e12) = e10 )
| ( op1(e10,e10) != e11
& op1(e11,e11) = e10 )
| ( 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,e23) != e22
& op2(e22,e22) = e23 )
| ( op2(e23,e23) != e21
& op2(e21,e21) = e23 )
| ( op2(e23,e23) != e20
& op2(e20,e20) = e23 ) )
& ( ( op2(e22,e22) != e23
& op2(e23,e23) = e22 )
| ( op2(e22,e22) != e22
& op2(e22,e22) = e22 )
| ( op2(e22,e22) != e21
& op2(e21,e21) = e22 )
| ( op2(e22,e22) != e20
& op2(e20,e20) = e22 ) )
& ( ( op2(e21,e21) != e23
& op2(e23,e23) = e21 )
| ( op2(e21,e21) != e22
& op2(e22,e22) = e21 )
| ( op2(e21,e21) != e21
& op2(e21,e21) = e21 )
| ( op2(e21,e21) != e20
& op2(e20,e20) = e21 ) )
& ( ( op2(e20,e20) != e23
& op2(e23,e23) = e20 )
| ( op2(e20,e20) != e22
& op2(e22,e22) = e20 )
| ( op2(e20,e20) != e21
& op2(e21,e21) = e20 )
| ( op2(e20,e20) != e20
& op2(e20,e20) = e20 ) ) ),
file('theBenchmark.p',ax11) ).
fof(ax12,axiom,
( e13 = op1(e12,e12)
& e11 = op1(op1(e12,e12),op1(e12,e12))
& e10 = op1(op1(e12,e12),e12) ),
file('theBenchmark.p',ax12) ).
fof(ax13,axiom,
( e23 = op2(e22,e22)
& e21 = op2(op2(e22,e22),op2(e22,e22))
& e20 = op2(op2(e22,e22),e22) ),
file('theBenchmark.p',ax13) ).
fof(ax14,axiom,
( h1(e13) = op2(e20,e20)
& h1(e11) = op2(op2(e20,e20),op2(e20,e20))
& h1(e10) = op2(op2(e20,e20),e20)
& h1(e12) = e20 ),
file('theBenchmark.p',ax14) ).
fof(ax15,axiom,
( h2(e13) = op2(e21,e21)
& h2(e11) = op2(op2(e21,e21),op2(e21,e21))
& h2(e10) = op2(op2(e21,e21),e21)
& h2(e12) = e21 ),
file('theBenchmark.p',ax15) ).
fof(ax16,axiom,
( h3(e13) = op2(e22,e22)
& h3(e11) = op2(op2(e22,e22),op2(e22,e22))
& h3(e10) = op2(op2(e22,e22),e22)
& h3(e12) = e22 ),
file('theBenchmark.p',ax16) ).
fof(ax17,axiom,
( h4(e13) = op2(e23,e23)
& h4(e11) = op2(op2(e23,e23),op2(e23,e23))
& h4(e10) = op2(op2(e23,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_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_31,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_35,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_36,plain,
( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_38,plain,
( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11
| op1(e10,e10) = e11 ),
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_48,plain,
( op1(e13,e11) = e12
| op1(e12,e11) = e12
| op1(e11,e11) = e12
| op1(e10,e11) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_53,plain,
( op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_55,plain,
( op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_56,plain,
( op1(e13,e12) = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_66,plain,
( op1(e13,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_79,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_83,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_84,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| op2(e20,e20) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_86,plain,
( op2(e23,e20) = e21
| op2(e22,e20) = e21
| op2(e21,e20) = e21
| op2(e20,e20) = e21 ),
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_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_103,plain,
( op2(e22,e23) = e22
| op2(e22,e22) = e22
| op2(e22,e21) = e22
| op2(e22,e20) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_104,plain,
( op2(e23,e22) = e22
| op2(e22,e22) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_111,plain,
( op2(e23,e23) = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_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_118,plain,
op1(e13,e10) != op1(e10,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_123,plain,
op1(e11,e11) != op1(e10,e11),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_132,plain,
op1(e12,e12) != op1(e10,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_133,plain,
op1(e10,e12) != op1(e12,e12),
inference(copy,[status(thm)],[c_132]) ).
cnf(c_134,plain,
op1(e13,e12) != op1(e10,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_146,plain,
op1(e13,e13) != op1(e12,e13),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_147,plain,
op1(e10,e11) != op1(e10,e10),
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_155,plain,
op1(e11,e11) != op1(e11,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_170,plain,
op1(e12,e13) != op1(e12,e12),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_172,plain,
op1(e13,e12) != op1(e13,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_173,plain,
op1(e13,e10) != op1(e13,e12),
inference(copy,[status(thm)],[c_172]) ).
cnf(c_174,plain,
op1(e13,e13) != op1(e13,e10),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_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_196,plain,
op2(e22,e22) != op2(e20,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_197,plain,
op2(e20,e22) != op2(e22,e22),
inference(copy,[status(thm)],[c_196]) ).
cnf(c_198,plain,
op2(e23,e22) != op2(e20,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_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_219,plain,
op2(e21,e21) != op2(e21,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_234,plain,
op2(e22,e23) != op2(e22,e22),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_236,plain,
op2(e23,e22) != op2(e23,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_237,plain,
op2(e23,e20) != op2(e23,e22),
inference(copy,[status(thm)],[c_236]) ).
cnf(c_238,plain,
op2(e23,e23) != op2(e23,e20),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_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,e13) = e10
| op1(e12,e12) = e10
| op1(e11,e11) = e10 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_304,plain,
( op1(e13,e13) = e12
| op1(e11,e11) = e12
| op1(e10,e10) = e12 ),
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_320,plain,
( op2(e23,e23) = e20
| op2(e22,e22) = e20
| op2(e21,e21) = e20 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_336,plain,
( op2(e23,e23) = e22
| op2(e21,e21) = e22
| op2(e20,e20) = e22 ),
inference(clausify,[status(thm)],[ax11]) ).
cnf(c_352,plain,
op1(op1(e12,e12),e12) = e10,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_353,plain,
op1(op1(e12,e12),op1(e12,e12)) = e11,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_354,plain,
op1(e12,e12) = e13,
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_355,plain,
op2(op2(e22,e22),e22) = e20,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_356,plain,
op2(op2(e22,e22),op2(e22,e22)) = e21,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_357,plain,
op2(e22,e22) = e23,
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_359,plain,
h1(e10) = op2(op2(e20,e20),e20),
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_360,plain,
op2(op2(e20,e20),e20) = h1(e10),
inference(copy,[status(thm)],[c_359]) ).
cnf(c_363,plain,
h1(e13) = op2(e20,e20),
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_364,plain,
op2(e20,e20) = h1(e13),
inference(copy,[status(thm)],[c_363]) ).
cnf(c_365,plain,
h2(e12) = e21,
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_366,plain,
h2(e10) = op2(op2(e21,e21),e21),
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_367,plain,
op2(op2(e21,e21),e21) = h2(e10),
inference(copy,[status(thm)],[c_366]) ).
cnf(c_368,plain,
h2(e11) = op2(op2(e21,e21),op2(e21,e21)),
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_369,plain,
op2(op2(e21,e21),op2(e21,e21)) = h2(e11),
inference(copy,[status(thm)],[c_368]) ).
cnf(c_370,plain,
h2(e13) = op2(e21,e21),
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_371,plain,
op2(e21,e21) = h2(e13),
inference(copy,[status(thm)],[c_370]) ).
cnf(c_373,plain,
h3(e10) = op2(op2(e22,e22),e22),
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_1871,plain,
h3(e10) = op2(e23,e22),
inference(paramod,[status(thm)],[c_357,c_373]) ).
cnf(c_374,plain,
op2(e23,e22) = h3(e10),
inference(copy,[status(thm)],[c_1871]) ).
cnf(c_375,plain,
h3(e11) = op2(op2(e22,e22),op2(e22,e22)),
inference(clausify,[status(thm)],[ax16]) ).
cnf(c_1872,plain,
h3(e11) = op2(e23,op2(e22,e22)),
inference(paramod,[status(thm)],[c_357,c_375]) ).
cnf(c_1873,plain,
h3(e11) = op2(e23,e23),
inference(paramod,[status(thm)],[c_357,c_1872]) ).
cnf(c_376,plain,
op2(e23,e23) = h3(e11),
inference(copy,[status(thm)],[c_1873]) ).
cnf(c_380,plain,
h4(e10) = op2(op2(e23,e23),e23),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_1874,plain,
h4(e10) = op2(h3(e11),e23),
inference(paramod,[status(thm)],[c_376,c_380]) ).
cnf(c_381,plain,
op2(h3(e11),e23) = h4(e10),
inference(copy,[status(thm)],[c_1874]) ).
cnf(c_1026,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e12) != e21
| h2(e13) != 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)) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1875,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e12) != e21
| h2(e13) != 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),e21)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_365,c_1026]) ).
cnf(c_1876,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e12) != e21
| h2(e13) != 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),e21)
| 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),e21)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_365,c_1875]) ).
cnf(c_1877,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e12) != e21
| h2(e13) != 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(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| 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),e21)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_365,c_1876]) ).
cnf(c_1878,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e12) != e21
| h2(e13) != 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(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| 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),e21)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_365,c_1877]) ).
cnf(c_1879,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e12) != e21
| h2(e13) != 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(e13) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| 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),e21)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_354,c_1878]) ).
cnf(c_1880,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e12) != e21
| h2(e13) != 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(e13) != op2(e21,h2(e12))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| 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),e21)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_365,c_1879]) ).
cnf(c_1881,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e12) != e21
| h2(e13) != 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(e13) != op2(e21,e21)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| 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),e21)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_365,c_1880]) ).
cnf(c_1882,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e12) != e21
| h2(e13) != 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(e13) != h2(e13)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| 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),e21)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_371,c_1881]) ).
cnf(c_1883,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e12) != e21
| h2(e13) != 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(e21,h2(e13))
| h2(e13) != h2(e13)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| 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),e21)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_365,c_1882]) ).
cnf(c_1884,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e12) != e21
| h2(e13) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(e13) != h2(e13)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| 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),e21)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_365,c_1883]) ).
cnf(c_1885,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| e21 != e21
| h2(e13) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(e13) != h2(e13)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| 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),e21)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(paramod,[status(thm)],[c_365,c_1884]) ).
cnf(c_1886,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| e21 != e21
| h2(e13) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(e13) != h2(e13)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| 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),e21)
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1885]) ).
cnf(c_1887,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| e21 != e21
| h2(e13) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(e13) != h2(e13)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| 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),e21)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1886]) ).
cnf(c_1888,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| e21 != e21
| h2(e13) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(e13) != h2(e13)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1887]) ).
cnf(c_1889,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| e21 != e21
| h2(e13) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(e13) != h2(e13)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1888]) ).
cnf(c_1890,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| e21 != e21
| h2(e13) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(e13) != h2(e13)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1889]) ).
cnf(c_1891,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| e21 != e21
| h2(e13) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(e13) != h2(e13)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1890]) ).
cnf(c_1892,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| e21 != e21
| h2(e13) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(e13) != h2(e13)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1891]) ).
cnf(c_1893,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| e21 != e21
| h2(e13) != e20
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(e13) != h2(e13)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1892]) ).
cnf(c_1894,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| e21 != e21
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(e13) != h2(e13)
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1893]) ).
cnf(c_1895,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| e21 != e21
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1894]) ).
cnf(c_1027,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),h2(e11)) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1895]) ).
cnf(c_1896,plain,
op1(e13,op1(e12,e12)) = e11,
inference(paramod,[status(thm)],[c_354,c_353]) ).
cnf(c_1689,plain,
op1(e13,e13) = e11,
inference(paramod,[status(thm)],[c_354,c_1896]) ).
cnf(c_1690,plain,
op1(e13,e12) = e10,
inference(paramod,[status(thm)],[c_354,c_352]) ).
cnf(c_1897,plain,
( op1(e13,e13) = e10
| e13 = e10
| op1(e11,e11) = e10 ),
inference(paramod,[status(thm)],[c_354,c_288]) ).
cnf(c_1898,plain,
( e11 = e10
| e13 = e10
| op1(e11,e11) = e10 ),
inference(paramod,[status(thm)],[c_1689,c_1897]) ).
cnf(c_1899,plain,
( e11 = e10
| op1(e11,e11) = e10 ),
inference(resolve,[status(thm)],[c_246,c_1898]) ).
cnf(c_1697,plain,
op1(e11,e11) = e10,
inference(resolve,[status(thm)],[c_243,c_1899]) ).
cnf(c_1698,plain,
op1(e12,e13) != e13,
inference(paramod,[status(thm)],[c_354,c_170]) ).
cnf(c_1702,plain,
op1(e10,e12) != e13,
inference(paramod,[status(thm)],[c_354,c_133]) ).
cnf(c_1900,plain,
( op1(e13,e12) = e12
| e13 = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_354,c_56]) ).
cnf(c_1901,plain,
( e10 = e12
| e13 = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(paramod,[status(thm)],[c_1690,c_1900]) ).
cnf(c_1902,plain,
( e10 = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(resolve,[status(thm)],[c_250,c_1901]) ).
cnf(c_1703,plain,
( op1(e11,e12) = e12
| op1(e10,e12) = e12 ),
inference(resolve,[status(thm)],[c_245,c_1902]) ).
cnf(c_1903,plain,
( op1(e12,e13) = e12
| e13 = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 ),
inference(paramod,[status(thm)],[c_354,c_55]) ).
cnf(c_1704,plain,
( op1(e12,e13) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 ),
inference(resolve,[status(thm)],[c_250,c_1903]) ).
cnf(c_1904,plain,
( op1(e12,e13) = e11
| e13 = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 ),
inference(paramod,[status(thm)],[c_354,c_53]) ).
cnf(c_1706,plain,
( op1(e12,e13) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 ),
inference(resolve,[status(thm)],[c_249,c_1904]) ).
cnf(c_1905,plain,
op2(e23,op2(e22,e22)) = e21,
inference(paramod,[status(thm)],[c_357,c_356]) ).
cnf(c_1906,plain,
op2(e23,e23) = e21,
inference(paramod,[status(thm)],[c_357,c_1905]) ).
cnf(c_1708,plain,
h3(e11) = e21,
inference(paramod,[status(thm)],[c_376,c_1906]) ).
cnf(c_1907,plain,
op2(e23,e22) = e20,
inference(paramod,[status(thm)],[c_357,c_355]) ).
cnf(c_1709,plain,
h3(e10) = e20,
inference(paramod,[status(thm)],[c_374,c_1907]) ).
cnf(c_1908,plain,
( op2(e23,e23) = e20
| op2(e22,e22) = e20
| h2(e13) = e20 ),
inference(paramod,[status(thm)],[c_371,c_320]) ).
cnf(c_1909,plain,
( op2(e23,e23) = e20
| e23 = e20
| h2(e13) = e20 ),
inference(paramod,[status(thm)],[c_357,c_1908]) ).
cnf(c_1910,plain,
( h3(e11) = e20
| e23 = e20
| h2(e13) = e20 ),
inference(paramod,[status(thm)],[c_376,c_1909]) ).
cnf(c_1911,plain,
( e21 = e20
| e23 = e20
| h2(e13) = e20 ),
inference(paramod,[status(thm)],[c_1708,c_1910]) ).
cnf(c_1912,plain,
( e21 = e20
| h2(e13) = e20 ),
inference(resolve,[status(thm)],[c_254,c_1911]) ).
cnf(c_1716,plain,
h2(e13) = e20,
inference(resolve,[status(thm)],[c_251,c_1912]) ).
cnf(c_1717,plain,
op2(e22,e23) != e23,
inference(paramod,[status(thm)],[c_357,c_234]) ).
cnf(c_1721,plain,
op2(e20,e22) != e23,
inference(paramod,[status(thm)],[c_357,c_197]) ).
cnf(c_1913,plain,
( op2(e23,e22) = e22
| e23 = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_357,c_104]) ).
cnf(c_1914,plain,
( h3(e10) = e22
| e23 = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_374,c_1913]) ).
cnf(c_1915,plain,
( e20 = e22
| e23 = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(paramod,[status(thm)],[c_1709,c_1914]) ).
cnf(c_1916,plain,
( e20 = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(resolve,[status(thm)],[c_258,c_1915]) ).
cnf(c_1722,plain,
( op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(resolve,[status(thm)],[c_253,c_1916]) ).
cnf(c_1917,plain,
( op2(e22,e23) = e22
| e23 = e22
| op2(e22,e21) = e22
| op2(e22,e20) = e22 ),
inference(paramod,[status(thm)],[c_357,c_103]) ).
cnf(c_1723,plain,
( op2(e22,e23) = e22
| op2(e22,e21) = e22
| op2(e22,e20) = e22 ),
inference(resolve,[status(thm)],[c_258,c_1917]) ).
cnf(c_1728,plain,
op2(h1(e13),e20) = h1(e10),
inference(paramod,[status(thm)],[c_364,c_360]) ).
cnf(c_1918,plain,
( op2(e23,e23) = e22
| op2(e21,e21) = e22
| h1(e13) = e22 ),
inference(paramod,[status(thm)],[c_364,c_336]) ).
cnf(c_1919,plain,
( op2(e23,e23) = e22
| h2(e13) = e22
| h1(e13) = e22 ),
inference(paramod,[status(thm)],[c_371,c_1918]) ).
cnf(c_1920,plain,
( op2(e23,e23) = e22
| e20 = e22
| h1(e13) = e22 ),
inference(paramod,[status(thm)],[c_1716,c_1919]) ).
cnf(c_1921,plain,
( h3(e11) = e22
| e20 = e22
| h1(e13) = e22 ),
inference(paramod,[status(thm)],[c_376,c_1920]) ).
cnf(c_1922,plain,
( e21 = e22
| e20 = e22
| h1(e13) = e22 ),
inference(paramod,[status(thm)],[c_1708,c_1921]) ).
cnf(c_1923,plain,
( e21 = e22
| h1(e13) = e22 ),
inference(resolve,[status(thm)],[c_253,c_1922]) ).
cnf(c_1729,plain,
h1(e13) = e22,
inference(resolve,[status(thm)],[c_256,c_1923]) ).
cnf(c_1924,plain,
h1(e13) != op2(e20,e22),
inference(paramod,[status(thm)],[c_364,c_213]) ).
cnf(c_1925,plain,
e22 != op2(e20,e22),
inference(paramod,[status(thm)],[c_1729,c_1924]) ).
cnf(c_1731,plain,
op2(e20,e22) != e22,
inference(copy,[status(thm)],[c_1925]) ).
cnf(c_1926,plain,
op2(e23,e20) != h1(e13),
inference(paramod,[status(thm)],[c_364,c_182]) ).
cnf(c_1733,plain,
op2(e23,e20) != e22,
inference(paramod,[status(thm)],[c_1729,c_1926]) ).
cnf(c_1927,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| h1(e13) = e23 ),
inference(paramod,[status(thm)],[c_364,c_89]) ).
cnf(c_1928,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| e22 = e23 ),
inference(paramod,[status(thm)],[c_1729,c_1927]) ).
cnf(c_1929,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| e23 = e22 ),
inference(copy,[status(thm)],[c_1928]) ).
cnf(c_1930,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_258,c_1929]) ).
cnf(c_1737,plain,
( op2(e20,e23) = e23
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_1721,c_1930]) ).
cnf(c_1931,plain,
( op2(e23,e20) = e21
| op2(e22,e20) = e21
| op2(e21,e20) = e21
| h1(e13) = e21 ),
inference(paramod,[status(thm)],[c_364,c_86]) ).
cnf(c_1932,plain,
( op2(e23,e20) = e21
| op2(e22,e20) = e21
| op2(e21,e20) = e21
| e22 = e21 ),
inference(paramod,[status(thm)],[c_1729,c_1931]) ).
cnf(c_1933,plain,
( op2(e23,e20) = e21
| op2(e22,e20) = e21
| op2(e21,e20) = e21
| e21 = e22 ),
inference(copy,[status(thm)],[c_1932]) ).
cnf(c_1738,plain,
( op2(e23,e20) = e21
| op2(e22,e20) = e21
| op2(e21,e20) = e21 ),
inference(resolve,[status(thm)],[c_256,c_1933]) ).
cnf(c_1934,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| h1(e13) = e20 ),
inference(paramod,[status(thm)],[c_364,c_84]) ).
cnf(c_1935,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| e22 = e20 ),
inference(paramod,[status(thm)],[c_1729,c_1934]) ).
cnf(c_1936,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| e20 = e22 ),
inference(copy,[status(thm)],[c_1935]) ).
cnf(c_1740,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20 ),
inference(resolve,[status(thm)],[c_253,c_1936]) ).
cnf(c_1937,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| h1(e13) = e20 ),
inference(paramod,[status(thm)],[c_364,c_83]) ).
cnf(c_1938,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| e22 = e20 ),
inference(paramod,[status(thm)],[c_1729,c_1937]) ).
cnf(c_1939,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| e20 = e22 ),
inference(copy,[status(thm)],[c_1938]) ).
cnf(c_1741,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20 ),
inference(resolve,[status(thm)],[c_253,c_1939]) ).
cnf(c_1940,plain,
op2(h2(e13),op2(e21,e21)) = h2(e11),
inference(paramod,[status(thm)],[c_371,c_369]) ).
cnf(c_1941,plain,
op2(e20,op2(e21,e21)) = h2(e11),
inference(paramod,[status(thm)],[c_1716,c_1940]) ).
cnf(c_1942,plain,
op2(e20,h2(e13)) = h2(e11),
inference(paramod,[status(thm)],[c_371,c_1941]) ).
cnf(c_1943,plain,
op2(e20,e20) = h2(e11),
inference(paramod,[status(thm)],[c_1716,c_1942]) ).
cnf(c_1944,plain,
h1(e13) = h2(e11),
inference(paramod,[status(thm)],[c_364,c_1943]) ).
cnf(c_1945,plain,
e22 = h2(e11),
inference(paramod,[status(thm)],[c_1729,c_1944]) ).
cnf(c_1742,plain,
h2(e11) = e22,
inference(copy,[status(thm)],[c_1945]) ).
cnf(c_1946,plain,
op2(h2(e13),e21) = h2(e10),
inference(paramod,[status(thm)],[c_371,c_367]) ).
cnf(c_1743,plain,
op2(e20,e21) = h2(e10),
inference(paramod,[status(thm)],[c_1716,c_1946]) ).
cnf(c_1947,plain,
h2(e13) != op2(e21,e20),
inference(paramod,[status(thm)],[c_371,c_219]) ).
cnf(c_1948,plain,
e20 != op2(e21,e20),
inference(paramod,[status(thm)],[c_1716,c_1947]) ).
cnf(c_1746,plain,
op2(e21,e20) != e20,
inference(copy,[status(thm)],[c_1948]) ).
cnf(c_1949,plain,
h2(e13) != op2(e20,e21),
inference(paramod,[status(thm)],[c_371,c_187]) ).
cnf(c_1950,plain,
e20 != op2(e20,e21),
inference(paramod,[status(thm)],[c_1716,c_1949]) ).
cnf(c_1951,plain,
e20 != h2(e10),
inference(paramod,[status(thm)],[c_1743,c_1950]) ).
cnf(c_1749,plain,
h2(e10) != e20,
inference(copy,[status(thm)],[c_1951]) ).
cnf(c_1952,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| op2(e21,e21) = e21
| h2(e10) = e21 ),
inference(paramod,[status(thm)],[c_1743,c_94]) ).
cnf(c_1953,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| h2(e13) = e21
| h2(e10) = e21 ),
inference(paramod,[status(thm)],[c_371,c_1952]) ).
cnf(c_1954,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| e20 = e21
| h2(e10) = e21 ),
inference(paramod,[status(thm)],[c_1716,c_1953]) ).
cnf(c_1955,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| e21 = e20
| h2(e10) = e21 ),
inference(copy,[status(thm)],[c_1954]) ).
cnf(c_1754,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| h2(e10) = e21 ),
inference(resolve,[status(thm)],[c_251,c_1955]) ).
cnf(c_1956,plain,
op2(e23,e20) != h3(e10),
inference(paramod,[status(thm)],[c_374,c_237]) ).
cnf(c_1756,plain,
op2(e23,e20) != e20,
inference(paramod,[status(thm)],[c_1709,c_1956]) ).
cnf(c_1957,plain,
h3(e10) != op2(e20,e22),
inference(paramod,[status(thm)],[c_374,c_198]) ).
cnf(c_1958,plain,
e20 != op2(e20,e22),
inference(paramod,[status(thm)],[c_1709,c_1957]) ).
cnf(c_1757,plain,
op2(e20,e22) != e20,
inference(copy,[status(thm)],[c_1958]) ).
cnf(c_1959,plain,
( op2(e23,e23) = e22
| h3(e10) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(paramod,[status(thm)],[c_374,c_111]) ).
cnf(c_1960,plain,
( op2(e23,e23) = e22
| e20 = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(paramod,[status(thm)],[c_1709,c_1959]) ).
cnf(c_1961,plain,
( h3(e11) = e22
| e20 = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(paramod,[status(thm)],[c_376,c_1960]) ).
cnf(c_1962,plain,
( e21 = e22
| e20 = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 ),
inference(paramod,[status(thm)],[c_1708,c_1961]) ).
cnf(c_1963,plain,
( e21 = e22
| e20 = e22
| op2(e23,e21) = e22 ),
inference(resolve,[status(thm)],[c_1733,c_1962]) ).
cnf(c_1964,plain,
( e21 = e22
| op2(e23,e21) = e22 ),
inference(resolve,[status(thm)],[c_253,c_1963]) ).
cnf(c_1759,plain,
op2(e23,e21) = e22,
inference(resolve,[status(thm)],[c_256,c_1964]) ).
cnf(c_1965,plain,
h3(e11) != op2(e23,e20),
inference(paramod,[status(thm)],[c_376,c_238]) ).
cnf(c_1966,plain,
e21 != op2(e23,e20),
inference(paramod,[status(thm)],[c_1708,c_1965]) ).
cnf(c_1760,plain,
op2(e23,e20) != e21,
inference(copy,[status(thm)],[c_1966]) ).
cnf(c_1967,plain,
( h3(e11) = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| op2(e20,e23) = e23 ),
inference(paramod,[status(thm)],[c_376,c_114]) ).
cnf(c_1968,plain,
( e21 = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| op2(e20,e23) = e23 ),
inference(paramod,[status(thm)],[c_1708,c_1967]) ).
cnf(c_1969,plain,
( e23 = e21
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| op2(e20,e23) = e23 ),
inference(copy,[status(thm)],[c_1968]) ).
cnf(c_1970,plain,
( e23 = e21
| op2(e21,e23) = e23
| op2(e20,e23) = e23 ),
inference(resolve,[status(thm)],[c_1717,c_1969]) ).
cnf(c_1764,plain,
( op2(e21,e23) = e23
| op2(e20,e23) = e23 ),
inference(resolve,[status(thm)],[c_257,c_1970]) ).
cnf(c_1971,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),h2(e13)) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1742,c_1027]) ).
cnf(c_1972,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(h2(e11),h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1716,c_1971]) ).
cnf(c_1973,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| op2(h2(e11),h2(e11)) != h2(op1(e11,e11))
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1742,c_1972]) ).
cnf(c_1974,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| op2(e22,h2(e11)) != h2(op1(e11,e11))
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1742,c_1973]) ).
cnf(c_1975,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| op2(e22,e22) != h2(op1(e11,e11))
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1742,c_1974]) ).
cnf(c_1976,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| e23 != h2(op1(e11,e11))
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_357,c_1975]) ).
cnf(c_1977,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(h2(e11),e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1697,c_1976]) ).
cnf(c_1978,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(h2(e11),h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1742,c_1977]) ).
cnf(c_1979,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,h2(e13)) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1742,c_1978]) ).
cnf(c_1980,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(op1(e12,e11)) != op2(e21,h2(e11))
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1716,c_1979]) ).
cnf(c_1981,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,h2(e13))
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1742,c_1980]) ).
cnf(c_1982,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(h2(e13),h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1716,c_1981]) ).
cnf(c_1983,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(h2(e13),h2(e11)) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1716,c_1982]) ).
cnf(c_1984,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(e20,h2(e11)) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1716,c_1983]) ).
cnf(c_1985,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(op1(e13,e12)) != op2(h2(e13),e21)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1742,c_1984]) ).
cnf(c_1986,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(e10) != op2(h2(e13),e21)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1690,c_1985]) ).
cnf(c_1987,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(e10) != op2(e20,e21)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1716,c_1986]) ).
cnf(c_1988,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(h2(e13),h2(e13)) != h2(op1(e13,e13))
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1743,c_1987]) ).
cnf(c_1989,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(e20,h2(e13)) != h2(op1(e13,e13))
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1716,c_1988]) ).
cnf(c_1990,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| op2(e20,e20) != h2(op1(e13,e13))
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1716,c_1989]) ).
cnf(c_1991,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| h1(e13) != h2(op1(e13,e13))
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_364,c_1990]) ).
cnf(c_1992,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| e22 != h2(op1(e13,e13))
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1729,c_1991]) ).
cnf(c_1993,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| e22 != h2(e11)
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1689,c_1992]) ).
cnf(c_1994,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| h2(e13) != e20
| e22 != e22
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1742,c_1993]) ).
cnf(c_1995,negated_conjecture,
( h2(e10) != e23
| h2(e11) != e22
| e20 != e20
| e22 != e22
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1716,c_1994]) ).
cnf(c_1996,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| op2(h2(e10),e22) != h2(op1(e10,e11))
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1742,c_1995]) ).
cnf(c_1997,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| op2(h2(e10),e20) != h2(op1(e10,e13))
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1996]) ).
cnf(c_1998,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| op2(e22,h2(e10)) != h2(op1(e11,e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1997]) ).
cnf(c_1999,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != h2(e10)
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1998]) ).
cnf(c_2000,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| op2(e22,e20) != h2(op1(e11,e13))
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_1999]) ).
cnf(c_2001,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| op2(e20,h2(e10)) != h2(op1(e13,e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2000]) ).
cnf(c_2002,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(e10) != h2(e10)
| op2(e20,e22) != h2(op1(e13,e11))
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2001]) ).
cnf(c_2003,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(e10) != h2(e10)
| h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2002]) ).
cnf(c_2004,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| e20 != e20
| e22 != e22
| h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2003]) ).
cnf(c_2005,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| e20 != e20
| h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2004]) ).
cnf(c_2006,negated_conjecture,
( h2(e10) != e23
| e22 != e22
| h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2005]) ).
cnf(c_2007,negated_conjecture,
( h2(e10) != e23
| h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2006]) ).
cnf(c_1772,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2007]) ).
cnf(c_2008,plain,
( op1(e13,e13) = e12
| e10 = e12
| op1(e10,e10) = e12 ),
inference(paramod,[status(thm)],[c_1697,c_304]) ).
cnf(c_2009,plain,
( e11 = e12
| e10 = e12
| op1(e10,e10) = e12 ),
inference(paramod,[status(thm)],[c_1689,c_2008]) ).
cnf(c_2010,plain,
( e11 = e12
| op1(e10,e10) = e12 ),
inference(resolve,[status(thm)],[c_245,c_2009]) ).
cnf(c_1775,plain,
op1(e10,e10) = e12,
inference(resolve,[status(thm)],[c_248,c_2010]) ).
cnf(c_2011,plain,
e11 != op1(e13,e10),
inference(paramod,[status(thm)],[c_1689,c_174]) ).
cnf(c_1777,plain,
op1(e13,e10) != e11,
inference(copy,[status(thm)],[c_2011]) ).
cnf(c_2012,plain,
e11 != op1(e12,e13),
inference(paramod,[status(thm)],[c_1689,c_146]) ).
cnf(c_1778,plain,
op1(e12,e13) != e11,
inference(copy,[status(thm)],[c_2012]) ).
cnf(c_2013,plain,
( e11 = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| op1(e10,e13) = e13 ),
inference(paramod,[status(thm)],[c_1689,c_66]) ).
cnf(c_2014,plain,
( e13 = e11
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| op1(e10,e13) = e13 ),
inference(copy,[status(thm)],[c_2013]) ).
cnf(c_2015,plain,
( e13 = e11
| op1(e11,e13) = e13
| op1(e10,e13) = e13 ),
inference(resolve,[status(thm)],[c_1698,c_2014]) ).
cnf(c_1781,plain,
( op1(e11,e13) = e13
| op1(e10,e13) = e13 ),
inference(resolve,[status(thm)],[c_249,c_2015]) ).
cnf(c_1787,plain,
op1(e13,e10) != e10,
inference(paramod,[status(thm)],[c_1690,c_173]) ).
cnf(c_2016,plain,
e10 != op1(e10,e12),
inference(paramod,[status(thm)],[c_1690,c_134]) ).
cnf(c_1789,plain,
op1(e10,e12) != e10,
inference(copy,[status(thm)],[c_2016]) ).
cnf(c_2017,plain,
( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11
| e12 = e11 ),
inference(paramod,[status(thm)],[c_1775,c_38]) ).
cnf(c_2018,plain,
( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11
| e11 = e12 ),
inference(copy,[status(thm)],[c_2017]) ).
cnf(c_2019,plain,
( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11 ),
inference(resolve,[status(thm)],[c_248,c_2018]) ).
cnf(c_1790,plain,
( op1(e12,e10) = e11
| op1(e11,e10) = e11 ),
inference(resolve,[status(thm)],[c_1777,c_2019]) ).
cnf(c_2020,plain,
e10 != op1(e11,e10),
inference(paramod,[status(thm)],[c_1697,c_155]) ).
cnf(c_1793,plain,
op1(e11,e10) != e10,
inference(copy,[status(thm)],[c_2020]) ).
cnf(c_2021,plain,
e10 != op1(e10,e11),
inference(paramod,[status(thm)],[c_1697,c_123]) ).
cnf(c_1795,plain,
op1(e10,e11) != e10,
inference(copy,[status(thm)],[c_2021]) ).
cnf(c_2022,plain,
( op1(e13,e11) = e12
| op1(e12,e11) = e12
| e10 = e12
| op1(e10,e11) = e12 ),
inference(paramod,[status(thm)],[c_1697,c_48]) ).
cnf(c_1798,plain,
( op1(e13,e11) = e12
| op1(e12,e11) = e12
| op1(e10,e11) = e12 ),
inference(resolve,[status(thm)],[c_245,c_2022]) ).
cnf(c_2023,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| e12 = e13 ),
inference(paramod,[status(thm)],[c_1775,c_41]) ).
cnf(c_2024,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| e13 = e12 ),
inference(copy,[status(thm)],[c_2023]) ).
cnf(c_2025,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13 ),
inference(resolve,[status(thm)],[c_250,c_2024]) ).
cnf(c_1807,plain,
( op1(e10,e13) = e13
| op1(e10,e11) = e13 ),
inference(resolve,[status(thm)],[c_1702,c_2025]) ).
cnf(c_2026,plain,
( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11 ),
inference(resolve,[status(thm)],[c_1789,c_21]) ).
cnf(c_1808,plain,
( op1(e10,e12) = e12
| op1(e10,e12) = e11 ),
inference(resolve,[status(thm)],[c_1702,c_2026]) ).
cnf(c_1811,plain,
op2(e21,e23) = h4(e10),
inference(paramod,[status(thm)],[c_1708,c_381]) ).
cnf(c_1812,plain,
op2(e23,e23) = e21,
inference(paramod,[status(thm)],[c_1708,c_376]) ).
cnf(c_1813,plain,
op2(e23,e22) = e20,
inference(paramod,[status(thm)],[c_1709,c_374]) ).
cnf(c_2027,plain,
( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21 ),
inference(resolve,[status(thm)],[c_1757,c_69]) ).
cnf(c_2028,plain,
( op2(e20,e22) = e23
| op2(e20,e22) = e21 ),
inference(resolve,[status(thm)],[c_1731,c_2027]) ).
cnf(c_1819,plain,
op2(e20,e22) = e21,
inference(resolve,[status(thm)],[c_1721,c_2028]) ).
cnf(c_1820,plain,
op2(e22,e20) = h1(e10),
inference(paramod,[status(thm)],[c_1729,c_1728]) ).
cnf(c_2029,plain,
( op2(e21,e22) = e22
| e21 = e22 ),
inference(paramod,[status(thm)],[c_1819,c_1722]) ).
cnf(c_1824,plain,
op2(e21,e22) = e22,
inference(resolve,[status(thm)],[c_256,c_2029]) ).
cnf(c_2030,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21 ),
inference(resolve,[status(thm)],[c_1756,c_79]) ).
cnf(c_2031,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22 ),
inference(resolve,[status(thm)],[c_1760,c_2030]) ).
cnf(c_1826,plain,
op2(e23,e20) = e23,
inference(resolve,[status(thm)],[c_1733,c_2031]) ).
cnf(c_1827,plain,
( op2(e22,e23) = e22
| op2(e22,e21) = e22
| h1(e10) = e22 ),
inference(paramod,[status(thm)],[c_1820,c_1723]) ).
cnf(c_2032,plain,
( op2(e20,e23) = e20
| op2(e20,e22) = e20
| h2(e10) = e20 ),
inference(paramod,[status(thm)],[c_1743,c_1741]) ).
cnf(c_2033,plain,
( op2(e20,e23) = e20
| e21 = e20
| h2(e10) = e20 ),
inference(paramod,[status(thm)],[c_1819,c_2032]) ).
cnf(c_2034,plain,
( op2(e20,e23) = e20
| e21 = e20 ),
inference(resolve,[status(thm)],[c_1749,c_2033]) ).
cnf(c_1829,plain,
op2(e20,e23) = e20,
inference(resolve,[status(thm)],[c_251,c_2034]) ).
cnf(c_2035,plain,
( op2(e20,e23) = e23
| h2(e10) = e23 ),
inference(paramod,[status(thm)],[c_1743,c_1737]) ).
cnf(c_2036,plain,
( e20 = e23
| h2(e10) = e23 ),
inference(paramod,[status(thm)],[c_1829,c_2035]) ).
cnf(c_2037,plain,
( e23 = e20
| h2(e10) = e23 ),
inference(copy,[status(thm)],[c_2036]) ).
cnf(c_1830,plain,
h2(e10) = e23,
inference(resolve,[status(thm)],[c_254,c_2037]) ).
cnf(c_2038,plain,
( op2(e23,e20) = e20
| h1(e10) = e20
| op2(e21,e20) = e20 ),
inference(paramod,[status(thm)],[c_1820,c_1740]) ).
cnf(c_2039,plain,
( e23 = e20
| h1(e10) = e20
| op2(e21,e20) = e20 ),
inference(paramod,[status(thm)],[c_1826,c_2038]) ).
cnf(c_2040,plain,
( e23 = e20
| h1(e10) = e20 ),
inference(resolve,[status(thm)],[c_1746,c_2039]) ).
cnf(c_1832,plain,
h1(e10) = e20,
inference(resolve,[status(thm)],[c_254,c_2040]) ).
cnf(c_2041,plain,
( op2(e23,e21) = e21
| op2(e22,e21) = e21
| e23 = e21 ),
inference(paramod,[status(thm)],[c_1830,c_1754]) ).
cnf(c_2042,plain,
( e22 = e21
| op2(e22,e21) = e21
| e23 = e21 ),
inference(paramod,[status(thm)],[c_1759,c_2041]) ).
cnf(c_2043,plain,
( e21 = e22
| op2(e22,e21) = e21
| e23 = e21 ),
inference(copy,[status(thm)],[c_2042]) ).
cnf(c_2044,plain,
( e21 = e22
| op2(e22,e21) = e21 ),
inference(resolve,[status(thm)],[c_257,c_2043]) ).
cnf(c_1833,plain,
op2(e22,e21) = e21,
inference(resolve,[status(thm)],[c_256,c_2044]) ).
cnf(c_2045,plain,
( op2(e23,e20) = e21
| h1(e10) = e21
| op2(e21,e20) = e21 ),
inference(paramod,[status(thm)],[c_1820,c_1738]) ).
cnf(c_2046,plain,
( op2(e23,e20) = e21
| e20 = e21
| op2(e21,e20) = e21 ),
inference(paramod,[status(thm)],[c_1832,c_2045]) ).
cnf(c_2047,plain,
( e23 = e21
| e20 = e21
| op2(e21,e20) = e21 ),
inference(paramod,[status(thm)],[c_1826,c_2046]) ).
cnf(c_2048,plain,
( e23 = e21
| e21 = e20
| op2(e21,e20) = e21 ),
inference(copy,[status(thm)],[c_2047]) ).
cnf(c_2049,plain,
( e23 = e21
| op2(e21,e20) = e21 ),
inference(resolve,[status(thm)],[c_251,c_2048]) ).
cnf(c_1834,plain,
op2(e21,e20) = e21,
inference(resolve,[status(thm)],[c_257,c_2049]) ).
cnf(c_2050,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(e23,h2(e10)) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1830,c_1772]) ).
cnf(c_2051,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| op2(e23,e23) != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1830,c_2050]) ).
cnf(c_2052,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| e21 != h2(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1812,c_2051]) ).
cnf(c_2053,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| e21 != h2(e12) ),
inference(paramod,[status(thm)],[c_1775,c_2052]) ).
cnf(c_2054,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(h2(e10),e22)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_365,c_2053]) ).
cnf(c_2055,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != op2(e23,e22)
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1830,c_2054]) ).
cnf(c_2056,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(h2(e10),e21)
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1813,c_2055]) ).
cnf(c_2057,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != op2(e23,e21)
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1830,c_2056]) ).
cnf(c_2058,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),e20)
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1759,c_2057]) ).
cnf(c_2059,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != op2(e23,e20)
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1830,c_2058]) ).
cnf(c_2060,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,h2(e10))
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1826,c_2059]) ).
cnf(c_2061,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| h2(e10) != e23
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1830,c_2060]) ).
cnf(c_2062,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != op2(e22,e21)
| e23 != e23
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1830,c_2061]) ).
cnf(c_2063,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != op2(e22,e20)
| h2(op1(e11,e12)) != e21
| e23 != e23
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1833,c_2062]) ).
cnf(c_2064,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != h1(e10)
| h2(op1(e11,e12)) != e21
| e23 != e23
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1820,c_2063]) ).
cnf(c_2065,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,h2(e10))
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| e23 != e23
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1832,c_2064]) ).
cnf(c_2066,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != op2(e21,e23)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| e23 != e23
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1830,c_2065]) ).
cnf(c_2067,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != op2(e21,e22)
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| e23 != e23
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1811,c_2066]) ).
cnf(c_2068,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != op2(e21,e20)
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| e23 != e23
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1824,c_2067]) ).
cnf(c_2069,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,h2(e10))
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| e23 != e23
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1834,c_2068]) ).
cnf(c_2070,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != op2(e20,e23)
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| e23 != e23
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1830,c_2069]) ).
cnf(c_2071,negated_conjecture,
( h2(op1(e13,e11)) != op2(e20,e22)
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| e23 != e23
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1829,c_2070]) ).
cnf(c_2072,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| e23 != e23
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20
| e21 != e21 ),
inference(paramod,[status(thm)],[c_1819,c_2071]) ).
cnf(c_2073,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| e23 != e23
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20 ),
inference(copy,[status(thm)],[c_2072]) ).
cnf(c_1835,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(op1(e10,e12)) != e22
| h2(op1(e10,e11)) != e20 ),
inference(copy,[status(thm)],[c_2073]) ).
cnf(c_2074,plain,
e12 != op1(e10,e12),
inference(paramod,[status(thm)],[c_1775,c_149]) ).
cnf(c_1840,plain,
op1(e10,e12) != e12,
inference(copy,[status(thm)],[c_2074]) ).
cnf(c_1841,plain,
op1(e10,e11) != e12,
inference(paramod,[status(thm)],[c_1775,c_147]) ).
cnf(c_1842,plain,
op1(e13,e10) != e12,
inference(paramod,[status(thm)],[c_1775,c_118]) ).
cnf(c_2075,plain,
( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| e12 = e10 ),
inference(paramod,[status(thm)],[c_1775,c_36]) ).
cnf(c_2076,plain,
( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| e10 = e12 ),
inference(copy,[status(thm)],[c_2075]) ).
cnf(c_2077,plain,
( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10 ),
inference(resolve,[status(thm)],[c_245,c_2076]) ).
cnf(c_2078,plain,
( op1(e13,e10) = e10
| op1(e12,e10) = e10 ),
inference(resolve,[status(thm)],[c_1793,c_2077]) ).
cnf(c_1845,plain,
op1(e12,e10) = e10,
inference(resolve,[status(thm)],[c_1787,c_2078]) ).
cnf(c_2079,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| e12 = e10 ),
inference(paramod,[status(thm)],[c_1775,c_35]) ).
cnf(c_2080,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| e10 = e12 ),
inference(copy,[status(thm)],[c_2079]) ).
cnf(c_2081,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10 ),
inference(resolve,[status(thm)],[c_245,c_2080]) ).
cnf(c_2082,plain,
( op1(e10,e13) = e10
| op1(e10,e12) = e10 ),
inference(resolve,[status(thm)],[c_1795,c_2081]) ).
cnf(c_1846,plain,
op1(e10,e13) = e10,
inference(resolve,[status(thm)],[c_1789,c_2082]) ).
cnf(c_2083,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11 ),
inference(resolve,[status(thm)],[c_1787,c_31]) ).
cnf(c_2084,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e12 ),
inference(resolve,[status(thm)],[c_1777,c_2083]) ).
cnf(c_1848,plain,
op1(e13,e10) = e13,
inference(resolve,[status(thm)],[c_1842,c_2084]) ).
cnf(c_2085,plain,
( op1(e12,e13) = e11
| op1(e12,e11) = e11
| e10 = e11 ),
inference(paramod,[status(thm)],[c_1845,c_1706]) ).
cnf(c_2086,plain,
( op1(e12,e13) = e11
| op1(e12,e11) = e11
| e11 = e10 ),
inference(copy,[status(thm)],[c_2085]) ).
cnf(c_2087,plain,
( op1(e12,e13) = e11
| op1(e12,e11) = e11 ),
inference(resolve,[status(thm)],[c_243,c_2086]) ).
cnf(c_1849,plain,
op1(e12,e11) = e11,
inference(resolve,[status(thm)],[c_1778,c_2087]) ).
cnf(c_2088,plain,
( op2(e21,e23) = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_1829,c_1764]) ).
cnf(c_2089,plain,
( h4(e10) = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_1811,c_2088]) ).
cnf(c_2090,plain,
( h4(e10) = e23
| e23 = e20 ),
inference(copy,[status(thm)],[c_2089]) ).
cnf(c_1854,plain,
h4(e10) = e23,
inference(resolve,[status(thm)],[c_254,c_2090]) ).
cnf(c_2091,plain,
( op2(e22,e23) = e22
| op2(e22,e21) = e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_1832,c_1827]) ).
cnf(c_2092,plain,
( op2(e22,e23) = e22
| e21 = e22
| e20 = e22 ),
inference(paramod,[status(thm)],[c_1833,c_2091]) ).
cnf(c_2093,plain,
( op2(e22,e23) = e22
| e21 = e22 ),
inference(resolve,[status(thm)],[c_253,c_2092]) ).
cnf(c_1857,plain,
op2(e22,e23) = e22,
inference(resolve,[status(thm)],[c_256,c_2093]) ).
cnf(c_1860,plain,
op1(e10,e12) = e11,
inference(resolve,[status(thm)],[c_1840,c_1808]) ).
cnf(c_2094,plain,
( op1(e11,e12) = e12
| e11 = e12 ),
inference(paramod,[status(thm)],[c_1860,c_1703]) ).
cnf(c_1861,plain,
op1(e11,e12) = e12,
inference(resolve,[status(thm)],[c_248,c_2094]) ).
cnf(c_2095,plain,
( op1(e13,e11) = e12
| e11 = e12
| op1(e10,e11) = e12 ),
inference(paramod,[status(thm)],[c_1849,c_1798]) ).
cnf(c_2096,plain,
( op1(e13,e11) = e12
| e11 = e12 ),
inference(resolve,[status(thm)],[c_1841,c_2095]) ).
cnf(c_1862,plain,
op1(e13,e11) = e12,
inference(resolve,[status(thm)],[c_248,c_2096]) ).
cnf(c_2097,plain,
( op1(e12,e13) = e12
| op1(e12,e11) = e12
| e10 = e12 ),
inference(paramod,[status(thm)],[c_1845,c_1704]) ).
cnf(c_2098,plain,
( op1(e12,e13) = e12
| e11 = e12
| e10 = e12 ),
inference(paramod,[status(thm)],[c_1849,c_2097]) ).
cnf(c_2099,plain,
( op1(e12,e13) = e12
| e11 = e12 ),
inference(resolve,[status(thm)],[c_245,c_2098]) ).
cnf(c_1863,plain,
op1(e12,e13) = e12,
inference(resolve,[status(thm)],[c_248,c_2099]) ).
cnf(c_2100,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| h2(e11) != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1860,c_1835]) ).
cnf(c_2101,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(op1(e10,e13)) != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1742,c_2100]) ).
cnf(c_2102,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| h2(op1(e11,e10)) != op2(e22,e23)
| h2(e10) != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1846,c_2101]) ).
cnf(c_2103,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| h2(op1(e11,e10)) != op2(e22,e23)
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1830,c_2102]) ).
cnf(c_2104,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e12)) != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1857,c_2103]) ).
cnf(c_2105,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| h2(e12) != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1861,c_2104]) ).
cnf(c_2106,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(op1(e12,e10)) != h4(e10)
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_365,c_2105]) ).
cnf(c_2107,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| h2(e10) != h4(e10)
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1845,c_2106]) ).
cnf(c_2108,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| e23 != h4(e10)
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1830,c_2107]) ).
cnf(c_2109,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(op1(e12,e11)) != e22
| e23 != e23
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1854,c_2108]) ).
cnf(c_2110,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| h2(e11) != e22
| e23 != e23
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1849,c_2109]) ).
cnf(c_2111,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(op1(e12,e13)) != e21
| e22 != e22
| e23 != e23
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1742,c_2110]) ).
cnf(c_2112,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| h2(e12) != e21
| e22 != e22
| e23 != e23
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1863,c_2111]) ).
cnf(c_2113,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(op1(e13,e10)) != e20
| e21 != e21
| e22 != e22
| e23 != e23
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_365,c_2112]) ).
cnf(c_2114,negated_conjecture,
( h2(op1(e13,e11)) != e21
| h2(e13) != e20
| e21 != e21
| e22 != e22
| e23 != e23
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1848,c_2113]) ).
cnf(c_2115,negated_conjecture,
( h2(op1(e13,e11)) != e21
| e20 != e20
| e21 != e21
| e22 != e22
| e23 != e23
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1716,c_2114]) ).
cnf(c_2116,negated_conjecture,
( h2(e12) != e21
| e20 != e20
| e21 != e21
| e22 != e22
| e23 != e23
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_1862,c_2115]) ).
cnf(c_2117,negated_conjecture,
( e21 != e21
| e20 != e20
| e21 != e21
| e22 != e22
| e23 != e23
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| e22 != e22
| h2(op1(e10,e11)) != e20 ),
inference(paramod,[status(thm)],[c_365,c_2116]) ).
cnf(c_2118,negated_conjecture,
( e21 != e21
| e20 != e20
| e21 != e21
| e22 != e22
| e23 != e23
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| e23 != e23
| h2(op1(e10,e11)) != e20 ),
inference(copy,[status(thm)],[c_2117]) ).
cnf(c_2119,negated_conjecture,
( e21 != e21
| e20 != e20
| e21 != e21
| e22 != e22
| e23 != e23
| h2(op1(e11,e13)) != e20
| e21 != e21
| h2(op1(e11,e10)) != e22
| h2(op1(e10,e11)) != e20 ),
inference(copy,[status(thm)],[c_2118]) ).
cnf(c_2120,negated_conjecture,
( e21 != e21
| e20 != e20
| e21 != e21
| e22 != e22
| e23 != e23
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e10)) != e22
| h2(op1(e10,e11)) != e20 ),
inference(copy,[status(thm)],[c_2119]) ).
cnf(c_2121,negated_conjecture,
( e21 != e21
| e20 != e20
| e21 != e21
| e22 != e22
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e10)) != e22
| h2(op1(e10,e11)) != e20 ),
inference(copy,[status(thm)],[c_2120]) ).
cnf(c_2122,negated_conjecture,
( e21 != e21
| e20 != e20
| e21 != e21
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e10)) != e22
| h2(op1(e10,e11)) != e20 ),
inference(copy,[status(thm)],[c_2121]) ).
cnf(c_2123,negated_conjecture,
( e21 != e21
| e20 != e20
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e10)) != e22
| h2(op1(e10,e11)) != e20 ),
inference(copy,[status(thm)],[c_2122]) ).
cnf(c_2124,negated_conjecture,
( e21 != e21
| h2(op1(e11,e13)) != e20
| h2(op1(e11,e10)) != e22
| h2(op1(e10,e11)) != e20 ),
inference(copy,[status(thm)],[c_2123]) ).
cnf(c_1865,negated_conjecture,
( h2(op1(e11,e13)) != e20
| h2(op1(e11,e10)) != e22
| h2(op1(e10,e11)) != e20 ),
inference(copy,[status(thm)],[c_2124]) ).
cnf(c_2125,plain,
( e10 = e11
| op1(e11,e10) = e11 ),
inference(paramod,[status(thm)],[c_1845,c_1790]) ).
cnf(c_2126,plain,
( e11 = e10
| op1(e11,e10) = e11 ),
inference(copy,[status(thm)],[c_2125]) ).
cnf(c_1866,plain,
op1(e11,e10) = e11,
inference(resolve,[status(thm)],[c_243,c_2126]) ).
cnf(c_2127,plain,
( e10 = e13
| op1(e10,e11) = e13 ),
inference(paramod,[status(thm)],[c_1846,c_1807]) ).
cnf(c_2128,plain,
( e13 = e10
| op1(e10,e11) = e13 ),
inference(copy,[status(thm)],[c_2127]) ).
cnf(c_1867,plain,
op1(e10,e11) = e13,
inference(resolve,[status(thm)],[c_246,c_2128]) ).
cnf(c_2129,plain,
( op1(e11,e13) = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_1846,c_1781]) ).
cnf(c_2130,plain,
( op1(e11,e13) = e13
| e13 = e10 ),
inference(copy,[status(thm)],[c_2129]) ).
cnf(c_1868,plain,
op1(e11,e13) = e13,
inference(resolve,[status(thm)],[c_246,c_2130]) ).
cnf(c_2131,negated_conjecture,
( h2(op1(e11,e13)) != e20
| h2(op1(e11,e10)) != e22
| h2(e13) != e20 ),
inference(paramod,[status(thm)],[c_1867,c_1865]) ).
cnf(c_2132,negated_conjecture,
( h2(op1(e11,e13)) != e20
| h2(op1(e11,e10)) != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_1716,c_2131]) ).
cnf(c_2133,negated_conjecture,
( h2(op1(e11,e13)) != e20
| h2(e11) != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_1866,c_2132]) ).
cnf(c_2134,negated_conjecture,
( h2(op1(e11,e13)) != e20
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_1742,c_2133]) ).
cnf(c_2135,negated_conjecture,
( h2(e13) != e20
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_1868,c_2134]) ).
cnf(c_2136,negated_conjecture,
( e20 != e20
| e22 != e22
| e20 != e20 ),
inference(paramod,[status(thm)],[c_1716,c_2135]) ).
cnf(c_2137,negated_conjecture,
( e20 != e20
| e22 != e22 ),
inference(copy,[status(thm)],[c_2136]) ).
cnf(c_2138,negated_conjecture,
e20 != e20,
inference(copy,[status(thm)],[c_2137]) ).
cnf(c_1870,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_2138]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG114+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n010.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 26 21:11:00 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 34701 was started by sandbox2 on n010,
% 0.11/0.37 % Sat Sep 26 21:11:00 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 4.66/5.00
% 4.66/5.00 % From the command line: assign(max_seconds, 300).
% 4.77/5.32
% 4.77/5.32 % SZS status Theorem for theBenchmark
% 4.77/5.32
% 4.77/5.32 % Proof 1 at 0.26 (+ 0.02) seconds.
% 4.77/5.32 % Length of proof is 188.
% 4.77/5.32 % Level of proof is 13.
% 4.77/5.32 % Maximum clause weight is 171.000.
% 4.77/5.32 % Given clauses 0.
% 4.77/5.32
% 4.77/5.32 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------