%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO009+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 : Thu Sep 24 01:59:16 PM UTC 2026
% Result : Theorem 0.12s 5.53s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 12
% Syntax : Number of formulae : 97 ( 21 unt; 0 def)
% Number of atoms : 335 ( 21 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 385 ( 147 ~; 139 |; 86 &)
% ( 4 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-3 aty)
% Number of variables : 191 ( 162 !; 29 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [X28,X29,X30] :
( ( occurrence_of(X28,X30)
& occurrence_of(X28,X29) )
=> X29 = X30 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X39,X40] :
( subactivity_occurrence(X39,X40)
=> ( activity_occurrence(X40)
& activity_occurrence(X39) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X41] :
( activity_occurrence(X41)
=> ? [X42] :
( occurrence_of(X41,X42)
& activity(X42) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X55,X56] :
( leaf_occ(X55,X56)
<=> ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X58,X59] :
( root_occ(X58,X59)
<=> ? [X60] :
( root(X58,X60)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X60) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [X68,X69,X70] :
( min_precedes(X68,X69,X70)
=> ? [X71] :
( min_precedes(X71,X69,X70)
& root(X71,X70) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [X78,X79,X80] :
( next_subocc(X78,X79,X80)
<=> ( ~ ? [X81] :
( min_precedes(X81,X79,X80)
& min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [X82,X83,X84,X85] :
( ( subactivity_occurrence(X83,X85)
& occurrence_of(X85,X84)
& min_precedes(X82,X83,X84) )
=> subactivity_occurrence(X82,X85) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X90,X91,X92,X93] :
( ( root_occ(X91,X92)
& root_occ(X90,X92)
& occurrence_of(X92,X93) )
=> X90 = X91 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X101] :
( occurrence_of(X101,tptp0)
=> ? [X102,X103,X104] :
( leaf_occ(X104,X101)
& next_subocc(X103,X104,tptp0)
& ( occurrence_of(X104,tptp1)
| occurrence_of(X104,tptp2) )
& next_subocc(X102,X103,tptp0)
& occurrence_of(X103,tptp4)
& root_occ(X102,X101)
& occurrence_of(X102,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
tptp2 != tptp1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,conjecture,
! [X105] :
( occurrence_of(X105,tptp0)
=> ? [X106,X107] :
( leaf_occ(X107,X105)
& min_precedes(X106,X107,tptp0)
& ( occurrence_of(X107,tptp1)
| occurrence_of(X107,tptp2) )
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
~ ! [X105] :
( occurrence_of(X105,tptp0)
=> ? [X106,X107] :
( leaf_occ(X107,X105)
& min_precedes(X106,X107,tptp0)
& ( occurrence_of(X107,tptp1)
| occurrence_of(X107,tptp2) )
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f77,plain,
! [X28,X29,X30] :
( X29 = X30
| ~ occurrence_of(X28,X30)
| ~ occurrence_of(X28,X29) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f78,plain,
! [X29,X30] :
( X29 = X30
| ! [X28] :
( ~ occurrence_of(X28,X30)
| ~ occurrence_of(X28,X29) ) ),
inference(miniscoping,[status(thm)],[f77]) ).
fof(f79,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f86,plain,
! [X39,X40] :
( ( activity_occurrence(X40)
& activity_occurrence(X39) )
| ~ subactivity_occurrence(X39,X40) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f87,plain,
! [X0,X1] :
( activity_occurrence(X0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f89,plain,
! [X41] :
( ? [X42] :
( occurrence_of(X41,X42)
& activity(X42) )
| ~ activity_occurrence(X41) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f90,plain,
! [X41] :
( ( occurrence_of(X41,sK4_skl(X41))
& activity(sK4_skl(X41)) )
| ~ activity_occurrence(X41) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X42,sK4_skl(X41))],[f89]) ).
fof(f92,plain,
! [X0] :
( occurrence_of(X0,sK4_skl(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f117,plain,
! [X55,X56] :
( ( ! [X57] :
( ~ leaf(X55,X57)
| ~ subactivity_occurrence(X55,X56)
| ~ occurrence_of(X56,X57) )
| leaf_occ(X55,X56) )
& ( ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) )
| ~ leaf_occ(X55,X56) ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f118,plain,
( ! [X55,X56] :
( ! [X57] :
( ~ leaf(X55,X57)
| ~ subactivity_occurrence(X55,X56)
| ~ occurrence_of(X56,X57) )
| leaf_occ(X55,X56) )
& ! [X55,X56] :
( ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) )
| ~ leaf_occ(X55,X56) ) ),
inference(miniscoping,[status(thm)],[f117]) ).
fof(f119,plain,
( ! [X55,X56] :
( ! [X57] :
( ~ leaf(X55,X57)
| ~ subactivity_occurrence(X55,X56)
| ~ occurrence_of(X56,X57) )
| leaf_occ(X55,X56) )
& ! [X55,X56] :
( ( leaf(X55,sK8_skl(X56,X55))
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,sK8_skl(X56,X55)) )
| ~ leaf_occ(X55,X56) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X57,sK8_skl(X56,X55))],[f118]) ).
fof(f121,plain,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f124,plain,
! [X58,X59] :
( ( ! [X60] :
( ~ root(X58,X60)
| ~ subactivity_occurrence(X58,X59)
| ~ occurrence_of(X59,X60) )
| root_occ(X58,X59) )
& ( ? [X60] :
( root(X58,X60)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X60) )
| ~ root_occ(X58,X59) ) ),
inference(NNF_transformation,[status(thm)],[f20]) ).
fof(f125,plain,
( ! [X58,X59] :
( ! [X60] :
( ~ root(X58,X60)
| ~ subactivity_occurrence(X58,X59)
| ~ occurrence_of(X59,X60) )
| root_occ(X58,X59) )
& ! [X58,X59] :
( ? [X60] :
( root(X58,X60)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X60) )
| ~ root_occ(X58,X59) ) ),
inference(miniscoping,[status(thm)],[f124]) ).
fof(f126,plain,
( ! [X58,X59] :
( ! [X60] :
( ~ root(X58,X60)
| ~ subactivity_occurrence(X58,X59)
| ~ occurrence_of(X59,X60) )
| root_occ(X58,X59) )
& ! [X58,X59] :
( ( root(X58,sK9_skl(X59,X58))
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,sK9_skl(X59,X58)) )
| ~ root_occ(X58,X59) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X60,sK9_skl(X59,X58))],[f125]) ).
fof(f130,plain,
! [X0,X1,X2] :
( ~ root(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2)
| root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f141,plain,
! [X68,X69,X70] :
( ? [X71] :
( min_precedes(X71,X69,X70)
& root(X71,X70) )
| ~ min_precedes(X68,X69,X70) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f142,plain,
! [X69,X70] :
( ? [X71] :
( min_precedes(X71,X69,X70)
& root(X71,X70) )
| ! [X68] : ~ min_precedes(X68,X69,X70) ),
inference(miniscoping,[status(thm)],[f141]) ).
fof(f143,plain,
! [X69,X70] :
( ( min_precedes(sK10_skl(X70,X69),X69,X70)
& root(sK10_skl(X70,X69),X70) )
| ! [X68] : ~ min_precedes(X68,X69,X70) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(X71,sK10_skl(X70,X69))],[f142]) ).
fof(f144,plain,
! [X0,X1,X2] :
( root(sK10_skl(X2,X1),X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f145,plain,
! [X0,X1,X2] :
( min_precedes(sK10_skl(X2,X1),X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f153,plain,
! [X78,X79,X80] :
( next_subocc(X78,X79,X80)
<=> ( ! [X81] :
( ~ min_precedes(X81,X79,X80)
| ~ min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) ) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f154,plain,
! [X78,X79,X80] :
( ( ? [X81] :
( min_precedes(X81,X79,X80)
& min_precedes(X78,X81,X80) )
| ~ min_precedes(X78,X79,X80)
| next_subocc(X78,X79,X80) )
& ( ( ! [X81] :
( ~ min_precedes(X81,X79,X80)
| ~ min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) )
| ~ next_subocc(X78,X79,X80) ) ),
inference(NNF_transformation,[status(thm)],[f153]) ).
fof(f155,plain,
( ! [X78,X79,X80] :
( ? [X81] :
( min_precedes(X81,X79,X80)
& min_precedes(X78,X81,X80) )
| ~ min_precedes(X78,X79,X80)
| next_subocc(X78,X79,X80) )
& ! [X78,X79,X80] :
( ( ! [X81] :
( ~ min_precedes(X81,X79,X80)
| ~ min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) )
| ~ next_subocc(X78,X79,X80) ) ),
inference(miniscoping,[status(thm)],[f154]) ).
fof(f156,plain,
( ! [X78,X79,X80] :
( ( min_precedes(sK11_skl(X80,X79,X78),X79,X80)
& min_precedes(X78,sK11_skl(X80,X79,X78),X80) )
| ~ min_precedes(X78,X79,X80)
| next_subocc(X78,X79,X80) )
& ! [X78,X79,X80] :
( ( ! [X81] :
( ~ min_precedes(X81,X79,X80)
| ~ min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) )
| ~ next_subocc(X78,X79,X80) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X81,sK11_skl(X80,X79,X78))],[f155]) ).
fof(f157,plain,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f161,plain,
! [X82,X83,X84,X85] :
( subactivity_occurrence(X82,X85)
| ~ subactivity_occurrence(X83,X85)
| ~ occurrence_of(X85,X84)
| ~ min_precedes(X82,X83,X84) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f162,plain,
! [X82,X85] :
( subactivity_occurrence(X82,X85)
| ! [X83] :
( ~ subactivity_occurrence(X83,X85)
| ! [X84] :
( ~ occurrence_of(X85,X84)
| ~ min_precedes(X82,X83,X84) ) ) ),
inference(miniscoping,[status(thm)],[f161]) ).
fof(f163,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ subactivity_occurrence(X1,X3)
| ~ occurrence_of(X3,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f167,plain,
! [X90,X91,X92,X93] :
( X90 = X91
| ~ root_occ(X91,X92)
| ~ root_occ(X90,X92)
| ~ occurrence_of(X92,X93) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f168,plain,
! [X90,X91] :
( X90 = X91
| ! [X92] :
( ~ root_occ(X91,X92)
| ~ root_occ(X90,X92)
| ! [X93] : ~ occurrence_of(X92,X93) ) ),
inference(miniscoping,[status(thm)],[f167]) ).
fof(f169,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ root_occ(X3,X0)
| ~ root_occ(X2,X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f176,plain,
! [X101] :
( ? [X102,X103,X104] :
( leaf_occ(X104,X101)
& next_subocc(X103,X104,tptp0)
& ( occurrence_of(X104,tptp1)
| occurrence_of(X104,tptp2) )
& next_subocc(X102,X103,tptp0)
& occurrence_of(X103,tptp4)
& root_occ(X102,X101)
& occurrence_of(X102,tptp3) )
| ~ occurrence_of(X101,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f177,plain,
! [X101] :
( ? [X104] :
( leaf_occ(X104,X101)
& ? [X103] :
( next_subocc(X103,X104,tptp0)
& ( occurrence_of(X104,tptp1)
| occurrence_of(X104,tptp2) )
& ? [X102] :
( next_subocc(X102,X103,tptp0)
& occurrence_of(X103,tptp4)
& root_occ(X102,X101)
& occurrence_of(X102,tptp3) ) ) )
| ~ occurrence_of(X101,tptp0) ),
inference(miniscoping,[status(thm)],[f176]) ).
fof(f178,plain,
! [X101] :
( ( leaf_occ(sK12_skl(X101),X101)
& next_subocc(sK13_skl(X101),sK12_skl(X101),tptp0)
& ( occurrence_of(sK12_skl(X101),tptp1)
| occurrence_of(sK12_skl(X101),tptp2) )
& next_subocc(sK14_skl(X101),sK13_skl(X101),tptp0)
& occurrence_of(sK13_skl(X101),tptp4)
& root_occ(sK14_skl(X101),X101)
& occurrence_of(sK14_skl(X101),tptp3) )
| ~ occurrence_of(X101,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(X104,sK12_skl(X101)),skolemize(X103,sK13_skl(X101)),skolemize(X102,sK14_skl(X101))],[f177]) ).
fof(f179,plain,
! [X0] :
( occurrence_of(sK14_skl(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f180,plain,
! [X0] :
( root_occ(sK14_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f183,plain,
! [X0] :
( occurrence_of(sK12_skl(X0),tptp1)
| occurrence_of(sK12_skl(X0),tptp2)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f184,plain,
! [X0] :
( next_subocc(sK13_skl(X0),sK12_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f185,plain,
! [X0] :
( leaf_occ(sK12_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f197,plain,
tptp2 != tptp1,
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f198,plain,
? [X105] :
( ! [X106,X107] :
( ~ leaf_occ(X107,X105)
| ~ min_precedes(X106,X107,tptp0)
| ( ~ occurrence_of(X107,tptp1)
& ~ occurrence_of(X107,tptp2) )
| ~ root_occ(X106,X105)
| ~ occurrence_of(X106,tptp3) )
& occurrence_of(X105,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f199,plain,
? [X105] :
( ! [X107] :
( ~ leaf_occ(X107,X105)
| ! [X106] :
( ~ min_precedes(X106,X107,tptp0)
| ( ~ occurrence_of(X107,tptp1)
& ~ occurrence_of(X107,tptp2) )
| ~ root_occ(X106,X105)
| ~ occurrence_of(X106,tptp3) ) )
& occurrence_of(X105,tptp0) ),
inference(miniscoping,[status(thm)],[f198]) ).
fof(f200,plain,
( ! [X107] :
( ~ leaf_occ(X107,sK15_skl)
| ! [X106] :
( ~ min_precedes(X106,X107,tptp0)
| ( ~ occurrence_of(X107,tptp1)
& ~ occurrence_of(X107,tptp2) )
| ~ root_occ(X106,sK15_skl)
| ~ occurrence_of(X106,tptp3) ) )
& occurrence_of(sK15_skl,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X105,sK15_skl)],[f199]) ).
fof(f201,plain,
occurrence_of(sK15_skl,tptp0),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f202,plain,
! [X0,X1] :
( ~ leaf_occ(X1,sK15_skl)
| ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp2)
| ~ root_occ(X0,sK15_skl)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f203,plain,
! [X0,X1] :
( ~ leaf_occ(X1,sK15_skl)
| ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp1)
| ~ root_occ(X0,sK15_skl)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f211,plain,
! [X0,X1] :
( X0 = X1
| ~ root_occ(X1,sK15_skl)
| ~ root_occ(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f169,f201]) ).
fof(f304,plain,
root_occ(sK14_skl(sK15_skl),sK15_skl),
inference(resolution,[status(thm)],[f180,f201]) ).
fof(f305,plain,
! [X0] :
( sK14_skl(sK15_skl) = X0
| ~ root_occ(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f304,f211]) ).
fof(f317,plain,
leaf_occ(sK12_skl(sK15_skl),sK15_skl),
inference(resolution,[status(thm)],[f185,f201]) ).
fof(f323,plain,
subactivity_occurrence(sK12_skl(sK15_skl),sK15_skl),
inference(resolution,[status(thm)],[f317,f121]) ).
fof(f328,plain,
activity_occurrence(sK12_skl(sK15_skl)),
inference(resolution,[status(thm)],[f323,f87]) ).
fof(f329,plain,
occurrence_of(sK12_skl(sK15_skl),sK4_skl(sK12_skl(sK15_skl))),
inference(resolution,[status(thm)],[f328,f92]) ).
fof(f332,plain,
occurrence_of(sK14_skl(sK15_skl),tptp3),
inference(resolution,[status(thm)],[f179,f201]) ).
fof(f423,plain,
! [X0] :
( sK4_skl(sK12_skl(sK15_skl)) = X0
| ~ occurrence_of(sK12_skl(sK15_skl),X0) ),
inference(resolution,[status(thm)],[f329,f79]) ).
fof(f581,plain,
next_subocc(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),
inference(resolution,[status(thm)],[f184,f201]) ).
fof(f583,plain,
min_precedes(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),
inference(resolution,[status(thm)],[f581,f157]) ).
fof(f602,plain,
! [X0] :
( ~ root(X0,tptp0)
| ~ subactivity_occurrence(X0,sK15_skl)
| root_occ(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f130,f201]) ).
fof(f610,plain,
min_precedes(sK10_skl(tptp0,sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0),
inference(resolution,[status(thm)],[f583,f145]) ).
fof(f612,plain,
root(sK10_skl(tptp0,sK12_skl(sK15_skl)),tptp0),
inference(resolution,[status(thm)],[f583,f144]) ).
fof(f639,plain,
( ~ subactivity_occurrence(sK10_skl(tptp0,sK12_skl(sK15_skl)),sK15_skl)
| root_occ(sK10_skl(tptp0,sK12_skl(sK15_skl)),sK15_skl) ),
inference(resolution,[status(thm)],[f602,f612]) ).
fof(f768,plain,
! [X0] :
( subactivity_occurrence(sK10_skl(tptp0,sK12_skl(sK15_skl)),X0)
| ~ subactivity_occurrence(sK12_skl(sK15_skl),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f610,f163]) ).
fof(f886,plain,
( occurrence_of(sK12_skl(sK15_skl),tptp1)
| occurrence_of(sK12_skl(sK15_skl),tptp2) ),
inference(resolution,[status(thm)],[f183,f201]) ).
fof(f887,plain,
( sK4_skl(sK12_skl(sK15_skl)) = tptp2
| occurrence_of(sK12_skl(sK15_skl),tptp1) ),
inference(resolution,[status(thm)],[f886,f423]) ).
fof(f941,plain,
( sK4_skl(sK12_skl(sK15_skl)) = tptp1
| sK4_skl(sK12_skl(sK15_skl)) = tptp2 ),
inference(resolution,[status(thm)],[f887,f423]) ).
fof(f961,plain,
( sK4_skl(sK12_skl(sK15_skl)) = tptp1
| occurrence_of(sK12_skl(sK15_skl),tptp2) ),
inference(paramodulation,[status(thm)],[f941,f329]) ).
fof(f1630,plain,
( subactivity_occurrence(sK10_skl(tptp0,sK12_skl(sK15_skl)),sK15_skl)
| ~ occurrence_of(sK15_skl,tptp0) ),
inference(resolution,[status(thm)],[f768,f323]) ).
fof(f1634,plain,
subactivity_occurrence(sK10_skl(tptp0,sK12_skl(sK15_skl)),sK15_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1630,f201]) ).
fof(f2077,plain,
root_occ(sK10_skl(tptp0,sK12_skl(sK15_skl)),sK15_skl),
inference(forward_subsumption_resolution,[status(thm)],[f639,f1634]) ).
fof(f2078,plain,
sK14_skl(sK15_skl) = sK10_skl(tptp0,sK12_skl(sK15_skl)),
inference(resolution,[status(thm)],[f2077,f305]) ).
fof(f2122,plain,
min_precedes(sK14_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),
inference(backward_demodulation,[status(thm)],[f2078,f610]) ).
fof(f2138,plain,
( ~ leaf_occ(sK12_skl(sK15_skl),sK15_skl)
| ~ occurrence_of(sK12_skl(sK15_skl),tptp1)
| ~ root_occ(sK14_skl(sK15_skl),sK15_skl)
| ~ occurrence_of(sK14_skl(sK15_skl),tptp3) ),
inference(resolution,[status(thm)],[f2122,f203]) ).
fof(f2139,plain,
( ~ leaf_occ(sK12_skl(sK15_skl),sK15_skl)
| ~ occurrence_of(sK12_skl(sK15_skl),tptp2)
| ~ root_occ(sK14_skl(sK15_skl),sK15_skl)
| ~ occurrence_of(sK14_skl(sK15_skl),tptp3) ),
inference(resolution,[status(thm)],[f2122,f202]) ).
fof(f2153,plain,
( ~ leaf_occ(sK12_skl(sK15_skl),sK15_skl)
| ~ occurrence_of(sK12_skl(sK15_skl),tptp1)
| ~ root_occ(sK14_skl(sK15_skl),sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2138,f332]) ).
fof(f2154,plain,
( ~ leaf_occ(sK12_skl(sK15_skl),sK15_skl)
| ~ occurrence_of(sK12_skl(sK15_skl),tptp2)
| ~ root_occ(sK14_skl(sK15_skl),sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2139,f332]) ).
fof(f2561,plain,
( ~ leaf_occ(sK12_skl(sK15_skl),sK15_skl)
| ~ occurrence_of(sK12_skl(sK15_skl),tptp1) ),
inference(forward_subsumption_resolution,[status(thm)],[f2153,f304]) ).
fof(f2562,plain,
( sK4_skl(sK12_skl(sK15_skl)) = tptp2
| ~ leaf_occ(sK12_skl(sK15_skl),sK15_skl) ),
inference(resolution,[status(thm)],[f2561,f887]) ).
fof(f2564,plain,
sK4_skl(sK12_skl(sK15_skl)) = tptp2,
inference(forward_subsumption_resolution,[status(thm)],[f2562,f317]) ).
fof(f2576,plain,
( tptp2 = tptp1
| occurrence_of(sK12_skl(sK15_skl),tptp2) ),
inference(backward_demodulation,[status(thm)],[f2564,f961]) ).
fof(f2587,plain,
occurrence_of(sK12_skl(sK15_skl),tptp2),
inference(forward_subsumption_resolution,[status(thm)],[f2576,f197]) ).
fof(f2748,plain,
( ~ leaf_occ(sK12_skl(sK15_skl),sK15_skl)
| ~ occurrence_of(sK12_skl(sK15_skl),tptp2) ),
inference(forward_subsumption_resolution,[status(thm)],[f2154,f304]) ).
fof(f2749,plain,
~ leaf_occ(sK12_skl(sK15_skl),sK15_skl),
inference(resolution,[status(thm)],[f2748,f2587]) ).
fof(f2750,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2749,f317]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO009+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/5.35 % Computer : n002.cluster.edu
% 0.08/5.35 % Model : x86_64 x86_64
% 0.08/5.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.35 % Memory : 8046.5625MB
% 0.08/5.35 % OS : Linux 6.8.0-71-generic
% 0.08/5.35 % CPULimit : 300
% 0.08/5.35 % WCLimit : 300
% 0.08/5.35 % DateTime : Mon Sep 21 03:45:07 UTC 2026
% 0.08/5.36 % CPUTime :
% 0.08/5.37 % Drodi V4.1.1
% 0.12/5.53 % Refutation found
% 0.12/5.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/5.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/5.55 % Elapsed time: 0.182144 seconds
% 0.12/5.55 % CPU time: 1.174695 seconds
% 0.12/5.55 % Total memory used: 106.985 MB
% 0.12/5.55 % Net memory used: 105.475 MB
%------------------------------------------------------------------------------