%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRO017+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:30:40 PM UTC 2026
% Result : Theorem 0.93s 0.59s
% Output : Refutation 0.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 22
% Syntax : Number of formulae : 162 ( 38 unt; 10 def)
% Number of atoms : 472 ( 37 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 495 ( 185 ~; 230 |; 57 &)
% ( 13 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 11 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-3 aty)
% Number of variables : 159 ( 0 sgn 138 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ~ ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_04) ).
fof(f7,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> precedes(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_06) ).
fof(f9,axiom,
! [X0,X1] :
( precedes(X0,X1)
<=> ( earlier(X0,X1)
& legal(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_08) ).
fof(f18,axiom,
! [X0] :
( legal(X0)
=> arboreal(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_17) ).
fof(f22,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& leaf_occ(X1,X0) )
=> ~ ? [X3] : min_precedes(X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_21) ).
fof(f23,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_22) ).
fof(f25,axiom,
! [X0,X1,X2] :
( min_precedes(X1,X2,X0)
=> ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_24) ).
fof(f33,axiom,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> ? [X2,X3,X4] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X3,tptp4)
& min_precedes(X2,X3,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& min_precedes(X3,X4,tptp0)
& ! [X5] :
( min_precedes(X2,X5,tptp0)
=> ( X5 = X3
| X5 = X4 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_32) ).
fof(f40,axiom,
tptp4 != tptp3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_39) ).
fof(f43,axiom,
tptp3 != tptp2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_42) ).
fof(f44,axiom,
tptp3 != tptp1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_43) ).
fof(f46,conjecture,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> ? [X2,X3] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& ( occurrence_of(X3,tptp2)
| occurrence_of(X3,tptp1) )
& min_precedes(X2,X3,tptp0)
& leaf(X3,tptp0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f47,negated_conjecture,
~ ! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> ? [X2,X3] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& ( occurrence_of(X3,tptp2)
| occurrence_of(X3,tptp1) )
& min_precedes(X2,X3,tptp0)
& leaf(X3,tptp0) ) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f48,plain,
! [X0,X1] :
( precedes(X0,X1)
=> ( earlier(X0,X1)
& legal(X1) ) ),
inference(unused_predicate_definition_removal,[],[f9]) ).
fof(f58,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,[],[f5]) ).
fof(f60,plain,
! [X0,X1,X2] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f62,plain,
! [X0,X1] :
( ( earlier(X0,X1)
& legal(X1) )
| ~ precedes(X0,X1) ),
inference(ennf_transformation,[],[f48]) ).
fof(f70,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f75,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(flattening,[],[f75]) ).
fof(f77,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f78,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f77]) ).
fof(f81,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,[],[f25]) ).
fof(f92,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X3,tptp4)
& min_precedes(X2,X3,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& min_precedes(X3,X4,tptp0)
& ! [X5] :
( X5 = X3
| X5 = X4
| ~ min_precedes(X2,X5,tptp0) ) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f33]) ).
fof(f93,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X3,tptp4)
& min_precedes(X2,X3,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& min_precedes(X3,X4,tptp0)
& ! [X5] :
( X5 = X3
| X5 = X4
| ~ min_precedes(X2,X5,tptp0) ) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(flattening,[],[f92]) ).
fof(f94,plain,
? [X0,X1] :
( ! [X2,X3] :
( ~ occurrence_of(X2,tptp3)
| ~ next_subocc(X0,X2,tptp0)
| ( ~ occurrence_of(X3,tptp2)
& ~ occurrence_of(X3,tptp1) )
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf(X3,tptp0) )
& occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f47]) ).
fof(f95,plain,
? [X0,X1] :
( ! [X2,X3] :
( ~ occurrence_of(X2,tptp3)
| ~ next_subocc(X0,X2,tptp0)
| ( ~ occurrence_of(X3,tptp2)
& ~ occurrence_of(X3,tptp1) )
| ~ min_precedes(X2,X3,tptp0)
| ~ leaf(X3,tptp0) )
& occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) ),
inference(flattening,[],[f94]) ).
fof(f103,plain,
! [X2,X0,X1] :
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[],[f58]) ).
fof(f106,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(cnf_transformation,[],[f60]) ).
fof(f108,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| legal(X1) ),
inference(cnf_transformation,[],[f62]) ).
fof(f128,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(cnf_transformation,[],[f70]) ).
fof(f134,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,X2)
| ~ min_precedes(X1,X3,X2) ),
inference(cnf_transformation,[],[f76]) ).
fof(f135,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f78]) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| subactivity_occurrence(X1,sK7(X0,X1,X2)) ),
inference(cnf_transformation,[],[f81]) ).
fof(f140,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| occurrence_of(sK7(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f155,plain,
! [X0,X1,X5] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ~ min_precedes(sK13(X0),X5,tptp0)
| sK15(X0) = X5
| sK14(X0) = X5 ),
inference(cnf_transformation,[],[f93]) ).
fof(f156,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK15(X0),tptp1)
| occurrence_of(sK15(X0),tptp2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f158,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| min_precedes(sK13(X0),sK14(X0),tptp0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f159,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK14(X0),tptp4) ),
inference(cnf_transformation,[],[f93]) ).
fof(f160,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(X0,sK13(X0),tptp0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f161,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK13(X0),tptp3) ),
inference(cnf_transformation,[],[f93]) ).
fof(f168,plain,
tptp3 != tptp4,
inference(cnf_transformation,[],[f40]) ).
fof(f171,plain,
tptp3 != tptp2,
inference(cnf_transformation,[],[f43]) ).
fof(f172,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f44]) ).
fof(f176,plain,
~ leaf_occ(sK16,sK17),
inference(cnf_transformation,[],[f95]) ).
fof(f177,plain,
arboreal(sK16),
inference(cnf_transformation,[],[f95]) ).
fof(f178,plain,
subactivity_occurrence(sK16,sK17),
inference(cnf_transformation,[],[f95]) ).
fof(f179,plain,
occurrence_of(sK17,tptp0),
inference(cnf_transformation,[],[f95]) ).
fof(f182,plain,
! [X2,X0,X1] :
( next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f103]) ).
fof(f204,plain,
! [X0] :
( ~ legal(X0)
| ~ arboreal(X0) ),
inference(consistent_polarity_flipping,[],[f128]) ).
fof(f208,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X1,X3,X2)
| occurrence_of(X0,X2)
| leaf_occ(X1,X0) ),
inference(consistent_polarity_flipping,[],[f134]) ).
fof(f209,plain,
! [X2,X0,X1] :
( occurrence_of(X0,X2)
| occurrence_of(X0,X1)
| X1 = X2 ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f212,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| ~ occurrence_of(sK7(X0,X1,X2),X0) ),
inference(consistent_polarity_flipping,[],[f140]) ).
fof(f225,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| arboreal(X0)
| ~ leaf_occ(X0,X1)
| occurrence_of(X1,tptp0)
| ~ occurrence_of(sK13(X0),tptp3) ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f226,plain,
! [X0,X1] :
( ~ next_subocc(X0,sK13(X0),tptp0)
| arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| occurrence_of(X1,tptp0)
| ~ leaf_occ(X0,X1) ),
inference(consistent_polarity_flipping,[],[f160]) ).
fof(f227,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| arboreal(X0)
| ~ leaf_occ(X0,X1)
| occurrence_of(X1,tptp0)
| ~ occurrence_of(sK14(X0),tptp4) ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f228,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| arboreal(X0)
| ~ leaf_occ(X0,X1)
| occurrence_of(X1,tptp0)
| min_precedes(sK13(X0),sK14(X0),tptp0) ),
inference(consistent_polarity_flipping,[],[f158]) ).
fof(f230,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| arboreal(X0)
| ~ leaf_occ(X0,X1)
| occurrence_of(X1,tptp0)
| ~ occurrence_of(sK15(X0),tptp1)
| ~ occurrence_of(sK15(X0),tptp2) ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f231,plain,
! [X0,X1,X5] :
( ~ min_precedes(sK13(X0),X5,tptp0)
| arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| occurrence_of(X1,tptp0)
| ~ leaf_occ(X0,X1)
| sK15(X0) = X5
| sK14(X0) = X5 ),
inference(consistent_polarity_flipping,[],[f155]) ).
fof(f233,plain,
~ occurrence_of(sK17,tptp0),
inference(consistent_polarity_flipping,[],[f179]) ).
fof(f234,plain,
~ arboreal(sK16),
inference(consistent_polarity_flipping,[],[f177]) ).
fof(f235,plain,
leaf_occ(sK16,sK17),
inference(consistent_polarity_flipping,[],[f176]) ).
fof(f333,plain,
( arboreal(sK16)
| ~ leaf_occ(sK16,sK17)
| occurrence_of(sK17,tptp0)
| ~ occurrence_of(sK14(sK16),tptp4) ),
inference(resolution,[],[f227,f178]) ).
fof(f335,plain,
( ~ leaf_occ(sK16,sK17)
| occurrence_of(sK17,tptp0)
| ~ occurrence_of(sK14(sK16),tptp4) ),
inference(forward_subsumption_resolution,[],[f333,f234]) ).
fof(f336,plain,
( occurrence_of(sK17,tptp0)
| ~ occurrence_of(sK14(sK16),tptp4) ),
inference(forward_subsumption_resolution,[],[f335,f235]) ).
fof(f337,plain,
~ occurrence_of(sK14(sK16),tptp4),
inference(forward_subsumption_resolution,[],[f336,f233]) ).
fof(f338,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| arboreal(X0)
| occurrence_of(X1,tptp0)
| ~ leaf_occ(X0,X1)
| min_precedes(X0,sK13(X0),tptp0) ),
inference(resolution,[],[f226,f182]) ).
fof(f340,plain,
( arboreal(sK16)
| ~ leaf_occ(sK16,sK17)
| occurrence_of(sK17,tptp0)
| min_precedes(sK13(sK16),sK14(sK16),tptp0) ),
inference(resolution,[],[f228,f178]) ).
fof(f342,plain,
( ~ leaf_occ(sK16,sK17)
| occurrence_of(sK17,tptp0)
| min_precedes(sK13(sK16),sK14(sK16),tptp0) ),
inference(forward_subsumption_resolution,[],[f340,f234]) ).
fof(f343,plain,
( occurrence_of(sK17,tptp0)
| min_precedes(sK13(sK16),sK14(sK16),tptp0) ),
inference(forward_subsumption_resolution,[],[f342,f235]) ).
fof(f344,plain,
min_precedes(sK13(sK16),sK14(sK16),tptp0),
inference(forward_subsumption_resolution,[],[f343,f233]) ).
fof(f356,definition,
( spl18_3
<=> occurrence_of(sK15(sK16),tptp2) ),
introduced(definition,[new_symbols(definition,[spl18_3])],[avatar_definition]) ).
fof(f358,plain,
( ~ occurrence_of(sK15(sK16),tptp2)
| spl18_3 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f360,definition,
( spl18_4
<=> occurrence_of(sK15(sK16),tptp1) ),
introduced(definition,[new_symbols(definition,[spl18_4])],[avatar_definition]) ).
fof(f362,plain,
( ~ occurrence_of(sK15(sK16),tptp1)
| spl18_4 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f372,plain,
! [X0] :
( occurrence_of(sK14(sK16),X0)
| tptp4 = X0 ),
inference(resolution,[],[f337,f209]) ).
fof(f376,plain,
( ! [X0] :
( occurrence_of(sK15(sK16),X0)
| tptp2 = X0 )
| spl18_3 ),
inference(resolution,[],[f358,f209]) ).
fof(f387,plain,
subactivity_occurrence(sK13(sK16),sK7(tptp0,sK13(sK16),sK14(sK16))),
inference(resolution,[],[f344,f139]) ).
fof(f392,plain,
! [X0] :
( leaf_occ(sK13(sK16),X0)
| occurrence_of(X0,tptp0) ),
inference(resolution,[],[f344,f208]) ).
fof(f393,plain,
~ occurrence_of(sK7(tptp0,sK13(sK16),sK14(sK16)),tptp0),
inference(resolution,[],[f344,f212]) ).
fof(f475,definition,
( spl18_18
<=> occurrence_of(sK14(sK16),tptp3) ),
introduced(definition,[new_symbols(definition,[spl18_18])],[avatar_definition]) ).
fof(f476,plain,
( ~ occurrence_of(sK14(sK16),tptp3)
| spl18_18 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f631,plain,
( arboreal(sK16)
| occurrence_of(sK17,tptp0)
| ~ leaf_occ(sK16,sK17)
| min_precedes(sK16,sK13(sK16),tptp0) ),
inference(resolution,[],[f338,f178]) ).
fof(f632,plain,
( occurrence_of(sK17,tptp0)
| ~ leaf_occ(sK16,sK17)
| min_precedes(sK16,sK13(sK16),tptp0) ),
inference(forward_subsumption_resolution,[],[f631,f234]) ).
fof(f633,plain,
( ~ leaf_occ(sK16,sK17)
| min_precedes(sK16,sK13(sK16),tptp0) ),
inference(forward_subsumption_resolution,[],[f632,f233]) ).
fof(f634,plain,
min_precedes(sK16,sK13(sK16),tptp0),
inference(forward_subsumption_resolution,[],[f633,f235]) ).
fof(f688,plain,
precedes(sK16,sK13(sK16)),
inference(resolution,[],[f634,f106]) ).
fof(f691,plain,
subactivity_occurrence(sK16,sK7(tptp0,sK16,sK13(sK16))),
inference(resolution,[],[f634,f139]) ).
fof(f696,plain,
! [X0] :
( leaf_occ(sK16,X0)
| occurrence_of(X0,tptp0) ),
inference(resolution,[],[f634,f208]) ).
fof(f697,plain,
~ occurrence_of(sK7(tptp0,sK16,sK13(sK16)),tptp0),
inference(resolution,[],[f634,f212]) ).
fof(f975,definition,
( spl18_49
<=> occurrence_of(sK15(sK16),tptp3) ),
introduced(definition,[new_symbols(definition,[spl18_49])],[avatar_definition]) ).
fof(f976,plain,
( ~ occurrence_of(sK15(sK16),tptp3)
| spl18_49 ),
inference(avatar_component_clause,[],[f975]) ).
fof(f1028,plain,
legal(sK13(sK16)),
inference(resolution,[],[f688,f108]) ).
fof(f1119,plain,
~ arboreal(sK13(sK16)),
inference(resolution,[],[f1028,f204]) ).
fof(f1124,plain,
( arboreal(sK13(sK16))
| ~ leaf_occ(sK13(sK16),sK7(tptp0,sK13(sK16),sK14(sK16)))
| occurrence_of(sK7(tptp0,sK13(sK16),sK14(sK16)),tptp0)
| ~ occurrence_of(sK13(sK13(sK16)),tptp3) ),
inference(resolution,[],[f387,f225]) ).
fof(f1129,plain,
( arboreal(sK13(sK16))
| occurrence_of(sK7(tptp0,sK13(sK16),sK14(sK16)),tptp0)
| ~ leaf_occ(sK13(sK16),sK7(tptp0,sK13(sK16),sK14(sK16)))
| min_precedes(sK13(sK16),sK13(sK13(sK16)),tptp0) ),
inference(resolution,[],[f387,f338]) ).
fof(f1137,definition,
( spl18_66
<=> arboreal(sK13(sK16)) ),
introduced(definition,[new_symbols(definition,[spl18_66])],[avatar_definition]) ).
fof(f1141,plain,
( arboreal(sK13(sK16))
| occurrence_of(sK7(tptp0,sK13(sK16),sK14(sK16)),tptp0)
| min_precedes(sK13(sK16),sK13(sK13(sK16)),tptp0) ),
inference(forward_subsumption_resolution,[],[f1129,f392]) ).
fof(f1146,plain,
( arboreal(sK13(sK16))
| occurrence_of(sK7(tptp0,sK13(sK16),sK14(sK16)),tptp0)
| ~ occurrence_of(sK13(sK13(sK16)),tptp3) ),
inference(forward_subsumption_resolution,[],[f1124,f392]) ).
fof(f1160,plain,
( arboreal(sK13(sK16))
| min_precedes(sK13(sK16),sK13(sK13(sK16)),tptp0) ),
inference(forward_subsumption_resolution,[],[f1141,f393]) ).
fof(f1165,plain,
( arboreal(sK13(sK16))
| ~ occurrence_of(sK13(sK13(sK16)),tptp3) ),
inference(forward_subsumption_resolution,[],[f1146,f393]) ).
fof(f1184,definition,
( spl18_74
<=> min_precedes(sK13(sK16),sK13(sK13(sK16)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl18_74])],[avatar_definition]) ).
fof(f1186,plain,
( min_precedes(sK13(sK16),sK13(sK13(sK16)),tptp0)
| ~ spl18_74 ),
inference(avatar_component_clause,[],[f1184]) ).
fof(f1187,plain,
( spl18_74
| spl18_66 ),
inference(avatar_split_clause,[],[f1160,f1137,f1184]) ).
fof(f1213,definition,
( spl18_80
<=> occurrence_of(sK13(sK13(sK16)),tptp3) ),
introduced(definition,[new_symbols(definition,[spl18_80])],[avatar_definition]) ).
fof(f1215,plain,
( ~ occurrence_of(sK13(sK13(sK16)),tptp3)
| spl18_80 ),
inference(avatar_component_clause,[],[f1213]) ).
fof(f1216,plain,
( ~ spl18_80
| spl18_66 ),
inference(avatar_split_clause,[],[f1165,f1137,f1213]) ).
fof(f1224,plain,
~ spl18_66,
inference(avatar_split_clause,[],[f1119,f1137]) ).
fof(f2607,plain,
( arboreal(sK16)
| ~ leaf_occ(sK16,sK7(tptp0,sK16,sK13(sK16)))
| occurrence_of(sK7(tptp0,sK16,sK13(sK16)),tptp0)
| ~ occurrence_of(sK15(sK16),tptp1)
| ~ occurrence_of(sK15(sK16),tptp2) ),
inference(resolution,[],[f691,f230]) ).
fof(f2614,plain,
( arboreal(sK16)
| occurrence_of(sK7(tptp0,sK16,sK13(sK16)),tptp0)
| ~ occurrence_of(sK15(sK16),tptp1)
| ~ occurrence_of(sK15(sK16),tptp2) ),
inference(forward_subsumption_resolution,[],[f2607,f696]) ).
fof(f3576,plain,
( ! [X0] :
( arboreal(sK16)
| ~ subactivity_occurrence(sK16,X0)
| occurrence_of(X0,tptp0)
| ~ leaf_occ(sK16,X0)
| sK15(sK16) = sK13(sK13(sK16))
| sK14(sK16) = sK13(sK13(sK16)) )
| ~ spl18_74 ),
inference(resolution,[],[f1186,f231]) ).
fof(f3607,plain,
( ! [X0] :
( arboreal(sK16)
| ~ subactivity_occurrence(sK16,X0)
| occurrence_of(X0,tptp0)
| sK15(sK16) = sK13(sK13(sK16))
| sK14(sK16) = sK13(sK13(sK16)) )
| ~ spl18_74 ),
inference(forward_subsumption_resolution,[],[f3576,f696]) ).
fof(f3608,plain,
( ! [X0] :
( ~ subactivity_occurrence(sK16,X0)
| occurrence_of(X0,tptp0)
| sK15(sK16) = sK13(sK13(sK16))
| sK14(sK16) = sK13(sK13(sK16)) )
| ~ spl18_74 ),
inference(forward_subsumption_resolution,[],[f3607,f234]) ).
fof(f3610,definition,
( spl18_147
<=> sK14(sK16) = sK13(sK13(sK16)) ),
introduced(definition,[new_symbols(definition,[spl18_147])],[avatar_definition]) ).
fof(f3612,plain,
( sK14(sK16) = sK13(sK13(sK16))
| ~ spl18_147 ),
inference(avatar_component_clause,[],[f3610]) ).
fof(f3614,definition,
( spl18_148
<=> sK15(sK16) = sK13(sK13(sK16)) ),
introduced(definition,[new_symbols(definition,[spl18_148])],[avatar_definition]) ).
fof(f3616,plain,
( sK15(sK16) = sK13(sK13(sK16))
| ~ spl18_148 ),
inference(avatar_component_clause,[],[f3614]) ).
fof(f3618,definition,
( spl18_149
<=> ! [X0] :
( ~ subactivity_occurrence(sK16,X0)
| occurrence_of(X0,tptp0) ) ),
introduced(definition,[new_symbols(definition,[spl18_149])],[avatar_definition]) ).
fof(f3619,plain,
( ! [X0] :
( ~ subactivity_occurrence(sK16,X0)
| occurrence_of(X0,tptp0) )
| ~ spl18_149 ),
inference(avatar_component_clause,[],[f3618]) ).
fof(f3620,plain,
( spl18_147
| spl18_148
| spl18_149
| ~ spl18_74 ),
inference(avatar_split_clause,[],[f3608,f1184,f3618,f3614,f3610]) ).
fof(f3660,plain,
( ~ occurrence_of(sK14(sK16),tptp3)
| spl18_80
| ~ spl18_147 ),
inference(superposition,[],[f1215,f3612]) ).
fof(f3687,plain,
( ~ occurrence_of(sK15(sK16),tptp3)
| spl18_80
| ~ spl18_148 ),
inference(superposition,[],[f1215,f3616]) ).
fof(f3700,plain,
( ~ spl18_49
| spl18_80
| ~ spl18_148 ),
inference(avatar_split_clause,[],[f3687,f3614,f1213,f975]) ).
fof(f3711,plain,
( occurrence_of(sK17,tptp0)
| ~ spl18_149 ),
inference(resolution,[],[f3619,f178]) ).
fof(f3718,plain,
( $false
| ~ spl18_149 ),
inference(forward_subsumption_resolution,[],[f3711,f233]) ).
fof(f3719,plain,
~ spl18_149,
inference(avatar_contradiction_clause,[],[f3718]) ).
fof(f3720,plain,
( ~ spl18_18
| spl18_80
| ~ spl18_147 ),
inference(avatar_split_clause,[],[f3660,f3610,f1213,f475]) ).
fof(f3726,plain,
( tptp3 = tptp4
| spl18_18 ),
inference(resolution,[],[f476,f372]) ).
fof(f3732,plain,
( $false
| spl18_18 ),
inference(forward_subsumption_resolution,[],[f3726,f168]) ).
fof(f3733,plain,
spl18_18,
inference(avatar_contradiction_clause,[],[f3732]) ).
fof(f3743,plain,
( tptp3 = tptp2
| spl18_3
| spl18_49 ),
inference(resolution,[],[f976,f376]) ).
fof(f3749,plain,
( $false
| spl18_3
| spl18_49 ),
inference(forward_subsumption_resolution,[],[f3743,f171]) ).
fof(f3750,plain,
( spl18_3
| spl18_49 ),
inference(avatar_contradiction_clause,[],[f3749]) ).
fof(f3751,plain,
( occurrence_of(sK7(tptp0,sK16,sK13(sK16)),tptp0)
| ~ occurrence_of(sK15(sK16),tptp1)
| ~ occurrence_of(sK15(sK16),tptp2) ),
inference(forward_subsumption_resolution,[],[f2614,f234]) ).
fof(f3752,plain,
( ~ occurrence_of(sK15(sK16),tptp1)
| ~ occurrence_of(sK15(sK16),tptp2) ),
inference(forward_subsumption_resolution,[],[f3751,f697]) ).
fof(f3753,plain,
( ~ spl18_3
| ~ spl18_4 ),
inference(avatar_split_clause,[],[f3752,f360,f356]) ).
fof(f3755,plain,
( ! [X0] :
( occurrence_of(sK15(sK16),X0)
| tptp1 = X0 )
| spl18_4 ),
inference(resolution,[],[f362,f209]) ).
fof(f3766,plain,
( tptp3 = tptp1
| spl18_4
| spl18_49 ),
inference(resolution,[],[f3755,f976]) ).
fof(f3770,plain,
( $false
| spl18_4
| spl18_49 ),
inference(forward_subsumption_resolution,[],[f3766,f172]) ).
fof(f3771,plain,
( spl18_4
| spl18_49 ),
inference(avatar_contradiction_clause,[],[f3770]) ).
cnf(s59,plain,
( spl18_66
| spl18_74 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s64,plain,
( spl18_66
| ~ spl18_80 ),
inference(sat_conversion,[],[f1216]) ).
cnf(s66,plain,
~ spl18_66,
inference(sat_conversion,[],[f1224]) ).
cnf(s150,plain,
( ~ spl18_74
| spl18_147
| spl18_148
| spl18_149 ),
inference(sat_conversion,[],[f3620]) ).
cnf(s156,plain,
( ~ spl18_49
| spl18_80
| ~ spl18_148 ),
inference(sat_conversion,[],[f3700]) ).
cnf(s162,plain,
~ spl18_149,
inference(sat_conversion,[],[f3719]) ).
cnf(s163,plain,
( ~ spl18_18
| spl18_80
| ~ spl18_147 ),
inference(sat_conversion,[],[f3720]) ).
cnf(s167,plain,
spl18_18,
inference(sat_conversion,[],[f3733]) ).
cnf(s176,plain,
( spl18_3
| spl18_49 ),
inference(sat_conversion,[],[f3750]) ).
cnf(s177,plain,
( ~ spl18_3
| ~ spl18_4 ),
inference(sat_conversion,[],[f3753]) ).
cnf(s178,plain,
( spl18_4
| spl18_49 ),
inference(sat_conversion,[],[f3771]) ).
cnf(s180,plain,
( spl18_80
| ~ spl18_147 ),
inference(rat,[],[s163,s167]) ).
cnf(s183,plain,
( ~ spl18_74
| spl18_147
| spl18_148 ),
inference(rat,[],[s150,s162]) ).
cnf(s186,plain,
~ spl18_80,
inference(rat,[],[s64,s66]) ).
cnf(s187,plain,
~ spl18_147,
inference(rat,[],[s180,s186]) ).
cnf(s192,plain,
spl18_74,
inference(rat,[],[s59,s66]) ).
cnf(s193,plain,
spl18_148,
inference(rat,[],[s183,s187,s192]) ).
cnf(s195,plain,
~ spl18_49,
inference(rat,[],[s156,s186,s193]) ).
cnf(s196,plain,
spl18_4,
inference(rat,[],[s178,s195]) ).
cnf(s197,plain,
spl18_3,
inference(rat,[],[s176,s195]) ).
cnf(s198,plain,
$false,
inference(rat,[],[s177,s196,s197]) ).
fof(f3772,plain,
$false,
inference(avatar_sat_refutation,[],[s198]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO017+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.37 % Computer : n017.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sun Sep 27 22:20:36 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.41 Running first-order model finding
% 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.93/0.59 % (2993931)Will run a generic schedule for satisfiability detection.
% 0.93/0.59 % (2993939)dis+10_1_sil=32000:sp=arity:random_seed=3024657541:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.93/0.59 % (2993937)% WARNING: option uhcvi not known.
% 0.93/0.59 % (2993936)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2591084013_2999 on theBenchmark for (2999ds/0Mi)
% 0.93/0.59 % (2993940)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3366957259:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.93/0.59 % (2993941)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=809228343:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.93/0.59 % (2993938)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1875711643:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.93/0.59 % (2993937)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3512811549:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.93/0.59 % (2993942)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2451511879:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.93/0.59 % Detected minimum model sizes of [4]
% 0.93/0.59 % Detected maximum model sizes of [max]
% 0.93/0.59 % TRYING [4]
% 0.93/0.59 % TRYING [5]
% 0.93/0.59 % (2993939)Instruction limit reached!
% 0.93/0.59 % (2993939)------------------------------
% 0.93/0.59 % (2993939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.59 % (2993939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.59 % (2993939)CaDiCaL version: 2.1.3
% 0.93/0.59 % (2993939)Termination reason: Instruction limit
% 0.93/0.59 % (2993939)Termination phase: Saturation
% 0.93/0.59 % (2993939)Time elapsed: 0.039 s
% 0.93/0.59 % (2993939)Peak memory usage: 13 MB
% 0.93/0.59 % (2993939)Instructions burned: 105 (million)
% 0.93/0.59 % TRYING [6]
% 0.93/0.59 % (2993950)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1754727061:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.93/0.59 % Detected minimum model sizes of [4]
% 0.93/0.59 % Detected maximum model sizes of [max]
% 0.93/0.59 % TRYING [4]
% 0.93/0.59 % TRYING [5]
% 0.93/0.59 % (2993940)Instruction limit reached!
% 0.93/0.59 % (2993940)------------------------------
% 0.93/0.59 % (2993940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.59 % (2993940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.59 % (2993940)CaDiCaL version: 2.1.3
% 0.93/0.59 % (2993940)Termination reason: Instruction limit
% 0.93/0.59 % (2993940)Termination phase: Saturation
% 0.93/0.59 % (2993940)Time elapsed: 0.076 s
% 0.93/0.59 % (2993940)Peak memory usage: 12 MB
% 0.93/0.59 % (2993940)Instructions burned: 118 (million)
% 0.93/0.59 % (2993941)Instruction limit reached!
% 0.93/0.59 % (2993941)------------------------------
% 0.93/0.59 % (2993941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.59 % (2993941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.59 % (2993941)CaDiCaL version: 2.1.3
% 0.93/0.59 % (2993941)Termination reason: Instruction limit
% 0.93/0.59 % (2993941)Termination phase: Saturation
% 0.93/0.59 % (2993941)Time elapsed: 0.087 s
% 0.93/0.59 % (2993941)Peak memory usage: 13 MB
% 0.93/0.59 % (2993941)Instructions burned: 131 (million)
% 0.93/0.59 % TRYING [6]
% 0.93/0.59 % (2993952)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3055539251:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.93/0.59 % (2993953)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=3937764585:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.93/0.59 % (2993942)Instruction limit reached!
% 0.93/0.59 % (2993942)------------------------------
% 0.93/0.59 % (2993942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.59 % (2993942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.59 % (2993942)CaDiCaL version: 2.1.3
% 0.93/0.59 % (2993942)Termination reason: Instruction limit
% 0.93/0.59 % (2993942)Termination phase: Saturation
% 0.93/0.59 % (2993942)Time elapsed: 0.115 s
% 0.93/0.59 % (2993942)Peak memory usage: 14 MB
% 0.93/0.59 % (2993942)Instructions burned: 159 (million)
% 0.93/0.59 % (2993937) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2993931-2993937"...
% 0.93/0.59 % (2993937)...printing done.
% 0.93/0.59 % (2993937)Refutation found. Thanks to Tanya!
% 0.93/0.59 % SZS status Theorem for theBenchmark
% 0.93/0.59 % SZS output start Proof for theBenchmark
% See solution above
% 0.93/0.60 % (2993937)------------------------------
% 0.93/0.60 % (2993937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.93/0.60 % (2993937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.93/0.60 % (2993937)CaDiCaL version: 2.1.3
% 0.93/0.60 % (2993937)Termination reason: Refutation
% 0.93/0.60 % (2993937)Time elapsed: 0.132 s
% 0.93/0.60 % (2993937)Peak memory usage: 14 MB
% 0.93/0.60 % (2993937)Instructions burned: 211 (million)
% 0.93/0.60 % (2993931)Success in time 0.175 s
% 0.93/0.60 % Vampire exiting
%------------------------------------------------------------------------------