%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG076+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 : n015.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.21s 5.52s
% Output : CNFRefutation 0.21s
% 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(f168,plain,
aScalar0(xA),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f170,plain,
aScalar0(xB),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f172,plain,
aScalar0(xC),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f174,plain,
aScalar0(xD),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f176,plain,
aScalar0(xE),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f179,plain,
xF = sdtasdt0(xA,xA),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f181,plain,
xG = sdtasdt0(xB,xB),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f182,plain,
aScalar0(xH),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f185,plain,
xR = sdtasdt0(xC,xG),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f187,plain,
xP = sdtasdt0(xE,xH),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f189,plain,
xS = sdtasdt0(xF,xD),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f192,plain,
sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f193,plain,
sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f194,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(f213,plain,
( aScalar0(xP)
| ~ aScalar0(xH)
| ~ aScalar0(xE) ),
inference(paramodulation,[status(thm)],[f187,f84]) ).
fof(f214,definition,
( sQ4_spl
<=> aScalar0(xE) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f216,plain,
( sQ4_spl
| ~ aScalar0(xE) ),
inference(component_clause,[status(thm)],[f214]) ).
fof(f217,definition,
( sQ5_spl
<=> aScalar0(xH) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f219,plain,
( sQ5_spl
| ~ aScalar0(xH) ),
inference(component_clause,[status(thm)],[f217]) ).
fof(f220,definition,
( sQ6_spl
<=> aScalar0(xP) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f223,plain,
( sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f213,f214,f217,f220]) ).
fof(f240,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f219,f182]) ).
fof(f241,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f240]) ).
fof(f242,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f216,f176]) ).
fof(f243,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f242]) ).
fof(f290,definition,
( sQ16_spl
<=> aScalar0(sdtpldt0(xR,xS)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f292,plain,
( sQ16_spl
| ~ aScalar0(sdtpldt0(xR,xS)) ),
inference(component_clause,[status(thm)],[f290]) ).
fof(f293,definition,
( sQ17_spl
<=> aScalar0(sdtpldt0(xP,xP)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f295,plain,
( sQ17_spl
| ~ aScalar0(sdtpldt0(xP,xP)) ),
inference(component_clause,[status(thm)],[f293]) ).
fof(f310,definition,
( sQ22_spl
<=> aScalar0(sdtasdt0(xC,xD)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f312,plain,
( sQ22_spl
| ~ aScalar0(sdtasdt0(xC,xD)) ),
inference(component_clause,[status(thm)],[f310]) ).
fof(f313,definition,
( sQ23_spl
<=> aScalar0(sdtasdt0(xE,xE)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f315,plain,
( sQ23_spl
| ~ aScalar0(sdtasdt0(xE,xE)) ),
inference(component_clause,[status(thm)],[f313]) ).
fof(f323,plain,
( sQ23_spl
| ~ aScalar0(xE)
| ~ aScalar0(xE) ),
inference(resolution,[status(thm)],[f315,f84]) ).
fof(f324,plain,
( sQ23_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f323,f214,f313]) ).
fof(f407,plain,
( aScalar0(xF)
| ~ aScalar0(xA)
| ~ aScalar0(xA) ),
inference(paramodulation,[status(thm)],[f179,f84]) ).
fof(f413,definition,
( sQ42_spl
<=> aScalar0(xA) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f415,plain,
( sQ42_spl
| ~ aScalar0(xA) ),
inference(component_clause,[status(thm)],[f413]) ).
fof(f437,definition,
( sQ48_spl
<=> aScalar0(xF) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f440,plain,
( sQ48_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f407,f413,f437]) ).
fof(f449,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f415,f168]) ).
fof(f450,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f449]) ).
fof(f457,plain,
( aScalar0(xG)
| ~ aScalar0(xB)
| ~ aScalar0(xB) ),
inference(paramodulation,[status(thm)],[f181,f84]) ).
fof(f463,definition,
( sQ52_spl
<=> aScalar0(xB) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f465,plain,
( sQ52_spl
| ~ aScalar0(xB) ),
inference(component_clause,[status(thm)],[f463]) ).
fof(f487,definition,
( sQ58_spl
<=> aScalar0(xG) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f490,plain,
( sQ58_spl
| ~ sQ52_spl ),
inference(split_clause,[status(thm)],[f457,f463,f487]) ).
fof(f499,plain,
( sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f465,f170]) ).
fof(f500,plain,
sQ52_spl,
inference(contradiction_clause,[status(thm)],[f499]) ).
fof(f558,plain,
( aScalar0(xR)
| ~ aScalar0(xG)
| ~ aScalar0(xC) ),
inference(paramodulation,[status(thm)],[f185,f84]) ).
fof(f564,definition,
( sQ71_spl
<=> aScalar0(xC) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f566,plain,
( sQ71_spl
| ~ aScalar0(xC) ),
inference(component_clause,[status(thm)],[f564]) ).
fof(f593,definition,
( sQ78_spl
<=> aScalar0(xR) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f596,plain,
( sQ78_spl
| ~ sQ58_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f558,f564,f487,f593]) ).
fof(f605,plain,
( sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f566,f172]) ).
fof(f606,plain,
sQ71_spl,
inference(contradiction_clause,[status(thm)],[f605]) ).
fof(f613,plain,
( aScalar0(xS)
| ~ aScalar0(xD)
| ~ aScalar0(xF) ),
inference(paramodulation,[status(thm)],[f189,f84]) ).
fof(f619,definition,
( sQ82_spl
<=> aScalar0(xD) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f621,plain,
( sQ82_spl
| ~ aScalar0(xD) ),
inference(component_clause,[status(thm)],[f619]) ).
fof(f643,definition,
( sQ88_spl
<=> aScalar0(xS) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f646,plain,
( sQ88_spl
| ~ sQ82_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f613,f437,f619,f643]) ).
fof(f655,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f621,f174]) ).
fof(f656,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f655]) ).
fof(f676,definition,
( sQ94_spl
<=> aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH))) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f678,plain,
( sQ94_spl
| ~ aScalar0(sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH))) ),
inference(component_clause,[status(thm)],[f676]) ).
fof(f680,plain,
( sQ94_spl
| ~ aScalar0(sdtasdt0(xH,xH))
| ~ aScalar0(sdtpldt0(xR,xS)) ),
inference(resolution,[status(thm)],[f678,f82]) ).
fof(f681,definition,
( sQ95_spl
<=> aScalar0(sdtasdt0(xH,xH)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f683,plain,
( sQ95_spl
| ~ aScalar0(sdtasdt0(xH,xH)) ),
inference(component_clause,[status(thm)],[f681]) ).
fof(f684,plain,
( sQ94_spl
| ~ sQ95_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f680,f290,f681,f676]) ).
fof(f686,definition,
( sQ96_spl
<=> aScalar0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f688,plain,
( sQ96_spl
| ~ aScalar0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))) ),
inference(component_clause,[status(thm)],[f686]) ).
fof(f690,plain,
( sQ95_spl
| ~ aScalar0(xH)
| ~ aScalar0(xH) ),
inference(resolution,[status(thm)],[f683,f84]) ).
fof(f691,plain,
( sQ95_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f690,f217,f681]) ).
fof(f692,plain,
( sQ96_spl
| ~ aScalar0(sdtasdt0(xH,xH))
| ~ aScalar0(sdtpldt0(xP,xP)) ),
inference(resolution,[status(thm)],[f688,f82]) ).
fof(f693,plain,
( sQ96_spl
| ~ sQ95_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f692,f293,f681,f686]) ).
fof(f694,plain,
( sQ22_spl
| ~ aScalar0(xD)
| ~ aScalar0(xC) ),
inference(resolution,[status(thm)],[f312,f84]) ).
fof(f695,plain,
( sQ22_spl
| ~ sQ82_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f694,f564,f619,f310]) ).
fof(f780,plain,
( sQ16_spl
| ~ aScalar0(xS)
| ~ aScalar0(xR) ),
inference(resolution,[status(thm)],[f292,f82]) ).
fof(f781,plain,
( sQ16_spl
| ~ sQ88_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f780,f593,f643,f290]) ).
fof(f782,plain,
( sQ17_spl
| ~ aScalar0(xP)
| ~ aScalar0(xP) ),
inference(resolution,[status(thm)],[f295,f82]) ).
fof(f783,plain,
( sQ17_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f782,f220,f293]) ).
fof(f785,definition,
( sQ113_spl
<=> sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f787,plain,
( sQ113_spl
| ~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)) ),
inference(component_clause,[status(thm)],[f785]) ).
fof(f802,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,f194]) ).
fof(f805,definition,
( sQ116_spl
<=> sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH))) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f807,plain,
( sQ116_spl
| ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH))) ),
inference(component_clause,[status(thm)],[f805]) ).
fof(f808,plain,
( ~ sQ116_spl
| ~ sQ113_spl
| ~ sQ94_spl
| ~ sQ96_spl
| ~ sQ22_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f802,f313,f310,f686,f676,f785,f805]) ).
fof(f1002,plain,
( sQ116_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)],[f807,f120]) ).
fof(f1004,definition,
( sQ153_spl
<=> sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1006,plain,
( sQ153_spl
| ~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)) ),
inference(component_clause,[status(thm)],[f1004]) ).
fof(f1007,definition,
( sQ154_spl
<=> sdtlseqdt0(sdtasdt0(xH,xH),sdtasdt0(xH,xH)) ),
introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition]) ).
fof(f1009,plain,
( sQ154_spl
| ~ sdtlseqdt0(sdtasdt0(xH,xH),sdtasdt0(xH,xH)) ),
inference(component_clause,[status(thm)],[f1007]) ).
fof(f1010,plain,
( sQ116_spl
| ~ sQ154_spl
| ~ sQ153_spl
| ~ sQ95_spl
| ~ sQ16_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1002,f293,f290,f681,f1004,f1007,f805]) ).
fof(f1015,plain,
( sQ153_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1006,f193]) ).
fof(f1016,plain,
sQ153_spl,
inference(contradiction_clause,[status(thm)],[f1015]) ).
fof(f1398,plain,
( sQ154_spl
| sdtlseqdt0(sdtasdt0(xH,xH),sdtasdt0(xH,xH))
| ~ aScalar0(sdtasdt0(xH,xH))
| ~ aScalar0(sdtasdt0(xH,xH)) ),
inference(resolution,[status(thm)],[f1009,f124]) ).
fof(f1404,plain,
( sQ154_spl
| ~ sQ95_spl ),
inference(split_clause,[status(thm)],[f1398,f681,f1007]) ).
fof(f1406,plain,
( sQ113_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f787,f192]) ).
fof(f1407,plain,
sQ113_spl,
inference(contradiction_clause,[status(thm)],[f1406]) ).
fof(f1408,plain,
$false,
inference(sat_refutation,[status(thm)],[f223,f241,f243,f324,f440,f450,f490,f500,f596,f606,f646,f656,f684,f691,f693,f695,f781,f783,f808,f1010,f1016,f1404,f1407]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG076+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.46 % Computer : n015.cluster.edu
% 0.16/5.46 % Model : x86_64 x86_64
% 0.16/5.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.46 % Memory : 8046.5625MB
% 0.16/5.46 % OS : Linux 6.8.0-71-generic
% 0.16/5.46 % CPULimit : 300
% 0.16/5.46 % WCLimit : 300
% 0.16/5.46 % DateTime : Mon Sep 21 04:21:12 UTC 2026
% 0.16/5.46 % CPUTime :
% 0.16/5.47 % Drodi V4.1.1
% 0.21/5.52 % Refutation found
% 0.21/5.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/5.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.21/5.58 % Elapsed time: 0.112677 seconds
% 0.21/5.58 % CPU time: 0.356460 seconds
% 0.21/5.58 % Total memory used: 63.648 MB
% 0.21/5.58 % Net memory used: 63.344 MB
%------------------------------------------------------------------------------