%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG079+1 : 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:04:53 PM UTC 2026
% Result : Theorem 0.23s 0.88s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 26
% Syntax : Number of formulae : 87 ( 30 unt; 12 def)
% Number of atoms : 179 ( 27 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 154 ( 62 ~; 67 |; 12 &)
% ( 12 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 17 ( 15 usr; 13 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 15 con; 0-2 aty)
% Number of variables : 24 ( 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [W0,W1,W2,W3] :
( ( aScalar0(W3)
& aScalar0(W2)
& aScalar0(W1)
& aScalar0(W0) )
=> sdtasdt0(sdtpldt0(W0,W1),sdtpldt0(W2,W3)) = sdtpldt0(sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W0,W3)),sdtpldt0(sdtasdt0(W1,W2),sdtasdt0(W1,W3))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
( xC = sdtasasdt0(xp,xp)
& aScalar0(xC) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,hypothesis,
( xD = sdtasasdt0(xq,xq)
& aScalar0(xD) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,hypothesis,
( xE = sdtasasdt0(xp,xq)
& aScalar0(xE) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
( xF = sdtasdt0(xA,xA)
& aScalar0(xF) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,hypothesis,
( xG = sdtasdt0(xB,xB)
& aScalar0(xG) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,hypothesis,
( xH = sdtasdt0(xA,xB)
& aScalar0(xH) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,hypothesis,
( xR = sdtasdt0(xC,xG)
& aScalar0(xR) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,hypothesis,
( xP = sdtasdt0(xE,xH)
& aScalar0(xP) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,hypothesis,
( xS = sdtasdt0(xF,xD)
& aScalar0(xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,hypothesis,
sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE,xE),sdtasdt0(xE,xH)),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),sdtpldt0(sdtpldt0(sdtasdt0(xC,xD),sdtasdt0(xC,xG)),sdtpldt0(sdtasdt0(xF,xD),sdtasdt0(xF,xG)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,conjecture,
sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,negated_conjecture,
~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))),
inference(negated_conjecture,[status(cth)],[f61]) ).
fof(f66,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f83,plain,
aScalar0(sz0z00),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f107,plain,
! [W0,W1,W2,W3] :
( sdtasdt0(sdtpldt0(W0,W1),sdtpldt0(W2,W3)) = sdtpldt0(sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W0,W3)),sdtpldt0(sdtasdt0(W1,W2),sdtasdt0(W1,W3)))
| ~ aScalar0(W3)
| ~ aScalar0(W2)
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f108,plain,
! [X0,X1,X2,X3] :
( sdtasdt0(sdtpldt0(X0,X1),sdtpldt0(X2,X3)) = sdtpldt0(sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X0,X3)),sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3)))
| ~ aScalar0(X3)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f175,plain,
aScalar0(xC),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f177,plain,
aScalar0(xD),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f179,plain,
aScalar0(xE),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f181,plain,
aScalar0(xF),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f183,plain,
aScalar0(xG),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f185,plain,
aScalar0(xH),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f188,plain,
xR = sdtasdt0(xC,xG),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f190,plain,
xP = sdtasdt0(xE,xH),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f192,plain,
xS = sdtasdt0(xF,xD),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f199,plain,
sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE,xE),sdtasdt0(xE,xH)),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),sdtpldt0(sdtpldt0(sdtasdt0(xC,xD),sdtasdt0(xC,xG)),sdtpldt0(sdtasdt0(xF,xD),sdtasdt0(xF,xG)))),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f200,plain,
~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f221,plain,
sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE,xE),xP),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),sdtpldt0(sdtpldt0(sdtasdt0(xC,xD),sdtasdt0(xC,xG)),sdtpldt0(sdtasdt0(xF,xD),sdtasdt0(xF,xG)))),
inference(forward_demodulation,[status(thm)],[f190,f199]) ).
fof(f222,plain,
sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE,xE),xP),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),sdtpldt0(sdtpldt0(sdtasdt0(xC,xD),xR),sdtpldt0(sdtasdt0(xF,xD),sdtasdt0(xF,xG)))),
inference(forward_demodulation,[status(thm)],[f188,f221]) ).
fof(f223,plain,
sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE,xE),xP),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),sdtpldt0(sdtpldt0(sdtasdt0(xC,xD),xR),sdtpldt0(xS,sdtasdt0(xF,xG)))),
inference(forward_demodulation,[status(thm)],[f192,f222]) ).
fof(f254,plain,
! [X0,X1] :
( sdtasdt0(sdtpldt0(xC,X0),sdtpldt0(X1,xG)) = sdtpldt0(sdtpldt0(sdtasdt0(xC,X1),xR),sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,xG)))
| ~ aScalar0(xG)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ aScalar0(xC) ),
inference(paramodulation,[status(thm)],[f188,f108]) ).
fof(f256,definition,
( sQ7_spl
<=> aScalar0(xC) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f258,plain,
( sQ7_spl
| ~ aScalar0(xC) ),
inference(component_clause,[status(thm)],[f256]) ).
fof(f259,definition,
( sQ8_spl
<=> aScalar0(xG) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f261,plain,
( sQ8_spl
| ~ aScalar0(xG) ),
inference(component_clause,[status(thm)],[f259]) ).
fof(f274,definition,
! [X0,X1] :
( sQ12_spl
<=> ( sdtasdt0(sdtpldt0(xC,X0),sdtpldt0(X1,xG)) = sdtpldt0(sdtpldt0(sdtasdt0(xC,X1),xR),sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,xG)))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f275,plain,
! [X0,X1] :
( ~ sQ12_spl
| sdtasdt0(sdtpldt0(xC,X0),sdtpldt0(X1,xG)) = sdtpldt0(sdtpldt0(sdtasdt0(xC,X1),xR),sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,xG)))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(component_clause,[status(thm)],[f274]) ).
fof(f277,plain,
( ~ sQ8_spl
| sQ12_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f254,f256,f274,f259]) ).
fof(f282,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f261,f183]) ).
fof(f283,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f282]) ).
fof(f284,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f258,f175]) ).
fof(f285,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f284]) ).
fof(f289,plain,
! [X0,X1] :
( sdtasdt0(sdtpldt0(xE,X0),sdtpldt0(X1,xH)) = sdtpldt0(sdtpldt0(sdtasdt0(xE,X1),xP),sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,xH)))
| ~ aScalar0(xH)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ aScalar0(xE) ),
inference(paramodulation,[status(thm)],[f190,f108]) ).
fof(f291,definition,
( sQ14_spl
<=> aScalar0(xE) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f293,plain,
( sQ14_spl
| ~ aScalar0(xE) ),
inference(component_clause,[status(thm)],[f291]) ).
fof(f294,definition,
( sQ15_spl
<=> aScalar0(xH) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f296,plain,
( sQ15_spl
| ~ aScalar0(xH) ),
inference(component_clause,[status(thm)],[f294]) ).
fof(f309,definition,
! [X0,X1] :
( sQ19_spl
<=> ( sdtasdt0(sdtpldt0(xE,X0),sdtpldt0(X1,xH)) = sdtpldt0(sdtpldt0(sdtasdt0(xE,X1),xP),sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,xH)))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f310,plain,
! [X0,X1] :
( ~ sQ19_spl
| sdtasdt0(sdtpldt0(xE,X0),sdtpldt0(X1,xH)) = sdtpldt0(sdtpldt0(sdtasdt0(xE,X1),xP),sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,xH)))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(component_clause,[status(thm)],[f309]) ).
fof(f312,plain,
( ~ sQ15_spl
| sQ19_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f289,f291,f309,f294]) ).
fof(f317,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f296,f185]) ).
fof(f318,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f317]) ).
fof(f319,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f293,f179]) ).
fof(f320,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f319]) ).
fof(f328,definition,
( sQ21_spl
<=> aScalar0(xD) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f330,plain,
( sQ21_spl
| ~ aScalar0(xD) ),
inference(component_clause,[status(thm)],[f328]) ).
fof(f331,definition,
( sQ22_spl
<=> aScalar0(xF) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f333,plain,
( sQ22_spl
| ~ aScalar0(xF) ),
inference(component_clause,[status(thm)],[f331]) ).
fof(f359,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f330,f177]) ).
fof(f360,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f359]) ).
fof(f361,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f333,f181]) ).
fof(f362,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f361]) ).
fof(f419,plain,
( ~ sQ12_spl
| sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)) = sdtpldt0(sdtpldt0(sdtasdt0(xC,xD),xR),sdtpldt0(xS,sdtasdt0(xF,xG)))
| ~ aScalar0(xD)
| ~ aScalar0(xF) ),
inference(paramodulation,[status(thm)],[f192,f275]) ).
fof(f428,definition,
( sQ40_spl
<=> sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)) = sdtpldt0(sdtpldt0(sdtasdt0(xC,xD),xR),sdtpldt0(xS,sdtasdt0(xF,xG))) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f429,plain,
( ~ sQ40_spl
| sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG)) = sdtpldt0(sdtpldt0(sdtasdt0(xC,xD),xR),sdtpldt0(xS,sdtasdt0(xF,xG))) ),
inference(component_clause,[status(thm)],[f428]) ).
fof(f431,plain,
( ~ sQ12_spl
| sQ40_spl
| ~ sQ21_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f419,f331,f328,f428,f274]) ).
fof(f444,plain,
( ~ sQ40_spl
| sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE,xE),xP),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))) ),
inference(backward_demodulation,[status(thm)],[f429,f223]) ).
fof(f674,definition,
( sQ78_spl
<=> aScalar0(sz0z00) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f676,plain,
( sQ78_spl
| ~ aScalar0(sz0z00) ),
inference(component_clause,[status(thm)],[f674]) ).
fof(f710,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f676,f83]) ).
fof(f711,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f710]) ).
fof(f840,definition,
( sQ107_spl
<=> aNaturalNumber0(sz00) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f842,plain,
( sQ107_spl
| ~ aNaturalNumber0(sz00) ),
inference(component_clause,[status(thm)],[f840]) ).
fof(f850,plain,
( sQ107_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f842,f66]) ).
fof(f851,plain,
sQ107_spl,
inference(contradiction_clause,[status(thm)],[f850]) ).
fof(f1270,definition,
( sQ183_spl
<=> sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)) = sdtpldt0(sdtpldt0(sdtasdt0(xE,xE),xP),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))) ),
introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition]) ).
fof(f1271,plain,
( ~ sQ183_spl
| sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)) = sdtpldt0(sdtpldt0(sdtasdt0(xE,xE),xP),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))) ),
inference(component_clause,[status(thm)],[f1270]) ).
fof(f1272,plain,
( sQ183_spl
| sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)) != sdtpldt0(sdtpldt0(sdtasdt0(xE,xE),xP),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))) ),
inference(component_clause,[status(thm)],[f1270]) ).
fof(f1280,plain,
( ~ sQ40_spl
| ~ sQ183_spl
| sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))) ),
inference(backward_demodulation,[status(thm)],[f1271,f444]) ).
fof(f1297,plain,
( ~ sQ40_spl
| ~ sQ183_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1280,f200]) ).
fof(f1298,plain,
( ~ sQ40_spl
| ~ sQ183_spl ),
inference(contradiction_clause,[status(thm)],[f1297]) ).
fof(f1299,plain,
( ~ sQ19_spl
| sQ183_spl
| ~ aScalar0(xE)
| ~ aScalar0(xH) ),
inference(resolution,[status(thm)],[f1272,f310]) ).
fof(f1300,plain,
( ~ sQ19_spl
| sQ183_spl
| ~ sQ14_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1299,f294,f291,f1270,f309]) ).
fof(f1301,plain,
$false,
inference(sat_refutation,[status(thm)],[f277,f283,f285,f312,f318,f320,f360,f362,f431,f711,f851,f1298,f1300]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG079+1 : 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.46 % Computer : n017.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.46 % CPULimit : 300
% 0.20/0.46 % WCLimit : 300
% 0.20/0.46 % DateTime : Mon Sep 21 04:13:27 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.48 % Drodi V4.1.1
% 0.23/0.88 % Refutation found
% 0.23/0.88 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.23/0.88 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.35/0.93 % Elapsed time: 0.462821 seconds
% 1.35/0.93 % CPU time: 2.945754 seconds
% 1.35/0.93 % Total memory used: 132.040 MB
% 1.35/0.93 % Net memory used: 130.647 MB
%------------------------------------------------------------------------------