%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO017+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:19 PM UTC 2026
% Result : Theorem 124.01s 21.68s
% Output : CNFRefutation 124.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 13
% Syntax : Number of formulae : 116 ( 29 unt; 0 def)
% Number of atoms : 394 ( 53 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 425 ( 147 ~; 182 |; 82 &)
% ( 4 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-3 aty)
% Number of variables : 158 ( 133 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity_occurrence(X1)
& activity(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X2] :
( activity_occurrence(X2)
=> ? [X3] :
( occurrence_of(X2,X3)
& activity(X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X4,X5,X6] :
( ( occurrence_of(X4,X6)
& occurrence_of(X4,X5) )
=> X5 = X6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X16,X17] :
( occurrence_of(X16,X17)
=> ( arboreal(X16)
<=> atomic(X17) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X69,X70,X71] :
( min_precedes(X70,X71,X69)
=> ? [X72] :
( subactivity_occurrence(X71,X72)
& subactivity_occurrence(X70,X72)
& occurrence_of(X72,X69) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [X113,X114,X115] :
( ( leaf_occ(X114,X113)
& occurrence_of(X113,X115) )
=> ~ ? [X116] : min_precedes(X114,X116,X115) ),
file('/export/starexec/sandbox2/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] :
( ! [X166] :
( min_precedes(X163,X166,tptp0)
=> ( X166 = X165
| X166 = X164 ) )
& min_precedes(X164,X165,tptp0)
& ( occurrence_of(X165,tptp1)
| occurrence_of(X165,tptp2) )
& min_precedes(X163,X164,tptp0)
& occurrence_of(X164,tptp4)
& next_subocc(X161,X163,tptp0)
& occurrence_of(X163,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
atomic(tptp3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
tptp4 != tptp3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
tptp3 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
tptp3 != tptp1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,conjecture,
! [X167,X168] :
( ( ~ leaf_occ(X167,X168)
& arboreal(X167)
& subactivity_occurrence(X167,X168)
& occurrence_of(X168,tptp0) )
=> ? [X169,X170] :
( leaf(X170,tptp0)
& min_precedes(X169,X170,tptp0)
& ( occurrence_of(X170,tptp1)
| occurrence_of(X170,tptp2) )
& next_subocc(X167,X169,tptp0)
& occurrence_of(X169,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,negated_conjecture,
~ ! [X167,X168] :
( ( ~ leaf_occ(X167,X168)
& arboreal(X167)
& subactivity_occurrence(X167,X168)
& occurrence_of(X168,tptp0) )
=> ? [X169,X170] :
( leaf(X170,tptp0)
& min_precedes(X169,X170,tptp0)
& ( occurrence_of(X170,tptp1)
| occurrence_of(X170,tptp2) )
& next_subocc(X167,X169,tptp0)
& occurrence_of(X169,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f63]) ).
fof(f65,plain,
! [X0,X1] :
( ( activity_occurrence(X1)
& activity(X0) )
| ~ occurrence_of(X1,X0) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f67,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| activity_occurrence(X0) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f68,plain,
! [X2] :
( ? [X3] :
( occurrence_of(X2,X3)
& activity(X3) )
| ~ activity_occurrence(X2) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f69,plain,
! [X2] :
( ( occurrence_of(X2,sK0_skl(X2))
& activity(sK0_skl(X2)) )
| ~ activity_occurrence(X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X3,sK0_skl(X2))],[f68]) ).
fof(f71,plain,
! [X0] :
( ~ activity_occurrence(X0)
| occurrence_of(X0,sK0_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f72,plain,
! [X4,X5,X6] :
( X5 = X6
| ~ occurrence_of(X4,X6)
| ~ occurrence_of(X4,X5) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f73,plain,
! [X5,X6] :
( X5 = X6
| ! [X4] :
( ~ occurrence_of(X4,X6)
| ~ occurrence_of(X4,X5) ) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f74,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f85,plain,
! [X16,X17] :
( ( arboreal(X16)
<=> atomic(X17) )
| ~ occurrence_of(X16,X17) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f86,plain,
! [X16,X17] :
( ( ( ~ atomic(X17)
| arboreal(X16) )
& ( atomic(X17)
| ~ arboreal(X16) ) )
| ~ occurrence_of(X16,X17) ),
inference(NNF_transformation,[status(thm)],[f85]) ).
fof(f88,plain,
! [X0,X1] :
( ~ atomic(X1)
| ~ occurrence_of(X0,X1)
| arboreal(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
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] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f161,plain,
! [X69,X70,X71] :
( ? [X72] :
( subactivity_occurrence(X71,X72)
& subactivity_occurrence(X70,X72)
& occurrence_of(X72,X69) )
| ~ min_precedes(X70,X71,X69) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f162,plain,
! [X69,X70,X71] :
( ( subactivity_occurrence(X71,sK9_skl(X71,X70,X69))
& subactivity_occurrence(X70,sK9_skl(X71,X70,X69))
& occurrence_of(sK9_skl(X71,X70,X69),X69) )
| ~ min_precedes(X70,X71,X69) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X72,sK9_skl(X71,X70,X69))],[f161]) ).
fof(f163,plain,
! [X0,X1,X2] :
( occurrence_of(sK9_skl(X1,X0,X2),X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f164,plain,
! [X0,X1,X2] :
( subactivity_occurrence(X0,sK9_skl(X1,X0,X2))
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f211,plain,
! [X113,X114,X115] :
( ! [X116] : ~ min_precedes(X114,X116,X115)
| ~ leaf_occ(X114,X113)
| ~ occurrence_of(X113,X115) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f212,plain,
! [X114,X115] :
( ! [X116] : ~ min_precedes(X114,X116,X115)
| ! [X113] :
( ~ leaf_occ(X114,X113)
| ~ occurrence_of(X113,X115) ) ),
inference(miniscoping,[status(thm)],[f211]) ).
fof(f213,plain,
! [X0,X1,X2,X3] :
( ~ leaf_occ(X2,X0)
| ~ min_precedes(X2,X3,X1)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f249,plain,
! [X161,X162] :
( ? [X163,X164,X165] :
( ! [X166] :
( X166 = X165
| X166 = X164
| ~ min_precedes(X163,X166,tptp0) )
& min_precedes(X164,X165,tptp0)
& ( occurrence_of(X165,tptp1)
| occurrence_of(X165,tptp2) )
& min_precedes(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] :
( ? [X163,X164,X165] :
( ! [X166] :
( X166 = X165
| X166 = X164
| ~ min_precedes(X163,X166,tptp0) )
& min_precedes(X164,X165,tptp0)
& ( occurrence_of(X165,tptp1)
| occurrence_of(X165,tptp2) )
& min_precedes(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] :
( ( ! [X166] :
( X166 = sK18_skl(X161)
| X166 = sK17_skl(X161)
| ~ min_precedes(sK16_skl(X161),X166,tptp0) )
& min_precedes(sK17_skl(X161),sK18_skl(X161),tptp0)
& ( occurrence_of(sK18_skl(X161),tptp1)
| occurrence_of(sK18_skl(X161),tptp2) )
& min_precedes(sK16_skl(X161),sK17_skl(X161),tptp0)
& occurrence_of(sK17_skl(X161),tptp4)
& next_subocc(X161,sK16_skl(X161),tptp0)
& occurrence_of(sK16_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(X163,sK16_skl(X161)),skolemize(X164,sK17_skl(X161)),skolemize(X165,sK18_skl(X161))],[f250]) ).
fof(f252,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK16_skl(X0),tptp3) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f253,plain,
! [X0,X1] :
( ~ arboreal(X0)
| leaf_occ(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(X0,sK16_skl(X0),tptp0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f254,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ subactivity_occurrence(X0,X1)
| occurrence_of(sK17_skl(X0),tptp4)
| ~ occurrence_of(X1,tptp0)
| ~ arboreal(X0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f255,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ subactivity_occurrence(X0,X1)
| min_precedes(sK16_skl(X0),sK17_skl(X0),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ arboreal(X0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f256,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| occurrence_of(sK18_skl(X0),tptp2)
| ~ occurrence_of(X1,tptp0)
| ~ arboreal(X0)
| occurrence_of(sK18_skl(X0),tptp1)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f258,plain,
! [X0,X1,X2] :
( sK17_skl(X0) = X2
| ~ min_precedes(sK16_skl(X0),X2,tptp0)
| leaf_occ(X0,X1)
| ~ subactivity_occurrence(X0,X1)
| X2 = sK18_skl(X0)
| ~ occurrence_of(X1,tptp0)
| ~ arboreal(X0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f264,plain,
atomic(tptp3),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f265,plain,
tptp4 != tptp3,
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f268,plain,
tptp3 != tptp2,
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f269,plain,
tptp3 != tptp1,
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f271,plain,
? [X167,X168] :
( ! [X169,X170] :
( ~ leaf(X170,tptp0)
| ~ min_precedes(X169,X170,tptp0)
| ( ~ occurrence_of(X170,tptp1)
& ~ occurrence_of(X170,tptp2) )
| ~ next_subocc(X167,X169,tptp0)
| ~ occurrence_of(X169,tptp3) )
& ~ leaf_occ(X167,X168)
& arboreal(X167)
& subactivity_occurrence(X167,X168)
& occurrence_of(X168,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f272,plain,
? [X167] :
( ! [X170] :
( ~ leaf(X170,tptp0)
| ! [X169] :
( ~ min_precedes(X169,X170,tptp0)
| ( ~ occurrence_of(X170,tptp1)
& ~ occurrence_of(X170,tptp2) )
| ~ next_subocc(X167,X169,tptp0)
| ~ occurrence_of(X169,tptp3) ) )
& ? [X168] :
( ~ leaf_occ(X167,X168)
& arboreal(X167)
& subactivity_occurrence(X167,X168)
& occurrence_of(X168,tptp0) ) ),
inference(miniscoping,[status(thm)],[f271]) ).
fof(f273,plain,
( ! [X170] :
( ~ leaf(X170,tptp0)
| ! [X169] :
( ~ min_precedes(X169,X170,tptp0)
| ( ~ occurrence_of(X170,tptp1)
& ~ occurrence_of(X170,tptp2) )
| ~ next_subocc(sK19_skl,X169,tptp0)
| ~ occurrence_of(X169,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(X167,sK19_skl),skolemize(X168,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(f320,plain,
( leaf_occ(sK19_skl,sK20_skl)
| ~ arboreal(sK19_skl)
| ~ occurrence_of(sK20_skl,tptp0)
| occurrence_of(sK16_skl(sK19_skl),tptp3) ),
inference(resolution,[status(thm)],[f252,f275]) ).
fof(f321,plain,
( ~ arboreal(sK19_skl)
| occurrence_of(sK16_skl(sK19_skl),tptp3)
| leaf_occ(sK19_skl,sK20_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f320,f274]) ).
fof(f337,plain,
( ~ arboreal(sK19_skl)
| occurrence_of(sK16_skl(sK19_skl),tptp3) ),
inference(forward_subsumption_resolution,[status(thm)],[f321,f277]) ).
fof(f338,plain,
occurrence_of(sK16_skl(sK19_skl),tptp3),
inference(resolution,[status(thm)],[f337,f276]) ).
fof(f347,plain,
( ~ atomic(tptp3)
| arboreal(sK16_skl(sK19_skl)) ),
inference(resolution,[status(thm)],[f338,f88]) ).
fof(f348,plain,
arboreal(sK16_skl(sK19_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f347,f264]) ).
fof(f410,plain,
! [X0] :
( sK17_skl(sK19_skl) = X0
| ~ min_precedes(sK16_skl(sK19_skl),X0,tptp0)
| leaf_occ(sK19_skl,sK20_skl)
| X0 = sK18_skl(sK19_skl)
| ~ occurrence_of(sK20_skl,tptp0)
| ~ arboreal(sK19_skl) ),
inference(resolution,[status(thm)],[f258,f275]) ).
fof(f411,plain,
! [X0] :
( X0 = sK17_skl(sK19_skl)
| leaf_occ(sK19_skl,sK20_skl)
| ~ min_precedes(sK16_skl(sK19_skl),X0,tptp0)
| X0 = sK18_skl(sK19_skl)
| ~ occurrence_of(sK20_skl,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f410,f276]) ).
fof(f468,plain,
( leaf_occ(sK19_skl,sK20_skl)
| min_precedes(sK16_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)
| ~ occurrence_of(sK20_skl,tptp0)
| ~ arboreal(sK19_skl) ),
inference(resolution,[status(thm)],[f255,f275]) ).
fof(f469,plain,
( leaf_occ(sK19_skl,sK20_skl)
| min_precedes(sK16_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)
| ~ occurrence_of(sK20_skl,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f468,f276]) ).
fof(f474,plain,
( leaf_occ(sK19_skl,sK20_skl)
| occurrence_of(sK18_skl(sK19_skl),tptp2)
| ~ occurrence_of(sK20_skl,tptp0)
| ~ arboreal(sK19_skl)
| occurrence_of(sK18_skl(sK19_skl),tptp1) ),
inference(resolution,[status(thm)],[f256,f275]) ).
fof(f475,plain,
( occurrence_of(sK18_skl(sK19_skl),tptp1)
| occurrence_of(sK18_skl(sK19_skl),tptp2)
| ~ occurrence_of(sK20_skl,tptp0)
| leaf_occ(sK19_skl,sK20_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f474,f276]) ).
fof(f833,plain,
! [X0] :
( sK18_skl(sK19_skl) = X0
| leaf_occ(sK19_skl,sK20_skl)
| sK17_skl(sK19_skl) = X0
| ~ min_precedes(sK16_skl(sK19_skl),X0,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f411,f274]) ).
fof(f850,plain,
( min_precedes(sK16_skl(sK19_skl),sK17_skl(sK19_skl),tptp0)
| leaf_occ(sK19_skl,sK20_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f469,f274]) ).
fof(f859,plain,
( occurrence_of(sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0),tptp0)
| leaf_occ(sK19_skl,sK20_skl) ),
inference(resolution,[status(thm)],[f850,f163]) ).
fof(f866,plain,
( subactivity_occurrence(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))
| leaf_occ(sK19_skl,sK20_skl) ),
inference(resolution,[status(thm)],[f850,f164]) ).
fof(f889,plain,
subactivity_occurrence(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)),
inference(forward_subsumption_resolution,[status(thm)],[f866,f277]) ).
fof(f890,plain,
occurrence_of(sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f859,f277]) ).
fof(f897,plain,
( occurrence_of(sK18_skl(sK19_skl),tptp1)
| ~ occurrence_of(sK20_skl,tptp0)
| occurrence_of(sK18_skl(sK19_skl),tptp2) ),
inference(forward_subsumption_resolution,[status(thm)],[f475,f277]) ).
fof(f898,plain,
( occurrence_of(sK18_skl(sK19_skl),tptp2)
| occurrence_of(sK18_skl(sK19_skl),tptp1) ),
inference(resolution,[status(thm)],[f897,f274]) ).
fof(f971,plain,
! [X0,X1] :
( ~ leaf_occ(X0,sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[status(thm)],[f890,f213]) ).
fof(f994,plain,
( activity_occurrence(sK18_skl(sK19_skl))
| occurrence_of(sK18_skl(sK19_skl),tptp2) ),
inference(resolution,[status(thm)],[f898,f67]) ).
fof(f1000,plain,
activity_occurrence(sK18_skl(sK19_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f994,f67]) ).
fof(f1001,plain,
occurrence_of(sK18_skl(sK19_skl),sK0_skl(sK18_skl(sK19_skl))),
inference(resolution,[status(thm)],[f1000,f71]) ).
fof(f1008,plain,
( leaf_occ(sK19_skl,sK20_skl)
| occurrence_of(sK17_skl(sK19_skl),tptp4)
| ~ occurrence_of(sK20_skl,tptp0)
| ~ arboreal(sK19_skl) ),
inference(resolution,[status(thm)],[f254,f275]) ).
fof(f1013,plain,
( occurrence_of(sK17_skl(sK19_skl),tptp4)
| leaf_occ(sK19_skl,sK20_skl)
| ~ occurrence_of(sK20_skl,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1008,f276]) ).
fof(f1037,plain,
! [X0] :
( X0 = sK0_skl(sK18_skl(sK19_skl))
| ~ occurrence_of(sK18_skl(sK19_skl),X0) ),
inference(resolution,[status(thm)],[f1001,f74]) ).
fof(f1063,plain,
( leaf_occ(sK19_skl,sK20_skl)
| occurrence_of(sK17_skl(sK19_skl),tptp4) ),
inference(forward_subsumption_resolution,[status(thm)],[f1013,f274]) ).
fof(f1071,plain,
! [X0] :
( tptp4 = X0
| ~ occurrence_of(sK17_skl(sK19_skl),X0)
| leaf_occ(sK19_skl,sK20_skl) ),
inference(resolution,[status(thm)],[f1063,f74]) ).
fof(f1078,plain,
! [X0] :
( tptp4 = X0
| ~ occurrence_of(sK17_skl(sK19_skl),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1071,f277]) ).
fof(f1259,plain,
( occurrence_of(sK18_skl(sK19_skl),tptp2)
| sK0_skl(sK18_skl(sK19_skl)) = tptp1 ),
inference(resolution,[status(thm)],[f1037,f898]) ).
fof(f1415,plain,
! [X0] :
( ~ occurrence_of(sK18_skl(sK19_skl),X0)
| sK0_skl(sK18_skl(sK19_skl)) = tptp1
| X0 = tptp2 ),
inference(resolution,[status(thm)],[f1259,f74]) ).
fof(f1535,plain,
( ~ arboreal(sK16_skl(sK19_skl))
| leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))
| ~ occurrence_of(sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0),tptp0)
| next_subocc(sK16_skl(sK19_skl),sK16_skl(sK16_skl(sK19_skl)),tptp0) ),
inference(resolution,[status(thm)],[f889,f253]) ).
fof(f1540,plain,
( leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))
| ~ arboreal(sK16_skl(sK19_skl))
| ~ occurrence_of(sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0),tptp0)
| occurrence_of(sK16_skl(sK16_skl(sK19_skl)),tptp3) ),
inference(resolution,[status(thm)],[f889,f252]) ).
fof(f1543,plain,
( ~ arboreal(sK16_skl(sK19_skl))
| leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))
| occurrence_of(sK16_skl(sK16_skl(sK19_skl)),tptp3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1540,f890]) ).
fof(f1551,plain,
( next_subocc(sK16_skl(sK19_skl),sK16_skl(sK16_skl(sK19_skl)),tptp0)
| leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))
| ~ arboreal(sK16_skl(sK19_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1535,f890]) ).
fof(f2858,plain,
( leaf_occ(sK19_skl,sK20_skl)
| ~ leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)) ),
inference(resolution,[status(thm)],[f971,f850]) ).
fof(f2864,plain,
~ leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0)),
inference(forward_subsumption_resolution,[status(thm)],[f2858,f277]) ).
fof(f5720,plain,
( ~ arboreal(sK16_skl(sK19_skl))
| occurrence_of(sK16_skl(sK16_skl(sK19_skl)),tptp3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1543,f2864]) ).
fof(f5721,plain,
occurrence_of(sK16_skl(sK16_skl(sK19_skl)),tptp3),
inference(resolution,[status(thm)],[f5720,f348]) ).
fof(f5740,plain,
! [X0] :
( X0 = tptp3
| ~ occurrence_of(sK16_skl(sK16_skl(sK19_skl)),X0) ),
inference(resolution,[status(thm)],[f5721,f74]) ).
fof(f5742,plain,
activity_occurrence(sK16_skl(sK16_skl(sK19_skl))),
inference(resolution,[status(thm)],[f5721,f67]) ).
fof(f5747,plain,
occurrence_of(sK16_skl(sK16_skl(sK19_skl)),sK0_skl(sK16_skl(sK16_skl(sK19_skl)))),
inference(resolution,[status(thm)],[f5742,f71]) ).
fof(f5956,plain,
tptp3 = sK0_skl(sK16_skl(sK16_skl(sK19_skl))),
inference(resolution,[status(thm)],[f5747,f5740]) ).
fof(f5985,plain,
( leaf_occ(sK16_skl(sK19_skl),sK9_skl(sK17_skl(sK19_skl),sK16_skl(sK19_skl),tptp0))
| next_subocc(sK16_skl(sK19_skl),sK16_skl(sK16_skl(sK19_skl)),tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1551,f348]) ).
fof(f5986,plain,
next_subocc(sK16_skl(sK19_skl),sK16_skl(sK16_skl(sK19_skl)),tptp0),
inference(resolution,[status(thm)],[f5985,f2864]) ).
fof(f6000,plain,
min_precedes(sK16_skl(sK19_skl),sK16_skl(sK16_skl(sK19_skl)),tptp0),
inference(resolution,[status(thm)],[f5986,f147]) ).
fof(f6004,plain,
( sK18_skl(sK19_skl) = sK16_skl(sK16_skl(sK19_skl))
| leaf_occ(sK19_skl,sK20_skl)
| sK17_skl(sK19_skl) = sK16_skl(sK16_skl(sK19_skl)) ),
inference(resolution,[status(thm)],[f6000,f833]) ).
fof(f6032,plain,
( sK17_skl(sK19_skl) = sK16_skl(sK16_skl(sK19_skl))
| sK18_skl(sK19_skl) = sK16_skl(sK16_skl(sK19_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6004,f277]) ).
fof(f8083,plain,
( sK16_skl(sK16_skl(sK19_skl)) = sK17_skl(sK19_skl)
| sK0_skl(sK18_skl(sK19_skl)) = tptp3 ),
inference(paramodulation,[status(thm)],[f6032,f5956]) ).
fof(f8089,plain,
( occurrence_of(sK18_skl(sK19_skl),tptp3)
| sK17_skl(sK19_skl) = sK16_skl(sK16_skl(sK19_skl)) ),
inference(paramodulation,[status(thm)],[f6032,f5721]) ).
fof(f8094,plain,
( sK0_skl(sK18_skl(sK19_skl)) = tptp1
| tptp3 = tptp2
| sK17_skl(sK19_skl) = sK16_skl(sK16_skl(sK19_skl)) ),
inference(resolution,[status(thm)],[f8089,f1415]) ).
fof(f8121,plain,
( sK16_skl(sK16_skl(sK19_skl)) = sK17_skl(sK19_skl)
| sK0_skl(sK18_skl(sK19_skl)) = tptp1 ),
inference(forward_subsumption_resolution,[status(thm)],[f8094,f268]) ).
fof(f8315,plain,
( sK16_skl(sK16_skl(sK19_skl)) = sK17_skl(sK19_skl)
| sK16_skl(sK16_skl(sK19_skl)) = sK17_skl(sK19_skl)
| tptp1 = tptp3 ),
inference(paramodulation,[status(thm)],[f8121,f8083]) ).
fof(f8336,plain,
( sK16_skl(sK16_skl(sK19_skl)) = sK17_skl(sK19_skl)
| tptp1 = tptp3 ),
inference(duplicate_literals_removal,[status(thm)],[f8315]) ).
fof(f8337,plain,
sK17_skl(sK19_skl) = sK16_skl(sK16_skl(sK19_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f8336,f269]) ).
fof(f8427,plain,
occurrence_of(sK17_skl(sK19_skl),tptp3),
inference(backward_demodulation,[status(thm)],[f8337,f5721]) ).
fof(f8445,plain,
tptp4 = tptp3,
inference(resolution,[status(thm)],[f8427,f1078]) ).
fof(f8470,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f8445,f265]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PRO017+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.43 % Computer : n019.cluster.edu
% 0.16/5.43 % Model : x86_64 x86_64
% 0.16/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.43 % Memory : 8046.5625MB
% 0.16/5.43 % OS : Linux 6.8.0-71-generic
% 0.16/5.43 % CPULimit : 300
% 0.16/5.43 % WCLimit : 300
% 0.16/5.43 % DateTime : Mon Sep 21 03:44:10 UTC 2026
% 0.16/5.43 % CPUTime :
% 0.16/5.45 % Drodi V4.1.1
% 124.01/21.68 % Refutation found
% 124.01/21.68 % SZS status Theorem for theBenchmark: Theorem is valid
% 124.01/21.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 72.62/21.78 % Elapsed time: 16.334155 seconds
% 72.62/21.78 % CPU time: 128.541960 seconds
% 72.62/21.78 % Total memory used: 486.513 MB
% 72.62/21.78 % Net memory used: 455.509 MB
%------------------------------------------------------------------------------