%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG031+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 11:47:49 AM UTC 2026
% Result : Theorem 0.12s 0.45s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 65
% Syntax : Number of formulae : 508 ( 103 unt; 60 def)
% Number of atoms : 1566 ( 996 equ)
% Maximal formula atoms : 156 ( 3 avg)
% Number of connectives : 1502 ( 444 ~; 615 |; 381 &)
% ( 60 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 96 ( 3 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 62 ( 60 usr; 61 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 12 con; 0-2 aty)
% Number of variables : 0 ( 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( e14 != e15
& e13 != e15
& e13 != e14
& e12 != e15
& e12 != e14
& e12 != e13
& e11 != e15
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e15
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
( e24 != e25
& e23 != e25
& e23 != e24
& e22 != e25
& e22 != e24
& e22 != e23
& e21 != e25
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e25
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
( op1(e15,e15) = e12
& op1(e15,e14) = e10
& op1(e15,e13) = e14
& op1(e15,e12) = e11
& op1(e15,e11) = e13
& op1(e15,e10) = e15
& op1(e14,e15) = e10
& op1(e14,e14) = e13
& op1(e14,e13) = e11
& op1(e14,e12) = e15
& op1(e14,e11) = e12
& op1(e14,e10) = e14
& op1(e13,e15) = e14
& op1(e13,e14) = e11
& op1(e13,e13) = e12
& op1(e13,e12) = e10
& op1(e13,e11) = e15
& op1(e13,e10) = e13
& op1(e12,e15) = e11
& op1(e12,e14) = e15
& op1(e12,e13) = e10
& op1(e12,e12) = e13
& op1(e12,e11) = e14
& op1(e12,e10) = e12
& op1(e11,e15) = e13
& op1(e11,e14) = e12
& op1(e11,e13) = e15
& op1(e11,e12) = e14
& op1(e11,e11) = e10
& op1(e11,e10) = e11
& op1(e10,e15) = e15
& op1(e10,e14) = e14
& op1(e10,e13) = e13
& op1(e10,e12) = e12
& op1(e10,e11) = e11
& op1(e10,e10) = e10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
( op2(e25,e25) = e20
& op2(e25,e24) = e22
& op2(e25,e23) = e21
& op2(e25,e22) = e24
& op2(e25,e21) = e23
& op2(e25,e20) = e25
& op2(e24,e25) = e21
& op2(e24,e24) = e23
& op2(e24,e23) = e20
& op2(e24,e22) = e25
& op2(e24,e21) = e22
& op2(e24,e20) = e24
& op2(e23,e25) = e22
& op2(e23,e24) = e20
& op2(e23,e23) = e24
& op2(e23,e22) = e21
& op2(e23,e21) = e25
& op2(e23,e20) = e23
& op2(e22,e25) = e23
& op2(e22,e24) = e21
& op2(e22,e23) = e25
& op2(e22,e22) = e20
& op2(e22,e21) = e24
& op2(e22,e20) = e22
& op2(e21,e25) = e24
& op2(e21,e24) = e25
& op2(e21,e23) = e22
& op2(e21,e22) = e23
& op2(e21,e21) = e20
& op2(e21,e20) = e21
& op2(e20,e25) = e25
& op2(e20,e24) = e24
& op2(e20,e23) = e23
& op2(e20,e22) = e22
& op2(e20,e21) = e21
& op2(e20,e20) = e20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,conjecture,
( ( ( j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e25
| h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e15)) = e15
& j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e25)) = e25
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& j(op2(e25,e25)) = op1(j(e25),j(e25))
& j(op2(e25,e24)) = op1(j(e25),j(e24))
& j(op2(e25,e23)) = op1(j(e25),j(e23))
& j(op2(e25,e22)) = op1(j(e25),j(e22))
& j(op2(e25,e21)) = op1(j(e25),j(e21))
& j(op2(e25,e20)) = op1(j(e25),j(e20))
& j(op2(e24,e25)) = op1(j(e24),j(e25))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e23,e25)) = op1(j(e23),j(e25))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e22,e25)) = op1(j(e22),j(e25))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e21,e25)) = op1(j(e21),j(e25))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e20,e25)) = op1(j(e20),j(e25))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& h(op1(e15,e15)) = op2(h(e15),h(e15))
& h(op1(e15,e14)) = op2(h(e15),h(e14))
& h(op1(e15,e13)) = op2(h(e15),h(e13))
& h(op1(e15,e12)) = op2(h(e15),h(e12))
& h(op1(e15,e11)) = op2(h(e15),h(e11))
& h(op1(e15,e10)) = op2(h(e15),h(e10))
& h(op1(e14,e15)) = op2(h(e14),h(e15))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e13,e15)) = op2(h(e13),h(e15))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e12,e15)) = op2(h(e12),h(e15))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e11,e15)) = op2(h(e11),h(e15))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e10,e15)) = op2(h(e10),h(e15))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e10)) = op2(h(e10),h(e10)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,negated_conjecture,
~ ( ( ( j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e25
| h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e15)) = e15
& j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e25)) = e25
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& j(op2(e25,e25)) = op1(j(e25),j(e25))
& j(op2(e25,e24)) = op1(j(e25),j(e24))
& j(op2(e25,e23)) = op1(j(e25),j(e23))
& j(op2(e25,e22)) = op1(j(e25),j(e22))
& j(op2(e25,e21)) = op1(j(e25),j(e21))
& j(op2(e25,e20)) = op1(j(e25),j(e20))
& j(op2(e24,e25)) = op1(j(e24),j(e25))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e23,e25)) = op1(j(e23),j(e25))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e22,e25)) = op1(j(e22),j(e25))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e21,e25)) = op1(j(e21),j(e25))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e20,e25)) = op1(j(e20),j(e25))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& h(op1(e15,e15)) = op2(h(e15),h(e15))
& h(op1(e15,e14)) = op2(h(e15),h(e14))
& h(op1(e15,e13)) = op2(h(e15),h(e13))
& h(op1(e15,e12)) = op2(h(e15),h(e12))
& h(op1(e15,e11)) = op2(h(e15),h(e11))
& h(op1(e15,e10)) = op2(h(e15),h(e10))
& h(op1(e14,e15)) = op2(h(e14),h(e15))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e13,e15)) = op2(h(e13),h(e15))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e12,e15)) = op2(h(e12),h(e15))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e11,e15)) = op2(h(e11),h(e15))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e10,e15)) = op2(h(e10),h(e15))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e10)) = op2(h(e10),h(e10)) ) ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f8,plain,
e10 != e11,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f15,plain,
e11 != e14,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f16,plain,
e11 != e15,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f17,plain,
e12 != e13,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f18,plain,
e12 != e14,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f19,plain,
e12 != e15,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f20,plain,
e13 != e14,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f21,plain,
e13 != e15,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f22,plain,
e14 != e15,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f24,plain,
e20 != e22,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f25,plain,
e20 != e23,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f28,plain,
e21 != e22,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f32,plain,
e22 != e23,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f35,plain,
e23 != e24,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f37,plain,
e24 != e25,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f74,plain,
op1(e10,e10) = e10,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f81,plain,
op1(e11,e11) = e10,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f83,plain,
op1(e11,e13) = e15,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f84,plain,
op1(e11,e14) = e12,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f88,plain,
op1(e12,e12) = e13,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f91,plain,
op1(e12,e15) = e11,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f95,plain,
op1(e13,e13) = e12,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f96,plain,
op1(e13,e14) = e11,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f101,plain,
op1(e14,e13) = e11,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f102,plain,
op1(e14,e14) = e13,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f105,plain,
op1(e15,e11) = e13,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f109,plain,
op1(e15,e15) = e12,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f110,plain,
op2(e20,e20) = e20,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f111,plain,
op2(e20,e21) = e21,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f115,plain,
op2(e20,e25) = e25,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f116,plain,
op2(e21,e20) = e21,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f117,plain,
op2(e21,e21) = e20,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f118,plain,
op2(e21,e22) = e23,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f124,plain,
op2(e22,e22) = e20,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f126,plain,
op2(e22,e24) = e21,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f127,plain,
op2(e22,e25) = e23,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f131,plain,
op2(e23,e23) = e24,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f132,plain,
op2(e23,e24) = e20,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f134,plain,
op2(e24,e20) = e24,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f138,plain,
op2(e24,e24) = e23,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f145,plain,
op2(e25,e25) = e20,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f146,plain,
( j(h(e15)) = e15
& j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e25)) = e25
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& j(op2(e25,e25)) = op1(j(e25),j(e25))
& j(op2(e25,e24)) = op1(j(e25),j(e24))
& j(op2(e25,e23)) = op1(j(e25),j(e23))
& j(op2(e25,e22)) = op1(j(e25),j(e22))
& j(op2(e25,e21)) = op1(j(e25),j(e21))
& j(op2(e25,e20)) = op1(j(e25),j(e20))
& j(op2(e24,e25)) = op1(j(e24),j(e25))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e23,e25)) = op1(j(e23),j(e25))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e22,e25)) = op1(j(e22),j(e25))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e21,e25)) = op1(j(e21),j(e25))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e20,e25)) = op1(j(e20),j(e25))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& h(op1(e15,e15)) = op2(h(e15),h(e15))
& h(op1(e15,e14)) = op2(h(e15),h(e14))
& h(op1(e15,e13)) = op2(h(e15),h(e13))
& h(op1(e15,e12)) = op2(h(e15),h(e12))
& h(op1(e15,e11)) = op2(h(e15),h(e11))
& h(op1(e15,e10)) = op2(h(e15),h(e10))
& h(op1(e14,e15)) = op2(h(e14),h(e15))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e13,e15)) = op2(h(e13),h(e15))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e12,e15)) = op2(h(e12),h(e15))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e11,e15)) = op2(h(e11),h(e15))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e10,e15)) = op2(h(e10),h(e15))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e10)) = op2(h(e10),h(e10))
& ( j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e25
| h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f148,plain,
( h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f149,plain,
( h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f151,plain,
( h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f152,plain,
( h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f155,plain,
( j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f159,plain,
h(op1(e10,e10)) = op2(h(e10),h(e10)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f166,plain,
h(op1(e11,e11)) = op2(h(e11),h(e11)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f168,plain,
h(op1(e11,e13)) = op2(h(e11),h(e13)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f173,plain,
h(op1(e12,e12)) = op2(h(e12),h(e12)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f180,plain,
h(op1(e13,e13)) = op2(h(e13),h(e13)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f181,plain,
h(op1(e13,e14)) = op2(h(e13),h(e14)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f186,plain,
h(op1(e14,e13)) = op2(h(e14),h(e13)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f187,plain,
h(op1(e14,e14)) = op2(h(e14),h(e14)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f194,plain,
h(op1(e15,e15)) = op2(h(e15),h(e15)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f195,plain,
j(op2(e20,e20)) = op1(j(e20),j(e20)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f196,plain,
j(op2(e20,e21)) = op1(j(e20),j(e21)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f202,plain,
j(op2(e21,e21)) = op1(j(e21),j(e21)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f203,plain,
j(op2(e21,e22)) = op1(j(e21),j(e22)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f209,plain,
j(op2(e22,e22)) = op1(j(e22),j(e22)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f211,plain,
j(op2(e22,e24)) = op1(j(e22),j(e24)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f212,plain,
j(op2(e22,e25)) = op1(j(e22),j(e25)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f216,plain,
j(op2(e23,e23)) = op1(j(e23),j(e23)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f217,plain,
j(op2(e23,e24)) = op1(j(e23),j(e24)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f219,plain,
j(op2(e24,e20)) = op1(j(e24),j(e20)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f223,plain,
j(op2(e24,e24)) = op1(j(e24),j(e24)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f230,plain,
j(op2(e25,e25)) = op1(j(e25),j(e25)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f231,plain,
h(j(e20)) = e20,
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f232,plain,
h(j(e21)) = e21,
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f233,plain,
h(j(e22)) = e22,
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f234,plain,
h(j(e23)) = e23,
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f235,plain,
h(j(e24)) = e24,
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f236,plain,
h(j(e25)) = e25,
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f238,plain,
j(h(e11)) = e11,
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f239,plain,
j(h(e12)) = e12,
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f240,plain,
j(h(e13)) = e13,
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f241,plain,
j(h(e14)) = e14,
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f242,plain,
j(h(e15)) = e15,
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f243,definition,
( sQ0_spl
<=> h(e10) = e20 ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f244,plain,
( ~ sQ0_spl
| h(e10) = e20 ),
inference(component_clause,[status(thm)],[f243]) ).
fof(f246,definition,
( sQ1_spl
<=> h(e10) = e21 ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f247,plain,
( ~ sQ1_spl
| h(e10) = e21 ),
inference(component_clause,[status(thm)],[f246]) ).
fof(f249,definition,
( sQ2_spl
<=> h(e10) = e22 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f250,plain,
( ~ sQ2_spl
| h(e10) = e22 ),
inference(component_clause,[status(thm)],[f249]) ).
fof(f252,definition,
( sQ3_spl
<=> h(e10) = e23 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f253,plain,
( ~ sQ3_spl
| h(e10) = e23 ),
inference(component_clause,[status(thm)],[f252]) ).
fof(f255,definition,
( sQ4_spl
<=> h(e10) = e24 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f256,plain,
( ~ sQ4_spl
| h(e10) = e24 ),
inference(component_clause,[status(thm)],[f255]) ).
fof(f262,definition,
( sQ6_spl
<=> h(e11) = e20 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f263,plain,
( ~ sQ6_spl
| h(e11) = e20 ),
inference(component_clause,[status(thm)],[f262]) ).
fof(f265,definition,
( sQ7_spl
<=> h(e11) = e21 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f266,plain,
( ~ sQ7_spl
| h(e11) = e21 ),
inference(component_clause,[status(thm)],[f265]) ).
fof(f268,definition,
( sQ8_spl
<=> h(e11) = e22 ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f269,plain,
( ~ sQ8_spl
| h(e11) = e22 ),
inference(component_clause,[status(thm)],[f268]) ).
fof(f271,definition,
( sQ9_spl
<=> h(e11) = e23 ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f272,plain,
( ~ sQ9_spl
| h(e11) = e23 ),
inference(component_clause,[status(thm)],[f271]) ).
fof(f274,definition,
( sQ10_spl
<=> h(e11) = e24 ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f277,definition,
( sQ11_spl
<=> h(e11) = e25 ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f278,plain,
( ~ sQ11_spl
| h(e11) = e25 ),
inference(component_clause,[status(thm)],[f277]) ).
fof(f279,plain,
( sQ11_spl
| h(e11) != e25 ),
inference(component_clause,[status(thm)],[f277]) ).
fof(f280,plain,
( sQ11_spl
| sQ10_spl
| sQ9_spl
| sQ8_spl
| sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f148,f262,f265,f268,f271,f274,f277]) ).
fof(f281,definition,
( sQ12_spl
<=> h(e12) = e20 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f282,plain,
( ~ sQ12_spl
| h(e12) = e20 ),
inference(component_clause,[status(thm)],[f281]) ).
fof(f283,plain,
( sQ12_spl
| h(e12) != e20 ),
inference(component_clause,[status(thm)],[f281]) ).
fof(f284,definition,
( sQ13_spl
<=> h(e12) = e21 ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f285,plain,
( ~ sQ13_spl
| h(e12) = e21 ),
inference(component_clause,[status(thm)],[f284]) ).
fof(f287,definition,
( sQ14_spl
<=> h(e12) = e22 ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f288,plain,
( ~ sQ14_spl
| h(e12) = e22 ),
inference(component_clause,[status(thm)],[f287]) ).
fof(f290,definition,
( sQ15_spl
<=> h(e12) = e23 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f291,plain,
( ~ sQ15_spl
| h(e12) = e23 ),
inference(component_clause,[status(thm)],[f290]) ).
fof(f292,plain,
( sQ15_spl
| h(e12) != e23 ),
inference(component_clause,[status(thm)],[f290]) ).
fof(f293,definition,
( sQ16_spl
<=> h(e12) = e24 ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f294,plain,
( ~ sQ16_spl
| h(e12) = e24 ),
inference(component_clause,[status(thm)],[f293]) ).
fof(f296,definition,
( sQ17_spl
<=> h(e12) = e25 ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f297,plain,
( ~ sQ17_spl
| h(e12) = e25 ),
inference(component_clause,[status(thm)],[f296]) ).
fof(f299,plain,
( sQ17_spl
| sQ16_spl
| sQ15_spl
| sQ14_spl
| sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f149,f281,f284,f287,f290,f293,f296]) ).
fof(f300,definition,
( sQ18_spl
<=> h(e13) = e20 ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f301,plain,
( ~ sQ18_spl
| h(e13) = e20 ),
inference(component_clause,[status(thm)],[f300]) ).
fof(f306,definition,
( sQ20_spl
<=> h(e13) = e22 ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f307,plain,
( ~ sQ20_spl
| h(e13) = e22 ),
inference(component_clause,[status(thm)],[f306]) ).
fof(f315,definition,
( sQ23_spl
<=> h(e13) = e25 ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f316,plain,
( ~ sQ23_spl
| h(e13) = e25 ),
inference(component_clause,[status(thm)],[f315]) ).
fof(f319,definition,
( sQ24_spl
<=> h(e14) = e20 ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f320,plain,
( ~ sQ24_spl
| h(e14) = e20 ),
inference(component_clause,[status(thm)],[f319]) ).
fof(f322,definition,
( sQ25_spl
<=> h(e14) = e21 ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f323,plain,
( ~ sQ25_spl
| h(e14) = e21 ),
inference(component_clause,[status(thm)],[f322]) ).
fof(f325,definition,
( sQ26_spl
<=> h(e14) = e22 ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f326,plain,
( ~ sQ26_spl
| h(e14) = e22 ),
inference(component_clause,[status(thm)],[f325]) ).
fof(f328,definition,
( sQ27_spl
<=> h(e14) = e23 ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f329,plain,
( ~ sQ27_spl
| h(e14) = e23 ),
inference(component_clause,[status(thm)],[f328]) ).
fof(f331,definition,
( sQ28_spl
<=> h(e14) = e24 ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f332,plain,
( ~ sQ28_spl
| h(e14) = e24 ),
inference(component_clause,[status(thm)],[f331]) ).
fof(f334,definition,
( sQ29_spl
<=> h(e14) = e25 ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f335,plain,
( ~ sQ29_spl
| h(e14) = e25 ),
inference(component_clause,[status(thm)],[f334]) ).
fof(f337,plain,
( sQ29_spl
| sQ28_spl
| sQ27_spl
| sQ26_spl
| sQ25_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f151,f319,f322,f325,f328,f331,f334]) ).
fof(f338,definition,
( sQ30_spl
<=> h(e15) = e20 ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f339,plain,
( ~ sQ30_spl
| h(e15) = e20 ),
inference(component_clause,[status(thm)],[f338]) ).
fof(f341,definition,
( sQ31_spl
<=> h(e15) = e21 ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f342,plain,
( ~ sQ31_spl
| h(e15) = e21 ),
inference(component_clause,[status(thm)],[f341]) ).
fof(f344,definition,
( sQ32_spl
<=> h(e15) = e22 ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f345,plain,
( ~ sQ32_spl
| h(e15) = e22 ),
inference(component_clause,[status(thm)],[f344]) ).
fof(f347,definition,
( sQ33_spl
<=> h(e15) = e23 ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f348,plain,
( ~ sQ33_spl
| h(e15) = e23 ),
inference(component_clause,[status(thm)],[f347]) ).
fof(f350,definition,
( sQ34_spl
<=> h(e15) = e24 ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f351,plain,
( ~ sQ34_spl
| h(e15) = e24 ),
inference(component_clause,[status(thm)],[f350]) ).
fof(f353,definition,
( sQ35_spl
<=> h(e15) = e25 ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f354,plain,
( ~ sQ35_spl
| h(e15) = e25 ),
inference(component_clause,[status(thm)],[f353]) ).
fof(f356,plain,
( sQ35_spl
| sQ34_spl
| sQ33_spl
| sQ32_spl
| sQ31_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f152,f338,f341,f344,f347,f350,f353]) ).
fof(f357,definition,
( sQ36_spl
<=> j(e20) = e10 ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f358,plain,
( ~ sQ36_spl
| j(e20) = e10 ),
inference(component_clause,[status(thm)],[f357]) ).
fof(f360,definition,
( sQ37_spl
<=> j(e20) = e11 ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f361,plain,
( ~ sQ37_spl
| j(e20) = e11 ),
inference(component_clause,[status(thm)],[f360]) ).
fof(f363,definition,
( sQ38_spl
<=> j(e20) = e12 ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f364,plain,
( ~ sQ38_spl
| j(e20) = e12 ),
inference(component_clause,[status(thm)],[f363]) ).
fof(f365,plain,
( sQ38_spl
| j(e20) != e12 ),
inference(component_clause,[status(thm)],[f363]) ).
fof(f366,definition,
( sQ39_spl
<=> j(e20) = e13 ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f367,plain,
( ~ sQ39_spl
| j(e20) = e13 ),
inference(component_clause,[status(thm)],[f366]) ).
fof(f369,definition,
( sQ40_spl
<=> j(e20) = e14 ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f370,plain,
( ~ sQ40_spl
| j(e20) = e14 ),
inference(component_clause,[status(thm)],[f369]) ).
fof(f372,definition,
( sQ41_spl
<=> j(e20) = e15 ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f373,plain,
( ~ sQ41_spl
| j(e20) = e15 ),
inference(component_clause,[status(thm)],[f372]) ).
fof(f376,definition,
( sQ42_spl
<=> j(e21) = e10 ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f377,plain,
( ~ sQ42_spl
| j(e21) = e10 ),
inference(component_clause,[status(thm)],[f376]) ).
fof(f379,definition,
( sQ43_spl
<=> j(e21) = e11 ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f380,plain,
( ~ sQ43_spl
| j(e21) = e11 ),
inference(component_clause,[status(thm)],[f379]) ).
fof(f382,definition,
( sQ44_spl
<=> j(e21) = e12 ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f383,plain,
( ~ sQ44_spl
| j(e21) = e12 ),
inference(component_clause,[status(thm)],[f382]) ).
fof(f384,plain,
( sQ44_spl
| j(e21) != e12 ),
inference(component_clause,[status(thm)],[f382]) ).
fof(f388,definition,
( sQ46_spl
<=> j(e21) = e14 ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f389,plain,
( ~ sQ46_spl
| j(e21) = e14 ),
inference(component_clause,[status(thm)],[f388]) ).
fof(f395,definition,
( sQ48_spl
<=> j(e22) = e10 ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f396,plain,
( ~ sQ48_spl
| j(e22) = e10 ),
inference(component_clause,[status(thm)],[f395]) ).
fof(f398,definition,
( sQ49_spl
<=> j(e22) = e11 ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f399,plain,
( ~ sQ49_spl
| j(e22) = e11 ),
inference(component_clause,[status(thm)],[f398]) ).
fof(f401,definition,
( sQ50_spl
<=> j(e22) = e12 ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f402,plain,
( ~ sQ50_spl
| j(e22) = e12 ),
inference(component_clause,[status(thm)],[f401]) ).
fof(f404,definition,
( sQ51_spl
<=> j(e22) = e13 ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f405,plain,
( ~ sQ51_spl
| j(e22) = e13 ),
inference(component_clause,[status(thm)],[f404]) ).
fof(f407,definition,
( sQ52_spl
<=> j(e22) = e14 ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f408,plain,
( ~ sQ52_spl
| j(e22) = e14 ),
inference(component_clause,[status(thm)],[f407]) ).
fof(f410,definition,
( sQ53_spl
<=> j(e22) = e15 ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f411,plain,
( ~ sQ53_spl
| j(e22) = e15 ),
inference(component_clause,[status(thm)],[f410]) ).
fof(f413,plain,
( sQ53_spl
| sQ52_spl
| sQ51_spl
| sQ50_spl
| sQ49_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f155,f395,f398,f401,f404,f407,f410]) ).
fof(f414,definition,
( sQ54_spl
<=> j(e23) = e10 ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f415,plain,
( ~ sQ54_spl
| j(e23) = e10 ),
inference(component_clause,[status(thm)],[f414]) ).
fof(f416,plain,
( sQ54_spl
| j(e23) != e10 ),
inference(component_clause,[status(thm)],[f414]) ).
fof(f417,definition,
( sQ55_spl
<=> j(e23) = e11 ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f418,plain,
( ~ sQ55_spl
| j(e23) = e11 ),
inference(component_clause,[status(thm)],[f417]) ).
fof(f419,plain,
( sQ55_spl
| j(e23) != e11 ),
inference(component_clause,[status(thm)],[f417]) ).
fof(f420,definition,
( sQ56_spl
<=> j(e23) = e12 ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f421,plain,
( ~ sQ56_spl
| j(e23) = e12 ),
inference(component_clause,[status(thm)],[f420]) ).
fof(f422,plain,
( sQ56_spl
| j(e23) != e12 ),
inference(component_clause,[status(thm)],[f420]) ).
fof(f426,definition,
( sQ58_spl
<=> j(e23) = e14 ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f427,plain,
( ~ sQ58_spl
| j(e23) = e14 ),
inference(component_clause,[status(thm)],[f426]) ).
fof(f429,definition,
( sQ59_spl
<=> j(e23) = e15 ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f430,plain,
( ~ sQ59_spl
| j(e23) = e15 ),
inference(component_clause,[status(thm)],[f429]) ).
fof(f433,definition,
( sQ60_spl
<=> j(e24) = e10 ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f434,plain,
( ~ sQ60_spl
| j(e24) = e10 ),
inference(component_clause,[status(thm)],[f433]) ).
fof(f435,plain,
( sQ60_spl
| j(e24) != e10 ),
inference(component_clause,[status(thm)],[f433]) ).
fof(f439,definition,
( sQ62_spl
<=> j(e24) = e12 ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f440,plain,
( ~ sQ62_spl
| j(e24) = e12 ),
inference(component_clause,[status(thm)],[f439]) ).
fof(f445,definition,
( sQ64_spl
<=> j(e24) = e14 ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f446,plain,
( ~ sQ64_spl
| j(e24) = e14 ),
inference(component_clause,[status(thm)],[f445]) ).
fof(f448,definition,
( sQ65_spl
<=> j(e24) = e15 ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f449,plain,
( ~ sQ65_spl
| j(e24) = e15 ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f455,definition,
( sQ67_spl
<=> j(e25) = e11 ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f456,plain,
( ~ sQ67_spl
| j(e25) = e11 ),
inference(component_clause,[status(thm)],[f455]) ).
fof(f461,definition,
( sQ69_spl
<=> j(e25) = e13 ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f462,plain,
( ~ sQ69_spl
| j(e25) = e13 ),
inference(component_clause,[status(thm)],[f461]) ).
fof(f464,definition,
( sQ70_spl
<=> j(e25) = e14 ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f465,plain,
( ~ sQ70_spl
| j(e25) = e14 ),
inference(component_clause,[status(thm)],[f464]) ).
fof(f500,plain,
h(e10) = op2(h(e10),h(e10)),
inference(backward_demodulation,[status(thm)],[f74,f159]) ).
fof(f508,plain,
( ~ sQ58_spl
| ~ sQ59_spl
| e15 = e14 ),
inference(forward_demodulation,[status(thm)],[f430,f427]) ).
fof(f509,plain,
( ~ sQ58_spl
| ~ sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f508,f22]) ).
fof(f510,plain,
( ~ sQ58_spl
| ~ sQ59_spl ),
inference(contradiction_clause,[status(thm)],[f509]) ).
fof(f525,plain,
( ~ sQ48_spl
| ~ sQ49_spl
| e11 = e10 ),
inference(forward_demodulation,[status(thm)],[f399,f396]) ).
fof(f526,plain,
( ~ sQ48_spl
| ~ sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f525,f8]) ).
fof(f527,plain,
( ~ sQ48_spl
| ~ sQ49_spl ),
inference(contradiction_clause,[status(thm)],[f526]) ).
fof(f537,plain,
h(e10) = op2(h(e11),h(e11)),
inference(forward_demodulation,[status(thm)],[f81,f166]) ).
fof(f544,plain,
( ~ sQ36_spl
| ~ sQ37_spl
| e11 = e10 ),
inference(forward_demodulation,[status(thm)],[f361,f358]) ).
fof(f545,plain,
( ~ sQ36_spl
| ~ sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f544,f8]) ).
fof(f546,plain,
( ~ sQ36_spl
| ~ sQ37_spl ),
inference(contradiction_clause,[status(thm)],[f545]) ).
fof(f576,plain,
h(e15) = op2(h(e11),h(e13)),
inference(forward_demodulation,[status(thm)],[f83,f168]) ).
fof(f587,plain,
( ~ sQ11_spl
| h(e10) = op2(h(e11),e25) ),
inference(backward_demodulation,[status(thm)],[f278,f537]) ).
fof(f589,plain,
( ~ sQ11_spl
| h(e10) = op2(e25,e25) ),
inference(forward_demodulation,[status(thm)],[f278,f587]) ).
fof(f604,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| e23 = e22 ),
inference(forward_demodulation,[status(thm)],[f253,f250]) ).
fof(f605,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f604,f32]) ).
fof(f606,plain,
( ~ sQ2_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f605]) ).
fof(f620,plain,
( ~ sQ56_spl
| ~ sQ58_spl
| e14 = e12 ),
inference(forward_demodulation,[status(thm)],[f427,f421]) ).
fof(f621,plain,
( ~ sQ56_spl
| ~ sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f620,f18]) ).
fof(f622,plain,
( ~ sQ56_spl
| ~ sQ58_spl ),
inference(contradiction_clause,[status(thm)],[f621]) ).
fof(f658,plain,
h(e13) = op2(h(e12),h(e12)),
inference(forward_demodulation,[status(thm)],[f88,f173]) ).
fof(f683,plain,
( ~ sQ0_spl
| ~ sQ2_spl
| e22 = e20 ),
inference(forward_demodulation,[status(thm)],[f250,f244]) ).
fof(f684,plain,
( ~ sQ0_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f683,f24]) ).
fof(f685,plain,
( ~ sQ0_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f684]) ).
fof(f769,plain,
h(e12) = op2(h(e13),h(e13)),
inference(forward_demodulation,[status(thm)],[f95,f180]) ).
fof(f771,plain,
h(e11) = op2(h(e13),h(e14)),
inference(forward_demodulation,[status(thm)],[f96,f181]) ).
fof(f800,plain,
( ~ sQ55_spl
| ~ sQ59_spl
| e15 = e11 ),
inference(forward_demodulation,[status(thm)],[f430,f418]) ).
fof(f801,plain,
( ~ sQ55_spl
| ~ sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f800,f16]) ).
fof(f802,plain,
( ~ sQ55_spl
| ~ sQ59_spl ),
inference(contradiction_clause,[status(thm)],[f801]) ).
fof(f804,plain,
h(e11) = op2(h(e14),h(e13)),
inference(forward_demodulation,[status(thm)],[f101,f186]) ).
fof(f805,plain,
h(e13) = op2(h(e14),h(e14)),
inference(forward_demodulation,[status(thm)],[f102,f187]) ).
fof(f845,plain,
h(e12) = op2(h(e15),h(e15)),
inference(forward_demodulation,[status(thm)],[f109,f194]) ).
fof(f852,plain,
j(e20) = op1(j(e20),j(e20)),
inference(forward_demodulation,[status(thm)],[f110,f195]) ).
fof(f853,plain,
j(e21) = op1(j(e20),j(e21)),
inference(forward_demodulation,[status(thm)],[f111,f196]) ).
fof(f858,plain,
( ~ sQ25_spl
| h(e13) = op2(h(e14),e21) ),
inference(backward_demodulation,[status(thm)],[f323,f805]) ).
fof(f859,plain,
( ~ sQ25_spl
| h(e11) = op2(e21,h(e13)) ),
inference(backward_demodulation,[status(thm)],[f323,f804]) ).
fof(f860,plain,
( ~ sQ25_spl
| h(e13) = op2(e21,e21) ),
inference(forward_demodulation,[status(thm)],[f323,f858]) ).
fof(f861,plain,
( ~ sQ25_spl
| h(e13) = e20 ),
inference(forward_demodulation,[status(thm)],[f117,f860]) ).
fof(f868,plain,
j(e20) = op1(j(e21),j(e21)),
inference(forward_demodulation,[status(thm)],[f117,f202]) ).
fof(f872,plain,
j(e23) = op1(j(e21),j(e22)),
inference(forward_demodulation,[status(thm)],[f118,f203]) ).
fof(f885,plain,
j(e20) = op1(j(e22),j(e22)),
inference(forward_demodulation,[status(thm)],[f124,f209]) ).
fof(f899,plain,
j(e21) = op1(j(e22),j(e24)),
inference(forward_demodulation,[status(thm)],[f126,f211]) ).
fof(f909,plain,
j(e23) = op1(j(e22),j(e25)),
inference(forward_demodulation,[status(thm)],[f127,f212]) ).
fof(f926,plain,
( ~ sQ56_spl
| e12 = op1(j(e21),j(e22)) ),
inference(backward_demodulation,[status(thm)],[f421,f872]) ).
fof(f930,plain,
j(e24) = op1(j(e23),j(e23)),
inference(forward_demodulation,[status(thm)],[f131,f216]) ).
fof(f931,plain,
( ~ sQ64_spl
| e14 = op1(j(e23),j(e23)) ),
inference(forward_demodulation,[status(thm)],[f446,f930]) ).
fof(f932,plain,
( ~ sQ64_spl
| ~ sQ56_spl
| e14 = op1(e12,j(e23)) ),
inference(forward_demodulation,[status(thm)],[f421,f931]) ).
fof(f933,plain,
( ~ sQ64_spl
| ~ sQ56_spl
| e14 = op1(e12,e12) ),
inference(forward_demodulation,[status(thm)],[f421,f932]) ).
fof(f934,plain,
( ~ sQ64_spl
| ~ sQ56_spl
| e14 = e13 ),
inference(forward_demodulation,[status(thm)],[f88,f933]) ).
fof(f935,plain,
( ~ sQ64_spl
| ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f934,f20]) ).
fof(f936,plain,
( ~ sQ64_spl
| ~ sQ56_spl ),
inference(contradiction_clause,[status(thm)],[f935]) ).
fof(f937,plain,
j(e20) = op1(j(e23),j(e24)),
inference(forward_demodulation,[status(thm)],[f132,f217]) ).
fof(f943,plain,
( ~ sQ50_spl
| j(e20) = op1(j(e22),e12) ),
inference(backward_demodulation,[status(thm)],[f402,f885]) ).
fof(f946,plain,
( ~ sQ50_spl
| j(e20) = op1(e12,e12) ),
inference(forward_demodulation,[status(thm)],[f402,f943]) ).
fof(f947,plain,
( ~ sQ50_spl
| j(e20) = e13 ),
inference(forward_demodulation,[status(thm)],[f88,f946]) ).
fof(f953,plain,
j(e24) = op1(j(e24),j(e20)),
inference(forward_demodulation,[status(thm)],[f134,f219]) ).
fof(f972,plain,
j(e23) = op1(j(e24),j(e24)),
inference(forward_demodulation,[status(thm)],[f138,f223]) ).
fof(f981,plain,
( ~ sQ38_spl
| j(e20) = op1(j(e20),e12) ),
inference(backward_demodulation,[status(thm)],[f364,f852]) ).
fof(f982,plain,
( ~ sQ38_spl
| e12 = op1(j(e20),e12) ),
inference(forward_demodulation,[status(thm)],[f364,f981]) ).
fof(f983,plain,
( ~ sQ38_spl
| e12 = op1(e12,e12) ),
inference(forward_demodulation,[status(thm)],[f364,f982]) ).
fof(f984,plain,
( ~ sQ38_spl
| e12 = e13 ),
inference(forward_demodulation,[status(thm)],[f88,f983]) ).
fof(f985,plain,
( ~ sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f984,f17]) ).
fof(f986,plain,
~ sQ38_spl,
inference(contradiction_clause,[status(thm)],[f985]) ).
fof(f1012,plain,
j(e20) = op1(j(e25),j(e25)),
inference(forward_demodulation,[status(thm)],[f145,f230]) ).
fof(f1022,plain,
( ~ sQ9_spl
| j(e23) = e11 ),
inference(forward_demodulation,[status(thm)],[f272,f238]) ).
fof(f1023,plain,
( ~ sQ9_spl
| sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1022,f419]) ).
fof(f1024,plain,
( ~ sQ9_spl
| sQ55_spl ),
inference(contradiction_clause,[status(thm)],[f1023]) ).
fof(f1045,plain,
( ~ sQ62_spl
| j(e23) = op1(j(e24),e12) ),
inference(backward_demodulation,[status(thm)],[f440,f972]) ).
fof(f1047,plain,
( ~ sQ62_spl
| j(e23) = op1(e12,e12) ),
inference(forward_demodulation,[status(thm)],[f440,f1045]) ).
fof(f1048,plain,
( ~ sQ62_spl
| j(e23) = e13 ),
inference(forward_demodulation,[status(thm)],[f88,f1047]) ).
fof(f1057,plain,
( ~ sQ27_spl
| j(e23) = e14 ),
inference(forward_demodulation,[status(thm)],[f329,f241]) ).
fof(f1075,plain,
( ~ sQ51_spl
| h(e13) = e22 ),
inference(backward_demodulation,[status(thm)],[f405,f233]) ).
fof(f1083,plain,
( ~ sQ67_spl
| h(e11) = e25 ),
inference(backward_demodulation,[status(thm)],[f456,f236]) ).
fof(f1084,plain,
( ~ sQ67_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f1083,f277,f455]) ).
fof(f1104,plain,
( ~ sQ7_spl
| h(e15) = op2(e21,h(e13)) ),
inference(backward_demodulation,[status(thm)],[f266,f576]) ).
fof(f1115,plain,
( ~ sQ33_spl
| j(e23) = e15 ),
inference(backward_demodulation,[status(thm)],[f348,f242]) ).
fof(f1117,plain,
( ~ sQ33_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1115,f429,f347]) ).
fof(f1118,plain,
( ~ sQ13_spl
| h(e13) = op2(h(e12),e21) ),
inference(backward_demodulation,[status(thm)],[f285,f658]) ).
fof(f1125,plain,
( ~ sQ13_spl
| h(e13) = op2(e21,e21) ),
inference(forward_demodulation,[status(thm)],[f285,f1118]) ).
fof(f1126,plain,
( ~ sQ13_spl
| h(e13) = e20 ),
inference(forward_demodulation,[status(thm)],[f117,f1125]) ).
fof(f1155,plain,
( ~ sQ20_spl
| h(e12) = op2(e22,h(e13)) ),
inference(forward_demodulation,[status(thm)],[f307,f769]) ).
fof(f1156,plain,
( ~ sQ20_spl
| h(e12) = op2(e22,e22) ),
inference(forward_demodulation,[status(thm)],[f307,f1155]) ).
fof(f1162,plain,
( ~ sQ20_spl
| h(e12) = e20 ),
inference(forward_demodulation,[status(thm)],[f124,f1156]) ).
fof(f1166,plain,
( ~ sQ51_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1075,f306,f404]) ).
fof(f1181,plain,
( ~ sQ24_spl
| h(e13) = op2(h(e14),e20) ),
inference(backward_demodulation,[status(thm)],[f320,f805]) ).
fof(f1188,plain,
( ~ sQ24_spl
| h(e13) = op2(e20,e20) ),
inference(forward_demodulation,[status(thm)],[f320,f1181]) ).
fof(f1189,plain,
( ~ sQ24_spl
| h(e13) = e20 ),
inference(forward_demodulation,[status(thm)],[f110,f1188]) ).
fof(f1225,plain,
( ~ sQ42_spl
| j(e20) = op1(e10,j(e21)) ),
inference(forward_demodulation,[status(thm)],[f377,f868]) ).
fof(f1226,plain,
( ~ sQ42_spl
| j(e20) = op1(e10,e10) ),
inference(forward_demodulation,[status(thm)],[f377,f1225]) ).
fof(f1228,plain,
( ~ sQ42_spl
| j(e20) = e10 ),
inference(forward_demodulation,[status(thm)],[f74,f1226]) ).
fof(f1265,plain,
( ~ sQ54_spl
| j(e24) = op1(e10,j(e23)) ),
inference(forward_demodulation,[status(thm)],[f415,f930]) ).
fof(f1266,plain,
( ~ sQ54_spl
| j(e24) = op1(e10,e10) ),
inference(forward_demodulation,[status(thm)],[f415,f1265]) ).
fof(f1267,plain,
( ~ sQ54_spl
| j(e24) = e10 ),
inference(forward_demodulation,[status(thm)],[f74,f1266]) ).
fof(f1315,plain,
( ~ sQ6_spl
| j(e20) = op1(j(e20),e11) ),
inference(backward_demodulation,[status(thm)],[f1316,f852]) ).
fof(f1316,plain,
( ~ sQ6_spl
| j(e20) = e11 ),
inference(forward_demodulation,[status(thm)],[f263,f238]) ).
fof(f1317,plain,
( ~ sQ6_spl
| e11 = op1(j(e20),e11) ),
inference(forward_demodulation,[status(thm)],[f1316,f1315]) ).
fof(f1318,plain,
( ~ sQ6_spl
| e11 = op1(e11,e11) ),
inference(forward_demodulation,[status(thm)],[f1316,f1317]) ).
fof(f1319,plain,
( ~ sQ6_spl
| e11 = e10 ),
inference(forward_demodulation,[status(thm)],[f81,f1318]) ).
fof(f1320,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1319,f8]) ).
fof(f1321,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f1320]) ).
fof(f1322,plain,
( ~ sQ24_spl
| h(e11) = op2(e20,h(e13)) ),
inference(forward_demodulation,[status(thm)],[f320,f804]) ).
fof(f1323,plain,
( ~ sQ24_spl
| h(e11) = op2(e20,e20) ),
inference(forward_demodulation,[status(thm)],[f1189,f1322]) ).
fof(f1324,plain,
( ~ sQ24_spl
| h(e11) = e20 ),
inference(forward_demodulation,[status(thm)],[f110,f1323]) ).
fof(f1353,plain,
( ~ sQ54_spl
| h(e10) = e24 ),
inference(forward_demodulation,[status(thm)],[f1267,f235]) ).
fof(f1368,plain,
( ~ sQ43_spl
| h(e11) = e21 ),
inference(forward_demodulation,[status(thm)],[f380,f232]) ).
fof(f1397,plain,
( ~ sQ54_spl
| e24 = op2(h(e10),h(e10)) ),
inference(forward_demodulation,[status(thm)],[f1353,f500]) ).
fof(f1398,plain,
( ~ sQ54_spl
| e24 = op2(e24,h(e10)) ),
inference(forward_demodulation,[status(thm)],[f1353,f1397]) ).
fof(f1399,plain,
( ~ sQ54_spl
| e24 = op2(e24,e24) ),
inference(forward_demodulation,[status(thm)],[f1353,f1398]) ).
fof(f1400,plain,
( ~ sQ54_spl
| e24 = e23 ),
inference(forward_demodulation,[status(thm)],[f138,f1399]) ).
fof(f1401,plain,
( ~ sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1400,f35]) ).
fof(f1402,plain,
~ sQ54_spl,
inference(contradiction_clause,[status(thm)],[f1401]) ).
fof(f1403,plain,
( ~ sQ43_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f1368,f265,f379]) ).
fof(f1427,plain,
( ~ sQ24_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1324,f262,f319]) ).
fof(f1428,plain,
( ~ sQ25_spl
| ~ sQ18_spl
| h(e11) = op2(e21,e20) ),
inference(forward_demodulation,[status(thm)],[f301,f859]) ).
fof(f1429,plain,
( ~ sQ25_spl
| ~ sQ18_spl
| h(e11) = e21 ),
inference(forward_demodulation,[status(thm)],[f116,f1428]) ).
fof(f1448,plain,
( ~ sQ8_spl
| h(e10) = op2(e22,h(e11)) ),
inference(forward_demodulation,[status(thm)],[f269,f537]) ).
fof(f1449,plain,
( ~ sQ8_spl
| h(e10) = op2(e22,e22) ),
inference(forward_demodulation,[status(thm)],[f269,f1448]) ).
fof(f1451,plain,
( ~ sQ8_spl
| h(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f124,f1449]) ).
fof(f1458,plain,
( ~ sQ7_spl
| ~ sQ18_spl
| h(e15) = op2(e21,e20) ),
inference(forward_demodulation,[status(thm)],[f301,f1104]) ).
fof(f1459,plain,
( ~ sQ7_spl
| ~ sQ18_spl
| h(e15) = e21 ),
inference(forward_demodulation,[status(thm)],[f116,f1458]) ).
fof(f1478,plain,
( ~ sQ25_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f861,f300,f322]) ).
fof(f1479,plain,
( ~ sQ20_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f1162,f281,f306]) ).
fof(f1481,plain,
( ~ sQ25_spl
| ~ sQ18_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f1429,f265,f300,f322]) ).
fof(f1491,plain,
( ~ sQ69_spl
| j(e20) = op1(j(e25),e13) ),
inference(backward_demodulation,[status(thm)],[f462,f1012]) ).
fof(f1494,plain,
( ~ sQ69_spl
| j(e20) = op1(e13,e13) ),
inference(forward_demodulation,[status(thm)],[f462,f1491]) ).
fof(f1495,plain,
( ~ sQ69_spl
| j(e20) = e12 ),
inference(forward_demodulation,[status(thm)],[f95,f1494]) ).
fof(f1496,plain,
( ~ sQ69_spl
| sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1495,f365]) ).
fof(f1497,plain,
( ~ sQ69_spl
| sQ38_spl ),
inference(contradiction_clause,[status(thm)],[f1496]) ).
fof(f1513,plain,
( ~ sQ55_spl
| h(e11) = e23 ),
inference(backward_demodulation,[status(thm)],[f418,f234]) ).
fof(f1514,plain,
( ~ sQ55_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f1513,f271,f417]) ).
fof(f1519,plain,
( ~ sQ42_spl
| h(e10) = e20 ),
inference(backward_demodulation,[status(thm)],[f1228,f231]) ).
fof(f1528,plain,
( ~ sQ48_spl
| h(e10) = e22 ),
inference(forward_demodulation,[status(thm)],[f396,f233]) ).
fof(f1540,plain,
( ~ sQ32_spl
| h(e12) = op2(h(e15),e22) ),
inference(backward_demodulation,[status(thm)],[f345,f845]) ).
fof(f1544,plain,
( ~ sQ32_spl
| h(e12) = op2(e22,e22) ),
inference(forward_demodulation,[status(thm)],[f345,f1540]) ).
fof(f1545,plain,
( ~ sQ32_spl
| h(e12) = e20 ),
inference(forward_demodulation,[status(thm)],[f124,f1544]) ).
fof(f1552,plain,
( ~ sQ50_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f947,f366,f401]) ).
fof(f1560,plain,
( ~ sQ48_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1528,f249,f395]) ).
fof(f1567,plain,
( ~ sQ26_spl
| j(e22) = e14 ),
inference(backward_demodulation,[status(thm)],[f326,f241]) ).
fof(f1568,plain,
( ~ sQ26_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f1567,f407,f325]) ).
fof(f1573,plain,
( ~ sQ12_spl
| j(e20) = e12 ),
inference(backward_demodulation,[status(thm)],[f282,f239]) ).
fof(f1574,plain,
( ~ sQ12_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f1573,f363,f281]) ).
fof(f1609,plain,
( ~ sQ27_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f1057,f426,f328]) ).
fof(f1614,plain,
( ~ sQ13_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1126,f300,f284]) ).
fof(f1617,plain,
( ~ sQ49_spl
| j(e20) = op1(j(e22),e11) ),
inference(backward_demodulation,[status(thm)],[f399,f885]) ).
fof(f1622,plain,
( ~ sQ49_spl
| j(e21) = op1(e11,j(e24)) ),
inference(backward_demodulation,[status(thm)],[f399,f899]) ).
fof(f1624,plain,
( ~ sQ49_spl
| j(e20) = op1(e11,e11) ),
inference(forward_demodulation,[status(thm)],[f399,f1617]) ).
fof(f1625,plain,
( ~ sQ49_spl
| j(e20) = e10 ),
inference(forward_demodulation,[status(thm)],[f81,f1624]) ).
fof(f1646,plain,
( ~ sQ4_spl
| e24 = op2(h(e10),h(e10)) ),
inference(forward_demodulation,[status(thm)],[f256,f500]) ).
fof(f1647,plain,
( ~ sQ4_spl
| e24 = op2(e24,h(e10)) ),
inference(forward_demodulation,[status(thm)],[f256,f1646]) ).
fof(f1648,plain,
( ~ sQ4_spl
| e24 = op2(e24,e24) ),
inference(forward_demodulation,[status(thm)],[f256,f1647]) ).
fof(f1649,plain,
( ~ sQ4_spl
| e24 = e23 ),
inference(forward_demodulation,[status(thm)],[f138,f1648]) ).
fof(f1650,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1649,f35]) ).
fof(f1651,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f1650]) ).
fof(f1652,plain,
( ~ sQ41_spl
| j(e20) = op1(j(e20),e15) ),
inference(backward_demodulation,[status(thm)],[f373,f852]) ).
fof(f1661,plain,
( ~ sQ41_spl
| e15 = op1(j(e20),e15) ),
inference(forward_demodulation,[status(thm)],[f373,f1652]) ).
fof(f1662,plain,
( ~ sQ41_spl
| e15 = op1(e15,e15) ),
inference(forward_demodulation,[status(thm)],[f373,f1661]) ).
fof(f1663,plain,
( ~ sQ41_spl
| e15 = e12 ),
inference(forward_demodulation,[status(thm)],[f109,f1662]) ).
fof(f1664,plain,
( ~ sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1663,f19]) ).
fof(f1665,plain,
~ sQ41_spl,
inference(contradiction_clause,[status(thm)],[f1664]) ).
fof(f1673,plain,
( ~ sQ65_spl
| j(e23) = op1(e15,j(e24)) ),
inference(forward_demodulation,[status(thm)],[f449,f972]) ).
fof(f1674,plain,
( ~ sQ65_spl
| j(e23) = op1(e15,e15) ),
inference(forward_demodulation,[status(thm)],[f449,f1673]) ).
fof(f1675,plain,
( ~ sQ65_spl
| j(e23) = e12 ),
inference(forward_demodulation,[status(thm)],[f109,f1674]) ).
fof(f1680,plain,
( ~ sQ65_spl
| e15 = op1(j(e24),j(e20)) ),
inference(forward_demodulation,[status(thm)],[f449,f953]) ).
fof(f1681,plain,
( ~ sQ65_spl
| e15 = op1(e15,j(e20)) ),
inference(forward_demodulation,[status(thm)],[f449,f1680]) ).
fof(f1709,plain,
( ~ sQ65_spl
| j(e20) = op1(e12,j(e24)) ),
inference(forward_demodulation,[status(thm)],[f1675,f937]) ).
fof(f1710,plain,
( ~ sQ65_spl
| j(e20) = op1(e12,e15) ),
inference(forward_demodulation,[status(thm)],[f449,f1709]) ).
fof(f1711,plain,
( ~ sQ65_spl
| e15 = op1(e15,e11) ),
inference(backward_demodulation,[status(thm)],[f1712,f1681]) ).
fof(f1712,plain,
( ~ sQ65_spl
| j(e20) = e11 ),
inference(forward_demodulation,[status(thm)],[f91,f1710]) ).
fof(f1713,plain,
( ~ sQ65_spl
| e15 = e13 ),
inference(forward_demodulation,[status(thm)],[f105,f1711]) ).
fof(f1714,plain,
( ~ sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1713,f21]) ).
fof(f1715,plain,
~ sQ65_spl,
inference(contradiction_clause,[status(thm)],[f1714]) ).
fof(f1717,plain,
( ~ sQ44_spl
| h(e12) = e21 ),
inference(backward_demodulation,[status(thm)],[f383,f232]) ).
fof(f1721,plain,
( ~ sQ44_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f1717,f284,f382]) ).
fof(f1727,plain,
( ~ sQ28_spl
| h(e13) = op2(h(e14),e24) ),
inference(backward_demodulation,[status(thm)],[f332,f805]) ).
fof(f1728,plain,
( ~ sQ28_spl
| h(e13) = op2(e24,e24) ),
inference(forward_demodulation,[status(thm)],[f332,f1727]) ).
fof(f1729,plain,
( ~ sQ28_spl
| h(e13) = e23 ),
inference(forward_demodulation,[status(thm)],[f138,f1728]) ).
fof(f1805,plain,
( ~ sQ34_spl
| h(e12) = op2(e24,h(e15)) ),
inference(forward_demodulation,[status(thm)],[f351,f845]) ).
fof(f1806,plain,
( ~ sQ34_spl
| h(e12) = op2(e24,e24) ),
inference(forward_demodulation,[status(thm)],[f351,f1805]) ).
fof(f1807,plain,
( ~ sQ34_spl
| h(e12) = e23 ),
inference(forward_demodulation,[status(thm)],[f138,f1806]) ).
fof(f1808,plain,
( ~ sQ34_spl
| sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1807,f292]) ).
fof(f1809,plain,
( ~ sQ34_spl
| sQ15_spl ),
inference(contradiction_clause,[status(thm)],[f1808]) ).
fof(f1815,plain,
( ~ sQ42_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1519,f243,f376]) ).
fof(f1816,plain,
( ~ sQ8_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1451,f243,f268]) ).
fof(f1827,plain,
( ~ sQ70_spl
| j(e20) = op1(j(e25),e14) ),
inference(backward_demodulation,[status(thm)],[f465,f1012]) ).
fof(f1838,plain,
( ~ sQ70_spl
| j(e20) = op1(e14,e14) ),
inference(forward_demodulation,[status(thm)],[f465,f1827]) ).
fof(f1839,plain,
( ~ sQ70_spl
| j(e20) = e13 ),
inference(forward_demodulation,[status(thm)],[f102,f1838]) ).
fof(f1841,plain,
( ~ sQ7_spl
| ~ sQ18_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f1459,f341,f300,f265]) ).
fof(f1842,plain,
( ~ sQ40_spl
| h(e14) = e20 ),
inference(backward_demodulation,[status(thm)],[f370,f231]) ).
fof(f1846,plain,
( ~ sQ40_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f1842,f319,f369]) ).
fof(f1881,plain,
( ~ sQ15_spl
| j(e23) = e12 ),
inference(forward_demodulation,[status(thm)],[f291,f239]) ).
fof(f1882,plain,
( ~ sQ15_spl
| sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1881,f422]) ).
fof(f1883,plain,
( ~ sQ15_spl
| sQ56_spl ),
inference(contradiction_clause,[status(thm)],[f1882]) ).
fof(f1912,plain,
( ~ sQ1_spl
| ~ sQ2_spl
| e22 = e21 ),
inference(forward_demodulation,[status(thm)],[f250,f247]) ).
fof(f1913,plain,
( ~ sQ1_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1912,f28]) ).
fof(f1914,plain,
( ~ sQ1_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1913]) ).
fof(f1915,plain,
( ~ sQ32_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f1545,f281,f344]) ).
fof(f1917,plain,
( ~ sQ11_spl
| h(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f145,f589]) ).
fof(f1950,plain,
( ~ sQ11_spl
| j(e25) = e11 ),
inference(backward_demodulation,[status(thm)],[f278,f238]) ).
fof(f1961,plain,
( ~ sQ46_spl
| e14 = op1(j(e20),j(e21)) ),
inference(forward_demodulation,[status(thm)],[f389,f853]) ).
fof(f1962,plain,
( ~ sQ46_spl
| e14 = op1(j(e20),e14) ),
inference(forward_demodulation,[status(thm)],[f389,f1961]) ).
fof(f1965,plain,
( ~ sQ46_spl
| j(e20) = op1(e14,j(e21)) ),
inference(forward_demodulation,[status(thm)],[f389,f868]) ).
fof(f1966,plain,
( ~ sQ46_spl
| j(e20) = op1(e14,e14) ),
inference(forward_demodulation,[status(thm)],[f389,f1965]) ).
fof(f1968,plain,
( ~ sQ46_spl
| e14 = op1(e13,e14) ),
inference(backward_demodulation,[status(thm)],[f1975,f1962]) ).
fof(f1975,plain,
( ~ sQ46_spl
| j(e20) = e13 ),
inference(forward_demodulation,[status(thm)],[f102,f1966]) ).
fof(f2023,plain,
( ~ sQ60_spl
| j(e23) = op1(e10,j(e24)) ),
inference(forward_demodulation,[status(thm)],[f434,f972]) ).
fof(f2024,plain,
( ~ sQ60_spl
| j(e23) = op1(e10,e10) ),
inference(forward_demodulation,[status(thm)],[f434,f2023]) ).
fof(f2026,plain,
( ~ sQ60_spl
| j(e23) = e10 ),
inference(forward_demodulation,[status(thm)],[f74,f2024]) ).
fof(f2029,plain,
( sQ54_spl
| ~ sQ60_spl
| e10 != e10 ),
inference(forward_demodulation,[status(thm)],[f2026,f416]) ).
fof(f2030,plain,
( sQ54_spl
| ~ sQ60_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2029]) ).
fof(f2031,plain,
( sQ54_spl
| ~ sQ60_spl ),
inference(contradiction_clause,[status(thm)],[f2030]) ).
fof(f2101,plain,
( ~ sQ31_spl
| h(e12) = op2(e21,h(e15)) ),
inference(forward_demodulation,[status(thm)],[f342,f845]) ).
fof(f2102,plain,
( ~ sQ31_spl
| h(e12) = op2(e21,e21) ),
inference(forward_demodulation,[status(thm)],[f342,f2101]) ).
fof(f2103,plain,
( ~ sQ31_spl
| h(e12) = e20 ),
inference(forward_demodulation,[status(thm)],[f117,f2102]) ).
fof(f2127,plain,
( ~ sQ11_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1917,f243,f277]) ).
fof(f2150,plain,
( ~ sQ7_spl
| h(e10) = op2(h(e11),e21) ),
inference(backward_demodulation,[status(thm)],[f266,f537]) ).
fof(f2153,plain,
( ~ sQ7_spl
| h(e10) = op2(e21,e21) ),
inference(forward_demodulation,[status(thm)],[f266,f2150]) ).
fof(f2154,plain,
( ~ sQ7_spl
| h(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f117,f2153]) ).
fof(f2159,plain,
( sQ12_spl
| ~ sQ31_spl
| e20 != e20 ),
inference(forward_demodulation,[status(thm)],[f2103,f283]) ).
fof(f2160,plain,
( sQ12_spl
| ~ sQ31_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2159]) ).
fof(f2161,plain,
( sQ12_spl
| ~ sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f2160]) ).
fof(f2162,plain,
( ~ sQ46_spl
| e14 = e11 ),
inference(forward_demodulation,[status(thm)],[f96,f1968]) ).
fof(f2163,plain,
( ~ sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2162,f15]) ).
fof(f2164,plain,
~ sQ46_spl,
inference(contradiction_clause,[status(thm)],[f2163]) ).
fof(f2172,plain,
( ~ sQ52_spl
| j(e20) = op1(j(e22),e14) ),
inference(backward_demodulation,[status(thm)],[f408,f885]) ).
fof(f2177,plain,
( ~ sQ52_spl
| j(e20) = op1(e14,e14) ),
inference(forward_demodulation,[status(thm)],[f408,f2172]) ).
fof(f2178,plain,
( ~ sQ52_spl
| j(e20) = e13 ),
inference(forward_demodulation,[status(thm)],[f102,f2177]) ).
fof(f2235,plain,
( ~ sQ7_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f2154,f243,f265]) ).
fof(f2243,plain,
( ~ sQ14_spl
| j(e22) = e12 ),
inference(backward_demodulation,[status(thm)],[f288,f239]) ).
fof(f2245,plain,
( ~ sQ14_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f2243,f401,f287]) ).
fof(f2343,plain,
( ~ sQ70_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f1839,f366,f464]) ).
fof(f2344,plain,
( ~ sQ56_spl
| e12 = j(e23) ),
inference(forward_demodulation,[status(thm)],[f872,f926]) ).
fof(f2410,plain,
( ~ sQ59_spl
| ~ sQ56_spl
| e12 = e15 ),
inference(forward_demodulation,[status(thm)],[f2344,f430]) ).
fof(f2411,plain,
( ~ sQ59_spl
| ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2410,f19]) ).
fof(f2412,plain,
( ~ sQ59_spl
| ~ sQ56_spl ),
inference(contradiction_clause,[status(thm)],[f2411]) ).
fof(f2438,plain,
( ~ sQ49_spl
| j(e23) = op1(e11,j(e25)) ),
inference(forward_demodulation,[status(thm)],[f399,f909]) ).
fof(f2439,plain,
( ~ sQ49_spl
| ~ sQ11_spl
| j(e23) = op1(e11,e11) ),
inference(forward_demodulation,[status(thm)],[f1950,f2438]) ).
fof(f2440,plain,
( ~ sQ49_spl
| ~ sQ11_spl
| j(e24) = op1(j(e23),e10) ),
inference(backward_demodulation,[status(thm)],[f2443,f930]) ).
fof(f2443,plain,
( ~ sQ49_spl
| ~ sQ11_spl
| j(e23) = e10 ),
inference(forward_demodulation,[status(thm)],[f81,f2439]) ).
fof(f2444,plain,
( ~ sQ49_spl
| ~ sQ11_spl
| j(e24) = op1(e10,e10) ),
inference(forward_demodulation,[status(thm)],[f2443,f2440]) ).
fof(f2445,plain,
( ~ sQ49_spl
| ~ sQ11_spl
| j(e24) = e10 ),
inference(forward_demodulation,[status(thm)],[f74,f2444]) ).
fof(f2446,plain,
( ~ sQ49_spl
| ~ sQ11_spl
| sQ60_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2445,f435]) ).
fof(f2447,plain,
( ~ sQ49_spl
| ~ sQ11_spl
| sQ60_spl ),
inference(contradiction_clause,[status(thm)],[f2446]) ).
fof(f2496,plain,
( ~ sQ52_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f2178,f366,f407]) ).
fof(f2507,plain,
( ~ sQ33_spl
| h(e12) = op2(e23,h(e15)) ),
inference(forward_demodulation,[status(thm)],[f348,f845]) ).
fof(f2508,plain,
( ~ sQ33_spl
| h(e12) = op2(e23,e23) ),
inference(forward_demodulation,[status(thm)],[f348,f2507]) ).
fof(f2512,plain,
( ~ sQ33_spl
| h(e12) = e24 ),
inference(forward_demodulation,[status(thm)],[f131,f2508]) ).
fof(f2529,plain,
( ~ sQ62_spl
| ~ sQ59_spl
| e15 = e13 ),
inference(forward_demodulation,[status(thm)],[f430,f1048]) ).
fof(f2530,plain,
( ~ sQ62_spl
| ~ sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2529,f21]) ).
fof(f2531,plain,
( ~ sQ62_spl
| ~ sQ59_spl ),
inference(contradiction_clause,[status(thm)],[f2530]) ).
fof(f2600,plain,
( ~ sQ39_spl
| j(e20) = op1(j(e20),e13) ),
inference(backward_demodulation,[status(thm)],[f367,f852]) ).
fof(f2603,plain,
( ~ sQ39_spl
| e13 = op1(j(e20),e13) ),
inference(forward_demodulation,[status(thm)],[f367,f2600]) ).
fof(f2604,plain,
( ~ sQ39_spl
| e13 = op1(e13,e13) ),
inference(forward_demodulation,[status(thm)],[f367,f2603]) ).
fof(f2605,plain,
( ~ sQ39_spl
| e13 = e12 ),
inference(forward_demodulation,[status(thm)],[f95,f2604]) ).
fof(f2606,plain,
( ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2605,f17]) ).
fof(f2607,plain,
~ sQ39_spl,
inference(contradiction_clause,[status(thm)],[f2606]) ).
fof(f2626,plain,
( ~ sQ28_spl
| j(e24) = e14 ),
inference(forward_demodulation,[status(thm)],[f332,f241]) ).
fof(f2629,plain,
( ~ sQ18_spl
| ~ sQ28_spl
| e23 = e20 ),
inference(forward_demodulation,[status(thm)],[f1729,f301]) ).
fof(f2630,plain,
( ~ sQ18_spl
| ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2629,f25]) ).
fof(f2631,plain,
( ~ sQ18_spl
| ~ sQ28_spl ),
inference(contradiction_clause,[status(thm)],[f2630]) ).
fof(f2646,plain,
( ~ sQ28_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f2626,f445,f331]) ).
fof(f2661,plain,
( ~ sQ30_spl
| j(e20) = e15 ),
inference(backward_demodulation,[status(thm)],[f339,f242]) ).
fof(f2663,plain,
( ~ sQ30_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f2661,f372,f338]) ).
fof(f2666,plain,
( ~ sQ16_spl
| j(e24) = e12 ),
inference(backward_demodulation,[status(thm)],[f294,f239]) ).
fof(f2670,plain,
( ~ sQ16_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f2666,f439,f293]) ).
fof(f2711,plain,
( ~ sQ49_spl
| ~ sQ64_spl
| j(e21) = op1(e11,e14) ),
inference(forward_demodulation,[status(thm)],[f446,f1622]) ).
fof(f2712,plain,
( ~ sQ49_spl
| ~ sQ64_spl
| j(e21) = e12 ),
inference(forward_demodulation,[status(thm)],[f84,f2711]) ).
fof(f2713,plain,
( ~ sQ49_spl
| ~ sQ64_spl
| sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2712,f384]) ).
fof(f2714,plain,
( ~ sQ49_spl
| ~ sQ64_spl
| sQ44_spl ),
inference(contradiction_clause,[status(thm)],[f2713]) ).
fof(f2736,plain,
( ~ sQ17_spl
| ~ sQ33_spl
| e24 = e25 ),
inference(forward_demodulation,[status(thm)],[f2512,f297]) ).
fof(f2737,plain,
( ~ sQ17_spl
| ~ sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2736,f37]) ).
fof(f2738,plain,
( ~ sQ17_spl
| ~ sQ33_spl ),
inference(contradiction_clause,[status(thm)],[f2737]) ).
fof(f2744,plain,
( ~ sQ29_spl
| h(e13) = op2(h(e14),e25) ),
inference(backward_demodulation,[status(thm)],[f335,f805]) ).
fof(f2749,plain,
( ~ sQ29_spl
| h(e13) = op2(e25,e25) ),
inference(forward_demodulation,[status(thm)],[f335,f2744]) ).
fof(f2750,plain,
( ~ sQ29_spl
| h(e13) = e20 ),
inference(forward_demodulation,[status(thm)],[f145,f2749]) ).
fof(f2756,plain,
( ~ sQ23_spl
| j(e25) = e13 ),
inference(backward_demodulation,[status(thm)],[f316,f240]) ).
fof(f2757,plain,
( ~ sQ23_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f2756,f461,f315]) ).
fof(f2769,plain,
( ~ sQ53_spl
| h(e15) = e22 ),
inference(backward_demodulation,[status(thm)],[f411,f233]) ).
fof(f2772,plain,
( ~ sQ53_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f2769,f344,f410]) ).
fof(f2814,plain,
( ~ sQ35_spl
| h(e12) = op2(e25,h(e15)) ),
inference(forward_demodulation,[status(thm)],[f354,f845]) ).
fof(f2815,plain,
( ~ sQ35_spl
| h(e12) = op2(e25,e25) ),
inference(forward_demodulation,[status(thm)],[f354,f2814]) ).
fof(f2816,plain,
( ~ sQ35_spl
| h(e12) = e20 ),
inference(forward_demodulation,[status(thm)],[f145,f2815]) ).
fof(f2817,plain,
( ~ sQ35_spl
| sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2816,f283]) ).
fof(f2818,plain,
( ~ sQ35_spl
| sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f2817]) ).
fof(f2838,plain,
( ~ sQ49_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1625,f357,f398]) ).
fof(f2854,plain,
( ~ sQ29_spl
| h(e11) = op2(e20,h(e14)) ),
inference(forward_demodulation,[status(thm)],[f2750,f771]) ).
fof(f2855,plain,
( ~ sQ29_spl
| h(e11) = op2(e20,e25) ),
inference(forward_demodulation,[status(thm)],[f335,f2854]) ).
fof(f2856,plain,
( ~ sQ29_spl
| h(e11) = e25 ),
inference(forward_demodulation,[status(thm)],[f115,f2855]) ).
fof(f2857,plain,
( ~ sQ29_spl
| sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2856,f279]) ).
fof(f2858,plain,
( ~ sQ29_spl
| sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f2857]) ).
fof(f2859,plain,
$false,
inference(sat_refutation,[status(thm)],[f280,f299,f337,f356,f413,f510,f527,f546,f606,f622,f685,f802,f936,f986,f1024,f1084,f1117,f1166,f1321,f1402,f1403,f1427,f1478,f1479,f1481,f1497,f1514,f1552,f1560,f1568,f1574,f1609,f1614,f1651,f1665,f1715,f1721,f1809,f1815,f1816,f1841,f1846,f1883,f1914,f1915,f2031,f2127,f2161,f2164,f2235,f2245,f2343,f2412,f2447,f2496,f2531,f2607,f2631,f2646,f2663,f2670,f2714,f2738,f2757,f2772,f2818,f2838,f2858]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG031+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n026.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 12:56:38 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 0.12/0.45 % Refutation found
% 0.12/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.49 % Elapsed time: 0.114979 seconds
% 0.12/0.49 % CPU time: 0.532844 seconds
% 0.12/0.49 % Total memory used: 124.067 MB
% 0.12/0.49 % Net memory used: 123.800 MB
%------------------------------------------------------------------------------