%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG125+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 : n017.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 02:05:04 PM UTC 2026
% Result : Theorem 0.20s 0.52s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 7
% Syntax : Number of formulae : 26 ( 5 unt; 4 def)
% Number of atoms : 85 ( 14 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 98 ( 39 ~; 28 |; 27 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 5 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 11 ( 6 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f46,hypothesis,
~ ( ( aDivisorOf0(xu,xb)
| doDivides0(xu,xb)
| ? [W0] :
( sdtasdt0(xu,W0) = xb
& aElement0(W0) ) )
& ( aDivisorOf0(xu,xa)
| doDivides0(xu,xa)
| ? [W0] :
( sdtasdt0(xu,W0) = xa
& aElement0(W0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,hypothesis,
~ ~ ( doDivides0(xu,xa)
& ? [W0] :
( sdtasdt0(xu,W0) = xa
& aElement0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
~ ~ ( doDivides0(xu,xb)
& ? [W0] :
( sdtasdt0(xu,W0) = xb
& aElement0(W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f280,plain,
( ( ~ aDivisorOf0(xu,xb)
& ~ doDivides0(xu,xb)
& ! [W0] :
( sdtasdt0(xu,W0) != xb
| ~ aElement0(W0) ) )
| ( ~ aDivisorOf0(xu,xa)
& ~ doDivides0(xu,xa)
& ! [W0] :
( sdtasdt0(xu,W0) != xa
| ~ aElement0(W0) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f281,definition,
( sP4_prd
<=> ( ~ aDivisorOf0(xu,xa)
& ~ doDivides0(xu,xa)
& ! [W0] :
( sdtasdt0(xu,W0) != xa
| ~ aElement0(W0) ) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f282,plain,
( ( ~ aDivisorOf0(xu,xb)
& ~ doDivides0(xu,xb)
& ! [W0] :
( sdtasdt0(xu,W0) != xb
| ~ aElement0(W0) ) )
| sP4_prd ),
inference(formula_renaming,[status(thm)],[f280,f281]) ).
fof(f284,plain,
( ~ doDivides0(xu,xb)
| sP4_prd ),
inference(cnf_transformation,[status(thm)],[f282]) ).
fof(f290,plain,
( doDivides0(xu,xa)
& sdtasdt0(xu,sK40_skl) = xa
& aElement0(sK40_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40_skl]),skolemize(W0,sK40_skl)],[f48]) ).
fof(f293,plain,
doDivides0(xu,xa),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f294,plain,
( doDivides0(xu,xb)
& sdtasdt0(xu,sK41_skl) = xb
& aElement0(sK41_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl]),skolemize(W0,sK41_skl)],[f49]) ).
fof(f297,plain,
doDivides0(xu,xb),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f326,plain,
( ( aDivisorOf0(xu,xa)
| doDivides0(xu,xa)
| ? [W0] :
( sdtasdt0(xu,W0) = xa
& aElement0(W0) )
| sP4_prd )
& ( ( ~ aDivisorOf0(xu,xa)
& ~ doDivides0(xu,xa)
& ! [W0] :
( sdtasdt0(xu,W0) != xa
| ~ aElement0(W0) ) )
| ~ sP4_prd ) ),
inference(NNF_transformation,[status(thm)],[f281]) ).
fof(f327,plain,
( ( aDivisorOf0(xu,xa)
| doDivides0(xu,xa)
| ( sdtasdt0(xu,sK43_skl) = xa
& aElement0(sK43_skl) )
| sP4_prd )
& ( ( ~ aDivisorOf0(xu,xa)
& ~ doDivides0(xu,xa)
& ! [W0] :
( sdtasdt0(xu,W0) != xa
| ~ aElement0(W0) ) )
| ~ sP4_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43_skl]),skolemize(W0,sK43_skl)],[f326]) ).
fof(f329,plain,
( ~ doDivides0(xu,xa)
| ~ sP4_prd ),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f349,definition,
( sQ2_spl
<=> sP4_prd ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f356,definition,
( sQ4_spl
<=> doDivides0(xu,xb) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f358,plain,
( sQ4_spl
| ~ doDivides0(xu,xb) ),
inference(component_clause,[status(thm)],[f356]) ).
fof(f359,plain,
( ~ sQ4_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f284,f349,f356]) ).
fof(f368,definition,
( sQ7_spl
<=> doDivides0(xu,xa) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f370,plain,
( sQ7_spl
| ~ doDivides0(xu,xa) ),
inference(component_clause,[status(thm)],[f368]) ).
fof(f371,plain,
( ~ sQ7_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f329,f349,f368]) ).
fof(f441,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f358,f297]) ).
fof(f442,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f441]) ).
fof(f443,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f370,f293]) ).
fof(f444,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f443]) ).
fof(f445,plain,
$false,
inference(sat_refutation,[status(thm)],[f359,f371,f442,f444]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG125+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n017.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Mon Sep 21 04:16:56 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.48 % Drodi V4.1.1
% 0.20/0.52 % Refutation found
% 0.20/0.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/0.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.23/0.57 % Elapsed time: 0.100909 seconds
% 0.23/0.57 % CPU time: 0.123631 seconds
% 0.23/0.57 % Total memory used: 10.377 MB
% 0.23/0.57 % Net memory used: 10.347 MB
%------------------------------------------------------------------------------