%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRO003+1 : 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 : n001.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 97.64s 14.22s
% Output : Refutation 97.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 16
% Syntax : Number of formulae : 121 ( 38 unt; 1 def)
% Number of atoms : 327 ( 19 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 349 ( 143 ~; 138 |; 53 &)
% ( 6 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 2 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-3 aty)
% Number of variables : 174 ( 0 sgn 154 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
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(f15,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ~ root(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_14) ).
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(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(f29,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& arboreal(X2)
& arboreal(X3)
& subactivity_occurrence(X2,X1)
& subactivity_occurrence(X3,X1) )
=> ( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_28) ).
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(f35,axiom,
! [X0,X1] :
( leaf_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_34) ).
fof(f36,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_35) ).
fof(f39,axiom,
atomic(tptp4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_38) ).
fof(f40,axiom,
atomic(tptp3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_39) ).
fof(f42,axiom,
atomic(tptp1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_41) ).
fof(f46,axiom,
tptp1 != tptp3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_45) ).
fof(f49,axiom,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& root_occ(X0,X1) )
=> ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_48) ).
fof(f50,conjecture,
~ ? [X0] : occurrence_of(X0,tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f51,negated_conjecture,
~ ~ ? [X0] : occurrence_of(X0,tptp0),
inference(negated_conjecture,[status(cth)],[f50]) ).
fof(f52,plain,
? [X0] : occurrence_of(X0,tptp0),
inference(flattening,[],[f51]) ).
fof(f53,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) ) ),
inference(unused_predicate_definition_removal,[],[f35]) ).
fof(f55,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(unused_predicate_definition_removal,[],[f23]) ).
fof(f58,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f3]) ).
fof(f59,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f58]) ).
fof(f66,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f73,plain,
! [X0,X1,X2] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f15]) ).
fof(f84,plain,
! [X0,X1,X2] :
( ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ),
inference(ennf_transformation,[],[f55]) ).
fof(f86,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(f91,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| ~ subactivity_occurrence(X3,X1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f92,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| ~ subactivity_occurrence(X3,X1) ),
inference(flattening,[],[f91]) ).
fof(f101,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) )
| ~ leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f53]) ).
fof(f102,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,[],[f36]) ).
fof(f103,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ root_occ(X0,X1) ),
inference(ennf_transformation,[],[f49]) ).
fof(f104,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ root_occ(X0,X1) ),
inference(flattening,[],[f103]) ).
fof(f106,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f66]) ).
fof(f116,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK7(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK7(X0,X1,X2))
& subactivity_occurrence(X2,sK7(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X3,sK7(X0,X1,X2))],[f86]) ).
fof(f120,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(f121,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,[],[f120]) ).
fof(f122,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ( occurrence_of(X1,sK11(X0,X1))
& subactivity_occurrence(X0,X1)
& root(X0,sK11(X0,X1)) )
| ~ root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X3,sK11(X0,X1))],[f121]) ).
fof(f123,plain,
! [X0,X1] :
( ( occurrence_of(X1,sK12(X0,X1))
& subactivity_occurrence(X0,X1)
& leaf(X0,sK12(X0,X1)) )
| ~ leaf_occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f101]) ).
fof(f124,plain,
! [X0] :
( ( occurrence_of(sK13(X0),tptp4)
& root_occ(sK13(X0),X0)
& occurrence_of(sK14(X0),tptp3)
& leaf_occ(sK14(X0),X0)
& next_subocc(sK13(X0),sK14(X0),tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14]),skolemize(X1,sK13(X0)),skolemize(X2,sK14(X0))],[f102]) ).
fof(f125,plain,
! [X0,X1] :
( ( occurrence_of(sK15(X0),tptp1)
& next_subocc(X0,sK15(X0),tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ root_occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X2,sK15(X0))],[f104]) ).
fof(f126,plain,
occurrence_of(sK16,tptp0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X0,sK16)],[f52]) ).
fof(f131,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f59]) ).
fof(f137,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f106]) ).
fof(f151,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| ~ root(X1,X2) ),
inference(cnf_transformation,[],[f73]) ).
fof(f160,plain,
! [X2,X3,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X3,X2) ),
inference(cnf_transformation,[],[f84]) ).
fof(f161,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f84]) ).
fof(f168,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK7(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f169,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X1,sK7(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f170,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| occurrence_of(sK7(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f175,plain,
! [X2,X3,X0,X1] :
( ~ subactivity_occurrence(X3,X1)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| min_precedes(X2,X3,X0) ),
inference(cnf_transformation,[],[f92]) ).
fof(f181,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| root(X0,sK11(X0,X1)) ),
inference(cnf_transformation,[],[f122]) ).
fof(f182,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f122]) ).
fof(f183,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| occurrence_of(X1,sK11(X0,X1)) ),
inference(cnf_transformation,[],[f122]) ).
fof(f186,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f123]) ).
fof(f188,plain,
! [X0] :
( next_subocc(sK13(X0),sK14(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f189,plain,
! [X0] :
( leaf_occ(sK14(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f190,plain,
! [X0] :
( occurrence_of(sK14(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f191,plain,
! [X0] :
( root_occ(sK13(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f192,plain,
! [X0] :
( occurrence_of(sK13(X0),tptp4)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f195,plain,
atomic(tptp4),
inference(cnf_transformation,[],[f39]) ).
fof(f196,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f40]) ).
fof(f198,plain,
atomic(tptp1),
inference(cnf_transformation,[],[f42]) ).
fof(f202,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f46]) ).
fof(f205,plain,
! [X0,X1] :
( next_subocc(X0,sK15(X0),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f206,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK15(X0),tptp1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f207,plain,
occurrence_of(sK16,tptp0),
inference(cnf_transformation,[],[f126]) ).
fof(f247,plain,
! [X0] :
( subactivity_occurrence(sK14(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f189,f186]) ).
fof(f258,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp3)
| arboreal(sK14(X0)) ),
inference(resolution,[],[f190,f137]) ).
fof(f262,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK14(X0)) ),
inference(forward_subsumption_resolution,[],[f258,f196]) ).
fof(f293,plain,
root_occ(sK13(sK16),sK16),
inference(unit_resulting_resolution,[],[f191,f207]) ).
fof(f294,plain,
! [X0] :
( subactivity_occurrence(sK13(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f191,f182]) ).
fof(f313,definition,
( spl17_1
<=> arboreal(sK13(sK16)) ),
introduced(definition,[new_symbols(definition,[spl17_1])],[avatar_definition]) ).
fof(f314,plain,
( ~ arboreal(sK13(sK16))
| spl17_1 ),
inference(avatar_component_clause,[],[f313]) ).
fof(f315,plain,
( arboreal(sK13(sK16))
| ~ spl17_1 ),
inference(avatar_component_clause,[],[f313]) ).
fof(f324,plain,
( ~ occurrence_of(sK13(sK16),tptp4)
| spl17_1 ),
inference(unit_resulting_resolution,[],[f137,f195,f314]) ).
fof(f335,plain,
( ~ occurrence_of(sK16,tptp0)
| spl17_1 ),
inference(unit_resulting_resolution,[],[f192,f324]) ).
fof(f338,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp4)
| arboreal(sK13(X0)) ),
inference(resolution,[],[f192,f137]) ).
fof(f343,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK13(X0)) ),
inference(forward_subsumption_resolution,[],[f338,f195]) ).
fof(f348,plain,
( $false
| spl17_1 ),
inference(forward_subsumption_resolution,[],[f335,f207]) ).
fof(f349,plain,
spl17_1,
inference(avatar_contradiction_clause,[],[f348]) ).
fof(f394,plain,
root(sK13(sK16),sK11(sK13(sK16),sK16)),
inference(unit_resulting_resolution,[],[f181,f293]) ).
fof(f396,plain,
! [X0] :
( root(sK13(X0),sK11(sK13(X0),X0))
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f181,f191]) ).
fof(f400,plain,
! [X0] : ~ min_precedes(X0,sK13(sK16),sK11(sK13(sK16),sK16)),
inference(unit_resulting_resolution,[],[f151,f394]) ).
fof(f484,plain,
occurrence_of(sK16,sK11(sK13(sK16),sK16)),
inference(unit_resulting_resolution,[],[f183,f293]) ).
fof(f485,plain,
! [X0] :
( occurrence_of(X0,sK11(sK13(X0),X0))
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f183,f191]) ).
fof(f807,plain,
tptp0 = sK11(sK13(sK16),sK16),
inference(unit_resulting_resolution,[],[f131,f484,f207]) ).
fof(f1083,plain,
! [X0] : ~ min_precedes(X0,sK13(sK16),tptp0),
inference(superposition,[],[f400,f807]) ).
fof(f1586,plain,
! [X0] :
( min_precedes(sK13(X0),sK14(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f188,f161]) ).
fof(f4133,plain,
occurrence_of(sK15(sK13(sK16)),tptp1),
inference(unit_resulting_resolution,[],[f206,f293,f207]) ).
fof(f4141,plain,
~ occurrence_of(sK15(sK13(sK16)),tptp3),
inference(unit_resulting_resolution,[],[f131,f202,f4133]) ).
fof(f4148,plain,
arboreal(sK15(sK13(sK16))),
inference(unit_resulting_resolution,[],[f137,f198,f4133]) ).
fof(f4718,plain,
next_subocc(sK13(sK16),sK15(sK13(sK16)),tptp0),
inference(unit_resulting_resolution,[],[f205,f293,f207]) ).
fof(f4727,plain,
min_precedes(sK13(sK16),sK15(sK13(sK16)),tptp0),
inference(unit_resulting_resolution,[],[f161,f4718]) ).
fof(f4739,plain,
subactivity_occurrence(sK15(sK13(sK16)),sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),
inference(unit_resulting_resolution,[],[f168,f4727]) ).
fof(f4740,plain,
subactivity_occurrence(sK13(sK16),sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),
inference(unit_resulting_resolution,[],[f169,f4727]) ).
fof(f4741,plain,
occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0),
inference(unit_resulting_resolution,[],[f170,f4727]) ).
fof(f5219,plain,
! [X0] :
( ~ min_precedes(X0,sK15(sK13(sK16)),tptp0)
| ~ min_precedes(sK13(sK16),X0,tptp0) ),
inference(resolution,[],[f160,f4718]) ).
fof(f5962,plain,
next_subocc(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0),
inference(unit_resulting_resolution,[],[f188,f4741]) ).
fof(f7442,plain,
! [X2,X0,X1] :
( min_precedes(sK14(X0),X1,X2)
| sK14(X0) = X1
| ~ occurrence_of(X0,X2)
| ~ arboreal(X1)
| ~ arboreal(sK14(X0))
| ~ subactivity_occurrence(X1,X0)
| min_precedes(X1,sK14(X0),X2)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f175,f247]) ).
fof(f7443,plain,
! [X2,X0,X1] :
( min_precedes(sK13(X0),X1,X2)
| sK13(X0) = X1
| ~ occurrence_of(X0,X2)
| ~ arboreal(X1)
| ~ arboreal(sK13(X0))
| ~ subactivity_occurrence(X1,X0)
| min_precedes(X1,sK13(X0),X2)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f175,f294]) ).
fof(f7477,plain,
! [X2,X0,X1] :
( ~ subactivity_occurrence(X1,X0)
| sK13(X0) = X1
| ~ occurrence_of(X0,X2)
| ~ arboreal(X1)
| min_precedes(sK13(X0),X1,X2)
| min_precedes(X1,sK13(X0),X2)
| ~ occurrence_of(X0,tptp0) ),
inference(forward_subsumption_resolution,[],[f7443,f343]) ).
fof(f7478,plain,
! [X2,X0,X1] :
( ~ subactivity_occurrence(X1,X0)
| sK14(X0) = X1
| ~ occurrence_of(X0,X2)
| ~ arboreal(X1)
| min_precedes(sK14(X0),X1,X2)
| min_precedes(X1,sK14(X0),X2)
| ~ occurrence_of(X0,tptp0) ),
inference(forward_subsumption_resolution,[],[f7442,f262]) ).
fof(f9264,plain,
! [X0,X1] :
( ~ occurrence_of(X0,tptp0)
| ~ occurrence_of(X0,X1)
| sK11(sK13(X0),X0) = X1 ),
inference(resolution,[],[f485,f131]) ).
fof(f9561,plain,
min_precedes(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0),
inference(unit_resulting_resolution,[],[f1586,f4741]) ).
fof(f34344,plain,
tptp0 = sK11(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),
inference(unit_resulting_resolution,[],[f9264,f4741,f4741]) ).
fof(f76174,plain,
( root(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0) ),
inference(superposition,[],[f396,f34344]) ).
fof(f76189,plain,
root(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0),
inference(forward_subsumption_resolution,[],[f76174,f4741]) ).
fof(f76194,plain,
! [X0] : ~ min_precedes(X0,sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0),
inference(unit_resulting_resolution,[],[f151,f76189]) ).
fof(f76221,plain,
( sK13(sK16) = sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ spl17_1 ),
inference(unit_resulting_resolution,[],[f7477,f315,f4741,f4741,f4740,f1083,f76194]) ).
fof(f76239,plain,
( next_subocc(sK13(sK16),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ spl17_1 ),
inference(superposition,[],[f5962,f76221]) ).
fof(f76260,plain,
( min_precedes(sK13(sK16),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ spl17_1 ),
inference(superposition,[],[f9561,f76221]) ).
fof(f76903,plain,
( ~ min_precedes(sK15(sK13(sK16)),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ spl17_1 ),
inference(unit_resulting_resolution,[],[f160,f4727,f76239]) ).
fof(f76910,plain,
( ~ min_precedes(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK15(sK13(sK16)),tptp0)
| ~ spl17_1 ),
inference(unit_resulting_resolution,[],[f5219,f76260]) ).
fof(f77132,plain,
( sK15(sK13(sK16)) = sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ spl17_1 ),
inference(unit_resulting_resolution,[],[f7478,f4148,f4741,f4741,f4739,f76903,f76910]) ).
fof(f77410,plain,
( occurrence_of(sK15(sK13(sK16)),tptp3)
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0)
| ~ spl17_1 ),
inference(superposition,[],[f190,f77132]) ).
fof(f77540,plain,
( ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0)
| ~ spl17_1 ),
inference(forward_subsumption_resolution,[],[f77410,f4141]) ).
fof(f77674,plain,
( $false
| ~ spl17_1 ),
inference(forward_subsumption_resolution,[],[f77540,f4741]) ).
fof(f77675,plain,
~ spl17_1,
inference(avatar_contradiction_clause,[],[f77674]) ).
cnf(s6,plain,
spl17_1,
inference(sat_conversion,[],[f349]) ).
cnf(s52,plain,
~ spl17_1,
inference(sat_conversion,[],[f77675]) ).
cnf(s53,plain,
$false,
inference(rat,[],[s6,s52]) ).
fof(f77685,plain,
$false,
inference(avatar_sat_refutation,[],[s53]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO003+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n001.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 22:22:16 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/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.71/2.91 % (4022808)Will run a generic schedule for satisfiability detection.
% 16.71/2.91 % (4022813)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2495567660_2999 on theBenchmark for (2999ds/0Mi)
% 16.71/2.91 % Detected minimum model sizes of [4]
% 16.71/2.91 % Detected maximum model sizes of [max]
% 16.71/2.91 % TRYING [4]
% 16.71/2.91 % (4022814)% WARNING: option uhcvi not known.
% 16.71/2.91 % (4022816)dis+10_1_sil=32000:sp=arity:random_seed=1259435308:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.71/2.91 % (4022814)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3347239985:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.71/2.91 % (4022815)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2820010623:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.71/2.91 % TRYING [5]
% 16.71/2.91 % (4022817)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=824546395:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.71/2.91 % (4022818)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1979855412:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.71/2.91 % (4022819)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2780132614:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.71/2.91 % TRYING [6]
% 16.71/2.91 % (4022817)Instruction limit reached!
% 16.71/2.91 % (4022817)------------------------------
% 16.71/2.91 % (4022817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.71/2.91 % (4022817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.71/2.91 % (4022817)CaDiCaL version: 2.1.3
% 16.71/2.91 % (4022817)Termination reason: Instruction limit
% 16.71/2.91 % (4022817)Termination phase: Saturation
% 16.71/2.91 % (4022817)Time elapsed: 0.068 s
% 16.71/2.91 % (4022817)Peak memory usage: 12 MB
% 16.71/2.91 % (4022817)Instructions burned: 124 (million)
% 16.71/2.91 % TRYING [7]
% 16.71/2.91 % (4022816)Instruction limit reached!
% 16.71/2.91 % (4022816)------------------------------
% 16.71/2.91 % (4022816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.71/2.91 % (4022816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.71/2.91 % (4022816)CaDiCaL version: 2.1.3
% 16.71/2.91 % (4022816)Termination reason: Instruction limit
% 16.71/2.91 % (4022816)Termination phase: Saturation
% 16.71/2.91 % (4022816)Time elapsed: 0.073 s
% 16.71/2.91 % (4022816)Peak memory usage: 12 MB
% 16.71/2.91 % (4022816)Instructions burned: 104 (million)
% 16.71/2.91 % (4022818)Instruction limit reached!
% 16.71/2.91 % (4022818)------------------------------
% 16.71/2.91 % (4022818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.71/2.91 % (4022818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.71/2.91 % (4022818)CaDiCaL version: 2.1.3
% 16.71/2.91 % (4022818)Termination reason: Instruction limit
% 16.71/2.91 % (4022818)Termination phase: Saturation
% 16.71/2.91 % (4022818)Time elapsed: 0.087 s
% 16.71/2.91 % (4022818)Peak memory usage: 13 MB
% 16.71/2.91 % (4022818)Instructions burned: 132 (million)
% 16.71/2.91 % (4022827)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1815516626:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 16.71/2.91 % (4022828)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=280454789:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.71/2.91 % Detected minimum model sizes of [4]
% 16.71/2.91 % Detected maximum model sizes of [max]
% 16.71/2.91 % TRYING [4]
% 16.71/2.91 % TRYING [5]
% 16.71/2.91 % (4022829)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=988966380:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.71/2.91 % (4022819)Instruction limit reached!
% 16.71/2.91 % (4022819)------------------------------
% 16.71/2.91 % (4022819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.71/2.91 % (4022819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.71/2.91 % (4022819)CaDiCaL version: 2.1.3
% 16.71/2.91 % (4022819)Termination reason: Instruction limit
% 16.71/2.91 % (4022819)Termination phase: Saturation
% 16.71/2.91 % (4022819)Time elapsed: 0.110 s
% 16.71/2.91 % (4022819)Peak memory usage: 14 MB
% 16.71/2.91 % (4022819)Instructions burned: 159 (million)
% 16.71/2.91 % (4022833)ott-21_1_sil=16000:fs=off:random_seed=2371722603:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.71/2.91 % TRYING [6]
% 16.71/2.91 % (4022828)Instruction limit reached!
% 16.71/2.91 % (4022828)------------------------------
% 45.41/6.99 % (4022828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.41/6.99 % (4022828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.41/6.99 % (4022828)CaDiCaL version: 2.1.3
% 45.41/6.99 % (4022828)Termination reason: Instruction limit
% 45.41/6.99 % (4022828)Termination phase: Saturation
% 45.41/6.99 % (4022828)Time elapsed: 0.092 s
% 45.41/6.99 % (4022828)Peak memory usage: 14 MB
% 45.41/6.99 % (4022828)Instructions burned: 132 (million)
% 45.41/6.99 % (4022835)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2476574709:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 45.41/6.99 % (4022833)Instruction limit reached!
% 45.41/6.99 % (4022833)------------------------------
% 45.41/6.99 % (4022833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.41/6.99 % (4022833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.41/6.99 % (4022833)CaDiCaL version: 2.1.3
% 45.41/6.99 % (4022833)Termination reason: Instruction limit
% 45.41/6.99 % (4022833)Termination phase: Saturation
% 45.41/6.99 % (4022833)Time elapsed: 0.098 s
% 45.41/6.99 % (4022833)Peak memory usage: 13 MB
% 45.41/6.99 % (4022833)Instructions burned: 180 (million)
% 45.41/6.99 % TRYING [7]
% 45.41/6.99 % (4022837)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2229387778:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 45.41/6.99 % Detected minimum model sizes of [4]
% 45.41/6.99 % Detected maximum model sizes of [max]
% 45.41/6.99 % TRYING [4]
% 45.41/6.99 % TRYING [5]
% 45.41/6.99 % TRYING [6]
% 45.41/6.99 % (4022827)Instruction limit reached!
% 45.41/6.99 % (4022827)------------------------------
% 45.41/6.99 % (4022827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.41/6.99 % (4022827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.41/6.99 % (4022827)CaDiCaL version: 2.1.3
% 45.41/6.99 % (4022827)Termination reason: Instruction limit
% 45.41/6.99 % (4022827)Termination phase: Finite model building SAT solving
% 45.41/6.99 % (4022827)Time elapsed: 0.354 s
% 45.41/6.99 % (4022827)Peak memory usage: 28 MB
% 45.41/6.99 % (4022827)Instructions burned: 715 (million)
% 45.41/6.99 % TRYING [7]
% 45.41/6.99 % (4022839)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2741585174:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 45.41/6.99 % (4022829)Instruction limit reached!
% 45.41/6.99 % (4022829)------------------------------
% 45.41/6.99 % (4022829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.41/6.99 % (4022829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.41/6.99 % (4022829)CaDiCaL version: 2.1.3
% 45.41/6.99 % (4022829)Termination reason: Instruction limit
% 45.41/6.99 % (4022829)Termination phase: Saturation
% 45.41/6.99 % (4022829)Time elapsed: 0.409 s
% 45.41/6.99 % (4022829)Peak memory usage: 19 MB
% 45.41/6.99 % (4022829)Instructions burned: 685 (million)
% 45.41/6.99 % (4022841)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=465547178:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 45.41/6.99 % (4022835)Instruction limit reached!
% 45.41/6.99 % (4022835)------------------------------
% 45.41/6.99 % (4022835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.41/6.99 % (4022835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.41/6.99 % (4022835)CaDiCaL version: 2.1.3
% 45.41/6.99 % (4022835)Termination reason: Instruction limit
% 45.41/6.99 % (4022835)Termination phase: Saturation
% 45.41/6.99 % (4022835)Time elapsed: 0.343 s
% 45.41/6.99 % (4022835)Peak memory usage: 15 MB
% 45.41/6.99 % (4022835)Instructions burned: 478 (million)
% 45.41/6.99 % (4022843)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=2821659778: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)
% 45.41/6.99 % (4022837)Instruction limit reached!
% 45.41/6.99 % (4022837)------------------------------
% 45.41/6.99 % (4022837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.41/6.99 % (4022837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.41/6.99 % (4022837)CaDiCaL version: 2.1.3
% 45.41/6.99 % (4022837)Termination reason: Instruction limit
% 45.41/6.99 % (4022837)Termination phase: Finite model building SAT solving
% 45.41/6.99 % (4022837)Time elapsed: 0.357 s
% 45.41/6.99 % (4022837)Peak memory usage: 23 MB
% 45.41/6.99 % (4022837)Instructions burned: 867 (million)
% 45.41/6.99 % TRYING [14]
% 45.41/6.99 % TRYING [8]
% 45.41/6.99 % (4022845)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2780178066:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 87.70/12.80 % (4022841)Instruction limit reached!
% 87.70/12.80 % (4022841)------------------------------
% 87.70/12.80 % (4022841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.70/12.80 % (4022841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.70/12.80 % (4022841)CaDiCaL version: 2.1.3
% 87.70/12.80 % (4022841)Termination reason: Instruction limit
% 87.70/12.80 % (4022841)Termination phase: Finite model building constraint generation
% 87.70/12.80 % (4022841)Time elapsed: 0.338 s
% 87.70/12.80 % (4022841)Peak memory usage: 80 MB
% 87.70/12.80 % (4022841)Instructions burned: 889 (million)
% 87.70/12.80 % (4022848)fmb+10_1_sil=64000:random_seed=174009261:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 87.70/12.80 % Detected minimum model sizes of [4]
% 87.70/12.80 % Detected maximum model sizes of [max]
% 87.70/12.80 % TRYING [4]
% 87.70/12.80 % TRYING [5]
% 87.70/12.80 % (4022843)Instruction limit reached!
% 87.70/12.80 % (4022843)------------------------------
% 87.70/12.80 % (4022843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.70/12.80 % (4022843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.70/12.80 % (4022843)CaDiCaL version: 2.1.3
% 87.70/12.80 % (4022843)Termination reason: Instruction limit
% 87.70/12.80 % (4022843)Termination phase: Saturation
% 87.70/12.80 % (4022843)Time elapsed: 0.379 s
% 87.70/12.80 % (4022843)Peak memory usage: 17 MB
% 87.70/12.80 % (4022843)Instructions burned: 694 (million)
% 87.70/12.80 % (4022850)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1389426161:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 87.70/12.80 % TRYING [6]
% 87.70/12.80 % Detected minimum model sizes of [4]
% 87.70/12.80 % Detected maximum model sizes of [max]
% 87.70/12.80 % TRYING [20]
% 87.70/12.80 % TRYING [7]
% 87.70/12.80 % (4022845)Instruction limit reached!
% 87.70/12.80 % (4022845)------------------------------
% 87.70/12.80 % (4022845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.70/12.80 % (4022845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.70/12.80 % (4022845)CaDiCaL version: 2.1.3
% 87.70/12.80 % (4022845)Termination reason: Instruction limit
% 87.70/12.81 % (4022845)Termination phase: Saturation
% 87.70/12.81 % (4022845)Time elapsed: 0.509 s
% 87.70/12.81 % (4022845)Peak memory usage: 18 MB
% 87.70/12.81 % (4022845)Instructions burned: 880 (million)
% 87.70/12.81 % (4022852)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2581294081:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 87.70/12.81 % Detected minimum model sizes of [4]
% 87.70/12.81 % Detected maximum model sizes of [max]
% 87.70/12.81 % TRYING [8]
% 87.70/12.81 % (4022839)Instruction limit reached!
% 87.70/12.81 % (4022839)------------------------------
% 87.70/12.81 % (4022839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.70/12.81 % (4022839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.70/12.81 % (4022839)CaDiCaL version: 2.1.3
% 87.70/12.81 % (4022839)Termination reason: Instruction limit
% 87.70/12.81 % (4022839)Termination phase: Saturation
% 87.70/12.81 % (4022839)Time elapsed: 0.734 s
% 87.70/12.81 % (4022839)Peak memory usage: 25 MB
% 87.70/12.81 % (4022839)Instructions burned: 1179 (million)
% 87.70/12.81 % (4022854)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1658232692:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 87.70/12.81 % TRYING [8]
% 87.70/12.81 % (4022852)Instruction limit reached!
% 87.70/12.81 % (4022852)------------------------------
% 87.70/12.81 % (4022852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.70/12.81 % (4022852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.70/12.81 % (4022852)CaDiCaL version: 2.1.3
% 87.70/12.81 % (4022852)Termination reason: Instruction limit
% 87.70/12.81 % (4022852)Termination phase: Finite model building SAT solving
% 87.70/12.81 % (4022852)Time elapsed: 0.493 s
% 87.70/12.81 % (4022852)Peak memory usage: 47 MB
% 87.70/12.81 % (4022852)Instructions burned: 921 (million)
% 87.70/12.81 % (4022856)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2740951544:i=1472:ins=7:fdi=8:gsp=on_2982 on theBenchmark for (2982ds/1472Mi)
% 87.70/12.81 % (4022856)Instruction limit reached!
% 87.70/12.81 % (4022856)------------------------------
% 87.70/12.81 % (4022856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.70/12.81 % (4022856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.64/14.22 % (4022856)CaDiCaL version: 2.1.3
% 97.64/14.22 % (4022856)Termination reason: Instruction limit
% 97.64/14.22 % (4022856)Termination phase: Saturation
% 97.64/14.22 % (4022856)Time elapsed: 0.762 s
% 97.64/14.22 % (4022856)Peak memory usage: 27 MB
% 97.64/14.22 % (4022856)Instructions burned: 1472 (million)
% 97.64/14.22 % (4022858)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2059120730:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 97.64/14.22 % Detected minimum model sizes of [4]
% 97.64/14.22 % Detected maximum model sizes of [max]
% 97.64/14.22 % TRYING [77]
% 97.64/14.22 % TRYING [9]
% 97.64/14.22 % (4022854)Instruction limit reached!
% 97.64/14.22 % (4022854)------------------------------
% 97.64/14.22 % (4022854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.64/14.22 % (4022854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.64/14.22 % (4022854)CaDiCaL version: 2.1.3
% 97.64/14.22 % (4022854)Termination reason: Instruction limit
% 97.64/14.22 % (4022854)Termination phase: Saturation
% 97.64/14.22 % (4022854)Time elapsed: 2.881 s
% 97.64/14.22 % (4022854)Peak memory usage: 21 MB
% 97.64/14.22 % (4022854)Instructions burned: 5132 (million)
% 97.64/14.22 % (4022860)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1942771561:fmbsr=2.30978:i=2174_2958 on theBenchmark for (2958ds/2174Mi)
% 97.64/14.22 % Detected minimum model sizes of [4]
% 97.64/14.22 % Detected maximum model sizes of [max]
% 97.64/14.22 % TRYING [16]
% 97.64/14.22 % (4022858)Instruction limit reached!
% 97.64/14.22 % (4022858)------------------------------
% 97.64/14.22 % (4022858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.64/14.22 % (4022858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.64/14.22 % (4022858)CaDiCaL version: 2.1.3
% 97.64/14.22 % (4022858)Termination reason: Instruction limit
% 97.64/14.22 % (4022858)Termination phase: Finite model building constraint generation
% 97.64/14.22 % (4022858)Time elapsed: 2.261 s
% 97.64/14.22 % (4022858)Peak memory usage: 430 MB
% 97.64/14.22 % (4022858)Instructions burned: 6325 (million)
% 97.64/14.22 % (4022862)ott-2_1_sil=16000:newcnf=on:random_seed=241586492:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2951 on theBenchmark for (2951ds/869Mi)
% 97.64/14.22 % (4022860)Instruction limit reached!
% 97.64/14.22 % (4022860)------------------------------
% 97.64/14.22 % (4022860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.64/14.22 % (4022860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.64/14.22 % (4022860)CaDiCaL version: 2.1.3
% 97.64/14.22 % (4022860)Termination reason: Instruction limit
% 97.64/14.22 % (4022860)Termination phase: Finite model building constraint generation
% 97.64/14.22 % (4022860)Time elapsed: 0.945 s
% 97.64/14.22 % (4022860)Peak memory usage: 217 MB
% 97.64/14.22 % (4022860)Instructions burned: 2174 (million)
% 97.64/14.22 % (4022864)ott+10_1_sil=32000:tgt=ground:random_seed=592118639:i=5114:av=off_2948 on theBenchmark for (2948ds/5114Mi)
% 97.64/14.22 % (4022862)Instruction limit reached!
% 97.64/14.22 % (4022862)------------------------------
% 97.64/14.22 % (4022862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.64/14.22 % (4022862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.64/14.22 % (4022862)CaDiCaL version: 2.1.3
% 97.64/14.22 % (4022862)Termination reason: Instruction limit
% 97.64/14.22 % (4022862)Termination phase: Saturation
% 97.64/14.22 % (4022862)Time elapsed: 0.530 s
% 97.64/14.22 % (4022862)Peak memory usage: 17 MB
% 97.64/14.22 % (4022862)Instructions burned: 869 (million)
% 97.64/14.22 % (4022866)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1467668408:i=54282_2946 on theBenchmark for (2946ds/54282Mi)
% 97.64/14.22 % Detected minimum model sizes of [4]
% 97.64/14.22 % Detected maximum model sizes of [max]
% 97.64/14.22 % TRYING [4]
% 97.64/14.22 % TRYING [5]
% 97.64/14.22 % TRYING [6]
% 97.64/14.22 % TRYING [7]
% 97.64/14.22 % (4022850)Instruction limit reached!
% 97.64/14.22 % (4022850)------------------------------
% 97.64/14.22 % (4022850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.64/14.22 % (4022850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.64/14.22 % (4022850)CaDiCaL version: 2.1.3
% 97.64/14.22 % (4022850)Termination reason: Instruction limit
% 97.64/14.22 % (4022850)Termination phase: Finite model building constraint generation
% 97.64/14.22 % (4022850)Time elapsed: 4.918 s
% 97.64/14.22 % (4022850)Peak memory usage: 837 MB
% 97.64/14.22 % (4022850)Instructions burned: 9516 (million)
% 97.64/14.22 % (4022868)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3342262189:i=3512:aac=none_2939 on theBenchmark for (2939ds/3512Mi)
% 97.64/14.22 % TRYING [8]
% 97.64/14.22 % TRYING [9]
% 97.64/14.22 % (4022868)Instruction limit reached!
% 97.64/14.22 % (4022868)------------------------------
% 97.64/14.22 % (4022868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.64/14.22 % (4022868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.64/14.22 % (4022868)CaDiCaL version: 2.1.3
% 97.64/14.22 % (4022868)Termination reason: Instruction limit
% 97.64/14.22 % (4022868)Termination phase: Saturation
% 97.64/14.22 % (4022868)Time elapsed: 1.920 s
% 97.64/14.22 % (4022868)Peak memory usage: 17 MB
% 97.64/14.22 % (4022868)Instructions burned: 3514 (million)
% 97.64/14.22 % (4022870)dis+21_1_sil=32000:sas=cadical:random_seed=3881536222:i=3773:amm=off_2920 on theBenchmark for (2920ds/3773Mi)
% 97.64/14.22 % (4022864)Instruction limit reached!
% 97.64/14.22 % (4022864)------------------------------
% 97.64/14.22 % (4022864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.64/14.22 % (4022864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.64/14.22 % (4022864)CaDiCaL version: 2.1.3
% 97.64/14.22 % (4022864)Termination reason: Instruction limit
% 97.64/14.22 % (4022864)Termination phase: Saturation
% 97.64/14.22 % (4022864)Time elapsed: 3.118 s
% 97.64/14.22 % (4022864)Peak memory usage: 38 MB
% 97.64/14.22 % (4022864)Instructions burned: 5114 (million)
% 97.64/14.22 % (4022872)ott+11_1_sil=16000:gs=on:random_seed=2024700539:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2917 on theBenchmark for (2917ds/2251Mi)
% 97.64/14.22 % (4022872)Instruction limit reached!
% 97.64/14.22 % (4022872)------------------------------
% 97.64/14.22 % (4022872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.64/14.22 % (4022872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.64/14.22 % (4022872)CaDiCaL version: 2.1.3
% 97.64/14.22 % (4022872)Termination reason: Instruction limit
% 97.64/14.22 % (4022872)Termination phase: Saturation
% 97.64/14.22 % (4022872)Time elapsed: 1.533 s
% 97.64/14.22 % (4022872)Peak memory usage: 34 MB
% 97.64/14.22 % (4022872)Instructions burned: 2251 (million)
% 97.64/14.22 % (4022874)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1681165154:fmbsr=1.6:i=67534_2901 on theBenchmark for (2901ds/67534Mi)
% 97.64/14.22 % Detected minimum model sizes of [4]
% 97.64/14.22 % Detected maximum model sizes of [max]
% 97.64/14.22 % TRYING [7]
% 97.64/14.22 % (4022870)Instruction limit reached!
% 97.64/14.22 % (4022870)------------------------------
% 97.64/14.22 % (4022870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.64/14.22 % (4022870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.64/14.22 % (4022870)CaDiCaL version: 2.1.3
% 97.64/14.22 % (4022870)Termination reason: Instruction limit
% 97.64/14.22 % (4022870)Termination phase: Saturation
% 97.64/14.22 % (4022870)Time elapsed: 2.272 s
% 97.64/14.22 % (4022870)Peak memory usage: 32 MB
% 97.64/14.22 % (4022870)Instructions burned: 3775 (million)
% 97.64/14.22 % (4022876)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=277089709:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2897 on theBenchmark for (2897ds/4591Mi)
% 97.64/14.22 % TRYING [8]
% 97.64/14.22 % (4022876)Instruction limit reached!
% 97.64/14.22 % (4022876)------------------------------
% 97.64/14.22 % (4022876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.64/14.22 % (4022876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.64/14.22 % (4022876)CaDiCaL version: 2.1.3
% 97.64/14.22 % (4022876)Termination reason: Instruction limit
% 97.64/14.22 % (4022876)Termination phase: Saturation
% 97.64/14.22 % (4022876)Time elapsed: 0.759 s
% 97.64/14.22 % (4022876)Peak memory usage: 12 MB
% 97.64/14.22 % (4022876)Instructions burned: 4593 (million)
% 97.64/14.22 % (4022878)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=820194051:i=29340_2889 on theBenchmark for (2889ds/29340Mi)
% 97.64/14.22 % TRYING [9]
% 97.64/14.22 % (4022848)Instruction limit reached!
% 97.64/14.22 % (4022848)------------------------------
% 97.64/14.22 % (4022848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.64/14.22 % (4022848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.64/14.22 % (4022848)CaDiCaL version: 2.1.3
% 97.64/14.22 % (4022848)Termination reason: Instruction limit
% 97.64/14.22 % (4022848)Termination phase: Finite model building SAT solving
% 97.64/14.22 % (4022848)Time elapsed: 11.408 s
% 97.64/14.22 % (4022848)Peak memory usage: 44 MB
% 97.64/14.22 % (4022848)Instructions burned: 22062 (million)
% 97.64/14.22 % (4022880)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2126679843:i=5211_2876 on theBenchmark for (2876ds/5211Mi)
% 97.64/14.22 % (4022878) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4022808-4022878"...
% 97.64/14.22 % (4022878)...printing done.
% 97.64/14.22 % (4022878)Refutation found. Thanks to Tanya!
% 97.64/14.22 % SZS status Theorem for theBenchmark
% 97.64/14.22 % SZS output start Proof for theBenchmark
% See solution above
% 97.64/14.22 % (4022878)------------------------------
% 97.64/14.22 % (4022878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.64/14.22 % (4022878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.64/14.22 % (4022878)CaDiCaL version: 2.1.3
% 97.64/14.22 % (4022878)Termination reason: Refutation
% 97.64/14.22 % (4022878)Time elapsed: 2.716 s
% 97.64/14.22 % (4022878)Peak memory usage: 39 MB
% 97.64/14.22 % (4022878)Instructions burned: 10048 (million)
% 97.64/14.22 % (4022808)Success in time 13.797 s
% 97.64/14.22 % Vampire exiting
%------------------------------------------------------------------------------