%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PRO006+4 : 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 : n016.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:23 PM UTC 2026
% Result : Theorem 5.83s 1.79s
% Output : Refutation 7.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 43
% Syntax : Number of formulae : 332 ( 51 unt; 22 def)
% Number of atoms : 987 ( 86 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1164 ( 509 ~; 541 |; 72 &)
% ( 27 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 23 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 348 ( 0 sgn 325 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2,X3,X4] :
( ( occurrence_of(X1,X0)
& root_occ(X3,X1)
& leaf_occ(X4,X1)
& subactivity_occurrence(X2,X1)
& min_precedes(X3,X2,X0)
& X2 != X4 )
=> min_precedes(X2,X4,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_01) ).
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/sandbox/benchmark/theBenchmark.p',sos_02) ).
fof(f4,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_03) ).
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/sandbox/benchmark/theBenchmark.p',sos_06) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_08) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& leaf_occ(X1,X0) )
=> ~ ? [X3] : min_precedes(X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_09) ).
fof(f13,axiom,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_12) ).
fof(f17,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_16) ).
fof(f20,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_19) ).
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/sandbox/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/sandbox/benchmark/theBenchmark.p',sos_27) ).
fof(f29,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X2,X3)
& ~ atomic(X3)
& leaf_occ(X0,X2)
& leaf_occ(X1,X2) )
=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_28) ).
fof(f30,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X2,X3)
& root_occ(X0,X2)
& root_occ(X1,X2) )
=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_29) ).
fof(f33,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_32) ).
fof(f35,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_34) ).
fof(f36,axiom,
atomic(tptp4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_35) ).
fof(f37,axiom,
atomic(tptp3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_36) ).
fof(f41,axiom,
tptp4 != tptp3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_40) ).
fof(f43,axiom,
tptp1 != tptp3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_42) ).
fof(f46,axiom,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_45) ).
fof(f47,conjecture,
~ ? [X0] : occurrence_of(X0,tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f48,negated_conjecture,
~ ~ ? [X0] : occurrence_of(X0,tptp0),
inference(negated_conjecture,[status(cth)],[f47]) ).
fof(f49,plain,
? [X0] : occurrence_of(X0,tptp0),
inference(flattening,[],[f48]) ).
fof(f53,plain,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] : occurrence_of(X0,X1) ),
inference(pure_predicate_removal,[],[f13]) ).
fof(f54,plain,
! [X0,X1] :
( occurrence_of(X1,X0)
=> activity_occurrence(X1) ),
inference(pure_predicate_removal,[],[f4]) ).
fof(f58,plain,
! [X0,X1,X2,X3,X4] :
( min_precedes(X2,X4,X0)
| ~ occurrence_of(X1,X0)
| ~ root_occ(X3,X1)
| ~ leaf_occ(X4,X1)
| ~ subactivity_occurrence(X2,X1)
| ~ min_precedes(X3,X2,X0)
| X2 = X4 ),
inference(ennf_transformation,[],[f2]) ).
fof(f59,plain,
! [X0,X1,X2,X3,X4] :
( min_precedes(X2,X4,X0)
| ~ occurrence_of(X1,X0)
| ~ root_occ(X3,X1)
| ~ leaf_occ(X4,X1)
| ~ subactivity_occurrence(X2,X1)
| ~ min_precedes(X3,X2,X0)
| X2 = X4 ),
inference(flattening,[],[f58]) ).
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(ennf_transformation,[],[f3]) ).
fof(f61,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,[],[f60]) ).
fof(f62,plain,
! [X0,X1] :
( activity_occurrence(X1)
| ~ occurrence_of(X1,X0) ),
inference(ennf_transformation,[],[f54]) ).
fof(f66,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(f69,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f9]) ).
fof(f70,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f69]) ).
fof(f71,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f72,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(flattening,[],[f71]) ).
fof(f76,plain,
! [X0] :
( ? [X1] : occurrence_of(X0,X1)
| ~ activity_occurrence(X0) ),
inference(ennf_transformation,[],[f53]) ).
fof(f80,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f17]) ).
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(f90,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| ~ leaf_occ(X1,X2) ),
inference(ennf_transformation,[],[f29]) ).
fof(f91,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| ~ leaf_occ(X1,X2) ),
inference(flattening,[],[f90]) ).
fof(f92,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| ~ root_occ(X1,X2) ),
inference(ennf_transformation,[],[f30]) ).
fof(f93,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| ~ root_occ(X1,X2) ),
inference(flattening,[],[f92]) ).
fof(f98,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,[],[f33]) ).
fof(f99,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f46]) ).
fof(f100,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(flattening,[],[f99]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK2(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK2(X0,X1,X2))
& subactivity_occurrence(X2,sK2(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X3,sK2(X0,X1,X2))],[f66]) ).
fof(f105,plain,
! [X0] :
( occurrence_of(X0,sK4(X0))
| ~ activity_occurrence(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X1,sK4(X0))],[f76]) ).
fof(f111,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f80]) ).
fof(f115,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) )
| ~ root_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f20]) ).
fof(f116,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,[],[f115]) ).
fof(f117,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ( occurrence_of(X1,sK9(X0,X1))
& subactivity_occurrence(X0,X1)
& root(X0,sK9(X0,X1)) )
| ~ root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X3,sK9(X0,X1))],[f116]) ).
fof(f121,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) )
& ( ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f87]) ).
fof(f122,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) )
& ( ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(flattening,[],[f121]) ).
fof(f123,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) )
& ( ( min_precedes(X0,X1,X2)
& ! [X4] :
( ~ min_precedes(X0,X4,X2)
| ~ min_precedes(X4,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(rectify,[],[f122]) ).
fof(f124,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ( min_precedes(X0,sK11(X0,X1,X2),X2)
& min_precedes(sK11(X0,X1,X2),X1,X2) ) )
& ( ( min_precedes(X0,X1,X2)
& ! [X4] :
( ~ min_precedes(X0,X4,X2)
| ~ min_precedes(X4,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X3,sK11(X0,X1,X2))],[f123]) ).
fof(f125,plain,
! [X0] :
( ( occurrence_of(sK12(X0),tptp4)
& root_occ(sK12(X0),X0)
& occurrence_of(sK13(X0),tptp3)
& leaf_occ(sK13(X0),X0)
& next_subocc(sK12(X0),sK13(X0),tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13]),skolemize(X1,sK12(X0)),skolemize(X2,sK13(X0))],[f98]) ).
fof(f126,plain,
! [X0,X1] :
( ( occurrence_of(sK14(X0),tptp1)
& next_subocc(X0,sK14(X0),tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X2,sK14(X0))],[f100]) ).
fof(f127,plain,
occurrence_of(sK15,tptp0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X0,sK15)],[f49]) ).
fof(f130,plain,
! [X2,X3,X0,X1,X4] :
( ~ min_precedes(X3,X2,X0)
| ~ occurrence_of(X1,X0)
| ~ root_occ(X3,X1)
| ~ leaf_occ(X4,X1)
| ~ subactivity_occurrence(X2,X1)
| min_precedes(X2,X4,X0)
| X2 = X4 ),
inference(cnf_transformation,[],[f59]) ).
fof(f131,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X3,X1)
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| X2 = X3
| ~ arboreal(X2)
| min_precedes(X2,X3,X0) ),
inference(cnf_transformation,[],[f61]) ).
fof(f132,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f62]) ).
fof(f135,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f136,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X1,sK2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f137,plain,
! [X2,X0,X1] :
( occurrence_of(sK2(X0,X1,X2),X0)
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f140,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f70]) ).
fof(f141,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(cnf_transformation,[],[f72]) ).
fof(f145,plain,
! [X0] :
( occurrence_of(X0,sK4(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f154,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f160,plain,
! [X0,X1] :
( root(X0,sK9(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f161,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f162,plain,
! [X0,X1] :
( occurrence_of(X1,sK9(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f163,plain,
! [X2,X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2)
| root_occ(X0,X1)
| ~ root(X0,X2) ),
inference(cnf_transformation,[],[f117]) ).
fof(f174,plain,
! [X2,X0,X1,X4] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) ),
inference(cnf_transformation,[],[f124]) ).
fof(f175,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f124]) ).
fof(f178,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| subactivity_occurrence(X0,X3)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(cnf_transformation,[],[f89]) ).
fof(f179,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X1,X2)
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f91]) ).
fof(f180,plain,
! [X2,X3,X0,X1] :
( ~ root_occ(X1,X2)
| ~ occurrence_of(X2,X3)
| ~ root_occ(X0,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f93]) ).
fof(f183,plain,
! [X0] :
( next_subocc(sK12(X0),sK13(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f184,plain,
! [X0] :
( leaf_occ(sK13(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f185,plain,
! [X0] :
( occurrence_of(sK13(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f186,plain,
! [X0] :
( root_occ(sK12(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f187,plain,
! [X0] :
( occurrence_of(sK12(X0),tptp4)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f188,plain,
~ atomic(tptp0),
inference(cnf_transformation,[],[f35]) ).
fof(f189,plain,
atomic(tptp4),
inference(cnf_transformation,[],[f36]) ).
fof(f190,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f37]) ).
fof(f194,plain,
tptp4 != tptp3,
inference(cnf_transformation,[],[f41]) ).
fof(f196,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f43]) ).
fof(f199,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(X0,sK14(X0),tptp0)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f126]) ).
fof(f200,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK14(X0),tptp1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f126]) ).
fof(f201,plain,
occurrence_of(sK15,tptp0),
inference(cnf_transformation,[],[f127]) ).
fof(f202,plain,
! [X0] :
( ~ occurrence_of(sK15,X0)
| tptp0 = X0 ),
inference(resolution,[],[f140,f201]) ).
fof(f205,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp4)
| arboreal(sK12(X0)) ),
inference(resolution,[],[f187,f154]) ).
fof(f206,plain,
! [X0,X1] :
( ~ occurrence_of(sK12(X0),X1)
| ~ occurrence_of(X0,tptp0)
| tptp4 = X1 ),
inference(resolution,[],[f187,f140]) ).
fof(f207,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK12(X0)) ),
inference(forward_subsumption_resolution,[],[f205,f189]) ).
fof(f208,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp3)
| arboreal(sK13(X0)) ),
inference(resolution,[],[f185,f154]) ).
fof(f209,plain,
! [X0,X1] :
( ~ occurrence_of(sK13(X0),X1)
| ~ occurrence_of(X0,tptp0)
| tptp3 = X1 ),
inference(resolution,[],[f185,f140]) ).
fof(f210,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK13(X0)) ),
inference(forward_subsumption_resolution,[],[f208,f190]) ).
fof(f211,plain,
activity_occurrence(sK15),
inference(resolution,[],[f132,f201]) ).
fof(f212,plain,
! [X0] :
( activity_occurrence(sK12(X0))
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f132,f187]) ).
fof(f213,plain,
! [X0] :
( activity_occurrence(sK13(X0))
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f132,f185]) ).
fof(f214,plain,
! [X2,X0,X1] :
( min_precedes(X2,sK13(X0),X1)
| ~ subactivity_occurrence(X2,X0)
| sK13(X0) = X2
| ~ arboreal(X2)
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f131,f184]) ).
fof(f217,plain,
arboreal(sK12(sK15)),
inference(resolution,[],[f207,f201]) ).
fof(f226,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK2(X2,X0,X1),tptp0)
| ~ min_precedes(X0,X1,X2)
| next_subocc(X1,sK14(X1),tptp0)
| ~ arboreal(X1)
| leaf_occ(X1,sK2(X2,X0,X1)) ),
inference(resolution,[],[f135,f199]) ).
fof(f229,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK2(X2,X0,X1),tptp0)
| ~ min_precedes(X0,X1,X2)
| next_subocc(X0,sK14(X0),tptp0)
| ~ arboreal(X0)
| leaf_occ(X0,sK2(X2,X0,X1)) ),
inference(resolution,[],[f136,f199]) ).
fof(f230,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK2(X2,X0,X1),tptp0)
| ~ min_precedes(X0,X1,X2)
| occurrence_of(sK14(X0),tptp1)
| ~ arboreal(X0)
| leaf_occ(X0,sK2(X2,X0,X1)) ),
inference(resolution,[],[f136,f200]) ).
fof(f244,plain,
! [X0] :
( min_precedes(sK12(X0),sK13(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f175,f183]) ).
fof(f248,plain,
! [X0,X1] :
( ~ leaf_occ(sK12(X0),X1)
| ~ occurrence_of(X1,tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f244,f141]) ).
fof(f249,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| ~ min_precedes(X0,X1,tptp0)
| occurrence_of(sK14(X0),tptp1)
| ~ arboreal(X0)
| leaf_occ(X0,sK2(tptp0,X0,X1)) ),
inference(resolution,[],[f137,f230]) ).
fof(f258,plain,
! [X0,X1] :
( leaf_occ(X0,sK2(tptp0,X0,X1))
| occurrence_of(sK14(X0),tptp1)
| ~ arboreal(X0)
| ~ min_precedes(X0,X1,tptp0) ),
inference(duplicate_literal_removal,[],[f249]) ).
fof(f266,plain,
! [X0,X1] :
( occurrence_of(sK14(sK12(X0)),tptp1)
| ~ arboreal(sK12(X0))
| ~ min_precedes(sK12(X0),X1,tptp0)
| ~ occurrence_of(sK2(tptp0,sK12(X0),X1),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f258,f248]) ).
fof(f267,plain,
! [X0,X1] :
( occurrence_of(sK14(sK12(X0)),tptp1)
| ~ arboreal(sK12(X0))
| ~ min_precedes(sK12(X0),X1,tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(forward_subsumption_resolution,[],[f266,f137]) ).
fof(f268,plain,
! [X0,X1] :
( ~ min_precedes(sK12(X0),X1,tptp0)
| occurrence_of(sK14(sK12(X0)),tptp1)
| ~ occurrence_of(X0,tptp0) ),
inference(forward_subsumption_resolution,[],[f267,f207]) ).
fof(f269,plain,
! [X0] :
( occurrence_of(sK14(sK12(X0)),tptp1)
| ~ occurrence_of(X0,tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f268,f244]) ).
fof(f272,plain,
! [X0] :
( occurrence_of(sK14(sK12(X0)),tptp1)
| ~ occurrence_of(X0,tptp0) ),
inference(duplicate_literal_removal,[],[f269]) ).
fof(f277,plain,
! [X0,X1] :
( ~ occurrence_of(sK14(sK12(X0)),X1)
| ~ occurrence_of(X0,tptp0)
| tptp1 = X1 ),
inference(resolution,[],[f272,f140]) ).
fof(f282,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| next_subocc(X1,sK14(X1),tptp0)
| ~ arboreal(X1)
| leaf_occ(X1,sK2(tptp0,X0,X1))
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f226,f137]) ).
fof(f283,plain,
! [X0,X1] :
( leaf_occ(X1,sK2(tptp0,X0,X1))
| next_subocc(X1,sK14(X1),tptp0)
| ~ arboreal(X1)
| ~ min_precedes(X0,X1,tptp0) ),
inference(duplicate_literal_removal,[],[f282]) ).
fof(f289,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| next_subocc(X0,sK14(X0),tptp0)
| ~ arboreal(X0)
| leaf_occ(X0,sK2(tptp0,X0,X1))
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f229,f137]) ).
fof(f290,plain,
! [X0,X1] :
( leaf_occ(X0,sK2(tptp0,X0,X1))
| next_subocc(X0,sK14(X0),tptp0)
| ~ arboreal(X0)
| ~ min_precedes(X0,X1,tptp0) ),
inference(duplicate_literal_removal,[],[f289]) ).
fof(f313,plain,
! [X2,X0,X1] :
( ~ leaf_occ(X2,X0)
| atomic(X1)
| ~ occurrence_of(X0,X1)
| sK13(X0) = X2
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f179,f184]) ).
fof(f319,plain,
! [X2,X0,X1] :
( atomic(X0)
| ~ occurrence_of(sK2(tptp0,X1,X2),X0)
| sK13(sK2(tptp0,X1,X2)) = X2
| ~ occurrence_of(sK2(tptp0,X1,X2),tptp0)
| next_subocc(X2,sK14(X2),tptp0)
| ~ arboreal(X2)
| ~ min_precedes(X1,X2,tptp0) ),
inference(resolution,[],[f313,f283]) ).
fof(f327,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK2(tptp0,X1,X2),X0)
| atomic(X0)
| sK13(sK2(tptp0,X1,X2)) = X2
| next_subocc(X2,sK14(X2),tptp0)
| ~ arboreal(X2)
| ~ min_precedes(X1,X2,tptp0) ),
inference(forward_subsumption_resolution,[],[f319,f137]) ).
fof(f336,plain,
! [X0,X1] :
( atomic(tptp0)
| sK13(sK2(tptp0,X0,X1)) = X1
| next_subocc(X1,sK14(X1),tptp0)
| ~ arboreal(X1)
| ~ min_precedes(X0,X1,tptp0)
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f327,f137]) ).
fof(f338,plain,
! [X0,X1] :
( atomic(tptp0)
| sK13(sK2(tptp0,X0,X1)) = X1
| next_subocc(X1,sK14(X1),tptp0)
| ~ arboreal(X1)
| ~ min_precedes(X0,X1,tptp0) ),
inference(duplicate_literal_removal,[],[f336]) ).
fof(f339,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| next_subocc(X1,sK14(X1),tptp0)
| ~ arboreal(X1)
| sK13(sK2(tptp0,X0,X1)) = X1 ),
inference(forward_subsumption_resolution,[],[f338,f188]) ).
fof(f341,plain,
! [X0] :
( next_subocc(sK13(X0),sK14(sK13(X0)),tptp0)
| ~ arboreal(sK13(X0))
| sK13(X0) = sK13(sK2(tptp0,sK12(X0),sK13(X0)))
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f339,f244]) ).
fof(f345,plain,
! [X0] :
( next_subocc(sK13(X0),sK14(sK13(X0)),tptp0)
| sK13(X0) = sK13(sK2(tptp0,sK12(X0),sK13(X0)))
| ~ occurrence_of(X0,tptp0) ),
inference(forward_subsumption_resolution,[],[f341,f210]) ).
fof(f383,plain,
! [X0] :
( min_precedes(sK13(X0),sK14(sK13(X0)),tptp0)
| ~ occurrence_of(X0,tptp0)
| sK13(X0) = sK13(sK2(tptp0,sK12(X0),sK13(X0))) ),
inference(resolution,[],[f345,f175]) ).
fof(f391,plain,
! [X0,X1] :
( ~ leaf_occ(sK13(X0),X1)
| sK13(X0) = sK13(sK2(tptp0,sK12(X0),sK13(X0)))
| ~ occurrence_of(X1,tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f383,f141]) ).
fof(f414,plain,
! [X0,X1] :
( ~ activity_occurrence(X0)
| ~ occurrence_of(X0,X1)
| sK4(X0) = X1 ),
inference(resolution,[],[f145,f140]) ).
fof(f419,plain,
! [X0] :
( ~ activity_occurrence(sK12(X0))
| ~ occurrence_of(X0,tptp0)
| tptp4 = sK4(sK12(X0)) ),
inference(resolution,[],[f145,f206]) ).
fof(f420,plain,
! [X0] :
( ~ activity_occurrence(sK13(X0))
| ~ occurrence_of(X0,tptp0)
| tptp3 = sK4(sK13(X0)) ),
inference(resolution,[],[f145,f209]) ).
fof(f423,plain,
( ~ activity_occurrence(sK15)
| tptp0 = sK4(sK15) ),
inference(resolution,[],[f145,f202]) ).
fof(f424,plain,
tptp0 = sK4(sK15),
inference(forward_subsumption_resolution,[],[f423,f211]) ).
fof(f427,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| tptp3 = sK4(sK13(X0)) ),
inference(forward_subsumption_resolution,[],[f420,f213]) ).
fof(f428,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| tptp4 = sK4(sK12(X0)) ),
inference(forward_subsumption_resolution,[],[f419,f212]) ).
fof(f429,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| sK4(X0) = X1 ),
inference(forward_subsumption_resolution,[],[f414,f132]) ).
fof(f465,definition,
( spl16_4
<=> occurrence_of(sK2(tptp0,sK12(sK15),sK13(sK15)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_4])],[avatar_definition]) ).
fof(f466,plain,
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK13(sK15)),tptp0)
| spl16_4 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f467,plain,
( occurrence_of(sK2(tptp0,sK12(sK15),sK13(sK15)),tptp0)
| ~ spl16_4 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f480,definition,
( spl16_5
<=> leaf_occ(sK13(sK15),sK15) ),
introduced(definition,[new_symbols(definition,[spl16_5])],[avatar_definition]) ).
fof(f481,plain,
( leaf_occ(sK13(sK15),sK15)
| ~ spl16_5 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f482,plain,
( ~ leaf_occ(sK13(sK15),sK15)
| spl16_5 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f488,plain,
( ~ occurrence_of(sK15,tptp0)
| spl16_5 ),
inference(resolution,[],[f482,f184]) ).
fof(f489,plain,
( $false
| spl16_5 ),
inference(forward_subsumption_resolution,[],[f488,f201]) ).
fof(f490,plain,
spl16_5,
inference(avatar_contradiction_clause,[],[f489]) ).
fof(f540,plain,
tptp3 = sK4(sK13(sK15)),
inference(resolution,[],[f427,f201]) ).
fof(f554,plain,
tptp4 = sK4(sK12(sK15)),
inference(resolution,[],[f428,f201]) ).
fof(f565,plain,
! [X2,X0,X1] :
( ~ root_occ(X2,X0)
| ~ occurrence_of(X0,X1)
| sK12(X0) = X2
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f180,f186]) ).
fof(f625,definition,
( spl16_16
<=> leaf_occ(sK13(sK2(tptp0,sK12(sK15),sK13(sK15))),sK2(tptp0,sK12(sK15),sK13(sK15))) ),
introduced(definition,[new_symbols(definition,[spl16_16])],[avatar_definition]) ).
fof(f626,plain,
( leaf_occ(sK13(sK2(tptp0,sK12(sK15),sK13(sK15))),sK2(tptp0,sK12(sK15),sK13(sK15)))
| ~ spl16_16 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f627,plain,
( ~ leaf_occ(sK13(sK2(tptp0,sK12(sK15),sK13(sK15))),sK2(tptp0,sK12(sK15),sK13(sK15)))
| spl16_16 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f634,plain,
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK13(sK15)),tptp0)
| spl16_16 ),
inference(resolution,[],[f627,f184]) ).
fof(f635,plain,
( ~ spl16_4
| spl16_16 ),
inference(avatar_split_clause,[],[f634,f625,f465]) ).
fof(f636,plain,
( ~ min_precedes(sK12(sK15),sK13(sK15),tptp0)
| spl16_4 ),
inference(resolution,[],[f466,f137]) ).
fof(f637,plain,
( ~ occurrence_of(sK15,tptp0)
| spl16_4 ),
inference(resolution,[],[f636,f244]) ).
fof(f641,plain,
( $false
| spl16_4 ),
inference(forward_subsumption_resolution,[],[f637,f201]) ).
fof(f642,plain,
spl16_4,
inference(avatar_contradiction_clause,[],[f641]) ).
fof(f653,definition,
( spl16_19
<=> ! [X0] :
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK13(sK15)),X0)
| atomic(X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_19])],[avatar_definition]) ).
fof(f654,plain,
( ! [X0] :
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK13(sK15)),X0)
| atomic(X0) )
| ~ spl16_19 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f733,plain,
( sK13(sK15) = sK13(sK2(tptp0,sK12(sK15),sK13(sK15)))
| ~ occurrence_of(sK15,tptp0)
| ~ occurrence_of(sK15,tptp0)
| ~ spl16_5 ),
inference(resolution,[],[f391,f481]) ).
fof(f740,plain,
( sK13(sK15) = sK13(sK2(tptp0,sK12(sK15),sK13(sK15)))
| ~ occurrence_of(sK15,tptp0)
| ~ spl16_5 ),
inference(duplicate_literal_removal,[],[f733]) ).
fof(f743,plain,
( sK13(sK15) = sK13(sK2(tptp0,sK12(sK15),sK13(sK15)))
| ~ spl16_5 ),
inference(forward_subsumption_resolution,[],[f740,f201]) ).
fof(f746,plain,
( leaf_occ(sK13(sK15),sK2(tptp0,sK12(sK15),sK13(sK15)))
| ~ spl16_5
| ~ spl16_16 ),
inference(superposition,[],[f626,f743]) ).
fof(f1184,plain,
( ! [X0,X1] :
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK13(sK15)),X0)
| atomic(X0)
| ~ leaf_occ(X1,sK2(tptp0,sK12(sK15),sK13(sK15)))
| sK13(sK15) = X1 )
| ~ spl16_5
| ~ spl16_16 ),
inference(resolution,[],[f746,f179]) ).
fof(f1188,definition,
( spl16_65
<=> ! [X1] :
( ~ leaf_occ(X1,sK2(tptp0,sK12(sK15),sK13(sK15)))
| sK13(sK15) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl16_65])],[avatar_definition]) ).
fof(f1189,plain,
( ! [X1] :
( ~ leaf_occ(X1,sK2(tptp0,sK12(sK15),sK13(sK15)))
| sK13(sK15) = X1 )
| ~ spl16_65 ),
inference(avatar_component_clause,[],[f1188]) ).
fof(f1190,plain,
( spl16_65
| spl16_19
| ~ spl16_5
| ~ spl16_16 ),
inference(avatar_split_clause,[],[f1184,f625,f480,f653,f1188]) ).
fof(f1332,plain,
( atomic(tptp0)
| ~ spl16_4
| ~ spl16_19 ),
inference(resolution,[],[f654,f467]) ).
fof(f1336,plain,
( $false
| ~ spl16_4
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f1332,f188]) ).
fof(f1337,plain,
( ~ spl16_4
| ~ spl16_19 ),
inference(avatar_contradiction_clause,[],[f1336]) ).
fof(f1346,plain,
! [X0] :
( subactivity_occurrence(sK12(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f161,f186]) ).
fof(f1517,definition,
( spl16_81
<=> occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_81])],[avatar_definition]) ).
fof(f1518,plain,
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| spl16_81 ),
inference(avatar_component_clause,[],[f1517]) ).
fof(f1519,plain,
( occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| ~ spl16_81 ),
inference(avatar_component_clause,[],[f1517]) ).
fof(f1537,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| sK9(X0,X1) = sK4(X1) ),
inference(resolution,[],[f162,f429]) ).
fof(f1554,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| sK4(X0) = sK9(sK12(X0),X0) ),
inference(resolution,[],[f1537,f186]) ).
fof(f1557,plain,
sK4(sK15) = sK9(sK12(sK15),sK15),
inference(resolution,[],[f1554,f201]) ).
fof(f1558,plain,
tptp0 = sK9(sK12(sK15),sK15),
inference(forward_demodulation,[],[f1557,f424]) ).
fof(f1561,plain,
( root(sK12(sK15),tptp0)
| ~ root_occ(sK12(sK15),sK15) ),
inference(superposition,[],[f160,f1558]) ).
fof(f1563,definition,
( spl16_82
<=> root_occ(sK12(sK15),sK15) ),
introduced(definition,[new_symbols(definition,[spl16_82])],[avatar_definition]) ).
fof(f1565,plain,
( ~ root_occ(sK12(sK15),sK15)
| spl16_82 ),
inference(avatar_component_clause,[],[f1563]) ).
fof(f1567,definition,
( spl16_83
<=> root(sK12(sK15),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_83])],[avatar_definition]) ).
fof(f1569,plain,
( root(sK12(sK15),tptp0)
| ~ spl16_83 ),
inference(avatar_component_clause,[],[f1567]) ).
fof(f1570,plain,
( ~ spl16_82
| spl16_83 ),
inference(avatar_split_clause,[],[f1561,f1567,f1563]) ).
fof(f1571,plain,
( ~ occurrence_of(sK15,tptp0)
| spl16_82 ),
inference(resolution,[],[f1565,f186]) ).
fof(f1572,plain,
( $false
| spl16_82 ),
inference(forward_subsumption_resolution,[],[f1571,f201]) ).
fof(f1573,plain,
spl16_82,
inference(avatar_contradiction_clause,[],[f1572]) ).
fof(f1765,plain,
( sK12(sK15) = sK13(sK15)
| next_subocc(sK12(sK15),sK14(sK12(sK15)),tptp0)
| ~ arboreal(sK12(sK15))
| ~ min_precedes(sK12(sK15),sK13(sK15),tptp0)
| ~ spl16_65 ),
inference(resolution,[],[f1189,f290]) ).
fof(f1768,plain,
( sK12(sK15) = sK13(sK15)
| next_subocc(sK12(sK15),sK14(sK12(sK15)),tptp0)
| ~ min_precedes(sK12(sK15),sK13(sK15),tptp0)
| ~ spl16_65 ),
inference(forward_subsumption_resolution,[],[f1765,f217]) ).
fof(f1770,definition,
( spl16_94
<=> min_precedes(sK12(sK15),sK13(sK15),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_94])],[avatar_definition]) ).
fof(f1772,plain,
( ~ min_precedes(sK12(sK15),sK13(sK15),tptp0)
| spl16_94 ),
inference(avatar_component_clause,[],[f1770]) ).
fof(f1774,definition,
( spl16_95
<=> sK12(sK15) = sK13(sK15) ),
introduced(definition,[new_symbols(definition,[spl16_95])],[avatar_definition]) ).
fof(f1776,plain,
( sK12(sK15) = sK13(sK15)
| ~ spl16_95 ),
inference(avatar_component_clause,[],[f1774]) ).
fof(f1779,definition,
( spl16_96
<=> next_subocc(sK12(sK15),sK14(sK12(sK15)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_96])],[avatar_definition]) ).
fof(f1781,plain,
( next_subocc(sK12(sK15),sK14(sK12(sK15)),tptp0)
| ~ spl16_96 ),
inference(avatar_component_clause,[],[f1779]) ).
fof(f1782,plain,
( ~ spl16_94
| spl16_96
| spl16_95
| ~ spl16_65 ),
inference(avatar_split_clause,[],[f1768,f1188,f1774,f1779,f1770]) ).
fof(f1784,plain,
( ~ subactivity_occurrence(sK12(sK15),sK15)
| sK12(sK15) = sK13(sK15)
| ~ arboreal(sK12(sK15))
| ~ occurrence_of(sK15,tptp0)
| ~ occurrence_of(sK15,tptp0)
| spl16_94 ),
inference(resolution,[],[f1772,f214]) ).
fof(f1786,plain,
( ~ subactivity_occurrence(sK12(sK15),sK15)
| sK12(sK15) = sK13(sK15)
| ~ arboreal(sK12(sK15))
| ~ occurrence_of(sK15,tptp0)
| spl16_94 ),
inference(duplicate_literal_removal,[],[f1784]) ).
fof(f1788,plain,
( sK12(sK15) = sK13(sK15)
| ~ arboreal(sK12(sK15))
| ~ occurrence_of(sK15,tptp0)
| spl16_94 ),
inference(forward_subsumption_resolution,[],[f1786,f1346]) ).
fof(f1792,plain,
( sK12(sK15) = sK13(sK15)
| ~ occurrence_of(sK15,tptp0)
| spl16_94 ),
inference(forward_subsumption_resolution,[],[f1788,f207]) ).
fof(f1794,plain,
( sK12(sK15) = sK13(sK15)
| spl16_94 ),
inference(forward_subsumption_resolution,[],[f1792,f201]) ).
fof(f1796,plain,
( spl16_95
| spl16_94 ),
inference(avatar_split_clause,[],[f1794,f1770,f1774]) ).
fof(f1808,plain,
( tptp3 = sK4(sK12(sK15))
| ~ spl16_95 ),
inference(superposition,[],[f540,f1776]) ).
fof(f1893,plain,
( tptp4 = tptp3
| ~ spl16_95 ),
inference(forward_demodulation,[],[f1808,f554]) ).
fof(f1896,plain,
( $false
| ~ spl16_95 ),
inference(forward_subsumption_resolution,[],[f1893,f194]) ).
fof(f1897,plain,
~ spl16_95,
inference(avatar_contradiction_clause,[],[f1896]) ).
fof(f1930,plain,
( min_precedes(sK12(sK15),sK14(sK12(sK15)),tptp0)
| ~ spl16_96 ),
inference(resolution,[],[f1781,f175]) ).
fof(f1958,definition,
( spl16_99
<=> sK14(sK12(sK15)) = sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))) ),
introduced(definition,[new_symbols(definition,[spl16_99])],[avatar_definition]) ).
fof(f1959,plain,
( sK14(sK12(sK15)) != sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| spl16_99 ),
inference(avatar_component_clause,[],[f1958]) ).
fof(f1960,plain,
( sK14(sK12(sK15)) = sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ spl16_99 ),
inference(avatar_component_clause,[],[f1958]) ).
fof(f1969,plain,
( occurrence_of(sK14(sK12(sK15)),tptp3)
| ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| ~ spl16_99 ),
inference(superposition,[],[f185,f1960]) ).
fof(f2034,definition,
( spl16_111
<=> min_precedes(sK12(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),sK14(sK12(sK15)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_111])],[avatar_definition]) ).
fof(f2035,plain,
( ~ min_precedes(sK12(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),sK14(sK12(sK15)),tptp0)
| spl16_111 ),
inference(avatar_component_clause,[],[f2034]) ).
fof(f2036,plain,
( min_precedes(sK12(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),sK14(sK12(sK15)),tptp0)
| ~ spl16_111 ),
inference(avatar_component_clause,[],[f2034]) ).
fof(f2039,definition,
( spl16_112
<=> subactivity_occurrence(sK14(sK12(sK15)),sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))) ),
introduced(definition,[new_symbols(definition,[spl16_112])],[avatar_definition]) ).
fof(f2040,plain,
( ~ subactivity_occurrence(sK14(sK12(sK15)),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| spl16_112 ),
inference(avatar_component_clause,[],[f2039]) ).
fof(f2041,plain,
( subactivity_occurrence(sK14(sK12(sK15)),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ spl16_112 ),
inference(avatar_component_clause,[],[f2039]) ).
fof(f2052,definition,
( spl16_115
<=> occurrence_of(sK14(sK12(sK15)),tptp3) ),
introduced(definition,[new_symbols(definition,[spl16_115])],[avatar_definition]) ).
fof(f2054,plain,
( occurrence_of(sK14(sK12(sK15)),tptp3)
| ~ spl16_115 ),
inference(avatar_component_clause,[],[f2052]) ).
fof(f2055,plain,
( ~ spl16_81
| spl16_115
| ~ spl16_99 ),
inference(avatar_split_clause,[],[f1969,f1958,f2052,f1517]) ).
fof(f2062,definition,
( spl16_117
<=> next_subocc(sK12(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),sK14(sK12(sK15)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_117])],[avatar_definition]) ).
fof(f2063,plain,
( ~ next_subocc(sK12(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),sK14(sK12(sK15)),tptp0)
| spl16_117 ),
inference(avatar_component_clause,[],[f2062]) ).
fof(f2064,plain,
( next_subocc(sK12(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),sK14(sK12(sK15)),tptp0)
| ~ spl16_117 ),
inference(avatar_component_clause,[],[f2062]) ).
fof(f2294,plain,
( ~ occurrence_of(sK15,tptp0)
| tptp3 = tptp1
| ~ spl16_115 ),
inference(resolution,[],[f2054,f277]) ).
fof(f2304,plain,
( tptp3 = tptp1
| ~ spl16_115 ),
inference(forward_subsumption_resolution,[],[f2294,f201]) ).
fof(f2307,plain,
( $false
| ~ spl16_115 ),
inference(forward_subsumption_resolution,[],[f2304,f196]) ).
fof(f2308,plain,
~ spl16_115,
inference(avatar_contradiction_clause,[],[f2307]) ).
fof(f2573,plain,
( min_precedes(sK12(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),sK14(sK12(sK15)),tptp0)
| ~ spl16_117 ),
inference(resolution,[],[f2064,f175]) ).
fof(f2574,plain,
( ~ min_precedes(sK12(sK15),sK14(sK12(sK15)),tptp0)
| spl16_81 ),
inference(resolution,[],[f1518,f137]) ).
fof(f2575,plain,
( $false
| spl16_81
| ~ spl16_96 ),
inference(forward_subsumption_resolution,[],[f2574,f1930]) ).
fof(f2576,plain,
( spl16_81
| ~ spl16_96 ),
inference(avatar_contradiction_clause,[],[f2575]) ).
fof(f2779,plain,
( $false
| spl16_111
| ~ spl16_117 ),
inference(forward_subsumption_resolution,[],[f2573,f2035]) ).
fof(f2780,plain,
( spl16_111
| ~ spl16_117 ),
inference(avatar_contradiction_clause,[],[f2779]) ).
fof(f3140,definition,
( spl16_219
<=> ! [X0] : ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),X0) ),
introduced(definition,[new_symbols(definition,[spl16_219])],[avatar_definition]) ).
fof(f3141,plain,
( ! [X0] : ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),X0)
| ~ spl16_219 ),
inference(avatar_component_clause,[],[f3140]) ).
fof(f3145,plain,
( ~ min_precedes(sK12(sK15),sK14(sK12(sK15)),tptp0)
| ~ spl16_219 ),
inference(resolution,[],[f3141,f137]) ).
fof(f3153,plain,
( $false
| ~ spl16_96
| ~ spl16_219 ),
inference(forward_subsumption_resolution,[],[f3145,f1930]) ).
fof(f3154,plain,
( ~ spl16_96
| ~ spl16_219 ),
inference(avatar_contradiction_clause,[],[f3153]) ).
fof(f3738,definition,
( spl16_274
<=> min_precedes(sK14(sK12(sK15)),sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_274])],[avatar_definition]) ).
fof(f3739,plain,
( min_precedes(sK14(sK12(sK15)),sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),tptp0)
| ~ spl16_274 ),
inference(avatar_component_clause,[],[f3738]) ).
fof(f3740,plain,
( ~ min_precedes(sK14(sK12(sK15)),sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),tptp0)
| spl16_274 ),
inference(avatar_component_clause,[],[f3738]) ).
fof(f4269,plain,
( ! [X0,X1] :
( ~ subactivity_occurrence(sK14(sK12(sK15)),X0)
| ~ root_occ(sK12(sK15),X0)
| ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,tptp0)
| min_precedes(sK14(sK12(sK15)),X1,tptp0)
| sK14(sK12(sK15)) = X1 )
| ~ spl16_96 ),
inference(resolution,[],[f130,f1930]) ).
fof(f4280,plain,
( ! [X0] :
( ~ root_occ(sK12(sK15),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ leaf_occ(X0,sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| min_precedes(sK14(sK12(sK15)),X0,tptp0)
| sK14(sK12(sK15)) = X0 )
| ~ spl16_96
| ~ spl16_112 ),
inference(resolution,[],[f4269,f2041]) ).
fof(f4283,plain,
( ! [X0] :
( ~ root_occ(sK12(sK15),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ leaf_occ(X0,sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| min_precedes(sK14(sK12(sK15)),X0,tptp0)
| sK14(sK12(sK15)) = X0 )
| ~ spl16_81
| ~ spl16_96
| ~ spl16_112 ),
inference(forward_subsumption_resolution,[],[f4280,f1519]) ).
fof(f4285,definition,
( spl16_298
<=> ! [X0] :
( ~ leaf_occ(X0,sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| sK14(sK12(sK15)) = X0
| min_precedes(sK14(sK12(sK15)),X0,tptp0) ) ),
introduced(definition,[new_symbols(definition,[spl16_298])],[avatar_definition]) ).
fof(f4286,plain,
( ! [X0] :
( ~ leaf_occ(X0,sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| sK14(sK12(sK15)) = X0
| min_precedes(sK14(sK12(sK15)),X0,tptp0) )
| ~ spl16_298 ),
inference(avatar_component_clause,[],[f4285]) ).
fof(f4288,definition,
( spl16_299
<=> root_occ(sK12(sK15),sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))) ),
introduced(definition,[new_symbols(definition,[spl16_299])],[avatar_definition]) ).
fof(f4289,plain,
( root_occ(sK12(sK15),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ spl16_299 ),
inference(avatar_component_clause,[],[f4288]) ).
fof(f4290,plain,
( ~ root_occ(sK12(sK15),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| spl16_299 ),
inference(avatar_component_clause,[],[f4288]) ).
fof(f4291,plain,
( spl16_298
| ~ spl16_299
| ~ spl16_81
| ~ spl16_96
| ~ spl16_112 ),
inference(avatar_split_clause,[],[f4283,f2039,f1779,f1517,f4288,f4285]) ).
fof(f4534,definition,
( spl16_304
<=> sK12(sK15) = sK12(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))) ),
introduced(definition,[new_symbols(definition,[spl16_304])],[avatar_definition]) ).
fof(f4535,plain,
( sK12(sK15) != sK12(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| spl16_304 ),
inference(avatar_component_clause,[],[f4534]) ).
fof(f4536,plain,
( sK12(sK15) = sK12(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ spl16_304 ),
inference(avatar_component_clause,[],[f4534]) ).
fof(f4555,plain,
( ~ next_subocc(sK12(sK15),sK14(sK12(sK15)),tptp0)
| spl16_117
| ~ spl16_304 ),
inference(superposition,[],[f2063,f4536]) ).
fof(f4616,plain,
( $false
| ~ spl16_96
| spl16_117
| ~ spl16_304 ),
inference(forward_subsumption_resolution,[],[f4555,f1781]) ).
fof(f4617,plain,
( ~ spl16_96
| spl16_117
| ~ spl16_304 ),
inference(avatar_contradiction_clause,[],[f4616]) ).
fof(f4954,definition,
( spl16_323
<=> subactivity_occurrence(sK12(sK15),sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))) ),
introduced(definition,[new_symbols(definition,[spl16_323])],[avatar_definition]) ).
fof(f4955,plain,
( subactivity_occurrence(sK12(sK15),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ spl16_323 ),
inference(avatar_component_clause,[],[f4954]) ).
fof(f5799,plain,
( ! [X0] :
( ~ subactivity_occurrence(sK14(sK12(sK15)),X0)
| ~ occurrence_of(X0,tptp0)
| subactivity_occurrence(sK12(sK15),X0) )
| ~ spl16_96 ),
inference(resolution,[],[f178,f1930]) ).
fof(f5808,plain,
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| subactivity_occurrence(sK12(sK15),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ spl16_96
| ~ spl16_112 ),
inference(resolution,[],[f5799,f2041]) ).
fof(f5811,plain,
( subactivity_occurrence(sK12(sK15),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ spl16_81
| ~ spl16_96
| ~ spl16_112 ),
inference(forward_subsumption_resolution,[],[f5808,f1519]) ).
fof(f5812,plain,
( spl16_323
| ~ spl16_81
| ~ spl16_96
| ~ spl16_112 ),
inference(avatar_split_clause,[],[f5811,f2039,f1779,f1517,f4954]) ).
fof(f5819,plain,
( ! [X0] :
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),X0)
| root_occ(sK12(sK15),sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ root(sK12(sK15),X0) )
| ~ spl16_323 ),
inference(resolution,[],[f4955,f163]) ).
fof(f5834,plain,
( ! [X0] :
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),X0)
| ~ root(sK12(sK15),X0) )
| spl16_299
| ~ spl16_323 ),
inference(forward_subsumption_resolution,[],[f5819,f4290]) ).
fof(f6179,plain,
( ~ root(sK12(sK15),tptp0)
| ~ min_precedes(sK12(sK15),sK14(sK12(sK15)),tptp0)
| spl16_299
| ~ spl16_323 ),
inference(resolution,[],[f5834,f137]) ).
fof(f6187,plain,
( ~ min_precedes(sK12(sK15),sK14(sK12(sK15)),tptp0)
| ~ spl16_83
| spl16_299
| ~ spl16_323 ),
inference(forward_subsumption_resolution,[],[f6179,f1569]) ).
fof(f6189,plain,
( $false
| ~ spl16_83
| ~ spl16_96
| spl16_299
| ~ spl16_323 ),
inference(forward_subsumption_resolution,[],[f6187,f1930]) ).
fof(f6190,plain,
( ~ spl16_83
| ~ spl16_96
| spl16_299
| ~ spl16_323 ),
inference(avatar_contradiction_clause,[],[f6189]) ).
fof(f6194,plain,
( sK14(sK12(sK15)) = sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| min_precedes(sK14(sK12(sK15)),sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),tptp0)
| ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| ~ spl16_298 ),
inference(resolution,[],[f4286,f184]) ).
fof(f6203,plain,
( ! [X0] :
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),X0)
| sK12(sK15) = sK12(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))))
| ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0) )
| ~ spl16_299 ),
inference(resolution,[],[f4289,f565]) ).
fof(f6209,plain,
( ! [X0] :
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),X0)
| ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0) )
| ~ spl16_299
| spl16_304 ),
inference(forward_subsumption_resolution,[],[f6203,f4535]) ).
fof(f6213,plain,
( ! [X0] : ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),X0)
| ~ spl16_81
| ~ spl16_299
| spl16_304 ),
inference(forward_subsumption_resolution,[],[f6209,f1519]) ).
fof(f6214,plain,
( spl16_219
| ~ spl16_81
| ~ spl16_299
| spl16_304 ),
inference(avatar_split_clause,[],[f6213,f4534,f4288,f1517,f3140]) ).
fof(f6924,plain,
! [X0,X1] :
( ~ min_precedes(sK12(X1),X0,tptp0)
| ~ min_precedes(X0,sK13(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(resolution,[],[f174,f183]) ).
fof(f6958,plain,
( ~ min_precedes(sK14(sK12(sK15)),sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),tptp0)
| ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| ~ spl16_111 ),
inference(resolution,[],[f6924,f2036]) ).
fof(f6975,plain,
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| ~ spl16_111
| ~ spl16_274 ),
inference(forward_subsumption_resolution,[],[f6958,f3739]) ).
fof(f6994,plain,
( $false
| ~ spl16_81
| ~ spl16_111
| ~ spl16_274 ),
inference(forward_subsumption_resolution,[],[f6975,f1519]) ).
fof(f6995,plain,
( ~ spl16_81
| ~ spl16_111
| ~ spl16_274 ),
inference(avatar_contradiction_clause,[],[f6994]) ).
fof(f7010,plain,
( min_precedes(sK14(sK12(sK15)),sK13(sK2(tptp0,sK12(sK15),sK14(sK12(sK15)))),tptp0)
| ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| spl16_99
| ~ spl16_298 ),
inference(forward_subsumption_resolution,[],[f6194,f1959]) ).
fof(f7013,plain,
( ~ occurrence_of(sK2(tptp0,sK12(sK15),sK14(sK12(sK15))),tptp0)
| spl16_99
| spl16_274
| ~ spl16_298 ),
inference(forward_subsumption_resolution,[],[f7010,f3740]) ).
fof(f7017,plain,
( $false
| ~ spl16_81
| spl16_99
| spl16_274
| ~ spl16_298 ),
inference(forward_subsumption_resolution,[],[f7013,f1519]) ).
fof(f7018,plain,
( ~ spl16_81
| spl16_99
| spl16_274
| ~ spl16_298 ),
inference(avatar_contradiction_clause,[],[f7017]) ).
fof(f7030,plain,
( ~ min_precedes(sK12(sK15),sK14(sK12(sK15)),tptp0)
| spl16_112 ),
inference(resolution,[],[f2040,f135]) ).
fof(f7031,plain,
( $false
| ~ spl16_96
| spl16_112 ),
inference(forward_subsumption_resolution,[],[f7030,f1930]) ).
fof(f7032,plain,
( ~ spl16_96
| spl16_112 ),
inference(avatar_contradiction_clause,[],[f7031]) ).
cnf(s4,plain,
spl16_5,
inference(sat_conversion,[],[f490]) ).
cnf(s12,plain,
( ~ spl16_4
| spl16_16 ),
inference(sat_conversion,[],[f635]) ).
cnf(s13,plain,
spl16_4,
inference(sat_conversion,[],[f642]) ).
cnf(s66,plain,
( ~ spl16_5
| ~ spl16_16
| spl16_19
| spl16_65 ),
inference(sat_conversion,[],[f1190]) ).
cnf(s86,plain,
( ~ spl16_4
| ~ spl16_19 ),
inference(sat_conversion,[],[f1337]) ).
cnf(s92,plain,
( ~ spl16_82
| spl16_83 ),
inference(sat_conversion,[],[f1570]) ).
cnf(s93,plain,
spl16_82,
inference(sat_conversion,[],[f1573]) ).
cnf(s101,plain,
( ~ spl16_65
| ~ spl16_94
| spl16_95
| spl16_96 ),
inference(sat_conversion,[],[f1782]) ).
cnf(s104,plain,
( spl16_94
| spl16_95 ),
inference(sat_conversion,[],[f1796]) ).
cnf(s111,plain,
~ spl16_95,
inference(sat_conversion,[],[f1897]) ).
cnf(s129,plain,
( ~ spl16_81
| ~ spl16_99
| spl16_115 ),
inference(sat_conversion,[],[f2055]) ).
cnf(s169,plain,
~ spl16_115,
inference(sat_conversion,[],[f2308]) ).
cnf(s202,plain,
( spl16_81
| ~ spl16_96 ),
inference(sat_conversion,[],[f2576]) ).
cnf(s228,plain,
( spl16_111
| ~ spl16_117 ),
inference(sat_conversion,[],[f2780]) ).
cnf(s285,plain,
( ~ spl16_96
| ~ spl16_219 ),
inference(sat_conversion,[],[f3154]) ).
cnf(s415,plain,
( ~ spl16_81
| ~ spl16_96
| ~ spl16_112
| spl16_298
| ~ spl16_299 ),
inference(sat_conversion,[],[f4291]) ).
cnf(s431,plain,
( ~ spl16_96
| spl16_117
| ~ spl16_304 ),
inference(sat_conversion,[],[f4617]) ).
cnf(s543,plain,
( ~ spl16_81
| ~ spl16_96
| ~ spl16_112
| spl16_323 ),
inference(sat_conversion,[],[f5812]) ).
cnf(s563,plain,
( ~ spl16_83
| ~ spl16_96
| spl16_299
| ~ spl16_323 ),
inference(sat_conversion,[],[f6190]) ).
cnf(s567,plain,
( ~ spl16_81
| spl16_219
| ~ spl16_299
| spl16_304 ),
inference(sat_conversion,[],[f6214]) ).
cnf(s609,plain,
( ~ spl16_81
| ~ spl16_111
| ~ spl16_274 ),
inference(sat_conversion,[],[f6995]) ).
cnf(s612,plain,
( ~ spl16_81
| spl16_99
| spl16_274
| ~ spl16_298 ),
inference(sat_conversion,[],[f7018]) ).
cnf(s613,plain,
( ~ spl16_96
| spl16_112 ),
inference(sat_conversion,[],[f7032]) ).
cnf(s615,plain,
( ~ spl16_81
| ~ spl16_99 ),
inference(rat,[],[s129,s169]) ).
cnf(s617,plain,
spl16_94,
inference(rat,[],[s104,s111]) ).
cnf(s619,plain,
( ~ spl16_65
| spl16_96 ),
inference(rat,[],[s101,s111,s617]) ).
cnf(s623,plain,
spl16_83,
inference(rat,[],[s92,s93]) ).
cnf(s630,plain,
~ spl16_19,
inference(rat,[],[s86,s13]) ).
cnf(s635,plain,
spl16_16,
inference(rat,[],[s12,s13]) ).
cnf(s646,plain,
spl16_65,
inference(rat,[],[s66,s635,s630,s4]) ).
cnf(s652,plain,
spl16_96,
inference(rat,[],[s619,s646]) ).
cnf(s659,plain,
spl16_112,
inference(rat,[],[s613,s652]) ).
cnf(s660,plain,
~ spl16_219,
inference(rat,[],[s285,s652]) ).
cnf(s661,plain,
spl16_81,
inference(rat,[],[s202,s652]) ).
cnf(s664,plain,
spl16_323,
inference(rat,[],[s543,s652,s659,s661]) ).
cnf(s671,plain,
~ spl16_99,
inference(rat,[],[s615,s661]) ).
cnf(s672,plain,
spl16_299,
inference(rat,[],[s563,s652,s623,s664]) ).
cnf(s682,plain,
spl16_304,
inference(rat,[],[s567,s661,s660,s672]) ).
cnf(s683,plain,
spl16_298,
inference(rat,[],[s415,s661,s652,s659,s672]) ).
cnf(s692,plain,
spl16_117,
inference(rat,[],[s431,s652,s682]) ).
cnf(s695,plain,
spl16_274,
inference(rat,[],[s612,s671,s661,s683]) ).
cnf(s701,plain,
spl16_111,
inference(rat,[],[s228,s692]) ).
cnf(s705,plain,
$false,
inference(rat,[],[s609,s661,s695,s701]) ).
fof(f7033,plain,
$false,
inference(avatar_sat_refutation,[],[s705]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO006+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n016.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 22:23:04 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 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
% 5.83/1.79 % (3052896)Detected formulas, will run a generic FOF schedule.
% 5.83/1.79 % (3052901)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=3381639952:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.83/1.79 % (3052902)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=2927729298:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.83/1.79 % (3052906)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2918385372:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.83/1.79 % (3052904)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1202771164:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.83/1.79 % (3052905)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3230628601:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.83/1.79 % (3052907)dis-21_1_sil=8000:lcm=predicate:random_seed=4288665189: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)
% 5.83/1.79 % (3052903)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=1089494432:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.83/1.79 % (3052905)Refutation not found, incomplete strategy
% 5.83/1.79 % (3052905)------------------------------
% 5.83/1.79 % (3052905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3052905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3052904)Refutation not found, incomplete strategy
% 5.83/1.79 % (3052904)------------------------------
% 5.83/1.79 % (3052904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3052904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3052905)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3052905)Termination reason: Refutation not found, incomplete strategy
% 5.83/1.79 % (3052905)Time elapsed: 0.001 s
% 5.83/1.79 % (3052904)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3052905)Peak memory usage: 86 MB
% 5.83/1.79 % (3052904)Termination reason: Refutation not found, incomplete strategy
% 5.83/1.79 % (3052904)Time elapsed: 0.001 s
% 5.83/1.79 % (3052904)Peak memory usage: 86 MB
% 5.83/1.79 % (3052907)Instruction limit reached!
% 5.83/1.79 % (3052907)------------------------------
% 5.83/1.79 % (3052907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3052907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3052907)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3052907)Termination reason: Instruction limit
% 5.83/1.79 % (3052907)Termination phase: Saturation
% 5.83/1.79 % (3052907)Time elapsed: 0.079 s
% 5.83/1.79 % (3052907)Peak memory usage: 89 MB
% 5.83/1.79 % (3052907)Instructions burned: 129 (million)
% 5.83/1.79 % (3052906)Instruction limit reached!
% 5.83/1.79 % (3052906)------------------------------
% 5.83/1.79 % (3052906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3052906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3052906)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3052906)Termination reason: Instruction limit
% 5.83/1.79 % (3052906)Termination phase: Saturation
% 5.83/1.79 % (3052906)Time elapsed: 0.100 s
% 5.83/1.79 % (3052906)Peak memory usage: 90 MB
% 5.83/1.79 % (3052906)Instructions burned: 139 (million)
% 5.83/1.79 % (3052915)lrs+10_1_sil=8000:sp=occurrence:random_seed=3093513943:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.83/1.79 % (3052904)------------------------------
% 5.83/1.79 % (3052904)------------------------------
% 5.83/1.79 % (3052905)------------------------------
% 5.83/1.79 % (3052905)------------------------------
% 5.83/1.79 % (3052916)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2639176497:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.83/1.79 % (3052916)Refutation not found, incomplete strategy
% 5.83/1.79 % (3052916)------------------------------
% 5.83/1.79 % (3052916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3052916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3052916)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3052916)Termination reason: Refutation not found, incomplete strategy
% 5.83/1.79 % (3052916)Time elapsed: 0.001 s
% 5.83/1.79 % (3052916)Peak memory usage: 88 MB
% 5.83/1.79 % (3052915)Instruction limit reached!
% 5.83/1.79 % (3052915)------------------------------
% 5.83/1.79 % (3052915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3052915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3052915)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3052915)Termination reason: Instruction limit
% 5.83/1.79 % (3052915)Termination phase: Saturation
% 5.83/1.79 % (3052915)Time elapsed: 0.180 s
% 5.83/1.79 % (3052915)Peak memory usage: 91 MB
% 5.83/1.79 % (3052915)Instructions burned: 286 (million)
% 5.83/1.79 % (3052918)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1472460620:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 5.83/1.79 % (3052919)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=2604380035:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 5.83/1.79 % (3052916)------------------------------
% 5.83/1.79 % (3052916)------------------------------
% 5.83/1.79 % (3052919)Instruction limit reached!
% 5.83/1.79 % (3052919)------------------------------
% 5.83/1.79 % (3052919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3052919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3052919)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3052919)Termination reason: Instruction limit
% 5.83/1.79 % (3052919)Termination phase: Saturation
% 5.83/1.79 % (3052919)Time elapsed: 0.142 s
% 5.83/1.79 % (3052919)Peak memory usage: 89 MB
% 5.83/1.79 % (3052919)Instructions burned: 249 (million)
% 5.83/1.79 % (3052923)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=961848074:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 5.83/1.79 % (3052901)First to succeed.
% 5.83/1.79 % (3052901)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3052896"
% 5.83/1.79 % (3052918)Instruction limit reached!
% 5.83/1.79 % (3052918)------------------------------
% 5.83/1.79 % (3052918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3052918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3052918)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3052918)Termination reason: Instruction limit
% 5.83/1.79 % (3052918)Termination phase: Saturation
% 5.83/1.79 % (3052918)Time elapsed: 0.195 s
% 5.83/1.79 % (3052918)Peak memory usage: 90 MB
% 5.83/1.79 % (3052918)Instructions burned: 326 (million)
% 5.83/1.79 % (3052924)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=382316459:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 5.83/1.79 % (3052925)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=625430004:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 5.83/1.79 % (3052923)Instruction limit reached!
% 5.83/1.79 % (3052923)------------------------------
% 5.83/1.79 % (3052923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3052923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3052923)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3052923)Termination reason: Instruction limit
% 5.83/1.79 % (3052923)Termination phase: Saturation
% 5.83/1.79 % (3052923)Time elapsed: 0.169 s
% 5.83/1.79 % (3052923)Peak memory usage: 89 MB
% 5.83/1.79 % (3052923)Instructions burned: 295 (million)
% 5.83/1.79 % (3052901)Refutation found. Thanks to Tanya!
% 5.83/1.79 % SZS status Theorem for theBenchmark
% 5.83/1.79 % SZS output start Proof for theBenchmark
% See solution above
% 7.14/1.99 % (3052901)------------------------------
% 7.14/1.99 % (3052901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.14/1.99 % (3052901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.99 % (3052901)CaDiCaL version: 2.1.3
% 7.14/1.99 % (3052901)Termination reason: Refutation
% 7.14/1.99 % (3052901)Time elapsed: 0.636 s
% 7.14/1.99 % (3052901)Peak memory usage: 136 MB
% 7.14/1.99 % (3052901)Instructions burned: 1673 (million)
% 7.14/1.99 % (3052901)------------------------------
% 7.14/1.99 % (3052901)------------------------------
% 7.14/1.99 % (3052896)Success in time 0.936 s
% 7.14/1.99 % Vampire exiting
%------------------------------------------------------------------------------