%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO014+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:18 PM UTC 2026
% Result : Theorem 0.02s 0.54s
% Output : CNFRefutation 0.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 4
% Syntax : Number of formulae : 69 ( 16 unt; 0 def)
% Number of atoms : 280 ( 0 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 335 ( 124 ~; 136 |; 69 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-3 aty)
% Number of variables : 103 ( 83 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X1,X2,X3)
& min_precedes(X0,X1,X3) )
=> min_precedes(X0,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X15,X16,X17] :
( next_subocc(X15,X16,X17)
<=> ( ~ ? [X18] :
( min_precedes(X18,X16,X17)
& min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X95,X96] :
( ( ~ leaf_occ(X95,X96)
& arboreal(X95)
& subactivity_occurrence(X95,X96)
& occurrence_of(X96,tptp0) )
=> ? [X97,X98,X99] :
( leaf(X99,tptp0)
& next_subocc(X98,X99,tptp0)
& ( occurrence_of(X99,tptp1)
| occurrence_of(X99,tptp2) )
& next_subocc(X97,X98,tptp0)
& occurrence_of(X98,tptp4)
& next_subocc(X95,X97,tptp0)
& occurrence_of(X97,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,conjecture,
! [X100,X101] :
( ( ~ leaf_occ(X100,X101)
& arboreal(X100)
& subactivity_occurrence(X100,X101)
& occurrence_of(X101,tptp0) )
=> ? [X102,X103] :
( leaf(X103,tptp0)
& min_precedes(X102,X103,tptp0)
& ( occurrence_of(X103,tptp1)
| occurrence_of(X103,tptp2) )
& next_subocc(X100,X102,tptp0)
& occurrence_of(X102,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
~ ! [X100,X101] :
( ( ~ leaf_occ(X100,X101)
& arboreal(X100)
& subactivity_occurrence(X100,X101)
& occurrence_of(X101,tptp0) )
=> ? [X102,X103] :
( leaf(X103,tptp0)
& min_precedes(X102,X103,tptp0)
& ( occurrence_of(X103,tptp1)
| occurrence_of(X103,tptp2) )
& next_subocc(X100,X102,tptp0)
& occurrence_of(X102,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f48,plain,
! [X0,X1,X2,X3] :
( min_precedes(X0,X2,X3)
| ~ min_precedes(X1,X2,X3)
| ~ min_precedes(X0,X1,X3) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f49,plain,
! [X0,X2,X3] :
( min_precedes(X0,X2,X3)
| ! [X1] :
( ~ min_precedes(X1,X2,X3)
| ~ min_precedes(X0,X1,X3) ) ),
inference(miniscoping,[status(thm)],[f48]) ).
fof(f50,plain,
! [X0,X1,X2,X3] :
( min_precedes(X0,X3,X2)
| ~ min_precedes(X1,X3,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f60,plain,
! [X15,X16,X17] :
( next_subocc(X15,X16,X17)
<=> ( ! [X18] :
( ~ min_precedes(X18,X16,X17)
| ~ min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f61,plain,
! [X15,X16,X17] :
( ( ? [X18] :
( min_precedes(X18,X16,X17)
& min_precedes(X15,X18,X17) )
| ~ min_precedes(X15,X16,X17)
| next_subocc(X15,X16,X17) )
& ( ( ! [X18] :
( ~ min_precedes(X18,X16,X17)
| ~ min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) )
| ~ next_subocc(X15,X16,X17) ) ),
inference(NNF_transformation,[status(thm)],[f60]) ).
fof(f62,plain,
( ! [X15,X16,X17] :
( ? [X18] :
( min_precedes(X18,X16,X17)
& min_precedes(X15,X18,X17) )
| ~ min_precedes(X15,X16,X17)
| next_subocc(X15,X16,X17) )
& ! [X15,X16,X17] :
( ( ! [X18] :
( ~ min_precedes(X18,X16,X17)
| ~ min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) )
| ~ next_subocc(X15,X16,X17) ) ),
inference(miniscoping,[status(thm)],[f61]) ).
fof(f63,plain,
( ! [X15,X16,X17] :
( ( min_precedes(sK0_skl(X17,X16,X15),X16,X17)
& min_precedes(X15,sK0_skl(X17,X16,X15),X17) )
| ~ min_precedes(X15,X16,X17)
| next_subocc(X15,X16,X17) )
& ! [X15,X16,X17] :
( ( ! [X18] :
( ~ min_precedes(X18,X16,X17)
| ~ min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) )
| ~ next_subocc(X15,X16,X17) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X18,sK0_skl(X17,X16,X15))],[f62]) ).
fof(f64,plain,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f177,plain,
! [X95,X96] :
( ? [X97,X98,X99] :
( leaf(X99,tptp0)
& next_subocc(X98,X99,tptp0)
& ( occurrence_of(X99,tptp1)
| occurrence_of(X99,tptp2) )
& next_subocc(X97,X98,tptp0)
& occurrence_of(X98,tptp4)
& next_subocc(X95,X97,tptp0)
& occurrence_of(X97,tptp3) )
| leaf_occ(X95,X96)
| ~ arboreal(X95)
| ~ subactivity_occurrence(X95,X96)
| ~ occurrence_of(X96,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f178,plain,
! [X95] :
( ? [X99] :
( leaf(X99,tptp0)
& ? [X98] :
( next_subocc(X98,X99,tptp0)
& ( occurrence_of(X99,tptp1)
| occurrence_of(X99,tptp2) )
& ? [X97] :
( next_subocc(X97,X98,tptp0)
& occurrence_of(X98,tptp4)
& next_subocc(X95,X97,tptp0)
& occurrence_of(X97,tptp3) ) ) )
| ! [X96] :
( leaf_occ(X95,X96)
| ~ arboreal(X95)
| ~ subactivity_occurrence(X95,X96)
| ~ occurrence_of(X96,tptp0) ) ),
inference(miniscoping,[status(thm)],[f177]) ).
fof(f179,plain,
! [X95] :
( ( leaf(sK14_skl(X95),tptp0)
& next_subocc(sK15_skl(X95),sK14_skl(X95),tptp0)
& ( occurrence_of(sK14_skl(X95),tptp1)
| occurrence_of(sK14_skl(X95),tptp2) )
& next_subocc(sK16_skl(X95),sK15_skl(X95),tptp0)
& occurrence_of(sK15_skl(X95),tptp4)
& next_subocc(X95,sK16_skl(X95),tptp0)
& occurrence_of(sK16_skl(X95),tptp3) )
| ! [X96] :
( leaf_occ(X95,X96)
| ~ arboreal(X95)
| ~ subactivity_occurrence(X95,X96)
| ~ occurrence_of(X96,tptp0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl]),skolemize(X99,sK14_skl(X95)),skolemize(X98,sK15_skl(X95)),skolemize(X97,sK16_skl(X95))],[f178]) ).
fof(f180,plain,
! [X0,X1] :
( occurrence_of(sK16_skl(X1),tptp3)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f181,plain,
! [X0,X1] :
( next_subocc(X1,sK16_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f183,plain,
! [X0,X1] :
( next_subocc(sK16_skl(X1),sK15_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f184,plain,
! [X0,X1] :
( occurrence_of(sK14_skl(X1),tptp1)
| occurrence_of(sK14_skl(X1),tptp2)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f185,plain,
! [X0,X1] :
( next_subocc(sK15_skl(X1),sK14_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f186,plain,
! [X0,X1] :
( leaf(sK14_skl(X1),tptp0)
| leaf_occ(X1,X0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f199,plain,
? [X100,X101] :
( ! [X102,X103] :
( ~ leaf(X103,tptp0)
| ~ min_precedes(X102,X103,tptp0)
| ( ~ occurrence_of(X103,tptp1)
& ~ occurrence_of(X103,tptp2) )
| ~ next_subocc(X100,X102,tptp0)
| ~ occurrence_of(X102,tptp3) )
& ~ leaf_occ(X100,X101)
& arboreal(X100)
& subactivity_occurrence(X100,X101)
& occurrence_of(X101,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f200,plain,
? [X100] :
( ! [X103] :
( ~ leaf(X103,tptp0)
| ! [X102] :
( ~ min_precedes(X102,X103,tptp0)
| ( ~ occurrence_of(X103,tptp1)
& ~ occurrence_of(X103,tptp2) )
| ~ next_subocc(X100,X102,tptp0)
| ~ occurrence_of(X102,tptp3) ) )
& ? [X101] :
( ~ leaf_occ(X100,X101)
& arboreal(X100)
& subactivity_occurrence(X100,X101)
& occurrence_of(X101,tptp0) ) ),
inference(miniscoping,[status(thm)],[f199]) ).
fof(f201,plain,
( ! [X103] :
( ~ leaf(X103,tptp0)
| ! [X102] :
( ~ min_precedes(X102,X103,tptp0)
| ( ~ occurrence_of(X103,tptp1)
& ~ occurrence_of(X103,tptp2) )
| ~ next_subocc(sK17_skl,X102,tptp0)
| ~ occurrence_of(X102,tptp3) ) )
& ~ leaf_occ(sK17_skl,sK18_skl)
& arboreal(sK17_skl)
& subactivity_occurrence(sK17_skl,sK18_skl)
& occurrence_of(sK18_skl,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl]),skolemize(X100,sK17_skl),skolemize(X101,sK18_skl)],[f200]) ).
fof(f202,plain,
occurrence_of(sK18_skl,tptp0),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f203,plain,
subactivity_occurrence(sK17_skl,sK18_skl),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f204,plain,
arboreal(sK17_skl),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f205,plain,
~ leaf_occ(sK17_skl,sK18_skl),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f206,plain,
! [X0,X1] :
( ~ leaf(X1,tptp0)
| ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp2)
| ~ next_subocc(sK17_skl,X0,tptp0)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f207,plain,
! [X0,X1] :
( ~ leaf(X1,tptp0)
| ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp1)
| ~ next_subocc(sK17_skl,X0,tptp0)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f344,plain,
( occurrence_of(sK16_skl(sK17_skl),tptp3)
| leaf_occ(sK17_skl,sK18_skl)
| ~ arboreal(sK17_skl)
| ~ occurrence_of(sK18_skl,tptp0) ),
inference(resolution,[status(thm)],[f180,f203]) ).
fof(f346,plain,
( occurrence_of(sK16_skl(sK17_skl),tptp3)
| leaf_occ(sK17_skl,sK18_skl)
| ~ arboreal(sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f344,f202]) ).
fof(f348,plain,
( next_subocc(sK17_skl,sK16_skl(sK17_skl),tptp0)
| leaf_occ(sK17_skl,sK18_skl)
| ~ arboreal(sK17_skl)
| ~ occurrence_of(sK18_skl,tptp0) ),
inference(resolution,[status(thm)],[f181,f203]) ).
fof(f350,plain,
( next_subocc(sK17_skl,sK16_skl(sK17_skl),tptp0)
| leaf_occ(sK17_skl,sK18_skl)
| ~ arboreal(sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f348,f202]) ).
fof(f404,plain,
( occurrence_of(sK16_skl(sK17_skl),tptp3)
| leaf_occ(sK17_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f346,f204]) ).
fof(f405,plain,
occurrence_of(sK16_skl(sK17_skl),tptp3),
inference(forward_subsumption_resolution,[status(thm)],[f404,f205]) ).
fof(f468,plain,
( next_subocc(sK17_skl,sK16_skl(sK17_skl),tptp0)
| leaf_occ(sK17_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f350,f204]) ).
fof(f469,plain,
next_subocc(sK17_skl,sK16_skl(sK17_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f468,f205]) ).
fof(f493,plain,
! [X0] :
( ~ leaf(X0,tptp0)
| ~ min_precedes(sK16_skl(sK17_skl),X0,tptp0)
| ~ occurrence_of(X0,tptp1)
| ~ occurrence_of(sK16_skl(sK17_skl),tptp3) ),
inference(resolution,[status(thm)],[f469,f207]) ).
fof(f494,plain,
! [X0] :
( ~ leaf(X0,tptp0)
| ~ min_precedes(sK16_skl(sK17_skl),X0,tptp0)
| ~ occurrence_of(X0,tptp2)
| ~ occurrence_of(sK16_skl(sK17_skl),tptp3) ),
inference(resolution,[status(thm)],[f469,f206]) ).
fof(f499,plain,
! [X0] :
( ~ leaf(X0,tptp0)
| ~ min_precedes(sK16_skl(sK17_skl),X0,tptp0)
| ~ occurrence_of(X0,tptp1) ),
inference(forward_subsumption_resolution,[status(thm)],[f493,f405]) ).
fof(f500,plain,
! [X0] :
( ~ leaf(X0,tptp0)
| ~ min_precedes(sK16_skl(sK17_skl),X0,tptp0)
| ~ occurrence_of(X0,tptp2) ),
inference(forward_subsumption_resolution,[status(thm)],[f494,f405]) ).
fof(f535,plain,
( next_subocc(sK16_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)
| leaf_occ(sK17_skl,sK18_skl)
| ~ arboreal(sK17_skl)
| ~ occurrence_of(sK18_skl,tptp0) ),
inference(resolution,[status(thm)],[f183,f203]) ).
fof(f537,plain,
( next_subocc(sK16_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)
| leaf_occ(sK17_skl,sK18_skl)
| ~ arboreal(sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f535,f202]) ).
fof(f539,plain,
( occurrence_of(sK14_skl(sK17_skl),tptp1)
| occurrence_of(sK14_skl(sK17_skl),tptp2)
| leaf_occ(sK17_skl,sK18_skl)
| ~ arboreal(sK17_skl)
| ~ occurrence_of(sK18_skl,tptp0) ),
inference(resolution,[status(thm)],[f184,f203]) ).
fof(f541,plain,
( occurrence_of(sK14_skl(sK17_skl),tptp1)
| occurrence_of(sK14_skl(sK17_skl),tptp2)
| leaf_occ(sK17_skl,sK18_skl)
| ~ arboreal(sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f539,f202]) ).
fof(f543,plain,
( next_subocc(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0)
| leaf_occ(sK17_skl,sK18_skl)
| ~ arboreal(sK17_skl)
| ~ occurrence_of(sK18_skl,tptp0) ),
inference(resolution,[status(thm)],[f185,f203]) ).
fof(f545,plain,
( next_subocc(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0)
| leaf_occ(sK17_skl,sK18_skl)
| ~ arboreal(sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f543,f202]) ).
fof(f585,plain,
( next_subocc(sK16_skl(sK17_skl),sK15_skl(sK17_skl),tptp0)
| leaf_occ(sK17_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f537,f204]) ).
fof(f586,plain,
next_subocc(sK16_skl(sK17_skl),sK15_skl(sK17_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f585,f205]) ).
fof(f590,plain,
min_precedes(sK16_skl(sK17_skl),sK15_skl(sK17_skl),tptp0),
inference(resolution,[status(thm)],[f586,f64]) ).
fof(f608,plain,
! [X0] :
( min_precedes(sK16_skl(sK17_skl),X0,tptp0)
| ~ min_precedes(sK15_skl(sK17_skl),X0,tptp0) ),
inference(resolution,[status(thm)],[f590,f50]) ).
fof(f622,plain,
( occurrence_of(sK14_skl(sK17_skl),tptp1)
| occurrence_of(sK14_skl(sK17_skl),tptp2)
| leaf_occ(sK17_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f541,f204]) ).
fof(f623,plain,
( occurrence_of(sK14_skl(sK17_skl),tptp1)
| occurrence_of(sK14_skl(sK17_skl),tptp2) ),
inference(forward_subsumption_resolution,[status(thm)],[f622,f205]) ).
fof(f624,plain,
( next_subocc(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0)
| leaf_occ(sK17_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f545,f204]) ).
fof(f625,plain,
next_subocc(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f624,f205]) ).
fof(f635,plain,
min_precedes(sK15_skl(sK17_skl),sK14_skl(sK17_skl),tptp0),
inference(resolution,[status(thm)],[f625,f64]) ).
fof(f669,plain,
( leaf(sK14_skl(sK17_skl),tptp0)
| leaf_occ(sK17_skl,sK18_skl)
| ~ arboreal(sK17_skl)
| ~ occurrence_of(sK18_skl,tptp0) ),
inference(resolution,[status(thm)],[f186,f203]) ).
fof(f671,plain,
( leaf(sK14_skl(sK17_skl),tptp0)
| leaf_occ(sK17_skl,sK18_skl)
| ~ arboreal(sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f669,f202]) ).
fof(f672,plain,
( leaf(sK14_skl(sK17_skl),tptp0)
| leaf_occ(sK17_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f671,f204]) ).
fof(f673,plain,
leaf(sK14_skl(sK17_skl),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f672,f205]) ).
fof(f1528,plain,
min_precedes(sK16_skl(sK17_skl),sK14_skl(sK17_skl),tptp0),
inference(resolution,[status(thm)],[f608,f635]) ).
fof(f1531,plain,
( ~ leaf(sK14_skl(sK17_skl),tptp0)
| ~ occurrence_of(sK14_skl(sK17_skl),tptp2) ),
inference(resolution,[status(thm)],[f1528,f500]) ).
fof(f1532,plain,
( ~ leaf(sK14_skl(sK17_skl),tptp0)
| ~ occurrence_of(sK14_skl(sK17_skl),tptp1) ),
inference(resolution,[status(thm)],[f1528,f499]) ).
fof(f1550,plain,
occurrence_of(sK14_skl(sK17_skl),tptp1),
inference(backward_subsumption_resolution,[status(thm)],[f623,f1559]) ).
fof(f1559,plain,
~ occurrence_of(sK14_skl(sK17_skl),tptp2),
inference(forward_subsumption_resolution,[status(thm)],[f1531,f673]) ).
fof(f1561,plain,
~ occurrence_of(sK14_skl(sK17_skl),tptp1),
inference(forward_subsumption_resolution,[status(thm)],[f1532,f673]) ).
fof(f1562,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1550,f1561]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO014+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n020.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.02/0.35 % WCLimit : 300
% 0.02/0.35 % DateTime : Mon Sep 21 03:43:32 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.37 % Drodi V4.1.1
% 0.02/0.54 % Refutation found
% 0.02/0.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.02/0.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.95/0.57 % Elapsed time: 0.195417 seconds
% 0.95/0.57 % CPU time: 1.251014 seconds
% 0.95/0.57 % Total memory used: 99.056 MB
% 0.95/0.57 % Net memory used: 98.111 MB
%------------------------------------------------------------------------------