%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG076+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 : n013.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:09:30 AM UTC 2026
% Result : Theorem 3.79s 1.13s
% Output : Refutation 3.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 55
% Syntax : Number of formulae : 837 ( 90 unt; 50 def)
% Number of atoms : 2682 ( 978 equ)
% Maximal formula atoms : 110 ( 3 avg)
% Number of connectives : 3210 (1365 ~;1453 |; 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) = e11
& op1(e10,e12) = e12
& op1(e10,e13) = e13
& op1(e10,e14) = e14
& op1(e11,e10) = e11
& op1(e11,e11) = e14
& op1(e11,e12) = e13
& op1(e11,e13) = e10
& op1(e11,e14) = e12
& op1(e12,e10) = e12
& op1(e12,e11) = e10
& op1(e12,e12) = e14
& op1(e12,e13) = e11
& op1(e12,e14) = e13
& op1(e13,e10) = e13
& op1(e13,e11) = e12
& op1(e13,e12) = e10
& op1(e13,e13) = e14
& op1(e13,e14) = e11
& op1(e14,e10) = e14
& op1(e14,e11) = e13
& op1(e14,e12) = e11
& op1(e14,e13) = e12
& op1(e14,e14) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op2(e20,e20) = e20
& op2(e20,e21) = e21
& op2(e20,e22) = e22
& op2(e20,e23) = e23
& op2(e20,e24) = e24
& op2(e21,e20) = e21
& op2(e21,e21) = e20
& op2(e21,e22) = e24
& op2(e21,e23) = e22
& op2(e21,e24) = e23
& op2(e22,e20) = e22
& op2(e22,e21) = e24
& op2(e22,e22) = e23
& op2(e22,e23) = e20
& op2(e22,e24) = e21
& op2(e23,e20) = e23
& op2(e23,e21) = e22
& op2(e23,e22) = e21
& op2(e23,e23) = e24
& op2(e23,e24) = e20
& op2(e24,e20) = e24
& op2(e24,e21) = e23
& op2(e24,e22) = e20
& op2(e24,e23) = e21
& op2(e24,e24) = e22 ),
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(f30,plain,
j(op2(e24,e24)) = op1(j(e24),j(e24)),
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(f80,plain,
e22 = op2(e24,e24),
inference(cnf_transformation,[],[f5]) ).
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,
e23 = op2(e24,e21),
inference(cnf_transformation,[],[f5]) ).
fof(f84,plain,
e24 = op2(e24,e20),
inference(cnf_transformation,[],[f5]) ).
fof(f105,plain,
e10 = op1(e14,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f106,plain,
e12 = op1(e14,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f107,plain,
e11 = op1(e14,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f108,plain,
e13 = op1(e14,e11),
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(f113,plain,
e12 = op1(e13,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f115,plain,
e13 = op1(e12,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f116,plain,
e11 = op1(e12,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f118,plain,
e10 = op1(e12,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f119,plain,
e12 = op1(e12,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f120,plain,
e12 = op1(e11,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f121,plain,
e10 = op1(e11,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f122,plain,
e13 = op1(e11,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f124,plain,
e11 = op1(e11,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f127,plain,
e12 = op1(e10,e12),
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(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(f161,plain,
e20 != e24,
inference(cnf_transformation,[],[f2]) ).
fof(f162,plain,
e20 != e23,
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(f198,plain,
( e14 != j(e23)
| spl0_6 ),
inference(avatar_component_clause,[],[f197]) ).
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(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(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(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(f385,plain,
j(e22) = op1(j(e24),j(e24)),
inference(forward_demodulation,[],[f30,f80]) ).
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(e23) = op1(j(e24),j(e21)),
inference(forward_demodulation,[],[f33,f83]) ).
fof(f389,plain,
j(e24) = 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(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(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(f481,plain,
( e11 = e14
| ~ spl0_16
| ~ spl0_19 ),
inference(superposition,[],[f253,f241]) ).
fof(f485,plain,
( $false
| ~ spl0_16
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f481,f168]) ).
fof(f486,plain,
( ~ spl0_16
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f485]) ).
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(f527,plain,
( e13 = j(e23)
| ~ spl0_32 ),
inference(superposition,[],[f21,f308]) ).
fof(f528,plain,
( e12 = e13
| ~ spl0_8
| ~ spl0_32 ),
inference(forward_demodulation,[],[f527,f207]) ).
fof(f529,plain,
( $false
| ~ spl0_8
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f528,f167]) ).
fof(f530,plain,
( ~ spl0_8
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f529]) ).
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(f625,plain,
( e24 = h(e11)
| ~ spl0_4 ),
inference(superposition,[],[f25,f190]) ).
fof(f626,plain,
( e23 = h(e12)
| ~ spl0_8 ),
inference(superposition,[],[f26,f207]) ).
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(f633,plain,
( j(e21) = op1(j(e24),e12)
| ~ spl0_8 ),
inference(superposition,[],[f386,f207]) ).
fof(f644,plain,
( j(e23) = op1(e11,j(e21))
| ~ spl0_4 ),
inference(superposition,[],[f388,f190]) ).
fof(f645,plain,
( j(e23) = op1(j(e24),e13)
| ~ spl0_17 ),
inference(superposition,[],[f388,f245]) ).
fof(f647,plain,
( op1(e11,e13) = j(e23)
| ~ spl0_4
| ~ spl0_17 ),
inference(forward_demodulation,[],[f644,f245]) ).
fof(f649,plain,
( e12 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_demodulation,[],[f647,f207]) ).
fof(f651,plain,
( e10 = e12
| ~ spl0_4
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_demodulation,[],[f649,f121]) ).
fof(f654,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f651,f173]) ).
fof(f655,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f654]) ).
fof(f658,plain,
( e10 = e11
| ~ spl0_25
| ~ spl0_45 ),
inference(forward_demodulation,[],[f556,f278]) ).
fof(f665,plain,
( op1(e12,e13) = j(e23)
| ~ spl0_3
| ~ spl0_17 ),
inference(forward_demodulation,[],[f645,f186]) ).
fof(f668,plain,
( $false
| ~ spl0_25
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f658,f174]) ).
fof(f669,plain,
( ~ spl0_25
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f668]) ).
fof(f672,plain,
( e12 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_demodulation,[],[f665,f207]) ).
fof(f673,plain,
( e11 = e12
| ~ spl0_3
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_demodulation,[],[f672,f116]) ).
fof(f674,plain,
( $false
| ~ spl0_3
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f673,f170]) ).
fof(f675,plain,
( ~ spl0_3
| ~ spl0_8
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f674]) ).
fof(f680,plain,
( op1(e10,e12) = j(e21)
| ~ spl0_5
| ~ spl0_8 ),
inference(forward_demodulation,[],[f633,f194]) ).
fof(f683,plain,
( e13 = op1(e10,e12)
| ~ spl0_5
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_demodulation,[],[f680,f245]) ).
fof(f686,plain,
( e12 = e13
| ~ spl0_5
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_demodulation,[],[f683,f127]) ).
fof(f687,plain,
( $false
| ~ spl0_5
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f686,f167]) ).
fof(f688,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f687]) ).
fof(f708,plain,
( e24 = h(e13)
| ~ spl0_2 ),
inference(superposition,[],[f25,f182]) ).
fof(f719,plain,
( e21 = e24
| ~ spl0_2
| ~ spl0_34 ),
inference(forward_demodulation,[],[f708,f316]) ).
fof(f722,plain,
( $false
| ~ spl0_2
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f719,f158]) ).
fof(f723,plain,
( ~ spl0_2
| ~ spl0_34 ),
inference(avatar_contradiction_clause,[],[f722]) ).
fof(f746,plain,
( $false
| spl0_2
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f441,f181]) ).
fof(f747,plain,
( spl0_2
| ~ spl0_31 ),
inference(avatar_contradiction_clause,[],[f746]) ).
fof(f771,plain,
( e23 = h(e10)
| ~ spl0_10 ),
inference(superposition,[],[f26,f215]) ).
fof(f772,plain,
( e22 = e23
| ~ spl0_10
| ~ spl0_48 ),
inference(forward_demodulation,[],[f771,f375]) ).
fof(f774,plain,
( $false
| ~ spl0_10
| ~ spl0_48 ),
inference(forward_subsumption_resolution,[],[f772,f157]) ).
fof(f775,plain,
( ~ spl0_10
| ~ spl0_48 ),
inference(avatar_contradiction_clause,[],[f774]) ).
fof(f780,plain,
( j(e20) = op1(j(e24),e10)
| ~ spl0_15 ),
inference(superposition,[],[f387,f236]) ).
fof(f781,plain,
( e22 = h(e10)
| ~ spl0_15 ),
inference(superposition,[],[f27,f236]) ).
fof(f782,plain,
( spl0_48
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f781,f234,f373]) ).
fof(f805,plain,
( e24 = h(e14)
| ~ spl0_1 ),
inference(superposition,[],[f25,f178]) ).
fof(f848,plain,
( e24 = h(e12)
| ~ spl0_3 ),
inference(superposition,[],[f25,f186]) ).
fof(f912,plain,
( j(e23) = op1(j(e24),e12)
| ~ spl0_18 ),
inference(superposition,[],[f388,f249]) ).
fof(f913,plain,
( e21 = h(e12)
| ~ spl0_18 ),
inference(superposition,[],[f28,f249]) ).
fof(f914,plain,
( spl0_39
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f913,f247,f335]) ).
fof(f921,plain,
( e14 = j(e23)
| ~ spl0_27 ),
inference(superposition,[],[f20,f287]) ).
fof(f927,plain,
( e13 = j(e20)
| ~ spl0_35 ),
inference(superposition,[],[f21,f320]) ).
fof(f931,plain,
( spl0_7
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f527,f306,f201]) ).
fof(f934,plain,
( e10 = e13
| ~ spl0_15
| ~ spl0_33 ),
inference(forward_demodulation,[],[f533,f236]) ).
fof(f938,plain,
( $false
| ~ spl0_15
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f934,f172]) ).
fof(f939,plain,
( ~ spl0_15
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f938]) ).
fof(f942,plain,
( spl0_34
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f628,f243,f314]) ).
fof(f943,plain,
( e12 = e13
| ~ spl0_18
| ~ spl0_34 ),
inference(forward_demodulation,[],[f538,f249]) ).
fof(f947,plain,
( $false
| ~ spl0_18
| ~ spl0_34 ),
inference(forward_subsumption_resolution,[],[f943,f167]) ).
fof(f948,plain,
( ~ spl0_18
| ~ spl0_34 ),
inference(avatar_contradiction_clause,[],[f947]) ).
fof(f952,plain,
( e10 = e11
| ~ spl0_15
| ~ spl0_43 ),
inference(forward_demodulation,[],[f467,f236]) ).
fof(f959,plain,
( $false
| ~ spl0_15
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f952,f174]) ).
fof(f960,plain,
( ~ spl0_15
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[],[f959]) ).
fof(f972,plain,
( spl0_22
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f927,f318,f264]) ).
fof(f985,plain,
( op1(e10,e10) = j(e20)
| ~ spl0_5
| ~ spl0_15 ),
inference(forward_demodulation,[],[f780,f194]) ).
fof(f987,plain,
( op1(e10,e12) = j(e23)
| ~ spl0_5
| ~ spl0_18 ),
inference(forward_demodulation,[],[f912,f194]) ).
fof(f1000,plain,
( e12 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_15
| ~ spl0_23 ),
inference(forward_demodulation,[],[f985,f270]) ).
fof(f1005,plain,
( e13 = e14
| ~ spl0_7
| ~ spl0_27 ),
inference(forward_demodulation,[],[f921,f203]) ).
fof(f1006,plain,
( e13 = op1(e10,e12)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f987,f203]) ).
fof(f1007,plain,
( e10 = e12
| ~ spl0_5
| ~ spl0_15
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1000,f129]) ).
fof(f1010,plain,
( $false
| ~ spl0_7
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f1005,f165]) ).
fof(f1011,plain,
( ~ spl0_7
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f1010]) ).
fof(f1012,plain,
( e12 = e13
| ~ spl0_5
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1006,f127]) ).
fof(f1013,plain,
( $false
| ~ spl0_5
| ~ spl0_15
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1007,f173]) ).
fof(f1014,plain,
( ~ spl0_5
| ~ spl0_15
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f1013]) ).
fof(f1015,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1012,f167]) ).
fof(f1016,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1015]) ).
fof(f1017,plain,
( spl0_26
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f805,f176,f281]) ).
fof(f1023,plain,
( op1(e14,e12) = j(e23)
| ~ spl0_1
| ~ spl0_18 ),
inference(forward_demodulation,[],[f912,f178]) ).
fof(f1025,plain,
( e13 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1023,f203]) ).
fof(f1026,plain,
( e11 = e13
| ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1025,f107]) ).
fof(f1027,plain,
( $false
| ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1026,f169]) ).
fof(f1028,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1027]) ).
fof(f1029,plain,
( e21 = e24
| ~ spl0_4
| ~ spl0_44 ),
inference(forward_demodulation,[],[f625,f358]) ).
fof(f1032,plain,
( $false
| spl0_1
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f435,f177]) ).
fof(f1033,plain,
( spl0_1
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f1032]) ).
fof(f1036,plain,
( $false
| ~ spl0_4
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f1029,f158]) ).
fof(f1037,plain,
( ~ spl0_4
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f1036]) ).
fof(f1055,plain,
( spl0_50
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f629,f276,f381]) ).
fof(f1060,plain,
( e24 = h(e11)
| ~ spl0_4 ),
inference(superposition,[],[f25,f190]) ).
fof(f1065,plain,
( j(e21) = op1(e11,j(e23))
| ~ spl0_4 ),
inference(superposition,[],[f386,f190]) ).
fof(f1070,plain,
( op1(e11,e13) = j(e21)
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_demodulation,[],[f1065,f203]) ).
fof(f1074,plain,
( e12 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1070,f249]) ).
fof(f1075,plain,
( e10 = e12
| ~ spl0_4
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1074,f121]) ).
fof(f1076,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1075,f173]) ).
fof(f1077,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1076]) ).
fof(f1083,plain,
( op1(e10,e10) = j(e20)
| ~ spl0_5
| ~ spl0_15 ),
inference(forward_demodulation,[],[f780,f194]) ).
fof(f1092,plain,
( e13 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_15
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1083,f266]) ).
fof(f1093,plain,
( e10 = e13
| ~ spl0_5
| ~ spl0_15
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1092,f129]) ).
fof(f1094,plain,
( $false
| ~ spl0_5
| ~ spl0_15
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1093,f172]) ).
fof(f1095,plain,
( ~ spl0_5
| ~ spl0_15
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f1094]) ).
fof(f1124,plain,
( e23 = h(e11)
| ~ spl0_9 ),
inference(superposition,[],[f26,f211]) ).
fof(f1131,plain,
( e21 = h(e11)
| ~ spl0_19 ),
inference(superposition,[],[f28,f253]) ).
fof(f1142,plain,
( e20 = h(e13)
| ~ spl0_22 ),
inference(superposition,[],[f29,f266]) ).
fof(f1156,plain,
( e12 = j(e21)
| ~ spl0_39 ),
inference(superposition,[],[f22,f337]) ).
fof(f1167,plain,
( e14 = op1(e14,j(e20))
| ~ spl0_1 ),
inference(superposition,[],[f389,f178]) ).
fof(f1168,plain,
( j(e24) = op1(j(e24),e13)
| ~ spl0_22 ),
inference(superposition,[],[f389,f266]) ).
fof(f1170,plain,
( e14 = op1(e14,e13)
| ~ spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1167,f266]) ).
fof(f1172,plain,
( e12 = e14
| ~ spl0_1
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1170,f106]) ).
fof(f1175,plain,
( $false
| ~ spl0_1
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1172,f166]) ).
fof(f1176,plain,
( ~ spl0_1
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f1175]) ).
fof(f1178,plain,
( e23 = e24
| ~ spl0_4
| ~ spl0_42 ),
inference(forward_demodulation,[],[f1060,f350]) ).
fof(f1184,plain,
( e11 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1168,f190]) ).
fof(f1187,plain,
( $false
| ~ spl0_4
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f1178,f155]) ).
fof(f1188,plain,
( ~ spl0_4
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[],[f1187]) ).
fof(f1194,plain,
( e10 = e11
| ~ spl0_4
| ~ spl0_22 ),
inference(forward_demodulation,[],[f1184,f121]) ).
fof(f1196,plain,
( $false
| ~ spl0_4
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f1194,f174]) ).
fof(f1197,plain,
( ~ spl0_4
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f1196]) ).
fof(f1200,plain,
( e20 = e24
| ~ spl0_2
| ~ spl0_35 ),
inference(forward_demodulation,[],[f708,f320]) ).
fof(f1206,plain,
( op1(e13,e12) = j(e23)
| ~ spl0_2
| ~ spl0_18 ),
inference(forward_demodulation,[],[f912,f182]) ).
fof(f1209,plain,
( $false
| ~ spl0_2
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1200,f161]) ).
fof(f1210,plain,
( ~ spl0_2
| ~ spl0_35 ),
inference(avatar_contradiction_clause,[],[f1209]) ).
fof(f1214,plain,
( e11 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1206,f211]) ).
fof(f1216,plain,
( e10 = e11
| ~ spl0_2
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1214,f112]) ).
fof(f1217,plain,
( $false
| ~ spl0_2
| ~ spl0_9
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1216,f174]) ).
fof(f1218,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1217]) ).
fof(f1228,plain,
( e14 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1206,f199]) ).
fof(f1229,plain,
( e10 = e14
| ~ spl0_2
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1228,f112]) ).
fof(f1230,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1229,f171]) ).
fof(f1231,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1230]) ).
fof(f1232,plain,
( e21 = e23
| ~ spl0_8
| ~ spl0_39 ),
inference(forward_demodulation,[],[f626,f337]) ).
fof(f1239,plain,
( e12 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1206,f207]) ).
fof(f1240,plain,
( $false
| ~ spl0_8
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f1232,f159]) ).
fof(f1241,plain,
( ~ spl0_8
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f1240]) ).
fof(f1244,plain,
( e10 = e12
| ~ spl0_2
| ~ spl0_8
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1239,f112]) ).
fof(f1245,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1244,f173]) ).
fof(f1246,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1245]) ).
fof(f1251,plain,
( e13 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1206,f203]) ).
fof(f1252,plain,
( e10 = e13
| ~ spl0_2
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1251,f112]) ).
fof(f1253,plain,
( $false
| ~ spl0_2
| ~ spl0_7
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1252,f172]) ).
fof(f1254,plain,
( ~ spl0_2
| ~ spl0_7
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1253]) ).
fof(f1256,plain,
( e21 = e24
| ~ spl0_3
| ~ spl0_39 ),
inference(forward_demodulation,[],[f848,f337]) ).
fof(f1261,plain,
( spl0_35
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1142,f264,f318]) ).
fof(f1277,plain,
( $false
| ~ spl0_3
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f1256,f158]) ).
fof(f1278,plain,
( ~ spl0_3
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f1277]) ).
fof(f1292,plain,
( e11 = e13
| ~ spl0_14
| ~ spl0_33 ),
inference(forward_demodulation,[],[f533,f232]) ).
fof(f1298,plain,
( op1(e11,e12) = j(e23)
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_demodulation,[],[f912,f190]) ).
fof(f1305,plain,
( $false
| ~ spl0_14
| ~ spl0_33 ),
inference(forward_subsumption_resolution,[],[f1292,f169]) ).
fof(f1306,plain,
( ~ spl0_14
| ~ spl0_33 ),
inference(avatar_contradiction_clause,[],[f1305]) ).
fof(f1309,plain,
( e14 = op1(e11,e12)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1298,f199]) ).
fof(f1310,plain,
( e13 = e14
| ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1309,f122]) ).
fof(f1311,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1310,f165]) ).
fof(f1312,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1311]) ).
fof(f1316,plain,
( $false
| spl0_6
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f440,f198]) ).
fof(f1317,plain,
( spl0_6
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f1316]) ).
fof(f1318,plain,
( $false
| spl0_6
| ~ spl0_27 ),
inference(forward_subsumption_resolution,[],[f921,f198]) ).
fof(f1319,plain,
( spl0_6
| ~ spl0_27 ),
inference(avatar_contradiction_clause,[],[f1318]) ).
fof(f1354,plain,
( spl0_42
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f1124,f209,f348]) ).
fof(f1382,plain,
( e24 = h(e10)
| ~ spl0_5 ),
inference(superposition,[],[f25,f194]) ).
fof(f1386,plain,
( op1(e10,e10) = j(e22)
| ~ spl0_5 ),
inference(superposition,[],[f385,f194]) ).
fof(f1395,plain,
( e12 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1386,f228]) ).
fof(f1401,plain,
( e10 = e12
| ~ spl0_5
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1395,f129]) ).
fof(f1404,plain,
( $false
| ~ spl0_5
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f1401,f173]) ).
fof(f1405,plain,
( ~ spl0_5
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f1404]) ).
fof(f1413,plain,
( e21 = e24
| ~ spl0_5
| ~ spl0_49 ),
inference(forward_demodulation,[],[f1382,f379]) ).
fof(f1415,plain,
( e11 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1386,f232]) ).
fof(f1423,plain,
( $false
| ~ spl0_5
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f1413,f158]) ).
fof(f1424,plain,
( ~ spl0_5
| ~ spl0_49 ),
inference(avatar_contradiction_clause,[],[f1423]) ).
fof(f1426,plain,
( e10 = e11
| ~ spl0_5
| ~ spl0_14 ),
inference(forward_demodulation,[],[f1415,f129]) ).
fof(f1429,plain,
( $false
| ~ spl0_5
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1426,f174]) ).
fof(f1430,plain,
( ~ spl0_5
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f1429]) ).
fof(f1455,plain,
( j(e21) = op1(e11,j(e23))
| ~ spl0_4 ),
inference(superposition,[],[f386,f190]) ).
fof(f1456,plain,
( j(e20) = op1(e11,j(e22))
| ~ spl0_4 ),
inference(superposition,[],[f387,f190]) ).
fof(f1461,plain,
( op1(e11,e13) = j(e20)
| ~ spl0_4
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1456,f224]) ).
fof(f1462,plain,
( op1(e11,e10) = j(e21)
| ~ spl0_4
| ~ spl0_10 ),
inference(forward_demodulation,[],[f1455,f215]) ).
fof(f1466,plain,
( e12 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_12
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1461,f270]) ).
fof(f1467,plain,
( e12 = op1(e11,e10)
| ~ spl0_4
| ~ spl0_10
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1462,f249]) ).
fof(f1470,plain,
( e10 = e12
| ~ spl0_4
| ~ spl0_12
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1466,f121]) ).
fof(f1471,plain,
( e11 = e12
| ~ spl0_4
| ~ spl0_10
| ~ spl0_18 ),
inference(forward_demodulation,[],[f1467,f124]) ).
fof(f1472,plain,
( $false
| ~ spl0_4
| ~ spl0_12
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1470,f173]) ).
fof(f1473,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f1472]) ).
fof(f1474,plain,
( $false
| ~ spl0_4
| ~ spl0_10
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1471,f170]) ).
fof(f1475,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1474]) ).
fof(f1491,plain,
( j(e21) = op1(e13,j(e23))
| ~ spl0_2 ),
inference(superposition,[],[f386,f182]) ).
fof(f1493,plain,
( j(e23) = op1(e13,j(e21))
| ~ spl0_2 ),
inference(superposition,[],[f388,f182]) ).
fof(f1494,plain,
( e13 = op1(e13,j(e20))
| ~ spl0_2 ),
inference(superposition,[],[f389,f182]) ).
fof(f1495,plain,
( e13 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1494,f270]) ).
fof(f1500,plain,
( e10 = e13
| ~ spl0_2
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1495,f112]) ).
fof(f1504,plain,
( $false
| ~ spl0_2
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1500,f172]) ).
fof(f1505,plain,
( ~ spl0_2
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f1504]) ).
fof(f1507,plain,
( e13 = op1(e13,e11)
| ~ spl0_2
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1494,f274]) ).
fof(f1509,plain,
( e12 = e13
| ~ spl0_2
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1507,f113]) ).
fof(f1510,plain,
( $false
| ~ spl0_2
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1509,f167]) ).
fof(f1511,plain,
( ~ spl0_2
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f1510]) ).
fof(f1515,plain,
( e13 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1494,f262]) ).
fof(f1518,plain,
( e11 = e13
| ~ spl0_2
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1515,f110]) ).
fof(f1520,plain,
( $false
| ~ spl0_2
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1518,f169]) ).
fof(f1521,plain,
( ~ spl0_2
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1520]) ).
fof(f1532,plain,
( e23 = h(e10)
| ~ spl0_10 ),
inference(superposition,[],[f26,f215]) ).
fof(f1547,plain,
( e21 = h(e10)
| ~ spl0_20 ),
inference(superposition,[],[f28,f257]) ).
fof(f1566,plain,
( e14 = j(e20)
| ~ spl0_30 ),
inference(superposition,[],[f20,f299]) ).
fof(f1567,plain,
( $false
| spl0_21
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f1566,f261]) ).
fof(f1568,plain,
( spl0_21
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f1567]) ).
fof(f1573,plain,
( e14 = j(e21)
| ~ spl0_29 ),
inference(superposition,[],[f20,f295]) ).
fof(f1574,plain,
( $false
| spl0_16
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f1573,f240]) ).
fof(f1575,plain,
( spl0_16
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f1574]) ).
fof(f1578,plain,
( spl0_44
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f1131,f251,f356]) ).
fof(f1583,plain,
( $false
| spl0_18
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f1156,f248]) ).
fof(f1584,plain,
( spl0_18
| ~ spl0_39 ),
inference(avatar_contradiction_clause,[],[f1583]) ).
fof(f1605,plain,
( j(e23) = op1(j(e24),e11)
| ~ spl0_19 ),
inference(superposition,[],[f388,f253]) ).
fof(f1607,plain,
( op1(e13,e11) = j(e23)
| ~ spl0_2
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1605,f182]) ).
fof(f1618,plain,
( e12 = j(e22)
| ~ spl0_38 ),
inference(superposition,[],[f22,f333]) ).
fof(f1619,plain,
( $false
| spl0_13
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1618,f227]) ).
fof(f1620,plain,
( spl0_13
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f1619]) ).
fof(f1625,plain,
( e12 = j(e20)
| ~ spl0_40 ),
inference(superposition,[],[f22,f341]) ).
fof(f1633,plain,
( e12 = e14
| ~ spl0_11
| ~ spl0_13 ),
inference(superposition,[],[f228,f220]) ).
fof(f1642,plain,
( $false
| ~ spl0_11
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f1633,f166]) ).
fof(f1643,plain,
( ~ spl0_11
| ~ spl0_13 ),
inference(avatar_contradiction_clause,[],[f1642]) ).
fof(f1674,plain,
( e12 = e13
| ~ spl0_2
| ~ spl0_3 ),
inference(superposition,[],[f186,f182]) ).
fof(f1690,plain,
( $false
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f1674,f167]) ).
fof(f1691,plain,
( ~ spl0_2
| ~ spl0_3 ),
inference(avatar_contradiction_clause,[],[f1690]) ).
fof(f1712,plain,
( e14 = op1(e13,e11)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1607,f199]) ).
fof(f1716,plain,
( e12 = e14
| ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1712,f113]) ).
fof(f1719,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1716,f166]) ).
fof(f1720,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1719]) ).
fof(f1722,plain,
( e20 = e21
| ~ spl0_20
| ~ spl0_50 ),
inference(forward_demodulation,[],[f1547,f383]) ).
fof(f1729,plain,
( $false
| ~ spl0_20
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f1722,f164]) ).
fof(f1730,plain,
( ~ spl0_20
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f1729]) ).
fof(f1740,plain,
( op1(e13,e14) = j(e23)
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1493,f241]) ).
fof(f1742,plain,
( e14 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1740,f199]) ).
fof(f1744,plain,
( e11 = e14
| ~ spl0_2
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1742,f110]) ).
fof(f1747,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1744,f168]) ).
fof(f1748,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1747]) ).
fof(f1756,plain,
( op1(e13,e11) = j(e21)
| ~ spl0_2
| ~ spl0_9 ),
inference(forward_demodulation,[],[f1491,f211]) ).
fof(f1762,plain,
( e14 = op1(e13,e11)
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1756,f241]) ).
fof(f1763,plain,
( e12 = e14
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1762,f113]) ).
fof(f1764,plain,
( $false
| ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1763,f166]) ).
fof(f1765,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1764]) ).
fof(f1783,plain,
( op1(e13,e12) = j(e21)
| ~ spl0_2
| ~ spl0_8 ),
inference(forward_demodulation,[],[f1491,f207]) ).
fof(f1786,plain,
( e11 = op1(e13,e12)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1783,f253]) ).
fof(f1787,plain,
( e10 = e11
| ~ spl0_2
| ~ spl0_8
| ~ spl0_19 ),
inference(forward_demodulation,[],[f1786,f112]) ).
fof(f1788,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1787,f174]) ).
fof(f1789,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1788]) ).
fof(f1796,plain,
( op1(e13,e14) = j(e23)
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1493,f241]) ).
fof(f1801,plain,
( e12 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1796,f207]) ).
fof(f1804,plain,
( e11 = e12
| ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1801,f110]) ).
fof(f1807,plain,
( $false
| ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1804,f170]) ).
fof(f1808,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1807]) ).
fof(f1817,plain,
( e13 = op1(e13,e14)
| ~ spl0_2
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1796,f203]) ).
fof(f1823,plain,
( e11 = e13
| ~ spl0_2
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1817,f110]) ).
fof(f1824,plain,
( $false
| ~ spl0_2
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1823,f169]) ).
fof(f1825,plain,
( ~ spl0_2
| ~ spl0_7
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1824]) ).
fof(f1830,plain,
( spl0_23
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1625,f339,f268]) ).
fof(f1845,plain,
( op1(e10,e10) = j(e22)
| ~ spl0_5 ),
inference(superposition,[],[f385,f194]) ).
fof(f1854,plain,
( e13 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1845,f224]) ).
fof(f1858,plain,
( e10 = e13
| ~ spl0_5
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1854,f129]) ).
fof(f1861,plain,
( $false
| ~ spl0_5
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f1858,f172]) ).
fof(f1862,plain,
( ~ spl0_5
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[],[f1861]) ).
fof(f1882,plain,
( op1(e14,e14) = j(e22)
| ~ spl0_1 ),
inference(superposition,[],[f385,f178]) ).
fof(f1886,plain,
( e14 = op1(e14,j(e20))
| ~ spl0_1 ),
inference(superposition,[],[f389,f178]) ).
fof(f1887,plain,
( e14 = op1(e14,e12)
| ~ spl0_1
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1886,f270]) ).
fof(f1892,plain,
( e11 = e14
| ~ spl0_1
| ~ spl0_23 ),
inference(forward_demodulation,[],[f1887,f107]) ).
fof(f1896,plain,
( $false
| ~ spl0_1
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f1892,f168]) ).
fof(f1897,plain,
( ~ spl0_1
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f1896]) ).
fof(f1905,plain,
( spl0_49
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f1547,f255,f377]) ).
fof(f1908,plain,
( e10 = e12
| ~ spl0_15
| ~ spl0_38 ),
inference(forward_demodulation,[],[f1618,f236]) ).
fof(f1913,plain,
( e14 = op1(e14,e11)
| ~ spl0_1
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1886,f274]) ).
fof(f1920,plain,
( $false
| ~ spl0_15
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1908,f173]) ).
fof(f1921,plain,
( ~ spl0_15
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f1920]) ).
fof(f1922,plain,
( e13 = e14
| ~ spl0_1
| ~ spl0_24 ),
inference(forward_demodulation,[],[f1913,f108]) ).
fof(f1924,plain,
( $false
| ~ spl0_1
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f1922,f165]) ).
fof(f1925,plain,
( ~ spl0_1
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f1924]) ).
fof(f1938,plain,
( e10 = j(e22)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1882,f105]) ).
fof(f1954,plain,
( j(e21) = op1(e11,j(e23))
| ~ spl0_4 ),
inference(superposition,[],[f386,f190]) ).
fof(f1955,plain,
( j(e20) = op1(e11,j(e22))
| ~ spl0_4 ),
inference(superposition,[],[f387,f190]) ).
fof(f1956,plain,
( j(e23) = op1(e11,j(e21))
| ~ spl0_4 ),
inference(superposition,[],[f388,f190]) ).
fof(f1959,plain,
( op1(e11,e10) = j(e23)
| ~ spl0_4
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1956,f257]) ).
fof(f1960,plain,
( op1(e11,e12) = j(e20)
| ~ spl0_4
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1955,f228]) ).
fof(f1963,plain,
( e13 = op1(e11,e10)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1959,f203]) ).
fof(f1964,plain,
( e14 = op1(e11,e12)
| ~ spl0_4
| ~ spl0_13
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1960,f262]) ).
fof(f1966,plain,
( e11 = e13
| ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1963,f124]) ).
fof(f1967,plain,
( e13 = e14
| ~ spl0_4
| ~ spl0_13
| ~ spl0_21 ),
inference(forward_demodulation,[],[f1964,f122]) ).
fof(f1968,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f1966,f169]) ).
fof(f1969,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f1968]) ).
fof(f1970,plain,
( $false
| ~ spl0_4
| ~ spl0_13
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f1967,f165]) ).
fof(f1971,plain,
( ~ spl0_4
| ~ spl0_13
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f1970]) ).
fof(f1981,plain,
( op1(e11,e14) = j(e23)
| ~ spl0_4
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1956,f241]) ).
fof(f1984,plain,
( e13 = op1(e11,e14)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1981,f203]) ).
fof(f1988,plain,
( e12 = e13
| ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1984,f120]) ).
fof(f1991,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1988,f167]) ).
fof(f1992,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1991]) ).
fof(f1998,plain,
( op1(e11,e13) = j(e23)
| ~ spl0_4
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1956,f245]) ).
fof(f2004,plain,
( e13 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f1998,f203]) ).
fof(f2007,plain,
( e10 = e13
| ~ spl0_4
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2004,f121]) ).
fof(f2010,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2007,f172]) ).
fof(f2011,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2010]) ).
fof(f2018,plain,
( op1(e11,e10) = j(e21)
| ~ spl0_4
| ~ spl0_10 ),
inference(forward_demodulation,[],[f1954,f215]) ).
fof(f2020,plain,
( e13 = op1(e11,e10)
| ~ spl0_4
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2018,f245]) ).
fof(f2021,plain,
( e11 = e13
| ~ spl0_4
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2020,f124]) ).
fof(f2022,plain,
( $false
| ~ spl0_4
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2021,f169]) ).
fof(f2023,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2022]) ).
fof(f2024,plain,
( e11 = e12
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f186,f190]) ).
fof(f2036,plain,
( op1(e11,e14) = j(e21)
| ~ spl0_4
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1954,f199]) ).
fof(f2038,plain,
( $false
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f2024,f170]) ).
fof(f2039,plain,
( ~ spl0_3
| ~ spl0_4 ),
inference(avatar_contradiction_clause,[],[f2038]) ).
fof(f2048,plain,
( e13 = op1(e11,e14)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2036,f245]) ).
fof(f2050,plain,
( e12 = e13
| ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2048,f120]) ).
fof(f2053,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2050,f167]) ).
fof(f2054,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2053]) ).
fof(f2066,plain,
( op1(e11,e10) = j(e23)
| ~ spl0_4
| ~ spl0_20 ),
inference(forward_demodulation,[],[f1956,f257]) ).
fof(f2070,plain,
( op1(e11,e12) = j(e21)
| ~ spl0_4
| ~ spl0_8 ),
inference(forward_demodulation,[],[f1954,f207]) ).
fof(f2071,plain,
( e12 = op1(e11,e10)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2066,f207]) ).
fof(f2073,plain,
( e11 = e12
| ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2071,f124]) ).
fof(f2074,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2073,f170]) ).
fof(f2075,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2074]) ).
fof(f2082,plain,
( e14 = op1(e11,e12)
| ~ spl0_4
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2070,f241]) ).
fof(f2084,plain,
( e13 = e14
| ~ spl0_4
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2082,f122]) ).
fof(f2085,plain,
( $false
| ~ spl0_4
| ~ spl0_8
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2084,f165]) ).
fof(f2086,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2085]) ).
fof(f2099,plain,
( op1(e11,e13) = j(e20)
| ~ spl0_4
| ~ spl0_12 ),
inference(forward_demodulation,[],[f1955,f224]) ).
fof(f2106,plain,
( e11 = op1(e11,e13)
| ~ spl0_4
| ~ spl0_12
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2099,f274]) ).
fof(f2110,plain,
( e10 = e11
| ~ spl0_4
| ~ spl0_12
| ~ spl0_24 ),
inference(forward_demodulation,[],[f2106,f121]) ).
fof(f2115,plain,
( $false
| ~ spl0_4
| ~ spl0_12
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f2110,f174]) ).
fof(f2116,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_24 ),
inference(avatar_contradiction_clause,[],[f2115]) ).
fof(f2122,plain,
( op1(e11,e14) = j(e23)
| ~ spl0_4
| ~ spl0_16 ),
inference(forward_demodulation,[],[f1956,f241]) ).
fof(f2124,plain,
( e14 = op1(e11,e14)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2122,f199]) ).
fof(f2126,plain,
( e12 = e14
| ~ spl0_4
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2124,f120]) ).
fof(f2129,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2126,f166]) ).
fof(f2130,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2129]) ).
fof(f2132,plain,
( e20 = e23
| ~ spl0_10
| ~ spl0_50 ),
inference(forward_demodulation,[],[f1532,f383]) ).
fof(f2143,plain,
( $false
| ~ spl0_10
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f2132,f162]) ).
fof(f2144,plain,
( ~ spl0_10
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f2143]) ).
fof(f2170,plain,
( op1(e10,e10) = j(e22)
| ~ spl0_5 ),
inference(superposition,[],[f385,f194]) ).
fof(f2179,plain,
( e14 = op1(e10,e10)
| ~ spl0_5
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2170,f220]) ).
fof(f2183,plain,
( e10 = e14
| ~ spl0_5
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2179,f129]) ).
fof(f2184,plain,
( $false
| ~ spl0_5
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f2183,f171]) ).
fof(f2185,plain,
( ~ spl0_5
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f2184]) ).
fof(f2198,plain,
( j(e21) = op1(e12,j(e23))
| ~ spl0_3 ),
inference(superposition,[],[f386,f186]) ).
fof(f2199,plain,
( j(e20) = op1(e12,j(e22))
| ~ spl0_3 ),
inference(superposition,[],[f387,f186]) ).
fof(f2200,plain,
( j(e23) = op1(e12,j(e21))
| ~ spl0_3 ),
inference(superposition,[],[f388,f186]) ).
fof(f2205,plain,
( op1(e12,e13) = j(e21)
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f2198,f203]) ).
fof(f2209,plain,
( e13 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2205,f245]) ).
fof(f2211,plain,
( e11 = e13
| ~ spl0_3
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2209,f116]) ).
fof(f2214,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2211,f169]) ).
fof(f2215,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2214]) ).
fof(f2218,plain,
( op1(e12,e11) = j(e23)
| ~ spl0_3
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2200,f253]) ).
fof(f2220,plain,
( e13 = op1(e12,e11)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2218,f203]) ).
fof(f2221,plain,
( e10 = e13
| ~ spl0_3
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2220,f118]) ).
fof(f2222,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2221,f172]) ).
fof(f2223,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2222]) ).
fof(f2228,plain,
( op1(e12,e10) = j(e23)
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2200,f257]) ).
fof(f2230,plain,
( e13 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2228,f203]) ).
fof(f2231,plain,
( e12 = e13
| ~ spl0_3
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2230,f119]) ).
fof(f2232,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2231,f167]) ).
fof(f2233,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2232]) ).
fof(f2261,plain,
( j(e21) = op1(j(e24),e10)
| ~ spl0_10 ),
inference(superposition,[],[f386,f215]) ).
fof(f2263,plain,
( op1(e12,e10) = j(e21)
| ~ spl0_3
| ~ spl0_10 ),
inference(forward_demodulation,[],[f2261,f186]) ).
fof(f2266,plain,
( j(e20) = op1(j(e24),e14)
| ~ spl0_11 ),
inference(superposition,[],[f387,f220]) ).
fof(f2267,plain,
( op1(e12,e14) = j(e20)
| ~ spl0_3
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2266,f186]) ).
fof(f2294,plain,
( e13 = j(e20)
| ~ spl0_3
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2267,f115]) ).
fof(f2306,plain,
( j(e24) = op1(j(e24),e13)
| ~ spl0_22 ),
inference(superposition,[],[f389,f266]) ).
fof(f2307,plain,
( e12 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2306,f186]) ).
fof(f2308,plain,
( e11 = e12
| ~ spl0_3
| ~ spl0_22 ),
inference(forward_demodulation,[],[f2307,f116]) ).
fof(f2309,plain,
( $false
| ~ spl0_3
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f2308,f170]) ).
fof(f2310,plain,
( ~ spl0_3
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f2309]) ).
fof(f2316,plain,
( $false
| ~ spl0_3
| ~ spl0_11
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f2294,f265]) ).
fof(f2317,plain,
( ~ spl0_3
| ~ spl0_11
| spl0_22 ),
inference(avatar_contradiction_clause,[],[f2316]) ).
fof(f2319,plain,
( op1(e12,e13) = j(e23)
| ~ spl0_3
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2200,f245]) ).
fof(f2321,plain,
( e13 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2263,f245]) ).
fof(f2324,plain,
( e12 = e13
| ~ spl0_3
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2321,f119]) ).
fof(f2327,plain,
( $false
| ~ spl0_3
| ~ spl0_10
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2324,f167]) ).
fof(f2328,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2327]) ).
fof(f2337,plain,
( op1(e12,e13) = j(e20)
| ~ spl0_3
| ~ spl0_12 ),
inference(forward_demodulation,[],[f2199,f224]) ).
fof(f2342,plain,
( e14 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2319,f199]) ).
fof(f2345,plain,
( e11 = e14
| ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2342,f116]) ).
fof(f2346,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2345,f168]) ).
fof(f2347,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2346]) ).
fof(f2353,plain,
( op1(e12,e11) = j(e23)
| ~ spl0_3
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2200,f253]) ).
fof(f2355,plain,
( e14 = op1(e12,e11)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2353,f199]) ).
fof(f2356,plain,
( e10 = e14
| ~ spl0_3
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_demodulation,[],[f2355,f118]) ).
fof(f2357,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f2356,f171]) ).
fof(f2358,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f2357]) ).
fof(f2365,plain,
( e14 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_12
| ~ spl0_21 ),
inference(forward_demodulation,[],[f2337,f262]) ).
fof(f2370,plain,
( op1(e12,e11) = j(e21)
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f2198,f211]) ).
fof(f2371,plain,
( e11 = e14
| ~ spl0_3
| ~ spl0_12
| ~ spl0_21 ),
inference(forward_demodulation,[],[f2365,f116]) ).
fof(f2374,plain,
( $false
| ~ spl0_3
| ~ spl0_12
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f2371,f168]) ).
fof(f2375,plain,
( ~ spl0_3
| ~ spl0_12
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f2374]) ).
fof(f2381,plain,
( e14 = op1(e12,e11)
| ~ spl0_3
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2370,f241]) ).
fof(f2383,plain,
( e10 = e14
| ~ spl0_3
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2381,f118]) ).
fof(f2384,plain,
( $false
| ~ spl0_3
| ~ spl0_9
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2383,f171]) ).
fof(f2385,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2384]) ).
fof(f2407,plain,
( op1(e12,e10) = j(e23)
| ~ spl0_3
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2200,f257]) ).
fof(f2409,plain,
( e14 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2407,f199]) ).
fof(f2410,plain,
( e12 = e14
| ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_demodulation,[],[f2409,f119]) ).
fof(f2411,plain,
( $false
| ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2410,f166]) ).
fof(f2412,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2411]) ).
fof(f2422,plain,
( op1(e12,e10) = j(e21)
| ~ spl0_3
| ~ spl0_10 ),
inference(forward_demodulation,[],[f2198,f215]) ).
fof(f2424,plain,
( e14 = op1(e12,e10)
| ~ spl0_3
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2422,f241]) ).
fof(f2425,plain,
( e12 = e14
| ~ spl0_3
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2424,f119]) ).
fof(f2426,plain,
( $false
| ~ spl0_3
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2425,f166]) ).
fof(f2427,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2426]) ).
fof(f2428,plain,
( e12 = e14
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f178,f186]) ).
fof(f2429,plain,
( spl0_15
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f1938,f176,f234]) ).
fof(f2447,plain,
( op1(e12,e11) = j(e21)
| ~ spl0_3
| ~ spl0_9 ),
inference(forward_demodulation,[],[f2198,f211]) ).
fof(f2448,plain,
( $false
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f2428,f166]) ).
fof(f2449,plain,
( ~ spl0_1
| ~ spl0_3 ),
inference(avatar_contradiction_clause,[],[f2448]) ).
fof(f2456,plain,
( e13 = op1(e12,e11)
| ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2447,f245]) ).
fof(f2457,plain,
( e10 = e13
| ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f2456,f118]) ).
fof(f2458,plain,
( $false
| ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f2457,f172]) ).
fof(f2459,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f2458]) ).
fof(f2499,plain,
( e10 = e14
| ~ spl0_16
| ~ spl0_20 ),
inference(superposition,[],[f257,f241]) ).
fof(f2508,plain,
( $false
| ~ spl0_16
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f2499,f171]) ).
fof(f2509,plain,
( ~ spl0_16
| ~ spl0_20 ),
inference(avatar_contradiction_clause,[],[f2508]) ).
fof(f2524,plain,
( op1(e12,e13) = j(e21)
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_demodulation,[],[f2198,f203]) ).
fof(f2528,plain,
( e14 = op1(e12,e13)
| ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2524,f241]) ).
fof(f2529,plain,
( e11 = e14
| ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_demodulation,[],[f2528,f116]) ).
fof(f2530,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f2529,f168]) ).
fof(f2531,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f2530]) ).
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(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(s22,plain,
( spl0_19
| ~ spl0_44 ),
inference(sat_conversion,[],[f480]) ).
cnf(s24,plain,
( ~ spl0_16
| ~ spl0_19 ),
inference(sat_conversion,[],[f486]) ).
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(s35,plain,
( ~ spl0_8
| ~ spl0_32 ),
inference(sat_conversion,[],[f530]) ).
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(s54,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_17 ),
inference(sat_conversion,[],[f655]) ).
cnf(s56,plain,
( ~ spl0_25
| ~ spl0_45 ),
inference(sat_conversion,[],[f669]) ).
cnf(s57,plain,
( ~ spl0_3
| ~ spl0_8
| ~ spl0_17 ),
inference(sat_conversion,[],[f675]) ).
cnf(s58,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_17 ),
inference(sat_conversion,[],[f688]) ).
cnf(s62,plain,
( ~ spl0_2
| ~ spl0_34 ),
inference(sat_conversion,[],[f723]) ).
cnf(s66,plain,
( spl0_2
| ~ spl0_31 ),
inference(sat_conversion,[],[f747]) ).
cnf(s70,plain,
( ~ spl0_10
| ~ spl0_48 ),
inference(sat_conversion,[],[f775]) ).
cnf(s71,plain,
( ~ spl0_15
| spl0_48 ),
inference(sat_conversion,[],[f782]) ).
cnf(s89,plain,
( ~ spl0_18
| spl0_39 ),
inference(sat_conversion,[],[f914]) ).
cnf(s91,plain,
( spl0_7
| ~ spl0_32 ),
inference(sat_conversion,[],[f931]) ).
cnf(s93,plain,
( ~ spl0_15
| ~ spl0_33 ),
inference(sat_conversion,[],[f939]) ).
cnf(s94,plain,
( ~ spl0_17
| spl0_34 ),
inference(sat_conversion,[],[f942]) ).
cnf(s96,plain,
( ~ spl0_18
| ~ spl0_34 ),
inference(sat_conversion,[],[f948]) ).
cnf(s98,plain,
( ~ spl0_15
| ~ spl0_43 ),
inference(sat_conversion,[],[f960]) ).
cnf(s101,plain,
( spl0_22
| ~ spl0_35 ),
inference(sat_conversion,[],[f972]) ).
cnf(s107,plain,
( ~ spl0_7
| ~ spl0_27 ),
inference(sat_conversion,[],[f1011]) ).
cnf(s108,plain,
( ~ spl0_5
| ~ spl0_15
| ~ spl0_23 ),
inference(sat_conversion,[],[f1014]) ).
cnf(s109,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_18 ),
inference(sat_conversion,[],[f1016]) ).
cnf(s110,plain,
( ~ spl0_1
| spl0_26 ),
inference(sat_conversion,[],[f1017]) ).
cnf(s111,plain,
( ~ spl0_1
| ~ spl0_7
| ~ spl0_18 ),
inference(sat_conversion,[],[f1028]) ).
cnf(s112,plain,
( spl0_1
| ~ spl0_26 ),
inference(sat_conversion,[],[f1033]) ).
cnf(s113,plain,
( ~ spl0_4
| ~ spl0_44 ),
inference(sat_conversion,[],[f1037]) ).
cnf(s118,plain,
( ~ spl0_25
| spl0_50 ),
inference(sat_conversion,[],[f1055]) ).
cnf(s119,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_18 ),
inference(sat_conversion,[],[f1077]) ).
cnf(s122,plain,
( ~ spl0_5
| ~ spl0_15
| ~ spl0_22 ),
inference(sat_conversion,[],[f1095]) ).
cnf(s130,plain,
( ~ spl0_1
| ~ spl0_22 ),
inference(sat_conversion,[],[f1176]) ).
cnf(s132,plain,
( ~ spl0_4
| ~ spl0_42 ),
inference(sat_conversion,[],[f1188]) ).
cnf(s134,plain,
( ~ spl0_4
| ~ spl0_22 ),
inference(sat_conversion,[],[f1197]) ).
cnf(s136,plain,
( ~ spl0_2
| ~ spl0_35 ),
inference(sat_conversion,[],[f1210]) ).
cnf(s138,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_18 ),
inference(sat_conversion,[],[f1218]) ).
cnf(s144,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_18 ),
inference(sat_conversion,[],[f1231]) ).
cnf(s145,plain,
( ~ spl0_8
| ~ spl0_39 ),
inference(sat_conversion,[],[f1241]) ).
cnf(s147,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_18 ),
inference(sat_conversion,[],[f1246]) ).
cnf(s148,plain,
( ~ spl0_2
| ~ spl0_7
| ~ spl0_18 ),
inference(sat_conversion,[],[f1254]) ).
cnf(s149,plain,
( ~ spl0_22
| spl0_35 ),
inference(sat_conversion,[],[f1261]) ).
cnf(s151,plain,
( ~ spl0_3
| ~ spl0_39 ),
inference(sat_conversion,[],[f1278]) ).
cnf(s161,plain,
( ~ spl0_14
| ~ spl0_33 ),
inference(sat_conversion,[],[f1306]) ).
cnf(s163,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_18 ),
inference(sat_conversion,[],[f1312]) ).
cnf(s167,plain,
( spl0_6
| ~ spl0_27 ),
inference(sat_conversion,[],[f1317]) ).
cnf(s168,plain,
( spl0_6
| ~ spl0_27 ),
inference(sat_conversion,[],[f1319]) ).
cnf(s178,plain,
( ~ spl0_9
| spl0_42 ),
inference(sat_conversion,[],[f1354]) ).
cnf(s184,plain,
( ~ spl0_5
| ~ spl0_13 ),
inference(sat_conversion,[],[f1405]) ).
cnf(s189,plain,
( ~ spl0_5
| ~ spl0_49 ),
inference(sat_conversion,[],[f1424]) ).
cnf(s190,plain,
( ~ spl0_5
| ~ spl0_14 ),
inference(sat_conversion,[],[f1430]) ).
cnf(s198,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_23 ),
inference(sat_conversion,[],[f1473]) ).
cnf(s199,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_18 ),
inference(sat_conversion,[],[f1475]) ).
cnf(s204,plain,
( ~ spl0_2
| ~ spl0_23 ),
inference(sat_conversion,[],[f1505]) ).
cnf(s205,plain,
( ~ spl0_2
| ~ spl0_24 ),
inference(sat_conversion,[],[f1511]) ).
cnf(s206,plain,
( ~ spl0_2
| ~ spl0_21 ),
inference(sat_conversion,[],[f1521]) ).
cnf(s212,plain,
( spl0_21
| ~ spl0_30 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s213,plain,
( spl0_16
| ~ spl0_29 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s215,plain,
( ~ spl0_19
| spl0_44 ),
inference(sat_conversion,[],[f1578]) ).
cnf(s216,plain,
( spl0_18
| ~ spl0_39 ),
inference(sat_conversion,[],[f1584]) ).
cnf(s217,plain,
( spl0_13
| ~ spl0_38 ),
inference(sat_conversion,[],[f1620]) ).
cnf(s220,plain,
( ~ spl0_11
| ~ spl0_13 ),
inference(sat_conversion,[],[f1643]) ).
cnf(s231,plain,
( ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f1691]) ).
cnf(s236,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_19 ),
inference(sat_conversion,[],[f1720]) ).
cnf(s238,plain,
( ~ spl0_20
| ~ spl0_50 ),
inference(sat_conversion,[],[f1730]) ).
cnf(s242,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_16 ),
inference(sat_conversion,[],[f1748]) ).
cnf(s245,plain,
( ~ spl0_2
| ~ spl0_9
| ~ spl0_16 ),
inference(sat_conversion,[],[f1765]) ).
cnf(s251,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_19 ),
inference(sat_conversion,[],[f1789]) ).
cnf(s254,plain,
( ~ spl0_2
| ~ spl0_8
| ~ spl0_16 ),
inference(sat_conversion,[],[f1808]) ).
cnf(s258,plain,
( ~ spl0_2
| ~ spl0_7
| ~ spl0_16 ),
inference(sat_conversion,[],[f1825]) ).
cnf(s262,plain,
( spl0_23
| ~ spl0_40 ),
inference(sat_conversion,[],[f1830]) ).
cnf(s263,plain,
( ~ spl0_5
| ~ spl0_12 ),
inference(sat_conversion,[],[f1862]) ).
cnf(s272,plain,
( ~ spl0_1
| ~ spl0_23 ),
inference(sat_conversion,[],[f1897]) ).
cnf(s276,plain,
( ~ spl0_20
| spl0_49 ),
inference(sat_conversion,[],[f1905]) ).
cnf(s278,plain,
( ~ spl0_15
| ~ spl0_38 ),
inference(sat_conversion,[],[f1921]) ).
cnf(s279,plain,
( ~ spl0_1
| ~ spl0_24 ),
inference(sat_conversion,[],[f1925]) ).
cnf(s290,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_20 ),
inference(sat_conversion,[],[f1969]) ).
cnf(s291,plain,
( ~ spl0_4
| ~ spl0_13
| ~ spl0_21 ),
inference(sat_conversion,[],[f1971]) ).
cnf(s296,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_16 ),
inference(sat_conversion,[],[f1992]) ).
cnf(s302,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_17 ),
inference(sat_conversion,[],[f2011]) ).
cnf(s303,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_17 ),
inference(sat_conversion,[],[f2023]) ).
cnf(s309,plain,
( ~ spl0_3
| ~ spl0_4 ),
inference(sat_conversion,[],[f2039]) ).
cnf(s315,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_17 ),
inference(sat_conversion,[],[f2054]) ).
cnf(s319,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_20 ),
inference(sat_conversion,[],[f2075]) ).
cnf(s322,plain,
( ~ spl0_4
| ~ spl0_8
| ~ spl0_16 ),
inference(sat_conversion,[],[f2086]) ).
cnf(s330,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_24 ),
inference(sat_conversion,[],[f2116]) ).
cnf(s334,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_16 ),
inference(sat_conversion,[],[f2130]) ).
cnf(s336,plain,
( ~ spl0_10
| ~ spl0_50 ),
inference(sat_conversion,[],[f2144]) ).
cnf(s345,plain,
( ~ spl0_5
| ~ spl0_11 ),
inference(sat_conversion,[],[f2185]) ).
cnf(s353,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_17 ),
inference(sat_conversion,[],[f2215]) ).
cnf(s356,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_19 ),
inference(sat_conversion,[],[f2223]) ).
cnf(s358,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_20 ),
inference(sat_conversion,[],[f2233]) ).
cnf(s374,plain,
( ~ spl0_3
| ~ spl0_22 ),
inference(sat_conversion,[],[f2310]) ).
cnf(s378,plain,
( ~ spl0_3
| ~ spl0_11
| spl0_22 ),
inference(sat_conversion,[],[f2317]) ).
cnf(s380,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_17 ),
inference(sat_conversion,[],[f2328]) ).
cnf(s387,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_17 ),
inference(sat_conversion,[],[f2347]) ).
cnf(s392,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_19 ),
inference(sat_conversion,[],[f2358]) ).
cnf(s395,plain,
( ~ spl0_3
| ~ spl0_12
| ~ spl0_21 ),
inference(sat_conversion,[],[f2375]) ).
cnf(s398,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_16 ),
inference(sat_conversion,[],[f2385]) ).
cnf(s405,plain,
( ~ spl0_3
| ~ spl0_6
| ~ spl0_20 ),
inference(sat_conversion,[],[f2412]) ).
cnf(s409,plain,
( ~ spl0_3
| ~ spl0_10
| ~ spl0_16 ),
inference(sat_conversion,[],[f2427]) ).
cnf(s414,plain,
( ~ spl0_1
| spl0_15 ),
inference(sat_conversion,[],[f2429]) ).
cnf(s420,plain,
( ~ spl0_1
| ~ spl0_3 ),
inference(sat_conversion,[],[f2449]) ).
cnf(s423,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_17 ),
inference(sat_conversion,[],[f2459]) ).
cnf(s429,plain,
( ~ spl0_16
| ~ spl0_20 ),
inference(sat_conversion,[],[f2509]) ).
cnf(s433,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_16 ),
inference(sat_conversion,[],[f2531]) ).
cnf(s434,plain,
( ~ spl0_32
| ~ spl0_5
| spl0_36 ),
inference(rat,[],[s8,s216,s13,s109,s35,s91,s217,s262,s108,s3,s184,s345,s190,s263]) ).
cnf(s435,plain,
( ~ spl0_5
| spl0_36
| spl0_31 ),
inference(rat,[],[s13,s8,s58,s216,s38,s96,s7,s434,s262,s101,s108,s122,s3,s217,s36,s184,s190,s263,s345]) ).
cnf(s436,plain,
( spl0_17
| spl0_33
| ~ spl0_4
| spl0_31 ),
inference(rat,[],[s4,s119,s290,s296,s91,s7,s38,s101,s134,s215,s113]) ).
cnf(s437,plain,
( ~ spl0_17
| spl0_8
| ~ spl0_4 ),
inference(rat,[],[s2,s303,s315,s302,s178,s132]) ).
cnf(s438,plain,
( ~ spl0_7
| spl0_17
| ~ spl0_4 ),
inference(rat,[],[s4,s119,s290,s296,s215,s113]) ).
cnf(s439,plain,
( spl0_18
| spl0_23
| spl0_24
| spl0_8
| ~ spl0_4
| spl0_36 ),
inference(rat,[],[s334,s4,s2,s238,s336,s118,s5,s291,s217,s8,s216,s134,s178,s132,s215,s113,s13,s262,s438,s437]) ).
cnf(s440,plain,
( spl0_8
| ~ spl0_4
| spl0_36
| spl0_31 ),
inference(rat,[],[s2,s163,s199,s439,s438,s198,s330,s36,s436,s437,s178,s132]) ).
cnf(s441,plain,
( spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s89,s4,s54,s145,s319,s322,s440,s215,s113,s1,s435,s12,s66]) ).
cnf(s442,plain,
( spl0_17
| ~ spl0_5
| ~ spl0_3
| spl0_31 ),
inference(rat,[],[s4,s356,s433,s91,s7,s38,s101,s374,s89,s151,s36,s263,s276,s189]) ).
cnf(s443,plain,
( ~ spl0_5
| ~ spl0_3
| spl0_31 ),
inference(rat,[],[s2,s353,s387,s423,s58,s442,s70,s71,s3,s184,s190,s263,s378,s374]) ).
cnf(s444,plain,
( ~ spl0_7
| spl0_17
| ~ spl0_3 ),
inference(rat,[],[s4,s356,s358,s433,s89,s151]) ).
cnf(s445,plain,
( spl0_16
| spl0_30
| spl0_17
| ~ spl0_3
| spl0_26 ),
inference(rat,[],[s4,s392,s405,s168,s6,s213,s89,s151,s48,s378,s374]) ).
cnf(s446,plain,
( spl0_17
| ~ spl0_3
| spl0_31
| spl0_26 ),
inference(rat,[],[s56,s29,s9,s10,s18,s26,s22,s28,s398,s409,s24,s429,s445,s212,s395,s27,s19,s36,s93,s161,s7,s91,s444,s38,s101,s374,s17,s309,s25,s443]) ).
cnf(s447,plain,
( ~ spl0_17
| ~ spl0_3 ),
inference(rat,[],[s2,s57,s353,s380,s387,s423]) ).
cnf(s448,plain,
( ~ spl0_3
| spl0_31
| spl0_26 ),
inference(rat,[],[s447,s446]) ).
cnf(s449,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s448,s441,s66,s112]) ).
cnf(s450,plain,
( ~ spl0_7
| spl0_1 ),
inference(rat,[],[s217,s8,s220,s13,s48,s251,s6,s4,s216,s213,s107,s148,s258,s112,s12,s231,s212,s262,s94,s62,s238,s118,s5,s149,s136,s204,s206,s205,s449]) ).
cnf(s451,plain,
( spl0_16
| spl0_28
| spl0_18
| spl0_1 ),
inference(rat,[],[s167,s236,s6,s4,s213,s112,s212,s94,s62,s238,s118,s5,s149,s136,s204,s206,s205,s449]) ).
cnf(s452,plain,
( spl0_8
| spl0_18
| spl0_1 ),
inference(rat,[],[s2,s242,s245,s451,s48,s220,s217,s8,s13,s12,s231,s262,s336,s118,s5,s149,s136,s204,s206,s205,s449,s450,s216]) ).
cnf(s453,plain,
( spl0_18
| spl0_1 ),
inference(rat,[],[s4,s251,s254,s452,s94,s62,s238,s118,s5,s149,s136,s204,s206,s205,s449]) ).
cnf(s454,plain,
spl0_1,
inference(rat,[],[s2,s138,s144,s147,s453,s450,s336,s118,s5,s149,s136,s204,s205,s206,s449]) ).
cnf(s455,plain,
~ spl0_3,
inference(rat,[],[s420,s454]) ).
cnf(s456,plain,
spl0_15,
inference(rat,[],[s414,s454]) ).
cnf(s457,plain,
~ spl0_24,
inference(rat,[],[s279,s454]) ).
cnf(s458,plain,
~ spl0_23,
inference(rat,[],[s272,s454]) ).
cnf(s462,plain,
~ spl0_22,
inference(rat,[],[s130,s454]) ).
cnf(s464,plain,
spl0_26,
inference(rat,[],[s110,s454]) ).
cnf(s465,plain,
~ spl0_36,
inference(rat,[],[s12,s455]) ).
cnf(s466,plain,
~ spl0_38,
inference(rat,[],[s278,s456]) ).
cnf(s468,plain,
~ spl0_43,
inference(rat,[],[s98,s456]) ).
cnf(s470,plain,
~ spl0_33,
inference(rat,[],[s93,s456]) ).
cnf(s473,plain,
~ spl0_45,
inference(rat,[],[s41,s457]) ).
cnf(s474,plain,
~ spl0_40,
inference(rat,[],[s262,s458]) ).
cnf(s477,plain,
~ spl0_35,
inference(rat,[],[s101,s462]) ).
cnf(s479,plain,
~ spl0_2,
inference(rat,[],[s11,s464]) ).
cnf(s483,plain,
~ spl0_31,
inference(rat,[],[s66,s479]) ).
cnf(s489,plain,
~ spl0_32,
inference(rat,[],[s8,s216,s13,s111,s35,s91,s474,s465,s466,s454]) ).
cnf(s490,plain,
spl0_34,
inference(rat,[],[s7,s477,s470,s483,s489]) ).
cnf(s491,plain,
~ spl0_18,
inference(rat,[],[s96,s490]) ).
cnf(s492,plain,
spl0_17,
inference(rat,[],[s38,s490]) ).
cnf(s493,plain,
~ spl0_19,
inference(rat,[],[s37,s490]) ).
cnf(s494,plain,
~ spl0_39,
inference(rat,[],[s216,s491]) ).
cnf(s497,plain,
~ spl0_44,
inference(rat,[],[s22,s493]) ).
cnf(s498,plain,
spl0_37,
inference(rat,[],[s8,s466,s465,s474,s494]) ).
cnf(s499,plain,
spl0_8,
inference(rat,[],[s13,s498]) ).
cnf(s500,plain,
~ spl0_4,
inference(rat,[],[s54,s492,s499]) ).
cnf(s501,plain,
~ spl0_9,
inference(rat,[],[s45,s499]) ).
cnf(s502,plain,
~ spl0_41,
inference(rat,[],[s17,s500]) ).
cnf(s503,plain,
~ spl0_42,
inference(rat,[],[s18,s501]) ).
cnf(s504,plain,
$false,
inference(rat,[],[s9,s473,s468,s497,s502,s503]) ).
fof(f2532,plain,
$false,
inference(avatar_sat_refutation,[],[s504]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG076+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n013.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 19:24:36 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/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
% 2.99/1.13 % (1475426)Detected formulas, will run a generic FOF schedule.
% 2.99/1.13 % (1475434)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2383711280:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.99/1.13 % (1475434)Instruction limit reached!
% 2.99/1.13 % (1475434)------------------------------
% 2.99/1.13 % (1475434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.13 % (1475434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.13 % (1475434)CaDiCaL version: 2.1.3
% 2.99/1.13 % (1475434)Termination reason: Instruction limit
% 2.99/1.13 % (1475434)Termination phase: Saturation
% 2.99/1.13 % (1475434)Time elapsed: 0.034 s
% 2.99/1.13 % (1475434)Peak memory usage: 89 MB
% 2.99/1.13 % (1475434)Instructions burned: 111 (million)
% 2.99/1.13 % (1475436)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3536346597:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.99/1.13 % (1475435)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=370480413:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.99/1.13 % (1475437)dis-21_1_sil=8000:lcm=predicate:random_seed=3917471635: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)
% 2.99/1.13 % (1475431)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=3861317298:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.99/1.13 % (1475433)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=3305383131:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.99/1.13 % (1475432)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=3813491306:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.99/1.13 % (1475437)Refutation not found, incomplete strategy
% 2.99/1.13 % (1475437)------------------------------
% 2.99/1.13 % (1475437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.13 % (1475437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.13 % (1475437)CaDiCaL version: 2.1.3
% 2.99/1.13 % (1475437)Termination reason: Refutation not found, incomplete strategy
% 2.99/1.13 % (1475437)Time elapsed: 0.005 s
% 2.99/1.13 % (1475437)Peak memory usage: 88 MB
% 2.99/1.13 % (1475437)Instructions burned: 8 (million)
% 2.99/1.13 % (1475435)Instruction limit reached!
% 2.99/1.13 % (1475435)------------------------------
% 2.99/1.13 % (1475435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.13 % (1475435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.13 % (1475435)CaDiCaL version: 2.1.3
% 2.99/1.13 % (1475435)Termination reason: Instruction limit
% 2.99/1.13 % (1475435)Termination phase: Saturation
% 2.99/1.13 % (1475435)Time elapsed: 0.050 s
% 2.99/1.13 % (1475435)Peak memory usage: 87 MB
% 2.99/1.13 % (1475435)Instructions burned: 119 (million)
% 2.99/1.13 % (1475436)Instruction limit reached!
% 2.99/1.13 % (1475436)------------------------------
% 2.99/1.13 % (1475436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.13 % (1475436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.13 % (1475436)CaDiCaL version: 2.1.3
% 3.79/1.13 % (1475436)Termination reason: Instruction limit
% 3.79/1.13 % (1475436)Termination phase: Saturation
% 3.79/1.13 % (1475436)Time elapsed: 0.077 s
% 3.79/1.13 % (1475436)Peak memory usage: 89 MB
% 3.79/1.13 % (1475436)Instructions burned: 140 (million)
% 3.79/1.13 % (1475439)lrs+10_1_sil=8000:sp=occurrence:random_seed=3888523724:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.79/1.13 % (1475439)First to succeed.
% 3.79/1.13 % (1475439)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1475426"
% 3.79/1.13 % (1475446)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2083402890:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.79/1.13 % (1475446)Also succeeded, but the first one will report.
% 3.79/1.13 % (1475447)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2681959370:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 3.79/1.13 % (1475437)------------------------------
% 3.79/1.13 % (1475437)------------------------------
% 3.79/1.13 % (1475447)Also succeeded, but the first one will report.
% 3.79/1.13 % (1475439)Refutation found. Thanks to Tanya!
% 3.79/1.13 % SZS status Theorem for theBenchmark
% 3.79/1.13 % SZS output start Proof for theBenchmark
% See solution above
% 3.96/1.32 % (1475439)------------------------------
% 3.96/1.32 % (1475439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.96/1.32 % (1475439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.96/1.32 % (1475439)CaDiCaL version: 2.1.3
% 3.96/1.32 % (1475439)Termination reason: Refutation
% 3.96/1.32 % (1475439)Time elapsed: 0.025 s
% 3.96/1.32 % (1475439)Peak memory usage: 90 MB
% 3.96/1.32 % (1475439)Instructions burned: 82 (million)
% 3.96/1.32 % (1475439)------------------------------
% 3.96/1.32 % (1475439)------------------------------
% 3.96/1.32 % (1475426)Success in time 0.47 s
% 3.96/1.32 % Vampire exiting
%------------------------------------------------------------------------------