%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : PRO018+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n005.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:39 PM UTC 2026
% Result : Theorem 47.34s 14.94s
% Output : CNFRefutation 47.34s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f143ERROR: Could not build tree for root c_28517ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& occurrence_of(X0,X1) )
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
fof(f8,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_07) ).
fof(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/sandbox2/benchmark/theBenchmark.p',sos_22) ).
fof(f26,axiom,
! [X0,X1,X2] :
( min_precedes(X1,X2,X0)
=> ? [X3] :
( subactivity_occurrence(X2,X3)
& subactivity_occurrence(X1,X3)
& occurrence_of(X3,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_25) ).
fof(f38,axiom,
! [X0,X1,X2] :
( ( leaf_occ(X1,X0)
& occurrence_of(X0,X2) )
=> ~ ? [X3] : min_precedes(X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_37) ).
fof(f50,axiom,
! [X0,X1] :
( ( ~ leaf_occ(X0,X1)
& arboreal(X0)
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,tptp0) )
=> ? [X2,X3,X4] :
( ! [X5] :
( min_precedes(X2,X5,tptp0)
=> ( X5 = X4
| X5 = X3 ) )
& min_precedes(X3,X4,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& min_precedes(X2,X3,tptp0)
& occurrence_of(X3,tptp4)
& next_subocc(X0,X2,tptp0)
& occurrence_of(X2,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_49) ).
fof(f56,axiom,
atomic(tptp3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_55) ).
fof(f57,axiom,
tptp4 != tptp3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_56) ).
fof(f60,axiom,
tptp3 != tptp1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_59) ).
fof(f61,axiom,
tptp3 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_60) ).
fof(f68,plain,
! [X0,X1,X2] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(ennf_transformation,[],[f3]) ).
fof(f69,plain,
! [X0,X1,X2] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(flattening,[],[f68]) ).
fof(f76,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ( arboreal(X0)
<=> atomic(X1) ) ),
inference(ennf_transformation,[],[f8]) ).
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(f96,plain,
! [X0,X1,X2] :
( ~ min_precedes(X1,X2,X0)
| ? [X3] :
( subactivity_occurrence(X2,X3)
& subactivity_occurrence(X1,X3)
& occurrence_of(X3,X0) ) ),
inference(ennf_transformation,[],[f26]) ).
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(f138,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ? [X2,X3,X4] :
( ! [X5] :
( ~ min_precedes(X2,X5,tptp0)
| X5 = X4
| X5 = X3 )
& min_precedes(X3,X4,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& min_precedes(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] :
( ! [X5] :
( ~ min_precedes(X2,X5,tptp0)
| X5 = X4
| X5 = X3 )
& min_precedes(X3,X4,tptp0)
& ( occurrence_of(X4,tptp2)
| occurrence_of(X4,tptp1) )
& min_precedes(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(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(f162,plain,
! [X0,X1,X2] :
( ~ min_precedes(X1,X2,X0)
| ( subactivity_occurrence(X2,sK10(X0,X1,X2))
& subactivity_occurrence(X1,sK10(X0,X1,X2))
& occurrence_of(sK10(X0,X1,X2),X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X3,sK10(X0,X1,X2))],[f96]) ).
fof(f170,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ( ! [X5] :
( ~ min_precedes(sK16(X0),X5,tptp0)
| sK18(X0) = X5
| sK17(X0) = X5 )
& min_precedes(sK17(X0),sK18(X0),tptp0)
& ( occurrence_of(sK18(X0),tptp2)
| occurrence_of(sK18(X0),tptp1) )
& min_precedes(sK16(X0),sK17(X0),tptp0)
& occurrence_of(sK17(X0),tptp4)
& next_subocc(X0,sK16(X0),tptp0)
& occurrence_of(sK16(X0),tptp3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18]),skolemize(X2,sK16(X0)),skolemize(X3,sK17(X0)),skolemize(X4,sK18(X0))],[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(f179,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f69]) ).
fof(f185,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f211,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f158]) ).
fof(f221,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| subactivity_occurrence(X1,sK10(X0,X1,X2)) ),
inference(cnf_transformation,[],[f162]) ).
fof(f222,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| occurrence_of(sK10(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f162]) ).
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(f254,plain,
! [X0,X1,X5] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ~ min_precedes(sK16(X0),X5,tptp0)
| sK18(X0) = X5
| sK17(X0) = X5 ),
inference(cnf_transformation,[],[f170]) ).
fof(f256,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK18(X0),tptp2)
| occurrence_of(sK18(X0),tptp1) ),
inference(cnf_transformation,[],[f170]) ).
fof(f257,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| min_precedes(sK16(X0),sK17(X0),tptp0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f258,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK17(X0),tptp4) ),
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),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),tptp3) ),
inference(cnf_transformation,[],[f170]) ).
fof(f266,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f56]) ).
fof(f267,plain,
tptp3 != tptp4,
inference(cnf_transformation,[],[f57]) ).
fof(f270,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f60]) ).
fof(f271,plain,
tptp3 != tptp2,
inference(cnf_transformation,[],[f61]) ).
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_53,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( arboreal(X0)
| ~ atomic(X1)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[],[f185]) ).
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_94,plain,
! [X0: $i,X1: $i,X2: $i] :
( occurrence_of(sK10(X2,X0,X1),X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i,X2: $i] :
( subactivity_occurrence(X0,sK10(X2,X0,X1))
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f221]) ).
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_128,plain,
! [X0: $i,X1: $i] :
( leaf_occ(X0,X1)
| occurrence_of(sK16(X0),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),tptp0)
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f259]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i] :
( leaf_occ(X0,X1)
| occurrence_of(sK17(X0),tptp4)
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f258]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i] :
( leaf_occ(X0,X1)
| min_precedes(sK16(X0),sK17(X0),tptp0)
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f257]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i] :
( leaf_occ(X0,X1)
| occurrence_of(sK18(X0),tptp2)
| occurrence_of(sK18(X0),tptp1)
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f256]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i,X2: $i] :
( leaf_occ(X0,X2)
| ( sK18(X0) = X1 )
| ( sK17(X0) = X1 )
| ~ arboreal(X0)
| ~ occurrence_of(X2,tptp0)
| ~ subactivity_occurrence(X0,X2)
| ~ min_precedes(sK16(X0),X1,tptp0) ),
inference(cnf_transformation,[],[f254]) ).
tcf(c_140,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f266]) ).
tcf(c_141,plain,
tptp3 != tptp4,
inference(cnf_transformation,[],[f267]) ).
tcf(c_144,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f270]) ).
tcf(c_145,plain,
tptp3 != tptp2,
inference(cnf_transformation,[],[f271]) ).
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_3700,negated_conjecture,
subactivity_occurrence(sK20,sK21),
inference(subtyping,[status(esa)],[c_156]) ).
tcf(c_3711,plain,
tptp3 != tptp2,
inference(subtyping,[status(esa)],[c_145]) ).
tcf(c_3712,plain,
tptp3 != tptp1,
inference(subtyping,[status(esa)],[c_144]) ).
tcf(c_3715,plain,
tptp3 != tptp4,
inference(subtyping,[status(esa)],[c_141]) ).
tcf(c_3722,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,X2_iProver_leaf_occ_2)
| ( sK18(X0_iProver_leaf_occ_2) = X1_iProver_leaf_occ_2 )
| ( sK17(X0_iProver_leaf_occ_2) = X1_iProver_leaf_occ_2 )
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(X2_iProver_leaf_occ_2,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,X2_iProver_leaf_occ_2)
| ~ min_precedes(sK16(X0_iProver_leaf_occ_2),X1_iProver_leaf_occ_2,tptp0) ),
inference(subtyping,[status(esa)],[c_134]) ).
tcf(c_3724,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(sK18(X0_iProver_leaf_occ_2),tptp2)
| occurrence_of(sK18(X0_iProver_leaf_occ_2),tptp1)
| ~ 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_132]) ).
tcf(c_3725,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)
| min_precedes(sK16(X0_iProver_leaf_occ_2),sK17(X0_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_3726,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(sK17(X0_iProver_leaf_occ_2),tptp4)
| ~ 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_130]) ).
tcf(c_3727,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),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_3728,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),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_3742,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_3761,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] :
( subactivity_occurrence(X0_iProver_leaf_occ_2,sK10(X0_iProver_occurrence_of_2,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_95]) ).
tcf(c_3762,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] :
( occurrence_of(sK10(X0_iProver_occurrence_of_2,X0_iProver_leaf_occ_2,X1_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_94]) ).
tcf(c_3770,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_3798,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_3803,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X0_iProver_occurrence_of_2: iProver_occurrence_of_2,X1_iProver_occurrence_of_2: iProver_occurrence_of_2] :
( ( X0_iProver_occurrence_of_2 = X1_iProver_occurrence_of_2 )
| ~ occurrence_of(X0_iProver_leaf_occ_2,X1_iProver_occurrence_of_2)
| ~ occurrence_of(X0_iProver_leaf_occ_2,X0_iProver_occurrence_of_2) ),
inference(subtyping,[status(esa)],[c_53]) ).
tcf(c_3810,plain,
! [X0_iProver_occurrence_of_2: iProver_occurrence_of_2] : X0_iProver_occurrence_of_2 = X0_iProver_occurrence_of_2,
theory(equality) ).
tcf(c_3814,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,X1_iProver_occurrence_of_2: iProver_occurrence_of_2] :
( occurrence_of(X0_iProver_leaf_occ_2,X0_iProver_occurrence_of_2)
| ~ occurrence_of(X1_iProver_leaf_occ_2,X1_iProver_occurrence_of_2)
| ( X0_iProver_occurrence_of_2 != X1_iProver_occurrence_of_2 )
| ( X0_iProver_leaf_occ_2 != X1_iProver_leaf_occ_2 ) ),
theory(equality) ).
tcf(c_5447,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),tptp3)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,sK21) ),
inference(instantiation,[status(thm)],[c_3728]) ).
tcf(c_5448,plain,
( leaf_occ(sK20,sK21)
| occurrence_of(sK16(sK20),tptp3)
| ~ arboreal(sK20)
| ~ subactivity_occurrence(sK20,sK21)
| ~ occurrence_of(sK21,tptp0) ),
inference(instantiation,[status(thm)],[c_5447]) ).
tcf(c_5449,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)
| ( sK18(X0_iProver_leaf_occ_2) = X1_iProver_leaf_occ_2 )
| ( sK17(X0_iProver_leaf_occ_2) = X1_iProver_leaf_occ_2 )
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,sK21)
| ~ min_precedes(sK16(X0_iProver_leaf_occ_2),X1_iProver_leaf_occ_2,tptp0) ),
inference(instantiation,[status(thm)],[c_3722]) ).
tcf(c_5463,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,sK21)
| min_precedes(sK16(X0_iProver_leaf_occ_2),sK17(X0_iProver_leaf_occ_2),tptp0)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,sK21) ),
inference(instantiation,[status(thm)],[c_3725]) ).
tcf(c_5464,plain,
( leaf_occ(sK20,sK21)
| min_precedes(sK16(sK20),sK17(sK20),tptp0)
| ~ arboreal(sK20)
| ~ subactivity_occurrence(sK20,sK21)
| ~ occurrence_of(sK21,tptp0) ),
inference(instantiation,[status(thm)],[c_5463]) ).
tcf(c_5465,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,sK21)
| occurrence_of(sK17(X0_iProver_leaf_occ_2),tptp4)
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,sK21) ),
inference(instantiation,[status(thm)],[c_3726]) ).
tcf(c_5466,plain,
( leaf_occ(sK20,sK21)
| occurrence_of(sK17(sK20),tptp4)
| ~ arboreal(sK20)
| ~ subactivity_occurrence(sK20,sK21)
| ~ occurrence_of(sK21,tptp0) ),
inference(instantiation,[status(thm)],[c_5465]) ).
tcf(c_5510,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ( tptp3 = tptp4 )
| ~ occurrence_of(X0_iProver_leaf_occ_2,tptp4)
| ~ occurrence_of(X0_iProver_leaf_occ_2,tptp3) ),
inference(instantiation,[status(thm)],[c_3803]) ).
tcf(c_5794,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( occurrence_of(sK10(tptp0,sK16(X0_iProver_leaf_occ_2),sK17(X0_iProver_leaf_occ_2)),tptp0)
| ~ min_precedes(sK16(X0_iProver_leaf_occ_2),sK17(X0_iProver_leaf_occ_2),tptp0) ),
inference(instantiation,[status(thm)],[c_3762]) ).
tcf(c_5795,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( subactivity_occurrence(sK16(X0_iProver_leaf_occ_2),sK10(tptp0,sK16(X0_iProver_leaf_occ_2),sK17(X0_iProver_leaf_occ_2)))
| ~ min_precedes(sK16(X0_iProver_leaf_occ_2),sK17(X0_iProver_leaf_occ_2),tptp0) ),
inference(instantiation,[status(thm)],[c_3761]) ).
tcf(c_5800,plain,
( subactivity_occurrence(sK16(sK20),sK10(tptp0,sK16(sK20),sK17(sK20)))
| ~ min_precedes(sK16(sK20),sK17(sK20),tptp0) ),
inference(instantiation,[status(thm)],[c_5795]) ).
tcf(c_5801,plain,
( occurrence_of(sK10(tptp0,sK16(sK20),sK17(sK20)),tptp0)
| ~ min_precedes(sK16(sK20),sK17(sK20),tptp0) ),
inference(instantiation,[status(thm)],[c_5794]) ).
tcf(c_5822,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ( tptp3 = tptp4 )
| ~ occurrence_of(sK17(X0_iProver_leaf_occ_2),tptp4)
| ~ occurrence_of(sK17(X0_iProver_leaf_occ_2),tptp3) ),
inference(instantiation,[status(thm)],[c_5510]) ).
tcf(c_5827,plain,
( ( tptp3 = tptp4 )
| ~ occurrence_of(sK17(sK20),tptp4)
| ~ occurrence_of(sK17(sK20),tptp3) ),
inference(instantiation,[status(thm)],[c_5822]) ).
tcf(c_5828,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(X0_iProver_leaf_occ_2,sK16(X0_iProver_leaf_occ_2),tptp0)
| ~ next_subocc(X0_iProver_leaf_occ_2,sK16(X0_iProver_leaf_occ_2),tptp0) ),
inference(instantiation,[status(thm)],[c_3770]) ).
tcf(c_5910,plain,
tptp3 = tptp3,
inference(instantiation,[status(thm)],[c_3810]) ).
tcf(c_6005,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( min_precedes(sK16(X0_iProver_leaf_occ_2),sK16(sK16(X0_iProver_leaf_occ_2)),tptp0)
| ~ next_subocc(sK16(X0_iProver_leaf_occ_2),sK16(sK16(X0_iProver_leaf_occ_2)),tptp0) ),
inference(instantiation,[status(thm)],[c_5828]) ).
tcf(c_6006,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( leaf_occ(X0_iProver_leaf_occ_2,sK21)
| ( sK18(X0_iProver_leaf_occ_2) = sK16(sK16(X0_iProver_leaf_occ_2)) )
| ( sK17(X0_iProver_leaf_occ_2) = sK16(sK16(X0_iProver_leaf_occ_2)) )
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,sK21)
| ~ min_precedes(sK16(X0_iProver_leaf_occ_2),sK16(sK16(X0_iProver_leaf_occ_2)),tptp0) ),
inference(instantiation,[status(thm)],[c_5449]) ).
tcf(c_6007,plain,
( min_precedes(sK16(sK20),sK16(sK16(sK20)),tptp0)
| ~ next_subocc(sK16(sK20),sK16(sK16(sK20)),tptp0) ),
inference(instantiation,[status(thm)],[c_6005]) ).
tcf(c_6008,plain,
( leaf_occ(sK20,sK21)
| ( sK18(sK20) = sK16(sK16(sK20)) )
| ( sK17(sK20) = sK16(sK16(sK20)) )
| ~ arboreal(sK20)
| ~ subactivity_occurrence(sK20,sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ min_precedes(sK16(sK20),sK16(sK16(sK20)),tptp0) ),
inference(instantiation,[status(thm)],[c_6006]) ).
tcf(c_6342,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ( tptp3 = tptp2 )
| ~ occurrence_of(X0_iProver_leaf_occ_2,tptp2)
| ~ occurrence_of(X0_iProver_leaf_occ_2,tptp3) ),
inference(instantiation,[status(thm)],[c_3803]) ).
tcf(c_6343,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ( tptp3 = tptp1 )
| ~ occurrence_of(X0_iProver_leaf_occ_2,tptp1)
| ~ occurrence_of(X0_iProver_leaf_occ_2,tptp3) ),
inference(instantiation,[status(thm)],[c_3803]) ).
tcf(c_6374,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] :
( occurrence_of(X0_iProver_leaf_occ_2,X0_iProver_occurrence_of_2)
| ~ occurrence_of(sK16(X1_iProver_leaf_occ_2),tptp3)
| ( X0_iProver_occurrence_of_2 != tptp3 )
| ( X0_iProver_leaf_occ_2 != sK16(X1_iProver_leaf_occ_2) ) ),
inference(instantiation,[status(thm)],[c_3814]) ).
tcf(c_6544,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( next_subocc(X0_iProver_leaf_occ_2,sK16(X0_iProver_leaf_occ_2),tptp0)
| leaf_occ(X0_iProver_leaf_occ_2,sK10(tptp0,sK16(X1_iProver_leaf_occ_2),sK17(X1_iProver_leaf_occ_2)))
| ~ arboreal(X0_iProver_leaf_occ_2)
| ~ occurrence_of(sK10(tptp0,sK16(X1_iProver_leaf_occ_2),sK17(X1_iProver_leaf_occ_2)),tptp0)
| ~ subactivity_occurrence(X0_iProver_leaf_occ_2,sK10(tptp0,sK16(X1_iProver_leaf_occ_2),sK17(X1_iProver_leaf_occ_2))) ),
inference(instantiation,[status(thm)],[c_3727]) ).
tcf(c_6637,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( occurrence_of(X0_iProver_leaf_occ_2,tptp3)
| ~ occurrence_of(sK16(X1_iProver_leaf_occ_2),tptp3)
| ( tptp3 != tptp3 )
| ( X0_iProver_leaf_occ_2 != sK16(X1_iProver_leaf_occ_2) ) ),
inference(instantiation,[status(thm)],[c_6374]) ).
tcf(c_7598,plain,
( leaf_occ(sK20,sK21)
| occurrence_of(sK16(sK20),tptp3)
| ~ arboreal(sK20)
| ~ occurrence_of(sK21,tptp0) ),
inference(resolution,[status(thm)],[c_3728,c_3700]) ).
tcf(c_7599,plain,
occurrence_of(sK16(sK20),tptp3),
inference(global_subsumption_just,[status(thm)],[c_7598,c_157,c_156,c_155,c_158,c_5448]) ).
tcf(c_7682,plain,
( leaf_occ(sK20,sK21)
| min_precedes(sK16(sK20),sK17(sK20),tptp0)
| ~ arboreal(sK20)
| ~ occurrence_of(sK21,tptp0) ),
inference(resolution,[status(thm)],[c_3725,c_3700]) ).
tcf(c_7683,plain,
min_precedes(sK16(sK20),sK17(sK20),tptp0),
inference(global_subsumption_just,[status(thm)],[c_7682,c_157,c_156,c_155,c_158,c_5464]) ).
tcf(c_7706,plain,
( leaf_occ(sK20,sK21)
| occurrence_of(sK18(sK20),tptp2)
| occurrence_of(sK18(sK20),tptp1)
| ~ arboreal(sK20)
| ~ occurrence_of(sK21,tptp0) ),
inference(resolution,[status(thm)],[c_3724,c_3700]) ).
tcf(c_7707,plain,
( occurrence_of(sK18(sK20),tptp1)
| occurrence_of(sK18(sK20),tptp2) ),
inference(global_subsumption_just,[status(thm)],[c_7706,c_157,c_155,c_158,c_7706]) ).
tcf(c_7708,plain,
( occurrence_of(sK18(sK20),tptp2)
| occurrence_of(sK18(sK20),tptp1) ),
inference(renaming,[status(thm)],[c_7707]) ).
tcf(c_8162,plain,
( arboreal(sK16(sK20))
| ~ atomic(tptp3) ),
inference(resolution,[status(thm)],[c_7599,c_3798]) ).
tcf(c_8706,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2,X1_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( next_subocc(sK16(X0_iProver_leaf_occ_2),sK16(sK16(X0_iProver_leaf_occ_2)),tptp0)
| leaf_occ(sK16(X0_iProver_leaf_occ_2),sK10(tptp0,sK16(X1_iProver_leaf_occ_2),sK17(X1_iProver_leaf_occ_2)))
| ~ arboreal(sK16(X0_iProver_leaf_occ_2))
| ~ occurrence_of(sK10(tptp0,sK16(X1_iProver_leaf_occ_2),sK17(X1_iProver_leaf_occ_2)),tptp0)
| ~ subactivity_occurrence(sK16(X0_iProver_leaf_occ_2),sK10(tptp0,sK16(X1_iProver_leaf_occ_2),sK17(X1_iProver_leaf_occ_2))) ),
inference(instantiation,[status(thm)],[c_6544]) ).
tcf(c_8711,plain,
( next_subocc(sK16(sK20),sK16(sK16(sK20)),tptp0)
| leaf_occ(sK16(sK20),sK10(tptp0,sK16(sK20),sK17(sK20)))
| ~ arboreal(sK16(sK20))
| ~ occurrence_of(sK10(tptp0,sK16(sK20),sK17(sK20)),tptp0)
| ~ subactivity_occurrence(sK16(sK20),sK10(tptp0,sK16(sK20),sK17(sK20))) ),
inference(instantiation,[status(thm)],[c_8706]) ).
tcf(c_8740,plain,
subactivity_occurrence(sK16(sK20),sK10(tptp0,sK16(sK20),sK17(sK20))),
inference(resolution,[status(thm)],[c_7683,c_3761]) ).
tcf(c_8978,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( occurrence_of(sK17(X0_iProver_leaf_occ_2),tptp3)
| ~ occurrence_of(sK16(sK16(X0_iProver_leaf_occ_2)),tptp3)
| ( tptp3 != tptp3 )
| ( sK17(X0_iProver_leaf_occ_2) != sK16(sK16(X0_iProver_leaf_occ_2)) ) ),
inference(instantiation,[status(thm)],[c_6637]) ).
tcf(c_8981,plain,
( occurrence_of(sK17(sK20),tptp3)
| ~ occurrence_of(sK16(sK16(sK20)),tptp3)
| ( tptp3 != tptp3 )
| ( sK17(sK20) != sK16(sK16(sK20)) ) ),
inference(instantiation,[status(thm)],[c_8978]) ).
tcf(c_10716,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(sK16(X0_iProver_leaf_occ_2),X1_iProver_leaf_occ_2,X0_iProver_occurrence_of_2)
| ~ occurrence_of(sK10(tptp0,sK16(X0_iProver_leaf_occ_2),sK17(X0_iProver_leaf_occ_2)),X0_iProver_occurrence_of_2)
| ~ leaf_occ(sK16(X0_iProver_leaf_occ_2),sK10(tptp0,sK16(X0_iProver_leaf_occ_2),sK17(X0_iProver_leaf_occ_2))) ),
inference(instantiation,[status(thm)],[c_3742]) ).
tcf(c_13435,plain,
( next_subocc(sK16(sK20),sK16(sK16(sK20)),tptp0)
| leaf_occ(sK16(sK20),sK10(tptp0,sK16(sK20),sK17(sK20)))
| ~ arboreal(sK16(sK20))
| ~ occurrence_of(sK10(tptp0,sK16(sK20),sK17(sK20)),tptp0) ),
inference(resolution,[status(thm)],[c_8740,c_3727]) ).
tcf(c_13437,plain,
( occurrence_of(sK16(sK16(sK20)),tptp3)
| leaf_occ(sK16(sK20),sK10(tptp0,sK16(sK20),sK17(sK20)))
| ~ arboreal(sK16(sK20))
| ~ occurrence_of(sK10(tptp0,sK16(sK20),sK17(sK20)),tptp0) ),
inference(resolution,[status(thm)],[c_8740,c_3728]) ).
tcf(c_13440,plain,
( occurrence_of(sK16(sK16(sK20)),tptp3)
| leaf_occ(sK16(sK20),sK10(tptp0,sK16(sK20),sK17(sK20))) ),
inference(global_subsumption_just,[status(thm)],[c_13437,c_157,c_140,c_156,c_155,c_158,c_5464,c_5801,c_8162,c_13437]) ).
tcf(c_13444,plain,
( next_subocc(sK16(sK20),sK16(sK16(sK20)),tptp0)
| leaf_occ(sK16(sK20),sK10(tptp0,sK16(sK20),sK17(sK20))) ),
inference(global_subsumption_just,[status(thm)],[c_13435,c_157,c_140,c_156,c_155,c_158,c_5464,c_5800,c_5801,c_8162,c_8711]) ).
tcf(c_14941,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( occurrence_of(sK18(X0_iProver_leaf_occ_2),tptp3)
| ~ occurrence_of(sK16(sK16(X0_iProver_leaf_occ_2)),tptp3)
| ( tptp3 != tptp3 )
| ( sK18(X0_iProver_leaf_occ_2) != sK16(sK16(X0_iProver_leaf_occ_2)) ) ),
inference(instantiation,[status(thm)],[c_6637]) ).
tcf(c_14944,plain,
( occurrence_of(sK18(sK20),tptp3)
| ~ occurrence_of(sK16(sK16(sK20)),tptp3)
| ( tptp3 != tptp3 )
| ( sK18(sK20) != sK16(sK16(sK20)) ) ),
inference(instantiation,[status(thm)],[c_14941]) ).
tcf(c_18012,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ~ min_precedes(sK16(X0_iProver_leaf_occ_2),sK17(X0_iProver_leaf_occ_2),tptp0)
| ~ occurrence_of(sK10(tptp0,sK16(X0_iProver_leaf_occ_2),sK17(X0_iProver_leaf_occ_2)),tptp0)
| ~ leaf_occ(sK16(X0_iProver_leaf_occ_2),sK10(tptp0,sK16(X0_iProver_leaf_occ_2),sK17(X0_iProver_leaf_occ_2))) ),
inference(instantiation,[status(thm)],[c_10716]) ).
tcf(c_18013,plain,
( ~ min_precedes(sK16(sK20),sK17(sK20),tptp0)
| ~ occurrence_of(sK10(tptp0,sK16(sK20),sK17(sK20)),tptp0)
| ~ leaf_occ(sK16(sK20),sK10(tptp0,sK16(sK20),sK17(sK20))) ),
inference(instantiation,[status(thm)],[c_18012]) ).
tcf(c_18882,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ( tptp3 = tptp2 )
| ~ occurrence_of(sK18(X0_iProver_leaf_occ_2),tptp2)
| ~ occurrence_of(sK18(X0_iProver_leaf_occ_2),tptp3) ),
inference(instantiation,[status(thm)],[c_6342]) ).
tcf(c_18887,plain,
( ( tptp3 = tptp2 )
| ~ occurrence_of(sK18(sK20),tptp2)
| ~ occurrence_of(sK18(sK20),tptp3) ),
inference(instantiation,[status(thm)],[c_18882]) ).
tcf(c_28513,plain,
! [X0_iProver_leaf_occ_2: iProver_leaf_occ_2] :
( ( tptp3 = tptp1 )
| ~ occurrence_of(sK18(X0_iProver_leaf_occ_2),tptp1)
| ~ occurrence_of(sK18(X0_iProver_leaf_occ_2),tptp3) ),
inference(instantiation,[status(thm)],[c_6343]) ).
tcf(c_28516,plain,
( ( tptp3 = tptp1 )
| ~ occurrence_of(sK18(sK20),tptp1)
| ~ occurrence_of(sK18(sK20),tptp3) ),
inference(instantiation,[status(thm)],[c_28513]) ).
tcf(c_28517,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_28516,c_18887,c_18013,c_14944,c_13444,c_13440,c_8981,c_7708,c_6008,c_6007,c_5910,c_5827,c_5801,c_5466,c_5464,c_3715,c_3712,c_3711,c_158,c_155,c_156,c_157]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO018+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.35 % Computer : n005.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Thu Sep 24 06:33:32 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.41
% 0.10/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.41
% 0.10/0.41 % Detected problem language: tptp
% 0.10/0.42 % Proving...
% 47.34/14.94 % SZS status Started for theBenchmark.p
% 47.34/14.94 % SZS status Theorem for theBenchmark.p
% 47.34/14.94
% 47.34/14.94 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 47.34/14.94
% 47.34/14.94 % ------ iProver source info
% 47.34/14.94
% 47.34/14.94 % git: date: 2026-07-19 20:42:38 +0200
% 47.34/14.94 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 47.34/14.94 % git: non_committed_changes: false
% 47.34/14.94
% 47.34/14.94 % ------ Parsing...
% 47.34/14.94 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 47.34/14.94
% 47.34/14.94 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 47.34/14.94
% 47.34/14.94 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 47.34/14.94
% 47.34/14.94 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 47.34/14.94 % ------ Proving...
% 47.34/14.94 % ------ Problem Properties
% 47.34/14.94
% 47.34/14.94 %
% 47.34/14.94 % clauses 110
% 47.34/14.94 % conjectures 9
% 47.34/14.94 % EPR 66
% 47.34/14.94 % Horn 77
% 47.34/14.94 % unary 16
% 47.34/14.94 % binary 40
% 47.34/14.94 % lits 336
% 47.34/14.94 % lits eq 20
% 47.34/14.94 % fd_pure 0
% 47.34/14.94 % fd_pseudo 0
% 47.34/14.94 % fd_cond 0
% 47.34/14.94 % fd_pseudo_cond 13
% 47.34/14.94 % AC symbols 0
% 47.34/14.94
% 47.34/14.94 % ------ Input Options Time Limit: Unbounded
% 47.34/14.94
% 47.34/14.94
% 47.34/14.94 % ------
% 47.34/14.94 % Current options:
% 47.34/14.94 % ------
% 47.34/14.94
% 47.34/14.94
% 47.34/14.94 %
% 47.34/14.94
% 47.34/14.94 % ------ Proving...
% 47.34/14.94 %
% 47.34/14.94
% 47.34/14.94 % SZS status Theorem for theBenchmark.p
% 47.34/14.94
% 47.34/14.94 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 47.34/14.94
% 47.34/14.94
%------------------------------------------------------------------------------