%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV544+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 : n011.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 35.54s 6.04s
% Output : Refutation 37.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 55
% Syntax : Number of formulae : 491 ( 83 unt; 43 def)
% Number of atoms : 1198 ( 87 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1186 ( 479 ~; 626 |; 32 &)
% ( 43 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 42 ( 40 usr; 36 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 9 con; 0-2 aty)
% Number of variables : 184 ( 0 sgn 173 !; 11 ?)
% 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(f26,conjecture,
~ atleast4p(a(p(s(s(n(e)))),n(s(n(e))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',atmost3_81) ).
fof(f27,negated_conjecture,
~ ~ atleast4p(a(p(s(s(n(e)))),n(s(n(e))))),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f28,plain,
atleast4p(a(p(s(s(n(e)))),n(s(n(e))))),
inference(flattening,[],[f27]) ).
fof(f29,plain,
! [X0] :
( atleast4p(X0)
=> ? [X1] :
( subq(X1,X0)
& atleast3p(X1)
& ~ subq(X0,X1) ) ),
inference(unused_predicate_definition_removal,[],[f13]) ).
fof(f30,plain,
! [X0] :
( atleast3p(X0)
=> ? [X1] :
( subq(X1,X0)
& atleast2p(X1)
& ~ subq(X0,X1) ) ),
inference(unused_predicate_definition_removal,[],[f12]) ).
fof(f31,plain,
! [X0] :
( atleast2p(X0)
=> ? [X1] :
( mem(X1,X0)
& ~ subq(X0,p(X1)) ) ),
inference(unused_predicate_definition_removal,[],[f11]) ).
fof(f32,plain,
! [X0,X1] :
( subq(X0,X1)
<=> ! [X2] :
( mem(X2,X1)
| ~ mem(X2,X0) ) ),
inference(ennf_transformation,[],[f1]) ).
fof(f33,plain,
! [X0,X1] :
( X0 = X1
| ~ subq(X1,X0)
| ~ subq(X0,X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f34,plain,
! [X0,X1] :
( X0 = X1
| ~ subq(X1,X0)
| ~ subq(X0,X1) ),
inference(flattening,[],[f33]) ).
fof(f35,plain,
! [X0] :
( ? [X1] :
( mem(X1,X0)
& ~ subq(X0,p(X1)) )
| ~ atleast2p(X0) ),
inference(ennf_transformation,[],[f31]) ).
fof(f36,plain,
! [X0] :
( ? [X1] :
( subq(X1,X0)
& atleast2p(X1)
& ~ subq(X0,X1) )
| ~ atleast3p(X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f37,plain,
! [X0] :
( ? [X1] :
( subq(X1,X0)
& atleast3p(X1)
& ~ subq(X0,X1) )
| ~ atleast4p(X0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f38,plain,
! [X0,X1] :
( ( subq(X0,X1)
| ? [X2] :
( ~ mem(X2,X1)
& mem(X2,X0) ) )
& ( ! [X2] :
( mem(X2,X1)
| ~ mem(X2,X0) )
| ~ subq(X0,X1) ) ),
inference(nnf_transformation,[],[f32]) ).
fof(f39,plain,
! [X0,X1] :
( ( subq(X0,X1)
| ? [X2] :
( ~ mem(X2,X1)
& mem(X2,X0) ) )
& ( ! [X3] :
( mem(X3,X1)
| ~ mem(X3,X0) )
| ~ subq(X0,X1) ) ),
inference(rectify,[],[f38]) ).
fof(f40,plain,
! [X0,X1] :
( ( subq(X0,X1)
| ( ~ mem(sK0(X0,X1),X1)
& mem(sK0(X0,X1),X0) ) )
& ( ! [X3] :
( mem(X3,X1)
| ~ mem(X3,X0) )
| ~ subq(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f39]) ).
fof(f41,plain,
! [X0,X1] :
( ( mem(X0,s(X1))
| X0 != X1 )
& ( X0 = X1
| ~ mem(X0,s(X1)) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f42,plain,
! [X0,X1,X2] :
( ( mem(X0,u(X1,X2))
| ( ~ mem(X0,X1)
& ~ mem(X0,X2) ) )
& ( mem(X0,X1)
| mem(X0,X2)
| ~ mem(X0,u(X1,X2)) ) ),
inference(nnf_transformation,[],[f6]) ).
fof(f43,plain,
! [X0,X1,X2] :
( ( mem(X0,u(X1,X2))
| ( ~ mem(X0,X1)
& ~ mem(X0,X2) ) )
& ( mem(X0,X1)
| mem(X0,X2)
| ~ mem(X0,u(X1,X2)) ) ),
inference(flattening,[],[f42]) ).
fof(f46,plain,
! [X0,X1] :
( ( mem(X0,p(X1))
| ~ subq(X0,X1) )
& ( subq(X0,X1)
| ~ mem(X0,p(X1)) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f47,plain,
! [X0] :
( ( mem(sK1(X0),X0)
& ~ subq(X0,p(sK1(X0))) )
| ~ atleast2p(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X1,sK1(X0))],[f35]) ).
fof(f48,plain,
! [X0] :
( ( subq(sK2(X0),X0)
& atleast2p(sK2(X0))
& ~ subq(X0,sK2(X0)) )
| ~ atleast3p(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X1,sK2(X0))],[f36]) ).
fof(f49,plain,
! [X0] :
( ( subq(sK3(X0),X0)
& atleast3p(sK3(X0))
& ~ subq(X0,sK3(X0)) )
| ~ atleast4p(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X1,sK3(X0))],[f37]) ).
fof(f50,plain,
! [X3,X0,X1] :
( ~ mem(X3,X0)
| mem(X3,X1)
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
fof(f51,plain,
! [X0,X1] :
( mem(sK0(X0,X1),X0)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
fof(f52,plain,
! [X0,X1] :
( ~ mem(sK0(X0,X1),X1)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
fof(f53,plain,
! [X0,X1] :
( ~ subq(X1,X0)
| X0 = X1
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f54,plain,
! [X0] : ~ mem(X0,e),
inference(cnf_transformation,[],[f4]) ).
fof(f55,plain,
! [X0,X1] :
( ~ mem(X0,s(X1))
| X0 = X1 ),
inference(cnf_transformation,[],[f41]) ).
fof(f56,plain,
! [X0,X1] :
( mem(X0,s(X1))
| X0 != X1 ),
inference(cnf_transformation,[],[f41]) ).
fof(f57,plain,
! [X2,X0,X1] :
( ~ mem(X0,u(X1,X2))
| mem(X0,X2)
| mem(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f58,plain,
! [X2,X0,X1] :
( mem(X0,u(X1,X2))
| ~ mem(X0,X2) ),
inference(cnf_transformation,[],[f43]) ).
fof(f59,plain,
! [X2,X0,X1] :
( mem(X0,u(X1,X2))
| ~ mem(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f63,plain,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
inference(cnf_transformation,[],[f8]) ).
fof(f64,plain,
! [X0] : n(X0) = a(X0,X0),
inference(cnf_transformation,[],[f9]) ).
fof(f65,plain,
! [X0,X1] :
( ~ mem(X0,p(X1))
| subq(X0,X1) ),
inference(cnf_transformation,[],[f46]) ).
fof(f66,plain,
! [X0,X1] :
( mem(X0,p(X1))
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f46]) ).
fof(f67,plain,
! [X0] :
( ~ subq(X0,p(sK1(X0)))
| ~ atleast2p(X0) ),
inference(cnf_transformation,[],[f47]) ).
fof(f68,plain,
! [X0] :
( mem(sK1(X0),X0)
| ~ atleast2p(X0) ),
inference(cnf_transformation,[],[f47]) ).
fof(f69,plain,
! [X0] :
( ~ subq(X0,sK2(X0))
| ~ atleast3p(X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f70,plain,
! [X0] :
( atleast2p(sK2(X0))
| ~ atleast3p(X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f71,plain,
! [X0] :
( subq(sK2(X0),X0)
| ~ atleast3p(X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f72,plain,
! [X0] :
( ~ subq(X0,sK3(X0))
| ~ atleast4p(X0) ),
inference(cnf_transformation,[],[f49]) ).
fof(f73,plain,
! [X0] :
( atleast3p(sK3(X0))
| ~ atleast4p(X0) ),
inference(cnf_transformation,[],[f49]) ).
fof(f74,plain,
! [X0] :
( subq(sK3(X0),X0)
| ~ atleast4p(X0) ),
inference(cnf_transformation,[],[f49]) ).
fof(f75,plain,
atleast4p(a(p(s(s(n(e)))),n(s(n(e))))),
inference(cnf_transformation,[],[f28]) ).
fof(f76,plain,
! [X0] : n(X0) = u(X0,s(X0)),
inference(definition_unfolding,[],[f64,f63]) ).
fof(f77,plain,
atleast4p(u(p(s(s(u(e,s(e))))),s(u(s(u(e,s(e))),s(s(u(e,s(e)))))))),
inference(definition_unfolding,[],[f75,f63,f76,f76,f76]) ).
fof(f78,plain,
! [X1] : mem(X1,s(X1)),
inference(equality_resolution,[],[f56]) ).
fof(f79,definition,
sF4 = s(e),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f80,plain,
s(e) = sF4,
inference(reorient_equations,[],[f79]) ).
fof(f81,definition,
sF5 = u(e,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f82,plain,
u(e,sF4) = sF5,
inference(reorient_equations,[],[f81]) ).
fof(f83,definition,
sF6 = s(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f84,plain,
s(sF5) = sF6,
inference(reorient_equations,[],[f83]) ).
fof(f85,definition,
sF7 = s(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f86,plain,
s(sF6) = sF7,
inference(reorient_equations,[],[f85]) ).
fof(f87,definition,
sF8 = p(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f88,plain,
p(sF7) = sF8,
inference(reorient_equations,[],[f87]) ).
fof(f89,definition,
sF9 = u(sF6,sF7),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f90,plain,
u(sF6,sF7) = sF9,
inference(reorient_equations,[],[f89]) ).
fof(f91,definition,
sF10 = s(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f92,plain,
s(sF9) = sF10,
inference(reorient_equations,[],[f91]) ).
fof(f93,definition,
sF11 = u(sF8,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f94,plain,
u(sF8,sF10) = sF11,
inference(reorient_equations,[],[f93]) ).
fof(f95,plain,
atleast4p(sF11),
inference(definition_folding,[],[f77,f94,f92,f90,f86,f84,f82,f80,f84,f82,f80,f88,f86,f84,f82,f80]) ).
fof(f96,plain,
mem(e,sF4),
inference(superposition,[],[f78,f80]) ).
fof(f102,plain,
! [X0] :
( ~ mem(X0,sF4)
| e = X0 ),
inference(superposition,[],[f55,f80]) ).
fof(f104,plain,
! [X0] :
( ~ mem(X0,sF7)
| sF6 = X0 ),
inference(superposition,[],[f55,f86]) ).
fof(f105,plain,
! [X0] :
( ~ mem(X0,sF10)
| sF9 = X0 ),
inference(superposition,[],[f55,f92]) ).
fof(f106,plain,
! [X0] :
( ~ mem(X0,sF8)
| subq(X0,sF7) ),
inference(superposition,[],[f65,f88]) ).
fof(f119,plain,
! [X0] :
( subq(X0,X0)
| subq(X0,X0) ),
inference(resolution,[],[f51,f52]) ).
fof(f120,plain,
! [X0] : subq(e,X0),
inference(resolution,[],[f51,f54]) ).
fof(f121,plain,
! [X0,X1] :
( sK0(s(X0),X1) = X0
| subq(s(X0),X1) ),
inference(resolution,[],[f51,f55]) ).
fof(f125,plain,
! [X0] :
( sF6 = sK0(sF7,X0)
| subq(sF7,X0) ),
inference(resolution,[],[f51,f104]) ).
fof(f127,plain,
! [X0] : subq(X0,X0),
inference(duplicate_literal_removal,[],[f119]) ).
fof(f133,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X2)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f58,f52]) ).
fof(f135,plain,
! [X0] :
( ~ mem(X0,sF4)
| mem(X0,sF5) ),
inference(superposition,[],[f58,f82]) ).
fof(f137,plain,
subq(sK3(sF11),sF11),
inference(unit_resulting_resolution,[],[f74,f95]) ).
fof(f144,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X1)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f59,f52]) ).
fof(f155,plain,
! [X0] :
( ~ mem(X0,sF11)
| mem(X0,sF10)
| mem(X0,sF8) ),
inference(superposition,[],[f57,f94]) ).
fof(f156,plain,
! [X0] :
( ~ mem(X0,sF5)
| mem(X0,sF4)
| mem(X0,e) ),
inference(superposition,[],[f57,f82]) ).
fof(f158,plain,
! [X0] :
( ~ mem(X0,sF5)
| mem(X0,sF4) ),
inference(forward_subsumption_resolution,[],[f156,f54]) ).
fof(f160,plain,
! [X0] :
( mem(sK0(sF5,X0),sF4)
| subq(sF5,X0) ),
inference(resolution,[],[f158,f51]) ).
fof(f162,plain,
mem(e,sF5),
inference(resolution,[],[f135,f96]) ).
fof(f178,plain,
! [X0,X1] :
( ~ subq(s(X0),X1)
| mem(X0,X1) ),
inference(resolution,[],[f50,f78]) ).
fof(f184,plain,
! [X2,X0,X1] :
( mem(sK0(X0,X1),X2)
| ~ subq(X0,X2)
| subq(X0,X1) ),
inference(resolution,[],[f50,f51]) ).
fof(f207,plain,
atleast3p(sK3(sF11)),
inference(unit_resulting_resolution,[],[f73,f95]) ).
fof(f212,plain,
! [X0] :
( ~ subq(X0,e)
| e = X0 ),
inference(resolution,[],[f120,f53]) ).
fof(f214,plain,
( sF11 = sK3(sF11)
| ~ subq(sF11,sK3(sF11)) ),
inference(resolution,[],[f137,f53]) ).
fof(f216,definition,
( spl12_1
<=> subq(sF11,sK3(sF11)) ),
introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition]) ).
fof(f218,plain,
( ~ subq(sF11,sK3(sF11))
| spl12_1 ),
inference(avatar_component_clause,[],[f216]) ).
fof(f220,definition,
( spl12_2
<=> sF11 = sK3(sF11) ),
introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition]) ).
fof(f222,plain,
( sF11 = sK3(sF11)
| ~ spl12_2 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f223,plain,
( ~ spl12_1
| spl12_2 ),
inference(avatar_split_clause,[],[f214,f220,f216]) ).
fof(f226,plain,
! [X0,X1] :
( mem(sK1(X0),X1)
| ~ atleast2p(X0)
| ~ subq(X0,X1) ),
inference(resolution,[],[f68,f50]) ).
fof(f361,plain,
~ subq(sF11,sK3(sF11)),
inference(unit_resulting_resolution,[],[f72,f95]) ).
fof(f370,plain,
subq(sK2(sK3(sF11)),sK3(sF11)),
inference(unit_resulting_resolution,[],[f71,f207]) ).
fof(f383,plain,
( sK3(sF11) = sK2(sK3(sF11))
| ~ subq(sK3(sF11),sK2(sK3(sF11))) ),
inference(resolution,[],[f370,f53]) ).
fof(f385,definition,
( spl12_30
<=> subq(sK3(sF11),sK2(sK3(sF11))) ),
introduced(definition,[new_symbols(definition,[spl12_30])],[avatar_definition]) ).
fof(f387,plain,
( ~ subq(sK3(sF11),sK2(sK3(sF11)))
| spl12_30 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f389,definition,
( spl12_31
<=> sK3(sF11) = sK2(sK3(sF11)) ),
introduced(definition,[new_symbols(definition,[spl12_31])],[avatar_definition]) ).
fof(f391,plain,
( sK3(sF11) = sK2(sK3(sF11))
| ~ spl12_31 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f392,plain,
( ~ spl12_30
| spl12_31 ),
inference(avatar_split_clause,[],[f383,f389,f385]) ).
fof(f394,plain,
( subq(sF5,sF4)
| subq(sF5,sF4) ),
inference(resolution,[],[f160,f52]) ).
fof(f396,plain,
! [X0] :
( e = sK0(sF5,X0)
| subq(sF5,X0) ),
inference(resolution,[],[f160,f102]) ).
fof(f398,plain,
subq(sF5,sF4),
inference(duplicate_literal_removal,[],[f394]) ).
fof(f401,plain,
! [X0] :
( ~ mem(e,X0)
| subq(sF5,X0)
| subq(sF5,X0) ),
inference(superposition,[],[f52,f396]) ).
fof(f402,plain,
! [X0] :
( ~ mem(e,X0)
| subq(sF5,X0) ),
inference(duplicate_literal_removal,[],[f401]) ).
fof(f407,plain,
( sF4 = sF5
| ~ subq(sF4,sF5) ),
inference(resolution,[],[f398,f53]) ).
fof(f409,definition,
( spl12_32
<=> subq(sF4,sF5) ),
introduced(definition,[new_symbols(definition,[spl12_32])],[avatar_definition]) ).
fof(f411,plain,
( ~ subq(sF4,sF5)
| spl12_32 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f413,definition,
( spl12_33
<=> sF4 = sF5 ),
introduced(definition,[new_symbols(definition,[spl12_33])],[avatar_definition]) ).
fof(f415,plain,
( sF4 = sF5
| ~ spl12_33 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f416,plain,
( ~ spl12_32
| spl12_33 ),
inference(avatar_split_clause,[],[f407,f413,f409]) ).
fof(f423,plain,
! [X0] :
( subq(sF5,p(X0))
| ~ subq(e,X0) ),
inference(resolution,[],[f402,f66]) ).
fof(f426,plain,
! [X0] : subq(sF5,p(X0)),
inference(forward_subsumption_resolution,[],[f423,f120]) ).
fof(f429,plain,
( mem(sK0(sK3(sF11),sK2(sK3(sF11))),sK3(sF11))
| spl12_30 ),
inference(unit_resulting_resolution,[],[f51,f387]) ).
fof(f432,plain,
( mem(sK0(sK3(sF11),sK2(sK3(sF11))),sF11)
| spl12_30 ),
inference(unit_resulting_resolution,[],[f50,f137,f429]) ).
fof(f440,plain,
( mem(sK0(sK3(sF11),sK2(sK3(sF11))),sF10)
| mem(sK0(sK3(sF11),sK2(sK3(sF11))),sF8)
| spl12_30 ),
inference(resolution,[],[f432,f155]) ).
fof(f443,definition,
( spl12_34
<=> mem(sK0(sK3(sF11),sK2(sK3(sF11))),sF8) ),
introduced(definition,[new_symbols(definition,[spl12_34])],[avatar_definition]) ).
fof(f445,plain,
( mem(sK0(sK3(sF11),sK2(sK3(sF11))),sF8)
| ~ spl12_34 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f447,definition,
( spl12_35
<=> mem(sK0(sK3(sF11),sK2(sK3(sF11))),sF10) ),
introduced(definition,[new_symbols(definition,[spl12_35])],[avatar_definition]) ).
fof(f448,plain,
( ~ mem(sK0(sK3(sF11),sK2(sK3(sF11))),sF10)
| spl12_35 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f449,plain,
( mem(sK0(sK3(sF11),sK2(sK3(sF11))),sF10)
| ~ spl12_35 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f450,plain,
( spl12_34
| spl12_35
| spl12_30 ),
inference(avatar_split_clause,[],[f440,f385,f447,f443]) ).
fof(f460,plain,
! [X0,X1] :
( ~ mem(X0,X1)
| subq(s(X0),X1)
| subq(s(X0),X1) ),
inference(superposition,[],[f52,f121]) ).
fof(f461,plain,
! [X0,X1] :
( subq(s(X0),X1)
| ~ mem(X0,X1) ),
inference(duplicate_literal_removal,[],[f460]) ).
fof(f465,plain,
subq(s(e),sF5),
inference(unit_resulting_resolution,[],[f461,f162]) ).
fof(f478,plain,
! [X0] :
( ~ mem(sF6,X0)
| subq(sF7,X0) ),
inference(superposition,[],[f461,f86]) ).
fof(f479,plain,
! [X0] :
( ~ mem(sF9,X0)
| subq(sF10,X0) ),
inference(superposition,[],[f461,f92]) ).
fof(f481,plain,
subq(sF4,sF5),
inference(forward_demodulation,[],[f465,f80]) ).
fof(f488,plain,
( $false
| spl12_32 ),
inference(forward_subsumption_resolution,[],[f481,f411]) ).
fof(f489,plain,
spl12_32,
inference(avatar_contradiction_clause,[],[f488]) ).
fof(f520,plain,
( ! [X0] : subq(sF4,p(X0))
| ~ spl12_33 ),
inference(backward_demodulation,[],[f426,f415]) ).
fof(f590,plain,
! [X0,X1] :
( subq(X0,u(X1,X0))
| subq(X0,u(X1,X0)) ),
inference(resolution,[],[f133,f51]) ).
fof(f598,plain,
! [X0,X1] : subq(X0,u(X1,X0)),
inference(duplicate_literal_removal,[],[f590]) ).
fof(f599,plain,
( mem(sK0(sF11,sK3(sF11)),sF11)
| spl12_1 ),
inference(unit_resulting_resolution,[],[f51,f218]) ).
fof(f618,plain,
! [X0,X1] :
( sK0(X0,X1) = sF6
| subq(X0,X1)
| ~ subq(X0,sF7) ),
inference(resolution,[],[f184,f104]) ).
fof(f624,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF10)
| subq(X0,X1)
| ~ subq(X0,sF11)
| mem(sK0(X0,X1),sF8) ),
inference(resolution,[],[f184,f155]) ).
fof(f630,plain,
! [X0,X1] :
( subq(X0,u(X0,X1))
| subq(X0,u(X0,X1)) ),
inference(resolution,[],[f144,f51]) ).
fof(f640,plain,
! [X0,X1] : subq(X0,u(X0,X1)),
inference(duplicate_literal_removal,[],[f630]) ).
fof(f699,plain,
atleast2p(sK2(sK3(sF11))),
inference(unit_resulting_resolution,[],[f70,f207]) ).
fof(f737,plain,
( subq(sK0(sK3(sF11),sK2(sK3(sF11))),sF7)
| ~ spl12_34 ),
inference(resolution,[],[f445,f106]) ).
fof(f740,plain,
~ subq(sK2(sK3(sF11)),p(sK1(sK2(sK3(sF11))))),
inference(unit_resulting_resolution,[],[f67,f699]) ).
fof(f741,plain,
mem(sK1(sK2(sK3(sF11))),sK2(sK3(sF11))),
inference(unit_resulting_resolution,[],[f68,f699]) ).
fof(f752,plain,
( sF7 = sK0(sK3(sF11),sK2(sK3(sF11)))
| ~ subq(sF7,sK0(sK3(sF11),sK2(sK3(sF11))))
| ~ spl12_34 ),
inference(resolution,[],[f737,f53]) ).
fof(f754,definition,
( spl12_44
<=> subq(sF7,sK0(sK3(sF11),sK2(sK3(sF11)))) ),
introduced(definition,[new_symbols(definition,[spl12_44])],[avatar_definition]) ).
fof(f756,plain,
( ~ subq(sF7,sK0(sK3(sF11),sK2(sK3(sF11))))
| spl12_44 ),
inference(avatar_component_clause,[],[f754]) ).
fof(f758,definition,
( spl12_45
<=> sF7 = sK0(sK3(sF11),sK2(sK3(sF11))) ),
introduced(definition,[new_symbols(definition,[spl12_45])],[avatar_definition]) ).
fof(f760,plain,
( sF7 = sK0(sK3(sF11),sK2(sK3(sF11)))
| ~ spl12_45 ),
inference(avatar_component_clause,[],[f758]) ).
fof(f761,plain,
( ~ spl12_44
| spl12_45
| ~ spl12_34 ),
inference(avatar_split_clause,[],[f752,f443,f758,f754]) ).
fof(f763,plain,
subq(s(sK1(sK2(sK3(sF11)))),sK2(sK3(sF11))),
inference(unit_resulting_resolution,[],[f461,f741]) ).
fof(f764,plain,
mem(sK1(sK2(sK3(sF11))),sK3(sF11)),
inference(unit_resulting_resolution,[],[f50,f370,f741]) ).
fof(f769,plain,
! [X0] :
( mem(sK1(sK2(sK3(sF11))),X0)
| ~ subq(sK2(sK3(sF11)),X0) ),
inference(resolution,[],[f741,f50]) ).
fof(f770,plain,
subq(s(sK1(sK2(sK3(sF11)))),sK3(sF11)),
inference(unit_resulting_resolution,[],[f461,f764]) ).
fof(f785,definition,
( spl12_46
<=> mem(sK1(sK2(sK3(sF11))),sF8) ),
introduced(definition,[new_symbols(definition,[spl12_46])],[avatar_definition]) ).
fof(f786,plain,
( ~ mem(sK1(sK2(sK3(sF11))),sF8)
| spl12_46 ),
inference(avatar_component_clause,[],[f785]) ).
fof(f787,plain,
( mem(sK1(sK2(sK3(sF11))),sF8)
| ~ spl12_46 ),
inference(avatar_component_clause,[],[f785]) ).
fof(f800,plain,
( subq(sK1(sK2(sK3(sF11))),sF7)
| ~ spl12_46 ),
inference(resolution,[],[f787,f106]) ).
fof(f806,plain,
( sF7 = sK1(sK2(sK3(sF11)))
| ~ subq(sF7,sK1(sK2(sK3(sF11))))
| ~ spl12_46 ),
inference(resolution,[],[f800,f53]) ).
fof(f808,definition,
( spl12_48
<=> subq(sF7,sK1(sK2(sK3(sF11)))) ),
introduced(definition,[new_symbols(definition,[spl12_48])],[avatar_definition]) ).
fof(f810,plain,
( ~ subq(sF7,sK1(sK2(sK3(sF11))))
| spl12_48 ),
inference(avatar_component_clause,[],[f808]) ).
fof(f812,definition,
( spl12_49
<=> sF7 = sK1(sK2(sK3(sF11))) ),
introduced(definition,[new_symbols(definition,[spl12_49])],[avatar_definition]) ).
fof(f814,plain,
( sF7 = sK1(sK2(sK3(sF11)))
| ~ spl12_49 ),
inference(avatar_component_clause,[],[f812]) ).
fof(f815,plain,
( ~ spl12_48
| spl12_49
| ~ spl12_46 ),
inference(avatar_split_clause,[],[f806,f785,f812,f808]) ).
fof(f820,plain,
( mem(sK0(sK3(sF11),sK2(sK3(sF11))),sK3(sF11))
| spl12_30 ),
inference(unit_resulting_resolution,[],[f51,f387]) ).
fof(f821,plain,
( ~ mem(sK0(sK3(sF11),sK2(sK3(sF11))),sK2(sK3(sF11)))
| spl12_30 ),
inference(unit_resulting_resolution,[],[f52,f387]) ).
fof(f823,plain,
( subq(s(sK0(sK3(sF11),sK2(sK3(sF11)))),sK3(sF11))
| spl12_30 ),
inference(unit_resulting_resolution,[],[f461,f820]) ).
fof(f835,plain,
( ~ subq(s(sK0(sK3(sF11),sK2(sK3(sF11)))),sK2(sK3(sF11)))
| spl12_30 ),
inference(unit_resulting_resolution,[],[f50,f78,f821]) ).
fof(f866,plain,
( sF6 = sK0(sF7,sK1(sK2(sK3(sF11))))
| spl12_48 ),
inference(unit_resulting_resolution,[],[f125,f810]) ).
fof(f871,plain,
( ~ mem(sK0(sF7,sK1(sK2(sK3(sF11)))),sK1(sK2(sK3(sF11))))
| spl12_48 ),
inference(unit_resulting_resolution,[],[f52,f810]) ).
fof(f876,plain,
( ~ mem(sF6,sK1(sK2(sK3(sF11))))
| spl12_48 ),
inference(forward_demodulation,[],[f871,f866]) ).
fof(f945,plain,
( sF6 = sK0(sF7,sK0(sK3(sF11),sK2(sK3(sF11))))
| spl12_44 ),
inference(unit_resulting_resolution,[],[f125,f756]) ).
fof(f950,plain,
( ~ mem(sK0(sF7,sK0(sK3(sF11),sK2(sK3(sF11)))),sK0(sK3(sF11),sK2(sK3(sF11))))
| spl12_44 ),
inference(unit_resulting_resolution,[],[f52,f756]) ).
fof(f955,plain,
( ~ mem(sF6,sK0(sK3(sF11),sK2(sK3(sF11))))
| spl12_44 ),
inference(forward_demodulation,[],[f950,f945]) ).
fof(f964,plain,
( ~ subq(sK2(sK3(sF11)),sF4)
| e = sK1(sK2(sK3(sF11))) ),
inference(resolution,[],[f769,f102]) ).
fof(f969,plain,
( ~ subq(sK2(sK3(sF11)),sF8)
| subq(sK1(sK2(sK3(sF11))),sF7) ),
inference(resolution,[],[f769,f106]) ).
fof(f973,plain,
( ~ subq(sK2(sK3(sF11)),sF10)
| sF9 = sK1(sK2(sK3(sF11))) ),
inference(resolution,[],[f769,f105]) ).
fof(f976,definition,
( spl12_54
<=> sF9 = sK1(sK2(sK3(sF11))) ),
introduced(definition,[new_symbols(definition,[spl12_54])],[avatar_definition]) ).
fof(f978,plain,
( sF9 = sK1(sK2(sK3(sF11)))
| ~ spl12_54 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f980,definition,
( spl12_55
<=> subq(sK2(sK3(sF11)),sF10) ),
introduced(definition,[new_symbols(definition,[spl12_55])],[avatar_definition]) ).
fof(f981,plain,
( subq(sK2(sK3(sF11)),sF10)
| ~ spl12_55 ),
inference(avatar_component_clause,[],[f980]) ).
fof(f982,plain,
( ~ subq(sK2(sK3(sF11)),sF10)
| spl12_55 ),
inference(avatar_component_clause,[],[f980]) ).
fof(f983,plain,
( spl12_54
| ~ spl12_55 ),
inference(avatar_split_clause,[],[f973,f980,f976]) ).
fof(f1022,definition,
( spl12_64
<=> e = sK1(sK2(sK3(sF11))) ),
introduced(definition,[new_symbols(definition,[spl12_64])],[avatar_definition]) ).
fof(f1023,plain,
( e != sK1(sK2(sK3(sF11)))
| spl12_64 ),
inference(avatar_component_clause,[],[f1022]) ).
fof(f1024,plain,
( e = sK1(sK2(sK3(sF11)))
| ~ spl12_64 ),
inference(avatar_component_clause,[],[f1022]) ).
fof(f1026,definition,
( spl12_65
<=> subq(sK2(sK3(sF11)),sF4) ),
introduced(definition,[new_symbols(definition,[spl12_65])],[avatar_definition]) ).
fof(f1027,plain,
( subq(sK2(sK3(sF11)),sF4)
| ~ spl12_65 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1028,plain,
( ~ subq(sK2(sK3(sF11)),sF4)
| spl12_65 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1029,plain,
( spl12_64
| ~ spl12_65 ),
inference(avatar_split_clause,[],[f964,f1026,f1022]) ).
fof(f1043,plain,
( mem(sK0(sK2(sK3(sF11)),sF10),sK3(sF11))
| spl12_55 ),
inference(unit_resulting_resolution,[],[f184,f370,f982]) ).
fof(f1047,plain,
( ~ mem(sK0(sK2(sK3(sF11)),sF10),sF10)
| spl12_55 ),
inference(unit_resulting_resolution,[],[f52,f982]) ).
fof(f1049,plain,
( mem(sK0(sK2(sK3(sF11)),sF4),sK3(sF11))
| spl12_65 ),
inference(unit_resulting_resolution,[],[f184,f370,f1028]) ).
fof(f1231,plain,
( mem(sK0(sK2(sK3(sF11)),sF4),sF11)
| spl12_65 ),
inference(unit_resulting_resolution,[],[f50,f137,f1049]) ).
fof(f1306,plain,
( mem(sK0(sK2(sK3(sF11)),sF4),sF10)
| mem(sK0(sK2(sK3(sF11)),sF4),sF8)
| spl12_65 ),
inference(resolution,[],[f1231,f155]) ).
fof(f1309,definition,
( spl12_72
<=> mem(sK0(sK2(sK3(sF11)),sF4),sF8) ),
introduced(definition,[new_symbols(definition,[spl12_72])],[avatar_definition]) ).
fof(f1311,plain,
( mem(sK0(sK2(sK3(sF11)),sF4),sF8)
| ~ spl12_72 ),
inference(avatar_component_clause,[],[f1309]) ).
fof(f1313,definition,
( spl12_73
<=> mem(sK0(sK2(sK3(sF11)),sF4),sF10) ),
introduced(definition,[new_symbols(definition,[spl12_73])],[avatar_definition]) ).
fof(f1315,plain,
( mem(sK0(sK2(sK3(sF11)),sF4),sF10)
| ~ spl12_73 ),
inference(avatar_component_clause,[],[f1313]) ).
fof(f1316,plain,
( spl12_72
| spl12_73
| spl12_65 ),
inference(avatar_split_clause,[],[f1306,f1026,f1313,f1309]) ).
fof(f1317,plain,
( ~ subq(sK2(sK3(sF11)),p(e))
| ~ spl12_64 ),
inference(backward_demodulation,[],[f740,f1024]) ).
fof(f1319,plain,
( subq(s(e),sK2(sK3(sF11)))
| ~ spl12_64 ),
inference(backward_demodulation,[],[f763,f1024]) ).
fof(f1324,plain,
( subq(s(e),sK3(sF11))
| ~ spl12_64 ),
inference(backward_demodulation,[],[f770,f1024]) ).
fof(f1364,plain,
( subq(sF4,sK3(sF11))
| ~ spl12_64 ),
inference(forward_demodulation,[],[f1324,f80]) ).
fof(f1365,plain,
( subq(sF4,sK2(sK3(sF11)))
| ~ spl12_64 ),
inference(forward_demodulation,[],[f1319,f80]) ).
fof(f1377,plain,
( sF4 = sK2(sK3(sF11))
| ~ subq(sF4,sK2(sK3(sF11)))
| ~ spl12_65 ),
inference(resolution,[],[f1027,f53]) ).
fof(f1378,plain,
( sF4 = sK2(sK3(sF11))
| ~ spl12_64
| ~ spl12_65 ),
inference(forward_subsumption_resolution,[],[f1377,f1365]) ).
fof(f1498,plain,
( ~ subq(sF4,p(e))
| ~ spl12_64
| ~ spl12_65 ),
inference(backward_demodulation,[],[f1317,f1378]) ).
fof(f1528,plain,
( $false
| ~ spl12_33
| ~ spl12_64
| ~ spl12_65 ),
inference(forward_subsumption_resolution,[],[f1498,f520]) ).
fof(f1529,plain,
( ~ spl12_33
| ~ spl12_64
| ~ spl12_65 ),
inference(avatar_contradiction_clause,[],[f1528]) ).
fof(f1618,plain,
( subq(sK0(sK2(sK3(sF11)),sF4),sF7)
| ~ spl12_72 ),
inference(resolution,[],[f1311,f106]) ).
fof(f1632,plain,
( sF7 = sK0(sK2(sK3(sF11)),sF4)
| ~ subq(sF7,sK0(sK2(sK3(sF11)),sF4))
| ~ spl12_72 ),
inference(resolution,[],[f1618,f53]) ).
fof(f1634,definition,
( spl12_74
<=> subq(sF7,sK0(sK2(sK3(sF11)),sF4)) ),
introduced(definition,[new_symbols(definition,[spl12_74])],[avatar_definition]) ).
fof(f1636,plain,
( ~ subq(sF7,sK0(sK2(sK3(sF11)),sF4))
| spl12_74 ),
inference(avatar_component_clause,[],[f1634]) ).
fof(f1638,definition,
( spl12_75
<=> sF7 = sK0(sK2(sK3(sF11)),sF4) ),
introduced(definition,[new_symbols(definition,[spl12_75])],[avatar_definition]) ).
fof(f1640,plain,
( sF7 = sK0(sK2(sK3(sF11)),sF4)
| ~ spl12_75 ),
inference(avatar_component_clause,[],[f1638]) ).
fof(f1641,plain,
( ~ spl12_74
| spl12_75
| ~ spl12_72 ),
inference(avatar_split_clause,[],[f1632,f1309,f1638,f1634]) ).
fof(f1753,plain,
( ! [X0] : mem(sK0(sK2(sK3(sF11)),sF4),u(sK2(sK3(sF11)),X0))
| spl12_65 ),
inference(unit_resulting_resolution,[],[f184,f640,f1028]) ).
fof(f1755,plain,
( mem(sK0(sK2(sK3(sF11)),sF4),sK2(sK3(sF11)))
| spl12_65 ),
inference(unit_resulting_resolution,[],[f51,f1028]) ).
fof(f1756,plain,
( ~ mem(sK0(sK2(sK3(sF11)),sF4),sF4)
| spl12_65 ),
inference(unit_resulting_resolution,[],[f52,f1028]) ).
fof(f1758,plain,
( subq(s(sK0(sK2(sK3(sF11)),sF4)),sK2(sK3(sF11)))
| spl12_65 ),
inference(unit_resulting_resolution,[],[f461,f1755]) ).
fof(f1884,plain,
( mem(sK0(sK2(sK3(sF11)),sF10),sF11)
| spl12_55 ),
inference(unit_resulting_resolution,[],[f50,f137,f1043]) ).
fof(f1925,plain,
( mem(sK0(sK2(sK3(sF11)),sF10),sF10)
| mem(sK0(sK2(sK3(sF11)),sF10),sF8)
| spl12_55 ),
inference(resolution,[],[f1884,f155]) ).
fof(f1927,plain,
( mem(sK0(sK2(sK3(sF11)),sF10),sF8)
| spl12_55 ),
inference(forward_subsumption_resolution,[],[f1925,f1047]) ).
fof(f1936,plain,
( subq(sK0(sK2(sK3(sF11)),sF10),sF7)
| spl12_55 ),
inference(resolution,[],[f1927,f106]) ).
fof(f1942,plain,
( sF7 = sK0(sK2(sK3(sF11)),sF10)
| ~ subq(sF7,sK0(sK2(sK3(sF11)),sF10))
| spl12_55 ),
inference(resolution,[],[f1936,f53]) ).
fof(f1944,definition,
( spl12_78
<=> subq(sF7,sK0(sK2(sK3(sF11)),sF10)) ),
introduced(definition,[new_symbols(definition,[spl12_78])],[avatar_definition]) ).
fof(f1946,plain,
( ~ subq(sF7,sK0(sK2(sK3(sF11)),sF10))
| spl12_78 ),
inference(avatar_component_clause,[],[f1944]) ).
fof(f1948,definition,
( spl12_79
<=> sF7 = sK0(sK2(sK3(sF11)),sF10) ),
introduced(definition,[new_symbols(definition,[spl12_79])],[avatar_definition]) ).
fof(f1950,plain,
( sF7 = sK0(sK2(sK3(sF11)),sF10)
| ~ spl12_79 ),
inference(avatar_component_clause,[],[f1948]) ).
fof(f1951,plain,
( ~ spl12_78
| spl12_79
| spl12_55 ),
inference(avatar_split_clause,[],[f1942,f980,f1948,f1944]) ).
fof(f3626,plain,
! [X0] : mem(X0,p(X0)),
inference(unit_resulting_resolution,[],[f66,f127]) ).
fof(f3684,plain,
( mem(sK0(sF11,sK3(sF11)),sF10)
| mem(sK0(sF11,sK3(sF11)),sF8)
| spl12_1 ),
inference(resolution,[],[f599,f155]) ).
fof(f3687,definition,
( spl12_88
<=> mem(sK0(sF11,sK3(sF11)),sF8) ),
introduced(definition,[new_symbols(definition,[spl12_88])],[avatar_definition]) ).
fof(f3689,plain,
( mem(sK0(sF11,sK3(sF11)),sF8)
| ~ spl12_88 ),
inference(avatar_component_clause,[],[f3687]) ).
fof(f3691,definition,
( spl12_89
<=> mem(sK0(sF11,sK3(sF11)),sF10) ),
introduced(definition,[new_symbols(definition,[spl12_89])],[avatar_definition]) ).
fof(f3693,plain,
( mem(sK0(sF11,sK3(sF11)),sF10)
| ~ spl12_89 ),
inference(avatar_component_clause,[],[f3691]) ).
fof(f3694,plain,
( spl12_88
| spl12_89
| spl12_1 ),
inference(avatar_split_clause,[],[f3684,f216,f3691,f3687]) ).
fof(f3935,plain,
( ~ subq(sF11,sF11)
| ~ spl12_2 ),
inference(forward_demodulation,[],[f361,f222]) ).
fof(f3952,plain,
( $false
| ~ spl12_2 ),
inference(forward_subsumption_resolution,[],[f3935,f127]) ).
fof(f3953,plain,
~ spl12_2,
inference(avatar_contradiction_clause,[],[f3952]) ).
fof(f3981,plain,
~ subq(sK3(sF11),sK2(sK3(sF11))),
inference(unit_resulting_resolution,[],[f69,f207]) ).
fof(f4233,plain,
( ~ mem(sK0(sF11,sK3(sF11)),sK3(sF11))
| spl12_1 ),
inference(unit_resulting_resolution,[],[f52,f218]) ).
fof(f4385,plain,
( subq(sK0(sF11,sK3(sF11)),sF7)
| ~ spl12_88 ),
inference(resolution,[],[f3689,f106]) ).
fof(f4402,plain,
( sF7 = sK0(sF11,sK3(sF11))
| ~ subq(sF7,sK0(sF11,sK3(sF11)))
| ~ spl12_88 ),
inference(resolution,[],[f4385,f53]) ).
fof(f4404,definition,
( spl12_90
<=> subq(sF7,sK0(sF11,sK3(sF11))) ),
introduced(definition,[new_symbols(definition,[spl12_90])],[avatar_definition]) ).
fof(f4406,plain,
( ~ subq(sF7,sK0(sF11,sK3(sF11)))
| spl12_90 ),
inference(avatar_component_clause,[],[f4404]) ).
fof(f4408,definition,
( spl12_91
<=> sF7 = sK0(sF11,sK3(sF11)) ),
introduced(definition,[new_symbols(definition,[spl12_91])],[avatar_definition]) ).
fof(f4410,plain,
( sF7 = sK0(sF11,sK3(sF11))
| ~ spl12_91 ),
inference(avatar_component_clause,[],[f4408]) ).
fof(f4411,plain,
( ~ spl12_90
| spl12_91
| ~ spl12_88 ),
inference(avatar_split_clause,[],[f4402,f3687,f4408,f4404]) ).
fof(f4545,plain,
( sF6 = sK0(sF7,sK0(sK2(sK3(sF11)),sF4))
| spl12_74 ),
inference(unit_resulting_resolution,[],[f125,f1636]) ).
fof(f4552,plain,
( ~ mem(sK0(sF7,sK0(sK2(sK3(sF11)),sF4)),sK0(sK2(sK3(sF11)),sF4))
| spl12_74 ),
inference(unit_resulting_resolution,[],[f52,f1636]) ).
fof(f4559,plain,
( ~ mem(sF6,sK0(sK2(sK3(sF11)),sF4))
| spl12_74 ),
inference(forward_demodulation,[],[f4552,f4545]) ).
fof(f4708,plain,
( ~ subq(s(sK0(sF11,sK3(sF11))),sK3(sF11))
| spl12_1 ),
inference(unit_resulting_resolution,[],[f178,f4233]) ).
fof(f4711,plain,
( ~ mem(sK0(sF11,sK3(sF11)),sK2(sK3(sF11)))
| spl12_1 ),
inference(unit_resulting_resolution,[],[f50,f370,f4233]) ).
fof(f4736,plain,
( ~ mem(sK0(sF11,sK3(sF11)),u(e,sK2(sK3(sF11))))
| spl12_1 ),
inference(unit_resulting_resolution,[],[f57,f54,f4711]) ).
fof(f5134,definition,
( spl12_114
<=> mem(sF6,sK0(sF11,sK3(sF11))) ),
introduced(definition,[new_symbols(definition,[spl12_114])],[avatar_definition]) ).
fof(f5136,plain,
( mem(sF6,sK0(sF11,sK3(sF11)))
| ~ spl12_114 ),
inference(avatar_component_clause,[],[f5134]) ).
fof(f5143,definition,
( spl12_116
<=> mem(sF6,sK0(sK2(sK3(sF11)),sF10)) ),
introduced(definition,[new_symbols(definition,[spl12_116])],[avatar_definition]) ).
fof(f5145,plain,
( mem(sF6,sK0(sK2(sK3(sF11)),sF10))
| ~ spl12_116 ),
inference(avatar_component_clause,[],[f5143]) ).
fof(f5177,plain,
subq(sF10,p(sF9)),
inference(resolution,[],[f479,f3626]) ).
fof(f6796,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF8)
| ~ subq(X0,sF11)
| subq(X0,X1)
| sK0(X0,X1) = sF9 ),
inference(resolution,[],[f624,f105]) ).
fof(f6825,plain,
! [X0] :
( ~ subq(X0,sF11)
| subq(X0,sF8)
| sF9 = sK0(X0,sF8)
| subq(X0,sF8) ),
inference(resolution,[],[f6796,f52]) ).
fof(f6839,plain,
! [X0] :
( sF9 = sK0(X0,sF8)
| subq(X0,sF8)
| ~ subq(X0,sF11) ),
inference(duplicate_literal_removal,[],[f6825]) ).
fof(f6854,plain,
( ~ subq(s(sK0(sK2(sK3(sF11)),sF4)),sF4)
| spl12_65 ),
inference(unit_resulting_resolution,[],[f178,f1756]) ).
fof(f8282,definition,
( spl12_139
<=> mem(sF9,sK2(sK3(sF11))) ),
introduced(definition,[new_symbols(definition,[spl12_139])],[avatar_definition]) ).
fof(f8283,plain,
( mem(sF9,sK2(sK3(sF11)))
| ~ spl12_139 ),
inference(avatar_component_clause,[],[f8282]) ).
fof(f8284,plain,
( ~ mem(sF9,sK2(sK3(sF11)))
| spl12_139 ),
inference(avatar_component_clause,[],[f8282]) ).
fof(f8503,plain,
! [X0,X1] :
( mem(sF6,X0)
| subq(X0,X1)
| subq(X0,X1)
| ~ subq(X0,sF7) ),
inference(superposition,[],[f51,f618]) ).
fof(f8589,plain,
! [X0,X1] :
( ~ subq(X0,sF7)
| subq(X0,X1)
| mem(sF6,X0) ),
inference(duplicate_literal_removal,[],[f8503]) ).
fof(f8629,plain,
( ! [X0] : subq(sK0(sK3(sF11),sK2(sK3(sF11))),X0)
| ~ spl12_34
| spl12_44 ),
inference(unit_resulting_resolution,[],[f8589,f955,f737]) ).
fof(f8633,plain,
( ! [X0] :
( subq(sK0(sK2(sK3(sF11)),sF4),X0)
| mem(sF6,sK0(sK2(sK3(sF11)),sF4)) )
| ~ spl12_72 ),
inference(resolution,[],[f8589,f1618]) ).
fof(f8637,plain,
( ! [X0] :
( subq(sK0(sK2(sK3(sF11)),sF10),X0)
| mem(sF6,sK0(sK2(sK3(sF11)),sF10)) )
| spl12_55 ),
inference(resolution,[],[f8589,f1936]) ).
fof(f8639,plain,
( ! [X0] :
( subq(sK0(sF11,sK3(sF11)),X0)
| mem(sF6,sK0(sF11,sK3(sF11))) )
| ~ spl12_88 ),
inference(resolution,[],[f8589,f4385]) ).
fof(f8648,definition,
( spl12_153
<=> ! [X0] : subq(sK0(sF11,sK3(sF11)),X0) ),
introduced(definition,[new_symbols(definition,[spl12_153])],[avatar_definition]) ).
fof(f8649,plain,
( ! [X0] : subq(sK0(sF11,sK3(sF11)),X0)
| ~ spl12_153 ),
inference(avatar_component_clause,[],[f8648]) ).
fof(f8650,plain,
( spl12_114
| spl12_153
| ~ spl12_88 ),
inference(avatar_split_clause,[],[f8639,f3687,f8648,f5134]) ).
fof(f8653,definition,
( spl12_154
<=> ! [X0] : subq(sK0(sK2(sK3(sF11)),sF10),X0) ),
introduced(definition,[new_symbols(definition,[spl12_154])],[avatar_definition]) ).
fof(f8654,plain,
( ! [X0] : subq(sK0(sK2(sK3(sF11)),sF10),X0)
| ~ spl12_154 ),
inference(avatar_component_clause,[],[f8653]) ).
fof(f8655,plain,
( spl12_116
| spl12_154
| spl12_55 ),
inference(avatar_split_clause,[],[f8637,f980,f8653,f5143]) ).
fof(f8659,plain,
( ! [X0] : subq(sK0(sK2(sK3(sF11)),sF4),X0)
| ~ spl12_72
| spl12_74 ),
inference(forward_subsumption_resolution,[],[f8633,f4559]) ).
fof(f8697,plain,
( sF9 = sK0(sF11,sK3(sF11))
| ~ spl12_89 ),
inference(resolution,[],[f3693,f105]) ).
fof(f8706,plain,
( ~ mem(sF9,sK3(sF11))
| spl12_1
| ~ spl12_89 ),
inference(backward_demodulation,[],[f4233,f8697]) ).
fof(f8876,plain,
( ~ mem(sF9,sK2(sK3(sF11)))
| spl12_1
| ~ spl12_89 ),
inference(unit_resulting_resolution,[],[f50,f370,f8706]) ).
fof(f9011,plain,
( subq(sF7,sK0(sK2(sK3(sF11)),sF10))
| ~ spl12_116 ),
inference(resolution,[],[f5145,f478]) ).
fof(f9015,plain,
( $false
| spl12_78
| ~ spl12_116 ),
inference(forward_subsumption_resolution,[],[f9011,f1946]) ).
fof(f9016,plain,
( spl12_78
| ~ spl12_116 ),
inference(avatar_contradiction_clause,[],[f9015]) ).
fof(f9022,plain,
( mem(sF7,sK3(sF11))
| spl12_55
| ~ spl12_79 ),
inference(backward_demodulation,[],[f1043,f1950]) ).
fof(f9209,plain,
( e = sK0(sK2(sK3(sF11)),sF4)
| ~ spl12_72
| spl12_74 ),
inference(resolution,[],[f8659,f212]) ).
fof(f9254,plain,
( ~ subq(s(e),sF4)
| spl12_65
| ~ spl12_72
| spl12_74 ),
inference(backward_demodulation,[],[f6854,f9209]) ).
fof(f9368,plain,
( ~ subq(sF4,sF4)
| spl12_65
| ~ spl12_72
| spl12_74 ),
inference(forward_demodulation,[],[f9254,f80]) ).
fof(f9376,plain,
( $false
| spl12_65
| ~ spl12_72
| spl12_74 ),
inference(forward_subsumption_resolution,[],[f9368,f127]) ).
fof(f9377,plain,
( spl12_65
| ~ spl12_72
| spl12_74 ),
inference(avatar_contradiction_clause,[],[f9376]) ).
fof(f9394,plain,
( sF9 = sK0(sK2(sK3(sF11)),sF4)
| ~ spl12_73 ),
inference(resolution,[],[f1315,f105]) ).
fof(f9406,plain,
( subq(s(sF9),sK2(sK3(sF11)))
| spl12_65
| ~ spl12_73 ),
inference(backward_demodulation,[],[f1758,f9394]) ).
fof(f9498,plain,
( subq(sF10,sK2(sK3(sF11)))
| spl12_65
| ~ spl12_73 ),
inference(forward_demodulation,[],[f9406,f92]) ).
fof(f9519,plain,
( ~ mem(sK0(sK3(sF11),sK2(sK3(sF11))),sF10)
| spl12_30
| spl12_65
| ~ spl12_73 ),
inference(unit_resulting_resolution,[],[f50,f821,f9498]) ).
fof(f9524,plain,
( sF10 = sK2(sK3(sF11))
| ~ subq(sK2(sK3(sF11)),sF10)
| spl12_65
| ~ spl12_73 ),
inference(resolution,[],[f9498,f53]) ).
fof(f9525,plain,
( ~ spl12_35
| spl12_30
| spl12_65
| ~ spl12_73 ),
inference(avatar_split_clause,[],[f9519,f1313,f1026,f385,f447]) ).
fof(f9549,plain,
( ~ mem(sK0(sK3(sF11),sK2(sK3(sF11))),u(sK2(sK3(sF11)),sF10))
| spl12_30
| spl12_35 ),
inference(unit_resulting_resolution,[],[f57,f821,f448]) ).
fof(f9736,plain,
( ~ mem(sK0(sF11,sK3(sF11)),sF10)
| spl12_1
| spl12_65
| ~ spl12_73 ),
inference(unit_resulting_resolution,[],[f50,f9498,f4711]) ).
fof(f10263,plain,
( e = sK0(sF11,sK3(sF11))
| ~ spl12_153 ),
inference(resolution,[],[f8649,f212]) ).
fof(f10287,plain,
( ~ subq(s(e),sK3(sF11))
| spl12_1
| ~ spl12_153 ),
inference(backward_demodulation,[],[f4708,f10263]) ).
fof(f10484,plain,
( ~ subq(sF4,sK3(sF11))
| spl12_1
| ~ spl12_153 ),
inference(forward_demodulation,[],[f10287,f80]) ).
fof(f10490,plain,
( $false
| spl12_1
| ~ spl12_64
| ~ spl12_153 ),
inference(forward_subsumption_resolution,[],[f10484,f1364]) ).
fof(f10491,plain,
( spl12_1
| ~ spl12_64
| ~ spl12_153 ),
inference(avatar_contradiction_clause,[],[f10490]) ).
fof(f10552,plain,
( subq(s(sF6),sK0(sF11,sK3(sF11)))
| ~ spl12_114 ),
inference(unit_resulting_resolution,[],[f461,f5136]) ).
fof(f10571,plain,
( subq(sF7,sK0(sF11,sK3(sF11)))
| ~ spl12_114 ),
inference(resolution,[],[f5136,f478]) ).
fof(f10575,plain,
( $false
| spl12_90
| ~ spl12_114 ),
inference(forward_subsumption_resolution,[],[f10571,f4406]) ).
fof(f10576,plain,
( spl12_90
| ~ spl12_114 ),
inference(avatar_contradiction_clause,[],[f10575]) ).
fof(f10579,plain,
( subq(sF7,sK0(sF11,sK3(sF11)))
| ~ spl12_114 ),
inference(forward_demodulation,[],[f10552,f86]) ).
fof(f10580,plain,
( $false
| spl12_90
| ~ spl12_114 ),
inference(forward_subsumption_resolution,[],[f10579,f4406]) ).
fof(f10581,plain,
( spl12_90
| ~ spl12_114 ),
inference(avatar_contradiction_clause,[],[f10580]) ).
fof(f10586,plain,
( ~ mem(sF7,sK3(sF11))
| spl12_1
| ~ spl12_91 ),
inference(backward_demodulation,[],[f4233,f4410]) ).
fof(f10590,plain,
( ~ subq(s(sF7),sK3(sF11))
| spl12_1
| ~ spl12_91 ),
inference(backward_demodulation,[],[f4708,f4410]) ).
fof(f10591,plain,
( ~ mem(sF7,sK2(sK3(sF11)))
| spl12_1
| ~ spl12_91 ),
inference(backward_demodulation,[],[f4711,f4410]) ).
fof(f10769,plain,
( $false
| spl12_1
| spl12_55
| ~ spl12_79
| ~ spl12_91 ),
inference(forward_subsumption_resolution,[],[f10586,f9022]) ).
fof(f10770,plain,
( spl12_1
| spl12_55
| ~ spl12_79
| ~ spl12_91 ),
inference(avatar_contradiction_clause,[],[f10769]) ).
fof(f10796,plain,
( sF10 = sK2(sK3(sF11))
| ~ spl12_55
| spl12_65
| ~ spl12_73 ),
inference(forward_subsumption_resolution,[],[f9524,f981]) ).
fof(f12298,plain,
( ! [X0] : mem(sK0(sK2(sK3(sF11)),sF10),u(X0,sK2(sK3(sF11))))
| spl12_55 ),
inference(unit_resulting_resolution,[],[f184,f598,f982]) ).
fof(f12325,plain,
( mem(sK0(sK2(sK3(sF11)),sF4),sK2(sK3(sF11)))
| spl12_65 ),
inference(unit_resulting_resolution,[],[f184,f127,f1028]) ).
fof(f12983,plain,
( e = sK0(sK2(sK3(sF11)),sF10)
| ~ spl12_154 ),
inference(resolution,[],[f8654,f212]) ).
fof(f13007,plain,
( ! [X0] : mem(e,u(X0,sK2(sK3(sF11))))
| spl12_55
| ~ spl12_154 ),
inference(backward_demodulation,[],[f12298,f12983]) ).
fof(f13071,plain,
( mem(e,sK2(sK3(sF11)))
| subq(sK2(sK3(sF11)),sF10)
| ~ spl12_154 ),
inference(superposition,[],[f51,f12983]) ).
fof(f14327,plain,
! [X0] :
( mem(sF9,X0)
| subq(X0,sF8)
| subq(X0,sF8)
| ~ subq(X0,sF11) ),
inference(superposition,[],[f51,f6839]) ).
fof(f14344,plain,
! [X0] :
( ~ subq(X0,sF11)
| subq(X0,sF8)
| mem(sF9,X0) ),
inference(duplicate_literal_removal,[],[f14327]) ).
fof(f15844,plain,
( e = sK0(sK3(sF11),sK2(sK3(sF11)))
| ~ spl12_34
| spl12_44 ),
inference(resolution,[],[f8629,f212]) ).
fof(f15876,plain,
( ~ mem(e,sK2(sK3(sF11)))
| spl12_30
| ~ spl12_34
| spl12_44 ),
inference(backward_demodulation,[],[f821,f15844]) ).
fof(f15877,plain,
( subq(s(e),sK3(sF11))
| spl12_30
| ~ spl12_34
| spl12_44 ),
inference(backward_demodulation,[],[f823,f15844]) ).
fof(f15880,plain,
( ~ subq(s(e),sK2(sK3(sF11)))
| spl12_30
| ~ spl12_34
| spl12_44 ),
inference(backward_demodulation,[],[f835,f15844]) ).
fof(f16180,plain,
( ~ subq(sF4,sK2(sK3(sF11)))
| spl12_30
| ~ spl12_34
| spl12_44 ),
inference(forward_demodulation,[],[f15880,f80]) ).
fof(f16181,plain,
( subq(sF4,sK3(sF11))
| spl12_30
| ~ spl12_34
| spl12_44 ),
inference(forward_demodulation,[],[f15877,f80]) ).
fof(f16191,plain,
( $false
| spl12_30
| ~ spl12_34
| spl12_44
| ~ spl12_64 ),
inference(forward_subsumption_resolution,[],[f16180,f1365]) ).
fof(f16192,plain,
( spl12_30
| ~ spl12_34
| spl12_44
| ~ spl12_64 ),
inference(avatar_contradiction_clause,[],[f16191]) ).
fof(f16219,plain,
( ~ mem(sF7,sK2(sK3(sF11)))
| spl12_30
| ~ spl12_45 ),
inference(forward_demodulation,[],[f821,f760]) ).
fof(f16220,plain,
( subq(s(sF7),sK3(sF11))
| spl12_30
| ~ spl12_45 ),
inference(forward_demodulation,[],[f823,f760]) ).
fof(f16297,plain,
( ~ mem(sF7,u(sK2(sK3(sF11)),sF10))
| spl12_30
| spl12_35
| ~ spl12_45 ),
inference(forward_demodulation,[],[f9549,f760]) ).
fof(f16350,plain,
( $false
| spl12_1
| spl12_30
| ~ spl12_45
| ~ spl12_91 ),
inference(forward_subsumption_resolution,[],[f16220,f10590]) ).
fof(f16351,plain,
( spl12_1
| spl12_30
| ~ spl12_45
| ~ spl12_91 ),
inference(avatar_contradiction_clause,[],[f16350]) ).
fof(f17032,plain,
( ~ subq(sK3(sF11),sK3(sF11))
| ~ spl12_31 ),
inference(forward_demodulation,[],[f3981,f391]) ).
fof(f17182,plain,
( $false
| ~ spl12_31 ),
inference(forward_subsumption_resolution,[],[f17032,f127]) ).
fof(f17183,plain,
~ spl12_31,
inference(avatar_contradiction_clause,[],[f17182]) ).
fof(f17232,plain,
( ! [X0] : mem(sF7,u(sK2(sK3(sF11)),X0))
| spl12_65
| ~ spl12_75 ),
inference(forward_demodulation,[],[f1753,f1640]) ).
fof(f17297,plain,
( mem(sF7,sK2(sK3(sF11)))
| spl12_65
| ~ spl12_75 ),
inference(forward_demodulation,[],[f12325,f1640]) ).
fof(f17337,plain,
( $false
| spl12_1
| spl12_65
| ~ spl12_75
| ~ spl12_91 ),
inference(forward_subsumption_resolution,[],[f17297,f10591]) ).
fof(f17338,plain,
( spl12_1
| spl12_65
| ~ spl12_75
| ~ spl12_91 ),
inference(avatar_contradiction_clause,[],[f17337]) ).
fof(f17631,definition,
( spl12_170
<=> mem(sF9,sK3(sF11)) ),
introduced(definition,[new_symbols(definition,[spl12_170])],[avatar_definition]) ).
fof(f17632,plain,
( ~ mem(sF9,sK3(sF11))
| spl12_170 ),
inference(avatar_component_clause,[],[f17631]) ).
fof(f17639,plain,
( ~ spl12_170
| spl12_1
| ~ spl12_89 ),
inference(avatar_split_clause,[],[f8706,f3691,f216,f17631]) ).
fof(f17730,plain,
( sF9 = sK0(sK3(sF11),sK2(sK3(sF11)))
| ~ spl12_35 ),
inference(resolution,[],[f449,f105]) ).
fof(f17763,plain,
( mem(sF9,sK3(sF11))
| subq(sK3(sF11),sK2(sK3(sF11)))
| ~ spl12_35 ),
inference(superposition,[],[f51,f17730]) ).
fof(f17769,plain,
( subq(sK3(sF11),sK2(sK3(sF11)))
| ~ spl12_35
| spl12_170 ),
inference(forward_subsumption_resolution,[],[f17763,f17632]) ).
fof(f17771,plain,
( $false
| spl12_30
| ~ spl12_35
| spl12_170 ),
inference(forward_subsumption_resolution,[],[f17769,f387]) ).
fof(f17772,plain,
( spl12_30
| ~ spl12_35
| spl12_170 ),
inference(avatar_contradiction_clause,[],[f17771]) ).
fof(f17775,plain,
( $false
| spl12_30
| spl12_35
| ~ spl12_45
| spl12_65
| ~ spl12_75 ),
inference(forward_subsumption_resolution,[],[f16297,f17232]) ).
fof(f17776,plain,
( spl12_30
| spl12_35
| ~ spl12_45
| spl12_65
| ~ spl12_75 ),
inference(avatar_contradiction_clause,[],[f17775]) ).
fof(f17833,plain,
( subq(sK2(sK3(sF11)),sF10)
| spl12_30
| ~ spl12_34
| spl12_44
| ~ spl12_154 ),
inference(forward_subsumption_resolution,[],[f13071,f15876]) ).
fof(f17854,plain,
( $false
| spl12_30
| ~ spl12_34
| spl12_44
| spl12_55
| ~ spl12_154 ),
inference(forward_subsumption_resolution,[],[f17833,f982]) ).
fof(f17855,plain,
( spl12_30
| ~ spl12_34
| spl12_44
| spl12_55
| ~ spl12_154 ),
inference(avatar_contradiction_clause,[],[f17854]) ).
fof(f17858,plain,
( ~ subq(sK2(sK3(sF11)),p(sF9))
| ~ spl12_54 ),
inference(backward_demodulation,[],[f740,f978]) ).
fof(f18958,plain,
( ~ subq(s(e),sK3(sF11))
| spl12_1
| ~ spl12_153 ),
inference(forward_demodulation,[],[f4708,f10263]) ).
fof(f19584,plain,
( ~ subq(sF4,sK3(sF11))
| spl12_1
| ~ spl12_153 ),
inference(forward_demodulation,[],[f18958,f80]) ).
fof(f19820,definition,
( spl12_177
<=> subq(sK2(sK3(sF11)),sF8) ),
introduced(definition,[new_symbols(definition,[spl12_177])],[avatar_definition]) ).
fof(f19821,plain,
( subq(sK2(sK3(sF11)),sF8)
| ~ spl12_177 ),
inference(avatar_component_clause,[],[f19820]) ).
fof(f19822,plain,
( ~ subq(sK2(sK3(sF11)),sF8)
| spl12_177 ),
inference(avatar_component_clause,[],[f19820]) ).
fof(f19932,plain,
( $false
| spl12_1
| spl12_30
| ~ spl12_34
| spl12_44
| ~ spl12_153 ),
inference(forward_subsumption_resolution,[],[f19584,f16181]) ).
fof(f19933,plain,
( spl12_1
| spl12_30
| ~ spl12_34
| spl12_44
| ~ spl12_153 ),
inference(avatar_contradiction_clause,[],[f19932]) ).
fof(f20096,plain,
( ~ spl12_139
| spl12_1
| ~ spl12_89 ),
inference(avatar_split_clause,[],[f8876,f3691,f216,f8282]) ).
fof(f22010,plain,
( ~ mem(sK0(sK3(sF11),sK2(sK3(sF11))),sK2(sK3(sF11)))
| spl12_30 ),
inference(unit_resulting_resolution,[],[f52,f387]) ).
fof(f23352,plain,
( mem(sK1(sK2(sK3(sF11))),sF8)
| ~ spl12_177 ),
inference(unit_resulting_resolution,[],[f226,f699,f19821]) ).
fof(f24786,plain,
( subq(sK1(sK2(sK3(sF11))),sF7)
| ~ spl12_177 ),
inference(forward_subsumption_resolution,[],[f969,f19821]) ).
fof(f24787,plain,
( $false
| spl12_46
| ~ spl12_177 ),
inference(forward_subsumption_resolution,[],[f23352,f786]) ).
fof(f24788,plain,
( spl12_46
| ~ spl12_177 ),
inference(avatar_contradiction_clause,[],[f24787]) ).
fof(f28022,plain,
( mem(sF7,sK2(sK3(sF11)))
| subq(sK2(sK3(sF11)),sF10)
| ~ spl12_79 ),
inference(superposition,[],[f51,f1950]) ).
fof(f29116,plain,
( ! [X0] : subq(sK1(sK2(sK3(sF11))),X0)
| spl12_48
| ~ spl12_177 ),
inference(unit_resulting_resolution,[],[f8589,f876,f24786]) ).
fof(f30460,definition,
( spl12_191
<=> subq(sK2(sK3(sF11)),sF11) ),
introduced(definition,[new_symbols(definition,[spl12_191])],[avatar_definition]) ).
fof(f30461,plain,
( subq(sK2(sK3(sF11)),sF11)
| ~ spl12_191 ),
inference(avatar_component_clause,[],[f30460]) ).
fof(f30462,plain,
( ~ subq(sK2(sK3(sF11)),sF11)
| spl12_191 ),
inference(avatar_component_clause,[],[f30460]) ).
fof(f30513,plain,
( ~ mem(sK0(sK2(sK3(sF11)),sF11),sF11)
| spl12_191 ),
inference(unit_resulting_resolution,[],[f52,f30462]) ).
fof(f30515,plain,
( mem(sK0(sK2(sK3(sF11)),sF11),sK3(sF11))
| spl12_191 ),
inference(unit_resulting_resolution,[],[f184,f370,f30462]) ).
fof(f30544,plain,
( mem(sK0(sK2(sK3(sF11)),sF11),sF11)
| spl12_191 ),
inference(unit_resulting_resolution,[],[f50,f137,f30515]) ).
fof(f30560,plain,
( $false
| spl12_191 ),
inference(forward_subsumption_resolution,[],[f30544,f30513]) ).
fof(f30561,plain,
spl12_191,
inference(avatar_contradiction_clause,[],[f30560]) ).
fof(f30586,plain,
( subq(sK2(sK3(sF11)),sF8)
| mem(sF9,sK2(sK3(sF11)))
| ~ spl12_191 ),
inference(resolution,[],[f30461,f14344]) ).
fof(f30705,plain,
( e = sK1(sK2(sK3(sF11)))
| spl12_48
| ~ spl12_177 ),
inference(unit_resulting_resolution,[],[f212,f29116]) ).
fof(f30740,plain,
( $false
| spl12_48
| spl12_64
| ~ spl12_177 ),
inference(forward_subsumption_resolution,[],[f30705,f1023]) ).
fof(f30741,plain,
( spl12_48
| spl12_64
| ~ spl12_177 ),
inference(avatar_contradiction_clause,[],[f30740]) ).
fof(f30742,plain,
( ~ subq(sK2(sK3(sF11)),p(sF7))
| ~ spl12_49 ),
inference(backward_demodulation,[],[f740,f814]) ).
fof(f31467,plain,
( ~ subq(sK2(sK3(sF11)),sF8)
| ~ spl12_49 ),
inference(forward_demodulation,[],[f30742,f88]) ).
fof(f31496,plain,
( $false
| ~ spl12_49
| ~ spl12_177 ),
inference(forward_subsumption_resolution,[],[f31467,f19821]) ).
fof(f31497,plain,
( ~ spl12_49
| ~ spl12_177 ),
inference(avatar_contradiction_clause,[],[f31496]) ).
fof(f32590,plain,
( ~ spl12_89
| spl12_1
| spl12_65
| ~ spl12_73 ),
inference(avatar_split_clause,[],[f9736,f1313,f1026,f216,f3691]) ).
fof(f36495,plain,
( ~ subq(sF10,p(sF9))
| ~ spl12_54
| ~ spl12_55
| spl12_65
| ~ spl12_73 ),
inference(forward_demodulation,[],[f17858,f10796]) ).
fof(f36810,plain,
( $false
| ~ spl12_54
| ~ spl12_55
| spl12_65
| ~ spl12_73 ),
inference(forward_subsumption_resolution,[],[f36495,f5177]) ).
fof(f36811,plain,
( ~ spl12_54
| ~ spl12_55
| spl12_65
| ~ spl12_73 ),
inference(avatar_contradiction_clause,[],[f36810]) ).
fof(f37126,plain,
( ~ mem(e,u(e,sK2(sK3(sF11))))
| spl12_1
| ~ spl12_153 ),
inference(forward_demodulation,[],[f4736,f10263]) ).
fof(f37261,plain,
( subq(sK2(sK3(sF11)),sF10)
| spl12_30
| ~ spl12_45
| ~ spl12_79 ),
inference(forward_subsumption_resolution,[],[f28022,f16219]) ).
fof(f37790,plain,
( $false
| spl12_30
| ~ spl12_45
| spl12_55
| ~ spl12_79 ),
inference(forward_subsumption_resolution,[],[f37261,f982]) ).
fof(f37791,plain,
( spl12_30
| ~ spl12_45
| spl12_55
| ~ spl12_79 ),
inference(avatar_contradiction_clause,[],[f37790]) ).
fof(f38585,plain,
( $false
| spl12_1
| spl12_55
| ~ spl12_153
| ~ spl12_154 ),
inference(forward_subsumption_resolution,[],[f37126,f13007]) ).
fof(f38586,plain,
( spl12_1
| spl12_55
| ~ spl12_153
| ~ spl12_154 ),
inference(avatar_contradiction_clause,[],[f38585]) ).
fof(f38700,plain,
( ~ mem(sF9,sK2(sK3(sF11)))
| spl12_30
| ~ spl12_35 ),
inference(forward_demodulation,[],[f22010,f17730]) ).
fof(f38713,plain,
( $false
| spl12_30
| ~ spl12_35
| ~ spl12_139 ),
inference(forward_subsumption_resolution,[],[f38700,f8283]) ).
fof(f38714,plain,
( spl12_30
| ~ spl12_35
| ~ spl12_139 ),
inference(avatar_contradiction_clause,[],[f38713]) ).
fof(f38743,plain,
( mem(sF9,sK2(sK3(sF11)))
| spl12_177
| ~ spl12_191 ),
inference(forward_subsumption_resolution,[],[f30586,f19822]) ).
fof(f38804,plain,
( $false
| spl12_139
| spl12_177
| ~ spl12_191 ),
inference(forward_subsumption_resolution,[],[f38743,f8284]) ).
fof(f38805,plain,
( spl12_139
| spl12_177
| ~ spl12_191 ),
inference(avatar_contradiction_clause,[],[f38804]) ).
cnf(s1,plain,
( ~ spl12_1
| spl12_2 ),
inference(sat_conversion,[],[f223]) ).
cnf(s17,plain,
( ~ spl12_30
| spl12_31 ),
inference(sat_conversion,[],[f392]) ).
cnf(s18,plain,
( ~ spl12_32
| spl12_33 ),
inference(sat_conversion,[],[f416]) ).
cnf(s19,plain,
( spl12_30
| spl12_34
| spl12_35 ),
inference(sat_conversion,[],[f450]) ).
cnf(s20,plain,
spl12_32,
inference(sat_conversion,[],[f489]) ).
cnf(s25,plain,
( ~ spl12_34
| ~ spl12_44
| spl12_45 ),
inference(sat_conversion,[],[f761]) ).
cnf(s27,plain,
( ~ spl12_46
| ~ spl12_48
| spl12_49 ),
inference(sat_conversion,[],[f815]) ).
cnf(s30,plain,
( spl12_54
| ~ spl12_55 ),
inference(sat_conversion,[],[f983]) ).
cnf(s36,plain,
( spl12_64
| ~ spl12_65 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s40,plain,
( spl12_65
| spl12_72
| spl12_73 ),
inference(sat_conversion,[],[f1316]) ).
cnf(s41,plain,
( ~ spl12_33
| ~ spl12_64
| ~ spl12_65 ),
inference(sat_conversion,[],[f1529]) ).
cnf(s44,plain,
( ~ spl12_72
| ~ spl12_74
| spl12_75 ),
inference(sat_conversion,[],[f1641]) ).
cnf(s46,plain,
( spl12_55
| ~ spl12_78
| spl12_79 ),
inference(sat_conversion,[],[f1951]) ).
cnf(s78,plain,
( spl12_1
| spl12_88
| spl12_89 ),
inference(sat_conversion,[],[f3694]) ).
cnf(s79,plain,
~ spl12_2,
inference(sat_conversion,[],[f3953]) ).
cnf(s80,plain,
( ~ spl12_88
| ~ spl12_90
| spl12_91 ),
inference(sat_conversion,[],[f4411]) ).
cnf(s132,plain,
( ~ spl12_88
| spl12_114
| spl12_153 ),
inference(sat_conversion,[],[f8650]) ).
cnf(s133,plain,
( spl12_55
| spl12_116
| spl12_154 ),
inference(sat_conversion,[],[f8655]) ).
cnf(s135,plain,
( spl12_78
| ~ spl12_116 ),
inference(sat_conversion,[],[f9016]) ).
cnf(s141,plain,
( spl12_65
| ~ spl12_72
| spl12_74 ),
inference(sat_conversion,[],[f9377]) ).
cnf(s149,plain,
( spl12_30
| ~ spl12_35
| spl12_65
| ~ spl12_73 ),
inference(sat_conversion,[],[f9525]) ).
cnf(s162,plain,
( spl12_1
| ~ spl12_64
| ~ spl12_153 ),
inference(sat_conversion,[],[f10491]) ).
cnf(s163,plain,
( spl12_90
| ~ spl12_114 ),
inference(sat_conversion,[],[f10576]) ).
cnf(s165,plain,
( spl12_90
| ~ spl12_114 ),
inference(sat_conversion,[],[f10581]) ).
cnf(s177,plain,
( spl12_1
| spl12_55
| ~ spl12_79
| ~ spl12_91 ),
inference(sat_conversion,[],[f10770]) ).
cnf(s235,plain,
( spl12_30
| ~ spl12_34
| spl12_44
| ~ spl12_64 ),
inference(sat_conversion,[],[f16192]) ).
cnf(s237,plain,
( spl12_1
| spl12_30
| ~ spl12_45
| ~ spl12_91 ),
inference(sat_conversion,[],[f16351]) ).
cnf(s239,plain,
~ spl12_31,
inference(sat_conversion,[],[f17183]) ).
cnf(s258,plain,
( spl12_1
| spl12_65
| ~ spl12_75
| ~ spl12_91 ),
inference(sat_conversion,[],[f17338]) ).
cnf(s282,plain,
( spl12_1
| ~ spl12_89
| ~ spl12_170 ),
inference(sat_conversion,[],[f17639]) ).
cnf(s292,plain,
( spl12_30
| ~ spl12_35
| spl12_170 ),
inference(sat_conversion,[],[f17772]) ).
cnf(s294,plain,
( spl12_30
| spl12_35
| ~ spl12_45
| spl12_65
| ~ spl12_75 ),
inference(sat_conversion,[],[f17776]) ).
cnf(s319,plain,
( spl12_30
| ~ spl12_34
| spl12_44
| spl12_55
| ~ spl12_154 ),
inference(sat_conversion,[],[f17855]) ).
cnf(s401,plain,
( spl12_1
| spl12_30
| ~ spl12_34
| spl12_44
| ~ spl12_153 ),
inference(sat_conversion,[],[f19933]) ).
cnf(s450,plain,
( spl12_1
| ~ spl12_89
| ~ spl12_139 ),
inference(sat_conversion,[],[f20096]) ).
cnf(s521,plain,
( spl12_46
| ~ spl12_177 ),
inference(sat_conversion,[],[f24788]) ).
cnf(s571,plain,
spl12_191,
inference(sat_conversion,[],[f30561]) ).
cnf(s575,plain,
( spl12_48
| spl12_64
| ~ spl12_177 ),
inference(sat_conversion,[],[f30741]) ).
cnf(s589,plain,
( ~ spl12_49
| ~ spl12_177 ),
inference(sat_conversion,[],[f31497]) ).
cnf(s595,plain,
( spl12_1
| spl12_65
| ~ spl12_73
| ~ spl12_89 ),
inference(sat_conversion,[],[f32590]) ).
cnf(s715,plain,
( ~ spl12_54
| ~ spl12_55
| spl12_65
| ~ spl12_73 ),
inference(sat_conversion,[],[f36811]) ).
cnf(s769,plain,
( spl12_30
| ~ spl12_45
| spl12_55
| ~ spl12_79 ),
inference(sat_conversion,[],[f37791]) ).
cnf(s784,plain,
( spl12_1
| spl12_55
| ~ spl12_153
| ~ spl12_154 ),
inference(sat_conversion,[],[f38586]) ).
cnf(s787,plain,
( spl12_30
| ~ spl12_35
| ~ spl12_139 ),
inference(sat_conversion,[],[f38714]) ).
cnf(s802,plain,
( spl12_139
| spl12_177
| ~ spl12_191 ),
inference(sat_conversion,[],[f38805]) ).
cnf(s818,plain,
spl12_33,
inference(rat,[],[s18,s20]) ).
cnf(s819,plain,
~ spl12_30,
inference(rat,[],[s17,s239]) ).
cnf(s820,plain,
~ spl12_1,
inference(rat,[],[s1,s79]) ).
cnf(s821,plain,
~ spl12_35,
inference(rat,[],[s44,s258,s141,s80,s40,s165,s149,s132,s41,s162,s575,s27,s78,s521,s589,s282,s802,s292,s787,s820,s819,s818,s571]) ).
cnf(s823,plain,
spl12_34,
inference(rat,[],[s19,s819,s821]) ).
cnf(s824,plain,
( ~ spl12_72
| spl12_75
| spl12_65 ),
inference(rat,[],[s44,s141]) ).
cnf(s825,plain,
( ~ spl12_88
| spl12_153
| spl12_91 ),
inference(rat,[],[s163,s132,s80]) ).
cnf(s826,plain,
( spl12_65
| ~ spl12_89
| ~ spl12_45 ),
inference(rat,[],[s40,s824,s595,s294,s820,s819,s821]) ).
cnf(s827,plain,
~ spl12_65,
inference(rat,[],[s41,s36,s818]) ).
cnf(s829,plain,
( ~ spl12_177
| spl12_64 ),
inference(rat,[],[s27,s575,s521,s589]) ).
cnf(s833,plain,
( spl12_55
| ~ spl12_45 ),
inference(rat,[],[s135,s133,s46,s784,s769,s825,s78,s826,s237,s820,s819,s827]) ).
cnf(s834,plain,
~ spl12_45,
inference(rat,[],[s715,s30,s833,s40,s824,s294,s827,s819,s821]) ).
cnf(s835,plain,
~ spl12_44,
inference(rat,[],[s25,s823,s834]) ).
cnf(s836,plain,
~ spl12_64,
inference(rat,[],[s235,s823,s819,s835]) ).
cnf(s837,plain,
~ spl12_153,
inference(rat,[],[s401,s823,s820,s819,s835]) ).
cnf(s839,plain,
~ spl12_177,
inference(rat,[],[s829,s836]) ).
cnf(s845,plain,
spl12_139,
inference(rat,[],[s802,s571,s839]) ).
cnf(s848,plain,
~ spl12_89,
inference(rat,[],[s450,s820,s845]) ).
cnf(s850,plain,
spl12_88,
inference(rat,[],[s78,s820,s848]) ).
cnf(s852,plain,
spl12_91,
inference(rat,[],[s825,s837,s850]) ).
cnf(s857,plain,
~ spl12_75,
inference(rat,[],[s258,s827,s820,s852]) ).
cnf(s860,plain,
~ spl12_72,
inference(rat,[],[s824,s827,s857]) ).
cnf(s861,plain,
spl12_73,
inference(rat,[],[s40,s827,s860]) ).
cnf(s863,plain,
spl12_55,
inference(rat,[],[s135,s46,s133,s177,s319,s820,s852,s819,s823,s835]) ).
cnf(s865,plain,
spl12_54,
inference(rat,[],[s30,s863]) ).
cnf(s869,plain,
$false,
inference(rat,[],[s715,s827,s861,s863,s865]) ).
fof(f38824,plain,
$false,
inference(avatar_sat_refutation,[],[s869]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV544+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.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 28 06:34:32 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.45/2.31 % (3206570)Detected formulas, will run a generic FOF schedule.
% 10.45/2.31 % (3206581)dis-21_1_sil=8000:lcm=predicate:random_seed=3988775767: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)
% 10.45/2.31 % (3206581)Instruction limit reached!
% 10.45/2.31 % (3206581)------------------------------
% 10.45/2.31 % (3206581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.31 % (3206581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.31 % (3206581)CaDiCaL version: 2.1.3
% 10.45/2.31 % (3206581)Termination reason: Instruction limit
% 10.45/2.31 % (3206581)Termination phase: Saturation
% 10.45/2.31 % (3206581)Time elapsed: 0.042 s
% 10.45/2.31 % (3206581)Peak memory usage: 89 MB
% 10.45/2.31 % (3206581)Instructions burned: 133 (million)
% 10.45/2.31 % (3206575)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=3176617026:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.45/2.31 % (3206576)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=911832978:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.45/2.31 % (3206577)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=3771298732:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.45/2.31 % (3206579)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2917710673:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.45/2.31 % (3206578)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2663589106:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.45/2.31 % (3206580)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1494746597:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.45/2.31 % (3206578)Refutation not found, incomplete strategy
% 10.45/2.31 % (3206578)------------------------------
% 10.45/2.31 % (3206578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.31 % (3206578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.31 % (3206578)CaDiCaL version: 2.1.3
% 10.45/2.31 % (3206578)Termination reason: Refutation not found, incomplete strategy
% 10.45/2.31 % (3206578)Time elapsed: 0.001 s
% 10.45/2.31 % (3206578)Peak memory usage: 88 MB
% 10.45/2.31 % (3206579)Instruction limit reached!
% 10.45/2.31 % (3206579)------------------------------
% 10.45/2.31 % (3206579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.31 % (3206579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.31 % (3206579)CaDiCaL version: 2.1.3
% 10.45/2.31 % (3206579)Termination reason: Instruction limit
% 10.45/2.31 % (3206579)Termination phase: Saturation
% 10.45/2.31 % (3206579)Time elapsed: 0.072 s
% 10.45/2.31 % (3206579)Peak memory usage: 88 MB
% 10.45/2.31 % (3206579)Instructions burned: 119 (million)
% 10.45/2.31 % (3206580)Instruction limit reached!
% 10.45/2.31 % (3206580)------------------------------
% 10.45/2.31 % (3206580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.31 % (3206580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.31 % (3206580)CaDiCaL version: 2.1.3
% 10.45/2.31 % (3206580)Termination reason: Instruction limit
% 10.45/2.31 % (3206580)Termination phase: Saturation
% 10.45/2.31 % (3206580)Time elapsed: 0.092 s
% 10.45/2.31 % (3206580)Peak memory usage: 89 MB
% 10.45/2.31 % (3206580)Instructions burned: 139 (million)
% 10.45/2.31 % (3206589)lrs+10_1_sil=8000:sp=occurrence:random_seed=736199597:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.45/2.31 % (3206589)Instruction limit reached!
% 10.45/2.31 % (3206589)------------------------------
% 10.45/2.31 % (3206589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.31 % (3206589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.31 % (3206589)CaDiCaL version: 2.1.3
% 10.45/2.31 % (3206589)Termination reason: Instruction limit
% 10.45/2.31 % (3206589)Termination phase: Saturation
% 10.45/2.31 % (3206589)Time elapsed: 0.100 s
% 10.45/2.31 % (3206589)Peak memory usage: 92 MB
% 10.45/2.31 % (3206589)Instructions burned: 287 (million)
% 10.45/2.31 % (3206590)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3553770806:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.10/2.86 % (3206590)Refutation not found, incomplete strategy
% 13.10/2.86 % (3206590)------------------------------
% 13.10/2.86 % (3206590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.10/2.86 % (3206590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.10/2.86 % (3206590)CaDiCaL version: 2.1.3
% 13.10/2.86 % (3206590)Termination reason: Refutation not found, incomplete strategy
% 13.10/2.86 % (3206590)Time elapsed: 0.002 s
% 13.10/2.86 % (3206590)Peak memory usage: 88 MB
% 13.10/2.86 % (3206590)Instructions burned: 1 (million)
% 13.10/2.86 % (3206578)------------------------------
% 13.10/2.86 % (3206578)------------------------------
% 13.10/2.86 % (3206591)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1899201144:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.10/2.86 % (3206591)Refutation not found, incomplete strategy
% 13.10/2.86 % (3206591)------------------------------
% 13.10/2.86 % (3206591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.10/2.86 % (3206591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.10/2.86 % (3206591)CaDiCaL version: 2.1.3
% 13.10/2.86 % (3206591)Termination reason: Refutation not found, incomplete strategy
% 13.10/2.86 % (3206591)Time elapsed: 0.002 s
% 13.10/2.86 % (3206591)Peak memory usage: 88 MB
% 13.10/2.86 % (3206593)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=892035401:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 13.10/2.86 % (3206593)Instruction limit reached!
% 13.10/2.86 % (3206593)------------------------------
% 13.10/2.86 % (3206593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.10/2.86 % (3206593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.10/2.86 % (3206593)CaDiCaL version: 2.1.3
% 13.10/2.86 % (3206593)Termination reason: Instruction limit
% 13.10/2.86 % (3206593)Termination phase: Saturation
% 13.10/2.86 % (3206593)Time elapsed: 0.077 s
% 13.10/2.86 % (3206593)Peak memory usage: 91 MB
% 13.10/2.86 % (3206593)Instructions burned: 250 (million)
% 13.10/2.86 % (3206596)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=312578003:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 13.10/2.86 % (3206596)Refutation not found, incomplete strategy
% 13.10/2.86 % (3206596)------------------------------
% 13.10/2.86 % (3206596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.10/2.86 % (3206596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.10/2.86 % (3206596)CaDiCaL version: 2.1.3
% 13.10/2.86 % (3206596)Termination reason: Refutation not found, incomplete strategy
% 13.10/2.86 % (3206596)Time elapsed: 0.002 s
% 13.10/2.86 % (3206596)Peak memory usage: 88 MB
% 13.10/2.86 % (3206596)Instructions burned: 1 (million)
% 13.10/2.86 % (3206590)------------------------------
% 13.10/2.86 % (3206590)------------------------------
% 13.10/2.86 % (3206591)------------------------------
% 13.10/2.86 % (3206591)------------------------------
% 13.10/2.86 % (3206598)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1616176960:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 13.10/2.86 % (3206577)Refutation not found, incomplete strategy
% 13.10/2.86 % (3206577)------------------------------
% 13.10/2.86 % (3206577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.10/2.86 % (3206577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.10/2.86 % (3206577)CaDiCaL version: 2.1.3
% 13.10/2.86 % (3206577)Termination reason: Refutation not found, incomplete strategy
% 13.10/2.86 % (3206577)Time elapsed: 0.562 s
% 13.10/2.86 % (3206577)Peak memory usage: 125 MB
% 13.10/2.86 % (3206577)Instructions burned: 827 (million)
% 13.10/2.86 % (3206600)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=150083415:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 13.10/2.86 % (3206596)------------------------------
% 13.10/2.86 % (3206596)------------------------------
% 13.10/2.86 % (3206601)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=254095484:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 13.10/2.86 % (3206600)Instruction limit reached!
% 13.10/2.86 % (3206600)------------------------------
% 13.10/2.86 % (3206600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.80/5.18 % (3206600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.80/5.18 % (3206600)CaDiCaL version: 2.1.3
% 30.80/5.18 % (3206600)Termination reason: Instruction limit
% 30.80/5.18 % (3206600)Termination phase: Saturation
% 30.80/5.18 % (3206600)Time elapsed: 0.075 s
% 30.80/5.18 % (3206600)Peak memory usage: 89 MB
% 30.80/5.18 % (3206600)Instructions burned: 114 (million)
% 30.80/5.18 % (3206601)Instruction limit reached!
% 30.80/5.18 % (3206601)------------------------------
% 30.80/5.18 % (3206601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.80/5.18 % (3206601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.80/5.18 % (3206601)CaDiCaL version: 2.1.3
% 30.80/5.18 % (3206601)Termination reason: Instruction limit
% 30.80/5.18 % (3206601)Termination phase: Saturation
% 30.80/5.18 % (3206601)Time elapsed: 0.061 s
% 30.80/5.18 % (3206601)Peak memory usage: 88 MB
% 30.80/5.18 % (3206601)Instructions burned: 128 (million)
% 30.80/5.18 % (3206577)------------------------------
% 30.80/5.18 % (3206577)------------------------------
% 30.80/5.18 % (3206605)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2465896211:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 30.80/5.18 % (3206606)lrs+10_1_sil=8000:sp=occurrence:random_seed=2484319528:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 30.80/5.18 % (3206605)Instruction limit reached!
% 30.80/5.18 % (3206605)------------------------------
% 30.80/5.18 % (3206605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.80/5.18 % (3206605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.80/5.18 % (3206605)CaDiCaL version: 2.1.3
% 30.80/5.18 % (3206605)Termination reason: Instruction limit
% 30.80/5.18 % (3206605)Termination phase: Saturation
% 30.80/5.18 % (3206605)Time elapsed: 0.070 s
% 30.80/5.18 % (3206605)Peak memory usage: 89 MB
% 30.80/5.18 % (3206605)Instructions burned: 115 (million)
% 30.80/5.18 % (3206607)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=837032721:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 30.80/5.18 % (3206607)Refutation not found, incomplete strategy
% 30.80/5.18 % (3206607)------------------------------
% 30.80/5.18 % (3206607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.80/5.18 % (3206607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.80/5.18 % (3206607)CaDiCaL version: 2.1.3
% 30.80/5.18 % (3206607)Termination reason: Refutation not found, incomplete strategy
% 30.80/5.18 % (3206607)Time elapsed: 0.001 s
% 30.80/5.18 % (3206607)Peak memory usage: 88 MB
% 30.80/5.18 % (3206608)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2118030741:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 30.80/5.18 % (3206612)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=182082681:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 30.80/5.18 % (3206612)Instruction limit reached!
% 30.80/5.18 % (3206612)------------------------------
% 30.80/5.18 % (3206612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.80/5.18 % (3206612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.80/5.18 % (3206612)CaDiCaL version: 2.1.3
% 30.80/5.18 % (3206612)Termination reason: Instruction limit
% 30.80/5.18 % (3206612)Termination phase: Saturation
% 30.80/5.18 % (3206612)Time elapsed: 0.072 s
% 30.80/5.18 % (3206612)Peak memory usage: 89 MB
% 30.80/5.18 % (3206612)Instructions burned: 135 (million)
% 30.80/5.18 % (3206607)------------------------------
% 30.80/5.18 % (3206607)------------------------------
% 30.80/5.18 % (3206616)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3408315411:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 30.80/5.18 % (3206615)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3703530851:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 30.80/5.18 % (3206615)Refutation not found, incomplete strategy
% 30.80/5.18 % (3206615)------------------------------
% 30.80/5.18 % (3206615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.80/5.18 % (3206615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.80/5.18 % (3206615)CaDiCaL version: 2.1.3
% 30.80/5.18 % (3206615)Termination reason: Refutation not found, incomplete strategy
% 35.54/6.04 % (3206615)Time elapsed: 0.002 s
% 35.54/6.04 % (3206615)Peak memory usage: 88 MB
% 35.54/6.04 % (3206615)Instructions burned: 1 (million)
% 35.54/6.04 % (3206598)Instruction limit reached!
% 35.54/6.04 % (3206598)------------------------------
% 35.54/6.04 % (3206598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.04 % (3206598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.04 % (3206598)CaDiCaL version: 2.1.3
% 35.54/6.04 % (3206598)Termination reason: Instruction limit
% 35.54/6.04 % (3206598)Termination phase: Saturation
% 35.54/6.04 % (3206598)Time elapsed: 0.857 s
% 35.54/6.04 % (3206598)Peak memory usage: 142 MB
% 35.54/6.04 % (3206598)Instructions burned: 2350 (million)
% 35.54/6.04 % (3206606)Instruction limit reached!
% 35.54/6.04 % (3206606)------------------------------
% 35.54/6.04 % (3206606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.04 % (3206606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.04 % (3206606)CaDiCaL version: 2.1.3
% 35.54/6.04 % (3206606)Termination reason: Instruction limit
% 35.54/6.04 % (3206606)Termination phase: Saturation
% 35.54/6.04 % (3206606)Time elapsed: 0.574 s
% 35.54/6.04 % (3206606)Peak memory usage: 97 MB
% 35.54/6.04 % (3206606)Instructions burned: 908 (million)
% 35.54/6.04 % (3206619)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=605179262:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 35.54/6.04 % (3206615)------------------------------
% 35.54/6.04 % (3206615)------------------------------
% 35.54/6.04 % (3206619)Instruction limit reached!
% 35.54/6.04 % (3206619)------------------------------
% 35.54/6.04 % (3206619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.04 % (3206619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.04 % (3206619)CaDiCaL version: 2.1.3
% 35.54/6.04 % (3206619)Termination reason: Instruction limit
% 35.54/6.04 % (3206619)Termination phase: Saturation
% 35.54/6.04 % (3206619)Time elapsed: 0.044 s
% 35.54/6.04 % (3206619)Peak memory usage: 90 MB
% 35.54/6.04 % (3206619)Instructions burned: 125 (million)
% 35.54/6.04 % (3206620)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=11068089:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 35.54/6.04 % (3206623)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=25645181:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi)
% 35.54/6.04 % (3206623)Refutation not found, incomplete strategy
% 35.54/6.04 % (3206623)------------------------------
% 35.54/6.04 % (3206623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.04 % (3206623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.04 % (3206623)CaDiCaL version: 2.1.3
% 35.54/6.04 % (3206623)Termination reason: Refutation not found, incomplete strategy
% 35.54/6.04 % (3206623)Time elapsed: 0.001 s
% 35.54/6.04 % (3206623)Peak memory usage: 88 MB
% 35.54/6.04 % (3206622)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2609750899:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi)
% 35.54/6.04 % (3206620)Instruction limit reached!
% 35.54/6.04 % (3206620)------------------------------
% 35.54/6.04 % (3206620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.04 % (3206620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.04 % (3206620)CaDiCaL version: 2.1.3
% 35.54/6.04 % (3206620)Termination reason: Instruction limit
% 35.54/6.04 % (3206620)Termination phase: Saturation
% 35.54/6.04 % (3206620)Time elapsed: 0.077 s
% 35.54/6.04 % (3206620)Peak memory usage: 90 MB
% 35.54/6.04 % (3206620)Instructions burned: 136 (million)
% 35.54/6.04 % (3206622)Refutation not found, incomplete strategy
% 35.54/6.04 % (3206622)------------------------------
% 35.54/6.04 % (3206622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.04 % (3206622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.04 % (3206622)CaDiCaL version: 2.1.3
% 35.54/6.04 % (3206622)Termination reason: Refutation not found, incomplete strategy
% 35.54/6.04 % (3206622)Time elapsed: 0.001 s
% 35.54/6.04 % (3206622)Peak memory usage: 88 MB
% 35.54/6.04 % (3206623)------------------------------
% 35.54/6.04 % (3206623)------------------------------
% 35.54/6.04 % (3206627)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=2527936688:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi)
% 35.54/6.04 % (3206622)------------------------------
% 35.54/6.04 % (3206622)------------------------------
% 35.54/6.04 % (3206628)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=845128596:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2979 on theBenchmark for (2979ds/150Mi)
% 35.54/6.04 % (3206628)Instruction limit reached!
% 35.54/6.04 % (3206628)------------------------------
% 35.54/6.04 % (3206628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.04 % (3206628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.04 % (3206628)CaDiCaL version: 2.1.3
% 35.54/6.04 % (3206628)Termination reason: Instruction limit
% 35.54/6.04 % (3206628)Termination phase: Saturation
% 35.54/6.04 % (3206628)Time elapsed: 0.047 s
% 35.54/6.04 % (3206628)Peak memory usage: 90 MB
% 35.54/6.04 % (3206628)Instructions burned: 150 (million)
% 35.54/6.04 % (3206630)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1272589289:i=14155:bd=all_2978 on theBenchmark for (2978ds/14155Mi)
% 35.54/6.04 % (3206632)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4190779989:i=667:av=off:fsr=off_2978 on theBenchmark for (2978ds/667Mi)
% 35.54/6.04 % (3206632)Refutation not found, incomplete strategy
% 35.54/6.04 % (3206632)------------------------------
% 35.54/6.04 % (3206632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.04 % (3206632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.04 % (3206632)CaDiCaL version: 2.1.3
% 35.54/6.04 % (3206632)Termination reason: Refutation not found, incomplete strategy
% 35.54/6.04 % (3206632)Time elapsed: 0.002 s
% 35.54/6.04 % (3206632)Peak memory usage: 88 MB
% 35.54/6.04 % (3206632)Instructions burned: 1 (million)
% 35.54/6.04 % (3206632)------------------------------
% 35.54/6.04 % (3206632)------------------------------
% 35.54/6.04 % (3206635)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=4065782134:s2a=on:i=185:s2at=1.8:fdi=4_2974 on theBenchmark for (2974ds/185Mi)
% 35.54/6.04 % (3206635)Instruction limit reached!
% 35.54/6.04 % (3206635)------------------------------
% 35.54/6.04 % (3206635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.04 % (3206635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.04 % (3206635)CaDiCaL version: 2.1.3
% 35.54/6.04 % (3206635)Termination reason: Instruction limit
% 35.54/6.04 % (3206635)Termination phase: Saturation
% 35.54/6.04 % (3206635)Time elapsed: 0.099 s
% 35.54/6.04 % (3206635)Peak memory usage: 90 MB
% 35.54/6.04 % (3206635)Instructions burned: 185 (million)
% 35.54/6.04 % (3206637)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2500575884:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2971 on theBenchmark for (2971ds/193Mi)
% 35.54/6.04 % (3206637)Instruction limit reached!
% 35.54/6.04 % (3206637)------------------------------
% 35.54/6.04 % (3206637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.04 % (3206637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.04 % (3206637)CaDiCaL version: 2.1.3
% 35.54/6.04 % (3206637)Termination reason: Instruction limit
% 35.54/6.04 % (3206637)Termination phase: Saturation
% 35.54/6.04 % (3206637)Time elapsed: 0.131 s
% 35.54/6.04 % (3206637)Peak memory usage: 91 MB
% 35.54/6.04 % (3206637)Instructions burned: 195 (million)
% 35.54/6.04 % (3206639)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2541960712:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2968 on theBenchmark for (2968ds/4850Mi)
% 35.54/6.04 % (3206608)Instruction limit reached!
% 35.54/6.04 % (3206608)------------------------------
% 35.54/6.04 % (3206608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.04 % (3206608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.04 % (3206608)CaDiCaL version: 2.1.3
% 35.54/6.04 % (3206608)Termination reason: Instruction limit
% 35.54/6.04 % (3206608)Termination phase: Saturation
% 35.54/6.04 % (3206608)Time elapsed: 3.205 s
% 35.54/6.04 % (3206608)Peak memory usage: 166 MB
% 35.54/6.04 % (3206608)Instructions burned: 5203 (million)
% 35.54/6.04 % (3206641)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4123154996:i=12111:sd=1:ss=included_2956 on theBenchmark for (2956ds/12111Mi)
% 35.54/6.04 % (3206630)First to succeed.
% 35.54/6.04 % (3206630)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3206570"
% 35.54/6.04 % (3206641)Refutation not found, incomplete strategy
% 35.54/6.04 % (3206641)------------------------------
% 35.54/6.04 % (3206641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.54/6.04 % (3206641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/6.04 % (3206641)CaDiCaL version: 2.1.3
% 35.54/6.04 % (3206641)Termination reason: Refutation not found, incomplete strategy
% 35.54/6.04 % (3206641)Time elapsed: 0.565 s
% 35.54/6.04 % (3206641)Peak memory usage: 127 MB
% 35.54/6.04 % (3206641)Instructions burned: 855 (million)
% 35.54/6.04 % (3206630)Refutation found. Thanks to Tanya!
% 35.54/6.04 % SZS status Theorem for theBenchmark
% 35.54/6.04 % SZS output start Proof for theBenchmark
% See solution above
% 37.10/6.13 % (3206630)------------------------------
% 37.10/6.13 % (3206630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.10/6.13 % (3206630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.10/6.13 % (3206630)CaDiCaL version: 2.1.3
% 37.10/6.13 % (3206630)Termination reason: Refutation
% 37.10/6.13 % (3206630)Time elapsed: 2.624 s
% 37.10/6.13 % (3206630)Peak memory usage: 152 MB
% 37.10/6.13 % (3206630)Instructions burned: 4339 (million)
% 37.10/6.13 % (3206630)------------------------------
% 37.10/6.13 % (3206630)------------------------------
% 37.10/6.13 % (3206570)Success in time 5.199 s
% 37.10/6.13 % Vampire exiting
%------------------------------------------------------------------------------