%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV550+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:58:18 PM UTC 2026
% Result : Theorem 10.67s 2.46s
% Output : Refutation 11.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 84
% Syntax : Number of formulae : 778 ( 87 unt; 72 def)
% Number of atoms : 2116 ( 257 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 2262 ( 924 ~;1226 |; 32 &)
% ( 74 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 73 ( 71 usr; 67 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-2 aty)
% Number of variables : 254 ( 0 sgn 243 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( subq(X0,X1)
<=> ! [X2] :
( mem(X2,X0)
=> mem(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subq_def) ).
fof(f2,axiom,
! [X0,X1] :
( subq(X0,X1)
=> ( subq(X1,X0)
=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',setext) ).
fof(f4,axiom,
! [X0] : ~ mem(X0,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_ax) ).
fof(f5,axiom,
! [X0,X1] :
( mem(X0,s(X1))
<=> X0 = X1 ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',u_ax) ).
fof(f8,axiom,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_def) ).
fof(f9,axiom,
! [X0] : n(X0) = a(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',n_def) ).
fof(f10,axiom,
! [X0,X1] :
( mem(X0,p(X1))
<=> subq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p_ax) ).
fof(f11,axiom,
! [X0] :
( atleast2p(X0)
<=> ? [X1] :
( mem(X1,X0)
& ~ subq(X0,p(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',atleast2p_def) ).
fof(f12,axiom,
! [X0] :
( atleast3p(X0)
<=> ? [X1] :
( subq(X1,X0)
& atleast2p(X1)
& ~ subq(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',atleast3p_def) ).
fof(f13,axiom,
! [X0] :
( atleast4p(X0)
<=> ? [X1] :
( subq(X1,X0)
& atleast3p(X1)
& ~ subq(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',atleast4p_def) ).
fof(f26,conjecture,
~ atleast4p(u(n(e),n(s(n(e))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',atmost3_7) ).
fof(f27,negated_conjecture,
~ ~ atleast4p(u(n(e),n(s(n(e))))),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f28,plain,
atleast4p(u(n(e),n(s(n(e))))),
inference(flattening,[],[f27]) ).
fof(f29,plain,
! [X0] :
( atleast4p(X0)
=> ? [X1] :
( subq(X1,X0)
& atleast3p(X1)
& ~ subq(X0,X1) ) ),
inference(unused_predicate_definition_removal,[],[f13]) ).
fof(f30,plain,
! [X0] :
( atleast3p(X0)
=> ? [X1] :
( subq(X1,X0)
& atleast2p(X1)
& ~ subq(X0,X1) ) ),
inference(unused_predicate_definition_removal,[],[f12]) ).
fof(f31,plain,
! [X0] :
( atleast2p(X0)
=> ? [X1] :
( mem(X1,X0)
& ~ subq(X0,p(X1)) ) ),
inference(unused_predicate_definition_removal,[],[f11]) ).
fof(f32,plain,
! [X0,X1] :
( subq(X0,X1)
<=> ! [X2] :
( mem(X2,X1)
| ~ mem(X2,X0) ) ),
inference(ennf_transformation,[],[f1]) ).
fof(f33,plain,
! [X0,X1] :
( X0 = X1
| ~ subq(X1,X0)
| ~ subq(X0,X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f34,plain,
! [X0,X1] :
( X0 = X1
| ~ subq(X1,X0)
| ~ subq(X0,X1) ),
inference(flattening,[],[f33]) ).
fof(f35,plain,
! [X0] :
( ? [X1] :
( mem(X1,X0)
& ~ subq(X0,p(X1)) )
| ~ atleast2p(X0) ),
inference(ennf_transformation,[],[f31]) ).
fof(f36,plain,
! [X0] :
( ? [X1] :
( subq(X1,X0)
& atleast2p(X1)
& ~ subq(X0,X1) )
| ~ atleast3p(X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f37,plain,
! [X0] :
( ? [X1] :
( subq(X1,X0)
& atleast3p(X1)
& ~ subq(X0,X1) )
| ~ atleast4p(X0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f38,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,[],[f32]) ).
fof(f39,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,[],[f38]) ).
fof(f40,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))],[f39]) ).
fof(f41,plain,
! [X0,X1] :
( ( mem(X0,s(X1))
| X0 != X1 )
& ( X0 = X1
| ~ mem(X0,s(X1)) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f42,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(f43,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,[],[f42]) ).
fof(f46,plain,
! [X0,X1] :
( ( mem(X0,p(X1))
| ~ subq(X0,X1) )
& ( subq(X0,X1)
| ~ mem(X0,p(X1)) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f47,plain,
! [X0] :
( ( mem(sK1(X0),X0)
& ~ subq(X0,p(sK1(X0))) )
| ~ atleast2p(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X1,sK1(X0))],[f35]) ).
fof(f48,plain,
! [X0] :
( ( subq(sK2(X0),X0)
& atleast2p(sK2(X0))
& ~ subq(X0,sK2(X0)) )
| ~ atleast3p(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X1,sK2(X0))],[f36]) ).
fof(f49,plain,
! [X0] :
( ( subq(sK3(X0),X0)
& atleast3p(sK3(X0))
& ~ subq(X0,sK3(X0)) )
| ~ atleast4p(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X1,sK3(X0))],[f37]) ).
fof(f50,plain,
! [X3,X0,X1] :
( ~ mem(X3,X0)
| mem(X3,X1)
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
fof(f51,plain,
! [X0,X1] :
( mem(sK0(X0,X1),X0)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
fof(f52,plain,
! [X0,X1] :
( ~ mem(sK0(X0,X1),X1)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
fof(f53,plain,
! [X0,X1] :
( ~ subq(X1,X0)
| X0 = X1
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f54,plain,
! [X0] : ~ mem(X0,e),
inference(cnf_transformation,[],[f4]) ).
fof(f55,plain,
! [X0,X1] :
( ~ mem(X0,s(X1))
| X0 = X1 ),
inference(cnf_transformation,[],[f41]) ).
fof(f56,plain,
! [X0,X1] :
( mem(X0,s(X1))
| X0 != X1 ),
inference(cnf_transformation,[],[f41]) ).
fof(f57,plain,
! [X2,X0,X1] :
( ~ mem(X0,u(X1,X2))
| mem(X0,X2)
| mem(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f58,plain,
! [X2,X0,X1] :
( mem(X0,u(X1,X2))
| ~ mem(X0,X2) ),
inference(cnf_transformation,[],[f43]) ).
fof(f59,plain,
! [X2,X0,X1] :
( mem(X0,u(X1,X2))
| ~ mem(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f63,plain,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
inference(cnf_transformation,[],[f8]) ).
fof(f64,plain,
! [X0] : n(X0) = a(X0,X0),
inference(cnf_transformation,[],[f9]) ).
fof(f65,plain,
! [X0,X1] :
( ~ mem(X0,p(X1))
| subq(X0,X1) ),
inference(cnf_transformation,[],[f46]) ).
fof(f66,plain,
! [X0,X1] :
( mem(X0,p(X1))
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f46]) ).
fof(f67,plain,
! [X0] :
( ~ subq(X0,p(sK1(X0)))
| ~ atleast2p(X0) ),
inference(cnf_transformation,[],[f47]) ).
fof(f68,plain,
! [X0] :
( mem(sK1(X0),X0)
| ~ atleast2p(X0) ),
inference(cnf_transformation,[],[f47]) ).
fof(f69,plain,
! [X0] :
( ~ subq(X0,sK2(X0))
| ~ atleast3p(X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f70,plain,
! [X0] :
( atleast2p(sK2(X0))
| ~ atleast3p(X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f71,plain,
! [X0] :
( subq(sK2(X0),X0)
| ~ atleast3p(X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f72,plain,
! [X0] :
( ~ subq(X0,sK3(X0))
| ~ atleast4p(X0) ),
inference(cnf_transformation,[],[f49]) ).
fof(f73,plain,
! [X0] :
( atleast3p(sK3(X0))
| ~ atleast4p(X0) ),
inference(cnf_transformation,[],[f49]) ).
fof(f74,plain,
! [X0] :
( subq(sK3(X0),X0)
| ~ atleast4p(X0) ),
inference(cnf_transformation,[],[f49]) ).
fof(f75,plain,
atleast4p(u(n(e),n(s(n(e))))),
inference(cnf_transformation,[],[f28]) ).
fof(f76,plain,
! [X0] : n(X0) = u(X0,s(X0)),
inference(definition_unfolding,[],[f64,f63]) ).
fof(f77,plain,
atleast4p(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),
inference(definition_unfolding,[],[f75,f76,f76,f76]) ).
fof(f78,plain,
! [X1] : mem(X1,s(X1)),
inference(equality_resolution,[],[f56]) ).
fof(f79,definition,
sF4 = s(e),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f80,plain,
s(e) = sF4,
inference(reorient_equations,[],[f79]) ).
fof(f81,definition,
sF5 = u(e,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f82,plain,
u(e,sF4) = sF5,
inference(reorient_equations,[],[f81]) ).
fof(f83,definition,
sF6 = s(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f84,plain,
s(sF5) = sF6,
inference(reorient_equations,[],[f83]) ).
fof(f85,definition,
sF7 = s(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f86,plain,
s(sF6) = sF7,
inference(reorient_equations,[],[f85]) ).
fof(f87,definition,
sF8 = u(sF6,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f88,plain,
u(sF6,sF7) = sF8,
inference(reorient_equations,[],[f87]) ).
fof(f89,definition,
sF9 = u(sF5,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f90,plain,
u(sF5,sF8) = sF9,
inference(reorient_equations,[],[f89]) ).
fof(f91,plain,
atleast4p(sF9),
inference(definition_folding,[],[f77,f90,f88,f86,f84,f82,f80,f84,f82,f80,f82,f80]) ).
fof(f92,plain,
mem(e,sF4),
inference(superposition,[],[f78,f80]) ).
fof(f93,plain,
mem(sF5,sF6),
inference(superposition,[],[f78,f84]) ).
fof(f96,plain,
! [X0] :
( ~ mem(X0,sF4)
| e = X0 ),
inference(superposition,[],[f55,f80]) ).
fof(f97,plain,
! [X0] :
( ~ mem(X0,sF6)
| sF5 = X0 ),
inference(superposition,[],[f55,f84]) ).
fof(f98,plain,
! [X0] :
( ~ mem(X0,sF7)
| sF6 = X0 ),
inference(superposition,[],[f55,f86]) ).
fof(f100,plain,
! [X0] :
( ~ mem(X0,sF4)
| mem(X0,sF5) ),
inference(superposition,[],[f58,f82]) ).
fof(f102,plain,
! [X0] :
( ~ mem(X0,sF5)
| mem(X0,sF9) ),
inference(superposition,[],[f59,f90]) ).
fof(f104,plain,
! [X0] :
( ~ mem(X0,sF6)
| mem(X0,sF8) ),
inference(superposition,[],[f59,f88]) ).
fof(f106,plain,
mem(e,sF5),
inference(resolution,[],[f100,f92]) ).
fof(f109,plain,
! [X0] :
( ~ mem(X0,sF9)
| mem(X0,sF8)
| mem(X0,sF5) ),
inference(superposition,[],[f57,f90]) ).
fof(f110,plain,
! [X0] :
( ~ mem(X0,sF5)
| mem(X0,sF4)
| mem(X0,e) ),
inference(superposition,[],[f57,f82]) ).
fof(f111,plain,
! [X0] :
( ~ mem(X0,sF8)
| mem(X0,sF7)
| mem(X0,sF6) ),
inference(superposition,[],[f57,f88]) ).
fof(f112,plain,
! [X0] :
( ~ mem(X0,sF5)
| mem(X0,sF4) ),
inference(forward_subsumption_resolution,[],[f110,f54]) ).
fof(f113,plain,
mem(sF5,sF8),
inference(resolution,[],[f104,f93]) ).
fof(f116,plain,
! [X0] : subq(e,X0),
inference(resolution,[],[f51,f54]) ).
fof(f117,plain,
! [X0,X1] :
( subq(s(X0),X1)
| sK0(s(X0),X1) = X0 ),
inference(resolution,[],[f51,f55]) ).
fof(f124,plain,
! [X0] :
( mem(sK0(sF9,X0),sF8)
| subq(sF9,X0)
| mem(sK0(sF9,X0),sF5) ),
inference(resolution,[],[f51,f109]) ).
fof(f127,plain,
mem(e,sF9),
inference(resolution,[],[f102,f106]) ).
fof(f132,plain,
! [X0] :
( subq(X0,X0)
| subq(X0,X0) ),
inference(resolution,[],[f52,f51]) ).
fof(f133,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X1)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f52,f59]) ).
fof(f134,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X2)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f52,f58]) ).
fof(f135,plain,
! [X0] : subq(X0,X0),
inference(duplicate_literal_removal,[],[f132]) ).
fof(f136,plain,
! [X0] :
( subq(sF7,X0)
| sF6 = sK0(sF7,X0) ),
inference(resolution,[],[f98,f51]) ).
fof(f138,plain,
! [X0] :
( subq(sF6,X0)
| sF5 = sK0(sF6,X0) ),
inference(resolution,[],[f97,f51]) ).
fof(f141,plain,
! [X0] :
( mem(sK0(sF5,X0),sF4)
| subq(sF5,X0) ),
inference(resolution,[],[f112,f51]) ).
fof(f144,plain,
! [X0] :
( ~ subq(X0,e)
| e = X0 ),
inference(resolution,[],[f53,f116]) ).
fof(f146,plain,
! [X0,X1] :
( ~ subq(s(X0),X1)
| mem(X0,X1) ),
inference(resolution,[],[f50,f78]) ).
fof(f152,plain,
! [X2,X0,X1] :
( mem(sK0(X0,X1),X2)
| ~ subq(X0,X2)
| subq(X0,X1) ),
inference(resolution,[],[f50,f51]) ).
fof(f153,plain,
! [X0] :
( ~ subq(sF6,X0)
| mem(sF5,X0) ),
inference(resolution,[],[f50,f93]) ).
fof(f160,plain,
( subq(sF5,sF4)
| subq(sF5,sF4) ),
inference(resolution,[],[f141,f52]) ).
fof(f161,plain,
! [X0] :
( subq(sF5,X0)
| e = sK0(sF5,X0) ),
inference(resolution,[],[f141,f96]) ).
fof(f164,plain,
subq(sF5,sF4),
inference(duplicate_literal_removal,[],[f160]) ).
fof(f165,plain,
! [X0] :
( ~ subq(X0,sF5)
| sF5 = X0
| e = sK0(sF5,X0) ),
inference(resolution,[],[f161,f53]) ).
fof(f176,plain,
( sF4 = sF5
| ~ subq(sF4,sF5) ),
inference(resolution,[],[f164,f53]) ).
fof(f178,definition,
( spl10_3
<=> subq(sF4,sF5) ),
introduced(definition,[new_symbols(definition,[spl10_3])],[avatar_definition]) ).
fof(f180,plain,
( ~ subq(sF4,sF5)
| spl10_3 ),
inference(avatar_component_clause,[],[f178]) ).
fof(f182,definition,
( spl10_4
<=> sF4 = sF5 ),
introduced(definition,[new_symbols(definition,[spl10_4])],[avatar_definition]) ).
fof(f184,plain,
( sF4 = sF5
| ~ spl10_4 ),
inference(avatar_component_clause,[],[f182]) ).
fof(f185,plain,
( ~ spl10_3
| spl10_4 ),
inference(avatar_split_clause,[],[f176,f182,f178]) ).
fof(f199,plain,
! [X2,X3,X0,X1] :
( ~ subq(X1,X3)
| subq(X0,X2)
| mem(sK0(X0,X2),X3)
| ~ subq(X0,X1) ),
inference(resolution,[],[f152,f50]) ).
fof(f200,plain,
! [X0,X1] :
( ~ subq(X0,e)
| subq(X0,X1) ),
inference(resolution,[],[f152,f54]) ).
fof(f212,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF7)
| subq(X0,X1)
| ~ subq(X0,sF8)
| mem(sK0(X0,X1),sF6) ),
inference(resolution,[],[f152,f111]) ).
fof(f213,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF8)
| subq(X0,X1)
| ~ subq(X0,sF9)
| mem(sK0(X0,X1),sF5) ),
inference(resolution,[],[f152,f109]) ).
fof(f216,plain,
! [X0,X1] :
( subq(X0,u(X1,X0))
| subq(X0,u(X1,X0)) ),
inference(resolution,[],[f134,f51]) ).
fof(f221,plain,
! [X0] :
( ~ mem(sK0(X0,sF9),sF8)
| subq(X0,sF9) ),
inference(superposition,[],[f134,f90]) ).
fof(f226,plain,
! [X0,X1] : subq(X0,u(X1,X0)),
inference(duplicate_literal_removal,[],[f216]) ).
fof(f233,plain,
subq(sF4,sF5),
inference(superposition,[],[f226,f82]) ).
fof(f234,plain,
subq(sF7,sF8),
inference(superposition,[],[f226,f88]) ).
fof(f235,plain,
( $false
| spl10_3 ),
inference(forward_subsumption_resolution,[],[f233,f180]) ).
fof(f236,plain,
spl10_3,
inference(avatar_contradiction_clause,[],[f235]) ).
fof(f239,plain,
( ! [X0] :
( ~ mem(X0,sF5)
| e = X0 )
| ~ spl10_4 ),
inference(superposition,[],[f96,f184]) ).
fof(f248,plain,
( sF7 = sF8
| ~ subq(sF8,sF7) ),
inference(resolution,[],[f234,f53]) ).
fof(f250,definition,
( spl10_5
<=> subq(sF8,sF7) ),
introduced(definition,[new_symbols(definition,[spl10_5])],[avatar_definition]) ).
fof(f252,plain,
( ~ subq(sF8,sF7)
| spl10_5 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f254,definition,
( spl10_6
<=> sF7 = sF8 ),
introduced(definition,[new_symbols(definition,[spl10_6])],[avatar_definition]) ).
fof(f256,plain,
( sF7 = sF8
| ~ spl10_6 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f257,plain,
( ~ spl10_5
| spl10_6 ),
inference(avatar_split_clause,[],[f248,f254,f250]) ).
fof(f258,plain,
! [X0,X1] :
( subq(sK0(p(X0),X1),X0)
| subq(p(X0),X1) ),
inference(resolution,[],[f65,f51]) ).
fof(f273,plain,
! [X0] :
( ~ mem(sK0(X0,sF9),sF5)
| subq(X0,sF9) ),
inference(superposition,[],[f133,f90]) ).
fof(f305,plain,
! [X0,X1] :
( mem(sK1(X0),X1)
| ~ atleast2p(X0)
| ~ subq(X0,X1) ),
inference(resolution,[],[f68,f50]) ).
fof(f315,plain,
( ~ atleast2p(sF6)
| sF5 = sK1(sF6) ),
inference(resolution,[],[f68,f97]) ).
fof(f317,plain,
( ~ atleast2p(sF7)
| sF6 = sK1(sF7) ),
inference(resolution,[],[f68,f98]) ).
fof(f358,definition,
( spl10_17
<=> atleast2p(sF7) ),
introduced(definition,[new_symbols(definition,[spl10_17])],[avatar_definition]) ).
fof(f359,plain,
( atleast2p(sF7)
| ~ spl10_17 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f360,plain,
( ~ atleast2p(sF7)
| spl10_17 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f363,definition,
( spl10_18
<=> sF6 = sK1(sF7) ),
introduced(definition,[new_symbols(definition,[spl10_18])],[avatar_definition]) ).
fof(f365,plain,
( sF6 = sK1(sF7)
| ~ spl10_18 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f366,plain,
( spl10_18
| ~ spl10_17 ),
inference(avatar_split_clause,[],[f317,f358,f363]) ).
fof(f372,definition,
( spl10_20
<=> atleast2p(sF6) ),
introduced(definition,[new_symbols(definition,[spl10_20])],[avatar_definition]) ).
fof(f373,plain,
( atleast2p(sF6)
| ~ spl10_20 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f374,plain,
( ~ atleast2p(sF6)
| spl10_20 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f377,definition,
( spl10_21
<=> sF5 = sK1(sF6) ),
introduced(definition,[new_symbols(definition,[spl10_21])],[avatar_definition]) ).
fof(f379,plain,
( sF5 = sK1(sF6)
| ~ spl10_21 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f380,plain,
( spl10_21
| ~ spl10_20 ),
inference(avatar_split_clause,[],[f315,f372,f377]) ).
fof(f386,definition,
( spl10_23
<=> atleast2p(sF5) ),
introduced(definition,[new_symbols(definition,[spl10_23])],[avatar_definition]) ).
fof(f387,plain,
( atleast2p(sF5)
| ~ spl10_23 ),
inference(avatar_component_clause,[],[f386]) ).
fof(f388,plain,
( ~ atleast2p(sF5)
| spl10_23 ),
inference(avatar_component_clause,[],[f386]) ).
fof(f401,plain,
! [X0] :
( ~ subq(X0,sF7)
| sF7 = X0
| sF6 = sK0(sF7,X0) ),
inference(resolution,[],[f136,f53]) ).
fof(f413,plain,
! [X0,X1] :
( mem(X0,X1)
| sK0(s(X0),X1) = X0 ),
inference(resolution,[],[f146,f117]) ).
fof(f420,plain,
! [X0] : sK0(s(X0),e) = X0,
inference(resolution,[],[f413,f54]) ).
fof(f442,plain,
e = sK0(sF4,e),
inference(superposition,[],[f420,f80]) ).
fof(f448,plain,
( e = sK0(sF5,e)
| ~ spl10_4 ),
inference(forward_demodulation,[],[f442,f184]) ).
fof(f486,plain,
! [X0] :
( ~ atleast2p(s(X0))
| sK0(s(X0),p(sK1(s(X0)))) = X0 ),
inference(resolution,[],[f67,f117]) ).
fof(f546,plain,
! [X0] :
( subq(p(e),X0)
| e = sK0(p(e),X0) ),
inference(resolution,[],[f144,f258]) ).
fof(f607,definition,
( spl10_41
<=> mem(e,sF6) ),
introduced(definition,[new_symbols(definition,[spl10_41])],[avatar_definition]) ).
fof(f608,plain,
( ~ mem(e,sF6)
| spl10_41 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f609,plain,
( mem(e,sF6)
| ~ spl10_41 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f615,definition,
( spl10_43
<=> e = sK0(sF5,sF8) ),
introduced(definition,[new_symbols(definition,[spl10_43])],[avatar_definition]) ).
fof(f617,plain,
( e = sK0(sF5,sF8)
| ~ spl10_43 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f629,definition,
( spl10_46
<=> e = sF6 ),
introduced(definition,[new_symbols(definition,[spl10_46])],[avatar_definition]) ).
fof(f630,plain,
( e != sF6
| spl10_46 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f631,plain,
( e = sF6
| ~ spl10_46 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f639,definition,
( spl10_48
<=> e = sF5 ),
introduced(definition,[new_symbols(definition,[spl10_48])],[avatar_definition]) ).
fof(f640,plain,
( e != sF5
| spl10_48 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f641,plain,
( e = sF5
| ~ spl10_48 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f643,plain,
( e = sF5
| ~ spl10_41 ),
inference(resolution,[],[f609,f97]) ).
fof(f647,plain,
( spl10_48
| ~ spl10_41 ),
inference(avatar_split_clause,[],[f643,f607,f639]) ).
fof(f708,plain,
! [X0,X1] :
( ~ subq(sK0(X0,p(X1)),X1)
| subq(X0,p(X1)) ),
inference(resolution,[],[f66,f52]) ).
fof(f862,plain,
! [X0] :
( subq(X0,sF8)
| ~ subq(X0,sF9)
| mem(sK0(X0,sF8),sF5)
| subq(X0,sF8) ),
inference(resolution,[],[f213,f52]) ).
fof(f866,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF7)
| ~ subq(X0,sF9)
| mem(sK0(X0,X1),sF5)
| subq(X0,X1)
| mem(sK0(X0,X1),sF6) ),
inference(resolution,[],[f213,f111]) ).
fof(f871,plain,
! [X0] :
( mem(sK0(X0,sF8),sF5)
| ~ subq(X0,sF9)
| subq(X0,sF8) ),
inference(duplicate_literal_removal,[],[f862]) ).
fof(f875,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF6)
| mem(sK0(X0,X1),sF5)
| subq(X0,X1)
| ~ subq(X0,sF9)
| sK0(X0,X1) = sF6 ),
inference(resolution,[],[f866,f98]) ).
fof(f885,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF5)
| subq(X0,X1)
| ~ subq(X0,sF9)
| sK0(X0,X1) = sF6
| sK0(X0,X1) = sF5 ),
inference(resolution,[],[f875,f97]) ).
fof(f892,plain,
! [X0] :
( subq(X0,sF5)
| ~ subq(X0,sF9)
| sF6 = sK0(X0,sF5)
| sF5 = sK0(X0,sF5)
| subq(X0,sF5) ),
inference(resolution,[],[f885,f52]) ).
fof(f895,plain,
( ! [X0,X1] :
( ~ subq(X0,sF9)
| subq(X0,X1)
| sK0(X0,X1) = sF6
| sK0(X0,X1) = sF5
| e = sK0(X0,X1) )
| ~ spl10_4 ),
inference(resolution,[],[f885,f239]) ).
fof(f902,plain,
! [X0] :
( ~ subq(X0,sF9)
| subq(X0,sF5)
| sF6 = sK0(X0,sF5)
| sF5 = sK0(X0,sF5) ),
inference(duplicate_literal_removal,[],[f892]) ).
fof(f922,plain,
( sF5 = p(e)
| e = sK0(sF5,p(e))
| e = sK0(p(e),sF5) ),
inference(resolution,[],[f165,f546]) ).
fof(f933,definition,
( spl10_59
<=> e = sK0(p(e),sF5) ),
introduced(definition,[new_symbols(definition,[spl10_59])],[avatar_definition]) ).
fof(f935,plain,
( e = sK0(p(e),sF5)
| ~ spl10_59 ),
inference(avatar_component_clause,[],[f933]) ).
fof(f937,definition,
( spl10_60
<=> e = sK0(sF5,p(e)) ),
introduced(definition,[new_symbols(definition,[spl10_60])],[avatar_definition]) ).
fof(f939,plain,
( e = sK0(sF5,p(e))
| ~ spl10_60 ),
inference(avatar_component_clause,[],[f937]) ).
fof(f941,definition,
( spl10_61
<=> sF5 = p(e) ),
introduced(definition,[new_symbols(definition,[spl10_61])],[avatar_definition]) ).
fof(f943,plain,
( sF5 = p(e)
| ~ spl10_61 ),
inference(avatar_component_clause,[],[f941]) ).
fof(f944,plain,
( spl10_59
| spl10_60
| spl10_61 ),
inference(avatar_split_clause,[],[f922,f941,f937,f933]) ).
fof(f972,plain,
! [X0] :
( subq(X0,sF7)
| ~ subq(X0,sF8)
| mem(sK0(X0,sF7),sF6)
| subq(X0,sF7) ),
inference(resolution,[],[f212,f52]) ).
fof(f975,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF6)
| ~ subq(X0,sF8)
| subq(X0,X1)
| sK0(X0,X1) = sF6 ),
inference(resolution,[],[f212,f98]) ).
fof(f982,plain,
! [X0] :
( mem(sK0(X0,sF7),sF6)
| ~ subq(X0,sF8)
| subq(X0,sF7) ),
inference(duplicate_literal_removal,[],[f972]) ).
fof(f983,plain,
! [X0] :
( ~ subq(X0,sF8)
| subq(X0,sF6)
| sF6 = sK0(X0,sF6)
| subq(X0,sF6) ),
inference(resolution,[],[f975,f52]) ).
fof(f986,plain,
! [X0,X1] :
( ~ subq(X0,sF8)
| subq(X0,X1)
| sK0(X0,X1) = sF6
| sK0(X0,X1) = sF5 ),
inference(resolution,[],[f975,f97]) ).
fof(f993,plain,
! [X0] :
( ~ subq(X0,sF8)
| subq(X0,sF6)
| sF6 = sK0(X0,sF6) ),
inference(duplicate_literal_removal,[],[f983]) ).
fof(f1003,plain,
! [X0] :
( subq(sF5,X0)
| sF6 = sK0(sF5,X0)
| sF5 = sK0(sF5,X0)
| e = sK0(sF5,sF8) ),
inference(resolution,[],[f986,f161]) ).
fof(f1053,plain,
! [X2,X0,X1] :
( ~ subq(X1,X2)
| ~ subq(X0,X1)
| mem(sK1(X0),X2)
| ~ atleast2p(X0) ),
inference(resolution,[],[f305,f50]) ).
fof(f1068,plain,
! [X0] :
( mem(sK1(X0),sF7)
| ~ subq(X0,sF8)
| ~ atleast2p(X0)
| mem(sK1(X0),sF6) ),
inference(resolution,[],[f305,f111]) ).
fof(f1069,plain,
! [X0] :
( mem(sK1(X0),sF8)
| ~ subq(X0,sF9)
| ~ atleast2p(X0)
| mem(sK1(X0),sF5) ),
inference(resolution,[],[f305,f109]) ).
fof(f1120,plain,
! [X0,X1] :
( subq(sK0(p(e),X0),X1)
| subq(p(e),X0) ),
inference(resolution,[],[f200,f258]) ).
fof(f1262,plain,
( ~ atleast2p(sF6)
| sF5 = sK0(sF6,p(sK1(sF6))) ),
inference(superposition,[],[f486,f84]) ).
fof(f1263,plain,
( ~ atleast2p(sF7)
| sF6 = sK0(sF7,p(sK1(sF7))) ),
inference(superposition,[],[f486,f86]) ).
fof(f1314,definition,
( spl10_74
<=> sF5 = sK0(sF8,sF7) ),
introduced(definition,[new_symbols(definition,[spl10_74])],[avatar_definition]) ).
fof(f1315,plain,
( sF5 != sK0(sF8,sF7)
| spl10_74 ),
inference(avatar_component_clause,[],[f1314]) ).
fof(f1316,plain,
( sF5 = sK0(sF8,sF7)
| ~ spl10_74 ),
inference(avatar_component_clause,[],[f1314]) ).
fof(f1346,plain,
( mem(sF5,sF7)
| ~ spl10_6 ),
inference(superposition,[],[f113,f256]) ).
fof(f1365,plain,
( sF5 = sF6
| ~ spl10_6 ),
inference(resolution,[],[f1346,f98]) ).
fof(f1383,plain,
( ~ mem(e,sF5)
| ~ spl10_6
| spl10_41 ),
inference(superposition,[],[f608,f1365]) ).
fof(f1396,plain,
( $false
| ~ spl10_6
| spl10_41 ),
inference(forward_subsumption_resolution,[],[f1383,f106]) ).
fof(f1397,plain,
( ~ spl10_6
| spl10_41 ),
inference(avatar_contradiction_clause,[],[f1396]) ).
fof(f1411,plain,
( ~ mem(sF5,sF7)
| subq(sF8,sF7)
| ~ spl10_74 ),
inference(superposition,[],[f52,f1316]) ).
fof(f1422,plain,
( ~ mem(sF5,sF7)
| spl10_5
| ~ spl10_74 ),
inference(forward_subsumption_resolution,[],[f1411,f252]) ).
fof(f1456,definition,
( spl10_80
<=> subq(sF5,sF8) ),
introduced(definition,[new_symbols(definition,[spl10_80])],[avatar_definition]) ).
fof(f1457,plain,
( ~ subq(sF5,sF8)
| spl10_80 ),
inference(avatar_component_clause,[],[f1456]) ).
fof(f1458,plain,
( subq(sF5,sF8)
| ~ spl10_80 ),
inference(avatar_component_clause,[],[f1456]) ).
fof(f1528,definition,
( spl10_86
<=> sF5 = sK0(sF6,sF5) ),
introduced(definition,[new_symbols(definition,[spl10_86])],[avatar_definition]) ).
fof(f1529,plain,
( sF5 != sK0(sF6,sF5)
| spl10_86 ),
inference(avatar_component_clause,[],[f1528]) ).
fof(f1530,plain,
( sF5 = sK0(sF6,sF5)
| ~ spl10_86 ),
inference(avatar_component_clause,[],[f1528]) ).
fof(f1576,definition,
( spl10_90
<=> ! [X0] : subq(sF6,X0) ),
introduced(definition,[new_symbols(definition,[spl10_90])],[avatar_definition]) ).
fof(f1577,plain,
( ! [X0] : subq(sF6,X0)
| ~ spl10_90 ),
inference(avatar_component_clause,[],[f1576]) ).
fof(f1579,plain,
( ! [X0] : ~ mem(X0,sF5)
| ~ spl10_48 ),
inference(superposition,[],[f54,f641]) ).
fof(f1583,plain,
( mem(sF5,sF5)
| ~ spl10_48 ),
inference(superposition,[],[f106,f641]) ).
fof(f1627,definition,
( spl10_93
<=> ! [X0] :
( subq(sF5,X0)
| sF5 = sK0(sF5,X0)
| sF6 = sK0(sF5,X0) ) ),
introduced(definition,[new_symbols(definition,[spl10_93])],[avatar_definition]) ).
fof(f1628,plain,
( ! [X0] :
( subq(sF5,X0)
| sF5 = sK0(sF5,X0)
| sF6 = sK0(sF5,X0) )
| ~ spl10_93 ),
inference(avatar_component_clause,[],[f1627]) ).
fof(f1629,plain,
( spl10_43
| spl10_93 ),
inference(avatar_split_clause,[],[f1003,f1627,f615]) ).
fof(f1645,plain,
( sF4 = s(sF6)
| ~ spl10_46 ),
inference(superposition,[],[f80,f631]) ).
fof(f1649,plain,
( ! [X0] : subq(sF6,X0)
| ~ spl10_46 ),
inference(superposition,[],[f116,f631]) ).
fof(f1661,plain,
( spl10_90
| ~ spl10_46 ),
inference(avatar_split_clause,[],[f1649,f629,f1576]) ).
fof(f1664,plain,
( sF4 = sF7
| ~ spl10_46 ),
inference(forward_demodulation,[],[f1645,f86]) ).
fof(f1665,plain,
( sF5 = sF7
| ~ spl10_4
| ~ spl10_46 ),
inference(forward_demodulation,[],[f1664,f184]) ).
fof(f1668,plain,
( ! [X0] :
( subq(sF5,X0)
| sF6 = sK0(sF5,X0)
| sF5 = sK0(sF5,X0) )
| ~ spl10_80 ),
inference(resolution,[],[f1458,f986]) ).
fof(f1675,plain,
( spl10_93
| ~ spl10_80 ),
inference(avatar_split_clause,[],[f1668,f1456,f1627]) ).
fof(f1789,definition,
( spl10_98
<=> subq(sF6,sF5) ),
introduced(definition,[new_symbols(definition,[spl10_98])],[avatar_definition]) ).
fof(f1790,plain,
( ~ subq(sF6,sF5)
| spl10_98 ),
inference(avatar_component_clause,[],[f1789]) ).
fof(f1791,plain,
( subq(sF6,sF5)
| ~ spl10_98 ),
inference(avatar_component_clause,[],[f1789]) ).
fof(f1793,definition,
( spl10_99
<=> mem(sF5,sF5) ),
introduced(definition,[new_symbols(definition,[spl10_99])],[avatar_definition]) ).
fof(f1794,plain,
( mem(sF5,sF5)
| ~ spl10_99 ),
inference(avatar_component_clause,[],[f1793]) ).
fof(f1795,plain,
( ~ mem(sF5,sF5)
| spl10_99 ),
inference(avatar_component_clause,[],[f1793]) ).
fof(f1799,plain,
( sF5 = sK0(s(sF5),sF5)
| spl10_99 ),
inference(resolution,[],[f1795,f413]) ).
fof(f1800,plain,
( sF5 = sK0(sF6,sF5)
| spl10_99 ),
inference(forward_demodulation,[],[f1799,f84]) ).
fof(f1898,plain,
( $false
| ~ spl10_48 ),
inference(forward_subsumption_resolution,[],[f1583,f1579]) ).
fof(f1899,plain,
~ spl10_48,
inference(avatar_contradiction_clause,[],[f1898]) ).
fof(f2042,plain,
( $false
| spl10_86
| spl10_99 ),
inference(forward_subsumption_resolution,[],[f1800,f1529]) ).
fof(f2043,plain,
( spl10_86
| spl10_99 ),
inference(avatar_contradiction_clause,[],[f2042]) ).
fof(f2140,plain,
( ~ atleast2p(sF5)
| ~ spl10_4
| spl10_17
| ~ spl10_46 ),
inference(superposition,[],[f360,f1665]) ).
fof(f2192,plain,
( e = sF5
| ~ spl10_4
| ~ spl10_99 ),
inference(resolution,[],[f1794,f239]) ).
fof(f2197,plain,
( $false
| ~ spl10_4
| spl10_48
| ~ spl10_99 ),
inference(forward_subsumption_resolution,[],[f2192,f640]) ).
fof(f2198,plain,
( ~ spl10_4
| spl10_48
| ~ spl10_99 ),
inference(avatar_contradiction_clause,[],[f2197]) ).
fof(f2206,plain,
( ! [X0] : mem(sF5,X0)
| ~ spl10_90 ),
inference(resolution,[],[f1577,f153]) ).
fof(f2242,plain,
( mem(sF5,sF5)
| ~ spl10_98 ),
inference(resolution,[],[f1791,f153]) ).
fof(f2246,plain,
( $false
| ~ spl10_98
| spl10_99 ),
inference(forward_subsumption_resolution,[],[f2242,f1795]) ).
fof(f2247,plain,
( ~ spl10_98
| spl10_99 ),
inference(avatar_contradiction_clause,[],[f2246]) ).
fof(f2261,plain,
( sF5 = sK0(sF5,e)
| sF6 = sK0(sF5,e)
| e = sF5
| ~ spl10_93 ),
inference(resolution,[],[f1628,f144]) ).
fof(f2280,plain,
( sF5 = sK0(sF5,e)
| sF6 = sK0(sF5,e)
| spl10_48
| ~ spl10_93 ),
inference(forward_subsumption_resolution,[],[f2261,f640]) ).
fof(f2285,plain,
( e = sF5
| sF6 = sK0(sF5,e)
| ~ spl10_4
| spl10_48
| ~ spl10_93 ),
inference(forward_demodulation,[],[f2280,f448]) ).
fof(f2290,plain,
( sF6 = sK0(sF5,e)
| ~ spl10_4
| spl10_48
| ~ spl10_93 ),
inference(forward_subsumption_resolution,[],[f2285,f640]) ).
fof(f2295,plain,
( e = sF6
| ~ spl10_4
| spl10_48
| ~ spl10_93 ),
inference(forward_demodulation,[],[f2290,f448]) ).
fof(f2298,plain,
( $false
| ~ spl10_4
| spl10_46
| spl10_48
| ~ spl10_93 ),
inference(forward_subsumption_resolution,[],[f2295,f630]) ).
fof(f2299,plain,
( ~ spl10_4
| spl10_46
| spl10_48
| ~ spl10_93 ),
inference(avatar_contradiction_clause,[],[f2298]) ).
fof(f2561,plain,
! [X0] :
( ~ subq(X0,sF8)
| subq(X0,sF7)
| sF5 = sK0(X0,sF7) ),
inference(resolution,[],[f982,f97]) ).
fof(f2567,plain,
( subq(sF8,sF7)
| sF5 = sK0(sF8,sF7) ),
inference(resolution,[],[f2561,f135]) ).
fof(f2590,plain,
! [X0] :
( mem(sK0(sF9,X0),sF7)
| mem(sK0(sF9,X0),sF5)
| subq(sF9,X0)
| mem(sK0(sF9,X0),sF6) ),
inference(resolution,[],[f124,f111]) ).
fof(f2626,plain,
! [X0] :
( mem(sK0(sF9,X0),sF6)
| subq(sF9,X0)
| mem(sK0(sF9,X0),sF5)
| sF6 = sK0(sF9,X0) ),
inference(resolution,[],[f2590,f98]) ).
fof(f2669,plain,
! [X0] :
( mem(sK0(sF9,X0),sF5)
| subq(sF9,X0)
| sF6 = sK0(sF9,X0)
| sF5 = sK0(sF9,X0) ),
inference(resolution,[],[f2626,f97]) ).
fof(f2700,plain,
( ! [X0] :
( subq(sF9,X0)
| sF6 = sK0(sF9,X0)
| sF5 = sK0(sF9,X0)
| e = sK0(sF9,X0) )
| ~ spl10_4 ),
inference(resolution,[],[f2669,f239]) ).
fof(f2753,plain,
( sF6 = sK0(sF9,sK3(sF9))
| sF5 = sK0(sF9,sK3(sF9))
| e = sK0(sF9,sK3(sF9))
| ~ atleast4p(sF9)
| ~ spl10_4 ),
inference(resolution,[],[f2700,f72]) ).
fof(f2766,plain,
( sF6 = sK0(sF9,sK3(sF9))
| sF5 = sK0(sF9,sK3(sF9))
| e = sK0(sF9,sK3(sF9))
| ~ spl10_4 ),
inference(forward_subsumption_resolution,[],[f2753,f91]) ).
fof(f2807,definition,
( spl10_118
<=> e = sK0(sF9,sK3(sF9)) ),
introduced(definition,[new_symbols(definition,[spl10_118])],[avatar_definition]) ).
fof(f2809,plain,
( e = sK0(sF9,sK3(sF9))
| ~ spl10_118 ),
inference(avatar_component_clause,[],[f2807]) ).
fof(f2811,definition,
( spl10_119
<=> sF5 = sK0(sF9,sK3(sF9)) ),
introduced(definition,[new_symbols(definition,[spl10_119])],[avatar_definition]) ).
fof(f2812,plain,
( sF5 != sK0(sF9,sK3(sF9))
| spl10_119 ),
inference(avatar_component_clause,[],[f2811]) ).
fof(f2813,plain,
( sF5 = sK0(sF9,sK3(sF9))
| ~ spl10_119 ),
inference(avatar_component_clause,[],[f2811]) ).
fof(f2815,definition,
( spl10_120
<=> sF6 = sK0(sF9,sK3(sF9)) ),
introduced(definition,[new_symbols(definition,[spl10_120])],[avatar_definition]) ).
fof(f2816,plain,
( sF6 != sK0(sF9,sK3(sF9))
| spl10_120 ),
inference(avatar_component_clause,[],[f2815]) ).
fof(f2817,plain,
( sF6 = sK0(sF9,sK3(sF9))
| ~ spl10_120 ),
inference(avatar_component_clause,[],[f2815]) ).
fof(f2818,plain,
( spl10_118
| spl10_119
| spl10_120
| ~ spl10_4 ),
inference(avatar_split_clause,[],[f2766,f182,f2815,f2811,f2807]) ).
fof(f2826,plain,
( ~ mem(e,sK3(sF9))
| subq(sF9,sK3(sF9))
| ~ spl10_118 ),
inference(superposition,[],[f52,f2809]) ).
fof(f2836,definition,
( spl10_121
<=> subq(sF9,sK3(sF9)) ),
introduced(definition,[new_symbols(definition,[spl10_121])],[avatar_definition]) ).
fof(f2837,plain,
( ~ subq(sF9,sK3(sF9))
| spl10_121 ),
inference(avatar_component_clause,[],[f2836]) ).
fof(f2838,plain,
( subq(sF9,sK3(sF9))
| ~ spl10_121 ),
inference(avatar_component_clause,[],[f2836]) ).
fof(f2840,definition,
( spl10_122
<=> mem(e,sK3(sF9)) ),
introduced(definition,[new_symbols(definition,[spl10_122])],[avatar_definition]) ).
fof(f2842,plain,
( ~ mem(e,sK3(sF9))
| spl10_122 ),
inference(avatar_component_clause,[],[f2840]) ).
fof(f2843,plain,
( spl10_121
| ~ spl10_122
| ~ spl10_118 ),
inference(avatar_split_clause,[],[f2826,f2807,f2840,f2836]) ).
fof(f3106,plain,
( ! [X0] :
( ~ subq(X0,sF9)
| subq(X0,sF8)
| e = sK0(X0,sF8) )
| ~ spl10_4 ),
inference(resolution,[],[f871,f239]) ).
fof(f3122,plain,
( ! [X0] :
( subq(sK3(sF9),X0)
| sF6 = sK0(sK3(sF9),X0)
| sF5 = sK0(sK3(sF9),X0)
| e = sK0(sK3(sF9),X0)
| ~ atleast4p(sF9) )
| ~ spl10_4 ),
inference(resolution,[],[f895,f74]) ).
fof(f3130,plain,
( ! [X0] :
( subq(sK3(sF9),X0)
| sF6 = sK0(sK3(sF9),X0)
| sF5 = sK0(sK3(sF9),X0)
| e = sK0(sK3(sF9),X0) )
| ~ spl10_4 ),
inference(forward_subsumption_resolution,[],[f3122,f91]) ).
fof(f3138,plain,
( sF6 = sK0(sK3(sF9),sK2(sK3(sF9)))
| sF5 = sK0(sK3(sF9),sK2(sK3(sF9)))
| e = sK0(sK3(sF9),sK2(sK3(sF9)))
| ~ atleast3p(sK3(sF9))
| ~ spl10_4 ),
inference(resolution,[],[f3130,f69]) ).
fof(f3267,definition,
( spl10_150
<=> atleast3p(sK3(sF9)) ),
introduced(definition,[new_symbols(definition,[spl10_150])],[avatar_definition]) ).
fof(f3268,plain,
( atleast3p(sK3(sF9))
| ~ spl10_150 ),
inference(avatar_component_clause,[],[f3267]) ).
fof(f3269,plain,
( ~ atleast3p(sK3(sF9))
| spl10_150 ),
inference(avatar_component_clause,[],[f3267]) ).
fof(f3271,definition,
( spl10_151
<=> e = sK0(sK3(sF9),sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_151])],[avatar_definition]) ).
fof(f3272,plain,
( e != sK0(sK3(sF9),sK2(sK3(sF9)))
| spl10_151 ),
inference(avatar_component_clause,[],[f3271]) ).
fof(f3273,plain,
( e = sK0(sK3(sF9),sK2(sK3(sF9)))
| ~ spl10_151 ),
inference(avatar_component_clause,[],[f3271]) ).
fof(f3275,definition,
( spl10_152
<=> sF5 = sK0(sK3(sF9),sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_152])],[avatar_definition]) ).
fof(f3277,plain,
( sF5 = sK0(sK3(sF9),sK2(sK3(sF9)))
| ~ spl10_152 ),
inference(avatar_component_clause,[],[f3275]) ).
fof(f3279,definition,
( spl10_153
<=> sF6 = sK0(sK3(sF9),sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_153])],[avatar_definition]) ).
fof(f3281,plain,
( sF6 = sK0(sK3(sF9),sK2(sK3(sF9)))
| ~ spl10_153 ),
inference(avatar_component_clause,[],[f3279]) ).
fof(f3282,plain,
( ~ spl10_150
| spl10_151
| spl10_152
| spl10_153
| ~ spl10_4 ),
inference(avatar_split_clause,[],[f3138,f182,f3279,f3275,f3271,f3267]) ).
fof(f3382,definition,
( spl10_170
<=> mem(sF5,sK3(sF9)) ),
introduced(definition,[new_symbols(definition,[spl10_170])],[avatar_definition]) ).
fof(f3383,plain,
( ~ mem(sF5,sK3(sF9))
| spl10_170 ),
inference(avatar_component_clause,[],[f3382]) ).
fof(f3384,plain,
( mem(sF5,sK3(sF9))
| ~ spl10_170 ),
inference(avatar_component_clause,[],[f3382]) ).
fof(f3405,definition,
( spl10_173
<=> mem(sF6,sK3(sF9)) ),
introduced(definition,[new_symbols(definition,[spl10_173])],[avatar_definition]) ).
fof(f3406,plain,
( ~ mem(sF6,sK3(sF9))
| spl10_173 ),
inference(avatar_component_clause,[],[f3405]) ).
fof(f3407,plain,
( mem(sF6,sK3(sF9))
| ~ spl10_173 ),
inference(avatar_component_clause,[],[f3405]) ).
fof(f3489,plain,
( ~ atleast4p(sF9)
| spl10_150 ),
inference(resolution,[],[f3269,f73]) ).
fof(f3490,plain,
( $false
| spl10_150 ),
inference(forward_subsumption_resolution,[],[f3489,f91]) ).
fof(f3491,plain,
spl10_150,
inference(avatar_contradiction_clause,[],[f3490]) ).
fof(f3492,plain,
( mem(e,sK3(sF9))
| subq(sK3(sF9),sK2(sK3(sF9)))
| ~ spl10_151 ),
inference(superposition,[],[f51,f3273]) ).
fof(f3493,plain,
( ~ mem(e,sK2(sK3(sF9)))
| subq(sK3(sF9),sK2(sK3(sF9)))
| ~ spl10_151 ),
inference(superposition,[],[f52,f3273]) ).
fof(f3505,definition,
( spl10_174
<=> subq(sK3(sF9),sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_174])],[avatar_definition]) ).
fof(f3506,plain,
( ~ subq(sK3(sF9),sK2(sK3(sF9)))
| spl10_174 ),
inference(avatar_component_clause,[],[f3505]) ).
fof(f3507,plain,
( subq(sK3(sF9),sK2(sK3(sF9)))
| ~ spl10_174 ),
inference(avatar_component_clause,[],[f3505]) ).
fof(f3510,definition,
( spl10_175
<=> mem(e,sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_175])],[avatar_definition]) ).
fof(f3511,plain,
( mem(e,sK2(sK3(sF9)))
| ~ spl10_175 ),
inference(avatar_component_clause,[],[f3510]) ).
fof(f3512,plain,
( ~ mem(e,sK2(sK3(sF9)))
| spl10_175 ),
inference(avatar_component_clause,[],[f3510]) ).
fof(f3513,plain,
( spl10_174
| ~ spl10_175
| ~ spl10_151 ),
inference(avatar_split_clause,[],[f3493,f3271,f3510,f3505]) ).
fof(f3514,plain,
( subq(sK3(sF9),sK2(sK3(sF9)))
| spl10_122
| ~ spl10_151 ),
inference(forward_subsumption_resolution,[],[f3492,f2842]) ).
fof(f3517,plain,
( spl10_174
| spl10_122
| ~ spl10_151 ),
inference(avatar_split_clause,[],[f3514,f3271,f2840,f3505]) ).
fof(f3520,plain,
( ~ atleast3p(sK3(sF9))
| ~ spl10_174 ),
inference(resolution,[],[f3507,f69]) ).
fof(f3531,plain,
( $false
| ~ spl10_150
| ~ spl10_174 ),
inference(forward_subsumption_resolution,[],[f3520,f3268]) ).
fof(f3532,plain,
( ~ spl10_150
| ~ spl10_174 ),
inference(avatar_contradiction_clause,[],[f3531]) ).
fof(f3538,plain,
( ~ mem(sF5,sK3(sF9))
| subq(sF9,sK3(sF9))
| ~ spl10_119 ),
inference(superposition,[],[f52,f2813]) ).
fof(f3546,plain,
( subq(sF9,sK3(sF9))
| ~ spl10_119
| ~ spl10_170 ),
inference(forward_subsumption_resolution,[],[f3538,f3384]) ).
fof(f3547,plain,
( spl10_121
| ~ spl10_119
| ~ spl10_170 ),
inference(avatar_split_clause,[],[f3546,f3382,f2811,f2836]) ).
fof(f3551,plain,
( ~ atleast4p(sF9)
| ~ spl10_121 ),
inference(resolution,[],[f2838,f72]) ).
fof(f3562,plain,
( $false
| ~ spl10_121 ),
inference(forward_subsumption_resolution,[],[f3551,f91]) ).
fof(f3563,plain,
~ spl10_121,
inference(avatar_contradiction_clause,[],[f3562]) ).
fof(f3567,plain,
( ~ mem(sF6,sK3(sF9))
| subq(sF9,sK3(sF9))
| ~ spl10_120 ),
inference(superposition,[],[f52,f2817]) ).
fof(f3573,plain,
( subq(sF9,sK3(sF9))
| ~ spl10_120
| ~ spl10_173 ),
inference(forward_subsumption_resolution,[],[f3567,f3407]) ).
fof(f3574,plain,
( $false
| ~ spl10_120
| spl10_121
| ~ spl10_173 ),
inference(forward_subsumption_resolution,[],[f3573,f2837]) ).
fof(f3575,plain,
( ~ spl10_120
| spl10_121
| ~ spl10_173 ),
inference(avatar_contradiction_clause,[],[f3574]) ).
fof(f3597,plain,
( sF6 = sK0(sF9,sK3(sF9))
| sF5 = sK0(sF9,sK3(sF9))
| e = sK0(sF9,sK3(sF9))
| ~ spl10_4
| spl10_121 ),
inference(resolution,[],[f2837,f2700]) ).
fof(f3598,plain,
( mem(sF5,sK3(sF9))
| subq(sK3(sF9),sK2(sK3(sF9)))
| ~ spl10_152 ),
inference(superposition,[],[f51,f3277]) ).
fof(f3599,plain,
( ~ mem(sF5,sK2(sK3(sF9)))
| subq(sK3(sF9),sK2(sK3(sF9)))
| ~ spl10_152 ),
inference(superposition,[],[f52,f3277]) ).
fof(f3607,plain,
( ~ mem(sF5,sK2(sK3(sF9)))
| ~ spl10_152
| spl10_174 ),
inference(forward_subsumption_resolution,[],[f3599,f3506]) ).
fof(f3861,plain,
( subq(sK3(sF9),sK2(sK3(sF9)))
| ~ spl10_152
| spl10_170 ),
inference(forward_subsumption_resolution,[],[f3598,f3383]) ).
fof(f3867,plain,
( $false
| ~ spl10_152
| spl10_170
| spl10_174 ),
inference(forward_subsumption_resolution,[],[f3861,f3506]) ).
fof(f3868,plain,
( ~ spl10_152
| spl10_170
| spl10_174 ),
inference(avatar_contradiction_clause,[],[f3867]) ).
fof(f4079,plain,
( subq(p(e),sF5)
| sF6 = sK0(p(e),sF5)
| sF5 = sK0(p(e),sF5)
| e = sK0(p(e),sF9) ),
inference(resolution,[],[f902,f546]) ).
fof(f4091,plain,
( e = sF6
| subq(p(e),sF5)
| sF5 = sK0(p(e),sF5)
| e = sK0(p(e),sF9)
| ~ spl10_59 ),
inference(forward_demodulation,[],[f4079,f935]) ).
fof(f4092,plain,
( subq(p(e),sF5)
| sF5 = sK0(p(e),sF5)
| e = sK0(p(e),sF9)
| spl10_46
| ~ spl10_59 ),
inference(forward_subsumption_resolution,[],[f4091,f630]) ).
fof(f4093,plain,
( e = sF5
| subq(p(e),sF5)
| e = sK0(p(e),sF9)
| spl10_46
| ~ spl10_59 ),
inference(forward_demodulation,[],[f4092,f935]) ).
fof(f4094,plain,
( subq(p(e),sF5)
| e = sK0(p(e),sF9)
| spl10_46
| spl10_48
| ~ spl10_59 ),
inference(forward_subsumption_resolution,[],[f4093,f640]) ).
fof(f4096,definition,
( spl10_187
<=> e = sK0(p(e),sF9) ),
introduced(definition,[new_symbols(definition,[spl10_187])],[avatar_definition]) ).
fof(f4098,plain,
( e = sK0(p(e),sF9)
| ~ spl10_187 ),
inference(avatar_component_clause,[],[f4096]) ).
fof(f4100,definition,
( spl10_188
<=> subq(p(e),sF5) ),
introduced(definition,[new_symbols(definition,[spl10_188])],[avatar_definition]) ).
fof(f4102,plain,
( subq(p(e),sF5)
| ~ spl10_188 ),
inference(avatar_component_clause,[],[f4100]) ).
fof(f4103,plain,
( spl10_187
| spl10_188
| spl10_46
| spl10_48
| ~ spl10_59 ),
inference(avatar_split_clause,[],[f4094,f933,f639,f629,f4100,f4096]) ).
fof(f4108,plain,
( ~ mem(e,sF9)
| subq(p(e),sF9)
| ~ spl10_187 ),
inference(superposition,[],[f52,f4098]) ).
fof(f4118,definition,
( spl10_189
<=> subq(p(e),sF9) ),
introduced(definition,[new_symbols(definition,[spl10_189])],[avatar_definition]) ).
fof(f4120,plain,
( subq(p(e),sF9)
| ~ spl10_189 ),
inference(avatar_component_clause,[],[f4118]) ).
fof(f4125,plain,
( subq(p(e),sF9)
| ~ spl10_187 ),
inference(forward_subsumption_resolution,[],[f4108,f127]) ).
fof(f4132,plain,
( spl10_189
| ~ spl10_187 ),
inference(avatar_split_clause,[],[f4125,f4096,f4118]) ).
fof(f4134,plain,
( subq(p(e),sF5)
| sF6 = sK0(p(e),sF5)
| sF5 = sK0(p(e),sF5)
| ~ spl10_189 ),
inference(resolution,[],[f4120,f902]) ).
fof(f4146,plain,
( e = sF6
| subq(p(e),sF5)
| sF5 = sK0(p(e),sF5)
| ~ spl10_59
| ~ spl10_189 ),
inference(forward_demodulation,[],[f4134,f935]) ).
fof(f4147,plain,
( subq(p(e),sF5)
| sF5 = sK0(p(e),sF5)
| spl10_46
| ~ spl10_59
| ~ spl10_189 ),
inference(forward_subsumption_resolution,[],[f4146,f630]) ).
fof(f4148,plain,
( e = sF5
| subq(p(e),sF5)
| spl10_46
| ~ spl10_59
| ~ spl10_189 ),
inference(forward_demodulation,[],[f4147,f935]) ).
fof(f4149,plain,
( subq(p(e),sF5)
| spl10_46
| spl10_48
| ~ spl10_59
| ~ spl10_189 ),
inference(forward_subsumption_resolution,[],[f4148,f640]) ).
fof(f4150,plain,
( spl10_188
| spl10_46
| spl10_48
| ~ spl10_59
| ~ spl10_189 ),
inference(avatar_split_clause,[],[f4149,f4118,f933,f639,f629,f4100]) ).
fof(f4152,plain,
( sF5 = p(e)
| e = sK0(sF5,p(e))
| ~ spl10_188 ),
inference(resolution,[],[f4102,f165]) ).
fof(f4155,definition,
( spl10_194
<=> subq(sF5,p(e)) ),
introduced(definition,[new_symbols(definition,[spl10_194])],[avatar_definition]) ).
fof(f4156,plain,
( subq(sF5,p(e))
| ~ spl10_194 ),
inference(avatar_component_clause,[],[f4155]) ).
fof(f4157,plain,
( ~ subq(sF5,p(e))
| spl10_194 ),
inference(avatar_component_clause,[],[f4155]) ).
fof(f4159,plain,
( spl10_60
| spl10_61
| ~ spl10_188 ),
inference(avatar_split_clause,[],[f4152,f4100,f941,f937]) ).
fof(f4163,plain,
( ~ subq(e,e)
| subq(sF5,p(e))
| ~ spl10_60 ),
inference(superposition,[],[f708,f939]) ).
fof(f4175,plain,
( subq(sF5,p(e))
| ~ spl10_60 ),
inference(forward_subsumption_resolution,[],[f4163,f116]) ).
fof(f4177,plain,
( $false
| ~ spl10_60
| spl10_194 ),
inference(forward_subsumption_resolution,[],[f4175,f4157]) ).
fof(f4178,plain,
( ~ spl10_60
| spl10_194 ),
inference(avatar_contradiction_clause,[],[f4177]) ).
fof(f4467,plain,
! [X0,X1] :
( mem(sK1(X0),sF6)
| mem(sK1(X0),X1)
| ~ atleast2p(X0)
| ~ subq(X0,sF8)
| ~ subq(sF7,X1) ),
inference(resolution,[],[f1068,f50]) ).
fof(f4770,definition,
( spl10_214
<=> subq(sF6,sF7) ),
introduced(definition,[new_symbols(definition,[spl10_214])],[avatar_definition]) ).
fof(f4771,plain,
( subq(sF6,sF7)
| ~ spl10_214 ),
inference(avatar_component_clause,[],[f4770]) ).
fof(f4772,plain,
( ~ subq(sF6,sF7)
| spl10_214 ),
inference(avatar_component_clause,[],[f4770]) ).
fof(f5071,plain,
( mem(sF6,sK3(sF9))
| subq(sK3(sF9),sK2(sK3(sF9)))
| ~ spl10_153 ),
inference(superposition,[],[f51,f3281]) ).
fof(f5072,plain,
( ~ mem(sF6,sK2(sK3(sF9)))
| subq(sK3(sF9),sK2(sK3(sF9)))
| ~ spl10_153 ),
inference(superposition,[],[f52,f3281]) ).
fof(f5080,plain,
( ~ mem(sF6,sK2(sK3(sF9)))
| ~ spl10_153
| spl10_174 ),
inference(forward_subsumption_resolution,[],[f5072,f3506]) ).
fof(f5103,plain,
( mem(sF6,sK3(sF9))
| ~ spl10_153
| spl10_174 ),
inference(forward_subsumption_resolution,[],[f5071,f3506]) ).
fof(f6615,plain,
( mem(sF5,sF7)
| ~ spl10_214 ),
inference(resolution,[],[f4771,f153]) ).
fof(f6632,plain,
( $false
| spl10_5
| ~ spl10_74
| ~ spl10_214 ),
inference(forward_subsumption_resolution,[],[f6615,f1422]) ).
fof(f6633,plain,
( spl10_5
| ~ spl10_74
| ~ spl10_214 ),
inference(avatar_contradiction_clause,[],[f6632]) ).
fof(f6641,plain,
( sF5 = sK0(sF8,sF7)
| spl10_5 ),
inference(forward_subsumption_resolution,[],[f2567,f252]) ).
fof(f6648,plain,
( $false
| spl10_5
| spl10_74 ),
inference(forward_subsumption_resolution,[],[f6641,f1315]) ).
fof(f6649,plain,
( spl10_5
| spl10_74 ),
inference(avatar_contradiction_clause,[],[f6648]) ).
fof(f6956,plain,
! [X2,X0,X1] :
( mem(sK0(X0,X1),X2)
| subq(X0,X1)
| ~ subq(X0,sK2(X2))
| ~ atleast3p(X2) ),
inference(resolution,[],[f199,f71]) ).
fof(f6957,plain,
! [X2,X0,X1] :
( mem(sK0(X0,X1),X2)
| subq(X0,X1)
| ~ subq(X0,sK3(X2))
| ~ atleast4p(X2) ),
inference(resolution,[],[f199,f74]) ).
fof(f7424,plain,
! [X0] :
( mem(sK1(X0),sF7)
| ~ atleast2p(X0)
| mem(sK1(X0),sF5)
| ~ subq(X0,sF9)
| mem(sK1(X0),sF6) ),
inference(resolution,[],[f1069,f111]) ).
fof(f7427,plain,
! [X0] :
( mem(sK1(X0),sF6)
| mem(sK1(X0),sF5)
| ~ subq(X0,sF9)
| ~ atleast2p(X0)
| sK1(X0) = sF6 ),
inference(resolution,[],[f7424,f98]) ).
fof(f7431,plain,
! [X0] :
( mem(sK1(X0),sF5)
| ~ subq(X0,sF9)
| ~ atleast2p(X0)
| sK1(X0) = sF6
| sK1(X0) = sF5 ),
inference(resolution,[],[f7427,f97]) ).
fof(f7436,plain,
( ! [X0] :
( ~ subq(X0,sF9)
| ~ atleast2p(X0)
| sK1(X0) = sF6
| sK1(X0) = sF5
| e = sK1(X0) )
| ~ spl10_4 ),
inference(resolution,[],[f7431,f239]) ).
fof(f8475,plain,
! [X0] :
( subq(p(e),p(X0))
| subq(p(e),p(X0)) ),
inference(resolution,[],[f1120,f708]) ).
fof(f8513,plain,
! [X0] : subq(p(e),p(X0)),
inference(duplicate_literal_removal,[],[f8475]) ).
fof(f8526,plain,
( ! [X0] : subq(sF5,p(X0))
| ~ spl10_61 ),
inference(forward_demodulation,[],[f8513,f943]) ).
fof(f8550,plain,
( ~ atleast2p(sF5)
| ~ spl10_61 ),
inference(resolution,[],[f8526,f67]) ).
fof(f8597,plain,
! [X0,X1] :
( mem(sK1(X0),X1)
| ~ atleast2p(X0)
| ~ subq(X0,sF8)
| ~ subq(sF7,X1)
| sK1(X0) = sF5 ),
inference(resolution,[],[f4467,f97]) ).
fof(f10114,definition,
( spl10_461
<=> sF6 = sK0(sF7,p(sF6)) ),
introduced(definition,[new_symbols(definition,[spl10_461])],[avatar_definition]) ).
fof(f10115,plain,
( sF6 != sK0(sF7,p(sF6))
| spl10_461 ),
inference(avatar_component_clause,[],[f10114]) ).
fof(f10116,plain,
( sF6 = sK0(sF7,p(sF6))
| ~ spl10_461 ),
inference(avatar_component_clause,[],[f10114]) ).
fof(f10120,plain,
( ~ subq(sF6,sF6)
| subq(sF7,p(sF6))
| ~ spl10_461 ),
inference(superposition,[],[f708,f10116]) ).
fof(f10135,plain,
( subq(sF7,p(sF6))
| ~ spl10_461 ),
inference(forward_subsumption_resolution,[],[f10120,f135]) ).
fof(f10529,plain,
! [X0,X1] :
( ~ subq(X0,sK2(X1))
| mem(sK1(X0),X1)
| ~ atleast2p(X0)
| ~ atleast3p(X1) ),
inference(resolution,[],[f1053,f71]) ).
fof(f10681,definition,
( spl10_479
<=> mem(sK1(sK2(sK3(sF9))),sF7) ),
introduced(definition,[new_symbols(definition,[spl10_479])],[avatar_definition]) ).
fof(f10682,plain,
( ~ mem(sK1(sK2(sK3(sF9))),sF7)
| spl10_479 ),
inference(avatar_component_clause,[],[f10681]) ).
fof(f10683,plain,
( mem(sK1(sK2(sK3(sF9))),sF7)
| ~ spl10_479 ),
inference(avatar_component_clause,[],[f10681]) ).
fof(f10686,plain,
( sF6 = sK1(sK2(sK3(sF9)))
| ~ spl10_479 ),
inference(resolution,[],[f10683,f98]) ).
fof(f10692,plain,
( ~ subq(sK2(sK3(sF9)),p(sF6))
| ~ atleast2p(sK2(sK3(sF9)))
| ~ spl10_479 ),
inference(superposition,[],[f67,f10686]) ).
fof(f10693,plain,
( mem(sF6,sK2(sK3(sF9)))
| ~ atleast2p(sK2(sK3(sF9)))
| ~ spl10_479 ),
inference(superposition,[],[f68,f10686]) ).
fof(f10694,plain,
( ! [X0] :
( mem(sF6,X0)
| ~ atleast2p(sK2(sK3(sF9)))
| ~ subq(sK2(sK3(sF9)),X0) )
| ~ spl10_479 ),
inference(superposition,[],[f305,f10686]) ).
fof(f10709,definition,
( spl10_480
<=> atleast2p(sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_480])],[avatar_definition]) ).
fof(f10710,plain,
( atleast2p(sK2(sK3(sF9)))
| ~ spl10_480 ),
inference(avatar_component_clause,[],[f10709]) ).
fof(f10711,plain,
( ~ atleast2p(sK2(sK3(sF9)))
| spl10_480 ),
inference(avatar_component_clause,[],[f10709]) ).
fof(f10713,definition,
( spl10_481
<=> ! [X0] :
( mem(sF6,X0)
| ~ subq(sK2(sK3(sF9)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl10_481])],[avatar_definition]) ).
fof(f10714,plain,
( ! [X0] :
( ~ subq(sK2(sK3(sF9)),X0)
| mem(sF6,X0) )
| ~ spl10_481 ),
inference(avatar_component_clause,[],[f10713]) ).
fof(f10715,plain,
( ~ spl10_480
| spl10_481
| ~ spl10_479 ),
inference(avatar_split_clause,[],[f10694,f10681,f10713,f10709]) ).
fof(f10717,definition,
( spl10_482
<=> mem(sF6,sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_482])],[avatar_definition]) ).
fof(f10718,plain,
( ~ mem(sF6,sK2(sK3(sF9)))
| spl10_482 ),
inference(avatar_component_clause,[],[f10717]) ).
fof(f10719,plain,
( mem(sF6,sK2(sK3(sF9)))
| ~ spl10_482 ),
inference(avatar_component_clause,[],[f10717]) ).
fof(f10720,plain,
( ~ spl10_480
| spl10_482
| ~ spl10_479 ),
inference(avatar_split_clause,[],[f10693,f10681,f10717,f10709]) ).
fof(f10722,definition,
( spl10_483
<=> subq(sK2(sK3(sF9)),p(sF6)) ),
introduced(definition,[new_symbols(definition,[spl10_483])],[avatar_definition]) ).
fof(f10724,plain,
( ~ subq(sK2(sK3(sF9)),p(sF6))
| spl10_483 ),
inference(avatar_component_clause,[],[f10722]) ).
fof(f10725,plain,
( ~ spl10_480
| ~ spl10_483
| ~ spl10_479 ),
inference(avatar_split_clause,[],[f10692,f10681,f10722,f10709]) ).
fof(f10729,plain,
( ~ atleast3p(sK3(sF9))
| spl10_480 ),
inference(resolution,[],[f10711,f70]) ).
fof(f10730,plain,
( $false
| ~ spl10_150
| spl10_480 ),
inference(forward_subsumption_resolution,[],[f10729,f3268]) ).
fof(f10731,plain,
( ~ spl10_150
| spl10_480 ),
inference(avatar_contradiction_clause,[],[f10730]) ).
fof(f10737,plain,
( ~ atleast2p(sK2(sK3(sF9)))
| ~ subq(sK2(sK3(sF9)),sF7)
| spl10_479 ),
inference(resolution,[],[f10682,f305]) ).
fof(f10739,plain,
( ~ subq(sK2(sK3(sF9)),sF7)
| spl10_479
| ~ spl10_480 ),
inference(forward_subsumption_resolution,[],[f10737,f10710]) ).
fof(f10745,definition,
( spl10_484
<=> subq(sK2(sK3(sF9)),sF8) ),
introduced(definition,[new_symbols(definition,[spl10_484])],[avatar_definition]) ).
fof(f10746,plain,
( subq(sK2(sK3(sF9)),sF8)
| ~ spl10_484 ),
inference(avatar_component_clause,[],[f10745]) ).
fof(f10747,plain,
( ~ subq(sK2(sK3(sF9)),sF8)
| spl10_484 ),
inference(avatar_component_clause,[],[f10745]) ).
fof(f10750,definition,
( spl10_485
<=> subq(sK2(sK3(sF9)),sF9) ),
introduced(definition,[new_symbols(definition,[spl10_485])],[avatar_definition]) ).
fof(f10751,plain,
( subq(sK2(sK3(sF9)),sF9)
| ~ spl10_485 ),
inference(avatar_component_clause,[],[f10750]) ).
fof(f10752,plain,
( ~ subq(sK2(sK3(sF9)),sF9)
| spl10_485 ),
inference(avatar_component_clause,[],[f10750]) ).
fof(f10858,definition,
( spl10_498
<=> subq(sK2(sK3(sF9)),sF5) ),
introduced(definition,[new_symbols(definition,[spl10_498])],[avatar_definition]) ).
fof(f10859,plain,
( subq(sK2(sK3(sF9)),sF5)
| ~ spl10_498 ),
inference(avatar_component_clause,[],[f10858]) ).
fof(f10860,plain,
( ~ subq(sK2(sK3(sF9)),sF5)
| spl10_498 ),
inference(avatar_component_clause,[],[f10858]) ).
fof(f11118,definition,
( spl10_535
<=> sF6 = sK1(sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_535])],[avatar_definition]) ).
fof(f11119,plain,
( sF6 != sK1(sK2(sK3(sF9)))
| spl10_535 ),
inference(avatar_component_clause,[],[f11118]) ).
fof(f11120,plain,
( sF6 = sK1(sK2(sK3(sF9)))
| ~ spl10_535 ),
inference(avatar_component_clause,[],[f11118]) ).
fof(f11184,plain,
( mem(sF6,sK2(sK3(sF9)))
| ~ atleast2p(sK2(sK3(sF9)))
| ~ spl10_535 ),
inference(superposition,[],[f68,f11120]) ).
fof(f11185,plain,
( ! [X0] :
( mem(sF6,X0)
| ~ atleast2p(sK2(sK3(sF9)))
| ~ subq(sK2(sK3(sF9)),X0) )
| ~ spl10_535 ),
inference(superposition,[],[f305,f11120]) ).
fof(f11199,plain,
( ! [X0] :
( mem(sF6,X0)
| ~ subq(sK2(sK3(sF9)),X0) )
| ~ spl10_480
| ~ spl10_535 ),
inference(forward_subsumption_resolution,[],[f11185,f10710]) ).
fof(f11200,plain,
( mem(sF6,sK2(sK3(sF9)))
| ~ spl10_480
| ~ spl10_535 ),
inference(forward_subsumption_resolution,[],[f11184,f10710]) ).
fof(f11206,plain,
( spl10_481
| ~ spl10_480
| ~ spl10_535 ),
inference(avatar_split_clause,[],[f11199,f11118,f10709,f10713]) ).
fof(f11207,plain,
( spl10_482
| ~ spl10_480
| ~ spl10_535 ),
inference(avatar_split_clause,[],[f11200,f11118,f10709,f10717]) ).
fof(f11214,definition,
( spl10_536
<=> subq(sK2(sK3(sF9)),sF7) ),
introduced(definition,[new_symbols(definition,[spl10_536])],[avatar_definition]) ).
fof(f11215,plain,
( subq(sK2(sK3(sF9)),sF7)
| ~ spl10_536 ),
inference(avatar_component_clause,[],[f11214]) ).
fof(f11216,plain,
( ~ subq(sK2(sK3(sF9)),sF7)
| spl10_536 ),
inference(avatar_component_clause,[],[f11214]) ).
fof(f11219,definition,
( spl10_537
<=> subq(sK2(sK3(sF9)),sF6) ),
introduced(definition,[new_symbols(definition,[spl10_537])],[avatar_definition]) ).
fof(f11220,plain,
( subq(sK2(sK3(sF9)),sF6)
| ~ spl10_537 ),
inference(avatar_component_clause,[],[f11219]) ).
fof(f11221,plain,
( ~ subq(sK2(sK3(sF9)),sF6)
| spl10_537 ),
inference(avatar_component_clause,[],[f11219]) ).
fof(f11323,plain,
( mem(sF6,sK3(sF9))
| ~ atleast3p(sK3(sF9))
| ~ spl10_481 ),
inference(resolution,[],[f10714,f71]) ).
fof(f11324,plain,
( mem(sF6,sK2(sK3(sF9)))
| ~ spl10_481 ),
inference(resolution,[],[f10714,f135]) ).
fof(f11705,plain,
! [X0] :
( mem(sK1(sK2(X0)),X0)
| ~ atleast2p(sK2(X0))
| ~ atleast3p(X0) ),
inference(resolution,[],[f10529,f135]) ).
fof(f11736,plain,
! [X0] :
( mem(sK1(sK2(X0)),X0)
| ~ atleast3p(X0) ),
inference(forward_subsumption_resolution,[],[f11705,f70]) ).
fof(f12904,definition,
( spl10_600
<=> subq(sF5,sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_600])],[avatar_definition]) ).
fof(f12905,plain,
( subq(sF5,sK2(sK3(sF9)))
| ~ spl10_600 ),
inference(avatar_component_clause,[],[f12904]) ).
fof(f12906,plain,
( ~ subq(sF5,sK2(sK3(sF9)))
| spl10_600 ),
inference(avatar_component_clause,[],[f12904]) ).
fof(f12909,plain,
( e = sK0(sF5,sK2(sK3(sF9)))
| spl10_600 ),
inference(resolution,[],[f12906,f161]) ).
fof(f13866,plain,
( ~ mem(e,sK2(sK3(sF9)))
| subq(sF5,sK2(sK3(sF9)))
| spl10_600 ),
inference(superposition,[],[f52,f12909]) ).
fof(f15708,plain,
( ! [X0] :
( mem(e,X0)
| subq(sF5,sF8)
| ~ subq(sF5,sK2(X0))
| ~ atleast3p(X0) )
| ~ spl10_43 ),
inference(superposition,[],[f6956,f617]) ).
fof(f15717,plain,
( ! [X0] :
( mem(sF5,X0)
| subq(sF6,sF5)
| ~ subq(sF6,sK2(X0))
| ~ atleast3p(X0) )
| ~ spl10_86 ),
inference(superposition,[],[f6956,f1530]) ).
fof(f15814,plain,
( ! [X0] :
( mem(sF5,X0)
| ~ subq(sF6,sK2(X0))
| ~ atleast3p(X0) )
| ~ spl10_86
| spl10_98 ),
inference(forward_subsumption_resolution,[],[f15717,f1790]) ).
fof(f15822,definition,
( spl10_660
<=> ! [X0] :
( mem(sF5,X0)
| ~ atleast3p(X0)
| ~ subq(sF6,sK2(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl10_660])],[avatar_definition]) ).
fof(f15823,plain,
( ! [X0] :
( ~ subq(sF6,sK2(X0))
| ~ atleast3p(X0)
| mem(sF5,X0) )
| ~ spl10_660 ),
inference(avatar_component_clause,[],[f15822]) ).
fof(f15837,plain,
( ! [X0] :
( ~ subq(sF5,sK2(X0))
| mem(e,X0)
| ~ atleast3p(X0) )
| ~ spl10_43
| spl10_80 ),
inference(forward_subsumption_resolution,[],[f15708,f1457]) ).
fof(f15904,plain,
( spl10_660
| ~ spl10_86
| spl10_98 ),
inference(avatar_split_clause,[],[f15814,f1789,f1528,f15822]) ).
fof(f17484,definition,
( spl10_683
<=> subq(sF6,sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_683])],[avatar_definition]) ).
fof(f17485,plain,
( ~ subq(sF6,sK2(sK3(sF9)))
| spl10_683 ),
inference(avatar_component_clause,[],[f17484]) ).
fof(f17486,plain,
( subq(sF6,sK2(sK3(sF9)))
| ~ spl10_683 ),
inference(avatar_component_clause,[],[f17484]) ).
fof(f17488,definition,
( spl10_684
<=> mem(sF5,sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_684])],[avatar_definition]) ).
fof(f17489,plain,
( mem(sF5,sK2(sK3(sF9)))
| ~ spl10_684 ),
inference(avatar_component_clause,[],[f17488]) ).
fof(f17490,plain,
( ~ mem(sF5,sK2(sK3(sF9)))
| spl10_684 ),
inference(avatar_component_clause,[],[f17488]) ).
fof(f17512,definition,
( spl10_686
<=> sF6 = sK0(sF7,sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_686])],[avatar_definition]) ).
fof(f17514,plain,
( sF6 = sK0(sF7,sK2(sK3(sF9)))
| ~ spl10_686 ),
inference(avatar_component_clause,[],[f17512]) ).
fof(f17523,plain,
( ~ atleast3p(sK3(sF9))
| mem(sF5,sK3(sF9))
| ~ spl10_660
| ~ spl10_683 ),
inference(resolution,[],[f17486,f15823]) ).
fof(f17535,plain,
( mem(sF5,sK3(sF9))
| ~ spl10_150
| ~ spl10_660
| ~ spl10_683 ),
inference(forward_subsumption_resolution,[],[f17523,f3268]) ).
fof(f17539,plain,
( $false
| ~ spl10_150
| spl10_170
| ~ spl10_660
| ~ spl10_683 ),
inference(forward_subsumption_resolution,[],[f17535,f3383]) ).
fof(f17540,plain,
( ~ spl10_150
| spl10_170
| ~ spl10_660
| ~ spl10_683 ),
inference(avatar_contradiction_clause,[],[f17539]) ).
fof(f17573,plain,
( sF5 = sK0(sF6,sK2(sK3(sF9)))
| spl10_683 ),
inference(resolution,[],[f17485,f138]) ).
fof(f17684,definition,
( spl10_693
<=> mem(sF6,p(sK2(sK3(sF9)))) ),
introduced(definition,[new_symbols(definition,[spl10_693])],[avatar_definition]) ).
fof(f17685,plain,
( mem(sF6,p(sK2(sK3(sF9))))
| ~ spl10_693 ),
inference(avatar_component_clause,[],[f17684]) ).
fof(f17686,plain,
( ~ mem(sF6,p(sK2(sK3(sF9))))
| spl10_693 ),
inference(avatar_component_clause,[],[f17684]) ).
fof(f17721,plain,
( ~ subq(sF6,sK2(sK3(sF9)))
| spl10_693 ),
inference(resolution,[],[f17686,f66]) ).
fof(f18967,definition,
( spl10_708
<=> sF5 = sK0(sF6,p(sF5)) ),
introduced(definition,[new_symbols(definition,[spl10_708])],[avatar_definition]) ).
fof(f18968,plain,
( sF5 != sK0(sF6,p(sF5))
| spl10_708 ),
inference(avatar_component_clause,[],[f18967]) ).
fof(f18969,plain,
( sF5 = sK0(sF6,p(sF5))
| ~ spl10_708 ),
inference(avatar_component_clause,[],[f18967]) ).
fof(f19028,plain,
( ~ subq(sF5,sF5)
| subq(sF6,p(sF5))
| ~ spl10_708 ),
inference(superposition,[],[f708,f18969]) ).
fof(f19052,plain,
( subq(sF6,p(sF5))
| ~ spl10_708 ),
inference(forward_subsumption_resolution,[],[f19028,f135]) ).
fof(f22362,plain,
! [X0,X1] :
( subq(X0,X1)
| ~ subq(X0,sK3(sF9))
| ~ atleast4p(sF9)
| mem(sK0(X0,X1),sF8)
| mem(sK0(X0,X1),sF5) ),
inference(resolution,[],[f6957,f109]) ).
fof(f22608,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF8)
| ~ subq(X0,sK3(sF9))
| subq(X0,X1)
| mem(sK0(X0,X1),sF5) ),
inference(forward_subsumption_resolution,[],[f22362,f91]) ).
fof(f22663,plain,
! [X0] :
( ~ subq(X0,sK3(sF9))
| subq(X0,sF9)
| mem(sK0(X0,sF9),sF5)
| subq(X0,sF9) ),
inference(resolution,[],[f22608,f221]) ).
fof(f22791,plain,
! [X0] :
( ~ subq(X0,sK3(sF9))
| subq(X0,sF9)
| mem(sK0(X0,sF9),sF5) ),
inference(duplicate_literal_removal,[],[f22663]) ).
fof(f22819,plain,
! [X0] :
( ~ subq(X0,sK3(sF9))
| subq(X0,sF9) ),
inference(forward_subsumption_resolution,[],[f22791,f273]) ).
fof(f22839,plain,
( subq(sK2(sK3(sF9)),sF9)
| ~ atleast3p(sK3(sF9)) ),
inference(resolution,[],[f22819,f71]) ).
fof(f22872,plain,
( ~ atleast3p(sK3(sF9))
| spl10_485 ),
inference(forward_subsumption_resolution,[],[f22839,f10752]) ).
fof(f22877,plain,
( $false
| ~ spl10_150
| spl10_485 ),
inference(forward_subsumption_resolution,[],[f22872,f3268]) ).
fof(f22878,plain,
( ~ spl10_150
| spl10_485 ),
inference(avatar_contradiction_clause,[],[f22877]) ).
fof(f22884,plain,
( ~ atleast2p(sK2(sK3(sF9)))
| sF6 = sK1(sK2(sK3(sF9)))
| sF5 = sK1(sK2(sK3(sF9)))
| e = sK1(sK2(sK3(sF9)))
| ~ spl10_4
| ~ spl10_485 ),
inference(resolution,[],[f10751,f7436]) ).
fof(f22885,plain,
( subq(sK2(sK3(sF9)),sF8)
| e = sK0(sK2(sK3(sF9)),sF8)
| ~ spl10_4
| ~ spl10_485 ),
inference(resolution,[],[f10751,f3106]) ).
fof(f22886,plain,
( subq(sK2(sK3(sF9)),sF5)
| sF6 = sK0(sK2(sK3(sF9)),sF5)
| sF5 = sK0(sK2(sK3(sF9)),sF5)
| ~ spl10_485 ),
inference(resolution,[],[f10751,f902]) ).
fof(f22893,plain,
( sF6 = sK0(sK2(sK3(sF9)),sF5)
| sF5 = sK0(sK2(sK3(sF9)),sF5)
| ~ spl10_485
| spl10_498 ),
inference(forward_subsumption_resolution,[],[f22886,f10860]) ).
fof(f22894,plain,
( e = sK0(sK2(sK3(sF9)),sF8)
| ~ spl10_4
| spl10_484
| ~ spl10_485 ),
inference(forward_subsumption_resolution,[],[f22885,f10747]) ).
fof(f22896,definition,
( spl10_831
<=> sF5 = sK0(sK2(sK3(sF9)),sF5) ),
introduced(definition,[new_symbols(definition,[spl10_831])],[avatar_definition]) ).
fof(f22898,plain,
( sF5 = sK0(sK2(sK3(sF9)),sF5)
| ~ spl10_831 ),
inference(avatar_component_clause,[],[f22896]) ).
fof(f22900,definition,
( spl10_832
<=> sF6 = sK0(sK2(sK3(sF9)),sF5) ),
introduced(definition,[new_symbols(definition,[spl10_832])],[avatar_definition]) ).
fof(f22902,plain,
( sF6 = sK0(sK2(sK3(sF9)),sF5)
| ~ spl10_832 ),
inference(avatar_component_clause,[],[f22900]) ).
fof(f22903,plain,
( spl10_831
| spl10_832
| ~ spl10_485
| spl10_498 ),
inference(avatar_split_clause,[],[f22893,f10858,f10750,f22900,f22896]) ).
fof(f22909,plain,
( mem(sF5,sK2(sK3(sF9)))
| subq(sK2(sK3(sF9)),sF5)
| ~ spl10_831 ),
inference(superposition,[],[f51,f22898]) ).
fof(f22940,plain,
( subq(sK2(sK3(sF9)),sF5)
| spl10_684
| ~ spl10_831 ),
inference(forward_subsumption_resolution,[],[f22909,f17490]) ).
fof(f22943,plain,
( $false
| spl10_498
| spl10_684
| ~ spl10_831 ),
inference(forward_subsumption_resolution,[],[f22940,f10860]) ).
fof(f22944,plain,
( spl10_498
| spl10_684
| ~ spl10_831 ),
inference(avatar_contradiction_clause,[],[f22943]) ).
fof(f22953,plain,
( mem(sF6,sK2(sK3(sF9)))
| subq(sK2(sK3(sF9)),sF5)
| ~ spl10_832 ),
inference(superposition,[],[f51,f22902]) ).
fof(f22992,plain,
( mem(e,sK2(sK3(sF9)))
| subq(sK2(sK3(sF9)),sF8)
| ~ spl10_4
| spl10_484
| ~ spl10_485 ),
inference(superposition,[],[f51,f22894]) ).
fof(f23022,plain,
( subq(sK2(sK3(sF9)),sF8)
| ~ spl10_4
| spl10_175
| spl10_484
| ~ spl10_485 ),
inference(forward_subsumption_resolution,[],[f22992,f3512]) ).
fof(f23023,plain,
( $false
| ~ spl10_4
| spl10_175
| spl10_484
| ~ spl10_485 ),
inference(forward_subsumption_resolution,[],[f23022,f10747]) ).
fof(f23024,plain,
( ~ spl10_4
| spl10_175
| spl10_484
| ~ spl10_485 ),
inference(avatar_contradiction_clause,[],[f23023]) ).
fof(f23025,plain,
( ~ spl10_482
| ~ spl10_153
| spl10_174 ),
inference(avatar_split_clause,[],[f5080,f3505,f3279,f10717]) ).
fof(f23068,definition,
( spl10_842
<=> sF5 = sK1(sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_842])],[avatar_definition]) ).
fof(f23069,plain,
( sF5 != sK1(sK2(sK3(sF9)))
| spl10_842 ),
inference(avatar_component_clause,[],[f23068]) ).
fof(f23070,plain,
( sF5 = sK1(sK2(sK3(sF9)))
| ~ spl10_842 ),
inference(avatar_component_clause,[],[f23068]) ).
fof(f23094,definition,
( spl10_848
<=> e = sK1(sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_848])],[avatar_definition]) ).
fof(f23096,plain,
( e = sK1(sK2(sK3(sF9)))
| ~ spl10_848 ),
inference(avatar_component_clause,[],[f23094]) ).
fof(f23276,plain,
( sF6 = sK1(sK2(sK3(sF9)))
| sF5 = sK1(sK2(sK3(sF9)))
| e = sK1(sK2(sK3(sF9)))
| ~ spl10_4
| ~ spl10_480
| ~ spl10_485 ),
inference(forward_subsumption_resolution,[],[f22884,f10710]) ).
fof(f23279,plain,
( subq(sK2(sK3(sF9)),sF5)
| spl10_482
| ~ spl10_832 ),
inference(forward_subsumption_resolution,[],[f22953,f10718]) ).
fof(f23280,plain,
( subq(sF5,sK2(sK3(sF9)))
| ~ spl10_175
| spl10_600 ),
inference(forward_subsumption_resolution,[],[f13866,f3511]) ).
fof(f23295,plain,
( $false
| ~ spl10_175
| spl10_600 ),
inference(forward_subsumption_resolution,[],[f23280,f12906]) ).
fof(f23296,plain,
( ~ spl10_175
| spl10_600 ),
inference(avatar_contradiction_clause,[],[f23295]) ).
fof(f24137,plain,
( subq(sK2(sK3(sF9)),sF7)
| sF5 = sK0(sK2(sK3(sF9)),sF7)
| ~ spl10_484 ),
inference(resolution,[],[f10746,f2561]) ).
fof(f24146,plain,
( sF5 = sK0(sK2(sK3(sF9)),sF7)
| ~ spl10_484
| spl10_536 ),
inference(forward_subsumption_resolution,[],[f24137,f11216]) ).
fof(f24228,plain,
( mem(sF5,sK2(sK3(sF9)))
| subq(sK2(sK3(sF9)),sF7)
| ~ spl10_484
| spl10_536 ),
inference(superposition,[],[f51,f24146]) ).
fof(f24260,plain,
( subq(sK2(sK3(sF9)),sF7)
| ~ spl10_484
| spl10_536
| spl10_684 ),
inference(forward_subsumption_resolution,[],[f24228,f17490]) ).
fof(f24262,plain,
( $false
| ~ spl10_484
| spl10_536
| spl10_684 ),
inference(forward_subsumption_resolution,[],[f24260,f11216]) ).
fof(f24263,plain,
( ~ spl10_484
| spl10_536
| spl10_684 ),
inference(avatar_contradiction_clause,[],[f24262]) ).
fof(f24653,plain,
( sF7 = sK2(sK3(sF9))
| sF6 = sK0(sF7,sK2(sK3(sF9)))
| ~ spl10_536 ),
inference(resolution,[],[f11215,f401]) ).
fof(f24659,plain,
( sF7 = sK2(sK3(sF9))
| ~ subq(sF7,sK2(sK3(sF9)))
| ~ spl10_536 ),
inference(resolution,[],[f11215,f53]) ).
fof(f24661,definition,
( spl10_899
<=> subq(sF7,sK2(sK3(sF9))) ),
introduced(definition,[new_symbols(definition,[spl10_899])],[avatar_definition]) ).
fof(f24665,definition,
( spl10_900
<=> sF7 = sK2(sK3(sF9)) ),
introduced(definition,[new_symbols(definition,[spl10_900])],[avatar_definition]) ).
fof(f24667,plain,
( sF7 = sK2(sK3(sF9))
| ~ spl10_900 ),
inference(avatar_component_clause,[],[f24665]) ).
fof(f24668,plain,
( ~ spl10_899
| spl10_900
| ~ spl10_536 ),
inference(avatar_split_clause,[],[f24659,f11214,f24665,f24661]) ).
fof(f24669,plain,
( spl10_686
| spl10_900
| ~ spl10_536 ),
inference(avatar_split_clause,[],[f24653,f11214,f24665,f17512]) ).
fof(f24681,plain,
( ~ subq(sF7,p(sF6))
| spl10_483
| ~ spl10_900 ),
inference(superposition,[],[f10724,f24667]) ).
fof(f24730,plain,
( atleast2p(sF7)
| ~ atleast3p(sK3(sF9))
| ~ spl10_900 ),
inference(superposition,[],[f70,f24667]) ).
fof(f24760,plain,
( ~ atleast3p(sK3(sF9))
| spl10_17
| ~ spl10_900 ),
inference(forward_subsumption_resolution,[],[f24730,f360]) ).
fof(f24779,plain,
( $false
| spl10_17
| ~ spl10_150
| ~ spl10_900 ),
inference(forward_subsumption_resolution,[],[f24760,f3268]) ).
fof(f24780,plain,
( spl10_17
| ~ spl10_150
| ~ spl10_900 ),
inference(avatar_contradiction_clause,[],[f24779]) ).
fof(f24789,plain,
( ~ mem(sF6,sK2(sK3(sF9)))
| subq(sF7,sK2(sK3(sF9)))
| ~ spl10_686 ),
inference(superposition,[],[f52,f17514]) ).
fof(f24815,plain,
( subq(sF7,sK2(sK3(sF9)))
| ~ spl10_482
| ~ spl10_686 ),
inference(forward_subsumption_resolution,[],[f24789,f10719]) ).
fof(f24840,plain,
( sF6 = sK0(sF7,p(sK1(sF7)))
| ~ spl10_17 ),
inference(forward_subsumption_resolution,[],[f1263,f359]) ).
fof(f24879,plain,
( sF6 = sK0(sF7,p(sF6))
| ~ spl10_17
| ~ spl10_18 ),
inference(forward_demodulation,[],[f24840,f365]) ).
fof(f24906,plain,
( $false
| ~ spl10_17
| ~ spl10_18
| spl10_461 ),
inference(forward_subsumption_resolution,[],[f24879,f10115]) ).
fof(f24907,plain,
( ~ spl10_17
| ~ spl10_18
| spl10_461 ),
inference(avatar_contradiction_clause,[],[f24906]) ).
fof(f25133,plain,
( spl10_498
| spl10_482
| ~ spl10_832 ),
inference(avatar_split_clause,[],[f23279,f22900,f10717,f10858]) ).
fof(f25280,plain,
( ~ atleast2p(sK2(sK3(sF9)))
| ~ subq(sK2(sK3(sF9)),sF8)
| ~ subq(sF7,sF7)
| sF5 = sK1(sK2(sK3(sF9)))
| spl10_479 ),
inference(resolution,[],[f10682,f8597]) ).
fof(f25437,plain,
( mem(sF5,sK3(sF9))
| ~ atleast3p(sK3(sF9))
| ~ spl10_842 ),
inference(superposition,[],[f11736,f23070]) ).
fof(f25446,plain,
( mem(sF5,sK2(sK3(sF9)))
| ~ atleast2p(sK2(sK3(sF9)))
| ~ spl10_842 ),
inference(superposition,[],[f68,f23070]) ).
fof(f25473,plain,
( ~ atleast2p(sK2(sK3(sF9)))
| spl10_684
| ~ spl10_842 ),
inference(forward_subsumption_resolution,[],[f25446,f17490]) ).
fof(f25476,plain,
( ~ atleast3p(sK3(sF9))
| spl10_170
| ~ spl10_842 ),
inference(forward_subsumption_resolution,[],[f25437,f3383]) ).
fof(f25479,plain,
( $false
| ~ spl10_480
| spl10_684
| ~ spl10_842 ),
inference(forward_subsumption_resolution,[],[f25473,f10710]) ).
fof(f25480,plain,
( ~ spl10_480
| spl10_684
| ~ spl10_842 ),
inference(avatar_contradiction_clause,[],[f25479]) ).
fof(f25482,plain,
( $false
| ~ spl10_150
| spl10_170
| ~ spl10_842 ),
inference(forward_subsumption_resolution,[],[f25476,f3268]) ).
fof(f25483,plain,
( ~ spl10_150
| spl10_170
| ~ spl10_842 ),
inference(avatar_contradiction_clause,[],[f25482]) ).
fof(f25725,plain,
( mem(e,sK3(sF9))
| ~ atleast3p(sK3(sF9))
| ~ spl10_43
| spl10_80
| ~ spl10_600 ),
inference(resolution,[],[f12905,f15837]) ).
fof(f25735,plain,
( sF5 = sK2(sK3(sF9))
| ~ subq(sK2(sK3(sF9)),sF5)
| ~ spl10_600 ),
inference(resolution,[],[f12905,f53]) ).
fof(f25736,plain,
( sF5 = sK2(sK3(sF9))
| ~ spl10_498
| ~ spl10_600 ),
inference(forward_subsumption_resolution,[],[f25735,f10859]) ).
fof(f25782,plain,
( atleast2p(sF5)
| ~ atleast3p(sK3(sF9))
| ~ spl10_498
| ~ spl10_600 ),
inference(superposition,[],[f70,f25736]) ).
fof(f25812,plain,
( ~ atleast3p(sK3(sF9))
| spl10_23
| ~ spl10_498
| ~ spl10_600 ),
inference(forward_subsumption_resolution,[],[f25782,f388]) ).
fof(f25829,plain,
( $false
| spl10_23
| ~ spl10_150
| ~ spl10_498
| ~ spl10_600 ),
inference(forward_subsumption_resolution,[],[f25812,f3268]) ).
fof(f25830,plain,
( spl10_23
| ~ spl10_150
| ~ spl10_498
| ~ spl10_600 ),
inference(avatar_contradiction_clause,[],[f25829]) ).
fof(f25861,plain,
( $false
| ~ spl10_23
| ~ spl10_61 ),
inference(forward_subsumption_resolution,[],[f8550,f387]) ).
fof(f25862,plain,
( ~ spl10_23
| ~ spl10_61 ),
inference(avatar_contradiction_clause,[],[f25861]) ).
fof(f25978,plain,
( spl10_194
| ~ spl10_60 ),
inference(avatar_split_clause,[],[f4175,f937,f4155]) ).
fof(f26663,plain,
( ~ subq(sK2(sK3(sF9)),p(e))
| ~ atleast2p(sK2(sK3(sF9)))
| ~ spl10_848 ),
inference(superposition,[],[f67,f23096]) ).
fof(f26685,plain,
( ~ subq(sK2(sK3(sF9)),p(e))
| ~ spl10_480
| ~ spl10_848 ),
inference(forward_subsumption_resolution,[],[f26663,f10710]) ).
fof(f26686,plain,
( ~ subq(sF5,p(e))
| ~ spl10_480
| ~ spl10_498
| ~ spl10_600
| ~ spl10_848 ),
inference(forward_demodulation,[],[f26685,f25736]) ).
fof(f26687,plain,
( $false
| ~ spl10_194
| ~ spl10_480
| ~ spl10_498
| ~ spl10_600
| ~ spl10_848 ),
inference(forward_subsumption_resolution,[],[f26686,f4156]) ).
fof(f26688,plain,
( ~ spl10_194
| ~ spl10_480
| ~ spl10_498
| ~ spl10_600
| ~ spl10_848 ),
inference(avatar_contradiction_clause,[],[f26687]) ).
fof(f26746,plain,
( sF5 = sK1(sK2(sK3(sF9)))
| e = sK1(sK2(sK3(sF9)))
| ~ spl10_4
| ~ spl10_480
| ~ spl10_485
| spl10_535 ),
inference(forward_subsumption_resolution,[],[f23276,f11119]) ).
fof(f26845,plain,
( mem(e,sK3(sF9))
| ~ spl10_43
| spl10_80
| ~ spl10_150
| ~ spl10_600 ),
inference(forward_subsumption_resolution,[],[f25725,f3268]) ).
fof(f27672,plain,
( $false
| ~ spl10_43
| spl10_80
| spl10_122
| ~ spl10_150
| ~ spl10_600 ),
inference(forward_subsumption_resolution,[],[f26845,f2842]) ).
fof(f27673,plain,
( ~ spl10_43
| spl10_80
| spl10_122
| ~ spl10_150
| ~ spl10_600 ),
inference(avatar_contradiction_clause,[],[f27672]) ).
fof(f28182,plain,
( subq(sK2(sK3(sF9)),sF6)
| sF6 = sK0(sK2(sK3(sF9)),sF6)
| ~ spl10_484 ),
inference(resolution,[],[f10746,f993]) ).
fof(f28193,plain,
( sF6 = sK0(sK2(sK3(sF9)),sF6)
| ~ spl10_484
| spl10_537 ),
inference(forward_subsumption_resolution,[],[f28182,f11221]) ).
fof(f28229,plain,
( mem(sF6,sK2(sK3(sF9)))
| subq(sK2(sK3(sF9)),sF6)
| ~ spl10_484
| spl10_537 ),
inference(superposition,[],[f51,f28193]) ).
fof(f28231,plain,
( ! [X0] :
( mem(sF6,X0)
| ~ subq(sK2(sK3(sF9)),X0)
| subq(sK2(sK3(sF9)),sF6) )
| ~ spl10_484
| spl10_537 ),
inference(superposition,[],[f152,f28193]) ).
fof(f28259,plain,
( ! [X0] :
( mem(sF6,X0)
| ~ subq(sK2(sK3(sF9)),X0) )
| ~ spl10_484
| spl10_537 ),
inference(forward_subsumption_resolution,[],[f28231,f11221]) ).
fof(f28260,plain,
( subq(sK2(sK3(sF9)),sF6)
| spl10_482
| ~ spl10_484
| spl10_537 ),
inference(forward_subsumption_resolution,[],[f28229,f10718]) ).
fof(f28262,plain,
( spl10_481
| ~ spl10_484
| spl10_537 ),
inference(avatar_split_clause,[],[f28259,f11219,f10745,f10713]) ).
fof(f28263,plain,
( $false
| spl10_482
| ~ spl10_484
| spl10_537 ),
inference(forward_subsumption_resolution,[],[f28260,f11221]) ).
fof(f28264,plain,
( spl10_482
| ~ spl10_484
| spl10_537 ),
inference(avatar_contradiction_clause,[],[f28263]) ).
fof(f28272,plain,
( ~ mem(sF5,sK2(sK3(sF9)))
| subq(sF6,sK2(sK3(sF9)))
| spl10_683 ),
inference(superposition,[],[f52,f17573]) ).
fof(f28301,plain,
( subq(sF6,sK2(sK3(sF9)))
| spl10_683
| ~ spl10_684 ),
inference(forward_subsumption_resolution,[],[f28272,f17489]) ).
fof(f28303,plain,
( $false
| spl10_683
| ~ spl10_684 ),
inference(forward_subsumption_resolution,[],[f28301,f17485]) ).
fof(f28304,plain,
( spl10_683
| ~ spl10_684 ),
inference(avatar_contradiction_clause,[],[f28303]) ).
fof(f28307,plain,
( $false
| ~ spl10_683
| spl10_693 ),
inference(forward_subsumption_resolution,[],[f17721,f17486]) ).
fof(f28308,plain,
( ~ spl10_683
| spl10_693 ),
inference(avatar_contradiction_clause,[],[f28307]) ).
fof(f28319,plain,
( sF6 = sK2(sK3(sF9))
| ~ subq(sK2(sK3(sF9)),sF6)
| ~ spl10_683 ),
inference(resolution,[],[f17486,f53]) ).
fof(f28320,plain,
( sF6 = sK2(sK3(sF9))
| ~ spl10_537
| ~ spl10_683 ),
inference(forward_subsumption_resolution,[],[f28319,f11220]) ).
fof(f28357,plain,
( atleast2p(sF6)
| ~ atleast3p(sK3(sF9))
| ~ spl10_537
| ~ spl10_683 ),
inference(superposition,[],[f70,f28320]) ).
fof(f28387,plain,
( ~ atleast3p(sK3(sF9))
| spl10_20
| ~ spl10_537
| ~ spl10_683 ),
inference(forward_subsumption_resolution,[],[f28357,f374]) ).
fof(f28396,plain,
( $false
| spl10_20
| ~ spl10_150
| ~ spl10_537
| ~ spl10_683 ),
inference(forward_subsumption_resolution,[],[f28387,f3268]) ).
fof(f28397,plain,
( spl10_20
| ~ spl10_150
| ~ spl10_537
| ~ spl10_683 ),
inference(avatar_contradiction_clause,[],[f28396]) ).
fof(f28401,plain,
( sF5 = sK0(sF6,p(sK1(sF6)))
| ~ spl10_20 ),
inference(forward_subsumption_resolution,[],[f1262,f373]) ).
fof(f28440,plain,
( sF5 = sK0(sF6,p(sF5))
| ~ spl10_20
| ~ spl10_21 ),
inference(forward_demodulation,[],[f28401,f379]) ).
fof(f28658,plain,
( subq(sF6,sK2(sK3(sF9)))
| ~ spl10_693 ),
inference(resolution,[],[f17685,f65]) ).
fof(f29472,plain,
( ~ subq(sF6,p(sF5))
| ~ atleast2p(sF6)
| ~ spl10_21 ),
inference(superposition,[],[f67,f379]) ).
fof(f29504,plain,
( $false
| ~ spl10_20
| ~ spl10_21
| spl10_708 ),
inference(forward_subsumption_resolution,[],[f28440,f18968]) ).
fof(f29505,plain,
( ~ spl10_20
| ~ spl10_21
| spl10_708 ),
inference(avatar_contradiction_clause,[],[f29504]) ).
fof(f29510,plain,
( ~ atleast2p(sF6)
| ~ spl10_21
| ~ spl10_708 ),
inference(forward_subsumption_resolution,[],[f29472,f19052]) ).
fof(f29513,plain,
( $false
| ~ spl10_20
| ~ spl10_21
| ~ spl10_708 ),
inference(forward_subsumption_resolution,[],[f29510,f373]) ).
fof(f29514,plain,
( ~ spl10_20
| ~ spl10_21
| ~ spl10_708 ),
inference(avatar_contradiction_clause,[],[f29513]) ).
fof(f29994,plain,
( mem(sF6,sK3(sF9))
| ~ spl10_150
| ~ spl10_481 ),
inference(forward_subsumption_resolution,[],[f11323,f3268]) ).
fof(f29995,plain,
( spl10_482
| ~ spl10_481 ),
inference(avatar_split_clause,[],[f11324,f10713,f10717]) ).
fof(f29996,plain,
( spl10_899
| ~ spl10_482
| ~ spl10_686 ),
inference(avatar_split_clause,[],[f24815,f17512,f10717,f24661]) ).
fof(f30577,plain,
( $false
| ~ spl10_150
| spl10_173
| ~ spl10_481 ),
inference(forward_subsumption_resolution,[],[f29994,f3406]) ).
fof(f30578,plain,
( ~ spl10_150
| spl10_173
| ~ spl10_481 ),
inference(avatar_contradiction_clause,[],[f30577]) ).
fof(f30611,plain,
( $false
| ~ spl10_4
| spl10_17
| ~ spl10_23
| ~ spl10_46 ),
inference(forward_subsumption_resolution,[],[f2140,f387]) ).
fof(f30612,plain,
( ~ spl10_4
| spl10_17
| ~ spl10_23
| ~ spl10_46 ),
inference(avatar_contradiction_clause,[],[f30611]) ).
fof(f30641,plain,
( sF6 != sK0(sK3(sF9),sK2(sK3(sF9)))
| ~ spl10_46
| spl10_151 ),
inference(forward_demodulation,[],[f3272,f631]) ).
fof(f30645,plain,
( spl10_173
| ~ spl10_153
| spl10_174 ),
inference(avatar_split_clause,[],[f5103,f3505,f3279,f3405]) ).
fof(f30740,plain,
( $false
| ~ spl10_90
| spl10_684 ),
inference(forward_subsumption_resolution,[],[f17490,f2206]) ).
fof(f30741,plain,
( ~ spl10_90
| spl10_684 ),
inference(avatar_contradiction_clause,[],[f30740]) ).
fof(f30773,plain,
( e = sK1(sK2(sK3(sF9)))
| ~ spl10_4
| ~ spl10_480
| ~ spl10_485
| spl10_535
| spl10_842 ),
inference(forward_subsumption_resolution,[],[f26746,f23069]) ).
fof(f30774,plain,
( ~ subq(sK2(sK3(sF9)),sF8)
| ~ subq(sF7,sF7)
| sF5 = sK1(sK2(sK3(sF9)))
| spl10_479
| ~ spl10_480 ),
inference(forward_subsumption_resolution,[],[f25280,f10710]) ).
fof(f30815,plain,
( sF5 = sK0(sF9,sK3(sF9))
| e = sK0(sF9,sK3(sF9))
| ~ spl10_4
| spl10_120
| spl10_121 ),
inference(forward_subsumption_resolution,[],[f3597,f2816]) ).
fof(f30960,plain,
( $false
| ~ spl10_46
| spl10_151
| ~ spl10_153 ),
inference(forward_subsumption_resolution,[],[f30641,f3281]) ).
fof(f30961,plain,
( ~ spl10_46
| spl10_151
| ~ spl10_153 ),
inference(avatar_contradiction_clause,[],[f30960]) ).
fof(f31023,plain,
( ~ subq(sK2(sK3(sF9)),sF8)
| sF5 = sK1(sK2(sK3(sF9)))
| spl10_479
| ~ spl10_480 ),
inference(forward_subsumption_resolution,[],[f30774,f135]) ).
fof(f31050,plain,
( e = sK0(sF9,sK3(sF9))
| ~ spl10_4
| spl10_119
| spl10_120
| spl10_121 ),
inference(forward_subsumption_resolution,[],[f30815,f2812]) ).
fof(f31163,plain,
( ~ subq(sK2(sK3(sF9)),sF8)
| spl10_479
| ~ spl10_480
| spl10_842 ),
inference(forward_subsumption_resolution,[],[f31023,f23069]) ).
fof(f31182,plain,
( sF6 = sK0(sF9,sK3(sF9))
| ~ spl10_4
| ~ spl10_46
| spl10_119
| spl10_120
| spl10_121 ),
inference(forward_demodulation,[],[f31050,f631]) ).
fof(f31254,plain,
( $false
| ~ spl10_4
| ~ spl10_46
| spl10_119
| spl10_120
| spl10_121 ),
inference(forward_subsumption_resolution,[],[f31182,f2816]) ).
fof(f31255,plain,
( ~ spl10_4
| ~ spl10_46
| spl10_119
| spl10_120
| spl10_121 ),
inference(avatar_contradiction_clause,[],[f31254]) ).
fof(f31434,plain,
( $false
| ~ spl10_461
| spl10_483
| ~ spl10_900 ),
inference(forward_subsumption_resolution,[],[f24681,f10135]) ).
fof(f31435,plain,
( ~ spl10_461
| spl10_483
| ~ spl10_900 ),
inference(avatar_contradiction_clause,[],[f31434]) ).
fof(f31524,plain,
( subq(sF6,sF7)
| ~ spl10_693
| ~ spl10_900 ),
inference(forward_demodulation,[],[f28658,f24667]) ).
fof(f31742,plain,
( $false
| spl10_214
| ~ spl10_693
| ~ spl10_900 ),
inference(forward_subsumption_resolution,[],[f31524,f4772]) ).
fof(f31743,plain,
( spl10_214
| ~ spl10_693
| ~ spl10_900 ),
inference(avatar_contradiction_clause,[],[f31742]) ).
fof(f32161,plain,
( ~ spl10_684
| ~ spl10_152
| spl10_174 ),
inference(avatar_split_clause,[],[f3607,f3505,f3275,f17488]) ).
fof(f32174,plain,
( ~ spl10_536
| spl10_479
| ~ spl10_480 ),
inference(avatar_split_clause,[],[f10739,f10709,f10681,f11214]) ).
fof(f32176,plain,
( ~ spl10_484
| spl10_479
| ~ spl10_480
| spl10_842 ),
inference(avatar_split_clause,[],[f31163,f23068,f10709,f10681,f10745]) ).
fof(f32180,plain,
( spl10_848
| ~ spl10_4
| ~ spl10_480
| ~ spl10_485
| spl10_535
| spl10_842 ),
inference(avatar_split_clause,[],[f30773,f23068,f11118,f10750,f10709,f182,f23094]) ).
fof(f32317,plain,
( ! [X0] :
( mem(sF6,X0)
| ~ subq(sK2(sK3(sF9)),X0) )
| ~ spl10_482 ),
inference(resolution,[],[f10719,f50]) ).
fof(f32318,plain,
( spl10_481
| ~ spl10_482 ),
inference(avatar_split_clause,[],[f32317,f10717,f10713]) ).
cnf(s2,plain,
( ~ spl10_3
| spl10_4 ),
inference(sat_conversion,[],[f185]) ).
cnf(s3,plain,
spl10_3,
inference(sat_conversion,[],[f236]) ).
cnf(s4,plain,
( ~ spl10_5
| spl10_6 ),
inference(sat_conversion,[],[f257]) ).
cnf(s10,plain,
( ~ spl10_17
| spl10_18 ),
inference(sat_conversion,[],[f366]) ).
cnf(s12,plain,
( ~ spl10_20
| spl10_21 ),
inference(sat_conversion,[],[f380]) ).
cnf(s31,plain,
( ~ spl10_41
| spl10_48 ),
inference(sat_conversion,[],[f647]) ).
cnf(s41,plain,
( spl10_59
| spl10_60
| spl10_61 ),
inference(sat_conversion,[],[f944]) ).
cnf(s50,plain,
( ~ spl10_6
| spl10_41 ),
inference(sat_conversion,[],[f1397]) ).
cnf(s66,plain,
( spl10_43
| spl10_93 ),
inference(sat_conversion,[],[f1629]) ).
cnf(s72,plain,
( ~ spl10_46
| spl10_90 ),
inference(sat_conversion,[],[f1661]) ).
cnf(s74,plain,
( ~ spl10_80
| spl10_93 ),
inference(sat_conversion,[],[f1675]) ).
cnf(s92,plain,
~ spl10_48,
inference(sat_conversion,[],[f1899]) ).
cnf(s118,plain,
( spl10_86
| spl10_99 ),
inference(sat_conversion,[],[f2043]) ).
cnf(s135,plain,
( ~ spl10_4
| spl10_48
| ~ spl10_99 ),
inference(sat_conversion,[],[f2198]) ).
cnf(s140,plain,
( ~ spl10_98
| spl10_99 ),
inference(sat_conversion,[],[f2247]) ).
cnf(s142,plain,
( ~ spl10_4
| spl10_46
| spl10_48
| ~ spl10_93 ),
inference(sat_conversion,[],[f2299]) ).
cnf(s153,plain,
( ~ spl10_4
| spl10_118
| spl10_119
| spl10_120 ),
inference(sat_conversion,[],[f2818]) ).
cnf(s154,plain,
( ~ spl10_118
| spl10_121
| ~ spl10_122 ),
inference(sat_conversion,[],[f2843]) ).
cnf(s172,plain,
( ~ spl10_4
| ~ spl10_150
| spl10_151
| spl10_152
| spl10_153 ),
inference(sat_conversion,[],[f3282]) ).
cnf(s201,plain,
spl10_150,
inference(sat_conversion,[],[f3491]) ).
cnf(s203,plain,
( ~ spl10_151
| spl10_174
| ~ spl10_175 ),
inference(sat_conversion,[],[f3513]) ).
cnf(s204,plain,
( spl10_122
| ~ spl10_151
| spl10_174 ),
inference(sat_conversion,[],[f3517]) ).
cnf(s208,plain,
( ~ spl10_150
| ~ spl10_174 ),
inference(sat_conversion,[],[f3532]) ).
cnf(s209,plain,
( ~ spl10_119
| spl10_121
| ~ spl10_170 ),
inference(sat_conversion,[],[f3547]) ).
cnf(s211,plain,
~ spl10_121,
inference(sat_conversion,[],[f3563]) ).
cnf(s212,plain,
( ~ spl10_120
| spl10_121
| ~ spl10_173 ),
inference(sat_conversion,[],[f3575]) ).
cnf(s230,plain,
( ~ spl10_152
| spl10_170
| spl10_174 ),
inference(sat_conversion,[],[f3868]) ).
cnf(s241,plain,
( spl10_46
| spl10_48
| ~ spl10_59
| spl10_187
| spl10_188 ),
inference(sat_conversion,[],[f4103]) ).
cnf(s244,plain,
( ~ spl10_187
| spl10_189 ),
inference(sat_conversion,[],[f4132]) ).
cnf(s247,plain,
( spl10_46
| spl10_48
| ~ spl10_59
| spl10_188
| ~ spl10_189 ),
inference(sat_conversion,[],[f4150]) ).
cnf(s249,plain,
( spl10_60
| spl10_61
| ~ spl10_188 ),
inference(sat_conversion,[],[f4159]) ).
cnf(s251,plain,
( ~ spl10_60
| spl10_194 ),
inference(sat_conversion,[],[f4178]) ).
cnf(s474,plain,
( spl10_5
| ~ spl10_74
| ~ spl10_214 ),
inference(sat_conversion,[],[f6633]) ).
cnf(s478,plain,
( spl10_5
| spl10_74 ),
inference(sat_conversion,[],[f6649]) ).
cnf(s638,plain,
( ~ spl10_479
| ~ spl10_480
| spl10_481 ),
inference(sat_conversion,[],[f10715]) ).
cnf(s639,plain,
( ~ spl10_479
| ~ spl10_480
| spl10_482 ),
inference(sat_conversion,[],[f10720]) ).
cnf(s640,plain,
( ~ spl10_479
| ~ spl10_480
| ~ spl10_483 ),
inference(sat_conversion,[],[f10725]) ).
cnf(s641,plain,
( ~ spl10_150
| spl10_480 ),
inference(sat_conversion,[],[f10731]) ).
cnf(s676,plain,
( ~ spl10_480
| spl10_481
| ~ spl10_535 ),
inference(sat_conversion,[],[f11206]) ).
cnf(s677,plain,
( ~ spl10_480
| spl10_482
| ~ spl10_535 ),
inference(sat_conversion,[],[f11207]) ).
cnf(s839,plain,
( ~ spl10_86
| spl10_98
| spl10_660 ),
inference(sat_conversion,[],[f15904]) ).
cnf(s873,plain,
( ~ spl10_150
| spl10_170
| ~ spl10_660
| ~ spl10_683 ),
inference(sat_conversion,[],[f17540]) ).
cnf(s1146,plain,
( ~ spl10_150
| spl10_485 ),
inference(sat_conversion,[],[f22878]) ).
cnf(s1148,plain,
( ~ spl10_485
| spl10_498
| spl10_831
| spl10_832 ),
inference(sat_conversion,[],[f22903]) ).
cnf(s1149,plain,
( spl10_498
| spl10_684
| ~ spl10_831 ),
inference(sat_conversion,[],[f22944]) ).
cnf(s1151,plain,
( ~ spl10_4
| spl10_175
| spl10_484
| ~ spl10_485 ),
inference(sat_conversion,[],[f23024]) ).
cnf(s1152,plain,
( ~ spl10_153
| spl10_174
| ~ spl10_482 ),
inference(sat_conversion,[],[f23025]) ).
cnf(s1190,plain,
( ~ spl10_175
| spl10_600 ),
inference(sat_conversion,[],[f23296]) ).
cnf(s1267,plain,
( ~ spl10_484
| spl10_536
| spl10_684 ),
inference(sat_conversion,[],[f24263]) ).
cnf(s1270,plain,
( ~ spl10_536
| ~ spl10_899
| spl10_900 ),
inference(sat_conversion,[],[f24668]) ).
cnf(s1271,plain,
( ~ spl10_536
| spl10_686
| spl10_900 ),
inference(sat_conversion,[],[f24669]) ).
cnf(s1277,plain,
( spl10_17
| ~ spl10_150
| ~ spl10_900 ),
inference(sat_conversion,[],[f24780]) ).
cnf(s1288,plain,
( ~ spl10_17
| ~ spl10_18
| spl10_461 ),
inference(sat_conversion,[],[f24907]) ).
cnf(s1306,plain,
( spl10_482
| spl10_498
| ~ spl10_832 ),
inference(sat_conversion,[],[f25133]) ).
cnf(s1332,plain,
( ~ spl10_480
| spl10_684
| ~ spl10_842 ),
inference(sat_conversion,[],[f25480]) ).
cnf(s1334,plain,
( ~ spl10_150
| spl10_170
| ~ spl10_842 ),
inference(sat_conversion,[],[f25483]) ).
cnf(s1359,plain,
( spl10_23
| ~ spl10_150
| ~ spl10_498
| ~ spl10_600 ),
inference(sat_conversion,[],[f25830]) ).
cnf(s1361,plain,
( ~ spl10_23
| ~ spl10_61 ),
inference(sat_conversion,[],[f25862]) ).
cnf(s1367,plain,
( ~ spl10_60
| spl10_194 ),
inference(sat_conversion,[],[f25978]) ).
cnf(s1434,plain,
( ~ spl10_194
| ~ spl10_480
| ~ spl10_498
| ~ spl10_600
| ~ spl10_848 ),
inference(sat_conversion,[],[f26688]) ).
cnf(s1572,plain,
( ~ spl10_43
| spl10_80
| spl10_122
| ~ spl10_150
| ~ spl10_600 ),
inference(sat_conversion,[],[f27673]) ).
cnf(s1611,plain,
( spl10_481
| ~ spl10_484
| spl10_537 ),
inference(sat_conversion,[],[f28262]) ).
cnf(s1612,plain,
( spl10_482
| ~ spl10_484
| spl10_537 ),
inference(sat_conversion,[],[f28264]) ).
cnf(s1614,plain,
( spl10_683
| ~ spl10_684 ),
inference(sat_conversion,[],[f28304]) ).
cnf(s1615,plain,
( ~ spl10_683
| spl10_693 ),
inference(sat_conversion,[],[f28308]) ).
cnf(s1621,plain,
( spl10_20
| ~ spl10_150
| ~ spl10_537
| ~ spl10_683 ),
inference(sat_conversion,[],[f28397]) ).
cnf(s1674,plain,
( ~ spl10_20
| ~ spl10_21
| spl10_708 ),
inference(sat_conversion,[],[f29505]) ).
cnf(s1676,plain,
( ~ spl10_20
| ~ spl10_21
| ~ spl10_708 ),
inference(sat_conversion,[],[f29514]) ).
cnf(s1723,plain,
( ~ spl10_481
| spl10_482 ),
inference(sat_conversion,[],[f29995]) ).
cnf(s1724,plain,
( ~ spl10_482
| ~ spl10_686
| spl10_899 ),
inference(sat_conversion,[],[f29996]) ).
cnf(s1803,plain,
( ~ spl10_150
| spl10_173
| ~ spl10_481 ),
inference(sat_conversion,[],[f30578]) ).
cnf(s1817,plain,
( ~ spl10_4
| spl10_17
| ~ spl10_23
| ~ spl10_46 ),
inference(sat_conversion,[],[f30612]) ).
cnf(s1831,plain,
( ~ spl10_153
| spl10_173
| spl10_174 ),
inference(sat_conversion,[],[f30645]) ).
cnf(s1856,plain,
( ~ spl10_90
| spl10_684 ),
inference(sat_conversion,[],[f30741]) ).
cnf(s1887,plain,
( ~ spl10_46
| spl10_151
| ~ spl10_153 ),
inference(sat_conversion,[],[f30961]) ).
cnf(s1944,plain,
( ~ spl10_4
| ~ spl10_46
| spl10_119
| spl10_120
| spl10_121 ),
inference(sat_conversion,[],[f31255]) ).
cnf(s1986,plain,
( ~ spl10_461
| spl10_483
| ~ spl10_900 ),
inference(sat_conversion,[],[f31435]) ).
cnf(s2005,plain,
( spl10_214
| ~ spl10_693
| ~ spl10_900 ),
inference(sat_conversion,[],[f31743]) ).
cnf(s2059,plain,
( ~ spl10_152
| spl10_174
| ~ spl10_684 ),
inference(sat_conversion,[],[f32161]) ).
cnf(s2066,plain,
( spl10_479
| ~ spl10_480
| ~ spl10_536 ),
inference(sat_conversion,[],[f32174]) ).
cnf(s2067,plain,
( spl10_479
| ~ spl10_480
| ~ spl10_484
| spl10_842 ),
inference(sat_conversion,[],[f32176]) ).
cnf(s2070,plain,
( ~ spl10_4
| ~ spl10_480
| ~ spl10_485
| spl10_535
| spl10_842
| spl10_848 ),
inference(sat_conversion,[],[f32180]) ).
cnf(s2095,plain,
( spl10_481
| ~ spl10_482 ),
inference(sat_conversion,[],[f32318]) ).
cnf(s2101,plain,
( ~ spl10_119
| ~ spl10_170 ),
inference(rat,[],[s209,s211]) ).
cnf(s2103,plain,
spl10_485,
inference(rat,[],[s1146,s201]) ).
cnf(s2104,plain,
spl10_480,
inference(rat,[],[s641,s201]) ).
cnf(s2105,plain,
~ spl10_174,
inference(rat,[],[s208,s201]) ).
cnf(s2108,plain,
( ~ spl10_4
| spl10_151
| spl10_152
| spl10_153 ),
inference(rat,[],[s172,s201]) ).
cnf(s2109,plain,
( ~ spl10_118
| ~ spl10_122 ),
inference(rat,[],[s154,s211]) ).
cnf(s2123,plain,
~ spl10_41,
inference(rat,[],[s31,s92]) ).
cnf(s2124,plain,
~ spl10_6,
inference(rat,[],[s50,s2123]) ).
cnf(s2127,plain,
~ spl10_5,
inference(rat,[],[s4,s2124]) ).
cnf(s2131,plain,
spl10_74,
inference(rat,[],[s478,s2127]) ).
cnf(s2137,plain,
~ spl10_214,
inference(rat,[],[s474,s2127,s2131]) ).
cnf(s2141,plain,
spl10_4,
inference(rat,[],[s2,s3]) ).
cnf(s2142,plain,
~ spl10_99,
inference(rat,[],[s135,s92,s2141]) ).
cnf(s2143,plain,
~ spl10_98,
inference(rat,[],[s140,s2142]) ).
cnf(s2144,plain,
spl10_86,
inference(rat,[],[s118,s2142]) ).
cnf(s2149,plain,
spl10_660,
inference(rat,[],[s839,s2143,s2144]) ).
cnf(s2156,plain,
( spl10_684
| spl10_481
| spl10_23 ),
inference(rat,[],[s1148,s1149,s1306,s1359,s1190,s1151,s1267,s2095,s2066,s638,s2103,s201,s2141,s2104]) ).
cnf(s2157,plain,
( spl10_173
| spl10_23
| spl10_20 ),
inference(rat,[],[s1151,s203,s1611,s2108,s1621,s2059,s1614,s2156,s1803,s1831,s2141,s2103,s2105,s201]) ).
cnf(s2158,plain,
( spl10_170
| spl10_23
| spl10_900 ),
inference(rat,[],[s1724,s1270,s1271,s1267,s1151,s203,s2108,s1152,s1723,s2156,s1614,s230,s873,s2141,s2103,s2105,s201,s2149]) ).
cnf(s2159,plain,
( spl10_684
| ~ spl10_484
| spl10_23
| spl10_900 ),
inference(rat,[],[s1724,s1270,s1271,s1723,s1267,s2156]) ).
cnf(s2160,plain,
( ~ spl10_484
| spl10_23
| spl10_20
| spl10_900 ),
inference(rat,[],[s1152,s1612,s2108,s1621,s2059,s1614,s2159,s204,s2109,s153,s2101,s2158,s212,s2157,s2105,s2141,s201,s211]) ).
cnf(s2161,plain,
( spl10_23
| spl10_20
| spl10_900 ),
inference(rat,[],[s1572,s66,s74,s1190,s142,s1151,s1944,s2160,s2109,s153,s2101,s2158,s212,s2157,s201,s92,s2141,s2103,s211]) ).
cnf(s2162,plain,
( spl10_684
| ~ spl10_484
| spl10_900 ),
inference(rat,[],[s1724,s639,s1270,s1271,s2067,s1267,s1332,s2104]) ).
cnf(s2163,plain,
( ~ spl10_484
| spl10_20
| spl10_900 ),
inference(rat,[],[s2109,s204,s153,s2108,s212,s1152,s1803,s1612,s1611,s2101,s1621,s873,s2059,s1614,s2162,s2105,s2141,s211,s201,s2149]) ).
cnf(s2164,plain,
( spl10_498
| spl10_482
| spl10_684 ),
inference(rat,[],[s1148,s1149,s1306,s2103]) ).
cnf(s2165,plain,
( ~ spl10_59
| spl10_188
| spl10_46 ),
inference(rat,[],[s244,s247,s241,s92]) ).
cnf(s2166,plain,
( spl10_60
| spl10_46
| spl10_61 ),
inference(rat,[],[s2165,s249,s41]) ).
cnf(s2167,plain,
( ~ spl10_152
| ~ spl10_194
| spl10_118
| ~ spl10_600 ),
inference(rat,[],[s1434,s2070,s2164,s676,s2095,s1803,s212,s153,s2101,s1332,s230,s2059,s2104,s2103,s2141,s201,s211,s2105]) ).
cnf(s2168,plain,
( spl10_20
| spl10_17 ),
inference(rat,[],[s2164,s1434,s1614,s2070,s873,s1334,s2101,s153,s677,s212,s1152,s1831,s2108,s2167,s1367,s2166,s2109,s1572,s203,s1190,s1151,s2163,s66,s74,s142,s1817,s1361,s2161,s1277,s2104,s2103,s2141,s201,s2149,s211,s2105,s92]) ).
cnf(s2169,plain,
( ~ spl10_21
| ~ spl10_20 ),
inference(rat,[],[s1674,s1676]) ).
cnf(s2170,plain,
~ spl10_20,
inference(rat,[],[s2169,s12]) ).
cnf(s2174,plain,
spl10_17,
inference(rat,[],[s2168,s2170]) ).
cnf(s2178,plain,
spl10_18,
inference(rat,[],[s10,s2174]) ).
cnf(s2183,plain,
spl10_461,
inference(rat,[],[s1288,s2174,s2178]) ).
cnf(s2184,plain,
( ~ spl10_484
| spl10_684 ),
inference(rat,[],[s640,s1986,s2067,s2162,s1332,s2104,s2183]) ).
cnf(s2185,plain,
~ spl10_152,
inference(rat,[],[s1361,s2157,s2166,s212,s1367,s153,s2167,s2109,s1572,s1190,s1151,s2184,s66,s74,s142,s72,s2101,s1856,s230,s2059,s2170,s211,s2141,s201,s2103,s92,s2105]) ).
cnf(s2186,plain,
spl10_684,
inference(rat,[],[s251,s2166,s1434,s1361,s2070,s2156,s2164,s677,s1723,s1152,s2108,s203,s1190,s1151,s72,s2184,s1332,s1856,s2104,s2103,s2141,s2105,s2185]) ).
cnf(s2187,plain,
spl10_683,
inference(rat,[],[s1614,s2186]) ).
cnf(s2188,plain,
spl10_693,
inference(rat,[],[s1615,s2187]) ).
cnf(s2190,plain,
spl10_170,
inference(rat,[],[s873,s2149,s201,s2187]) ).
cnf(s2192,plain,
~ spl10_900,
inference(rat,[],[s2005,s2137,s2188]) ).
cnf(s2195,plain,
~ spl10_119,
inference(rat,[],[s2101,s2190]) ).
cnf(s2198,plain,
~ spl10_484,
inference(rat,[],[s2163,s2170,s2192]) ).
cnf(s2206,plain,
spl10_175,
inference(rat,[],[s1151,s2103,s2141,s2198]) ).
cnf(s2212,plain,
spl10_600,
inference(rat,[],[s1190,s2206]) ).
cnf(s2213,plain,
~ spl10_151,
inference(rat,[],[s203,s2105,s2206]) ).
cnf(s2217,plain,
spl10_153,
inference(rat,[],[s2108,s2185,s2141,s2213]) ).
cnf(s2218,plain,
spl10_173,
inference(rat,[],[s1831,s2105,s2217]) ).
cnf(s2221,plain,
~ spl10_46,
inference(rat,[],[s1887,s2213,s2217]) ).
cnf(s2222,plain,
~ spl10_120,
inference(rat,[],[s212,s211,s2218]) ).
cnf(s2233,plain,
~ spl10_93,
inference(rat,[],[s142,s2141,s92,s2221]) ).
cnf(s2241,plain,
spl10_118,
inference(rat,[],[s153,s2195,s2141,s2222]) ).
cnf(s2244,plain,
~ spl10_80,
inference(rat,[],[s74,s2233]) ).
cnf(s2245,plain,
spl10_43,
inference(rat,[],[s66,s2233]) ).
cnf(s2251,plain,
~ spl10_122,
inference(rat,[],[s2109,s2241]) ).
cnf(s2254,plain,
$false,
inference(rat,[],[s1572,s2212,s201,s2245,s2244,s2251]) ).
fof(f32319,plain,
$false,
inference(avatar_sat_refutation,[],[s2254]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV550+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n026.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Mon Sep 28 06:38:10 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.68/2.26 % (3653440)Detected formulas, will run a generic FOF schedule.
% 9.68/2.26 % (3653445)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=2299381184:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.68/2.26 % (3653446)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=3315687527:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.68/2.26 % (3653451)dis-21_1_sil=8000:lcm=predicate:random_seed=3919417116: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)
% 9.68/2.26 % (3653449)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3768628977:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.68/2.26 % (3653448)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2596772872:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.68/2.26 % (3653450)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=850692068:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.68/2.26 % (3653447)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=1475408863:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.68/2.26 % (3653448)Refutation not found, incomplete strategy
% 9.68/2.26 % (3653448)------------------------------
% 9.68/2.26 % (3653448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.26 % (3653448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.26 % (3653448)CaDiCaL version: 2.1.3
% 9.68/2.26 % (3653448)Termination reason: Refutation not found, incomplete strategy
% 9.68/2.26 % (3653448)Time elapsed: 0.001 s
% 9.68/2.26 % (3653448)Peak memory usage: 88 MB
% 9.68/2.26 % (3653449)Instruction limit reached!
% 9.68/2.26 % (3653449)------------------------------
% 9.68/2.26 % (3653449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.26 % (3653449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.26 % (3653449)CaDiCaL version: 2.1.3
% 9.68/2.26 % (3653449)Termination reason: Instruction limit
% 9.68/2.26 % (3653449)Termination phase: Saturation
% 9.68/2.26 % (3653449)Time elapsed: 0.076 s
% 9.68/2.26 % (3653449)Peak memory usage: 89 MB
% 9.68/2.26 % (3653449)Instructions burned: 121 (million)
% 9.68/2.26 % (3653451)Instruction limit reached!
% 9.68/2.26 % (3653451)------------------------------
% 9.68/2.26 % (3653451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.26 % (3653451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.26 % (3653451)CaDiCaL version: 2.1.3
% 9.68/2.26 % (3653451)Termination reason: Instruction limit
% 9.68/2.26 % (3653451)Termination phase: Saturation
% 9.68/2.26 % (3653451)Time elapsed: 0.077 s
% 9.68/2.26 % (3653451)Peak memory usage: 89 MB
% 9.68/2.26 % (3653451)Instructions burned: 130 (million)
% 9.68/2.26 % (3653450)Instruction limit reached!
% 9.68/2.26 % (3653450)------------------------------
% 9.68/2.26 % (3653450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.26 % (3653450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.68/2.26 % (3653450)CaDiCaL version: 2.1.3
% 9.68/2.26 % (3653450)Termination reason: Instruction limit
% 9.68/2.26 % (3653450)Termination phase: Saturation
% 9.68/2.26 % (3653450)Time elapsed: 0.093 s
% 9.68/2.26 % (3653450)Peak memory usage: 89 MB
% 9.68/2.26 % (3653450)Instructions burned: 140 (million)
% 9.68/2.26 % (3653474)lrs+10_1_sil=8000:sp=occurrence:random_seed=2768116939:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 9.68/2.26 % (3653476)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2393043174:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.68/2.26 % (3653483)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4261997937:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 9.68/2.26 % (3653483)Refutation not found, incomplete strategy
% 9.68/2.26 % (3653483)------------------------------
% 9.68/2.26 % (3653483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.68/2.26 % (3653483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.46 % (3653483)CaDiCaL version: 2.1.3
% 10.67/2.46 % (3653483)Termination reason: Refutation not found, incomplete strategy
% 10.67/2.46 % (3653483)Time elapsed: 0.002 s
% 10.67/2.46 % (3653483)Peak memory usage: 88 MB
% 10.67/2.46 % (3653448)------------------------------
% 10.67/2.46 % (3653448)------------------------------
% 10.67/2.46 % (3653476)Instruction limit reached!
% 10.67/2.46 % (3653476)------------------------------
% 10.67/2.46 % (3653476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.46 % (3653476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.46 % (3653476)CaDiCaL version: 2.1.3
% 10.67/2.46 % (3653476)Termination reason: Instruction limit
% 10.67/2.46 % (3653476)Termination phase: Saturation
% 10.67/2.46 % (3653476)Time elapsed: 0.077 s
% 10.67/2.46 % (3653476)Peak memory usage: 89 MB
% 10.67/2.46 % (3653476)Instructions burned: 158 (million)
% 10.67/2.46 % (3653548)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=1391940972:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 10.67/2.46 % (3653474)Instruction limit reached!
% 10.67/2.46 % (3653474)------------------------------
% 10.67/2.46 % (3653474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.46 % (3653474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.46 % (3653474)CaDiCaL version: 2.1.3
% 10.67/2.46 % (3653474)Termination reason: Instruction limit
% 10.67/2.46 % (3653474)Termination phase: Saturation
% 10.67/2.46 % (3653474)Time elapsed: 0.185 s
% 10.67/2.46 % (3653474)Peak memory usage: 91 MB
% 10.67/2.46 % (3653474)Instructions burned: 286 (million)
% 10.67/2.46 % (3653559)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=287873411:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 10.67/2.46 % (3653559)Refutation not found, incomplete strategy
% 10.67/2.46 % (3653559)------------------------------
% 10.67/2.46 % (3653559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.46 % (3653559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.46 % (3653559)CaDiCaL version: 2.1.3
% 10.67/2.46 % (3653559)Termination reason: Refutation not found, incomplete strategy
% 10.67/2.46 % (3653559)Time elapsed: 0.002 s
% 10.67/2.46 % (3653559)Peak memory usage: 88 MB
% 10.67/2.46 % (3653559)Instructions burned: 1 (million)
% 10.67/2.46 % (3653483)------------------------------
% 10.67/2.46 % (3653483)------------------------------
% 10.67/2.46 % (3653604)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=75816279:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 10.67/2.46 % (3653548)Instruction limit reached!
% 10.67/2.46 % (3653548)------------------------------
% 10.67/2.46 % (3653548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.46 % (3653548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.46 % (3653548)CaDiCaL version: 2.1.3
% 10.67/2.46 % (3653548)Termination reason: Instruction limit
% 10.67/2.46 % (3653548)Termination phase: Saturation
% 10.67/2.46 % (3653548)Time elapsed: 0.143 s
% 10.67/2.46 % (3653548)Peak memory usage: 92 MB
% 10.67/2.46 % (3653548)Instructions burned: 249 (million)
% 10.67/2.46 % (3653447)Refutation not found, incomplete strategy
% 10.67/2.46 % (3653447)------------------------------
% 10.67/2.46 % (3653447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.46 % (3653447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.46 % (3653447)CaDiCaL version: 2.1.3
% 10.67/2.46 % (3653447)Termination reason: Refutation not found, incomplete strategy
% 10.67/2.46 % (3653447)Time elapsed: 0.561 s
% 10.67/2.46 % (3653447)Peak memory usage: 127 MB
% 10.67/2.46 % (3653447)Instructions burned: 828 (million)
% 10.67/2.46 % (3653622)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1694105097:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 10.67/2.46 % (3653624)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1047204409:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 10.67/2.46 % (3653559)------------------------------
% 10.67/2.46 % (3653559)------------------------------
% 10.67/2.46 % (3653622)Instruction limit reached!
% 10.67/2.46 % (3653622)------------------------------
% 10.67/2.46 % (3653622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.46 % (3653622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.46 % (3653622)CaDiCaL version: 2.1.3
% 10.67/2.46 % (3653622)Termination reason: Instruction limit
% 10.67/2.46 % (3653622)Termination phase: Saturation
% 10.67/2.46 % (3653622)Time elapsed: 0.073 s
% 10.67/2.46 % (3653622)Peak memory usage: 89 MB
% 10.67/2.46 % (3653622)Instructions burned: 113 (million)
% 10.67/2.46 % (3653624)Instruction limit reached!
% 10.67/2.46 % (3653624)------------------------------
% 10.67/2.46 % (3653624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.46 % (3653624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.46 % (3653624)CaDiCaL version: 2.1.3
% 10.67/2.46 % (3653624)Termination reason: Instruction limit
% 10.67/2.46 % (3653624)Termination phase: Saturation
% 10.67/2.46 % (3653624)Time elapsed: 0.062 s
% 10.67/2.46 % (3653624)Peak memory usage: 88 MB
% 10.67/2.46 % (3653624)Instructions burned: 129 (million)
% 10.67/2.46 % (3653447)------------------------------
% 10.67/2.46 % (3653447)------------------------------
% 10.67/2.46 % (3653627)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3452349726:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 10.67/2.46 % (3653628)lrs+10_1_sil=8000:sp=occurrence:random_seed=1835981111:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 10.67/2.46 % (3653629)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3366780971:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 10.67/2.46 % (3653629)Refutation not found, incomplete strategy
% 10.67/2.46 % (3653629)------------------------------
% 10.67/2.46 % (3653629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.46 % (3653629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.46 % (3653629)CaDiCaL version: 2.1.3
% 10.67/2.46 % (3653629)Termination reason: Refutation not found, incomplete strategy
% 10.67/2.46 % (3653629)Time elapsed: 0.001 s
% 10.67/2.46 % (3653629)Peak memory usage: 88 MB
% 10.67/2.46 % (3653627)Instruction limit reached!
% 10.67/2.46 % (3653627)------------------------------
% 10.67/2.46 % (3653627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.46 % (3653627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.46 % (3653627)CaDiCaL version: 2.1.3
% 10.67/2.46 % (3653627)Termination reason: Instruction limit
% 10.67/2.46 % (3653627)Termination phase: Saturation
% 10.67/2.46 % (3653627)Time elapsed: 0.059 s
% 10.67/2.46 % (3653627)Peak memory usage: 88 MB
% 10.67/2.46 % (3653627)Instructions burned: 115 (million)
% 10.67/2.46 % (3653631)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3686110020:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 10.67/2.46 % (3653634)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3516012356:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 10.67/2.46 % (3653634)Instruction limit reached!
% 10.67/2.46 % (3653634)------------------------------
% 10.67/2.46 % (3653634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.46 % (3653634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.46 % (3653634)CaDiCaL version: 2.1.3
% 10.67/2.46 % (3653634)Termination reason: Instruction limit
% 10.67/2.46 % (3653634)Termination phase: Saturation
% 10.67/2.46 % (3653634)Time elapsed: 0.065 s
% 10.67/2.46 % (3653634)Peak memory usage: 89 MB
% 10.67/2.46 % (3653634)Instructions burned: 134 (million)
% 10.67/2.46 % (3653629)------------------------------
% 10.67/2.46 % (3653629)------------------------------
% 10.67/2.46 % (3653637)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3930783135:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 10.67/2.46 % (3653637)Refutation not found, incomplete strategy
% 10.67/2.46 % (3653637)------------------------------
% 10.67/2.46 % (3653637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.46 % (3653637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.46 % (3653637)CaDiCaL version: 2.1.3
% 10.67/2.46 % (3653637)Termination reason: Refutation not found, incomplete strategy
% 10.67/2.46 % (3653637)Time elapsed: 0.002 s
% 10.67/2.46 % (3653637)Peak memory usage: 88 MB
% 10.67/2.46 % (3653637)Instructions burned: 1 (million)
% 10.67/2.46 % (3653638)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1315644965:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 10.67/2.46 % (3653445)First to succeed.
% 10.67/2.46 % (3653445)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3653440"
% 10.67/2.46 % (3653628)Instruction limit reached!
% 10.67/2.46 % (3653628)------------------------------
% 10.67/2.46 % (3653628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.67/2.46 % (3653628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.67/2.46 % (3653628)CaDiCaL version: 2.1.3
% 10.67/2.46 % (3653628)Termination reason: Instruction limit
% 10.67/2.46 % (3653628)Termination phase: Saturation
% 10.67/2.46 % (3653628)Time elapsed: 0.581 s
% 10.67/2.46 % (3653628)Peak memory usage: 97 MB
% 10.67/2.46 % (3653628)Instructions burned: 908 (million)
% 10.67/2.46 % (3653445)Refutation found. Thanks to Tanya!
% 10.67/2.46 % SZS status Theorem for theBenchmark
% 10.67/2.46 % SZS output start Proof for theBenchmark
% See solution above
% 11.70/2.56 % (3653445)------------------------------
% 11.70/2.56 % (3653445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.70/2.56 % (3653445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.70/2.56 % (3653445)CaDiCaL version: 2.1.3
% 11.70/2.56 % (3653445)Termination reason: Refutation
% 11.70/2.56 % (3653445)Time elapsed: 1.305 s
% 11.70/2.56 % (3653445)Peak memory usage: 150 MB
% 11.70/2.56 % (3653445)Instructions burned: 3550 (million)
% 11.70/2.56 % (3653445)------------------------------
% 11.70/2.56 % (3653445)------------------------------
% 11.70/2.56 % (3653440)Success in time 1.586 s
% 11.70/2.56 % Vampire exiting
%------------------------------------------------------------------------------