%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG015+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 : n008.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:07 AM UTC 2026
% Result : Theorem 71.61s 59.51s
% Output : CNFRefutation 71.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 112
% Number of leaves : 14
% Syntax : Number of formulae : 411 ( 214 unt; 0 def)
% Number of atoms : 3127 (3126 equ)
% Maximal formula atoms : 384 ( 7 avg)
% Number of connectives : 4371 (1655 ~;1971 |; 745 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 64 ( 6 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
( ( op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e13,e13) = e10 )
& ( op1(e13,e12) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11
| op1(e13,e12) = e10 )
& ( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e13,e11) = e10 )
& ( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 )
& ( op1(e12,e13) = e13
| op1(e12,e13) = e12
| op1(e12,e13) = e11
| op1(e12,e13) = e10 )
& ( op1(e12,e12) = e13
| op1(e12,e12) = e12
| op1(e12,e12) = e11
| op1(e12,e12) = e10 )
& ( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 )
& ( op1(e12,e10) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 )
& ( op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11
| op1(e11,e13) = e10 )
& ( op1(e11,e12) = e13
| op1(e11,e12) = e12
| op1(e11,e12) = e11
| op1(e11,e12) = e10 )
& ( op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e11) = e10 )
& ( op1(e11,e10) = e13
| op1(e11,e10) = e12
| op1(e11,e10) = e11
| op1(e11,e10) = e10 )
& ( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 )
& ( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 )
& ( op1(e10,e11) = e13
| op1(e10,e11) = e12
| op1(e10,e11) = e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e11
| op1(e10,e10) = e10 ) ),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
( op1(op1(e13,e13),e13) = op1(e13,op1(e13,e13))
& op1(op1(e13,e13),e12) = op1(e13,op1(e13,e12))
& op1(op1(e13,e13),e11) = op1(e13,op1(e13,e11))
& op1(op1(e13,e13),e10) = op1(e13,op1(e13,e10))
& op1(op1(e13,e12),e13) = op1(e13,op1(e12,e13))
& op1(op1(e13,e12),e12) = op1(e13,op1(e12,e12))
& op1(op1(e13,e12),e11) = op1(e13,op1(e12,e11))
& op1(op1(e13,e12),e10) = op1(e13,op1(e12,e10))
& op1(op1(e13,e11),e13) = op1(e13,op1(e11,e13))
& op1(op1(e13,e11),e12) = op1(e13,op1(e11,e12))
& op1(op1(e13,e11),e11) = op1(e13,op1(e11,e11))
& op1(op1(e13,e11),e10) = op1(e13,op1(e11,e10))
& op1(op1(e13,e10),e13) = op1(e13,op1(e10,e13))
& op1(op1(e13,e10),e12) = op1(e13,op1(e10,e12))
& op1(op1(e13,e10),e11) = op1(e13,op1(e10,e11))
& op1(op1(e13,e10),e10) = op1(e13,op1(e10,e10))
& op1(op1(e12,e13),e13) = op1(e12,op1(e13,e13))
& op1(op1(e12,e13),e12) = op1(e12,op1(e13,e12))
& op1(op1(e12,e13),e11) = op1(e12,op1(e13,e11))
& op1(op1(e12,e13),e10) = op1(e12,op1(e13,e10))
& op1(op1(e12,e12),e13) = op1(e12,op1(e12,e13))
& op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12))
& op1(op1(e12,e12),e11) = op1(e12,op1(e12,e11))
& op1(op1(e12,e12),e10) = op1(e12,op1(e12,e10))
& op1(op1(e12,e11),e13) = op1(e12,op1(e11,e13))
& op1(op1(e12,e11),e12) = op1(e12,op1(e11,e12))
& op1(op1(e12,e11),e11) = op1(e12,op1(e11,e11))
& op1(op1(e12,e11),e10) = op1(e12,op1(e11,e10))
& op1(op1(e12,e10),e13) = op1(e12,op1(e10,e13))
& op1(op1(e12,e10),e12) = op1(e12,op1(e10,e12))
& op1(op1(e12,e10),e11) = op1(e12,op1(e10,e11))
& op1(op1(e12,e10),e10) = op1(e12,op1(e10,e10))
& op1(op1(e11,e13),e13) = op1(e11,op1(e13,e13))
& op1(op1(e11,e13),e12) = op1(e11,op1(e13,e12))
& op1(op1(e11,e13),e11) = op1(e11,op1(e13,e11))
& op1(op1(e11,e13),e10) = op1(e11,op1(e13,e10))
& op1(op1(e11,e12),e13) = op1(e11,op1(e12,e13))
& op1(op1(e11,e12),e12) = op1(e11,op1(e12,e12))
& op1(op1(e11,e12),e11) = op1(e11,op1(e12,e11))
& op1(op1(e11,e12),e10) = op1(e11,op1(e12,e10))
& op1(op1(e11,e11),e13) = op1(e11,op1(e11,e13))
& op1(op1(e11,e11),e12) = op1(e11,op1(e11,e12))
& op1(op1(e11,e11),e11) = op1(e11,op1(e11,e11))
& op1(op1(e11,e11),e10) = op1(e11,op1(e11,e10))
& op1(op1(e11,e10),e13) = op1(e11,op1(e10,e13))
& op1(op1(e11,e10),e12) = op1(e11,op1(e10,e12))
& op1(op1(e11,e10),e11) = op1(e11,op1(e10,e11))
& op1(op1(e11,e10),e10) = op1(e11,op1(e10,e10))
& op1(op1(e10,e13),e13) = op1(e10,op1(e13,e13))
& op1(op1(e10,e13),e12) = op1(e10,op1(e13,e12))
& op1(op1(e10,e13),e11) = op1(e10,op1(e13,e11))
& op1(op1(e10,e13),e10) = op1(e10,op1(e13,e10))
& op1(op1(e10,e12),e13) = op1(e10,op1(e12,e13))
& op1(op1(e10,e12),e12) = op1(e10,op1(e12,e12))
& op1(op1(e10,e12),e11) = op1(e10,op1(e12,e11))
& op1(op1(e10,e12),e10) = op1(e10,op1(e12,e10))
& op1(op1(e10,e11),e13) = op1(e10,op1(e11,e13))
& op1(op1(e10,e11),e12) = op1(e10,op1(e11,e12))
& op1(op1(e10,e11),e11) = op1(e10,op1(e11,e11))
& op1(op1(e10,e11),e10) = op1(e10,op1(e11,e10))
& op1(op1(e10,e10),e13) = op1(e10,op1(e10,e13))
& op1(op1(e10,e10),e12) = op1(e10,op1(e10,e12))
& op1(op1(e10,e10),e11) = op1(e10,op1(e10,e11))
& op1(op1(e10,e10),e10) = op1(e10,op1(e10,e10)) ),
file('theBenchmark.p',ax2) ).
fof(ax5,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',ax5) ).
fof(ax6,axiom,
( op2(op2(e23,e23),e23) = op2(e23,op2(e23,e23))
& op2(op2(e23,e23),e22) = op2(e23,op2(e23,e22))
& op2(op2(e23,e23),e21) = op2(e23,op2(e23,e21))
& op2(op2(e23,e23),e20) = op2(e23,op2(e23,e20))
& op2(op2(e23,e22),e23) = op2(e23,op2(e22,e23))
& op2(op2(e23,e22),e22) = op2(e23,op2(e22,e22))
& op2(op2(e23,e22),e21) = op2(e23,op2(e22,e21))
& op2(op2(e23,e22),e20) = op2(e23,op2(e22,e20))
& op2(op2(e23,e21),e23) = op2(e23,op2(e21,e23))
& op2(op2(e23,e21),e22) = op2(e23,op2(e21,e22))
& op2(op2(e23,e21),e21) = op2(e23,op2(e21,e21))
& op2(op2(e23,e21),e20) = op2(e23,op2(e21,e20))
& op2(op2(e23,e20),e23) = op2(e23,op2(e20,e23))
& op2(op2(e23,e20),e22) = op2(e23,op2(e20,e22))
& op2(op2(e23,e20),e21) = op2(e23,op2(e20,e21))
& op2(op2(e23,e20),e20) = op2(e23,op2(e20,e20))
& op2(op2(e22,e23),e23) = op2(e22,op2(e23,e23))
& op2(op2(e22,e23),e22) = op2(e22,op2(e23,e22))
& op2(op2(e22,e23),e21) = op2(e22,op2(e23,e21))
& op2(op2(e22,e23),e20) = op2(e22,op2(e23,e20))
& op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23))
& op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22))
& op2(op2(e22,e22),e21) = op2(e22,op2(e22,e21))
& op2(op2(e22,e22),e20) = op2(e22,op2(e22,e20))
& op2(op2(e22,e21),e23) = op2(e22,op2(e21,e23))
& op2(op2(e22,e21),e22) = op2(e22,op2(e21,e22))
& op2(op2(e22,e21),e21) = op2(e22,op2(e21,e21))
& op2(op2(e22,e21),e20) = op2(e22,op2(e21,e20))
& op2(op2(e22,e20),e23) = op2(e22,op2(e20,e23))
& op2(op2(e22,e20),e22) = op2(e22,op2(e20,e22))
& op2(op2(e22,e20),e21) = op2(e22,op2(e20,e21))
& op2(op2(e22,e20),e20) = op2(e22,op2(e20,e20))
& op2(op2(e21,e23),e23) = op2(e21,op2(e23,e23))
& op2(op2(e21,e23),e22) = op2(e21,op2(e23,e22))
& op2(op2(e21,e23),e21) = op2(e21,op2(e23,e21))
& op2(op2(e21,e23),e20) = op2(e21,op2(e23,e20))
& op2(op2(e21,e22),e23) = op2(e21,op2(e22,e23))
& op2(op2(e21,e22),e22) = op2(e21,op2(e22,e22))
& op2(op2(e21,e22),e21) = op2(e21,op2(e22,e21))
& op2(op2(e21,e22),e20) = op2(e21,op2(e22,e20))
& op2(op2(e21,e21),e23) = op2(e21,op2(e21,e23))
& op2(op2(e21,e21),e22) = op2(e21,op2(e21,e22))
& op2(op2(e21,e21),e21) = op2(e21,op2(e21,e21))
& op2(op2(e21,e21),e20) = op2(e21,op2(e21,e20))
& op2(op2(e21,e20),e23) = op2(e21,op2(e20,e23))
& op2(op2(e21,e20),e22) = op2(e21,op2(e20,e22))
& op2(op2(e21,e20),e21) = op2(e21,op2(e20,e21))
& op2(op2(e21,e20),e20) = op2(e21,op2(e20,e20))
& op2(op2(e20,e23),e23) = op2(e20,op2(e23,e23))
& op2(op2(e20,e23),e22) = op2(e20,op2(e23,e22))
& op2(op2(e20,e23),e21) = op2(e20,op2(e23,e21))
& op2(op2(e20,e23),e20) = op2(e20,op2(e23,e20))
& op2(op2(e20,e22),e23) = op2(e20,op2(e22,e23))
& op2(op2(e20,e22),e22) = op2(e20,op2(e22,e22))
& op2(op2(e20,e22),e21) = op2(e20,op2(e22,e21))
& op2(op2(e20,e22),e20) = op2(e20,op2(e22,e20))
& op2(op2(e20,e21),e23) = op2(e20,op2(e21,e23))
& op2(op2(e20,e21),e22) = op2(e20,op2(e21,e22))
& op2(op2(e20,e21),e21) = op2(e20,op2(e21,e21))
& op2(op2(e20,e21),e20) = op2(e20,op2(e21,e20))
& op2(op2(e20,e20),e23) = op2(e20,op2(e20,e23))
& op2(op2(e20,e20),e22) = op2(e20,op2(e20,e22))
& op2(op2(e20,e20),e21) = op2(e20,op2(e20,e21))
& op2(op2(e20,e20),e20) = op2(e20,op2(e20,e20)) ),
file('theBenchmark.p',ax6) ).
fof(ax17,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',ax17) ).
fof(ax18,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',ax18) ).
fof(ax19,axiom,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('theBenchmark.p',ax19) ).
fof(ax20,axiom,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('theBenchmark.p',ax20) ).
fof(ax22,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',ax22) ).
fof(ax23,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',ax23) ).
fof(ax24,axiom,
( e11 = op1(e12,e13)
& e10 = op1(e13,e13) ),
file('theBenchmark.p',ax24) ).
fof(ax25,axiom,
( e21 = op2(e22,e23)
& e20 = op2(e23,e23) ),
file('theBenchmark.p',ax25) ).
fof(ax34,axiom,
( h9(e11) = op2(e22,e23)
& h9(e10) = op2(e23,e23)
& h9(e13) = e23
& h9(e12) = e22 ),
file('theBenchmark.p',ax34) ).
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_44,plain,
( op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11
| op1(e11,e13) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_49,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_71,plain,
op1(op1(e11,e10),e12) = op1(e11,op1(e10,e12)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_76,plain,
op1(op1(e11,e11),e13) = op1(e11,op1(e11,e13)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_90,plain,
op1(op1(e12,e11),e11) = op1(e12,op1(e11,e11)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_94,plain,
op1(op1(e12,e12),e11) = op1(e12,op1(e12,e11)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_95,plain,
op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_96,plain,
op1(op1(e12,e12),e13) = op1(e12,op1(e12,e13)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_97,plain,
op1(op1(e12,e13),e10) = op1(e12,op1(e13,e10)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_100,plain,
op1(op1(e12,e13),e13) = op1(e12,op1(e13,e13)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_102,plain,
op1(op1(e13,e10),e11) = op1(e13,op1(e10,e11)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_103,plain,
op1(op1(e13,e10),e12) = op1(e13,op1(e10,e12)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_113,plain,
op1(op1(e13,e13),e10) = op1(e13,op1(e13,e10)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_114,plain,
op1(op1(e13,e13),e11) = op1(e13,op1(e13,e11)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_115,plain,
op1(op1(e13,e13),e12) = op1(e13,op1(e13,e12)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_116,plain,
op1(op1(e13,e13),e13) = op1(e13,op1(e13,e13)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_145,plain,
( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| op2(e21,e23) = e20 ),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_150,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 ),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_172,plain,
op2(op2(e21,e20),e22) = op2(e21,op2(e20,e22)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_177,plain,
op2(op2(e21,e21),e23) = op2(e21,op2(e21,e23)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_191,plain,
op2(op2(e22,e21),e21) = op2(e22,op2(e21,e21)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_195,plain,
op2(op2(e22,e22),e21) = op2(e22,op2(e22,e21)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_196,plain,
op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_197,plain,
op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_198,plain,
op2(op2(e22,e23),e20) = op2(e22,op2(e23,e20)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_201,plain,
op2(op2(e22,e23),e23) = op2(e22,op2(e23,e23)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_203,plain,
op2(op2(e23,e20),e21) = op2(e23,op2(e20,e21)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_204,plain,
op2(op2(e23,e20),e22) = op2(e23,op2(e20,e22)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_214,plain,
op2(op2(e23,e23),e20) = op2(e23,op2(e23,e20)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_215,plain,
op2(op2(e23,e23),e21) = op2(e23,op2(e23,e21)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_216,plain,
op2(op2(e23,e23),e22) = op2(e23,op2(e23,e22)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_217,plain,
op2(op2(e23,e23),e23) = op2(e23,op2(e23,e23)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_310,plain,
op1(e12,e12) != op1(e10,e12),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_319,plain,
op1(e12,e13) != op1(e10,e13),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_334,plain,
op1(e10,e13) != op1(e10,e12),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_335,plain,
op1(e10,e12) != op1(e10,e13),
inference(copy,[status(thm)],[c_334]) ).
cnf(c_347,plain,
op1(e12,e13) != op1(e12,e10),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_348,plain,
op1(e12,e10) != op1(e12,e13),
inference(copy,[status(thm)],[c_347]) ).
cnf(c_356,plain,
op1(e13,e13) != op1(e13,e10),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_357,plain,
op1(e13,e10) != op1(e13,e13),
inference(copy,[status(thm)],[c_356]) ).
cnf(c_361,plain,
op1(e13,e13) != op1(e13,e12),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_362,plain,
op1(e13,e12) != op1(e13,e13),
inference(copy,[status(thm)],[c_361]) ).
cnf(c_382,plain,
op2(e22,e22) != op2(e20,e22),
inference(clausify,[status(thm)],[ax18]) ).
cnf(c_391,plain,
op2(e22,e23) != op2(e20,e23),
inference(clausify,[status(thm)],[ax18]) ).
cnf(c_406,plain,
op2(e20,e23) != op2(e20,e22),
inference(clausify,[status(thm)],[ax18]) ).
cnf(c_407,plain,
op2(e20,e22) != op2(e20,e23),
inference(copy,[status(thm)],[c_406]) ).
cnf(c_419,plain,
op2(e22,e23) != op2(e22,e20),
inference(clausify,[status(thm)],[ax18]) ).
cnf(c_420,plain,
op2(e22,e20) != op2(e22,e23),
inference(copy,[status(thm)],[c_419]) ).
cnf(c_428,plain,
op2(e23,e23) != op2(e23,e20),
inference(clausify,[status(thm)],[ax18]) ).
cnf(c_429,plain,
op2(e23,e20) != op2(e23,e23),
inference(copy,[status(thm)],[c_428]) ).
cnf(c_433,plain,
op2(e23,e23) != op2(e23,e22),
inference(clausify,[status(thm)],[ax18]) ).
cnf(c_434,plain,
op2(e23,e22) != op2(e23,e23),
inference(copy,[status(thm)],[c_433]) ).
cnf(c_435,plain,
e11 != e10,
inference(clausify,[status(thm)],[ax19]) ).
cnf(c_436,plain,
e12 != e10,
inference(clausify,[status(thm)],[ax19]) ).
cnf(c_437,plain,
e13 != e10,
inference(clausify,[status(thm)],[ax19]) ).
cnf(c_438,plain,
e10 != e13,
inference(copy,[status(thm)],[c_437]) ).
cnf(c_444,plain,
e21 != e20,
inference(clausify,[status(thm)],[ax20]) ).
cnf(c_445,plain,
e22 != e20,
inference(clausify,[status(thm)],[ax20]) ).
cnf(c_446,plain,
e23 != e20,
inference(clausify,[status(thm)],[ax20]) ).
cnf(c_447,plain,
e20 != e23,
inference(copy,[status(thm)],[c_446]) ).
cnf(c_547,plain,
( op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e10,e10) = e10 ),
inference(clausify,[status(thm)],[ax22]) ).
cnf(c_610,plain,
( op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e11,e11) = e10 ),
inference(clausify,[status(thm)],[ax22]) ).
cnf(c_673,plain,
( op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e12,e12) = e10 ),
inference(clausify,[status(thm)],[ax22]) ).
cnf(c_799,plain,
( op2(e23,e23) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e20,e20) = e20 ),
inference(clausify,[status(thm)],[ax23]) ).
cnf(c_862,plain,
( op2(e23,e23) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e21,e21) = e20 ),
inference(clausify,[status(thm)],[ax23]) ).
cnf(c_925,plain,
( op2(e23,e23) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e22,e22) = e20 ),
inference(clausify,[status(thm)],[ax23]) ).
cnf(c_989,plain,
op1(e13,e13) = e10,
inference(clausify,[status(thm)],[ax24]) ).
cnf(c_990,plain,
op1(e12,e13) = e11,
inference(clausify,[status(thm)],[ax24]) ).
cnf(c_991,plain,
op2(e23,e23) = e20,
inference(clausify,[status(thm)],[ax25]) ).
cnf(c_992,plain,
op2(e22,e23) = e21,
inference(clausify,[status(thm)],[ax25]) ).
cnf(c_1027,plain,
h9(e12) = e22,
inference(clausify,[status(thm)],[ax34]) ).
cnf(c_1028,plain,
h9(e13) = e23,
inference(clausify,[status(thm)],[ax34]) ).
cnf(c_1029,plain,
h9(e10) = op2(e23,e23),
inference(clausify,[status(thm)],[ax34]) ).
cnf(c_1030,plain,
h9(e10) = e20,
inference(paramod,[status(thm)],[c_991,c_1029]) ).
cnf(c_1031,plain,
h9(e11) = op2(e22,e23),
inference(clausify,[status(thm)],[ax34]) ).
cnf(c_1032,plain,
h9(e11) = e21,
inference(paramod,[status(thm)],[c_992,c_1031]) ).
cnf(c_3342,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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)) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_4761,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e20,h9(e10)) ),
inference(paramod,[status(thm)],[c_1030,c_3342]) ).
cnf(c_4762,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e20,e20) ),
inference(paramod,[status(thm)],[c_1030,c_4761]) ).
cnf(c_4763,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e20,h9(e11))
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1030,c_4762]) ).
cnf(c_4764,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1032,c_4763]) ).
cnf(c_4765,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e20,h9(e12))
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1030,c_4764]) ).
cnf(c_4766,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1027,c_4765]) ).
cnf(c_4767,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e20,h9(e13))
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1030,c_4766]) ).
cnf(c_4768,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1028,c_4767]) ).
cnf(c_4769,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e21,h9(e10))
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1032,c_4768]) ).
cnf(c_4770,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1030,c_4769]) ).
cnf(c_4771,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e21,h9(e11))
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1032,c_4770]) ).
cnf(c_4772,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1032,c_4771]) ).
cnf(c_4773,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e21,h9(e12))
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1032,c_4772]) ).
cnf(c_4774,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1027,c_4773]) ).
cnf(c_4775,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e21,h9(e13))
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1032,c_4774]) ).
cnf(c_4776,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1028,c_4775]) ).
cnf(c_4777,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e22,h9(e10))
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1027,c_4776]) ).
cnf(c_4778,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1030,c_4777]) ).
cnf(c_4779,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e22,h9(e11))
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1027,c_4778]) ).
cnf(c_4780,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1032,c_4779]) ).
cnf(c_4781,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e22,h9(e12))
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1027,c_4780]) ).
cnf(c_4782,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1027,c_4781]) ).
cnf(c_4783,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e11) != op2(h9(e12),h9(e13))
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_990,c_4782]) ).
cnf(c_4784,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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))
| e21 != op2(h9(e12),h9(e13))
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1032,c_4783]) ).
cnf(c_4785,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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))
| e21 != op2(e22,h9(e13))
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1027,c_4784]) ).
cnf(c_4786,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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))
| e21 != op2(e22,e23)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1028,c_4785]) ).
cnf(c_4787,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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))
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_992,c_4786]) ).
cnf(c_4788,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e23,h9(e10))
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1028,c_4787]) ).
cnf(c_4789,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1030,c_4788]) ).
cnf(c_4790,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e23,h9(e11))
| h9(op1(e13,e10)) != op2(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1028,c_4789]) ).
cnf(c_4791,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| 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(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1032,c_4790]) ).
cnf(c_4792,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| h9(e10) != e20
| h9(op1(e13,e13)) != op2(h9(e13),h9(e13))
| h9(op1(e13,e12)) != op2(e23,h9(e12))
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1028,c_4791]) ).
cnf(c_4793,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| h9(e10) != e20
| h9(op1(e13,e13)) != op2(h9(e13),h9(e13))
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1027,c_4792]) ).
cnf(c_4794,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| h9(e10) != e20
| h9(e10) != op2(h9(e13),h9(e13))
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_989,c_4793]) ).
cnf(c_4795,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| h9(e10) != e20
| e20 != op2(h9(e13),h9(e13))
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1030,c_4794]) ).
cnf(c_4796,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| h9(e10) != e20
| e20 != op2(e23,h9(e13))
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1028,c_4795]) ).
cnf(c_4797,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| h9(e10) != e20
| e20 != op2(e23,e23)
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1028,c_4796]) ).
cnf(c_4798,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| h9(e10) != e20
| e20 != e20
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_991,c_4797]) ).
cnf(c_4799,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| h9(e11) != e21
| e20 != e20
| e20 != e20
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1030,c_4798]) ).
cnf(c_4800,negated_conjecture,
( h9(e13) != e23
| h9(e12) != e22
| e21 != e21
| e20 != e20
| e20 != e20
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1032,c_4799]) ).
cnf(c_4801,negated_conjecture,
( h9(e13) != e23
| e22 != e22
| e21 != e21
| e20 != e20
| e20 != e20
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1027,c_4800]) ).
cnf(c_4802,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20
| e20 != e20
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e21 != e21
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1028,c_4801]) ).
cnf(c_4803,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20
| e20 != e20
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_4802]) ).
cnf(c_4804,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| e20 != e20
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_4803]) ).
cnf(c_4805,negated_conjecture,
( e23 != e23
| e22 != e22
| e21 != e21
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_4804]) ).
cnf(c_4806,negated_conjecture,
( e23 != e23
| e22 != e22
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_4805]) ).
cnf(c_4807,negated_conjecture,
( e23 != e23
| h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_4806]) ).
cnf(c_3343,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(op1(e10,e10)) != op2(e20,e20) ),
inference(copy,[status(thm)],[c_4807]) ).
cnf(c_4808,plain,
( op1(e13,e13) = e13
| op1(e13,e13) = e12
| e10 = e11
| op1(e12,e12) = e10 ),
inference(paramod,[status(thm)],[c_989,c_673]) ).
cnf(c_4809,plain,
( op1(e13,e13) = e13
| e10 = e12
| e10 = e11
| op1(e12,e12) = e10 ),
inference(paramod,[status(thm)],[c_989,c_4808]) ).
cnf(c_4810,plain,
( e10 = e13
| e10 = e12
| e10 = e11
| op1(e12,e12) = e10 ),
inference(paramod,[status(thm)],[c_989,c_4809]) ).
cnf(c_4811,plain,
( e10 = e13
| e10 = e12
| e11 = e10
| op1(e12,e12) = e10 ),
inference(copy,[status(thm)],[c_4810]) ).
cnf(c_4812,plain,
( e10 = e13
| e12 = e10
| e11 = e10
| op1(e12,e12) = e10 ),
inference(copy,[status(thm)],[c_4811]) ).
cnf(c_4813,plain,
( e10 = e13
| e12 = e10
| op1(e12,e12) = e10 ),
inference(resolve,[status(thm)],[c_435,c_4812]) ).
cnf(c_4814,plain,
( e10 = e13
| op1(e12,e12) = e10 ),
inference(resolve,[status(thm)],[c_436,c_4813]) ).
cnf(c_4448,plain,
op1(e12,e12) = e10,
inference(resolve,[status(thm)],[c_438,c_4814]) ).
cnf(c_4815,plain,
( op1(e13,e13) = e13
| op1(e13,e13) = e12
| e10 = e11
| op1(e11,e11) = e10 ),
inference(paramod,[status(thm)],[c_989,c_610]) ).
cnf(c_4816,plain,
( op1(e13,e13) = e13
| e10 = e12
| e10 = e11
| op1(e11,e11) = e10 ),
inference(paramod,[status(thm)],[c_989,c_4815]) ).
cnf(c_4817,plain,
( e10 = e13
| e10 = e12
| e10 = e11
| op1(e11,e11) = e10 ),
inference(paramod,[status(thm)],[c_989,c_4816]) ).
cnf(c_4818,plain,
( e10 = e13
| e10 = e12
| e11 = e10
| op1(e11,e11) = e10 ),
inference(copy,[status(thm)],[c_4817]) ).
cnf(c_4819,plain,
( e10 = e13
| e12 = e10
| e11 = e10
| op1(e11,e11) = e10 ),
inference(copy,[status(thm)],[c_4818]) ).
cnf(c_4820,plain,
( e10 = e13
| e12 = e10
| op1(e11,e11) = e10 ),
inference(resolve,[status(thm)],[c_435,c_4819]) ).
cnf(c_4821,plain,
( e10 = e13
| op1(e11,e11) = e10 ),
inference(resolve,[status(thm)],[c_436,c_4820]) ).
cnf(c_4449,plain,
op1(e11,e11) = e10,
inference(resolve,[status(thm)],[c_438,c_4821]) ).
cnf(c_4822,plain,
( op1(e13,e13) = e13
| op1(e13,e13) = e12
| e10 = e11
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_989,c_547]) ).
cnf(c_4823,plain,
( op1(e13,e13) = e13
| e10 = e12
| e10 = e11
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_989,c_4822]) ).
cnf(c_4824,plain,
( e10 = e13
| e10 = e12
| e10 = e11
| op1(e10,e10) = e10 ),
inference(paramod,[status(thm)],[c_989,c_4823]) ).
cnf(c_4825,plain,
( e10 = e13
| e10 = e12
| e11 = e10
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_4824]) ).
cnf(c_4826,plain,
( e10 = e13
| e12 = e10
| e11 = e10
| op1(e10,e10) = e10 ),
inference(copy,[status(thm)],[c_4825]) ).
cnf(c_4827,plain,
( e10 = e13
| e12 = e10
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_435,c_4826]) ).
cnf(c_4828,plain,
( e10 = e13
| op1(e10,e10) = e10 ),
inference(resolve,[status(thm)],[c_436,c_4827]) ).
cnf(c_4450,plain,
op1(e10,e10) = e10,
inference(resolve,[status(thm)],[c_438,c_4828]) ).
cnf(c_4451,plain,
op1(e13,e12) != e10,
inference(paramod,[status(thm)],[c_989,c_362]) ).
cnf(c_4453,plain,
op1(e13,e10) != e10,
inference(paramod,[status(thm)],[c_989,c_357]) ).
cnf(c_4829,plain,
op1(e10,e13) = op1(e13,op1(e13,e13)),
inference(paramod,[status(thm)],[c_989,c_116]) ).
cnf(c_4456,plain,
op1(e10,e13) = op1(e13,e10),
inference(paramod,[status(thm)],[c_989,c_4829]) ).
cnf(c_4457,plain,
op1(e10,e12) = op1(e13,op1(e13,e12)),
inference(paramod,[status(thm)],[c_989,c_115]) ).
cnf(c_4458,plain,
op1(e10,e11) = op1(e13,op1(e13,e11)),
inference(paramod,[status(thm)],[c_989,c_114]) ).
cnf(c_4830,plain,
op1(e10,e10) = op1(e13,op1(e13,e10)),
inference(paramod,[status(thm)],[c_989,c_113]) ).
cnf(c_4831,plain,
e10 = op1(e13,op1(e13,e10)),
inference(paramod,[status(thm)],[c_4450,c_4830]) ).
cnf(c_4459,plain,
op1(e13,op1(e13,e10)) = e10,
inference(copy,[status(thm)],[c_4831]) ).
cnf(c_4832,plain,
op1(e11,e13) = op1(e12,op1(e13,e13)),
inference(paramod,[status(thm)],[c_990,c_100]) ).
cnf(c_4833,plain,
op1(e11,e13) = op1(e12,e10),
inference(paramod,[status(thm)],[c_989,c_4832]) ).
cnf(c_4460,plain,
op1(e12,e10) = op1(e11,e13),
inference(copy,[status(thm)],[c_4833]) ).
cnf(c_4834,plain,
op1(e11,e13) != op1(e12,e13),
inference(paramod,[status(thm)],[c_4460,c_348]) ).
cnf(c_4463,plain,
op1(e11,e13) != e11,
inference(paramod,[status(thm)],[c_990,c_4834]) ).
cnf(c_4835,plain,
e11 != op1(e10,e13),
inference(paramod,[status(thm)],[c_990,c_319]) ).
cnf(c_4836,plain,
e11 != op1(e13,e10),
inference(paramod,[status(thm)],[c_4456,c_4835]) ).
cnf(c_4464,plain,
op1(e13,e10) != e11,
inference(copy,[status(thm)],[c_4836]) ).
cnf(c_4837,plain,
op1(e11,e10) = op1(e12,op1(e13,e10)),
inference(paramod,[status(thm)],[c_990,c_97]) ).
cnf(c_4468,plain,
op1(e12,op1(e13,e10)) = op1(e11,e10),
inference(copy,[status(thm)],[c_4837]) ).
cnf(c_4838,plain,
op1(e10,e13) = op1(e12,op1(e12,e13)),
inference(paramod,[status(thm)],[c_4448,c_96]) ).
cnf(c_4839,plain,
op1(e13,e10) = op1(e12,op1(e12,e13)),
inference(paramod,[status(thm)],[c_4456,c_4838]) ).
cnf(c_4840,plain,
op1(e13,e10) = op1(e12,e11),
inference(paramod,[status(thm)],[c_990,c_4839]) ).
cnf(c_4469,plain,
op1(e12,e11) = op1(e13,e10),
inference(copy,[status(thm)],[c_4840]) ).
cnf(c_4841,plain,
( op2(e23,e23) = e23
| op2(e23,e23) = e22
| e20 = e21
| op2(e22,e22) = e20 ),
inference(paramod,[status(thm)],[c_991,c_925]) ).
cnf(c_4842,plain,
( op2(e23,e23) = e23
| e20 = e22
| e20 = e21
| op2(e22,e22) = e20 ),
inference(paramod,[status(thm)],[c_991,c_4841]) ).
cnf(c_4843,plain,
( e20 = e23
| e20 = e22
| e20 = e21
| op2(e22,e22) = e20 ),
inference(paramod,[status(thm)],[c_991,c_4842]) ).
cnf(c_4844,plain,
( e20 = e23
| e20 = e22
| e21 = e20
| op2(e22,e22) = e20 ),
inference(copy,[status(thm)],[c_4843]) ).
cnf(c_4845,plain,
( e20 = e23
| e22 = e20
| e21 = e20
| op2(e22,e22) = e20 ),
inference(copy,[status(thm)],[c_4844]) ).
cnf(c_4846,plain,
( e20 = e23
| e22 = e20
| op2(e22,e22) = e20 ),
inference(resolve,[status(thm)],[c_444,c_4845]) ).
cnf(c_4847,plain,
( e20 = e23
| op2(e22,e22) = e20 ),
inference(resolve,[status(thm)],[c_445,c_4846]) ).
cnf(c_4472,plain,
op2(e22,e22) = e20,
inference(resolve,[status(thm)],[c_447,c_4847]) ).
cnf(c_4848,plain,
( op2(e23,e23) = e23
| op2(e23,e23) = e22
| e20 = e21
| op2(e21,e21) = e20 ),
inference(paramod,[status(thm)],[c_991,c_862]) ).
cnf(c_4849,plain,
( op2(e23,e23) = e23
| e20 = e22
| e20 = e21
| op2(e21,e21) = e20 ),
inference(paramod,[status(thm)],[c_991,c_4848]) ).
cnf(c_4850,plain,
( e20 = e23
| e20 = e22
| e20 = e21
| op2(e21,e21) = e20 ),
inference(paramod,[status(thm)],[c_991,c_4849]) ).
cnf(c_4851,plain,
( e20 = e23
| e20 = e22
| e21 = e20
| op2(e21,e21) = e20 ),
inference(copy,[status(thm)],[c_4850]) ).
cnf(c_4852,plain,
( e20 = e23
| e22 = e20
| e21 = e20
| op2(e21,e21) = e20 ),
inference(copy,[status(thm)],[c_4851]) ).
cnf(c_4853,plain,
( e20 = e23
| e22 = e20
| op2(e21,e21) = e20 ),
inference(resolve,[status(thm)],[c_444,c_4852]) ).
cnf(c_4854,plain,
( e20 = e23
| op2(e21,e21) = e20 ),
inference(resolve,[status(thm)],[c_445,c_4853]) ).
cnf(c_4473,plain,
op2(e21,e21) = e20,
inference(resolve,[status(thm)],[c_447,c_4854]) ).
cnf(c_4855,plain,
( op2(e23,e23) = e23
| op2(e23,e23) = e22
| e20 = e21
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_991,c_799]) ).
cnf(c_4856,plain,
( op2(e23,e23) = e23
| e20 = e22
| e20 = e21
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_991,c_4855]) ).
cnf(c_4857,plain,
( e20 = e23
| e20 = e22
| e20 = e21
| op2(e20,e20) = e20 ),
inference(paramod,[status(thm)],[c_991,c_4856]) ).
cnf(c_4858,plain,
( e20 = e23
| e20 = e22
| e21 = e20
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_4857]) ).
cnf(c_4859,plain,
( e20 = e23
| e22 = e20
| e21 = e20
| op2(e20,e20) = e20 ),
inference(copy,[status(thm)],[c_4858]) ).
cnf(c_4860,plain,
( e20 = e23
| e22 = e20
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_444,c_4859]) ).
cnf(c_4861,plain,
( e20 = e23
| op2(e20,e20) = e20 ),
inference(resolve,[status(thm)],[c_445,c_4860]) ).
cnf(c_4474,plain,
op2(e20,e20) = e20,
inference(resolve,[status(thm)],[c_447,c_4861]) ).
cnf(c_4475,plain,
op2(e23,e22) != e20,
inference(paramod,[status(thm)],[c_991,c_434]) ).
cnf(c_4477,plain,
op2(e23,e20) != e20,
inference(paramod,[status(thm)],[c_991,c_429]) ).
cnf(c_4862,plain,
op2(e20,e23) = op2(e23,op2(e23,e23)),
inference(paramod,[status(thm)],[c_991,c_217]) ).
cnf(c_4480,plain,
op2(e20,e23) = op2(e23,e20),
inference(paramod,[status(thm)],[c_991,c_4862]) ).
cnf(c_4481,plain,
op2(e20,e22) = op2(e23,op2(e23,e22)),
inference(paramod,[status(thm)],[c_991,c_216]) ).
cnf(c_4482,plain,
op2(e20,e21) = op2(e23,op2(e23,e21)),
inference(paramod,[status(thm)],[c_991,c_215]) ).
cnf(c_4863,plain,
op2(e20,e20) = op2(e23,op2(e23,e20)),
inference(paramod,[status(thm)],[c_991,c_214]) ).
cnf(c_4864,plain,
e20 = op2(e23,op2(e23,e20)),
inference(paramod,[status(thm)],[c_4474,c_4863]) ).
cnf(c_4483,plain,
op2(e23,op2(e23,e20)) = e20,
inference(copy,[status(thm)],[c_4864]) ).
cnf(c_4865,plain,
op2(e21,e23) = op2(e22,op2(e23,e23)),
inference(paramod,[status(thm)],[c_992,c_201]) ).
cnf(c_4866,plain,
op2(e21,e23) = op2(e22,e20),
inference(paramod,[status(thm)],[c_991,c_4865]) ).
cnf(c_4484,plain,
op2(e22,e20) = op2(e21,e23),
inference(copy,[status(thm)],[c_4866]) ).
cnf(c_4867,plain,
op2(e21,e23) != op2(e22,e23),
inference(paramod,[status(thm)],[c_4484,c_420]) ).
cnf(c_4487,plain,
op2(e21,e23) != e21,
inference(paramod,[status(thm)],[c_992,c_4867]) ).
cnf(c_4868,plain,
e21 != op2(e20,e23),
inference(paramod,[status(thm)],[c_992,c_391]) ).
cnf(c_4869,plain,
e21 != op2(e23,e20),
inference(paramod,[status(thm)],[c_4480,c_4868]) ).
cnf(c_4488,plain,
op2(e23,e20) != e21,
inference(copy,[status(thm)],[c_4869]) ).
cnf(c_4870,plain,
op2(e21,e20) = op2(e22,op2(e23,e20)),
inference(paramod,[status(thm)],[c_992,c_198]) ).
cnf(c_4492,plain,
op2(e22,op2(e23,e20)) = op2(e21,e20),
inference(copy,[status(thm)],[c_4870]) ).
cnf(c_4871,plain,
op2(e20,e23) = op2(e22,op2(e22,e23)),
inference(paramod,[status(thm)],[c_4472,c_197]) ).
cnf(c_4872,plain,
op2(e23,e20) = op2(e22,op2(e22,e23)),
inference(paramod,[status(thm)],[c_4480,c_4871]) ).
cnf(c_4873,plain,
op2(e23,e20) = op2(e22,e21),
inference(paramod,[status(thm)],[c_992,c_4872]) ).
cnf(c_4493,plain,
op2(e22,e21) = op2(e23,e20),
inference(copy,[status(thm)],[c_4873]) ).
cnf(c_4874,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| h9(e10) != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_4450,c_3343]) ).
cnf(c_4875,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| e20 != op2(e20,e20) ),
inference(paramod,[status(thm)],[c_1030,c_4874]) ).
cnf(c_4876,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e10,e11)) != op2(e20,e21)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4474,c_4875]) ).
cnf(c_4877,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e13,op1(e13,e11))) != op2(e20,e21)
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4458,c_4876]) ).
cnf(c_4878,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e10,e12)) != op2(e20,e22)
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4482,c_4877]) ).
cnf(c_4879,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e13,op1(e13,e12))) != op2(e20,e22)
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4457,c_4878]) ).
cnf(c_4880,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e10,e13)) != op2(e20,e23)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4481,c_4879]) ).
cnf(c_4881,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e20,e23)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4456,c_4880]) ).
cnf(c_4882,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e11)) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4480,c_4881]) ).
cnf(c_4883,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(e10) != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4449,c_4882]) ).
cnf(c_4884,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| e20 != op2(e21,e21)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_1030,c_4883]) ).
cnf(c_4885,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e12,e10)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4473,c_4884]) ).
cnf(c_4886,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e11,e13)) != op2(e22,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4460,c_4885]) ).
cnf(c_4887,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e12,e11)) != op2(e22,e21)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4484,c_4886]) ).
cnf(c_4888,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e13,e10)) != op2(e22,e21)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4469,c_4887]) ).
cnf(c_4889,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e12,e12)) != op2(e22,e22)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4493,c_4888]) ).
cnf(c_4890,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(e10) != op2(e22,e22)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4448,c_4889]) ).
cnf(c_4891,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e20 != op2(e22,e22)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_1030,c_4890]) ).
cnf(c_4892,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e20 != e20
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| e20 != e20 ),
inference(paramod,[status(thm)],[c_4472,c_4891]) ).
cnf(c_4893,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e20 != e20
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| e20 != e20
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21)) ),
inference(copy,[status(thm)],[c_4892]) ).
cnf(c_4894,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| e20 != e20
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21)) ),
inference(copy,[status(thm)],[c_4893]) ).
cnf(c_4895,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21)) ),
inference(copy,[status(thm)],[c_4894]) ).
cnf(c_4896,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21)) ),
inference(copy,[status(thm)],[c_4895]) ).
cnf(c_4897,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21)) ),
inference(copy,[status(thm)],[c_4896]) ).
cnf(c_4498,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e11,e10)) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21)) ),
inference(copy,[status(thm)],[c_4897]) ).
cnf(c_4898,plain,
e10 != op1(e10,e12),
inference(paramod,[status(thm)],[c_4448,c_310]) ).
cnf(c_4899,plain,
e10 != op1(e13,op1(e13,e12)),
inference(paramod,[status(thm)],[c_4457,c_4898]) ).
cnf(c_4507,plain,
op1(e13,op1(e13,e12)) != e10,
inference(copy,[status(thm)],[c_4899]) ).
cnf(c_4900,plain,
op1(e10,e12) = op1(e12,op1(e12,e12)),
inference(paramod,[status(thm)],[c_4448,c_95]) ).
cnf(c_4901,plain,
op1(e13,op1(e13,e12)) = op1(e12,op1(e12,e12)),
inference(paramod,[status(thm)],[c_4457,c_4900]) ).
cnf(c_4902,plain,
op1(e13,op1(e13,e12)) = op1(e12,e10),
inference(paramod,[status(thm)],[c_4448,c_4901]) ).
cnf(c_4903,plain,
op1(e13,op1(e13,e12)) = op1(e11,e13),
inference(paramod,[status(thm)],[c_4460,c_4902]) ).
cnf(c_4509,plain,
op1(e11,e13) = op1(e13,op1(e13,e12)),
inference(copy,[status(thm)],[c_4903]) ).
cnf(c_4904,plain,
op1(e10,e11) = op1(e12,op1(e12,e11)),
inference(paramod,[status(thm)],[c_4448,c_94]) ).
cnf(c_4905,plain,
op1(e13,op1(e13,e11)) = op1(e12,op1(e12,e11)),
inference(paramod,[status(thm)],[c_4458,c_4904]) ).
cnf(c_4906,plain,
op1(e13,op1(e13,e11)) = op1(e12,op1(e13,e10)),
inference(paramod,[status(thm)],[c_4469,c_4905]) ).
cnf(c_4907,plain,
op1(e13,op1(e13,e11)) = op1(e11,e10),
inference(paramod,[status(thm)],[c_4468,c_4906]) ).
cnf(c_4510,plain,
op1(e11,e10) = op1(e13,op1(e13,e11)),
inference(copy,[status(thm)],[c_4907]) ).
cnf(c_4908,plain,
op1(op1(e13,e10),e11) = op1(e12,op1(e11,e11)),
inference(paramod,[status(thm)],[c_4469,c_90]) ).
cnf(c_4909,plain,
op1(e13,op1(e10,e11)) = op1(e12,op1(e11,e11)),
inference(paramod,[status(thm)],[c_102,c_4908]) ).
cnf(c_4910,plain,
op1(e13,op1(e13,op1(e13,e11))) = op1(e12,op1(e11,e11)),
inference(paramod,[status(thm)],[c_4458,c_4909]) ).
cnf(c_4911,plain,
op1(e13,op1(e13,op1(e13,e11))) = op1(e12,e10),
inference(paramod,[status(thm)],[c_4449,c_4910]) ).
cnf(c_4912,plain,
op1(e13,op1(e13,op1(e13,e11))) = op1(e11,e13),
inference(paramod,[status(thm)],[c_4460,c_4911]) ).
cnf(c_4516,plain,
op1(e13,op1(e13,op1(e13,e11))) = op1(e13,op1(e13,e12)),
inference(paramod,[status(thm)],[c_4509,c_4912]) ).
cnf(c_4913,plain,
op1(e10,e13) = op1(e11,op1(e11,e13)),
inference(paramod,[status(thm)],[c_4449,c_76]) ).
cnf(c_4914,plain,
op1(e13,e10) = op1(e11,op1(e11,e13)),
inference(paramod,[status(thm)],[c_4456,c_4913]) ).
cnf(c_4915,plain,
op1(e13,e10) = op1(e11,op1(e13,op1(e13,e12))),
inference(paramod,[status(thm)],[c_4509,c_4914]) ).
cnf(c_4517,plain,
op1(e11,op1(e13,op1(e13,e12))) = op1(e13,e10),
inference(copy,[status(thm)],[c_4915]) ).
cnf(c_4916,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11 ),
inference(resolve,[status(thm)],[c_4453,c_49]) ).
cnf(c_4529,plain,
( op1(e13,e10) = e13
| op1(e13,e10) = e12 ),
inference(resolve,[status(thm)],[c_4464,c_4916]) ).
cnf(c_4917,plain,
( op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11
| op1(e13,op1(e13,e12)) = e10 ),
inference(paramod,[status(thm)],[c_4509,c_44]) ).
cnf(c_4918,plain,
( op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e13,op1(e13,e12)) = e11
| op1(e13,op1(e13,e12)) = e10 ),
inference(paramod,[status(thm)],[c_4509,c_4917]) ).
cnf(c_4919,plain,
( op1(e11,e13) = e13
| op1(e13,op1(e13,e12)) = e12
| op1(e13,op1(e13,e12)) = e11
| op1(e13,op1(e13,e12)) = e10 ),
inference(paramod,[status(thm)],[c_4509,c_4918]) ).
cnf(c_4920,plain,
( op1(e13,op1(e13,e12)) = e13
| op1(e13,op1(e13,e12)) = e12
| op1(e13,op1(e13,e12)) = e11
| op1(e13,op1(e13,e12)) = e10 ),
inference(paramod,[status(thm)],[c_4509,c_4919]) ).
cnf(c_4530,plain,
( op1(e13,op1(e13,e12)) = e13
| op1(e13,op1(e13,e12)) = e12
| op1(e13,op1(e13,e12)) = e11 ),
inference(resolve,[status(thm)],[c_4507,c_4920]) ).
cnf(c_4921,plain,
op1(e13,op1(e13,e12)) != op1(e10,e13),
inference(paramod,[status(thm)],[c_4457,c_335]) ).
cnf(c_4531,plain,
op1(e13,op1(e13,e12)) != op1(e13,e10),
inference(paramod,[status(thm)],[c_4456,c_4921]) ).
cnf(c_4540,plain,
op1(op1(e13,e10),e12) = op1(e13,op1(e13,op1(e13,e12))),
inference(paramod,[status(thm)],[c_4457,c_103]) ).
cnf(c_4922,plain,
op1(op1(e13,op1(e13,e11)),e12) = op1(e11,op1(e10,e12)),
inference(paramod,[status(thm)],[c_4510,c_71]) ).
cnf(c_4923,plain,
op1(op1(e13,op1(e13,e11)),e12) = op1(e11,op1(e13,op1(e13,e12))),
inference(paramod,[status(thm)],[c_4457,c_4922]) ).
cnf(c_4541,plain,
op1(op1(e13,op1(e13,e11)),e12) = op1(e13,e10),
inference(paramod,[status(thm)],[c_4517,c_4923]) ).
cnf(c_4924,plain,
op1(op1(e13,e10),e11) = op1(e13,op1(e13,op1(e13,e11))),
inference(paramod,[status(thm)],[c_4458,c_102]) ).
cnf(c_4544,plain,
op1(op1(e13,e10),e11) = op1(e13,op1(e13,e12)),
inference(paramod,[status(thm)],[c_4516,c_4924]) ).
cnf(c_4925,plain,
e20 != op2(e20,e22),
inference(paramod,[status(thm)],[c_4472,c_382]) ).
cnf(c_4926,plain,
e20 != op2(e23,op2(e23,e22)),
inference(paramod,[status(thm)],[c_4481,c_4925]) ).
cnf(c_4558,plain,
op2(e23,op2(e23,e22)) != e20,
inference(copy,[status(thm)],[c_4926]) ).
cnf(c_4927,plain,
op2(e20,e22) = op2(e22,op2(e22,e22)),
inference(paramod,[status(thm)],[c_4472,c_196]) ).
cnf(c_4928,plain,
op2(e23,op2(e23,e22)) = op2(e22,op2(e22,e22)),
inference(paramod,[status(thm)],[c_4481,c_4927]) ).
cnf(c_4929,plain,
op2(e23,op2(e23,e22)) = op2(e22,e20),
inference(paramod,[status(thm)],[c_4472,c_4928]) ).
cnf(c_4930,plain,
op2(e23,op2(e23,e22)) = op2(e21,e23),
inference(paramod,[status(thm)],[c_4484,c_4929]) ).
cnf(c_4560,plain,
op2(e21,e23) = op2(e23,op2(e23,e22)),
inference(copy,[status(thm)],[c_4930]) ).
cnf(c_4931,plain,
op2(e20,e21) = op2(e22,op2(e22,e21)),
inference(paramod,[status(thm)],[c_4472,c_195]) ).
cnf(c_4932,plain,
op2(e23,op2(e23,e21)) = op2(e22,op2(e22,e21)),
inference(paramod,[status(thm)],[c_4482,c_4931]) ).
cnf(c_4933,plain,
op2(e23,op2(e23,e21)) = op2(e22,op2(e23,e20)),
inference(paramod,[status(thm)],[c_4493,c_4932]) ).
cnf(c_4934,plain,
op2(e23,op2(e23,e21)) = op2(e21,e20),
inference(paramod,[status(thm)],[c_4492,c_4933]) ).
cnf(c_4561,plain,
op2(e21,e20) = op2(e23,op2(e23,e21)),
inference(copy,[status(thm)],[c_4934]) ).
cnf(c_4935,plain,
op2(op2(e23,e20),e21) = op2(e22,op2(e21,e21)),
inference(paramod,[status(thm)],[c_4493,c_191]) ).
cnf(c_4936,plain,
op2(e23,op2(e20,e21)) = op2(e22,op2(e21,e21)),
inference(paramod,[status(thm)],[c_203,c_4935]) ).
cnf(c_4937,plain,
op2(e23,op2(e23,op2(e23,e21))) = op2(e22,op2(e21,e21)),
inference(paramod,[status(thm)],[c_4482,c_4936]) ).
cnf(c_4938,plain,
op2(e23,op2(e23,op2(e23,e21))) = op2(e22,e20),
inference(paramod,[status(thm)],[c_4473,c_4937]) ).
cnf(c_4939,plain,
op2(e23,op2(e23,op2(e23,e21))) = op2(e21,e23),
inference(paramod,[status(thm)],[c_4484,c_4938]) ).
cnf(c_4570,plain,
op2(e23,op2(e23,op2(e23,e21))) = op2(e23,op2(e23,e22)),
inference(paramod,[status(thm)],[c_4560,c_4939]) ).
cnf(c_4940,plain,
op2(e20,e23) = op2(e21,op2(e21,e23)),
inference(paramod,[status(thm)],[c_4473,c_177]) ).
cnf(c_4941,plain,
op2(e23,e20) = op2(e21,op2(e21,e23)),
inference(paramod,[status(thm)],[c_4480,c_4940]) ).
cnf(c_4942,plain,
op2(e23,e20) = op2(e21,op2(e23,op2(e23,e22))),
inference(paramod,[status(thm)],[c_4560,c_4941]) ).
cnf(c_4571,plain,
op2(e21,op2(e23,op2(e23,e22))) = op2(e23,e20),
inference(copy,[status(thm)],[c_4942]) ).
cnf(c_4943,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21 ),
inference(resolve,[status(thm)],[c_4477,c_150]) ).
cnf(c_4586,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22 ),
inference(resolve,[status(thm)],[c_4488,c_4943]) ).
cnf(c_4944,plain,
( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| op2(e23,op2(e23,e22)) = e20 ),
inference(paramod,[status(thm)],[c_4560,c_145]) ).
cnf(c_4945,plain,
( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e23,op2(e23,e22)) = e21
| op2(e23,op2(e23,e22)) = e20 ),
inference(paramod,[status(thm)],[c_4560,c_4944]) ).
cnf(c_4946,plain,
( op2(e21,e23) = e23
| op2(e23,op2(e23,e22)) = e22
| op2(e23,op2(e23,e22)) = e21
| op2(e23,op2(e23,e22)) = e20 ),
inference(paramod,[status(thm)],[c_4560,c_4945]) ).
cnf(c_4947,plain,
( op2(e23,op2(e23,e22)) = e23
| op2(e23,op2(e23,e22)) = e22
| op2(e23,op2(e23,e22)) = e21
| op2(e23,op2(e23,e22)) = e20 ),
inference(paramod,[status(thm)],[c_4560,c_4946]) ).
cnf(c_4587,plain,
( op2(e23,op2(e23,e22)) = e23
| op2(e23,op2(e23,e22)) = e22
| op2(e23,op2(e23,e22)) = e21 ),
inference(resolve,[status(thm)],[c_4558,c_4947]) ).
cnf(c_4948,plain,
op2(e23,op2(e23,e22)) != op2(e20,e23),
inference(paramod,[status(thm)],[c_4481,c_407]) ).
cnf(c_4589,plain,
op2(e23,op2(e23,e22)) != op2(e23,e20),
inference(paramod,[status(thm)],[c_4480,c_4948]) ).
cnf(c_4599,plain,
op2(op2(e23,e20),e22) = op2(e23,op2(e23,op2(e23,e22))),
inference(paramod,[status(thm)],[c_4481,c_204]) ).
cnf(c_4949,plain,
op2(op2(e23,op2(e23,e21)),e22) = op2(e21,op2(e20,e22)),
inference(paramod,[status(thm)],[c_4561,c_172]) ).
cnf(c_4950,plain,
op2(op2(e23,op2(e23,e21)),e22) = op2(e21,op2(e23,op2(e23,e22))),
inference(paramod,[status(thm)],[c_4481,c_4949]) ).
cnf(c_4600,plain,
op2(op2(e23,op2(e23,e21)),e22) = op2(e23,e20),
inference(paramod,[status(thm)],[c_4571,c_4950]) ).
cnf(c_4951,plain,
op2(op2(e23,e20),e21) = op2(e23,op2(e23,op2(e23,e21))),
inference(paramod,[status(thm)],[c_4482,c_203]) ).
cnf(c_4604,plain,
op2(op2(e23,e20),e21) = op2(e23,op2(e23,e22)),
inference(paramod,[status(thm)],[c_4570,c_4951]) ).
cnf(c_4952,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e13,op1(e13,e11))) != op2(e21,e20)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21)) ),
inference(paramod,[status(thm)],[c_4510,c_4498]) ).
cnf(c_4953,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e11,e13)) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21)) ),
inference(paramod,[status(thm)],[c_4561,c_4952]) ).
cnf(c_4954,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,op1(e13,e12))) != op2(e21,e23)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21)) ),
inference(paramod,[status(thm)],[c_4509,c_4953]) ).
cnf(c_4955,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21))
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21)) ),
inference(paramod,[status(thm)],[c_4560,c_4954]) ).
cnf(c_4956,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21)) ),
inference(copy,[status(thm)],[c_4955]) ).
cnf(c_4623,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(op1(e13,op1(e13,e11))) != op2(e23,op2(e23,e21)) ),
inference(copy,[status(thm)],[c_4956]) ).
cnf(c_4626,plain,
op1(e13,op1(e13,e12)) != e11,
inference(paramod,[status(thm)],[c_4509,c_4463]) ).
cnf(c_4631,plain,
op1(e12,op1(e13,e10)) = op1(e13,op1(e13,e11)),
inference(paramod,[status(thm)],[c_4510,c_4468]) ).
cnf(c_4636,plain,
op2(e23,op2(e23,e22)) != e21,
inference(paramod,[status(thm)],[c_4560,c_4487]) ).
cnf(c_4642,plain,
op2(e22,op2(e23,e20)) = op2(e23,op2(e23,e21)),
inference(paramod,[status(thm)],[c_4561,c_4492]) ).
cnf(c_4647,plain,
( op1(e13,op1(e13,e12)) = e13
| op1(e13,op1(e13,e12)) = e12 ),
inference(resolve,[status(thm)],[c_4626,c_4530]) ).
cnf(c_4648,plain,
( op2(e23,op2(e23,e22)) = e23
| op2(e23,op2(e23,e22)) = e22 ),
inference(resolve,[status(thm)],[c_4636,c_4587]) ).
cnf(c_4957,plain,
( op1(e13,e12) = e10
| op1(e13,e10) = e13 ),
inference(paramod,[status(thm)],[c_4529,c_4459]) ).
cnf(c_4700,plain,
op1(e13,e10) = e13,
inference(resolve,[status(thm)],[c_4451,c_4957]) ).
cnf(c_4958,plain,
op1(e12,e13) = op1(e13,op1(e13,e11)),
inference(paramod,[status(thm)],[c_4700,c_4631]) ).
cnf(c_4959,plain,
e11 = op1(e13,op1(e13,e11)),
inference(paramod,[status(thm)],[c_990,c_4958]) ).
cnf(c_4702,plain,
op1(e13,op1(e13,e11)) = e11,
inference(copy,[status(thm)],[c_4959]) ).
cnf(c_4960,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| h9(e11) != op2(e23,op2(e23,e21)) ),
inference(paramod,[status(thm)],[c_4702,c_4623]) ).
cnf(c_4961,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(op1(e13,e10)) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| e21 != op2(e23,op2(e23,e21)) ),
inference(paramod,[status(thm)],[c_1032,c_4960]) ).
cnf(c_4962,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e11,e12)) != op2(e21,e22)
| h9(e13) != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| e21 != op2(e23,op2(e23,e21)) ),
inference(paramod,[status(thm)],[c_4700,c_4961]) ).
cnf(c_4963,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e11,e12)) != op2(e21,e22)
| e23 != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| e21 != op2(e23,op2(e23,e21)) ),
inference(paramod,[status(thm)],[c_1028,c_4962]) ).
cnf(c_4964,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e11,e12)) != op2(e21,e22)
| e23 != op2(e23,e20)
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| op2(e23,op2(e23,e21)) != e21 ),
inference(copy,[status(thm)],[c_4963]) ).
cnf(c_4704,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e11,e12)) != op2(e21,e22)
| op2(e23,e20) != e23
| h9(op1(e13,op1(e13,e12))) != op2(e23,op2(e23,e22))
| op2(e23,op2(e23,e21)) != e21 ),
inference(copy,[status(thm)],[c_4964]) ).
cnf(c_4965,plain,
op1(e13,e11) = op1(e13,op1(e13,e12)),
inference(paramod,[status(thm)],[c_4700,c_4544]) ).
cnf(c_4707,plain,
op1(e13,op1(e13,e12)) = op1(e13,e11),
inference(copy,[status(thm)],[c_4965]) ).
cnf(c_4966,plain,
op1(e11,e12) = op1(e13,e10),
inference(paramod,[status(thm)],[c_4702,c_4541]) ).
cnf(c_4708,plain,
op1(e11,e12) = e13,
inference(paramod,[status(thm)],[c_4700,c_4966]) ).
cnf(c_4967,plain,
op1(e13,e12) = op1(e13,op1(e13,op1(e13,e12))),
inference(paramod,[status(thm)],[c_4700,c_4540]) ).
cnf(c_4968,plain,
op1(e13,e12) = op1(e13,op1(e13,e11)),
inference(paramod,[status(thm)],[c_4707,c_4967]) ).
cnf(c_4709,plain,
op1(e13,e12) = e11,
inference(paramod,[status(thm)],[c_4702,c_4968]) ).
cnf(c_4969,plain,
op1(e13,e11) != op1(e13,e10),
inference(paramod,[status(thm)],[c_4709,c_4531]) ).
cnf(c_4710,plain,
op1(e13,e11) != e13,
inference(paramod,[status(thm)],[c_4700,c_4969]) ).
cnf(c_4970,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(op1(e11,e12)) != op2(e21,e22)
| op2(e23,e20) != e23
| h9(op1(e13,e11)) != op2(e23,op2(e23,e22))
| op2(e23,op2(e23,e21)) != e21 ),
inference(paramod,[status(thm)],[c_4709,c_4704]) ).
cnf(c_4971,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| h9(e13) != op2(e21,e22)
| op2(e23,e20) != e23
| h9(op1(e13,e11)) != op2(e23,op2(e23,e22))
| op2(e23,op2(e23,e21)) != e21 ),
inference(paramod,[status(thm)],[c_4708,c_4970]) ).
cnf(c_4972,negated_conjecture,
( h9(op1(e13,e12)) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| e23 != op2(e21,e22)
| op2(e23,e20) != e23
| h9(op1(e13,e11)) != op2(e23,op2(e23,e22))
| op2(e23,op2(e23,e21)) != e21 ),
inference(paramod,[status(thm)],[c_1028,c_4971]) ).
cnf(c_4973,negated_conjecture,
( h9(e11) != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| e23 != op2(e21,e22)
| op2(e23,e20) != e23
| h9(op1(e13,e11)) != op2(e23,op2(e23,e22))
| op2(e23,op2(e23,e21)) != e21 ),
inference(paramod,[status(thm)],[c_4709,c_4972]) ).
cnf(c_4974,negated_conjecture,
( e21 != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| e23 != op2(e21,e22)
| op2(e23,e20) != e23
| h9(op1(e13,e11)) != op2(e23,op2(e23,e22))
| op2(e23,op2(e23,e21)) != e21 ),
inference(paramod,[status(thm)],[c_1032,c_4973]) ).
cnf(c_4975,negated_conjecture,
( e21 != op2(e23,e22)
| h9(op1(e13,e11)) != op2(e23,e21)
| op2(e21,e22) != e23
| op2(e23,e20) != e23
| h9(op1(e13,e11)) != op2(e23,op2(e23,e22))
| op2(e23,op2(e23,e21)) != e21 ),
inference(copy,[status(thm)],[c_4974]) ).
cnf(c_4717,negated_conjecture,
( op2(e23,e22) != e21
| h9(op1(e13,e11)) != op2(e23,e21)
| op2(e21,e22) != e23
| op2(e23,e20) != e23
| h9(op1(e13,e11)) != op2(e23,op2(e23,e22))
| op2(e23,op2(e23,e21)) != e21 ),
inference(copy,[status(thm)],[c_4975]) ).
cnf(c_4976,plain,
( op1(e13,op1(e13,e12)) = e13
| op1(e13,e11) = e12 ),
inference(paramod,[status(thm)],[c_4709,c_4647]) ).
cnf(c_4977,plain,
( op1(e13,e11) = e13
| op1(e13,e11) = e12 ),
inference(paramod,[status(thm)],[c_4709,c_4976]) ).
cnf(c_4719,plain,
op1(e13,e11) = e12,
inference(resolve,[status(thm)],[c_4710,c_4977]) ).
cnf(c_4978,negated_conjecture,
( op2(e23,e22) != e21
| h9(op1(e13,e11)) != op2(e23,e21)
| op2(e21,e22) != e23
| op2(e23,e20) != e23
| h9(e12) != op2(e23,op2(e23,e22))
| op2(e23,op2(e23,e21)) != e21 ),
inference(paramod,[status(thm)],[c_4719,c_4717]) ).
cnf(c_4979,negated_conjecture,
( op2(e23,e22) != e21
| h9(op1(e13,e11)) != op2(e23,e21)
| op2(e21,e22) != e23
| op2(e23,e20) != e23
| e22 != op2(e23,op2(e23,e22))
| op2(e23,op2(e23,e21)) != e21 ),
inference(paramod,[status(thm)],[c_1027,c_4978]) ).
cnf(c_4980,negated_conjecture,
( op2(e23,e22) != e21
| h9(e12) != op2(e23,e21)
| op2(e21,e22) != e23
| op2(e23,e20) != e23
| e22 != op2(e23,op2(e23,e22))
| op2(e23,op2(e23,e21)) != e21 ),
inference(paramod,[status(thm)],[c_4719,c_4979]) ).
cnf(c_4981,negated_conjecture,
( op2(e23,e22) != e21
| e22 != op2(e23,e21)
| op2(e21,e22) != e23
| op2(e23,e20) != e23
| e22 != op2(e23,op2(e23,e22))
| op2(e23,op2(e23,e21)) != e21 ),
inference(paramod,[status(thm)],[c_1027,c_4980]) ).
cnf(c_4982,negated_conjecture,
( op2(e23,e22) != e21
| e22 != op2(e23,e21)
| op2(e21,e22) != e23
| op2(e23,e20) != e23
| op2(e23,op2(e23,e22)) != e22
| op2(e23,op2(e23,e21)) != e21 ),
inference(copy,[status(thm)],[c_4981]) ).
cnf(c_4724,negated_conjecture,
( op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e21,e22) != e23
| op2(e23,e20) != e23
| op2(e23,op2(e23,e22)) != e22
| op2(e23,op2(e23,e21)) != e21 ),
inference(copy,[status(thm)],[c_4982]) ).
cnf(c_4983,plain,
( op2(e23,e22) = e20
| op2(e23,e20) = e23 ),
inference(paramod,[status(thm)],[c_4586,c_4483]) ).
cnf(c_4736,plain,
op2(e23,e20) = e23,
inference(resolve,[status(thm)],[c_4475,c_4983]) ).
cnf(c_4984,negated_conjecture,
( op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e21,e22) != e23
| e23 != e23
| op2(e23,op2(e23,e22)) != e22
| op2(e23,op2(e23,e21)) != e21 ),
inference(paramod,[status(thm)],[c_4736,c_4724]) ).
cnf(c_4737,negated_conjecture,
( op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e21,e22) != e23
| op2(e23,op2(e23,e22)) != e22
| op2(e23,op2(e23,e21)) != e21 ),
inference(copy,[status(thm)],[c_4984]) ).
cnf(c_4985,plain,
op2(e22,e23) = op2(e23,op2(e23,e21)),
inference(paramod,[status(thm)],[c_4736,c_4642]) ).
cnf(c_4986,plain,
e21 = op2(e23,op2(e23,e21)),
inference(paramod,[status(thm)],[c_992,c_4985]) ).
cnf(c_4739,plain,
op2(e23,op2(e23,e21)) = e21,
inference(copy,[status(thm)],[c_4986]) ).
cnf(c_4987,plain,
op2(e23,e21) = op2(e23,op2(e23,e22)),
inference(paramod,[status(thm)],[c_4736,c_4604]) ).
cnf(c_4744,plain,
op2(e23,op2(e23,e22)) = op2(e23,e21),
inference(copy,[status(thm)],[c_4987]) ).
cnf(c_4988,plain,
op2(e21,e22) = op2(e23,e20),
inference(paramod,[status(thm)],[c_4739,c_4600]) ).
cnf(c_4745,plain,
op2(e21,e22) = e23,
inference(paramod,[status(thm)],[c_4736,c_4988]) ).
cnf(c_4989,plain,
op2(e23,e22) = op2(e23,op2(e23,op2(e23,e22))),
inference(paramod,[status(thm)],[c_4736,c_4599]) ).
cnf(c_4990,plain,
op2(e23,e22) = op2(e23,op2(e23,e21)),
inference(paramod,[status(thm)],[c_4744,c_4989]) ).
cnf(c_4746,plain,
op2(e23,e22) = e21,
inference(paramod,[status(thm)],[c_4739,c_4990]) ).
cnf(c_4991,plain,
op2(e23,e21) != op2(e23,e20),
inference(paramod,[status(thm)],[c_4746,c_4589]) ).
cnf(c_4747,plain,
op2(e23,e21) != e23,
inference(paramod,[status(thm)],[c_4736,c_4991]) ).
cnf(c_4992,negated_conjecture,
( op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e21,e22) != e23
| op2(e23,op2(e23,e22)) != e22
| e21 != e21 ),
inference(paramod,[status(thm)],[c_4739,c_4737]) ).
cnf(c_4993,negated_conjecture,
( op2(e23,e22) != e21
| op2(e23,e21) != e22
| op2(e21,e22) != e23
| op2(e23,e21) != e22
| e21 != e21 ),
inference(paramod,[status(thm)],[c_4746,c_4992]) ).
cnf(c_4994,negated_conjecture,
( op2(e23,e22) != e21
| op2(e23,e21) != e22
| e23 != e23
| op2(e23,e21) != e22
| e21 != e21 ),
inference(paramod,[status(thm)],[c_4745,c_4993]) ).
cnf(c_4995,negated_conjecture,
( e21 != e21
| op2(e23,e21) != e22
| e23 != e23
| op2(e23,e21) != e22
| e21 != e21 ),
inference(paramod,[status(thm)],[c_4746,c_4994]) ).
cnf(c_4996,negated_conjecture,
( e21 != e21
| op2(e23,e21) != e22
| e23 != e23
| op2(e23,e21) != e22 ),
inference(copy,[status(thm)],[c_4995]) ).
cnf(c_4997,negated_conjecture,
( e21 != e21
| op2(e23,e21) != e22
| op2(e23,e21) != e22 ),
inference(copy,[status(thm)],[c_4996]) ).
cnf(c_4998,negated_conjecture,
( op2(e23,e21) != e22
| op2(e23,e21) != e22 ),
inference(copy,[status(thm)],[c_4997]) ).
cnf(c_4753,negated_conjecture,
op2(e23,e21) != e22,
inference(copy,[status(thm)],[c_4998]) ).
cnf(c_4999,plain,
( op2(e23,op2(e23,e22)) = e23
| op2(e23,e21) = e22 ),
inference(paramod,[status(thm)],[c_4746,c_4648]) ).
cnf(c_5000,plain,
( op2(e23,e21) = e23
| op2(e23,e21) = e22 ),
inference(paramod,[status(thm)],[c_4746,c_4999]) ).
cnf(c_5001,negated_conjecture,
op2(e23,e21) = e23,
inference(resolve,[status(thm)],[c_4753,c_5000]) ).
cnf(c_4760,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_4747,c_5001]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG015+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.56 % Computer : n008.cluster.edu
% 0.10/0.56 % Model : x86_64 x86_64
% 0.10/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.56 % Memory : 8046.5625MB
% 0.10/0.56 % OS : Linux 6.8.0-71-generic
% 0.10/0.56 % CPULimit : 300
% 0.10/0.56 % WCLimit : 300
% 0.10/0.56 % DateTime : Sat Sep 26 20:59:28 UTC 2026
% 0.10/0.57 % CPUTime :
% 0.10/0.57 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.57 % Process 350310 was started by sandbox2 on n008,
% 0.10/0.57 % Sat Sep 26 20:59:28 2026
% 0.10/0.57 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 56.87/57.35
% 56.87/57.35 % From the command line: assign(max_seconds, 300).
% 71.61/59.51
% 71.61/59.51 % SZS status Theorem for theBenchmark
% 71.61/59.51
% 71.61/59.51 % Proof 1 at 1.83 (+ 0.20) seconds.
% 71.61/59.51 % Length of proof is 169.
% 71.61/59.51 % Level of proof is 14.
% 71.61/59.51 % Maximum clause weight is 127.000.
% 71.61/59.51 % Given clauses 253.
% 71.61/59.51
% 71.61/59.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------