%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : PRO008+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n013.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 : Fri Sep 25 02:31:34 PM UTC 2026
% Result : Theorem 84.06s 12.43s
% Output : CNFRefutation 84.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 31
% Syntax : Number of formulae : 401 ( 52 unt; 1 def)
% Number of atoms : 1482 ( 175 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 1854 ( 822 ~; 864 |; 142 &)
% ( 9 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 19 usr; 3 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 6 con; 0-3 aty)
% Number of variables : 681 ( 0 sgn 635 !; 46 ?; 390 :)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& occurrence_of(X0,X1) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_02) ).
fof(f8,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_07) ).
fof(f9,axiom,
! [X0] :
( legal(X0)
=> arboreal(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_08) ).
fof(f11,axiom,
! [X0,X1] :
( precedes(X0,X1)
<=> ( legal(X1)
& earlier(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_10) ).
fof(f12,axiom,
! [X0,X1,X2] :
( min_precedes(X1,X2,X0)
=> ? [X3,X4] :
( atocc(X2,X4)
& atocc(X1,X3)
& subactivity(X4,X0)
& subactivity(X3,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_11) ).
fof(f15,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ~ root(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_14) ).
fof(f16,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> precedes(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_15) ).
fof(f17,axiom,
! [X0,X1] :
( root(X0,X1)
=> legal(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_16) ).
fof(f22,axiom,
! [X0,X1] :
( leaf(X0,X1)
<=> ( ~ ? [X3] : min_precedes(X0,X3,X1)
& ( ? [X2] : min_precedes(X2,X0,X1)
| root(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_21) ).
fof(f23,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( ~ ? [X3] :
( min_precedes(X3,X1,X2)
& min_precedes(X0,X3,X2) )
& min_precedes(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_22) ).
fof(f24,axiom,
! [X0,X1] :
( atocc(X0,X1)
<=> ? [X2] :
( occurrence_of(X0,X2)
& atomic(X2)
& subactivity(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_23) ).
fof(f29,axiom,
! [X0,X1,X2,X3] :
( ( subactivity_occurrence(X3,X1)
& subactivity_occurrence(X2,X1)
& arboreal(X3)
& arboreal(X2)
& occurrence_of(X1,X0) )
=> ( X2 = X3
| min_precedes(X3,X2,X0)
| min_precedes(X2,X3,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_28) ).
fof(f30,axiom,
! [X0,X1,X2,X3] :
( ( subactivity_occurrence(X1,X3)
& occurrence_of(X3,X2)
& min_precedes(X0,X1,X2) )
=> subactivity_occurrence(X0,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_29) ).
fof(f34,axiom,
! [X0,X1] :
( root_occ(X0,X1)
<=> ? [X2] :
( root(X0,X2)
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_33) ).
fof(f35,axiom,
! [X0,X1] :
( leaf_occ(X0,X1)
<=> ? [X2] :
( leaf(X0,X2)
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_34) ).
fof(f36,axiom,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2,X3] :
( leaf_occ(X3,X0)
& next_subocc(X2,X3,tptp0)
& ( occurrence_of(X3,tptp2)
| occurrence_of(X3,tptp1) )
& next_subocc(X1,X2,tptp0)
& occurrence_of(X2,tptp4)
& root_occ(X1,X0)
& occurrence_of(X1,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_35) ).
fof(f39,axiom,
atomic(tptp4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_38) ).
fof(f40,axiom,
atomic(tptp1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_39) ).
fof(f41,axiom,
atomic(tptp2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_40) ).
fof(f42,axiom,
atomic(tptp3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_41) ).
fof(f44,axiom,
tptp4 != tptp1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_43) ).
fof(f45,axiom,
tptp4 != tptp2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_44) ).
fof(f48,axiom,
tptp1 != tptp2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_47) ).
fof(f49,conjecture,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( ( occurrence_of(X2,tptp2)
=> ~ ? [X4] :
( min_precedes(X1,X4,tptp0)
& subactivity_occurrence(X4,X0)
& occurrence_of(X4,tptp1) ) )
& ( occurrence_of(X2,tptp1)
=> ~ ? [X3] :
( min_precedes(X1,X3,tptp0)
& subactivity_occurrence(X3,X0)
& occurrence_of(X3,tptp2) ) )
& leaf_occ(X2,X0)
& min_precedes(X1,X2,tptp0)
& ( occurrence_of(X2,tptp2)
| occurrence_of(X2,tptp1) )
& root_occ(X1,X0)
& occurrence_of(X1,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f50,negated_conjecture,
~ ! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( ( occurrence_of(X2,tptp2)
=> ~ ? [X4] :
( min_precedes(X1,X4,tptp0)
& subactivity_occurrence(X4,X0)
& occurrence_of(X4,tptp1) ) )
& ( occurrence_of(X2,tptp1)
=> ~ ? [X3] :
( min_precedes(X1,X3,tptp0)
& subactivity_occurrence(X3,X0)
& occurrence_of(X3,tptp2) ) )
& leaf_occ(X2,X0)
& min_precedes(X1,X2,tptp0)
& ( occurrence_of(X2,tptp2)
| occurrence_of(X2,tptp1) )
& root_occ(X1,X0)
& occurrence_of(X1,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f49]) ).
fof(f51,plain,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
=> ( ~ ? [X3] :
( min_precedes(X3,X1,X2)
& min_precedes(X0,X3,X2) )
& min_precedes(X0,X1,X2) ) ),
inference(unused_predicate_definition_removal,[],[f23]) ).
fof(f54,plain,
! [X0,X1,X2] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(ennf_transformation,[],[f3]) ).
fof(f55,plain,
! [X0,X1,X2] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(flattening,[],[f54]) ).
fof(f62,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ( arboreal(X0)
<=> atomic(X1) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f63,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f66,plain,
! [X0,X1,X2] :
( ~ min_precedes(X1,X2,X0)
| ? [X3,X4] :
( atocc(X2,X4)
& atocc(X1,X3)
& subactivity(X4,X0)
& subactivity(X3,X0) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f69,plain,
! [X0,X1,X2] :
( ~ min_precedes(X0,X1,X2)
| ~ root(X1,X2) ),
inference(ennf_transformation,[],[f15]) ).
fof(f70,plain,
! [X0,X1,X2] :
( ~ min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(ennf_transformation,[],[f16]) ).
fof(f71,plain,
! [X0,X1] :
( ~ root(X0,X1)
| legal(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f79,plain,
! [X0,X1] :
( leaf(X0,X1)
<=> ( ! [X3] : ~ min_precedes(X0,X3,X1)
& ( ? [X2] : min_precedes(X2,X0,X1)
| root(X0,X1) ) ) ),
inference(ennf_transformation,[],[f22]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ next_subocc(X0,X1,X2)
| ( ! [X3] :
( ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X3,X2) )
& min_precedes(X0,X1,X2) ) ),
inference(ennf_transformation,[],[f51]) ).
fof(f87,plain,
! [X0,X1,X2,X3] :
( ~ subactivity_occurrence(X3,X1)
| ~ subactivity_occurrence(X2,X1)
| ~ arboreal(X3)
| ~ arboreal(X2)
| ~ occurrence_of(X1,X0)
| X2 = X3
| min_precedes(X3,X2,X0)
| min_precedes(X2,X3,X0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f88,plain,
! [X0,X1,X2,X3] :
( ~ subactivity_occurrence(X3,X1)
| ~ subactivity_occurrence(X2,X1)
| ~ arboreal(X3)
| ~ arboreal(X2)
| ~ occurrence_of(X1,X0)
| X2 = X3
| min_precedes(X3,X2,X0)
| min_precedes(X2,X3,X0) ),
inference(flattening,[],[f87]) ).
fof(f89,plain,
! [X0,X1,X2,X3] :
( ~ subactivity_occurrence(X1,X3)
| ~ occurrence_of(X3,X2)
| ~ min_precedes(X0,X1,X2)
| subactivity_occurrence(X0,X3) ),
inference(ennf_transformation,[],[f30]) ).
fof(f90,plain,
! [X0,X1,X2,X3] :
( ~ subactivity_occurrence(X1,X3)
| ~ occurrence_of(X3,X2)
| ~ min_precedes(X0,X1,X2)
| subactivity_occurrence(X0,X3) ),
inference(flattening,[],[f89]) ).
fof(f97,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ? [X1,X2,X3] :
( leaf_occ(X3,X0)
& next_subocc(X2,X3,tptp0)
& ( occurrence_of(X3,tptp2)
| occurrence_of(X3,tptp1) )
& next_subocc(X1,X2,tptp0)
& occurrence_of(X2,tptp4)
& root_occ(X1,X0)
& occurrence_of(X1,tptp3) ) ),
inference(ennf_transformation,[],[f36]) ).
fof(f98,plain,
? [X0] :
( occurrence_of(X0,tptp0)
& ! [X1,X2] :
( ( occurrence_of(X2,tptp2)
& ? [X4] :
( min_precedes(X1,X4,tptp0)
& subactivity_occurrence(X4,X0)
& occurrence_of(X4,tptp1) ) )
| ( occurrence_of(X2,tptp1)
& ? [X3] :
( min_precedes(X1,X3,tptp0)
& subactivity_occurrence(X3,X0)
& occurrence_of(X3,tptp2) ) )
| ~ leaf_occ(X2,X0)
| ~ min_precedes(X1,X2,tptp0)
| ( ~ occurrence_of(X2,tptp2)
& ~ occurrence_of(X2,tptp1) )
| ~ root_occ(X1,X0)
| ~ occurrence_of(X1,tptp3) ) ),
inference(ennf_transformation,[],[f50]) ).
fof(f102,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ( ( ~ arboreal(X0)
| atomic(X1) )
& ( ~ atomic(X1)
| arboreal(X0) ) ) ),
inference(nnf_transformation,[],[f62]) ).
fof(f103,plain,
! [X0,X1] :
( ( ~ precedes(X0,X1)
| ( legal(X1)
& earlier(X0,X1) ) )
& ( ~ legal(X1)
| ~ earlier(X0,X1)
| precedes(X0,X1) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f104,plain,
! [X0,X1] :
( ( ~ precedes(X0,X1)
| ( legal(X1)
& earlier(X0,X1) ) )
& ( ~ legal(X1)
| ~ earlier(X0,X1)
| precedes(X0,X1) ) ),
inference(flattening,[],[f103]) ).
fof(f105,plain,
! [X0,X1,X2] :
( ~ min_precedes(X1,X2,X0)
| ( atocc(X2,sK3(X0,X1,X2))
& atocc(X1,sK2(X0,X1,X2))
& subactivity(sK3(X0,X1,X2),X0)
& subactivity(sK2(X0,X1,X2),X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X3,sK2(X0,X1,X2)),skolemize(X4,sK3(X0,X1,X2))],[f66]) ).
fof(f108,plain,
! [X0,X1] :
( ( ~ leaf(X0,X1)
| ( ! [X3] : ~ min_precedes(X0,X3,X1)
& ( ? [X2] : min_precedes(X2,X0,X1)
| root(X0,X1) ) ) )
& ( ? [X3] : min_precedes(X0,X3,X1)
| ( ! [X2] : ~ min_precedes(X2,X0,X1)
& ~ root(X0,X1) )
| leaf(X0,X1) ) ),
inference(nnf_transformation,[],[f79]) ).
fof(f109,plain,
! [X0,X1] :
( ( ~ leaf(X0,X1)
| ( ! [X3] : ~ min_precedes(X0,X3,X1)
& ( ? [X2] : min_precedes(X2,X0,X1)
| root(X0,X1) ) ) )
& ( ? [X3] : min_precedes(X0,X3,X1)
| ( ! [X2] : ~ min_precedes(X2,X0,X1)
& ~ root(X0,X1) )
| leaf(X0,X1) ) ),
inference(flattening,[],[f108]) ).
fof(f110,plain,
! [X0,X1] :
( ( ~ leaf(X0,X1)
| ( ! [X5] : ~ min_precedes(X0,X5,X1)
& ( ? [X4] : min_precedes(X4,X0,X1)
| root(X0,X1) ) ) )
& ( ? [X3] : min_precedes(X0,X3,X1)
| ( ! [X2] : ~ min_precedes(X2,X0,X1)
& ~ root(X0,X1) )
| leaf(X0,X1) ) ),
inference(rectify,[],[f109]) ).
fof(f111,plain,
! [X0,X1] :
( ( ~ leaf(X0,X1)
| ( ! [X5] : ~ min_precedes(X0,X5,X1)
& ( min_precedes(sK7(X0,X1),X0,X1)
| root(X0,X1) ) ) )
& ( min_precedes(X0,sK6(X0,X1),X1)
| ( ! [X2] : ~ min_precedes(X2,X0,X1)
& ~ root(X0,X1) )
| leaf(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X3,sK6(X0,X1)),skolemize(X4,sK7(X0,X1))],[f110]) ).
fof(f112,plain,
! [X0,X1] :
( ( ~ atocc(X0,X1)
| ? [X2] :
( occurrence_of(X0,X2)
& atomic(X2)
& subactivity(X1,X2) ) )
& ( ! [X2] :
( ~ occurrence_of(X0,X2)
| ~ atomic(X2)
| ~ subactivity(X1,X2) )
| atocc(X0,X1) ) ),
inference(nnf_transformation,[],[f24]) ).
fof(f113,plain,
! [X0,X1] :
( ( ~ atocc(X0,X1)
| ? [X3] :
( occurrence_of(X0,X3)
& atomic(X3)
& subactivity(X1,X3) ) )
& ( ! [X2] :
( ~ occurrence_of(X0,X2)
| ~ atomic(X2)
| ~ subactivity(X1,X2) )
| atocc(X0,X1) ) ),
inference(rectify,[],[f112]) ).
fof(f114,plain,
! [X0,X1] :
( ( ~ atocc(X0,X1)
| ( occurrence_of(X0,sK8(X0,X1))
& atomic(sK8(X0,X1))
& subactivity(X1,sK8(X0,X1)) ) )
& ( ! [X2] :
( ~ occurrence_of(X0,X2)
| ~ atomic(X2)
| ~ subactivity(X1,X2) )
| atocc(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X3,sK8(X0,X1))],[f113]) ).
fof(f119,plain,
! [X0,X1] :
( ( ~ root_occ(X0,X1)
| ? [X2] :
( root(X0,X2)
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,X2) ) )
& ( ! [X2] :
( ~ root(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2) )
| root_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f120,plain,
! [X0,X1] :
( ( ~ root_occ(X0,X1)
| ? [X3] :
( root(X0,X3)
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,X3) ) )
& ( ! [X2] :
( ~ root(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2) )
| root_occ(X0,X1) ) ),
inference(rectify,[],[f119]) ).
fof(f121,plain,
! [X0,X1] :
( ( ~ root_occ(X0,X1)
| ( root(X0,sK13(X0,X1))
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,sK13(X0,X1)) ) )
& ( ! [X2] :
( ~ root(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2) )
| root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X3,sK13(X0,X1))],[f120]) ).
fof(f122,plain,
! [X0,X1] :
( ( ~ leaf_occ(X0,X1)
| ? [X2] :
( leaf(X0,X2)
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,X2) ) )
& ( ! [X2] :
( ~ leaf(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2) )
| leaf_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f35]) ).
fof(f123,plain,
! [X0,X1] :
( ( ~ leaf_occ(X0,X1)
| ? [X3] :
( leaf(X0,X3)
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,X3) ) )
& ( ! [X2] :
( ~ leaf(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2) )
| leaf_occ(X0,X1) ) ),
inference(rectify,[],[f122]) ).
fof(f124,plain,
! [X0,X1] :
( ( ~ leaf_occ(X0,X1)
| ( leaf(X0,sK14(X0,X1))
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,sK14(X0,X1)) ) )
& ( ! [X2] :
( ~ leaf(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2) )
| leaf_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X3,sK14(X0,X1))],[f123]) ).
fof(f125,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ( leaf_occ(sK17(X0),X0)
& next_subocc(sK16(X0),sK17(X0),tptp0)
& ( occurrence_of(sK17(X0),tptp2)
| occurrence_of(sK17(X0),tptp1) )
& next_subocc(sK15(X0),sK16(X0),tptp0)
& occurrence_of(sK16(X0),tptp4)
& root_occ(sK15(X0),X0)
& occurrence_of(sK15(X0),tptp3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16,sK17]),skolemize(X1,sK15(X0)),skolemize(X2,sK16(X0)),skolemize(X3,sK17(X0))],[f97]) ).
fof(f129,plain,
( occurrence_of(sK19,tptp0)
& ! [X1,X2] :
( sP0(sK19,X1,X2)
| ( occurrence_of(X2,tptp1)
& min_precedes(X1,sK20(X1),tptp0)
& subactivity_occurrence(sK20(X1),sK19)
& occurrence_of(sK20(X1),tptp2) )
| ~ leaf_occ(X2,sK19)
| ~ min_precedes(X1,X2,tptp0)
| ( ~ occurrence_of(X2,tptp2)
& ~ occurrence_of(X2,tptp1) )
| ~ root_occ(X1,sK19)
| ~ occurrence_of(X1,tptp3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19,sK20]),skolemize(X0,sK19),skolemize(X3,sK20(X1))],[f100]) ).
fof(f134,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f55]) ).
fof(f140,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f141,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f143,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| legal(X1) ),
inference(cnf_transformation,[],[f104]) ).
fof(f147,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| atocc(X1,sK2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f105]) ).
fof(f154,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| ~ root(X1,X2) ),
inference(cnf_transformation,[],[f69]) ).
fof(f155,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(cnf_transformation,[],[f70]) ).
fof(f156,plain,
! [X0,X1] :
( ~ root(X0,X1)
| legal(X0) ),
inference(cnf_transformation,[],[f71]) ).
fof(f161,plain,
! [X0,X1,X5] :
( ~ leaf(X0,X1)
| ~ min_precedes(X0,X5,X1) ),
inference(cnf_transformation,[],[f111]) ).
fof(f165,plain,
! [X2,X3,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X3,X2) ),
inference(cnf_transformation,[],[f80]) ).
fof(f166,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f80]) ).
fof(f167,plain,
! [X0,X1] :
( ~ atocc(X0,X1)
| occurrence_of(X0,sK8(X0,X1)) ),
inference(cnf_transformation,[],[f114]) ).
fof(f168,plain,
! [X0,X1] :
( ~ atocc(X0,X1)
| atomic(sK8(X0,X1)) ),
inference(cnf_transformation,[],[f114]) ).
fof(f180,plain,
! [X2,X3,X0,X1] :
( ~ subactivity_occurrence(X3,X1)
| ~ subactivity_occurrence(X2,X1)
| ~ arboreal(X3)
| ~ arboreal(X2)
| ~ occurrence_of(X1,X0)
| X2 = X3
| min_precedes(X3,X2,X0)
| min_precedes(X2,X3,X0) ),
inference(cnf_transformation,[],[f88]) ).
fof(f181,plain,
! [X2,X3,X0,X1] :
( ~ subactivity_occurrence(X1,X3)
| ~ occurrence_of(X3,X2)
| ~ min_precedes(X0,X1,X2)
| subactivity_occurrence(X0,X3) ),
inference(cnf_transformation,[],[f90]) ).
fof(f186,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| root(X0,sK13(X0,X1)) ),
inference(cnf_transformation,[],[f121]) ).
fof(f187,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f121]) ).
fof(f188,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| occurrence_of(X1,sK13(X0,X1)) ),
inference(cnf_transformation,[],[f121]) ).
fof(f189,plain,
! [X2,X0,X1] :
( ~ root(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2)
| root_occ(X0,X1) ),
inference(cnf_transformation,[],[f121]) ).
fof(f190,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| leaf(X0,sK14(X0,X1)) ),
inference(cnf_transformation,[],[f124]) ).
fof(f191,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f124]) ).
fof(f192,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| occurrence_of(X1,sK14(X0,X1)) ),
inference(cnf_transformation,[],[f124]) ).
fof(f193,plain,
! [X2,X0,X1] :
( ~ leaf(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f124]) ).
fof(f194,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| leaf_occ(sK17(X0),X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f195,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| next_subocc(sK16(X0),sK17(X0),tptp0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f196,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| occurrence_of(sK17(X0),tptp2)
| occurrence_of(sK17(X0),tptp1) ),
inference(cnf_transformation,[],[f125]) ).
fof(f197,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| next_subocc(sK15(X0),sK16(X0),tptp0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f198,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| occurrence_of(sK16(X0),tptp4) ),
inference(cnf_transformation,[],[f125]) ).
fof(f199,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| root_occ(sK15(X0),X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f200,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| occurrence_of(sK15(X0),tptp3) ),
inference(cnf_transformation,[],[f125]) ).
fof(f203,plain,
atomic(tptp4),
inference(cnf_transformation,[],[f39]) ).
fof(f204,plain,
atomic(tptp1),
inference(cnf_transformation,[],[f40]) ).
fof(f205,plain,
atomic(tptp2),
inference(cnf_transformation,[],[f41]) ).
fof(f206,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f42]) ).
fof(f208,plain,
tptp4 != tptp1,
inference(cnf_transformation,[],[f44]) ).
fof(f209,plain,
tptp4 != tptp2,
inference(cnf_transformation,[],[f45]) ).
fof(f212,plain,
tptp1 != tptp2,
inference(cnf_transformation,[],[f48]) ).
fof(f217,plain,
occurrence_of(sK19,tptp0),
inference(cnf_transformation,[],[f129]) ).
fof(f218,plain,
! [X2,X1] :
( sP0(sK19,X1,X2)
| occurrence_of(X2,tptp1)
| ~ leaf_occ(X2,sK19)
| ~ min_precedes(X1,X2,tptp0)
| ~ occurrence_of(X2,tptp2)
| ~ root_occ(X1,sK19)
| ~ occurrence_of(X1,tptp3) ),
inference(cnf_transformation,[],[f129]) ).
fof(f223,plain,
! [X2,X1] :
( sP0(sK19,X1,X2)
| min_precedes(X1,sK20(X1),tptp0)
| ~ leaf_occ(X2,sK19)
| ~ min_precedes(X1,X2,tptp0)
| ~ occurrence_of(X2,tptp1)
| ~ root_occ(X1,sK19)
| ~ occurrence_of(X1,tptp3) ),
inference(cnf_transformation,[],[f129]) ).
fof(f224,plain,
! [X2,X1] :
( sP0(sK19,X1,X2)
| subactivity_occurrence(sK20(X1),sK19)
| ~ leaf_occ(X2,sK19)
| ~ min_precedes(X1,X2,tptp0)
| ~ occurrence_of(X2,tptp1)
| ~ root_occ(X1,sK19)
| ~ occurrence_of(X1,tptp3) ),
inference(cnf_transformation,[],[f129]) ).
fof(f225,plain,
! [X2,X1] :
( sP0(sK19,X1,X2)
| occurrence_of(sK20(X1),tptp2)
| ~ leaf_occ(X2,sK19)
| ~ min_precedes(X1,X2,tptp0)
| ~ occurrence_of(X2,tptp1)
| ~ root_occ(X1,sK19)
| ~ occurrence_of(X1,tptp3) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( arboreal(X0)
| ~ atomic(X1)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_60,plain,
! [X0: $i] :
( arboreal(X0)
| ~ legal(X0) ),
inference(cnf_transformation,[],[f141]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] :
( legal(X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[],[f143]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i] :
( atocc(X0,sK2(X2,X0,X1))
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f147]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f154]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i,X2: $i] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f155]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] :
( legal(X0)
| ~ root(X0,X1) ),
inference(cnf_transformation,[],[f156]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ leaf(X0,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f161]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i,X2: $i] :
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[],[f166]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ next_subocc(X0,X3,X2)
| ~ min_precedes(X1,X3,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f165]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] :
( atomic(sK8(X0,X1))
| ~ atocc(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( occurrence_of(X0,sK8(X0,X1))
| ~ atocc(X0,X1) ),
inference(cnf_transformation,[],[f167]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( min_precedes(X3,X2,X1)
| min_precedes(X2,X3,X1)
| ( X2 = X3 )
| ~ arboreal(X3)
| ~ arboreal(X2)
| ~ subactivity_occurrence(X3,X0)
| ~ subactivity_occurrence(X2,X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( subactivity_occurrence(X0,X3)
| ~ subactivity_occurrence(X1,X3)
| ~ occurrence_of(X3,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f181]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] :
( root_occ(X2,X0)
| ~ subactivity_occurrence(X2,X0)
| ~ root(X2,X1)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[],[f189]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i] :
( occurrence_of(X1,sK13(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i] :
( subactivity_occurrence(X0,X1)
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f187]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i] :
( root(X0,sK13(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f186]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i] :
( leaf_occ(X2,X0)
| ~ subactivity_occurrence(X2,X0)
| ~ leaf(X2,X1)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[],[f193]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i] :
( occurrence_of(X1,sK14(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f192]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i] :
( subactivity_occurrence(X0,X1)
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f191]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i] :
( leaf(X0,sK14(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f190]) ).
tcf(c_113,plain,
! [X0: $i] :
( occurrence_of(sK15(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_114,plain,
! [X0: $i] :
( root_occ(sK15(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f199]) ).
tcf(c_115,plain,
! [X0: $i] :
( occurrence_of(sK16(X0),tptp4)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f198]) ).
tcf(c_116,plain,
! [X0: $i] :
( next_subocc(sK15(X0),sK16(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f197]) ).
tcf(c_117,plain,
! [X0: $i] :
( occurrence_of(sK17(X0),tptp2)
| occurrence_of(sK17(X0),tptp1)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f196]) ).
tcf(c_118,plain,
! [X0: $i] :
( next_subocc(sK16(X0),sK17(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f195]) ).
tcf(c_119,plain,
! [X0: $i] :
( leaf_occ(sK17(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f194]) ).
tcf(c_122,plain,
atomic(tptp4),
inference(cnf_transformation,[],[f203]) ).
tcf(c_123,plain,
atomic(tptp1),
inference(cnf_transformation,[],[f204]) ).
tcf(c_124,plain,
atomic(tptp2),
inference(cnf_transformation,[],[f205]) ).
tcf(c_125,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f206]) ).
tcf(c_127,plain,
tptp4 != tptp1,
inference(cnf_transformation,[],[f208]) ).
tcf(c_128,plain,
tptp4 != tptp2,
inference(cnf_transformation,[],[f209]) ).
tcf(c_131,plain,
tptp1 != tptp2,
inference(cnf_transformation,[],[f212]) ).
tcf(c_136,negated_conjecture,
! [X0: $i,X1: $i] :
( occurrence_of(sK20(X0),tptp2)
| sP0(sK19,X0,X1)
| ~ leaf_occ(X1,sK19)
| ~ root_occ(X0,sK19)
| ~ occurrence_of(X1,tptp1)
| ~ occurrence_of(X0,tptp3)
| ~ min_precedes(X0,X1,tptp0) ),
inference(cnf_transformation,[],[f225]) ).
tcf(c_137,negated_conjecture,
! [X0: $i,X1: $i] :
( subactivity_occurrence(sK20(X0),sK19)
| sP0(sK19,X0,X1)
| ~ leaf_occ(X1,sK19)
| ~ root_occ(X0,sK19)
| ~ occurrence_of(X1,tptp1)
| ~ occurrence_of(X0,tptp3)
| ~ min_precedes(X0,X1,tptp0) ),
inference(cnf_transformation,[],[f224]) ).
tcf(c_138,negated_conjecture,
! [X0: $i,X1: $i] :
( sP0(sK19,X0,X1)
| min_precedes(X0,sK20(X0),tptp0)
| ~ leaf_occ(X1,sK19)
| ~ root_occ(X0,sK19)
| ~ occurrence_of(X1,tptp1)
| ~ occurrence_of(X0,tptp3)
| ~ min_precedes(X0,X1,tptp0) ),
inference(cnf_transformation,[],[f223]) ).
tcf(c_142,negated_conjecture,
! [X0: $i,X1: $i] :
( occurrence_of(X1,tptp1)
| sP0(sK19,X0,X1)
| ~ leaf_occ(X1,sK19)
| ~ root_occ(X0,sK19)
| ~ occurrence_of(X1,tptp2)
| ~ occurrence_of(X0,tptp3)
| ~ min_precedes(X0,X1,tptp0) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_143,negated_conjecture,
occurrence_of(sK19,tptp0),
inference(cnf_transformation,[],[f217]) ).
tcf(c_157,plain,
( leaf_occ(sK17(sK19),sK19)
| ~ occurrence_of(sK19,tptp0) ),
inference(instantiation,[status(thm)],[c_119]) ).
tcf(c_158,plain,
( occurrence_of(sK16(sK19),tptp4)
| ~ occurrence_of(sK19,tptp0) ),
inference(instantiation,[status(thm)],[c_115]) ).
tcf(c_159,plain,
( root_occ(sK15(sK19),sK19)
| ~ occurrence_of(sK19,tptp0) ),
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_160,plain,
( occurrence_of(sK15(sK19),tptp3)
| ~ occurrence_of(sK19,tptp0) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_196,plain,
( occurrence_of(sK17(sK19),tptp2)
| occurrence_of(sK17(sK19),tptp1)
| ~ occurrence_of(sK19,tptp0) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_1277,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( min_precedes(X1,X2,X3)
| ~ occurrence_of(X0,tptp0)
| ( X3 != tptp0 )
| ( sK17(X0) != X2 )
| ( sK16(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_84,c_118]) ).
tcf(c_1278,plain,
! [X0: $i] :
( min_precedes(sK16(X0),sK17(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(unflattening,[status(thm)],[c_1277]) ).
tcf(c_1286,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ occurrence_of(X0,tptp0)
| ~ min_precedes(X4,X3,X2)
| ~ min_precedes(X1,X4,X2)
| ( X2 != tptp0 )
| ( sK16(X0) != X3 )
| ( sK15(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_85,c_116]) ).
tcf(c_1287,plain,
! [X0: $i,X1: $i] :
( ~ occurrence_of(X0,tptp0)
| ~ min_precedes(X1,sK16(X0),tptp0)
| ~ min_precedes(sK15(X0),X1,tptp0) ),
inference(unflattening,[status(thm)],[c_1286]) ).
tcf(c_1298,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ occurrence_of(X0,tptp0)
| ~ min_precedes(X4,X3,X2)
| ~ min_precedes(X1,X4,X2)
| ( X2 != tptp0 )
| ( sK17(X0) != X3 )
| ( sK16(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_85,c_118]) ).
tcf(c_1299,plain,
! [X0: $i,X1: $i] :
( ~ occurrence_of(X0,tptp0)
| ~ min_precedes(X1,sK17(X0),tptp0)
| ~ min_precedes(sK16(X0),X1,tptp0) ),
inference(unflattening,[status(thm)],[c_1298]) ).
tcf(c_3500,plain,
! [X0: $i,X1: $i,X2: $i] :
( root(X1,sK13(X1,X2))
| ~ occurrence_of(X0,tptp0)
| ( X0 != X2 )
| ( sK15(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_108,c_114]) ).
tcf(c_3501,plain,
! [X0: $i] :
( root(sK15(X0),sK13(sK15(X0),X0))
| ~ occurrence_of(X0,tptp0) ),
inference(unflattening,[status(thm)],[c_3500]) ).
tcf(c_3502,plain,
( root(sK15(sK19),sK13(sK15(sK19),sK19))
| ~ occurrence_of(sK19,tptp0) ),
inference(instantiation,[status(thm)],[c_3501]) ).
tcf(c_3509,plain,
! [X0: $i,X1: $i,X2: $i] :
( subactivity_occurrence(X1,X2)
| ~ occurrence_of(X0,tptp0)
| ( X0 != X2 )
| ( sK15(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_107,c_114]) ).
tcf(c_3510,plain,
! [X0: $i] :
( subactivity_occurrence(sK15(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(unflattening,[status(thm)],[c_3509]) ).
tcf(c_3511,plain,
( subactivity_occurrence(sK15(sK19),sK19)
| ~ occurrence_of(sK19,tptp0) ),
inference(instantiation,[status(thm)],[c_3510]) ).
tcf(c_3518,plain,
! [X0: $i,X1: $i,X2: $i] :
( occurrence_of(X2,sK13(X1,X2))
| ~ occurrence_of(X0,tptp0)
| ( X0 != X2 )
| ( sK15(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_106,c_114]) ).
tcf(c_3519,plain,
! [X0: $i] :
( occurrence_of(X0,sK13(sK15(X0),X0))
| ~ occurrence_of(X0,tptp0) ),
inference(unflattening,[status(thm)],[c_3518]) ).
tcf(c_3520,plain,
( occurrence_of(sK19,sK13(sK15(sK19),sK19))
| ~ occurrence_of(sK19,tptp0) ),
inference(instantiation,[status(thm)],[c_3519]) ).
tcf(c_4028,plain,
! [X0: $i,X1: $i,X2: $i] :
( leaf(X1,sK14(X1,X2))
| ~ occurrence_of(X0,tptp0)
| ( X0 != X2 )
| ( sK17(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_112,c_119]) ).
tcf(c_4029,plain,
! [X0: $i] :
( leaf(sK17(X0),sK14(sK17(X0),X0))
| ~ occurrence_of(X0,tptp0) ),
inference(unflattening,[status(thm)],[c_4028]) ).
tcf(c_4030,plain,
( leaf(sK17(sK19),sK14(sK17(sK19),sK19))
| ~ occurrence_of(sK19,tptp0) ),
inference(instantiation,[status(thm)],[c_4029]) ).
tcf(c_4037,plain,
! [X0: $i,X1: $i,X2: $i] :
( subactivity_occurrence(X1,X2)
| ~ occurrence_of(X0,tptp0)
| ( X0 != X2 )
| ( sK17(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_111,c_119]) ).
tcf(c_4038,plain,
! [X0: $i] :
( subactivity_occurrence(sK17(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(unflattening,[status(thm)],[c_4037]) ).
tcf(c_4039,plain,
( subactivity_occurrence(sK17(sK19),sK19)
| ~ occurrence_of(sK19,tptp0) ),
inference(instantiation,[status(thm)],[c_4038]) ).
tcf(c_4046,plain,
! [X0: $i,X1: $i,X2: $i] :
( occurrence_of(X2,sK14(X1,X2))
| ~ occurrence_of(X0,tptp0)
| ( X0 != X2 )
| ( sK17(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_110,c_119]) ).
tcf(c_4047,plain,
! [X0: $i] :
( occurrence_of(X0,sK14(sK17(X0),X0))
| ~ occurrence_of(X0,tptp0) ),
inference(unflattening,[status(thm)],[c_4046]) ).
tcf(c_4048,plain,
( occurrence_of(sK19,sK14(sK17(sK19),sK19))
| ~ occurrence_of(sK19,tptp0) ),
inference(instantiation,[status(thm)],[c_4047]) ).
tcf(c_5270,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( ~ occurrence_of(X0_iProver_min_precedes_1,tptp0)
| ~ min_precedes(X1_iProver_min_precedes_1,sK17(X0_iProver_min_precedes_1),tptp0)
| ~ min_precedes(sK16(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1,tptp0) ),
inference(subtyping,[status(esa)],[c_1299]) ).
tcf(c_5271,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( ~ occurrence_of(X0_iProver_min_precedes_1,tptp0)
| ~ min_precedes(X1_iProver_min_precedes_1,sK16(X0_iProver_min_precedes_1),tptp0)
| ~ min_precedes(sK15(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1,tptp0) ),
inference(subtyping,[status(esa)],[c_1287]) ).
tcf(c_5272,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( min_precedes(sK16(X0_iProver_min_precedes_1),sK17(X0_iProver_min_precedes_1),tptp0)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(subtyping,[status(esa)],[c_1278]) ).
tcf(c_5274,negated_conjecture,
occurrence_of(sK19,tptp0),
inference(subtyping,[status(esa)],[c_143]) ).
tcf(c_5275,negated_conjecture,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X1_iProver_min_precedes_1,tptp1)
| sP0(sK19,X0_iProver_min_precedes_1,X1_iProver_min_precedes_1)
| ~ leaf_occ(X1_iProver_min_precedes_1,sK19)
| ~ root_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X1_iProver_min_precedes_1,tptp2)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp3)
| ~ min_precedes(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,tptp0) ),
inference(subtyping,[status(esa)],[c_142]) ).
tcf(c_5279,negated_conjecture,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( sP0(sK19,X0_iProver_min_precedes_1,X1_iProver_min_precedes_1)
| min_precedes(X0_iProver_min_precedes_1,sK20(X0_iProver_min_precedes_1),tptp0)
| ~ leaf_occ(X1_iProver_min_precedes_1,sK19)
| ~ root_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X1_iProver_min_precedes_1,tptp1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp3)
| ~ min_precedes(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,tptp0) ),
inference(subtyping,[status(esa)],[c_138]) ).
tcf(c_5280,negated_conjecture,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( subactivity_occurrence(sK20(X0_iProver_min_precedes_1),sK19)
| sP0(sK19,X0_iProver_min_precedes_1,X1_iProver_min_precedes_1)
| ~ leaf_occ(X1_iProver_min_precedes_1,sK19)
| ~ root_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X1_iProver_min_precedes_1,tptp1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp3)
| ~ min_precedes(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,tptp0) ),
inference(subtyping,[status(esa)],[c_137]) ).
tcf(c_5281,negated_conjecture,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(sK20(X0_iProver_min_precedes_1),tptp2)
| sP0(sK19,X0_iProver_min_precedes_1,X1_iProver_min_precedes_1)
| ~ leaf_occ(X1_iProver_min_precedes_1,sK19)
| ~ root_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X1_iProver_min_precedes_1,tptp1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp3)
| ~ min_precedes(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,tptp0) ),
inference(subtyping,[status(esa)],[c_136]) ).
tcf(c_5286,plain,
tptp1 != tptp2,
inference(subtyping,[status(esa)],[c_131]) ).
tcf(c_5289,plain,
tptp4 != tptp2,
inference(subtyping,[status(esa)],[c_128]) ).
tcf(c_5290,plain,
tptp4 != tptp1,
inference(subtyping,[status(esa)],[c_127]) ).
tcf(c_5294,plain,
atomic(tptp1),
inference(subtyping,[status(esa)],[c_123]) ).
tcf(c_5295,plain,
atomic(tptp4),
inference(subtyping,[status(esa)],[c_122]) ).
tcf(c_5298,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( leaf_occ(sK17(X0_iProver_min_precedes_1),X0_iProver_min_precedes_1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(subtyping,[status(esa)],[c_119]) ).
tcf(c_5299,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(sK17(X0_iProver_min_precedes_1),tptp2)
| occurrence_of(sK17(X0_iProver_min_precedes_1),tptp1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(subtyping,[status(esa)],[c_117]) ).
tcf(c_5300,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(sK16(X0_iProver_min_precedes_1),tptp4)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(subtyping,[status(esa)],[c_115]) ).
tcf(c_5301,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( root_occ(sK15(X0_iProver_min_precedes_1),X0_iProver_min_precedes_1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(subtyping,[status(esa)],[c_114]) ).
tcf(c_5302,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(sK15(X0_iProver_min_precedes_1),tptp3)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(subtyping,[status(esa)],[c_113]) ).
tcf(c_5304,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( subactivity_occurrence(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1)
| ~ leaf_occ(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1) ),
inference(subtyping,[status(esa)],[c_111]) ).
tcf(c_5306,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( leaf_occ(X1_iProver_min_precedes_1,X0_iProver_min_precedes_1)
| ~ subactivity_occurrence(X1_iProver_min_precedes_1,X0_iProver_min_precedes_1)
| ~ leaf(X1_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ occurrence_of(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(subtyping,[status(esa)],[c_109]) ).
tcf(c_5307,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( root(X0_iProver_min_precedes_1,sK13(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1))
| ~ root_occ(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1) ),
inference(subtyping,[status(esa)],[c_108]) ).
tcf(c_5308,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( subactivity_occurrence(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1)
| ~ root_occ(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1) ),
inference(subtyping,[status(esa)],[c_107]) ).
tcf(c_5309,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X1_iProver_min_precedes_1,sK13(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1))
| ~ root_occ(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1) ),
inference(subtyping,[status(esa)],[c_106]) ).
tcf(c_5310,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( root_occ(X1_iProver_min_precedes_1,X0_iProver_min_precedes_1)
| ~ subactivity_occurrence(X1_iProver_min_precedes_1,X0_iProver_min_precedes_1)
| ~ root(X1_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ occurrence_of(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(subtyping,[status(esa)],[c_105]) ).
tcf(c_5315,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1,X2_iProver_min_precedes_1: iProver_min_precedes_1] :
( subactivity_occurrence(X0_iProver_min_precedes_1,X2_iProver_min_precedes_1)
| ~ subactivity_occurrence(X1_iProver_min_precedes_1,X2_iProver_min_precedes_1)
| ~ occurrence_of(X2_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ min_precedes(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(subtyping,[status(esa)],[c_100]) ).
tcf(c_5316,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1,X2_iProver_min_precedes_1: iProver_min_precedes_1] :
( min_precedes(X2_iProver_min_precedes_1,X1_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| min_precedes(X1_iProver_min_precedes_1,X2_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ( X1_iProver_min_precedes_1 = X2_iProver_min_precedes_1 )
| ~ arboreal(X2_iProver_min_precedes_1)
| ~ arboreal(X1_iProver_min_precedes_1)
| ~ subactivity_occurrence(X2_iProver_min_precedes_1,X0_iProver_min_precedes_1)
| ~ subactivity_occurrence(X1_iProver_min_precedes_1,X0_iProver_min_precedes_1)
| ~ occurrence_of(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(subtyping,[status(esa)],[c_99]) ).
tcf(c_5326,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( occurrence_of(X0_iProver_min_precedes_1,sK8(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3))
| ~ atocc(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(subtyping,[status(esa)],[c_89]) ).
tcf(c_5327,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( atomic(sK8(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3))
| ~ atocc(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(subtyping,[status(esa)],[c_88]) ).
tcf(c_5330,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( ~ leaf(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ min_precedes(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(subtyping,[status(esa)],[c_83]) ).
tcf(c_5338,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( legal(X0_iProver_min_precedes_1)
| ~ root(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(subtyping,[status(esa)],[c_75]) ).
tcf(c_5339,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( precedes(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1)
| ~ min_precedes(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(subtyping,[status(esa)],[c_74]) ).
tcf(c_5340,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( ~ root(X1_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ min_precedes(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(subtyping,[status(esa)],[c_73]) ).
tcf(c_5346,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( atocc(X0_iProver_min_precedes_1,sK2(X0_iProver_min_precedes_3,X0_iProver_min_precedes_1,X1_iProver_min_precedes_1))
| ~ min_precedes(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(subtyping,[status(esa)],[c_67]) ).
tcf(c_5349,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( legal(X1_iProver_min_precedes_1)
| ~ precedes(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1) ),
inference(subtyping,[status(esa)],[c_64]) ).
tcf(c_5353,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(X0_iProver_min_precedes_1)
| ~ legal(X0_iProver_min_precedes_1) ),
inference(subtyping,[status(esa)],[c_60]) ).
tcf(c_5355,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( arboreal(X0_iProver_min_precedes_1)
| ~ atomic(X0_iProver_min_precedes_3)
| ~ occurrence_of(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(subtyping,[status(esa)],[c_58]) ).
tcf(c_5360,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_3: iProver_min_precedes_3] :
( ( X0_iProver_min_precedes_3 = X1_iProver_min_precedes_3 )
| ~ occurrence_of(X0_iProver_min_precedes_1,X1_iProver_min_precedes_3)
| ~ occurrence_of(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(subtyping,[status(esa)],[c_53]) ).
tcf(c_5366,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] : X0_iProver_min_precedes_1 = X0_iProver_min_precedes_1,
theory(equality) ).
tcf(c_5367,plain,
! [X0_iProver_min_precedes_3: iProver_min_precedes_3] : X0_iProver_min_precedes_3 = X0_iProver_min_precedes_3,
theory(equality) ).
tcf(c_5368,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1,X2_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( X2_iProver_min_precedes_1 = X0_iProver_min_precedes_1 )
| ( X2_iProver_min_precedes_1 != X1_iProver_min_precedes_1 )
| ( X0_iProver_min_precedes_1 != X1_iProver_min_precedes_1 ) ),
theory(equality) ).
tcf(c_5371,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_3: iProver_min_precedes_3] :
( occurrence_of(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ occurrence_of(X1_iProver_min_precedes_1,X1_iProver_min_precedes_3)
| ( X0_iProver_min_precedes_3 != X1_iProver_min_precedes_3 )
| ( X0_iProver_min_precedes_1 != X1_iProver_min_precedes_1 ) ),
theory(equality) ).
tcf(c_5376,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_3: iProver_min_precedes_3] :
( root(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ root(X1_iProver_min_precedes_1,X1_iProver_min_precedes_3)
| ( X0_iProver_min_precedes_3 != X1_iProver_min_precedes_3 )
| ( X0_iProver_min_precedes_1 != X1_iProver_min_precedes_1 ) ),
theory(equality) ).
tcf(c_5377,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_3: iProver_min_precedes_3] :
( leaf(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ leaf(X0_iProver_min_precedes_1,X1_iProver_min_precedes_3)
| ( X0_iProver_min_precedes_3 != X1_iProver_min_precedes_3 ) ),
theory(equality) ).
tcf(c_6664,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(sK20(X0_iProver_min_precedes_1),tptp2)
| sP0(sK19,X0_iProver_min_precedes_1,sK17(sK19))
| ~ root_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp3)
| ~ leaf_occ(sK17(sK19),sK19)
| ~ occurrence_of(sK17(sK19),tptp1)
| ~ min_precedes(X0_iProver_min_precedes_1,sK17(sK19),tptp0) ),
inference(instantiation,[status(thm)],[c_5281]) ).
tcf(c_6665,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( subactivity_occurrence(sK20(X0_iProver_min_precedes_1),sK19)
| sP0(sK19,X0_iProver_min_precedes_1,sK17(sK19))
| ~ root_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp3)
| ~ leaf_occ(sK17(sK19),sK19)
| ~ occurrence_of(sK17(sK19),tptp1)
| ~ min_precedes(X0_iProver_min_precedes_1,sK17(sK19),tptp0) ),
inference(instantiation,[status(thm)],[c_5280]) ).
tcf(c_6680,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(X0_iProver_min_precedes_1)
| ~ atomic(tptp2)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp2) ),
inference(instantiation,[status(thm)],[c_5355]) ).
tcf(c_6681,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(X0_iProver_min_precedes_1)
| ~ atomic(tptp3)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp3) ),
inference(instantiation,[status(thm)],[c_5355]) ).
tcf(c_6714,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( tptp1 = tptp2 )
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp2)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1) ),
inference(instantiation,[status(thm)],[c_5360]) ).
tcf(c_6720,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( tptp4 = tptp2 )
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp2)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp4) ),
inference(instantiation,[status(thm)],[c_5360]) ).
tcf(c_6917,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(X0_iProver_min_precedes_1)
| ~ atomic(tptp4)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp4) ),
inference(instantiation,[status(thm)],[c_5355]) ).
tcf(c_7001,plain,
( occurrence_of(sK20(sK15(sK19)),tptp2)
| sP0(sK19,sK15(sK19),sK17(sK19))
| ~ leaf_occ(sK17(sK19),sK19)
| ~ root_occ(sK15(sK19),sK19)
| ~ occurrence_of(sK17(sK19),tptp1)
| ~ occurrence_of(sK15(sK19),tptp3)
| ~ min_precedes(sK15(sK19),sK17(sK19),tptp0) ),
inference(instantiation,[status(thm)],[c_6664]) ).
tcf(c_7027,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ occurrence_of(X1_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ( tptp1 != X0_iProver_min_precedes_3 )
| ( X0_iProver_min_precedes_1 != X1_iProver_min_precedes_1 ) ),
inference(instantiation,[status(thm)],[c_5371]) ).
tcf(c_7049,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(sK15(X0_iProver_min_precedes_1))
| ~ atomic(tptp3)
| ~ occurrence_of(sK15(X0_iProver_min_precedes_1),tptp3) ),
inference(instantiation,[status(thm)],[c_6681]) ).
tcf(c_7050,plain,
( arboreal(sK15(sK19))
| ~ atomic(tptp3)
| ~ occurrence_of(sK15(sK19),tptp3) ),
inference(instantiation,[status(thm)],[c_7049]) ).
tcf(c_7110,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X0_iProver_min_precedes_1,tptp4)
| ~ occurrence_of(X1_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ( tptp4 != X0_iProver_min_precedes_3 )
| ( X0_iProver_min_precedes_1 != X1_iProver_min_precedes_1 ) ),
inference(instantiation,[status(thm)],[c_5371]) ).
tcf(c_7117,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(sK16(X0_iProver_min_precedes_1))
| ~ atomic(tptp4)
| ~ occurrence_of(sK16(X0_iProver_min_precedes_1),tptp4) ),
inference(instantiation,[status(thm)],[c_6917]) ).
tcf(c_7118,plain,
( arboreal(sK16(sK19))
| ~ atomic(tptp4)
| ~ occurrence_of(sK16(sK19),tptp4) ),
inference(instantiation,[status(thm)],[c_7117]) ).
tcf(c_7299,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( arboreal(X0_iProver_min_precedes_1)
| ~ atocc(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ atomic(sK8(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)) ),
inference(superposition,[status(thm)],[c_5326,c_5355]) ).
tcf(c_7353,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ~ occurrence_of(X0_iProver_min_precedes_1,tptp0)
| ~ root(sK17(X0_iProver_min_precedes_1),tptp0) ),
inference(superposition,[status(thm)],[c_5272,c_5340]) ).
tcf(c_7359,plain,
( ~ occurrence_of(sK19,tptp0)
| ~ root(sK17(sK19),tptp0) ),
inference(instantiation,[status(thm)],[c_7353]) ).
tcf(c_7480,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( leaf(sK17(X0_iProver_min_precedes_1),X0_iProver_min_precedes_3)
| ~ leaf(sK17(X0_iProver_min_precedes_1),sK14(sK17(X0_iProver_min_precedes_1),X0_iProver_min_precedes_1))
| ( X0_iProver_min_precedes_3 != sK14(sK17(X0_iProver_min_precedes_1),X0_iProver_min_precedes_1) ) ),
inference(instantiation,[status(thm)],[c_5377]) ).
tcf(c_7481,plain,
( leaf(sK17(sK19),tptp0)
| ~ leaf(sK17(sK19),sK14(sK17(sK19),sK19))
| ( tptp0 != sK14(sK17(sK19),sK19) ) ),
inference(instantiation,[status(thm)],[c_7480]) ).
tcf(c_7497,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( root(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ root(sK15(X1_iProver_min_precedes_1),sK13(sK15(X1_iProver_min_precedes_1),X1_iProver_min_precedes_1))
| ( X0_iProver_min_precedes_3 != sK13(sK15(X1_iProver_min_precedes_1),X1_iProver_min_precedes_1) )
| ( X0_iProver_min_precedes_1 != sK15(X1_iProver_min_precedes_1) ) ),
inference(instantiation,[status(thm)],[c_5376]) ).
tcf(c_7819,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( arboreal(X0_iProver_min_precedes_1)
| ~ atocc(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ atomic(sK8(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)) ),
inference(superposition,[status(thm)],[c_5326,c_5355]) ).
tcf(c_7895,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( arboreal(X0_iProver_min_precedes_1)
| ~ atocc(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(global_subsumption_just,[status(thm)],[c_7819,c_5327,c_7299]) ).
tcf(c_8313,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1,X2_iProver_min_precedes_1: iProver_min_precedes_1] :
( min_precedes(X2_iProver_min_precedes_1,sK15(X0_iProver_min_precedes_1),X0_iProver_min_precedes_3)
| min_precedes(sK15(X0_iProver_min_precedes_1),X2_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ( X2_iProver_min_precedes_1 = sK15(X0_iProver_min_precedes_1) )
| ~ arboreal(X2_iProver_min_precedes_1)
| ~ arboreal(sK15(X0_iProver_min_precedes_1))
| ~ subactivity_occurrence(X2_iProver_min_precedes_1,X1_iProver_min_precedes_1)
| ~ occurrence_of(X1_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ subactivity_occurrence(sK15(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1) ),
inference(instantiation,[status(thm)],[c_5316]) ).
tcf(c_8316,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] : sK15(X0_iProver_min_precedes_1) = sK15(X0_iProver_min_precedes_1),
inference(instantiation,[status(thm)],[c_5366]) ).
tcf(c_8317,plain,
sK15(sK19) = sK15(sK19),
inference(instantiation,[status(thm)],[c_8316]) ).
tcf(c_8338,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] : sK17(X0_iProver_min_precedes_1) = sK17(X0_iProver_min_precedes_1),
inference(instantiation,[status(thm)],[c_5366]) ).
tcf(c_8339,plain,
sK17(sK19) = sK17(sK19),
inference(instantiation,[status(thm)],[c_8338]) ).
tcf(c_8911,plain,
( subactivity_occurrence(sK20(sK15(sK19)),sK19)
| sP0(sK19,sK15(sK19),sK17(sK19))
| ~ leaf_occ(sK17(sK19),sK19)
| ~ root_occ(sK15(sK19),sK19)
| ~ occurrence_of(sK17(sK19),tptp1)
| ~ occurrence_of(sK15(sK19),tptp3)
| ~ min_precedes(sK15(sK19),sK17(sK19),tptp0) ),
inference(instantiation,[status(thm)],[c_6665]) ).
tcf(c_9094,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( tptp1 = tptp2 )
| ~ occurrence_of(sK17(X0_iProver_min_precedes_1),tptp2)
| ~ occurrence_of(sK17(X0_iProver_min_precedes_1),tptp1) ),
inference(instantiation,[status(thm)],[c_6714]) ).
tcf(c_9095,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(sK17(X0_iProver_min_precedes_1))
| ~ atomic(tptp2)
| ~ occurrence_of(sK17(X0_iProver_min_precedes_1),tptp2) ),
inference(instantiation,[status(thm)],[c_6680]) ).
tcf(c_9097,plain,
( ( tptp1 = tptp2 )
| ~ occurrence_of(sK17(sK19),tptp2)
| ~ occurrence_of(sK17(sK19),tptp1) ),
inference(instantiation,[status(thm)],[c_9094]) ).
tcf(c_9219,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( precedes(sK16(X0_iProver_min_precedes_1),sK17(X0_iProver_min_precedes_1))
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(resolution,[status(thm)],[c_5339,c_5272]) ).
tcf(c_9436,plain,
tptp2 = tptp2,
inference(instantiation,[status(thm)],[c_5367]) ).
tcf(c_9444,plain,
tptp1 = tptp1,
inference(instantiation,[status(thm)],[c_5367]) ).
tcf(c_9607,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( legal(sK17(X0_iProver_min_precedes_1))
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(resolution,[status(thm)],[c_5349,c_9219]) ).
tcf(c_9663,plain,
legal(sK17(sK19)),
inference(resolution,[status(thm)],[c_9607,c_5274]) ).
tcf(c_9674,plain,
arboreal(sK17(sK19)),
inference(resolution,[status(thm)],[c_9663,c_5353]) ).
tcf(c_9916,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( ~ leaf(sK17(X0_iProver_min_precedes_1),tptp0)
| ~ min_precedes(sK17(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1,tptp0) ),
inference(instantiation,[status(thm)],[c_5330]) ).
tcf(c_9969,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(sK17(X0_iProver_min_precedes_1))
| occurrence_of(sK17(X0_iProver_min_precedes_1),tptp2)
| ~ atomic(tptp1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(superposition,[status(thm)],[c_5299,c_5355]) ).
tcf(c_9973,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(sK17(X0_iProver_min_precedes_1))
| occurrence_of(sK17(X0_iProver_min_precedes_1),tptp2)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9969,c_5294]) ).
tcf(c_10216,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X0_iProver_min_precedes_1,tptp4)
| ~ occurrence_of(X1_iProver_min_precedes_1,tptp4)
| ( tptp4 != tptp4 )
| ( X0_iProver_min_precedes_1 != X1_iProver_min_precedes_1 ) ),
inference(instantiation,[status(thm)],[c_7110]) ).
tcf(c_10217,plain,
tptp4 = tptp4,
inference(instantiation,[status(thm)],[c_5367]) ).
tcf(c_11065,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(sK17(X0_iProver_min_precedes_1))
| occurrence_of(sK17(X0_iProver_min_precedes_1),tptp2)
| ~ atomic(tptp1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(superposition,[status(thm)],[c_5299,c_5355]) ).
tcf(c_11069,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(sK17(X0_iProver_min_precedes_1))
| occurrence_of(sK17(X0_iProver_min_precedes_1),tptp2)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11065,c_5294]) ).
tcf(c_11550,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(sK17(X1_iProver_min_precedes_1),tptp1)
| sP0(sK19,X0_iProver_min_precedes_1,sK17(X1_iProver_min_precedes_1))
| ~ root_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp3)
| ~ leaf_occ(sK17(X1_iProver_min_precedes_1),sK19)
| ~ occurrence_of(sK17(X1_iProver_min_precedes_1),tptp2)
| ~ min_precedes(X0_iProver_min_precedes_1,sK17(X1_iProver_min_precedes_1),tptp0) ),
inference(instantiation,[status(thm)],[c_5275]) ).
tcf(c_12469,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(sK17(X0_iProver_min_precedes_1))
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(global_subsumption_just,[status(thm)],[c_11069,c_124,c_9095,c_9973]) ).
tcf(c_12615,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1,X2_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( sK17(X0_iProver_min_precedes_1) = X2_iProver_min_precedes_1 )
| ( X2_iProver_min_precedes_1 != X1_iProver_min_precedes_1 )
| ( sK17(X0_iProver_min_precedes_1) != X1_iProver_min_precedes_1 ) ),
inference(instantiation,[status(thm)],[c_5368]) ).
tcf(c_12690,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( X0_iProver_min_precedes_3 = sK14(sK17(X1_iProver_min_precedes_1),X1_iProver_min_precedes_1) )
| ~ occurrence_of(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ occurrence_of(X0_iProver_min_precedes_1,sK14(sK17(X1_iProver_min_precedes_1),X1_iProver_min_precedes_1)) ),
inference(instantiation,[status(thm)],[c_5360]) ).
tcf(c_12691,plain,
( ( tptp0 = sK14(sK17(sK19),sK19) )
| ~ occurrence_of(sK19,tptp0)
| ~ occurrence_of(sK19,sK14(sK17(sK19),sK19)) ),
inference(instantiation,[status(thm)],[c_12690]) ).
tcf(c_12695,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( X0_iProver_min_precedes_3 = sK13(sK15(X1_iProver_min_precedes_1),X1_iProver_min_precedes_1) )
| ~ occurrence_of(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ occurrence_of(X0_iProver_min_precedes_1,sK13(sK15(X1_iProver_min_precedes_1),X1_iProver_min_precedes_1)) ),
inference(instantiation,[status(thm)],[c_5360]) ).
tcf(c_12696,plain,
( ( tptp0 = sK13(sK15(sK19),sK19) )
| ~ occurrence_of(sK19,tptp0)
| ~ occurrence_of(sK19,sK13(sK15(sK19),sK19)) ),
inference(instantiation,[status(thm)],[c_12695]) ).
tcf(c_12956,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( min_precedes(sK17(sK19),sK15(X0_iProver_min_precedes_1),X0_iProver_min_precedes_3)
| min_precedes(sK15(X0_iProver_min_precedes_1),sK17(sK19),X0_iProver_min_precedes_3)
| ( sK17(sK19) = sK15(X0_iProver_min_precedes_1) )
| ~ arboreal(sK17(sK19))
| ~ arboreal(sK15(X0_iProver_min_precedes_1))
| ~ occurrence_of(X1_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ subactivity_occurrence(sK17(sK19),X1_iProver_min_precedes_1)
| ~ subactivity_occurrence(sK15(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1) ),
inference(instantiation,[status(thm)],[c_8313]) ).
tcf(c_12957,plain,
( min_precedes(sK17(sK19),sK15(sK19),tptp0)
| min_precedes(sK15(sK19),sK17(sK19),tptp0)
| ( sK17(sK19) = sK15(sK19) )
| ~ arboreal(sK17(sK19))
| ~ arboreal(sK15(sK19))
| ~ occurrence_of(sK19,tptp0)
| ~ subactivity_occurrence(sK17(sK19),sK19)
| ~ subactivity_occurrence(sK15(sK19),sK19) ),
inference(instantiation,[status(thm)],[c_12956]) ).
tcf(c_13030,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ occurrence_of(X1_iProver_min_precedes_1,tptp1)
| ( tptp1 != tptp1 )
| ( X0_iProver_min_precedes_1 != X1_iProver_min_precedes_1 ) ),
inference(instantiation,[status(thm)],[c_7027]) ).
tcf(c_13853,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( ~ leaf(sK17(X0_iProver_min_precedes_1),X0_iProver_min_precedes_3)
| ~ min_precedes(sK17(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(instantiation,[status(thm)],[c_5330]) ).
tcf(c_13892,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X0_iProver_min_precedes_1,tptp4)
| ~ occurrence_of(sK16(X1_iProver_min_precedes_1),tptp4)
| ( tptp4 != tptp4 )
| ( X0_iProver_min_precedes_1 != sK16(X1_iProver_min_precedes_1) ) ),
inference(instantiation,[status(thm)],[c_10216]) ).
tcf(c_14443,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( root(sK15(X0_iProver_min_precedes_1),X0_iProver_min_precedes_3)
| ~ root(sK15(X0_iProver_min_precedes_1),sK13(sK15(X0_iProver_min_precedes_1),X0_iProver_min_precedes_1))
| ( X0_iProver_min_precedes_3 != sK13(sK15(X0_iProver_min_precedes_1),X0_iProver_min_precedes_1) )
| ( sK15(X0_iProver_min_precedes_1) != sK15(X0_iProver_min_precedes_1) ) ),
inference(instantiation,[status(thm)],[c_7497]) ).
tcf(c_14444,plain,
( root(sK15(sK19),tptp0)
| ~ root(sK15(sK19),sK13(sK15(sK19),sK19))
| ( tptp0 != sK13(sK15(sK19),sK19) )
| ( sK15(sK19) != sK15(sK19) ) ),
inference(instantiation,[status(thm)],[c_14443]) ).
tcf(c_18521,plain,
( ( tptp4 = tptp2 )
| ~ occurrence_of(sK20(sK15(sK19)),tptp2)
| ~ occurrence_of(sK20(sK15(sK19)),tptp4) ),
inference(instantiation,[status(thm)],[c_6720]) ).
tcf(c_18523,plain,
( ( tptp1 = tptp2 )
| ~ occurrence_of(sK20(sK15(sK19)),tptp2)
| ~ occurrence_of(sK20(sK15(sK19)),tptp1) ),
inference(instantiation,[status(thm)],[c_6714]) ).
tcf(c_18524,plain,
( arboreal(sK20(sK15(sK19)))
| ~ atomic(tptp2)
| ~ occurrence_of(sK20(sK15(sK19)),tptp2) ),
inference(instantiation,[status(thm)],[c_6680]) ).
tcf(c_20027,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( sK17(sK19) = X1_iProver_min_precedes_1 )
| ( X1_iProver_min_precedes_1 != sK17(X0_iProver_min_precedes_1) )
| ( sK17(sK19) != sK17(X0_iProver_min_precedes_1) ) ),
inference(instantiation,[status(thm)],[c_12615]) ).
tcf(c_20084,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ~ leaf(sK17(sK19),tptp0)
| ~ min_precedes(sK17(sK19),sK15(X0_iProver_min_precedes_1),tptp0) ),
inference(instantiation,[status(thm)],[c_9916]) ).
tcf(c_20085,plain,
( ~ leaf(sK17(sK19),tptp0)
| ~ min_precedes(sK17(sK19),sK15(sK19),tptp0) ),
inference(instantiation,[status(thm)],[c_20084]) ).
tcf(c_20891,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( subactivity_occurrence(sK16(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1)
| ~ occurrence_of(X1_iProver_min_precedes_1,tptp0)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0)
| ~ subactivity_occurrence(sK17(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1) ),
inference(superposition,[status(thm)],[c_5272,c_5315]) ).
tcf(c_20900,plain,
( subactivity_occurrence(sK16(sK19),sK19)
| ~ occurrence_of(sK19,tptp0)
| ~ subactivity_occurrence(sK17(sK19),sK19) ),
inference(instantiation,[status(thm)],[c_20891]) ).
tcf(c_21420,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ occurrence_of(sK17(X1_iProver_min_precedes_1),tptp1)
| ( tptp1 != tptp1 )
| ( X0_iProver_min_precedes_1 != sK17(X1_iProver_min_precedes_1) ) ),
inference(instantiation,[status(thm)],[c_13030]) ).
tcf(c_22481,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( root(sK17(sK19),X0_iProver_min_precedes_3)
| ~ root(sK15(X0_iProver_min_precedes_1),sK13(sK15(X0_iProver_min_precedes_1),X0_iProver_min_precedes_1))
| ( X0_iProver_min_precedes_3 != sK13(sK15(X0_iProver_min_precedes_1),X0_iProver_min_precedes_1) )
| ( sK17(sK19) != sK15(X0_iProver_min_precedes_1) ) ),
inference(instantiation,[status(thm)],[c_7497]) ).
tcf(c_22484,plain,
( root(sK17(sK19),tptp0)
| ~ root(sK15(sK19),sK13(sK15(sK19),sK19))
| ( tptp0 != sK13(sK15(sK19),sK19) )
| ( sK17(sK19) != sK15(sK19) ) ),
inference(instantiation,[status(thm)],[c_22481]) ).
tcf(c_29624,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( sK17(sK19) = sK15(X0_iProver_min_precedes_1) )
| ( sK17(sK19) != sK17(sK19) )
| ( sK15(X0_iProver_min_precedes_1) != sK17(sK19) ) ),
inference(instantiation,[status(thm)],[c_20027]) ).
tcf(c_29625,plain,
( ( sK17(sK19) = sK15(sK19) )
| ( sK17(sK19) != sK17(sK19) )
| ( sK15(sK19) != sK17(sK19) ) ),
inference(instantiation,[status(thm)],[c_29624]) ).
tcf(c_31247,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(sK17(sK19),tptp1)
| sP0(sK19,sK15(X0_iProver_min_precedes_1),sK17(sK19))
| ~ leaf_occ(sK17(sK19),sK19)
| ~ occurrence_of(sK17(sK19),tptp2)
| ~ root_occ(sK15(X0_iProver_min_precedes_1),sK19)
| ~ occurrence_of(sK15(X0_iProver_min_precedes_1),tptp3)
| ~ min_precedes(sK15(X0_iProver_min_precedes_1),sK17(sK19),tptp0) ),
inference(instantiation,[status(thm)],[c_11550]) ).
tcf(c_31252,plain,
( occurrence_of(sK17(sK19),tptp1)
| sP0(sK19,sK15(sK19),sK17(sK19))
| ~ leaf_occ(sK17(sK19),sK19)
| ~ root_occ(sK15(sK19),sK19)
| ~ occurrence_of(sK17(sK19),tptp2)
| ~ occurrence_of(sK15(sK19),tptp3)
| ~ min_precedes(sK15(sK19),sK17(sK19),tptp0) ),
inference(instantiation,[status(thm)],[c_31247]) ).
tcf(c_40390,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( subactivity_occurrence(sK17(X0_iProver_min_precedes_1),X0_iProver_min_precedes_1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(superposition,[status(thm)],[c_5298,c_5304]) ).
tcf(c_40458,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( legal(X0_iProver_min_precedes_1)
| ~ root_occ(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1) ),
inference(superposition,[status(thm)],[c_5307,c_5338]) ).
tcf(c_40467,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( legal(sK15(X0_iProver_min_precedes_1))
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(superposition,[status(thm)],[c_5301,c_40458]) ).
tcf(c_40480,plain,
legal(sK15(sK19)),
inference(superposition,[status(thm)],[c_5274,c_40467]) ).
tcf(c_40481,plain,
arboreal(sK15(sK19)),
inference(superposition,[status(thm)],[c_40480,c_5353]) ).
tcf(c_40555,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(sK16(X0_iProver_min_precedes_1))
| ~ atomic(tptp4)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(superposition,[status(thm)],[c_5300,c_5355]) ).
tcf(c_40559,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( arboreal(X0_iProver_min_precedes_1)
| ~ atocc(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ atomic(sK8(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)) ),
inference(superposition,[status(thm)],[c_5326,c_5355]) ).
tcf(c_40562,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(sK16(X0_iProver_min_precedes_1))
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_40555,c_5295]) ).
tcf(c_40576,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( arboreal(X0_iProver_min_precedes_1)
| ~ atocc(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(global_subsumption_just,[status(thm)],[c_40559,c_7895]) ).
tcf(c_40974,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(X0_iProver_min_precedes_1)
| ~ min_precedes(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(superposition,[status(thm)],[c_5346,c_40576]) ).
tcf(c_41161,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(sK17(X0_iProver_min_precedes_1))
| occurrence_of(sK17(X0_iProver_min_precedes_1),tptp2)
| ~ atomic(tptp1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(superposition,[status(thm)],[c_5299,c_5355]) ).
tcf(c_41165,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(sK17(X0_iProver_min_precedes_1))
| occurrence_of(sK17(X0_iProver_min_precedes_1),tptp2)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_41161,c_5294]) ).
tcf(c_41169,plain,
! [X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( ( X0_iProver_min_precedes_3 = tptp0 )
| ~ occurrence_of(sK19,X0_iProver_min_precedes_3) ),
inference(superposition,[status(thm)],[c_5274,c_5360]) ).
tcf(c_41183,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(sK17(X0_iProver_min_precedes_1))
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0) ),
inference(global_subsumption_just,[status(thm)],[c_41165,c_12469]) ).
tcf(c_41187,plain,
arboreal(sK17(sK19)),
inference(superposition,[status(thm)],[c_5274,c_41183]) ).
tcf(c_41195,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( sK13(X0_iProver_min_precedes_1,sK19) = tptp0 )
| ~ root_occ(X0_iProver_min_precedes_1,sK19) ),
inference(superposition,[status(thm)],[c_5309,c_41169]) ).
tcf(c_41473,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( leaf_occ(X0_iProver_min_precedes_1,sK19)
| ~ subactivity_occurrence(X0_iProver_min_precedes_1,sK19)
| ~ leaf(X0_iProver_min_precedes_1,tptp0) ),
inference(superposition,[status(thm)],[c_5274,c_5306]) ).
tcf(c_41488,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( root_occ(X0_iProver_min_precedes_1,sK19)
| ~ subactivity_occurrence(X0_iProver_min_precedes_1,sK19)
| ~ root(X0_iProver_min_precedes_1,tptp0) ),
inference(superposition,[status(thm)],[c_5274,c_5310]) ).
tcf(c_41543,plain,
( leaf_occ(sK17(sK19),sK19)
| ~ occurrence_of(sK19,tptp0)
| ~ leaf(sK17(sK19),tptp0) ),
inference(superposition,[status(thm)],[c_40390,c_41473]) ).
tcf(c_41546,plain,
( leaf_occ(sK17(sK19),sK19)
| ~ leaf(sK17(sK19),tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_41543,c_5274]) ).
tcf(c_41547,plain,
leaf_occ(sK17(sK19),sK19),
inference(global_subsumption_just,[status(thm)],[c_41546,c_143,c_157]) ).
tcf(c_41551,plain,
subactivity_occurrence(sK17(sK19),sK19),
inference(superposition,[status(thm)],[c_41547,c_5304]) ).
tcf(c_41851,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( min_precedes(X0_iProver_min_precedes_1,sK17(sK19),X0_iProver_min_precedes_3)
| min_precedes(sK17(sK19),X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ( sK17(sK19) = X0_iProver_min_precedes_1 )
| ~ arboreal(X0_iProver_min_precedes_1)
| ~ arboreal(sK17(sK19))
| ~ subactivity_occurrence(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(sK19,X0_iProver_min_precedes_3) ),
inference(superposition,[status(thm)],[c_41551,c_5316]) ).
tcf(c_41853,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( min_precedes(X0_iProver_min_precedes_1,sK17(sK19),X0_iProver_min_precedes_3)
| min_precedes(sK17(sK19),X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ( sK17(sK19) = X0_iProver_min_precedes_1 )
| ~ arboreal(X0_iProver_min_precedes_1)
| ~ subactivity_occurrence(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(sK19,X0_iProver_min_precedes_3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_41851,c_41187]) ).
tcf(c_41932,plain,
arboreal(sK16(sK19)),
inference(superposition,[status(thm)],[c_5274,c_40562]) ).
tcf(c_42284,plain,
( ( sK13(sK15(sK19),sK19) = tptp0 )
| ~ occurrence_of(sK19,tptp0) ),
inference(superposition,[status(thm)],[c_5301,c_41195]) ).
tcf(c_42285,plain,
sK13(sK15(sK19),sK19) = tptp0,
inference(forward_subsumption_resolution,[status(thm)],[c_42284,c_5274]) ).
tcf(c_42288,plain,
( root(sK15(sK19),tptp0)
| ~ root_occ(sK15(sK19),sK19) ),
inference(superposition,[status(thm)],[c_42285,c_5307]) ).
tcf(c_42290,plain,
root(sK15(sK19),tptp0),
inference(global_subsumption_just,[status(thm)],[c_42288,c_143,c_3502,c_3520,c_8317,c_12696,c_14444]) ).
tcf(c_42295,plain,
( root_occ(sK15(sK19),sK19)
| ~ subactivity_occurrence(sK15(sK19),sK19) ),
inference(superposition,[status(thm)],[c_42290,c_41488]) ).
tcf(c_42327,plain,
root_occ(sK15(sK19),sK19),
inference(global_subsumption_just,[status(thm)],[c_42295,c_143,c_159]) ).
tcf(c_42334,plain,
subactivity_occurrence(sK15(sK19),sK19),
inference(superposition,[status(thm)],[c_42327,c_5308]) ).
tcf(c_43097,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( subactivity_occurrence(sK16(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1)
| ~ occurrence_of(X1_iProver_min_precedes_1,tptp0)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0)
| ~ subactivity_occurrence(sK17(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1) ),
inference(superposition,[status(thm)],[c_5272,c_5315]) ).
tcf(c_44156,plain,
( subactivity_occurrence(sK16(sK19),sK19)
| ~ occurrence_of(sK19,tptp0) ),
inference(superposition,[status(thm)],[c_41551,c_43097]) ).
tcf(c_44162,plain,
subactivity_occurrence(sK16(sK19),sK19),
inference(forward_subsumption_resolution,[status(thm)],[c_44156,c_5274]) ).
tcf(c_44179,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( min_precedes(X0_iProver_min_precedes_1,sK16(sK19),X0_iProver_min_precedes_3)
| min_precedes(sK16(sK19),X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ( sK16(sK19) = X0_iProver_min_precedes_1 )
| ~ arboreal(X0_iProver_min_precedes_1)
| ~ arboreal(sK16(sK19))
| ~ subactivity_occurrence(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(sK19,X0_iProver_min_precedes_3) ),
inference(superposition,[status(thm)],[c_44162,c_5316]) ).
tcf(c_44182,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( min_precedes(X0_iProver_min_precedes_1,sK16(sK19),X0_iProver_min_precedes_3)
| min_precedes(sK16(sK19),X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ( sK16(sK19) = X0_iProver_min_precedes_1 )
| ~ arboreal(X0_iProver_min_precedes_1)
| ~ subactivity_occurrence(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(sK19,X0_iProver_min_precedes_3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_44179,c_41932]) ).
tcf(c_52197,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ~ occurrence_of(X0_iProver_min_precedes_1,tptp0)
| ~ min_precedes(sK16(X0_iProver_min_precedes_1),sK20(sK15(sK19)),tptp0)
| ~ min_precedes(sK20(sK15(sK19)),sK17(X0_iProver_min_precedes_1),tptp0) ),
inference(instantiation,[status(thm)],[c_5270]) ).
tcf(c_52198,plain,
( ~ occurrence_of(sK19,tptp0)
| ~ min_precedes(sK16(sK19),sK20(sK15(sK19)),tptp0)
| ~ min_precedes(sK20(sK15(sK19)),sK17(sK19),tptp0) ),
inference(instantiation,[status(thm)],[c_52197]) ).
tcf(c_58753,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( sP0(sK19,sK15(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1)
| ~ leaf_occ(X1_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X1_iProver_min_precedes_1,tptp1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0)
| ~ root_occ(sK15(X0_iProver_min_precedes_1),sK19)
| ~ occurrence_of(sK15(X0_iProver_min_precedes_1),tptp3)
| ~ min_precedes(sK15(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1,tptp0)
| ~ min_precedes(sK20(sK15(X0_iProver_min_precedes_1)),sK16(X0_iProver_min_precedes_1),tptp0) ),
inference(superposition,[status(thm)],[c_5279,c_5271]) ).
tcf(c_60116,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( sP0(sK19,sK15(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1)
| ~ leaf_occ(X1_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X1_iProver_min_precedes_1,tptp1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0)
| ~ root_occ(sK15(X0_iProver_min_precedes_1),sK19)
| ~ min_precedes(sK20(sK15(X0_iProver_min_precedes_1)),sK16(X0_iProver_min_precedes_1),tptp0)
| ~ min_precedes(sK15(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1,tptp0) ),
inference(global_subsumption_just,[status(thm)],[c_58753,c_5302,c_58753]) ).
tcf(c_60117,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( sP0(sK19,sK15(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1)
| ~ leaf_occ(X1_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X1_iProver_min_precedes_1,tptp1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp0)
| ~ root_occ(sK15(X0_iProver_min_precedes_1),sK19)
| ~ min_precedes(sK15(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1,tptp0)
| ~ min_precedes(sK20(sK15(X0_iProver_min_precedes_1)),sK16(X0_iProver_min_precedes_1),tptp0) ),
inference(renaming,[status(thm)],[c_60116]) ).
tcf(c_60128,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( sP0(sK19,sK15(sK19),X0_iProver_min_precedes_1)
| min_precedes(sK16(sK19),sK20(sK15(sK19)),tptp0)
| ( sK20(sK15(sK19)) = sK16(sK19) )
| ~ occurrence_of(sK19,tptp0)
| ~ leaf_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ root_occ(sK15(sK19),sK19)
| ~ arboreal(sK20(sK15(sK19)))
| ~ subactivity_occurrence(sK20(sK15(sK19)),sK19)
| ~ min_precedes(sK15(sK19),X0_iProver_min_precedes_1,tptp0) ),
inference(superposition,[status(thm)],[c_44182,c_60117]) ).
tcf(c_60134,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( sP0(sK19,sK15(sK19),X0_iProver_min_precedes_1)
| min_precedes(sK16(sK19),sK20(sK15(sK19)),tptp0)
| ( sK20(sK15(sK19)) = sK16(sK19) )
| ~ leaf_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ arboreal(sK20(sK15(sK19)))
| ~ subactivity_occurrence(sK20(sK15(sK19)),sK19)
| ~ min_precedes(sK15(sK19),X0_iProver_min_precedes_1,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_60128,c_5274,c_42327]) ).
tcf(c_60348,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( sP0(sK19,sK15(sK19),X0_iProver_min_precedes_1)
| ( sK20(sK15(sK19)) = sK16(sK19) )
| ~ occurrence_of(sK19,tptp0)
| ~ leaf_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ arboreal(sK20(sK15(sK19)))
| ~ subactivity_occurrence(sK20(sK15(sK19)),sK19)
| ~ min_precedes(sK15(sK19),X0_iProver_min_precedes_1,tptp0)
| ~ min_precedes(sK20(sK15(sK19)),sK17(sK19),tptp0) ),
inference(superposition,[status(thm)],[c_60134,c_5270]) ).
tcf(c_60410,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( sP0(sK19,sK15(sK19),X0_iProver_min_precedes_1)
| ( sK20(sK15(sK19)) = sK16(sK19) )
| ~ leaf_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ arboreal(sK20(sK15(sK19)))
| ~ subactivity_occurrence(sK20(sK15(sK19)),sK19)
| ~ min_precedes(sK15(sK19),X0_iProver_min_precedes_1,tptp0)
| ~ min_precedes(sK20(sK15(sK19)),sK17(sK19),tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_60348,c_5274]) ).
tcf(c_60801,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(sK20(sK15(sK19)),tptp1)
| ~ occurrence_of(sK17(X0_iProver_min_precedes_1),tptp1)
| ( tptp1 != tptp1 )
| ( sK20(sK15(sK19)) != sK17(X0_iProver_min_precedes_1) ) ),
inference(instantiation,[status(thm)],[c_21420]) ).
tcf(c_60805,plain,
( occurrence_of(sK20(sK15(sK19)),tptp1)
| ~ occurrence_of(sK17(sK19),tptp1)
| ( tptp1 != tptp1 )
| ( sK20(sK15(sK19)) != sK17(sK19) ) ),
inference(instantiation,[status(thm)],[c_60801]) ).
tcf(c_63197,plain,
! [X0_iProver_min_precedes_3: iProver_min_precedes_3] :
( ~ leaf(sK17(sK19),X0_iProver_min_precedes_3)
| ~ min_precedes(sK17(sK19),sK20(sK15(sK19)),X0_iProver_min_precedes_3) ),
inference(instantiation,[status(thm)],[c_13853]) ).
tcf(c_63200,plain,
( ~ leaf(sK17(sK19),tptp0)
| ~ min_precedes(sK17(sK19),sK20(sK15(sK19)),tptp0) ),
inference(instantiation,[status(thm)],[c_63197]) ).
tcf(c_65952,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(sK20(sK15(sK19)),tptp4)
| ~ occurrence_of(sK16(X0_iProver_min_precedes_1),tptp4)
| ( tptp4 != tptp4 )
| ( sK20(sK15(sK19)) != sK16(X0_iProver_min_precedes_1) ) ),
inference(instantiation,[status(thm)],[c_13892]) ).
tcf(c_65955,plain,
( occurrence_of(sK20(sK15(sK19)),tptp4)
| ~ occurrence_of(sK16(sK19),tptp4)
| ( tptp4 != tptp4 )
| ( sK20(sK15(sK19)) != sK16(sK19) ) ),
inference(instantiation,[status(thm)],[c_65952]) ).
tcf(c_67388,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( arboreal(X0_iProver_min_precedes_1)
| ~ atomic(tptp1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1) ),
inference(instantiation,[status(thm)],[c_5355]) ).
tcf(c_67407,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( tptp1 = tptp2 )
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp2)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1) ),
inference(instantiation,[status(thm)],[c_5360]) ).
tcf(c_67411,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( tptp4 = tptp1 )
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp4) ),
inference(instantiation,[status(thm)],[c_5360]) ).
tcf(c_67480,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X0_iProver_min_precedes_1,tptp2)
| ~ occurrence_of(X1_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ( tptp2 != X0_iProver_min_precedes_3 )
| ( X0_iProver_min_precedes_1 != X1_iProver_min_precedes_1 ) ),
inference(instantiation,[status(thm)],[c_5371]) ).
tcf(c_67498,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X0_iProver_min_precedes_1,tptp4)
| ~ occurrence_of(X1_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ( tptp4 != X0_iProver_min_precedes_3 )
| ( X0_iProver_min_precedes_1 != X1_iProver_min_precedes_1 ) ),
inference(instantiation,[status(thm)],[c_5371]) ).
tcf(c_67642,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1,X2_iProver_min_precedes_1: iProver_min_precedes_1] :
( min_precedes(X2_iProver_min_precedes_1,sK17(X0_iProver_min_precedes_1),X0_iProver_min_precedes_3)
| min_precedes(sK17(X0_iProver_min_precedes_1),X2_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ( X2_iProver_min_precedes_1 = sK17(X0_iProver_min_precedes_1) )
| ~ arboreal(X2_iProver_min_precedes_1)
| ~ arboreal(sK17(X0_iProver_min_precedes_1))
| ~ subactivity_occurrence(X2_iProver_min_precedes_1,X1_iProver_min_precedes_1)
| ~ occurrence_of(X1_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ subactivity_occurrence(sK17(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1) ),
inference(instantiation,[status(thm)],[c_5316]) ).
tcf(c_67652,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1,X2_iProver_min_precedes_1: iProver_min_precedes_1] :
( min_precedes(X2_iProver_min_precedes_1,sK16(X0_iProver_min_precedes_1),X0_iProver_min_precedes_3)
| min_precedes(sK16(X0_iProver_min_precedes_1),X2_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ( X2_iProver_min_precedes_1 = sK16(X0_iProver_min_precedes_1) )
| ~ arboreal(X2_iProver_min_precedes_1)
| ~ arboreal(sK16(X0_iProver_min_precedes_1))
| ~ subactivity_occurrence(X2_iProver_min_precedes_1,X1_iProver_min_precedes_1)
| ~ occurrence_of(X1_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ subactivity_occurrence(sK16(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1) ),
inference(instantiation,[status(thm)],[c_5316]) ).
tcf(c_67900,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( ~ leaf(sK17(X0_iProver_min_precedes_1),X0_iProver_min_precedes_3)
| ~ min_precedes(sK17(X0_iProver_min_precedes_1),X1_iProver_min_precedes_1,X0_iProver_min_precedes_3) ),
inference(instantiation,[status(thm)],[c_5330]) ).
tcf(c_67980,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X0_iProver_min_precedes_1,tptp4)
| ~ occurrence_of(X1_iProver_min_precedes_1,tptp4)
| ( tptp4 != tptp4 )
| ( X0_iProver_min_precedes_1 != X1_iProver_min_precedes_1 ) ),
inference(instantiation,[status(thm)],[c_67498]) ).
tcf(c_68375,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X0_iProver_min_precedes_1,tptp2)
| ~ occurrence_of(X1_iProver_min_precedes_1,tptp2)
| ( tptp2 != tptp2 )
| ( X0_iProver_min_precedes_1 != X1_iProver_min_precedes_1 ) ),
inference(instantiation,[status(thm)],[c_67480]) ).
tcf(c_68502,plain,
( ( tptp4 = tptp1 )
| ~ occurrence_of(sK18(sK19,sK15(sK19)),tptp1)
| ~ occurrence_of(sK18(sK19,sK15(sK19)),tptp4) ),
inference(instantiation,[status(thm)],[c_67411]) ).
tcf(c_68504,plain,
( ( tptp1 = tptp2 )
| ~ occurrence_of(sK18(sK19,sK15(sK19)),tptp2)
| ~ occurrence_of(sK18(sK19,sK15(sK19)),tptp1) ),
inference(instantiation,[status(thm)],[c_67407]) ).
tcf(c_68505,plain,
( arboreal(sK18(sK19,sK15(sK19)))
| ~ atomic(tptp1)
| ~ occurrence_of(sK18(sK19,sK15(sK19)),tptp1) ),
inference(instantiation,[status(thm)],[c_67388]) ).
tcf(c_68887,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X0_iProver_min_precedes_1,tptp4)
| ~ occurrence_of(sK16(X1_iProver_min_precedes_1),tptp4)
| ( tptp4 != tptp4 )
| ( X0_iProver_min_precedes_1 != sK16(X1_iProver_min_precedes_1) ) ),
inference(instantiation,[status(thm)],[c_67980]) ).
tcf(c_70493,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( min_precedes(sK16(X1_iProver_min_precedes_1),sK18(sK19,sK15(sK19)),X0_iProver_min_precedes_3)
| min_precedes(sK18(sK19,sK15(sK19)),sK16(X1_iProver_min_precedes_1),X0_iProver_min_precedes_3)
| ( sK18(sK19,sK15(sK19)) = sK16(X1_iProver_min_precedes_1) )
| ~ arboreal(sK16(X1_iProver_min_precedes_1))
| ~ occurrence_of(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ subactivity_occurrence(sK16(X1_iProver_min_precedes_1),X0_iProver_min_precedes_1)
| ~ arboreal(sK18(sK19,sK15(sK19)))
| ~ subactivity_occurrence(sK18(sK19,sK15(sK19)),X0_iProver_min_precedes_1) ),
inference(instantiation,[status(thm)],[c_67652]) ).
tcf(c_70494,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X0_iProver_min_precedes_3: iProver_min_precedes_3,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( min_precedes(sK17(X1_iProver_min_precedes_1),sK18(sK19,sK15(sK19)),X0_iProver_min_precedes_3)
| min_precedes(sK18(sK19,sK15(sK19)),sK17(X1_iProver_min_precedes_1),X0_iProver_min_precedes_3)
| ( sK18(sK19,sK15(sK19)) = sK17(X1_iProver_min_precedes_1) )
| ~ arboreal(sK17(X1_iProver_min_precedes_1))
| ~ occurrence_of(X0_iProver_min_precedes_1,X0_iProver_min_precedes_3)
| ~ subactivity_occurrence(sK17(X1_iProver_min_precedes_1),X0_iProver_min_precedes_1)
| ~ arboreal(sK18(sK19,sK15(sK19)))
| ~ subactivity_occurrence(sK18(sK19,sK15(sK19)),X0_iProver_min_precedes_1) ),
inference(instantiation,[status(thm)],[c_67642]) ).
tcf(c_70497,plain,
( min_precedes(sK17(sK19),sK18(sK19,sK15(sK19)),tptp0)
| min_precedes(sK18(sK19,sK15(sK19)),sK17(sK19),tptp0)
| ( sK18(sK19,sK15(sK19)) = sK17(sK19) )
| ~ arboreal(sK17(sK19))
| ~ occurrence_of(sK19,tptp0)
| ~ subactivity_occurrence(sK17(sK19),sK19)
| ~ arboreal(sK18(sK19,sK15(sK19)))
| ~ subactivity_occurrence(sK18(sK19,sK15(sK19)),sK19) ),
inference(instantiation,[status(thm)],[c_70494]) ).
tcf(c_70498,plain,
( min_precedes(sK16(sK19),sK18(sK19,sK15(sK19)),tptp0)
| min_precedes(sK18(sK19,sK15(sK19)),sK16(sK19),tptp0)
| ( sK18(sK19,sK15(sK19)) = sK16(sK19) )
| ~ arboreal(sK16(sK19))
| ~ occurrence_of(sK19,tptp0)
| ~ subactivity_occurrence(sK16(sK19),sK19)
| ~ arboreal(sK18(sK19,sK15(sK19)))
| ~ subactivity_occurrence(sK18(sK19,sK15(sK19)),sK19) ),
inference(instantiation,[status(thm)],[c_70493]) ).
tcf(c_70875,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X0_iProver_min_precedes_1,tptp2)
| ~ occurrence_of(sK17(sK19),tptp2)
| ( tptp2 != tptp2 )
| ( X0_iProver_min_precedes_1 != sK17(sK19) ) ),
inference(instantiation,[status(thm)],[c_68375]) ).
tcf(c_73717,plain,
( occurrence_of(sK18(sK19,sK15(sK19)),tptp2)
| ~ occurrence_of(sK17(sK19),tptp2)
| ( tptp2 != tptp2 )
| ( sK18(sK19,sK15(sK19)) != sK17(sK19) ) ),
inference(instantiation,[status(thm)],[c_70875]) ).
tcf(c_75677,plain,
( ~ occurrence_of(sK19,tptp0)
| ~ min_precedes(sK16(sK19),sK18(sK19,sK15(sK19)),tptp0)
| ~ min_precedes(sK18(sK19,sK15(sK19)),sK17(sK19),tptp0) ),
inference(instantiation,[status(thm)],[c_5270]) ).
tcf(c_76136,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ~ occurrence_of(X0_iProver_min_precedes_1,tptp0)
| ~ min_precedes(sK15(X0_iProver_min_precedes_1),sK18(sK19,sK15(sK19)),tptp0)
| ~ min_precedes(sK18(sK19,sK15(sK19)),sK16(X0_iProver_min_precedes_1),tptp0) ),
inference(instantiation,[status(thm)],[c_5271]) ).
tcf(c_76137,plain,
( ~ occurrence_of(sK19,tptp0)
| ~ min_precedes(sK15(sK19),sK18(sK19,sK15(sK19)),tptp0)
| ~ min_precedes(sK18(sK19,sK15(sK19)),sK16(sK19),tptp0) ),
inference(instantiation,[status(thm)],[c_76136]) ).
tcf(c_78232,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1] :
( ~ leaf(sK17(X0_iProver_min_precedes_1),tptp0)
| ~ min_precedes(sK17(X0_iProver_min_precedes_1),sK18(sK19,sK15(X1_iProver_min_precedes_1)),tptp0) ),
inference(instantiation,[status(thm)],[c_67900]) ).
tcf(c_78234,plain,
( ~ leaf(sK17(sK19),tptp0)
| ~ min_precedes(sK17(sK19),sK18(sK19,sK15(sK19)),tptp0) ),
inference(instantiation,[status(thm)],[c_78232]) ).
tcf(c_82346,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(sK18(sK19,sK15(sK19)),tptp4)
| ~ occurrence_of(sK16(X0_iProver_min_precedes_1),tptp4)
| ( tptp4 != tptp4 )
| ( sK18(sK19,sK15(sK19)) != sK16(X0_iProver_min_precedes_1) ) ),
inference(instantiation,[status(thm)],[c_68887]) ).
tcf(c_82349,plain,
( occurrence_of(sK18(sK19,sK15(sK19)),tptp4)
| ~ occurrence_of(sK16(sK19),tptp4)
| ( tptp4 != tptp4 )
| ( sK18(sK19,sK15(sK19)) != sK16(sK19) ) ),
inference(instantiation,[status(thm)],[c_82346]) ).
fof(f99,definition,
! [X0,X1,X2] :
( ~ sP0(X0,X1,X2)
| ( occurrence_of(X2,tptp2)
& ? [X4] :
( min_precedes(X1,X4,tptp0)
& subactivity_occurrence(X4,X0)
& occurrence_of(X4,tptp1) ) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f100,plain,
? [X0] :
( occurrence_of(X0,tptp0)
& ! [X1,X2] :
( sP0(X0,X1,X2)
| ( occurrence_of(X2,tptp1)
& ? [X3] :
( min_precedes(X1,X3,tptp0)
& subactivity_occurrence(X3,X0)
& occurrence_of(X3,tptp2) ) )
| ~ leaf_occ(X2,X0)
| ~ min_precedes(X1,X2,tptp0)
| ( ~ occurrence_of(X2,tptp2)
& ~ occurrence_of(X2,tptp1) )
| ~ root_occ(X1,X0)
| ~ occurrence_of(X1,tptp3) ) ),
inference(definition_folding,[],[f98,f99]) ).
fof(f126,plain,
! [X0,X1,X2] :
( ~ sP0(X0,X1,X2)
| ( occurrence_of(X2,tptp2)
& ? [X4] :
( min_precedes(X1,X4,tptp0)
& subactivity_occurrence(X4,X0)
& occurrence_of(X4,tptp1) ) ) ),
inference(nnf_transformation,[],[f99]) ).
fof(f127,plain,
! [X0,X1,X2] :
( ~ sP0(X0,X1,X2)
| ( occurrence_of(X2,tptp2)
& ? [X3] :
( min_precedes(X1,X3,tptp0)
& subactivity_occurrence(X3,X0)
& occurrence_of(X3,tptp1) ) ) ),
inference(rectify,[],[f126]) ).
fof(f128,plain,
! [X0,X1,X2] :
( ~ sP0(X0,X1,X2)
| ( occurrence_of(X2,tptp2)
& min_precedes(X1,sK18(X0,X1),tptp0)
& subactivity_occurrence(sK18(X0,X1),X0)
& occurrence_of(sK18(X0,X1),tptp1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X3,sK18(X0,X1))],[f127]) ).
fof(f213,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| occurrence_of(X2,tptp2) ),
inference(cnf_transformation,[],[f128]) ).
fof(f214,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| min_precedes(X1,sK18(X0,X1),tptp0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f215,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| subactivity_occurrence(sK18(X0,X1),X0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f216,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| occurrence_of(sK18(X0,X1),tptp1) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i,X2: $i] :
( occurrence_of(sK18(X0,X1),tptp1)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i,X2: $i] :
( subactivity_occurrence(sK18(X0,X1),X0)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i,X2: $i] :
( min_precedes(X1,sK18(X0,X1),tptp0)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_135,plain,
! [X0: $i,X1: $i,X2: $i] :
( occurrence_of(X2,tptp2)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_5282,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1,X2_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X2_iProver_min_precedes_1,tptp2)
| ~ sP0(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,X2_iProver_min_precedes_1) ),
inference(subtyping,[status(esa)],[c_135]) ).
tcf(c_5283,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1,X2_iProver_min_precedes_1: iProver_min_precedes_1] :
( min_precedes(X1_iProver_min_precedes_1,sK18(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1),tptp0)
| ~ sP0(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,X2_iProver_min_precedes_1) ),
inference(subtyping,[status(esa)],[c_134]) ).
tcf(c_5284,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1,X2_iProver_min_precedes_1: iProver_min_precedes_1] :
( subactivity_occurrence(sK18(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1),X0_iProver_min_precedes_1)
| ~ sP0(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,X2_iProver_min_precedes_1) ),
inference(subtyping,[status(esa)],[c_133]) ).
tcf(c_5285,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1,X1_iProver_min_precedes_1: iProver_min_precedes_1,X2_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(sK18(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1),tptp1)
| ~ sP0(X0_iProver_min_precedes_1,X1_iProver_min_precedes_1,X2_iProver_min_precedes_1) ),
inference(subtyping,[status(esa)],[c_132]) ).
tcf(c_29493,plain,
( subactivity_occurrence(sK18(sK19,sK15(sK19)),sK19)
| ~ sP0(sK19,sK15(sK19),sK17(sK19)) ),
inference(instantiation,[status(thm)],[c_5284]) ).
tcf(c_29494,plain,
( min_precedes(sK15(sK19),sK18(sK19,sK15(sK19)),tptp0)
| ~ sP0(sK19,sK15(sK19),sK17(sK19)) ),
inference(instantiation,[status(thm)],[c_5283]) ).
tcf(c_29495,plain,
( occurrence_of(sK18(sK19,sK15(sK19)),tptp1)
| ~ sP0(sK19,sK15(sK19),sK17(sK19)) ),
inference(instantiation,[status(thm)],[c_5285]) ).
tcf(c_29496,plain,
( occurrence_of(sK17(sK19),tptp2)
| ~ sP0(sK19,sK15(sK19),sK17(sK19)) ),
inference(instantiation,[status(thm)],[c_5282]) ).
tcf(c_60347,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( occurrence_of(X0_iProver_min_precedes_1,tptp2)
| min_precedes(sK16(sK19),sK20(sK15(sK19)),tptp0)
| ( sK20(sK15(sK19)) = sK16(sK19) )
| ~ leaf_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ arboreal(sK20(sK15(sK19)))
| ~ subactivity_occurrence(sK20(sK15(sK19)),sK19)
| ~ min_precedes(sK15(sK19),X0_iProver_min_precedes_1,tptp0) ),
inference(superposition,[status(thm)],[c_60134,c_5282]) ).
tcf(c_60637,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ~ min_precedes(sK20(sK15(sK19)),sK17(sK19),tptp0)
| ~ min_precedes(sK15(sK19),X0_iProver_min_precedes_1,tptp0)
| ~ subactivity_occurrence(sK20(sK15(sK19)),sK19)
| ~ arboreal(sK20(sK15(sK19)))
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ leaf_occ(X0_iProver_min_precedes_1,sK19)
| ( sK20(sK15(sK19)) = sK16(sK19) ) ),
inference(global_subsumption_just,[status(thm)],[c_60410,c_143,c_5286,c_6714,c_52198,c_60347]) ).
tcf(c_60638,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( sK20(sK15(sK19)) = sK16(sK19) )
| ~ leaf_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ arboreal(sK20(sK15(sK19)))
| ~ subactivity_occurrence(sK20(sK15(sK19)),sK19)
| ~ min_precedes(sK15(sK19),X0_iProver_min_precedes_1,tptp0)
| ~ min_precedes(sK20(sK15(sK19)),sK17(sK19),tptp0) ),
inference(renaming,[status(thm)],[c_60637]) ).
tcf(c_60647,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( ( sK20(sK15(sK19)) = sK16(sK19) )
| ~ leaf_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ subactivity_occurrence(sK20(sK15(sK19)),sK19)
| ~ min_precedes(sK15(sK19),X0_iProver_min_precedes_1,tptp0)
| ~ min_precedes(sK20(sK15(sK19)),sK17(sK19),tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_60638,c_40974]) ).
tcf(c_60665,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( min_precedes(sK17(sK19),sK20(sK15(sK19)),tptp0)
| ( sK20(sK15(sK19)) = sK17(sK19) )
| ( sK20(sK15(sK19)) = sK16(sK19) )
| ~ occurrence_of(sK19,tptp0)
| ~ leaf_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ arboreal(sK20(sK15(sK19)))
| ~ subactivity_occurrence(sK20(sK15(sK19)),sK19)
| ~ min_precedes(sK15(sK19),X0_iProver_min_precedes_1,tptp0) ),
inference(superposition,[status(thm)],[c_41853,c_60647]) ).
tcf(c_60668,plain,
! [X0_iProver_min_precedes_1: iProver_min_precedes_1] :
( min_precedes(sK17(sK19),sK20(sK15(sK19)),tptp0)
| ( sK20(sK15(sK19)) = sK17(sK19) )
| ( sK20(sK15(sK19)) = sK16(sK19) )
| ~ leaf_occ(X0_iProver_min_precedes_1,sK19)
| ~ occurrence_of(X0_iProver_min_precedes_1,tptp1)
| ~ arboreal(sK20(sK15(sK19)))
| ~ subactivity_occurrence(sK20(sK15(sK19)),sK19)
| ~ min_precedes(sK15(sK19),X0_iProver_min_precedes_1,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_60665,c_5274]) ).
tcf(c_61256,plain,
( min_precedes(sK17(sK19),sK15(sK19),tptp0)
| min_precedes(sK17(sK19),sK20(sK15(sK19)),tptp0)
| ( sK15(sK19) = sK17(sK19) )
| ( sK20(sK15(sK19)) = sK17(sK19) )
| ( sK20(sK15(sK19)) = sK16(sK19) )
| ~ arboreal(sK15(sK19))
| ~ occurrence_of(sK19,tptp0)
| ~ leaf_occ(sK17(sK19),sK19)
| ~ subactivity_occurrence(sK15(sK19),sK19)
| ~ arboreal(sK20(sK15(sK19)))
| ~ occurrence_of(sK17(sK19),tptp1)
| ~ subactivity_occurrence(sK20(sK15(sK19)),sK19) ),
inference(superposition,[status(thm)],[c_41853,c_60668]) ).
tcf(c_61264,plain,
( min_precedes(sK17(sK19),sK15(sK19),tptp0)
| min_precedes(sK17(sK19),sK20(sK15(sK19)),tptp0)
| ( sK15(sK19) = sK17(sK19) )
| ( sK20(sK15(sK19)) = sK17(sK19) )
| ( sK20(sK15(sK19)) = sK16(sK19) )
| ~ arboreal(sK20(sK15(sK19)))
| ~ occurrence_of(sK17(sK19),tptp1)
| ~ subactivity_occurrence(sK20(sK15(sK19)),sK19) ),
inference(forward_subsumption_resolution,[status(thm)],[c_61256,c_40481,c_5274,c_41547,c_42334]) ).
tcf(c_61472,plain,
( ~ occurrence_of(sK17(sK19),tptp1)
| ( sK20(sK15(sK19)) = sK16(sK19) )
| min_precedes(sK17(sK19),sK20(sK15(sK19)),tptp0) ),
inference(global_subsumption_just,[status(thm)],[c_61264,c_125,c_124,c_143,c_157,c_159,c_160,c_3502,c_3511,c_3520,c_4030,c_4039,c_4048,c_5286,c_7001,c_7050,c_7359,c_7481,c_8339,c_8911,c_9097,c_9444,c_9674,c_12691,c_12696,c_12957,c_18524,c_18523,c_20085,c_22484,c_29496,c_29625,c_60805,c_61264]) ).
tcf(c_61473,plain,
( min_precedes(sK17(sK19),sK20(sK15(sK19)),tptp0)
| ( sK20(sK15(sK19)) = sK16(sK19) )
| ~ occurrence_of(sK17(sK19),tptp1) ),
inference(renaming,[status(thm)],[c_61472]) ).
tcf(c_82350,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_82349,c_78234,c_76137,c_75677,c_73717,c_70498,c_70497,c_68502,c_68504,c_68505,c_65955,c_63200,c_61473,c_31252,c_29493,c_29494,c_29495,c_29496,c_22484,c_20900,c_20085,c_18521,c_12957,c_12696,c_12691,c_10217,c_9674,c_9436,c_9097,c_7481,c_7359,c_7118,c_7050,c_7001,c_5290,c_5289,c_5286,c_4048,c_4039,c_4030,c_3520,c_3511,c_3502,c_196,c_160,c_159,c_158,c_157,c_143,c_122,c_123,c_125]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO008+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.35 % Computer : n013.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 06:25:36 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.39 Running first-order theorem proving
% 0.12/0.39 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.40
% 0.12/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.40
% 0.12/0.40 % Detected problem language: tptp
% 0.12/0.42 % Proving...
% 84.06/12.43 % SZS status Started for theBenchmark.p
% 84.06/12.43 % SZS status Theorem for theBenchmark.p
% 84.06/12.43
% 84.06/12.43 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 84.06/12.43
% 84.06/12.43 % ------ iProver source info
% 84.06/12.43
% 84.06/12.43 % git: date: 2026-07-19 20:42:38 +0200
% 84.06/12.43 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 84.06/12.43 % git: non_committed_changes: false
% 84.06/12.43
% 84.06/12.43 % ------ Parsing...
% 84.06/12.43 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 84.06/12.43
% 84.06/12.43 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e %
% 84.06/12.43
% 84.06/12.43 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 84.06/12.43
% 84.06/12.43 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 84.06/12.43 % ------ Proving...
% 84.06/12.43 % ------ Problem Properties
% 84.06/12.43
% 84.06/12.43 %
% 84.06/12.43 % clauses 95
% 84.06/12.43 % conjectures 8
% 84.06/12.43 % EPR 48
% 84.06/12.43 % Horn 76
% 84.06/12.43 % unary 13
% 84.06/12.43 % binary 46
% 84.06/12.43 % lits 260
% 84.06/12.43 % lits eq 9
% 84.06/12.43 % fd_pure 0
% 84.06/12.43 % fd_pseudo 0
% 84.06/12.43 % fd_cond 0
% 84.06/12.43 % fd_pseudo_cond 3
% 84.06/12.43 % AC symbols 0
% 84.06/12.43
% 84.06/12.43 % ------ Input Options Time Limit: Unbounded
% 84.06/12.43
% 84.06/12.43
% 84.06/12.43 % ------
% 84.06/12.43 % Current options:
% 84.06/12.43 % ------
% 84.06/12.43
% 84.06/12.43
% 84.06/12.43 %
% 84.06/12.43
% 84.06/12.43 % ------ Proving...
% 84.06/12.43 %
% 84.06/12.43
% 84.06/12.43 % SZS status Theorem for theBenchmark.p
% 84.06/12.43
% 84.06/12.43 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 84.06/12.44
% 84.06/12.44
%------------------------------------------------------------------------------