%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO014+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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 23.40s 18.40s
% Output : CNFRefutation 23.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 13
% Syntax : Number of formulae : 136 ( 33 unt; 0 def)
% Number of atoms : 483 ( 9 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 562 ( 215 ~; 236 |; 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 : 228 ( 203 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X8,X9] :
( earlier(X8,X9)
=> ~ earlier(X9,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X10,X11,X12] :
( ( earlier(X11,X12)
& earlier(X10,X11) )
=> earlier(X10,X12) ),
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(f16,axiom,
! [X38,X39,X40] :
( min_precedes(X38,X39,X40)
=> precedes(X38,X39) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X45,X46,X47,X48] :
( ( precedes(X46,X47)
& min_precedes(X45,X47,X48)
& min_precedes(X45,X46,X48) )
=> min_precedes(X46,X47,X48) ),
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(f30,axiom,
! [X83,X84,X85,X86] :
( ( subactivity_occurrence(X84,X86)
& occurrence_of(X86,X85)
& min_precedes(X83,X84,X85) )
=> subactivity_occurrence(X83,X86) ),
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(f44,axiom,
! [X138,X139,X140,X141] :
( ( ~ min_precedes(X140,X141,X138)
& arboreal(X140)
& leaf_occ(X141,X139)
& subactivity_occurrence(X140,X139)
& occurrence_of(X139,X138) )
=> X141 = X140 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [X145,X146] :
( ( ~ atomic(X146)
& leaf(X145,X146) )
=> ? [X147] :
( leaf_occ(X145,X147)
& occurrence_of(X147,X146) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [X161,X162] :
( ( ~ leaf_occ(X161,X162)
& arboreal(X161)
& subactivity_occurrence(X161,X162)
& occurrence_of(X162,tptp0) )
=> ? [X163,X164,X165] :
( leaf(X165,tptp0)
& next_subocc(X164,X165,tptp0)
& ( occurrence_of(X165,tptp1)
| occurrence_of(X165,tptp2) )
& next_subocc(X163,X164,tptp0)
& occurrence_of(X164,tptp4)
& next_subocc(X161,X163,tptp0)
& occurrence_of(X163,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,conjecture,
! [X166,X167] :
( ( ~ leaf_occ(X166,X167)
& arboreal(X166)
& subactivity_occurrence(X166,X167)
& occurrence_of(X167,tptp0) )
=> ? [X168,X169] :
( leaf(X169,tptp0)
& min_precedes(X168,X169,tptp0)
& ( occurrence_of(X169,tptp1)
| occurrence_of(X169,tptp2) )
& next_subocc(X166,X168,tptp0)
& occurrence_of(X168,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,negated_conjecture,
~ ! [X166,X167] :
( ( ~ leaf_occ(X166,X167)
& arboreal(X166)
& subactivity_occurrence(X166,X167)
& occurrence_of(X167,tptp0) )
=> ? [X168,X169] :
( leaf(X169,tptp0)
& min_precedes(X168,X169,tptp0)
& ( occurrence_of(X169,tptp1)
| occurrence_of(X169,tptp2) )
& next_subocc(X166,X168,tptp0)
& occurrence_of(X168,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f63]) ).
fof(f77,plain,
! [X8,X9] :
( ~ earlier(X9,X8)
| ~ earlier(X8,X9) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f78,plain,
! [X0,X1] :
( ~ earlier(X1,X0)
| ~ earlier(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f79,plain,
! [X10,X11,X12] :
( earlier(X10,X12)
| ~ earlier(X11,X12)
| ~ earlier(X10,X11) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f80,plain,
! [X10,X12] :
( earlier(X10,X12)
| ! [X11] :
( ~ earlier(X11,X12)
| ~ earlier(X10,X11) ) ),
inference(miniscoping,[status(thm)],[f79]) ).
fof(f81,plain,
! [X0,X1,X2] :
( earlier(X0,X2)
| ~ earlier(X1,X2)
| ~ earlier(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f94,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(f95,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)],[f94]) ).
fof(f96,plain,
! [X0,X1] :
( earlier(X0,X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f97,plain,
! [X0,X1] :
( legal(X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f98,plain,
! [X0,X1] :
( ~ legal(X1)
| ~ earlier(X0,X1)
| precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f118,plain,
! [X38,X39,X40] :
( precedes(X38,X39)
| ~ min_precedes(X38,X39,X40) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f119,plain,
! [X38,X39] :
( precedes(X38,X39)
| ! [X40] : ~ min_precedes(X38,X39,X40) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f120,plain,
! [X0,X1,X2] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f126,plain,
! [X45,X46,X47,X48] :
( min_precedes(X46,X47,X48)
| ~ precedes(X46,X47)
| ~ min_precedes(X45,X47,X48)
| ~ min_precedes(X45,X46,X48) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f127,plain,
! [X46,X47,X48] :
( min_precedes(X46,X47,X48)
| ~ precedes(X46,X47)
| ! [X45] :
( ~ min_precedes(X45,X47,X48)
| ~ min_precedes(X45,X46,X48) ) ),
inference(miniscoping,[status(thm)],[f126]) ).
fof(f128,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)],[f127]) ).
fof(f143,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(f144,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)],[f143]) ).
fof(f145,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)],[f144]) ).
fof(f146,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))],[f145]) ).
fof(f147,plain,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f177,plain,
! [X83,X84,X85,X86] :
( subactivity_occurrence(X83,X86)
| ~ subactivity_occurrence(X84,X86)
| ~ occurrence_of(X86,X85)
| ~ min_precedes(X83,X84,X85) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f178,plain,
! [X83,X86] :
( subactivity_occurrence(X83,X86)
| ! [X84] :
( ~ subactivity_occurrence(X84,X86)
| ! [X85] :
( ~ occurrence_of(X86,X85)
| ~ min_precedes(X83,X84,X85) ) ) ),
inference(miniscoping,[status(thm)],[f177]) ).
fof(f179,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)],[f178]) ).
fof(f198,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(f199,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)],[f198]) ).
fof(f200,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))],[f199]) ).
fof(f202,plain,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f229,plain,
! [X138,X139,X140,X141] :
( X141 = X140
| min_precedes(X140,X141,X138)
| ~ arboreal(X140)
| ~ leaf_occ(X141,X139)
| ~ subactivity_occurrence(X140,X139)
| ~ occurrence_of(X139,X138) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f230,plain,
! [X140,X141] :
( X141 = X140
| ! [X138] :
( min_precedes(X140,X141,X138)
| ~ arboreal(X140)
| ! [X139] :
( ~ leaf_occ(X141,X139)
| ~ subactivity_occurrence(X140,X139)
| ~ occurrence_of(X139,X138) ) ) ),
inference(miniscoping,[status(thm)],[f229]) ).
fof(f231,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)],[f230]) ).
fof(f236,plain,
! [X145,X146] :
( ? [X147] :
( leaf_occ(X145,X147)
& occurrence_of(X147,X146) )
| atomic(X146)
| ~ leaf(X145,X146) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f237,plain,
! [X145,X146] :
( ( leaf_occ(X145,sK15_skl(X146,X145))
& occurrence_of(sK15_skl(X146,X145),X146) )
| atomic(X146)
| ~ leaf(X145,X146) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X147,sK15_skl(X146,X145))],[f236]) ).
fof(f238,plain,
! [X0,X1] :
( occurrence_of(sK15_skl(X1,X0),X1)
| atomic(X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f239,plain,
! [X0,X1] :
( leaf_occ(X0,sK15_skl(X1,X0))
| atomic(X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f249,plain,
! [X161,X162] :
( ? [X163,X164,X165] :
( leaf(X165,tptp0)
& next_subocc(X164,X165,tptp0)
& ( occurrence_of(X165,tptp1)
| occurrence_of(X165,tptp2) )
& next_subocc(X163,X164,tptp0)
& occurrence_of(X164,tptp4)
& next_subocc(X161,X163,tptp0)
& occurrence_of(X163,tptp3) )
| leaf_occ(X161,X162)
| ~ arboreal(X161)
| ~ subactivity_occurrence(X161,X162)
| ~ occurrence_of(X162,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f250,plain,
! [X161] :
( ? [X165] :
( leaf(X165,tptp0)
& ? [X164] :
( next_subocc(X164,X165,tptp0)
& ( occurrence_of(X165,tptp1)
| occurrence_of(X165,tptp2) )
& ? [X163] :
( next_subocc(X163,X164,tptp0)
& occurrence_of(X164,tptp4)
& next_subocc(X161,X163,tptp0)
& occurrence_of(X163,tptp3) ) ) )
| ! [X162] :
( leaf_occ(X161,X162)
| ~ arboreal(X161)
| ~ subactivity_occurrence(X161,X162)
| ~ occurrence_of(X162,tptp0) ) ),
inference(miniscoping,[status(thm)],[f249]) ).
fof(f251,plain,
! [X161] :
( ( leaf(sK16_skl(X161),tptp0)
& next_subocc(sK17_skl(X161),sK16_skl(X161),tptp0)
& ( occurrence_of(sK16_skl(X161),tptp1)
| occurrence_of(sK16_skl(X161),tptp2) )
& next_subocc(sK18_skl(X161),sK17_skl(X161),tptp0)
& occurrence_of(sK17_skl(X161),tptp4)
& next_subocc(X161,sK18_skl(X161),tptp0)
& occurrence_of(sK18_skl(X161),tptp3) )
| ! [X162] :
( leaf_occ(X161,X162)
| ~ arboreal(X161)
| ~ subactivity_occurrence(X161,X162)
| ~ occurrence_of(X162,tptp0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl]),skolemize(X165,sK16_skl(X161)),skolemize(X164,sK17_skl(X161)),skolemize(X163,sK18_skl(X161))],[f250]) ).
fof(f252,plain,
! [X0,X1] :
( occurrence_of(sK18_skl(X1),tptp3)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f253,plain,
! [X0,X1] :
( next_subocc(X1,sK18_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f255,plain,
! [X0,X1] :
( next_subocc(sK18_skl(X1),sK17_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f256,plain,
! [X0,X1] :
( occurrence_of(sK16_skl(X1),tptp1)
| occurrence_of(sK16_skl(X1),tptp2)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f257,plain,
! [X0,X1] :
( next_subocc(sK17_skl(X1),sK16_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f258,plain,
! [X0,X1] :
( leaf(sK16_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f260,plain,
~ atomic(tptp0),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f271,plain,
? [X166,X167] :
( ! [X168,X169] :
( ~ leaf(X169,tptp0)
| ~ min_precedes(X168,X169,tptp0)
| ( ~ occurrence_of(X169,tptp1)
& ~ occurrence_of(X169,tptp2) )
| ~ next_subocc(X166,X168,tptp0)
| ~ occurrence_of(X168,tptp3) )
& ~ leaf_occ(X166,X167)
& arboreal(X166)
& subactivity_occurrence(X166,X167)
& occurrence_of(X167,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f272,plain,
? [X166] :
( ! [X169] :
( ~ leaf(X169,tptp0)
| ! [X168] :
( ~ min_precedes(X168,X169,tptp0)
| ( ~ occurrence_of(X169,tptp1)
& ~ occurrence_of(X169,tptp2) )
| ~ next_subocc(X166,X168,tptp0)
| ~ occurrence_of(X168,tptp3) ) )
& ? [X167] :
( ~ leaf_occ(X166,X167)
& arboreal(X166)
& subactivity_occurrence(X166,X167)
& occurrence_of(X167,tptp0) ) ),
inference(miniscoping,[status(thm)],[f271]) ).
fof(f273,plain,
( ! [X169] :
( ~ leaf(X169,tptp0)
| ! [X168] :
( ~ min_precedes(X168,X169,tptp0)
| ( ~ occurrence_of(X169,tptp1)
& ~ occurrence_of(X169,tptp2) )
| ~ next_subocc(sK19_skl,X168,tptp0)
| ~ occurrence_of(X168,tptp3) ) )
& ~ leaf_occ(sK19_skl,sK20_skl)
& arboreal(sK19_skl)
& subactivity_occurrence(sK19_skl,sK20_skl)
& occurrence_of(sK20_skl,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(X166,sK19_skl),skolemize(X167,sK20_skl)],[f272]) ).
fof(f274,plain,
occurrence_of(sK20_skl,tptp0),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f275,plain,
subactivity_occurrence(sK19_skl,sK20_skl),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f276,plain,
arboreal(sK19_skl),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f277,plain,
~ leaf_occ(sK19_skl,sK20_skl),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f278,plain,
! [X0,X1] :
( ~ leaf(X1,tptp0)
| ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp2)
| ~ next_subocc(sK19_skl,X0,tptp0)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f279,plain,
! [X0,X1] :
( ~ leaf(X1,tptp0)
| ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp1)
| ~ next_subocc(sK19_skl,X0,tptp0)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f526,plain,
! [X0] :
( occurrence_of(sK18_skl(X0),tptp3)
| leaf_occ(X0,sK20_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK20_skl) ),
inference(resolution,[status(thm)],[f252,f274]) ).
fof(f529,plain,
( occurrence_of(sK18_skl(sK19_skl),tptp3)
| leaf_occ(sK19_skl,sK20_skl)
| ~ arboreal(sK19_skl) ),
inference(resolution,[status(thm)],[f526,f275]) ).
fof(f531,plain,
( occurrence_of(sK18_skl(sK19_skl),tptp3)
| leaf_occ(sK19_skl,sK20_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f529,f276]) ).
fof(f532,plain,
occurrence_of(sK18_skl(sK19_skl),tptp3),
inference(forward_subsumption_resolution,[status(thm)],[f531,f277]) ).
fof(f670,plain,
! [X0] :
( next_subocc(X0,sK18_skl(X0),tptp0)
| leaf_occ(X0,sK20_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK20_skl) ),
inference(resolution,[status(thm)],[f253,f274]) ).
fof(f678,plain,
! [X0,X1] :
( min_precedes(sK18_skl(X1),sK17_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f255,f147]) ).
fof(f717,plain,
( next_subocc(sK19_skl,sK18_skl(sK19_skl),tptp0)
| leaf_occ(sK19_skl,sK20_skl)
| ~ arboreal(sK19_skl) ),
inference(resolution,[status(thm)],[f670,f275]) ).
fof(f719,plain,
( next_subocc(sK19_skl,sK18_skl(sK19_skl),tptp0)
| leaf_occ(sK19_skl,sK20_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f717,f276]) ).
fof(f728,plain,
next_subocc(sK19_skl,sK18_skl(sK19_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f719,f277]) ).
fof(f734,plain,
min_precedes(sK19_skl,sK18_skl(sK19_skl),tptp0),
inference(resolution,[status(thm)],[f728,f147]) ).
fof(f747,plain,
! [X0] :
( subactivity_occurrence(sK19_skl,X0)
| ~ subactivity_occurrence(sK18_skl(sK19_skl),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f734,f179]) ).
fof(f748,plain,
precedes(sK19_skl,sK18_skl(sK19_skl)),
inference(resolution,[status(thm)],[f734,f120]) ).
fof(f752,plain,
earlier(sK19_skl,sK18_skl(sK19_skl)),
inference(resolution,[status(thm)],[f748,f96]) ).
fof(f815,plain,
! [X0] :
( occurrence_of(sK16_skl(X0),tptp1)
| occurrence_of(sK16_skl(X0),tptp2)
| leaf_occ(X0,sK20_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK20_skl) ),
inference(resolution,[status(thm)],[f256,f274]) ).
fof(f819,plain,
! [X0,X1] :
( min_precedes(sK17_skl(X1),sK16_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f257,f147]) ).
fof(f824,plain,
! [X0] :
( leaf(sK16_skl(X0),tptp0)
| leaf_occ(X0,sK20_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK20_skl) ),
inference(resolution,[status(thm)],[f258,f274]) ).
fof(f836,plain,
( occurrence_of(sK16_skl(sK19_skl),tptp1)
| occurrence_of(sK16_skl(sK19_skl),tptp2)
| leaf_occ(sK19_skl,sK20_skl)
| ~ arboreal(sK19_skl) ),
inference(resolution,[status(thm)],[f815,f275]) ).
fof(f838,plain,
( occurrence_of(sK16_skl(sK19_skl),tptp1)
| occurrence_of(sK16_skl(sK19_skl),tptp2)
| leaf_occ(sK19_skl,sK20_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f836,f276]) ).
fof(f878,plain,
! [X0] :
( min_precedes(sK18_skl(X0),sK17_skl(X0),tptp0)
| leaf_occ(X0,sK20_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK20_skl) ),
inference(resolution,[status(thm)],[f678,f274]) ).
fof(f947,plain,
( leaf(sK16_skl(sK19_skl),tptp0)
| leaf_occ(sK19_skl,sK20_skl)
| ~ arboreal(sK19_skl) ),
inference(resolution,[status(thm)],[f824,f275]) ).
fof(f949,plain,
( leaf(sK16_skl(sK19_skl),tptp0)
| leaf_occ(sK19_skl,sK20_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f947,f276]) ).
fof(f950,plain,
leaf(sK16_skl(sK19_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f949,f277]) ).
fof(f954,plain,
( leaf_occ(sK16_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl)))
| atomic(tptp0) ),
inference(resolution,[status(thm)],[f950,f239]) ).
fof(f955,plain,
( occurrence_of(sK15_skl(tptp0,sK16_skl(sK19_skl)),tptp0)
| atomic(tptp0) ),
inference(resolution,[status(thm)],[f950,f238]) ).
fof(f958,plain,
leaf_occ(sK16_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f954,f260]) ).
fof(f959,plain,
occurrence_of(sK15_skl(tptp0,sK16_skl(sK19_skl)),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f955,f260]) ).
fof(f986,plain,
! [X0,X1] :
( sK16_skl(sK19_skl) = X1
| min_precedes(X1,sK16_skl(sK19_skl),X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,sK15_skl(tptp0,sK16_skl(sK19_skl)))
| ~ occurrence_of(sK15_skl(tptp0,sK16_skl(sK19_skl)),X0) ),
inference(resolution,[status(thm)],[f958,f231]) ).
fof(f988,plain,
subactivity_occurrence(sK16_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl))),
inference(resolution,[status(thm)],[f958,f202]) ).
fof(f996,plain,
( min_precedes(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)
| leaf_occ(sK19_skl,sK20_skl)
| ~ arboreal(sK19_skl)
| ~ occurrence_of(sK20_skl,tptp0) ),
inference(resolution,[status(thm)],[f819,f275]) ).
fof(f1001,plain,
( min_precedes(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)
| leaf_occ(sK19_skl,sK20_skl)
| ~ arboreal(sK19_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f996,f274]) ).
fof(f1053,plain,
( occurrence_of(sK16_skl(sK19_skl),tptp1)
| occurrence_of(sK16_skl(sK19_skl),tptp2) ),
inference(forward_subsumption_resolution,[status(thm)],[f838,f277]) ).
fof(f1054,plain,
! [X0] :
( ~ leaf(sK16_skl(sK19_skl),tptp0)
| ~ min_precedes(X0,sK16_skl(sK19_skl),tptp0)
| ~ next_subocc(sK19_skl,X0,tptp0)
| ~ occurrence_of(X0,tptp3)
| occurrence_of(sK16_skl(sK19_skl),tptp2) ),
inference(resolution,[status(thm)],[f1053,f279]) ).
fof(f1060,plain,
! [X0] :
( ~ leaf(sK16_skl(sK19_skl),tptp0)
| ~ min_precedes(X0,sK16_skl(sK19_skl),tptp0)
| ~ next_subocc(sK19_skl,X0,tptp0)
| ~ occurrence_of(X0,tptp3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1054,f278]) ).
fof(f1064,plain,
( min_precedes(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)
| leaf_occ(sK19_skl,sK20_skl)
| ~ arboreal(sK19_skl) ),
inference(resolution,[status(thm)],[f878,f275]) ).
fof(f1066,plain,
( min_precedes(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)
| leaf_occ(sK19_skl,sK20_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1064,f276]) ).
fof(f1100,plain,
( min_precedes(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)
| leaf_occ(sK19_skl,sK20_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1001,f276]) ).
fof(f1101,plain,
min_precedes(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0),
inference(resolution,[status(thm)],[f1100,f277]) ).
fof(f1120,plain,
! [X0] :
( subactivity_occurrence(sK17_skl(sK19_skl),X0)
| ~ subactivity_occurrence(sK16_skl(sK19_skl),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f1101,f179]) ).
fof(f1121,plain,
precedes(sK17_skl(sK19_skl),sK16_skl(sK19_skl)),
inference(resolution,[status(thm)],[f1101,f120]) ).
fof(f1125,plain,
earlier(sK17_skl(sK19_skl),sK16_skl(sK19_skl)),
inference(resolution,[status(thm)],[f1121,f96]) ).
fof(f1126,plain,
legal(sK16_skl(sK19_skl)),
inference(resolution,[status(thm)],[f1121,f97]) ).
fof(f1128,plain,
! [X0] :
( ~ earlier(X0,sK16_skl(sK19_skl))
| precedes(X0,sK16_skl(sK19_skl)) ),
inference(resolution,[status(thm)],[f1126,f98]) ).
fof(f1132,plain,
! [X0] :
( earlier(X0,sK16_skl(sK19_skl))
| ~ earlier(X0,sK17_skl(sK19_skl)) ),
inference(resolution,[status(thm)],[f1125,f81]) ).
fof(f1353,plain,
min_precedes(sK18_skl(sK19_skl),sK17_skl(sK19_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f1066,f277]) ).
fof(f1365,plain,
! [X0] :
( subactivity_occurrence(sK18_skl(sK19_skl),X0)
| ~ subactivity_occurrence(sK17_skl(sK19_skl),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f1353,f179]) ).
fof(f1366,plain,
precedes(sK18_skl(sK19_skl),sK17_skl(sK19_skl)),
inference(resolution,[status(thm)],[f1353,f120]) ).
fof(f1371,plain,
earlier(sK18_skl(sK19_skl),sK17_skl(sK19_skl)),
inference(resolution,[status(thm)],[f1366,f96]) ).
fof(f1374,plain,
earlier(sK18_skl(sK19_skl),sK16_skl(sK19_skl)),
inference(resolution,[status(thm)],[f1371,f1132]) ).
fof(f1379,plain,
precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl)),
inference(resolution,[status(thm)],[f1374,f1128]) ).
fof(f1383,plain,
~ earlier(sK16_skl(sK19_skl),sK18_skl(sK19_skl)),
inference(resolution,[status(thm)],[f1374,f78]) ).
fof(f1391,plain,
! [X0,X1] :
( min_precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl),X1)
| ~ min_precedes(X0,sK16_skl(sK19_skl),X1)
| ~ min_precedes(X0,sK18_skl(sK19_skl),X1) ),
inference(resolution,[status(thm)],[f1379,f128]) ).
fof(f1625,plain,
! [X0] :
( ~ min_precedes(X0,sK16_skl(sK19_skl),tptp0)
| ~ next_subocc(sK19_skl,X0,tptp0)
| ~ occurrence_of(X0,tptp3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1060,f950]) ).
fof(f1626,plain,
( ~ min_precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)
| ~ occurrence_of(sK18_skl(sK19_skl),tptp3) ),
inference(resolution,[status(thm)],[f1625,f728]) ).
fof(f1627,plain,
~ min_precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f1626,f532]) ).
fof(f1785,plain,
( subactivity_occurrence(sK17_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl)))
| ~ occurrence_of(sK15_skl(tptp0,sK16_skl(sK19_skl)),tptp0) ),
inference(resolution,[status(thm)],[f1120,f988]) ).
fof(f1786,plain,
subactivity_occurrence(sK17_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f1785,f959]) ).
fof(f1804,plain,
( subactivity_occurrence(sK18_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl)))
| ~ occurrence_of(sK15_skl(tptp0,sK16_skl(sK19_skl)),tptp0) ),
inference(resolution,[status(thm)],[f1365,f1786]) ).
fof(f1807,plain,
subactivity_occurrence(sK18_skl(sK19_skl),sK15_skl(tptp0,sK16_skl(sK19_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f1804,f959]) ).
fof(f1809,plain,
( subactivity_occurrence(sK19_skl,sK15_skl(tptp0,sK16_skl(sK19_skl)))
| ~ occurrence_of(sK15_skl(tptp0,sK16_skl(sK19_skl)),tptp0) ),
inference(resolution,[status(thm)],[f1807,f747]) ).
fof(f1817,plain,
subactivity_occurrence(sK19_skl,sK15_skl(tptp0,sK16_skl(sK19_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f1809,f959]) ).
fof(f3366,plain,
! [X0] :
( sK16_skl(sK19_skl) = X0
| min_precedes(X0,sK16_skl(sK19_skl),tptp0)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK15_skl(tptp0,sK16_skl(sK19_skl))) ),
inference(resolution,[status(thm)],[f986,f959]) ).
fof(f7712,plain,
( min_precedes(sK18_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)
| ~ min_precedes(sK19_skl,sK16_skl(sK19_skl),tptp0) ),
inference(resolution,[status(thm)],[f1391,f734]) ).
fof(f7714,plain,
~ min_precedes(sK19_skl,sK16_skl(sK19_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f7712,f1627]) ).
fof(f9812,plain,
( sK16_skl(sK19_skl) = sK19_skl
| min_precedes(sK19_skl,sK16_skl(sK19_skl),tptp0)
| ~ arboreal(sK19_skl) ),
inference(resolution,[status(thm)],[f3366,f1817]) ).
fof(f9819,plain,
( sK16_skl(sK19_skl) = sK19_skl
| min_precedes(sK19_skl,sK16_skl(sK19_skl),tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f9812,f276]) ).
fof(f10203,plain,
~ earlier(sK19_skl,sK18_skl(sK19_skl)),
inference(backward_demodulation,[status(thm)],[f10259,f1383]) ).
fof(f10259,plain,
sK16_skl(sK19_skl) = sK19_skl,
inference(forward_subsumption_resolution,[status(thm)],[f9819,f7714]) ).
fof(f10653,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f10203,f752]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO014+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/15.37 % Computer : n012.cluster.edu
% 0.10/15.37 % Model : x86_64 x86_64
% 0.10/15.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/15.37 % Memory : 8046.5625MB
% 0.10/15.37 % OS : Linux 6.8.0-71-generic
% 0.10/15.37 % CPULimit : 300
% 0.10/15.37 % WCLimit : 300
% 0.10/15.37 % DateTime : Mon Sep 21 03:42:52 UTC 2026
% 0.10/15.37 % CPUTime :
% 0.10/15.38 % Drodi V4.1.1
% 23.40/18.40 % Refutation found
% 23.40/18.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 23.40/18.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 23.40/18.46 % Elapsed time: 3.069707 seconds
% 23.40/18.46 % CPU time: 24.037884 seconds
% 23.40/18.46 % Total memory used: 282.719 MB
% 23.40/18.46 % Net memory used: 266.427 MB
%------------------------------------------------------------------------------