%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRO014+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:39 PM UTC 2026
% Result : Theorem 66.93s 10.01s
% Output : Refutation 66.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 16
% Syntax : Number of formulae : 108 ( 32 unt; 2 def)
% Number of atoms : 391 ( 14 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 462 ( 179 ~; 171 |; 96 &)
% ( 7 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 3 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-3 aty)
% Number of variables : 181 ( 0 sgn 153 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
fof(f8,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_07) ).
fof(f23,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/sandbox2/benchmark/theBenchmark.p',sos_22) ).
fof(f30,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X0,X1,X2)
& occurrence_of(X3,X2)
& subactivity_occurrence(X1,X3) )
=> subactivity_occurrence(X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_29) ).
fof(f35,axiom,
! [X0,X1] :
( leaf_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_34) ).
fof(f38,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& leaf_occ(X1,X0) )
=> ~ ? [X3] : min_precedes(X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_37) ).
fof(f44,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& subactivity_occurrence(X2,X1)
& leaf_occ(X3,X1)
& arboreal(X2)
& ~ min_precedes(X2,X3,X0) )
=> X3 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_43) ).
fof(f46,axiom,
! [X0,X1] :
( ( leaf(X0,X1)
& ~ atomic(X1) )
=> ? [X2] :
( occurrence_of(X2,X1)
& leaf_occ(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_45) ).
fof(f50,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)
& next_subocc(X2,X3,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& next_subocc(X3,X4,tptp0)
& leaf(X4,tptp0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_49) ).
fof(f52,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_51) ).
fof(f56,axiom,
atomic(tptp3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_55) ).
fof(f60,axiom,
tptp3 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_59) ).
fof(f61,axiom,
tptp3 != tptp1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_60) ).
fof(f63,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,tptp2)
| occurrence_of(X3,tptp1) )
& min_precedes(X2,X3,tptp0)
& leaf(X3,tptp0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f64,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,tptp2)
| occurrence_of(X3,tptp1) )
& min_precedes(X2,X3,tptp0)
& leaf(X3,tptp0) ) ),
inference(negated_conjecture,[status(cth)],[f63]) ).
fof(f68,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f3]) ).
fof(f69,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f68]) ).
fof(f76,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f94,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,[],[f23]) ).
fof(f103,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ min_precedes(X0,X1,X2)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(ennf_transformation,[],[f30]) ).
fof(f104,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ min_precedes(X0,X1,X2)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(flattening,[],[f103]) ).
fof(f116,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f117,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(flattening,[],[f116]) ).
fof(f128,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| ~ leaf_occ(X3,X1)
| ~ arboreal(X2)
| min_precedes(X2,X3,X0) ),
inference(ennf_transformation,[],[f44]) ).
fof(f129,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| ~ leaf_occ(X3,X1)
| ~ arboreal(X2)
| min_precedes(X2,X3,X0) ),
inference(flattening,[],[f128]) ).
fof(f131,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,X1)
& leaf_occ(X0,X2) )
| ~ leaf(X0,X1)
| atomic(X1) ),
inference(ennf_transformation,[],[f46]) ).
fof(f132,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,X1)
& leaf_occ(X0,X2) )
| ~ leaf(X0,X1)
| atomic(X1) ),
inference(flattening,[],[f131]) ).
fof(f138,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X3,tptp4)
& next_subocc(X2,X3,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& next_subocc(X3,X4,tptp0)
& leaf(X4,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f50]) ).
fof(f139,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X3,tptp4)
& next_subocc(X2,X3,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& next_subocc(X3,X4,tptp0)
& leaf(X4,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(flattening,[],[f138]) ).
fof(f140,plain,
? [X0,X1] :
( ! [X2,X3] :
( ~ occurrence_of(X2,tptp3)
| ~ next_subocc(X0,X2,tptp0)
| ( ~ occurrence_of(X3,tptp2)
& ~ occurrence_of(X3,tptp1) )
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf(X3,tptp0) )
& occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f64]) ).
fof(f141,plain,
? [X0,X1] :
( ! [X2,X3] :
( ~ occurrence_of(X2,tptp3)
| ~ next_subocc(X0,X2,tptp0)
| ( ~ occurrence_of(X3,tptp2)
& ~ occurrence_of(X3,tptp1) )
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf(X3,tptp0) )
& occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) ),
inference(flattening,[],[f140]) ).
fof(f143,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f76]) ).
fof(f153,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,[],[f94]) ).
fof(f154,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,[],[f153]) ).
fof(f155,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,[],[f154]) ).
fof(f156,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ( min_precedes(X0,sK7(X0,X1,X2),X2)
& min_precedes(sK7(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,[sK7]),skolemize(X3,sK7(X0,X1,X2))],[f155]) ).
fof(f164,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) )
| ~ leaf_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f35]) ).
fof(f165,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ? [X3] :
( occurrence_of(X1,X3)
& subactivity_occurrence(X0,X1)
& leaf(X0,X3) )
| ~ leaf_occ(X0,X1) ) ),
inference(rectify,[],[f164]) ).
fof(f166,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ( occurrence_of(X1,sK13(X0,X1))
& subactivity_occurrence(X0,X1)
& leaf(X0,sK13(X0,X1)) )
| ~ leaf_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X3,sK13(X0,X1))],[f165]) ).
fof(f167,plain,
! [X0,X1] :
( ( occurrence_of(sK14(X0,X1),X1)
& leaf_occ(X0,sK14(X0,X1)) )
| ~ leaf(X0,X1)
| atomic(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X2,sK14(X0,X1))],[f132]) ).
fof(f168,plain,
! [X0,X1] :
( ( occurrence_of(sK15(X0),tptp3)
& next_subocc(X0,sK15(X0),tptp0)
& occurrence_of(sK16(X0),tptp4)
& next_subocc(sK15(X0),sK16(X0),tptp0)
& ( occurrence_of(sK17(X0),tptp2)
| occurrence_of(sK17(X0),tptp1) )
& next_subocc(sK16(X0),sK17(X0),tptp0)
& leaf(sK17(X0),tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16,sK17]),skolemize(X2,sK15(X0)),skolemize(X3,sK16(X0)),skolemize(X4,sK17(X0))],[f139]) ).
fof(f169,plain,
( ! [X2,X3] :
( ~ occurrence_of(X2,tptp3)
| ~ next_subocc(sK18,X2,tptp0)
| ( ~ occurrence_of(X3,tptp2)
& ~ occurrence_of(X3,tptp1) )
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf(X3,tptp0) )
& occurrence_of(sK19,tptp0)
& subactivity_occurrence(sK18,sK19)
& arboreal(sK18)
& ~ leaf_occ(sK18,sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19]),skolemize(X0,sK18),skolemize(X1,sK19)],[f141]) ).
fof(f174,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f69]) ).
fof(f180,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f206,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f156]) ).
fof(f223,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| subactivity_occurrence(X0,X3)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(cnf_transformation,[],[f104]) ).
fof(f230,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f166]) ).
fof(f235,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f241,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X3,X1)
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| X2 = X3
| ~ arboreal(X2)
| min_precedes(X2,X3,X0) ),
inference(cnf_transformation,[],[f129]) ).
fof(f244,plain,
! [X0,X1] :
( ~ leaf(X0,X1)
| leaf_occ(X0,sK14(X0,X1))
| atomic(X1) ),
inference(cnf_transformation,[],[f167]) ).
fof(f245,plain,
! [X0,X1] :
( ~ leaf(X0,X1)
| occurrence_of(sK14(X0,X1),X1)
| atomic(X1) ),
inference(cnf_transformation,[],[f167]) ).
fof(f249,plain,
! [X0,X1] :
( leaf(sK17(X0),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
fof(f250,plain,
! [X0,X1] :
( next_subocc(sK16(X0),sK17(X0),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
fof(f251,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| occurrence_of(sK17(X0),tptp1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK17(X0),tptp2)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
fof(f252,plain,
! [X0,X1] :
( next_subocc(sK15(X0),sK16(X0),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
fof(f254,plain,
! [X0,X1] :
( next_subocc(X0,sK15(X0),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
fof(f255,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK15(X0),tptp3)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
fof(f257,plain,
~ atomic(tptp0),
inference(cnf_transformation,[],[f52]) ).
fof(f261,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f56]) ).
fof(f265,plain,
tptp3 != tptp2,
inference(cnf_transformation,[],[f60]) ).
fof(f266,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f61]) ).
fof(f268,plain,
~ leaf_occ(sK18,sK19),
inference(cnf_transformation,[],[f169]) ).
fof(f269,plain,
arboreal(sK18),
inference(cnf_transformation,[],[f169]) ).
fof(f270,plain,
subactivity_occurrence(sK18,sK19),
inference(cnf_transformation,[],[f169]) ).
fof(f271,plain,
occurrence_of(sK19,tptp0),
inference(cnf_transformation,[],[f169]) ).
fof(f272,plain,
! [X2,X3] :
( ~ next_subocc(sK18,X2,tptp0)
| ~ occurrence_of(X2,tptp3)
| ~ occurrence_of(X3,tptp1)
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf(X3,tptp0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f273,plain,
! [X2,X3] :
( ~ next_subocc(sK18,X2,tptp0)
| ~ occurrence_of(X2,tptp3)
| ~ occurrence_of(X3,tptp2)
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf(X3,tptp0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f7977,plain,
leaf(sK17(sK18),tptp0),
inference(unit_resulting_resolution,[],[f249,f269,f268,f270,f271]) ).
fof(f7986,plain,
occurrence_of(sK14(sK17(sK18),tptp0),tptp0),
inference(unit_resulting_resolution,[],[f245,f257,f7977]) ).
fof(f7987,plain,
leaf_occ(sK17(sK18),sK14(sK17(sK18),tptp0)),
inference(unit_resulting_resolution,[],[f244,f257,f7977]) ).
fof(f8219,plain,
subactivity_occurrence(sK17(sK18),sK14(sK17(sK18),tptp0)),
inference(unit_resulting_resolution,[],[f230,f7987]) ).
fof(f9238,plain,
occurrence_of(sK15(sK18),tptp3),
inference(unit_resulting_resolution,[],[f255,f269,f268,f270,f271]) ).
fof(f9311,plain,
arboreal(sK15(sK18)),
inference(unit_resulting_resolution,[],[f180,f261,f9238]) ).
fof(f9930,plain,
next_subocc(sK18,sK15(sK18),tptp0),
inference(unit_resulting_resolution,[],[f254,f269,f268,f270,f271]) ).
fof(f9966,plain,
min_precedes(sK18,sK15(sK18),tptp0),
inference(unit_resulting_resolution,[],[f206,f9930]) ).
fof(f10036,plain,
! [X0] :
( ~ leaf_occ(sK18,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f9966,f235]) ).
fof(f11266,plain,
next_subocc(sK16(sK18),sK17(sK18),tptp0),
inference(unit_resulting_resolution,[],[f250,f269,f268,f270,f271]) ).
fof(f11277,plain,
min_precedes(sK16(sK18),sK17(sK18),tptp0),
inference(unit_resulting_resolution,[],[f206,f11266]) ).
fof(f11305,plain,
subactivity_occurrence(sK16(sK18),sK14(sK17(sK18),tptp0)),
inference(unit_resulting_resolution,[],[f223,f7986,f8219,f11277]) ).
fof(f11752,plain,
next_subocc(sK15(sK18),sK16(sK18),tptp0),
inference(unit_resulting_resolution,[],[f252,f269,f268,f270,f271]) ).
fof(f11763,plain,
min_precedes(sK15(sK18),sK16(sK18),tptp0),
inference(unit_resulting_resolution,[],[f206,f11752]) ).
fof(f12413,plain,
subactivity_occurrence(sK15(sK18),sK14(sK17(sK18),tptp0)),
inference(unit_resulting_resolution,[],[f223,f11763,f7986,f11305]) ).
fof(f12994,plain,
( occurrence_of(sK17(sK18),tptp1)
| ~ occurrence_of(sK19,tptp0)
| occurrence_of(sK17(sK18),tptp2)
| ~ arboreal(sK18)
| leaf_occ(sK18,sK19) ),
inference(resolution,[],[f251,f270]) ).
fof(f12999,plain,
( occurrence_of(sK17(sK18),tptp1)
| ~ occurrence_of(sK19,tptp0)
| occurrence_of(sK17(sK18),tptp2)
| ~ arboreal(sK18) ),
inference(forward_subsumption_resolution,[],[f12994,f10036]) ).
fof(f13018,plain,
( occurrence_of(sK17(sK18),tptp1)
| occurrence_of(sK17(sK18),tptp2)
| ~ arboreal(sK18) ),
inference(forward_subsumption_resolution,[],[f12999,f271]) ).
fof(f13033,plain,
( occurrence_of(sK17(sK18),tptp1)
| occurrence_of(sK17(sK18),tptp2) ),
inference(forward_subsumption_resolution,[],[f13018,f269]) ).
fof(f14815,definition,
( spl20_18
<=> occurrence_of(sK17(sK18),tptp2) ),
introduced(definition,[new_symbols(definition,[spl20_18])],[avatar_definition]) ).
fof(f14817,plain,
( occurrence_of(sK17(sK18),tptp2)
| ~ spl20_18 ),
inference(avatar_component_clause,[],[f14815]) ).
fof(f14819,definition,
( spl20_19
<=> occurrence_of(sK17(sK18),tptp1) ),
introduced(definition,[new_symbols(definition,[spl20_19])],[avatar_definition]) ).
fof(f14821,plain,
( occurrence_of(sK17(sK18),tptp1)
| ~ spl20_19 ),
inference(avatar_component_clause,[],[f14819]) ).
fof(f14822,plain,
( spl20_18
| spl20_19 ),
inference(avatar_split_clause,[],[f13033,f14819,f14815]) ).
fof(f14823,plain,
( ~ min_precedes(sK15(sK18),sK17(sK18),tptp0)
| ~ spl20_18 ),
inference(unit_resulting_resolution,[],[f273,f9238,f9930,f7977,f14817]) ).
fof(f14827,plain,
( ~ occurrence_of(sK17(sK18),tptp3)
| ~ spl20_18 ),
inference(unit_resulting_resolution,[],[f174,f265,f14817]) ).
fof(f14956,plain,
( sK17(sK18) = sK15(sK18)
| ~ spl20_18 ),
inference(unit_resulting_resolution,[],[f241,f9311,f7986,f7987,f12413,f14823]) ).
fof(f14957,plain,
( occurrence_of(sK17(sK18),tptp3)
| ~ spl20_18 ),
inference(superposition,[],[f9238,f14956]) ).
fof(f15199,plain,
( $false
| ~ spl20_18 ),
inference(forward_subsumption_resolution,[],[f14957,f14827]) ).
fof(f15200,plain,
~ spl20_18,
inference(avatar_contradiction_clause,[],[f15199]) ).
fof(f15207,plain,
( ~ min_precedes(sK15(sK18),sK17(sK18),tptp0)
| ~ spl20_19 ),
inference(unit_resulting_resolution,[],[f272,f9238,f9930,f7977,f14821]) ).
fof(f15210,plain,
( ~ occurrence_of(sK17(sK18),tptp3)
| ~ spl20_19 ),
inference(unit_resulting_resolution,[],[f174,f266,f14821]) ).
fof(f15420,plain,
( sK17(sK18) = sK15(sK18)
| ~ spl20_19 ),
inference(unit_resulting_resolution,[],[f241,f9311,f7986,f7987,f12413,f15207]) ).
fof(f15421,plain,
( occurrence_of(sK17(sK18),tptp3)
| ~ spl20_19 ),
inference(superposition,[],[f9238,f15420]) ).
fof(f15663,plain,
( $false
| ~ spl20_19 ),
inference(forward_subsumption_resolution,[],[f15421,f15210]) ).
fof(f15664,plain,
~ spl20_19,
inference(avatar_contradiction_clause,[],[f15663]) ).
cnf(s22,plain,
( spl20_18
| spl20_19 ),
inference(sat_conversion,[],[f14822]) ).
cnf(s39,plain,
~ spl20_18,
inference(sat_conversion,[],[f15200]) ).
cnf(s55,plain,
~ spl20_19,
inference(sat_conversion,[],[f15664]) ).
cnf(s56,plain,
$false,
inference(rat,[],[s22,s55,s39]) ).
fof(f15668,plain,
$false,
inference(avatar_sat_refutation,[],[s56]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO014+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n017.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 22:20:21 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.43 Running first-order model finding
% 0.12/0.43 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
% 19.05/3.15 % (2993305)Will run a generic schedule for satisfiability detection.
% 19.05/3.15 % (2993314)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=350118193:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 19.05/3.15 % (2993313)dis+10_1_sil=32000:sp=arity:random_seed=205305215:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 19.05/3.15 % (2993311)% WARNING: option uhcvi not known.
% 19.05/3.15 % (2993311)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1824080606:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 19.05/3.15 % (2993315)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1882039789:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 19.05/3.15 % (2993316)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=73344374:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 19.05/3.15 % (2993312)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=241872978:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 19.05/3.15 % (2993310)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2983124751_2999 on theBenchmark for (2999ds/0Mi)
% 19.05/3.15 % Detected minimum model sizes of [4]
% 19.05/3.15 % Detected maximum model sizes of [max]
% 19.05/3.15 % TRYING [4]
% 19.05/3.15 % (2993314)Instruction limit reached!
% 19.05/3.15 % (2993314)------------------------------
% 19.05/3.15 % (2993314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.05/3.15 % (2993314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.05/3.15 % (2993314)CaDiCaL version: 2.1.3
% 19.05/3.15 % (2993314)Termination reason: Instruction limit
% 19.05/3.15 % (2993314)Termination phase: Saturation
% 19.05/3.15 % (2993314)Time elapsed: 0.044 s
% 19.05/3.15 % (2993314)Peak memory usage: 12 MB
% 19.05/3.15 % (2993314)Instructions burned: 118 (million)
% 19.05/3.15 % TRYING [5]
% 19.05/3.15 % (2993325)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4194656548:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 19.05/3.15 % Detected minimum model sizes of [4]
% 19.05/3.15 % Detected maximum model sizes of [max]
% 19.05/3.15 % TRYING [4]
% 19.05/3.15 % (2993313)Instruction limit reached!
% 19.05/3.15 % (2993313)------------------------------
% 19.05/3.15 % (2993313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.05/3.15 % (2993313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.05/3.15 % (2993313)CaDiCaL version: 2.1.3
% 19.05/3.15 % (2993313)Termination reason: Instruction limit
% 19.05/3.15 % (2993313)Termination phase: Saturation
% 19.05/3.15 % (2993313)Time elapsed: 0.095 s
% 19.05/3.15 % (2993313)Peak memory usage: 12 MB
% 19.05/3.15 % (2993313)Instructions burned: 104 (million)
% 19.05/3.15 % TRYING [5]
% 19.05/3.15 % (2993329)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=553060826:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 19.05/3.15 % TRYING [6]
% 19.05/3.15 % (2993316)Instruction limit reached!
% 19.05/3.15 % (2993316)------------------------------
% 19.05/3.15 % (2993316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.05/3.15 % (2993316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.05/3.15 % (2993316)CaDiCaL version: 2.1.3
% 19.05/3.15 % (2993316)Termination reason: Instruction limit
% 19.05/3.15 % (2993316)Termination phase: Saturation
% 19.05/3.15 % (2993316)Time elapsed: 0.138 s
% 19.05/3.15 % (2993316)Peak memory usage: 14 MB
% 19.05/3.15 % (2993316)Instructions burned: 160 (million)
% 19.05/3.15 % (2993315)Instruction limit reached!
% 19.05/3.15 % (2993315)------------------------------
% 19.05/3.15 % (2993315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.05/3.15 % (2993315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.05/3.15 % (2993315)CaDiCaL version: 2.1.3
% 19.05/3.15 % (2993315)Termination reason: Instruction limit
% 19.05/3.15 % (2993315)Termination phase: Saturation
% 19.05/3.15 % (2993315)Time elapsed: 0.147 s
% 19.05/3.15 % (2993315)Peak memory usage: 14 MB
% 19.05/3.15 % (2993315)Instructions burned: 131 (million)
% 19.05/3.15 % (2993332)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=492974001:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 19.05/3.15 % (2993329)Instruction limit reached!
% 19.05/3.15 % (2993329)------------------------------
% 19.05/3.15 % (2993329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.05/3.15 % (2993329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.95/6.38 % (2993329)CaDiCaL version: 2.1.3
% 36.95/6.38 % (2993329)Termination reason: Instruction limit
% 36.95/6.38 % (2993329)Termination phase: Saturation
% 36.95/6.38 % (2993329)Time elapsed: 0.068 s
% 36.95/6.38 % (2993329)Peak memory usage: 14 MB
% 36.95/6.38 % (2993329)Instructions burned: 133 (million)
% 36.95/6.38 % (2993333)ott-21_1_sil=16000:fs=off:random_seed=421949966:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 36.95/6.38 % (2993335)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1335525027:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 36.95/6.38 % TRYING [6]
% 36.95/6.38 % TRYING [7]
% 36.95/6.38 % TRYING [7]
% 36.95/6.38 % (2993333)Instruction limit reached!
% 36.95/6.38 % (2993333)------------------------------
% 36.95/6.38 % (2993333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.95/6.38 % (2993333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.95/6.38 % (2993333)CaDiCaL version: 2.1.3
% 36.95/6.38 % (2993333)Termination reason: Instruction limit
% 36.95/6.38 % (2993333)Termination phase: Saturation
% 36.95/6.38 % (2993333)Time elapsed: 0.174 s
% 36.95/6.38 % (2993333)Peak memory usage: 13 MB
% 36.95/6.38 % (2993333)Instructions burned: 180 (million)
% 36.95/6.38 % (2993341)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3462406516:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 36.95/6.38 % Detected minimum model sizes of [4]
% 36.95/6.38 % Detected maximum model sizes of [max]
% 36.95/6.38 % TRYING [4]
% 36.95/6.38 % TRYING [5]
% 36.95/6.38 % (2993335)Instruction limit reached!
% 36.95/6.38 % (2993335)------------------------------
% 36.95/6.38 % (2993335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.95/6.38 % (2993335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.95/6.38 % (2993335)CaDiCaL version: 2.1.3
% 36.95/6.38 % (2993335)Termination reason: Instruction limit
% 36.95/6.38 % (2993335)Termination phase: Saturation
% 36.95/6.38 % (2993335)Time elapsed: 0.278 s
% 36.95/6.38 % (2993335)Peak memory usage: 15 MB
% 36.95/6.38 % (2993335)Instructions burned: 477 (million)
% 36.95/6.38 % (2993345)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2869284280:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 36.95/6.38 % TRYING [6]
% 36.95/6.38 % TRYING [8]
% 36.95/6.38 % (2993325)Instruction limit reached!
% 36.95/6.38 % (2993325)------------------------------
% 36.95/6.38 % (2993325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.95/6.38 % (2993325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.95/6.38 % (2993325)CaDiCaL version: 2.1.3
% 36.95/6.38 % (2993325)Termination reason: Instruction limit
% 36.95/6.38 % (2993325)Termination phase: Finite model building SAT solving
% 36.95/6.38 % (2993325)Time elapsed: 0.568 s
% 36.95/6.38 % (2993325)Peak memory usage: 33 MB
% 36.95/6.38 % (2993325)Instructions burned: 715 (million)
% 36.95/6.38 % (2993349)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2239142945:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 36.95/6.38 % (2993332)Instruction limit reached!
% 36.95/6.38 % (2993332)------------------------------
% 36.95/6.38 % (2993332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.95/6.38 % (2993332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.95/6.38 % (2993332)CaDiCaL version: 2.1.3
% 36.95/6.38 % (2993332)Termination reason: Instruction limit
% 36.95/6.38 % (2993332)Termination phase: Saturation
% 36.95/6.38 % (2993332)Time elapsed: 0.586 s
% 36.95/6.38 % (2993332)Peak memory usage: 18 MB
% 36.95/6.38 % (2993332)Instructions burned: 684 (million)
% 36.95/6.38 % TRYING [7]
% 36.95/6.38 % (2993354)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=4292009480:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 36.95/6.38 % TRYING [14]
% 36.95/6.38 % (2993341)Instruction limit reached!
% 36.95/6.38 % (2993341)------------------------------
% 36.95/6.38 % (2993341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.95/6.38 % (2993341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.95/6.38 % (2993341)CaDiCaL version: 2.1.3
% 36.95/6.38 % (2993341)Termination reason: Instruction limit
% 36.95/6.38 % (2993341)Termination phase: Finite model building constraint generation
% 36.95/6.38 % (2993341)Time elapsed: 0.519 s
% 36.95/6.38 % (2993341)Peak memory usage: 25 MB
% 36.95/6.38 % (2993341)Instructions burned: 866 (million)
% 66.93/10.01 % (2993357)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1225552305:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 66.93/10.01 % (2993345)Instruction limit reached!
% 66.93/10.01 % (2993345)------------------------------
% 66.93/10.01 % (2993345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993345)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993345)Termination reason: Instruction limit
% 66.93/10.01 % (2993345)Termination phase: Saturation
% 66.93/10.01 % (2993345)Time elapsed: 0.567 s
% 66.93/10.01 % (2993345)Peak memory usage: 24 MB
% 66.93/10.01 % (2993345)Instructions burned: 1180 (million)
% 66.93/10.01 % (2993363)fmb+10_1_sil=64000:random_seed=3720569298:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 66.93/10.01 % Detected minimum model sizes of [4]
% 66.93/10.01 % Detected maximum model sizes of [max]
% 66.93/10.01 % TRYING [4]
% 66.93/10.01 % TRYING [5]
% 66.93/10.01 % TRYING [6]
% 66.93/10.01 % (2993349)Instruction limit reached!
% 66.93/10.01 % (2993349)------------------------------
% 66.93/10.01 % (2993349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993349)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993349)Termination reason: Instruction limit
% 66.93/10.01 % (2993349)Termination phase: Finite model building constraint generation
% 66.93/10.01 % (2993349)Time elapsed: 0.620 s
% 66.93/10.01 % (2993349)Peak memory usage: 73 MB
% 66.93/10.01 % (2993349)Instructions burned: 889 (million)
% 66.93/10.01 % TRYING [7]
% 66.93/10.01 % (2993354)Instruction limit reached!
% 66.93/10.01 % (2993354)------------------------------
% 66.93/10.01 % (2993354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993354)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993354)Termination reason: Instruction limit
% 66.93/10.01 % (2993354)Termination phase: Saturation
% 66.93/10.01 % (2993354)Time elapsed: 0.509 s
% 66.93/10.01 % (2993354)Peak memory usage: 15 MB
% 66.93/10.01 % (2993354)Instructions burned: 693 (million)
% 66.93/10.01 % (2993368)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3177836363:i=9515:nm=5_2986 on theBenchmark for (2986ds/9515Mi)
% 66.93/10.01 % Detected minimum model sizes of [4]
% 66.93/10.01 % Detected maximum model sizes of [max]
% 66.93/10.01 % TRYING [20]
% 66.93/10.01 % (2993369)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=32185769:fmbsr=1.7:i=920_2986 on theBenchmark for (2986ds/920Mi)
% 66.93/10.01 % Detected minimum model sizes of [4]
% 66.93/10.01 % Detected maximum model sizes of [max]
% 66.93/10.01 % TRYING [8]
% 66.93/10.01 % TRYING [9]
% 66.93/10.01 % TRYING [8]
% 66.93/10.01 % (2993357)Instruction limit reached!
% 66.93/10.01 % (2993357)------------------------------
% 66.93/10.01 % (2993357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993357)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993357)Termination reason: Instruction limit
% 66.93/10.01 % (2993357)Termination phase: Saturation
% 66.93/10.01 % (2993357)Time elapsed: 0.758 s
% 66.93/10.01 % (2993357)Peak memory usage: 18 MB
% 66.93/10.01 % (2993357)Instructions burned: 880 (million)
% 66.93/10.01 % (2993374)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=947288756:i=5131_2982 on theBenchmark for (2982ds/5131Mi)
% 66.93/10.01 % (2993369)Instruction limit reached!
% 66.93/10.01 % (2993369)------------------------------
% 66.93/10.01 % (2993369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993369)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993369)Termination reason: Instruction limit
% 66.93/10.01 % (2993369)Termination phase: Finite model building SAT solving
% 66.93/10.01 % (2993369)Time elapsed: 0.655 s
% 66.93/10.01 % (2993369)Peak memory usage: 53 MB
% 66.93/10.01 % (2993369)Instructions burned: 920 (million)
% 66.93/10.01 % TRYING [9]
% 66.93/10.01 % (2993383)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3633952345:i=1472:ins=7:fdi=8:gsp=on_2979 on theBenchmark for (2979ds/1472Mi)
% 66.93/10.01 % (2993383)Instruction limit reached!
% 66.93/10.01 % (2993383)------------------------------
% 66.93/10.01 % (2993383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993383)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993383)Termination reason: Instruction limit
% 66.93/10.01 % (2993383)Termination phase: Saturation
% 66.93/10.01 % (2993383)Time elapsed: 0.654 s
% 66.93/10.01 % (2993383)Peak memory usage: 25 MB
% 66.93/10.01 % (2993383)Instructions burned: 1473 (million)
% 66.93/10.01 % (2993531)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=214672643:i=6324_2972 on theBenchmark for (2972ds/6324Mi)
% 66.93/10.01 % Detected minimum model sizes of [4]
% 66.93/10.01 % Detected maximum model sizes of [max]
% 66.93/10.01 % TRYING [77]
% 66.93/10.01 % TRYING [10]
% 66.93/10.01 % (2993374)Instruction limit reached!
% 66.93/10.01 % (2993374)------------------------------
% 66.93/10.01 % (2993374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993374)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993374)Termination reason: Instruction limit
% 66.93/10.01 % (2993374)Termination phase: Saturation
% 66.93/10.01 % (2993374)Time elapsed: 2.813 s
% 66.93/10.01 % (2993374)Peak memory usage: 20 MB
% 66.93/10.01 % (2993374)Instructions burned: 5132 (million)
% 66.93/10.01 % (2993533)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2583708965:fmbsr=2.30978:i=2174_2954 on theBenchmark for (2954ds/2174Mi)
% 66.93/10.01 % Detected minimum model sizes of [4]
% 66.93/10.01 % Detected maximum model sizes of [max]
% 66.93/10.01 % TRYING [16]
% 66.93/10.01 % TRYING [10]
% 66.93/10.01 % (2993531)Instruction limit reached!
% 66.93/10.01 % (2993531)------------------------------
% 66.93/10.01 % (2993531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993531)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993531)Termination reason: Instruction limit
% 66.93/10.01 % (2993531)Termination phase: Finite model building constraint generation
% 66.93/10.01 % (2993531)Time elapsed: 2.225 s
% 66.93/10.01 % (2993531)Peak memory usage: 445 MB
% 66.93/10.01 % (2993531)Instructions burned: 6326 (million)
% 66.93/10.01 % (2993535)ott-2_1_sil=16000:newcnf=on:random_seed=2444757305:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2949 on theBenchmark for (2949ds/869Mi)
% 66.93/10.01 % (2993533)Instruction limit reached!
% 66.93/10.01 % (2993533)------------------------------
% 66.93/10.01 % (2993533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993533)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993533)Termination reason: Instruction limit
% 66.93/10.01 % (2993533)Termination phase: Finite model building constraint generation
% 66.93/10.01 % (2993533)Time elapsed: 0.772 s
% 66.93/10.01 % (2993533)Peak memory usage: 161 MB
% 66.93/10.01 % (2993533)Instructions burned: 2175 (million)
% 66.93/10.01 % (2993537)ott+10_1_sil=32000:tgt=ground:random_seed=1659846004:i=5114:av=off_2946 on theBenchmark for (2946ds/5114Mi)
% 66.93/10.01 % (2993535)Instruction limit reached!
% 66.93/10.01 % (2993535)------------------------------
% 66.93/10.01 % (2993535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993535)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993535)Termination reason: Instruction limit
% 66.93/10.01 % (2993535)Termination phase: Saturation
% 66.93/10.01 % (2993535)Time elapsed: 0.511 s
% 66.93/10.01 % (2993535)Peak memory usage: 16 MB
% 66.93/10.01 % (2993535)Instructions burned: 870 (million)
% 66.93/10.01 % (2993539)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=757956339:i=54282_2944 on theBenchmark for (2944ds/54282Mi)
% 66.93/10.01 % Detected minimum model sizes of [4]
% 66.93/10.01 % Detected maximum model sizes of [max]
% 66.93/10.01 % TRYING [4]
% 66.93/10.01 % TRYING [5]
% 66.93/10.01 % TRYING [6]
% 66.93/10.01 % TRYING [7]
% 66.93/10.01 % (2993368)Instruction limit reached!
% 66.93/10.01 % (2993368)------------------------------
% 66.93/10.01 % (2993368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993368)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993368)Termination reason: Instruction limit
% 66.93/10.01 % (2993368)Termination phase: Finite model building constraint generation
% 66.93/10.01 % (2993368)Time elapsed: 4.457 s
% 66.93/10.01 % (2993368)Peak memory usage: 863 MB
% 66.93/10.01 % (2993368)Instructions burned: 9515 (million)
% 66.93/10.01 % TRYING [8]
% 66.93/10.01 % (2993541)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=463359769:i=3512:aac=none_2940 on theBenchmark for (2940ds/3512Mi)
% 66.93/10.01 % TRYING [9]
% 66.93/10.01 % (2993363)Instruction limit reached!
% 66.93/10.01 % (2993363)------------------------------
% 66.93/10.01 % (2993363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993363)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993363)Termination reason: Instruction limit
% 66.93/10.01 % (2993363)Termination phase: Finite model building SAT solving
% 66.93/10.01 % (2993363)Time elapsed: 6.185 s
% 66.93/10.01 % (2993363)Peak memory usage: 88 MB
% 66.93/10.01 % (2993363)Instructions burned: 22064 (million)
% 66.93/10.01 % (2993543)dis+21_1_sil=32000:sas=cadical:random_seed=3967429805:i=3773:amm=off_2926 on theBenchmark for (2926ds/3773Mi)
% 66.93/10.01 % (2993541)Instruction limit reached!
% 66.93/10.01 % (2993541)------------------------------
% 66.93/10.01 % (2993541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993541)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993541)Termination reason: Instruction limit
% 66.93/10.01 % (2993541)Termination phase: Saturation
% 66.93/10.01 % (2993541)Time elapsed: 1.999 s
% 66.93/10.01 % (2993541)Peak memory usage: 19 MB
% 66.93/10.01 % (2993541)Instructions burned: 3513 (million)
% 66.93/10.01 % (2993545)ott+11_1_sil=16000:gs=on:random_seed=1553727207:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2920 on theBenchmark for (2920ds/2251Mi)
% 66.93/10.01 % (2993537)Instruction limit reached!
% 66.93/10.01 % (2993537)------------------------------
% 66.93/10.01 % (2993537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993537)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993537)Termination reason: Instruction limit
% 66.93/10.01 % (2993537)Termination phase: Saturation
% 66.93/10.01 % (2993537)Time elapsed: 3.113 s
% 66.93/10.01 % (2993537)Peak memory usage: 36 MB
% 66.93/10.01 % (2993537)Instructions burned: 5114 (million)
% 66.93/10.01 % (2993547)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3456993708:fmbsr=1.6:i=67534_2914 on theBenchmark for (2914ds/67534Mi)
% 66.93/10.01 % (2993543)Instruction limit reached!
% 66.93/10.01 % (2993543)------------------------------
% 66.93/10.01 % (2993543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993543)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993543)Termination reason: Instruction limit
% 66.93/10.01 % (2993543)Termination phase: Saturation
% 66.93/10.01 % (2993543)Time elapsed: 1.233 s
% 66.93/10.01 % (2993543)Peak memory usage: 27 MB
% 66.93/10.01 % (2993543)Instructions burned: 3773 (million)
% 66.93/10.01 % Detected minimum model sizes of [4]
% 66.93/10.01 % Detected maximum model sizes of [max]
% 66.93/10.01 % TRYING [7]
% 66.93/10.01 % (2993549)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=311365319:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2914 on theBenchmark for (2914ds/4591Mi)
% 66.93/10.01 % TRYING [8]
% 66.93/10.01 % (2993549)Instruction limit reached!
% 66.93/10.01 % (2993549)------------------------------
% 66.93/10.01 % (2993549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.01 % (2993549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.01 % (2993549)CaDiCaL version: 2.1.3
% 66.93/10.01 % (2993549)Termination reason: Instruction limit
% 66.93/10.01 % (2993549)Termination phase: Saturation
% 66.93/10.01 % (2993549)Time elapsed: 0.759 s
% 66.93/10.01 % (2993549)Peak memory usage: 12 MB
% 66.93/10.01 % (2993549)Instructions burned: 4594 (million)
% 66.93/10.01 % (2993551)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1133020237:i=29340_2906 on theBenchmark for (2906ds/29340Mi)
% 66.93/10.01 % TRYING [9]
% 66.93/10.01 % (2993551) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2993305-2993551"...
% 66.93/10.01 % (2993551)...printing done.
% 66.93/10.01 % (2993551)Refutation found. Thanks to Tanya!
% 66.93/10.01 % SZS status Theorem for theBenchmark
% 66.93/10.01 % SZS output start Proof for theBenchmark
% See solution above
% 66.93/10.02 % (2993551)------------------------------
% 66.93/10.02 % (2993551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.93/10.02 % (2993551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.93/10.02 % (2993551)CaDiCaL version: 2.1.3
% 66.93/10.02 % (2993551)Termination reason: Refutation
% 66.93/10.02 % (2993551)Time elapsed: 0.221 s
% 66.93/10.02 % (2993551)Peak memory usage: 18 MB
% 66.93/10.02 % (2993551)Instructions burned: 761 (million)
% 66.93/10.02 % (2993305)Success in time 9.574 s
% 66.93/10.02 % Vampire exiting
%------------------------------------------------------------------------------