%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO012+1 : 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:17 PM UTC 2026
% Result : Theorem 102.97s 13.61s
% Output : CNFRefutation 95.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 14
% Syntax : Number of formulae : 143 ( 27 unt; 0 def)
% Number of atoms : 436 ( 45 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 473 ( 180 ~; 200 |; 77 &)
% ( 3 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 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; 6 con; 0-3 aty)
% Number of variables : 247 ( 221 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X4,X5,X6] :
( ( occurrence_of(X4,X6)
& occurrence_of(X4,X5) )
=> X5 = X6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X10,X11,X12] :
( ( earlier(X11,X12)
& earlier(X10,X11) )
=> earlier(X10,X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X13,X14,X15] :
( ( earlier(X15,X14)
& earlier(X13,X14) )
=> ( X13 = X15
| earlier(X13,X15)
| earlier(X15,X13) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X19,X20] :
( ( earlier(X20,X19)
& legal(X19) )
=> legal(X20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X21,X22] :
( precedes(X21,X22)
<=> ( legal(X22)
& earlier(X21,X22) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X23,X24,X25] :
( min_precedes(X24,X25,X23)
=> ? [X26,X27] :
( atocc(X25,X27)
& atocc(X24,X26)
& subactivity(X27,X23)
& subactivity(X26,X23) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X31,X32,X33] :
( min_precedes(X31,X32,X33)
=> ? [X34] :
( min_precedes(X34,X32,X33)
& root(X34,X33) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X35,X36,X37] :
( min_precedes(X35,X36,X37)
=> ~ root(X36,X37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X38,X39,X40] :
( min_precedes(X38,X39,X40)
=> precedes(X38,X39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X52,X53,X54,X55] :
( ( precedes(X53,X54)
& min_precedes(X54,X52,X55)
& min_precedes(X53,X52,X55) )
=> min_precedes(X53,X54,X55) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [X64,X65] :
( atocc(X64,X65)
<=> ? [X66] :
( occurrence_of(X64,X66)
& atomic(X66)
& subactivity(X65,X66) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [X99,X100] :
( root_occ(X99,X100)
<=> ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X105] :
( occurrence_of(X105,tptp0)
=> ? [X106,X107,X108] :
( ! [X109] :
( min_precedes(X106,X109,tptp0)
=> ( X109 = X108
| X109 = X107 ) )
& min_precedes(X107,X108,tptp0)
& ( occurrence_of(X108,tptp1)
| occurrence_of(X108,tptp2) )
& min_precedes(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,conjecture,
! [X110] :
( occurrence_of(X110,tptp0)
=> ? [X111,X112] :
( min_precedes(X111,X112,tptp0)
& ( occurrence_of(X112,tptp1)
| occurrence_of(X112,tptp2) )
& root_occ(X111,X110)
& occurrence_of(X111,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,negated_conjecture,
~ ! [X110] :
( occurrence_of(X110,tptp0)
=> ? [X111,X112] :
( min_precedes(X111,X112,tptp0)
& ( occurrence_of(X112,tptp1)
| occurrence_of(X112,tptp2) )
& root_occ(X111,X110)
& occurrence_of(X111,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f49]) ).
fof(f58,plain,
! [X4,X5,X6] :
( X5 = X6
| ~ occurrence_of(X4,X6)
| ~ occurrence_of(X4,X5) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f59,plain,
! [X5,X6] :
( X5 = X6
| ! [X4] :
( ~ occurrence_of(X4,X6)
| ~ occurrence_of(X4,X5) ) ),
inference(miniscoping,[status(thm)],[f58]) ).
fof(f60,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f65,plain,
! [X10,X11,X12] :
( earlier(X10,X12)
| ~ earlier(X11,X12)
| ~ earlier(X10,X11) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f66,plain,
! [X10,X12] :
( earlier(X10,X12)
| ! [X11] :
( ~ earlier(X11,X12)
| ~ earlier(X10,X11) ) ),
inference(miniscoping,[status(thm)],[f65]) ).
fof(f67,plain,
! [X0,X1,X2] :
( earlier(X0,X2)
| ~ earlier(X1,X2)
| ~ earlier(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f68,plain,
! [X13,X14,X15] :
( X13 = X15
| earlier(X13,X15)
| earlier(X15,X13)
| ~ earlier(X15,X14)
| ~ earlier(X13,X14) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f69,plain,
! [X13,X15] :
( X13 = X15
| earlier(X13,X15)
| earlier(X15,X13)
| ! [X14] :
( ~ earlier(X15,X14)
| ~ earlier(X13,X14) ) ),
inference(miniscoping,[status(thm)],[f68]) ).
fof(f70,plain,
! [X0,X1,X2] :
( X0 = X2
| earlier(X0,X2)
| earlier(X2,X0)
| ~ earlier(X2,X1)
| ~ earlier(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f77,plain,
! [X19,X20] :
( legal(X20)
| ~ earlier(X20,X19)
| ~ legal(X19) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f78,plain,
! [X20] :
( legal(X20)
| ! [X19] :
( ~ earlier(X20,X19)
| ~ legal(X19) ) ),
inference(miniscoping,[status(thm)],[f77]) ).
fof(f79,plain,
! [X0,X1] :
( legal(X1)
| ~ earlier(X1,X0)
| ~ legal(X0) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f80,plain,
! [X21,X22] :
( ( ~ legal(X22)
| ~ earlier(X21,X22)
| precedes(X21,X22) )
& ( ( legal(X22)
& earlier(X21,X22) )
| ~ precedes(X21,X22) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f81,plain,
( ! [X21,X22] :
( ~ legal(X22)
| ~ earlier(X21,X22)
| precedes(X21,X22) )
& ! [X21,X22] :
( ( legal(X22)
& earlier(X21,X22) )
| ~ precedes(X21,X22) ) ),
inference(miniscoping,[status(thm)],[f80]) ).
fof(f82,plain,
! [X0,X1] :
( earlier(X0,X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
! [X0,X1] :
( legal(X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f84,plain,
! [X0,X1] :
( ~ legal(X1)
| ~ earlier(X0,X1)
| precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f85,plain,
! [X23,X24,X25] :
( ? [X26,X27] :
( atocc(X25,X27)
& atocc(X24,X26)
& subactivity(X27,X23)
& subactivity(X26,X23) )
| ~ min_precedes(X24,X25,X23) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f86,plain,
! [X23,X24,X25] :
( ? [X27] :
( atocc(X25,X27)
& ? [X26] :
( atocc(X24,X26)
& subactivity(X27,X23)
& subactivity(X26,X23) ) )
| ~ min_precedes(X24,X25,X23) ),
inference(miniscoping,[status(thm)],[f85]) ).
fof(f87,plain,
! [X23,X24,X25] :
( ( atocc(X25,sK1_skl(X25,X24,X23))
& atocc(X24,sK2_skl(X25,X24,X23))
& subactivity(sK1_skl(X25,X24,X23),X23)
& subactivity(sK2_skl(X25,X24,X23),X23) )
| ~ min_precedes(X24,X25,X23) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(X27,sK1_skl(X25,X24,X23)),skolemize(X26,sK2_skl(X25,X24,X23))],[f86]) ).
fof(f90,plain,
! [X0,X1,X2] :
( atocc(X0,sK2_skl(X1,X0,X2))
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f96,plain,
! [X31,X32,X33] :
( ? [X34] :
( min_precedes(X34,X32,X33)
& root(X34,X33) )
| ~ min_precedes(X31,X32,X33) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f97,plain,
! [X32,X33] :
( ? [X34] :
( min_precedes(X34,X32,X33)
& root(X34,X33) )
| ! [X31] : ~ min_precedes(X31,X32,X33) ),
inference(miniscoping,[status(thm)],[f96]) ).
fof(f98,plain,
! [X32,X33] :
( ( min_precedes(sK4_skl(X33,X32),X32,X33)
& root(sK4_skl(X33,X32),X33) )
| ! [X31] : ~ min_precedes(X31,X32,X33) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X34,sK4_skl(X33,X32))],[f97]) ).
fof(f99,plain,
! [X0,X1,X2] :
( root(sK4_skl(X2,X1),X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f100,plain,
! [X0,X1,X2] :
( min_precedes(sK4_skl(X2,X1),X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f101,plain,
! [X35,X36,X37] :
( ~ root(X36,X37)
| ~ min_precedes(X35,X36,X37) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f102,plain,
! [X36,X37] :
( ~ root(X36,X37)
| ! [X35] : ~ min_precedes(X35,X36,X37) ),
inference(miniscoping,[status(thm)],[f101]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f104,plain,
! [X38,X39,X40] :
( precedes(X38,X39)
| ~ min_precedes(X38,X39,X40) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f105,plain,
! [X38,X39] :
( precedes(X38,X39)
| ! [X40] : ~ min_precedes(X38,X39,X40) ),
inference(miniscoping,[status(thm)],[f104]) ).
fof(f106,plain,
! [X0,X1,X2] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f118,plain,
! [X52,X53,X54,X55] :
( min_precedes(X53,X54,X55)
| ~ precedes(X53,X54)
| ~ min_precedes(X54,X52,X55)
| ~ min_precedes(X53,X52,X55) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f119,plain,
! [X53,X54,X55] :
( min_precedes(X53,X54,X55)
| ~ precedes(X53,X54)
| ! [X52] :
( ~ min_precedes(X54,X52,X55)
| ~ min_precedes(X53,X52,X55) ) ),
inference(miniscoping,[status(thm)],[f118]) ).
fof(f120,plain,
! [X0,X1,X2,X3] :
( min_precedes(X0,X3,X2)
| ~ precedes(X0,X3)
| ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f137,plain,
! [X64,X65] :
( ( ! [X66] :
( ~ occurrence_of(X64,X66)
| ~ atomic(X66)
| ~ subactivity(X65,X66) )
| atocc(X64,X65) )
& ( ? [X66] :
( occurrence_of(X64,X66)
& atomic(X66)
& subactivity(X65,X66) )
| ~ atocc(X64,X65) ) ),
inference(NNF_transformation,[status(thm)],[f24]) ).
fof(f138,plain,
( ! [X64,X65] :
( ! [X66] :
( ~ occurrence_of(X64,X66)
| ~ atomic(X66)
| ~ subactivity(X65,X66) )
| atocc(X64,X65) )
& ! [X64,X65] :
( ? [X66] :
( occurrence_of(X64,X66)
& atomic(X66)
& subactivity(X65,X66) )
| ~ atocc(X64,X65) ) ),
inference(miniscoping,[status(thm)],[f137]) ).
fof(f139,plain,
( ! [X64,X65] :
( ! [X66] :
( ~ occurrence_of(X64,X66)
| ~ atomic(X66)
| ~ subactivity(X65,X66) )
| atocc(X64,X65) )
& ! [X64,X65] :
( ( occurrence_of(X64,sK8_skl(X65,X64))
& atomic(sK8_skl(X65,X64))
& subactivity(X65,sK8_skl(X65,X64)) )
| ~ atocc(X64,X65) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X66,sK8_skl(X65,X64))],[f138]) ).
fof(f142,plain,
! [X0,X1] :
( occurrence_of(X0,sK8_skl(X1,X0))
| ~ atocc(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f177,plain,
! [X99,X100] :
( ( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ( ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) )
| ~ root_occ(X99,X100) ) ),
inference(NNF_transformation,[status(thm)],[f34]) ).
fof(f178,plain,
( ! [X99,X100] :
( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ! [X99,X100] :
( ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) )
| ~ root_occ(X99,X100) ) ),
inference(miniscoping,[status(thm)],[f177]) ).
fof(f179,plain,
( ! [X99,X100] :
( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ! [X99,X100] :
( ( root(X99,sK13_skl(X100,X99))
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,sK13_skl(X100,X99)) )
| ~ root_occ(X99,X100) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(X101,sK13_skl(X100,X99))],[f178]) ).
fof(f180,plain,
! [X0,X1] :
( occurrence_of(X1,sK13_skl(X1,X0))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f182,plain,
! [X0,X1] :
( root(X0,sK13_skl(X1,X0))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f191,plain,
! [X105] :
( ? [X106,X107,X108] :
( ! [X109] :
( X109 = X108
| X109 = X107
| ~ min_precedes(X106,X109,tptp0) )
& min_precedes(X107,X108,tptp0)
& ( occurrence_of(X108,tptp1)
| occurrence_of(X108,tptp2) )
& min_precedes(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) )
| ~ occurrence_of(X105,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f192,plain,
! [X105] :
( ( ! [X109] :
( X109 = sK17_skl(X105)
| X109 = sK16_skl(X105)
| ~ min_precedes(sK15_skl(X105),X109,tptp0) )
& min_precedes(sK16_skl(X105),sK17_skl(X105),tptp0)
& ( occurrence_of(sK17_skl(X105),tptp1)
| occurrence_of(sK17_skl(X105),tptp2) )
& min_precedes(sK15_skl(X105),sK16_skl(X105),tptp0)
& occurrence_of(sK16_skl(X105),tptp4)
& root_occ(sK15_skl(X105),X105)
& occurrence_of(sK15_skl(X105),tptp3) )
| ~ occurrence_of(X105,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(X106,sK15_skl(X105)),skolemize(X107,sK16_skl(X105)),skolemize(X108,sK17_skl(X105))],[f191]) ).
fof(f193,plain,
! [X0] :
( occurrence_of(sK15_skl(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f194,plain,
! [X0] :
( root_occ(sK15_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f196,plain,
! [X0] :
( min_precedes(sK15_skl(X0),sK16_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f197,plain,
! [X0] :
( occurrence_of(sK17_skl(X0),tptp1)
| occurrence_of(sK17_skl(X0),tptp2)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f198,plain,
! [X0] :
( min_precedes(sK16_skl(X0),sK17_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f212,plain,
? [X110] :
( ! [X111,X112] :
( ~ min_precedes(X111,X112,tptp0)
| ( ~ occurrence_of(X112,tptp1)
& ~ occurrence_of(X112,tptp2) )
| ~ root_occ(X111,X110)
| ~ occurrence_of(X111,tptp3) )
& occurrence_of(X110,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f213,plain,
( ! [X111,X112] :
( ~ min_precedes(X111,X112,tptp0)
| ( ~ occurrence_of(X112,tptp1)
& ~ occurrence_of(X112,tptp2) )
| ~ root_occ(X111,sK18_skl)
| ~ occurrence_of(X111,tptp3) )
& occurrence_of(sK18_skl,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(X110,sK18_skl)],[f212]) ).
fof(f214,plain,
occurrence_of(sK18_skl,tptp0),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f215,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp2)
| ~ root_occ(X0,sK18_skl)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f216,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp1)
| ~ root_occ(X0,sK18_skl)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f217,plain,
! [X0] :
( X0 = tptp0
| ~ occurrence_of(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f60,f214]) ).
fof(f221,plain,
min_precedes(sK15_skl(sK18_skl),sK16_skl(sK18_skl),tptp0),
inference(resolution,[status(thm)],[f196,f214]) ).
fof(f226,plain,
precedes(sK15_skl(sK18_skl),sK16_skl(sK18_skl)),
inference(resolution,[status(thm)],[f221,f106]) ).
fof(f228,plain,
earlier(sK15_skl(sK18_skl),sK16_skl(sK18_skl)),
inference(resolution,[status(thm)],[f226,f82]) ).
fof(f235,plain,
min_precedes(sK16_skl(sK18_skl),sK17_skl(sK18_skl),tptp0),
inference(resolution,[status(thm)],[f198,f214]) ).
fof(f236,plain,
legal(sK16_skl(sK18_skl)),
inference(resolution,[status(thm)],[f83,f226]) ).
fof(f237,plain,
! [X0] :
( legal(X0)
| ~ earlier(X0,sK16_skl(sK18_skl)) ),
inference(resolution,[status(thm)],[f236,f79]) ).
fof(f240,plain,
! [X0] :
( ~ earlier(X0,sK16_skl(sK18_skl))
| precedes(X0,sK16_skl(sK18_skl)) ),
inference(resolution,[status(thm)],[f236,f84]) ).
fof(f242,plain,
legal(sK15_skl(sK18_skl)),
inference(resolution,[status(thm)],[f237,f228]) ).
fof(f246,plain,
! [X0] :
( ~ earlier(X0,sK15_skl(sK18_skl))
| precedes(X0,sK15_skl(sK18_skl)) ),
inference(resolution,[status(thm)],[f242,f84]) ).
fof(f249,plain,
min_precedes(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK17_skl(sK18_skl),tptp0),
inference(resolution,[status(thm)],[f235,f100]) ).
fof(f250,plain,
root(sK4_skl(tptp0,sK17_skl(sK18_skl)),tptp0),
inference(resolution,[status(thm)],[f235,f99]) ).
fof(f251,plain,
precedes(sK16_skl(sK18_skl),sK17_skl(sK18_skl)),
inference(resolution,[status(thm)],[f235,f106]) ).
fof(f254,plain,
legal(sK17_skl(sK18_skl)),
inference(resolution,[status(thm)],[f251,f83]) ).
fof(f255,plain,
earlier(sK16_skl(sK18_skl),sK17_skl(sK18_skl)),
inference(resolution,[status(thm)],[f251,f82]) ).
fof(f256,plain,
! [X0] :
( legal(X0)
| ~ earlier(X0,sK17_skl(sK18_skl)) ),
inference(resolution,[status(thm)],[f254,f79]) ).
fof(f261,plain,
! [X0] :
( X0 = sK16_skl(sK18_skl)
| earlier(X0,sK16_skl(sK18_skl))
| earlier(sK16_skl(sK18_skl),X0)
| ~ earlier(X0,sK17_skl(sK18_skl)) ),
inference(resolution,[status(thm)],[f255,f70]) ).
fof(f262,plain,
! [X0] :
( earlier(X0,sK17_skl(sK18_skl))
| ~ earlier(X0,sK16_skl(sK18_skl)) ),
inference(resolution,[status(thm)],[f255,f67]) ).
fof(f270,plain,
! [X0] : ~ min_precedes(X0,sK4_skl(tptp0,sK17_skl(sK18_skl)),tptp0),
inference(resolution,[status(thm)],[f250,f103]) ).
fof(f280,plain,
earlier(sK15_skl(sK18_skl),sK17_skl(sK18_skl)),
inference(resolution,[status(thm)],[f262,f228]) ).
fof(f283,plain,
! [X0] :
( X0 = sK15_skl(sK18_skl)
| earlier(X0,sK15_skl(sK18_skl))
| earlier(sK15_skl(sK18_skl),X0)
| ~ earlier(X0,sK17_skl(sK18_skl)) ),
inference(resolution,[status(thm)],[f280,f70]) ).
fof(f289,plain,
atocc(sK15_skl(sK18_skl),sK2_skl(sK16_skl(sK18_skl),sK15_skl(sK18_skl),tptp0)),
inference(resolution,[status(thm)],[f90,f221]) ).
fof(f328,plain,
precedes(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK17_skl(sK18_skl)),
inference(resolution,[status(thm)],[f249,f106]) ).
fof(f331,plain,
earlier(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK17_skl(sK18_skl)),
inference(resolution,[status(thm)],[f328,f82]) ).
fof(f333,plain,
legal(sK4_skl(tptp0,sK17_skl(sK18_skl))),
inference(resolution,[status(thm)],[f331,f256]) ).
fof(f343,plain,
! [X0] :
( ~ earlier(X0,sK4_skl(tptp0,sK17_skl(sK18_skl)))
| precedes(X0,sK4_skl(tptp0,sK17_skl(sK18_skl))) ),
inference(resolution,[status(thm)],[f333,f84]) ).
fof(f398,plain,
! [X0] :
( min_precedes(X0,sK4_skl(tptp0,sK17_skl(sK18_skl)),tptp0)
| ~ precedes(X0,sK4_skl(tptp0,sK17_skl(sK18_skl)))
| ~ min_precedes(X0,sK17_skl(sK18_skl),tptp0) ),
inference(resolution,[status(thm)],[f120,f249]) ).
fof(f400,plain,
! [X0] :
( min_precedes(X0,sK16_skl(sK18_skl),tptp0)
| ~ precedes(X0,sK16_skl(sK18_skl))
| ~ min_precedes(X0,sK17_skl(sK18_skl),tptp0) ),
inference(resolution,[status(thm)],[f120,f235]) ).
fof(f401,plain,
! [X0] :
( min_precedes(X0,sK15_skl(sK18_skl),tptp0)
| ~ precedes(X0,sK15_skl(sK18_skl))
| ~ min_precedes(X0,sK16_skl(sK18_skl),tptp0) ),
inference(resolution,[status(thm)],[f120,f221]) ).
fof(f402,plain,
! [X0] :
( ~ precedes(X0,sK4_skl(tptp0,sK17_skl(sK18_skl)))
| ~ min_precedes(X0,sK17_skl(sK18_skl),tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f398,f270]) ).
fof(f449,plain,
( min_precedes(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK16_skl(sK18_skl),tptp0)
| ~ precedes(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK16_skl(sK18_skl)) ),
inference(resolution,[status(thm)],[f400,f249]) ).
fof(f471,plain,
! [X0,X1,X2] :
( X2 = sK8_skl(X1,X0)
| ~ occurrence_of(X0,X2)
| ~ atocc(X0,X1) ),
inference(resolution,[status(thm)],[f142,f60]) ).
fof(f529,plain,
( sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK16_skl(sK18_skl)
| earlier(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK16_skl(sK18_skl))
| earlier(sK16_skl(sK18_skl),sK4_skl(tptp0,sK17_skl(sK18_skl))) ),
inference(resolution,[status(thm)],[f261,f331]) ).
fof(f533,plain,
( sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK15_skl(sK18_skl)
| earlier(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK15_skl(sK18_skl))
| earlier(sK15_skl(sK18_skl),sK4_skl(tptp0,sK17_skl(sK18_skl))) ),
inference(resolution,[status(thm)],[f283,f331]) ).
fof(f992,plain,
! [X0,X1] :
( tptp3 = sK8_skl(X1,sK15_skl(X0))
| ~ atocc(sK15_skl(X0),X1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f193,f471]) ).
fof(f994,plain,
! [X0] :
( ~ min_precedes(sK15_skl(sK18_skl),X0,tptp0)
| ~ occurrence_of(X0,tptp1)
| ~ occurrence_of(sK15_skl(sK18_skl),tptp3)
| ~ occurrence_of(sK18_skl,tptp0) ),
inference(resolution,[status(thm)],[f194,f216]) ).
fof(f995,plain,
! [X0] :
( ~ min_precedes(sK15_skl(sK18_skl),X0,tptp0)
| ~ occurrence_of(X0,tptp2)
| ~ occurrence_of(sK15_skl(sK18_skl),tptp3)
| ~ occurrence_of(sK18_skl,tptp0) ),
inference(resolution,[status(thm)],[f194,f215]) ).
fof(f996,plain,
! [X0] :
( occurrence_of(X0,sK13_skl(X0,sK15_skl(X0)))
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f194,f180]) ).
fof(f997,plain,
! [X0] :
( root(sK15_skl(X0),sK13_skl(X0,sK15_skl(X0)))
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f194,f182]) ).
fof(f999,plain,
! [X0] :
( ~ min_precedes(sK15_skl(sK18_skl),X0,tptp0)
| ~ occurrence_of(X0,tptp1)
| ~ occurrence_of(sK15_skl(sK18_skl),tptp3) ),
inference(forward_subsumption_resolution,[status(thm)],[f994,f214]) ).
fof(f1000,plain,
! [X0] :
( ~ min_precedes(sK15_skl(sK18_skl),X0,tptp0)
| ~ occurrence_of(X0,tptp2)
| ~ occurrence_of(sK15_skl(sK18_skl),tptp3) ),
inference(forward_subsumption_resolution,[status(thm)],[f995,f214]) ).
fof(f1081,plain,
! [X0] :
( ~ min_precedes(sK15_skl(sK18_skl),sK17_skl(X0),tptp0)
| ~ occurrence_of(sK15_skl(sK18_skl),tptp3)
| occurrence_of(sK17_skl(X0),tptp2)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f197,f999]) ).
fof(f1085,plain,
! [X0] :
( ~ min_precedes(sK15_skl(sK18_skl),sK17_skl(X0),tptp0)
| ~ occurrence_of(sK15_skl(sK18_skl),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1081,f1000]) ).
fof(f1380,plain,
( tptp3 = sK8_skl(sK2_skl(sK16_skl(sK18_skl),sK15_skl(sK18_skl),tptp0),sK15_skl(sK18_skl))
| ~ occurrence_of(sK18_skl,tptp0) ),
inference(resolution,[status(thm)],[f992,f289]) ).
fof(f1384,plain,
tptp3 = sK8_skl(sK2_skl(sK16_skl(sK18_skl),sK15_skl(sK18_skl),tptp0),sK15_skl(sK18_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f1380,f214]) ).
fof(f1388,plain,
( occurrence_of(sK15_skl(sK18_skl),tptp3)
| ~ atocc(sK15_skl(sK18_skl),sK2_skl(sK16_skl(sK18_skl),sK15_skl(sK18_skl),tptp0)) ),
inference(paramodulation,[status(thm)],[f1384,f142]) ).
fof(f1392,plain,
! [X0] :
( ~ min_precedes(sK15_skl(sK18_skl),sK17_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1085,f1395]) ).
fof(f1395,plain,
occurrence_of(sK15_skl(sK18_skl),tptp3),
inference(forward_subsumption_resolution,[status(thm)],[f1388,f289]) ).
fof(f1438,plain,
( sK13_skl(sK18_skl,sK15_skl(sK18_skl)) = tptp0
| ~ occurrence_of(sK18_skl,tptp0) ),
inference(resolution,[status(thm)],[f996,f217]) ).
fof(f1442,plain,
sK13_skl(sK18_skl,sK15_skl(sK18_skl)) = tptp0,
inference(forward_subsumption_resolution,[status(thm)],[f1438,f214]) ).
fof(f1453,plain,
( root(sK15_skl(sK18_skl),tptp0)
| ~ occurrence_of(sK18_skl,tptp0) ),
inference(paramodulation,[status(thm)],[f1442,f997]) ).
fof(f1455,plain,
root(sK15_skl(sK18_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f1453,f214]) ).
fof(f1461,plain,
! [X0] : ~ min_precedes(X0,sK15_skl(sK18_skl),tptp0),
inference(resolution,[status(thm)],[f1455,f103]) ).
fof(f1463,plain,
! [X0] :
( ~ precedes(X0,sK15_skl(sK18_skl))
| ~ min_precedes(X0,sK16_skl(sK18_skl),tptp0) ),
inference(backward_subsumption_resolution,[status(thm)],[f401,f1461]) ).
fof(f3819,plain,
( precedes(sK16_skl(sK18_skl),sK4_skl(tptp0,sK17_skl(sK18_skl)))
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK16_skl(sK18_skl)
| earlier(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK16_skl(sK18_skl)) ),
inference(resolution,[status(thm)],[f529,f343]) ).
fof(f3825,plain,
( precedes(sK15_skl(sK18_skl),sK4_skl(tptp0,sK17_skl(sK18_skl)))
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK15_skl(sK18_skl)
| earlier(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK15_skl(sK18_skl)) ),
inference(resolution,[status(thm)],[f533,f343]) ).
fof(f5194,plain,
( ~ min_precedes(sK16_skl(sK18_skl),sK17_skl(sK18_skl),tptp0)
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK16_skl(sK18_skl)
| earlier(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK16_skl(sK18_skl)) ),
inference(resolution,[status(thm)],[f3819,f402]) ).
fof(f5197,plain,
( sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK16_skl(sK18_skl)
| earlier(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK16_skl(sK18_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5194,f235]) ).
fof(f5201,plain,
( precedes(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK16_skl(sK18_skl))
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK16_skl(sK18_skl) ),
inference(resolution,[status(thm)],[f5197,f240]) ).
fof(f5272,plain,
( min_precedes(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK16_skl(sK18_skl),tptp0)
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK16_skl(sK18_skl) ),
inference(resolution,[status(thm)],[f5201,f449]) ).
fof(f5285,plain,
! [X0] :
( min_precedes(X0,sK4_skl(tptp0,sK17_skl(sK18_skl)),tptp0)
| ~ precedes(X0,sK4_skl(tptp0,sK17_skl(sK18_skl)))
| ~ min_precedes(X0,sK16_skl(sK18_skl),tptp0)
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK16_skl(sK18_skl) ),
inference(resolution,[status(thm)],[f5272,f120]) ).
fof(f5298,plain,
! [X0] :
( ~ precedes(X0,sK4_skl(tptp0,sK17_skl(sK18_skl)))
| ~ min_precedes(X0,sK16_skl(sK18_skl),tptp0)
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK16_skl(sK18_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f5285,f270]) ).
fof(f5436,plain,
( ~ min_precedes(sK15_skl(sK18_skl),sK16_skl(sK18_skl),tptp0)
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK16_skl(sK18_skl)
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK15_skl(sK18_skl)
| earlier(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK15_skl(sK18_skl)) ),
inference(resolution,[status(thm)],[f3825,f5298]) ).
fof(f5440,plain,
( sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK16_skl(sK18_skl)
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK15_skl(sK18_skl)
| earlier(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK15_skl(sK18_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5436,f221]) ).
fof(f5443,plain,
( precedes(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK15_skl(sK18_skl))
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK16_skl(sK18_skl)
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK15_skl(sK18_skl) ),
inference(resolution,[status(thm)],[f5440,f246]) ).
fof(f5451,plain,
( ~ min_precedes(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK16_skl(sK18_skl),tptp0)
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK16_skl(sK18_skl)
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK15_skl(sK18_skl) ),
inference(resolution,[status(thm)],[f5443,f1463]) ).
fof(f5454,plain,
( sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK16_skl(sK18_skl)
| sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK15_skl(sK18_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f5451,f5272]) ).
fof(f5564,plain,
! [X0] :
( sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK15_skl(sK18_skl)
| ~ min_precedes(X0,sK16_skl(sK18_skl),tptp0) ),
inference(paramodulation,[status(thm)],[f5454,f270]) ).
fof(f5655,plain,
sK4_skl(tptp0,sK17_skl(sK18_skl)) = sK15_skl(sK18_skl),
inference(resolution,[status(thm)],[f5564,f221]) ).
fof(f5803,plain,
min_precedes(sK15_skl(sK18_skl),sK17_skl(sK18_skl),tptp0),
inference(backward_demodulation,[status(thm)],[f5655,f249]) ).
fof(f6928,plain,
~ occurrence_of(sK18_skl,tptp0),
inference(resolution,[status(thm)],[f5803,f1392]) ).
fof(f6953,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f6928,f214]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PRO012+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n001.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 03:47:59 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.49 % Drodi V4.1.1
% 102.97/13.61 % Refutation found
% 102.97/13.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 102.97/13.61 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.37/13.77 % Elapsed time: 13.291161 seconds
% 11.37/13.77 % CPU time: 104.388738 seconds
% 11.37/13.77 % Total memory used: 465.389 MB
% 11.37/13.77 % Net memory used: 437.298 MB
%------------------------------------------------------------------------------