%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG113+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 : Thu Sep 24 11:48:15 AM UTC 2026
% Result : Theorem 0.09s 0.53s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 98
% Number of leaves : 57
% Syntax : Number of formulae : 483 ( 201 unt; 36 def)
% Number of atoms : 4120 (3811 equ)
% Maximal formula atoms : 384 ( 8 avg)
% Number of connectives : 5964 (2327 ~;2637 |; 964 &)
% ( 36 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 6 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 38 ( 36 usr; 37 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
( ( op1(e13,e13) = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| op1(e10,e13) = e13 )
& ( op1(e13,e13) = e13
| op1(e13,e12) = e13
| op1(e13,e11) = e13
| op1(e13,e10) = e13 )
& ( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 )
& ( op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 )
& ( op1(e13,e13) = e11
| op1(e12,e13) = e11
| op1(e11,e13) = e11
| op1(e10,e13) = e11 )
& ( op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 )
& ( op1(e13,e13) = e10
| op1(e12,e13) = e10
| op1(e11,e13) = e10
| op1(e10,e13) = e10 )
& ( op1(e13,e13) = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 )
& ( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| op1(e10,e12) = e13 )
& ( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 )
& ( op1(e13,e12) = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 )
& ( op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 )
& ( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 )
& ( op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 )
& ( op1(e13,e12) = e10
| op1(e12,e12) = e10
| op1(e11,e12) = e10
| op1(e10,e12) = e10 )
& ( op1(e12,e13) = e10
| op1(e12,e12) = e10
| op1(e12,e11) = e10
| op1(e12,e10) = e10 )
& ( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| op1(e10,e11) = e13 )
& ( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e11) = e13
| op1(e11,e10) = e13 )
& ( op1(e13,e11) = e12
| op1(e12,e11) = e12
| op1(e11,e11) = e12
| op1(e10,e11) = e12 )
& ( op1(e11,e13) = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 )
& ( op1(e13,e11) = e11
| op1(e12,e11) = e11
| op1(e11,e11) = e11
| op1(e10,e11) = e11 )
& ( op1(e11,e13) = e11
| op1(e11,e12) = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 )
& ( op1(e13,e11) = e10
| op1(e12,e11) = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 )
& ( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 )
& ( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| op1(e10,e10) = e13 )
& ( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 )
& ( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| op1(e10,e10) = e12 )
& ( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 )
& ( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11
| op1(e10,e10) = e11 )
& ( op1(e10,e13) = e11
| op1(e10,e12) = e11
| op1(e10,e11) = e11
| op1(e10,e10) = e11 )
& ( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 )
& ( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
( op1(e13,e13) = e13
& op1(e12,e12) = e12
& op1(e11,e11) = e11
& op1(e10,e10) = e10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
( op2(e23,e23) = e23
& op2(e22,e22) = e22
& op2(e21,e21) = e21
& op2(e20,e20) = e20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
( e11 = op1(op1(e12,e13),e13)
& e10 = op1(e12,e13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
( e21 = op2(op2(e22,e23),e23)
& e20 = op2(e22,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
( h1(e11) = op2(op2(e20,e21),e21)
& h1(e10) = op2(e20,e21)
& h1(e13) = e21
& h1(e12) = e20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
( h2(e11) = op2(op2(e20,e22),e22)
& h2(e10) = op2(e20,e22)
& h2(e13) = e22
& h2(e12) = e20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
( h3(e11) = op2(op2(e20,e23),e23)
& h3(e10) = op2(e20,e23)
& h3(e13) = e23
& h3(e12) = e20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
( h4(e11) = op2(op2(e21,e20),e20)
& h4(e10) = op2(e21,e20)
& h4(e13) = e20
& h4(e12) = e21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
( h5(e11) = op2(op2(e21,e22),e22)
& h5(e10) = op2(e21,e22)
& h5(e13) = e22
& h5(e12) = e21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
( h6(e11) = op2(op2(e21,e23),e23)
& h6(e10) = op2(e21,e23)
& h6(e13) = e23
& h6(e12) = e21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
( h7(e11) = op2(op2(e22,e20),e20)
& h7(e10) = op2(e22,e20)
& h7(e13) = e20
& h7(e12) = e22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
( h8(e11) = op2(op2(e22,e21),e21)
& h8(e10) = op2(e22,e21)
& h8(e13) = e21
& h8(e12) = e22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( h10(e11) = op2(op2(e23,e20),e20)
& h10(e10) = op2(e23,e20)
& h10(e13) = e20
& h10(e12) = e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
( h11(e11) = op2(op2(e23,e21),e21)
& h11(e10) = op2(e23,e21)
& h11(e13) = e21
& h11(e12) = e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
( h12(e11) = op2(op2(e23,e22),e22)
& h12(e10) = op2(e23,e22)
& h12(e13) = e22
& h12(e12) = e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,conjecture,
( ( ( h12(e13) = e23
| h12(e12) = e23
| h12(e11) = e23
| h12(e10) = e23 )
& ( h12(e13) = e22
| h12(e12) = e22
| h12(e11) = e22
| h12(e10) = e22 )
& ( h12(e13) = e21
| h12(e12) = e21
| h12(e11) = e21
| h12(e10) = e21 )
& ( h12(e13) = e20
| h12(e12) = e20
| h12(e11) = e20
| h12(e10) = e20 )
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e10)) = op2(h12(e10),h12(e10)) )
| ( ( h11(e13) = e23
| h11(e12) = e23
| h11(e11) = e23
| h11(e10) = e23 )
& ( h11(e13) = e22
| h11(e12) = e22
| h11(e11) = e22
| h11(e10) = e22 )
& ( h11(e13) = e21
| h11(e12) = e21
| h11(e11) = e21
| h11(e10) = e21 )
& ( h11(e13) = e20
| h11(e12) = e20
| h11(e11) = e20
| h11(e10) = e20 )
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e10)) = op2(h11(e10),h11(e10)) )
| ( ( h10(e13) = e23
| h10(e12) = e23
| h10(e11) = e23
| h10(e10) = e23 )
& ( h10(e13) = e22
| h10(e12) = e22
| h10(e11) = e22
| h10(e10) = e22 )
& ( h10(e13) = e21
| h10(e12) = e21
| h10(e11) = e21
| h10(e10) = e21 )
& ( h10(e13) = e20
| h10(e12) = e20
| h10(e11) = e20
| h10(e10) = e20 )
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e10)) = op2(h10(e10),h10(e10)) )
| ( ( h9(e13) = e23
| h9(e12) = e23
| h9(e11) = e23
| h9(e10) = e23 )
& ( h9(e13) = e22
| h9(e12) = e22
| h9(e11) = e22
| h9(e10) = e22 )
& ( h9(e13) = e21
| h9(e12) = e21
| h9(e11) = e21
| h9(e10) = e21 )
& ( h9(e13) = e20
| h9(e12) = e20
| h9(e11) = e20
| h9(e10) = e20 )
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e10)) = op2(h9(e10),h9(e10)) )
| ( ( h8(e13) = e23
| h8(e12) = e23
| h8(e11) = e23
| h8(e10) = e23 )
& ( h8(e13) = e22
| h8(e12) = e22
| h8(e11) = e22
| h8(e10) = e22 )
& ( h8(e13) = e21
| h8(e12) = e21
| h8(e11) = e21
| h8(e10) = e21 )
& ( h8(e13) = e20
| h8(e12) = e20
| h8(e11) = e20
| h8(e10) = e20 )
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e10)) = op2(h8(e10),h8(e10)) )
| ( ( h7(e13) = e23
| h7(e12) = e23
| h7(e11) = e23
| h7(e10) = e23 )
& ( h7(e13) = e22
| h7(e12) = e22
| h7(e11) = e22
| h7(e10) = e22 )
& ( h7(e13) = e21
| h7(e12) = e21
| h7(e11) = e21
| h7(e10) = e21 )
& ( h7(e13) = e20
| h7(e12) = e20
| h7(e11) = e20
| h7(e10) = e20 )
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e10)) = op2(h7(e10),h7(e10)) )
| ( ( h6(e13) = e23
| h6(e12) = e23
| h6(e11) = e23
| h6(e10) = e23 )
& ( h6(e13) = e22
| h6(e12) = e22
| h6(e11) = e22
| h6(e10) = e22 )
& ( h6(e13) = e21
| h6(e12) = e21
| h6(e11) = e21
| h6(e10) = e21 )
& ( h6(e13) = e20
| h6(e12) = e20
| h6(e11) = e20
| h6(e10) = e20 )
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e10)) = op2(h6(e10),h6(e10)) )
| ( ( h5(e13) = e23
| h5(e12) = e23
| h5(e11) = e23
| h5(e10) = e23 )
& ( h5(e13) = e22
| h5(e12) = e22
| h5(e11) = e22
| h5(e10) = e22 )
& ( h5(e13) = e21
| h5(e12) = e21
| h5(e11) = e21
| h5(e10) = e21 )
& ( h5(e13) = e20
| h5(e12) = e20
| h5(e11) = e20
| h5(e10) = e20 )
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e10)) = op2(h5(e10),h5(e10)) )
| ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
~ ( ( ( h12(e13) = e23
| h12(e12) = e23
| h12(e11) = e23
| h12(e10) = e23 )
& ( h12(e13) = e22
| h12(e12) = e22
| h12(e11) = e22
| h12(e10) = e22 )
& ( h12(e13) = e21
| h12(e12) = e21
| h12(e11) = e21
| h12(e10) = e21 )
& ( h12(e13) = e20
| h12(e12) = e20
| h12(e11) = e20
| h12(e10) = e20 )
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e10)) = op2(h12(e10),h12(e10)) )
| ( ( h11(e13) = e23
| h11(e12) = e23
| h11(e11) = e23
| h11(e10) = e23 )
& ( h11(e13) = e22
| h11(e12) = e22
| h11(e11) = e22
| h11(e10) = e22 )
& ( h11(e13) = e21
| h11(e12) = e21
| h11(e11) = e21
| h11(e10) = e21 )
& ( h11(e13) = e20
| h11(e12) = e20
| h11(e11) = e20
| h11(e10) = e20 )
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e10)) = op2(h11(e10),h11(e10)) )
| ( ( h10(e13) = e23
| h10(e12) = e23
| h10(e11) = e23
| h10(e10) = e23 )
& ( h10(e13) = e22
| h10(e12) = e22
| h10(e11) = e22
| h10(e10) = e22 )
& ( h10(e13) = e21
| h10(e12) = e21
| h10(e11) = e21
| h10(e10) = e21 )
& ( h10(e13) = e20
| h10(e12) = e20
| h10(e11) = e20
| h10(e10) = e20 )
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e10)) = op2(h10(e10),h10(e10)) )
| ( ( h9(e13) = e23
| h9(e12) = e23
| h9(e11) = e23
| h9(e10) = e23 )
& ( h9(e13) = e22
| h9(e12) = e22
| h9(e11) = e22
| h9(e10) = e22 )
& ( h9(e13) = e21
| h9(e12) = e21
| h9(e11) = e21
| h9(e10) = e21 )
& ( h9(e13) = e20
| h9(e12) = e20
| h9(e11) = e20
| h9(e10) = e20 )
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e10)) = op2(h9(e10),h9(e10)) )
| ( ( h8(e13) = e23
| h8(e12) = e23
| h8(e11) = e23
| h8(e10) = e23 )
& ( h8(e13) = e22
| h8(e12) = e22
| h8(e11) = e22
| h8(e10) = e22 )
& ( h8(e13) = e21
| h8(e12) = e21
| h8(e11) = e21
| h8(e10) = e21 )
& ( h8(e13) = e20
| h8(e12) = e20
| h8(e11) = e20
| h8(e10) = e20 )
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e10)) = op2(h8(e10),h8(e10)) )
| ( ( h7(e13) = e23
| h7(e12) = e23
| h7(e11) = e23
| h7(e10) = e23 )
& ( h7(e13) = e22
| h7(e12) = e22
| h7(e11) = e22
| h7(e10) = e22 )
& ( h7(e13) = e21
| h7(e12) = e21
| h7(e11) = e21
| h7(e10) = e21 )
& ( h7(e13) = e20
| h7(e12) = e20
| h7(e11) = e20
| h7(e10) = e20 )
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e10)) = op2(h7(e10),h7(e10)) )
| ( ( h6(e13) = e23
| h6(e12) = e23
| h6(e11) = e23
| h6(e10) = e23 )
& ( h6(e13) = e22
| h6(e12) = e22
| h6(e11) = e22
| h6(e10) = e22 )
& ( h6(e13) = e21
| h6(e12) = e21
| h6(e11) = e21
| h6(e10) = e21 )
& ( h6(e13) = e20
| h6(e12) = e20
| h6(e11) = e20
| h6(e10) = e20 )
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e10)) = op2(h6(e10),h6(e10)) )
| ( ( h5(e13) = e23
| h5(e12) = e23
| h5(e11) = e23
| h5(e10) = e23 )
& ( h5(e13) = e22
| h5(e12) = e22
| h5(e11) = e22
| h5(e10) = e22 )
& ( h5(e13) = e21
| h5(e12) = e21
| h5(e11) = e21
| h5(e10) = e21 )
& ( h5(e13) = e20
| h5(e12) = e20
| h5(e11) = e20
| h5(e10) = e20 )
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e10)) = op2(h5(e10),h5(e10)) )
| ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f47,plain,
( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11
| op1(e10,e10) = e11 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f48,plain,
( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f50,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f52,plain,
( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f58,plain,
( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e11) = e13
| op1(e11,e10) = e13 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f63,plain,
( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f66,plain,
( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f68,plain,
( op1(e13,e13) = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f72,plain,
( op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f73,plain,
( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f77,plain,
( op2(e20,e21) = e23
| op2(e20,e21) = e22
| op2(e20,e21) = e21
| op2(e20,e21) = e20 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f78,plain,
( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| op2(e20,e22) = e20 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f80,plain,
( op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e21
| op2(e21,e20) = e20 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f82,plain,
( op2(e21,e22) = e23
| op2(e21,e22) = e22
| op2(e21,e22) = e21
| op2(e21,e22) = e20 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f83,plain,
( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| op2(e21,e23) = e20 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f84,plain,
( op2(e22,e20) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f85,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f88,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f89,plain,
( op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e23,e21) = e21
| op2(e23,e21) = e20 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f90,plain,
( op2(e23,e22) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21
| op2(e23,e22) = e20 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f124,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f126,plain,
op1(e10,e10) != op1(e13,e10),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f127,plain,
op1(e11,e10) != op1(e12,e10),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f137,plain,
op1(e10,e12) != op1(e12,e12),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f141,plain,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f144,plain,
op1(e10,e13) != op1(e13,e13),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f146,plain,
op1(e11,e13) != op1(e13,e13),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f153,plain,
op1(e10,e12) != op1(e10,e13),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f154,plain,
op1(e11,e10) != op1(e11,e11),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f157,plain,
op1(e11,e11) != op1(e11,e12),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f172,plain,
op2(e20,e20) != op2(e21,e20),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f173,plain,
op2(e20,e20) != op2(e22,e20),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f174,plain,
op2(e20,e20) != op2(e23,e20),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f175,plain,
op2(e21,e20) != op2(e22,e20),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f177,plain,
op2(e22,e20) != op2(e23,e20),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f178,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f180,plain,
op2(e20,e21) != op2(e23,e21),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f181,plain,
op2(e21,e21) != op2(e22,e21),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f182,plain,
op2(e21,e21) != op2(e23,e21),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f184,plain,
op2(e20,e22) != op2(e21,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f185,plain,
op2(e20,e22) != op2(e22,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f187,plain,
op2(e21,e22) != op2(e22,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f188,plain,
op2(e21,e22) != op2(e23,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f189,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f193,plain,
op2(e21,e23) != op2(e22,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f194,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f196,plain,
op2(e20,e20) != op2(e20,e21),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f197,plain,
op2(e20,e20) != op2(e20,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f199,plain,
op2(e20,e21) != op2(e20,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f201,plain,
op2(e20,e22) != op2(e20,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f202,plain,
op2(e21,e20) != op2(e21,e21),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f204,plain,
op2(e21,e20) != op2(e21,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f205,plain,
op2(e21,e21) != op2(e21,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f206,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f209,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f211,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f212,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f216,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f218,plain,
op2(e23,e21) != op2(e23,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f219,plain,
op2(e23,e22) != op2(e23,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f220,plain,
e10 != e11,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f221,plain,
e10 != e12,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f222,plain,
e10 != e13,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f223,plain,
e11 != e12,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f224,plain,
e11 != e13,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f225,plain,
e12 != e13,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f248,plain,
op1(e10,e10) = e10,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f249,plain,
op1(e11,e11) = e11,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f250,plain,
op1(e12,e12) = e12,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f251,plain,
op1(e13,e13) = e13,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f252,plain,
op2(e20,e20) = e20,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f253,plain,
op2(e21,e21) = e21,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f254,plain,
op2(e22,e22) = e22,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f255,plain,
op2(e23,e23) = e23,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f256,plain,
e10 = op1(e12,e13),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f257,plain,
e11 = op1(op1(e12,e13),e13),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f258,plain,
e20 = op2(e22,e23),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f259,plain,
e21 = op2(op2(e22,e23),e23),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f262,plain,
h1(e10) = op2(e20,e21),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f263,plain,
h1(e11) = op2(op2(e20,e21),e21),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f266,plain,
h2(e10) = op2(e20,e22),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f267,plain,
h2(e11) = op2(op2(e20,e22),e22),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f268,plain,
h3(e12) = e20,
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f269,plain,
h3(e13) = e23,
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f270,plain,
h3(e10) = op2(e20,e23),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f271,plain,
h3(e11) = op2(op2(e20,e23),e23),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f274,plain,
h4(e10) = op2(e21,e20),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f278,plain,
h5(e10) = op2(e21,e22),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f282,plain,
h6(e10) = op2(e21,e23),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f286,plain,
h7(e10) = op2(e22,e20),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f290,plain,
h8(e10) = op2(e22,e21),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f298,plain,
h10(e10) = op2(e23,e20),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f302,plain,
h11(e10) = op2(e23,e21),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f306,plain,
h12(e10) = op2(e23,e22),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f308,plain,
( ( ( h12(e13) != e23
& h12(e12) != e23
& h12(e11) != e23
& h12(e10) != e23 )
| ( h12(e13) != e22
& h12(e12) != e22
& h12(e11) != e22
& h12(e10) != e22 )
| ( h12(e13) != e21
& h12(e12) != e21
& h12(e11) != e21
& h12(e10) != e21 )
| ( h12(e13) != e20
& h12(e12) != e20
& h12(e11) != e20
& h12(e10) != e20 )
| h12(op1(e13,e13)) != op2(h12(e13),h12(e13))
| h12(op1(e13,e12)) != op2(h12(e13),h12(e12))
| h12(op1(e13,e11)) != op2(h12(e13),h12(e11))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e12,e13)) != op2(h12(e12),h12(e13))
| h12(op1(e12,e12)) != op2(h12(e12),h12(e12))
| h12(op1(e12,e11)) != op2(h12(e12),h12(e11))
| h12(op1(e12,e10)) != op2(h12(e12),h12(e10))
| h12(op1(e11,e13)) != op2(h12(e11),h12(e13))
| h12(op1(e11,e12)) != op2(h12(e11),h12(e12))
| h12(op1(e11,e11)) != op2(h12(e11),h12(e11))
| h12(op1(e11,e10)) != op2(h12(e11),h12(e10))
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e10,e12)) != op2(h12(e10),h12(e12))
| h12(op1(e10,e11)) != op2(h12(e10),h12(e11))
| h12(op1(e10,e10)) != op2(h12(e10),h12(e10)) )
& ( ( h11(e13) != e23
& h11(e12) != e23
& h11(e11) != e23
& h11(e10) != e23 )
| ( h11(e13) != e22
& h11(e12) != e22
& h11(e11) != e22
& h11(e10) != e22 )
| ( h11(e13) != e21
& h11(e12) != e21
& h11(e11) != e21
& h11(e10) != e21 )
| ( h11(e13) != e20
& h11(e12) != e20
& h11(e11) != e20
& h11(e10) != e20 )
| h11(op1(e13,e13)) != op2(h11(e13),h11(e13))
| h11(op1(e13,e12)) != op2(h11(e13),h11(e12))
| h11(op1(e13,e11)) != op2(h11(e13),h11(e11))
| h11(op1(e13,e10)) != op2(h11(e13),h11(e10))
| h11(op1(e12,e13)) != op2(h11(e12),h11(e13))
| h11(op1(e12,e12)) != op2(h11(e12),h11(e12))
| h11(op1(e12,e11)) != op2(h11(e12),h11(e11))
| h11(op1(e12,e10)) != op2(h11(e12),h11(e10))
| h11(op1(e11,e13)) != op2(h11(e11),h11(e13))
| h11(op1(e11,e12)) != op2(h11(e11),h11(e12))
| h11(op1(e11,e11)) != op2(h11(e11),h11(e11))
| h11(op1(e11,e10)) != op2(h11(e11),h11(e10))
| h11(op1(e10,e13)) != op2(h11(e10),h11(e13))
| h11(op1(e10,e12)) != op2(h11(e10),h11(e12))
| h11(op1(e10,e11)) != op2(h11(e10),h11(e11))
| h11(op1(e10,e10)) != op2(h11(e10),h11(e10)) )
& ( ( h10(e13) != e23
& h10(e12) != e23
& h10(e11) != e23
& h10(e10) != e23 )
| ( h10(e13) != e22
& h10(e12) != e22
& h10(e11) != e22
& h10(e10) != e22 )
| ( h10(e13) != e21
& h10(e12) != e21
& h10(e11) != e21
& h10(e10) != e21 )
| ( h10(e13) != e20
& h10(e12) != e20
& h10(e11) != e20
& h10(e10) != e20 )
| h10(op1(e13,e13)) != op2(h10(e13),h10(e13))
| h10(op1(e13,e12)) != op2(h10(e13),h10(e12))
| h10(op1(e13,e11)) != op2(h10(e13),h10(e11))
| h10(op1(e13,e10)) != op2(h10(e13),h10(e10))
| h10(op1(e12,e13)) != op2(h10(e12),h10(e13))
| h10(op1(e12,e12)) != op2(h10(e12),h10(e12))
| h10(op1(e12,e11)) != op2(h10(e12),h10(e11))
| h10(op1(e12,e10)) != op2(h10(e12),h10(e10))
| h10(op1(e11,e13)) != op2(h10(e11),h10(e13))
| h10(op1(e11,e12)) != op2(h10(e11),h10(e12))
| h10(op1(e11,e11)) != op2(h10(e11),h10(e11))
| h10(op1(e11,e10)) != op2(h10(e11),h10(e10))
| h10(op1(e10,e13)) != op2(h10(e10),h10(e13))
| h10(op1(e10,e12)) != op2(h10(e10),h10(e12))
| h10(op1(e10,e11)) != op2(h10(e10),h10(e11))
| h10(op1(e10,e10)) != op2(h10(e10),h10(e10)) )
& ( ( h9(e13) != e23
& h9(e12) != e23
& h9(e11) != e23
& h9(e10) != e23 )
| ( h9(e13) != e22
& h9(e12) != e22
& h9(e11) != e22
& h9(e10) != e22 )
| ( h9(e13) != e21
& h9(e12) != e21
& h9(e11) != e21
& h9(e10) != e21 )
| ( h9(e13) != e20
& h9(e12) != e20
& h9(e11) != e20
& h9(e10) != e20 )
| h9(op1(e13,e13)) != op2(h9(e13),h9(e13))
| h9(op1(e13,e12)) != op2(h9(e13),h9(e12))
| h9(op1(e13,e11)) != op2(h9(e13),h9(e11))
| h9(op1(e13,e10)) != op2(h9(e13),h9(e10))
| h9(op1(e12,e13)) != op2(h9(e12),h9(e13))
| h9(op1(e12,e12)) != op2(h9(e12),h9(e12))
| h9(op1(e12,e11)) != op2(h9(e12),h9(e11))
| h9(op1(e12,e10)) != op2(h9(e12),h9(e10))
| h9(op1(e11,e13)) != op2(h9(e11),h9(e13))
| h9(op1(e11,e12)) != op2(h9(e11),h9(e12))
| h9(op1(e11,e11)) != op2(h9(e11),h9(e11))
| h9(op1(e11,e10)) != op2(h9(e11),h9(e10))
| h9(op1(e10,e13)) != op2(h9(e10),h9(e13))
| h9(op1(e10,e12)) != op2(h9(e10),h9(e12))
| h9(op1(e10,e11)) != op2(h9(e10),h9(e11))
| h9(op1(e10,e10)) != op2(h9(e10),h9(e10)) )
& ( ( h8(e13) != e23
& h8(e12) != e23
& h8(e11) != e23
& h8(e10) != e23 )
| ( h8(e13) != e22
& h8(e12) != e22
& h8(e11) != e22
& h8(e10) != e22 )
| ( h8(e13) != e21
& h8(e12) != e21
& h8(e11) != e21
& h8(e10) != e21 )
| ( h8(e13) != e20
& h8(e12) != e20
& h8(e11) != e20
& h8(e10) != e20 )
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| h8(op1(e11,e10)) != op2(h8(e11),h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),h8(e12))
| h8(op1(e10,e11)) != op2(h8(e10),h8(e11))
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) )
& ( ( h7(e13) != e23
& h7(e12) != e23
& h7(e11) != e23
& h7(e10) != e23 )
| ( h7(e13) != e22
& h7(e12) != e22
& h7(e11) != e22
& h7(e10) != e22 )
| ( h7(e13) != e21
& h7(e12) != e21
& h7(e11) != e21
& h7(e10) != e21 )
| ( h7(e13) != e20
& h7(e12) != e20
& h7(e11) != e20
& h7(e10) != e20 )
| h7(op1(e13,e13)) != op2(h7(e13),h7(e13))
| h7(op1(e13,e12)) != op2(h7(e13),h7(e12))
| h7(op1(e13,e11)) != op2(h7(e13),h7(e11))
| h7(op1(e13,e10)) != op2(h7(e13),h7(e10))
| h7(op1(e12,e13)) != op2(h7(e12),h7(e13))
| h7(op1(e12,e12)) != op2(h7(e12),h7(e12))
| h7(op1(e12,e11)) != op2(h7(e12),h7(e11))
| h7(op1(e12,e10)) != op2(h7(e12),h7(e10))
| h7(op1(e11,e13)) != op2(h7(e11),h7(e13))
| h7(op1(e11,e12)) != op2(h7(e11),h7(e12))
| h7(op1(e11,e11)) != op2(h7(e11),h7(e11))
| h7(op1(e11,e10)) != op2(h7(e11),h7(e10))
| h7(op1(e10,e13)) != op2(h7(e10),h7(e13))
| h7(op1(e10,e12)) != op2(h7(e10),h7(e12))
| h7(op1(e10,e11)) != op2(h7(e10),h7(e11))
| h7(op1(e10,e10)) != op2(h7(e10),h7(e10)) )
& ( ( h6(e13) != e23
& h6(e12) != e23
& h6(e11) != e23
& h6(e10) != e23 )
| ( h6(e13) != e22
& h6(e12) != e22
& h6(e11) != e22
& h6(e10) != e22 )
| ( h6(e13) != e21
& h6(e12) != e21
& h6(e11) != e21
& h6(e10) != e21 )
| ( h6(e13) != e20
& h6(e12) != e20
& h6(e11) != e20
& h6(e10) != e20 )
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e10,e12)) != op2(h6(e10),h6(e12))
| h6(op1(e10,e11)) != op2(h6(e10),h6(e11))
| h6(op1(e10,e10)) != op2(h6(e10),h6(e10)) )
& ( ( h5(e13) != e23
& h5(e12) != e23
& h5(e11) != e23
& h5(e10) != e23 )
| ( h5(e13) != e22
& h5(e12) != e22
& h5(e11) != e22
& h5(e10) != e22 )
| ( h5(e13) != e21
& h5(e12) != e21
& h5(e11) != e21
& h5(e10) != e21 )
| ( h5(e13) != e20
& h5(e12) != e20
& h5(e11) != e20
& h5(e10) != e20 )
| h5(op1(e13,e13)) != op2(h5(e13),h5(e13))
| h5(op1(e13,e12)) != op2(h5(e13),h5(e12))
| h5(op1(e13,e11)) != op2(h5(e13),h5(e11))
| h5(op1(e13,e10)) != op2(h5(e13),h5(e10))
| h5(op1(e12,e13)) != op2(h5(e12),h5(e13))
| h5(op1(e12,e12)) != op2(h5(e12),h5(e12))
| h5(op1(e12,e11)) != op2(h5(e12),h5(e11))
| h5(op1(e12,e10)) != op2(h5(e12),h5(e10))
| h5(op1(e11,e13)) != op2(h5(e11),h5(e13))
| h5(op1(e11,e12)) != op2(h5(e11),h5(e12))
| h5(op1(e11,e11)) != op2(h5(e11),h5(e11))
| h5(op1(e11,e10)) != op2(h5(e11),h5(e10))
| h5(op1(e10,e13)) != op2(h5(e10),h5(e13))
| h5(op1(e10,e12)) != op2(h5(e10),h5(e12))
| h5(op1(e10,e11)) != op2(h5(e10),h5(e11))
| h5(op1(e10,e10)) != op2(h5(e10),h5(e10)) )
& ( ( h4(e13) != e23
& h4(e12) != e23
& h4(e11) != e23
& h4(e10) != e23 )
| ( h4(e13) != e22
& h4(e12) != e22
& h4(e11) != e22
& h4(e10) != e22 )
| ( h4(e13) != e21
& h4(e12) != e21
& h4(e11) != e21
& h4(e10) != e21 )
| ( h4(e13) != e20
& h4(e12) != e20
& h4(e11) != e20
& h4(e10) != e20 )
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e10)) != op2(h4(e10),h4(e10)) )
& ( ( h3(e13) != e23
& h3(e12) != e23
& h3(e11) != e23
& h3(e10) != e23 )
| ( h3(e13) != e22
& h3(e12) != e22
& h3(e11) != e22
& h3(e10) != e22 )
| ( h3(e13) != e21
& h3(e12) != e21
& h3(e11) != e21
& h3(e10) != e21 )
| ( h3(e13) != e20
& h3(e12) != e20
& h3(e11) != e20
& h3(e10) != e20 )
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) )
& ( ( h2(e13) != e23
& h2(e12) != e23
& h2(e11) != e23
& h2(e10) != e23 )
| ( h2(e13) != e22
& h2(e12) != e22
& h2(e11) != e22
& h2(e10) != e22 )
| ( h2(e13) != e21
& h2(e12) != e21
& h2(e11) != e21
& h2(e10) != e21 )
| ( h2(e13) != e20
& h2(e12) != e20
& h2(e11) != e20
& h2(e10) != e20 )
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) )
& ( ( h1(e13) != e23
& h1(e12) != e23
& h1(e11) != e23
& h1(e10) != e23 )
| ( h1(e13) != e22
& h1(e12) != e22
& h1(e11) != e22
& h1(e10) != e22 )
| ( h1(e13) != e21
& h1(e12) != e21
& h1(e11) != e21
& h1(e10) != e21 )
| ( h1(e13) != e20
& h1(e12) != e20
& h1(e11) != e20
& h1(e10) != e20 )
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e10)) != op2(h1(e10),h1(e10)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f309,definition,
( sP0_prd
<=> ( h1(e13) != e20
& h1(e12) != e20
& h1(e11) != e20
& h1(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f310,definition,
( sP1_prd
<=> ( h1(e13) != e21
& h1(e12) != e21
& h1(e11) != e21
& h1(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f311,definition,
( sP2_prd
<=> ( h1(e13) != e22
& h1(e12) != e22
& h1(e11) != e22
& h1(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f312,definition,
( sP3_prd
<=> ( h2(e13) != e20
& h2(e12) != e20
& h2(e11) != e20
& h2(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f313,definition,
( sP4_prd
<=> ( h2(e13) != e21
& h2(e12) != e21
& h2(e11) != e21
& h2(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f314,definition,
( sP5_prd
<=> ( h2(e13) != e22
& h2(e12) != e22
& h2(e11) != e22
& h2(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f315,definition,
( sP6_prd
<=> ( h3(e13) != e20
& h3(e12) != e20
& h3(e11) != e20
& h3(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f316,definition,
( sP7_prd
<=> ( h3(e13) != e21
& h3(e12) != e21
& h3(e11) != e21
& h3(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP7_prd])],[]) ).
fof(f317,definition,
( sP8_prd
<=> ( h3(e13) != e22
& h3(e12) != e22
& h3(e11) != e22
& h3(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP8_prd])],[]) ).
fof(f318,definition,
( sP9_prd
<=> ( h4(e13) != e20
& h4(e12) != e20
& h4(e11) != e20
& h4(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP9_prd])],[]) ).
fof(f319,definition,
( sP10_prd
<=> ( h4(e13) != e21
& h4(e12) != e21
& h4(e11) != e21
& h4(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP10_prd])],[]) ).
fof(f320,definition,
( sP11_prd
<=> ( h4(e13) != e22
& h4(e12) != e22
& h4(e11) != e22
& h4(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP11_prd])],[]) ).
fof(f321,definition,
( sP12_prd
<=> ( h5(e13) != e20
& h5(e12) != e20
& h5(e11) != e20
& h5(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP12_prd])],[]) ).
fof(f322,definition,
( sP13_prd
<=> ( h5(e13) != e21
& h5(e12) != e21
& h5(e11) != e21
& h5(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP13_prd])],[]) ).
fof(f323,definition,
( sP14_prd
<=> ( h5(e13) != e22
& h5(e12) != e22
& h5(e11) != e22
& h5(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP14_prd])],[]) ).
fof(f324,definition,
( sP15_prd
<=> ( h6(e13) != e20
& h6(e12) != e20
& h6(e11) != e20
& h6(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP15_prd])],[]) ).
fof(f325,definition,
( sP16_prd
<=> ( h6(e13) != e21
& h6(e12) != e21
& h6(e11) != e21
& h6(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP16_prd])],[]) ).
fof(f326,definition,
( sP17_prd
<=> ( h6(e13) != e22
& h6(e12) != e22
& h6(e11) != e22
& h6(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP17_prd])],[]) ).
fof(f327,definition,
( sP18_prd
<=> ( h7(e13) != e20
& h7(e12) != e20
& h7(e11) != e20
& h7(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP18_prd])],[]) ).
fof(f328,definition,
( sP19_prd
<=> ( h7(e13) != e21
& h7(e12) != e21
& h7(e11) != e21
& h7(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP19_prd])],[]) ).
fof(f329,definition,
( sP20_prd
<=> ( h7(e13) != e22
& h7(e12) != e22
& h7(e11) != e22
& h7(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP20_prd])],[]) ).
fof(f330,definition,
( sP21_prd
<=> ( h8(e13) != e20
& h8(e12) != e20
& h8(e11) != e20
& h8(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP21_prd])],[]) ).
fof(f331,definition,
( sP22_prd
<=> ( h8(e13) != e21
& h8(e12) != e21
& h8(e11) != e21
& h8(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP22_prd])],[]) ).
fof(f332,definition,
( sP23_prd
<=> ( h8(e13) != e22
& h8(e12) != e22
& h8(e11) != e22
& h8(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP23_prd])],[]) ).
fof(f333,definition,
( sP24_prd
<=> ( h9(e13) != e20
& h9(e12) != e20
& h9(e11) != e20
& h9(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP24_prd])],[]) ).
fof(f334,definition,
( sP25_prd
<=> ( h9(e13) != e21
& h9(e12) != e21
& h9(e11) != e21
& h9(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP25_prd])],[]) ).
fof(f335,definition,
( sP26_prd
<=> ( h9(e13) != e22
& h9(e12) != e22
& h9(e11) != e22
& h9(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP26_prd])],[]) ).
fof(f336,definition,
( sP27_prd
<=> ( h10(e13) != e20
& h10(e12) != e20
& h10(e11) != e20
& h10(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP27_prd])],[]) ).
fof(f337,definition,
( sP28_prd
<=> ( h10(e13) != e21
& h10(e12) != e21
& h10(e11) != e21
& h10(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP28_prd])],[]) ).
fof(f338,definition,
( sP29_prd
<=> ( h10(e13) != e22
& h10(e12) != e22
& h10(e11) != e22
& h10(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP29_prd])],[]) ).
fof(f339,definition,
( sP30_prd
<=> ( h11(e13) != e20
& h11(e12) != e20
& h11(e11) != e20
& h11(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP30_prd])],[]) ).
fof(f340,definition,
( sP31_prd
<=> ( h11(e13) != e21
& h11(e12) != e21
& h11(e11) != e21
& h11(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP31_prd])],[]) ).
fof(f341,definition,
( sP32_prd
<=> ( h11(e13) != e22
& h11(e12) != e22
& h11(e11) != e22
& h11(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP32_prd])],[]) ).
fof(f342,definition,
( sP33_prd
<=> ( h12(e13) != e20
& h12(e12) != e20
& h12(e11) != e20
& h12(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP33_prd])],[]) ).
fof(f343,definition,
( sP34_prd
<=> ( h12(e13) != e21
& h12(e12) != e21
& h12(e11) != e21
& h12(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP34_prd])],[]) ).
fof(f344,definition,
( sP35_prd
<=> ( h12(e13) != e22
& h12(e12) != e22
& h12(e11) != e22
& h12(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP35_prd])],[]) ).
fof(f345,plain,
( ( ( h12(e13) != e23
& h12(e12) != e23
& h12(e11) != e23
& h12(e10) != e23 )
| sP35_prd
| sP34_prd
| sP33_prd
| h12(op1(e13,e13)) != op2(h12(e13),h12(e13))
| h12(op1(e13,e12)) != op2(h12(e13),h12(e12))
| h12(op1(e13,e11)) != op2(h12(e13),h12(e11))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e12,e13)) != op2(h12(e12),h12(e13))
| h12(op1(e12,e12)) != op2(h12(e12),h12(e12))
| h12(op1(e12,e11)) != op2(h12(e12),h12(e11))
| h12(op1(e12,e10)) != op2(h12(e12),h12(e10))
| h12(op1(e11,e13)) != op2(h12(e11),h12(e13))
| h12(op1(e11,e12)) != op2(h12(e11),h12(e12))
| h12(op1(e11,e11)) != op2(h12(e11),h12(e11))
| h12(op1(e11,e10)) != op2(h12(e11),h12(e10))
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e10,e12)) != op2(h12(e10),h12(e12))
| h12(op1(e10,e11)) != op2(h12(e10),h12(e11))
| h12(op1(e10,e10)) != op2(h12(e10),h12(e10)) )
& ( ( h11(e13) != e23
& h11(e12) != e23
& h11(e11) != e23
& h11(e10) != e23 )
| sP32_prd
| sP31_prd
| sP30_prd
| h11(op1(e13,e13)) != op2(h11(e13),h11(e13))
| h11(op1(e13,e12)) != op2(h11(e13),h11(e12))
| h11(op1(e13,e11)) != op2(h11(e13),h11(e11))
| h11(op1(e13,e10)) != op2(h11(e13),h11(e10))
| h11(op1(e12,e13)) != op2(h11(e12),h11(e13))
| h11(op1(e12,e12)) != op2(h11(e12),h11(e12))
| h11(op1(e12,e11)) != op2(h11(e12),h11(e11))
| h11(op1(e12,e10)) != op2(h11(e12),h11(e10))
| h11(op1(e11,e13)) != op2(h11(e11),h11(e13))
| h11(op1(e11,e12)) != op2(h11(e11),h11(e12))
| h11(op1(e11,e11)) != op2(h11(e11),h11(e11))
| h11(op1(e11,e10)) != op2(h11(e11),h11(e10))
| h11(op1(e10,e13)) != op2(h11(e10),h11(e13))
| h11(op1(e10,e12)) != op2(h11(e10),h11(e12))
| h11(op1(e10,e11)) != op2(h11(e10),h11(e11))
| h11(op1(e10,e10)) != op2(h11(e10),h11(e10)) )
& ( ( h10(e13) != e23
& h10(e12) != e23
& h10(e11) != e23
& h10(e10) != e23 )
| sP29_prd
| sP28_prd
| sP27_prd
| h10(op1(e13,e13)) != op2(h10(e13),h10(e13))
| h10(op1(e13,e12)) != op2(h10(e13),h10(e12))
| h10(op1(e13,e11)) != op2(h10(e13),h10(e11))
| h10(op1(e13,e10)) != op2(h10(e13),h10(e10))
| h10(op1(e12,e13)) != op2(h10(e12),h10(e13))
| h10(op1(e12,e12)) != op2(h10(e12),h10(e12))
| h10(op1(e12,e11)) != op2(h10(e12),h10(e11))
| h10(op1(e12,e10)) != op2(h10(e12),h10(e10))
| h10(op1(e11,e13)) != op2(h10(e11),h10(e13))
| h10(op1(e11,e12)) != op2(h10(e11),h10(e12))
| h10(op1(e11,e11)) != op2(h10(e11),h10(e11))
| h10(op1(e11,e10)) != op2(h10(e11),h10(e10))
| h10(op1(e10,e13)) != op2(h10(e10),h10(e13))
| h10(op1(e10,e12)) != op2(h10(e10),h10(e12))
| h10(op1(e10,e11)) != op2(h10(e10),h10(e11))
| h10(op1(e10,e10)) != op2(h10(e10),h10(e10)) )
& ( ( h9(e13) != e23
& h9(e12) != e23
& h9(e11) != e23
& h9(e10) != e23 )
| sP26_prd
| sP25_prd
| sP24_prd
| h9(op1(e13,e13)) != op2(h9(e13),h9(e13))
| h9(op1(e13,e12)) != op2(h9(e13),h9(e12))
| h9(op1(e13,e11)) != op2(h9(e13),h9(e11))
| h9(op1(e13,e10)) != op2(h9(e13),h9(e10))
| h9(op1(e12,e13)) != op2(h9(e12),h9(e13))
| h9(op1(e12,e12)) != op2(h9(e12),h9(e12))
| h9(op1(e12,e11)) != op2(h9(e12),h9(e11))
| h9(op1(e12,e10)) != op2(h9(e12),h9(e10))
| h9(op1(e11,e13)) != op2(h9(e11),h9(e13))
| h9(op1(e11,e12)) != op2(h9(e11),h9(e12))
| h9(op1(e11,e11)) != op2(h9(e11),h9(e11))
| h9(op1(e11,e10)) != op2(h9(e11),h9(e10))
| h9(op1(e10,e13)) != op2(h9(e10),h9(e13))
| h9(op1(e10,e12)) != op2(h9(e10),h9(e12))
| h9(op1(e10,e11)) != op2(h9(e10),h9(e11))
| h9(op1(e10,e10)) != op2(h9(e10),h9(e10)) )
& ( ( h8(e13) != e23
& h8(e12) != e23
& h8(e11) != e23
& h8(e10) != e23 )
| sP23_prd
| sP22_prd
| sP21_prd
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| h8(op1(e11,e10)) != op2(h8(e11),h8(e10))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e10,e12)) != op2(h8(e10),h8(e12))
| h8(op1(e10,e11)) != op2(h8(e10),h8(e11))
| h8(op1(e10,e10)) != op2(h8(e10),h8(e10)) )
& ( ( h7(e13) != e23
& h7(e12) != e23
& h7(e11) != e23
& h7(e10) != e23 )
| sP20_prd
| sP19_prd
| sP18_prd
| h7(op1(e13,e13)) != op2(h7(e13),h7(e13))
| h7(op1(e13,e12)) != op2(h7(e13),h7(e12))
| h7(op1(e13,e11)) != op2(h7(e13),h7(e11))
| h7(op1(e13,e10)) != op2(h7(e13),h7(e10))
| h7(op1(e12,e13)) != op2(h7(e12),h7(e13))
| h7(op1(e12,e12)) != op2(h7(e12),h7(e12))
| h7(op1(e12,e11)) != op2(h7(e12),h7(e11))
| h7(op1(e12,e10)) != op2(h7(e12),h7(e10))
| h7(op1(e11,e13)) != op2(h7(e11),h7(e13))
| h7(op1(e11,e12)) != op2(h7(e11),h7(e12))
| h7(op1(e11,e11)) != op2(h7(e11),h7(e11))
| h7(op1(e11,e10)) != op2(h7(e11),h7(e10))
| h7(op1(e10,e13)) != op2(h7(e10),h7(e13))
| h7(op1(e10,e12)) != op2(h7(e10),h7(e12))
| h7(op1(e10,e11)) != op2(h7(e10),h7(e11))
| h7(op1(e10,e10)) != op2(h7(e10),h7(e10)) )
& ( ( h6(e13) != e23
& h6(e12) != e23
& h6(e11) != e23
& h6(e10) != e23 )
| sP17_prd
| sP16_prd
| sP15_prd
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e10,e12)) != op2(h6(e10),h6(e12))
| h6(op1(e10,e11)) != op2(h6(e10),h6(e11))
| h6(op1(e10,e10)) != op2(h6(e10),h6(e10)) )
& ( ( h5(e13) != e23
& h5(e12) != e23
& h5(e11) != e23
& h5(e10) != e23 )
| sP14_prd
| sP13_prd
| sP12_prd
| h5(op1(e13,e13)) != op2(h5(e13),h5(e13))
| h5(op1(e13,e12)) != op2(h5(e13),h5(e12))
| h5(op1(e13,e11)) != op2(h5(e13),h5(e11))
| h5(op1(e13,e10)) != op2(h5(e13),h5(e10))
| h5(op1(e12,e13)) != op2(h5(e12),h5(e13))
| h5(op1(e12,e12)) != op2(h5(e12),h5(e12))
| h5(op1(e12,e11)) != op2(h5(e12),h5(e11))
| h5(op1(e12,e10)) != op2(h5(e12),h5(e10))
| h5(op1(e11,e13)) != op2(h5(e11),h5(e13))
| h5(op1(e11,e12)) != op2(h5(e11),h5(e12))
| h5(op1(e11,e11)) != op2(h5(e11),h5(e11))
| h5(op1(e11,e10)) != op2(h5(e11),h5(e10))
| h5(op1(e10,e13)) != op2(h5(e10),h5(e13))
| h5(op1(e10,e12)) != op2(h5(e10),h5(e12))
| h5(op1(e10,e11)) != op2(h5(e10),h5(e11))
| h5(op1(e10,e10)) != op2(h5(e10),h5(e10)) )
& ( ( h4(e13) != e23
& h4(e12) != e23
& h4(e11) != e23
& h4(e10) != e23 )
| sP11_prd
| sP10_prd
| sP9_prd
| 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 )
| sP8_prd
| sP7_prd
| sP6_prd
| 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 )
| sP5_prd
| sP4_prd
| sP3_prd
| 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 )
| sP2_prd
| sP1_prd
| sP0_prd
| 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(formula_renaming,[status(thm)],[f308,f344,f343,f342,f341,f340,f339,f338,f337,f336,f335,f334,f333,f332,f331,f330,f329,f328,f327,f326,f325,f324,f323,f322,f321,f320,f319,f318,f317,f316,f315,f314,f313,f312,f311,f310,f309]) ).
fof(f357,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(cnf_transformation,[status(thm)],[f345]) ).
fof(f430,plain,
( ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20
| sP6_prd )
& ( ( h3(e13) != e20
& h3(e12) != e20
& h3(e11) != e20
& h3(e10) != e20 )
| ~ sP6_prd ) ),
inference(NNF_transformation,[status(thm)],[f315]) ).
fof(f433,plain,
( h3(e12) != e20
| ~ sP6_prd ),
inference(cnf_transformation,[status(thm)],[f430]) ).
fof(f436,plain,
( ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21
| sP7_prd )
& ( ( h3(e13) != e21
& h3(e12) != e21
& h3(e11) != e21
& h3(e10) != e21 )
| ~ sP7_prd ) ),
inference(NNF_transformation,[status(thm)],[f316]) ).
fof(f437,plain,
( h3(e10) != e21
| ~ sP7_prd ),
inference(cnf_transformation,[status(thm)],[f436]) ).
fof(f442,plain,
( ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22
| sP8_prd )
& ( ( h3(e13) != e22
& h3(e12) != e22
& h3(e11) != e22
& h3(e10) != e22 )
| ~ sP8_prd ) ),
inference(NNF_transformation,[status(thm)],[f317]) ).
fof(f444,plain,
( h3(e11) != e22
| ~ sP8_prd ),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f711,plain,
( e20 != e20
| ~ sP6_prd ),
inference(forward_demodulation,[status(thm)],[f268,f433]) ).
fof(f712,plain,
~ sP6_prd,
inference(trivial_equality_resolution,[status(thm)],[f711]) ).
fof(f789,plain,
( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11
| e10 = e11 ),
inference(forward_demodulation,[status(thm)],[f248,f47]) ).
fof(f790,plain,
( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11 ),
inference(forward_subsumption_resolution,[status(thm)],[f789,f220]) ).
fof(f831,plain,
( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| e10 = e12 ),
inference(forward_demodulation,[status(thm)],[f248,f48]) ).
fof(f832,plain,
( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12 ),
inference(forward_subsumption_resolution,[status(thm)],[f831,f221]) ).
fof(f859,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| e10 = e13 ),
inference(forward_demodulation,[status(thm)],[f248,f50]) ).
fof(f860,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13 ),
inference(forward_subsumption_resolution,[status(thm)],[f859,f222]) ).
fof(f883,plain,
( op1(e11,e13) = e10
| op1(e11,e12) = e10
| e11 = e10
| op1(e11,e10) = e10 ),
inference(forward_demodulation,[status(thm)],[f249,f52]) ).
fof(f884,plain,
( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e10) = e10 ),
inference(forward_subsumption_resolution,[status(thm)],[f883,f220]) ).
fof(f1001,plain,
( op1(e11,e13) = e10
| op1(e11,e12) = e10 ),
inference(backward_subsumption_resolution,[status(thm)],[f884,f1003]) ).
fof(f1003,plain,
e10 != op1(e11,e10),
inference(forward_demodulation,[status(thm)],[f248,f124]) ).
fof(f1010,plain,
e10 != op1(e13,e10),
inference(forward_demodulation,[status(thm)],[f248,f126]) ).
fof(f1017,plain,
( op1(e11,e13) = e13
| op1(e11,e12) = e13
| e11 = e13
| op1(e11,e10) = e13 ),
inference(forward_demodulation,[status(thm)],[f249,f58]) ).
fof(f1018,plain,
( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e10) = e13 ),
inference(forward_subsumption_resolution,[status(thm)],[f1017,f224]) ).
fof(f1052,plain,
( op1(e10,e13) = e12
| op1(e10,e11) = e12 ),
inference(backward_subsumption_resolution,[status(thm)],[f832,f1054]) ).
fof(f1054,plain,
op1(e10,e12) != e12,
inference(forward_demodulation,[status(thm)],[f250,f137]) ).
fof(f1063,plain,
e12 != op1(e13,e12),
inference(forward_demodulation,[status(thm)],[f250,f141]) ).
fof(f1067,plain,
( op1(e10,e12) = e13
| op1(e10,e11) = e13 ),
inference(backward_subsumption_resolution,[status(thm)],[f860,f1068]) ).
fof(f1068,plain,
op1(e10,e13) != e13,
inference(forward_demodulation,[status(thm)],[f251,f144]) ).
fof(f1071,plain,
( op1(e11,e12) = e13
| op1(e11,e10) = e13 ),
inference(backward_subsumption_resolution,[status(thm)],[f1018,f1072]) ).
fof(f1072,plain,
op1(e11,e13) != e13,
inference(forward_demodulation,[status(thm)],[f251,f146]) ).
fof(f1154,plain,
( op1(e13,e10) = e11
| op1(e12,e10) = e11 ),
inference(backward_subsumption_resolution,[status(thm)],[f790,f1155]) ).
fof(f1155,plain,
op1(e11,e10) != e11,
inference(forward_demodulation,[status(thm)],[f249,f154]) ).
fof(f1156,plain,
e11 != op1(e11,e12),
inference(forward_demodulation,[status(thm)],[f249,f157]) ).
fof(f1160,plain,
( op1(e13,e12) = e11
| e12 = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 ),
inference(forward_demodulation,[status(thm)],[f250,f63]) ).
fof(f1161,plain,
( op1(e13,e12) = e11
| e12 = e11
| op1(e10,e12) = e11 ),
inference(forward_subsumption_resolution,[status(thm)],[f1160,f1156]) ).
fof(f1186,plain,
e20 != op2(e21,e20),
inference(forward_demodulation,[status(thm)],[f252,f172]) ).
fof(f1187,plain,
e20 != h4(e10),
inference(forward_demodulation,[status(thm)],[f274,f1186]) ).
fof(f1188,plain,
e20 != op2(e22,e20),
inference(forward_demodulation,[status(thm)],[f252,f173]) ).
fof(f1189,plain,
e20 != h7(e10),
inference(forward_demodulation,[status(thm)],[f286,f1188]) ).
fof(f1190,plain,
e20 != op2(e23,e20),
inference(forward_demodulation,[status(thm)],[f252,f174]) ).
fof(f1191,plain,
e20 != h10(e10),
inference(forward_demodulation,[status(thm)],[f298,f1190]) ).
fof(f1192,plain,
h4(e10) != op2(e22,e20),
inference(forward_demodulation,[status(thm)],[f274,f175]) ).
fof(f1193,plain,
h4(e10) != h7(e10),
inference(forward_demodulation,[status(thm)],[f286,f1192]) ).
fof(f1196,plain,
h7(e10) != op2(e23,e20),
inference(forward_demodulation,[status(thm)],[f286,f177]) ).
fof(f1197,plain,
h7(e10) != h10(e10),
inference(forward_demodulation,[status(thm)],[f298,f1196]) ).
fof(f1198,plain,
h1(e10) != op2(e21,e21),
inference(forward_demodulation,[status(thm)],[f262,f178]) ).
fof(f1199,plain,
h1(e10) != e21,
inference(forward_demodulation,[status(thm)],[f253,f1198]) ).
fof(f1200,plain,
( op1(e12,e13) = e13
| e12 = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 ),
inference(forward_demodulation,[status(thm)],[f250,f66]) ).
fof(f1201,plain,
( e10 = e13
| e12 = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 ),
inference(forward_demodulation,[status(thm)],[f256,f1200]) ).
fof(f1202,plain,
( e10 = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 ),
inference(forward_subsumption_resolution,[status(thm)],[f1201,f225]) ).
fof(f1274,plain,
h1(e10) != op2(e23,e21),
inference(forward_demodulation,[status(thm)],[f262,f180]) ).
fof(f1275,plain,
h1(e10) != h11(e10),
inference(forward_demodulation,[status(thm)],[f302,f1274]) ).
fof(f1276,plain,
e21 != op2(e22,e21),
inference(forward_demodulation,[status(thm)],[f253,f181]) ).
fof(f1277,plain,
e21 != h8(e10),
inference(forward_demodulation,[status(thm)],[f290,f1276]) ).
fof(f1278,plain,
e21 != op2(e23,e21),
inference(forward_demodulation,[status(thm)],[f253,f182]) ).
fof(f1279,plain,
e21 != h11(e10),
inference(forward_demodulation,[status(thm)],[f302,f1278]) ).
fof(f1282,plain,
h2(e10) != op2(e21,e22),
inference(forward_demodulation,[status(thm)],[f266,f184]) ).
fof(f1283,plain,
h2(e10) != h5(e10),
inference(forward_demodulation,[status(thm)],[f278,f1282]) ).
fof(f1284,plain,
h2(e10) != op2(e22,e22),
inference(forward_demodulation,[status(thm)],[f266,f185]) ).
fof(f1285,plain,
h2(e10) != e22,
inference(forward_demodulation,[status(thm)],[f254,f1284]) ).
fof(f1288,plain,
h5(e10) != op2(e22,e22),
inference(forward_demodulation,[status(thm)],[f278,f187]) ).
fof(f1289,plain,
h5(e10) != e22,
inference(forward_demodulation,[status(thm)],[f254,f1288]) ).
fof(f1290,plain,
h5(e10) != op2(e23,e22),
inference(forward_demodulation,[status(thm)],[f278,f188]) ).
fof(f1291,plain,
h5(e10) != h12(e10),
inference(forward_demodulation,[status(thm)],[f306,f1290]) ).
fof(f1292,plain,
e22 != op2(e23,e22),
inference(forward_demodulation,[status(thm)],[f254,f189]) ).
fof(f1293,plain,
e22 != h12(e10),
inference(forward_demodulation,[status(thm)],[f306,f1292]) ).
fof(f1296,plain,
( e13 = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 ),
inference(forward_demodulation,[status(thm)],[f251,f68]) ).
fof(f1297,plain,
( e13 = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10 ),
inference(forward_subsumption_resolution,[status(thm)],[f1296,f1010]) ).
fof(f1315,plain,
h6(e10) != op2(e22,e23),
inference(forward_demodulation,[status(thm)],[f282,f193]) ).
fof(f1317,plain,
h6(e10) != e20,
inference(forward_demodulation,[status(thm)],[f258,f1315]) ).
fof(f1322,plain,
h6(e10) != op2(e23,e23),
inference(forward_demodulation,[status(thm)],[f282,f194]) ).
fof(f1323,plain,
h6(e10) != e23,
inference(forward_demodulation,[status(thm)],[f255,f1322]) ).
fof(f1326,plain,
e20 != op2(e20,e21),
inference(forward_demodulation,[status(thm)],[f252,f196]) ).
fof(f1327,plain,
e20 != h1(e10),
inference(forward_demodulation,[status(thm)],[f262,f1326]) ).
fof(f1328,plain,
e20 != op2(e20,e22),
inference(forward_demodulation,[status(thm)],[f252,f197]) ).
fof(f1329,plain,
e20 != h2(e10),
inference(forward_demodulation,[status(thm)],[f266,f1328]) ).
fof(f1332,plain,
h1(e10) != op2(e20,e22),
inference(forward_demodulation,[status(thm)],[f262,f199]) ).
fof(f1333,plain,
h1(e10) != h2(e10),
inference(forward_demodulation,[status(thm)],[f266,f1332]) ).
fof(f1338,plain,
h2(e10) != op2(e20,e23),
inference(forward_demodulation,[status(thm)],[f266,f201]) ).
fof(f1339,plain,
h2(e10) != h3(e10),
inference(forward_demodulation,[status(thm)],[f270,f1338]) ).
fof(f1341,plain,
h4(e10) != op2(e21,e21),
inference(forward_demodulation,[status(thm)],[f274,f202]) ).
fof(f1342,plain,
h4(e10) != e21,
inference(forward_demodulation,[status(thm)],[f253,f1341]) ).
fof(f1345,plain,
h4(e10) != op2(e21,e23),
inference(forward_demodulation,[status(thm)],[f274,f204]) ).
fof(f1346,plain,
h4(e10) != h6(e10),
inference(forward_demodulation,[status(thm)],[f282,f1345]) ).
fof(f1347,plain,
e21 != op2(e21,e22),
inference(forward_demodulation,[status(thm)],[f253,f205]) ).
fof(f1348,plain,
e21 != h5(e10),
inference(forward_demodulation,[status(thm)],[f278,f1347]) ).
fof(f1349,plain,
e21 != op2(e21,e23),
inference(forward_demodulation,[status(thm)],[f253,f206]) ).
fof(f1350,plain,
e21 != h6(e10),
inference(forward_demodulation,[status(thm)],[f282,f1349]) ).
fof(f1376,plain,
( e13 = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 ),
inference(forward_demodulation,[status(thm)],[f251,f72]) ).
fof(f1377,plain,
( e13 = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 ),
inference(forward_subsumption_resolution,[status(thm)],[f1376,f1063]) ).
fof(f1451,plain,
h7(e10) != op2(e22,e22),
inference(forward_demodulation,[status(thm)],[f286,f209]) ).
fof(f1452,plain,
h7(e10) != e22,
inference(forward_demodulation,[status(thm)],[f254,f1451]) ).
fof(f1455,plain,
h8(e10) != op2(e22,e22),
inference(forward_demodulation,[status(thm)],[f290,f211]) ).
fof(f1456,plain,
h8(e10) != e22,
inference(forward_demodulation,[status(thm)],[f254,f1455]) ).
fof(f1457,plain,
h8(e10) != op2(e22,e23),
inference(forward_demodulation,[status(thm)],[f290,f212]) ).
fof(f1458,plain,
h8(e10) != e20,
inference(forward_demodulation,[status(thm)],[f258,f1457]) ).
fof(f1465,plain,
h10(e10) != op2(e23,e23),
inference(forward_demodulation,[status(thm)],[f298,f216]) ).
fof(f1466,plain,
h10(e10) != e23,
inference(forward_demodulation,[status(thm)],[f255,f1465]) ).
fof(f1469,plain,
h11(e10) != op2(e23,e23),
inference(forward_demodulation,[status(thm)],[f302,f218]) ).
fof(f1470,plain,
h11(e10) != e23,
inference(forward_demodulation,[status(thm)],[f255,f1469]) ).
fof(f1471,plain,
h12(e10) != op2(e23,e23),
inference(forward_demodulation,[status(thm)],[f306,f219]) ).
fof(f1472,plain,
h12(e10) != e23,
inference(forward_demodulation,[status(thm)],[f255,f1471]) ).
fof(f1473,plain,
( op1(e13,e13) = e12
| e10 = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(forward_demodulation,[status(thm)],[f256,f73]) ).
fof(f1474,plain,
( e13 = e12
| e10 = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(forward_demodulation,[status(thm)],[f251,f1473]) ).
fof(f1475,plain,
( e13 = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 ),
inference(forward_subsumption_resolution,[status(thm)],[f1474,f221]) ).
fof(f1483,plain,
( e13 = e12
| op1(e11,e13) = e12
| e11 = e12 ),
inference(backward_demodulation,[status(thm)],[f1491,f1475]) ).
fof(f1486,plain,
op1(e10,e12) != e11,
inference(backward_demodulation,[status(thm)],[f1491,f153]) ).
fof(f1491,plain,
e11 = op1(e10,e13),
inference(forward_demodulation,[status(thm)],[f256,f257]) ).
fof(f1492,plain,
( e13 = e12
| op1(e11,e13) = e12 ),
inference(forward_subsumption_resolution,[status(thm)],[f1483,f223]) ).
fof(f1493,plain,
( op1(e13,e12) = e11
| e12 = e11 ),
inference(backward_subsumption_resolution,[status(thm)],[f1161,f1486]) ).
fof(f1494,plain,
op1(e13,e12) = e11,
inference(forward_subsumption_resolution,[status(thm)],[f1493,f223]) ).
fof(f1496,plain,
( e13 = e10
| e11 = e10
| op1(e13,e11) = e10 ),
inference(backward_demodulation,[status(thm)],[f1494,f1297]) ).
fof(f1504,plain,
( e13 = e10
| op1(e13,e11) = e10 ),
inference(forward_subsumption_resolution,[status(thm)],[f1496,f220]) ).
fof(f1506,plain,
h3(e10) = e21,
inference(backward_demodulation,[status(thm)],[f1507,f270]) ).
fof(f1507,plain,
e21 = op2(e20,e23),
inference(forward_demodulation,[status(thm)],[f258,f259]) ).
fof(f1510,plain,
h2(e10) != e21,
inference(backward_demodulation,[status(thm)],[f1506,f1339]) ).
fof(f1519,plain,
( e21 != e21
| ~ sP7_prd ),
inference(backward_demodulation,[status(thm)],[f1506,f437]) ).
fof(f1521,plain,
~ sP7_prd,
inference(trivial_equality_resolution,[status(thm)],[f1519]) ).
fof(f1531,plain,
op1(e11,e13) = e12,
inference(forward_subsumption_resolution,[status(thm)],[f1492,f225]) ).
fof(f1532,plain,
( e13 = e12
| e10 = e12
| op1(e13,e10) = e12 ),
inference(backward_demodulation,[status(thm)],[f1538,f1377]) ).
fof(f1538,plain,
op1(e13,e11) = e10,
inference(forward_subsumption_resolution,[status(thm)],[f1504,f222]) ).
fof(f1539,plain,
( e13 = e12
| op1(e13,e10) = e12 ),
inference(forward_subsumption_resolution,[status(thm)],[f1532,f221]) ).
fof(f1548,plain,
op1(e13,e10) = e12,
inference(forward_subsumption_resolution,[status(thm)],[f1539,f225]) ).
fof(f1549,plain,
h1(e11) = op2(h1(e10),e21),
inference(forward_demodulation,[status(thm)],[f262,f263]) ).
fof(f1550,plain,
h2(e11) = op2(h2(e10),e22),
inference(forward_demodulation,[status(thm)],[f266,f267]) ).
fof(f1554,plain,
( op2(e20,e21) = e23
| op2(e20,e21) = e22
| op2(e20,e21) = e21
| h1(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f262,f77]) ).
fof(f1555,plain,
( op2(e20,e21) = e23
| op2(e20,e21) = e22
| h1(e10) = e21
| h1(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f262,f1554]) ).
fof(f1556,plain,
( op2(e20,e21) = e23
| h1(e10) = e22
| h1(e10) = e21
| h1(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f262,f1555]) ).
fof(f1557,plain,
( h1(e10) = e23
| h1(e10) = e22
| h1(e10) = e21
| h1(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f262,f1556]) ).
fof(f1558,plain,
( h1(e10) = e23
| h1(e10) = e22
| h1(e10) = e21 ),
inference(forward_subsumption_resolution,[status(thm)],[f1557,f1327]) ).
fof(f1626,plain,
h6(e10) = h3(e11),
inference(backward_demodulation,[status(thm)],[f1627,f282]) ).
fof(f1627,plain,
h3(e11) = op2(e21,e23),
inference(forward_demodulation,[status(thm)],[f1507,f271]) ).
fof(f1631,plain,
e21 != h3(e11),
inference(backward_demodulation,[status(thm)],[f1626,f1350]) ).
fof(f1632,plain,
h4(e10) != h3(e11),
inference(backward_demodulation,[status(thm)],[f1626,f1346]) ).
fof(f1633,plain,
h3(e11) != e23,
inference(backward_demodulation,[status(thm)],[f1626,f1323]) ).
fof(f1634,plain,
h3(e11) != e20,
inference(backward_demodulation,[status(thm)],[f1626,f1317]) ).
fof(f1653,plain,
( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| h2(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f266,f78]) ).
fof(f1654,plain,
( op2(e20,e22) = e23
| op2(e20,e22) = e22
| h2(e10) = e21
| h2(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f266,f1653]) ).
fof(f1655,plain,
( op2(e20,e22) = e23
| h2(e10) = e22
| h2(e10) = e21
| h2(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f266,f1654]) ).
fof(f1656,plain,
( h2(e10) = e23
| h2(e10) = e22
| h2(e10) = e21
| h2(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f266,f1655]) ).
fof(f1657,plain,
( h2(e10) = e23
| h2(e10) = e22
| h2(e10) = e21 ),
inference(forward_subsumption_resolution,[status(thm)],[f1656,f1329]) ).
fof(f1658,plain,
( h2(e10) = e23
| h2(e10) = e21 ),
inference(resolution,[status(thm)],[f1657,f1285]) ).
fof(f1666,plain,
h2(e10) = e23,
inference(forward_subsumption_resolution,[status(thm)],[f1658,f1510]) ).
fof(f1674,plain,
h2(e11) = op2(e23,e22),
inference(backward_demodulation,[status(thm)],[f1666,f1550]) ).
fof(f1676,plain,
h1(e10) != e23,
inference(backward_demodulation,[status(thm)],[f1666,f1333]) ).
fof(f1680,plain,
e23 != h5(e10),
inference(backward_demodulation,[status(thm)],[f1666,f1283]) ).
fof(f1681,plain,
e23 = op2(e20,e22),
inference(backward_demodulation,[status(thm)],[f1666,f266]) ).
fof(f1683,plain,
( h1(e10) = e22
| h1(e10) = e21 ),
inference(backward_subsumption_resolution,[status(thm)],[f1558,f1676]) ).
fof(f1684,plain,
h1(e10) = e22,
inference(forward_subsumption_resolution,[status(thm)],[f1683,f1199]) ).
fof(f1688,plain,
h1(e11) = op2(e22,e21),
inference(backward_demodulation,[status(thm)],[f1684,f1549]) ).
fof(f1690,plain,
e22 != h11(e10),
inference(backward_demodulation,[status(thm)],[f1684,f1275]) ).
fof(f1693,plain,
e22 = op2(e20,e21),
inference(backward_demodulation,[status(thm)],[f1684,f262]) ).
fof(f1694,plain,
h12(e10) = h2(e11),
inference(backward_demodulation,[status(thm)],[f1674,f306]) ).
fof(f1695,plain,
h2(e11) != e23,
inference(backward_demodulation,[status(thm)],[f1694,f1472]) ).
fof(f1698,plain,
e22 != h2(e11),
inference(backward_demodulation,[status(thm)],[f1694,f1293]) ).
fof(f1699,plain,
h5(e10) != h2(e11),
inference(backward_demodulation,[status(thm)],[f1694,f1291]) ).
fof(f1707,plain,
( op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e21
| h4(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f274,f80]) ).
fof(f1708,plain,
( op2(e21,e20) = e23
| op2(e21,e20) = e22
| h4(e10) = e21
| h4(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f274,f1707]) ).
fof(f1709,plain,
( op2(e21,e20) = e23
| h4(e10) = e22
| h4(e10) = e21
| h4(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f274,f1708]) ).
fof(f1710,plain,
( h4(e10) = e23
| h4(e10) = e22
| h4(e10) = e21
| h4(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f274,f1709]) ).
fof(f1711,plain,
( h4(e10) = e23
| h4(e10) = e22
| h4(e10) = e21 ),
inference(forward_subsumption_resolution,[status(thm)],[f1710,f1187]) ).
fof(f1729,plain,
( op2(e21,e22) = e23
| op2(e21,e22) = e22
| op2(e21,e22) = e21
| h5(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f278,f82]) ).
fof(f1730,plain,
( op2(e21,e22) = e23
| op2(e21,e22) = e22
| h5(e10) = e21
| h5(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f278,f1729]) ).
fof(f1731,plain,
( op2(e21,e22) = e23
| h5(e10) = e22
| h5(e10) = e21
| h5(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f278,f1730]) ).
fof(f1732,plain,
( h5(e10) = e23
| h5(e10) = e22
| h5(e10) = e21
| h5(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f278,f1731]) ).
fof(f1733,plain,
( h5(e10) = e23
| h5(e10) = e22
| h5(e10) = e20 ),
inference(forward_subsumption_resolution,[status(thm)],[f1732,f1348]) ).
fof(f1734,plain,
( h5(e10) = e23
| h5(e10) = e20 ),
inference(resolution,[status(thm)],[f1733,f1289]) ).
fof(f1745,plain,
h5(e10) = e20,
inference(forward_subsumption_resolution,[status(thm)],[f1734,f1680]) ).
fof(f1762,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e10) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f248,f357]) ).
fof(f1763,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e21 != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1506,f1762]) ).
fof(f1764,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e21 != op2(e21,h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1506,f1763]) ).
fof(f1765,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e21 != op2(e21,e21) ),
inference(forward_demodulation,[status(thm)],[f1506,f1764]) ).
fof(f1766,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f253,f1765]) ).
fof(f1767,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1506,f1766]) ).
fof(f1768,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e21,h3(e12))
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1506,f1767]) ).
fof(f1769,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e21,e20)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f268,f1768]) ).
fof(f1770,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f274,f1769]) ).
fof(f1771,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e11) != op2(h3(e10),h3(e13))
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1491,f1770]) ).
fof(f1772,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e11) != op2(e21,h3(e13))
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1506,f1771]) ).
fof(f1773,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e11) != op2(e21,e23)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f269,f1772]) ).
fof(f1774,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1627,f1773]) ).
fof(f1775,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1506,f1774]) ).
fof(f1776,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f249,f1775]) ).
fof(f1777,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f268,f1776]) ).
fof(f1778,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e12) != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1531,f1777]) ).
fof(f1779,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e20 != op2(h3(e11),h3(e13))
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f268,f1778]) ).
fof(f1780,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f269,f1779]) ).
fof(f1781,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e20,h3(e10))
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f268,f1780]) ).
fof(f1782,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e20,e21)
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1506,f1781]) ).
fof(f1783,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1693,f1782]) ).
fof(f1784,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f268,f1783]) ).
fof(f1785,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e12) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f250,f1784]) ).
fof(f1786,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e20 != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f268,f1785]) ).
fof(f1787,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e20 != op2(e20,h3(e12))
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f268,f1786]) ).
fof(f1788,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e20 != op2(e20,e20)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f268,f1787]) ).
fof(f1789,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f252,f1788]) ).
fof(f1790,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e10) != op2(h3(e12),h3(e13))
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f256,f1789]) ).
fof(f1791,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e21 != op2(h3(e12),h3(e13))
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1506,f1790]) ).
fof(f1792,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e21 != op2(e20,h3(e13))
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f268,f1791]) ).
fof(f1793,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e21 != op2(e20,e23)
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f269,f1792]) ).
fof(f1794,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1507,f1793]) ).
fof(f1795,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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(e12) != op2(h3(e13),h3(e10))
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1548,f1794]) ).
fof(f1796,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e20 != op2(h3(e13),h3(e10))
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f268,f1795]) ).
fof(f1797,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e20 != op2(e23,h3(e10))
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f269,f1796]) ).
fof(f1798,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e20 != op2(e23,e21)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1506,f1797]) ).
fof(f1799,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| 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))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f302,f1798]) ).
fof(f1800,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(e10) != op2(h3(e13),h3(e11))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1538,f1799]) ).
fof(f1801,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| e21 != op2(h3(e13),h3(e11))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1506,f1800]) ).
fof(f1802,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f269,f1801]) ).
fof(f1803,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(e11) != op2(h3(e13),h3(e12))
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1494,f1802]) ).
fof(f1804,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(e11) != op2(e23,h3(e12))
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f269,f1803]) ).
fof(f1805,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(e11) != op2(e23,e20)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f268,f1804]) ).
fof(f1806,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(e11) != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f298,f1805]) ).
fof(f1807,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(e13) != op2(h3(e13),h3(e13))
| h3(e11) != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f251,f1806]) ).
fof(f1808,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| e23 != op2(h3(e13),h3(e13))
| h3(e11) != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f269,f1807]) ).
fof(f1809,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| e23 != op2(e23,h3(e13))
| h3(e11) != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f269,f1808]) ).
fof(f1810,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| e23 != op2(e23,e23)
| h3(e11) != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f269,f1809]) ).
fof(f1811,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| e23 != e23
| h3(e11) != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f255,f1810]) ).
fof(f1812,plain,
( e23 != e23
| sP8_prd
| sP7_prd
| sP6_prd
| e23 != e23
| h3(e11) != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| e21 != e21
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f269,f1811]) ).
fof(f1813,plain,
( sP8_prd
| sP7_prd
| sP6_prd
| e23 != e23
| h3(e11) != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| e20 != e20
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(e11) != h3(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11))
| e21 != e21 ),
inference(duplicate_literals_removal,[status(thm)],[f1812]) ).
fof(f1814,plain,
( sP8_prd
| sP7_prd
| sP6_prd
| h3(e11) != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11)) ),
inference(trivial_equality_resolution,[status(thm)],[f1813]) ).
fof(f1815,plain,
( sP8_prd
| sP7_prd
| h3(e11) != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1814,f712]) ).
fof(f1817,plain,
e20 != h2(e11),
inference(backward_demodulation,[status(thm)],[f1745,f1699]) ).
fof(f1824,plain,
e20 = op2(e21,e22),
inference(backward_demodulation,[status(thm)],[f1745,f278]) ).
fof(f1828,plain,
h8(e10) = h1(e11),
inference(backward_demodulation,[status(thm)],[f1688,f290]) ).
fof(f1829,plain,
h1(e11) != e20,
inference(backward_demodulation,[status(thm)],[f1828,f1458]) ).
fof(f1830,plain,
h1(e11) != e22,
inference(backward_demodulation,[status(thm)],[f1828,f1456]) ).
fof(f1833,plain,
e21 != h1(e11),
inference(backward_demodulation,[status(thm)],[f1828,f1277]) ).
fof(f1834,plain,
( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| h3(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f1627,f83]) ).
fof(f1835,plain,
( op2(e21,e23) = e23
| op2(e21,e23) = e22
| h3(e11) = e21
| h3(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f1627,f1834]) ).
fof(f1836,plain,
( op2(e21,e23) = e23
| h3(e11) = e22
| h3(e11) = e21
| h3(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f1627,f1835]) ).
fof(f1837,plain,
( h3(e11) = e23
| h3(e11) = e22
| h3(e11) = e21
| h3(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f1627,f1836]) ).
fof(f1838,plain,
( h3(e11) = e23
| h3(e11) = e22
| h3(e11) = e21 ),
inference(forward_subsumption_resolution,[status(thm)],[f1837,f1634]) ).
fof(f1841,plain,
( h3(e11) = e22
| h3(e11) = e21 ),
inference(resolution,[status(thm)],[f1838,f1633]) ).
fof(f1855,plain,
h3(e11) = e22,
inference(forward_subsumption_resolution,[status(thm)],[f1841,f1631]) ).
fof(f1860,plain,
( op2(e22,e20) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21
| h7(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f286,f84]) ).
fof(f1861,plain,
( op2(e22,e20) = e23
| op2(e22,e20) = e22
| h7(e10) = e21
| h7(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f286,f1860]) ).
fof(f1862,plain,
( op2(e22,e20) = e23
| h7(e10) = e22
| h7(e10) = e21
| h7(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f286,f1861]) ).
fof(f1863,plain,
( h7(e10) = e23
| h7(e10) = e22
| h7(e10) = e21
| h7(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f286,f1862]) ).
fof(f1864,plain,
( h7(e10) = e23
| h7(e10) = e22
| h7(e10) = e21 ),
inference(forward_subsumption_resolution,[status(thm)],[f1863,f1189]) ).
fof(f1875,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,h3(e11)) ),
inference(backward_demodulation,[status(thm)],[f1855,f1815]) ).
fof(f1878,plain,
h4(e10) != e22,
inference(backward_demodulation,[status(thm)],[f1855,f1632]) ).
fof(f1885,plain,
( e22 != e22
| ~ sP8_prd ),
inference(backward_demodulation,[status(thm)],[f1855,f444]) ).
fof(f1887,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != op2(e21,e22) ),
inference(forward_demodulation,[status(thm)],[f1855,f1875]) ).
fof(f1888,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),e21)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1824,f1887]) ).
fof(f1889,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(e22,e21)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1855,f1888]) ).
fof(f1890,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| h3(e11) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1688,f1889]) ).
fof(f1891,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| e22 != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1855,f1890]) ).
fof(f1892,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| e22 != op2(e22,h3(e11))
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1855,f1891]) ).
fof(f1893,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| e22 != op2(e22,e22)
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1855,f1892]) ).
fof(f1894,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e20)
| e22 != e22
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f254,f1893]) ).
fof(f1895,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(e22,e20)
| e22 != e22
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1855,f1894]) ).
fof(f1896,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(h3(e11),e23)
| h3(op1(e11,e12)) != h7(e10)
| e22 != e22
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f286,f1895]) ).
fof(f1897,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != op2(e22,e23)
| h3(op1(e11,e12)) != h7(e10)
| e22 != e22
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1855,f1896]) ).
fof(f1898,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,h3(e11))
| h3(op1(e12,e10)) != e22
| e20 != e20
| h3(op1(e11,e12)) != h7(e10)
| e22 != e22
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f258,f1897]) ).
fof(f1899,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != op2(e20,e22)
| h3(op1(e12,e10)) != e22
| e20 != e20
| h3(op1(e11,e12)) != h7(e10)
| e22 != e22
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1855,f1898]) ).
fof(f1900,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,h3(e11))
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| e20 != e20
| h3(op1(e11,e12)) != h7(e10)
| e22 != e22
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1681,f1899]) ).
fof(f1901,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != op2(e23,e22)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| e20 != e20
| h3(op1(e11,e12)) != h7(e10)
| e22 != e22
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1855,f1900]) ).
fof(f1902,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| e20 != e20
| h3(op1(e11,e12)) != h7(e10)
| e22 != e22
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1674,f1901]) ).
fof(f1903,plain,
( sP8_prd
| sP7_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e11,e12)) != h7(e10)
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(trivial_equality_resolution,[status(thm)],[f1902]) ).
fof(f1904,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e11,e12)) != h7(e10)
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(op1(e10,e11)) != e20 ),
inference(forward_subsumption_resolution,[status(thm)],[f1903,f1521]) ).
fof(f1906,plain,
~ sP8_prd,
inference(trivial_equality_resolution,[status(thm)],[f1885]) ).
fof(f1911,plain,
( h4(e10) = e23
| h4(e10) = e21 ),
inference(backward_subsumption_resolution,[status(thm)],[f1711,f1878]) ).
fof(f1913,plain,
h4(e10) = e23,
inference(forward_subsumption_resolution,[status(thm)],[f1911,f1342]) ).
fof(f1918,plain,
e23 != h7(e10),
inference(backward_demodulation,[status(thm)],[f1913,f1193]) ).
fof(f1921,plain,
( h7(e10) = e22
| h7(e10) = e21 ),
inference(backward_subsumption_resolution,[status(thm)],[f1864,f1918]) ).
fof(f1922,plain,
h7(e10) = e21,
inference(forward_subsumption_resolution,[status(thm)],[f1921,f1452]) ).
fof(f1926,plain,
e21 != h10(e10),
inference(backward_demodulation,[status(thm)],[f1922,f1197]) ).
fof(f1935,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| h1(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f1688,f85]) ).
fof(f1936,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22
| h1(e11) = e21
| h1(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f1688,f1935]) ).
fof(f1937,plain,
( op2(e22,e21) = e23
| h1(e11) = e22
| h1(e11) = e21
| h1(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f1688,f1936]) ).
fof(f1938,plain,
( h1(e11) = e23
| h1(e11) = e22
| h1(e11) = e21
| h1(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f1688,f1937]) ).
fof(f1939,plain,
( h1(e11) = e23
| h1(e11) = e22
| h1(e11) = e21 ),
inference(forward_subsumption_resolution,[status(thm)],[f1938,f1829]) ).
fof(f1940,plain,
( h1(e11) = e23
| h1(e11) = e21 ),
inference(resolution,[status(thm)],[f1939,f1830]) ).
fof(f1946,plain,
h1(e11) = e23,
inference(forward_subsumption_resolution,[status(thm)],[f1940,f1833]) ).
fof(f2021,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| h10(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f298,f88]) ).
fof(f2022,plain,
( op2(e23,e20) = e23
| op2(e23,e20) = e22
| h10(e10) = e21
| h10(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f298,f2021]) ).
fof(f2023,plain,
( op2(e23,e20) = e23
| h10(e10) = e22
| h10(e10) = e21
| h10(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f298,f2022]) ).
fof(f2024,plain,
( h10(e10) = e23
| h10(e10) = e22
| h10(e10) = e21
| h10(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f298,f2023]) ).
fof(f2025,plain,
( h10(e10) = e23
| h10(e10) = e22
| h10(e10) = e21 ),
inference(forward_subsumption_resolution,[status(thm)],[f2024,f1191]) ).
fof(f2027,plain,
( h10(e10) = e22
| h10(e10) = e21 ),
inference(resolution,[status(thm)],[f2025,f1466]) ).
fof(f2036,plain,
h10(e10) = e22,
inference(forward_subsumption_resolution,[status(thm)],[f2027,f1926]) ).
fof(f2039,plain,
( op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e23,e21) = e21
| h11(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f302,f89]) ).
fof(f2040,plain,
( op2(e23,e21) = e23
| op2(e23,e21) = e22
| h11(e10) = e21
| h11(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f302,f2039]) ).
fof(f2041,plain,
( op2(e23,e21) = e23
| h11(e10) = e22
| h11(e10) = e21
| h11(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f302,f2040]) ).
fof(f2042,plain,
( h11(e10) = e23
| h11(e10) = e22
| h11(e10) = e21
| h11(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f302,f2041]) ).
fof(f2043,plain,
( h11(e10) = e23
| h11(e10) = e22
| h11(e10) = e20 ),
inference(forward_subsumption_resolution,[status(thm)],[f2042,f1279]) ).
fof(f2044,plain,
( h11(e10) = e23
| h11(e10) = e20 ),
inference(resolution,[status(thm)],[f2043,f1690]) ).
fof(f2054,plain,
h11(e10) = e20,
inference(forward_subsumption_resolution,[status(thm)],[f2044,f1470]) ).
fof(f2094,plain,
( op2(e23,e22) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21
| h2(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f1674,f90]) ).
fof(f2095,plain,
( op2(e23,e22) = e23
| op2(e23,e22) = e22
| h2(e11) = e21
| h2(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f1674,f2094]) ).
fof(f2096,plain,
( op2(e23,e22) = e23
| h2(e11) = e22
| h2(e11) = e21
| h2(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f1674,f2095]) ).
fof(f2097,plain,
( h2(e11) = e23
| h2(e11) = e22
| h2(e11) = e21
| h2(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f1674,f2096]) ).
fof(f2098,plain,
( h2(e11) = e23
| h2(e11) = e22
| h2(e11) = e21 ),
inference(forward_subsumption_resolution,[status(thm)],[f2097,f1817]) ).
fof(f2099,plain,
( h2(e11) = e23
| h2(e11) = e21 ),
inference(resolution,[status(thm)],[f2098,f1698]) ).
fof(f2110,plain,
h2(e11) = e21,
inference(forward_subsumption_resolution,[status(thm)],[f2099,f1695]) ).
fof(f2242,plain,
( e12 = e10
| op1(e11,e12) = e10 ),
inference(forward_demodulation,[status(thm)],[f1531,f1001]) ).
fof(f2247,plain,
op1(e11,e12) = e10,
inference(forward_subsumption_resolution,[status(thm)],[f2242,f221]) ).
fof(f2248,plain,
( e11 = e12
| op1(e10,e11) = e12 ),
inference(forward_demodulation,[status(thm)],[f1491,f1052]) ).
fof(f2253,plain,
op1(e10,e11) = e12,
inference(forward_subsumption_resolution,[status(thm)],[f2248,f223]) ).
fof(f2254,plain,
( op1(e10,e12) = e13
| e12 = e13 ),
inference(forward_demodulation,[status(thm)],[f2253,f1067]) ).
fof(f2258,plain,
op1(e10,e12) = e13,
inference(forward_subsumption_resolution,[status(thm)],[f2254,f225]) ).
fof(f2259,plain,
( e10 = e13
| op1(e11,e10) = e13 ),
inference(forward_demodulation,[status(thm)],[f2247,f1071]) ).
fof(f2262,plain,
e13 != op1(e12,e10),
inference(backward_demodulation,[status(thm)],[f2264,f127]) ).
fof(f2264,plain,
op1(e11,e10) = e13,
inference(forward_subsumption_resolution,[status(thm)],[f2259,f222]) ).
fof(f2265,plain,
( e10 = e13
| op1(e12,e11) = e13 ),
inference(backward_subsumption_resolution,[status(thm)],[f1202,f2262]) ).
fof(f2267,plain,
op1(e12,e11) = e13,
inference(forward_subsumption_resolution,[status(thm)],[f2265,f222]) ).
fof(f2273,plain,
( e12 = e11
| op1(e12,e10) = e11 ),
inference(forward_demodulation,[status(thm)],[f1548,f1154]) ).
fof(f2278,plain,
op1(e12,e10) = e11,
inference(forward_subsumption_resolution,[status(thm)],[f2273,f223]) ).
fof(f2419,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e11,e12)) != h7(e10)
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| h3(e12) != e20 ),
inference(forward_demodulation,[status(thm)],[f2253,f1904]) ).
fof(f2420,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e11,e12)) != h7(e10)
| h3(op1(e11,e10)) != h1(e11)
| h3(op1(e10,e12)) != h4(e10)
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f268,f2419]) ).
fof(f2421,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e11,e12)) != h7(e10)
| h3(op1(e11,e10)) != h1(e11)
| h3(e13) != h4(e10)
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f2258,f2420]) ).
fof(f2422,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e11,e12)) != h7(e10)
| h3(op1(e11,e10)) != h1(e11)
| e23 != h4(e10)
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f269,f2421]) ).
fof(f2423,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e11,e12)) != h7(e10)
| h3(op1(e11,e10)) != h1(e11)
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f1913,f2422]) ).
fof(f2424,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e11,e12)) != h7(e10)
| h3(e13) != h1(e11)
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f2264,f2423]) ).
fof(f2425,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e11,e12)) != h7(e10)
| e23 != h1(e11)
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f269,f2424]) ).
fof(f2426,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e11,e12)) != h7(e10)
| e23 != e23
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f1946,f2425]) ).
fof(f2427,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| h3(e10) != h7(e10)
| e23 != e23
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f2247,f2426]) ).
fof(f2428,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| e21 != h7(e10)
| e23 != e23
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f1506,f2427]) ).
fof(f2429,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(op1(e12,e10)) != e22
| e21 != e21
| e23 != e23
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f1922,f2428]) ).
fof(f2430,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| h3(e11) != e22
| e21 != e21
| e23 != e23
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f2278,f2429]) ).
fof(f2431,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(op1(e12,e11)) != e23
| e22 != e22
| e21 != e21
| e23 != e23
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f1855,f2430]) ).
fof(f2432,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| h3(e13) != e23
| e22 != e22
| e21 != e21
| e23 != e23
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f2267,f2431]) ).
fof(f2433,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != h11(e10)
| e23 != e23
| e22 != e22
| e21 != e21
| e23 != e23
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f269,f2432]) ).
fof(f2434,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != h2(e11)
| e20 != e20
| e23 != e23
| e22 != e22
| e21 != e21
| e23 != e23
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f2054,f2433]) ).
fof(f2435,plain,
( sP8_prd
| e22 != h10(e10)
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22
| e21 != e21
| e23 != e23
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f2110,f2434]) ).
fof(f2436,plain,
( sP8_prd
| e22 != e22
| e21 != e21
| e20 != e20
| e23 != e23
| e22 != e22
| e21 != e21
| e23 != e23
| e23 != e23
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f2036,f2435]) ).
fof(f2437,plain,
( sP8_prd
| e22 != e22
| e21 != e21
| e23 != e23
| e20 != e20 ),
inference(duplicate_literals_removal,[status(thm)],[f2436]) ).
fof(f2438,plain,
sP8_prd,
inference(trivial_equality_resolution,[status(thm)],[f2437]) ).
fof(f2439,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2438,f1906]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG113+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n026.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 12:59:21 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.40 % Drodi V4.1.1
% 0.09/0.53 % Refutation found
% 0.09/0.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.57 % Elapsed time: 0.185737 seconds
% 0.09/0.57 % CPU time: 1.083483 seconds
% 0.09/0.57 % Total memory used: 153.589 MB
% 0.09/0.57 % Net memory used: 153.090 MB
%------------------------------------------------------------------------------