%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO018+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 : n017.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:20 PM UTC 2026
% Result : Theorem 28.84s 4.14s
% Output : CNFRefutation 28.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 15
% Syntax : Number of formulae : 129 ( 35 unt; 2 def)
% Number of atoms : 455 ( 43 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 493 ( 167 ~; 203 |; 103 &)
% ( 6 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-3 aty)
% Number of variables : 187 ( 154 !; 33 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X12,X13] :
( occurrence_of(X13,X12)
=> ( activity_occurrence(X13)
& activity(X12) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X21,X22,X23] :
( min_precedes(X22,X23,X21)
=> ? [X24] :
( subactivity_occurrence(X23,X24)
& subactivity_occurrence(X22,X24)
& occurrence_of(X24,X21) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X28,X29,X30] :
( ( occurrence_of(X28,X30)
& occurrence_of(X28,X29) )
=> X29 = X30 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X31,X32,X33] :
( ( leaf_occ(X32,X31)
& occurrence_of(X31,X33) )
=> ~ ? [X34] : min_precedes(X32,X34,X33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X41] :
( activity_occurrence(X41)
=> ? [X42] :
( occurrence_of(X41,X42)
& activity(X42) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [X51,X52] :
( occurrence_of(X51,X52)
=> ( arboreal(X51)
<=> atomic(X52) ) ),
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(f33,axiom,
! [X101,X102] :
( ( ~ leaf_occ(X101,X102)
& arboreal(X101)
& subactivity_occurrence(X101,X102)
& occurrence_of(X102,tptp0) )
=> ? [X103,X104,X105] :
( ! [X106] :
( min_precedes(X103,X106,tptp0)
=> ( X106 = X105
| X106 = X104 ) )
& min_precedes(X104,X105,tptp0)
& ( occurrence_of(X105,tptp2)
| occurrence_of(X105,tptp1) )
& min_precedes(X103,X104,tptp0)
& occurrence_of(X104,tptp4)
& next_subocc(X101,X103,tptp0)
& occurrence_of(X103,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
atomic(tptp3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
tptp4 != tptp3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
tptp3 != tptp1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
tptp3 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,conjecture,
! [X107,X108] :
( ( ~ leaf_occ(X107,X108)
& arboreal(X107)
& subactivity_occurrence(X107,X108)
& occurrence_of(X108,tptp0) )
=> ? [X109,X110] :
( ( occurrence_of(X110,tptp2)
=> ~ ? [X112] :
( min_precedes(X109,X112,tptp0)
& occurrence_of(X112,tptp1) ) )
& ( occurrence_of(X110,tptp1)
=> ~ ? [X111] :
( min_precedes(X109,X111,tptp0)
& occurrence_of(X111,tptp2) ) )
& leaf_occ(X110,X108)
& min_precedes(X109,X110,tptp0)
& ( occurrence_of(X110,tptp2)
| occurrence_of(X110,tptp1) )
& next_subocc(X107,X109,tptp0)
& occurrence_of(X109,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
~ ! [X107,X108] :
( ( ~ leaf_occ(X107,X108)
& arboreal(X107)
& subactivity_occurrence(X107,X108)
& occurrence_of(X108,tptp0) )
=> ? [X109,X110] :
( ( occurrence_of(X110,tptp2)
=> ~ ? [X112] :
( min_precedes(X109,X112,tptp0)
& occurrence_of(X112,tptp1) ) )
& ( occurrence_of(X110,tptp1)
=> ~ ? [X111] :
( min_precedes(X109,X111,tptp0)
& occurrence_of(X111,tptp2) ) )
& leaf_occ(X110,X108)
& min_precedes(X109,X110,tptp0)
& ( occurrence_of(X110,tptp2)
| occurrence_of(X110,tptp1) )
& next_subocc(X107,X109,tptp0)
& occurrence_of(X109,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f58,plain,
! [X12,X13] :
( ( activity_occurrence(X13)
& activity(X12) )
| ~ occurrence_of(X13,X12) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f60,plain,
! [X0,X1] :
( activity_occurrence(X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f68,plain,
! [X21,X22,X23] :
( ? [X24] :
( subactivity_occurrence(X23,X24)
& subactivity_occurrence(X22,X24)
& occurrence_of(X24,X21) )
| ~ min_precedes(X22,X23,X21) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f69,plain,
! [X21,X22,X23] :
( ( subactivity_occurrence(X23,sK2_skl(X23,X22,X21))
& subactivity_occurrence(X22,sK2_skl(X23,X22,X21))
& occurrence_of(sK2_skl(X23,X22,X21),X21) )
| ~ min_precedes(X22,X23,X21) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X24,sK2_skl(X23,X22,X21))],[f68]) ).
fof(f70,plain,
! [X0,X1,X2] :
( occurrence_of(sK2_skl(X1,X0,X2),X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f72,plain,
! [X0,X1,X2] :
( subactivity_occurrence(X1,sK2_skl(X1,X0,X2))
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f77,plain,
! [X28,X29,X30] :
( X29 = X30
| ~ occurrence_of(X28,X30)
| ~ occurrence_of(X28,X29) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f78,plain,
! [X29,X30] :
( X29 = X30
| ! [X28] :
( ~ occurrence_of(X28,X30)
| ~ occurrence_of(X28,X29) ) ),
inference(miniscoping,[status(thm)],[f77]) ).
fof(f79,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f80,plain,
! [X31,X32,X33] :
( ! [X34] : ~ min_precedes(X32,X34,X33)
| ~ leaf_occ(X32,X31)
| ~ occurrence_of(X31,X33) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f81,plain,
! [X32,X33] :
( ! [X34] : ~ min_precedes(X32,X34,X33)
| ! [X31] :
( ~ leaf_occ(X32,X31)
| ~ occurrence_of(X31,X33) ) ),
inference(miniscoping,[status(thm)],[f80]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( ~ min_precedes(X2,X3,X1)
| ~ leaf_occ(X2,X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f89,plain,
! [X41] :
( ? [X42] :
( occurrence_of(X41,X42)
& activity(X42) )
| ~ activity_occurrence(X41) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f90,plain,
! [X41] :
( ( occurrence_of(X41,sK4_skl(X41))
& activity(sK4_skl(X41)) )
| ~ activity_occurrence(X41) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X42,sK4_skl(X41))],[f89]) ).
fof(f92,plain,
! [X0] :
( occurrence_of(X0,sK4_skl(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f110,plain,
! [X51,X52] :
( ( arboreal(X51)
<=> atomic(X52) )
| ~ occurrence_of(X51,X52) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f111,plain,
! [X51,X52] :
( ( ( ~ atomic(X52)
| arboreal(X51) )
& ( atomic(X52)
| ~ arboreal(X51) ) )
| ~ occurrence_of(X51,X52) ),
inference(NNF_transformation,[status(thm)],[f110]) ).
fof(f113,plain,
! [X0,X1] :
( ~ atomic(X1)
| arboreal(X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
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(f176,plain,
! [X101,X102] :
( ? [X103,X104,X105] :
( ! [X106] :
( X106 = X105
| X106 = X104
| ~ min_precedes(X103,X106,tptp0) )
& min_precedes(X104,X105,tptp0)
& ( occurrence_of(X105,tptp2)
| occurrence_of(X105,tptp1) )
& min_precedes(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] :
( ? [X103,X104,X105] :
( ! [X106] :
( X106 = X105
| X106 = X104
| ~ min_precedes(X103,X106,tptp0) )
& min_precedes(X104,X105,tptp0)
& ( occurrence_of(X105,tptp2)
| occurrence_of(X105,tptp1) )
& min_precedes(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] :
( ( ! [X106] :
( X106 = sK14_skl(X101)
| X106 = sK13_skl(X101)
| ~ min_precedes(sK12_skl(X101),X106,tptp0) )
& min_precedes(sK13_skl(X101),sK14_skl(X101),tptp0)
& ( occurrence_of(sK14_skl(X101),tptp2)
| occurrence_of(sK14_skl(X101),tptp1) )
& min_precedes(sK12_skl(X101),sK13_skl(X101),tptp0)
& occurrence_of(sK13_skl(X101),tptp4)
& next_subocc(X101,sK12_skl(X101),tptp0)
& occurrence_of(sK12_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(X103,sK12_skl(X101)),skolemize(X104,sK13_skl(X101)),skolemize(X105,sK14_skl(X101))],[f177]) ).
fof(f179,plain,
! [X0,X1] :
( occurrence_of(sK12_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,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(f181,plain,
! [X0,X1] :
( occurrence_of(sK13_skl(X1),tptp4)
| 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] :
( min_precedes(sK12_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(sK14_skl(X1),tptp2)
| occurrence_of(sK14_skl(X1),tptp1)
| 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,X2] :
( X2 = sK14_skl(X1)
| X2 = sK13_skl(X1)
| ~ min_precedes(sK12_skl(X1),X2,tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f191,plain,
atomic(tptp3),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f192,plain,
tptp4 != tptp3,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f195,plain,
tptp3 != tptp1,
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f196,plain,
tptp3 != tptp2,
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f198,plain,
? [X107,X108] :
( ! [X109,X110] :
( ( ? [X112] :
( min_precedes(X109,X112,tptp0)
& occurrence_of(X112,tptp1) )
& occurrence_of(X110,tptp2) )
| ( ? [X111] :
( min_precedes(X109,X111,tptp0)
& occurrence_of(X111,tptp2) )
& occurrence_of(X110,tptp1) )
| ~ leaf_occ(X110,X108)
| ~ min_precedes(X109,X110,tptp0)
| ( ~ occurrence_of(X110,tptp2)
& ~ occurrence_of(X110,tptp1) )
| ~ next_subocc(X107,X109,tptp0)
| ~ occurrence_of(X109,tptp3) )
& ~ leaf_occ(X107,X108)
& arboreal(X107)
& subactivity_occurrence(X107,X108)
& occurrence_of(X108,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f199,definition,
! [X110] :
( sP0_prd(X110)
<=> ( ~ occurrence_of(X110,tptp2)
& ~ occurrence_of(X110,tptp1) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f200,definition,
! [X109,X110] :
( sP1_prd(X110,X109)
<=> ( ? [X111] :
( min_precedes(X109,X111,tptp0)
& occurrence_of(X111,tptp2) )
& occurrence_of(X110,tptp1) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f201,plain,
? [X107,X108] :
( ! [X109,X110] :
( ( ? [X112] :
( min_precedes(X109,X112,tptp0)
& occurrence_of(X112,tptp1) )
& occurrence_of(X110,tptp2) )
| sP1_prd(X110,X109)
| ~ leaf_occ(X110,X108)
| ~ min_precedes(X109,X110,tptp0)
| sP0_prd(X110)
| ~ next_subocc(X107,X109,tptp0)
| ~ occurrence_of(X109,tptp3) )
& ~ leaf_occ(X107,X108)
& arboreal(X107)
& subactivity_occurrence(X107,X108)
& occurrence_of(X108,tptp0) ),
inference(formula_renaming,[status(thm)],[f198,f200,f199]) ).
fof(f202,plain,
( ! [X109,X110] :
( ( min_precedes(X109,sK17_skl(X110,X109),tptp0)
& occurrence_of(sK17_skl(X110,X109),tptp1)
& occurrence_of(X110,tptp2) )
| sP1_prd(X110,X109)
| ~ leaf_occ(X110,sK16_skl)
| ~ min_precedes(X109,X110,tptp0)
| sP0_prd(X110)
| ~ next_subocc(sK15_skl,X109,tptp0)
| ~ occurrence_of(X109,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,sK17_skl]),skolemize(X107,sK15_skl),skolemize(X108,sK16_skl),skolemize(X112,sK17_skl(X110,X109))],[f201]) ).
fof(f203,plain,
occurrence_of(sK16_skl,tptp0),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f204,plain,
subactivity_occurrence(sK15_skl,sK16_skl),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f205,plain,
arboreal(sK15_skl),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f206,plain,
~ leaf_occ(sK15_skl,sK16_skl),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f210,plain,
! [X110] :
( ( occurrence_of(X110,tptp2)
| occurrence_of(X110,tptp1)
| sP0_prd(X110) )
& ( ( ~ occurrence_of(X110,tptp2)
& ~ occurrence_of(X110,tptp1) )
| ~ sP0_prd(X110) ) ),
inference(NNF_transformation,[status(thm)],[f199]) ).
fof(f211,plain,
( ! [X110] :
( occurrence_of(X110,tptp2)
| occurrence_of(X110,tptp1)
| sP0_prd(X110) )
& ! [X110] :
( ( ~ occurrence_of(X110,tptp2)
& ~ occurrence_of(X110,tptp1) )
| ~ sP0_prd(X110) ) ),
inference(miniscoping,[status(thm)],[f210]) ).
fof(f212,plain,
! [X0] :
( ~ occurrence_of(X0,tptp1)
| ~ sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f213,plain,
! [X0] :
( ~ occurrence_of(X0,tptp2)
| ~ sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f214,plain,
! [X0] :
( occurrence_of(X0,tptp2)
| occurrence_of(X0,tptp1)
| sP0_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f233,plain,
! [X0,X1] :
( X1 = tptp2
| ~ occurrence_of(X0,X1)
| occurrence_of(X0,tptp1)
| sP0_prd(X0) ),
inference(resolution,[status(thm)],[f214,f79]) ).
fof(f307,plain,
! [X0] :
( arboreal(X0)
| ~ occurrence_of(X0,tptp3) ),
inference(resolution,[status(thm)],[f113,f191]) ).
fof(f458,plain,
! [X0] :
( occurrence_of(sK12_skl(X0),tptp3)
| leaf_occ(X0,sK16_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f179,f203]) ).
fof(f459,plain,
! [X0] :
( next_subocc(X0,sK12_skl(X0),tptp0)
| leaf_occ(X0,sK16_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f180,f203]) ).
fof(f460,plain,
! [X0] :
( occurrence_of(sK13_skl(X0),tptp4)
| leaf_occ(X0,sK16_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f181,f203]) ).
fof(f462,plain,
( occurrence_of(sK12_skl(sK15_skl),tptp3)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl) ),
inference(resolution,[status(thm)],[f458,f204]) ).
fof(f464,plain,
( occurrence_of(sK12_skl(sK15_skl),tptp3)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f462,f205]) ).
fof(f465,plain,
occurrence_of(sK12_skl(sK15_skl),tptp3),
inference(forward_subsumption_resolution,[status(thm)],[f464,f206]) ).
fof(f466,plain,
arboreal(sK12_skl(sK15_skl)),
inference(resolution,[status(thm)],[f465,f307]) ).
fof(f476,plain,
( next_subocc(sK15_skl,sK12_skl(sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl) ),
inference(resolution,[status(thm)],[f459,f204]) ).
fof(f478,plain,
( next_subocc(sK15_skl,sK12_skl(sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f476,f205]) ).
fof(f502,plain,
( occurrence_of(sK13_skl(sK15_skl),tptp4)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl) ),
inference(resolution,[status(thm)],[f460,f204]) ).
fof(f504,plain,
( occurrence_of(sK13_skl(sK15_skl),tptp4)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f502,f205]) ).
fof(f534,plain,
! [X0] :
( min_precedes(sK12_skl(X0),sK13_skl(X0),tptp0)
| leaf_occ(X0,sK16_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f182,f203]) ).
fof(f535,plain,
! [X0] :
( occurrence_of(sK14_skl(X0),tptp2)
| occurrence_of(sK14_skl(X0),tptp1)
| leaf_occ(X0,sK16_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f183,f203]) ).
fof(f539,plain,
( min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl) ),
inference(resolution,[status(thm)],[f534,f204]) ).
fof(f541,plain,
( min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f539,f205]) ).
fof(f542,plain,
occurrence_of(sK13_skl(sK15_skl),tptp4),
inference(forward_subsumption_resolution,[status(thm)],[f504,f206]) ).
fof(f547,plain,
! [X0] :
( X0 = tptp4
| ~ occurrence_of(sK13_skl(sK15_skl),X0) ),
inference(resolution,[status(thm)],[f542,f79]) ).
fof(f548,plain,
activity_occurrence(sK13_skl(sK15_skl)),
inference(resolution,[status(thm)],[f542,f60]) ).
fof(f556,plain,
occurrence_of(sK13_skl(sK15_skl),sK4_skl(sK13_skl(sK15_skl))),
inference(resolution,[status(thm)],[f548,f92]) ).
fof(f564,plain,
( occurrence_of(sK14_skl(sK15_skl),tptp2)
| occurrence_of(sK14_skl(sK15_skl),tptp1)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl) ),
inference(resolution,[status(thm)],[f535,f204]) ).
fof(f566,plain,
( occurrence_of(sK14_skl(sK15_skl),tptp2)
| occurrence_of(sK14_skl(sK15_skl),tptp1)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f564,f205]) ).
fof(f575,plain,
sK4_skl(sK13_skl(sK15_skl)) = tptp4,
inference(resolution,[status(thm)],[f556,f547]) ).
fof(f623,plain,
next_subocc(sK15_skl,sK12_skl(sK15_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f478,f206]) ).
fof(f628,plain,
min_precedes(sK15_skl,sK12_skl(sK15_skl),tptp0),
inference(resolution,[status(thm)],[f623,f157]) ).
fof(f640,plain,
subactivity_occurrence(sK12_skl(sK15_skl),sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0)),
inference(resolution,[status(thm)],[f628,f72]) ).
fof(f645,plain,
occurrence_of(sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0),tptp0),
inference(resolution,[status(thm)],[f628,f70]) ).
fof(f701,plain,
! [X0] :
( next_subocc(X0,sK12_skl(X0),tptp0)
| leaf_occ(X0,sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0))
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0)) ),
inference(resolution,[status(thm)],[f645,f180]) ).
fof(f702,plain,
! [X0] :
( occurrence_of(sK12_skl(X0),tptp3)
| leaf_occ(X0,sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0))
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0)) ),
inference(resolution,[status(thm)],[f645,f179]) ).
fof(f715,plain,
min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f541,f206]) ).
fof(f745,plain,
( occurrence_of(sK14_skl(sK15_skl),tptp2)
| occurrence_of(sK14_skl(sK15_skl),tptp1) ),
inference(forward_subsumption_resolution,[status(thm)],[f566,f206]) ).
fof(f6063,plain,
( next_subocc(sK12_skl(sK15_skl),sK12_skl(sK12_skl(sK15_skl)),tptp0)
| leaf_occ(sK12_skl(sK15_skl),sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0))
| ~ arboreal(sK12_skl(sK15_skl)) ),
inference(resolution,[status(thm)],[f701,f640]) ).
fof(f6069,plain,
( next_subocc(sK12_skl(sK15_skl),sK12_skl(sK12_skl(sK15_skl)),tptp0)
| leaf_occ(sK12_skl(sK15_skl),sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6063,f466]) ).
fof(f6077,plain,
! [X0,X1] :
( ~ min_precedes(sK12_skl(sK15_skl),X1,X0)
| ~ occurrence_of(sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0),X0)
| next_subocc(sK12_skl(sK15_skl),sK12_skl(sK12_skl(sK15_skl)),tptp0) ),
inference(resolution,[status(thm)],[f6069,f82]) ).
fof(f6109,plain,
( occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp3)
| leaf_occ(sK12_skl(sK15_skl),sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0))
| ~ arboreal(sK12_skl(sK15_skl)) ),
inference(resolution,[status(thm)],[f702,f640]) ).
fof(f6115,plain,
( occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp3)
| leaf_occ(sK12_skl(sK15_skl),sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6109,f466]) ).
fof(f6215,plain,
! [X0,X1] :
( ~ min_precedes(sK12_skl(sK15_skl),X1,X0)
| ~ occurrence_of(sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0),X0)
| occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp3) ),
inference(resolution,[status(thm)],[f6115,f82]) ).
fof(f6221,plain,
! [X0] :
( ~ min_precedes(sK12_skl(sK15_skl),X0,tptp0)
| occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp3) ),
inference(resolution,[status(thm)],[f6215,f645]) ).
fof(f6227,plain,
occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp3),
inference(resolution,[status(thm)],[f6221,f715]) ).
fof(f6234,plain,
( tptp3 = tptp2
| occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp1)
| sP0_prd(sK12_skl(sK12_skl(sK15_skl))) ),
inference(resolution,[status(thm)],[f6227,f233]) ).
fof(f6236,plain,
! [X0] :
( X0 = tptp3
| ~ occurrence_of(sK12_skl(sK12_skl(sK15_skl)),X0) ),
inference(resolution,[status(thm)],[f6227,f79]) ).
fof(f6237,plain,
activity_occurrence(sK12_skl(sK12_skl(sK15_skl))),
inference(resolution,[status(thm)],[f6227,f60]) ).
fof(f6239,plain,
( occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp1)
| sP0_prd(sK12_skl(sK12_skl(sK15_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f6234,f196]) ).
fof(f6246,plain,
occurrence_of(sK12_skl(sK12_skl(sK15_skl)),sK4_skl(sK12_skl(sK12_skl(sK15_skl)))),
inference(resolution,[status(thm)],[f6237,f92]) ).
fof(f6290,plain,
sK4_skl(sK12_skl(sK12_skl(sK15_skl))) = tptp3,
inference(resolution,[status(thm)],[f6246,f6236]) ).
fof(f6350,plain,
( tptp1 = tptp3
| sP0_prd(sK12_skl(sK12_skl(sK15_skl))) ),
inference(resolution,[status(thm)],[f6239,f6236]) ).
fof(f6369,plain,
sP0_prd(sK12_skl(sK12_skl(sK15_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f6350,f195]) ).
fof(f6371,plain,
~ occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp2),
inference(resolution,[status(thm)],[f6369,f213]) ).
fof(f6372,plain,
~ occurrence_of(sK12_skl(sK12_skl(sK15_skl)),tptp1),
inference(resolution,[status(thm)],[f6369,f212]) ).
fof(f11998,plain,
! [X0,X1] :
( min_precedes(sK12_skl(sK15_skl),sK12_skl(sK12_skl(sK15_skl)),tptp0)
| ~ min_precedes(sK12_skl(sK15_skl),X1,X0)
| ~ occurrence_of(sK2_skl(sK12_skl(sK15_skl),sK15_skl,tptp0),X0) ),
inference(resolution,[status(thm)],[f6077,f157]) ).
fof(f12889,plain,
! [X0] :
( min_precedes(sK12_skl(sK15_skl),sK12_skl(sK12_skl(sK15_skl)),tptp0)
| ~ min_precedes(sK12_skl(sK15_skl),X0,tptp0) ),
inference(resolution,[status(thm)],[f11998,f645]) ).
fof(f12897,plain,
min_precedes(sK12_skl(sK15_skl),sK12_skl(sK12_skl(sK15_skl)),tptp0),
inference(resolution,[status(thm)],[f12889,f715]) ).
fof(f12900,plain,
! [X0] :
( sK12_skl(sK12_skl(sK15_skl)) = sK14_skl(sK15_skl)
| sK12_skl(sK12_skl(sK15_skl)) = sK13_skl(sK15_skl)
| leaf_occ(sK15_skl,X0)
| ~ arboreal(sK15_skl)
| ~ subactivity_occurrence(sK15_skl,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f12897,f185]) ).
fof(f12913,plain,
! [X0] :
( sK12_skl(sK12_skl(sK15_skl)) = sK14_skl(sK15_skl)
| sK12_skl(sK12_skl(sK15_skl)) = sK13_skl(sK15_skl)
| leaf_occ(sK15_skl,X0)
| ~ subactivity_occurrence(sK15_skl,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f12900,f205]) ).
fof(f13806,plain,
( sK12_skl(sK12_skl(sK15_skl)) = sK14_skl(sK15_skl)
| sK12_skl(sK12_skl(sK15_skl)) = sK13_skl(sK15_skl)
| ~ subactivity_occurrence(sK15_skl,sK16_skl)
| ~ occurrence_of(sK16_skl,tptp0) ),
inference(resolution,[status(thm)],[f12913,f206]) ).
fof(f13822,plain,
( sK12_skl(sK12_skl(sK15_skl)) = sK14_skl(sK15_skl)
| sK12_skl(sK12_skl(sK15_skl)) = sK13_skl(sK15_skl)
| ~ subactivity_occurrence(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f13806,f203]) ).
fof(f13829,plain,
( sK12_skl(sK12_skl(sK15_skl)) = sK14_skl(sK15_skl)
| sK12_skl(sK12_skl(sK15_skl)) = sK13_skl(sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f13822,f204]) ).
fof(f13949,plain,
( sK12_skl(sK12_skl(sK15_skl)) = sK13_skl(sK15_skl)
| ~ occurrence_of(sK14_skl(sK15_skl),tptp1) ),
inference(paramodulation,[status(thm)],[f13829,f6372]) ).
fof(f13950,plain,
( sK12_skl(sK12_skl(sK15_skl)) = sK13_skl(sK15_skl)
| ~ occurrence_of(sK14_skl(sK15_skl),tptp2) ),
inference(paramodulation,[status(thm)],[f13829,f6371]) ).
fof(f13985,plain,
( occurrence_of(sK14_skl(sK15_skl),tptp1)
| sK12_skl(sK12_skl(sK15_skl)) = sK13_skl(sK15_skl) ),
inference(resolution,[status(thm)],[f13950,f745]) ).
fof(f13987,plain,
sK12_skl(sK12_skl(sK15_skl)) = sK13_skl(sK15_skl),
inference(forward_subsumption_resolution,[status(thm)],[f13985,f13949]) ).
fof(f14102,plain,
sK4_skl(sK13_skl(sK15_skl)) = tptp3,
inference(backward_demodulation,[status(thm)],[f13987,f6290]) ).
fof(f14179,plain,
tptp4 = tptp3,
inference(forward_demodulation,[status(thm)],[f575,f14102]) ).
fof(f14180,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f14179,f192]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO018+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 03:39:12 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 28.84/4.14 % Refutation found
% 28.84/4.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 28.84/4.14 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 28.84/4.20 % Elapsed time: 3.816641 seconds
% 28.84/4.20 % CPU time: 29.447803 seconds
% 28.84/4.20 % Total memory used: 225.628 MB
% 28.84/4.20 % Net memory used: 208.281 MB
%------------------------------------------------------------------------------