%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG104+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 : n002.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:04:59 PM UTC 2026
% Result : Theorem 75.49s 9.96s
% Output : CNFRefutation 75.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 21
% Syntax : Number of formulae : 99 ( 32 unt; 11 def)
% Number of atoms : 195 ( 50 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 161 ( 65 ~; 64 |; 18 &)
% ( 11 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 12 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 37 ( 35 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
aElement0(sz10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> aElement0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0,W1,W2] :
( ( aElement0(W2)
& aElement0(W1)
& aElement0(W0) )
=> sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
sz10 != sz00,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
aElement0(xc),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
( aElement0(xz)
& aElementOf0(xy,slsdtgt0(xc))
& ? [W0] :
( sdtasdt0(xc,W0) = xy
& aElement0(W0) )
& aElementOf0(xx,slsdtgt0(xc))
& ? [W0] :
( sdtasdt0(xc,W0) = xx
& aElement0(W0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
( sdtasdt0(xc,xu) = xx
& aElement0(xu) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
( sdtasdt0(xc,xv) = xy
& aElement0(xv) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,conjecture,
sdtasdt0(xz,xx) = sdtasdt0(xc,sdtasdt0(xu,xz)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,negated_conjecture,
sdtasdt0(xz,xx) != sdtasdt0(xc,sdtasdt0(xu,xz)),
inference(negated_conjecture,[status(cth)],[f43]) ).
fof(f49,plain,
aElement0(sz10),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f54,plain,
! [W0,W1] :
( aElement0(sdtasdt0(W0,W1))
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f55,plain,
! [X0,X1] :
( aElement0(sdtasdt0(X0,X1))
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f66,plain,
! [W0,W1] :
( sdtasdt0(W0,W1) = sdtasdt0(W1,W0)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f67,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f68,plain,
! [W0,W1,W2] :
( sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2))
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ aElement0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f69,plain,
! [X0,X1,X2] :
( sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f84,plain,
sz10 != sz00,
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f195,plain,
aElement0(xc),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f196,plain,
( aElement0(xz)
& aElementOf0(xy,slsdtgt0(xc))
& sdtasdt0(xc,sK21_skl) = xy
& aElement0(sK21_skl)
& aElementOf0(xx,slsdtgt0(xc))
& sdtasdt0(xc,sK20_skl) = xx
& aElement0(sK20_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl]),skolemize(W0,sK20_skl),skolemize(W0,sK21_skl)],[f39]) ).
fof(f197,plain,
aElement0(sK20_skl),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f198,plain,
sdtasdt0(xc,sK20_skl) = xx,
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f200,plain,
aElement0(sK21_skl),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f203,plain,
aElement0(xz),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f204,plain,
aElement0(xu),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f205,plain,
sdtasdt0(xc,xu) = xx,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f206,plain,
aElement0(xv),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f209,plain,
sdtasdt0(xz,xx) != sdtasdt0(xc,sdtasdt0(xu,xz)),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f243,plain,
! [X0,X1] :
( sdtasdt0(sdtasdt0(X0,xc),X1) = sdtasdt0(X0,sdtasdt0(xc,X1))
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f195,f69]) ).
fof(f245,plain,
! [X0] :
( sdtasdt0(X0,xc) = sdtasdt0(xc,X0)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f195,f67]) ).
fof(f247,plain,
! [X0,X1] :
( sdtasdt0(sdtasdt0(X0,X1),xz) = sdtasdt0(X0,sdtasdt0(X1,xz))
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f203,f69]) ).
fof(f249,plain,
! [X0,X1] :
( sdtasdt0(sdtasdt0(X0,xz),X1) = sdtasdt0(X0,sdtasdt0(xz,X1))
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f203,f69]) ).
fof(f251,plain,
! [X0] :
( sdtasdt0(X0,xz) = sdtasdt0(xz,X0)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f203,f67]) ).
fof(f256,plain,
! [X0] :
( aElement0(sdtasdt0(X0,xu))
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f204,f55]) ).
fof(f309,plain,
sdtasdt0(xz,xc) = sdtasdt0(xc,xz),
inference(resolution,[status(thm)],[f245,f203]) ).
fof(f314,plain,
! [X0] :
( sdtasdt0(sdtasdt0(X0,xu),xz) = sdtasdt0(X0,sdtasdt0(xu,xz))
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f247,f204]) ).
fof(f329,plain,
! [X0] :
( sdtasdt0(sdtasdt0(X0,sK20_skl),xz) = sdtasdt0(X0,sdtasdt0(sK20_skl,xz))
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f197,f247]) ).
fof(f331,plain,
! [X0] :
( sdtasdt0(sdtasdt0(X0,xc),sK20_skl) = sdtasdt0(X0,sdtasdt0(xc,sK20_skl))
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f197,f243]) ).
fof(f411,plain,
! [X0] :
( sdtasdt0(sdtasdt0(X0,xz),sK20_skl) = sdtasdt0(X0,sdtasdt0(xz,sK20_skl))
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[f249,f197]) ).
fof(f418,plain,
sdtasdt0(sK20_skl,xz) = sdtasdt0(xz,sK20_skl),
inference(resolution,[status(thm)],[f251,f197]) ).
fof(f421,plain,
sdtasdt0(xu,xz) = sdtasdt0(xz,xu),
inference(resolution,[status(thm)],[f251,f204]) ).
fof(f432,definition,
( sQ0_spl
<=> aElement0(xc) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f434,plain,
( sQ0_spl
| ~ aElement0(xc) ),
inference(component_clause,[status(thm)],[f432]) ).
fof(f439,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f434,f195]) ).
fof(f440,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f439]) ).
fof(f462,plain,
aElement0(sdtasdt0(xc,xu)),
inference(resolution,[status(thm)],[f256,f195]) ).
fof(f463,plain,
aElement0(xx),
inference(forward_demodulation,[status(thm)],[f205,f462]) ).
fof(f648,definition,
( sQ12_spl
<=> sz10 = sz00 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f649,plain,
( ~ sQ12_spl
| sz10 = sz00 ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f714,definition,
( sQ25_spl
<=> aElement0(xz) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f716,plain,
( sQ25_spl
| ~ aElement0(xz) ),
inference(component_clause,[status(thm)],[f714]) ).
fof(f729,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f716,f203]) ).
fof(f730,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f729]) ).
fof(f747,plain,
( sdtasdt0(xx,xz) = sdtasdt0(xc,sdtasdt0(xu,xz))
| ~ aElement0(xc) ),
inference(paramodulation,[status(thm)],[f205,f314]) ).
fof(f748,definition,
( sQ29_spl
<=> sdtasdt0(xx,xz) = sdtasdt0(xc,sdtasdt0(xu,xz)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f749,plain,
( ~ sQ29_spl
| sdtasdt0(xx,xz) = sdtasdt0(xc,sdtasdt0(xu,xz)) ),
inference(component_clause,[status(thm)],[f748]) ).
fof(f751,plain,
( sQ29_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f747,f432,f748]) ).
fof(f753,plain,
( sdtasdt0(xx,xz) = sdtasdt0(xc,sdtasdt0(sK20_skl,xz))
| ~ aElement0(xc) ),
inference(paramodulation,[status(thm)],[f198,f329]) ).
fof(f754,definition,
( sQ30_spl
<=> aElement0(sz10) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f756,plain,
( sQ30_spl
| ~ aElement0(sz10) ),
inference(component_clause,[status(thm)],[f754]) ).
fof(f761,definition,
( sQ32_spl
<=> sdtasdt0(xx,xz) = sdtasdt0(xc,sdtasdt0(sK20_skl,xz)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f762,plain,
( ~ sQ32_spl
| sdtasdt0(xx,xz) = sdtasdt0(xc,sdtasdt0(sK20_skl,xz)) ),
inference(component_clause,[status(thm)],[f761]) ).
fof(f764,plain,
( sQ32_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f753,f432,f761]) ).
fof(f765,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f756,f49]) ).
fof(f766,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f765]) ).
fof(f769,definition,
( sQ33_spl
<=> aElement0(sK20_skl) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f771,plain,
( sQ33_spl
| ~ aElement0(sK20_skl) ),
inference(component_clause,[status(thm)],[f769]) ).
fof(f776,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f771,f197]) ).
fof(f777,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f776]) ).
fof(f778,plain,
! [X0] :
( sdtasdt0(sdtasdt0(X0,xc),sK20_skl) = sdtasdt0(X0,xx)
| ~ aElement0(X0) ),
inference(forward_demodulation,[status(thm)],[f198,f331]) ).
fof(f780,plain,
( sdtasdt0(sdtasdt0(xc,xz),sK20_skl) = sdtasdt0(xz,xx)
| ~ aElement0(xz) ),
inference(paramodulation,[status(thm)],[f309,f778]) ).
fof(f786,definition,
( sQ36_spl
<=> sdtasdt0(sdtasdt0(xc,xz),sK20_skl) = sdtasdt0(xz,xx) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f787,plain,
( ~ sQ36_spl
| sdtasdt0(sdtasdt0(xc,xz),sK20_skl) = sdtasdt0(xz,xx) ),
inference(component_clause,[status(thm)],[f786]) ).
fof(f789,plain,
( sQ36_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f780,f714,f786]) ).
fof(f882,definition,
( sQ44_spl
<=> aElement0(sK21_skl) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f884,plain,
( sQ44_spl
| ~ aElement0(sK21_skl) ),
inference(component_clause,[status(thm)],[f882]) ).
fof(f893,plain,
( sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f884,f200]) ).
fof(f894,plain,
sQ44_spl,
inference(contradiction_clause,[status(thm)],[f893]) ).
fof(f1018,plain,
sdtasdt0(sdtasdt0(xc,xz),sK20_skl) = sdtasdt0(xc,sdtasdt0(xz,sK20_skl)),
inference(resolution,[status(thm)],[f411,f195]) ).
fof(f1039,plain,
sdtasdt0(xz,xx) != sdtasdt0(xc,sdtasdt0(xz,xu)),
inference(backward_demodulation,[status(thm)],[f421,f209]) ).
fof(f1483,definition,
( sQ75_spl
<=> aElement0(xx) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1485,plain,
( sQ75_spl
| ~ aElement0(xx) ),
inference(component_clause,[status(thm)],[f1483]) ).
fof(f1502,plain,
( sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1485,f463]) ).
fof(f1503,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f1502]) ).
fof(f1564,plain,
( ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f649,f84]) ).
fof(f1565,plain,
~ sQ12_spl,
inference(contradiction_clause,[status(thm)],[f1564]) ).
fof(f1698,plain,
( ~ sQ29_spl
| sdtasdt0(xz,xx) != sdtasdt0(xx,xz) ),
inference(backward_demodulation,[status(thm)],[f1699,f1039]) ).
fof(f1699,plain,
( ~ sQ29_spl
| sdtasdt0(xx,xz) = sdtasdt0(xc,sdtasdt0(xz,xu)) ),
inference(forward_demodulation,[status(thm)],[f421,f749]) ).
fof(f1714,plain,
( ~ sQ32_spl
| sdtasdt0(xx,xz) = sdtasdt0(xc,sdtasdt0(xz,sK20_skl)) ),
inference(forward_demodulation,[status(thm)],[f418,f762]) ).
fof(f1730,definition,
( sQ111_spl
<=> aElement0(xv) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1732,plain,
( sQ111_spl
| ~ aElement0(xv) ),
inference(component_clause,[status(thm)],[f1730]) ).
fof(f1741,plain,
( sQ111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1732,f206]) ).
fof(f1742,plain,
sQ111_spl,
inference(contradiction_clause,[status(thm)],[f1741]) ).
fof(f2438,plain,
( ~ sQ36_spl
| sdtasdt0(xz,xx) = sdtasdt0(xc,sdtasdt0(xz,sK20_skl)) ),
inference(forward_demodulation,[status(thm)],[f787,f1018]) ).
fof(f2439,plain,
( ~ sQ36_spl
| ~ sQ32_spl
| sdtasdt0(xz,xx) = sdtasdt0(xx,xz) ),
inference(forward_demodulation,[status(thm)],[f1714,f2438]) ).
fof(f2440,plain,
( ~ sQ36_spl
| ~ sQ32_spl
| ~ sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2439,f1698]) ).
fof(f2441,plain,
( ~ sQ36_spl
| ~ sQ32_spl
| ~ sQ29_spl ),
inference(contradiction_clause,[status(thm)],[f2440]) ).
fof(f2442,plain,
$false,
inference(sat_refutation,[status(thm)],[f440,f730,f751,f764,f766,f777,f789,f894,f1503,f1565,f1742,f2441]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG104+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n002.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 21 04:22:46 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Drodi V4.1.1
% 75.49/9.96 % Refutation found
% 75.49/9.96 % SZS status Theorem for theBenchmark: Theorem is valid
% 75.49/9.96 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 19.65/10.04 % Elapsed time: 9.677536 seconds
% 19.65/10.04 % CPU time: 76.338163 seconds
% 19.65/10.04 % Total memory used: 453.516 MB
% 19.65/10.04 % Net memory used: 417.829 MB
%------------------------------------------------------------------------------