%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PRO005+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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:22 PM UTC 2026
% Result : Theorem 14.75s 3.04s
% Output : Refutation 15.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 43
% Syntax : Number of formulae : 308 ( 50 unt; 22 def)
% Number of atoms : 950 ( 36 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 1130 ( 488 ~; 514 |; 87 &)
% ( 30 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 35 ( 33 usr; 23 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-3 aty)
% Number of variables : 283 ( 0 sgn 252 !; 31 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
fof(f8,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_07) ).
fof(f9,axiom,
! [X0] :
( legal(X0)
=> arboreal(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_08) ).
fof(f15,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ~ root(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_14) ).
fof(f17,axiom,
! [X0,X1] :
( root(X0,X1)
=> legal(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_16) ).
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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',sos_28) ).
fof(f30,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X0,X1,X2)
& occurrence_of(X3,X2)
& subactivity_occurrence(X1,X3) )
=> subactivity_occurrence(X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_29) ).
fof(f34,axiom,
! [X0,X1] :
( root_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_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/sandbox2/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)
| occurrence_of(X2,tptp2) )
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_35) ).
fof(f40,axiom,
atomic(tptp3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_39) ).
fof(f41,axiom,
atomic(tptp2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_40) ).
fof(f42,axiom,
atomic(tptp1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_41) ).
fof(f46,axiom,
tptp1 != tptp3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_45) ).
fof(f47,axiom,
tptp1 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_46) ).
fof(f49,axiom,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> root_occ(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_48) ).
fof(f50,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/sandbox2/benchmark/theBenchmark.p',sos_49) ).
fof(f51,conjecture,
~ ? [X0] : occurrence_of(X0,tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f52,negated_conjecture,
~ ~ ? [X0] : occurrence_of(X0,tptp0),
inference(negated_conjecture,[status(cth)],[f51]) ).
fof(f53,plain,
? [X0] : occurrence_of(X0,tptp0),
inference(flattening,[],[f52]) ).
fof(f56,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f3]) ).
fof(f57,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f56]) ).
fof(f64,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f65,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f71,plain,
! [X0,X1,X2] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f15]) ).
fof(f73,plain,
! [X0,X1] :
( legal(X0)
| ~ root(X0,X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f81,plain,
! [X0,X1] :
( leaf(X0,X1)
<=> ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) ) ),
inference(ennf_transformation,[],[f22]) ).
fof(f82,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,[],[f23]) ).
fof(f84,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(f89,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(f90,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,[],[f89]) ).
fof(f91,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,[],[f30]) ).
fof(f92,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ min_precedes(X0,X1,X2)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(flattening,[],[f91]) ).
fof(f99,plain,
! [X0] :
( ? [X1,X2] :
( occurrence_of(X1,tptp4)
& root_occ(X1,X0)
& ( occurrence_of(X2,tptp3)
| occurrence_of(X2,tptp2) )
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f100,plain,
! [X0,X1] :
( root_occ(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f49]) ).
fof(f101,plain,
! [X0,X1] :
( root_occ(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(flattening,[],[f100]) ).
fof(f102,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,[],[f50]) ).
fof(f103,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,[],[f102]) ).
fof(f105,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f64]) ).
fof(f111,plain,
! [X0,X1] :
( ( leaf(X0,X1)
| ( ~ root(X0,X1)
& ! [X2] : ~ min_precedes(X2,X0,X1) )
| ? [X3] : min_precedes(X0,X3,X1) )
& ( ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) )
| ~ leaf(X0,X1) ) ),
inference(nnf_transformation,[],[f81]) ).
fof(f112,plain,
! [X0,X1] :
( ( leaf(X0,X1)
| ( ~ root(X0,X1)
& ! [X2] : ~ min_precedes(X2,X0,X1) )
| ? [X3] : min_precedes(X0,X3,X1) )
& ( ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) )
| ~ leaf(X0,X1) ) ),
inference(flattening,[],[f111]) ).
fof(f113,plain,
! [X0,X1] :
( ( leaf(X0,X1)
| ( ~ root(X0,X1)
& ! [X2] : ~ min_precedes(X2,X0,X1) )
| ? [X3] : min_precedes(X0,X3,X1) )
& ( ( ( root(X0,X1)
| ? [X4] : min_precedes(X4,X0,X1) )
& ! [X5] : ~ min_precedes(X0,X5,X1) )
| ~ leaf(X0,X1) ) ),
inference(rectify,[],[f112]) ).
fof(f114,plain,
! [X0,X1] :
( ( leaf(X0,X1)
| ( ~ root(X0,X1)
& ! [X2] : ~ min_precedes(X2,X0,X1) )
| min_precedes(X0,sK5(X0,X1),X1) )
& ( ( ( root(X0,X1)
| min_precedes(sK6(X0,X1),X0,X1) )
& ! [X5] : ~ min_precedes(X0,X5,X1) )
| ~ leaf(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6]),skolemize(X3,sK5(X0,X1)),skolemize(X4,sK6(X0,X1))],[f113]) ).
fof(f115,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,[],[f82]) ).
fof(f116,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,[],[f115]) ).
fof(f117,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,[],[f116]) ).
fof(f118,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ( min_precedes(X0,sK7(X0,X1,X2),X2)
& min_precedes(sK7(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,[sK7]),skolemize(X3,sK7(X0,X1,X2))],[f117]) ).
fof(f122,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK9(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK9(X0,X1,X2))
& subactivity_occurrence(X2,sK9(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X3,sK9(X0,X1,X2))],[f84]) ).
fof(f126,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(f127,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,[],[f126]) ).
fof(f128,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ( occurrence_of(X1,sK13(X0,X1))
& subactivity_occurrence(X0,X1)
& root(X0,sK13(X0,X1)) )
| ~ root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X3,sK13(X0,X1))],[f127]) ).
fof(f129,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) )
| ~ leaf_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f35]) ).
fof(f130,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ? [X3] :
( occurrence_of(X1,X3)
& subactivity_occurrence(X0,X1)
& leaf(X0,X3) )
| ~ leaf_occ(X0,X1) ) ),
inference(rectify,[],[f129]) ).
fof(f131,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ( occurrence_of(X1,sK14(X0,X1))
& subactivity_occurrence(X0,X1)
& leaf(X0,sK14(X0,X1)) )
| ~ leaf_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X3,sK14(X0,X1))],[f130]) ).
fof(f132,plain,
! [X0] :
( ( occurrence_of(sK15(X0),tptp4)
& root_occ(sK15(X0),X0)
& ( occurrence_of(sK16(X0),tptp3)
| occurrence_of(sK16(X0),tptp2) )
& leaf_occ(sK16(X0),X0)
& next_subocc(sK15(X0),sK16(X0),tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16]),skolemize(X1,sK15(X0)),skolemize(X2,sK16(X0))],[f99]) ).
fof(f133,plain,
! [X0,X1] :
( ( occurrence_of(sK17(X0),tptp1)
& next_subocc(X0,sK17(X0),tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(X2,sK17(X0))],[f103]) ).
fof(f134,plain,
occurrence_of(sK18,tptp0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X0,sK18)],[f53]) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f57]) ).
fof(f145,plain,
! [X0,X1] :
( ~ atomic(X1)
| arboreal(X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[],[f105]) ).
fof(f146,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(cnf_transformation,[],[f65]) ).
fof(f159,plain,
! [X2,X0,X1] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f71]) ).
fof(f161,plain,
! [X0,X1] :
( ~ root(X0,X1)
| legal(X0) ),
inference(cnf_transformation,[],[f73]) ).
fof(f166,plain,
! [X0,X1,X5] :
( ~ min_precedes(X0,X5,X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[],[f114]) ).
fof(f170,plain,
! [X2,X0,X1,X4] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) ),
inference(cnf_transformation,[],[f118]) ).
fof(f171,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f118]) ).
fof(f180,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK9(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f181,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X1,sK9(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f182,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| occurrence_of(sK9(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f187,plain,
! [X2,X3,X0,X1] :
( ~ arboreal(X3)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| min_precedes(X2,X3,X0)
| ~ subactivity_occurrence(X2,X1)
| ~ subactivity_occurrence(X3,X1) ),
inference(cnf_transformation,[],[f90]) ).
fof(f188,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,[],[f92]) ).
fof(f193,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| root(X0,sK13(X0,X1)) ),
inference(cnf_transformation,[],[f128]) ).
fof(f195,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| occurrence_of(X1,sK13(X0,X1)) ),
inference(cnf_transformation,[],[f128]) ).
fof(f197,plain,
! [X0,X1] :
( leaf(X0,sK14(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f131]) ).
fof(f198,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f131]) ).
fof(f199,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| occurrence_of(X1,sK14(X0,X1)) ),
inference(cnf_transformation,[],[f131]) ).
fof(f201,plain,
! [X0] :
( next_subocc(sK15(X0),sK16(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f132]) ).
fof(f202,plain,
! [X0] :
( leaf_occ(sK16(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f132]) ).
fof(f203,plain,
! [X0] :
( occurrence_of(sK16(X0),tptp2)
| occurrence_of(sK16(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f132]) ).
fof(f204,plain,
! [X0] :
( root_occ(sK15(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f132]) ).
fof(f209,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f40]) ).
fof(f210,plain,
atomic(tptp2),
inference(cnf_transformation,[],[f41]) ).
fof(f211,plain,
atomic(tptp1),
inference(cnf_transformation,[],[f42]) ).
fof(f215,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f46]) ).
fof(f216,plain,
tptp2 != tptp1,
inference(cnf_transformation,[],[f47]) ).
fof(f218,plain,
! [X0,X1] :
( ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| root_occ(X0,X1)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f219,plain,
! [X0,X1] :
( ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| next_subocc(X0,sK17(X0),tptp0)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f220,plain,
! [X0,X1] :
( ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| occurrence_of(sK17(X0),tptp1)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
fof(f221,plain,
occurrence_of(sK18,tptp0),
inference(cnf_transformation,[],[f134]) ).
fof(f222,plain,
! [X0] :
( ~ occurrence_of(sK18,X0)
| tptp0 = X0 ),
inference(resolution,[],[f139,f221]) ).
fof(f224,plain,
! [X0] :
( subactivity_occurrence(sK16(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f198,f202]) ).
fof(f226,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| occurrence_of(X0,sK14(sK16(X0),X0)) ),
inference(resolution,[],[f199,f202]) ).
fof(f236,definition,
( spl19_1
<=> leaf_occ(sK16(sK18),sK18) ),
introduced(definition,[new_symbols(definition,[spl19_1])],[avatar_definition]) ).
fof(f237,plain,
( ~ leaf_occ(sK16(sK18),sK18)
| spl19_1 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f243,plain,
( ~ occurrence_of(sK18,tptp0)
| spl19_1 ),
inference(resolution,[],[f237,f202]) ).
fof(f245,plain,
( $false
| spl19_1 ),
inference(forward_subsumption_resolution,[],[f243,f221]) ).
fof(f246,plain,
spl19_1,
inference(avatar_contradiction_clause,[],[f245]) ).
fof(f247,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| occurrence_of(X0,sK13(sK15(X0),X0)) ),
inference(resolution,[],[f195,f204]) ).
fof(f248,plain,
occurrence_of(sK18,sK13(sK15(sK18),sK18)),
inference(resolution,[],[f247,f221]) ).
fof(f250,plain,
tptp0 = sK13(sK15(sK18),sK18),
inference(resolution,[],[f248,f222]) ).
fof(f266,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| root(sK15(X0),sK13(sK15(X0),X0)) ),
inference(resolution,[],[f193,f204]) ).
fof(f267,plain,
root(sK15(sK18),sK13(sK15(sK18),sK18)),
inference(resolution,[],[f266,f221]) ).
fof(f268,plain,
root(sK15(sK18),tptp0),
inference(forward_demodulation,[],[f267,f250]) ).
fof(f269,plain,
! [X0] : ~ min_precedes(X0,sK15(sK18),tptp0),
inference(resolution,[],[f268,f159]) ).
fof(f270,plain,
! [X0] :
( min_precedes(sK15(X0),sK16(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f201,f171]) ).
fof(f288,plain,
! [X0] :
( ~ occurrence_of(X0,tptp2)
| arboreal(X0) ),
inference(resolution,[],[f210,f145]) ).
fof(f290,plain,
! [X0] :
( ~ occurrence_of(X0,tptp1)
| arboreal(X0) ),
inference(resolution,[],[f211,f145]) ).
fof(f292,plain,
! [X0] :
( ~ occurrence_of(X0,tptp3)
| arboreal(X0) ),
inference(resolution,[],[f209,f145]) ).
fof(f296,plain,
legal(sK15(sK18)),
inference(resolution,[],[f161,f268]) ).
fof(f297,plain,
! [X0,X1] :
( ~ occurrence_of(X1,tptp0)
| ~ min_precedes(sK15(X1),X0,tptp0)
| ~ min_precedes(X0,sK16(X1),tptp0) ),
inference(resolution,[],[f170,f201]) ).
fof(f298,plain,
! [X0] :
( ~ min_precedes(sK15(sK18),X0,tptp0)
| ~ min_precedes(X0,sK16(sK18),tptp0) ),
inference(resolution,[],[f297,f221]) ).
fof(f299,plain,
( ~ min_precedes(sK16(sK18),sK16(sK18),tptp0)
| ~ occurrence_of(sK18,tptp0) ),
inference(resolution,[],[f298,f270]) ).
fof(f300,plain,
~ min_precedes(sK16(sK18),sK16(sK18),tptp0),
inference(forward_subsumption_resolution,[],[f299,f221]) ).
fof(f301,plain,
! [X0,X1] :
( subactivity_occurrence(sK15(X0),X1)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(sK16(X0),X1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f188,f270]) ).
fof(f302,plain,
arboreal(sK15(sK18)),
inference(resolution,[],[f296,f146]) ).
fof(f314,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ subactivity_occurrence(sK15(sK18),X0)
| occurrence_of(sK17(sK15(sK18)),tptp1)
| leaf_occ(sK15(sK18),X0) ),
inference(resolution,[],[f302,f220]) ).
fof(f315,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ subactivity_occurrence(sK15(sK18),X0)
| next_subocc(sK15(sK18),sK17(sK15(sK18)),tptp0)
| leaf_occ(sK15(sK18),X0) ),
inference(resolution,[],[f302,f219]) ).
fof(f318,definition,
( spl19_7
<=> next_subocc(sK15(sK18),sK17(sK15(sK18)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl19_7])],[avatar_definition]) ).
fof(f319,plain,
( next_subocc(sK15(sK18),sK17(sK15(sK18)),tptp0)
| ~ spl19_7 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f321,definition,
( spl19_8
<=> ! [X0] :
( ~ occurrence_of(X0,tptp0)
| leaf_occ(sK15(sK18),X0)
| ~ subactivity_occurrence(sK15(sK18),X0) ) ),
introduced(definition,[new_symbols(definition,[spl19_8])],[avatar_definition]) ).
fof(f322,plain,
( ! [X0] :
( ~ occurrence_of(X0,tptp0)
| leaf_occ(sK15(sK18),X0)
| ~ subactivity_occurrence(sK15(sK18),X0) )
| ~ spl19_8 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f323,plain,
( spl19_7
| spl19_8 ),
inference(avatar_split_clause,[],[f315,f321,f318]) ).
fof(f325,definition,
( spl19_9
<=> occurrence_of(sK17(sK15(sK18)),tptp1) ),
introduced(definition,[new_symbols(definition,[spl19_9])],[avatar_definition]) ).
fof(f326,plain,
( occurrence_of(sK17(sK15(sK18)),tptp1)
| ~ spl19_9 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f327,plain,
( spl19_9
| spl19_8 ),
inference(avatar_split_clause,[],[f314,f321,f325]) ).
fof(f330,definition,
( spl19_10
<=> subactivity_occurrence(sK15(sK18),sK18) ),
introduced(definition,[new_symbols(definition,[spl19_10])],[avatar_definition]) ).
fof(f331,plain,
( ~ subactivity_occurrence(sK15(sK18),sK18)
| spl19_10 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f333,definition,
( spl19_11
<=> leaf_occ(sK15(sK18),sK18) ),
introduced(definition,[new_symbols(definition,[spl19_11])],[avatar_definition]) ).
fof(f334,plain,
( leaf_occ(sK15(sK18),sK18)
| ~ spl19_11 ),
inference(avatar_component_clause,[],[f333]) ).
fof(f338,plain,
( ~ occurrence_of(sK18,tptp0)
| ~ subactivity_occurrence(sK16(sK18),sK18)
| ~ occurrence_of(sK18,tptp0)
| spl19_10 ),
inference(resolution,[],[f331,f301]) ).
fof(f339,plain,
( ~ occurrence_of(sK18,tptp0)
| ~ subactivity_occurrence(sK16(sK18),sK18)
| spl19_10 ),
inference(duplicate_literal_removal,[],[f338]) ).
fof(f341,plain,
( ~ occurrence_of(sK18,tptp0)
| spl19_10 ),
inference(forward_subsumption_resolution,[],[f339,f224]) ).
fof(f344,plain,
( $false
| spl19_10 ),
inference(forward_subsumption_resolution,[],[f341,f221]) ).
fof(f345,plain,
spl19_10,
inference(avatar_contradiction_clause,[],[f344]) ).
fof(f346,plain,
( arboreal(sK17(sK15(sK18)))
| ~ spl19_9 ),
inference(resolution,[],[f326,f290]) ).
fof(f354,plain,
( ! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ subactivity_occurrence(sK17(sK15(sK18)),X0)
| next_subocc(sK17(sK15(sK18)),sK17(sK17(sK15(sK18))),tptp0)
| leaf_occ(sK17(sK15(sK18)),X0) )
| ~ spl19_9 ),
inference(resolution,[],[f346,f219]) ).
fof(f357,definition,
( spl19_12
<=> next_subocc(sK17(sK15(sK18)),sK17(sK17(sK15(sK18))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl19_12])],[avatar_definition]) ).
fof(f358,plain,
( next_subocc(sK17(sK15(sK18)),sK17(sK17(sK15(sK18))),tptp0)
| ~ spl19_12 ),
inference(avatar_component_clause,[],[f357]) ).
fof(f360,definition,
( spl19_13
<=> ! [X0] :
( ~ occurrence_of(X0,tptp0)
| leaf_occ(sK17(sK15(sK18)),X0)
| ~ subactivity_occurrence(sK17(sK15(sK18)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl19_13])],[avatar_definition]) ).
fof(f361,plain,
( ! [X0] :
( ~ occurrence_of(X0,tptp0)
| leaf_occ(sK17(sK15(sK18)),X0)
| ~ subactivity_occurrence(sK17(sK15(sK18)),X0) )
| ~ spl19_13 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f362,plain,
( spl19_12
| spl19_13
| ~ spl19_9 ),
inference(avatar_split_clause,[],[f354,f325,f360,f357]) ).
fof(f368,plain,
( occurrence_of(sK18,sK14(sK15(sK18),sK18))
| ~ spl19_11 ),
inference(resolution,[],[f334,f199]) ).
fof(f369,plain,
( subactivity_occurrence(sK15(sK18),sK18)
| ~ spl19_11 ),
inference(resolution,[],[f334,f198]) ).
fof(f372,plain,
( tptp0 = sK14(sK15(sK18),sK18)
| ~ spl19_11 ),
inference(resolution,[],[f368,f222]) ).
fof(f379,plain,
( leaf(sK15(sK18),tptp0)
| ~ leaf_occ(sK15(sK18),sK18)
| ~ spl19_11 ),
inference(superposition,[],[f197,f372]) ).
fof(f380,plain,
( leaf(sK15(sK18),tptp0)
| ~ spl19_11 ),
inference(forward_subsumption_resolution,[],[f379,f334]) ).
fof(f381,plain,
( leaf_occ(sK15(sK18),sK18)
| ~ subactivity_occurrence(sK15(sK18),sK18)
| ~ spl19_8 ),
inference(resolution,[],[f322,f221]) ).
fof(f383,plain,
( min_precedes(sK15(sK18),sK17(sK15(sK18)),tptp0)
| ~ spl19_7 ),
inference(resolution,[],[f319,f171]) ).
fof(f413,plain,
( ~ spl19_10
| spl19_11
| ~ spl19_8 ),
inference(avatar_split_clause,[],[f381,f321,f333,f330]) ).
fof(f457,plain,
! [X0] :
( arboreal(sK16(X0))
| occurrence_of(sK16(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f288,f203]) ).
fof(f458,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK16(X0)) ),
inference(forward_subsumption_resolution,[],[f457,f292]) ).
fof(f459,plain,
arboreal(sK16(sK18)),
inference(resolution,[],[f458,f221]) ).
fof(f461,plain,
! [X2,X0,X1] :
( ~ arboreal(X0)
| sK16(sK18) = X0
| ~ occurrence_of(X2,X1)
| min_precedes(sK16(sK18),X0,X1)
| min_precedes(X0,sK16(sK18),X1)
| ~ subactivity_occurrence(X0,X2)
| ~ subactivity_occurrence(sK16(sK18),X2) ),
inference(resolution,[],[f459,f187]) ).
fof(f480,plain,
( leaf_occ(sK16(sK18),sK18)
| ~ spl19_1 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f483,plain,
( subactivity_occurrence(sK16(sK18),sK18)
| ~ spl19_1 ),
inference(resolution,[],[f480,f198]) ).
fof(f630,plain,
! [X0,X1] :
( sK16(sK18) = sK15(sK18)
| ~ occurrence_of(X0,X1)
| min_precedes(sK16(sK18),sK15(sK18),X1)
| min_precedes(sK15(sK18),sK16(sK18),X1)
| ~ subactivity_occurrence(sK15(sK18),X0)
| ~ subactivity_occurrence(sK16(sK18),X0) ),
inference(resolution,[],[f461,f302]) ).
fof(f642,definition,
( spl19_35
<=> ! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ subactivity_occurrence(sK16(sK18),X0)
| ~ subactivity_occurrence(sK15(sK18),X0)
| min_precedes(sK15(sK18),sK16(sK18),X1)
| min_precedes(sK16(sK18),sK15(sK18),X1) ) ),
introduced(definition,[new_symbols(definition,[spl19_35])],[avatar_definition]) ).
fof(f643,plain,
( ! [X0,X1] :
( ~ subactivity_occurrence(sK16(sK18),X0)
| ~ occurrence_of(X0,X1)
| ~ subactivity_occurrence(sK15(sK18),X0)
| min_precedes(sK15(sK18),sK16(sK18),X1)
| min_precedes(sK16(sK18),sK15(sK18),X1) )
| ~ spl19_35 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f645,definition,
( spl19_36
<=> sK16(sK18) = sK15(sK18) ),
introduced(definition,[new_symbols(definition,[spl19_36])],[avatar_definition]) ).
fof(f646,plain,
( sK16(sK18) = sK15(sK18)
| ~ spl19_36 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f647,plain,
( spl19_35
| spl19_36 ),
inference(avatar_split_clause,[],[f630,f645,f642]) ).
fof(f652,plain,
( ! [X0] :
( ~ occurrence_of(sK18,X0)
| ~ subactivity_occurrence(sK15(sK18),sK18)
| min_precedes(sK15(sK18),sK16(sK18),X0)
| min_precedes(sK16(sK18),sK15(sK18),X0) )
| ~ spl19_1
| ~ spl19_35 ),
inference(resolution,[],[f643,f483]) ).
fof(f653,plain,
( ! [X0] :
( ~ occurrence_of(sK18,X0)
| min_precedes(sK15(sK18),sK16(sK18),X0)
| min_precedes(sK16(sK18),sK15(sK18),X0) )
| ~ spl19_1
| ~ spl19_11
| ~ spl19_35 ),
inference(forward_subsumption_resolution,[],[f652,f369]) ).
fof(f656,plain,
( min_precedes(sK15(sK18),sK16(sK18),tptp0)
| min_precedes(sK16(sK18),sK15(sK18),tptp0)
| ~ spl19_1
| ~ spl19_11
| ~ spl19_35 ),
inference(resolution,[],[f653,f221]) ).
fof(f663,plain,
( min_precedes(sK15(sK18),sK16(sK18),tptp0)
| ~ spl19_1
| ~ spl19_11
| ~ spl19_35 ),
inference(forward_subsumption_resolution,[],[f656,f269]) ).
fof(f672,plain,
( ~ leaf(sK15(sK18),tptp0)
| ~ spl19_1
| ~ spl19_11
| ~ spl19_35 ),
inference(resolution,[],[f663,f166]) ).
fof(f674,plain,
( $false
| ~ spl19_1
| ~ spl19_11
| ~ spl19_35 ),
inference(forward_subsumption_resolution,[],[f672,f380]) ).
fof(f675,plain,
( ~ spl19_1
| ~ spl19_11
| ~ spl19_35 ),
inference(avatar_contradiction_clause,[],[f674]) ).
fof(f691,plain,
( ! [X0] :
( ~ occurrence_of(sK17(sK15(sK18)),X0)
| tptp1 = X0 )
| ~ spl19_9 ),
inference(resolution,[],[f326,f139]) ).
fof(f719,plain,
( min_precedes(sK16(sK18),sK16(sK18),tptp0)
| ~ occurrence_of(sK18,tptp0)
| ~ spl19_36 ),
inference(superposition,[],[f270,f646]) ).
fof(f724,plain,
( ~ occurrence_of(sK18,tptp0)
| ~ spl19_36 ),
inference(forward_subsumption_resolution,[],[f719,f300]) ).
fof(f727,plain,
( $false
| ~ spl19_36 ),
inference(forward_subsumption_resolution,[],[f724,f221]) ).
fof(f728,plain,
~ spl19_36,
inference(avatar_contradiction_clause,[],[f727]) ).
fof(f737,plain,
( occurrence_of(sK9(tptp0,sK15(sK18),sK17(sK15(sK18))),tptp0)
| ~ spl19_7 ),
inference(resolution,[],[f383,f182]) ).
fof(f743,plain,
( occurrence_of(sK9(tptp0,sK15(sK18),sK17(sK15(sK18))),sK14(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))))
| ~ spl19_7 ),
inference(resolution,[],[f737,f226]) ).
fof(f750,plain,
( leaf_occ(sK17(sK15(sK18)),sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| ~ subactivity_occurrence(sK17(sK15(sK18)),sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| ~ spl19_7
| ~ spl19_13 ),
inference(resolution,[],[f737,f361]) ).
fof(f760,plain,
( ! [X0] :
( ~ occurrence_of(sK9(tptp0,sK15(sK18),sK17(sK15(sK18))),X0)
| tptp0 = X0 )
| ~ spl19_7 ),
inference(resolution,[],[f737,f139]) ).
fof(f780,definition,
( spl19_44
<=> subactivity_occurrence(sK17(sK15(sK18)),sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))) ),
introduced(definition,[new_symbols(definition,[spl19_44])],[avatar_definition]) ).
fof(f781,plain,
( ~ subactivity_occurrence(sK17(sK15(sK18)),sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| spl19_44 ),
inference(avatar_component_clause,[],[f780]) ).
fof(f783,definition,
( spl19_45
<=> leaf_occ(sK17(sK15(sK18)),sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))) ),
introduced(definition,[new_symbols(definition,[spl19_45])],[avatar_definition]) ).
fof(f784,plain,
( leaf_occ(sK17(sK15(sK18)),sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| ~ spl19_45 ),
inference(avatar_component_clause,[],[f783]) ).
fof(f785,plain,
( ~ spl19_44
| spl19_45
| ~ spl19_7
| ~ spl19_13 ),
inference(avatar_split_clause,[],[f750,f360,f318,f783,f780]) ).
fof(f795,plain,
( ~ min_precedes(sK15(sK18),sK17(sK15(sK18)),tptp0)
| spl19_44 ),
inference(resolution,[],[f781,f180]) ).
fof(f797,plain,
( $false
| ~ spl19_7
| spl19_44 ),
inference(forward_subsumption_resolution,[],[f795,f383]) ).
fof(f798,plain,
( ~ spl19_7
| spl19_44 ),
inference(avatar_contradiction_clause,[],[f797]) ).
fof(f804,plain,
( min_precedes(sK17(sK15(sK18)),sK17(sK17(sK15(sK18))),tptp0)
| ~ spl19_12 ),
inference(resolution,[],[f358,f171]) ).
fof(f808,plain,
( ~ leaf(sK17(sK15(sK18)),tptp0)
| ~ spl19_12 ),
inference(resolution,[],[f804,f166]) ).
fof(f821,plain,
( ! [X2,X0,X1] :
( ~ subactivity_occurrence(sK17(sK15(sK18)),X2)
| sK17(sK15(sK18)) = X0
| ~ occurrence_of(X2,X1)
| ~ arboreal(X0)
| min_precedes(X0,sK17(sK15(sK18)),X1)
| ~ subactivity_occurrence(X0,X2)
| min_precedes(sK17(sK15(sK18)),X0,X1) )
| ~ spl19_9 ),
inference(resolution,[],[f346,f187]) ).
fof(f824,plain,
( ! [X0] :
( root_occ(sK17(sK15(sK18)),X0)
| ~ subactivity_occurrence(sK17(sK15(sK18)),X0)
| ~ occurrence_of(X0,tptp0)
| leaf_occ(sK17(sK15(sK18)),X0) )
| ~ spl19_9 ),
inference(resolution,[],[f346,f218]) ).
fof(f875,plain,
( occurrence_of(sK9(tptp0,sK15(sK18),sK17(sK15(sK18))),sK14(sK17(sK15(sK18)),sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))))
| ~ spl19_45 ),
inference(resolution,[],[f784,f199]) ).
fof(f876,plain,
( subactivity_occurrence(sK17(sK15(sK18)),sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| ~ spl19_45 ),
inference(resolution,[],[f784,f198]) ).
fof(f942,plain,
( ! [X0] :
( ~ subactivity_occurrence(sK17(sK15(sK18)),X0)
| ~ occurrence_of(X0,tptp0)
| leaf_occ(sK17(sK15(sK18)),X0)
| root(sK17(sK15(sK18)),sK13(sK17(sK15(sK18)),X0)) )
| ~ spl19_9 ),
inference(resolution,[],[f824,f193]) ).
fof(f943,plain,
( ! [X0] :
( ~ subactivity_occurrence(sK17(sK15(sK18)),X0)
| ~ occurrence_of(X0,tptp0)
| leaf_occ(sK17(sK15(sK18)),X0)
| occurrence_of(X0,sK13(sK17(sK15(sK18)),X0)) )
| ~ spl19_9 ),
inference(resolution,[],[f824,f195]) ).
fof(f946,plain,
( tptp0 = sK14(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| ~ spl19_7 ),
inference(resolution,[],[f760,f743]) ).
fof(f958,plain,
( tptp0 = sK14(sK17(sK15(sK18)),sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| ~ spl19_7
| ~ spl19_45 ),
inference(resolution,[],[f875,f760]) ).
fof(f963,plain,
( leaf(sK17(sK15(sK18)),tptp0)
| ~ leaf_occ(sK17(sK15(sK18)),sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| ~ spl19_7
| ~ spl19_45 ),
inference(superposition,[],[f197,f958]) ).
fof(f964,plain,
( leaf(sK17(sK15(sK18)),tptp0)
| ~ spl19_7
| ~ spl19_45 ),
inference(forward_subsumption_resolution,[],[f963,f784]) ).
fof(f1146,plain,
( leaf(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),tptp0)
| ~ leaf_occ(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| ~ spl19_7 ),
inference(superposition,[],[f197,f946]) ).
fof(f1148,definition,
( spl19_84
<=> leaf_occ(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))) ),
introduced(definition,[new_symbols(definition,[spl19_84])],[avatar_definition]) ).
fof(f1149,plain,
( ~ leaf_occ(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| spl19_84 ),
inference(avatar_component_clause,[],[f1148]) ).
fof(f1151,definition,
( spl19_85
<=> leaf(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl19_85])],[avatar_definition]) ).
fof(f1152,plain,
( leaf(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),tptp0)
| ~ spl19_85 ),
inference(avatar_component_clause,[],[f1151]) ).
fof(f1153,plain,
( ~ spl19_84
| spl19_85
| ~ spl19_7 ),
inference(avatar_split_clause,[],[f1146,f318,f1151,f1148]) ).
fof(f1156,plain,
( ~ occurrence_of(sK9(tptp0,sK15(sK18),sK17(sK15(sK18))),tptp0)
| spl19_84 ),
inference(resolution,[],[f1149,f202]) ).
fof(f1158,plain,
( $false
| ~ spl19_7
| spl19_84 ),
inference(forward_subsumption_resolution,[],[f1156,f737]) ).
fof(f1159,plain,
( ~ spl19_7
| spl19_84 ),
inference(avatar_contradiction_clause,[],[f1158]) ).
fof(f2072,plain,
( ! [X0,X1] :
( ~ occurrence_of(sK9(X0,sK17(sK15(sK18)),X1),tptp0)
| leaf_occ(sK17(sK15(sK18)),sK9(X0,sK17(sK15(sK18)),X1))
| root(sK17(sK15(sK18)),sK13(sK17(sK15(sK18)),sK9(X0,sK17(sK15(sK18)),X1)))
| ~ min_precedes(sK17(sK15(sK18)),X1,X0) )
| ~ spl19_9 ),
inference(resolution,[],[f942,f181]) ).
fof(f2075,plain,
( ! [X0,X1] :
( ~ occurrence_of(sK9(X0,sK17(sK15(sK18)),X1),tptp0)
| leaf_occ(sK17(sK15(sK18)),sK9(X0,sK17(sK15(sK18)),X1))
| occurrence_of(sK9(X0,sK17(sK15(sK18)),X1),sK13(sK17(sK15(sK18)),sK9(X0,sK17(sK15(sK18)),X1)))
| ~ min_precedes(sK17(sK15(sK18)),X1,X0) )
| ~ spl19_9 ),
inference(resolution,[],[f943,f181]) ).
fof(f2119,plain,
( ! [X0,X1] :
( ~ occurrence_of(sK9(tptp0,sK15(sK18),sK17(sK15(sK18))),X1)
| sK17(sK15(sK18)) = X0
| ~ arboreal(X0)
| min_precedes(X0,sK17(sK15(sK18)),X1)
| ~ subactivity_occurrence(X0,sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| min_precedes(sK17(sK15(sK18)),X0,X1) )
| ~ spl19_9
| ~ spl19_45 ),
inference(resolution,[],[f876,f821]) ).
fof(f2543,plain,
( ! [X0] :
( ~ subactivity_occurrence(X0,sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| ~ arboreal(X0)
| min_precedes(X0,sK17(sK15(sK18)),tptp0)
| sK17(sK15(sK18)) = X0
| min_precedes(sK17(sK15(sK18)),X0,tptp0) )
| ~ spl19_7
| ~ spl19_9
| ~ spl19_45 ),
inference(resolution,[],[f2119,f737]) ).
fof(f2563,plain,
( ~ arboreal(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))))
| min_precedes(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),sK17(sK15(sK18)),tptp0)
| sK17(sK15(sK18)) = sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| min_precedes(sK17(sK15(sK18)),sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),tptp0)
| ~ occurrence_of(sK9(tptp0,sK15(sK18),sK17(sK15(sK18))),tptp0)
| ~ spl19_7
| ~ spl19_9
| ~ spl19_45 ),
inference(resolution,[],[f2543,f224]) ).
fof(f2570,plain,
( min_precedes(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),sK17(sK15(sK18)),tptp0)
| sK17(sK15(sK18)) = sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| min_precedes(sK17(sK15(sK18)),sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),tptp0)
| ~ occurrence_of(sK9(tptp0,sK15(sK18),sK17(sK15(sK18))),tptp0)
| ~ spl19_7
| ~ spl19_9
| ~ spl19_45 ),
inference(forward_subsumption_resolution,[],[f2563,f458]) ).
fof(f2577,definition,
( spl19_156
<=> sK17(sK15(sK18)) = sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))) ),
introduced(definition,[new_symbols(definition,[spl19_156])],[avatar_definition]) ).
fof(f2578,plain,
( sK17(sK15(sK18)) = sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| ~ spl19_156 ),
inference(avatar_component_clause,[],[f2577]) ).
fof(f2580,definition,
( spl19_157
<=> min_precedes(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),sK17(sK15(sK18)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl19_157])],[avatar_definition]) ).
fof(f2581,plain,
( min_precedes(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),sK17(sK15(sK18)),tptp0)
| ~ spl19_157 ),
inference(avatar_component_clause,[],[f2580]) ).
fof(f2620,plain,
( occurrence_of(sK17(sK15(sK18)),tptp2)
| occurrence_of(sK17(sK15(sK18)),tptp3)
| ~ occurrence_of(sK9(tptp0,sK15(sK18),sK17(sK15(sK18))),tptp0)
| ~ spl19_156 ),
inference(superposition,[],[f203,f2578]) ).
fof(f2623,plain,
( occurrence_of(sK17(sK15(sK18)),tptp2)
| occurrence_of(sK17(sK15(sK18)),tptp3)
| ~ spl19_7
| ~ spl19_156 ),
inference(forward_subsumption_resolution,[],[f2620,f737]) ).
fof(f2638,definition,
( spl19_158
<=> occurrence_of(sK17(sK15(sK18)),tptp3) ),
introduced(definition,[new_symbols(definition,[spl19_158])],[avatar_definition]) ).
fof(f2639,plain,
( occurrence_of(sK17(sK15(sK18)),tptp3)
| ~ spl19_158 ),
inference(avatar_component_clause,[],[f2638]) ).
fof(f2641,definition,
( spl19_159
<=> occurrence_of(sK17(sK15(sK18)),tptp2) ),
introduced(definition,[new_symbols(definition,[spl19_159])],[avatar_definition]) ).
fof(f2642,plain,
( occurrence_of(sK17(sK15(sK18)),tptp2)
| ~ spl19_159 ),
inference(avatar_component_clause,[],[f2641]) ).
fof(f2653,plain,
( ~ leaf(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),tptp0)
| ~ spl19_157 ),
inference(resolution,[],[f2581,f166]) ).
fof(f2667,plain,
( $false
| ~ spl19_85
| ~ spl19_157 ),
inference(forward_subsumption_resolution,[],[f2653,f1152]) ).
fof(f2668,plain,
( ~ spl19_85
| ~ spl19_157 ),
inference(avatar_contradiction_clause,[],[f2667]) ).
fof(f2673,plain,
( spl19_158
| spl19_159
| ~ spl19_7
| ~ spl19_156 ),
inference(avatar_split_clause,[],[f2623,f2577,f318,f2641,f2638]) ).
fof(f2688,plain,
( tptp3 = tptp1
| ~ spl19_9
| ~ spl19_158 ),
inference(resolution,[],[f2639,f691]) ).
fof(f2696,plain,
( $false
| ~ spl19_9
| ~ spl19_158 ),
inference(forward_subsumption_resolution,[],[f2688,f215]) ).
fof(f2697,plain,
( ~ spl19_9
| ~ spl19_158 ),
inference(avatar_contradiction_clause,[],[f2696]) ).
fof(f2704,plain,
( tptp2 = tptp1
| ~ spl19_9
| ~ spl19_159 ),
inference(resolution,[],[f2642,f691]) ).
fof(f2712,plain,
( $false
| ~ spl19_9
| ~ spl19_159 ),
inference(forward_subsumption_resolution,[],[f2704,f216]) ).
fof(f2713,plain,
( ~ spl19_9
| ~ spl19_159 ),
inference(avatar_contradiction_clause,[],[f2712]) ).
fof(f2776,plain,
( min_precedes(sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),sK17(sK15(sK18)),tptp0)
| sK17(sK15(sK18)) = sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18))))
| min_precedes(sK17(sK15(sK18)),sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),tptp0)
| ~ spl19_7
| ~ spl19_9
| ~ spl19_45 ),
inference(forward_subsumption_resolution,[],[f2570,f737]) ).
fof(f2785,definition,
( spl19_179
<=> min_precedes(sK17(sK15(sK18)),sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl19_179])],[avatar_definition]) ).
fof(f2786,plain,
( min_precedes(sK17(sK15(sK18)),sK16(sK9(tptp0,sK15(sK18),sK17(sK15(sK18)))),tptp0)
| ~ spl19_179 ),
inference(avatar_component_clause,[],[f2785]) ).
fof(f2787,plain,
( spl19_179
| spl19_156
| spl19_157
| ~ spl19_7
| ~ spl19_9
| ~ spl19_45 ),
inference(avatar_split_clause,[],[f2776,f783,f325,f318,f2580,f2577,f2785]) ).
fof(f2856,plain,
( ~ leaf(sK17(sK15(sK18)),tptp0)
| ~ spl19_179 ),
inference(resolution,[],[f2786,f166]) ).
fof(f2868,plain,
( $false
| ~ spl19_7
| ~ spl19_45
| ~ spl19_179 ),
inference(forward_subsumption_resolution,[],[f2856,f964]) ).
fof(f2869,plain,
( ~ spl19_7
| ~ spl19_45
| ~ spl19_179 ),
inference(avatar_contradiction_clause,[],[f2868]) ).
fof(f2880,plain,
( occurrence_of(sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))),tptp0)
| ~ spl19_12 ),
inference(resolution,[],[f804,f182]) ).
fof(f2922,plain,
( leaf_occ(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))))
| occurrence_of(sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))),sK13(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18))))))
| ~ min_precedes(sK17(sK15(sK18)),sK17(sK17(sK15(sK18))),tptp0)
| ~ spl19_9
| ~ spl19_12 ),
inference(resolution,[],[f2880,f2075]) ).
fof(f2923,plain,
( leaf_occ(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))))
| root(sK17(sK15(sK18)),sK13(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18))))))
| ~ min_precedes(sK17(sK15(sK18)),sK17(sK17(sK15(sK18))),tptp0)
| ~ spl19_9
| ~ spl19_12 ),
inference(resolution,[],[f2880,f2072]) ).
fof(f2949,plain,
( ! [X0] :
( ~ occurrence_of(sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))),X0)
| tptp0 = X0 )
| ~ spl19_12 ),
inference(resolution,[],[f2880,f139]) ).
fof(f2957,plain,
( leaf_occ(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))))
| root(sK17(sK15(sK18)),sK13(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18))))))
| ~ spl19_9
| ~ spl19_12 ),
inference(forward_subsumption_resolution,[],[f2923,f804]) ).
fof(f2958,plain,
( leaf_occ(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))))
| occurrence_of(sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))),sK13(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18))))))
| ~ spl19_9
| ~ spl19_12 ),
inference(forward_subsumption_resolution,[],[f2922,f804]) ).
fof(f2960,definition,
( spl19_184
<=> root(sK17(sK15(sK18)),sK13(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))))) ),
introduced(definition,[new_symbols(definition,[spl19_184])],[avatar_definition]) ).
fof(f2961,plain,
( root(sK17(sK15(sK18)),sK13(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18))))))
| ~ spl19_184 ),
inference(avatar_component_clause,[],[f2960]) ).
fof(f2963,definition,
( spl19_185
<=> leaf_occ(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18))))) ),
introduced(definition,[new_symbols(definition,[spl19_185])],[avatar_definition]) ).
fof(f2964,plain,
( leaf_occ(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))))
| ~ spl19_185 ),
inference(avatar_component_clause,[],[f2963]) ).
fof(f2965,plain,
( spl19_184
| spl19_185
| ~ spl19_9
| ~ spl19_12 ),
inference(avatar_split_clause,[],[f2957,f357,f325,f2963,f2960]) ).
fof(f2967,definition,
( spl19_186
<=> occurrence_of(sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))),sK13(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))))) ),
introduced(definition,[new_symbols(definition,[spl19_186])],[avatar_definition]) ).
fof(f2968,plain,
( occurrence_of(sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))),sK13(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18))))))
| ~ spl19_186 ),
inference(avatar_component_clause,[],[f2967]) ).
fof(f2969,plain,
( spl19_186
| spl19_185
| ~ spl19_9
| ~ spl19_12 ),
inference(avatar_split_clause,[],[f2958,f357,f325,f2963,f2967]) ).
fof(f3090,plain,
( tptp0 = sK13(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))))
| ~ spl19_12
| ~ spl19_186 ),
inference(resolution,[],[f2949,f2968]) ).
fof(f3093,plain,
( root(sK17(sK15(sK18)),tptp0)
| ~ spl19_12
| ~ spl19_184
| ~ spl19_186 ),
inference(superposition,[],[f2961,f3090]) ).
fof(f3094,plain,
( $false
| ~ spl19_7
| ~ spl19_12
| ~ spl19_184
| ~ spl19_186 ),
inference(unit_resulting_resolution,[],[f159,f383,f3093]) ).
fof(f3098,plain,
( ~ spl19_7
| ~ spl19_12
| ~ spl19_184
| ~ spl19_186 ),
inference(avatar_contradiction_clause,[],[f3094]) ).
fof(f3099,plain,
( occurrence_of(sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))),sK14(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18))))))
| ~ spl19_185 ),
inference(resolution,[],[f2964,f199]) ).
fof(f3111,plain,
( tptp0 = sK14(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))))
| ~ spl19_12
| ~ spl19_185 ),
inference(resolution,[],[f3099,f2949]) ).
fof(f3119,plain,
( leaf(sK17(sK15(sK18)),tptp0)
| ~ leaf_occ(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))))
| ~ spl19_12
| ~ spl19_185 ),
inference(superposition,[],[f197,f3111]) ).
fof(f3120,plain,
( ~ leaf_occ(sK17(sK15(sK18)),sK9(tptp0,sK17(sK15(sK18)),sK17(sK17(sK15(sK18)))))
| ~ spl19_12
| ~ spl19_185 ),
inference(forward_subsumption_resolution,[],[f3119,f808]) ).
fof(f3122,plain,
( $false
| ~ spl19_12
| ~ spl19_185 ),
inference(forward_subsumption_resolution,[],[f3120,f2964]) ).
fof(f3123,plain,
( ~ spl19_12
| ~ spl19_185 ),
inference(avatar_contradiction_clause,[],[f3122]) ).
cnf(s3,plain,
spl19_1,
inference(sat_conversion,[],[f246]) ).
cnf(s6,plain,
( spl19_7
| spl19_8 ),
inference(sat_conversion,[],[f323]) ).
cnf(s7,plain,
( spl19_8
| spl19_9 ),
inference(sat_conversion,[],[f327]) ).
cnf(s11,plain,
spl19_10,
inference(sat_conversion,[],[f345]) ).
cnf(s12,plain,
( ~ spl19_9
| spl19_12
| spl19_13 ),
inference(sat_conversion,[],[f362]) ).
cnf(s19,plain,
( ~ spl19_8
| ~ spl19_10
| spl19_11 ),
inference(sat_conversion,[],[f413]) ).
cnf(s36,plain,
( spl19_35
| spl19_36 ),
inference(sat_conversion,[],[f647]) ).
cnf(s38,plain,
( ~ spl19_1
| ~ spl19_11
| ~ spl19_35 ),
inference(sat_conversion,[],[f675]) ).
cnf(s44,plain,
~ spl19_36,
inference(sat_conversion,[],[f728]) ).
cnf(s50,plain,
( ~ spl19_7
| ~ spl19_13
| ~ spl19_44
| spl19_45 ),
inference(sat_conversion,[],[f785]) ).
cnf(s53,plain,
( ~ spl19_7
| spl19_44 ),
inference(sat_conversion,[],[f798]) ).
cnf(s79,plain,
( ~ spl19_7
| ~ spl19_84
| spl19_85 ),
inference(sat_conversion,[],[f1153]) ).
cnf(s81,plain,
( ~ spl19_7
| spl19_84 ),
inference(sat_conversion,[],[f1159]) ).
cnf(s173,plain,
( ~ spl19_85
| ~ spl19_157 ),
inference(sat_conversion,[],[f2668]) ).
cnf(s175,plain,
( ~ spl19_7
| ~ spl19_156
| spl19_158
| spl19_159 ),
inference(sat_conversion,[],[f2673]) ).
cnf(s179,plain,
( ~ spl19_9
| ~ spl19_158 ),
inference(sat_conversion,[],[f2697]) ).
cnf(s183,plain,
( ~ spl19_9
| ~ spl19_159 ),
inference(sat_conversion,[],[f2713]) ).
cnf(s196,plain,
( ~ spl19_7
| ~ spl19_9
| ~ spl19_45
| spl19_156
| spl19_157
| spl19_179 ),
inference(sat_conversion,[],[f2787]) ).
cnf(s200,plain,
( ~ spl19_7
| ~ spl19_45
| ~ spl19_179 ),
inference(sat_conversion,[],[f2869]) ).
cnf(s206,plain,
( ~ spl19_9
| ~ spl19_12
| spl19_184
| spl19_185 ),
inference(sat_conversion,[],[f2965]) ).
cnf(s207,plain,
( ~ spl19_9
| ~ spl19_12
| spl19_185
| spl19_186 ),
inference(sat_conversion,[],[f2969]) ).
cnf(s212,plain,
( ~ spl19_7
| ~ spl19_12
| ~ spl19_184
| ~ spl19_186 ),
inference(sat_conversion,[],[f3098]) ).
cnf(s213,plain,
( ~ spl19_12
| ~ spl19_185 ),
inference(sat_conversion,[],[f3123]) ).
cnf(s215,plain,
spl19_35,
inference(rat,[],[s36,s44]) ).
cnf(s224,plain,
~ spl19_11,
inference(rat,[],[s38,s215,s3]) ).
cnf(s226,plain,
~ spl19_8,
inference(rat,[],[s19,s11,s224]) ).
cnf(s228,plain,
spl19_9,
inference(rat,[],[s7,s226]) ).
cnf(s229,plain,
spl19_7,
inference(rat,[],[s6,s226]) ).
cnf(s231,plain,
~ spl19_159,
inference(rat,[],[s183,s228]) ).
cnf(s232,plain,
~ spl19_158,
inference(rat,[],[s179,s228]) ).
cnf(s233,plain,
~ spl19_156,
inference(rat,[],[s175,s231,s232,s229]) ).
cnf(s235,plain,
spl19_84,
inference(rat,[],[s81,s229]) ).
cnf(s237,plain,
spl19_44,
inference(rat,[],[s53,s229]) ).
cnf(s239,plain,
spl19_85,
inference(rat,[],[s79,s229,s235]) ).
cnf(s240,plain,
~ spl19_157,
inference(rat,[],[s173,s239]) ).
cnf(s244,plain,
~ spl19_45,
inference(rat,[],[s196,s200,s228,s229,s233,s240]) ).
cnf(s245,plain,
~ spl19_13,
inference(rat,[],[s50,s229,s237,s244]) ).
cnf(s247,plain,
spl19_12,
inference(rat,[],[s12,s228,s245]) ).
cnf(s250,plain,
~ spl19_185,
inference(rat,[],[s213,s247]) ).
cnf(s251,plain,
spl19_184,
inference(rat,[],[s206,s250,s228,s247]) ).
cnf(s254,plain,
spl19_186,
inference(rat,[],[s207,s250,s228,s247]) ).
cnf(s255,plain,
$false,
inference(rat,[],[s212,s247,s229,s254,s251]) ).
fof(f3125,plain,
$false,
inference(avatar_sat_refutation,[],[s255]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : PRO005+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.43 % Computer : n020.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sun Sep 27 22:17:20 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.48 Running first-order theorem proving
% 0.23/0.48 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.18/3.04 % (3818778)Detected formulas, will run a generic FOF schedule.
% 12.18/3.04 % (3818797)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2473119719:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.18/3.04 % (3818796)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1512832624:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.18/3.04 % (3818796)Refutation not found, incomplete strategy
% 12.18/3.04 % (3818796)------------------------------
% 12.18/3.04 % (3818796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/3.04 % (3818796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/3.04 % (3818796)CaDiCaL version: 2.1.3
% 12.18/3.04 % (3818796)Termination reason: Refutation not found, incomplete strategy
% 12.18/3.04 % (3818796)Time elapsed: 0.001 s
% 12.18/3.04 % (3818796)Peak memory usage: 87 MB
% 12.18/3.04 % (3818794)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=854042924:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.18/3.04 % (3818792)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=657628775:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.18/3.04 % (3818793)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=2833565108:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.18/3.04 % (3818795)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=794548455:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.18/3.04 % (3818795)Refutation not found, incomplete strategy
% 12.18/3.04 % (3818795)------------------------------
% 12.18/3.04 % (3818795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/3.04 % (3818795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/3.04 % (3818795)CaDiCaL version: 2.1.3
% 12.18/3.04 % (3818795)Termination reason: Refutation not found, incomplete strategy
% 12.18/3.04 % (3818795)Time elapsed: 0.001 s
% 12.18/3.04 % (3818795)Peak memory usage: 86 MB
% 12.18/3.04 % (3818798)dis-21_1_sil=8000:lcm=predicate:random_seed=1645497930: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)
% 12.18/3.04 % (3818797)Instruction limit reached!
% 12.18/3.04 % (3818797)------------------------------
% 12.18/3.04 % (3818797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/3.04 % (3818797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/3.04 % (3818797)CaDiCaL version: 2.1.3
% 12.18/3.04 % (3818797)Termination reason: Instruction limit
% 12.18/3.04 % (3818797)Termination phase: Saturation
% 12.18/3.04 % (3818797)Time elapsed: 0.080 s
% 12.18/3.04 % (3818797)Peak memory usage: 89 MB
% 12.18/3.04 % (3818797)Instructions burned: 139 (million)
% 12.18/3.04 % (3818798)Instruction limit reached!
% 12.18/3.04 % (3818798)------------------------------
% 12.18/3.04 % (3818798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/3.04 % (3818798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/3.04 % (3818798)CaDiCaL version: 2.1.3
% 12.18/3.04 % (3818798)Termination reason: Instruction limit
% 12.18/3.04 % (3818798)Termination phase: Saturation
% 12.18/3.04 % (3818798)Time elapsed: 0.131 s
% 12.18/3.04 % (3818798)Peak memory usage: 89 MB
% 12.18/3.04 % (3818798)Instructions burned: 129 (million)
% 12.18/3.04 % (3818806)lrs+10_1_sil=8000:sp=occurrence:random_seed=660490976:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.18/3.04 % (3818806)Instruction limit reached!
% 12.18/3.04 % (3818806)------------------------------
% 12.18/3.04 % (3818806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/3.04 % (3818806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/3.04 % (3818806)CaDiCaL version: 2.1.3
% 12.18/3.04 % (3818806)Termination reason: Instruction limit
% 12.18/3.04 % (3818806)Termination phase: Saturation
% 12.18/3.04 % (3818806)Time elapsed: 0.144 s
% 12.18/3.04 % (3818806)Peak memory usage: 92 MB
% 12.18/3.04 % (3818806)Instructions burned: 285 (million)
% 12.18/3.04 % (3818807)lrs+10_1_sil=32000:urr=on:br=off:random_seed=60797099:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 12.18/3.04 % (3818807)Refutation not found, incomplete strategy
% 12.18/3.04 % (3818807)------------------------------
% 12.18/3.04 % (3818807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/3.04 % (3818807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/3.04 % (3818807)CaDiCaL version: 2.1.3
% 12.18/3.04 % (3818807)Termination reason: Refutation not found, incomplete strategy
% 12.18/3.04 % (3818807)Time elapsed: 0.002 s
% 12.18/3.04 % (3818807)Peak memory usage: 88 MB
% 12.18/3.04 % (3818796)------------------------------
% 12.18/3.04 % (3818796)------------------------------
% 12.18/3.04 % (3818795)------------------------------
% 12.18/3.04 % (3818795)------------------------------
% 12.18/3.04 % (3818810)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3375160713:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 12.18/3.04 % (3818813)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=1214137087:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 12.18/3.04 % (3818814)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=462636612:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 12.18/3.04 % (3818814)Refutation not found, incomplete strategy
% 12.18/3.04 % (3818814)------------------------------
% 12.18/3.04 % (3818814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/3.04 % (3818814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/3.04 % (3818814)CaDiCaL version: 2.1.3
% 12.18/3.04 % (3818814)Termination reason: Refutation not found, incomplete strategy
% 12.18/3.04 % (3818814)Time elapsed: 0.006 s
% 12.18/3.04 % (3818814)Peak memory usage: 88 MB
% 12.18/3.04 % (3818814)Instructions burned: 3 (million)
% 12.18/3.04 % (3818810)Instruction limit reached!
% 12.18/3.04 % (3818810)------------------------------
% 12.18/3.04 % (3818810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/3.04 % (3818810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/3.04 % (3818810)CaDiCaL version: 2.1.3
% 12.18/3.04 % (3818810)Termination reason: Instruction limit
% 12.18/3.04 % (3818810)Termination phase: Saturation
% 12.18/3.04 % (3818810)Time elapsed: 0.169 s
% 12.18/3.04 % (3818810)Peak memory usage: 91 MB
% 12.18/3.04 % (3818810)Instructions burned: 327 (million)
% 12.18/3.04 % (3818807)------------------------------
% 12.18/3.04 % (3818807)------------------------------
% 12.18/3.04 % (3818819)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3836680830:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 12.18/3.04 % (3818813)Instruction limit reached!
% 12.18/3.04 % (3818813)------------------------------
% 12.18/3.04 % (3818813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/3.04 % (3818813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/3.04 % (3818813)CaDiCaL version: 2.1.3
% 12.18/3.04 % (3818813)Termination reason: Instruction limit
% 12.18/3.04 % (3818813)Termination phase: Saturation
% 12.18/3.04 % (3818813)Time elapsed: 0.228 s
% 12.18/3.04 % (3818813)Peak memory usage: 89 MB
% 12.18/3.04 % (3818813)Instructions burned: 248 (million)
% 12.18/3.04 % (3818820)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3633021241:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 12.18/3.04 % (3818814)------------------------------
% 12.18/3.04 % (3818814)------------------------------
% 12.18/3.04 % (3818822)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1862289421:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 12.18/3.04 % (3818820)Instruction limit reached!
% 12.18/3.04 % (3818820)------------------------------
% 12.18/3.04 % (3818820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/3.04 % (3818820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/3.04 % (3818820)CaDiCaL version: 2.1.3
% 12.18/3.04 % (3818820)Termination reason: Instruction limit
% 12.18/3.04 % (3818820)Termination phase: Saturation
% 12.18/3.04 % (3818820)Time elapsed: 0.135 s
% 12.18/3.04 % (3818820)Peak memory usage: 90 MB
% 12.18/3.04 % (3818820)Instructions burned: 113 (million)
% 12.18/3.04 % (3818822)Instruction limit reached!
% 12.18/3.04 % (3818822)------------------------------
% 12.18/3.04 % (3818822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/3.04 % (3818822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/3.04 % (3818822)CaDiCaL version: 2.1.3
% 12.18/3.04 % (3818822)Termination reason: Instruction limit
% 12.18/3.04 % (3818822)Termination phase: Saturation
% 12.18/3.04 % (3818822)Time elapsed: 0.117 s
% 12.18/3.04 % (3818822)Peak memory usage: 89 MB
% 12.18/3.04 % (3818822)Instructions burned: 127 (million)
% 12.18/3.04 % (3818824)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1525460113:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 12.18/3.04 % (3818824)Refutation not found, incomplete strategy
% 12.18/3.04 % (3818824)------------------------------
% 12.18/3.04 % (3818824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/3.04 % (3818824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/3.04 % (3818824)CaDiCaL version: 2.1.3
% 12.18/3.04 % (3818824)Termination reason: Refutation not found, incomplete strategy
% 12.18/3.04 % (3818824)Time elapsed: 0.001 s
% 12.18/3.04 % (3818824)Peak memory usage: 87 MB
% 12.18/3.04 % (3818793)First to succeed.
% 12.18/3.04 % (3818826)lrs+10_1_sil=8000:sp=occurrence:random_seed=1267851498:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 14.75/3.04 % (3818793)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3818778"
% 14.75/3.04 % (3818827)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3116097831:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 14.75/3.04 % (3818827)Refutation not found, incomplete strategy
% 14.75/3.04 % (3818827)------------------------------
% 14.75/3.04 % (3818827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.75/3.04 % (3818827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.75/3.04 % (3818827)CaDiCaL version: 2.1.3
% 14.75/3.04 % (3818827)Termination reason: Refutation not found, incomplete strategy
% 14.75/3.04 % (3818827)Time elapsed: 0.007 s
% 14.75/3.04 % (3818827)Peak memory usage: 88 MB
% 14.75/3.04 % (3818827)Instructions burned: 4 (million)
% 14.75/3.04 % (3818792)Also succeeded, but the first one will report.
% 14.75/3.04 % (3818824)------------------------------
% 14.75/3.04 % (3818824)------------------------------
% 14.75/3.04 % (3818819)Also succeeded, but the first one will report.
% 14.75/3.04 % (3818793)Refutation found. Thanks to Tanya!
% 14.75/3.04 % SZS status Theorem for theBenchmark
% 14.75/3.04 % SZS output start Proof for theBenchmark
% See solution above
% 15.01/3.35 % (3818793)------------------------------
% 15.01/3.35 % (3818793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.01/3.35 % (3818793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.01/3.35 % (3818793)CaDiCaL version: 2.1.3
% 15.01/3.35 % (3818793)Termination reason: Refutation
% 15.01/3.35 % (3818793)Time elapsed: 1.365 s
% 15.01/3.35 % (3818793)Peak memory usage: 133 MB
% 15.01/3.35 % (3818793)Instructions burned: 1400 (million)
% 15.01/3.35 % (3818793)------------------------------
% 15.01/3.35 % (3818793)------------------------------
% 15.01/3.35 % (3818778)Success in time 2.01 s
% 15.01/3.35 % Vampire exiting
%------------------------------------------------------------------------------