%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG016+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:49:07 AM UTC 2026
% Result : Theorem 11.21s 11.81s
% Output : CNFRefutation 11.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 137
% Number of leaves : 13
% Syntax : Number of formulae : 413 ( 239 unt; 0 def)
% Number of atoms : 2864 (2863 equ)
% Maximal formula atoms : 128 ( 6 avg)
% Number of connectives : 4472 (2021 ~;2033 |; 418 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 64 ( 7 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
( ( op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e13,e13) = e10 )
& ( op1(e13,e12) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11
| op1(e13,e12) = e10 )
& ( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e13,e11) = e10 )
& ( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 )
& ( op1(e12,e13) = e13
| op1(e12,e13) = e12
| op1(e12,e13) = e11
| op1(e12,e13) = e10 )
& ( op1(e12,e12) = e13
| op1(e12,e12) = e12
| op1(e12,e12) = e11
| op1(e12,e12) = e10 )
& ( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 )
& ( op1(e12,e10) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 )
& ( op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11
| op1(e11,e13) = e10 )
& ( op1(e11,e12) = e13
| op1(e11,e12) = e12
| op1(e11,e12) = e11
| op1(e11,e12) = e10 )
& ( op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e11) = e10 )
& ( op1(e11,e10) = e13
| op1(e11,e10) = e12
| op1(e11,e10) = e11
| op1(e11,e10) = e10 )
& ( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 )
& ( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 )
& ( op1(e10,e11) = e13
| op1(e10,e11) = e12
| op1(e10,e11) = e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e11
| op1(e10,e10) = e10 ) ),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
( op1(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(ax24,axiom,
( e13 = op1(e12,e12)
& e11 = op1(e12,op1(e12,e12))
& e10 = op1(op1(e12,op1(e12,e12)),e12) ),
file('theBenchmark.p',ax24) ).
fof(ax25,axiom,
( e23 = op2(e22,e22)
& e21 = op2(e22,op2(e22,e22))
& e20 = op2(op2(e22,op2(e22,e22)),e22) ),
file('theBenchmark.p',ax25) ).
fof(ax26,axiom,
( h1(e13) = op2(e20,e20)
& h1(e11) = op2(e20,op2(e20,e20))
& h1(e10) = op2(op2(e20,op2(e20,e20)),e20)
& h1(e12) = e20 ),
file('theBenchmark.p',ax26) ).
fof(ax27,axiom,
( h2(e13) = op2(e21,e21)
& h2(e11) = op2(e21,op2(e21,e21))
& h2(e10) = op2(op2(e21,op2(e21,e21)),e21)
& h2(e12) = e21 ),
file('theBenchmark.p',ax27) ).
fof(ax28,axiom,
( h3(e13) = op2(e22,e22)
& h3(e11) = op2(e22,op2(e22,e22))
& h3(e10) = op2(op2(e22,op2(e22,e22)),e22)
& h3(e12) = e22 ),
file('theBenchmark.p',ax28) ).
fof(ax29,axiom,
( h4(e13) = op2(e23,e23)
& h4(e11) = op2(e23,op2(e23,e23))
& h4(e10) = op2(op2(e23,op2(e23,e23)),e23)
& h4(e12) = e23 ),
file('theBenchmark.p',ax29) ).
fof(co1,conjecture,
( ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ( ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_42,plain,
( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e13,e11) = e10 ),
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_55,plain,
op1(op1(e10,e12),e12) = op1(e10,op1(e12,e12)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_56,plain,
op1(op1(e10,e12),e13) = op1(e10,op1(e12,e13)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_71,plain,
op1(op1(e11,e12),e12) = op1(e11,op1(e12,e12)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_75,plain,
op1(op1(e11,e13),e12) = op1(e11,op1(e13,e12)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_80,plain,
op1(op1(e12,e10),e13) = op1(e12,op1(e10,e13)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_81,plain,
op1(op1(e12,e11),e10) = op1(e12,op1(e11,e10)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_82,plain,
op1(op1(e12,e11),e11) = op1(e12,op1(e11,e11)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_83,plain,
op1(op1(e12,e11),e12) = op1(e12,op1(e11,e12)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_84,plain,
op1(op1(e12,e11),e13) = op1(e12,op1(e11,e13)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_86,plain,
op1(op1(e12,e12),e11) = op1(e12,op1(e12,e11)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_87,plain,
op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_88,plain,
op1(op1(e12,e12),e13) = op1(e12,op1(e12,e13)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_89,plain,
op1(op1(e12,e13),e10) = op1(e12,op1(e13,e10)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_91,plain,
op1(op1(e12,e13),e12) = op1(e12,op1(e13,e12)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_92,plain,
op1(op1(e12,e13),e13) = op1(e12,op1(e13,e13)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_102,plain,
op1(op1(e13,e12),e11) = op1(e13,op1(e12,e11)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_103,plain,
op1(op1(e13,e12),e12) = op1(e13,op1(e12,e12)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_107,plain,
op1(op1(e13,e13),e12) = op1(e13,op1(e13,e12)),
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_143,plain,
( op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e23,e21) = e21
| op2(e23,e21) = e20 ),
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_170,plain,
op2(op2(e21,e22),e20) = op2(e21,op2(e22,e20)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_171,plain,
op2(op2(e21,e22),e21) = op2(e21,op2(e22,e21)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_176,plain,
op2(op2(e21,e23),e22) = op2(e21,op2(e23,e22)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_177,plain,
op2(op2(e21,e23),e23) = op2(e21,op2(e23,e23)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_184,plain,
op2(op2(e22,e21),e22) = op2(e22,op2(e21,e22)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_185,plain,
op2(op2(e22,e21),e23) = op2(e22,op2(e21,e23)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_186,plain,
op2(op2(e22,e22),e20) = op2(e22,op2(e22,e20)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_187,plain,
op2(op2(e22,e22),e21) = op2(e22,op2(e22,e21)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_188,plain,
op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_189,plain,
op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_191,plain,
op2(op2(e22,e23),e21) = op2(e22,op2(e23,e21)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_192,plain,
op2(op2(e22,e23),e22) = op2(e22,op2(e23,e22)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_200,plain,
op2(op2(e23,e21),e22) = op2(e23,op2(e21,e22)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_204,plain,
op2(op2(e23,e22),e22) = op2(e23,op2(e22,e22)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_205,plain,
op2(op2(e23,e22),e23) = op2(e23,op2(e22,e23)),
inference(clausify,[status(thm)],[ax6]) ).
cnf(c_330,plain,
op1(e12,e12) != op1(e12,e10),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_331,plain,
op1(e12,e10) != op1(e12,e12),
inference(copy,[status(thm)],[c_330]) ).
cnf(c_332,plain,
op1(e12,e13) != op1(e12,e10),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_343,plain,
op1(e13,e13) != op1(e13,e11),
inference(clausify,[status(thm)],[ax17]) ).
cnf(c_393,plain,
op2(e22,e21) != op2(e22,e20),
inference(clausify,[status(thm)],[ax18]) ).
cnf(c_394,plain,
op2(e22,e22) != op2(e22,e20),
inference(clausify,[status(thm)],[ax18]) ).
cnf(c_395,plain,
op2(e22,e20) != op2(e22,e22),
inference(copy,[status(thm)],[c_394]) ).
cnf(c_396,plain,
op2(e22,e23) != op2(e22,e20),
inference(clausify,[status(thm)],[ax18]) ).
cnf(c_462,plain,
op1(op1(e12,op1(e12,e12)),e12) = e10,
inference(clausify,[status(thm)],[ax24]) ).
cnf(c_463,plain,
op1(e12,op1(e12,e12)) = e11,
inference(clausify,[status(thm)],[ax24]) ).
cnf(c_464,plain,
op1(e12,e12) = e13,
inference(clausify,[status(thm)],[ax24]) ).
cnf(c_465,plain,
op2(op2(e22,op2(e22,e22)),e22) = e20,
inference(clausify,[status(thm)],[ax25]) ).
cnf(c_466,plain,
op2(e22,op2(e22,e22)) = e21,
inference(clausify,[status(thm)],[ax25]) ).
cnf(c_467,plain,
op2(e22,e22) = e23,
inference(clausify,[status(thm)],[ax25]) ).
cnf(c_473,plain,
h1(e13) = op2(e20,e20),
inference(clausify,[status(thm)],[ax26]) ).
cnf(c_474,plain,
op2(e20,e20) = h1(e13),
inference(copy,[status(thm)],[c_473]) ).
cnf(c_480,plain,
h2(e13) = op2(e21,e21),
inference(clausify,[status(thm)],[ax27]) ).
cnf(c_481,plain,
op2(e21,e21) = h2(e13),
inference(copy,[status(thm)],[c_480]) ).
cnf(c_482,plain,
h3(e12) = e22,
inference(clausify,[status(thm)],[ax28]) ).
cnf(c_483,plain,
h3(e10) = op2(op2(e22,op2(e22,e22)),e22),
inference(clausify,[status(thm)],[ax28]) ).
cnf(c_2122,plain,
h3(e10) = op2(op2(e22,e23),e22),
inference(paramod,[status(thm)],[c_467,c_483]) ).
cnf(c_2123,plain,
h3(e10) = op2(e22,op2(e23,e22)),
inference(paramod,[status(thm)],[c_192,c_2122]) ).
cnf(c_484,plain,
op2(e22,op2(e23,e22)) = h3(e10),
inference(copy,[status(thm)],[c_2123]) ).
cnf(c_485,plain,
h3(e11) = op2(e22,op2(e22,e22)),
inference(clausify,[status(thm)],[ax28]) ).
cnf(c_2124,plain,
h3(e11) = op2(e22,e23),
inference(paramod,[status(thm)],[c_467,c_485]) ).
cnf(c_486,plain,
op2(e22,e23) = h3(e11),
inference(copy,[status(thm)],[c_2124]) ).
cnf(c_487,plain,
h3(e13) = op2(e22,e22),
inference(clausify,[status(thm)],[ax28]) ).
cnf(c_488,plain,
h3(e13) = e23,
inference(paramod,[status(thm)],[c_467,c_487]) ).
cnf(c_494,plain,
h4(e13) = op2(e23,e23),
inference(clausify,[status(thm)],[ax29]) ).
cnf(c_495,plain,
op2(e23,e23) = h4(e13),
inference(copy,[status(thm)],[c_494]) ).
cnf(c_1214,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_2125,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_482,c_1214]) ).
cnf(c_2126,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_488,c_2125]) ).
cnf(c_2127,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_482,c_2126]) ).
cnf(c_2128,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_488,c_2127]) ).
cnf(c_2129,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_482,c_2128]) ).
cnf(c_2130,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_482,c_2129]) ).
cnf(c_2131,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(e13) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_464,c_2130]) ).
cnf(c_2132,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| e23 != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_488,c_2131]) ).
cnf(c_2133,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| e23 != op2(e22,h3(e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_482,c_2132]) ).
cnf(c_2134,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| e23 != op2(e22,e22)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_482,c_2133]) ).
cnf(c_2135,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_467,c_2134]) ).
cnf(c_2136,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(e22,h3(e13))
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_482,c_2135]) ).
cnf(c_2137,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_488,c_2136]) ).
cnf(c_2138,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_486,c_2137]) ).
cnf(c_2139,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_488,c_2138]) ).
cnf(c_2140,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_488,c_2139]) ).
cnf(c_2141,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(e23,h3(e12))
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_488,c_2140]) ).
cnf(c_2142,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_482,c_2141]) ).
cnf(c_2143,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(e23,h3(e13))
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_488,c_2142]) ).
cnf(c_2144,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_488,c_2143]) ).
cnf(c_2145,negated_conjecture,
( h3(e13) != e23
| h3(e12) != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_495,c_2144]) ).
cnf(c_2146,negated_conjecture,
( h3(e13) != e23
| e22 != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_482,c_2145]) ).
cnf(c_2147,negated_conjecture,
( e23 != e23
| e22 != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(paramod,[status(thm)],[c_488,c_2146]) ).
cnf(c_2148,negated_conjecture,
( e23 != e23
| e22 != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2147]) ).
cnf(c_2149,negated_conjecture,
( e23 != e23
| e22 != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),h3(e11)) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2148]) ).
cnf(c_2150,negated_conjecture,
( e23 != e23
| e22 != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),h3(e11)) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2149]) ).
cnf(c_2151,negated_conjecture,
( e23 != e23
| e22 != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),h3(e11)) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2150]) ).
cnf(c_2152,negated_conjecture,
( e23 != e23
| e22 != e22
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),h3(e11)) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2151]) ).
cnf(c_2153,negated_conjecture,
( e23 != e23
| h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),h3(e11)) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2152]) ).
cnf(c_1215,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),h3(e11)) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2153]) ).
cnf(c_2154,plain,
op1(op1(e12,e13),e12) = e10,
inference(paramod,[status(thm)],[c_464,c_462]) ).
cnf(c_1799,plain,
op1(e12,op1(e13,e12)) = e10,
inference(paramod,[status(thm)],[c_91,c_2154]) ).
cnf(c_2155,plain,
op1(e13,e12) = op1(e12,op1(e12,e12)),
inference(paramod,[status(thm)],[c_464,c_87]) ).
cnf(c_1800,plain,
op1(e13,e12) = op1(e12,e13),
inference(paramod,[status(thm)],[c_464,c_2155]) ).
cnf(c_1801,plain,
op1(e12,e13) = e11,
inference(paramod,[status(thm)],[c_464,c_463]) ).
cnf(c_1804,plain,
op1(e12,e10) != e13,
inference(paramod,[status(thm)],[c_464,c_331]) ).
cnf(c_2156,plain,
op1(op1(e12,e13),e12) = op1(e13,op1(e12,e12)),
inference(paramod,[status(thm)],[c_1800,c_103]) ).
cnf(c_2157,plain,
op1(e11,e12) = op1(e13,op1(e12,e12)),
inference(paramod,[status(thm)],[c_1801,c_2156]) ).
cnf(c_2158,plain,
op1(e11,e12) = op1(e13,e13),
inference(paramod,[status(thm)],[c_464,c_2157]) ).
cnf(c_1807,plain,
op1(e13,e13) = op1(e11,e12),
inference(copy,[status(thm)],[c_2158]) ).
cnf(c_2159,plain,
op1(e13,e13) = op1(e12,op1(e12,e13)),
inference(paramod,[status(thm)],[c_464,c_88]) ).
cnf(c_2160,plain,
op1(e11,e12) = op1(e12,op1(e12,e13)),
inference(paramod,[status(thm)],[c_1807,c_2159]) ).
cnf(c_1808,plain,
op1(e11,e12) = op1(e12,e11),
inference(paramod,[status(thm)],[c_1801,c_2160]) ).
cnf(c_2161,plain,
op1(e13,e11) = op1(e12,op1(e12,e11)),
inference(paramod,[status(thm)],[c_464,c_86]) ).
cnf(c_1809,plain,
op1(e12,op1(e12,e11)) = op1(e13,e11),
inference(copy,[status(thm)],[c_2161]) ).
cnf(c_2162,plain,
op1(op1(e12,e11),e12) = op1(e11,op1(e12,e12)),
inference(paramod,[status(thm)],[c_1808,c_71]) ).
cnf(c_2163,plain,
op1(e12,op1(e11,e12)) = op1(e11,op1(e12,e12)),
inference(paramod,[status(thm)],[c_83,c_2162]) ).
cnf(c_2164,plain,
op1(e12,op1(e12,e11)) = op1(e11,op1(e12,e12)),
inference(paramod,[status(thm)],[c_1808,c_2163]) ).
cnf(c_2165,plain,
op1(e13,e11) = op1(e11,op1(e12,e12)),
inference(paramod,[status(thm)],[c_1809,c_2164]) ).
cnf(c_1811,plain,
op1(e13,e11) = op1(e11,e13),
inference(paramod,[status(thm)],[c_464,c_2165]) ).
cnf(c_1812,plain,
op1(op1(e10,e12),e12) = op1(e10,e13),
inference(paramod,[status(thm)],[c_464,c_55]) ).
cnf(c_2166,plain,
op2(op2(e22,e23),e22) = e20,
inference(paramod,[status(thm)],[c_467,c_465]) ).
cnf(c_1813,plain,
op2(h3(e11),e22) = e20,
inference(paramod,[status(thm)],[c_486,c_2166]) ).
cnf(c_2167,plain,
op2(e23,e22) = op2(e22,op2(e22,e22)),
inference(paramod,[status(thm)],[c_467,c_188]) ).
cnf(c_2168,plain,
op2(e23,e22) = op2(e22,e23),
inference(paramod,[status(thm)],[c_467,c_2167]) ).
cnf(c_1814,plain,
op2(e23,e22) = h3(e11),
inference(paramod,[status(thm)],[c_486,c_2168]) ).
cnf(c_2169,plain,
op2(e22,e23) = e21,
inference(paramod,[status(thm)],[c_467,c_466]) ).
cnf(c_1815,plain,
h3(e11) = e21,
inference(paramod,[status(thm)],[c_486,c_2169]) ).
cnf(c_1818,plain,
op2(e22,e20) != e23,
inference(paramod,[status(thm)],[c_467,c_395]) ).
cnf(c_2170,plain,
op2(h3(e11),e22) = op2(e23,op2(e22,e22)),
inference(paramod,[status(thm)],[c_1814,c_204]) ).
cnf(c_2171,plain,
op2(e21,e22) = op2(e23,op2(e22,e22)),
inference(paramod,[status(thm)],[c_1815,c_2170]) ).
cnf(c_2172,plain,
op2(e21,e22) = op2(e23,e23),
inference(paramod,[status(thm)],[c_467,c_2171]) ).
cnf(c_1821,plain,
op2(e21,e22) = h4(e13),
inference(paramod,[status(thm)],[c_495,c_2172]) ).
cnf(c_2173,plain,
op2(e23,e23) = op2(e22,op2(e22,e23)),
inference(paramod,[status(thm)],[c_467,c_189]) ).
cnf(c_2174,plain,
h4(e13) = op2(e22,op2(e22,e23)),
inference(paramod,[status(thm)],[c_495,c_2173]) ).
cnf(c_2175,plain,
h4(e13) = op2(e22,h3(e11)),
inference(paramod,[status(thm)],[c_486,c_2174]) ).
cnf(c_2176,plain,
h4(e13) = op2(e22,e21),
inference(paramod,[status(thm)],[c_1815,c_2175]) ).
cnf(c_1822,plain,
op2(e22,e21) = h4(e13),
inference(copy,[status(thm)],[c_2176]) ).
cnf(c_2177,plain,
op2(e23,e21) = op2(e22,op2(e22,e21)),
inference(paramod,[status(thm)],[c_467,c_187]) ).
cnf(c_2178,plain,
op2(e23,e21) = op2(e22,h4(e13)),
inference(paramod,[status(thm)],[c_1822,c_2177]) ).
cnf(c_1823,plain,
op2(e22,h4(e13)) = op2(e23,e21),
inference(copy,[status(thm)],[c_2178]) ).
cnf(c_2179,plain,
op2(e23,e20) = op2(e22,op2(e22,e20)),
inference(paramod,[status(thm)],[c_467,c_186]) ).
cnf(c_1824,plain,
op2(e22,op2(e22,e20)) = op2(e23,e20),
inference(copy,[status(thm)],[c_2179]) ).
cnf(c_2180,plain,
h3(e11) != op2(e22,e20),
inference(paramod,[status(thm)],[c_486,c_396]) ).
cnf(c_2181,plain,
e21 != op2(e22,e20),
inference(paramod,[status(thm)],[c_1815,c_2180]) ).
cnf(c_1859,plain,
op2(e22,e20) != e21,
inference(copy,[status(thm)],[c_2181]) ).
cnf(c_2182,plain,
op2(h3(e11),e23) = op2(e23,op2(e22,e23)),
inference(paramod,[status(thm)],[c_1814,c_205]) ).
cnf(c_2183,plain,
op2(e21,e23) = op2(e23,op2(e22,e23)),
inference(paramod,[status(thm)],[c_1815,c_2182]) ).
cnf(c_2184,plain,
op2(e21,e23) = op2(e23,h3(e11)),
inference(paramod,[status(thm)],[c_486,c_2183]) ).
cnf(c_2185,plain,
op2(e21,e23) = op2(e23,e21),
inference(paramod,[status(thm)],[c_1815,c_2184]) ).
cnf(c_1862,plain,
op2(e23,e21) = op2(e21,e23),
inference(copy,[status(thm)],[c_2185]) ).
cnf(c_2186,plain,
op2(h3(e11),e21) = op2(e22,op2(e23,e21)),
inference(paramod,[status(thm)],[c_486,c_191]) ).
cnf(c_2187,plain,
op2(e21,e21) = op2(e22,op2(e23,e21)),
inference(paramod,[status(thm)],[c_1815,c_2186]) ).
cnf(c_2188,plain,
h2(e13) = op2(e22,op2(e23,e21)),
inference(paramod,[status(thm)],[c_481,c_2187]) ).
cnf(c_2189,plain,
h2(e13) = op2(e22,op2(e21,e23)),
inference(paramod,[status(thm)],[c_1862,c_2188]) ).
cnf(c_1863,plain,
op2(e22,op2(e21,e23)) = h2(e13),
inference(copy,[status(thm)],[c_2189]) ).
cnf(c_1875,plain,
op2(op2(e21,e23),e23) = op2(e21,h4(e13)),
inference(paramod,[status(thm)],[c_495,c_177]) ).
cnf(c_2190,plain,
op1(e12,op1(e12,e13)) = e10,
inference(paramod,[status(thm)],[c_1800,c_1799]) ).
cnf(c_1878,plain,
op1(e12,e11) = e10,
inference(paramod,[status(thm)],[c_1801,c_2190]) ).
cnf(c_2191,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(h3(e11),h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1815,c_1215]) ).
cnf(c_2192,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(h3(e11),h3(e11)) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1815,c_2191]) ).
cnf(c_2193,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(e21,h3(e11)) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1815,c_2192]) ).
cnf(c_2194,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| op2(e21,e21) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1815,c_2193]) ).
cnf(c_2195,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_481,c_2194]) ).
cnf(c_2196,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e12,e11)) != op2(h3(e11),e22)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1808,c_2195]) ).
cnf(c_2197,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(e10) != op2(h3(e11),e22)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1878,c_2196]) ).
cnf(c_2198,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(e10) != op2(e21,e22)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1815,c_2197]) ).
cnf(c_2199,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1821,c_2198]) ).
cnf(c_2200,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1815,c_2199]) ).
cnf(c_2201,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(e10) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1878,c_2200]) ).
cnf(c_2202,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(e10) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1815,c_2201]) ).
cnf(c_2203,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != h3(e11)
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1822,c_2202]) ).
cnf(c_2204,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != h3(e11)
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1801,c_2203]) ).
cnf(c_2205,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != h3(e11)
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1815,c_2204]) ).
cnf(c_2206,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1815,c_2205]) ).
cnf(c_2207,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1811,c_2206]) ).
cnf(c_2208,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1815,c_2207]) ).
cnf(c_2209,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1862,c_2208]) ).
cnf(c_2210,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e12,e13)) != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1800,c_2209]) ).
cnf(c_2211,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| h3(e11) != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1801,c_2210]) ).
cnf(c_2212,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| e21 != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1815,c_2211]) ).
cnf(c_2213,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| e21 != h3(e11)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1814,c_2212]) ).
cnf(c_2214,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e13,e13)) != h4(e13)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1815,c_2213]) ).
cnf(c_2215,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e11,e12)) != h4(e13)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1807,c_2214]) ).
cnf(c_2216,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(op1(e12,e11)) != h4(e13)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1808,c_2215]) ).
cnf(c_2217,negated_conjecture,
( h3(e11) != e21
| h3(e10) != e20
| h3(e10) != h4(e13)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1878,c_2216]) ).
cnf(c_2218,negated_conjecture,
( e21 != e21
| h3(e10) != e20
| h3(e10) != h4(e13)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| op2(h3(e10),e21) != h3(op1(e10,e11))
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1815,c_2217]) ).
cnf(c_2219,negated_conjecture,
( e21 != e21
| h3(e10) != e20
| h3(e10) != h4(e13)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| op2(e21,h3(e10)) != h3(op1(e11,e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2218]) ).
cnf(c_2220,negated_conjecture,
( e21 != e21
| h3(e10) != e20
| h3(e10) != h4(e13)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h2(e13) != h3(op1(e11,e11))
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2219]) ).
cnf(c_2221,negated_conjecture,
( e21 != e21
| h3(e10) != e20
| h3(e10) != h4(e13)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2220]) ).
cnf(c_2222,negated_conjecture,
( e21 != e21
| h3(e10) != e20
| h3(e10) != h4(e13)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(e10) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2221]) ).
cnf(c_2223,negated_conjecture,
( e21 != e21
| h3(e10) != e20
| h3(e10) != h4(e13)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h4(e13) != h3(e10)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2222]) ).
cnf(c_2224,negated_conjecture,
( e21 != e21
| h3(e10) != e20
| h4(e13) != h3(e10)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h4(e13) != h3(e10)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2223]) ).
cnf(c_2225,negated_conjecture,
( e21 != e21
| h3(e10) != e20
| h4(e13) != h3(e10)
| e21 != e21
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h4(e13) != h3(e10)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2224]) ).
cnf(c_2226,negated_conjecture,
( e21 != e21
| h3(e10) != e20
| h4(e13) != h3(e10)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h4(e13) != h3(e10)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2225]) ).
cnf(c_2227,negated_conjecture,
( h3(e10) != e20
| h4(e13) != h3(e10)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h4(e13) != h3(e10)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2226]) ).
cnf(c_2228,negated_conjecture,
( h3(e10) != e20
| h4(e13) != h3(e10)
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2227]) ).
cnf(c_2229,negated_conjecture,
( h3(e10) != e20
| h4(e13) != h3(e10)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2228]) ).
cnf(c_1897,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(h3(e10),h3(e10)) != h3(op1(e10,e10)) ),
inference(copy,[status(thm)],[c_2229]) ).
cnf(c_2230,plain,
op1(op1(e11,e12),e12) = op1(e13,op1(e13,e12)),
inference(paramod,[status(thm)],[c_1807,c_107]) ).
cnf(c_2231,plain,
op1(op1(e12,e11),e12) = op1(e13,op1(e13,e12)),
inference(paramod,[status(thm)],[c_1808,c_2230]) ).
cnf(c_2232,plain,
op1(e10,e12) = op1(e13,op1(e13,e12)),
inference(paramod,[status(thm)],[c_1878,c_2231]) ).
cnf(c_2233,plain,
op1(e10,e12) = op1(e13,op1(e12,e13)),
inference(paramod,[status(thm)],[c_1800,c_2232]) ).
cnf(c_2234,plain,
op1(e10,e12) = op1(e13,e11),
inference(paramod,[status(thm)],[c_1801,c_2233]) ).
cnf(c_2235,plain,
op1(e10,e12) = op1(e11,e13),
inference(paramod,[status(thm)],[c_1811,c_2234]) ).
cnf(c_1955,plain,
op1(e11,e13) = op1(e10,e12),
inference(copy,[status(thm)],[c_2235]) ).
cnf(c_2236,plain,
op1(op1(e12,e13),e11) = op1(e13,op1(e12,e11)),
inference(paramod,[status(thm)],[c_1800,c_102]) ).
cnf(c_2237,plain,
op1(e11,e11) = op1(e13,op1(e12,e11)),
inference(paramod,[status(thm)],[c_1801,c_2236]) ).
cnf(c_2238,plain,
op1(e11,e11) = op1(e13,e10),
inference(paramod,[status(thm)],[c_1878,c_2237]) ).
cnf(c_1956,plain,
op1(e13,e10) = op1(e11,e11),
inference(copy,[status(thm)],[c_2238]) ).
cnf(c_2239,plain,
op1(op1(e10,e12),e12) = op1(e11,op1(e13,e12)),
inference(paramod,[status(thm)],[c_1955,c_75]) ).
cnf(c_2240,plain,
op1(e10,e13) = op1(e11,op1(e13,e12)),
inference(paramod,[status(thm)],[c_1812,c_2239]) ).
cnf(c_2241,plain,
op1(e10,e13) = op1(e11,op1(e12,e13)),
inference(paramod,[status(thm)],[c_1800,c_2240]) ).
cnf(c_2242,plain,
op1(e10,e13) = op1(e11,e11),
inference(paramod,[status(thm)],[c_1801,c_2241]) ).
cnf(c_1958,plain,
op1(e11,e11) = op1(e10,e13),
inference(copy,[status(thm)],[c_2242]) ).
cnf(c_2243,plain,
e11 != op1(e12,e10),
inference(paramod,[status(thm)],[c_1801,c_332]) ).
cnf(c_1961,plain,
op1(e12,e10) != e11,
inference(copy,[status(thm)],[c_2243]) ).
cnf(c_2244,plain,
op1(e11,e13) = op1(e12,op1(e13,e13)),
inference(paramod,[status(thm)],[c_1801,c_92]) ).
cnf(c_2245,plain,
op1(e10,e12) = op1(e12,op1(e13,e13)),
inference(paramod,[status(thm)],[c_1955,c_2244]) ).
cnf(c_2246,plain,
op1(e10,e12) = op1(e12,op1(e11,e12)),
inference(paramod,[status(thm)],[c_1807,c_2245]) ).
cnf(c_2247,plain,
op1(e10,e12) = op1(e12,op1(e12,e11)),
inference(paramod,[status(thm)],[c_1808,c_2246]) ).
cnf(c_1963,plain,
op1(e10,e12) = op1(e12,e10),
inference(paramod,[status(thm)],[c_1878,c_2247]) ).
cnf(c_2248,plain,
op1(e11,e10) = op1(e12,op1(e13,e10)),
inference(paramod,[status(thm)],[c_1801,c_89]) ).
cnf(c_2249,plain,
op1(e11,e10) = op1(e12,op1(e11,e11)),
inference(paramod,[status(thm)],[c_1956,c_2248]) ).
cnf(c_2250,plain,
op1(e11,e10) = op1(e12,op1(e10,e13)),
inference(paramod,[status(thm)],[c_1958,c_2249]) ).
cnf(c_1964,plain,
op1(e12,op1(e10,e13)) = op1(e11,e10),
inference(copy,[status(thm)],[c_2250]) ).
cnf(c_2251,plain,
op1(op1(e12,e10),e13) = op1(e10,op1(e12,e13)),
inference(paramod,[status(thm)],[c_1963,c_56]) ).
cnf(c_2252,plain,
op1(e12,op1(e10,e13)) = op1(e10,op1(e12,e13)),
inference(paramod,[status(thm)],[c_80,c_2251]) ).
cnf(c_2253,plain,
op1(e11,e10) = op1(e10,op1(e12,e13)),
inference(paramod,[status(thm)],[c_1964,c_2252]) ).
cnf(c_1965,plain,
op1(e11,e10) = op1(e10,e11),
inference(paramod,[status(thm)],[c_1801,c_2253]) ).
cnf(c_2254,plain,
op1(e11,e12) != op1(e13,e11),
inference(paramod,[status(thm)],[c_1807,c_343]) ).
cnf(c_2255,plain,
op1(e12,e11) != op1(e13,e11),
inference(paramod,[status(thm)],[c_1808,c_2254]) ).
cnf(c_2256,plain,
e10 != op1(e13,e11),
inference(paramod,[status(thm)],[c_1878,c_2255]) ).
cnf(c_2257,plain,
e10 != op1(e11,e13),
inference(paramod,[status(thm)],[c_1811,c_2256]) ).
cnf(c_2258,plain,
e10 != op1(e10,e12),
inference(paramod,[status(thm)],[c_1955,c_2257]) ).
cnf(c_2259,plain,
e10 != op1(e12,e10),
inference(paramod,[status(thm)],[c_1963,c_2258]) ).
cnf(c_1967,plain,
op1(e12,e10) != e10,
inference(copy,[status(thm)],[c_2259]) ).
cnf(c_2260,plain,
( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e11,e13) = e10 ),
inference(paramod,[status(thm)],[c_1811,c_42]) ).
cnf(c_2261,plain,
( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e10,e12) = e10 ),
inference(paramod,[status(thm)],[c_1955,c_2260]) ).
cnf(c_2262,plain,
( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e12,e10) = e10 ),
inference(paramod,[status(thm)],[c_1963,c_2261]) ).
cnf(c_2263,plain,
( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e11,e13) = e11
| op1(e12,e10) = e10 ),
inference(paramod,[status(thm)],[c_1811,c_2262]) ).
cnf(c_2264,plain,
( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e10,e12) = e11
| op1(e12,e10) = e10 ),
inference(paramod,[status(thm)],[c_1955,c_2263]) ).
cnf(c_2265,plain,
( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 ),
inference(paramod,[status(thm)],[c_1963,c_2264]) ).
cnf(c_2266,plain,
( op1(e13,e11) = e13
| op1(e11,e13) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 ),
inference(paramod,[status(thm)],[c_1811,c_2265]) ).
cnf(c_2267,plain,
( op1(e13,e11) = e13
| op1(e10,e12) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 ),
inference(paramod,[status(thm)],[c_1955,c_2266]) ).
cnf(c_2268,plain,
( op1(e13,e11) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 ),
inference(paramod,[status(thm)],[c_1963,c_2267]) ).
cnf(c_2269,plain,
( op1(e11,e13) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 ),
inference(paramod,[status(thm)],[c_1811,c_2268]) ).
cnf(c_2270,plain,
( op1(e10,e12) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 ),
inference(paramod,[status(thm)],[c_1955,c_2269]) ).
cnf(c_2271,plain,
( op1(e12,e10) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 ),
inference(paramod,[status(thm)],[c_1963,c_2270]) ).
cnf(c_2272,plain,
( op1(e12,e10) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11 ),
inference(resolve,[status(thm)],[c_1967,c_2271]) ).
cnf(c_2273,plain,
( op1(e12,e10) = e13
| op1(e12,e10) = e12 ),
inference(resolve,[status(thm)],[c_1961,c_2272]) ).
cnf(c_1980,plain,
op1(e12,e10) = e12,
inference(resolve,[status(thm)],[c_1804,c_2273]) ).
cnf(c_2274,plain,
op2(e22,h3(e11)) = h3(e10),
inference(paramod,[status(thm)],[c_1814,c_484]) ).
cnf(c_2275,plain,
op2(e22,e21) = h3(e10),
inference(paramod,[status(thm)],[c_1815,c_2274]) ).
cnf(c_1981,plain,
h4(e13) = h3(e10),
inference(paramod,[status(thm)],[c_1822,c_2275]) ).
cnf(c_2276,plain,
op2(op2(e21,e23),e22) = op2(e21,h3(e11)),
inference(paramod,[status(thm)],[c_1814,c_176]) ).
cnf(c_2277,plain,
op2(op2(e21,e23),e22) = op2(e21,e21),
inference(paramod,[status(thm)],[c_1815,c_2276]) ).
cnf(c_1987,plain,
op2(op2(e21,e23),e22) = h2(e13),
inference(paramod,[status(thm)],[c_481,c_2277]) ).
cnf(c_2278,plain,
op2(e21,e22) = e20,
inference(paramod,[status(thm)],[c_1815,c_1813]) ).
cnf(c_2279,plain,
h4(e13) = e20,
inference(paramod,[status(thm)],[c_1821,c_2278]) ).
cnf(c_1990,plain,
h3(e10) = e20,
inference(paramod,[status(thm)],[c_1981,c_2279]) ).
cnf(c_1991,plain,
op2(e22,e23) = e21,
inference(paramod,[status(thm)],[c_1815,c_486]) ).
cnf(c_2280,plain,
op2(op2(e21,e23),e22) = op2(e23,op2(e21,e22)),
inference(paramod,[status(thm)],[c_1862,c_200]) ).
cnf(c_2281,plain,
h2(e13) = op2(e23,op2(e21,e22)),
inference(paramod,[status(thm)],[c_1987,c_2280]) ).
cnf(c_2282,plain,
h2(e13) = op2(e23,h4(e13)),
inference(paramod,[status(thm)],[c_1821,c_2281]) ).
cnf(c_2283,plain,
h2(e13) = op2(e23,h3(e10)),
inference(paramod,[status(thm)],[c_1981,c_2282]) ).
cnf(c_2284,plain,
h2(e13) = op2(e23,e20),
inference(paramod,[status(thm)],[c_1990,c_2283]) ).
cnf(c_1997,plain,
op2(e23,e20) = h2(e13),
inference(copy,[status(thm)],[c_2284]) ).
cnf(c_2285,plain,
op2(h4(e13),e22) = op2(e22,op2(e21,e22)),
inference(paramod,[status(thm)],[c_1822,c_184]) ).
cnf(c_2286,plain,
op2(h3(e10),e22) = op2(e22,op2(e21,e22)),
inference(paramod,[status(thm)],[c_1981,c_2285]) ).
cnf(c_2287,plain,
op2(e20,e22) = op2(e22,op2(e21,e22)),
inference(paramod,[status(thm)],[c_1990,c_2286]) ).
cnf(c_2288,plain,
op2(e20,e22) = op2(e22,h4(e13)),
inference(paramod,[status(thm)],[c_1821,c_2287]) ).
cnf(c_2289,plain,
op2(e20,e22) = op2(e22,h3(e10)),
inference(paramod,[status(thm)],[c_1981,c_2288]) ).
cnf(c_1998,plain,
op2(e20,e22) = op2(e22,e20),
inference(paramod,[status(thm)],[c_1990,c_2289]) ).
cnf(c_2290,plain,
op2(h4(e13),e21) = op2(e21,op2(e22,e21)),
inference(paramod,[status(thm)],[c_1821,c_171]) ).
cnf(c_2291,plain,
op2(h3(e10),e21) = op2(e21,op2(e22,e21)),
inference(paramod,[status(thm)],[c_1981,c_2290]) ).
cnf(c_2292,plain,
op2(e20,e21) = op2(e21,op2(e22,e21)),
inference(paramod,[status(thm)],[c_1990,c_2291]) ).
cnf(c_2293,plain,
op2(e20,e21) = op2(e21,h4(e13)),
inference(paramod,[status(thm)],[c_1822,c_2292]) ).
cnf(c_2294,plain,
op2(e20,e21) = op2(e21,h3(e10)),
inference(paramod,[status(thm)],[c_1981,c_2293]) ).
cnf(c_2295,plain,
op2(e20,e21) = op2(e21,e20),
inference(paramod,[status(thm)],[c_1990,c_2294]) ).
cnf(c_1999,plain,
op2(e21,e20) = op2(e20,e21),
inference(copy,[status(thm)],[c_2295]) ).
cnf(c_2296,plain,
op2(h4(e13),e20) = op2(e21,op2(e22,e20)),
inference(paramod,[status(thm)],[c_1821,c_170]) ).
cnf(c_2297,plain,
op2(h3(e10),e20) = op2(e21,op2(e22,e20)),
inference(paramod,[status(thm)],[c_1981,c_2296]) ).
cnf(c_2298,plain,
op2(e20,e20) = op2(e21,op2(e22,e20)),
inference(paramod,[status(thm)],[c_1990,c_2297]) ).
cnf(c_2299,plain,
h1(e13) = op2(e21,op2(e22,e20)),
inference(paramod,[status(thm)],[c_474,c_2298]) ).
cnf(c_2000,plain,
op2(e21,op2(e22,e20)) = h1(e13),
inference(copy,[status(thm)],[c_2299]) ).
cnf(c_2300,plain,
h4(e13) != op2(e22,e20),
inference(paramod,[status(thm)],[c_1822,c_393]) ).
cnf(c_2301,plain,
h3(e10) != op2(e22,e20),
inference(paramod,[status(thm)],[c_1981,c_2300]) ).
cnf(c_2302,plain,
e20 != op2(e22,e20),
inference(paramod,[status(thm)],[c_1990,c_2301]) ).
cnf(c_2002,plain,
op2(e22,e20) != e20,
inference(copy,[status(thm)],[c_2302]) ).
cnf(c_2303,plain,
op2(h4(e13),e23) = op2(e22,op2(e21,e23)),
inference(paramod,[status(thm)],[c_1822,c_185]) ).
cnf(c_2304,plain,
op2(h3(e10),e23) = op2(e22,op2(e21,e23)),
inference(paramod,[status(thm)],[c_1981,c_2303]) ).
cnf(c_2305,plain,
op2(e20,e23) = op2(e22,op2(e21,e23)),
inference(paramod,[status(thm)],[c_1990,c_2304]) ).
cnf(c_2004,plain,
op2(e20,e23) = h2(e13),
inference(paramod,[status(thm)],[c_1863,c_2305]) ).
cnf(c_2306,plain,
op2(e22,h3(e10)) = op2(e23,e21),
inference(paramod,[status(thm)],[c_1981,c_1823]) ).
cnf(c_2307,plain,
op2(e22,e20) = op2(e23,e21),
inference(paramod,[status(thm)],[c_1990,c_2306]) ).
cnf(c_2308,plain,
op2(e22,e20) = op2(e21,e23),
inference(paramod,[status(thm)],[c_1862,c_2307]) ).
cnf(c_2012,plain,
op2(e21,e23) = op2(e22,e20),
inference(copy,[status(thm)],[c_2308]) ).
cnf(c_2309,plain,
( op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e23,e21) = e21
| op2(e21,e23) = e20 ),
inference(paramod,[status(thm)],[c_1862,c_143]) ).
cnf(c_2310,plain,
( op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e23,e21) = e21
| op2(e22,e20) = e20 ),
inference(paramod,[status(thm)],[c_2012,c_2309]) ).
cnf(c_2311,plain,
( op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e21,e23) = e21
| op2(e22,e20) = e20 ),
inference(paramod,[status(thm)],[c_1862,c_2310]) ).
cnf(c_2312,plain,
( op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 ),
inference(paramod,[status(thm)],[c_2012,c_2311]) ).
cnf(c_2313,plain,
( op2(e23,e21) = e23
| op2(e21,e23) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 ),
inference(paramod,[status(thm)],[c_1862,c_2312]) ).
cnf(c_2314,plain,
( op2(e23,e21) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 ),
inference(paramod,[status(thm)],[c_2012,c_2313]) ).
cnf(c_2315,plain,
( op2(e21,e23) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 ),
inference(paramod,[status(thm)],[c_1862,c_2314]) ).
cnf(c_2316,plain,
( op2(e22,e20) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 ),
inference(paramod,[status(thm)],[c_2012,c_2315]) ).
cnf(c_2317,plain,
( op2(e22,e20) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21 ),
inference(resolve,[status(thm)],[c_2002,c_2316]) ).
cnf(c_2318,plain,
( op2(e22,e20) = e23
| op2(e22,e20) = e22 ),
inference(resolve,[status(thm)],[c_1859,c_2317]) ).
cnf(c_2018,plain,
op2(e22,e20) = e22,
inference(resolve,[status(thm)],[c_1818,c_2318]) ).
cnf(c_2319,plain,
op1(e10,e13) = op1(e12,op1(e11,e13)),
inference(paramod,[status(thm)],[c_1878,c_84]) ).
cnf(c_2320,plain,
op1(e10,e13) = op1(e12,op1(e10,e12)),
inference(paramod,[status(thm)],[c_1955,c_2319]) ).
cnf(c_2321,plain,
op1(e10,e13) = op1(e12,op1(e12,e10)),
inference(paramod,[status(thm)],[c_1963,c_2320]) ).
cnf(c_2322,plain,
op1(e10,e13) = op1(e12,e12),
inference(paramod,[status(thm)],[c_1980,c_2321]) ).
cnf(c_2021,plain,
op1(e10,e13) = e13,
inference(paramod,[status(thm)],[c_464,c_2322]) ).
cnf(c_2323,plain,
op1(e10,e11) = op1(e12,op1(e11,e11)),
inference(paramod,[status(thm)],[c_1878,c_82]) ).
cnf(c_2324,plain,
op1(e10,e11) = op1(e12,op1(e10,e13)),
inference(paramod,[status(thm)],[c_1958,c_2323]) ).
cnf(c_2325,plain,
op1(e10,e11) = op1(e12,e13),
inference(paramod,[status(thm)],[c_2021,c_2324]) ).
cnf(c_2022,plain,
op1(e10,e11) = e11,
inference(paramod,[status(thm)],[c_1801,c_2325]) ).
cnf(c_2326,plain,
op1(e10,e10) = op1(e12,op1(e11,e10)),
inference(paramod,[status(thm)],[c_1878,c_81]) ).
cnf(c_2327,plain,
op1(e10,e10) = op1(e12,op1(e10,e11)),
inference(paramod,[status(thm)],[c_1965,c_2326]) ).
cnf(c_2328,plain,
op1(e10,e10) = op1(e12,e11),
inference(paramod,[status(thm)],[c_2022,c_2327]) ).
cnf(c_2023,plain,
op1(e10,e10) = e10,
inference(paramod,[status(thm)],[c_1878,c_2328]) ).
cnf(c_2329,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(e20,h3(e10)) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1990,c_1897]) ).
cnf(c_2330,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| op2(e20,e20) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_1990,c_2329]) ).
cnf(c_2331,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h1(e13) != h3(op1(e10,e10)) ),
inference(paramod,[status(thm)],[c_474,c_2330]) ).
cnf(c_2332,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h1(e13) != h3(e10) ),
inference(paramod,[status(thm)],[c_2023,c_2331]) ).
cnf(c_2333,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1990,c_2332]) ).
cnf(c_2334,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(e11) != op2(h3(e10),e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_2022,c_2333]) ).
cnf(c_2335,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| e21 != op2(h3(e10),e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1815,c_2334]) ).
cnf(c_2336,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1990,c_2335]) ).
cnf(c_2337,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e12,e10)) != op2(h3(e10),e22)
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1963,c_2336]) ).
cnf(c_2338,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(e12) != op2(h3(e10),e22)
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1980,c_2337]) ).
cnf(c_2339,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| e22 != op2(h3(e10),e22)
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_482,c_2338]) ).
cnf(c_2340,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| e22 != op2(e20,e22)
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1990,c_2339]) ).
cnf(c_2341,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| e22 != op2(e22,e20)
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1998,c_2340]) ).
cnf(c_2342,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_2018,c_2341]) ).
cnf(c_2343,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(e13) != op2(h3(e10),e23)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_2021,c_2342]) ).
cnf(c_2344,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| e23 != op2(h3(e10),e23)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_488,c_2343]) ).
cnf(c_2345,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| e23 != op2(e20,e23)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1990,c_2344]) ).
cnf(c_2346,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_2004,c_2345]) ).
cnf(c_2347,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e10,e11)) != op2(e21,h3(e10))
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1965,c_2346]) ).
cnf(c_2348,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| h3(e11) != op2(e21,h3(e10))
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_2022,c_2347]) ).
cnf(c_2349,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| e21 != op2(e21,h3(e10))
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1815,c_2348]) ).
cnf(c_2350,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| e21 != op2(e21,e20)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1990,c_2349]) ).
cnf(c_2351,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e11,e11)) != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1999,c_2350]) ).
cnf(c_2352,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(op1(e10,e13)) != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1958,c_2351]) ).
cnf(c_2353,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| h3(e13) != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_2021,c_2352]) ).
cnf(c_2354,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h4(e13) != h3(e10)
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_488,c_2353]) ).
cnf(c_2355,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h3(e10)
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1981,c_2354]) ).
cnf(c_2356,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| e20 != h3(e10)
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1990,c_2355]) ).
cnf(c_2357,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1990,c_2356]) ).
cnf(c_2358,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e10,e12)) != op2(e21,e23)
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1955,c_2357]) ).
cnf(c_2359,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e12,e10)) != op2(e21,e23)
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1963,c_2358]) ).
cnf(c_2360,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(e12) != op2(e21,e23)
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1980,c_2359]) ).
cnf(c_2361,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| e22 != op2(e21,e23)
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_482,c_2360]) ).
cnf(c_2362,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| e22 != op2(e22,e20)
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_2012,c_2361]) ).
cnf(c_2363,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_2018,c_2362]) ).
cnf(c_2364,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e12) != op2(e22,h3(e10))
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1980,c_2363]) ).
cnf(c_2365,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e22 != op2(e22,h3(e10))
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_482,c_2364]) ).
cnf(c_2366,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e22 != op2(e22,e20)
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1990,c_2365]) ).
cnf(c_2367,negated_conjecture,
( h3(e10) != e20
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e22 != e22
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_2018,c_2366]) ).
cnf(c_2368,negated_conjecture,
( h3(e10) != e20
| h3(op1(e11,e11)) != op2(e23,h3(e10))
| e22 != e22
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1956,c_2367]) ).
cnf(c_2369,negated_conjecture,
( h3(e10) != e20
| h3(op1(e10,e13)) != op2(e23,h3(e10))
| e22 != e22
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1958,c_2368]) ).
cnf(c_2370,negated_conjecture,
( h3(e10) != e20
| h3(e13) != op2(e23,h3(e10))
| e22 != e22
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_2021,c_2369]) ).
cnf(c_2371,negated_conjecture,
( h3(e10) != e20
| e23 != op2(e23,h3(e10))
| e22 != e22
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_488,c_2370]) ).
cnf(c_2372,negated_conjecture,
( h3(e10) != e20
| e23 != op2(e23,e20)
| e22 != e22
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1990,c_2371]) ).
cnf(c_2373,negated_conjecture,
( h3(e10) != e20
| e23 != h2(e13)
| e22 != e22
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1997,c_2372]) ).
cnf(c_2374,negated_conjecture,
( e20 != e20
| e23 != h2(e13)
| e22 != e22
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| e21 != op2(e20,e21)
| h1(e13) != e20 ),
inference(paramod,[status(thm)],[c_1990,c_2373]) ).
cnf(c_2375,negated_conjecture,
( e20 != e20
| e23 != h2(e13)
| e22 != e22
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| e23 != h2(e13)
| e22 != e22
| op2(e20,e21) != e21
| h1(e13) != e20 ),
inference(copy,[status(thm)],[c_2374]) ).
cnf(c_2376,negated_conjecture,
( e20 != e20
| e23 != h2(e13)
| e22 != e22
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| e21 != op2(e20,e21)
| h2(e13) != e23
| e22 != e22
| op2(e20,e21) != e21
| h1(e13) != e20 ),
inference(copy,[status(thm)],[c_2375]) ).
cnf(c_2377,negated_conjecture,
( e20 != e20
| e23 != h2(e13)
| e22 != e22
| e22 != e22
| e20 != e20
| e23 != h2(e13)
| op2(e20,e21) != e21
| h2(e13) != e23
| e22 != e22
| op2(e20,e21) != e21
| h1(e13) != e20 ),
inference(copy,[status(thm)],[c_2376]) ).
cnf(c_2378,negated_conjecture,
( e20 != e20
| e23 != h2(e13)
| e22 != e22
| e22 != e22
| e20 != e20
| h2(e13) != e23
| op2(e20,e21) != e21
| h2(e13) != e23
| e22 != e22
| op2(e20,e21) != e21
| h1(e13) != e20 ),
inference(copy,[status(thm)],[c_2377]) ).
cnf(c_2379,negated_conjecture,
( e20 != e20
| h2(e13) != e23
| e22 != e22
| e22 != e22
| e20 != e20
| h2(e13) != e23
| op2(e20,e21) != e21
| h2(e13) != e23
| e22 != e22
| op2(e20,e21) != e21
| h1(e13) != e20 ),
inference(copy,[status(thm)],[c_2378]) ).
cnf(c_2380,negated_conjecture,
( e20 != e20
| h2(e13) != e23
| e22 != e22
| e22 != e22
| e20 != e20
| h2(e13) != e23
| op2(e20,e21) != e21
| h2(e13) != e23
| op2(e20,e21) != e21
| h1(e13) != e20 ),
inference(copy,[status(thm)],[c_2379]) ).
cnf(c_2381,negated_conjecture,
( e20 != e20
| h2(e13) != e23
| e22 != e22
| e22 != e22
| h2(e13) != e23
| op2(e20,e21) != e21
| h2(e13) != e23
| op2(e20,e21) != e21
| h1(e13) != e20 ),
inference(copy,[status(thm)],[c_2380]) ).
cnf(c_2382,negated_conjecture,
( e20 != e20
| h2(e13) != e23
| e22 != e22
| h2(e13) != e23
| op2(e20,e21) != e21
| h2(e13) != e23
| op2(e20,e21) != e21
| h1(e13) != e20 ),
inference(copy,[status(thm)],[c_2381]) ).
cnf(c_2383,negated_conjecture,
( e20 != e20
| h2(e13) != e23
| h2(e13) != e23
| op2(e20,e21) != e21
| h2(e13) != e23
| op2(e20,e21) != e21
| h1(e13) != e20 ),
inference(copy,[status(thm)],[c_2382]) ).
cnf(c_2384,negated_conjecture,
( h2(e13) != e23
| h2(e13) != e23
| op2(e20,e21) != e21
| h2(e13) != e23
| op2(e20,e21) != e21
| h1(e13) != e20 ),
inference(copy,[status(thm)],[c_2383]) ).
cnf(c_2385,negated_conjecture,
( h2(e13) != e23
| h2(e13) != e23
| h2(e13) != e23
| op2(e20,e21) != e21
| h1(e13) != e20 ),
inference(copy,[status(thm)],[c_2384]) ).
cnf(c_2386,negated_conjecture,
( h2(e13) != e23
| h2(e13) != e23
| op2(e20,e21) != e21
| h1(e13) != e20 ),
inference(copy,[status(thm)],[c_2385]) ).
cnf(c_2078,negated_conjecture,
( h2(e13) != e23
| op2(e20,e21) != e21
| h1(e13) != e20 ),
inference(copy,[status(thm)],[c_2386]) ).
cnf(c_2387,plain,
op2(op2(e22,e20),e23) = op2(e21,h4(e13)),
inference(paramod,[status(thm)],[c_2012,c_1875]) ).
cnf(c_2388,plain,
op2(e22,e23) = op2(e21,h4(e13)),
inference(paramod,[status(thm)],[c_2018,c_2387]) ).
cnf(c_2389,plain,
e21 = op2(e21,h4(e13)),
inference(paramod,[status(thm)],[c_1991,c_2388]) ).
cnf(c_2390,plain,
e21 = op2(e21,h3(e10)),
inference(paramod,[status(thm)],[c_1981,c_2389]) ).
cnf(c_2391,plain,
e21 = op2(e21,e20),
inference(paramod,[status(thm)],[c_1990,c_2390]) ).
cnf(c_2392,plain,
e21 = op2(e20,e21),
inference(paramod,[status(thm)],[c_1999,c_2391]) ).
cnf(c_2096,plain,
op2(e20,e21) = e21,
inference(copy,[status(thm)],[c_2392]) ).
cnf(c_2393,plain,
op2(e21,e22) = h3(e10),
inference(paramod,[status(thm)],[c_1981,c_1821]) ).
cnf(c_2100,plain,
op2(e21,e22) = e20,
inference(paramod,[status(thm)],[c_1990,c_2393]) ).
cnf(c_2394,plain,
op2(e22,e22) = op2(e23,e20),
inference(paramod,[status(thm)],[c_2018,c_1824]) ).
cnf(c_2395,plain,
e23 = op2(e23,e20),
inference(paramod,[status(thm)],[c_467,c_2394]) ).
cnf(c_2396,plain,
e23 = h2(e13),
inference(paramod,[status(thm)],[c_1997,c_2395]) ).
cnf(c_2107,plain,
h2(e13) = e23,
inference(copy,[status(thm)],[c_2396]) ).
cnf(c_2397,plain,
op2(e21,e22) = h1(e13),
inference(paramod,[status(thm)],[c_2018,c_2000]) ).
cnf(c_2398,plain,
e20 = h1(e13),
inference(paramod,[status(thm)],[c_2100,c_2397]) ).
cnf(c_2117,plain,
h1(e13) = e20,
inference(copy,[status(thm)],[c_2398]) ).
cnf(c_2399,negated_conjecture,
( h2(e13) != e23
| op2(e20,e21) != e21
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2117,c_2078]) ).
cnf(c_2400,negated_conjecture,
( h2(e13) != e23
| e21 != e21
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2096,c_2399]) ).
cnf(c_2401,negated_conjecture,
( e23 != e23
| e21 != e21
| e20 != e20 ),
inference(paramod,[status(thm)],[c_2107,c_2400]) ).
cnf(c_2402,negated_conjecture,
( e23 != e23
| e21 != e21 ),
inference(copy,[status(thm)],[c_2401]) ).
cnf(c_2403,negated_conjecture,
e23 != e23,
inference(copy,[status(thm)],[c_2402]) ).
cnf(c_2121,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_2403]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG016+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 20:59:16 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 20499 was started by sandbox on n010,
% 0.10/0.37 % Sat Sep 26 20:59:16 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 11.16/11.45
% 11.16/11.45 % From the command line: assign(max_seconds, 300).
% 11.21/11.81
% 11.21/11.81 % SZS status Theorem for theBenchmark
% 11.21/11.81
% 11.21/11.81 % Proof 1 at 0.30 (+ 0.03) seconds.
% 11.21/11.81 % Length of proof is 130.
% 11.21/11.81 % Level of proof is 14.
% 11.21/11.81 % Maximum clause weight is 157.000.
% 11.21/11.81 % Given clauses 0.
% 11.21/11.81
% 11.21/11.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------