%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRO006+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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:30:35 PM UTC 2026
% Result : Theorem 38.23s 12.32s
% Output : Refutation 38.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 18
% Syntax : Number of formulae : 137 ( 33 unt; 1 def)
% Number of atoms : 408 ( 20 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 460 ( 189 ~; 189 |; 65 &)
% ( 6 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 2 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 211 ( 0 sgn 188 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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) ).
fof(f3,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_02) ).
fof(f7,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_06) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_08) ).
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(f14,axiom,
! [X0] :
( legal(X0)
=> arboreal(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_13) ).
fof(f17,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_16) ).
fof(f18,axiom,
! [X0,X1] :
( root(X0,X1)
=> legal(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_17) ).
fof(f20,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_19) ).
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(f30,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_29) ).
fof(f33,axiom,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( occurrence_of(X1,tptp4)
& root_occ(X1,X0)
& occurrence_of(X2,tptp3)
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_32) ).
fof(f35,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_34) ).
fof(f39,axiom,
atomic(tptp1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_38) ).
fof(f43,axiom,
tptp1 != tptp3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_42) ).
fof(f46,axiom,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_45) ).
fof(f47,conjecture,
~ ? [X0] : occurrence_of(X0,tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f48,negated_conjecture,
~ ~ ? [X0] : occurrence_of(X0,tptp0),
inference(negated_conjecture,[status(cth)],[f47]) ).
fof(f49,plain,
? [X0] : occurrence_of(X0,tptp0),
inference(flattening,[],[f48]) ).
fof(f56,plain,
! [X0,X1] :
( ? [X2] :
( root(X2,X0)
& subactivity_occurrence(X2,X1) )
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f57,plain,
! [X0,X1] :
( ? [X2] :
( root(X2,X0)
& subactivity_occurrence(X2,X1) )
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(flattening,[],[f56]) ).
fof(f60,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,[],[f3]) ).
fof(f61,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,[],[f60]) ).
fof(f66,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,[],[f7]) ).
fof(f69,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f9]) ).
fof(f70,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f69]) ).
fof(f71,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f72,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(flattening,[],[f71]) ).
fof(f77,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f80,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f81,plain,
! [X0,X1] :
( legal(X0)
| ~ root(X0,X1) ),
inference(ennf_transformation,[],[f18]) ).
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(f92,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| ~ root_occ(X1,X2) ),
inference(ennf_transformation,[],[f30]) ).
fof(f93,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| ~ root_occ(X1,X2) ),
inference(flattening,[],[f92]) ).
fof(f98,plain,
! [X0] :
( ? [X1,X2] :
( occurrence_of(X1,tptp4)
& root_occ(X1,X0)
& occurrence_of(X2,tptp3)
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(ennf_transformation,[],[f33]) ).
fof(f99,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f46]) ).
fof(f100,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(flattening,[],[f99]) ).
fof(f101,plain,
! [X0,X1] :
( ( root(sK0(X0,X1),X0)
& subactivity_occurrence(sK0(X0,X1),X1) )
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f57]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK2(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK2(X0,X1,X2))
& subactivity_occurrence(X2,sK2(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X3,sK2(X0,X1,X2))],[f66]) ).
fof(f111,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f80]) ).
fof(f115,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,[],[f20]) ).
fof(f116,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,[],[f115]) ).
fof(f117,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ( occurrence_of(X1,sK9(X0,X1))
& subactivity_occurrence(X0,X1)
& root(X0,sK9(X0,X1)) )
| ~ root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X3,sK9(X0,X1))],[f116]) ).
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] :
( ( occurrence_of(sK12(X0),tptp4)
& root_occ(sK12(X0),X0)
& occurrence_of(sK13(X0),tptp3)
& leaf_occ(sK13(X0),X0)
& next_subocc(sK12(X0),sK13(X0),tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13]),skolemize(X1,sK12(X0)),skolemize(X2,sK13(X0))],[f98]) ).
fof(f126,plain,
! [X0,X1] :
( ( occurrence_of(sK14(X0),tptp1)
& next_subocc(X0,sK14(X0),tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X2,sK14(X0))],[f100]) ).
fof(f127,plain,
occurrence_of(sK15,tptp0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X0,sK15)],[f49]) ).
fof(f128,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| subactivity_occurrence(sK0(X0,X1),X1)
| atomic(X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f129,plain,
! [X0,X1] :
( root(sK0(X0,X1),X0)
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f131,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,[],[f61]) ).
fof(f135,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f136,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X1,sK2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f137,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| occurrence_of(sK2(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f140,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f70]) ).
fof(f141,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(cnf_transformation,[],[f72]) ).
fof(f146,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f153,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ arboreal(X0)
| atomic(X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f154,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f155,plain,
! [X0,X1] :
( ~ root(X0,X1)
| legal(X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f160,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| root(X0,sK9(X0,X1)) ),
inference(cnf_transformation,[],[f117]) ).
fof(f162,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| occurrence_of(X1,sK9(X0,X1)) ),
inference(cnf_transformation,[],[f117]) ).
fof(f163,plain,
! [X2,X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2)
| root_occ(X0,X1)
| ~ root(X0,X2) ),
inference(cnf_transformation,[],[f117]) ).
fof(f174,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(f175,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f124]) ).
fof(f180,plain,
! [X2,X3,X0,X1] :
( ~ root_occ(X1,X2)
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f93]) ).
fof(f183,plain,
! [X0] :
( next_subocc(sK12(X0),sK13(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f184,plain,
! [X0] :
( leaf_occ(sK13(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f185,plain,
! [X0] :
( occurrence_of(sK13(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f186,plain,
! [X0] :
( root_occ(sK12(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f188,plain,
~ atomic(tptp0),
inference(cnf_transformation,[],[f35]) ).
fof(f192,plain,
atomic(tptp1),
inference(cnf_transformation,[],[f39]) ).
fof(f196,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f43]) ).
fof(f199,plain,
! [X0,X1] :
( next_subocc(X0,sK14(X0),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f126]) ).
fof(f200,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK14(X0),tptp1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f126]) ).
fof(f201,plain,
occurrence_of(sK15,tptp0),
inference(cnf_transformation,[],[f127]) ).
fof(f210,plain,
~ arboreal(sK15),
inference(unit_resulting_resolution,[],[f153,f188,f201]) ).
fof(f296,plain,
root_occ(sK12(sK15),sK15),
inference(unit_resulting_resolution,[],[f186,f201]) ).
fof(f384,plain,
root(sK12(sK15),sK9(sK12(sK15),sK15)),
inference(unit_resulting_resolution,[],[f160,f296]) ).
fof(f396,plain,
occurrence_of(sK15,sK9(sK12(sK15),sK15)),
inference(unit_resulting_resolution,[],[f162,f296]) ).
fof(f402,plain,
~ atomic(sK9(sK12(sK15),sK15)),
inference(unit_resulting_resolution,[],[f154,f210,f396]) ).
fof(f433,plain,
tptp0 = sK9(sK12(sK15),sK15),
inference(unit_resulting_resolution,[],[f140,f396,f201]) ).
fof(f508,plain,
root(sK12(sK15),tptp0),
inference(superposition,[],[f384,f433]) ).
fof(f559,plain,
next_subocc(sK12(sK15),sK13(sK15),tptp0),
inference(unit_resulting_resolution,[],[f183,f201]) ).
fof(f563,plain,
min_precedes(sK12(sK15),sK13(sK15),tptp0),
inference(unit_resulting_resolution,[],[f175,f559]) ).
fof(f649,plain,
subactivity_occurrence(sK0(tptp0,sK15),sK15),
inference(unit_resulting_resolution,[],[f128,f188,f201]) ).
fof(f691,definition,
( spl16_5
<=> arboreal(sK0(tptp0,sK15)) ),
introduced(definition,[new_symbols(definition,[spl16_5])],[avatar_definition]) ).
fof(f692,plain,
( ~ arboreal(sK0(tptp0,sK15))
| spl16_5 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f693,plain,
( arboreal(sK0(tptp0,sK15))
| ~ spl16_5 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f717,plain,
( ~ legal(sK0(tptp0,sK15))
| spl16_5 ),
inference(unit_resulting_resolution,[],[f146,f692]) ).
fof(f723,plain,
( ! [X0] : ~ root(sK0(tptp0,sK15),X0)
| spl16_5 ),
inference(unit_resulting_resolution,[],[f155,f717]) ).
fof(f782,plain,
root(sK0(tptp0,sK15),tptp0),
inference(unit_resulting_resolution,[],[f129,f188,f201]) ).
fof(f785,plain,
root(sK0(sK9(sK12(sK15),sK15),sK15),sK9(sK12(sK15),sK15)),
inference(unit_resulting_resolution,[],[f129,f402,f396]) ).
fof(f807,plain,
root(sK0(tptp0,sK15),tptp0),
inference(forward_demodulation,[],[f785,f433]) ).
fof(f824,plain,
( $false
| spl16_5 ),
inference(forward_subsumption_resolution,[],[f807,f723]) ).
fof(f825,plain,
spl16_5,
inference(avatar_contradiction_clause,[],[f824]) ).
fof(f1614,plain,
~ leaf_occ(sK12(sK15),sK15),
inference(unit_resulting_resolution,[],[f141,f201,f563]) ).
fof(f2858,plain,
root_occ(sK0(tptp0,sK15),sK15),
inference(unit_resulting_resolution,[],[f163,f201,f782,f649]) ).
fof(f2876,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK2(X0,X1,X2),X3)
| root_occ(X1,sK2(X0,X1,X2))
| ~ root(X1,X3)
| ~ min_precedes(X1,X2,X0) ),
inference(resolution,[],[f163,f136]) ).
fof(f3174,plain,
sK12(sK15) = sK0(tptp0,sK15),
inference(unit_resulting_resolution,[],[f180,f201,f2858,f296]) ).
fof(f3184,plain,
! [X2,X0,X1] :
( ~ root_occ(X2,X0)
| ~ occurrence_of(X0,X1)
| sK12(X0) = X2
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f180,f186]) ).
fof(f5158,plain,
( ~ occurrence_of(sK15,tptp0)
| occurrence_of(sK14(sK0(tptp0,sK15)),tptp1)
| ~ arboreal(sK0(tptp0,sK15))
| leaf_occ(sK0(tptp0,sK15),sK15) ),
inference(resolution,[],[f200,f649]) ).
fof(f5170,plain,
( occurrence_of(sK14(sK0(tptp0,sK15)),tptp1)
| ~ arboreal(sK0(tptp0,sK15))
| leaf_occ(sK0(tptp0,sK15),sK15) ),
inference(forward_subsumption_resolution,[],[f5158,f201]) ).
fof(f5186,plain,
( occurrence_of(sK14(sK0(tptp0,sK15)),tptp1)
| leaf_occ(sK0(tptp0,sK15),sK15)
| ~ spl16_5 ),
inference(forward_subsumption_resolution,[],[f5170,f693]) ).
fof(f5196,plain,
( occurrence_of(sK14(sK12(sK15)),tptp1)
| leaf_occ(sK0(tptp0,sK15),sK15)
| ~ spl16_5 ),
inference(forward_demodulation,[],[f5186,f3174]) ).
fof(f5205,plain,
( leaf_occ(sK12(sK15),sK15)
| occurrence_of(sK14(sK12(sK15)),tptp1)
| ~ spl16_5 ),
inference(forward_demodulation,[],[f5196,f3174]) ).
fof(f5209,plain,
( occurrence_of(sK14(sK12(sK15)),tptp1)
| ~ spl16_5 ),
inference(forward_subsumption_resolution,[],[f5205,f1614]) ).
fof(f5213,plain,
( ~ occurrence_of(sK14(sK12(sK15)),tptp3)
| ~ spl16_5 ),
inference(unit_resulting_resolution,[],[f140,f196,f5209]) ).
fof(f5220,plain,
( arboreal(sK14(sK12(sK15)))
| ~ spl16_5 ),
inference(unit_resulting_resolution,[],[f154,f192,f5209]) ).
fof(f5328,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0)
| ~ arboreal(X1)
| leaf_occ(X1,X0)
| min_precedes(X1,sK14(X1),tptp0) ),
inference(resolution,[],[f199,f175]) ).
fof(f5534,plain,
! [X2,X0,X1] :
( ~ subactivity_occurrence(X2,X0)
| ~ occurrence_of(X0,X1)
| sK13(X0) = X2
| ~ arboreal(X2)
| min_precedes(X2,sK13(X0),X1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f131,f184]) ).
fof(f9138,plain,
( ~ occurrence_of(sK15,tptp0)
| ~ arboreal(sK0(tptp0,sK15))
| leaf_occ(sK0(tptp0,sK15),sK15)
| min_precedes(sK0(tptp0,sK15),sK14(sK0(tptp0,sK15)),tptp0) ),
inference(resolution,[],[f5328,f649]) ).
fof(f9149,plain,
( ~ arboreal(sK0(tptp0,sK15))
| leaf_occ(sK0(tptp0,sK15),sK15)
| min_precedes(sK0(tptp0,sK15),sK14(sK0(tptp0,sK15)),tptp0) ),
inference(forward_subsumption_resolution,[],[f9138,f201]) ).
fof(f9174,plain,
( leaf_occ(sK0(tptp0,sK15),sK15)
| min_precedes(sK0(tptp0,sK15),sK14(sK0(tptp0,sK15)),tptp0)
| ~ spl16_5 ),
inference(forward_subsumption_resolution,[],[f9149,f693]) ).
fof(f9187,plain,
( leaf_occ(sK12(sK15),sK15)
| min_precedes(sK0(tptp0,sK15),sK14(sK0(tptp0,sK15)),tptp0)
| ~ spl16_5 ),
inference(forward_demodulation,[],[f9174,f3174]) ).
fof(f9198,plain,
( min_precedes(sK0(tptp0,sK15),sK14(sK0(tptp0,sK15)),tptp0)
| ~ spl16_5 ),
inference(forward_subsumption_resolution,[],[f9187,f1614]) ).
fof(f9206,plain,
( min_precedes(sK12(sK15),sK14(sK12(sK15)),tptp0)
| ~ spl16_5 ),
inference(forward_demodulation,[],[f9198,f3174]) ).
fof(f10623,plain,
( subactivity_occurrence(sK14(sK12(sK15)),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ spl16_5 ),
inference(unit_resulting_resolution,[],[f135,f9206]) ).
fof(f10625,plain,
( occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| ~ spl16_5 ),
inference(unit_resulting_resolution,[],[f137,f9206]) ).
fof(f11176,plain,
( root_occ(sK12(sK15),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ root(sK12(sK15),tptp0)
| ~ min_precedes(sK12(sK15),sK14(sK12(sK15)),tptp0)
| ~ spl16_5 ),
inference(resolution,[],[f10625,f2876]) ).
fof(f11190,plain,
( root_occ(sK12(sK15),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ min_precedes(sK12(sK15),sK14(sK12(sK15)),tptp0)
| ~ spl16_5 ),
inference(forward_subsumption_resolution,[],[f11176,f508]) ).
fof(f11204,plain,
( root_occ(sK12(sK15),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ spl16_5 ),
inference(forward_subsumption_resolution,[],[f11190,f9206]) ).
fof(f11644,plain,
( sK12(sK15) = sK12(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ spl16_5 ),
inference(unit_resulting_resolution,[],[f3184,f10625,f10625,f11204]) ).
fof(f13763,plain,
( next_subocc(sK12(sK15),sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),tptp0)
| ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| ~ spl16_5 ),
inference(superposition,[],[f183,f11644]) ).
fof(f13783,plain,
( next_subocc(sK12(sK15),sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),tptp0)
| ~ spl16_5 ),
inference(forward_subsumption_resolution,[],[f13763,f10625]) ).
fof(f14921,plain,
( ~ min_precedes(sK14(sK12(sK15)),sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),tptp0)
| ~ spl16_5 ),
inference(unit_resulting_resolution,[],[f174,f9206,f13783]) ).
fof(f17440,plain,
( sK14(sK12(sK15)) = sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ spl16_5 ),
inference(unit_resulting_resolution,[],[f5534,f5220,f10625,f10625,f10623,f14921]) ).
fof(f17486,plain,
( occurrence_of(sK14(sK12(sK15)),tptp3)
| ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| ~ spl16_5 ),
inference(superposition,[],[f185,f17440]) ).
fof(f17507,plain,
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| ~ spl16_5 ),
inference(forward_subsumption_resolution,[],[f17486,f5213]) ).
fof(f17519,plain,
( $false
| ~ spl16_5 ),
inference(forward_subsumption_resolution,[],[f17507,f10625]) ).
fof(f17520,plain,
~ spl16_5,
inference(avatar_contradiction_clause,[],[f17519]) ).
cnf(s31,plain,
spl16_5,
inference(sat_conversion,[],[f825]) ).
cnf(s92,plain,
~ spl16_5,
inference(sat_conversion,[],[f17520]) ).
cnf(s96,plain,
$false,
inference(rat,[],[s31,s92]) ).
fof(f17524,plain,
$false,
inference(avatar_sat_refutation,[],[s96]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO006+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.38 % Computer : n009.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 22:18:17 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/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
% 16.73/2.94 % (2464479)Will run a generic schedule for satisfiability detection.
% 16.73/2.94 % (2464486)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=114923604:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.73/2.94 % (2464485)% WARNING: option uhcvi not known.
% 16.73/2.94 % (2464484)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3494767127_2999 on theBenchmark for (2999ds/0Mi)
% 16.73/2.94 % (2464485)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3576475207:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.73/2.94 % (2464487)dis+10_1_sil=32000:sp=arity:random_seed=128996912:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.73/2.94 % (2464488)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1906211248:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.73/2.94 % (2464490)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3272060455:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.73/2.94 % (2464489)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1676342313:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.73/2.94 % Detected minimum model sizes of [4]
% 16.73/2.94 % Detected maximum model sizes of [max]
% 16.73/2.94 % TRYING [4]
% 16.73/2.94 % TRYING [5]
% 16.73/2.94 % TRYING [6]
% 16.73/2.94 % (2464487)Instruction limit reached!
% 16.73/2.94 % (2464487)------------------------------
% 16.73/2.94 % (2464487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.73/2.94 % (2464487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.73/2.94 % (2464487)CaDiCaL version: 2.1.3
% 16.73/2.94 % (2464487)Termination reason: Instruction limit
% 16.73/2.94 % (2464487)Termination phase: Saturation
% 16.73/2.94 % (2464487)Time elapsed: 0.072 s
% 16.73/2.94 % (2464487)Peak memory usage: 12 MB
% 16.73/2.94 % (2464487)Instructions burned: 104 (million)
% 16.73/2.94 % (2464488)Instruction limit reached!
% 16.73/2.94 % (2464488)------------------------------
% 16.73/2.94 % (2464488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.73/2.94 % (2464488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.73/2.94 % (2464488)CaDiCaL version: 2.1.3
% 16.73/2.94 % (2464488)Termination reason: Instruction limit
% 16.73/2.94 % (2464488)Termination phase: Saturation
% 16.73/2.94 % (2464488)Time elapsed: 0.075 s
% 16.73/2.94 % (2464488)Peak memory usage: 12 MB
% 16.73/2.94 % (2464488)Instructions burned: 117 (million)
% 16.73/2.94 % TRYING [7]
% 16.73/2.94 % (2464489)Instruction limit reached!
% 16.73/2.94 % (2464489)------------------------------
% 16.73/2.94 % (2464489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.73/2.94 % (2464489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.73/2.94 % (2464489)CaDiCaL version: 2.1.3
% 16.73/2.94 % (2464489)Termination reason: Instruction limit
% 16.73/2.94 % (2464489)Termination phase: Saturation
% 16.73/2.94 % (2464489)Time elapsed: 0.088 s
% 16.73/2.94 % (2464489)Peak memory usage: 13 MB
% 16.73/2.94 % (2464489)Instructions burned: 131 (million)
% 16.73/2.94 % (2464498)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3464673650:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 16.73/2.94 % (2464499)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1833097525:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.73/2.94 % Detected minimum model sizes of [4]
% 16.73/2.94 % Detected maximum model sizes of [max]
% 16.73/2.94 % TRYING [4]
% 16.73/2.94 % TRYING [5]
% 16.73/2.94 % (2464500)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=3263131734:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.73/2.94 % (2464490)Instruction limit reached!
% 16.73/2.94 % (2464490)------------------------------
% 16.73/2.94 % (2464490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.73/2.94 % (2464490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.73/2.94 % (2464490)CaDiCaL version: 2.1.3
% 16.73/2.94 % (2464490)Termination reason: Instruction limit
% 16.73/2.94 % (2464490)Termination phase: Saturation
% 16.73/2.94 % (2464490)Time elapsed: 0.112 s
% 16.73/2.94 % (2464490)Peak memory usage: 14 MB
% 16.73/2.94 % (2464490)Instructions burned: 159 (million)
% 16.73/2.94 % TRYING [6]
% 16.73/2.94 % (2464504)ott-21_1_sil=16000:fs=off:random_seed=2090889476:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.73/2.94 % (2464499)Instruction limit reached!
% 42.43/6.42 % (2464499)------------------------------
% 42.43/6.42 % (2464499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.43/6.42 % (2464499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.43/6.42 % (2464499)CaDiCaL version: 2.1.3
% 42.43/6.42 % (2464499)Termination reason: Instruction limit
% 42.43/6.42 % (2464499)Termination phase: Saturation
% 42.43/6.42 % (2464499)Time elapsed: 0.090 s
% 42.43/6.42 % (2464499)Peak memory usage: 13 MB
% 42.43/6.42 % (2464499)Instructions burned: 132 (million)
% 42.43/6.42 % TRYING [7]
% 42.43/6.42 % (2464506)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3537394904:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 42.43/6.42 % (2464504)Instruction limit reached!
% 42.43/6.42 % (2464504)------------------------------
% 42.43/6.42 % (2464504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.43/6.42 % (2464504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.43/6.42 % (2464504)CaDiCaL version: 2.1.3
% 42.43/6.42 % (2464504)Termination reason: Instruction limit
% 42.43/6.42 % (2464504)Termination phase: Saturation
% 42.43/6.42 % (2464504)Time elapsed: 0.099 s
% 42.43/6.42 % (2464504)Peak memory usage: 13 MB
% 42.43/6.42 % (2464504)Instructions burned: 181 (million)
% 42.43/6.42 % TRYING [8]
% 42.43/6.42 % (2464508)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2306333970:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 42.43/6.42 % Detected minimum model sizes of [4]
% 42.43/6.42 % Detected maximum model sizes of [max]
% 42.43/6.42 % TRYING [4]
% 42.43/6.42 % TRYING [5]
% 42.43/6.42 % TRYING [6]
% 42.43/6.42 % TRYING [8]
% 42.43/6.42 % (2464498)Instruction limit reached!
% 42.43/6.42 % (2464498)------------------------------
% 42.43/6.42 % (2464498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.43/6.42 % (2464498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.43/6.42 % (2464498)CaDiCaL version: 2.1.3
% 42.43/6.42 % (2464498)Termination reason: Instruction limit
% 42.43/6.42 % (2464498)Termination phase: Finite model building constraint generation
% 42.43/6.42 % (2464498)Time elapsed: 0.305 s
% 42.43/6.42 % (2464498)Peak memory usage: 26 MB
% 42.43/6.42 % (2464498)Instructions burned: 714 (million)
% 42.43/6.42 % TRYING [7]
% 42.43/6.42 % (2464510)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2138761486:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 42.43/6.42 % (2464500)Instruction limit reached!
% 42.43/6.42 % (2464500)------------------------------
% 42.43/6.42 % (2464500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.43/6.42 % (2464500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.43/6.42 % (2464500)CaDiCaL version: 2.1.3
% 42.43/6.42 % (2464500)Termination reason: Instruction limit
% 42.43/6.42 % (2464500)Termination phase: Saturation
% 42.43/6.42 % (2464500)Time elapsed: 0.395 s
% 42.43/6.42 % (2464500)Peak memory usage: 20 MB
% 42.43/6.42 % (2464500)Instructions burned: 684 (million)
% 42.43/6.42 % (2464512)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=619382153:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 42.43/6.42 % (2464506)Instruction limit reached!
% 42.43/6.42 % (2464506)------------------------------
% 42.43/6.42 % (2464506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.43/6.42 % (2464506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.43/6.42 % (2464506)CaDiCaL version: 2.1.3
% 42.43/6.42 % (2464506)Termination reason: Instruction limit
% 42.43/6.42 % (2464506)Termination phase: Saturation
% 42.43/6.42 % (2464506)Time elapsed: 0.337 s
% 42.43/6.42 % (2464506)Peak memory usage: 15 MB
% 42.43/6.42 % (2464506)Instructions burned: 477 (million)
% 42.43/6.42 % (2464514)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=1521018129: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)
% 42.43/6.42 % (2464508)Instruction limit reached!
% 42.43/6.42 % (2464508)------------------------------
% 42.43/6.42 % (2464508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.43/6.42 % (2464508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.43/6.42 % (2464508)CaDiCaL version: 2.1.3
% 42.43/6.42 % (2464508)Termination reason: Instruction limit
% 42.43/6.42 % (2464508)Termination phase: Finite model building SAT solving
% 42.43/6.42 % (2464508)Time elapsed: 0.328 s
% 42.43/6.42 % (2464508)Peak memory usage: 21 MB
% 42.43/6.42 % (2464508)Instructions burned: 867 (million)
% 38.23/12.31 % TRYING [14]
% 38.23/12.31 % TRYING [9]
% 38.23/12.31 % (2464516)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2237991372:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 38.23/12.31 % (2464512)Instruction limit reached!
% 38.23/12.31 % (2464512)------------------------------
% 38.23/12.31 % (2464512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.31 % (2464512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.31 % (2464512)CaDiCaL version: 2.1.3
% 38.23/12.31 % (2464512)Termination reason: Instruction limit
% 38.23/12.31 % (2464512)Termination phase: Finite model building constraint generation
% 38.23/12.31 % (2464512)Time elapsed: 0.337 s
% 38.23/12.31 % (2464512)Peak memory usage: 75 MB
% 38.23/12.31 % (2464512)Instructions burned: 890 (million)
% 38.23/12.31 % (2464518)fmb+10_1_sil=64000:random_seed=1949667864:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 38.23/12.31 % Detected minimum model sizes of [4]
% 38.23/12.31 % Detected maximum model sizes of [max]
% 38.23/12.31 % TRYING [4]
% 38.23/12.31 % TRYING [5]
% 38.23/12.31 % (2464514)Instruction limit reached!
% 38.23/12.31 % (2464514)------------------------------
% 38.23/12.31 % (2464514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.31 % (2464514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.31 % (2464514)CaDiCaL version: 2.1.3
% 38.23/12.31 % (2464514)Termination reason: Instruction limit
% 38.23/12.31 % (2464514)Termination phase: Saturation
% 38.23/12.31 % (2464514)Time elapsed: 0.373 s
% 38.23/12.31 % (2464514)Peak memory usage: 19 MB
% 38.23/12.31 % (2464514)Instructions burned: 694 (million)
% 38.23/12.31 % TRYING [6]
% 38.23/12.31 % (2464520)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=490986605:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 38.23/12.31 % Detected minimum model sizes of [4]
% 38.23/12.31 % Detected maximum model sizes of [max]
% 38.23/12.31 % TRYING [20]
% 38.23/12.31 % TRYING [7]
% 38.23/12.31 % (2464510)Instruction limit reached!
% 38.23/12.31 % (2464510)------------------------------
% 38.23/12.31 % (2464510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.31 % (2464510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.31 % (2464510)CaDiCaL version: 2.1.3
% 38.23/12.31 % (2464510)Termination reason: Instruction limit
% 38.23/12.31 % (2464510)Termination phase: Saturation
% 38.23/12.31 % (2464510)Time elapsed: 0.674 s
% 38.23/12.31 % (2464510)Peak memory usage: 24 MB
% 38.23/12.31 % (2464510)Instructions burned: 1180 (million)
% 38.23/12.31 % (2464516)Instruction limit reached!
% 38.23/12.31 % (2464516)------------------------------
% 38.23/12.31 % (2464516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.31 % (2464516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.31 % (2464516)CaDiCaL version: 2.1.3
% 38.23/12.31 % (2464516)Termination reason: Instruction limit
% 38.23/12.31 % (2464516)Termination phase: Saturation
% 38.23/12.31 % (2464516)Time elapsed: 0.509 s
% 38.23/12.31 % (2464516)Peak memory usage: 18 MB
% 38.23/12.31 % (2464516)Instructions burned: 880 (million)
% 38.23/12.31 % (2464522)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2442481048:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 38.23/12.31 % Detected minimum model sizes of [4]
% 38.23/12.31 % Detected maximum model sizes of [max]
% 38.23/12.31 % TRYING [8]
% 38.23/12.31 % (2464523)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2999440606:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 38.23/12.31 % TRYING [8]
% 38.23/12.31 % TRYING [9]
% 38.23/12.31 % (2464522)Instruction limit reached!
% 38.23/12.31 % (2464522)------------------------------
% 38.23/12.31 % (2464522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.31 % (2464522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.31 % (2464522)CaDiCaL version: 2.1.3
% 38.23/12.31 % (2464522)Termination reason: Instruction limit
% 38.23/12.31 % (2464522)Termination phase: Finite model building constraint generation
% 38.23/12.31 % (2464522)Time elapsed: 0.459 s
% 38.23/12.31 % (2464522)Peak memory usage: 42 MB
% 38.23/12.31 % (2464522)Instructions burned: 921 (million)
% 38.23/12.31 % (2464526)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1779019075:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 38.23/12.31 % TRYING [9]
% 38.23/12.31 % (2464526)Instruction limit reached!
% 38.23/12.31 % (2464526)------------------------------
% 38.23/12.31 % (2464526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.31 % (2464526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.31 % (2464526)CaDiCaL version: 2.1.3
% 38.23/12.31 % (2464526)Termination reason: Instruction limit
% 38.23/12.31 % (2464526)Termination phase: Saturation
% 38.23/12.31 % (2464526)Time elapsed: 0.892 s
% 38.23/12.31 % (2464526)Peak memory usage: 27 MB
% 38.23/12.31 % (2464526)Instructions burned: 1473 (million)
% 38.23/12.31 % (2464528)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4121086311:i=6324_2974 on theBenchmark for (2974ds/6324Mi)
% 38.23/12.31 % Detected minimum model sizes of [4]
% 38.23/12.31 % Detected maximum model sizes of [max]
% 38.23/12.31 % TRYING [77]
% 38.23/12.31 % TRYING [10]
% 38.23/12.31 % TRYING [10]
% 38.23/12.31 % (2464523)Instruction limit reached!
% 38.23/12.31 % (2464523)------------------------------
% 38.23/12.31 % (2464523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.31 % (2464523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.31 % (2464523)CaDiCaL version: 2.1.3
% 38.23/12.31 % (2464523)Termination reason: Instruction limit
% 38.23/12.31 % (2464523)Termination phase: Saturation
% 38.23/12.31 % (2464523)Time elapsed: 2.831 s
% 38.23/12.31 % (2464523)Peak memory usage: 23 MB
% 38.23/12.31 % (2464523)Instructions burned: 5133 (million)
% 38.23/12.31 % (2464530)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3814114206:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi)
% 38.23/12.31 % Detected minimum model sizes of [4]
% 38.23/12.31 % Detected maximum model sizes of [max]
% 38.23/12.31 % TRYING [16]
% 38.23/12.31 % (2464528)Instruction limit reached!
% 38.23/12.31 % (2464528)------------------------------
% 38.23/12.31 % (2464528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.31 % (2464528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.31 % (2464528)CaDiCaL version: 2.1.3
% 38.23/12.31 % (2464528)Termination reason: Instruction limit
% 38.23/12.31 % (2464528)Termination phase: Finite model building constraint generation
% 38.23/12.31 % (2464528)Time elapsed: 2.258 s
% 38.23/12.31 % (2464528)Peak memory usage: 416 MB
% 38.23/12.31 % (2464528)Instructions burned: 6324 (million)
% 38.23/12.31 % (2464534)ott-2_1_sil=16000:newcnf=on:random_seed=3906839617:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2951 on theBenchmark for (2951ds/869Mi)
% 38.23/12.31 % (2464530)Instruction limit reached!
% 38.23/12.31 % (2464530)------------------------------
% 38.23/12.31 % (2464530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.31 % (2464530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.31 % (2464530)CaDiCaL version: 2.1.3
% 38.23/12.31 % (2464530)Termination reason: Instruction limit
% 38.23/12.31 % (2464530)Termination phase: Finite model building constraint generation
% 38.23/12.31 % (2464530)Time elapsed: 0.998 s
% 38.23/12.31 % (2464530)Peak memory usage: 193 MB
% 38.23/12.31 % (2464530)Instructions burned: 2175 (million)
% 38.23/12.31 % (2464536)ott+10_1_sil=32000:tgt=ground:random_seed=2321381841:i=5114:av=off_2949 on theBenchmark for (2949ds/5114Mi)
% 38.23/12.31 % (2464534)Instruction limit reached!
% 38.23/12.31 % (2464534)------------------------------
% 38.23/12.31 % (2464534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.31 % (2464534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.31 % (2464534)CaDiCaL version: 2.1.3
% 38.23/12.31 % (2464534)Termination reason: Instruction limit
% 38.23/12.31 % (2464534)Termination phase: Saturation
% 38.23/12.31 % (2464534)Time elapsed: 0.522 s
% 38.23/12.31 % (2464534)Peak memory usage: 16 MB
% 38.23/12.31 % (2464534)Instructions burned: 869 (million)
% 38.23/12.31 % (2464538)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3697300323:i=54282_2945 on theBenchmark for (2945ds/54282Mi)
% 38.23/12.31 % Detected minimum model sizes of [4]
% 38.23/12.31 % Detected maximum model sizes of [max]
% 38.23/12.31 % TRYING [4]
% 38.23/12.31 % TRYING [5]
% 38.23/12.31 % TRYING [6]
% 38.23/12.31 % TRYING [7]
% 38.23/12.31 % TRYING [8]
% 38.23/12.31 % (2464520)Instruction limit reached!
% 38.23/12.31 % (2464520)------------------------------
% 38.23/12.31 % (2464520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.31 % (2464520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.31 % (2464520)CaDiCaL version: 2.1.3
% 38.23/12.31 % (2464520)Termination reason: Instruction limit
% 38.23/12.31 % (2464520)Termination phase: Finite model building constraint generation
% 38.23/12.31 % (2464520)Time elapsed: 4.893 s
% 38.23/12.31 % (2464520)Peak memory usage: 772 MB
% 38.23/12.31 % (2464520)Instructions burned: 9518 (million)
% 38.23/12.31 % (2464540)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=359406934:i=3512:aac=none_2940 on theBenchmark for (2940ds/3512Mi)
% 38.23/12.32 % TRYING [9]
% 38.23/12.32 % TRYING [11]
% 38.23/12.32 % (2464540)Instruction limit reached!
% 38.23/12.32 % (2464540)------------------------------
% 38.23/12.32 % (2464540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.32 % (2464540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.32 % (2464540)CaDiCaL version: 2.1.3
% 38.23/12.32 % (2464540)Termination reason: Instruction limit
% 38.23/12.32 % (2464540)Termination phase: Saturation
% 38.23/12.32 % (2464540)Time elapsed: 2.026 s
% 38.23/12.32 % (2464540)Peak memory usage: 22 MB
% 38.23/12.32 % (2464540)Instructions burned: 3514 (million)
% 38.23/12.32 % (2464542)dis+21_1_sil=32000:sas=cadical:random_seed=3818365377:i=3773:amm=off_2919 on theBenchmark for (2919ds/3773Mi)
% 38.23/12.32 % TRYING [11]
% 38.23/12.32 % (2464536)Instruction limit reached!
% 38.23/12.32 % (2464536)------------------------------
% 38.23/12.32 % (2464536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.32 % (2464536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.32 % (2464536)CaDiCaL version: 2.1.3
% 38.23/12.32 % (2464536)Termination reason: Instruction limit
% 38.23/12.32 % (2464536)Termination phase: Saturation
% 38.23/12.32 % (2464536)Time elapsed: 3.153 s
% 38.23/12.32 % (2464536)Peak memory usage: 35 MB
% 38.23/12.32 % (2464536)Instructions burned: 5114 (million)
% 38.23/12.32 % (2464544)ott+11_1_sil=16000:gs=on:random_seed=1093894431:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2917 on theBenchmark for (2917ds/2251Mi)
% 38.23/12.32 % TRYING [10]
% 38.23/12.32 % (2464544)Instruction limit reached!
% 38.23/12.32 % (2464544)------------------------------
% 38.23/12.32 % (2464544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.32 % (2464544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.32 % (2464544)CaDiCaL version: 2.1.3
% 38.23/12.32 % (2464544)Termination reason: Instruction limit
% 38.23/12.32 % (2464544)Termination phase: Saturation
% 38.23/12.32 % (2464544)Time elapsed: 1.578 s
% 38.23/12.32 % (2464544)Peak memory usage: 39 MB
% 38.23/12.32 % (2464544)Instructions burned: 2252 (million)
% 38.23/12.32 % (2464546)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2214958658:fmbsr=1.6:i=67534_2901 on theBenchmark for (2901ds/67534Mi)
% 38.23/12.32 % Detected minimum model sizes of [4]
% 38.23/12.32 % Detected maximum model sizes of [max]
% 38.23/12.32 % TRYING [7]
% 38.23/12.32 % TRYING [8]
% 38.23/12.32 % (2464542)Instruction limit reached!
% 38.23/12.32 % (2464542)------------------------------
% 38.23/12.32 % (2464542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.32 % (2464542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.32 % (2464542)CaDiCaL version: 2.1.3
% 38.23/12.32 % (2464542)Termination reason: Instruction limit
% 38.23/12.32 % (2464542)Termination phase: Saturation
% 38.23/12.32 % (2464542)Time elapsed: 2.408 s
% 38.23/12.32 % (2464542)Peak memory usage: 30 MB
% 38.23/12.32 % (2464542)Instructions burned: 3774 (million)
% 38.23/12.32 % (2464548)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1222317499:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2895 on theBenchmark for (2895ds/4591Mi)
% 38.23/12.32 % TRYING [9]
% 38.23/12.32 % (2464518)Instruction limit reached!
% 38.23/12.32 % (2464518)------------------------------
% 38.23/12.32 % (2464518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.32 % (2464518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.32 % (2464518)CaDiCaL version: 2.1.3
% 38.23/12.32 % (2464518)Termination reason: Instruction limit
% 38.23/12.32 % (2464518)Termination phase: Finite model building SAT solving
% 38.23/12.32 % (2464518)Time elapsed: 10.397 s
% 38.23/12.32 % (2464518)Peak memory usage: 74 MB
% 38.23/12.32 % (2464518)Instructions burned: 22061 (million)
% 38.23/12.32 % (2464550)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=897291613:i=29340_2886 on theBenchmark for (2886ds/29340Mi)
% 38.23/12.32 % (2464550) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2464479-2464550"...
% 38.23/12.32 % (2464550)...printing done.
% 38.23/12.32 % (2464550)Refutation found. Thanks to Tanya!
% 38.23/12.32 % SZS status Theorem for theBenchmark
% 38.23/12.32 % SZS output start Proof for theBenchmark
% See solution above
% 38.23/12.32 % (2464550)------------------------------
% 38.23/12.32 % (2464550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.23/12.32 % (2464550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/12.32 % (2464550)CaDiCaL version: 2.1.3
% 38.23/12.32 % (2464550)Termination reason: Refutation
% 38.23/12.32 % (2464550)Time elapsed: 0.522 s
% 38.23/12.32 % (2464550)Peak memory usage: 18 MB
% 38.23/12.32 % (2464550)Instructions burned: 943 (million)
% 38.23/12.32 % (2464479)Success in time 11.897 s
% 38.23/12.32 % Vampire exiting
%------------------------------------------------------------------------------