%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRO014+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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:30:39 PM UTC 2026
% Result : Theorem 22.82s 4.04s
% Output : Refutation 22.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 24
% Syntax : Number of formulae : 204 ( 36 unt; 10 def)
% Number of atoms : 681 ( 15 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 744 ( 267 ~; 386 |; 64 &)
% ( 16 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 11 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-3 aty)
% Number of variables : 260 ( 0 sgn 235 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& subactivity_occurrence(X2,X1)
& leaf_occ(X3,X1)
& arboreal(X2)
& ~ min_precedes(X2,X3,X0) )
=> X3 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
fof(f7,axiom,
! [X0,X1,X2] :
( min_precedes(X1,X2,X0)
=> ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_06) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& leaf_occ(X1,X0) )
=> ~ ? [X3] : min_precedes(X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_09) ).
fof(f14,axiom,
! [X0] :
( legal(X0)
=> arboreal(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_13) ).
fof(f16,axiom,
! [X0,X1] :
( leaf(X0,X1)
<=> ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ~ ? [X3] : min_precedes(X0,X3,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_15) ).
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(f21,axiom,
! [X0,X1] :
( earlier(X0,X1)
=> ~ earlier(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_20) ).
fof(f22,axiom,
! [X0,X1] :
( precedes(X0,X1)
<=> ( earlier(X0,X1)
& legal(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_21) ).
fof(f23,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ~ root(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_22) ).
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(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)
& next_subocc(X2,X3,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& next_subocc(X3,X4,tptp0)
& leaf(X4,tptp0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_32) ).
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/sandbox2/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(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(ennf_transformation,[],[f3]) ).
fof(f60,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| ~ leaf_occ(X3,X1)
| ~ arboreal(X2)
| min_precedes(X2,X3,X0) ),
inference(flattening,[],[f59]) ).
fof(f65,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(f70,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f71,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(flattening,[],[f70]) ).
fof(f76,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f78,plain,
! [X0,X1] :
( leaf(X0,X1)
<=> ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) ) ),
inference(ennf_transformation,[],[f16]) ).
fof(f82,plain,
! [X0,X1] :
( ~ earlier(X1,X0)
| ~ earlier(X0,X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f83,plain,
! [X0,X1,X2] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f85,plain,
! [X0,X1,X2] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f25]) ).
fof(f87,plain,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) ) ),
inference(ennf_transformation,[],[f27]) ).
fof(f88,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(f89,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ min_precedes(X0,X1,X2)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(flattening,[],[f88]) ).
fof(f98,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X3,tptp4)
& next_subocc(X2,X3,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& next_subocc(X3,X4,tptp0)
& leaf(X4,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f33]) ).
fof(f99,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( occurrence_of(X2,tptp3)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X3,tptp4)
& next_subocc(X2,X3,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& next_subocc(X3,X4,tptp0)
& leaf(X4,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(flattening,[],[f98]) ).
fof(f100,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(f101,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,[],[f100]) ).
fof(f105,plain,
! [X2,X3,X0,X1] :
( min_precedes(X2,X3,X0)
| ~ arboreal(X2)
| ~ leaf_occ(X3,X1)
| ~ subactivity_occurrence(X2,X1)
| ~ occurrence_of(X1,X0)
| X2 = X3 ),
inference(cnf_transformation,[],[f60]) ).
fof(f109,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| subactivity_occurrence(X2,sK2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f65]) ).
fof(f110,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| subactivity_occurrence(X1,sK2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f65]) ).
fof(f111,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| occurrence_of(sK2(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f65]) ).
fof(f115,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,X2)
| ~ min_precedes(X1,X3,X2) ),
inference(cnf_transformation,[],[f71]) ).
fof(f120,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(cnf_transformation,[],[f76]) ).
fof(f125,plain,
! [X0,X1] :
( min_precedes(sK7(X0,X1),X0,X1)
| root(X0,X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[],[f78]) ).
fof(f133,plain,
! [X2,X0,X1] :
( ~ leaf(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f135,plain,
! [X0,X1] :
( ~ earlier(X1,X0)
| ~ earlier(X0,X1) ),
inference(cnf_transformation,[],[f82]) ).
fof(f136,plain,
! [X0,X1] :
( legal(X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f137,plain,
! [X0,X1] :
( earlier(X0,X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f83]) ).
fof(f142,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(cnf_transformation,[],[f85]) ).
fof(f148,plain,
! [X2,X0,X1] :
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[],[f87]) ).
fof(f149,plain,
! [X2,X3,X0,X1] :
( ~ subactivity_occurrence(X1,X3)
| ~ occurrence_of(X3,X2)
| ~ min_precedes(X0,X1,X2)
| subactivity_occurrence(X0,X3) ),
inference(cnf_transformation,[],[f89]) ).
fof(f154,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK13(X0),tptp1)
| occurrence_of(sK13(X0),tptp2) ),
inference(cnf_transformation,[],[f99]) ).
fof(f155,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| leaf(sK13(X0),tptp0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f156,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(sK12(X0),sK13(X0),tptp0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f157,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(sK11(X0),sK12(X0),tptp0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f159,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(X0,sK11(X0),tptp0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f160,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK11(X0),tptp3) ),
inference(cnf_transformation,[],[f99]) ).
fof(f172,plain,
! [X2,X3] :
( ~ leaf(X3,tptp0)
| ~ min_precedes(X2,X3,tptp0)
| ~ occurrence_of(X3,tptp1)
| ~ next_subocc(sK14,X2,tptp0)
| ~ occurrence_of(X2,tptp3) ),
inference(cnf_transformation,[],[f101]) ).
fof(f173,plain,
! [X2,X3] :
( ~ leaf(X3,tptp0)
| ~ min_precedes(X2,X3,tptp0)
| ~ occurrence_of(X3,tptp2)
| ~ next_subocc(sK14,X2,tptp0)
| ~ occurrence_of(X2,tptp3) ),
inference(cnf_transformation,[],[f101]) ).
fof(f174,plain,
~ leaf_occ(sK14,sK15),
inference(cnf_transformation,[],[f101]) ).
fof(f175,plain,
arboreal(sK14),
inference(cnf_transformation,[],[f101]) ).
fof(f176,plain,
subactivity_occurrence(sK14,sK15),
inference(cnf_transformation,[],[f101]) ).
fof(f177,plain,
occurrence_of(sK15,tptp0),
inference(cnf_transformation,[],[f101]) ).
fof(f180,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X3,X1)
| arboreal(X2)
| min_precedes(X2,X3,X0)
| ~ subactivity_occurrence(X2,X1)
| ~ occurrence_of(X1,X0)
| X2 = X3 ),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f185,plain,
! [X0] :
( ~ legal(X0)
| ~ arboreal(X0) ),
inference(consistent_polarity_flipping,[],[f120]) ).
fof(f189,plain,
! [X0,X1] :
( min_precedes(sK7(X0,X1),X0,X1)
| root(X0,X1)
| leaf(X0,X1) ),
inference(consistent_polarity_flipping,[],[f125]) ).
fof(f194,plain,
! [X2,X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| leaf(X0,X2)
| ~ occurrence_of(X1,X2)
| leaf_occ(X0,X1) ),
inference(consistent_polarity_flipping,[],[f133]) ).
fof(f197,plain,
! [X0,X1] :
( precedes(X0,X1)
| earlier(X0,X1) ),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f198,plain,
! [X0,X1] :
( precedes(X0,X1)
| legal(X1) ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f199,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| ~ precedes(X0,X1) ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f202,plain,
! [X2,X0,X1] :
( next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f208,plain,
! [X0,X1] :
( ~ occurrence_of(X1,tptp0)
| arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| leaf_occ(X0,X1)
| occurrence_of(sK11(X0),tptp3) ),
inference(consistent_polarity_flipping,[],[f160]) ).
fof(f209,plain,
! [X0,X1] :
( ~ occurrence_of(X1,tptp0)
| arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| leaf_occ(X0,X1)
| ~ next_subocc(X0,sK11(X0),tptp0) ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f211,plain,
! [X0,X1] :
( ~ next_subocc(sK11(X0),sK12(X0),tptp0)
| arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| leaf_occ(X0,X1) ),
inference(consistent_polarity_flipping,[],[f157]) ).
fof(f212,plain,
! [X0,X1] :
( ~ next_subocc(sK12(X0),sK13(X0),tptp0)
| arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| leaf_occ(X0,X1) ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f213,plain,
! [X0,X1] :
( ~ leaf(sK13(X0),tptp0)
| arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| leaf_occ(X0,X1) ),
inference(consistent_polarity_flipping,[],[f155]) ).
fof(f214,plain,
! [X0,X1] :
( ~ occurrence_of(X1,tptp0)
| arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| leaf_occ(X0,X1)
| occurrence_of(sK13(X0),tptp1)
| occurrence_of(sK13(X0),tptp2) ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f220,plain,
~ arboreal(sK14),
inference(consistent_polarity_flipping,[],[f175]) ).
fof(f221,plain,
! [X2,X3] :
( ~ min_precedes(X2,X3,tptp0)
| leaf(X3,tptp0)
| ~ occurrence_of(X3,tptp2)
| next_subocc(sK14,X2,tptp0)
| ~ occurrence_of(X2,tptp3) ),
inference(consistent_polarity_flipping,[],[f173]) ).
fof(f222,plain,
! [X2,X3] :
( ~ min_precedes(X2,X3,tptp0)
| leaf(X3,tptp0)
| ~ occurrence_of(X3,tptp1)
| next_subocc(sK14,X2,tptp0)
| ~ occurrence_of(X2,tptp3) ),
inference(consistent_polarity_flipping,[],[f172]) ).
fof(f265,plain,
! [X0,X1] :
( subactivity_occurrence(X0,sK2(X1,sK7(X0,X1),X0))
| leaf(X0,X1)
| root(X0,X1) ),
inference(resolution,[],[f189,f109]) ).
fof(f267,plain,
! [X0,X1] :
( occurrence_of(sK2(X1,sK7(X0,X1),X0),X1)
| leaf(X0,X1)
| root(X0,X1) ),
inference(resolution,[],[f189,f111]) ).
fof(f298,plain,
! [X0] :
( ~ subactivity_occurrence(X0,sK15)
| arboreal(X0)
| leaf_occ(X0,sK15)
| occurrence_of(sK11(X0),tptp3) ),
inference(resolution,[],[f208,f177]) ).
fof(f306,plain,
! [X0] :
( ~ subactivity_occurrence(X0,sK15)
| arboreal(X0)
| leaf_occ(X0,sK15)
| ~ next_subocc(X0,sK11(X0),tptp0) ),
inference(resolution,[],[f209,f177]) ).
fof(f315,plain,
! [X0,X1] :
( ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| arboreal(X0)
| leaf_occ(X0,X1)
| min_precedes(sK11(X0),sK12(X0),tptp0) ),
inference(resolution,[],[f211,f202]) ).
fof(f321,plain,
! [X0,X1] :
( ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| arboreal(X0)
| leaf_occ(X0,X1)
| min_precedes(sK12(X0),sK13(X0),tptp0) ),
inference(resolution,[],[f212,f202]) ).
fof(f329,plain,
( arboreal(sK14)
| leaf_occ(sK14,sK15)
| occurrence_of(sK11(sK14),tptp3) ),
inference(resolution,[],[f298,f176]) ).
fof(f330,plain,
( leaf_occ(sK14,sK15)
| occurrence_of(sK11(sK14),tptp3) ),
inference(forward_subsumption_resolution,[],[f329,f220]) ).
fof(f331,plain,
occurrence_of(sK11(sK14),tptp3),
inference(forward_subsumption_resolution,[],[f330,f174]) ).
fof(f337,plain,
( arboreal(sK14)
| leaf_occ(sK14,sK15)
| ~ next_subocc(sK14,sK11(sK14),tptp0) ),
inference(resolution,[],[f306,f176]) ).
fof(f338,plain,
( leaf_occ(sK14,sK15)
| ~ next_subocc(sK14,sK11(sK14),tptp0) ),
inference(forward_subsumption_resolution,[],[f337,f220]) ).
fof(f339,plain,
~ next_subocc(sK14,sK11(sK14),tptp0),
inference(forward_subsumption_resolution,[],[f338,f174]) ).
fof(f347,definition,
( spl16_3
<=> occurrence_of(sK13(sK14),tptp2) ),
introduced(definition,[new_symbols(definition,[spl16_3])],[avatar_definition]) ).
fof(f351,definition,
( spl16_4
<=> occurrence_of(sK13(sK14),tptp1) ),
introduced(definition,[new_symbols(definition,[spl16_4])],[avatar_definition]) ).
fof(f361,plain,
min_precedes(sK14,sK11(sK14),tptp0),
inference(resolution,[],[f339,f202]) ).
fof(f439,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK2(X1,sK7(X0,X1),X0),X2)
| root(X0,X1)
| leaf(X0,X1)
| ~ min_precedes(X3,X0,X2)
| subactivity_occurrence(X3,sK2(X1,sK7(X0,X1),X0)) ),
inference(resolution,[],[f265,f149]) ).
fof(f440,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK2(X1,sK7(X0,X1),X0),X2)
| root(X0,X1)
| leaf(X0,X2)
| leaf(X0,X1)
| leaf_occ(X0,sK2(X1,sK7(X0,X1),X0)) ),
inference(resolution,[],[f265,f194]) ).
fof(f472,plain,
! [X0] :
( ~ subactivity_occurrence(X0,sK15)
| arboreal(X0)
| leaf_occ(X0,sK15)
| min_precedes(sK11(X0),sK12(X0),tptp0) ),
inference(resolution,[],[f315,f177]) ).
fof(f475,plain,
! [X0] :
( ~ subactivity_occurrence(X0,sK15)
| arboreal(X0)
| leaf_occ(X0,sK15)
| min_precedes(sK12(X0),sK13(X0),tptp0) ),
inference(resolution,[],[f321,f177]) ).
fof(f546,plain,
( arboreal(sK14)
| leaf_occ(sK14,sK15)
| min_precedes(sK11(sK14),sK12(sK14),tptp0) ),
inference(resolution,[],[f472,f176]) ).
fof(f547,plain,
( leaf_occ(sK14,sK15)
| min_precedes(sK11(sK14),sK12(sK14),tptp0) ),
inference(forward_subsumption_resolution,[],[f546,f220]) ).
fof(f553,plain,
min_precedes(sK11(sK14),sK12(sK14),tptp0),
inference(forward_subsumption_resolution,[],[f547,f174]) ).
fof(f555,plain,
( arboreal(sK14)
| leaf_occ(sK14,sK15)
| min_precedes(sK12(sK14),sK13(sK14),tptp0) ),
inference(resolution,[],[f475,f176]) ).
fof(f556,plain,
( leaf_occ(sK14,sK15)
| min_precedes(sK12(sK14),sK13(sK14),tptp0) ),
inference(forward_subsumption_resolution,[],[f555,f220]) ).
fof(f562,plain,
min_precedes(sK12(sK14),sK13(sK14),tptp0),
inference(forward_subsumption_resolution,[],[f556,f174]) ).
fof(f685,plain,
subactivity_occurrence(sK14,sK2(tptp0,sK14,sK11(sK14))),
inference(resolution,[],[f361,f110]) ).
fof(f686,plain,
occurrence_of(sK2(tptp0,sK14,sK11(sK14)),tptp0),
inference(resolution,[],[f361,f111]) ).
fof(f690,plain,
~ precedes(sK14,sK11(sK14)),
inference(resolution,[],[f361,f199]) ).
fof(f750,plain,
legal(sK11(sK14)),
inference(resolution,[],[f690,f198]) ).
fof(f781,plain,
~ arboreal(sK11(sK14)),
inference(resolution,[],[f750,f185]) ).
fof(f793,plain,
! [X0,X1] :
( root(X0,X1)
| leaf(X0,X1)
| leaf(X0,X1)
| leaf_occ(X0,sK2(X1,sK7(X0,X1),X0))
| leaf(X0,X1)
| root(X0,X1) ),
inference(resolution,[],[f440,f267]) ).
fof(f795,plain,
! [X0,X1] :
( leaf_occ(X0,sK2(X1,sK7(X0,X1),X0))
| leaf(X0,X1)
| root(X0,X1) ),
inference(duplicate_literal_removal,[],[f793]) ).
fof(f798,plain,
! [X2,X0,X1] :
( root(X0,X1)
| leaf(X0,X1)
| ~ min_precedes(X2,X0,X1)
| subactivity_occurrence(X2,sK2(X1,sK7(X0,X1),X0))
| leaf(X0,X1)
| root(X0,X1) ),
inference(resolution,[],[f439,f267]) ).
fof(f800,plain,
! [X2,X0,X1] :
( root(X0,X1)
| leaf(X0,X1)
| ~ min_precedes(X2,X0,X1)
| subactivity_occurrence(X2,sK2(X1,sK7(X0,X1),X0)) ),
inference(duplicate_literal_removal,[],[f798]) ).
fof(f801,plain,
! [X2,X0,X1] :
( ~ min_precedes(X2,X0,X1)
| leaf(X0,X1)
| subactivity_occurrence(X2,sK2(X1,sK7(X0,X1),X0)) ),
inference(forward_subsumption_resolution,[],[f800,f139]) ).
fof(f938,plain,
~ precedes(sK11(sK14),sK12(sK14)),
inference(resolution,[],[f553,f199]) ).
fof(f966,plain,
~ precedes(sK12(sK14),sK13(sK14)),
inference(resolution,[],[f562,f199]) ).
fof(f995,definition,
( spl16_57
<=> leaf(sK13(sK14),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_57])],[avatar_definition]) ).
fof(f996,plain,
( ~ leaf(sK13(sK14),tptp0)
| spl16_57 ),
inference(avatar_component_clause,[],[f995]) ).
fof(f997,plain,
( leaf(sK13(sK14),tptp0)
| ~ spl16_57 ),
inference(avatar_component_clause,[],[f995]) ).
fof(f1108,plain,
earlier(sK11(sK14),sK12(sK14)),
inference(resolution,[],[f938,f197]) ).
fof(f1112,plain,
earlier(sK12(sK14),sK13(sK14)),
inference(resolution,[],[f966,f197]) ).
fof(f1206,plain,
~ earlier(sK13(sK14),sK12(sK14)),
inference(resolution,[],[f1112,f135]) ).
fof(f1240,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK2(X1,sK7(X0,X1),X0),X3)
| root(X0,X1)
| arboreal(X2)
| min_precedes(X2,X0,X3)
| ~ subactivity_occurrence(X2,sK2(X1,sK7(X0,X1),X0))
| leaf(X0,X1)
| X0 = X2 ),
inference(resolution,[],[f795,f180]) ).
fof(f1279,plain,
( leaf(sK13(sK14),tptp0)
| subactivity_occurrence(sK12(sK14),sK2(tptp0,sK7(sK13(sK14),tptp0),sK13(sK14))) ),
inference(resolution,[],[f801,f562]) ).
fof(f1283,definition,
( spl16_74
<=> subactivity_occurrence(sK12(sK14),sK2(tptp0,sK7(sK13(sK14),tptp0),sK13(sK14))) ),
introduced(definition,[new_symbols(definition,[spl16_74])],[avatar_definition]) ).
fof(f1285,plain,
( subactivity_occurrence(sK12(sK14),sK2(tptp0,sK7(sK13(sK14),tptp0),sK13(sK14)))
| ~ spl16_74 ),
inference(avatar_component_clause,[],[f1283]) ).
fof(f1286,plain,
( spl16_74
| spl16_57 ),
inference(avatar_split_clause,[],[f1279,f995,f1283]) ).
fof(f1830,definition,
( spl16_80
<=> leaf_occ(sK14,sK2(tptp0,sK14,sK11(sK14))) ),
introduced(definition,[new_symbols(definition,[spl16_80])],[avatar_definition]) ).
fof(f1831,plain,
( ~ leaf_occ(sK14,sK2(tptp0,sK14,sK11(sK14)))
| spl16_80 ),
inference(avatar_component_clause,[],[f1830]) ).
fof(f1832,plain,
( leaf_occ(sK14,sK2(tptp0,sK14,sK11(sK14)))
| ~ spl16_80 ),
inference(avatar_component_clause,[],[f1830]) ).
fof(f1852,plain,
! [X0] :
( ~ subactivity_occurrence(X0,sK2(tptp0,sK14,sK11(sK14)))
| arboreal(X0)
| leaf_occ(X0,sK2(tptp0,sK14,sK11(sK14)))
| occurrence_of(sK13(X0),tptp1)
| occurrence_of(sK13(X0),tptp2) ),
inference(resolution,[],[f686,f214]) ).
fof(f2167,definition,
( spl16_119
<=> root(sK13(sK14),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_119])],[avatar_definition]) ).
fof(f2168,plain,
( ~ root(sK13(sK14),tptp0)
| spl16_119 ),
inference(avatar_component_clause,[],[f2167]) ).
fof(f2169,plain,
( root(sK13(sK14),tptp0)
| ~ spl16_119 ),
inference(avatar_component_clause,[],[f2167]) ).
fof(f2174,plain,
( ! [X0] :
( arboreal(sK14)
| ~ subactivity_occurrence(sK14,X0)
| ~ occurrence_of(X0,tptp0)
| leaf_occ(sK14,X0) )
| ~ spl16_57 ),
inference(resolution,[],[f997,f213]) ).
fof(f2183,definition,
( spl16_122
<=> ! [X0] : ~ min_precedes(X0,sK13(sK14),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_122])],[avatar_definition]) ).
fof(f2184,plain,
( ! [X0] : ~ min_precedes(X0,sK13(sK14),tptp0)
| ~ spl16_122 ),
inference(avatar_component_clause,[],[f2183]) ).
fof(f2186,plain,
( ! [X0] :
( ~ subactivity_occurrence(sK14,X0)
| ~ occurrence_of(X0,tptp0)
| leaf_occ(sK14,X0) )
| ~ spl16_57 ),
inference(forward_subsumption_resolution,[],[f2174,f220]) ).
fof(f2190,plain,
( $false
| ~ spl16_122 ),
inference(backward_subsumption_resolution,[],[f562,f2184]) ).
fof(f2194,plain,
~ spl16_122,
inference(avatar_contradiction_clause,[],[f2190]) ).
fof(f2778,plain,
( ! [X0,X1] :
( ~ min_precedes(X1,sK12(sK14),X0)
| ~ occurrence_of(sK2(tptp0,sK7(sK13(sK14),tptp0),sK13(sK14)),X0)
| subactivity_occurrence(X1,sK2(tptp0,sK7(sK13(sK14),tptp0),sK13(sK14))) )
| ~ spl16_74 ),
inference(resolution,[],[f1285,f149]) ).
fof(f4894,plain,
! [X2,X0,X1] :
( root(X0,X1)
| arboreal(X2)
| min_precedes(X2,X0,X1)
| ~ subactivity_occurrence(X2,sK2(X1,sK7(X0,X1),X0))
| leaf(X0,X1)
| X0 = X2
| leaf(X0,X1)
| root(X0,X1) ),
inference(resolution,[],[f1240,f267]) ).
fof(f4901,plain,
! [X2,X0,X1] :
( ~ subactivity_occurrence(X2,sK2(X1,sK7(X0,X1),X0))
| arboreal(X2)
| min_precedes(X2,X0,X1)
| root(X0,X1)
| leaf(X0,X1)
| X0 = X2 ),
inference(duplicate_literal_removal,[],[f4894]) ).
fof(f8072,plain,
( ~ occurrence_of(sK15,tptp0)
| leaf_occ(sK14,sK15)
| ~ spl16_57 ),
inference(resolution,[],[f2186,f176]) ).
fof(f8084,plain,
( leaf_occ(sK14,sK15)
| ~ spl16_57 ),
inference(forward_subsumption_resolution,[],[f8072,f177]) ).
fof(f8088,plain,
( $false
| ~ spl16_57 ),
inference(forward_subsumption_resolution,[],[f8084,f174]) ).
fof(f8089,plain,
~ spl16_57,
inference(avatar_contradiction_clause,[],[f8088]) ).
fof(f8313,plain,
( ! [X0] : ~ min_precedes(X0,sK13(sK14),tptp0)
| ~ spl16_119 ),
inference(resolution,[],[f2169,f139]) ).
fof(f8315,plain,
( spl16_122
| ~ spl16_119 ),
inference(avatar_split_clause,[],[f8313,f2167,f2183]) ).
fof(f14565,plain,
( arboreal(sK14)
| leaf_occ(sK14,sK2(tptp0,sK14,sK11(sK14)))
| occurrence_of(sK13(sK14),tptp1)
| occurrence_of(sK13(sK14),tptp2) ),
inference(resolution,[],[f1852,f685]) ).
fof(f14738,plain,
( ~ occurrence_of(sK2(tptp0,sK7(sK13(sK14),tptp0),sK13(sK14)),tptp0)
| subactivity_occurrence(sK11(sK14),sK2(tptp0,sK7(sK13(sK14),tptp0),sK13(sK14)))
| ~ spl16_74 ),
inference(resolution,[],[f2778,f553]) ).
fof(f14749,definition,
( spl16_1026
<=> subactivity_occurrence(sK11(sK14),sK2(tptp0,sK7(sK13(sK14),tptp0),sK13(sK14))) ),
introduced(definition,[new_symbols(definition,[spl16_1026])],[avatar_definition]) ).
fof(f14751,plain,
( subactivity_occurrence(sK11(sK14),sK2(tptp0,sK7(sK13(sK14),tptp0),sK13(sK14)))
| ~ spl16_1026 ),
inference(avatar_component_clause,[],[f14749]) ).
fof(f14753,definition,
( spl16_1027
<=> occurrence_of(sK2(tptp0,sK7(sK13(sK14),tptp0),sK13(sK14)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_1027])],[avatar_definition]) ).
fof(f14755,plain,
( ~ occurrence_of(sK2(tptp0,sK7(sK13(sK14),tptp0),sK13(sK14)),tptp0)
| spl16_1027 ),
inference(avatar_component_clause,[],[f14753]) ).
fof(f14756,plain,
( spl16_1026
| ~ spl16_1027
| ~ spl16_74 ),
inference(avatar_split_clause,[],[f14738,f1283,f14753,f14749]) ).
fof(f47222,definition,
( spl16_2216
<=> sK11(sK14) = sK13(sK14) ),
introduced(definition,[new_symbols(definition,[spl16_2216])],[avatar_definition]) ).
fof(f47223,plain,
( sK11(sK14) != sK13(sK14)
| spl16_2216 ),
inference(avatar_component_clause,[],[f47222]) ).
fof(f47224,plain,
( sK11(sK14) = sK13(sK14)
| ~ spl16_2216 ),
inference(avatar_component_clause,[],[f47222]) ).
fof(f47266,plain,
( earlier(sK13(sK14),sK12(sK14))
| ~ spl16_2216 ),
inference(superposition,[],[f1108,f47224]) ).
fof(f47527,plain,
( $false
| ~ spl16_2216 ),
inference(forward_subsumption_resolution,[],[f47266,f1206]) ).
fof(f47528,plain,
~ spl16_2216,
inference(avatar_contradiction_clause,[],[f47527]) ).
fof(f71936,plain,
( ! [X0,X1] :
( ~ min_precedes(sK14,X1,X0)
| ~ occurrence_of(sK2(tptp0,sK14,sK11(sK14)),X0) )
| ~ spl16_80 ),
inference(resolution,[],[f1832,f115]) ).
fof(f71976,plain,
( ~ occurrence_of(sK2(tptp0,sK14,sK11(sK14)),tptp0)
| ~ spl16_80 ),
inference(resolution,[],[f71936,f361]) ).
fof(f71977,plain,
( $false
| ~ spl16_80 ),
inference(forward_subsumption_resolution,[],[f71976,f686]) ).
fof(f71978,plain,
~ spl16_80,
inference(avatar_contradiction_clause,[],[f71977]) ).
fof(f84763,plain,
( leaf_occ(sK14,sK2(tptp0,sK14,sK11(sK14)))
| occurrence_of(sK13(sK14),tptp1)
| occurrence_of(sK13(sK14),tptp2) ),
inference(forward_subsumption_resolution,[],[f14565,f220]) ).
fof(f84800,plain,
( occurrence_of(sK13(sK14),tptp1)
| occurrence_of(sK13(sK14),tptp2)
| spl16_80 ),
inference(forward_subsumption_resolution,[],[f84763,f1831]) ).
fof(f84817,plain,
( spl16_3
| spl16_4
| spl16_80 ),
inference(avatar_split_clause,[],[f84800,f1830,f351,f347]) ).
fof(f85782,plain,
( arboreal(sK11(sK14))
| min_precedes(sK11(sK14),sK13(sK14),tptp0)
| root(sK13(sK14),tptp0)
| leaf(sK13(sK14),tptp0)
| sK11(sK14) = sK13(sK14)
| ~ spl16_1026 ),
inference(resolution,[],[f14751,f4901]) ).
fof(f85799,plain,
( min_precedes(sK11(sK14),sK13(sK14),tptp0)
| root(sK13(sK14),tptp0)
| leaf(sK13(sK14),tptp0)
| sK11(sK14) = sK13(sK14)
| ~ spl16_1026 ),
inference(forward_subsumption_resolution,[],[f85782,f781]) ).
fof(f85807,plain,
( min_precedes(sK11(sK14),sK13(sK14),tptp0)
| leaf(sK13(sK14),tptp0)
| sK11(sK14) = sK13(sK14)
| spl16_119
| ~ spl16_1026 ),
inference(forward_subsumption_resolution,[],[f85799,f2168]) ).
fof(f85814,plain,
( min_precedes(sK11(sK14),sK13(sK14),tptp0)
| sK11(sK14) = sK13(sK14)
| spl16_57
| spl16_119
| ~ spl16_1026 ),
inference(forward_subsumption_resolution,[],[f85807,f996]) ).
fof(f85820,plain,
( min_precedes(sK11(sK14),sK13(sK14),tptp0)
| spl16_57
| spl16_119
| ~ spl16_1026
| spl16_2216 ),
inference(forward_subsumption_resolution,[],[f85814,f47223]) ).
fof(f86243,plain,
( leaf(sK13(sK14),tptp0)
| ~ occurrence_of(sK13(sK14),tptp1)
| next_subocc(sK14,sK11(sK14),tptp0)
| ~ occurrence_of(sK11(sK14),tptp3)
| spl16_57
| spl16_119
| ~ spl16_1026
| spl16_2216 ),
inference(resolution,[],[f85820,f222]) ).
fof(f86244,plain,
( leaf(sK13(sK14),tptp0)
| ~ occurrence_of(sK13(sK14),tptp2)
| next_subocc(sK14,sK11(sK14),tptp0)
| ~ occurrence_of(sK11(sK14),tptp3)
| spl16_57
| spl16_119
| ~ spl16_1026
| spl16_2216 ),
inference(resolution,[],[f85820,f221]) ).
fof(f86266,plain,
( ~ occurrence_of(sK13(sK14),tptp1)
| next_subocc(sK14,sK11(sK14),tptp0)
| ~ occurrence_of(sK11(sK14),tptp3)
| spl16_57
| spl16_119
| ~ spl16_1026
| spl16_2216 ),
inference(forward_subsumption_resolution,[],[f86243,f996]) ).
fof(f86283,plain,
( ~ occurrence_of(sK13(sK14),tptp1)
| ~ occurrence_of(sK11(sK14),tptp3)
| spl16_57
| spl16_119
| ~ spl16_1026
| spl16_2216 ),
inference(forward_subsumption_resolution,[],[f86266,f339]) ).
fof(f86284,plain,
( ~ occurrence_of(sK13(sK14),tptp2)
| next_subocc(sK14,sK11(sK14),tptp0)
| ~ occurrence_of(sK11(sK14),tptp3)
| spl16_57
| spl16_119
| ~ spl16_1026
| spl16_2216 ),
inference(forward_subsumption_resolution,[],[f86244,f996]) ).
fof(f86286,plain,
( ~ occurrence_of(sK13(sK14),tptp1)
| spl16_57
| spl16_119
| ~ spl16_1026
| spl16_2216 ),
inference(forward_subsumption_resolution,[],[f86283,f331]) ).
fof(f86287,plain,
( ~ occurrence_of(sK13(sK14),tptp2)
| ~ occurrence_of(sK11(sK14),tptp3)
| spl16_57
| spl16_119
| ~ spl16_1026
| spl16_2216 ),
inference(forward_subsumption_resolution,[],[f86284,f339]) ).
fof(f86288,plain,
( ~ spl16_4
| spl16_57
| spl16_119
| ~ spl16_1026
| spl16_2216 ),
inference(avatar_split_clause,[],[f86286,f47222,f14749,f2167,f995,f351]) ).
fof(f86289,plain,
( ~ occurrence_of(sK13(sK14),tptp2)
| spl16_57
| spl16_119
| ~ spl16_1026
| spl16_2216 ),
inference(forward_subsumption_resolution,[],[f86287,f331]) ).
fof(f86290,plain,
( ~ spl16_3
| spl16_57
| spl16_119
| ~ spl16_1026
| spl16_2216 ),
inference(avatar_split_clause,[],[f86289,f47222,f14749,f2167,f995,f347]) ).
fof(f86334,plain,
( leaf(sK13(sK14),tptp0)
| root(sK13(sK14),tptp0)
| spl16_1027 ),
inference(resolution,[],[f14755,f267]) ).
fof(f86335,plain,
( root(sK13(sK14),tptp0)
| spl16_57
| spl16_1027 ),
inference(forward_subsumption_resolution,[],[f86334,f996]) ).
fof(f86336,plain,
( $false
| spl16_57
| spl16_119
| spl16_1027 ),
inference(forward_subsumption_resolution,[],[f86335,f2168]) ).
fof(f86337,plain,
( spl16_57
| spl16_119
| spl16_1027 ),
inference(avatar_contradiction_clause,[],[f86336]) ).
cnf(s55,plain,
( spl16_57
| spl16_74 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s107,plain,
~ spl16_122,
inference(sat_conversion,[],[f2194]) ).
cnf(s411,plain,
~ spl16_57,
inference(sat_conversion,[],[f8089]) ).
cnf(s439,plain,
( ~ spl16_119
| spl16_122 ),
inference(sat_conversion,[],[f8315]) ).
cnf(s1094,plain,
( ~ spl16_74
| spl16_1026
| ~ spl16_1027 ),
inference(sat_conversion,[],[f14756]) ).
cnf(s3913,plain,
~ spl16_2216,
inference(sat_conversion,[],[f47528]) ).
cnf(s5649,plain,
~ spl16_80,
inference(sat_conversion,[],[f71978]) ).
cnf(s6993,plain,
( spl16_3
| spl16_4
| spl16_80 ),
inference(sat_conversion,[],[f84817]) ).
cnf(s7204,plain,
( ~ spl16_4
| spl16_57
| spl16_119
| ~ spl16_1026
| spl16_2216 ),
inference(sat_conversion,[],[f86288]) ).
cnf(s7205,plain,
( ~ spl16_3
| spl16_57
| spl16_119
| ~ spl16_1026
| spl16_2216 ),
inference(sat_conversion,[],[f86290]) ).
cnf(s7213,plain,
( spl16_57
| spl16_119
| spl16_1027 ),
inference(sat_conversion,[],[f86337]) ).
cnf(s7436,plain,
~ spl16_119,
inference(rat,[],[s439,s107]) ).
cnf(s7437,plain,
spl16_1027,
inference(rat,[],[s7213,s411,s7436]) ).
cnf(s7489,plain,
spl16_74,
inference(rat,[],[s55,s411]) ).
cnf(s7497,plain,
spl16_1026,
inference(rat,[],[s1094,s7437,s7489]) ).
cnf(s7499,plain,
~ spl16_3,
inference(rat,[],[s7205,s3913,s7436,s411,s7497]) ).
cnf(s7500,plain,
~ spl16_4,
inference(rat,[],[s7204,s3913,s7436,s411,s7497]) ).
cnf(s7505,plain,
$false,
inference(rat,[],[s6993,s5649,s7500,s7499]) ).
fof(f86338,plain,
$false,
inference(avatar_sat_refutation,[],[s7505]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO014+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.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 22:30:31 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 Running first-order model finding
% 0.10/0.39 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.59/2.67 % (4025997)Will run a generic schedule for satisfiability detection.
% 15.59/2.67 % (4026007)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3289047087:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.59/2.67 % (4026003)% WARNING: option uhcvi not known.
% 15.59/2.67 % (4026002)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=515221563_2999 on theBenchmark for (2999ds/0Mi)
% 15.59/2.67 % (4026004)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3789315070:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.59/2.67 % (4026005)dis+10_1_sil=32000:sp=arity:random_seed=2635089058:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.59/2.67 % (4026006)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2083652376:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.59/2.67 % (4026008)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3978986829:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.59/2.67 % (4026003)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2080928912:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.59/2.67 % Detected minimum model sizes of [4]
% 15.59/2.67 % Detected maximum model sizes of [max]
% 15.59/2.67 % TRYING [4]
% 15.59/2.67 % TRYING [5]
% 15.59/2.67 % TRYING [6]
% 15.59/2.67 % (4026007)Instruction limit reached!
% 15.59/2.67 % (4026007)------------------------------
% 15.59/2.67 % (4026007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.59/2.67 % (4026007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.59/2.67 % (4026007)CaDiCaL version: 2.1.3
% 15.59/2.67 % (4026007)Termination reason: Instruction limit
% 15.59/2.67 % (4026007)Termination phase: Saturation
% 15.59/2.67 % (4026007)Time elapsed: 0.049 s
% 15.59/2.67 % (4026007)Peak memory usage: 14 MB
% 15.59/2.67 % (4026007)Instructions burned: 134 (million)
% 15.59/2.67 % (4026016)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1634886431:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.59/2.67 % Detected minimum model sizes of [4]
% 15.59/2.67 % Detected maximum model sizes of [max]
% 15.59/2.67 % TRYING [4]
% 15.59/2.67 % TRYING [5]
% 15.59/2.67 % (4026005)Instruction limit reached!
% 15.59/2.67 % (4026005)------------------------------
% 15.59/2.67 % (4026005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.59/2.67 % (4026005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.59/2.67 % (4026005)CaDiCaL version: 2.1.3
% 15.59/2.67 % (4026005)Termination reason: Instruction limit
% 15.59/2.67 % (4026005)Termination phase: Saturation
% 15.59/2.67 % (4026005)Time elapsed: 0.071 s
% 15.59/2.67 % (4026005)Peak memory usage: 12 MB
% 15.59/2.67 % (4026005)Instructions burned: 103 (million)
% 15.59/2.67 % TRYING [6]
% 15.59/2.67 % (4026006)Instruction limit reached!
% 15.59/2.67 % (4026006)------------------------------
% 15.59/2.67 % (4026006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.59/2.67 % (4026006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.59/2.67 % (4026006)CaDiCaL version: 2.1.3
% 15.59/2.67 % (4026006)Termination reason: Instruction limit
% 15.59/2.67 % (4026006)Termination phase: Saturation
% 15.59/2.67 % (4026006)Time elapsed: 0.074 s
% 15.59/2.67 % (4026006)Peak memory usage: 12 MB
% 15.59/2.67 % (4026006)Instructions burned: 116 (million)
% 15.59/2.67 % TRYING [7]
% 15.59/2.67 % (4026018)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3700356029:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.59/2.67 % (4026019)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=2282346009:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.59/2.67 % TRYING [7]
% 15.59/2.67 % (4026008)Instruction limit reached!
% 15.59/2.67 % (4026008)------------------------------
% 15.59/2.67 % (4026008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.59/2.67 % (4026008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.59/2.67 % (4026008)CaDiCaL version: 2.1.3
% 15.59/2.67 % (4026008)Termination reason: Instruction limit
% 15.59/2.67 % (4026008)Termination phase: Saturation
% 15.59/2.67 % (4026008)Time elapsed: 0.105 s
% 15.59/2.67 % (4026008)Peak memory usage: 14 MB
% 15.59/2.67 % (4026008)Instructions burned: 160 (million)
% 15.59/2.67 % (4026022)ott-21_1_sil=16000:fs=off:random_seed=3515303922:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.59/2.67 % TRYING [8]
% 15.59/2.67 % (4026018)Instruction limit reached!
% 22.82/4.04 % (4026018)------------------------------
% 22.82/4.04 % (4026018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.82/4.04 % (4026018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.82/4.04 % (4026018)CaDiCaL version: 2.1.3
% 22.82/4.04 % (4026018)Termination reason: Instruction limit
% 22.82/4.04 % (4026018)Termination phase: Saturation
% 22.82/4.04 % (4026018)Time elapsed: 0.089 s
% 22.82/4.04 % (4026018)Peak memory usage: 14 MB
% 22.82/4.04 % (4026018)Instructions burned: 131 (million)
% 22.82/4.04 % (4026024)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1847438636:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 22.82/4.04 % (4026016)Instruction limit reached!
% 22.82/4.04 % (4026016)------------------------------
% 22.82/4.04 % (4026016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.82/4.04 % (4026016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.82/4.04 % (4026016)CaDiCaL version: 2.1.3
% 22.82/4.04 % (4026016)Termination reason: Instruction limit
% 22.82/4.04 % (4026016)Termination phase: Finite model building constraint generation
% 22.82/4.04 % (4026016)Time elapsed: 0.161 s
% 22.82/4.04 % (4026016)Peak memory usage: 28 MB
% 22.82/4.04 % (4026016)Instructions burned: 720 (million)
% 22.82/4.04 % (4026022)Instruction limit reached!
% 22.82/4.04 % (4026022)------------------------------
% 22.82/4.04 % (4026022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.82/4.04 % (4026022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.82/4.04 % (4026022)CaDiCaL version: 2.1.3
% 22.82/4.04 % (4026022)Termination reason: Instruction limit
% 22.82/4.04 % (4026022)Termination phase: Saturation
% 22.82/4.04 % (4026022)Time elapsed: 0.098 s
% 22.82/4.04 % (4026022)Peak memory usage: 13 MB
% 22.82/4.04 % (4026022)Instructions burned: 181 (million)
% 22.82/4.04 % (4026026)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=891047105:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 22.82/4.04 % Detected minimum model sizes of [4]
% 22.82/4.04 % Detected maximum model sizes of [max]
% 22.82/4.04 % TRYING [4]
% 22.82/4.04 % TRYING [5]
% 22.82/4.04 % (4026027)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1332400666:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 22.82/4.04 % TRYING [8]
% 22.82/4.04 % TRYING [6]
% 22.82/4.04 % TRYING [7]
% 22.82/4.04 % (4026026)Instruction limit reached!
% 22.82/4.04 % (4026026)------------------------------
% 22.82/4.04 % (4026026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.82/4.04 % (4026026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.82/4.04 % (4026026)CaDiCaL version: 2.1.3
% 22.82/4.04 % (4026026)Termination reason: Instruction limit
% 22.82/4.04 % (4026026)Termination phase: Finite model building SAT solving
% 22.82/4.04 % (4026026)Time elapsed: 0.175 s
% 22.82/4.04 % (4026026)Peak memory usage: 21 MB
% 22.82/4.04 % (4026026)Instructions burned: 870 (million)
% 22.82/4.04 % (4026030)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=39330248:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 22.82/4.04 % TRYING [14]
% 22.82/4.04 % (4026019)Instruction limit reached!
% 22.82/4.04 % (4026019)------------------------------
% 22.82/4.04 % (4026019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.82/4.04 % (4026019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.82/4.04 % (4026019)CaDiCaL version: 2.1.3
% 22.82/4.04 % (4026019)Termination reason: Instruction limit
% 22.82/4.04 % (4026019)Termination phase: Saturation
% 22.82/4.04 % (4026019)Time elapsed: 0.423 s
% 22.82/4.04 % (4026019)Peak memory usage: 19 MB
% 22.82/4.04 % (4026019)Instructions burned: 684 (million)
% 22.82/4.04 % (4026024)Instruction limit reached!
% 22.82/4.04 % (4026024)------------------------------
% 22.82/4.04 % (4026024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.82/4.04 % (4026024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.82/4.04 % (4026024)CaDiCaL version: 2.1.3
% 22.82/4.04 % (4026024)Termination reason: Instruction limit
% 22.82/4.04 % (4026024)Termination phase: Saturation
% 22.82/4.04 % (4026024)Time elapsed: 0.329 s
% 22.82/4.04 % (4026024)Peak memory usage: 14 MB
% 22.82/4.04 % (4026024)Instructions burned: 478 (million)
% 22.82/4.04 % (4026032)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=2972111875: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)
% 22.82/4.04 % (4026033)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1084628220:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 22.82/4.04 % (4026030)Instruction limit reached!
% 22.82/4.04 % (4026030)------------------------------
% 22.82/4.04 % (4026030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.82/4.04 % (4026030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.82/4.04 % (4026030)CaDiCaL version: 2.1.3
% 22.82/4.04 % (4026030)Termination reason: Instruction limit
% 22.82/4.04 % (4026030)Termination phase: Finite model building constraint generation
% 22.82/4.04 % (4026030)Time elapsed: 0.187 s
% 22.82/4.04 % (4026030)Peak memory usage: 75 MB
% 22.82/4.04 % (4026030)Instructions burned: 890 (million)
% 22.82/4.04 % (4026036)fmb+10_1_sil=64000:random_seed=1649756839:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 22.82/4.04 % Detected minimum model sizes of [4]
% 22.82/4.04 % Detected maximum model sizes of [max]
% 22.82/4.04 % TRYING [4]
% 22.82/4.04 % TRYING [5]
% 22.82/4.04 % TRYING [6]
% 22.82/4.04 % TRYING [9]
% 22.82/4.04 % TRYING [7]
% 22.82/4.04 % TRYING [8]
% 22.82/4.04 % (4026027)Instruction limit reached!
% 22.82/4.04 % (4026027)------------------------------
% 22.82/4.04 % (4026027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.82/4.04 % (4026027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.82/4.04 % (4026027)CaDiCaL version: 2.1.3
% 22.82/4.04 % (4026027)Termination reason: Instruction limit
% 22.82/4.04 % (4026027)Termination phase: Saturation
% 22.82/4.04 % (4026027)Time elapsed: 0.700 s
% 22.82/4.04 % (4026027)Peak memory usage: 24 MB
% 22.82/4.04 % (4026027)Instructions burned: 1180 (million)
% 22.82/4.04 % (4026032)Instruction limit reached!
% 22.82/4.04 % (4026032)------------------------------
% 22.82/4.04 % (4026032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.82/4.04 % (4026032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.82/4.04 % (4026032)CaDiCaL version: 2.1.3
% 22.82/4.04 % (4026032)Termination reason: Instruction limit
% 22.82/4.04 % (4026032)Termination phase: Saturation
% 22.82/4.04 % (4026032)Time elapsed: 0.413 s
% 22.82/4.04 % (4026032)Peak memory usage: 21 MB
% 22.82/4.04 % (4026032)Instructions burned: 694 (million)
% 22.82/4.04 % (4026038)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3988444244:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 22.82/4.04 % (4026039)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3974865274:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 22.82/4.04 % Detected minimum model sizes of [4]
% 22.82/4.04 % Detected maximum model sizes of [max]
% 22.82/4.04 % TRYING [20]
% 22.82/4.04 % Detected minimum model sizes of [4]
% 22.82/4.04 % Detected maximum model sizes of [max]
% 22.82/4.04 % TRYING [8]
% 22.82/4.04 % (4026033)Instruction limit reached!
% 22.82/4.04 % (4026033)------------------------------
% 22.82/4.04 % (4026033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.82/4.04 % (4026033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.82/4.04 % (4026033)CaDiCaL version: 2.1.3
% 22.82/4.04 % (4026033)Termination reason: Instruction limit
% 22.82/4.04 % (4026033)Termination phase: Saturation
% 22.82/4.04 % (4026033)Time elapsed: 0.519 s
% 22.82/4.04 % (4026033)Peak memory usage: 17 MB
% 22.82/4.04 % (4026033)Instructions burned: 881 (million)
% 22.82/4.04 % TRYING [9]
% 22.82/4.04 % (4026042)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4253177521:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 22.82/4.04 % TRYING [9]
% 22.82/4.04 % (4026039)Instruction limit reached!
% 22.82/4.04 % (4026039)------------------------------
% 22.82/4.04 % (4026039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.82/4.04 % (4026039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.82/4.04 % (4026039)CaDiCaL version: 2.1.3
% 22.82/4.04 % (4026039)Termination reason: Instruction limit
% 22.82/4.04 % (4026039)Termination phase: Finite model building constraint generation
% 22.82/4.04 % (4026039)Time elapsed: 0.491 s
% 22.82/4.04 % (4026039)Peak memory usage: 42 MB
% 22.82/4.04 % (4026039)Instructions burned: 921 (million)
% 22.82/4.04 % (4026044)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4069570106:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 22.82/4.04 % TRYING [10]
% 22.82/4.04 % (4026044)Instruction limit reached!
% 22.82/4.04 % (4026044)------------------------------
% 22.82/4.04 % (4026044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.82/4.04 % (4026044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.82/4.04 % (4026044)CaDiCaL version: 2.1.3
% 22.82/4.04 % (4026044)Termination reason: Instruction limit
% 22.82/4.04 % (4026044)Termination phase: Saturation
% 22.82/4.04 % (4026044)Time elapsed: 0.752 s
% 22.82/4.04 % (4026044)Peak memory usage: 28 MB
% 22.82/4.04 % (4026044)Instructions burned: 1472 (million)
% 22.82/4.04 % (4026046)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=555167257:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 22.82/4.04 % Detected minimum model sizes of [4]
% 22.82/4.04 % Detected maximum model sizes of [max]
% 22.82/4.04 % TRYING [77]
% 22.82/4.04 % TRYING [10]
% 22.82/4.04 % (4026003) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4025997-4026003"...
% 22.82/4.04 % (4026003)...printing done.
% 22.82/4.04 % (4026003)Refutation found. Thanks to Tanya!
% 22.82/4.04 % SZS status Theorem for theBenchmark
% 22.82/4.04 % SZS output start Proof for theBenchmark
% See solution above
% 22.82/4.05 % (4026003)------------------------------
% 22.82/4.05 % (4026003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.82/4.05 % (4026003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.82/4.05 % (4026003)CaDiCaL version: 2.1.3
% 22.82/4.05 % (4026003)Termination reason: Refutation
% 22.82/4.05 % (4026003)Time elapsed: 3.527 s
% 22.82/4.05 % (4026003)Peak memory usage: 47 MB
% 22.82/4.05 % (4026003)Instructions burned: 5957 (million)
% 22.82/4.05 % (4025997)Success in time 3.644 s
% 22.82/4.05 % Vampire exiting
%------------------------------------------------------------------------------