%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRO006+3 : 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 : n003.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:35 PM UTC 2026
% Result : Theorem 95.55s 14.03s
% Output : Refutation 95.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 27
% Syntax : Number of formulae : 189 ( 67 unt; 0 def)
% Number of atoms : 550 ( 26 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 596 ( 235 ~; 233 |; 101 &)
% ( 9 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-3 aty)
% Number of variables : 347 ( 312 !; 35 ?)
% 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(f7,axiom,
! [X0,X1,X2] :
( ( earlier(X0,X1)
& earlier(X2,X1) )
=> ( earlier(X2,X0)
| earlier(X0,X2)
| X0 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_06) ).
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(f10,axiom,
! [X0,X1] :
( ( legal(X0)
& earlier(X1,X0) )
=> legal(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_09) ).
fof(f11,axiom,
! [X0,X1] :
( precedes(X0,X1)
<=> ( earlier(X0,X1)
& legal(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_10) ).
fof(f15,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ~ root(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_14) ).
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(f21,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X1,X0,X3)
& min_precedes(X2,X0,X3)
& precedes(X1,X2) )
=> min_precedes(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_20) ).
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(f26,axiom,
! [X0,X1,X2] :
( min_precedes(X1,X2,X0)
=> ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_25) ).
fof(f28,axiom,
! [X0,X1] :
( ( occurrence_of(X1,X0)
& ~ atomic(X0) )
=> ? [X2] :
( root(X2,X0)
& subactivity_occurrence(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_27) ).
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(f34,axiom,
! [X0,X1] :
( root_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_33) ).
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,X2,X3] :
( ( occurrence_of(X2,X3)
& root_occ(X0,X2)
& root_occ(X1,X2) )
=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_35) ).
fof(f38,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& leaf_occ(X1,X0) )
=> ~ ? [X3] : min_precedes(X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_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/sandbox/benchmark/theBenchmark.p',sos_43) ).
fof(f47,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> arboreal(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_46) ).
fof(f50,axiom,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( occurrence_of(X1,tptp4)
& root_occ(X1,X0)
& occurrence_of(X2,tptp3)
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_49) ).
fof(f52,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_51) ).
fof(f56,axiom,
atomic(tptp1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_55) ).
fof(f60,axiom,
tptp1 != tptp3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_59) ).
fof(f63,axiom,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_62) ).
fof(f64,conjecture,
~ ? [X0] : occurrence_of(X0,tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f65,negated_conjecture,
~ ~ ? [X0] : occurrence_of(X0,tptp0),
inference(negated_conjecture,[status(cth)],[f64]) ).
fof(f66,plain,
? [X0] : occurrence_of(X0,tptp0),
inference(flattening,[],[f65]) ).
fof(f69,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f3]) ).
fof(f70,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f69]) ).
fof(f75,plain,
! [X0,X1,X2] :
( earlier(X2,X0)
| earlier(X0,X2)
| X0 = X2
| ~ earlier(X0,X1)
| ~ earlier(X2,X1) ),
inference(ennf_transformation,[],[f7]) ).
fof(f76,plain,
! [X0,X1,X2] :
( earlier(X2,X0)
| earlier(X0,X2)
| X0 = X2
| ~ earlier(X0,X1)
| ~ earlier(X2,X1) ),
inference(flattening,[],[f75]) ).
fof(f77,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f78,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f79,plain,
! [X0,X1] :
( legal(X1)
| ~ legal(X0)
| ~ earlier(X1,X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f80,plain,
! [X0,X1] :
( legal(X1)
| ~ legal(X0)
| ~ earlier(X1,X0) ),
inference(flattening,[],[f79]) ).
fof(f84,plain,
! [X0,X1,X2] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f15]) ).
fof(f85,plain,
! [X0,X1,X2] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f16]) ).
fof(f86,plain,
! [X0,X1] :
( legal(X0)
| ~ root(X0,X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f92,plain,
! [X0,X1,X2,X3] :
( min_precedes(X1,X2,X3)
| ~ min_precedes(X1,X0,X3)
| ~ min_precedes(X2,X0,X3)
| ~ precedes(X1,X2) ),
inference(ennf_transformation,[],[f21]) ).
fof(f93,plain,
! [X0,X1,X2,X3] :
( min_precedes(X1,X2,X3)
| ~ min_precedes(X1,X0,X3)
| ~ min_precedes(X2,X0,X3)
| ~ precedes(X1,X2) ),
inference(flattening,[],[f92]) ).
fof(f94,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(f95,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(f97,plain,
! [X0,X1,X2] :
( ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) )
| ~ min_precedes(X1,X2,X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f100,plain,
! [X0,X1] :
( ? [X2] :
( root(X2,X0)
& subactivity_occurrence(X2,X1) )
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f101,plain,
! [X0,X1] :
( ? [X2] :
( root(X2,X0)
& subactivity_occurrence(X2,X1) )
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(flattening,[],[f100]) ).
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(ennf_transformation,[],[f30]) ).
fof(f105,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ min_precedes(X0,X1,X2)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(flattening,[],[f104]) ).
fof(f112,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| ~ root_occ(X1,X2) ),
inference(ennf_transformation,[],[f36]) ).
fof(f113,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| ~ root_occ(X1,X2) ),
inference(flattening,[],[f112]) ).
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(f133,plain,
! [X0,X1,X2] :
( arboreal(X0)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f47]) ).
fof(f138,plain,
! [X0] :
( ? [X1,X2] :
( occurrence_of(X1,tptp4)
& root_occ(X1,X0)
& occurrence_of(X2,tptp3)
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f139,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f63]) ).
fof(f140,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(flattening,[],[f139]) ).
fof(f142,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f77]) ).
fof(f143,plain,
! [X0,X1] :
( ( precedes(X0,X1)
| ~ earlier(X0,X1)
| ~ legal(X1) )
& ( ( earlier(X0,X1)
& legal(X1) )
| ~ precedes(X0,X1) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f144,plain,
! [X0,X1] :
( ( precedes(X0,X1)
| ~ earlier(X0,X1)
| ~ legal(X1) )
& ( ( earlier(X0,X1)
& legal(X1) )
| ~ precedes(X0,X1) ) ),
inference(flattening,[],[f143]) ).
fof(f148,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,[],[f94]) ).
fof(f149,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,[],[f148]) ).
fof(f150,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,[],[f149]) ).
fof(f151,plain,
! [X0,X1] :
( ( leaf(X0,X1)
| ( ~ root(X0,X1)
& ! [X2] : ~ min_precedes(X2,X0,X1) )
| min_precedes(X0,sK5(X0,X1),X1) )
& ( ( ( root(X0,X1)
| min_precedes(sK6(X0,X1),X0,X1) )
& ! [X5] : ~ min_precedes(X0,X5,X1) )
| ~ leaf(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6]),skolemize(X3,sK5(X0,X1)),skolemize(X4,sK6(X0,X1))],[f150]) ).
fof(f152,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,[],[f95]) ).
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(flattening,[],[f152]) ).
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)
& ! [X4] :
( ~ min_precedes(X0,X4,X2)
| ~ min_precedes(X4,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(rectify,[],[f153]) ).
fof(f155,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))],[f154]) ).
fof(f159,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK9(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK9(X0,X1,X2))
& subactivity_occurrence(X2,sK9(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X3,sK9(X0,X1,X2))],[f97]) ).
fof(f161,plain,
! [X0,X1] :
( ( root(sK11(X0,X1),X0)
& subactivity_occurrence(sK11(X0,X1),X1) )
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X2,sK11(X0,X1))],[f101]) ).
fof(f163,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) )
| ~ root_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f164,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ? [X3] :
( occurrence_of(X1,X3)
& subactivity_occurrence(X0,X1)
& root(X0,X3) )
| ~ root_occ(X0,X1) ) ),
inference(rectify,[],[f163]) ).
fof(f165,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ( occurrence_of(X1,sK13(X0,X1))
& subactivity_occurrence(X0,X1)
& root(X0,sK13(X0,X1)) )
| ~ root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X3,sK13(X0,X1))],[f164]) ).
fof(f166,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(f167,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,[],[f166]) ).
fof(f168,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))],[f167]) ).
fof(f170,plain,
! [X0] :
( ( occurrence_of(sK16(X0),tptp4)
& root_occ(sK16(X0),X0)
& occurrence_of(sK17(X0),tptp3)
& leaf_occ(sK17(X0),X0)
& next_subocc(sK16(X0),sK17(X0),tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17]),skolemize(X1,sK16(X0)),skolemize(X2,sK17(X0))],[f138]) ).
fof(f171,plain,
! [X0,X1] :
( ( occurrence_of(sK18(X0),tptp1)
& next_subocc(X0,sK18(X0),tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X2,sK18(X0))],[f140]) ).
fof(f172,plain,
occurrence_of(sK19,tptp0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(X0,sK19)],[f66]) ).
fof(f177,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f70]) ).
fof(f181,plain,
! [X2,X0,X1] :
( ~ earlier(X2,X1)
| earlier(X0,X2)
| X0 = X2
| ~ earlier(X0,X1)
| earlier(X2,X0) ),
inference(cnf_transformation,[],[f76]) ).
fof(f183,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f184,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f185,plain,
! [X0,X1] :
( ~ earlier(X1,X0)
| ~ legal(X0)
| legal(X1) ),
inference(cnf_transformation,[],[f80]) ).
fof(f186,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| legal(X1) ),
inference(cnf_transformation,[],[f144]) ).
fof(f187,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| earlier(X0,X1) ),
inference(cnf_transformation,[],[f144]) ).
fof(f188,plain,
! [X0,X1] :
( ~ earlier(X0,X1)
| precedes(X0,X1)
| ~ legal(X1) ),
inference(cnf_transformation,[],[f144]) ).
fof(f197,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| ~ root(X1,X2) ),
inference(cnf_transformation,[],[f84]) ).
fof(f198,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(cnf_transformation,[],[f85]) ).
fof(f199,plain,
! [X0,X1] :
( ~ root(X0,X1)
| legal(X0) ),
inference(cnf_transformation,[],[f86]) ).
fof(f203,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X2,X0,X3)
| ~ min_precedes(X1,X0,X3)
| min_precedes(X1,X2,X3)
| ~ precedes(X1,X2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f205,plain,
! [X0,X1] :
( ~ leaf(X0,X1)
| min_precedes(sK6(X0,X1),X0,X1)
| root(X0,X1) ),
inference(cnf_transformation,[],[f151]) ).
fof(f208,plain,
! [X2,X0,X1,X4] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) ),
inference(cnf_transformation,[],[f155]) ).
fof(f209,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f155]) ).
fof(f218,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK9(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f159]) ).
fof(f219,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X1,sK9(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f159]) ).
fof(f220,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| occurrence_of(sK9(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f159]) ).
fof(f223,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| subactivity_occurrence(sK11(X0,X1),X1)
| atomic(X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f224,plain,
! [X0,X1] :
( root(sK11(X0,X1),X0)
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f226,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,[],[f105]) ).
fof(f231,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| root(X0,sK13(X0,X1)) ),
inference(cnf_transformation,[],[f165]) ).
fof(f233,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| occurrence_of(X1,sK13(X0,X1)) ),
inference(cnf_transformation,[],[f165]) ).
fof(f234,plain,
! [X2,X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2)
| root_occ(X0,X1)
| ~ root(X0,X2) ),
inference(cnf_transformation,[],[f165]) ).
fof(f235,plain,
! [X0,X1] :
( leaf(X0,sK14(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
fof(f236,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
fof(f237,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| occurrence_of(X1,sK14(X0,X1)) ),
inference(cnf_transformation,[],[f168]) ).
fof(f239,plain,
! [X2,X3,X0,X1] :
( ~ root_occ(X1,X2)
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f113]) ).
fof(f241,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f247,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(f252,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| arboreal(X0) ),
inference(cnf_transformation,[],[f133]) ).
fof(f255,plain,
! [X0] :
( next_subocc(sK16(X0),sK17(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f256,plain,
! [X0] :
( leaf_occ(sK17(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f257,plain,
! [X0] :
( occurrence_of(sK17(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f258,plain,
! [X0] :
( root_occ(sK16(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f261,plain,
~ atomic(tptp0),
inference(cnf_transformation,[],[f52]) ).
fof(f265,plain,
atomic(tptp1),
inference(cnf_transformation,[],[f56]) ).
fof(f269,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f60]) ).
fof(f272,plain,
! [X0,X1] :
( next_subocc(X0,sK18(X0),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f171]) ).
fof(f273,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK18(X0),tptp1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f171]) ).
fof(f274,plain,
occurrence_of(sK19,tptp0),
inference(cnf_transformation,[],[f172]) ).
fof(f316,plain,
leaf_occ(sK17(sK19),sK19),
inference(unit_resulting_resolution,[],[f256,f274]) ).
fof(f318,plain,
subactivity_occurrence(sK17(sK19),sK19),
inference(unit_resulting_resolution,[],[f236,f316]) ).
fof(f394,plain,
root_occ(sK16(sK19),sK19),
inference(unit_resulting_resolution,[],[f258,f274]) ).
fof(f498,plain,
root(sK16(sK19),sK13(sK16(sK19),sK19)),
inference(unit_resulting_resolution,[],[f231,f394]) ).
fof(f504,plain,
! [X0] : ~ min_precedes(X0,sK16(sK19),sK13(sK16(sK19),sK19)),
inference(unit_resulting_resolution,[],[f197,f498]) ).
fof(f505,plain,
legal(sK16(sK19)),
inference(unit_resulting_resolution,[],[f199,f498]) ).
fof(f559,plain,
occurrence_of(sK19,sK13(sK16(sK19),sK19)),
inference(unit_resulting_resolution,[],[f233,f394]) ).
fof(f669,plain,
leaf(sK17(sK19),sK14(sK17(sK19),sK19)),
inference(unit_resulting_resolution,[],[f235,f316]) ).
fof(f774,plain,
occurrence_of(sK19,sK14(sK17(sK19),sK19)),
inference(unit_resulting_resolution,[],[f237,f316]) ).
fof(f892,plain,
tptp0 = sK13(sK16(sK19),sK19),
inference(unit_resulting_resolution,[],[f177,f559,f274]) ).
fof(f893,plain,
tptp0 = sK14(sK17(sK19),sK19),
inference(unit_resulting_resolution,[],[f177,f774,f274]) ).
fof(f1165,plain,
root(sK16(sK19),tptp0),
inference(superposition,[],[f498,f892]) ).
fof(f1168,plain,
! [X0] : ~ min_precedes(X0,sK16(sK19),tptp0),
inference(superposition,[],[f504,f892]) ).
fof(f1661,plain,
next_subocc(sK16(sK19),sK17(sK19),tptp0),
inference(unit_resulting_resolution,[],[f255,f274]) ).
fof(f1665,plain,
min_precedes(sK16(sK19),sK17(sK19),tptp0),
inference(unit_resulting_resolution,[],[f209,f1661]) ).
fof(f1673,plain,
precedes(sK16(sK19),sK17(sK19)),
inference(unit_resulting_resolution,[],[f198,f1665]) ).
fof(f1674,plain,
~ root(sK17(sK19),tptp0),
inference(unit_resulting_resolution,[],[f197,f1665]) ).
fof(f1682,plain,
earlier(sK16(sK19),sK17(sK19)),
inference(unit_resulting_resolution,[],[f187,f1673]) ).
fof(f1683,plain,
legal(sK17(sK19)),
inference(unit_resulting_resolution,[],[f186,f1673]) ).
fof(f3722,plain,
subactivity_occurrence(sK11(tptp0,sK19),sK19),
inference(unit_resulting_resolution,[],[f223,f261,f274]) ).
fof(f3987,plain,
root(sK11(tptp0,sK19),tptp0),
inference(unit_resulting_resolution,[],[f224,f261,f274]) ).
fof(f4006,plain,
legal(sK11(tptp0,sK19)),
inference(unit_resulting_resolution,[],[f199,f3987]) ).
fof(f4017,plain,
arboreal(sK11(tptp0,sK19)),
inference(unit_resulting_resolution,[],[f184,f4006]) ).
fof(f4219,plain,
~ leaf_occ(sK16(sK19),sK19),
inference(unit_resulting_resolution,[],[f241,f274,f1665]) ).
fof(f5526,plain,
( min_precedes(sK6(sK17(sK19),sK14(sK17(sK19),sK19)),sK17(sK19),sK14(sK17(sK19),sK19))
| root(sK17(sK19),sK14(sK17(sK19),sK19)) ),
inference(resolution,[],[f205,f669]) ).
fof(f5530,plain,
( min_precedes(sK6(sK17(sK19),tptp0),sK17(sK19),tptp0)
| root(sK17(sK19),sK14(sK17(sK19),sK19)) ),
inference(forward_demodulation,[],[f5526,f893]) ).
fof(f5636,plain,
( root(sK17(sK19),tptp0)
| min_precedes(sK6(sK17(sK19),tptp0),sK17(sK19),tptp0) ),
inference(forward_demodulation,[],[f5530,f893]) ).
fof(f5679,plain,
min_precedes(sK6(sK17(sK19),tptp0),sK17(sK19),tptp0),
inference(forward_subsumption_resolution,[],[f5636,f1674]) ).
fof(f5964,plain,
precedes(sK6(sK17(sK19),tptp0),sK17(sK19)),
inference(unit_resulting_resolution,[],[f198,f5679]) ).
fof(f5976,plain,
~ leaf_occ(sK6(sK17(sK19),tptp0),sK19),
inference(unit_resulting_resolution,[],[f241,f274,f5679]) ).
fof(f5984,plain,
arboreal(sK6(sK17(sK19),tptp0)),
inference(unit_resulting_resolution,[],[f252,f5679]) ).
fof(f6006,plain,
earlier(sK6(sK17(sK19),tptp0),sK17(sK19)),
inference(unit_resulting_resolution,[],[f187,f5964]) ).
fof(f6017,plain,
legal(sK6(sK17(sK19),tptp0)),
inference(unit_resulting_resolution,[],[f185,f1683,f6006]) ).
fof(f6119,plain,
~ min_precedes(sK16(sK19),sK6(sK17(sK19),tptp0),tptp0),
inference(unit_resulting_resolution,[],[f208,f5679,f1661]) ).
fof(f6336,plain,
root_occ(sK11(tptp0,sK19),sK19),
inference(unit_resulting_resolution,[],[f234,f274,f3987,f3722]) ).
fof(f6766,plain,
sK16(sK19) = sK11(tptp0,sK19),
inference(unit_resulting_resolution,[],[f239,f274,f6336,f394]) ).
fof(f6778,plain,
! [X2,X0,X1] :
( ~ root_occ(X2,X0)
| ~ occurrence_of(X0,X1)
| sK16(X0) = X2
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f239,f258]) ).
fof(f7564,plain,
subactivity_occurrence(sK6(sK17(sK19),tptp0),sK19),
inference(unit_resulting_resolution,[],[f226,f274,f318,f5679]) ).
fof(f10146,plain,
~ precedes(sK6(sK17(sK19),tptp0),sK16(sK19)),
inference(unit_resulting_resolution,[],[f203,f1168,f5679,f1665]) ).
fof(f10150,plain,
~ precedes(sK16(sK19),sK6(sK17(sK19),tptp0)),
inference(unit_resulting_resolution,[],[f203,f1665,f6119,f5679]) ).
fof(f10191,plain,
~ earlier(sK6(sK17(sK19),tptp0),sK16(sK19)),
inference(unit_resulting_resolution,[],[f188,f505,f10146]) ).
fof(f10193,plain,
~ earlier(sK16(sK19),sK6(sK17(sK19),tptp0)),
inference(unit_resulting_resolution,[],[f188,f6017,f10150]) ).
fof(f10197,plain,
sK16(sK19) = sK6(sK17(sK19),tptp0),
inference(unit_resulting_resolution,[],[f181,f1682,f6006,f10191,f10193]) ).
fof(f13163,plain,
( ~ occurrence_of(sK19,tptp0)
| occurrence_of(sK18(sK11(tptp0,sK19)),tptp1)
| ~ arboreal(sK11(tptp0,sK19))
| leaf_occ(sK11(tptp0,sK19),sK19) ),
inference(resolution,[],[f273,f3722]) ).
fof(f13169,plain,
( occurrence_of(sK18(sK11(tptp0,sK19)),tptp1)
| ~ arboreal(sK11(tptp0,sK19))
| leaf_occ(sK11(tptp0,sK19),sK19) ),
inference(forward_subsumption_resolution,[],[f13163,f274]) ).
fof(f13194,plain,
( occurrence_of(sK18(sK11(tptp0,sK19)),tptp1)
| leaf_occ(sK11(tptp0,sK19),sK19) ),
inference(forward_subsumption_resolution,[],[f13169,f4017]) ).
fof(f13209,plain,
( occurrence_of(sK18(sK16(sK19)),tptp1)
| leaf_occ(sK11(tptp0,sK19),sK19) ),
inference(forward_demodulation,[],[f13194,f6766]) ).
fof(f13222,plain,
( leaf_occ(sK16(sK19),sK19)
| occurrence_of(sK18(sK16(sK19)),tptp1) ),
inference(forward_demodulation,[],[f13209,f6766]) ).
fof(f13230,plain,
occurrence_of(sK18(sK16(sK19)),tptp1),
inference(forward_subsumption_resolution,[],[f13222,f4219]) ).
fof(f13243,plain,
arboreal(sK18(sK16(sK19))),
inference(unit_resulting_resolution,[],[f183,f265,f13230]) ).
fof(f13893,plain,
next_subocc(sK6(sK17(sK19),tptp0),sK18(sK6(sK17(sK19),tptp0)),tptp0),
inference(unit_resulting_resolution,[],[f272,f5984,f5976,f7564,f274]) ).
fof(f13954,plain,
next_subocc(sK16(sK19),sK18(sK16(sK19)),tptp0),
inference(forward_demodulation,[],[f13893,f10197]) ).
fof(f14052,plain,
min_precedes(sK16(sK19),sK18(sK16(sK19)),tptp0),
inference(unit_resulting_resolution,[],[f209,f13954]) ).
fof(f14082,plain,
subactivity_occurrence(sK18(sK16(sK19)),sK9(tptp0,sK16(sK19),sK18(sK16(sK19)))),
inference(unit_resulting_resolution,[],[f218,f14052]) ).
fof(f14083,plain,
subactivity_occurrence(sK16(sK19),sK9(tptp0,sK16(sK19),sK18(sK16(sK19)))),
inference(unit_resulting_resolution,[],[f219,f14052]) ).
fof(f14084,plain,
occurrence_of(sK9(tptp0,sK16(sK19),sK18(sK16(sK19))),tptp0),
inference(unit_resulting_resolution,[],[f220,f14052]) ).
fof(f14582,plain,
occurrence_of(sK17(sK9(tptp0,sK16(sK19),sK18(sK16(sK19)))),tptp3),
inference(unit_resulting_resolution,[],[f257,f14084]) ).
fof(f15614,plain,
! [X2,X0,X1] :
( ~ subactivity_occurrence(X2,X0)
| ~ occurrence_of(X0,X1)
| sK17(X0) = X2
| ~ arboreal(X2)
| min_precedes(X2,sK17(X0),X1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f247,f256]) ).
fof(f16026,plain,
root_occ(sK16(sK19),sK9(tptp0,sK16(sK19),sK18(sK16(sK19)))),
inference(unit_resulting_resolution,[],[f234,f1165,f14084,f14083]) ).
fof(f16450,plain,
~ occurrence_of(sK17(sK9(tptp0,sK16(sK19),sK18(sK16(sK19)))),tptp1),
inference(unit_resulting_resolution,[],[f177,f269,f14582]) ).
fof(f26467,plain,
sK16(sK19) = sK16(sK9(tptp0,sK16(sK19),sK18(sK16(sK19)))),
inference(unit_resulting_resolution,[],[f6778,f14084,f16026,f14084]) ).
fof(f26889,plain,
( next_subocc(sK16(sK19),sK17(sK9(tptp0,sK16(sK19),sK18(sK16(sK19)))),tptp0)
| ~ occurrence_of(sK9(tptp0,sK16(sK19),sK18(sK16(sK19))),tptp0) ),
inference(superposition,[],[f255,f26467]) ).
fof(f26912,plain,
next_subocc(sK16(sK19),sK17(sK9(tptp0,sK16(sK19),sK18(sK16(sK19)))),tptp0),
inference(forward_subsumption_resolution,[],[f26889,f14084]) ).
fof(f27801,plain,
~ min_precedes(sK18(sK16(sK19)),sK17(sK9(tptp0,sK16(sK19),sK18(sK16(sK19)))),tptp0),
inference(unit_resulting_resolution,[],[f208,f14052,f26912]) ).
fof(f35955,plain,
sK18(sK16(sK19)) = sK17(sK9(tptp0,sK16(sK19),sK18(sK16(sK19)))),
inference(unit_resulting_resolution,[],[f15614,f13243,f14084,f14084,f14082,f27801]) ).
fof(f36122,plain,
~ occurrence_of(sK18(sK16(sK19)),tptp1),
inference(superposition,[],[f16450,f35955]) ).
fof(f36222,plain,
$false,
inference(forward_subsumption_resolution,[],[f36122,f13230]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO006+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n003.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 22:18:56 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 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.07/2.83 % (974440)Will run a generic schedule for satisfiability detection.
% 16.07/2.83 % (974446)% WARNING: option uhcvi not known.
% 16.07/2.83 % (974446)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1104146922:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.07/2.83 % (974445)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1249076252_2999 on theBenchmark for (2999ds/0Mi)
% 16.07/2.83 % (974447)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3870439210:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.07/2.83 % (974448)dis+10_1_sil=32000:sp=arity:random_seed=282110607:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.07/2.83 % (974449)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4169634287:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.07/2.83 % (974450)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1124117970:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.07/2.83 % (974451)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3533919027:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.07/2.83 % Detected minimum model sizes of [4]
% 16.07/2.83 % Detected maximum model sizes of [max]
% 16.07/2.83 % TRYING [4]
% 16.07/2.83 % TRYING [5]
% 16.07/2.83 % (974451)Instruction limit reached!
% 16.07/2.83 % (974451)------------------------------
% 16.07/2.83 % (974451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.07/2.83 % (974451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.07/2.83 % (974451)CaDiCaL version: 2.1.3
% 16.07/2.83 % (974451)Termination reason: Instruction limit
% 16.07/2.83 % (974451)Termination phase: Saturation
% 16.07/2.83 % (974451)Time elapsed: 0.058 s
% 16.07/2.83 % (974451)Peak memory usage: 12 MB
% 16.07/2.83 % (974451)Instructions burned: 161 (million)
% 16.07/2.83 % TRYING [6]
% 16.07/2.83 % (974448)Instruction limit reached!
% 16.07/2.83 % (974448)------------------------------
% 16.07/2.83 % (974448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.07/2.83 % (974448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.07/2.83 % (974448)CaDiCaL version: 2.1.3
% 16.07/2.83 % (974448)Termination reason: Instruction limit
% 16.07/2.83 % (974448)Termination phase: Saturation
% 16.07/2.83 % (974448)Time elapsed: 0.071 s
% 16.07/2.83 % (974448)Peak memory usage: 12 MB
% 16.07/2.83 % (974448)Instructions burned: 104 (million)
% 16.07/2.83 % (974449)Instruction limit reached!
% 16.07/2.83 % (974449)------------------------------
% 16.07/2.83 % (974449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.07/2.83 % (974449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.07/2.83 % (974449)CaDiCaL version: 2.1.3
% 16.07/2.83 % (974449)Termination reason: Instruction limit
% 16.07/2.83 % (974449)Termination phase: Saturation
% 16.07/2.83 % (974449)Time elapsed: 0.073 s
% 16.07/2.83 % (974449)Peak memory usage: 12 MB
% 16.07/2.83 % (974449)Instructions burned: 117 (million)
% 16.07/2.83 % (974459)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=771199709:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.07/2.83 % Detected minimum model sizes of [4]
% 16.07/2.83 % Detected maximum model sizes of [max]
% 16.07/2.83 % TRYING [4]
% 16.07/2.83 % (974450)Instruction limit reached!
% 16.07/2.83 % (974450)------------------------------
% 16.07/2.83 % (974450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.07/2.83 % (974450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.07/2.83 % (974450)CaDiCaL version: 2.1.3
% 16.07/2.83 % (974450)Termination reason: Instruction limit
% 16.07/2.83 % (974450)Termination phase: Saturation
% 16.07/2.83 % (974450)Time elapsed: 0.088 s
% 16.07/2.83 % (974450)Peak memory usage: 13 MB
% 16.07/2.83 % (974450)Instructions burned: 132 (million)
% 16.07/2.83 % (974461)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=1314747569:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.07/2.83 % (974460)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=530167005:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.07/2.83 % TRYING [5]
% 16.07/2.83 % (974463)ott-21_1_sil=16000:fs=off:random_seed=529260627:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.07/2.83 % TRYING [6]
% 16.07/2.83 % (974460)Instruction limit reached!
% 16.07/2.83 % (974460)------------------------------
% 16.07/2.83 % (974460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.01/7.95 % (974460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.01/7.95 % (974460)CaDiCaL version: 2.1.3
% 53.01/7.95 % (974460)Termination reason: Instruction limit
% 53.01/7.95 % (974460)Termination phase: Saturation
% 53.01/7.95 % (974460)Time elapsed: 0.088 s
% 53.01/7.95 % (974460)Peak memory usage: 13 MB
% 53.01/7.95 % (974460)Instructions burned: 132 (million)
% 53.01/7.95 % (974467)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3522064768:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 53.01/7.95 % (974463)Instruction limit reached!
% 53.01/7.95 % (974463)------------------------------
% 53.01/7.95 % (974463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.01/7.95 % (974463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.01/7.95 % (974463)CaDiCaL version: 2.1.3
% 53.01/7.95 % (974463)Termination reason: Instruction limit
% 53.01/7.95 % (974463)Termination phase: Saturation
% 53.01/7.95 % (974463)Time elapsed: 0.098 s
% 53.01/7.95 % (974463)Peak memory usage: 13 MB
% 53.01/7.95 % (974463)Instructions burned: 181 (million)
% 53.01/7.96 % TRYING [7]
% 53.01/7.96 % (974469)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1442471184:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 53.01/7.96 % Detected minimum model sizes of [4]
% 53.01/7.96 % Detected maximum model sizes of [max]
% 53.01/7.96 % TRYING [4]
% 53.01/7.96 % TRYING [5]
% 53.01/7.96 % TRYING [7]
% 53.01/7.96 % TRYING [6]
% 53.01/7.96 % (974459)Instruction limit reached!
% 53.01/7.96 % (974459)------------------------------
% 53.01/7.96 % (974459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.01/7.96 % (974459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.01/7.96 % (974459)CaDiCaL version: 2.1.3
% 53.01/7.96 % (974459)Termination reason: Instruction limit
% 53.01/7.96 % (974459)Termination phase: Finite model building constraint generation
% 53.01/7.96 % (974459)Time elapsed: 0.313 s
% 53.01/7.96 % (974459)Peak memory usage: 29 MB
% 53.01/7.96 % (974459)Instructions burned: 716 (million)
% 53.01/7.96 % (974471)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2035617730:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 53.01/7.96 % TRYING [7]
% 53.01/7.96 % (974461)Instruction limit reached!
% 53.01/7.96 % (974461)------------------------------
% 53.01/7.96 % (974461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.01/7.96 % (974461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.01/7.96 % (974461)CaDiCaL version: 2.1.3
% 53.01/7.96 % (974461)Termination reason: Instruction limit
% 53.01/7.96 % (974461)Termination phase: Saturation
% 53.01/7.96 % (974461)Time elapsed: 0.421 s
% 53.01/7.96 % (974461)Peak memory usage: 19 MB
% 53.01/7.96 % (974461)Instructions burned: 686 (million)
% 53.01/7.96 % (974473)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3490906833:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 53.01/7.96 % (974467)Instruction limit reached!
% 53.01/7.96 % (974467)------------------------------
% 53.01/7.96 % (974467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.01/7.96 % (974467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.01/7.96 % (974467)CaDiCaL version: 2.1.3
% 53.01/7.96 % (974467)Termination reason: Instruction limit
% 53.01/7.96 % (974467)Termination phase: Saturation
% 53.01/7.96 % (974467)Time elapsed: 0.337 s
% 53.01/7.96 % (974467)Peak memory usage: 15 MB
% 53.01/7.96 % (974467)Instructions burned: 477 (million)
% 53.01/7.96 % (974475)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=2418400803: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)
% 53.01/7.96 % (974469)Instruction limit reached!
% 53.01/7.96 % (974469)------------------------------
% 53.01/7.96 % (974469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.01/7.96 % (974469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.01/7.96 % (974469)CaDiCaL version: 2.1.3
% 53.01/7.96 % (974469)Termination reason: Instruction limit
% 53.01/7.96 % (974469)Termination phase: Finite model building constraint generation
% 53.01/7.96 % (974469)Time elapsed: 0.337 s
% 53.01/7.96 % (974469)Peak memory usage: 23 MB
% 53.01/7.96 % (974469)Instructions burned: 865 (million)
% 53.01/7.96 % (974477)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1758908991:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 95.55/14.03 % TRYING [14]
% 95.55/14.03 % (974473)Instruction limit reached!
% 95.55/14.03 % (974473)------------------------------
% 95.55/14.03 % (974473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974473)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974473)Termination reason: Instruction limit
% 95.55/14.03 % (974473)Termination phase: Finite model building constraint generation
% 95.55/14.03 % (974473)Time elapsed: 0.320 s
% 95.55/14.03 % (974473)Peak memory usage: 73 MB
% 95.55/14.03 % (974473)Instructions burned: 890 (million)
% 95.55/14.03 % (974479)fmb+10_1_sil=64000:random_seed=2306803858:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 95.55/14.03 % Detected minimum model sizes of [4]
% 95.55/14.03 % Detected maximum model sizes of [max]
% 95.55/14.03 % TRYING [4]
% 95.55/14.03 % TRYING [5]
% 95.55/14.03 % (974475)Instruction limit reached!
% 95.55/14.03 % (974475)------------------------------
% 95.55/14.03 % (974475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974475)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974475)Termination reason: Instruction limit
% 95.55/14.03 % (974475)Termination phase: Saturation
% 95.55/14.03 % (974475)Time elapsed: 0.425 s
% 95.55/14.03 % (974475)Peak memory usage: 20 MB
% 95.55/14.03 % (974475)Instructions burned: 692 (million)
% 95.55/14.03 % TRYING [6]
% 95.55/14.03 % (974481)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1719179566:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 95.55/14.03 % Detected minimum model sizes of [4]
% 95.55/14.03 % Detected maximum model sizes of [max]
% 95.55/14.03 % TRYING [20]
% 95.55/14.03 % (974477)Instruction limit reached!
% 95.55/14.03 % (974477)------------------------------
% 95.55/14.03 % (974477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974477)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974477)Termination reason: Instruction limit
% 95.55/14.03 % (974477)Termination phase: Saturation
% 95.55/14.03 % (974477)Time elapsed: 0.504 s
% 95.55/14.03 % (974477)Peak memory usage: 18 MB
% 95.55/14.03 % (974477)Instructions burned: 879 (million)
% 95.55/14.03 % (974483)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4251235695:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 95.55/14.03 % Detected minimum model sizes of [4]
% 95.55/14.03 % Detected maximum model sizes of [max]
% 95.55/14.03 % TRYING [8]
% 95.55/14.03 % (974471)Instruction limit reached!
% 95.55/14.03 % (974471)------------------------------
% 95.55/14.03 % (974471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974471)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974471)Termination reason: Instruction limit
% 95.55/14.03 % (974471)Termination phase: Saturation
% 95.55/14.03 % (974471)Time elapsed: 0.724 s
% 95.55/14.03 % (974471)Peak memory usage: 25 MB
% 95.55/14.03 % (974471)Instructions burned: 1181 (million)
% 95.55/14.03 % (974485)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3815831095:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 95.55/14.03 % TRYING [7]
% 95.55/14.03 % TRYING [8]
% 95.55/14.03 % (974483)Instruction limit reached!
% 95.55/14.03 % (974483)------------------------------
% 95.55/14.03 % (974483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974483)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974483)Termination reason: Instruction limit
% 95.55/14.03 % (974483)Termination phase: Finite model building SAT solving
% 95.55/14.03 % (974483)Time elapsed: 0.448 s
% 95.55/14.03 % (974483)Peak memory usage: 54 MB
% 95.55/14.03 % (974483)Instructions burned: 921 (million)
% 95.55/14.03 % (974487)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1182324684:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 95.55/14.03 % TRYING [8]
% 95.55/14.03 % (974487)Instruction limit reached!
% 95.55/14.03 % (974487)------------------------------
% 95.55/14.03 % (974487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974487)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974487)Termination reason: Instruction limit
% 95.55/14.03 % (974487)Termination phase: Saturation
% 95.55/14.03 % (974487)Time elapsed: 0.789 s
% 95.55/14.03 % (974487)Peak memory usage: 27 MB
% 95.55/14.03 % (974487)Instructions burned: 1473 (million)
% 95.55/14.03 % (974489)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=503416504:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 95.55/14.03 % Detected minimum model sizes of [4]
% 95.55/14.03 % Detected maximum model sizes of [max]
% 95.55/14.03 % TRYING [77]
% 95.55/14.03 % (974485)Instruction limit reached!
% 95.55/14.03 % (974485)------------------------------
% 95.55/14.03 % (974485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974485)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974485)Termination reason: Instruction limit
% 95.55/14.03 % (974485)Termination phase: Saturation
% 95.55/14.03 % (974485)Time elapsed: 2.783 s
% 95.55/14.03 % (974485)Peak memory usage: 22 MB
% 95.55/14.03 % (974485)Instructions burned: 5134 (million)
% 95.55/14.03 % (974491)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=608575275:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 95.55/14.03 % Detected minimum model sizes of [4]
% 95.55/14.03 % Detected maximum model sizes of [max]
% 95.55/14.03 % TRYING [16]
% 95.55/14.03 % (974489)Instruction limit reached!
% 95.55/14.03 % (974489)------------------------------
% 95.55/14.03 % (974489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974489)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974489)Termination reason: Instruction limit
% 95.55/14.03 % (974489)Termination phase: Finite model building constraint generation
% 95.55/14.03 % (974489)Time elapsed: 2.178 s
% 95.55/14.03 % (974489)Peak memory usage: 409 MB
% 95.55/14.03 % (974489)Instructions burned: 6325 (million)
% 95.55/14.03 % (974493)ott-2_1_sil=16000:newcnf=on:random_seed=3707494799:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2953 on theBenchmark for (2953ds/869Mi)
% 95.55/14.03 % TRYING [9]
% 95.55/14.03 % (974491)Instruction limit reached!
% 95.55/14.03 % (974491)------------------------------
% 95.55/14.03 % (974491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974491)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974491)Termination reason: Instruction limit
% 95.55/14.03 % (974491)Termination phase: Finite model building constraint generation
% 95.55/14.03 % (974491)Time elapsed: 0.769 s
% 95.55/14.03 % (974491)Peak memory usage: 161 MB
% 95.55/14.03 % (974491)Instructions burned: 2175 (million)
% 95.55/14.03 % (974495)ott+10_1_sil=32000:tgt=ground:random_seed=4057709439:i=5114:av=off_2952 on theBenchmark for (2952ds/5114Mi)
% 95.55/14.03 % (974493)Instruction limit reached!
% 95.55/14.03 % (974493)------------------------------
% 95.55/14.03 % (974493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974493)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974493)Termination reason: Instruction limit
% 95.55/14.03 % (974493)Termination phase: Saturation
% 95.55/14.03 % (974493)Time elapsed: 0.518 s
% 95.55/14.03 % (974493)Peak memory usage: 17 MB
% 95.55/14.03 % (974493)Instructions burned: 869 (million)
% 95.55/14.03 % (974497)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2497897226:i=54282_2948 on theBenchmark for (2948ds/54282Mi)
% 95.55/14.03 % Detected minimum model sizes of [4]
% 95.55/14.03 % Detected maximum model sizes of [max]
% 95.55/14.03 % TRYING [4]
% 95.55/14.03 % TRYING [5]
% 95.55/14.03 % TRYING [6]
% 95.55/14.03 % (974481)Instruction limit reached!
% 95.55/14.03 % (974481)------------------------------
% 95.55/14.03 % (974481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974481)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974481)Termination reason: Instruction limit
% 95.55/14.03 % (974481)Termination phase: Finite model building constraint generation
% 95.55/14.03 % (974481)Time elapsed: 4.324 s
% 95.55/14.03 % (974481)Peak memory usage: 870 MB
% 95.55/14.03 % (974481)Instructions burned: 9516 (million)
% 95.55/14.03 % TRYING [7]
% 95.55/14.03 % (974499)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=351743447:i=3512:aac=none_2945 on theBenchmark for (2945ds/3512Mi)
% 95.55/14.03 % TRYING [9]
% 95.55/14.03 % TRYING [8]
% 95.55/14.03 % (974499)Instruction limit reached!
% 95.55/14.03 % (974499)------------------------------
% 95.55/14.03 % (974499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974499)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974499)Termination reason: Instruction limit
% 95.55/14.03 % (974499)Termination phase: Saturation
% 95.55/14.03 % (974499)Time elapsed: 2.042 s
% 95.55/14.03 % (974499)Peak memory usage: 23 MB
% 95.55/14.03 % (974499)Instructions burned: 3513 (million)
% 95.55/14.03 % (974501)dis+21_1_sil=32000:sas=cadical:random_seed=678346097:i=3773:amm=off_2924 on theBenchmark for (2924ds/3773Mi)
% 95.55/14.03 % (974495)Instruction limit reached!
% 95.55/14.03 % (974495)------------------------------
% 95.55/14.03 % (974495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974495)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974495)Termination reason: Instruction limit
% 95.55/14.03 % (974495)Termination phase: Saturation
% 95.55/14.03 % (974495)Time elapsed: 3.184 s
% 95.55/14.03 % (974495)Peak memory usage: 39 MB
% 95.55/14.03 % (974495)Instructions burned: 5114 (million)
% 95.55/14.03 % (974503)ott+11_1_sil=16000:gs=on:random_seed=1083041281:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2920 on theBenchmark for (2920ds/2251Mi)
% 95.55/14.03 % (974503)Instruction limit reached!
% 95.55/14.03 % (974503)------------------------------
% 95.55/14.03 % (974503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974503)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974503)Termination reason: Instruction limit
% 95.55/14.03 % (974503)Termination phase: Saturation
% 95.55/14.03 % (974503)Time elapsed: 1.617 s
% 95.55/14.03 % (974503)Peak memory usage: 30 MB
% 95.55/14.03 % (974503)Instructions burned: 2252 (million)
% 95.55/14.03 % (974505)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2307266638:fmbsr=1.6:i=67534_2903 on theBenchmark for (2903ds/67534Mi)
% 95.55/14.03 % Detected minimum model sizes of [4]
% 95.55/14.03 % Detected maximum model sizes of [max]
% 95.55/14.03 % TRYING [7]
% 95.55/14.03 % (974501)Instruction limit reached!
% 95.55/14.03 % (974501)------------------------------
% 95.55/14.03 % (974501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974501)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974501)Termination reason: Instruction limit
% 95.55/14.03 % (974501)Termination phase: Saturation
% 95.55/14.03 % (974501)Time elapsed: 2.420 s
% 95.55/14.03 % (974501)Peak memory usage: 33 MB
% 95.55/14.03 % (974501)Instructions burned: 3774 (million)
% 95.55/14.03 % (974507)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2811343923:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2900 on theBenchmark for (2900ds/4591Mi)
% 95.55/14.03 % TRYING [8]
% 95.55/14.03 % TRYING [9]
% 95.55/14.03 % (974507)Instruction limit reached!
% 95.55/14.03 % (974507)------------------------------
% 95.55/14.03 % (974507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974507)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974507)Termination reason: Instruction limit
% 95.55/14.03 % (974507)Termination phase: Saturation
% 95.55/14.03 % (974507)Time elapsed: 1.449 s
% 95.55/14.03 % (974507)Peak memory usage: 12 MB
% 95.55/14.03 % (974507)Instructions burned: 4592 (million)
% 95.55/14.03 % (974509)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2264284679:i=29340_2885 on theBenchmark for (2885ds/29340Mi)
% 95.55/14.03 % (974479)Instruction limit reached!
% 95.55/14.03 % (974479)------------------------------
% 95.55/14.03 % (974479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974479)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974479)Termination reason: Instruction limit
% 95.55/14.03 % (974479)Termination phase: Finite model building SAT solving
% 95.55/14.03 % (974479)Time elapsed: 11.052 s
% 95.55/14.03 % (974479)Peak memory usage: 63 MB
% 95.55/14.03 % (974479)Instructions burned: 22062 (million)
% 95.55/14.03 % (974511)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1894864547:i=5211_2880 on theBenchmark for (2880ds/5211Mi)
% 95.55/14.03 % TRYING [9]
% 95.55/14.03 % (974509) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-974440-974509"...
% 95.55/14.03 % (974509)...printing done.
% 95.55/14.03 % (974509)Refutation found. Thanks to Tanya!
% 95.55/14.03 % SZS status Theorem for theBenchmark
% 95.55/14.03 % SZS output start Proof for theBenchmark
% See solution above
% 95.55/14.03 % (974509)------------------------------
% 95.55/14.03 % (974509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.55/14.03 % (974509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.55/14.03 % (974509)CaDiCaL version: 2.1.3
% 95.55/14.03 % (974509)Termination reason: Refutation
% 95.55/14.03 % (974509)Time elapsed: 2.112 s
% 95.55/14.03 % (974509)Peak memory usage: 22 MB
% 95.55/14.03 % (974509)Instructions burned: 4258 (million)
% 95.55/14.03 % (974440)Success in time 13.607 s
% 95.55/14.03 % Vampire exiting
%------------------------------------------------------------------------------