%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO009+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:59:16 PM UTC 2026
% Result : Theorem 1.15s 0.71s
% Output : CNFRefutation 1.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 13
% Syntax : Number of formulae : 107 ( 26 unt; 0 def)
% Number of atoms : 370 ( 17 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 430 ( 167 ~; 166 |; 82 &)
% ( 5 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-3 aty)
% Number of variables : 207 ( 183 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X4,X5,X6] :
( ( occurrence_of(X4,X6)
& occurrence_of(X4,X5) )
=> X5 = X6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X8,X9] :
( earlier(X8,X9)
=> ~ earlier(X9,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X18] :
( legal(X18)
=> arboreal(X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X21,X22] :
( precedes(X21,X22)
<=> ( legal(X22)
& earlier(X21,X22) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X35,X36,X37] :
( min_precedes(X35,X36,X37)
=> ~ root(X36,X37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X38,X39,X40] :
( min_precedes(X38,X39,X40)
=> precedes(X38,X39) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [X41,X42] :
( root(X41,X42)
=> legal(X41) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X60,X61,X62] :
( next_subocc(X60,X61,X62)
<=> ( ~ ? [X63] :
( min_precedes(X63,X61,X62)
& min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X79,X80,X81,X82] :
( ( subactivity_occurrence(X82,X80)
& subactivity_occurrence(X81,X80)
& arboreal(X82)
& arboreal(X81)
& occurrence_of(X80,X79) )
=> ( X81 = X82
| min_precedes(X82,X81,X79)
| min_precedes(X81,X82,X79) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [X99,X100] :
( root_occ(X99,X100)
<=> ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [X102,X103] :
( leaf_occ(X102,X103)
<=> ? [X104] :
( leaf(X102,X104)
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,X104) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X105] :
( occurrence_of(X105,tptp0)
=> ? [X106,X107,X108] :
( leaf_occ(X108,X105)
& next_subocc(X107,X108,tptp0)
& ( occurrence_of(X108,tptp1)
| occurrence_of(X108,tptp2) )
& next_subocc(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,conjecture,
! [X109] :
( occurrence_of(X109,tptp0)
=> ? [X110,X111] :
( leaf_occ(X111,X109)
& min_precedes(X110,X111,tptp0)
& ( occurrence_of(X111,tptp1)
| occurrence_of(X111,tptp2) )
& root_occ(X110,X109)
& occurrence_of(X110,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,negated_conjecture,
~ ! [X109] :
( occurrence_of(X109,tptp0)
=> ? [X110,X111] :
( leaf_occ(X111,X109)
& min_precedes(X110,X111,tptp0)
& ( occurrence_of(X111,tptp1)
| occurrence_of(X111,tptp2) )
& root_occ(X110,X109)
& occurrence_of(X110,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f49]) ).
fof(f58,plain,
! [X4,X5,X6] :
( X5 = X6
| ~ occurrence_of(X4,X6)
| ~ occurrence_of(X4,X5) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f59,plain,
! [X5,X6] :
( X5 = X6
| ! [X4] :
( ~ occurrence_of(X4,X6)
| ~ occurrence_of(X4,X5) ) ),
inference(miniscoping,[status(thm)],[f58]) ).
fof(f60,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f63,plain,
! [X8,X9] :
( ~ earlier(X9,X8)
| ~ earlier(X8,X9) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f64,plain,
! [X0,X1] :
( ~ earlier(X1,X0)
| ~ earlier(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f75,plain,
! [X18] :
( arboreal(X18)
| ~ legal(X18) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f76,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f80,plain,
! [X21,X22] :
( ( ~ legal(X22)
| ~ earlier(X21,X22)
| precedes(X21,X22) )
& ( ( legal(X22)
& earlier(X21,X22) )
| ~ precedes(X21,X22) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f81,plain,
( ! [X21,X22] :
( ~ legal(X22)
| ~ earlier(X21,X22)
| precedes(X21,X22) )
& ! [X21,X22] :
( ( legal(X22)
& earlier(X21,X22) )
| ~ precedes(X21,X22) ) ),
inference(miniscoping,[status(thm)],[f80]) ).
fof(f82,plain,
! [X0,X1] :
( earlier(X0,X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
! [X0,X1] :
( legal(X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f101,plain,
! [X35,X36,X37] :
( ~ root(X36,X37)
| ~ min_precedes(X35,X36,X37) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f102,plain,
! [X36,X37] :
( ~ root(X36,X37)
| ! [X35] : ~ min_precedes(X35,X36,X37) ),
inference(miniscoping,[status(thm)],[f101]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f104,plain,
! [X38,X39,X40] :
( precedes(X38,X39)
| ~ min_precedes(X38,X39,X40) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f105,plain,
! [X38,X39] :
( precedes(X38,X39)
| ! [X40] : ~ min_precedes(X38,X39,X40) ),
inference(miniscoping,[status(thm)],[f104]) ).
fof(f106,plain,
! [X0,X1,X2] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f107,plain,
! [X41,X42] :
( legal(X41)
| ~ root(X41,X42) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f108,plain,
! [X41] :
( legal(X41)
| ! [X42] : ~ root(X41,X42) ),
inference(miniscoping,[status(thm)],[f107]) ).
fof(f109,plain,
! [X0,X1] :
( legal(X0)
| ~ root(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f129,plain,
! [X60,X61,X62] :
( next_subocc(X60,X61,X62)
<=> ( ! [X63] :
( ~ min_precedes(X63,X61,X62)
| ~ min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) ) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f130,plain,
! [X60,X61,X62] :
( ( ? [X63] :
( min_precedes(X63,X61,X62)
& min_precedes(X60,X63,X62) )
| ~ min_precedes(X60,X61,X62)
| next_subocc(X60,X61,X62) )
& ( ( ! [X63] :
( ~ min_precedes(X63,X61,X62)
| ~ min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) )
| ~ next_subocc(X60,X61,X62) ) ),
inference(NNF_transformation,[status(thm)],[f129]) ).
fof(f131,plain,
( ! [X60,X61,X62] :
( ? [X63] :
( min_precedes(X63,X61,X62)
& min_precedes(X60,X63,X62) )
| ~ min_precedes(X60,X61,X62)
| next_subocc(X60,X61,X62) )
& ! [X60,X61,X62] :
( ( ! [X63] :
( ~ min_precedes(X63,X61,X62)
| ~ min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) )
| ~ next_subocc(X60,X61,X62) ) ),
inference(miniscoping,[status(thm)],[f130]) ).
fof(f132,plain,
( ! [X60,X61,X62] :
( ( min_precedes(sK7_skl(X62,X61,X60),X61,X62)
& min_precedes(X60,sK7_skl(X62,X61,X60),X62) )
| ~ min_precedes(X60,X61,X62)
| next_subocc(X60,X61,X62) )
& ! [X60,X61,X62] :
( ( ! [X63] :
( ~ min_precedes(X63,X61,X62)
| ~ min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) )
| ~ next_subocc(X60,X61,X62) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X63,sK7_skl(X62,X61,X60))],[f131]) ).
fof(f133,plain,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f160,plain,
! [X79,X80,X81,X82] :
( X81 = X82
| min_precedes(X82,X81,X79)
| min_precedes(X81,X82,X79)
| ~ subactivity_occurrence(X82,X80)
| ~ subactivity_occurrence(X81,X80)
| ~ arboreal(X82)
| ~ arboreal(X81)
| ~ occurrence_of(X80,X79) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f161,plain,
! [X79,X81,X82] :
( X81 = X82
| min_precedes(X82,X81,X79)
| min_precedes(X81,X82,X79)
| ! [X80] :
( ~ subactivity_occurrence(X82,X80)
| ~ subactivity_occurrence(X81,X80)
| ~ arboreal(X82)
| ~ arboreal(X81)
| ~ occurrence_of(X80,X79) ) ),
inference(miniscoping,[status(thm)],[f160]) ).
fof(f162,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| min_precedes(X3,X2,X1)
| min_precedes(X2,X3,X1)
| ~ subactivity_occurrence(X3,X0)
| ~ subactivity_occurrence(X2,X0)
| ~ arboreal(X3)
| ~ arboreal(X2)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f177,plain,
! [X99,X100] :
( ( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ( ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) )
| ~ root_occ(X99,X100) ) ),
inference(NNF_transformation,[status(thm)],[f34]) ).
fof(f178,plain,
( ! [X99,X100] :
( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ! [X99,X100] :
( ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) )
| ~ root_occ(X99,X100) ) ),
inference(miniscoping,[status(thm)],[f177]) ).
fof(f179,plain,
( ! [X99,X100] :
( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ! [X99,X100] :
( ( root(X99,sK13_skl(X100,X99))
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,sK13_skl(X100,X99)) )
| ~ root_occ(X99,X100) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(X101,sK13_skl(X100,X99))],[f178]) ).
fof(f180,plain,
! [X0,X1] :
( occurrence_of(X1,sK13_skl(X1,X0))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f181,plain,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f182,plain,
! [X0,X1] :
( root(X0,sK13_skl(X1,X0))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f184,plain,
! [X102,X103] :
( ( ! [X104] :
( ~ leaf(X102,X104)
| ~ subactivity_occurrence(X102,X103)
| ~ occurrence_of(X103,X104) )
| leaf_occ(X102,X103) )
& ( ? [X104] :
( leaf(X102,X104)
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,X104) )
| ~ leaf_occ(X102,X103) ) ),
inference(NNF_transformation,[status(thm)],[f35]) ).
fof(f185,plain,
( ! [X102,X103] :
( ! [X104] :
( ~ leaf(X102,X104)
| ~ subactivity_occurrence(X102,X103)
| ~ occurrence_of(X103,X104) )
| leaf_occ(X102,X103) )
& ! [X102,X103] :
( ? [X104] :
( leaf(X102,X104)
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,X104) )
| ~ leaf_occ(X102,X103) ) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f186,plain,
( ! [X102,X103] :
( ! [X104] :
( ~ leaf(X102,X104)
| ~ subactivity_occurrence(X102,X103)
| ~ occurrence_of(X103,X104) )
| leaf_occ(X102,X103) )
& ! [X102,X103] :
( ( leaf(X102,sK14_skl(X103,X102))
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,sK14_skl(X103,X102)) )
| ~ leaf_occ(X102,X103) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X104,sK14_skl(X103,X102))],[f185]) ).
fof(f188,plain,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f191,plain,
! [X105] :
( ? [X106,X107,X108] :
( leaf_occ(X108,X105)
& next_subocc(X107,X108,tptp0)
& ( occurrence_of(X108,tptp1)
| occurrence_of(X108,tptp2) )
& next_subocc(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) )
| ~ occurrence_of(X105,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f192,plain,
! [X105] :
( ? [X108] :
( leaf_occ(X108,X105)
& ? [X107] :
( next_subocc(X107,X108,tptp0)
& ( occurrence_of(X108,tptp1)
| occurrence_of(X108,tptp2) )
& ? [X106] :
( next_subocc(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) ) ) )
| ~ occurrence_of(X105,tptp0) ),
inference(miniscoping,[status(thm)],[f191]) ).
fof(f193,plain,
! [X105] :
( ( leaf_occ(sK15_skl(X105),X105)
& next_subocc(sK16_skl(X105),sK15_skl(X105),tptp0)
& ( occurrence_of(sK15_skl(X105),tptp1)
| occurrence_of(sK15_skl(X105),tptp2) )
& next_subocc(sK17_skl(X105),sK16_skl(X105),tptp0)
& occurrence_of(sK16_skl(X105),tptp4)
& root_occ(sK17_skl(X105),X105)
& occurrence_of(sK17_skl(X105),tptp3) )
| ~ occurrence_of(X105,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(X108,sK15_skl(X105)),skolemize(X107,sK16_skl(X105)),skolemize(X106,sK17_skl(X105))],[f192]) ).
fof(f194,plain,
! [X0] :
( occurrence_of(sK17_skl(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f195,plain,
! [X0] :
( root_occ(sK17_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f197,plain,
! [X0] :
( next_subocc(sK17_skl(X0),sK16_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f198,plain,
! [X0] :
( occurrence_of(sK15_skl(X0),tptp1)
| occurrence_of(sK15_skl(X0),tptp2)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f199,plain,
! [X0] :
( next_subocc(sK16_skl(X0),sK15_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f200,plain,
! [X0] :
( leaf_occ(sK15_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f213,plain,
? [X109] :
( ! [X110,X111] :
( ~ leaf_occ(X111,X109)
| ~ min_precedes(X110,X111,tptp0)
| ( ~ occurrence_of(X111,tptp1)
& ~ occurrence_of(X111,tptp2) )
| ~ root_occ(X110,X109)
| ~ occurrence_of(X110,tptp3) )
& occurrence_of(X109,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f214,plain,
? [X109] :
( ! [X111] :
( ~ leaf_occ(X111,X109)
| ! [X110] :
( ~ min_precedes(X110,X111,tptp0)
| ( ~ occurrence_of(X111,tptp1)
& ~ occurrence_of(X111,tptp2) )
| ~ root_occ(X110,X109)
| ~ occurrence_of(X110,tptp3) ) )
& occurrence_of(X109,tptp0) ),
inference(miniscoping,[status(thm)],[f213]) ).
fof(f215,plain,
( ! [X111] :
( ~ leaf_occ(X111,sK18_skl)
| ! [X110] :
( ~ min_precedes(X110,X111,tptp0)
| ( ~ occurrence_of(X111,tptp1)
& ~ occurrence_of(X111,tptp2) )
| ~ root_occ(X110,sK18_skl)
| ~ occurrence_of(X110,tptp3) ) )
& occurrence_of(sK18_skl,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(X109,sK18_skl)],[f214]) ).
fof(f216,plain,
occurrence_of(sK18_skl,tptp0),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f217,plain,
! [X0,X1] :
( ~ leaf_occ(X1,sK18_skl)
| ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp2)
| ~ root_occ(X0,sK18_skl)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f218,plain,
! [X0,X1] :
( ~ leaf_occ(X1,sK18_skl)
| ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp1)
| ~ root_occ(X0,sK18_skl)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f219,plain,
! [X0] :
( X0 = tptp0
| ~ occurrence_of(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f60,f216]) ).
fof(f234,plain,
root_occ(sK17_skl(sK18_skl),sK18_skl),
inference(resolution,[status(thm)],[f195,f216]) ).
fof(f237,plain,
root(sK17_skl(sK18_skl),sK13_skl(sK18_skl,sK17_skl(sK18_skl))),
inference(resolution,[status(thm)],[f234,f182]) ).
fof(f238,plain,
occurrence_of(sK18_skl,sK13_skl(sK18_skl,sK17_skl(sK18_skl))),
inference(resolution,[status(thm)],[f234,f180]) ).
fof(f239,plain,
subactivity_occurrence(sK17_skl(sK18_skl),sK18_skl),
inference(resolution,[status(thm)],[f234,f181]) ).
fof(f244,plain,
leaf_occ(sK15_skl(sK18_skl),sK18_skl),
inference(resolution,[status(thm)],[f200,f216]) ).
fof(f246,plain,
! [X0] :
( ~ min_precedes(X0,sK15_skl(sK18_skl),tptp0)
| ~ occurrence_of(sK15_skl(sK18_skl),tptp2)
| ~ root_occ(X0,sK18_skl)
| ~ occurrence_of(X0,tptp3) ),
inference(resolution,[status(thm)],[f244,f217]) ).
fof(f249,plain,
subactivity_occurrence(sK15_skl(sK18_skl),sK18_skl),
inference(resolution,[status(thm)],[f244,f188]) ).
fof(f254,plain,
sK13_skl(sK18_skl,sK17_skl(sK18_skl)) = tptp0,
inference(resolution,[status(thm)],[f238,f219]) ).
fof(f272,plain,
root(sK17_skl(sK18_skl),tptp0),
inference(forward_demodulation,[status(thm)],[f254,f237]) ).
fof(f273,plain,
! [X0] : ~ min_precedes(X0,sK17_skl(sK18_skl),tptp0),
inference(resolution,[status(thm)],[f272,f103]) ).
fof(f274,plain,
legal(sK17_skl(sK18_skl)),
inference(resolution,[status(thm)],[f272,f109]) ).
fof(f278,plain,
arboreal(sK17_skl(sK18_skl)),
inference(resolution,[status(thm)],[f274,f76]) ).
fof(f283,plain,
occurrence_of(sK17_skl(sK18_skl),tptp3),
inference(resolution,[status(thm)],[f194,f216]) ).
fof(f436,plain,
! [X0,X1] :
( X1 = sK17_skl(sK18_skl)
| min_precedes(sK17_skl(sK18_skl),X1,X0)
| min_precedes(X1,sK17_skl(sK18_skl),X0)
| ~ subactivity_occurrence(X1,sK18_skl)
| ~ arboreal(sK17_skl(sK18_skl))
| ~ arboreal(X1)
| ~ occurrence_of(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f162,f239]) ).
fof(f438,plain,
! [X0,X1] :
( X1 = sK17_skl(sK18_skl)
| min_precedes(sK17_skl(sK18_skl),X1,X0)
| min_precedes(X1,sK17_skl(sK18_skl),X0)
| ~ subactivity_occurrence(X1,sK18_skl)
| ~ arboreal(X1)
| ~ occurrence_of(sK18_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f436,f278]) ).
fof(f468,plain,
! [X0] :
( min_precedes(sK17_skl(X0),sK16_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f197,f133]) ).
fof(f470,plain,
! [X0] :
( min_precedes(sK16_skl(X0),sK15_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f199,f133]) ).
fof(f472,plain,
min_precedes(sK17_skl(sK18_skl),sK16_skl(sK18_skl),tptp0),
inference(resolution,[status(thm)],[f468,f216]) ).
fof(f486,plain,
precedes(sK17_skl(sK18_skl),sK16_skl(sK18_skl)),
inference(resolution,[status(thm)],[f472,f106]) ).
fof(f490,plain,
earlier(sK17_skl(sK18_skl),sK16_skl(sK18_skl)),
inference(resolution,[status(thm)],[f486,f82]) ).
fof(f498,plain,
~ earlier(sK16_skl(sK18_skl),sK17_skl(sK18_skl)),
inference(resolution,[status(thm)],[f490,f64]) ).
fof(f521,plain,
! [X0] :
( X0 = sK17_skl(sK18_skl)
| min_precedes(sK17_skl(sK18_skl),X0,tptp0)
| min_precedes(X0,sK17_skl(sK18_skl),tptp0)
| ~ subactivity_occurrence(X0,sK18_skl)
| ~ arboreal(X0) ),
inference(resolution,[status(thm)],[f438,f216]) ).
fof(f522,plain,
! [X0] :
( X0 = sK17_skl(sK18_skl)
| min_precedes(sK17_skl(sK18_skl),X0,tptp0)
| ~ subactivity_occurrence(X0,sK18_skl)
| ~ arboreal(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f521,f273]) ).
fof(f530,plain,
min_precedes(sK16_skl(sK18_skl),sK15_skl(sK18_skl),tptp0),
inference(resolution,[status(thm)],[f470,f216]) ).
fof(f542,plain,
precedes(sK16_skl(sK18_skl),sK15_skl(sK18_skl)),
inference(resolution,[status(thm)],[f530,f106]) ).
fof(f546,plain,
earlier(sK16_skl(sK18_skl),sK15_skl(sK18_skl)),
inference(resolution,[status(thm)],[f542,f82]) ).
fof(f547,plain,
legal(sK15_skl(sK18_skl)),
inference(resolution,[status(thm)],[f542,f83]) ).
fof(f551,plain,
arboreal(sK15_skl(sK18_skl)),
inference(resolution,[status(thm)],[f547,f76]) ).
fof(f560,plain,
( occurrence_of(sK15_skl(sK18_skl),tptp1)
| occurrence_of(sK15_skl(sK18_skl),tptp2) ),
inference(resolution,[status(thm)],[f198,f216]) ).
fof(f593,plain,
! [X0] :
( ~ leaf_occ(sK15_skl(sK18_skl),sK18_skl)
| ~ min_precedes(X0,sK15_skl(sK18_skl),tptp0)
| ~ root_occ(X0,sK18_skl)
| ~ occurrence_of(X0,tptp3)
| occurrence_of(sK15_skl(sK18_skl),tptp2) ),
inference(resolution,[status(thm)],[f560,f218]) ).
fof(f601,plain,
! [X0] :
( ~ leaf_occ(sK15_skl(sK18_skl),sK18_skl)
| ~ min_precedes(X0,sK15_skl(sK18_skl),tptp0)
| ~ root_occ(X0,sK18_skl)
| ~ occurrence_of(X0,tptp3) ),
inference(forward_subsumption_resolution,[status(thm)],[f593,f246]) ).
fof(f673,plain,
! [X0] :
( ~ min_precedes(X0,sK15_skl(sK18_skl),tptp0)
| ~ root_occ(X0,sK18_skl)
| ~ occurrence_of(X0,tptp3) ),
inference(forward_subsumption_resolution,[status(thm)],[f601,f244]) ).
fof(f675,plain,
( ~ min_precedes(sK17_skl(sK18_skl),sK15_skl(sK18_skl),tptp0)
| ~ occurrence_of(sK17_skl(sK18_skl),tptp3) ),
inference(resolution,[status(thm)],[f673,f234]) ).
fof(f678,plain,
~ min_precedes(sK17_skl(sK18_skl),sK15_skl(sK18_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f675,f283]) ).
fof(f2161,plain,
( sK15_skl(sK18_skl) = sK17_skl(sK18_skl)
| min_precedes(sK17_skl(sK18_skl),sK15_skl(sK18_skl),tptp0)
| ~ arboreal(sK15_skl(sK18_skl)) ),
inference(resolution,[status(thm)],[f522,f249]) ).
fof(f2165,plain,
( sK15_skl(sK18_skl) = sK17_skl(sK18_skl)
| min_precedes(sK17_skl(sK18_skl),sK15_skl(sK18_skl),tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2161,f551]) ).
fof(f2244,plain,
~ earlier(sK16_skl(sK18_skl),sK15_skl(sK18_skl)),
inference(backward_demodulation,[status(thm)],[f2281,f498]) ).
fof(f2281,plain,
sK15_skl(sK18_skl) = sK17_skl(sK18_skl),
inference(forward_subsumption_resolution,[status(thm)],[f2165,f678]) ).
fof(f2346,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2244,f546]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO009+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n020.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 03:42:47 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 1.15/0.71 % Refutation found
% 1.15/0.71 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.15/0.71 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.40/0.75 % Elapsed time: 0.370976 seconds
% 0.40/0.75 % CPU time: 2.690323 seconds
% 0.40/0.75 % Total memory used: 131.756 MB
% 0.40/0.75 % Net memory used: 128.803 MB
%------------------------------------------------------------------------------