%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO005+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:15 PM UTC 2026
% Result : Theorem 12.67s 7.24s
% Output : CNFRefutation 14.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 20
% Syntax : Number of formulae : 147 ( 43 unt; 0 def)
% Number of atoms : 419 ( 42 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 440 ( 168 ~; 178 |; 75 &)
% ( 6 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-3 aty)
% Number of variables : 243 ( 220 !; 23 ?)
% 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/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X12,X13] :
( occurrence_of(X13,X12)
=> ( activity_occurrence(X13)
& activity(X12) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X28,X29,X30] :
( ( occurrence_of(X28,X30)
& occurrence_of(X28,X29) )
=> X29 = X30 ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X39,X40] :
( subactivity_occurrence(X39,X40)
=> ( activity_occurrence(X40)
& activity_occurrence(X39) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X41] :
( activity_occurrence(X41)
=> ? [X42] :
( occurrence_of(X41,X42)
& activity(X42) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X43] :
( legal(X43)
=> arboreal(X43) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [X51,X52] :
( occurrence_of(X51,X52)
=> ( arboreal(X51)
<=> atomic(X52) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [X53,X54] :
( root(X53,X54)
=> legal(X53) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X58,X59] :
( root_occ(X58,X59)
<=> ? [X60] :
( root(X58,X60)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X60) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X90,X91,X92,X93] :
( ( root_occ(X91,X92)
& root_occ(X90,X92)
& occurrence_of(X92,X93) )
=> X90 = X91 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X101] :
( occurrence_of(X101,tptp0)
=> ? [X102,X103] :
( next_subocc(X102,X103,tptp0)
& leaf_occ(X103,X101)
& ( occurrence_of(X103,tptp2)
| occurrence_of(X103,tptp3) )
& root_occ(X102,X101)
& occurrence_of(X102,tptp4) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
atomic(tptp1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
tptp1 != tptp3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
tptp1 != tptp2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [X106,X107] :
( ( ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) )
=> ? [X108] :
( next_subocc(X106,X108,tptp0)
& occurrence_of(X108,tptp1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,conjecture,
~ ? [X109] : occurrence_of(X109,tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,negated_conjecture,
~ ~ ? [X109] : occurrence_of(X109,tptp0),
inference(negated_conjecture,[status(cth)],[f48]) ).
fof(f57,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(f58,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)],[f57]) ).
fof(f59,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)],[f58]) ).
fof(f60,plain,
! [X12,X13] :
( ( activity_occurrence(X13)
& activity(X12) )
| ~ occurrence_of(X13,X12) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f62,plain,
! [X0,X1] :
( activity_occurrence(X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f70,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(f71,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))],[f70]) ).
fof(f72,plain,
! [X0,X1,X2] :
( occurrence_of(sK2_skl(X1,X0,X2),X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
! [X0,X1,X2] :
( subactivity_occurrence(X0,sK2_skl(X1,X0,X2))
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f74,plain,
! [X0,X1,X2] :
( subactivity_occurrence(X1,sK2_skl(X1,X0,X2))
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f79,plain,
! [X28,X29,X30] :
( X29 = X30
| ~ occurrence_of(X28,X30)
| ~ occurrence_of(X28,X29) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f80,plain,
! [X29,X30] :
( X29 = X30
| ! [X28] :
( ~ occurrence_of(X28,X30)
| ~ occurrence_of(X28,X29) ) ),
inference(miniscoping,[status(thm)],[f79]) ).
fof(f81,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f82,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(f83,plain,
! [X32,X33] :
( ! [X34] : ~ min_precedes(X32,X34,X33)
| ! [X31] :
( ~ leaf_occ(X32,X31)
| ~ occurrence_of(X31,X33) ) ),
inference(miniscoping,[status(thm)],[f82]) ).
fof(f84,plain,
! [X0,X1,X2,X3] :
( ~ min_precedes(X2,X3,X1)
| ~ leaf_occ(X2,X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f88,plain,
! [X39,X40] :
( ( activity_occurrence(X40)
& activity_occurrence(X39) )
| ~ subactivity_occurrence(X39,X40) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f89,plain,
! [X0,X1] :
( activity_occurrence(X0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f91,plain,
! [X41] :
( ? [X42] :
( occurrence_of(X41,X42)
& activity(X42) )
| ~ activity_occurrence(X41) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f92,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))],[f91]) ).
fof(f94,plain,
! [X0] :
( occurrence_of(X0,sK4_skl(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f95,plain,
! [X43] :
( arboreal(X43)
| ~ legal(X43) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f96,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f112,plain,
! [X51,X52] :
( ( arboreal(X51)
<=> atomic(X52) )
| ~ occurrence_of(X51,X52) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f113,plain,
! [X51,X52] :
( ( ( ~ atomic(X52)
| arboreal(X51) )
& ( atomic(X52)
| ~ arboreal(X51) ) )
| ~ occurrence_of(X51,X52) ),
inference(NNF_transformation,[status(thm)],[f112]) ).
fof(f115,plain,
! [X0,X1] :
( ~ atomic(X1)
| arboreal(X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f116,plain,
! [X53,X54] :
( legal(X53)
| ~ root(X53,X54) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f117,plain,
! [X53] :
( legal(X53)
| ! [X54] : ~ root(X53,X54) ),
inference(miniscoping,[status(thm)],[f116]) ).
fof(f118,plain,
! [X0,X1] :
( legal(X0)
| ~ root(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f119,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(f120,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)],[f119]) ).
fof(f121,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))],[f120]) ).
fof(f123,plain,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f126,plain,
! [X58,X59] :
( ( ! [X60] :
( ~ root(X58,X60)
| ~ subactivity_occurrence(X58,X59)
| ~ occurrence_of(X59,X60) )
| root_occ(X58,X59) )
& ( ? [X60] :
( root(X58,X60)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X60) )
| ~ root_occ(X58,X59) ) ),
inference(NNF_transformation,[status(thm)],[f20]) ).
fof(f127,plain,
( ! [X58,X59] :
( ! [X60] :
( ~ root(X58,X60)
| ~ subactivity_occurrence(X58,X59)
| ~ occurrence_of(X59,X60) )
| root_occ(X58,X59) )
& ! [X58,X59] :
( ? [X60] :
( root(X58,X60)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X60) )
| ~ root_occ(X58,X59) ) ),
inference(miniscoping,[status(thm)],[f126]) ).
fof(f128,plain,
( ! [X58,X59] :
( ! [X60] :
( ~ root(X58,X60)
| ~ subactivity_occurrence(X58,X59)
| ~ occurrence_of(X59,X60) )
| root_occ(X58,X59) )
& ! [X58,X59] :
( ( root(X58,sK9_skl(X59,X58))
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,sK9_skl(X59,X58)) )
| ~ root_occ(X58,X59) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X60,sK9_skl(X59,X58))],[f127]) ).
fof(f129,plain,
! [X0,X1] :
( occurrence_of(X1,sK9_skl(X1,X0))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f131,plain,
! [X0,X1] :
( root(X0,sK9_skl(X1,X0))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f132,plain,
! [X0,X1,X2] :
( ~ root(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2)
| root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f155,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(f156,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)],[f155]) ).
fof(f157,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)],[f156]) ).
fof(f158,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))],[f157]) ).
fof(f159,plain,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f160,plain,
! [X0,X1,X2,X3] :
( ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X3,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f169,plain,
! [X90,X91,X92,X93] :
( X90 = X91
| ~ root_occ(X91,X92)
| ~ root_occ(X90,X92)
| ~ occurrence_of(X92,X93) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f170,plain,
! [X90,X91] :
( X90 = X91
| ! [X92] :
( ~ root_occ(X91,X92)
| ~ root_occ(X90,X92)
| ! [X93] : ~ occurrence_of(X92,X93) ) ),
inference(miniscoping,[status(thm)],[f169]) ).
fof(f171,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ root_occ(X3,X0)
| ~ root_occ(X2,X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f178,plain,
! [X101] :
( ? [X102,X103] :
( next_subocc(X102,X103,tptp0)
& leaf_occ(X103,X101)
& ( occurrence_of(X103,tptp2)
| occurrence_of(X103,tptp3) )
& root_occ(X102,X101)
& occurrence_of(X102,tptp4) )
| ~ occurrence_of(X101,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f179,plain,
! [X101] :
( ( next_subocc(sK12_skl(X101),sK13_skl(X101),tptp0)
& leaf_occ(sK13_skl(X101),X101)
& ( occurrence_of(sK13_skl(X101),tptp2)
| occurrence_of(sK13_skl(X101),tptp3) )
& root_occ(sK12_skl(X101),X101)
& occurrence_of(sK12_skl(X101),tptp4) )
| ~ occurrence_of(X101,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(X102,sK12_skl(X101)),skolemize(X103,sK13_skl(X101))],[f178]) ).
fof(f181,plain,
! [X0] :
( root_occ(sK12_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f182,plain,
! [X0] :
( occurrence_of(sK13_skl(X0),tptp2)
| occurrence_of(sK13_skl(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f183,plain,
! [X0] :
( leaf_occ(sK13_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f184,plain,
! [X0] :
( next_subocc(sK12_skl(X0),sK13_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f190,plain,
atomic(tptp1),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f194,plain,
tptp1 != tptp3,
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f195,plain,
tptp1 != tptp2,
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f199,plain,
! [X106,X107] :
( ? [X108] :
( next_subocc(X106,X108,tptp0)
& occurrence_of(X108,tptp1) )
| leaf_occ(X106,X107)
| ~ arboreal(X106)
| ~ subactivity_occurrence(X106,X107)
| ~ occurrence_of(X107,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f200,plain,
! [X106] :
( ? [X108] :
( next_subocc(X106,X108,tptp0)
& occurrence_of(X108,tptp1) )
| ! [X107] :
( leaf_occ(X106,X107)
| ~ arboreal(X106)
| ~ subactivity_occurrence(X106,X107)
| ~ occurrence_of(X107,tptp0) ) ),
inference(miniscoping,[status(thm)],[f199]) ).
fof(f201,plain,
! [X106] :
( ( next_subocc(X106,sK14_skl(X106),tptp0)
& occurrence_of(sK14_skl(X106),tptp1) )
| ! [X107] :
( leaf_occ(X106,X107)
| ~ arboreal(X106)
| ~ subactivity_occurrence(X106,X107)
| ~ occurrence_of(X107,tptp0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X108,sK14_skl(X106))],[f200]) ).
fof(f202,plain,
! [X0,X1] :
( 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)],[f201]) ).
fof(f203,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)],[f201]) ).
fof(f204,plain,
occurrence_of(sK15_skl,tptp0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X109,sK15_skl)],[f49]) ).
fof(f205,plain,
occurrence_of(sK15_skl,tptp0),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f206,plain,
! [X0] :
( tptp0 = X0
| ~ occurrence_of(sK15_skl,X0) ),
inference(resolution,[status(thm)],[f81,f205]) ).
fof(f299,plain,
root_occ(sK12_skl(sK15_skl),sK15_skl),
inference(resolution,[status(thm)],[f181,f205]) ).
fof(f300,plain,
root(sK12_skl(sK15_skl),sK9_skl(sK15_skl,sK12_skl(sK15_skl))),
inference(resolution,[status(thm)],[f299,f131]) ).
fof(f301,plain,
occurrence_of(sK15_skl,sK9_skl(sK15_skl,sK12_skl(sK15_skl))),
inference(resolution,[status(thm)],[f299,f129]) ).
fof(f302,plain,
subactivity_occurrence(sK12_skl(sK15_skl),sK15_skl),
inference(resolution,[status(thm)],[f299,f130]) ).
fof(f310,plain,
legal(sK12_skl(sK15_skl)),
inference(resolution,[status(thm)],[f300,f118]) ).
fof(f311,plain,
tptp0 = sK9_skl(sK15_skl,sK12_skl(sK15_skl)),
inference(resolution,[status(thm)],[f301,f206]) ).
fof(f325,plain,
arboreal(sK12_skl(sK15_skl)),
inference(resolution,[status(thm)],[f310,f96]) ).
fof(f327,plain,
root(sK12_skl(sK15_skl),tptp0),
inference(backward_demodulation,[status(thm)],[f311,f300]) ).
fof(f359,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| ~ leaf_occ(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f84,f205]) ).
fof(f511,plain,
next_subocc(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0),
inference(resolution,[status(thm)],[f184,f205]) ).
fof(f513,plain,
min_precedes(sK12_skl(sK15_skl),sK13_skl(sK15_skl),tptp0),
inference(resolution,[status(thm)],[f511,f159]) ).
fof(f519,plain,
~ leaf_occ(sK12_skl(sK15_skl),sK15_skl),
inference(resolution,[status(thm)],[f513,f359]) ).
fof(f874,plain,
! [X0] :
( occurrence_of(sK14_skl(X0),tptp1)
| leaf_occ(X0,sK15_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f202,f205]) ).
fof(f877,plain,
! [X0] :
( next_subocc(X0,sK14_skl(X0),tptp0)
| leaf_occ(X0,sK15_skl)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK15_skl) ),
inference(resolution,[status(thm)],[f203,f205]) ).
fof(f879,plain,
( occurrence_of(sK14_skl(sK12_skl(sK15_skl)),tptp1)
| leaf_occ(sK12_skl(sK15_skl),sK15_skl)
| ~ arboreal(sK12_skl(sK15_skl)) ),
inference(resolution,[status(thm)],[f874,f302]) ).
fof(f880,plain,
( occurrence_of(sK14_skl(sK12_skl(sK15_skl)),tptp1)
| leaf_occ(sK12_skl(sK15_skl),sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f879,f325]) ).
fof(f881,plain,
occurrence_of(sK14_skl(sK12_skl(sK15_skl)),tptp1),
inference(forward_subsumption_resolution,[status(thm)],[f880,f519]) ).
fof(f888,plain,
( ~ atomic(tptp1)
| arboreal(sK14_skl(sK12_skl(sK15_skl))) ),
inference(resolution,[status(thm)],[f881,f115]) ).
fof(f893,plain,
activity_occurrence(sK14_skl(sK12_skl(sK15_skl))),
inference(resolution,[status(thm)],[f881,f62]) ).
fof(f897,plain,
! [X0] :
( tptp1 = X0
| ~ occurrence_of(sK14_skl(sK12_skl(sK15_skl)),X0) ),
inference(resolution,[status(thm)],[f881,f81]) ).
fof(f898,plain,
arboreal(sK14_skl(sK12_skl(sK15_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f888,f190]) ).
fof(f899,plain,
occurrence_of(sK14_skl(sK12_skl(sK15_skl)),sK4_skl(sK14_skl(sK12_skl(sK15_skl)))),
inference(resolution,[status(thm)],[f893,f94]) ).
fof(f902,plain,
( next_subocc(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)
| leaf_occ(sK12_skl(sK15_skl),sK15_skl)
| ~ arboreal(sK12_skl(sK15_skl)) ),
inference(resolution,[status(thm)],[f877,f302]) ).
fof(f903,plain,
( next_subocc(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)
| leaf_occ(sK12_skl(sK15_skl),sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f902,f325]) ).
fof(f905,plain,
tptp1 = sK4_skl(sK14_skl(sK12_skl(sK15_skl))),
inference(resolution,[status(thm)],[f899,f897]) ).
fof(f1059,plain,
next_subocc(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f903,f519]) ).
fof(f1061,plain,
min_precedes(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0),
inference(resolution,[status(thm)],[f1059,f159]) ).
fof(f1076,plain,
subactivity_occurrence(sK14_skl(sK12_skl(sK15_skl)),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),
inference(resolution,[status(thm)],[f1061,f74]) ).
fof(f1077,plain,
subactivity_occurrence(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),
inference(resolution,[status(thm)],[f1061,f73]) ).
fof(f1078,plain,
occurrence_of(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0),tptp0),
inference(resolution,[status(thm)],[f1061,f72]) ).
fof(f1103,plain,
( occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp2)
| occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp3) ),
inference(resolution,[status(thm)],[f1078,f182]) ).
fof(f1104,plain,
next_subocc(sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0),
inference(resolution,[status(thm)],[f1078,f184]) ).
fof(f1106,plain,
leaf_occ(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),
inference(resolution,[status(thm)],[f1078,f183]) ).
fof(f1107,plain,
root_occ(sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),
inference(resolution,[status(thm)],[f1078,f181]) ).
fof(f1109,plain,
! [X0] :
( ~ root(X0,tptp0)
| ~ subactivity_occurrence(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))
| root_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)) ),
inference(resolution,[status(thm)],[f1078,f132]) ).
fof(f1111,plain,
! [X0,X1] :
( X0 = X1
| ~ root_occ(X1,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))
| ~ root_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)) ),
inference(resolution,[status(thm)],[f1078,f171]) ).
fof(f1117,plain,
! [X0,X1] :
( X1 = X0
| min_precedes(X0,X1,tptp0)
| ~ arboreal(X0)
| ~ leaf_occ(X1,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))
| ~ subactivity_occurrence(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)) ),
inference(resolution,[status(thm)],[f1078,f59]) ).
fof(f2855,plain,
subactivity_occurrence(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),
inference(resolution,[status(thm)],[f1106,f123]) ).
fof(f3246,plain,
activity_occurrence(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))),
inference(resolution,[status(thm)],[f2855,f89]) ).
fof(f3247,plain,
occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)))),
inference(resolution,[status(thm)],[f3246,f94]) ).
fof(f3540,plain,
! [X0] :
( sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)) = X0
| ~ root_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)) ),
inference(resolution,[status(thm)],[f1111,f1107]) ).
fof(f3698,plain,
! [X0] :
( sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))) = X0
| ~ occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),X0) ),
inference(resolution,[status(thm)],[f3247,f81]) ).
fof(f4130,plain,
( ~ root(sK12_skl(sK15_skl),tptp0)
| root_occ(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)) ),
inference(resolution,[status(thm)],[f1109,f1077]) ).
fof(f4133,plain,
root_occ(sK12_skl(sK15_skl),sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),
inference(forward_subsumption_resolution,[status(thm)],[f4130,f327]) ).
fof(f4134,plain,
sK12_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)) = sK12_skl(sK15_skl),
inference(resolution,[status(thm)],[f4133,f3540]) ).
fof(f4150,plain,
next_subocc(sK12_skl(sK15_skl),sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0),
inference(backward_demodulation,[status(thm)],[f4134,f1104]) ).
fof(f4196,plain,
! [X0] :
( ~ min_precedes(X0,sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0)
| ~ min_precedes(sK12_skl(sK15_skl),X0,tptp0) ),
inference(resolution,[status(thm)],[f4150,f160]) ).
fof(f4462,plain,
( sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))) = tptp3
| occurrence_of(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp2) ),
inference(resolution,[status(thm)],[f1103,f3698]) ).
fof(f5151,plain,
( sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))) = tptp2
| sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))) = tptp3 ),
inference(resolution,[status(thm)],[f4462,f3698]) ).
fof(f9355,plain,
! [X0] :
( X0 = sK14_skl(sK12_skl(sK15_skl))
| min_precedes(sK14_skl(sK12_skl(sK15_skl)),X0,tptp0)
| ~ arboreal(sK14_skl(sK12_skl(sK15_skl)))
| ~ leaf_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)) ),
inference(resolution,[status(thm)],[f1117,f1076]) ).
fof(f9358,plain,
! [X0] :
( X0 = sK14_skl(sK12_skl(sK15_skl))
| min_precedes(sK14_skl(sK12_skl(sK15_skl)),X0,tptp0)
| ~ leaf_occ(X0,sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9355,f898]) ).
fof(f9367,plain,
( sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)) = sK14_skl(sK12_skl(sK15_skl))
| min_precedes(sK14_skl(sK12_skl(sK15_skl)),sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)),tptp0) ),
inference(resolution,[status(thm)],[f9358,f1106]) ).
fof(f10322,plain,
( ~ min_precedes(sK12_skl(sK15_skl),sK14_skl(sK12_skl(sK15_skl)),tptp0)
| sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)) = sK14_skl(sK12_skl(sK15_skl)) ),
inference(resolution,[status(thm)],[f9367,f4196]) ).
fof(f10339,plain,
sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0)) = sK14_skl(sK12_skl(sK15_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f10322,f1061]) ).
fof(f10438,plain,
( sK4_skl(sK14_skl(sK12_skl(sK15_skl))) = tptp2
| sK4_skl(sK13_skl(sK2_skl(sK14_skl(sK12_skl(sK15_skl)),sK12_skl(sK15_skl),tptp0))) = tptp3 ),
inference(backward_demodulation,[status(thm)],[f10339,f5151]) ).
fof(f10567,plain,
( sK4_skl(sK14_skl(sK12_skl(sK15_skl))) = tptp2
| sK4_skl(sK14_skl(sK12_skl(sK15_skl))) = tptp3 ),
inference(forward_demodulation,[status(thm)],[f10339,f10438]) ).
fof(f10568,plain,
( sK4_skl(sK14_skl(sK12_skl(sK15_skl))) = tptp2
| tptp1 = tptp3 ),
inference(forward_demodulation,[status(thm)],[f905,f10567]) ).
fof(f10569,plain,
( tptp1 = tptp2
| tptp1 = tptp3 ),
inference(forward_demodulation,[status(thm)],[f905,f10568]) ).
fof(f10570,plain,
tptp1 = tptp2,
inference(forward_subsumption_resolution,[status(thm)],[f10569,f194]) ).
fof(f10604,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f10570,f195]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO005+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n007.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Mon Sep 21 03:39:40 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.39 % Drodi V4.1.1
% 12.67/7.24 % Refutation found
% 12.67/7.24 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.67/7.24 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 14.37/7.28 % Elapsed time: 1.882883 seconds
% 14.37/7.28 % CPU time: 14.727237 seconds
% 14.37/7.28 % Total memory used: 231.133 MB
% 14.37/7.28 % Net memory used: 219.218 MB
%------------------------------------------------------------------------------