%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG016+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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:47:45 AM UTC 2026
% Result : Theorem 1.29s 0.64s
% Output : CNFRefutation 1.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 105
% Number of leaves : 27
% Syntax : Number of formulae : 314 ( 147 unt; 12 def)
% Number of atoms : 2483 (2319 equ)
% Maximal formula atoms : 128 ( 7 avg)
% Number of connectives : 3741 (1572 ~;1612 |; 545 &)
% ( 12 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 64 ( 7 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 14 ( 12 usr; 13 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-2 aty)
% Number of variables : 0 ( 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e13,e13) = e10 )
& ( op1(e13,e12) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11
| op1(e13,e12) = e10 )
& ( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e13,e11) = e10 )
& ( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 )
& ( op1(e12,e13) = e13
| op1(e12,e13) = e12
| op1(e12,e13) = e11
| op1(e12,e13) = e10 )
& ( op1(e12,e12) = e13
| op1(e12,e12) = e12
| op1(e12,e12) = e11
| op1(e12,e12) = e10 )
& ( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 )
& ( op1(e12,e10) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 )
& ( op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11
| op1(e11,e13) = e10 )
& ( op1(e11,e12) = e13
| op1(e11,e12) = e12
| op1(e11,e12) = e11
| op1(e11,e12) = e10 )
& ( op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e11) = e10 )
& ( op1(e11,e10) = e13
| op1(e11,e10) = e12
| op1(e11,e10) = e11
| op1(e11,e10) = e10 )
& ( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 )
& ( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 )
& ( op1(e10,e11) = e13
| op1(e10,e11) = e12
| op1(e10,e11) = e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e11
| op1(e10,e10) = e10 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
( op1(op1(e13,e13),e13) = op1(e13,op1(e13,e13))
& op1(op1(e13,e13),e12) = op1(e13,op1(e13,e12))
& op1(op1(e13,e13),e11) = op1(e13,op1(e13,e11))
& op1(op1(e13,e13),e10) = op1(e13,op1(e13,e10))
& op1(op1(e13,e12),e13) = op1(e13,op1(e12,e13))
& op1(op1(e13,e12),e12) = op1(e13,op1(e12,e12))
& op1(op1(e13,e12),e11) = op1(e13,op1(e12,e11))
& op1(op1(e13,e12),e10) = op1(e13,op1(e12,e10))
& op1(op1(e13,e11),e13) = op1(e13,op1(e11,e13))
& op1(op1(e13,e11),e12) = op1(e13,op1(e11,e12))
& op1(op1(e13,e11),e11) = op1(e13,op1(e11,e11))
& op1(op1(e13,e11),e10) = op1(e13,op1(e11,e10))
& op1(op1(e13,e10),e13) = op1(e13,op1(e10,e13))
& op1(op1(e13,e10),e12) = op1(e13,op1(e10,e12))
& op1(op1(e13,e10),e11) = op1(e13,op1(e10,e11))
& op1(op1(e13,e10),e10) = op1(e13,op1(e10,e10))
& op1(op1(e12,e13),e13) = op1(e12,op1(e13,e13))
& op1(op1(e12,e13),e12) = op1(e12,op1(e13,e12))
& op1(op1(e12,e13),e11) = op1(e12,op1(e13,e11))
& op1(op1(e12,e13),e10) = op1(e12,op1(e13,e10))
& op1(op1(e12,e12),e13) = op1(e12,op1(e12,e13))
& op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12))
& op1(op1(e12,e12),e11) = op1(e12,op1(e12,e11))
& op1(op1(e12,e12),e10) = op1(e12,op1(e12,e10))
& op1(op1(e12,e11),e13) = op1(e12,op1(e11,e13))
& op1(op1(e12,e11),e12) = op1(e12,op1(e11,e12))
& op1(op1(e12,e11),e11) = op1(e12,op1(e11,e11))
& op1(op1(e12,e11),e10) = op1(e12,op1(e11,e10))
& op1(op1(e12,e10),e13) = op1(e12,op1(e10,e13))
& op1(op1(e12,e10),e12) = op1(e12,op1(e10,e12))
& op1(op1(e12,e10),e11) = op1(e12,op1(e10,e11))
& op1(op1(e12,e10),e10) = op1(e12,op1(e10,e10))
& op1(op1(e11,e13),e13) = op1(e11,op1(e13,e13))
& op1(op1(e11,e13),e12) = op1(e11,op1(e13,e12))
& op1(op1(e11,e13),e11) = op1(e11,op1(e13,e11))
& op1(op1(e11,e13),e10) = op1(e11,op1(e13,e10))
& op1(op1(e11,e12),e13) = op1(e11,op1(e12,e13))
& op1(op1(e11,e12),e12) = op1(e11,op1(e12,e12))
& op1(op1(e11,e12),e11) = op1(e11,op1(e12,e11))
& op1(op1(e11,e12),e10) = op1(e11,op1(e12,e10))
& op1(op1(e11,e11),e13) = op1(e11,op1(e11,e13))
& op1(op1(e11,e11),e12) = op1(e11,op1(e11,e12))
& op1(op1(e11,e11),e11) = op1(e11,op1(e11,e11))
& op1(op1(e11,e11),e10) = op1(e11,op1(e11,e10))
& op1(op1(e11,e10),e13) = op1(e11,op1(e10,e13))
& op1(op1(e11,e10),e12) = op1(e11,op1(e10,e12))
& op1(op1(e11,e10),e11) = op1(e11,op1(e10,e11))
& op1(op1(e11,e10),e10) = op1(e11,op1(e10,e10))
& op1(op1(e10,e13),e13) = op1(e10,op1(e13,e13))
& op1(op1(e10,e13),e12) = op1(e10,op1(e13,e12))
& op1(op1(e10,e13),e11) = op1(e10,op1(e13,e11))
& op1(op1(e10,e13),e10) = op1(e10,op1(e13,e10))
& op1(op1(e10,e12),e13) = op1(e10,op1(e12,e13))
& op1(op1(e10,e12),e12) = op1(e10,op1(e12,e12))
& op1(op1(e10,e12),e11) = op1(e10,op1(e12,e11))
& op1(op1(e10,e12),e10) = op1(e10,op1(e12,e10))
& op1(op1(e10,e11),e13) = op1(e10,op1(e11,e13))
& op1(op1(e10,e11),e12) = op1(e10,op1(e11,e12))
& op1(op1(e10,e11),e11) = op1(e10,op1(e11,e11))
& op1(op1(e10,e11),e10) = op1(e10,op1(e11,e10))
& op1(op1(e10,e10),e13) = op1(e10,op1(e10,e13))
& op1(op1(e10,e10),e12) = op1(e10,op1(e10,e12))
& op1(op1(e10,e10),e11) = op1(e10,op1(e10,e11))
& op1(op1(e10,e10),e10) = op1(e10,op1(e10,e10)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
( op2(op2(e23,e23),e23) = op2(e23,op2(e23,e23))
& op2(op2(e23,e23),e22) = op2(e23,op2(e23,e22))
& op2(op2(e23,e23),e21) = op2(e23,op2(e23,e21))
& op2(op2(e23,e23),e20) = op2(e23,op2(e23,e20))
& op2(op2(e23,e22),e23) = op2(e23,op2(e22,e23))
& op2(op2(e23,e22),e22) = op2(e23,op2(e22,e22))
& op2(op2(e23,e22),e21) = op2(e23,op2(e22,e21))
& op2(op2(e23,e22),e20) = op2(e23,op2(e22,e20))
& op2(op2(e23,e21),e23) = op2(e23,op2(e21,e23))
& op2(op2(e23,e21),e22) = op2(e23,op2(e21,e22))
& op2(op2(e23,e21),e21) = op2(e23,op2(e21,e21))
& op2(op2(e23,e21),e20) = op2(e23,op2(e21,e20))
& op2(op2(e23,e20),e23) = op2(e23,op2(e20,e23))
& op2(op2(e23,e20),e22) = op2(e23,op2(e20,e22))
& op2(op2(e23,e20),e21) = op2(e23,op2(e20,e21))
& op2(op2(e23,e20),e20) = op2(e23,op2(e20,e20))
& op2(op2(e22,e23),e23) = op2(e22,op2(e23,e23))
& op2(op2(e22,e23),e22) = op2(e22,op2(e23,e22))
& op2(op2(e22,e23),e21) = op2(e22,op2(e23,e21))
& op2(op2(e22,e23),e20) = op2(e22,op2(e23,e20))
& op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23))
& op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22))
& op2(op2(e22,e22),e21) = op2(e22,op2(e22,e21))
& op2(op2(e22,e22),e20) = op2(e22,op2(e22,e20))
& op2(op2(e22,e21),e23) = op2(e22,op2(e21,e23))
& op2(op2(e22,e21),e22) = op2(e22,op2(e21,e22))
& op2(op2(e22,e21),e21) = op2(e22,op2(e21,e21))
& op2(op2(e22,e21),e20) = op2(e22,op2(e21,e20))
& op2(op2(e22,e20),e23) = op2(e22,op2(e20,e23))
& op2(op2(e22,e20),e22) = op2(e22,op2(e20,e22))
& op2(op2(e22,e20),e21) = op2(e22,op2(e20,e21))
& op2(op2(e22,e20),e20) = op2(e22,op2(e20,e20))
& op2(op2(e21,e23),e23) = op2(e21,op2(e23,e23))
& op2(op2(e21,e23),e22) = op2(e21,op2(e23,e22))
& op2(op2(e21,e23),e21) = op2(e21,op2(e23,e21))
& op2(op2(e21,e23),e20) = op2(e21,op2(e23,e20))
& op2(op2(e21,e22),e23) = op2(e21,op2(e22,e23))
& op2(op2(e21,e22),e22) = op2(e21,op2(e22,e22))
& op2(op2(e21,e22),e21) = op2(e21,op2(e22,e21))
& op2(op2(e21,e22),e20) = op2(e21,op2(e22,e20))
& op2(op2(e21,e21),e23) = op2(e21,op2(e21,e23))
& op2(op2(e21,e21),e22) = op2(e21,op2(e21,e22))
& op2(op2(e21,e21),e21) = op2(e21,op2(e21,e21))
& op2(op2(e21,e21),e20) = op2(e21,op2(e21,e20))
& op2(op2(e21,e20),e23) = op2(e21,op2(e20,e23))
& op2(op2(e21,e20),e22) = op2(e21,op2(e20,e22))
& op2(op2(e21,e20),e21) = op2(e21,op2(e20,e21))
& op2(op2(e21,e20),e20) = op2(e21,op2(e20,e20))
& op2(op2(e20,e23),e23) = op2(e20,op2(e23,e23))
& op2(op2(e20,e23),e22) = op2(e20,op2(e23,e22))
& op2(op2(e20,e23),e21) = op2(e20,op2(e23,e21))
& op2(op2(e20,e23),e20) = op2(e20,op2(e23,e20))
& op2(op2(e20,e22),e23) = op2(e20,op2(e22,e23))
& op2(op2(e20,e22),e22) = op2(e20,op2(e22,e22))
& op2(op2(e20,e22),e21) = op2(e20,op2(e22,e21))
& op2(op2(e20,e22),e20) = op2(e20,op2(e22,e20))
& op2(op2(e20,e21),e23) = op2(e20,op2(e21,e23))
& op2(op2(e20,e21),e22) = op2(e20,op2(e21,e22))
& op2(op2(e20,e21),e21) = op2(e20,op2(e21,e21))
& op2(op2(e20,e21),e20) = op2(e20,op2(e21,e20))
& op2(op2(e20,e20),e23) = op2(e20,op2(e20,e23))
& op2(op2(e20,e20),e22) = op2(e20,op2(e20,e22))
& op2(op2(e20,e20),e21) = op2(e20,op2(e20,e21))
& op2(op2(e20,e20),e20) = op2(e20,op2(e20,e20)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
( ( unit2 = e23
| unit2 = e22
| unit2 = e21
| unit2 = e20 )
& op2(e23,unit2) = e23
& op2(unit2,e23) = e23
& op2(e22,unit2) = e22
& op2(unit2,e22) = e22
& op2(e21,unit2) = e21
& op2(unit2,e21) = e21
& op2(e20,unit2) = e20
& op2(unit2,e20) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
( e13 = op1(e12,e12)
& e11 = op1(e12,op1(e12,e12))
& e10 = op1(op1(e12,op1(e12,e12)),e12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
( e23 = op2(e22,e22)
& e21 = op2(e22,op2(e22,e22))
& e20 = op2(op2(e22,op2(e22,e22)),e22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
( h1(e13) = op2(e20,e20)
& h1(e11) = op2(e20,op2(e20,e20))
& h1(e10) = op2(op2(e20,op2(e20,e20)),e20)
& h1(e12) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
( h2(e13) = op2(e21,e21)
& h2(e11) = op2(e21,op2(e21,e21))
& h2(e10) = op2(op2(e21,op2(e21,e21)),e21)
& h2(e12) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
( h3(e13) = op2(e22,e22)
& h3(e11) = op2(e22,op2(e22,e22))
& h3(e10) = op2(op2(e22,op2(e22,e22)),e22)
& h3(e12) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
( h4(e13) = op2(e23,e23)
& h4(e11) = op2(e23,op2(e23,e23))
& h4(e10) = op2(op2(e23,op2(e23,e23)),e23)
& h4(e12) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,conjecture,
( ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,negated_conjecture,
~ ( ( ( h4(e13) = e23
| h4(e12) = e23
| h4(e11) = e23
| h4(e10) = e23 )
& ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22 )
& ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21 )
& ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20 )
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) )
| ( ( h3(e13) = e23
| h3(e12) = e23
| h3(e11) = e23
| h3(e10) = e23 )
& ( h3(e13) = e22
| h3(e12) = e22
| h3(e11) = e22
| h3(e10) = e22 )
& ( h3(e13) = e21
| h3(e12) = e21
| h3(e11) = e21
| h3(e10) = e21 )
& ( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20 )
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e10)) = op2(h3(e10),h3(e10)) )
| ( ( h2(e13) = e23
| h2(e12) = e23
| h2(e11) = e23
| h2(e10) = e23 )
& ( h2(e13) = e22
| h2(e12) = e22
| h2(e11) = e22
| h2(e10) = e22 )
& ( h2(e13) = e21
| h2(e12) = e21
| h2(e11) = e21
| h2(e10) = e21 )
& ( h2(e13) = e20
| h2(e12) = e20
| h2(e11) = e20
| h2(e10) = e20 )
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) )
| ( ( h1(e13) = e23
| h1(e12) = e23
| h1(e11) = e23
| h1(e10) = e23 )
& ( h1(e13) = e22
| h1(e12) = e22
| h1(e11) = e22
| h1(e10) = e22 )
& ( h1(e13) = e21
| h1(e12) = e21
| h1(e11) = e21
| h1(e10) = e21 )
& ( h1(e13) = e20
| h1(e12) = e20
| h1(e11) = e20
| h1(e10) = e20 )
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e10)) = op2(h1(e10),h1(e10)) ) ),
inference(negated_conjecture,[status(cth)],[f30]) ).
fof(f34,plain,
( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f40,plain,
( op1(e12,e10) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f58,plain,
op1(op1(e10,e12),e12) = op1(e10,op1(e12,e12)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f59,plain,
op1(op1(e10,e12),e13) = op1(e10,op1(e12,e13)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f74,plain,
op1(op1(e11,e12),e12) = op1(e11,op1(e12,e12)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f88,plain,
op1(op1(e12,e12),e10) = op1(e12,op1(e12,e10)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f90,plain,
op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f91,plain,
op1(op1(e12,e12),e13) = op1(e12,op1(e12,e13)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f92,plain,
op1(op1(e12,e13),e10) = op1(e12,op1(e13,e10)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f94,plain,
op1(op1(e12,e13),e12) = op1(e12,op1(e13,e12)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f95,plain,
op1(op1(e12,e13),e13) = op1(e12,op1(e13,e13)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f105,plain,
op1(op1(e13,e12),e11) = op1(e13,op1(e12,e11)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f107,plain,
op1(op1(e13,e12),e13) = op1(e13,op1(e12,e13)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f108,plain,
op1(op1(e13,e13),e10) = op1(e13,op1(e13,e10)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f140,plain,
( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| op2(e21,e23) = e20 ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f191,plain,
op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f192,plain,
op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23)),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f194,plain,
op2(op2(e22,e23),e21) = op2(e22,op2(e23,e21)),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f195,plain,
op2(op2(e22,e23),e22) = op2(e22,op2(e23,e22)),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f208,plain,
op2(op2(e23,e22),e23) = op2(e23,op2(e22,e23)),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f214,plain,
op2(e20,unit2) = e20,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f215,plain,
op2(unit2,e21) = e21,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f216,plain,
op2(e21,unit2) = e21,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f217,plain,
op2(unit2,e22) = e22,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f218,plain,
op2(e22,unit2) = e22,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f219,plain,
op2(unit2,e23) = e23,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f220,plain,
op2(e23,unit2) = e23,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f221,plain,
( unit2 = e23
| unit2 = e22
| unit2 = e21
| unit2 = e20 ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f302,plain,
op1(e10,e12) != op1(e11,e12),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f303,plain,
op1(e10,e12) != op1(e12,e12),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f304,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f326,plain,
op1(e12,e10) != op1(e12,e11),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f327,plain,
op1(e12,e10) != op1(e12,e12),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f328,plain,
op1(e12,e10) != op1(e12,e13),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f345,plain,
op2(e20,e21) != op2(e22,e21),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f355,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f359,plain,
op2(e21,e23) != op2(e22,e23),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f360,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f380,plain,
op2(e23,e20) != op2(e23,e21),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f392,plain,
e20 != e21,
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f393,plain,
e20 != e22,
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f394,plain,
e20 != e23,
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f395,plain,
e21 != e22,
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f424,plain,
e10 = op1(op1(e12,op1(e12,e12)),e12),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f425,plain,
e11 = op1(e12,op1(e12,e12)),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f426,plain,
e13 = op1(e12,e12),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f427,plain,
e20 = op2(op2(e22,op2(e22,e22)),e22),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f428,plain,
e21 = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f429,plain,
e23 = op2(e22,e22),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f433,plain,
h1(e13) = op2(e20,e20),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f437,plain,
h2(e13) = op2(e21,e21),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f438,plain,
h3(e12) = e22,
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f439,plain,
h3(e10) = op2(op2(e22,op2(e22,e22)),e22),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f440,plain,
h3(e11) = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f441,plain,
h3(e13) = op2(e22,e22),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f445,plain,
h4(e13) = op2(e23,e23),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f446,plain,
( ( ( 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)],[f31]) ).
fof(f447,definition,
( sP0_prd
<=> ( h1(e13) != e20
& h1(e12) != e20
& h1(e11) != e20
& h1(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f448,definition,
( sP1_prd
<=> ( h1(e13) != e21
& h1(e12) != e21
& h1(e11) != e21
& h1(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f449,definition,
( sP2_prd
<=> ( h1(e13) != e22
& h1(e12) != e22
& h1(e11) != e22
& h1(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f450,definition,
( sP3_prd
<=> ( h2(e13) != e20
& h2(e12) != e20
& h2(e11) != e20
& h2(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f451,definition,
( sP4_prd
<=> ( h2(e13) != e21
& h2(e12) != e21
& h2(e11) != e21
& h2(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f452,definition,
( sP5_prd
<=> ( h2(e13) != e22
& h2(e12) != e22
& h2(e11) != e22
& h2(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f453,definition,
( sP6_prd
<=> ( h3(e13) != e20
& h3(e12) != e20
& h3(e11) != e20
& h3(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f454,definition,
( sP7_prd
<=> ( h3(e13) != e21
& h3(e12) != e21
& h3(e11) != e21
& h3(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP7_prd])],[]) ).
fof(f455,definition,
( sP8_prd
<=> ( h3(e13) != e22
& h3(e12) != e22
& h3(e11) != e22
& h3(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP8_prd])],[]) ).
fof(f456,definition,
( sP9_prd
<=> ( h4(e13) != e20
& h4(e12) != e20
& h4(e11) != e20
& h4(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP9_prd])],[]) ).
fof(f457,definition,
( sP10_prd
<=> ( h4(e13) != e21
& h4(e12) != e21
& h4(e11) != e21
& h4(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP10_prd])],[]) ).
fof(f458,definition,
( sP11_prd
<=> ( h4(e13) != e22
& h4(e12) != e22
& h4(e11) != e22
& h4(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP11_prd])],[]) ).
fof(f459,plain,
( ( ( 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)],[f446,f458,f457,f456,f455,f454,f453,f452,f451,f450,f449,f448,f447]) ).
fof(f471,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)],[f459]) ).
fof(f512,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)],[f453]) ).
fof(f513,plain,
( h3(e10) != e20
| ~ sP6_prd ),
inference(cnf_transformation,[status(thm)],[f512]) ).
fof(f517,plain,
( h3(e13) = e20
| h3(e12) = e20
| h3(e11) = e20
| h3(e10) = e20
| sP6_prd ),
inference(cnf_transformation,[status(thm)],[f512]) ).
fof(f518,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)],[f454]) ).
fof(f520,plain,
( h3(e11) != e21
| ~ sP7_prd ),
inference(cnf_transformation,[status(thm)],[f518]) ).
fof(f524,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)],[f455]) ).
fof(f527,plain,
( h3(e12) != e22
| ~ sP8_prd ),
inference(cnf_transformation,[status(thm)],[f524]) ).
fof(f663,plain,
op1(op1(e10,e12),e12) = op1(e10,e13),
inference(forward_demodulation,[status(thm)],[f426,f58]) ).
fof(f714,plain,
( e22 != e22
| ~ sP8_prd ),
inference(forward_demodulation,[status(thm)],[f438,f527]) ).
fof(f716,plain,
~ sP8_prd,
inference(trivial_equality_resolution,[status(thm)],[f714]) ).
fof(f719,plain,
op1(op1(e11,e12),e12) = op1(e11,e13),
inference(forward_demodulation,[status(thm)],[f426,f74]) ).
fof(f758,plain,
h3(e13) = e23,
inference(forward_demodulation,[status(thm)],[f429,f441]) ).
fof(f783,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),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f438,f471]) ).
fof(f784,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),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f758,f783]) ).
fof(f785,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),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f438,f784]) ).
fof(f786,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),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f758,f785]) ).
fof(f787,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(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f438,f786]) ).
fof(f788,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(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f438,f787]) ).
fof(f789,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(e13) != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f426,f788]) ).
fof(f790,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))
| e23 != op2(h3(e12),h3(e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f758,f789]) ).
fof(f791,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))
| e23 != op2(e22,h3(e12))
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f438,f790]) ).
fof(f792,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))
| e23 != op2(e22,e22)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f438,f791]) ).
fof(f793,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))
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f429,f792]) ).
fof(f794,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(e22,h3(e13))
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f438,f793]) ).
fof(f795,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(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f758,f794]) ).
fof(f796,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(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f758,f795]) ).
fof(f797,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(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f758,f796]) ).
fof(f798,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(e23,h3(e12))
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f758,f797]) ).
fof(f799,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f438,f798]) ).
fof(f800,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != op2(e23,h3(e13))
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f758,f799]) ).
fof(f801,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != op2(e23,e23)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f758,f800]) ).
fof(f802,plain,
( h3(e13) != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f445,f801]) ).
fof(f803,plain,
( e23 != e23
| sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f758,f802]) ).
fof(f804,plain,
( sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| e23 != e23
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(duplicate_literals_removal,[status(thm)],[f803]) ).
fof(f805,plain,
( sP8_prd
| sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(trivial_equality_resolution,[status(thm)],[f804]) ).
fof(f806,plain,
( sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e13,e12)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_subsumption_resolution,[status(thm)],[f805,f716]) ).
fof(f812,plain,
op1(e13,e10) = op1(e12,op1(e12,e10)),
inference(forward_demodulation,[status(thm)],[f426,f88]) ).
fof(f816,plain,
op1(e13,e12) = op1(e12,op1(e12,e12)),
inference(forward_demodulation,[status(thm)],[f426,f90]) ).
fof(f817,plain,
( sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != h4(e13)
| h3(op1(e12,e13)) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(backward_demodulation,[status(thm)],[f821,f806]) ).
fof(f821,plain,
op1(e13,e12) = op1(e12,e13),
inference(forward_demodulation,[status(thm)],[f426,f816]) ).
fof(f827,plain,
op1(e13,e13) = op1(e12,op1(e12,e13)),
inference(forward_demodulation,[status(thm)],[f426,f91]) ).
fof(f852,plain,
op1(op1(e12,e13),e12) = op1(e12,op1(e12,e13)),
inference(forward_demodulation,[status(thm)],[f821,f94]) ).
fof(f853,plain,
op1(op1(e12,e13),e12) = op1(e13,e13),
inference(forward_demodulation,[status(thm)],[f827,f852]) ).
fof(f863,plain,
( h3(e13) = e20
| e22 = e20
| h3(e11) = e20
| h3(e10) = e20
| sP6_prd ),
inference(forward_demodulation,[status(thm)],[f438,f517]) ).
fof(f864,plain,
( e23 = e20
| e22 = e20
| h3(e11) = e20
| h3(e10) = e20
| sP6_prd ),
inference(forward_demodulation,[status(thm)],[f758,f863]) ).
fof(f865,plain,
( e23 = e20
| h3(e11) = e20
| h3(e10) = e20
| sP6_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f864,f393]) ).
fof(f908,plain,
( op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 ),
inference(backward_subsumption_resolution,[status(thm)],[f34,f909]) ).
fof(f909,plain,
op1(e10,e12) != e13,
inference(forward_demodulation,[status(thm)],[f426,f303]) ).
fof(f910,plain,
op1(e10,e12) != op1(e12,e13),
inference(forward_demodulation,[status(thm)],[f821,f304]) ).
fof(f917,plain,
op1(op1(e12,e13),e11) = op1(e13,op1(e12,e11)),
inference(forward_demodulation,[status(thm)],[f821,f105]) ).
fof(f949,plain,
op1(op1(e12,e13),e13) = op1(e13,op1(e12,e13)),
inference(forward_demodulation,[status(thm)],[f821,f107]) ).
fof(f1096,plain,
( op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 ),
inference(backward_subsumption_resolution,[status(thm)],[f40,f1097]) ).
fof(f1097,plain,
op1(e12,e10) != e13,
inference(forward_demodulation,[status(thm)],[f426,f327]) ).
fof(f1217,plain,
e23 != op2(e23,e22),
inference(forward_demodulation,[status(thm)],[f429,f355]) ).
fof(f1239,plain,
op2(e21,e23) != h4(e13),
inference(forward_demodulation,[status(thm)],[f445,f360]) ).
fof(f1319,plain,
op1(e12,e10) != e11,
inference(backward_demodulation,[status(thm)],[f1342,f328]) ).
fof(f1324,plain,
( sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != h4(e13)
| h3(e11) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e13)) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(backward_demodulation,[status(thm)],[f1342,f817]) ).
fof(f1326,plain,
op1(op1(e12,e13),e13) = op1(e13,e11),
inference(backward_demodulation,[status(thm)],[f1342,f949]) ).
fof(f1330,plain,
op1(e11,e11) = op1(e13,op1(e12,e11)),
inference(backward_demodulation,[status(thm)],[f1342,f917]) ).
fof(f1332,plain,
op1(e10,e12) != e11,
inference(backward_demodulation,[status(thm)],[f1342,f910]) ).
fof(f1334,plain,
op1(e11,e13) = op1(e12,op1(e13,e13)),
inference(backward_demodulation,[status(thm)],[f1342,f95]) ).
fof(f1335,plain,
op1(e11,e12) = op1(e13,e13),
inference(backward_demodulation,[status(thm)],[f1342,f853]) ).
fof(f1337,plain,
op1(e11,e10) = op1(e12,op1(e13,e10)),
inference(backward_demodulation,[status(thm)],[f1342,f92]) ).
fof(f1338,plain,
op1(e13,e13) = op1(e12,e11),
inference(backward_demodulation,[status(thm)],[f1342,f827]) ).
fof(f1341,plain,
op1(op1(e10,e12),e13) = op1(e10,e11),
inference(backward_demodulation,[status(thm)],[f1342,f59]) ).
fof(f1342,plain,
e11 = op1(e12,e13),
inference(forward_demodulation,[status(thm)],[f426,f425]) ).
fof(f1346,plain,
( sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != h4(e13)
| h3(e11) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != op2(e22,e23)
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1342,f1324]) ).
fof(f1347,plain,
op1(e11,e13) = op1(e13,e11),
inference(forward_demodulation,[status(thm)],[f1342,f1326]) ).
fof(f1369,plain,
( sP7_prd
| sP6_prd
| h3(op1(e13,e13)) != h4(e13)
| h3(e11) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(backward_demodulation,[status(thm)],[f1377,f1346]) ).
fof(f1375,plain,
op2(e21,e23) != e21,
inference(backward_demodulation,[status(thm)],[f1377,f359]) ).
fof(f1377,plain,
e21 = op2(e22,e23),
inference(forward_demodulation,[status(thm)],[f429,f428]) ).
fof(f1378,plain,
( sP6_prd
| h3(op1(e13,e13)) != h4(e13)
| h3(e11) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e12,e11)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1369,f520]) ).
fof(f1381,plain,
( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e20 ),
inference(backward_subsumption_resolution,[status(thm)],[f140,f1375]) ).
fof(f1406,plain,
op1(op1(e11,e12),e10) = op1(e13,op1(e13,e10)),
inference(backward_demodulation,[status(thm)],[f1335,f108]) ).
fof(f1414,plain,
op1(e12,e10) != op1(e11,e12),
inference(backward_demodulation,[status(thm)],[f1423,f326]) ).
fof(f1423,plain,
op1(e11,e12) = op1(e12,e11),
inference(forward_demodulation,[status(thm)],[f1335,f1338]) ).
fof(f1433,plain,
( sP6_prd
| h3(op1(e13,e13)) != h4(e13)
| h3(e11) != op2(e23,e22)
| h3(op1(e13,e11)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e11,e12)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1423,f1378]) ).
fof(f1434,plain,
( sP6_prd
| h3(op1(e13,e13)) != h4(e13)
| h3(e11) != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e11,e12)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1347,f1433]) ).
fof(f1435,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| h3(e11) != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e11,e12)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1335,f1434]) ).
fof(f1474,plain,
h3(e11) = op2(e22,e23),
inference(forward_demodulation,[status(thm)],[f429,f440]) ).
fof(f1475,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| e21 != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e11,e12)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(backward_demodulation,[status(thm)],[f1480,f1435]) ).
fof(f1477,plain,
( e23 = e20
| e21 = e20
| h3(e10) = e20
| sP6_prd ),
inference(backward_demodulation,[status(thm)],[f1480,f865]) ).
fof(f1480,plain,
h3(e11) = e21,
inference(forward_demodulation,[status(thm)],[f1377,f1474]) ).
fof(f1481,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| e21 != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e11,e12)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1480,f1475]) ).
fof(f1482,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| e21 != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e11,e12)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1480,f1481]) ).
fof(f1483,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| e21 != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e11,e12)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(e21,h3(e11))
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1480,f1482]) ).
fof(f1484,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| e21 != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e11,e12)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != op2(e21,e21)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1480,f1483]) ).
fof(f1485,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| e21 != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e11,e12)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(h3(e11),e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f437,f1484]) ).
fof(f1486,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| e21 != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e11,e12)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(h3(e11),e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1480,f1485]) ).
fof(f1487,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| e21 != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e11,e12)) != op2(e22,h3(e11))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1480,f1486]) ).
fof(f1488,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| e21 != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(e11) != e21
| h3(op1(e11,e12)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1480,f1487]) ).
fof(f1489,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| e21 != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,h3(e11))
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(op1(e11,e12)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1480,f1488]) ).
fof(f1490,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| e21 != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| e21 != e21
| h3(op1(e11,e12)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1480,f1489]) ).
fof(f1491,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| e21 != op2(e23,e22)
| h3(op1(e11,e13)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e11,e12)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(trivial_equality_resolution,[status(thm)],[f1490]) ).
fof(f1492,plain,
( e23 = e20
| h3(e10) = e20
| sP6_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1477,f392]) ).
fof(f1494,plain,
( h3(e10) = e20
| sP6_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1492,f394]) ).
fof(f1499,plain,
( unit2 = e22
| unit2 = e21
| unit2 = e20
| op2(e22,e23) = e22 ),
inference(paramodulation,[status(thm)],[f221,f218]) ).
fof(f1511,plain,
( unit2 = e22
| unit2 = e21
| unit2 = e20
| e21 = e22 ),
inference(forward_demodulation,[status(thm)],[f1377,f1499]) ).
fof(f1512,plain,
( unit2 = e22
| unit2 = e21
| unit2 = e20 ),
inference(forward_subsumption_resolution,[status(thm)],[f1511,f395]) ).
fof(f1514,plain,
( unit2 = e21
| unit2 = e20
| op2(e23,e22) = e23 ),
inference(paramodulation,[status(thm)],[f1512,f220]) ).
fof(f1525,plain,
( unit2 = e21
| unit2 = e20 ),
inference(forward_subsumption_resolution,[status(thm)],[f1514,f1217]) ).
fof(f1539,plain,
( unit2 = e20
| op2(e20,e21) = e20 ),
inference(paramodulation,[status(thm)],[f1525,f214]) ).
fof(f1599,plain,
op2(e23,e22) = op2(e22,op2(e22,e22)),
inference(forward_demodulation,[status(thm)],[f429,f191]) ).
fof(f1600,plain,
op2(e23,e22) = op2(e22,e23),
inference(forward_demodulation,[status(thm)],[f429,f1599]) ).
fof(f1601,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| e21 != e21
| h3(op1(e11,e13)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e11,e12)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(backward_demodulation,[status(thm)],[f1610,f1491]) ).
fof(f1610,plain,
op2(e23,e22) = e21,
inference(forward_demodulation,[status(thm)],[f1377,f1600]) ).
fof(f1611,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| h3(op1(e11,e13)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e11,e12)) != op2(e22,e21)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(trivial_equality_resolution,[status(thm)],[f1601]) ).
fof(f1613,plain,
op2(e23,e23) = op2(e22,op2(e22,e23)),
inference(forward_demodulation,[status(thm)],[f429,f192]) ).
fof(f1614,plain,
h4(e13) = op2(e22,op2(e22,e23)),
inference(forward_demodulation,[status(thm)],[f445,f1613]) ).
fof(f1627,plain,
op2(e20,e21) != h4(e13),
inference(backward_demodulation,[status(thm)],[f1628,f345]) ).
fof(f1628,plain,
h4(e13) = op2(e22,e21),
inference(forward_demodulation,[status(thm)],[f1377,f1614]) ).
fof(f1629,plain,
( sP6_prd
| h3(op1(e11,e12)) != h4(e13)
| h3(op1(e11,e13)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e11,e12)) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1628,f1611]) ).
fof(f1630,plain,
( sP6_prd
| h3(op1(e11,e13)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e11,e12)) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != op2(e21,e22)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(duplicate_literals_removal,[status(thm)],[f1629]) ).
fof(f1653,plain,
op2(e21,e21) = op2(e22,op2(e23,e21)),
inference(forward_demodulation,[status(thm)],[f1377,f194]) ).
fof(f1654,plain,
h2(e13) = op2(e22,op2(e23,e21)),
inference(forward_demodulation,[status(thm)],[f437,f1653]) ).
fof(f1674,plain,
op2(e21,e22) = op2(e22,op2(e23,e22)),
inference(forward_demodulation,[status(thm)],[f1377,f195]) ).
fof(f1675,plain,
op2(e21,e22) = op2(e22,e21),
inference(forward_demodulation,[status(thm)],[f1610,f1674]) ).
fof(f1677,plain,
( sP6_prd
| h3(op1(e11,e13)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e11,e12)) != h4(e13)
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != h4(e13)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(backward_demodulation,[status(thm)],[f1688,f1630]) ).
fof(f1688,plain,
op2(e21,e22) = h4(e13),
inference(forward_demodulation,[status(thm)],[f1628,f1675]) ).
fof(f1689,plain,
( sP6_prd
| h3(op1(e11,e13)) != op2(e23,e21)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != h4(e13)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(duplicate_literals_removal,[status(thm)],[f1677]) ).
fof(f1715,plain,
( unit2 = e20
| e20 != h4(e13) ),
inference(paramodulation,[status(thm)],[f1539,f1627]) ).
fof(f1852,plain,
op2(e21,e23) = op2(e23,op2(e22,e23)),
inference(forward_demodulation,[status(thm)],[f1610,f208]) ).
fof(f1856,plain,
( sP6_prd
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != h4(e13)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(backward_demodulation,[status(thm)],[f1866,f1689]) ).
fof(f1857,plain,
h2(e13) = op2(e22,op2(e21,e23)),
inference(backward_demodulation,[status(thm)],[f1866,f1654]) ).
fof(f1862,plain,
op2(e23,e20) != op2(e21,e23),
inference(backward_demodulation,[status(thm)],[f1866,f380]) ).
fof(f1866,plain,
op2(e21,e23) = op2(e23,e21),
inference(forward_demodulation,[status(thm)],[f1377,f1852]) ).
fof(f1868,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(op1(e11,e12)) != h4(e13)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(duplicate_literals_removal,[status(thm)],[f1856]) ).
fof(f1912,plain,
e10 = op1(op1(e12,e13),e12),
inference(forward_demodulation,[status(thm)],[f426,f424]) ).
fof(f1922,plain,
op1(e12,e10) != e10,
inference(backward_demodulation,[status(thm)],[f1937,f1414]) ).
fof(f1925,plain,
e10 = op1(e12,e11),
inference(backward_demodulation,[status(thm)],[f1937,f1423]) ).
fof(f1926,plain,
e10 = op1(e13,e13),
inference(backward_demodulation,[status(thm)],[f1937,f1335]) ).
fof(f1932,plain,
op1(e10,e12) != e10,
inference(backward_demodulation,[status(thm)],[f1937,f302]) ).
fof(f1933,plain,
op1(e10,e12) = op1(e11,e13),
inference(backward_demodulation,[status(thm)],[f1937,f719]) ).
fof(f1937,plain,
e10 = op1(e11,e12),
inference(forward_demodulation,[status(thm)],[f1342,f1912]) ).
fof(f2000,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e11,e13)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f1937,f1868]) ).
fof(f2014,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(e10) != h4(e13)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(backward_demodulation,[status(thm)],[f1933,f2000]) ).
fof(f2060,plain,
e20 = op2(op2(e22,e23),e22),
inference(forward_demodulation,[status(thm)],[f429,f427]) ).
fof(f2061,plain,
e20 = h4(e13),
inference(backward_demodulation,[status(thm)],[f2062,f1688]) ).
fof(f2062,plain,
e20 = op2(e21,e22),
inference(forward_demodulation,[status(thm)],[f1377,f2060]) ).
fof(f2064,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(e10) != e20
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(backward_demodulation,[status(thm)],[f2061,f2014]) ).
fof(f2072,plain,
( unit2 = e20
| e20 != e20 ),
inference(backward_demodulation,[status(thm)],[f2061,f1715]) ).
fof(f2086,plain,
op2(e21,e23) != e20,
inference(backward_demodulation,[status(thm)],[f2061,f1239]) ).
fof(f2094,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(h3(e10),h3(e10)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2064,f1494]) ).
fof(f2097,plain,
unit2 = e20,
inference(trivial_equality_resolution,[status(thm)],[f2072]) ).
fof(f2138,plain,
op2(e23,e20) = e23,
inference(backward_demodulation,[status(thm)],[f2097,f220]) ).
fof(f2139,plain,
op2(e20,e23) = e23,
inference(backward_demodulation,[status(thm)],[f2097,f219]) ).
fof(f2140,plain,
op2(e22,e20) = e22,
inference(backward_demodulation,[status(thm)],[f2097,f218]) ).
fof(f2141,plain,
op2(e20,e22) = e22,
inference(backward_demodulation,[status(thm)],[f2097,f217]) ).
fof(f2142,plain,
op2(e21,e20) = e21,
inference(backward_demodulation,[status(thm)],[f2097,f216]) ).
fof(f2143,plain,
op2(e20,e21) = e21,
inference(backward_demodulation,[status(thm)],[f2097,f215]) ).
fof(f2144,plain,
op2(e20,e20) = e20,
inference(backward_demodulation,[status(thm)],[f2097,f214]) ).
fof(f2171,plain,
h3(e10) = op2(op2(e22,e23),e22),
inference(forward_demodulation,[status(thm)],[f429,f439]) ).
fof(f2172,plain,
h3(e10) = op2(e21,e22),
inference(forward_demodulation,[status(thm)],[f1377,f2171]) ).
fof(f2174,plain,
( e20 != e20
| ~ sP6_prd ),
inference(backward_demodulation,[status(thm)],[f2175,f513]) ).
fof(f2175,plain,
h3(e10) = e20,
inference(forward_demodulation,[status(thm)],[f2062,f2172]) ).
fof(f2176,plain,
~ sP6_prd,
inference(trivial_equality_resolution,[status(thm)],[f2174]) ).
fof(f2189,plain,
( op1(e10,e12) = e12
| op1(e10,e12) = e11 ),
inference(forward_subsumption_resolution,[status(thm)],[f908,f1932]) ).
fof(f2198,plain,
( op1(e10,e12) = e11
| op1(e12,e12) = op1(e10,e13) ),
inference(paramodulation,[status(thm)],[f2189,f663]) ).
fof(f2209,plain,
( op1(e10,e12) = e11
| e13 = op1(e10,e13) ),
inference(forward_demodulation,[status(thm)],[f426,f2198]) ).
fof(f2210,plain,
e13 = op1(e10,e13),
inference(forward_subsumption_resolution,[status(thm)],[f2209,f1332]) ).
fof(f2214,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(e20,h3(e10)) ),
inference(forward_demodulation,[status(thm)],[f2175,f2094]) ).
fof(f2215,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != op2(e20,e20) ),
inference(forward_demodulation,[status(thm)],[f2175,f2214]) ).
fof(f2216,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(h3(e10),e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(forward_demodulation,[status(thm)],[f433,f2215]) ).
fof(f2217,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(h3(e10),e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(forward_demodulation,[status(thm)],[f2175,f2216]) ).
fof(f2218,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(h3(e10),e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(forward_demodulation,[status(thm)],[f2175,f2217]) ).
fof(f2219,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,h3(e10))
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(forward_demodulation,[status(thm)],[f2175,f2218]) ).
fof(f2220,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,h3(e10))
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(forward_demodulation,[status(thm)],[f2175,f2219]) ).
fof(f2221,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,h3(e10))
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(forward_demodulation,[status(thm)],[f2175,f2220]) ).
fof(f2222,plain,
( sP6_prd
| h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(forward_demodulation,[status(thm)],[f2175,f2221]) ).
fof(f2223,plain,
( h3(op1(e13,e10)) != op2(e23,e20)
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(forward_subsumption_resolution,[status(thm)],[f2222,f2176]) ).
fof(f2231,plain,
( op1(e12,e10) = e12
| op1(e12,e10) = e11 ),
inference(forward_subsumption_resolution,[status(thm)],[f1096,f1922]) ).
fof(f2235,plain,
( op1(e12,e10) = e11
| op1(e13,e10) = op1(e12,e12) ),
inference(paramodulation,[status(thm)],[f2231,f812]) ).
fof(f2240,plain,
( op1(e12,e10) = e11
| op1(e13,e10) = e13 ),
inference(forward_demodulation,[status(thm)],[f426,f2235]) ).
fof(f2241,plain,
op1(e13,e10) = e13,
inference(forward_subsumption_resolution,[status(thm)],[f2240,f1319]) ).
fof(f2246,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != op2(e20,e22)
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(backward_demodulation,[status(thm)],[f2138,f2223]) ).
fof(f2247,plain,
e23 != op2(e21,e23),
inference(backward_demodulation,[status(thm)],[f2138,f1862]) ).
fof(f2306,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e13)) != op2(e20,e23)
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(forward_demodulation,[status(thm)],[f2141,f2246]) ).
fof(f2307,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e12,e10)) != op2(e22,e20)
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e13)) != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(forward_demodulation,[status(thm)],[f2139,f2306]) ).
fof(f2308,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != op2(e21,e20)
| h3(op1(e10,e13)) != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(forward_demodulation,[status(thm)],[f2140,f2307]) ).
fof(f2313,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e13)) != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != h1(e13) ),
inference(backward_demodulation,[status(thm)],[f2142,f2308]) ).
fof(f2339,plain,
h1(e13) = e20,
inference(backward_demodulation,[status(thm)],[f2144,f433]) ).
fof(f2437,plain,
op1(e11,e11) = op1(e13,e10),
inference(forward_demodulation,[status(thm)],[f1925,f1330]) ).
fof(f2445,plain,
op1(e11,e11) = e13,
inference(forward_demodulation,[status(thm)],[f2241,f2437]) ).
fof(f2455,plain,
op1(e10,e12) = op1(e12,op1(e13,e13)),
inference(forward_demodulation,[status(thm)],[f1933,f1334]) ).
fof(f2467,plain,
op1(e10,e12) = op1(e12,e10),
inference(forward_demodulation,[status(thm)],[f1926,f2455]) ).
fof(f2473,plain,
op1(e11,e10) = op1(e12,e13),
inference(forward_demodulation,[status(thm)],[f2241,f1337]) ).
fof(f2482,plain,
op1(e11,e10) = e11,
inference(forward_demodulation,[status(thm)],[f1342,f2473]) ).
fof(f2490,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e13)) != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != op2(e20,e21)
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f2339,f2313]) ).
fof(f2491,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != e21
| h3(op1(e10,e13)) != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f2143,f2490]) ).
fof(f2492,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != e21
| h3(e13) != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f2210,f2491]) ).
fof(f2493,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(op1(e11,e10)) != e21
| e23 != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f758,f2492]) ).
fof(f2494,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| h3(e11) != e21
| e23 != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f2482,f2493]) ).
fof(f2495,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(op1(e11,e11)) != h2(e13)
| e21 != e21
| e23 != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1480,f2494]) ).
fof(f2496,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e10,e12)) != op2(e21,e23)
| h3(e13) != h2(e13)
| e21 != e21
| e23 != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f2445,f2495]) ).
fof(f2497,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e12,e10)) != e22
| h3(op1(e10,e12)) != op2(e21,e23)
| e23 != h2(e13)
| e21 != e21
| e23 != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f758,f2496]) ).
fof(f2498,plain,
( h3(op1(e13,e10)) != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e12)) != op2(e21,e23)
| e23 != h2(e13)
| e21 != e21
| e23 != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f2467,f2497]) ).
fof(f2499,plain,
( h3(e13) != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e12)) != op2(e21,e23)
| e23 != h2(e13)
| e21 != e21
| e23 != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f2241,f2498]) ).
fof(f2500,plain,
( e23 != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e12)) != op2(e21,e23)
| e23 != h2(e13)
| e21 != e21
| e23 != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f758,f2499]) ).
fof(f2501,plain,
( h3(op1(e10,e12)) != op2(e21,e23)
| e23 != h2(e13)
| e21 != e21
| e23 != e23
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(duplicate_literals_removal,[status(thm)],[f2500]) ).
fof(f2502,plain,
( h3(op1(e10,e12)) != op2(e21,e23)
| e23 != h2(e13)
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(trivial_equality_resolution,[status(thm)],[f2501]) ).
fof(f2503,plain,
( op1(e10,e12) = e11
| h3(e12) != op2(e21,e23)
| e23 != h2(e13)
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(paramodulation,[status(thm)],[f2189,f2502]) ).
fof(f2504,plain,
( op1(e10,e12) = e11
| e22 != op2(e21,e23)
| e23 != h2(e13)
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f438,f2503]) ).
fof(f2505,plain,
( e22 != op2(e21,e23)
| e23 != h2(e13)
| h3(op1(e10,e12)) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_subsumption_resolution,[status(thm)],[f2504,f1332]) ).
fof(f2562,plain,
( op1(e10,e12) = e11
| op1(e12,e13) = op1(e10,e11) ),
inference(paramodulation,[status(thm)],[f2189,f1341]) ).
fof(f2563,plain,
( op1(e10,e12) = e11
| e11 = op1(e10,e11) ),
inference(forward_demodulation,[status(thm)],[f1342,f2562]) ).
fof(f2564,plain,
e11 = op1(e10,e11),
inference(forward_subsumption_resolution,[status(thm)],[f2563,f1332]) ).
fof(f2594,plain,
( op1(e10,e12) = e11
| e22 != op2(e21,e23)
| e23 != h2(e13)
| h3(e12) != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(paramodulation,[status(thm)],[f2189,f2505]) ).
fof(f2596,plain,
( op1(e10,e12) = e11
| e22 != op2(e21,e23)
| e23 != h2(e13)
| e22 != e22
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f438,f2594]) ).
fof(f2597,plain,
( op1(e10,e12) = e11
| e22 != op2(e21,e23)
| e23 != h2(e13)
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(trivial_equality_resolution,[status(thm)],[f2596]) ).
fof(f2598,plain,
( e22 != op2(e21,e23)
| e23 != h2(e13)
| h3(op1(e10,e11)) != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_subsumption_resolution,[status(thm)],[f2597,f1332]) ).
fof(f2617,plain,
( e22 != op2(e21,e23)
| e23 != h2(e13)
| h3(e11) != e21
| h3(op1(e10,e10)) != e20 ),
inference(backward_demodulation,[status(thm)],[f2564,f2598]) ).
fof(f2627,plain,
( e22 != op2(e21,e23)
| e23 != h2(e13)
| e21 != e21
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f1480,f2617]) ).
fof(f2628,plain,
( e22 != op2(e21,e23)
| e23 != h2(e13)
| h3(op1(e10,e10)) != e20 ),
inference(trivial_equality_resolution,[status(thm)],[f2627]) ).
fof(f2652,plain,
( op2(e21,e23) = e23
| op2(e21,e23) = e22 ),
inference(forward_subsumption_resolution,[status(thm)],[f1381,f2086]) ).
fof(f2653,plain,
op2(e21,e23) = e22,
inference(resolution,[status(thm)],[f2652,f2247]) ).
fof(f2728,plain,
( e22 != e22
| e23 != h2(e13)
| h3(op1(e10,e10)) != e20 ),
inference(backward_demodulation,[status(thm)],[f2653,f2628]) ).
fof(f2732,plain,
h2(e13) = op2(e22,e22),
inference(backward_demodulation,[status(thm)],[f2653,f1857]) ).
fof(f2738,plain,
( e23 != h2(e13)
| h3(op1(e10,e10)) != e20 ),
inference(trivial_equality_resolution,[status(thm)],[f2728]) ).
fof(f2739,plain,
h2(e13) = e23,
inference(forward_demodulation,[status(thm)],[f429,f2732]) ).
fof(f2852,plain,
( e23 != e23
| h3(op1(e10,e10)) != e20 ),
inference(forward_demodulation,[status(thm)],[f2739,f2738]) ).
fof(f2853,plain,
h3(op1(e10,e10)) != e20,
inference(trivial_equality_resolution,[status(thm)],[f2852]) ).
fof(f2911,plain,
op1(e10,e10) = op1(e13,op1(e13,e10)),
inference(forward_demodulation,[status(thm)],[f1937,f1406]) ).
fof(f2912,plain,
op1(e10,e10) = op1(e13,e13),
inference(forward_demodulation,[status(thm)],[f2241,f2911]) ).
fof(f2913,plain,
h3(e10) != e20,
inference(backward_demodulation,[status(thm)],[f2918,f2853]) ).
fof(f2918,plain,
op1(e10,e10) = e10,
inference(forward_demodulation,[status(thm)],[f1926,f2912]) ).
fof(f2919,plain,
e20 != e20,
inference(forward_demodulation,[status(thm)],[f2175,f2913]) ).
fof(f2920,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f2919]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG016+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n007.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 12:51:21 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 1.29/0.64 % Refutation found
% 1.29/0.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.29/0.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.29/0.67 % Elapsed time: 0.294405 seconds
% 1.29/0.67 % CPU time: 1.975836 seconds
% 1.29/0.67 % Total memory used: 161.096 MB
% 1.29/0.67 % Net memory used: 158.600 MB
%------------------------------------------------------------------------------