%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRO002+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : 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:32 PM UTC 2026
% Result : Theorem 128.39s 18.60s
% Output : Refutation 128.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 22
% Syntax : Number of formulae : 156 ( 42 unt; 3 def)
% Number of atoms : 435 ( 30 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 459 ( 180 ~; 167 |; 88 &)
% ( 8 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 4 prp; 0-5 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-3 aty)
% Number of variables : 296 ( 0 sgn 257 !; 39 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos) ).
fof(f2,axiom,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_01) ).
fof(f3,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
fof(f8,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_07) ).
fof(f9,axiom,
! [X0] :
( legal(X0)
=> arboreal(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_08) ).
fof(f17,axiom,
! [X0,X1] :
( root(X0,X1)
=> legal(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_16) ).
fof(f23,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ~ ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_22) ).
fof(f25,axiom,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
=> ( activity_occurrence(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_24) ).
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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',sos_27) ).
fof(f34,axiom,
! [X0,X1] :
( root_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_33) ).
fof(f36,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X2,X3)
& root_occ(X0,X2)
& root_occ(X1,X2) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_35) ).
fof(f44,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& subactivity_occurrence(X2,X1)
& leaf_occ(X3,X1)
& arboreal(X2)
& ~ min_precedes(X2,X3,X0) )
=> X3 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_43) ).
fof(f50,axiom,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( occurrence_of(X1,tptp4)
& root_occ(X1,X0)
& ( occurrence_of(X2,tptp3)
| occurrence_of(X2,tptp2) )
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_49) ).
fof(f64,axiom,
! [X0,X1,X2,X3,X4] :
( send_message(X0,X1,X2,X3,X4)
=> ( X0 != tptp4
& X0 != tptp3
& X0 != tptp2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_63) ).
fof(f65,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( send_message(X0,X1,X2,X3,X4)
& occurrence_of(X5,X0) )
=> min_precedes(X3,X5,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_64) ).
fof(f66,axiom,
! [X0,X1,X2] :
( tptp1(X0,X1,X2)
=> ( activity(X0)
& ~ atomic(X0)
& ~ atomic(X1)
& root(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_65) ).
fof(f67,axiom,
! [X0,X1,X2,X3] :
( ( tptp1(X0,X1,X2)
& occurrence_of(X3,X0) )
=> ? [X4,X5,X6,X7] :
( send_message(X4,X5,X6,X2,X1)
& occurrence_of(X7,X4)
& root_occ(X7,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_66) ).
fof(f69,conjecture,
~ ? [X0,X1,X2] :
( tptp1(X0,tptp0,X1)
& occurrence_of(X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f70,negated_conjecture,
~ ~ ? [X0,X1,X2] :
( tptp1(X0,tptp0,X1)
& occurrence_of(X2,X0) ),
inference(negated_conjecture,[status(cth)],[f69]) ).
fof(f71,plain,
? [X0,X1,X2] :
( tptp1(X0,tptp0,X1)
& occurrence_of(X2,X0) ),
inference(flattening,[],[f70]) ).
fof(f72,plain,
! [X0,X1] :
( ( activity(X0)
& activity_occurrence(X1) )
| ~ occurrence_of(X1,X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f73,plain,
! [X0] :
( ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) )
| ~ activity_occurrence(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f74,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f3]) ).
fof(f75,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f74]) ).
fof(f82,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f83,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f91,plain,
! [X0,X1] :
( legal(X0)
| ~ root(X0,X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f100,plain,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) ) ),
inference(ennf_transformation,[],[f23]) ).
fof(f101,plain,
! [X0,X1] :
( ( activity_occurrence(X0)
& activity_occurrence(X1) )
| ~ subactivity_occurrence(X0,X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f102,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(f105,plain,
! [X0,X1] :
( ? [X2] :
( root(X2,X0)
& subactivity_occurrence(X2,X1) )
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f106,plain,
! [X0,X1] :
( ? [X2] :
( root(X2,X0)
& subactivity_occurrence(X2,X1) )
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(flattening,[],[f105]) ).
fof(f117,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| ~ root_occ(X1,X2) ),
inference(ennf_transformation,[],[f36]) ).
fof(f118,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| ~ root_occ(X1,X2) ),
inference(flattening,[],[f117]) ).
fof(f133,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(f134,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,[],[f133]) ).
fof(f143,plain,
! [X0] :
( ? [X1,X2] :
( occurrence_of(X1,tptp4)
& root_occ(X1,X0)
& ( occurrence_of(X2,tptp3)
| occurrence_of(X2,tptp2) )
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f145,plain,
! [X0,X1,X2,X3,X4] :
( ( X0 != tptp4
& X0 != tptp3
& X0 != tptp2 )
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(ennf_transformation,[],[f64]) ).
fof(f146,plain,
! [X0,X1,X2,X3,X4,X5] :
( min_precedes(X3,X5,X4)
| ~ send_message(X0,X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(ennf_transformation,[],[f65]) ).
fof(f147,plain,
! [X0,X1,X2,X3,X4,X5] :
( min_precedes(X3,X5,X4)
| ~ send_message(X0,X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(flattening,[],[f146]) ).
fof(f148,plain,
! [X0,X1,X2] :
( ( activity(X0)
& ~ atomic(X0)
& ~ atomic(X1)
& root(X2,X1) )
| ~ tptp1(X0,X1,X2) ),
inference(ennf_transformation,[],[f66]) ).
fof(f149,plain,
! [X0,X1,X2,X3] :
( ? [X4,X5,X6,X7] :
( send_message(X4,X5,X6,X2,X1)
& occurrence_of(X7,X4)
& root_occ(X7,X3) )
| ~ tptp1(X0,X1,X2)
| ~ occurrence_of(X3,X0) ),
inference(ennf_transformation,[],[f67]) ).
fof(f150,plain,
! [X0,X1,X2,X3] :
( ? [X4,X5,X6,X7] :
( send_message(X4,X5,X6,X2,X1)
& occurrence_of(X7,X4)
& root_occ(X7,X3) )
| ~ tptp1(X0,X1,X2)
| ~ occurrence_of(X3,X0) ),
inference(flattening,[],[f149]) ).
fof(f151,plain,
! [X0] :
( ( activity(sK0(X0))
& occurrence_of(X0,sK0(X0)) )
| ~ activity_occurrence(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[f73]) ).
fof(f152,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f82]) ).
fof(f162,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,[],[f100]) ).
fof(f163,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,[],[f162]) ).
fof(f164,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,[],[f163]) ).
fof(f165,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))],[f164]) ).
fof(f169,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))],[f102]) ).
fof(f171,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))],[f106]) ).
fof(f173,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(f174,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,[],[f173]) ).
fof(f175,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))],[f174]) ).
fof(f180,plain,
! [X0] :
( ( occurrence_of(sK16(X0),tptp4)
& root_occ(sK16(X0),X0)
& ( occurrence_of(sK17(X0),tptp3)
| occurrence_of(sK17(X0),tptp2) )
& 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))],[f143]) ).
fof(f181,plain,
! [X0,X1,X2,X3] :
( ( send_message(sK18(X1,X2,X3),sK19(X1,X2,X3),sK20(X1,X2,X3),X2,X1)
& occurrence_of(sK21(X1,X2,X3),sK18(X1,X2,X3))
& root_occ(sK21(X1,X2,X3),X3) )
| ~ tptp1(X0,X1,X2)
| ~ occurrence_of(X3,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19,sK20,sK21]),skolemize(X4,sK18(X1,X2,X3)),skolemize(X5,sK19(X1,X2,X3)),skolemize(X6,sK20(X1,X2,X3)),skolemize(X7,sK21(X1,X2,X3))],[f150]) ).
fof(f182,plain,
( tptp1(sK22,tptp0,sK23)
& occurrence_of(sK24,sK22) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23,sK24]),skolemize(X0,sK22),skolemize(X1,sK23),skolemize(X2,sK24)],[f71]) ).
fof(f183,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f72]) ).
fof(f185,plain,
! [X0] :
( ~ activity_occurrence(X0)
| occurrence_of(X0,sK0(X0)) ),
inference(cnf_transformation,[],[f151]) ).
fof(f187,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f75]) ).
fof(f192,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ arboreal(X0)
| atomic(X1) ),
inference(cnf_transformation,[],[f152]) ).
fof(f193,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f194,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(cnf_transformation,[],[f83]) ).
fof(f209,plain,
! [X0,X1] :
( ~ root(X0,X1)
| legal(X0) ),
inference(cnf_transformation,[],[f91]) ).
fof(f218,plain,
! [X2,X0,X1,X4] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) ),
inference(cnf_transformation,[],[f165]) ).
fof(f227,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| activity_occurrence(X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f228,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK9(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f229,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X1,sK9(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f230,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| occurrence_of(sK9(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f233,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| subactivity_occurrence(sK11(X0,X1),X1)
| atomic(X0) ),
inference(cnf_transformation,[],[f171]) ).
fof(f234,plain,
! [X0,X1] :
( root(sK11(X0,X1),X0)
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(cnf_transformation,[],[f171]) ).
fof(f244,plain,
! [X2,X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2)
| root_occ(X0,X1)
| ~ root(X0,X2) ),
inference(cnf_transformation,[],[f175]) ).
fof(f249,plain,
! [X2,X3,X0,X1] :
( ~ root_occ(X1,X2)
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f118]) ).
fof(f257,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,[],[f134]) ).
fof(f265,plain,
! [X0] :
( next_subocc(sK16(X0),sK17(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f180]) ).
fof(f266,plain,
! [X0] :
( leaf_occ(sK17(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f180]) ).
fof(f267,plain,
! [X0] :
( occurrence_of(sK17(X0),tptp2)
| occurrence_of(sK17(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f180]) ).
fof(f268,plain,
! [X0] :
( root_occ(sK16(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f180]) ).
fof(f286,plain,
! [X2,X3,X0,X1,X4] :
( tptp2 != X0
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f145]) ).
fof(f287,plain,
! [X2,X3,X0,X1,X4] :
( tptp3 != X0
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f145]) ).
fof(f289,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ send_message(X0,X1,X2,X3,X4)
| min_precedes(X3,X5,X4)
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f290,plain,
! [X2,X0,X1] :
( ~ tptp1(X0,X1,X2)
| root(X2,X1) ),
inference(cnf_transformation,[],[f148]) ).
fof(f292,plain,
! [X2,X0,X1] :
( ~ tptp1(X0,X1,X2)
| ~ atomic(X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f294,plain,
! [X2,X3,X0,X1] :
( ~ tptp1(X0,X1,X2)
| root_occ(sK21(X1,X2,X3),X3)
| ~ occurrence_of(X3,X0) ),
inference(cnf_transformation,[],[f181]) ).
fof(f295,plain,
! [X2,X3,X0,X1] :
( ~ tptp1(X0,X1,X2)
| occurrence_of(sK21(X1,X2,X3),sK18(X1,X2,X3))
| ~ occurrence_of(X3,X0) ),
inference(cnf_transformation,[],[f181]) ).
fof(f296,plain,
! [X2,X3,X0,X1] :
( ~ tptp1(X0,X1,X2)
| send_message(sK18(X1,X2,X3),sK19(X1,X2,X3),sK20(X1,X2,X3),X2,X1)
| ~ occurrence_of(X3,X0) ),
inference(cnf_transformation,[],[f181]) ).
fof(f298,plain,
occurrence_of(sK24,sK22),
inference(cnf_transformation,[],[f182]) ).
fof(f299,plain,
tptp1(sK22,tptp0,sK23),
inference(cnf_transformation,[],[f182]) ).
fof(f301,plain,
! [X2,X3,X1,X4] : ~ send_message(tptp3,X1,X2,X3,X4),
inference(equality_resolution,[],[f287]) ).
fof(f302,plain,
! [X2,X3,X1,X4] : ~ send_message(tptp2,X1,X2,X3,X4),
inference(equality_resolution,[],[f286]) ).
fof(f303,plain,
activity_occurrence(sK24),
inference(unit_resulting_resolution,[],[f183,f298]) ).
fof(f315,plain,
occurrence_of(sK24,sK0(sK24)),
inference(unit_resulting_resolution,[],[f185,f303]) ).
fof(f335,plain,
~ atomic(sK22),
inference(unit_resulting_resolution,[],[f292,f299]) ).
fof(f340,plain,
( ~ arboreal(sK24)
| atomic(sK22) ),
inference(resolution,[],[f192,f298]) ).
fof(f342,plain,
~ arboreal(sK24),
inference(forward_subsumption_resolution,[],[f340,f335]) ).
fof(f354,plain,
~ atomic(sK0(sK24)),
inference(unit_resulting_resolution,[],[f193,f342,f315]) ).
fof(f376,plain,
root(sK23,tptp0),
inference(unit_resulting_resolution,[],[f290,f299]) ).
fof(f1361,plain,
sK22 = sK0(sK24),
inference(unit_resulting_resolution,[],[f187,f315,f298]) ).
fof(f4496,plain,
( subactivity_occurrence(sK11(sK22,sK24),sK24)
| atomic(sK22) ),
inference(resolution,[],[f233,f298]) ).
fof(f4499,plain,
subactivity_occurrence(sK11(sK22,sK24),sK24),
inference(forward_subsumption_resolution,[],[f4496,f335]) ).
fof(f4507,plain,
activity_occurrence(sK11(sK22,sK24)),
inference(unit_resulting_resolution,[],[f227,f4499]) ).
fof(f4512,plain,
occurrence_of(sK11(sK22,sK24),sK0(sK11(sK22,sK24))),
inference(unit_resulting_resolution,[],[f185,f4507]) ).
fof(f4523,plain,
! [X0] :
( ~ occurrence_of(sK11(sK22,sK24),X0)
| sK0(sK11(sK22,sK24)) = X0 ),
inference(resolution,[],[f4512,f187]) ).
fof(f4540,definition,
( spl25_7
<=> arboreal(sK11(sK22,sK24)) ),
introduced(definition,[new_symbols(definition,[spl25_7])],[avatar_definition]) ).
fof(f4541,plain,
( ~ arboreal(sK11(sK22,sK24))
| spl25_7 ),
inference(avatar_component_clause,[],[f4540]) ).
fof(f4542,plain,
( arboreal(sK11(sK22,sK24))
| ~ spl25_7 ),
inference(avatar_component_clause,[],[f4540]) ).
fof(f4602,plain,
( ~ legal(sK11(sK22,sK24))
| spl25_7 ),
inference(unit_resulting_resolution,[],[f194,f4541]) ).
fof(f4642,plain,
( ! [X0] : ~ root(sK11(sK22,sK24),X0)
| spl25_7 ),
inference(unit_resulting_resolution,[],[f209,f4602]) ).
fof(f4659,plain,
root(sK11(sK22,sK24),sK22),
inference(unit_resulting_resolution,[],[f234,f335,f298]) ).
fof(f4660,plain,
root(sK11(sK0(sK24),sK24),sK0(sK24)),
inference(unit_resulting_resolution,[],[f234,f354,f315]) ).
fof(f4675,plain,
root(sK11(sK22,sK24),sK22),
inference(forward_demodulation,[],[f4660,f1361]) ).
fof(f4682,plain,
( $false
| spl25_7 ),
inference(forward_subsumption_resolution,[],[f4675,f4642]) ).
fof(f4683,plain,
spl25_7,
inference(avatar_contradiction_clause,[],[f4682]) ).
fof(f7082,plain,
root_occ(sK11(sK22,sK24),sK24),
inference(unit_resulting_resolution,[],[f244,f298,f4659,f4499]) ).
fof(f7861,plain,
! [X2,X0,X1] :
( ~ root_occ(X2,X0)
| ~ occurrence_of(X0,X1)
| sK16(X0) = X2
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f249,f268]) ).
fof(f24630,plain,
root_occ(sK21(tptp0,sK23,sK24),sK24),
inference(unit_resulting_resolution,[],[f294,f298,f299]) ).
fof(f24632,plain,
sK11(sK22,sK24) = sK21(tptp0,sK23,sK24),
inference(unit_resulting_resolution,[],[f249,f298,f7082,f24630]) ).
fof(f30358,plain,
occurrence_of(sK21(tptp0,sK23,sK24),sK18(tptp0,sK23,sK24)),
inference(unit_resulting_resolution,[],[f295,f298,f299]) ).
fof(f30360,plain,
occurrence_of(sK11(sK22,sK24),sK18(tptp0,sK23,sK24)),
inference(forward_demodulation,[],[f30358,f24632]) ).
fof(f30364,plain,
sK0(sK11(sK22,sK24)) = sK18(tptp0,sK23,sK24),
inference(unit_resulting_resolution,[],[f187,f4512,f30360]) ).
fof(f31495,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,[],[f257,f266]) ).
fof(f32414,plain,
send_message(sK18(tptp0,sK23,sK24),sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0),
inference(unit_resulting_resolution,[],[f296,f298,f299]) ).
fof(f32756,plain,
send_message(sK0(sK11(sK22,sK24)),sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0),
inference(forward_demodulation,[],[f32414,f30364]) ).
fof(f34422,plain,
min_precedes(sK23,sK11(sK22,sK24),tptp0),
inference(unit_resulting_resolution,[],[f289,f4512,f32756]) ).
fof(f34451,plain,
subactivity_occurrence(sK11(sK22,sK24),sK9(tptp0,sK23,sK11(sK22,sK24))),
inference(unit_resulting_resolution,[],[f228,f34422]) ).
fof(f34452,plain,
subactivity_occurrence(sK23,sK9(tptp0,sK23,sK11(sK22,sK24))),
inference(unit_resulting_resolution,[],[f229,f34422]) ).
fof(f34453,plain,
occurrence_of(sK9(tptp0,sK23,sK11(sK22,sK24)),tptp0),
inference(unit_resulting_resolution,[],[f230,f34422]) ).
fof(f34893,plain,
root_occ(sK23,sK9(tptp0,sK23,sK11(sK22,sK24))),
inference(unit_resulting_resolution,[],[f244,f376,f34452,f34453]) ).
fof(f51464,plain,
sK23 = sK16(sK9(tptp0,sK23,sK11(sK22,sK24))),
inference(unit_resulting_resolution,[],[f7861,f34453,f34893,f34453]) ).
fof(f51561,plain,
( next_subocc(sK23,sK17(sK9(tptp0,sK23,sK11(sK22,sK24))),tptp0)
| ~ occurrence_of(sK9(tptp0,sK23,sK11(sK22,sK24)),tptp0) ),
inference(superposition,[],[f265,f51464]) ).
fof(f51586,plain,
next_subocc(sK23,sK17(sK9(tptp0,sK23,sK11(sK22,sK24))),tptp0),
inference(forward_subsumption_resolution,[],[f51561,f34453]) ).
fof(f52019,plain,
~ min_precedes(sK11(sK22,sK24),sK17(sK9(tptp0,sK23,sK11(sK22,sK24))),tptp0),
inference(unit_resulting_resolution,[],[f218,f34422,f51586]) ).
fof(f61147,plain,
( sK11(sK22,sK24) = sK17(sK9(tptp0,sK23,sK11(sK22,sK24)))
| ~ spl25_7 ),
inference(unit_resulting_resolution,[],[f31495,f4542,f34453,f34453,f34451,f52019]) ).
fof(f71528,plain,
( occurrence_of(sK11(sK22,sK24),tptp2)
| occurrence_of(sK11(sK22,sK24),tptp3)
| ~ occurrence_of(sK9(tptp0,sK23,sK11(sK22,sK24)),tptp0)
| ~ spl25_7 ),
inference(superposition,[],[f267,f61147]) ).
fof(f71543,plain,
( occurrence_of(sK11(sK22,sK24),tptp2)
| occurrence_of(sK11(sK22,sK24),tptp3)
| ~ spl25_7 ),
inference(forward_subsumption_resolution,[],[f71528,f34453]) ).
fof(f71885,definition,
( spl25_27
<=> occurrence_of(sK11(sK22,sK24),tptp3) ),
introduced(definition,[new_symbols(definition,[spl25_27])],[avatar_definition]) ).
fof(f71887,plain,
( occurrence_of(sK11(sK22,sK24),tptp3)
| ~ spl25_27 ),
inference(avatar_component_clause,[],[f71885]) ).
fof(f71889,definition,
( spl25_28
<=> occurrence_of(sK11(sK22,sK24),tptp2) ),
introduced(definition,[new_symbols(definition,[spl25_28])],[avatar_definition]) ).
fof(f71891,plain,
( occurrence_of(sK11(sK22,sK24),tptp2)
| ~ spl25_28 ),
inference(avatar_component_clause,[],[f71889]) ).
fof(f71892,plain,
( spl25_27
| spl25_28
| ~ spl25_7 ),
inference(avatar_split_clause,[],[f71543,f4540,f71889,f71885]) ).
fof(f71893,plain,
( tptp3 = sK0(sK11(sK22,sK24))
| ~ spl25_27 ),
inference(unit_resulting_resolution,[],[f4523,f71887]) ).
fof(f72103,plain,
( send_message(tptp3,sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0)
| ~ spl25_27 ),
inference(superposition,[],[f32756,f71893]) ).
fof(f72122,plain,
( $false
| ~ spl25_27 ),
inference(forward_subsumption_resolution,[],[f72103,f301]) ).
fof(f72123,plain,
~ spl25_27,
inference(avatar_contradiction_clause,[],[f72122]) ).
fof(f72124,plain,
( tptp2 = sK0(sK11(sK22,sK24))
| ~ spl25_28 ),
inference(unit_resulting_resolution,[],[f4523,f71891]) ).
fof(f72691,plain,
( send_message(tptp2,sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0)
| ~ spl25_28 ),
inference(superposition,[],[f32756,f72124]) ).
fof(f72710,plain,
( $false
| ~ spl25_28 ),
inference(forward_subsumption_resolution,[],[f72691,f302]) ).
fof(f72711,plain,
~ spl25_28,
inference(avatar_contradiction_clause,[],[f72710]) ).
cnf(s19,plain,
spl25_7,
inference(sat_conversion,[],[f4683]) ).
cnf(s52,plain,
( ~ spl25_7
| spl25_27
| spl25_28 ),
inference(sat_conversion,[],[f71892]) ).
cnf(s54,plain,
~ spl25_27,
inference(sat_conversion,[],[f72123]) ).
cnf(s55,plain,
~ spl25_28,
inference(sat_conversion,[],[f72711]) ).
cnf(s56,plain,
~ spl25_7,
inference(rat,[],[s52,s55,s54]) ).
cnf(s59,plain,
$false,
inference(rat,[],[s19,s56]) ).
fof(f72712,plain,
$false,
inference(avatar_sat_refutation,[],[s59]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO002+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n004.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 22:16:07 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 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
% 15.49/2.67 % (3937830)Will run a generic schedule for satisfiability detection.
% 15.49/2.67 % (3937839)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1807929906:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.49/2.67 % (3937836)% WARNING: option uhcvi not known.
% 15.49/2.67 % (3937836)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=964141203:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.49/2.67 % (3937835)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1316933945_2999 on theBenchmark for (2999ds/0Mi)
% 15.49/2.67 % (3937837)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=304810112:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.49/2.67 % (3937838)dis+10_1_sil=32000:sp=arity:random_seed=2287326825:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.49/2.67 % (3937840)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1434310007:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.49/2.67 % (3937841)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=237776178:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.49/2.67 % Detected minimum model sizes of [4]
% 15.49/2.67 % Detected maximum model sizes of [max]
% 15.49/2.67 % TRYING [4]
% 15.49/2.67 % (3937839)Instruction limit reached!
% 15.49/2.67 % (3937839)------------------------------
% 15.49/2.67 % (3937839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.49/2.67 % (3937839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/2.67 % (3937839)CaDiCaL version: 2.1.3
% 15.49/2.67 % (3937839)Termination reason: Instruction limit
% 15.49/2.67 % (3937839)Termination phase: Saturation
% 15.49/2.67 % (3937839)Time elapsed: 0.042 s
% 15.49/2.67 % (3937839)Peak memory usage: 12 MB
% 15.49/2.67 % (3937839)Instructions burned: 119 (million)
% 15.49/2.67 % TRYING [5]
% 15.49/2.67 % (3937849)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2119256251:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.49/2.67 % Detected minimum model sizes of [4]
% 15.49/2.67 % Detected maximum model sizes of [max]
% 15.49/2.67 % TRYING [4]
% 15.49/2.67 % TRYING [5]
% 15.49/2.67 % (3937838)Instruction limit reached!
% 15.49/2.67 % (3937838)------------------------------
% 15.49/2.67 % (3937838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.49/2.67 % (3937838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/2.67 % (3937838)CaDiCaL version: 2.1.3
% 15.49/2.67 % (3937838)Termination reason: Instruction limit
% 15.49/2.67 % (3937838)Termination phase: Saturation
% 15.49/2.67 % (3937838)Time elapsed: 0.070 s
% 15.49/2.67 % (3937838)Peak memory usage: 12 MB
% 15.49/2.67 % (3937838)Instructions burned: 103 (million)
% 15.49/2.67 % (3937851)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2794152236:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.49/2.67 % (3937840)Instruction limit reached!
% 15.49/2.67 % (3937840)------------------------------
% 15.49/2.67 % (3937840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.49/2.67 % (3937840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/2.67 % (3937840)CaDiCaL version: 2.1.3
% 15.49/2.67 % (3937840)Termination reason: Instruction limit
% 15.49/2.67 % (3937840)Termination phase: Saturation
% 15.49/2.67 % (3937840)Time elapsed: 0.092 s
% 15.49/2.67 % (3937840)Peak memory usage: 13 MB
% 15.49/2.67 % (3937840)Instructions burned: 131 (million)
% 15.49/2.67 % (3937841)Instruction limit reached!
% 15.49/2.67 % (3937841)------------------------------
% 15.49/2.67 % (3937841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.49/2.67 % (3937841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.49/2.67 % (3937841)CaDiCaL version: 2.1.3
% 15.49/2.67 % (3937841)Termination reason: Instruction limit
% 15.49/2.67 % (3937841)Termination phase: Saturation
% 15.49/2.67 % (3937841)Time elapsed: 0.110 s
% 15.49/2.67 % (3937841)Peak memory usage: 14 MB
% 15.49/2.67 % (3937841)Instructions burned: 159 (million)
% 15.49/2.67 % (3937853)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=3836196434:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.49/2.67 % TRYING [6]
% 15.49/2.67 % TRYING [6]
% 15.49/2.67 % (3937854)ott-21_1_sil=16000:fs=off:random_seed=3821073083:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.49/2.67 % (3937851)Instruction limit reached!
% 15.49/2.67 % (3937851)------------------------------
% 26.12/4.77 % (3937851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.12/4.77 % (3937851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.12/4.77 % (3937851)CaDiCaL version: 2.1.3
% 26.12/4.77 % (3937851)Termination reason: Instruction limit
% 26.12/4.77 % (3937851)Termination phase: Saturation
% 26.12/4.77 % (3937851)Time elapsed: 0.090 s
% 26.12/4.77 % (3937851)Peak memory usage: 13 MB
% 26.12/4.77 % (3937851)Instructions burned: 131 (million)
% 26.12/4.77 % (3937849)Instruction limit reached!
% 26.12/4.77 % (3937849)------------------------------
% 26.12/4.77 % (3937849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.12/4.77 % (3937849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.12/4.77 % (3937849)CaDiCaL version: 2.1.3
% 26.12/4.77 % (3937849)Termination reason: Instruction limit
% 26.12/4.77 % (3937849)Termination phase: Finite model building constraint generation
% 26.12/4.77 % (3937849)Time elapsed: 0.152 s
% 26.12/4.77 % (3937849)Peak memory usage: 42 MB
% 26.12/4.77 % (3937849)Instructions burned: 717 (million)
% 26.12/4.77 % (3937857)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1108073954:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 26.12/4.77 % (3937859)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=589769167:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 26.12/4.77 % Detected minimum model sizes of [4]
% 26.12/4.77 % Detected maximum model sizes of [max]
% 26.12/4.77 % TRYING [4]
% 26.12/4.77 % (3937854)Instruction limit reached!
% 26.12/4.77 % (3937854)------------------------------
% 26.12/4.77 % (3937854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.12/4.77 % (3937854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.12/4.77 % (3937854)CaDiCaL version: 2.1.3
% 26.12/4.77 % (3937854)Termination reason: Instruction limit
% 26.12/4.77 % (3937854)Termination phase: Saturation
% 26.12/4.77 % (3937854)Time elapsed: 0.103 s
% 26.12/4.77 % (3937854)Peak memory usage: 13 MB
% 26.12/4.77 % (3937854)Instructions burned: 181 (million)
% 26.12/4.77 % TRYING [5]
% 26.12/4.77 % (3937861)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=287336572:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 26.12/4.77 % TRYING [6]
% 26.12/4.77 % TRYING [7]
% 26.12/4.77 % (3937859)Instruction limit reached!
% 26.12/4.77 % (3937859)------------------------------
% 26.12/4.77 % (3937859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.12/4.77 % (3937859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.12/4.77 % (3937859)CaDiCaL version: 2.1.3
% 26.12/4.77 % (3937859)Termination reason: Instruction limit
% 26.12/4.77 % (3937859)Termination phase: Finite model building SAT solving
% 26.12/4.77 % (3937859)Time elapsed: 0.173 s
% 26.12/4.77 % (3937859)Peak memory usage: 32 MB
% 26.12/4.77 % (3937859)Instructions burned: 866 (million)
% 26.12/4.77 % (3937863)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1988965966:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 26.12/4.77 % (3937853)Instruction limit reached!
% 26.12/4.77 % (3937853)------------------------------
% 26.12/4.77 % (3937853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.12/4.77 % (3937853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.12/4.77 % (3937853)CaDiCaL version: 2.1.3
% 26.12/4.77 % (3937853)Termination reason: Instruction limit
% 26.12/4.77 % (3937853)Termination phase: Saturation
% 26.12/4.77 % (3937853)Time elapsed: 0.432 s
% 26.12/4.77 % (3937853)Peak memory usage: 20 MB
% 26.12/4.77 % (3937853)Instructions burned: 685 (million)
% 26.12/4.77 % (3937857)Instruction limit reached!
% 26.12/4.77 % (3937857)------------------------------
% 26.12/4.77 % (3937857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.12/4.77 % (3937857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.12/4.77 % (3937857)CaDiCaL version: 2.1.3
% 26.12/4.77 % (3937857)Termination reason: Instruction limit
% 26.12/4.77 % (3937857)Termination phase: Saturation
% 26.12/4.77 % (3937857)Time elapsed: 0.346 s
% 26.12/4.77 % (3937857)Peak memory usage: 15 MB
% 26.12/4.77 % (3937857)Instructions burned: 477 (million)
% 26.12/4.77 % (3937865)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=4094723135: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)
% 26.12/4.77 % (3937866)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2067767342:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 57.14/8.53 % (3937863)Instruction limit reached!
% 57.14/8.53 % (3937863)------------------------------
% 57.14/8.53 % (3937863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.14/8.53 % (3937863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.14/8.53 % (3937863)CaDiCaL version: 2.1.3
% 57.14/8.53 % (3937863)Termination reason: Instruction limit
% 57.14/8.53 % (3937863)Termination phase: Finite model building constraint generation
% 57.14/8.53 % (3937863)Time elapsed: 0.230 s
% 57.14/8.53 % (3937863)Peak memory usage: 108 MB
% 57.14/8.53 % (3937863)Instructions burned: 890 (million)
% 57.14/8.53 % (3937869)fmb+10_1_sil=64000:random_seed=4176495716:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 57.14/8.53 % Detected minimum model sizes of [4]
% 57.14/8.53 % Detected maximum model sizes of [max]
% 57.14/8.53 % TRYING [4]
% 57.14/8.53 % TRYING [5]
% 57.14/8.53 % TRYING [6]
% 57.14/8.53 % TRYING [8]
% 57.14/8.53 % (3937865)Instruction limit reached!
% 57.14/8.53 % (3937865)------------------------------
% 57.14/8.53 % (3937865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.14/8.53 % (3937865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.14/8.53 % (3937865)CaDiCaL version: 2.1.3
% 57.14/8.53 % (3937865)Termination reason: Instruction limit
% 57.14/8.53 % (3937865)Termination phase: Saturation
% 57.14/8.53 % (3937865)Time elapsed: 0.385 s
% 57.14/8.53 % (3937865)Peak memory usage: 19 MB
% 57.14/8.53 % (3937865)Instructions burned: 695 (million)
% 57.14/8.53 % TRYING [7]
% 57.14/8.53 % (3937871)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1844388281:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 57.14/8.53 % Detected minimum model sizes of [4]
% 57.14/8.53 % Detected maximum model sizes of [max]
% 57.14/8.53 % TRYING [20]
% 57.14/8.53 % (3937861)Instruction limit reached!
% 57.14/8.53 % (3937861)------------------------------
% 57.14/8.53 % (3937861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.14/8.53 % (3937861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.14/8.53 % (3937861)CaDiCaL version: 2.1.3
% 57.14/8.53 % (3937861)Termination reason: Instruction limit
% 57.14/8.53 % (3937861)Termination phase: Saturation
% 57.14/8.53 % (3937861)Time elapsed: 0.728 s
% 57.14/8.53 % (3937861)Peak memory usage: 26 MB
% 57.14/8.53 % (3937861)Instructions burned: 1179 (million)
% 57.14/8.53 % (3937873)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3650565343:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 57.14/8.53 % Detected minimum model sizes of [4]
% 57.14/8.53 % Detected maximum model sizes of [max]
% 57.14/8.53 % TRYING [8]
% 57.14/8.53 % (3937866)Instruction limit reached!
% 57.14/8.53 % (3937866)------------------------------
% 57.14/8.53 % (3937866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.14/8.53 % (3937866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.14/8.53 % (3937866)CaDiCaL version: 2.1.3
% 57.14/8.53 % (3937866)Termination reason: Instruction limit
% 57.14/8.53 % (3937866)Termination phase: Saturation
% 57.14/8.53 % (3937866)Time elapsed: 0.497 s
% 57.14/8.53 % (3937866)Peak memory usage: 18 MB
% 57.14/8.53 % (3937866)Instructions burned: 880 (million)
% 57.14/8.53 % (3937875)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2232934885:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 57.14/8.53 % (3937873)Instruction limit reached!
% 57.14/8.53 % (3937873)------------------------------
% 57.14/8.53 % (3937873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.14/8.53 % (3937873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.14/8.53 % (3937873)CaDiCaL version: 2.1.3
% 57.14/8.53 % (3937873)Termination reason: Instruction limit
% 57.14/8.53 % (3937873)Termination phase: Finite model building constraint generation
% 57.14/8.53 % (3937873)Time elapsed: 0.364 s
% 57.14/8.53 % (3937873)Peak memory usage: 85 MB
% 57.14/8.53 % (3937873)Instructions burned: 921 (million)
% 57.14/8.53 % (3937877)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=327316671:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 57.14/8.53 % TRYING [8]
% 57.14/8.53 % (3937877)Instruction limit reached!
% 57.14/8.53 % (3937877)------------------------------
% 57.14/8.53 % (3937877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.14/8.53 % (3937877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.14/8.53 % (3937877)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937877)Termination reason: Instruction limit
% 128.39/18.60 % (3937877)Termination phase: Saturation
% 128.39/18.60 % (3937877)Time elapsed: 0.823 s
% 128.39/18.60 % (3937877)Peak memory usage: 29 MB
% 128.39/18.60 % (3937877)Instructions burned: 1472 (million)
% 128.39/18.60 % (3937880)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4212244445:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 128.39/18.60 % Detected minimum model sizes of [4]
% 128.39/18.60 % Detected maximum model sizes of [max]
% 128.39/18.60 % (3937880)Cannot represent all propositional literals internally
% 128.39/18.60 % (3937880)Refutation not found, incomplete strategy
% 128.39/18.60 % (3937880)------------------------------
% 128.39/18.60 % (3937880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937880)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937880)Termination reason: Refutation not found, incomplete strategy
% 128.39/18.60 % (3937880)Time elapsed: 0.006 s
% 128.39/18.60 % (3937880)Peak memory usage: 11 MB
% 128.39/18.60 % (3937880)Instructions burned: 10 (million)
% 128.39/18.60 % (3937880)------------------------------
% 128.39/18.60 % (3937880)------------------------------
% 128.39/18.60 % (3937882)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=864474737:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 128.39/18.60 % Detected minimum model sizes of [4]
% 128.39/18.60 % Detected maximum model sizes of [max]
% 128.39/18.60 % TRYING [16]
% 128.39/18.60 % TRYING [9]
% 128.39/18.60 % (3937882)Instruction limit reached!
% 128.39/18.60 % (3937882)------------------------------
% 128.39/18.60 % (3937882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937882)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937882)Termination reason: Instruction limit
% 128.39/18.60 % (3937882)Termination phase: Finite model building constraint generation
% 128.39/18.60 % (3937882)Time elapsed: 0.747 s
% 128.39/18.60 % (3937882)Peak memory usage: 132 MB
% 128.39/18.60 % (3937882)Instructions burned: 2176 (million)
% 128.39/18.60 % (3937884)ott-2_1_sil=16000:newcnf=on:random_seed=4255322144:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2969 on theBenchmark for (2969ds/869Mi)
% 128.39/18.60 % TRYING [9]
% 128.39/18.60 % (3937884)Instruction limit reached!
% 128.39/18.60 % (3937884)------------------------------
% 128.39/18.60 % (3937884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937884)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937884)Termination reason: Instruction limit
% 128.39/18.60 % (3937884)Termination phase: Saturation
% 128.39/18.60 % (3937884)Time elapsed: 0.533 s
% 128.39/18.60 % (3937884)Peak memory usage: 15 MB
% 128.39/18.60 % (3937884)Instructions burned: 870 (million)
% 128.39/18.60 % (3937886)ott+10_1_sil=32000:tgt=ground:random_seed=339669081:i=5114:av=off_2963 on theBenchmark for (2963ds/5114Mi)
% 128.39/18.60 % (3937875)Instruction limit reached!
% 128.39/18.60 % (3937875)------------------------------
% 128.39/18.60 % (3937875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937875)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937875)Termination reason: Instruction limit
% 128.39/18.60 % (3937875)Termination phase: Saturation
% 128.39/18.60 % (3937875)Time elapsed: 2.889 s
% 128.39/18.60 % (3937875)Peak memory usage: 24 MB
% 128.39/18.60 % (3937875)Instructions burned: 5131 (million)
% 128.39/18.60 % (3937888)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2537524392:i=54282_2959 on theBenchmark for (2959ds/54282Mi)
% 128.39/18.60 % Detected minimum model sizes of [4]
% 128.39/18.60 % Detected maximum model sizes of [max]
% 128.39/18.60 % TRYING [4]
% 128.39/18.60 % TRYING [5]
% 128.39/18.60 % TRYING [6]
% 128.39/18.60 % (3937871)Instruction limit reached!
% 128.39/18.60 % (3937871)------------------------------
% 128.39/18.60 % (3937871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937871)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937871)Termination reason: Instruction limit
% 128.39/18.60 % (3937871)Termination phase: Finite model building constraint generation
% 128.39/18.60 % (3937871)Time elapsed: 3.273 s
% 128.39/18.60 % (3937871)Peak memory usage: 513 MB
% 128.39/18.60 % (3937871)Instructions burned: 9516 (million)
% 128.39/18.60 % TRYING [7]
% 128.39/18.60 % (3937890)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4053188895:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi)
% 128.39/18.60 % TRYING [8]
% 128.39/18.60 % TRYING [10]
% 128.39/18.60 % (3937869)Instruction limit reached!
% 128.39/18.60 % (3937869)------------------------------
% 128.39/18.60 % (3937869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937869)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937869)Termination reason: Instruction limit
% 128.39/18.60 % (3937869)Termination phase: Finite model building constraint generation
% 128.39/18.60 % (3937869)Time elapsed: 5.354 s
% 128.39/18.60 % (3937869)Peak memory usage: 214 MB
% 128.39/18.60 % (3937869)Instructions burned: 22061 (million)
% 128.39/18.60 % (3937892)dis+21_1_sil=32000:sas=cadical:random_seed=3404593314:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi)
% 128.39/18.60 % (3937890)Instruction limit reached!
% 128.39/18.60 % (3937890)------------------------------
% 128.39/18.60 % (3937890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937890)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937890)Termination reason: Instruction limit
% 128.39/18.60 % (3937890)Termination phase: Saturation
% 128.39/18.60 % (3937890)Time elapsed: 2.097 s
% 128.39/18.60 % (3937890)Peak memory usage: 23 MB
% 128.39/18.60 % (3937890)Instructions burned: 3513 (million)
% 128.39/18.60 % (3937894)ott+11_1_sil=16000:gs=on:random_seed=3018118803:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2935 on theBenchmark for (2935ds/2251Mi)
% 128.39/18.60 % (3937886)Instruction limit reached!
% 128.39/18.60 % (3937886)------------------------------
% 128.39/18.60 % (3937886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937886)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937886)Termination reason: Instruction limit
% 128.39/18.60 % (3937886)Termination phase: Saturation
% 128.39/18.60 % (3937886)Time elapsed: 3.192 s
% 128.39/18.60 % (3937886)Peak memory usage: 39 MB
% 128.39/18.60 % (3937886)Instructions burned: 5115 (million)
% 128.39/18.60 % TRYING [9]
% 128.39/18.60 % (3937896)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=725059070:fmbsr=1.6:i=67534_2931 on theBenchmark for (2931ds/67534Mi)
% 128.39/18.60 % Detected minimum model sizes of [4]
% 128.39/18.60 % Detected maximum model sizes of [max]
% 128.39/18.60 % TRYING [7]
% 128.39/18.60 % (3937892)Instruction limit reached!
% 128.39/18.60 % (3937892)------------------------------
% 128.39/18.60 % (3937892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937892)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937892)Termination reason: Instruction limit
% 128.39/18.60 % (3937892)Termination phase: Saturation
% 128.39/18.60 % (3937892)Time elapsed: 1.269 s
% 128.39/18.60 % (3937892)Peak memory usage: 31 MB
% 128.39/18.60 % (3937892)Instructions burned: 3773 (million)
% 128.39/18.60 % (3937898)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3436801707:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2926 on theBenchmark for (2926ds/4591Mi)
% 128.39/18.60 % TRYING [8]
% 128.39/18.60 % (3937894)Instruction limit reached!
% 128.39/18.60 % (3937894)------------------------------
% 128.39/18.60 % (3937894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937894)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937894)Termination reason: Instruction limit
% 128.39/18.60 % (3937894)Termination phase: Saturation
% 128.39/18.60 % (3937894)Time elapsed: 1.388 s
% 128.39/18.60 % (3937894)Peak memory usage: 27 MB
% 128.39/18.60 % (3937894)Instructions burned: 2251 (million)
% 128.39/18.60 % (3937900)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1032721943:i=29340_2921 on theBenchmark for (2921ds/29340Mi)
% 128.39/18.60 % (3937898)Instruction limit reached!
% 128.39/18.60 % (3937898)------------------------------
% 128.39/18.60 % (3937898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937898)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937898)Termination reason: Instruction limit
% 128.39/18.60 % (3937898)Termination phase: Saturation
% 128.39/18.60 % (3937898)Time elapsed: 0.772 s
% 128.39/18.60 % (3937898)Peak memory usage: 12 MB
% 128.39/18.60 % (3937898)Instructions burned: 4594 (million)
% 128.39/18.60 % (3937902)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3146364316:i=5211_2918 on theBenchmark for (2918ds/5211Mi)
% 128.39/18.60 % (3937902)Instruction limit reached!
% 128.39/18.60 % (3937902)------------------------------
% 128.39/18.60 % (3937902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937902)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937902)Termination reason: Instruction limit
% 128.39/18.60 % (3937902)Termination phase: Saturation
% 128.39/18.60 % (3937902)Time elapsed: 1.521 s
% 128.39/18.60 % (3937902)Peak memory usage: 41 MB
% 128.39/18.60 % (3937902)Instructions burned: 5213 (million)
% 128.39/18.60 % (3937904)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3665013619:i=5497:nm=2_2903 on theBenchmark for (2903ds/5497Mi)
% 128.39/18.60 % Detected minimum model sizes of [4]
% 128.39/18.60 % Detected maximum model sizes of [max]
% 128.39/18.60 % TRYING [17]
% 128.39/18.60 % TRYING [9]
% 128.39/18.60 % (3937904)Instruction limit reached!
% 128.39/18.60 % (3937904)------------------------------
% 128.39/18.60 % (3937904)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937904)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937904)Termination reason: Instruction limit
% 128.39/18.60 % (3937904)Termination phase: Finite model building constraint generation
% 128.39/18.60 % (3937904)Time elapsed: 1.052 s
% 128.39/18.60 % (3937904)Peak memory usage: 314 MB
% 128.39/18.60 % (3937904)Instructions burned: 5500 (million)
% 128.39/18.60 % (3937906)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1705033411:fmbsr=2:i=46332_2892 on theBenchmark for (2892ds/46332Mi)
% 128.39/18.60 % Detected minimum model sizes of [4]
% 128.39/18.60 % Detected maximum model sizes of [max]
% 128.39/18.60 % TRYING [15]
% 128.39/18.60 % TRYING [10]
% 128.39/18.60 % TRYING [10]
% 128.39/18.60 % TRYING [10]
% 128.39/18.60 % (3937900) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3937830-3937900"...
% 128.39/18.60 % (3937900)...printing done.
% 128.39/18.60 % (3937900)Refutation found. Thanks to Tanya!
% 128.39/18.60 % SZS status Theorem for theBenchmark
% 128.39/18.60 % SZS output start Proof for theBenchmark
% See solution above
% 128.39/18.60 % (3937900)------------------------------
% 128.39/18.60 % (3937900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 128.39/18.60 % (3937900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.39/18.60 % (3937900)CaDiCaL version: 2.1.3
% 128.39/18.60 % (3937900)Termination reason: Refutation
% 128.39/18.60 % (3937900)Time elapsed: 10.136 s
% 128.39/18.60 % (3937900)Peak memory usage: 30 MB
% 128.39/18.60 % (3937900)Instructions burned: 19884 (million)
% 128.39/18.60 % (3937830)Success in time 18.179 s
% 128.39/18.60 % Vampire exiting
%------------------------------------------------------------------------------