%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV553+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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 12:58:19 PM UTC 2026
% Result : Theorem 23.19s 4.63s
% Output : Refutation 27.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 125
% Syntax : Number of formulae : 1090 ( 197 unt; 114 def)
% Number of atoms : 2656 ( 327 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 2549 ( 983 ~;1442 |; 21 &)
% ( 99 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 11 ( 1 avg)
% Number of predicates : 97 ( 95 usr; 93 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 23 con; 0-2 aty)
% Number of variables : 350 ( 0 sgn 345 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( subq(X0,X1)
<=> ! [X2] :
( mem(X2,X0)
=> mem(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subq_def) ).
fof(f2,axiom,
! [X0,X1] :
( subq(X0,X1)
=> ( subq(X1,X0)
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setext) ).
fof(f3,axiom,
! [X0,X1] :
( disj(X0,X1)
<=> ~ ? [X2] :
( mem(X2,X0)
& mem(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',disj_def) ).
fof(f4,axiom,
! [X0] : ~ mem(X0,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_ax) ).
fof(f5,axiom,
! [X0,X1] :
( mem(X0,s(X1))
<=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s_ax) ).
fof(f6,axiom,
! [X0,X1,X2] :
( mem(X0,u(X1,X2))
<=> ( mem(X0,X1)
| mem(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_ax) ).
fof(f7,axiom,
! [X0,X1,X2] :
( mem(X0,m(X1,X2))
<=> ( mem(X0,X1)
& ~ mem(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_ax) ).
fof(f8,axiom,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_def) ).
fof(f9,axiom,
! [X0] : n(X0) = a(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_def) ).
fof(f10,axiom,
! [X0,X1] :
( mem(X0,p(X1))
<=> subq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p_ax) ).
fof(f26,conjecture,
disj(u(s(u(n(e),n(s(n(e))))),m(p(n(n(n(e)))),n(n(n(n(e)))))),a(a(p(p(s(n(e)))),n(s(n(e)))),a(s(s(n(e))),n(n(e))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',disj_1924_4211) ).
fof(f27,negated_conjecture,
~ disj(u(s(u(n(e),n(s(n(e))))),m(p(n(n(n(e)))),n(n(n(n(e)))))),a(a(p(p(s(n(e)))),n(s(n(e)))),a(s(s(n(e))),n(n(e))))),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f28,plain,
~ disj(u(s(u(n(e),n(s(n(e))))),m(p(n(n(n(e)))),n(n(n(n(e)))))),a(a(p(p(s(n(e)))),n(s(n(e)))),a(s(s(n(e))),n(n(e))))),
inference(flattening,[],[f27]) ).
fof(f29,plain,
! [X0,X1] :
( ~ ? [X2] :
( mem(X2,X0)
& mem(X2,X1) )
=> disj(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f3]) ).
fof(f30,plain,
! [X0,X1] :
( subq(X0,X1)
<=> ! [X2] :
( mem(X2,X1)
| ~ mem(X2,X0) ) ),
inference(ennf_transformation,[],[f1]) ).
fof(f31,plain,
! [X0,X1] :
( X0 = X1
| ~ subq(X1,X0)
| ~ subq(X0,X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f32,plain,
! [X0,X1] :
( X0 = X1
| ~ subq(X1,X0)
| ~ subq(X0,X1) ),
inference(flattening,[],[f31]) ).
fof(f33,plain,
! [X0,X1] :
( disj(X0,X1)
| ? [X2] :
( mem(X2,X0)
& mem(X2,X1) ) ),
inference(ennf_transformation,[],[f29]) ).
fof(f34,plain,
! [X0,X1] :
( ( subq(X0,X1)
| ? [X2] :
( ~ mem(X2,X1)
& mem(X2,X0) ) )
& ( ! [X2] :
( mem(X2,X1)
| ~ mem(X2,X0) )
| ~ subq(X0,X1) ) ),
inference(nnf_transformation,[],[f30]) ).
fof(f35,plain,
! [X0,X1] :
( ( subq(X0,X1)
| ? [X2] :
( ~ mem(X2,X1)
& mem(X2,X0) ) )
& ( ! [X3] :
( mem(X3,X1)
| ~ mem(X3,X0) )
| ~ subq(X0,X1) ) ),
inference(rectify,[],[f34]) ).
fof(f36,plain,
! [X0,X1] :
( ( subq(X0,X1)
| ( ~ mem(sK0(X0,X1),X1)
& mem(sK0(X0,X1),X0) ) )
& ( ! [X3] :
( mem(X3,X1)
| ~ mem(X3,X0) )
| ~ subq(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f35]) ).
fof(f37,plain,
! [X0,X1] :
( disj(X0,X1)
| ( mem(sK1(X0,X1),X0)
& mem(sK1(X0,X1),X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0,X1))],[f33]) ).
fof(f38,plain,
! [X0,X1] :
( ( mem(X0,s(X1))
| X0 != X1 )
& ( X0 = X1
| ~ mem(X0,s(X1)) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f39,plain,
! [X0,X1,X2] :
( ( mem(X0,u(X1,X2))
| ( ~ mem(X0,X1)
& ~ mem(X0,X2) ) )
& ( mem(X0,X1)
| mem(X0,X2)
| ~ mem(X0,u(X1,X2)) ) ),
inference(nnf_transformation,[],[f6]) ).
fof(f40,plain,
! [X0,X1,X2] :
( ( mem(X0,u(X1,X2))
| ( ~ mem(X0,X1)
& ~ mem(X0,X2) ) )
& ( mem(X0,X1)
| mem(X0,X2)
| ~ mem(X0,u(X1,X2)) ) ),
inference(flattening,[],[f39]) ).
fof(f41,plain,
! [X0,X1,X2] :
( ( mem(X0,m(X1,X2))
| ~ mem(X0,X1)
| mem(X0,X2) )
& ( ( mem(X0,X1)
& ~ mem(X0,X2) )
| ~ mem(X0,m(X1,X2)) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f42,plain,
! [X0,X1,X2] :
( ( mem(X0,m(X1,X2))
| ~ mem(X0,X1)
| mem(X0,X2) )
& ( ( mem(X0,X1)
& ~ mem(X0,X2) )
| ~ mem(X0,m(X1,X2)) ) ),
inference(flattening,[],[f41]) ).
fof(f43,plain,
! [X0,X1] :
( ( mem(X0,p(X1))
| ~ subq(X0,X1) )
& ( subq(X0,X1)
| ~ mem(X0,p(X1)) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f44,plain,
! [X3,X0,X1] :
( ~ mem(X3,X0)
| mem(X3,X1)
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f45,plain,
! [X0,X1] :
( mem(sK0(X0,X1),X0)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f46,plain,
! [X0,X1] :
( ~ mem(sK0(X0,X1),X1)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f47,plain,
! [X0,X1] :
( ~ subq(X1,X0)
| X0 = X1
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f32]) ).
fof(f48,plain,
! [X0,X1] :
( mem(sK1(X0,X1),X1)
| disj(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f49,plain,
! [X0,X1] :
( mem(sK1(X0,X1),X0)
| disj(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f50,plain,
! [X0] : ~ mem(X0,e),
inference(cnf_transformation,[],[f4]) ).
fof(f51,plain,
! [X0,X1] :
( ~ mem(X0,s(X1))
| X0 = X1 ),
inference(cnf_transformation,[],[f38]) ).
fof(f52,plain,
! [X0,X1] :
( mem(X0,s(X1))
| X0 != X1 ),
inference(cnf_transformation,[],[f38]) ).
fof(f53,plain,
! [X2,X0,X1] :
( ~ mem(X0,u(X1,X2))
| mem(X0,X2)
| mem(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
fof(f54,plain,
! [X2,X0,X1] :
( mem(X0,u(X1,X2))
| ~ mem(X0,X2) ),
inference(cnf_transformation,[],[f40]) ).
fof(f55,plain,
! [X2,X0,X1] :
( mem(X0,u(X1,X2))
| ~ mem(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
fof(f56,plain,
! [X2,X0,X1] :
( ~ mem(X0,m(X1,X2))
| ~ mem(X0,X2) ),
inference(cnf_transformation,[],[f42]) ).
fof(f57,plain,
! [X2,X0,X1] :
( ~ mem(X0,m(X1,X2))
| mem(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f58,plain,
! [X2,X0,X1] :
( mem(X0,m(X1,X2))
| ~ mem(X0,X1)
| mem(X0,X2) ),
inference(cnf_transformation,[],[f42]) ).
fof(f59,plain,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
inference(cnf_transformation,[],[f8]) ).
fof(f60,plain,
! [X0] : n(X0) = a(X0,X0),
inference(cnf_transformation,[],[f9]) ).
fof(f61,plain,
! [X0,X1] :
( ~ mem(X0,p(X1))
| subq(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f62,plain,
! [X0,X1] :
( mem(X0,p(X1))
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f63,plain,
~ disj(u(s(u(n(e),n(s(n(e))))),m(p(n(n(n(e)))),n(n(n(n(e)))))),a(a(p(p(s(n(e)))),n(s(n(e)))),a(s(s(n(e))),n(n(e))))),
inference(cnf_transformation,[],[f28]) ).
fof(f64,plain,
! [X0] : n(X0) = u(X0,s(X0)),
inference(definition_unfolding,[],[f60,f59]) ).
fof(f65,plain,
~ disj(u(s(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),m(p(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))),u(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))),s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))))))),u(u(p(p(s(u(e,s(e))))),s(u(s(u(e,s(e))),s(s(u(e,s(e))))))),s(u(s(s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))))),
inference(definition_unfolding,[],[f63,f64,f64,f64,f64,f64,f64,f64,f64,f64,f64,f59,f59,f64,f64,f64,f59,f64,f64,f64]) ).
fof(f66,plain,
! [X1] : mem(X1,s(X1)),
inference(equality_resolution,[],[f52]) ).
fof(f67,definition,
sF2 = s(e),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f68,plain,
s(e) = sF2,
inference(reorient_equations,[],[f67]) ).
fof(f69,definition,
sF3 = u(e,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f70,plain,
u(e,sF2) = sF3,
inference(reorient_equations,[],[f69]) ).
fof(f71,definition,
sF4 = s(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f72,plain,
s(sF3) = sF4,
inference(reorient_equations,[],[f71]) ).
fof(f73,definition,
sF5 = s(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f74,plain,
s(sF4) = sF5,
inference(reorient_equations,[],[f73]) ).
fof(f75,definition,
sF6 = u(sF4,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f76,plain,
u(sF4,sF5) = sF6,
inference(reorient_equations,[],[f75]) ).
fof(f77,definition,
sF7 = u(sF3,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f78,plain,
u(sF3,sF6) = sF7,
inference(reorient_equations,[],[f77]) ).
fof(f79,definition,
sF8 = s(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f80,plain,
s(sF7) = sF8,
inference(reorient_equations,[],[f79]) ).
fof(f81,definition,
sF9 = u(sF3,sF4),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f82,plain,
u(sF3,sF4) = sF9,
inference(reorient_equations,[],[f81]) ).
fof(f83,definition,
sF10 = s(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f84,plain,
s(sF9) = sF10,
inference(reorient_equations,[],[f83]) ).
fof(f85,definition,
sF11 = u(sF9,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f86,plain,
u(sF9,sF10) = sF11,
inference(reorient_equations,[],[f85]) ).
fof(f87,definition,
sF12 = p(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f88,plain,
p(sF11) = sF12,
inference(reorient_equations,[],[f87]) ).
fof(f89,definition,
sF13 = s(sF11),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f90,plain,
s(sF11) = sF13,
inference(reorient_equations,[],[f89]) ).
fof(f91,definition,
sF14 = u(sF11,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f92,plain,
u(sF11,sF13) = sF14,
inference(reorient_equations,[],[f91]) ).
fof(f93,definition,
sF15 = m(sF12,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f94,plain,
m(sF12,sF14) = sF15,
inference(reorient_equations,[],[f93]) ).
fof(f95,definition,
sF16 = u(sF8,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f96,plain,
u(sF8,sF15) = sF16,
inference(reorient_equations,[],[f95]) ).
fof(f97,definition,
sF17 = p(sF4),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f98,plain,
p(sF4) = sF17,
inference(reorient_equations,[],[f97]) ).
fof(f99,definition,
sF18 = p(sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f100,plain,
p(sF17) = sF18,
inference(reorient_equations,[],[f99]) ).
fof(f101,definition,
sF19 = s(sF6),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f102,plain,
s(sF6) = sF19,
inference(reorient_equations,[],[f101]) ).
fof(f103,definition,
sF20 = u(sF18,sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f104,plain,
u(sF18,sF19) = sF20,
inference(reorient_equations,[],[f103]) ).
fof(f105,definition,
sF21 = u(sF5,sF10),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f106,plain,
u(sF5,sF10) = sF21,
inference(reorient_equations,[],[f105]) ).
fof(f107,definition,
sF22 = s(sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f108,plain,
s(sF21) = sF22,
inference(reorient_equations,[],[f107]) ).
fof(f109,definition,
sF23 = u(sF20,sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f110,plain,
u(sF20,sF22) = sF23,
inference(reorient_equations,[],[f109]) ).
fof(f111,plain,
~ disj(sF16,sF23),
inference(definition_folding,[],[f65,f110,f108,f106,f84,f82,f72,f70,f68,f70,f68,f74,f72,f70,f68,f104,f102,f76,f74,f72,f70,f68,f72,f70,f68,f100,f98,f72,f70,f68,f96,f94,f92,f90,f86,f84,f82,f72,f70,f68,f70,f68,f82,f72,f70,f68,f70,f68,f86,f84,f82,f72,f70,f68,f70,f68,f82,f72,f70,f68,f70,f68,f88,f86,f84,f82,f72,f70,f68,f70,f68,f82,f72,f70,f68,f70,f68,f80,f78,f76,f74,f72,f70,f68,f72,f70,f68,f70,f68]) ).
fof(f112,plain,
mem(e,sF2),
inference(superposition,[],[f66,f68]) ).
fof(f113,plain,
mem(sF3,sF4),
inference(superposition,[],[f66,f72]) ).
fof(f114,plain,
mem(sF4,sF5),
inference(superposition,[],[f66,f74]) ).
fof(f116,plain,
mem(sF7,sF8),
inference(superposition,[],[f66,f80]) ).
fof(f117,plain,
mem(sF9,sF10),
inference(superposition,[],[f66,f84]) ).
fof(f120,plain,
! [X0] :
( ~ mem(X0,sF2)
| mem(X0,sF3) ),
inference(superposition,[],[f54,f70]) ).
fof(f121,plain,
! [X0] :
( ~ mem(X0,sF4)
| mem(X0,sF9) ),
inference(superposition,[],[f54,f82]) ).
fof(f122,plain,
! [X0] :
( ~ mem(X0,sF5)
| mem(X0,sF6) ),
inference(superposition,[],[f54,f76]) ).
fof(f133,plain,
! [X0] :
( ~ mem(X0,sF3)
| mem(X0,sF9) ),
inference(superposition,[],[f55,f82]) ).
fof(f134,plain,
! [X0] :
( ~ mem(X0,sF4)
| mem(X0,sF6) ),
inference(superposition,[],[f55,f76]) ).
fof(f135,plain,
! [X0] :
( ~ mem(X0,sF8)
| mem(X0,sF16) ),
inference(superposition,[],[f55,f96]) ).
fof(f136,plain,
! [X0] :
( ~ mem(X0,sF9)
| mem(X0,sF11) ),
inference(superposition,[],[f55,f86]) ).
fof(f137,plain,
! [X0] :
( ~ mem(X0,sF11)
| mem(X0,sF14) ),
inference(superposition,[],[f55,f92]) ).
fof(f146,plain,
! [X0] :
( ~ mem(X0,sF12)
| subq(X0,sF11) ),
inference(superposition,[],[f61,f88]) ).
fof(f147,plain,
! [X0] :
( ~ mem(X0,sF17)
| subq(X0,sF4) ),
inference(superposition,[],[f61,f98]) ).
fof(f148,plain,
! [X0] :
( ~ mem(X0,sF18)
| subq(X0,sF17) ),
inference(superposition,[],[f61,f100]) ).
fof(f149,plain,
! [X0] :
( ~ mem(X0,sF5)
| mem(X0,sF21) ),
inference(superposition,[],[f55,f106]) ).
fof(f155,plain,
! [X0] :
( ~ mem(X0,sF15)
| ~ mem(X0,sF14) ),
inference(superposition,[],[f56,f94]) ).
fof(f156,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X1)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f46,f55]) ).
fof(f157,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X2)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f46,f54]) ).
fof(f161,plain,
! [X0] :
( ~ mem(X0,sF2)
| e = X0 ),
inference(superposition,[],[f51,f68]) ).
fof(f162,plain,
! [X0] :
( ~ mem(X0,sF4)
| sF3 = X0 ),
inference(superposition,[],[f51,f72]) ).
fof(f163,plain,
! [X0] :
( ~ mem(X0,sF5)
| sF4 = X0 ),
inference(superposition,[],[f51,f74]) ).
fof(f164,plain,
! [X0] :
( ~ mem(X0,sF19)
| sF6 = X0 ),
inference(superposition,[],[f51,f102]) ).
fof(f165,plain,
! [X0] :
( ~ mem(X0,sF8)
| sF7 = X0 ),
inference(superposition,[],[f51,f80]) ).
fof(f166,plain,
! [X0] :
( ~ mem(X0,sF10)
| sF9 = X0 ),
inference(superposition,[],[f51,f84]) ).
fof(f168,plain,
! [X0] :
( ~ mem(X0,sF22)
| sF21 = X0 ),
inference(superposition,[],[f51,f108]) ).
fof(f171,plain,
! [X0] :
( ~ mem(X0,sF3)
| mem(X0,sF7) ),
inference(superposition,[],[f55,f78]) ).
fof(f172,plain,
! [X0] :
( ~ mem(X0,sF6)
| mem(X0,sF7) ),
inference(superposition,[],[f54,f78]) ).
fof(f177,plain,
mem(sF4,sF6),
inference(resolution,[],[f122,f114]) ).
fof(f180,plain,
! [X0] :
( ~ mem(X0,sF15)
| mem(X0,sF12) ),
inference(superposition,[],[f57,f94]) ).
fof(f181,plain,
mem(e,sF3),
inference(resolution,[],[f120,f112]) ).
fof(f188,plain,
mem(sF3,sF9),
inference(resolution,[],[f113,f121]) ).
fof(f193,plain,
mem(sF3,sF6),
inference(resolution,[],[f134,f113]) ).
fof(f196,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,m(X1,X2)),X1)
| mem(sK0(X0,m(X1,X2)),X2)
| subq(X0,m(X1,X2)) ),
inference(resolution,[],[f58,f46]) ).
fof(f203,plain,
! [X0] :
( ~ mem(X0,sF3)
| mem(X0,sF2)
| mem(X0,e) ),
inference(superposition,[],[f53,f70]) ).
fof(f204,plain,
! [X0] :
( ~ mem(X0,sF9)
| mem(X0,sF4)
| mem(X0,sF3) ),
inference(superposition,[],[f53,f82]) ).
fof(f205,plain,
! [X0] :
( ~ mem(X0,sF7)
| mem(X0,sF6)
| mem(X0,sF3) ),
inference(superposition,[],[f53,f78]) ).
fof(f206,plain,
! [X0] :
( ~ mem(X0,sF6)
| mem(X0,sF5)
| mem(X0,sF4) ),
inference(superposition,[],[f53,f76]) ).
fof(f207,plain,
! [X0] :
( ~ mem(X0,sF21)
| mem(X0,sF10)
| mem(X0,sF5) ),
inference(superposition,[],[f53,f106]) ).
fof(f208,plain,
! [X0] :
( ~ mem(X0,sF16)
| mem(X0,sF15)
| mem(X0,sF8) ),
inference(superposition,[],[f53,f96]) ).
fof(f209,plain,
! [X0] :
( ~ mem(X0,sF11)
| mem(X0,sF10)
| mem(X0,sF9) ),
inference(superposition,[],[f53,f86]) ).
fof(f211,plain,
! [X0] :
( ~ mem(X0,sF20)
| mem(X0,sF19)
| mem(X0,sF18) ),
inference(superposition,[],[f53,f104]) ).
fof(f212,plain,
! [X0] :
( ~ mem(X0,sF23)
| mem(X0,sF22)
| mem(X0,sF20) ),
inference(superposition,[],[f53,f110]) ).
fof(f213,plain,
! [X0] :
( ~ mem(X0,sF3)
| mem(X0,sF2) ),
inference(forward_subsumption_resolution,[],[f203,f50]) ).
fof(f219,plain,
! [X0] :
( ~ subq(X0,sF4)
| mem(X0,sF17) ),
inference(superposition,[],[f62,f98]) ).
fof(f220,plain,
! [X0] :
( ~ subq(X0,sF17)
| mem(X0,sF18) ),
inference(superposition,[],[f62,f100]) ).
fof(f221,plain,
! [X0] :
( subq(X0,X0)
| subq(X0,X0) ),
inference(resolution,[],[f45,f46]) ).
fof(f222,plain,
! [X0] : subq(e,X0),
inference(resolution,[],[f45,f50]) ).
fof(f223,plain,
! [X0,X1] :
( subq(s(X0),X1)
| sK0(s(X0),X1) = X0 ),
inference(resolution,[],[f45,f51]) ).
fof(f224,plain,
! [X2,X0,X1] :
( mem(sK0(u(X0,X1),X2),X1)
| mem(sK0(u(X0,X1),X2),X0)
| subq(u(X0,X1),X2) ),
inference(resolution,[],[f45,f53]) ).
fof(f225,plain,
! [X2,X0,X1] :
( mem(sK0(m(X0,X1),X2),X0)
| subq(m(X0,X1),X2) ),
inference(resolution,[],[f45,f57]) ).
fof(f226,plain,
! [X2,X0,X1] :
( ~ mem(sK0(m(X0,X1),X2),X1)
| subq(m(X0,X1),X2) ),
inference(resolution,[],[f45,f56]) ).
fof(f229,plain,
! [X0] :
( mem(sK0(sF4,X0),sF6)
| subq(sF4,X0) ),
inference(resolution,[],[f45,f134]) ).
fof(f240,plain,
! [X0] : subq(X0,X0),
inference(duplicate_literal_removal,[],[f221]) ).
fof(f241,plain,
mem(e,sF9),
inference(resolution,[],[f133,f181]) ).
fof(f248,plain,
mem(sF7,sF16),
inference(resolution,[],[f116,f135]) ).
fof(f264,plain,
! [X0] :
( mem(sK0(sF16,X0),sF15)
| mem(sK0(sF16,X0),sF8)
| subq(sF16,X0) ),
inference(resolution,[],[f208,f45]) ).
fof(f266,plain,
! [X0] :
( mem(sK1(sF16,X0),sF15)
| mem(sK1(sF16,X0),sF8)
| disj(sF16,X0) ),
inference(resolution,[],[f208,f49]) ).
fof(f268,plain,
! [X0] :
( mem(sK1(X0,sF23),sF22)
| mem(sK1(X0,sF23),sF20)
| disj(X0,sF23) ),
inference(resolution,[],[f212,f48]) ).
fof(f271,plain,
! [X0] :
( mem(sK0(sF3,X0),sF2)
| subq(sF3,X0) ),
inference(resolution,[],[f213,f45]) ).
fof(f274,plain,
! [X0] :
( subq(sF8,X0)
| sF7 = sK0(sF8,X0) ),
inference(resolution,[],[f165,f45]) ).
fof(f295,plain,
mem(e,sF11),
inference(resolution,[],[f136,f241]) ).
fof(f300,plain,
mem(e,sF14),
inference(resolution,[],[f295,f137]) ).
fof(f332,plain,
mem(sF4,sF21),
inference(resolution,[],[f149,f114]) ).
fof(f339,plain,
mem(sF4,sF7),
inference(resolution,[],[f172,f177]) ).
fof(f340,plain,
mem(sF3,sF7),
inference(resolution,[],[f193,f172]) ).
fof(f342,plain,
mem(e,sF7),
inference(resolution,[],[f171,f181]) ).
fof(f354,plain,
mem(sF3,sF11),
inference(resolution,[],[f188,f136]) ).
fof(f357,plain,
mem(sF3,sF14),
inference(resolution,[],[f354,f137]) ).
fof(f371,plain,
! [X0,X1] :
( ~ subq(s(X0),X1)
| mem(X0,X1) ),
inference(resolution,[],[f44,f66]) ).
fof(f377,plain,
! [X0] :
( ~ subq(sF3,X0)
| mem(e,X0) ),
inference(resolution,[],[f44,f181]) ).
fof(f382,plain,
! [X2,X0,X1] :
( mem(sK0(X0,X1),X2)
| ~ subq(X0,X2)
| subq(X0,X1) ),
inference(resolution,[],[f44,f45]) ).
fof(f383,plain,
! [X2,X0,X1] :
( mem(sK1(X0,X1),X2)
| ~ subq(X1,X2)
| disj(X0,X1) ),
inference(resolution,[],[f44,f48]) ).
fof(f385,plain,
! [X0] :
( ~ subq(sF4,X0)
| mem(sF3,X0) ),
inference(resolution,[],[f44,f113]) ).
fof(f387,plain,
! [X0] :
( ~ subq(sF7,X0)
| mem(sF3,X0) ),
inference(resolution,[],[f44,f340]) ).
fof(f388,plain,
! [X0] :
( ~ subq(sF9,X0)
| mem(sF3,X0) ),
inference(resolution,[],[f44,f188]) ).
fof(f391,plain,
! [X0] :
( ~ subq(sF5,X0)
| mem(sF4,X0) ),
inference(resolution,[],[f44,f114]) ).
fof(f392,plain,
! [X0] :
( ~ subq(sF6,X0)
| mem(sF4,X0) ),
inference(resolution,[],[f44,f177]) ).
fof(f393,plain,
! [X0] :
( ~ subq(sF7,X0)
| mem(sF4,X0) ),
inference(resolution,[],[f44,f339]) ).
fof(f398,plain,
! [X0] :
( ~ subq(sF8,X0)
| mem(sF7,X0) ),
inference(resolution,[],[f44,f116]) ).
fof(f399,plain,
! [X0] :
( ~ subq(sF16,X0)
| mem(sF7,X0) ),
inference(resolution,[],[f44,f248]) ).
fof(f414,plain,
! [X0] :
( ~ subq(X0,e)
| e = X0 ),
inference(resolution,[],[f47,f222]) ).
fof(f417,plain,
mem(e,sF17),
inference(resolution,[],[f219,f222]) ).
fof(f418,plain,
! [X0] :
( mem(sK1(sF16,X0),sF12)
| disj(sF16,X0)
| mem(sK1(sF16,X0),sF8) ),
inference(resolution,[],[f266,f180]) ).
fof(f421,plain,
! [X0,X1] :
( mem(sK1(sF16,X0),sF8)
| mem(sK1(sF16,X0),X1)
| disj(sF16,X0)
| ~ subq(sF15,X1) ),
inference(resolution,[],[f266,f44]) ).
fof(f434,plain,
! [X0] :
( subq(sK1(sF16,X0),sF11)
| mem(sK1(sF16,X0),sF8)
| disj(sF16,X0) ),
inference(resolution,[],[f418,f146]) ).
fof(f453,plain,
! [X0] :
( mem(sK0(sF16,X0),sF12)
| subq(sF16,X0)
| mem(sK0(sF16,X0),sF8) ),
inference(resolution,[],[f264,f180]) ).
fof(f468,plain,
( subq(sF16,sF12)
| mem(sK0(sF16,sF12),sF8)
| subq(sF16,sF12) ),
inference(resolution,[],[f453,f46]) ).
fof(f472,plain,
( subq(sF16,sF12)
| mem(sK0(sF16,sF12),sF8) ),
inference(duplicate_literal_removal,[],[f468]) ).
fof(f475,definition,
( spl24_5
<=> mem(sK0(sF16,sF12),sF8) ),
introduced(definition,[new_symbols(definition,[spl24_5])],[avatar_definition]) ).
fof(f477,plain,
( mem(sK0(sF16,sF12),sF8)
| ~ spl24_5 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f479,definition,
( spl24_6
<=> subq(sF16,sF12) ),
introduced(definition,[new_symbols(definition,[spl24_6])],[avatar_definition]) ).
fof(f481,plain,
( subq(sF16,sF12)
| ~ spl24_6 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f482,plain,
( spl24_5
| spl24_6 ),
inference(avatar_split_clause,[],[f472,f479,f475]) ).
fof(f582,plain,
! [X0] :
( mem(sK1(X0,sF23),sF20)
| disj(X0,sF23)
| sF21 = sK1(X0,sF23) ),
inference(resolution,[],[f268,f168]) ).
fof(f586,plain,
! [X0] :
( mem(sK1(X0,sF23),sF19)
| sF21 = sK1(X0,sF23)
| disj(X0,sF23)
| mem(sK1(X0,sF23),sF18) ),
inference(resolution,[],[f582,f211]) ).
fof(f589,plain,
! [X0] :
( mem(sK1(X0,sF23),sF18)
| disj(X0,sF23)
| sF21 = sK1(X0,sF23)
| sF6 = sK1(X0,sF23) ),
inference(resolution,[],[f586,f164]) ).
fof(f593,plain,
! [X0] :
( subq(sK1(X0,sF23),sF17)
| sF21 = sK1(X0,sF23)
| sF6 = sK1(X0,sF23)
| disj(X0,sF23) ),
inference(resolution,[],[f589,f148]) ).
fof(f616,plain,
( subq(sF3,sF2)
| subq(sF3,sF2) ),
inference(resolution,[],[f271,f46]) ).
fof(f617,plain,
! [X0] :
( subq(sF3,X0)
| e = sK0(sF3,X0) ),
inference(resolution,[],[f271,f161]) ).
fof(f620,plain,
subq(sF3,sF2),
inference(duplicate_literal_removal,[],[f616]) ).
fof(f621,plain,
! [X0] :
( mem(e,X0)
| e = sK0(sF3,X0) ),
inference(resolution,[],[f617,f377]) ).
fof(f622,plain,
! [X0] :
( ~ subq(X0,sF3)
| sF3 = X0
| e = sK0(sF3,X0) ),
inference(resolution,[],[f617,f47]) ).
fof(f625,plain,
( e = sK0(sF3,sF17)
| mem(sF3,sF18) ),
inference(resolution,[],[f617,f220]) ).
fof(f627,definition,
( spl24_21
<=> mem(sF3,sF18) ),
introduced(definition,[new_symbols(definition,[spl24_21])],[avatar_definition]) ).
fof(f628,plain,
( ~ mem(sF3,sF18)
| spl24_21 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f629,plain,
( mem(sF3,sF18)
| ~ spl24_21 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f631,definition,
( spl24_22
<=> e = sK0(sF3,sF17) ),
introduced(definition,[new_symbols(definition,[spl24_22])],[avatar_definition]) ).
fof(f633,plain,
( e = sK0(sF3,sF17)
| ~ spl24_22 ),
inference(avatar_component_clause,[],[f631]) ).
fof(f634,plain,
( spl24_21
| spl24_22 ),
inference(avatar_split_clause,[],[f625,f631,f627]) ).
fof(f645,definition,
( spl24_25
<=> mem(sF3,sF17) ),
introduced(definition,[new_symbols(definition,[spl24_25])],[avatar_definition]) ).
fof(f646,plain,
( ~ mem(sF3,sF17)
| spl24_25 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f647,plain,
( mem(sF3,sF17)
| ~ spl24_25 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f664,plain,
( subq(sF3,sF4)
| ~ spl24_25 ),
inference(resolution,[],[f647,f147]) ).
fof(f667,plain,
( sF2 = sF3
| ~ subq(sF2,sF3) ),
inference(resolution,[],[f620,f47]) ).
fof(f669,definition,
( spl24_27
<=> subq(sF2,sF3) ),
introduced(definition,[new_symbols(definition,[spl24_27])],[avatar_definition]) ).
fof(f671,plain,
( ~ subq(sF2,sF3)
| spl24_27 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f673,definition,
( spl24_28
<=> sF2 = sF3 ),
introduced(definition,[new_symbols(definition,[spl24_28])],[avatar_definition]) ).
fof(f675,plain,
( sF2 = sF3
| ~ spl24_28 ),
inference(avatar_component_clause,[],[f673]) ).
fof(f676,plain,
( ~ spl24_27
| spl24_28 ),
inference(avatar_split_clause,[],[f667,f673,f669]) ).
fof(f677,plain,
( mem(e,sF4)
| ~ spl24_25 ),
inference(resolution,[],[f664,f377]) ).
fof(f681,definition,
( spl24_29
<=> subq(sF4,sF3) ),
introduced(definition,[new_symbols(definition,[spl24_29])],[avatar_definition]) ).
fof(f682,plain,
( subq(sF4,sF3)
| ~ spl24_29 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f683,plain,
( ~ subq(sF4,sF3)
| spl24_29 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f685,definition,
( spl24_30
<=> sF3 = sF4 ),
introduced(definition,[new_symbols(definition,[spl24_30])],[avatar_definition]) ).
fof(f686,plain,
( sF3 != sF4
| spl24_30 ),
inference(avatar_component_clause,[],[f685]) ).
fof(f687,plain,
( sF3 = sF4
| ~ spl24_30 ),
inference(avatar_component_clause,[],[f685]) ).
fof(f689,plain,
( e = sF3
| ~ spl24_25 ),
inference(resolution,[],[f677,f162]) ).
fof(f693,plain,
( ! [X0] : ~ mem(X0,sF3)
| ~ spl24_25 ),
inference(superposition,[],[f50,f689]) ).
fof(f694,plain,
( sF2 = s(sF3)
| ~ spl24_25 ),
inference(superposition,[],[f68,f689]) ).
fof(f711,plain,
( sF2 = sF4
| ~ spl24_25 ),
inference(forward_demodulation,[],[f694,f72]) ).
fof(f712,plain,
( sF3 = u(e,sF4)
| ~ spl24_25 ),
inference(superposition,[],[f70,f711]) ).
fof(f714,plain,
( ! [X0] :
( ~ mem(X0,sF4)
| mem(X0,sF3) )
| ~ spl24_25 ),
inference(superposition,[],[f120,f711]) ).
fof(f719,plain,
( ! [X0] : ~ mem(X0,sF4)
| ~ spl24_25 ),
inference(forward_subsumption_resolution,[],[f714,f693]) ).
fof(f720,plain,
( sF3 = u(sF3,sF4)
| ~ spl24_25 ),
inference(forward_demodulation,[],[f712,f689]) ).
fof(f721,plain,
( sF3 = sF9
| ~ spl24_25 ),
inference(forward_demodulation,[],[f720,f82]) ).
fof(f722,plain,
( s(sF3) = sF10
| ~ spl24_25 ),
inference(superposition,[],[f84,f721]) ).
fof(f735,plain,
( sF4 = sF10
| ~ spl24_25 ),
inference(forward_demodulation,[],[f722,f72]) ).
fof(f738,plain,
( mem(sF9,sF4)
| ~ spl24_25 ),
inference(superposition,[],[f117,f735]) ).
fof(f742,plain,
( $false
| ~ spl24_25 ),
inference(forward_subsumption_resolution,[],[f738,f719]) ).
fof(f743,plain,
~ spl24_25,
inference(avatar_contradiction_clause,[],[f742]) ).
fof(f822,plain,
! [X0,X1] :
( mem(sK1(X1,X0),sF22)
| disj(X1,X0)
| ~ subq(X0,sF23)
| mem(sK1(X1,X0),sF20) ),
inference(resolution,[],[f383,f212]) ).
fof(f903,plain,
( e = sK0(sF3,sF5)
| e = sF4 ),
inference(resolution,[],[f621,f163]) ).
fof(f947,definition,
( spl24_39
<=> mem(e,sF5) ),
introduced(definition,[new_symbols(definition,[spl24_39])],[avatar_definition]) ).
fof(f948,plain,
( ~ mem(e,sF5)
| spl24_39 ),
inference(avatar_component_clause,[],[f947]) ).
fof(f949,plain,
( mem(e,sF5)
| ~ spl24_39 ),
inference(avatar_component_clause,[],[f947]) ).
fof(f1020,definition,
( spl24_55
<=> e = sF7 ),
introduced(definition,[new_symbols(definition,[spl24_55])],[avatar_definition]) ).
fof(f1021,plain,
( e != sF7
| spl24_55 ),
inference(avatar_component_clause,[],[f1020]) ).
fof(f1022,plain,
( e = sF7
| ~ spl24_55 ),
inference(avatar_component_clause,[],[f1020]) ).
fof(f1025,definition,
( spl24_56
<=> mem(e,sF4) ),
introduced(definition,[new_symbols(definition,[spl24_56])],[avatar_definition]) ).
fof(f1026,plain,
( ~ mem(e,sF4)
| spl24_56 ),
inference(avatar_component_clause,[],[f1025]) ).
fof(f1027,plain,
( mem(e,sF4)
| ~ spl24_56 ),
inference(avatar_component_clause,[],[f1025]) ).
fof(f1038,definition,
( spl24_59
<=> e = sK0(sF3,sF5) ),
introduced(definition,[new_symbols(definition,[spl24_59])],[avatar_definition]) ).
fof(f1040,plain,
( e = sK0(sF3,sF5)
| ~ spl24_59 ),
inference(avatar_component_clause,[],[f1038]) ).
fof(f1043,definition,
( spl24_60
<=> e = sF4 ),
introduced(definition,[new_symbols(definition,[spl24_60])],[avatar_definition]) ).
fof(f1044,plain,
( e != sF4
| spl24_60 ),
inference(avatar_component_clause,[],[f1043]) ).
fof(f1045,plain,
( e = sF4
| ~ spl24_60 ),
inference(avatar_component_clause,[],[f1043]) ).
fof(f1046,plain,
( spl24_60
| spl24_59 ),
inference(avatar_split_clause,[],[f903,f1038,f1043]) ).
fof(f1209,definition,
( spl24_67
<=> subq(sF15,sF16) ),
introduced(definition,[new_symbols(definition,[spl24_67])],[avatar_definition]) ).
fof(f1210,plain,
( subq(sF15,sF16)
| ~ spl24_67 ),
inference(avatar_component_clause,[],[f1209]) ).
fof(f1211,plain,
( ~ subq(sF15,sF16)
| spl24_67 ),
inference(avatar_component_clause,[],[f1209]) ).
fof(f1218,plain,
mem(sF4,sF17),
inference(resolution,[],[f240,f219]) ).
fof(f1276,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF5)
| subq(X0,X1)
| ~ subq(X0,sF6)
| mem(sK0(X0,X1),sF4) ),
inference(resolution,[],[f382,f206]) ).
fof(f1281,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF3)
| subq(X0,X1)
| mem(sK0(X0,X1),sF4)
| ~ subq(X0,sF9) ),
inference(resolution,[],[f382,f204]) ).
fof(f1285,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF10)
| subq(X0,X1)
| ~ subq(X0,sF11)
| mem(sK0(X0,X1),sF9) ),
inference(resolution,[],[f382,f209]) ).
fof(f1303,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF10)
| subq(X0,X1)
| ~ subq(X0,sF21)
| mem(sK0(X0,X1),sF5) ),
inference(resolution,[],[f382,f207]) ).
fof(f1403,plain,
! [X0,X1] :
( mem(sK0(X0,m(X0,X1)),X1)
| subq(X0,m(X0,X1))
| subq(X0,m(X0,X1)) ),
inference(resolution,[],[f196,f45]) ).
fof(f1425,plain,
! [X0,X1] :
( mem(sK0(X0,m(X0,X1)),X1)
| subq(X0,m(X0,X1)) ),
inference(duplicate_literal_removal,[],[f1403]) ).
fof(f1437,plain,
! [X0,X1] :
( ~ subq(X1,s(X0))
| s(X0) = X1
| sK0(s(X0),X1) = X0 ),
inference(resolution,[],[f223,f47]) ).
fof(f1449,plain,
! [X0,X1] :
( subq(X0,u(X1,X0))
| subq(X0,u(X1,X0)) ),
inference(resolution,[],[f157,f45]) ).
fof(f1467,plain,
! [X0] :
( ~ mem(sK0(X0,sF16),sF15)
| subq(X0,sF16) ),
inference(superposition,[],[f157,f96]) ).
fof(f1481,plain,
! [X0,X1] : subq(X0,u(X1,X0)),
inference(duplicate_literal_removal,[],[f1449]) ).
fof(f1500,plain,
( subq(sF15,sF16)
| subq(sF15,sF16) ),
inference(resolution,[],[f1467,f45]) ).
fof(f1503,plain,
subq(sF15,sF16),
inference(duplicate_literal_removal,[],[f1500]) ).
fof(f1505,plain,
( $false
| spl24_67 ),
inference(forward_subsumption_resolution,[],[f1503,f1211]) ).
fof(f1506,plain,
spl24_67,
inference(avatar_contradiction_clause,[],[f1505]) ).
fof(f1573,definition,
( spl24_75
<=> subq(sF3,sF4) ),
introduced(definition,[new_symbols(definition,[spl24_75])],[avatar_definition]) ).
fof(f1574,plain,
( ~ subq(sF3,sF4)
| spl24_75 ),
inference(avatar_component_clause,[],[f1573]) ).
fof(f1575,plain,
( subq(sF3,sF4)
| ~ spl24_75 ),
inference(avatar_component_clause,[],[f1573]) ).
fof(f1581,plain,
! [X0,X1] :
( mem(X0,X1)
| sK0(s(X0),X1) = X0 ),
inference(resolution,[],[f371,f223]) ).
fof(f1634,plain,
! [X0] :
( sK0(s(X0),sF19) = X0
| sF6 = X0 ),
inference(resolution,[],[f1581,f164]) ).
fof(f1639,plain,
! [X0] :
( sK0(s(X0),sF22) = X0
| sF21 = X0 ),
inference(resolution,[],[f1581,f168]) ).
fof(f1914,plain,
( sF7 = sK0(sF16,sF12)
| ~ spl24_5 ),
inference(resolution,[],[f477,f165]) ).
fof(f1916,plain,
( ! [X0] :
( mem(sK0(sF16,sF12),X0)
| ~ subq(sF8,X0) )
| ~ spl24_5 ),
inference(resolution,[],[f477,f44]) ).
fof(f1927,definition,
( spl24_89
<=> subq(sF5,sF4) ),
introduced(definition,[new_symbols(definition,[spl24_89])],[avatar_definition]) ).
fof(f1928,plain,
( ~ subq(sF5,sF4)
| spl24_89 ),
inference(avatar_component_clause,[],[f1927]) ).
fof(f1929,plain,
( subq(sF5,sF4)
| ~ spl24_89 ),
inference(avatar_component_clause,[],[f1927]) ).
fof(f1931,definition,
( spl24_90
<=> mem(sF4,sF4) ),
introduced(definition,[new_symbols(definition,[spl24_90])],[avatar_definition]) ).
fof(f1932,plain,
( mem(sF4,sF4)
| ~ spl24_90 ),
inference(avatar_component_clause,[],[f1931]) ).
fof(f1933,plain,
( ~ mem(sF4,sF4)
| spl24_90 ),
inference(avatar_component_clause,[],[f1931]) ).
fof(f2018,plain,
! [X0,X1] :
( subq(X0,u(X0,X1))
| subq(X0,u(X0,X1)) ),
inference(resolution,[],[f156,f45]) ).
fof(f2051,plain,
! [X0,X1] : subq(X0,u(X0,X1)),
inference(duplicate_literal_removal,[],[f2018]) ).
fof(f2099,definition,
( spl24_101
<=> mem(sF7,sF12) ),
introduced(definition,[new_symbols(definition,[spl24_101])],[avatar_definition]) ).
fof(f2100,plain,
( mem(sF7,sF12)
| ~ spl24_101 ),
inference(avatar_component_clause,[],[f2099]) ).
fof(f2101,plain,
( ~ mem(sF7,sF12)
| spl24_101 ),
inference(avatar_component_clause,[],[f2099]) ).
fof(f2345,definition,
( spl24_130
<=> subq(sF4,sF9) ),
introduced(definition,[new_symbols(definition,[spl24_130])],[avatar_definition]) ).
fof(f2346,plain,
( subq(sF4,sF9)
| ~ spl24_130 ),
inference(avatar_component_clause,[],[f2345]) ).
fof(f2347,plain,
( ~ subq(sF4,sF9)
| spl24_130 ),
inference(avatar_component_clause,[],[f2345]) ).
fof(f2349,definition,
( spl24_131
<=> sF4 = sF9 ),
introduced(definition,[new_symbols(definition,[spl24_131])],[avatar_definition]) ).
fof(f2350,plain,
( sF4 != sF9
| spl24_131 ),
inference(avatar_component_clause,[],[f2349]) ).
fof(f2351,plain,
( sF4 = sF9
| ~ spl24_131 ),
inference(avatar_component_clause,[],[f2349]) ).
fof(f2577,plain,
subq(sF2,sF3),
inference(superposition,[],[f1481,f70]) ).
fof(f2578,plain,
subq(sF4,sF9),
inference(superposition,[],[f1481,f82]) ).
fof(f2581,plain,
subq(sF10,sF21),
inference(superposition,[],[f1481,f106]) ).
fof(f2596,plain,
( $false
| spl24_130 ),
inference(forward_subsumption_resolution,[],[f2578,f2347]) ).
fof(f2597,plain,
spl24_130,
inference(avatar_contradiction_clause,[],[f2596]) ).
fof(f2598,plain,
( $false
| spl24_27 ),
inference(forward_subsumption_resolution,[],[f2577,f671]) ).
fof(f2599,plain,
spl24_27,
inference(avatar_contradiction_clause,[],[f2598]) ).
fof(f2685,plain,
( ! [X0] :
( ~ mem(X0,sF3)
| e = X0 )
| ~ spl24_28 ),
inference(superposition,[],[f161,f675]) ).
fof(f2727,plain,
( ~ mem(sF4,sF17)
| spl24_25
| ~ spl24_30 ),
inference(superposition,[],[f646,f687]) ).
fof(f2750,plain,
( $false
| spl24_25
| ~ spl24_30 ),
inference(forward_subsumption_resolution,[],[f2727,f1218]) ).
fof(f2751,plain,
( spl24_25
| ~ spl24_30 ),
inference(avatar_contradiction_clause,[],[f2750]) ).
fof(f2810,plain,
( mem(sF3,sF3)
| ~ spl24_29 ),
inference(resolution,[],[f682,f385]) ).
fof(f2985,plain,
( e = sF4
| ~ spl24_39 ),
inference(resolution,[],[f949,f163]) ).
fof(f3355,plain,
( e = sF3
| ~ spl24_28
| ~ spl24_29 ),
inference(resolution,[],[f2685,f2810]) ).
fof(f3361,plain,
( sF2 = s(sF3)
| ~ spl24_28
| ~ spl24_29 ),
inference(superposition,[],[f68,f3355]) ).
fof(f3383,plain,
( sF2 = sF4
| ~ spl24_28
| ~ spl24_29 ),
inference(forward_demodulation,[],[f3361,f72]) ).
fof(f3384,plain,
( sF3 = sF4
| ~ spl24_28
| ~ spl24_29 ),
inference(forward_demodulation,[],[f3383,f675]) ).
fof(f3385,plain,
( $false
| ~ spl24_28
| ~ spl24_29
| spl24_30 ),
inference(forward_subsumption_resolution,[],[f3384,f686]) ).
fof(f3386,plain,
( ~ spl24_28
| ~ spl24_29
| spl24_30 ),
inference(avatar_contradiction_clause,[],[f3385]) ).
fof(f3588,plain,
( sF10 = sF21
| ~ subq(sF21,sF10) ),
inference(resolution,[],[f2581,f47]) ).
fof(f3623,definition,
( spl24_162
<=> sF6 = sF7 ),
introduced(definition,[new_symbols(definition,[spl24_162])],[avatar_definition]) ).
fof(f3624,plain,
( sF6 != sF7
| spl24_162 ),
inference(avatar_component_clause,[],[f3623]) ).
fof(f3625,plain,
( sF6 = sF7
| ~ spl24_162 ),
inference(avatar_component_clause,[],[f3623]) ).
fof(f3716,definition,
( spl24_167
<=> subq(sF21,sF10) ),
introduced(definition,[new_symbols(definition,[spl24_167])],[avatar_definition]) ).
fof(f3718,plain,
( ~ subq(sF21,sF10)
| spl24_167 ),
inference(avatar_component_clause,[],[f3716]) ).
fof(f3720,definition,
( spl24_168
<=> sF10 = sF21 ),
introduced(definition,[new_symbols(definition,[spl24_168])],[avatar_definition]) ).
fof(f3722,plain,
( sF10 = sF21
| ~ spl24_168 ),
inference(avatar_component_clause,[],[f3720]) ).
fof(f3723,plain,
( ~ spl24_167
| spl24_168 ),
inference(avatar_split_clause,[],[f3588,f3720,f3716]) ).
fof(f3936,plain,
( sF4 = sF9
| ~ subq(sF9,sF4)
| ~ spl24_130 ),
inference(resolution,[],[f2346,f47]) ).
fof(f3937,plain,
( ~ subq(sF9,sF4)
| ~ spl24_130
| spl24_131 ),
inference(forward_subsumption_resolution,[],[f3936,f2350]) ).
fof(f4100,plain,
( sF3 = sF4
| ~ spl24_90 ),
inference(resolution,[],[f1932,f162]) ).
fof(f4104,plain,
( $false
| spl24_30
| ~ spl24_90 ),
inference(forward_subsumption_resolution,[],[f4100,f686]) ).
fof(f4105,plain,
( spl24_30
| ~ spl24_90 ),
inference(avatar_contradiction_clause,[],[f4104]) ).
fof(f4107,definition,
( spl24_190
<=> mem(sF4,sF11) ),
introduced(definition,[new_symbols(definition,[spl24_190])],[avatar_definition]) ).
fof(f4108,plain,
( ~ mem(sF4,sF11)
| spl24_190 ),
inference(avatar_component_clause,[],[f4107]) ).
fof(f4109,plain,
( mem(sF4,sF11)
| ~ spl24_190 ),
inference(avatar_component_clause,[],[f4107]) ).
fof(f4225,plain,
( ~ mem(e,sF17)
| subq(sF3,sF17)
| ~ spl24_22 ),
inference(superposition,[],[f46,f633]) ).
fof(f4226,plain,
( subq(sF3,sF17)
| ~ spl24_22 ),
inference(forward_subsumption_resolution,[],[f4225,f417]) ).
fof(f4228,plain,
( mem(sF3,sF18)
| ~ spl24_22 ),
inference(resolution,[],[f4226,f220]) ).
fof(f4230,plain,
( $false
| spl24_21
| ~ spl24_22 ),
inference(forward_subsumption_resolution,[],[f4228,f628]) ).
fof(f4231,plain,
( spl24_21
| ~ spl24_22 ),
inference(avatar_contradiction_clause,[],[f4230]) ).
fof(f4335,definition,
( spl24_201
<=> sF4 = sF21 ),
introduced(definition,[new_symbols(definition,[spl24_201])],[avatar_definition]) ).
fof(f4336,plain,
( sF4 != sF21
| spl24_201 ),
inference(avatar_component_clause,[],[f4335]) ).
fof(f4337,plain,
( sF4 = sF21
| ~ spl24_201 ),
inference(avatar_component_clause,[],[f4335]) ).
fof(f4345,definition,
( spl24_203
<=> mem(sF4,sF18) ),
introduced(definition,[new_symbols(definition,[spl24_203])],[avatar_definition]) ).
fof(f4346,plain,
( ~ mem(sF4,sF18)
| spl24_203 ),
inference(avatar_component_clause,[],[f4345]) ).
fof(f4347,plain,
( mem(sF4,sF18)
| ~ spl24_203 ),
inference(avatar_component_clause,[],[f4345]) ).
fof(f4359,definition,
( spl24_206
<=> sF4 = sF6 ),
introduced(definition,[new_symbols(definition,[spl24_206])],[avatar_definition]) ).
fof(f4360,plain,
( sF4 != sF6
| spl24_206 ),
inference(avatar_component_clause,[],[f4359]) ).
fof(f4361,plain,
( sF4 = sF6
| ~ spl24_206 ),
inference(avatar_component_clause,[],[f4359]) ).
fof(f4369,definition,
( spl24_208
<=> subq(sF4,sF17) ),
introduced(definition,[new_symbols(definition,[spl24_208])],[avatar_definition]) ).
fof(f4370,plain,
( ~ subq(sF4,sF17)
| spl24_208 ),
inference(avatar_component_clause,[],[f4369]) ).
fof(f4371,plain,
( subq(sF4,sF17)
| ~ spl24_208 ),
inference(avatar_component_clause,[],[f4369]) ).
fof(f4392,definition,
( spl24_212
<=> sF4 = sF7 ),
introduced(definition,[new_symbols(definition,[spl24_212])],[avatar_definition]) ).
fof(f4393,plain,
( sF4 != sF7
| spl24_212 ),
inference(avatar_component_clause,[],[f4392]) ).
fof(f4394,plain,
( sF4 = sF7
| ~ spl24_212 ),
inference(avatar_component_clause,[],[f4392]) ).
fof(f4401,definition,
( spl24_214
<=> mem(sF4,sF9) ),
introduced(definition,[new_symbols(definition,[spl24_214])],[avatar_definition]) ).
fof(f4402,plain,
( ~ mem(sF4,sF9)
| spl24_214 ),
inference(avatar_component_clause,[],[f4401]) ).
fof(f4403,plain,
( mem(sF4,sF9)
| ~ spl24_214 ),
inference(avatar_component_clause,[],[f4401]) ).
fof(f4416,definition,
( spl24_216
<=> mem(sF4,sF3) ),
introduced(definition,[new_symbols(definition,[spl24_216])],[avatar_definition]) ).
fof(f4417,plain,
( ~ mem(sF4,sF3)
| spl24_216 ),
inference(avatar_component_clause,[],[f4416]) ).
fof(f4418,plain,
( mem(sF4,sF3)
| ~ spl24_216 ),
inference(avatar_component_clause,[],[f4416]) ).
fof(f4427,plain,
( mem(e,sF4)
| ~ spl24_212 ),
inference(superposition,[],[f342,f4394]) ).
fof(f4435,plain,
( $false
| spl24_56
| ~ spl24_212 ),
inference(forward_subsumption_resolution,[],[f4427,f1026]) ).
fof(f4436,plain,
( spl24_56
| ~ spl24_212 ),
inference(avatar_contradiction_clause,[],[f4435]) ).
fof(f4496,plain,
! [X0] :
( mem(sF7,X0)
| sF7 = sK0(sF8,X0) ),
inference(resolution,[],[f398,f274]) ).
fof(f4626,definition,
( spl24_225
<=> mem(sF3,sF5) ),
introduced(definition,[new_symbols(definition,[spl24_225])],[avatar_definition]) ).
fof(f4627,plain,
( ~ mem(sF3,sF5)
| spl24_225 ),
inference(avatar_component_clause,[],[f4626]) ).
fof(f4628,plain,
( mem(sF3,sF5)
| ~ spl24_225 ),
inference(avatar_component_clause,[],[f4626]) ).
fof(f4681,definition,
( spl24_237
<=> sF3 = sF9 ),
introduced(definition,[new_symbols(definition,[spl24_237])],[avatar_definition]) ).
fof(f4682,plain,
( sF3 != sF9
| spl24_237 ),
inference(avatar_component_clause,[],[f4681]) ).
fof(f4683,plain,
( sF3 = sF9
| ~ spl24_237 ),
inference(avatar_component_clause,[],[f4681]) ).
fof(f4691,definition,
( spl24_239
<=> sF3 = sF7 ),
introduced(definition,[new_symbols(definition,[spl24_239])],[avatar_definition]) ).
fof(f4692,plain,
( sF3 != sF7
| spl24_239 ),
inference(avatar_component_clause,[],[f4691]) ).
fof(f4693,plain,
( sF3 = sF7
| ~ spl24_239 ),
inference(avatar_component_clause,[],[f4691]) ).
fof(f4703,definition,
( spl24_241
<=> e = sF3 ),
introduced(definition,[new_symbols(definition,[spl24_241])],[avatar_definition]) ).
fof(f4704,plain,
( e != sF3
| spl24_241 ),
inference(avatar_component_clause,[],[f4703]) ).
fof(f4705,plain,
( e = sF3
| ~ spl24_241 ),
inference(avatar_component_clause,[],[f4703]) ).
fof(f4730,plain,
( mem(sF3,sF17)
| ~ spl24_241 ),
inference(superposition,[],[f417,f4705]) ).
fof(f4748,plain,
( $false
| spl24_25
| ~ spl24_241 ),
inference(forward_subsumption_resolution,[],[f4730,f646]) ).
fof(f4749,plain,
( spl24_25
| ~ spl24_241 ),
inference(avatar_contradiction_clause,[],[f4748]) ).
fof(f4760,plain,
( mem(sF4,sF3)
| ~ spl24_239 ),
inference(superposition,[],[f339,f4693]) ).
fof(f4779,plain,
( spl24_216
| ~ spl24_239 ),
inference(avatar_split_clause,[],[f4760,f4691,f4416]) ).
fof(f4829,plain,
( subq(sF4,sF3)
| ~ spl24_130
| ~ spl24_237 ),
inference(superposition,[],[f2346,f4683]) ).
fof(f4830,plain,
( $false
| spl24_29
| ~ spl24_130
| ~ spl24_237 ),
inference(forward_subsumption_resolution,[],[f4829,f683]) ).
fof(f4831,plain,
( spl24_29
| ~ spl24_130
| ~ spl24_237 ),
inference(avatar_contradiction_clause,[],[f4830]) ).
fof(f4836,plain,
( sF3 = sF4
| ~ spl24_225 ),
inference(resolution,[],[f4628,f163]) ).
fof(f4839,plain,
( $false
| spl24_30
| ~ spl24_225 ),
inference(forward_subsumption_resolution,[],[f4836,f686]) ).
fof(f4840,plain,
( spl24_30
| ~ spl24_225 ),
inference(avatar_contradiction_clause,[],[f4839]) ).
fof(f4874,definition,
( spl24_244
<=> mem(sF7,sF17) ),
introduced(definition,[new_symbols(definition,[spl24_244])],[avatar_definition]) ).
fof(f4875,plain,
( mem(sF7,sF17)
| ~ spl24_244 ),
inference(avatar_component_clause,[],[f4874]) ).
fof(f4876,plain,
( ~ mem(sF7,sF17)
| spl24_244 ),
inference(avatar_component_clause,[],[f4874]) ).
fof(f4888,definition,
( spl24_246
<=> mem(sF9,sF17) ),
introduced(definition,[new_symbols(definition,[spl24_246])],[avatar_definition]) ).
fof(f4889,plain,
( mem(sF9,sF17)
| ~ spl24_246 ),
inference(avatar_component_clause,[],[f4888]) ).
fof(f4890,plain,
( ~ mem(sF9,sF17)
| spl24_246 ),
inference(avatar_component_clause,[],[f4888]) ).
fof(f4931,plain,
subq(sF3,sF9),
inference(superposition,[],[f2051,f82]) ).
fof(f4932,plain,
subq(sF3,sF7),
inference(superposition,[],[f2051,f78]) ).
fof(f4933,plain,
subq(sF4,sF6),
inference(superposition,[],[f2051,f76]) ).
fof(f4934,plain,
subq(sF5,sF21),
inference(superposition,[],[f2051,f106]) ).
fof(f4956,plain,
( sF4 = sF6
| ~ subq(sF6,sF4) ),
inference(resolution,[],[f4933,f47]) ).
fof(f4958,definition,
( spl24_249
<=> subq(sF6,sF4) ),
introduced(definition,[new_symbols(definition,[spl24_249])],[avatar_definition]) ).
fof(f4960,plain,
( ~ subq(sF6,sF4)
| spl24_249 ),
inference(avatar_component_clause,[],[f4958]) ).
fof(f4961,plain,
( ~ spl24_249
| spl24_206 ),
inference(avatar_split_clause,[],[f4956,f4359,f4958]) ).
fof(f4963,plain,
( sF3 = sF9
| ~ subq(sF9,sF3) ),
inference(resolution,[],[f4931,f47]) ).
fof(f4964,plain,
( ~ subq(sF9,sF3)
| spl24_237 ),
inference(forward_subsumption_resolution,[],[f4963,f4682]) ).
fof(f5180,definition,
( spl24_266
<=> sF9 = sF21 ),
introduced(definition,[new_symbols(definition,[spl24_266])],[avatar_definition]) ).
fof(f5181,plain,
( sF9 != sF21
| spl24_266 ),
inference(avatar_component_clause,[],[f5180]) ).
fof(f5182,plain,
( sF9 = sF21
| ~ spl24_266 ),
inference(avatar_component_clause,[],[f5180]) ).
fof(f5190,definition,
( spl24_268
<=> mem(sF9,sF18) ),
introduced(definition,[new_symbols(definition,[spl24_268])],[avatar_definition]) ).
fof(f5191,plain,
( ~ mem(sF9,sF18)
| spl24_268 ),
inference(avatar_component_clause,[],[f5190]) ).
fof(f5192,plain,
( mem(sF9,sF18)
| ~ spl24_268 ),
inference(avatar_component_clause,[],[f5190]) ).
fof(f5194,definition,
( spl24_269
<=> mem(sF9,sF19) ),
introduced(definition,[new_symbols(definition,[spl24_269])],[avatar_definition]) ).
fof(f5195,plain,
( ~ mem(sF9,sF19)
| spl24_269 ),
inference(avatar_component_clause,[],[f5194]) ).
fof(f5196,plain,
( mem(sF9,sF19)
| ~ spl24_269 ),
inference(avatar_component_clause,[],[f5194]) ).
fof(f5204,definition,
( spl24_271
<=> sF6 = sF9 ),
introduced(definition,[new_symbols(definition,[spl24_271])],[avatar_definition]) ).
fof(f5205,plain,
( sF6 != sF9
| spl24_271 ),
inference(avatar_component_clause,[],[f5204]) ).
fof(f5206,plain,
( sF6 = sF9
| ~ spl24_271 ),
inference(avatar_component_clause,[],[f5204]) ).
fof(f5214,definition,
( spl24_273
<=> subq(sF9,sF17) ),
introduced(definition,[new_symbols(definition,[spl24_273])],[avatar_definition]) ).
fof(f5215,plain,
( ~ subq(sF9,sF17)
| spl24_273 ),
inference(avatar_component_clause,[],[f5214]) ).
fof(f5216,plain,
( subq(sF9,sF17)
| ~ spl24_273 ),
inference(avatar_component_clause,[],[f5214]) ).
fof(f5354,plain,
( mem(sF3,sF17)
| ~ spl24_208 ),
inference(resolution,[],[f4371,f385]) ).
fof(f5367,plain,
( $false
| spl24_25
| ~ spl24_208 ),
inference(forward_subsumption_resolution,[],[f5354,f646]) ).
fof(f5368,plain,
( spl24_25
| ~ spl24_208 ),
inference(avatar_contradiction_clause,[],[f5367]) ).
fof(f5614,definition,
( spl24_327
<=> mem(sF4,sF10) ),
introduced(definition,[new_symbols(definition,[spl24_327])],[avatar_definition]) ).
fof(f5615,plain,
( ~ mem(sF4,sF10)
| spl24_327 ),
inference(avatar_component_clause,[],[f5614]) ).
fof(f5616,plain,
( mem(sF4,sF10)
| ~ spl24_327 ),
inference(avatar_component_clause,[],[f5614]) ).
fof(f5668,plain,
( mem(sF4,sF10)
| mem(sF4,sF9)
| ~ spl24_190 ),
inference(resolution,[],[f4109,f209]) ).
fof(f5673,plain,
( spl24_214
| spl24_327
| ~ spl24_190 ),
inference(avatar_split_clause,[],[f5668,f4107,f5614,f4401]) ).
fof(f5738,plain,
( sF4 = sF9
| ~ spl24_327 ),
inference(resolution,[],[f5616,f166]) ).
fof(f5742,plain,
( $false
| spl24_131
| ~ spl24_327 ),
inference(forward_subsumption_resolution,[],[f5738,f2350]) ).
fof(f5743,plain,
( spl24_131
| ~ spl24_327 ),
inference(avatar_contradiction_clause,[],[f5742]) ).
fof(f5972,plain,
( mem(sF4,sF4)
| ~ spl24_89 ),
inference(resolution,[],[f1929,f391]) ).
fof(f5984,plain,
( $false
| ~ spl24_89
| spl24_90 ),
inference(forward_subsumption_resolution,[],[f5972,f1933]) ).
fof(f5985,plain,
( ~ spl24_89
| spl24_90 ),
inference(avatar_contradiction_clause,[],[f5984]) ).
fof(f6059,plain,
( mem(sF4,sF4)
| mem(sF4,sF3)
| ~ spl24_214 ),
inference(resolution,[],[f4403,f204]) ).
fof(f6061,plain,
( mem(sF4,sF3)
| spl24_90
| ~ spl24_214 ),
inference(forward_subsumption_resolution,[],[f6059,f1933]) ).
fof(f6062,plain,
( spl24_216
| spl24_90
| ~ spl24_214 ),
inference(avatar_split_clause,[],[f6061,f4401,f1931,f4416]) ).
fof(f6063,plain,
( e = sF4
| ~ spl24_28
| ~ spl24_216 ),
inference(resolution,[],[f4418,f2685]) ).
fof(f6069,plain,
( spl24_60
| ~ spl24_28
| ~ spl24_216 ),
inference(avatar_split_clause,[],[f6063,f4416,f673,f1043]) ).
fof(f6070,plain,
( ! [X0] : ~ mem(X0,sF4)
| ~ spl24_60 ),
inference(superposition,[],[f50,f1045]) ).
fof(f6121,plain,
( $false
| ~ spl24_60 ),
inference(resolution,[],[f6070,f113]) ).
fof(f6126,plain,
~ spl24_60,
inference(avatar_contradiction_clause,[],[f6121]) ).
fof(f6129,plain,
( $false
| ~ spl24_39
| spl24_60 ),
inference(forward_subsumption_resolution,[],[f2985,f1044]) ).
fof(f6130,plain,
( ~ spl24_39
| spl24_60 ),
inference(avatar_contradiction_clause,[],[f6129]) ).
fof(f6147,plain,
( subq(sF3,sF4)
| ~ spl24_131 ),
inference(superposition,[],[f4931,f2351]) ).
fof(f6151,plain,
( $false
| spl24_75
| ~ spl24_131 ),
inference(forward_subsumption_resolution,[],[f6147,f1574]) ).
fof(f6152,plain,
( spl24_75
| ~ spl24_131 ),
inference(avatar_contradiction_clause,[],[f6151]) ).
fof(f6160,plain,
( e = sF3
| ~ spl24_56 ),
inference(resolution,[],[f1027,f162]) ).
fof(f6165,plain,
( $false
| ~ spl24_56
| spl24_241 ),
inference(forward_subsumption_resolution,[],[f6160,f4704]) ).
fof(f6166,plain,
( ~ spl24_56
| spl24_241 ),
inference(avatar_contradiction_clause,[],[f6165]) ).
fof(f6197,plain,
( subq(sF9,sF4)
| ~ spl24_246 ),
inference(resolution,[],[f4889,f147]) ).
fof(f6199,plain,
( $false
| ~ spl24_130
| spl24_131
| ~ spl24_246 ),
inference(forward_subsumption_resolution,[],[f6197,f3937]) ).
fof(f6200,plain,
( ~ spl24_130
| spl24_131
| ~ spl24_246 ),
inference(avatar_contradiction_clause,[],[f6199]) ).
fof(f6209,plain,
( subq(sF4,sF17)
| ~ spl24_203 ),
inference(resolution,[],[f4347,f148]) ).
fof(f6212,plain,
( $false
| ~ spl24_203
| spl24_208 ),
inference(forward_subsumption_resolution,[],[f6209,f4370]) ).
fof(f6213,plain,
( ~ spl24_203
| spl24_208 ),
inference(avatar_contradiction_clause,[],[f6212]) ).
fof(f6422,plain,
( mem(sF3,sF17)
| ~ spl24_75 ),
inference(resolution,[],[f1575,f219]) ).
fof(f6424,plain,
( $false
| spl24_25
| ~ spl24_75 ),
inference(forward_subsumption_resolution,[],[f6422,f646]) ).
fof(f6425,plain,
( spl24_25
| ~ spl24_75 ),
inference(avatar_contradiction_clause,[],[f6424]) ).
fof(f6505,definition,
( spl24_354
<=> mem(sF6,sF8) ),
introduced(definition,[new_symbols(definition,[spl24_354])],[avatar_definition]) ).
fof(f6506,plain,
( ~ mem(sF6,sF8)
| spl24_354 ),
inference(avatar_component_clause,[],[f6505]) ).
fof(f6507,plain,
( mem(sF6,sF8)
| ~ spl24_354 ),
inference(avatar_component_clause,[],[f6505]) ).
fof(f6561,definition,
( spl24_366
<=> subq(sF6,sF11) ),
introduced(definition,[new_symbols(definition,[spl24_366])],[avatar_definition]) ).
fof(f6562,plain,
( ~ subq(sF6,sF11)
| spl24_366 ),
inference(avatar_component_clause,[],[f6561]) ).
fof(f6761,plain,
( sF6 = sF7
| ~ spl24_354 ),
inference(resolution,[],[f6507,f165]) ).
fof(f6765,plain,
( spl24_162
| ~ spl24_354 ),
inference(avatar_split_clause,[],[f6761,f6505,f3623]) ).
fof(f6905,definition,
( spl24_386
<=> subq(sF3,sF6) ),
introduced(definition,[new_symbols(definition,[spl24_386])],[avatar_definition]) ).
fof(f6906,plain,
( ~ subq(sF3,sF6)
| spl24_386 ),
inference(avatar_component_clause,[],[f6905]) ).
fof(f6913,plain,
! [X0,X1] :
( subq(m(X0,X1),X0)
| subq(m(X0,X1),X0) ),
inference(resolution,[],[f225,f46]) ).
fof(f6921,plain,
! [X2,X3,X0,X1] :
( mem(sK0(m(X0,X1),X2),X3)
| subq(m(X0,X1),X2)
| ~ subq(X0,X3) ),
inference(resolution,[],[f225,f44]) ).
fof(f6923,plain,
! [X2,X0,X1] :
( subq(m(s(X0),X1),X2)
| sK0(m(s(X0),X1),X2) = X0 ),
inference(resolution,[],[f225,f51]) ).
fof(f6981,plain,
! [X0,X1] : subq(m(X0,X1),X0),
inference(duplicate_literal_removal,[],[f6913]) ).
fof(f6988,plain,
! [X0,X1] :
( ~ subq(X0,m(X0,X1))
| m(X0,X1) = X0 ),
inference(resolution,[],[f6981,f47]) ).
fof(f6993,plain,
subq(sF15,sF12),
inference(superposition,[],[f6981,f94]) ).
fof(f7133,plain,
! [X0] :
( mem(sK0(sF4,X0),sF7)
| subq(sF4,X0) ),
inference(resolution,[],[f229,f172]) ).
fof(f7142,plain,
( subq(sF4,sF7)
| subq(sF4,sF7) ),
inference(resolution,[],[f7133,f46]) ).
fof(f7153,plain,
subq(sF4,sF7),
inference(duplicate_literal_removal,[],[f7142]) ).
fof(f7155,plain,
( sF4 = sF7
| ~ subq(sF7,sF4) ),
inference(resolution,[],[f7153,f47]) ).
fof(f7156,plain,
( ~ subq(sF7,sF4)
| spl24_212 ),
inference(forward_subsumption_resolution,[],[f7155,f4393]) ).
fof(f8300,plain,
! [X0,X1] :
( sK0(s(X0),m(s(X0),X1)) = X0
| s(X0) = m(s(X0),X1) ),
inference(resolution,[],[f1437,f6981]) ).
fof(f9022,plain,
! [X0,X1] :
( mem(sK1(sF16,X0),X1)
| disj(sF16,X0)
| ~ subq(sF15,X1)
| sF7 = sK1(sF16,X0) ),
inference(resolution,[],[f421,f165]) ).
fof(f9154,plain,
( sF7 = sK0(sF8,sF22)
| sF7 = sF21 ),
inference(superposition,[],[f1639,f80]) ).
fof(f9161,definition,
( spl24_494
<=> sF7 = sF21 ),
introduced(definition,[new_symbols(definition,[spl24_494])],[avatar_definition]) ).
fof(f9162,plain,
( sF7 != sF21
| spl24_494 ),
inference(avatar_component_clause,[],[f9161]) ).
fof(f9163,plain,
( sF7 = sF21
| ~ spl24_494 ),
inference(avatar_component_clause,[],[f9161]) ).
fof(f9165,definition,
( spl24_495
<=> sF7 = sK0(sF8,sF22) ),
introduced(definition,[new_symbols(definition,[spl24_495])],[avatar_definition]) ).
fof(f9167,plain,
( sF7 = sK0(sF8,sF22)
| ~ spl24_495 ),
inference(avatar_component_clause,[],[f9165]) ).
fof(f9168,plain,
( spl24_494
| spl24_495 ),
inference(avatar_split_clause,[],[f9154,f9165,f9161]) ).
fof(f9278,plain,
( ~ mem(sF7,sF22)
| subq(sF8,sF22)
| ~ spl24_495 ),
inference(superposition,[],[f46,f9167]) ).
fof(f9280,definition,
( spl24_499
<=> subq(sF8,sF22) ),
introduced(definition,[new_symbols(definition,[spl24_499])],[avatar_definition]) ).
fof(f9282,plain,
( subq(sF8,sF22)
| ~ spl24_499 ),
inference(avatar_component_clause,[],[f9280]) ).
fof(f9284,definition,
( spl24_500
<=> mem(sF7,sF22) ),
introduced(definition,[new_symbols(definition,[spl24_500])],[avatar_definition]) ).
fof(f9286,plain,
( ~ mem(sF7,sF22)
| spl24_500 ),
inference(avatar_component_clause,[],[f9284]) ).
fof(f9287,plain,
( spl24_499
| ~ spl24_500
| ~ spl24_495 ),
inference(avatar_split_clause,[],[f9278,f9165,f9284,f9280]) ).
fof(f9475,plain,
( mem(sF7,sF17)
| ~ spl24_55 ),
inference(superposition,[],[f417,f1022]) ).
fof(f9513,plain,
( $false
| ~ spl24_55
| spl24_244 ),
inference(forward_subsumption_resolution,[],[f9475,f4876]) ).
fof(f9514,plain,
( ~ spl24_55
| spl24_244 ),
inference(avatar_contradiction_clause,[],[f9513]) ).
fof(f9533,plain,
( subq(sF7,sF11)
| ~ spl24_101 ),
inference(resolution,[],[f2100,f146]) ).
fof(f9539,plain,
( subq(sF7,sF4)
| ~ spl24_244 ),
inference(resolution,[],[f4875,f147]) ).
fof(f9614,plain,
( $false
| spl24_212
| ~ spl24_244 ),
inference(forward_subsumption_resolution,[],[f9539,f7156]) ).
fof(f9615,plain,
( spl24_212
| ~ spl24_244 ),
inference(avatar_contradiction_clause,[],[f9614]) ).
fof(f9629,plain,
( mem(sF4,sF11)
| ~ spl24_101 ),
inference(resolution,[],[f9533,f393]) ).
fof(f9634,plain,
( $false
| ~ spl24_101
| spl24_190 ),
inference(forward_subsumption_resolution,[],[f9629,f4108]) ).
fof(f9635,plain,
( ~ spl24_101
| spl24_190 ),
inference(avatar_contradiction_clause,[],[f9634]) ).
fof(f9640,plain,
( mem(sF7,sF12)
| ~ spl24_6 ),
inference(resolution,[],[f481,f399]) ).
fof(f9651,plain,
( $false
| ~ spl24_6
| spl24_101 ),
inference(forward_subsumption_resolution,[],[f9640,f2101]) ).
fof(f9652,plain,
( ~ spl24_6
| spl24_101 ),
inference(avatar_contradiction_clause,[],[f9651]) ).
fof(f10206,plain,
! [X0,X1] :
( mem(sK0(u(X0,X1),X0),X1)
| subq(u(X0,X1),X0)
| subq(u(X0,X1),X0) ),
inference(resolution,[],[f224,f46]) ).
fof(f10314,plain,
! [X0,X1] :
( mem(sK0(u(X0,X1),X0),X1)
| subq(u(X0,X1),X0) ),
inference(duplicate_literal_removal,[],[f10206]) ).
fof(f10538,plain,
! [X0,X1] :
( sK0(m(s(X0),X1),e) = X0
| e = m(s(X0),X1) ),
inference(resolution,[],[f6923,f414]) ).
fof(f11752,definition,
( spl24_648
<=> subq(sF8,sF23) ),
introduced(definition,[new_symbols(definition,[spl24_648])],[avatar_definition]) ).
fof(f11753,plain,
( subq(sF8,sF23)
| ~ spl24_648 ),
inference(avatar_component_clause,[],[f11752]) ).
fof(f11754,plain,
( ~ subq(sF8,sF23)
| spl24_648 ),
inference(avatar_component_clause,[],[f11752]) ).
fof(f11790,definition,
( spl24_657
<=> subq(sF8,sF19) ),
introduced(definition,[new_symbols(definition,[spl24_657])],[avatar_definition]) ).
fof(f11791,plain,
( subq(sF8,sF19)
| ~ spl24_657 ),
inference(avatar_component_clause,[],[f11790]) ).
fof(f11792,plain,
( ~ subq(sF8,sF19)
| spl24_657 ),
inference(avatar_component_clause,[],[f11790]) ).
fof(f11806,definition,
( spl24_661
<=> subq(sF8,sF18) ),
introduced(definition,[new_symbols(definition,[spl24_661])],[avatar_definition]) ).
fof(f11807,plain,
( subq(sF8,sF18)
| ~ spl24_661 ),
inference(avatar_component_clause,[],[f11806]) ).
fof(f11808,plain,
( ~ subq(sF8,sF18)
| spl24_661 ),
inference(avatar_component_clause,[],[f11806]) ).
fof(f12050,plain,
( mem(sF4,sF9)
| ~ spl24_266 ),
inference(superposition,[],[f332,f5182]) ).
fof(f12079,plain,
( $false
| spl24_214
| ~ spl24_266 ),
inference(forward_subsumption_resolution,[],[f12050,f4402]) ).
fof(f12080,plain,
( spl24_214
| ~ spl24_266 ),
inference(avatar_contradiction_clause,[],[f12079]) ).
fof(f12236,plain,
( sF7 = sK0(sF8,sF19)
| sF6 = sF7 ),
inference(superposition,[],[f1634,f80]) ).
fof(f12243,plain,
( sF7 = sK0(sF8,sF19)
| spl24_162 ),
inference(forward_subsumption_resolution,[],[f12236,f3624]) ).
fof(f12542,plain,
( ~ mem(sF7,sF19)
| subq(sF8,sF19)
| spl24_162 ),
inference(superposition,[],[f46,f12243]) ).
fof(f12543,plain,
( ~ mem(sF7,sF19)
| spl24_162
| spl24_657 ),
inference(forward_subsumption_resolution,[],[f12542,f11792]) ).
fof(f13205,plain,
! [X0] :
( subq(u(X0,X0),X0)
| subq(u(X0,X0),X0) ),
inference(resolution,[],[f10314,f46]) ).
fof(f13301,plain,
! [X0] : subq(u(X0,X0),X0),
inference(duplicate_literal_removal,[],[f13205]) ).
fof(f13318,plain,
! [X0] :
( u(X0,X0) = X0
| ~ subq(X0,u(X0,X0)) ),
inference(resolution,[],[f13301,f47]) ).
fof(f13370,plain,
! [X0] : u(X0,X0) = X0,
inference(forward_subsumption_resolution,[],[f13318,f1481]) ).
fof(f14003,definition,
( spl24_753
<=> subq(sF21,sF11) ),
introduced(definition,[new_symbols(definition,[spl24_753])],[avatar_definition]) ).
fof(f14004,plain,
( subq(sF21,sF11)
| ~ spl24_753 ),
inference(avatar_component_clause,[],[f14003]) ).
fof(f14005,plain,
( ~ subq(sF21,sF11)
| spl24_753 ),
inference(avatar_component_clause,[],[f14003]) ).
fof(f14024,definition,
( spl24_756
<=> mem(sF7,sF18) ),
introduced(definition,[new_symbols(definition,[spl24_756])],[avatar_definition]) ).
fof(f14025,plain,
( ~ mem(sF7,sF18)
| spl24_756 ),
inference(avatar_component_clause,[],[f14024]) ).
fof(f14842,plain,
( sF7 = sK0(sF8,sF23)
| spl24_648 ),
inference(resolution,[],[f11754,f274]) ).
fof(f15306,plain,
! [X0] :
( subq(X0,sF10)
| ~ subq(X0,sF21)
| mem(sK0(X0,sF10),sF5)
| subq(X0,sF10) ),
inference(resolution,[],[f1303,f46]) ).
fof(f15313,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF5)
| ~ subq(X0,sF21)
| subq(X0,X1)
| sK0(X0,X1) = sF9 ),
inference(resolution,[],[f1303,f166]) ).
fof(f15448,plain,
! [X0] :
( mem(sK0(X0,sF10),sF5)
| ~ subq(X0,sF21)
| subq(X0,sF10) ),
inference(duplicate_literal_removal,[],[f15306]) ).
fof(f16990,plain,
! [X0,X1] :
( ~ mem(X0,X1)
| subq(m(s(X0),X1),e)
| e = m(s(X0),X1) ),
inference(superposition,[],[f226,f10538]) ).
fof(f17019,plain,
! [X0,X1] :
( ~ mem(X0,X1)
| e = m(s(X0),X1) ),
inference(forward_subsumption_resolution,[],[f16990,f414]) ).
fof(f17231,plain,
e = m(s(sF3),sF7),
inference(resolution,[],[f17019,f340]) ).
fof(f17309,plain,
e = m(sF4,sF7),
inference(forward_demodulation,[],[f17231,f72]) ).
fof(f17992,plain,
! [X0] :
( mem(X0,e)
| ~ mem(X0,sF4)
| mem(X0,sF7) ),
inference(superposition,[],[f58,f17309]) ).
fof(f18013,plain,
! [X0] :
( ~ mem(X0,sF4)
| mem(X0,sF7) ),
inference(forward_subsumption_resolution,[],[f17992,f50]) ).
fof(f20369,plain,
( ~ mem(sF7,sF23)
| subq(sF8,sF23)
| spl24_648 ),
inference(superposition,[],[f46,f14842]) ).
fof(f20382,plain,
( ~ mem(sF7,sF23)
| spl24_648 ),
inference(forward_subsumption_resolution,[],[f20369,f11754]) ).
fof(f20581,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF9)
| ~ subq(X0,sF11)
| subq(X0,X1)
| sK0(X0,X1) = sF9 ),
inference(resolution,[],[f1285,f166]) ).
fof(f20887,plain,
! [X0] :
( ~ subq(X0,sF11)
| subq(X0,sF9)
| sF9 = sK0(X0,sF9)
| subq(X0,sF9) ),
inference(resolution,[],[f20581,f46]) ).
fof(f20894,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF3)
| subq(X0,X1)
| sK0(X0,X1) = sF9
| mem(sK0(X0,X1),sF4)
| ~ subq(X0,sF11) ),
inference(resolution,[],[f20581,f204]) ).
fof(f21020,plain,
! [X0] :
( ~ subq(X0,sF11)
| subq(X0,sF9)
| sF9 = sK0(X0,sF9) ),
inference(duplicate_literal_removal,[],[f20887]) ).
fof(f21499,definition,
( spl24_834
<=> subq(sF9,sF7) ),
introduced(definition,[new_symbols(definition,[spl24_834])],[avatar_definition]) ).
fof(f21500,plain,
( ~ subq(sF9,sF7)
| spl24_834 ),
inference(avatar_component_clause,[],[f21499]) ).
fof(f21501,plain,
( subq(sF9,sF7)
| ~ spl24_834 ),
inference(avatar_component_clause,[],[f21499]) ).
fof(f22763,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF4)
| ~ subq(X0,sF6)
| subq(X0,X1)
| sK0(X0,X1) = sF4 ),
inference(resolution,[],[f1276,f163]) ).
fof(f22806,plain,
( mem(e,sF5)
| subq(sF3,sF5)
| ~ subq(sF3,sF6)
| mem(e,sF4)
| ~ spl24_59 ),
inference(superposition,[],[f1276,f1040]) ).
fof(f22978,plain,
( mem(e,sF5)
| ~ subq(sF3,sF6)
| mem(e,sF4)
| ~ spl24_59 ),
inference(forward_subsumption_resolution,[],[f22806,f377]) ).
fof(f23059,plain,
( ~ subq(sF3,sF6)
| mem(e,sF4)
| spl24_39
| ~ spl24_59 ),
inference(forward_subsumption_resolution,[],[f22978,f948]) ).
fof(f23154,plain,
( ~ subq(sF3,sF6)
| spl24_39
| spl24_56
| ~ spl24_59 ),
inference(forward_subsumption_resolution,[],[f23059,f1026]) ).
fof(f23186,plain,
( ~ spl24_386
| spl24_39
| spl24_56
| ~ spl24_59 ),
inference(avatar_split_clause,[],[f23154,f1038,f1025,f947,f6905]) ).
fof(f23195,plain,
! [X0] :
( ~ subq(X0,sF6)
| subq(X0,sF4)
| sF4 = sK0(X0,sF4)
| subq(X0,sF4) ),
inference(resolution,[],[f22763,f46]) ).
fof(f23202,plain,
! [X0,X1] :
( ~ subq(X0,sF6)
| subq(X0,X1)
| sK0(X0,X1) = sF4
| sK0(X0,X1) = sF3 ),
inference(resolution,[],[f22763,f162]) ).
fof(f23350,plain,
! [X0] :
( ~ subq(X0,sF6)
| subq(X0,sF4)
| sF4 = sK0(X0,sF4) ),
inference(duplicate_literal_removal,[],[f23195]) ).
fof(f23362,plain,
! [X0] :
( subq(sF6,X0)
| sF4 = sK0(sF6,X0)
| sF3 = sK0(sF6,X0) ),
inference(resolution,[],[f23202,f240]) ).
fof(f23546,plain,
( sF4 = sK0(sF6,sF4)
| sF3 = sK0(sF6,sF4)
| spl24_249 ),
inference(resolution,[],[f23362,f4960]) ).
fof(f23600,definition,
( spl24_873
<=> sF3 = sK0(sF6,sF4) ),
introduced(definition,[new_symbols(definition,[spl24_873])],[avatar_definition]) ).
fof(f23602,plain,
( sF3 = sK0(sF6,sF4)
| ~ spl24_873 ),
inference(avatar_component_clause,[],[f23600]) ).
fof(f23604,definition,
( spl24_874
<=> sF4 = sK0(sF6,sF4) ),
introduced(definition,[new_symbols(definition,[spl24_874])],[avatar_definition]) ).
fof(f23606,plain,
( sF4 = sK0(sF6,sF4)
| ~ spl24_874 ),
inference(avatar_component_clause,[],[f23604]) ).
fof(f23631,plain,
( spl24_873
| spl24_874
| spl24_249 ),
inference(avatar_split_clause,[],[f23546,f4958,f23604,f23600]) ).
fof(f23824,plain,
( mem(sF4,sF3)
| subq(sF6,sF4)
| sF4 = sF9
| mem(sF4,sF4)
| ~ subq(sF6,sF11)
| ~ spl24_874 ),
inference(superposition,[],[f20894,f23606]) ).
fof(f23829,plain,
( mem(sF4,sF3)
| sF4 = sF9
| mem(sF4,sF4)
| ~ subq(sF6,sF11)
| ~ spl24_874 ),
inference(forward_subsumption_resolution,[],[f23824,f392]) ).
fof(f23835,plain,
( sF4 = sF9
| mem(sF4,sF4)
| ~ subq(sF6,sF11)
| spl24_216
| ~ spl24_874 ),
inference(forward_subsumption_resolution,[],[f23829,f4417]) ).
fof(f23841,plain,
( mem(sF4,sF4)
| ~ subq(sF6,sF11)
| spl24_131
| spl24_216
| ~ spl24_874 ),
inference(forward_subsumption_resolution,[],[f23835,f2350]) ).
fof(f23845,plain,
( ~ subq(sF6,sF11)
| spl24_90
| spl24_131
| spl24_216
| ~ spl24_874 ),
inference(forward_subsumption_resolution,[],[f23841,f1933]) ).
fof(f23848,plain,
( ~ spl24_366
| spl24_90
| spl24_131
| spl24_216
| ~ spl24_874 ),
inference(avatar_split_clause,[],[f23845,f23604,f4416,f2349,f1931,f6561]) ).
fof(f25076,plain,
! [X0] :
( subq(X0,sF3)
| mem(sK0(X0,sF3),sF4)
| ~ subq(X0,sF9)
| subq(X0,sF3) ),
inference(resolution,[],[f1281,f46]) ).
fof(f25082,plain,
! [X0,X1] :
( subq(X0,X1)
| mem(sK0(X0,X1),sF4)
| ~ subq(X0,sF9)
| mem(sK0(X0,X1),sF7) ),
inference(resolution,[],[f1281,f171]) ).
fof(f25248,plain,
! [X0] :
( mem(sK0(X0,sF3),sF4)
| subq(X0,sF3)
| ~ subq(X0,sF9) ),
inference(duplicate_literal_removal,[],[f25076]) ).
fof(f25338,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF7)
| ~ subq(X0,sF9)
| subq(X0,X1) ),
inference(forward_subsumption_resolution,[],[f25082,f18013]) ).
fof(f25536,plain,
! [X0] :
( ~ subq(X0,sF9)
| subq(X0,sF7)
| subq(X0,sF7) ),
inference(resolution,[],[f25338,f46]) ).
fof(f25695,plain,
! [X0] :
( ~ subq(X0,sF9)
| subq(X0,sF7) ),
inference(duplicate_literal_removal,[],[f25536]) ).
fof(f25880,plain,
subq(u(sF9,sF9),sF7),
inference(resolution,[],[f25695,f13301]) ).
fof(f25901,plain,
subq(sF9,sF7),
inference(forward_demodulation,[],[f25880,f13370]) ).
fof(f26362,definition,
( spl24_910
<=> subq(sF9,sF21) ),
introduced(definition,[new_symbols(definition,[spl24_910])],[avatar_definition]) ).
fof(f26364,plain,
( ~ subq(sF9,sF21)
| spl24_910 ),
inference(avatar_component_clause,[],[f26362]) ).
fof(f27452,plain,
( ~ subq(sF8,sF18)
| subq(sK0(sF16,sF12),sF17)
| ~ spl24_5 ),
inference(resolution,[],[f1916,f148]) ).
fof(f27457,plain,
( ~ subq(sF8,sF19)
| sF6 = sK0(sF16,sF12)
| ~ spl24_5 ),
inference(resolution,[],[f1916,f164]) ).
fof(f27464,plain,
( ~ subq(sF8,sF22)
| sF21 = sK0(sF16,sF12)
| ~ spl24_5 ),
inference(resolution,[],[f1916,f168]) ).
fof(f27466,plain,
( ~ subq(sF8,sF23)
| mem(sK0(sF16,sF12),sF22)
| mem(sK0(sF16,sF12),sF20)
| ~ spl24_5 ),
inference(resolution,[],[f1916,f212]) ).
fof(f30105,plain,
( subq(sF6,sF4)
| sF4 = sK0(sF6,sF4) ),
inference(resolution,[],[f23350,f240]) ).
fof(f30614,definition,
( spl24_978
<=> sF4 = sK0(sF21,sF10) ),
introduced(definition,[new_symbols(definition,[spl24_978])],[avatar_definition]) ).
fof(f30615,plain,
( sF4 != sK0(sF21,sF10)
| spl24_978 ),
inference(avatar_component_clause,[],[f30614]) ).
fof(f30616,plain,
( sF4 = sK0(sF21,sF10)
| ~ spl24_978 ),
inference(avatar_component_clause,[],[f30614]) ).
fof(f30965,plain,
( mem(sF4,sF3)
| subq(sF21,sF10)
| sF4 = sF9
| mem(sF4,sF4)
| ~ subq(sF21,sF11)
| ~ spl24_978 ),
inference(superposition,[],[f20894,f30616]) ).
fof(f32232,plain,
! [X0,X1] :
( mem(sK1(X0,X1),sF20)
| ~ subq(X1,sF23)
| disj(X0,X1)
| sK1(X0,X1) = sF21 ),
inference(resolution,[],[f822,f168]) ).
fof(f32251,plain,
! [X0,X1] :
( mem(sK1(X1,X0),sF19)
| disj(X1,X0)
| sF21 = sK1(X1,X0)
| ~ subq(X0,sF23)
| mem(sK1(X1,X0),sF18) ),
inference(resolution,[],[f32232,f211]) ).
fof(f32271,plain,
! [X0,X1] :
( mem(sK1(X0,X1),sF18)
| sK1(X0,X1) = sF21
| ~ subq(X1,sF23)
| disj(X0,X1)
| sK1(X0,X1) = sF6 ),
inference(resolution,[],[f32251,f164]) ).
fof(f32290,plain,
! [X0,X1] :
( subq(sK1(X0,X1),sF17)
| ~ subq(X1,sF23)
| disj(X0,X1)
| sK1(X0,X1) = sF6
| sK1(X0,X1) = sF21 ),
inference(resolution,[],[f32271,f148]) ).
fof(f33763,plain,
! [X0] :
( ~ subq(X0,sF21)
| subq(X0,sF10)
| sF4 = sK0(X0,sF10) ),
inference(resolution,[],[f15448,f163]) ).
fof(f33789,plain,
( subq(sF21,sF10)
| sF4 = sK0(sF21,sF10) ),
inference(resolution,[],[f33763,f240]) ).
fof(f37683,definition,
( spl24_1094
<=> subq(sF7,sF17) ),
introduced(definition,[new_symbols(definition,[spl24_1094])],[avatar_definition]) ).
fof(f37685,plain,
( subq(sF7,sF17)
| ~ spl24_1094 ),
inference(avatar_component_clause,[],[f37683]) ).
fof(f40593,plain,
( mem(sF4,sF10)
| ~ spl24_168 ),
inference(superposition,[],[f332,f3722]) ).
fof(f40720,plain,
( $false
| ~ spl24_168
| spl24_327 ),
inference(forward_subsumption_resolution,[],[f40593,f5615]) ).
fof(f40721,plain,
( ~ spl24_168
| spl24_327 ),
inference(avatar_contradiction_clause,[],[f40720]) ).
fof(f44640,plain,
( subq(sF3,sF6)
| ~ spl24_271 ),
inference(superposition,[],[f4931,f5206]) ).
fof(f44717,plain,
( $false
| ~ spl24_271
| spl24_386 ),
inference(forward_subsumption_resolution,[],[f44640,f6906]) ).
fof(f44718,plain,
( ~ spl24_271
| spl24_386 ),
inference(avatar_contradiction_clause,[],[f44717]) ).
fof(f44784,plain,
( subq(sF9,sF17)
| ~ spl24_268 ),
inference(resolution,[],[f5192,f148]) ).
fof(f44973,plain,
( mem(sF3,sF17)
| ~ spl24_273 ),
inference(resolution,[],[f5216,f388]) ).
fof(f44986,plain,
( $false
| spl24_25
| ~ spl24_273 ),
inference(forward_subsumption_resolution,[],[f44973,f646]) ).
fof(f44987,plain,
( spl24_25
| ~ spl24_273 ),
inference(avatar_contradiction_clause,[],[f44986]) ).
fof(f44989,plain,
( $false
| ~ spl24_268
| spl24_273 ),
inference(forward_subsumption_resolution,[],[f44784,f5215]) ).
fof(f44990,plain,
( ~ spl24_268
| spl24_273 ),
inference(avatar_contradiction_clause,[],[f44989]) ).
fof(f45335,definition,
( spl24_1371
<=> subq(sF6,sF18) ),
introduced(definition,[new_symbols(definition,[spl24_1371])],[avatar_definition]) ).
fof(f45336,plain,
( ~ subq(sF6,sF18)
| spl24_1371 ),
inference(avatar_component_clause,[],[f45335]) ).
fof(f45337,plain,
( subq(sF6,sF18)
| ~ spl24_1371 ),
inference(avatar_component_clause,[],[f45335]) ).
fof(f45501,plain,
( mem(sF4,sF18)
| ~ spl24_1371 ),
inference(resolution,[],[f45337,f392]) ).
fof(f45504,plain,
( $false
| spl24_203
| ~ spl24_1371 ),
inference(forward_subsumption_resolution,[],[f45501,f4346]) ).
fof(f45505,plain,
( spl24_203
| ~ spl24_1371 ),
inference(avatar_contradiction_clause,[],[f45504]) ).
fof(f45642,plain,
( sF4 = sK0(sF6,sF18)
| sF3 = sK0(sF6,sF18)
| spl24_1371 ),
inference(resolution,[],[f45336,f23362]) ).
fof(f45644,definition,
( spl24_1374
<=> sF3 = sK0(sF6,sF18) ),
introduced(definition,[new_symbols(definition,[spl24_1374])],[avatar_definition]) ).
fof(f45646,plain,
( sF3 = sK0(sF6,sF18)
| ~ spl24_1374 ),
inference(avatar_component_clause,[],[f45644]) ).
fof(f45648,definition,
( spl24_1375
<=> sF4 = sK0(sF6,sF18) ),
introduced(definition,[new_symbols(definition,[spl24_1375])],[avatar_definition]) ).
fof(f45650,plain,
( sF4 = sK0(sF6,sF18)
| ~ spl24_1375 ),
inference(avatar_component_clause,[],[f45648]) ).
fof(f45651,plain,
( spl24_1374
| spl24_1375
| spl24_1371 ),
inference(avatar_split_clause,[],[f45642,f45335,f45648,f45644]) ).
fof(f45658,plain,
( mem(sF4,sF3)
| subq(sF6,sF18)
| mem(sF4,sF4)
| ~ subq(sF6,sF9)
| ~ spl24_1375 ),
inference(superposition,[],[f1281,f45650]) ).
fof(f46274,plain,
( sF7 = sK0(sF8,sF18)
| subq(sF7,sF17) ),
inference(resolution,[],[f4496,f148]) ).
fof(f46291,definition,
( spl24_1379
<=> sF7 = sK0(sF8,sF18) ),
introduced(definition,[new_symbols(definition,[spl24_1379])],[avatar_definition]) ).
fof(f46293,plain,
( sF7 = sK0(sF8,sF18)
| ~ spl24_1379 ),
inference(avatar_component_clause,[],[f46291]) ).
fof(f46294,plain,
( spl24_1094
| spl24_1379 ),
inference(avatar_split_clause,[],[f46274,f46291,f37683]) ).
fof(f46311,plain,
( ~ mem(sF7,sF18)
| subq(sF8,sF18)
| ~ spl24_1379 ),
inference(superposition,[],[f46,f46293]) ).
fof(f46362,plain,
( ~ mem(sF7,sF18)
| spl24_661
| ~ spl24_1379 ),
inference(forward_subsumption_resolution,[],[f46311,f11808]) ).
fof(f46363,plain,
( ~ spl24_756
| spl24_661
| ~ spl24_1379 ),
inference(avatar_split_clause,[],[f46362,f46291,f11806,f14024]) ).
fof(f48903,plain,
! [X0] :
( disj(sF16,X0)
| ~ subq(sF15,sF12)
| sF7 = sK1(sF16,X0)
| subq(sK1(sF16,X0),sF11) ),
inference(resolution,[],[f9022,f146]) ).
fof(f48914,plain,
! [X0] :
( disj(sF16,X0)
| ~ subq(sF15,sF15)
| sF7 = sK1(sF16,X0)
| ~ mem(sK1(sF16,X0),sF14) ),
inference(resolution,[],[f9022,f155]) ).
fof(f48941,plain,
! [X0] :
( ~ mem(sK1(sF16,X0),sF14)
| sF7 = sK1(sF16,X0)
| disj(sF16,X0) ),
inference(forward_subsumption_resolution,[],[f48914,f240]) ).
fof(f48944,plain,
! [X0] :
( subq(sK1(sF16,X0),sF11)
| sF7 = sK1(sF16,X0)
| disj(sF16,X0) ),
inference(forward_subsumption_resolution,[],[f48903,f6993]) ).
fof(f52294,plain,
! [X0,X1] :
( mem(X0,X1)
| subq(s(X0),m(s(X0),X1))
| s(X0) = m(s(X0),X1) ),
inference(superposition,[],[f1425,f8300]) ).
fof(f52392,plain,
! [X0,X1] :
( mem(X0,X1)
| s(X0) = m(s(X0),X1) ),
inference(forward_subsumption_resolution,[],[f52294,f6988]) ).
fof(f52625,plain,
( s(sF7) = m(s(sF7),sF23)
| spl24_648 ),
inference(resolution,[],[f52392,f20382]) ).
fof(f52755,plain,
( sF8 = m(sF8,sF23)
| spl24_648 ),
inference(forward_demodulation,[],[f52625,f80]) ).
fof(f53988,plain,
( ! [X0] :
( ~ mem(X0,sF23)
| ~ mem(X0,sF8) )
| spl24_648 ),
inference(superposition,[],[f56,f52755]) ).
fof(f54058,plain,
( ! [X0] :
( ~ mem(sK1(X0,sF23),sF8)
| disj(X0,sF23) )
| spl24_648 ),
inference(resolution,[],[f53988,f48]) ).
fof(f59976,plain,
( ! [X0] :
( disj(sF16,sF23)
| mem(sK1(sF16,sF23),X0)
| disj(sF16,sF23)
| ~ subq(sF15,X0) )
| spl24_648 ),
inference(resolution,[],[f54058,f421]) ).
fof(f59986,plain,
( ! [X0] :
( disj(sF16,sF23)
| mem(sK1(sF16,sF23),X0)
| ~ subq(sF15,X0) )
| spl24_648 ),
inference(duplicate_literal_removal,[],[f59976]) ).
fof(f59996,plain,
( ! [X0] :
( mem(sK1(sF16,sF23),X0)
| ~ subq(sF15,X0) )
| spl24_648 ),
inference(forward_subsumption_resolution,[],[f59986,f111]) ).
fof(f60112,plain,
( ~ subq(sF15,sF12)
| subq(sK1(sF16,sF23),sF11)
| spl24_648 ),
inference(resolution,[],[f59996,f146]) ).
fof(f60204,plain,
( subq(sK1(sF16,sF23),sF11)
| spl24_648 ),
inference(forward_subsumption_resolution,[],[f60112,f6993]) ).
fof(f60222,definition,
( spl24_1494
<=> mem(sK1(sF16,sF23),sF8) ),
introduced(definition,[new_symbols(definition,[spl24_1494])],[avatar_definition]) ).
fof(f60223,plain,
( ~ mem(sK1(sF16,sF23),sF8)
| spl24_1494 ),
inference(avatar_component_clause,[],[f60222]) ).
fof(f60224,plain,
( mem(sK1(sF16,sF23),sF8)
| ~ spl24_1494 ),
inference(avatar_component_clause,[],[f60222]) ).
fof(f60226,definition,
( spl24_1495
<=> mem(sK1(sF16,sF23),sF15) ),
introduced(definition,[new_symbols(definition,[spl24_1495])],[avatar_definition]) ).
fof(f60227,plain,
( ~ mem(sK1(sF16,sF23),sF15)
| spl24_1495 ),
inference(avatar_component_clause,[],[f60226]) ).
fof(f60228,plain,
( mem(sK1(sF16,sF23),sF15)
| ~ spl24_1495 ),
inference(avatar_component_clause,[],[f60226]) ).
fof(f60266,plain,
( mem(sK1(sF16,sF23),sF12)
| ~ spl24_1495 ),
inference(resolution,[],[f60228,f180]) ).
fof(f60275,plain,
( ! [X0] :
( mem(sK1(sF16,sF23),X0)
| disj(sF16,sF23)
| ~ subq(sF15,X0) )
| spl24_1494 ),
inference(resolution,[],[f60223,f421]) ).
fof(f60284,plain,
( subq(sK1(sF16,sF23),sF9)
| sF9 = sK0(sK1(sF16,sF23),sF9)
| spl24_648 ),
inference(resolution,[],[f60204,f21020]) ).
fof(f60300,definition,
( spl24_1498
<=> subq(sK1(sF16,sF23),sF7) ),
introduced(definition,[new_symbols(definition,[spl24_1498])],[avatar_definition]) ).
fof(f60301,plain,
( ~ subq(sK1(sF16,sF23),sF7)
| spl24_1498 ),
inference(avatar_component_clause,[],[f60300]) ).
fof(f60302,plain,
( subq(sK1(sF16,sF23),sF7)
| ~ spl24_1498 ),
inference(avatar_component_clause,[],[f60300]) ).
fof(f60318,definition,
( spl24_1502
<=> sF9 = sK0(sK1(sF16,sF23),sF9) ),
introduced(definition,[new_symbols(definition,[spl24_1502])],[avatar_definition]) ).
fof(f60320,plain,
( sF9 = sK0(sK1(sF16,sF23),sF9)
| ~ spl24_1502 ),
inference(avatar_component_clause,[],[f60318]) ).
fof(f60322,definition,
( spl24_1503
<=> subq(sK1(sF16,sF23),sF9) ),
introduced(definition,[new_symbols(definition,[spl24_1503])],[avatar_definition]) ).
fof(f60324,plain,
( subq(sK1(sF16,sF23),sF9)
| ~ spl24_1503 ),
inference(avatar_component_clause,[],[f60322]) ).
fof(f60325,plain,
( spl24_1502
| spl24_1503
| spl24_648 ),
inference(avatar_split_clause,[],[f60284,f11752,f60322,f60318]) ).
fof(f60329,plain,
( ! [X0] :
( mem(sF9,X0)
| ~ subq(sK1(sF16,sF23),X0)
| subq(sK1(sF16,sF23),sF9) )
| ~ spl24_1502 ),
inference(superposition,[],[f382,f60320]) ).
fof(f60379,definition,
( spl24_1504
<=> ! [X0] :
( mem(sF9,X0)
| ~ subq(sK1(sF16,sF23),X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_1504])],[avatar_definition]) ).
fof(f60380,plain,
( ! [X0] :
( ~ subq(sK1(sF16,sF23),X0)
| mem(sF9,X0) )
| ~ spl24_1504 ),
inference(avatar_component_clause,[],[f60379]) ).
fof(f60381,plain,
( spl24_1503
| spl24_1504
| ~ spl24_1502 ),
inference(avatar_split_clause,[],[f60329,f60318,f60379,f60322]) ).
fof(f60403,definition,
( spl24_1506
<=> subq(sK1(sF16,sF23),sF6) ),
introduced(definition,[new_symbols(definition,[spl24_1506])],[avatar_definition]) ).
fof(f60404,plain,
( subq(sK1(sF16,sF23),sF6)
| ~ spl24_1506 ),
inference(avatar_component_clause,[],[f60403]) ).
fof(f60405,plain,
( ~ subq(sK1(sF16,sF23),sF6)
| spl24_1506 ),
inference(avatar_component_clause,[],[f60403]) ).
fof(f60433,definition,
( spl24_1509
<=> sF7 = sK1(sF16,sF23) ),
introduced(definition,[new_symbols(definition,[spl24_1509])],[avatar_definition]) ).
fof(f60435,plain,
( sF7 = sK1(sF16,sF23)
| ~ spl24_1509 ),
inference(avatar_component_clause,[],[f60433]) ).
fof(f60439,plain,
( subq(sK1(sF16,sF23),sF7)
| ~ spl24_1503 ),
inference(resolution,[],[f60324,f25695]) ).
fof(f60441,plain,
( sF9 = sK1(sF16,sF23)
| ~ subq(sF9,sK1(sF16,sF23))
| ~ spl24_1503 ),
inference(resolution,[],[f60324,f47]) ).
fof(f60443,definition,
( spl24_1510
<=> subq(sF9,sK1(sF16,sF23)) ),
introduced(definition,[new_symbols(definition,[spl24_1510])],[avatar_definition]) ).
fof(f60445,plain,
( ~ subq(sF9,sK1(sF16,sF23))
| spl24_1510 ),
inference(avatar_component_clause,[],[f60443]) ).
fof(f60447,definition,
( spl24_1511
<=> sF9 = sK1(sF16,sF23) ),
introduced(definition,[new_symbols(definition,[spl24_1511])],[avatar_definition]) ).
fof(f60449,plain,
( sF9 = sK1(sF16,sF23)
| ~ spl24_1511 ),
inference(avatar_component_clause,[],[f60447]) ).
fof(f60450,plain,
( ~ spl24_1510
| spl24_1511
| ~ spl24_1503 ),
inference(avatar_split_clause,[],[f60441,f60322,f60447,f60443]) ).
fof(f60917,definition,
( spl24_1514
<=> sF4 = sK1(sF16,sF23) ),
introduced(definition,[new_symbols(definition,[spl24_1514])],[avatar_definition]) ).
fof(f60919,plain,
( sF4 = sK1(sF16,sF23)
| ~ spl24_1514 ),
inference(avatar_component_clause,[],[f60917]) ).
fof(f61005,definition,
( spl24_1531
<=> sF6 = sK1(sF16,sF23) ),
introduced(definition,[new_symbols(definition,[spl24_1531])],[avatar_definition]) ).
fof(f61007,plain,
( sF6 = sK1(sF16,sF23)
| ~ spl24_1531 ),
inference(avatar_component_clause,[],[f61005]) ).
fof(f61495,definition,
( spl24_1547
<=> subq(sK1(sF16,sF23),sF3) ),
introduced(definition,[new_symbols(definition,[spl24_1547])],[avatar_definition]) ).
fof(f61496,plain,
( subq(sK1(sF16,sF23),sF3)
| ~ spl24_1547 ),
inference(avatar_component_clause,[],[f61495]) ).
fof(f61497,plain,
( ~ subq(sK1(sF16,sF23),sF3)
| spl24_1547 ),
inference(avatar_component_clause,[],[f61495]) ).
fof(f70756,plain,
! [X0] :
( ~ subq(X0,sF9)
| subq(X0,sF3)
| sF3 = sK0(X0,sF3) ),
inference(resolution,[],[f25248,f162]) ).
fof(f70790,plain,
( subq(sF9,sF3)
| sF3 = sK0(sF9,sF3) ),
inference(resolution,[],[f70756,f240]) ).
fof(f70803,plain,
( subq(sK1(sF16,sF23),sF3)
| sF3 = sK0(sK1(sF16,sF23),sF3)
| ~ spl24_1503 ),
inference(resolution,[],[f70756,f60324]) ).
fof(f70820,definition,
( spl24_1624
<=> sF3 = sK0(sK1(sF16,sF23),sF3) ),
introduced(definition,[new_symbols(definition,[spl24_1624])],[avatar_definition]) ).
fof(f70822,plain,
( sF3 = sK0(sK1(sF16,sF23),sF3)
| ~ spl24_1624 ),
inference(avatar_component_clause,[],[f70820]) ).
fof(f70823,plain,
( spl24_1624
| spl24_1547
| ~ spl24_1503 ),
inference(avatar_split_clause,[],[f70803,f60322,f61495,f70820]) ).
fof(f70826,plain,
( sF3 = sK0(sF9,sF3)
| spl24_237 ),
inference(forward_subsumption_resolution,[],[f70790,f4964]) ).
fof(f70831,plain,
( sF3 = sK1(sF16,sF23)
| e = sK0(sF3,sK1(sF16,sF23))
| ~ spl24_1547 ),
inference(resolution,[],[f61496,f622]) ).
fof(f70834,plain,
( sF3 = sK1(sF16,sF23)
| ~ subq(sF3,sK1(sF16,sF23))
| ~ spl24_1547 ),
inference(resolution,[],[f61496,f47]) ).
fof(f70836,definition,
( spl24_1625
<=> subq(sF3,sK1(sF16,sF23)) ),
introduced(definition,[new_symbols(definition,[spl24_1625])],[avatar_definition]) ).
fof(f70838,plain,
( ~ subq(sF3,sK1(sF16,sF23))
| spl24_1625 ),
inference(avatar_component_clause,[],[f70836]) ).
fof(f70840,definition,
( spl24_1626
<=> sF3 = sK1(sF16,sF23) ),
introduced(definition,[new_symbols(definition,[spl24_1626])],[avatar_definition]) ).
fof(f70842,plain,
( sF3 = sK1(sF16,sF23)
| ~ spl24_1626 ),
inference(avatar_component_clause,[],[f70840]) ).
fof(f70843,plain,
( ~ spl24_1625
| spl24_1626
| ~ spl24_1547 ),
inference(avatar_split_clause,[],[f70834,f61495,f70840,f70836]) ).
fof(f70845,definition,
( spl24_1627
<=> e = sK0(sF3,sK1(sF16,sF23)) ),
introduced(definition,[new_symbols(definition,[spl24_1627])],[avatar_definition]) ).
fof(f70847,plain,
( e = sK0(sF3,sK1(sF16,sF23))
| ~ spl24_1627 ),
inference(avatar_component_clause,[],[f70845]) ).
fof(f70848,plain,
( spl24_1627
| spl24_1626
| ~ spl24_1547 ),
inference(avatar_split_clause,[],[f70831,f61495,f70840,f70845]) ).
fof(f70851,plain,
( mem(sF3,sK1(sF16,sF23))
| subq(sK1(sF16,sF23),sF3)
| ~ spl24_1624 ),
inference(superposition,[],[f45,f70822]) ).
fof(f70908,plain,
( mem(sF3,sK1(sF16,sF23))
| spl24_1547
| ~ spl24_1624 ),
inference(forward_subsumption_resolution,[],[f70851,f61497]) ).
fof(f70917,plain,
( e = m(s(sF3),sK1(sF16,sF23))
| spl24_1547
| ~ spl24_1624 ),
inference(resolution,[],[f70908,f17019]) ).
fof(f70919,plain,
( e = m(sF4,sK1(sF16,sF23))
| spl24_1547
| ~ spl24_1624 ),
inference(forward_demodulation,[],[f70917,f72]) ).
fof(f70922,plain,
( ! [X0] :
( mem(X0,e)
| ~ mem(X0,sF4)
| mem(X0,sK1(sF16,sF23)) )
| spl24_1547
| ~ spl24_1624 ),
inference(superposition,[],[f58,f70919]) ).
fof(f70946,plain,
( ! [X0] :
( mem(X0,sK1(sF16,sF23))
| ~ mem(X0,sF4) )
| spl24_1547
| ~ spl24_1624 ),
inference(forward_subsumption_resolution,[],[f70922,f50]) ).
fof(f70949,plain,
( ! [X0] :
( ~ mem(sK0(X0,sK1(sF16,sF23)),sF4)
| subq(X0,sK1(sF16,sF23)) )
| spl24_1547
| ~ spl24_1624 ),
inference(resolution,[],[f70946,f46]) ).
fof(f70957,plain,
( subq(sF4,sK1(sF16,sF23))
| subq(sF4,sK1(sF16,sF23))
| spl24_1547
| ~ spl24_1624 ),
inference(resolution,[],[f70949,f45]) ).
fof(f70981,plain,
( subq(sF4,sK1(sF16,sF23))
| spl24_1547
| ~ spl24_1624 ),
inference(duplicate_literal_removal,[],[f70957]) ).
fof(f70987,plain,
( sF4 = sK1(sF16,sF23)
| ~ subq(sK1(sF16,sF23),sF4)
| spl24_1547
| ~ spl24_1624 ),
inference(resolution,[],[f70981,f47]) ).
fof(f70989,definition,
( spl24_1628
<=> subq(sK1(sF16,sF23),sF4) ),
introduced(definition,[new_symbols(definition,[spl24_1628])],[avatar_definition]) ).
fof(f70991,plain,
( ~ subq(sK1(sF16,sF23),sF4)
| spl24_1628 ),
inference(avatar_component_clause,[],[f70989]) ).
fof(f70992,plain,
( ~ spl24_1628
| spl24_1514
| spl24_1547
| ~ spl24_1624 ),
inference(avatar_split_clause,[],[f70987,f70820,f61495,f60917,f70989]) ).
fof(f71146,definition,
( spl24_1631
<=> mem(e,sK1(sF16,sF23)) ),
introduced(definition,[new_symbols(definition,[spl24_1631])],[avatar_definition]) ).
fof(f71147,plain,
( ~ mem(e,sK1(sF16,sF23))
| spl24_1631 ),
inference(avatar_component_clause,[],[f71146]) ).
fof(f71148,plain,
( mem(e,sK1(sF16,sF23))
| ~ spl24_1631 ),
inference(avatar_component_clause,[],[f71146]) ).
fof(f71162,definition,
( spl24_1634
<=> sF21 = sK1(sF16,sF23) ),
introduced(definition,[new_symbols(definition,[spl24_1634])],[avatar_definition]) ).
fof(f71164,plain,
( sF21 = sK1(sF16,sF23)
| ~ spl24_1634 ),
inference(avatar_component_clause,[],[f71162]) ).
fof(f71245,plain,
( mem(sF3,sF5)
| ~ subq(sF9,sF21)
| subq(sF9,sF3)
| sF3 = sF9
| spl24_237 ),
inference(superposition,[],[f15313,f70826]) ).
fof(f71292,plain,
( ~ subq(sF9,sF21)
| subq(sF9,sF3)
| sF3 = sF9
| spl24_225
| spl24_237 ),
inference(forward_subsumption_resolution,[],[f71245,f4627]) ).
fof(f71296,plain,
( ~ subq(sF9,sF21)
| sF3 = sF9
| spl24_225
| spl24_237 ),
inference(forward_subsumption_resolution,[],[f71292,f4964]) ).
fof(f71299,plain,
( ~ subq(sF9,sF21)
| spl24_225
| spl24_237 ),
inference(forward_subsumption_resolution,[],[f71296,f4682]) ).
fof(f71301,plain,
( ~ spl24_910
| spl24_225
| spl24_237 ),
inference(avatar_split_clause,[],[f71299,f4681,f4626,f26362]) ).
fof(f73152,plain,
( ~ mem(sF3,sF14)
| sF3 = sF7
| disj(sF16,sF23)
| ~ spl24_1626 ),
inference(superposition,[],[f48941,f70842]) ).
fof(f73297,plain,
( sF3 = sF7
| disj(sF16,sF23)
| ~ spl24_1626 ),
inference(forward_subsumption_resolution,[],[f73152,f357]) ).
fof(f73355,plain,
( disj(sF16,sF23)
| spl24_239
| ~ spl24_1626 ),
inference(forward_subsumption_resolution,[],[f73297,f4692]) ).
fof(f73373,plain,
( $false
| spl24_239
| ~ spl24_1626 ),
inference(forward_subsumption_resolution,[],[f73355,f111]) ).
fof(f73374,plain,
( spl24_239
| ~ spl24_1626 ),
inference(avatar_contradiction_clause,[],[f73373]) ).
fof(f73399,plain,
( ~ mem(e,sK1(sF16,sF23))
| subq(sF3,sK1(sF16,sF23))
| ~ spl24_1627 ),
inference(superposition,[],[f46,f70847]) ).
fof(f73452,plain,
( ~ mem(e,sK1(sF16,sF23))
| spl24_1625
| ~ spl24_1627 ),
inference(forward_subsumption_resolution,[],[f73399,f70838]) ).
fof(f73453,plain,
( ~ spl24_1631
| spl24_1625
| ~ spl24_1627 ),
inference(avatar_split_clause,[],[f73452,f70845,f70836,f71146]) ).
fof(f78295,plain,
( sF6 = sF9
| ~ spl24_269 ),
inference(resolution,[],[f5196,f164]) ).
fof(f78326,plain,
( $false
| ~ spl24_269
| spl24_271 ),
inference(forward_subsumption_resolution,[],[f78295,f5205]) ).
fof(f78327,plain,
( ~ spl24_269
| spl24_271 ),
inference(avatar_contradiction_clause,[],[f78326]) ).
fof(f80401,plain,
! [X2,X0,X1] :
( subq(m(X0,X1),X2)
| ~ subq(X0,X1)
| subq(m(X0,X1),X2) ),
inference(resolution,[],[f6921,f226]) ).
fof(f80877,plain,
! [X2,X0,X1] :
( subq(m(X0,X1),X2)
| ~ subq(X0,X1) ),
inference(duplicate_literal_removal,[],[f80401]) ).
fof(f81369,plain,
! [X0,X1] :
( ~ subq(X0,X1)
| e = m(X0,X1) ),
inference(resolution,[],[f80877,f414]) ).
fof(f82054,definition,
( spl24_1904
<=> subq(sK1(sF16,sF23),e) ),
introduced(definition,[new_symbols(definition,[spl24_1904])],[avatar_definition]) ).
fof(f82055,plain,
( ~ subq(sK1(sF16,sF23),e)
| spl24_1904 ),
inference(avatar_component_clause,[],[f82054]) ).
fof(f82056,plain,
( subq(sK1(sF16,sF23),e)
| ~ spl24_1904 ),
inference(avatar_component_clause,[],[f82054]) ).
fof(f82778,plain,
( e = sK1(sF16,sF23)
| ~ spl24_1904 ),
inference(resolution,[],[f82056,f414]) ).
fof(f82912,plain,
( ~ mem(e,sF14)
| e = sF7
| disj(sF16,sF23)
| ~ spl24_1904 ),
inference(superposition,[],[f48941,f82778]) ).
fof(f83064,plain,
( e = sF7
| disj(sF16,sF23)
| ~ spl24_1904 ),
inference(forward_subsumption_resolution,[],[f82912,f300]) ).
fof(f83141,plain,
( disj(sF16,sF23)
| spl24_55
| ~ spl24_1904 ),
inference(forward_subsumption_resolution,[],[f83064,f1021]) ).
fof(f83192,plain,
( $false
| spl24_55
| ~ spl24_1904 ),
inference(forward_subsumption_resolution,[],[f83141,f111]) ).
fof(f83193,plain,
( spl24_55
| ~ spl24_1904 ),
inference(avatar_contradiction_clause,[],[f83192]) ).
fof(f83242,definition,
( spl24_1918
<=> mem(sK0(sK1(sF16,sF23),e),sF3) ),
introduced(definition,[new_symbols(definition,[spl24_1918])],[avatar_definition]) ).
fof(f83243,plain,
( ~ mem(sK0(sK1(sF16,sF23),e),sF3)
| spl24_1918 ),
inference(avatar_component_clause,[],[f83242]) ).
fof(f83244,plain,
( mem(sK0(sK1(sF16,sF23),e),sF3)
| ~ spl24_1918 ),
inference(avatar_component_clause,[],[f83242]) ).
fof(f83394,plain,
( e = sK0(sK1(sF16,sF23),e)
| ~ spl24_28
| ~ spl24_1918 ),
inference(resolution,[],[f83244,f2685]) ).
fof(f83418,plain,
( mem(e,sK1(sF16,sF23))
| subq(sK1(sF16,sF23),e)
| ~ spl24_28
| ~ spl24_1918 ),
inference(superposition,[],[f45,f83394]) ).
fof(f83476,plain,
( subq(sK1(sF16,sF23),e)
| ~ spl24_28
| spl24_1631
| ~ spl24_1918 ),
inference(forward_subsumption_resolution,[],[f83418,f71147]) ).
fof(f83477,plain,
( $false
| ~ spl24_28
| spl24_1631
| spl24_1904
| ~ spl24_1918 ),
inference(forward_subsumption_resolution,[],[f83476,f82055]) ).
fof(f83478,plain,
( ~ spl24_28
| spl24_1631
| spl24_1904
| ~ spl24_1918 ),
inference(avatar_contradiction_clause,[],[f83477]) ).
fof(f83571,plain,
( mem(sK0(sF16,sF12),sF22)
| mem(sK0(sF16,sF12),sF20)
| ~ spl24_5
| ~ spl24_648 ),
inference(forward_subsumption_resolution,[],[f27466,f11753]) ).
fof(f83645,definition,
( spl24_1926
<=> subq(sK1(sF16,sF23),sF11) ),
introduced(definition,[new_symbols(definition,[spl24_1926])],[avatar_definition]) ).
fof(f83647,plain,
( subq(sK1(sF16,sF23),sF11)
| ~ spl24_1926 ),
inference(avatar_component_clause,[],[f83645]) ).
fof(f83661,plain,
( mem(sF7,sF22)
| mem(sK0(sF16,sF12),sF20)
| ~ spl24_5
| ~ spl24_648 ),
inference(forward_demodulation,[],[f83571,f1914]) ).
fof(f83665,definition,
( spl24_1927
<=> mem(sF7,sF20) ),
introduced(definition,[new_symbols(definition,[spl24_1927])],[avatar_definition]) ).
fof(f83667,plain,
( mem(sF7,sF20)
| ~ spl24_1927 ),
inference(avatar_component_clause,[],[f83665]) ).
fof(f83704,plain,
( mem(sK0(sF16,sF12),sF20)
| ~ spl24_5
| spl24_500
| ~ spl24_648 ),
inference(forward_subsumption_resolution,[],[f83661,f9286]) ).
fof(f83719,plain,
( mem(sF7,sF20)
| ~ spl24_5
| spl24_500
| ~ spl24_648 ),
inference(forward_demodulation,[],[f83704,f1914]) ).
fof(f83724,plain,
( spl24_1927
| ~ spl24_5
| spl24_500
| ~ spl24_648 ),
inference(avatar_split_clause,[],[f83719,f11752,f9284,f475,f83665]) ).
fof(f83734,plain,
( sF21 = sK0(sF16,sF12)
| ~ spl24_5
| ~ spl24_499 ),
inference(forward_subsumption_resolution,[],[f27464,f9282]) ).
fof(f83805,plain,
( sF7 = sF21
| ~ spl24_5
| ~ spl24_499 ),
inference(forward_demodulation,[],[f83734,f1914]) ).
fof(f83878,plain,
( $false
| ~ spl24_5
| spl24_494
| ~ spl24_499 ),
inference(forward_subsumption_resolution,[],[f83805,f9162]) ).
fof(f83879,plain,
( ~ spl24_5
| spl24_494
| ~ spl24_499 ),
inference(avatar_contradiction_clause,[],[f83878]) ).
fof(f83932,plain,
( subq(sK0(sF16,sF12),sF17)
| ~ spl24_5
| ~ spl24_661 ),
inference(forward_subsumption_resolution,[],[f27452,f11807]) ).
fof(f83948,plain,
( sF6 = sK0(sF16,sF12)
| ~ spl24_5
| ~ spl24_657 ),
inference(forward_subsumption_resolution,[],[f27457,f11791]) ).
fof(f84022,definition,
( spl24_1934
<=> mem(sF7,sF19) ),
introduced(definition,[new_symbols(definition,[spl24_1934])],[avatar_definition]) ).
fof(f84023,plain,
( ~ mem(sF7,sF19)
| spl24_1934 ),
inference(avatar_component_clause,[],[f84022]) ).
fof(f84044,plain,
( subq(sF7,sF17)
| ~ spl24_5
| ~ spl24_661 ),
inference(forward_demodulation,[],[f83932,f1914]) ).
fof(f84061,plain,
( sF6 = sF7
| ~ spl24_5
| ~ spl24_657 ),
inference(forward_demodulation,[],[f83948,f1914]) ).
fof(f84126,plain,
( spl24_1094
| ~ spl24_5
| ~ spl24_661 ),
inference(avatar_split_clause,[],[f84044,f11806,f475,f37683]) ).
fof(f84133,plain,
( $false
| ~ spl24_5
| spl24_162
| ~ spl24_657 ),
inference(forward_subsumption_resolution,[],[f84061,f3624]) ).
fof(f84134,plain,
( ~ spl24_5
| spl24_162
| ~ spl24_657 ),
inference(avatar_contradiction_clause,[],[f84133]) ).
fof(f84149,plain,
( ~ spl24_1934
| spl24_162
| spl24_657 ),
inference(avatar_split_clause,[],[f12543,f11790,f3623,f84022]) ).
fof(f84157,plain,
( subq(sK1(sF16,sF23),sF11)
| ~ spl24_1495 ),
inference(resolution,[],[f60266,f146]) ).
fof(f84161,plain,
( spl24_1926
| ~ spl24_1495 ),
inference(avatar_split_clause,[],[f84157,f60226,f83645]) ).
fof(f84169,plain,
( ! [X0] :
( mem(sK1(sF16,sF23),X0)
| ~ subq(sF15,X0) )
| spl24_1494 ),
inference(forward_subsumption_resolution,[],[f60275,f111]) ).
fof(f84317,plain,
( ~ subq(sF9,sF7)
| ~ spl24_494
| spl24_910 ),
inference(superposition,[],[f26364,f9163]) ).
fof(f84377,plain,
( $false
| ~ spl24_494
| ~ spl24_834
| spl24_910 ),
inference(forward_subsumption_resolution,[],[f84317,f21501]) ).
fof(f84378,plain,
( ~ spl24_494
| ~ spl24_834
| spl24_910 ),
inference(avatar_contradiction_clause,[],[f84377]) ).
fof(f84599,plain,
( ~ subq(sF15,sF16)
| mem(sK1(sF16,sF23),sF15)
| mem(sK1(sF16,sF23),sF8)
| spl24_1494 ),
inference(resolution,[],[f84169,f208]) ).
fof(f84689,plain,
( ~ subq(sK1(sF16,sF23),sF3)
| subq(sK1(sF16,sF23),e)
| spl24_1918 ),
inference(resolution,[],[f83243,f382]) ).
fof(f84699,plain,
( subq(sK1(sF16,sF23),e)
| ~ spl24_1547
| spl24_1918 ),
inference(forward_subsumption_resolution,[],[f84689,f61496]) ).
fof(f84718,plain,
( $false
| ~ spl24_1547
| spl24_1904
| spl24_1918 ),
inference(forward_subsumption_resolution,[],[f84699,f82055]) ).
fof(f84719,plain,
( ~ spl24_1547
| spl24_1904
| spl24_1918 ),
inference(avatar_contradiction_clause,[],[f84718]) ).
fof(f84757,plain,
( mem(sK1(sF16,sF23),sF15)
| mem(sK1(sF16,sF23),sF8)
| ~ spl24_67
| spl24_1494 ),
inference(forward_subsumption_resolution,[],[f84599,f1210]) ).
fof(f84805,plain,
( mem(sK1(sF16,sF23),sF8)
| ~ spl24_67
| spl24_1494
| spl24_1495 ),
inference(forward_subsumption_resolution,[],[f84757,f60227]) ).
fof(f84835,plain,
( $false
| ~ spl24_67
| spl24_1494
| spl24_1495 ),
inference(forward_subsumption_resolution,[],[f84805,f60223]) ).
fof(f84836,plain,
( ~ spl24_67
| spl24_1494
| spl24_1495 ),
inference(avatar_contradiction_clause,[],[f84835]) ).
fof(f84945,plain,
( sF7 = sK1(sF16,sF23)
| ~ spl24_1494 ),
inference(resolution,[],[f60224,f165]) ).
fof(f84954,plain,
( spl24_1509
| ~ spl24_1494 ),
inference(avatar_split_clause,[],[f84945,f60222,f60433]) ).
fof(f85052,plain,
( subq(sF7,sF17)
| sF7 = sF21
| sF6 = sF7
| disj(sF16,sF23)
| ~ spl24_1509 ),
inference(superposition,[],[f593,f60435]) ).
fof(f85185,plain,
( subq(sF7,sF17)
| sF6 = sF7
| disj(sF16,sF23)
| spl24_494
| ~ spl24_1509 ),
inference(forward_subsumption_resolution,[],[f85052,f9162]) ).
fof(f85241,plain,
( subq(sF7,sF17)
| disj(sF16,sF23)
| spl24_162
| spl24_494
| ~ spl24_1509 ),
inference(forward_subsumption_resolution,[],[f85185,f3624]) ).
fof(f85256,plain,
( subq(sF7,sF17)
| spl24_162
| spl24_494
| ~ spl24_1509 ),
inference(forward_subsumption_resolution,[],[f85241,f111]) ).
fof(f85273,plain,
( spl24_1094
| spl24_162
| spl24_494
| ~ spl24_1509 ),
inference(avatar_split_clause,[],[f85256,f60433,f9161,f3623,f37683]) ).
fof(f85397,plain,
( $false
| spl24_834 ),
inference(forward_subsumption_resolution,[],[f25901,f21500]) ).
fof(f85398,plain,
spl24_834,
inference(avatar_contradiction_clause,[],[f85397]) ).
fof(f85943,plain,
( subq(sF5,sF4)
| ~ spl24_201 ),
inference(superposition,[],[f4934,f4337]) ).
fof(f86115,plain,
( $false
| spl24_89
| ~ spl24_201 ),
inference(forward_subsumption_resolution,[],[f85943,f1928]) ).
fof(f86116,plain,
( spl24_89
| ~ spl24_201 ),
inference(avatar_contradiction_clause,[],[f86115]) ).
fof(f86248,plain,
( sF4 = sK0(sF6,sF4)
| spl24_249 ),
inference(forward_subsumption_resolution,[],[f30105,f4960]) ).
fof(f86263,plain,
( subq(sF6,sF18)
| mem(sF4,sF4)
| ~ subq(sF6,sF9)
| spl24_216
| ~ spl24_1375 ),
inference(forward_subsumption_resolution,[],[f45658,f4417]) ).
fof(f86308,plain,
( sF3 = sF4
| spl24_249
| ~ spl24_873 ),
inference(forward_demodulation,[],[f86248,f23602]) ).
fof(f86361,plain,
( $false
| spl24_30
| spl24_249
| ~ spl24_873 ),
inference(forward_subsumption_resolution,[],[f86308,f686]) ).
fof(f86362,plain,
( spl24_30
| spl24_249
| ~ spl24_873 ),
inference(avatar_contradiction_clause,[],[f86361]) ).
fof(f86861,plain,
( ! [X0] :
( mem(X0,e)
| ~ mem(X0,sF4)
| mem(X0,sK1(sF16,sF23)) )
| spl24_1547
| ~ spl24_1624 ),
inference(superposition,[],[f58,f70919]) ).
fof(f86890,plain,
( ! [X0] :
( mem(X0,sK1(sF16,sF23))
| ~ mem(X0,sF4) )
| spl24_1547
| ~ spl24_1624 ),
inference(forward_subsumption_resolution,[],[f86861,f50]) ).
fof(f86893,plain,
( ! [X0] :
( ~ mem(sK0(X0,sK1(sF16,sF23)),sF4)
| subq(X0,sK1(sF16,sF23)) )
| spl24_1547
| ~ spl24_1624 ),
inference(resolution,[],[f86890,f46]) ).
fof(f87175,plain,
( e = m(s(e),sK1(sF16,sF23))
| ~ spl24_1631 ),
inference(resolution,[],[f71148,f17019]) ).
fof(f87177,plain,
( e = m(sF2,sK1(sF16,sF23))
| ~ spl24_1631 ),
inference(forward_demodulation,[],[f87175,f68]) ).
fof(f87178,plain,
( e = m(sF3,sK1(sF16,sF23))
| ~ spl24_28
| ~ spl24_1631 ),
inference(forward_demodulation,[],[f87177,f675]) ).
fof(f87259,plain,
( mem(sF7,sF19)
| mem(sF7,sF18)
| ~ spl24_1927 ),
inference(resolution,[],[f83667,f211]) ).
fof(f87391,plain,
( mem(sF3,sF17)
| ~ spl24_1094 ),
inference(resolution,[],[f37685,f387]) ).
fof(f87400,plain,
( $false
| spl24_25
| ~ spl24_1094 ),
inference(forward_subsumption_resolution,[],[f87391,f646]) ).
fof(f87401,plain,
( spl24_25
| ~ spl24_1094 ),
inference(avatar_contradiction_clause,[],[f87400]) ).
fof(f87407,plain,
( mem(sF7,sF18)
| ~ spl24_1927
| spl24_1934 ),
inference(forward_subsumption_resolution,[],[f87259,f84023]) ).
fof(f87413,plain,
( $false
| spl24_756
| ~ spl24_1927
| spl24_1934 ),
inference(forward_subsumption_resolution,[],[f87407,f14025]) ).
fof(f87414,plain,
( spl24_756
| ~ spl24_1927
| spl24_1934 ),
inference(avatar_contradiction_clause,[],[f87413]) ).
fof(f87629,plain,
( mem(sF9,sF19)
| disj(sF16,sF23)
| sF9 = sF21
| ~ subq(sF23,sF23)
| mem(sF9,sF18)
| ~ spl24_1511 ),
inference(superposition,[],[f32251,f60449]) ).
fof(f87634,plain,
( disj(sF16,sF23)
| sF9 = sF21
| ~ subq(sF23,sF23)
| mem(sF9,sF18)
| spl24_269
| ~ spl24_1511 ),
inference(forward_subsumption_resolution,[],[f87629,f5195]) ).
fof(f87703,plain,
( sF9 = sF21
| ~ subq(sF23,sF23)
| mem(sF9,sF18)
| spl24_269
| ~ spl24_1511 ),
inference(forward_subsumption_resolution,[],[f87634,f111]) ).
fof(f87742,plain,
( ~ subq(sF23,sF23)
| mem(sF9,sF18)
| spl24_266
| spl24_269
| ~ spl24_1511 ),
inference(forward_subsumption_resolution,[],[f87703,f5181]) ).
fof(f87773,plain,
( mem(sF9,sF18)
| spl24_266
| spl24_269
| ~ spl24_1511 ),
inference(forward_subsumption_resolution,[],[f87742,f240]) ).
fof(f87793,plain,
( $false
| spl24_266
| spl24_268
| spl24_269
| ~ spl24_1511 ),
inference(forward_subsumption_resolution,[],[f87773,f5191]) ).
fof(f87794,plain,
( spl24_266
| spl24_268
| spl24_269
| ~ spl24_1511 ),
inference(avatar_contradiction_clause,[],[f87793]) ).
fof(f87814,plain,
( subq(sF3,sF6)
| ~ spl24_162 ),
inference(superposition,[],[f4932,f3625]) ).
fof(f87916,plain,
( $false
| ~ spl24_162
| spl24_386 ),
inference(forward_subsumption_resolution,[],[f87814,f6906]) ).
fof(f87917,plain,
( ~ spl24_162
| spl24_386 ),
inference(avatar_contradiction_clause,[],[f87916]) ).
fof(f95122,plain,
( ! [X0] :
( mem(X0,e)
| ~ mem(X0,sF3)
| mem(X0,sK1(sF16,sF23)) )
| ~ spl24_28
| ~ spl24_1631 ),
inference(superposition,[],[f58,f87178]) ).
fof(f95151,plain,
( ! [X0] :
( mem(X0,sK1(sF16,sF23))
| ~ mem(X0,sF3) )
| ~ spl24_28
| ~ spl24_1631 ),
inference(forward_subsumption_resolution,[],[f95122,f50]) ).
fof(f95157,plain,
( ! [X0] :
( ~ mem(sK0(X0,sK1(sF16,sF23)),sF3)
| subq(X0,sK1(sF16,sF23)) )
| ~ spl24_28
| ~ spl24_1631 ),
inference(resolution,[],[f95151,f46]) ).
fof(f95172,plain,
( ! [X0] :
( subq(X0,sK1(sF16,sF23))
| subq(X0,sK1(sF16,sF23))
| mem(sK0(X0,sK1(sF16,sF23)),sF4)
| ~ subq(X0,sF9) )
| ~ spl24_28
| ~ spl24_1631 ),
inference(resolution,[],[f95157,f1281]) ).
fof(f95219,plain,
( ! [X0] :
( subq(X0,sK1(sF16,sF23))
| mem(sK0(X0,sK1(sF16,sF23)),sF4)
| ~ subq(X0,sF9) )
| ~ spl24_28
| ~ spl24_1631 ),
inference(duplicate_literal_removal,[],[f95172]) ).
fof(f95226,plain,
( ! [X0] :
( subq(X0,sK1(sF16,sF23))
| ~ subq(X0,sF9) )
| ~ spl24_28
| spl24_1547
| ~ spl24_1624
| ~ spl24_1631 ),
inference(forward_subsumption_resolution,[],[f95219,f86893]) ).
fof(f95344,plain,
( ~ subq(sF9,sF9)
| ~ spl24_28
| spl24_1510
| spl24_1547
| ~ spl24_1624
| ~ spl24_1631 ),
inference(resolution,[],[f95226,f60445]) ).
fof(f95416,plain,
( $false
| ~ spl24_28
| spl24_1510
| spl24_1547
| ~ spl24_1624
| ~ spl24_1631 ),
inference(forward_subsumption_resolution,[],[f95344,f240]) ).
fof(f95417,plain,
( ~ spl24_28
| spl24_1510
| spl24_1547
| ~ spl24_1624
| ~ spl24_1631 ),
inference(avatar_contradiction_clause,[],[f95416]) ).
fof(f96703,plain,
( $false
| spl24_1498
| ~ spl24_1503 ),
inference(forward_subsumption_resolution,[],[f60439,f60301]) ).
fof(f96704,plain,
( spl24_1498
| ~ spl24_1503 ),
inference(avatar_contradiction_clause,[],[f96703]) ).
fof(f96765,plain,
( e = m(sK1(sF16,sF23),sF7)
| ~ spl24_1498 ),
inference(resolution,[],[f60302,f81369]) ).
fof(f96817,plain,
( ! [X0] :
( mem(X0,e)
| ~ mem(X0,sK1(sF16,sF23))
| mem(X0,sF7) )
| ~ spl24_1498 ),
inference(superposition,[],[f58,f96765]) ).
fof(f96846,plain,
( ! [X0] :
( ~ mem(X0,sK1(sF16,sF23))
| mem(X0,sF7) )
| ~ spl24_1498 ),
inference(forward_subsumption_resolution,[],[f96817,f50]) ).
fof(f96855,plain,
( ! [X0] :
( mem(sK0(sK1(sF16,sF23),X0),sF7)
| subq(sK1(sF16,sF23),X0) )
| ~ spl24_1498 ),
inference(resolution,[],[f96846,f45]) ).
fof(f96913,plain,
( ! [X0] :
( mem(sK0(sK1(sF16,sF23),X0),sF6)
| subq(sK1(sF16,sF23),X0)
| mem(sK0(sK1(sF16,sF23),X0),sF3) )
| ~ spl24_1498 ),
inference(resolution,[],[f96855,f205]) ).
fof(f96926,plain,
( subq(sK1(sF16,sF23),sF6)
| mem(sK0(sK1(sF16,sF23),sF6),sF3)
| subq(sK1(sF16,sF23),sF6)
| ~ spl24_1498 ),
inference(resolution,[],[f96913,f46]) ).
fof(f96945,plain,
( subq(sK1(sF16,sF23),sF6)
| mem(sK0(sK1(sF16,sF23),sF6),sF3)
| ~ spl24_1498 ),
inference(duplicate_literal_removal,[],[f96926]) ).
fof(f96946,plain,
( mem(sK0(sK1(sF16,sF23),sF6),sF3)
| ~ spl24_1498
| spl24_1506 ),
inference(forward_subsumption_resolution,[],[f96945,f60405]) ).
fof(f96950,plain,
( e = sK0(sK1(sF16,sF23),sF6)
| ~ spl24_28
| ~ spl24_1498
| spl24_1506 ),
inference(resolution,[],[f96946,f2685]) ).
fof(f96976,plain,
( mem(e,sK1(sF16,sF23))
| subq(sK1(sF16,sF23),sF6)
| ~ spl24_28
| ~ spl24_1498
| spl24_1506 ),
inference(superposition,[],[f45,f96950]) ).
fof(f97034,plain,
( subq(sK1(sF16,sF23),sF6)
| ~ spl24_28
| ~ spl24_1498
| spl24_1506
| spl24_1631 ),
inference(forward_subsumption_resolution,[],[f96976,f71147]) ).
fof(f97035,plain,
( $false
| ~ spl24_28
| ~ spl24_1498
| spl24_1506
| spl24_1631 ),
inference(forward_subsumption_resolution,[],[f97034,f60405]) ).
fof(f97036,plain,
( ~ spl24_28
| ~ spl24_1498
| spl24_1506
| spl24_1631 ),
inference(avatar_contradiction_clause,[],[f97035]) ).
fof(f97042,plain,
( subq(sK1(sF16,sF23),sF4)
| sF4 = sK0(sK1(sF16,sF23),sF4)
| ~ spl24_1506 ),
inference(resolution,[],[f60404,f23350]) ).
fof(f97054,plain,
( sF4 = sK0(sK1(sF16,sF23),sF4)
| ~ spl24_1506
| spl24_1628 ),
inference(forward_subsumption_resolution,[],[f97042,f70991]) ).
fof(f97079,plain,
( mem(sF4,sF9)
| ~ subq(sK1(sF16,sF23),sF11)
| subq(sK1(sF16,sF23),sF4)
| sF4 = sF9
| ~ spl24_1506
| spl24_1628 ),
inference(superposition,[],[f20581,f97054]) ).
fof(f97117,plain,
( ~ subq(sK1(sF16,sF23),sF11)
| subq(sK1(sF16,sF23),sF4)
| sF4 = sF9
| spl24_214
| ~ spl24_1506
| spl24_1628 ),
inference(forward_subsumption_resolution,[],[f97079,f4402]) ).
fof(f97136,plain,
( subq(sK1(sF16,sF23),sF4)
| sF4 = sF9
| spl24_214
| ~ spl24_1506
| spl24_1628
| ~ spl24_1926 ),
inference(forward_subsumption_resolution,[],[f97117,f83647]) ).
fof(f97157,plain,
( sF4 = sF9
| spl24_214
| ~ spl24_1506
| spl24_1628
| ~ spl24_1926 ),
inference(forward_subsumption_resolution,[],[f97136,f70991]) ).
fof(f97175,plain,
( $false
| spl24_131
| spl24_214
| ~ spl24_1506
| spl24_1628
| ~ spl24_1926 ),
inference(forward_subsumption_resolution,[],[f97157,f2350]) ).
fof(f97176,plain,
( spl24_131
| spl24_214
| ~ spl24_1506
| spl24_1628
| ~ spl24_1926 ),
inference(avatar_contradiction_clause,[],[f97175]) ).
fof(f97494,plain,
( subq(sF4,sF17)
| ~ subq(sF23,sF23)
| disj(sF16,sF23)
| sF4 = sF6
| sF4 = sF21
| ~ spl24_1514 ),
inference(superposition,[],[f32290,f60919]) ).
fof(f97499,plain,
( ~ subq(sF23,sF23)
| disj(sF16,sF23)
| sF4 = sF6
| sF4 = sF21
| spl24_208
| ~ spl24_1514 ),
inference(forward_subsumption_resolution,[],[f97494,f4370]) ).
fof(f97571,plain,
( disj(sF16,sF23)
| sF4 = sF6
| sF4 = sF21
| spl24_208
| ~ spl24_1514 ),
inference(forward_subsumption_resolution,[],[f97499,f240]) ).
fof(f97592,plain,
( sF4 = sF6
| sF4 = sF21
| spl24_208
| ~ spl24_1514 ),
inference(forward_subsumption_resolution,[],[f97571,f111]) ).
fof(f97609,plain,
( sF4 = sF21
| spl24_206
| spl24_208
| ~ spl24_1514 ),
inference(forward_subsumption_resolution,[],[f97592,f4360]) ).
fof(f97622,plain,
( $false
| spl24_201
| spl24_206
| spl24_208
| ~ spl24_1514 ),
inference(forward_subsumption_resolution,[],[f97609,f4336]) ).
fof(f97623,plain,
( spl24_201
| spl24_206
| spl24_208
| ~ spl24_1514 ),
inference(avatar_contradiction_clause,[],[f97622]) ).
fof(f97785,plain,
( mem(sF4,sF4)
| ~ subq(sF6,sF9)
| spl24_216
| spl24_1371
| ~ spl24_1375 ),
inference(forward_subsumption_resolution,[],[f86263,f45336]) ).
fof(f97918,plain,
( ~ subq(sF6,sF9)
| spl24_90
| spl24_216
| spl24_1371
| ~ spl24_1375 ),
inference(forward_subsumption_resolution,[],[f97785,f1933]) ).
fof(f98011,plain,
( ~ subq(sF4,sF9)
| spl24_90
| ~ spl24_206
| spl24_216
| spl24_1371
| ~ spl24_1375 ),
inference(forward_demodulation,[],[f97918,f4361]) ).
fof(f98046,plain,
( $false
| spl24_90
| ~ spl24_130
| ~ spl24_206
| spl24_216
| spl24_1371
| ~ spl24_1375 ),
inference(forward_subsumption_resolution,[],[f98011,f2346]) ).
fof(f98047,plain,
( spl24_90
| ~ spl24_130
| ~ spl24_206
| spl24_216
| spl24_1371
| ~ spl24_1375 ),
inference(avatar_contradiction_clause,[],[f98046]) ).
fof(f99658,plain,
( ~ mem(sF3,sF18)
| subq(sF6,sF18)
| ~ spl24_1374 ),
inference(superposition,[],[f46,f45646]) ).
fof(f99716,plain,
( subq(sF6,sF18)
| ~ spl24_21
| ~ spl24_1374 ),
inference(forward_subsumption_resolution,[],[f99658,f629]) ).
fof(f99718,plain,
( $false
| ~ spl24_21
| spl24_1371
| ~ spl24_1374 ),
inference(forward_subsumption_resolution,[],[f99716,f45336]) ).
fof(f99719,plain,
( ~ spl24_21
| spl24_1371
| ~ spl24_1374 ),
inference(avatar_contradiction_clause,[],[f99718]) ).
fof(f99950,plain,
( mem(sF9,sF17)
| ~ subq(sF23,sF23)
| disj(sF16,sF23)
| sF6 = sK1(sF16,sF23)
| sF21 = sK1(sF16,sF23)
| ~ spl24_1504 ),
inference(resolution,[],[f60380,f32290]) ).
fof(f99966,plain,
( ~ subq(sF23,sF23)
| disj(sF16,sF23)
| sF6 = sK1(sF16,sF23)
| sF21 = sK1(sF16,sF23)
| spl24_246
| ~ spl24_1504 ),
inference(forward_subsumption_resolution,[],[f99950,f4890]) ).
fof(f99975,plain,
( disj(sF16,sF23)
| sF6 = sK1(sF16,sF23)
| sF21 = sK1(sF16,sF23)
| spl24_246
| ~ spl24_1504 ),
inference(forward_subsumption_resolution,[],[f99966,f240]) ).
fof(f99977,plain,
( sF6 = sK1(sF16,sF23)
| sF21 = sK1(sF16,sF23)
| spl24_246
| ~ spl24_1504 ),
inference(forward_subsumption_resolution,[],[f99975,f111]) ).
fof(f99979,plain,
( spl24_1634
| spl24_1531
| spl24_246
| ~ spl24_1504 ),
inference(avatar_split_clause,[],[f99977,f60379,f4888,f61005,f71162]) ).
fof(f100158,plain,
( subq(sF6,sF11)
| mem(sF6,sF8)
| disj(sF16,sF23)
| ~ spl24_1531 ),
inference(superposition,[],[f434,f61007]) ).
fof(f100305,plain,
( mem(sF6,sF8)
| disj(sF16,sF23)
| spl24_366
| ~ spl24_1531 ),
inference(forward_subsumption_resolution,[],[f100158,f6562]) ).
fof(f100386,plain,
( disj(sF16,sF23)
| spl24_354
| spl24_366
| ~ spl24_1531 ),
inference(forward_subsumption_resolution,[],[f100305,f6506]) ).
fof(f100409,plain,
( $false
| spl24_354
| spl24_366
| ~ spl24_1531 ),
inference(forward_subsumption_resolution,[],[f100386,f111]) ).
fof(f100410,plain,
( spl24_354
| spl24_366
| ~ spl24_1531 ),
inference(avatar_contradiction_clause,[],[f100409]) ).
fof(f100597,plain,
( subq(sF21,sF11)
| sF7 = sF21
| disj(sF16,sF23)
| ~ spl24_1634 ),
inference(superposition,[],[f48944,f71164]) ).
fof(f100728,plain,
( sF7 = sF21
| disj(sF16,sF23)
| spl24_753
| ~ spl24_1634 ),
inference(forward_subsumption_resolution,[],[f100597,f14005]) ).
fof(f100816,plain,
( disj(sF16,sF23)
| spl24_494
| spl24_753
| ~ spl24_1634 ),
inference(forward_subsumption_resolution,[],[f100728,f9162]) ).
fof(f100847,plain,
( $false
| spl24_494
| spl24_753
| ~ spl24_1634 ),
inference(forward_subsumption_resolution,[],[f100816,f111]) ).
fof(f100848,plain,
( spl24_494
| spl24_753
| ~ spl24_1634 ),
inference(avatar_contradiction_clause,[],[f100847]) ).
fof(f101048,plain,
( subq(sF21,sF10)
| sF4 = sF9
| mem(sF4,sF4)
| ~ subq(sF21,sF11)
| spl24_216
| ~ spl24_978 ),
inference(forward_subsumption_resolution,[],[f30965,f4417]) ).
fof(f101259,plain,
( sF4 = sF9
| mem(sF4,sF4)
| ~ subq(sF21,sF11)
| spl24_167
| spl24_216
| ~ spl24_978 ),
inference(forward_subsumption_resolution,[],[f101048,f3718]) ).
fof(f101418,plain,
( mem(sF4,sF4)
| ~ subq(sF21,sF11)
| spl24_131
| spl24_167
| spl24_216
| ~ spl24_978 ),
inference(forward_subsumption_resolution,[],[f101259,f2350]) ).
fof(f101511,plain,
( ~ subq(sF21,sF11)
| spl24_90
| spl24_131
| spl24_167
| spl24_216
| ~ spl24_978 ),
inference(forward_subsumption_resolution,[],[f101418,f1933]) ).
fof(f101558,plain,
( $false
| spl24_90
| spl24_131
| spl24_167
| spl24_216
| ~ spl24_753
| ~ spl24_978 ),
inference(forward_subsumption_resolution,[],[f101511,f14004]) ).
fof(f101559,plain,
( spl24_90
| spl24_131
| spl24_167
| spl24_216
| ~ spl24_753
| ~ spl24_978 ),
inference(avatar_contradiction_clause,[],[f101558]) ).
fof(f101599,plain,
( sF4 = sK0(sF21,sF10)
| spl24_167 ),
inference(forward_subsumption_resolution,[],[f33789,f3718]) ).
fof(f101662,plain,
( $false
| spl24_167
| spl24_978 ),
inference(forward_subsumption_resolution,[],[f101599,f30615]) ).
fof(f101663,plain,
( spl24_167
| spl24_978 ),
inference(avatar_contradiction_clause,[],[f101662]) ).
cnf(s3,plain,
( spl24_5
| spl24_6 ),
inference(sat_conversion,[],[f482]) ).
cnf(s11,plain,
( spl24_21
| spl24_22 ),
inference(sat_conversion,[],[f634]) ).
cnf(s14,plain,
( ~ spl24_27
| spl24_28 ),
inference(sat_conversion,[],[f676]) ).
cnf(s16,plain,
~ spl24_25,
inference(sat_conversion,[],[f743]) ).
cnf(s32,plain,
( spl24_59
| spl24_60 ),
inference(sat_conversion,[],[f1046]) ).
cnf(s45,plain,
spl24_67,
inference(sat_conversion,[],[f1506]) ).
cnf(s84,plain,
spl24_130,
inference(sat_conversion,[],[f2597]) ).
cnf(s85,plain,
spl24_27,
inference(sat_conversion,[],[f2599]) ).
cnf(s91,plain,
( spl24_25
| ~ spl24_30 ),
inference(sat_conversion,[],[f2751]) ).
cnf(s136,plain,
( ~ spl24_28
| ~ spl24_29
| spl24_30 ),
inference(sat_conversion,[],[f3386]) ).
cnf(s152,plain,
( ~ spl24_167
| spl24_168 ),
inference(sat_conversion,[],[f3723]) ).
cnf(s175,plain,
( spl24_30
| ~ spl24_90 ),
inference(sat_conversion,[],[f4105]) ).
cnf(s186,plain,
( spl24_21
| ~ spl24_22 ),
inference(sat_conversion,[],[f4231]) ).
cnf(s208,plain,
( spl24_56
| ~ spl24_212 ),
inference(sat_conversion,[],[f4436]) ).
cnf(s240,plain,
( spl24_25
| ~ spl24_241 ),
inference(sat_conversion,[],[f4749]) ).
cnf(s246,plain,
( spl24_216
| ~ spl24_239 ),
inference(sat_conversion,[],[f4779]) ).
cnf(s257,plain,
( spl24_29
| ~ spl24_130
| ~ spl24_237 ),
inference(sat_conversion,[],[f4831]) ).
cnf(s259,plain,
( spl24_30
| ~ spl24_225 ),
inference(sat_conversion,[],[f4840]) ).
cnf(s268,plain,
( spl24_206
| ~ spl24_249 ),
inference(sat_conversion,[],[f4961]) ).
cnf(s309,plain,
( spl24_25
| ~ spl24_208 ),
inference(sat_conversion,[],[f5368]) ).
cnf(s360,plain,
( ~ spl24_190
| spl24_214
| spl24_327 ),
inference(sat_conversion,[],[f5673]) ).
cnf(s367,plain,
( spl24_131
| ~ spl24_327 ),
inference(sat_conversion,[],[f5743]) ).
cnf(s394,plain,
( ~ spl24_89
| spl24_90 ),
inference(sat_conversion,[],[f5985]) ).
cnf(s401,plain,
( spl24_90
| ~ spl24_214
| spl24_216 ),
inference(sat_conversion,[],[f6062]) ).
cnf(s402,plain,
( ~ spl24_28
| spl24_60
| ~ spl24_216 ),
inference(sat_conversion,[],[f6069]) ).
cnf(s409,plain,
~ spl24_60,
inference(sat_conversion,[],[f6126]) ).
cnf(s411,plain,
( ~ spl24_39
| spl24_60 ),
inference(sat_conversion,[],[f6130]) ).
cnf(s412,plain,
( spl24_75
| ~ spl24_131 ),
inference(sat_conversion,[],[f6152]) ).
cnf(s415,plain,
( ~ spl24_56
| spl24_241 ),
inference(sat_conversion,[],[f6166]) ).
cnf(s423,plain,
( ~ spl24_130
| spl24_131
| ~ spl24_246 ),
inference(sat_conversion,[],[f6200]) ).
cnf(s424,plain,
( ~ spl24_203
| spl24_208 ),
inference(sat_conversion,[],[f6213]) ).
cnf(s452,plain,
( spl24_25
| ~ spl24_75 ),
inference(sat_conversion,[],[f6425]) ).
cnf(s513,plain,
( spl24_162
| ~ spl24_354 ),
inference(sat_conversion,[],[f6765]) ).
cnf(s628,plain,
( spl24_494
| spl24_495 ),
inference(sat_conversion,[],[f9168]) ).
cnf(s631,plain,
( ~ spl24_495
| spl24_499
| ~ spl24_500 ),
inference(sat_conversion,[],[f9287]) ).
cnf(s653,plain,
( ~ spl24_55
| spl24_244 ),
inference(sat_conversion,[],[f9514]) ).
cnf(s663,plain,
( spl24_212
| ~ spl24_244 ),
inference(sat_conversion,[],[f9615]) ).
cnf(s666,plain,
( ~ spl24_101
| spl24_190 ),
inference(sat_conversion,[],[f9635]) ).
cnf(s668,plain,
( ~ spl24_6
| spl24_101 ),
inference(sat_conversion,[],[f9652]) ).
cnf(s858,plain,
( spl24_214
| ~ spl24_266 ),
inference(sat_conversion,[],[f12080]) ).
cnf(s1210,plain,
( spl24_39
| spl24_56
| ~ spl24_59
| ~ spl24_386 ),
inference(sat_conversion,[],[f23186]) ).
cnf(s1225,plain,
( spl24_249
| spl24_873
| spl24_874 ),
inference(sat_conversion,[],[f23631]) ).
cnf(s1243,plain,
( spl24_90
| spl24_131
| spl24_216
| ~ spl24_366
| ~ spl24_874 ),
inference(sat_conversion,[],[f23848]) ).
cnf(s2343,plain,
( ~ spl24_168
| spl24_327 ),
inference(sat_conversion,[],[f40721]) ).
cnf(s2870,plain,
( ~ spl24_271
| spl24_386 ),
inference(sat_conversion,[],[f44718]) ).
cnf(s2892,plain,
( spl24_25
| ~ spl24_273 ),
inference(sat_conversion,[],[f44987]) ).
cnf(s2893,plain,
( ~ spl24_268
| spl24_273 ),
inference(sat_conversion,[],[f44990]) ).
cnf(s2935,plain,
( spl24_203
| ~ spl24_1371 ),
inference(sat_conversion,[],[f45505]) ).
cnf(s2936,plain,
( spl24_1371
| spl24_1374
| spl24_1375 ),
inference(sat_conversion,[],[f45651]) ).
cnf(s2976,plain,
( spl24_1094
| spl24_1379 ),
inference(sat_conversion,[],[f46294]) ).
cnf(s2979,plain,
( spl24_661
| ~ spl24_756
| ~ spl24_1379 ),
inference(sat_conversion,[],[f46363]) ).
cnf(s3337,plain,
( spl24_648
| spl24_1502
| spl24_1503 ),
inference(sat_conversion,[],[f60325]) ).
cnf(s3338,plain,
( ~ spl24_1502
| spl24_1503
| spl24_1504 ),
inference(sat_conversion,[],[f60381]) ).
cnf(s3352,plain,
( ~ spl24_1503
| ~ spl24_1510
| spl24_1511 ),
inference(sat_conversion,[],[f60450]) ).
cnf(s3666,plain,
( ~ spl24_1503
| spl24_1547
| spl24_1624 ),
inference(sat_conversion,[],[f70823]) ).
cnf(s3667,plain,
( ~ spl24_1547
| ~ spl24_1625
| spl24_1626 ),
inference(sat_conversion,[],[f70843]) ).
cnf(s3668,plain,
( ~ spl24_1547
| spl24_1626
| spl24_1627 ),
inference(sat_conversion,[],[f70848]) ).
cnf(s3671,plain,
( spl24_1514
| spl24_1547
| ~ spl24_1624
| ~ spl24_1628 ),
inference(sat_conversion,[],[f70992]) ).
cnf(s3680,plain,
( spl24_225
| spl24_237
| ~ spl24_910 ),
inference(sat_conversion,[],[f71301]) ).
cnf(s3880,plain,
( spl24_239
| ~ spl24_1626 ),
inference(sat_conversion,[],[f73374]) ).
cnf(s3888,plain,
( spl24_1625
| ~ spl24_1627
| ~ spl24_1631 ),
inference(sat_conversion,[],[f73453]) ).
cnf(s4156,plain,
( ~ spl24_269
| spl24_271 ),
inference(sat_conversion,[],[f78327]) ).
cnf(s4278,plain,
( spl24_55
| ~ spl24_1904 ),
inference(sat_conversion,[],[f83193]) ).
cnf(s4306,plain,
( ~ spl24_28
| spl24_1631
| spl24_1904
| ~ spl24_1918 ),
inference(sat_conversion,[],[f83478]) ).
cnf(s4318,plain,
( ~ spl24_5
| spl24_500
| ~ spl24_648
| spl24_1927 ),
inference(sat_conversion,[],[f83724]) ).
cnf(s4327,plain,
( ~ spl24_5
| spl24_494
| ~ spl24_499 ),
inference(sat_conversion,[],[f83879]) ).
cnf(s4360,plain,
( ~ spl24_5
| ~ spl24_661
| spl24_1094 ),
inference(sat_conversion,[],[f84126]) ).
cnf(s4367,plain,
( ~ spl24_5
| spl24_162
| ~ spl24_657 ),
inference(sat_conversion,[],[f84134]) ).
cnf(s4375,plain,
( spl24_162
| spl24_657
| ~ spl24_1934 ),
inference(sat_conversion,[],[f84149]) ).
cnf(s4377,plain,
( ~ spl24_1495
| spl24_1926 ),
inference(sat_conversion,[],[f84161]) ).
cnf(s4393,plain,
( ~ spl24_494
| ~ spl24_834
| spl24_910 ),
inference(sat_conversion,[],[f84378]) ).
cnf(s4411,plain,
( ~ spl24_1547
| spl24_1904
| spl24_1918 ),
inference(sat_conversion,[],[f84719]) ).
cnf(s4422,plain,
( ~ spl24_67
| spl24_1494
| spl24_1495 ),
inference(sat_conversion,[],[f84836]) ).
cnf(s4427,plain,
( ~ spl24_1494
| spl24_1509 ),
inference(sat_conversion,[],[f84954]) ).
cnf(s4443,plain,
( spl24_162
| spl24_494
| spl24_1094
| ~ spl24_1509 ),
inference(sat_conversion,[],[f85273]) ).
cnf(s4464,plain,
spl24_834,
inference(sat_conversion,[],[f85398]) ).
cnf(s4530,plain,
( spl24_89
| ~ spl24_201 ),
inference(sat_conversion,[],[f86116]) ).
cnf(s4568,plain,
( spl24_30
| spl24_249
| ~ spl24_873 ),
inference(sat_conversion,[],[f86362]) ).
cnf(s4638,plain,
( spl24_25
| ~ spl24_1094 ),
inference(sat_conversion,[],[f87401]) ).
cnf(s4639,plain,
( spl24_756
| ~ spl24_1927
| spl24_1934 ),
inference(sat_conversion,[],[f87414]) ).
cnf(s4672,plain,
( spl24_266
| spl24_268
| spl24_269
| ~ spl24_1511 ),
inference(sat_conversion,[],[f87794]) ).
cnf(s4676,plain,
( ~ spl24_162
| spl24_386 ),
inference(sat_conversion,[],[f87917]) ).
cnf(s4919,plain,
( ~ spl24_28
| spl24_1510
| spl24_1547
| ~ spl24_1624
| ~ spl24_1631 ),
inference(sat_conversion,[],[f95417]) ).
cnf(s4986,plain,
( spl24_1498
| ~ spl24_1503 ),
inference(sat_conversion,[],[f96704]) ).
cnf(s4988,plain,
( ~ spl24_28
| ~ spl24_1498
| spl24_1506
| spl24_1631 ),
inference(sat_conversion,[],[f97036]) ).
cnf(s4998,plain,
( spl24_131
| spl24_214
| ~ spl24_1506
| spl24_1628
| ~ spl24_1926 ),
inference(sat_conversion,[],[f97176]) ).
cnf(s5025,plain,
( spl24_201
| spl24_206
| spl24_208
| ~ spl24_1514 ),
inference(sat_conversion,[],[f97623]) ).
cnf(s5093,plain,
( spl24_90
| ~ spl24_130
| ~ spl24_206
| spl24_216
| spl24_1371
| ~ spl24_1375 ),
inference(sat_conversion,[],[f98047]) ).
cnf(s5192,plain,
( ~ spl24_21
| spl24_1371
| ~ spl24_1374 ),
inference(sat_conversion,[],[f99719]) ).
cnf(s5198,plain,
( spl24_246
| ~ spl24_1504
| spl24_1531
| spl24_1634 ),
inference(sat_conversion,[],[f99979]) ).
cnf(s5227,plain,
( spl24_354
| spl24_366
| ~ spl24_1531 ),
inference(sat_conversion,[],[f100410]) ).
cnf(s5265,plain,
( spl24_494
| spl24_753
| ~ spl24_1634 ),
inference(sat_conversion,[],[f100848]) ).
cnf(s5385,plain,
( spl24_90
| spl24_131
| spl24_167
| spl24_216
| ~ spl24_753
| ~ spl24_978 ),
inference(sat_conversion,[],[f101559]) ).
cnf(s5395,plain,
( spl24_167
| spl24_978 ),
inference(sat_conversion,[],[f101663]) ).
cnf(s5402,plain,
( ~ spl24_494
| spl24_910 ),
inference(rat,[],[s4393,s4464]) ).
cnf(s5440,plain,
~ spl24_39,
inference(rat,[],[s411,s409]) ).
cnf(s5441,plain,
( ~ spl24_28
| ~ spl24_216 ),
inference(rat,[],[s402,s409]) ).
cnf(s5463,plain,
spl24_59,
inference(rat,[],[s32,s409]) ).
cnf(s5468,plain,
~ spl24_1094,
inference(rat,[],[s4638,s16]) ).
cnf(s5470,plain,
~ spl24_273,
inference(rat,[],[s2892,s16]) ).
cnf(s5472,plain,
~ spl24_75,
inference(rat,[],[s452,s16]) ).
cnf(s5473,plain,
~ spl24_208,
inference(rat,[],[s309,s16]) ).
cnf(s5474,plain,
~ spl24_241,
inference(rat,[],[s240,s16]) ).
cnf(s5476,plain,
~ spl24_30,
inference(rat,[],[s91,s16]) ).
cnf(s5477,plain,
spl24_1379,
inference(rat,[],[s2976,s5468]) ).
cnf(s5479,plain,
~ spl24_268,
inference(rat,[],[s2893,s5470]) ).
cnf(s5481,plain,
~ spl24_131,
inference(rat,[],[s412,s5472]) ).
cnf(s5483,plain,
~ spl24_203,
inference(rat,[],[s424,s5473]) ).
cnf(s5485,plain,
~ spl24_56,
inference(rat,[],[s415,s5474]) ).
cnf(s5488,plain,
~ spl24_225,
inference(rat,[],[s259,s5476]) ).
cnf(s5490,plain,
~ spl24_90,
inference(rat,[],[s175,s5476]) ).
cnf(s5495,plain,
~ spl24_246,
inference(rat,[],[s423,s84,s5481]) ).
cnf(s5496,plain,
~ spl24_327,
inference(rat,[],[s367,s5481]) ).
cnf(s5502,plain,
~ spl24_1371,
inference(rat,[],[s2935,s5483]) ).
cnf(s5504,plain,
~ spl24_386,
inference(rat,[],[s1210,s5463,s5440,s5485]) ).
cnf(s5506,plain,
~ spl24_212,
inference(rat,[],[s208,s5485]) ).
cnf(s5508,plain,
~ spl24_89,
inference(rat,[],[s394,s5490]) ).
cnf(s5516,plain,
~ spl24_168,
inference(rat,[],[s2343,s5496]) ).
cnf(s5519,plain,
~ spl24_162,
inference(rat,[],[s4676,s5504]) ).
cnf(s5520,plain,
~ spl24_271,
inference(rat,[],[s2870,s5504]) ).
cnf(s5524,plain,
~ spl24_244,
inference(rat,[],[s663,s5506]) ).
cnf(s5529,plain,
~ spl24_201,
inference(rat,[],[s4530,s5508]) ).
cnf(s5534,plain,
~ spl24_167,
inference(rat,[],[s152,s5516]) ).
cnf(s5537,plain,
~ spl24_354,
inference(rat,[],[s513,s5519]) ).
cnf(s5540,plain,
~ spl24_269,
inference(rat,[],[s4156,s5520]) ).
cnf(s5545,plain,
~ spl24_55,
inference(rat,[],[s653,s5524]) ).
cnf(s5558,plain,
spl24_978,
inference(rat,[],[s5395,s5534]) ).
cnf(s5563,plain,
~ spl24_1904,
inference(rat,[],[s4278,s5545]) ).
cnf(s5570,plain,
spl24_28,
inference(rat,[],[s14,s85]) ).
cnf(s5575,plain,
~ spl24_216,
inference(rat,[],[s5441,s5570]) ).
cnf(s5580,plain,
~ spl24_29,
inference(rat,[],[s136,s5476,s5570]) ).
cnf(s5585,plain,
~ spl24_239,
inference(rat,[],[s246,s5575]) ).
cnf(s5589,plain,
~ spl24_753,
inference(rat,[],[s5385,s5558,s5534,s5490,s5481,s5575]) ).
cnf(s5591,plain,
~ spl24_214,
inference(rat,[],[s401,s5490,s5575]) ).
cnf(s5594,plain,
~ spl24_237,
inference(rat,[],[s257,s84,s5580]) ).
cnf(s5599,plain,
~ spl24_1626,
inference(rat,[],[s3880,s5585]) ).
cnf(s5608,plain,
~ spl24_266,
inference(rat,[],[s858,s5591]) ).
cnf(s5610,plain,
~ spl24_190,
inference(rat,[],[s360,s5496,s5591]) ).
cnf(s5615,plain,
~ spl24_910,
inference(rat,[],[s3680,s5488,s5594]) ).
cnf(s5629,plain,
~ spl24_1511,
inference(rat,[],[s4672,s5540,s5479,s5608]) ).
cnf(s5638,plain,
~ spl24_101,
inference(rat,[],[s666,s5610]) ).
cnf(s5642,plain,
~ spl24_494,
inference(rat,[],[s5402,s5615]) ).
cnf(s5660,plain,
~ spl24_6,
inference(rat,[],[s668,s5638]) ).
cnf(s5667,plain,
~ spl24_1634,
inference(rat,[],[s5265,s5589,s5642]) ).
cnf(s5668,plain,
~ spl24_1509,
inference(rat,[],[s4443,s5519,s5468,s5642]) ).
cnf(s5670,plain,
spl24_495,
inference(rat,[],[s628,s5642]) ).
cnf(s5684,plain,
~ spl24_1494,
inference(rat,[],[s4427,s5668]) ).
cnf(s5687,plain,
spl24_1495,
inference(rat,[],[s4422,s45,s5684]) ).
cnf(s5692,plain,
spl24_1926,
inference(rat,[],[s4377,s5687]) ).
cnf(s5696,plain,
spl24_5,
inference(rat,[],[s3,s5660]) ).
cnf(s5700,plain,
~ spl24_657,
inference(rat,[],[s4367,s5519,s5696]) ).
cnf(s5701,plain,
~ spl24_661,
inference(rat,[],[s4360,s5468,s5696]) ).
cnf(s5702,plain,
~ spl24_499,
inference(rat,[],[s4327,s5642,s5696]) ).
cnf(s5708,plain,
~ spl24_1934,
inference(rat,[],[s4375,s5519,s5700]) ).
cnf(s5710,plain,
~ spl24_756,
inference(rat,[],[s2979,s5477,s5701]) ).
cnf(s5711,plain,
~ spl24_500,
inference(rat,[],[s631,s5670,s5702]) ).
cnf(s5715,plain,
~ spl24_1927,
inference(rat,[],[s4639,s5708,s5710]) ).
cnf(s5718,plain,
~ spl24_648,
inference(rat,[],[s4318,s5715,s5696,s5711]) ).
cnf(s5733,plain,
spl24_21,
inference(rat,[],[s11,s186]) ).
cnf(s5736,plain,
~ spl24_1374,
inference(rat,[],[s5192,s5502,s5733]) ).
cnf(s5741,plain,
spl24_1375,
inference(rat,[],[s2936,s5502,s5736]) ).
cnf(s5744,plain,
~ spl24_206,
inference(rat,[],[s5093,s5575,s5502,s5490,s84,s5741]) ).
cnf(s5746,plain,
~ spl24_1514,
inference(rat,[],[s5025,s5529,s5473,s5744]) ).
cnf(s5751,plain,
~ spl24_249,
inference(rat,[],[s268,s5744]) ).
cnf(s5762,plain,
~ spl24_873,
inference(rat,[],[s4568,s5476,s5751]) ).
cnf(s5774,plain,
spl24_874,
inference(rat,[],[s1225,s5751,s5762]) ).
cnf(s5781,plain,
~ spl24_366,
inference(rat,[],[s1243,s5575,s5490,s5481,s5774]) ).
cnf(s5785,plain,
~ spl24_1531,
inference(rat,[],[s5227,s5537,s5781]) ).
cnf(s5789,plain,
~ spl24_1504,
inference(rat,[],[s5198,s5667,s5495,s5785]) ).
cnf(s5793,plain,
spl24_1503,
inference(rat,[],[s3337,s3338,s5718,s5789]) ).
cnf(s5794,plain,
spl24_1498,
inference(rat,[],[s4986,s5793]) ).
cnf(s5795,plain,
~ spl24_1510,
inference(rat,[],[s3352,s5629,s5793]) ).
cnf(s5801,plain,
( spl24_1547
| ~ spl24_1631 ),
inference(rat,[],[s4919,s3666,s5570,s5795,s5793]) ).
cnf(s5802,plain,
~ spl24_1631,
inference(rat,[],[s3888,s3667,s3668,s5801,s5599]) ).
cnf(s5804,plain,
~ spl24_1918,
inference(rat,[],[s4306,s5570,s5563,s5802]) ).
cnf(s5805,plain,
spl24_1506,
inference(rat,[],[s4988,s5794,s5570,s5802]) ).
cnf(s5807,plain,
~ spl24_1547,
inference(rat,[],[s4411,s5563,s5804]) ).
cnf(s5808,plain,
spl24_1628,
inference(rat,[],[s4998,s5692,s5591,s5481,s5805]) ).
cnf(s5809,plain,
spl24_1624,
inference(rat,[],[s3666,s5793,s5807]) ).
cnf(s5810,plain,
$false,
inference(rat,[],[s3671,s5807,s5746,s5808,s5809]) ).
fof(f101711,plain,
$false,
inference(avatar_sat_refutation,[],[s5810]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV553+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n007.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 28 06:32:27 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 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
% 12.51/2.61 % (2185817)Detected formulas, will run a generic FOF schedule.
% 12.51/2.61 % (2185822)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=2784768792:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.51/2.61 % (2185828)dis-21_1_sil=8000:lcm=predicate:random_seed=4239607428: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)
% 12.51/2.61 % (2185825)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=80706650:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.51/2.61 % (2185826)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3971189054:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.51/2.61 % (2185827)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1102336682:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.51/2.61 % (2185824)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=2907038845:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.51/2.61 % (2185823)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=4099872125:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.51/2.61 % (2185825)Refutation not found, incomplete strategy
% 12.51/2.61 % (2185825)------------------------------
% 12.51/2.61 % (2185825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.61 % (2185825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.61 % (2185825)CaDiCaL version: 2.1.3
% 12.51/2.61 % (2185825)Termination reason: Refutation not found, incomplete strategy
% 12.51/2.61 % (2185825)Time elapsed: 0.002 s
% 12.51/2.61 % (2185825)Peak memory usage: 88 MB
% 12.51/2.61 % (2185825)Instructions burned: 1 (million)
% 12.51/2.61 % (2185828)Instruction limit reached!
% 12.51/2.61 % (2185828)------------------------------
% 12.51/2.61 % (2185828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.61 % (2185828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.61 % (2185828)CaDiCaL version: 2.1.3
% 12.51/2.61 % (2185828)Termination reason: Instruction limit
% 12.51/2.61 % (2185828)Termination phase: Saturation
% 12.51/2.61 % (2185828)Time elapsed: 0.066 s
% 12.51/2.61 % (2185828)Peak memory usage: 88 MB
% 12.51/2.61 % (2185828)Instructions burned: 131 (million)
% 12.51/2.61 % (2185826)Instruction limit reached!
% 12.51/2.61 % (2185826)------------------------------
% 12.51/2.61 % (2185826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.61 % (2185826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.61 % (2185826)CaDiCaL version: 2.1.3
% 12.51/2.61 % (2185826)Termination reason: Instruction limit
% 12.51/2.61 % (2185826)Termination phase: Saturation
% 12.51/2.61 % (2185826)Time elapsed: 0.077 s
% 12.51/2.61 % (2185826)Peak memory usage: 88 MB
% 12.51/2.61 % (2185826)Instructions burned: 121 (million)
% 12.51/2.61 % (2185827)Instruction limit reached!
% 12.51/2.61 % (2185827)------------------------------
% 12.51/2.61 % (2185827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.61 % (2185827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.61 % (2185827)CaDiCaL version: 2.1.3
% 12.51/2.61 % (2185827)Termination reason: Instruction limit
% 12.51/2.61 % (2185827)Termination phase: Saturation
% 12.51/2.61 % (2185827)Time elapsed: 0.092 s
% 12.51/2.61 % (2185827)Peak memory usage: 89 MB
% 12.51/2.61 % (2185827)Instructions burned: 140 (million)
% 12.51/2.61 % (2185836)lrs+10_1_sil=8000:sp=occurrence:random_seed=116162962:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.51/2.61 % (2185838)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1752611081:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 12.51/2.61 % (2185837)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3235180735:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.51/2.61 % (2185825)------------------------------
% 12.51/2.61 % (2185825)------------------------------
% 12.51/2.61 % (2185838)Refutation not found, incomplete strategy
% 12.51/2.61 % (2185838)------------------------------
% 12.51/2.61 % (2185838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.99/3.87 % (2185838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.99/3.87 % (2185838)CaDiCaL version: 2.1.3
% 20.99/3.87 % (2185838)Termination reason: Refutation not found, incomplete strategy
% 20.99/3.87 % (2185838)Time elapsed: 0.007 s
% 20.99/3.87 % (2185838)Peak memory usage: 88 MB
% 20.99/3.87 % (2185838)Instructions burned: 12 (million)
% 20.99/3.87 % (2185837)Instruction limit reached!
% 20.99/3.87 % (2185837)------------------------------
% 20.99/3.87 % (2185837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.99/3.87 % (2185837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.99/3.87 % (2185837)CaDiCaL version: 2.1.3
% 20.99/3.87 % (2185837)Termination reason: Instruction limit
% 20.99/3.87 % (2185837)Termination phase: Saturation
% 20.99/3.87 % (2185837)Time elapsed: 0.082 s
% 20.99/3.87 % (2185837)Peak memory usage: 90 MB
% 20.99/3.87 % (2185837)Instructions burned: 159 (million)
% 20.99/3.87 % (2185836)Instruction limit reached!
% 20.99/3.87 % (2185836)------------------------------
% 20.99/3.87 % (2185836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.99/3.87 % (2185836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.99/3.87 % (2185836)CaDiCaL version: 2.1.3
% 20.99/3.87 % (2185836)Termination reason: Instruction limit
% 20.99/3.87 % (2185836)Termination phase: Saturation
% 20.99/3.87 % (2185836)Time elapsed: 0.181 s
% 20.99/3.87 % (2185836)Peak memory usage: 92 MB
% 20.99/3.87 % (2185836)Instructions burned: 286 (million)
% 20.99/3.87 % (2185842)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=904187880:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 20.99/3.87 % (2185843)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=564479715:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 20.99/3.87 % (2185843)Refutation not found, incomplete strategy
% 20.99/3.87 % (2185843)------------------------------
% 20.99/3.87 % (2185843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.99/3.87 % (2185843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.99/3.87 % (2185843)CaDiCaL version: 2.1.3
% 20.99/3.87 % (2185843)Termination reason: Refutation not found, incomplete strategy
% 20.99/3.87 % (2185843)Time elapsed: 0.002 s
% 20.99/3.87 % (2185843)Peak memory usage: 88 MB
% 20.99/3.87 % (2185843)Instructions burned: 1 (million)
% 20.99/3.87 % (2185838)------------------------------
% 20.99/3.87 % (2185838)------------------------------
% 20.99/3.87 % (2185844)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2644846416:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 20.99/3.87 % (2185842)Instruction limit reached!
% 20.99/3.87 % (2185842)------------------------------
% 20.99/3.87 % (2185842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.99/3.87 % (2185842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.99/3.87 % (2185842)CaDiCaL version: 2.1.3
% 20.99/3.87 % (2185842)Termination reason: Instruction limit
% 20.99/3.87 % (2185842)Termination phase: Saturation
% 20.99/3.87 % (2185842)Time elapsed: 0.141 s
% 20.99/3.87 % (2185842)Peak memory usage: 91 MB
% 20.99/3.87 % (2185842)Instructions burned: 248 (million)
% 20.99/3.87 % (2185847)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3004204966:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 20.99/3.87 % (2185847)Instruction limit reached!
% 20.99/3.87 % (2185847)------------------------------
% 20.99/3.87 % (2185847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.99/3.87 % (2185847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.99/3.87 % (2185847)CaDiCaL version: 2.1.3
% 20.99/3.87 % (2185847)Termination reason: Instruction limit
% 20.99/3.87 % (2185847)Termination phase: Saturation
% 20.99/3.87 % (2185847)Time elapsed: 0.063 s
% 20.99/3.87 % (2185847)Peak memory usage: 89 MB
% 20.99/3.87 % (2185847)Instructions burned: 114 (million)
% 20.99/3.87 % (2185843)------------------------------
% 20.99/3.87 % (2185843)------------------------------
% 20.99/3.87 % (2185849)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2055293024:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 20.99/3.87 % (2185849)Instruction limit reached!
% 20.99/3.87 % (2185849)------------------------------
% 20.99/3.87 % (2185849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.19/4.63 % (2185849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.19/4.63 % (2185849)CaDiCaL version: 2.1.3
% 23.19/4.63 % (2185849)Termination reason: Instruction limit
% 23.19/4.63 % (2185849)Termination phase: Saturation
% 23.19/4.63 % (2185849)Time elapsed: 0.057 s
% 23.19/4.63 % (2185849)Peak memory usage: 88 MB
% 23.19/4.63 % (2185849)Instructions burned: 128 (million)
% 23.19/4.63 % (2185851)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2700435620:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 23.19/4.63 % (2185853)lrs+10_1_sil=8000:sp=occurrence:random_seed=686733808:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 23.19/4.63 % (2185851)Instruction limit reached!
% 23.19/4.63 % (2185851)------------------------------
% 23.19/4.63 % (2185851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.19/4.63 % (2185851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.19/4.63 % (2185851)CaDiCaL version: 2.1.3
% 23.19/4.63 % (2185851)Termination reason: Instruction limit
% 23.19/4.63 % (2185851)Termination phase: Saturation
% 23.19/4.63 % (2185851)Time elapsed: 0.053 s
% 23.19/4.63 % (2185851)Peak memory usage: 88 MB
% 23.19/4.63 % (2185851)Instructions burned: 116 (million)
% 23.19/4.63 % (2185854)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2242476234:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 23.19/4.63 % (2185854)Refutation not found, incomplete strategy
% 23.19/4.63 % (2185854)------------------------------
% 23.19/4.63 % (2185854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.19/4.63 % (2185854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.19/4.63 % (2185854)CaDiCaL version: 2.1.3
% 23.19/4.63 % (2185854)Termination reason: Refutation not found, incomplete strategy
% 23.19/4.63 % (2185854)Time elapsed: 0.002 s
% 23.19/4.63 % (2185854)Peak memory usage: 88 MB
% 23.19/4.63 % (2185854)Instructions burned: 1 (million)
% 23.19/4.63 % (2185857)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3556296976:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 23.19/4.63 % (2185854)------------------------------
% 23.19/4.63 % (2185854)------------------------------
% 23.19/4.63 % (2185860)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3360012765:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 23.19/4.63 % (2185853)Instruction limit reached!
% 23.19/4.63 % (2185853)------------------------------
% 23.19/4.63 % (2185853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.19/4.63 % (2185853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.19/4.63 % (2185853)CaDiCaL version: 2.1.3
% 23.19/4.63 % (2185853)Termination reason: Instruction limit
% 23.19/4.63 % (2185853)Termination phase: Saturation
% 23.19/4.63 % (2185853)Time elapsed: 0.554 s
% 23.19/4.63 % (2185853)Peak memory usage: 97 MB
% 23.19/4.63 % (2185853)Instructions burned: 908 (million)
% 23.19/4.63 % (2185860)Instruction limit reached!
% 23.19/4.63 % (2185860)------------------------------
% 23.19/4.63 % (2185860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.19/4.63 % (2185860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.19/4.63 % (2185860)CaDiCaL version: 2.1.3
% 23.19/4.63 % (2185860)Termination reason: Instruction limit
% 23.19/4.63 % (2185860)Termination phase: Saturation
% 23.19/4.63 % (2185860)Time elapsed: 0.070 s
% 23.19/4.63 % (2185860)Peak memory usage: 90 MB
% 23.19/4.63 % (2185860)Instructions burned: 136 (million)
% 23.19/4.63 % (2185862)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1190063318:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 23.19/4.63 % (2185863)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=709235461:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 23.19/4.63 % (2185862)Refutation not found, incomplete strategy
% 23.19/4.63 % (2185862)------------------------------
% 23.19/4.63 % (2185862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.19/4.63 % (2185862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.19/4.63 % (2185862)CaDiCaL version: 2.1.3
% 23.19/4.63 % (2185862)Termination reason: Refutation not found, incomplete strategy
% 23.19/4.63 % (2185862)Time elapsed: 0.002 s
% 23.19/4.63 % (2185862)Peak memory usage: 88 MB
% 23.19/4.63 % (2185862)Instructions burned: 1 (million)
% 23.19/4.63 % (2185862)------------------------------
% 23.19/4.63 % (2185862)------------------------------
% 23.19/4.63 % (2185866)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1892818194:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 23.19/4.63 % (2185866)Instruction limit reached!
% 23.19/4.63 % (2185866)------------------------------
% 23.19/4.63 % (2185866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.19/4.63 % (2185866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.19/4.63 % (2185866)CaDiCaL version: 2.1.3
% 23.19/4.63 % (2185866)Termination reason: Instruction limit
% 23.19/4.63 % (2185866)Termination phase: Saturation
% 23.19/4.63 % (2185866)Time elapsed: 0.077 s
% 23.19/4.63 % (2185866)Peak memory usage: 90 MB
% 23.19/4.63 % (2185866)Instructions burned: 127 (million)
% 23.19/4.63 % (2185844)Instruction limit reached!
% 23.19/4.63 % (2185844)------------------------------
% 23.19/4.63 % (2185844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.19/4.63 % (2185844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.19/4.63 % (2185844)CaDiCaL version: 2.1.3
% 23.19/4.63 % (2185844)Termination reason: Instruction limit
% 23.19/4.63 % (2185844)Termination phase: Saturation
% 23.19/4.63 % (2185844)Time elapsed: 1.560 s
% 23.19/4.63 % (2185844)Peak memory usage: 143 MB
% 23.19/4.63 % (2185844)Instructions burned: 2350 (million)
% 23.19/4.63 % (2185868)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2227718755:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 23.19/4.63 % (2185869)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=695661639:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 23.19/4.63 % (2185869)Refutation not found, incomplete strategy
% 23.19/4.63 % (2185869)------------------------------
% 23.19/4.63 % (2185869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.19/4.63 % (2185869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.19/4.63 % (2185869)CaDiCaL version: 2.1.3
% 23.19/4.63 % (2185869)Termination reason: Refutation not found, incomplete strategy
% 23.19/4.63 % (2185869)Time elapsed: 0.002 s
% 23.19/4.63 % (2185869)Peak memory usage: 88 MB
% 23.19/4.63 % (2185869)Instructions burned: 2 (million)
% 23.19/4.63 % (2185868)Instruction limit reached!
% 23.19/4.63 % (2185868)------------------------------
% 23.19/4.63 % (2185868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.19/4.63 % (2185868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.19/4.63 % (2185868)CaDiCaL version: 2.1.3
% 23.19/4.63 % (2185868)Termination reason: Instruction limit
% 23.19/4.63 % (2185868)Termination phase: Saturation
% 23.19/4.63 % (2185868)Time elapsed: 0.056 s
% 23.19/4.63 % (2185868)Peak memory usage: 89 MB
% 23.19/4.63 % (2185868)Instructions burned: 134 (million)
% 23.19/4.63 % (2185872)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1189241977:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/431Mi)
% 23.19/4.63 % (2185872)Refutation not found, incomplete strategy
% 23.19/4.63 % (2185872)------------------------------
% 23.19/4.63 % (2185872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.19/4.63 % (2185872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.19/4.63 % (2185872)CaDiCaL version: 2.1.3
% 23.19/4.63 % (2185872)Termination reason: Refutation not found, incomplete strategy
% 23.19/4.63 % (2185872)Time elapsed: 0.002 s
% 23.19/4.63 % (2185872)Peak memory usage: 88 MB
% 23.19/4.63 % (2185872)Instructions burned: 1 (million)
% 23.19/4.63 % (2185869)------------------------------
% 23.19/4.63 % (2185869)------------------------------
% 23.19/4.63 % (2185872)------------------------------
% 23.19/4.63 % (2185872)------------------------------
% 23.19/4.63 % (2185874)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=234086851:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 23.19/4.63 % (2185876)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=4161479343:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2971 on theBenchmark for (2971ds/150Mi)
% 23.19/4.63 % (2185876)Instruction limit reached!
% 23.19/4.63 % (2185876)------------------------------
% 23.19/4.63 % (2185876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.19/4.63 % (2185876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.19/4.63 % (2185876)CaDiCaL version: 2.1.3
% 23.19/4.63 % (2185876)Termination reason: Instruction limit
% 23.19/4.63 % (2185876)Termination phase: Saturation
% 23.19/4.63 % (2185876)Time elapsed: 0.088 s
% 23.19/4.63 % (2185876)Peak memory usage: 91 MB
% 23.19/4.63 % (2185876)Instructions burned: 151 (million)
% 23.19/4.63 % (2185878)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3061424909:i=14155:bd=all_2968 on theBenchmark for (2968ds/14155Mi)
% 23.19/4.63 % (2185822)First to succeed.
% 23.19/4.63 % (2185822)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2185817"
% 23.19/4.63 % (2185822)Refutation found. Thanks to Tanya!
% 23.19/4.63 % SZS status Theorem for theBenchmark
% 23.19/4.63 % SZS output start Proof for theBenchmark
% See solution above
% 27.34/4.83 % (2185822)------------------------------
% 27.34/4.83 % (2185822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.34/4.83 % (2185822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.34/4.83 % (2185822)CaDiCaL version: 2.1.3
% 27.34/4.83 % (2185822)Termination reason: Refutation
% 27.34/4.83 % (2185822)Time elapsed: 3.459 s
% 27.34/4.83 % (2185822)Peak memory usage: 204 MB
% 27.34/4.83 % (2185822)Instructions burned: 9522 (million)
% 27.34/4.83 % (2185822)------------------------------
% 27.34/4.83 % (2185822)------------------------------
% 27.34/4.83 % (2185817)Success in time 3.781 s
% 27.34/4.83 % Vampire exiting
%------------------------------------------------------------------------------