%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG205+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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 11:48:54 AM UTC 2026
% Result : Theorem 0.14s 0.49s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 94
% Syntax : Number of formulae : 1091 ( 223 unt; 89 def)
% Number of atoms : 3104 (1597 equ)
% Maximal formula atoms : 210 ( 2 avg)
% Number of connectives : 3273 (1260 ~;1413 |; 509 &)
% ( 89 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 126 ( 3 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 91 ( 89 usr; 90 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 14 con; 0-2 aty)
% Number of variables : 0 ( 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( e15 != e16
& e14 != e16
& e14 != e15
& e13 != e16
& e13 != e15
& e13 != e14
& e12 != e16
& e12 != e15
& e12 != e14
& e12 != e13
& e11 != e16
& e11 != e15
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e16
& e10 != e15
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
( e25 != e26
& e24 != e26
& e24 != e25
& e23 != e26
& e23 != e25
& e23 != e24
& e22 != e26
& e22 != e25
& e22 != e24
& e22 != e23
& e21 != e26
& e21 != e25
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e26
& e20 != e25
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
( op1(e16,e16) = e10
& op1(e16,e15) = e16
& op1(e16,e14) = e11
& op1(e16,e13) = e13
& op1(e16,e12) = e14
& op1(e16,e11) = e12
& op1(e16,e10) = e15
& op1(e15,e16) = e16
& op1(e15,e15) = e11
& op1(e15,e14) = e15
& op1(e15,e13) = e10
& op1(e15,e12) = e13
& op1(e15,e11) = e14
& op1(e15,e10) = e12
& op1(e14,e16) = e11
& op1(e14,e15) = e15
& op1(e14,e14) = e12
& op1(e14,e13) = e16
& op1(e14,e12) = e10
& op1(e14,e11) = e13
& op1(e14,e10) = e14
& op1(e13,e16) = e13
& op1(e13,e15) = e10
& op1(e13,e14) = e16
& op1(e13,e13) = e14
& op1(e13,e12) = e12
& op1(e13,e11) = e15
& op1(e13,e10) = e11
& op1(e12,e16) = e14
& op1(e12,e15) = e13
& op1(e12,e14) = e10
& op1(e12,e13) = e12
& op1(e12,e12) = e15
& op1(e12,e11) = e11
& op1(e12,e10) = e16
& op1(e11,e16) = e12
& op1(e11,e15) = e14
& op1(e11,e14) = e13
& op1(e11,e13) = e15
& op1(e11,e12) = e11
& op1(e11,e11) = e16
& op1(e11,e10) = e10
& op1(e10,e16) = e15
& op1(e10,e15) = e12
& op1(e10,e14) = e14
& op1(e10,e13) = e11
& op1(e10,e12) = e16
& op1(e10,e11) = e10
& op1(e10,e10) = e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
( op2(e26,e26) = e25
& op2(e26,e25) = e20
& op2(e26,e24) = e21
& op2(e26,e23) = e24
& op2(e26,e22) = e22
& op2(e26,e21) = e23
& op2(e26,e20) = e26
& op2(e25,e26) = e20
& op2(e25,e25) = e21
& op2(e25,e24) = e26
& op2(e25,e23) = e23
& op2(e25,e22) = e25
& op2(e25,e21) = e22
& op2(e25,e20) = e24
& op2(e24,e26) = e21
& op2(e24,e25) = e26
& op2(e24,e24) = e24
& op2(e24,e23) = e22
& op2(e24,e22) = e20
& op2(e24,e21) = e25
& op2(e24,e20) = e23
& op2(e23,e26) = e24
& op2(e23,e25) = e23
& op2(e23,e24) = e22
& op2(e23,e23) = e20
& op2(e23,e22) = e26
& op2(e23,e21) = e21
& op2(e23,e20) = e25
& op2(e22,e26) = e22
& op2(e22,e25) = e25
& op2(e22,e24) = e20
& op2(e22,e23) = e26
& op2(e22,e22) = e23
& op2(e22,e21) = e24
& op2(e22,e20) = e21
& op2(e21,e26) = e23
& op2(e21,e25) = e22
& op2(e21,e24) = e25
& op2(e21,e23) = e21
& op2(e21,e22) = e24
& op2(e21,e21) = e26
& op2(e21,e20) = e20
& op2(e20,e26) = e26
& op2(e20,e25) = e24
& op2(e20,e24) = e23
& op2(e20,e23) = e25
& op2(e20,e22) = e21
& op2(e20,e21) = e20
& op2(e20,e20) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,conjecture,
( ( ( j(e26) = e16
| j(e26) = e15
| j(e26) = e14
| j(e26) = e13
| j(e26) = e12
| j(e26) = e11
| j(e26) = e10 )
& ( j(e25) = e16
| j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e16
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e16
| j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e16
| j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e16
| j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e16) = e26
| h(e16) = e25
| h(e16) = e24
| h(e16) = e23
| h(e16) = e22
| h(e16) = e21
| h(e16) = e20 )
& ( h(e15) = e26
| h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e26
| h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e26
| h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e26
| h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e26
| h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e26
| h(e10) = e25
| h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e16)) = e16
& 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(e26)) = e26
& 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(e26,e26)) = op1(j(e26),j(e26))
& j(op2(e26,e25)) = op1(j(e26),j(e25))
& j(op2(e26,e24)) = op1(j(e26),j(e24))
& j(op2(e26,e23)) = op1(j(e26),j(e23))
& j(op2(e26,e22)) = op1(j(e26),j(e22))
& j(op2(e26,e21)) = op1(j(e26),j(e21))
& j(op2(e26,e20)) = op1(j(e26),j(e20))
& j(op2(e25,e26)) = op1(j(e25),j(e26))
& 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,e26)) = op1(j(e24),j(e26))
& 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,e26)) = op1(j(e23),j(e26))
& 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,e26)) = op1(j(e22),j(e26))
& 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,e26)) = op1(j(e21),j(e26))
& 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,e26)) = op1(j(e20),j(e26))
& 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(e16,e16)) = op2(h(e16),h(e16))
& h(op1(e16,e15)) = op2(h(e16),h(e15))
& h(op1(e16,e14)) = op2(h(e16),h(e14))
& h(op1(e16,e13)) = op2(h(e16),h(e13))
& h(op1(e16,e12)) = op2(h(e16),h(e12))
& h(op1(e16,e11)) = op2(h(e16),h(e11))
& h(op1(e16,e10)) = op2(h(e16),h(e10))
& h(op1(e15,e16)) = op2(h(e15),h(e16))
& 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,e16)) = op2(h(e14),h(e16))
& 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,e16)) = op2(h(e13),h(e16))
& 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,e16)) = op2(h(e12),h(e16))
& 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,e16)) = op2(h(e11),h(e16))
& 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,e16)) = op2(h(e10),h(e16))
& 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/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,negated_conjecture,
~ ( ( ( j(e26) = e16
| j(e26) = e15
| j(e26) = e14
| j(e26) = e13
| j(e26) = e12
| j(e26) = e11
| j(e26) = e10 )
& ( j(e25) = e16
| j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e16
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e16
| j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e16
| j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e16
| j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e16) = e26
| h(e16) = e25
| h(e16) = e24
| h(e16) = e23
| h(e16) = e22
| h(e16) = e21
| h(e16) = e20 )
& ( h(e15) = e26
| h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e26
| h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e26
| h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e26
| h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e26
| h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e26
| h(e10) = e25
| h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e16)) = e16
& 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(e26)) = e26
& 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(e26,e26)) = op1(j(e26),j(e26))
& j(op2(e26,e25)) = op1(j(e26),j(e25))
& j(op2(e26,e24)) = op1(j(e26),j(e24))
& j(op2(e26,e23)) = op1(j(e26),j(e23))
& j(op2(e26,e22)) = op1(j(e26),j(e22))
& j(op2(e26,e21)) = op1(j(e26),j(e21))
& j(op2(e26,e20)) = op1(j(e26),j(e20))
& j(op2(e25,e26)) = op1(j(e25),j(e26))
& 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,e26)) = op1(j(e24),j(e26))
& 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,e26)) = op1(j(e23),j(e26))
& 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,e26)) = op1(j(e22),j(e26))
& 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,e26)) = op1(j(e21),j(e26))
& 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,e26)) = op1(j(e20),j(e26))
& 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(e16,e16)) = op2(h(e16),h(e16))
& h(op1(e16,e15)) = op2(h(e16),h(e15))
& h(op1(e16,e14)) = op2(h(e16),h(e14))
& h(op1(e16,e13)) = op2(h(e16),h(e13))
& h(op1(e16,e12)) = op2(h(e16),h(e12))
& h(op1(e16,e11)) = op2(h(e16),h(e11))
& h(op1(e16,e10)) = op2(h(e16),h(e10))
& h(op1(e15,e16)) = op2(h(e15),h(e16))
& 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,e16)) = op2(h(e14),h(e16))
& 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,e16)) = op2(h(e13),h(e16))
& 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,e16)) = op2(h(e12),h(e16))
& 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,e16)) = op2(h(e11),h(e16))
& 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,e16)) = op2(h(e10),h(e16))
& 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(f9,plain,
e10 != e12,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f10,plain,
e10 != e13,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f12,plain,
e10 != e15,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f13,plain,
e10 != e16,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f14,plain,
e11 != e12,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f15,plain,
e11 != e13,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f16,plain,
e11 != e14,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f17,plain,
e11 != e15,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f18,plain,
e11 != e16,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f19,plain,
e12 != e13,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f20,plain,
e12 != e14,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f21,plain,
e12 != e15,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f22,plain,
e12 != e16,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f23,plain,
e13 != e14,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f24,plain,
e13 != e15,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f25,plain,
e13 != e16,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f27,plain,
e14 != e16,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f28,plain,
e15 != e16,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f29,plain,
e20 != e21,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f30,plain,
e20 != e22,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f31,plain,
e20 != e23,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f32,plain,
e20 != e24,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f33,plain,
e20 != e25,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f35,plain,
e21 != e22,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f37,plain,
e21 != e24,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f38,plain,
e21 != e25,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f39,plain,
e21 != e26,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f41,plain,
e22 != e24,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f42,plain,
e22 != e25,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f44,plain,
e23 != e24,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f45,plain,
e23 != e25,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f47,plain,
e24 != e25,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f48,plain,
e24 != e26,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f49,plain,
e25 != e26,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f99,plain,
op1(e10,e10) = e13,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f100,plain,
op1(e10,e11) = e10,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f101,plain,
op1(e10,e12) = e16,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f102,plain,
op1(e10,e13) = e11,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f104,plain,
op1(e10,e15) = e12,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f105,plain,
op1(e10,e16) = e15,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f106,plain,
op1(e11,e10) = e10,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f107,plain,
op1(e11,e11) = e16,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f108,plain,
op1(e11,e12) = e11,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f109,plain,
op1(e11,e13) = e15,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f110,plain,
op1(e11,e14) = e13,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f111,plain,
op1(e11,e15) = e14,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f112,plain,
op1(e11,e16) = e12,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f113,plain,
op1(e12,e10) = e16,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f115,plain,
op1(e12,e12) = e15,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f117,plain,
op1(e12,e14) = e10,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f118,plain,
op1(e12,e15) = e13,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f119,plain,
op1(e12,e16) = e14,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f121,plain,
op1(e13,e11) = e15,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f122,plain,
op1(e13,e12) = e12,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f123,plain,
op1(e13,e13) = e14,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f125,plain,
op1(e13,e15) = e10,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f126,plain,
op1(e13,e16) = e13,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f128,plain,
op1(e14,e11) = e13,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f131,plain,
op1(e14,e14) = e12,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f132,plain,
op1(e14,e15) = e15,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f134,plain,
op1(e15,e10) = e12,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f135,plain,
op1(e15,e11) = e14,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f136,plain,
op1(e15,e12) = e13,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f137,plain,
op1(e15,e13) = e10,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f139,plain,
op1(e15,e15) = e11,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f140,plain,
op1(e15,e16) = e16,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f141,plain,
op1(e16,e10) = e15,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f144,plain,
op1(e16,e13) = e13,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f147,plain,
op1(e16,e16) = e10,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f148,plain,
op2(e20,e20) = e22,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f149,plain,
op2(e20,e21) = e20,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f150,plain,
op2(e20,e22) = e21,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f152,plain,
op2(e20,e24) = e23,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f153,plain,
op2(e20,e25) = e24,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f154,plain,
op2(e20,e26) = e26,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f156,plain,
op2(e21,e21) = e26,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f157,plain,
op2(e21,e22) = e24,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f159,plain,
op2(e21,e24) = e25,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f160,plain,
op2(e21,e25) = e22,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f161,plain,
op2(e21,e26) = e23,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f162,plain,
op2(e22,e20) = e21,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f163,plain,
op2(e22,e21) = e24,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f164,plain,
op2(e22,e22) = e23,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f165,plain,
op2(e22,e23) = e26,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f166,plain,
op2(e22,e24) = e20,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f167,plain,
op2(e22,e25) = e25,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f168,plain,
op2(e22,e26) = e22,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f169,plain,
op2(e23,e20) = e25,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f171,plain,
op2(e23,e22) = e26,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f172,plain,
op2(e23,e23) = e20,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f175,plain,
op2(e23,e26) = e24,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f176,plain,
op2(e24,e20) = e23,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f177,plain,
op2(e24,e21) = e25,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f180,plain,
op2(e24,e24) = e24,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f181,plain,
op2(e24,e25) = e26,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f182,plain,
op2(e24,e26) = e21,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f187,plain,
op2(e25,e24) = e26,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f188,plain,
op2(e25,e25) = e21,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f191,plain,
op2(e26,e21) = e23,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f192,plain,
op2(e26,e22) = e22,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f194,plain,
op2(e26,e24) = e21,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f195,plain,
op2(e26,e25) = e20,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f196,plain,
op2(e26,e26) = e25,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f197,plain,
( j(h(e16)) = e16
& 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(e26)) = e26
& 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(e26,e26)) = op1(j(e26),j(e26))
& j(op2(e26,e25)) = op1(j(e26),j(e25))
& j(op2(e26,e24)) = op1(j(e26),j(e24))
& j(op2(e26,e23)) = op1(j(e26),j(e23))
& j(op2(e26,e22)) = op1(j(e26),j(e22))
& j(op2(e26,e21)) = op1(j(e26),j(e21))
& j(op2(e26,e20)) = op1(j(e26),j(e20))
& j(op2(e25,e26)) = op1(j(e25),j(e26))
& 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,e26)) = op1(j(e24),j(e26))
& 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,e26)) = op1(j(e23),j(e26))
& 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,e26)) = op1(j(e22),j(e26))
& 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,e26)) = op1(j(e21),j(e26))
& 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,e26)) = op1(j(e20),j(e26))
& 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(e16,e16)) = op2(h(e16),h(e16))
& h(op1(e16,e15)) = op2(h(e16),h(e15))
& h(op1(e16,e14)) = op2(h(e16),h(e14))
& h(op1(e16,e13)) = op2(h(e16),h(e13))
& h(op1(e16,e12)) = op2(h(e16),h(e12))
& h(op1(e16,e11)) = op2(h(e16),h(e11))
& h(op1(e16,e10)) = op2(h(e16),h(e10))
& h(op1(e15,e16)) = op2(h(e15),h(e16))
& 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,e16)) = op2(h(e14),h(e16))
& 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,e16)) = op2(h(e13),h(e16))
& 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,e16)) = op2(h(e12),h(e16))
& 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,e16)) = op2(h(e11),h(e16))
& 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,e16)) = op2(h(e10),h(e16))
& 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(e26) = e16
| j(e26) = e15
| j(e26) = e14
| j(e26) = e13
| j(e26) = e12
| j(e26) = e11
| j(e26) = e10 )
& ( j(e25) = e16
| j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e16
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e16
| j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e16
| j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e16
| j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e16) = e26
| h(e16) = e25
| h(e16) = e24
| h(e16) = e23
| h(e16) = e22
| h(e16) = e21
| h(e16) = e20 )
& ( h(e15) = e26
| h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e26
| h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e26
| h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e26
| h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e26
| h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e26
| 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(f199,plain,
( h(e11) = e26
| h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f206,plain,
( j(e21) = e16
| j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f209,plain,
( j(e24) = e16
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f212,plain,
h(op1(e10,e10)) = op2(h(e10),h(e10)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f213,plain,
h(op1(e10,e11)) = op2(h(e10),h(e11)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f214,plain,
h(op1(e10,e12)) = op2(h(e10),h(e12)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f218,plain,
h(op1(e10,e16)) = op2(h(e10),h(e16)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f220,plain,
h(op1(e11,e11)) = op2(h(e11),h(e11)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f221,plain,
h(op1(e11,e12)) = op2(h(e11),h(e12)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f222,plain,
h(op1(e11,e13)) = op2(h(e11),h(e13)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f223,plain,
h(op1(e11,e14)) = op2(h(e11),h(e14)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f224,plain,
h(op1(e11,e15)) = op2(h(e11),h(e15)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f225,plain,
h(op1(e11,e16)) = op2(h(e11),h(e16)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f226,plain,
h(op1(e12,e10)) = op2(h(e12),h(e10)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f228,plain,
h(op1(e12,e12)) = op2(h(e12),h(e12)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f232,plain,
h(op1(e12,e16)) = op2(h(e12),h(e16)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f235,plain,
h(op1(e13,e12)) = op2(h(e13),h(e12)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f236,plain,
h(op1(e13,e13)) = op2(h(e13),h(e13)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f238,plain,
h(op1(e13,e15)) = op2(h(e13),h(e15)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f239,plain,
h(op1(e13,e16)) = op2(h(e13),h(e16)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f244,plain,
h(op1(e14,e14)) = op2(h(e14),h(e14)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f245,plain,
h(op1(e14,e15)) = op2(h(e14),h(e15)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f247,plain,
h(op1(e15,e10)) = op2(h(e15),h(e10)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f248,plain,
h(op1(e15,e11)) = op2(h(e15),h(e11)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f252,plain,
h(op1(e15,e15)) = op2(h(e15),h(e15)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f253,plain,
h(op1(e15,e16)) = op2(h(e15),h(e16)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f254,plain,
h(op1(e16,e10)) = op2(h(e16),h(e10)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f257,plain,
h(op1(e16,e13)) = op2(h(e16),h(e13)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f260,plain,
h(op1(e16,e16)) = op2(h(e16),h(e16)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f261,plain,
j(op2(e20,e20)) = op1(j(e20),j(e20)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f263,plain,
j(op2(e20,e22)) = op1(j(e20),j(e22)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f265,plain,
j(op2(e20,e24)) = op1(j(e20),j(e24)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f267,plain,
j(op2(e20,e26)) = op1(j(e20),j(e26)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f269,plain,
j(op2(e21,e21)) = op1(j(e21),j(e21)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f272,plain,
j(op2(e21,e24)) = op1(j(e21),j(e24)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f273,plain,
j(op2(e21,e25)) = op1(j(e21),j(e25)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f274,plain,
j(op2(e21,e26)) = op1(j(e21),j(e26)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f276,plain,
j(op2(e22,e21)) = op1(j(e22),j(e21)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f277,plain,
j(op2(e22,e22)) = op1(j(e22),j(e22)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f279,plain,
j(op2(e22,e24)) = op1(j(e22),j(e24)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f280,plain,
j(op2(e22,e25)) = op1(j(e22),j(e25)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f281,plain,
j(op2(e22,e26)) = op1(j(e22),j(e26)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f282,plain,
j(op2(e23,e20)) = op1(j(e23),j(e20)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f284,plain,
j(op2(e23,e22)) = op1(j(e23),j(e22)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f285,plain,
j(op2(e23,e23)) = op1(j(e23),j(e23)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f290,plain,
j(op2(e24,e21)) = op1(j(e24),j(e21)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f293,plain,
j(op2(e24,e24)) = op1(j(e24),j(e24)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f294,plain,
j(op2(e24,e25)) = op1(j(e24),j(e25)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f300,plain,
j(op2(e25,e24)) = op1(j(e25),j(e24)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f301,plain,
j(op2(e25,e25)) = op1(j(e25),j(e25)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f304,plain,
j(op2(e26,e21)) = op1(j(e26),j(e21)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f305,plain,
j(op2(e26,e22)) = op1(j(e26),j(e22)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f309,plain,
j(op2(e26,e26)) = op1(j(e26),j(e26)),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f310,plain,
h(j(e20)) = e20,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f311,plain,
h(j(e21)) = e21,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f312,plain,
h(j(e22)) = e22,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f313,plain,
h(j(e23)) = e23,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f314,plain,
h(j(e24)) = e24,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f315,plain,
h(j(e25)) = e25,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f316,plain,
h(j(e26)) = e26,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f317,plain,
j(h(e10)) = e10,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f318,plain,
j(h(e11)) = e11,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f319,plain,
j(h(e12)) = e12,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f320,plain,
j(h(e13)) = e13,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f321,plain,
j(h(e14)) = e14,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f322,plain,
j(h(e15)) = e15,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f323,plain,
j(h(e16)) = e16,
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f324,definition,
( sQ0_spl
<=> h(e10) = e20 ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f325,plain,
( ~ sQ0_spl
| h(e10) = e20 ),
inference(component_clause,[status(thm)],[f324]) ).
fof(f327,definition,
( sQ1_spl
<=> h(e10) = e21 ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f328,plain,
( ~ sQ1_spl
| h(e10) = e21 ),
inference(component_clause,[status(thm)],[f327]) ).
fof(f330,definition,
( sQ2_spl
<=> h(e10) = e22 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f331,plain,
( ~ sQ2_spl
| h(e10) = e22 ),
inference(component_clause,[status(thm)],[f330]) ).
fof(f333,definition,
( sQ3_spl
<=> h(e10) = e23 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f334,plain,
( ~ sQ3_spl
| h(e10) = e23 ),
inference(component_clause,[status(thm)],[f333]) ).
fof(f335,plain,
( sQ3_spl
| h(e10) != e23 ),
inference(component_clause,[status(thm)],[f333]) ).
fof(f336,definition,
( sQ4_spl
<=> h(e10) = e24 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f337,plain,
( ~ sQ4_spl
| h(e10) = e24 ),
inference(component_clause,[status(thm)],[f336]) ).
fof(f339,definition,
( sQ5_spl
<=> h(e10) = e25 ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f340,plain,
( ~ sQ5_spl
| h(e10) = e25 ),
inference(component_clause,[status(thm)],[f339]) ).
fof(f342,definition,
( sQ6_spl
<=> h(e10) = e26 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f343,plain,
( ~ sQ6_spl
| h(e10) = e26 ),
inference(component_clause,[status(thm)],[f342]) ).
fof(f346,definition,
( sQ7_spl
<=> h(e11) = e20 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f347,plain,
( ~ sQ7_spl
| h(e11) = e20 ),
inference(component_clause,[status(thm)],[f346]) ).
fof(f349,definition,
( sQ8_spl
<=> h(e11) = e21 ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f350,plain,
( ~ sQ8_spl
| h(e11) = e21 ),
inference(component_clause,[status(thm)],[f349]) ).
fof(f351,plain,
( sQ8_spl
| h(e11) != e21 ),
inference(component_clause,[status(thm)],[f349]) ).
fof(f352,definition,
( sQ9_spl
<=> h(e11) = e22 ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f353,plain,
( ~ sQ9_spl
| h(e11) = e22 ),
inference(component_clause,[status(thm)],[f352]) ).
fof(f355,definition,
( sQ10_spl
<=> h(e11) = e23 ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f356,plain,
( ~ sQ10_spl
| h(e11) = e23 ),
inference(component_clause,[status(thm)],[f355]) ).
fof(f358,definition,
( sQ11_spl
<=> h(e11) = e24 ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f359,plain,
( ~ sQ11_spl
| h(e11) = e24 ),
inference(component_clause,[status(thm)],[f358]) ).
fof(f361,definition,
( sQ12_spl
<=> h(e11) = e25 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f362,plain,
( ~ sQ12_spl
| h(e11) = e25 ),
inference(component_clause,[status(thm)],[f361]) ).
fof(f364,definition,
( sQ13_spl
<=> h(e11) = e26 ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f365,plain,
( ~ sQ13_spl
| h(e11) = e26 ),
inference(component_clause,[status(thm)],[f364]) ).
fof(f367,plain,
( sQ13_spl
| sQ12_spl
| sQ11_spl
| sQ10_spl
| sQ9_spl
| sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f199,f346,f349,f352,f355,f358,f361,f364]) ).
fof(f368,definition,
( sQ14_spl
<=> h(e12) = e20 ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f369,plain,
( ~ sQ14_spl
| h(e12) = e20 ),
inference(component_clause,[status(thm)],[f368]) ).
fof(f370,plain,
( sQ14_spl
| h(e12) != e20 ),
inference(component_clause,[status(thm)],[f368]) ).
fof(f371,definition,
( sQ15_spl
<=> h(e12) = e21 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f372,plain,
( ~ sQ15_spl
| h(e12) = e21 ),
inference(component_clause,[status(thm)],[f371]) ).
fof(f374,definition,
( sQ16_spl
<=> h(e12) = e22 ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f375,plain,
( ~ sQ16_spl
| h(e12) = e22 ),
inference(component_clause,[status(thm)],[f374]) ).
fof(f376,plain,
( sQ16_spl
| h(e12) != e22 ),
inference(component_clause,[status(thm)],[f374]) ).
fof(f377,definition,
( sQ17_spl
<=> h(e12) = e23 ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f378,plain,
( ~ sQ17_spl
| h(e12) = e23 ),
inference(component_clause,[status(thm)],[f377]) ).
fof(f380,definition,
( sQ18_spl
<=> h(e12) = e24 ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f381,plain,
( ~ sQ18_spl
| h(e12) = e24 ),
inference(component_clause,[status(thm)],[f380]) ).
fof(f382,plain,
( sQ18_spl
| h(e12) != e24 ),
inference(component_clause,[status(thm)],[f380]) ).
fof(f383,definition,
( sQ19_spl
<=> h(e12) = e25 ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f384,plain,
( ~ sQ19_spl
| h(e12) = e25 ),
inference(component_clause,[status(thm)],[f383]) ).
fof(f385,plain,
( sQ19_spl
| h(e12) != e25 ),
inference(component_clause,[status(thm)],[f383]) ).
fof(f390,definition,
( sQ21_spl
<=> h(e13) = e20 ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f391,plain,
( ~ sQ21_spl
| h(e13) = e20 ),
inference(component_clause,[status(thm)],[f390]) ).
fof(f393,definition,
( sQ22_spl
<=> h(e13) = e21 ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f394,plain,
( ~ sQ22_spl
| h(e13) = e21 ),
inference(component_clause,[status(thm)],[f393]) ).
fof(f396,definition,
( sQ23_spl
<=> h(e13) = e22 ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f397,plain,
( ~ sQ23_spl
| h(e13) = e22 ),
inference(component_clause,[status(thm)],[f396]) ).
fof(f398,plain,
( sQ23_spl
| h(e13) != e22 ),
inference(component_clause,[status(thm)],[f396]) ).
fof(f399,definition,
( sQ24_spl
<=> h(e13) = e23 ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f400,plain,
( ~ sQ24_spl
| h(e13) = e23 ),
inference(component_clause,[status(thm)],[f399]) ).
fof(f402,definition,
( sQ25_spl
<=> h(e13) = e24 ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f403,plain,
( ~ sQ25_spl
| h(e13) = e24 ),
inference(component_clause,[status(thm)],[f402]) ).
fof(f405,definition,
( sQ26_spl
<=> h(e13) = e25 ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f406,plain,
( ~ sQ26_spl
| h(e13) = e25 ),
inference(component_clause,[status(thm)],[f405]) ).
fof(f412,definition,
( sQ28_spl
<=> h(e14) = e20 ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f413,plain,
( ~ sQ28_spl
| h(e14) = e20 ),
inference(component_clause,[status(thm)],[f412]) ).
fof(f414,plain,
( sQ28_spl
| h(e14) != e20 ),
inference(component_clause,[status(thm)],[f412]) ).
fof(f415,definition,
( sQ29_spl
<=> h(e14) = e21 ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f416,plain,
( ~ sQ29_spl
| h(e14) = e21 ),
inference(component_clause,[status(thm)],[f415]) ).
fof(f417,plain,
( sQ29_spl
| h(e14) != e21 ),
inference(component_clause,[status(thm)],[f415]) ).
fof(f421,definition,
( sQ31_spl
<=> h(e14) = e23 ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f422,plain,
( ~ sQ31_spl
| h(e14) = e23 ),
inference(component_clause,[status(thm)],[f421]) ).
fof(f424,definition,
( sQ32_spl
<=> h(e14) = e24 ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f425,plain,
( ~ sQ32_spl
| h(e14) = e24 ),
inference(component_clause,[status(thm)],[f424]) ).
fof(f426,plain,
( sQ32_spl
| h(e14) != e24 ),
inference(component_clause,[status(thm)],[f424]) ).
fof(f430,definition,
( sQ34_spl
<=> h(e14) = e26 ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f431,plain,
( ~ sQ34_spl
| h(e14) = e26 ),
inference(component_clause,[status(thm)],[f430]) ).
fof(f432,plain,
( sQ34_spl
| h(e14) != e26 ),
inference(component_clause,[status(thm)],[f430]) ).
fof(f434,definition,
( sQ35_spl
<=> h(e15) = e20 ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f435,plain,
( ~ sQ35_spl
| h(e15) = e20 ),
inference(component_clause,[status(thm)],[f434]) ).
fof(f437,definition,
( sQ36_spl
<=> h(e15) = e21 ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f438,plain,
( ~ sQ36_spl
| h(e15) = e21 ),
inference(component_clause,[status(thm)],[f437]) ).
fof(f440,definition,
( sQ37_spl
<=> h(e15) = e22 ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f441,plain,
( ~ sQ37_spl
| h(e15) = e22 ),
inference(component_clause,[status(thm)],[f440]) ).
fof(f443,definition,
( sQ38_spl
<=> h(e15) = e23 ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f444,plain,
( ~ sQ38_spl
| h(e15) = e23 ),
inference(component_clause,[status(thm)],[f443]) ).
fof(f446,definition,
( sQ39_spl
<=> h(e15) = e24 ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f447,plain,
( ~ sQ39_spl
| h(e15) = e24 ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f448,plain,
( sQ39_spl
| h(e15) != e24 ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f449,definition,
( sQ40_spl
<=> h(e15) = e25 ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f450,plain,
( ~ sQ40_spl
| h(e15) = e25 ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f452,definition,
( sQ41_spl
<=> h(e15) = e26 ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f453,plain,
( ~ sQ41_spl
| h(e15) = e26 ),
inference(component_clause,[status(thm)],[f452]) ).
fof(f454,plain,
( sQ41_spl
| h(e15) != e26 ),
inference(component_clause,[status(thm)],[f452]) ).
fof(f456,definition,
( sQ42_spl
<=> h(e16) = e20 ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f457,plain,
( ~ sQ42_spl
| h(e16) = e20 ),
inference(component_clause,[status(thm)],[f456]) ).
fof(f458,plain,
( sQ42_spl
| h(e16) != e20 ),
inference(component_clause,[status(thm)],[f456]) ).
fof(f459,definition,
( sQ43_spl
<=> h(e16) = e21 ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f460,plain,
( ~ sQ43_spl
| h(e16) = e21 ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f462,definition,
( sQ44_spl
<=> h(e16) = e22 ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f463,plain,
( ~ sQ44_spl
| h(e16) = e22 ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f465,definition,
( sQ45_spl
<=> h(e16) = e23 ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f466,plain,
( ~ sQ45_spl
| h(e16) = e23 ),
inference(component_clause,[status(thm)],[f465]) ).
fof(f468,definition,
( sQ46_spl
<=> h(e16) = e24 ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f469,plain,
( ~ sQ46_spl
| h(e16) = e24 ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f471,definition,
( sQ47_spl
<=> h(e16) = e25 ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f472,plain,
( ~ sQ47_spl
| h(e16) = e25 ),
inference(component_clause,[status(thm)],[f471]) ).
fof(f473,plain,
( sQ47_spl
| h(e16) != e25 ),
inference(component_clause,[status(thm)],[f471]) ).
fof(f478,definition,
( sQ49_spl
<=> j(e20) = e10 ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f479,plain,
( ~ sQ49_spl
| j(e20) = e10 ),
inference(component_clause,[status(thm)],[f478]) ).
fof(f481,definition,
( sQ50_spl
<=> j(e20) = e11 ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f482,plain,
( ~ sQ50_spl
| j(e20) = e11 ),
inference(component_clause,[status(thm)],[f481]) ).
fof(f484,definition,
( sQ51_spl
<=> j(e20) = e12 ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f485,plain,
( ~ sQ51_spl
| j(e20) = e12 ),
inference(component_clause,[status(thm)],[f484]) ).
fof(f487,definition,
( sQ52_spl
<=> j(e20) = e13 ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f488,plain,
( ~ sQ52_spl
| j(e20) = e13 ),
inference(component_clause,[status(thm)],[f487]) ).
fof(f490,definition,
( sQ53_spl
<=> j(e20) = e14 ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f491,plain,
( ~ sQ53_spl
| j(e20) = e14 ),
inference(component_clause,[status(thm)],[f490]) ).
fof(f492,plain,
( sQ53_spl
| j(e20) != e14 ),
inference(component_clause,[status(thm)],[f490]) ).
fof(f493,definition,
( sQ54_spl
<=> j(e20) = e15 ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f494,plain,
( ~ sQ54_spl
| j(e20) = e15 ),
inference(component_clause,[status(thm)],[f493]) ).
fof(f495,plain,
( sQ54_spl
| j(e20) != e15 ),
inference(component_clause,[status(thm)],[f493]) ).
fof(f496,definition,
( sQ55_spl
<=> j(e20) = e16 ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f497,plain,
( ~ sQ55_spl
| j(e20) = e16 ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f500,definition,
( sQ56_spl
<=> j(e21) = e10 ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f501,plain,
( ~ sQ56_spl
| j(e21) = e10 ),
inference(component_clause,[status(thm)],[f500]) ).
fof(f503,definition,
( sQ57_spl
<=> j(e21) = e11 ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f504,plain,
( ~ sQ57_spl
| j(e21) = e11 ),
inference(component_clause,[status(thm)],[f503]) ).
fof(f506,definition,
( sQ58_spl
<=> j(e21) = e12 ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f507,plain,
( ~ sQ58_spl
| j(e21) = e12 ),
inference(component_clause,[status(thm)],[f506]) ).
fof(f509,definition,
( sQ59_spl
<=> j(e21) = e13 ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f510,plain,
( ~ sQ59_spl
| j(e21) = e13 ),
inference(component_clause,[status(thm)],[f509]) ).
fof(f512,definition,
( sQ60_spl
<=> j(e21) = e14 ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f513,plain,
( ~ sQ60_spl
| j(e21) = e14 ),
inference(component_clause,[status(thm)],[f512]) ).
fof(f515,definition,
( sQ61_spl
<=> j(e21) = e15 ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f516,plain,
( ~ sQ61_spl
| j(e21) = e15 ),
inference(component_clause,[status(thm)],[f515]) ).
fof(f518,definition,
( sQ62_spl
<=> j(e21) = e16 ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f519,plain,
( ~ sQ62_spl
| j(e21) = e16 ),
inference(component_clause,[status(thm)],[f518]) ).
fof(f521,plain,
( sQ62_spl
| sQ61_spl
| sQ60_spl
| sQ59_spl
| sQ58_spl
| sQ57_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f206,f500,f503,f506,f509,f512,f515,f518]) ).
fof(f522,definition,
( sQ63_spl
<=> j(e22) = e10 ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f523,plain,
( ~ sQ63_spl
| j(e22) = e10 ),
inference(component_clause,[status(thm)],[f522]) ).
fof(f525,definition,
( sQ64_spl
<=> j(e22) = e11 ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f526,plain,
( ~ sQ64_spl
| j(e22) = e11 ),
inference(component_clause,[status(thm)],[f525]) ).
fof(f528,definition,
( sQ65_spl
<=> j(e22) = e12 ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f529,plain,
( ~ sQ65_spl
| j(e22) = e12 ),
inference(component_clause,[status(thm)],[f528]) ).
fof(f531,definition,
( sQ66_spl
<=> j(e22) = e13 ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f532,plain,
( ~ sQ66_spl
| j(e22) = e13 ),
inference(component_clause,[status(thm)],[f531]) ).
fof(f533,plain,
( sQ66_spl
| j(e22) != e13 ),
inference(component_clause,[status(thm)],[f531]) ).
fof(f534,definition,
( sQ67_spl
<=> j(e22) = e14 ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f535,plain,
( ~ sQ67_spl
| j(e22) = e14 ),
inference(component_clause,[status(thm)],[f534]) ).
fof(f537,definition,
( sQ68_spl
<=> j(e22) = e15 ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f538,plain,
( ~ sQ68_spl
| j(e22) = e15 ),
inference(component_clause,[status(thm)],[f537]) ).
fof(f540,definition,
( sQ69_spl
<=> j(e22) = e16 ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f541,plain,
( ~ sQ69_spl
| j(e22) = e16 ),
inference(component_clause,[status(thm)],[f540]) ).
fof(f544,definition,
( sQ70_spl
<=> j(e23) = e10 ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f545,plain,
( ~ sQ70_spl
| j(e23) = e10 ),
inference(component_clause,[status(thm)],[f544]) ).
fof(f547,definition,
( sQ71_spl
<=> j(e23) = e11 ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f548,plain,
( ~ sQ71_spl
| j(e23) = e11 ),
inference(component_clause,[status(thm)],[f547]) ).
fof(f550,definition,
( sQ72_spl
<=> j(e23) = e12 ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f551,plain,
( ~ sQ72_spl
| j(e23) = e12 ),
inference(component_clause,[status(thm)],[f550]) ).
fof(f553,definition,
( sQ73_spl
<=> j(e23) = e13 ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f554,plain,
( ~ sQ73_spl
| j(e23) = e13 ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f555,plain,
( sQ73_spl
| j(e23) != e13 ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f556,definition,
( sQ74_spl
<=> j(e23) = e14 ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f557,plain,
( ~ sQ74_spl
| j(e23) = e14 ),
inference(component_clause,[status(thm)],[f556]) ).
fof(f559,definition,
( sQ75_spl
<=> j(e23) = e15 ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f560,plain,
( ~ sQ75_spl
| j(e23) = e15 ),
inference(component_clause,[status(thm)],[f559]) ).
fof(f566,definition,
( sQ77_spl
<=> j(e24) = e10 ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f567,plain,
( ~ sQ77_spl
| j(e24) = e10 ),
inference(component_clause,[status(thm)],[f566]) ).
fof(f569,definition,
( sQ78_spl
<=> j(e24) = e11 ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f570,plain,
( ~ sQ78_spl
| j(e24) = e11 ),
inference(component_clause,[status(thm)],[f569]) ).
fof(f572,definition,
( sQ79_spl
<=> j(e24) = e12 ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f573,plain,
( ~ sQ79_spl
| j(e24) = e12 ),
inference(component_clause,[status(thm)],[f572]) ).
fof(f575,definition,
( sQ80_spl
<=> j(e24) = e13 ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f576,plain,
( ~ sQ80_spl
| j(e24) = e13 ),
inference(component_clause,[status(thm)],[f575]) ).
fof(f578,definition,
( sQ81_spl
<=> j(e24) = e14 ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f579,plain,
( ~ sQ81_spl
| j(e24) = e14 ),
inference(component_clause,[status(thm)],[f578]) ).
fof(f581,definition,
( sQ82_spl
<=> j(e24) = e15 ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f582,plain,
( ~ sQ82_spl
| j(e24) = e15 ),
inference(component_clause,[status(thm)],[f581]) ).
fof(f584,definition,
( sQ83_spl
<=> j(e24) = e16 ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f585,plain,
( ~ sQ83_spl
| j(e24) = e16 ),
inference(component_clause,[status(thm)],[f584]) ).
fof(f587,plain,
( sQ83_spl
| sQ82_spl
| sQ81_spl
| sQ80_spl
| sQ79_spl
| sQ78_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f209,f566,f569,f572,f575,f578,f581,f584]) ).
fof(f588,definition,
( sQ84_spl
<=> j(e25) = e10 ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f589,plain,
( ~ sQ84_spl
| j(e25) = e10 ),
inference(component_clause,[status(thm)],[f588]) ).
fof(f591,definition,
( sQ85_spl
<=> j(e25) = e11 ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f592,plain,
( ~ sQ85_spl
| j(e25) = e11 ),
inference(component_clause,[status(thm)],[f591]) ).
fof(f594,definition,
( sQ86_spl
<=> j(e25) = e12 ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f595,plain,
( ~ sQ86_spl
| j(e25) = e12 ),
inference(component_clause,[status(thm)],[f594]) ).
fof(f596,plain,
( sQ86_spl
| j(e25) != e12 ),
inference(component_clause,[status(thm)],[f594]) ).
fof(f597,definition,
( sQ87_spl
<=> j(e25) = e13 ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f598,plain,
( ~ sQ87_spl
| j(e25) = e13 ),
inference(component_clause,[status(thm)],[f597]) ).
fof(f599,plain,
( sQ87_spl
| j(e25) != e13 ),
inference(component_clause,[status(thm)],[f597]) ).
fof(f600,definition,
( sQ88_spl
<=> j(e25) = e14 ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f601,plain,
( ~ sQ88_spl
| j(e25) = e14 ),
inference(component_clause,[status(thm)],[f600]) ).
fof(f603,definition,
( sQ89_spl
<=> j(e25) = e15 ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f604,plain,
( ~ sQ89_spl
| j(e25) = e15 ),
inference(component_clause,[status(thm)],[f603]) ).
fof(f610,definition,
( sQ91_spl
<=> j(e26) = e10 ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f611,plain,
( ~ sQ91_spl
| j(e26) = e10 ),
inference(component_clause,[status(thm)],[f610]) ).
fof(f613,definition,
( sQ92_spl
<=> j(e26) = e11 ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f614,plain,
( ~ sQ92_spl
| j(e26) = e11 ),
inference(component_clause,[status(thm)],[f613]) ).
fof(f615,plain,
( sQ92_spl
| j(e26) != e11 ),
inference(component_clause,[status(thm)],[f613]) ).
fof(f616,definition,
( sQ93_spl
<=> j(e26) = e12 ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f617,plain,
( ~ sQ93_spl
| j(e26) = e12 ),
inference(component_clause,[status(thm)],[f616]) ).
fof(f618,plain,
( sQ93_spl
| j(e26) != e12 ),
inference(component_clause,[status(thm)],[f616]) ).
fof(f619,definition,
( sQ94_spl
<=> j(e26) = e13 ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f620,plain,
( ~ sQ94_spl
| j(e26) = e13 ),
inference(component_clause,[status(thm)],[f619]) ).
fof(f625,definition,
( sQ96_spl
<=> j(e26) = e15 ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f626,plain,
( ~ sQ96_spl
| j(e26) = e15 ),
inference(component_clause,[status(thm)],[f625]) ).
fof(f627,plain,
( sQ96_spl
| j(e26) != e15 ),
inference(component_clause,[status(thm)],[f625]) ).
fof(f676,plain,
( ~ sQ85_spl
| ~ sQ88_spl
| e14 = e11 ),
inference(forward_demodulation,[status(thm)],[f601,f592]) ).
fof(f692,plain,
( ~ sQ85_spl
| ~ sQ88_spl
| e14 != e14 ),
inference(forward_demodulation,[status(thm)],[f676,f16]) ).
fof(f693,plain,
( ~ sQ85_spl
| ~ sQ88_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f692]) ).
fof(f694,plain,
( ~ sQ85_spl
| ~ sQ88_spl ),
inference(contradiction_clause,[status(thm)],[f693]) ).
fof(f695,plain,
h(e13) = op2(h(e10),h(e10)),
inference(backward_demodulation,[status(thm)],[f99,f212]) ).
fof(f710,plain,
( ~ sQ73_spl
| ~ sQ74_spl
| e14 = e13 ),
inference(forward_demodulation,[status(thm)],[f557,f554]) ).
fof(f711,plain,
( ~ sQ73_spl
| ~ sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f710,f23]) ).
fof(f712,plain,
( ~ sQ73_spl
| ~ sQ74_spl ),
inference(contradiction_clause,[status(thm)],[f711]) ).
fof(f713,plain,
h(e15) = op2(h(e10),h(e16)),
inference(forward_demodulation,[status(thm)],[f105,f218]) ).
fof(f717,plain,
( ~ sQ68_spl
| ~ sQ69_spl
| e16 = e15 ),
inference(forward_demodulation,[status(thm)],[f541,f538]) ).
fof(f718,plain,
( ~ sQ68_spl
| ~ sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f717,f28]) ).
fof(f719,plain,
( ~ sQ68_spl
| ~ sQ69_spl ),
inference(contradiction_clause,[status(thm)],[f718]) ).
fof(f720,plain,
( ~ sQ66_spl
| ~ sQ67_spl
| e14 = e13 ),
inference(forward_demodulation,[status(thm)],[f535,f532]) ).
fof(f721,plain,
( ~ sQ66_spl
| ~ sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f720,f23]) ).
fof(f722,plain,
( ~ sQ66_spl
| ~ sQ67_spl ),
inference(contradiction_clause,[status(thm)],[f721]) ).
fof(f732,plain,
( ~ sQ57_spl
| ~ sQ58_spl
| e12 = e11 ),
inference(forward_demodulation,[status(thm)],[f507,f504]) ).
fof(f733,plain,
( ~ sQ57_spl
| ~ sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f732,f14]) ).
fof(f734,plain,
( ~ sQ57_spl
| ~ sQ58_spl ),
inference(contradiction_clause,[status(thm)],[f733]) ).
fof(f735,plain,
( ~ sQ54_spl
| ~ sQ55_spl
| e16 = e15 ),
inference(forward_demodulation,[status(thm)],[f497,f494]) ).
fof(f736,plain,
( ~ sQ54_spl
| ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f735,f28]) ).
fof(f737,plain,
( ~ sQ54_spl
| ~ sQ55_spl ),
inference(contradiction_clause,[status(thm)],[f736]) ).
fof(f738,plain,
( ~ sQ52_spl
| ~ sQ53_spl
| e14 = e13 ),
inference(forward_demodulation,[status(thm)],[f491,f488]) ).
fof(f739,plain,
( ~ sQ52_spl
| ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f738,f23]) ).
fof(f740,plain,
( ~ sQ52_spl
| ~ sQ53_spl ),
inference(contradiction_clause,[status(thm)],[f739]) ).
fof(f762,plain,
( ~ sQ36_spl
| ~ sQ37_spl
| e22 = e21 ),
inference(forward_demodulation,[status(thm)],[f441,f438]) ).
fof(f763,plain,
( ~ sQ36_spl
| ~ sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f762,f35]) ).
fof(f764,plain,
( ~ sQ36_spl
| ~ sQ37_spl ),
inference(contradiction_clause,[status(thm)],[f763]) ).
fof(f777,plain,
( ~ sQ24_spl
| ~ sQ25_spl
| e24 = e23 ),
inference(forward_demodulation,[status(thm)],[f403,f400]) ).
fof(f778,plain,
( ~ sQ24_spl
| ~ sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f777,f44]) ).
fof(f779,plain,
( ~ sQ24_spl
| ~ sQ25_spl ),
inference(contradiction_clause,[status(thm)],[f778]) ).
fof(f780,plain,
h(e16) = op2(h(e11),h(e11)),
inference(forward_demodulation,[status(thm)],[f107,f220]) ).
fof(f782,plain,
( ~ sQ22_spl
| ~ sQ23_spl
| e22 = e21 ),
inference(forward_demodulation,[status(thm)],[f397,f394]) ).
fof(f783,plain,
( ~ sQ22_spl
| ~ sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f782,f35]) ).
fof(f784,plain,
( ~ sQ22_spl
| ~ sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f783]) ).
fof(f788,plain,
( ~ sQ17_spl
| ~ sQ18_spl
| e24 = e23 ),
inference(forward_demodulation,[status(thm)],[f381,f378]) ).
fof(f789,plain,
( ~ sQ17_spl
| ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f788,f44]) ).
fof(f790,plain,
( ~ sQ17_spl
| ~ sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f789]) ).
fof(f806,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| e26 = e25 ),
inference(forward_demodulation,[status(thm)],[f343,f340]) ).
fof(f807,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f806,f49]) ).
fof(f808,plain,
( ~ sQ5_spl
| ~ sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f807]) ).
fof(f812,plain,
( ~ sQ1_spl
| ~ sQ2_spl
| e22 = e21 ),
inference(forward_demodulation,[status(thm)],[f331,f328]) ).
fof(f813,plain,
( ~ sQ1_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f812,f35]) ).
fof(f814,plain,
( ~ sQ1_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f813]) ).
fof(f815,plain,
h(e11) = op2(h(e11),h(e12)),
inference(forward_demodulation,[status(thm)],[f108,f221]) ).
fof(f816,plain,
( ~ sQ7_spl
| e20 = op2(h(e11),h(e12)) ),
inference(forward_demodulation,[status(thm)],[f347,f815]) ).
fof(f817,plain,
( ~ sQ7_spl
| e20 = op2(e20,h(e12)) ),
inference(forward_demodulation,[status(thm)],[f347,f816]) ).
fof(f818,plain,
( ~ sQ7_spl
| ~ sQ14_spl
| e20 = op2(e20,e20) ),
inference(forward_demodulation,[status(thm)],[f369,f817]) ).
fof(f825,plain,
( ~ sQ87_spl
| ~ sQ84_spl
| e10 = e13 ),
inference(forward_demodulation,[status(thm)],[f589,f598]) ).
fof(f826,plain,
( ~ sQ87_spl
| ~ sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f825,f10]) ).
fof(f827,plain,
( ~ sQ87_spl
| ~ sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f826]) ).
fof(f845,plain,
h(e15) = op2(h(e11),h(e13)),
inference(forward_demodulation,[status(thm)],[f109,f222]) ).
fof(f846,plain,
( ~ sQ35_spl
| e20 = op2(h(e11),h(e13)) ),
inference(forward_demodulation,[status(thm)],[f435,f845]) ).
fof(f847,plain,
( ~ sQ35_spl
| ~ sQ7_spl
| e20 = op2(e20,h(e13)) ),
inference(forward_demodulation,[status(thm)],[f347,f846]) ).
fof(f848,plain,
( ~ sQ35_spl
| ~ sQ7_spl
| ~ sQ21_spl
| e20 = op2(e20,e20) ),
inference(forward_demodulation,[status(thm)],[f391,f847]) ).
fof(f873,plain,
h(e13) = op2(h(e11),h(e14)),
inference(forward_demodulation,[status(thm)],[f110,f223]) ).
fof(f874,plain,
( ~ sQ21_spl
| e20 = op2(h(e11),h(e14)) ),
inference(forward_demodulation,[status(thm)],[f391,f873]) ).
fof(f877,plain,
( ~ sQ7_spl
| ~ sQ14_spl
| e20 = e22 ),
inference(forward_demodulation,[status(thm)],[f818,f148]) ).
fof(f878,plain,
( ~ sQ7_spl
| ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f877,f30]) ).
fof(f879,plain,
( ~ sQ7_spl
| ~ sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f878]) ).
fof(f880,plain,
( ~ sQ91_spl
| ~ sQ96_spl
| e15 = e10 ),
inference(forward_demodulation,[status(thm)],[f626,f611]) ).
fof(f881,plain,
( ~ sQ91_spl
| ~ sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f880,f12]) ).
fof(f882,plain,
( ~ sQ91_spl
| ~ sQ96_spl ),
inference(contradiction_clause,[status(thm)],[f881]) ).
fof(f883,plain,
( ~ sQ1_spl
| ~ sQ0_spl
| e20 = e21 ),
inference(forward_demodulation,[status(thm)],[f325,f328]) ).
fof(f884,plain,
( ~ sQ1_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f883,f29]) ).
fof(f885,plain,
( ~ sQ1_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f884]) ).
fof(f886,plain,
( ~ sQ3_spl
| ~ sQ0_spl
| e20 = e23 ),
inference(forward_demodulation,[status(thm)],[f325,f334]) ).
fof(f887,plain,
( ~ sQ3_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f886,f31]) ).
fof(f888,plain,
( ~ sQ3_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f887]) ).
fof(f893,plain,
( ~ sQ21_spl
| ~ sQ28_spl
| e20 = op2(h(e11),e20) ),
inference(forward_demodulation,[status(thm)],[f413,f874]) ).
fof(f899,plain,
( ~ sQ4_spl
| ~ sQ2_spl
| e22 = e24 ),
inference(forward_demodulation,[status(thm)],[f331,f337]) ).
fof(f900,plain,
( ~ sQ4_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f899,f41]) ).
fof(f901,plain,
( ~ sQ4_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f900]) ).
fof(f905,plain,
h(e14) = op2(h(e11),h(e15)),
inference(forward_demodulation,[status(thm)],[f111,f224]) ).
fof(f918,plain,
( ~ sQ49_spl
| h(e10) = e20 ),
inference(forward_demodulation,[status(thm)],[f479,f310]) ).
fof(f922,plain,
( ~ sQ49_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f918,f324,f478]) ).
fof(f926,plain,
( ~ sQ15_spl
| ~ sQ14_spl
| e20 = e21 ),
inference(forward_demodulation,[status(thm)],[f369,f372]) ).
fof(f927,plain,
( ~ sQ15_spl
| ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f926,f29]) ).
fof(f928,plain,
( ~ sQ15_spl
| ~ sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f927]) ).
fof(f929,plain,
( ~ sQ22_spl
| ~ sQ21_spl
| e20 = e21 ),
inference(forward_demodulation,[status(thm)],[f391,f394]) ).
fof(f930,plain,
( ~ sQ22_spl
| ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f929,f29]) ).
fof(f931,plain,
( ~ sQ22_spl
| ~ sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f930]) ).
fof(f932,plain,
( ~ sQ24_spl
| ~ sQ21_spl
| e20 = e23 ),
inference(forward_demodulation,[status(thm)],[f391,f400]) ).
fof(f933,plain,
( ~ sQ24_spl
| ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f932,f31]) ).
fof(f934,plain,
( ~ sQ24_spl
| ~ sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f933]) ).
fof(f935,plain,
( ~ sQ29_spl
| ~ sQ28_spl
| e20 = e21 ),
inference(forward_demodulation,[status(thm)],[f413,f416]) ).
fof(f936,plain,
( ~ sQ29_spl
| ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f935,f29]) ).
fof(f937,plain,
( ~ sQ29_spl
| ~ sQ28_spl ),
inference(contradiction_clause,[status(thm)],[f936]) ).
fof(f938,plain,
( ~ sQ31_spl
| ~ sQ28_spl
| e20 = e23 ),
inference(forward_demodulation,[status(thm)],[f413,f422]) ).
fof(f939,plain,
( ~ sQ31_spl
| ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f938,f31]) ).
fof(f940,plain,
( ~ sQ31_spl
| ~ sQ28_spl ),
inference(contradiction_clause,[status(thm)],[f939]) ).
fof(f941,plain,
( ~ sQ36_spl
| ~ sQ35_spl
| e20 = e21 ),
inference(forward_demodulation,[status(thm)],[f435,f438]) ).
fof(f942,plain,
( ~ sQ36_spl
| ~ sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f941,f29]) ).
fof(f943,plain,
( ~ sQ36_spl
| ~ sQ35_spl ),
inference(contradiction_clause,[status(thm)],[f942]) ).
fof(f944,plain,
( ~ sQ38_spl
| ~ sQ35_spl
| e20 = e23 ),
inference(forward_demodulation,[status(thm)],[f435,f444]) ).
fof(f945,plain,
( ~ sQ38_spl
| ~ sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f944,f31]) ).
fof(f946,plain,
( ~ sQ38_spl
| ~ sQ35_spl ),
inference(contradiction_clause,[status(thm)],[f945]) ).
fof(f953,plain,
h(e12) = op2(h(e11),h(e16)),
inference(forward_demodulation,[status(thm)],[f112,f225]) ).
fof(f959,plain,
( ~ sQ5_spl
| ~ sQ0_spl
| e20 = e25 ),
inference(forward_demodulation,[status(thm)],[f325,f340]) ).
fof(f960,plain,
( ~ sQ5_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f959,f33]) ).
fof(f961,plain,
( ~ sQ5_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f960]) ).
fof(f978,plain,
( ~ sQ47_spl
| h(e12) = op2(h(e11),e25) ),
inference(forward_demodulation,[status(thm)],[f472,f953]) ).
fof(f979,plain,
h(e16) = op2(h(e12),h(e10)),
inference(forward_demodulation,[status(thm)],[f113,f226]) ).
fof(f997,plain,
( ~ sQ37_spl
| ~ sQ40_spl
| e25 = e22 ),
inference(forward_demodulation,[status(thm)],[f450,f441]) ).
fof(f998,plain,
( ~ sQ37_spl
| ~ sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f997,f42]) ).
fof(f999,plain,
( ~ sQ37_spl
| ~ sQ40_spl ),
inference(contradiction_clause,[status(thm)],[f998]) ).
fof(f1024,plain,
( ~ sQ18_spl
| ~ sQ16_spl
| e22 = e24 ),
inference(forward_demodulation,[status(thm)],[f375,f381]) ).
fof(f1025,plain,
( ~ sQ18_spl
| ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1024,f41]) ).
fof(f1026,plain,
( ~ sQ18_spl
| ~ sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f1025]) ).
fof(f1050,plain,
( ~ sQ34_spl
| ~ sQ32_spl
| e24 = e26 ),
inference(forward_demodulation,[status(thm)],[f425,f431]) ).
fof(f1051,plain,
( ~ sQ34_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1050,f48]) ).
fof(f1052,plain,
( ~ sQ34_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f1051]) ).
fof(f1054,plain,
h(e15) = op2(h(e12),h(e12)),
inference(forward_demodulation,[status(thm)],[f115,f228]) ).
fof(f1058,plain,
( ~ sQ41_spl
| ~ sQ39_spl
| e24 = e26 ),
inference(forward_demodulation,[status(thm)],[f447,f453]) ).
fof(f1059,plain,
( ~ sQ41_spl
| ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1058,f48]) ).
fof(f1060,plain,
( ~ sQ41_spl
| ~ sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f1059]) ).
fof(f1124,plain,
h(e14) = op2(h(e12),h(e16)),
inference(forward_demodulation,[status(thm)],[f119,f232]) ).
fof(f1125,plain,
( ~ sQ43_spl
| h(e14) = op2(h(e12),e21) ),
inference(forward_demodulation,[status(thm)],[f460,f1124]) ).
fof(f1128,plain,
( ~ sQ43_spl
| ~ sQ14_spl
| h(e14) = op2(e20,e21) ),
inference(backward_demodulation,[status(thm)],[f369,f1125]) ).
fof(f1135,plain,
( ~ sQ43_spl
| ~ sQ14_spl
| h(e14) = e20 ),
inference(forward_demodulation,[status(thm)],[f149,f1128]) ).
fof(f1138,plain,
h(e12) = op2(h(e13),h(e12)),
inference(forward_demodulation,[status(thm)],[f122,f235]) ).
fof(f1139,plain,
( ~ sQ14_spl
| e20 = op2(h(e13),h(e12)) ),
inference(forward_demodulation,[status(thm)],[f369,f1138]) ).
fof(f1140,plain,
( ~ sQ14_spl
| e20 = op2(h(e13),e20) ),
inference(forward_demodulation,[status(thm)],[f369,f1139]) ).
fof(f1141,plain,
h(e14) = op2(h(e13),h(e13)),
inference(forward_demodulation,[status(thm)],[f123,f236]) ).
fof(f1178,plain,
h(e10) = op2(h(e13),h(e15)),
inference(forward_demodulation,[status(thm)],[f125,f238]) ).
fof(f1179,plain,
( ~ sQ37_spl
| h(e10) = op2(h(e13),e22) ),
inference(forward_demodulation,[status(thm)],[f441,f1178]) ).
fof(f1180,plain,
h(e13) = op2(h(e13),h(e16)),
inference(forward_demodulation,[status(thm)],[f126,f239]) ).
fof(f1207,plain,
h(e12) = op2(h(e14),h(e14)),
inference(forward_demodulation,[status(thm)],[f131,f244]) ).
fof(f1209,plain,
h(e15) = op2(h(e14),h(e15)),
inference(forward_demodulation,[status(thm)],[f132,f245]) ).
fof(f1210,plain,
( ~ sQ37_spl
| e22 = op2(h(e14),h(e15)) ),
inference(forward_demodulation,[status(thm)],[f441,f1209]) ).
fof(f1211,plain,
( ~ sQ37_spl
| e22 = op2(h(e14),e22) ),
inference(forward_demodulation,[status(thm)],[f441,f1210]) ).
fof(f1214,plain,
h(e12) = op2(h(e15),h(e10)),
inference(forward_demodulation,[status(thm)],[f134,f247]) ).
fof(f1215,plain,
( ~ sQ19_spl
| e25 = op2(h(e15),h(e10)) ),
inference(forward_demodulation,[status(thm)],[f384,f1214]) ).
fof(f1216,plain,
( ~ sQ19_spl
| ~ sQ37_spl
| e25 = op2(e22,h(e10)) ),
inference(forward_demodulation,[status(thm)],[f441,f1215]) ).
fof(f1217,plain,
( ~ sQ19_spl
| ~ sQ37_spl
| ~ sQ2_spl
| e25 = op2(e22,e22) ),
inference(forward_demodulation,[status(thm)],[f331,f1216]) ).
fof(f1218,plain,
( ~ sQ19_spl
| ~ sQ37_spl
| ~ sQ2_spl
| e25 = e23 ),
inference(forward_demodulation,[status(thm)],[f164,f1217]) ).
fof(f1219,plain,
( ~ sQ19_spl
| ~ sQ37_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1218,f45]) ).
fof(f1220,plain,
( ~ sQ19_spl
| ~ sQ37_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1219]) ).
fof(f1221,plain,
h(e14) = op2(h(e15),h(e11)),
inference(forward_demodulation,[status(thm)],[f135,f248]) ).
fof(f1222,plain,
( ~ sQ9_spl
| h(e14) = op2(h(e15),e22) ),
inference(forward_demodulation,[status(thm)],[f353,f1221]) ).
fof(f1252,plain,
h(e11) = op2(h(e15),h(e15)),
inference(forward_demodulation,[status(thm)],[f139,f252]) ).
fof(f1253,plain,
( ~ sQ9_spl
| e22 = op2(h(e15),h(e15)) ),
inference(forward_demodulation,[status(thm)],[f353,f1252]) ).
fof(f1254,plain,
h(e16) = op2(h(e15),h(e16)),
inference(forward_demodulation,[status(thm)],[f140,f253]) ).
fof(f1257,plain,
h(e15) = op2(h(e16),h(e10)),
inference(forward_demodulation,[status(thm)],[f141,f254]) ).
fof(f1258,plain,
( ~ sQ44_spl
| h(e15) = op2(e22,h(e10)) ),
inference(forward_demodulation,[status(thm)],[f463,f1257]) ).
fof(f1259,plain,
( ~ sQ44_spl
| ~ sQ3_spl
| h(e15) = op2(e22,e23) ),
inference(backward_demodulation,[status(thm)],[f334,f1258]) ).
fof(f1267,plain,
( ~ sQ44_spl
| ~ sQ3_spl
| h(e15) = e26 ),
inference(forward_demodulation,[status(thm)],[f165,f1259]) ).
fof(f1268,plain,
( ~ sQ44_spl
| ~ sQ3_spl
| sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1267,f454]) ).
fof(f1269,plain,
( ~ sQ44_spl
| ~ sQ3_spl
| sQ41_spl ),
inference(contradiction_clause,[status(thm)],[f1268]) ).
fof(f1282,plain,
( ~ sQ21_spl
| ~ sQ28_spl
| ~ sQ9_spl
| e20 = op2(e22,e20) ),
inference(forward_demodulation,[status(thm)],[f353,f893]) ).
fof(f1283,plain,
( ~ sQ21_spl
| ~ sQ28_spl
| ~ sQ9_spl
| e20 = e21 ),
inference(forward_demodulation,[status(thm)],[f162,f1282]) ).
fof(f1284,plain,
( ~ sQ21_spl
| ~ sQ28_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1283,f29]) ).
fof(f1285,plain,
( ~ sQ21_spl
| ~ sQ28_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f1284]) ).
fof(f1293,plain,
h(e13) = op2(h(e16),h(e13)),
inference(forward_demodulation,[status(thm)],[f144,f257]) ).
fof(f1317,plain,
h(e10) = op2(h(e16),h(e16)),
inference(forward_demodulation,[status(thm)],[f147,f260]) ).
fof(f1330,plain,
( ~ sQ50_spl
| j(op2(e20,e20)) = op1(e11,j(e20)) ),
inference(forward_demodulation,[status(thm)],[f482,f261]) ).
fof(f1331,plain,
( ~ sQ50_spl
| j(op2(e20,e20)) = op1(e11,e11) ),
inference(forward_demodulation,[status(thm)],[f482,f1330]) ).
fof(f1332,plain,
( ~ sQ50_spl
| j(op2(e20,e20)) = e16 ),
inference(forward_demodulation,[status(thm)],[f107,f1331]) ).
fof(f1341,plain,
j(e21) = op1(j(e20),j(e22)),
inference(forward_demodulation,[status(thm)],[f150,f263]) ).
fof(f1342,plain,
( ~ sQ56_spl
| e10 = op1(j(e20),j(e22)) ),
inference(forward_demodulation,[status(thm)],[f501,f1341]) ).
fof(f1364,plain,
j(e23) = op1(j(e20),j(e24)),
inference(forward_demodulation,[status(thm)],[f152,f265]) ).
fof(f1375,plain,
j(e26) = op1(j(e20),j(e26)),
inference(forward_demodulation,[status(thm)],[f154,f267]) ).
fof(f1376,plain,
( ~ sQ96_spl
| e15 = op1(j(e20),j(e26)) ),
inference(forward_demodulation,[status(thm)],[f626,f1375]) ).
fof(f1377,plain,
( ~ sQ96_spl
| e15 = op1(j(e20),e15) ),
inference(forward_demodulation,[status(thm)],[f626,f1376]) ).
fof(f1379,plain,
j(e26) = op1(j(e21),j(e21)),
inference(forward_demodulation,[status(thm)],[f156,f269]) ).
fof(f1380,plain,
( ~ sQ96_spl
| e15 = op1(j(e21),j(e21)) ),
inference(forward_demodulation,[status(thm)],[f626,f1379]) ).
fof(f1407,plain,
( ~ sQ96_spl
| ~ sQ51_spl
| e15 = op1(e12,e15) ),
inference(backward_demodulation,[status(thm)],[f485,f1377]) ).
fof(f1411,plain,
( ~ sQ96_spl
| ~ sQ51_spl
| e15 = e13 ),
inference(forward_demodulation,[status(thm)],[f118,f1407]) ).
fof(f1412,plain,
( ~ sQ96_spl
| ~ sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1411,f24]) ).
fof(f1413,plain,
( ~ sQ96_spl
| ~ sQ51_spl ),
inference(contradiction_clause,[status(thm)],[f1412]) ).
fof(f1414,plain,
( ~ sQ64_spl
| ~ sQ63_spl
| e10 = e11 ),
inference(forward_demodulation,[status(thm)],[f523,f526]) ).
fof(f1415,plain,
( ~ sQ64_spl
| ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1414,f8]) ).
fof(f1416,plain,
( ~ sQ64_spl
| ~ sQ63_spl ),
inference(contradiction_clause,[status(thm)],[f1415]) ).
fof(f1417,plain,
( ~ sQ71_spl
| ~ sQ70_spl
| e10 = e11 ),
inference(forward_demodulation,[status(thm)],[f545,f548]) ).
fof(f1418,plain,
( ~ sQ71_spl
| ~ sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1417,f8]) ).
fof(f1419,plain,
( ~ sQ71_spl
| ~ sQ70_spl ),
inference(contradiction_clause,[status(thm)],[f1418]) ).
fof(f1427,plain,
j(e25) = op1(j(e21),j(e24)),
inference(forward_demodulation,[status(thm)],[f159,f272]) ).
fof(f1442,plain,
j(e22) = op1(j(e21),j(e25)),
inference(forward_demodulation,[status(thm)],[f160,f273]) ).
fof(f1443,plain,
( ~ sQ57_spl
| j(e22) = op1(e11,j(e25)) ),
inference(forward_demodulation,[status(thm)],[f504,f1442]) ).
fof(f1444,plain,
( ~ sQ57_spl
| ~ sQ84_spl
| j(e22) = op1(e11,e10) ),
inference(forward_demodulation,[status(thm)],[f589,f1443]) ).
fof(f1445,plain,
( ~ sQ57_spl
| ~ sQ84_spl
| j(e22) = e10 ),
inference(forward_demodulation,[status(thm)],[f106,f1444]) ).
fof(f1446,plain,
j(e23) = op1(j(e21),j(e26)),
inference(forward_demodulation,[status(thm)],[f161,f274]) ).
fof(f1451,plain,
j(e24) = op1(j(e22),j(e21)),
inference(forward_demodulation,[status(thm)],[f163,f276]) ).
fof(f1452,plain,
( ~ sQ57_spl
| ~ sQ84_spl
| j(e24) = op1(e10,j(e21)) ),
inference(forward_demodulation,[status(thm)],[f1445,f1451]) ).
fof(f1453,plain,
( ~ sQ57_spl
| ~ sQ84_spl
| j(e24) = op1(e10,e11) ),
inference(forward_demodulation,[status(thm)],[f504,f1452]) ).
fof(f1454,plain,
( ~ sQ57_spl
| ~ sQ84_spl
| j(e24) = e10 ),
inference(forward_demodulation,[status(thm)],[f100,f1453]) ).
fof(f1459,plain,
( ~ sQ68_spl
| ~ sQ66_spl
| e13 = e15 ),
inference(forward_demodulation,[status(thm)],[f532,f538]) ).
fof(f1460,plain,
( ~ sQ68_spl
| ~ sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1459,f24]) ).
fof(f1461,plain,
( ~ sQ68_spl
| ~ sQ66_spl ),
inference(contradiction_clause,[status(thm)],[f1460]) ).
fof(f1462,plain,
j(e23) = op1(j(e22),j(e22)),
inference(forward_demodulation,[status(thm)],[f164,f277]) ).
fof(f1463,plain,
( ~ sQ73_spl
| e13 = op1(j(e22),j(e22)) ),
inference(forward_demodulation,[status(thm)],[f554,f1462]) ).
fof(f1466,plain,
( ~ sQ75_spl
| ~ sQ73_spl
| e13 = e15 ),
inference(forward_demodulation,[status(thm)],[f554,f560]) ).
fof(f1467,plain,
( ~ sQ75_spl
| ~ sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1466,f24]) ).
fof(f1468,plain,
( ~ sQ75_spl
| ~ sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f1467]) ).
fof(f1469,plain,
( ~ sQ86_spl
| ~ sQ84_spl
| e10 = e12 ),
inference(forward_demodulation,[status(thm)],[f589,f595]) ).
fof(f1470,plain,
( ~ sQ86_spl
| ~ sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1469,f9]) ).
fof(f1471,plain,
( ~ sQ86_spl
| ~ sQ84_spl ),
inference(contradiction_clause,[status(thm)],[f1470]) ).
fof(f1485,plain,
j(e20) = op1(j(e22),j(e24)),
inference(forward_demodulation,[status(thm)],[f166,f279]) ).
fof(f1492,plain,
j(e25) = op1(j(e22),j(e25)),
inference(forward_demodulation,[status(thm)],[f167,f280]) ).
fof(f1499,plain,
( ~ sQ82_spl
| j(e20) = op1(j(e22),e15) ),
inference(forward_demodulation,[status(thm)],[f582,f1485]) ).
fof(f1500,plain,
j(e22) = op1(j(e22),j(e26)),
inference(forward_demodulation,[status(thm)],[f168,f281]) ).
fof(f1501,plain,
( ~ sQ92_spl
| j(e22) = op1(j(e22),e11) ),
inference(forward_demodulation,[status(thm)],[f614,f1500]) ).
fof(f1502,plain,
( ~ sQ79_spl
| ~ sQ82_spl
| e15 = e12 ),
inference(forward_demodulation,[status(thm)],[f582,f573]) ).
fof(f1503,plain,
( ~ sQ79_spl
| ~ sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1502,f21]) ).
fof(f1504,plain,
( ~ sQ79_spl
| ~ sQ82_spl ),
inference(contradiction_clause,[status(thm)],[f1503]) ).
fof(f1507,plain,
j(e25) = op1(j(e23),j(e20)),
inference(forward_demodulation,[status(thm)],[f169,f282]) ).
fof(f1508,plain,
( ~ sQ72_spl
| j(e25) = op1(e12,j(e20)) ),
inference(forward_demodulation,[status(thm)],[f551,f1507]) ).
fof(f1511,plain,
( ~ sQ72_spl
| ~ sQ53_spl
| j(e25) = op1(e12,e14) ),
inference(backward_demodulation,[status(thm)],[f491,f1508]) ).
fof(f1512,plain,
( ~ sQ72_spl
| ~ sQ53_spl
| j(e25) = e10 ),
inference(forward_demodulation,[status(thm)],[f117,f1511]) ).
fof(f1513,plain,
( ~ sQ55_spl
| ~ sQ53_spl
| e14 = e16 ),
inference(forward_demodulation,[status(thm)],[f491,f497]) ).
fof(f1514,plain,
( ~ sQ55_spl
| ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1513,f27]) ).
fof(f1515,plain,
( ~ sQ55_spl
| ~ sQ53_spl ),
inference(contradiction_clause,[status(thm)],[f1514]) ).
fof(f1528,plain,
j(e26) = op1(j(e23),j(e22)),
inference(forward_demodulation,[status(thm)],[f171,f284]) ).
fof(f1529,plain,
( ~ sQ92_spl
| e11 = op1(j(e23),j(e22)) ),
inference(forward_demodulation,[status(thm)],[f614,f1528]) ).
fof(f1530,plain,
( ~ sQ60_spl
| ~ sQ58_spl
| e12 = e14 ),
inference(forward_demodulation,[status(thm)],[f507,f513]) ).
fof(f1531,plain,
( ~ sQ60_spl
| ~ sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1530,f20]) ).
fof(f1532,plain,
( ~ sQ60_spl
| ~ sQ58_spl ),
inference(contradiction_clause,[status(thm)],[f1531]) ).
fof(f1543,plain,
j(e20) = op1(j(e23),j(e23)),
inference(forward_demodulation,[status(thm)],[f172,f285]) ).
fof(f1544,plain,
( ~ sQ74_spl
| j(e20) = op1(e14,j(e23)) ),
inference(forward_demodulation,[status(thm)],[f557,f1543]) ).
fof(f1545,plain,
( ~ sQ74_spl
| j(e20) = op1(e14,e14) ),
inference(forward_demodulation,[status(thm)],[f557,f1544]) ).
fof(f1546,plain,
( ~ sQ74_spl
| j(e20) = e12 ),
inference(forward_demodulation,[status(thm)],[f131,f1545]) ).
fof(f1570,plain,
j(e25) = op1(j(e24),j(e21)),
inference(forward_demodulation,[status(thm)],[f177,f290]) ).
fof(f1592,plain,
j(e24) = op1(j(e24),j(e24)),
inference(forward_demodulation,[status(thm)],[f180,f293]) ).
fof(f1593,plain,
( ~ sQ81_spl
| e14 = op1(j(e24),j(e24)) ),
inference(forward_demodulation,[status(thm)],[f579,f1592]) ).
fof(f1594,plain,
( ~ sQ81_spl
| e14 = op1(e14,j(e24)) ),
inference(forward_demodulation,[status(thm)],[f579,f1593]) ).
fof(f1595,plain,
( ~ sQ81_spl
| e14 = op1(e14,e14) ),
inference(forward_demodulation,[status(thm)],[f579,f1594]) ).
fof(f1596,plain,
( ~ sQ81_spl
| e14 = e12 ),
inference(forward_demodulation,[status(thm)],[f131,f1595]) ).
fof(f1597,plain,
( ~ sQ81_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1596,f20]) ).
fof(f1598,plain,
~ sQ81_spl,
inference(contradiction_clause,[status(thm)],[f1597]) ).
fof(f1607,plain,
j(e26) = op1(j(e24),j(e25)),
inference(forward_demodulation,[status(thm)],[f181,f294]) ).
fof(f1610,plain,
( ~ sQ93_spl
| e12 = op1(j(e24),j(e25)) ),
inference(backward_demodulation,[status(thm)],[f617,f1607]) ).
fof(f1657,plain,
j(e26) = op1(j(e25),j(e24)),
inference(forward_demodulation,[status(thm)],[f187,f300]) ).
fof(f1658,plain,
j(e21) = op1(j(e25),j(e25)),
inference(forward_demodulation,[status(thm)],[f188,f301]) ).
fof(f1672,plain,
( ~ sQ80_spl
| j(e26) = op1(j(e25),e13) ),
inference(backward_demodulation,[status(thm)],[f576,f1657]) ).
fof(f1683,plain,
j(e23) = op1(j(e26),j(e21)),
inference(forward_demodulation,[status(thm)],[f191,f304]) ).
fof(f1698,plain,
j(e22) = op1(j(e26),j(e22)),
inference(forward_demodulation,[status(thm)],[f192,f305]) ).
fof(f1699,plain,
( ~ sQ63_spl
| j(e22) = op1(j(e26),e10) ),
inference(backward_demodulation,[status(thm)],[f523,f1698]) ).
fof(f1705,plain,
( ~ sQ63_spl
| e10 = op1(j(e26),e10) ),
inference(forward_demodulation,[status(thm)],[f523,f1699]) ).
fof(f1734,plain,
j(e25) = op1(j(e26),j(e26)),
inference(forward_demodulation,[status(thm)],[f196,f309]) ).
fof(f1741,plain,
( ~ sQ92_spl
| ~ sQ70_spl
| e11 = op1(e10,j(e22)) ),
inference(forward_demodulation,[status(thm)],[f545,f1529]) ).
fof(f1742,plain,
( ~ sQ92_spl
| ~ sQ70_spl
| ~ sQ63_spl
| e11 = op1(e10,e10) ),
inference(forward_demodulation,[status(thm)],[f523,f1741]) ).
fof(f1743,plain,
( ~ sQ92_spl
| ~ sQ70_spl
| ~ sQ63_spl
| e11 = e13 ),
inference(forward_demodulation,[status(thm)],[f99,f1742]) ).
fof(f1744,plain,
( ~ sQ92_spl
| ~ sQ70_spl
| ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1743,f15]) ).
fof(f1745,plain,
( ~ sQ92_spl
| ~ sQ70_spl
| ~ sQ63_spl ),
inference(contradiction_clause,[status(thm)],[f1744]) ).
fof(f1746,plain,
( ~ sQ57_spl
| h(e11) = e21 ),
inference(forward_demodulation,[status(thm)],[f504,f311]) ).
fof(f1750,plain,
( ~ sQ63_spl
| h(e10) = e22 ),
inference(forward_demodulation,[status(thm)],[f523,f312]) ).
fof(f1751,plain,
( ~ sQ63_spl
| ~ sQ0_spl
| e20 = e22 ),
inference(forward_demodulation,[status(thm)],[f325,f1750]) ).
fof(f1752,plain,
( ~ sQ63_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1751,f30]) ).
fof(f1753,plain,
( ~ sQ63_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f1752]) ).
fof(f1754,plain,
( ~ sQ63_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1750,f330,f522]) ).
fof(f1771,plain,
( ~ sQ79_spl
| h(e12) = e24 ),
inference(forward_demodulation,[status(thm)],[f573,f314]) ).
fof(f1785,plain,
( ~ sQ18_spl
| j(e24) = e12 ),
inference(forward_demodulation,[status(thm)],[f381,f319]) ).
fof(f1786,plain,
( ~ sQ23_spl
| j(e22) = e13 ),
inference(forward_demodulation,[status(thm)],[f397,f320]) ).
fof(f1793,plain,
( ~ sQ11_spl
| j(e24) = e11 ),
inference(backward_demodulation,[status(thm)],[f359,f318]) ).
fof(f1794,plain,
( ~ sQ11_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f1793,f569,f358]) ).
fof(f1795,plain,
( ~ sQ18_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f1785,f572,f380]) ).
fof(f1800,plain,
( ~ sQ79_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1771,f380,f572]) ).
fof(f1810,plain,
( sQ66_spl
| ~ sQ23_spl
| e13 != e13 ),
inference(forward_demodulation,[status(thm)],[f1786,f533]) ).
fof(f1811,plain,
( sQ66_spl
| ~ sQ23_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1810]) ).
fof(f1812,plain,
( sQ66_spl
| ~ sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f1811]) ).
fof(f1813,plain,
( ~ sQ36_spl
| j(e21) = e15 ),
inference(forward_demodulation,[status(thm)],[f438,f322]) ).
fof(f1814,plain,
( ~ sQ36_spl
| ~ sQ58_spl
| e12 = e15 ),
inference(forward_demodulation,[status(thm)],[f507,f1813]) ).
fof(f1815,plain,
( ~ sQ36_spl
| ~ sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1814,f21]) ).
fof(f1816,plain,
( ~ sQ36_spl
| ~ sQ58_spl ),
inference(contradiction_clause,[status(thm)],[f1815]) ).
fof(f1821,plain,
( ~ sQ42_spl
| j(e20) = e16 ),
inference(forward_demodulation,[status(thm)],[f457,f323]) ).
fof(f1825,plain,
h(e16) = op2(h(e10),h(e12)),
inference(forward_demodulation,[status(thm)],[f101,f214]) ).
fof(f1830,plain,
( ~ sQ70_spl
| h(e10) = e23 ),
inference(backward_demodulation,[status(thm)],[f545,f313]) ).
fof(f1831,plain,
( ~ sQ70_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1830,f333,f544]) ).
fof(f1837,plain,
( ~ sQ28_spl
| j(e20) = e14 ),
inference(backward_demodulation,[status(thm)],[f413,f321]) ).
fof(f1838,plain,
( ~ sQ28_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f1837,f490,f412]) ).
fof(f1839,plain,
h(e10) = op2(h(e10),h(e11)),
inference(forward_demodulation,[status(thm)],[f100,f213]) ).
fof(f1854,plain,
( ~ sQ12_spl
| h(e10) = op2(h(e10),e25) ),
inference(backward_demodulation,[status(thm)],[f362,f1839]) ).
fof(f1857,plain,
( ~ sQ12_spl
| e25 = op2(h(e11),h(e12)) ),
inference(forward_demodulation,[status(thm)],[f362,f815]) ).
fof(f1858,plain,
( ~ sQ12_spl
| e25 = op2(e25,h(e12)) ),
inference(forward_demodulation,[status(thm)],[f362,f1857]) ).
fof(f1865,plain,
( ~ sQ25_spl
| e24 = op2(h(e10),h(e10)) ),
inference(backward_demodulation,[status(thm)],[f403,f695]) ).
fof(f1871,plain,
( ~ sQ12_spl
| ~ sQ19_spl
| e25 = op2(e25,e25) ),
inference(backward_demodulation,[status(thm)],[f384,f1858]) ).
fof(f1878,plain,
( ~ sQ12_spl
| ~ sQ19_spl
| e25 = e21 ),
inference(forward_demodulation,[status(thm)],[f188,f1871]) ).
fof(f1879,plain,
( ~ sQ12_spl
| ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1878,f38]) ).
fof(f1880,plain,
( ~ sQ12_spl
| ~ sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f1879]) ).
fof(f1881,plain,
( ~ sQ43_spl
| ~ sQ14_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f1135,f412,f368,f459]) ).
fof(f1882,plain,
( ~ sQ14_spl
| ~ sQ25_spl
| e20 = op2(e24,e20) ),
inference(forward_demodulation,[status(thm)],[f403,f1140]) ).
fof(f1883,plain,
( ~ sQ14_spl
| ~ sQ25_spl
| e20 = e23 ),
inference(forward_demodulation,[status(thm)],[f176,f1882]) ).
fof(f1884,plain,
( ~ sQ14_spl
| ~ sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1883,f31]) ).
fof(f1885,plain,
( ~ sQ14_spl
| ~ sQ25_spl ),
inference(contradiction_clause,[status(thm)],[f1884]) ).
fof(f1886,plain,
( ~ sQ42_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f1821,f496,f456]) ).
fof(f1906,plain,
( ~ sQ3_spl
| j(e23) = e10 ),
inference(backward_demodulation,[status(thm)],[f334,f317]) ).
fof(f1907,plain,
( ~ sQ3_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f1906,f544,f333]) ).
fof(f1927,plain,
( ~ sQ8_spl
| h(e16) = op2(h(e11),e21) ),
inference(backward_demodulation,[status(thm)],[f350,f780]) ).
fof(f1930,plain,
( ~ sQ8_spl
| h(e16) = op2(e21,e21) ),
inference(forward_demodulation,[status(thm)],[f350,f1927]) ).
fof(f1931,plain,
( ~ sQ8_spl
| h(e16) = e26 ),
inference(forward_demodulation,[status(thm)],[f156,f1930]) ).
fof(f1936,plain,
( ~ sQ9_spl
| ~ sQ35_spl
| h(e14) = op2(e20,e22) ),
inference(forward_demodulation,[status(thm)],[f435,f1222]) ).
fof(f1937,plain,
( ~ sQ9_spl
| ~ sQ35_spl
| h(e14) = e21 ),
inference(forward_demodulation,[status(thm)],[f150,f1936]) ).
fof(f1938,plain,
( ~ sQ9_spl
| ~ sQ35_spl
| sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1937,f417]) ).
fof(f1939,plain,
( ~ sQ9_spl
| ~ sQ35_spl
| sQ29_spl ),
inference(contradiction_clause,[status(thm)],[f1938]) ).
fof(f1944,plain,
( ~ sQ36_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f1813,f515,f437]) ).
fof(f1962,plain,
( ~ sQ22_spl
| h(e14) = op2(e21,h(e13)) ),
inference(forward_demodulation,[status(thm)],[f394,f1141]) ).
fof(f1963,plain,
( ~ sQ22_spl
| h(e14) = op2(e21,e21) ),
inference(forward_demodulation,[status(thm)],[f394,f1962]) ).
fof(f1964,plain,
( ~ sQ22_spl
| h(e14) = e26 ),
inference(forward_demodulation,[status(thm)],[f156,f1963]) ).
fof(f1965,plain,
( ~ sQ22_spl
| sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1964,f432]) ).
fof(f1966,plain,
( ~ sQ22_spl
| sQ34_spl ),
inference(contradiction_clause,[status(thm)],[f1965]) ).
fof(f1967,plain,
( ~ sQ18_spl
| e24 = op2(h(e13),h(e12)) ),
inference(forward_demodulation,[status(thm)],[f381,f1138]) ).
fof(f1968,plain,
( ~ sQ18_spl
| e24 = op2(h(e13),e24) ),
inference(forward_demodulation,[status(thm)],[f381,f1967]) ).
fof(f1992,plain,
( ~ sQ80_spl
| ~ sQ84_spl
| j(e26) = op1(e10,e13) ),
inference(forward_demodulation,[status(thm)],[f589,f1672]) ).
fof(f1993,plain,
( ~ sQ80_spl
| ~ sQ84_spl
| j(e26) = e11 ),
inference(forward_demodulation,[status(thm)],[f102,f1992]) ).
fof(f1994,plain,
( ~ sQ80_spl
| ~ sQ84_spl
| sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1993,f615]) ).
fof(f1995,plain,
( ~ sQ80_spl
| ~ sQ84_spl
| sQ92_spl ),
inference(contradiction_clause,[status(thm)],[f1994]) ).
fof(f1996,plain,
( ~ sQ96_spl
| ~ sQ56_spl
| e15 = op1(e10,j(e21)) ),
inference(forward_demodulation,[status(thm)],[f501,f1380]) ).
fof(f1997,plain,
( ~ sQ96_spl
| ~ sQ56_spl
| e15 = op1(e10,e10) ),
inference(forward_demodulation,[status(thm)],[f501,f1996]) ).
fof(f1998,plain,
( ~ sQ96_spl
| ~ sQ56_spl
| e15 = e13 ),
inference(forward_demodulation,[status(thm)],[f99,f1997]) ).
fof(f1999,plain,
( ~ sQ96_spl
| ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1998,f24]) ).
fof(f2000,plain,
( ~ sQ96_spl
| ~ sQ56_spl ),
inference(contradiction_clause,[status(thm)],[f1999]) ).
fof(f2001,plain,
( ~ sQ92_spl
| ~ sQ66_spl
| e13 = op1(j(e22),e11) ),
inference(forward_demodulation,[status(thm)],[f532,f1501]) ).
fof(f2002,plain,
( ~ sQ92_spl
| ~ sQ66_spl
| e13 = op1(e13,e11) ),
inference(forward_demodulation,[status(thm)],[f532,f2001]) ).
fof(f2003,plain,
( ~ sQ92_spl
| ~ sQ66_spl
| e13 = e15 ),
inference(forward_demodulation,[status(thm)],[f121,f2002]) ).
fof(f2004,plain,
( ~ sQ92_spl
| ~ sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2003,f24]) ).
fof(f2005,plain,
( ~ sQ92_spl
| ~ sQ66_spl ),
inference(contradiction_clause,[status(thm)],[f2004]) ).
fof(f2009,plain,
( ~ sQ0_spl
| h(e12) = op2(h(e15),e20) ),
inference(backward_demodulation,[status(thm)],[f325,f1214]) ).
fof(f2032,plain,
( ~ sQ35_spl
| h(e16) = op2(e20,h(e16)) ),
inference(forward_demodulation,[status(thm)],[f435,f1254]) ).
fof(f2039,plain,
( ~ sQ25_spl
| ~ sQ0_spl
| e24 = op2(e20,h(e10)) ),
inference(forward_demodulation,[status(thm)],[f325,f1865]) ).
fof(f2040,plain,
( ~ sQ25_spl
| ~ sQ0_spl
| e24 = op2(e20,e20) ),
inference(forward_demodulation,[status(thm)],[f325,f2039]) ).
fof(f2041,plain,
( ~ sQ25_spl
| ~ sQ0_spl
| e24 = e22 ),
inference(forward_demodulation,[status(thm)],[f148,f2040]) ).
fof(f2042,plain,
( ~ sQ25_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2041,f41]) ).
fof(f2043,plain,
( ~ sQ25_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f2042]) ).
fof(f2045,plain,
( ~ sQ35_spl
| h(e12) = op2(e20,h(e10)) ),
inference(forward_demodulation,[status(thm)],[f435,f1214]) ).
fof(f2047,plain,
( ~ sQ35_spl
| ~ sQ7_spl
| ~ sQ21_spl
| e20 = e22 ),
inference(forward_demodulation,[status(thm)],[f148,f848]) ).
fof(f2048,plain,
( ~ sQ35_spl
| ~ sQ7_spl
| ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2047,f30]) ).
fof(f2049,plain,
( ~ sQ35_spl
| ~ sQ7_spl
| ~ sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f2048]) ).
fof(f2050,plain,
( ~ sQ35_spl
| ~ sQ44_spl
| h(e16) = op2(e20,e22) ),
inference(backward_demodulation,[status(thm)],[f463,f2032]) ).
fof(f2056,plain,
( ~ sQ35_spl
| ~ sQ44_spl
| e22 = op2(e20,e22) ),
inference(forward_demodulation,[status(thm)],[f463,f2050]) ).
fof(f2057,plain,
( ~ sQ35_spl
| ~ sQ44_spl
| e22 = e21 ),
inference(forward_demodulation,[status(thm)],[f150,f2056]) ).
fof(f2058,plain,
( ~ sQ35_spl
| ~ sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2057,f35]) ).
fof(f2059,plain,
( ~ sQ35_spl
| ~ sQ44_spl ),
inference(contradiction_clause,[status(thm)],[f2058]) ).
fof(f2068,plain,
( ~ sQ32_spl
| h(e12) = op2(h(e14),e24) ),
inference(backward_demodulation,[status(thm)],[f425,f1207]) ).
fof(f2072,plain,
( ~ sQ32_spl
| h(e12) = op2(e24,e24) ),
inference(forward_demodulation,[status(thm)],[f425,f2068]) ).
fof(f2073,plain,
( ~ sQ32_spl
| h(e12) = e24 ),
inference(forward_demodulation,[status(thm)],[f180,f2072]) ).
fof(f2074,plain,
( ~ sQ32_spl
| sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2073,f382]) ).
fof(f2075,plain,
( ~ sQ32_spl
| sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f2074]) ).
fof(f2083,plain,
( ~ sQ51_spl
| h(e12) = e20 ),
inference(backward_demodulation,[status(thm)],[f485,f310]) ).
fof(f2084,plain,
( ~ sQ51_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f2083,f368,f484]) ).
fof(f2085,plain,
( ~ sQ50_spl
| j(e22) = e16 ),
inference(forward_demodulation,[status(thm)],[f148,f1332]) ).
fof(f2086,plain,
( ~ sQ50_spl
| ~ sQ66_spl
| e13 = e16 ),
inference(forward_demodulation,[status(thm)],[f532,f2085]) ).
fof(f2087,plain,
( ~ sQ50_spl
| ~ sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2086,f25]) ).
fof(f2088,plain,
( ~ sQ50_spl
| ~ sQ66_spl ),
inference(contradiction_clause,[status(thm)],[f2087]) ).
fof(f2094,plain,
( ~ sQ5_spl
| e25 = op2(h(e16),h(e16)) ),
inference(backward_demodulation,[status(thm)],[f340,f1317]) ).
fof(f2107,plain,
( ~ sQ24_spl
| h(e13) = op2(e23,h(e16)) ),
inference(backward_demodulation,[status(thm)],[f400,f1180]) ).
fof(f2109,plain,
( ~ sQ24_spl
| e23 = op2(e23,h(e16)) ),
inference(forward_demodulation,[status(thm)],[f400,f2107]) ).
fof(f2110,plain,
( ~ sQ24_spl
| e23 = op2(h(e16),h(e13)) ),
inference(forward_demodulation,[status(thm)],[f400,f1293]) ).
fof(f2111,plain,
( ~ sQ24_spl
| e23 = op2(h(e16),e23) ),
inference(forward_demodulation,[status(thm)],[f400,f2110]) ).
fof(f2120,plain,
( ~ sQ40_spl
| h(e11) = op2(h(e15),e25) ),
inference(backward_demodulation,[status(thm)],[f450,f1252]) ).
fof(f2122,plain,
( ~ sQ40_spl
| h(e11) = op2(e25,e25) ),
inference(forward_demodulation,[status(thm)],[f450,f2120]) ).
fof(f2123,plain,
( ~ sQ40_spl
| h(e11) = e21 ),
inference(forward_demodulation,[status(thm)],[f188,f2122]) ).
fof(f2124,plain,
( ~ sQ40_spl
| sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2123,f351]) ).
fof(f2125,plain,
( ~ sQ40_spl
| sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f2124]) ).
fof(f2127,plain,
( ~ sQ37_spl
| ~ sQ5_spl
| e25 = op2(h(e13),e22) ),
inference(forward_demodulation,[status(thm)],[f340,f1179]) ).
fof(f2128,plain,
( ~ sQ37_spl
| ~ sQ5_spl
| ~ sQ24_spl
| e25 = op2(e23,e22) ),
inference(forward_demodulation,[status(thm)],[f400,f2127]) ).
fof(f2129,plain,
( ~ sQ37_spl
| ~ sQ5_spl
| ~ sQ24_spl
| e25 = e26 ),
inference(forward_demodulation,[status(thm)],[f171,f2128]) ).
fof(f2130,plain,
( ~ sQ37_spl
| ~ sQ5_spl
| ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2129,f49]) ).
fof(f2131,plain,
( ~ sQ37_spl
| ~ sQ5_spl
| ~ sQ24_spl ),
inference(contradiction_clause,[status(thm)],[f2130]) ).
fof(f2133,plain,
j(e22) = op1(j(e20),j(e20)),
inference(forward_demodulation,[status(thm)],[f148,f261]) ).
fof(f2197,plain,
( ~ sQ73_spl
| ~ sQ67_spl
| e13 = op1(e14,j(e22)) ),
inference(forward_demodulation,[status(thm)],[f535,f1463]) ).
fof(f2198,plain,
( ~ sQ73_spl
| ~ sQ67_spl
| e13 = op1(e14,e14) ),
inference(forward_demodulation,[status(thm)],[f535,f2197]) ).
fof(f2199,plain,
( ~ sQ73_spl
| ~ sQ67_spl
| e13 = e12 ),
inference(forward_demodulation,[status(thm)],[f131,f2198]) ).
fof(f2200,plain,
( ~ sQ73_spl
| ~ sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2199,f19]) ).
fof(f2201,plain,
( ~ sQ73_spl
| ~ sQ67_spl ),
inference(contradiction_clause,[status(thm)],[f2200]) ).
fof(f2202,plain,
( ~ sQ74_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1546,f484,f556]) ).
fof(f2249,plain,
( ~ sQ87_spl
| e13 = op1(j(e22),j(e25)) ),
inference(forward_demodulation,[status(thm)],[f598,f1492]) ).
fof(f2250,plain,
( ~ sQ87_spl
| e13 = op1(j(e22),e13) ),
inference(forward_demodulation,[status(thm)],[f598,f2249]) ).
fof(f2257,plain,
( ~ sQ54_spl
| e15 = op1(j(e22),j(e24)) ),
inference(forward_demodulation,[status(thm)],[f494,f1485]) ).
fof(f2258,plain,
( ~ sQ54_spl
| ~ sQ79_spl
| e15 = op1(j(e22),e12) ),
inference(forward_demodulation,[status(thm)],[f573,f2257]) ).
fof(f2270,plain,
( ~ sQ54_spl
| ~ sQ79_spl
| ~ sQ68_spl
| e15 = op1(e15,e12) ),
inference(backward_demodulation,[status(thm)],[f538,f2258]) ).
fof(f2273,plain,
( ~ sQ87_spl
| ~ sQ68_spl
| e13 = op1(e15,e13) ),
inference(backward_demodulation,[status(thm)],[f538,f2250]) ).
fof(f2276,plain,
( ~ sQ54_spl
| ~ sQ79_spl
| ~ sQ68_spl
| e15 = e13 ),
inference(forward_demodulation,[status(thm)],[f136,f2270]) ).
fof(f2277,plain,
( ~ sQ54_spl
| ~ sQ79_spl
| ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2276,f24]) ).
fof(f2278,plain,
( ~ sQ54_spl
| ~ sQ79_spl
| ~ sQ68_spl ),
inference(contradiction_clause,[status(thm)],[f2277]) ).
fof(f2301,plain,
( ~ sQ57_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f1746,f349,f503]) ).
fof(f2317,plain,
( ~ sQ96_spl
| j(e22) = op1(j(e22),e15) ),
inference(forward_demodulation,[status(thm)],[f626,f1500]) ).
fof(f2318,plain,
( ~ sQ96_spl
| ~ sQ65_spl
| j(e22) = op1(e12,e15) ),
inference(backward_demodulation,[status(thm)],[f529,f2317]) ).
fof(f2326,plain,
( ~ sQ96_spl
| ~ sQ65_spl
| e12 = op1(e12,e15) ),
inference(forward_demodulation,[status(thm)],[f529,f2318]) ).
fof(f2327,plain,
( ~ sQ96_spl
| ~ sQ65_spl
| e12 = e13 ),
inference(forward_demodulation,[status(thm)],[f118,f2326]) ).
fof(f2328,plain,
( ~ sQ96_spl
| ~ sQ65_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2327,f19]) ).
fof(f2329,plain,
( ~ sQ96_spl
| ~ sQ65_spl ),
inference(contradiction_clause,[status(thm)],[f2328]) ).
fof(f2337,plain,
( ~ sQ72_spl
| j(e20) = op1(j(e23),e12) ),
inference(backward_demodulation,[status(thm)],[f551,f1543]) ).
fof(f2345,plain,
( ~ sQ72_spl
| j(e20) = op1(e12,e12) ),
inference(forward_demodulation,[status(thm)],[f551,f2337]) ).
fof(f2346,plain,
( ~ sQ72_spl
| j(e20) = e15 ),
inference(forward_demodulation,[status(thm)],[f115,f2345]) ).
fof(f2347,plain,
( ~ sQ72_spl
| sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2346,f495]) ).
fof(f2348,plain,
( ~ sQ72_spl
| sQ54_spl ),
inference(contradiction_clause,[status(thm)],[f2347]) ).
fof(f2349,plain,
( ~ sQ78_spl
| j(e24) = op1(j(e24),e11) ),
inference(backward_demodulation,[status(thm)],[f570,f1592]) ).
fof(f2354,plain,
( ~ sQ78_spl
| e11 = op1(j(e24),e11) ),
inference(forward_demodulation,[status(thm)],[f570,f2349]) ).
fof(f2355,plain,
( ~ sQ78_spl
| e11 = op1(e11,e11) ),
inference(forward_demodulation,[status(thm)],[f570,f2354]) ).
fof(f2356,plain,
( ~ sQ78_spl
| e11 = e16 ),
inference(forward_demodulation,[status(thm)],[f107,f2355]) ).
fof(f2357,plain,
( ~ sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2356,f18]) ).
fof(f2358,plain,
~ sQ78_spl,
inference(contradiction_clause,[status(thm)],[f2357]) ).
fof(f2382,plain,
( ~ sQ58_spl
| j(e25) = op1(e12,j(e24)) ),
inference(forward_demodulation,[status(thm)],[f507,f1427]) ).
fof(f2394,plain,
( ~ sQ58_spl
| j(e23) = op1(j(e26),e12) ),
inference(forward_demodulation,[status(thm)],[f507,f1683]) ).
fof(f2402,plain,
( ~ sQ58_spl
| ~ sQ94_spl
| j(e23) = op1(e13,e12) ),
inference(backward_demodulation,[status(thm)],[f620,f2394]) ).
fof(f2409,plain,
( ~ sQ58_spl
| ~ sQ94_spl
| j(e23) = e12 ),
inference(forward_demodulation,[status(thm)],[f122,f2402]) ).
fof(f2410,plain,
( ~ sQ58_spl
| e12 = op1(j(e25),j(e25)) ),
inference(forward_demodulation,[status(thm)],[f507,f1658]) ).
fof(f2429,plain,
( ~ sQ89_spl
| j(e21) = op1(e15,j(e25)) ),
inference(forward_demodulation,[status(thm)],[f604,f1658]) ).
fof(f2430,plain,
( ~ sQ89_spl
| j(e21) = op1(e15,e15) ),
inference(forward_demodulation,[status(thm)],[f604,f2429]) ).
fof(f2431,plain,
( ~ sQ89_spl
| j(e21) = e11 ),
inference(forward_demodulation,[status(thm)],[f139,f2430]) ).
fof(f2456,plain,
( ~ sQ37_spl
| ~ sQ29_spl
| e22 = op2(e21,e22) ),
inference(forward_demodulation,[status(thm)],[f416,f1211]) ).
fof(f2457,plain,
( ~ sQ37_spl
| ~ sQ29_spl
| e22 = e24 ),
inference(forward_demodulation,[status(thm)],[f157,f2456]) ).
fof(f2458,plain,
( ~ sQ37_spl
| ~ sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2457,f41]) ).
fof(f2459,plain,
( ~ sQ37_spl
| ~ sQ29_spl ),
inference(contradiction_clause,[status(thm)],[f2458]) ).
fof(f2522,plain,
( ~ sQ65_spl
| h(e12) = e22 ),
inference(forward_demodulation,[status(thm)],[f529,f312]) ).
fof(f2523,plain,
( ~ sQ65_spl
| sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2522,f376]) ).
fof(f2524,plain,
( ~ sQ65_spl
| sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f2523]) ).
fof(f2547,plain,
( ~ sQ59_spl
| h(e13) = e21 ),
inference(backward_demodulation,[status(thm)],[f510,f311]) ).
fof(f2552,plain,
( ~ sQ59_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f2547,f393,f509]) ).
fof(f2560,plain,
( ~ sQ80_spl
| h(e13) = e24 ),
inference(backward_demodulation,[status(thm)],[f576,f314]) ).
fof(f2561,plain,
( ~ sQ80_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f2560,f402,f575]) ).
fof(f2562,plain,
( ~ sQ38_spl
| j(e23) = e15 ),
inference(backward_demodulation,[status(thm)],[f444,f322]) ).
fof(f2568,plain,
( ~ sQ38_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f2562,f559,f443]) ).
fof(f2570,plain,
( ~ sQ84_spl
| h(e10) = e25 ),
inference(backward_demodulation,[status(thm)],[f589,f315]) ).
fof(f2577,plain,
( ~ sQ84_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f2570,f339,f588]) ).
fof(f2578,plain,
( ~ sQ87_spl
| ~ sQ68_spl
| e13 = e10 ),
inference(forward_demodulation,[status(thm)],[f137,f2273]) ).
fof(f2579,plain,
( ~ sQ87_spl
| ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2578,f10]) ).
fof(f2580,plain,
( ~ sQ87_spl
| ~ sQ68_spl ),
inference(contradiction_clause,[status(thm)],[f2579]) ).
fof(f2581,plain,
( ~ sQ89_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f2431,f503,f603]) ).
fof(f2589,plain,
( ~ sQ12_spl
| j(e25) = e11 ),
inference(backward_demodulation,[status(thm)],[f362,f318]) ).
fof(f2591,plain,
( ~ sQ12_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f2589,f591,f361]) ).
fof(f2603,plain,
( ~ sQ24_spl
| j(e23) = e13 ),
inference(backward_demodulation,[status(thm)],[f400,f320]) ).
fof(f2604,plain,
( ~ sQ24_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f2603,f553,f399]) ).
fof(f2605,plain,
( ~ sQ14_spl
| e20 = op2(h(e11),h(e16)) ),
inference(backward_demodulation,[status(thm)],[f369,f953]) ).
fof(f2606,plain,
( ~ sQ14_spl
| h(e16) = op2(h(e10),e20) ),
inference(backward_demodulation,[status(thm)],[f369,f1825]) ).
fof(f2609,plain,
( ~ sQ14_spl
| j(e20) = e12 ),
inference(backward_demodulation,[status(thm)],[f369,f319]) ).
fof(f2635,plain,
( ~ sQ0_spl
| j(e20) = e10 ),
inference(backward_demodulation,[status(thm)],[f325,f317]) ).
fof(f2652,plain,
( ~ sQ8_spl
| h(e16) = op2(h(e11),e21) ),
inference(backward_demodulation,[status(thm)],[f350,f780]) ).
fof(f2654,plain,
( ~ sQ8_spl
| h(e16) = op2(e21,e21) ),
inference(forward_demodulation,[status(thm)],[f350,f2652]) ).
fof(f2655,plain,
( ~ sQ8_spl
| h(e16) = e26 ),
inference(forward_demodulation,[status(thm)],[f156,f2654]) ).
fof(f2662,plain,
( ~ sQ8_spl
| h(e14) = op2(e21,h(e15)) ),
inference(forward_demodulation,[status(thm)],[f350,f905]) ).
fof(f2663,plain,
( ~ sQ0_spl
| h(e15) = op2(e20,h(e16)) ),
inference(forward_demodulation,[status(thm)],[f325,f713]) ).
fof(f2664,plain,
( ~ sQ0_spl
| ~ sQ8_spl
| h(e15) = op2(e20,e26) ),
inference(forward_demodulation,[status(thm)],[f1931,f2663]) ).
fof(f2665,plain,
( ~ sQ8_spl
| ~ sQ0_spl
| h(e14) = op2(e21,e26) ),
inference(backward_demodulation,[status(thm)],[f2672,f2662]) ).
fof(f2672,plain,
( ~ sQ0_spl
| ~ sQ8_spl
| h(e15) = e26 ),
inference(forward_demodulation,[status(thm)],[f154,f2664]) ).
fof(f2673,plain,
( ~ sQ8_spl
| ~ sQ0_spl
| h(e14) = e23 ),
inference(forward_demodulation,[status(thm)],[f161,f2665]) ).
fof(f2679,plain,
( ~ sQ73_spl
| h(e13) = e23 ),
inference(backward_demodulation,[status(thm)],[f554,f313]) ).
fof(f2680,plain,
( ~ sQ73_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f2679,f399,f553]) ).
fof(f2682,plain,
( ~ sQ24_spl
| ~ sQ8_spl
| e23 = op2(e23,e26) ),
inference(forward_demodulation,[status(thm)],[f1931,f2109]) ).
fof(f2683,plain,
( ~ sQ24_spl
| ~ sQ8_spl
| e23 = e24 ),
inference(forward_demodulation,[status(thm)],[f175,f2682]) ).
fof(f2684,plain,
( ~ sQ24_spl
| ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2683,f44]) ).
fof(f2685,plain,
( ~ sQ24_spl
| ~ sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f2684]) ).
fof(f2706,plain,
( ~ sQ14_spl
| ~ sQ8_spl
| e20 = op2(e21,h(e16)) ),
inference(forward_demodulation,[status(thm)],[f350,f2605]) ).
fof(f2707,plain,
( ~ sQ14_spl
| ~ sQ8_spl
| e20 = op2(e21,e26) ),
inference(forward_demodulation,[status(thm)],[f1931,f2706]) ).
fof(f2708,plain,
( ~ sQ14_spl
| ~ sQ8_spl
| e20 = e23 ),
inference(forward_demodulation,[status(thm)],[f161,f2707]) ).
fof(f2709,plain,
( ~ sQ14_spl
| ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2708,f31]) ).
fof(f2710,plain,
( ~ sQ14_spl
| ~ sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f2709]) ).
fof(f2711,plain,
( ~ sQ0_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f2635,f478,f324]) ).
fof(f2712,plain,
( ~ sQ72_spl
| ~ sQ53_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f1512,f588,f490,f550]) ).
fof(f2722,plain,
( ~ sQ26_spl
| h(e14) = op2(h(e13),e25) ),
inference(backward_demodulation,[status(thm)],[f406,f1141]) ).
fof(f2727,plain,
( ~ sQ26_spl
| h(e14) = op2(e25,e25) ),
inference(forward_demodulation,[status(thm)],[f406,f2722]) ).
fof(f2728,plain,
( ~ sQ26_spl
| h(e14) = e21 ),
inference(forward_demodulation,[status(thm)],[f188,f2727]) ).
fof(f2729,plain,
( ~ sQ26_spl
| sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2728,f417]) ).
fof(f2730,plain,
( ~ sQ26_spl
| sQ29_spl ),
inference(contradiction_clause,[status(thm)],[f2729]) ).
fof(f2760,plain,
( ~ sQ16_spl
| h(e16) = op2(e22,h(e10)) ),
inference(backward_demodulation,[status(thm)],[f375,f979]) ).
fof(f2772,plain,
( ~ sQ39_spl
| h(e16) = op2(e24,h(e16)) ),
inference(forward_demodulation,[status(thm)],[f447,f1254]) ).
fof(f2835,plain,
( ~ sQ22_spl
| h(e12) = op2(h(e14),e26) ),
inference(backward_demodulation,[status(thm)],[f1964,f1207]) ).
fof(f2837,plain,
( ~ sQ22_spl
| h(e15) = op2(e26,h(e15)) ),
inference(backward_demodulation,[status(thm)],[f1964,f1209]) ).
fof(f2842,plain,
( ~ sQ22_spl
| h(e12) = op2(e26,e26) ),
inference(forward_demodulation,[status(thm)],[f1964,f2835]) ).
fof(f2843,plain,
( ~ sQ22_spl
| h(e12) = e25 ),
inference(forward_demodulation,[status(thm)],[f196,f2842]) ).
fof(f2844,plain,
( ~ sQ22_spl
| sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2843,f385]) ).
fof(f2845,plain,
( ~ sQ22_spl
| sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f2844]) ).
fof(f2856,plain,
( ~ sQ50_spl
| h(e11) = e20 ),
inference(backward_demodulation,[status(thm)],[f482,f310]) ).
fof(f2900,plain,
( ~ sQ24_spl
| ~ sQ45_spl
| e23 = op2(e23,e23) ),
inference(forward_demodulation,[status(thm)],[f466,f2111]) ).
fof(f2901,plain,
( ~ sQ24_spl
| ~ sQ45_spl
| e23 = e20 ),
inference(forward_demodulation,[status(thm)],[f172,f2900]) ).
fof(f2902,plain,
( ~ sQ24_spl
| ~ sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2901,f31]) ).
fof(f2903,plain,
( ~ sQ24_spl
| ~ sQ45_spl ),
inference(contradiction_clause,[status(thm)],[f2902]) ).
fof(f2920,plain,
( ~ sQ60_spl
| j(e26) = op1(j(e21),e14) ),
inference(backward_demodulation,[status(thm)],[f513,f1379]) ).
fof(f2926,plain,
( ~ sQ60_spl
| j(e26) = op1(e14,e14) ),
inference(forward_demodulation,[status(thm)],[f513,f2920]) ).
fof(f2927,plain,
( ~ sQ60_spl
| j(e26) = e12 ),
inference(forward_demodulation,[status(thm)],[f131,f2926]) ).
fof(f2928,plain,
( ~ sQ60_spl
| sQ93_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2927,f618]) ).
fof(f2929,plain,
( ~ sQ60_spl
| sQ93_spl ),
inference(contradiction_clause,[status(thm)],[f2928]) ).
fof(f2943,plain,
( ~ sQ49_spl
| j(e22) = op1(j(e20),e10) ),
inference(backward_demodulation,[status(thm)],[f479,f2133]) ).
fof(f2947,plain,
( ~ sQ49_spl
| j(e22) = op1(e10,e10) ),
inference(forward_demodulation,[status(thm)],[f479,f2943]) ).
fof(f2948,plain,
( ~ sQ49_spl
| j(e22) = e13 ),
inference(forward_demodulation,[status(thm)],[f99,f2947]) ).
fof(f2949,plain,
( ~ sQ49_spl
| sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2948,f533]) ).
fof(f2950,plain,
( ~ sQ49_spl
| sQ66_spl ),
inference(contradiction_clause,[status(thm)],[f2949]) ).
fof(f2956,plain,
( ~ sQ0_spl
| ~ sQ37_spl
| h(e12) = op2(e22,e20) ),
inference(forward_demodulation,[status(thm)],[f441,f2009]) ).
fof(f2957,plain,
( ~ sQ0_spl
| ~ sQ37_spl
| h(e12) = e21 ),
inference(forward_demodulation,[status(thm)],[f162,f2956]) ).
fof(f2990,plain,
( ~ sQ93_spl
| j(e22) = op1(j(e22),e12) ),
inference(forward_demodulation,[status(thm)],[f617,f1500]) ).
fof(f2997,plain,
( ~ sQ93_spl
| ~ sQ66_spl
| j(e22) = op1(e13,e12) ),
inference(backward_demodulation,[status(thm)],[f532,f2990]) ).
fof(f3004,plain,
( ~ sQ93_spl
| ~ sQ66_spl
| e13 = op1(e13,e12) ),
inference(forward_demodulation,[status(thm)],[f532,f2997]) ).
fof(f3005,plain,
( ~ sQ93_spl
| ~ sQ66_spl
| e13 = e12 ),
inference(forward_demodulation,[status(thm)],[f122,f3004]) ).
fof(f3006,plain,
( ~ sQ93_spl
| ~ sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3005,f19]) ).
fof(f3007,plain,
( ~ sQ93_spl
| ~ sQ66_spl ),
inference(contradiction_clause,[status(thm)],[f3006]) ).
fof(f3025,plain,
( ~ sQ64_spl
| j(e25) = op1(e11,j(e25)) ),
inference(backward_demodulation,[status(thm)],[f526,f1492]) ).
fof(f3056,plain,
( ~ sQ77_spl
| e10 = op1(j(e24),j(e24)) ),
inference(forward_demodulation,[status(thm)],[f567,f1592]) ).
fof(f3057,plain,
( ~ sQ77_spl
| e10 = op1(e10,j(e24)) ),
inference(forward_demodulation,[status(thm)],[f567,f3056]) ).
fof(f3058,plain,
( ~ sQ77_spl
| e10 = op1(e10,e10) ),
inference(forward_demodulation,[status(thm)],[f567,f3057]) ).
fof(f3059,plain,
( ~ sQ77_spl
| e10 = e13 ),
inference(forward_demodulation,[status(thm)],[f99,f3058]) ).
fof(f3060,plain,
( ~ sQ77_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3059,f10]) ).
fof(f3061,plain,
~ sQ77_spl,
inference(contradiction_clause,[status(thm)],[f3060]) ).
fof(f3068,plain,
( ~ sQ14_spl
| ~ sQ4_spl
| h(e16) = op2(e24,e20) ),
inference(forward_demodulation,[status(thm)],[f337,f2606]) ).
fof(f3069,plain,
( ~ sQ14_spl
| ~ sQ4_spl
| h(e16) = e23 ),
inference(forward_demodulation,[status(thm)],[f176,f3068]) ).
fof(f3073,plain,
( ~ sQ82_spl
| ~ sQ64_spl
| j(e20) = op1(e11,e15) ),
inference(forward_demodulation,[status(thm)],[f526,f1499]) ).
fof(f3074,plain,
( ~ sQ82_spl
| ~ sQ64_spl
| j(e20) = e14 ),
inference(forward_demodulation,[status(thm)],[f111,f3073]) ).
fof(f3080,plain,
( ~ sQ58_spl
| ~ sQ92_spl
| j(e23) = op1(e11,e12) ),
inference(forward_demodulation,[status(thm)],[f614,f2394]) ).
fof(f3081,plain,
( ~ sQ58_spl
| ~ sQ92_spl
| j(e23) = e11 ),
inference(forward_demodulation,[status(thm)],[f108,f3080]) ).
fof(f3083,plain,
( ~ sQ12_spl
| ~ sQ4_spl
| e24 = op2(h(e10),e25) ),
inference(forward_demodulation,[status(thm)],[f337,f1854]) ).
fof(f3084,plain,
( ~ sQ12_spl
| ~ sQ4_spl
| e24 = op2(e24,e25) ),
inference(forward_demodulation,[status(thm)],[f337,f3083]) ).
fof(f3085,plain,
( ~ sQ12_spl
| ~ sQ4_spl
| e24 = e26 ),
inference(forward_demodulation,[status(thm)],[f181,f3084]) ).
fof(f3086,plain,
( ~ sQ12_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3085,f48]) ).
fof(f3087,plain,
( ~ sQ12_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f3086]) ).
fof(f3091,plain,
( ~ sQ56_spl
| ~ sQ64_spl
| e10 = op1(j(e20),e11) ),
inference(forward_demodulation,[status(thm)],[f526,f1342]) ).
fof(f3109,plain,
( ~ sQ82_spl
| j(e25) = op1(j(e21),e15) ),
inference(backward_demodulation,[status(thm)],[f582,f1427]) ).
fof(f3118,plain,
( sQ53_spl
| ~ sQ82_spl
| ~ sQ64_spl
| e14 != e14 ),
inference(forward_demodulation,[status(thm)],[f3074,f492]) ).
fof(f3119,plain,
( sQ53_spl
| ~ sQ82_spl
| ~ sQ64_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f3118]) ).
fof(f3120,plain,
( sQ53_spl
| ~ sQ82_spl
| ~ sQ64_spl ),
inference(contradiction_clause,[status(thm)],[f3119]) ).
fof(f3121,plain,
( ~ sQ0_spl
| ~ sQ37_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f2957,f371,f440,f324]) ).
fof(f3127,plain,
( ~ sQ37_spl
| ~ sQ21_spl
| h(e10) = op2(e20,e22) ),
inference(forward_demodulation,[status(thm)],[f391,f1179]) ).
fof(f3128,plain,
( ~ sQ37_spl
| ~ sQ21_spl
| h(e10) = e21 ),
inference(forward_demodulation,[status(thm)],[f150,f3127]) ).
fof(f3129,plain,
( ~ sQ18_spl
| ~ sQ21_spl
| e24 = op2(e20,e24) ),
inference(forward_demodulation,[status(thm)],[f391,f1968]) ).
fof(f3130,plain,
( ~ sQ18_spl
| ~ sQ21_spl
| e24 = e23 ),
inference(forward_demodulation,[status(thm)],[f152,f3129]) ).
fof(f3131,plain,
( ~ sQ18_spl
| ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3130,f44]) ).
fof(f3132,plain,
( ~ sQ18_spl
| ~ sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f3131]) ).
fof(f3150,plain,
( ~ sQ44_spl
| h(e10) = op2(h(e16),e22) ),
inference(backward_demodulation,[status(thm)],[f463,f1317]) ).
fof(f3155,plain,
( ~ sQ44_spl
| h(e10) = op2(e22,e22) ),
inference(forward_demodulation,[status(thm)],[f463,f3150]) ).
fof(f3156,plain,
( ~ sQ44_spl
| h(e10) = e23 ),
inference(forward_demodulation,[status(thm)],[f164,f3155]) ).
fof(f3157,plain,
( ~ sQ44_spl
| sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3156,f335]) ).
fof(f3158,plain,
( ~ sQ44_spl
| sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f3157]) ).
fof(f3170,plain,
( ~ sQ66_spl
| h(e13) = e22 ),
inference(forward_demodulation,[status(thm)],[f532,f312]) ).
fof(f3171,plain,
( ~ sQ66_spl
| sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3170,f398]) ).
fof(f3172,plain,
( ~ sQ66_spl
| sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f3171]) ).
fof(f3184,plain,
( ~ sQ93_spl
| e12 = j(e26) ),
inference(forward_demodulation,[status(thm)],[f1607,f1610]) ).
fof(f3232,plain,
( ~ sQ82_spl
| h(e15) = e24 ),
inference(forward_demodulation,[status(thm)],[f582,f314]) ).
fof(f3233,plain,
( ~ sQ82_spl
| sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3232,f448]) ).
fof(f3234,plain,
( ~ sQ82_spl
| sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f3233]) ).
fof(f3264,plain,
( ~ sQ93_spl
| j(e25) = op1(e12,j(e26)) ),
inference(forward_demodulation,[status(thm)],[f3184,f1734]) ).
fof(f3265,plain,
( ~ sQ93_spl
| j(e25) = op1(e12,e12) ),
inference(forward_demodulation,[status(thm)],[f3184,f3264]) ).
fof(f3267,plain,
( ~ sQ93_spl
| h(e15) = e25 ),
inference(backward_demodulation,[status(thm)],[f3268,f315]) ).
fof(f3268,plain,
( ~ sQ93_spl
| j(e25) = e15 ),
inference(forward_demodulation,[status(thm)],[f115,f3265]) ).
fof(f3270,plain,
( ~ sQ93_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f3267,f449,f616]) ).
fof(f3272,plain,
( ~ sQ8_spl
| ~ sQ0_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f2673,f421,f324,f349]) ).
fof(f3277,plain,
( ~ sQ61_spl
| h(e15) = e21 ),
inference(backward_demodulation,[status(thm)],[f516,f311]) ).
fof(f3299,plain,
( ~ sQ9_spl
| j(e22) = e11 ),
inference(backward_demodulation,[status(thm)],[f353,f318]) ).
fof(f3307,plain,
( ~ sQ9_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f3299,f525,f352]) ).
fof(f3310,plain,
( ~ sQ64_spl
| ~ sQ85_spl
| e11 = op1(e11,j(e25)) ),
inference(forward_demodulation,[status(thm)],[f592,f3025]) ).
fof(f3311,plain,
( ~ sQ64_spl
| ~ sQ85_spl
| e11 = op1(e11,e11) ),
inference(forward_demodulation,[status(thm)],[f592,f3310]) ).
fof(f3312,plain,
( ~ sQ64_spl
| ~ sQ85_spl
| e11 = e16 ),
inference(forward_demodulation,[status(thm)],[f107,f3311]) ).
fof(f3313,plain,
( ~ sQ64_spl
| ~ sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3312,f18]) ).
fof(f3314,plain,
( ~ sQ64_spl
| ~ sQ85_spl ),
inference(contradiction_clause,[status(thm)],[f3313]) ).
fof(f3338,plain,
( ~ sQ18_spl
| h(e15) = op2(h(e12),e24) ),
inference(backward_demodulation,[status(thm)],[f381,f1054]) ).
fof(f3345,plain,
( ~ sQ18_spl
| h(e15) = op2(e24,e24) ),
inference(forward_demodulation,[status(thm)],[f381,f3338]) ).
fof(f3346,plain,
( ~ sQ18_spl
| h(e15) = e24 ),
inference(forward_demodulation,[status(thm)],[f180,f3345]) ).
fof(f3347,plain,
( ~ sQ18_spl
| sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3346,f448]) ).
fof(f3348,plain,
( ~ sQ18_spl
| sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f3347]) ).
fof(f3366,plain,
( ~ sQ10_spl
| h(e16) = op2(e23,h(e11)) ),
inference(forward_demodulation,[status(thm)],[f356,f780]) ).
fof(f3367,plain,
( ~ sQ10_spl
| h(e16) = op2(e23,e23) ),
inference(forward_demodulation,[status(thm)],[f356,f3366]) ).
fof(f3368,plain,
( ~ sQ10_spl
| h(e16) = e20 ),
inference(forward_demodulation,[status(thm)],[f172,f3367]) ).
fof(f3369,plain,
( ~ sQ10_spl
| sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3368,f458]) ).
fof(f3370,plain,
( ~ sQ10_spl
| sQ42_spl ),
inference(contradiction_clause,[status(thm)],[f3369]) ).
fof(f3380,plain,
( ~ sQ92_spl
| h(e11) = e26 ),
inference(backward_demodulation,[status(thm)],[f614,f316]) ).
fof(f3381,plain,
( ~ sQ92_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f3380,f364,f613]) ).
fof(f3382,plain,
( ~ sQ37_spl
| ~ sQ21_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f3128,f327,f390,f440]) ).
fof(f3393,plain,
( ~ sQ75_spl
| h(e15) = e23 ),
inference(backward_demodulation,[status(thm)],[f560,f313]) ).
fof(f3394,plain,
( ~ sQ75_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f3393,f443,f559]) ).
fof(f3469,plain,
( ~ sQ1_spl
| j(e21) = e10 ),
inference(backward_demodulation,[status(thm)],[f328,f317]) ).
fof(f3487,plain,
( ~ sQ96_spl
| ~ sQ68_spl
| e15 = op1(j(e22),e15) ),
inference(forward_demodulation,[status(thm)],[f538,f2317]) ).
fof(f3488,plain,
( ~ sQ96_spl
| ~ sQ68_spl
| e15 = op1(e15,e15) ),
inference(forward_demodulation,[status(thm)],[f538,f3487]) ).
fof(f3489,plain,
( ~ sQ96_spl
| ~ sQ68_spl
| e15 = e11 ),
inference(forward_demodulation,[status(thm)],[f139,f3488]) ).
fof(f3490,plain,
( ~ sQ96_spl
| ~ sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3489,f17]) ).
fof(f3491,plain,
( ~ sQ96_spl
| ~ sQ68_spl ),
inference(contradiction_clause,[status(thm)],[f3490]) ).
fof(f3518,plain,
( ~ sQ53_spl
| h(e14) = e20 ),
inference(forward_demodulation,[status(thm)],[f491,f310]) ).
fof(f3519,plain,
( ~ sQ53_spl
| sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3518,f414]) ).
fof(f3520,plain,
( ~ sQ53_spl
| sQ28_spl ),
inference(contradiction_clause,[status(thm)],[f3519]) ).
fof(f3524,plain,
( ~ sQ35_spl
| ~ sQ5_spl
| h(e12) = op2(e20,e25) ),
inference(forward_demodulation,[status(thm)],[f340,f2045]) ).
fof(f3525,plain,
( ~ sQ35_spl
| ~ sQ5_spl
| h(e12) = e24 ),
inference(forward_demodulation,[status(thm)],[f153,f3524]) ).
fof(f3526,plain,
( ~ sQ35_spl
| ~ sQ5_spl
| sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3525,f382]) ).
fof(f3527,plain,
( ~ sQ35_spl
| ~ sQ5_spl
| sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f3526]) ).
fof(f3539,plain,
( ~ sQ16_spl
| ~ sQ5_spl
| h(e16) = op2(e22,e25) ),
inference(forward_demodulation,[status(thm)],[f340,f2760]) ).
fof(f3540,plain,
( ~ sQ16_spl
| ~ sQ5_spl
| h(e16) = e25 ),
inference(forward_demodulation,[status(thm)],[f167,f3539]) ).
fof(f3541,plain,
( ~ sQ16_spl
| ~ sQ5_spl
| sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3540,f473]) ).
fof(f3542,plain,
( ~ sQ16_spl
| ~ sQ5_spl
| sQ47_spl ),
inference(contradiction_clause,[status(thm)],[f3541]) ).
fof(f3560,plain,
( ~ sQ7_spl
| e20 = op2(h(e15),h(e15)) ),
inference(backward_demodulation,[status(thm)],[f347,f1252]) ).
fof(f3570,plain,
( ~ sQ54_spl
| j(e23) = op1(e15,j(e24)) ),
inference(backward_demodulation,[status(thm)],[f494,f1364]) ).
fof(f3576,plain,
( ~ sQ61_spl
| j(e26) = op1(j(e21),e15) ),
inference(backward_demodulation,[status(thm)],[f516,f1379]) ).
fof(f3580,plain,
( ~ sQ61_spl
| j(e26) = op1(e15,e15) ),
inference(forward_demodulation,[status(thm)],[f516,f3576]) ).
fof(f3581,plain,
( ~ sQ61_spl
| j(e26) = e11 ),
inference(forward_demodulation,[status(thm)],[f139,f3580]) ).
fof(f3582,plain,
( ~ sQ61_spl
| sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3581,f615]) ).
fof(f3583,plain,
( ~ sQ61_spl
| sQ92_spl ),
inference(contradiction_clause,[status(thm)],[f3582]) ).
fof(f3623,plain,
( ~ sQ14_spl
| j(e22) = op1(j(e20),e12) ),
inference(backward_demodulation,[status(thm)],[f2609,f2133]) ).
fof(f3624,plain,
( ~ sQ14_spl
| j(e22) = op1(e12,e12) ),
inference(forward_demodulation,[status(thm)],[f2609,f3623]) ).
fof(f3625,plain,
( ~ sQ14_spl
| j(e22) = e15 ),
inference(forward_demodulation,[status(thm)],[f115,f3624]) ).
fof(f3695,plain,
( ~ sQ58_spl
| ~ sQ85_spl
| e12 = op1(e11,j(e25)) ),
inference(forward_demodulation,[status(thm)],[f592,f2410]) ).
fof(f3696,plain,
( ~ sQ58_spl
| ~ sQ85_spl
| e12 = op1(e11,e11) ),
inference(forward_demodulation,[status(thm)],[f592,f3695]) ).
fof(f3697,plain,
( ~ sQ58_spl
| ~ sQ85_spl
| e12 = e16 ),
inference(forward_demodulation,[status(thm)],[f107,f3696]) ).
fof(f3698,plain,
( ~ sQ58_spl
| ~ sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3697,f22]) ).
fof(f3699,plain,
( ~ sQ58_spl
| ~ sQ85_spl ),
inference(contradiction_clause,[status(thm)],[f3698]) ).
fof(f3701,plain,
( ~ sQ1_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f3469,f500,f327]) ).
fof(f3746,plain,
( ~ sQ66_spl
| j(e25) = op1(e13,j(e25)) ),
inference(forward_demodulation,[status(thm)],[f532,f1492]) ).
fof(f3771,plain,
( ~ sQ66_spl
| ~ sQ87_spl
| j(e25) = op1(e13,e13) ),
inference(backward_demodulation,[status(thm)],[f598,f3746]) ).
fof(f3776,plain,
( ~ sQ66_spl
| ~ sQ87_spl
| e13 = op1(e13,e13) ),
inference(forward_demodulation,[status(thm)],[f598,f3771]) ).
fof(f3777,plain,
( ~ sQ66_spl
| ~ sQ87_spl
| e13 = e14 ),
inference(forward_demodulation,[status(thm)],[f123,f3776]) ).
fof(f3778,plain,
( ~ sQ66_spl
| ~ sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3777,f23]) ).
fof(f3779,plain,
( ~ sQ66_spl
| ~ sQ87_spl ),
inference(contradiction_clause,[status(thm)],[f3778]) ).
fof(f3781,plain,
( ~ sQ71_spl
| j(e20) = op1(j(e23),e11) ),
inference(backward_demodulation,[status(thm)],[f548,f1543]) ).
fof(f3782,plain,
( ~ sQ71_spl
| j(e20) = op1(e11,e11) ),
inference(forward_demodulation,[status(thm)],[f548,f3781]) ).
fof(f3783,plain,
( ~ sQ71_spl
| j(e20) = e16 ),
inference(forward_demodulation,[status(thm)],[f107,f3782]) ).
fof(f3854,plain,
( ~ sQ80_spl
| h(e13) = e24 ),
inference(backward_demodulation,[status(thm)],[f576,f314]) ).
fof(f3870,plain,
( ~ sQ5_spl
| ~ sQ46_spl
| e25 = op2(e24,h(e16)) ),
inference(forward_demodulation,[status(thm)],[f469,f2094]) ).
fof(f3871,plain,
( ~ sQ5_spl
| ~ sQ46_spl
| e25 = op2(e24,e24) ),
inference(forward_demodulation,[status(thm)],[f469,f3870]) ).
fof(f3872,plain,
( ~ sQ5_spl
| ~ sQ46_spl
| e25 = e24 ),
inference(forward_demodulation,[status(thm)],[f180,f3871]) ).
fof(f3873,plain,
( ~ sQ5_spl
| ~ sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3872,f47]) ).
fof(f3874,plain,
( ~ sQ5_spl
| ~ sQ46_spl ),
inference(contradiction_clause,[status(thm)],[f3873]) ).
fof(f3898,plain,
( ~ sQ82_spl
| ~ sQ56_spl
| j(e25) = op1(e10,e15) ),
inference(forward_demodulation,[status(thm)],[f501,f3109]) ).
fof(f3899,plain,
( ~ sQ82_spl
| ~ sQ56_spl
| j(e25) = e12 ),
inference(forward_demodulation,[status(thm)],[f104,f3898]) ).
fof(f3900,plain,
( ~ sQ82_spl
| ~ sQ56_spl
| sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3899,f596]) ).
fof(f3901,plain,
( ~ sQ82_spl
| ~ sQ56_spl
| sQ86_spl ),
inference(contradiction_clause,[status(thm)],[f3900]) ).
fof(f3943,plain,
( ~ sQ14_spl
| ~ sQ4_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f3069,f465,f336,f368]) ).
fof(f3944,plain,
( ~ sQ58_spl
| ~ sQ92_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f3081,f547,f613,f506]) ).
fof(f3958,plain,
( ~ sQ39_spl
| j(e24) = e15 ),
inference(forward_demodulation,[status(thm)],[f447,f322]) ).
fof(f3962,plain,
( ~ sQ86_spl
| h(e12) = e25 ),
inference(backward_demodulation,[status(thm)],[f595,f315]) ).
fof(f3969,plain,
( ~ sQ86_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f3962,f383,f594]) ).
fof(f3970,plain,
( ~ sQ39_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f3958,f581,f446]) ).
fof(f3973,plain,
( ~ sQ71_spl
| sQ55_spl ),
inference(split_clause,[status(thm)],[f3783,f496,f547]) ).
fof(f3992,plain,
( ~ sQ56_spl
| h(e10) = e21 ),
inference(backward_demodulation,[status(thm)],[f501,f311]) ).
fof(f4033,plain,
( ~ sQ13_spl
| h(e16) = op2(e26,h(e11)) ),
inference(forward_demodulation,[status(thm)],[f365,f780]) ).
fof(f4034,plain,
( ~ sQ13_spl
| h(e16) = op2(e26,e26) ),
inference(forward_demodulation,[status(thm)],[f365,f4033]) ).
fof(f4035,plain,
( ~ sQ13_spl
| h(e16) = e25 ),
inference(forward_demodulation,[status(thm)],[f196,f4034]) ).
fof(f4047,plain,
( ~ sQ47_spl
| ~ sQ13_spl
| h(e12) = op2(e26,e25) ),
inference(forward_demodulation,[status(thm)],[f365,f978]) ).
fof(f4048,plain,
( ~ sQ47_spl
| ~ sQ13_spl
| h(e12) = e20 ),
inference(forward_demodulation,[status(thm)],[f195,f4047]) ).
fof(f4049,plain,
( ~ sQ47_spl
| ~ sQ13_spl
| sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4048,f370]) ).
fof(f4050,plain,
( ~ sQ47_spl
| ~ sQ13_spl
| sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f4049]) ).
fof(f4055,plain,
( ~ sQ56_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f3992,f327,f500]) ).
fof(f4065,plain,
( ~ sQ57_spl
| ~ sQ84_spl
| sQ77_spl ),
inference(split_clause,[status(thm)],[f1454,f566,f588,f503]) ).
fof(f4082,plain,
( ~ sQ15_spl
| j(e21) = e12 ),
inference(backward_demodulation,[status(thm)],[f372,f319]) ).
fof(f4084,plain,
( ~ sQ15_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f4082,f506,f371]) ).
fof(f4085,plain,
( ~ sQ56_spl
| ~ sQ64_spl
| ~ sQ53_spl
| e10 = op1(e14,e11) ),
inference(forward_demodulation,[status(thm)],[f491,f3091]) ).
fof(f4086,plain,
( ~ sQ56_spl
| ~ sQ64_spl
| ~ sQ53_spl
| e10 = e13 ),
inference(forward_demodulation,[status(thm)],[f128,f4085]) ).
fof(f4087,plain,
( ~ sQ56_spl
| ~ sQ64_spl
| ~ sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4086,f10]) ).
fof(f4088,plain,
( ~ sQ56_spl
| ~ sQ64_spl
| ~ sQ53_spl ),
inference(contradiction_clause,[status(thm)],[f4087]) ).
fof(f4089,plain,
( ~ sQ61_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f3277,f437,f515]) ).
fof(f4090,plain,
( ~ sQ14_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f3625,f537,f368]) ).
fof(f4091,plain,
( ~ sQ13_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f4035,f471,f364]) ).
fof(f4105,plain,
( ~ sQ8_spl
| h(e16) = op2(h(e15),e26) ),
inference(backward_demodulation,[status(thm)],[f2655,f1254]) ).
fof(f4110,plain,
( ~ sQ8_spl
| e26 = op2(h(e15),e26) ),
inference(forward_demodulation,[status(thm)],[f2655,f4105]) ).
fof(f4126,plain,
( ~ sQ80_spl
| h(e14) = op2(e24,h(e13)) ),
inference(forward_demodulation,[status(thm)],[f3854,f1141]) ).
fof(f4127,plain,
( ~ sQ80_spl
| h(e14) = op2(e24,e24) ),
inference(forward_demodulation,[status(thm)],[f3854,f4126]) ).
fof(f4128,plain,
( ~ sQ80_spl
| h(e14) = e24 ),
inference(forward_demodulation,[status(thm)],[f180,f4127]) ).
fof(f4129,plain,
( ~ sQ80_spl
| sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4128,f426]) ).
fof(f4130,plain,
( ~ sQ80_spl
| sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f4129]) ).
fof(f4143,plain,
( ~ sQ58_spl
| ~ sQ94_spl
| sQ72_spl ),
inference(split_clause,[status(thm)],[f2409,f550,f619,f506]) ).
fof(f4163,plain,
( ~ sQ10_spl
| e23 = op2(h(e15),h(e15)) ),
inference(backward_demodulation,[status(thm)],[f356,f1252]) ).
fof(f4208,plain,
( ~ sQ58_spl
| j(e26) = op1(j(e21),e12) ),
inference(backward_demodulation,[status(thm)],[f507,f1379]) ).
fof(f4212,plain,
( ~ sQ58_spl
| j(e26) = op1(e12,e12) ),
inference(forward_demodulation,[status(thm)],[f507,f4208]) ).
fof(f4213,plain,
( ~ sQ58_spl
| j(e26) = e15 ),
inference(forward_demodulation,[status(thm)],[f115,f4212]) ).
fof(f4214,plain,
( ~ sQ58_spl
| sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4213,f627]) ).
fof(f4215,plain,
( ~ sQ58_spl
| sQ96_spl ),
inference(contradiction_clause,[status(thm)],[f4214]) ).
fof(f4237,plain,
( ~ sQ63_spl
| ~ sQ91_spl
| e10 = op1(e10,e10) ),
inference(forward_demodulation,[status(thm)],[f611,f1705]) ).
fof(f4238,plain,
( ~ sQ63_spl
| ~ sQ91_spl
| e10 = e13 ),
inference(forward_demodulation,[status(thm)],[f99,f4237]) ).
fof(f4239,plain,
( ~ sQ63_spl
| ~ sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4238,f10]) ).
fof(f4240,plain,
( ~ sQ63_spl
| ~ sQ91_spl ),
inference(contradiction_clause,[status(thm)],[f4239]) ).
fof(f4274,plain,
( ~ sQ2_spl
| j(e22) = e10 ),
inference(backward_demodulation,[status(thm)],[f331,f317]) ).
fof(f4296,plain,
( ~ sQ83_spl
| e16 = op1(j(e24),j(e24)) ),
inference(forward_demodulation,[status(thm)],[f585,f1592]) ).
fof(f4297,plain,
( ~ sQ83_spl
| e16 = op1(e16,j(e24)) ),
inference(forward_demodulation,[status(thm)],[f585,f4296]) ).
fof(f4298,plain,
( ~ sQ83_spl
| e16 = op1(e16,e16) ),
inference(forward_demodulation,[status(thm)],[f585,f4297]) ).
fof(f4299,plain,
( ~ sQ83_spl
| e16 = e10 ),
inference(forward_demodulation,[status(thm)],[f147,f4298]) ).
fof(f4300,plain,
( ~ sQ83_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4299,f13]) ).
fof(f4301,plain,
~ sQ83_spl,
inference(contradiction_clause,[status(thm)],[f4300]) ).
fof(f4302,plain,
( ~ sQ39_spl
| ~ sQ47_spl
| e25 = op2(e24,h(e16)) ),
inference(forward_demodulation,[status(thm)],[f472,f2772]) ).
fof(f4303,plain,
( ~ sQ39_spl
| ~ sQ47_spl
| e25 = op2(e24,e25) ),
inference(forward_demodulation,[status(thm)],[f472,f4302]) ).
fof(f4304,plain,
( ~ sQ39_spl
| ~ sQ47_spl
| e25 = e26 ),
inference(forward_demodulation,[status(thm)],[f181,f4303]) ).
fof(f4305,plain,
( ~ sQ39_spl
| ~ sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4304,f49]) ).
fof(f4306,plain,
( ~ sQ39_spl
| ~ sQ47_spl ),
inference(contradiction_clause,[status(thm)],[f4305]) ).
fof(f4345,plain,
( ~ sQ58_spl
| j(e23) = op1(e12,j(e26)) ),
inference(forward_demodulation,[status(thm)],[f507,f1446]) ).
fof(f4346,plain,
( ~ sQ58_spl
| j(e23) = op1(e12,e15) ),
inference(forward_demodulation,[status(thm)],[f4213,f4345]) ).
fof(f4347,plain,
( ~ sQ58_spl
| j(e23) = e13 ),
inference(forward_demodulation,[status(thm)],[f118,f4346]) ).
fof(f4348,plain,
( ~ sQ58_spl
| sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4347,f555]) ).
fof(f4349,plain,
( ~ sQ58_spl
| sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f4348]) ).
fof(f4356,plain,
( ~ sQ22_spl
| ~ sQ39_spl
| e24 = op2(e26,h(e15)) ),
inference(forward_demodulation,[status(thm)],[f447,f2837]) ).
fof(f4357,plain,
( ~ sQ22_spl
| ~ sQ39_spl
| e24 = op2(e26,e24) ),
inference(forward_demodulation,[status(thm)],[f447,f4356]) ).
fof(f4358,plain,
( ~ sQ22_spl
| ~ sQ39_spl
| e24 = e21 ),
inference(forward_demodulation,[status(thm)],[f194,f4357]) ).
fof(f4359,plain,
( ~ sQ22_spl
| ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4358,f37]) ).
fof(f4360,plain,
( ~ sQ22_spl
| ~ sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f4359]) ).
fof(f4361,plain,
( ~ sQ54_spl
| ~ sQ82_spl
| j(e23) = op1(e15,e15) ),
inference(forward_demodulation,[status(thm)],[f582,f3570]) ).
fof(f4362,plain,
( ~ sQ54_spl
| ~ sQ82_spl
| j(e23) = e11 ),
inference(forward_demodulation,[status(thm)],[f139,f4361]) ).
fof(f4368,plain,
( ~ sQ7_spl
| ~ sQ39_spl
| e20 = op2(e24,h(e15)) ),
inference(forward_demodulation,[status(thm)],[f447,f3560]) ).
fof(f4369,plain,
( ~ sQ7_spl
| ~ sQ39_spl
| e20 = op2(e24,e24) ),
inference(forward_demodulation,[status(thm)],[f447,f4368]) ).
fof(f4370,plain,
( ~ sQ7_spl
| ~ sQ39_spl
| e20 = e24 ),
inference(forward_demodulation,[status(thm)],[f180,f4369]) ).
fof(f4371,plain,
( ~ sQ7_spl
| ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4370,f32]) ).
fof(f4372,plain,
( ~ sQ7_spl
| ~ sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f4371]) ).
fof(f4374,plain,
( ~ sQ58_spl
| ~ sQ82_spl
| j(e25) = op1(e12,e15) ),
inference(forward_demodulation,[status(thm)],[f582,f2382]) ).
fof(f4375,plain,
( ~ sQ58_spl
| ~ sQ82_spl
| j(e25) = e13 ),
inference(forward_demodulation,[status(thm)],[f118,f4374]) ).
fof(f4376,plain,
( ~ sQ58_spl
| ~ sQ82_spl
| sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4375,f599]) ).
fof(f4377,plain,
( ~ sQ58_spl
| ~ sQ82_spl
| sQ87_spl ),
inference(contradiction_clause,[status(thm)],[f4376]) ).
fof(f4386,plain,
( ~ sQ10_spl
| ~ sQ39_spl
| e23 = op2(e24,h(e15)) ),
inference(forward_demodulation,[status(thm)],[f447,f4163]) ).
fof(f4387,plain,
( ~ sQ10_spl
| ~ sQ39_spl
| e23 = op2(e24,e24) ),
inference(forward_demodulation,[status(thm)],[f447,f4386]) ).
fof(f4388,plain,
( ~ sQ10_spl
| ~ sQ39_spl
| e23 = e24 ),
inference(forward_demodulation,[status(thm)],[f180,f4387]) ).
fof(f4389,plain,
( ~ sQ10_spl
| ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4388,f44]) ).
fof(f4390,plain,
( ~ sQ10_spl
| ~ sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f4389]) ).
fof(f4391,plain,
( ~ sQ2_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f4274,f522,f330]) ).
fof(f4404,plain,
( ~ sQ50_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f2856,f346,f481]) ).
fof(f4413,plain,
( ~ sQ54_spl
| ~ sQ82_spl
| sQ71_spl ),
inference(split_clause,[status(thm)],[f4362,f547,f581,f493]) ).
fof(f4476,plain,
( ~ sQ85_spl
| e11 = op1(j(e24),j(e21)) ),
inference(forward_demodulation,[status(thm)],[f592,f1570]) ).
fof(f4477,plain,
( ~ sQ85_spl
| ~ sQ82_spl
| e11 = op1(e15,j(e21)) ),
inference(forward_demodulation,[status(thm)],[f582,f4476]) ).
fof(f4478,plain,
( ~ sQ85_spl
| ~ sQ82_spl
| ~ sQ62_spl
| e11 = op1(e15,e16) ),
inference(forward_demodulation,[status(thm)],[f519,f4477]) ).
fof(f4479,plain,
( ~ sQ85_spl
| ~ sQ82_spl
| ~ sQ62_spl
| e11 = e16 ),
inference(forward_demodulation,[status(thm)],[f140,f4478]) ).
fof(f4480,plain,
( ~ sQ85_spl
| ~ sQ82_spl
| ~ sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4479,f18]) ).
fof(f4481,plain,
( ~ sQ85_spl
| ~ sQ82_spl
| ~ sQ62_spl ),
inference(contradiction_clause,[status(thm)],[f4480]) ).
fof(f4493,plain,
( ~ sQ8_spl
| ~ sQ39_spl
| e26 = op2(e24,e26) ),
inference(forward_demodulation,[status(thm)],[f447,f4110]) ).
fof(f4494,plain,
( ~ sQ8_spl
| ~ sQ39_spl
| e26 = e21 ),
inference(forward_demodulation,[status(thm)],[f182,f4493]) ).
fof(f4495,plain,
( ~ sQ8_spl
| ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4494,f39]) ).
fof(f4496,plain,
( ~ sQ8_spl
| ~ sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f4495]) ).
fof(f4508,plain,
( ~ sQ9_spl
| ~ sQ39_spl
| e22 = op2(e24,h(e15)) ),
inference(forward_demodulation,[status(thm)],[f447,f1253]) ).
fof(f4509,plain,
( ~ sQ9_spl
| ~ sQ39_spl
| e22 = op2(e24,e24) ),
inference(forward_demodulation,[status(thm)],[f447,f4508]) ).
fof(f4510,plain,
( ~ sQ9_spl
| ~ sQ39_spl
| e22 = e24 ),
inference(forward_demodulation,[status(thm)],[f180,f4509]) ).
fof(f4511,plain,
( ~ sQ9_spl
| ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4510,f41]) ).
fof(f4512,plain,
( ~ sQ9_spl
| ~ sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f4511]) ).
fof(f4513,plain,
$false,
inference(sat_refutation,[status(thm)],[f367,f521,f587,f694,f712,f719,f722,f734,f737,f740,f764,f779,f784,f790,f808,f814,f827,f879,f882,f885,f888,f901,f922,f928,f931,f934,f937,f940,f943,f946,f961,f999,f1026,f1052,f1060,f1220,f1269,f1285,f1413,f1416,f1419,f1461,f1468,f1471,f1504,f1515,f1532,f1598,f1745,f1753,f1754,f1794,f1795,f1800,f1812,f1816,f1831,f1838,f1880,f1881,f1885,f1886,f1907,f1939,f1944,f1966,f1995,f2000,f2005,f2043,f2049,f2059,f2075,f2084,f2088,f2125,f2131,f2201,f2202,f2278,f2301,f2329,f2348,f2358,f2459,f2524,f2552,f2561,f2568,f2577,f2580,f2581,f2591,f2604,f2680,f2685,f2710,f2711,f2712,f2730,f2845,f2903,f2929,f2950,f3007,f3061,f3087,f3120,f3121,f3132,f3158,f3172,f3234,f3270,f3272,f3307,f3314,f3348,f3370,f3381,f3382,f3394,f3491,f3520,f3527,f3542,f3583,f3699,f3701,f3779,f3874,f3901,f3943,f3944,f3969,f3970,f3973,f4050,f4055,f4065,f4084,f4088,f4089,f4090,f4091,f4130,f4143,f4215,f4240,f4301,f4306,f4349,f4360,f4372,f4377,f4390,f4391,f4404,f4413,f4481,f4496,f4512]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG205+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n026.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 13:04:06 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 0.14/0.49 % Refutation found
% 0.14/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.52 % Elapsed time: 0.156914 seconds
% 0.14/0.52 % CPU time: 0.858400 seconds
% 0.14/0.52 % Total memory used: 133.005 MB
% 0.14/0.52 % Net memory used: 132.597 MB
%------------------------------------------------------------------------------