%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG116+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 : n013.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:23 PM UTC 2026
% Result : Theorem 0.32s 0.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : RNG116+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.42 % Computer : n013.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Mon Sep 21 04:20:36 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.45 % Drodi V4.1.1
% 0.32/0.93 % Refutation found
% 0.32/0.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.32/0.93 % SZS output start CNFRefutation for theBenchmark
% 0.32/0.93 fof(f47,hypothesis,(
% 0.32/0.93 ( (? [W0] :( aElement0(W0)& sdtasdt0(xa,W0) = xk ))& aElementOf0(xk,slsdtgt0(xa))& (? [W0] :( aElement0(W0)& sdtasdt0(xb,W0) = xl ))& aElementOf0(xl,slsdtgt0(xb))& xu = sdtpldt0(xk,xl) ) ),
% 0.32/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.32/0.93 fof(f48,conjecture,(
% 0.32/0.93 (? [W0,W1] :( aElement0(W0)& aElement0(W1)& xu = sdtpldt0(sdtasdt0(xa,W0),sdtasdt0(xb,W1)) ) )),
% 0.32/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.32/0.93 fof(f49,negated_conjecture,(
% 0.32/0.93 ~((? [W0,W1] :( aElement0(W0)& aElement0(W1)& xu = sdtpldt0(sdtasdt0(xa,W0),sdtasdt0(xb,W1)) ) ))),
% 0.32/0.93 inference(negated_conjecture,[status(cth)],[f48])).
% 0.32/0.93 fof(f284,plain,(
% 0.32/0.93 ((((aElement0(sK38_skl)&sdtasdt0(xa,sK38_skl)=xk)&aElementOf0(xk,slsdtgt0(xa)))&(aElement0(sK39_skl)&sdtasdt0(xb,sK39_skl)=xl))&aElementOf0(xl,slsdtgt0(xb)))&xu=sdtpldt0(xk,xl)),
% 0.32/0.93 inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl,sK39_skl]),skolemize(W0,sK38_skl),skolemize(W0,sK39_skl)],[f47])).
% 0.32/0.93 fof(f285,plain,(
% 0.32/0.93 aElement0(sK38_skl)),
% 0.32/0.93 inference(cnf_transformation,[status(thm)],[f284])).
% 0.32/0.93 fof(f286,plain,(
% 0.32/0.93 sdtasdt0(xa,sK38_skl)=xk),
% 0.32/0.93 inference(cnf_transformation,[status(thm)],[f284])).
% 0.32/0.93 fof(f288,plain,(
% 0.32/0.93 aElement0(sK39_skl)),
% 0.32/0.93 inference(cnf_transformation,[status(thm)],[f284])).
% 0.32/0.93 fof(f289,plain,(
% 0.32/0.93 sdtasdt0(xb,sK39_skl)=xl),
% 0.32/0.93 inference(cnf_transformation,[status(thm)],[f284])).
% 0.32/0.93 fof(f291,plain,(
% 0.32/0.93 xu=sdtpldt0(xk,xl)),
% 0.32/0.93 inference(cnf_transformation,[status(thm)],[f284])).
% 0.32/0.93 fof(f292,plain,(
% 0.32/0.93 (![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|~xu=sdtpldt0(sdtasdt0(xa,W0),sdtasdt0(xb,W1))))),
% 0.32/0.93 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.32/0.93 fof(f293,plain,(
% 0.32/0.93 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|~xu=sdtpldt0(sdtasdt0(xa,X0),sdtasdt0(xb,X1)))),
% 0.32/0.93 inference(cnf_transformation,[status(thm)],[f292])).
% 0.32/0.93 fof(f823,plain,(
% 0.32/0.93 ![X0]: (~aElement0(sK38_skl)|~aElement0(X0)|~xu=sdtpldt0(xk,sdtasdt0(xb,X0)))),
% 0.32/0.93 inference(paramodulation,[status(thm)],[f286,f293])).
% 0.32/0.93 fof(f824,definition,(
% 0.32/0.93 sQ23_spl <=> (aElement0(sK38_skl))),
% 0.32/0.93 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.32/0.93 fof(f826,plain,(
% 0.32/0.93 ~aElement0(sK38_skl)|sQ23_spl),
% 0.32/0.93 inference(component_clause,[status(thm)],[f824])).
% 0.32/0.93 fof(f827,definition,(
% 0.32/0.93 ![X0]: (sQ24_spl <=> (~aElement0(X0)|~xu=sdtpldt0(xk,sdtasdt0(xb,X0))))),
% 0.32/0.93 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.32/0.93 fof(f828,plain,(
% 0.32/0.93 ![X0]: (~aElement0(X0)|~xu=sdtpldt0(xk,sdtasdt0(xb,X0))|~sQ24_spl)),
% 0.32/0.93 inference(component_clause,[status(thm)],[f827])).
% 0.32/0.93 fof(f830,plain,(
% 0.32/0.93 ~sQ23_spl|sQ24_spl),
% 0.32/0.93 inference(split_clause,[status(thm)],[f823,f824,f827])).
% 0.32/0.93 fof(f831,plain,(
% 0.32/0.93 $false|sQ23_spl),
% 0.32/0.93 inference(forward_subsumption_resolution,[status(thm)],[f826,f285])).
% 0.32/0.93 fof(f832,plain,(
% 0.32/0.93 sQ23_spl),
% 0.32/0.93 inference(contradiction_clause,[status(thm)],[f831])).
% 0.32/0.93 fof(f869,definition,(
% 0.32/0.93 sQ25_spl <=> (aElement0(sK39_skl))),
% 0.32/0.93 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.32/0.93 fof(f871,plain,(
% 0.32/0.93 ~aElement0(sK39_skl)|sQ25_spl),
% 0.32/0.93 inference(component_clause,[status(thm)],[f869])).
% 0.32/0.93 fof(f884,plain,(
% 0.32/0.93 $false|sQ25_spl),
% 0.32/0.93 inference(forward_subsumption_resolution,[status(thm)],[f871,f288])).
% 0.32/0.93 fof(f885,plain,(
% 0.32/0.93 sQ25_spl),
% 0.32/0.93 inference(contradiction_clause,[status(thm)],[f884])).
% 0.32/0.93 fof(f1113,plain,(
% 0.32/0.93 ~aElement0(sK39_skl)|~xu=sdtpldt0(xk,xl)|~sQ24_spl),
% 0.32/0.93 inference(paramodulation,[status(thm)],[f289,f828])).
% 0.32/0.93 fof(f1117,definition,(
% 0.32/0.93 sQ32_spl <=> (xu=sdtpldt0(xk,xl))),
% 0.32/0.93 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.32/0.93 fof(f1119,plain,(
% 0.32/0.93 ~xu=sdtpldt0(xk,xl)|sQ32_spl),
% 0.32/0.93 inference(component_clause,[status(thm)],[f1117])).
% 0.32/0.93 fof(f1120,plain,(
% 0.32/0.93 ~sQ25_spl|~sQ32_spl|~sQ24_spl),
% 0.32/0.93 inference(split_clause,[status(thm)],[f1113,f869,f1117,f827])).
% 0.32/0.93 fof(f1123,plain,(
% 0.32/0.93 ~xu=xu|sQ32_spl),
% 0.32/0.93 inference(forward_demodulation,[status(thm)],[f291,f1119])).
% 0.32/0.93 fof(f1124,plain,(
% 0.32/0.93 $false|sQ32_spl),
% 0.32/0.93 inference(trivial_equality_resolution,[status(thm)],[f1123])).
% 0.32/0.94 fof(f1125,plain,(
% 0.32/0.94 sQ32_spl),
% 0.32/0.94 inference(contradiction_clause,[status(thm)],[f1124])).
% 0.32/0.94 fof(f1126,plain,(
% 0.32/0.94 $false),
% 0.32/0.94 inference(sat_refutation,[status(thm)],[f830,f832,f885,f1120,f1125])).
% 0.32/0.94 % SZS output end CNFRefutation for theBenchmark.p
% 0.65/0.97 % Elapsed time: 0.526499 seconds
% 0.65/0.97 % CPU time: 3.742743 seconds
% 0.65/0.97 % Total memory used: 147.216 MB
% 0.65/0.97 % Net memory used: 143.615 MB
%------------------------------------------------------------------------------