%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG185+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 : Tue Sep 29 09:18:07 AM UTC 2026
% Result : Theorem 4.53s 1.12s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 55
% Syntax : Number of formulae : 1218 ( 85 unt; 50 def)
% Number of atoms : 3958 (1166 equ)
% Maximal formula atoms : 110 ( 3 avg)
% Number of connectives : 5091 (2351 ~;2348 |; 340 &)
% ( 50 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 70 ( 4 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 52 ( 50 usr; 51 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e10 != e14
& e11 != e12
& e11 != e13
& e11 != e14
& e12 != e13
& e12 != e14
& e13 != e14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e20 != e24
& e21 != e22
& e21 != e23
& e21 != e24
& e22 != e23
& e22 != e24
& e23 != e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f4,axiom,
( op1(e10,e10) = e10
& op1(e10,e11) = e13
& op1(e10,e12) = e14
& op1(e10,e13) = e11
& op1(e10,e14) = e12
& op1(e11,e10) = e14
& op1(e11,e11) = e11
& op1(e11,e12) = e13
& op1(e11,e13) = e12
& op1(e11,e14) = e10
& op1(e12,e10) = e11
& op1(e12,e11) = e10
& op1(e12,e12) = e12
& op1(e12,e13) = e14
& op1(e12,e14) = e13
& op1(e13,e10) = e12
& op1(e13,e11) = e14
& op1(e13,e12) = e10
& op1(e13,e13) = e13
& op1(e13,e14) = e11
& op1(e14,e10) = e13
& op1(e14,e11) = e12
& op1(e14,e12) = e11
& op1(e14,e13) = e10
& op1(e14,e14) = e14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op2(e20,e20) = e20
& op2(e20,e21) = e23
& op2(e20,e22) = e24
& op2(e20,e23) = e22
& op2(e20,e24) = e21
& op2(e21,e20) = e22
& op2(e21,e21) = e21
& op2(e21,e22) = e23
& op2(e21,e23) = e24
& op2(e21,e24) = e20
& op2(e22,e20) = e21
& op2(e22,e21) = e24
& op2(e22,e22) = e22
& op2(e22,e23) = e20
& op2(e22,e24) = e23
& op2(e23,e20) = e24
& op2(e23,e21) = e20
& op2(e23,e22) = e21
& op2(e23,e23) = e23
& op2(e23,e24) = e22
& op2(e24,e20) = e23
& op2(e24,e21) = e22
& op2(e24,e22) = e20
& op2(e24,e23) = e21
& op2(e24,e24) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,conjecture,
( ( ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14 ) )
=> ~ ( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f7,negated_conjecture,
~ ( ( ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14 ) )
=> ~ ( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14 ) ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f8,plain,
( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14
& ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14 ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f9,plain,
( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14
& ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14 ) ),
inference(flattening,[],[f8]) ).
fof(f10,plain,
( e10 = j(e24)
| e11 = j(e24)
| e12 = j(e24)
| e13 = j(e24)
| e14 = j(e24) ),
inference(cnf_transformation,[],[f9]) ).
fof(f11,plain,
( e10 = j(e23)
| e11 = j(e23)
| e12 = j(e23)
| e13 = j(e23)
| e14 = j(e23) ),
inference(cnf_transformation,[],[f9]) ).
fof(f12,plain,
( e10 = j(e22)
| e11 = j(e22)
| e12 = j(e22)
| e13 = j(e22)
| e14 = j(e22) ),
inference(cnf_transformation,[],[f9]) ).
fof(f13,plain,
( e10 = j(e21)
| e11 = j(e21)
| e12 = j(e21)
| e13 = j(e21)
| e14 = j(e21) ),
inference(cnf_transformation,[],[f9]) ).
fof(f14,plain,
( e10 = j(e20)
| e11 = j(e20)
| e12 = j(e20)
| e13 = j(e20)
| e14 = j(e20) ),
inference(cnf_transformation,[],[f9]) ).
fof(f15,plain,
( e20 = h(e14)
| e21 = h(e14)
| e22 = h(e14)
| e23 = h(e14)
| e24 = h(e14) ),
inference(cnf_transformation,[],[f9]) ).
fof(f16,plain,
( e20 = h(e13)
| e21 = h(e13)
| e22 = h(e13)
| e23 = h(e13)
| e24 = h(e13) ),
inference(cnf_transformation,[],[f9]) ).
fof(f17,plain,
( e20 = h(e12)
| e21 = h(e12)
| e22 = h(e12)
| e23 = h(e12)
| e24 = h(e12) ),
inference(cnf_transformation,[],[f9]) ).
fof(f18,plain,
( e20 = h(e11)
| e21 = h(e11)
| e22 = h(e11)
| e23 = h(e11)
| e24 = h(e11) ),
inference(cnf_transformation,[],[f9]) ).
fof(f19,plain,
( e20 = h(e10)
| e21 = h(e10)
| e22 = h(e10)
| e23 = h(e10)
| e24 = h(e10) ),
inference(cnf_transformation,[],[f9]) ).
fof(f20,plain,
e14 = j(h(e14)),
inference(cnf_transformation,[],[f9]) ).
fof(f21,plain,
e13 = j(h(e13)),
inference(cnf_transformation,[],[f9]) ).
fof(f22,plain,
e12 = j(h(e12)),
inference(cnf_transformation,[],[f9]) ).
fof(f23,plain,
e11 = j(h(e11)),
inference(cnf_transformation,[],[f9]) ).
fof(f24,plain,
e10 = j(h(e10)),
inference(cnf_transformation,[],[f9]) ).
fof(f25,plain,
e24 = h(j(e24)),
inference(cnf_transformation,[],[f9]) ).
fof(f26,plain,
e23 = h(j(e23)),
inference(cnf_transformation,[],[f9]) ).
fof(f27,plain,
e22 = h(j(e22)),
inference(cnf_transformation,[],[f9]) ).
fof(f28,plain,
e21 = h(j(e21)),
inference(cnf_transformation,[],[f9]) ).
fof(f29,plain,
e20 = h(j(e20)),
inference(cnf_transformation,[],[f9]) ).
fof(f31,plain,
j(op2(e24,e23)) = op1(j(e24),j(e23)),
inference(cnf_transformation,[],[f9]) ).
fof(f32,plain,
j(op2(e24,e22)) = op1(j(e24),j(e22)),
inference(cnf_transformation,[],[f9]) ).
fof(f33,plain,
j(op2(e24,e21)) = op1(j(e24),j(e21)),
inference(cnf_transformation,[],[f9]) ).
fof(f34,plain,
j(op2(e24,e20)) = op1(j(e24),j(e20)),
inference(cnf_transformation,[],[f9]) ).
fof(f81,plain,
e21 = op2(e24,e23),
inference(cnf_transformation,[],[f5]) ).
fof(f82,plain,
e20 = op2(e24,e22),
inference(cnf_transformation,[],[f5]) ).
fof(f83,plain,
e22 = op2(e24,e21),
inference(cnf_transformation,[],[f5]) ).
fof(f84,plain,
e23 = op2(e24,e20),
inference(cnf_transformation,[],[f5]) ).
fof(f106,plain,
e10 = op1(e14,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f107,plain,
e11 = op1(e14,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f108,plain,
e12 = op1(e14,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f109,plain,
e13 = op1(e14,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f110,plain,
e11 = op1(e13,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f112,plain,
e10 = op1(e13,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f114,plain,
e12 = op1(e13,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f117,plain,
e12 = op1(e12,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f118,plain,
e10 = op1(e12,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f119,plain,
e11 = op1(e12,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f120,plain,
e10 = op1(e11,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f121,plain,
e12 = op1(e11,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f122,plain,
e13 = op1(e11,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f123,plain,
e11 = op1(e11,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f125,plain,
e12 = op1(e10,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f126,plain,
e11 = op1(e10,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f128,plain,
e13 = op1(e10,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f129,plain,
e10 = op1(e10,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f155,plain,
e23 != e24,
inference(cnf_transformation,[],[f2]) ).
fof(f156,plain,
e22 != e24,
inference(cnf_transformation,[],[f2]) ).
fof(f157,plain,
e22 != e23,
inference(cnf_transformation,[],[f2]) ).
fof(f158,plain,
e21 != e24,
inference(cnf_transformation,[],[f2]) ).
fof(f159,plain,
e21 != e23,
inference(cnf_transformation,[],[f2]) ).
fof(f160,plain,
e21 != e22,
inference(cnf_transformation,[],[f2]) ).
fof(f161,plain,
e20 != e24,
inference(cnf_transformation,[],[f2]) ).
fof(f162,plain,
e20 != e23,
inference(cnf_transformation,[],[f2]) ).
fof(f163,plain,
e20 != e22,
inference(cnf_transformation,[],[f2]) ).
fof(f164,plain,
e20 != e21,
inference(cnf_transformation,[],[f2]) ).
fof(f165,plain,
e13 != e14,
inference(cnf_transformation,[],[f1]) ).
fof(f166,plain,
e12 != e14,
inference(cnf_transformation,[],[f1]) ).
fof(f167,plain,
e12 != e13,
inference(cnf_transformation,[],[f1]) ).
fof(f168,plain,
e11 != e14,
inference(cnf_transformation,[],[f1]) ).
fof(f169,plain,
e11 != e13,
inference(cnf_transformation,[],[f1]) ).
fof(f170,plain,
e11 != e12,
inference(cnf_transformation,[],[f1]) ).
fof(f171,plain,
e10 != e14,
inference(cnf_transformation,[],[f1]) ).
fof(f172,plain,
e10 != e13,
inference(cnf_transformation,[],[f1]) ).
fof(f173,plain,
e10 != e12,
inference(cnf_transformation,[],[f1]) ).
fof(f174,plain,
e10 != e11,
inference(cnf_transformation,[],[f1]) ).
fof(f176,definition,
( spl0_1
<=> e14 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f177,plain,
( e14 != j(e24)
| spl0_1 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f178,plain,
( e14 = j(e24)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f180,definition,
( spl0_2
<=> e13 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f181,plain,
( e13 != j(e24)
| spl0_2 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f182,plain,
( e13 = j(e24)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f184,definition,
( spl0_3
<=> e12 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f186,plain,
( e12 = j(e24)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f184]) ).
fof(f188,definition,
( spl0_4
<=> e11 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f190,plain,
( e11 = j(e24)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f192,definition,
( spl0_5
<=> e10 = j(e24) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f194,plain,
( e10 = j(e24)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f195,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f10,f192,f188,f184,f180,f176]) ).
fof(f197,definition,
( spl0_6
<=> e14 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f199,plain,
( e14 = j(e23)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f197]) ).
fof(f201,definition,
( spl0_7
<=> e13 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f202,plain,
( e13 != j(e23)
| spl0_7 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f203,plain,
( e13 = j(e23)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f205,definition,
( spl0_8
<=> e12 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f207,plain,
( e12 = j(e23)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f209,definition,
( spl0_9
<=> e11 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f211,plain,
( e11 = j(e23)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f213,definition,
( spl0_10
<=> e10 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f215,plain,
( e10 = j(e23)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f216,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10 ),
inference(avatar_split_clause,[],[f11,f213,f209,f205,f201,f197]) ).
fof(f218,definition,
( spl0_11
<=> e14 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f219,plain,
( e14 != j(e22)
| spl0_11 ),
inference(avatar_component_clause,[],[f218]) ).
fof(f220,plain,
( e14 = j(e22)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f218]) ).
fof(f222,definition,
( spl0_12
<=> e13 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f224,plain,
( e13 = j(e22)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f226,definition,
( spl0_13
<=> e12 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f227,plain,
( e12 != j(e22)
| spl0_13 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f228,plain,
( e12 = j(e22)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f230,definition,
( spl0_14
<=> e11 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f231,plain,
( e11 != j(e22)
| spl0_14 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f232,plain,
( e11 = j(e22)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f234,definition,
( spl0_15
<=> e10 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f236,plain,
( e10 = j(e22)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f234]) ).
fof(f237,plain,
( spl0_11
| spl0_12
| spl0_13
| spl0_14
| spl0_15 ),
inference(avatar_split_clause,[],[f12,f234,f230,f226,f222,f218]) ).
fof(f239,definition,
( spl0_16
<=> e14 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f240,plain,
( e14 != j(e21)
| spl0_16 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f241,plain,
( e14 = j(e21)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f243,definition,
( spl0_17
<=> e13 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f245,plain,
( e13 = j(e21)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f247,definition,
( spl0_18
<=> e12 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f248,plain,
( e12 != j(e21)
| spl0_18 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f249,plain,
( e12 = j(e21)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f251,definition,
( spl0_19
<=> e11 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f253,plain,
( e11 = j(e21)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f255,definition,
( spl0_20
<=> e10 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f257,plain,
( e10 = j(e21)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f258,plain,
( spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(avatar_split_clause,[],[f13,f255,f251,f247,f243,f239]) ).
fof(f260,definition,
( spl0_21
<=> e14 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f261,plain,
( e14 != j(e20)
| spl0_21 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f262,plain,
( e14 = j(e20)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f264,definition,
( spl0_22
<=> e13 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f265,plain,
( e13 != j(e20)
| spl0_22 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f266,plain,
( e13 = j(e20)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f268,definition,
( spl0_23
<=> e12 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f269,plain,
( e12 != j(e20)
| spl0_23 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f270,plain,
( e12 = j(e20)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f272,definition,
( spl0_24
<=> e11 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f274,plain,
( e11 = j(e20)
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f272]) ).
fof(f276,definition,
( spl0_25
<=> e10 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f278,plain,
( e10 = j(e20)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f279,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_25 ),
inference(avatar_split_clause,[],[f14,f276,f272,f268,f264,f260]) ).
fof(f281,definition,
( spl0_26
<=> e24 = h(e14) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f283,plain,
( e24 = h(e14)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f285,definition,
( spl0_27
<=> e23 = h(e14) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f287,plain,
( e23 = h(e14)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f289,definition,
( spl0_28
<=> e22 = h(e14) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f291,plain,
( e22 = h(e14)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f293,definition,
( spl0_29
<=> e21 = h(e14) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f295,plain,
( e21 = h(e14)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f297,definition,
( spl0_30
<=> e20 = h(e14) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f299,plain,
( e20 = h(e14)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f300,plain,
( spl0_26
| spl0_27
| spl0_28
| spl0_29
| spl0_30 ),
inference(avatar_split_clause,[],[f15,f297,f293,f289,f285,f281]) ).
fof(f302,definition,
( spl0_31
<=> e24 = h(e13) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f304,plain,
( e24 = h(e13)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f306,definition,
( spl0_32
<=> e23 = h(e13) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f308,plain,
( e23 = h(e13)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f310,definition,
( spl0_33
<=> e22 = h(e13) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f312,plain,
( e22 = h(e13)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f314,definition,
( spl0_34
<=> e21 = h(e13) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f316,plain,
( e21 = h(e13)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f314]) ).
fof(f318,definition,
( spl0_35
<=> e20 = h(e13) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f320,plain,
( e20 = h(e13)
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f321,plain,
( spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35 ),
inference(avatar_split_clause,[],[f16,f318,f314,f310,f306,f302]) ).
fof(f323,definition,
( spl0_36
<=> e24 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f325,plain,
( e24 = h(e12)
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f327,definition,
( spl0_37
<=> e23 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f329,plain,
( e23 = h(e12)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f331,definition,
( spl0_38
<=> e22 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f333,plain,
( e22 = h(e12)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f331]) ).
fof(f335,definition,
( spl0_39
<=> e21 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f337,plain,
( e21 = h(e12)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f339,definition,
( spl0_40
<=> e20 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f341,plain,
( e20 = h(e12)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f342,plain,
( spl0_36
| spl0_37
| spl0_38
| spl0_39
| spl0_40 ),
inference(avatar_split_clause,[],[f17,f339,f335,f331,f327,f323]) ).
fof(f344,definition,
( spl0_41
<=> e24 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f346,plain,
( e24 = h(e11)
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f348,definition,
( spl0_42
<=> e23 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f350,plain,
( e23 = h(e11)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f352,definition,
( spl0_43
<=> e22 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f354,plain,
( e22 = h(e11)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f356,definition,
( spl0_44
<=> e21 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f358,plain,
( e21 = h(e11)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f360,definition,
( spl0_45
<=> e20 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f362,plain,
( e20 = h(e11)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f363,plain,
( spl0_41
| spl0_42
| spl0_43
| spl0_44
| spl0_45 ),
inference(avatar_split_clause,[],[f18,f360,f356,f352,f348,f344]) ).
fof(f365,definition,
( spl0_46
<=> e24 = h(e10) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f367,plain,
( e24 = h(e10)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f369,definition,
( spl0_47
<=> e23 = h(e10) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f371,plain,
( e23 = h(e10)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f373,definition,
( spl0_48
<=> e22 = h(e10) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f375,plain,
( e22 = h(e10)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f373]) ).
fof(f377,definition,
( spl0_49
<=> e21 = h(e10) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f379,plain,
( e21 = h(e10)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f381,definition,
( spl0_50
<=> e20 = h(e10) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f383,plain,
( e20 = h(e10)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f381]) ).
fof(f384,plain,
( spl0_46
| spl0_47
| spl0_48
| spl0_49
| spl0_50 ),
inference(avatar_split_clause,[],[f19,f381,f377,f373,f369,f365]) ).
fof(f386,plain,
j(e21) = op1(j(e24),j(e23)),
inference(forward_demodulation,[],[f31,f81]) ).
fof(f387,plain,
j(e20) = op1(j(e24),j(e22)),
inference(forward_demodulation,[],[f32,f82]) ).
fof(f388,plain,
j(e22) = op1(j(e24),j(e21)),
inference(forward_demodulation,[],[f33,f83]) ).
fof(f389,plain,
j(e23) = op1(j(e24),j(e20)),
inference(forward_demodulation,[],[f34,f84]) ).
fof(f435,plain,
( e14 = j(e24)
| ~ spl0_26 ),
inference(superposition,[],[f20,f283]) ).
fof(f436,plain,
( e13 = e14
| ~ spl0_2
| ~ spl0_26 ),
inference(forward_demodulation,[],[f435,f182]) ).
fof(f437,plain,
( $false
| ~ spl0_2
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f436,f165]) ).
fof(f438,plain,
( ~ spl0_2
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f437]) ).
fof(f440,plain,
( e14 = j(e23)
| ~ spl0_27 ),
inference(superposition,[],[f20,f287]) ).
fof(f441,plain,
( e13 = j(e24)
| ~ spl0_31 ),
inference(superposition,[],[f21,f304]) ).
fof(f442,plain,
( e12 = j(e24)
| ~ spl0_36 ),
inference(superposition,[],[f22,f325]) ).
fof(f443,plain,
( spl0_3
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f442,f323,f184]) ).
fof(f445,plain,
( e12 = j(e23)
| ~ spl0_37 ),
inference(superposition,[],[f22,f329]) ).
fof(f446,plain,
( spl0_8
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f445,f327,f205]) ).
fof(f454,plain,
( e12 = e14
| ~ spl0_8
| ~ spl0_27 ),
inference(forward_demodulation,[],[f440,f207]) ).
fof(f455,plain,
( $false
| ~ spl0_8
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f454,f166]) ).
fof(f456,plain,
( ~ spl0_8
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f455]) ).
fof(f459,plain,
( e14 = j(e22)
| ~ spl0_28 ),
inference(superposition,[],[f20,f291]) ).
fof(f460,plain,
( e11 = j(e24)
| ~ spl0_41 ),
inference(superposition,[],[f23,f346]) ).
fof(f461,plain,
( spl0_4
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f460,f344,f188]) ).
fof(f463,plain,
( e11 = j(e23)
| ~ spl0_42 ),
inference(superposition,[],[f23,f350]) ).
fof(f464,plain,
( spl0_9
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f463,f348,f209]) ).
fof(f467,plain,
( e11 = j(e22)
| ~ spl0_43 ),
inference(superposition,[],[f23,f354]) ).
fof(f468,plain,
( spl0_14
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f467,f352,f230]) ).
fof(f469,plain,
( e11 = e14
| ~ spl0_11
| ~ spl0_14 ),
inference(superposition,[],[f232,f220]) ).
fof(f473,plain,
( $false
| ~ spl0_11
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f469,f168]) ).
fof(f474,plain,
( ~ spl0_11
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f473]) ).
fof(f479,plain,
( e11 = j(e21)
| ~ spl0_44 ),
inference(superposition,[],[f23,f358]) ).
fof(f480,plain,
( spl0_19
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f479,f356,f251]) ).
fof(f488,plain,
( e10 = j(e24)
| ~ spl0_46 ),
inference(superposition,[],[f24,f367]) ).
fof(f489,plain,
( spl0_5
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f488,f365,f192]) ).
fof(f491,plain,
( e10 = j(e23)
| ~ spl0_47 ),
inference(superposition,[],[f24,f371]) ).
fof(f492,plain,
( spl0_10
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f491,f369,f213]) ).
fof(f495,plain,
( e10 = j(e22)
| ~ spl0_48 ),
inference(superposition,[],[f24,f375]) ).
fof(f496,plain,
( spl0_15
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f495,f373,f234]) ).
fof(f500,plain,
( e10 = j(e21)
| ~ spl0_49 ),
inference(superposition,[],[f24,f379]) ).
fof(f501,plain,
( spl0_20
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f500,f377,f255]) ).
fof(f506,plain,
( e10 = j(e20)
| ~ spl0_50 ),
inference(superposition,[],[f24,f383]) ).
fof(f507,plain,
( spl0_25
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f506,f381,f276]) ).
fof(f508,plain,
( e10 = e14
| ~ spl0_21
| ~ spl0_25 ),
inference(superposition,[],[f278,f262]) ).
fof(f512,plain,
( $false
| ~ spl0_21
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f508,f171]) ).
fof(f513,plain,
( ~ spl0_21
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f512]) ).
fof(f533,plain,
( e13 = j(e22)
| ~ spl0_33 ),
inference(superposition,[],[f21,f312]) ).
fof(f534,plain,
( spl0_12
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f533,f310,f222]) ).
fof(f538,plain,
( e13 = j(e21)
| ~ spl0_34 ),
inference(superposition,[],[f21,f316]) ).
fof(f539,plain,
( e11 = e13
| ~ spl0_19
| ~ spl0_34 ),
inference(forward_demodulation,[],[f538,f253]) ).
fof(f540,plain,
( $false
| ~ spl0_19
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f539,f169]) ).
fof(f541,plain,
( ~ spl0_19
| ~ spl0_34 ),
inference(avatar_contradiction_clause,[],[f540]) ).
fof(f543,plain,
( spl0_17
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f538,f314,f243]) ).
fof(f556,plain,
( e11 = j(e20)
| ~ spl0_45 ),
inference(superposition,[],[f23,f362]) ).
fof(f557,plain,
( spl0_24
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f556,f360,f272]) ).
fof(f567,plain,
( e11 = e12
| ~ spl0_8
| ~ spl0_9 ),
inference(superposition,[],[f211,f207]) ).
fof(f571,plain,
( $false
| ~ spl0_8
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f567,f170]) ).
fof(f572,plain,
( ~ spl0_8
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[],[f571]) ).
fof(f590,plain,
( $false
| spl0_11
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f459,f219]) ).
fof(f591,plain,
( spl0_11
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f590]) ).
fof(f610,plain,
( e10 = e13
| ~ spl0_17
| ~ spl0_20 ),
inference(superposition,[],[f257,f245]) ).
fof(f614,plain,
( $false
| ~ spl0_17
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f610,f172]) ).
fof(f615,plain,
( ~ spl0_17
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f614]) ).
fof(f625,plain,
( e24 = h(e11)
| ~ spl0_4 ),
inference(superposition,[],[f25,f190]) ).
fof(f626,plain,
( e23 = h(e12)
| ~ spl0_8 ),
inference(superposition,[],[f26,f207]) ).
fof(f627,plain,
( e22 = h(e14)
| ~ spl0_11 ),
inference(superposition,[],[f27,f220]) ).
fof(f628,plain,
( e21 = h(e13)
| ~ spl0_17 ),
inference(superposition,[],[f28,f245]) ).
fof(f629,plain,
( e20 = h(e10)
| ~ spl0_25 ),
inference(superposition,[],[f29,f278]) ).
fof(f632,plain,
( j(e21) = op1(j(e24),e12)
| ~ spl0_8 ),
inference(superposition,[],[f386,f207]) ).
fof(f643,plain,
( j(e22) = op1(e11,j(e21))
| ~ spl0_4 ),
inference(superposition,[],[f388,f190]) ).
fof(f644,plain,
( j(e22) = op1(j(e24),e13)
| ~ spl0_17 ),
inference(superposition,[],[f388,f245]) ).
fof(f646,plain,
( op1(e11,e13) = j(e22)
| ~ spl0_4
| ~ spl0_17 ),
inference(forward_demodulation,[],[f643,f245]) ).
fof(f648,plain,
( e14 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_11
| ~ spl0_17 ),
inference(forward_demodulation,[],[f646,f220]) ).
fof(f650,plain,
( e12 = e14
| ~ spl0_4
| ~ spl0_11
| ~ spl0_17 ),
inference(forward_demodulation,[],[f648,f121]) ).
fof(f653,plain,
( $false
| ~ spl0_4
| ~ spl0_11
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f650,f166]) ).
fof(f654,plain,
( ~ spl0_4
| ~ spl0_11
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f653]) ).
fof(f662,plain,
( op1(e12,e12) = j(e21)
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_demodulation,[],[f632,f186]) ).
fof(f669,plain,
( e13 = op1(e12,e12)
| ~ spl0_3
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_demodulation,[],[f662,f245]) ).
fof(f672,plain,
( e12 = e13
| ~ spl0_3
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_demodulation,[],[f669,f117]) ).
fof(f673,plain,
( $false
| ~ spl0_3
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f672,f167]) ).
fof(f674,plain,
( ~ spl0_3
| ~ spl0_8
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f673]) ).
fof(f681,plain,
( op1(e10,e13) = j(e22)
| ~ spl0_5
| ~ spl0_17 ),
inference(forward_demodulation,[],[f644,f194]) ).
fof(f684,plain,
( e14 = op1(e10,e13)
| ~ spl0_5
| ~ spl0_11
| ~ spl0_17 ),
inference(forward_demodulation,[],[f681,f220]) ).
fof(f685,plain,
( e11 = e14
| ~ spl0_5
| ~ spl0_11
| ~ spl0_17 ),
inference(forward_demodulation,[],[f684,f126]) ).
fof(f686,plain,
( $false
| ~ spl0_5
| ~ spl0_11
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f685,f168]) ).
fof(f687,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f686]) ).
fof(f690,plain,
( e12 = op1(e10,e13)
| ~ spl0_5
| ~ spl0_13
| ~ spl0_17 ),
inference(forward_demodulation,[],[f681,f228]) ).
fof(f691,plain,
( e11 = e12
| ~ spl0_5
| ~ spl0_13
| ~ spl0_17 ),
inference(forward_demodulation,[],[f690,f126]) ).
fof(f692,plain,
( $false
| ~ spl0_5
| ~ spl0_13
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f691,f170]) ).
fof(f693,plain,
( ~ spl0_5
| ~ spl0_13
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f692]) ).
fof(f707,plain,
( j(e21) = op1(e10,j(e23))
| ~ spl0_5 ),
inference(superposition,[],[f386,f194]) ).
fof(f708,plain,
( j(e20) = op1(e10,j(e22))
| ~ spl0_5 ),
inference(superposition,[],[f387,f194]) ).
fof(f709,plain,
( j(e22) = op1(e10,j(e21))
| ~ spl0_5 ),
inference(superposition,[],[f388,f194]) ).
fof(f719,plain,
( e22 = h(e11)
| ~ spl0_14 ),
inference(superposition,[],[f27,f232]) ).
fof(f731,plain,
( spl0_34
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f628,f243,f314]) ).
fof(f735,plain,
( op1(e10,e13) = j(e21)
| ~ spl0_5
| ~ spl0_7 ),
inference(forward_demodulation,[],[f707,f203]) ).
fof(f738,plain,
( e13 = op1(e10,e13)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f735,f245]) ).
fof(f739,plain,
( e11 = e13
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f738,f126]) ).
fof(f740,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f739,f169]) ).
fof(f741,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f740]) ).
fof(f754,plain,
( e23 = h(e13)
| ~ spl0_7 ),
inference(superposition,[],[f26,f203]) ).
fof(f759,plain,
( e22 = h(e13)
| ~ spl0_12 ),
inference(superposition,[],[f27,f224]) ).
fof(f772,plain,
( e22 = h(e12)
| ~ spl0_13 ),
inference(superposition,[],[f27,f228]) ).
fof(f778,plain,
( spl0_33
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f759,f222,f310]) ).
fof(f787,plain,
( e22 = h(e13)
| ~ spl0_12 ),
inference(superposition,[],[f27,f224]) ).
fof(f791,plain,
( e21 = h(e11)
| ~ spl0_19 ),
inference(superposition,[],[f28,f253]) ).
fof(f794,plain,
( e20 = h(e11)
| ~ spl0_24 ),
inference(superposition,[],[f29,f274]) ).
fof(f796,plain,
( spl0_45
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f794,f272,f360]) ).
fof(f806,plain,
( spl0_38
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f772,f226,f331]) ).
fof(f824,plain,
( e20 = h(e13)
| ~ spl0_22 ),
inference(superposition,[],[f29,f266]) ).
fof(f826,plain,
( spl0_35
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f824,f264,f318]) ).
fof(f831,plain,
( e14 = j(e20)
| ~ spl0_30 ),
inference(superposition,[],[f20,f299]) ).
fof(f832,plain,
( $false
| spl0_21
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f831,f261]) ).
fof(f833,plain,
( spl0_21
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f832]) ).
fof(f838,plain,
( e13 = e14
| ~ spl0_7
| ~ spl0_27 ),
inference(forward_demodulation,[],[f440,f203]) ).
fof(f840,plain,
( $false
| ~ spl0_7
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f838,f165]) ).
fof(f841,plain,
( ~ spl0_7
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f840]) ).
fof(f843,plain,
( e13 = e14
| ~ spl0_22
| ~ spl0_30 ),
inference(forward_demodulation,[],[f831,f266]) ).
fof(f846,plain,
( $false
| ~ spl0_22
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f843,f165]) ).
fof(f847,plain,
( ~ spl0_22
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f846]) ).
fof(f851,plain,
( e20 = h(e14)
| ~ spl0_21 ),
inference(superposition,[],[f29,f262]) ).
fof(f859,plain,
( e13 = j(e23)
| ~ spl0_32 ),
inference(superposition,[],[f21,f308]) ).
fof(f863,plain,
( e13 = j(e20)
| ~ spl0_35 ),
inference(superposition,[],[f21,f320]) ).
fof(f864,plain,
( $false
| spl0_22
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f863,f265]) ).
fof(f865,plain,
( spl0_22
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f864]) ).
fof(f873,plain,
( e20 = e23
| ~ spl0_7
| ~ spl0_35 ),
inference(forward_demodulation,[],[f754,f320]) ).
fof(f879,plain,
( $false
| ~ spl0_7
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f873,f162]) ).
fof(f880,plain,
( ~ spl0_7
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f879]) ).
fof(f888,plain,
( op1(e10,e13) = j(e20)
| ~ spl0_5
| ~ spl0_12 ),
inference(forward_demodulation,[],[f708,f224]) ).
fof(f893,plain,
( e12 = op1(e10,e13)
| ~ spl0_5
| ~ spl0_12
| ~ spl0_23 ),
inference(forward_demodulation,[],[f888,f270]) ).
fof(f894,plain,
( e11 = e12
| ~ spl0_5
| ~ spl0_12
| ~ spl0_23 ),
inference(forward_demodulation,[],[f893,f126]) ).
fof(f895,plain,
( $false
| ~ spl0_5
| ~ spl0_12
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f894,f170]) ).
fof(f896,plain,
( ~ spl0_5
| ~ spl0_12
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f895]) ).
fof(f897,plain,
( spl0_30
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f851,f260,f297]) ).
fof(f899,plain,
( e14 = op1(e10,e13)
| ~ spl0_5
| ~ spl0_12
| ~ spl0_21 ),
inference(forward_demodulation,[],[f888,f262]) ).
fof(f903,plain,
( op1(e10,e10) = j(e21)
| ~ spl0_5
| ~ spl0_10 ),
inference(forward_demodulation,[],[f707,f215]) ).
fof(f904,plain,
( e11 = e14
| ~ spl0_5
| ~ spl0_12
| ~ spl0_21 ),
inference(forward_demodulation,[],[f899,f126]) ).
fof(f905,plain,
( e11 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_10
| ~ spl0_19 ),
inference(forward_demodulation,[],[f903,f253]) ).
fof(f906,plain,
( $false
| ~ spl0_5
| ~ spl0_12
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f904,f168]) ).
fof(f907,plain,
( ~ spl0_5
| ~ spl0_12
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f906]) ).
fof(f908,plain,
( e10 = e11
| ~ spl0_5
| ~ spl0_10
| ~ spl0_19 ),
inference(forward_demodulation,[],[f905,f129]) ).
fof(f909,plain,
( $false
| ~ spl0_5
| ~ spl0_10
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f908,f174]) ).
fof(f910,plain,
( ~ spl0_5
| ~ spl0_10
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f909]) ).
fof(f914,plain,
( $false
| spl0_7
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f859,f202]) ).
fof(f915,plain,
( spl0_7
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f914]) ).
fof(f930,plain,
( e23 = h(e14)
| ~ spl0_6 ),
inference(superposition,[],[f26,f199]) ).
fof(f942,plain,
( e23 = h(e13)
| ~ spl0_7 ),
inference(superposition,[],[f26,f203]) ).
fof(f958,plain,
( e14 = j(e21)
| ~ spl0_29 ),
inference(superposition,[],[f20,f295]) ).
fof(f966,plain,
( e14 = j(e20)
| ~ spl0_30 ),
inference(superposition,[],[f20,f299]) ).
fof(f971,plain,
( e12 = j(e22)
| ~ spl0_38 ),
inference(superposition,[],[f22,f333]) ).
fof(f979,plain,
( j(e23) = op1(e10,j(e20))
| ~ spl0_5 ),
inference(superposition,[],[f389,f194]) ).
fof(f982,plain,
( op1(e10,e14) = j(e23)
| ~ spl0_5
| ~ spl0_21 ),
inference(forward_demodulation,[],[f979,f262]) ).
fof(f984,plain,
( e13 = op1(e10,e14)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_21 ),
inference(forward_demodulation,[],[f982,f203]) ).
fof(f986,plain,
( e12 = e13
| ~ spl0_5
| ~ spl0_7
| ~ spl0_21 ),
inference(forward_demodulation,[],[f984,f125]) ).
fof(f989,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f986,f167]) ).
fof(f990,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f989]) ).
fof(f1001,plain,
( op1(e10,e10) = j(e20)
| ~ spl0_5
| ~ spl0_15 ),
inference(forward_demodulation,[],[f708,f236]) ).
fof(f1002,plain,
( $false
| spl0_13
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f971,f227]) ).
fof(f1003,plain,
( spl0_13
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f1002]) ).
fof(f1011,plain,
( e14 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1001,f262]) ).
fof(f1013,plain,
( e10 = e14
| ~ spl0_5
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1011,f129]) ).
fof(f1014,plain,
( $false
| ~ spl0_5
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1013,f171]) ).
fof(f1015,plain,
( ~ spl0_5
| ~ spl0_15
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1014]) ).
fof(f1017,plain,
( spl0_43
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f719,f230,f352]) ).
fof(f1021,plain,
( op1(e10,e11) = j(e20)
| ~ spl0_5
| ~ spl0_14 ),
inference(forward_demodulation,[],[f708,f232]) ).
fof(f1032,plain,
( e11 = e14
| ~ spl0_9
| ~ spl0_27 ),
inference(forward_demodulation,[],[f440,f211]) ).
fof(f1038,plain,
( $false
| ~ spl0_9
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f1032,f168]) ).
fof(f1039,plain,
( ~ spl0_9
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f1038]) ).
fof(f1041,plain,
( e13 = e14
| ~ spl0_17
| ~ spl0_29 ),
inference(forward_demodulation,[],[f958,f245]) ).
fof(f1043,plain,
( $false
| ~ spl0_17
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f1041,f165]) ).
fof(f1044,plain,
( ~ spl0_17
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f1043]) ).
fof(f1045,plain,
( e10 = e14
| ~ spl0_10
| ~ spl0_27 ),
inference(forward_demodulation,[],[f440,f215]) ).
fof(f1053,plain,
( op1(e10,e10) = j(e21)
| ~ spl0_5
| ~ spl0_10 ),
inference(forward_demodulation,[],[f707,f215]) ).
fof(f1055,plain,
( $false
| ~ spl0_10
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f1045,f171]) ).
fof(f1056,plain,
( ~ spl0_10
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f1055]) ).
fof(f1057,plain,
( e13 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1053,f245]) ).
fof(f1058,plain,
( e10 = e13
| ~ spl0_5
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1057,f129]) ).
fof(f1059,plain,
( $false
| ~ spl0_5
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1058,f172]) ).
fof(f1060,plain,
( ~ spl0_5
| ~ spl0_10
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1059]) ).
fof(f1063,plain,
( op1(e10,e14) = j(e21)
| ~ spl0_5
| ~ spl0_6 ),
inference(forward_demodulation,[],[f707,f199]) ).
fof(f1065,plain,
( e13 = op1(e10,e14)
| ~ spl0_5
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1063,f245]) ).
fof(f1066,plain,
( e12 = e13
| ~ spl0_5
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1065,f125]) ).
fof(f1067,plain,
( $false
| ~ spl0_5
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1066,f167]) ).
fof(f1068,plain,
( ~ spl0_5
| ~ spl0_6
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1067]) ).
fof(f1070,plain,
( e12 = e13
| ~ spl0_23
| ~ spl0_35 ),
inference(forward_demodulation,[],[f863,f270]) ).
fof(f1078,plain,
( $false
| ~ spl0_23
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1070,f167]) ).
fof(f1079,plain,
( ~ spl0_23
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f1078]) ).
fof(f1084,plain,
( spl0_44
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f791,f251,f356]) ).
fof(f1086,plain,
( e14 = op1(e10,j(e20))
| ~ spl0_5
| ~ spl0_6 ),
inference(forward_demodulation,[],[f979,f199]) ).
fof(f1087,plain,
( e13 = j(e20)
| ~ spl0_5
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1021,f128]) ).
fof(f1091,plain,
( e14 = op1(e10,e13)
| ~ spl0_5
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1086,f266]) ).
fof(f1093,plain,
( e11 = e14
| ~ spl0_5
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1091,f126]) ).
fof(f1094,plain,
( $false
| ~ spl0_5
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1093,f168]) ).
fof(f1095,plain,
( ~ spl0_5
| ~ spl0_6
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f1094]) ).
fof(f1099,plain,
( e12 = e14
| ~ spl0_18
| ~ spl0_29 ),
inference(forward_demodulation,[],[f958,f249]) ).
fof(f1106,plain,
( op1(e10,e13) = j(e23)
| ~ spl0_5
| ~ spl0_22 ),
inference(forward_demodulation,[],[f979,f266]) ).
fof(f1107,plain,
( $false
| ~ spl0_18
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f1099,f166]) ).
fof(f1108,plain,
( ~ spl0_18
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f1107]) ).
fof(f1111,plain,
( e12 = op1(e10,e13)
| ~ spl0_5
| ~ spl0_8
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1106,f207]) ).
fof(f1113,plain,
( e11 = e12
| ~ spl0_5
| ~ spl0_8
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1111,f126]) ).
fof(f1116,plain,
( $false
| ~ spl0_5
| ~ spl0_8
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1113,f170]) ).
fof(f1117,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f1116]) ).
fof(f1122,plain,
( op1(e10,e10) = j(e21)
| ~ spl0_5
| ~ spl0_10 ),
inference(forward_demodulation,[],[f707,f215]) ).
fof(f1125,plain,
( e14 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1122,f241]) ).
fof(f1126,plain,
( e10 = e14
| ~ spl0_5
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1125,f129]) ).
fof(f1127,plain,
( $false
| ~ spl0_5
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1126,f171]) ).
fof(f1128,plain,
( ~ spl0_5
| ~ spl0_10
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1127]) ).
fof(f1130,plain,
( op1(e10,e11) = j(e21)
| ~ spl0_5
| ~ spl0_9 ),
inference(forward_demodulation,[],[f707,f211]) ).
fof(f1132,plain,
( e14 = op1(e10,e11)
| ~ spl0_5
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1130,f241]) ).
fof(f1133,plain,
( e13 = e14
| ~ spl0_5
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1132,f128]) ).
fof(f1134,plain,
( $false
| ~ spl0_5
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1133,f165]) ).
fof(f1135,plain,
( ~ spl0_5
| ~ spl0_9
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1134]) ).
fof(f1140,plain,
( $false
| spl0_16
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f958,f240]) ).
fof(f1141,plain,
( spl0_16
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f1140]) ).
fof(f1142,plain,
( op1(e10,e10) = j(e22)
| ~ spl0_5
| ~ spl0_20 ),
inference(forward_demodulation,[],[f709,f257]) ).
fof(f1144,plain,
( op1(e10,e10) = j(e21)
| ~ spl0_5
| ~ spl0_10 ),
inference(forward_demodulation,[],[f707,f215]) ).
fof(f1152,plain,
( spl0_28
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f627,f218,f289]) ).
fof(f1156,plain,
( op1(e10,e14) = j(e20)
| ~ spl0_5
| ~ spl0_11 ),
inference(forward_demodulation,[],[f708,f220]) ).
fof(f1157,plain,
( e14 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_11
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1142,f220]) ).
fof(f1158,plain,
( e13 = op1(e10,e14)
| ~ spl0_5
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1156,f266]) ).
fof(f1159,plain,
( e10 = e14
| ~ spl0_5
| ~ spl0_11
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1157,f129]) ).
fof(f1160,plain,
( e12 = e13
| ~ spl0_5
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1158,f125]) ).
fof(f1161,plain,
( $false
| ~ spl0_5
| ~ spl0_11
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1159,f171]) ).
fof(f1162,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f1161]) ).
fof(f1163,plain,
( $false
| ~ spl0_5
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1160,f167]) ).
fof(f1164,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f1163]) ).
fof(f1168,plain,
( op1(e10,e11) = j(e23)
| ~ spl0_5
| ~ spl0_24 ),
inference(forward_demodulation,[],[f979,f274]) ).
fof(f1172,plain,
( e12 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_10
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1144,f249]) ).
fof(f1175,plain,
( e10 = e12
| ~ spl0_5
| ~ spl0_10
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1172,f129]) ).
fof(f1176,plain,
( $false
| ~ spl0_5
| ~ spl0_10
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1175,f173]) ).
fof(f1177,plain,
( ~ spl0_5
| ~ spl0_10
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1176]) ).
fof(f1186,plain,
( op1(e10,e14) = j(e22)
| ~ spl0_5
| ~ spl0_16 ),
inference(forward_demodulation,[],[f709,f241]) ).
fof(f1195,plain,
( e13 = op1(e10,e14)
| ~ spl0_5
| ~ spl0_12
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1186,f224]) ).
fof(f1198,plain,
( e12 = e13
| ~ spl0_5
| ~ spl0_12
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1195,f125]) ).
fof(f1199,plain,
( $false
| ~ spl0_5
| ~ spl0_12
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1198,f167]) ).
fof(f1200,plain,
( ~ spl0_5
| ~ spl0_12
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1199]) ).
fof(f1212,plain,
( e14 = op1(e10,e11)
| ~ spl0_5
| ~ spl0_6
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1168,f199]) ).
fof(f1215,plain,
( e13 = e14
| ~ spl0_5
| ~ spl0_6
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1212,f128]) ).
fof(f1217,plain,
( $false
| ~ spl0_5
| ~ spl0_6
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1215,f165]) ).
fof(f1218,plain,
( ~ spl0_5
| ~ spl0_6
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f1217]) ).
fof(f1222,plain,
( spl0_50
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f629,f276,f381]) ).
fof(f1226,plain,
( op1(e10,e10) = j(e23)
| ~ spl0_5
| ~ spl0_25 ),
inference(forward_demodulation,[],[f979,f278]) ).
fof(f1231,plain,
( e14 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_6
| ~ spl0_25 ),
inference(forward_demodulation,[],[f1226,f199]) ).
fof(f1233,plain,
( e10 = e14
| ~ spl0_5
| ~ spl0_6
| ~ spl0_25 ),
inference(forward_demodulation,[],[f1231,f129]) ).
fof(f1234,plain,
( $false
| ~ spl0_5
| ~ spl0_6
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f1233,f171]) ).
fof(f1235,plain,
( ~ spl0_5
| ~ spl0_6
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f1234]) ).
fof(f1238,plain,
( e13 = e14
| ~ spl0_12
| ~ spl0_28 ),
inference(forward_demodulation,[],[f459,f224]) ).
fof(f1249,plain,
( $false
| ~ spl0_12
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f1238,f165]) ).
fof(f1250,plain,
( ~ spl0_12
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f1249]) ).
fof(f1253,plain,
( spl0_32
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f754,f201,f306]) ).
fof(f1255,plain,
( spl0_22
| ~ spl0_5
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f1087,f230,f192,f264]) ).
fof(f1274,plain,
( op1(e10,e13) = j(e21)
| ~ spl0_5
| ~ spl0_7 ),
inference(forward_demodulation,[],[f707,f203]) ).
fof(f1278,plain,
( e14 = op1(e10,e13)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1274,f241]) ).
fof(f1279,plain,
( e11 = e14
| ~ spl0_5
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1278,f126]) ).
fof(f1280,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1279,f168]) ).
fof(f1281,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1280]) ).
fof(f1289,plain,
( op1(e10,e11) = j(e22)
| ~ spl0_5
| ~ spl0_19 ),
inference(forward_demodulation,[],[f709,f253]) ).
fof(f1293,plain,
( e14 = op1(e10,e11)
| ~ spl0_5
| ~ spl0_11
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1289,f220]) ).
fof(f1295,plain,
( e13 = e14
| ~ spl0_5
| ~ spl0_11
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1293,f128]) ).
fof(f1296,plain,
( $false
| ~ spl0_5
| ~ spl0_11
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1295,f165]) ).
fof(f1297,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1296]) ).
fof(f1302,plain,
( e12 = op1(e10,e13)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1274,f249]) ).
fof(f1304,plain,
( e11 = e12
| ~ spl0_5
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1302,f126]) ).
fof(f1305,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1304,f170]) ).
fof(f1306,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1305]) ).
fof(f1312,plain,
( e12 = e14
| ~ spl0_23
| ~ spl0_30 ),
inference(forward_demodulation,[],[f966,f270]) ).
fof(f1332,plain,
( $false
| ~ spl0_23
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f1312,f166]) ).
fof(f1333,plain,
( ~ spl0_23
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f1332]) ).
fof(f1335,plain,
( e24 = h(e12)
| ~ spl0_3 ),
inference(superposition,[],[f25,f186]) ).
fof(f1337,plain,
( j(e21) = op1(e12,j(e23))
| ~ spl0_3 ),
inference(superposition,[],[f386,f186]) ).
fof(f1338,plain,
( j(e20) = op1(e12,j(e22))
| ~ spl0_3 ),
inference(superposition,[],[f387,f186]) ).
fof(f1343,plain,
( op1(e12,e10) = j(e20)
| ~ spl0_3
| ~ spl0_15 ),
inference(forward_demodulation,[],[f1338,f236]) ).
fof(f1344,plain,
( op1(e12,e11) = j(e21)
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f1337,f211]) ).
fof(f1349,plain,
( e14 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1343,f262]) ).
fof(f1350,plain,
( e13 = op1(e12,e11)
| ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1344,f245]) ).
fof(f1351,plain,
( e11 = e14
| ~ spl0_3
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1349,f119]) ).
fof(f1352,plain,
( e10 = e13
| ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1350,f118]) ).
fof(f1353,plain,
( $false
| ~ spl0_3
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1351,f168]) ).
fof(f1354,plain,
( ~ spl0_3
| ~ spl0_15
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1353]) ).
fof(f1355,plain,
( $false
| ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1352,f172]) ).
fof(f1356,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1355]) ).
fof(f1361,plain,
( e24 = h(e14)
| ~ spl0_1 ),
inference(superposition,[],[f25,f178]) ).
fof(f1363,plain,
( j(e21) = op1(e14,j(e23))
| ~ spl0_1 ),
inference(superposition,[],[f386,f178]) ).
fof(f1370,plain,
( op1(e14,e11) = j(e21)
| ~ spl0_1
| ~ spl0_9 ),
inference(forward_demodulation,[],[f1363,f211]) ).
fof(f1376,plain,
( e13 = op1(e14,e11)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1370,f245]) ).
fof(f1378,plain,
( e12 = e13
| ~ spl0_1
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1376,f108]) ).
fof(f1381,plain,
( $false
| ~ spl0_1
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1378,f167]) ).
fof(f1382,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1381]) ).
fof(f1386,plain,
( e24 = h(e13)
| ~ spl0_2 ),
inference(superposition,[],[f25,f182]) ).
fof(f1390,plain,
( j(e20) = op1(e13,j(e22))
| ~ spl0_2 ),
inference(superposition,[],[f387,f182]) ).
fof(f1395,plain,
( op1(e13,e10) = j(e20)
| ~ spl0_2
| ~ spl0_15 ),
inference(forward_demodulation,[],[f1390,f236]) ).
fof(f1401,plain,
( e14 = op1(e13,e10)
| ~ spl0_2
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1395,f262]) ).
fof(f1403,plain,
( e12 = e14
| ~ spl0_2
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1401,f114]) ).
fof(f1404,plain,
( $false
| ~ spl0_2
| ~ spl0_15
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1403,f166]) ).
fof(f1405,plain,
( ~ spl0_2
| ~ spl0_15
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1404]) ).
fof(f1411,plain,
( e23 = e24
| ~ spl0_4
| ~ spl0_42 ),
inference(forward_demodulation,[],[f625,f350]) ).
fof(f1414,plain,
( $false
| ~ spl0_4
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f1411,f155]) ).
fof(f1415,plain,
( ~ spl0_4
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[],[f1414]) ).
fof(f1421,plain,
( j(e20) = op1(e11,j(e22))
| ~ spl0_4 ),
inference(superposition,[],[f387,f190]) ).
fof(f1445,plain,
( j(e21) = op1(j(e24),e10)
| ~ spl0_10 ),
inference(superposition,[],[f386,f215]) ).
fof(f1446,plain,
( e23 = h(e10)
| ~ spl0_10 ),
inference(superposition,[],[f26,f215]) ).
fof(f1447,plain,
( e22 = e23
| ~ spl0_10
| ~ spl0_48 ),
inference(forward_demodulation,[],[f1446,f375]) ).
fof(f1449,plain,
( $false
| ~ spl0_10
| ~ spl0_48 ),
inference(forward_subsumption_resolution,[],[f1447,f157]) ).
fof(f1450,plain,
( ~ spl0_10
| ~ spl0_48 ),
inference(avatar_contradiction_clause,[],[f1449]) ).
fof(f1458,plain,
( e22 = h(e10)
| ~ spl0_15 ),
inference(superposition,[],[f27,f236]) ).
fof(f1459,plain,
( spl0_48
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f1458,f234,f373]) ).
fof(f1466,plain,
( op1(e11,e12) = j(e20)
| ~ spl0_4
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1421,f228]) ).
fof(f1468,plain,
( e14 = op1(e11,e12)
| ~ spl0_4
| ~ spl0_13
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1466,f262]) ).
fof(f1469,plain,
( e13 = e14
| ~ spl0_4
| ~ spl0_13
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1468,f122]) ).
fof(f1470,plain,
( $false
| ~ spl0_4
| ~ spl0_13
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1469,f165]) ).
fof(f1471,plain,
( ~ spl0_4
| ~ spl0_13
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1470]) ).
fof(f1472,plain,
( e22 = e24
| ~ spl0_3
| ~ spl0_38 ),
inference(forward_demodulation,[],[f1335,f333]) ).
fof(f1476,plain,
( op1(e12,e10) = j(e21)
| ~ spl0_3
| ~ spl0_10 ),
inference(forward_demodulation,[],[f1445,f186]) ).
fof(f1477,plain,
( $false
| ~ spl0_3
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1472,f156]) ).
fof(f1478,plain,
( ~ spl0_3
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f1477]) ).
fof(f1481,plain,
( e13 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1476,f245]) ).
fof(f1482,plain,
( e11 = e13
| ~ spl0_3
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1481,f119]) ).
fof(f1483,plain,
( $false
| ~ spl0_3
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f1482,f169]) ).
fof(f1484,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f1483]) ).
fof(f1493,plain,
( e24 = h(e11)
| ~ spl0_4 ),
inference(superposition,[],[f25,f190]) ).
fof(f1499,plain,
( j(e20) = op1(e11,j(e22))
| ~ spl0_4 ),
inference(superposition,[],[f387,f190]) ).
fof(f1501,plain,
( j(e23) = op1(e11,j(e20))
| ~ spl0_4 ),
inference(superposition,[],[f389,f190]) ).
fof(f1502,plain,
( op1(e11,e14) = j(e23)
| ~ spl0_4
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1501,f262]) ).
fof(f1504,plain,
( op1(e11,e11) = j(e20)
| ~ spl0_4
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1499,f232]) ).
fof(f1508,plain,
( e14 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_14
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1504,f262]) ).
fof(f1510,plain,
( e11 = e14
| ~ spl0_4
| ~ spl0_14
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1508,f123]) ).
fof(f1511,plain,
( $false
| ~ spl0_4
| ~ spl0_14
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1510,f168]) ).
fof(f1512,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1511]) ).
fof(f1521,plain,
( e12 = op1(e11,e14)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1502,f207]) ).
fof(f1528,plain,
( e10 = e12
| ~ spl0_4
| ~ spl0_8
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1521,f120]) ).
fof(f1529,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1528,f173]) ).
fof(f1530,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1529]) ).
fof(f1531,plain,
( e20 = e24
| ~ spl0_1
| ~ spl0_30 ),
inference(forward_demodulation,[],[f1361,f299]) ).
fof(f1542,plain,
( $false
| ~ spl0_1
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f1531,f161]) ).
fof(f1543,plain,
( ~ spl0_1
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f1542]) ).
fof(f1546,plain,
( e21 = e24
| ~ spl0_2
| ~ spl0_34 ),
inference(forward_demodulation,[],[f1386,f316]) ).
fof(f1551,plain,
( $false
| ~ spl0_2
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f1546,f158]) ).
fof(f1552,plain,
( ~ spl0_2
| ~ spl0_34 ),
inference(avatar_contradiction_clause,[],[f1551]) ).
fof(f1557,plain,
( e20 = e24
| ~ spl0_4
| ~ spl0_45 ),
inference(forward_demodulation,[],[f1493,f362]) ).
fof(f1558,plain,
( e20 = e23
| ~ spl0_6
| ~ spl0_30 ),
inference(forward_demodulation,[],[f930,f299]) ).
fof(f1570,plain,
( $false
| ~ spl0_4
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f1557,f161]) ).
fof(f1571,plain,
( ~ spl0_4
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f1570]) ).
fof(f1572,plain,
( $false
| ~ spl0_6
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f1558,f162]) ).
fof(f1573,plain,
( ~ spl0_6
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f1572]) ).
fof(f1579,plain,
( e21 = e22
| ~ spl0_12
| ~ spl0_34 ),
inference(forward_demodulation,[],[f787,f316]) ).
fof(f1588,plain,
( $false
| ~ spl0_12
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f1579,f160]) ).
fof(f1589,plain,
( ~ spl0_12
| ~ spl0_34 ),
inference(avatar_contradiction_clause,[],[f1588]) ).
fof(f1593,plain,
( e21 = e23
| ~ spl0_7
| ~ spl0_34 ),
inference(forward_demodulation,[],[f942,f316]) ).
fof(f1600,plain,
( $false
| ~ spl0_7
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f1593,f159]) ).
fof(f1601,plain,
( ~ spl0_7
| ~ spl0_34 ),
inference(avatar_contradiction_clause,[],[f1600]) ).
fof(f1608,plain,
( $false
| spl0_2
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f441,f181]) ).
fof(f1609,plain,
( spl0_2
| ~ spl0_31 ),
inference(avatar_contradiction_clause,[],[f1608]) ).
fof(f1620,plain,
( e12 = e13
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f182,f186]) ).
fof(f1622,plain,
( $false
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f1620,f167]) ).
fof(f1623,plain,
( ~ spl0_2
| ~ spl0_3 ),
inference(avatar_contradiction_clause,[],[f1622]) ).
fof(f1633,plain,
( j(e20) = op1(e13,j(e22))
| ~ spl0_2 ),
inference(superposition,[],[f387,f182]) ).
fof(f1635,plain,
( j(e23) = op1(e13,j(e20))
| ~ spl0_2 ),
inference(superposition,[],[f389,f182]) ).
fof(f1636,plain,
( op1(e13,e14) = j(e23)
| ~ spl0_2
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1635,f262]) ).
fof(f1640,plain,
( e12 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1636,f207]) ).
fof(f1644,plain,
( e11 = e12
| ~ spl0_2
| ~ spl0_8
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1640,f110]) ).
fof(f1645,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1644,f170]) ).
fof(f1646,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1645]) ).
fof(f1660,plain,
( e23 = h(e11)
| ~ spl0_9 ),
inference(superposition,[],[f26,f211]) ).
fof(f1666,plain,
( e22 = e23
| ~ spl0_9
| ~ spl0_43 ),
inference(forward_demodulation,[],[f1660,f354]) ).
fof(f1669,plain,
( $false
| ~ spl0_9
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f1666,f157]) ).
fof(f1670,plain,
( ~ spl0_9
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f1669]) ).
fof(f1676,plain,
( op1(e13,e12) = j(e20)
| ~ spl0_2
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1633,f228]) ).
fof(f1678,plain,
( e14 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_13
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1676,f262]) ).
fof(f1679,plain,
( e10 = e14
| ~ spl0_2
| ~ spl0_13
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1678,f112]) ).
fof(f1680,plain,
( $false
| ~ spl0_2
| ~ spl0_13
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1679,f171]) ).
fof(f1681,plain,
( ~ spl0_2
| ~ spl0_13
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1680]) ).
fof(f1716,plain,
( j(e22) = op1(e12,j(e21))
| ~ spl0_3 ),
inference(superposition,[],[f388,f186]) ).
fof(f1719,plain,
( op1(e12,e10) = j(e22)
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1716,f257]) ).
fof(f1723,plain,
( e13 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_12
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1719,f224]) ).
fof(f1726,plain,
( e11 = e13
| ~ spl0_3
| ~ spl0_12
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1723,f119]) ).
fof(f1727,plain,
( $false
| ~ spl0_3
| ~ spl0_12
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1726,f169]) ).
fof(f1728,plain,
( ~ spl0_3
| ~ spl0_12
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f1727]) ).
fof(f1731,plain,
( e20 = e22
| ~ spl0_11
| ~ spl0_30 ),
inference(forward_demodulation,[],[f627,f299]) ).
fof(f1742,plain,
( $false
| ~ spl0_11
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f1731,f163]) ).
fof(f1743,plain,
( ~ spl0_11
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f1742]) ).
fof(f1747,plain,
( e21 = e23
| ~ spl0_10
| ~ spl0_49 ),
inference(forward_demodulation,[],[f1446,f379]) ).
fof(f1753,plain,
( $false
| ~ spl0_10
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f1747,f159]) ).
fof(f1754,plain,
( ~ spl0_10
| ~ spl0_49 ),
inference(avatar_contradiction_clause,[],[f1753]) ).
fof(f1757,plain,
( e24 = h(e13)
| ~ spl0_2 ),
inference(superposition,[],[f25,f182]) ).
fof(f1764,plain,
( j(e22) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f388,f182]) ).
fof(f1779,plain,
( j(e21) = op1(j(e24),e10)
| ~ spl0_10 ),
inference(superposition,[],[f386,f215]) ).
fof(f1780,plain,
( op1(e13,e10) = j(e21)
| ~ spl0_2
| ~ spl0_10 ),
inference(forward_demodulation,[],[f1779,f182]) ).
fof(f1783,plain,
( j(e20) = op1(j(e24),e11)
| ~ spl0_14 ),
inference(superposition,[],[f387,f232]) ).
fof(f1790,plain,
( e21 = h(e10)
| ~ spl0_20 ),
inference(superposition,[],[f28,f257]) ).
fof(f1797,plain,
( op1(e13,e12) = j(e22)
| ~ spl0_2
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1764,f249]) ).
fof(f1800,plain,
( e11 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_14
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1797,f232]) ).
fof(f1801,plain,
( e10 = e11
| ~ spl0_2
| ~ spl0_14
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1800,f112]) ).
fof(f1802,plain,
( $false
| ~ spl0_2
| ~ spl0_14
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1801,f174]) ).
fof(f1803,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1802]) ).
fof(f1809,plain,
( e14 = op1(e13,e10)
| ~ spl0_2
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1780,f241]) ).
fof(f1812,plain,
( e12 = e14
| ~ spl0_2
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1809,f114]) ).
fof(f1815,plain,
( $false
| ~ spl0_2
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1812,f166]) ).
fof(f1816,plain,
( ~ spl0_2
| ~ spl0_10
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1815]) ).
fof(f1819,plain,
( e11 = e13
| ~ spl0_12
| ~ spl0_14 ),
inference(forward_demodulation,[],[f224,f232]) ).
fof(f1820,plain,
( e11 = e13
| ~ spl0_14
| ~ spl0_33 ),
inference(forward_demodulation,[],[f533,f232]) ).
fof(f1828,plain,
( op1(e12,e11) = j(e20)
| ~ spl0_3
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1783,f186]) ).
fof(f1833,plain,
( $false
| ~ spl0_12
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1819,f169]) ).
fof(f1834,plain,
( ~ spl0_12
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1833]) ).
fof(f1835,plain,
( $false
| ~ spl0_14
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f1820,f169]) ).
fof(f1836,plain,
( ~ spl0_14
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f1835]) ).
fof(f1840,plain,
( e14 = op1(e12,e11)
| ~ spl0_3
| ~ spl0_14
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1828,f262]) ).
fof(f1842,plain,
( e10 = e14
| ~ spl0_3
| ~ spl0_14
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1840,f118]) ).
fof(f1845,plain,
( $false
| ~ spl0_3
| ~ spl0_14
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1842,f171]) ).
fof(f1846,plain,
( ~ spl0_3
| ~ spl0_14
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1845]) ).
fof(f1855,plain,
( j(e21) = op1(e12,j(e23))
| ~ spl0_3 ),
inference(superposition,[],[f386,f186]) ).
fof(f1857,plain,
( j(e22) = op1(e12,j(e21))
| ~ spl0_3 ),
inference(superposition,[],[f388,f186]) ).
fof(f1860,plain,
( op1(e12,e11) = j(e22)
| ~ spl0_3
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1857,f253]) ).
fof(f1862,plain,
( op1(e12,e10) = j(e21)
| ~ spl0_3
| ~ spl0_10 ),
inference(forward_demodulation,[],[f1855,f215]) ).
fof(f1864,plain,
( e13 = op1(e12,e11)
| ~ spl0_3
| ~ spl0_12
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1860,f224]) ).
fof(f1867,plain,
( e10 = e13
| ~ spl0_3
| ~ spl0_12
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1864,f118]) ).
fof(f1868,plain,
( $false
| ~ spl0_3
| ~ spl0_12
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1867,f172]) ).
fof(f1869,plain,
( ~ spl0_3
| ~ spl0_12
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1868]) ).
fof(f1874,plain,
( e14 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1862,f241]) ).
fof(f1877,plain,
( e11 = e14
| ~ spl0_3
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1874,f119]) ).
fof(f1880,plain,
( $false
| ~ spl0_3
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1877,f168]) ).
fof(f1881,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1880]) ).
fof(f1895,plain,
( j(e20) = op1(e11,j(e22))
| ~ spl0_4 ),
inference(superposition,[],[f387,f190]) ).
fof(f1897,plain,
( j(e23) = op1(e11,j(e20))
| ~ spl0_4 ),
inference(superposition,[],[f389,f190]) ).
fof(f1898,plain,
( op1(e11,e14) = j(e23)
| ~ spl0_4
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1897,f262]) ).
fof(f1900,plain,
( op1(e11,e13) = j(e20)
| ~ spl0_4
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1895,f224]) ).
fof(f1904,plain,
( e14 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_12
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1900,f262]) ).
fof(f1906,plain,
( e12 = e14
| ~ spl0_4
| ~ spl0_12
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1904,f121]) ).
fof(f1907,plain,
( $false
| ~ spl0_4
| ~ spl0_12
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1906,f166]) ).
fof(f1908,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1907]) ).
fof(f1916,plain,
( e13 = op1(e11,e14)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1898,f203]) ).
fof(f1919,plain,
( e10 = e13
| ~ spl0_4
| ~ spl0_7
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1916,f120]) ).
fof(f1920,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1919,f172]) ).
fof(f1921,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1920]) ).
fof(f1924,plain,
( e23 = e24
| ~ spl0_2
| ~ spl0_32 ),
inference(forward_demodulation,[],[f1757,f308]) ).
fof(f1927,plain,
( spl0_49
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f1790,f255,f377]) ).
fof(f1935,plain,
( $false
| ~ spl0_2
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1924,f155]) ).
fof(f1936,plain,
( ~ spl0_2
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f1935]) ).
fof(f1939,plain,
( spl0_26
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f1361,f176,f281]) ).
fof(f1955,plain,
( j(e23) = op1(e14,j(e20))
| ~ spl0_1 ),
inference(superposition,[],[f389,f178]) ).
fof(f1956,plain,
( op1(e14,e12) = j(e23)
| ~ spl0_1
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1955,f270]) ).
fof(f1960,plain,
( e13 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_7
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1956,f203]) ).
fof(f1964,plain,
( e11 = e13
| ~ spl0_1
| ~ spl0_7
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1960,f107]) ).
fof(f1965,plain,
( $false
| ~ spl0_1
| ~ spl0_7
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1964,f169]) ).
fof(f1966,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f1965]) ).
fof(f1975,plain,
( j(e21) = op1(j(e24),e13)
| ~ spl0_7 ),
inference(superposition,[],[f386,f203]) ).
fof(f1976,plain,
( op1(e14,e13) = j(e21)
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1975,f178]) ).
fof(f1988,plain,
( e21 = h(e10)
| ~ spl0_20 ),
inference(superposition,[],[f28,f257]) ).
fof(f1998,plain,
( e14 = j(e24)
| ~ spl0_26 ),
inference(superposition,[],[f20,f283]) ).
fof(f2003,plain,
( e12 = j(e21)
| ~ spl0_39 ),
inference(superposition,[],[f22,f337]) ).
fof(f2004,plain,
( $false
| spl0_18
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f2003,f248]) ).
fof(f2005,plain,
( spl0_18
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f2004]) ).
fof(f2010,plain,
( e12 = j(e20)
| ~ spl0_40 ),
inference(superposition,[],[f22,f341]) ).
fof(f2011,plain,
( $false
| spl0_23
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f2010,f269]) ).
fof(f2012,plain,
( spl0_23
| ~ spl0_40 ),
inference(avatar_contradiction_clause,[],[f2011]) ).
fof(f2036,plain,
( e12 = op1(e14,e13)
| ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1976,f249]) ).
fof(f2039,plain,
( e10 = e12
| ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2036,f106]) ).
fof(f2042,plain,
( $false
| ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2039,f173]) ).
fof(f2043,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2042]) ).
fof(f2051,plain,
( e11 = op1(e14,e13)
| ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1976,f253]) ).
fof(f2056,plain,
( e10 = e11
| ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2051,f106]) ).
fof(f2060,plain,
( $false
| ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2056,f174]) ).
fof(f2061,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2060]) ).
fof(f2062,plain,
( spl0_42
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f1660,f209,f348]) ).
fof(f2069,plain,
( e14 = op1(e14,e13)
| ~ spl0_1
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1976,f241]) ).
fof(f2072,plain,
( e10 = e14
| ~ spl0_1
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2069,f106]) ).
fof(f2075,plain,
( $false
| ~ spl0_1
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2072,f171]) ).
fof(f2076,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2075]) ).
fof(f2077,plain,
( e20 = e21
| ~ spl0_20
| ~ spl0_50 ),
inference(forward_demodulation,[],[f1790,f383]) ).
fof(f2078,plain,
( e20 = e21
| ~ spl0_20
| ~ spl0_50 ),
inference(forward_demodulation,[],[f1988,f383]) ).
fof(f2084,plain,
( $false
| ~ spl0_20
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f2077,f164]) ).
fof(f2085,plain,
( ~ spl0_20
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f2084]) ).
fof(f2086,plain,
( $false
| ~ spl0_20
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f2078,f164]) ).
fof(f2087,plain,
( ~ spl0_20
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f2086]) ).
fof(f2092,plain,
( op1(e14,e11) = j(e23)
| ~ spl0_1
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1955,f274]) ).
fof(f2094,plain,
( e13 = op1(e14,e11)
| ~ spl0_1
| ~ spl0_7
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2092,f203]) ).
fof(f2095,plain,
( e12 = e13
| ~ spl0_1
| ~ spl0_7
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2094,f108]) ).
fof(f2096,plain,
( $false
| ~ spl0_1
| ~ spl0_7
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f2095,f167]) ).
fof(f2097,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f2096]) ).
fof(f2112,plain,
( $false
| spl0_1
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f1998,f177]) ).
fof(f2113,plain,
( spl0_1
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f2112]) ).
fof(f2132,plain,
( j(e23) = op1(e12,j(e20))
| ~ spl0_3 ),
inference(superposition,[],[f389,f186]) ).
fof(f2133,plain,
( op1(e12,e12) = j(e23)
| ~ spl0_3
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2132,f270]) ).
fof(f2137,plain,
( e13 = op1(e12,e12)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2133,f203]) ).
fof(f2141,plain,
( e12 = e13
| ~ spl0_3
| ~ spl0_7
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2137,f117]) ).
fof(f2143,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f2141,f167]) ).
fof(f2144,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f2143]) ).
fof(f2149,plain,
( op1(e12,e10) = j(e23)
| ~ spl0_3
| ~ spl0_25 ),
inference(forward_demodulation,[],[f2132,f278]) ).
fof(f2151,plain,
( e13 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_25 ),
inference(forward_demodulation,[],[f2149,f203]) ).
fof(f2152,plain,
( e11 = e13
| ~ spl0_3
| ~ spl0_7
| ~ spl0_25 ),
inference(forward_demodulation,[],[f2151,f119]) ).
fof(f2153,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f2152,f169]) ).
fof(f2154,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f2153]) ).
fof(f2159,plain,
( op1(e12,e11) = j(e23)
| ~ spl0_3
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2132,f274]) ).
fof(f2162,plain,
( e13 = op1(e12,e11)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2159,f203]) ).
fof(f2164,plain,
( e10 = e13
| ~ spl0_3
| ~ spl0_7
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2162,f118]) ).
fof(f2165,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f2164,f172]) ).
fof(f2166,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f2165]) ).
fof(f2174,plain,
( op1(e11,e13) = j(e21)
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1975,f190]) ).
fof(f2175,plain,
( e14 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2174,f241]) ).
fof(f2176,plain,
( e12 = e14
| ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2175,f121]) ).
fof(f2177,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2176,f166]) ).
fof(f2178,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2177]) ).
fof(f2189,plain,
( j(e21) = op1(e11,j(e23))
| ~ spl0_4 ),
inference(superposition,[],[f386,f190]) ).
fof(f2190,plain,
( j(e20) = op1(e11,j(e22))
| ~ spl0_4 ),
inference(superposition,[],[f387,f190]) ).
fof(f2191,plain,
( j(e22) = op1(e11,j(e21))
| ~ spl0_4 ),
inference(superposition,[],[f388,f190]) ).
fof(f2192,plain,
( j(e23) = op1(e11,j(e20))
| ~ spl0_4 ),
inference(superposition,[],[f389,f190]) ).
fof(f2194,plain,
( op1(e11,e11) = j(e22)
| ~ spl0_4
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2191,f253]) ).
fof(f2195,plain,
( op1(e11,e14) = j(e20)
| ~ spl0_4
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2190,f220]) ).
fof(f2198,plain,
( e14 = op1(e11,e11)
| ~ spl0_4
| ~ spl0_11
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2194,f220]) ).
fof(f2199,plain,
( e12 = op1(e11,e14)
| ~ spl0_4
| ~ spl0_11
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2195,f270]) ).
fof(f2201,plain,
( e11 = e14
| ~ spl0_4
| ~ spl0_11
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2198,f123]) ).
fof(f2202,plain,
( e10 = e12
| ~ spl0_4
| ~ spl0_11
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2199,f120]) ).
fof(f2203,plain,
( $false
| ~ spl0_4
| ~ spl0_11
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2201,f168]) ).
fof(f2204,plain,
( ~ spl0_4
| ~ spl0_11
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2203]) ).
fof(f2205,plain,
( $false
| ~ spl0_4
| ~ spl0_11
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f2202,f173]) ).
fof(f2206,plain,
( ~ spl0_4
| ~ spl0_11
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f2205]) ).
fof(f2216,plain,
( op1(e11,e12) = j(e22)
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2191,f249]) ).
fof(f2219,plain,
( e14 = op1(e11,e12)
| ~ spl0_4
| ~ spl0_11
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2216,f220]) ).
fof(f2220,plain,
( e13 = e14
| ~ spl0_4
| ~ spl0_11
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2219,f122]) ).
fof(f2221,plain,
( $false
| ~ spl0_4
| ~ spl0_11
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2220,f165]) ).
fof(f2222,plain,
( ~ spl0_4
| ~ spl0_11
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2221]) ).
fof(f2233,plain,
( op1(e11,e13) = j(e23)
| ~ spl0_4
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2192,f266]) ).
fof(f2234,plain,
( e13 = op1(e11,e14)
| ~ spl0_4
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2195,f266]) ).
fof(f2241,plain,
( e10 = e13
| ~ spl0_4
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2234,f120]) ).
fof(f2244,plain,
( $false
| ~ spl0_4
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2241,f172]) ).
fof(f2245,plain,
( ~ spl0_4
| ~ spl0_11
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2244]) ).
fof(f2258,plain,
( e14 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2233,f199]) ).
fof(f2261,plain,
( e12 = e14
| ~ spl0_4
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2258,f121]) ).
fof(f2262,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2261,f166]) ).
fof(f2263,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2262]) ).
fof(f2264,plain,
( e22 = e23
| ~ spl0_8
| ~ spl0_38 ),
inference(forward_demodulation,[],[f626,f333]) ).
fof(f2270,plain,
( op1(e11,e14) = j(e22)
| ~ spl0_4
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2191,f241]) ).
fof(f2273,plain,
( op1(e11,e12) = j(e21)
| ~ spl0_4
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2189,f207]) ).
fof(f2275,plain,
( $false
| ~ spl0_8
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f2264,f157]) ).
fof(f2276,plain,
( ~ spl0_8
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f2275]) ).
fof(f2279,plain,
( e12 = op1(e11,e14)
| ~ spl0_4
| ~ spl0_13
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2270,f228]) ).
fof(f2280,plain,
( e14 = op1(e11,e12)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2273,f241]) ).
fof(f2281,plain,
( e10 = e12
| ~ spl0_4
| ~ spl0_13
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2279,f120]) ).
fof(f2282,plain,
( e13 = e14
| ~ spl0_4
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2280,f122]) ).
fof(f2283,plain,
( $false
| ~ spl0_4
| ~ spl0_13
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2281,f173]) ).
fof(f2284,plain,
( ~ spl0_4
| ~ spl0_13
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2283]) ).
fof(f2285,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2282,f165]) ).
fof(f2286,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2285]) ).
fof(f2287,plain,
( e11 = e14
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f178,f190]) ).
fof(f2288,plain,
( e20 = e23
| ~ spl0_10
| ~ spl0_50 ),
inference(forward_demodulation,[],[f1446,f383]) ).
fof(f2303,plain,
( $false
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f2287,f168]) ).
fof(f2304,plain,
( ~ spl0_1
| ~ spl0_4 ),
inference(avatar_contradiction_clause,[],[f2303]) ).
fof(f2305,plain,
( $false
| ~ spl0_10
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f2288,f162]) ).
fof(f2306,plain,
( ~ spl0_10
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f2305]) ).
fof(f2347,plain,
( op1(e11,e14) = j(e21)
| ~ spl0_4
| ~ spl0_6 ),
inference(forward_demodulation,[],[f2189,f199]) ).
fof(f2365,plain,
( e12 = e13
| ~ spl0_13
| ~ spl0_33 ),
inference(forward_demodulation,[],[f533,f228]) ).
fof(f2371,plain,
( e12 = op1(e11,e14)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2347,f249]) ).
fof(f2374,plain,
( $false
| ~ spl0_13
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f2365,f167]) ).
fof(f2375,plain,
( ~ spl0_13
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f2374]) ).
fof(f2377,plain,
( e10 = e12
| ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2371,f120]) ).
fof(f2379,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2377,f173]) ).
fof(f2380,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2379]) ).
fof(f2389,plain,
( op1(e11,e12) = j(e23)
| ~ spl0_4
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2192,f270]) ).
fof(f2394,plain,
( e14 = op1(e11,e12)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2389,f199]) ).
fof(f2397,plain,
( e13 = e14
| ~ spl0_4
| ~ spl0_6
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2394,f122]) ).
fof(f2398,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f2397,f165]) ).
fof(f2399,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f2398]) ).
fof(f2400,plain,
( e11 = e12
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f186,f190]) ).
fof(f2411,plain,
( op1(e11,e14) = j(e22)
| ~ spl0_4
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2191,f241]) ).
fof(f2413,plain,
( $false
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f2400,f170]) ).
fof(f2414,plain,
( ~ spl0_3
| ~ spl0_4 ),
inference(avatar_contradiction_clause,[],[f2413]) ).
fof(f2419,plain,
( e13 = op1(e11,e14)
| ~ spl0_4
| ~ spl0_12
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2411,f224]) ).
fof(f2421,plain,
( e10 = e13
| ~ spl0_4
| ~ spl0_12
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2419,f120]) ).
fof(f2424,plain,
( $false
| ~ spl0_4
| ~ spl0_12
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2421,f172]) ).
fof(f2425,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2424]) ).
fof(f2434,plain,
( e13 = op1(e11,e14)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2347,f245]) ).
fof(f2437,plain,
( e10 = e13
| ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2434,f120]) ).
fof(f2439,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2437,f172]) ).
fof(f2440,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2439]) ).
fof(f2455,plain,
( e24 = h(e14)
| ~ spl0_1 ),
inference(superposition,[],[f25,f178]) ).
fof(f2458,plain,
( j(e21) = op1(e14,j(e23))
| ~ spl0_1 ),
inference(superposition,[],[f386,f178]) ).
fof(f2459,plain,
( j(e20) = op1(e14,j(e22))
| ~ spl0_1 ),
inference(superposition,[],[f387,f178]) ).
fof(f2464,plain,
( op1(e14,e12) = j(e20)
| ~ spl0_1
| ~ spl0_13 ),
inference(forward_demodulation,[],[f2459,f228]) ).
fof(f2465,plain,
( op1(e14,e10) = j(e21)
| ~ spl0_1
| ~ spl0_10 ),
inference(forward_demodulation,[],[f2458,f215]) ).
fof(f2468,plain,
( e13 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_13
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2464,f266]) ).
fof(f2469,plain,
( e14 = op1(e14,e10)
| ~ spl0_1
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2465,f241]) ).
fof(f2470,plain,
( e11 = e13
| ~ spl0_1
| ~ spl0_13
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2468,f107]) ).
fof(f2471,plain,
( e13 = e14
| ~ spl0_1
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2469,f109]) ).
fof(f2472,plain,
( $false
| ~ spl0_1
| ~ spl0_13
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2470,f169]) ).
fof(f2473,plain,
( ~ spl0_1
| ~ spl0_13
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2472]) ).
fof(f2474,plain,
( $false
| ~ spl0_1
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2471,f165]) ).
fof(f2475,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2474]) ).
fof(f2486,plain,
( op1(e14,e11) = j(e20)
| ~ spl0_1
| ~ spl0_14 ),
inference(forward_demodulation,[],[f2459,f232]) ).
fof(f2488,plain,
( e13 = op1(e14,e11)
| ~ spl0_1
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2486,f266]) ).
fof(f2489,plain,
( e12 = e13
| ~ spl0_1
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2488,f108]) ).
fof(f2490,plain,
( $false
| ~ spl0_1
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2489,f167]) ).
fof(f2491,plain,
( ~ spl0_1
| ~ spl0_14
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2490]) ).
fof(f2529,plain,
( j(e22) = op1(e12,j(e21))
| ~ spl0_3 ),
inference(superposition,[],[f388,f186]) ).
fof(f2532,plain,
( op1(e12,e11) = j(e22)
| ~ spl0_3
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2529,f253]) ).
fof(f2536,plain,
( e14 = op1(e12,e11)
| ~ spl0_3
| ~ spl0_11
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2532,f220]) ).
fof(f2539,plain,
( e10 = e14
| ~ spl0_3
| ~ spl0_11
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2536,f118]) ).
fof(f2540,plain,
( $false
| ~ spl0_3
| ~ spl0_11
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2539,f171]) ).
fof(f2541,plain,
( ~ spl0_3
| ~ spl0_11
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2540]) ).
fof(f2544,plain,
( e20 = e24
| ~ spl0_2
| ~ spl0_35 ),
inference(forward_demodulation,[],[f1757,f320]) ).
fof(f2555,plain,
( $false
| ~ spl0_2
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f2544,f161]) ).
fof(f2556,plain,
( ~ spl0_2
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f2555]) ).
fof(f2565,plain,
( j(e20) = op1(e13,j(e22))
| ~ spl0_2 ),
inference(superposition,[],[f387,f182]) ).
fof(f2566,plain,
( j(e22) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f388,f182]) ).
fof(f2570,plain,
( op1(e13,e14) = j(e20)
| ~ spl0_2
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2565,f220]) ).
fof(f2574,plain,
( e12 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_11
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2570,f270]) ).
fof(f2576,plain,
( e11 = e12
| ~ spl0_2
| ~ spl0_11
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2574,f110]) ).
fof(f2577,plain,
( $false
| ~ spl0_2
| ~ spl0_11
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f2576,f170]) ).
fof(f2578,plain,
( ~ spl0_2
| ~ spl0_11
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f2577]) ).
fof(f2585,plain,
( op1(e13,e12) = j(e22)
| ~ spl0_2
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2566,f249]) ).
fof(f2588,plain,
( e14 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_11
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2585,f220]) ).
fof(f2589,plain,
( e10 = e14
| ~ spl0_2
| ~ spl0_11
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2588,f112]) ).
fof(f2590,plain,
( $false
| ~ spl0_2
| ~ spl0_11
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2589,f171]) ).
fof(f2591,plain,
( ~ spl0_2
| ~ spl0_11
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2590]) ).
fof(f2594,plain,
( e22 = e24
| ~ spl0_1
| ~ spl0_28 ),
inference(forward_demodulation,[],[f2455,f291]) ).
fof(f2606,plain,
( $false
| ~ spl0_1
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f2594,f156]) ).
fof(f2607,plain,
( ~ spl0_1
| ~ spl0_28 ),
inference(avatar_contradiction_clause,[],[f2606]) ).
fof(f2616,plain,
( j(e20) = op1(e14,j(e22))
| ~ spl0_1 ),
inference(superposition,[],[f387,f178]) ).
fof(f2617,plain,
( j(e22) = op1(e14,j(e21))
| ~ spl0_1 ),
inference(superposition,[],[f388,f178]) ).
fof(f2618,plain,
( j(e23) = op1(e14,j(e20))
| ~ spl0_1 ),
inference(superposition,[],[f389,f178]) ).
fof(f2620,plain,
( op1(e14,e13) = j(e22)
| ~ spl0_1
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2617,f245]) ).
fof(f2624,plain,
( e12 = op1(e14,e13)
| ~ spl0_1
| ~ spl0_13
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2620,f228]) ).
fof(f2627,plain,
( e10 = e12
| ~ spl0_1
| ~ spl0_13
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2624,f106]) ).
fof(f2628,plain,
( $false
| ~ spl0_1
| ~ spl0_13
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2627,f173]) ).
fof(f2629,plain,
( ~ spl0_1
| ~ spl0_13
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2628]) ).
fof(f2637,plain,
( e11 = op1(e14,e13)
| ~ spl0_1
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2620,f232]) ).
fof(f2640,plain,
( e10 = e11
| ~ spl0_1
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2637,f106]) ).
fof(f2641,plain,
( $false
| ~ spl0_1
| ~ spl0_14
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2640,f174]) ).
fof(f2642,plain,
( ~ spl0_1
| ~ spl0_14
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2641]) ).
fof(f2648,plain,
( op1(e14,e11) = j(e22)
| ~ spl0_1
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2617,f253]) ).
fof(f2651,plain,
( op1(e14,e13) = j(e20)
| ~ spl0_1
| ~ spl0_12 ),
inference(forward_demodulation,[],[f2616,f224]) ).
fof(f2652,plain,
( e13 = op1(e14,e11)
| ~ spl0_1
| ~ spl0_12
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2648,f224]) ).
fof(f2653,plain,
( e12 = op1(e14,e13)
| ~ spl0_1
| ~ spl0_12
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2651,f270]) ).
fof(f2654,plain,
( e12 = e13
| ~ spl0_1
| ~ spl0_12
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2652,f108]) ).
fof(f2655,plain,
( e10 = e12
| ~ spl0_1
| ~ spl0_12
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2653,f106]) ).
fof(f2656,plain,
( $false
| ~ spl0_1
| ~ spl0_12
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2654,f167]) ).
fof(f2657,plain,
( ~ spl0_1
| ~ spl0_12
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2656]) ).
fof(f2658,plain,
( $false
| ~ spl0_1
| ~ spl0_12
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f2655,f173]) ).
fof(f2659,plain,
( ~ spl0_1
| ~ spl0_12
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f2658]) ).
fof(f2664,plain,
( e11 = op1(e14,e13)
| ~ spl0_1
| ~ spl0_12
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2651,f274]) ).
fof(f2666,plain,
( op1(e14,e12) = j(e22)
| ~ spl0_1
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2617,f249]) ).
fof(f2669,plain,
( e10 = e11
| ~ spl0_1
| ~ spl0_12
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2664,f106]) ).
fof(f2670,plain,
( e13 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2666,f224]) ).
fof(f2671,plain,
( $false
| ~ spl0_1
| ~ spl0_12
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f2669,f174]) ).
fof(f2672,plain,
( ~ spl0_1
| ~ spl0_12
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f2671]) ).
fof(f2673,plain,
( e11 = e13
| ~ spl0_1
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2670,f107]) ).
fof(f2674,plain,
( $false
| ~ spl0_1
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2673,f169]) ).
fof(f2675,plain,
( ~ spl0_1
| ~ spl0_12
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2674]) ).
fof(f2678,plain,
( e11 = e13
| ~ spl0_24
| ~ spl0_35 ),
inference(forward_demodulation,[],[f863,f274]) ).
fof(f2693,plain,
( $false
| ~ spl0_24
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f2678,f169]) ).
fof(f2694,plain,
( ~ spl0_24
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f2693]) ).
fof(f2705,plain,
( e12 = op1(e14,j(e20))
| ~ spl0_1
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2618,f207]) ).
fof(f2713,plain,
( e12 = op1(e14,e13)
| ~ spl0_1
| ~ spl0_8
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2705,f266]) ).
fof(f2714,plain,
( e10 = e12
| ~ spl0_1
| ~ spl0_8
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2713,f106]) ).
fof(f2715,plain,
( $false
| ~ spl0_1
| ~ spl0_8
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2714,f173]) ).
fof(f2716,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2715]) ).
fof(f2717,plain,
( e21 = e23
| ~ spl0_9
| ~ spl0_44 ),
inference(forward_demodulation,[],[f1660,f358]) ).
fof(f2725,plain,
( op1(e14,e13) = j(e23)
| ~ spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2618,f266]) ).
fof(f2726,plain,
( $false
| ~ spl0_9
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f2717,f159]) ).
fof(f2727,plain,
( ~ spl0_9
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f2726]) ).
fof(f2732,plain,
( e11 = op1(e14,e13)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2725,f211]) ).
fof(f2733,plain,
( e10 = e11
| ~ spl0_1
| ~ spl0_9
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2732,f106]) ).
fof(f2734,plain,
( $false
| ~ spl0_1
| ~ spl0_9
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2733,f174]) ).
fof(f2735,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2734]) ).
fof(f2740,plain,
( e14 = op1(e14,e13)
| ~ spl0_1
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2725,f199]) ).
fof(f2742,plain,
( e10 = e14
| ~ spl0_1
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2740,f106]) ).
fof(f2743,plain,
( $false
| ~ spl0_1
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2742,f171]) ).
fof(f2744,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2743]) ).
fof(f2755,plain,
( j(e20) = op1(e12,j(e22))
| ~ spl0_3 ),
inference(superposition,[],[f387,f186]) ).
fof(f2760,plain,
( op1(e12,e10) = j(e20)
| ~ spl0_3
| ~ spl0_15 ),
inference(forward_demodulation,[],[f2755,f236]) ).
fof(f2764,plain,
( e13 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_15
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2760,f266]) ).
fof(f2766,plain,
( e11 = e13
| ~ spl0_3
| ~ spl0_15
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2764,f119]) ).
fof(f2767,plain,
( $false
| ~ spl0_3
| ~ spl0_15
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2766,f169]) ).
fof(f2768,plain,
( ~ spl0_3
| ~ spl0_15
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2767]) ).
fof(f2776,plain,
( op1(e12,e11) = j(e20)
| ~ spl0_3
| ~ spl0_14 ),
inference(forward_demodulation,[],[f2755,f232]) ).
fof(f2778,plain,
( e13 = op1(e12,e11)
| ~ spl0_3
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2776,f266]) ).
fof(f2779,plain,
( e10 = e13
| ~ spl0_3
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2778,f118]) ).
fof(f2780,plain,
( $false
| ~ spl0_3
| ~ spl0_14
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2779,f172]) ).
fof(f2781,plain,
( ~ spl0_3
| ~ spl0_14
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2780]) ).
fof(f2794,plain,
( e24 = h(e13)
| ~ spl0_2 ),
inference(superposition,[],[f25,f182]) ).
fof(f2798,plain,
( j(e21) = op1(e13,j(e23))
| ~ spl0_2 ),
inference(superposition,[],[f386,f182]) ).
fof(f2799,plain,
( j(e20) = op1(e13,j(e22))
| ~ spl0_2 ),
inference(superposition,[],[f387,f182]) ).
fof(f2800,plain,
( j(e22) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f388,f182]) ).
fof(f2801,plain,
( j(e23) = op1(e13,j(e20))
| ~ spl0_2 ),
inference(superposition,[],[f389,f182]) ).
fof(f2802,plain,
( op1(e13,e10) = j(e23)
| ~ spl0_2
| ~ spl0_25 ),
inference(forward_demodulation,[],[f2801,f278]) ).
fof(f2804,plain,
( op1(e13,e12) = j(e20)
| ~ spl0_2
| ~ spl0_13 ),
inference(forward_demodulation,[],[f2799,f228]) ).
fof(f2805,plain,
( op1(e13,e14) = j(e21)
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_demodulation,[],[f2798,f199]) ).
fof(f2806,plain,
( e14 = op1(e13,e10)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_25 ),
inference(forward_demodulation,[],[f2802,f199]) ).
fof(f2809,plain,
( e12 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2805,f249]) ).
fof(f2810,plain,
( e12 = e14
| ~ spl0_2
| ~ spl0_6
| ~ spl0_25 ),
inference(forward_demodulation,[],[f2806,f114]) ).
fof(f2812,plain,
( e11 = e12
| ~ spl0_2
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2809,f110]) ).
fof(f2813,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f2810,f166]) ).
fof(f2814,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f2813]) ).
fof(f2817,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2812,f170]) ).
fof(f2818,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2817]) ).
fof(f2824,plain,
( op1(e13,e12) = j(e23)
| ~ spl0_2
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2801,f270]) ).
fof(f2829,plain,
( e14 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2824,f199]) ).
fof(f2832,plain,
( e10 = e14
| ~ spl0_2
| ~ spl0_6
| ~ spl0_23 ),
inference(forward_demodulation,[],[f2829,f112]) ).
fof(f2835,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f2832,f171]) ).
fof(f2836,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f2835]) ).
fof(f2841,plain,
( e11 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_13
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2804,f274]) ).
fof(f2843,plain,
( op1(e13,e10) = j(e22)
| ~ spl0_2
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2800,f257]) ).
fof(f2846,plain,
( e10 = e11
| ~ spl0_2
| ~ spl0_13
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2841,f112]) ).
fof(f2848,plain,
( $false
| ~ spl0_2
| ~ spl0_13
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f2846,f174]) ).
fof(f2849,plain,
( ~ spl0_2
| ~ spl0_13
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f2848]) ).
fof(f2860,plain,
( e14 = op1(e13,e10)
| ~ spl0_2
| ~ spl0_11
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2843,f220]) ).
fof(f2863,plain,
( op1(e13,e12) = j(e21)
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_demodulation,[],[f2798,f207]) ).
fof(f2866,plain,
( e12 = e14
| ~ spl0_2
| ~ spl0_11
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2860,f114]) ).
fof(f2868,plain,
( $false
| ~ spl0_2
| ~ spl0_11
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2866,f166]) ).
fof(f2869,plain,
( ~ spl0_2
| ~ spl0_11
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2868]) ).
fof(f2879,plain,
( e11 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2863,f253]) ).
fof(f2882,plain,
( e10 = e11
| ~ spl0_2
| ~ spl0_8
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2879,f112]) ).
fof(f2883,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2882,f174]) ).
fof(f2884,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2883]) ).
fof(f2905,plain,
( j(e22) = op1(e12,j(e21))
| ~ spl0_3 ),
inference(superposition,[],[f388,f186]) ).
fof(f2906,plain,
( j(e23) = op1(e12,j(e20))
| ~ spl0_3 ),
inference(superposition,[],[f389,f186]) ).
fof(f2908,plain,
( op1(e12,e10) = j(e22)
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2905,f257]) ).
fof(f2912,plain,
( e14 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_11
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2908,f220]) ).
fof(f2915,plain,
( e11 = e14
| ~ spl0_3
| ~ spl0_11
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2912,f119]) ).
fof(f2916,plain,
( $false
| ~ spl0_3
| ~ spl0_11
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2915,f168]) ).
fof(f2917,plain,
( ~ spl0_3
| ~ spl0_11
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2916]) ).
fof(f2920,plain,
( op1(e12,e12) = j(e22)
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2905,f249]) ).
fof(f2922,plain,
( e14 = op1(e12,e12)
| ~ spl0_3
| ~ spl0_11
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2920,f220]) ).
fof(f2924,plain,
( e12 = e14
| ~ spl0_3
| ~ spl0_11
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2922,f117]) ).
fof(f2927,plain,
( $false
| ~ spl0_3
| ~ spl0_11
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2924,f166]) ).
fof(f2928,plain,
( ~ spl0_3
| ~ spl0_11
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2927]) ).
fof(f2937,plain,
( op1(e12,e11) = j(e23)
| ~ spl0_3
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2906,f274]) ).
fof(f2941,plain,
( e13 = op1(e12,e12)
| ~ spl0_3
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2920,f224]) ).
fof(f2944,plain,
( e14 = op1(e12,e11)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2937,f199]) ).
fof(f2946,plain,
( e12 = e13
| ~ spl0_3
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_demodulation,[],[f2941,f117]) ).
fof(f2948,plain,
( e10 = e14
| ~ spl0_3
| ~ spl0_6
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2944,f118]) ).
fof(f2949,plain,
( $false
| ~ spl0_3
| ~ spl0_12
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f2946,f167]) ).
fof(f2950,plain,
( ~ spl0_3
| ~ spl0_12
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f2949]) ).
fof(f2951,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f2948,f171]) ).
fof(f2952,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f2951]) ).
fof(f2957,plain,
( e22 = e24
| ~ spl0_2
| ~ spl0_33 ),
inference(forward_demodulation,[],[f2794,f312]) ).
fof(f2981,plain,
( $false
| ~ spl0_2
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f2957,f156]) ).
fof(f2982,plain,
( ~ spl0_2
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f2981]) ).
fof(f3000,plain,
( j(e21) = op1(e13,j(e23))
| ~ spl0_2 ),
inference(superposition,[],[f386,f182]) ).
fof(f3002,plain,
( j(e22) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f388,f182]) ).
fof(f3005,plain,
( op1(e13,e14) = j(e22)
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3002,f241]) ).
fof(f3032,plain,
( e11 = j(e22)
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3005,f110]) ).
fof(f3034,plain,
( $false
| ~ spl0_2
| spl0_14
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f3032,f231]) ).
fof(f3035,plain,
( ~ spl0_2
| spl0_14
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f3034]) ).
fof(f3042,plain,
( op1(e13,e12) = j(e21)
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_demodulation,[],[f3000,f207]) ).
fof(f3044,plain,
( e14 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3042,f241]) ).
fof(f3045,plain,
( e10 = e14
| ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3044,f112]) ).
fof(f3046,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f3045,f171]) ).
fof(f3047,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f3046]) ).
fof(f3061,plain,
( j(e21) = op1(e12,j(e23))
| ~ spl0_3 ),
inference(superposition,[],[f386,f186]) ).
fof(f3068,plain,
( op1(e12,e11) = j(e21)
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f3061,f211]) ).
fof(f3072,plain,
( e14 = op1(e12,e11)
| ~ spl0_3
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3068,f241]) ).
fof(f3073,plain,
( e10 = e14
| ~ spl0_3
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3072,f118]) ).
fof(f3074,plain,
( $false
| ~ spl0_3
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f3073,f171]) ).
fof(f3075,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f3074]) ).
fof(f3083,plain,
( op1(e12,e12) = j(e21)
| ~ spl0_3
| ~ spl0_8 ),
inference(forward_demodulation,[],[f3061,f207]) ).
fof(f3085,plain,
( e14 = op1(e12,e12)
| ~ spl0_3
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3083,f241]) ).
fof(f3087,plain,
( e12 = e14
| ~ spl0_3
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f3085,f117]) ).
fof(f3090,plain,
( $false
| ~ spl0_3
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f3087,f166]) ).
fof(f3091,plain,
( ~ spl0_3
| ~ spl0_8
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f3090]) ).
fof(f3108,plain,
( j(e21) = op1(e14,j(e23))
| ~ spl0_1 ),
inference(superposition,[],[f386,f178]) ).
fof(f3111,plain,
( j(e23) = op1(e14,j(e20))
| ~ spl0_1 ),
inference(superposition,[],[f389,f178]) ).
fof(f3112,plain,
( op1(e14,e11) = j(e23)
| ~ spl0_1
| ~ spl0_24 ),
inference(forward_demodulation,[],[f3111,f274]) ).
fof(f3115,plain,
( op1(e14,e12) = j(e21)
| ~ spl0_1
| ~ spl0_8 ),
inference(forward_demodulation,[],[f3108,f207]) ).
fof(f3119,plain,
( e13 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_demodulation,[],[f3115,f245]) ).
fof(f3120,plain,
( e11 = e13
| ~ spl0_1
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_demodulation,[],[f3119,f107]) ).
fof(f3121,plain,
( $false
| ~ spl0_1
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f3120,f169]) ).
fof(f3122,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f3121]) ).
fof(f3130,plain,
( e14 = op1(e14,e11)
| ~ spl0_1
| ~ spl0_6
| ~ spl0_24 ),
inference(forward_demodulation,[],[f3112,f199]) ).
fof(f3132,plain,
( e12 = e14
| ~ spl0_1
| ~ spl0_6
| ~ spl0_24 ),
inference(forward_demodulation,[],[f3130,f108]) ).
fof(f3133,plain,
( $false
| ~ spl0_1
| ~ spl0_6
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f3132,f166]) ).
fof(f3134,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f3133]) ).
fof(f3138,plain,
( e10 = e11
| ~ spl0_15
| ~ spl0_43 ),
inference(forward_demodulation,[],[f467,f236]) ).
fof(f3147,plain,
( $false
| ~ spl0_15
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f3138,f174]) ).
fof(f3148,plain,
( ~ spl0_15
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f3147]) ).
fof(f3158,plain,
( j(e23) = op1(e12,j(e20))
| ~ spl0_3 ),
inference(superposition,[],[f389,f186]) ).
fof(f3159,plain,
( op1(e12,e10) = j(e23)
| ~ spl0_3
| ~ spl0_25 ),
inference(forward_demodulation,[],[f3158,f278]) ).
fof(f3163,plain,
( e14 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_25 ),
inference(forward_demodulation,[],[f3159,f199]) ).
fof(f3167,plain,
( e11 = e14
| ~ spl0_3
| ~ spl0_6
| ~ spl0_25 ),
inference(forward_demodulation,[],[f3163,f119]) ).
fof(f3168,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f3167,f168]) ).
fof(f3169,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f3168]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f195]) ).
cnf(s2,plain,
( spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f216]) ).
cnf(s3,plain,
( spl0_11
| spl0_12
| spl0_13
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f237]) ).
cnf(s4,plain,
( spl0_16
| spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f258]) ).
cnf(s5,plain,
( spl0_21
| spl0_22
| spl0_23
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f279]) ).
cnf(s6,plain,
( spl0_26
| spl0_27
| spl0_28
| spl0_29
| spl0_30 ),
inference(sat_conversion,[],[f300]) ).
cnf(s7,plain,
( spl0_31
| spl0_32
| spl0_33
| spl0_34
| spl0_35 ),
inference(sat_conversion,[],[f321]) ).
cnf(s8,plain,
( spl0_36
| spl0_37
| spl0_38
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f342]) ).
cnf(s9,plain,
( spl0_41
| spl0_42
| spl0_43
| spl0_44
| spl0_45 ),
inference(sat_conversion,[],[f363]) ).
cnf(s10,plain,
( spl0_46
| spl0_47
| spl0_48
| spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f384]) ).
cnf(s11,plain,
( ~ spl0_2
| ~ spl0_26 ),
inference(sat_conversion,[],[f438]) ).
cnf(s12,plain,
( spl0_3
| ~ spl0_36 ),
inference(sat_conversion,[],[f443]) ).
cnf(s13,plain,
( spl0_8
| ~ spl0_37 ),
inference(sat_conversion,[],[f446]) ).
cnf(s16,plain,
( ~ spl0_8
| ~ spl0_27 ),
inference(sat_conversion,[],[f456]) ).
cnf(s17,plain,
( spl0_4
| ~ spl0_41 ),
inference(sat_conversion,[],[f461]) ).
cnf(s18,plain,
( spl0_9
| ~ spl0_42 ),
inference(sat_conversion,[],[f464]) ).
cnf(s19,plain,
( spl0_14
| ~ spl0_43 ),
inference(sat_conversion,[],[f468]) ).
cnf(s21,plain,
( ~ spl0_11
| ~ spl0_14 ),
inference(sat_conversion,[],[f474]) ).
cnf(s22,plain,
( spl0_19
| ~ spl0_44 ),
inference(sat_conversion,[],[f480]) ).
cnf(s25,plain,
( spl0_5
| ~ spl0_46 ),
inference(sat_conversion,[],[f489]) ).
cnf(s26,plain,
( spl0_10
| ~ spl0_47 ),
inference(sat_conversion,[],[f492]) ).
cnf(s27,plain,
( spl0_15
| ~ spl0_48 ),
inference(sat_conversion,[],[f496]) ).
cnf(s28,plain,
( spl0_20
| ~ spl0_49 ),
inference(sat_conversion,[],[f501]) ).
cnf(s29,plain,
( spl0_25
| ~ spl0_50 ),
inference(sat_conversion,[],[f507]) ).
cnf(s31,plain,
( ~ spl0_21
| ~ spl0_25 ),
inference(sat_conversion,[],[f513]) ).
cnf(s36,plain,
( spl0_12
| ~ spl0_33 ),
inference(sat_conversion,[],[f534]) ).
cnf(s37,plain,
( ~ spl0_19
| ~ spl0_34 ),
inference(sat_conversion,[],[f541]) ).
cnf(s38,plain,
( spl0_17
| ~ spl0_34 ),
inference(sat_conversion,[],[f543]) ).
cnf(s41,plain,
( spl0_24
| ~ spl0_45 ),
inference(sat_conversion,[],[f557]) ).
cnf(s45,plain,
( ~ spl0_8
| ~ spl0_9 ),
inference(sat_conversion,[],[f572]) ).
cnf(s48,plain,
( spl0_11
| ~ spl0_28 ),
inference(sat_conversion,[],[f591]) ).
cnf(s52,plain,
( ~ spl0_17
| ~ spl0_20 ),
inference(sat_conversion,[],[f615]) ).
cnf(s54,plain,
( ~ spl0_4
| ~ spl0_11
| ~ spl0_17 ),
inference(sat_conversion,[],[f654]) ).
cnf(s57,plain,
( ~ spl0_3
| ~ spl0_8
| ~ spl0_17 ),
inference(sat_conversion,[],[f674]) ).
cnf(s58,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_17 ),
inference(sat_conversion,[],[f687]) ).
cnf(s59,plain,
( ~ spl0_5
| ~ spl0_13
| ~ spl0_17 ),
inference(sat_conversion,[],[f693]) ).
cnf(s62,plain,
( ~ spl0_17
| spl0_34 ),
inference(sat_conversion,[],[f731]) ).
cnf(s64,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(sat_conversion,[],[f741]) ).
cnf(s67,plain,
( ~ spl0_12
| spl0_33 ),
inference(sat_conversion,[],[f778]) ).
cnf(s68,plain,
( ~ spl0_24
| spl0_45 ),
inference(sat_conversion,[],[f796]) ).
cnf(s71,plain,
( ~ spl0_13
| spl0_38 ),
inference(sat_conversion,[],[f806]) ).
cnf(s73,plain,
( ~ spl0_22
| spl0_35 ),
inference(sat_conversion,[],[f826]) ).
cnf(s74,plain,
( spl0_21
| ~ spl0_30 ),
inference(sat_conversion,[],[f833]) ).
cnf(s76,plain,
( ~ spl0_7
| ~ spl0_27 ),
inference(sat_conversion,[],[f841]) ).
cnf(s78,plain,
( ~ spl0_22
| ~ spl0_30 ),
inference(sat_conversion,[],[f847]) ).
cnf(s79,plain,
( spl0_22
| ~ spl0_35 ),
inference(sat_conversion,[],[f865]) ).
cnf(s84,plain,
( ~ spl0_7
| ~ spl0_35 ),
inference(sat_conversion,[],[f880]) ).
cnf(s88,plain,
( ~ spl0_5
| ~ spl0_12
| ~ spl0_23 ),
inference(sat_conversion,[],[f896]) ).
cnf(s89,plain,
( ~ spl0_21
| spl0_30 ),
inference(sat_conversion,[],[f897]) ).
cnf(s90,plain,
( ~ spl0_5
| ~ spl0_12
| ~ spl0_21 ),
inference(sat_conversion,[],[f907]) ).
cnf(s91,plain,
( ~ spl0_5
| ~ spl0_10
| ~ spl0_19 ),
inference(sat_conversion,[],[f910]) ).
cnf(s93,plain,
( spl0_7
| ~ spl0_32 ),
inference(sat_conversion,[],[f915]) ).
cnf(s97,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_21 ),
inference(sat_conversion,[],[f990]) ).
cnf(s99,plain,
( spl0_13
| ~ spl0_38 ),
inference(sat_conversion,[],[f1003]) ).
cnf(s100,plain,
( ~ spl0_5
| ~ spl0_15
| ~ spl0_21 ),
inference(sat_conversion,[],[f1015]) ).
cnf(s101,plain,
( ~ spl0_14
| spl0_43 ),
inference(sat_conversion,[],[f1017]) ).
cnf(s105,plain,
( ~ spl0_9
| ~ spl0_27 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s106,plain,
( ~ spl0_17
| ~ spl0_29 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s107,plain,
( ~ spl0_10
| ~ spl0_27 ),
inference(sat_conversion,[],[f1056]) ).
cnf(s108,plain,
( ~ spl0_5
| ~ spl0_10
| ~ spl0_17 ),
inference(sat_conversion,[],[f1060]) ).
cnf(s109,plain,
( ~ spl0_5
| ~ spl0_6
| ~ spl0_17 ),
inference(sat_conversion,[],[f1068]) ).
cnf(s112,plain,
( ~ spl0_23
| ~ spl0_35 ),
inference(sat_conversion,[],[f1079]) ).
cnf(s114,plain,
( ~ spl0_19
| spl0_44 ),
inference(sat_conversion,[],[f1084]) ).
cnf(s115,plain,
( ~ spl0_5
| ~ spl0_6
| ~ spl0_22 ),
inference(sat_conversion,[],[f1095]) ).
cnf(s117,plain,
( ~ spl0_18
| ~ spl0_29 ),
inference(sat_conversion,[],[f1108]) ).
cnf(s119,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_22 ),
inference(sat_conversion,[],[f1117]) ).
cnf(s120,plain,
( ~ spl0_5
| ~ spl0_10
| ~ spl0_16 ),
inference(sat_conversion,[],[f1128]) ).
cnf(s121,plain,
( ~ spl0_5
| ~ spl0_9
| ~ spl0_16 ),
inference(sat_conversion,[],[f1135]) ).
cnf(s123,plain,
( spl0_16
| ~ spl0_29 ),
inference(sat_conversion,[],[f1141]) ).
cnf(s125,plain,
( ~ spl0_11
| spl0_28 ),
inference(sat_conversion,[],[f1152]) ).
cnf(s126,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_20 ),
inference(sat_conversion,[],[f1162]) ).
cnf(s127,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_22 ),
inference(sat_conversion,[],[f1164]) ).
cnf(s130,plain,
( ~ spl0_5
| ~ spl0_10
| ~ spl0_18 ),
inference(sat_conversion,[],[f1177]) ).
cnf(s133,plain,
( ~ spl0_5
| ~ spl0_12
| ~ spl0_16 ),
inference(sat_conversion,[],[f1200]) ).
cnf(s135,plain,
( ~ spl0_5
| ~ spl0_6
| ~ spl0_24 ),
inference(sat_conversion,[],[f1218]) ).
cnf(s138,plain,
( ~ spl0_25
| spl0_50 ),
inference(sat_conversion,[],[f1222]) ).
cnf(s139,plain,
( ~ spl0_5
| ~ spl0_6
| ~ spl0_25 ),
inference(sat_conversion,[],[f1235]) ).
cnf(s143,plain,
( ~ spl0_12
| ~ spl0_28 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s144,plain,
( ~ spl0_7
| spl0_32 ),
inference(sat_conversion,[],[f1253]) ).
cnf(s147,plain,
( ~ spl0_5
| ~ spl0_14
| spl0_22 ),
inference(sat_conversion,[],[f1255]) ).
cnf(s148,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_16 ),
inference(sat_conversion,[],[f1281]) ).
cnf(s151,plain,
( ~ spl0_5
| ~ spl0_11
| ~ spl0_19 ),
inference(sat_conversion,[],[f1297]) ).
cnf(s153,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_18 ),
inference(sat_conversion,[],[f1306]) ).
cnf(s160,plain,
( ~ spl0_23
| ~ spl0_30 ),
inference(sat_conversion,[],[f1333]) ).
cnf(s162,plain,
( ~ spl0_3
| ~ spl0_15
| ~ spl0_21 ),
inference(sat_conversion,[],[f1354]) ).
cnf(s163,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(sat_conversion,[],[f1356]) ).
cnf(s166,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_17 ),
inference(sat_conversion,[],[f1382]) ).
cnf(s168,plain,
( ~ spl0_2
| ~ spl0_15
| ~ spl0_21 ),
inference(sat_conversion,[],[f1405]) ).
cnf(s171,plain,
( ~ spl0_4
| ~ spl0_42 ),
inference(sat_conversion,[],[f1415]) ).
cnf(s174,plain,
( ~ spl0_10
| ~ spl0_48 ),
inference(sat_conversion,[],[f1450]) ).
cnf(s175,plain,
( ~ spl0_15
| spl0_48 ),
inference(sat_conversion,[],[f1459]) ).
cnf(s179,plain,
( ~ spl0_4
| ~ spl0_13
| ~ spl0_21 ),
inference(sat_conversion,[],[f1471]) ).
cnf(s181,plain,
( ~ spl0_3
| ~ spl0_38 ),
inference(sat_conversion,[],[f1478]) ).
cnf(s183,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_17 ),
inference(sat_conversion,[],[f1484]) ).
cnf(s187,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_21 ),
inference(sat_conversion,[],[f1512]) ).
cnf(s191,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_21 ),
inference(sat_conversion,[],[f1530]) ).
cnf(s197,plain,
( ~ spl0_1
| ~ spl0_30 ),
inference(sat_conversion,[],[f1543]) ).
cnf(s199,plain,
( ~ spl0_2
| ~ spl0_34 ),
inference(sat_conversion,[],[f1552]) ).
cnf(s204,plain,
( ~ spl0_4
| ~ spl0_45 ),
inference(sat_conversion,[],[f1571]) ).
cnf(s205,plain,
( ~ spl0_6
| ~ spl0_30 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s213,plain,
( ~ spl0_12
| ~ spl0_34 ),
inference(sat_conversion,[],[f1589]) ).
cnf(s217,plain,
( ~ spl0_7
| ~ spl0_34 ),
inference(sat_conversion,[],[f1601]) ).
cnf(s222,plain,
( spl0_2
| ~ spl0_31 ),
inference(sat_conversion,[],[f1609]) ).
cnf(s223,plain,
( ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f1623]) ).
cnf(s225,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_21 ),
inference(sat_conversion,[],[f1646]) ).
cnf(s228,plain,
( ~ spl0_9
| ~ spl0_43 ),
inference(sat_conversion,[],[f1670]) ).
cnf(s232,plain,
( ~ spl0_2
| ~ spl0_13
| ~ spl0_21 ),
inference(sat_conversion,[],[f1681]) ).
cnf(s240,plain,
( ~ spl0_3
| ~ spl0_12
| ~ spl0_20 ),
inference(sat_conversion,[],[f1728]) ).
cnf(s243,plain,
( ~ spl0_11
| ~ spl0_30 ),
inference(sat_conversion,[],[f1743]) ).
cnf(s246,plain,
( ~ spl0_10
| ~ spl0_49 ),
inference(sat_conversion,[],[f1754]) ).
cnf(s250,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_18 ),
inference(sat_conversion,[],[f1803]) ).
cnf(s252,plain,
( ~ spl0_2
| ~ spl0_10
| ~ spl0_16 ),
inference(sat_conversion,[],[f1816]) ).
cnf(s257,plain,
( ~ spl0_12
| ~ spl0_14 ),
inference(sat_conversion,[],[f1834]) ).
cnf(s258,plain,
( ~ spl0_14
| ~ spl0_33 ),
inference(sat_conversion,[],[f1836]) ).
cnf(s261,plain,
( ~ spl0_3
| ~ spl0_14
| ~ spl0_21 ),
inference(sat_conversion,[],[f1846]) ).
cnf(s265,plain,
( ~ spl0_3
| ~ spl0_12
| ~ spl0_19 ),
inference(sat_conversion,[],[f1869]) ).
cnf(s268,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_16 ),
inference(sat_conversion,[],[f1881]) ).
cnf(s272,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_21 ),
inference(sat_conversion,[],[f1908]) ).
cnf(s276,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_21 ),
inference(sat_conversion,[],[f1921]) ).
cnf(s279,plain,
( ~ spl0_20
| spl0_49 ),
inference(sat_conversion,[],[f1927]) ).
cnf(s282,plain,
( ~ spl0_2
| ~ spl0_32 ),
inference(sat_conversion,[],[f1936]) ).
cnf(s284,plain,
( ~ spl0_1
| spl0_26 ),
inference(sat_conversion,[],[f1939]) ).
cnf(s285,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_23 ),
inference(sat_conversion,[],[f1966]) ).
cnf(s287,plain,
( spl0_18
| ~ spl0_39 ),
inference(sat_conversion,[],[f2005]) ).
cnf(s288,plain,
( spl0_23
| ~ spl0_40 ),
inference(sat_conversion,[],[f2012]) ).
cnf(s297,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(sat_conversion,[],[f2043]) ).
cnf(s303,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_19 ),
inference(sat_conversion,[],[f2061]) ).
cnf(s304,plain,
( ~ spl0_9
| spl0_42 ),
inference(sat_conversion,[],[f2062]) ).
cnf(s306,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_16 ),
inference(sat_conversion,[],[f2076]) ).
cnf(s307,plain,
( ~ spl0_20
| ~ spl0_50 ),
inference(sat_conversion,[],[f2085]) ).
cnf(s308,plain,
( ~ spl0_20
| ~ spl0_50 ),
inference(sat_conversion,[],[f2087]) ).
cnf(s313,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_24 ),
inference(sat_conversion,[],[f2097]) ).
cnf(s321,plain,
( spl0_1
| ~ spl0_26 ),
inference(sat_conversion,[],[f2113]) ).
cnf(s326,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_23 ),
inference(sat_conversion,[],[f2144]) ).
cnf(s328,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_25 ),
inference(sat_conversion,[],[f2154]) ).
cnf(s331,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_24 ),
inference(sat_conversion,[],[f2166]) ).
cnf(s336,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(sat_conversion,[],[f2178]) ).
cnf(s341,plain,
( ~ spl0_4
| ~ spl0_11
| ~ spl0_19 ),
inference(sat_conversion,[],[f2204]) ).
cnf(s342,plain,
( ~ spl0_4
| ~ spl0_11
| ~ spl0_23 ),
inference(sat_conversion,[],[f2206]) ).
cnf(s343,plain,
( ~ spl0_4
| ~ spl0_11
| ~ spl0_18 ),
inference(sat_conversion,[],[f2222]) ).
cnf(s348,plain,
( ~ spl0_4
| ~ spl0_11
| ~ spl0_22 ),
inference(sat_conversion,[],[f2245]) ).
cnf(s353,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_22 ),
inference(sat_conversion,[],[f2263]) ).
cnf(s356,plain,
( ~ spl0_8
| ~ spl0_38 ),
inference(sat_conversion,[],[f2276]) ).
cnf(s358,plain,
( ~ spl0_4
| ~ spl0_13
| ~ spl0_16 ),
inference(sat_conversion,[],[f2284]) ).
cnf(s359,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_16 ),
inference(sat_conversion,[],[f2286]) ).
cnf(s365,plain,
( ~ spl0_1
| ~ spl0_4 ),
inference(sat_conversion,[],[f2304]) ).
cnf(s366,plain,
( ~ spl0_10
| ~ spl0_50 ),
inference(sat_conversion,[],[f2306]) ).
cnf(s388,plain,
( ~ spl0_13
| ~ spl0_33 ),
inference(sat_conversion,[],[f2375]) ).
cnf(s389,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(sat_conversion,[],[f2380]) ).
cnf(s393,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_23 ),
inference(sat_conversion,[],[f2399]) ).
cnf(s400,plain,
( ~ spl0_3
| ~ spl0_4 ),
inference(sat_conversion,[],[f2414]) ).
cnf(s403,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_16 ),
inference(sat_conversion,[],[f2425]) ).
cnf(s408,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(sat_conversion,[],[f2440]) ).
cnf(s415,plain,
( ~ spl0_1
| ~ spl0_13
| ~ spl0_22 ),
inference(sat_conversion,[],[f2473]) ).
cnf(s416,plain,
( ~ spl0_1
| ~ spl0_10
| ~ spl0_16 ),
inference(sat_conversion,[],[f2475]) ).
cnf(s420,plain,
( ~ spl0_1
| ~ spl0_14
| ~ spl0_22 ),
inference(sat_conversion,[],[f2491]) ).
cnf(s432,plain,
( ~ spl0_3
| ~ spl0_11
| ~ spl0_19 ),
inference(sat_conversion,[],[f2541]) ).
cnf(s438,plain,
( ~ spl0_2
| ~ spl0_35 ),
inference(sat_conversion,[],[f2556]) ).
cnf(s443,plain,
( ~ spl0_2
| ~ spl0_11
| ~ spl0_23 ),
inference(sat_conversion,[],[f2578]) ).
cnf(s445,plain,
( ~ spl0_2
| ~ spl0_11
| ~ spl0_18 ),
inference(sat_conversion,[],[f2591]) ).
cnf(s449,plain,
( ~ spl0_1
| ~ spl0_28 ),
inference(sat_conversion,[],[f2607]) ).
cnf(s454,plain,
( ~ spl0_1
| ~ spl0_13
| ~ spl0_17 ),
inference(sat_conversion,[],[f2629]) ).
cnf(s458,plain,
( ~ spl0_1
| ~ spl0_14
| ~ spl0_17 ),
inference(sat_conversion,[],[f2642]) ).
cnf(s462,plain,
( ~ spl0_1
| ~ spl0_12
| ~ spl0_19 ),
inference(sat_conversion,[],[f2657]) ).
cnf(s463,plain,
( ~ spl0_1
| ~ spl0_12
| ~ spl0_23 ),
inference(sat_conversion,[],[f2659]) ).
cnf(s465,plain,
( ~ spl0_1
| ~ spl0_12
| ~ spl0_24 ),
inference(sat_conversion,[],[f2672]) ).
cnf(s466,plain,
( ~ spl0_1
| ~ spl0_12
| ~ spl0_18 ),
inference(sat_conversion,[],[f2675]) ).
cnf(s473,plain,
( ~ spl0_24
| ~ spl0_35 ),
inference(sat_conversion,[],[f2694]) ).
cnf(s479,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_22 ),
inference(sat_conversion,[],[f2716]) ).
cnf(s480,plain,
( ~ spl0_9
| ~ spl0_44 ),
inference(sat_conversion,[],[f2727]) ).
cnf(s482,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_22 ),
inference(sat_conversion,[],[f2735]) ).
cnf(s484,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_22 ),
inference(sat_conversion,[],[f2744]) ).
cnf(s490,plain,
( ~ spl0_3
| ~ spl0_15
| ~ spl0_22 ),
inference(sat_conversion,[],[f2768]) ).
cnf(s496,plain,
( ~ spl0_3
| ~ spl0_14
| ~ spl0_22 ),
inference(sat_conversion,[],[f2781]) ).
cnf(s505,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_25 ),
inference(sat_conversion,[],[f2814]) ).
cnf(s507,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_18 ),
inference(sat_conversion,[],[f2818]) ).
cnf(s510,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_23 ),
inference(sat_conversion,[],[f2836]) ).
cnf(s514,plain,
( ~ spl0_2
| ~ spl0_13
| ~ spl0_24 ),
inference(sat_conversion,[],[f2849]) ).
cnf(s517,plain,
( ~ spl0_2
| ~ spl0_11
| ~ spl0_20 ),
inference(sat_conversion,[],[f2869]) ).
cnf(s521,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_19 ),
inference(sat_conversion,[],[f2884]) ).
cnf(s532,plain,
( ~ spl0_3
| ~ spl0_11
| ~ spl0_20 ),
inference(sat_conversion,[],[f2917]) ).
cnf(s536,plain,
( ~ spl0_3
| ~ spl0_11
| ~ spl0_18 ),
inference(sat_conversion,[],[f2928]) ).
cnf(s542,plain,
( ~ spl0_3
| ~ spl0_12
| ~ spl0_18 ),
inference(sat_conversion,[],[f2950]) ).
cnf(s543,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_24 ),
inference(sat_conversion,[],[f2952]) ).
cnf(s548,plain,
( ~ spl0_2
| ~ spl0_33 ),
inference(sat_conversion,[],[f2982]) ).
cnf(s569,plain,
( ~ spl0_2
| spl0_14
| ~ spl0_16 ),
inference(sat_conversion,[],[f3035]) ).
cnf(s574,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(sat_conversion,[],[f3047]) ).
cnf(s585,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_16 ),
inference(sat_conversion,[],[f3075]) ).
cnf(s590,plain,
( ~ spl0_3
| ~ spl0_8
| ~ spl0_16 ),
inference(sat_conversion,[],[f3091]) ).
cnf(s596,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_17 ),
inference(sat_conversion,[],[f3122]) ).
cnf(s598,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_24 ),
inference(sat_conversion,[],[f3134]) ).
cnf(s613,plain,
( ~ spl0_15
| ~ spl0_43 ),
inference(sat_conversion,[],[f3148]) ).
cnf(s614,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_25 ),
inference(sat_conversion,[],[f3169]) ).
cnf(s615,plain,
( ~ spl0_10
| ~ spl0_5 ),
inference(rat,[],[s4,s279,s91,s108,s120,s130,s246]) ).
cnf(s617,plain,
( ~ spl0_30
| spl0_34
| spl0_32
| ~ spl0_5
| spl0_31 ),
inference(rat,[],[s36,s7,s90,s79,s74,s78]) ).
cnf(s618,plain,
( spl0_34
| ~ spl0_9
| spl0_32
| ~ spl0_5
| spl0_31
| spl0_26 ),
inference(rat,[],[s79,s7,s127,s36,s48,s143,s6,s617,s105,s123,s121]) ).
cnf(s619,plain,
( ~ spl0_9
| spl0_32
| ~ spl0_5
| spl0_31
| spl0_26 ),
inference(rat,[],[s74,s6,s100,s48,s3,s58,s59,s38,s213,s618,s123,s101,s105,s121,s228]) ).
cnf(s620,plain,
( spl0_34
| spl0_35
| spl0_27
| spl0_32
| ~ spl0_5
| spl0_31
| spl0_26 ),
inference(rat,[],[s123,s6,s133,s143,s36,s7,s617]) ).
cnf(s621,plain,
( spl0_7
| spl0_6
| ~ spl0_5
| spl0_31
| spl0_26 ),
inference(rat,[],[s74,s100,s6,s3,s48,s58,s106,s38,s213,s620,s147,s79,s71,s16,s119,s356,s2,s619,s93,s615]) ).
cnf(s622,plain,
( ~ spl0_7
| ~ spl0_5
| spl0_26 ),
inference(rat,[],[s4,s126,s151,s48,s6,s74,s123,s64,s76,s97,s148,s153]) ).
cnf(s623,plain,
( ~ spl0_5
| spl0_31
| spl0_26 ),
inference(rat,[],[s36,s7,s88,s38,s79,s5,s89,s109,s115,s135,s139,s205,s621,s93,s622]) ).
cnf(s624,plain,
( ~ spl0_30
| spl0_34
| spl0_32
| ~ spl0_4
| spl0_31 ),
inference(rat,[],[s36,s7,s272,s79,s74,s78]) ).
cnf(s625,plain,
( ~ spl0_29
| spl0_40
| ~ spl0_4
| spl0_36 ),
inference(rat,[],[s8,s99,s13,s287,s358,s359,s117,s123]) ).
cnf(s626,plain,
( ~ spl0_35
| spl0_30
| spl0_7
| ~ spl0_4
| spl0_36
| spl0_26 ),
inference(rat,[],[s2,s16,s107,s6,s625,s48,s353,s348,s288,s79,s112,s304,s171]) ).
cnf(s627,plain,
( spl0_34
| spl0_7
| ~ spl0_4
| spl0_36
| spl0_31
| spl0_26 ),
inference(rat,[],[s8,s287,s288,s389,s393,s2,s13,s16,s107,s6,s123,s143,s403,s99,s36,s388,s7,s626,s624,s304,s171,s93]) ).
cnf(s628,plain,
( ~ spl0_21
| spl0_6
| spl0_11
| spl0_12
| spl0_7
| ~ spl0_4 ),
inference(rat,[],[s175,s174,s3,s2,s179,s187,s191,s304,s171]) ).
cnf(s629,plain,
( spl0_7
| ~ spl0_4
| spl0_36
| spl0_31
| spl0_26 ),
inference(rat,[],[s2,s16,s107,s6,s74,s628,s48,s408,s54,s106,s38,s213,s627,s304,s171]) ).
cnf(s630,plain,
( spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s307,s138,s4,s5,s341,s343,s342,s48,s6,s73,s62,s74,s123,s76,s84,s217,s276,s336,s629,s68,s204,s1,s12,s623,s222,s321]) ).
cnf(s631,plain,
( ~ spl0_30
| ~ spl0_3
| spl0_46 ),
inference(rat,[],[s268,s26,s4,s10,s62,s28,s213,s240,s265,s542,s3,s27,s29,s162,s261,s31,s74,s243,s71,s181]) ).
cnf(s632,plain,
( spl0_12
| spl0_32
| spl0_17
| ~ spl0_3
| spl0_31 ),
inference(rat,[],[s18,s9,s585,s22,s4,s432,s532,s536,s3,s19,s490,s496,s41,s79,s473,s7,s36,s17,s400,s71,s181,s38]) ).
cnf(s633,plain,
( spl0_7
| spl0_17
| ~ spl0_3
| spl0_31 ),
inference(rat,[],[s41,s543,s9,s2,s18,s268,s585,s590,s4,s19,s22,s240,s257,s265,s542,s632,s93,s17,s400]) ).
cnf(s634,plain,
( ~ spl0_7
| spl0_21
| ~ spl0_3 ),
inference(rat,[],[s73,s5,s84,s326,s328,s331]) ).
cnf(s635,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s613,s27,s9,s10,s41,s29,s543,s614,s22,s18,s2,s26,s28,s37,s57,s163,s183,s52,s62,s633,s634,s89,s631,s17,s400,s630,s25,s623,s222,s321]) ).
cnf(s636,plain,
( ~ spl0_30
| ~ spl0_2 ),
inference(rat,[],[s287,s250,s8,s3,s13,s99,s168,s225,s232,s288,s74,s160,s243,s67,s548,s12,s223]) ).
cnf(s637,plain,
( ~ spl0_9
| spl0_28
| spl0_1 ),
inference(rat,[],[s123,s569,s6,s101,s105,s228,s321,s636,s635]) ).
cnf(s638,plain,
( ~ spl0_6
| spl0_37
| ~ spl0_2 ),
inference(rat,[],[s99,s514,s8,s5,s287,s288,s505,s507,s510,s73,s438,s12,s223,s89,s636]) ).
cnf(s639,plain,
( spl0_28
| spl0_8
| spl0_1 ),
inference(rat,[],[s6,s123,s107,s252,s2,s637,s321,s144,s282,s636,s638,s13,s635]) ).
cnf(s640,plain,
( spl0_8
| spl0_1 ),
inference(rat,[],[s366,s138,s2,s5,s480,s514,s114,s99,s4,s8,s569,s288,s287,s21,s443,s445,s517,s48,s639,s638,s13,s73,s438,s144,s282,s12,s223,s62,s199,s89,s636,s635]) ).
cnf(s641,plain,
spl0_1,
inference(rat,[],[s4,s445,s517,s48,s6,s123,s16,s521,s574,s640,s636,s62,s199,s635,s321]) ).
cnf(s642,plain,
~ spl0_28,
inference(rat,[],[s449,s641]) ).
cnf(s643,plain,
~ spl0_4,
inference(rat,[],[s365,s641]) ).
cnf(s644,plain,
spl0_26,
inference(rat,[],[s284,s641]) ).
cnf(s645,plain,
~ spl0_30,
inference(rat,[],[s197,s641]) ).
cnf(s646,plain,
~ spl0_11,
inference(rat,[],[s125,s642]) ).
cnf(s647,plain,
~ spl0_41,
inference(rat,[],[s17,s643]) ).
cnf(s649,plain,
~ spl0_2,
inference(rat,[],[s11,s644]) ).
cnf(s650,plain,
~ spl0_21,
inference(rat,[],[s89,s645]) ).
cnf(s652,plain,
~ spl0_31,
inference(rat,[],[s222,s649]) ).
cnf(s653,plain,
( ~ spl0_9
| spl0_36
| spl0_34
| spl0_32 ),
inference(rat,[],[s8,s288,s287,s463,s466,s99,s36,s388,s7,s13,s79,s45,s482,s641,s652]) ).
cnf(s654,plain,
( spl0_12
| spl0_15
| spl0_34
| spl0_32 ),
inference(rat,[],[s3,s415,s420,s79,s7,s36,s646,s641,s652]) ).
cnf(s655,plain,
( ~ spl0_10
| spl0_17
| spl0_32 ),
inference(rat,[],[s4,s462,s466,s654,s175,s279,s174,s246,s416,s38,s641]) ).
cnf(s656,plain,
( ~ spl0_6
| spl0_42
| spl0_34
| spl0_32 ),
inference(rat,[],[s22,s9,s462,s19,s36,s258,s7,s79,s41,s484,s598,s647,s641,s652]) ).
cnf(s657,plain,
( spl0_17
| spl0_7 ),
inference(rat,[],[s9,s22,s41,s462,s465,s19,s36,s258,s7,s79,s479,s2,s656,s655,s18,s653,s12,s633,s38,s93,s647,s641,s652]) ).
cnf(s658,plain,
spl0_7,
inference(rat,[],[s598,s2,s41,s174,s9,s175,s22,s3,s18,s19,s37,s213,s166,s454,s458,s596,s62,s657,s641,s647,s646]) ).
cnf(s659,plain,
~ spl0_24,
inference(rat,[],[s313,s641,s658]) ).
cnf(s660,plain,
~ spl0_16,
inference(rat,[],[s306,s641,s658]) ).
cnf(s661,plain,
~ spl0_19,
inference(rat,[],[s303,s641,s658]) ).
cnf(s662,plain,
~ spl0_18,
inference(rat,[],[s297,s641,s658]) ).
cnf(s663,plain,
~ spl0_23,
inference(rat,[],[s285,s641,s658]) ).
cnf(s664,plain,
~ spl0_34,
inference(rat,[],[s217,s658]) ).
cnf(s667,plain,
~ spl0_35,
inference(rat,[],[s84,s658]) ).
cnf(s675,plain,
~ spl0_17,
inference(rat,[],[s62,s664]) ).
cnf(s678,plain,
~ spl0_22,
inference(rat,[],[s73,s667]) ).
cnf(s681,plain,
spl0_20,
inference(rat,[],[s4,s662,s661,s660,s675]) ).
cnf(s683,plain,
spl0_25,
inference(rat,[],[s5,s659,s650,s663,s678]) ).
cnf(s684,plain,
~ spl0_50,
inference(rat,[],[s308,s681]) ).
cnf(s687,plain,
$false,
inference(rat,[],[s138,s684,s683]) ).
fof(f3170,plain,
$false,
inference(avatar_sat_refutation,[],[s687]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG185+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n003.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 19:41:57 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.53/1.12 % (1902904)Detected formulas, will run a generic FOF schedule.
% 4.53/1.12 % (1902915)dis-21_1_sil=8000:lcm=predicate:random_seed=349663069:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.53/1.12 % (1902915)Refutation not found, incomplete strategy
% 4.53/1.12 % (1902915)------------------------------
% 4.53/1.12 % (1902915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.12 % (1902915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.12 % (1902915)CaDiCaL version: 2.1.3
% 4.53/1.12 % (1902915)Termination reason: Refutation not found, incomplete strategy
% 4.53/1.12 % (1902915)Time elapsed: 0.003 s
% 4.53/1.12 % (1902915)Peak memory usage: 88 MB
% 4.53/1.12 % (1902915)Instructions burned: 8 (million)
% 4.53/1.12 % (1902909)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2349749331:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.53/1.12 % (1902910)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3216005971:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.53/1.12 % (1902912)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3311137572:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.53/1.12 % (1902913)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4097361247:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.53/1.12 % (1902914)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2345849143:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.53/1.12 % (1902911)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2672166913:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.53/1.12 % (1902913)Instruction limit reached!
% 4.53/1.12 % (1902913)------------------------------
% 4.53/1.12 % (1902913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.12 % (1902913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.12 % (1902913)CaDiCaL version: 2.1.3
% 4.53/1.12 % (1902913)Termination reason: Instruction limit
% 4.53/1.12 % (1902913)Termination phase: Saturation
% 4.53/1.12 % (1902913)Time elapsed: 0.050 s
% 4.53/1.12 % (1902913)Peak memory usage: 87 MB
% 4.53/1.12 % (1902913)Instructions burned: 121 (million)
% 4.53/1.12 % (1902912)Instruction limit reached!
% 4.53/1.12 % (1902912)------------------------------
% 4.53/1.12 % (1902912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.12 % (1902912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.12 % (1902912)CaDiCaL version: 2.1.3
% 4.53/1.12 % (1902912)Termination reason: Instruction limit
% 4.53/1.12 % (1902912)Termination phase: Saturation
% 4.53/1.12 % (1902912)Time elapsed: 0.057 s
% 4.53/1.12 % (1902912)Peak memory usage: 89 MB
% 4.53/1.12 % (1902912)Instructions burned: 110 (million)
% 4.53/1.12 % (1902914)Instruction limit reached!
% 4.53/1.12 % (1902914)------------------------------
% 4.53/1.12 % (1902914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.12 % (1902914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.12 % (1902914)CaDiCaL version: 2.1.3
% 4.53/1.12 % (1902914)Termination reason: Instruction limit
% 4.53/1.12 % (1902914)Termination phase: Saturation
% 4.53/1.12 % (1902914)Time elapsed: 0.075 s
% 4.53/1.12 % (1902914)Peak memory usage: 89 MB
% 4.53/1.12 % (1902914)Instructions burned: 140 (million)
% 4.53/1.12 % (1902915)------------------------------
% 4.53/1.12 % (1902915)------------------------------
% 4.53/1.12 % (1902923)lrs+10_1_sil=8000:sp=occurrence:random_seed=145161482:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 4.53/1.12 % (1902924)lrs+10_1_sil=32000:urr=on:br=off:random_seed=668071194:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.53/1.12 % (1902926)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2281881480:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 4.53/1.12 % (1902925)lrs+1011_1_sil=32000:sp=occurrence:random_seed=217147919:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 4.53/1.12 % (1902924)First to succeed.
% 4.53/1.12 % (1902925)Also succeeded, but the first one will report.
% 4.53/1.12 % (1902924)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1902904"
% 4.53/1.12 % (1902923)Also succeeded, but the first one will report.
% 4.53/1.12 % (1902926)Instruction limit reached!
% 4.53/1.12 % (1902926)------------------------------
% 4.53/1.12 % (1902926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.12 % (1902926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.12 % (1902926)CaDiCaL version: 2.1.3
% 4.53/1.12 % (1902926)Termination reason: Instruction limit
% 4.53/1.12 % (1902926)Termination phase: Saturation
% 4.53/1.12 % (1902926)Time elapsed: 0.076 s
% 4.53/1.12 % (1902926)Peak memory usage: 89 MB
% 4.53/1.12 % (1902926)Instructions burned: 249 (million)
% 4.53/1.12 [W928 19:41:58.798153864 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.798193914 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.798229538 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.798242208 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.798270465 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.798282302 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.798684117 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.798717647 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.798752574 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.798764614 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.798790741 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.798802148 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.799462093 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.799488923 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.799525510 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.799538290 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.799565124 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 [W928 19:41:58.799576931 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.53/1.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.53/1.12 % (1902931)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3397097543:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 4.53/1.12 % (1902931)Instruction limit reached!
% 4.53/1.12 % (1902931)------------------------------
% 4.53/1.12 % (1902931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.53/1.12 % (1902931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.53/1.12 % (1902931)CaDiCaL version: 2.1.3
% 4.53/1.12 % (1902931)Termination reason: Instruction limit
% 4.53/1.12 % (1902931)Termination phase: Saturation
% 4.53/1.12 % (1902931)Time elapsed: 0.079 s
% 4.53/1.12 % (1902931)Peak memory usage: 90 MB
% 4.53/1.12 % (1902931)Instructions burned: 297 (million)
% 4.53/1.12 % (1902924)Refutation found. Thanks to Tanya!
% 4.53/1.12 % SZS status Theorem for theBenchmark
% 4.53/1.12 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/1.31 % (1902924)------------------------------
% 0.19/1.31 % (1902924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.19/1.31 % (1902924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/1.31 % (1902924)CaDiCaL version: 2.1.3
% 0.19/1.31 % (1902924)Termination reason: Refutation
% 0.19/1.31 % (1902924)Time elapsed: 0.062 s
% 0.19/1.31 % (1902924)Peak memory usage: 90 MB
% 0.19/1.31 % (1902924)Instructions burned: 109 (million)
% 0.19/1.31 % (1902924)------------------------------
% 0.19/1.31 % (1902924)------------------------------
% 0.19/1.31 % (1902904)Success in time 0.697 s
% 0.19/1.31 % Vampire exiting
%------------------------------------------------------------------------------