%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV579+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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:59:31 PM UTC 2026
% Result : Theorem 2.29s 0.94s
% Output : Refutation 2.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 52
% Syntax : Number of formulae : 271 ( 113 unt; 46 def)
% Number of atoms : 489 ( 91 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 390 ( 172 ~; 184 |; 11 &)
% ( 22 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 19 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 29 con; 0-2 aty)
% Number of variables : 85 ( 0 sgn 83 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( subq(X0,X1)
<=> ! [X2] :
( mem(X2,X0)
=> mem(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax',subq_def) ).
fof(f5,axiom,
! [X0,X1] :
( mem(X0,s(X1))
<=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax',s_ax) ).
fof(f6,axiom,
! [X0,X1,X2] :
( mem(X0,u(X1,X2))
<=> ( mem(X0,X1)
| mem(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax',u_ax) ).
fof(f8,axiom,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax',a_def) ).
fof(f9,axiom,
! [X0] : n(X0) = a(X0,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax',n_def) ).
fof(f26,conjecture,
subq(u(a(s(n(n(e))),p(s(n(e)))),a(n(n(s(n(e)))),n(n(n(e))))),u(u(a(s(s(n(n(e)))),n(n(n(e)))),n(a(s(s(n(e))),n(n(e))))),u(a(s(n(e)),p(s(n(e)))),a(s(n(s(n(e)))),p(n(n(e))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subq_2158_39278) ).
fof(f27,negated_conjecture,
~ subq(u(a(s(n(n(e))),p(s(n(e)))),a(n(n(s(n(e)))),n(n(n(e))))),u(u(a(s(s(n(n(e)))),n(n(n(e)))),n(a(s(s(n(e))),n(n(e))))),u(a(s(n(e)),p(s(n(e)))),a(s(n(s(n(e)))),p(n(n(e))))))),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f28,plain,
~ subq(u(a(s(n(n(e))),p(s(n(e)))),a(n(n(s(n(e)))),n(n(n(e))))),u(u(a(s(s(n(n(e)))),n(n(n(e)))),n(a(s(s(n(e))),n(n(e))))),u(a(s(n(e)),p(s(n(e)))),a(s(n(s(n(e)))),p(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(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(f42,plain,
! [X0,X1] :
( subq(X0,X1)
| mem(sK0(X0,X1),X0) ),
inference(cnf_transformation,[],[f34]) ).
fof(f43,plain,
! [X0,X1] :
( ~ mem(sK0(X0,X1),X1)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
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(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(f58,plain,
~ subq(u(a(s(n(n(e))),p(s(n(e)))),a(n(n(s(n(e)))),n(n(n(e))))),u(u(a(s(s(n(n(e)))),n(n(n(e)))),n(a(s(s(n(e))),n(n(e))))),u(a(s(n(e)),p(s(n(e)))),a(s(n(s(n(e)))),p(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(s(u(u(e,s(e)),s(u(e,s(e))))),s(p(s(u(e,s(e)))))),u(u(u(s(u(e,s(e))),s(s(u(e,s(e))))),s(u(s(u(e,s(e))),s(s(u(e,s(e))))))),s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))))),u(u(u(s(s(u(u(e,s(e)),s(u(e,s(e)))))),s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))))),u(u(s(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(u(e,s(e))),s(p(s(u(e,s(e)))))),u(s(u(s(u(e,s(e))),s(s(u(e,s(e)))))),s(p(u(u(e,s(e)),s(u(e,s(e)))))))))),
inference(definition_unfolding,[],[f58,f54,f59,f59,f59,f54,f59,f59,f59,f59,f59,f59,f54,f59,f59,f59,f59,f59,f59,f54,f59,f59,f59,f54,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(sF3),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f73,plain,
p(sF3) = sF6,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF7 = s(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f75,plain,
s(sF6) = sF7,
inference(reorient_equations,[],[f74]) ).
fof(f76,definition,
sF8 = u(sF5,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f77,plain,
u(sF5,sF7) = sF8,
inference(reorient_equations,[],[f76]) ).
fof(f78,definition,
sF9 = s(sF3),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f79,plain,
s(sF3) = sF9,
inference(reorient_equations,[],[f78]) ).
fof(f80,definition,
sF10 = u(sF3,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f81,plain,
u(sF3,sF9) = sF10,
inference(reorient_equations,[],[f80]) ).
fof(f82,definition,
sF11 = s(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f83,plain,
s(sF10) = sF11,
inference(reorient_equations,[],[f82]) ).
fof(f84,definition,
sF12 = u(sF10,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f85,plain,
u(sF10,sF11) = sF12,
inference(reorient_equations,[],[f84]) ).
fof(f86,definition,
sF13 = u(sF4,sF5),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f87,plain,
u(sF4,sF5) = sF13,
inference(reorient_equations,[],[f86]) ).
fof(f88,definition,
sF14 = s(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f89,plain,
s(sF13) = sF14,
inference(reorient_equations,[],[f88]) ).
fof(f90,definition,
sF15 = u(sF12,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f91,plain,
u(sF12,sF14) = sF15,
inference(reorient_equations,[],[f90]) ).
fof(f92,definition,
sF16 = u(sF8,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f93,plain,
u(sF8,sF15) = sF16,
inference(reorient_equations,[],[f92]) ).
fof(f94,definition,
sF17 = s(sF5),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f95,plain,
s(sF5) = sF17,
inference(reorient_equations,[],[f94]) ).
fof(f96,definition,
sF18 = u(sF17,sF14),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f97,plain,
u(sF17,sF14) = sF18,
inference(reorient_equations,[],[f96]) ).
fof(f98,definition,
sF19 = u(sF9,sF5),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f99,plain,
u(sF9,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(sF19,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f103,plain,
u(sF19,sF20) = sF21,
inference(reorient_equations,[],[f102]) ).
fof(f104,definition,
sF22 = u(sF18,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f105,plain,
u(sF18,sF21) = sF22,
inference(reorient_equations,[],[f104]) ).
fof(f106,definition,
sF23 = u(sF3,sF7),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f107,plain,
u(sF3,sF7) = sF23,
inference(reorient_equations,[],[f106]) ).
fof(f108,definition,
sF24 = p(sF4),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f109,plain,
p(sF4) = sF24,
inference(reorient_equations,[],[f108]) ).
fof(f110,definition,
sF25 = s(sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f111,plain,
s(sF24) = sF25,
inference(reorient_equations,[],[f110]) ).
fof(f112,definition,
sF26 = u(sF11,sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f113,plain,
u(sF11,sF25) = sF26,
inference(reorient_equations,[],[f112]) ).
fof(f114,definition,
sF27 = u(sF23,sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f115,plain,
u(sF23,sF26) = sF27,
inference(reorient_equations,[],[f114]) ).
fof(f116,definition,
sF28 = u(sF22,sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f117,plain,
u(sF22,sF27) = sF28,
inference(reorient_equations,[],[f116]) ).
fof(f118,plain,
~ subq(sF16,sF28),
inference(definition_folding,[],[f60,f117,f115,f113,f111,f109,f69,f67,f65,f63,f65,f63,f83,f81,f79,f67,f65,f63,f67,f65,f63,f107,f75,f73,f67,f65,f63,f67,f65,f63,f105,f103,f101,f99,f71,f69,f67,f65,f63,f65,f63,f79,f67,f65,f63,f99,f71,f69,f67,f65,f63,f65,f63,f79,f67,f65,f63,f97,f89,f87,f71,f69,f67,f65,f63,f65,f63,f69,f67,f65,f63,f65,f63,f95,f71,f69,f67,f65,f63,f65,f63,f93,f91,f89,f87,f71,f69,f67,f65,f63,f65,f63,f69,f67,f65,f63,f65,f63,f85,f83,f81,f79,f67,f65,f63,f67,f65,f63,f81,f79,f67,f65,f63,f67,f65,f63,f77,f75,f73,f67,f65,f63,f71,f69,f67,f65,f63,f65,f63]) ).
fof(f121,plain,
mem(sF4,sF5),
inference(superposition,[],[f61,f71]) ).
fof(f122,plain,
mem(sF6,sF7),
inference(superposition,[],[f61,f75]) ).
fof(f123,plain,
mem(sF3,sF9),
inference(superposition,[],[f61,f79]) ).
fof(f124,plain,
mem(sF10,sF11),
inference(superposition,[],[f61,f83]) ).
fof(f125,plain,
mem(sF13,sF14),
inference(superposition,[],[f61,f89]) ).
fof(f132,plain,
! [X0] :
( ~ mem(X0,sF9)
| sF3 = X0 ),
inference(superposition,[],[f46,f79]) ).
fof(f133,plain,
! [X0] :
( ~ mem(X0,sF5)
| sF4 = X0 ),
inference(superposition,[],[f46,f71]) ).
fof(f135,plain,
! [X0] :
( ~ mem(X0,sF7)
| sF6 = X0 ),
inference(superposition,[],[f46,f75]) ).
fof(f136,plain,
! [X0] :
( ~ mem(X0,sF11)
| sF10 = X0 ),
inference(superposition,[],[f46,f83]) ).
fof(f137,plain,
! [X0] :
( ~ mem(X0,sF14)
| sF13 = X0 ),
inference(superposition,[],[f46,f89]) ).
fof(f145,plain,
mem(sK0(sF16,sF28),sF16),
inference(resolution,[],[f42,f118]) ).
fof(f148,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X2)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f49,f43]) ).
fof(f152,plain,
! [X0] :
( ~ mem(X0,sF7)
| mem(X0,sF23) ),
inference(superposition,[],[f49,f107]) ).
fof(f156,plain,
! [X0] :
( ~ mem(X0,sF5)
| mem(X0,sF19) ),
inference(superposition,[],[f49,f99]) ).
fof(f160,plain,
! [X0] :
( ~ mem(X0,sF14)
| mem(X0,sF18) ),
inference(superposition,[],[f49,f97]) ).
fof(f161,plain,
! [X0] :
( ~ mem(X0,sF21)
| mem(X0,sF22) ),
inference(superposition,[],[f49,f105]) ).
fof(f163,plain,
! [X0] :
( ~ mem(X0,sF27)
| mem(X0,sF28) ),
inference(superposition,[],[f49,f117]) ).
fof(f164,plain,
! [X0] :
( ~ mem(X0,sF26)
| mem(X0,sF27) ),
inference(superposition,[],[f49,f115]) ).
fof(f166,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X1)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f50,f43]) ).
fof(f170,plain,
! [X0] :
( ~ mem(X0,sF3)
| mem(X0,sF23) ),
inference(superposition,[],[f50,f107]) ).
fof(f174,plain,
! [X0] :
( ~ mem(X0,sF9)
| mem(X0,sF19) ),
inference(superposition,[],[f50,f99]) ).
fof(f176,plain,
! [X0] :
( ~ mem(X0,sF11)
| mem(X0,sF26) ),
inference(superposition,[],[f50,f113]) ).
fof(f179,plain,
! [X0] :
( ~ mem(X0,sF18)
| mem(X0,sF22) ),
inference(superposition,[],[f50,f105]) ).
fof(f180,plain,
! [X0] :
( ~ mem(X0,sF19)
| mem(X0,sF21) ),
inference(superposition,[],[f50,f103]) ).
fof(f182,plain,
! [X0] :
( ~ mem(X0,sF23)
| mem(X0,sF27) ),
inference(superposition,[],[f50,f115]) ).
fof(f226,definition,
( spl29_3
<=> sF13 = sK0(sF16,sF28) ),
introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).
fof(f227,plain,
( sF13 != sK0(sF16,sF28)
| spl29_3 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f228,plain,
( sF13 = sK0(sF16,sF28)
| ~ spl29_3 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f235,definition,
( spl29_5
<=> sF10 = sK0(sF16,sF28) ),
introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).
fof(f236,plain,
( sF10 != sK0(sF16,sF28)
| spl29_5 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f237,plain,
( sF10 = sK0(sF16,sF28)
| ~ spl29_5 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f244,definition,
( spl29_7
<=> sF3 = sK0(sF16,sF28) ),
introduced(definition,[new_symbols(definition,[spl29_7])],[avatar_definition]) ).
fof(f245,plain,
( sF3 != sK0(sF16,sF28)
| spl29_7 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f246,plain,
( sF3 = sK0(sF16,sF28)
| ~ spl29_7 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f253,definition,
( spl29_9
<=> sF6 = sK0(sF16,sF28) ),
introduced(definition,[new_symbols(definition,[spl29_9])],[avatar_definition]) ).
fof(f254,plain,
( sF6 != sK0(sF16,sF28)
| spl29_9 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f255,plain,
( sF6 = sK0(sF16,sF28)
| ~ spl29_9 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f262,definition,
( spl29_11
<=> sF4 = sK0(sF16,sF28) ),
introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).
fof(f263,plain,
( sF4 != sK0(sF16,sF28)
| spl29_11 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f264,plain,
( sF4 = sK0(sF16,sF28)
| ~ spl29_11 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f295,plain,
! [X0] :
( ~ mem(X0,sF10)
| mem(X0,sF9)
| mem(X0,sF3) ),
inference(superposition,[],[f48,f81]) ).
fof(f298,plain,
! [X0] :
( ~ mem(X0,sF8)
| mem(X0,sF7)
| mem(X0,sF5) ),
inference(superposition,[],[f48,f77]) ).
fof(f299,plain,
! [X0] :
( ~ mem(X0,sF16)
| mem(X0,sF15)
| mem(X0,sF8) ),
inference(superposition,[],[f48,f93]) ).
fof(f301,plain,
! [X0] :
( ~ mem(X0,sF12)
| mem(X0,sF11)
| mem(X0,sF10) ),
inference(superposition,[],[f48,f85]) ).
fof(f303,plain,
! [X0] :
( ~ mem(X0,sF15)
| mem(X0,sF14)
| mem(X0,sF12) ),
inference(superposition,[],[f48,f91]) ).
fof(f452,plain,
mem(sF6,sF23),
inference(resolution,[],[f152,f122]) ).
fof(f462,plain,
mem(sF4,sF19),
inference(resolution,[],[f156,f121]) ).
fof(f475,plain,
mem(sF13,sF18),
inference(resolution,[],[f160,f125]) ).
fof(f510,definition,
( spl29_38
<=> mem(sK0(sF16,sF28),sF28) ),
introduced(definition,[new_symbols(definition,[spl29_38])],[avatar_definition]) ).
fof(f511,plain,
( ~ mem(sK0(sF16,sF28),sF28)
| spl29_38 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f512,plain,
( mem(sK0(sF16,sF28),sF28)
| ~ spl29_38 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f520,definition,
( spl29_40
<=> mem(sK0(sF16,sF28),sF27) ),
introduced(definition,[new_symbols(definition,[spl29_40])],[avatar_definition]) ).
fof(f521,plain,
( ~ mem(sK0(sF16,sF28),sF27)
| spl29_40 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f522,plain,
( mem(sK0(sF16,sF28),sF27)
| ~ spl29_40 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f551,plain,
mem(sF3,sF19),
inference(resolution,[],[f174,f123]) ).
fof(f559,definition,
( spl29_45
<=> mem(sK0(sF16,sF28),sF12) ),
introduced(definition,[new_symbols(definition,[spl29_45])],[avatar_definition]) ).
fof(f560,plain,
( ~ mem(sK0(sF16,sF28),sF12)
| spl29_45 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f561,plain,
( mem(sK0(sF16,sF28),sF12)
| ~ spl29_45 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f565,plain,
mem(sF10,sF26),
inference(resolution,[],[f176,f124]) ).
fof(f573,definition,
( spl29_47
<=> mem(sK0(sF16,sF28),sF15) ),
introduced(definition,[new_symbols(definition,[spl29_47])],[avatar_definition]) ).
fof(f575,plain,
( mem(sK0(sF16,sF28),sF15)
| ~ spl29_47 ),
inference(avatar_component_clause,[],[f573]) ).
fof(f614,plain,
( subq(sF16,sF28)
| ~ spl29_38 ),
inference(resolution,[],[f512,f43]) ).
fof(f616,plain,
( $false
| ~ spl29_38 ),
inference(forward_subsumption_resolution,[],[f614,f118]) ).
fof(f617,plain,
~ spl29_38,
inference(avatar_contradiction_clause,[],[f616]) ).
fof(f688,plain,
( mem(sK0(sF16,sF28),sF28)
| ~ spl29_40 ),
inference(resolution,[],[f522,f163]) ).
fof(f690,plain,
( $false
| spl29_38
| ~ spl29_40 ),
inference(forward_subsumption_resolution,[],[f688,f511]) ).
fof(f691,plain,
( spl29_38
| ~ spl29_40 ),
inference(avatar_contradiction_clause,[],[f690]) ).
fof(f701,definition,
( spl29_53
<=> mem(sK0(sF16,sF28),sF5) ),
introduced(definition,[new_symbols(definition,[spl29_53])],[avatar_definition]) ).
fof(f702,plain,
( ~ mem(sK0(sF16,sF28),sF5)
| spl29_53 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f703,plain,
( mem(sK0(sF16,sF28),sF5)
| ~ spl29_53 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f713,definition,
( spl29_55
<=> mem(sK0(sF16,sF28),sF7) ),
introduced(definition,[new_symbols(definition,[spl29_55])],[avatar_definition]) ).
fof(f714,plain,
( ~ mem(sK0(sF16,sF28),sF7)
| spl29_55 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f715,plain,
( mem(sK0(sF16,sF28),sF7)
| ~ spl29_55 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f739,plain,
( mem(sK0(sF16,sF28),sF15)
| mem(sK0(sF16,sF28),sF8) ),
inference(resolution,[],[f299,f145]) ).
fof(f747,definition,
( spl29_57
<=> mem(sK0(sF16,sF28),sF8) ),
introduced(definition,[new_symbols(definition,[spl29_57])],[avatar_definition]) ).
fof(f749,plain,
( mem(sK0(sF16,sF28),sF8)
| ~ spl29_57 ),
inference(avatar_component_clause,[],[f747]) ).
fof(f751,plain,
( spl29_57
| spl29_47 ),
inference(avatar_split_clause,[],[f739,f573,f747]) ).
fof(f1319,definition,
( spl29_111
<=> mem(sK0(sF16,sF28),sF14) ),
introduced(definition,[new_symbols(definition,[spl29_111])],[avatar_definition]) ).
fof(f1321,plain,
( mem(sK0(sF16,sF28),sF14)
| ~ spl29_111 ),
inference(avatar_component_clause,[],[f1319]) ).
fof(f1419,plain,
! [X0] :
( ~ mem(sK0(X0,sF28),sF27)
| subq(X0,sF28) ),
inference(superposition,[],[f148,f117]) ).
fof(f1445,plain,
! [X0] :
( ~ mem(sK0(X0,sF28),sF22)
| subq(X0,sF28) ),
inference(superposition,[],[f166,f117]) ).
fof(f1518,plain,
mem(sF6,sF27),
inference(resolution,[],[f452,f182]) ).
fof(f1547,plain,
mem(sF4,sF21),
inference(resolution,[],[f462,f180]) ).
fof(f1573,plain,
mem(sF13,sF22),
inference(resolution,[],[f475,f179]) ).
fof(f1603,plain,
mem(sF3,sF21),
inference(resolution,[],[f551,f180]) ).
fof(f1608,plain,
mem(sF10,sF27),
inference(resolution,[],[f565,f164]) ).
fof(f1851,definition,
( spl29_130
<=> mem(sK0(sF16,sF28),sF3) ),
introduced(definition,[new_symbols(definition,[spl29_130])],[avatar_definition]) ).
fof(f1852,plain,
( ~ mem(sK0(sF16,sF28),sF3)
| spl29_130 ),
inference(avatar_component_clause,[],[f1851]) ).
fof(f1853,plain,
( mem(sK0(sF16,sF28),sF3)
| ~ spl29_130 ),
inference(avatar_component_clause,[],[f1851]) ).
fof(f1867,plain,
( mem(sK0(sF16,sF28),sF11)
| mem(sK0(sF16,sF28),sF10)
| ~ spl29_45 ),
inference(resolution,[],[f561,f301]) ).
fof(f1871,definition,
( spl29_131
<=> mem(sK0(sF16,sF28),sF10) ),
introduced(definition,[new_symbols(definition,[spl29_131])],[avatar_definition]) ).
fof(f1873,plain,
( mem(sK0(sF16,sF28),sF10)
| ~ spl29_131 ),
inference(avatar_component_clause,[],[f1871]) ).
fof(f1875,definition,
( spl29_132
<=> mem(sK0(sF16,sF28),sF11) ),
introduced(definition,[new_symbols(definition,[spl29_132])],[avatar_definition]) ).
fof(f1877,plain,
( mem(sK0(sF16,sF28),sF11)
| ~ spl29_132 ),
inference(avatar_component_clause,[],[f1875]) ).
fof(f1878,plain,
( spl29_131
| spl29_132
| ~ spl29_45 ),
inference(avatar_split_clause,[],[f1867,f559,f1875,f1871]) ).
fof(f2193,plain,
( sF4 = sK0(sF16,sF28)
| ~ spl29_53 ),
inference(resolution,[],[f703,f133]) ).
fof(f2195,plain,
( $false
| spl29_11
| ~ spl29_53 ),
inference(forward_subsumption_resolution,[],[f2193,f263]) ).
fof(f2196,plain,
( spl29_11
| ~ spl29_53 ),
inference(avatar_contradiction_clause,[],[f2195]) ).
fof(f2354,plain,
( sF6 = sK0(sF16,sF28)
| ~ spl29_55 ),
inference(resolution,[],[f715,f135]) ).
fof(f2356,plain,
( $false
| spl29_9
| ~ spl29_55 ),
inference(forward_subsumption_resolution,[],[f2354,f254]) ).
fof(f2357,plain,
( spl29_9
| ~ spl29_55 ),
inference(avatar_contradiction_clause,[],[f2356]) ).
fof(f2507,plain,
( ~ mem(sF6,sF27)
| subq(sF16,sF28)
| ~ spl29_9 ),
inference(superposition,[],[f1419,f255]) ).
fof(f2511,plain,
( subq(sF16,sF28)
| ~ spl29_9 ),
inference(forward_subsumption_resolution,[],[f2507,f1518]) ).
fof(f2517,plain,
( $false
| ~ spl29_9 ),
inference(forward_subsumption_resolution,[],[f2511,f118]) ).
fof(f2518,plain,
~ spl29_9,
inference(avatar_contradiction_clause,[],[f2517]) ).
fof(f2566,plain,
( mem(sK0(sF16,sF28),sF7)
| mem(sK0(sF16,sF28),sF5)
| ~ spl29_57 ),
inference(resolution,[],[f749,f298]) ).
fof(f2569,plain,
( mem(sK0(sF16,sF28),sF5)
| spl29_55
| ~ spl29_57 ),
inference(forward_subsumption_resolution,[],[f2566,f714]) ).
fof(f2570,plain,
( $false
| spl29_53
| spl29_55
| ~ spl29_57 ),
inference(forward_subsumption_resolution,[],[f2569,f702]) ).
fof(f2571,plain,
( spl29_53
| spl29_55
| ~ spl29_57 ),
inference(avatar_contradiction_clause,[],[f2570]) ).
fof(f4452,plain,
( ~ mem(sF13,sF22)
| subq(sF16,sF28)
| ~ spl29_3 ),
inference(superposition,[],[f1445,f228]) ).
fof(f4458,plain,
( subq(sF16,sF28)
| ~ spl29_3 ),
inference(forward_subsumption_resolution,[],[f4452,f1573]) ).
fof(f4474,plain,
( $false
| ~ spl29_3 ),
inference(forward_subsumption_resolution,[],[f4458,f118]) ).
fof(f4475,plain,
~ spl29_3,
inference(avatar_contradiction_clause,[],[f4474]) ).
fof(f6554,plain,
mem(sF4,sF22),
inference(resolution,[],[f1547,f161]) ).
fof(f6641,plain,
mem(sF3,sF22),
inference(resolution,[],[f1603,f161]) ).
fof(f8471,plain,
( ~ mem(sF3,sF22)
| subq(sF16,sF28)
| ~ spl29_7 ),
inference(superposition,[],[f1445,f246]) ).
fof(f8478,plain,
( subq(sF16,sF28)
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f8471,f6641]) ).
fof(f8494,plain,
( $false
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f8478,f118]) ).
fof(f8495,plain,
~ spl29_7,
inference(avatar_contradiction_clause,[],[f8494]) ).
fof(f14560,definition,
( spl29_503
<=> mem(sK0(sF16,sF28),sF23) ),
introduced(definition,[new_symbols(definition,[spl29_503])],[avatar_definition]) ).
fof(f14562,plain,
( mem(sK0(sF16,sF28),sF23)
| ~ spl29_503 ),
inference(avatar_component_clause,[],[f14560]) ).
fof(f14916,definition,
( spl29_524
<=> mem(sK0(sF16,sF28),sF9) ),
introduced(definition,[new_symbols(definition,[spl29_524])],[avatar_definition]) ).
fof(f14918,plain,
( mem(sK0(sF16,sF28),sF9)
| ~ spl29_524 ),
inference(avatar_component_clause,[],[f14916]) ).
fof(f15786,plain,
( mem(sK0(sF16,sF28),sF14)
| mem(sK0(sF16,sF28),sF12)
| ~ spl29_47 ),
inference(resolution,[],[f575,f303]) ).
fof(f15792,plain,
( mem(sK0(sF16,sF28),sF14)
| spl29_45
| ~ spl29_47 ),
inference(forward_subsumption_resolution,[],[f15786,f560]) ).
fof(f16056,plain,
( mem(sK0(sF16,sF28),sF9)
| mem(sK0(sF16,sF28),sF3)
| ~ spl29_131 ),
inference(resolution,[],[f1873,f295]) ).
fof(f16065,plain,
( mem(sK0(sF16,sF28),sF9)
| spl29_130
| ~ spl29_131 ),
inference(forward_subsumption_resolution,[],[f16056,f1852]) ).
fof(f16067,plain,
( spl29_524
| spl29_130
| ~ spl29_131 ),
inference(avatar_split_clause,[],[f16065,f1871,f1851,f14916]) ).
fof(f16124,plain,
( sF3 = sK0(sF16,sF28)
| ~ spl29_524 ),
inference(resolution,[],[f14918,f132]) ).
fof(f16129,plain,
( $false
| spl29_7
| ~ spl29_524 ),
inference(forward_subsumption_resolution,[],[f16124,f245]) ).
fof(f16130,plain,
( spl29_7
| ~ spl29_524 ),
inference(avatar_contradiction_clause,[],[f16129]) ).
fof(f16171,plain,
( mem(sK0(sF16,sF28),sF23)
| ~ spl29_130 ),
inference(resolution,[],[f1853,f170]) ).
fof(f16181,plain,
( spl29_503
| ~ spl29_130 ),
inference(avatar_split_clause,[],[f16171,f1851,f14560]) ).
fof(f16231,plain,
( sF10 = sK0(sF16,sF28)
| ~ spl29_132 ),
inference(resolution,[],[f1877,f136]) ).
fof(f16236,plain,
( $false
| spl29_5
| ~ spl29_132 ),
inference(forward_subsumption_resolution,[],[f16231,f236]) ).
fof(f16237,plain,
( spl29_5
| ~ spl29_132 ),
inference(avatar_contradiction_clause,[],[f16236]) ).
fof(f16280,plain,
( ~ mem(sF10,sF27)
| subq(sF16,sF28)
| ~ spl29_5 ),
inference(superposition,[],[f1419,f237]) ).
fof(f16284,plain,
( subq(sF16,sF28)
| ~ spl29_5 ),
inference(forward_subsumption_resolution,[],[f16280,f1608]) ).
fof(f16297,plain,
( $false
| ~ spl29_5 ),
inference(forward_subsumption_resolution,[],[f16284,f118]) ).
fof(f16298,plain,
~ spl29_5,
inference(avatar_contradiction_clause,[],[f16297]) ).
fof(f16820,plain,
( spl29_111
| spl29_45
| ~ spl29_47 ),
inference(avatar_split_clause,[],[f15792,f573,f559,f1319]) ).
fof(f16898,plain,
( sF13 = sK0(sF16,sF28)
| ~ spl29_111 ),
inference(resolution,[],[f1321,f137]) ).
fof(f16903,plain,
( $false
| spl29_3
| ~ spl29_111 ),
inference(forward_subsumption_resolution,[],[f16898,f227]) ).
fof(f16904,plain,
( spl29_3
| ~ spl29_111 ),
inference(avatar_contradiction_clause,[],[f16903]) ).
fof(f17710,plain,
( ~ mem(sF4,sF22)
| subq(sF16,sF28)
| ~ spl29_11 ),
inference(superposition,[],[f1445,f264]) ).
fof(f17715,plain,
( subq(sF16,sF28)
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f17710,f6554]) ).
fof(f17724,plain,
( $false
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f17715,f118]) ).
fof(f17725,plain,
~ spl29_11,
inference(avatar_contradiction_clause,[],[f17724]) ).
fof(f18530,plain,
( mem(sK0(sF16,sF28),sF27)
| ~ spl29_503 ),
inference(resolution,[],[f14562,f182]) ).
fof(f18538,plain,
( $false
| spl29_40
| ~ spl29_503 ),
inference(forward_subsumption_resolution,[],[f18530,f521]) ).
fof(f18539,plain,
( spl29_40
| ~ spl29_503 ),
inference(avatar_contradiction_clause,[],[f18538]) ).
cnf(s35,plain,
~ spl29_38,
inference(sat_conversion,[],[f617]) ).
cnf(s36,plain,
( spl29_38
| ~ spl29_40 ),
inference(sat_conversion,[],[f691]) ).
cnf(s40,plain,
( spl29_47
| spl29_57 ),
inference(sat_conversion,[],[f751]) ).
cnf(s108,plain,
( ~ spl29_45
| spl29_131
| spl29_132 ),
inference(sat_conversion,[],[f1878]) ).
cnf(s127,plain,
( spl29_11
| ~ spl29_53 ),
inference(sat_conversion,[],[f2196]) ).
cnf(s139,plain,
( spl29_9
| ~ spl29_55 ),
inference(sat_conversion,[],[f2357]) ).
cnf(s150,plain,
~ spl29_9,
inference(sat_conversion,[],[f2518]) ).
cnf(s153,plain,
( spl29_53
| spl29_55
| ~ spl29_57 ),
inference(sat_conversion,[],[f2571]) ).
cnf(s208,plain,
~ spl29_3,
inference(sat_conversion,[],[f4475]) ).
cnf(s327,plain,
~ spl29_7,
inference(sat_conversion,[],[f8495]) ).
cnf(s743,plain,
( spl29_130
| ~ spl29_131
| spl29_524 ),
inference(sat_conversion,[],[f16067]) ).
cnf(s744,plain,
( spl29_7
| ~ spl29_524 ),
inference(sat_conversion,[],[f16130]) ).
cnf(s746,plain,
( ~ spl29_130
| spl29_503 ),
inference(sat_conversion,[],[f16181]) ).
cnf(s750,plain,
( spl29_5
| ~ spl29_132 ),
inference(sat_conversion,[],[f16237]) ).
cnf(s755,plain,
~ spl29_5,
inference(sat_conversion,[],[f16298]) ).
cnf(s794,plain,
( spl29_45
| ~ spl29_47
| spl29_111 ),
inference(sat_conversion,[],[f16820]) ).
cnf(s803,plain,
( spl29_3
| ~ spl29_111 ),
inference(sat_conversion,[],[f16904]) ).
cnf(s879,plain,
~ spl29_11,
inference(sat_conversion,[],[f17725]) ).
cnf(s925,plain,
( spl29_40
| ~ spl29_503 ),
inference(sat_conversion,[],[f18539]) ).
cnf(s926,plain,
~ spl29_132,
inference(rat,[],[s750,s755]) ).
cnf(s936,plain,
~ spl29_524,
inference(rat,[],[s744,s327]) ).
cnf(s945,plain,
~ spl29_111,
inference(rat,[],[s803,s208]) ).
cnf(s949,plain,
~ spl29_55,
inference(rat,[],[s139,s150]) ).
cnf(s951,plain,
~ spl29_53,
inference(rat,[],[s127,s879]) ).
cnf(s952,plain,
~ spl29_57,
inference(rat,[],[s153,s949,s951]) ).
cnf(s956,plain,
( ~ spl29_45
| spl29_131 ),
inference(rat,[],[s108,s926]) ).
cnf(s962,plain,
spl29_47,
inference(rat,[],[s40,s952]) ).
cnf(s963,plain,
spl29_45,
inference(rat,[],[s794,s945,s962]) ).
cnf(s965,plain,
spl29_131,
inference(rat,[],[s956,s963]) ).
cnf(s966,plain,
spl29_130,
inference(rat,[],[s743,s936,s965]) ).
cnf(s971,plain,
spl29_503,
inference(rat,[],[s746,s966]) ).
cnf(s974,plain,
spl29_40,
inference(rat,[],[s925,s971]) ).
cnf(s978,plain,
spl29_38,
inference(rat,[],[s36,s974]) ).
cnf(s979,plain,
$false,
inference(rat,[],[s35,s978]) ).
fof(f18542,plain,
$false,
inference(avatar_sat_refutation,[],[s979]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV579+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n015.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 06:42:31 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.29/0.94 % (2429054)Will run a generic schedule for satisfiability detection.
% 2.29/0.94 % (2429063)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=490628679:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.29/0.94 % (2429060)% WARNING: option uhcvi not known.
% 2.29/0.94 % (2429062)dis+10_1_sil=32000:sp=arity:random_seed=2897406779:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.29/0.94 % (2429059)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1371546139_2999 on theBenchmark for (2999ds/0Mi)
% 2.29/0.94 % (2429060)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3157220309:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.29/0.94 % (2429061)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=879913352:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.29/0.94 % (2429064)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1008905900:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.29/0.94 % (2429065)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1289406186:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.29/0.94 % TRYING [1]
% 2.29/0.94 % TRYING [2]
% 2.29/0.94 % TRYING [3]
% 2.29/0.94 % TRYING [4]
% 2.29/0.94 % TRYING [5]
% 2.29/0.94 % TRYING [6]
% 2.29/0.94 % (2429063)Instruction limit reached!
% 2.29/0.94 % (2429063)------------------------------
% 2.29/0.94 % (2429063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.94 % (2429063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.94 % (2429063)CaDiCaL version: 2.1.3
% 2.29/0.94 % (2429063)Termination reason: Instruction limit
% 2.29/0.94 % (2429063)Termination phase: Saturation
% 2.29/0.94 % (2429063)Time elapsed: 0.038 s
% 2.29/0.94 % (2429063)Peak memory usage: 12 MB
% 2.29/0.94 % (2429063)Instructions burned: 118 (million)
% 2.29/0.94 % TRYING [7]
% 2.29/0.94 % (2429073)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2667275470:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.29/0.94 % TRYING [1]
% 2.29/0.94 % TRYING [2]
% 2.29/0.94 % TRYING [3]
% 2.29/0.94 % TRYING [4]
% 2.29/0.94 % TRYING [5]
% 2.29/0.94 % TRYING [6]
% 2.29/0.94 % TRYING [8]
% 2.29/0.94 % (2429062)Instruction limit reached!
% 2.29/0.94 % (2429062)------------------------------
% 2.29/0.94 % (2429062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.94 % (2429062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.94 % (2429062)CaDiCaL version: 2.1.3
% 2.29/0.94 % (2429062)Termination reason: Instruction limit
% 2.29/0.94 % (2429062)Termination phase: Saturation
% 2.29/0.94 % (2429062)Time elapsed: 0.064 s
% 2.29/0.94 % (2429062)Peak memory usage: 12 MB
% 2.29/0.94 % (2429062)Instructions burned: 104 (million)
% 2.29/0.94 % TRYING [7]
% 2.29/0.94 % (2429064)Instruction limit reached!
% 2.29/0.94 % (2429064)------------------------------
% 2.29/0.94 % (2429064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.94 % (2429064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.94 % (2429064)CaDiCaL version: 2.1.3
% 2.29/0.94 % (2429064)Termination reason: Instruction limit
% 2.29/0.94 % (2429064)Termination phase: Saturation
% 2.29/0.94 % (2429064)Time elapsed: 0.079 s
% 2.29/0.94 % (2429064)Peak memory usage: 13 MB
% 2.29/0.94 % (2429064)Instructions burned: 131 (million)
% 2.29/0.94 % (2429075)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3731308944:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.29/0.94 % (2429065)Instruction limit reached!
% 2.29/0.94 % (2429065)------------------------------
% 2.29/0.94 % (2429065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.94 % (2429065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.94 % (2429065)CaDiCaL version: 2.1.3
% 2.29/0.94 % (2429065)Termination reason: Instruction limit
% 2.29/0.94 % (2429065)Termination phase: Saturation
% 2.29/0.94 % (2429065)Time elapsed: 0.094 s
% 2.29/0.94 % (2429065)Peak memory usage: 12 MB
% 2.29/0.94 % (2429065)Instructions burned: 159 (million)
% 2.29/0.94 % (2429076)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3530830278:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 2.29/0.94 % TRYING [8]
% 2.29/0.94 % (2429078)ott-21_1_sil=16000:fs=off:random_seed=2319770186:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.29/0.94 % TRYING [9]
% 2.29/0.94 % (2429075)Instruction limit reached!
% 2.29/0.94 % (2429075)------------------------------
% 2.29/0.94 % (2429075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.94 % (2429075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.94 % (2429075)CaDiCaL version: 2.1.3
% 2.29/0.94 % (2429075)Termination reason: Instruction limit
% 2.29/0.94 % (2429075)Termination phase: Saturation
% 2.29/0.94 % (2429075)Time elapsed: 0.085 s
% 2.29/0.94 % (2429075)Peak memory usage: 13 MB
% 2.29/0.94 % (2429075)Instructions burned: 132 (million)
% 2.29/0.94 % (2429081)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=401679521:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 2.29/0.94 % (2429078)Instruction limit reached!
% 2.29/0.94 % (2429078)------------------------------
% 2.29/0.94 % (2429078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.94 % (2429078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.94 % (2429078)CaDiCaL version: 2.1.3
% 2.29/0.94 % (2429078)Termination reason: Instruction limit
% 2.29/0.94 % (2429078)Termination phase: Saturation
% 2.29/0.94 % (2429078)Time elapsed: 0.093 s
% 2.29/0.94 % (2429078)Peak memory usage: 13 MB
% 2.29/0.94 % (2429078)Instructions burned: 181 (million)
% 2.29/0.94 % (2429083)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3240637435:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 2.29/0.94 % TRYING [1]
% 2.29/0.94 % TRYING [2]
% 2.29/0.94 % TRYING [3]
% 2.29/0.94 % (2429073)Instruction limit reached!
% 2.29/0.94 % (2429073)------------------------------
% 2.29/0.94 % (2429073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.94 % (2429073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.94 % (2429073)CaDiCaL version: 2.1.3
% 2.29/0.94 % (2429073)Termination reason: Instruction limit
% 2.29/0.94 % (2429073)Termination phase: Finite model building SAT solving
% 2.29/0.94 % (2429073)Time elapsed: 0.195 s
% 2.29/0.94 % (2429073)Peak memory usage: 20 MB
% 2.29/0.94 % (2429073)Instructions burned: 715 (million)
% 2.29/0.94 % TRYING [4]
% 2.29/0.94 % (2429085)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2068355166:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 2.29/0.94 % TRYING [5]
% 2.29/0.94 % TRYING [6]
% 2.29/0.94 % TRYING [7]
% 2.29/0.94 % (2429085) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2429054-2429085"...
% 2.29/0.94 % (2429085)...printing done.
% 2.29/0.94 % (2429085)Refutation found. Thanks to Tanya!
% 2.29/0.94 % SZS status Theorem for theBenchmark
% 2.29/0.94 % SZS output start Proof for theBenchmark
% See solution above
% 2.29/0.95 % (2429085)------------------------------
% 2.29/0.95 % (2429085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.29/0.95 % (2429085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/0.95 % (2429085)CaDiCaL version: 2.1.3
% 2.29/0.95 % (2429085)Termination reason: Refutation
% 2.29/0.95 % (2429085)Time elapsed: 0.226 s
% 2.29/0.95 % (2429085)Peak memory usage: 20 MB
% 2.29/0.95 % (2429085)Instructions burned: 709 (million)
% 2.29/0.95 % (2429054)Success in time 0.518 s
% 2.29/0.95 % Vampire exiting
%------------------------------------------------------------------------------