%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG121+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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 11:48:18 AM UTC 2026
% Result : Theorem 0.14s 0.61s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 144
% Syntax : Number of formulae : 693 ( 120 unt; 128 def)
% Number of atoms : 2863 (1957 equ)
% Maximal formula atoms : 128 ( 4 avg)
% Number of connectives : 3338 (1168 ~;1371 |; 671 &)
% ( 128 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 130 ( 128 usr; 129 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 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(e13,e13) = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| op1(e10,e13) = e13 )
& ( op1(e13,e13) = e13
| op1(e13,e12) = e13
| op1(e13,e11) = e13
| op1(e13,e10) = e13 )
& ( op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 )
& ( op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 )
& ( op1(e13,e13) = e11
| op1(e12,e13) = e11
| op1(e11,e13) = e11
| op1(e10,e13) = e11 )
& ( op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 )
& ( op1(e13,e13) = e10
| op1(e12,e13) = e10
| op1(e11,e13) = e10
| op1(e10,e13) = e10 )
& ( op1(e13,e13) = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 )
& ( op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| op1(e10,e12) = e13 )
& ( op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 )
& ( op1(e13,e12) = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 )
& ( op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 )
& ( op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 )
& ( op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 )
& ( op1(e13,e12) = e10
| op1(e12,e12) = e10
| op1(e11,e12) = e10
| op1(e10,e12) = e10 )
& ( op1(e12,e13) = e10
| op1(e12,e12) = e10
| op1(e12,e11) = e10
| op1(e12,e10) = e10 )
& ( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| op1(e10,e11) = e13 )
& ( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e11) = e13
| op1(e11,e10) = e13 )
& ( op1(e13,e11) = e12
| op1(e12,e11) = e12
| op1(e11,e11) = e12
| op1(e10,e11) = e12 )
& ( op1(e11,e13) = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 )
& ( op1(e13,e11) = e11
| op1(e12,e11) = e11
| op1(e11,e11) = e11
| op1(e10,e11) = e11 )
& ( op1(e11,e13) = e11
| op1(e11,e12) = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 )
& ( op1(e13,e11) = e10
| op1(e12,e11) = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 )
& ( op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 )
& ( op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| op1(e10,e10) = e13 )
& ( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 )
& ( op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| op1(e10,e10) = e12 )
& ( op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 )
& ( op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11
| op1(e10,e10) = e11 )
& ( op1(e10,e13) = e11
| op1(e10,e12) = e11
| op1(e10,e11) = e11
| op1(e10,e10) = e11 )
& ( op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 )
& ( op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
( ( op2(e23,e23) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e23,e23) = e20 )
& ( op2(e23,e22) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21
| op2(e23,e22) = e20 )
& ( op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e23,e21) = e21
| op2(e23,e21) = e20 )
& ( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 )
& ( op2(e22,e23) = e23
| op2(e22,e23) = e22
| op2(e22,e23) = e21
| op2(e22,e23) = e20 )
& ( op2(e22,e22) = e23
| op2(e22,e22) = e22
| op2(e22,e22) = e21
| op2(e22,e22) = e20 )
& ( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 )
& ( op2(e22,e20) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 )
& ( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| op2(e21,e23) = e20 )
& ( op2(e21,e22) = e23
| op2(e21,e22) = e22
| op2(e21,e22) = e21
| op2(e21,e22) = e20 )
& ( op2(e21,e21) = e23
| op2(e21,e21) = e22
| op2(e21,e21) = e21
| op2(e21,e21) = e20 )
& ( op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e21
| op2(e21,e20) = e20 )
& ( op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 )
& ( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| op2(e20,e22) = e20 )
& ( op2(e20,e21) = e23
| op2(e20,e21) = e22
| op2(e20,e21) = e21
| op2(e20,e21) = e20 )
& ( op2(e20,e20) = e23
| op2(e20,e20) = e22
| op2(e20,e20) = e21
| op2(e20,e20) = e20 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
( ( op2(e23,e23) = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| op2(e20,e23) = e23 )
& ( op2(e23,e23) = e23
| op2(e23,e22) = e23
| op2(e23,e21) = e23
| op2(e23,e20) = e23 )
& ( op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 )
& ( op2(e23,e23) = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 )
& ( op2(e23,e23) = e21
| op2(e22,e23) = e21
| op2(e21,e23) = e21
| op2(e20,e23) = e21 )
& ( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 )
& ( op2(e23,e23) = e20
| op2(e22,e23) = e20
| op2(e21,e23) = e20
| op2(e20,e23) = e20 )
& ( op2(e23,e23) = e20
| op2(e23,e22) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 )
& ( op2(e23,e22) = e23
| op2(e22,e22) = e23
| op2(e21,e22) = e23
| op2(e20,e22) = e23 )
& ( op2(e22,e23) = e23
| op2(e22,e22) = e23
| op2(e22,e21) = e23
| op2(e22,e20) = e23 )
& ( op2(e23,e22) = e22
| op2(e22,e22) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 )
& ( op2(e22,e23) = e22
| op2(e22,e22) = e22
| op2(e22,e21) = e22
| op2(e22,e20) = e22 )
& ( op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 )
& ( op2(e22,e23) = e21
| op2(e22,e22) = e21
| op2(e22,e21) = e21
| op2(e22,e20) = e21 )
& ( op2(e23,e22) = e20
| op2(e22,e22) = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 )
& ( op2(e22,e23) = e20
| op2(e22,e22) = e20
| op2(e22,e21) = e20
| op2(e22,e20) = e20 )
& ( op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e21,e21) = e23
| op2(e20,e21) = e23 )
& ( op2(e21,e23) = e23
| op2(e21,e22) = e23
| op2(e21,e21) = e23
| op2(e21,e20) = e23 )
& ( op2(e23,e21) = e22
| op2(e22,e21) = e22
| op2(e21,e21) = e22
| op2(e20,e21) = e22 )
& ( op2(e21,e23) = e22
| op2(e21,e22) = e22
| op2(e21,e21) = e22
| op2(e21,e20) = e22 )
& ( op2(e23,e21) = e21
| op2(e22,e21) = e21
| op2(e21,e21) = e21
| op2(e20,e21) = e21 )
& ( op2(e21,e23) = e21
| op2(e21,e22) = e21
| op2(e21,e21) = e21
| op2(e21,e20) = e21 )
& ( op2(e23,e21) = e20
| op2(e22,e21) = e20
| op2(e21,e21) = e20
| op2(e20,e21) = e20 )
& ( op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20
| op2(e21,e20) = e20 )
& ( op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| op2(e20,e20) = e23 )
& ( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 )
& ( op2(e23,e20) = e22
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| op2(e20,e20) = e22 )
& ( op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| op2(e20,e20) = e22 )
& ( op2(e23,e20) = e21
| op2(e22,e20) = e21
| op2(e21,e20) = e21
| op2(e20,e20) = e21 )
& ( op2(e20,e23) = e21
| op2(e20,e22) = e21
| op2(e20,e21) = e21
| op2(e20,e20) = e21 )
& ( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| op2(e20,e20) = e20 )
& ( op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
( op1(e13,e12) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e11)
& op1(e12,e12) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e11)
& op1(e11,e12) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e11)
& op1(e10,e12) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e11)
& op1(e12,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e11,e13)
& op1(e12,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e11,e12)
& op1(e12,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e11,e11)
& op1(e12,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e11,e10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
( op2(e23,e22) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e21)
& op2(e22,e22) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e21)
& op2(e21,e22) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e21)
& op2(e20,e22) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e21)
& op2(e22,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e21,e23)
& op2(e22,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e21,e22)
& op2(e22,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e21,e21)
& op2(e22,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e21,e20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
( e12 != e13
& e11 != e13
& e11 != e12
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
( e22 != e23
& e21 != e23
& e21 != e22
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
( ( ( op1(e13,e13) != e13
& op1(e13,e13) = e13
& op1(e13,e13) = e13 )
| ( op1(e12,e12) != e12
& op1(e12,e13) = e13
& op1(e13,e12) = e13 )
| ( op1(e11,e11) != e11
& op1(e11,e13) = e13
& op1(e13,e11) = e13 )
| ( op1(e10,e10) != e10
& op1(e10,e13) = e13
& op1(e13,e10) = e13 )
| ( op1(e13,e13) != e13
& op1(e13,e12) = e12
& op1(e12,e13) = e12 )
| ( op1(e12,e12) != e12
& op1(e12,e12) = e12
& op1(e12,e12) = e12 )
| ( op1(e11,e11) != e11
& op1(e11,e12) = e12
& op1(e12,e11) = e12 )
| ( op1(e10,e10) != e10
& op1(e10,e12) = e12
& op1(e12,e10) = e12 )
| ( op1(e13,e13) != e13
& op1(e13,e11) = e11
& op1(e11,e13) = e11 )
| ( op1(e12,e12) != e12
& op1(e12,e11) = e11
& op1(e11,e12) = e11 )
| ( op1(e11,e11) != e11
& op1(e11,e11) = e11
& op1(e11,e11) = e11 )
| ( op1(e10,e10) != e10
& op1(e10,e11) = e11
& op1(e11,e10) = e11 )
| ( op1(e13,e13) != e13
& op1(e13,e10) = e10
& op1(e10,e13) = e10 )
| ( op1(e12,e12) != e12
& op1(e12,e10) = e10
& op1(e10,e12) = e10 )
| ( op1(e11,e11) != e11
& op1(e11,e10) = e10
& op1(e10,e11) = e10 )
| ( op1(e10,e10) != e10
& op1(e10,e10) = e10
& op1(e10,e10) = e10 ) )
& ( op1(e13,e13) = e13
| op1(e13,e13) != e13 )
& ( op1(e13,e12) = e13
| op1(e13,e13) != e12 )
& ( op1(e13,e11) = e13
| op1(e13,e13) != e11 )
& ( op1(e13,e10) = e13
| op1(e13,e13) != e10 )
& ( op1(e12,e13) = e12
| op1(e12,e12) != e13 )
& ( op1(e12,e12) = e12
| op1(e12,e12) != e12 )
& ( op1(e12,e11) = e12
| op1(e12,e12) != e11 )
& ( op1(e12,e10) = e12
| op1(e12,e12) != e10 )
& ( op1(e11,e13) = e11
| op1(e11,e11) != e13 )
& ( op1(e11,e12) = e11
| op1(e11,e11) != e12 )
& ( op1(e11,e11) = e11
| op1(e11,e11) != e11 )
& ( op1(e11,e10) = e11
| op1(e11,e11) != e10 )
& ( op1(e10,e13) = e10
| op1(e10,e10) != e13 )
& ( op1(e10,e12) = e10
| op1(e10,e10) != e12 )
& ( op1(e10,e11) = e10
| op1(e10,e10) != e11 )
& ( op1(e10,e10) = e10
| op1(e10,e10) != e10 )
& ( op1(e13,e13) = e13
| op1(e12,e12) = e12
| op1(e11,e11) = e11
| op1(e10,e10) = e10 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
( ( ( op2(e23,e23) != e23
& op2(e23,e23) = e23
& op2(e23,e23) = e23 )
| ( op2(e22,e22) != e22
& op2(e22,e23) = e23
& op2(e23,e22) = e23 )
| ( op2(e21,e21) != e21
& op2(e21,e23) = e23
& op2(e23,e21) = e23 )
| ( op2(e20,e20) != e20
& op2(e20,e23) = e23
& op2(e23,e20) = e23 )
| ( op2(e23,e23) != e23
& op2(e23,e22) = e22
& op2(e22,e23) = e22 )
| ( op2(e22,e22) != e22
& op2(e22,e22) = e22
& op2(e22,e22) = e22 )
| ( op2(e21,e21) != e21
& op2(e21,e22) = e22
& op2(e22,e21) = e22 )
| ( op2(e20,e20) != e20
& op2(e20,e22) = e22
& op2(e22,e20) = e22 )
| ( op2(e23,e23) != e23
& op2(e23,e21) = e21
& op2(e21,e23) = e21 )
| ( op2(e22,e22) != e22
& op2(e22,e21) = e21
& op2(e21,e22) = e21 )
| ( op2(e21,e21) != e21
& op2(e21,e21) = e21
& op2(e21,e21) = e21 )
| ( op2(e20,e20) != e20
& op2(e20,e21) = e21
& op2(e21,e20) = e21 )
| ( op2(e23,e23) != e23
& op2(e23,e20) = e20
& op2(e20,e23) = e20 )
| ( op2(e22,e22) != e22
& op2(e22,e20) = e20
& op2(e20,e22) = e20 )
| ( op2(e21,e21) != e21
& op2(e21,e20) = e20
& op2(e20,e21) = e20 )
| ( op2(e20,e20) != e20
& op2(e20,e20) = e20
& op2(e20,e20) = e20 ) )
& ( op2(e23,e23) = e23
| op2(e23,e23) != e23 )
& ( op2(e23,e22) = e23
| op2(e23,e23) != e22 )
& ( op2(e23,e21) = e23
| op2(e23,e23) != e21 )
& ( op2(e23,e20) = e23
| op2(e23,e23) != e20 )
& ( op2(e22,e23) = e22
| op2(e22,e22) != e23 )
& ( op2(e22,e22) = e22
| op2(e22,e22) != e22 )
& ( op2(e22,e21) = e22
| op2(e22,e22) != e21 )
& ( op2(e22,e20) = e22
| op2(e22,e22) != e20 )
& ( op2(e21,e23) = e21
| op2(e21,e21) != e23 )
& ( op2(e21,e22) = e21
| op2(e21,e21) != e22 )
& ( op2(e21,e21) = e21
| op2(e21,e21) != e21 )
& ( op2(e21,e20) = e21
| op2(e21,e21) != e20 )
& ( op2(e20,e23) = e20
| op2(e20,e20) != e23 )
& ( op2(e20,e22) = e20
| op2(e20,e20) != e22 )
& ( op2(e20,e21) = e20
| op2(e20,e20) != e21 )
& ( op2(e20,e20) = e20
| op2(e20,e20) != e20 )
& ( op2(e23,e23) = e23
| op2(e22,e22) = e22
| op2(e21,e21) = e21
| op2(e20,e20) = e20 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
( e12 = op1(op1(op1(e13,e13),op1(e13,e13)),e13)
& e11 = op1(op1(e13,e13),op1(e13,e13))
& e10 = op1(e13,e13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
( e22 = op2(op2(op2(e23,e23),op2(e23,e23)),e23)
& e21 = op2(op2(e23,e23),op2(e23,e23))
& e20 = op2(e23,e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
( h1(e12) = op2(op2(op2(e20,e20),op2(e20,e20)),e20)
& h1(e11) = op2(op2(e20,e20),op2(e20,e20))
& h1(e10) = op2(e20,e20)
& h1(e13) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
( h3(e12) = op2(op2(op2(e22,e22),op2(e22,e22)),e22)
& h3(e11) = op2(op2(e22,e22),op2(e22,e22))
& h3(e10) = op2(e22,e22)
& h3(e13) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
( h4(e12) = op2(op2(op2(e23,e23),op2(e23,e23)),e23)
& h4(e11) = op2(op2(e23,e23),op2(e23,e23))
& h4(e10) = op2(e23,e23)
& h4(e13) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,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(f19,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)],[f18]) ).
fof(f20,plain,
( op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e11
| op1(e10,e10) = e10 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f22,plain,
( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f24,plain,
( op1(e11,e10) = e13
| op1(e11,e10) = e12
| op1(e11,e10) = e11
| op1(e11,e10) = e10 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f30,plain,
( op1(e12,e12) = e13
| op1(e12,e12) = e12
| op1(e12,e12) = e11
| op1(e12,e12) = e10 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f34,plain,
( op1(e13,e12) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11
| op1(e13,e12) = e10 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f35,plain,
( op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e13,e13) = e10 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f42,plain,
( op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f46,plain,
( op1(e11,e13) = e11
| op1(e11,e12) = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f49,plain,
( op1(e13,e11) = e12
| op1(e12,e11) = e12
| op1(e11,e11) = e12
| op1(e10,e11) = e12 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f50,plain,
( op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e11) = e13
| op1(e11,e10) = e13 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f51,plain,
( op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| op1(e10,e11) = e13 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f63,plain,
( op1(e13,e13) = e11
| op1(e12,e13) = e11
| op1(e11,e13) = e11
| op1(e10,e13) = e11 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f74,plain,
( op2(e21,e22) = e23
| op2(e21,e22) = e22
| op2(e21,e22) = e21
| op2(e21,e22) = e20 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f77,plain,
( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f79,plain,
( op2(e22,e23) = e23
| op2(e22,e23) = e22
| op2(e22,e23) = e21
| op2(e22,e23) = e20 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f85,plain,
( op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| op2(e20,e20) = e20 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f89,plain,
( op2(e23,e20) = e22
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| op2(e20,e20) = e22 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f90,plain,
( op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f97,plain,
( op2(e23,e21) = e22
| op2(e22,e21) = e22
| op2(e21,e21) = e22
| op2(e20,e21) = e22 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f101,plain,
( op2(e23,e22) = e20
| op2(e22,e22) = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f105,plain,
( op2(e23,e22) = e22
| op2(e22,e22) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f108,plain,
( op2(e23,e23) = e20
| op2(e23,e22) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f110,plain,
( op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f116,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f120,plain,
op1(e11,e10) != op1(e13,e10),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f128,plain,
op1(e10,e12) != op1(e11,e12),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f129,plain,
op1(e10,e12) != op1(e12,e12),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f130,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f131,plain,
op1(e11,e12) != op1(e12,e12),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f132,plain,
op1(e11,e12) != op1(e13,e12),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f141,plain,
op1(e10,e10) != op1(e10,e12),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f143,plain,
op1(e10,e11) != op1(e10,e12),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f148,plain,
op1(e11,e10) != op1(e11,e13),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f157,plain,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f158,plain,
op1(e13,e10) != op1(e13,e11),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f159,plain,
op1(e13,e10) != op1(e13,e12),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f163,plain,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f166,plain,
op2(e20,e20) != op2(e23,e20),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f171,plain,
op2(e20,e21) != op2(e22,e21),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f172,plain,
op2(e20,e21) != op2(e23,e21),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f174,plain,
op2(e21,e21) != op2(e23,e21),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f180,plain,
op2(e21,e22) != op2(e23,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f183,plain,
op2(e20,e23) != op2(e22,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f187,plain,
op2(e22,e23) != op2(e23,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f191,plain,
op2(e20,e21) != op2(e20,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f195,plain,
op2(e21,e20) != op2(e21,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f196,plain,
op2(e21,e20) != op2(e21,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f199,plain,
op2(e21,e22) != op2(e21,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f200,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f201,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f202,plain,
op2(e22,e20) != op2(e22,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f204,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f208,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f209,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f211,plain,
op2(e23,e22) != op2(e23,e23),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f212,plain,
e10 != e11,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f213,plain,
e10 != e12,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f214,plain,
e10 != e13,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f215,plain,
e11 != e12,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f216,plain,
e11 != e13,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f217,plain,
e12 != e13,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f218,plain,
e20 != e21,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f219,plain,
e20 != e22,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f220,plain,
e20 != e23,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f222,plain,
e21 != e23,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f223,plain,
e22 != e23,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f240,definition,
( sP0_prd
<=> ( ( op1(e12,e12) != e12
& op1(e12,e13) = e13
& op1(e13,e12) = e13 )
| ( op1(e11,e11) != e11
& op1(e11,e13) = e13
& op1(e13,e11) = e13 )
| ( op1(e10,e10) != e10
& op1(e10,e13) = e13
& op1(e13,e10) = e13 )
| ( op1(e13,e13) != e13
& op1(e13,e12) = e12
& op1(e12,e13) = e12 )
| ( op1(e12,e12) != e12
& op1(e12,e12) = e12
& op1(e12,e12) = e12 )
| ( op1(e11,e11) != e11
& op1(e11,e12) = e12
& op1(e12,e11) = e12 )
| ( op1(e10,e10) != e10
& op1(e10,e12) = e12
& op1(e12,e10) = e12 )
| ( op1(e13,e13) != e13
& op1(e13,e11) = e11
& op1(e11,e13) = e11 )
| ( op1(e12,e12) != e12
& op1(e12,e11) = e11
& op1(e11,e12) = e11 )
| ( op1(e11,e11) != e11
& op1(e11,e11) = e11
& op1(e11,e11) = e11 )
| ( op1(e10,e10) != e10
& op1(e10,e11) = e11
& op1(e11,e10) = e11 )
| ( op1(e13,e13) != e13
& op1(e13,e10) = e10
& op1(e10,e13) = e10 )
| ( op1(e12,e12) != e12
& op1(e12,e10) = e10
& op1(e10,e12) = e10 )
| ( op1(e11,e11) != e11
& op1(e11,e10) = e10
& op1(e10,e11) = e10 )
| ( op1(e10,e10) != e10
& op1(e10,e10) = e10
& op1(e10,e10) = e10 ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f241,plain,
( ( ( op1(e13,e13) != e13
& op1(e13,e13) = e13
& op1(e13,e13) = e13 )
| sP0_prd )
& ( op1(e13,e13) = e13
| op1(e13,e13) != e13 )
& ( op1(e13,e12) = e13
| op1(e13,e13) != e12 )
& ( op1(e13,e11) = e13
| op1(e13,e13) != e11 )
& ( op1(e13,e10) = e13
| op1(e13,e13) != e10 )
& ( op1(e12,e13) = e12
| op1(e12,e12) != e13 )
& ( op1(e12,e12) = e12
| op1(e12,e12) != e12 )
& ( op1(e12,e11) = e12
| op1(e12,e12) != e11 )
& ( op1(e12,e10) = e12
| op1(e12,e12) != e10 )
& ( op1(e11,e13) = e11
| op1(e11,e11) != e13 )
& ( op1(e11,e12) = e11
| op1(e11,e11) != e12 )
& ( op1(e11,e11) = e11
| op1(e11,e11) != e11 )
& ( op1(e11,e10) = e11
| op1(e11,e11) != e10 )
& ( op1(e10,e13) = e10
| op1(e10,e10) != e13 )
& ( op1(e10,e12) = e10
| op1(e10,e10) != e12 )
& ( op1(e10,e11) = e10
| op1(e10,e10) != e11 )
& ( op1(e10,e10) = e10
| op1(e10,e10) != e10 )
& ( op1(e13,e13) = e13
| op1(e12,e12) = e12
| op1(e11,e11) = e11
| op1(e10,e10) = e10 ) ),
inference(formula_renaming,[status(thm)],[f10,f240]) ).
fof(f244,plain,
( op1(e10,e11) = e10
| op1(e10,e10) != e11 ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f249,plain,
( op1(e11,e12) = e11
| op1(e11,e11) != e12 ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f250,plain,
( op1(e11,e13) = e11
| op1(e11,e11) != e13 ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f251,plain,
( op1(e12,e10) = e12
| op1(e12,e12) != e10 ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f255,plain,
( op1(e13,e10) = e13
| op1(e13,e13) != e10 ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f262,definition,
( sP1_prd
<=> ( ( op2(e22,e22) != e22
& op2(e22,e23) = e23
& op2(e23,e22) = e23 )
| ( op2(e21,e21) != e21
& op2(e21,e23) = e23
& op2(e23,e21) = e23 )
| ( op2(e20,e20) != e20
& op2(e20,e23) = e23
& op2(e23,e20) = e23 )
| ( op2(e23,e23) != e23
& op2(e23,e22) = e22
& op2(e22,e23) = e22 )
| ( op2(e22,e22) != e22
& op2(e22,e22) = e22
& op2(e22,e22) = e22 )
| ( op2(e21,e21) != e21
& op2(e21,e22) = e22
& op2(e22,e21) = e22 )
| ( op2(e20,e20) != e20
& op2(e20,e22) = e22
& op2(e22,e20) = e22 )
| ( op2(e23,e23) != e23
& op2(e23,e21) = e21
& op2(e21,e23) = e21 )
| ( op2(e22,e22) != e22
& op2(e22,e21) = e21
& op2(e21,e22) = e21 )
| ( op2(e21,e21) != e21
& op2(e21,e21) = e21
& op2(e21,e21) = e21 )
| ( op2(e20,e20) != e20
& op2(e20,e21) = e21
& op2(e21,e20) = e21 )
| ( op2(e23,e23) != e23
& op2(e23,e20) = e20
& op2(e20,e23) = e20 )
| ( op2(e22,e22) != e22
& op2(e22,e20) = e20
& op2(e20,e22) = e20 )
| ( op2(e21,e21) != e21
& op2(e21,e20) = e20
& op2(e20,e21) = e20 )
| ( op2(e20,e20) != e20
& op2(e20,e20) = e20
& op2(e20,e20) = e20 ) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f263,plain,
( ( ( op2(e23,e23) != e23
& op2(e23,e23) = e23
& op2(e23,e23) = e23 )
| sP1_prd )
& ( op2(e23,e23) = e23
| op2(e23,e23) != e23 )
& ( op2(e23,e22) = e23
| op2(e23,e23) != e22 )
& ( op2(e23,e21) = e23
| op2(e23,e23) != e21 )
& ( op2(e23,e20) = e23
| op2(e23,e23) != e20 )
& ( op2(e22,e23) = e22
| op2(e22,e22) != e23 )
& ( op2(e22,e22) = e22
| op2(e22,e22) != e22 )
& ( op2(e22,e21) = e22
| op2(e22,e22) != e21 )
& ( op2(e22,e20) = e22
| op2(e22,e22) != e20 )
& ( op2(e21,e23) = e21
| op2(e21,e21) != e23 )
& ( op2(e21,e22) = e21
| op2(e21,e21) != e22 )
& ( op2(e21,e21) = e21
| op2(e21,e21) != e21 )
& ( op2(e21,e20) = e21
| op2(e21,e21) != e20 )
& ( op2(e20,e23) = e20
| op2(e20,e20) != e23 )
& ( op2(e20,e22) = e20
| op2(e20,e20) != e22 )
& ( op2(e20,e21) = e20
| op2(e20,e20) != e21 )
& ( op2(e20,e20) = e20
| op2(e20,e20) != e20 )
& ( op2(e23,e23) = e23
| op2(e22,e22) = e22
| op2(e21,e21) = e21
| op2(e20,e20) = e20 ) ),
inference(formula_renaming,[status(thm)],[f11,f262]) ).
fof(f264,plain,
( op2(e23,e23) = e23
| op2(e22,e22) = e22
| op2(e21,e21) = e21
| op2(e20,e20) = e20 ),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f266,plain,
( op2(e20,e21) = e20
| op2(e20,e20) != e21 ),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f267,plain,
( op2(e20,e22) = e20
| op2(e20,e20) != e22 ),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f271,plain,
( op2(e21,e22) = e21
| op2(e21,e21) != e22 ),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f277,plain,
( op2(e23,e20) = e23
| op2(e23,e23) != e20 ),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f284,plain,
e10 = op1(e13,e13),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f285,plain,
e11 = op1(op1(e13,e13),op1(e13,e13)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f286,plain,
e12 = op1(op1(op1(e13,e13),op1(e13,e13)),e13),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f287,plain,
e20 = op2(e23,e23),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f288,plain,
e21 = op2(op2(e23,e23),op2(e23,e23)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f289,plain,
e22 = op2(op2(op2(e23,e23),op2(e23,e23)),e23),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f290,plain,
h1(e13) = e20,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f291,plain,
h1(e10) = op2(e20,e20),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f292,plain,
h1(e11) = op2(op2(e20,e20),op2(e20,e20)),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f299,plain,
h3(e10) = op2(e22,e22),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f302,plain,
h4(e13) = e23,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f303,plain,
h4(e10) = op2(e23,e23),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f304,plain,
h4(e11) = op2(op2(e23,e23),op2(e23,e23)),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f305,plain,
h4(e12) = op2(op2(op2(e23,e23),op2(e23,e23)),e23),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f306,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)],[f19]) ).
fof(f307,definition,
( sP2_prd
<=> ( h1(e13) != e20
& h1(e12) != e20
& h1(e11) != e20
& h1(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f308,definition,
( sP3_prd
<=> ( h1(e13) != e21
& h1(e12) != e21
& h1(e11) != e21
& h1(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f309,definition,
( sP4_prd
<=> ( h1(e13) != e22
& h1(e12) != e22
& h1(e11) != e22
& h1(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f310,definition,
( sP5_prd
<=> ( h2(e13) != e20
& h2(e12) != e20
& h2(e11) != e20
& h2(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f311,definition,
( sP6_prd
<=> ( h2(e13) != e21
& h2(e12) != e21
& h2(e11) != e21
& h2(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f312,definition,
( sP7_prd
<=> ( h2(e13) != e22
& h2(e12) != e22
& h2(e11) != e22
& h2(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP7_prd])],[]) ).
fof(f313,definition,
( sP8_prd
<=> ( h3(e13) != e20
& h3(e12) != e20
& h3(e11) != e20
& h3(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP8_prd])],[]) ).
fof(f314,definition,
( sP9_prd
<=> ( h3(e13) != e21
& h3(e12) != e21
& h3(e11) != e21
& h3(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP9_prd])],[]) ).
fof(f315,definition,
( sP10_prd
<=> ( h3(e13) != e22
& h3(e12) != e22
& h3(e11) != e22
& h3(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP10_prd])],[]) ).
fof(f316,definition,
( sP11_prd
<=> ( h4(e13) != e20
& h4(e12) != e20
& h4(e11) != e20
& h4(e10) != e20 ) ),
introduced(definition,[new_symbols(definition,[sP11_prd])],[]) ).
fof(f317,definition,
( sP12_prd
<=> ( h4(e13) != e21
& h4(e12) != e21
& h4(e11) != e21
& h4(e10) != e21 ) ),
introduced(definition,[new_symbols(definition,[sP12_prd])],[]) ).
fof(f318,definition,
( sP13_prd
<=> ( h4(e13) != e22
& h4(e12) != e22
& h4(e11) != e22
& h4(e10) != e22 ) ),
introduced(definition,[new_symbols(definition,[sP13_prd])],[]) ).
fof(f319,plain,
( ( ( h4(e13) != e23
& h4(e12) != e23
& h4(e11) != e23
& h4(e10) != e23 )
| sP13_prd
| sP12_prd
| sP11_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 )
| sP10_prd
| sP9_prd
| sP8_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 )
| sP7_prd
| sP6_prd
| sP5_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 )
| sP4_prd
| sP3_prd
| sP2_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)],[f306,f318,f317,f316,f315,f314,f313,f312,f311,f310,f309,f308,f307]) ).
fof(f335,plain,
( h4(e13) != e23
| sP13_prd
| sP12_prd
| sP11_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)) ),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f406,plain,
( ( h4(e13) = e20
| h4(e12) = e20
| h4(e11) = e20
| h4(e10) = e20
| sP11_prd )
& ( ( h4(e13) != e20
& h4(e12) != e20
& h4(e11) != e20
& h4(e10) != e20 )
| ~ sP11_prd ) ),
inference(NNF_transformation,[status(thm)],[f316]) ).
fof(f407,plain,
( h4(e10) != e20
| ~ sP11_prd ),
inference(cnf_transformation,[status(thm)],[f406]) ).
fof(f412,plain,
( ( h4(e13) = e21
| h4(e12) = e21
| h4(e11) = e21
| h4(e10) = e21
| sP12_prd )
& ( ( h4(e13) != e21
& h4(e12) != e21
& h4(e11) != e21
& h4(e10) != e21 )
| ~ sP12_prd ) ),
inference(NNF_transformation,[status(thm)],[f317]) ).
fof(f414,plain,
( h4(e11) != e21
| ~ sP12_prd ),
inference(cnf_transformation,[status(thm)],[f412]) ).
fof(f418,plain,
( ( h4(e13) = e22
| h4(e12) = e22
| h4(e11) = e22
| h4(e10) = e22
| sP13_prd )
& ( ( h4(e13) != e22
& h4(e12) != e22
& h4(e11) != e22
& h4(e10) != e22 )
| ~ sP13_prd ) ),
inference(NNF_transformation,[status(thm)],[f318]) ).
fof(f421,plain,
( h4(e12) != e22
| ~ sP13_prd ),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f642,definition,
( sQ0_spl
<=> op1(e10,e10) = e10 ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f643,plain,
( ~ sQ0_spl
| op1(e10,e10) = e10 ),
inference(component_clause,[status(thm)],[f642]) ).
fof(f645,definition,
( sQ1_spl
<=> op1(e10,e10) = e11 ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f648,definition,
( sQ2_spl
<=> op1(e10,e10) = e12 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f649,plain,
( ~ sQ2_spl
| op1(e10,e10) = e12 ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f651,definition,
( sQ3_spl
<=> op1(e10,e10) = e13 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f652,plain,
( ~ sQ3_spl
| op1(e10,e10) = e13 ),
inference(component_clause,[status(thm)],[f651]) ).
fof(f654,plain,
( sQ3_spl
| sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f20,f642,f645,f648,f651]) ).
fof(f655,definition,
( sQ4_spl
<=> op1(e10,e11) = e10 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f656,plain,
( ~ sQ4_spl
| op1(e10,e11) = e10 ),
inference(component_clause,[status(thm)],[f655]) ).
fof(f661,definition,
( sQ6_spl
<=> op1(e10,e11) = e12 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f662,plain,
( ~ sQ6_spl
| op1(e10,e11) = e12 ),
inference(component_clause,[status(thm)],[f661]) ).
fof(f664,definition,
( sQ7_spl
<=> op1(e10,e11) = e13 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f665,plain,
( ~ sQ7_spl
| op1(e10,e11) = e13 ),
inference(component_clause,[status(thm)],[f664]) ).
fof(f668,definition,
( sQ8_spl
<=> op1(e10,e12) = e10 ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f671,definition,
( sQ9_spl
<=> op1(e10,e12) = e11 ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f672,plain,
( ~ sQ9_spl
| op1(e10,e12) = e11 ),
inference(component_clause,[status(thm)],[f671]) ).
fof(f674,definition,
( sQ10_spl
<=> op1(e10,e12) = e12 ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f675,plain,
( ~ sQ10_spl
| op1(e10,e12) = e12 ),
inference(component_clause,[status(thm)],[f674]) ).
fof(f677,definition,
( sQ11_spl
<=> op1(e10,e12) = e13 ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f678,plain,
( ~ sQ11_spl
| op1(e10,e12) = e13 ),
inference(component_clause,[status(thm)],[f677]) ).
fof(f680,plain,
( sQ11_spl
| sQ10_spl
| sQ9_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f22,f668,f671,f674,f677]) ).
fof(f684,definition,
( sQ13_spl
<=> op1(e10,e13) = e11 ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f685,plain,
( ~ sQ13_spl
| op1(e10,e13) = e11 ),
inference(component_clause,[status(thm)],[f684]) ).
fof(f690,definition,
( sQ15_spl
<=> op1(e10,e13) = e13 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f691,plain,
( ~ sQ15_spl
| op1(e10,e13) = e13 ),
inference(component_clause,[status(thm)],[f690]) ).
fof(f694,definition,
( sQ16_spl
<=> op1(e11,e10) = e10 ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f695,plain,
( ~ sQ16_spl
| op1(e11,e10) = e10 ),
inference(component_clause,[status(thm)],[f694]) ).
fof(f697,definition,
( sQ17_spl
<=> op1(e11,e10) = e11 ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f698,plain,
( ~ sQ17_spl
| op1(e11,e10) = e11 ),
inference(component_clause,[status(thm)],[f697]) ).
fof(f700,definition,
( sQ18_spl
<=> op1(e11,e10) = e12 ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f701,plain,
( ~ sQ18_spl
| op1(e11,e10) = e12 ),
inference(component_clause,[status(thm)],[f700]) ).
fof(f703,definition,
( sQ19_spl
<=> op1(e11,e10) = e13 ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f706,plain,
( sQ19_spl
| sQ18_spl
| sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f24,f694,f697,f700,f703]) ).
fof(f710,definition,
( sQ21_spl
<=> op1(e11,e11) = e11 ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f711,plain,
( ~ sQ21_spl
| op1(e11,e11) = e11 ),
inference(component_clause,[status(thm)],[f710]) ).
fof(f713,definition,
( sQ22_spl
<=> op1(e11,e11) = e12 ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f716,definition,
( sQ23_spl
<=> op1(e11,e11) = e13 ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f723,definition,
( sQ25_spl
<=> op1(e11,e12) = e11 ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f729,definition,
( sQ27_spl
<=> op1(e11,e12) = e13 ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f730,plain,
( ~ sQ27_spl
| op1(e11,e12) = e13 ),
inference(component_clause,[status(thm)],[f729]) ).
fof(f736,definition,
( sQ29_spl
<=> op1(e11,e13) = e11 ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f737,plain,
( ~ sQ29_spl
| op1(e11,e13) = e11 ),
inference(component_clause,[status(thm)],[f736]) ).
fof(f742,definition,
( sQ31_spl
<=> op1(e11,e13) = e13 ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f743,plain,
( ~ sQ31_spl
| op1(e11,e13) = e13 ),
inference(component_clause,[status(thm)],[f742]) ).
fof(f752,definition,
( sQ34_spl
<=> op1(e12,e10) = e12 ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f753,plain,
( ~ sQ34_spl
| op1(e12,e10) = e12 ),
inference(component_clause,[status(thm)],[f752]) ).
fof(f765,definition,
( sQ38_spl
<=> op1(e12,e11) = e12 ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f766,plain,
( ~ sQ38_spl
| op1(e12,e11) = e12 ),
inference(component_clause,[status(thm)],[f765]) ).
fof(f768,definition,
( sQ39_spl
<=> op1(e12,e11) = e13 ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f769,plain,
( ~ sQ39_spl
| op1(e12,e11) = e13 ),
inference(component_clause,[status(thm)],[f768]) ).
fof(f772,definition,
( sQ40_spl
<=> op1(e12,e12) = e10 ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f773,plain,
( ~ sQ40_spl
| op1(e12,e12) = e10 ),
inference(component_clause,[status(thm)],[f772]) ).
fof(f775,definition,
( sQ41_spl
<=> op1(e12,e12) = e11 ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f778,definition,
( sQ42_spl
<=> op1(e12,e12) = e12 ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f781,definition,
( sQ43_spl
<=> op1(e12,e12) = e13 ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f784,plain,
( sQ43_spl
| sQ42_spl
| sQ41_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f30,f772,f775,f778,f781]) ).
fof(f788,definition,
( sQ45_spl
<=> op1(e12,e13) = e11 ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f789,plain,
( ~ sQ45_spl
| op1(e12,e13) = e11 ),
inference(component_clause,[status(thm)],[f788]) ).
fof(f807,definition,
( sQ51_spl
<=> op1(e13,e10) = e13 ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f808,plain,
( ~ sQ51_spl
| op1(e13,e10) = e13 ),
inference(component_clause,[status(thm)],[f807]) ).
fof(f817,definition,
( sQ54_spl
<=> op1(e13,e11) = e12 ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f818,plain,
( ~ sQ54_spl
| op1(e13,e11) = e12 ),
inference(component_clause,[status(thm)],[f817]) ).
fof(f820,definition,
( sQ55_spl
<=> op1(e13,e11) = e13 ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f824,definition,
( sQ56_spl
<=> op1(e13,e12) = e10 ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f825,plain,
( ~ sQ56_spl
| op1(e13,e12) = e10 ),
inference(component_clause,[status(thm)],[f824]) ).
fof(f827,definition,
( sQ57_spl
<=> op1(e13,e12) = e11 ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f828,plain,
( ~ sQ57_spl
| op1(e13,e12) = e11 ),
inference(component_clause,[status(thm)],[f827]) ).
fof(f830,definition,
( sQ58_spl
<=> op1(e13,e12) = e12 ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f831,plain,
( ~ sQ58_spl
| op1(e13,e12) = e12 ),
inference(component_clause,[status(thm)],[f830]) ).
fof(f833,definition,
( sQ59_spl
<=> op1(e13,e12) = e13 ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f836,plain,
( sQ59_spl
| sQ58_spl
| sQ57_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f34,f824,f827,f830,f833]) ).
fof(f837,definition,
( sQ60_spl
<=> op1(e13,e13) = e10 ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f840,definition,
( sQ61_spl
<=> op1(e13,e13) = e11 ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f841,plain,
( ~ sQ61_spl
| op1(e13,e13) = e11 ),
inference(component_clause,[status(thm)],[f840]) ).
fof(f843,definition,
( sQ62_spl
<=> op1(e13,e13) = e12 ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f844,plain,
( ~ sQ62_spl
| op1(e13,e13) = e12 ),
inference(component_clause,[status(thm)],[f843]) ).
fof(f846,definition,
( sQ63_spl
<=> op1(e13,e13) = e13 ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f847,plain,
( ~ sQ63_spl
| op1(e13,e13) = e13 ),
inference(component_clause,[status(thm)],[f846]) ).
fof(f849,plain,
( sQ63_spl
| sQ62_spl
| sQ61_spl
| sQ60_spl ),
inference(split_clause,[status(thm)],[f35,f837,f840,f843,f846]) ).
fof(f856,plain,
( sQ15_spl
| sQ11_spl
| sQ7_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f42,f651,f664,f677,f690]) ).
fof(f860,plain,
( sQ29_spl
| sQ25_spl
| sQ21_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f46,f697,f710,f723,f736]) ).
fof(f863,plain,
( sQ54_spl
| sQ38_spl
| sQ22_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f49,f661,f713,f765,f817]) ).
fof(f864,plain,
( sQ31_spl
| sQ27_spl
| sQ23_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f50,f703,f716,f729,f742]) ).
fof(f865,plain,
( sQ55_spl
| sQ39_spl
| sQ23_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f51,f664,f716,f768,f820]) ).
fof(f877,plain,
( sQ61_spl
| sQ45_spl
| sQ29_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f63,f684,f736,f788,f840]) ).
fof(f882,definition,
( sQ64_spl
<=> op2(e20,e20) = e20 ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f883,plain,
( ~ sQ64_spl
| op2(e20,e20) = e20 ),
inference(component_clause,[status(thm)],[f882]) ).
fof(f885,definition,
( sQ65_spl
<=> op2(e20,e20) = e21 ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f886,plain,
( ~ sQ65_spl
| op2(e20,e20) = e21 ),
inference(component_clause,[status(thm)],[f885]) ).
fof(f888,definition,
( sQ66_spl
<=> op2(e20,e20) = e22 ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f891,definition,
( sQ67_spl
<=> op2(e20,e20) = e23 ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f892,plain,
( ~ sQ67_spl
| op2(e20,e20) = e23 ),
inference(component_clause,[status(thm)],[f891]) ).
fof(f895,definition,
( sQ68_spl
<=> op2(e20,e21) = e20 ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f896,plain,
( ~ sQ68_spl
| op2(e20,e21) = e20 ),
inference(component_clause,[status(thm)],[f895]) ).
fof(f901,definition,
( sQ70_spl
<=> op2(e20,e21) = e22 ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f902,plain,
( ~ sQ70_spl
| op2(e20,e21) = e22 ),
inference(component_clause,[status(thm)],[f901]) ).
fof(f904,definition,
( sQ71_spl
<=> op2(e20,e21) = e23 ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f905,plain,
( ~ sQ71_spl
| op2(e20,e21) = e23 ),
inference(component_clause,[status(thm)],[f904]) ).
fof(f908,definition,
( sQ72_spl
<=> op2(e20,e22) = e20 ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f909,plain,
( ~ sQ72_spl
| op2(e20,e22) = e20 ),
inference(component_clause,[status(thm)],[f908]) ).
fof(f914,definition,
( sQ74_spl
<=> op2(e20,e22) = e22 ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f915,plain,
( ~ sQ74_spl
| op2(e20,e22) = e22 ),
inference(component_clause,[status(thm)],[f914]) ).
fof(f917,definition,
( sQ75_spl
<=> op2(e20,e22) = e23 ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f918,plain,
( ~ sQ75_spl
| op2(e20,e22) = e23 ),
inference(component_clause,[status(thm)],[f917]) ).
fof(f930,definition,
( sQ79_spl
<=> op2(e20,e23) = e23 ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f931,plain,
( ~ sQ79_spl
| op2(e20,e23) = e23 ),
inference(component_clause,[status(thm)],[f930]) ).
fof(f934,definition,
( sQ80_spl
<=> op2(e21,e20) = e20 ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f935,plain,
( ~ sQ80_spl
| op2(e21,e20) = e20 ),
inference(component_clause,[status(thm)],[f934]) ).
fof(f940,definition,
( sQ82_spl
<=> op2(e21,e20) = e22 ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f941,plain,
( ~ sQ82_spl
| op2(e21,e20) = e22 ),
inference(component_clause,[status(thm)],[f940]) ).
fof(f950,definition,
( sQ85_spl
<=> op2(e21,e21) = e21 ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f951,plain,
( ~ sQ85_spl
| op2(e21,e21) = e21 ),
inference(component_clause,[status(thm)],[f950]) ).
fof(f953,definition,
( sQ86_spl
<=> op2(e21,e21) = e22 ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f960,definition,
( sQ88_spl
<=> op2(e21,e22) = e20 ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f963,definition,
( sQ89_spl
<=> op2(e21,e22) = e21 ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f966,definition,
( sQ90_spl
<=> op2(e21,e22) = e22 ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f967,plain,
( ~ sQ90_spl
| op2(e21,e22) = e22 ),
inference(component_clause,[status(thm)],[f966]) ).
fof(f969,definition,
( sQ91_spl
<=> op2(e21,e22) = e23 ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f970,plain,
( ~ sQ91_spl
| op2(e21,e22) = e23 ),
inference(component_clause,[status(thm)],[f969]) ).
fof(f972,plain,
( sQ91_spl
| sQ90_spl
| sQ89_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f74,f960,f963,f966,f969]) ).
fof(f973,definition,
( sQ92_spl
<=> op2(e21,e23) = e20 ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f974,plain,
( ~ sQ92_spl
| op2(e21,e23) = e20 ),
inference(component_clause,[status(thm)],[f973]) ).
fof(f986,definition,
( sQ96_spl
<=> op2(e22,e20) = e20 ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f987,plain,
( ~ sQ96_spl
| op2(e22,e20) = e20 ),
inference(component_clause,[status(thm)],[f986]) ).
fof(f992,definition,
( sQ98_spl
<=> op2(e22,e20) = e22 ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f993,plain,
( ~ sQ98_spl
| op2(e22,e20) = e22 ),
inference(component_clause,[status(thm)],[f992]) ).
fof(f999,definition,
( sQ100_spl
<=> op2(e22,e21) = e20 ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f1002,definition,
( sQ101_spl
<=> op2(e22,e21) = e21 ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1003,plain,
( ~ sQ101_spl
| op2(e22,e21) = e21 ),
inference(component_clause,[status(thm)],[f1002]) ).
fof(f1005,definition,
( sQ102_spl
<=> op2(e22,e21) = e22 ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1008,definition,
( sQ103_spl
<=> op2(e22,e21) = e23 ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1009,plain,
( ~ sQ103_spl
| op2(e22,e21) = e23 ),
inference(component_clause,[status(thm)],[f1008]) ).
fof(f1011,plain,
( sQ103_spl
| sQ102_spl
| sQ101_spl
| sQ100_spl ),
inference(split_clause,[status(thm)],[f77,f999,f1002,f1005,f1008]) ).
fof(f1012,definition,
( sQ104_spl
<=> op2(e22,e22) = e20 ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1013,plain,
( ~ sQ104_spl
| op2(e22,e22) = e20 ),
inference(component_clause,[status(thm)],[f1012]) ).
fof(f1018,definition,
( sQ106_spl
<=> op2(e22,e22) = e22 ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1019,plain,
( ~ sQ106_spl
| op2(e22,e22) = e22 ),
inference(component_clause,[status(thm)],[f1018]) ).
fof(f1025,definition,
( sQ108_spl
<=> op2(e22,e23) = e20 ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1026,plain,
( ~ sQ108_spl
| op2(e22,e23) = e20 ),
inference(component_clause,[status(thm)],[f1025]) ).
fof(f1028,definition,
( sQ109_spl
<=> op2(e22,e23) = e21 ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1029,plain,
( ~ sQ109_spl
| op2(e22,e23) = e21 ),
inference(component_clause,[status(thm)],[f1028]) ).
fof(f1031,definition,
( sQ110_spl
<=> op2(e22,e23) = e22 ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1034,definition,
( sQ111_spl
<=> op2(e22,e23) = e23 ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1035,plain,
( ~ sQ111_spl
| op2(e22,e23) = e23 ),
inference(component_clause,[status(thm)],[f1034]) ).
fof(f1037,plain,
( sQ111_spl
| sQ110_spl
| sQ109_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f79,f1025,f1028,f1031,f1034]) ).
fof(f1038,definition,
( sQ112_spl
<=> op2(e23,e20) = e20 ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1039,plain,
( ~ sQ112_spl
| op2(e23,e20) = e20 ),
inference(component_clause,[status(thm)],[f1038]) ).
fof(f1041,definition,
( sQ113_spl
<=> op2(e23,e20) = e21 ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f1042,plain,
( ~ sQ113_spl
| op2(e23,e20) = e21 ),
inference(component_clause,[status(thm)],[f1041]) ).
fof(f1044,definition,
( sQ114_spl
<=> op2(e23,e20) = e22 ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f1045,plain,
( ~ sQ114_spl
| op2(e23,e20) = e22 ),
inference(component_clause,[status(thm)],[f1044]) ).
fof(f1047,definition,
( sQ115_spl
<=> op2(e23,e20) = e23 ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f1048,plain,
( ~ sQ115_spl
| op2(e23,e20) = e23 ),
inference(component_clause,[status(thm)],[f1047]) ).
fof(f1051,definition,
( sQ116_spl
<=> op2(e23,e21) = e20 ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1054,definition,
( sQ117_spl
<=> op2(e23,e21) = e21 ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1055,plain,
( ~ sQ117_spl
| op2(e23,e21) = e21 ),
inference(component_clause,[status(thm)],[f1054]) ).
fof(f1057,definition,
( sQ118_spl
<=> op2(e23,e21) = e22 ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1058,plain,
( ~ sQ118_spl
| op2(e23,e21) = e22 ),
inference(component_clause,[status(thm)],[f1057]) ).
fof(f1064,definition,
( sQ120_spl
<=> op2(e23,e22) = e20 ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f1065,plain,
( ~ sQ120_spl
| op2(e23,e22) = e20 ),
inference(component_clause,[status(thm)],[f1064]) ).
fof(f1067,definition,
( sQ121_spl
<=> op2(e23,e22) = e21 ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1068,plain,
( ~ sQ121_spl
| op2(e23,e22) = e21 ),
inference(component_clause,[status(thm)],[f1067]) ).
fof(f1070,definition,
( sQ122_spl
<=> op2(e23,e22) = e22 ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1071,plain,
( ~ sQ122_spl
| op2(e23,e22) = e22 ),
inference(component_clause,[status(thm)],[f1070]) ).
fof(f1077,definition,
( sQ124_spl
<=> op2(e23,e23) = e20 ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f1080,definition,
( sQ125_spl
<=> op2(e23,e23) = e21 ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1081,plain,
( ~ sQ125_spl
| op2(e23,e23) = e21 ),
inference(component_clause,[status(thm)],[f1080]) ).
fof(f1086,definition,
( sQ127_spl
<=> op2(e23,e23) = e23 ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f1087,plain,
( ~ sQ127_spl
| op2(e23,e23) = e23 ),
inference(component_clause,[status(thm)],[f1086]) ).
fof(f1091,plain,
( sQ112_spl
| sQ96_spl
| sQ80_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f85,f882,f934,f986,f1038]) ).
fof(f1095,plain,
( sQ114_spl
| sQ98_spl
| sQ82_spl
| sQ66_spl ),
inference(split_clause,[status(thm)],[f89,f888,f940,f992,f1044]) ).
fof(f1096,plain,
( sQ79_spl
| sQ75_spl
| sQ71_spl
| sQ67_spl ),
inference(split_clause,[status(thm)],[f90,f891,f904,f917,f930]) ).
fof(f1103,plain,
( sQ118_spl
| sQ102_spl
| sQ86_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f97,f901,f953,f1005,f1057]) ).
fof(f1107,plain,
( sQ120_spl
| sQ104_spl
| sQ88_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f101,f908,f960,f1012,f1064]) ).
fof(f1111,plain,
( sQ122_spl
| sQ106_spl
| sQ90_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f105,f914,f966,f1018,f1070]) ).
fof(f1114,plain,
( sQ124_spl
| sQ120_spl
| sQ116_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f108,f1038,f1051,f1064,f1077]) ).
fof(f1116,plain,
( sQ125_spl
| sQ121_spl
| sQ117_spl
| sQ113_spl ),
inference(split_clause,[status(thm)],[f110,f1041,f1054,f1067,f1080]) ).
fof(f1124,plain,
( sQ4_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f244,f645,f655]) ).
fof(f1129,plain,
( sQ25_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f249,f713,f723]) ).
fof(f1130,plain,
( sQ29_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f250,f716,f736]) ).
fof(f1131,plain,
( sQ34_spl
| ~ sQ40_spl ),
inference(split_clause,[status(thm)],[f251,f772,f752]) ).
fof(f1135,plain,
( sQ51_spl
| ~ sQ60_spl ),
inference(split_clause,[status(thm)],[f255,f837,f807]) ).
fof(f1145,plain,
( sQ127_spl
| sQ106_spl
| sQ85_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f264,f882,f950,f1018,f1086]) ).
fof(f1147,plain,
( sQ68_spl
| ~ sQ65_spl ),
inference(split_clause,[status(thm)],[f266,f885,f895]) ).
fof(f1148,plain,
( sQ72_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f267,f888,f908]) ).
fof(f1152,plain,
( sQ89_spl
| ~ sQ86_spl ),
inference(split_clause,[status(thm)],[f271,f953,f963]) ).
fof(f1158,plain,
( sQ115_spl
| ~ sQ124_spl ),
inference(split_clause,[status(thm)],[f277,f1077,f1047]) ).
fof(f1213,definition,
( sQ145_spl
<=> h1(op1(e13,e13)) = op2(h1(e13),h1(e13)) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f1214,plain,
( ~ sQ145_spl
| h1(op1(e13,e13)) = op2(h1(e13),h1(e13)) ),
inference(component_clause,[status(thm)],[f1213]) ).
fof(f1215,plain,
( sQ145_spl
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13)) ),
inference(component_clause,[status(thm)],[f1213]) ).
fof(f1387,definition,
( sQ199_spl
<=> h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) ),
introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition]) ).
fof(f1388,plain,
( ~ sQ199_spl
| h4(op1(e10,e10)) = op2(h4(e10),h4(e10)) ),
inference(component_clause,[status(thm)],[f1387]) ).
fof(f1389,plain,
( sQ199_spl
| h4(op1(e10,e10)) != op2(h4(e10),h4(e10)) ),
inference(component_clause,[status(thm)],[f1387]) ).
fof(f1390,definition,
( sQ200_spl
<=> h4(op1(e10,e11)) = op2(h4(e10),h4(e11)) ),
introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition]) ).
fof(f1392,plain,
( sQ200_spl
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11)) ),
inference(component_clause,[status(thm)],[f1390]) ).
fof(f1393,definition,
( sQ201_spl
<=> h4(op1(e10,e12)) = op2(h4(e10),h4(e12)) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f1395,plain,
( sQ201_spl
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12)) ),
inference(component_clause,[status(thm)],[f1393]) ).
fof(f1396,definition,
( sQ202_spl
<=> h4(op1(e10,e13)) = op2(h4(e10),h4(e13)) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f1398,plain,
( sQ202_spl
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13)) ),
inference(component_clause,[status(thm)],[f1396]) ).
fof(f1399,definition,
( sQ203_spl
<=> h4(op1(e11,e10)) = op2(h4(e11),h4(e10)) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f1401,plain,
( sQ203_spl
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10)) ),
inference(component_clause,[status(thm)],[f1399]) ).
fof(f1402,definition,
( sQ204_spl
<=> h4(op1(e11,e11)) = op2(h4(e11),h4(e11)) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f1404,plain,
( sQ204_spl
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11)) ),
inference(component_clause,[status(thm)],[f1402]) ).
fof(f1405,definition,
( sQ205_spl
<=> h4(op1(e11,e12)) = op2(h4(e11),h4(e12)) ),
introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition]) ).
fof(f1407,plain,
( sQ205_spl
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12)) ),
inference(component_clause,[status(thm)],[f1405]) ).
fof(f1408,definition,
( sQ206_spl
<=> h4(op1(e11,e13)) = op2(h4(e11),h4(e13)) ),
introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition]) ).
fof(f1410,plain,
( sQ206_spl
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13)) ),
inference(component_clause,[status(thm)],[f1408]) ).
fof(f1411,definition,
( sQ207_spl
<=> h4(op1(e12,e10)) = op2(h4(e12),h4(e10)) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f1413,plain,
( sQ207_spl
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10)) ),
inference(component_clause,[status(thm)],[f1411]) ).
fof(f1414,definition,
( sQ208_spl
<=> h4(op1(e12,e11)) = op2(h4(e12),h4(e11)) ),
introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition]) ).
fof(f1416,plain,
( sQ208_spl
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11)) ),
inference(component_clause,[status(thm)],[f1414]) ).
fof(f1417,definition,
( sQ209_spl
<=> h4(op1(e12,e12)) = op2(h4(e12),h4(e12)) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f1419,plain,
( sQ209_spl
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12)) ),
inference(component_clause,[status(thm)],[f1417]) ).
fof(f1420,definition,
( sQ210_spl
<=> h4(op1(e12,e13)) = op2(h4(e12),h4(e13)) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f1422,plain,
( sQ210_spl
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13)) ),
inference(component_clause,[status(thm)],[f1420]) ).
fof(f1423,definition,
( sQ211_spl
<=> h4(op1(e13,e10)) = op2(h4(e13),h4(e10)) ),
introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition]) ).
fof(f1425,plain,
( sQ211_spl
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10)) ),
inference(component_clause,[status(thm)],[f1423]) ).
fof(f1426,definition,
( sQ212_spl
<=> h4(op1(e13,e11)) = op2(h4(e13),h4(e11)) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f1428,plain,
( sQ212_spl
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11)) ),
inference(component_clause,[status(thm)],[f1426]) ).
fof(f1429,definition,
( sQ213_spl
<=> h4(op1(e13,e12)) = op2(h4(e13),h4(e12)) ),
introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition]) ).
fof(f1431,plain,
( sQ213_spl
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12)) ),
inference(component_clause,[status(thm)],[f1429]) ).
fof(f1432,definition,
( sQ214_spl
<=> h4(op1(e13,e13)) = op2(h4(e13),h4(e13)) ),
introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition]) ).
fof(f1434,plain,
( sQ214_spl
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13)) ),
inference(component_clause,[status(thm)],[f1432]) ).
fof(f1435,definition,
( sQ215_spl
<=> sP11_prd ),
introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition]) ).
fof(f1438,definition,
( sQ216_spl
<=> sP12_prd ),
introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition]) ).
fof(f1441,definition,
( sQ217_spl
<=> sP13_prd ),
introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition]) ).
fof(f1456,definition,
( sQ221_spl
<=> h4(e13) = e23 ),
introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition]) ).
fof(f1458,plain,
( sQ221_spl
| h4(e13) != e23 ),
inference(component_clause,[status(thm)],[f1456]) ).
fof(f1459,plain,
( ~ sQ221_spl
| sQ217_spl
| sQ216_spl
| sQ215_spl
| ~ sQ214_spl
| ~ sQ213_spl
| ~ sQ212_spl
| ~ sQ211_spl
| ~ sQ210_spl
| ~ sQ209_spl
| ~ sQ208_spl
| ~ sQ207_spl
| ~ sQ206_spl
| ~ sQ205_spl
| ~ sQ204_spl
| ~ sQ203_spl
| ~ sQ202_spl
| ~ sQ201_spl
| ~ sQ200_spl
| ~ sQ199_spl ),
inference(split_clause,[status(thm)],[f335,f1387,f1390,f1393,f1396,f1399,f1402,f1405,f1408,f1411,f1414,f1417,f1420,f1423,f1426,f1429,f1432,f1435,f1438,f1441,f1456]) ).
fof(f1497,definition,
( sQ229_spl
<=> h1(e11) = e21 ),
introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition]) ).
fof(f1498,plain,
( ~ sQ229_spl
| h1(e11) = e21 ),
inference(component_clause,[status(thm)],[f1497]) ).
fof(f1612,definition,
( sQ256_spl
<=> h3(e10) = e22 ),
introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition]) ).
fof(f1629,definition,
( sQ260_spl
<=> h4(e10) = e20 ),
introduced(definition,[new_symbols(definition,[sQ260_spl])],[split_symbol_definition]) ).
fof(f1631,plain,
( sQ260_spl
| h4(e10) != e20 ),
inference(component_clause,[status(thm)],[f1629]) ).
fof(f1632,plain,
( ~ sQ260_spl
| ~ sQ215_spl ),
inference(split_clause,[status(thm)],[f407,f1435,f1629]) ).
fof(f1650,definition,
( sQ265_spl
<=> h4(e11) = e21 ),
introduced(definition,[new_symbols(definition,[sQ265_spl])],[split_symbol_definition]) ).
fof(f1652,plain,
( sQ265_spl
| h4(e11) != e21 ),
inference(component_clause,[status(thm)],[f1650]) ).
fof(f1653,plain,
( ~ sQ265_spl
| ~ sQ216_spl ),
inference(split_clause,[status(thm)],[f414,f1438,f1650]) ).
fof(f1671,definition,
( sQ270_spl
<=> h4(e12) = e22 ),
introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition]) ).
fof(f1673,plain,
( sQ270_spl
| h4(e12) != e22 ),
inference(component_clause,[status(thm)],[f1671]) ).
fof(f1674,plain,
( ~ sQ270_spl
| ~ sQ217_spl ),
inference(split_clause,[status(thm)],[f421,f1441,f1671]) ).
fof(f1896,plain,
op1(e13,e12) != e10,
inference(backward_demodulation,[status(thm)],[f284,f163]) ).
fof(f1902,plain,
e11 = op1(e10,op1(e13,e13)),
inference(forward_demodulation,[status(thm)],[f284,f285]) ).
fof(f1904,plain,
e11 != op1(e10,e12),
inference(backward_demodulation,[status(thm)],[f1909,f141]) ).
fof(f1908,plain,
e11 != op1(e11,e10),
inference(backward_demodulation,[status(thm)],[f1909,f116]) ).
fof(f1909,plain,
e11 = op1(e10,e10),
inference(forward_demodulation,[status(thm)],[f284,f1902]) ).
fof(f1910,plain,
e12 = op1(op1(e10,op1(e13,e13)),e13),
inference(forward_demodulation,[status(thm)],[f284,f286]) ).
fof(f1911,plain,
e12 = op1(op1(e10,e10),e13),
inference(forward_demodulation,[status(thm)],[f284,f1910]) ).
fof(f1914,plain,
op1(e11,e10) != e12,
inference(backward_demodulation,[status(thm)],[f1917,f148]) ).
fof(f1917,plain,
e12 = op1(e11,e13),
inference(forward_demodulation,[status(thm)],[f1909,f1911]) ).
fof(f1918,plain,
op2(e23,e22) != e20,
inference(backward_demodulation,[status(thm)],[f287,f211]) ).
fof(f1920,plain,
op2(e23,e20) != e20,
inference(backward_demodulation,[status(thm)],[f287,f208]) ).
fof(f1921,plain,
op2(e22,e23) != e20,
inference(backward_demodulation,[status(thm)],[f287,f187]) ).
fof(f1924,plain,
e21 = op2(e20,op2(e23,e23)),
inference(forward_demodulation,[status(thm)],[f287,f288]) ).
fof(f1928,plain,
e21 != op2(e23,e20),
inference(backward_demodulation,[status(thm)],[f1931,f166]) ).
fof(f1931,plain,
e21 = op2(e20,e20),
inference(forward_demodulation,[status(thm)],[f287,f1924]) ).
fof(f1932,plain,
e22 = op2(op2(e20,op2(e23,e23)),e23),
inference(forward_demodulation,[status(thm)],[f287,f289]) ).
fof(f1933,plain,
e22 = op2(op2(e20,e20),e23),
inference(forward_demodulation,[status(thm)],[f287,f1932]) ).
fof(f1934,plain,
op2(e21,e22) != e22,
inference(backward_demodulation,[status(thm)],[f1939,f199]) ).
fof(f1936,plain,
op2(e21,e20) != e22,
inference(backward_demodulation,[status(thm)],[f1939,f196]) ).
fof(f1939,plain,
e22 = op2(e21,e23),
inference(forward_demodulation,[status(thm)],[f1931,f1933]) ).
fof(f1940,plain,
h1(e10) = e21,
inference(forward_demodulation,[status(thm)],[f1931,f291]) ).
fof(f1941,plain,
h1(e11) = op2(e21,op2(e20,e20)),
inference(forward_demodulation,[status(thm)],[f1931,f292]) ).
fof(f1944,plain,
h1(e11) != op2(e23,e21),
inference(backward_demodulation,[status(thm)],[f1947,f174]) ).
fof(f1947,plain,
h1(e11) = op2(e21,e21),
inference(forward_demodulation,[status(thm)],[f1931,f1941]) ).
fof(f1959,plain,
op2(e22,e20) != h3(e10),
inference(backward_demodulation,[status(thm)],[f299,f201]) ).
fof(f1968,plain,
h4(e10) = e20,
inference(forward_demodulation,[status(thm)],[f287,f303]) ).
fof(f1969,plain,
h4(e11) = op2(e20,op2(e23,e23)),
inference(forward_demodulation,[status(thm)],[f287,f304]) ).
fof(f1970,plain,
h4(e11) = op2(e20,e20),
inference(forward_demodulation,[status(thm)],[f287,f1969]) ).
fof(f1971,plain,
h4(e11) = e21,
inference(forward_demodulation,[status(thm)],[f1931,f1970]) ).
fof(f1972,plain,
h4(e12) = op2(op2(e20,op2(e23,e23)),e23),
inference(forward_demodulation,[status(thm)],[f287,f305]) ).
fof(f1973,plain,
h4(e12) = op2(op2(e20,e20),e23),
inference(forward_demodulation,[status(thm)],[f287,f1972]) ).
fof(f1974,plain,
h4(e12) = op2(e21,e23),
inference(forward_demodulation,[status(thm)],[f1931,f1973]) ).
fof(f1975,plain,
h4(e12) = e22,
inference(forward_demodulation,[status(thm)],[f1939,f1974]) ).
fof(f1976,plain,
( sQ214_spl
| h4(e10) != op2(h4(e13),h4(e13)) ),
inference(forward_demodulation,[status(thm)],[f284,f1434]) ).
fof(f1977,plain,
( sQ214_spl
| e20 != op2(h4(e13),h4(e13)) ),
inference(forward_demodulation,[status(thm)],[f1968,f1976]) ).
fof(f1978,plain,
( sQ214_spl
| e20 != op2(e23,h4(e13)) ),
inference(forward_demodulation,[status(thm)],[f302,f1977]) ).
fof(f1979,plain,
( sQ214_spl
| e20 != op2(e23,e23) ),
inference(forward_demodulation,[status(thm)],[f302,f1978]) ).
fof(f1980,plain,
( sQ214_spl
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f287,f1979]) ).
fof(f1981,plain,
( sQ214_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1980]) ).
fof(f1982,plain,
sQ214_spl,
inference(contradiction_clause,[status(thm)],[f1981]) ).
fof(f1983,plain,
( sQ213_spl
| h4(op1(e13,e12)) != op2(e23,h4(e12)) ),
inference(forward_demodulation,[status(thm)],[f302,f1431]) ).
fof(f1984,plain,
( sQ213_spl
| h4(op1(e13,e12)) != op2(e23,e22) ),
inference(forward_demodulation,[status(thm)],[f1975,f1983]) ).
fof(f1985,plain,
( sQ212_spl
| h4(op1(e13,e11)) != op2(e23,h4(e11)) ),
inference(forward_demodulation,[status(thm)],[f302,f1428]) ).
fof(f1986,plain,
( sQ212_spl
| h4(op1(e13,e11)) != op2(e23,e21) ),
inference(forward_demodulation,[status(thm)],[f1971,f1985]) ).
fof(f1987,plain,
( sQ211_spl
| h4(op1(e13,e10)) != op2(e23,h4(e10)) ),
inference(forward_demodulation,[status(thm)],[f302,f1425]) ).
fof(f1988,plain,
( sQ211_spl
| h4(op1(e13,e10)) != op2(e23,e20) ),
inference(forward_demodulation,[status(thm)],[f1968,f1987]) ).
fof(f1989,plain,
( sQ210_spl
| h4(op1(e12,e13)) != op2(e22,h4(e13)) ),
inference(forward_demodulation,[status(thm)],[f1975,f1422]) ).
fof(f1990,plain,
( sQ210_spl
| h4(op1(e12,e13)) != op2(e22,e23) ),
inference(forward_demodulation,[status(thm)],[f302,f1989]) ).
fof(f1991,plain,
( sQ209_spl
| h4(op1(e12,e12)) != op2(e22,h4(e12)) ),
inference(forward_demodulation,[status(thm)],[f1975,f1419]) ).
fof(f1992,plain,
( sQ209_spl
| h4(op1(e12,e12)) != op2(e22,e22) ),
inference(forward_demodulation,[status(thm)],[f1975,f1991]) ).
fof(f1993,plain,
( sQ209_spl
| h4(op1(e12,e12)) != h3(e10) ),
inference(forward_demodulation,[status(thm)],[f299,f1992]) ).
fof(f1994,plain,
( sQ208_spl
| h4(op1(e12,e11)) != op2(e22,h4(e11)) ),
inference(forward_demodulation,[status(thm)],[f1975,f1416]) ).
fof(f1995,plain,
( sQ208_spl
| h4(op1(e12,e11)) != op2(e22,e21) ),
inference(forward_demodulation,[status(thm)],[f1971,f1994]) ).
fof(f1996,plain,
( sQ207_spl
| h4(op1(e12,e10)) != op2(e22,h4(e10)) ),
inference(forward_demodulation,[status(thm)],[f1975,f1413]) ).
fof(f1997,plain,
( sQ207_spl
| h4(op1(e12,e10)) != op2(e22,e20) ),
inference(forward_demodulation,[status(thm)],[f1968,f1996]) ).
fof(f1998,plain,
( sQ206_spl
| h4(e12) != op2(h4(e11),h4(e13)) ),
inference(forward_demodulation,[status(thm)],[f1917,f1410]) ).
fof(f1999,plain,
( sQ206_spl
| e22 != op2(h4(e11),h4(e13)) ),
inference(forward_demodulation,[status(thm)],[f1975,f1998]) ).
fof(f2000,plain,
( sQ206_spl
| e22 != op2(e21,h4(e13)) ),
inference(forward_demodulation,[status(thm)],[f1971,f1999]) ).
fof(f2001,plain,
( sQ206_spl
| e22 != op2(e21,e23) ),
inference(forward_demodulation,[status(thm)],[f302,f2000]) ).
fof(f2002,plain,
( sQ206_spl
| e22 != e22 ),
inference(forward_demodulation,[status(thm)],[f1939,f2001]) ).
fof(f2003,plain,
( sQ206_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2002]) ).
fof(f2004,plain,
sQ206_spl,
inference(contradiction_clause,[status(thm)],[f2003]) ).
fof(f2005,plain,
( sQ205_spl
| h4(op1(e11,e12)) != op2(e21,h4(e12)) ),
inference(forward_demodulation,[status(thm)],[f1971,f1407]) ).
fof(f2006,plain,
( sQ205_spl
| h4(op1(e11,e12)) != op2(e21,e22) ),
inference(forward_demodulation,[status(thm)],[f1975,f2005]) ).
fof(f2007,plain,
( sQ204_spl
| h4(op1(e11,e11)) != op2(e21,h4(e11)) ),
inference(forward_demodulation,[status(thm)],[f1971,f1404]) ).
fof(f2008,plain,
( sQ204_spl
| h4(op1(e11,e11)) != op2(e21,e21) ),
inference(forward_demodulation,[status(thm)],[f1971,f2007]) ).
fof(f2009,plain,
( sQ204_spl
| h4(op1(e11,e11)) != h1(e11) ),
inference(forward_demodulation,[status(thm)],[f1947,f2008]) ).
fof(f2010,plain,
( sQ203_spl
| h4(op1(e11,e10)) != op2(e21,h4(e10)) ),
inference(forward_demodulation,[status(thm)],[f1971,f1401]) ).
fof(f2011,plain,
( sQ203_spl
| h4(op1(e11,e10)) != op2(e21,e20) ),
inference(forward_demodulation,[status(thm)],[f1968,f2010]) ).
fof(f2012,plain,
( sQ202_spl
| h4(op1(e10,e13)) != op2(e20,h4(e13)) ),
inference(forward_demodulation,[status(thm)],[f1968,f1398]) ).
fof(f2013,plain,
( sQ202_spl
| h4(op1(e10,e13)) != op2(e20,e23) ),
inference(forward_demodulation,[status(thm)],[f302,f2012]) ).
fof(f2014,plain,
( sQ201_spl
| h4(op1(e10,e12)) != op2(e20,h4(e12)) ),
inference(forward_demodulation,[status(thm)],[f1968,f1395]) ).
fof(f2015,plain,
( sQ201_spl
| h4(op1(e10,e12)) != op2(e20,e22) ),
inference(forward_demodulation,[status(thm)],[f1975,f2014]) ).
fof(f2016,plain,
( sQ200_spl
| h4(op1(e10,e11)) != op2(e20,h4(e11)) ),
inference(forward_demodulation,[status(thm)],[f1968,f1392]) ).
fof(f2017,plain,
( sQ200_spl
| h4(op1(e10,e11)) != op2(e20,e21) ),
inference(forward_demodulation,[status(thm)],[f1971,f2016]) ).
fof(f2018,plain,
( sQ199_spl
| h4(e11) != op2(h4(e10),h4(e10)) ),
inference(forward_demodulation,[status(thm)],[f1909,f1389]) ).
fof(f2019,plain,
( sQ199_spl
| e21 != op2(h4(e10),h4(e10)) ),
inference(forward_demodulation,[status(thm)],[f1971,f2018]) ).
fof(f2020,plain,
( sQ199_spl
| e21 != op2(e20,h4(e10)) ),
inference(forward_demodulation,[status(thm)],[f1968,f2019]) ).
fof(f2021,plain,
( sQ199_spl
| e21 != op2(e20,e20) ),
inference(forward_demodulation,[status(thm)],[f1968,f2020]) ).
fof(f2022,plain,
( sQ199_spl
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1931,f2021]) ).
fof(f2023,plain,
( sQ199_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2022]) ).
fof(f2024,plain,
sQ199_spl,
inference(contradiction_clause,[status(thm)],[f2023]) ).
fof(f2074,plain,
( sQ145_spl
| h1(e10) != op2(h1(e13),h1(e13)) ),
inference(forward_demodulation,[status(thm)],[f284,f1215]) ).
fof(f2075,plain,
( sQ145_spl
| e21 != op2(h1(e13),h1(e13)) ),
inference(forward_demodulation,[status(thm)],[f1940,f2074]) ).
fof(f2076,plain,
( sQ145_spl
| e21 != op2(e20,h1(e13)) ),
inference(forward_demodulation,[status(thm)],[f290,f2075]) ).
fof(f2077,plain,
( sQ145_spl
| e21 != op2(e20,e20) ),
inference(forward_demodulation,[status(thm)],[f290,f2076]) ).
fof(f2078,plain,
( sQ145_spl
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1931,f2077]) ).
fof(f2079,plain,
( sQ145_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2078]) ).
fof(f2080,plain,
sQ145_spl,
inference(contradiction_clause,[status(thm)],[f2079]) ).
fof(f2109,plain,
( ~ sQ118_spl
| e22 != op2(e23,e22) ),
inference(backward_demodulation,[status(thm)],[f1058,f209]) ).
fof(f2118,plain,
( ~ sQ109_spl
| op2(e22,e21) != e21 ),
inference(backward_demodulation,[status(thm)],[f1029,f204]) ).
fof(f2122,plain,
( ~ sQ121_spl
| op2(e21,e22) != e21 ),
inference(backward_demodulation,[status(thm)],[f1068,f180]) ).
fof(f2126,plain,
( ~ sQ92_spl
| e22 = e20 ),
inference(backward_demodulation,[status(thm)],[f974,f1939]) ).
fof(f2170,plain,
( ~ sQ45_spl
| op1(e12,e12) != e11 ),
inference(backward_demodulation,[status(thm)],[f789,f157]) ).
fof(f2178,plain,
( ~ sQ57_spl
| op1(e11,e12) != e11 ),
inference(backward_demodulation,[status(thm)],[f828,f132]) ).
fof(f2190,plain,
( ~ sQ27_spl
| e13 != op1(e12,e12) ),
inference(backward_demodulation,[status(thm)],[f730,f131]) ).
fof(f2191,plain,
( ~ sQ27_spl
| op1(e10,e12) != e13 ),
inference(backward_demodulation,[status(thm)],[f730,f128]) ).
fof(f2223,plain,
( sQ221_spl
| e23 != e23 ),
inference(forward_demodulation,[status(thm)],[f302,f1458]) ).
fof(f2224,plain,
( sQ221_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2223]) ).
fof(f2225,plain,
sQ221_spl,
inference(contradiction_clause,[status(thm)],[f2224]) ).
fof(f2235,plain,
( ~ sQ85_spl
| h1(e11) = e21 ),
inference(backward_demodulation,[status(thm)],[f951,f1947]) ).
fof(f2237,plain,
( ~ sQ106_spl
| h3(e10) = e22 ),
inference(backward_demodulation,[status(thm)],[f1019,f299]) ).
fof(f2246,plain,
( ~ sQ6_spl
| ~ sQ4_spl
| e10 = e12 ),
inference(backward_demodulation,[status(thm)],[f656,f662]) ).
fof(f2368,plain,
( ~ sQ112_spl
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f1039,f1920]) ).
fof(f2369,plain,
( ~ sQ112_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2368]) ).
fof(f2370,plain,
~ sQ112_spl,
inference(contradiction_clause,[status(thm)],[f2369]) ).
fof(f2385,plain,
( ~ sQ229_spl
| e21 != op2(e23,e21) ),
inference(forward_demodulation,[status(thm)],[f1498,f1944]) ).
fof(f2386,plain,
( ~ sQ229_spl
| ~ sQ117_spl
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1055,f2385]) ).
fof(f2387,plain,
( ~ sQ229_spl
| ~ sQ117_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2386]) ).
fof(f2388,plain,
( ~ sQ229_spl
| ~ sQ117_spl ),
inference(contradiction_clause,[status(thm)],[f2387]) ).
fof(f2410,plain,
( ~ sQ199_spl
| h4(e11) = op2(h4(e10),h4(e10)) ),
inference(forward_demodulation,[status(thm)],[f1909,f1388]) ).
fof(f2436,plain,
( ~ sQ145_spl
| h1(e10) = op2(h1(e13),h1(e13)) ),
inference(forward_demodulation,[status(thm)],[f284,f1214]) ).
fof(f2437,plain,
( ~ sQ145_spl
| e21 = op2(h1(e13),h1(e13)) ),
inference(forward_demodulation,[status(thm)],[f1940,f2436]) ).
fof(f2438,plain,
( ~ sQ145_spl
| e21 = op2(e20,h1(e13)) ),
inference(forward_demodulation,[status(thm)],[f290,f2437]) ).
fof(f2439,plain,
( ~ sQ145_spl
| e21 = op2(e20,e20) ),
inference(forward_demodulation,[status(thm)],[f290,f2438]) ).
fof(f2455,plain,
( ~ sQ118_spl
| ~ sQ122_spl
| e22 != e22 ),
inference(forward_demodulation,[status(thm)],[f1071,f2109]) ).
fof(f2456,plain,
( ~ sQ118_spl
| ~ sQ122_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2455]) ).
fof(f2457,plain,
( ~ sQ118_spl
| ~ sQ122_spl ),
inference(contradiction_clause,[status(thm)],[f2456]) ).
fof(f2466,plain,
( ~ sQ121_spl
| ~ sQ89_spl ),
inference(split_clause,[status(thm)],[f2122,f963,f1067]) ).
fof(f2511,plain,
( ~ sQ45_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f2170,f775,f788]) ).
fof(f2518,plain,
( ~ sQ57_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f2178,f723,f827]) ).
fof(f2564,plain,
( ~ sQ115_spl
| ~ sQ114_spl
| e22 = e23 ),
inference(backward_demodulation,[status(thm)],[f1045,f1048]) ).
fof(f2594,plain,
( ~ sQ85_spl
| sQ229_spl ),
inference(split_clause,[status(thm)],[f2235,f1497,f950]) ).
fof(f2606,plain,
( ~ sQ67_spl
| ~ sQ65_spl
| e21 = e23 ),
inference(forward_demodulation,[status(thm)],[f886,f892]) ).
fof(f2607,plain,
( ~ sQ67_spl
| ~ sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2606,f222]) ).
fof(f2608,plain,
( ~ sQ67_spl
| ~ sQ65_spl ),
inference(contradiction_clause,[status(thm)],[f2607]) ).
fof(f2629,plain,
( ~ sQ62_spl
| e10 = e12 ),
inference(forward_demodulation,[status(thm)],[f284,f844]) ).
fof(f2630,plain,
( ~ sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2629,f213]) ).
fof(f2631,plain,
~ sQ62_spl,
inference(contradiction_clause,[status(thm)],[f2630]) ).
fof(f2633,plain,
( ~ sQ101_spl
| ~ sQ109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1003,f2118]) ).
fof(f2634,plain,
( ~ sQ101_spl
| ~ sQ109_spl ),
inference(contradiction_clause,[status(thm)],[f2633]) ).
fof(f2636,plain,
( ~ sQ29_spl
| e12 = e11 ),
inference(forward_demodulation,[status(thm)],[f737,f1917]) ).
fof(f2637,plain,
( ~ sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2636,f215]) ).
fof(f2638,plain,
~ sQ29_spl,
inference(contradiction_clause,[status(thm)],[f2637]) ).
fof(f2639,plain,
( ~ sQ3_spl
| e11 = e13 ),
inference(forward_demodulation,[status(thm)],[f1909,f652]) ).
fof(f2640,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2639,f216]) ).
fof(f2641,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f2640]) ).
fof(f2642,plain,
( ~ sQ0_spl
| e11 = e10 ),
inference(backward_demodulation,[status(thm)],[f643,f1909]) ).
fof(f2689,plain,
( ~ sQ106_spl
| sQ256_spl ),
inference(split_clause,[status(thm)],[f2237,f1612,f1018]) ).
fof(f2705,plain,
( ~ sQ145_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f2439,f885,f1213]) ).
fof(f2719,plain,
( ~ sQ68_spl
| e20 != op2(e23,e21) ),
inference(forward_demodulation,[status(thm)],[f896,f172]) ).
fof(f2721,plain,
( ~ sQ71_spl
| ~ sQ68_spl
| e20 = e23 ),
inference(forward_demodulation,[status(thm)],[f896,f905]) ).
fof(f2722,plain,
( ~ sQ71_spl
| ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2721,f220]) ).
fof(f2723,plain,
( ~ sQ71_spl
| ~ sQ68_spl ),
inference(contradiction_clause,[status(thm)],[f2722]) ).
fof(f2783,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| e10 = e13 ),
inference(forward_demodulation,[status(thm)],[f656,f665]) ).
fof(f2784,plain,
( ~ sQ7_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2783,f214]) ).
fof(f2785,plain,
( ~ sQ7_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f2784]) ).
fof(f2786,plain,
( ~ sQ39_spl
| ~ sQ38_spl
| e12 = e13 ),
inference(forward_demodulation,[status(thm)],[f766,f769]) ).
fof(f2787,plain,
( ~ sQ39_spl
| ~ sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2786,f217]) ).
fof(f2788,plain,
( ~ sQ39_spl
| ~ sQ38_spl ),
inference(contradiction_clause,[status(thm)],[f2787]) ).
fof(f2791,plain,
( ~ sQ27_spl
| ~ sQ11_spl
| e13 != e13 ),
inference(forward_demodulation,[status(thm)],[f678,f2191]) ).
fof(f2792,plain,
( ~ sQ27_spl
| ~ sQ11_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2791]) ).
fof(f2793,plain,
( ~ sQ27_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f2792]) ).
fof(f2802,plain,
( ~ sQ68_spl
| e20 != op2(e22,e21) ),
inference(forward_demodulation,[status(thm)],[f896,f171]) ).
fof(f2806,plain,
( ~ sQ17_spl
| e11 != e11 ),
inference(forward_demodulation,[status(thm)],[f698,f1908]) ).
fof(f2807,plain,
( ~ sQ17_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2806]) ).
fof(f2808,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f2807]) ).
fof(f2812,plain,
( ~ sQ51_spl
| e13 != op1(e13,e12) ),
inference(forward_demodulation,[status(thm)],[f808,f159]) ).
fof(f2815,plain,
( ~ sQ51_spl
| op1(e11,e10) != e13 ),
inference(forward_demodulation,[status(thm)],[f808,f120]) ).
fof(f2844,plain,
( ~ sQ68_spl
| e20 != op2(e20,e22) ),
inference(forward_demodulation,[status(thm)],[f896,f191]) ).
fof(f2845,plain,
( ~ sQ68_spl
| ~ sQ72_spl
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f909,f2844]) ).
fof(f2846,plain,
( ~ sQ68_spl
| ~ sQ72_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2845]) ).
fof(f2847,plain,
( ~ sQ68_spl
| ~ sQ72_spl ),
inference(contradiction_clause,[status(thm)],[f2846]) ).
fof(f2849,plain,
( ~ sQ111_spl
| op2(e20,e23) != e23 ),
inference(backward_demodulation,[status(thm)],[f1035,f183]) ).
fof(f2857,plain,
( ~ sQ31_spl
| e12 = e13 ),
inference(backward_demodulation,[status(thm)],[f1917,f743]) ).
fof(f2872,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2642,f212]) ).
fof(f2873,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f2872]) ).
fof(f2881,plain,
( ~ sQ199_spl
| h4(e11) = op2(e20,h4(e10)) ),
inference(forward_demodulation,[status(thm)],[f1968,f2410]) ).
fof(f2882,plain,
( ~ sQ199_spl
| h4(e11) = op2(e20,e20) ),
inference(forward_demodulation,[status(thm)],[f1968,f2881]) ).
fof(f2886,plain,
( ~ sQ199_spl
| ~ sQ64_spl
| h4(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f883,f2882]) ).
fof(f2887,plain,
( ~ sQ199_spl
| ~ sQ64_spl
| e20 = e21 ),
inference(forward_demodulation,[status(thm)],[f2886,f1971]) ).
fof(f2888,plain,
( ~ sQ199_spl
| ~ sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2887,f218]) ).
fof(f2889,plain,
( ~ sQ199_spl
| ~ sQ64_spl ),
inference(contradiction_clause,[status(thm)],[f2888]) ).
fof(f2907,plain,
( ~ sQ104_spl
| h3(e10) = e20 ),
inference(backward_demodulation,[status(thm)],[f1013,f299]) ).
fof(f2908,plain,
( ~ sQ98_spl
| e22 != h3(e10) ),
inference(backward_demodulation,[status(thm)],[f993,f1959]) ).
fof(f2911,plain,
( ~ sQ98_spl
| e22 != op2(e22,e21) ),
inference(backward_demodulation,[status(thm)],[f993,f200]) ).
fof(f2917,plain,
( sQ205_spl
| ~ sQ91_spl
| h4(op1(e11,e12)) != e23 ),
inference(backward_demodulation,[status(thm)],[f970,f2006]) ).
fof(f2942,plain,
( ~ sQ70_spl
| ~ sQ68_spl
| e20 = e22 ),
inference(forward_demodulation,[status(thm)],[f896,f902]) ).
fof(f2943,plain,
( ~ sQ70_spl
| ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2942,f219]) ).
fof(f2944,plain,
( ~ sQ70_spl
| ~ sQ68_spl ),
inference(contradiction_clause,[status(thm)],[f2943]) ).
fof(f2946,plain,
( sQ200_spl
| ~ sQ68_spl
| h4(op1(e10,e11)) != e20 ),
inference(forward_demodulation,[status(thm)],[f896,f2017]) ).
fof(f2965,plain,
( ~ sQ6_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2246,f213]) ).
fof(f2966,plain,
( ~ sQ6_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f2965]) ).
fof(f2968,plain,
( ~ sQ10_spl
| e12 != op1(e13,e12) ),
inference(forward_demodulation,[status(thm)],[f675,f130]) ).
fof(f2969,plain,
( ~ sQ10_spl
| ~ sQ58_spl
| e12 != e12 ),
inference(forward_demodulation,[status(thm)],[f831,f2968]) ).
fof(f2970,plain,
( ~ sQ10_spl
| ~ sQ58_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2969]) ).
fof(f2971,plain,
( ~ sQ10_spl
| ~ sQ58_spl ),
inference(contradiction_clause,[status(thm)],[f2970]) ).
fof(f2978,plain,
( ~ sQ4_spl
| e10 != op1(e10,e12) ),
inference(forward_demodulation,[status(thm)],[f656,f143]) ).
fof(f2980,plain,
( ~ sQ10_spl
| e12 != op1(e12,e12) ),
inference(forward_demodulation,[status(thm)],[f675,f129]) ).
fof(f2981,plain,
( ~ sQ80_spl
| e20 != op2(e21,e22) ),
inference(forward_demodulation,[status(thm)],[f935,f195]) ).
fof(f3002,plain,
( ~ sQ15_spl
| ~ sQ13_spl
| e11 = e13 ),
inference(forward_demodulation,[status(thm)],[f685,f691]) ).
fof(f3003,plain,
( ~ sQ15_spl
| ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3002,f216]) ).
fof(f3004,plain,
( ~ sQ15_spl
| ~ sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f3003]) ).
fof(f3053,plain,
( ~ sQ111_spl
| ~ sQ79_spl
| e23 != e23 ),
inference(forward_demodulation,[status(thm)],[f931,f2849]) ).
fof(f3054,plain,
( ~ sQ111_spl
| ~ sQ79_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3053]) ).
fof(f3055,plain,
( ~ sQ111_spl
| ~ sQ79_spl ),
inference(contradiction_clause,[status(thm)],[f3054]) ).
fof(f3057,plain,
( ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2857,f217]) ).
fof(f3058,plain,
~ sQ31_spl,
inference(contradiction_clause,[status(thm)],[f3057]) ).
fof(f3060,plain,
( ~ sQ63_spl
| e10 = e13 ),
inference(forward_demodulation,[status(thm)],[f284,f847]) ).
fof(f3061,plain,
( ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3060,f214]) ).
fof(f3062,plain,
~ sQ63_spl,
inference(contradiction_clause,[status(thm)],[f3061]) ).
fof(f3075,plain,
( sQ270_spl
| e22 != e22 ),
inference(forward_demodulation,[status(thm)],[f1975,f1673]) ).
fof(f3076,plain,
( sQ270_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3075]) ).
fof(f3077,plain,
sQ270_spl,
inference(contradiction_clause,[status(thm)],[f3076]) ).
fof(f3082,plain,
( sQ265_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1971,f1652]) ).
fof(f3083,plain,
sQ265_spl,
inference(contradiction_clause,[status(thm)],[f3082]) ).
fof(f3086,plain,
( ~ sQ199_spl
| ~ sQ65_spl
| h4(e11) = e21 ),
inference(forward_demodulation,[status(thm)],[f886,f2882]) ).
fof(f3120,plain,
( ~ sQ90_spl
| e22 != e22 ),
inference(forward_demodulation,[status(thm)],[f967,f1934]) ).
fof(f3121,plain,
( ~ sQ90_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3120]) ).
fof(f3122,plain,
~ sQ90_spl,
inference(contradiction_clause,[status(thm)],[f3121]) ).
fof(f3127,plain,
( ~ sQ51_spl
| e13 != op1(e13,e11) ),
inference(backward_demodulation,[status(thm)],[f808,f158]) ).
fof(f3133,plain,
( sQ211_spl
| ~ sQ51_spl
| h4(e13) != op2(e23,e20) ),
inference(backward_demodulation,[status(thm)],[f808,f1988]) ).
fof(f3139,plain,
( ~ sQ51_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f2815,f703,f807]) ).
fof(f3141,plain,
( ~ sQ2_spl
| e11 = e12 ),
inference(forward_demodulation,[status(thm)],[f1909,f649]) ).
fof(f3142,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3141,f215]) ).
fof(f3143,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f3142]) ).
fof(f3147,plain,
( sQ200_spl
| ~ sQ68_spl
| ~ sQ4_spl
| h4(e10) != e20 ),
inference(forward_demodulation,[status(thm)],[f656,f2946]) ).
fof(f3148,plain,
( sQ200_spl
| ~ sQ68_spl
| ~ sQ4_spl
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f1968,f3147]) ).
fof(f3149,plain,
( sQ200_spl
| ~ sQ68_spl
| ~ sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3148]) ).
fof(f3150,plain,
( sQ200_spl
| ~ sQ68_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f3149]) ).
fof(f3161,plain,
( ~ sQ51_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f2812,f833,f807]) ).
fof(f3192,plain,
( ~ sQ4_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f2978,f668,f655]) ).
fof(f3210,plain,
( ~ sQ115_spl
| ~ sQ114_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2564,f223]) ).
fof(f3211,plain,
( ~ sQ115_spl
| ~ sQ114_spl ),
inference(contradiction_clause,[status(thm)],[f3210]) ).
fof(f3221,plain,
( ~ sQ75_spl
| ~ sQ74_spl
| e22 = e23 ),
inference(backward_demodulation,[status(thm)],[f915,f918]) ).
fof(f3228,plain,
( ~ sQ125_spl
| e20 = e21 ),
inference(forward_demodulation,[status(thm)],[f287,f1081]) ).
fof(f3229,plain,
( ~ sQ125_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3228,f218]) ).
fof(f3230,plain,
~ sQ125_spl,
inference(contradiction_clause,[status(thm)],[f3229]) ).
fof(f3235,plain,
( ~ sQ10_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f2980,f778,f674]) ).
fof(f3273,plain,
( sQ260_spl
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f1968,f1631]) ).
fof(f3274,plain,
( sQ260_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3273]) ).
fof(f3275,plain,
sQ260_spl,
inference(contradiction_clause,[status(thm)],[f3274]) ).
fof(f3284,plain,
( ~ sQ127_spl
| e20 = e23 ),
inference(forward_demodulation,[status(thm)],[f287,f1087]) ).
fof(f3285,plain,
( ~ sQ127_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3284,f220]) ).
fof(f3286,plain,
~ sQ127_spl,
inference(contradiction_clause,[status(thm)],[f3285]) ).
fof(f3317,plain,
( ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f825,f1896]) ).
fof(f3318,plain,
~ sQ56_spl,
inference(contradiction_clause,[status(thm)],[f3317]) ).
fof(f3319,plain,
( ~ sQ61_spl
| e10 = e11 ),
inference(forward_demodulation,[status(thm)],[f284,f841]) ).
fof(f3320,plain,
( ~ sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3319,f212]) ).
fof(f3321,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f3320]) ).
fof(f3335,plain,
( sQ207_spl
| ~ sQ34_spl
| h4(e12) != op2(e22,e20) ),
inference(backward_demodulation,[status(thm)],[f753,f1997]) ).
fof(f3353,plain,
( sQ204_spl
| ~ sQ21_spl
| h4(e11) != h1(e11) ),
inference(backward_demodulation,[status(thm)],[f711,f2009]) ).
fof(f3372,plain,
( ~ sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1026,f1921]) ).
fof(f3373,plain,
~ sQ108_spl,
inference(contradiction_clause,[status(thm)],[f3372]) ).
fof(f3381,plain,
( ~ sQ68_spl
| ~ sQ116_spl ),
inference(split_clause,[status(thm)],[f2719,f1051,f895]) ).
fof(f3388,plain,
( sQ209_spl
| ~ sQ104_spl
| h4(op1(e12,e12)) != e20 ),
inference(backward_demodulation,[status(thm)],[f2907,f1993]) ).
fof(f3394,plain,
( ~ sQ98_spl
| ~ sQ102_spl ),
inference(split_clause,[status(thm)],[f2911,f1005,f992]) ).
fof(f3395,plain,
( ~ sQ98_spl
| e22 != op2(e22,e23) ),
inference(backward_demodulation,[status(thm)],[f993,f202]) ).
fof(f3403,plain,
( ~ sQ113_spl
| e21 != e21 ),
inference(forward_demodulation,[status(thm)],[f1042,f1928]) ).
fof(f3404,plain,
( ~ sQ113_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3403]) ).
fof(f3405,plain,
~ sQ113_spl,
inference(contradiction_clause,[status(thm)],[f3404]) ).
fof(f3415,plain,
( sQ203_spl
| ~ sQ16_spl
| h4(e10) != op2(e21,e20) ),
inference(forward_demodulation,[status(thm)],[f695,f2011]) ).
fof(f3416,plain,
( sQ203_spl
| ~ sQ16_spl
| e20 != op2(e21,e20) ),
inference(forward_demodulation,[status(thm)],[f1968,f3415]) ).
fof(f3419,plain,
( ~ sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f941,f1936]) ).
fof(f3420,plain,
~ sQ82_spl,
inference(contradiction_clause,[status(thm)],[f3419]) ).
fof(f3426,plain,
( ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f672,f1904]) ).
fof(f3427,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f3426]) ).
fof(f3447,plain,
( ~ sQ27_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f2190,f781,f729]) ).
fof(f3448,plain,
( sQ202_spl
| ~ sQ15_spl
| h4(e13) != op2(e20,e23) ),
inference(backward_demodulation,[status(thm)],[f691,f2013]) ).
fof(f3457,plain,
( ~ sQ51_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f3127,f820,f807]) ).
fof(f3463,plain,
( sQ211_spl
| ~ sQ51_spl
| e23 != op2(e23,e20) ),
inference(forward_demodulation,[status(thm)],[f302,f3133]) ).
fof(f3469,plain,
( sQ210_spl
| ~ sQ45_spl
| h4(e11) != op2(e22,e23) ),
inference(forward_demodulation,[status(thm)],[f789,f1990]) ).
fof(f3470,plain,
( sQ210_spl
| ~ sQ45_spl
| ~ sQ199_spl
| ~ sQ65_spl
| e21 != op2(e22,e23) ),
inference(forward_demodulation,[status(thm)],[f3086,f3469]) ).
fof(f3495,plain,
( sQ204_spl
| ~ sQ21_spl
| ~ sQ199_spl
| ~ sQ65_spl
| e21 != h1(e11) ),
inference(forward_demodulation,[status(thm)],[f3086,f3353]) ).
fof(f3520,plain,
( ~ sQ115_spl
| sQ211_spl
| ~ sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1048,f3463]) ).
fof(f3521,plain,
( ~ sQ115_spl
| sQ211_spl
| ~ sQ51_spl ),
inference(contradiction_clause,[status(thm)],[f3520]) ).
fof(f3528,plain,
( ~ sQ109_spl
| sQ210_spl
| ~ sQ45_spl
| ~ sQ199_spl
| ~ sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1029,f3470]) ).
fof(f3529,plain,
( ~ sQ109_spl
| sQ210_spl
| ~ sQ45_spl
| ~ sQ199_spl
| ~ sQ65_spl ),
inference(contradiction_clause,[status(thm)],[f3528]) ).
fof(f3545,plain,
( ~ sQ98_spl
| ~ sQ110_spl ),
inference(split_clause,[status(thm)],[f3395,f1031,f992]) ).
fof(f3546,plain,
( ~ sQ98_spl
| ~ sQ96_spl
| e20 = e22 ),
inference(forward_demodulation,[status(thm)],[f987,f993]) ).
fof(f3547,plain,
( ~ sQ98_spl
| ~ sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3546,f219]) ).
fof(f3548,plain,
( ~ sQ98_spl
| ~ sQ96_spl ),
inference(contradiction_clause,[status(thm)],[f3547]) ).
fof(f3549,plain,
( ~ sQ98_spl
| ~ sQ256_spl ),
inference(split_clause,[status(thm)],[f2908,f1612,f992]) ).
fof(f3550,plain,
( ~ sQ68_spl
| ~ sQ100_spl ),
inference(split_clause,[status(thm)],[f2802,f999,f895]) ).
fof(f3568,plain,
( ~ sQ18_spl
| e12 != e12 ),
inference(forward_demodulation,[status(thm)],[f701,f1914]) ).
fof(f3569,plain,
( ~ sQ18_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3568]) ).
fof(f3570,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f3569]) ).
fof(f3587,plain,
( sQ202_spl
| ~ sQ15_spl
| e23 != op2(e20,e23) ),
inference(forward_demodulation,[status(thm)],[f302,f3448]) ).
fof(f3605,plain,
( sQ208_spl
| ~ sQ39_spl
| h4(e13) != op2(e22,e21) ),
inference(backward_demodulation,[status(thm)],[f769,f1995]) ).
fof(f3626,plain,
( sQ207_spl
| ~ sQ34_spl
| e22 != op2(e22,e20) ),
inference(forward_demodulation,[status(thm)],[f1975,f3335]) ).
fof(f3631,plain,
( sQ203_spl
| ~ sQ16_spl
| ~ sQ80_spl ),
inference(split_clause,[status(thm)],[f3416,f934,f694,f1399]) ).
fof(f3664,plain,
( ~ sQ120_spl
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f1065,f1918]) ).
fof(f3665,plain,
( ~ sQ120_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3664]) ).
fof(f3666,plain,
~ sQ120_spl,
inference(contradiction_clause,[status(thm)],[f3665]) ).
fof(f3669,plain,
( sQ213_spl
| ~ sQ57_spl
| h4(e11) != op2(e23,e22) ),
inference(forward_demodulation,[status(thm)],[f828,f1984]) ).
fof(f3670,plain,
( sQ213_spl
| ~ sQ57_spl
| ~ sQ199_spl
| ~ sQ65_spl
| e21 != op2(e23,e22) ),
inference(forward_demodulation,[status(thm)],[f3086,f3669]) ).
fof(f3673,plain,
( sQ212_spl
| ~ sQ54_spl
| h4(e12) != op2(e23,e21) ),
inference(forward_demodulation,[status(thm)],[f818,f1986]) ).
fof(f3674,plain,
( sQ212_spl
| ~ sQ54_spl
| e22 != op2(e23,e21) ),
inference(forward_demodulation,[status(thm)],[f1975,f3673]) ).
fof(f3675,plain,
( sQ212_spl
| ~ sQ54_spl
| ~ sQ118_spl
| e22 != e22 ),
inference(forward_demodulation,[status(thm)],[f1058,f3674]) ).
fof(f3676,plain,
( sQ212_spl
| ~ sQ54_spl
| ~ sQ118_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3675]) ).
fof(f3677,plain,
( sQ212_spl
| ~ sQ54_spl
| ~ sQ118_spl ),
inference(contradiction_clause,[status(thm)],[f3676]) ).
fof(f3693,plain,
( ~ sQ80_spl
| ~ sQ88_spl ),
inference(split_clause,[status(thm)],[f2981,f960,f934]) ).
fof(f3695,plain,
( sQ201_spl
| ~ sQ10_spl
| h4(e12) != op2(e20,e22) ),
inference(forward_demodulation,[status(thm)],[f675,f2015]) ).
fof(f3696,plain,
( sQ201_spl
| ~ sQ10_spl
| e22 != op2(e20,e22) ),
inference(forward_demodulation,[status(thm)],[f1975,f3695]) ).
fof(f3700,plain,
( ~ sQ98_spl
| sQ207_spl
| ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f993,f3626]) ).
fof(f3701,plain,
( ~ sQ98_spl
| sQ207_spl
| ~ sQ34_spl ),
inference(contradiction_clause,[status(thm)],[f3700]) ).
fof(f3755,plain,
( sQ209_spl
| ~ sQ104_spl
| ~ sQ40_spl
| h4(e10) != e20 ),
inference(forward_demodulation,[status(thm)],[f773,f3388]) ).
fof(f3756,plain,
( sQ209_spl
| ~ sQ104_spl
| ~ sQ40_spl
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f1968,f3755]) ).
fof(f3757,plain,
( sQ209_spl
| ~ sQ104_spl
| ~ sQ40_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3756]) ).
fof(f3758,plain,
( sQ209_spl
| ~ sQ104_spl
| ~ sQ40_spl ),
inference(contradiction_clause,[status(thm)],[f3757]) ).
fof(f3763,plain,
( ~ sQ121_spl
| sQ213_spl
| ~ sQ57_spl
| ~ sQ199_spl
| ~ sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1068,f3670]) ).
fof(f3764,plain,
( ~ sQ121_spl
| sQ213_spl
| ~ sQ57_spl
| ~ sQ199_spl
| ~ sQ65_spl ),
inference(contradiction_clause,[status(thm)],[f3763]) ).
fof(f3765,plain,
( ~ sQ75_spl
| ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3221,f223]) ).
fof(f3766,plain,
( ~ sQ75_spl
| ~ sQ74_spl ),
inference(contradiction_clause,[status(thm)],[f3765]) ).
fof(f3767,plain,
( ~ sQ74_spl
| sQ201_spl
| ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f915,f3696]) ).
fof(f3768,plain,
( ~ sQ74_spl
| sQ201_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f3767]) ).
fof(f3815,plain,
( sQ208_spl
| ~ sQ39_spl
| e23 != op2(e22,e21) ),
inference(forward_demodulation,[status(thm)],[f302,f3605]) ).
fof(f3828,plain,
( ~ sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2126,f219]) ).
fof(f3829,plain,
~ sQ92_spl,
inference(contradiction_clause,[status(thm)],[f3828]) ).
fof(f3836,plain,
( ~ sQ103_spl
| sQ208_spl
| ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1009,f3815]) ).
fof(f3837,plain,
( ~ sQ103_spl
| sQ208_spl
| ~ sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f3836]) ).
fof(f3853,plain,
( sQ205_spl
| ~ sQ91_spl
| ~ sQ27_spl
| h4(e13) != e23 ),
inference(forward_demodulation,[status(thm)],[f730,f2917]) ).
fof(f3854,plain,
( sQ205_spl
| ~ sQ91_spl
| ~ sQ27_spl
| e23 != e23 ),
inference(forward_demodulation,[status(thm)],[f302,f3853]) ).
fof(f3855,plain,
( sQ205_spl
| ~ sQ91_spl
| ~ sQ27_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3854]) ).
fof(f3856,plain,
( sQ205_spl
| ~ sQ91_spl
| ~ sQ27_spl ),
inference(contradiction_clause,[status(thm)],[f3855]) ).
fof(f3895,plain,
( sQ204_spl
| ~ sQ21_spl
| ~ sQ199_spl
| ~ sQ65_spl
| ~ sQ229_spl ),
inference(split_clause,[status(thm)],[f3495,f1497,f885,f1387,f710,f1402]) ).
fof(f3939,plain,
( ~ sQ79_spl
| sQ202_spl
| ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f931,f3587]) ).
fof(f3940,plain,
( ~ sQ79_spl
| sQ202_spl
| ~ sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f3939]) ).
fof(f3941,plain,
$false,
inference(sat_refutation,[status(thm)],[f654,f680,f706,f784,f836,f849,f856,f860,f863,f864,f865,f877,f972,f1011,f1037,f1091,f1095,f1096,f1103,f1107,f1111,f1114,f1116,f1124,f1129,f1130,f1131,f1135,f1145,f1147,f1148,f1152,f1158,f1459,f1632,f1653,f1674,f1982,f2004,f2024,f2080,f2225,f2370,f2388,f2457,f2466,f2511,f2518,f2594,f2608,f2631,f2634,f2638,f2641,f2689,f2705,f2723,f2785,f2788,f2793,f2808,f2847,f2873,f2889,f2944,f2966,f2971,f3004,f3055,f3058,f3062,f3077,f3083,f3122,f3139,f3143,f3150,f3161,f3192,f3211,f3230,f3235,f3275,f3286,f3318,f3321,f3373,f3381,f3394,f3405,f3420,f3427,f3447,f3457,f3521,f3529,f3545,f3548,f3549,f3550,f3570,f3631,f3666,f3677,f3693,f3701,f3758,f3764,f3766,f3768,f3829,f3837,f3856,f3895,f3940]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG121+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 13:02:44 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.41 % Drodi V4.1.1
% 0.14/0.61 % Refutation found
% 0.14/0.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.61 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.67 % Elapsed time: 0.282543 seconds
% 0.14/0.67 % CPU time: 1.319553 seconds
% 0.14/0.67 % Total memory used: 142.950 MB
% 0.14/0.67 % Net memory used: 142.329 MB
%------------------------------------------------------------------------------