%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG125+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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 02:05:25 PM UTC 2026
% Result : Theorem 0.14s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG125+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.53 % Computer : n015.cluster.edu
% 0.10/0.53 % Model : x86_64 x86_64
% 0.10/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.53 % Memory : 8046.5625MB
% 0.10/0.53 % OS : Linux 6.8.0-71-generic
% 0.10/0.53 % CPULimit : 300
% 0.10/0.53 % WCLimit : 300
% 0.10/0.53 % DateTime : Mon Sep 21 04:24:51 UTC 2026
% 0.10/0.53 % CPUTime :
% 0.10/0.55 % Drodi V4.1.1
% 0.14/0.58 % Refutation found
% 0.14/0.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.58 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.58 fof(f46,hypothesis,(
% 0.14/0.58 ~ ( ( (? [W0] :( aElement0(W0)& sdtasdt0(xu,W0) = xa ))| doDivides0(xu,xa)| aDivisorOf0(xu,xa) )& ( (? [W0] :( aElement0(W0)& sdtasdt0(xu,W0) = xb ))| doDivides0(xu,xb)| aDivisorOf0(xu,xb) ) ) ),
% 0.14/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.58 fof(f48,hypothesis,(
% 0.14/0.58 ~ ~ ( (? [W0] :( aElement0(W0)& sdtasdt0(xu,W0) = xa ))& doDivides0(xu,xa) ) ),
% 0.14/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.58 fof(f49,hypothesis,(
% 0.14/0.58 ~ ~ ( (? [W0] :( aElement0(W0)& sdtasdt0(xu,W0) = xb ))& doDivides0(xu,xb) ) ),
% 0.14/0.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.58 fof(f280,plain,(
% 0.14/0.58 ((((![W0]: (~aElement0(W0)|~sdtasdt0(xu,W0)=xa))&~doDivides0(xu,xa))&~aDivisorOf0(xu,xa))|(((![W0]: (~aElement0(W0)|~sdtasdt0(xu,W0)=xb))&~doDivides0(xu,xb))&~aDivisorOf0(xu,xb)))),
% 0.14/0.58 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 0.14/0.58 fof(f281,definition,(
% 0.14/0.58 sP4_prd<=>(((![W0]: (~aElement0(W0)|~sdtasdt0(xu,W0)=xa))&~doDivides0(xu,xa))&~aDivisorOf0(xu,xa))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.14/0.58 fof(f282,plain,(
% 0.14/0.58 sP4_prd|(((![W0]: (~aElement0(W0)|~sdtasdt0(xu,W0)=xb))&~doDivides0(xu,xb))&~aDivisorOf0(xu,xb))),
% 0.14/0.58 inference(formula_renaming,[status(thm)],[f280,f281])).
% 0.14/0.58 fof(f284,plain,(
% 0.14/0.58 sP4_prd|~doDivides0(xu,xb)),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f282])).
% 0.14/0.58 fof(f290,plain,(
% 0.14/0.58 (aElement0(sK40_skl)&sdtasdt0(xu,sK40_skl)=xa)&doDivides0(xu,xa)),
% 0.14/0.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK40_skl]),skolemize(W0,sK40_skl)],[f48])).
% 0.14/0.58 fof(f293,plain,(
% 0.14/0.58 doDivides0(xu,xa)),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f290])).
% 0.14/0.58 fof(f294,plain,(
% 0.14/0.58 (aElement0(sK41_skl)&sdtasdt0(xu,sK41_skl)=xb)&doDivides0(xu,xb)),
% 0.14/0.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl]),skolemize(W0,sK41_skl)],[f49])).
% 0.14/0.58 fof(f297,plain,(
% 0.14/0.58 doDivides0(xu,xb)),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f294])).
% 0.14/0.58 fof(f326,plain,(
% 0.14/0.58 (~sP4_prd|(((![W0]: (~aElement0(W0)|~sdtasdt0(xu,W0)=xa))&~doDivides0(xu,xa))&~aDivisorOf0(xu,xa)))&(sP4_prd|(((?[W0]: (aElement0(W0)&sdtasdt0(xu,W0)=xa))|doDivides0(xu,xa))|aDivisorOf0(xu,xa)))),
% 0.14/0.58 inference(NNF_transformation,[status(thm)],[f281])).
% 0.14/0.58 fof(f327,plain,(
% 0.14/0.58 (~sP4_prd|(((![W0]: (~aElement0(W0)|~sdtasdt0(xu,W0)=xa))&~doDivides0(xu,xa))&~aDivisorOf0(xu,xa)))&(sP4_prd|(((aElement0(sK43_skl)&sdtasdt0(xu,sK43_skl)=xa)|doDivides0(xu,xa))|aDivisorOf0(xu,xa)))),
% 0.14/0.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK43_skl]),skolemize(W0,sK43_skl)],[f326])).
% 0.14/0.58 fof(f329,plain,(
% 0.14/0.58 ~sP4_prd|~doDivides0(xu,xa)),
% 0.14/0.58 inference(cnf_transformation,[status(thm)],[f327])).
% 0.14/0.58 fof(f349,definition,(
% 0.14/0.58 sQ2_spl <=> (sP4_prd)),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f356,definition,(
% 0.14/0.58 sQ4_spl <=> (doDivides0(xu,xb))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f358,plain,(
% 0.14/0.58 ~doDivides0(xu,xb)|sQ4_spl),
% 0.14/0.58 inference(component_clause,[status(thm)],[f356])).
% 0.14/0.58 fof(f359,plain,(
% 0.14/0.58 sQ2_spl|~sQ4_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f284,f349,f356])).
% 0.14/0.58 fof(f368,definition,(
% 0.14/0.58 sQ7_spl <=> (doDivides0(xu,xa))),
% 0.14/0.58 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.58 fof(f370,plain,(
% 0.14/0.58 ~doDivides0(xu,xa)|sQ7_spl),
% 0.14/0.58 inference(component_clause,[status(thm)],[f368])).
% 0.14/0.58 fof(f371,plain,(
% 0.14/0.58 ~sQ2_spl|~sQ7_spl),
% 0.14/0.58 inference(split_clause,[status(thm)],[f329,f349,f368])).
% 0.14/0.58 fof(f560,plain,(
% 0.14/0.58 $false|sQ4_spl),
% 0.14/0.58 inference(forward_subsumption_resolution,[status(thm)],[f358,f297])).
% 0.14/0.58 fof(f561,plain,(
% 0.14/0.58 sQ4_spl),
% 0.14/0.58 inference(contradiction_clause,[status(thm)],[f560])).
% 0.14/0.58 fof(f562,plain,(
% 0.14/0.58 $false|sQ7_spl),
% 0.14/0.58 inference(forward_subsumption_resolution,[status(thm)],[f370,f293])).
% 0.14/0.58 fof(f563,plain,(
% 0.14/0.58 sQ7_spl),
% 0.14/0.58 inference(contradiction_clause,[status(thm)],[f562])).
% 0.14/0.58 fof(f564,plain,(
% 0.14/0.58 $false),
% 0.14/0.58 inference(sat_refutation,[status(thm)],[f359,f371,f561,f563])).
% 0.14/0.58 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.60 % Elapsed time: 0.055847 seconds
% 0.14/0.60 % CPU time: 0.177624 seconds
% 0.14/0.60 % Total memory used: 89.386 MB
% 0.14/0.60 % Net memory used: 89.178 MB
%------------------------------------------------------------------------------