%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : PRO016+3 : 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 : n017.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:38 PM UTC 2026
% Result : Theorem 106.94s 16.38s
% Output : CNFRefutation 106.94s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f143ERROR: Could not build tree for root c_85723ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
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(f16,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> precedes(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_15) ).
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(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(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(f38,axiom,
! [X0,X1,X2] :
( ( leaf_occ(X1,X0)
& occurrence_of(X0,X2) )
=> ~ ? [X3] : min_precedes(X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_37) ).
fof(f44,axiom,
! [X0,X1,X2,X3] :
( ( ~ min_precedes(X2,X3,X0)
& arboreal(X2)
& leaf_occ(X3,X1)
& subactivity_occurrence(X2,X1)
& occurrence_of(X1,X0) )
=> X3 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_43) ).
fof(f50,axiom,
! [X0,X1] :
( ( ~ leaf_occ(X0,X1)
& arboreal(X0)
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,tptp0) )
=> ? [X2,X3,X4] :
( leaf_occ(X4,X1)
& next_subocc(X3,X4,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& next_subocc(X2,X3,tptp0)
& occurrence_of(X3,tptp4)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X2,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_49) ).
fof(f56,axiom,
atomic(tptp3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_55) ).
fof(f76,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ( arboreal(X0)
<=> atomic(X1) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f77,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f84,plain,
! [X0,X1,X2] :
( ~ min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(ennf_transformation,[],[f16]) ).
fof(f94,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,[],[f23]) ).
fof(f103,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(f104,plain,
! [X0,X1,X2,X3] :
( ~ subactivity_occurrence(X1,X3)
| ~ occurrence_of(X3,X2)
| ~ min_precedes(X0,X1,X2)
| subactivity_occurrence(X0,X3) ),
inference(flattening,[],[f103]) ).
fof(f116,plain,
! [X0,X1,X2] :
( ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,X2)
| ! [X3] : ~ min_precedes(X1,X3,X2) ),
inference(ennf_transformation,[],[f38]) ).
fof(f117,plain,
! [X0,X1,X2] :
( ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,X2)
| ! [X3] : ~ min_precedes(X1,X3,X2) ),
inference(flattening,[],[f116]) ).
fof(f128,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X3,X0)
| ~ arboreal(X2)
| ~ leaf_occ(X3,X1)
| ~ subactivity_occurrence(X2,X1)
| ~ occurrence_of(X1,X0)
| X3 = X2 ),
inference(ennf_transformation,[],[f44]) ).
fof(f129,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X3,X0)
| ~ arboreal(X2)
| ~ leaf_occ(X3,X1)
| ~ subactivity_occurrence(X2,X1)
| ~ occurrence_of(X1,X0)
| X3 = X2 ),
inference(flattening,[],[f128]) ).
fof(f138,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ? [X2,X3,X4] :
( leaf_occ(X4,X1)
& next_subocc(X3,X4,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& next_subocc(X2,X3,tptp0)
& occurrence_of(X3,tptp4)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X2,tptp3) ) ),
inference(ennf_transformation,[],[f50]) ).
fof(f139,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ? [X2,X3,X4] :
( leaf_occ(X4,X1)
& next_subocc(X3,X4,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& next_subocc(X2,X3,tptp0)
& occurrence_of(X3,tptp4)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X2,tptp3) ) ),
inference(flattening,[],[f138]) ).
fof(f145,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ( ( ~ arboreal(X0)
| atomic(X1) )
& ( ~ atomic(X1)
| arboreal(X0) ) ) ),
inference(nnf_transformation,[],[f76]) ).
fof(f146,plain,
! [X0,X1] :
( ( ~ precedes(X0,X1)
| ( legal(X1)
& earlier(X0,X1) ) )
& ( ~ legal(X1)
| ~ earlier(X0,X1)
| precedes(X0,X1) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f147,plain,
! [X0,X1] :
( ( ~ precedes(X0,X1)
| ( legal(X1)
& earlier(X0,X1) ) )
& ( ~ legal(X1)
| ~ earlier(X0,X1)
| precedes(X0,X1) ) ),
inference(flattening,[],[f146]) ).
fof(f155,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) ) )
& ( ? [X3] :
( min_precedes(X3,X1,X2)
& min_precedes(X0,X3,X2) )
| ~ min_precedes(X0,X1,X2)
| next_subocc(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f94]) ).
fof(f156,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) ) )
& ( ? [X3] :
( min_precedes(X3,X1,X2)
& min_precedes(X0,X3,X2) )
| ~ min_precedes(X0,X1,X2)
| next_subocc(X0,X1,X2) ) ),
inference(flattening,[],[f155]) ).
fof(f157,plain,
! [X0,X1,X2] :
( ( ~ next_subocc(X0,X1,X2)
| ( ! [X4] :
( ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) )
& min_precedes(X0,X1,X2) ) )
& ( ? [X3] :
( min_precedes(X3,X1,X2)
& min_precedes(X0,X3,X2) )
| ~ min_precedes(X0,X1,X2)
| next_subocc(X0,X1,X2) ) ),
inference(rectify,[],[f156]) ).
fof(f158,plain,
! [X0,X1,X2] :
( ( ~ next_subocc(X0,X1,X2)
| ( ! [X4] :
( ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) )
& min_precedes(X0,X1,X2) ) )
& ( ( min_precedes(sK8(X0,X1,X2),X1,X2)
& min_precedes(X0,sK8(X0,X1,X2),X2) )
| ~ min_precedes(X0,X1,X2)
| next_subocc(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X3,sK8(X0,X1,X2))],[f157]) ).
fof(f166,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(f167,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,[],[f166]) ).
fof(f168,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))],[f167]) ).
fof(f170,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ( leaf_occ(sK18(X0,X1),X1)
& next_subocc(sK17(X0,X1),sK18(X0,X1),tptp0)
& ( occurrence_of(sK18(X0,X1),tptp2)
| occurrence_of(sK18(X0,X1),tptp1) )
& next_subocc(sK16(X0,X1),sK17(X0,X1),tptp0)
& occurrence_of(sK17(X0,X1),tptp4)
& next_subocc(X0,sK16(X0,X1),tptp0)
& occurrence_of(sK16(X0,X1),tptp3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18]),skolemize(X2,sK16(X0,X1)),skolemize(X3,sK17(X0,X1)),skolemize(X4,sK18(X0,X1))],[f139]) ).
fof(f174,plain,
( ~ leaf_occ(sK20,sK21)
& arboreal(sK20)
& subactivity_occurrence(sK20,sK21)
& occurrence_of(sK21,tptp0)
& ! [X2,X3] :
( sP0(X2,X3)
| ( occurrence_of(X3,tptp1)
& min_precedes(X2,sK22(X2),tptp0)
& occurrence_of(sK22(X2),tptp2) )
| ~ leaf_occ(X3,sK21)
| ~ min_precedes(X2,X3,tptp0)
| ( ~ occurrence_of(X3,tptp2)
& ~ occurrence_of(X3,tptp1) )
| ~ next_subocc(sK20,X2,tptp0)
| ~ occurrence_of(X2,tptp3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22]),skolemize(X0,sK20),skolemize(X1,sK21),skolemize(X4,sK22(X2))],[f143]) ).
fof(f185,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f186,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f188,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| legal(X1) ),
inference(cnf_transformation,[],[f147]) ).
fof(f200,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(cnf_transformation,[],[f84]) ).
fof(f210,plain,
! [X2,X0,X1,X4] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) ),
inference(cnf_transformation,[],[f158]) ).
fof(f211,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f158]) ).
fof(f228,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,[],[f104]) ).
fof(f235,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
fof(f240,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,X2)
| ~ min_precedes(X1,X3,X2) ),
inference(cnf_transformation,[],[f117]) ).
fof(f246,plain,
! [X2,X3,X0,X1] :
( min_precedes(X2,X3,X0)
| ~ arboreal(X2)
| ~ leaf_occ(X3,X1)
| ~ subactivity_occurrence(X2,X1)
| ~ occurrence_of(X1,X0)
| X2 = X3 ),
inference(cnf_transformation,[],[f129]) ).
fof(f254,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| leaf_occ(sK18(X0,X1),X1) ),
inference(cnf_transformation,[],[f170]) ).
fof(f255,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(sK17(X0,X1),sK18(X0,X1),tptp0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f257,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(sK16(X0,X1),sK17(X0,X1),tptp0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f259,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(X0,sK16(X0,X1),tptp0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f260,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK16(X0,X1),tptp3) ),
inference(cnf_transformation,[],[f170]) ).
fof(f266,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f56]) ).
fof(f276,plain,
~ leaf_occ(sK20,sK21),
inference(cnf_transformation,[],[f174]) ).
fof(f277,plain,
arboreal(sK20),
inference(cnf_transformation,[],[f174]) ).
fof(f278,plain,
subactivity_occurrence(sK20,sK21),
inference(cnf_transformation,[],[f174]) ).
fof(f279,plain,
occurrence_of(sK21,tptp0),
inference(cnf_transformation,[],[f174]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( arboreal(X0)
| ~ atomic(X1)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[],[f185]) ).
tcf(c_60,plain,
! [X0: $i] :
( arboreal(X0)
| ~ legal(X0) ),
inference(cnf_transformation,[],[f186]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] :
( legal(X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i,X2: $i] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i,X2: $i] :
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[],[f211]) ).
tcf(c_87,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,[],[f210]) ).
tcf(c_102,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,[],[f228]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i] :
( subactivity_occurrence(X0,X1)
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f235]) ).
tcf(c_114,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ leaf_occ(X0,X3)
| ~ occurrence_of(X3,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f240]) ).
tcf(c_120,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( min_precedes(X2,X3,X1)
| ( X2 = X3 )
| ~ arboreal(X2)
| ~ leaf_occ(X3,X0)
| ~ subactivity_occurrence(X2,X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[],[f246]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i] :
( leaf_occ(X0,X1)
| occurrence_of(sK16(X0,X1),tptp3)
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f260]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i] :
( leaf_occ(X0,X1)
| next_subocc(X0,sK16(X0,X1),tptp0)
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f259]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i] :
( leaf_occ(X0,X1)
| next_subocc(sK16(X0,X1),sK17(X0,X1),tptp0)
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f257]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i] :
( leaf_occ(X0,X1)
| next_subocc(sK17(X0,X1),sK18(X0,X1),tptp0)
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f255]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i] :
( leaf_occ(X0,X1)
| leaf_occ(sK18(X0,X1),X1)
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f254]) ).
tcf(c_140,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f266]) ).
tcf(c_155,negated_conjecture,
occurrence_of(sK21,tptp0),
inference(cnf_transformation,[],[f279]) ).
tcf(c_156,negated_conjecture,
subactivity_occurrence(sK20,sK21),
inference(cnf_transformation,[],[f278]) ).
tcf(c_157,negated_conjecture,
arboreal(sK20),
inference(cnf_transformation,[],[f277]) ).
tcf(c_158,negated_conjecture,
~ leaf_occ(sK20,sK21),
inference(cnf_transformation,[],[f276]) ).
tcf(c_273,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2)
| leaf_occ(sK18(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2),X1_iProver_leaf_occ_2)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(X1_iProver_leaf_occ_2,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2) ),
inference(subtyping,[status(esa)],[c_134]) ).
tcf(c_274,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2)
| next_subocc(sK17(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2),sK18(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2),tptp0)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(X1_iProver_leaf_occ_2,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2) ),
inference(subtyping,[status(esa)],[c_133]) ).
tcf(c_276,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2)
| next_subocc(sK16(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2),sK17(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2),tptp0)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(X1_iProver_leaf_occ_2,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2) ),
inference(subtyping,[status(esa)],[c_131]) ).
tcf(c_278,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2)
| next_subocc(X0_iProver_leaf_occ_2,sK16(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2),tptp0)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(X1_iProver_leaf_occ_2,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2) ),
inference(subtyping,[status(esa)],[c_129]) ).
tcf(c_279,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2)
| occurrence_of(sK16(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2),tptp3)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(X1_iProver_leaf_occ_2,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2) ),
inference(subtyping,[status(esa)],[c_128]) ).
tcf(c_287,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X0_iProver_occurrence_of_2: iProver_occurrence_of_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2,X2_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(X1_iProver_leaf_occ_2,X2_iProver_leaf_occ_2,X0_iProver_occurrence_of_2)
| ( X1_iProver_leaf_occ_2 = X2_iProver_leaf_occ_2 )
| ~ arboreal(X1_iProver_leaf_occ_2)
| ~ leaf_occ(X2_iProver_leaf_occ_2,X0_iProver_leaf_occ_2)
| ~ subactivity_occurrence(X1_iProver_leaf_occ_2,X0_iProver_leaf_occ_2)
| ~ occurrence_of(X0_iProver_leaf_occ_2,X0_iProver_occurrence_of_2) ),
inference(subtyping,[status(esa)],[c_120]) ).
tcf(c_293,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X0_iProver_occurrence_of_2: iProver_occurrence_of_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2,X2_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ~ leaf_occ(X0_iProver_leaf_occ_2,X2_iProver_leaf_occ_2)
| ~ occurrence_of(X2_iProver_leaf_occ_2,X0_iProver_occurrence_of_2)
| ~ min_precedes(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2,X0_iProver_occurrence_of_2) ),
inference(subtyping,[status(esa)],[c_114]) ).
tcf(c_297,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2)
| ~ leaf_occ(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2) ),
inference(subtyping,[status(esa)],[c_110]) ).
tcf(c_305,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X0_iProver_occurrence_of_2: iProver_occurrence_of_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2,X2_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(X0_iProver_leaf_occ_2,X2_iProver_leaf_occ_2)
| ~ subactivity_occurrence(X1_iProver_leaf_occ_2,X2_iProver_leaf_occ_2)
| ~ occurrence_of(X2_iProver_leaf_occ_2,X0_iProver_occurrence_of_2)
| ~ min_precedes(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2,X0_iProver_occurrence_of_2) ),
inference(subtyping,[status(esa)],[c_102]) ).
tcf(c_320,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X0_iProver_occurrence_of_2: iProver_occurrence_of_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2,X2_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ~ next_subocc(X0_iProver_leaf_occ_2,X2_iProver_leaf_occ_2,X0_iProver_occurrence_of_2)
| ~ min_precedes(X1_iProver_leaf_occ_2,X2_iProver_leaf_occ_2,X0_iProver_occurrence_of_2)
| ~ min_precedes(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2,X0_iProver_occurrence_of_2) ),
inference(subtyping,[status(esa)],[c_87]) ).
tcf(c_321,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X0_iProver_occurrence_of_2: iProver_occurrence_of_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2,X0_iProver_occurrence_of_2)
| ~ next_subocc(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2,X0_iProver_occurrence_of_2) ),
inference(subtyping,[status(esa)],[c_86]) ).
tcf(c_333,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X0_iProver_occurrence_of_2: iProver_occurrence_of_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( precedes(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2)
| ~ min_precedes(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2,X0_iProver_occurrence_of_2) ),
inference(subtyping,[status(esa)],[c_74]) ).
tcf(c_343,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( legal(X1_iProver_leaf_occ_2)
| ~ precedes(X0_iProver_leaf_occ_2,X1_iProver_leaf_occ_2) ),
inference(subtyping,[status(esa)],[c_64]) ).
tcf(c_347,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( arboreal(X0_iProver_leaf_occ_2)
| ~ legal(X0_iProver_leaf_occ_2) ),
inference(subtyping,[status(esa)],[c_60]) ).
tcf(c_349,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X0_iProver_occurrence_of_2: iProver_occurrence_of_2] :
( arboreal(X0_iProver_leaf_occ_2)
| ~ atomic(X0_iProver_occurrence_of_2)
| ~ occurrence_of(X0_iProver_leaf_occ_2,X0_iProver_occurrence_of_2) ),
inference(subtyping,[status(esa)],[c_58]) ).
tcf(c_360,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] : X0_iProver_leaf_occ_2 = X0_iProver_leaf_occ_2,
theory(equality) ).
tcf(c_375,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2,X2_iProver_leaf_occ_2: iProver_leaf_occ_2,X3_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,X2_iProver_leaf_occ_2)
| ~ leaf_occ(X1_iProver_leaf_occ_2,X3_iProver_leaf_occ_2)
| ( X2_iProver_leaf_occ_2 != X3_iProver_leaf_occ_2 )
| ( X0_iProver_leaf_occ_2 != X1_iProver_leaf_occ_2 ) ),
theory(equality) ).
tcf(c_492,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,sK21)
| occurrence_of(sK16(X0_iProver_leaf_occ_2,sK21),tptp3)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,sK21) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_498,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,sK21)
| leaf_occ(sK18(X0_iProver_leaf_occ_2,sK21),sK21)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,sK21) ),
inference(instantiation,[status(thm)],[c_273]) ).
tcf(c_499,plain,
( leaf_occ(sK20,sK21)
| leaf_occ(sK18(sK20,sK21),sK21)
| ~ arboreal(sK20)
| ~ subactivity_occurrence(sK20,sK21)
| ~ occurrence_of(sK21,tptp0) ),
inference(instantiation,[status(thm)],[c_498]) ).
tcf(c_500,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,sK21)
| next_subocc(X0_iProver_leaf_occ_2,sK16(X0_iProver_leaf_occ_2,sK21),tptp0)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,sK21) ),
inference(instantiation,[status(thm)],[c_278]) ).
tcf(c_502,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,sK21)
| next_subocc(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,sK21) ),
inference(instantiation,[status(thm)],[c_274]) ).
tcf(c_503,plain,
( leaf_occ(sK20,sK21)
| next_subocc(sK17(sK20,sK21),sK18(sK20,sK21),tptp0)
| ~ arboreal(sK20)
| ~ subactivity_occurrence(sK20,sK21)
| ~ occurrence_of(sK21,tptp0) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_506,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,sK21)
| next_subocc(sK16(X0_iProver_leaf_occ_2,sK21),sK17(X0_iProver_leaf_occ_2,sK21),tptp0)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,sK21) ),
inference(instantiation,[status(thm)],[c_276]) ).
tcf(c_507,plain,
( leaf_occ(sK20,sK21)
| next_subocc(sK16(sK20,sK21),sK17(sK20,sK21),tptp0)
| ~ arboreal(sK20)
| ~ subactivity_occurrence(sK20,sK21)
| ~ occurrence_of(sK21,tptp0) ),
inference(instantiation,[status(thm)],[c_506]) ).
tcf(c_699,plain,
sK21 = sK21,
inference(instantiation,[status(thm)],[c_360]) ).
tcf(c_807,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(sK18(X0_iProver_leaf_occ_2,sK21),sK21)
| ~ leaf_occ(sK18(X0_iProver_leaf_occ_2,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_808,plain,
( subactivity_occurrence(sK18(sK20,sK21),sK21)
| ~ leaf_occ(sK18(sK20,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_823,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(X0_iProver_leaf_occ_2,sK16(X0_iProver_leaf_occ_2,sK21),tptp0)
| ~ next_subocc(X0_iProver_leaf_occ_2,sK16(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_877,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0)
| ~ next_subocc(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_878,plain,
( min_precedes(sK17(sK20,sK21),sK18(sK20,sK21),tptp0)
| ~ next_subocc(sK17(sK20,sK21),sK18(sK20,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_877]) ).
tcf(c_879,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ~ min_precedes(X1_iProver_leaf_occ_2,sK18(X0_iProver_leaf_occ_2,sK21),tptp0)
| ~ min_precedes(sK17(X0_iProver_leaf_occ_2,sK21),X1_iProver_leaf_occ_2,tptp0)
| ~ next_subocc(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_320]) ).
tcf(c_895,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(sK16(X0_iProver_leaf_occ_2,sK21),sK17(X0_iProver_leaf_occ_2,sK21),tptp0)
| ~ next_subocc(sK16(X0_iProver_leaf_occ_2,sK21),sK17(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_896,plain,
( min_precedes(sK16(sK20,sK21),sK17(sK20,sK21),tptp0)
| ~ next_subocc(sK16(sK20,sK21),sK17(sK20,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_895]) ).
tcf(c_1550,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(sK17(X0_iProver_leaf_occ_2,sK21),X1_iProver_leaf_occ_2)
| ~ occurrence_of(X1_iProver_leaf_occ_2,tptp0)
| ~ subactivity_occurrence(sK18(X0_iProver_leaf_occ_2,sK21),X1_iProver_leaf_occ_2)
| ~ min_precedes(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_1595,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(sK16(X0_iProver_leaf_occ_2,sK21),X1_iProver_leaf_occ_2)
| ~ occurrence_of(X1_iProver_leaf_occ_2,tptp0)
| ~ subactivity_occurrence(sK17(X0_iProver_leaf_occ_2,sK21),X1_iProver_leaf_occ_2)
| ~ min_precedes(sK16(X0_iProver_leaf_occ_2,sK21),sK17(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_1605,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( precedes(sK16(X0_iProver_leaf_occ_2,sK21),sK17(X0_iProver_leaf_occ_2,sK21))
| ~ min_precedes(sK16(X0_iProver_leaf_occ_2,sK21),sK17(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_333]) ).
tcf(c_1607,plain,
( precedes(sK16(sK20,sK21),sK17(sK20,sK21))
| ~ min_precedes(sK16(sK20,sK21),sK17(sK20,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_1605]) ).
tcf(c_1649,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X0_iProver_occurrence_of_2: iProver_occurrence_of_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2,X2_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(X2_iProver_leaf_occ_2,sK18(X0_iProver_leaf_occ_2,sK21),X0_iProver_occurrence_of_2)
| ( X2_iProver_leaf_occ_2 = sK18(X0_iProver_leaf_occ_2,sK21) )
| ~ arboreal(X2_iProver_leaf_occ_2)
| ~ subactivity_occurrence(X2_iProver_leaf_occ_2,X1_iProver_leaf_occ_2)
| ~ occurrence_of(X1_iProver_leaf_occ_2,X0_iProver_occurrence_of_2)
| ~ leaf_occ(sK18(X0_iProver_leaf_occ_2,sK21),X1_iProver_leaf_occ_2) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_2861,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( legal(sK17(X0_iProver_leaf_occ_2,sK21))
| ~ precedes(sK16(X0_iProver_leaf_occ_2,sK21),sK17(X0_iProver_leaf_occ_2,sK21)) ),
inference(instantiation,[status(thm)],[c_343]) ).
tcf(c_2862,plain,
( legal(sK17(sK20,sK21))
| ~ precedes(sK16(sK20,sK21),sK17(sK20,sK21)) ),
inference(instantiation,[status(thm)],[c_2861]) ).
tcf(c_3443,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(sK17(X0_iProver_leaf_occ_2,sK21),sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(sK18(X0_iProver_leaf_occ_2,sK21),sK21)
| ~ min_precedes(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_1550]) ).
tcf(c_3444,plain,
( subactivity_occurrence(sK17(sK20,sK21),sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(sK18(sK20,sK21),sK21)
| ~ min_precedes(sK17(sK20,sK21),sK18(sK20,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_3443]) ).
tcf(c_3460,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(sK16(X0_iProver_leaf_occ_2,sK21),sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(sK17(X0_iProver_leaf_occ_2,sK21),sK21)
| ~ min_precedes(sK16(X0_iProver_leaf_occ_2,sK21),sK17(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_1595]) ).
tcf(c_3545,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(sK17(X0_iProver_leaf_occ_2,sK21),sK21)
| next_subocc(sK17(X0_iProver_leaf_occ_2,sK21),sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ arboreal(sK17(X0_iProver_leaf_occ_2,sK21))
| ~ subactivity_occurrence(sK17(X0_iProver_leaf_occ_2,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_500]) ).
tcf(c_3547,plain,
( leaf_occ(sK17(sK20,sK21),sK21)
| next_subocc(sK17(sK20,sK21),sK16(sK17(sK20,sK21),sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ arboreal(sK17(sK20,sK21))
| ~ subactivity_occurrence(sK17(sK20,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_3545]) ).
tcf(c_3773,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X0_iProver_occurrence_of_2: iProver_occurrence_of_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(X1_iProver_leaf_occ_2,sK18(X0_iProver_leaf_occ_2,sK21),X0_iProver_occurrence_of_2)
| ( X1_iProver_leaf_occ_2 = sK18(X0_iProver_leaf_occ_2,sK21) )
| ~ arboreal(X1_iProver_leaf_occ_2)
| ~ subactivity_occurrence(X1_iProver_leaf_occ_2,sK21)
| ~ occurrence_of(sK21,X0_iProver_occurrence_of_2)
| ~ leaf_occ(sK18(X0_iProver_leaf_occ_2,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_1649]) ).
tcf(c_3839,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( arboreal(sK17(X0_iProver_leaf_occ_2,sK21))
| ~ legal(sK17(X0_iProver_leaf_occ_2,sK21)) ),
inference(instantiation,[status(thm)],[c_347]) ).
tcf(c_3840,plain,
( arboreal(sK17(sK20,sK21))
| ~ legal(sK17(sK20,sK21)) ),
inference(instantiation,[status(thm)],[c_3839]) ).
tcf(c_4198,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(X1_iProver_leaf_occ_2,sK18(X0_iProver_leaf_occ_2,sK21),tptp0)
| ( X1_iProver_leaf_occ_2 = sK18(X0_iProver_leaf_occ_2,sK21) )
| ~ arboreal(X1_iProver_leaf_occ_2)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X1_iProver_leaf_occ_2,sK21)
| ~ leaf_occ(sK18(X0_iProver_leaf_occ_2,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_3773]) ).
tcf(c_4203,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ~ next_subocc(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0)
| ~ min_precedes(sK17(X0_iProver_leaf_occ_2,sK21),sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp0)
| ~ min_precedes(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_879]) ).
tcf(c_4204,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(sK17(X0_iProver_leaf_occ_2,sK21),sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp0)
| ~ next_subocc(sK17(X0_iProver_leaf_occ_2,sK21),sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_823]) ).
tcf(c_4205,plain,
( ~ next_subocc(sK17(sK20,sK21),sK18(sK20,sK21),tptp0)
| ~ min_precedes(sK17(sK20,sK21),sK16(sK17(sK20,sK21),sK21),tptp0)
| ~ min_precedes(sK16(sK17(sK20,sK21),sK21),sK18(sK20,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_4203]) ).
tcf(c_4206,plain,
( min_precedes(sK17(sK20,sK21),sK16(sK17(sK20,sK21),sK21),tptp0)
| ~ next_subocc(sK17(sK20,sK21),sK16(sK17(sK20,sK21),sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_4204]) ).
tcf(c_9996,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(sK16(X0_iProver_leaf_occ_2,sK21),sK18(X1_iProver_leaf_occ_2,sK21),tptp0)
| ( sK16(X0_iProver_leaf_occ_2,sK21) = sK18(X1_iProver_leaf_occ_2,sK21) )
| ~ occurrence_of(sK21,tptp0)
| ~ arboreal(sK16(X0_iProver_leaf_occ_2,sK21))
| ~ leaf_occ(sK18(X1_iProver_leaf_occ_2,sK21),sK21)
| ~ subactivity_occurrence(sK16(X0_iProver_leaf_occ_2,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_4198]) ).
tcf(c_16676,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(sK17(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK21)
| ~ min_precedes(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK17(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_3460]) ).
tcf(c_16677,plain,
( subactivity_occurrence(sK16(sK17(sK20,sK21),sK21),sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(sK17(sK17(sK20,sK21),sK21),sK21)
| ~ min_precedes(sK16(sK17(sK20,sK21),sK21),sK17(sK17(sK20,sK21),sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_16676]) ).
tcf(c_20278,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK17(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp0)
| ~ next_subocc(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK17(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_895]) ).
tcf(c_20279,plain,
( min_precedes(sK16(sK17(sK20,sK21),sK21),sK17(sK17(sK20,sK21),sK21),tptp0)
| ~ next_subocc(sK16(sK17(sK20,sK21),sK21),sK17(sK17(sK20,sK21),sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_20278]) ).
tcf(c_23113,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(sK17(X0_iProver_leaf_occ_2,sK21),sK21)
| occurrence_of(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp3)
| ~ occurrence_of(sK21,tptp0)
| ~ arboreal(sK17(X0_iProver_leaf_occ_2,sK21))
| ~ subactivity_occurrence(sK17(X0_iProver_leaf_occ_2,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_492]) ).
tcf(c_23115,plain,
( leaf_occ(sK17(sK20,sK21),sK21)
| occurrence_of(sK16(sK17(sK20,sK21),sK21),tptp3)
| ~ occurrence_of(sK21,tptp0)
| ~ arboreal(sK17(sK20,sK21))
| ~ subactivity_occurrence(sK17(sK20,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_23113]) ).
tcf(c_26597,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(sK17(X0_iProver_leaf_occ_2,sK21),sK21)
| next_subocc(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK17(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ arboreal(sK17(X0_iProver_leaf_occ_2,sK21))
| ~ subactivity_occurrence(sK17(X0_iProver_leaf_occ_2,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_506]) ).
tcf(c_26598,plain,
( leaf_occ(sK17(sK20,sK21),sK21)
| next_subocc(sK16(sK17(sK20,sK21),sK21),sK17(sK17(sK20,sK21),sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ arboreal(sK17(sK20,sK21))
| ~ subactivity_occurrence(sK17(sK20,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_26597]) ).
tcf(c_28057,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0)
| ( sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21) = sK18(X0_iProver_leaf_occ_2,sK21) )
| ~ occurrence_of(sK21,tptp0)
| ~ leaf_occ(sK18(X0_iProver_leaf_occ_2,sK21),sK21)
| ~ arboreal(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21))
| ~ subactivity_occurrence(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK21) ),
inference(instantiation,[status(thm)],[c_9996]) ).
tcf(c_28058,plain,
( min_precedes(sK16(sK17(sK20,sK21),sK21),sK18(sK20,sK21),tptp0)
| ( sK16(sK17(sK20,sK21),sK21) = sK18(sK20,sK21) )
| ~ occurrence_of(sK21,tptp0)
| ~ leaf_occ(sK18(sK20,sK21),sK21)
| ~ arboreal(sK16(sK17(sK20,sK21),sK21))
| ~ subactivity_occurrence(sK16(sK17(sK20,sK21),sK21),sK21) ),
inference(instantiation,[status(thm)],[c_28057]) ).
tcf(c_30643,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2,X2_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,sK21)
| ~ leaf_occ(X1_iProver_leaf_occ_2,X2_iProver_leaf_occ_2)
| ( sK21 != X2_iProver_leaf_occ_2 )
| ( X0_iProver_leaf_occ_2 != X1_iProver_leaf_occ_2 ) ),
inference(instantiation,[status(thm)],[c_375]) ).
tcf(c_30644,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,sK21)
| leaf_occ(sK18(X0_iProver_leaf_occ_2,sK21),sK21)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,sK21) ),
inference(instantiation,[status(thm)],[c_273]) ).
tcf(c_30651,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,sK21)
| next_subocc(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,sK21) ),
inference(instantiation,[status(thm)],[c_274]) ).
tcf(c_30733,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0)
| ~ next_subocc(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_321]) ).
tcf(c_31011,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,sK21)
| ~ leaf_occ(X1_iProver_leaf_occ_2,sK21)
| ( sK21 != sK21 )
| ( X0_iProver_leaf_occ_2 != X1_iProver_leaf_occ_2 ) ),
inference(instantiation,[status(thm)],[c_30643]) ).
tcf(c_31146,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ~ occurrence_of(X1_iProver_leaf_occ_2,tptp0)
| ~ leaf_occ(sK17(X0_iProver_leaf_occ_2,sK21),X1_iProver_leaf_occ_2)
| ~ min_precedes(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_293]) ).
tcf(c_31164,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ~ occurrence_of(X1_iProver_leaf_occ_2,tptp0)
| ~ leaf_occ(sK16(X0_iProver_leaf_occ_2,sK21),X1_iProver_leaf_occ_2)
| ~ min_precedes(sK16(X0_iProver_leaf_occ_2,sK21),sK17(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_293]) ).
tcf(c_32350,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(sK18(X0_iProver_leaf_occ_2,sK21),sK21)
| ~ leaf_occ(sK18(X0_iProver_leaf_occ_2,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_32386,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(sK17(X0_iProver_leaf_occ_2,sK21),X1_iProver_leaf_occ_2)
| ~ occurrence_of(X1_iProver_leaf_occ_2,tptp0)
| ~ subactivity_occurrence(sK18(X0_iProver_leaf_occ_2,sK21),X1_iProver_leaf_occ_2)
| ~ min_precedes(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_32784,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,sK21)
| ~ leaf_occ(sK18(X1_iProver_leaf_occ_2,sK21),sK21)
| ( sK21 != sK21 )
| ( X0_iProver_leaf_occ_2 != sK18(X1_iProver_leaf_occ_2,sK21) ) ),
inference(instantiation,[status(thm)],[c_31011]) ).
tcf(c_33631,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ~ occurrence_of(sK21,tptp0)
| ~ leaf_occ(sK17(X0_iProver_leaf_occ_2,sK21),sK21)
| ~ min_precedes(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_31146]) ).
tcf(c_33632,plain,
( ~ occurrence_of(sK21,tptp0)
| ~ leaf_occ(sK17(sK20,sK21),sK21)
| ~ min_precedes(sK17(sK20,sK21),sK18(sK20,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_33631]) ).
tcf(c_33698,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ~ occurrence_of(sK21,tptp0)
| ~ leaf_occ(sK16(X0_iProver_leaf_occ_2,sK21),sK21)
| ~ min_precedes(sK16(X0_iProver_leaf_occ_2,sK21),sK17(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_31164]) ).
tcf(c_34053,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(sK17(X0_iProver_leaf_occ_2,sK21),sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(sK18(X0_iProver_leaf_occ_2,sK21),sK21)
| ~ min_precedes(sK17(X0_iProver_leaf_occ_2,sK21),sK18(X0_iProver_leaf_occ_2,sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_32386]) ).
tcf(c_52363,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X0_iProver_occurrence_of_2: iProver_occurrence_of_2] :
( arboreal(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21))
| ~ atomic(X0_iProver_occurrence_of_2)
| ~ occurrence_of(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),X0_iProver_occurrence_of_2) ),
inference(instantiation,[status(thm)],[c_349]) ).
tcf(c_63711,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(sK17(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(sK18(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK21)
| ~ min_precedes(sK17(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK18(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_34053]) ).
tcf(c_63712,plain,
( subactivity_occurrence(sK17(sK17(sK20,sK21),sK21),sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(sK18(sK17(sK20,sK21),sK21),sK21)
| ~ min_precedes(sK17(sK17(sK20,sK21),sK21),sK18(sK17(sK20,sK21),sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_63711]) ).
tcf(c_68982,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( arboreal(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21))
| ~ atomic(tptp3)
| ~ occurrence_of(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp3) ),
inference(instantiation,[status(thm)],[c_52363]) ).
tcf(c_68985,plain,
( arboreal(sK16(sK17(sK20,sK21),sK21))
| ~ atomic(tptp3)
| ~ occurrence_of(sK16(sK17(sK20,sK21),sK21),tptp3) ),
inference(instantiation,[status(thm)],[c_68982]) ).
tcf(c_74147,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(sK18(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK21)
| ~ leaf_occ(sK18(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK21) ),
inference(instantiation,[status(thm)],[c_32350]) ).
tcf(c_74148,plain,
( subactivity_occurrence(sK18(sK17(sK20,sK21),sK21),sK21)
| ~ leaf_occ(sK18(sK17(sK20,sK21),sK21),sK21) ),
inference(instantiation,[status(thm)],[c_74147]) ).
tcf(c_74931,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(sK17(X0_iProver_leaf_occ_2,sK21),sK21)
| leaf_occ(sK18(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ arboreal(sK17(X0_iProver_leaf_occ_2,sK21))
| ~ subactivity_occurrence(sK17(X0_iProver_leaf_occ_2,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_30644]) ).
tcf(c_74932,plain,
( leaf_occ(sK17(sK20,sK21),sK21)
| leaf_occ(sK18(sK17(sK20,sK21),sK21),sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ arboreal(sK17(sK20,sK21))
| ~ subactivity_occurrence(sK17(sK20,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_74931]) ).
tcf(c_78915,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(sK17(X0_iProver_leaf_occ_2,sK21),sK21)
| next_subocc(sK17(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK18(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ arboreal(sK17(X0_iProver_leaf_occ_2,sK21))
| ~ subactivity_occurrence(sK17(X0_iProver_leaf_occ_2,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_30651]) ).
tcf(c_78917,plain,
( leaf_occ(sK17(sK20,sK21),sK21)
| next_subocc(sK17(sK17(sK20,sK21),sK21),sK18(sK17(sK20,sK21),sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ arboreal(sK17(sK20,sK21))
| ~ subactivity_occurrence(sK17(sK20,sK21),sK21) ),
inference(instantiation,[status(thm)],[c_78915]) ).
tcf(c_78952,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(sK17(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK18(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp0)
| ~ next_subocc(sK17(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK18(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_30733]) ).
tcf(c_78954,plain,
( min_precedes(sK17(sK17(sK20,sK21),sK21),sK18(sK17(sK20,sK21),sK21),tptp0)
| ~ next_subocc(sK17(sK17(sK20,sK21),sK21),sK18(sK17(sK20,sK21),sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_78952]) ).
tcf(c_82472,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK21)
| ~ leaf_occ(sK18(X0_iProver_leaf_occ_2,sK21),sK21)
| ( sK21 != sK21 )
| ( sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21) != sK18(X0_iProver_leaf_occ_2,sK21) ) ),
inference(instantiation,[status(thm)],[c_32784]) ).
tcf(c_82477,plain,
( leaf_occ(sK16(sK17(sK20,sK21),sK21),sK21)
| ~ leaf_occ(sK18(sK20,sK21),sK21)
| ( sK21 != sK21 )
| ( sK16(sK17(sK20,sK21),sK21) != sK18(sK20,sK21) ) ),
inference(instantiation,[status(thm)],[c_82472]) ).
tcf(c_85721,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ~ occurrence_of(sK21,tptp0)
| ~ leaf_occ(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK21)
| ~ min_precedes(sK16(sK17(X0_iProver_leaf_occ_2,sK21),sK21),sK17(sK17(X0_iProver_leaf_occ_2,sK21),sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_33698]) ).
tcf(c_85722,plain,
( ~ occurrence_of(sK21,tptp0)
| ~ leaf_occ(sK16(sK17(sK20,sK21),sK21),sK21)
| ~ min_precedes(sK16(sK17(sK20,sK21),sK21),sK17(sK17(sK20,sK21),sK21),tptp0) ),
inference(instantiation,[status(thm)],[c_85721]) ).
tcf(c_85723,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_85722,c_82477,c_78954,c_78917,c_74932,c_74148,c_68985,c_63712,c_33632,c_28058,c_26598,c_23115,c_20279,c_16677,c_4206,c_4205,c_3840,c_3547,c_3444,c_2862,c_1607,c_896,c_878,c_808,c_699,c_507,c_503,c_499,c_158,c_155,c_156,c_140,c_157]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO016+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.38 % Computer : n017.cluster.edu
% 0.08/0.38 % Model : x86_64 x86_64
% 0.08/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.38 % Memory : 8046.5625MB
% 0.08/0.38 % OS : Linux 6.8.0-71-generic
% 0.08/0.38 % CPULimit : 300
% 0.08/0.38 % WCLimit : 300
% 0.08/0.38 % DateTime : Thu Sep 24 06:27:49 UTC 2026
% 0.08/0.38 % CPUTime :
% 0.08/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.42 Running first-order theorem proving
% 0.08/0.42 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.08/0.43
% 0.08/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.08/0.43
% 0.08/0.43 % Detected problem language: tptp
% 0.08/0.44 % Proving...
% 106.94/16.38 % SZS status Started for theBenchmark.p
% 106.94/16.38 % SZS status Theorem for theBenchmark.p
% 106.94/16.38
% 106.94/16.38 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 106.94/16.38
% 106.94/16.38 % ------ iProver source info
% 106.94/16.38
% 106.94/16.38 % git: date: 2026-07-19 20:42:38 +0200
% 106.94/16.38 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 106.94/16.38 % git: non_committed_changes: false
% 106.94/16.38
% 106.94/16.38 % ------ Parsing...
% 106.94/16.38 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 106.94/16.38
% 106.94/16.38 % ------ Preprocessing... sf_s rm: 1 0s sf_e %
% 106.94/16.38
% 106.94/16.38 % ------ Preprocessing...%
% 106.94/16.38
% 106.94/16.38 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 106.94/16.38 % ------ Proving...
% 106.94/16.38 % ------ Problem Properties
% 106.94/16.38
% 106.94/16.38 %
% 106.94/16.38 % clauses 110
% 106.94/16.38 % conjectures 9
% 106.94/16.38 % EPR 66
% 106.94/16.38 % Horn 77
% 106.94/16.38 % unary 16
% 106.94/16.38 % binary 40
% 106.94/16.38 % lits 334
% 106.94/16.38 % lits eq 18
% 106.94/16.38 % fd_pure 0
% 106.94/16.38 % fd_pseudo 0
% 106.94/16.38 % fd_cond 0
% 106.94/16.38 % fd_pseudo_cond 12
% 106.94/16.38 % AC symbols 0
% 106.94/16.38
% 106.94/16.38 % ------ Input Options Time Limit: Unbounded
% 106.94/16.38
% 106.94/16.38
% 106.94/16.38 % ------
% 106.94/16.38 % Current options:
% 106.94/16.38 % ------
% 106.94/16.38
% 106.94/16.38
% 106.94/16.38 %
% 106.94/16.38
% 106.94/16.38 % ------ Proving...
% 106.94/16.38 %
% 106.94/16.38
% 106.94/16.38 % SZS status Theorem for theBenchmark.p
% 106.94/16.38
% 106.94/16.38 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 106.94/16.39
% 106.94/16.39
%------------------------------------------------------------------------------