%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO011+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 : n015.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 0.11s 0.38s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 13
% Syntax : Number of formulae : 75 ( 14 unt; 7 def)
% Number of atoms : 280 ( 14 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 303 ( 98 ~; 98 |; 89 &)
% ( 10 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 7 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-3 aty)
% Number of variables : 151 ( 116 !; 35 ?)
% 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(f22,axiom,
! [X56,X57] :
( leaf(X56,X57)
<=> ( ~ ? [X59] : min_precedes(X56,X59,X57)
& ( ? [X58] : min_precedes(X58,X56,X57)
| root(X56,X57) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [X102,X103] :
( leaf_occ(X102,X103)
<=> ? [X104] :
( leaf(X102,X104)
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,X104) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X105] :
( occurrence_of(X105,tptp0)
=> ? [X106,X107,X108] :
( leaf_occ(X108,X105)
& next_subocc(X107,X108,tptp0)
& ( occurrence_of(X108,tptp2)
| occurrence_of(X108,tptp1) )
& next_subocc(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
tptp1 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,conjecture,
! [X109] :
( occurrence_of(X109,tptp0)
=> ? [X110,X111] :
( ( occurrence_of(X111,tptp2)
=> ~ ? [X113] :
( min_precedes(X110,X113,tptp0)
& subactivity_occurrence(X113,X109)
& occurrence_of(X113,tptp1) ) )
& ( occurrence_of(X111,tptp1)
=> ~ ? [X112] :
( min_precedes(X110,X112,tptp0)
& subactivity_occurrence(X112,X109)
& occurrence_of(X112,tptp2) ) )
& leaf_occ(X111,X109) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,negated_conjecture,
~ ! [X109] :
( occurrence_of(X109,tptp0)
=> ? [X110,X111] :
( ( occurrence_of(X111,tptp2)
=> ~ ? [X113] :
( min_precedes(X110,X113,tptp0)
& subactivity_occurrence(X113,X109)
& occurrence_of(X113,tptp1) ) )
& ( occurrence_of(X111,tptp1)
=> ~ ? [X112] :
( min_precedes(X110,X112,tptp0)
& subactivity_occurrence(X112,X109)
& occurrence_of(X112,tptp2) ) )
& leaf_occ(X111,X109) ) ),
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(f121,plain,
! [X56,X57] :
( leaf(X56,X57)
<=> ( ! [X59] : ~ min_precedes(X56,X59,X57)
& ( ? [X58] : min_precedes(X58,X56,X57)
| root(X56,X57) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f122,plain,
! [X56,X57] :
( ( ? [X59] : min_precedes(X56,X59,X57)
| ( ! [X58] : ~ min_precedes(X58,X56,X57)
& ~ root(X56,X57) )
| leaf(X56,X57) )
& ( ( ! [X59] : ~ min_precedes(X56,X59,X57)
& ( ? [X58] : min_precedes(X58,X56,X57)
| root(X56,X57) ) )
| ~ leaf(X56,X57) ) ),
inference(NNF_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
( ! [X56,X57] :
( ? [X59] : min_precedes(X56,X59,X57)
| ( ! [X58] : ~ min_precedes(X58,X56,X57)
& ~ root(X56,X57) )
| leaf(X56,X57) )
& ! [X56,X57] :
( ( ! [X59] : ~ min_precedes(X56,X59,X57)
& ( ? [X58] : min_precedes(X58,X56,X57)
| root(X56,X57) ) )
| ~ leaf(X56,X57) ) ),
inference(miniscoping,[status(thm)],[f122]) ).
fof(f124,plain,
( ! [X56,X57] :
( min_precedes(X56,sK6_skl(X57,X56),X57)
| ( ! [X58] : ~ min_precedes(X58,X56,X57)
& ~ root(X56,X57) )
| leaf(X56,X57) )
& ! [X56,X57] :
( ( ! [X59] : ~ min_precedes(X56,X59,X57)
& ( min_precedes(sK5_skl(X57,X56),X56,X57)
| root(X56,X57) ) )
| ~ leaf(X56,X57) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl]),skolemize(X58,sK5_skl(X57,X56)),skolemize(X59,sK6_skl(X57,X56))],[f123]) ).
fof(f126,plain,
! [X0,X1,X2] :
( ~ min_precedes(X0,X2,X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f184,plain,
! [X102,X103] :
( ( ! [X104] :
( ~ leaf(X102,X104)
| ~ subactivity_occurrence(X102,X103)
| ~ occurrence_of(X103,X104) )
| leaf_occ(X102,X103) )
& ( ? [X104] :
( leaf(X102,X104)
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,X104) )
| ~ leaf_occ(X102,X103) ) ),
inference(NNF_transformation,[status(thm)],[f35]) ).
fof(f185,plain,
( ! [X102,X103] :
( ! [X104] :
( ~ leaf(X102,X104)
| ~ subactivity_occurrence(X102,X103)
| ~ occurrence_of(X103,X104) )
| leaf_occ(X102,X103) )
& ! [X102,X103] :
( ? [X104] :
( leaf(X102,X104)
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,X104) )
| ~ leaf_occ(X102,X103) ) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f186,plain,
( ! [X102,X103] :
( ! [X104] :
( ~ leaf(X102,X104)
| ~ subactivity_occurrence(X102,X103)
| ~ occurrence_of(X103,X104) )
| leaf_occ(X102,X103) )
& ! [X102,X103] :
( ( leaf(X102,sK14_skl(X103,X102))
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,sK14_skl(X103,X102)) )
| ~ leaf_occ(X102,X103) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X104,sK14_skl(X103,X102))],[f185]) ).
fof(f187,plain,
! [X0,X1] :
( occurrence_of(X1,sK14_skl(X1,X0))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f189,plain,
! [X0,X1] :
( leaf(X0,sK14_skl(X1,X0))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f191,plain,
! [X105] :
( ? [X106,X107,X108] :
( leaf_occ(X108,X105)
& next_subocc(X107,X108,tptp0)
& ( occurrence_of(X108,tptp2)
| occurrence_of(X108,tptp1) )
& next_subocc(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] :
( ? [X108] :
( leaf_occ(X108,X105)
& ? [X107] :
( next_subocc(X107,X108,tptp0)
& ( occurrence_of(X108,tptp2)
| occurrence_of(X108,tptp1) )
& ? [X106] :
( next_subocc(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) ) ) )
| ~ occurrence_of(X105,tptp0) ),
inference(miniscoping,[status(thm)],[f191]) ).
fof(f193,plain,
! [X105] :
( ( leaf_occ(sK15_skl(X105),X105)
& next_subocc(sK16_skl(X105),sK15_skl(X105),tptp0)
& ( occurrence_of(sK15_skl(X105),tptp2)
| occurrence_of(sK15_skl(X105),tptp1) )
& next_subocc(sK17_skl(X105),sK16_skl(X105),tptp0)
& occurrence_of(sK16_skl(X105),tptp4)
& root_occ(sK17_skl(X105),X105)
& occurrence_of(sK17_skl(X105),tptp3) )
| ~ occurrence_of(X105,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(X108,sK15_skl(X105)),skolemize(X107,sK16_skl(X105)),skolemize(X106,sK17_skl(X105))],[f192]) ).
fof(f200,plain,
! [X0] :
( leaf_occ(sK15_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f212,plain,
tptp1 != tptp2,
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f213,plain,
? [X109] :
( ! [X110,X111] :
( ( ? [X113] :
( min_precedes(X110,X113,tptp0)
& subactivity_occurrence(X113,X109)
& occurrence_of(X113,tptp1) )
& occurrence_of(X111,tptp2) )
| ( ? [X112] :
( min_precedes(X110,X112,tptp0)
& subactivity_occurrence(X112,X109)
& occurrence_of(X112,tptp2) )
& occurrence_of(X111,tptp1) )
| ~ leaf_occ(X111,X109) )
& occurrence_of(X109,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f214,definition,
! [X109,X110,X111] :
( sP0_prd(X111,X110,X109)
<=> ( ? [X112] :
( min_precedes(X110,X112,tptp0)
& subactivity_occurrence(X112,X109)
& occurrence_of(X112,tptp2) )
& occurrence_of(X111,tptp1) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f215,plain,
? [X109] :
( ! [X110,X111] :
( ( ? [X113] :
( min_precedes(X110,X113,tptp0)
& subactivity_occurrence(X113,X109)
& occurrence_of(X113,tptp1) )
& occurrence_of(X111,tptp2) )
| sP0_prd(X111,X110,X109)
| ~ leaf_occ(X111,X109) )
& occurrence_of(X109,tptp0) ),
inference(formula_renaming,[status(thm)],[f213,f214]) ).
fof(f216,plain,
( ! [X110,X111] :
( ( min_precedes(X110,sK19_skl(X111,X110),tptp0)
& subactivity_occurrence(sK19_skl(X111,X110),sK18_skl)
& occurrence_of(sK19_skl(X111,X110),tptp1)
& occurrence_of(X111,tptp2) )
| sP0_prd(X111,X110,sK18_skl)
| ~ leaf_occ(X111,sK18_skl) )
& occurrence_of(sK18_skl,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl]),skolemize(X109,sK18_skl),skolemize(X113,sK19_skl(X111,X110))],[f215]) ).
fof(f217,plain,
occurrence_of(sK18_skl,tptp0),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f218,plain,
! [X0,X1] :
( occurrence_of(X0,tptp2)
| sP0_prd(X0,X1,sK18_skl)
| ~ leaf_occ(X0,sK18_skl) ),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f221,plain,
! [X0,X1] :
( min_precedes(X1,sK19_skl(X0,X1),tptp0)
| sP0_prd(X0,X1,sK18_skl)
| ~ leaf_occ(X0,sK18_skl) ),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f222,plain,
! [X109,X110,X111] :
( ( ! [X112] :
( ~ min_precedes(X110,X112,tptp0)
| ~ subactivity_occurrence(X112,X109)
| ~ occurrence_of(X112,tptp2) )
| ~ occurrence_of(X111,tptp1)
| sP0_prd(X111,X110,X109) )
& ( ( ? [X112] :
( min_precedes(X110,X112,tptp0)
& subactivity_occurrence(X112,X109)
& occurrence_of(X112,tptp2) )
& occurrence_of(X111,tptp1) )
| ~ sP0_prd(X111,X110,X109) ) ),
inference(NNF_transformation,[status(thm)],[f214]) ).
fof(f223,plain,
( ! [X109,X110,X111] :
( ! [X112] :
( ~ min_precedes(X110,X112,tptp0)
| ~ subactivity_occurrence(X112,X109)
| ~ occurrence_of(X112,tptp2) )
| ~ occurrence_of(X111,tptp1)
| sP0_prd(X111,X110,X109) )
& ! [X109,X110,X111] :
( ( ? [X112] :
( min_precedes(X110,X112,tptp0)
& subactivity_occurrence(X112,X109)
& occurrence_of(X112,tptp2) )
& occurrence_of(X111,tptp1) )
| ~ sP0_prd(X111,X110,X109) ) ),
inference(miniscoping,[status(thm)],[f222]) ).
fof(f224,plain,
( ! [X109,X110,X111] :
( ! [X112] :
( ~ min_precedes(X110,X112,tptp0)
| ~ subactivity_occurrence(X112,X109)
| ~ occurrence_of(X112,tptp2) )
| ~ occurrence_of(X111,tptp1)
| sP0_prd(X111,X110,X109) )
& ! [X109,X110,X111] :
( ( min_precedes(X110,sK20_skl(X111,X110,X109),tptp0)
& subactivity_occurrence(sK20_skl(X111,X110,X109),X109)
& occurrence_of(sK20_skl(X111,X110,X109),tptp2)
& occurrence_of(X111,tptp1) )
| ~ sP0_prd(X111,X110,X109) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(X112,sK20_skl(X111,X110,X109))],[f223]) ).
fof(f225,plain,
! [X0,X1,X2] :
( occurrence_of(X0,tptp1)
| ~ sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f228,plain,
! [X0,X1,X2] :
( min_precedes(X1,sK20_skl(X0,X1,X2),tptp0)
| ~ sP0_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f231,plain,
! [X0] :
( X0 = tptp0
| ~ occurrence_of(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f60,f217]) ).
fof(f340,plain,
leaf_occ(sK15_skl(sK18_skl),sK18_skl),
inference(resolution,[status(thm)],[f200,f217]) ).
fof(f345,plain,
leaf(sK15_skl(sK18_skl),sK14_skl(sK18_skl,sK15_skl(sK18_skl))),
inference(resolution,[status(thm)],[f340,f189]) ).
fof(f346,plain,
occurrence_of(sK18_skl,sK14_skl(sK18_skl,sK15_skl(sK18_skl))),
inference(resolution,[status(thm)],[f340,f187]) ).
fof(f347,definition,
! [X0] :
( sQ9_spl
<=> ( X0 = tptp2
| ~ occurrence_of(sK15_skl(sK18_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f348,plain,
! [X0] :
( ~ sQ9_spl
| X0 = tptp2
| ~ occurrence_of(sK15_skl(sK18_skl),X0) ),
inference(component_clause,[status(thm)],[f347]) ).
fof(f350,definition,
! [X1] :
( sQ10_spl
<=> sP0_prd(sK15_skl(sK18_skl),X1,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f351,plain,
! [X0] :
( ~ sQ10_spl
| sP0_prd(sK15_skl(sK18_skl),X0,sK18_skl) ),
inference(component_clause,[status(thm)],[f350]) ).
fof(f361,plain,
! [X0] :
( ~ sQ10_spl
| min_precedes(X0,sK20_skl(sK15_skl(sK18_skl),X0,sK18_skl),tptp0) ),
inference(resolution,[status(thm)],[f351,f228]) ).
fof(f391,definition,
( sQ15_spl
<=> leaf_occ(sK15_skl(sK18_skl),sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f393,plain,
( sQ15_spl
| ~ leaf_occ(sK15_skl(sK18_skl),sK18_skl) ),
inference(component_clause,[status(thm)],[f391]) ).
fof(f395,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f393,f340]) ).
fof(f396,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f395]) ).
fof(f416,definition,
( sQ16_spl
<=> occurrence_of(sK15_skl(sK18_skl),tptp2) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f417,plain,
( ~ sQ16_spl
| occurrence_of(sK15_skl(sK18_skl),tptp2) ),
inference(component_clause,[status(thm)],[f416]) ).
fof(f418,plain,
( sQ16_spl
| ~ occurrence_of(sK15_skl(sK18_skl),tptp2) ),
inference(component_clause,[status(thm)],[f416]) ).
fof(f426,plain,
! [X0] :
( min_precedes(X0,sK19_skl(sK15_skl(sK18_skl),X0),tptp0)
| sP0_prd(sK15_skl(sK18_skl),X0,sK18_skl) ),
inference(resolution,[status(thm)],[f340,f221]) ).
fof(f456,plain,
! [X0] :
( ~ sQ16_spl
| X0 = tptp2
| ~ occurrence_of(sK15_skl(sK18_skl),X0) ),
inference(resolution,[status(thm)],[f417,f60]) ).
fof(f462,plain,
! [X0,X1] :
( ~ sQ9_spl
| ~ sP0_prd(sK15_skl(sK18_skl),X0,X1)
| tptp1 = tptp2 ),
inference(resolution,[status(thm)],[f348,f225]) ).
fof(f468,definition,
( sQ22_spl
<=> tptp1 = tptp2 ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f469,plain,
( ~ sQ22_spl
| tptp1 = tptp2 ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f471,definition,
! [X0,X1] :
( sQ23_spl
<=> ~ sP0_prd(sK15_skl(sK18_skl),X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f472,plain,
! [X0,X1] :
( ~ sQ23_spl
| ~ sP0_prd(sK15_skl(sK18_skl),X0,X1) ),
inference(component_clause,[status(thm)],[f471]) ).
fof(f474,plain,
( ~ sQ9_spl
| sQ23_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f462,f468,f471,f347]) ).
fof(f475,plain,
( ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f469,f212]) ).
fof(f476,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f475]) ).
fof(f574,plain,
sK14_skl(sK18_skl,sK15_skl(sK18_skl)) = tptp0,
inference(resolution,[status(thm)],[f346,f231]) ).
fof(f583,plain,
leaf(sK15_skl(sK18_skl),tptp0),
inference(backward_demodulation,[status(thm)],[f574,f345]) ).
fof(f585,plain,
! [X0] : ~ min_precedes(sK15_skl(sK18_skl),X0,tptp0),
inference(resolution,[status(thm)],[f583,f126]) ).
fof(f623,plain,
( ~ sQ16_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f456,f347,f416]) ).
fof(f629,plain,
! [X0] :
( ~ sQ23_spl
| min_precedes(X0,sK19_skl(sK15_skl(sK18_skl),X0),tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f426,f472]) ).
fof(f630,plain,
( ~ sQ23_spl
| $false ),
inference(resolution,[status(thm)],[f629,f585]) ).
fof(f642,plain,
~ sQ23_spl,
inference(contradiction_clause,[status(thm)],[f630]) ).
fof(f646,plain,
! [X0] :
( sQ16_spl
| sP0_prd(sK15_skl(sK18_skl),X0,sK18_skl)
| ~ leaf_occ(sK15_skl(sK18_skl),sK18_skl) ),
inference(resolution,[status(thm)],[f418,f218]) ).
fof(f647,plain,
( sQ16_spl
| sQ10_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f646,f391,f350,f416]) ).
fof(f817,plain,
( ~ sQ10_spl
| $false ),
inference(resolution,[status(thm)],[f361,f585]) ).
fof(f830,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f817]) ).
fof(f831,plain,
$false,
inference(sat_refutation,[status(thm)],[f396,f474,f476,f623,f642,f647,f830]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO011+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n015.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 03:45:51 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 0.11/0.38 % Refutation found
% 0.11/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.11/0.41 % Elapsed time: 0.060560 seconds
% 0.11/0.41 % CPU time: 0.207550 seconds
% 0.11/0.41 % Total memory used: 85.798 MB
% 0.11/0.41 % Net memory used: 85.574 MB
%------------------------------------------------------------------------------