%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO012+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 : n006.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.13s 5.42s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 3
% Syntax : Number of formulae : 34 ( 10 unt; 0 def)
% Number of atoms : 112 ( 6 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 125 ( 47 ~; 44 |; 29 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-1 aty)
% Number of variables : 49 ( 38 !; 11 ?)
% 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(f33,axiom,
! [X95] :
( occurrence_of(X95,tptp0)
=> ? [X96,X97,X98] :
( ! [X99] :
( min_precedes(X96,X99,tptp0)
=> ( X99 = X98
| X99 = X97 ) )
& min_precedes(X97,X98,tptp0)
& ( occurrence_of(X98,tptp1)
| occurrence_of(X98,tptp2) )
& min_precedes(X96,X97,tptp0)
& occurrence_of(X97,tptp4)
& root_occ(X96,X95)
& occurrence_of(X96,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,conjecture,
! [X100] :
( occurrence_of(X100,tptp0)
=> ? [X101,X102] :
( min_precedes(X101,X102,tptp0)
& ( occurrence_of(X102,tptp1)
| occurrence_of(X102,tptp2) )
& root_occ(X101,X100)
& occurrence_of(X101,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
~ ! [X100] :
( occurrence_of(X100,tptp0)
=> ? [X101,X102] :
( min_precedes(X101,X102,tptp0)
& ( occurrence_of(X102,tptp1)
| occurrence_of(X102,tptp2) )
& root_occ(X101,X100)
& occurrence_of(X101,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(f177,plain,
! [X95] :
( ? [X96,X97,X98] :
( ! [X99] :
( X99 = X98
| X99 = X97
| ~ min_precedes(X96,X99,tptp0) )
& min_precedes(X97,X98,tptp0)
& ( occurrence_of(X98,tptp1)
| occurrence_of(X98,tptp2) )
& min_precedes(X96,X97,tptp0)
& occurrence_of(X97,tptp4)
& root_occ(X96,X95)
& occurrence_of(X96,tptp3) )
| ~ occurrence_of(X95,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f178,plain,
! [X95] :
( ( ! [X99] :
( X99 = sK16_skl(X95)
| X99 = sK15_skl(X95)
| ~ min_precedes(sK14_skl(X95),X99,tptp0) )
& min_precedes(sK15_skl(X95),sK16_skl(X95),tptp0)
& ( occurrence_of(sK16_skl(X95),tptp1)
| occurrence_of(sK16_skl(X95),tptp2) )
& min_precedes(sK14_skl(X95),sK15_skl(X95),tptp0)
& occurrence_of(sK15_skl(X95),tptp4)
& root_occ(sK14_skl(X95),X95)
& occurrence_of(sK14_skl(X95),tptp3) )
| ~ occurrence_of(X95,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl]),skolemize(X96,sK14_skl(X95)),skolemize(X97,sK15_skl(X95)),skolemize(X98,sK16_skl(X95))],[f177]) ).
fof(f179,plain,
! [X0] :
( occurrence_of(sK14_skl(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f180,plain,
! [X0] :
( root_occ(sK14_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f182,plain,
! [X0] :
( min_precedes(sK14_skl(X0),sK15_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f183,plain,
! [X0] :
( occurrence_of(sK16_skl(X0),tptp1)
| occurrence_of(sK16_skl(X0),tptp2)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f184,plain,
! [X0] :
( min_precedes(sK15_skl(X0),sK16_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f178]) ).
fof(f198,plain,
? [X100] :
( ! [X101,X102] :
( ~ min_precedes(X101,X102,tptp0)
| ( ~ occurrence_of(X102,tptp1)
& ~ occurrence_of(X102,tptp2) )
| ~ root_occ(X101,X100)
| ~ occurrence_of(X101,tptp3) )
& occurrence_of(X100,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f199,plain,
( ! [X101,X102] :
( ~ min_precedes(X101,X102,tptp0)
| ( ~ occurrence_of(X102,tptp1)
& ~ occurrence_of(X102,tptp2) )
| ~ root_occ(X101,sK17_skl)
| ~ occurrence_of(X101,tptp3) )
& occurrence_of(sK17_skl,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(X100,sK17_skl)],[f198]) ).
fof(f200,plain,
occurrence_of(sK17_skl,tptp0),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f201,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp2)
| ~ root_occ(X0,sK17_skl)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f202,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| ~ occurrence_of(X1,tptp1)
| ~ root_occ(X0,sK17_skl)
| ~ occurrence_of(X0,tptp3) ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f234,plain,
root_occ(sK14_skl(sK17_skl),sK17_skl),
inference(resolution,[status(thm)],[f180,f200]) ).
fof(f245,plain,
occurrence_of(sK14_skl(sK17_skl),tptp3),
inference(resolution,[status(thm)],[f179,f200]) ).
fof(f429,plain,
min_precedes(sK14_skl(sK17_skl),sK15_skl(sK17_skl),tptp0),
inference(resolution,[status(thm)],[f182,f200]) ).
fof(f430,plain,
( occurrence_of(sK16_skl(sK17_skl),tptp1)
| occurrence_of(sK16_skl(sK17_skl),tptp2) ),
inference(resolution,[status(thm)],[f183,f200]) ).
fof(f448,plain,
! [X0] :
( min_precedes(sK14_skl(sK17_skl),X0,tptp0)
| ~ min_precedes(sK15_skl(sK17_skl),X0,tptp0) ),
inference(resolution,[status(thm)],[f429,f50]) ).
fof(f574,plain,
min_precedes(sK15_skl(sK17_skl),sK16_skl(sK17_skl),tptp0),
inference(resolution,[status(thm)],[f184,f200]) ).
fof(f872,plain,
min_precedes(sK14_skl(sK17_skl),sK16_skl(sK17_skl),tptp0),
inference(resolution,[status(thm)],[f448,f574]) ).
fof(f876,plain,
( ~ occurrence_of(sK16_skl(sK17_skl),tptp1)
| ~ root_occ(sK14_skl(sK17_skl),sK17_skl)
| ~ occurrence_of(sK14_skl(sK17_skl),tptp3) ),
inference(resolution,[status(thm)],[f872,f202]) ).
fof(f877,plain,
( ~ occurrence_of(sK16_skl(sK17_skl),tptp2)
| ~ root_occ(sK14_skl(sK17_skl),sK17_skl)
| ~ occurrence_of(sK14_skl(sK17_skl),tptp3) ),
inference(resolution,[status(thm)],[f872,f201]) ).
fof(f892,plain,
( ~ occurrence_of(sK16_skl(sK17_skl),tptp1)
| ~ root_occ(sK14_skl(sK17_skl),sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f876,f245]) ).
fof(f893,plain,
( ~ occurrence_of(sK16_skl(sK17_skl),tptp2)
| ~ root_occ(sK14_skl(sK17_skl),sK17_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f877,f245]) ).
fof(f916,plain,
occurrence_of(sK16_skl(sK17_skl),tptp2),
inference(backward_subsumption_resolution,[status(thm)],[f430,f919]) ).
fof(f919,plain,
~ occurrence_of(sK16_skl(sK17_skl),tptp1),
inference(forward_subsumption_resolution,[status(thm)],[f892,f234]) ).
fof(f999,plain,
~ occurrence_of(sK16_skl(sK17_skl),tptp2),
inference(forward_subsumption_resolution,[status(thm)],[f893,f234]) ).
fof(f1000,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f916,f999]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO012+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n006.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 03:42:17 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 0.13/5.42 % Refutation found
% 0.13/5.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/5.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/5.45 % Elapsed time: 0.069392 seconds
% 0.13/5.45 % CPU time: 0.208257 seconds
% 0.13/5.45 % Total memory used: 84.207 MB
% 0.13/5.45 % Net memory used: 84.069 MB
%------------------------------------------------------------------------------