%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO016+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 : n001.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 39.54s 5.51s
% Output : CNFRefutation 36.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 15
% Syntax : Number of formulae : 128 ( 16 unt; 2 def)
% Number of atoms : 487 ( 11 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 548 ( 189 ~; 226 |; 113 &)
% ( 6 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-3 aty)
% Number of variables : 235 ( 203 !; 32 ?)
% Comments :
%------------------------------------------------------------------------------
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(f19,axiom,
! [X55,X56] :
( leaf_occ(X55,X56)
<=> ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X63,X64] :
( precedes(X63,X64)
<=> ( legal(X64)
& earlier(X63,X64) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X72,X73,X74] :
( min_precedes(X72,X73,X74)
=> precedes(X72,X73) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X75,X76,X77] :
( next_subocc(X75,X76,X77)
=> ( arboreal(X76)
& arboreal(X75) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [X78,X79,X80] :
( next_subocc(X78,X79,X80)
<=> ( ~ ? [X81] :
( min_precedes(X81,X79,X80)
& min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [X82,X83,X84,X85] :
( ( subactivity_occurrence(X83,X85)
& occurrence_of(X85,X84)
& min_precedes(X82,X83,X84) )
=> subactivity_occurrence(X82,X85) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X86,X87,X88,X89] :
( ( leaf_occ(X87,X88)
& leaf_occ(X86,X88)
& ~ atomic(X89)
& occurrence_of(X88,X89) )
=> X86 = X87 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [X94,X95,X96] :
( ( earlier(X95,X96)
& earlier(X94,X95) )
=> earlier(X94,X96) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [X97,X98,X99,X100] :
( ( precedes(X98,X99)
& min_precedes(X97,X99,X100)
& min_precedes(X97,X98,X100) )
=> min_precedes(X98,X99,X100) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X101,X102] :
( ( ~ leaf_occ(X101,X102)
& arboreal(X101)
& subactivity_occurrence(X101,X102)
& occurrence_of(X102,tptp0) )
=> ? [X103,X104,X105] :
( leaf_occ(X105,X102)
& next_subocc(X104,X105,tptp0)
& ( occurrence_of(X105,tptp2)
| occurrence_of(X105,tptp1) )
& next_subocc(X103,X104,tptp0)
& occurrence_of(X104,tptp4)
& next_subocc(X101,X103,tptp0)
& occurrence_of(X103,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,conjecture,
! [X106,X107] :
( ( ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) )
=> ? [X108,X109] :
( ( occurrence_of(X109,tptp2)
=> ~ ? [X111] :
( min_precedes(X108,X111,tptp0)
& occurrence_of(X111,tptp1) ) )
& ( occurrence_of(X109,tptp1)
=> ~ ? [X110] :
( min_precedes(X108,X110,tptp0)
& occurrence_of(X110,tptp2) ) )
& leaf_occ(X109,X107)
& min_precedes(X108,X109,tptp0)
& ( occurrence_of(X109,tptp2)
| occurrence_of(X109,tptp1) )
& next_subocc(X106,X108,tptp0)
& occurrence_of(X108,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
~ ! [X106,X107] :
( ( ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) )
=> ? [X108,X109] :
( ( occurrence_of(X109,tptp2)
=> ~ ? [X111] :
( min_precedes(X108,X111,tptp0)
& occurrence_of(X111,tptp1) ) )
& ( occurrence_of(X109,tptp1)
=> ~ ? [X110] :
( min_precedes(X108,X110,tptp0)
& occurrence_of(X110,tptp2) ) )
& leaf_occ(X109,X107)
& min_precedes(X108,X109,tptp0)
& ( occurrence_of(X109,tptp2)
| occurrence_of(X109,tptp1) )
& next_subocc(X106,X108,tptp0)
& occurrence_of(X108,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
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(f117,plain,
! [X55,X56] :
( ( ! [X57] :
( ~ leaf(X55,X57)
| ~ subactivity_occurrence(X55,X56)
| ~ occurrence_of(X56,X57) )
| leaf_occ(X55,X56) )
& ( ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) )
| ~ leaf_occ(X55,X56) ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f118,plain,
( ! [X55,X56] :
( ! [X57] :
( ~ leaf(X55,X57)
| ~ subactivity_occurrence(X55,X56)
| ~ occurrence_of(X56,X57) )
| leaf_occ(X55,X56) )
& ! [X55,X56] :
( ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) )
| ~ leaf_occ(X55,X56) ) ),
inference(miniscoping,[status(thm)],[f117]) ).
fof(f119,plain,
( ! [X55,X56] :
( ! [X57] :
( ~ leaf(X55,X57)
| ~ subactivity_occurrence(X55,X56)
| ~ occurrence_of(X56,X57) )
| leaf_occ(X55,X56) )
& ! [X55,X56] :
( ( leaf(X55,sK8_skl(X56,X55))
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,sK8_skl(X56,X55)) )
| ~ leaf_occ(X55,X56) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X57,sK8_skl(X56,X55))],[f118]) ).
fof(f121,plain,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f133,plain,
! [X63,X64] :
( ( ~ legal(X64)
| ~ earlier(X63,X64)
| precedes(X63,X64) )
& ( ( legal(X64)
& earlier(X63,X64) )
| ~ precedes(X63,X64) ) ),
inference(NNF_transformation,[status(thm)],[f22]) ).
fof(f134,plain,
( ! [X63,X64] :
( ~ legal(X64)
| ~ earlier(X63,X64)
| precedes(X63,X64) )
& ! [X63,X64] :
( ( legal(X64)
& earlier(X63,X64) )
| ~ precedes(X63,X64) ) ),
inference(miniscoping,[status(thm)],[f133]) ).
fof(f135,plain,
! [X0,X1] :
( earlier(X0,X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f136,plain,
! [X0,X1] :
( legal(X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f137,plain,
! [X0,X1] :
( ~ legal(X1)
| ~ earlier(X0,X1)
| precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f146,plain,
! [X72,X73,X74] :
( precedes(X72,X73)
| ~ min_precedes(X72,X73,X74) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f147,plain,
! [X72,X73] :
( precedes(X72,X73)
| ! [X74] : ~ min_precedes(X72,X73,X74) ),
inference(miniscoping,[status(thm)],[f146]) ).
fof(f148,plain,
! [X0,X1,X2] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f149,plain,
! [X75,X76,X77] :
( ( arboreal(X76)
& arboreal(X75) )
| ~ next_subocc(X75,X76,X77) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f150,plain,
! [X75,X76] :
( ( arboreal(X76)
& arboreal(X75) )
| ! [X77] : ~ next_subocc(X75,X76,X77) ),
inference(miniscoping,[status(thm)],[f149]) ).
fof(f152,plain,
! [X0,X1,X2] :
( arboreal(X1)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
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(f158,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)],[f156]) ).
fof(f161,plain,
! [X82,X83,X84,X85] :
( subactivity_occurrence(X82,X85)
| ~ subactivity_occurrence(X83,X85)
| ~ occurrence_of(X85,X84)
| ~ min_precedes(X82,X83,X84) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f162,plain,
! [X82,X85] :
( subactivity_occurrence(X82,X85)
| ! [X83] :
( ~ subactivity_occurrence(X83,X85)
| ! [X84] :
( ~ occurrence_of(X85,X84)
| ~ min_precedes(X82,X83,X84) ) ) ),
inference(miniscoping,[status(thm)],[f161]) ).
fof(f163,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ subactivity_occurrence(X1,X3)
| ~ occurrence_of(X3,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f164,plain,
! [X86,X87,X88,X89] :
( X86 = X87
| ~ leaf_occ(X87,X88)
| ~ leaf_occ(X86,X88)
| atomic(X89)
| ~ occurrence_of(X88,X89) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f165,plain,
! [X86,X87] :
( X86 = X87
| ! [X88] :
( ~ leaf_occ(X87,X88)
| ~ leaf_occ(X86,X88)
| ! [X89] :
( atomic(X89)
| ~ occurrence_of(X88,X89) ) ) ),
inference(miniscoping,[status(thm)],[f164]) ).
fof(f166,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ leaf_occ(X3,X0)
| ~ leaf_occ(X2,X0)
| atomic(X1)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f170,plain,
! [X94,X95,X96] :
( earlier(X94,X96)
| ~ earlier(X95,X96)
| ~ earlier(X94,X95) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f171,plain,
! [X94,X96] :
( earlier(X94,X96)
| ! [X95] :
( ~ earlier(X95,X96)
| ~ earlier(X94,X95) ) ),
inference(miniscoping,[status(thm)],[f170]) ).
fof(f172,plain,
! [X0,X1,X2] :
( earlier(X0,X2)
| ~ earlier(X1,X2)
| ~ earlier(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f173,plain,
! [X97,X98,X99,X100] :
( min_precedes(X98,X99,X100)
| ~ precedes(X98,X99)
| ~ min_precedes(X97,X99,X100)
| ~ min_precedes(X97,X98,X100) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f174,plain,
! [X98,X99,X100] :
( min_precedes(X98,X99,X100)
| ~ precedes(X98,X99)
| ! [X97] :
( ~ min_precedes(X97,X99,X100)
| ~ min_precedes(X97,X98,X100) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( min_precedes(X1,X3,X2)
| ~ precedes(X1,X3)
| ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f176,plain,
! [X101,X102] :
( ? [X103,X104,X105] :
( leaf_occ(X105,X102)
& next_subocc(X104,X105,tptp0)
& ( occurrence_of(X105,tptp2)
| occurrence_of(X105,tptp1) )
& next_subocc(X103,X104,tptp0)
& occurrence_of(X104,tptp4)
& next_subocc(X101,X103,tptp0)
& occurrence_of(X103,tptp3) )
| leaf_occ(X101,X102)
| ~ arboreal(X101)
| ~ subactivity_occurrence(X101,X102)
| ~ occurrence_of(X102,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f177,plain,
! [X101,X102] :
( ? [X105] :
( leaf_occ(X105,X102)
& ? [X104] :
( next_subocc(X104,X105,tptp0)
& ( occurrence_of(X105,tptp2)
| occurrence_of(X105,tptp1) )
& ? [X103] :
( next_subocc(X103,X104,tptp0)
& occurrence_of(X104,tptp4)
& next_subocc(X101,X103,tptp0)
& occurrence_of(X103,tptp3) ) ) )
| leaf_occ(X101,X102)
| ~ arboreal(X101)
| ~ subactivity_occurrence(X101,X102)
| ~ occurrence_of(X102,tptp0) ),
inference(miniscoping,[status(thm)],[f176]) ).
fof(f178,plain,
! [X101,X102] :
( ( leaf_occ(sK12_skl(X102,X101),X102)
& next_subocc(sK13_skl(X102,X101),sK12_skl(X102,X101),tptp0)
& ( occurrence_of(sK12_skl(X102,X101),tptp2)
| occurrence_of(sK12_skl(X102,X101),tptp1) )
& next_subocc(sK14_skl(X102,X101),sK13_skl(X102,X101),tptp0)
& occurrence_of(sK13_skl(X102,X101),tptp4)
& next_subocc(X101,sK14_skl(X102,X101),tptp0)
& occurrence_of(sK14_skl(X102,X101),tptp3) )
| leaf_occ(X101,X102)
| ~ arboreal(X101)
| ~ subactivity_occurrence(X101,X102)
| ~ occurrence_of(X102,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(X105,sK12_skl(X102,X101)),skolemize(X104,sK13_skl(X102,X101)),skolemize(X103,sK14_skl(X102,X101))],[f177]) ).
fof(f180,plain,
! [X0,X1] :
( next_subocc(X1,sK14_skl(X0,X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f182,plain,
! [X0,X1] :
( next_subocc(sK14_skl(X0,X1),sK13_skl(X0,X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f184,plain,
! [X0,X1] :
( next_subocc(sK13_skl(X0,X1),sK12_skl(X0,X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f185,plain,
! [X0,X1] :
( leaf_occ(sK12_skl(X0,X1),X0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f187,plain,
~ atomic(tptp0),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f198,plain,
? [X106,X107] :
( ! [X108,X109] :
( ( ? [X111] :
( min_precedes(X108,X111,tptp0)
& occurrence_of(X111,tptp1) )
& occurrence_of(X109,tptp2) )
| ( ? [X110] :
( min_precedes(X108,X110,tptp0)
& occurrence_of(X110,tptp2) )
& occurrence_of(X109,tptp1) )
| ~ leaf_occ(X109,X107)
| ~ min_precedes(X108,X109,tptp0)
| ( ~ occurrence_of(X109,tptp2)
& ~ occurrence_of(X109,tptp1) )
| ~ next_subocc(X106,X108,tptp0)
| ~ occurrence_of(X108,tptp3) )
& ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f199,definition,
! [X109] :
( sP0_prd(X109)
<=> ( ~ occurrence_of(X109,tptp2)
& ~ occurrence_of(X109,tptp1) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f200,definition,
! [X108,X109] :
( sP1_prd(X109,X108)
<=> ( ? [X110] :
( min_precedes(X108,X110,tptp0)
& occurrence_of(X110,tptp2) )
& occurrence_of(X109,tptp1) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f201,plain,
? [X106,X107] :
( ! [X108,X109] :
( ( ? [X111] :
( min_precedes(X108,X111,tptp0)
& occurrence_of(X111,tptp1) )
& occurrence_of(X109,tptp2) )
| sP1_prd(X109,X108)
| ~ leaf_occ(X109,X107)
| ~ min_precedes(X108,X109,tptp0)
| sP0_prd(X109)
| ~ next_subocc(X106,X108,tptp0)
| ~ occurrence_of(X108,tptp3) )
& ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) ),
inference(formula_renaming,[status(thm)],[f198,f200,f199]) ).
fof(f202,plain,
( ! [X108,X109] :
( ( min_precedes(X108,sK17_skl(X109,X108),tptp0)
& occurrence_of(sK17_skl(X109,X108),tptp1)
& occurrence_of(X109,tptp2) )
| sP1_prd(X109,X108)
| ~ leaf_occ(X109,sK16_skl)
| ~ min_precedes(X108,X109,tptp0)
| sP0_prd(X109)
| ~ next_subocc(sK15_skl,X108,tptp0)
| ~ occurrence_of(X108,tptp3) )
& ~ leaf_occ(sK15_skl,sK16_skl)
& arboreal(sK15_skl)
& subactivity_occurrence(sK15_skl,sK16_skl)
& occurrence_of(sK16_skl,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(X106,sK15_skl),skolemize(X107,sK16_skl),skolemize(X111,sK17_skl(X109,X108))],[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(f476,plain,
( next_subocc(sK14_skl(sK16_skl,sK15_skl),sK13_skl(sK16_skl,sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl)
| ~ occurrence_of(sK16_skl,tptp0) ),
inference(resolution,[status(thm)],[f182,f204]) ).
fof(f478,plain,
( next_subocc(sK14_skl(sK16_skl,sK15_skl),sK13_skl(sK16_skl,sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f476,f203]) ).
fof(f504,plain,
( next_subocc(sK14_skl(sK16_skl,sK15_skl),sK13_skl(sK16_skl,sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f478,f205]) ).
fof(f507,plain,
( arboreal(sK13_skl(sK16_skl,sK15_skl))
| leaf_occ(sK15_skl,sK16_skl) ),
inference(resolution,[status(thm)],[f504,f152]) ).
fof(f511,plain,
arboreal(sK13_skl(sK16_skl,sK15_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f507,f206]) ).
fof(f539,plain,
( next_subocc(sK13_skl(sK16_skl,sK15_skl),sK12_skl(sK16_skl,sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl)
| ~ occurrence_of(sK16_skl,tptp0) ),
inference(resolution,[status(thm)],[f184,f204]) ).
fof(f541,plain,
( next_subocc(sK13_skl(sK16_skl,sK15_skl),sK12_skl(sK16_skl,sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f539,f203]) ).
fof(f543,plain,
( leaf_occ(sK12_skl(sK16_skl,sK15_skl),sK16_skl)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl)
| ~ occurrence_of(sK16_skl,tptp0) ),
inference(resolution,[status(thm)],[f185,f204]) ).
fof(f545,plain,
( leaf_occ(sK12_skl(sK16_skl,sK15_skl),sK16_skl)
| leaf_occ(sK15_skl,sK16_skl)
| ~ arboreal(sK15_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f543,f203]) ).
fof(f546,plain,
( next_subocc(sK13_skl(sK16_skl,sK15_skl),sK12_skl(sK16_skl,sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f541,f205]) ).
fof(f547,plain,
! [X0] :
( ~ min_precedes(X0,sK12_skl(sK16_skl,sK15_skl),tptp0)
| ~ min_precedes(sK13_skl(sK16_skl,sK15_skl),X0,tptp0)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(resolution,[status(thm)],[f546,f158]) ).
fof(f548,plain,
( min_precedes(sK13_skl(sK16_skl,sK15_skl),sK12_skl(sK16_skl,sK15_skl),tptp0)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(resolution,[status(thm)],[f546,f157]) ).
fof(f551,plain,
! [X0] :
( ~ min_precedes(X0,sK12_skl(sK16_skl,sK15_skl),tptp0)
| ~ min_precedes(sK13_skl(sK16_skl,sK15_skl),X0,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f547,f206]) ).
fof(f552,plain,
min_precedes(sK13_skl(sK16_skl,sK15_skl),sK12_skl(sK16_skl,sK15_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f548,f206]) ).
fof(f555,plain,
( leaf_occ(sK12_skl(sK16_skl,sK15_skl),sK16_skl)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f545,f205]) ).
fof(f560,plain,
! [X0,X1] :
( X1 = sK12_skl(sK16_skl,sK15_skl)
| ~ leaf_occ(X1,sK16_skl)
| atomic(X0)
| ~ occurrence_of(sK16_skl,X0)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(resolution,[status(thm)],[f555,f166]) ).
fof(f565,plain,
( subactivity_occurrence(sK12_skl(sK16_skl,sK15_skl),sK16_skl)
| leaf_occ(sK15_skl,sK16_skl) ),
inference(resolution,[status(thm)],[f555,f121]) ).
fof(f570,plain,
! [X0,X1] :
( X1 = sK12_skl(sK16_skl,sK15_skl)
| ~ leaf_occ(X1,sK16_skl)
| atomic(X0)
| ~ occurrence_of(sK16_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f560,f206]) ).
fof(f574,plain,
subactivity_occurrence(sK12_skl(sK16_skl,sK15_skl),sK16_skl),
inference(forward_subsumption_resolution,[status(thm)],[f565,f206]) ).
fof(f913,plain,
! [X0] :
( min_precedes(X0,sK12_skl(sK16_skl,sK15_skl),tptp0)
| ~ precedes(X0,sK12_skl(sK16_skl,sK15_skl))
| ~ min_precedes(sK13_skl(sK16_skl,sK15_skl),X0,tptp0) ),
inference(resolution,[status(thm)],[f552,f175]) ).
fof(f919,plain,
precedes(sK13_skl(sK16_skl,sK15_skl),sK12_skl(sK16_skl,sK15_skl)),
inference(resolution,[status(thm)],[f552,f148]) ).
fof(f925,plain,
! [X0] :
( subactivity_occurrence(sK13_skl(sK16_skl,sK15_skl),X0)
| ~ subactivity_occurrence(sK12_skl(sK16_skl,sK15_skl),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f552,f163]) ).
fof(f927,plain,
! [X0] :
( ~ leaf_occ(sK13_skl(sK16_skl,sK15_skl),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f552,f82]) ).
fof(f953,plain,
legal(sK12_skl(sK16_skl,sK15_skl)),
inference(resolution,[status(thm)],[f919,f136]) ).
fof(f2111,plain,
! [X0] :
( ~ precedes(X0,sK12_skl(sK16_skl,sK15_skl))
| ~ min_precedes(sK13_skl(sK16_skl,sK15_skl),X0,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f913,f551]) ).
fof(f2222,plain,
( subactivity_occurrence(sK13_skl(sK16_skl,sK15_skl),sK16_skl)
| ~ occurrence_of(sK16_skl,tptp0) ),
inference(resolution,[status(thm)],[f925,f574]) ).
fof(f2224,plain,
subactivity_occurrence(sK13_skl(sK16_skl,sK15_skl),sK16_skl),
inference(forward_subsumption_resolution,[status(thm)],[f2222,f203]) ).
fof(f2232,plain,
( leaf_occ(sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK16_skl)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)
| ~ arboreal(sK13_skl(sK16_skl,sK15_skl))
| ~ occurrence_of(sK16_skl,tptp0) ),
inference(resolution,[status(thm)],[f2224,f185]) ).
fof(f2233,plain,
( next_subocc(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)
| ~ arboreal(sK13_skl(sK16_skl,sK15_skl))
| ~ occurrence_of(sK16_skl,tptp0) ),
inference(resolution,[status(thm)],[f2224,f184]) ).
fof(f2235,plain,
( next_subocc(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)
| ~ arboreal(sK13_skl(sK16_skl,sK15_skl))
| ~ occurrence_of(sK16_skl,tptp0) ),
inference(resolution,[status(thm)],[f2224,f182]) ).
fof(f2237,plain,
( next_subocc(sK13_skl(sK16_skl,sK15_skl),sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)
| ~ arboreal(sK13_skl(sK16_skl,sK15_skl))
| ~ occurrence_of(sK16_skl,tptp0) ),
inference(resolution,[status(thm)],[f2224,f180]) ).
fof(f2255,plain,
( leaf_occ(sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK16_skl)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)
| ~ arboreal(sK13_skl(sK16_skl,sK15_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2232,f203]) ).
fof(f2256,plain,
( next_subocc(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)
| ~ arboreal(sK13_skl(sK16_skl,sK15_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2233,f203]) ).
fof(f2258,plain,
( next_subocc(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)
| ~ arboreal(sK13_skl(sK16_skl,sK15_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2235,f203]) ).
fof(f2260,plain,
( next_subocc(sK13_skl(sK16_skl,sK15_skl),sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)
| ~ arboreal(sK13_skl(sK16_skl,sK15_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2237,f203]) ).
fof(f11512,plain,
( leaf_occ(sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK16_skl)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2255,f511]) ).
fof(f11524,plain,
! [X0] :
( sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)) = sK12_skl(sK16_skl,sK15_skl)
| atomic(X0)
| ~ occurrence_of(sK16_skl,X0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f11512,f570]) ).
fof(f13846,plain,
( sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)) = sK12_skl(sK16_skl,sK15_skl)
| atomic(tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f11524,f203]) ).
fof(f13849,plain,
( sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)) = sK12_skl(sK16_skl,sK15_skl)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f13846,f187]) ).
fof(f13850,plain,
( ~ occurrence_of(sK16_skl,tptp0)
| sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)) = sK12_skl(sK16_skl,sK15_skl) ),
inference(resolution,[status(thm)],[f13849,f927]) ).
fof(f13872,plain,
sK12_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)) = sK12_skl(sK16_skl,sK15_skl),
inference(forward_subsumption_resolution,[status(thm)],[f13850,f203]) ).
fof(f14771,plain,
( next_subocc(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl),tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)
| ~ arboreal(sK13_skl(sK16_skl,sK15_skl)) ),
inference(forward_demodulation,[status(thm)],[f13872,f2256]) ).
fof(f14772,plain,
( next_subocc(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl),tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f14771,f511]) ).
fof(f14774,plain,
( min_precedes(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl),tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f14772,f157]) ).
fof(f14786,plain,
( precedes(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl))
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f14774,f148]) ).
fof(f14801,plain,
( earlier(sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl))
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f14786,f135]) ).
fof(f14803,plain,
! [X0] :
( earlier(X0,sK12_skl(sK16_skl,sK15_skl))
| ~ earlier(X0,sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)))
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f14801,f172]) ).
fof(f14806,plain,
( next_subocc(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2258,f511]) ).
fof(f14808,plain,
( min_precedes(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f14806,f157]) ).
fof(f14811,plain,
( next_subocc(sK13_skl(sK16_skl,sK15_skl),sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2260,f511]) ).
fof(f14813,plain,
( min_precedes(sK13_skl(sK16_skl,sK15_skl),sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),tptp0)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f14811,f157]) ).
fof(f14820,plain,
( ~ precedes(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl))
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f14813,f2111]) ).
fof(f15491,plain,
( precedes(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)))
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f14808,f148]) ).
fof(f15557,plain,
( earlier(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK13_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)))
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f15491,f135]) ).
fof(f15579,plain,
( earlier(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl))
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl)
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f15557,f14803]) ).
fof(f15583,plain,
( earlier(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl))
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f15579]) ).
fof(f15585,plain,
( ~ legal(sK12_skl(sK16_skl,sK15_skl))
| precedes(sK14_skl(sK16_skl,sK13_skl(sK16_skl,sK15_skl)),sK12_skl(sK16_skl,sK15_skl))
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f15583,f137]) ).
fof(f15587,plain,
( ~ legal(sK12_skl(sK16_skl,sK15_skl))
| leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f15585,f14820]) ).
fof(f15588,plain,
leaf_occ(sK13_skl(sK16_skl,sK15_skl),sK16_skl),
inference(forward_subsumption_resolution,[status(thm)],[f15587,f953]) ).
fof(f15589,plain,
~ occurrence_of(sK16_skl,tptp0),
inference(resolution,[status(thm)],[f15588,f927]) ).
fof(f15611,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f15589,f203]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO016+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.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:48:29 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 39.54/5.51 % Refutation found
% 39.54/5.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 39.54/5.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 36.64/5.59 % Elapsed time: 5.215798 seconds
% 36.64/5.59 % CPU time: 40.825946 seconds
% 36.64/5.59 % Total memory used: 284.570 MB
% 36.64/5.59 % Net memory used: 263.082 MB
%------------------------------------------------------------------------------