%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG076+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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:52 PM UTC 2026
% Result : Theorem 0.08s 0.40s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 40
% Syntax : Number of formulae : 127 ( 27 unt; 22 def)
% Number of atoms : 292 ( 16 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 277 ( 112 ~; 120 |; 18 &)
% ( 22 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 23 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 15 con; 0-2 aty)
% Number of variables : 30 ( 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10,axiom,
! [W0,W1] :
( ( aScalar0(W1)
& aScalar0(W0) )
=> aScalar0(sdtpldt0(W0,W1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [W0,W1] :
( ( aScalar0(W1)
& aScalar0(W0) )
=> aScalar0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [W0,W1,W2,W3] :
( ( aScalar0(W3)
& aScalar0(W2)
& aScalar0(W1)
& aScalar0(W0) )
=> ( ( sdtlseqdt0(W2,W3)
& sdtlseqdt0(W0,W1) )
=> sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [W0,W1] :
( ( aScalar0(W1)
& aScalar0(W0) )
=> ( sdtlseqdt0(W1,W0)
| sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
( xA = sdtlbdtrb0(xs,aDimensionOf0(xs))
& aScalar0(xA) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,hypothesis,
( xB = sdtlbdtrb0(xt,aDimensionOf0(xt))
& aScalar0(xB) ),
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(f56,hypothesis,
sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,hypothesis,
sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,conjecture,
sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))),sdtpldt0(sdtasdt0(xC,xD),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,negated_conjecture,
~ sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))),sdtpldt0(sdtasdt0(xC,xD),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))),
inference(negated_conjecture,[status(cth)],[f58]) ).
fof(f81,plain,
! [W0,W1] :
( aScalar0(sdtpldt0(W0,W1))
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f82,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
! [W0,W1] :
( aScalar0(sdtasdt0(W0,W1))
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f84,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f119,plain,
! [W0,W1,W2,W3] :
( sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W3))
| ~ sdtlseqdt0(W2,W3)
| ~ sdtlseqdt0(W0,W1)
| ~ aScalar0(W3)
| ~ aScalar0(W2)
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f120,plain,
! [X0,X1,X2,X3] :
( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3))
| ~ sdtlseqdt0(X2,X3)
| ~ sdtlseqdt0(X0,X1)
| ~ aScalar0(X3)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f123,plain,
! [W0,W1] :
( sdtlseqdt0(W1,W0)
| sdtlseqdt0(W0,W1)
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f124,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f174,plain,
aScalar0(xA),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f176,plain,
aScalar0(xB),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f178,plain,
aScalar0(xC),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f180,plain,
aScalar0(xD),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f182,plain,
aScalar0(xE),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f185,plain,
xF = sdtasdt0(xA,xA),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f187,plain,
xG = sdtasdt0(xB,xB),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f188,plain,
aScalar0(xH),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f191,plain,
xR = sdtasdt0(xC,xG),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f193,plain,
xP = sdtasdt0(xE,xH),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f195,plain,
xS = sdtasdt0(xF,xD),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f198,plain,
sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f199,plain,
sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f200,plain,
~ sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))),sdtpldt0(sdtasdt0(xC,xD),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f219,plain,
( aScalar0(xP)
| ~ aScalar0(xH)
| ~ aScalar0(xE) ),
inference(paramodulation,[status(thm)],[f193,f84]) ).
fof(f220,definition,
( sQ4_spl
<=> aScalar0(xE) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f222,plain,
( sQ4_spl
| ~ aScalar0(xE) ),
inference(component_clause,[status(thm)],[f220]) ).
fof(f223,definition,
( sQ5_spl
<=> aScalar0(xH) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f225,plain,
( sQ5_spl
| ~ aScalar0(xH) ),
inference(component_clause,[status(thm)],[f223]) ).
fof(f226,definition,
( sQ6_spl
<=> aScalar0(xP) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f229,plain,
( sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f219,f220,f223,f226]) ).
fof(f246,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f225,f188]) ).
fof(f247,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f246]) ).
fof(f248,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f222,f182]) ).
fof(f249,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f248]) ).
fof(f296,definition,
( sQ16_spl
<=> aScalar0(sdtasdt0(xC,xD)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f298,plain,
( sQ16_spl
| ~ aScalar0(sdtasdt0(xC,xD)) ),
inference(component_clause,[status(thm)],[f296]) ).
fof(f299,definition,
( sQ17_spl
<=> aScalar0(sdtasdt0(xE,xE)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f301,plain,
( sQ17_spl
| ~ aScalar0(sdtasdt0(xE,xE)) ),
inference(component_clause,[status(thm)],[f299]) ).
fof(f309,definition,
( sQ20_spl
<=> aScalar0(sdtpldt0(xR,xS)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f311,plain,
( sQ20_spl
| ~ aScalar0(sdtpldt0(xR,xS)) ),
inference(component_clause,[status(thm)],[f309]) ).
fof(f312,definition,
( sQ21_spl
<=> aScalar0(sdtpldt0(xP,xP)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f314,plain,
( sQ21_spl
| ~ aScalar0(sdtpldt0(xP,xP)) ),
inference(component_clause,[status(thm)],[f312]) ).
fof(f411,plain,
( aScalar0(xF)
| ~ aScalar0(xA)
| ~ aScalar0(xA) ),
inference(paramodulation,[status(thm)],[f185,f84]) ).
fof(f417,definition,
( sQ42_spl
<=> aScalar0(xA) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f419,plain,
( sQ42_spl
| ~ aScalar0(xA) ),
inference(component_clause,[status(thm)],[f417]) ).
fof(f441,definition,
( sQ48_spl
<=> aScalar0(xF) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f444,plain,
( sQ48_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f411,f417,f441]) ).
fof(f453,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f419,f174]) ).
fof(f454,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f453]) ).
fof(f461,plain,
( aScalar0(xG)
| ~ aScalar0(xB)
| ~ aScalar0(xB) ),
inference(paramodulation,[status(thm)],[f187,f84]) ).
fof(f467,definition,
( sQ52_spl
<=> aScalar0(xB) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f469,plain,
( sQ52_spl
| ~ aScalar0(xB) ),
inference(component_clause,[status(thm)],[f467]) ).
fof(f491,definition,
( sQ58_spl
<=> aScalar0(xG) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f494,plain,
( sQ58_spl
| ~ sQ52_spl ),
inference(split_clause,[status(thm)],[f461,f467,f491]) ).
fof(f503,plain,
( sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f469,f176]) ).
fof(f504,plain,
sQ52_spl,
inference(contradiction_clause,[status(thm)],[f503]) ).
fof(f562,plain,
( aScalar0(xR)
| ~ aScalar0(xG)
| ~ aScalar0(xC) ),
inference(paramodulation,[status(thm)],[f191,f84]) ).
fof(f568,definition,
( sQ71_spl
<=> aScalar0(xC) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f570,plain,
( sQ71_spl
| ~ aScalar0(xC) ),
inference(component_clause,[status(thm)],[f568]) ).
fof(f597,definition,
( sQ78_spl
<=> aScalar0(xR) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f600,plain,
( sQ78_spl
| ~ sQ58_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f562,f568,f491,f597]) ).
fof(f609,plain,
( sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f570,f178]) ).
fof(f610,plain,
sQ71_spl,
inference(contradiction_clause,[status(thm)],[f609]) ).
fof(f617,plain,
( aScalar0(xS)
| ~ aScalar0(xD)
| ~ aScalar0(xF) ),
inference(paramodulation,[status(thm)],[f195,f84]) ).
fof(f623,definition,
( sQ82_spl
<=> aScalar0(xD) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f625,plain,
( sQ82_spl
| ~ aScalar0(xD) ),
inference(component_clause,[status(thm)],[f623]) ).
fof(f647,definition,
( sQ88_spl
<=> aScalar0(xS) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f650,plain,
( sQ88_spl
| ~ sQ82_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f617,f441,f623,f647]) ).
fof(f659,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f625,f180]) ).
fof(f660,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f659]) ).
fof(f732,definition,
( sQ104_spl
<=> aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH))) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f734,plain,
( sQ104_spl
| ~ aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH))) ),
inference(component_clause,[status(thm)],[f732]) ).
fof(f736,plain,
( sQ104_spl
| ~ aScalar0(sdtasdt0(xH,xH))
| ~ aScalar0(sdtpldt0(xR,xS)) ),
inference(resolution,[status(thm)],[f734,f82]) ).
fof(f737,definition,
( sQ105_spl
<=> aScalar0(sdtasdt0(xH,xH)) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f739,plain,
( sQ105_spl
| ~ aScalar0(sdtasdt0(xH,xH)) ),
inference(component_clause,[status(thm)],[f737]) ).
fof(f740,plain,
( sQ104_spl
| ~ sQ105_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f736,f309,f737,f732]) ).
fof(f742,definition,
( sQ106_spl
<=> aScalar0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f744,plain,
( sQ106_spl
| ~ aScalar0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))) ),
inference(component_clause,[status(thm)],[f742]) ).
fof(f746,plain,
( sQ105_spl
| ~ aScalar0(xH)
| ~ aScalar0(xH) ),
inference(resolution,[status(thm)],[f739,f84]) ).
fof(f747,plain,
( sQ105_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f746,f223,f737]) ).
fof(f748,plain,
( sQ106_spl
| ~ aScalar0(sdtasdt0(xH,xH))
| ~ aScalar0(sdtpldt0(xP,xP)) ),
inference(resolution,[status(thm)],[f744,f82]) ).
fof(f749,plain,
( sQ106_spl
| ~ sQ105_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f748,f312,f737,f742]) ).
fof(f876,plain,
( sQ16_spl
| ~ aScalar0(xD)
| ~ aScalar0(xC) ),
inference(resolution,[status(thm)],[f298,f84]) ).
fof(f877,plain,
( sQ16_spl
| ~ sQ82_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f876,f568,f623,f296]) ).
fof(f878,plain,
( sQ20_spl
| ~ aScalar0(xS)
| ~ aScalar0(xR) ),
inference(resolution,[status(thm)],[f311,f82]) ).
fof(f879,plain,
( sQ20_spl
| ~ sQ88_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f878,f597,f647,f309]) ).
fof(f880,plain,
( sQ17_spl
| ~ aScalar0(xE)
| ~ aScalar0(xE) ),
inference(resolution,[status(thm)],[f301,f84]) ).
fof(f881,plain,
( sQ17_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f880,f220,f299]) ).
fof(f882,plain,
( sQ21_spl
| ~ aScalar0(xP)
| ~ aScalar0(xP) ),
inference(resolution,[status(thm)],[f314,f82]) ).
fof(f883,plain,
( sQ21_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f882,f226,f312]) ).
fof(f897,plain,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))
| ~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD))
| ~ aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))
| ~ aScalar0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)))
| ~ aScalar0(sdtasdt0(xC,xD))
| ~ aScalar0(sdtasdt0(xE,xE)) ),
inference(resolution,[status(thm)],[f120,f200]) ).
fof(f900,definition,
( sQ133_spl
<=> sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f902,plain,
( sQ133_spl
| ~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)) ),
inference(component_clause,[status(thm)],[f900]) ).
fof(f903,definition,
( sQ134_spl
<=> sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH))) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f905,plain,
( sQ134_spl
| ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH))) ),
inference(component_clause,[status(thm)],[f903]) ).
fof(f906,plain,
( ~ sQ134_spl
| ~ sQ133_spl
| ~ sQ104_spl
| ~ sQ106_spl
| ~ sQ16_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f897,f299,f296,f742,f732,f900,f903]) ).
fof(f909,plain,
( sQ133_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f902,f198]) ).
fof(f910,plain,
sQ133_spl,
inference(contradiction_clause,[status(thm)],[f909]) ).
fof(f976,plain,
( sQ134_spl
| ~ sdtlseqdt0(sdtasdt0(xH,xH),sdtasdt0(xH,xH))
| ~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS))
| ~ aScalar0(sdtasdt0(xH,xH))
| ~ aScalar0(sdtasdt0(xH,xH))
| ~ aScalar0(sdtpldt0(xR,xS))
| ~ aScalar0(sdtpldt0(xP,xP)) ),
inference(resolution,[status(thm)],[f905,f120]) ).
fof(f978,definition,
( sQ144_spl
<=> sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f980,plain,
( sQ144_spl
| ~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)) ),
inference(component_clause,[status(thm)],[f978]) ).
fof(f981,definition,
( sQ145_spl
<=> sdtlseqdt0(sdtasdt0(xH,xH),sdtasdt0(xH,xH)) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f983,plain,
( sQ145_spl
| ~ sdtlseqdt0(sdtasdt0(xH,xH),sdtasdt0(xH,xH)) ),
inference(component_clause,[status(thm)],[f981]) ).
fof(f984,plain,
( sQ134_spl
| ~ sQ145_spl
| ~ sQ144_spl
| ~ sQ105_spl
| ~ sQ20_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f976,f312,f309,f737,f978,f981,f903]) ).
fof(f989,plain,
( sQ144_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f980,f199]) ).
fof(f990,plain,
sQ144_spl,
inference(contradiction_clause,[status(thm)],[f989]) ).
fof(f1413,plain,
( sQ145_spl
| sdtlseqdt0(sdtasdt0(xH,xH),sdtasdt0(xH,xH))
| ~ aScalar0(sdtasdt0(xH,xH))
| ~ aScalar0(sdtasdt0(xH,xH)) ),
inference(resolution,[status(thm)],[f983,f124]) ).
fof(f1422,plain,
( sQ145_spl
| ~ sQ105_spl ),
inference(split_clause,[status(thm)],[f1413,f737,f981]) ).
fof(f1424,plain,
$false,
inference(sat_refutation,[status(thm)],[f229,f247,f249,f444,f454,f494,f504,f600,f610,f650,f660,f740,f747,f749,f877,f879,f881,f883,f906,f910,f984,f990,f1422]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG076+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 04:17:51 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.08/0.40 % Refutation found
% 0.08/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.42 % Elapsed time: 0.064268 seconds
% 0.13/0.42 % CPU time: 0.242147 seconds
% 0.13/0.42 % Total memory used: 69.833 MB
% 0.13/0.42 % Net memory used: 69.522 MB
%------------------------------------------------------------------------------