%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRO018+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:30:41 PM UTC 2026
% Result : Theorem 1.83s 0.69s
% Output : Refutation 1.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 24
% Syntax : Number of formulae : 175 ( 34 unt; 11 def)
% Number of atoms : 597 ( 41 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 689 ( 267 ~; 282 |; 112 &)
% ( 14 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 11 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-3 aty)
% Number of variables : 196 ( 0 sgn 158 !; 38 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ~ ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_04) ).
fof(f14,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_13) ).
fof(f19,axiom,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_18) ).
fof(f22,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& leaf_occ(X1,X0) )
=> ~ ? [X3] : min_precedes(X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_21) ).
fof(f23,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_22) ).
fof(f25,axiom,
! [X0,X1,X2] :
( min_precedes(X1,X2,X0)
=> ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_24) ).
fof(f30,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_29) ).
fof(f33,axiom,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> ? [X2,X3,X4] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X3,tptp4)
& min_precedes(X2,X3,tptp0)
& ( occurrence_of(X4,tptp1)
| occurrence_of(X4,tptp2) )
& min_precedes(X3,X4,tptp0)
& ! [X5] :
( min_precedes(X2,X5,tptp0)
=> ( X5 = X3
| X5 = X4 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_32) ).
fof(f39,axiom,
atomic(tptp3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_38) ).
fof(f40,axiom,
tptp4 != tptp3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_39) ).
fof(f43,axiom,
tptp3 != tptp1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_42) ).
fof(f44,axiom,
tptp3 != tptp2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_43) ).
fof(f46,conjecture,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> ? [X2,X3] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& ( occurrence_of(X3,tptp1)
| occurrence_of(X3,tptp2) )
& min_precedes(X2,X3,tptp0)
& leaf_occ(X3,X1)
& ( occurrence_of(X3,tptp1)
=> ~ ? [X4] :
( occurrence_of(X4,tptp2)
& min_precedes(X2,X4,tptp0) ) )
& ( occurrence_of(X3,tptp2)
=> ~ ? [X5] :
( occurrence_of(X5,tptp1)
& min_precedes(X2,X5,tptp0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f47,negated_conjecture,
~ ! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> ? [X2,X3] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& ( occurrence_of(X3,tptp1)
| occurrence_of(X3,tptp2) )
& min_precedes(X2,X3,tptp0)
& leaf_occ(X3,X1)
& ( occurrence_of(X3,tptp1)
=> ~ ? [X4] :
( occurrence_of(X4,tptp2)
& min_precedes(X2,X4,tptp0) ) )
& ( occurrence_of(X3,tptp2)
=> ~ ? [X5] :
( occurrence_of(X5,tptp1)
& min_precedes(X2,X5,tptp0) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f58,plain,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f66,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f14]) ).
fof(f71,plain,
! [X0] :
( ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) )
| ~ activity_occurrence(X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f75,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(flattening,[],[f75]) ).
fof(f77,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f78,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f77]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) )
| ~ min_precedes(X1,X2,X0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f88,plain,
! [X0,X1] :
( ( activity(X0)
& activity_occurrence(X1) )
| ~ occurrence_of(X1,X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f92,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X3,tptp4)
& min_precedes(X2,X3,tptp0)
& ( occurrence_of(X4,tptp1)
| occurrence_of(X4,tptp2) )
& min_precedes(X3,X4,tptp0)
& ! [X5] :
( X5 = X3
| X5 = X4
| ~ min_precedes(X2,X5,tptp0) ) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f33]) ).
fof(f93,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X3,tptp4)
& min_precedes(X2,X3,tptp0)
& ( occurrence_of(X4,tptp1)
| occurrence_of(X4,tptp2) )
& min_precedes(X3,X4,tptp0)
& ! [X5] :
( X5 = X3
| X5 = X4
| ~ min_precedes(X2,X5,tptp0) ) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(flattening,[],[f92]) ).
fof(f94,plain,
? [X0,X1] :
( ! [X2,X3] :
( ~ occurrence_of(X2,tptp3)
| ~ next_subocc(X0,X2,tptp0)
| ( ~ occurrence_of(X3,tptp1)
& ~ occurrence_of(X3,tptp2) )
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf_occ(X3,X1)
| ( ? [X4] :
( occurrence_of(X4,tptp2)
& min_precedes(X2,X4,tptp0) )
& occurrence_of(X3,tptp1) )
| ( ? [X5] :
( occurrence_of(X5,tptp1)
& min_precedes(X2,X5,tptp0) )
& occurrence_of(X3,tptp2) ) )
& occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f47]) ).
fof(f95,plain,
? [X0,X1] :
( ! [X2,X3] :
( ~ occurrence_of(X2,tptp3)
| ~ next_subocc(X0,X2,tptp0)
| ( ~ occurrence_of(X3,tptp1)
& ~ occurrence_of(X3,tptp2) )
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf_occ(X3,X1)
| ( ? [X4] :
( occurrence_of(X4,tptp2)
& min_precedes(X2,X4,tptp0) )
& occurrence_of(X3,tptp1) )
| ( ? [X5] :
( occurrence_of(X5,tptp1)
& min_precedes(X2,X5,tptp0) )
& occurrence_of(X3,tptp2) ) )
& occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) ),
inference(flattening,[],[f94]) ).
fof(f96,definition,
! [X2,X3] :
( ( ? [X5] :
( occurrence_of(X5,tptp1)
& min_precedes(X2,X5,tptp0) )
& occurrence_of(X3,tptp2) )
| ~ sP0(X2,X3) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f97,plain,
? [X0,X1] :
( ! [X2,X3] :
( ~ occurrence_of(X2,tptp3)
| ~ next_subocc(X0,X2,tptp0)
| ( ~ occurrence_of(X3,tptp1)
& ~ occurrence_of(X3,tptp2) )
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf_occ(X3,X1)
| ( ? [X4] :
( occurrence_of(X4,tptp2)
& min_precedes(X2,X4,tptp0) )
& occurrence_of(X3,tptp1) )
| sP0(X2,X3) )
& occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) ),
inference(definition_folding,[],[f95,f96]) ).
fof(f98,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) )
& ( ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f58]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) )
& ( ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(flattening,[],[f98]) ).
fof(f100,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) )
& ( ( min_precedes(X0,X1,X2)
& ! [X4] :
( ~ min_precedes(X0,X4,X2)
| ~ min_precedes(X4,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(rectify,[],[f99]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ( min_precedes(X0,sK1(X0,X1,X2),X2)
& min_precedes(sK1(X0,X1,X2),X1,X2) ) )
& ( ( min_precedes(X0,X1,X2)
& ! [X4] :
( ~ min_precedes(X0,X4,X2)
| ~ min_precedes(X4,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1,X2))],[f100]) ).
fof(f105,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f66]) ).
fof(f113,plain,
! [X0] :
( ( activity(sK6(X0))
& occurrence_of(X0,sK6(X0)) )
| ~ activity_occurrence(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X1,sK6(X0))],[f71]) ).
fof(f115,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK8(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK8(X0,X1,X2))
& subactivity_occurrence(X2,sK8(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X3,sK8(X0,X1,X2))],[f81]) ).
fof(f120,plain,
! [X0,X1] :
( ( occurrence_of(sK14(X0),tptp3)
& next_subocc(X0,sK14(X0),tptp0)
& occurrence_of(sK15(X0),tptp4)
& min_precedes(sK14(X0),sK15(X0),tptp0)
& ( occurrence_of(sK16(X0),tptp1)
| occurrence_of(sK16(X0),tptp2) )
& min_precedes(sK15(X0),sK16(X0),tptp0)
& ! [X5] :
( sK15(X0) = X5
| sK16(X0) = X5
| ~ min_precedes(sK14(X0),X5,tptp0) ) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15,sK16]),skolemize(X2,sK14(X0)),skolemize(X3,sK15(X0)),skolemize(X4,sK16(X0))],[f93]) ).
fof(f124,plain,
( ! [X2,X3] :
( ~ occurrence_of(X2,tptp3)
| ~ next_subocc(sK18,X2,tptp0)
| ( ~ occurrence_of(X3,tptp1)
& ~ occurrence_of(X3,tptp2) )
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf_occ(X3,sK19)
| ( occurrence_of(sK20(X2),tptp2)
& min_precedes(X2,sK20(X2),tptp0)
& occurrence_of(X3,tptp1) )
| sP0(X2,X3) )
& occurrence_of(sK19,tptp0)
& subactivity_occurrence(sK18,sK19)
& arboreal(sK18)
& ~ leaf_occ(sK18,sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19,sK20]),skolemize(X0,sK18),skolemize(X1,sK19),skolemize(X4,sK20(X2))],[f97]) ).
fof(f130,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f101]) ).
fof(f147,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f158,plain,
! [X0] :
( occurrence_of(X0,sK6(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f163,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(cnf_transformation,[],[f76]) ).
fof(f164,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f78]) ).
fof(f167,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK8(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f169,plain,
! [X2,X0,X1] :
( occurrence_of(sK8(X0,X1,X2),X0)
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f179,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f88]) ).
fof(f184,plain,
! [X0,X1,X5] :
( ~ min_precedes(sK14(X0),X5,tptp0)
| sK16(X0) = X5
| sK15(X0) = X5
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f120]) ).
fof(f186,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| occurrence_of(sK16(X0),tptp2)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK16(X0),tptp1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f120]) ).
fof(f187,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| min_precedes(sK14(X0),sK15(X0),tptp0)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f120]) ).
fof(f188,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK15(X0),tptp4)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f120]) ).
fof(f189,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(X0,sK14(X0),tptp0)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f120]) ).
fof(f190,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK14(X0),tptp3)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f120]) ).
fof(f196,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f39]) ).
fof(f197,plain,
tptp3 != tptp4,
inference(cnf_transformation,[],[f40]) ).
fof(f200,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f43]) ).
fof(f201,plain,
tptp3 != tptp2,
inference(cnf_transformation,[],[f44]) ).
fof(f206,plain,
~ leaf_occ(sK18,sK19),
inference(cnf_transformation,[],[f124]) ).
fof(f207,plain,
arboreal(sK18),
inference(cnf_transformation,[],[f124]) ).
fof(f208,plain,
subactivity_occurrence(sK18,sK19),
inference(cnf_transformation,[],[f124]) ).
fof(f209,plain,
occurrence_of(sK19,tptp0),
inference(cnf_transformation,[],[f124]) ).
fof(f259,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| sK6(X0) = X1
| ~ activity_occurrence(X0) ),
inference(resolution,[],[f164,f158]) ).
fof(f262,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| sK6(X0) = X1 ),
inference(forward_subsumption_resolution,[],[f259,f179]) ).
fof(f412,plain,
( ~ occurrence_of(sK19,tptp0)
| occurrence_of(sK15(sK18),tptp4)
| ~ arboreal(sK18)
| leaf_occ(sK18,sK19) ),
inference(resolution,[],[f188,f208]) ).
fof(f416,plain,
( occurrence_of(sK15(sK18),tptp4)
| ~ arboreal(sK18)
| leaf_occ(sK18,sK19) ),
inference(forward_subsumption_resolution,[],[f412,f209]) ).
fof(f417,plain,
( occurrence_of(sK15(sK18),tptp4)
| leaf_occ(sK18,sK19) ),
inference(forward_subsumption_resolution,[],[f416,f207]) ).
fof(f418,plain,
occurrence_of(sK15(sK18),tptp4),
inference(forward_subsumption_resolution,[],[f417,f206]) ).
fof(f425,plain,
tptp4 = sK6(sK15(sK18)),
inference(resolution,[],[f418,f262]) ).
fof(f427,plain,
( ~ occurrence_of(sK19,tptp0)
| occurrence_of(sK14(sK18),tptp3)
| ~ arboreal(sK18)
| leaf_occ(sK18,sK19) ),
inference(resolution,[],[f190,f208]) ).
fof(f428,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK8(X0,X1,X2),tptp0)
| occurrence_of(sK14(X2),tptp3)
| ~ arboreal(X2)
| leaf_occ(X2,sK8(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(resolution,[],[f190,f167]) ).
fof(f431,plain,
( occurrence_of(sK14(sK18),tptp3)
| ~ arboreal(sK18)
| leaf_occ(sK18,sK19) ),
inference(forward_subsumption_resolution,[],[f427,f209]) ).
fof(f432,plain,
( occurrence_of(sK14(sK18),tptp3)
| leaf_occ(sK18,sK19) ),
inference(forward_subsumption_resolution,[],[f431,f207]) ).
fof(f433,plain,
occurrence_of(sK14(sK18),tptp3),
inference(forward_subsumption_resolution,[],[f432,f206]) ).
fof(f435,plain,
( ~ occurrence_of(sK19,tptp0)
| next_subocc(sK18,sK14(sK18),tptp0)
| ~ arboreal(sK18)
| leaf_occ(sK18,sK19) ),
inference(resolution,[],[f189,f208]) ).
fof(f436,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK8(X0,X1,X2),tptp0)
| next_subocc(X2,sK14(X2),tptp0)
| ~ arboreal(X2)
| leaf_occ(X2,sK8(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(resolution,[],[f189,f167]) ).
fof(f439,plain,
( next_subocc(sK18,sK14(sK18),tptp0)
| ~ arboreal(sK18)
| leaf_occ(sK18,sK19) ),
inference(forward_subsumption_resolution,[],[f435,f209]) ).
fof(f440,plain,
( next_subocc(sK18,sK14(sK18),tptp0)
| leaf_occ(sK18,sK19) ),
inference(forward_subsumption_resolution,[],[f439,f207]) ).
fof(f441,plain,
next_subocc(sK18,sK14(sK18),tptp0),
inference(forward_subsumption_resolution,[],[f440,f206]) ).
fof(f452,plain,
( ~ occurrence_of(sK19,tptp0)
| min_precedes(sK14(sK18),sK15(sK18),tptp0)
| ~ arboreal(sK18)
| leaf_occ(sK18,sK19) ),
inference(resolution,[],[f187,f208]) ).
fof(f456,plain,
( min_precedes(sK14(sK18),sK15(sK18),tptp0)
| ~ arboreal(sK18)
| leaf_occ(sK18,sK19) ),
inference(forward_subsumption_resolution,[],[f452,f209]) ).
fof(f457,plain,
( min_precedes(sK14(sK18),sK15(sK18),tptp0)
| leaf_occ(sK18,sK19) ),
inference(forward_subsumption_resolution,[],[f456,f207]) ).
fof(f458,plain,
min_precedes(sK14(sK18),sK15(sK18),tptp0),
inference(forward_subsumption_resolution,[],[f457,f206]) ).
fof(f461,plain,
( occurrence_of(sK16(sK18),tptp2)
| ~ occurrence_of(sK19,tptp0)
| occurrence_of(sK16(sK18),tptp1)
| ~ arboreal(sK18)
| leaf_occ(sK18,sK19) ),
inference(resolution,[],[f186,f208]) ).
fof(f465,plain,
( occurrence_of(sK16(sK18),tptp2)
| occurrence_of(sK16(sK18),tptp1)
| ~ arboreal(sK18)
| leaf_occ(sK18,sK19) ),
inference(forward_subsumption_resolution,[],[f461,f209]) ).
fof(f466,plain,
( occurrence_of(sK16(sK18),tptp2)
| occurrence_of(sK16(sK18),tptp1)
| leaf_occ(sK18,sK19) ),
inference(forward_subsumption_resolution,[],[f465,f207]) ).
fof(f467,plain,
( occurrence_of(sK16(sK18),tptp2)
| occurrence_of(sK16(sK18),tptp1) ),
inference(forward_subsumption_resolution,[],[f466,f206]) ).
fof(f469,definition,
( spl21_7
<=> occurrence_of(sK16(sK18),tptp1) ),
introduced(definition,[new_symbols(definition,[spl21_7])],[avatar_definition]) ).
fof(f471,plain,
( occurrence_of(sK16(sK18),tptp1)
| ~ spl21_7 ),
inference(avatar_component_clause,[],[f469]) ).
fof(f473,definition,
( spl21_8
<=> occurrence_of(sK16(sK18),tptp2) ),
introduced(definition,[new_symbols(definition,[spl21_8])],[avatar_definition]) ).
fof(f475,plain,
( occurrence_of(sK16(sK18),tptp2)
| ~ spl21_8 ),
inference(avatar_component_clause,[],[f473]) ).
fof(f476,plain,
( spl21_7
| spl21_8 ),
inference(avatar_split_clause,[],[f467,f473,f469]) ).
fof(f478,plain,
( ~ atomic(tptp3)
| arboreal(sK14(sK18)) ),
inference(resolution,[],[f433,f147]) ).
fof(f484,plain,
arboreal(sK14(sK18)),
inference(forward_subsumption_resolution,[],[f478,f196]) ).
fof(f511,plain,
min_precedes(sK18,sK14(sK18),tptp0),
inference(resolution,[],[f441,f130]) ).
fof(f603,plain,
! [X0] :
( ~ leaf_occ(sK14(sK18),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f458,f163]) ).
fof(f652,plain,
! [X0] :
( ~ leaf_occ(sK18,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f511,f163]) ).
fof(f1079,definition,
( spl21_45
<=> ! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ subactivity_occurrence(sK18,X0) ) ),
introduced(definition,[new_symbols(definition,[spl21_45])],[avatar_definition]) ).
fof(f1080,plain,
( ! [X0] :
( ~ subactivity_occurrence(sK18,X0)
| ~ occurrence_of(X0,tptp0) )
| ~ spl21_45 ),
inference(avatar_component_clause,[],[f1079]) ).
fof(f1292,plain,
! [X0,X1] :
( occurrence_of(sK14(X0),tptp3)
| ~ arboreal(X0)
| leaf_occ(X0,sK8(tptp0,X1,X0))
| ~ min_precedes(X1,X0,tptp0)
| ~ min_precedes(X1,X0,tptp0) ),
inference(resolution,[],[f428,f169]) ).
fof(f1293,plain,
! [X0,X1] :
( leaf_occ(X0,sK8(tptp0,X1,X0))
| ~ arboreal(X0)
| occurrence_of(sK14(X0),tptp3)
| ~ min_precedes(X1,X0,tptp0) ),
inference(duplicate_literal_removal,[],[f1292]) ).
fof(f1330,plain,
! [X0,X1] :
( next_subocc(X0,sK14(X0),tptp0)
| ~ arboreal(X0)
| leaf_occ(X0,sK8(tptp0,X1,X0))
| ~ min_precedes(X1,X0,tptp0)
| ~ min_precedes(X1,X0,tptp0) ),
inference(resolution,[],[f436,f169]) ).
fof(f1331,plain,
! [X0,X1] :
( leaf_occ(X0,sK8(tptp0,X1,X0))
| ~ arboreal(X0)
| next_subocc(X0,sK14(X0),tptp0)
| ~ min_precedes(X1,X0,tptp0) ),
inference(duplicate_literal_removal,[],[f1330]) ).
fof(f1780,definition,
( spl21_113
<=> occurrence_of(sK15(sK18),tptp3) ),
introduced(definition,[new_symbols(definition,[spl21_113])],[avatar_definition]) ).
fof(f1781,plain,
( occurrence_of(sK15(sK18),tptp3)
| ~ spl21_113 ),
inference(avatar_component_clause,[],[f1780]) ).
fof(f1782,plain,
( ~ occurrence_of(sK15(sK18),tptp3)
| spl21_113 ),
inference(avatar_component_clause,[],[f1780]) ).
fof(f2739,definition,
( spl21_170
<=> ! [X0] : ~ min_precedes(X0,sK14(sK18),tptp0) ),
introduced(definition,[new_symbols(definition,[spl21_170])],[avatar_definition]) ).
fof(f2740,plain,
( ! [X0] : ~ min_precedes(X0,sK14(sK18),tptp0)
| ~ spl21_170 ),
inference(avatar_component_clause,[],[f2739]) ).
fof(f2759,plain,
( tptp2 = sK6(sK16(sK18))
| ~ spl21_8 ),
inference(resolution,[],[f475,f262]) ).
fof(f2912,plain,
! [X0] :
( ~ arboreal(sK14(sK18))
| occurrence_of(sK14(sK14(sK18)),tptp3)
| ~ min_precedes(X0,sK14(sK18),tptp0)
| ~ occurrence_of(sK8(tptp0,X0,sK14(sK18)),tptp0) ),
inference(resolution,[],[f1293,f603]) ).
fof(f2946,definition,
( spl21_180
<=> occurrence_of(sK14(sK14(sK18)),tptp3) ),
introduced(definition,[new_symbols(definition,[spl21_180])],[avatar_definition]) ).
fof(f2948,plain,
( occurrence_of(sK14(sK14(sK18)),tptp3)
| ~ spl21_180 ),
inference(avatar_component_clause,[],[f2946]) ).
fof(f2956,plain,
( $false
| ~ spl21_170 ),
inference(resolution,[],[f2740,f511]) ).
fof(f2957,plain,
~ spl21_170,
inference(avatar_contradiction_clause,[],[f2956]) ).
fof(f2958,plain,
! [X0] :
( occurrence_of(sK14(sK14(sK18)),tptp3)
| ~ min_precedes(X0,sK14(sK18),tptp0)
| ~ occurrence_of(sK8(tptp0,X0,sK14(sK18)),tptp0) ),
inference(forward_subsumption_resolution,[],[f2912,f484]) ).
fof(f2959,plain,
! [X0] :
( occurrence_of(sK14(sK14(sK18)),tptp3)
| ~ min_precedes(X0,sK14(sK18),tptp0) ),
inference(forward_subsumption_resolution,[],[f2958,f169]) ).
fof(f2960,plain,
( spl21_170
| spl21_180 ),
inference(avatar_split_clause,[],[f2959,f2946,f2739]) ).
fof(f3057,plain,
! [X0] :
( ~ arboreal(sK14(sK18))
| next_subocc(sK14(sK18),sK14(sK14(sK18)),tptp0)
| ~ min_precedes(X0,sK14(sK18),tptp0)
| ~ occurrence_of(sK8(tptp0,X0,sK14(sK18)),tptp0) ),
inference(resolution,[],[f1331,f603]) ).
fof(f3063,plain,
! [X0] :
( next_subocc(sK14(sK18),sK14(sK14(sK18)),tptp0)
| ~ min_precedes(X0,sK14(sK18),tptp0)
| ~ occurrence_of(sK8(tptp0,X0,sK14(sK18)),tptp0) ),
inference(forward_subsumption_resolution,[],[f3057,f484]) ).
fof(f3067,plain,
! [X0] :
( next_subocc(sK14(sK18),sK14(sK14(sK18)),tptp0)
| ~ min_precedes(X0,sK14(sK18),tptp0) ),
inference(forward_subsumption_resolution,[],[f3063,f169]) ).
fof(f3074,definition,
( spl21_182
<=> next_subocc(sK14(sK18),sK14(sK14(sK18)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl21_182])],[avatar_definition]) ).
fof(f3076,plain,
( next_subocc(sK14(sK18),sK14(sK14(sK18)),tptp0)
| ~ spl21_182 ),
inference(avatar_component_clause,[],[f3074]) ).
fof(f3077,plain,
( spl21_170
| spl21_182 ),
inference(avatar_split_clause,[],[f3067,f3074,f2739]) ).
fof(f3098,plain,
( tptp3 = sK6(sK14(sK14(sK18)))
| ~ spl21_180 ),
inference(resolution,[],[f2948,f262]) ).
fof(f3964,plain,
( min_precedes(sK14(sK18),sK14(sK14(sK18)),tptp0)
| ~ spl21_182 ),
inference(resolution,[],[f3076,f130]) ).
fof(f4445,plain,
( ! [X0] :
( sK16(sK18) = sK14(sK14(sK18))
| sK15(sK18) = sK14(sK14(sK18))
| ~ occurrence_of(X0,tptp0)
| ~ subactivity_occurrence(sK18,X0)
| ~ arboreal(sK18)
| leaf_occ(sK18,X0) )
| ~ spl21_182 ),
inference(resolution,[],[f3964,f184]) ).
fof(f4524,plain,
( ! [X0] :
( sK16(sK18) = sK14(sK14(sK18))
| sK15(sK18) = sK14(sK14(sK18))
| ~ occurrence_of(X0,tptp0)
| ~ subactivity_occurrence(sK18,X0)
| ~ arboreal(sK18) )
| ~ spl21_182 ),
inference(forward_subsumption_resolution,[],[f4445,f652]) ).
fof(f4529,plain,
( ! [X0] :
( sK16(sK18) = sK14(sK14(sK18))
| sK15(sK18) = sK14(sK14(sK18))
| ~ occurrence_of(X0,tptp0)
| ~ subactivity_occurrence(sK18,X0) )
| ~ spl21_182 ),
inference(forward_subsumption_resolution,[],[f4524,f207]) ).
fof(f4541,definition,
( spl21_256
<=> occurrence_of(sK14(sK14(sK18)),tptp1) ),
introduced(definition,[new_symbols(definition,[spl21_256])],[avatar_definition]) ).
fof(f4542,plain,
( occurrence_of(sK14(sK14(sK18)),tptp1)
| ~ spl21_256 ),
inference(avatar_component_clause,[],[f4541]) ).
fof(f4547,definition,
( spl21_257
<=> sK15(sK18) = sK14(sK14(sK18)) ),
introduced(definition,[new_symbols(definition,[spl21_257])],[avatar_definition]) ).
fof(f4549,plain,
( sK15(sK18) = sK14(sK14(sK18))
| ~ spl21_257 ),
inference(avatar_component_clause,[],[f4547]) ).
fof(f4551,definition,
( spl21_258
<=> sK16(sK18) = sK14(sK14(sK18)) ),
introduced(definition,[new_symbols(definition,[spl21_258])],[avatar_definition]) ).
fof(f4553,plain,
( sK16(sK18) = sK14(sK14(sK18))
| ~ spl21_258 ),
inference(avatar_component_clause,[],[f4551]) ).
fof(f4554,plain,
( spl21_45
| spl21_257
| spl21_258
| ~ spl21_182 ),
inference(avatar_split_clause,[],[f4529,f3074,f4551,f4547,f1079]) ).
fof(f4588,plain,
( ~ occurrence_of(sK19,tptp0)
| ~ spl21_45 ),
inference(resolution,[],[f1080,f208]) ).
fof(f4593,plain,
( $false
| ~ spl21_45 ),
inference(forward_subsumption_resolution,[],[f4588,f209]) ).
fof(f4594,plain,
~ spl21_45,
inference(avatar_contradiction_clause,[],[f4593]) ).
fof(f4797,plain,
( ~ occurrence_of(sK14(sK14(sK18)),tptp3)
| spl21_113
| ~ spl21_257 ),
inference(superposition,[],[f1782,f4549]) ).
fof(f4829,plain,
( $false
| spl21_113
| ~ spl21_180
| ~ spl21_257 ),
inference(forward_subsumption_resolution,[],[f4797,f2948]) ).
fof(f4830,plain,
( spl21_113
| ~ spl21_180
| ~ spl21_257 ),
inference(avatar_contradiction_clause,[],[f4829]) ).
fof(f5150,plain,
( tptp3 = sK6(sK15(sK18))
| ~ spl21_113 ),
inference(resolution,[],[f1781,f262]) ).
fof(f5152,plain,
( tptp3 = tptp4
| ~ spl21_113 ),
inference(forward_demodulation,[],[f5150,f425]) ).
fof(f5157,plain,
( $false
| ~ spl21_113 ),
inference(forward_subsumption_resolution,[],[f5152,f197]) ).
fof(f5158,plain,
~ spl21_113,
inference(avatar_contradiction_clause,[],[f5157]) ).
fof(f5275,plain,
( tptp2 = sK6(sK14(sK14(sK18)))
| ~ spl21_8
| ~ spl21_258 ),
inference(superposition,[],[f2759,f4553]) ).
fof(f5296,plain,
( tptp3 = tptp2
| ~ spl21_8
| ~ spl21_180
| ~ spl21_258 ),
inference(forward_demodulation,[],[f5275,f3098]) ).
fof(f5306,plain,
( $false
| ~ spl21_8
| ~ spl21_180
| ~ spl21_258 ),
inference(forward_subsumption_resolution,[],[f5296,f201]) ).
fof(f5307,plain,
( ~ spl21_8
| ~ spl21_180
| ~ spl21_258 ),
inference(avatar_contradiction_clause,[],[f5306]) ).
fof(f5308,plain,
( occurrence_of(sK14(sK14(sK18)),tptp1)
| ~ spl21_7
| ~ spl21_258 ),
inference(forward_demodulation,[],[f471,f4553]) ).
fof(f5351,plain,
( spl21_256
| ~ spl21_7
| ~ spl21_258 ),
inference(avatar_split_clause,[],[f5308,f4551,f469,f4541]) ).
fof(f5456,plain,
( tptp1 = sK6(sK14(sK14(sK18)))
| ~ spl21_256 ),
inference(resolution,[],[f4542,f262]) ).
fof(f5458,plain,
( tptp3 = tptp1
| ~ spl21_180
| ~ spl21_256 ),
inference(forward_demodulation,[],[f5456,f3098]) ).
fof(f5459,plain,
( $false
| ~ spl21_180
| ~ spl21_256 ),
inference(forward_subsumption_resolution,[],[f5458,f200]) ).
fof(f5460,plain,
( ~ spl21_180
| ~ spl21_256 ),
inference(avatar_contradiction_clause,[],[f5459]) ).
cnf(s4,plain,
( spl21_7
| spl21_8 ),
inference(sat_conversion,[],[f476]) ).
cnf(s139,plain,
~ spl21_170,
inference(sat_conversion,[],[f2957]) ).
cnf(s140,plain,
( spl21_170
| spl21_180 ),
inference(sat_conversion,[],[f2960]) ).
cnf(s144,plain,
( spl21_170
| spl21_182 ),
inference(sat_conversion,[],[f3077]) ).
cnf(s214,plain,
( spl21_45
| ~ spl21_182
| spl21_257
| spl21_258 ),
inference(sat_conversion,[],[f4554]) ).
cnf(s217,plain,
~ spl21_45,
inference(sat_conversion,[],[f4594]) ).
cnf(s227,plain,
( spl21_113
| ~ spl21_180
| ~ spl21_257 ),
inference(sat_conversion,[],[f4830]) ).
cnf(s246,plain,
~ spl21_113,
inference(sat_conversion,[],[f5158]) ).
cnf(s255,plain,
( ~ spl21_8
| ~ spl21_180
| ~ spl21_258 ),
inference(sat_conversion,[],[f5307]) ).
cnf(s256,plain,
( ~ spl21_7
| spl21_256
| ~ spl21_258 ),
inference(sat_conversion,[],[f5351]) ).
cnf(s270,plain,
( ~ spl21_180
| ~ spl21_256 ),
inference(sat_conversion,[],[f5460]) ).
cnf(s271,plain,
( ~ spl21_180
| ~ spl21_257 ),
inference(rat,[],[s227,s246]) ).
cnf(s273,plain,
( ~ spl21_182
| spl21_257
| spl21_258 ),
inference(rat,[],[s214,s217]) ).
cnf(s276,plain,
spl21_182,
inference(rat,[],[s144,s139]) ).
cnf(s277,plain,
spl21_180,
inference(rat,[],[s140,s139]) ).
cnf(s279,plain,
~ spl21_256,
inference(rat,[],[s270,s277]) ).
cnf(s280,plain,
~ spl21_257,
inference(rat,[],[s271,s277]) ).
cnf(s282,plain,
spl21_258,
inference(rat,[],[s273,s276,s280]) ).
cnf(s283,plain,
~ spl21_8,
inference(rat,[],[s255,s277,s282]) ).
cnf(s285,plain,
~ spl21_7,
inference(rat,[],[s256,s279,s282]) ).
cnf(s308,plain,
$false,
inference(rat,[],[s4,s283,s285]) ).
fof(f5461,plain,
$false,
inference(avatar_sat_refutation,[],[s308]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO018+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.31 % Computer : n012.cluster.edu
% 0.06/0.31 % Model : x86_64 x86_64
% 0.06/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.31 % Memory : 8046.5625MB
% 0.06/0.31 % OS : Linux 6.8.0-71-generic
% 0.06/0.31 % CPULimit : 300
% 0.06/0.31 % WCLimit : 300
% 0.06/0.31 % DateTime : Sun Sep 27 22:24:49 UTC 2026
% 0.06/0.32 % CPUTime :
% 0.06/0.32 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.33 Running first-order model finding
% 0.09/0.33 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.83/0.69 % (2815442)Will run a generic schedule for satisfiability detection.
% 1.83/0.69 % (2815448)% WARNING: option uhcvi not known.
% 1.83/0.69 % (2815451)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1845821554:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.83/0.69 % (2815448)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=635984137:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.83/0.69 % (2815447)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3857242914_2999 on theBenchmark for (2999ds/0Mi)
% 1.83/0.69 % (2815449)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1815829132:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.83/0.69 % (2815450)dis+10_1_sil=32000:sp=arity:random_seed=3062534976:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.83/0.69 % (2815452)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2951465205:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.83/0.69 % (2815453)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1313638248:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.83/0.69 % Detected minimum model sizes of [4]
% 1.83/0.69 % Detected maximum model sizes of [max]
% 1.83/0.69 % TRYING [4]
% 1.83/0.69 % TRYING [5]
% 1.83/0.69 % TRYING [6]
% 1.83/0.69 % (2815450)Instruction limit reached!
% 1.83/0.69 % (2815450)------------------------------
% 1.83/0.69 % (2815450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.69 % (2815450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.69 % (2815450)CaDiCaL version: 2.1.3
% 1.83/0.69 % (2815450)Termination reason: Instruction limit
% 1.83/0.69 % (2815450)Termination phase: Saturation
% 1.83/0.69 % (2815450)Time elapsed: 0.039 s
% 1.83/0.69 % (2815450)Peak memory usage: 13 MB
% 1.83/0.69 % (2815450)Instructions burned: 105 (million)
% 1.83/0.69 % (2815451)Instruction limit reached!
% 1.83/0.69 % (2815451)------------------------------
% 1.83/0.69 % (2815451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.69 % (2815451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.69 % (2815451)CaDiCaL version: 2.1.3
% 1.83/0.69 % (2815451)Termination reason: Instruction limit
% 1.83/0.69 % (2815451)Termination phase: Saturation
% 1.83/0.69 % (2815451)Time elapsed: 0.041 s
% 1.83/0.69 % (2815451)Peak memory usage: 13 MB
% 1.83/0.69 % (2815451)Instructions burned: 117 (million)
% 1.83/0.69 % (2815452)Instruction limit reached!
% 1.83/0.69 % (2815452)------------------------------
% 1.83/0.69 % (2815452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.69 % (2815452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.69 % (2815452)CaDiCaL version: 2.1.3
% 1.83/0.69 % (2815452)Termination reason: Instruction limit
% 1.83/0.69 % (2815452)Termination phase: Saturation
% 1.83/0.69 % (2815452)Time elapsed: 0.048 s
% 1.83/0.69 % (2815452)Peak memory usage: 13 MB
% 1.83/0.69 % (2815452)Instructions burned: 133 (million)
% 1.83/0.69 % (2815461)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4117958735:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.83/0.69 % (2815462)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3620551646:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.83/0.69 % Detected minimum model sizes of [4]
% 1.83/0.69 % Detected maximum model sizes of [max]
% 1.83/0.69 % TRYING [4]
% 1.83/0.69 % (2815463)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=1741374956:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.83/0.69 % TRYING [5]
% 1.83/0.69 % (2815453)Instruction limit reached!
% 1.83/0.69 % (2815453)------------------------------
% 1.83/0.69 % (2815453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.69 % (2815453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.69 % (2815453)CaDiCaL version: 2.1.3
% 1.83/0.69 % (2815453)Termination reason: Instruction limit
% 1.83/0.69 % (2815453)Termination phase: Saturation
% 1.83/0.69 % (2815453)Time elapsed: 0.063 s
% 1.83/0.69 % (2815453)Peak memory usage: 14 MB
% 1.83/0.69 % (2815453)Instructions burned: 160 (million)
% 1.83/0.69 % (2815467)ott-21_1_sil=16000:fs=off:random_seed=598395166:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 1.83/0.69 % TRYING [6]
% 1.83/0.69 % TRYING [7]
% 1.83/0.69 % (2815462)Instruction limit reached!
% 1.83/0.69 % (2815462)------------------------------
% 1.83/0.69 % (2815462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.69 % (2815462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.69 % (2815462)CaDiCaL version: 2.1.3
% 1.83/0.69 % (2815462)Termination reason: Instruction limit
% 1.83/0.69 % (2815462)Termination phase: Saturation
% 1.83/0.69 % (2815462)Time elapsed: 0.049 s
% 1.83/0.69 % (2815462)Peak memory usage: 13 MB
% 1.83/0.69 % (2815462)Instructions burned: 133 (million)
% 1.83/0.69 % (2815469)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=81349329:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.83/0.69 % (2815467)Instruction limit reached!
% 1.83/0.69 % (2815467)------------------------------
% 1.83/0.69 % (2815467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.69 % (2815467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.69 % (2815467)CaDiCaL version: 2.1.3
% 1.83/0.69 % (2815467)Termination reason: Instruction limit
% 1.83/0.69 % (2815467)Termination phase: Saturation
% 1.83/0.69 % (2815467)Time elapsed: 0.051 s
% 1.83/0.69 % (2815467)Peak memory usage: 12 MB
% 1.83/0.69 % (2815467)Instructions burned: 182 (million)
% 1.83/0.69 % (2815471)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3384304326:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.83/0.69 % Detected minimum model sizes of [4]
% 1.83/0.69 % Detected maximum model sizes of [max]
% 1.83/0.69 % TRYING [4]
% 1.83/0.69 % TRYING [7]
% 1.83/0.69 % TRYING [5]
% 1.83/0.69 % TRYING [6]
% 1.83/0.69 % TRYING [8]
% 1.83/0.69 % (2815461)Instruction limit reached!
% 1.83/0.69 % (2815461)------------------------------
% 1.83/0.69 % (2815461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.69 % (2815461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.69 % (2815461)CaDiCaL version: 2.1.3
% 1.83/0.69 % (2815461)Termination reason: Instruction limit
% 1.83/0.69 % (2815461)Termination phase: Finite model building SAT solving
% 1.83/0.69 % (2815461)Time elapsed: 0.183 s
% 1.83/0.69 % (2815461)Peak memory usage: 28 MB
% 1.83/0.69 % (2815461)Instructions burned: 716 (million)
% 1.83/0.69 % (2815463)Instruction limit reached!
% 1.83/0.69 % (2815463)------------------------------
% 1.83/0.69 % (2815463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.69 % (2815463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.69 % (2815463)CaDiCaL version: 2.1.3
% 1.83/0.69 % (2815463)Termination reason: Instruction limit
% 1.83/0.69 % (2815463)Termination phase: Saturation
% 1.83/0.69 % (2815463)Time elapsed: 0.182 s
% 1.83/0.69 % (2815463)Peak memory usage: 17 MB
% 1.83/0.69 % (2815463)Instructions burned: 685 (million)
% 1.83/0.69 % (2815473)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2634533822:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.83/0.69 % TRYING [7]
% 1.83/0.69 % (2815474)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3482050602:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 1.83/0.69 % (2815469)Instruction limit reached!
% 1.83/0.69 % (2815469)------------------------------
% 1.83/0.69 % (2815469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.69 % (2815469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.69 % (2815469)CaDiCaL version: 2.1.3
% 1.83/0.69 % (2815469)Termination reason: Instruction limit
% 1.83/0.69 % (2815469)Termination phase: Saturation
% 1.83/0.69 % (2815469)Time elapsed: 0.189 s
% 1.83/0.69 % (2815469)Peak memory usage: 14 MB
% 1.83/0.69 % (2815469)Instructions burned: 477 (million)
% 1.83/0.69 % TRYING [14]
% 1.83/0.69 % (2815477)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2823472759:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 1.83/0.69 % (2815473) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2815442-2815473"...
% 1.83/0.69 % (2815473)...printing done.
% 1.83/0.69 % (2815473)Refutation found. Thanks to Tanya!
% 1.83/0.69 % SZS status Theorem for theBenchmark
% 1.83/0.69 % SZS output start Proof for theBenchmark
% See solution above
% 1.83/0.70 % (2815473)------------------------------
% 1.83/0.70 % (2815473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.83/0.70 % (2815473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.83/0.70 % (2815473)CaDiCaL version: 2.1.3
% 1.83/0.70 % (2815473)Termination reason: Refutation
% 1.83/0.70 % (2815473)Time elapsed: 0.070 s
% 1.83/0.70 % (2815473)Peak memory usage: 15 MB
% 1.83/0.70 % (2815473)Instructions burned: 193 (million)
% 1.83/0.70 % (2815442)Success in time 0.353 s
% 1.83/0.70 % Vampire exiting
%------------------------------------------------------------------------------