%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO014+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:18 PM UTC 2026
% Result : Theorem 2.91s 1.11s
% Output : CNFRefutation 2.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 13
% Syntax : Number of formulae : 136 ( 35 unt; 0 def)
% Number of atoms : 475 ( 9 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 548 ( 209 ~; 228 |; 97 &)
% ( 4 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-3 aty)
% Number of variables : 225 ( 200 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X8,X9,X10,X11] :
( ( ~ min_precedes(X10,X11,X8)
& arboreal(X10)
& leaf_occ(X11,X9)
& subactivity_occurrence(X10,X9)
& occurrence_of(X9,X8) )
=> X11 = X10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X25,X26] :
( ( ~ atomic(X26)
& leaf(X25,X26) )
=> ? [X27] :
( leaf_occ(X25,X27)
& occurrence_of(X27,X26) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X61,X62] :
( earlier(X61,X62)
=> ~ earlier(X62,X61) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X63,X64] :
( precedes(X63,X64)
<=> ( legal(X64)
& earlier(X63,X64) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X72,X73,X74] :
( min_precedes(X72,X73,X74)
=> precedes(X72,X73) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [X94,X95,X96] :
( ( earlier(X95,X96)
& earlier(X94,X95) )
=> earlier(X94,X96) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [X97,X98,X99,X100] :
( ( precedes(X98,X99)
& min_precedes(X97,X99,X100)
& min_precedes(X97,X98,X100) )
=> min_precedes(X98,X99,X100) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X101,X102] :
( ( ~ leaf_occ(X101,X102)
& arboreal(X101)
& subactivity_occurrence(X101,X102)
& occurrence_of(X102,tptp0) )
=> ? [X103,X104,X105] :
( leaf(X105,tptp0)
& next_subocc(X104,X105,tptp0)
& ( occurrence_of(X105,tptp1)
| occurrence_of(X105,tptp2) )
& next_subocc(X103,X104,tptp0)
& occurrence_of(X104,tptp4)
& next_subocc(X101,X103,tptp0)
& occurrence_of(X103,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,conjecture,
! [X106,X107] :
( ( ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) )
=> ? [X108,X109] :
( leaf(X109,tptp0)
& min_precedes(X108,X109,tptp0)
& ( occurrence_of(X109,tptp1)
| occurrence_of(X109,tptp2) )
& next_subocc(X106,X108,tptp0)
& occurrence_of(X108,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
~ ! [X106,X107] :
( ( ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) )
=> ? [X108,X109] :
( leaf(X109,tptp0)
& min_precedes(X108,X109,tptp0)
& ( occurrence_of(X109,tptp1)
| occurrence_of(X109,tptp2) )
& next_subocc(X106,X108,tptp0)
& occurrence_of(X108,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f55,plain,
! [X8,X9,X10,X11] :
( X11 = X10
| min_precedes(X10,X11,X8)
| ~ arboreal(X10)
| ~ leaf_occ(X11,X9)
| ~ subactivity_occurrence(X10,X9)
| ~ occurrence_of(X9,X8) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f56,plain,
! [X10,X11] :
( X11 = X10
| ! [X8] :
( min_precedes(X10,X11,X8)
| ~ arboreal(X10)
| ! [X9] :
( ~ leaf_occ(X11,X9)
| ~ subactivity_occurrence(X10,X9)
| ~ occurrence_of(X9,X8) ) ) ),
inference(miniscoping,[status(thm)],[f55]) ).
fof(f57,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| min_precedes(X2,X3,X1)
| ~ arboreal(X2)
| ~ leaf_occ(X3,X0)
| ~ subactivity_occurrence(X2,X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f73,plain,
! [X25,X26] :
( ? [X27] :
( leaf_occ(X25,X27)
& occurrence_of(X27,X26) )
| atomic(X26)
| ~ leaf(X25,X26) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f74,plain,
! [X25,X26] :
( ( leaf_occ(X25,sK3_skl(X26,X25))
& occurrence_of(sK3_skl(X26,X25),X26) )
| atomic(X26)
| ~ leaf(X25,X26) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X27,sK3_skl(X26,X25))],[f73]) ).
fof(f75,plain,
! [X0,X1] :
( occurrence_of(sK3_skl(X1,X0),X1)
| atomic(X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f76,plain,
! [X0,X1] :
( leaf_occ(X0,sK3_skl(X1,X0))
| atomic(X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
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(f131,plain,
! [X61,X62] :
( ~ earlier(X62,X61)
| ~ earlier(X61,X62) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f132,plain,
! [X0,X1] :
( ~ earlier(X1,X0)
| ~ earlier(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
! [X63,X64] :
( ( ~ legal(X64)
| ~ earlier(X63,X64)
| precedes(X63,X64) )
& ( ( legal(X64)
& earlier(X63,X64) )
| ~ precedes(X63,X64) ) ),
inference(NNF_transformation,[status(thm)],[f22]) ).
fof(f134,plain,
( ! [X63,X64] :
( ~ legal(X64)
| ~ earlier(X63,X64)
| precedes(X63,X64) )
& ! [X63,X64] :
( ( legal(X64)
& earlier(X63,X64) )
| ~ precedes(X63,X64) ) ),
inference(miniscoping,[status(thm)],[f133]) ).
fof(f135,plain,
! [X0,X1] :
( earlier(X0,X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f136,plain,
! [X0,X1] :
( legal(X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f137,plain,
! [X0,X1] :
( ~ legal(X1)
| ~ earlier(X0,X1)
| precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f146,plain,
! [X72,X73,X74] :
( precedes(X72,X73)
| ~ min_precedes(X72,X73,X74) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f147,plain,
! [X72,X73] :
( precedes(X72,X73)
| ! [X74] : ~ min_precedes(X72,X73,X74) ),
inference(miniscoping,[status(thm)],[f146]) ).
fof(f148,plain,
! [X0,X1,X2] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
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(f170,plain,
! [X94,X95,X96] :
( earlier(X94,X96)
| ~ earlier(X95,X96)
| ~ earlier(X94,X95) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f171,plain,
! [X94,X96] :
( earlier(X94,X96)
| ! [X95] :
( ~ earlier(X95,X96)
| ~ earlier(X94,X95) ) ),
inference(miniscoping,[status(thm)],[f170]) ).
fof(f172,plain,
! [X0,X1,X2] :
( earlier(X0,X2)
| ~ earlier(X1,X2)
| ~ earlier(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f173,plain,
! [X97,X98,X99,X100] :
( min_precedes(X98,X99,X100)
| ~ precedes(X98,X99)
| ~ min_precedes(X97,X99,X100)
| ~ min_precedes(X97,X98,X100) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f174,plain,
! [X98,X99,X100] :
( min_precedes(X98,X99,X100)
| ~ precedes(X98,X99)
| ! [X97] :
( ~ min_precedes(X97,X99,X100)
| ~ min_precedes(X97,X98,X100) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( min_precedes(X1,X3,X2)
| ~ precedes(X1,X3)
| ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f176,plain,
! [X101,X102] :
( ? [X103,X104,X105] :
( leaf(X105,tptp0)
& next_subocc(X104,X105,tptp0)
& ( occurrence_of(X105,tptp1)
| occurrence_of(X105,tptp2) )
& next_subocc(X103,X104,tptp0)
& occurrence_of(X104,tptp4)
& next_subocc(X101,X103,tptp0)
& occurrence_of(X103,tptp3) )
| leaf_occ(X101,X102)
| ~ arboreal(X101)
| ~ subactivity_occurrence(X101,X102)
| ~ occurrence_of(X102,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f177,plain,
! [X101] :
( ? [X105] :
( leaf(X105,tptp0)
& ? [X104] :
( next_subocc(X104,X105,tptp0)
& ( occurrence_of(X105,tptp1)
| occurrence_of(X105,tptp2) )
& ? [X103] :
( next_subocc(X103,X104,tptp0)
& occurrence_of(X104,tptp4)
& next_subocc(X101,X103,tptp0)
& occurrence_of(X103,tptp3) ) ) )
| ! [X102] :
( leaf_occ(X101,X102)
| ~ arboreal(X101)
| ~ subactivity_occurrence(X101,X102)
| ~ occurrence_of(X102,tptp0) ) ),
inference(miniscoping,[status(thm)],[f176]) ).
fof(f178,plain,
! [X101] :
( ( leaf(sK12_skl(X101),tptp0)
& 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)
& next_subocc(X101,sK14_skl(X101),tptp0)
& occurrence_of(sK14_skl(X101),tptp3) )
| ! [X102] :
( leaf_occ(X101,X102)
| ~ arboreal(X101)
| ~ subactivity_occurrence(X101,X102)
| ~ occurrence_of(X102,tptp0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(X105,sK12_skl(X101)),skolemize(X104,sK13_skl(X101)),skolemize(X103,sK14_skl(X101))],[f177]) ).
fof(f179,plain,
! [X0,X1] :
( occurrence_of(sK14_skl(X1),tptp3)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f180,plain,
! [X0,X1] :
( next_subocc(X1,sK14_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f182,plain,
! [X0,X1] :
( next_subocc(sK14_skl(X1),sK13_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f183,plain,
! [X0,X1] :
( occurrence_of(sK12_skl(X1),tptp1)
| occurrence_of(sK12_skl(X1),tptp2)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f184,plain,
! [X0,X1] :
( next_subocc(sK13_skl(X1),sK12_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f185,plain,
! [X0,X1] :
( leaf(sK12_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f187,plain,
~ atomic(tptp0),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f198,plain,
? [X106,X107] :
( ! [X108,X109] :
( ~ leaf(X109,tptp0)
| ~ min_precedes(X108,X109,tptp0)
| ( ~ occurrence_of(X109,tptp1)
& ~ occurrence_of(X109,tptp2) )
| ~ next_subocc(X106,X108,tptp0)
| ~ occurrence_of(X108,tptp3) )
& ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f199,plain,
? [X106] :
( ! [X109] :
( ~ leaf(X109,tptp0)
| ! [X108] :
( ~ min_precedes(X108,X109,tptp0)
| ( ~ occurrence_of(X109,tptp1)
& ~ occurrence_of(X109,tptp2) )
| ~ next_subocc(X106,X108,tptp0)
| ~ occurrence_of(X108,tptp3) ) )
& ? [X107] :
( ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) ) ),
inference(miniscoping,[status(thm)],[f198]) ).
fof(f200,plain,
( ! [X109] :
( ~ leaf(X109,tptp0)
| ! [X108] :
( ~ min_precedes(X108,X109,tptp0)
| ( ~ occurrence_of(X109,tptp1)
& ~ occurrence_of(X109,tptp2) )
| ~ next_subocc(sK15_skl,X108,tptp0)
| ~ occurrence_of(X108,tptp3) ) )
& ~ leaf_occ(sK15_skl,sK16_skl)
& arboreal(sK15_skl)
& subactivity_occurrence(sK15_skl,sK16_skl)
& occurrence_of(sK16_skl,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(X106,sK15_skl),skolemize(X107,sK16_skl)],[f199]) ).
fof(f201,plain,
occurrence_of(sK16_skl,tptp0),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f202,plain,
subactivity_occurrence(sK15_skl,sK16_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f203,plain,
arboreal(sK15_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f204,plain,
~ leaf_occ(sK15_skl,sK16_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f205,plain,
! [X0,X1] :
( ~ leaf(X1,tptp0)
| ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp2)
| ~ next_subocc(sK15_skl,X0,tptp0)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f206,plain,
! [X0,X1] :
( ~ leaf(X1,tptp0)
| ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp1)
| ~ next_subocc(sK15_skl,X0,tptp0)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f308,plain,
! [X0] :
( occurrence_of(sK14_skl(X0),tptp3)
| leaf_occ(X0,sK16_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f179,f201]) ).
fof(f309,plain,
! [X0] :
( next_subocc(X0,sK14_skl(X0),tptp0)
| leaf_occ(X0,sK16_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f180,f201]) ).
fof(f312,plain,
( occurrence_of(sK14_skl(sK15_skl),tptp3)
| leaf_occ(sK15_skl,sK16_skl)
| ~ subactivity_occurrence(sK15_skl,sK16_skl) ),
inference(resolution,[status(thm)],[f308,f203]) ).
fof(f313,plain,
( occurrence_of(sK14_skl(sK15_skl),tptp3)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f312,f202]) ).
fof(f314,plain,
occurrence_of(sK14_skl(sK15_skl),tptp3),
inference(forward_subsumption_resolution,[status(thm)],[f313,f204]) ).
fof(f323,plain,
( next_subocc(sK15_skl,sK14_skl(sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl)
| ~ subactivity_occurrence(sK15_skl,sK16_skl) ),
inference(resolution,[status(thm)],[f309,f203]) ).
fof(f324,plain,
( next_subocc(sK15_skl,sK14_skl(sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f323,f202]) ).
fof(f346,plain,
next_subocc(sK15_skl,sK14_skl(sK15_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f324,f204]) ).
fof(f350,plain,
min_precedes(sK15_skl,sK14_skl(sK15_skl),tptp0),
inference(resolution,[status(thm)],[f346,f157]) ).
fof(f365,plain,
precedes(sK15_skl,sK14_skl(sK15_skl)),
inference(resolution,[status(thm)],[f350,f148]) ).
fof(f368,plain,
! [X0] :
( subactivity_occurrence(sK15_skl,X0)
| ~ subactivity_occurrence(sK14_skl(sK15_skl),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f350,f163]) ).
fof(f371,plain,
earlier(sK15_skl,sK14_skl(sK15_skl)),
inference(resolution,[status(thm)],[f365,f135]) ).
fof(f381,plain,
! [X0] :
( next_subocc(sK14_skl(X0),sK13_skl(X0),tptp0)
| leaf_occ(X0,sK16_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f182,f201]) ).
fof(f382,plain,
! [X0] :
( occurrence_of(sK12_skl(X0),tptp1)
| occurrence_of(sK12_skl(X0),tptp2)
| leaf_occ(X0,sK16_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f183,f201]) ).
fof(f383,plain,
! [X0] :
( next_subocc(sK13_skl(X0),sK12_skl(X0),tptp0)
| leaf_occ(X0,sK16_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f184,f201]) ).
fof(f393,plain,
( next_subocc(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl) ),
inference(resolution,[status(thm)],[f381,f202]) ).
fof(f395,plain,
( next_subocc(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f393,f203]) ).
fof(f414,plain,
( occurrence_of(sK12_skl(sK15_skl),tptp1)
| occurrence_of(sK12_skl(sK15_skl),tptp2)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl) ),
inference(resolution,[status(thm)],[f382,f202]) ).
fof(f416,plain,
( occurrence_of(sK12_skl(sK15_skl),tptp1)
| occurrence_of(sK12_skl(sK15_skl),tptp2)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f414,f203]) ).
fof(f418,plain,
( next_subocc(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl) ),
inference(resolution,[status(thm)],[f383,f202]) ).
fof(f420,plain,
( next_subocc(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f418,f203]) ).
fof(f454,plain,
! [X0] :
( leaf(sK12_skl(X0),tptp0)
| leaf_occ(X0,sK16_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f185,f201]) ).
fof(f468,plain,
( leaf(sK12_skl(sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl) ),
inference(resolution,[status(thm)],[f454,f202]) ).
fof(f470,plain,
( leaf(sK12_skl(sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f468,f203]) ).
fof(f471,plain,
leaf(sK12_skl(sK15_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f470,f204]) ).
fof(f475,plain,
( leaf_occ(sK12_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl)))
| atomic(tptp0) ),
inference(resolution,[status(thm)],[f471,f76]) ).
fof(f476,plain,
( occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),tptp0)
| atomic(tptp0) ),
inference(resolution,[status(thm)],[f471,f75]) ).
fof(f479,plain,
leaf_occ(sK12_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f475,f187]) ).
fof(f480,plain,
occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f476,f187]) ).
fof(f503,plain,
subactivity_occurrence(sK12_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl))),
inference(resolution,[status(thm)],[f479,f121]) ).
fof(f505,plain,
! [X0,X1] :
( sK12_skl(sK15_skl) = X1
| min_precedes(X1,sK12_skl(sK15_skl),X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,sK3_skl(tptp0,sK12_skl(sK15_skl)))
| ~ occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),X0) ),
inference(resolution,[status(thm)],[f479,f57]) ).
fof(f562,plain,
next_subocc(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f395,f204]) ).
fof(f564,plain,
min_precedes(sK14_skl(sK15_skl),sK13_skl(sK15_skl),tptp0),
inference(resolution,[status(thm)],[f562,f157]) ).
fof(f573,plain,
precedes(sK14_skl(sK15_skl),sK13_skl(sK15_skl)),
inference(resolution,[status(thm)],[f564,f148]) ).
fof(f576,plain,
! [X0] :
( subactivity_occurrence(sK14_skl(sK15_skl),X0)
| ~ subactivity_occurrence(sK13_skl(sK15_skl),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f564,f163]) ).
fof(f579,plain,
earlier(sK14_skl(sK15_skl),sK13_skl(sK15_skl)),
inference(resolution,[status(thm)],[f573,f135]) ).
fof(f587,plain,
( occurrence_of(sK12_skl(sK15_skl),tptp1)
| occurrence_of(sK12_skl(sK15_skl),tptp2) ),
inference(forward_subsumption_resolution,[status(thm)],[f416,f204]) ).
fof(f589,plain,
! [X0] :
( ~ leaf(sK12_skl(sK15_skl),tptp0)
| ~ min_precedes(X0,sK12_skl(sK15_skl),tptp0)
| ~ next_subocc(sK15_skl,X0,tptp0)
| ~ occurrence_of(X0,tptp3)
| occurrence_of(sK12_skl(sK15_skl),tptp2) ),
inference(resolution,[status(thm)],[f587,f206]) ).
fof(f598,plain,
! [X0] :
( ~ leaf(sK12_skl(sK15_skl),tptp0)
| ~ min_precedes(X0,sK12_skl(sK15_skl),tptp0)
| ~ next_subocc(sK15_skl,X0,tptp0)
| ~ occurrence_of(X0,tptp3) ),
inference(forward_subsumption_resolution,[status(thm)],[f589,f205]) ).
fof(f638,plain,
next_subocc(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f420,f204]) ).
fof(f640,plain,
min_precedes(sK13_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),
inference(resolution,[status(thm)],[f638,f157]) ).
fof(f672,plain,
precedes(sK13_skl(sK15_skl),sK12_skl(sK15_skl)),
inference(resolution,[status(thm)],[f640,f148]) ).
fof(f675,plain,
! [X0] :
( subactivity_occurrence(sK13_skl(sK15_skl),X0)
| ~ subactivity_occurrence(sK12_skl(sK15_skl),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f640,f163]) ).
fof(f678,plain,
earlier(sK13_skl(sK15_skl),sK12_skl(sK15_skl)),
inference(resolution,[status(thm)],[f672,f135]) ).
fof(f679,plain,
legal(sK12_skl(sK15_skl)),
inference(resolution,[status(thm)],[f672,f136]) ).
fof(f680,plain,
! [X0] :
( ~ earlier(X0,sK12_skl(sK15_skl))
| precedes(X0,sK12_skl(sK15_skl)) ),
inference(resolution,[status(thm)],[f679,f137]) ).
fof(f682,plain,
! [X0] :
( earlier(X0,sK12_skl(sK15_skl))
| ~ earlier(X0,sK13_skl(sK15_skl)) ),
inference(resolution,[status(thm)],[f678,f172]) ).
fof(f728,plain,
earlier(sK14_skl(sK15_skl),sK12_skl(sK15_skl)),
inference(resolution,[status(thm)],[f682,f579]) ).
fof(f749,plain,
precedes(sK14_skl(sK15_skl),sK12_skl(sK15_skl)),
inference(resolution,[status(thm)],[f728,f680]) ).
fof(f751,plain,
~ earlier(sK12_skl(sK15_skl),sK14_skl(sK15_skl)),
inference(resolution,[status(thm)],[f728,f132]) ).
fof(f752,plain,
! [X0,X1] :
( min_precedes(sK14_skl(sK15_skl),sK12_skl(sK15_skl),X1)
| ~ min_precedes(X0,sK12_skl(sK15_skl),X1)
| ~ min_precedes(X0,sK14_skl(sK15_skl),X1) ),
inference(resolution,[status(thm)],[f749,f175]) ).
fof(f858,plain,
! [X0] :
( ~ min_precedes(X0,sK12_skl(sK15_skl),tptp0)
| ~ next_subocc(sK15_skl,X0,tptp0)
| ~ occurrence_of(X0,tptp3) ),
inference(forward_subsumption_resolution,[status(thm)],[f598,f471]) ).
fof(f859,plain,
( ~ min_precedes(sK14_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)
| ~ occurrence_of(sK14_skl(sK15_skl),tptp3) ),
inference(resolution,[status(thm)],[f858,f346]) ).
fof(f860,plain,
~ min_precedes(sK14_skl(sK15_skl),sK12_skl(sK15_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f859,f314]) ).
fof(f1136,plain,
( subactivity_occurrence(sK13_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl)))
| ~ occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),tptp0) ),
inference(resolution,[status(thm)],[f675,f503]) ).
fof(f1137,plain,
subactivity_occurrence(sK13_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f1136,f480]) ).
fof(f1138,plain,
( subactivity_occurrence(sK14_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl)))
| ~ occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),tptp0) ),
inference(resolution,[status(thm)],[f1137,f576]) ).
fof(f1141,plain,
subactivity_occurrence(sK14_skl(sK15_skl),sK3_skl(tptp0,sK12_skl(sK15_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f1138,f480]) ).
fof(f1142,plain,
( subactivity_occurrence(sK15_skl,sK3_skl(tptp0,sK12_skl(sK15_skl)))
| ~ occurrence_of(sK3_skl(tptp0,sK12_skl(sK15_skl)),tptp0) ),
inference(resolution,[status(thm)],[f1141,f368]) ).
fof(f1145,plain,
subactivity_occurrence(sK15_skl,sK3_skl(tptp0,sK12_skl(sK15_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f1142,f480]) ).
fof(f1553,plain,
! [X0] :
( sK12_skl(sK15_skl) = X0
| min_precedes(X0,sK12_skl(sK15_skl),tptp0)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK3_skl(tptp0,sK12_skl(sK15_skl))) ),
inference(resolution,[status(thm)],[f505,f480]) ).
fof(f2798,plain,
( min_precedes(sK14_skl(sK15_skl),sK12_skl(sK15_skl),tptp0)
| ~ min_precedes(sK15_skl,sK12_skl(sK15_skl),tptp0) ),
inference(resolution,[status(thm)],[f752,f350]) ).
fof(f2800,plain,
~ min_precedes(sK15_skl,sK12_skl(sK15_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f2798,f860]) ).
fof(f3138,plain,
( sK12_skl(sK15_skl) = sK15_skl
| min_precedes(sK15_skl,sK12_skl(sK15_skl),tptp0)
| ~ arboreal(sK15_skl) ),
inference(resolution,[status(thm)],[f1553,f1145]) ).
fof(f3145,plain,
( sK12_skl(sK15_skl) = sK15_skl
| min_precedes(sK15_skl,sK12_skl(sK15_skl),tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3138,f203]) ).
fof(f3336,plain,
~ earlier(sK15_skl,sK14_skl(sK15_skl)),
inference(backward_demodulation,[status(thm)],[f3375,f751]) ).
fof(f3375,plain,
sK12_skl(sK15_skl) = sK15_skl,
inference(forward_subsumption_resolution,[status(thm)],[f3145,f2800]) ).
fof(f3513,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f3336,f371]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO014+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n018.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 03:44:59 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.02/0.38 % Drodi V4.1.1
% 2.91/1.11 % Refutation found
% 2.91/1.11 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.91/1.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.91/1.15 % Elapsed time: 0.772054 seconds
% 2.91/1.15 % CPU time: 5.689378 seconds
% 2.91/1.15 % Total memory used: 129.859 MB
% 2.91/1.15 % Net memory used: 125.143 MB
%------------------------------------------------------------------------------