%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRO016+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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 61.01s 9.07s
% Output : Refutation 61.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 16
% Syntax : Number of formulae : 114 ( 42 unt; 1 def)
% Number of atoms : 457 ( 10 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 542 ( 199 ~; 194 |; 128 &)
% ( 6 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-3 aty)
% Number of variables : 235 ( 198 !; 37 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,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/sandbox2/benchmark/theBenchmark.p',sos_04) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& leaf_occ(X1,X0) )
=> ~ ? [X3] : min_precedes(X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_09) ).
fof(f17,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_16) ).
fof(f19,axiom,
! [X0,X1] :
( leaf_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_18) ).
fof(f22,axiom,
! [X0,X1] :
( precedes(X0,X1)
<=> ( earlier(X0,X1)
& legal(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_21) ).
fof(f25,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> precedes(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_24) ).
fof(f27,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ~ ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_26) ).
fof(f28,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X0,X1,X2)
& occurrence_of(X3,X2)
& subactivity_occurrence(X1,X3) )
=> subactivity_occurrence(X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_27) ).
fof(f29,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X2,X3)
& ~ atomic(X3)
& leaf_occ(X0,X2)
& leaf_occ(X1,X2) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_28) ).
fof(f31,axiom,
! [X0,X1,X2] :
( ( earlier(X0,X1)
& earlier(X1,X2) )
=> earlier(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_30) ).
fof(f32,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X0,X1,X3)
& min_precedes(X0,X2,X3)
& precedes(X1,X2) )
=> min_precedes(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_31) ).
fof(f33,axiom,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> ? [X2,X3,X4] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X3,tptp4)
& 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/sandbox2/benchmark/theBenchmark.p',sos_32) ).
fof(f35,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_34) ).
fof(f36,axiom,
atomic(tptp4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_35) ).
fof(f46,conjecture,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> ? [X2,X3] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& ( occurrence_of(X3,tptp1)
| occurrence_of(X3,tptp2) )
& min_precedes(X2,X3,tptp0)
& leaf_occ(X3,X1)
& ( occurrence_of(X3,tptp1)
=> ~ ? [X4] :
( occurrence_of(X4,tptp2)
& min_precedes(X2,X4,tptp0) ) )
& ( occurrence_of(X3,tptp2)
=> ~ ? [X5] :
( occurrence_of(X5,tptp1)
& min_precedes(X2,X5,tptp0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f47,negated_conjecture,
~ ! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> ? [X2,X3] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& ( occurrence_of(X3,tptp1)
| occurrence_of(X3,tptp2) )
& min_precedes(X2,X3,tptp0)
& leaf_occ(X3,X1)
& ( occurrence_of(X3,tptp1)
=> ~ ? [X4] :
( occurrence_of(X4,tptp2)
& min_precedes(X2,X4,tptp0) ) )
& ( occurrence_of(X3,tptp2)
=> ~ ? [X5] :
( occurrence_of(X5,tptp1)
& min_precedes(X2,X5,tptp0) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f62,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,[],[f5]) ).
fof(f63,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,[],[f62]) ).
fof(f70,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f71,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(flattening,[],[f70]) ).
fof(f79,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f85,plain,
! [X0,X1,X2] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f25]) ).
fof(f87,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,[],[f27]) ).
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,[],[f28]) ).
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(f90,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| ~ leaf_occ(X1,X2) ),
inference(ennf_transformation,[],[f29]) ).
fof(f91,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| ~ leaf_occ(X1,X2) ),
inference(flattening,[],[f90]) ).
fof(f94,plain,
! [X0,X1,X2] :
( earlier(X0,X2)
| ~ earlier(X0,X1)
| ~ earlier(X1,X2) ),
inference(ennf_transformation,[],[f31]) ).
fof(f95,plain,
! [X0,X1,X2] :
( earlier(X0,X2)
| ~ earlier(X0,X1)
| ~ earlier(X1,X2) ),
inference(flattening,[],[f94]) ).
fof(f96,plain,
! [X0,X1,X2,X3] :
( min_precedes(X1,X2,X3)
| ~ min_precedes(X0,X1,X3)
| ~ min_precedes(X0,X2,X3)
| ~ precedes(X1,X2) ),
inference(ennf_transformation,[],[f32]) ).
fof(f97,plain,
! [X0,X1,X2,X3] :
( min_precedes(X1,X2,X3)
| ~ min_precedes(X0,X1,X3)
| ~ min_precedes(X0,X2,X3)
| ~ precedes(X1,X2) ),
inference(flattening,[],[f96]) ).
fof(f98,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,[],[f33]) ).
fof(f99,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,[],[f98]) ).
fof(f100,plain,
? [X0,X1] :
( ! [X2,X3] :
( ~ occurrence_of(X2,tptp3)
| ~ next_subocc(X0,X2,tptp0)
| ( ~ occurrence_of(X3,tptp1)
& ~ occurrence_of(X3,tptp2) )
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf_occ(X3,X1)
| ( ? [X4] :
( occurrence_of(X4,tptp2)
& min_precedes(X2,X4,tptp0) )
& occurrence_of(X3,tptp1) )
| ( ? [X5] :
( occurrence_of(X5,tptp1)
& min_precedes(X2,X5,tptp0) )
& occurrence_of(X3,tptp2) ) )
& occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f47]) ).
fof(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) )
| ( ? [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,[],[f100]) ).
fof(f102,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(f103,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,[],[f101,f102]) ).
fof(f114,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f79]) ).
fof(f115,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,[],[f19]) ).
fof(f116,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,[],[f115]) ).
fof(f117,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ( occurrence_of(X1,sK9(X0,X1))
& subactivity_occurrence(X0,X1)
& leaf(X0,sK9(X0,X1)) )
| ~ leaf_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X3,sK9(X0,X1))],[f116]) ).
fof(f118,plain,
! [X0,X1] :
( ( precedes(X0,X1)
| ~ earlier(X0,X1)
| ~ legal(X1) )
& ( ( earlier(X0,X1)
& legal(X1) )
| ~ precedes(X0,X1) ) ),
inference(nnf_transformation,[],[f22]) ).
fof(f119,plain,
! [X0,X1] :
( ( precedes(X0,X1)
| ~ earlier(X0,X1)
| ~ legal(X1) )
& ( ( earlier(X0,X1)
& legal(X1) )
| ~ precedes(X0,X1) ) ),
inference(flattening,[],[f118]) ).
fof(f121,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,[],[f87]) ).
fof(f122,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,[],[f121]) ).
fof(f123,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,[],[f122]) ).
fof(f124,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ( min_precedes(X0,sK11(X0,X1,X2),X2)
& min_precedes(sK11(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,[sK11]),skolemize(X3,sK11(X0,X1,X2))],[f123]) ).
fof(f125,plain,
! [X0,X1] :
( ( occurrence_of(sK12(X0,X1),tptp3)
& next_subocc(X0,sK12(X0,X1),tptp0)
& occurrence_of(sK13(X0,X1),tptp4)
& next_subocc(sK12(X0,X1),sK13(X0,X1),tptp0)
& ( occurrence_of(sK14(X0,X1),tptp1)
| occurrence_of(sK14(X0,X1),tptp2) )
& next_subocc(sK13(X0,X1),sK14(X0,X1),tptp0)
& leaf_occ(sK14(X0,X1),X1) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14]),skolemize(X2,sK12(X0,X1)),skolemize(X3,sK13(X0,X1)),skolemize(X4,sK14(X0,X1))],[f99]) ).
fof(f129,plain,
( ! [X2,X3] :
( ~ occurrence_of(X2,tptp3)
| ~ next_subocc(sK16,X2,tptp0)
| ( ~ occurrence_of(X3,tptp1)
& ~ occurrence_of(X3,tptp2) )
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf_occ(X3,sK17)
| ( occurrence_of(sK18(X2),tptp2)
& min_precedes(X2,sK18(X2),tptp0)
& occurrence_of(X3,tptp1) )
| sP0(X2,X3) )
& occurrence_of(sK17,tptp0)
& subactivity_occurrence(sK16,sK17)
& arboreal(sK16)
& ~ leaf_occ(sK16,sK17) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18]),skolemize(X0,sK16),skolemize(X1,sK17),skolemize(X4,sK18(X2))],[f103]) ).
fof(f135,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,[],[f63]) ).
fof(f143,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(cnf_transformation,[],[f71]) ).
fof(f156,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f159,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f164,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| legal(X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f165,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| earlier(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f166,plain,
! [X0,X1] :
( ~ earlier(X0,X1)
| precedes(X0,X1)
| ~ legal(X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f170,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(cnf_transformation,[],[f85]) ).
fof(f173,plain,
! [X2,X0,X1,X4] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) ),
inference(cnf_transformation,[],[f124]) ).
fof(f174,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f124]) ).
fof(f177,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(f178,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X1,X2)
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f91]) ).
fof(f180,plain,
! [X2,X0,X1] :
( ~ earlier(X1,X2)
| ~ earlier(X0,X1)
| earlier(X0,X2) ),
inference(cnf_transformation,[],[f95]) ).
fof(f181,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X0,X2,X3)
| ~ min_precedes(X0,X1,X3)
| min_precedes(X1,X2,X3)
| ~ precedes(X1,X2) ),
inference(cnf_transformation,[],[f97]) ).
fof(f182,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| leaf_occ(sK14(X0,X1),X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f183,plain,
! [X0,X1] :
( next_subocc(sK13(X0,X1),sK14(X0,X1),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f185,plain,
! [X0,X1] :
( next_subocc(sK12(X0,X1),sK13(X0,X1),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f186,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK13(X0,X1),tptp4)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f187,plain,
! [X0,X1] :
( next_subocc(X0,sK12(X0,X1),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f189,plain,
~ atomic(tptp0),
inference(cnf_transformation,[],[f35]) ).
fof(f190,plain,
atomic(tptp4),
inference(cnf_transformation,[],[f36]) ).
fof(f203,plain,
~ leaf_occ(sK16,sK17),
inference(cnf_transformation,[],[f129]) ).
fof(f204,plain,
arboreal(sK16),
inference(cnf_transformation,[],[f129]) ).
fof(f205,plain,
subactivity_occurrence(sK16,sK17),
inference(cnf_transformation,[],[f129]) ).
fof(f206,plain,
occurrence_of(sK17,tptp0),
inference(cnf_transformation,[],[f129]) ).
fof(f2351,plain,
leaf_occ(sK14(sK16,sK17),sK17),
inference(unit_resulting_resolution,[],[f182,f204,f203,f205,f206]) ).
fof(f2371,plain,
subactivity_occurrence(sK14(sK16,sK17),sK17),
inference(unit_resulting_resolution,[],[f159,f2351]) ).
fof(f2598,plain,
occurrence_of(sK13(sK16,sK17),tptp4),
inference(unit_resulting_resolution,[],[f186,f204,f203,f205,f206]) ).
fof(f2621,plain,
arboreal(sK13(sK16,sK17)),
inference(unit_resulting_resolution,[],[f156,f190,f2598]) ).
fof(f3414,plain,
next_subocc(sK13(sK16,sK17),sK14(sK16,sK17),tptp0),
inference(unit_resulting_resolution,[],[f183,f204,f203,f205,f206]) ).
fof(f3426,plain,
min_precedes(sK13(sK16,sK17),sK14(sK16,sK17),tptp0),
inference(unit_resulting_resolution,[],[f174,f3414]) ).
fof(f3439,plain,
~ leaf_occ(sK13(sK16,sK17),sK17),
inference(unit_resulting_resolution,[],[f143,f206,f3426]) ).
fof(f3451,plain,
~ min_precedes(sK13(sK16,sK17),sK13(sK16,sK17),tptp0),
inference(unit_resulting_resolution,[],[f173,f3414,f3426]) ).
fof(f3452,plain,
subactivity_occurrence(sK13(sK16,sK17),sK17),
inference(unit_resulting_resolution,[],[f177,f206,f2371,f3426]) ).
fof(f3462,plain,
! [X0] :
( ~ leaf_occ(sK13(sK16,sK17),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f3426,f143]) ).
fof(f3487,plain,
leaf_occ(sK14(sK13(sK16,sK17),sK17),sK17),
inference(unit_resulting_resolution,[],[f182,f206,f2621,f3439,f3452]) ).
fof(f3489,plain,
occurrence_of(sK13(sK13(sK16,sK17),sK17),tptp4),
inference(unit_resulting_resolution,[],[f186,f206,f2621,f3439,f3452]) ).
fof(f3490,plain,
next_subocc(sK13(sK16,sK17),sK12(sK13(sK16,sK17),sK17),tptp0),
inference(unit_resulting_resolution,[],[f187,f206,f2621,f3439,f3452]) ).
fof(f3550,plain,
sK14(sK16,sK17) = sK14(sK13(sK16,sK17),sK17),
inference(unit_resulting_resolution,[],[f178,f189,f206,f2351,f3487]) ).
fof(f3589,plain,
arboreal(sK13(sK13(sK16,sK17),sK17)),
inference(unit_resulting_resolution,[],[f156,f190,f3489]) ).
fof(f3660,plain,
next_subocc(sK12(sK16,sK17),sK13(sK16,sK17),tptp0),
inference(unit_resulting_resolution,[],[f185,f204,f203,f205,f206]) ).
fof(f3662,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0)
| ~ arboreal(X1)
| leaf_occ(X1,X0)
| min_precedes(sK12(X1,X0),sK13(X1,X0),tptp0) ),
inference(resolution,[],[f185,f174]) ).
fof(f3666,plain,
min_precedes(sK12(sK16,sK17),sK13(sK16,sK17),tptp0),
inference(unit_resulting_resolution,[],[f174,f3660]) ).
fof(f3689,plain,
precedes(sK12(sK16,sK17),sK13(sK16,sK17)),
inference(unit_resulting_resolution,[],[f170,f3666]) ).
fof(f3779,plain,
legal(sK13(sK16,sK17)),
inference(unit_resulting_resolution,[],[f164,f3689]) ).
fof(f4066,plain,
~ precedes(sK13(sK16,sK17),sK13(sK16,sK17)),
inference(unit_resulting_resolution,[],[f181,f3666,f3666,f3451]) ).
fof(f4068,plain,
~ earlier(sK13(sK16,sK17),sK13(sK16,sK17)),
inference(unit_resulting_resolution,[],[f166,f3779,f4066]) ).
fof(f4343,plain,
( next_subocc(sK13(sK13(sK16,sK17),sK17),sK14(sK16,sK17),tptp0)
| ~ occurrence_of(sK17,tptp0)
| ~ subactivity_occurrence(sK13(sK16,sK17),sK17)
| ~ arboreal(sK13(sK16,sK17))
| leaf_occ(sK13(sK16,sK17),sK17) ),
inference(superposition,[],[f183,f3550]) ).
fof(f4344,plain,
( next_subocc(sK13(sK13(sK16,sK17),sK17),sK14(sK16,sK17),tptp0)
| ~ occurrence_of(sK17,tptp0)
| ~ subactivity_occurrence(sK13(sK16,sK17),sK17)
| ~ arboreal(sK13(sK16,sK17)) ),
inference(forward_subsumption_resolution,[],[f4343,f3462]) ).
fof(f4345,plain,
( next_subocc(sK13(sK13(sK16,sK17),sK17),sK14(sK16,sK17),tptp0)
| ~ subactivity_occurrence(sK13(sK16,sK17),sK17)
| ~ arboreal(sK13(sK16,sK17)) ),
inference(forward_subsumption_resolution,[],[f4344,f206]) ).
fof(f4346,plain,
( next_subocc(sK13(sK13(sK16,sK17),sK17),sK14(sK16,sK17),tptp0)
| ~ arboreal(sK13(sK16,sK17)) ),
inference(forward_subsumption_resolution,[],[f4345,f3452]) ).
fof(f4347,plain,
next_subocc(sK13(sK13(sK16,sK17),sK17),sK14(sK16,sK17),tptp0),
inference(forward_subsumption_resolution,[],[f4346,f2621]) ).
fof(f6168,plain,
min_precedes(sK13(sK16,sK17),sK12(sK13(sK16,sK17),sK17),tptp0),
inference(unit_resulting_resolution,[],[f174,f3490]) ).
fof(f6833,plain,
precedes(sK13(sK16,sK17),sK12(sK13(sK16,sK17),sK17)),
inference(unit_resulting_resolution,[],[f170,f6168]) ).
fof(f6885,plain,
earlier(sK13(sK16,sK17),sK12(sK13(sK16,sK17),sK17)),
inference(unit_resulting_resolution,[],[f165,f6833]) ).
fof(f6906,plain,
~ earlier(sK12(sK13(sK16,sK17),sK17),sK13(sK16,sK17)),
inference(unit_resulting_resolution,[],[f180,f4068,f6885]) ).
fof(f6956,plain,
~ precedes(sK12(sK13(sK16,sK17),sK17),sK13(sK16,sK17)),
inference(unit_resulting_resolution,[],[f165,f6906]) ).
fof(f7147,plain,
~ min_precedes(sK13(sK13(sK16,sK17),sK17),sK13(sK16,sK17),tptp0),
inference(unit_resulting_resolution,[],[f173,f3426,f4347]) ).
fof(f7149,plain,
min_precedes(sK13(sK13(sK16,sK17),sK17),sK14(sK16,sK17),tptp0),
inference(unit_resulting_resolution,[],[f174,f4347]) ).
fof(f7790,plain,
~ min_precedes(sK13(sK16,sK17),sK13(sK13(sK16,sK17),sK17),tptp0),
inference(unit_resulting_resolution,[],[f173,f3414,f7149]) ).
fof(f7791,plain,
subactivity_occurrence(sK13(sK13(sK16,sK17),sK17),sK17),
inference(unit_resulting_resolution,[],[f177,f206,f2371,f7149]) ).
fof(f8727,plain,
sK13(sK16,sK17) = sK13(sK13(sK16,sK17),sK17),
inference(unit_resulting_resolution,[],[f135,f206,f2621,f3452,f7791,f3589,f7147,f7790]) ).
fof(f12240,plain,
min_precedes(sK12(sK13(sK16,sK17),sK17),sK13(sK13(sK16,sK17),sK17),tptp0),
inference(unit_resulting_resolution,[],[f3662,f2621,f3452,f3439,f206]) ).
fof(f12295,plain,
min_precedes(sK12(sK13(sK16,sK17),sK17),sK13(sK16,sK17),tptp0),
inference(forward_demodulation,[],[f12240,f8727]) ).
fof(f13411,plain,
$false,
inference(unit_resulting_resolution,[],[f170,f6956,f12295]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO016+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n004.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:22:22 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.11/2.71 % (3939978)Will run a generic schedule for satisfiability detection.
% 16.11/2.71 % (3939987)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2404640735:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.11/2.71 % (3939984)% WARNING: option uhcvi not known.
% 16.11/2.71 % (3939983)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1045186387_2999 on theBenchmark for (2999ds/0Mi)
% 16.11/2.71 % (3939984)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=983666206:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.11/2.71 % (3939985)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=476030306:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.11/2.71 % (3939986)dis+10_1_sil=32000:sp=arity:random_seed=1266001721:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.11/2.71 % (3939988)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3517771279:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.11/2.71 % (3939989)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1690140417:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.11/2.71 % Detected minimum model sizes of [4]
% 16.11/2.71 % Detected maximum model sizes of [max]
% 16.11/2.71 % TRYING [4]
% 16.11/2.71 % TRYING [5]
% 16.11/2.71 % (3939987)Instruction limit reached!
% 16.11/2.71 % (3939987)------------------------------
% 16.11/2.71 % (3939987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.11/2.71 % (3939987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.11/2.71 % (3939987)CaDiCaL version: 2.1.3
% 16.11/2.71 % (3939987)Termination reason: Instruction limit
% 16.11/2.71 % (3939987)Termination phase: Saturation
% 16.11/2.71 % (3939987)Time elapsed: 0.040 s
% 16.11/2.71 % (3939987)Peak memory usage: 12 MB
% 16.11/2.71 % (3939987)Instructions burned: 119 (million)
% 16.11/2.71 % TRYING [6]
% 16.11/2.71 % (3939997)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3071279402:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.11/2.71 % Detected minimum model sizes of [4]
% 16.11/2.71 % Detected maximum model sizes of [max]
% 16.11/2.71 % TRYING [4]
% 16.11/2.71 % TRYING [5]
% 16.11/2.71 % TRYING [6]
% 16.11/2.71 % (3939986)Instruction limit reached!
% 16.11/2.71 % (3939986)------------------------------
% 16.11/2.72 % (3939986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.11/2.72 % (3939986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.11/2.72 % (3939986)CaDiCaL version: 2.1.3
% 16.11/2.72 % (3939986)Termination reason: Instruction limit
% 16.11/2.72 % (3939986)Termination phase: Saturation
% 16.11/2.72 % (3939986)Time elapsed: 0.068 s
% 16.11/2.72 % (3939986)Peak memory usage: 12 MB
% 16.11/2.72 % (3939986)Instructions burned: 103 (million)
% 16.11/2.72 % (3939988)Instruction limit reached!
% 16.11/2.72 % (3939988)------------------------------
% 16.11/2.72 % (3939988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.11/2.72 % (3939988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.11/2.72 % (3939988)CaDiCaL version: 2.1.3
% 16.11/2.72 % (3939988)Termination reason: Instruction limit
% 16.11/2.72 % (3939988)Termination phase: Saturation
% 16.11/2.72 % (3939988)Time elapsed: 0.089 s
% 16.11/2.72 % (3939988)Peak memory usage: 13 MB
% 16.11/2.72 % (3939988)Instructions burned: 132 (million)
% 16.11/2.72 % (3939999)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4092927362:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.11/2.72 % TRYING [7]
% 16.11/2.72 % TRYING [7]
% 16.11/2.72 % (3939989)Instruction limit reached!
% 16.11/2.72 % (3939989)------------------------------
% 16.11/2.72 % (3939989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.11/2.72 % (3939989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.11/2.72 % (3939989)CaDiCaL version: 2.1.3
% 16.11/2.72 % (3939989)Termination reason: Instruction limit
% 16.11/2.72 % (3939989)Termination phase: Saturation
% 16.11/2.72 % (3939989)Time elapsed: 0.103 s
% 16.11/2.72 % (3939989)Peak memory usage: 14 MB
% 16.11/2.72 % (3939989)Instructions burned: 159 (million)
% 16.11/2.72 % (3940000)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=3395204211:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.11/2.72 % (3940002)ott-21_1_sil=16000:fs=off:random_seed=241652479:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.11/2.72 % (3939999)Instruction limit reached!
% 40.92/6.29 % (3939999)------------------------------
% 40.92/6.29 % (3939999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.92/6.29 % (3939999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.92/6.29 % (3939999)CaDiCaL version: 2.1.3
% 40.92/6.29 % (3939999)Termination reason: Instruction limit
% 40.92/6.29 % (3939999)Termination phase: Saturation
% 40.92/6.29 % (3939999)Time elapsed: 0.088 s
% 40.92/6.29 % (3939999)Peak memory usage: 13 MB
% 40.92/6.29 % (3939999)Instructions burned: 131 (million)
% 40.92/6.29 % TRYING [8]
% 40.92/6.29 % (3940005)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2668983681:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 40.92/6.29 % (3939997)Instruction limit reached!
% 40.92/6.29 % (3939997)------------------------------
% 40.92/6.29 % (3939997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.92/6.29 % (3939997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.92/6.29 % (3939997)CaDiCaL version: 2.1.3
% 40.92/6.29 % (3939997)Termination reason: Instruction limit
% 40.92/6.29 % (3939997)Termination phase: Finite model building constraint generation
% 40.92/6.29 % (3939997)Time elapsed: 0.169 s
% 40.92/6.29 % (3939997)Peak memory usage: 27 MB
% 40.92/6.29 % (3939997)Instructions burned: 714 (million)
% 40.92/6.29 % (3940002)Instruction limit reached!
% 40.92/6.29 % (3940002)------------------------------
% 40.92/6.29 % (3940002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.92/6.29 % (3940002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.92/6.29 % (3940002)CaDiCaL version: 2.1.3
% 40.92/6.29 % (3940002)Termination reason: Instruction limit
% 40.92/6.29 % (3940002)Termination phase: Saturation
% 40.92/6.29 % (3940002)Time elapsed: 0.094 s
% 40.92/6.29 % (3940002)Peak memory usage: 12 MB
% 40.92/6.29 % (3940002)Instructions burned: 180 (million)
% 40.92/6.29 % (3940007)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=276382533:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 40.92/6.29 % Detected minimum model sizes of [4]
% 40.92/6.29 % Detected maximum model sizes of [max]
% 40.92/6.29 % TRYING [4]
% 40.92/6.29 % (3940008)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2036681312:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 40.92/6.29 % TRYING [5]
% 40.92/6.29 % TRYING [6]
% 40.92/6.29 % TRYING [8]
% 40.92/6.29 % TRYING [7]
% 40.92/6.29 % (3940007)Instruction limit reached!
% 40.92/6.29 % (3940007)------------------------------
% 40.92/6.29 % (3940007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.92/6.29 % (3940007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.92/6.29 % (3940007)CaDiCaL version: 2.1.3
% 40.92/6.29 % (3940007)Termination reason: Instruction limit
% 40.92/6.29 % (3940007)Termination phase: Finite model building SAT solving
% 40.92/6.29 % (3940007)Time elapsed: 0.177 s
% 40.92/6.29 % (3940007)Peak memory usage: 22 MB
% 40.92/6.29 % (3940007)Instructions burned: 868 (million)
% 40.92/6.29 % (3940011)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=6359033:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 40.92/6.29 % TRYING [14]
% 40.92/6.29 % (3940000)Instruction limit reached!
% 40.92/6.29 % (3940000)------------------------------
% 40.92/6.29 % (3940000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.92/6.29 % (3940000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.92/6.29 % (3940000)CaDiCaL version: 2.1.3
% 40.92/6.29 % (3940000)Termination reason: Instruction limit
% 40.92/6.29 % (3940000)Termination phase: Saturation
% 40.92/6.29 % (3940000)Time elapsed: 0.353 s
% 40.92/6.29 % (3940000)Peak memory usage: 22 MB
% 40.92/6.29 % (3940000)Instructions burned: 684 (million)
% 40.92/6.29 % (3940013)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=86887890:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 40.92/6.29 % (3940005)Instruction limit reached!
% 40.92/6.29 % (3940005)------------------------------
% 40.92/6.29 % (3940005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.92/6.29 % (3940005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.92/6.29 % (3940005)CaDiCaL version: 2.1.3
% 40.92/6.29 % (3940005)Termination reason: Instruction limit
% 40.92/6.29 % (3940005)Termination phase: Saturation
% 40.92/6.29 % (3940005)Time elapsed: 0.343 s
% 40.92/6.29 % (3940005)Peak memory usage: 14 MB
% 40.92/6.29 % (3940005)Instructions burned: 477 (million)
% 61.01/9.07 % (3940015)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=685174875:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 61.01/9.07 % (3940011)Instruction limit reached!
% 61.01/9.07 % (3940011)------------------------------
% 61.01/9.07 % (3940011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940011)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940011)Termination reason: Instruction limit
% 61.01/9.07 % (3940011)Termination phase: Finite model building constraint generation
% 61.01/9.07 % (3940011)Time elapsed: 0.177 s
% 61.01/9.07 % (3940011)Peak memory usage: 77 MB
% 61.01/9.07 % (3940011)Instructions burned: 892 (million)
% 61.01/9.07 % (3940017)fmb+10_1_sil=64000:random_seed=3391928804:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 61.01/9.07 % Detected minimum model sizes of [4]
% 61.01/9.07 % Detected maximum model sizes of [max]
% 61.01/9.07 % TRYING [4]
% 61.01/9.07 % TRYING [5]
% 61.01/9.07 % TRYING [6]
% 61.01/9.07 % TRYING [7]
% 61.01/9.07 % TRYING [9]
% 61.01/9.07 % TRYING [8]
% 61.01/9.07 % (3940013)Instruction limit reached!
% 61.01/9.07 % (3940013)------------------------------
% 61.01/9.07 % (3940013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940013)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940013)Termination reason: Instruction limit
% 61.01/9.07 % (3940013)Termination phase: Saturation
% 61.01/9.07 % (3940013)Time elapsed: 0.415 s
% 61.01/9.07 % (3940013)Peak memory usage: 17 MB
% 61.01/9.07 % (3940013)Instructions burned: 693 (million)
% 61.01/9.07 % (3940019)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4067039888:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 61.01/9.07 % Detected minimum model sizes of [4]
% 61.01/9.07 % Detected maximum model sizes of [max]
% 61.01/9.07 % TRYING [20]
% 61.01/9.07 % (3940008)Instruction limit reached!
% 61.01/9.07 % (3940008)------------------------------
% 61.01/9.07 % (3940008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940008)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940008)Termination reason: Instruction limit
% 61.01/9.07 % (3940008)Termination phase: Saturation
% 61.01/9.07 % (3940008)Time elapsed: 0.718 s
% 61.01/9.07 % (3940008)Peak memory usage: 24 MB
% 61.01/9.07 % (3940008)Instructions burned: 1180 (million)
% 61.01/9.07 % (3940021)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3349181813:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 61.01/9.07 % Detected minimum model sizes of [4]
% 61.01/9.07 % Detected maximum model sizes of [max]
% 61.01/9.07 % TRYING [8]
% 61.01/9.07 % (3940015)Instruction limit reached!
% 61.01/9.07 % (3940015)------------------------------
% 61.01/9.07 % (3940015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940015)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940015)Termination reason: Instruction limit
% 61.01/9.07 % (3940015)Termination phase: Saturation
% 61.01/9.07 % (3940015)Time elapsed: 0.515 s
% 61.01/9.07 % (3940015)Peak memory usage: 18 MB
% 61.01/9.07 % (3940015)Instructions burned: 880 (million)
% 61.01/9.07 % (3940023)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3108331342:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 61.01/9.07 % TRYING [9]
% 61.01/9.07 % (3940021)Instruction limit reached!
% 61.01/9.07 % (3940021)------------------------------
% 61.01/9.07 % (3940021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940021)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940021)Termination reason: Instruction limit
% 61.01/9.07 % (3940021)Termination phase: Finite model building SAT solving
% 61.01/9.07 % (3940021)Time elapsed: 0.492 s
% 61.01/9.07 % (3940021)Peak memory usage: 44 MB
% 61.01/9.07 % (3940021)Instructions burned: 921 (million)
% 61.01/9.07 % (3940025)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2143421869:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 61.01/9.07 % TRYING [10]
% 61.01/9.07 % TRYING [10]
% 61.01/9.07 % (3940025)Instruction limit reached!
% 61.01/9.07 % (3940025)------------------------------
% 61.01/9.07 % (3940025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940025)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940025)Termination reason: Instruction limit
% 61.01/9.07 % (3940025)Termination phase: Saturation
% 61.01/9.07 % (3940025)Time elapsed: 0.758 s
% 61.01/9.07 % (3940025)Peak memory usage: 28 MB
% 61.01/9.07 % (3940025)Instructions burned: 1473 (million)
% 61.01/9.07 % (3940027)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=270023709:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 61.01/9.07 % Detected minimum model sizes of [4]
% 61.01/9.07 % Detected maximum model sizes of [max]
% 61.01/9.07 % TRYING [77]
% 61.01/9.07 % TRYING [11]
% 61.01/9.07 % (3940023)Instruction limit reached!
% 61.01/9.07 % (3940023)------------------------------
% 61.01/9.07 % (3940023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940023)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940023)Termination reason: Instruction limit
% 61.01/9.07 % (3940023)Termination phase: Saturation
% 61.01/9.07 % (3940023)Time elapsed: 2.775 s
% 61.01/9.07 % (3940023)Peak memory usage: 18 MB
% 61.01/9.07 % (3940023)Instructions burned: 5132 (million)
% 61.01/9.07 % (3940029)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1953359404:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 61.01/9.07 % Detected minimum model sizes of [4]
% 61.01/9.07 % Detected maximum model sizes of [max]
% 61.01/9.07 % TRYING [16]
% 61.01/9.07 % (3940027)Instruction limit reached!
% 61.01/9.07 % (3940027)------------------------------
% 61.01/9.07 % (3940027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940027)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940027)Termination reason: Instruction limit
% 61.01/9.07 % (3940027)Termination phase: Finite model building constraint generation
% 61.01/9.07 % (3940027)Time elapsed: 2.107 s
% 61.01/9.07 % (3940027)Peak memory usage: 387 MB
% 61.01/9.07 % (3940027)Instructions burned: 6326 (million)
% 61.01/9.07 % (3940031)ott-2_1_sil=16000:newcnf=on:random_seed=1164597036:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 61.01/9.07 % TRYING [12]
% 61.01/9.07 % (3940029)Instruction limit reached!
% 61.01/9.07 % (3940029)------------------------------
% 61.01/9.07 % (3940029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940029)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940029)Termination reason: Instruction limit
% 61.01/9.07 % (3940029)Termination phase: Finite model building constraint generation
% 61.01/9.07 % (3940029)Time elapsed: 0.916 s
% 61.01/9.07 % (3940029)Peak memory usage: 196 MB
% 61.01/9.07 % (3940029)Instructions burned: 2174 (million)
% 61.01/9.07 % (3940033)ott+10_1_sil=32000:tgt=ground:random_seed=1027163952:i=5114:av=off_2951 on theBenchmark for (2951ds/5114Mi)
% 61.01/9.07 % (3940031)Instruction limit reached!
% 61.01/9.07 % (3940031)------------------------------
% 61.01/9.07 % (3940031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940031)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940031)Termination reason: Instruction limit
% 61.01/9.07 % (3940031)Termination phase: Saturation
% 61.01/9.07 % (3940031)Time elapsed: 0.472 s
% 61.01/9.07 % (3940031)Peak memory usage: 15 MB
% 61.01/9.07 % (3940031)Instructions burned: 870 (million)
% 61.01/9.07 % (3940035)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1713700773:i=54282_2950 on theBenchmark for (2950ds/54282Mi)
% 61.01/9.07 % Detected minimum model sizes of [4]
% 61.01/9.07 % Detected maximum model sizes of [max]
% 61.01/9.07 % TRYING [4]
% 61.01/9.07 % TRYING [5]
% 61.01/9.07 % TRYING [6]
% 61.01/9.07 % TRYING [7]
% 61.01/9.07 % TRYING [8]
% 61.01/9.07 % (3940019)Instruction limit reached!
% 61.01/9.07 % (3940019)------------------------------
% 61.01/9.07 % (3940019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940019)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940019)Termination reason: Instruction limit
% 61.01/9.07 % (3940019)Termination phase: Finite model building constraint generation
% 61.01/9.07 % (3940019)Time elapsed: 4.841 s
% 61.01/9.07 % (3940019)Peak memory usage: 786 MB
% 61.01/9.07 % (3940019)Instructions burned: 9517 (million)
% 61.01/9.07 % TRYING [9]
% 61.01/9.07 % (3940017)Instruction limit reached!
% 61.01/9.07 % (3940017)------------------------------
% 61.01/9.07 % (3940017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940017)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940017)Termination reason: Instruction limit
% 61.01/9.07 % (3940017)Termination phase: Finite model building SAT solving
% 61.01/9.07 % (3940017)Time elapsed: 5.218 s
% 61.01/9.07 % (3940017)Peak memory usage: 114 MB
% 61.01/9.07 % (3940017)Instructions burned: 22066 (million)
% 61.01/9.07 % (3940037)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1349857089:i=3512:aac=none_2941 on theBenchmark for (2941ds/3512Mi)
% 61.01/9.07 % (3940039)dis+21_1_sil=32000:sas=cadical:random_seed=2804655761:i=3773:amm=off_2941 on theBenchmark for (2941ds/3773Mi)
% 61.01/9.07 % TRYING [11]
% 61.01/9.07 % (3940037)Instruction limit reached!
% 61.01/9.07 % (3940037)------------------------------
% 61.01/9.07 % (3940037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940037)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940037)Termination reason: Instruction limit
% 61.01/9.07 % (3940037)Termination phase: Saturation
% 61.01/9.07 % (3940037)Time elapsed: 1.011 s
% 61.01/9.07 % (3940037)Peak memory usage: 19 MB
% 61.01/9.07 % (3940037)Instructions burned: 3513 (million)
% 61.01/9.07 % (3940041)ott+11_1_sil=16000:gs=on:random_seed=852326511:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2931 on theBenchmark for (2931ds/2251Mi)
% 61.01/9.07 % TRYING [10]
% 61.01/9.07 % (3940041)Instruction limit reached!
% 61.01/9.07 % (3940041)------------------------------
% 61.01/9.07 % (3940041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940041)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940041)Termination reason: Instruction limit
% 61.01/9.07 % (3940041)Termination phase: Saturation
% 61.01/9.07 % (3940041)Time elapsed: 0.939 s
% 61.01/9.07 % (3940041)Peak memory usage: 33 MB
% 61.01/9.07 % (3940041)Instructions burned: 2253 (million)
% 61.01/9.07 % (3940043)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1118582093:fmbsr=1.6:i=67534_2921 on theBenchmark for (2921ds/67534Mi)
% 61.01/9.07 % Detected minimum model sizes of [4]
% 61.01/9.07 % Detected maximum model sizes of [max]
% 61.01/9.07 % (3940033)Instruction limit reached!
% 61.01/9.07 % (3940033)------------------------------
% 61.01/9.07 % (3940033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940033)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940033)Termination reason: Instruction limit
% 61.01/9.07 % (3940033)Termination phase: Saturation
% 61.01/9.07 % (3940033)Time elapsed: 2.983 s
% 61.01/9.07 % (3940033)Peak memory usage: 28 MB
% 61.01/9.07 % (3940033)Instructions burned: 5115 (million)
% 61.01/9.07 % TRYING [7]
% 61.01/9.07 % (3940045)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4008733021:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2921 on theBenchmark for (2921ds/4591Mi)
% 61.01/9.07 % TRYING [8]
% 61.01/9.07 % (3940039)Instruction limit reached!
% 61.01/9.07 % (3940039)------------------------------
% 61.01/9.07 % (3940039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.07 % (3940039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.07 % (3940039)CaDiCaL version: 2.1.3
% 61.01/9.07 % (3940039)Termination reason: Instruction limit
% 61.01/9.07 % (3940039)Termination phase: Saturation
% 61.01/9.07 % (3940039)Time elapsed: 2.276 s
% 61.01/9.07 % (3940039)Peak memory usage: 27 MB
% 61.01/9.07 % (3940039)Instructions burned: 3774 (million)
% 61.01/9.07 % (3940047)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3766902261:i=29340_2918 on theBenchmark for (2918ds/29340Mi)
% 61.01/9.07 % TRYING [9]
% 61.01/9.07 % (3940047) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3939978-3940047"...
% 61.01/9.07 % (3940047)...printing done.
% 61.01/9.07 % (3940047)Refutation found. Thanks to Tanya!
% 61.01/9.07 % SZS status Theorem for theBenchmark
% 61.01/9.07 % SZS output start Proof for theBenchmark
% See solution above
% 61.01/9.08 % (3940047)------------------------------
% 61.01/9.08 % (3940047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.01/9.08 % (3940047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.01/9.08 % (3940047)CaDiCaL version: 2.1.3
% 61.01/9.08 % (3940047)Termination reason: Refutation
% 61.01/9.08 % (3940047)Time elapsed: 0.407 s
% 61.01/9.08 % (3940047)Peak memory usage: 16 MB
% 61.01/9.08 % (3940047)Instructions burned: 713 (million)
% 61.01/9.08 % (3939978)Success in time 8.649 s
% 61.01/9.08 % Vampire exiting
%------------------------------------------------------------------------------