%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG037+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:19 AM UTC 2026
% Result : Theorem 73.23s 58.12s
% Output : CNFRefutation 73.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 117
% Number of leaves : 16
% Syntax : Number of formulae : 487 ( 112 unt; 0 def)
% Number of atoms : 3843 (3842 equ)
% Maximal formula atoms : 384 ( 7 avg)
% Number of connectives : 5177 (1821 ~;2659 |; 697 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 10 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,
( ( unit1 = e13
| unit1 = e12
| unit1 = e11
| unit1 = e10 )
& op1(e13,unit1) = e13
& op1(unit1,e13) = e13
& op1(e12,unit1) = e12
& op1(unit1,e12) = e12
& op1(e11,unit1) = e11
& op1(unit1,e11) = e11
& op1(e10,unit1) = e10
& op1(unit1,e10) = e10 ),
file('theBenchmark.p',ax2) ).
fof(ax3,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',ax3) ).
fof(ax4,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',ax4) ).
fof(ax5,axiom,
( ( unit2 = e23
| unit2 = e22
| unit2 = e21
| unit2 = e20 )
& op2(e23,unit2) = e23
& op2(unit2,e23) = e23
& op2(e22,unit2) = e22
& op2(unit2,e22) = e22
& op2(e21,unit2) = e21
& op2(unit2,e21) = e21
& op2(e20,unit2) = e20
& op2(unit2,e20) = e20 ),
file('theBenchmark.p',ax5) ).
fof(ax6,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',ax6) ).
fof(ax7,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',ax7) ).
fof(ax8,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',ax8) ).
fof(ax9,axiom,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('theBenchmark.p',ax9) ).
fof(ax10,axiom,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('theBenchmark.p',ax10) ).
fof(ax12,axiom,
( ( op1(e13,e13) = e13
& op1(e12,e12) = e13
& op1(e11,e11) = e13
& op1(e10,e10) = e13 )
| ( op1(e13,e13) = e12
& op1(e12,e12) = e12
& op1(e11,e11) = e12
& op1(e10,e10) = e12 )
| ( op1(e13,e13) = e11
& op1(e12,e12) = e11
& op1(e11,e11) = e11
& op1(e10,e10) = e11 )
| ( op1(e13,e13) = e10
& op1(e12,e12) = e10
& op1(e11,e11) = e10
& op1(e10,e10) = e10 ) ),
file('theBenchmark.p',ax12) ).
fof(ax13,axiom,
( ( op2(e23,e23) = e23
& op2(e22,e22) = e23
& op2(e21,e21) = e23
& op2(e20,e20) = e23 )
| ( op2(e23,e23) = e22
& op2(e22,e22) = e22
& op2(e21,e21) = e22
& op2(e20,e20) = e22 )
| ( op2(e23,e23) = e21
& op2(e22,e22) = e21
& op2(e21,e21) = e21
& op2(e20,e20) = e21 )
| ( op2(e23,e23) = e20
& op2(e22,e22) = e20
& op2(e21,e21) = e20
& op2(e20,e20) = e20 ) ),
file('theBenchmark.p',ax13) ).
fof(ax14,axiom,
( e12 = op1(e13,e11)
& e10 = op1(e11,e11) ),
file('theBenchmark.p',ax14) ).
fof(ax15,axiom,
( e22 = op2(e23,e21)
& e20 = op2(e21,e21) ),
file('theBenchmark.p',ax15) ).
fof(ax21,axiom,
( h6(e12) = op2(e23,e21)
& h6(e10) = op2(e21,e21)
& h6(e13) = e23
& h6(e11) = e21 ),
file('theBenchmark.p',ax21) ).
fof(co1,conjecture,
( ( ( h12(e13) = e23
| h12(e12) = e23
| h12(e11) = e23
| h12(e10) = e23 )
& ( h12(e13) = e22
| h12(e12) = e22
| h12(e11) = e22
| h12(e10) = e22 )
& ( h12(e13) = e21
| h12(e12) = e21
| h12(e11) = e21
| h12(e10) = e21 )
& ( h12(e13) = e20
| h12(e12) = e20
| h12(e11) = e20
| h12(e10) = e20 )
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e10)) = op2(h12(e10),h12(e10)) )
| ( ( h11(e13) = e23
| h11(e12) = e23
| h11(e11) = e23
| h11(e10) = e23 )
& ( h11(e13) = e22
| h11(e12) = e22
| h11(e11) = e22
| h11(e10) = e22 )
& ( h11(e13) = e21
| h11(e12) = e21
| h11(e11) = e21
| h11(e10) = e21 )
& ( h11(e13) = e20
| h11(e12) = e20
| h11(e11) = e20
| h11(e10) = e20 )
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e10)) = op2(h11(e10),h11(e10)) )
| ( ( h10(e13) = e23
| h10(e12) = e23
| h10(e11) = e23
| h10(e10) = e23 )
& ( h10(e13) = e22
| h10(e12) = e22
| h10(e11) = e22
| h10(e10) = e22 )
& ( h10(e13) = e21
| h10(e12) = e21
| h10(e11) = e21
| h10(e10) = e21 )
& ( h10(e13) = e20
| h10(e12) = e20
| h10(e11) = e20
| h10(e10) = e20 )
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e10)) = op2(h10(e10),h10(e10)) )
| ( ( h9(e13) = e23
| h9(e12) = e23
| h9(e11) = e23
| h9(e10) = e23 )
& ( h9(e13) = e22
| h9(e12) = e22
| h9(e11) = e22
| h9(e10) = e22 )
& ( h9(e13) = e21
| h9(e12) = e21
| h9(e11) = e21
| h9(e10) = e21 )
& ( h9(e13) = e20
| h9(e12) = e20
| h9(e11) = e20
| h9(e10) = e20 )
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e10)) = op2(h9(e10),h9(e10)) )
| ( ( h8(e13) = e23
| h8(e12) = e23
| h8(e11) = e23
| h8(e10) = e23 )
& ( h8(e13) = e22
| h8(e12) = e22
| h8(e11) = e22
| h8(e10) = e22 )
& ( h8(e13) = e21
| h8(e12) = e21
| h8(e11) = e21
| h8(e10) = e21 )
& ( h8(e13) = e20
| h8(e12) = e20
| h8(e11) = e20
| h8(e10) = e20 )
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e10)) = op2(h8(e10),h8(e10)) )
| ( ( h7(e13) = e23
| h7(e12) = e23
| h7(e11) = e23
| h7(e10) = e23 )
& ( h7(e13) = e22
| h7(e12) = e22
| h7(e11) = e22
| h7(e10) = e22 )
& ( h7(e13) = e21
| h7(e12) = e21
| h7(e11) = e21
| h7(e10) = e21 )
& ( h7(e13) = e20
| h7(e12) = e20
| h7(e11) = e20
| h7(e10) = e20 )
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e10)) = op2(h7(e10),h7(e10)) )
| ( ( h6(e13) = e23
| h6(e12) = e23
| h6(e11) = e23
| h6(e10) = e23 )
& ( h6(e13) = e22
| h6(e12) = e22
| h6(e11) = e22
| h6(e10) = e22 )
& ( h6(e13) = e21
| h6(e12) = e21
| h6(e11) = e21
| h6(e10) = e21 )
& ( h6(e13) = e20
| h6(e12) = e20
| h6(e11) = e20
| h6(e10) = e20 )
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e10)) = op2(h6(e10),h6(e10)) )
| ( ( h5(e13) = e23
| h5(e12) = e23
| h5(e11) = e23
| h5(e10) = e23 )
& ( h5(e13) = e22
| h5(e12) = e22
| h5(e11) = e22
| h5(e10) = e22 )
& ( h5(e13) = e21
| h5(e12) = e21
| h5(e11) = e21
| h5(e10) = e21 )
& ( h5(e13) = e20
| h5(e12) = e20
| h5(e11) = e20
| h5(e10) = e20 )
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e10)) = op2(h5(e10),h5(e10)) )
| ( ( 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,
~ ( ( ( h12(e13) = e23
| h12(e12) = e23
| h12(e11) = e23
| h12(e10) = e23 )
& ( h12(e13) = e22
| h12(e12) = e22
| h12(e11) = e22
| h12(e10) = e22 )
& ( h12(e13) = e21
| h12(e12) = e21
| h12(e11) = e21
| h12(e10) = e21 )
& ( h12(e13) = e20
| h12(e12) = e20
| h12(e11) = e20
| h12(e10) = e20 )
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e10)) = op2(h12(e10),h12(e10)) )
| ( ( h11(e13) = e23
| h11(e12) = e23
| h11(e11) = e23
| h11(e10) = e23 )
& ( h11(e13) = e22
| h11(e12) = e22
| h11(e11) = e22
| h11(e10) = e22 )
& ( h11(e13) = e21
| h11(e12) = e21
| h11(e11) = e21
| h11(e10) = e21 )
& ( h11(e13) = e20
| h11(e12) = e20
| h11(e11) = e20
| h11(e10) = e20 )
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e10)) = op2(h11(e10),h11(e10)) )
| ( ( h10(e13) = e23
| h10(e12) = e23
| h10(e11) = e23
| h10(e10) = e23 )
& ( h10(e13) = e22
| h10(e12) = e22
| h10(e11) = e22
| h10(e10) = e22 )
& ( h10(e13) = e21
| h10(e12) = e21
| h10(e11) = e21
| h10(e10) = e21 )
& ( h10(e13) = e20
| h10(e12) = e20
| h10(e11) = e20
| h10(e10) = e20 )
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e10)) = op2(h10(e10),h10(e10)) )
| ( ( h9(e13) = e23
| h9(e12) = e23
| h9(e11) = e23
| h9(e10) = e23 )
& ( h9(e13) = e22
| h9(e12) = e22
| h9(e11) = e22
| h9(e10) = e22 )
& ( h9(e13) = e21
| h9(e12) = e21
| h9(e11) = e21
| h9(e10) = e21 )
& ( h9(e13) = e20
| h9(e12) = e20
| h9(e11) = e20
| h9(e10) = e20 )
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e10)) = op2(h9(e10),h9(e10)) )
| ( ( h8(e13) = e23
| h8(e12) = e23
| h8(e11) = e23
| h8(e10) = e23 )
& ( h8(e13) = e22
| h8(e12) = e22
| h8(e11) = e22
| h8(e10) = e22 )
& ( h8(e13) = e21
| h8(e12) = e21
| h8(e11) = e21
| h8(e10) = e21 )
& ( h8(e13) = e20
| h8(e12) = e20
| h8(e11) = e20
| h8(e10) = e20 )
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e10)) = op2(h8(e10),h8(e10)) )
| ( ( h7(e13) = e23
| h7(e12) = e23
| h7(e11) = e23
| h7(e10) = e23 )
& ( h7(e13) = e22
| h7(e12) = e22
| h7(e11) = e22
| h7(e10) = e22 )
& ( h7(e13) = e21
| h7(e12) = e21
| h7(e11) = e21
| h7(e10) = e21 )
& ( h7(e13) = e20
| h7(e12) = e20
| h7(e11) = e20
| h7(e10) = e20 )
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e10)) = op2(h7(e10),h7(e10)) )
| ( ( h6(e13) = e23
| h6(e12) = e23
| h6(e11) = e23
| h6(e10) = e23 )
& ( h6(e13) = e22
| h6(e12) = e22
| h6(e11) = e22
| h6(e10) = e22 )
& ( h6(e13) = e21
| h6(e12) = e21
| h6(e11) = e21
| h6(e10) = e21 )
& ( h6(e13) = e20
| h6(e12) = e20
| h6(e11) = e20
| h6(e10) = e20 )
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e10)) = op2(h6(e10),h6(e10)) )
| ( ( h5(e13) = e23
| h5(e12) = e23
| h5(e11) = e23
| h5(e10) = e23 )
& ( h5(e13) = e22
| h5(e12) = e22
| h5(e11) = e22
| h5(e10) = e22 )
& ( h5(e13) = e21
| h5(e12) = e21
| h5(e11) = e21
| h5(e10) = e21 )
& ( h5(e13) = e20
| h5(e12) = e20
| h5(e11) = e20
| h5(e10) = e20 )
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e10)) = op2(h5(e10),h5(e10)) )
| ( ( 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_36,plain,
( op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11
| op1(e11,e13) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_38,plain,
( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_45,plain,
op1(unit1,e10) = e10,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_47,plain,
op1(unit1,e11) = e11,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_48,plain,
op1(e11,unit1) = e11,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_49,plain,
op1(unit1,e12) = e12,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_50,plain,
op1(e12,unit1) = e12,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_51,plain,
op1(unit1,e13) = e13,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_52,plain,
op1(e13,unit1) = e13,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_53,plain,
( unit1 = e13
| unit1 = e12
| unit1 = e11
| unit1 = e10 ),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_60,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_61,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| op1(e10,e10) = e13 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_68,plain,
( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e11) = e13
| op1(e11,e10) = e13 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_69,plain,
( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| op1(e10,e11) = e13 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_72,plain,
( op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_80,plain,
( op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_83,plain,
( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(clausify,[status(thm)],[ax3]) ).
cnf(c_93,plain,
( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| op2(e21,e23) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_95,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_102,plain,
op2(unit2,e20) = e20,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_104,plain,
op2(unit2,e21) = e21,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_105,plain,
op2(e21,unit2) = e21,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_106,plain,
op2(unit2,e22) = e22,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_107,plain,
op2(e22,unit2) = e22,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_108,plain,
op2(unit2,e23) = e23,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_109,plain,
op2(e23,unit2) = e23,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_110,plain,
( unit2 = e23
| unit2 = e22
| unit2 = e21
| unit2 = e20 ),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_117,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_118,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| op2(e20,e20) = e23 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_125,plain,
( op2(e21,e23) = e23
| op2(e21,e22) = e23
| op2(e21,e21) = e23
| op2(e21,e20) = e23 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_126,plain,
( op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e21,e21) = e23
| op2(e20,e21) = e23 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_129,plain,
( op2(e22,e23) = e21
| op2(e22,e22) = e21
| op2(e22,e21) = e21
| op2(e22,e20) = e21 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_137,plain,
( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_140,plain,
( op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 ),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_152,plain,
op1(e12,e11) != op1(e10,e11),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_154,plain,
op1(e12,e11) != op1(e11,e11),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_156,plain,
op1(e13,e11) != op1(e12,e11),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_164,plain,
op1(e11,e13) != op1(e10,e13),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_165,plain,
op1(e10,e13) != op1(e11,e13),
inference(copy,[status(thm)],[c_164]) ).
cnf(c_178,plain,
op1(e11,e11) != op1(e11,e10),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_179,plain,
op1(e11,e10) != op1(e11,e11),
inference(copy,[status(thm)],[c_178]) ).
cnf(c_181,plain,
op1(e11,e13) != op1(e11,e10),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_183,plain,
op1(e11,e13) != op1(e11,e11),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_187,plain,
op1(e12,e12) != op1(e12,e10),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_195,plain,
op1(e13,e13) != op1(e13,e10),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_208,plain,
op2(e22,e21) != op2(e20,e21),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_210,plain,
op2(e22,e21) != op2(e21,e21),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_212,plain,
op2(e23,e21) != op2(e22,e21),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_220,plain,
op2(e21,e23) != op2(e20,e23),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_221,plain,
op2(e20,e23) != op2(e21,e23),
inference(copy,[status(thm)],[c_220]) ).
cnf(c_234,plain,
op2(e21,e21) != op2(e21,e20),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_235,plain,
op2(e21,e20) != op2(e21,e21),
inference(copy,[status(thm)],[c_234]) ).
cnf(c_237,plain,
op2(e21,e23) != op2(e21,e20),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_239,plain,
op2(e21,e23) != op2(e21,e21),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_243,plain,
op2(e22,e22) != op2(e22,e20),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_251,plain,
op2(e23,e23) != op2(e23,e20),
inference(clausify,[status(thm)],[ax8]) ).
cnf(c_255,plain,
e11 != e10,
inference(clausify,[status(thm)],[ax9]) ).
cnf(c_256,plain,
e10 != e11,
inference(copy,[status(thm)],[c_255]) ).
cnf(c_257,plain,
e12 != e10,
inference(clausify,[status(thm)],[ax9]) ).
cnf(c_258,plain,
e13 != e10,
inference(clausify,[status(thm)],[ax9]) ).
cnf(c_259,plain,
e12 != e11,
inference(clausify,[status(thm)],[ax9]) ).
cnf(c_260,plain,
e13 != e11,
inference(clausify,[status(thm)],[ax9]) ).
cnf(c_261,plain,
e13 != e12,
inference(clausify,[status(thm)],[ax9]) ).
cnf(c_262,plain,
e21 != e20,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_263,plain,
e20 != e21,
inference(copy,[status(thm)],[c_262]) ).
cnf(c_264,plain,
e22 != e20,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_265,plain,
e23 != e20,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_266,plain,
e22 != e21,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_267,plain,
e23 != e21,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_268,plain,
e23 != e22,
inference(clausify,[status(thm)],[ax10]) ).
cnf(c_361,plain,
( op1(e11,e11) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e10,e10) = e10 ),
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_487,plain,
( op1(e11,e11) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e12,e12) = e10 ),
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_511,plain,
( op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e13,e13) = e10 ),
inference(clausify,[status(thm)],[ax12]) ).
cnf(c_613,plain,
( op2(e21,e21) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e20,e20) = e20 ),
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_739,plain,
( op2(e21,e21) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e22,e22) = e20 ),
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_763,plain,
( op2(e21,e21) = e23
| op2(e21,e21) = e22
| op2(e21,e21) = e21
| op2(e23,e23) = e20 ),
inference(clausify,[status(thm)],[ax13]) ).
cnf(c_805,plain,
op1(e11,e11) = e10,
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_806,plain,
op1(e13,e11) = e12,
inference(clausify,[status(thm)],[ax14]) ).
cnf(c_807,plain,
op2(e21,e21) = e20,
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_808,plain,
op2(e23,e21) = e22,
inference(clausify,[status(thm)],[ax15]) ).
cnf(c_831,plain,
h6(e11) = e21,
inference(clausify,[status(thm)],[ax21]) ).
cnf(c_832,plain,
h6(e13) = e23,
inference(clausify,[status(thm)],[ax21]) ).
cnf(c_833,plain,
h6(e10) = op2(e21,e21),
inference(clausify,[status(thm)],[ax21]) ).
cnf(c_834,plain,
h6(e10) = e20,
inference(paramod,[status(thm)],[c_807,c_833]) ).
cnf(c_835,plain,
h6(e12) = op2(e23,e21),
inference(clausify,[status(thm)],[ax21]) ).
cnf(c_836,plain,
h6(e12) = e22,
inference(paramod,[status(thm)],[c_808,c_835]) ).
cnf(c_2243,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e10,e12)) != op2(h6(e10),h6(e12))
| h6(op1(e10,e11)) != op2(h6(e10),h6(e11))
| h6(op1(e10,e10)) != op2(h6(e10),h6(e10)) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_4952,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e10,e12)) != op2(h6(e10),h6(e12))
| h6(op1(e10,e11)) != op2(h6(e10),h6(e11))
| h6(op1(e10,e10)) != op2(e20,h6(e10)) ),
inference(paramod,[status(thm)],[c_834,c_2243]) ).
cnf(c_4953,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e10,e12)) != op2(h6(e10),h6(e12))
| h6(op1(e10,e11)) != op2(h6(e10),h6(e11))
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_834,c_4952]) ).
cnf(c_4954,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e10,e12)) != op2(h6(e10),h6(e12))
| h6(op1(e10,e11)) != op2(e20,h6(e11))
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_834,c_4953]) ).
cnf(c_4955,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e10,e12)) != op2(h6(e10),h6(e12))
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_831,c_4954]) ).
cnf(c_4956,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e10,e12)) != op2(e20,h6(e12))
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_834,c_4955]) ).
cnf(c_4957,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_836,c_4956]) ).
cnf(c_4958,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e10,e13)) != op2(e20,h6(e13))
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_834,c_4957]) ).
cnf(c_4959,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_832,c_4958]) ).
cnf(c_4960,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(e21,h6(e10))
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_831,c_4959]) ).
cnf(c_4961,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_834,c_4960]) ).
cnf(c_4962,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(e10) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_805,c_4961]) ).
cnf(c_4963,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| e20 != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_834,c_4962]) ).
cnf(c_4964,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| e20 != op2(e21,h6(e11))
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_831,c_4963]) ).
cnf(c_4965,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| e20 != op2(e21,e21)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_831,c_4964]) ).
cnf(c_4966,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_807,c_4965]) ).
cnf(c_4967,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(e21,h6(e12))
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_831,c_4966]) ).
cnf(c_4968,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_836,c_4967]) ).
cnf(c_4969,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(e21,h6(e13))
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_831,c_4968]) ).
cnf(c_4970,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_832,c_4969]) ).
cnf(c_4971,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(e22,h6(e10))
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_836,c_4970]) ).
cnf(c_4972,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_834,c_4971]) ).
cnf(c_4973,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(e22,h6(e11))
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_836,c_4972]) ).
cnf(c_4974,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_831,c_4973]) ).
cnf(c_4975,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(e22,h6(e12))
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_836,c_4974]) ).
cnf(c_4976,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_836,c_4975]) ).
cnf(c_4977,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(e22,h6(e13))
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_836,c_4976]) ).
cnf(c_4978,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_832,c_4977]) ).
cnf(c_4979,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(e23,h6(e10))
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_832,c_4978]) ).
cnf(c_4980,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_834,c_4979]) ).
cnf(c_4981,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(e12) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_806,c_4980]) ).
cnf(c_4982,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| e22 != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_836,c_4981]) ).
cnf(c_4983,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| e22 != op2(e23,h6(e11))
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_832,c_4982]) ).
cnf(c_4984,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| e22 != op2(e23,e21)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_831,c_4983]) ).
cnf(c_4985,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| e22 != e22
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_808,c_4984]) ).
cnf(c_4986,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(e23,h6(e12))
| e22 != e22
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_832,c_4985]) ).
cnf(c_4987,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_836,c_4986]) ).
cnf(c_4988,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(e23,h6(e13))
| h6(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_832,c_4987]) ).
cnf(c_4989,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| h6(e10) != e20
| h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_832,c_4988]) ).
cnf(c_4990,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| h6(e11) != e21
| e20 != e20
| h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_834,c_4989]) ).
cnf(c_4991,negated_conjecture,
( h6(e13) != e23
| h6(e12) != e22
| e21 != e21
| e20 != e20
| h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_831,c_4990]) ).
cnf(c_4992,negated_conjecture,
( h6(e13) != e23
| e22 != e22
| e21 != e21
| e20 != e20
| h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_836,c_4991]) ).
cnf(c_4993,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20
| h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_832,c_4992]) ).
cnf(c_4994,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20
| h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| e22 != e22
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_4993]) ).
cnf(c_4995,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20
| h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_4994]) ).
cnf(c_4996,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_4995]) ).
cnf(c_4997,negated_conjecture,
( e23 != e23
| e22 != e22
| h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_4996]) ).
cnf(c_4998,negated_conjecture,
( e23 != e23
| h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_4997]) ).
cnf(c_2244,negated_conjecture,
( h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_4998]) ).
cnf(c_4999,plain,
( op1(e11,e11) = e13
| op1(e11,e11) = e12
| e10 = e11
| op1(e13,e13) = e10 ),
inference(paramod,[status(thm)],[c_805,c_511]) ).
cnf(c_5000,plain,
( op1(e11,e11) = e13
| e10 = e12
| e10 = e11
| op1(e13,e13) = e10 ),
inference(paramod,[status(thm)],[c_805,c_4999]) ).
cnf(c_5001,plain,
( e10 = e13
| e10 = e12
| e10 = e11
| op1(e13,e13) = e10 ),
inference(paramod,[status(thm)],[c_805,c_5000]) ).
cnf(c_5002,plain,
( e10 = e13
| e12 = e10
| e10 = e11
| op1(e13,e13) = e10 ),
inference(copy,[status(thm)],[c_5001]) ).
cnf(c_5003,plain,
( e13 = e10
| e12 = e10
| e10 = e11
| op1(e13,e13) = e10 ),
inference(copy,[status(thm)],[c_5002]) ).
cnf(c_5004,plain,
( e13 = e10
| e12 = e10
| op1(e13,e13) = e10 ),
inference(resolve,[status(thm)],[c_256,c_5003]) ).
cnf(c_5005,plain,
( e13 = e10
| op1(e13,e13) = e10 ),
inference(resolve,[status(thm)],[c_257,c_5004]) ).
cnf(c_4171,plain,
op1(e13,e13) = e10,
inference(resolve,[status(thm)],[c_258,c_5005]) ).
cnf(c_5006,plain,
( op1(e11,e11) = e13
| op1(e13,e13) = e12
| e10 = e11
| op1(e12,e12) = e10 ),
inference(paramod,[status(thm)],[c_4171,c_487]) ).
cnf(c_5007,plain,
( op1(e11,e11) = e13
| e10 = e12
| e10 = e11
| op1(e12,e12) = e10 ),
inference(paramod,[status(thm)],[c_4171,c_5006]) ).
cnf(c_5008,plain,
( e10 = e13
| e10 = e12
| e10 = e11
| op1(e12,e12) = e10 ),
inference(paramod,[status(thm)],[c_805,c_5007]) ).
cnf(c_5009,plain,
( e10 = e13
| e12 = e10
| e10 = e11
| op1(e12,e12) = e10 ),
inference(copy,[status(thm)],[c_5008]) ).
cnf(c_5010,plain,
( e13 = e10
| e12 = e10
| e10 = e11
| op1(e12,e12) = e10 ),
inference(copy,[status(thm)],[c_5009]) ).
cnf(c_5011,plain,
( e13 = e10
| e12 = e10
| op1(e12,e12) = e10 ),
inference(resolve,[status(thm)],[c_256,c_5010]) ).
cnf(c_5012,plain,
( e13 = e10
| op1(e12,e12) = e10 ),
inference(resolve,[status(thm)],[c_257,c_5011]) ).
cnf(c_4172,plain,
op1(e12,e12) = e10,
inference(resolve,[status(thm)],[c_258,c_5012]) ).
cnf(c_5013,plain,
( op1(e11,e11) = e13
| op1(e13,e13) = e12
| e10 = e11
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_4171,c_361]) ).
cnf(c_5014,plain,
( op1(e11,e11) = e13
| e10 = e12
| e10 = e11
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_4171,c_5013]) ).
cnf(c_5015,plain,
( e10 = e13
| e10 = e12
| e10 = e11
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_805,c_5014]) ).
cnf(c_5016,plain,
( e10 = e13
| e12 = e10
| e10 = e11
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_5015]) ).
cnf(c_5017,plain,
( e13 = e10
| e12 = e10
| e10 = e11
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_5016]) ).
cnf(c_5018,plain,
( e13 = e10
| e12 = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_256,c_5017]) ).
cnf(c_5019,plain,
( e13 = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_257,c_5018]) ).
cnf(c_4173,plain,
op1(e10,e10) = e10,
inference(resolve,[status(thm)],[c_258,c_5019]) ).
cnf(c_4174,plain,
op1(e11,e13) != e10,
inference(paramod,[status(thm)],[c_805,c_183]) ).
cnf(c_4176,plain,
op1(e11,e10) != e10,
inference(paramod,[status(thm)],[c_805,c_179]) ).
cnf(c_4177,plain,
op1(e12,e11) != e10,
inference(paramod,[status(thm)],[c_805,c_154]) ).
cnf(c_5020,plain,
( op1(e13,e11) = e13
| op1(e12,e11) = e13
| e10 = e13
| op1(e10,e11) = e13 ),
inference(paramod,[status(thm)],[c_805,c_69]) ).
cnf(c_5021,plain,
( e12 = e13
| op1(e12,e11) = e13
| e10 = e13
| op1(e10,e11) = e13 ),
inference(paramod,[status(thm)],[c_806,c_5020]) ).
cnf(c_5022,plain,
( e12 = e13
| op1(e12,e11) = e13
| e13 = e10
| op1(e10,e11) = e13 ),
inference(copy,[status(thm)],[c_5021]) ).
cnf(c_5023,plain,
( e13 = e12
| op1(e12,e11) = e13
| e13 = e10
| op1(e10,e11) = e13 ),
inference(copy,[status(thm)],[c_5022]) ).
cnf(c_5024,plain,
( e13 = e12
| op1(e12,e11) = e13
| op1(e10,e11) = e13 ),
inference(resolve,[status(thm)],[c_258,c_5023]) ).
cnf(c_4179,plain,
( op1(e12,e11) = e13
| op1(e10,e11) = e13 ),
inference(resolve,[status(thm)],[c_261,c_5024]) ).
cnf(c_5025,plain,
( op1(e11,e13) = e13
| op1(e11,e12) = e13
| e10 = e13
| op1(e11,e10) = e13 ),
inference(paramod,[status(thm)],[c_805,c_68]) ).
cnf(c_5026,plain,
( op1(e11,e13) = e13
| op1(e11,e12) = e13
| e13 = e10
| op1(e11,e10) = e13 ),
inference(copy,[status(thm)],[c_5025]) ).
cnf(c_4180,plain,
( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e10) = e13 ),
inference(resolve,[status(thm)],[c_258,c_5026]) ).
cnf(c_5027,plain,
e12 != op1(e12,e11),
inference(paramod,[status(thm)],[c_806,c_156]) ).
cnf(c_4186,plain,
op1(e12,e11) != e12,
inference(copy,[status(thm)],[c_5027]) ).
cnf(c_5028,plain,
( op1(e13,e13) = e11
| op1(e13,e12) = e11
| e12 = e11
| op1(e13,e10) = e11 ),
inference(paramod,[status(thm)],[c_806,c_80]) ).
cnf(c_5029,plain,
( e10 = e11
| op1(e13,e12) = e11
| e12 = e11
| op1(e13,e10) = e11 ),
inference(paramod,[status(thm)],[c_4171,c_5028]) ).
cnf(c_5030,plain,
( e10 = e11
| op1(e13,e12) = e11
| op1(e13,e10) = e11 ),
inference(resolve,[status(thm)],[c_259,c_5029]) ).
cnf(c_4189,plain,
( op1(e13,e12) = e11
| op1(e13,e10) = e11 ),
inference(resolve,[status(thm)],[c_256,c_5030]) ).
cnf(c_5031,plain,
( op2(e21,e21) = e23
| op2(e21,e21) = e22
| e20 = e21
| op2(e23,e23) = e20 ),
inference(paramod,[status(thm)],[c_807,c_763]) ).
cnf(c_5032,plain,
( op2(e21,e21) = e23
| e20 = e22
| e20 = e21
| op2(e23,e23) = e20 ),
inference(paramod,[status(thm)],[c_807,c_5031]) ).
cnf(c_5033,plain,
( e20 = e23
| e20 = e22
| e20 = e21
| op2(e23,e23) = e20 ),
inference(paramod,[status(thm)],[c_807,c_5032]) ).
cnf(c_5034,plain,
( e20 = e23
| e22 = e20
| e20 = e21
| op2(e23,e23) = e20 ),
inference(copy,[status(thm)],[c_5033]) ).
cnf(c_5035,plain,
( e23 = e20
| e22 = e20
| e20 = e21
| op2(e23,e23) = e20 ),
inference(copy,[status(thm)],[c_5034]) ).
cnf(c_5036,plain,
( e23 = e20
| e22 = e20
| op2(e23,e23) = e20 ),
inference(resolve,[status(thm)],[c_263,c_5035]) ).
cnf(c_5037,plain,
( e23 = e20
| op2(e23,e23) = e20 ),
inference(resolve,[status(thm)],[c_264,c_5036]) ).
cnf(c_4208,plain,
op2(e23,e23) = e20,
inference(resolve,[status(thm)],[c_265,c_5037]) ).
cnf(c_5038,plain,
( op2(e21,e21) = e23
| op2(e23,e23) = e22
| e20 = e21
| op2(e22,e22) = e20 ),
inference(paramod,[status(thm)],[c_4208,c_739]) ).
cnf(c_5039,plain,
( op2(e21,e21) = e23
| e20 = e22
| e20 = e21
| op2(e22,e22) = e20 ),
inference(paramod,[status(thm)],[c_4208,c_5038]) ).
cnf(c_5040,plain,
( e20 = e23
| e20 = e22
| e20 = e21
| op2(e22,e22) = e20 ),
inference(paramod,[status(thm)],[c_807,c_5039]) ).
cnf(c_5041,plain,
( e20 = e23
| e22 = e20
| e20 = e21
| op2(e22,e22) = e20 ),
inference(copy,[status(thm)],[c_5040]) ).
cnf(c_5042,plain,
( e23 = e20
| e22 = e20
| e20 = e21
| op2(e22,e22) = e20 ),
inference(copy,[status(thm)],[c_5041]) ).
cnf(c_5043,plain,
( e23 = e20
| e22 = e20
| op2(e22,e22) = e20 ),
inference(resolve,[status(thm)],[c_263,c_5042]) ).
cnf(c_5044,plain,
( e23 = e20
| op2(e22,e22) = e20 ),
inference(resolve,[status(thm)],[c_264,c_5043]) ).
cnf(c_4209,plain,
op2(e22,e22) = e20,
inference(resolve,[status(thm)],[c_265,c_5044]) ).
cnf(c_5045,plain,
( op2(e21,e21) = e23
| op2(e23,e23) = e22
| e20 = e21
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_4208,c_613]) ).
cnf(c_5046,plain,
( op2(e21,e21) = e23
| e20 = e22
| e20 = e21
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_4208,c_5045]) ).
cnf(c_5047,plain,
( e20 = e23
| e20 = e22
| e20 = e21
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_807,c_5046]) ).
cnf(c_5048,plain,
( e20 = e23
| e22 = e20
| e20 = e21
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_5047]) ).
cnf(c_5049,plain,
( e23 = e20
| e22 = e20
| e20 = e21
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_5048]) ).
cnf(c_5050,plain,
( e23 = e20
| e22 = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_263,c_5049]) ).
cnf(c_5051,plain,
( e23 = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_264,c_5050]) ).
cnf(c_4210,plain,
op2(e20,e20) = e20,
inference(resolve,[status(thm)],[c_265,c_5051]) ).
cnf(c_4211,plain,
op2(e21,e23) != e20,
inference(paramod,[status(thm)],[c_807,c_239]) ).
cnf(c_4213,plain,
op2(e21,e20) != e20,
inference(paramod,[status(thm)],[c_807,c_235]) ).
cnf(c_4214,plain,
op2(e22,e21) != e20,
inference(paramod,[status(thm)],[c_807,c_210]) ).
cnf(c_5052,plain,
( op2(e23,e21) = e23
| op2(e22,e21) = e23
| e20 = e23
| op2(e20,e21) = e23 ),
inference(paramod,[status(thm)],[c_807,c_126]) ).
cnf(c_5053,plain,
( e22 = e23
| op2(e22,e21) = e23
| e20 = e23
| op2(e20,e21) = e23 ),
inference(paramod,[status(thm)],[c_808,c_5052]) ).
cnf(c_5054,plain,
( e22 = e23
| op2(e22,e21) = e23
| e23 = e20
| op2(e20,e21) = e23 ),
inference(copy,[status(thm)],[c_5053]) ).
cnf(c_5055,plain,
( e23 = e22
| op2(e22,e21) = e23
| e23 = e20
| op2(e20,e21) = e23 ),
inference(copy,[status(thm)],[c_5054]) ).
cnf(c_5056,plain,
( e23 = e22
| op2(e22,e21) = e23
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_265,c_5055]) ).
cnf(c_4216,plain,
( op2(e22,e21) = e23
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_268,c_5056]) ).
cnf(c_5057,plain,
( op2(e21,e23) = e23
| op2(e21,e22) = e23
| e20 = e23
| op2(e21,e20) = e23 ),
inference(paramod,[status(thm)],[c_807,c_125]) ).
cnf(c_5058,plain,
( op2(e21,e23) = e23
| op2(e21,e22) = e23
| e23 = e20
| op2(e21,e20) = e23 ),
inference(copy,[status(thm)],[c_5057]) ).
cnf(c_4217,plain,
( op2(e21,e23) = e23
| op2(e21,e22) = e23
| op2(e21,e20) = e23 ),
inference(resolve,[status(thm)],[c_265,c_5058]) ).
cnf(c_5059,plain,
e22 != op2(e22,e21),
inference(paramod,[status(thm)],[c_808,c_212]) ).
cnf(c_4223,plain,
op2(e22,e21) != e22,
inference(copy,[status(thm)],[c_5059]) ).
cnf(c_5060,plain,
( op2(e23,e23) = e21
| op2(e23,e22) = e21
| e22 = e21
| op2(e23,e20) = e21 ),
inference(paramod,[status(thm)],[c_808,c_137]) ).
cnf(c_5061,plain,
( e20 = e21
| op2(e23,e22) = e21
| e22 = e21
| op2(e23,e20) = e21 ),
inference(paramod,[status(thm)],[c_4208,c_5060]) ).
cnf(c_5062,plain,
( e20 = e21
| op2(e23,e22) = e21
| op2(e23,e20) = e21 ),
inference(resolve,[status(thm)],[c_266,c_5061]) ).
cnf(c_4226,plain,
( op2(e23,e22) = e21
| op2(e23,e20) = e21 ),
inference(resolve,[status(thm)],[c_263,c_5062]) ).
cnf(c_5063,negated_conjecture,
( h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| h6(e10) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_4173,c_2244]) ).
cnf(c_5064,negated_conjecture,
( h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_834,c_5063]) ).
cnf(c_5065,negated_conjecture,
( h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e12)) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4210,c_5064]) ).
cnf(c_5066,negated_conjecture,
( h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(e10) != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4172,c_5065]) ).
cnf(c_5067,negated_conjecture,
( h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| e20 != op2(e22,e22)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_834,c_5066]) ).
cnf(c_5068,negated_conjecture,
( h6(op1(e13,e13)) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4209,c_5067]) ).
cnf(c_5069,negated_conjecture,
( h6(e10) != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4171,c_5068]) ).
cnf(c_5070,negated_conjecture,
( e20 != op2(e23,e23)
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_834,c_5069]) ).
cnf(c_5071,negated_conjecture,
( e20 != e20
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4208,c_5070]) ).
cnf(c_5072,negated_conjecture,
( e20 != e20
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| e20 != e20
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21) ),
inference(copy,[status(thm)],[c_5071]) ).
cnf(c_5073,negated_conjecture,
( e20 != e20
| h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21) ),
inference(copy,[status(thm)],[c_5072]) ).
cnf(c_4235,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(op1(e10,e11)) != op2(e20,e21) ),
inference(copy,[status(thm)],[c_5073]) ).
cnf(c_5074,plain,
e10 != op1(e13,e10),
inference(paramod,[status(thm)],[c_4171,c_195]) ).
cnf(c_4240,plain,
op1(e13,e10) != e10,
inference(copy,[status(thm)],[c_5074]) ).
cnf(c_5075,plain,
( e10 = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(paramod,[status(thm)],[c_4171,c_83]) ).
cnf(c_5076,plain,
( e12 = e10
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(copy,[status(thm)],[c_5075]) ).
cnf(c_4244,plain,
( op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(resolve,[status(thm)],[c_257,c_5076]) ).
cnf(c_5077,plain,
e10 != op1(e12,e10),
inference(paramod,[status(thm)],[c_4172,c_187]) ).
cnf(c_4246,plain,
op1(e12,e10) != e10,
inference(copy,[status(thm)],[c_5077]) ).
cnf(c_5078,plain,
( op1(e12,e13) = e11
| e10 = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 ),
inference(paramod,[status(thm)],[c_4172,c_72]) ).
cnf(c_4253,plain,
( op1(e12,e13) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 ),
inference(resolve,[status(thm)],[c_256,c_5078]) ).
cnf(c_5079,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_4173,c_61]) ).
cnf(c_5080,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| e13 = e10 ),
inference(copy,[status(thm)],[c_5079]) ).
cnf(c_4254,plain,
( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13 ),
inference(resolve,[status(thm)],[c_258,c_5080]) ).
cnf(c_5081,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_4173,c_60]) ).
cnf(c_5082,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| e13 = e10 ),
inference(copy,[status(thm)],[c_5081]) ).
cnf(c_4255,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13 ),
inference(resolve,[status(thm)],[c_258,c_5082]) ).
cnf(c_4260,plain,
( op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11 ),
inference(resolve,[status(thm)],[c_4174,c_36]) ).
cnf(c_5083,plain,
( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11 ),
inference(resolve,[status(thm)],[c_4177,c_38]) ).
cnf(c_4263,plain,
( op1(e12,e11) = e13
| op1(e12,e11) = e11 ),
inference(resolve,[status(thm)],[c_4186,c_5083]) ).
cnf(c_5084,plain,
e20 != op2(e23,e20),
inference(paramod,[status(thm)],[c_4208,c_251]) ).
cnf(c_4271,plain,
op2(e23,e20) != e20,
inference(copy,[status(thm)],[c_5084]) ).
cnf(c_5085,plain,
( e20 = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 ),
inference(paramod,[status(thm)],[c_4208,c_140]) ).
cnf(c_5086,plain,
( e22 = e20
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 ),
inference(copy,[status(thm)],[c_5085]) ).
cnf(c_4275,plain,
( op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 ),
inference(resolve,[status(thm)],[c_264,c_5086]) ).
cnf(c_5087,plain,
e20 != op2(e22,e20),
inference(paramod,[status(thm)],[c_4209,c_243]) ).
cnf(c_4280,plain,
op2(e22,e20) != e20,
inference(copy,[status(thm)],[c_5087]) ).
cnf(c_5088,plain,
( op2(e22,e23) = e21
| e20 = e21
| op2(e22,e21) = e21
| op2(e22,e20) = e21 ),
inference(paramod,[status(thm)],[c_4209,c_129]) ).
cnf(c_4287,plain,
( op2(e22,e23) = e21
| op2(e22,e21) = e21
| op2(e22,e20) = e21 ),
inference(resolve,[status(thm)],[c_263,c_5088]) ).
cnf(c_5089,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_4210,c_118]) ).
cnf(c_5090,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| e23 = e20 ),
inference(copy,[status(thm)],[c_5089]) ).
cnf(c_4291,plain,
( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23 ),
inference(resolve,[status(thm)],[c_265,c_5090]) ).
cnf(c_5091,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_4210,c_117]) ).
cnf(c_5092,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| e23 = e20 ),
inference(copy,[status(thm)],[c_5091]) ).
cnf(c_4292,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23 ),
inference(resolve,[status(thm)],[c_265,c_5092]) ).
cnf(c_4297,plain,
( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21 ),
inference(resolve,[status(thm)],[c_4211,c_93]) ).
cnf(c_5093,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21 ),
inference(resolve,[status(thm)],[c_4214,c_95]) ).
cnf(c_4300,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e21 ),
inference(resolve,[status(thm)],[c_4223,c_5093]) ).
cnf(c_5094,plain,
( op1(e11,e10) = e10
| unit1 = e13
| unit1 = e12
| unit1 = e10 ),
inference(paramod,[status(thm)],[c_53,c_45]) ).
cnf(c_4312,plain,
( unit1 = e13
| unit1 = e12
| unit1 = e10 ),
inference(resolve,[status(thm)],[c_4176,c_5094]) ).
cnf(c_5095,plain,
( op2(e21,e20) = e20
| unit2 = e23
| unit2 = e22
| unit2 = e20 ),
inference(paramod,[status(thm)],[c_110,c_102]) ).
cnf(c_4321,plain,
( unit2 = e23
| unit2 = e22
| unit2 = e20 ),
inference(resolve,[status(thm)],[c_4213,c_5095]) ).
cnf(c_5096,plain,
( e12 = e13
| op1(e11,e12) = e13
| op1(e11,e10) = e13
| op1(e12,e13) = e12
| op1(e10,e13) = e12 ),
inference(paramod,[status(thm)],[c_4244,c_4180]) ).
cnf(c_5097,plain,
( e13 = e12
| op1(e11,e12) = e13
| op1(e11,e10) = e13
| op1(e12,e13) = e12
| op1(e10,e13) = e12 ),
inference(copy,[status(thm)],[c_5096]) ).
cnf(c_4424,plain,
( op1(e11,e12) = e13
| op1(e11,e10) = e13
| op1(e12,e13) = e12
| op1(e10,e13) = e12 ),
inference(resolve,[status(thm)],[c_261,c_5097]) ).
cnf(c_5098,plain,
( e11 = e13
| op1(e10,e11) = e13
| op1(e12,e13) = e11
| op1(e12,e10) = e11 ),
inference(paramod,[status(thm)],[c_4253,c_4179]) ).
cnf(c_5099,plain,
( e13 = e11
| op1(e10,e11) = e13
| op1(e12,e13) = e11
| op1(e12,e10) = e11 ),
inference(copy,[status(thm)],[c_5098]) ).
cnf(c_4485,plain,
( op1(e10,e11) = e13
| op1(e12,e13) = e11
| op1(e12,e10) = e11 ),
inference(resolve,[status(thm)],[c_260,c_5099]) ).
cnf(c_5100,plain,
( op1(e13,e12) = e11
| e13 = e11
| op1(e12,e10) = e13
| op1(e11,e10) = e13 ),
inference(paramod,[status(thm)],[c_4254,c_4189]) ).
cnf(c_4497,plain,
( op1(e13,e12) = e11
| op1(e12,e10) = e13
| op1(e11,e10) = e13 ),
inference(resolve,[status(thm)],[c_260,c_5100]) ).
cnf(c_5101,plain,
( e13 != op1(e11,e13)
| op1(e10,e12) = e13
| op1(e10,e11) = e13 ),
inference(paramod,[status(thm)],[c_4255,c_165]) ).
cnf(c_4503,plain,
( op1(e11,e13) != e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13 ),
inference(copy,[status(thm)],[c_5101]) ).
cnf(c_5102,plain,
( e11 != op1(e11,e10)
| op1(e11,e13) = e13
| op1(e11,e13) = e12 ),
inference(paramod,[status(thm)],[c_4260,c_181]) ).
cnf(c_4555,plain,
( op1(e11,e10) != e11
| op1(e11,e13) = e13
| op1(e11,e13) = e12 ),
inference(copy,[status(thm)],[c_5102]) ).
cnf(c_5103,plain,
( e11 != op1(e10,e11)
| op1(e12,e11) = e13 ),
inference(paramod,[status(thm)],[c_4263,c_152]) ).
cnf(c_4583,plain,
( op1(e10,e11) != e11
| op1(e12,e11) = e13 ),
inference(copy,[status(thm)],[c_5103]) ).
cnf(c_5104,plain,
( e22 = e23
| op2(e21,e22) = e23
| op2(e21,e20) = e23
| op2(e22,e23) = e22
| op2(e20,e23) = e22 ),
inference(paramod,[status(thm)],[c_4275,c_4217]) ).
cnf(c_5105,plain,
( e23 = e22
| op2(e21,e22) = e23
| op2(e21,e20) = e23
| op2(e22,e23) = e22
| op2(e20,e23) = e22 ),
inference(copy,[status(thm)],[c_5104]) ).
cnf(c_4619,plain,
( op2(e21,e22) = e23
| op2(e21,e20) = e23
| op2(e22,e23) = e22
| op2(e20,e23) = e22 ),
inference(resolve,[status(thm)],[c_268,c_5105]) ).
cnf(c_5106,plain,
( e21 = e23
| op2(e20,e21) = e23
| op2(e22,e23) = e21
| op2(e22,e20) = e21 ),
inference(paramod,[status(thm)],[c_4287,c_4216]) ).
cnf(c_5107,plain,
( e23 = e21
| op2(e20,e21) = e23
| op2(e22,e23) = e21
| op2(e22,e20) = e21 ),
inference(copy,[status(thm)],[c_5106]) ).
cnf(c_4680,plain,
( op2(e20,e21) = e23
| op2(e22,e23) = e21
| op2(e22,e20) = e21 ),
inference(resolve,[status(thm)],[c_267,c_5107]) ).
cnf(c_5108,plain,
( op2(e23,e22) = e21
| e23 = e21
| op2(e22,e20) = e23
| op2(e21,e20) = e23 ),
inference(paramod,[status(thm)],[c_4291,c_4226]) ).
cnf(c_4692,plain,
( op2(e23,e22) = e21
| op2(e22,e20) = e23
| op2(e21,e20) = e23 ),
inference(resolve,[status(thm)],[c_267,c_5108]) ).
cnf(c_5109,plain,
( e23 != op2(e21,e23)
| op2(e20,e22) = e23
| op2(e20,e21) = e23 ),
inference(paramod,[status(thm)],[c_4292,c_221]) ).
cnf(c_4698,plain,
( op2(e21,e23) != e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23 ),
inference(copy,[status(thm)],[c_5109]) ).
cnf(c_5110,plain,
( e21 != op2(e21,e20)
| op2(e21,e23) = e23
| op2(e21,e23) = e22 ),
inference(paramod,[status(thm)],[c_4297,c_237]) ).
cnf(c_4750,plain,
( op2(e21,e20) != e21
| op2(e21,e23) = e23
| op2(e21,e23) = e22 ),
inference(copy,[status(thm)],[c_5110]) ).
cnf(c_5111,plain,
( e21 != op2(e20,e21)
| op2(e22,e21) = e23 ),
inference(paramod,[status(thm)],[c_4300,c_208]) ).
cnf(c_4778,plain,
( op2(e20,e21) != e21
| op2(e22,e21) = e23 ),
inference(copy,[status(thm)],[c_5111]) ).
cnf(c_5112,plain,
( op1(e12,e10) = e10
| unit1 = e13
| unit1 = e10 ),
inference(paramod,[status(thm)],[c_4312,c_45]) ).
cnf(c_4886,plain,
( unit1 = e13
| unit1 = e10 ),
inference(resolve,[status(thm)],[c_4246,c_5112]) ).
cnf(c_5113,plain,
( op1(e13,e10) = e10
| unit1 = e10 ),
inference(paramod,[status(thm)],[c_4886,c_45]) ).
cnf(c_4894,plain,
unit1 = e10,
inference(resolve,[status(thm)],[c_4240,c_5113]) ).
cnf(c_5114,plain,
( op1(e10,e11) = e11
| unit1 = e13 ),
inference(paramod,[status(thm)],[c_4886,c_47]) ).
cnf(c_5115,plain,
( op1(e10,e11) = e11
| e10 = e13 ),
inference(paramod,[status(thm)],[c_4894,c_5114]) ).
cnf(c_5116,plain,
( op1(e10,e11) = e11
| e13 = e10 ),
inference(copy,[status(thm)],[c_5115]) ).
cnf(c_4895,plain,
op1(e10,e11) = e11,
inference(resolve,[status(thm)],[c_258,c_5116]) ).
cnf(c_5117,plain,
( op1(e11,e10) = e11
| unit1 = e13 ),
inference(paramod,[status(thm)],[c_4886,c_48]) ).
cnf(c_5118,plain,
( op1(e11,e10) = e11
| e10 = e13 ),
inference(paramod,[status(thm)],[c_4894,c_5117]) ).
cnf(c_5119,plain,
( op1(e11,e10) = e11
| e13 = e10 ),
inference(copy,[status(thm)],[c_5118]) ).
cnf(c_4896,plain,
op1(e11,e10) = e11,
inference(resolve,[status(thm)],[c_258,c_5119]) ).
cnf(c_5120,plain,
( op1(e10,e12) = e12
| unit1 = e13 ),
inference(paramod,[status(thm)],[c_4886,c_49]) ).
cnf(c_5121,plain,
( op1(e10,e12) = e12
| e10 = e13 ),
inference(paramod,[status(thm)],[c_4894,c_5120]) ).
cnf(c_5122,plain,
( op1(e10,e12) = e12
| e13 = e10 ),
inference(copy,[status(thm)],[c_5121]) ).
cnf(c_4897,plain,
op1(e10,e12) = e12,
inference(resolve,[status(thm)],[c_258,c_5122]) ).
cnf(c_5123,plain,
( op1(e12,e10) = e12
| unit1 = e13 ),
inference(paramod,[status(thm)],[c_4886,c_50]) ).
cnf(c_5124,plain,
( op1(e12,e10) = e12
| e10 = e13 ),
inference(paramod,[status(thm)],[c_4894,c_5123]) ).
cnf(c_5125,plain,
( op1(e12,e10) = e12
| e13 = e10 ),
inference(copy,[status(thm)],[c_5124]) ).
cnf(c_4898,plain,
op1(e12,e10) = e12,
inference(resolve,[status(thm)],[c_258,c_5125]) ).
cnf(c_5126,plain,
( op1(e10,e13) = e13
| unit1 = e13 ),
inference(paramod,[status(thm)],[c_4886,c_51]) ).
cnf(c_5127,plain,
( op1(e10,e13) = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_4894,c_5126]) ).
cnf(c_5128,plain,
( op1(e10,e13) = e13
| e13 = e10 ),
inference(copy,[status(thm)],[c_5127]) ).
cnf(c_4899,plain,
op1(e10,e13) = e13,
inference(resolve,[status(thm)],[c_258,c_5128]) ).
cnf(c_5129,plain,
( op1(e13,e10) = e13
| unit1 = e13 ),
inference(paramod,[status(thm)],[c_4886,c_52]) ).
cnf(c_5130,plain,
( op1(e13,e10) = e13
| e10 = e13 ),
inference(paramod,[status(thm)],[c_4894,c_5129]) ).
cnf(c_5131,plain,
( op1(e13,e10) = e13
| e13 = e10 ),
inference(copy,[status(thm)],[c_5130]) ).
cnf(c_4900,plain,
op1(e13,e10) = e13,
inference(resolve,[status(thm)],[c_258,c_5131]) ).
cnf(c_5132,plain,
( e11 != e11
| op1(e12,e11) = e13 ),
inference(paramod,[status(thm)],[c_4895,c_4583]) ).
cnf(c_4902,plain,
op1(e12,e11) = e13,
inference(copy,[status(thm)],[c_5132]) ).
cnf(c_5133,plain,
( op1(e11,e13) != e13
| op1(e10,e12) = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_4895,c_4503]) ).
cnf(c_5134,plain,
( op1(e11,e13) != e13
| e12 = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_4897,c_5133]) ).
cnf(c_5135,plain,
( op1(e11,e13) != e13
| e12 = e13
| e13 = e11 ),
inference(copy,[status(thm)],[c_5134]) ).
cnf(c_5136,plain,
( op1(e11,e13) != e13
| e13 = e12
| e13 = e11 ),
inference(copy,[status(thm)],[c_5135]) ).
cnf(c_5137,plain,
( op1(e11,e13) != e13
| e13 = e12 ),
inference(resolve,[status(thm)],[c_260,c_5136]) ).
cnf(c_4905,plain,
op1(e11,e13) != e13,
inference(resolve,[status(thm)],[c_261,c_5137]) ).
cnf(c_5138,plain,
( op1(e10,e11) = e13
| op1(e12,e13) = e11
| e12 = e11 ),
inference(paramod,[status(thm)],[c_4898,c_4485]) ).
cnf(c_5139,plain,
( e11 = e13
| op1(e12,e13) = e11
| e12 = e11 ),
inference(paramod,[status(thm)],[c_4895,c_5138]) ).
cnf(c_5140,plain,
( e13 = e11
| op1(e12,e13) = e11
| e12 = e11 ),
inference(copy,[status(thm)],[c_5139]) ).
cnf(c_5141,plain,
( e13 = e11
| op1(e12,e13) = e11 ),
inference(resolve,[status(thm)],[c_259,c_5140]) ).
cnf(c_4906,plain,
op1(e12,e13) = e11,
inference(resolve,[status(thm)],[c_260,c_5141]) ).
cnf(c_5142,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| h6(e11) != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_4895,c_4235]) ).
cnf(c_5143,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(op1(e10,e12)) != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_831,c_5142]) ).
cnf(c_5144,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| h6(e12) != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_4897,c_5143]) ).
cnf(c_5145,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(op1(e10,e13)) != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_836,c_5144]) ).
cnf(c_5146,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| h6(e13) != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_4899,c_5145]) ).
cnf(c_5147,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(op1(e11,e10)) != op2(e21,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_832,c_5146]) ).
cnf(c_5148,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| h6(e11) != op2(e21,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_4896,c_5147]) ).
cnf(c_5149,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(op1(e12,e10)) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e21 != op2(e21,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_831,c_5148]) ).
cnf(c_5150,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e11)) != op2(e22,e21)
| h6(e12) != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e21 != op2(e21,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_4898,c_5149]) ).
cnf(c_5151,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(op1(e12,e11)) != op2(e22,e21)
| e22 != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e21 != op2(e21,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_836,c_5150]) ).
cnf(c_5152,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| h6(e13) != op2(e22,e21)
| e22 != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e21 != op2(e21,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_4902,c_5151]) ).
cnf(c_5153,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(op1(e12,e13)) != op2(e22,e23)
| e23 != op2(e22,e21)
| e22 != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e21 != op2(e21,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_832,c_5152]) ).
cnf(c_5154,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| h6(e11) != op2(e22,e23)
| e23 != op2(e22,e21)
| e22 != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e21 != op2(e21,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_4906,c_5153]) ).
cnf(c_5155,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(op1(e13,e10)) != op2(e23,e20)
| e21 != op2(e22,e23)
| e23 != op2(e22,e21)
| e22 != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e21 != op2(e21,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_831,c_5154]) ).
cnf(c_5156,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| h6(e13) != op2(e23,e20)
| e21 != op2(e22,e23)
| e23 != op2(e22,e21)
| e22 != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e21 != op2(e21,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_4900,c_5155]) ).
cnf(c_5157,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| e23 != op2(e23,e20)
| e21 != op2(e22,e23)
| e23 != op2(e22,e21)
| e22 != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e21 != op2(e21,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21) ),
inference(paramod,[status(thm)],[c_832,c_5156]) ).
cnf(c_5158,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| e23 != op2(e23,e20)
| e21 != op2(e22,e23)
| e23 != op2(e22,e21)
| e22 != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e21 != op2(e21,e20)
| e23 != op2(e20,e23)
| e22 != op2(e20,e22)
| op2(e20,e21) != e21 ),
inference(copy,[status(thm)],[c_5157]) ).
cnf(c_5159,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| e23 != op2(e23,e20)
| e21 != op2(e22,e23)
| e23 != op2(e22,e21)
| e22 != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e21 != op2(e21,e20)
| e23 != op2(e20,e23)
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(copy,[status(thm)],[c_5158]) ).
cnf(c_5160,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| e23 != op2(e23,e20)
| e21 != op2(e22,e23)
| e23 != op2(e22,e21)
| e22 != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| e21 != op2(e21,e20)
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(copy,[status(thm)],[c_5159]) ).
cnf(c_5161,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| e23 != op2(e23,e20)
| e21 != op2(e22,e23)
| e23 != op2(e22,e21)
| e22 != op2(e22,e20)
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(copy,[status(thm)],[c_5160]) ).
cnf(c_5162,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| e23 != op2(e23,e20)
| e21 != op2(e22,e23)
| e23 != op2(e22,e21)
| op2(e22,e20) != e22
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(copy,[status(thm)],[c_5161]) ).
cnf(c_5163,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| e23 != op2(e23,e20)
| e21 != op2(e22,e23)
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(copy,[status(thm)],[c_5162]) ).
cnf(c_5164,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| e23 != op2(e23,e20)
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(copy,[status(thm)],[c_5163]) ).
cnf(c_4908,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(op1(e11,e12)) != op2(e21,e22)
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(copy,[status(thm)],[c_5164]) ).
cnf(c_5165,plain,
( e11 != e11
| op1(e11,e13) = e13
| op1(e11,e13) = e12 ),
inference(paramod,[status(thm)],[c_4896,c_4555]) ).
cnf(c_5166,plain,
( op1(e11,e13) = e13
| op1(e11,e13) = e12 ),
inference(copy,[status(thm)],[c_5165]) ).
cnf(c_4912,plain,
op1(e11,e13) = e12,
inference(resolve,[status(thm)],[c_4905,c_5166]) ).
cnf(c_5167,plain,
( op1(e13,e12) = e11
| op1(e12,e10) = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_4896,c_4497]) ).
cnf(c_5168,plain,
( op1(e13,e12) = e11
| e12 = e13
| e11 = e13 ),
inference(paramod,[status(thm)],[c_4898,c_5167]) ).
cnf(c_5169,plain,
( op1(e13,e12) = e11
| e12 = e13
| e13 = e11 ),
inference(copy,[status(thm)],[c_5168]) ).
cnf(c_5170,plain,
( op1(e13,e12) = e11
| e13 = e12
| e13 = e11 ),
inference(copy,[status(thm)],[c_5169]) ).
cnf(c_5171,plain,
( op1(e13,e12) = e11
| e13 = e12 ),
inference(resolve,[status(thm)],[c_260,c_5170]) ).
cnf(c_4913,plain,
op1(e13,e12) = e11,
inference(resolve,[status(thm)],[c_261,c_5171]) ).
cnf(c_5172,plain,
( op1(e11,e12) = e13
| op1(e11,e10) = e13
| op1(e12,e13) = e12
| e13 = e12 ),
inference(paramod,[status(thm)],[c_4899,c_4424]) ).
cnf(c_5173,plain,
( op1(e11,e12) = e13
| op1(e11,e10) = e13
| e11 = e12
| e13 = e12 ),
inference(paramod,[status(thm)],[c_4906,c_5172]) ).
cnf(c_5174,plain,
( op1(e11,e12) = e13
| e11 = e13
| e11 = e12
| e13 = e12 ),
inference(paramod,[status(thm)],[c_4896,c_5173]) ).
cnf(c_5175,plain,
( op1(e11,e12) = e13
| e11 = e13
| e12 = e11
| e13 = e12 ),
inference(copy,[status(thm)],[c_5174]) ).
cnf(c_5176,plain,
( op1(e11,e12) = e13
| e13 = e11
| e12 = e11
| e13 = e12 ),
inference(copy,[status(thm)],[c_5175]) ).
cnf(c_5177,plain,
( op1(e11,e12) = e13
| e13 = e11
| e12 = e11 ),
inference(resolve,[status(thm)],[c_261,c_5176]) ).
cnf(c_5178,plain,
( op1(e11,e12) = e13
| e13 = e11 ),
inference(resolve,[status(thm)],[c_259,c_5177]) ).
cnf(c_4914,plain,
op1(e11,e12) = e13,
inference(resolve,[status(thm)],[c_260,c_5178]) ).
cnf(c_5179,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| h6(op1(e11,e13)) != op2(e21,e23)
| h6(e13) != op2(e21,e22)
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(paramod,[status(thm)],[c_4914,c_4908]) ).
cnf(c_5180,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| h6(op1(e11,e13)) != op2(e21,e23)
| e23 != op2(e21,e22)
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(paramod,[status(thm)],[c_832,c_5179]) ).
cnf(c_5181,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| h6(e12) != op2(e21,e23)
| e23 != op2(e21,e22)
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(paramod,[status(thm)],[c_4912,c_5180]) ).
cnf(c_5182,negated_conjecture,
( h6(op1(e13,e12)) != op2(e23,e22)
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| e22 != op2(e21,e23)
| e23 != op2(e21,e22)
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(paramod,[status(thm)],[c_836,c_5181]) ).
cnf(c_5183,negated_conjecture,
( h6(e11) != op2(e23,e22)
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| e22 != op2(e21,e23)
| e23 != op2(e21,e22)
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(paramod,[status(thm)],[c_4913,c_5182]) ).
cnf(c_5184,negated_conjecture,
( e21 != op2(e23,e22)
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| e22 != op2(e21,e23)
| e23 != op2(e21,e22)
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(paramod,[status(thm)],[c_831,c_5183]) ).
cnf(c_5185,negated_conjecture,
( e21 != op2(e23,e22)
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| e22 != op2(e21,e23)
| op2(e21,e22) != e23
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(copy,[status(thm)],[c_5184]) ).
cnf(c_5186,negated_conjecture,
( e21 != op2(e23,e22)
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| op2(e21,e23) != e22
| op2(e21,e22) != e23
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(copy,[status(thm)],[c_5185]) ).
cnf(c_4915,negated_conjecture,
( op2(e23,e22) != e21
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| op2(e21,e23) != e22
| op2(e21,e22) != e23
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| op2(e20,e21) != e21 ),
inference(copy,[status(thm)],[c_5186]) ).
cnf(c_5187,plain,
( op2(e22,e20) = e20
| unit2 = e23
| unit2 = e20 ),
inference(paramod,[status(thm)],[c_4321,c_102]) ).
cnf(c_4916,plain,
( unit2 = e23
| unit2 = e20 ),
inference(resolve,[status(thm)],[c_4280,c_5187]) ).
cnf(c_5188,plain,
( op2(e23,e20) = e20
| unit2 = e20 ),
inference(paramod,[status(thm)],[c_4916,c_102]) ).
cnf(c_4924,plain,
unit2 = e20,
inference(resolve,[status(thm)],[c_4271,c_5188]) ).
cnf(c_5189,plain,
( op2(e20,e21) = e21
| unit2 = e23 ),
inference(paramod,[status(thm)],[c_4916,c_104]) ).
cnf(c_5190,plain,
( op2(e20,e21) = e21
| e20 = e23 ),
inference(paramod,[status(thm)],[c_4924,c_5189]) ).
cnf(c_5191,plain,
( op2(e20,e21) = e21
| e23 = e20 ),
inference(copy,[status(thm)],[c_5190]) ).
cnf(c_4925,plain,
op2(e20,e21) = e21,
inference(resolve,[status(thm)],[c_265,c_5191]) ).
cnf(c_5192,plain,
( op2(e21,e20) = e21
| unit2 = e23 ),
inference(paramod,[status(thm)],[c_4916,c_105]) ).
cnf(c_5193,plain,
( op2(e21,e20) = e21
| e20 = e23 ),
inference(paramod,[status(thm)],[c_4924,c_5192]) ).
cnf(c_5194,plain,
( op2(e21,e20) = e21
| e23 = e20 ),
inference(copy,[status(thm)],[c_5193]) ).
cnf(c_4926,plain,
op2(e21,e20) = e21,
inference(resolve,[status(thm)],[c_265,c_5194]) ).
cnf(c_5195,plain,
( op2(e20,e22) = e22
| unit2 = e23 ),
inference(paramod,[status(thm)],[c_4916,c_106]) ).
cnf(c_5196,plain,
( op2(e20,e22) = e22
| e20 = e23 ),
inference(paramod,[status(thm)],[c_4924,c_5195]) ).
cnf(c_5197,plain,
( op2(e20,e22) = e22
| e23 = e20 ),
inference(copy,[status(thm)],[c_5196]) ).
cnf(c_4927,plain,
op2(e20,e22) = e22,
inference(resolve,[status(thm)],[c_265,c_5197]) ).
cnf(c_5198,plain,
( op2(e22,e20) = e22
| unit2 = e23 ),
inference(paramod,[status(thm)],[c_4916,c_107]) ).
cnf(c_5199,plain,
( op2(e22,e20) = e22
| e20 = e23 ),
inference(paramod,[status(thm)],[c_4924,c_5198]) ).
cnf(c_5200,plain,
( op2(e22,e20) = e22
| e23 = e20 ),
inference(copy,[status(thm)],[c_5199]) ).
cnf(c_4928,plain,
op2(e22,e20) = e22,
inference(resolve,[status(thm)],[c_265,c_5200]) ).
cnf(c_5201,plain,
( op2(e20,e23) = e23
| unit2 = e23 ),
inference(paramod,[status(thm)],[c_4916,c_108]) ).
cnf(c_5202,plain,
( op2(e20,e23) = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_4924,c_5201]) ).
cnf(c_5203,plain,
( op2(e20,e23) = e23
| e23 = e20 ),
inference(copy,[status(thm)],[c_5202]) ).
cnf(c_4929,plain,
op2(e20,e23) = e23,
inference(resolve,[status(thm)],[c_265,c_5203]) ).
cnf(c_5204,plain,
( op2(e23,e20) = e23
| unit2 = e23 ),
inference(paramod,[status(thm)],[c_4916,c_109]) ).
cnf(c_5205,plain,
( op2(e23,e20) = e23
| e20 = e23 ),
inference(paramod,[status(thm)],[c_4924,c_5204]) ).
cnf(c_5206,plain,
( op2(e23,e20) = e23
| e23 = e20 ),
inference(copy,[status(thm)],[c_5205]) ).
cnf(c_4930,plain,
op2(e23,e20) = e23,
inference(resolve,[status(thm)],[c_265,c_5206]) ).
cnf(c_5207,negated_conjecture,
( op2(e23,e22) != e21
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| op2(e21,e23) != e22
| op2(e21,e22) != e23
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| op2(e20,e22) != e22
| e21 != e21 ),
inference(paramod,[status(thm)],[c_4925,c_4915]) ).
cnf(c_5208,negated_conjecture,
( op2(e23,e22) != e21
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| op2(e21,e23) != e22
| op2(e21,e22) != e23
| op2(e21,e20) != e21
| op2(e20,e23) != e23
| e22 != e22
| e21 != e21 ),
inference(paramod,[status(thm)],[c_4927,c_5207]) ).
cnf(c_5209,negated_conjecture,
( op2(e23,e22) != e21
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| op2(e21,e23) != e22
| op2(e21,e22) != e23
| op2(e21,e20) != e21
| e23 != e23
| e22 != e22
| e21 != e21 ),
inference(paramod,[status(thm)],[c_4929,c_5208]) ).
cnf(c_5210,negated_conjecture,
( op2(e23,e22) != e21
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e22,e20) != e22
| op2(e21,e23) != e22
| op2(e21,e22) != e23
| e21 != e21
| e23 != e23
| e22 != e22
| e21 != e21 ),
inference(paramod,[status(thm)],[c_4926,c_5209]) ).
cnf(c_5211,negated_conjecture,
( op2(e23,e22) != e21
| op2(e23,e20) != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| e22 != e22
| op2(e21,e23) != e22
| op2(e21,e22) != e23
| e21 != e21
| e23 != e23
| e22 != e22
| e21 != e21 ),
inference(paramod,[status(thm)],[c_4928,c_5210]) ).
cnf(c_5212,negated_conjecture,
( op2(e23,e22) != e21
| e23 != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| e22 != e22
| op2(e21,e23) != e22
| op2(e21,e22) != e23
| e21 != e21
| e23 != e23
| e22 != e22
| e21 != e21 ),
inference(paramod,[status(thm)],[c_4930,c_5211]) ).
cnf(c_5213,negated_conjecture,
( op2(e23,e22) != e21
| e23 != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| e22 != e22
| op2(e21,e23) != e22
| op2(e21,e22) != e23
| e21 != e21
| e23 != e23
| e22 != e22 ),
inference(copy,[status(thm)],[c_5212]) ).
cnf(c_5214,negated_conjecture,
( op2(e23,e22) != e21
| e23 != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| e22 != e22
| op2(e21,e23) != e22
| op2(e21,e22) != e23
| e21 != e21
| e23 != e23 ),
inference(copy,[status(thm)],[c_5213]) ).
cnf(c_5215,negated_conjecture,
( op2(e23,e22) != e21
| e23 != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| e22 != e22
| op2(e21,e23) != e22
| op2(e21,e22) != e23
| e21 != e21 ),
inference(copy,[status(thm)],[c_5214]) ).
cnf(c_5216,negated_conjecture,
( op2(e23,e22) != e21
| e23 != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| e22 != e22
| op2(e21,e23) != e22
| op2(e21,e22) != e23 ),
inference(copy,[status(thm)],[c_5215]) ).
cnf(c_5217,negated_conjecture,
( op2(e23,e22) != e21
| e23 != e23
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e21,e23) != e22
| op2(e21,e22) != e23 ),
inference(copy,[status(thm)],[c_5216]) ).
cnf(c_4931,negated_conjecture,
( op2(e23,e22) != e21
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e21,e23) != e22
| op2(e21,e22) != e23 ),
inference(copy,[status(thm)],[c_5217]) ).
cnf(c_5218,plain,
( e21 != e21
| op2(e22,e21) = e23 ),
inference(paramod,[status(thm)],[c_4925,c_4778]) ).
cnf(c_4933,plain,
op2(e22,e21) = e23,
inference(copy,[status(thm)],[c_5218]) ).
cnf(c_5219,plain,
( op2(e21,e23) != e23
| op2(e20,e22) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_4925,c_4698]) ).
cnf(c_5220,plain,
( op2(e21,e23) != e23
| e22 = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_4927,c_5219]) ).
cnf(c_5221,plain,
( op2(e21,e23) != e23
| e22 = e23
| e23 = e21 ),
inference(copy,[status(thm)],[c_5220]) ).
cnf(c_5222,plain,
( op2(e21,e23) != e23
| e23 = e22
| e23 = e21 ),
inference(copy,[status(thm)],[c_5221]) ).
cnf(c_5223,plain,
( op2(e21,e23) != e23
| e23 = e22 ),
inference(resolve,[status(thm)],[c_267,c_5222]) ).
cnf(c_4936,plain,
op2(e21,e23) != e23,
inference(resolve,[status(thm)],[c_268,c_5223]) ).
cnf(c_5224,plain,
( op2(e20,e21) = e23
| op2(e22,e23) = e21
| e22 = e21 ),
inference(paramod,[status(thm)],[c_4928,c_4680]) ).
cnf(c_5225,plain,
( e21 = e23
| op2(e22,e23) = e21
| e22 = e21 ),
inference(paramod,[status(thm)],[c_4925,c_5224]) ).
cnf(c_5226,plain,
( e23 = e21
| op2(e22,e23) = e21
| e22 = e21 ),
inference(copy,[status(thm)],[c_5225]) ).
cnf(c_5227,plain,
( e23 = e21
| op2(e22,e23) = e21 ),
inference(resolve,[status(thm)],[c_266,c_5226]) ).
cnf(c_4937,plain,
op2(e22,e23) = e21,
inference(resolve,[status(thm)],[c_267,c_5227]) ).
cnf(c_5228,plain,
( e21 != e21
| op2(e21,e23) = e23
| op2(e21,e23) = e22 ),
inference(paramod,[status(thm)],[c_4926,c_4750]) ).
cnf(c_5229,plain,
( op2(e21,e23) = e23
| op2(e21,e23) = e22 ),
inference(copy,[status(thm)],[c_5228]) ).
cnf(c_4943,plain,
op2(e21,e23) = e22,
inference(resolve,[status(thm)],[c_4936,c_5229]) ).
cnf(c_5230,plain,
( op2(e23,e22) = e21
| op2(e22,e20) = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_4926,c_4692]) ).
cnf(c_5231,plain,
( op2(e23,e22) = e21
| e22 = e23
| e21 = e23 ),
inference(paramod,[status(thm)],[c_4928,c_5230]) ).
cnf(c_5232,plain,
( op2(e23,e22) = e21
| e22 = e23
| e23 = e21 ),
inference(copy,[status(thm)],[c_5231]) ).
cnf(c_5233,plain,
( op2(e23,e22) = e21
| e23 = e22
| e23 = e21 ),
inference(copy,[status(thm)],[c_5232]) ).
cnf(c_5234,plain,
( op2(e23,e22) = e21
| e23 = e22 ),
inference(resolve,[status(thm)],[c_267,c_5233]) ).
cnf(c_4944,plain,
op2(e23,e22) = e21,
inference(resolve,[status(thm)],[c_268,c_5234]) ).
cnf(c_5235,plain,
( op2(e21,e22) = e23
| op2(e21,e20) = e23
| op2(e22,e23) = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_4929,c_4619]) ).
cnf(c_5236,plain,
( op2(e21,e22) = e23
| op2(e21,e20) = e23
| e21 = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_4937,c_5235]) ).
cnf(c_5237,plain,
( op2(e21,e22) = e23
| e21 = e23
| e21 = e22
| e23 = e22 ),
inference(paramod,[status(thm)],[c_4926,c_5236]) ).
cnf(c_5238,plain,
( op2(e21,e22) = e23
| e21 = e23
| e22 = e21
| e23 = e22 ),
inference(copy,[status(thm)],[c_5237]) ).
cnf(c_5239,plain,
( op2(e21,e22) = e23
| e23 = e21
| e22 = e21
| e23 = e22 ),
inference(copy,[status(thm)],[c_5238]) ).
cnf(c_5240,plain,
( op2(e21,e22) = e23
| e23 = e21
| e22 = e21 ),
inference(resolve,[status(thm)],[c_268,c_5239]) ).
cnf(c_5241,plain,
( op2(e21,e22) = e23
| e23 = e21 ),
inference(resolve,[status(thm)],[c_266,c_5240]) ).
cnf(c_4945,plain,
op2(e21,e22) = e23,
inference(resolve,[status(thm)],[c_267,c_5241]) ).
cnf(c_5242,negated_conjecture,
( op2(e23,e22) != e21
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| op2(e21,e23) != e22
| e23 != e23 ),
inference(paramod,[status(thm)],[c_4945,c_4931]) ).
cnf(c_5243,negated_conjecture,
( op2(e23,e22) != e21
| op2(e22,e23) != e21
| op2(e22,e21) != e23
| e22 != e22
| e23 != e23 ),
inference(paramod,[status(thm)],[c_4943,c_5242]) ).
cnf(c_5244,negated_conjecture,
( op2(e23,e22) != e21
| op2(e22,e23) != e21
| e23 != e23
| e22 != e22
| e23 != e23 ),
inference(paramod,[status(thm)],[c_4933,c_5243]) ).
cnf(c_5245,negated_conjecture,
( op2(e23,e22) != e21
| e21 != e21
| e23 != e23
| e22 != e22
| e23 != e23 ),
inference(paramod,[status(thm)],[c_4937,c_5244]) ).
cnf(c_5246,negated_conjecture,
( e21 != e21
| e21 != e21
| e23 != e23
| e22 != e22
| e23 != e23 ),
inference(paramod,[status(thm)],[c_4944,c_5245]) ).
cnf(c_5247,negated_conjecture,
( e21 != e21
| e21 != e21
| e23 != e23
| e22 != e22 ),
inference(copy,[status(thm)],[c_5246]) ).
cnf(c_5248,negated_conjecture,
( e21 != e21
| e21 != e21
| e23 != e23 ),
inference(copy,[status(thm)],[c_5247]) ).
cnf(c_5249,negated_conjecture,
( e21 != e21
| e21 != e21 ),
inference(copy,[status(thm)],[c_5248]) ).
cnf(c_5250,negated_conjecture,
e21 != e21,
inference(copy,[status(thm)],[c_5249]) ).
cnf(c_4951,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_5250]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG037+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n010.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 21:01:00 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.37 % Process 22643 was started by sandbox2 on n010,
% 0.08/0.37 % Sat Sep 26 21:01:00 2026
% 0.08/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 55.43/55.76
% 55.43/55.76 % From the command line: assign(max_seconds, 300).
% 73.23/58.12
% 73.23/58.12 % SZS status Theorem for theBenchmark
% 73.23/58.12
% 73.23/58.12 % Proof 1 at 0.93 (+ 0.16) seconds.
% 73.23/58.12 % Length of proof is 187.
% 73.23/58.12 % Level of proof is 13.
% 73.23/58.12 % Maximum clause weight is 127.000.
% 73.23/58.12 % Given clauses 255.
% 73.23/58.12
% 73.23/58.12 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------