%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PRO003+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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:20 PM UTC 2026
% Result : Theorem 13.66s 3.16s
% Output : Refutation 14.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 33
% Syntax : Number of formulae : 233 ( 37 unt; 14 def)
% Number of atoms : 641 ( 47 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 715 ( 307 ~; 314 |; 62 &)
% ( 20 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 28 ( 26 usr; 15 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-3 aty)
% Number of variables : 241 ( 0 sgn 214 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos) ).
fof(f2,axiom,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_01) ).
fof(f3,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_02) ).
fof(f8,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_07) ).
fof(f15,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ~ root(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_14) ).
fof(f22,axiom,
! [X0,X1] :
( leaf(X0,X1)
<=> ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ~ ? [X3] : min_precedes(X0,X3,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_21) ).
fof(f23,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ~ ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_22) ).
fof(f26,axiom,
! [X0,X1,X2] :
( min_precedes(X1,X2,X0)
=> ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_25) ).
fof(f29,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& arboreal(X2)
& arboreal(X3)
& subactivity_occurrence(X2,X1)
& subactivity_occurrence(X3,X1) )
=> ( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_28) ).
fof(f34,axiom,
! [X0,X1] :
( root_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_33) ).
fof(f35,axiom,
! [X0,X1] :
( leaf_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_34) ).
fof(f36,axiom,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( occurrence_of(X1,tptp4)
& root_occ(X1,X0)
& occurrence_of(X2,tptp3)
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_35) ).
fof(f39,axiom,
atomic(tptp4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_38) ).
fof(f40,axiom,
atomic(tptp3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_39) ).
fof(f42,axiom,
atomic(tptp1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_41) ).
fof(f43,axiom,
tptp4 != tptp1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_42) ).
fof(f46,axiom,
tptp1 != tptp3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_45) ).
fof(f49,axiom,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& root_occ(X0,X1) )
=> ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_48) ).
fof(f50,conjecture,
~ ? [X0] : occurrence_of(X0,tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f51,negated_conjecture,
~ ~ ? [X0] : occurrence_of(X0,tptp0),
inference(negated_conjecture,[status(cth)],[f50]) ).
fof(f52,plain,
? [X0] : occurrence_of(X0,tptp0),
inference(flattening,[],[f51]) ).
fof(f53,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) ) ),
inference(unused_predicate_definition_removal,[],[f35]) ).
fof(f54,plain,
! [X0,X1] :
( leaf(X0,X1)
=> ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ~ ? [X3] : min_precedes(X0,X3,X1) ) ),
inference(unused_predicate_definition_removal,[],[f22]) ).
fof(f55,plain,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
=> ( min_precedes(X0,X1,X2)
& ~ ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) ) ),
inference(unused_predicate_definition_removal,[],[f23]) ).
fof(f56,plain,
! [X0,X1] :
( ( activity(X0)
& activity_occurrence(X1) )
| ~ occurrence_of(X1,X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f57,plain,
! [X0] :
( ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) )
| ~ activity_occurrence(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f58,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f3]) ).
fof(f59,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f58]) ).
fof(f66,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f73,plain,
! [X0,X1,X2] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f15]) ).
fof(f83,plain,
! [X0,X1] :
( ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) )
| ~ leaf(X0,X1) ),
inference(ennf_transformation,[],[f54]) ).
fof(f84,plain,
! [X0,X1,X2] :
( ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ),
inference(ennf_transformation,[],[f55]) ).
fof(f86,plain,
! [X0,X1,X2] :
( ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) )
| ~ min_precedes(X1,X2,X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f91,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| ~ subactivity_occurrence(X3,X1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f92,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| ~ subactivity_occurrence(X3,X1) ),
inference(flattening,[],[f91]) ).
fof(f101,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) )
| ~ leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f53]) ).
fof(f102,plain,
! [X0] :
( ? [X1,X2] :
( occurrence_of(X1,tptp4)
& root_occ(X1,X0)
& occurrence_of(X2,tptp3)
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f103,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ root_occ(X0,X1) ),
inference(ennf_transformation,[],[f49]) ).
fof(f104,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ root_occ(X0,X1) ),
inference(flattening,[],[f103]) ).
fof(f105,plain,
! [X0] :
( ( activity(sK0(X0))
& occurrence_of(X0,sK0(X0)) )
| ~ activity_occurrence(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[f57]) ).
fof(f106,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f66]) ).
fof(f112,plain,
! [X0,X1] :
( ( ( root(X0,X1)
| min_precedes(sK5(X0,X1),X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) )
| ~ leaf(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X2,sK5(X0,X1))],[f83]) ).
fof(f116,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK7(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK7(X0,X1,X2))
& subactivity_occurrence(X2,sK7(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X3,sK7(X0,X1,X2))],[f86]) ).
fof(f120,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) )
| ~ root_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f121,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ? [X3] :
( occurrence_of(X1,X3)
& subactivity_occurrence(X0,X1)
& root(X0,X3) )
| ~ root_occ(X0,X1) ) ),
inference(rectify,[],[f120]) ).
fof(f122,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ( occurrence_of(X1,sK11(X0,X1))
& subactivity_occurrence(X0,X1)
& root(X0,sK11(X0,X1)) )
| ~ root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X3,sK11(X0,X1))],[f121]) ).
fof(f123,plain,
! [X0,X1] :
( ( occurrence_of(X1,sK12(X0,X1))
& subactivity_occurrence(X0,X1)
& leaf(X0,sK12(X0,X1)) )
| ~ leaf_occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f101]) ).
fof(f124,plain,
! [X0] :
( ( occurrence_of(sK13(X0),tptp4)
& root_occ(sK13(X0),X0)
& occurrence_of(sK14(X0),tptp3)
& leaf_occ(sK14(X0),X0)
& next_subocc(sK13(X0),sK14(X0),tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14]),skolemize(X1,sK13(X0)),skolemize(X2,sK14(X0))],[f102]) ).
fof(f125,plain,
! [X0,X1] :
( ( occurrence_of(sK15(X0),tptp1)
& next_subocc(X0,sK15(X0),tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ root_occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X2,sK15(X0))],[f104]) ).
fof(f126,plain,
occurrence_of(sK16,tptp0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X0,sK16)],[f52]) ).
fof(f127,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f56]) ).
fof(f129,plain,
! [X0] :
( occurrence_of(X0,sK0(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f131,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f59]) ).
fof(f137,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f106]) ).
fof(f151,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| ~ root(X1,X2) ),
inference(cnf_transformation,[],[f73]) ).
fof(f158,plain,
! [X3,X0,X1] :
( ~ min_precedes(X0,X3,X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f160,plain,
! [X2,X3,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X3,X2) ),
inference(cnf_transformation,[],[f84]) ).
fof(f161,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f84]) ).
fof(f168,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK7(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f170,plain,
! [X2,X0,X1] :
( occurrence_of(sK7(X0,X1,X2),X0)
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f175,plain,
! [X2,X3,X0,X1] :
( ~ subactivity_occurrence(X3,X1)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| min_precedes(X2,X3,X0) ),
inference(cnf_transformation,[],[f92]) ).
fof(f181,plain,
! [X0,X1] :
( root(X0,sK11(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f122]) ).
fof(f182,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f122]) ).
fof(f183,plain,
! [X0,X1] :
( occurrence_of(X1,sK11(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f122]) ).
fof(f185,plain,
! [X0,X1] :
( leaf(X0,sK12(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f123]) ).
fof(f186,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f123]) ).
fof(f187,plain,
! [X0,X1] :
( occurrence_of(X1,sK12(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f123]) ).
fof(f188,plain,
! [X0] :
( next_subocc(sK13(X0),sK14(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f189,plain,
! [X0] :
( leaf_occ(sK14(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f190,plain,
! [X0] :
( occurrence_of(sK14(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f191,plain,
! [X0] :
( root_occ(sK13(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f192,plain,
! [X0] :
( occurrence_of(sK13(X0),tptp4)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f195,plain,
atomic(tptp4),
inference(cnf_transformation,[],[f39]) ).
fof(f196,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f40]) ).
fof(f198,plain,
atomic(tptp1),
inference(cnf_transformation,[],[f42]) ).
fof(f199,plain,
tptp4 != tptp1,
inference(cnf_transformation,[],[f43]) ).
fof(f202,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f46]) ).
fof(f205,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(X0,sK15(X0),tptp0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f206,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK15(X0),tptp1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f207,plain,
occurrence_of(sK16,tptp0),
inference(cnf_transformation,[],[f126]) ).
fof(f211,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp3)
| arboreal(sK14(X0)) ),
inference(resolution,[],[f190,f137]) ).
fof(f213,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK14(X0)) ),
inference(forward_subsumption_resolution,[],[f211,f196]) ).
fof(f214,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp4)
| arboreal(sK13(X0)) ),
inference(resolution,[],[f192,f137]) ).
fof(f216,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK13(X0)) ),
inference(forward_subsumption_resolution,[],[f214,f195]) ).
fof(f217,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| occurrence_of(sK15(sK13(X0)),tptp1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f206,f191]) ).
fof(f218,plain,
! [X0] :
( occurrence_of(sK15(sK13(X0)),tptp1)
| ~ occurrence_of(X0,tptp0) ),
inference(duplicate_literal_removal,[],[f217]) ).
fof(f219,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp1)
| arboreal(sK15(sK13(X0))) ),
inference(resolution,[],[f218,f137]) ).
fof(f220,plain,
! [X0,X1] :
( ~ occurrence_of(sK15(sK13(X0)),X1)
| ~ occurrence_of(X0,tptp0)
| tptp1 = X1 ),
inference(resolution,[],[f218,f131]) ).
fof(f221,plain,
! [X0] :
( arboreal(sK15(sK13(X0)))
| ~ occurrence_of(X0,tptp0) ),
inference(forward_subsumption_resolution,[],[f219,f198]) ).
fof(f231,plain,
! [X0] :
( activity_occurrence(sK15(sK13(X0)))
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f127,f218]) ).
fof(f267,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| next_subocc(sK13(X0),sK15(sK13(X0)),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f205,f191]) ).
fof(f268,plain,
! [X0] :
( next_subocc(sK13(X0),sK15(sK13(X0)),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(duplicate_literal_removal,[],[f267]) ).
fof(f270,plain,
! [X0] :
( min_precedes(sK13(X0),sK15(sK13(X0)),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f161,f268]) ).
fof(f275,plain,
! [X2,X3,X0,X1,X4] :
( ~ subactivity_occurrence(X3,sK7(X2,X0,X1))
| min_precedes(X1,X3,X4)
| X1 = X3
| ~ occurrence_of(sK7(X2,X0,X1),X4)
| ~ arboreal(X3)
| ~ arboreal(X1)
| ~ min_precedes(X0,X1,X2)
| min_precedes(X3,X1,X4) ),
inference(resolution,[],[f168,f175]) ).
fof(f333,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK7(X2,X0,X1),X3)
| ~ min_precedes(X0,X1,X2)
| X2 = X3 ),
inference(resolution,[],[f170,f131]) ).
fof(f335,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| arboreal(sK13(sK7(tptp0,X0,X1))) ),
inference(resolution,[],[f170,f216]) ).
fof(f336,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| arboreal(sK14(sK7(tptp0,X0,X1))) ),
inference(resolution,[],[f170,f213]) ).
fof(f359,plain,
! [X0,X1] :
( ~ min_precedes(sK13(X1),X0,tptp0)
| ~ min_precedes(X0,sK14(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(resolution,[],[f160,f188]) ).
fof(f389,plain,
! [X0,X1] :
( ~ activity_occurrence(X0)
| ~ occurrence_of(X0,X1)
| sK0(X0) = X1 ),
inference(resolution,[],[f129,f131]) ).
fof(f391,plain,
! [X0] :
( ~ activity_occurrence(sK15(sK13(X0)))
| ~ occurrence_of(X0,tptp0)
| tptp1 = sK0(sK15(sK13(X0))) ),
inference(resolution,[],[f129,f220]) ).
fof(f396,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| tptp1 = sK0(sK15(sK13(X0))) ),
inference(forward_subsumption_resolution,[],[f391,f231]) ).
fof(f398,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| sK0(X0) = X1 ),
inference(forward_subsumption_resolution,[],[f389,f127]) ).
fof(f401,plain,
! [X0,X1] :
( ~ root_occ(X1,X0)
| sK0(X0) = sK11(X1,X0) ),
inference(resolution,[],[f398,f183]) ).
fof(f403,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| sK0(sK7(X0,X1,X2)) = X0 ),
inference(resolution,[],[f398,f170]) ).
fof(f404,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| tptp4 = sK0(sK13(X0)) ),
inference(resolution,[],[f398,f192]) ).
fof(f421,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| tptp0 = sK0(sK7(tptp0,sK13(X0),sK15(sK13(X0)))) ),
inference(resolution,[],[f403,f270]) ).
fof(f430,plain,
tptp0 = sK0(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),
inference(resolution,[],[f421,f207]) ).
fof(f437,definition,
( spl17_12
<=> occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl17_12])],[avatar_definition]) ).
fof(f438,plain,
( ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0)
| spl17_12 ),
inference(avatar_component_clause,[],[f437]) ).
fof(f439,plain,
( occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0)
| ~ spl17_12 ),
inference(avatar_component_clause,[],[f437]) ).
fof(f460,plain,
tptp1 = sK0(sK15(sK13(sK16))),
inference(resolution,[],[f396,f207]) ).
fof(f483,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| sK0(X0) = sK11(sK13(X0),X0) ),
inference(resolution,[],[f401,f191]) ).
fof(f539,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X3,sK7(X2,X0,X1))
| sK12(X3,sK7(X2,X0,X1)) = X2
| ~ min_precedes(X0,X1,X2) ),
inference(resolution,[],[f333,f187]) ).
fof(f543,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK7(X0,X1,X2),tptp0)
| ~ min_precedes(X1,X2,X0)
| sK12(sK14(sK7(X0,X1,X2)),sK7(X0,X1,X2)) = X0 ),
inference(resolution,[],[f539,f189]) ).
fof(f544,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| tptp0 = sK12(sK14(sK7(tptp0,X0,X1)),sK7(tptp0,X0,X1))
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f543,f170]) ).
fof(f545,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| tptp0 = sK12(sK14(sK7(tptp0,X0,X1)),sK7(tptp0,X0,X1)) ),
inference(duplicate_literal_removal,[],[f544]) ).
fof(f546,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| tptp0 = sK12(sK14(sK7(tptp0,sK13(X0),sK15(sK13(X0)))),sK7(tptp0,sK13(X0),sK15(sK13(X0)))) ),
inference(resolution,[],[f545,f270]) ).
fof(f563,plain,
tptp0 = sK12(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),
inference(resolution,[],[f546,f207]) ).
fof(f564,plain,
( leaf(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ leaf_occ(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))) ),
inference(superposition,[],[f185,f563]) ).
fof(f567,definition,
( spl17_22
<=> leaf_occ(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))) ),
introduced(definition,[new_symbols(definition,[spl17_22])],[avatar_definition]) ).
fof(f568,plain,
( leaf_occ(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ spl17_22 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f569,plain,
( ~ leaf_occ(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| spl17_22 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f572,definition,
( spl17_23
<=> leaf(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl17_23])],[avatar_definition]) ).
fof(f574,plain,
( leaf(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ spl17_23 ),
inference(avatar_component_clause,[],[f572]) ).
fof(f575,plain,
( ~ spl17_22
| spl17_23 ),
inference(avatar_split_clause,[],[f564,f572,f567]) ).
fof(f576,plain,
( ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0)
| spl17_22 ),
inference(resolution,[],[f569,f189]) ).
fof(f577,plain,
( ~ spl17_12
| spl17_22 ),
inference(avatar_split_clause,[],[f576,f567,f437]) ).
fof(f578,plain,
( ~ min_precedes(sK13(sK16),sK15(sK13(sK16)),tptp0)
| spl17_12 ),
inference(resolution,[],[f438,f170]) ).
fof(f579,plain,
( ~ occurrence_of(sK16,tptp0)
| spl17_12 ),
inference(resolution,[],[f578,f270]) ).
fof(f580,plain,
( $false
| spl17_12 ),
inference(forward_subsumption_resolution,[],[f579,f207]) ).
fof(f581,plain,
spl17_12,
inference(avatar_contradiction_clause,[],[f580]) ).
fof(f585,plain,
( subactivity_occurrence(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ spl17_22 ),
inference(resolution,[],[f568,f186]) ).
fof(f595,plain,
( tptp4 = sK0(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))))
| ~ spl17_12 ),
inference(resolution,[],[f439,f404]) ).
fof(f599,plain,
( sK0(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))) = sK11(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ spl17_12 ),
inference(resolution,[],[f439,f483]) ).
fof(f610,plain,
( tptp0 = sK11(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ spl17_12 ),
inference(forward_demodulation,[],[f599,f430]) ).
fof(f613,plain,
( root(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ root_occ(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ spl17_12 ),
inference(superposition,[],[f181,f610]) ).
fof(f616,definition,
( spl17_24
<=> root_occ(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))) ),
introduced(definition,[new_symbols(definition,[spl17_24])],[avatar_definition]) ).
fof(f617,plain,
( root_occ(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ spl17_24 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f618,plain,
( ~ root_occ(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| spl17_24 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f620,definition,
( spl17_25
<=> root(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl17_25])],[avatar_definition]) ).
fof(f622,plain,
( root(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ spl17_25 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f623,plain,
( ~ spl17_24
| spl17_25
| ~ spl17_12 ),
inference(avatar_split_clause,[],[f613,f437,f620,f616]) ).
fof(f624,plain,
( ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0)
| spl17_24 ),
inference(resolution,[],[f618,f191]) ).
fof(f625,plain,
( $false
| ~ spl17_12
| spl17_24 ),
inference(forward_subsumption_resolution,[],[f624,f439]) ).
fof(f626,plain,
( ~ spl17_12
| spl17_24 ),
inference(avatar_contradiction_clause,[],[f625]) ).
fof(f628,plain,
( subactivity_occurrence(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ spl17_24 ),
inference(resolution,[],[f617,f182]) ).
fof(f803,plain,
( ! [X0] :
( min_precedes(sK15(sK13(sK16)),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),X0)
| sK15(sK13(sK16)) = sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),X0)
| ~ arboreal(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))))
| ~ arboreal(sK15(sK13(sK16)))
| ~ min_precedes(sK13(sK16),sK15(sK13(sK16)),tptp0)
| min_precedes(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK15(sK13(sK16)),X0) )
| ~ spl17_22 ),
inference(resolution,[],[f275,f585]) ).
fof(f807,plain,
( ! [X0] :
( min_precedes(sK15(sK13(sK16)),sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),X0)
| sK15(sK13(sK16)) = sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),X0)
| ~ arboreal(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))))
| ~ arboreal(sK15(sK13(sK16)))
| ~ min_precedes(sK13(sK16),sK15(sK13(sK16)),tptp0)
| min_precedes(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK15(sK13(sK16)),X0) )
| ~ spl17_24 ),
inference(resolution,[],[f275,f628]) ).
fof(f812,plain,
( ! [X0] :
( min_precedes(sK15(sK13(sK16)),sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),X0)
| sK15(sK13(sK16)) = sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),X0)
| ~ arboreal(sK15(sK13(sK16)))
| ~ min_precedes(sK13(sK16),sK15(sK13(sK16)),tptp0)
| min_precedes(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK15(sK13(sK16)),X0) )
| ~ spl17_24 ),
inference(forward_subsumption_resolution,[],[f807,f335]) ).
fof(f814,plain,
( ! [X0] :
( min_precedes(sK15(sK13(sK16)),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),X0)
| sK15(sK13(sK16)) = sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),X0)
| ~ arboreal(sK15(sK13(sK16)))
| ~ min_precedes(sK13(sK16),sK15(sK13(sK16)),tptp0)
| min_precedes(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK15(sK13(sK16)),X0) )
| ~ spl17_22 ),
inference(forward_subsumption_resolution,[],[f803,f336]) ).
fof(f816,definition,
( spl17_36
<=> min_precedes(sK13(sK16),sK15(sK13(sK16)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl17_36])],[avatar_definition]) ).
fof(f818,plain,
( ~ min_precedes(sK13(sK16),sK15(sK13(sK16)),tptp0)
| spl17_36 ),
inference(avatar_component_clause,[],[f816]) ).
fof(f820,definition,
( spl17_37
<=> arboreal(sK15(sK13(sK16))) ),
introduced(definition,[new_symbols(definition,[spl17_37])],[avatar_definition]) ).
fof(f822,plain,
( ~ arboreal(sK15(sK13(sK16)))
| spl17_37 ),
inference(avatar_component_clause,[],[f820]) ).
fof(f824,definition,
( spl17_38
<=> sK15(sK13(sK16)) = sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))) ),
introduced(definition,[new_symbols(definition,[spl17_38])],[avatar_definition]) ).
fof(f826,plain,
( sK15(sK13(sK16)) = sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ spl17_38 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f828,definition,
( spl17_39
<=> ! [X0] :
( min_precedes(sK15(sK13(sK16)),sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),X0)
| min_precedes(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK15(sK13(sK16)),X0)
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl17_39])],[avatar_definition]) ).
fof(f829,plain,
( ! [X0] :
( min_precedes(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK15(sK13(sK16)),X0)
| min_precedes(sK15(sK13(sK16)),sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),X0)
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),X0) )
| ~ spl17_39 ),
inference(avatar_component_clause,[],[f828]) ).
fof(f830,plain,
( ~ spl17_36
| ~ spl17_37
| spl17_38
| spl17_39
| ~ spl17_24 ),
inference(avatar_split_clause,[],[f812,f616,f828,f824,f820,f816]) ).
fof(f832,definition,
( spl17_40
<=> sK15(sK13(sK16)) = sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))) ),
introduced(definition,[new_symbols(definition,[spl17_40])],[avatar_definition]) ).
fof(f834,plain,
( sK15(sK13(sK16)) = sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))))
| ~ spl17_40 ),
inference(avatar_component_clause,[],[f832]) ).
fof(f836,definition,
( spl17_41
<=> ! [X0] :
( min_precedes(sK15(sK13(sK16)),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),X0)
| min_precedes(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK15(sK13(sK16)),X0)
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl17_41])],[avatar_definition]) ).
fof(f837,plain,
( ! [X0] :
( min_precedes(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK15(sK13(sK16)),X0)
| min_precedes(sK15(sK13(sK16)),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),X0)
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),X0) )
| ~ spl17_41 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f838,plain,
( ~ spl17_36
| ~ spl17_37
| spl17_40
| spl17_41
| ~ spl17_22 ),
inference(avatar_split_clause,[],[f814,f567,f836,f832,f820,f816]) ).
fof(f839,plain,
( ~ occurrence_of(sK16,tptp0)
| spl17_36 ),
inference(resolution,[],[f818,f270]) ).
fof(f840,plain,
( $false
| spl17_36 ),
inference(forward_subsumption_resolution,[],[f839,f207]) ).
fof(f841,plain,
spl17_36,
inference(avatar_contradiction_clause,[],[f840]) ).
fof(f850,plain,
( ~ occurrence_of(sK16,tptp0)
| spl17_37 ),
inference(resolution,[],[f822,f221]) ).
fof(f851,plain,
( $false
| spl17_37 ),
inference(forward_subsumption_resolution,[],[f850,f207]) ).
fof(f852,plain,
spl17_37,
inference(avatar_contradiction_clause,[],[f851]) ).
fof(f861,plain,
( occurrence_of(sK15(sK13(sK16)),tptp3)
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0)
| ~ spl17_40 ),
inference(superposition,[],[f190,f834]) ).
fof(f877,plain,
( occurrence_of(sK15(sK13(sK16)),tptp3)
| ~ spl17_12
| ~ spl17_40 ),
inference(forward_subsumption_resolution,[],[f861,f439]) ).
fof(f885,plain,
( ~ occurrence_of(sK16,tptp0)
| tptp3 = tptp1
| ~ spl17_12
| ~ spl17_40 ),
inference(resolution,[],[f877,f220]) ).
fof(f895,plain,
( tptp3 = tptp1
| ~ spl17_12
| ~ spl17_40 ),
inference(forward_subsumption_resolution,[],[f885,f207]) ).
fof(f898,plain,
( $false
| ~ spl17_12
| ~ spl17_40 ),
inference(forward_subsumption_resolution,[],[f895,f202]) ).
fof(f899,plain,
( ~ spl17_12
| ~ spl17_40 ),
inference(avatar_contradiction_clause,[],[f898]) ).
fof(f916,definition,
( spl17_43
<=> min_precedes(sK15(sK13(sK16)),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl17_43])],[avatar_definition]) ).
fof(f917,plain,
( ~ min_precedes(sK15(sK13(sK16)),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| spl17_43 ),
inference(avatar_component_clause,[],[f916]) ).
fof(f918,plain,
( min_precedes(sK15(sK13(sK16)),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ spl17_43 ),
inference(avatar_component_clause,[],[f916]) ).
fof(f949,plain,
( min_precedes(sK15(sK13(sK16)),sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0)
| ~ min_precedes(sK15(sK13(sK16)),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0)
| ~ spl17_39 ),
inference(resolution,[],[f829,f359]) ).
fof(f956,plain,
( min_precedes(sK15(sK13(sK16)),sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0)
| ~ min_precedes(sK15(sK13(sK16)),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ spl17_39 ),
inference(duplicate_literal_removal,[],[f949]) ).
fof(f959,plain,
( min_precedes(sK15(sK13(sK16)),sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ min_precedes(sK15(sK13(sK16)),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ spl17_12
| ~ spl17_39 ),
inference(forward_subsumption_resolution,[],[f956,f439]) ).
fof(f966,definition,
( spl17_49
<=> min_precedes(sK15(sK13(sK16)),sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl17_49])],[avatar_definition]) ).
fof(f968,plain,
( min_precedes(sK15(sK13(sK16)),sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ spl17_49 ),
inference(avatar_component_clause,[],[f966]) ).
fof(f975,plain,
( min_precedes(sK15(sK13(sK16)),sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ spl17_12
| ~ spl17_39
| ~ spl17_43 ),
inference(forward_subsumption_resolution,[],[f959,f918]) ).
fof(f977,plain,
( spl17_49
| ~ spl17_12
| ~ spl17_39
| ~ spl17_43 ),
inference(avatar_split_clause,[],[f975,f916,f828,f437,f966]) ).
fof(f984,plain,
( tptp4 = sK0(sK15(sK13(sK16)))
| ~ spl17_12
| ~ spl17_38 ),
inference(superposition,[],[f595,f826]) ).
fof(f1030,plain,
( tptp4 = tptp1
| ~ spl17_12
| ~ spl17_38 ),
inference(forward_demodulation,[],[f984,f460]) ).
fof(f1031,plain,
( $false
| ~ spl17_12
| ~ spl17_38 ),
inference(forward_subsumption_resolution,[],[f1030,f199]) ).
fof(f1032,plain,
( ~ spl17_12
| ~ spl17_38 ),
inference(avatar_contradiction_clause,[],[f1031]) ).
fof(f1040,plain,
( ~ root(sK13(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ spl17_49 ),
inference(resolution,[],[f968,f151]) ).
fof(f1042,plain,
( $false
| ~ spl17_25
| ~ spl17_49 ),
inference(forward_subsumption_resolution,[],[f1040,f622]) ).
fof(f1043,plain,
( ~ spl17_25
| ~ spl17_49 ),
inference(avatar_contradiction_clause,[],[f1042]) ).
fof(f1239,definition,
( spl17_64
<=> min_precedes(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK15(sK13(sK16)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl17_64])],[avatar_definition]) ).
fof(f1240,plain,
( min_precedes(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK15(sK13(sK16)),tptp0)
| ~ spl17_64 ),
inference(avatar_component_clause,[],[f1239]) ).
fof(f1241,plain,
( ~ min_precedes(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),sK15(sK13(sK16)),tptp0)
| spl17_64 ),
inference(avatar_component_clause,[],[f1239]) ).
fof(f1250,plain,
( min_precedes(sK15(sK13(sK16)),sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0)
| ~ spl17_41
| spl17_64 ),
inference(resolution,[],[f1241,f837]) ).
fof(f1254,plain,
( ~ occurrence_of(sK7(tptp0,sK13(sK16),sK15(sK13(sK16))),tptp0)
| ~ spl17_41
| spl17_43
| spl17_64 ),
inference(forward_subsumption_resolution,[],[f1250,f917]) ).
fof(f1255,plain,
( $false
| ~ spl17_12
| ~ spl17_41
| spl17_43
| spl17_64 ),
inference(forward_subsumption_resolution,[],[f1254,f439]) ).
fof(f1256,plain,
( ~ spl17_12
| ~ spl17_41
| spl17_43
| spl17_64 ),
inference(avatar_contradiction_clause,[],[f1255]) ).
fof(f1300,plain,
( ~ leaf(sK14(sK7(tptp0,sK13(sK16),sK15(sK13(sK16)))),tptp0)
| ~ spl17_64 ),
inference(resolution,[],[f1240,f158]) ).
fof(f1303,plain,
( $false
| ~ spl17_23
| ~ spl17_64 ),
inference(forward_subsumption_resolution,[],[f1300,f574]) ).
fof(f1304,plain,
( ~ spl17_23
| ~ spl17_64 ),
inference(avatar_contradiction_clause,[],[f1303]) ).
cnf(s18,plain,
( ~ spl17_22
| spl17_23 ),
inference(sat_conversion,[],[f575]) ).
cnf(s19,plain,
( ~ spl17_12
| spl17_22 ),
inference(sat_conversion,[],[f577]) ).
cnf(s20,plain,
spl17_12,
inference(sat_conversion,[],[f581]) ).
cnf(s22,plain,
( ~ spl17_12
| ~ spl17_24
| spl17_25 ),
inference(sat_conversion,[],[f623]) ).
cnf(s23,plain,
( ~ spl17_12
| spl17_24 ),
inference(sat_conversion,[],[f626]) ).
cnf(s36,plain,
( ~ spl17_24
| ~ spl17_36
| ~ spl17_37
| spl17_38
| spl17_39 ),
inference(sat_conversion,[],[f830]) ).
cnf(s37,plain,
( ~ spl17_22
| ~ spl17_36
| ~ spl17_37
| spl17_40
| spl17_41 ),
inference(sat_conversion,[],[f838]) ).
cnf(s38,plain,
spl17_36,
inference(sat_conversion,[],[f841]) ).
cnf(s39,plain,
spl17_37,
inference(sat_conversion,[],[f852]) ).
cnf(s43,plain,
( ~ spl17_12
| ~ spl17_40 ),
inference(sat_conversion,[],[f899]) ).
cnf(s51,plain,
( ~ spl17_12
| ~ spl17_39
| ~ spl17_43
| spl17_49 ),
inference(sat_conversion,[],[f977]) ).
cnf(s54,plain,
( ~ spl17_12
| ~ spl17_38 ),
inference(sat_conversion,[],[f1032]) ).
cnf(s57,plain,
( ~ spl17_25
| ~ spl17_49 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s74,plain,
( ~ spl17_12
| ~ spl17_41
| spl17_43
| spl17_64 ),
inference(sat_conversion,[],[f1256]) ).
cnf(s78,plain,
( ~ spl17_23
| ~ spl17_64 ),
inference(sat_conversion,[],[f1304]) ).
cnf(s79,plain,
( ~ spl17_22
| spl17_40
| spl17_41 ),
inference(rat,[],[s37,s39,s38]) ).
cnf(s80,plain,
( ~ spl17_24
| spl17_38
| spl17_39 ),
inference(rat,[],[s36,s39,s38]) ).
cnf(s81,plain,
~ spl17_38,
inference(rat,[],[s54,s20]) ).
cnf(s82,plain,
~ spl17_40,
inference(rat,[],[s43,s20]) ).
cnf(s84,plain,
spl17_24,
inference(rat,[],[s23,s20]) ).
cnf(s87,plain,
spl17_39,
inference(rat,[],[s80,s81,s84]) ).
cnf(s89,plain,
spl17_25,
inference(rat,[],[s22,s20,s84]) ).
cnf(s92,plain,
~ spl17_49,
inference(rat,[],[s57,s89]) ).
cnf(s96,plain,
~ spl17_43,
inference(rat,[],[s51,s87,s20,s92]) ).
cnf(s102,plain,
spl17_22,
inference(rat,[],[s19,s20]) ).
cnf(s103,plain,
spl17_41,
inference(rat,[],[s79,s82,s102]) ).
cnf(s104,plain,
spl17_64,
inference(rat,[],[s74,s96,s20,s103]) ).
cnf(s110,plain,
~ spl17_23,
inference(rat,[],[s78,s104]) ).
cnf(s117,plain,
$false,
inference(rat,[],[s18,s110,s102]) ).
fof(f1305,plain,
$false,
inference(avatar_sat_refutation,[],[s117]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : PRO003+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.21/0.46 % Computer : n011.cluster.edu
% 0.21/0.46 % Model : x86_64 x86_64
% 0.21/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.46 % Memory : 8046.5625MB
% 0.21/0.46 % OS : Linux 6.8.0-71-generic
% 0.21/0.46 % CPULimit : 300
% 0.21/0.46 % WCLimit : 300
% 0.21/0.46 % DateTime : Sun Sep 27 22:16:30 UTC 2026
% 0.21/0.47 % CPUTime :
% 0.21/0.47 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.53 Running first-order theorem proving
% 0.25/0.53 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.66/3.16 % (2815270)Detected formulas, will run a generic FOF schedule.
% 13.66/3.16 % (2815278)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3350913229:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.66/3.16 % (2815278)Refutation not found, incomplete strategy
% 13.66/3.16 % (2815278)------------------------------
% 13.66/3.16 % (2815278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/3.16 % (2815278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/3.16 % (2815278)CaDiCaL version: 2.1.3
% 13.66/3.16 % (2815278)Termination reason: Refutation not found, incomplete strategy
% 13.66/3.16 % (2815278)Time elapsed: 0.001 s
% 13.66/3.16 % (2815278)Peak memory usage: 86 MB
% 13.66/3.16 % (2815275)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4242535610:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.66/3.16 % (2815277)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2419708739:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.66/3.16 % (2815280)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=455823292:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.66/3.16 % (2815276)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2333425339:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.66/3.16 % (2815281)dis-21_1_sil=8000:lcm=predicate:random_seed=1052718125:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 13.66/3.16 % (2815279)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1916295780:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.66/3.16 % (2815279)Refutation not found, incomplete strategy
% 13.66/3.16 % (2815279)------------------------------
% 13.66/3.16 % (2815279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/3.16 % (2815279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/3.16 % (2815279)CaDiCaL version: 2.1.3
% 13.66/3.16 % (2815279)Termination reason: Refutation not found, incomplete strategy
% 13.66/3.16 % (2815279)Time elapsed: 0.001 s
% 13.66/3.16 % (2815279)Peak memory usage: 86 MB
% 13.66/3.16 % (2815281)Instruction limit reached!
% 13.66/3.16 % (2815281)------------------------------
% 13.66/3.16 % (2815281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/3.16 % (2815281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/3.16 % (2815281)CaDiCaL version: 2.1.3
% 13.66/3.16 % (2815281)Termination reason: Instruction limit
% 13.66/3.16 % (2815281)Termination phase: Saturation
% 13.66/3.16 % (2815281)Time elapsed: 0.115 s
% 13.66/3.16 % (2815281)Peak memory usage: 88 MB
% 13.66/3.16 % (2815281)Instructions burned: 130 (million)
% 13.66/3.16 % (2815280)Instruction limit reached!
% 13.66/3.16 % (2815280)------------------------------
% 13.66/3.16 % (2815280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/3.16 % (2815280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/3.16 % (2815280)CaDiCaL version: 2.1.3
% 13.66/3.16 % (2815280)Termination reason: Instruction limit
% 13.66/3.16 % (2815280)Termination phase: Saturation
% 13.66/3.16 % (2815280)Time elapsed: 0.136 s
% 13.66/3.16 % (2815280)Peak memory usage: 89 MB
% 13.66/3.16 % (2815280)Instructions burned: 139 (million)
% 13.66/3.16 % (2815278)------------------------------
% 13.66/3.16 % (2815278)------------------------------
% 13.66/3.16 % (2815291)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3416493281:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 13.66/3.16 % (2815279)------------------------------
% 13.66/3.16 % (2815279)------------------------------
% 13.66/3.16 % (2815289)lrs+10_1_sil=8000:sp=occurrence:random_seed=445818412:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 13.66/3.16 % (2815290)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2798187581:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 13.66/3.16 % (2815290)Refutation not found, incomplete strategy
% 13.66/3.16 % (2815290)------------------------------
% 13.66/3.16 % (2815290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/3.16 % (2815290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/3.16 % (2815290)CaDiCaL version: 2.1.3
% 13.66/3.16 % (2815290)Termination reason: Refutation not found, incomplete strategy
% 13.66/3.16 % (2815290)Time elapsed: 0.002 s
% 13.66/3.16 % (2815290)Peak memory usage: 88 MB
% 13.66/3.16 % (2815291)Instruction limit reached!
% 13.66/3.16 % (2815291)------------------------------
% 13.66/3.16 % (2815291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/3.16 % (2815291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/3.16 % (2815291)CaDiCaL version: 2.1.3
% 13.66/3.16 % (2815291)Termination reason: Instruction limit
% 13.66/3.16 % (2815291)Termination phase: Saturation
% 13.66/3.16 % (2815291)Time elapsed: 0.166 s
% 13.66/3.16 % (2815291)Peak memory usage: 92 MB
% 13.66/3.16 % (2815291)Instructions burned: 326 (million)
% 13.66/3.16 % (2815294)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2484646671:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 13.66/3.16 % (2815289)Instruction limit reached!
% 13.66/3.16 % (2815289)------------------------------
% 13.66/3.16 % (2815289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/3.16 % (2815289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/3.16 % (2815289)CaDiCaL version: 2.1.3
% 13.66/3.16 % (2815289)Termination reason: Instruction limit
% 13.66/3.16 % (2815289)Termination phase: Saturation
% 13.66/3.16 % (2815289)Time elapsed: 0.287 s
% 13.66/3.16 % (2815289)Peak memory usage: 92 MB
% 13.66/3.16 % (2815289)Instructions burned: 286 (million)
% 13.66/3.16 % (2815297)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=826373764:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 13.66/3.16 % (2815290)------------------------------
% 13.66/3.16 % (2815290)------------------------------
% 13.66/3.16 % (2815294)Instruction limit reached!
% 13.66/3.16 % (2815294)------------------------------
% 13.66/3.16 % (2815294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/3.16 % (2815294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/3.16 % (2815294)CaDiCaL version: 2.1.3
% 13.66/3.16 % (2815294)Termination reason: Instruction limit
% 13.66/3.16 % (2815294)Termination phase: Saturation
% 13.66/3.16 % (2815294)Time elapsed: 0.223 s
% 13.66/3.16 % (2815294)Peak memory usage: 89 MB
% 13.66/3.16 % (2815294)Instructions burned: 248 (million)
% 13.66/3.16 % (2815308)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=910956625:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 13.66/3.16 % (2815297)Instruction limit reached!
% 13.66/3.16 % (2815297)------------------------------
% 13.66/3.16 % (2815297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/3.16 % (2815297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/3.16 % (2815297)CaDiCaL version: 2.1.3
% 13.66/3.16 % (2815297)Termination reason: Instruction limit
% 13.66/3.16 % (2815297)Termination phase: Saturation
% 13.66/3.16 % (2815297)Time elapsed: 0.228 s
% 13.66/3.16 % (2815297)Peak memory usage: 88 MB
% 13.66/3.16 % (2815297)Instructions burned: 294 (million)
% 13.66/3.16 % (2815310)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2012429016:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 13.66/3.16 % (2815310)Instruction limit reached!
% 13.66/3.16 % (2815310)------------------------------
% 13.66/3.16 % (2815310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/3.16 % (2815310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/3.16 % (2815310)CaDiCaL version: 2.1.3
% 13.66/3.16 % (2815310)Termination reason: Instruction limit
% 13.66/3.16 % (2815310)Termination phase: Saturation
% 13.66/3.16 % (2815310)Time elapsed: 0.064 s
% 13.66/3.16 % (2815310)Peak memory usage: 90 MB
% 13.66/3.16 % (2815310)Instructions burned: 113 (million)
% 13.66/3.16 % (2815275)First to succeed.
% 13.66/3.16 % (2815275)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2815270"
% 13.66/3.16 % (2815311)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2841038446:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 13.66/3.16 % (2815313)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3862595009:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 13.66/3.16 % (2815313)Refutation not found, incomplete strategy
% 13.66/3.16 % (2815313)------------------------------
% 13.66/3.16 % (2815313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/3.16 % (2815313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/3.16 % (2815313)CaDiCaL version: 2.1.3
% 13.66/3.16 % (2815313)Termination reason: Refutation not found, incomplete strategy
% 13.66/3.16 % (2815313)Time elapsed: 0.001 s
% 13.66/3.16 % (2815313)Peak memory usage: 87 MB
% 13.66/3.16 % (2815311)Instruction limit reached!
% 13.66/3.16 % (2815311)------------------------------
% 13.66/3.16 % (2815311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/3.16 % (2815311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/3.16 % (2815311)CaDiCaL version: 2.1.3
% 13.66/3.16 % (2815311)Termination reason: Instruction limit
% 13.66/3.16 % (2815311)Termination phase: Saturation
% 13.66/3.16 % (2815311)Time elapsed: 0.106 s
% 13.66/3.16 % (2815311)Peak memory usage: 88 MB
% 13.66/3.16 % (2815311)Instructions burned: 127 (million)
% 13.66/3.16 % (2815315)lrs+10_1_sil=8000:sp=occurrence:random_seed=2572041072:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 13.66/3.16 % (2815319)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=162162924:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 13.66/3.16 % (2815319)Refutation not found, incomplete strategy
% 13.66/3.16 % (2815319)------------------------------
% 13.66/3.16 % (2815319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/3.16 % (2815319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/3.16 % (2815319)CaDiCaL version: 2.1.3
% 13.66/3.16 % (2815319)Termination reason: Refutation not found, incomplete strategy
% 13.66/3.16 % (2815319)Time elapsed: 0.006 s
% 13.66/3.16 % (2815319)Peak memory usage: 88 MB
% 13.66/3.16 % (2815319)Instructions burned: 4 (million)
% 13.66/3.16 % (2815275)Refutation found. Thanks to Tanya!
% 13.66/3.16 % SZS status Theorem for theBenchmark
% 13.66/3.16 % SZS output start Proof for theBenchmark
% See solution above
% 14.70/3.53 % (2815275)------------------------------
% 14.70/3.53 % (2815275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.70/3.53 % (2815275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.70/3.53 % (2815275)CaDiCaL version: 2.1.3
% 14.70/3.53 % (2815275)Termination reason: Refutation
% 14.70/3.53 % (2815275)Time elapsed: 1.213 s
% 14.70/3.53 % (2815275)Peak memory usage: 131 MB
% 14.70/3.53 % (2815275)Instructions burned: 1136 (million)
% 14.70/3.53 % (2815275)------------------------------
% 14.70/3.53 % (2815275)------------------------------
% 14.70/3.53 % (2815270)Success in time 1.929 s
% 14.70/3.53 % Vampire exiting
%------------------------------------------------------------------------------