%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV546+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:57:57 PM UTC 2026
% Result : Theorem 33.54s 5.64s
% Output : Refutation 34.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 81
% Syntax : Number of formulae : 824 ( 105 unt; 67 def)
% Number of atoms : 2286 ( 86 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 2638 (1176 ~;1339 |; 48 &)
% ( 67 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 66 ( 64 usr; 58 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 11 con; 0-2 aty)
% Number of variables : 174 ( 0 sgn 157 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( subq(X0,X1)
<=> ! [X2] :
( mem(X2,X0)
=> mem(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subq_def) ).
fof(f2,axiom,
! [X0,X1] :
( subq(X0,X1)
=> ( subq(X1,X0)
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setext) ).
fof(f4,axiom,
! [X0] : ~ mem(X0,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_ax) ).
fof(f5,axiom,
! [X0,X1] :
( mem(X0,s(X1))
<=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s_ax) ).
fof(f6,axiom,
! [X0,X1,X2] :
( mem(X0,u(X1,X2))
<=> ( mem(X0,X1)
| mem(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_ax) ).
fof(f8,axiom,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_def) ).
fof(f9,axiom,
! [X0] : n(X0) = a(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_def) ).
fof(f10,axiom,
! [X0,X1] :
( mem(X0,p(X1))
<=> subq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p_ax) ).
fof(f11,axiom,
! [X0] :
( atleast2p(X0)
<=> ? [X1] :
( mem(X1,X0)
& ~ subq(X0,p(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',atleast2p_def) ).
fof(f12,axiom,
! [X0] :
( atleast3p(X0)
<=> ? [X1] :
( subq(X1,X0)
& atleast2p(X1)
& ~ subq(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',atleast3p_def) ).
fof(f13,axiom,
! [X0] :
( atleast4p(X0)
<=> ? [X1] :
( subq(X1,X0)
& atleast3p(X1)
& ~ subq(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',atleast4p_def) ).
fof(f14,axiom,
! [X0] :
( atleast5p(X0)
<=> ? [X1] :
( subq(X1,X0)
& atleast4p(X1)
& ~ subq(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',atleast5p_def) ).
fof(f15,axiom,
! [X0] :
( atleast6p(X0)
<=> ? [X1] :
( subq(X1,X0)
& atleast5p(X1)
& ~ subq(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',atleast6p_def) ).
fof(f26,conjecture,
~ atleast6p(a(n(n(n(e))),n(s(n(e))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',atmost5_75) ).
fof(f27,negated_conjecture,
~ ~ atleast6p(a(n(n(n(e))),n(s(n(e))))),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f28,plain,
atleast6p(a(n(n(n(e))),n(s(n(e))))),
inference(flattening,[],[f27]) ).
fof(f29,plain,
! [X0] :
( atleast6p(X0)
=> ? [X1] :
( subq(X1,X0)
& atleast5p(X1)
& ~ subq(X0,X1) ) ),
inference(unused_predicate_definition_removal,[],[f15]) ).
fof(f30,plain,
! [X0] :
( atleast5p(X0)
=> ? [X1] :
( subq(X1,X0)
& atleast4p(X1)
& ~ subq(X0,X1) ) ),
inference(unused_predicate_definition_removal,[],[f14]) ).
fof(f31,plain,
! [X0] :
( atleast4p(X0)
=> ? [X1] :
( subq(X1,X0)
& atleast3p(X1)
& ~ subq(X0,X1) ) ),
inference(unused_predicate_definition_removal,[],[f13]) ).
fof(f32,plain,
! [X0] :
( atleast3p(X0)
=> ? [X1] :
( subq(X1,X0)
& atleast2p(X1)
& ~ subq(X0,X1) ) ),
inference(unused_predicate_definition_removal,[],[f12]) ).
fof(f33,plain,
! [X0] :
( atleast2p(X0)
=> ? [X1] :
( mem(X1,X0)
& ~ subq(X0,p(X1)) ) ),
inference(unused_predicate_definition_removal,[],[f11]) ).
fof(f34,plain,
! [X0,X1] :
( subq(X0,X1)
<=> ! [X2] :
( mem(X2,X1)
| ~ mem(X2,X0) ) ),
inference(ennf_transformation,[],[f1]) ).
fof(f35,plain,
! [X0,X1] :
( X0 = X1
| ~ subq(X1,X0)
| ~ subq(X0,X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f36,plain,
! [X0,X1] :
( X0 = X1
| ~ subq(X1,X0)
| ~ subq(X0,X1) ),
inference(flattening,[],[f35]) ).
fof(f37,plain,
! [X0] :
( ? [X1] :
( mem(X1,X0)
& ~ subq(X0,p(X1)) )
| ~ atleast2p(X0) ),
inference(ennf_transformation,[],[f33]) ).
fof(f38,plain,
! [X0] :
( ? [X1] :
( subq(X1,X0)
& atleast2p(X1)
& ~ subq(X0,X1) )
| ~ atleast3p(X0) ),
inference(ennf_transformation,[],[f32]) ).
fof(f39,plain,
! [X0] :
( ? [X1] :
( subq(X1,X0)
& atleast3p(X1)
& ~ subq(X0,X1) )
| ~ atleast4p(X0) ),
inference(ennf_transformation,[],[f31]) ).
fof(f40,plain,
! [X0] :
( ? [X1] :
( subq(X1,X0)
& atleast4p(X1)
& ~ subq(X0,X1) )
| ~ atleast5p(X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f41,plain,
! [X0] :
( ? [X1] :
( subq(X1,X0)
& atleast5p(X1)
& ~ subq(X0,X1) )
| ~ atleast6p(X0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f42,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,[],[f34]) ).
fof(f43,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,[],[f42]) ).
fof(f44,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))],[f43]) ).
fof(f45,plain,
! [X0,X1] :
( ( mem(X0,s(X1))
| X0 != X1 )
& ( X0 = X1
| ~ mem(X0,s(X1)) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f46,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(f47,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,[],[f46]) ).
fof(f50,plain,
! [X0,X1] :
( ( mem(X0,p(X1))
| ~ subq(X0,X1) )
& ( subq(X0,X1)
| ~ mem(X0,p(X1)) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f51,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))],[f37]) ).
fof(f52,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))],[f38]) ).
fof(f53,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))],[f39]) ).
fof(f54,plain,
! [X0] :
( ( subq(sK4(X0),X0)
& atleast4p(sK4(X0))
& ~ subq(X0,sK4(X0)) )
| ~ atleast5p(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X1,sK4(X0))],[f40]) ).
fof(f55,plain,
! [X0] :
( ( subq(sK5(X0),X0)
& atleast5p(sK5(X0))
& ~ subq(X0,sK5(X0)) )
| ~ atleast6p(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X1,sK5(X0))],[f41]) ).
fof(f56,plain,
! [X3,X0,X1] :
( ~ mem(X3,X0)
| mem(X3,X1)
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f44]) ).
fof(f57,plain,
! [X0,X1] :
( mem(sK0(X0,X1),X0)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f44]) ).
fof(f58,plain,
! [X0,X1] :
( ~ mem(sK0(X0,X1),X1)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f44]) ).
fof(f59,plain,
! [X0,X1] :
( ~ subq(X1,X0)
| X0 = X1
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f60,plain,
! [X0] : ~ mem(X0,e),
inference(cnf_transformation,[],[f4]) ).
fof(f61,plain,
! [X0,X1] :
( ~ mem(X0,s(X1))
| X0 = X1 ),
inference(cnf_transformation,[],[f45]) ).
fof(f62,plain,
! [X0,X1] :
( mem(X0,s(X1))
| X0 != X1 ),
inference(cnf_transformation,[],[f45]) ).
fof(f63,plain,
! [X2,X0,X1] :
( ~ mem(X0,u(X1,X2))
| mem(X0,X2)
| mem(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f64,plain,
! [X2,X0,X1] :
( mem(X0,u(X1,X2))
| ~ mem(X0,X2) ),
inference(cnf_transformation,[],[f47]) ).
fof(f65,plain,
! [X2,X0,X1] :
( mem(X0,u(X1,X2))
| ~ mem(X0,X1) ),
inference(cnf_transformation,[],[f47]) ).
fof(f69,plain,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
inference(cnf_transformation,[],[f8]) ).
fof(f70,plain,
! [X0] : n(X0) = a(X0,X0),
inference(cnf_transformation,[],[f9]) ).
fof(f72,plain,
! [X0,X1] :
( mem(X0,p(X1))
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f50]) ).
fof(f73,plain,
! [X0] :
( ~ subq(X0,p(sK1(X0)))
| ~ atleast2p(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f74,plain,
! [X0] :
( mem(sK1(X0),X0)
| ~ atleast2p(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f76,plain,
! [X0] :
( atleast2p(sK2(X0))
| ~ atleast3p(X0) ),
inference(cnf_transformation,[],[f52]) ).
fof(f77,plain,
! [X0] :
( subq(sK2(X0),X0)
| ~ atleast3p(X0) ),
inference(cnf_transformation,[],[f52]) ).
fof(f78,plain,
! [X0] :
( ~ subq(X0,sK3(X0))
| ~ atleast4p(X0) ),
inference(cnf_transformation,[],[f53]) ).
fof(f79,plain,
! [X0] :
( atleast3p(sK3(X0))
| ~ atleast4p(X0) ),
inference(cnf_transformation,[],[f53]) ).
fof(f80,plain,
! [X0] :
( subq(sK3(X0),X0)
| ~ atleast4p(X0) ),
inference(cnf_transformation,[],[f53]) ).
fof(f81,plain,
! [X0] :
( ~ subq(X0,sK4(X0))
| ~ atleast5p(X0) ),
inference(cnf_transformation,[],[f54]) ).
fof(f82,plain,
! [X0] :
( atleast4p(sK4(X0))
| ~ atleast5p(X0) ),
inference(cnf_transformation,[],[f54]) ).
fof(f83,plain,
! [X0] :
( subq(sK4(X0),X0)
| ~ atleast5p(X0) ),
inference(cnf_transformation,[],[f54]) ).
fof(f84,plain,
! [X0] :
( ~ subq(X0,sK5(X0))
| ~ atleast6p(X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f85,plain,
! [X0] :
( atleast5p(sK5(X0))
| ~ atleast6p(X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f86,plain,
! [X0] :
( subq(sK5(X0),X0)
| ~ atleast6p(X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f87,plain,
atleast6p(a(n(n(n(e))),n(s(n(e))))),
inference(cnf_transformation,[],[f28]) ).
fof(f88,plain,
! [X0] : n(X0) = u(X0,s(X0)),
inference(definition_unfolding,[],[f70,f69]) ).
fof(f89,plain,
atleast6p(u(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))),s(u(s(u(e,s(e))),s(s(u(e,s(e)))))))),
inference(definition_unfolding,[],[f87,f69,f88,f88,f88,f88,f88]) ).
fof(f90,plain,
! [X1] : mem(X1,s(X1)),
inference(equality_resolution,[],[f62]) ).
fof(f91,definition,
sF6 = s(e),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f92,plain,
s(e) = sF6,
inference(reorient_equations,[],[f91]) ).
fof(f93,definition,
sF7 = u(e,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f94,plain,
u(e,sF6) = sF7,
inference(reorient_equations,[],[f93]) ).
fof(f95,definition,
sF8 = s(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f96,plain,
s(sF7) = sF8,
inference(reorient_equations,[],[f95]) ).
fof(f97,definition,
sF9 = u(sF7,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f98,plain,
u(sF7,sF8) = sF9,
inference(reorient_equations,[],[f97]) ).
fof(f99,definition,
sF10 = s(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f100,plain,
s(sF9) = sF10,
inference(reorient_equations,[],[f99]) ).
fof(f101,definition,
sF11 = u(sF9,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f102,plain,
u(sF9,sF10) = sF11,
inference(reorient_equations,[],[f101]) ).
fof(f103,definition,
sF12 = s(sF8),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f104,plain,
s(sF8) = sF12,
inference(reorient_equations,[],[f103]) ).
fof(f105,definition,
sF13 = u(sF8,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f106,plain,
u(sF8,sF12) = sF13,
inference(reorient_equations,[],[f105]) ).
fof(f107,definition,
sF14 = s(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f108,plain,
s(sF13) = sF14,
inference(reorient_equations,[],[f107]) ).
fof(f109,definition,
sF15 = u(sF11,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f110,plain,
u(sF11,sF14) = sF15,
inference(reorient_equations,[],[f109]) ).
fof(f111,plain,
atleast6p(sF15),
inference(definition_folding,[],[f89,f110,f108,f106,f104,f96,f94,f92,f96,f94,f92,f102,f100,f98,f96,f94,f92,f94,f92,f98,f96,f94,f92,f94,f92]) ).
fof(f112,plain,
mem(e,sF6),
inference(superposition,[],[f90,f92]) ).
fof(f113,plain,
mem(sF7,sF8),
inference(superposition,[],[f90,f96]) ).
fof(f115,plain,
mem(sF9,sF10),
inference(superposition,[],[f90,f100]) ).
fof(f116,plain,
mem(sF13,sF14),
inference(superposition,[],[f90,f108]) ).
fof(f119,plain,
! [X0] :
( ~ mem(X0,sF6)
| e = X0 ),
inference(superposition,[],[f61,f92]) ).
fof(f120,plain,
! [X0] :
( ~ mem(X0,sF8)
| sF7 = X0 ),
inference(superposition,[],[f61,f96]) ).
fof(f122,plain,
! [X0] :
( ~ mem(X0,sF10)
| sF9 = X0 ),
inference(superposition,[],[f61,f100]) ).
fof(f123,plain,
! [X0] :
( ~ mem(X0,sF14)
| sF13 = X0 ),
inference(superposition,[],[f61,f108]) ).
fof(f140,plain,
! [X0] :
( ~ mem(X0,sF6)
| mem(X0,sF7) ),
inference(superposition,[],[f64,f94]) ).
fof(f141,plain,
! [X0] :
( ~ mem(X0,sF8)
| mem(X0,sF9) ),
inference(superposition,[],[f64,f98]) ).
fof(f148,plain,
mem(e,sF7),
inference(resolution,[],[f140,f112]) ).
fof(f152,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X2)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f58,f64]) ).
fof(f162,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X1)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f65,f58]) ).
fof(f164,plain,
! [X0] :
( ~ mem(X0,sF7)
| mem(X0,sF9) ),
inference(superposition,[],[f65,f98]) ).
fof(f173,plain,
! [X0] :
( ~ mem(X0,sF7)
| mem(X0,sF6)
| mem(X0,e) ),
inference(superposition,[],[f63,f94]) ).
fof(f174,plain,
! [X0] :
( ~ mem(X0,sF9)
| mem(X0,sF8)
| mem(X0,sF7) ),
inference(superposition,[],[f63,f98]) ).
fof(f176,plain,
! [X0] :
( ~ mem(X0,sF11)
| mem(X0,sF10)
| mem(X0,sF9) ),
inference(superposition,[],[f63,f102]) ).
fof(f177,plain,
! [X0] :
( ~ mem(X0,sF15)
| mem(X0,sF14)
| mem(X0,sF11) ),
inference(superposition,[],[f63,f110]) ).
fof(f178,plain,
! [X0] :
( ~ mem(X0,sF7)
| mem(X0,sF6) ),
inference(forward_subsumption_resolution,[],[f173,f60]) ).
fof(f188,plain,
mem(e,sF9),
inference(resolution,[],[f164,f148]) ).
fof(f218,plain,
! [X0] :
( subq(X0,X0)
| subq(X0,X0) ),
inference(resolution,[],[f57,f58]) ).
fof(f219,plain,
! [X0] : subq(e,X0),
inference(resolution,[],[f57,f60]) ).
fof(f220,plain,
! [X0,X1] :
( sK0(s(X0),X1) = X0
| subq(s(X0),X1) ),
inference(resolution,[],[f57,f61]) ).
fof(f223,plain,
! [X0] :
( e = sK0(sF6,X0)
| subq(sF6,X0) ),
inference(resolution,[],[f57,f119]) ).
fof(f225,plain,
! [X0] :
( mem(sK0(sF7,X0),sF6)
| subq(sF7,X0) ),
inference(resolution,[],[f57,f178]) ).
fof(f241,plain,
! [X0] : subq(X0,X0),
inference(duplicate_literal_removal,[],[f218]) ).
fof(f242,plain,
atleast5p(sK5(sF15)),
inference(unit_resulting_resolution,[],[f85,f111]) ).
fof(f243,plain,
subq(sK5(sF15),sF15),
inference(unit_resulting_resolution,[],[f86,f111]) ).
fof(f260,plain,
! [X0,X1] :
( ~ subq(s(X0),X1)
| mem(X0,X1) ),
inference(resolution,[],[f56,f90]) ).
fof(f268,plain,
! [X2,X0,X1] :
( mem(sK0(X0,X1),X2)
| ~ subq(X0,X2)
| subq(X0,X1) ),
inference(resolution,[],[f56,f57]) ).
fof(f278,plain,
( sF15 = sK5(sF15)
| ~ subq(sF15,sK5(sF15)) ),
inference(resolution,[],[f243,f59]) ).
fof(f280,definition,
( spl16_1
<=> subq(sF15,sK5(sF15)) ),
introduced(definition,[new_symbols(definition,[spl16_1])],[avatar_definition]) ).
fof(f282,plain,
( ~ subq(sF15,sK5(sF15))
| spl16_1 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f284,definition,
( spl16_2
<=> sF15 = sK5(sF15) ),
introduced(definition,[new_symbols(definition,[spl16_2])],[avatar_definition]) ).
fof(f286,plain,
( sF15 = sK5(sF15)
| ~ spl16_2 ),
inference(avatar_component_clause,[],[f284]) ).
fof(f287,plain,
( ~ spl16_1
| spl16_2 ),
inference(avatar_split_clause,[],[f278,f284,f280]) ).
fof(f484,plain,
~ subq(sF15,sK5(sF15)),
inference(unit_resulting_resolution,[],[f84,f111]) ).
fof(f489,plain,
( mem(sK0(sF15,sK5(sF15)),sF15)
| spl16_1 ),
inference(unit_resulting_resolution,[],[f57,f282]) ).
fof(f492,plain,
! [X0] :
( ~ mem(e,X0)
| subq(sF6,X0)
| subq(sF6,X0) ),
inference(superposition,[],[f58,f223]) ).
fof(f493,plain,
! [X0] :
( ~ mem(e,X0)
| subq(sF6,X0) ),
inference(duplicate_literal_removal,[],[f492]) ).
fof(f502,plain,
subq(sF6,sF7),
inference(resolution,[],[f493,f148]) ).
fof(f503,plain,
subq(sF6,sF9),
inference(resolution,[],[f493,f188]) ).
fof(f512,plain,
( sF6 = sF7
| ~ subq(sF7,sF6) ),
inference(resolution,[],[f502,f59]) ).
fof(f514,definition,
( spl16_36
<=> subq(sF7,sF6) ),
introduced(definition,[new_symbols(definition,[spl16_36])],[avatar_definition]) ).
fof(f516,plain,
( ~ subq(sF7,sF6)
| spl16_36 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f518,definition,
( spl16_37
<=> sF6 = sF7 ),
introduced(definition,[new_symbols(definition,[spl16_37])],[avatar_definition]) ).
fof(f520,plain,
( sF6 = sF7
| ~ spl16_37 ),
inference(avatar_component_clause,[],[f518]) ).
fof(f521,plain,
( ~ spl16_36
| spl16_37 ),
inference(avatar_split_clause,[],[f512,f518,f514]) ).
fof(f544,plain,
! [X0,X1] :
( subq(X0,u(X1,X0))
| subq(X0,u(X1,X0)) ),
inference(resolution,[],[f152,f57]) ).
fof(f554,plain,
! [X0,X1] : subq(X0,u(X1,X0)),
inference(duplicate_literal_removal,[],[f544]) ).
fof(f555,plain,
subq(sK4(sK5(sF15)),sK5(sF15)),
inference(unit_resulting_resolution,[],[f83,f242]) ).
fof(f557,plain,
( sK5(sF15) = sK4(sK5(sF15))
| ~ subq(sK5(sF15),sK4(sK5(sF15))) ),
inference(resolution,[],[f555,f59]) ).
fof(f559,definition,
( spl16_42
<=> subq(sK5(sF15),sK4(sK5(sF15))) ),
introduced(definition,[new_symbols(definition,[spl16_42])],[avatar_definition]) ).
fof(f561,plain,
( ~ subq(sK5(sF15),sK4(sK5(sF15)))
| spl16_42 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f563,definition,
( spl16_43
<=> sK5(sF15) = sK4(sK5(sF15)) ),
introduced(definition,[new_symbols(definition,[spl16_43])],[avatar_definition]) ).
fof(f565,plain,
( sK5(sF15) = sK4(sK5(sF15))
| ~ spl16_43 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f566,plain,
( ~ spl16_42
| spl16_43 ),
inference(avatar_split_clause,[],[f557,f563,f559]) ).
fof(f567,plain,
( mem(sK0(sK5(sF15),sK4(sK5(sF15))),sK5(sF15))
| spl16_42 ),
inference(unit_resulting_resolution,[],[f57,f561]) ).
fof(f569,plain,
( mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF15)
| spl16_42 ),
inference(unit_resulting_resolution,[],[f56,f243,f567]) ).
fof(f577,plain,
( mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF14)
| mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF11)
| spl16_42 ),
inference(resolution,[],[f569,f177]) ).
fof(f580,definition,
( spl16_44
<=> mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF11) ),
introduced(definition,[new_symbols(definition,[spl16_44])],[avatar_definition]) ).
fof(f582,plain,
( mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF11)
| ~ spl16_44 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f584,definition,
( spl16_45
<=> mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF14) ),
introduced(definition,[new_symbols(definition,[spl16_45])],[avatar_definition]) ).
fof(f586,plain,
( mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF14)
| ~ spl16_45 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f587,plain,
( spl16_44
| spl16_45
| spl16_42 ),
inference(avatar_split_clause,[],[f577,f559,f584,f580]) ).
fof(f597,plain,
! [X0,X1] :
( ~ mem(X0,X1)
| subq(s(X0),X1)
| subq(s(X0),X1) ),
inference(superposition,[],[f58,f220]) ).
fof(f600,plain,
! [X0,X1] :
( subq(s(X0),X1)
| ~ mem(X0,X1) ),
inference(duplicate_literal_removal,[],[f597]) ).
fof(f602,plain,
( subq(sF7,sF6)
| subq(sF7,sF6) ),
inference(resolution,[],[f225,f58]) ).
fof(f608,plain,
subq(sF7,sF6),
inference(duplicate_literal_removal,[],[f602]) ).
fof(f609,plain,
( $false
| spl16_36 ),
inference(forward_subsumption_resolution,[],[f608,f516]) ).
fof(f610,plain,
spl16_36,
inference(avatar_contradiction_clause,[],[f609]) ).
fof(f612,plain,
( sF8 = s(sF6)
| ~ spl16_37 ),
inference(backward_demodulation,[],[f96,f520]) ).
fof(f614,plain,
( mem(sF6,sF8)
| ~ spl16_37 ),
inference(backward_demodulation,[],[f113,f520]) ).
fof(f615,plain,
( ! [X0] :
( ~ mem(X0,sF8)
| sF6 = X0 )
| ~ spl16_37 ),
inference(backward_demodulation,[],[f120,f520]) ).
fof(f626,plain,
( ! [X0] :
( ~ mem(X0,sF9)
| mem(X0,sF6)
| mem(X0,sF8) )
| ~ spl16_37 ),
inference(backward_demodulation,[],[f174,f520]) ).
fof(f728,plain,
! [X0,X1] :
( subq(X0,u(X0,X1))
| subq(X0,u(X0,X1)) ),
inference(resolution,[],[f162,f57]) ).
fof(f740,plain,
! [X0,X1] : subq(X0,u(X0,X1)),
inference(duplicate_literal_removal,[],[f728]) ).
fof(f884,plain,
! [X0,X1] :
( ~ subq(sK0(X0,p(X1)),X1)
| subq(X0,p(X1)) ),
inference(resolution,[],[f72,f58]) ).
fof(f1063,plain,
( mem(sK0(sF15,sK5(sF15)),sF14)
| mem(sK0(sF15,sK5(sF15)),sF11)
| spl16_1 ),
inference(resolution,[],[f489,f177]) ).
fof(f1066,definition,
( spl16_60
<=> mem(sK0(sF15,sK5(sF15)),sF11) ),
introduced(definition,[new_symbols(definition,[spl16_60])],[avatar_definition]) ).
fof(f1068,plain,
( mem(sK0(sF15,sK5(sF15)),sF11)
| ~ spl16_60 ),
inference(avatar_component_clause,[],[f1066]) ).
fof(f1070,definition,
( spl16_61
<=> mem(sK0(sF15,sK5(sF15)),sF14) ),
introduced(definition,[new_symbols(definition,[spl16_61])],[avatar_definition]) ).
fof(f1072,plain,
( mem(sK0(sF15,sK5(sF15)),sF14)
| ~ spl16_61 ),
inference(avatar_component_clause,[],[f1070]) ).
fof(f1073,plain,
( spl16_60
| spl16_61
| spl16_1 ),
inference(avatar_split_clause,[],[f1063,f280,f1070,f1066]) ).
fof(f1083,plain,
( ~ subq(sF15,sF15)
| ~ spl16_2 ),
inference(forward_demodulation,[],[f484,f286]) ).
fof(f1084,plain,
( $false
| ~ spl16_2 ),
inference(forward_subsumption_resolution,[],[f1083,f241]) ).
fof(f1085,plain,
~ spl16_2,
inference(avatar_contradiction_clause,[],[f1084]) ).
fof(f1101,plain,
( ~ mem(sK0(sF15,sK5(sF15)),sK5(sF15))
| spl16_1 ),
inference(unit_resulting_resolution,[],[f58,f282]) ).
fof(f1108,plain,
( mem(sK0(sF15,sK5(sF15)),sF10)
| mem(sK0(sF15,sK5(sF15)),sF9)
| ~ spl16_60 ),
inference(resolution,[],[f1068,f176]) ).
fof(f1111,definition,
( spl16_62
<=> mem(sK0(sF15,sK5(sF15)),sF9) ),
introduced(definition,[new_symbols(definition,[spl16_62])],[avatar_definition]) ).
fof(f1113,plain,
( mem(sK0(sF15,sK5(sF15)),sF9)
| ~ spl16_62 ),
inference(avatar_component_clause,[],[f1111]) ).
fof(f1115,definition,
( spl16_63
<=> mem(sK0(sF15,sK5(sF15)),sF10) ),
introduced(definition,[new_symbols(definition,[spl16_63])],[avatar_definition]) ).
fof(f1117,plain,
( mem(sK0(sF15,sK5(sF15)),sF10)
| ~ spl16_63 ),
inference(avatar_component_clause,[],[f1115]) ).
fof(f1118,plain,
( spl16_62
| spl16_63
| ~ spl16_60 ),
inference(avatar_split_clause,[],[f1108,f1066,f1115,f1111]) ).
fof(f1127,plain,
( sF13 = sK0(sF15,sK5(sF15))
| ~ spl16_61 ),
inference(resolution,[],[f1072,f123]) ).
fof(f1132,plain,
( ~ mem(sF13,sK5(sF15))
| spl16_1
| ~ spl16_61 ),
inference(backward_demodulation,[],[f1101,f1127]) ).
fof(f1145,plain,
( ~ subq(sF14,sK5(sF15))
| spl16_1
| ~ spl16_61 ),
inference(unit_resulting_resolution,[],[f56,f116,f1132]) ).
fof(f1425,plain,
atleast4p(sK4(sK5(sF15))),
inference(unit_resulting_resolution,[],[f82,f242]) ).
fof(f1534,plain,
( mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF10)
| mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF9)
| ~ spl16_44 ),
inference(resolution,[],[f582,f176]) ).
fof(f1537,definition,
( spl16_72
<=> mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF9) ),
introduced(definition,[new_symbols(definition,[spl16_72])],[avatar_definition]) ).
fof(f1539,plain,
( mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF9)
| ~ spl16_72 ),
inference(avatar_component_clause,[],[f1537]) ).
fof(f1541,definition,
( spl16_73
<=> mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF10) ),
introduced(definition,[new_symbols(definition,[spl16_73])],[avatar_definition]) ).
fof(f1543,plain,
( mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF10)
| ~ spl16_73 ),
inference(avatar_component_clause,[],[f1541]) ).
fof(f1544,plain,
( spl16_72
| spl16_73
| ~ spl16_44 ),
inference(avatar_split_clause,[],[f1534,f580,f1541,f1537]) ).
fof(f1555,plain,
( sF13 = sK0(sK5(sF15),sK4(sK5(sF15)))
| ~ spl16_45 ),
inference(resolution,[],[f586,f123]) ).
fof(f1570,plain,
( mem(sF13,sK5(sF15))
| subq(sK5(sF15),sK4(sK5(sF15)))
| ~ spl16_45 ),
inference(superposition,[],[f57,f1555]) ).
fof(f1571,plain,
( ~ mem(sF13,sK4(sK5(sF15)))
| subq(sK5(sF15),sK4(sK5(sF15)))
| ~ spl16_45 ),
inference(superposition,[],[f58,f1555]) ).
fof(f1572,plain,
( subq(sK5(sF15),sK4(sK5(sF15)))
| spl16_1
| ~ spl16_45
| ~ spl16_61 ),
inference(forward_subsumption_resolution,[],[f1570,f1132]) ).
fof(f1574,plain,
( $false
| spl16_1
| spl16_42
| ~ spl16_45
| ~ spl16_61 ),
inference(forward_subsumption_resolution,[],[f1572,f561]) ).
fof(f1575,plain,
( spl16_1
| spl16_42
| ~ spl16_45
| ~ spl16_61 ),
inference(avatar_contradiction_clause,[],[f1574]) ).
fof(f1576,plain,
( ~ mem(sF13,sK4(sK5(sF15)))
| spl16_42
| ~ spl16_45 ),
inference(forward_subsumption_resolution,[],[f1571,f561]) ).
fof(f1578,plain,
atleast3p(sK3(sK4(sK5(sF15)))),
inference(unit_resulting_resolution,[],[f79,f1425]) ).
fof(f1579,plain,
subq(sK3(sK4(sK5(sF15))),sK4(sK5(sF15))),
inference(unit_resulting_resolution,[],[f80,f1425]) ).
fof(f1581,plain,
( sK4(sK5(sF15)) = sK3(sK4(sK5(sF15)))
| ~ subq(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))) ),
inference(resolution,[],[f1579,f59]) ).
fof(f1583,definition,
( spl16_74
<=> subq(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))) ),
introduced(definition,[new_symbols(definition,[spl16_74])],[avatar_definition]) ).
fof(f1585,plain,
( ~ subq(sK4(sK5(sF15)),sK3(sK4(sK5(sF15))))
| spl16_74 ),
inference(avatar_component_clause,[],[f1583]) ).
fof(f1587,definition,
( spl16_75
<=> sK4(sK5(sF15)) = sK3(sK4(sK5(sF15))) ),
introduced(definition,[new_symbols(definition,[spl16_75])],[avatar_definition]) ).
fof(f1589,plain,
( sK4(sK5(sF15)) = sK3(sK4(sK5(sF15)))
| ~ spl16_75 ),
inference(avatar_component_clause,[],[f1587]) ).
fof(f1590,plain,
( ~ spl16_74
| spl16_75 ),
inference(avatar_split_clause,[],[f1581,f1587,f1583]) ).
fof(f1604,plain,
( ~ subq(sF14,sK4(sK5(sF15)))
| spl16_42
| ~ spl16_45 ),
inference(unit_resulting_resolution,[],[f56,f116,f1576]) ).
fof(f1611,plain,
( ~ mem(sF13,sK3(sK4(sK5(sF15))))
| spl16_42
| ~ spl16_45 ),
inference(unit_resulting_resolution,[],[f56,f1579,f1576]) ).
fof(f1618,plain,
atleast2p(sK2(sK3(sK4(sK5(sF15))))),
inference(unit_resulting_resolution,[],[f76,f1578]) ).
fof(f1619,plain,
subq(sK2(sK3(sK4(sK5(sF15)))),sK3(sK4(sK5(sF15)))),
inference(unit_resulting_resolution,[],[f77,f1578]) ).
fof(f1652,plain,
~ subq(sK2(sK3(sK4(sK5(sF15)))),p(sK1(sK2(sK3(sK4(sK5(sF15))))))),
inference(unit_resulting_resolution,[],[f73,f1618]) ).
fof(f1653,plain,
mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sK2(sK3(sK4(sK5(sF15))))),
inference(unit_resulting_resolution,[],[f74,f1618]) ).
fof(f1673,plain,
( mem(sK0(sF15,sK5(sF15)),sF6)
| mem(sK0(sF15,sK5(sF15)),sF8)
| ~ spl16_37
| ~ spl16_62 ),
inference(resolution,[],[f1113,f626]) ).
fof(f1677,definition,
( spl16_80
<=> mem(sK0(sF15,sK5(sF15)),sF8) ),
introduced(definition,[new_symbols(definition,[spl16_80])],[avatar_definition]) ).
fof(f1679,plain,
( mem(sK0(sF15,sK5(sF15)),sF8)
| ~ spl16_80 ),
inference(avatar_component_clause,[],[f1677]) ).
fof(f1681,definition,
( spl16_81
<=> mem(sK0(sF15,sK5(sF15)),sF6) ),
introduced(definition,[new_symbols(definition,[spl16_81])],[avatar_definition]) ).
fof(f1683,plain,
( mem(sK0(sF15,sK5(sF15)),sF6)
| ~ spl16_81 ),
inference(avatar_component_clause,[],[f1681]) ).
fof(f1684,plain,
( spl16_80
| spl16_81
| ~ spl16_37
| ~ spl16_62 ),
inference(avatar_split_clause,[],[f1673,f1111,f518,f1681,f1677]) ).
fof(f1696,plain,
( sF9 = sK0(sF15,sK5(sF15))
| ~ spl16_63 ),
inference(resolution,[],[f1117,f122]) ).
fof(f1700,plain,
( ~ mem(sF9,sK5(sF15))
| spl16_1
| ~ spl16_63 ),
inference(backward_demodulation,[],[f1101,f1696]) ).
fof(f1728,plain,
( ~ subq(sF10,sK5(sF15))
| spl16_1
| ~ spl16_63 ),
inference(unit_resulting_resolution,[],[f56,f115,f1700]) ).
fof(f1735,plain,
( ~ mem(sF9,sK4(sK5(sF15)))
| spl16_1
| ~ spl16_63 ),
inference(unit_resulting_resolution,[],[f56,f555,f1700]) ).
fof(f1747,plain,
( ~ subq(sF10,sK4(sK5(sF15)))
| spl16_1
| ~ spl16_63 ),
inference(unit_resulting_resolution,[],[f56,f115,f1735]) ).
fof(f1754,plain,
( ~ mem(sF9,sK3(sK4(sK5(sF15))))
| spl16_1
| ~ spl16_63 ),
inference(unit_resulting_resolution,[],[f56,f1579,f1735]) ).
fof(f1782,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sK5(sF15))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f268,f555,f1585]) ).
fof(f1787,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sK4(sK5(sF15)))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f57,f1585]) ).
fof(f1788,plain,
( ~ mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sK3(sK4(sK5(sF15))))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f58,f1585]) ).
fof(f1789,plain,
( subq(s(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15))))),sK4(sK5(sF15)))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f600,f1787]) ).
fof(f1817,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF15)
| spl16_74 ),
inference(unit_resulting_resolution,[],[f56,f243,f1782]) ).
fof(f1825,plain,
mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sK3(sK4(sK5(sF15)))),
inference(unit_resulting_resolution,[],[f56,f1619,f1653]) ).
fof(f1832,plain,
subq(s(sK1(sK2(sK3(sK4(sK5(sF15)))))),sK3(sK4(sK5(sF15)))),
inference(unit_resulting_resolution,[],[f600,f1825]) ).
fof(f1833,plain,
mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sK4(sK5(sF15))),
inference(unit_resulting_resolution,[],[f56,f1579,f1825]) ).
fof(f1840,plain,
subq(s(sK1(sK2(sK3(sK4(sK5(sF15)))))),sK4(sK5(sF15))),
inference(unit_resulting_resolution,[],[f600,f1833]) ).
fof(f1841,plain,
mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sK5(sF15)),
inference(unit_resulting_resolution,[],[f56,f555,f1833]) ).
fof(f1848,plain,
subq(s(sK1(sK2(sK3(sK4(sK5(sF15)))))),sK5(sF15)),
inference(unit_resulting_resolution,[],[f600,f1841]) ).
fof(f1849,plain,
mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF15),
inference(unit_resulting_resolution,[],[f56,f243,f1841]) ).
fof(f1862,plain,
( mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF14)
| mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF11) ),
inference(resolution,[],[f1849,f177]) ).
fof(f1865,definition,
( spl16_82
<=> mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF11) ),
introduced(definition,[new_symbols(definition,[spl16_82])],[avatar_definition]) ).
fof(f1867,plain,
( mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF11)
| ~ spl16_82 ),
inference(avatar_component_clause,[],[f1865]) ).
fof(f1869,definition,
( spl16_83
<=> mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF14) ),
introduced(definition,[new_symbols(definition,[spl16_83])],[avatar_definition]) ).
fof(f1871,plain,
( mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF14)
| ~ spl16_83 ),
inference(avatar_component_clause,[],[f1869]) ).
fof(f1872,plain,
( spl16_82
| spl16_83 ),
inference(avatar_split_clause,[],[f1862,f1869,f1865]) ).
fof(f1881,plain,
( mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF10)
| mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF9)
| ~ spl16_82 ),
inference(resolution,[],[f1867,f176]) ).
fof(f1884,definition,
( spl16_84
<=> mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF9) ),
introduced(definition,[new_symbols(definition,[spl16_84])],[avatar_definition]) ).
fof(f1886,plain,
( mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF9)
| ~ spl16_84 ),
inference(avatar_component_clause,[],[f1884]) ).
fof(f1888,definition,
( spl16_85
<=> mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF10) ),
introduced(definition,[new_symbols(definition,[spl16_85])],[avatar_definition]) ).
fof(f1890,plain,
( mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF10)
| ~ spl16_85 ),
inference(avatar_component_clause,[],[f1888]) ).
fof(f1891,plain,
( spl16_84
| spl16_85
| ~ spl16_82 ),
inference(avatar_split_clause,[],[f1881,f1865,f1888,f1884]) ).
fof(f1903,plain,
( sF13 = sK1(sK2(sK3(sK4(sK5(sF15)))))
| ~ spl16_83 ),
inference(resolution,[],[f1871,f123]) ).
fof(f1905,plain,
( ~ subq(sK2(sK3(sK4(sK5(sF15)))),p(sF13))
| ~ spl16_83 ),
inference(backward_demodulation,[],[f1652,f1903]) ).
fof(f1912,plain,
( subq(s(sF13),sK3(sK4(sK5(sF15))))
| ~ spl16_83 ),
inference(backward_demodulation,[],[f1832,f1903]) ).
fof(f1917,plain,
( subq(s(sF13),sK4(sK5(sF15)))
| ~ spl16_83 ),
inference(backward_demodulation,[],[f1840,f1903]) ).
fof(f1918,plain,
( mem(sF13,sK5(sF15))
| ~ spl16_83 ),
inference(backward_demodulation,[],[f1841,f1903]) ).
fof(f1945,plain,
( subq(sF14,sK4(sK5(sF15)))
| ~ spl16_83 ),
inference(forward_demodulation,[],[f1917,f108]) ).
fof(f1948,plain,
( subq(sF14,sK3(sK4(sK5(sF15))))
| ~ spl16_83 ),
inference(forward_demodulation,[],[f1912,f108]) ).
fof(f1953,plain,
( $false
| spl16_42
| ~ spl16_45
| ~ spl16_83 ),
inference(forward_subsumption_resolution,[],[f1945,f1604]) ).
fof(f1954,plain,
( spl16_42
| ~ spl16_45
| ~ spl16_83 ),
inference(avatar_contradiction_clause,[],[f1953]) ).
fof(f3257,plain,
( ~ mem(sF13,sK5(sF15))
| spl16_1
| ~ spl16_61 ),
inference(forward_demodulation,[],[f1101,f1127]) ).
fof(f3264,plain,
( $false
| spl16_1
| ~ spl16_61
| ~ spl16_83 ),
inference(forward_subsumption_resolution,[],[f3257,f1918]) ).
fof(f3265,plain,
( spl16_1
| ~ spl16_61
| ~ spl16_83 ),
inference(avatar_contradiction_clause,[],[f3264]) ).
fof(f4152,plain,
~ subq(sK5(sF15),sK4(sK5(sF15))),
inference(unit_resulting_resolution,[],[f81,f242]) ).
fof(f4158,plain,
( ~ subq(sK5(sF15),sK5(sF15))
| ~ spl16_43 ),
inference(forward_demodulation,[],[f4152,f565]) ).
fof(f4161,plain,
( $false
| ~ spl16_43 ),
inference(forward_subsumption_resolution,[],[f4158,f241]) ).
fof(f4162,plain,
~ spl16_43,
inference(avatar_contradiction_clause,[],[f4161]) ).
fof(f4240,plain,
( mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF6)
| mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF8)
| ~ spl16_37
| ~ spl16_72 ),
inference(resolution,[],[f1539,f626]) ).
fof(f4244,definition,
( spl16_131
<=> mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF8) ),
introduced(definition,[new_symbols(definition,[spl16_131])],[avatar_definition]) ).
fof(f4246,plain,
( mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF8)
| ~ spl16_131 ),
inference(avatar_component_clause,[],[f4244]) ).
fof(f4248,definition,
( spl16_132
<=> mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF6) ),
introduced(definition,[new_symbols(definition,[spl16_132])],[avatar_definition]) ).
fof(f4250,plain,
( mem(sK0(sK5(sF15),sK4(sK5(sF15))),sF6)
| ~ spl16_132 ),
inference(avatar_component_clause,[],[f4248]) ).
fof(f4251,plain,
( spl16_131
| spl16_132
| ~ spl16_37
| ~ spl16_72 ),
inference(avatar_split_clause,[],[f4240,f1537,f518,f4248,f4244]) ).
fof(f4325,plain,
( e = sK0(sK5(sF15),sK4(sK5(sF15)))
| ~ spl16_132 ),
inference(resolution,[],[f4250,f119]) ).
fof(f4363,plain,
( ~ mem(e,sK4(sK5(sF15)))
| subq(sK5(sF15),sK4(sK5(sF15)))
| ~ spl16_132 ),
inference(superposition,[],[f58,f4325]) ).
fof(f4364,plain,
( ~ mem(e,sK4(sK5(sF15)))
| spl16_42
| ~ spl16_132 ),
inference(forward_subsumption_resolution,[],[f4363,f561]) ).
fof(f4413,plain,
( ~ mem(e,u(sK4(sK5(sF15)),e))
| spl16_42
| ~ spl16_132 ),
inference(unit_resulting_resolution,[],[f63,f60,f4364]) ).
fof(f4465,plain,
( mem(sK0(sK5(sF15),sK4(sK5(sF15))),sK5(sF15))
| spl16_42 ),
inference(unit_resulting_resolution,[],[f268,f241,f561]) ).
fof(f4469,plain,
( ~ mem(sK0(sK5(sF15),sK4(sK5(sF15))),sK4(sK5(sF15)))
| spl16_42 ),
inference(unit_resulting_resolution,[],[f58,f561]) ).
fof(f4618,plain,
( ~ mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF14)
| spl16_74
| ~ spl16_83 ),
inference(unit_resulting_resolution,[],[f56,f1948,f1788]) ).
fof(f4648,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF14)
| mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF11)
| spl16_74 ),
inference(resolution,[],[f1817,f177]) ).
fof(f4650,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF11)
| spl16_74
| ~ spl16_83 ),
inference(forward_subsumption_resolution,[],[f4648,f4618]) ).
fof(f4661,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF10)
| mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF9)
| spl16_74
| ~ spl16_83 ),
inference(resolution,[],[f4650,f176]) ).
fof(f4664,definition,
( spl16_137
<=> mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF9) ),
introduced(definition,[new_symbols(definition,[spl16_137])],[avatar_definition]) ).
fof(f4665,plain,
( ~ mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF9)
| spl16_137 ),
inference(avatar_component_clause,[],[f4664]) ).
fof(f4666,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF9)
| ~ spl16_137 ),
inference(avatar_component_clause,[],[f4664]) ).
fof(f4668,definition,
( spl16_138
<=> mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF10) ),
introduced(definition,[new_symbols(definition,[spl16_138])],[avatar_definition]) ).
fof(f4669,plain,
( ~ mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF10)
| spl16_138 ),
inference(avatar_component_clause,[],[f4668]) ).
fof(f4670,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF10)
| ~ spl16_138 ),
inference(avatar_component_clause,[],[f4668]) ).
fof(f4671,plain,
( spl16_137
| spl16_138
| spl16_74
| ~ spl16_83 ),
inference(avatar_split_clause,[],[f4661,f1869,f1583,f4668,f4664]) ).
fof(f4680,plain,
( ~ subq(sF10,sK3(sK4(sK5(sF15))))
| spl16_74
| ~ spl16_138 ),
inference(unit_resulting_resolution,[],[f56,f1788,f4670]) ).
fof(f4685,plain,
( sF9 = sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15))))
| ~ spl16_138 ),
inference(resolution,[],[f4670,f122]) ).
fof(f4691,plain,
( ~ mem(sF9,sK3(sK4(sK5(sF15))))
| spl16_74
| ~ spl16_138 ),
inference(backward_demodulation,[],[f1788,f4685]) ).
fof(f4692,plain,
( subq(s(sF9),sK4(sK5(sF15)))
| spl16_74
| ~ spl16_138 ),
inference(backward_demodulation,[],[f1789,f4685]) ).
fof(f4729,plain,
( subq(sF10,sK4(sK5(sF15)))
| spl16_74
| ~ spl16_138 ),
inference(forward_demodulation,[],[f4692,f100]) ).
fof(f4737,plain,
( $false
| spl16_1
| ~ spl16_63
| spl16_74
| ~ spl16_138 ),
inference(forward_subsumption_resolution,[],[f4729,f1747]) ).
fof(f4738,plain,
( spl16_1
| ~ spl16_63
| spl16_74
| ~ spl16_138 ),
inference(avatar_contradiction_clause,[],[f4737]) ).
fof(f6047,plain,
( sF9 = sK0(sK5(sF15),sK4(sK5(sF15)))
| ~ spl16_73 ),
inference(resolution,[],[f1543,f122]) ).
fof(f6065,plain,
( mem(sF9,sK5(sF15))
| spl16_42
| ~ spl16_73 ),
inference(backward_demodulation,[],[f4465,f6047]) ).
fof(f6066,plain,
( ~ mem(sF9,sK4(sK5(sF15)))
| spl16_42
| ~ spl16_73 ),
inference(backward_demodulation,[],[f4469,f6047]) ).
fof(f6078,plain,
( $false
| spl16_1
| spl16_42
| ~ spl16_63
| ~ spl16_73 ),
inference(forward_subsumption_resolution,[],[f6065,f1700]) ).
fof(f6079,plain,
( spl16_1
| spl16_42
| ~ spl16_63
| ~ spl16_73 ),
inference(avatar_contradiction_clause,[],[f6078]) ).
fof(f6126,plain,
( sF6 = sK0(sK5(sF15),sK4(sK5(sF15)))
| ~ spl16_37
| ~ spl16_131 ),
inference(resolution,[],[f4246,f615]) ).
fof(f6148,plain,
( ~ mem(sF6,sK4(sK5(sF15)))
| ~ spl16_37
| spl16_42
| ~ spl16_131 ),
inference(backward_demodulation,[],[f4469,f6126]) ).
fof(f6221,plain,
( ~ subq(sF10,sK4(sK5(sF15)))
| spl16_42
| ~ spl16_73 ),
inference(unit_resulting_resolution,[],[f56,f115,f6066]) ).
fof(f6366,plain,
( sF6 = sK0(sF15,sK5(sF15))
| ~ spl16_37
| ~ spl16_80 ),
inference(resolution,[],[f1679,f615]) ).
fof(f6372,plain,
( ~ mem(sF6,sK5(sF15))
| spl16_1
| ~ spl16_37
| ~ spl16_80 ),
inference(backward_demodulation,[],[f1101,f6366]) ).
fof(f6424,plain,
( e = sK0(sF15,sK5(sF15))
| ~ spl16_81 ),
inference(resolution,[],[f1683,f119]) ).
fof(f6428,plain,
( ~ mem(e,sK5(sF15))
| spl16_1
| ~ spl16_81 ),
inference(backward_demodulation,[],[f1101,f6424]) ).
fof(f6528,plain,
( mem(e,sK5(sF15))
| spl16_42
| ~ spl16_132 ),
inference(forward_demodulation,[],[f4465,f4325]) ).
fof(f6534,plain,
( $false
| spl16_1
| spl16_42
| ~ spl16_81
| ~ spl16_132 ),
inference(forward_subsumption_resolution,[],[f6528,f6428]) ).
fof(f6535,plain,
( spl16_1
| spl16_42
| ~ spl16_81
| ~ spl16_132 ),
inference(avatar_contradiction_clause,[],[f6534]) ).
fof(f6655,plain,
( mem(sF6,sK5(sF15))
| ~ spl16_37
| spl16_42
| ~ spl16_131 ),
inference(forward_demodulation,[],[f4465,f6126]) ).
fof(f6666,plain,
( $false
| spl16_1
| ~ spl16_37
| spl16_42
| ~ spl16_80
| ~ spl16_131 ),
inference(forward_subsumption_resolution,[],[f6655,f6372]) ).
fof(f6667,plain,
( spl16_1
| ~ spl16_37
| spl16_42
| ~ spl16_80
| ~ spl16_131 ),
inference(avatar_contradiction_clause,[],[f6666]) ).
fof(f6828,definition,
( spl16_170
<=> mem(e,sK4(sK5(sF15))) ),
introduced(definition,[new_symbols(definition,[spl16_170])],[avatar_definition]) ).
fof(f6829,plain,
( ~ mem(e,sK4(sK5(sF15)))
| spl16_170 ),
inference(avatar_component_clause,[],[f6828]) ).
fof(f6971,plain,
( ~ subq(sF6,sK4(sK5(sF15)))
| spl16_170 ),
inference(unit_resulting_resolution,[],[f56,f112,f6829]) ).
fof(f7026,plain,
( ~ subq(sF6,sK5(sF15))
| spl16_1
| ~ spl16_81 ),
inference(unit_resulting_resolution,[],[f56,f112,f6428]) ).
fof(f7036,plain,
( ~ mem(e,sK4(sK5(sF15)))
| spl16_1
| ~ spl16_81 ),
inference(unit_resulting_resolution,[],[f56,f555,f6428]) ).
fof(f7099,plain,
( ~ subq(sF8,sK4(sK5(sF15)))
| ~ spl16_37
| spl16_42
| ~ spl16_131 ),
inference(unit_resulting_resolution,[],[f56,f614,f6148]) ).
fof(f7137,plain,
( ~ mem(sF9,sK2(sK3(sK4(sK5(sF15)))))
| spl16_74
| ~ spl16_138 ),
inference(unit_resulting_resolution,[],[f56,f1619,f4691]) ).
fof(f7364,plain,
( ~ subq(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF13)
| ~ spl16_83 ),
inference(unit_resulting_resolution,[],[f884,f1905]) ).
fof(f7365,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sK3(sK4(sK5(sF15))))
| ~ spl16_83 ),
inference(unit_resulting_resolution,[],[f268,f1619,f1905]) ).
fof(f7373,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sK5(sF15))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f268,f555,f1585]) ).
fof(f7376,plain,
( ! [X0] : mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),u(sK4(sK5(sF15)),X0))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f268,f740,f1585]) ).
fof(f7377,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sK4(sK5(sF15)))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f268,f241,f1585]) ).
fof(f7381,plain,
( ~ mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sK3(sK4(sK5(sF15))))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f58,f1585]) ).
fof(f7421,plain,
( subq(s(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13))),sK3(sK4(sK5(sF15))))
| ~ spl16_83 ),
inference(unit_resulting_resolution,[],[f600,f7365]) ).
fof(f7422,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sK4(sK5(sF15)))
| ~ spl16_83 ),
inference(unit_resulting_resolution,[],[f56,f1579,f7365]) ).
fof(f7430,plain,
( subq(s(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13))),sK4(sK5(sF15)))
| ~ spl16_83 ),
inference(unit_resulting_resolution,[],[f600,f7422]) ).
fof(f7431,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sK5(sF15))
| ~ spl16_83 ),
inference(unit_resulting_resolution,[],[f56,f555,f7422]) ).
fof(f7441,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF15)
| ~ spl16_83 ),
inference(unit_resulting_resolution,[],[f56,f243,f7431]) ).
fof(f7457,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF14)
| mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF11)
| ~ spl16_83 ),
inference(resolution,[],[f7441,f177]) ).
fof(f7460,definition,
( spl16_189
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF11) ),
introduced(definition,[new_symbols(definition,[spl16_189])],[avatar_definition]) ).
fof(f7462,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF11)
| ~ spl16_189 ),
inference(avatar_component_clause,[],[f7460]) ).
fof(f7464,definition,
( spl16_190
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF14) ),
introduced(definition,[new_symbols(definition,[spl16_190])],[avatar_definition]) ).
fof(f7466,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF14)
| ~ spl16_190 ),
inference(avatar_component_clause,[],[f7464]) ).
fof(f7467,plain,
( spl16_189
| spl16_190
| ~ spl16_83 ),
inference(avatar_split_clause,[],[f7457,f1869,f7464,f7460]) ).
fof(f7477,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF10)
| mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF9)
| ~ spl16_189 ),
inference(resolution,[],[f7462,f176]) ).
fof(f7480,definition,
( spl16_191
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF9) ),
introduced(definition,[new_symbols(definition,[spl16_191])],[avatar_definition]) ).
fof(f7482,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF9)
| ~ spl16_191 ),
inference(avatar_component_clause,[],[f7480]) ).
fof(f7484,definition,
( spl16_192
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF10) ),
introduced(definition,[new_symbols(definition,[spl16_192])],[avatar_definition]) ).
fof(f7486,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF10)
| ~ spl16_192 ),
inference(avatar_component_clause,[],[f7484]) ).
fof(f7487,plain,
( spl16_191
| spl16_192
| ~ spl16_189 ),
inference(avatar_split_clause,[],[f7477,f7460,f7484,f7480]) ).
fof(f7503,plain,
( sF9 = sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13))
| ~ spl16_192 ),
inference(resolution,[],[f7486,f122]) ).
fof(f7511,plain,
( subq(s(sF9),sK3(sK4(sK5(sF15))))
| ~ spl16_83
| ~ spl16_192 ),
inference(backward_demodulation,[],[f7421,f7503]) ).
fof(f7512,plain,
( mem(sF9,sK4(sK5(sF15)))
| ~ spl16_83
| ~ spl16_192 ),
inference(backward_demodulation,[],[f7422,f7503]) ).
fof(f7517,plain,
( mem(sF9,sK5(sF15))
| ~ spl16_83
| ~ spl16_192 ),
inference(backward_demodulation,[],[f7431,f7503]) ).
fof(f7556,plain,
( subq(sF10,sK3(sK4(sK5(sF15))))
| ~ spl16_83
| ~ spl16_192 ),
inference(forward_demodulation,[],[f7511,f100]) ).
fof(f7562,plain,
( $false
| spl16_74
| ~ spl16_83
| ~ spl16_138
| ~ spl16_192 ),
inference(forward_subsumption_resolution,[],[f7556,f4680]) ).
fof(f7563,plain,
( spl16_74
| ~ spl16_83
| ~ spl16_138
| ~ spl16_192 ),
inference(avatar_contradiction_clause,[],[f7562]) ).
fof(f7581,plain,
( sF13 = sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13))
| ~ spl16_190 ),
inference(resolution,[],[f7466,f123]) ).
fof(f7583,plain,
( ~ subq(sF13,sF13)
| ~ spl16_83
| ~ spl16_190 ),
inference(backward_demodulation,[],[f7364,f7581]) ).
fof(f7635,plain,
( $false
| ~ spl16_83
| ~ spl16_190 ),
inference(forward_subsumption_resolution,[],[f7583,f241]) ).
fof(f7636,plain,
( ~ spl16_83
| ~ spl16_190 ),
inference(avatar_contradiction_clause,[],[f7635]) ).
fof(f7646,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF6)
| mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF8)
| ~ spl16_37
| ~ spl16_191 ),
inference(resolution,[],[f7482,f626]) ).
fof(f7650,definition,
( spl16_193
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF8) ),
introduced(definition,[new_symbols(definition,[spl16_193])],[avatar_definition]) ).
fof(f7652,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF8)
| ~ spl16_193 ),
inference(avatar_component_clause,[],[f7650]) ).
fof(f7654,definition,
( spl16_194
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF6) ),
introduced(definition,[new_symbols(definition,[spl16_194])],[avatar_definition]) ).
fof(f7656,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13)),sF6)
| ~ spl16_194 ),
inference(avatar_component_clause,[],[f7654]) ).
fof(f7657,plain,
( spl16_193
| spl16_194
| ~ spl16_37
| ~ spl16_191 ),
inference(avatar_split_clause,[],[f7646,f7480,f518,f7654,f7650]) ).
fof(f7691,plain,
( e = sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13))
| ~ spl16_194 ),
inference(resolution,[],[f7656,f119]) ).
fof(f7693,plain,
( ~ subq(e,sF13)
| ~ spl16_83
| ~ spl16_194 ),
inference(backward_demodulation,[],[f7364,f7691]) ).
fof(f7761,plain,
( $false
| ~ spl16_83
| ~ spl16_194 ),
inference(forward_subsumption_resolution,[],[f7693,f219]) ).
fof(f7762,plain,
( ~ spl16_83
| ~ spl16_194 ),
inference(avatar_contradiction_clause,[],[f7761]) ).
fof(f7810,plain,
( sF6 = sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF13))
| ~ spl16_37
| ~ spl16_193 ),
inference(resolution,[],[f7652,f615]) ).
fof(f7825,plain,
( subq(s(sF6),sK4(sK5(sF15)))
| ~ spl16_37
| ~ spl16_83
| ~ spl16_193 ),
inference(backward_demodulation,[],[f7430,f7810]) ).
fof(f7826,plain,
( mem(sF6,sK5(sF15))
| ~ spl16_37
| ~ spl16_83
| ~ spl16_193 ),
inference(backward_demodulation,[],[f7431,f7810]) ).
fof(f7870,plain,
( subq(sF8,sK4(sK5(sF15)))
| ~ spl16_37
| ~ spl16_83
| ~ spl16_193 ),
inference(forward_demodulation,[],[f7825,f612]) ).
fof(f7877,plain,
( $false
| ~ spl16_37
| spl16_42
| ~ spl16_83
| ~ spl16_131
| ~ spl16_193 ),
inference(forward_subsumption_resolution,[],[f7870,f7099]) ).
fof(f7878,plain,
( ~ spl16_37
| spl16_42
| ~ spl16_83
| ~ spl16_131
| ~ spl16_193 ),
inference(avatar_contradiction_clause,[],[f7877]) ).
fof(f7931,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF6)
| mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF8)
| ~ spl16_37
| ~ spl16_137 ),
inference(resolution,[],[f4666,f626]) ).
fof(f7935,definition,
( spl16_195
<=> mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF8) ),
introduced(definition,[new_symbols(definition,[spl16_195])],[avatar_definition]) ).
fof(f7937,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF8)
| ~ spl16_195 ),
inference(avatar_component_clause,[],[f7935]) ).
fof(f7939,definition,
( spl16_196
<=> mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF6) ),
introduced(definition,[new_symbols(definition,[spl16_196])],[avatar_definition]) ).
fof(f7941,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF6)
| ~ spl16_196 ),
inference(avatar_component_clause,[],[f7939]) ).
fof(f7942,plain,
( spl16_195
| spl16_196
| ~ spl16_37
| ~ spl16_137 ),
inference(avatar_split_clause,[],[f7931,f4664,f518,f7939,f7935]) ).
fof(f8000,plain,
( e = sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15))))
| ~ spl16_196 ),
inference(resolution,[],[f7941,f119]) ).
fof(f8004,plain,
( mem(e,sK5(sF15))
| spl16_74
| ~ spl16_196 ),
inference(backward_demodulation,[],[f7373,f8000]) ).
fof(f8007,plain,
( ! [X0] : mem(e,u(sK4(sK5(sF15)),X0))
| spl16_74
| ~ spl16_196 ),
inference(backward_demodulation,[],[f7376,f8000]) ).
fof(f8008,plain,
( mem(e,sK4(sK5(sF15)))
| spl16_74
| ~ spl16_196 ),
inference(backward_demodulation,[],[f7377,f8000]) ).
fof(f8040,plain,
( $false
| spl16_74
| spl16_170
| ~ spl16_196 ),
inference(forward_subsumption_resolution,[],[f8008,f6829]) ).
fof(f8041,plain,
( spl16_74
| spl16_170
| ~ spl16_196 ),
inference(avatar_contradiction_clause,[],[f8040]) ).
fof(f8044,plain,
( $false
| spl16_1
| spl16_74
| ~ spl16_81
| ~ spl16_196 ),
inference(forward_subsumption_resolution,[],[f8004,f6428]) ).
fof(f8045,plain,
( spl16_1
| spl16_74
| ~ spl16_81
| ~ spl16_196 ),
inference(avatar_contradiction_clause,[],[f8044]) ).
fof(f8080,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF9)
| ~ spl16_195 ),
inference(unit_resulting_resolution,[],[f141,f7937]) ).
fof(f8089,plain,
( sF6 = sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15))))
| ~ spl16_37
| ~ spl16_195 ),
inference(resolution,[],[f7937,f615]) ).
fof(f8099,plain,
( mem(sF6,sK4(sK5(sF15)))
| ~ spl16_37
| spl16_74
| ~ spl16_195 ),
inference(backward_demodulation,[],[f7377,f8089]) ).
fof(f8100,plain,
( ~ mem(sF6,sK3(sK4(sK5(sF15))))
| ~ spl16_37
| spl16_74
| ~ spl16_195 ),
inference(backward_demodulation,[],[f7381,f8089]) ).
fof(f8131,plain,
( $false
| ~ spl16_37
| spl16_42
| spl16_74
| ~ spl16_131
| ~ spl16_195 ),
inference(forward_subsumption_resolution,[],[f8099,f6148]) ).
fof(f8132,plain,
( ~ spl16_37
| spl16_42
| spl16_74
| ~ spl16_131
| ~ spl16_195 ),
inference(avatar_contradiction_clause,[],[f8131]) ).
fof(f8181,plain,
( ~ mem(sF9,sK5(sF15))
| spl16_1
| ~ spl16_63 ),
inference(forward_demodulation,[],[f1101,f1696]) ).
fof(f8188,plain,
( $false
| spl16_1
| ~ spl16_63
| ~ spl16_83
| ~ spl16_192 ),
inference(forward_subsumption_resolution,[],[f8181,f7517]) ).
fof(f8189,plain,
( spl16_1
| ~ spl16_63
| ~ spl16_83
| ~ spl16_192 ),
inference(avatar_contradiction_clause,[],[f8188]) ).
fof(f8207,plain,
( ~ spl16_170
| spl16_1
| ~ spl16_81 ),
inference(avatar_split_clause,[],[f7036,f1681,f280,f6828]) ).
fof(f8210,plain,
( spl16_137
| ~ spl16_195 ),
inference(avatar_split_clause,[],[f8080,f7935,f4664]) ).
fof(f8253,plain,
( ~ mem(sF9,sK4(sK5(sF15)))
| spl16_42
| ~ spl16_73 ),
inference(forward_demodulation,[],[f4469,f6047]) ).
fof(f8270,plain,
( $false
| spl16_42
| ~ spl16_73
| ~ spl16_83
| ~ spl16_192 ),
inference(forward_subsumption_resolution,[],[f8253,f7512]) ).
fof(f8271,plain,
( spl16_42
| ~ spl16_73
| ~ spl16_83
| ~ spl16_192 ),
inference(avatar_contradiction_clause,[],[f8270]) ).
fof(f8283,plain,
( mem(sF6,sK3(sK4(sK5(sF15))))
| ~ spl16_37
| ~ spl16_83
| ~ spl16_193 ),
inference(forward_demodulation,[],[f7365,f7810]) ).
fof(f8317,plain,
( $false
| ~ spl16_37
| spl16_74
| ~ spl16_83
| ~ spl16_193
| ~ spl16_195 ),
inference(forward_subsumption_resolution,[],[f8283,f8100]) ).
fof(f8318,plain,
( ~ spl16_37
| spl16_74
| ~ spl16_83
| ~ spl16_193
| ~ spl16_195 ),
inference(avatar_contradiction_clause,[],[f8317]) ).
fof(f8341,plain,
( mem(sF9,sK4(sK5(sF15)))
| spl16_74
| ~ spl16_138 ),
inference(forward_demodulation,[],[f7377,f4685]) ).
fof(f8343,plain,
( $false
| spl16_42
| ~ spl16_73
| spl16_74
| ~ spl16_138 ),
inference(forward_subsumption_resolution,[],[f8341,f6066]) ).
fof(f8344,plain,
( spl16_42
| ~ spl16_73
| spl16_74
| ~ spl16_138 ),
inference(avatar_contradiction_clause,[],[f8343]) ).
fof(f8369,plain,
( ~ mem(sF6,sK5(sF15))
| spl16_1
| ~ spl16_37
| ~ spl16_80 ),
inference(forward_demodulation,[],[f1101,f6366]) ).
fof(f8373,plain,
( $false
| spl16_1
| ~ spl16_37
| ~ spl16_80
| ~ spl16_83
| ~ spl16_193 ),
inference(forward_subsumption_resolution,[],[f8369,f7826]) ).
fof(f8374,plain,
( spl16_1
| ~ spl16_37
| ~ spl16_80
| ~ spl16_83
| ~ spl16_193 ),
inference(avatar_contradiction_clause,[],[f8373]) ).
fof(f8388,plain,
( $false
| spl16_42
| spl16_74
| ~ spl16_132
| ~ spl16_196 ),
inference(forward_subsumption_resolution,[],[f4413,f8007]) ).
fof(f8389,plain,
( spl16_42
| spl16_74
| ~ spl16_132
| ~ spl16_196 ),
inference(avatar_contradiction_clause,[],[f8388]) ).
fof(f8479,plain,
( mem(sF6,sK5(sF15))
| ~ spl16_37
| spl16_74
| ~ spl16_195 ),
inference(forward_demodulation,[],[f7373,f8089]) ).
fof(f8484,plain,
( $false
| spl16_1
| ~ spl16_37
| spl16_74
| ~ spl16_80
| ~ spl16_195 ),
inference(forward_subsumption_resolution,[],[f8479,f6372]) ).
fof(f8485,plain,
( spl16_1
| ~ spl16_37
| spl16_74
| ~ spl16_80
| ~ spl16_195 ),
inference(avatar_contradiction_clause,[],[f8484]) ).
fof(f13291,plain,
( ~ mem(sK0(sK5(sF15),sK4(sK5(sF15))),sK4(sK5(sF15)))
| spl16_42 ),
inference(unit_resulting_resolution,[],[f58,f561]) ).
fof(f13465,plain,
( ~ mem(sK0(sF15,sK5(sF15)),sK5(sF15))
| spl16_1 ),
inference(unit_resulting_resolution,[],[f58,f282]) ).
fof(f16718,plain,
~ subq(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),
inference(unit_resulting_resolution,[],[f78,f1425]) ).
fof(f16726,plain,
( ~ subq(sK4(sK5(sF15)),sK4(sK5(sF15)))
| ~ spl16_75 ),
inference(forward_demodulation,[],[f16718,f1589]) ).
fof(f16729,plain,
( $false
| ~ spl16_75 ),
inference(forward_subsumption_resolution,[],[f16726,f241]) ).
fof(f16730,plain,
~ spl16_75,
inference(avatar_contradiction_clause,[],[f16729]) ).
fof(f16781,plain,
( ~ mem(sF9,sK3(sK4(sK5(sF15))))
| spl16_42
| ~ spl16_73 ),
inference(unit_resulting_resolution,[],[f56,f6066,f1579]) ).
fof(f16792,plain,
( mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF6)
| mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF8)
| ~ spl16_37
| ~ spl16_84 ),
inference(resolution,[],[f1886,f626]) ).
fof(f16797,definition,
( spl16_238
<=> mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF8) ),
introduced(definition,[new_symbols(definition,[spl16_238])],[avatar_definition]) ).
fof(f16799,plain,
( mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF8)
| ~ spl16_238 ),
inference(avatar_component_clause,[],[f16797]) ).
fof(f16801,definition,
( spl16_239
<=> mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF6) ),
introduced(definition,[new_symbols(definition,[spl16_239])],[avatar_definition]) ).
fof(f16803,plain,
( mem(sK1(sK2(sK3(sK4(sK5(sF15))))),sF6)
| ~ spl16_239 ),
inference(avatar_component_clause,[],[f16801]) ).
fof(f16804,plain,
( spl16_238
| spl16_239
| ~ spl16_37
| ~ spl16_84 ),
inference(avatar_split_clause,[],[f16792,f1884,f518,f16801,f16797]) ).
fof(f16871,plain,
( sF6 = sK1(sK2(sK3(sK4(sK5(sF15)))))
| ~ spl16_37
| ~ spl16_238 ),
inference(resolution,[],[f16799,f615]) ).
fof(f16876,plain,
( ~ subq(sK2(sK3(sK4(sK5(sF15)))),p(sF6))
| ~ spl16_37
| ~ spl16_238 ),
inference(backward_demodulation,[],[f1652,f16871]) ).
fof(f16879,plain,
( mem(sF6,sK3(sK4(sK5(sF15))))
| ~ spl16_37
| ~ spl16_238 ),
inference(backward_demodulation,[],[f1825,f16871]) ).
fof(f16938,plain,
( $false
| ~ spl16_37
| spl16_74
| ~ spl16_195
| ~ spl16_238 ),
inference(forward_subsumption_resolution,[],[f16879,f8100]) ).
fof(f16939,plain,
( ~ spl16_37
| spl16_74
| ~ spl16_195
| ~ spl16_238 ),
inference(avatar_contradiction_clause,[],[f16938]) ).
fof(f17020,plain,
( e = sK1(sK2(sK3(sK4(sK5(sF15)))))
| ~ spl16_239 ),
inference(resolution,[],[f16803,f119]) ).
fof(f17023,plain,
( ~ subq(sK2(sK3(sK4(sK5(sF15)))),p(e))
| ~ spl16_239 ),
inference(backward_demodulation,[],[f1652,f17020]) ).
fof(f17030,plain,
( subq(s(e),sK3(sK4(sK5(sF15))))
| ~ spl16_239 ),
inference(backward_demodulation,[],[f1832,f17020]) ).
fof(f17035,plain,
( subq(s(e),sK4(sK5(sF15)))
| ~ spl16_239 ),
inference(backward_demodulation,[],[f1840,f17020]) ).
fof(f17040,plain,
( subq(s(e),sK5(sF15))
| ~ spl16_239 ),
inference(backward_demodulation,[],[f1848,f17020]) ).
fof(f17084,plain,
( subq(sF6,sK5(sF15))
| ~ spl16_239 ),
inference(forward_demodulation,[],[f17040,f92]) ).
fof(f17088,plain,
( subq(sF6,sK4(sK5(sF15)))
| ~ spl16_239 ),
inference(forward_demodulation,[],[f17035,f92]) ).
fof(f17091,plain,
( subq(sF6,sK3(sK4(sK5(sF15))))
| ~ spl16_239 ),
inference(forward_demodulation,[],[f17030,f92]) ).
fof(f17096,plain,
( $false
| spl16_1
| ~ spl16_81
| ~ spl16_239 ),
inference(forward_subsumption_resolution,[],[f17084,f7026]) ).
fof(f17097,plain,
( spl16_1
| ~ spl16_81
| ~ spl16_239 ),
inference(avatar_contradiction_clause,[],[f17096]) ).
fof(f17098,plain,
( $false
| spl16_170
| ~ spl16_239 ),
inference(forward_subsumption_resolution,[],[f17088,f6971]) ).
fof(f17099,plain,
( spl16_170
| ~ spl16_239 ),
inference(avatar_contradiction_clause,[],[f17098]) ).
fof(f17115,plain,
( sF9 = sK1(sK2(sK3(sK4(sK5(sF15)))))
| ~ spl16_85 ),
inference(resolution,[],[f1890,f122]) ).
fof(f17118,plain,
( ~ subq(sK2(sK3(sK4(sK5(sF15)))),p(sF9))
| ~ spl16_85 ),
inference(backward_demodulation,[],[f1652,f17115]) ).
fof(f17119,plain,
( mem(sF9,sK2(sK3(sK4(sK5(sF15)))))
| ~ spl16_85 ),
inference(backward_demodulation,[],[f1653,f17115]) ).
fof(f17130,plain,
( subq(s(sF9),sK4(sK5(sF15)))
| ~ spl16_85 ),
inference(backward_demodulation,[],[f1840,f17115]) ).
fof(f17172,plain,
( subq(sF10,sK4(sK5(sF15)))
| ~ spl16_85 ),
inference(forward_demodulation,[],[f17130,f100]) ).
fof(f17180,plain,
( $false
| spl16_42
| ~ spl16_73
| ~ spl16_85 ),
inference(forward_subsumption_resolution,[],[f17172,f6221]) ).
fof(f17181,plain,
( spl16_42
| ~ spl16_73
| ~ spl16_85 ),
inference(avatar_contradiction_clause,[],[f17180]) ).
fof(f17263,plain,
( ~ mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF11)
| spl16_137
| spl16_138 ),
inference(unit_resulting_resolution,[],[f176,f4669,f4665]) ).
fof(f17378,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sK5(sF15))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f268,f555,f1585]) ).
fof(f17381,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sK4(sK5(sF15)))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f268,f241,f1585]) ).
fof(f17389,plain,
( ~ mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sK3(sK4(sK5(sF15))))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f58,f1585]) ).
fof(f17395,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF15)
| spl16_74 ),
inference(unit_resulting_resolution,[],[f56,f243,f17378]) ).
fof(f17511,plain,
( ~ subq(s(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15))))),sK3(sK4(sK5(sF15))))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f260,f17389]) ).
fof(f17514,plain,
( ~ mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sK2(sK3(sK4(sK5(sF15)))))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f56,f1619,f17389]) ).
fof(f17520,plain,
( ~ mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),u(sK3(sK4(sK5(sF15))),sK3(sK4(sK5(sF15)))))
| spl16_74 ),
inference(unit_resulting_resolution,[],[f63,f17389,f17389]) ).
fof(f17609,plain,
( mem(sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15)))),sF14)
| spl16_74
| spl16_137
| spl16_138 ),
inference(unit_resulting_resolution,[],[f177,f17263,f17395]) ).
fof(f17637,plain,
( ~ subq(sF14,sK3(sK4(sK5(sF15))))
| spl16_74
| spl16_137
| spl16_138 ),
inference(unit_resulting_resolution,[],[f56,f17389,f17609]) ).
fof(f17647,plain,
( sF13 = sK0(sK4(sK5(sF15)),sK3(sK4(sK5(sF15))))
| spl16_74
| spl16_137
| spl16_138 ),
inference(resolution,[],[f17609,f123]) ).
fof(f17685,plain,
( mem(sF13,sK5(sF15))
| spl16_74
| spl16_137
| spl16_138 ),
inference(backward_demodulation,[],[f17378,f17647]) ).
fof(f17688,plain,
( mem(sF13,sK4(sK5(sF15)))
| spl16_74
| spl16_137
| spl16_138 ),
inference(backward_demodulation,[],[f17381,f17647]) ).
fof(f17799,plain,
( ~ subq(sF10,sK3(sK4(sK5(sF15))))
| spl16_42
| ~ spl16_73 ),
inference(unit_resulting_resolution,[],[f56,f115,f16781]) ).
fof(f17827,plain,
( ~ subq(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF6)
| ~ spl16_37
| ~ spl16_238 ),
inference(unit_resulting_resolution,[],[f884,f16876]) ).
fof(f17828,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sK3(sK4(sK5(sF15))))
| ~ spl16_37
| ~ spl16_238 ),
inference(unit_resulting_resolution,[],[f268,f1619,f16876]) ).
fof(f17831,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sK2(sK3(sK4(sK5(sF15)))))
| ~ spl16_37
| ~ spl16_238 ),
inference(unit_resulting_resolution,[],[f268,f241,f16876]) ).
fof(f17836,plain,
( subq(s(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6))),sK3(sK4(sK5(sF15))))
| ~ spl16_37
| ~ spl16_238 ),
inference(unit_resulting_resolution,[],[f600,f17828]) ).
fof(f17837,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sK4(sK5(sF15)))
| ~ spl16_37
| ~ spl16_238 ),
inference(unit_resulting_resolution,[],[f56,f1579,f17828]) ).
fof(f17846,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sK5(sF15))
| ~ spl16_37
| ~ spl16_238 ),
inference(unit_resulting_resolution,[],[f56,f555,f17837]) ).
fof(f17854,plain,
( subq(s(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6))),sK5(sF15))
| ~ spl16_37
| ~ spl16_238 ),
inference(unit_resulting_resolution,[],[f600,f17846]) ).
fof(f17855,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF15)
| ~ spl16_37
| ~ spl16_238 ),
inference(unit_resulting_resolution,[],[f56,f243,f17846]) ).
fof(f17871,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF14)
| mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF11)
| ~ spl16_37
| ~ spl16_238 ),
inference(resolution,[],[f17855,f177]) ).
fof(f17874,definition,
( spl16_240
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF11) ),
introduced(definition,[new_symbols(definition,[spl16_240])],[avatar_definition]) ).
fof(f17876,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF11)
| ~ spl16_240 ),
inference(avatar_component_clause,[],[f17874]) ).
fof(f17878,definition,
( spl16_241
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF14) ),
introduced(definition,[new_symbols(definition,[spl16_241])],[avatar_definition]) ).
fof(f17880,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF14)
| ~ spl16_241 ),
inference(avatar_component_clause,[],[f17878]) ).
fof(f17881,plain,
( spl16_240
| spl16_241
| ~ spl16_37
| ~ spl16_238 ),
inference(avatar_split_clause,[],[f17871,f16797,f518,f17878,f17874]) ).
fof(f17891,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF10)
| mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF9)
| ~ spl16_240 ),
inference(resolution,[],[f17876,f176]) ).
fof(f17894,definition,
( spl16_242
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF9) ),
introduced(definition,[new_symbols(definition,[spl16_242])],[avatar_definition]) ).
fof(f17896,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF9)
| ~ spl16_242 ),
inference(avatar_component_clause,[],[f17894]) ).
fof(f17898,definition,
( spl16_243
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF10) ),
introduced(definition,[new_symbols(definition,[spl16_243])],[avatar_definition]) ).
fof(f17900,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF10)
| ~ spl16_243 ),
inference(avatar_component_clause,[],[f17898]) ).
fof(f17901,plain,
( spl16_242
| spl16_243
| ~ spl16_240 ),
inference(avatar_split_clause,[],[f17891,f17874,f17898,f17894]) ).
fof(f17917,plain,
( sF13 = sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6))
| ~ spl16_241 ),
inference(resolution,[],[f17880,f123]) ).
fof(f17925,plain,
( subq(s(sF13),sK3(sK4(sK5(sF15))))
| ~ spl16_37
| ~ spl16_238
| ~ spl16_241 ),
inference(backward_demodulation,[],[f17836,f17917]) ).
fof(f17926,plain,
( mem(sF13,sK4(sK5(sF15)))
| ~ spl16_37
| ~ spl16_238
| ~ spl16_241 ),
inference(backward_demodulation,[],[f17837,f17917]) ).
fof(f17935,plain,
( subq(s(sF13),sK5(sF15))
| ~ spl16_37
| ~ spl16_238
| ~ spl16_241 ),
inference(backward_demodulation,[],[f17854,f17917]) ).
fof(f17962,plain,
( subq(sF14,sK5(sF15))
| ~ spl16_37
| ~ spl16_238
| ~ spl16_241 ),
inference(forward_demodulation,[],[f17935,f108]) ).
fof(f17964,plain,
( subq(sF14,sK3(sK4(sK5(sF15))))
| ~ spl16_37
| ~ spl16_238
| ~ spl16_241 ),
inference(forward_demodulation,[],[f17925,f108]) ).
fof(f17970,plain,
( $false
| ~ spl16_37
| spl16_74
| spl16_137
| spl16_138
| ~ spl16_238
| ~ spl16_241 ),
inference(forward_subsumption_resolution,[],[f17964,f17637]) ).
fof(f17971,plain,
( ~ spl16_37
| spl16_74
| spl16_137
| spl16_138
| ~ spl16_238
| ~ spl16_241 ),
inference(avatar_contradiction_clause,[],[f17970]) ).
fof(f17987,plain,
( sF9 = sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6))
| ~ spl16_243 ),
inference(resolution,[],[f17900,f122]) ).
fof(f17993,plain,
( mem(sF9,sK2(sK3(sK4(sK5(sF15)))))
| ~ spl16_37
| ~ spl16_238
| ~ spl16_243 ),
inference(backward_demodulation,[],[f17831,f17987]) ).
fof(f17995,plain,
( subq(s(sF9),sK3(sK4(sK5(sF15))))
| ~ spl16_37
| ~ spl16_238
| ~ spl16_243 ),
inference(backward_demodulation,[],[f17836,f17987]) ).
fof(f18037,plain,
( subq(sF10,sK3(sK4(sK5(sF15))))
| ~ spl16_37
| ~ spl16_238
| ~ spl16_243 ),
inference(forward_demodulation,[],[f17995,f100]) ).
fof(f18045,plain,
( $false
| ~ spl16_37
| spl16_42
| ~ spl16_73
| ~ spl16_238
| ~ spl16_243 ),
inference(forward_subsumption_resolution,[],[f18037,f17799]) ).
fof(f18046,plain,
( ~ spl16_37
| spl16_42
| ~ spl16_73
| ~ spl16_238
| ~ spl16_243 ),
inference(avatar_contradiction_clause,[],[f18045]) ).
fof(f18056,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF6)
| mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF8)
| ~ spl16_37
| ~ spl16_242 ),
inference(resolution,[],[f17896,f626]) ).
fof(f18060,definition,
( spl16_244
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF8) ),
introduced(definition,[new_symbols(definition,[spl16_244])],[avatar_definition]) ).
fof(f18062,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF8)
| ~ spl16_244 ),
inference(avatar_component_clause,[],[f18060]) ).
fof(f18064,definition,
( spl16_245
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF6) ),
introduced(definition,[new_symbols(definition,[spl16_245])],[avatar_definition]) ).
fof(f18066,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6)),sF6)
| ~ spl16_245 ),
inference(avatar_component_clause,[],[f18064]) ).
fof(f18067,plain,
( spl16_244
| spl16_245
| ~ spl16_37
| ~ spl16_242 ),
inference(avatar_split_clause,[],[f18056,f17894,f518,f18064,f18060]) ).
fof(f18100,plain,
( sF6 = sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6))
| ~ spl16_37
| ~ spl16_244 ),
inference(resolution,[],[f18062,f615]) ).
fof(f18104,plain,
( ~ subq(sF6,sF6)
| ~ spl16_37
| ~ spl16_238
| ~ spl16_244 ),
inference(backward_demodulation,[],[f17827,f18100]) ).
fof(f18163,plain,
( $false
| ~ spl16_37
| ~ spl16_238
| ~ spl16_244 ),
inference(forward_subsumption_resolution,[],[f18104,f241]) ).
fof(f18164,plain,
( ~ spl16_37
| ~ spl16_238
| ~ spl16_244 ),
inference(avatar_contradiction_clause,[],[f18163]) ).
fof(f18211,plain,
( e = sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF6))
| ~ spl16_245 ),
inference(resolution,[],[f18066,f119]) ).
fof(f18213,plain,
( ~ subq(e,sF6)
| ~ spl16_37
| ~ spl16_238
| ~ spl16_245 ),
inference(backward_demodulation,[],[f17827,f18211]) ).
fof(f18282,plain,
( $false
| ~ spl16_37
| ~ spl16_238
| ~ spl16_245 ),
inference(forward_subsumption_resolution,[],[f18213,f219]) ).
fof(f18283,plain,
( ~ spl16_37
| ~ spl16_238
| ~ spl16_245 ),
inference(avatar_contradiction_clause,[],[f18282]) ).
fof(f18354,definition,
( spl16_247
<=> mem(sF6,sK2(sK3(sK4(sK5(sF15))))) ),
introduced(definition,[new_symbols(definition,[spl16_247])],[avatar_definition]) ).
fof(f18355,plain,
( ~ mem(sF6,sK2(sK3(sK4(sK5(sF15)))))
| spl16_247 ),
inference(avatar_component_clause,[],[f18354]) ).
fof(f18384,plain,
( ~ mem(sF13,sK4(sK5(sF15)))
| spl16_42
| ~ spl16_45 ),
inference(forward_demodulation,[],[f13291,f1555]) ).
fof(f18441,plain,
( $false
| spl16_42
| ~ spl16_45
| spl16_74
| spl16_137
| spl16_138 ),
inference(forward_subsumption_resolution,[],[f18384,f17688]) ).
fof(f18442,plain,
( spl16_42
| ~ spl16_45
| spl16_74
| spl16_137
| spl16_138 ),
inference(avatar_contradiction_clause,[],[f18441]) ).
fof(f18454,plain,
( $false
| spl16_74
| ~ spl16_85
| ~ spl16_138 ),
inference(forward_subsumption_resolution,[],[f7137,f17119]) ).
fof(f18455,plain,
( spl16_74
| ~ spl16_85
| ~ spl16_138 ),
inference(avatar_contradiction_clause,[],[f18454]) ).
fof(f19154,plain,
( ~ subq(s(sF9),sK3(sK4(sK5(sF15))))
| spl16_74
| ~ spl16_138 ),
inference(forward_demodulation,[],[f17511,f4685]) ).
fof(f19260,plain,
( ~ subq(sF10,sK3(sK4(sK5(sF15))))
| spl16_74
| ~ spl16_138 ),
inference(forward_demodulation,[],[f19154,f100]) ).
fof(f19294,plain,
( $false
| ~ spl16_37
| spl16_74
| ~ spl16_138
| ~ spl16_238
| ~ spl16_243 ),
inference(forward_subsumption_resolution,[],[f19260,f18037]) ).
fof(f19295,plain,
( ~ spl16_37
| spl16_74
| ~ spl16_138
| ~ spl16_238
| ~ spl16_243 ),
inference(avatar_contradiction_clause,[],[f19294]) ).
fof(f19315,plain,
( $false
| ~ spl16_37
| spl16_42
| ~ spl16_45
| ~ spl16_238
| ~ spl16_241 ),
inference(forward_subsumption_resolution,[],[f17926,f1576]) ).
fof(f19316,plain,
( ~ spl16_37
| spl16_42
| ~ spl16_45
| ~ spl16_238
| ~ spl16_241 ),
inference(avatar_contradiction_clause,[],[f19315]) ).
fof(f19401,plain,
( ~ mem(sF6,sK2(sK3(sK4(sK5(sF15)))))
| ~ spl16_37
| spl16_74
| ~ spl16_195 ),
inference(forward_demodulation,[],[f17514,f8089]) ).
fof(f20223,plain,
( ~ subq(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF9)
| ~ spl16_85 ),
inference(unit_resulting_resolution,[],[f884,f17118]) ).
fof(f20224,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sK3(sK4(sK5(sF15))))
| ~ spl16_85 ),
inference(unit_resulting_resolution,[],[f268,f1619,f17118]) ).
fof(f20311,plain,
( subq(s(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9))),sK3(sK4(sK5(sF15))))
| ~ spl16_85 ),
inference(unit_resulting_resolution,[],[f600,f20224]) ).
fof(f20312,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sK4(sK5(sF15)))
| ~ spl16_85 ),
inference(unit_resulting_resolution,[],[f56,f1579,f20224]) ).
fof(f20320,plain,
( subq(s(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9))),sK4(sK5(sF15)))
| ~ spl16_85 ),
inference(unit_resulting_resolution,[],[f600,f20312]) ).
fof(f20321,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sK5(sF15))
| ~ spl16_85 ),
inference(unit_resulting_resolution,[],[f56,f555,f20312]) ).
fof(f20331,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF15)
| ~ spl16_85 ),
inference(unit_resulting_resolution,[],[f56,f243,f20321]) ).
fof(f20347,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF14)
| mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF11)
| ~ spl16_85 ),
inference(resolution,[],[f20331,f177]) ).
fof(f20350,definition,
( spl16_263
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF11) ),
introduced(definition,[new_symbols(definition,[spl16_263])],[avatar_definition]) ).
fof(f20352,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF11)
| ~ spl16_263 ),
inference(avatar_component_clause,[],[f20350]) ).
fof(f20354,definition,
( spl16_264
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF14) ),
introduced(definition,[new_symbols(definition,[spl16_264])],[avatar_definition]) ).
fof(f20356,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF14)
| ~ spl16_264 ),
inference(avatar_component_clause,[],[f20354]) ).
fof(f20357,plain,
( spl16_263
| spl16_264
| ~ spl16_85 ),
inference(avatar_split_clause,[],[f20347,f1888,f20354,f20350]) ).
fof(f20372,plain,
( sF13 = sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9))
| ~ spl16_264 ),
inference(resolution,[],[f20356,f123]) ).
fof(f20385,plain,
( subq(s(sF13),sK4(sK5(sF15)))
| ~ spl16_85
| ~ spl16_264 ),
inference(backward_demodulation,[],[f20320,f20372]) ).
fof(f20417,plain,
( subq(sF14,sK4(sK5(sF15)))
| ~ spl16_85
| ~ spl16_264 ),
inference(forward_demodulation,[],[f20385,f108]) ).
fof(f20424,plain,
( $false
| spl16_42
| ~ spl16_45
| ~ spl16_85
| ~ spl16_264 ),
inference(forward_subsumption_resolution,[],[f20417,f1604]) ).
fof(f20425,plain,
( spl16_42
| ~ spl16_45
| ~ spl16_85
| ~ spl16_264 ),
inference(avatar_contradiction_clause,[],[f20424]) ).
fof(f20435,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF10)
| mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF9)
| ~ spl16_263 ),
inference(resolution,[],[f20352,f176]) ).
fof(f20438,definition,
( spl16_265
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF9) ),
introduced(definition,[new_symbols(definition,[spl16_265])],[avatar_definition]) ).
fof(f20440,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF9)
| ~ spl16_265 ),
inference(avatar_component_clause,[],[f20438]) ).
fof(f20442,definition,
( spl16_266
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF10) ),
introduced(definition,[new_symbols(definition,[spl16_266])],[avatar_definition]) ).
fof(f20444,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF10)
| ~ spl16_266 ),
inference(avatar_component_clause,[],[f20442]) ).
fof(f20445,plain,
( spl16_265
| spl16_266
| ~ spl16_263 ),
inference(avatar_split_clause,[],[f20435,f20350,f20442,f20438]) ).
fof(f20455,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF6)
| mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF8)
| ~ spl16_37
| ~ spl16_265 ),
inference(resolution,[],[f20440,f626]) ).
fof(f20459,definition,
( spl16_267
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF8) ),
introduced(definition,[new_symbols(definition,[spl16_267])],[avatar_definition]) ).
fof(f20461,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF8)
| ~ spl16_267 ),
inference(avatar_component_clause,[],[f20459]) ).
fof(f20463,definition,
( spl16_268
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF6) ),
introduced(definition,[new_symbols(definition,[spl16_268])],[avatar_definition]) ).
fof(f20465,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9)),sF6)
| ~ spl16_268 ),
inference(avatar_component_clause,[],[f20463]) ).
fof(f20466,plain,
( spl16_267
| spl16_268
| ~ spl16_37
| ~ spl16_265 ),
inference(avatar_split_clause,[],[f20455,f20438,f518,f20463,f20459]) ).
fof(f20480,plain,
( e = sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9))
| ~ spl16_268 ),
inference(resolution,[],[f20465,f119]) ).
fof(f20482,plain,
( ~ subq(e,sF9)
| ~ spl16_85
| ~ spl16_268 ),
inference(backward_demodulation,[],[f20223,f20480]) ).
fof(f20552,plain,
( $false
| ~ spl16_85
| ~ spl16_268 ),
inference(forward_subsumption_resolution,[],[f20482,f219]) ).
fof(f20553,plain,
( ~ spl16_85
| ~ spl16_268 ),
inference(avatar_contradiction_clause,[],[f20552]) ).
fof(f20580,plain,
( sF9 = sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9))
| ~ spl16_266 ),
inference(resolution,[],[f20444,f122]) ).
fof(f20582,plain,
( ~ subq(sF9,sF9)
| ~ spl16_85
| ~ spl16_266 ),
inference(backward_demodulation,[],[f20223,f20580]) ).
fof(f20643,plain,
( $false
| ~ spl16_85
| ~ spl16_266 ),
inference(forward_subsumption_resolution,[],[f20582,f241]) ).
fof(f20644,plain,
( ~ spl16_85
| ~ spl16_266 ),
inference(avatar_contradiction_clause,[],[f20643]) ).
fof(f20681,plain,
( sF6 = sK0(sK2(sK3(sK4(sK5(sF15)))),p(sF9))
| ~ spl16_37
| ~ spl16_267 ),
inference(resolution,[],[f20461,f615]) ).
fof(f20685,plain,
( ~ subq(sF6,sF9)
| ~ spl16_37
| ~ spl16_85
| ~ spl16_267 ),
inference(backward_demodulation,[],[f20223,f20681]) ).
fof(f20749,plain,
( $false
| ~ spl16_37
| ~ spl16_85
| ~ spl16_267 ),
inference(forward_subsumption_resolution,[],[f20685,f503]) ).
fof(f20750,plain,
( ~ spl16_37
| ~ spl16_85
| ~ spl16_267 ),
inference(avatar_contradiction_clause,[],[f20749]) ).
fof(f20786,plain,
( subq(s(sF13),sK3(sK4(sK5(sF15))))
| ~ spl16_85
| ~ spl16_264 ),
inference(forward_demodulation,[],[f20311,f20372]) ).
fof(f20792,plain,
( mem(sF13,sK5(sF15))
| ~ spl16_85
| ~ spl16_264 ),
inference(forward_demodulation,[],[f20321,f20372]) ).
fof(f20888,plain,
( subq(sF14,sK3(sK4(sK5(sF15))))
| ~ spl16_85
| ~ spl16_264 ),
inference(forward_demodulation,[],[f20786,f108]) ).
fof(f20906,plain,
( $false
| spl16_74
| ~ spl16_85
| spl16_137
| spl16_138
| ~ spl16_264 ),
inference(forward_subsumption_resolution,[],[f20888,f17637]) ).
fof(f20907,plain,
( spl16_74
| ~ spl16_85
| spl16_137
| spl16_138
| ~ spl16_264 ),
inference(avatar_contradiction_clause,[],[f20906]) ).
fof(f20970,plain,
( subq(s(sF6),sK4(sK5(sF15)))
| ~ spl16_37
| ~ spl16_238 ),
inference(forward_demodulation,[],[f1840,f16871]) ).
fof(f21021,plain,
( subq(sF8,sK4(sK5(sF15)))
| ~ spl16_37
| ~ spl16_238 ),
inference(forward_demodulation,[],[f20970,f612]) ).
fof(f21032,plain,
( $false
| ~ spl16_37
| spl16_42
| ~ spl16_131
| ~ spl16_238 ),
inference(forward_subsumption_resolution,[],[f21021,f7099]) ).
fof(f21033,plain,
( ~ spl16_37
| spl16_42
| ~ spl16_131
| ~ spl16_238 ),
inference(avatar_contradiction_clause,[],[f21032]) ).
fof(f21119,plain,
( ~ mem(sF13,sK5(sF15))
| spl16_1
| ~ spl16_61 ),
inference(forward_demodulation,[],[f13465,f1127]) ).
fof(f21143,plain,
( $false
| spl16_1
| ~ spl16_61
| spl16_74
| spl16_137
| spl16_138 ),
inference(forward_subsumption_resolution,[],[f21119,f17685]) ).
fof(f21144,plain,
( spl16_1
| ~ spl16_61
| spl16_74
| spl16_137
| spl16_138 ),
inference(avatar_contradiction_clause,[],[f21143]) ).
fof(f21250,definition,
( spl16_272
<=> mem(sF9,sK2(sK3(sK4(sK5(sF15))))) ),
introduced(definition,[new_symbols(definition,[spl16_272])],[avatar_definition]) ).
fof(f21251,plain,
( ~ mem(sF9,sK2(sK3(sK4(sK5(sF15)))))
| spl16_272 ),
inference(avatar_component_clause,[],[f21250]) ).
fof(f21252,plain,
( mem(sF9,sK2(sK3(sK4(sK5(sF15)))))
| ~ spl16_272 ),
inference(avatar_component_clause,[],[f21250]) ).
fof(f21283,plain,
( mem(sF9,sK3(sK4(sK5(sF15))))
| ~ spl16_272 ),
inference(unit_resulting_resolution,[],[f56,f1619,f21252]) ).
fof(f21292,plain,
( $false
| spl16_1
| ~ spl16_63
| ~ spl16_272 ),
inference(forward_subsumption_resolution,[],[f21283,f1754]) ).
fof(f21293,plain,
( spl16_1
| ~ spl16_63
| ~ spl16_272 ),
inference(avatar_contradiction_clause,[],[f21292]) ).
fof(f22039,plain,
( ~ subq(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),e)
| ~ spl16_239 ),
inference(unit_resulting_resolution,[],[f884,f17023]) ).
fof(f22040,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sK3(sK4(sK5(sF15))))
| ~ spl16_239 ),
inference(unit_resulting_resolution,[],[f268,f1619,f17023]) ).
fof(f22043,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sK2(sK3(sK4(sK5(sF15)))))
| ~ spl16_239 ),
inference(unit_resulting_resolution,[],[f268,f241,f17023]) ).
fof(f22498,plain,
( subq(s(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e))),sK3(sK4(sK5(sF15))))
| ~ spl16_239 ),
inference(unit_resulting_resolution,[],[f600,f22040]) ).
fof(f22499,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sK4(sK5(sF15)))
| ~ spl16_239 ),
inference(unit_resulting_resolution,[],[f56,f1579,f22040]) ).
fof(f22500,plain,
( ! [X0] : mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),u(X0,sK3(sK4(sK5(sF15)))))
| ~ spl16_239 ),
inference(unit_resulting_resolution,[],[f56,f554,f22040]) ).
fof(f22508,plain,
( subq(s(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e))),sK4(sK5(sF15)))
| ~ spl16_239 ),
inference(unit_resulting_resolution,[],[f600,f22499]) ).
fof(f22509,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sK5(sF15))
| ~ spl16_239 ),
inference(unit_resulting_resolution,[],[f56,f555,f22499]) ).
fof(f22518,plain,
( subq(s(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e))),sK5(sF15))
| ~ spl16_239 ),
inference(unit_resulting_resolution,[],[f600,f22509]) ).
fof(f22519,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF15)
| ~ spl16_239 ),
inference(unit_resulting_resolution,[],[f56,f243,f22509]) ).
fof(f22537,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF14)
| mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF11)
| ~ spl16_239 ),
inference(resolution,[],[f22519,f177]) ).
fof(f22540,definition,
( spl16_278
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF11) ),
introduced(definition,[new_symbols(definition,[spl16_278])],[avatar_definition]) ).
fof(f22542,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF11)
| ~ spl16_278 ),
inference(avatar_component_clause,[],[f22540]) ).
fof(f22544,definition,
( spl16_279
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF14) ),
introduced(definition,[new_symbols(definition,[spl16_279])],[avatar_definition]) ).
fof(f22546,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF14)
| ~ spl16_279 ),
inference(avatar_component_clause,[],[f22544]) ).
fof(f22547,plain,
( spl16_278
| spl16_279
| ~ spl16_239 ),
inference(avatar_split_clause,[],[f22537,f16801,f22544,f22540]) ).
fof(f22564,plain,
( sF13 = sK0(sK2(sK3(sK4(sK5(sF15)))),p(e))
| ~ spl16_279 ),
inference(resolution,[],[f22546,f123]) ).
fof(f22567,plain,
( mem(sF13,sK3(sK4(sK5(sF15))))
| ~ spl16_239
| ~ spl16_279 ),
inference(backward_demodulation,[],[f22040,f22564]) ).
fof(f22579,plain,
( subq(s(sF13),sK3(sK4(sK5(sF15))))
| ~ spl16_239
| ~ spl16_279 ),
inference(backward_demodulation,[],[f22498,f22564]) ).
fof(f22589,plain,
( subq(s(sF13),sK5(sF15))
| ~ spl16_239
| ~ spl16_279 ),
inference(backward_demodulation,[],[f22518,f22564]) ).
fof(f22615,plain,
( subq(sF14,sK5(sF15))
| ~ spl16_239
| ~ spl16_279 ),
inference(forward_demodulation,[],[f22589,f108]) ).
fof(f22617,plain,
( subq(sF14,sK3(sK4(sK5(sF15))))
| ~ spl16_239
| ~ spl16_279 ),
inference(forward_demodulation,[],[f22579,f108]) ).
fof(f22624,plain,
( $false
| spl16_74
| spl16_137
| spl16_138
| ~ spl16_239
| ~ spl16_279 ),
inference(forward_subsumption_resolution,[],[f22617,f17637]) ).
fof(f22625,plain,
( spl16_74
| spl16_137
| spl16_138
| ~ spl16_239
| ~ spl16_279 ),
inference(avatar_contradiction_clause,[],[f22624]) ).
fof(f22635,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF10)
| mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF9)
| ~ spl16_278 ),
inference(resolution,[],[f22542,f176]) ).
fof(f22638,definition,
( spl16_280
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF9) ),
introduced(definition,[new_symbols(definition,[spl16_280])],[avatar_definition]) ).
fof(f22640,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF9)
| ~ spl16_280 ),
inference(avatar_component_clause,[],[f22638]) ).
fof(f22642,definition,
( spl16_281
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF10) ),
introduced(definition,[new_symbols(definition,[spl16_281])],[avatar_definition]) ).
fof(f22644,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF10)
| ~ spl16_281 ),
inference(avatar_component_clause,[],[f22642]) ).
fof(f22645,plain,
( spl16_280
| spl16_281
| ~ spl16_278 ),
inference(avatar_split_clause,[],[f22635,f22540,f22642,f22638]) ).
fof(f22660,plain,
( sF9 = sK0(sK2(sK3(sK4(sK5(sF15)))),p(e))
| ~ spl16_281 ),
inference(resolution,[],[f22644,f122]) ).
fof(f22666,plain,
( mem(sF9,sK2(sK3(sK4(sK5(sF15)))))
| ~ spl16_239
| ~ spl16_281 ),
inference(backward_demodulation,[],[f22043,f22660]) ).
fof(f22677,plain,
( ! [X0] : mem(sF9,u(X0,sK3(sK4(sK5(sF15)))))
| ~ spl16_239
| ~ spl16_281 ),
inference(backward_demodulation,[],[f22500,f22660]) ).
fof(f22680,plain,
( subq(s(sF9),sK4(sK5(sF15)))
| ~ spl16_239
| ~ spl16_281 ),
inference(backward_demodulation,[],[f22508,f22660]) ).
fof(f22720,plain,
( subq(sF10,sK4(sK5(sF15)))
| ~ spl16_239
| ~ spl16_281 ),
inference(forward_demodulation,[],[f22680,f100]) ).
fof(f22725,plain,
( $false
| ~ spl16_239
| spl16_272
| ~ spl16_281 ),
inference(forward_subsumption_resolution,[],[f22666,f21251]) ).
fof(f22726,plain,
( ~ spl16_239
| spl16_272
| ~ spl16_281 ),
inference(avatar_contradiction_clause,[],[f22725]) ).
fof(f22732,plain,
( $false
| spl16_1
| ~ spl16_63
| ~ spl16_239
| ~ spl16_281 ),
inference(forward_subsumption_resolution,[],[f22720,f1747]) ).
fof(f22733,plain,
( spl16_1
| ~ spl16_63
| ~ spl16_239
| ~ spl16_281 ),
inference(avatar_contradiction_clause,[],[f22732]) ).
fof(f22743,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF6)
| mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF8)
| ~ spl16_37
| ~ spl16_280 ),
inference(resolution,[],[f22640,f626]) ).
fof(f22747,definition,
( spl16_282
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF8) ),
introduced(definition,[new_symbols(definition,[spl16_282])],[avatar_definition]) ).
fof(f22749,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF8)
| ~ spl16_282 ),
inference(avatar_component_clause,[],[f22747]) ).
fof(f22751,definition,
( spl16_283
<=> mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF6) ),
introduced(definition,[new_symbols(definition,[spl16_283])],[avatar_definition]) ).
fof(f22753,plain,
( mem(sK0(sK2(sK3(sK4(sK5(sF15)))),p(e)),sF6)
| ~ spl16_283 ),
inference(avatar_component_clause,[],[f22751]) ).
fof(f22754,plain,
( spl16_282
| spl16_283
| ~ spl16_37
| ~ spl16_280 ),
inference(avatar_split_clause,[],[f22743,f22638,f518,f22751,f22747]) ).
fof(f22777,plain,
( sF6 = sK0(sK2(sK3(sK4(sK5(sF15)))),p(e))
| ~ spl16_37
| ~ spl16_282 ),
inference(resolution,[],[f22749,f615]) ).
fof(f22785,plain,
( mem(sF6,sK2(sK3(sK4(sK5(sF15)))))
| ~ spl16_37
| ~ spl16_239
| ~ spl16_282 ),
inference(backward_demodulation,[],[f22043,f22777]) ).
fof(f22799,plain,
( subq(s(sF6),sK4(sK5(sF15)))
| ~ spl16_37
| ~ spl16_239
| ~ spl16_282 ),
inference(backward_demodulation,[],[f22508,f22777]) ).
fof(f22842,plain,
( subq(sF8,sK4(sK5(sF15)))
| ~ spl16_37
| ~ spl16_239
| ~ spl16_282 ),
inference(forward_demodulation,[],[f22799,f612]) ).
fof(f22847,plain,
( $false
| ~ spl16_37
| ~ spl16_239
| spl16_247
| ~ spl16_282 ),
inference(forward_subsumption_resolution,[],[f22785,f18355]) ).
fof(f22848,plain,
( ~ spl16_37
| ~ spl16_239
| spl16_247
| ~ spl16_282 ),
inference(avatar_contradiction_clause,[],[f22847]) ).
fof(f22852,plain,
( $false
| ~ spl16_37
| spl16_42
| ~ spl16_131
| ~ spl16_239
| ~ spl16_282 ),
inference(forward_subsumption_resolution,[],[f22842,f7099]) ).
fof(f22853,plain,
( ~ spl16_37
| spl16_42
| ~ spl16_131
| ~ spl16_239
| ~ spl16_282 ),
inference(avatar_contradiction_clause,[],[f22852]) ).
fof(f22895,plain,
( e = sK0(sK2(sK3(sK4(sK5(sF15)))),p(e))
| ~ spl16_283 ),
inference(resolution,[],[f22753,f119]) ).
fof(f22897,plain,
( ~ subq(e,e)
| ~ spl16_239
| ~ spl16_283 ),
inference(backward_demodulation,[],[f22039,f22895]) ).
fof(f22979,plain,
( $false
| ~ spl16_239
| ~ spl16_283 ),
inference(forward_subsumption_resolution,[],[f22897,f219]) ).
fof(f22980,plain,
( ~ spl16_239
| ~ spl16_283 ),
inference(avatar_contradiction_clause,[],[f22979]) ).
fof(f23025,plain,
( subq(s(sF9),sK4(sK5(sF15)))
| ~ spl16_239
| ~ spl16_281 ),
inference(forward_demodulation,[],[f22508,f22660]) ).
fof(f23106,plain,
( subq(sF10,sK4(sK5(sF15)))
| ~ spl16_239
| ~ spl16_281 ),
inference(forward_demodulation,[],[f23025,f100]) ).
fof(f23112,plain,
( $false
| spl16_42
| ~ spl16_73
| ~ spl16_239
| ~ spl16_281 ),
inference(forward_subsumption_resolution,[],[f23106,f6221]) ).
fof(f23113,plain,
( spl16_42
| ~ spl16_73
| ~ spl16_239
| ~ spl16_281 ),
inference(avatar_contradiction_clause,[],[f23112]) ).
fof(f23143,plain,
( mem(sF6,sK5(sF15))
| ~ spl16_37
| ~ spl16_239
| ~ spl16_282 ),
inference(forward_demodulation,[],[f22509,f22777]) ).
fof(f23168,plain,
( $false
| spl16_1
| ~ spl16_37
| ~ spl16_80
| ~ spl16_239
| ~ spl16_282 ),
inference(forward_subsumption_resolution,[],[f23143,f6372]) ).
fof(f23169,plain,
( spl16_1
| ~ spl16_37
| ~ spl16_80
| ~ spl16_239
| ~ spl16_282 ),
inference(avatar_contradiction_clause,[],[f23168]) ).
fof(f23180,plain,
( ~ spl16_170
| spl16_42
| ~ spl16_132 ),
inference(avatar_split_clause,[],[f4364,f4248,f559,f6828]) ).
fof(f23181,plain,
( spl16_272
| ~ spl16_37
| ~ spl16_238
| ~ spl16_243 ),
inference(avatar_split_clause,[],[f17993,f17898,f16797,f518,f21250]) ).
fof(f23209,plain,
( mem(sF6,sK5(sF15))
| ~ spl16_37
| ~ spl16_238 ),
inference(forward_demodulation,[],[f1841,f16871]) ).
fof(f23289,plain,
( $false
| spl16_1
| ~ spl16_37
| ~ spl16_80
| ~ spl16_238 ),
inference(forward_subsumption_resolution,[],[f23209,f6372]) ).
fof(f23290,plain,
( spl16_1
| ~ spl16_37
| ~ spl16_80
| ~ spl16_238 ),
inference(avatar_contradiction_clause,[],[f23289]) ).
fof(f23327,plain,
( ~ spl16_247
| ~ spl16_37
| spl16_74
| ~ spl16_195 ),
inference(avatar_split_clause,[],[f19401,f7935,f1583,f518,f18354]) ).
fof(f23427,plain,
( subq(s(sF9),sK5(sF15))
| ~ spl16_85 ),
inference(forward_demodulation,[],[f1848,f17115]) ).
fof(f23531,plain,
( subq(sF10,sK5(sF15))
| ~ spl16_85 ),
inference(forward_demodulation,[],[f23427,f100]) ).
fof(f23554,plain,
( $false
| spl16_1
| ~ spl16_63
| ~ spl16_85 ),
inference(forward_subsumption_resolution,[],[f23531,f1728]) ).
fof(f23555,plain,
( spl16_1
| ~ spl16_63
| ~ spl16_85 ),
inference(avatar_contradiction_clause,[],[f23554]) ).
fof(f23595,plain,
( ~ mem(sF13,sK5(sF15))
| spl16_1
| ~ spl16_61 ),
inference(forward_demodulation,[],[f13465,f1127]) ).
fof(f23602,plain,
( $false
| spl16_1
| ~ spl16_61
| ~ spl16_85
| ~ spl16_264 ),
inference(forward_subsumption_resolution,[],[f23595,f20792]) ).
fof(f23603,plain,
( spl16_1
| ~ spl16_61
| ~ spl16_85
| ~ spl16_264 ),
inference(avatar_contradiction_clause,[],[f23602]) ).
fof(f23691,plain,
( ~ subq(s(e),sK3(sK4(sK5(sF15))))
| spl16_74
| ~ spl16_196 ),
inference(forward_demodulation,[],[f17511,f8000]) ).
fof(f23811,plain,
( ~ subq(sF6,sK3(sK4(sK5(sF15))))
| spl16_74
| ~ spl16_196 ),
inference(forward_demodulation,[],[f23691,f92]) ).
fof(f23838,plain,
( $false
| spl16_74
| ~ spl16_196
| ~ spl16_239 ),
inference(forward_subsumption_resolution,[],[f23811,f17091]) ).
fof(f23839,plain,
( spl16_74
| ~ spl16_196
| ~ spl16_239 ),
inference(avatar_contradiction_clause,[],[f23838]) ).
fof(f23860,plain,
( $false
| spl16_42
| ~ spl16_45
| ~ spl16_239
| ~ spl16_279 ),
inference(forward_subsumption_resolution,[],[f22567,f1611]) ).
fof(f23861,plain,
( spl16_42
| ~ spl16_45
| ~ spl16_239
| ~ spl16_279 ),
inference(avatar_contradiction_clause,[],[f23860]) ).
fof(f23986,plain,
( $false
| spl16_1
| ~ spl16_61
| ~ spl16_239
| ~ spl16_279 ),
inference(forward_subsumption_resolution,[],[f22615,f1145]) ).
fof(f23987,plain,
( spl16_1
| ~ spl16_61
| ~ spl16_239
| ~ spl16_279 ),
inference(avatar_contradiction_clause,[],[f23986]) ).
fof(f24045,plain,
( ~ mem(sF9,sK2(sK3(sK4(sK5(sF15)))))
| spl16_74
| ~ spl16_138 ),
inference(forward_demodulation,[],[f17514,f4685]) ).
fof(f24046,plain,
( ~ mem(sF9,u(sK3(sK4(sK5(sF15))),sK3(sK4(sK5(sF15)))))
| spl16_74
| ~ spl16_138 ),
inference(forward_demodulation,[],[f17520,f4685]) ).
fof(f24098,plain,
( $false
| spl16_74
| ~ spl16_138
| ~ spl16_272 ),
inference(forward_subsumption_resolution,[],[f24045,f21252]) ).
fof(f24099,plain,
( spl16_74
| ~ spl16_138
| ~ spl16_272 ),
inference(avatar_contradiction_clause,[],[f24098]) ).
fof(f24100,plain,
( $false
| spl16_74
| ~ spl16_138
| ~ spl16_239
| ~ spl16_281 ),
inference(forward_subsumption_resolution,[],[f24046,f22677]) ).
fof(f24101,plain,
( spl16_74
| ~ spl16_138
| ~ spl16_239
| ~ spl16_281 ),
inference(avatar_contradiction_clause,[],[f24100]) ).
fof(f24114,plain,
( $false
| spl16_1
| ~ spl16_37
| ~ spl16_61
| ~ spl16_238
| ~ spl16_241 ),
inference(forward_subsumption_resolution,[],[f17962,f1145]) ).
fof(f24115,plain,
( spl16_1
| ~ spl16_37
| ~ spl16_61
| ~ spl16_238
| ~ spl16_241 ),
inference(avatar_contradiction_clause,[],[f24114]) ).
cnf(s1,plain,
( ~ spl16_1
| spl16_2 ),
inference(sat_conversion,[],[f287]) ).
cnf(s21,plain,
( ~ spl16_36
| spl16_37 ),
inference(sat_conversion,[],[f521]) ).
cnf(s24,plain,
( ~ spl16_42
| spl16_43 ),
inference(sat_conversion,[],[f566]) ).
cnf(s25,plain,
( spl16_42
| spl16_44
| spl16_45 ),
inference(sat_conversion,[],[f587]) ).
cnf(s26,plain,
spl16_36,
inference(sat_conversion,[],[f610]) ).
cnf(s34,plain,
( spl16_1
| spl16_60
| spl16_61 ),
inference(sat_conversion,[],[f1073]) ).
cnf(s35,plain,
~ spl16_2,
inference(sat_conversion,[],[f1085]) ).
cnf(s36,plain,
( ~ spl16_60
| spl16_62
| spl16_63 ),
inference(sat_conversion,[],[f1118]) ).
cnf(s41,plain,
( ~ spl16_44
| spl16_72
| spl16_73 ),
inference(sat_conversion,[],[f1544]) ).
cnf(s42,plain,
( spl16_1
| spl16_42
| ~ spl16_45
| ~ spl16_61 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s43,plain,
( ~ spl16_74
| spl16_75 ),
inference(sat_conversion,[],[f1590]) ).
cnf(s46,plain,
( ~ spl16_37
| ~ spl16_62
| spl16_80
| spl16_81 ),
inference(sat_conversion,[],[f1684]) ).
cnf(s47,plain,
( spl16_82
| spl16_83 ),
inference(sat_conversion,[],[f1872]) ).
cnf(s48,plain,
( ~ spl16_82
| spl16_84
| spl16_85 ),
inference(sat_conversion,[],[f1891]) ).
cnf(s51,plain,
( spl16_42
| ~ spl16_45
| ~ spl16_83 ),
inference(sat_conversion,[],[f1954]) ).
cnf(s90,plain,
( spl16_1
| ~ spl16_61
| ~ spl16_83 ),
inference(sat_conversion,[],[f3265]) ).
cnf(s122,plain,
~ spl16_43,
inference(sat_conversion,[],[f4162]) ).
cnf(s128,plain,
( ~ spl16_37
| ~ spl16_72
| spl16_131
| spl16_132 ),
inference(sat_conversion,[],[f4251]) ).
cnf(s131,plain,
( spl16_74
| ~ spl16_83
| spl16_137
| spl16_138 ),
inference(sat_conversion,[],[f4671]) ).
cnf(s135,plain,
( spl16_1
| ~ spl16_63
| spl16_74
| ~ spl16_138 ),
inference(sat_conversion,[],[f4738]) ).
cnf(s172,plain,
( spl16_1
| spl16_42
| ~ spl16_63
| ~ spl16_73 ),
inference(sat_conversion,[],[f6079]) ).
cnf(s190,plain,
( spl16_1
| spl16_42
| ~ spl16_81
| ~ spl16_132 ),
inference(sat_conversion,[],[f6535]) ).
cnf(s199,plain,
( spl16_1
| ~ spl16_37
| spl16_42
| ~ spl16_80
| ~ spl16_131 ),
inference(sat_conversion,[],[f6667]) ).
cnf(s240,plain,
( ~ spl16_83
| spl16_189
| spl16_190 ),
inference(sat_conversion,[],[f7467]) ).
cnf(s241,plain,
( ~ spl16_189
| spl16_191
| spl16_192 ),
inference(sat_conversion,[],[f7487]) ).
cnf(s244,plain,
( spl16_74
| ~ spl16_83
| ~ spl16_138
| ~ spl16_192 ),
inference(sat_conversion,[],[f7563]) ).
cnf(s246,plain,
( ~ spl16_83
| ~ spl16_190 ),
inference(sat_conversion,[],[f7636]) ).
cnf(s247,plain,
( ~ spl16_37
| ~ spl16_191
| spl16_193
| spl16_194 ),
inference(sat_conversion,[],[f7657]) ).
cnf(s253,plain,
( ~ spl16_83
| ~ spl16_194 ),
inference(sat_conversion,[],[f7762]) ).
cnf(s258,plain,
( ~ spl16_37
| spl16_42
| ~ spl16_83
| ~ spl16_131
| ~ spl16_193 ),
inference(sat_conversion,[],[f7878]) ).
cnf(s259,plain,
( ~ spl16_37
| ~ spl16_137
| spl16_195
| spl16_196 ),
inference(sat_conversion,[],[f7942]) ).
cnf(s260,plain,
( spl16_74
| spl16_170
| ~ spl16_196 ),
inference(sat_conversion,[],[f8041]) ).
cnf(s262,plain,
( spl16_1
| spl16_74
| ~ spl16_81
| ~ spl16_196 ),
inference(sat_conversion,[],[f8045]) ).
cnf(s263,plain,
( ~ spl16_37
| spl16_42
| spl16_74
| ~ spl16_131
| ~ spl16_195 ),
inference(sat_conversion,[],[f8132]) ).
cnf(s272,plain,
( spl16_1
| ~ spl16_63
| ~ spl16_83
| ~ spl16_192 ),
inference(sat_conversion,[],[f8189]) ).
cnf(s285,plain,
( spl16_1
| ~ spl16_81
| ~ spl16_170 ),
inference(sat_conversion,[],[f8207]) ).
cnf(s287,plain,
( spl16_137
| ~ spl16_195 ),
inference(sat_conversion,[],[f8210]) ).
cnf(s288,plain,
( spl16_42
| ~ spl16_73
| ~ spl16_83
| ~ spl16_192 ),
inference(sat_conversion,[],[f8271]) ).
cnf(s294,plain,
( ~ spl16_37
| spl16_74
| ~ spl16_83
| ~ spl16_193
| ~ spl16_195 ),
inference(sat_conversion,[],[f8318]) ).
cnf(s298,plain,
( spl16_42
| ~ spl16_73
| spl16_74
| ~ spl16_138 ),
inference(sat_conversion,[],[f8344]) ).
cnf(s300,plain,
( spl16_1
| ~ spl16_37
| ~ spl16_80
| ~ spl16_83
| ~ spl16_193 ),
inference(sat_conversion,[],[f8374]) ).
cnf(s310,plain,
( spl16_42
| spl16_74
| ~ spl16_132
| ~ spl16_196 ),
inference(sat_conversion,[],[f8389]) ).
cnf(s319,plain,
( spl16_1
| ~ spl16_37
| spl16_74
| ~ spl16_80
| ~ spl16_195 ),
inference(sat_conversion,[],[f8485]) ).
cnf(s628,plain,
~ spl16_75,
inference(sat_conversion,[],[f16730]) ).
cnf(s636,plain,
( ~ spl16_37
| ~ spl16_84
| spl16_238
| spl16_239 ),
inference(sat_conversion,[],[f16804]) ).
cnf(s637,plain,
( ~ spl16_37
| spl16_74
| ~ spl16_195
| ~ spl16_238 ),
inference(sat_conversion,[],[f16939]) ).
cnf(s642,plain,
( spl16_1
| ~ spl16_81
| ~ spl16_239 ),
inference(sat_conversion,[],[f17097]) ).
cnf(s643,plain,
( spl16_170
| ~ spl16_239 ),
inference(sat_conversion,[],[f17099]) ).
cnf(s646,plain,
( spl16_42
| ~ spl16_73
| ~ spl16_85 ),
inference(sat_conversion,[],[f17181]) ).
cnf(s653,plain,
( ~ spl16_37
| ~ spl16_238
| spl16_240
| spl16_241 ),
inference(sat_conversion,[],[f17881]) ).
cnf(s654,plain,
( ~ spl16_240
| spl16_242
| spl16_243 ),
inference(sat_conversion,[],[f17901]) ).
cnf(s657,plain,
( ~ spl16_37
| spl16_74
| spl16_137
| spl16_138
| ~ spl16_238
| ~ spl16_241 ),
inference(sat_conversion,[],[f17971]) ).
cnf(s662,plain,
( ~ spl16_37
| spl16_42
| ~ spl16_73
| ~ spl16_238
| ~ spl16_243 ),
inference(sat_conversion,[],[f18046]) ).
cnf(s663,plain,
( ~ spl16_37
| ~ spl16_242
| spl16_244
| spl16_245 ),
inference(sat_conversion,[],[f18067]) ).
cnf(s665,plain,
( ~ spl16_37
| ~ spl16_238
| ~ spl16_244 ),
inference(sat_conversion,[],[f18164]) ).
cnf(s672,plain,
( ~ spl16_37
| ~ spl16_238
| ~ spl16_245 ),
inference(sat_conversion,[],[f18283]) ).
cnf(s704,plain,
( spl16_42
| ~ spl16_45
| spl16_74
| spl16_137
| spl16_138 ),
inference(sat_conversion,[],[f18442]) ).
cnf(s710,plain,
( spl16_74
| ~ spl16_85
| ~ spl16_138 ),
inference(sat_conversion,[],[f18455]) ).
cnf(s779,plain,
( ~ spl16_37
| spl16_74
| ~ spl16_138
| ~ spl16_238
| ~ spl16_243 ),
inference(sat_conversion,[],[f19295]) ).
cnf(s782,plain,
( ~ spl16_37
| spl16_42
| ~ spl16_45
| ~ spl16_238
| ~ spl16_241 ),
inference(sat_conversion,[],[f19316]) ).
cnf(s799,plain,
( ~ spl16_85
| spl16_263
| spl16_264 ),
inference(sat_conversion,[],[f20357]) ).
cnf(s802,plain,
( spl16_42
| ~ spl16_45
| ~ spl16_85
| ~ spl16_264 ),
inference(sat_conversion,[],[f20425]) ).
cnf(s803,plain,
( ~ spl16_263
| spl16_265
| spl16_266 ),
inference(sat_conversion,[],[f20445]) ).
cnf(s804,plain,
( ~ spl16_37
| ~ spl16_265
| spl16_267
| spl16_268 ),
inference(sat_conversion,[],[f20466]) ).
cnf(s812,plain,
( ~ spl16_85
| ~ spl16_268 ),
inference(sat_conversion,[],[f20553]) ).
cnf(s817,plain,
( ~ spl16_85
| ~ spl16_266 ),
inference(sat_conversion,[],[f20644]) ).
cnf(s824,plain,
( ~ spl16_37
| ~ spl16_85
| ~ spl16_267 ),
inference(sat_conversion,[],[f20750]) ).
cnf(s842,plain,
( spl16_74
| ~ spl16_85
| spl16_137
| spl16_138
| ~ spl16_264 ),
inference(sat_conversion,[],[f20907]) ).
cnf(s866,plain,
( ~ spl16_37
| spl16_42
| ~ spl16_131
| ~ spl16_238 ),
inference(sat_conversion,[],[f21033]) ).
cnf(s876,plain,
( spl16_1
| ~ spl16_61
| spl16_74
| spl16_137
| spl16_138 ),
inference(sat_conversion,[],[f21144]) ).
cnf(s890,plain,
( spl16_1
| ~ spl16_63
| ~ spl16_272 ),
inference(sat_conversion,[],[f21293]) ).
cnf(s905,plain,
( ~ spl16_239
| spl16_278
| spl16_279 ),
inference(sat_conversion,[],[f22547]) ).
cnf(s908,plain,
( spl16_74
| spl16_137
| spl16_138
| ~ spl16_239
| ~ spl16_279 ),
inference(sat_conversion,[],[f22625]) ).
cnf(s909,plain,
( ~ spl16_278
| spl16_280
| spl16_281 ),
inference(sat_conversion,[],[f22645]) ).
cnf(s912,plain,
( ~ spl16_239
| spl16_272
| ~ spl16_281 ),
inference(sat_conversion,[],[f22726]) ).
cnf(s915,plain,
( spl16_1
| ~ spl16_63
| ~ spl16_239
| ~ spl16_281 ),
inference(sat_conversion,[],[f22733]) ).
cnf(s916,plain,
( ~ spl16_37
| ~ spl16_280
| spl16_282
| spl16_283 ),
inference(sat_conversion,[],[f22754]) ).
cnf(s918,plain,
( ~ spl16_37
| ~ spl16_239
| spl16_247
| ~ spl16_282 ),
inference(sat_conversion,[],[f22848]) ).
cnf(s920,plain,
( ~ spl16_37
| spl16_42
| ~ spl16_131
| ~ spl16_239
| ~ spl16_282 ),
inference(sat_conversion,[],[f22853]) ).
cnf(s927,plain,
( ~ spl16_239
| ~ spl16_283 ),
inference(sat_conversion,[],[f22980]) ).
cnf(s943,plain,
( spl16_42
| ~ spl16_73
| ~ spl16_239
| ~ spl16_281 ),
inference(sat_conversion,[],[f23113]) ).
cnf(s951,plain,
( spl16_1
| ~ spl16_37
| ~ spl16_80
| ~ spl16_239
| ~ spl16_282 ),
inference(sat_conversion,[],[f23169]) ).
cnf(s956,plain,
( spl16_42
| ~ spl16_132
| ~ spl16_170 ),
inference(sat_conversion,[],[f23180]) ).
cnf(s958,plain,
( ~ spl16_37
| ~ spl16_238
| ~ spl16_243
| spl16_272 ),
inference(sat_conversion,[],[f23181]) ).
cnf(s968,plain,
( spl16_1
| ~ spl16_37
| ~ spl16_80
| ~ spl16_238 ),
inference(sat_conversion,[],[f23290]) ).
cnf(s979,plain,
( ~ spl16_37
| spl16_74
| ~ spl16_195
| ~ spl16_247 ),
inference(sat_conversion,[],[f23327]) ).
cnf(s992,plain,
( spl16_1
| ~ spl16_63
| ~ spl16_85 ),
inference(sat_conversion,[],[f23555]) ).
cnf(s1005,plain,
( spl16_1
| ~ spl16_61
| ~ spl16_85
| ~ spl16_264 ),
inference(sat_conversion,[],[f23603]) ).
cnf(s1022,plain,
( spl16_74
| ~ spl16_196
| ~ spl16_239 ),
inference(sat_conversion,[],[f23839]) ).
cnf(s1028,plain,
( spl16_42
| ~ spl16_45
| ~ spl16_239
| ~ spl16_279 ),
inference(sat_conversion,[],[f23861]) ).
cnf(s1031,plain,
( spl16_1
| ~ spl16_61
| ~ spl16_239
| ~ spl16_279 ),
inference(sat_conversion,[],[f23987]) ).
cnf(s1044,plain,
( spl16_74
| ~ spl16_138
| ~ spl16_272 ),
inference(sat_conversion,[],[f24099]) ).
cnf(s1045,plain,
( spl16_74
| ~ spl16_138
| ~ spl16_239
| ~ spl16_281 ),
inference(sat_conversion,[],[f24101]) ).
cnf(s1057,plain,
( spl16_1
| ~ spl16_37
| ~ spl16_61
| ~ spl16_238
| ~ spl16_241 ),
inference(sat_conversion,[],[f24115]) ).
cnf(s1088,plain,
~ spl16_74,
inference(rat,[],[s43,s628]) ).
cnf(s1089,plain,
~ spl16_42,
inference(rat,[],[s24,s122]) ).
cnf(s1090,plain,
spl16_37,
inference(rat,[],[s21,s26]) ).
cnf(s1091,plain,
~ spl16_1,
inference(rat,[],[s1,s35]) ).
cnf(s1092,plain,
( spl16_170
| ~ spl16_137
| ~ spl16_84 ),
inference(rat,[],[s637,s259,s636,s260,s643,s1088,s1090]) ).
cnf(s1093,plain,
( ~ spl16_195
| ~ spl16_63
| ~ spl16_45 ),
inference(rat,[],[s909,s916,s905,s918,s1028,s912,s927,s636,s637,s979,s890,s48,s992,s47,s51,s1090,s1089,s1088,s1091]) ).
cnf(s1094,plain,
( ~ spl16_63
| ~ spl16_45 ),
inference(rat,[],[s654,s653,s663,s782,s665,s672,s958,s636,s1022,s259,s1093,s704,s48,s135,s890,s992,s47,s51,s1090,s1089,s1088,s1091]) ).
cnf(s1095,plain,
( ~ spl16_195
| ~ spl16_84
| ~ spl16_62 ),
inference(rat,[],[s285,s46,s1092,s319,s287,s1091,s1090,s1088]) ).
cnf(s1096,plain,
( ~ spl16_137
| ~ spl16_84
| ~ spl16_62 ),
inference(rat,[],[s968,s636,s46,s1022,s285,s259,s1092,s1095,s1090,s1091,s1088]) ).
cnf(s1097,plain,
( ~ spl16_239
| spl16_272
| ~ spl16_45 ),
inference(rat,[],[s916,s951,s909,s46,s905,s642,s1028,s912,s927,s36,s1094,s34,s42,s1090,s1091,s1089]) ).
cnf(s1098,plain,
( ~ spl16_84
| ~ spl16_45 ),
inference(rat,[],[s654,s653,s663,s782,s665,s672,s958,s636,s1097,s1044,s704,s1096,s36,s1094,s34,s42,s1090,s1089,s1088,s1091]) ).
cnf(s1099,plain,
~ spl16_45,
inference(rat,[],[s799,s803,s804,s802,s812,s817,s824,s48,s1098,s47,s51,s1090,s1089]) ).
cnf(s1100,plain,
spl16_44,
inference(rat,[],[s25,s1089,s1099]) ).
cnf(s1101,plain,
( ~ spl16_239
| spl16_132
| ~ spl16_137
| spl16_62 ),
inference(rat,[],[s1031,s34,s905,s36,s909,s172,s943,s41,s916,s128,s918,s263,s979,s259,s1022,s927,s1091,s1089,s1100,s1090,s1088]) ).
cnf(s1102,plain,
( ~ spl16_137
| spl16_62
| ~ spl16_84 ),
inference(rat,[],[s1057,s34,s653,s36,s654,s172,s662,s41,s128,s663,s866,s665,s672,s636,s1101,s956,s1092,s1090,s1091,s1089,s1100]) ).
cnf(s1103,plain,
( ~ spl16_63
| ~ spl16_239
| spl16_137 ),
inference(rat,[],[s916,s920,s909,s128,s905,s41,s908,s915,s172,s135,s927,s956,s643,s1090,s1089,s1100,s1088,s1091]) ).
cnf(s1104,plain,
( ~ spl16_239
| spl16_137
| spl16_62 ),
inference(rat,[],[s920,s128,s916,s41,s909,s1045,s298,s905,s876,s1031,s34,s36,s1103,s956,s643,s927,s1089,s1090,s1100,s1088,s1091]) ).
cnf(s1105,plain,
( ~ spl16_63
| ~ spl16_238
| spl16_137 ),
inference(rat,[],[s653,s654,s657,s958,s135,s890,s663,s665,s672,s1090,s1088,s1091]) ).
cnf(s1106,plain,
( spl16_62
| ~ spl16_84 ),
inference(rat,[],[s654,s653,s779,s1057,s876,s34,s36,s1105,s663,s665,s672,s636,s1104,s1102,s1091,s1088,s1090]) ).
cnf(s1107,plain,
( ~ spl16_239
| ~ spl16_84 ),
inference(rat,[],[s905,s908,s909,s298,s943,s41,s916,s128,s951,s199,s46,s956,s642,s643,s927,s1096,s1106,s1088,s1089,s1100,s1090,s1091]) ).
cnf(s1108,plain,
( ~ spl16_62
| ~ spl16_84 ),
inference(rat,[],[s653,s654,s657,s662,s298,s41,s128,s190,s46,s663,s968,s866,s665,s672,s636,s1107,s1096,s1091,s1100,s1089,s1088,s1090]) ).
cnf(s1109,plain,
~ spl16_84,
inference(rat,[],[s1108,s1106]) ).
cnf(s1112,plain,
( ~ spl16_63
| ~ spl16_137 ),
inference(rat,[],[s310,s128,s259,s258,s294,s247,s241,s272,s240,s246,s253,s47,s41,s48,s172,s992,s1088,s1089,s1090,s1091,s1100,s1109]) ).
cnf(s1113,plain,
~ spl16_61,
inference(rat,[],[s799,s803,s804,s1005,s812,s817,s824,s48,s47,s90,s1090,s1091,s1109]) ).
cnf(s1114,plain,
spl16_60,
inference(rat,[],[s34,s1091,s1113]) ).
cnf(s1115,plain,
~ spl16_63,
inference(rat,[],[s47,s131,s48,s1112,s135,s992,s1088,s1109,s1091]) ).
cnf(s1116,plain,
spl16_62,
inference(rat,[],[s36,s1114,s1115]) ).
cnf(s1118,plain,
( ~ spl16_73
| ~ spl16_137 ),
inference(rat,[],[s262,s46,s259,s300,s294,s247,s241,s288,s240,s246,s253,s47,s48,s646,s1088,s1091,s1090,s1116,s1089,s1109]) ).
cnf(s1119,plain,
( ~ spl16_131
| ~ spl16_137 ),
inference(rat,[],[s262,s46,s259,s199,s263,s1088,s1091,s1090,s1116,s1089]) ).
cnf(s1120,plain,
~ spl16_137,
inference(rat,[],[s319,s46,s259,s190,s310,s128,s1119,s41,s1118,s1088,s1090,s1091,s1116,s1089,s1100]) ).
cnf(s1125,plain,
~ spl16_73,
inference(rat,[],[s47,s131,s48,s298,s646,s1088,s1120,s1109,s1089]) ).
cnf(s1126,plain,
spl16_72,
inference(rat,[],[s41,s1100,s1125]) ).
cnf(s1127,plain,
spl16_138,
inference(rat,[],[s799,s803,s804,s842,s812,s817,s824,s48,s47,s131,s1090,s1088,s1120,s1109]) ).
cnf(s1129,plain,
~ spl16_85,
inference(rat,[],[s710,s1088,s1127]) ).
cnf(s1131,plain,
~ spl16_82,
inference(rat,[],[s48,s1109,s1129]) ).
cnf(s1133,plain,
spl16_83,
inference(rat,[],[s47,s1131]) ).
cnf(s1135,plain,
~ spl16_194,
inference(rat,[],[s253,s1133]) ).
cnf(s1136,plain,
~ spl16_190,
inference(rat,[],[s246,s1133]) ).
cnf(s1137,plain,
spl16_189,
inference(rat,[],[s240,s1136,s1133]) ).
cnf(s1138,plain,
~ spl16_192,
inference(rat,[],[s244,s1127,s1088,s1133]) ).
cnf(s1139,plain,
spl16_191,
inference(rat,[],[s241,s1137,s1138]) ).
cnf(s1140,plain,
spl16_193,
inference(rat,[],[s247,s1135,s1090,s1139]) ).
cnf(s1141,plain,
~ spl16_131,
inference(rat,[],[s258,s1133,s1090,s1089,s1140]) ).
cnf(s1142,plain,
~ spl16_80,
inference(rat,[],[s300,s1133,s1091,s1090,s1140]) ).
cnf(s1143,plain,
spl16_132,
inference(rat,[],[s128,s1126,s1090,s1141]) ).
cnf(s1144,plain,
spl16_81,
inference(rat,[],[s46,s1116,s1090,s1142]) ).
cnf(s1146,plain,
$false,
inference(rat,[],[s190,s1091,s1089,s1143,s1144]) ).
fof(f24283,plain,
$false,
inference(avatar_sat_refutation,[],[s1146]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV546+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n018.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Mon Sep 28 06:37:39 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.41 Running first-order theorem proving
% 0.13/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.79/2.24 % (3177684)Detected formulas, will run a generic FOF schedule.
% 9.79/2.24 % (3177692)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=292038907:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.79/2.24 % (3177692)Refutation not found, incomplete strategy
% 9.79/2.24 % (3177692)------------------------------
% 9.79/2.24 % (3177692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.79/2.24 % (3177692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.79/2.24 % (3177692)CaDiCaL version: 2.1.3
% 9.79/2.24 % (3177692)Termination reason: Refutation not found, incomplete strategy
% 9.79/2.24 % (3177692)Time elapsed: 0.001 s
% 9.79/2.24 % (3177692)Peak memory usage: 88 MB
% 9.79/2.24 % (3177690)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=2362536559:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.79/2.24 % (3177689)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=2354530677:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.79/2.24 % (3177691)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=3756326518:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.79/2.24 % (3177693)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3425623581:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.79/2.24 % (3177695)dis-21_1_sil=8000:lcm=predicate:random_seed=1270396622: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.79/2.24 % (3177694)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3527783477:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.79/2.24 % (3177693)Instruction limit reached!
% 9.79/2.24 % (3177693)------------------------------
% 9.79/2.24 % (3177693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.79/2.24 % (3177693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.79/2.24 % (3177693)CaDiCaL version: 2.1.3
% 9.79/2.24 % (3177693)Termination reason: Instruction limit
% 9.79/2.24 % (3177693)Termination phase: Saturation
% 9.79/2.24 % (3177693)Time elapsed: 0.052 s
% 9.79/2.24 % (3177693)Peak memory usage: 87 MB
% 9.79/2.24 % (3177693)Instructions burned: 119 (million)
% 9.79/2.24 % (3177695)Instruction limit reached!
% 9.79/2.24 % (3177695)------------------------------
% 9.79/2.24 % (3177695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.79/2.24 % (3177695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.79/2.24 % (3177695)CaDiCaL version: 2.1.3
% 9.79/2.24 % (3177695)Termination reason: Instruction limit
% 9.79/2.24 % (3177695)Termination phase: Saturation
% 9.79/2.24 % (3177695)Time elapsed: 0.073 s
% 9.79/2.24 % (3177695)Peak memory usage: 88 MB
% 9.79/2.24 % (3177695)Instructions burned: 130 (million)
% 9.79/2.24 % (3177694)Instruction limit reached!
% 9.79/2.24 % (3177694)------------------------------
% 9.79/2.24 % (3177694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.79/2.24 % (3177694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.79/2.24 % (3177694)CaDiCaL version: 2.1.3
% 9.79/2.24 % (3177694)Termination reason: Instruction limit
% 9.79/2.24 % (3177694)Termination phase: Saturation
% 9.79/2.24 % (3177694)Time elapsed: 0.097 s
% 9.79/2.24 % (3177694)Peak memory usage: 89 MB
% 9.79/2.24 % (3177694)Instructions burned: 140 (million)
% 9.79/2.24 % (3177692)------------------------------
% 9.79/2.24 % (3177692)------------------------------
% 9.79/2.24 % (3177703)lrs+10_1_sil=8000:sp=occurrence:random_seed=19490282:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 9.79/2.24 % (3177704)lrs+10_1_sil=32000:urr=on:br=off:random_seed=278123243:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.79/2.24 % (3177704)Refutation not found, incomplete strategy
% 9.79/2.24 % (3177704)------------------------------
% 9.79/2.24 % (3177704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.79/2.24 % (3177704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.79/2.24 % (3177704)CaDiCaL version: 2.1.3
% 9.79/2.24 % (3177704)Termination reason: Refutation not found, incomplete strategy
% 16.48/3.18 % (3177704)Time elapsed: 0.002 s
% 16.48/3.18 % (3177704)Peak memory usage: 88 MB
% 16.48/3.18 % (3177704)Instructions burned: 1 (million)
% 16.48/3.18 % (3177706)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=3061101675:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 16.48/3.18 % (3177705)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2582340733:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 16.48/3.18 % (3177705)Refutation not found, incomplete strategy
% 16.48/3.18 % (3177705)------------------------------
% 16.48/3.18 % (3177705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/3.18 % (3177705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/3.18 % (3177705)CaDiCaL version: 2.1.3
% 16.48/3.18 % (3177705)Termination reason: Refutation not found, incomplete strategy
% 16.48/3.18 % (3177705)Time elapsed: 0.002 s
% 16.48/3.18 % (3177705)Peak memory usage: 88 MB
% 16.48/3.18 % (3177703)Instruction limit reached!
% 16.48/3.18 % (3177703)------------------------------
% 16.48/3.18 % (3177703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/3.18 % (3177703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/3.18 % (3177703)CaDiCaL version: 2.1.3
% 16.48/3.18 % (3177703)Termination reason: Instruction limit
% 16.48/3.18 % (3177703)Termination phase: Saturation
% 16.48/3.18 % (3177703)Time elapsed: 0.101 s
% 16.48/3.18 % (3177703)Peak memory usage: 91 MB
% 16.48/3.18 % (3177703)Instructions burned: 286 (million)
% 16.48/3.18 % (3177706)Instruction limit reached!
% 16.48/3.18 % (3177706)------------------------------
% 16.48/3.18 % (3177706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/3.18 % (3177706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/3.18 % (3177706)CaDiCaL version: 2.1.3
% 16.48/3.18 % (3177706)Termination reason: Instruction limit
% 16.48/3.18 % (3177706)Termination phase: Saturation
% 16.48/3.18 % (3177706)Time elapsed: 0.145 s
% 16.48/3.18 % (3177706)Peak memory usage: 91 MB
% 16.48/3.18 % (3177706)Instructions burned: 248 (million)
% 16.48/3.18 % (3177711)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4060780030:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 16.48/3.18 % (3177711)Refutation not found, incomplete strategy
% 16.48/3.18 % (3177711)------------------------------
% 16.48/3.18 % (3177711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/3.18 % (3177711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/3.18 % (3177711)CaDiCaL version: 2.1.3
% 16.48/3.18 % (3177711)Termination reason: Refutation not found, incomplete strategy
% 16.48/3.18 % (3177711)Time elapsed: 0.001 s
% 16.48/3.18 % (3177711)Peak memory usage: 88 MB
% 16.48/3.18 % (3177711)Instructions burned: 1 (million)
% 16.48/3.18 % (3177704)------------------------------
% 16.48/3.18 % (3177704)------------------------------
% 16.48/3.18 % (3177705)------------------------------
% 16.48/3.18 % (3177705)------------------------------
% 16.48/3.18 % (3177712)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3434697737:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 16.48/3.18 % (3177691)Refutation not found, incomplete strategy
% 16.48/3.18 % (3177691)------------------------------
% 16.48/3.18 % (3177691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/3.18 % (3177691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/3.18 % (3177691)CaDiCaL version: 2.1.3
% 16.48/3.18 % (3177691)Termination reason: Refutation not found, incomplete strategy
% 16.48/3.18 % (3177691)Time elapsed: 0.555 s
% 16.48/3.18 % (3177691)Peak memory usage: 125 MB
% 16.48/3.18 % (3177691)Instructions burned: 824 (million)
% 16.48/3.18 % (3177711)------------------------------
% 16.48/3.18 % (3177711)------------------------------
% 16.48/3.18 % (3177714)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3160708084:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 16.48/3.18 % (3177715)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1700986759:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 16.48/3.18 % (3177717)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4117951657:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 29.98/5.10 % (3177717)Refutation not found, incomplete strategy
% 29.98/5.10 % (3177717)------------------------------
% 29.98/5.10 % (3177717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.98/5.10 % (3177717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/5.10 % (3177717)CaDiCaL version: 2.1.3
% 29.98/5.10 % (3177717)Termination reason: Refutation not found, incomplete strategy
% 29.98/5.10 % (3177717)Time elapsed: 0.001 s
% 29.98/5.10 % (3177717)Peak memory usage: 88 MB
% 29.98/5.10 % (3177714)Instruction limit reached!
% 29.98/5.10 % (3177714)------------------------------
% 29.98/5.10 % (3177714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.98/5.10 % (3177714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/5.10 % (3177714)CaDiCaL version: 2.1.3
% 29.98/5.10 % (3177714)Termination reason: Instruction limit
% 29.98/5.10 % (3177714)Termination phase: Saturation
% 29.98/5.10 % (3177714)Time elapsed: 0.071 s
% 29.98/5.10 % (3177714)Peak memory usage: 89 MB
% 29.98/5.10 % (3177714)Instructions burned: 113 (million)
% 29.98/5.10 % (3177715)Instruction limit reached!
% 29.98/5.10 % (3177715)------------------------------
% 29.98/5.10 % (3177715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.98/5.10 % (3177715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/5.10 % (3177715)CaDiCaL version: 2.1.3
% 29.98/5.10 % (3177715)Termination reason: Instruction limit
% 29.98/5.10 % (3177715)Termination phase: Saturation
% 29.98/5.10 % (3177715)Time elapsed: 0.062 s
% 29.98/5.10 % (3177715)Peak memory usage: 88 MB
% 29.98/5.10 % (3177715)Instructions burned: 128 (million)
% 29.98/5.10 % (3177691)------------------------------
% 29.98/5.10 % (3177691)------------------------------
% 29.98/5.10 % (3177717)------------------------------
% 29.98/5.10 % (3177717)------------------------------
% 29.98/5.10 % (3177721)lrs+10_1_sil=8000:sp=occurrence:random_seed=632921784:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 29.98/5.10 % (3177722)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=492834290:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 29.98/5.10 % (3177722)Refutation not found, incomplete strategy
% 29.98/5.10 % (3177722)------------------------------
% 29.98/5.10 % (3177722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.98/5.10 % (3177722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/5.10 % (3177722)CaDiCaL version: 2.1.3
% 29.98/5.10 % (3177722)Termination reason: Refutation not found, incomplete strategy
% 29.98/5.10 % (3177722)Time elapsed: 0.001 s
% 29.98/5.10 % (3177722)Peak memory usage: 88 MB
% 29.98/5.10 % (3177724)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1495986191:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2990 on theBenchmark for (2990ds/134Mi)
% 29.98/5.10 % (3177724)Refutation not found, incomplete strategy
% 29.98/5.10 % (3177724)------------------------------
% 29.98/5.10 % (3177724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.98/5.10 % (3177724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/5.10 % (3177724)CaDiCaL version: 2.1.3
% 29.98/5.10 % (3177724)Termination reason: Refutation not found, incomplete strategy
% 29.98/5.10 % (3177724)Time elapsed: 0.001 s
% 29.98/5.10 % (3177724)Peak memory usage: 88 MB
% 29.98/5.10 % (3177723)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=242777382:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 29.98/5.10 % (3177724)------------------------------
% 29.98/5.10 % (3177724)------------------------------
% 29.98/5.10 % (3177722)------------------------------
% 29.98/5.10 % (3177722)------------------------------
% 29.98/5.10 % (3177729)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1358365869:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 29.98/5.10 % (3177729)Refutation not found, incomplete strategy
% 29.98/5.10 % (3177729)------------------------------
% 29.98/5.10 % (3177729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.98/5.10 % (3177729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/5.10 % (3177729)CaDiCaL version: 2.1.3
% 29.98/5.10 % (3177729)Termination reason: Refutation not found, incomplete strategy
% 29.98/5.10 % (3177729)Time elapsed: 0.001 s
% 29.98/5.10 % (3177729)Peak memory usage: 88 MB
% 29.98/5.10 % (3177729)Instructions burned: 1 (million)
% 33.54/5.64 % (3177730)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1089924224:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 33.54/5.64 % (3177729)------------------------------
% 33.54/5.64 % (3177729)------------------------------
% 33.54/5.64 % (3177721)Instruction limit reached!
% 33.54/5.64 % (3177721)------------------------------
% 33.54/5.64 % (3177721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.64 % (3177721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.64 % (3177721)CaDiCaL version: 2.1.3
% 33.54/5.64 % (3177721)Termination reason: Instruction limit
% 33.54/5.64 % (3177721)Termination phase: Saturation
% 33.54/5.64 % (3177721)Time elapsed: 0.579 s
% 33.54/5.64 % (3177721)Peak memory usage: 98 MB
% 33.54/5.64 % (3177721)Instructions burned: 908 (million)
% 33.54/5.64 % (3177733)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=633863926:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 33.54/5.64 % (3177733)Instruction limit reached!
% 33.54/5.64 % (3177733)------------------------------
% 33.54/5.64 % (3177733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.64 % (3177733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.64 % (3177733)CaDiCaL version: 2.1.3
% 33.54/5.64 % (3177733)Termination reason: Instruction limit
% 33.54/5.64 % (3177733)Termination phase: Saturation
% 33.54/5.64 % (3177733)Time elapsed: 0.044 s
% 33.54/5.64 % (3177733)Peak memory usage: 90 MB
% 33.54/5.64 % (3177733)Instructions burned: 126 (million)
% 33.54/5.64 % (3177734)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=965639784:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 33.54/5.64 % (3177736)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1144054270:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi)
% 33.54/5.64 % (3177736)Refutation not found, incomplete strategy
% 33.54/5.64 % (3177736)------------------------------
% 33.54/5.64 % (3177736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.64 % (3177736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.64 % (3177736)CaDiCaL version: 2.1.3
% 33.54/5.64 % (3177736)Termination reason: Refutation not found, incomplete strategy
% 33.54/5.64 % (3177736)Time elapsed: 0.001 s
% 33.54/5.64 % (3177736)Peak memory usage: 88 MB
% 33.54/5.64 % (3177734)Instruction limit reached!
% 33.54/5.64 % (3177734)------------------------------
% 33.54/5.64 % (3177734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.64 % (3177734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.64 % (3177734)CaDiCaL version: 2.1.3
% 33.54/5.64 % (3177734)Termination reason: Instruction limit
% 33.54/5.64 % (3177734)Termination phase: Saturation
% 33.54/5.64 % (3177734)Time elapsed: 0.077 s
% 33.54/5.64 % (3177734)Peak memory usage: 91 MB
% 33.54/5.64 % (3177734)Instructions burned: 136 (million)
% 33.54/5.64 % (3177736)------------------------------
% 33.54/5.64 % (3177736)------------------------------
% 33.54/5.64 % (3177739)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=185682541:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 33.54/5.64 % (3177739)Refutation not found, incomplete strategy
% 33.54/5.64 % (3177739)------------------------------
% 33.54/5.64 % (3177739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.64 % (3177739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.64 % (3177739)CaDiCaL version: 2.1.3
% 33.54/5.64 % (3177739)Termination reason: Refutation not found, incomplete strategy
% 33.54/5.64 % (3177739)Time elapsed: 0.001 s
% 33.54/5.64 % (3177739)Peak memory usage: 88 MB
% 33.54/5.64 % (3177740)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=4075518908:i=6060:aac=none:ins=25_2980 on theBenchmark for (2980ds/6060Mi)
% 33.54/5.64 % (3177739)------------------------------
% 33.54/5.64 % (3177739)------------------------------
% 33.54/5.64 % (3177712)Instruction limit reached!
% 33.54/5.64 % (3177712)------------------------------
% 33.54/5.64 % (3177712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.64 % (3177712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.64 % (3177712)CaDiCaL version: 2.1.3
% 33.54/5.64 % (3177712)Termination reason: Instruction limit
% 33.54/5.64 % (3177712)Termination phase: Saturation
% 33.54/5.64 % (3177712)Time elapsed: 1.607 s
% 33.54/5.64 % (3177712)Peak memory usage: 141 MB
% 33.54/5.64 % (3177712)Instructions burned: 2351 (million)
% 33.54/5.64 % (3177743)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=4097760637:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2977 on theBenchmark for (2977ds/150Mi)
% 33.54/5.64 % (3177743)Instruction limit reached!
% 33.54/5.64 % (3177743)------------------------------
% 33.54/5.64 % (3177743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.64 % (3177743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.64 % (3177743)CaDiCaL version: 2.1.3
% 33.54/5.64 % (3177743)Termination reason: Instruction limit
% 33.54/5.64 % (3177743)Termination phase: Saturation
% 33.54/5.64 % (3177743)Time elapsed: 0.092 s
% 33.54/5.64 % (3177743)Peak memory usage: 90 MB
% 33.54/5.64 % (3177743)Instructions burned: 152 (million)
% 33.54/5.64 % (3177744)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2412025555:i=14155:bd=all_2976 on theBenchmark for (2976ds/14155Mi)
% 33.54/5.64 % (3177747)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=392691330:i=667:av=off:fsr=off_2974 on theBenchmark for (2974ds/667Mi)
% 33.54/5.64 % (3177747)Refutation not found, incomplete strategy
% 33.54/5.64 % (3177747)------------------------------
% 33.54/5.64 % (3177747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.64 % (3177747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.64 % (3177747)CaDiCaL version: 2.1.3
% 33.54/5.64 % (3177747)Termination reason: Refutation not found, incomplete strategy
% 33.54/5.64 % (3177747)Time elapsed: 0.002 s
% 33.54/5.64 % (3177747)Peak memory usage: 88 MB
% 33.54/5.64 % (3177747)Instructions burned: 1 (million)
% 33.54/5.64 % (3177747)------------------------------
% 33.54/5.64 % (3177747)------------------------------
% 33.54/5.64 % (3177749)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1392412515:s2a=on:i=185:s2at=1.8:fdi=4_2970 on theBenchmark for (2970ds/185Mi)
% 33.54/5.64 % (3177749)Instruction limit reached!
% 33.54/5.64 % (3177749)------------------------------
% 33.54/5.64 % (3177749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.64 % (3177749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.64 % (3177749)CaDiCaL version: 2.1.3
% 33.54/5.64 % (3177749)Termination reason: Instruction limit
% 33.54/5.64 % (3177749)Termination phase: Saturation
% 33.54/5.64 % (3177749)Time elapsed: 0.097 s
% 33.54/5.64 % (3177749)Peak memory usage: 90 MB
% 33.54/5.64 % (3177749)Instructions burned: 185 (million)
% 33.54/5.64 % (3177751)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3696623447:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2968 on theBenchmark for (2968ds/193Mi)
% 33.54/5.64 % (3177751)Instruction limit reached!
% 33.54/5.64 % (3177751)------------------------------
% 33.54/5.64 % (3177751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.64 % (3177751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.64 % (3177751)CaDiCaL version: 2.1.3
% 33.54/5.64 % (3177751)Termination reason: Instruction limit
% 33.54/5.64 % (3177751)Termination phase: Saturation
% 33.54/5.64 % (3177751)Time elapsed: 0.092 s
% 33.54/5.64 % (3177751)Peak memory usage: 89 MB
% 33.54/5.64 % (3177751)Instructions burned: 195 (million)
% 33.54/5.64 % (3177753)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=492425774:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2965 on theBenchmark for (2965ds/4850Mi)
% 33.54/5.64 % (3177723)Instruction limit reached!
% 33.54/5.64 % (3177723)------------------------------
% 33.54/5.64 % (3177723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.54/5.64 % (3177723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.54/5.64 % (3177723)CaDiCaL version: 2.1.3
% 33.54/5.64 % (3177723)Termination reason: Instruction limit
% 33.54/5.64 % (3177723)Termination phase: Saturation
% 33.54/5.64 % (3177723)Time elapsed: 3.126 s
% 33.54/5.64 % (3177723)Peak memory usage: 169 MB
% 33.54/5.64 % (3177723)Instructions burned: 5204 (million)
% 33.54/5.64 % (3177755)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3865366725:i=12111:sd=1:ss=included_2957 on theBenchmark for (2957ds/12111Mi)
% 33.54/5.64 % (3177744)First to succeed.
% 33.54/5.64 % (3177744)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3177684"
% 33.54/5.64 % (3177744)Refutation found. Thanks to Tanya!
% 33.54/5.64 % SZS status Theorem for theBenchmark
% 33.54/5.64 % SZS output start Proof for theBenchmark
% See solution above
% 34.44/5.84 % (3177744)------------------------------
% 34.44/5.84 % (3177744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.44/5.84 % (3177744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.44/5.84 % (3177744)CaDiCaL version: 2.1.3
% 34.44/5.84 % (3177744)Termination reason: Refutation
% 34.44/5.84 % (3177744)Time elapsed: 2.009 s
% 34.44/5.84 % (3177744)Peak memory usage: 144 MB
% 34.44/5.84 % (3177744)Instructions burned: 2977 (million)
% 34.44/5.84 % (3177744)------------------------------
% 34.44/5.84 % (3177744)------------------------------
% 34.44/5.84 % (3177684)Success in time 4.779 s
% 34.44/5.84 % Vampire exiting
%------------------------------------------------------------------------------