%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRO016+1 : 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 : n020.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:40 PM UTC 2026
% Result : Theorem 33.12s 10.92s
% Output : Refutation 33.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 18
% Syntax : Number of formulae : 161 ( 25 unt; 3 def)
% Number of atoms : 610 ( 14 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 699 ( 250 ~; 288 |; 136 &)
% ( 10 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 3 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-3 aty)
% Number of variables : 250 ( 0 sgn 205 !; 45 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_02) ).
fof(f5,axiom,
! [X0,X1] :
( earlier(X0,X1)
=> ~ earlier(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_04) ).
fof(f8,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_07) ).
fof(f9,axiom,
! [X0] :
( legal(X0)
=> arboreal(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_08) ).
fof(f11,axiom,
! [X0,X1] :
( precedes(X0,X1)
<=> ( earlier(X0,X1)
& legal(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_10) ).
fof(f16,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> precedes(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_15) ).
fof(f17,axiom,
! [X0,X1] :
( root(X0,X1)
=> legal(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_16) ).
fof(f22,axiom,
! [X0,X1] :
( leaf(X0,X1)
<=> ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ~ ? [X3] : min_precedes(X0,X3,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_21) ).
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/sandbox/benchmark/theBenchmark.p',sos_22) ).
fof(f29,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& arboreal(X2)
& arboreal(X3)
& subactivity_occurrence(X2,X1)
& subactivity_occurrence(X3,X1) )
=> ( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_28) ).
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/sandbox/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/sandbox/benchmark/theBenchmark.p',sos_34) ).
fof(f36,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,tptp1)
| occurrence_of(X4,tptp2) )
& next_subocc(X3,X4,tptp0)
& leaf_occ(X4,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_35) ).
fof(f39,axiom,
atomic(tptp4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_38) ).
fof(f49,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(f50,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)],[f49]) ).
fof(f53,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f3]) ).
fof(f54,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f53]) ).
fof(f56,plain,
! [X0,X1] :
( ~ earlier(X1,X0)
| ~ earlier(X0,X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f61,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f62,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f69,plain,
! [X0,X1,X2] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f16]) ).
fof(f70,plain,
! [X0,X1] :
( legal(X0)
| ~ root(X0,X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f78,plain,
! [X0,X1] :
( leaf(X0,X1)
<=> ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) ) ),
inference(ennf_transformation,[],[f22]) ).
fof(f79,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(f86,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| ~ subactivity_occurrence(X3,X1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f87,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| ~ subactivity_occurrence(X3,X1) ),
inference(flattening,[],[f86]) ).
fof(f88,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(f89,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ min_precedes(X0,X1,X2)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(flattening,[],[f88]) ).
fof(f96,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,tptp1)
| occurrence_of(X4,tptp2) )
& next_subocc(X3,X4,tptp0)
& leaf_occ(X4,X1) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f36]) ).
fof(f97,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,tptp1)
| occurrence_of(X4,tptp2) )
& next_subocc(X3,X4,tptp0)
& leaf_occ(X4,X1) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(flattening,[],[f96]) ).
fof(f98,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,[],[f50]) ).
fof(f99,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,[],[f98]) ).
fof(f100,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(f101,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,[],[f99,f100]) ).
fof(f103,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f61]) ).
fof(f104,plain,
! [X0,X1] :
( ( precedes(X0,X1)
| ~ earlier(X0,X1)
| ~ legal(X1) )
& ( ( earlier(X0,X1)
& legal(X1) )
| ~ precedes(X0,X1) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f105,plain,
! [X0,X1] :
( ( precedes(X0,X1)
| ~ earlier(X0,X1)
| ~ legal(X1) )
& ( ( earlier(X0,X1)
& legal(X1) )
| ~ precedes(X0,X1) ) ),
inference(flattening,[],[f104]) ).
fof(f109,plain,
! [X0,X1] :
( ( leaf(X0,X1)
| ( ~ root(X0,X1)
& ! [X2] : ~ min_precedes(X2,X0,X1) )
| ? [X3] : min_precedes(X0,X3,X1) )
& ( ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) )
| ~ leaf(X0,X1) ) ),
inference(nnf_transformation,[],[f78]) ).
fof(f110,plain,
! [X0,X1] :
( ( leaf(X0,X1)
| ( ~ root(X0,X1)
& ! [X2] : ~ min_precedes(X2,X0,X1) )
| ? [X3] : min_precedes(X0,X3,X1) )
& ( ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) )
| ~ leaf(X0,X1) ) ),
inference(flattening,[],[f109]) ).
fof(f111,plain,
! [X0,X1] :
( ( leaf(X0,X1)
| ( ~ root(X0,X1)
& ! [X2] : ~ min_precedes(X2,X0,X1) )
| ? [X3] : min_precedes(X0,X3,X1) )
& ( ( ( root(X0,X1)
| ? [X4] : min_precedes(X4,X0,X1) )
& ! [X5] : ~ min_precedes(X0,X5,X1) )
| ~ leaf(X0,X1) ) ),
inference(rectify,[],[f110]) ).
fof(f112,plain,
! [X0,X1] :
( ( leaf(X0,X1)
| ( ~ root(X0,X1)
& ! [X2] : ~ min_precedes(X2,X0,X1) )
| min_precedes(X0,sK6(X0,X1),X1) )
& ( ( ( root(X0,X1)
| min_precedes(sK7(X0,X1),X0,X1) )
& ! [X5] : ~ min_precedes(X0,X5,X1) )
| ~ leaf(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X3,sK6(X0,X1)),skolemize(X4,sK7(X0,X1))],[f111]) ).
fof(f113,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,[],[f79]) ).
fof(f114,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,[],[f113]) ).
fof(f115,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,[],[f114]) ).
fof(f116,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ( min_precedes(X0,sK8(X0,X1,X2),X2)
& min_precedes(sK8(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,[sK8]),skolemize(X3,sK8(X0,X1,X2))],[f115]) ).
fof(f124,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(f125,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,[],[f124]) ).
fof(f126,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ( occurrence_of(X1,sK14(X0,X1))
& subactivity_occurrence(X0,X1)
& leaf(X0,sK14(X0,X1)) )
| ~ leaf_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X3,sK14(X0,X1))],[f125]) ).
fof(f127,plain,
! [X0,X1] :
( ( occurrence_of(sK15(X0,X1),tptp3)
& next_subocc(X0,sK15(X0,X1),tptp0)
& occurrence_of(sK16(X0,X1),tptp4)
& next_subocc(sK15(X0,X1),sK16(X0,X1),tptp0)
& ( occurrence_of(sK17(X0,X1),tptp1)
| occurrence_of(sK17(X0,X1),tptp2) )
& next_subocc(sK16(X0,X1),sK17(X0,X1),tptp0)
& leaf_occ(sK17(X0,X1),X1) )
| ~ 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,X1)),skolemize(X3,sK16(X0,X1)),skolemize(X4,sK17(X0,X1))],[f97]) ).
fof(f131,plain,
( ! [X2,X3] :
( ~ occurrence_of(X2,tptp3)
| ~ next_subocc(sK19,X2,tptp0)
| ( ~ occurrence_of(X3,tptp1)
& ~ occurrence_of(X3,tptp2) )
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf_occ(X3,sK20)
| ( occurrence_of(sK21(X2),tptp2)
& min_precedes(X2,sK21(X2),tptp0)
& occurrence_of(X3,tptp1) )
| sP0(X2,X3) )
& occurrence_of(sK20,tptp0)
& subactivity_occurrence(sK19,sK20)
& arboreal(sK19)
& ~ leaf_occ(sK19,sK20) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19,sK20,sK21]),skolemize(X0,sK19),skolemize(X1,sK20),skolemize(X4,sK21(X2))],[f101]) ).
fof(f136,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f54]) ).
fof(f138,plain,
! [X0,X1] :
( ~ earlier(X1,X0)
| ~ earlier(X0,X1) ),
inference(cnf_transformation,[],[f56]) ).
fof(f142,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f143,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(cnf_transformation,[],[f62]) ).
fof(f145,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| legal(X1) ),
inference(cnf_transformation,[],[f105]) ).
fof(f146,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| earlier(X0,X1) ),
inference(cnf_transformation,[],[f105]) ).
fof(f157,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(cnf_transformation,[],[f69]) ).
fof(f158,plain,
! [X0,X1] :
( ~ root(X0,X1)
| legal(X0) ),
inference(cnf_transformation,[],[f70]) ).
fof(f163,plain,
! [X0,X1,X5] :
( ~ min_precedes(X0,X5,X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f164,plain,
! [X0,X1] :
( ~ leaf(X0,X1)
| min_precedes(sK7(X0,X1),X0,X1)
| root(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f167,plain,
! [X2,X0,X1,X4] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) ),
inference(cnf_transformation,[],[f116]) ).
fof(f168,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f116]) ).
fof(f184,plain,
! [X2,X3,X0,X1] :
( ~ subactivity_occurrence(X3,X1)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| min_precedes(X2,X3,X0) ),
inference(cnf_transformation,[],[f87]) ).
fof(f185,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,[],[f89]) ).
fof(f190,plain,
! [X0,X1] :
( leaf(X0,sK14(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f126]) ).
fof(f191,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f126]) ).
fof(f192,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| occurrence_of(X1,sK14(X0,X1)) ),
inference(cnf_transformation,[],[f126]) ).
fof(f194,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| leaf_occ(sK17(X0,X1),X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
fof(f195,plain,
! [X0,X1] :
( next_subocc(sK16(X0,X1),sK17(X0,X1),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
fof(f197,plain,
! [X0,X1] :
( next_subocc(sK15(X0,X1),sK16(X0,X1),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
fof(f198,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK16(X0,X1),tptp4)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
fof(f199,plain,
! [X0,X1] :
( next_subocc(X0,sK15(X0,X1),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
fof(f203,plain,
atomic(tptp4),
inference(cnf_transformation,[],[f39]) ).
fof(f216,plain,
~ leaf_occ(sK19,sK20),
inference(cnf_transformation,[],[f131]) ).
fof(f217,plain,
arboreal(sK19),
inference(cnf_transformation,[],[f131]) ).
fof(f218,plain,
subactivity_occurrence(sK19,sK20),
inference(cnf_transformation,[],[f131]) ).
fof(f219,plain,
occurrence_of(sK20,tptp0),
inference(cnf_transformation,[],[f131]) ).
fof(f310,plain,
! [X0] :
( ~ occurrence_of(sK20,X0)
| tptp0 = X0 ),
inference(resolution,[],[f136,f219]) ).
fof(f4027,plain,
leaf_occ(sK17(sK19,sK20),sK20),
inference(unit_resulting_resolution,[],[f194,f217,f216,f218,f219]) ).
fof(f4049,plain,
occurrence_of(sK20,sK14(sK17(sK19,sK20),sK20)),
inference(unit_resulting_resolution,[],[f192,f4027]) ).
fof(f4051,plain,
subactivity_occurrence(sK17(sK19,sK20),sK20),
inference(unit_resulting_resolution,[],[f191,f4027]) ).
fof(f4069,plain,
tptp0 = sK14(sK17(sK19,sK20),sK20),
inference(unit_resulting_resolution,[],[f310,f4049]) ).
fof(f4110,plain,
( leaf(sK17(sK19,sK20),tptp0)
| ~ leaf_occ(sK17(sK19,sK20),sK20) ),
inference(superposition,[],[f190,f4069]) ).
fof(f4111,plain,
leaf(sK17(sK19,sK20),tptp0),
inference(forward_subsumption_resolution,[],[f4110,f4027]) ).
fof(f4113,plain,
! [X0] : ~ min_precedes(sK17(sK19,sK20),X0,tptp0),
inference(unit_resulting_resolution,[],[f163,f4111]) ).
fof(f4156,definition,
( spl22_11
<=> arboreal(sK17(sK19,sK20)) ),
introduced(definition,[new_symbols(definition,[spl22_11])],[avatar_definition]) ).
fof(f4157,plain,
( ~ arboreal(sK17(sK19,sK20))
| spl22_11 ),
inference(avatar_component_clause,[],[f4156]) ).
fof(f4158,plain,
( arboreal(sK17(sK19,sK20))
| ~ spl22_11 ),
inference(avatar_component_clause,[],[f4156]) ).
fof(f4202,plain,
( ~ legal(sK17(sK19,sK20))
| spl22_11 ),
inference(unit_resulting_resolution,[],[f143,f4157]) ).
fof(f4215,plain,
( ! [X0] : ~ root(sK17(sK19,sK20),X0)
| spl22_11 ),
inference(unit_resulting_resolution,[],[f158,f4202]) ).
fof(f4216,plain,
( ! [X0] : ~ precedes(X0,sK17(sK19,sK20))
| spl22_11 ),
inference(unit_resulting_resolution,[],[f145,f4202]) ).
fof(f4246,plain,
( ! [X0,X1] : ~ min_precedes(X0,sK17(sK19,sK20),X1)
| spl22_11 ),
inference(unit_resulting_resolution,[],[f157,f4216]) ).
fof(f4261,plain,
( root(sK17(sK19,sK20),tptp0)
| spl22_11 ),
inference(unit_resulting_resolution,[],[f164,f4111,f4246]) ).
fof(f4284,plain,
( $false
| spl22_11 ),
inference(forward_subsumption_resolution,[],[f4261,f4215]) ).
fof(f4285,plain,
spl22_11,
inference(avatar_contradiction_clause,[],[f4284]) ).
fof(f4309,plain,
occurrence_of(sK16(sK19,sK20),tptp4),
inference(unit_resulting_resolution,[],[f198,f217,f216,f218,f219]) ).
fof(f4342,plain,
arboreal(sK16(sK19,sK20)),
inference(unit_resulting_resolution,[],[f142,f203,f4309]) ).
fof(f5758,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0)
| ~ arboreal(X1)
| leaf_occ(X1,X0)
| min_precedes(X1,sK15(X1,X0),tptp0) ),
inference(resolution,[],[f199,f168]) ).
fof(f6152,plain,
next_subocc(sK16(sK19,sK20),sK17(sK19,sK20),tptp0),
inference(unit_resulting_resolution,[],[f195,f217,f216,f218,f219]) ).
fof(f6154,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0)
| ~ arboreal(X1)
| leaf_occ(X1,X0)
| min_precedes(sK16(X1,X0),sK17(X1,X0),tptp0) ),
inference(resolution,[],[f195,f168]) ).
fof(f6295,plain,
min_precedes(sK16(sK19,sK20),sK17(sK19,sK20),tptp0),
inference(unit_resulting_resolution,[],[f168,f6152]) ).
fof(f6297,plain,
! [X0] :
( ~ min_precedes(sK16(sK19,sK20),X0,tptp0)
| ~ min_precedes(X0,sK17(sK19,sK20),tptp0) ),
inference(resolution,[],[f6152,f167]) ).
fof(f6392,plain,
~ leaf(sK16(sK19,sK20),tptp0),
inference(unit_resulting_resolution,[],[f163,f6295]) ).
fof(f6399,plain,
subactivity_occurrence(sK16(sK19,sK20),sK20),
inference(unit_resulting_resolution,[],[f185,f219,f4051,f6295]) ).
fof(f23808,definition,
( spl22_21
<=> leaf_occ(sK16(sK19,sK20),sK20) ),
introduced(definition,[new_symbols(definition,[spl22_21])],[avatar_definition]) ).
fof(f23809,plain,
( ~ leaf_occ(sK16(sK19,sK20),sK20)
| spl22_21 ),
inference(avatar_component_clause,[],[f23808]) ).
fof(f23810,plain,
( leaf_occ(sK16(sK19,sK20),sK20)
| ~ spl22_21 ),
inference(avatar_component_clause,[],[f23808]) ).
fof(f23818,plain,
( occurrence_of(sK20,sK14(sK16(sK19,sK20),sK20))
| ~ spl22_21 ),
inference(unit_resulting_resolution,[],[f192,f23810]) ).
fof(f23823,plain,
( tptp0 = sK14(sK16(sK19,sK20),sK20)
| ~ spl22_21 ),
inference(unit_resulting_resolution,[],[f310,f23818]) ).
fof(f23955,plain,
( leaf(sK16(sK19,sK20),tptp0)
| ~ leaf_occ(sK16(sK19,sK20),sK20)
| ~ spl22_21 ),
inference(superposition,[],[f190,f23823]) ).
fof(f23956,plain,
( ~ leaf_occ(sK16(sK19,sK20),sK20)
| ~ spl22_21 ),
inference(forward_subsumption_resolution,[],[f23955,f6392]) ).
fof(f23958,plain,
( $false
| ~ spl22_21 ),
inference(forward_subsumption_resolution,[],[f23956,f23810]) ).
fof(f23959,plain,
~ spl22_21,
inference(avatar_contradiction_clause,[],[f23958]) ).
fof(f23967,plain,
( leaf_occ(sK17(sK16(sK19,sK20),sK20),sK20)
| spl22_21 ),
inference(unit_resulting_resolution,[],[f194,f219,f4342,f6399,f23809]) ).
fof(f23970,plain,
( occurrence_of(sK16(sK16(sK19,sK20),sK20),tptp4)
| spl22_21 ),
inference(unit_resulting_resolution,[],[f198,f219,f4342,f6399,f23809]) ).
fof(f23973,plain,
( min_precedes(sK16(sK19,sK20),sK15(sK16(sK19,sK20),sK20),tptp0)
| spl22_21 ),
inference(unit_resulting_resolution,[],[f5758,f219,f4342,f6399,f23809]) ).
fof(f24060,plain,
( occurrence_of(sK20,sK14(sK17(sK16(sK19,sK20),sK20),sK20))
| spl22_21 ),
inference(unit_resulting_resolution,[],[f192,f23967]) ).
fof(f24062,plain,
( subactivity_occurrence(sK17(sK16(sK19,sK20),sK20),sK20)
| spl22_21 ),
inference(unit_resulting_resolution,[],[f191,f23967]) ).
fof(f24078,plain,
( arboreal(sK16(sK16(sK19,sK20),sK20))
| spl22_21 ),
inference(unit_resulting_resolution,[],[f142,f203,f23970]) ).
fof(f24250,plain,
( tptp0 = sK14(sK17(sK16(sK19,sK20),sK20),sK20)
| spl22_21 ),
inference(unit_resulting_resolution,[],[f310,f24060]) ).
fof(f24391,plain,
( leaf(sK17(sK16(sK19,sK20),sK20),tptp0)
| ~ leaf_occ(sK17(sK16(sK19,sK20),sK20),sK20)
| spl22_21 ),
inference(superposition,[],[f190,f24250]) ).
fof(f24392,plain,
( leaf(sK17(sK16(sK19,sK20),sK20),tptp0)
| spl22_21 ),
inference(forward_subsumption_resolution,[],[f24391,f23967]) ).
fof(f24395,plain,
( ! [X0] : ~ min_precedes(sK17(sK16(sK19,sK20),sK20),X0,tptp0)
| spl22_21 ),
inference(unit_resulting_resolution,[],[f163,f24392]) ).
fof(f24476,plain,
( ~ occurrence_of(sK20,tptp0)
| ~ arboreal(sK16(sK19,sK20))
| leaf_occ(sK16(sK19,sK20),sK20)
| min_precedes(sK16(sK16(sK19,sK20),sK20),sK17(sK16(sK19,sK20),sK20),tptp0) ),
inference(resolution,[],[f6154,f6399]) ).
fof(f24493,plain,
( ~ arboreal(sK16(sK19,sK20))
| leaf_occ(sK16(sK19,sK20),sK20)
| min_precedes(sK16(sK16(sK19,sK20),sK20),sK17(sK16(sK19,sK20),sK20),tptp0) ),
inference(forward_subsumption_resolution,[],[f24476,f219]) ).
fof(f24516,plain,
( leaf_occ(sK16(sK19,sK20),sK20)
| min_precedes(sK16(sK16(sK19,sK20),sK20),sK17(sK16(sK19,sK20),sK20),tptp0) ),
inference(forward_subsumption_resolution,[],[f24493,f4342]) ).
fof(f24532,plain,
( min_precedes(sK16(sK16(sK19,sK20),sK20),sK17(sK16(sK19,sK20),sK20),tptp0)
| spl22_21 ),
inference(forward_subsumption_resolution,[],[f24516,f23809]) ).
fof(f24584,plain,
( precedes(sK16(sK19,sK20),sK15(sK16(sK19,sK20),sK20))
| spl22_21 ),
inference(unit_resulting_resolution,[],[f157,f23973]) ).
fof(f24706,plain,
( earlier(sK16(sK19,sK20),sK15(sK16(sK19,sK20),sK20))
| spl22_21 ),
inference(unit_resulting_resolution,[],[f146,f24584]) ).
fof(f24844,plain,
( ~ earlier(sK15(sK16(sK19,sK20),sK20),sK16(sK19,sK20))
| spl22_21 ),
inference(unit_resulting_resolution,[],[f138,f24706]) ).
fof(f25106,plain,
( ~ precedes(sK15(sK16(sK19,sK20),sK20),sK16(sK19,sK20))
| spl22_21 ),
inference(unit_resulting_resolution,[],[f146,f24844]) ).
fof(f25161,plain,
( ! [X0] : ~ min_precedes(sK15(sK16(sK19,sK20),sK20),sK16(sK19,sK20),X0)
| spl22_21 ),
inference(unit_resulting_resolution,[],[f157,f25106]) ).
fof(f25924,plain,
( ! [X0] : ~ next_subocc(sK15(sK16(sK19,sK20),sK20),sK16(sK19,sK20),X0)
| spl22_21 ),
inference(unit_resulting_resolution,[],[f168,f25161]) ).
fof(f27424,plain,
( precedes(sK16(sK16(sK19,sK20),sK20),sK17(sK16(sK19,sK20),sK20))
| spl22_21 ),
inference(unit_resulting_resolution,[],[f157,f24532]) ).
fof(f27433,plain,
( subactivity_occurrence(sK16(sK16(sK19,sK20),sK20),sK20)
| spl22_21 ),
inference(unit_resulting_resolution,[],[f185,f219,f24062,f24532]) ).
fof(f27661,plain,
( legal(sK17(sK16(sK19,sK20),sK20))
| spl22_21 ),
inference(unit_resulting_resolution,[],[f145,f27424]) ).
fof(f27664,plain,
( arboreal(sK17(sK16(sK19,sK20),sK20))
| spl22_21 ),
inference(unit_resulting_resolution,[],[f143,f27661]) ).
fof(f27713,plain,
( sK17(sK19,sK20) = sK17(sK16(sK19,sK20),sK20)
| ~ spl22_11
| spl22_21 ),
inference(unit_resulting_resolution,[],[f184,f219,f4158,f4051,f24062,f4113,f24395,f27664]) ).
fof(f27814,plain,
( min_precedes(sK16(sK16(sK19,sK20),sK20),sK17(sK19,sK20),tptp0)
| ~ spl22_11
| spl22_21 ),
inference(superposition,[],[f24532,f27713]) ).
fof(f27835,plain,
( next_subocc(sK16(sK16(sK19,sK20),sK20),sK17(sK19,sK20),tptp0)
| ~ occurrence_of(sK20,tptp0)
| ~ subactivity_occurrence(sK16(sK19,sK20),sK20)
| ~ arboreal(sK16(sK19,sK20))
| leaf_occ(sK16(sK19,sK20),sK20)
| ~ spl22_11
| spl22_21 ),
inference(superposition,[],[f195,f27713]) ).
fof(f27836,plain,
( next_subocc(sK16(sK16(sK19,sK20),sK20),sK17(sK19,sK20),tptp0)
| ~ subactivity_occurrence(sK16(sK19,sK20),sK20)
| ~ arboreal(sK16(sK19,sK20))
| leaf_occ(sK16(sK19,sK20),sK20)
| ~ spl22_11
| spl22_21 ),
inference(forward_subsumption_resolution,[],[f27835,f219]) ).
fof(f27837,plain,
( next_subocc(sK16(sK16(sK19,sK20),sK20),sK17(sK19,sK20),tptp0)
| ~ arboreal(sK16(sK19,sK20))
| leaf_occ(sK16(sK19,sK20),sK20)
| ~ spl22_11
| spl22_21 ),
inference(forward_subsumption_resolution,[],[f27836,f6399]) ).
fof(f27838,plain,
( next_subocc(sK16(sK16(sK19,sK20),sK20),sK17(sK19,sK20),tptp0)
| leaf_occ(sK16(sK19,sK20),sK20)
| ~ spl22_11
| spl22_21 ),
inference(forward_subsumption_resolution,[],[f27837,f4342]) ).
fof(f27839,plain,
( next_subocc(sK16(sK16(sK19,sK20),sK20),sK17(sK19,sK20),tptp0)
| ~ spl22_11
| spl22_21 ),
inference(forward_subsumption_resolution,[],[f27838,f23809]) ).
fof(f28038,plain,
( ~ min_precedes(sK16(sK19,sK20),sK16(sK16(sK19,sK20),sK20),tptp0)
| ~ spl22_11
| spl22_21 ),
inference(unit_resulting_resolution,[],[f6297,f27814]) ).
fof(f28103,plain,
( ~ min_precedes(sK16(sK16(sK19,sK20),sK20),sK16(sK19,sK20),tptp0)
| ~ spl22_11
| spl22_21 ),
inference(unit_resulting_resolution,[],[f167,f6295,f27839]) ).
fof(f28211,plain,
( sK16(sK19,sK20) = sK16(sK16(sK19,sK20),sK20)
| ~ spl22_11
| spl22_21 ),
inference(unit_resulting_resolution,[],[f184,f219,f4342,f6399,f27433,f24078,f28038,f28103]) ).
fof(f28263,plain,
( next_subocc(sK15(sK16(sK19,sK20),sK20),sK16(sK19,sK20),tptp0)
| ~ occurrence_of(sK20,tptp0)
| ~ subactivity_occurrence(sK16(sK19,sK20),sK20)
| ~ arboreal(sK16(sK19,sK20))
| leaf_occ(sK16(sK19,sK20),sK20)
| ~ spl22_11
| spl22_21 ),
inference(superposition,[],[f197,f28211]) ).
fof(f28266,plain,
( ~ occurrence_of(sK20,tptp0)
| ~ subactivity_occurrence(sK16(sK19,sK20),sK20)
| ~ arboreal(sK16(sK19,sK20))
| leaf_occ(sK16(sK19,sK20),sK20)
| ~ spl22_11
| spl22_21 ),
inference(forward_subsumption_resolution,[],[f28263,f25924]) ).
fof(f28270,plain,
( ~ subactivity_occurrence(sK16(sK19,sK20),sK20)
| ~ arboreal(sK16(sK19,sK20))
| leaf_occ(sK16(sK19,sK20),sK20)
| ~ spl22_11
| spl22_21 ),
inference(forward_subsumption_resolution,[],[f28266,f219]) ).
fof(f28272,plain,
( ~ arboreal(sK16(sK19,sK20))
| leaf_occ(sK16(sK19,sK20),sK20)
| ~ spl22_11
| spl22_21 ),
inference(forward_subsumption_resolution,[],[f28270,f6399]) ).
fof(f28274,plain,
( leaf_occ(sK16(sK19,sK20),sK20)
| ~ spl22_11
| spl22_21 ),
inference(forward_subsumption_resolution,[],[f28272,f4342]) ).
fof(f28276,plain,
( $false
| ~ spl22_11
| spl22_21 ),
inference(forward_subsumption_resolution,[],[f28274,f23809]) ).
fof(f28277,plain,
( ~ spl22_11
| spl22_21 ),
inference(avatar_contradiction_clause,[],[f28276]) ).
cnf(s11,plain,
spl22_11,
inference(sat_conversion,[],[f4285]) ).
cnf(s36,plain,
~ spl22_21,
inference(sat_conversion,[],[f23959]) ).
cnf(s37,plain,
( ~ spl22_11
| spl22_21 ),
inference(sat_conversion,[],[f28277]) ).
cnf(s38,plain,
~ spl22_11,
inference(rat,[],[s37,s36]) ).
cnf(s45,plain,
$false,
inference(rat,[],[s11,s38]) ).
fof(f28278,plain,
$false,
inference(avatar_sat_refutation,[],[s45]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO016+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n020.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 22:23:35 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 Running first-order model finding
% 0.10/0.39 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
% 16.28/2.79 % (3825211)Will run a generic schedule for satisfiability detection.
% 16.28/2.79 % (3825219)dis+10_1_sil=32000:sp=arity:random_seed=1051689068:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.28/2.79 % (3825216)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3816514851_2999 on theBenchmark for (2999ds/0Mi)
% 16.28/2.79 % (3825217)% WARNING: option uhcvi not known.
% 16.28/2.79 % (3825218)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1379300897:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.28/2.79 % (3825220)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2099727562:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.28/2.79 % (3825221)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=815007861:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.28/2.79 % (3825222)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1985527869:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.28/2.79 % (3825217)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=347053807:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.28/2.79 % Detected minimum model sizes of [4]
% 16.28/2.79 % Detected maximum model sizes of [max]
% 16.28/2.79 % TRYING [4]
% 16.28/2.79 % TRYING [5]
% 16.28/2.79 % (3825219)Instruction limit reached!
% 16.28/2.79 % (3825219)------------------------------
% 16.28/2.79 % (3825219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/2.79 % (3825219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/2.79 % (3825219)CaDiCaL version: 2.1.3
% 16.28/2.79 % (3825219)Termination reason: Instruction limit
% 16.28/2.79 % (3825219)Termination phase: Saturation
% 16.28/2.79 % (3825219)Time elapsed: 0.039 s
% 16.28/2.79 % (3825219)Peak memory usage: 12 MB
% 16.28/2.79 % (3825219)Instructions burned: 106 (million)
% 16.28/2.79 % (3825230)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=30098787:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.28/2.79 % Detected minimum model sizes of [4]
% 16.28/2.79 % Detected maximum model sizes of [max]
% 16.28/2.79 % TRYING [4]
% 16.28/2.79 % TRYING [6]
% 16.28/2.79 % TRYING [5]
% 16.28/2.79 % (3825220)Instruction limit reached!
% 16.28/2.79 % (3825220)------------------------------
% 16.28/2.79 % (3825220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/2.79 % (3825220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/2.79 % (3825220)CaDiCaL version: 2.1.3
% 16.28/2.79 % (3825220)Termination reason: Instruction limit
% 16.28/2.79 % (3825220)Termination phase: Saturation
% 16.28/2.79 % (3825220)Time elapsed: 0.067 s
% 16.28/2.79 % (3825220)Peak memory usage: 12 MB
% 16.28/2.79 % (3825220)Instructions burned: 117 (million)
% 16.28/2.79 % TRYING [6]
% 16.28/2.79 % (3825232)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3635796720:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 16.28/2.79 % (3825221)Instruction limit reached!
% 16.28/2.79 % (3825221)------------------------------
% 16.28/2.79 % (3825221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/2.79 % (3825221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/2.79 % (3825221)CaDiCaL version: 2.1.3
% 16.28/2.79 % (3825221)Termination reason: Instruction limit
% 16.28/2.79 % (3825221)Termination phase: Saturation
% 16.28/2.79 % (3825221)Time elapsed: 0.088 s
% 16.28/2.79 % (3825221)Peak memory usage: 13 MB
% 16.28/2.79 % (3825221)Instructions burned: 132 (million)
% 16.28/2.79 % (3825234)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=4130959908:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.28/2.79 % (3825222)Instruction limit reached!
% 16.28/2.79 % (3825222)------------------------------
% 16.28/2.79 % (3825222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/2.79 % (3825222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/2.79 % (3825222)CaDiCaL version: 2.1.3
% 16.28/2.79 % (3825222)Termination reason: Instruction limit
% 16.28/2.79 % (3825222)Termination phase: Saturation
% 16.28/2.79 % (3825222)Time elapsed: 0.108 s
% 16.28/2.79 % (3825222)Peak memory usage: 13 MB
% 16.28/2.79 % (3825222)Instructions burned: 159 (million)
% 16.28/2.79 % TRYING [7]
% 16.28/2.79 % TRYING [7]
% 16.28/2.79 % (3825236)ott-21_1_sil=16000:fs=off:random_seed=2635511180:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.28/2.79 % (3825232)Instruction limit reached!
% 35.18/6.05 % (3825232)------------------------------
% 35.18/6.05 % (3825232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.18/6.05 % (3825232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.18/6.05 % (3825232)CaDiCaL version: 2.1.3
% 35.18/6.05 % (3825232)Termination reason: Instruction limit
% 35.18/6.05 % (3825232)Termination phase: Saturation
% 35.18/6.05 % (3825232)Time elapsed: 0.088 s
% 35.18/6.05 % (3825232)Peak memory usage: 13 MB
% 35.18/6.05 % (3825232)Instructions burned: 132 (million)
% 35.18/6.05 % (3825238)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=354325820:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 35.18/6.05 % (3825230)Instruction limit reached!
% 35.18/6.05 % (3825230)------------------------------
% 35.18/6.05 % (3825230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.18/6.05 % (3825230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.18/6.05 % (3825230)CaDiCaL version: 2.1.3
% 35.18/6.05 % (3825230)Termination reason: Instruction limit
% 35.18/6.05 % (3825230)Termination phase: Finite model building constraint generation
% 35.18/6.05 % (3825230)Time elapsed: 0.169 s
% 35.18/6.05 % (3825230)Peak memory usage: 31 MB
% 35.18/6.05 % (3825230)Instructions burned: 716 (million)
% 35.18/6.05 % (3825240)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=167997545:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 35.18/6.05 % (3825236)Instruction limit reached!
% 35.18/6.05 % (3825236)------------------------------
% 35.18/6.05 % (3825236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.18/6.05 % (3825236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.18/6.05 % (3825236)CaDiCaL version: 2.1.3
% 35.18/6.05 % (3825236)Termination reason: Instruction limit
% 35.18/6.05 % (3825236)Termination phase: Saturation
% 35.18/6.05 % (3825236)Time elapsed: 0.097 s
% 35.18/6.05 % (3825236)Peak memory usage: 12 MB
% 35.18/6.05 % (3825236)Instructions burned: 180 (million)
% 35.18/6.05 % Detected minimum model sizes of [4]
% 35.18/6.05 % Detected maximum model sizes of [max]
% 35.18/6.05 % TRYING [4]
% 35.18/6.05 % TRYING [5]
% 35.18/6.05 % (3825242)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2334295326:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 35.18/6.05 % TRYING [6]
% 35.18/6.05 % TRYING [8]
% 35.18/6.05 % TRYING [7]
% 35.18/6.05 % (3825240)Instruction limit reached!
% 35.18/6.05 % (3825240)------------------------------
% 35.18/6.05 % (3825240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.18/6.05 % (3825240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.18/6.05 % (3825240)CaDiCaL version: 2.1.3
% 35.18/6.05 % (3825240)Termination reason: Instruction limit
% 35.18/6.05 % (3825240)Termination phase: Finite model building SAT solving
% 35.18/6.05 % (3825240)Time elapsed: 0.179 s
% 35.18/6.05 % (3825240)Peak memory usage: 24 MB
% 35.18/6.05 % (3825240)Instructions burned: 870 (million)
% 35.18/6.05 % (3825244)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=67816649:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 35.18/6.05 % TRYING [14]
% 35.18/6.05 % (3825234)Instruction limit reached!
% 35.18/6.05 % (3825234)------------------------------
% 35.18/6.05 % (3825234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.18/6.05 % (3825234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.18/6.05 % (3825234)CaDiCaL version: 2.1.3
% 35.18/6.05 % (3825234)Termination reason: Instruction limit
% 35.18/6.05 % (3825234)Termination phase: Saturation
% 35.18/6.05 % (3825234)Time elapsed: 0.406 s
% 35.18/6.05 % (3825234)Peak memory usage: 19 MB
% 35.18/6.05 % (3825234)Instructions burned: 686 (million)
% 35.18/6.05 % (3825246)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=1261041853:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 35.18/6.05 % (3825238)Instruction limit reached!
% 35.18/6.05 % (3825238)------------------------------
% 35.18/6.05 % (3825238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.18/6.05 % (3825238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.18/6.05 % (3825238)CaDiCaL version: 2.1.3
% 35.18/6.05 % (3825238)Termination reason: Instruction limit
% 35.18/6.05 % (3825238)Termination phase: Saturation
% 35.18/6.05 % (3825238)Time elapsed: 0.349 s
% 35.18/6.05 % (3825238)Peak memory usage: 14 MB
% 35.18/6.05 % (3825238)Instructions burned: 478 (million)
% 65.21/9.61 % (3825248)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1737426099:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 65.21/9.61 % (3825244)Instruction limit reached!
% 65.21/9.61 % (3825244)------------------------------
% 65.21/9.61 % (3825244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.21/9.61 % (3825244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.21/9.61 % (3825244)CaDiCaL version: 2.1.3
% 65.21/9.61 % (3825244)Termination reason: Instruction limit
% 65.21/9.61 % (3825244)Termination phase: Finite model building constraint generation
% 65.21/9.61 % (3825244)Time elapsed: 0.176 s
% 65.21/9.61 % (3825244)Peak memory usage: 73 MB
% 65.21/9.61 % (3825244)Instructions burned: 890 (million)
% 65.21/9.61 % (3825250)fmb+10_1_sil=64000:random_seed=4207038785:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 65.21/9.61 % Detected minimum model sizes of [4]
% 65.21/9.61 % Detected maximum model sizes of [max]
% 65.21/9.61 % TRYING [4]
% 65.21/9.61 % TRYING [5]
% 65.21/9.61 % TRYING [6]
% 65.21/9.61 % TRYING [7]
% 65.21/9.61 % TRYING [9]
% 65.21/9.61 % TRYING [8]
% 65.21/9.61 % (3825246)Instruction limit reached!
% 65.21/9.61 % (3825246)------------------------------
% 65.21/9.61 % (3825246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.21/9.61 % (3825246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.21/9.61 % (3825246)CaDiCaL version: 2.1.3
% 65.21/9.61 % (3825246)Termination reason: Instruction limit
% 65.21/9.61 % (3825246)Termination phase: Saturation
% 65.21/9.61 % (3825246)Time elapsed: 0.356 s
% 65.21/9.61 % (3825246)Peak memory usage: 20 MB
% 65.21/9.61 % (3825246)Instructions burned: 694 (million)
% 65.21/9.61 % (3825252)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2161983216:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 65.21/9.61 % Detected minimum model sizes of [4]
% 65.21/9.61 % Detected maximum model sizes of [max]
% 65.21/9.61 % TRYING [20]
% 65.21/9.61 % (3825242)Instruction limit reached!
% 65.21/9.61 % (3825242)------------------------------
% 65.21/9.61 % (3825242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.21/9.61 % (3825242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.21/9.61 % (3825242)CaDiCaL version: 2.1.3
% 65.21/9.61 % (3825242)Termination reason: Instruction limit
% 65.21/9.61 % (3825242)Termination phase: Saturation
% 65.21/9.61 % (3825242)Time elapsed: 0.736 s
% 65.21/9.61 % (3825242)Peak memory usage: 25 MB
% 65.21/9.61 % (3825242)Instructions burned: 1179 (million)
% 65.21/9.61 % (3825254)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2080362443:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 65.21/9.61 % Detected minimum model sizes of [4]
% 65.21/9.61 % Detected maximum model sizes of [max]
% 65.21/9.61 % TRYING [8]
% 65.21/9.61 % (3825248)Instruction limit reached!
% 65.21/9.61 % (3825248)------------------------------
% 65.21/9.61 % (3825248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.21/9.61 % (3825248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.21/9.61 % (3825248)CaDiCaL version: 2.1.3
% 65.21/9.61 % (3825248)Termination reason: Instruction limit
% 65.21/9.61 % (3825248)Termination phase: Saturation
% 65.21/9.61 % (3825248)Time elapsed: 0.500 s
% 65.21/9.61 % (3825248)Peak memory usage: 18 MB
% 65.21/9.61 % (3825248)Instructions burned: 879 (million)
% 65.21/9.61 % (3825256)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3339004323:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 65.21/9.61 % TRYING [9]
% 65.21/9.61 % (3825254)Instruction limit reached!
% 65.21/9.61 % (3825254)------------------------------
% 65.21/9.61 % (3825254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.21/9.61 % (3825254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.21/9.61 % (3825254)CaDiCaL version: 2.1.3
% 65.21/9.61 % (3825254)Termination reason: Instruction limit
% 65.21/9.61 % (3825254)Termination phase: Finite model building SAT solving
% 65.21/9.61 % (3825254)Time elapsed: 0.490 s
% 65.21/9.61 % (3825254)Peak memory usage: 54 MB
% 65.21/9.61 % (3825254)Instructions burned: 920 (million)
% 65.21/9.61 % (3825258)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=548108737:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 65.21/9.61 % TRYING [10]
% 65.21/9.61 % (3825258)Instruction limit reached!
% 65.21/9.61 % (3825258)------------------------------
% 65.21/9.61 % (3825258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 65.21/9.61 % (3825258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/10.92 % (3825258)CaDiCaL version: 2.1.3
% 33.12/10.92 % (3825258)Termination reason: Instruction limit
% 33.12/10.92 % (3825258)Termination phase: Saturation
% 33.12/10.92 % (3825258)Time elapsed: 0.836 s
% 33.12/10.92 % (3825258)Peak memory usage: 28 MB
% 33.12/10.92 % (3825258)Instructions burned: 1472 (million)
% 33.12/10.92 % (3825260)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4049936201:i=6324_2976 on theBenchmark for (2976ds/6324Mi)
% 33.12/10.92 % Detected minimum model sizes of [4]
% 33.12/10.92 % Detected maximum model sizes of [max]
% 33.12/10.92 % TRYING [77]
% 33.12/10.92 % (3825256)Instruction limit reached!
% 33.12/10.92 % (3825256)------------------------------
% 33.12/10.92 % (3825256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/10.92 % (3825256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/10.92 % (3825256)CaDiCaL version: 2.1.3
% 33.12/10.92 % (3825256)Termination reason: Instruction limit
% 33.12/10.92 % (3825256)Termination phase: Saturation
% 33.12/10.92 % (3825256)Time elapsed: 2.578 s
% 33.12/10.92 % (3825256)Peak memory usage: 18 MB
% 33.12/10.92 % (3825256)Instructions burned: 5132 (million)
% 33.12/10.92 % (3825262)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3622261937:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi)
% 33.12/10.92 % Detected minimum model sizes of [4]
% 33.12/10.92 % Detected maximum model sizes of [max]
% 33.12/10.92 % TRYING [16]
% 33.12/10.92 % TRYING [10]
% 33.12/10.92 % TRYING [11]
% 33.12/10.92 % (3825260)Instruction limit reached!
% 33.12/10.92 % (3825260)------------------------------
% 33.12/10.92 % (3825260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/10.92 % (3825260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/10.92 % (3825260)CaDiCaL version: 2.1.3
% 33.12/10.92 % (3825260)Termination reason: Instruction limit
% 33.12/10.92 % (3825260)Termination phase: Finite model building constraint generation
% 33.12/10.92 % (3825260)Time elapsed: 2.106 s
% 33.12/10.92 % (3825260)Peak memory usage: 386 MB
% 33.12/10.92 % (3825260)Instructions burned: 6324 (million)
% 33.12/10.92 % (3825262)Instruction limit reached!
% 33.12/10.92 % (3825262)------------------------------
% 33.12/10.92 % (3825262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/10.92 % (3825262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/10.92 % (3825262)CaDiCaL version: 2.1.3
% 33.12/10.92 % (3825262)Termination reason: Instruction limit
% 33.12/10.92 % (3825262)Termination phase: Finite model building constraint generation
% 33.12/10.92 % (3825262)Time elapsed: 0.826 s
% 33.12/10.92 % (3825262)Peak memory usage: 201 MB
% 33.12/10.92 % (3825262)Instructions burned: 2174 (million)
% 33.12/10.92 % (3825265)ott+10_1_sil=32000:tgt=ground:random_seed=1931935129:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 33.12/10.92 % (3825264)ott-2_1_sil=16000:newcnf=on:random_seed=1117099397:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2954 on theBenchmark for (2954ds/869Mi)
% 33.12/10.92 % (3825264)Instruction limit reached!
% 33.12/10.92 % (3825264)------------------------------
% 33.12/10.92 % (3825264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/10.92 % (3825264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/10.92 % (3825264)CaDiCaL version: 2.1.3
% 33.12/10.92 % (3825264)Termination reason: Instruction limit
% 33.12/10.92 % (3825264)Termination phase: Saturation
% 33.12/10.92 % (3825264)Time elapsed: 0.538 s
% 33.12/10.92 % (3825264)Peak memory usage: 16 MB
% 33.12/10.92 % (3825264)Instructions burned: 870 (million)
% 33.12/10.92 % (3825268)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3819532736:i=54282_2948 on theBenchmark for (2948ds/54282Mi)
% 33.12/10.92 % Detected minimum model sizes of [4]
% 33.12/10.92 % Detected maximum model sizes of [max]
% 33.12/10.92 % TRYING [4]
% 33.12/10.92 % TRYING [5]
% 33.12/10.92 % TRYING [6]
% 33.12/10.92 % TRYING [7]
% 33.12/10.92 % TRYING [8]
% 33.12/10.92 % (3825252)Instruction limit reached!
% 33.12/10.92 % (3825252)------------------------------
% 33.12/10.92 % (3825252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/10.92 % (3825252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/10.92 % (3825252)CaDiCaL version: 2.1.3
% 33.12/10.92 % (3825252)Termination reason: Instruction limit
% 33.12/10.92 % (3825252)Termination phase: Finite model building constraint generation
% 33.12/10.92 % (3825252)Time elapsed: 4.583 s
% 33.12/10.92 % (3825252)Peak memory usage: 877 MB
% 33.12/10.92 % (3825252)Instructions burned: 9515 (million)
% 33.12/10.92 % (3825270)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2122604018:i=3512:aac=none_2943 on theBenchmark for (2943ds/3512Mi)
% 33.12/10.92 % TRYING [9]
% 33.12/10.92 % (3825250)Instruction limit reached!
% 33.12/10.92 % (3825250)------------------------------
% 33.12/10.92 % (3825250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/10.92 % (3825250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/10.92 % (3825250)CaDiCaL version: 2.1.3
% 33.12/10.92 % (3825250)Termination reason: Instruction limit
% 33.12/10.92 % (3825250)Termination phase: Finite model building SAT solving
% 33.12/10.92 % (3825250)Time elapsed: 6.050 s
% 33.12/10.92 % (3825250)Peak memory usage: 115 MB
% 33.12/10.92 % (3825250)Instructions burned: 22063 (million)
% 33.12/10.92 % (3825272)dis+21_1_sil=32000:sas=cadical:random_seed=3594055131:i=3773:amm=off_2932 on theBenchmark for (2932ds/3773Mi)
% 33.12/10.92 % (3825270)Instruction limit reached!
% 33.12/10.92 % (3825270)------------------------------
% 33.12/10.92 % (3825270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/10.92 % (3825270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/10.92 % (3825270)CaDiCaL version: 2.1.3
% 33.12/10.92 % (3825270)Termination reason: Instruction limit
% 33.12/10.92 % (3825270)Termination phase: Saturation
% 33.12/10.92 % (3825270)Time elapsed: 1.952 s
% 33.12/10.92 % (3825270)Peak memory usage: 20 MB
% 33.12/10.92 % (3825270)Instructions burned: 3512 (million)
% 33.12/10.92 % (3825274)ott+11_1_sil=16000:gs=on:random_seed=2436589307:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2923 on theBenchmark for (2923ds/2251Mi)
% 33.12/10.92 % (3825265)Instruction limit reached!
% 33.12/10.92 % (3825265)------------------------------
% 33.12/10.92 % (3825265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/10.92 % (3825265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/10.92 % (3825265)CaDiCaL version: 2.1.3
% 33.12/10.92 % (3825265)Termination reason: Instruction limit
% 33.12/10.92 % (3825265)Termination phase: Saturation
% 33.12/10.92 % (3825265)Time elapsed: 3.119 s
% 33.12/10.92 % (3825265)Peak memory usage: 33 MB
% 33.12/10.92 % (3825265)Instructions burned: 5115 (million)
% 33.12/10.92 % (3825276)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=81956199:fmbsr=1.6:i=67534_2922 on theBenchmark for (2922ds/67534Mi)
% 33.12/10.92 % Detected minimum model sizes of [4]
% 33.12/10.92 % Detected maximum model sizes of [max]
% 33.12/10.92 % TRYING [7]
% 33.12/10.92 % (3825272)Instruction limit reached!
% 33.12/10.92 % (3825272)------------------------------
% 33.12/10.92 % (3825272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/10.92 % (3825272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/10.92 % (3825272)CaDiCaL version: 2.1.3
% 33.12/10.92 % (3825272)Termination reason: Instruction limit
% 33.12/10.92 % (3825272)Termination phase: Saturation
% 33.12/10.92 % (3825272)Time elapsed: 1.212 s
% 33.12/10.92 % (3825272)Peak memory usage: 27 MB
% 33.12/10.92 % (3825272)Instructions burned: 3775 (million)
% 33.12/10.92 % (3825278)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2159899777:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2920 on theBenchmark for (2920ds/4591Mi)
% 33.12/10.92 % TRYING [8]
% 33.12/10.92 % TRYING [9]
% 33.12/10.92 % (3825274)Instruction limit reached!
% 33.12/10.92 % (3825274)------------------------------
% 33.12/10.92 % (3825274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/10.92 % (3825274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/10.92 % (3825274)CaDiCaL version: 2.1.3
% 33.12/10.92 % (3825274)Termination reason: Instruction limit
% 33.12/10.92 % (3825274)Termination phase: Saturation
% 33.12/10.92 % (3825274)Time elapsed: 1.557 s
% 33.12/10.92 % (3825274)Peak memory usage: 30 MB
% 33.12/10.92 % (3825274)Instructions burned: 2251 (million)
% 33.12/10.92 % (3825278)Instruction limit reached!
% 33.12/10.92 % (3825278)------------------------------
% 33.12/10.92 % (3825278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/10.92 % (3825278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/10.92 % (3825278)CaDiCaL version: 2.1.3
% 33.12/10.92 % (3825278)Termination reason: Instruction limit
% 33.12/10.92 % (3825278)Termination phase: Saturation
% 33.12/10.92 % (3825278)Time elapsed: 1.256 s
% 33.12/10.92 % (3825278)Peak memory usage: 23 MB
% 33.12/10.92 % (3825278)Instructions burned: 4592 (million)
% 33.12/10.92 % (3825280)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3632727101:i=29340_2908 on theBenchmark for (2908ds/29340Mi)
% 33.12/10.92 % (3825281)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=727585945:i=5211_2907 on theBenchmark for (2907ds/5211Mi)
% 33.12/10.92 % TRYING [10]
% 33.12/10.92 % TRYING [11]
% 33.12/10.92 % TRYING [10]
% 33.12/10.92 % (3825280) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3825211-3825280"...
% 33.12/10.92 % (3825280)...printing done.
% 33.12/10.92 % (3825280)Refutation found. Thanks to Tanya!
% 33.12/10.92 % SZS status Theorem for theBenchmark
% 33.12/10.92 % SZS output start Proof for theBenchmark
% See solution above
% 33.12/10.92 % (3825280)------------------------------
% 33.12/10.92 % (3825280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.12/10.92 % (3825280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.12/10.92 % (3825280)CaDiCaL version: 2.1.3
% 33.12/10.92 % (3825280)Termination reason: Refutation
% 33.12/10.92 % (3825280)Time elapsed: 1.281 s
% 33.12/10.92 % (3825280)Peak memory usage: 22 MB
% 33.12/10.92 % (3825280)Instructions burned: 2559 (million)
% 33.12/10.92 % (3825211)Success in time 10.515 s
% 33.12/10.92 % Vampire exiting
%------------------------------------------------------------------------------