%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG079+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 : n008.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.15s 1.49s
% Output : CNFRefutation 0.15s
% 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/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f46,hypothesis,
( xC = sdtasasdt0(xp,xp)
& aScalar0(xC) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,hypothesis,
( xD = sdtasasdt0(xq,xq)
& aScalar0(xD) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,hypothesis,
( xE = sdtasasdt0(xp,xq)
& aScalar0(xE) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
( xF = sdtasdt0(xA,xA)
& aScalar0(xF) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,hypothesis,
( xG = sdtasdt0(xB,xB)
& aScalar0(xG) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,hypothesis,
( xH = sdtasdt0(xA,xB)
& aScalar0(xH) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,hypothesis,
( xR = sdtasdt0(xC,xG)
& aScalar0(xR) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,hypothesis,
( xP = sdtasdt0(xE,xH)
& aScalar0(xP) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,hypothesis,
( xS = sdtasdt0(xF,xD)
& aScalar0(xS) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f61,conjecture,
sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))),
file('/export/starexec/sandbox/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(f181,plain,
aScalar0(xC),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f183,plain,
aScalar0(xD),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f185,plain,
aScalar0(xE),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f187,plain,
aScalar0(xF),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f189,plain,
aScalar0(xG),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f191,plain,
aScalar0(xH),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f194,plain,
xR = sdtasdt0(xC,xG),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f196,plain,
xP = sdtasdt0(xE,xH),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f198,plain,
xS = sdtasdt0(xF,xD),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f205,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(f206,plain,
~ sdtlseqdt0(sdtasdt0(sdtpldt0(xE,xH),sdtpldt0(xE,xH)),sdtasdt0(sdtpldt0(xC,xF),sdtpldt0(xD,xG))),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f228,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)],[f196,f205]) ).
fof(f229,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)],[f194,f228]) ).
fof(f230,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)],[f198,f229]) ).
fof(f261,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)],[f194,f108]) ).
fof(f263,definition,
( sQ7_spl
<=> aScalar0(xC) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f265,plain,
( sQ7_spl
| ~ aScalar0(xC) ),
inference(component_clause,[status(thm)],[f263]) ).
fof(f266,definition,
( sQ8_spl
<=> aScalar0(xG) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f268,plain,
( sQ8_spl
| ~ aScalar0(xG) ),
inference(component_clause,[status(thm)],[f266]) ).
fof(f281,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(f282,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)],[f281]) ).
fof(f284,plain,
( ~ sQ8_spl
| sQ12_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f261,f263,f281,f266]) ).
fof(f289,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f268,f189]) ).
fof(f290,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f289]) ).
fof(f291,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f265,f181]) ).
fof(f292,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f291]) ).
fof(f296,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)],[f196,f108]) ).
fof(f298,definition,
( sQ14_spl
<=> aScalar0(xE) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f300,plain,
( sQ14_spl
| ~ aScalar0(xE) ),
inference(component_clause,[status(thm)],[f298]) ).
fof(f301,definition,
( sQ15_spl
<=> aScalar0(xH) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f303,plain,
( sQ15_spl
| ~ aScalar0(xH) ),
inference(component_clause,[status(thm)],[f301]) ).
fof(f316,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(f317,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)],[f316]) ).
fof(f319,plain,
( ~ sQ15_spl
| sQ19_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f296,f298,f316,f301]) ).
fof(f324,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f303,f191]) ).
fof(f325,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f324]) ).
fof(f326,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f300,f185]) ).
fof(f327,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f326]) ).
fof(f335,definition,
( sQ21_spl
<=> aScalar0(xD) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f337,plain,
( sQ21_spl
| ~ aScalar0(xD) ),
inference(component_clause,[status(thm)],[f335]) ).
fof(f338,definition,
( sQ22_spl
<=> aScalar0(xF) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f340,plain,
( sQ22_spl
| ~ aScalar0(xF) ),
inference(component_clause,[status(thm)],[f338]) ).
fof(f366,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f337,f183]) ).
fof(f367,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f366]) ).
fof(f368,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f340,f187]) ).
fof(f369,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f368]) ).
fof(f426,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)],[f198,f282]) ).
fof(f435,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(f436,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)],[f435]) ).
fof(f438,plain,
( ~ sQ12_spl
| sQ40_spl
| ~ sQ21_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f426,f338,f335,f435,f281]) ).
fof(f451,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)],[f436,f230]) ).
fof(f681,definition,
( sQ78_spl
<=> aScalar0(sz0z00) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f683,plain,
( sQ78_spl
| ~ aScalar0(sz0z00) ),
inference(component_clause,[status(thm)],[f681]) ).
fof(f717,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f683,f83]) ).
fof(f718,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f717]) ).
fof(f847,definition,
( sQ107_spl
<=> aNaturalNumber0(sz00) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f849,plain,
( sQ107_spl
| ~ aNaturalNumber0(sz00) ),
inference(component_clause,[status(thm)],[f847]) ).
fof(f857,plain,
( sQ107_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f849,f66]) ).
fof(f858,plain,
sQ107_spl,
inference(contradiction_clause,[status(thm)],[f857]) ).
fof(f1277,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(f1278,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)],[f1277]) ).
fof(f1279,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)],[f1277]) ).
fof(f1287,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)],[f1278,f451]) ).
fof(f1304,plain,
( ~ sQ40_spl
| ~ sQ183_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1287,f206]) ).
fof(f1305,plain,
( ~ sQ40_spl
| ~ sQ183_spl ),
inference(contradiction_clause,[status(thm)],[f1304]) ).
fof(f1306,plain,
( ~ sQ19_spl
| sQ183_spl
| ~ aScalar0(xE)
| ~ aScalar0(xH) ),
inference(resolution,[status(thm)],[f1279,f317]) ).
fof(f1307,plain,
( ~ sQ19_spl
| sQ183_spl
| ~ sQ14_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1306,f301,f298,f1277,f316]) ).
fof(f1308,plain,
$false,
inference(sat_refutation,[status(thm)],[f284,f290,f292,f319,f325,f327,f367,f369,f438,f718,f858,f1305,f1307]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG079+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.58 % Computer : n008.cluster.edu
% 0.10/0.58 % Model : x86_64 x86_64
% 0.10/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.58 % Memory : 8046.5625MB
% 0.10/0.58 % OS : Linux 6.8.0-71-generic
% 0.10/0.58 % CPULimit : 300
% 0.10/0.58 % WCLimit : 300
% 0.10/0.58 % DateTime : Mon Sep 21 04:18:41 UTC 2026
% 0.10/0.58 % CPUTime :
% 0.10/0.62 % Drodi V4.1.1
% 0.15/1.49 % Refutation found
% 0.15/1.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/1.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.02/1.53 % Elapsed time: 0.920613 seconds
% 2.02/1.53 % CPU time: 6.628775 seconds
% 2.02/1.53 % Total memory used: 158.589 MB
% 2.02/1.53 % Net memory used: 155.497 MB
%------------------------------------------------------------------------------