%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRO008+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:36 PM UTC 2026
% Result : Theorem 81.31s 11.96s
% Output : Refutation 81.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 42
% Syntax : Number of formulae : 348 ( 92 unt; 11 def)
% Number of atoms : 1062 ( 59 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 1210 ( 496 ~; 522 |; 148 &)
% ( 17 <=>; 27 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 11 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 6 con; 0-3 aty)
% Number of variables : 426 ( 0 sgn 384 !; 42 ?)
% 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(f4,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_03) ).
fof(f5,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& arboreal(X2)
& arboreal(X3)
& subactivity_occurrence(X2,X1)
& subactivity_occurrence(X3,X1) )
=> ( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_04) ).
fof(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(f12,axiom,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
=> ( activity_occurrence(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_11) ).
fof(f13,axiom,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_12) ).
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(f19,axiom,
! [X0,X1] :
( leaf_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_18) ).
fof(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(f22,axiom,
! [X0,X1] :
( precedes(X0,X1)
<=> ( earlier(X0,X1)
& legal(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_21) ).
fof(f24,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ? [X3] :
( root(X3,X2)
& min_precedes(X3,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_23) ).
fof(f25,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> precedes(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_24) ).
fof(f27,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ~ ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_26) ).
fof(f28,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X0,X1,X2)
& occurrence_of(X3,X2)
& subactivity_occurrence(X1,X3) )
=> subactivity_occurrence(X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_27) ).
fof(f29,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X2,X3)
& ~ atomic(X3)
& leaf_occ(X0,X2)
& leaf_occ(X1,X2) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_28) ).
fof(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(f31,axiom,
! [X0,X1,X2] :
( ( earlier(X0,X1)
& earlier(X1,X2) )
=> earlier(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_30) ).
fof(f32,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X0,X1,X3)
& min_precedes(X0,X2,X3)
& precedes(X1,X2) )
=> min_precedes(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_31) ).
fof(f33,axiom,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2,X3] :
( occurrence_of(X1,tptp3)
& root_occ(X1,X0)
& occurrence_of(X2,tptp4)
& next_subocc(X1,X2,tptp0)
& ( occurrence_of(X3,tptp1)
| occurrence_of(X3,tptp2) )
& next_subocc(X2,X3,tptp0)
& leaf_occ(X3,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_32) ).
fof(f35,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_34) ).
fof(f36,axiom,
atomic(tptp4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_35) ).
fof(f37,axiom,
atomic(tptp1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_36) ).
fof(f38,axiom,
atomic(tptp2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_37) ).
fof(f41,axiom,
tptp4 != tptp1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_40) ).
fof(f42,axiom,
tptp4 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_41) ).
fof(f45,axiom,
tptp1 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_44) ).
fof(f46,conjecture,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( occurrence_of(X1,tptp3)
& root_occ(X1,X0)
& ( occurrence_of(X2,tptp1)
| occurrence_of(X2,tptp2) )
& min_precedes(X1,X2,tptp0)
& leaf_occ(X2,X0)
& ( occurrence_of(X2,tptp1)
=> ~ ? [X3] :
( occurrence_of(X3,tptp2)
& subactivity_occurrence(X3,X0)
& min_precedes(X1,X3,tptp0) ) )
& ( occurrence_of(X2,tptp2)
=> ~ ? [X4] :
( occurrence_of(X4,tptp1)
& subactivity_occurrence(X4,X0)
& min_precedes(X1,X4,tptp0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f47,negated_conjecture,
~ ! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( occurrence_of(X1,tptp3)
& root_occ(X1,X0)
& ( occurrence_of(X2,tptp1)
| occurrence_of(X2,tptp2) )
& min_precedes(X1,X2,tptp0)
& leaf_occ(X2,X0)
& ( occurrence_of(X2,tptp1)
=> ~ ? [X3] :
( occurrence_of(X3,tptp2)
& subactivity_occurrence(X3,X0)
& min_precedes(X1,X3,tptp0) ) )
& ( occurrence_of(X2,tptp2)
=> ~ ? [X4] :
( occurrence_of(X4,tptp1)
& subactivity_occurrence(X4,X0)
& min_precedes(X1,X4,tptp0) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f51,plain,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] : occurrence_of(X0,X1) ),
inference(pure_predicate_removal,[],[f13]) ).
fof(f52,plain,
! [X0,X1] :
( occurrence_of(X1,X0)
=> activity_occurrence(X1) ),
inference(pure_predicate_removal,[],[f4]) ).
fof(f54,plain,
! [X0,X1] :
( ? [X2] :
( root(X2,X0)
& subactivity_occurrence(X2,X1) )
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f55,plain,
! [X0,X1] :
( ? [X2] :
( root(X2,X0)
& subactivity_occurrence(X2,X1) )
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(flattening,[],[f54]) ).
fof(f58,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(f59,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,[],[f58]) ).
fof(f60,plain,
! [X0,X1] :
( activity_occurrence(X1)
| ~ occurrence_of(X1,X0) ),
inference(ennf_transformation,[],[f52]) ).
fof(f61,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| ~ subactivity_occurrence(X3,X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f62,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| ~ subactivity_occurrence(X3,X1) ),
inference(flattening,[],[f61]) ).
fof(f64,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(f67,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f9]) ).
fof(f68,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f67]) ).
fof(f73,plain,
! [X0,X1] :
( ( activity_occurrence(X0)
& activity_occurrence(X1) )
| ~ subactivity_occurrence(X0,X1) ),
inference(ennf_transformation,[],[f12]) ).
fof(f74,plain,
! [X0] :
( ? [X1] : occurrence_of(X0,X1)
| ~ activity_occurrence(X0) ),
inference(ennf_transformation,[],[f51]) ).
fof(f75,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f78,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f79,plain,
! [X0,X1] :
( legal(X0)
| ~ root(X0,X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ? [X3] :
( root(X3,X2)
& min_precedes(X3,X1,X2) )
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f24]) ).
fof(f83,plain,
! [X0,X1,X2] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f25]) ).
fof(f85,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(f86,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ min_precedes(X0,X1,X2)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(ennf_transformation,[],[f28]) ).
fof(f87,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ min_precedes(X0,X1,X2)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(flattening,[],[f86]) ).
fof(f88,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| ~ leaf_occ(X1,X2) ),
inference(ennf_transformation,[],[f29]) ).
fof(f89,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| ~ leaf_occ(X1,X2) ),
inference(flattening,[],[f88]) ).
fof(f90,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| ~ root_occ(X1,X2) ),
inference(ennf_transformation,[],[f30]) ).
fof(f91,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| ~ root_occ(X1,X2) ),
inference(flattening,[],[f90]) ).
fof(f92,plain,
! [X0,X1,X2] :
( earlier(X0,X2)
| ~ earlier(X0,X1)
| ~ earlier(X1,X2) ),
inference(ennf_transformation,[],[f31]) ).
fof(f93,plain,
! [X0,X1,X2] :
( earlier(X0,X2)
| ~ earlier(X0,X1)
| ~ earlier(X1,X2) ),
inference(flattening,[],[f92]) ).
fof(f94,plain,
! [X0,X1,X2,X3] :
( min_precedes(X1,X2,X3)
| ~ min_precedes(X0,X1,X3)
| ~ min_precedes(X0,X2,X3)
| ~ precedes(X1,X2) ),
inference(ennf_transformation,[],[f32]) ).
fof(f95,plain,
! [X0,X1,X2,X3] :
( min_precedes(X1,X2,X3)
| ~ min_precedes(X0,X1,X3)
| ~ min_precedes(X0,X2,X3)
| ~ precedes(X1,X2) ),
inference(flattening,[],[f94]) ).
fof(f96,plain,
! [X0] :
( ? [X1,X2,X3] :
( occurrence_of(X1,tptp3)
& root_occ(X1,X0)
& occurrence_of(X2,tptp4)
& next_subocc(X1,X2,tptp0)
& ( occurrence_of(X3,tptp1)
| occurrence_of(X3,tptp2) )
& next_subocc(X2,X3,tptp0)
& leaf_occ(X3,X0) )
| ~ occurrence_of(X0,tptp0) ),
inference(ennf_transformation,[],[f33]) ).
fof(f97,plain,
? [X0] :
( ! [X1,X2] :
( ~ occurrence_of(X1,tptp3)
| ~ root_occ(X1,X0)
| ( ~ occurrence_of(X2,tptp1)
& ~ occurrence_of(X2,tptp2) )
| ~ min_precedes(X1,X2,tptp0)
| ~ leaf_occ(X2,X0)
| ( ? [X3] :
( occurrence_of(X3,tptp2)
& subactivity_occurrence(X3,X0)
& min_precedes(X1,X3,tptp0) )
& occurrence_of(X2,tptp1) )
| ( ? [X4] :
( occurrence_of(X4,tptp1)
& subactivity_occurrence(X4,X0)
& min_precedes(X1,X4,tptp0) )
& occurrence_of(X2,tptp2) ) )
& occurrence_of(X0,tptp0) ),
inference(ennf_transformation,[],[f47]) ).
fof(f98,definition,
! [X0,X1,X2] :
( ( ? [X4] :
( occurrence_of(X4,tptp1)
& subactivity_occurrence(X4,X0)
& min_precedes(X1,X4,tptp0) )
& occurrence_of(X2,tptp2) )
| ~ sP0(X0,X1,X2) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f99,plain,
? [X0] :
( ! [X1,X2] :
( ~ occurrence_of(X1,tptp3)
| ~ root_occ(X1,X0)
| ( ~ occurrence_of(X2,tptp1)
& ~ occurrence_of(X2,tptp2) )
| ~ min_precedes(X1,X2,tptp0)
| ~ leaf_occ(X2,X0)
| ( ? [X3] :
( occurrence_of(X3,tptp2)
& subactivity_occurrence(X3,X0)
& min_precedes(X1,X3,tptp0) )
& occurrence_of(X2,tptp1) )
| sP0(X0,X1,X2) )
& occurrence_of(X0,tptp0) ),
inference(definition_folding,[],[f97,f98]) ).
fof(f100,plain,
! [X0,X1] :
( ( root(sK1(X0,X1),X0)
& subactivity_occurrence(sK1(X0,X1),X1) )
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0,X1))],[f55]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK3(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK3(X0,X1,X2))
& subactivity_occurrence(X2,sK3(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X3,sK3(X0,X1,X2))],[f64]) ).
fof(f104,plain,
! [X0] :
( occurrence_of(X0,sK5(X0))
| ~ activity_occurrence(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X1,sK5(X0))],[f74]) ).
fof(f110,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f78]) ).
fof(f111,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) )
| ~ leaf_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f19]) ).
fof(f112,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ? [X3] :
( occurrence_of(X1,X3)
& subactivity_occurrence(X0,X1)
& leaf(X0,X3) )
| ~ leaf_occ(X0,X1) ) ),
inference(rectify,[],[f111]) ).
fof(f113,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ( occurrence_of(X1,sK9(X0,X1))
& subactivity_occurrence(X0,X1)
& leaf(X0,sK9(X0,X1)) )
| ~ leaf_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X3,sK9(X0,X1))],[f112]) ).
fof(f114,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(f115,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,[],[f114]) ).
fof(f116,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ( occurrence_of(X1,sK10(X0,X1))
& subactivity_occurrence(X0,X1)
& root(X0,sK10(X0,X1)) )
| ~ root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X3,sK10(X0,X1))],[f115]) ).
fof(f117,plain,
! [X0,X1] :
( ( precedes(X0,X1)
| ~ earlier(X0,X1)
| ~ legal(X1) )
& ( ( earlier(X0,X1)
& legal(X1) )
| ~ precedes(X0,X1) ) ),
inference(nnf_transformation,[],[f22]) ).
fof(f118,plain,
! [X0,X1] :
( ( precedes(X0,X1)
| ~ earlier(X0,X1)
| ~ legal(X1) )
& ( ( earlier(X0,X1)
& legal(X1) )
| ~ precedes(X0,X1) ) ),
inference(flattening,[],[f117]) ).
fof(f119,plain,
! [X0,X1,X2] :
( ( root(sK11(X1,X2),X2)
& min_precedes(sK11(X1,X2),X1,X2) )
| ~ min_precedes(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X3,sK11(X1,X2))],[f82]) ).
fof(f120,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,[],[f85]) ).
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(flattening,[],[f120]) ).
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)
& ! [X4] :
( ~ min_precedes(X0,X4,X2)
| ~ min_precedes(X4,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(rectify,[],[f121]) ).
fof(f123,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ( min_precedes(X0,sK12(X0,X1,X2),X2)
& min_precedes(sK12(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,[sK12]),skolemize(X3,sK12(X0,X1,X2))],[f122]) ).
fof(f124,plain,
! [X0] :
( ( occurrence_of(sK13(X0),tptp3)
& root_occ(sK13(X0),X0)
& occurrence_of(sK14(X0),tptp4)
& next_subocc(sK13(X0),sK14(X0),tptp0)
& ( occurrence_of(sK15(X0),tptp1)
| occurrence_of(sK15(X0),tptp2) )
& next_subocc(sK14(X0),sK15(X0),tptp0)
& leaf_occ(sK15(X0),X0) )
| ~ occurrence_of(X0,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15]),skolemize(X1,sK13(X0)),skolemize(X2,sK14(X0)),skolemize(X3,sK15(X0))],[f96]) ).
fof(f125,plain,
! [X0,X1,X2] :
( ( ? [X4] :
( occurrence_of(X4,tptp1)
& subactivity_occurrence(X4,X0)
& min_precedes(X1,X4,tptp0) )
& occurrence_of(X2,tptp2) )
| ~ sP0(X0,X1,X2) ),
inference(nnf_transformation,[],[f98]) ).
fof(f126,plain,
! [X0,X1,X2] :
( ( ? [X3] :
( occurrence_of(X3,tptp1)
& subactivity_occurrence(X3,X0)
& min_precedes(X1,X3,tptp0) )
& occurrence_of(X2,tptp2) )
| ~ sP0(X0,X1,X2) ),
inference(rectify,[],[f125]) ).
fof(f127,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK16(X0,X1),tptp1)
& subactivity_occurrence(sK16(X0,X1),X0)
& min_precedes(X1,sK16(X0,X1),tptp0)
& occurrence_of(X2,tptp2) )
| ~ sP0(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X3,sK16(X0,X1))],[f126]) ).
fof(f128,plain,
( ! [X1,X2] :
( ~ occurrence_of(X1,tptp3)
| ~ root_occ(X1,sK17)
| ( ~ occurrence_of(X2,tptp1)
& ~ occurrence_of(X2,tptp2) )
| ~ min_precedes(X1,X2,tptp0)
| ~ leaf_occ(X2,sK17)
| ( occurrence_of(sK18(X1),tptp2)
& subactivity_occurrence(sK18(X1),sK17)
& min_precedes(X1,sK18(X1),tptp0)
& occurrence_of(X2,tptp1) )
| sP0(sK17,X1,X2) )
& occurrence_of(sK17,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18]),skolemize(X0,sK17),skolemize(X3,sK18(X1))],[f99]) ).
fof(f129,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| subactivity_occurrence(sK1(X0,X1),X1)
| atomic(X0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f130,plain,
! [X0,X1] :
( root(sK1(X0,X1),X0)
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f132,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,[],[f59]) ).
fof(f133,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f60]) ).
fof(f134,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,[],[f62]) ).
fof(f136,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK3(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f137,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X1,sK3(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f138,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| occurrence_of(sK3(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f141,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f68]) ).
fof(f144,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f73]) ).
fof(f145,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| activity_occurrence(X0) ),
inference(cnf_transformation,[],[f73]) ).
fof(f146,plain,
! [X0] :
( ~ activity_occurrence(X0)
| occurrence_of(X0,sK5(X0)) ),
inference(cnf_transformation,[],[f104]) ).
fof(f147,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(cnf_transformation,[],[f75]) ).
fof(f154,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ arboreal(X0)
| atomic(X1) ),
inference(cnf_transformation,[],[f110]) ).
fof(f155,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f156,plain,
! [X0,X1] :
( ~ root(X0,X1)
| legal(X0) ),
inference(cnf_transformation,[],[f79]) ).
fof(f157,plain,
! [X0,X1] :
( leaf(X0,sK9(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f158,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f159,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| occurrence_of(X1,sK9(X0,X1)) ),
inference(cnf_transformation,[],[f113]) ).
fof(f160,plain,
! [X2,X0,X1] :
( ~ leaf(X0,X2)
| ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f161,plain,
! [X0,X1] :
( root(X0,sK10(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f116]) ).
fof(f163,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| occurrence_of(X1,sK10(X0,X1)) ),
inference(cnf_transformation,[],[f116]) ).
fof(f164,plain,
! [X2,X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2)
| root_occ(X0,X1)
| ~ root(X0,X2) ),
inference(cnf_transformation,[],[f116]) ).
fof(f166,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| legal(X1) ),
inference(cnf_transformation,[],[f118]) ).
fof(f167,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| earlier(X0,X1) ),
inference(cnf_transformation,[],[f118]) ).
fof(f168,plain,
! [X0,X1] :
( ~ earlier(X0,X1)
| precedes(X0,X1)
| ~ legal(X1) ),
inference(cnf_transformation,[],[f118]) ).
fof(f170,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| min_precedes(sK11(X1,X2),X1,X2) ),
inference(cnf_transformation,[],[f119]) ).
fof(f171,plain,
! [X2,X0,X1] :
( root(sK11(X1,X2),X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f119]) ).
fof(f172,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(cnf_transformation,[],[f83]) ).
fof(f175,plain,
! [X2,X0,X1,X4] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) ),
inference(cnf_transformation,[],[f123]) ).
fof(f176,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f123]) ).
fof(f179,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| subactivity_occurrence(X0,X3)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(cnf_transformation,[],[f87]) ).
fof(f180,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X1,X2)
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f89]) ).
fof(f181,plain,
! [X2,X3,X0,X1] :
( ~ root_occ(X1,X2)
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f91]) ).
fof(f182,plain,
! [X2,X0,X1] :
( ~ earlier(X1,X2)
| ~ earlier(X0,X1)
| earlier(X0,X2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f183,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X0,X2,X3)
| ~ min_precedes(X0,X1,X3)
| min_precedes(X1,X2,X3)
| ~ precedes(X1,X2) ),
inference(cnf_transformation,[],[f95]) ).
fof(f184,plain,
! [X0] :
( leaf_occ(sK15(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f185,plain,
! [X0] :
( next_subocc(sK14(X0),sK15(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f186,plain,
! [X0] :
( occurrence_of(sK15(X0),tptp2)
| occurrence_of(sK15(X0),tptp1)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f187,plain,
! [X0] :
( next_subocc(sK13(X0),sK14(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f188,plain,
! [X0] :
( occurrence_of(sK14(X0),tptp4)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f189,plain,
! [X0] :
( root_occ(sK13(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f190,plain,
! [X0] :
( occurrence_of(sK13(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f191,plain,
~ atomic(tptp0),
inference(cnf_transformation,[],[f35]) ).
fof(f192,plain,
atomic(tptp4),
inference(cnf_transformation,[],[f36]) ).
fof(f193,plain,
atomic(tptp1),
inference(cnf_transformation,[],[f37]) ).
fof(f194,plain,
atomic(tptp2),
inference(cnf_transformation,[],[f38]) ).
fof(f197,plain,
tptp4 != tptp1,
inference(cnf_transformation,[],[f41]) ).
fof(f198,plain,
tptp4 != tptp2,
inference(cnf_transformation,[],[f42]) ).
fof(f201,plain,
tptp1 != tptp2,
inference(cnf_transformation,[],[f45]) ).
fof(f202,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| occurrence_of(X2,tptp2) ),
inference(cnf_transformation,[],[f127]) ).
fof(f203,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| min_precedes(X1,sK16(X0,X1),tptp0) ),
inference(cnf_transformation,[],[f127]) ).
fof(f204,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| subactivity_occurrence(sK16(X0,X1),X0) ),
inference(cnf_transformation,[],[f127]) ).
fof(f205,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| occurrence_of(sK16(X0,X1),tptp1) ),
inference(cnf_transformation,[],[f127]) ).
fof(f206,plain,
occurrence_of(sK17,tptp0),
inference(cnf_transformation,[],[f128]) ).
fof(f207,plain,
! [X2,X1] :
( ~ min_precedes(X1,X2,tptp0)
| ~ root_occ(X1,sK17)
| ~ occurrence_of(X2,tptp2)
| ~ occurrence_of(X1,tptp3)
| ~ leaf_occ(X2,sK17)
| occurrence_of(X2,tptp1)
| sP0(sK17,X1,X2) ),
inference(cnf_transformation,[],[f128]) ).
fof(f212,plain,
! [X2,X1] :
( ~ min_precedes(X1,X2,tptp0)
| ~ root_occ(X1,sK17)
| ~ occurrence_of(X2,tptp1)
| ~ occurrence_of(X1,tptp3)
| ~ leaf_occ(X2,sK17)
| min_precedes(X1,sK18(X1),tptp0)
| sP0(sK17,X1,X2) ),
inference(cnf_transformation,[],[f128]) ).
fof(f213,plain,
! [X2,X1] :
( ~ min_precedes(X1,X2,tptp0)
| ~ root_occ(X1,sK17)
| ~ occurrence_of(X2,tptp1)
| ~ occurrence_of(X1,tptp3)
| ~ leaf_occ(X2,sK17)
| subactivity_occurrence(sK18(X1),sK17)
| sP0(sK17,X1,X2) ),
inference(cnf_transformation,[],[f128]) ).
fof(f214,plain,
! [X2,X1] :
( ~ min_precedes(X1,X2,tptp0)
| ~ root_occ(X1,sK17)
| ~ occurrence_of(X2,tptp1)
| ~ occurrence_of(X1,tptp3)
| ~ leaf_occ(X2,sK17)
| occurrence_of(sK18(X1),tptp2)
| sP0(sK17,X1,X2) ),
inference(cnf_transformation,[],[f128]) ).
fof(f215,plain,
activity_occurrence(sK17),
inference(unit_resulting_resolution,[],[f133,f206]) ).
fof(f223,plain,
~ arboreal(sK17),
inference(unit_resulting_resolution,[],[f154,f191,f206]) ).
fof(f243,plain,
leaf_occ(sK15(sK17),sK17),
inference(unit_resulting_resolution,[],[f184,f206]) ).
fof(f245,plain,
subactivity_occurrence(sK15(sK17),sK17),
inference(unit_resulting_resolution,[],[f158,f243]) ).
fof(f247,plain,
activity_occurrence(sK15(sK17)),
inference(unit_resulting_resolution,[],[f145,f245]) ).
fof(f251,plain,
occurrence_of(sK15(sK17),sK5(sK15(sK17))),
inference(unit_resulting_resolution,[],[f146,f247]) ).
fof(f253,plain,
occurrence_of(sK14(sK17),tptp4),
inference(unit_resulting_resolution,[],[f188,f206]) ).
fof(f254,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp4)
| arboreal(sK14(X0)) ),
inference(resolution,[],[f188,f155]) ).
fof(f257,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK14(X0)) ),
inference(forward_subsumption_resolution,[],[f254,f192]) ).
fof(f258,plain,
arboreal(sK14(sK17)),
inference(unit_resulting_resolution,[],[f155,f192,f253]) ).
fof(f259,plain,
activity_occurrence(sK14(sK17)),
inference(unit_resulting_resolution,[],[f133,f253]) ).
fof(f267,plain,
occurrence_of(sK14(sK17),sK5(sK14(sK17))),
inference(unit_resulting_resolution,[],[f146,f259]) ).
fof(f309,plain,
root_occ(sK13(sK17),sK17),
inference(unit_resulting_resolution,[],[f189,f206]) ).
fof(f347,plain,
occurrence_of(sK13(sK17),tptp3),
inference(unit_resulting_resolution,[],[f190,f206]) ).
fof(f389,plain,
leaf(sK15(sK17),sK9(sK15(sK17),sK17)),
inference(unit_resulting_resolution,[],[f157,f243]) ).
fof(f391,plain,
occurrence_of(sK17,sK9(sK15(sK17),sK17)),
inference(unit_resulting_resolution,[],[f159,f243]) ).
fof(f403,plain,
root(sK13(sK17),sK10(sK13(sK17),sK17)),
inference(unit_resulting_resolution,[],[f161,f309]) ).
fof(f447,plain,
occurrence_of(sK17,sK10(sK13(sK17),sK17)),
inference(unit_resulting_resolution,[],[f163,f309]) ).
fof(f450,plain,
~ atomic(sK10(sK13(sK17),sK17)),
inference(unit_resulting_resolution,[],[f155,f223,f447]) ).
fof(f466,plain,
~ occurrence_of(sK14(sK17),tptp1),
inference(unit_resulting_resolution,[],[f141,f197,f253]) ).
fof(f485,plain,
tptp4 = sK5(sK14(sK17)),
inference(unit_resulting_resolution,[],[f141,f267,f253]) ).
fof(f491,plain,
tptp0 = sK9(sK15(sK17),sK17),
inference(unit_resulting_resolution,[],[f141,f391,f206]) ).
fof(f492,plain,
tptp0 = sK10(sK13(sK17),sK17),
inference(unit_resulting_resolution,[],[f141,f447,f206]) ).
fof(f512,plain,
! [X0] :
( ~ occurrence_of(sK15(sK17),X0)
| sK5(sK15(sK17)) = X0 ),
inference(resolution,[],[f141,f251]) ).
fof(f547,plain,
leaf(sK15(sK17),tptp0),
inference(superposition,[],[f389,f491]) ).
fof(f557,plain,
root(sK13(sK17),tptp0),
inference(superposition,[],[f403,f492]) ).
fof(f609,plain,
next_subocc(sK14(sK17),sK15(sK17),tptp0),
inference(unit_resulting_resolution,[],[f185,f206]) ).
fof(f613,plain,
! [X0] :
( min_precedes(sK14(X0),sK15(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f185,f176]) ).
fof(f634,plain,
min_precedes(sK14(sK17),sK15(sK17),tptp0),
inference(unit_resulting_resolution,[],[f176,f609]) ).
fof(f641,plain,
root(sK11(sK15(sK17),tptp0),tptp0),
inference(unit_resulting_resolution,[],[f171,f634]) ).
fof(f642,plain,
precedes(sK14(sK17),sK15(sK17)),
inference(unit_resulting_resolution,[],[f172,f634]) ).
fof(f656,plain,
next_subocc(sK13(sK17),sK14(sK17),tptp0),
inference(unit_resulting_resolution,[],[f187,f206]) ).
fof(f657,plain,
! [X0] :
( min_precedes(sK13(X0),sK14(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f187,f176]) ).
fof(f662,plain,
earlier(sK14(sK17),sK15(sK17)),
inference(unit_resulting_resolution,[],[f167,f642]) ).
fof(f683,plain,
min_precedes(sK13(sK17),sK14(sK17),tptp0),
inference(unit_resulting_resolution,[],[f176,f656]) ).
fof(f691,plain,
precedes(sK13(sK17),sK14(sK17)),
inference(unit_resulting_resolution,[],[f172,f683]) ).
fof(f707,plain,
earlier(sK13(sK17),sK14(sK17)),
inference(unit_resulting_resolution,[],[f167,f691]) ).
fof(f708,plain,
legal(sK14(sK17)),
inference(unit_resulting_resolution,[],[f166,f691]) ).
fof(f726,plain,
! [X0] :
( ~ earlier(X0,sK13(sK17))
| earlier(X0,sK14(sK17)) ),
inference(resolution,[],[f707,f182]) ).
fof(f931,plain,
subactivity_occurrence(sK1(tptp0,sK17),sK17),
inference(unit_resulting_resolution,[],[f129,f191,f206]) ).
fof(f978,definition,
( spl19_5
<=> arboreal(sK1(tptp0,sK17)) ),
introduced(definition,[new_symbols(definition,[spl19_5])],[avatar_definition]) ).
fof(f979,plain,
( ~ arboreal(sK1(tptp0,sK17))
| spl19_5 ),
inference(avatar_component_clause,[],[f978]) ).
fof(f980,plain,
( arboreal(sK1(tptp0,sK17))
| ~ spl19_5 ),
inference(avatar_component_clause,[],[f978]) ).
fof(f1009,plain,
( ~ legal(sK1(tptp0,sK17))
| spl19_5 ),
inference(unit_resulting_resolution,[],[f147,f979]) ).
fof(f1017,plain,
( ! [X0] : ~ root(sK1(tptp0,sK17),X0)
| spl19_5 ),
inference(unit_resulting_resolution,[],[f156,f1009]) ).
fof(f1094,plain,
root(sK1(tptp0,sK17),tptp0),
inference(unit_resulting_resolution,[],[f130,f191,f206]) ).
fof(f1097,plain,
root(sK1(sK10(sK13(sK17),sK17),sK17),sK10(sK13(sK17),sK17)),
inference(unit_resulting_resolution,[],[f130,f450,f447]) ).
fof(f1111,plain,
root(sK1(tptp0,sK17),tptp0),
inference(forward_demodulation,[],[f1097,f492]) ).
fof(f1122,plain,
( $false
| spl19_5 ),
inference(forward_subsumption_resolution,[],[f1111,f1017]) ).
fof(f1123,plain,
spl19_5,
inference(avatar_contradiction_clause,[],[f1122]) ).
fof(f1232,plain,
subactivity_occurrence(sK15(sK17),sK3(tptp0,sK14(sK17),sK15(sK17))),
inference(unit_resulting_resolution,[],[f136,f634]) ).
fof(f1237,plain,
activity_occurrence(sK3(tptp0,sK14(sK17),sK15(sK17))),
inference(unit_resulting_resolution,[],[f144,f1232]) ).
fof(f1240,plain,
occurrence_of(sK3(tptp0,sK14(sK17),sK15(sK17)),sK5(sK3(tptp0,sK14(sK17),sK15(sK17)))),
inference(unit_resulting_resolution,[],[f146,f1237]) ).
fof(f1324,plain,
subactivity_occurrence(sK14(sK17),sK3(tptp0,sK14(sK17),sK15(sK17))),
inference(unit_resulting_resolution,[],[f137,f634]) ).
fof(f1435,plain,
occurrence_of(sK3(tptp0,sK14(sK17),sK15(sK17)),tptp0),
inference(unit_resulting_resolution,[],[f138,f634]) ).
fof(f1449,plain,
arboreal(sK14(sK3(tptp0,sK14(sK17),sK15(sK17)))),
inference(unit_resulting_resolution,[],[f257,f1435]) ).
fof(f2247,plain,
min_precedes(sK11(sK15(sK17),tptp0),sK15(sK17),tptp0),
inference(unit_resulting_resolution,[],[f170,f634]) ).
fof(f2724,plain,
( occurrence_of(sK15(sK17),tptp1)
| ~ occurrence_of(sK17,tptp0)
| tptp2 = sK5(sK15(sK17)) ),
inference(resolution,[],[f186,f512]) ).
fof(f2731,plain,
( occurrence_of(sK15(sK17),tptp1)
| tptp2 = sK5(sK15(sK17)) ),
inference(forward_subsumption_resolution,[],[f2724,f206]) ).
fof(f2733,definition,
( spl19_15
<=> tptp2 = sK5(sK15(sK17)) ),
introduced(definition,[new_symbols(definition,[spl19_15])],[avatar_definition]) ).
fof(f2735,plain,
( tptp2 = sK5(sK15(sK17))
| ~ spl19_15 ),
inference(avatar_component_clause,[],[f2733]) ).
fof(f2737,definition,
( spl19_16
<=> occurrence_of(sK15(sK17),tptp1) ),
introduced(definition,[new_symbols(definition,[spl19_16])],[avatar_definition]) ).
fof(f2738,plain,
( ~ occurrence_of(sK15(sK17),tptp1)
| spl19_16 ),
inference(avatar_component_clause,[],[f2737]) ).
fof(f2739,plain,
( occurrence_of(sK15(sK17),tptp1)
| ~ spl19_16 ),
inference(avatar_component_clause,[],[f2737]) ).
fof(f2740,plain,
( spl19_15
| spl19_16 ),
inference(avatar_split_clause,[],[f2731,f2737,f2733]) ).
fof(f2741,plain,
( occurrence_of(sK15(sK17),tptp2)
| ~ spl19_15 ),
inference(superposition,[],[f251,f2735]) ).
fof(f3487,plain,
leaf_occ(sK15(sK17),sK3(tptp0,sK14(sK17),sK15(sK17))),
inference(unit_resulting_resolution,[],[f160,f1435,f1232,f547]) ).
fof(f3652,plain,
root_occ(sK1(tptp0,sK17),sK17),
inference(unit_resulting_resolution,[],[f164,f206,f1094,f931]) ).
fof(f3913,plain,
! [X0] :
( ~ min_precedes(sK14(sK17),X0,tptp0)
| ~ min_precedes(X0,sK15(sK17),tptp0) ),
inference(resolution,[],[f175,f609]) ).
fof(f3915,plain,
! [X0] :
( ~ min_precedes(sK13(sK17),X0,tptp0)
| ~ min_precedes(X0,sK14(sK17),tptp0) ),
inference(resolution,[],[f175,f656]) ).
fof(f3935,plain,
sK13(sK17) = sK1(tptp0,sK17),
inference(unit_resulting_resolution,[],[f181,f206,f3652,f309]) ).
fof(f3945,plain,
! [X2,X0,X1] :
( ~ root_occ(X2,X0)
| ~ occurrence_of(X0,X1)
| sK13(X0) = X2
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f181,f189]) ).
fof(f3949,plain,
! [X0,X1] :
( ~ occurrence_of(sK17,X0)
| ~ root_occ(X1,sK17)
| sK13(sK17) = X1 ),
inference(resolution,[],[f181,f309]) ).
fof(f4161,definition,
( spl19_17
<=> ! [X1] :
( ~ root_occ(X1,sK17)
| sK13(sK17) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl19_17])],[avatar_definition]) ).
fof(f4162,plain,
( ! [X1] :
( ~ root_occ(X1,sK17)
| sK13(sK17) = X1 )
| ~ spl19_17 ),
inference(avatar_component_clause,[],[f4161]) ).
fof(f4164,definition,
( spl19_18
<=> ! [X0] : ~ occurrence_of(sK17,X0) ),
introduced(definition,[new_symbols(definition,[spl19_18])],[avatar_definition]) ).
fof(f4165,plain,
( ! [X0] : ~ occurrence_of(sK17,X0)
| ~ spl19_18 ),
inference(avatar_component_clause,[],[f4164]) ).
fof(f4166,plain,
( spl19_17
| spl19_18 ),
inference(avatar_split_clause,[],[f3949,f4164,f4161]) ).
fof(f4366,plain,
subactivity_occurrence(sK11(sK15(sK17),tptp0),sK17),
inference(unit_resulting_resolution,[],[f179,f206,f245,f2247]) ).
fof(f4375,plain,
subactivity_occurrence(sK13(sK17),sK3(tptp0,sK14(sK17),sK15(sK17))),
inference(unit_resulting_resolution,[],[f179,f1435,f1324,f683]) ).
fof(f4377,plain,
subactivity_occurrence(sK14(sK17),sK17),
inference(unit_resulting_resolution,[],[f179,f206,f245,f634]) ).
fof(f4432,plain,
root_occ(sK11(sK15(sK17),tptp0),sK17),
inference(unit_resulting_resolution,[],[f164,f206,f641,f4366]) ).
fof(f4462,plain,
( sK13(sK17) = sK11(sK15(sK17),tptp0)
| ~ spl19_17 ),
inference(unit_resulting_resolution,[],[f4162,f4432]) ).
fof(f4577,plain,
( min_precedes(sK13(sK17),sK15(sK17),tptp0)
| ~ spl19_17 ),
inference(superposition,[],[f2247,f4462]) ).
fof(f4643,plain,
( sP0(sK17,sK13(sK17),sK15(sK17))
| ~ spl19_15
| spl19_16
| ~ spl19_17 ),
inference(unit_resulting_resolution,[],[f207,f309,f2738,f243,f347,f2741,f4577]) ).
fof(f4714,plain,
( occurrence_of(sK16(sK17,sK13(sK17)),tptp1)
| ~ spl19_15
| spl19_16
| ~ spl19_17 ),
inference(unit_resulting_resolution,[],[f205,f4643]) ).
fof(f4715,plain,
( subactivity_occurrence(sK16(sK17,sK13(sK17)),sK17)
| ~ spl19_15
| spl19_16
| ~ spl19_17 ),
inference(unit_resulting_resolution,[],[f204,f4643]) ).
fof(f4730,plain,
( arboreal(sK16(sK17,sK13(sK17)))
| ~ spl19_15
| spl19_16
| ~ spl19_17 ),
inference(unit_resulting_resolution,[],[f155,f193,f4714]) ).
fof(f5090,plain,
! [X2,X0,X1] :
( ~ leaf_occ(X2,X0)
| atomic(X1)
| ~ occurrence_of(X0,X1)
| sK15(X0) = X2
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f180,f184]) ).
fof(f5608,plain,
root_occ(sK13(sK17),sK3(tptp0,sK14(sK17),sK15(sK17))),
inference(unit_resulting_resolution,[],[f164,f557,f1435,f4375]) ).
fof(f5981,plain,
! [X0] :
( ~ min_precedes(sK13(sK17),X0,tptp0)
| min_precedes(X0,sK14(sK17),tptp0)
| ~ precedes(X0,sK14(sK17)) ),
inference(resolution,[],[f183,f683]) ).
fof(f5984,plain,
! [X0] :
( ~ min_precedes(sK14(sK17),X0,tptp0)
| min_precedes(X0,sK15(sK17),tptp0)
| ~ precedes(X0,sK15(sK17)) ),
inference(resolution,[],[f183,f634]) ).
fof(f5988,plain,
! [X0] :
( ~ min_precedes(sK14(sK17),X0,tptp0)
| ~ precedes(X0,sK15(sK17)) ),
inference(forward_subsumption_resolution,[],[f5984,f3913]) ).
fof(f5989,plain,
! [X0] :
( ~ min_precedes(sK13(sK17),X0,tptp0)
| ~ precedes(X0,sK14(sK17)) ),
inference(forward_subsumption_resolution,[],[f5981,f3915]) ).
fof(f6139,plain,
! [X2,X0,X1] :
( ~ subactivity_occurrence(X2,X0)
| ~ occurrence_of(X0,X1)
| sK15(X0) = X2
| ~ arboreal(X2)
| min_precedes(X2,sK15(X0),X1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f132,f184]) ).
fof(f8745,definition,
( spl19_21
<=> occurrence_of(sK18(sK13(sK17)),tptp2) ),
introduced(definition,[new_symbols(definition,[spl19_21])],[avatar_definition]) ).
fof(f8747,plain,
( occurrence_of(sK18(sK13(sK17)),tptp2)
| ~ spl19_21 ),
inference(avatar_component_clause,[],[f8745]) ).
fof(f9375,plain,
sK13(sK17) = sK13(sK3(tptp0,sK14(sK17),sK15(sK17))),
inference(unit_resulting_resolution,[],[f3945,f1240,f5608,f1435]) ).
fof(f9447,plain,
( next_subocc(sK13(sK17),sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),tptp0)
| ~ occurrence_of(sK3(tptp0,sK14(sK17),sK15(sK17)),tptp0) ),
inference(superposition,[],[f187,f9375]) ).
fof(f9454,plain,
( min_precedes(sK13(sK17),sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),tptp0)
| ~ occurrence_of(sK3(tptp0,sK14(sK17),sK15(sK17)),tptp0) ),
inference(superposition,[],[f657,f9375]) ).
fof(f9457,plain,
min_precedes(sK13(sK17),sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),tptp0),
inference(forward_subsumption_resolution,[],[f9454,f1435]) ).
fof(f9459,plain,
next_subocc(sK13(sK17),sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),tptp0),
inference(forward_subsumption_resolution,[],[f9447,f1435]) ).
fof(f9627,plain,
~ precedes(sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),sK14(sK17)),
inference(unit_resulting_resolution,[],[f5989,f9457]) ).
fof(f9628,plain,
~ min_precedes(sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),sK14(sK17),tptp0),
inference(unit_resulting_resolution,[],[f3915,f9457]) ).
fof(f9699,plain,
~ earlier(sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),sK14(sK17)),
inference(unit_resulting_resolution,[],[f168,f708,f9627]) ).
fof(f9712,plain,
~ earlier(sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),sK13(sK17)),
inference(unit_resulting_resolution,[],[f726,f9699]) ).
fof(f9756,plain,
~ min_precedes(sK14(sK17),sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),tptp0),
inference(unit_resulting_resolution,[],[f175,f683,f9459]) ).
fof(f10244,plain,
sK15(sK17) = sK15(sK3(tptp0,sK14(sK17),sK15(sK17))),
inference(unit_resulting_resolution,[],[f5090,f191,f3487,f1435,f1435]) ).
fof(f10280,plain,
( min_precedes(sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),sK15(sK17),tptp0)
| ~ occurrence_of(sK3(tptp0,sK14(sK17),sK15(sK17)),tptp0) ),
inference(superposition,[],[f613,f10244]) ).
fof(f10298,plain,
min_precedes(sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),sK15(sK17),tptp0),
inference(forward_subsumption_resolution,[],[f10280,f1435]) ).
fof(f10367,plain,
subactivity_occurrence(sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),sK17),
inference(unit_resulting_resolution,[],[f179,f206,f245,f10298]) ).
fof(f10411,plain,
sK14(sK17) = sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),
inference(unit_resulting_resolution,[],[f134,f206,f258,f4377,f1449,f9628,f9756,f10367]) ).
fof(f12381,plain,
! [X0] :
( ~ occurrence_of(sK17,X0)
| sK15(sK17) = sK1(tptp0,sK17)
| ~ arboreal(sK1(tptp0,sK17))
| min_precedes(sK1(tptp0,sK17),sK15(sK17),X0)
| ~ occurrence_of(sK17,tptp0) ),
inference(resolution,[],[f6139,f931]) ).
fof(f12411,plain,
( ! [X0] :
( ~ occurrence_of(sK17,X0)
| sK15(sK17) = sK1(tptp0,sK17)
| min_precedes(sK1(tptp0,sK17),sK15(sK17),X0)
| ~ occurrence_of(sK17,tptp0) )
| ~ spl19_5 ),
inference(forward_subsumption_resolution,[],[f12381,f980]) ).
fof(f12447,plain,
( ! [X0] :
( ~ occurrence_of(sK17,X0)
| sK15(sK17) = sK1(tptp0,sK17)
| min_precedes(sK1(tptp0,sK17),sK15(sK17),X0) )
| ~ spl19_5 ),
inference(forward_subsumption_resolution,[],[f12411,f206]) ).
fof(f12477,plain,
( ! [X0] :
( sK15(sK17) = sK13(sK17)
| ~ occurrence_of(sK17,X0)
| min_precedes(sK1(tptp0,sK17),sK15(sK17),X0) )
| ~ spl19_5 ),
inference(forward_demodulation,[],[f12447,f3935]) ).
fof(f12499,plain,
( ! [X0] :
( min_precedes(sK13(sK17),sK15(sK17),X0)
| sK15(sK17) = sK13(sK17)
| ~ occurrence_of(sK17,X0) )
| ~ spl19_5 ),
inference(forward_demodulation,[],[f12477,f3935]) ).
fof(f13516,definition,
( spl19_25
<=> sK15(sK17) = sK13(sK17) ),
introduced(definition,[new_symbols(definition,[spl19_25])],[avatar_definition]) ).
fof(f13518,plain,
( sK15(sK17) = sK13(sK17)
| ~ spl19_25 ),
inference(avatar_component_clause,[],[f13516]) ).
fof(f13520,definition,
( spl19_26
<=> ! [X0] :
( min_precedes(sK13(sK17),sK15(sK17),X0)
| ~ occurrence_of(sK17,X0) ) ),
introduced(definition,[new_symbols(definition,[spl19_26])],[avatar_definition]) ).
fof(f13521,plain,
( ! [X0] :
( min_precedes(sK13(sK17),sK15(sK17),X0)
| ~ occurrence_of(sK17,X0) )
| ~ spl19_26 ),
inference(avatar_component_clause,[],[f13520]) ).
fof(f13522,plain,
( spl19_25
| spl19_26
| ~ spl19_5 ),
inference(avatar_split_clause,[],[f12499,f978,f13520,f13516]) ).
fof(f14105,plain,
( ~ earlier(sK14(sK3(tptp0,sK14(sK17),sK15(sK17))),sK15(sK17))
| ~ spl19_25 ),
inference(superposition,[],[f9712,f13518]) ).
fof(f14308,plain,
( ~ earlier(sK14(sK17),sK15(sK17))
| ~ spl19_25 ),
inference(forward_demodulation,[],[f14105,f10411]) ).
fof(f14421,plain,
( $false
| ~ spl19_25 ),
inference(forward_subsumption_resolution,[],[f14308,f662]) ).
fof(f14422,plain,
~ spl19_25,
inference(avatar_contradiction_clause,[],[f14421]) ).
fof(f14653,plain,
( ! [X0] :
( min_precedes(sK11(sK15(sK17),X0),sK15(sK17),X0)
| ~ occurrence_of(sK17,X0) )
| ~ spl19_26 ),
inference(resolution,[],[f13521,f170]) ).
fof(f14795,plain,
( ~ occurrence_of(sK17,tptp0)
| ~ root_occ(sK11(sK15(sK17),tptp0),sK17)
| ~ occurrence_of(sK15(sK17),tptp2)
| ~ occurrence_of(sK11(sK15(sK17),tptp0),tptp3)
| ~ leaf_occ(sK15(sK17),sK17)
| occurrence_of(sK15(sK17),tptp1)
| sP0(sK17,sK11(sK15(sK17),tptp0),sK15(sK17))
| ~ spl19_26 ),
inference(resolution,[],[f14653,f207]) ).
fof(f14825,plain,
( ~ occurrence_of(sK17,tptp0)
| ~ root_occ(sK11(sK15(sK17),tptp0),sK17)
| ~ occurrence_of(sK11(sK15(sK17),tptp0),tptp3)
| ~ leaf_occ(sK15(sK17),sK17)
| occurrence_of(sK15(sK17),tptp1)
| sP0(sK17,sK11(sK15(sK17),tptp0),sK15(sK17))
| ~ spl19_26 ),
inference(forward_subsumption_resolution,[],[f14795,f186]) ).
fof(f14833,plain,
( ~ occurrence_of(sK17,tptp0)
| ~ root_occ(sK11(sK15(sK17),tptp0),sK17)
| ~ occurrence_of(sK11(sK15(sK17),tptp0),tptp3)
| occurrence_of(sK15(sK17),tptp1)
| sP0(sK17,sK11(sK15(sK17),tptp0),sK15(sK17))
| ~ spl19_26 ),
inference(forward_subsumption_resolution,[],[f14825,f184]) ).
fof(f14837,plain,
( ~ root_occ(sK11(sK15(sK17),tptp0),sK17)
| ~ occurrence_of(sK11(sK15(sK17),tptp0),tptp3)
| occurrence_of(sK15(sK17),tptp1)
| sP0(sK17,sK11(sK15(sK17),tptp0),sK15(sK17))
| ~ spl19_26 ),
inference(forward_subsumption_resolution,[],[f14833,f206]) ).
fof(f14841,plain,
( ~ occurrence_of(sK11(sK15(sK17),tptp0),tptp3)
| occurrence_of(sK15(sK17),tptp1)
| sP0(sK17,sK11(sK15(sK17),tptp0),sK15(sK17))
| ~ spl19_26 ),
inference(forward_subsumption_resolution,[],[f14837,f4432]) ).
fof(f14845,plain,
( ~ occurrence_of(sK11(sK15(sK17),tptp0),tptp3)
| sP0(sK17,sK11(sK15(sK17),tptp0),sK15(sK17))
| spl19_16
| ~ spl19_26 ),
inference(forward_subsumption_resolution,[],[f14841,f2738]) ).
fof(f14849,plain,
( ~ occurrence_of(sK13(sK17),tptp3)
| sP0(sK17,sK11(sK15(sK17),tptp0),sK15(sK17))
| spl19_16
| ~ spl19_17
| ~ spl19_26 ),
inference(forward_demodulation,[],[f14845,f4462]) ).
fof(f14853,plain,
( sP0(sK17,sK11(sK15(sK17),tptp0),sK15(sK17))
| spl19_16
| ~ spl19_17
| ~ spl19_26 ),
inference(forward_subsumption_resolution,[],[f14849,f347]) ).
fof(f14857,plain,
( sP0(sK17,sK13(sK17),sK15(sK17))
| spl19_16
| ~ spl19_17
| ~ spl19_26 ),
inference(forward_demodulation,[],[f14853,f4462]) ).
fof(f31039,definition,
( spl19_33
<=> precedes(sK16(sK17,sK13(sK17)),sK15(sK17)) ),
introduced(definition,[new_symbols(definition,[spl19_33])],[avatar_definition]) ).
fof(f31040,plain,
( precedes(sK16(sK17,sK13(sK17)),sK15(sK17))
| ~ spl19_33 ),
inference(avatar_component_clause,[],[f31039]) ).
fof(f31041,plain,
( ~ precedes(sK16(sK17,sK13(sK17)),sK15(sK17))
| spl19_33 ),
inference(avatar_component_clause,[],[f31039]) ).
fof(f31048,plain,
( ! [X0] : ~ min_precedes(sK16(sK17,sK13(sK17)),sK15(sK17),X0)
| spl19_33 ),
inference(unit_resulting_resolution,[],[f172,f31041]) ).
fof(f31103,plain,
( sK15(sK17) = sK16(sK17,sK13(sK17))
| ~ spl19_15
| spl19_16
| ~ spl19_17
| spl19_33 ),
inference(unit_resulting_resolution,[],[f6139,f206,f206,f4730,f4715,f31048]) ).
fof(f31118,plain,
( occurrence_of(sK15(sK17),tptp1)
| ~ spl19_15
| spl19_16
| ~ spl19_17
| spl19_33 ),
inference(superposition,[],[f4714,f31103]) ).
fof(f31439,plain,
( $false
| ~ spl19_15
| spl19_16
| ~ spl19_17
| spl19_33 ),
inference(forward_subsumption_resolution,[],[f31118,f2738]) ).
fof(f31440,plain,
( ~ spl19_15
| spl19_16
| ~ spl19_17
| spl19_33 ),
inference(avatar_contradiction_clause,[],[f31439]) ).
fof(f31644,plain,
( ~ occurrence_of(sK15(sK17),tptp2)
| ~ spl19_16 ),
inference(unit_resulting_resolution,[],[f141,f201,f2739]) ).
fof(f31664,plain,
( ! [X0,X1] : ~ sP0(X0,X1,sK15(sK17))
| ~ spl19_16 ),
inference(unit_resulting_resolution,[],[f202,f31644]) ).
fof(f31678,plain,
( min_precedes(sK13(sK17),sK18(sK13(sK17)),tptp0)
| ~ spl19_16
| ~ spl19_17 ),
inference(unit_resulting_resolution,[],[f212,f309,f347,f4577,f243,f2739,f31664]) ).
fof(f31679,plain,
( subactivity_occurrence(sK18(sK13(sK17)),sK17)
| ~ spl19_16
| ~ spl19_17 ),
inference(unit_resulting_resolution,[],[f213,f347,f309,f4577,f243,f2739,f31664]) ).
fof(f31680,plain,
( occurrence_of(sK18(sK13(sK17)),tptp2)
| ~ spl19_16
| ~ spl19_17 ),
inference(unit_resulting_resolution,[],[f214,f347,f309,f4577,f243,f2739,f31664]) ).
fof(f31689,plain,
( activity_occurrence(sK18(sK13(sK17)))
| ~ spl19_16
| ~ spl19_17 ),
inference(unit_resulting_resolution,[],[f145,f31679]) ).
fof(f31698,plain,
( occurrence_of(sK18(sK13(sK17)),sK5(sK18(sK13(sK17))))
| ~ spl19_16
| ~ spl19_17 ),
inference(unit_resulting_resolution,[],[f146,f31689]) ).
fof(f31700,plain,
( spl19_21
| ~ spl19_16
| ~ spl19_17 ),
inference(avatar_split_clause,[],[f31680,f4161,f2737,f8745]) ).
fof(f31712,plain,
( arboreal(sK18(sK13(sK17)))
| ~ spl19_21 ),
inference(unit_resulting_resolution,[],[f155,f194,f8747]) ).
fof(f31769,plain,
( ~ min_precedes(sK18(sK13(sK17)),sK14(sK17),tptp0)
| ~ spl19_16
| ~ spl19_17 ),
inference(unit_resulting_resolution,[],[f3915,f31678]) ).
fof(f32294,plain,
( tptp2 = sK5(sK18(sK13(sK17)))
| ~ spl19_16
| ~ spl19_17
| ~ spl19_21 ),
inference(unit_resulting_resolution,[],[f141,f8747,f31698]) ).
fof(f36965,definition,
( spl19_37
<=> precedes(sK18(sK13(sK17)),sK15(sK17)) ),
introduced(definition,[new_symbols(definition,[spl19_37])],[avatar_definition]) ).
fof(f36966,plain,
( precedes(sK18(sK13(sK17)),sK15(sK17))
| ~ spl19_37 ),
inference(avatar_component_clause,[],[f36965]) ).
fof(f36967,plain,
( ~ precedes(sK18(sK13(sK17)),sK15(sK17))
| spl19_37 ),
inference(avatar_component_clause,[],[f36965]) ).
fof(f36974,plain,
( ! [X0] : ~ min_precedes(sK18(sK13(sK17)),sK15(sK17),X0)
| spl19_37 ),
inference(unit_resulting_resolution,[],[f172,f36967]) ).
fof(f37029,plain,
( sK15(sK17) = sK18(sK13(sK17))
| ~ spl19_16
| ~ spl19_17
| ~ spl19_21
| spl19_37 ),
inference(unit_resulting_resolution,[],[f6139,f206,f206,f31712,f31679,f36974]) ).
fof(f37043,plain,
( occurrence_of(sK15(sK17),tptp2)
| ~ spl19_16
| ~ spl19_17
| ~ spl19_21
| spl19_37 ),
inference(superposition,[],[f8747,f37029]) ).
fof(f37324,plain,
( $false
| ~ spl19_16
| ~ spl19_17
| ~ spl19_21
| spl19_37 ),
inference(forward_subsumption_resolution,[],[f37043,f31644]) ).
fof(f37325,plain,
( ~ spl19_16
| ~ spl19_17
| ~ spl19_21
| spl19_37 ),
inference(avatar_contradiction_clause,[],[f37324]) ).
fof(f37327,plain,
( ~ min_precedes(sK14(sK17),sK18(sK13(sK17)),tptp0)
| ~ spl19_37 ),
inference(unit_resulting_resolution,[],[f5988,f36966]) ).
fof(f37463,plain,
( sK14(sK17) = sK18(sK13(sK17))
| ~ spl19_16
| ~ spl19_17
| ~ spl19_21
| ~ spl19_37 ),
inference(unit_resulting_resolution,[],[f134,f258,f206,f4377,f31679,f31712,f31769,f37327]) ).
fof(f37482,plain,
( tptp4 = sK5(sK18(sK13(sK17)))
| ~ spl19_16
| ~ spl19_17
| ~ spl19_21
| ~ spl19_37 ),
inference(superposition,[],[f485,f37463]) ).
fof(f38960,plain,
( tptp4 = tptp2
| ~ spl19_16
| ~ spl19_17
| ~ spl19_21
| ~ spl19_37 ),
inference(forward_demodulation,[],[f37482,f32294]) ).
fof(f39000,plain,
( $false
| ~ spl19_16
| ~ spl19_17
| ~ spl19_21
| ~ spl19_37 ),
inference(forward_subsumption_resolution,[],[f38960,f198]) ).
fof(f39001,plain,
( ~ spl19_16
| ~ spl19_17
| ~ spl19_21
| ~ spl19_37 ),
inference(avatar_contradiction_clause,[],[f39000]) ).
fof(f39196,plain,
( ~ activity_occurrence(sK17)
| ~ spl19_18 ),
inference(unit_resulting_resolution,[],[f146,f4165]) ).
fof(f39227,plain,
( $false
| ~ spl19_18 ),
inference(forward_subsumption_resolution,[],[f39196,f215]) ).
fof(f39228,plain,
~ spl19_18,
inference(avatar_contradiction_clause,[],[f39227]) ).
fof(f39503,plain,
( min_precedes(sK13(sK17),sK16(sK17,sK13(sK17)),tptp0)
| spl19_16
| ~ spl19_17
| ~ spl19_26 ),
inference(unit_resulting_resolution,[],[f203,f14857]) ).
fof(f39504,plain,
( occurrence_of(sK16(sK17,sK13(sK17)),tptp1)
| spl19_16
| ~ spl19_17
| ~ spl19_26 ),
inference(unit_resulting_resolution,[],[f205,f14857]) ).
fof(f39505,plain,
( subactivity_occurrence(sK16(sK17,sK13(sK17)),sK17)
| spl19_16
| ~ spl19_17
| ~ spl19_26 ),
inference(unit_resulting_resolution,[],[f204,f14857]) ).
fof(f40110,plain,
( ~ min_precedes(sK14(sK17),sK16(sK17,sK13(sK17)),tptp0)
| ~ spl19_33 ),
inference(unit_resulting_resolution,[],[f5988,f31040]) ).
fof(f40736,plain,
( ~ min_precedes(sK16(sK17,sK13(sK17)),sK14(sK17),tptp0)
| spl19_16
| ~ spl19_17
| ~ spl19_26 ),
inference(unit_resulting_resolution,[],[f3915,f39503]) ).
fof(f41152,plain,
( sK14(sK17) = sK16(sK17,sK13(sK17))
| ~ spl19_15
| spl19_16
| ~ spl19_17
| ~ spl19_26
| ~ spl19_33 ),
inference(unit_resulting_resolution,[],[f134,f258,f206,f4377,f39505,f4730,f40736,f40110]) ).
fof(f41183,plain,
( occurrence_of(sK14(sK17),tptp1)
| ~ spl19_15
| spl19_16
| ~ spl19_17
| ~ spl19_26
| ~ spl19_33 ),
inference(superposition,[],[f39504,f41152]) ).
fof(f41198,plain,
( $false
| ~ spl19_15
| spl19_16
| ~ spl19_17
| ~ spl19_26
| ~ spl19_33 ),
inference(forward_subsumption_resolution,[],[f41183,f466]) ).
fof(f41199,plain,
( ~ spl19_15
| spl19_16
| ~ spl19_17
| ~ spl19_26
| ~ spl19_33 ),
inference(avatar_contradiction_clause,[],[f41198]) ).
cnf(s25,plain,
spl19_5,
inference(sat_conversion,[],[f1123]) ).
cnf(s30,plain,
( spl19_15
| spl19_16 ),
inference(sat_conversion,[],[f2740]) ).
cnf(s32,plain,
( spl19_17
| spl19_18 ),
inference(sat_conversion,[],[f4166]) ).
cnf(s37,plain,
( ~ spl19_5
| spl19_25
| spl19_26 ),
inference(sat_conversion,[],[f13522]) ).
cnf(s92,plain,
~ spl19_25,
inference(sat_conversion,[],[f14422]) ).
cnf(s143,plain,
( ~ spl19_15
| spl19_16
| ~ spl19_17
| spl19_33 ),
inference(sat_conversion,[],[f31440]) ).
cnf(s144,plain,
( ~ spl19_16
| ~ spl19_17
| spl19_21 ),
inference(sat_conversion,[],[f31700]) ).
cnf(s157,plain,
( ~ spl19_16
| ~ spl19_17
| ~ spl19_21
| spl19_37 ),
inference(sat_conversion,[],[f37325]) ).
cnf(s161,plain,
( ~ spl19_16
| ~ spl19_17
| ~ spl19_21
| ~ spl19_37 ),
inference(sat_conversion,[],[f39001]) ).
cnf(s173,plain,
~ spl19_18,
inference(sat_conversion,[],[f39228]) ).
cnf(s175,plain,
( ~ spl19_15
| spl19_16
| ~ spl19_17
| ~ spl19_26
| ~ spl19_33 ),
inference(sat_conversion,[],[f41199]) ).
cnf(s177,plain,
( ~ spl19_5
| spl19_26 ),
inference(rat,[],[s37,s92]) ).
cnf(s178,plain,
spl19_17,
inference(rat,[],[s32,s173]) ).
cnf(s179,plain,
spl19_26,
inference(rat,[],[s177,s25]) ).
cnf(s183,plain,
( ~ spl19_21
| ~ spl19_16 ),
inference(rat,[],[s157,s161,s178]) ).
cnf(s184,plain,
~ spl19_16,
inference(rat,[],[s183,s144,s178]) ).
cnf(s185,plain,
spl19_15,
inference(rat,[],[s30,s184]) ).
cnf(s186,plain,
spl19_33,
inference(rat,[],[s143,s184,s178,s185]) ).
cnf(s187,plain,
$false,
inference(rat,[],[s175,s184,s179,s178,s186,s185]) ).
fof(f41200,plain,
$false,
inference(avatar_sat_refutation,[],[s187]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO008+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:19:15 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.61/2.94 % (2464956)Will run a generic schedule for satisfiability detection.
% 16.61/2.94 % (2464961)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=619507246_2999 on theBenchmark for (2999ds/0Mi)
% 16.61/2.94 % Detected minimum model sizes of [4]
% 16.61/2.94 % Detected maximum model sizes of [max]
% 16.61/2.94 % (2464962)% WARNING: option uhcvi not known.
% 16.61/2.94 % TRYING [4]
% 16.61/2.94 % (2464962)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=482673458:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.61/2.94 % (2464963)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1781223277:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.61/2.94 % (2464964)dis+10_1_sil=32000:sp=arity:random_seed=1436697706:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.61/2.94 % (2464965)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1532524789:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.61/2.94 % (2464967)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3151712061:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.61/2.94 % (2464966)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2891137231:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.61/2.94 % TRYING [5]
% 16.61/2.94 % TRYING [6]
% 16.61/2.94 % TRYING [7]
% 16.61/2.94 % (2464964)Instruction limit reached!
% 16.61/2.94 % (2464964)------------------------------
% 16.61/2.94 % (2464964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.61/2.94 % (2464964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.61/2.94 % (2464964)CaDiCaL version: 2.1.3
% 16.61/2.94 % (2464964)Termination reason: Instruction limit
% 16.61/2.94 % (2464964)Termination phase: Saturation
% 16.61/2.94 % (2464964)Time elapsed: 0.067 s
% 16.61/2.94 % (2464964)Peak memory usage: 12 MB
% 16.61/2.94 % (2464964)Instructions burned: 104 (million)
% 16.61/2.94 % (2464965)Instruction limit reached!
% 16.61/2.94 % (2464965)------------------------------
% 16.61/2.94 % (2464965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.61/2.94 % (2464965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.61/2.94 % (2464965)CaDiCaL version: 2.1.3
% 16.61/2.94 % (2464965)Termination reason: Instruction limit
% 16.61/2.94 % (2464965)Termination phase: Saturation
% 16.61/2.94 % (2464965)Time elapsed: 0.070 s
% 16.61/2.94 % (2464965)Peak memory usage: 12 MB
% 16.61/2.94 % (2464965)Instructions burned: 117 (million)
% 16.61/2.94 % (2464966)Instruction limit reached!
% 16.61/2.94 % (2464966)------------------------------
% 16.61/2.94 % (2464966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.61/2.94 % (2464966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.61/2.94 % (2464966)CaDiCaL version: 2.1.3
% 16.61/2.94 % (2464966)Termination reason: Instruction limit
% 16.61/2.94 % (2464966)Termination phase: Saturation
% 16.61/2.94 % (2464966)Time elapsed: 0.085 s
% 16.61/2.94 % (2464966)Peak memory usage: 13 MB
% 16.61/2.94 % (2464966)Instructions burned: 131 (million)
% 16.61/2.94 % (2464975)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2335287087:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 16.61/2.94 % (2464976)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1986275643:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.61/2.94 % Detected minimum model sizes of [4]
% 16.61/2.94 % Detected maximum model sizes of [max]
% 16.61/2.94 % TRYING [4]
% 16.61/2.94 % TRYING [5]
% 16.61/2.94 % (2464977)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=2109402815:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.61/2.94 % (2464967)Instruction limit reached!
% 16.61/2.94 % (2464967)------------------------------
% 16.61/2.94 % (2464967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.61/2.94 % (2464967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.61/2.94 % (2464967)CaDiCaL version: 2.1.3
% 16.61/2.94 % (2464967)Termination reason: Instruction limit
% 16.61/2.94 % (2464967)Termination phase: Saturation
% 16.61/2.94 % (2464967)Time elapsed: 0.114 s
% 16.61/2.94 % (2464967)Peak memory usage: 14 MB
% 16.61/2.94 % (2464967)Instructions burned: 160 (million)
% 16.61/2.94 % TRYING [6]
% 16.61/2.94 % (2464981)ott-21_1_sil=16000:fs=off:random_seed=94700791:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.61/2.94 % TRYING [8]
% 16.61/2.94 % (2464976)Instruction limit reached!
% 42.27/6.42 % (2464976)------------------------------
% 42.27/6.42 % (2464976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.27/6.42 % (2464976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.27/6.42 % (2464976)CaDiCaL version: 2.1.3
% 42.27/6.42 % (2464976)Termination reason: Instruction limit
% 42.27/6.42 % (2464976)Termination phase: Saturation
% 42.27/6.42 % (2464976)Time elapsed: 0.087 s
% 42.27/6.42 % (2464976)Peak memory usage: 13 MB
% 42.27/6.42 % (2464976)Instructions burned: 132 (million)
% 42.27/6.42 % TRYING [7]
% 42.27/6.42 % (2464983)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1088378251:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 42.27/6.42 % (2464981)Instruction limit reached!
% 42.27/6.42 % (2464981)------------------------------
% 42.27/6.42 % (2464981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.27/6.42 % (2464981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.27/6.42 % (2464981)CaDiCaL version: 2.1.3
% 42.27/6.42 % (2464981)Termination reason: Instruction limit
% 42.27/6.42 % (2464981)Termination phase: Saturation
% 42.27/6.42 % (2464981)Time elapsed: 0.098 s
% 42.27/6.42 % (2464981)Peak memory usage: 12 MB
% 42.27/6.42 % (2464981)Instructions burned: 180 (million)
% 42.27/6.42 % (2464985)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=809052802:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 42.27/6.42 % Detected minimum model sizes of [4]
% 42.27/6.42 % Detected maximum model sizes of [max]
% 42.27/6.42 % TRYING [4]
% 42.27/6.42 % TRYING [5]
% 42.27/6.42 % TRYING [6]
% 42.27/6.42 % TRYING [9]
% 42.27/6.42 % TRYING [8]
% 42.27/6.42 % (2464975)Instruction limit reached!
% 42.27/6.42 % (2464975)------------------------------
% 42.27/6.42 % (2464975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.27/6.42 % (2464975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.27/6.42 % (2464975)CaDiCaL version: 2.1.3
% 42.27/6.42 % (2464975)Termination reason: Instruction limit
% 42.27/6.42 % (2464975)Termination phase: Finite model building constraint generation
% 42.27/6.42 % (2464975)Time elapsed: 0.301 s
% 42.27/6.42 % (2464975)Peak memory usage: 27 MB
% 42.27/6.42 % (2464975)Instructions burned: 714 (million)
% 42.27/6.42 % (2464987)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4172028812:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 42.27/6.42 % TRYING [7]
% 42.27/6.42 % (2464977)Instruction limit reached!
% 42.27/6.42 % (2464977)------------------------------
% 42.27/6.42 % (2464977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.27/6.42 % (2464977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.27/6.42 % (2464977)CaDiCaL version: 2.1.3
% 42.27/6.42 % (2464977)Termination reason: Instruction limit
% 42.27/6.42 % (2464977)Termination phase: Saturation
% 42.27/6.42 % (2464977)Time elapsed: 0.357 s
% 42.27/6.42 % (2464977)Peak memory usage: 19 MB
% 42.27/6.42 % (2464977)Instructions burned: 684 (million)
% 42.27/6.42 % (2464989)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2216400649:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 42.27/6.42 % (2464983)Instruction limit reached!
% 42.27/6.42 % (2464983)------------------------------
% 42.27/6.42 % (2464983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.27/6.42 % (2464983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.27/6.42 % (2464983)CaDiCaL version: 2.1.3
% 42.27/6.43 % (2464983)Termination reason: Instruction limit
% 42.27/6.43 % (2464983)Termination phase: Saturation
% 42.27/6.43 % (2464983)Time elapsed: 0.340 s
% 42.27/6.43 % (2464983)Peak memory usage: 14 MB
% 42.27/6.43 % (2464983)Instructions burned: 478 (million)
% 42.27/6.43 % TRYING [14]
% 42.27/6.43 % (2464991)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=1104340053: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.27/6.43 % (2464985)Instruction limit reached!
% 42.27/6.43 % (2464985)------------------------------
% 42.27/6.43 % (2464985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.27/6.43 % (2464985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.27/6.43 % (2464985)CaDiCaL version: 2.1.3
% 42.27/6.43 % (2464985)Termination reason: Instruction limit
% 42.27/6.43 % (2464985)Termination phase: Finite model building SAT solving
% 42.27/6.43 % (2464985)Time elapsed: 0.337 s
% 42.27/6.43 % (2464985)Peak memory usage: 22 MB
% 42.27/6.43 % (2464985)Instructions burned: 866 (million)
% 81.31/11.96 % (2464993)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2512606762:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 81.31/11.96 % TRYING [10]
% 81.31/11.96 % (2464989)Instruction limit reached!
% 81.31/11.96 % (2464989)------------------------------
% 81.31/11.96 % (2464989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2464989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2464989)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2464989)Termination reason: Instruction limit
% 81.31/11.96 % (2464989)Termination phase: Finite model building constraint generation
% 81.31/11.96 % (2464989)Time elapsed: 0.329 s
% 81.31/11.96 % (2464989)Peak memory usage: 76 MB
% 81.31/11.96 % (2464989)Instructions burned: 892 (million)
% 81.31/11.96 % (2464995)fmb+10_1_sil=64000:random_seed=1270533193:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 81.31/11.96 % Detected minimum model sizes of [4]
% 81.31/11.96 % Detected maximum model sizes of [max]
% 81.31/11.96 % TRYING [4]
% 81.31/11.96 % TRYING [5]
% 81.31/11.96 % TRYING [6]
% 81.31/11.96 % (2464991)Instruction limit reached!
% 81.31/11.96 % (2464991)------------------------------
% 81.31/11.96 % (2464991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2464991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2464991)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2464991)Termination reason: Instruction limit
% 81.31/11.96 % (2464991)Termination phase: Saturation
% 81.31/11.96 % (2464991)Time elapsed: 0.399 s
% 81.31/11.96 % (2464991)Peak memory usage: 19 MB
% 81.31/11.96 % (2464991)Instructions burned: 693 (million)
% 81.31/11.96 % (2464997)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=795446008:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 81.31/11.96 % Detected minimum model sizes of [4]
% 81.31/11.96 % Detected maximum model sizes of [max]
% 81.31/11.96 % TRYING [20]
% 81.31/11.96 % TRYING [7]
% 81.31/11.96 % (2464993)Instruction limit reached!
% 81.31/11.96 % (2464993)------------------------------
% 81.31/11.96 % (2464993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2464993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2464993)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2464993)Termination reason: Instruction limit
% 81.31/11.96 % (2464993)Termination phase: Saturation
% 81.31/11.96 % (2464993)Time elapsed: 0.504 s
% 81.31/11.96 % (2464993)Peak memory usage: 16 MB
% 81.31/11.96 % (2464993)Instructions burned: 880 (million)
% 81.31/11.96 % (2464987)Instruction limit reached!
% 81.31/11.96 % (2464987)------------------------------
% 81.31/11.96 % (2464987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2464987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2464987)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2464987)Termination reason: Instruction limit
% 81.31/11.96 % (2464987)Termination phase: Saturation
% 81.31/11.96 % (2464987)Time elapsed: 0.709 s
% 81.31/11.96 % (2464987)Peak memory usage: 26 MB
% 81.31/11.96 % (2464987)Instructions burned: 1180 (million)
% 81.31/11.96 % (2464999)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1774084213:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 81.31/11.96 % (2465000)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1770910897:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 81.31/11.96 % Detected minimum model sizes of [4]
% 81.31/11.96 % Detected maximum model sizes of [max]
% 81.31/11.96 % TRYING [8]
% 81.31/11.96 % TRYING [8]
% 81.31/11.96 % TRYING [9]
% 81.31/11.96 % (2464999)Instruction limit reached!
% 81.31/11.96 % (2464999)------------------------------
% 81.31/11.96 % (2464999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2464999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2464999)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2464999)Termination reason: Instruction limit
% 81.31/11.96 % (2464999)Termination phase: Finite model building constraint generation
% 81.31/11.96 % (2464999)Time elapsed: 0.435 s
% 81.31/11.96 % (2464999)Peak memory usage: 41 MB
% 81.31/11.96 % (2464999)Instructions burned: 921 (million)
% 81.31/11.96 % (2465003)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2857582170:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 81.31/11.96 % TRYING [11]
% 81.31/11.96 % TRYING [9]
% 81.31/11.96 % (2465003)Instruction limit reached!
% 81.31/11.96 % (2465003)------------------------------
% 81.31/11.96 % (2465003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2465003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2465003)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2465003)Termination reason: Instruction limit
% 81.31/11.96 % (2465003)Termination phase: Saturation
% 81.31/11.96 % (2465003)Time elapsed: 0.877 s
% 81.31/11.96 % (2465003)Peak memory usage: 26 MB
% 81.31/11.96 % (2465003)Instructions burned: 1473 (million)
% 81.31/11.96 % (2465005)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4136903743:i=6324_2974 on theBenchmark for (2974ds/6324Mi)
% 81.31/11.96 % Detected minimum model sizes of [4]
% 81.31/11.96 % Detected maximum model sizes of [max]
% 81.31/11.96 % TRYING [77]
% 81.31/11.96 % TRYING [10]
% 81.31/11.96 % (2465000)Instruction limit reached!
% 81.31/11.96 % (2465000)------------------------------
% 81.31/11.96 % (2465000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2465000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2465000)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2465000)Termination reason: Instruction limit
% 81.31/11.96 % (2465000)Termination phase: Saturation
% 81.31/11.96 % (2465000)Time elapsed: 2.742 s
% 81.31/11.96 % (2465000)Peak memory usage: 19 MB
% 81.31/11.96 % (2465000)Instructions burned: 5132 (million)
% 81.31/11.96 % (2465007)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=373575921:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 81.31/11.96 % Detected minimum model sizes of [4]
% 81.31/11.96 % Detected maximum model sizes of [max]
% 81.31/11.96 % TRYING [16]
% 81.31/11.96 % TRYING [11]
% 81.31/11.96 % TRYING [12]
% 81.31/11.96 % (2465005)Instruction limit reached!
% 81.31/11.96 % (2465005)------------------------------
% 81.31/11.96 % (2465005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2465005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2465005)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2465005)Termination reason: Instruction limit
% 81.31/11.96 % (2465005)Termination phase: Finite model building constraint generation
% 81.31/11.96 % (2465005)Time elapsed: 2.116 s
% 81.31/11.96 % (2465005)Peak memory usage: 394 MB
% 81.31/11.96 % (2465005)Instructions burned: 6325 (million)
% 81.31/11.96 % (2465009)ott-2_1_sil=16000:newcnf=on:random_seed=2063247971:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2952 on theBenchmark for (2952ds/869Mi)
% 81.31/11.96 % (2465007)Instruction limit reached!
% 81.31/11.96 % (2465007)------------------------------
% 81.31/11.96 % (2465007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2465007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2465007)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2465007)Termination reason: Instruction limit
% 81.31/11.96 % (2465007)Termination phase: Finite model building constraint generation
% 81.31/11.96 % (2465007)Time elapsed: 0.973 s
% 81.31/11.96 % (2465007)Peak memory usage: 195 MB
% 81.31/11.96 % (2465007)Instructions burned: 2175 (million)
% 81.31/11.96 % (2465011)ott+10_1_sil=32000:tgt=ground:random_seed=2465016941:i=5114:av=off_2950 on theBenchmark for (2950ds/5114Mi)
% 81.31/11.96 % (2465009)Instruction limit reached!
% 81.31/11.96 % (2465009)------------------------------
% 81.31/11.96 % (2465009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2465009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2465009)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2465009)Termination reason: Instruction limit
% 81.31/11.96 % (2465009)Termination phase: Saturation
% 81.31/11.96 % (2465009)Time elapsed: 0.485 s
% 81.31/11.96 % (2465009)Peak memory usage: 16 MB
% 81.31/11.96 % (2465009)Instructions burned: 869 (million)
% 81.31/11.96 % (2465013)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2981684479:i=54282_2947 on theBenchmark for (2947ds/54282Mi)
% 81.31/11.96 % Detected minimum model sizes of [4]
% 81.31/11.96 % Detected maximum model sizes of [max]
% 81.31/11.96 % TRYING [4]
% 81.31/11.96 % TRYING [5]
% 81.31/11.96 % TRYING [6]
% 81.31/11.96 % TRYING [7]
% 81.31/11.96 % TRYING [8]
% 81.31/11.96 % TRYING [9]
% 81.31/11.96 % (2464997)Instruction limit reached!
% 81.31/11.96 % (2464997)------------------------------
% 81.31/11.96 % (2464997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2464997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2464997)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2464997)Termination reason: Instruction limit
% 81.31/11.96 % (2464997)Termination phase: Finite model building constraint generation
% 81.31/11.96 % (2464997)Time elapsed: 4.981 s
% 81.31/11.96 % (2464997)Peak memory usage: 785 MB
% 81.31/11.96 % (2464997)Instructions burned: 9515 (million)
% 81.31/11.96 % TRYING [12]
% 81.31/11.96 % (2465015)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1364137195:i=3512:aac=none_2939 on theBenchmark for (2939ds/3512Mi)
% 81.31/11.96 % TRYING [10]
% 81.31/11.96 % TRYING [11]
% 81.31/11.96 % TRYING [13]
% 81.31/11.96 % (2465011)Instruction limit reached!
% 81.31/11.96 % (2465011)------------------------------
% 81.31/11.96 % (2465011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2465011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2465011)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2465011)Termination reason: Instruction limit
% 81.31/11.96 % (2465011)Termination phase: Saturation
% 81.31/11.96 % (2465011)Time elapsed: 2.998 s
% 81.31/11.96 % (2465011)Peak memory usage: 33 MB
% 81.31/11.96 % (2465011)Instructions burned: 5115 (million)
% 81.31/11.96 % (2465017)dis+21_1_sil=32000:sas=cadical:random_seed=4033017646:i=3773:amm=off_2920 on theBenchmark for (2920ds/3773Mi)
% 81.31/11.96 % (2465015)Instruction limit reached!
% 81.31/11.96 % (2465015)------------------------------
% 81.31/11.96 % (2465015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2465015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2465015)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2465015)Termination reason: Instruction limit
% 81.31/11.96 % (2465015)Termination phase: Saturation
% 81.31/11.96 % (2465015)Time elapsed: 2.017 s
% 81.31/11.96 % (2465015)Peak memory usage: 20 MB
% 81.31/11.96 % (2465015)Instructions burned: 3513 (million)
% 81.31/11.96 % (2465019)ott+11_1_sil=16000:gs=on:random_seed=3754151594:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2918 on theBenchmark for (2918ds/2251Mi)
% 81.31/11.96 % TRYING [12]
% 81.31/11.96 % (2465019)Instruction limit reached!
% 81.31/11.96 % (2465019)------------------------------
% 81.31/11.96 % (2465019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2465019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2465019)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2465019)Termination reason: Instruction limit
% 81.31/11.96 % (2465019)Termination phase: Saturation
% 81.31/11.96 % (2465019)Time elapsed: 0.881 s
% 81.31/11.96 % (2465019)Peak memory usage: 14 MB
% 81.31/11.96 % (2465019)Instructions burned: 2253 (million)
% 81.31/11.96 % (2465021)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3416451132:fmbsr=1.6:i=67534_2909 on theBenchmark for (2909ds/67534Mi)
% 81.31/11.96 % Detected minimum model sizes of [4]
% 81.31/11.96 % Detected maximum model sizes of [max]
% 81.31/11.96 % TRYING [7]
% 81.31/11.96 % TRYING [13]
% 81.31/11.96 % TRYING [8]
% 81.31/11.96 % TRYING [14]
% 81.31/11.96 % (2464995)Instruction limit reached!
% 81.31/11.96 % (2464995)------------------------------
% 81.31/11.96 % (2464995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2464995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2464995)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2464995)Termination reason: Instruction limit
% 81.31/11.96 % (2464995)Termination phase: Finite model building constraint generation
% 81.31/11.96 % (2464995)Time elapsed: 8.832 s
% 81.31/11.96 % (2464995)Peak memory usage: 116 MB
% 81.31/11.96 % (2464995)Instructions burned: 22062 (million)
% 81.31/11.96 % (2465023)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2241808234:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2902 on theBenchmark for (2902ds/4591Mi)
% 81.31/11.96 % TRYING [9]
% 81.31/11.96 % (2465017)Instruction limit reached!
% 81.31/11.96 % (2465017)------------------------------
% 81.31/11.96 % (2465017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.96 % (2465017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.96 % (2465017)CaDiCaL version: 2.1.3
% 81.31/11.96 % (2465017)Termination reason: Instruction limit
% 81.31/11.96 % (2465017)Termination phase: Saturation
% 81.31/11.96 % (2465017)Time elapsed: 2.206 s
% 81.31/11.96 % (2465017)Peak memory usage: 24 MB
% 81.31/11.96 % (2465017)Instructions burned: 3774 (million)
% 81.31/11.96 % (2465025)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3761158813:i=29340_2898 on theBenchmark for (2898ds/29340Mi)
% 81.31/11.96 % TRYING [10]
% 81.31/11.96 % (2465025) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2464956-2465025"...
% 81.31/11.96 % (2465025)...printing done.
% 81.31/11.96 % (2465025)Refutation found. Thanks to Tanya!
% 81.31/11.96 % SZS status Theorem for theBenchmark
% 81.31/11.96 % SZS output start Proof for theBenchmark
% See solution above
% 81.31/11.97 % (2465025)------------------------------
% 81.31/11.97 % (2465025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.31/11.97 % (2465025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/11.97 % (2465025)CaDiCaL version: 2.1.3
% 81.31/11.97 % (2465025)Termination reason: Refutation
% 81.31/11.97 % (2465025)Time elapsed: 1.277 s
% 81.31/11.97 % (2465025)Peak memory usage: 27 MB
% 81.31/11.97 % (2465025)Instructions burned: 2293 (million)
% 81.31/11.97 % (2464956)Success in time 11.538 s
% 81.31/11.97 % Vampire exiting
%------------------------------------------------------------------------------