%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV576+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 : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:58:22 PM UTC 2026
% Result : Theorem 15.64s 5.14s
% Output : Refutation 31.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 61
% Syntax : Number of formulae : 415 ( 133 unt; 51 def)
% Number of atoms : 865 ( 149 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 748 ( 298 ~; 402 |; 17 &)
% ( 28 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 26 ( 24 usr; 23 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 30 con; 0-2 aty)
% Number of variables : 228 ( 0 sgn 226 !; 2 ?)
% 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(f7,axiom,
! [X0,X1,X2] :
( mem(X0,m(X1,X2))
<=> ( mem(X0,X1)
& ~ mem(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_ax) ).
fof(f8,axiom,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_def) ).
fof(f9,axiom,
! [X0] : n(X0) = a(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_def) ).
fof(f10,axiom,
! [X0,X1] :
( mem(X0,p(X1))
<=> subq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p_ax) ).
fof(f26,conjecture,
subq(u(a(a(p(s(n(n(e)))),n(n(n(e)))),a(s(s(n(e))),n(n(e)))),a(a(s(p(s(n(e)))),n(s(n(e)))),a(n(s(n(e))),n(n(e))))),u(u(a(s(p(s(n(e)))),n(s(n(e)))),a(p(s(n(n(e)))),n(n(n(e))))),m(p(a(n(s(n(e))),n(n(e)))),a(p(n(s(n(e)))),s(n(n(e))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subq_22881_23905) ).
fof(f27,negated_conjecture,
~ subq(u(a(a(p(s(n(n(e)))),n(n(n(e)))),a(s(s(n(e))),n(n(e)))),a(a(s(p(s(n(e)))),n(s(n(e)))),a(n(s(n(e))),n(n(e))))),u(u(a(s(p(s(n(e)))),n(s(n(e)))),a(p(s(n(n(e)))),n(n(n(e))))),m(p(a(n(s(n(e))),n(n(e)))),a(p(n(s(n(e)))),s(n(n(e))))))),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f28,plain,
~ subq(u(a(a(p(s(n(n(e)))),n(n(n(e)))),a(s(s(n(e))),n(n(e)))),a(a(s(p(s(n(e)))),n(s(n(e)))),a(n(s(n(e))),n(n(e))))),u(u(a(s(p(s(n(e)))),n(s(n(e)))),a(p(s(n(n(e)))),n(n(n(e))))),m(p(a(n(s(n(e))),n(n(e)))),a(p(n(s(n(e)))),s(n(n(e))))))),
inference(flattening,[],[f27]) ).
fof(f29,plain,
! [X0,X1] :
( subq(X0,X1)
<=> ! [X2] :
( mem(X2,X1)
| ~ mem(X2,X0) ) ),
inference(ennf_transformation,[],[f1]) ).
fof(f30,plain,
! [X0,X1] :
( X0 = X1
| ~ subq(X1,X0)
| ~ subq(X0,X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f31,plain,
! [X0,X1] :
( X0 = X1
| ~ subq(X1,X0)
| ~ subq(X0,X1) ),
inference(flattening,[],[f30]) ).
fof(f32,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,[],[f29]) ).
fof(f33,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,[],[f32]) ).
fof(f34,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))],[f33]) ).
fof(f35,plain,
! [X0,X1] :
( ( mem(X0,s(X1))
| X0 != X1 )
& ( X0 = X1
| ~ mem(X0,s(X1)) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f36,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(f37,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,[],[f36]) ).
fof(f38,plain,
! [X0,X1,X2] :
( ( mem(X0,m(X1,X2))
| ~ mem(X0,X1)
| mem(X0,X2) )
& ( ( mem(X0,X1)
& ~ mem(X0,X2) )
| ~ mem(X0,m(X1,X2)) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f39,plain,
! [X0,X1,X2] :
( ( mem(X0,m(X1,X2))
| ~ mem(X0,X1)
| mem(X0,X2) )
& ( ( mem(X0,X1)
& ~ mem(X0,X2) )
| ~ mem(X0,m(X1,X2)) ) ),
inference(flattening,[],[f38]) ).
fof(f40,plain,
! [X0,X1] :
( ( mem(X0,p(X1))
| ~ subq(X0,X1) )
& ( subq(X0,X1)
| ~ mem(X0,p(X1)) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f41,plain,
! [X3,X0,X1] :
( ~ mem(X3,X0)
| mem(X3,X1)
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f42,plain,
! [X0,X1] :
( mem(sK0(X0,X1),X0)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f43,plain,
! [X0,X1] :
( ~ mem(sK0(X0,X1),X1)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f44,plain,
! [X0,X1] :
( ~ subq(X1,X0)
| X0 = X1
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
fof(f45,plain,
! [X0] : ~ mem(X0,e),
inference(cnf_transformation,[],[f4]) ).
fof(f46,plain,
! [X0,X1] :
( ~ mem(X0,s(X1))
| X0 = X1 ),
inference(cnf_transformation,[],[f35]) ).
fof(f47,plain,
! [X0,X1] :
( mem(X0,s(X1))
| X0 != X1 ),
inference(cnf_transformation,[],[f35]) ).
fof(f48,plain,
! [X2,X0,X1] :
( ~ mem(X0,u(X1,X2))
| mem(X0,X2)
| mem(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f49,plain,
! [X2,X0,X1] :
( mem(X0,u(X1,X2))
| ~ mem(X0,X2) ),
inference(cnf_transformation,[],[f37]) ).
fof(f50,plain,
! [X2,X0,X1] :
( mem(X0,u(X1,X2))
| ~ mem(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f51,plain,
! [X2,X0,X1] :
( ~ mem(X0,m(X1,X2))
| ~ mem(X0,X2) ),
inference(cnf_transformation,[],[f39]) ).
fof(f52,plain,
! [X2,X0,X1] :
( ~ mem(X0,m(X1,X2))
| mem(X0,X1) ),
inference(cnf_transformation,[],[f39]) ).
fof(f53,plain,
! [X2,X0,X1] :
( mem(X0,m(X1,X2))
| ~ mem(X0,X1)
| mem(X0,X2) ),
inference(cnf_transformation,[],[f39]) ).
fof(f54,plain,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
inference(cnf_transformation,[],[f8]) ).
fof(f55,plain,
! [X0] : n(X0) = a(X0,X0),
inference(cnf_transformation,[],[f9]) ).
fof(f56,plain,
! [X0,X1] :
( ~ mem(X0,p(X1))
| subq(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
fof(f57,plain,
! [X0,X1] :
( mem(X0,p(X1))
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
fof(f58,plain,
~ subq(u(a(a(p(s(n(n(e)))),n(n(n(e)))),a(s(s(n(e))),n(n(e)))),a(a(s(p(s(n(e)))),n(s(n(e)))),a(n(s(n(e))),n(n(e))))),u(u(a(s(p(s(n(e)))),n(s(n(e)))),a(p(s(n(n(e)))),n(n(n(e))))),m(p(a(n(s(n(e))),n(n(e)))),a(p(n(s(n(e)))),s(n(n(e))))))),
inference(cnf_transformation,[],[f28]) ).
fof(f59,plain,
! [X0] : n(X0) = u(X0,s(X0)),
inference(definition_unfolding,[],[f55,f54]) ).
fof(f60,plain,
~ subq(u(u(u(p(s(u(u(e,s(e)),s(u(e,s(e)))))),s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))))),s(u(s(s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))))),u(u(s(p(s(u(e,s(e))))),s(u(s(u(e,s(e))),s(s(u(e,s(e))))))),s(u(u(s(u(e,s(e))),s(s(u(e,s(e))))),s(u(u(e,s(e)),s(u(e,s(e))))))))),u(u(u(s(p(s(u(e,s(e))))),s(u(s(u(e,s(e))),s(s(u(e,s(e))))))),u(p(s(u(u(e,s(e)),s(u(e,s(e)))))),s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))))),m(p(u(u(s(u(e,s(e))),s(s(u(e,s(e))))),s(u(u(e,s(e)),s(u(e,s(e))))))),u(p(u(s(u(e,s(e))),s(s(u(e,s(e)))))),s(s(u(u(e,s(e)),s(u(e,s(e)))))))))),
inference(definition_unfolding,[],[f58,f54,f54,f59,f59,f59,f59,f59,f54,f59,f59,f59,f54,f54,f59,f59,f59,f54,f59,f59,f59,f59,f54,f59,f59,f59,f54,f59,f59,f59,f59,f59,f54,f59,f59,f59,f59,f54,f59,f59,f59,f59]) ).
fof(f61,plain,
! [X1] : mem(X1,s(X1)),
inference(equality_resolution,[],[f47]) ).
fof(f62,definition,
sF1 = s(e),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f63,plain,
s(e) = sF1,
inference(reorient_equations,[],[f62]) ).
fof(f64,definition,
sF2 = u(e,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f65,plain,
u(e,sF1) = sF2,
inference(reorient_equations,[],[f64]) ).
fof(f66,definition,
sF3 = s(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f67,plain,
s(sF2) = sF3,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF4 = u(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f69,plain,
u(sF2,sF3) = sF4,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF5 = s(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f71,plain,
s(sF4) = sF5,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF6 = p(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f73,plain,
p(sF5) = sF6,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF7 = u(sF4,sF5),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f75,plain,
u(sF4,sF5) = sF7,
inference(reorient_equations,[],[f74]) ).
fof(f76,definition,
sF8 = s(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f77,plain,
s(sF7) = sF8,
inference(reorient_equations,[],[f76]) ).
fof(f78,definition,
sF9 = u(sF6,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f79,plain,
u(sF6,sF8) = sF9,
inference(reorient_equations,[],[f78]) ).
fof(f80,definition,
sF10 = s(sF3),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f81,plain,
s(sF3) = sF10,
inference(reorient_equations,[],[f80]) ).
fof(f82,definition,
sF11 = u(sF10,sF5),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f83,plain,
u(sF10,sF5) = sF11,
inference(reorient_equations,[],[f82]) ).
fof(f84,definition,
sF12 = s(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f85,plain,
s(sF11) = sF12,
inference(reorient_equations,[],[f84]) ).
fof(f86,definition,
sF13 = u(sF9,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f87,plain,
u(sF9,sF12) = sF13,
inference(reorient_equations,[],[f86]) ).
fof(f88,definition,
sF14 = p(sF3),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f89,plain,
p(sF3) = sF14,
inference(reorient_equations,[],[f88]) ).
fof(f90,definition,
sF15 = s(sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f91,plain,
s(sF14) = sF15,
inference(reorient_equations,[],[f90]) ).
fof(f92,definition,
sF16 = u(sF3,sF10),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f93,plain,
u(sF3,sF10) = sF16,
inference(reorient_equations,[],[f92]) ).
fof(f94,definition,
sF17 = s(sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f95,plain,
s(sF16) = sF17,
inference(reorient_equations,[],[f94]) ).
fof(f96,definition,
sF18 = u(sF15,sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f97,plain,
u(sF15,sF17) = sF18,
inference(reorient_equations,[],[f96]) ).
fof(f98,definition,
sF19 = u(sF16,sF5),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f99,plain,
u(sF16,sF5) = sF19,
inference(reorient_equations,[],[f98]) ).
fof(f100,definition,
sF20 = s(sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f101,plain,
s(sF19) = sF20,
inference(reorient_equations,[],[f100]) ).
fof(f102,definition,
sF21 = u(sF18,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f103,plain,
u(sF18,sF20) = sF21,
inference(reorient_equations,[],[f102]) ).
fof(f104,definition,
sF22 = u(sF13,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f105,plain,
u(sF13,sF21) = sF22,
inference(reorient_equations,[],[f104]) ).
fof(f106,definition,
sF23 = u(sF18,sF9),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f107,plain,
u(sF18,sF9) = sF23,
inference(reorient_equations,[],[f106]) ).
fof(f108,definition,
sF24 = p(sF19),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f109,plain,
p(sF19) = sF24,
inference(reorient_equations,[],[f108]) ).
fof(f110,definition,
sF25 = p(sF16),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f111,plain,
p(sF16) = sF25,
inference(reorient_equations,[],[f110]) ).
fof(f112,definition,
sF26 = s(sF5),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f113,plain,
s(sF5) = sF26,
inference(reorient_equations,[],[f112]) ).
fof(f114,definition,
sF27 = u(sF25,sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f115,plain,
u(sF25,sF26) = sF27,
inference(reorient_equations,[],[f114]) ).
fof(f116,definition,
sF28 = m(sF24,sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f117,plain,
m(sF24,sF27) = sF28,
inference(reorient_equations,[],[f116]) ).
fof(f118,definition,
sF29 = u(sF23,sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f119,plain,
u(sF23,sF28) = sF29,
inference(reorient_equations,[],[f118]) ).
fof(f120,plain,
~ subq(sF22,sF29),
inference(definition_folding,[],[f60,f119,f117,f115,f113,f71,f69,f67,f65,f63,f65,f63,f111,f93,f81,f67,f65,f63,f67,f65,f63,f109,f99,f71,f69,f67,f65,f63,f65,f63,f93,f81,f67,f65,f63,f67,f65,f63,f107,f79,f77,f75,f71,f69,f67,f65,f63,f65,f63,f69,f67,f65,f63,f65,f63,f73,f71,f69,f67,f65,f63,f65,f63,f97,f95,f93,f81,f67,f65,f63,f67,f65,f63,f91,f89,f67,f65,f63,f105,f103,f101,f99,f71,f69,f67,f65,f63,f65,f63,f93,f81,f67,f65,f63,f67,f65,f63,f97,f95,f93,f81,f67,f65,f63,f67,f65,f63,f91,f89,f67,f65,f63,f87,f85,f83,f71,f69,f67,f65,f63,f65,f63,f81,f67,f65,f63,f79,f77,f75,f71,f69,f67,f65,f63,f65,f63,f69,f67,f65,f63,f65,f63,f73,f71,f69,f67,f65,f63,f65,f63]) ).
fof(f121,plain,
! [X0] :
( subq(X0,X0)
| subq(X0,X0) ),
inference(resolution,[],[f42,f43]) ).
fof(f122,plain,
! [X0] : subq(X0,X0),
inference(duplicate_literal_removal,[],[f121]) ).
fof(f123,plain,
mem(sF2,sF3),
inference(superposition,[],[f61,f67]) ).
fof(f124,plain,
mem(sF3,sF10),
inference(superposition,[],[f61,f81]) ).
fof(f125,plain,
mem(sF4,sF5),
inference(superposition,[],[f61,f71]) ).
fof(f127,plain,
mem(sF16,sF17),
inference(superposition,[],[f61,f95]) ).
fof(f132,plain,
mem(e,sF1),
inference(superposition,[],[f61,f63]) ).
fof(f136,plain,
! [X0] :
( ~ mem(X0,sF25)
| subq(X0,sF16) ),
inference(superposition,[],[f56,f111]) ).
fof(f138,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X2)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f49,f43]) ).
fof(f139,plain,
! [X0] :
( ~ mem(X0,sF1)
| mem(X0,sF2) ),
inference(superposition,[],[f49,f65]) ).
fof(f146,plain,
! [X0] :
( ~ mem(X0,sF10)
| mem(X0,sF16) ),
inference(superposition,[],[f49,f93]) ).
fof(f148,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X1)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f50,f43]) ).
fof(f150,plain,
! [X0] :
( ~ mem(X0,sF3)
| mem(X0,sF16) ),
inference(superposition,[],[f50,f93]) ).
fof(f151,plain,
! [X0] :
( ~ mem(X0,sF6)
| mem(X0,sF9) ),
inference(superposition,[],[f50,f79]) ).
fof(f154,plain,
! [X0] :
( ~ mem(X0,sF23)
| mem(X0,sF29) ),
inference(superposition,[],[f50,f119]) ).
fof(f160,plain,
! [X0] :
( ~ mem(X0,sF2)
| mem(X0,sF4) ),
inference(superposition,[],[f50,f69]) ).
fof(f161,plain,
! [X0] :
( ~ mem(X0,sF3)
| mem(X0,sF4) ),
inference(superposition,[],[f49,f69]) ).
fof(f164,plain,
! [X0] :
( ~ mem(X0,sF18)
| mem(X0,sF23) ),
inference(superposition,[],[f50,f107]) ).
fof(f165,plain,
! [X0] :
( ~ mem(X0,sF9)
| mem(X0,sF23) ),
inference(superposition,[],[f49,f107]) ).
fof(f166,plain,
! [X0] :
( ~ mem(X0,sF16)
| mem(X0,sF19) ),
inference(superposition,[],[f50,f99]) ).
fof(f167,plain,
! [X0] :
( ~ mem(X0,sF5)
| mem(X0,sF19) ),
inference(superposition,[],[f49,f99]) ).
fof(f169,plain,
! [X0] :
( ~ mem(X0,sF5)
| mem(X0,sF11) ),
inference(superposition,[],[f49,f83]) ).
fof(f170,plain,
! [X2,X0,X1] :
( mem(sK0(u(X0,X1),X2),X1)
| mem(sK0(u(X0,X1),X2),X0)
| subq(u(X0,X1),X2) ),
inference(resolution,[],[f48,f42]) ).
fof(f173,plain,
! [X0] :
( ~ mem(X0,sF2)
| mem(X0,sF1)
| mem(X0,e) ),
inference(superposition,[],[f48,f65]) ).
fof(f175,plain,
! [X0] :
( ~ mem(X0,sF16)
| mem(X0,sF10)
| mem(X0,sF3) ),
inference(superposition,[],[f48,f93]) ).
fof(f177,plain,
! [X0] :
( ~ mem(X0,sF13)
| mem(X0,sF12)
| mem(X0,sF9) ),
inference(superposition,[],[f48,f87]) ).
fof(f178,plain,
! [X0] :
( ~ mem(X0,sF11)
| mem(X0,sF5)
| mem(X0,sF10) ),
inference(superposition,[],[f48,f83]) ).
fof(f179,plain,
! [X0] :
( ~ mem(X0,sF22)
| mem(X0,sF21)
| mem(X0,sF13) ),
inference(superposition,[],[f48,f105]) ).
fof(f182,plain,
! [X0] :
( ~ mem(X0,sF21)
| mem(X0,sF20)
| mem(X0,sF18) ),
inference(superposition,[],[f48,f103]) ).
fof(f185,plain,
! [X0] :
( ~ mem(X0,sF27)
| mem(X0,sF26)
| mem(X0,sF25) ),
inference(superposition,[],[f48,f115]) ).
fof(f186,plain,
! [X0] :
( ~ mem(X0,sF2)
| mem(X0,sF1) ),
inference(forward_subsumption_resolution,[],[f173,f45]) ).
fof(f193,plain,
! [X2,X0,X1] :
( mem(sK0(m(X0,X1),X2),X0)
| subq(m(X0,X1),X2) ),
inference(resolution,[],[f52,f42]) ).
fof(f199,plain,
! [X0] :
( ~ mem(X0,sF24)
| mem(X0,sF28)
| mem(X0,sF27) ),
inference(superposition,[],[f53,f117]) ).
fof(f202,plain,
! [X0,X1] :
( subq(s(X0),X1)
| sK0(s(X0),X1) = X0 ),
inference(resolution,[],[f46,f42]) ).
fof(f204,plain,
! [X0] :
( ~ mem(X0,sF1)
| e = X0 ),
inference(superposition,[],[f46,f63]) ).
fof(f205,plain,
! [X0] :
( ~ mem(X0,sF3)
| sF2 = X0 ),
inference(superposition,[],[f46,f67]) ).
fof(f206,plain,
! [X0] :
( ~ mem(X0,sF10)
| sF3 = X0 ),
inference(superposition,[],[f46,f81]) ).
fof(f207,plain,
! [X0] :
( ~ mem(X0,sF5)
| sF4 = X0 ),
inference(superposition,[],[f46,f71]) ).
fof(f208,plain,
! [X0] :
( ~ mem(X0,sF26)
| sF5 = X0 ),
inference(superposition,[],[f46,f113]) ).
fof(f210,plain,
! [X0] :
( ~ mem(X0,sF12)
| sF11 = X0 ),
inference(superposition,[],[f46,f85]) ).
fof(f212,plain,
! [X0] :
( ~ mem(X0,sF17)
| sF16 = X0 ),
inference(superposition,[],[f46,f95]) ).
fof(f213,plain,
! [X0] :
( ~ mem(X0,sF20)
| sF19 = X0 ),
inference(superposition,[],[f46,f101]) ).
fof(f217,plain,
! [X2,X0,X1] :
( ~ mem(sK0(m(X0,X1),X2),X1)
| subq(m(X0,X1),X2) ),
inference(resolution,[],[f51,f42]) ).
fof(f221,plain,
mem(e,sF2),
inference(resolution,[],[f139,f132]) ).
fof(f228,plain,
mem(sF3,sF16),
inference(resolution,[],[f124,f146]) ).
fof(f231,plain,
! [X0] : subq(e,X0),
inference(resolution,[],[f45,f42]) ).
fof(f234,plain,
mem(sF4,sF19),
inference(resolution,[],[f125,f167]) ).
fof(f238,plain,
mem(sF4,sF11),
inference(resolution,[],[f169,f125]) ).
fof(f242,plain,
! [X0] :
( mem(sK0(sF22,X0),sF21)
| mem(sK0(sF22,X0),sF13)
| subq(sF22,X0) ),
inference(resolution,[],[f179,f42]) ).
fof(f244,plain,
! [X0] :
( mem(sK0(sF22,X0),sF20)
| subq(sF22,X0)
| mem(sK0(sF22,X0),sF13)
| mem(sK0(sF22,X0),sF18) ),
inference(resolution,[],[f242,f182]) ).
fof(f289,plain,
mem(e,sF4),
inference(resolution,[],[f160,f221]) ).
fof(f310,plain,
mem(sF2,sF16),
inference(resolution,[],[f123,f150]) ).
fof(f311,plain,
mem(sF2,sF4),
inference(resolution,[],[f123,f161]) ).
fof(f317,plain,
! [X0] :
( mem(sK0(sF22,X0),sF13)
| subq(sF22,X0)
| sF19 = sK0(sF22,X0)
| mem(sK0(sF22,X0),sF18) ),
inference(resolution,[],[f213,f244]) ).
fof(f321,plain,
! [X0] :
( mem(sK0(sF22,X0),sF12)
| sF19 = sK0(sF22,X0)
| mem(sK0(sF22,X0),sF18)
| subq(sF22,X0)
| mem(sK0(sF22,X0),sF9) ),
inference(resolution,[],[f317,f177]) ).
fof(f377,plain,
! [X0] :
( mem(sK0(sF22,X0),sF18)
| sF19 = sK0(sF22,X0)
| subq(sF22,X0)
| mem(sK0(sF22,X0),sF9)
| sF11 = sK0(sF22,X0) ),
inference(resolution,[],[f321,f210]) ).
fof(f401,plain,
! [X0] :
( sF19 = sK0(sF22,X0)
| subq(sF22,X0)
| mem(sK0(sF22,X0),sF9)
| sF11 = sK0(sF22,X0)
| mem(sK0(sF22,X0),sF23) ),
inference(resolution,[],[f377,f164]) ).
fof(f403,plain,
! [X0] :
( mem(sK0(sF22,X0),sF23)
| subq(sF22,X0)
| sF11 = sK0(sF22,X0)
| sF19 = sK0(sF22,X0) ),
inference(forward_subsumption_resolution,[],[f401,f165]) ).
fof(f423,plain,
! [X0] :
( mem(sK0(sF22,X0),sF29)
| sF11 = sK0(sF22,X0)
| sF19 = sK0(sF22,X0)
| subq(sF22,X0) ),
inference(resolution,[],[f403,f154]) ).
fof(f438,plain,
( sF11 = sK0(sF22,sF29)
| sF19 = sK0(sF22,sF29)
| subq(sF22,sF29)
| subq(sF22,sF29) ),
inference(resolution,[],[f423,f43]) ).
fof(f440,plain,
( sF11 = sK0(sF22,sF29)
| sF19 = sK0(sF22,sF29)
| subq(sF22,sF29) ),
inference(duplicate_literal_removal,[],[f438]) ).
fof(f441,plain,
( sF11 = sK0(sF22,sF29)
| sF19 = sK0(sF22,sF29) ),
inference(forward_subsumption_resolution,[],[f440,f120]) ).
fof(f443,definition,
( spl30_24
<=> sF19 = sK0(sF22,sF29) ),
introduced(definition,[new_symbols(definition,[spl30_24])],[avatar_definition]) ).
fof(f444,plain,
( sF19 != sK0(sF22,sF29)
| spl30_24 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f445,plain,
( sF19 = sK0(sF22,sF29)
| ~ spl30_24 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f447,definition,
( spl30_25
<=> sF11 = sK0(sF22,sF29) ),
introduced(definition,[new_symbols(definition,[spl30_25])],[avatar_definition]) ).
fof(f449,plain,
( sF11 = sK0(sF22,sF29)
| ~ spl30_25 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f450,plain,
( spl30_24
| spl30_25 ),
inference(avatar_split_clause,[],[f441,f447,f443]) ).
fof(f484,plain,
mem(sF3,sF19),
inference(resolution,[],[f228,f166]) ).
fof(f489,plain,
mem(sF2,sF19),
inference(resolution,[],[f310,f166]) ).
fof(f623,plain,
! [X0,X1] :
( subq(X0,u(X1,X0))
| subq(X0,u(X1,X0)) ),
inference(resolution,[],[f138,f42]) ).
fof(f653,plain,
! [X0] :
( ~ mem(sK0(X0,sF29),sF28)
| subq(X0,sF29) ),
inference(superposition,[],[f138,f119]) ).
fof(f669,plain,
! [X0,X1] : subq(X0,u(X1,X0)),
inference(duplicate_literal_removal,[],[f623]) ).
fof(f672,plain,
( ~ mem(sF19,sF28)
| subq(sF22,sF29)
| ~ spl30_24 ),
inference(superposition,[],[f653,f445]) ).
fof(f675,plain,
( ~ mem(sF19,sF28)
| ~ spl30_24 ),
inference(forward_subsumption_resolution,[],[f672,f120]) ).
fof(f683,plain,
! [X0,X1] :
( subq(X0,u(X0,X1))
| subq(X0,u(X0,X1)) ),
inference(resolution,[],[f148,f42]) ).
fof(f729,plain,
! [X0,X1] : subq(X0,u(X0,X1)),
inference(duplicate_literal_removal,[],[f683]) ).
fof(f817,plain,
subq(sF16,sF19),
inference(superposition,[],[f729,f99]) ).
fof(f908,plain,
! [X0] :
( ~ subq(X0,sF5)
| mem(X0,sF6) ),
inference(superposition,[],[f57,f73]) ).
fof(f910,plain,
! [X0] :
( ~ subq(X0,sF19)
| mem(X0,sF24) ),
inference(superposition,[],[f57,f109]) ).
fof(f911,plain,
mem(sF19,sF24),
inference(resolution,[],[f910,f122]) ).
fof(f915,plain,
( mem(sF19,sF28)
| mem(sF19,sF27) ),
inference(resolution,[],[f911,f199]) ).
fof(f919,definition,
( spl30_65
<=> mem(sF19,sF25) ),
introduced(definition,[new_symbols(definition,[spl30_65])],[avatar_definition]) ).
fof(f921,plain,
( mem(sF19,sF25)
| ~ spl30_65 ),
inference(avatar_component_clause,[],[f919]) ).
fof(f923,definition,
( spl30_66
<=> mem(sF19,sF26) ),
introduced(definition,[new_symbols(definition,[spl30_66])],[avatar_definition]) ).
fof(f925,plain,
( mem(sF19,sF26)
| ~ spl30_66 ),
inference(avatar_component_clause,[],[f923]) ).
fof(f928,definition,
( spl30_67
<=> mem(sF19,sF27) ),
introduced(definition,[new_symbols(definition,[spl30_67])],[avatar_definition]) ).
fof(f930,plain,
( mem(sF19,sF27)
| ~ spl30_67 ),
inference(avatar_component_clause,[],[f928]) ).
fof(f932,definition,
( spl30_68
<=> mem(sF19,sF28) ),
introduced(definition,[new_symbols(definition,[spl30_68])],[avatar_definition]) ).
fof(f935,plain,
( spl30_67
| spl30_68 ),
inference(avatar_split_clause,[],[f915,f932,f928]) ).
fof(f941,plain,
( ~ mem(sF11,sF28)
| subq(sF22,sF29)
| ~ spl30_25 ),
inference(superposition,[],[f653,f449]) ).
fof(f943,plain,
( ~ mem(sF11,sF29)
| subq(sF22,sF29)
| ~ spl30_25 ),
inference(superposition,[],[f43,f449]) ).
fof(f944,plain,
( ~ mem(sF11,sF29)
| ~ spl30_25 ),
inference(forward_subsumption_resolution,[],[f943,f120]) ).
fof(f945,plain,
( ~ mem(sF11,sF28)
| ~ spl30_25 ),
inference(forward_subsumption_resolution,[],[f941,f120]) ).
fof(f949,plain,
( mem(sF19,sF26)
| mem(sF19,sF25)
| ~ spl30_67 ),
inference(resolution,[],[f930,f185]) ).
fof(f950,plain,
( spl30_65
| spl30_66
| ~ spl30_67 ),
inference(avatar_split_clause,[],[f949,f928,f923,f919]) ).
fof(f951,plain,
( subq(sF19,sF16)
| ~ spl30_65 ),
inference(resolution,[],[f921,f136]) ).
fof(f959,plain,
mem(sF5,sF6),
inference(resolution,[],[f908,f122]) ).
fof(f962,plain,
mem(sF5,sF9),
inference(resolution,[],[f959,f151]) ).
fof(f965,plain,
mem(sF5,sF23),
inference(resolution,[],[f962,f165]) ).
fof(f969,plain,
mem(sF5,sF29),
inference(resolution,[],[f965,f154]) ).
fof(f1127,definition,
( spl30_81
<=> mem(sF19,sF17) ),
introduced(definition,[new_symbols(definition,[spl30_81])],[avatar_definition]) ).
fof(f1128,plain,
( ~ mem(sF19,sF17)
| spl30_81 ),
inference(avatar_component_clause,[],[f1127]) ).
fof(f1129,plain,
( mem(sF19,sF17)
| ~ spl30_81 ),
inference(avatar_component_clause,[],[f1127]) ).
fof(f1157,plain,
! [X2,X0,X1] :
( subq(m(s(X0),X1),X2)
| sK0(m(s(X0),X1),X2) = X0 ),
inference(resolution,[],[f193,f46]) ).
fof(f1323,plain,
! [X0,X1] :
( ~ subq(s(X0),X1)
| mem(X0,X1) ),
inference(resolution,[],[f41,f61]) ).
fof(f1325,plain,
! [X2,X3,X0,X1] :
( ~ subq(u(X2,X3),X1)
| mem(X0,X1)
| ~ mem(X0,X3) ),
inference(resolution,[],[f41,f49]) ).
fof(f1342,plain,
! [X2,X0,X1] :
( mem(sK0(X0,X1),X2)
| ~ subq(X0,X2)
| subq(X0,X1) ),
inference(resolution,[],[f41,f42]) ).
fof(f1349,plain,
! [X0,X1] :
( mem(sK0(sF22,X0),sF18)
| mem(sK0(sF22,X0),X1)
| sF19 = sK0(sF22,X0)
| ~ subq(sF12,X1)
| subq(sF22,X0)
| mem(sK0(sF22,X0),sF9) ),
inference(resolution,[],[f41,f321]) ).
fof(f1382,plain,
! [X0] :
( ~ subq(sF11,X0)
| mem(sF4,X0) ),
inference(resolution,[],[f41,f238]) ).
fof(f1462,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF10)
| subq(X0,X1)
| mem(sK0(X0,X1),sF5)
| ~ subq(X0,sF11) ),
inference(resolution,[],[f1342,f178]) ).
fof(f1634,plain,
! [X0,X1] :
( mem(sK0(u(X0,X1),X1),X0)
| subq(u(X0,X1),X1)
| subq(u(X0,X1),X1) ),
inference(resolution,[],[f170,f43]) ).
fof(f1824,plain,
! [X0,X1] :
( mem(sK0(u(X0,X1),X1),X0)
| subq(u(X0,X1),X1) ),
inference(duplicate_literal_removal,[],[f1634]) ).
fof(f2328,plain,
! [X0,X1] :
( mem(X0,X1)
| sK0(s(X0),X1) = X0 ),
inference(resolution,[],[f1323,f202]) ).
fof(f2543,definition,
( spl30_156
<=> ! [X0] : subq(sF2,X0) ),
introduced(definition,[new_symbols(definition,[spl30_156])],[avatar_definition]) ).
fof(f2544,plain,
( ! [X0] : subq(sF2,X0)
| ~ spl30_156 ),
inference(avatar_component_clause,[],[f2543]) ).
fof(f3158,definition,
( spl30_172
<=> mem(e,sF3) ),
introduced(definition,[new_symbols(definition,[spl30_172])],[avatar_definition]) ).
fof(f3159,plain,
( ~ mem(e,sF3)
| spl30_172 ),
inference(avatar_component_clause,[],[f3158]) ).
fof(f3160,plain,
( mem(e,sF3)
| ~ spl30_172 ),
inference(avatar_component_clause,[],[f3158]) ).
fof(f3166,plain,
( e = sF2
| ~ spl30_172 ),
inference(resolution,[],[f3160,f205]) ).
fof(f3170,plain,
( ! [X0] : ~ mem(X0,sF2)
| ~ spl30_172 ),
inference(superposition,[],[f45,f3166]) ).
fof(f3174,plain,
( mem(sF2,sF2)
| ~ spl30_172 ),
inference(superposition,[],[f221,f3166]) ).
fof(f3299,plain,
( $false
| ~ spl30_172 ),
inference(forward_subsumption_resolution,[],[f3174,f3170]) ).
fof(f3300,plain,
~ spl30_172,
inference(avatar_contradiction_clause,[],[f3299]) ).
fof(f3970,plain,
! [X0,X1] :
( ~ subq(sF2,X0)
| mem(X1,X0)
| ~ mem(X1,sF1) ),
inference(superposition,[],[f1325,f65]) ).
fof(f3984,plain,
( ! [X0,X1] :
( ~ mem(X1,sF1)
| mem(X1,X0) )
| ~ spl30_156 ),
inference(forward_subsumption_resolution,[],[f3970,f2544]) ).
fof(f3986,plain,
( ! [X0] : mem(e,X0)
| ~ spl30_156 ),
inference(resolution,[],[f3984,f132]) ).
fof(f4002,plain,
( ! [X0] : ~ mem(e,X0)
| ~ spl30_156 ),
inference(resolution,[],[f3986,f51]) ).
fof(f4079,plain,
( $false
| ~ spl30_156 ),
inference(forward_subsumption_resolution,[],[f4002,f3986]) ).
fof(f4080,plain,
~ spl30_156,
inference(avatar_contradiction_clause,[],[f4079]) ).
fof(f4417,plain,
! [X0] :
( subq(u(X0,X0),X0)
| subq(u(X0,X0),X0) ),
inference(resolution,[],[f1824,f43]) ).
fof(f4511,plain,
! [X0] : subq(u(X0,X0),X0),
inference(duplicate_literal_removal,[],[f4417]) ).
fof(f4924,plain,
( ~ spl30_68
| ~ spl30_24 ),
inference(avatar_split_clause,[],[f675,f443,f932]) ).
fof(f5144,definition,
( spl30_334
<=> ! [X0] :
( mem(sK0(sF22,X0),sF18)
| mem(sK0(sF22,X0),sF9)
| sF19 = sK0(sF22,X0)
| subq(sF22,X0) ) ),
introduced(definition,[new_symbols(definition,[spl30_334])],[avatar_definition]) ).
fof(f5145,plain,
( ! [X0] :
( mem(sK0(sF22,X0),sF18)
| mem(sK0(sF22,X0),sF9)
| sF19 = sK0(sF22,X0)
| subq(sF22,X0) )
| ~ spl30_334 ),
inference(avatar_component_clause,[],[f5144]) ).
fof(f5641,definition,
( spl30_405
<=> e = sF2 ),
introduced(definition,[new_symbols(definition,[spl30_405])],[avatar_definition]) ).
fof(f5642,plain,
( e != sF2
| spl30_405 ),
inference(avatar_component_clause,[],[f5641]) ).
fof(f5643,plain,
( e = sF2
| ~ spl30_405 ),
inference(avatar_component_clause,[],[f5641]) ).
fof(f6975,plain,
( ! [X0] :
( mem(sK0(sF22,X0),sF9)
| sF19 = sK0(sF22,X0)
| subq(sF22,X0)
| mem(sK0(sF22,X0),sF23) )
| ~ spl30_334 ),
inference(resolution,[],[f5145,f164]) ).
fof(f6987,plain,
( ! [X0] :
( mem(sK0(sF22,X0),sF23)
| subq(sF22,X0)
| sF19 = sK0(sF22,X0) )
| ~ spl30_334 ),
inference(forward_subsumption_resolution,[],[f6975,f165]) ).
fof(f6994,plain,
( ! [X0] :
( mem(sK0(sF22,X0),sF29)
| sF19 = sK0(sF22,X0)
| subq(sF22,X0) )
| ~ spl30_334 ),
inference(resolution,[],[f6987,f154]) ).
fof(f7011,plain,
( sF19 = sK0(sF22,sF29)
| subq(sF22,sF29)
| subq(sF22,sF29)
| ~ spl30_334 ),
inference(resolution,[],[f6994,f43]) ).
fof(f7026,plain,
( sF19 = sK0(sF22,sF29)
| subq(sF22,sF29)
| ~ spl30_334 ),
inference(duplicate_literal_removal,[],[f7011]) ).
fof(f7027,plain,
( sF19 = sK0(sF22,sF29)
| ~ spl30_334 ),
inference(forward_subsumption_resolution,[],[f7026,f120]) ).
fof(f7028,plain,
( sF11 = sF19
| ~ spl30_25
| ~ spl30_334 ),
inference(forward_demodulation,[],[f7027,f449]) ).
fof(f7159,definition,
( spl30_420
<=> mem(sF2,sF5) ),
introduced(definition,[new_symbols(definition,[spl30_420])],[avatar_definition]) ).
fof(f7160,plain,
( ~ mem(sF2,sF5)
| spl30_420 ),
inference(avatar_component_clause,[],[f7159]) ).
fof(f7161,plain,
( mem(sF2,sF5)
| ~ spl30_420 ),
inference(avatar_component_clause,[],[f7159]) ).
fof(f7207,plain,
( sF2 = sF4
| ~ spl30_420 ),
inference(resolution,[],[f7161,f207]) ).
fof(f7219,plain,
( mem(sF2,sF2)
| ~ spl30_420 ),
inference(superposition,[],[f311,f7207]) ).
fof(f7415,plain,
( mem(sF2,sF1)
| ~ spl30_420 ),
inference(resolution,[],[f7219,f186]) ).
fof(f7418,plain,
( e = sF2
| ~ spl30_420 ),
inference(resolution,[],[f7415,f204]) ).
fof(f7421,plain,
( $false
| spl30_405
| ~ spl30_420 ),
inference(forward_subsumption_resolution,[],[f7418,f5642]) ).
fof(f7422,plain,
( spl30_405
| ~ spl30_420 ),
inference(avatar_contradiction_clause,[],[f7421]) ).
fof(f7576,plain,
( ! [X0] : subq(sF2,X0)
| ~ spl30_405 ),
inference(superposition,[],[f231,f5643]) ).
fof(f7605,plain,
( spl30_156
| ~ spl30_405 ),
inference(avatar_split_clause,[],[f7576,f5641,f2543]) ).
fof(f7609,plain,
( sF11 != sF19
| spl30_24
| ~ spl30_25 ),
inference(forward_demodulation,[],[f444,f449]) ).
fof(f7815,definition,
( spl30_429
<=> subq(sF19,sF16) ),
introduced(definition,[new_symbols(definition,[spl30_429])],[avatar_definition]) ).
fof(f7816,plain,
( ~ subq(sF19,sF16)
| spl30_429 ),
inference(avatar_component_clause,[],[f7815]) ).
fof(f7817,plain,
( subq(sF19,sF16)
| ~ spl30_429 ),
inference(avatar_component_clause,[],[f7815]) ).
fof(f7912,plain,
! [X0] :
( ~ subq(X0,e)
| e = X0 ),
inference(resolution,[],[f44,f231]) ).
fof(f7914,plain,
! [X0] :
( u(X0,X0) = X0
| ~ subq(X0,u(X0,X0)) ),
inference(resolution,[],[f44,f4511]) ).
fof(f8074,plain,
! [X0] : u(X0,X0) = X0,
inference(forward_subsumption_resolution,[],[f7914,f669]) ).
fof(f8891,definition,
( spl30_452
<=> mem(sF4,sF3) ),
introduced(definition,[new_symbols(definition,[spl30_452])],[avatar_definition]) ).
fof(f8892,plain,
( mem(sF4,sF3)
| ~ spl30_452 ),
inference(avatar_component_clause,[],[f8891]) ).
fof(f8893,plain,
( ~ mem(sF4,sF3)
| spl30_452 ),
inference(avatar_component_clause,[],[f8891]) ).
fof(f9169,plain,
( sF16 = sF19
| ~ spl30_81 ),
inference(resolution,[],[f1129,f212]) ).
fof(f9176,plain,
( mem(sF4,sF16)
| ~ spl30_81 ),
inference(superposition,[],[f234,f9169]) ).
fof(f9461,plain,
( $false
| ~ spl30_65
| spl30_429 ),
inference(forward_subsumption_resolution,[],[f951,f7816]) ).
fof(f9462,plain,
( ~ spl30_65
| spl30_429 ),
inference(avatar_contradiction_clause,[],[f9461]) ).
fof(f9786,plain,
( mem(sF4,sF10)
| mem(sF4,sF3)
| ~ spl30_81 ),
inference(resolution,[],[f9176,f175]) ).
fof(f9788,plain,
( mem(sF4,sF10)
| ~ spl30_81
| spl30_452 ),
inference(forward_subsumption_resolution,[],[f9786,f8893]) ).
fof(f9845,plain,
( sF3 = sF4
| ~ spl30_81
| spl30_452 ),
inference(resolution,[],[f9788,f206]) ).
fof(f9856,plain,
( mem(e,sF3)
| ~ spl30_81
| spl30_452 ),
inference(superposition,[],[f289,f9845]) ).
fof(f9860,plain,
( $false
| ~ spl30_81
| spl30_172
| spl30_452 ),
inference(forward_subsumption_resolution,[],[f9856,f3159]) ).
fof(f9861,plain,
( ~ spl30_81
| spl30_172
| spl30_452 ),
inference(avatar_contradiction_clause,[],[f9860]) ).
fof(f9963,plain,
( sF2 = sF4
| ~ spl30_452 ),
inference(resolution,[],[f8892,f205]) ).
fof(f9969,plain,
( mem(sF2,sF5)
| ~ spl30_452 ),
inference(superposition,[],[f125,f9963]) ).
fof(f9979,plain,
( $false
| spl30_420
| ~ spl30_452 ),
inference(forward_subsumption_resolution,[],[f9969,f7160]) ).
fof(f9980,plain,
( spl30_420
| ~ spl30_452 ),
inference(avatar_contradiction_clause,[],[f9979]) ).
fof(f10765,plain,
! [X0,X1] :
( sK0(m(s(X0),X1),e) = X0
| e = m(s(X0),X1) ),
inference(resolution,[],[f7912,f1157]) ).
fof(f11086,plain,
( sF16 = sF19
| ~ subq(sF16,sF19)
| ~ spl30_429 ),
inference(resolution,[],[f7817,f44]) ).
fof(f11096,plain,
( sF16 = sF19
| ~ spl30_429 ),
inference(forward_subsumption_resolution,[],[f11086,f817]) ).
fof(f11154,plain,
( ~ mem(sF16,sF17)
| spl30_81
| ~ spl30_429 ),
inference(superposition,[],[f1128,f11096]) ).
fof(f11177,plain,
( $false
| spl30_81
| ~ spl30_429 ),
inference(forward_subsumption_resolution,[],[f11154,f127]) ).
fof(f11178,plain,
( spl30_81
| ~ spl30_429 ),
inference(avatar_contradiction_clause,[],[f11177]) ).
fof(f12004,definition,
( spl30_514
<=> subq(sF12,sF26) ),
introduced(definition,[new_symbols(definition,[spl30_514])],[avatar_definition]) ).
fof(f12005,plain,
( subq(sF12,sF26)
| ~ spl30_514 ),
inference(avatar_component_clause,[],[f12004]) ).
fof(f12006,plain,
( ~ subq(sF12,sF26)
| spl30_514 ),
inference(avatar_component_clause,[],[f12004]) ).
fof(f19532,plain,
( sF5 = sF19
| ~ spl30_66 ),
inference(resolution,[],[f925,f208]) ).
fof(f19543,plain,
( mem(sF2,sF5)
| ~ spl30_66 ),
inference(superposition,[],[f489,f19532]) ).
fof(f19596,plain,
( $false
| ~ spl30_66
| spl30_420 ),
inference(forward_subsumption_resolution,[],[f19543,f7160]) ).
fof(f19597,plain,
( ~ spl30_66
| spl30_420 ),
inference(avatar_contradiction_clause,[],[f19596]) ).
fof(f22672,definition,
( spl30_798
<=> mem(sF11,sF25) ),
introduced(definition,[new_symbols(definition,[spl30_798])],[avatar_definition]) ).
fof(f22673,plain,
( ~ mem(sF11,sF25)
| spl30_798 ),
inference(avatar_component_clause,[],[f22672]) ).
fof(f22674,plain,
( mem(sF11,sF25)
| ~ spl30_798 ),
inference(avatar_component_clause,[],[f22672]) ).
fof(f22676,definition,
( spl30_799
<=> mem(sF11,sF26) ),
introduced(definition,[new_symbols(definition,[spl30_799])],[avatar_definition]) ).
fof(f22677,plain,
( ~ mem(sF11,sF26)
| spl30_799 ),
inference(avatar_component_clause,[],[f22676]) ).
fof(f22680,plain,
( subq(sF11,sF16)
| ~ spl30_798 ),
inference(resolution,[],[f22674,f136]) ).
fof(f28673,plain,
! [X0,X1] :
( ~ mem(X0,X1)
| subq(m(s(X0),X1),e)
| e = m(s(X0),X1) ),
inference(superposition,[],[f217,f10765]) ).
fof(f28722,plain,
! [X0,X1] :
( ~ mem(X0,X1)
| e = m(s(X0),X1) ),
inference(forward_subsumption_resolution,[],[f28673,f7912]) ).
fof(f28893,plain,
e = m(s(sF3),sF19),
inference(resolution,[],[f28722,f484]) ).
fof(f28902,plain,
e = m(s(sF5),sF9),
inference(resolution,[],[f28722,f962]) ).
fof(f28910,plain,
e = m(s(sF5),sF29),
inference(resolution,[],[f28722,f969]) ).
fof(f29039,plain,
e = m(sF26,sF29),
inference(forward_demodulation,[],[f28910,f113]) ).
fof(f29047,plain,
e = m(sF26,sF9),
inference(forward_demodulation,[],[f28902,f113]) ).
fof(f29056,plain,
e = m(sF10,sF19),
inference(forward_demodulation,[],[f28893,f81]) ).
fof(f29338,plain,
! [X0] :
( mem(X0,e)
| ~ mem(X0,sF26)
| mem(X0,sF29) ),
inference(superposition,[],[f53,f29039]) ).
fof(f29352,plain,
! [X0] :
( ~ mem(X0,sF26)
| mem(X0,sF29) ),
inference(forward_subsumption_resolution,[],[f29338,f45]) ).
fof(f29575,plain,
! [X0] :
( mem(X0,sF29)
| sK0(s(X0),sF26) = X0 ),
inference(resolution,[],[f29352,f2328]) ).
fof(f29648,plain,
! [X0] :
( mem(X0,e)
| ~ mem(X0,sF26)
| mem(X0,sF9) ),
inference(superposition,[],[f53,f29047]) ).
fof(f29662,plain,
! [X0] :
( ~ mem(X0,sF26)
| mem(X0,sF9) ),
inference(forward_subsumption_resolution,[],[f29648,f45]) ).
fof(f29676,plain,
! [X0] :
( mem(sK0(sF22,X0),sF9)
| mem(sK0(sF22,X0),sF18)
| sF19 = sK0(sF22,X0)
| ~ subq(sF12,sF26)
| subq(sF22,X0)
| mem(sK0(sF22,X0),sF9) ),
inference(resolution,[],[f29662,f1349]) ).
fof(f29691,plain,
! [X0] :
( mem(sK0(sF22,X0),sF9)
| mem(sK0(sF22,X0),sF18)
| sF19 = sK0(sF22,X0)
| ~ subq(sF12,sF26)
| subq(sF22,X0) ),
inference(duplicate_literal_removal,[],[f29676]) ).
fof(f30214,plain,
! [X0] :
( mem(X0,e)
| ~ mem(X0,sF10)
| mem(X0,sF19) ),
inference(superposition,[],[f53,f29056]) ).
fof(f30228,plain,
! [X0] :
( ~ mem(X0,sF10)
| mem(X0,sF19) ),
inference(forward_subsumption_resolution,[],[f30214,f45]) ).
fof(f32904,plain,
( sF11 = sK0(s(sF11),sF26)
| ~ spl30_25 ),
inference(resolution,[],[f29575,f944]) ).
fof(f32905,plain,
( sF11 = sK0(sF12,sF26)
| ~ spl30_25 ),
inference(forward_demodulation,[],[f32904,f85]) ).
fof(f32909,plain,
( ~ mem(sF11,sF26)
| subq(sF12,sF26)
| ~ spl30_25 ),
inference(superposition,[],[f43,f32905]) ).
fof(f32922,plain,
( ~ mem(sF11,sF26)
| ~ spl30_25
| spl30_514 ),
inference(forward_subsumption_resolution,[],[f32909,f12006]) ).
fof(f32923,plain,
( ~ spl30_799
| ~ spl30_25
| spl30_514 ),
inference(avatar_split_clause,[],[f32922,f12004,f447,f22676]) ).
fof(f36611,definition,
( spl30_1138
<=> sF3 = sF4 ),
introduced(definition,[new_symbols(definition,[spl30_1138])],[avatar_definition]) ).
fof(f36613,plain,
( sF3 = sF4
| ~ spl30_1138 ),
inference(avatar_component_clause,[],[f36611]) ).
fof(f38588,plain,
( ! [X0] :
( mem(sK0(sF22,X0),sF9)
| mem(sK0(sF22,X0),sF18)
| sF19 = sK0(sF22,X0)
| subq(sF22,X0) )
| ~ spl30_514 ),
inference(forward_subsumption_resolution,[],[f29691,f12005]) ).
fof(f38630,plain,
( spl30_334
| ~ spl30_514 ),
inference(avatar_split_clause,[],[f38588,f12004,f5144]) ).
fof(f38648,definition,
( spl30_1237
<=> subq(sF11,sF16) ),
introduced(definition,[new_symbols(definition,[spl30_1237])],[avatar_definition]) ).
fof(f38650,plain,
( subq(sF11,sF16)
| ~ spl30_1237 ),
inference(avatar_component_clause,[],[f38648]) ).
fof(f38805,definition,
( spl30_1246
<=> mem(sF11,sF27) ),
introduced(definition,[new_symbols(definition,[spl30_1246])],[avatar_definition]) ).
fof(f38806,plain,
( ~ mem(sF11,sF27)
| spl30_1246 ),
inference(avatar_component_clause,[],[f38805]) ).
fof(f38807,plain,
( mem(sF11,sF27)
| ~ spl30_1246 ),
inference(avatar_component_clause,[],[f38805]) ).
fof(f38815,definition,
( spl30_1247
<=> mem(sF11,sF24) ),
introduced(definition,[new_symbols(definition,[spl30_1247])],[avatar_definition]) ).
fof(f38816,plain,
( ~ mem(sF11,sF24)
| spl30_1247 ),
inference(avatar_component_clause,[],[f38815]) ).
fof(f38817,plain,
( mem(sF11,sF24)
| ~ spl30_1247 ),
inference(avatar_component_clause,[],[f38815]) ).
fof(f38825,definition,
( spl30_1248
<=> subq(sF11,sF19) ),
introduced(definition,[new_symbols(definition,[spl30_1248])],[avatar_definition]) ).
fof(f38826,plain,
( ~ subq(sF11,sF19)
| spl30_1248 ),
inference(avatar_component_clause,[],[f38825]) ).
fof(f38827,plain,
( subq(sF11,sF19)
| ~ spl30_1248 ),
inference(avatar_component_clause,[],[f38825]) ).
fof(f38855,plain,
( mem(sF11,sF28)
| mem(sF11,sF27)
| ~ spl30_1247 ),
inference(resolution,[],[f38817,f199]) ).
fof(f38859,plain,
( mem(sF11,sF26)
| mem(sF11,sF25)
| ~ spl30_1246 ),
inference(resolution,[],[f38807,f185]) ).
fof(f38863,plain,
( mem(sF11,sF25)
| spl30_799
| ~ spl30_1246 ),
inference(forward_subsumption_resolution,[],[f38859,f22677]) ).
fof(f38864,plain,
( $false
| spl30_798
| spl30_799
| ~ spl30_1246 ),
inference(forward_subsumption_resolution,[],[f38863,f22673]) ).
fof(f38865,plain,
( spl30_798
| spl30_799
| ~ spl30_1246 ),
inference(avatar_contradiction_clause,[],[f38864]) ).
fof(f38866,plain,
( mem(sF11,sF27)
| ~ spl30_25
| ~ spl30_1247 ),
inference(forward_subsumption_resolution,[],[f38855,f945]) ).
fof(f38869,plain,
( $false
| ~ spl30_25
| spl30_1246
| ~ spl30_1247 ),
inference(forward_subsumption_resolution,[],[f38866,f38806]) ).
fof(f38870,plain,
( ~ spl30_25
| spl30_1246
| ~ spl30_1247 ),
inference(avatar_contradiction_clause,[],[f38869]) ).
fof(f39553,plain,
( mem(sF11,sF24)
| ~ spl30_1248 ),
inference(resolution,[],[f38827,f910]) ).
fof(f39556,plain,
( $false
| spl30_1247
| ~ spl30_1248 ),
inference(forward_subsumption_resolution,[],[f39553,f38816]) ).
fof(f39557,plain,
( spl30_1247
| ~ spl30_1248 ),
inference(avatar_contradiction_clause,[],[f39556]) ).
fof(f44679,plain,
! [X0,X1] :
( subq(X0,X1)
| mem(sK0(X0,X1),sF5)
| ~ subq(X0,sF11)
| mem(sK0(X0,X1),sF19) ),
inference(resolution,[],[f1462,f30228]) ).
fof(f45107,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF19)
| ~ subq(X0,sF11)
| subq(X0,X1) ),
inference(forward_subsumption_resolution,[],[f44679,f167]) ).
fof(f45448,plain,
! [X0] :
( ~ subq(X0,sF11)
| subq(X0,sF19)
| subq(X0,sF19) ),
inference(resolution,[],[f45107,f43]) ).
fof(f45683,plain,
! [X0] :
( ~ subq(X0,sF11)
| subq(X0,sF19) ),
inference(duplicate_literal_removal,[],[f45448]) ).
fof(f45713,plain,
subq(u(sF11,sF11),sF19),
inference(resolution,[],[f45683,f4511]) ).
fof(f45768,plain,
subq(sF11,sF19),
inference(forward_demodulation,[],[f45713,f8074]) ).
fof(f45776,plain,
( $false
| spl30_1248 ),
inference(forward_subsumption_resolution,[],[f45768,f38826]) ).
fof(f45777,plain,
spl30_1248,
inference(avatar_contradiction_clause,[],[f45776]) ).
fof(f45825,plain,
( spl30_1237
| ~ spl30_798 ),
inference(avatar_split_clause,[],[f22680,f22672,f38648]) ).
fof(f57561,plain,
( mem(sF4,sF16)
| ~ spl30_1237 ),
inference(resolution,[],[f1382,f38650]) ).
fof(f57588,plain,
( mem(sF4,sF10)
| mem(sF4,sF3)
| ~ spl30_1237 ),
inference(resolution,[],[f57561,f175]) ).
fof(f57595,plain,
( mem(sF4,sF10)
| spl30_452
| ~ spl30_1237 ),
inference(forward_subsumption_resolution,[],[f57588,f8893]) ).
fof(f57598,plain,
( sF3 = sF4
| spl30_452
| ~ spl30_1237 ),
inference(resolution,[],[f57595,f206]) ).
fof(f57617,plain,
( spl30_1138
| spl30_452
| ~ spl30_1237 ),
inference(avatar_split_clause,[],[f57598,f38648,f8891,f36611]) ).
fof(f57670,plain,
( mem(e,sF3)
| ~ spl30_1138 ),
inference(superposition,[],[f289,f36613]) ).
fof(f57708,plain,
( $false
| spl30_172
| ~ spl30_1138 ),
inference(forward_subsumption_resolution,[],[f57670,f3159]) ).
fof(f57709,plain,
( spl30_172
| ~ spl30_1138 ),
inference(avatar_contradiction_clause,[],[f57708]) ).
fof(f58041,plain,
( $false
| spl30_24
| ~ spl30_25
| ~ spl30_334 ),
inference(forward_subsumption_resolution,[],[f7609,f7028]) ).
fof(f58042,plain,
( spl30_24
| ~ spl30_25
| ~ spl30_334 ),
inference(avatar_contradiction_clause,[],[f58041]) ).
cnf(s9,plain,
( spl30_24
| spl30_25 ),
inference(sat_conversion,[],[f450]) ).
cnf(s24,plain,
( spl30_67
| spl30_68 ),
inference(sat_conversion,[],[f935]) ).
cnf(s25,plain,
( spl30_65
| spl30_66
| ~ spl30_67 ),
inference(sat_conversion,[],[f950]) ).
cnf(s112,plain,
~ spl30_172,
inference(sat_conversion,[],[f3300]) ).
cnf(s166,plain,
~ spl30_156,
inference(sat_conversion,[],[f4080]) ).
cnf(s219,plain,
( ~ spl30_24
| ~ spl30_68 ),
inference(sat_conversion,[],[f4924]) ).
cnf(s359,plain,
( spl30_405
| ~ spl30_420 ),
inference(sat_conversion,[],[f7422]) ).
cnf(s365,plain,
( spl30_156
| ~ spl30_405 ),
inference(sat_conversion,[],[f7605]) ).
cnf(s539,plain,
( ~ spl30_65
| spl30_429 ),
inference(sat_conversion,[],[f9462]) ).
cnf(s585,plain,
( ~ spl30_81
| spl30_172
| spl30_452 ),
inference(sat_conversion,[],[f9861]) ).
cnf(s587,plain,
( spl30_420
| ~ spl30_452 ),
inference(sat_conversion,[],[f9980]) ).
cnf(s663,plain,
( spl30_81
| ~ spl30_429 ),
inference(sat_conversion,[],[f11178]) ).
cnf(s1101,plain,
( ~ spl30_66
| spl30_420 ),
inference(sat_conversion,[],[f19597]) ).
cnf(s1811,plain,
( ~ spl30_25
| spl30_514
| ~ spl30_799 ),
inference(sat_conversion,[],[f32923]) ).
cnf(s2068,plain,
( spl30_334
| ~ spl30_514 ),
inference(sat_conversion,[],[f38630]) ).
cnf(s2122,plain,
( spl30_798
| spl30_799
| ~ spl30_1246 ),
inference(sat_conversion,[],[f38865]) ).
cnf(s2124,plain,
( ~ spl30_25
| spl30_1246
| ~ spl30_1247 ),
inference(sat_conversion,[],[f38870]) ).
cnf(s2143,plain,
( spl30_1247
| ~ spl30_1248 ),
inference(sat_conversion,[],[f39557]) ).
cnf(s2554,plain,
spl30_1248,
inference(sat_conversion,[],[f45777]) ).
cnf(s2567,plain,
( ~ spl30_798
| spl30_1237 ),
inference(sat_conversion,[],[f45825]) ).
cnf(s3070,plain,
( spl30_452
| spl30_1138
| ~ spl30_1237 ),
inference(sat_conversion,[],[f57617]) ).
cnf(s3079,plain,
( spl30_172
| ~ spl30_1138 ),
inference(sat_conversion,[],[f57709]) ).
cnf(s3134,plain,
( spl30_24
| ~ spl30_25
| ~ spl30_334 ),
inference(sat_conversion,[],[f58042]) ).
cnf(s3172,plain,
spl30_1247,
inference(rat,[],[s2143,s2554]) ).
cnf(s3174,plain,
( ~ spl30_25
| spl30_1246 ),
inference(rat,[],[s2124,s3172]) ).
cnf(s3236,plain,
~ spl30_405,
inference(rat,[],[s365,s166]) ).
cnf(s3237,plain,
~ spl30_420,
inference(rat,[],[s359,s3236]) ).
cnf(s3243,plain,
~ spl30_66,
inference(rat,[],[s1101,s3237]) ).
cnf(s3245,plain,
~ spl30_452,
inference(rat,[],[s587,s3237]) ).
cnf(s3260,plain,
~ spl30_1138,
inference(rat,[],[s3079,s112]) ).
cnf(s3266,plain,
~ spl30_81,
inference(rat,[],[s585,s3245,s112]) ).
cnf(s3269,plain,
~ spl30_1237,
inference(rat,[],[s3070,s3245,s3260]) ).
cnf(s3279,plain,
~ spl30_429,
inference(rat,[],[s663,s3266]) ).
cnf(s3281,plain,
~ spl30_798,
inference(rat,[],[s2567,s3269]) ).
cnf(s3290,plain,
~ spl30_65,
inference(rat,[],[s539,s3279]) ).
cnf(s3385,plain,
~ spl30_67,
inference(rat,[],[s25,s3243,s3290]) ).
cnf(s3386,plain,
spl30_68,
inference(rat,[],[s24,s3385]) ).
cnf(s3392,plain,
~ spl30_24,
inference(rat,[],[s219,s3386]) ).
cnf(s3394,plain,
spl30_25,
inference(rat,[],[s9,s3392]) ).
cnf(s3395,plain,
~ spl30_334,
inference(rat,[],[s3134,s3392,s3394]) ).
cnf(s3397,plain,
spl30_1246,
inference(rat,[],[s3174,s3394]) ).
cnf(s3408,plain,
~ spl30_514,
inference(rat,[],[s2068,s3395]) ).
cnf(s3421,plain,
spl30_799,
inference(rat,[],[s2122,s3281,s3397]) ).
cnf(s3429,plain,
$false,
inference(rat,[],[s1811,s3394,s3421,s3408]) ).
fof(f58195,plain,
$false,
inference(avatar_sat_refutation,[],[s3429]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV576+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.11/0.36 % Computer : n015.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 28 06:43:01 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/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.70/2.32 % (2429939)Detected formulas, will run a generic FOF schedule.
% 10.70/2.32 % (2429945)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=1738439790:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.70/2.32 % (2429950)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=631858886:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.70/2.32 % (2429947)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=3332841282:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.70/2.32 % (2429948)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=556821530:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.70/2.32 % (2429946)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=173711453:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.70/2.33 % (2429948)Refutation not found, incomplete strategy
% 10.70/2.33 % (2429948)------------------------------
% 10.70/2.33 % (2429948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.33 % (2429948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.33 % (2429948)CaDiCaL version: 2.1.3
% 10.70/2.33 % (2429948)Termination reason: Refutation not found, incomplete strategy
% 10.70/2.33 % (2429948)Time elapsed: 0.002 s
% 10.70/2.33 % (2429948)Peak memory usage: 88 MB
% 10.70/2.33 % (2429948)Instructions burned: 1 (million)
% 10.70/2.33 % (2429949)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2567721383:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.70/2.33 % (2429951)dis-21_1_sil=8000:lcm=predicate:random_seed=3161520333: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.70/2.33 % (2429951)Instruction limit reached!
% 10.70/2.33 % (2429951)------------------------------
% 10.70/2.33 % (2429951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.33 % (2429951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.33 % (2429951)CaDiCaL version: 2.1.3
% 10.70/2.33 % (2429951)Termination reason: Instruction limit
% 10.70/2.33 % (2429951)Termination phase: Saturation
% 10.70/2.33 % (2429951)Time elapsed: 0.063 s
% 10.70/2.33 % (2429951)Peak memory usage: 88 MB
% 10.70/2.33 % (2429951)Instructions burned: 129 (million)
% 10.70/2.33 % (2429949)Instruction limit reached!
% 10.70/2.33 % (2429949)------------------------------
% 10.70/2.33 % (2429949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.33 % (2429949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.33 % (2429949)CaDiCaL version: 2.1.3
% 10.70/2.33 % (2429949)Termination reason: Instruction limit
% 10.70/2.33 % (2429949)Termination phase: Saturation
% 10.70/2.33 % (2429949)Time elapsed: 0.073 s
% 10.70/2.33 % (2429949)Peak memory usage: 89 MB
% 10.70/2.33 % (2429949)Instructions burned: 120 (million)
% 10.70/2.33 % (2429950)Instruction limit reached!
% 10.70/2.33 % (2429950)------------------------------
% 10.70/2.33 % (2429950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.33 % (2429950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.33 % (2429950)CaDiCaL version: 2.1.3
% 10.70/2.33 % (2429950)Termination reason: Instruction limit
% 10.70/2.33 % (2429950)Termination phase: Saturation
% 10.70/2.33 % (2429950)Time elapsed: 0.097 s
% 10.70/2.33 % (2429950)Peak memory usage: 89 MB
% 10.70/2.33 % (2429950)Instructions burned: 139 (million)
% 10.70/2.33 % (2429959)lrs+10_1_sil=8000:sp=occurrence:random_seed=1415651941:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.70/2.33 % (2429960)lrs+10_1_sil=32000:urr=on:br=off:random_seed=408919383:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.70/2.33 % (2429961)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2252400971:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 10.70/2.33 % (2429948)------------------------------
% 10.70/2.33 % (2429948)------------------------------
% 10.70/2.33 % (2429960)Instruction limit reached!
% 10.70/2.33 % (2429960)------------------------------
% 10.70/2.33 % (2429960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.32/3.62 % (2429960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.32/3.62 % (2429960)CaDiCaL version: 2.1.3
% 19.32/3.62 % (2429960)Termination reason: Instruction limit
% 19.32/3.62 % (2429960)Termination phase: Saturation
% 19.32/3.62 % (2429960)Time elapsed: 0.084 s
% 19.32/3.62 % (2429960)Peak memory usage: 90 MB
% 19.32/3.62 % (2429960)Instructions burned: 157 (million)
% 19.32/3.62 % (2429965)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=4094756793:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 19.32/3.62 % (2429959)Instruction limit reached!
% 19.32/3.62 % (2429959)------------------------------
% 19.32/3.62 % (2429959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.32/3.62 % (2429959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.32/3.62 % (2429959)CaDiCaL version: 2.1.3
% 19.32/3.62 % (2429959)Termination reason: Instruction limit
% 19.32/3.62 % (2429959)Termination phase: Saturation
% 19.32/3.62 % (2429959)Time elapsed: 0.182 s
% 19.32/3.62 % (2429959)Peak memory usage: 91 MB
% 19.32/3.62 % (2429959)Instructions burned: 286 (million)
% 19.32/3.62 % (2429965)Instruction limit reached!
% 19.32/3.62 % (2429965)------------------------------
% 19.32/3.62 % (2429965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.32/3.62 % (2429965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.32/3.62 % (2429965)CaDiCaL version: 2.1.3
% 19.32/3.62 % (2429965)Termination reason: Instruction limit
% 19.32/3.62 % (2429965)Termination phase: Saturation
% 19.32/3.62 % (2429965)Time elapsed: 0.074 s
% 19.32/3.62 % (2429965)Peak memory usage: 91 MB
% 19.32/3.62 % (2429965)Instructions burned: 250 (million)
% 19.32/3.62 % (2429961)Instruction limit reached!
% 19.32/3.62 % (2429961)------------------------------
% 19.32/3.62 % (2429961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.32/3.62 % (2429961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.32/3.62 % (2429961)CaDiCaL version: 2.1.3
% 19.32/3.62 % (2429961)Termination reason: Instruction limit
% 19.32/3.62 % (2429961)Termination phase: Saturation
% 19.32/3.62 % (2429961)Time elapsed: 0.197 s
% 19.32/3.62 % (2429961)Peak memory usage: 91 MB
% 19.32/3.62 % (2429961)Instructions burned: 326 (million)
% 19.32/3.62 % (2429966)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2172676386:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 19.32/3.62 % (2429966)Refutation not found, incomplete strategy
% 19.32/3.62 % (2429966)------------------------------
% 19.32/3.62 % (2429966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.32/3.62 % (2429966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.32/3.62 % (2429966)CaDiCaL version: 2.1.3
% 19.32/3.62 % (2429966)Termination reason: Refutation not found, incomplete strategy
% 19.32/3.62 % (2429966)Time elapsed: 0.002 s
% 19.32/3.62 % (2429966)Peak memory usage: 88 MB
% 19.32/3.62 % (2429966)Instructions burned: 1 (million)
% 19.32/3.62 % (2429969)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=356118007:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 19.32/3.62 % (2429969)Instruction limit reached!
% 19.32/3.62 % (2429969)------------------------------
% 19.32/3.62 % (2429969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.32/3.62 % (2429969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.32/3.62 % (2429969)CaDiCaL version: 2.1.3
% 19.32/3.62 % (2429969)Termination reason: Instruction limit
% 19.32/3.62 % (2429969)Termination phase: Saturation
% 19.32/3.62 % (2429969)Time elapsed: 0.033 s
% 19.32/3.62 % (2429969)Peak memory usage: 89 MB
% 19.32/3.62 % (2429969)Instructions burned: 114 (million)
% 19.32/3.62 % (2429968)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=466813183:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 19.32/3.62 % (2429971)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1333304988:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 19.32/3.62 % (2429971)Instruction limit reached!
% 19.32/3.62 % (2429971)------------------------------
% 19.32/3.62 % (2429971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.32/3.62 % (2429971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.32/3.62 % (2429971)CaDiCaL version: 2.1.3
% 15.64/5.14 % (2429971)Termination reason: Instruction limit
% 15.64/5.14 % (2429971)Termination phase: Saturation
% 15.64/5.14 % (2429971)Time elapsed: 0.057 s
% 15.64/5.14 % (2429971)Peak memory usage: 88 MB
% 15.64/5.14 % (2429971)Instructions burned: 128 (million)
% 15.64/5.14 % (2429974)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=688143805:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 15.64/5.14 % (2429974)Instruction limit reached!
% 15.64/5.14 % (2429974)------------------------------
% 15.64/5.14 % (2429974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/5.14 % (2429974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/5.14 % (2429974)CaDiCaL version: 2.1.3
% 15.64/5.14 % (2429974)Termination reason: Instruction limit
% 15.64/5.14 % (2429974)Termination phase: Saturation
% 15.64/5.14 % (2429974)Time elapsed: 0.028 s
% 15.64/5.14 % (2429974)Peak memory usage: 88 MB
% 15.64/5.14 % (2429974)Instructions burned: 115 (million)
% 15.64/5.14 % (2429966)------------------------------
% 15.64/5.14 % (2429966)------------------------------
% 15.64/5.14 % (2429978)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1938207830:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 15.64/5.14 % (2429976)lrs+10_1_sil=8000:sp=occurrence:random_seed=2353623620:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 15.64/5.14 % (2429978)Refutation not found, incomplete strategy
% 15.64/5.14 % (2429978)------------------------------
% 15.64/5.14 % (2429978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/5.14 % (2429978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/5.14 % (2429978)CaDiCaL version: 2.1.3
% 15.64/5.14 % (2429978)Termination reason: Refutation not found, incomplete strategy
% 15.64/5.14 % (2429978)Time elapsed: 0.001 s
% 15.64/5.14 % (2429978)Peak memory usage: 88 MB
% 15.64/5.14 % (2429978)Instructions burned: 1 (million)
% 15.64/5.14 % (2429979)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1264578063:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 15.64/5.14 % (2429978)------------------------------
% 15.64/5.14 % (2429978)------------------------------
% 15.64/5.14 % (2429983)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1392137326:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 15.64/5.14 % (2429983)Instruction limit reached!
% 15.64/5.14 % (2429983)------------------------------
% 15.64/5.14 % (2429983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/5.14 % (2429983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/5.14 % (2429983)CaDiCaL version: 2.1.3
% 15.64/5.14 % (2429983)Termination reason: Instruction limit
% 15.64/5.14 % (2429983)Termination phase: Saturation
% 15.64/5.14 % (2429983)Time elapsed: 0.038 s
% 15.64/5.14 % (2429983)Peak memory usage: 90 MB
% 15.64/5.14 % (2429983)Instructions burned: 137 (million)
% 15.64/5.14 % (2429985)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=540681243:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 15.64/5.14 % (2429985)Refutation not found, incomplete strategy
% 15.64/5.14 % (2429985)------------------------------
% 15.64/5.14 % (2429985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/5.14 % (2429985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/5.14 % (2429985)CaDiCaL version: 2.1.3
% 15.64/5.14 % (2429985)Termination reason: Refutation not found, incomplete strategy
% 15.64/5.14 % (2429985)Time elapsed: 0.001 s
% 15.64/5.14 % (2429985)Peak memory usage: 88 MB
% 15.64/5.14 % (2429985)Instructions burned: 1 (million)
% 15.64/5.14 % (2429985)------------------------------
% 15.64/5.14 % (2429985)------------------------------
% 15.64/5.14 % (2429976)Instruction limit reached!
% 15.64/5.14 % (2429976)------------------------------
% 15.64/5.14 % (2429976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/5.14 % (2429976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/5.14 % (2429976)CaDiCaL version: 2.1.3
% 15.64/5.14 % (2429976)Termination reason: Instruction limit
% 15.64/5.14 % (2429976)Termination phase: Saturation
% 15.64/5.14 % (2429976)Time elapsed: 0.567 s
% 15.64/5.14 % (2429976)Peak memory usage: 96 MB
% 15.64/5.14 % (2429976)Instructions burned: 908 (million)
% 15.64/5.14 % (2429987)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2099900307:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 15.64/5.14 % (2429988)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=2179609687:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 15.64/5.14 % (2429988)Instruction limit reached!
% 15.64/5.14 % (2429988)------------------------------
% 15.64/5.14 % (2429988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/5.14 % (2429988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/5.14 % (2429988)CaDiCaL version: 2.1.3
% 15.64/5.14 % (2429988)Termination reason: Instruction limit
% 15.64/5.14 % (2429988)Termination phase: Saturation
% 15.64/5.14 % (2429988)Time elapsed: 0.079 s
% 15.64/5.14 % (2429988)Peak memory usage: 90 MB
% 15.64/5.14 % (2429988)Instructions burned: 128 (million)
% 15.64/5.14 % (2429991)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1210238774:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 15.64/5.14 % (2429991)Instruction limit reached!
% 15.64/5.14 % (2429991)------------------------------
% 15.64/5.14 % (2429991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/5.14 % (2429991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/5.14 % (2429991)CaDiCaL version: 2.1.3
% 15.64/5.14 % (2429991)Termination reason: Instruction limit
% 15.64/5.14 % (2429991)Termination phase: Saturation
% 15.64/5.14 % (2429991)Time elapsed: 0.056 s
% 15.64/5.14 % (2429991)Peak memory usage: 89 MB
% 15.64/5.14 % (2429991)Instructions burned: 135 (million)
% 15.64/5.14 % (2429993)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=72973218:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/141Mi)
% 15.64/5.14 % (2429993)Refutation not found, incomplete strategy
% 15.64/5.14 % (2429993)------------------------------
% 15.64/5.14 % (2429993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/5.14 % (2429993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/5.14 % (2429993)CaDiCaL version: 2.1.3
% 15.64/5.14 % (2429993)Termination reason: Refutation not found, incomplete strategy
% 15.64/5.14 % (2429993)Time elapsed: 0.001 s
% 15.64/5.14 % (2429993)Peak memory usage: 88 MB
% 15.64/5.14 % (2429993)Instructions burned: 1 (million)
% 15.64/5.14 % (2429993)------------------------------
% 15.64/5.14 % (2429993)------------------------------
% 15.64/5.14 % (2429968)Instruction limit reached!
% 15.64/5.14 % (2429968)------------------------------
% 15.64/5.14 % (2429968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/5.14 % (2429968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/5.14 % (2429968)CaDiCaL version: 2.1.3
% 15.64/5.14 % (2429968)Termination reason: Instruction limit
% 15.64/5.14 % (2429968)Termination phase: Saturation
% 15.64/5.14 % (2429968)Time elapsed: 1.609 s
% 15.64/5.14 % (2429968)Peak memory usage: 141 MB
% 15.64/5.14 % (2429968)Instructions burned: 2350 (million)
% 15.64/5.14 % (2429995)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3139193298:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 15.64/5.14 % (2429996)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=409555806:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi)
% 15.64/5.14 % (2429995)Instruction limit reached!
% 15.64/5.14 % (2429995)------------------------------
% 15.64/5.14 % (2429995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/5.14 % (2429995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/5.14 % (2429995)CaDiCaL version: 2.1.3
% 15.64/5.14 % (2429995)Termination reason: Instruction limit
% 15.64/5.14 % (2429995)Termination phase: Saturation
% 15.64/5.14 % (2429995)Time elapsed: 0.228 s
% 15.64/5.14 % (2429995)Peak memory usage: 91 MB
% 15.64/5.14 % (2429995)Instructions burned: 431 (million)
% 15.64/5.14 % (2429999)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=781428949:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi)
% 15.64/5.14 % (2429999)Instruction limit reached!
% 15.64/5.14 % (2429999)------------------------------
% 15.64/5.14 % (2429999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/5.14 % (2429999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/5.14 % (2429999)CaDiCaL version: 2.1.3
% 15.64/5.14 % (2429999)Termination reason: Instruction limit
% 15.64/5.14 % (2429999)Termination phase: Saturation
% 15.64/5.14 % (2429999)Time elapsed: 0.083 s
% 15.64/5.14 % (2429999)Peak memory usage: 91 MB
% 15.64/5.14 % (2429999)Instructions burned: 151 (million)
% 15.64/5.14 % (2430001)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3523554134:i=14155:bd=all_2972 on theBenchmark for (2972ds/14155Mi)
% 15.64/5.14 % (2429945)First to succeed.
% 15.64/5.14 % (2429945)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2429939"
% 15.64/5.14 % (2429979)Instruction limit reached!
% 15.64/5.14 % (2429979)------------------------------
% 15.64/5.14 % (2429979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.64/5.14 % (2429979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.64/5.14 % (2429979)CaDiCaL version: 2.1.3
% 15.64/5.14 % (2429979)Termination reason: Instruction limit
% 15.64/5.14 % (2429979)Termination phase: Saturation
% 15.64/5.14 % (2429979)Time elapsed: 3.187 s
% 15.64/5.14 % (2429979)Peak memory usage: 164 MB
% 15.64/5.14 % (2429979)Instructions burned: 5202 (million)
% 15.64/5.14 % (2430003)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2518962381:i=667:av=off:fsr=off_2958 on theBenchmark for (2958ds/667Mi)
% 15.64/5.14 % (2429945)Refutation found. Thanks to Tanya!
% 15.64/5.14 % SZS status Theorem for theBenchmark
% 15.64/5.14 % SZS output start Proof for theBenchmark
% See solution above
% 31.06/5.36 % (2429945)------------------------------
% 31.06/5.36 % (2429945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.06/5.36 % (2429945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.06/5.36 % (2429945)CaDiCaL version: 2.1.3
% 31.06/5.36 % (2429945)Termination reason: Refutation
% 31.06/5.36 % (2429945)Time elapsed: 3.900 s
% 31.06/5.36 % (2429945)Peak memory usage: 172 MB
% 31.06/5.36 % (2429945)Instructions burned: 6267 (million)
% 31.06/5.36 % (2429945)------------------------------
% 31.06/5.36 % (2429945)------------------------------
% 31.06/5.36 % (2429939)Success in time 4.303 s
% 31.06/5.36 % Vampire exiting
%------------------------------------------------------------------------------