%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG052+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 : n009.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:47 PM UTC 2026
% Result : Theorem 38.63s 5.36s
% Output : CNFRefutation 38.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 32
% Syntax : Number of formulae : 129 ( 25 unt; 17 def)
% Number of atoms : 335 ( 105 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 343 ( 137 ~; 146 |; 30 &)
% ( 18 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 17 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 8 con; 0-2 aty)
% Number of variables : 56 ( 52 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( szszuzczcdt0(W0) != sz00
& aNaturalNumber0(szszuzczcdt0(W0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [W0] :
( ( W0 != sz00
& aNaturalNumber0(W0) )
=> ? [W1] :
( W0 = szszuzczcdt0(W1)
& aNaturalNumber0(W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( szszuzczcdt0(W0) = szszuzczcdt0(W1)
=> W0 = W1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> iLess0(W0,szszuzczcdt0(W0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [W0] :
( aVector0(W0)
=> aNaturalNumber0(aDimensionOf0(W0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,definition,
! [W0] :
( aVector0(W0)
=> ( aDimensionOf0(W0) != sz00
=> ! [W1] :
( W1 = sziznziztdt0(W0)
<=> ( ! [W2] :
( aNaturalNumber0(W2)
=> sdtlbdtrb0(W1,W2) = sdtlbdtrb0(W0,W2) )
& szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(W0)
& aVector0(W1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
( aVector0(xt)
& aVector0(xs) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
! [W0,W1] :
( ( aVector0(W1)
& aVector0(W0) )
=> ( aDimensionOf0(W0) = aDimensionOf0(W1)
=> ( iLess0(aDimensionOf0(W0),aDimensionOf0(xs))
=> sdtlseqdt0(sdtasdt0(sdtasasdt0(W0,W1),sdtasasdt0(W0,W1)),sdtasdt0(sdtasasdt0(W0,W0),sdtasasdt0(W1,W1))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
aDimensionOf0(xs) = aDimensionOf0(xt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
aDimensionOf0(xs) != sz00,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
( xp = sziznziztdt0(xs)
& aVector0(xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
( xq = sziznziztdt0(xt)
& aVector0(xq) ),
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(f56,conjecture,
sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,negated_conjecture,
~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(negated_conjecture,[status(cth)],[f56]) ).
fof(f62,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aNaturalNumber0(szszuzczcdt0(W0)) )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f63,plain,
! [X0] :
( aNaturalNumber0(szszuzczcdt0(X0))
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f64,plain,
! [X0] :
( szszuzczcdt0(X0) != sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f65,plain,
! [W0] :
( ? [W1] :
( W0 = szszuzczcdt0(W1)
& aNaturalNumber0(W1) )
| W0 = sz00
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f66,plain,
! [W0] :
( ( W0 = szszuzczcdt0(sK0_skl(W0))
& aNaturalNumber0(sK0_skl(W0)) )
| W0 = sz00
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f65]) ).
fof(f67,plain,
! [X0] :
( aNaturalNumber0(sK0_skl(X0))
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f68,plain,
! [X0] :
( X0 = szszuzczcdt0(sK0_skl(X0))
| X0 = sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f69,plain,
! [W0,W1] :
( W0 = W1
| szszuzczcdt0(W0) != szszuzczcdt0(W1)
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f70,plain,
! [X0,X1] :
( X0 = X1
| szszuzczcdt0(X0) != szszuzczcdt0(X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f73,plain,
! [W0] :
( iLess0(W0,szszuzczcdt0(W0))
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f74,plain,
! [X0] :
( iLess0(X0,szszuzczcdt0(X0))
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f133,plain,
! [W0] :
( aNaturalNumber0(aDimensionOf0(W0))
| ~ aVector0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f134,plain,
! [X0] :
( aNaturalNumber0(aDimensionOf0(X0))
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f137,plain,
! [W0] :
( ! [W1] :
( W1 = sziznziztdt0(W0)
<=> ( ! [W2] :
( sdtlbdtrb0(W1,W2) = sdtlbdtrb0(W0,W2)
| ~ aNaturalNumber0(W2) )
& szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(W0)
& aVector0(W1) ) )
| aDimensionOf0(W0) = sz00
| ~ aVector0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f138,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( sdtlbdtrb0(W1,W2) != sdtlbdtrb0(W0,W2)
& aNaturalNumber0(W2) )
| szszuzczcdt0(aDimensionOf0(W1)) != aDimensionOf0(W0)
| ~ aVector0(W1)
| W1 = sziznziztdt0(W0) )
& ( ( ! [W2] :
( sdtlbdtrb0(W1,W2) = sdtlbdtrb0(W0,W2)
| ~ aNaturalNumber0(W2) )
& szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(W0)
& aVector0(W1) )
| W1 != sziznziztdt0(W0) ) )
| aDimensionOf0(W0) = sz00
| ~ aVector0(W0) ),
inference(NNF_transformation,[status(thm)],[f137]) ).
fof(f139,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( sdtlbdtrb0(W1,W2) != sdtlbdtrb0(W0,W2)
& aNaturalNumber0(W2) )
| szszuzczcdt0(aDimensionOf0(W1)) != aDimensionOf0(W0)
| ~ aVector0(W1)
| W1 = sziznziztdt0(W0) )
& ! [W1] :
( ( ! [W2] :
( sdtlbdtrb0(W1,W2) = sdtlbdtrb0(W0,W2)
| ~ aNaturalNumber0(W2) )
& szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(W0)
& aVector0(W1) )
| W1 != sziznziztdt0(W0) ) )
| aDimensionOf0(W0) = sz00
| ~ aVector0(W0) ),
inference(miniscoping,[status(thm)],[f138]) ).
fof(f140,plain,
! [W0] :
( ( ! [W1] :
( ( sdtlbdtrb0(W1,sK1_skl(W1,W0)) != sdtlbdtrb0(W0,sK1_skl(W1,W0))
& aNaturalNumber0(sK1_skl(W1,W0)) )
| szszuzczcdt0(aDimensionOf0(W1)) != aDimensionOf0(W0)
| ~ aVector0(W1)
| W1 = sziznziztdt0(W0) )
& ! [W1] :
( ( ! [W2] :
( sdtlbdtrb0(W1,W2) = sdtlbdtrb0(W0,W2)
| ~ aNaturalNumber0(W2) )
& szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(W0)
& aVector0(W1) )
| W1 != sziznziztdt0(W0) ) )
| aDimensionOf0(W0) = sz00
| ~ aVector0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f139]) ).
fof(f142,plain,
! [X0,X1] :
( szszuzczcdt0(aDimensionOf0(X1)) = aDimensionOf0(X0)
| X1 != sziznziztdt0(X0)
| aDimensionOf0(X0) = sz00
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f156,plain,
aVector0(xs),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f157,plain,
aVector0(xt),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f158,plain,
! [W0,W1] :
( sdtlseqdt0(sdtasdt0(sdtasasdt0(W0,W1),sdtasasdt0(W0,W1)),sdtasdt0(sdtasasdt0(W0,W0),sdtasasdt0(W1,W1)))
| ~ iLess0(aDimensionOf0(W0),aDimensionOf0(xs))
| aDimensionOf0(W0) != aDimensionOf0(W1)
| ~ aVector0(W1)
| ~ aVector0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f159,plain,
! [X0,X1] :
( sdtlseqdt0(sdtasdt0(sdtasasdt0(X0,X1),sdtasasdt0(X0,X1)),sdtasdt0(sdtasasdt0(X0,X0),sdtasasdt0(X1,X1)))
| ~ iLess0(aDimensionOf0(X0),aDimensionOf0(xs))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X1)
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f160,plain,
aDimensionOf0(xs) = aDimensionOf0(xt),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f161,plain,
aDimensionOf0(xs) != sz00,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f162,plain,
aVector0(xp),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f163,plain,
xp = sziznziztdt0(xs),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f164,plain,
aVector0(xq),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f165,plain,
xq = sziznziztdt0(xt),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f171,plain,
xC = sdtasasdt0(xp,xp),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f173,plain,
xD = sdtasasdt0(xq,xq),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f175,plain,
xE = sdtasasdt0(xp,xq),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f190,plain,
~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f207,plain,
! [X0] :
( szszuzczcdt0(aDimensionOf0(sziznziztdt0(X0))) = aDimensionOf0(X0)
| aDimensionOf0(X0) = sz00
| ~ aVector0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f142]) ).
fof(f370,plain,
aDimensionOf0(xt) != sz00,
inference(backward_demodulation,[status(thm)],[f160,f161]) ).
fof(f372,definition,
( sQ22_spl
<=> aVector0(xs) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f374,plain,
( sQ22_spl
| ~ aVector0(xs) ),
inference(component_clause,[status(thm)],[f372]) ).
fof(f379,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f374,f156]) ).
fof(f380,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f379]) ).
fof(f473,plain,
! [X0] :
( szszuzczcdt0(X0) = sz00
| ~ aNaturalNumber0(szszuzczcdt0(X0))
| X0 = sK0_skl(szszuzczcdt0(X0))
| ~ aNaturalNumber0(sK0_skl(szszuzczcdt0(X0)))
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f70,f68]) ).
fof(f476,plain,
! [X0] :
( szszuzczcdt0(X0) = sz00
| ~ aNaturalNumber0(szszuzczcdt0(X0))
| X0 = sK0_skl(szszuzczcdt0(X0))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f473,f67]) ).
fof(f1294,definition,
( sQ174_spl
<=> aVector0(xq) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f1296,plain,
( sQ174_spl
| ~ aVector0(xq) ),
inference(component_clause,[status(thm)],[f1294]) ).
fof(f1301,definition,
( sQ176_spl
<=> aVector0(xp) ),
introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition]) ).
fof(f1303,plain,
( sQ176_spl
| ~ aVector0(xp) ),
inference(component_clause,[status(thm)],[f1301]) ).
fof(f1308,plain,
( sQ176_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1303,f162]) ).
fof(f1309,plain,
sQ176_spl,
inference(contradiction_clause,[status(thm)],[f1308]) ).
fof(f1310,plain,
( sQ174_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1296,f164]) ).
fof(f1311,plain,
sQ174_spl,
inference(contradiction_clause,[status(thm)],[f1310]) ).
fof(f1372,definition,
( sQ188_spl
<=> aVector0(xt) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f1374,plain,
( sQ188_spl
| ~ aVector0(xt) ),
inference(component_clause,[status(thm)],[f1372]) ).
fof(f2493,definition,
( sQ373_spl
<=> aDimensionOf0(xt) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ373_spl])],[split_symbol_definition]) ).
fof(f2494,plain,
( ~ sQ373_spl
| aDimensionOf0(xt) = sz00 ),
inference(component_clause,[status(thm)],[f2493]) ).
fof(f2500,plain,
( sQ188_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1374,f157]) ).
fof(f2501,plain,
sQ188_spl,
inference(contradiction_clause,[status(thm)],[f2500]) ).
fof(f2502,plain,
( ~ sQ373_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2494,f370]) ).
fof(f2503,plain,
~ sQ373_spl,
inference(contradiction_clause,[status(thm)],[f2502]) ).
fof(f3875,plain,
( szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
| aDimensionOf0(xt) = sz00
| ~ aVector0(xt) ),
inference(paramodulation,[status(thm)],[f165,f207]) ).
fof(f3876,plain,
( szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
| aDimensionOf0(xs) = sz00
| ~ aVector0(xs) ),
inference(paramodulation,[status(thm)],[f163,f207]) ).
fof(f3877,definition,
( sQ564_spl
<=> szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt) ),
introduced(definition,[new_symbols(definition,[sQ564_spl])],[split_symbol_definition]) ).
fof(f3878,plain,
( ~ sQ564_spl
| szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt) ),
inference(component_clause,[status(thm)],[f3877]) ).
fof(f3880,plain,
( sQ564_spl
| sQ373_spl
| ~ sQ188_spl ),
inference(split_clause,[status(thm)],[f3875,f1372,f2493,f3877]) ).
fof(f3881,definition,
( sQ565_spl
<=> aDimensionOf0(xs) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ565_spl])],[split_symbol_definition]) ).
fof(f3882,plain,
( ~ sQ565_spl
| aDimensionOf0(xs) = sz00 ),
inference(component_clause,[status(thm)],[f3881]) ).
fof(f3884,definition,
( sQ566_spl
<=> szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs) ),
introduced(definition,[new_symbols(definition,[sQ566_spl])],[split_symbol_definition]) ).
fof(f3885,plain,
( ~ sQ566_spl
| szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs) ),
inference(component_clause,[status(thm)],[f3884]) ).
fof(f3887,plain,
( sQ566_spl
| sQ565_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f3876,f372,f3881,f3884]) ).
fof(f3888,plain,
( ~ sQ565_spl
| aDimensionOf0(xt) = sz00 ),
inference(forward_demodulation,[status(thm)],[f160,f3882]) ).
fof(f3889,plain,
( ~ sQ565_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3888,f370]) ).
fof(f3890,plain,
~ sQ565_spl,
inference(contradiction_clause,[status(thm)],[f3889]) ).
fof(f3891,plain,
( ~ sQ566_spl
| szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xt) ),
inference(forward_demodulation,[status(thm)],[f160,f3885]) ).
fof(f4745,plain,
! [X0,X1] :
( sdtlseqdt0(sdtasdt0(sdtasasdt0(X0,X1),sdtasasdt0(X0,X1)),sdtasdt0(sdtasasdt0(X0,X0),sdtasasdt0(X1,X1)))
| ~ iLess0(aDimensionOf0(X0),aDimensionOf0(xt))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X1)
| ~ aVector0(X0) ),
inference(forward_demodulation,[status(thm)],[f160,f159]) ).
fof(f10032,plain,
! [X0] :
( szszuzczcdt0(X0) = sz00
| X0 = sK0_skl(szszuzczcdt0(X0))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f476,f63]) ).
fof(f11454,plain,
( ~ sQ564_spl
| szszuzczcdt0(aDimensionOf0(xq)) = sz00
| aDimensionOf0(xq) = sK0_skl(aDimensionOf0(xt))
| ~ aNaturalNumber0(aDimensionOf0(xq)) ),
inference(paramodulation,[status(thm)],[f3878,f10032]) ).
fof(f11471,definition,
( sQ1243_spl
<=> aNaturalNumber0(aDimensionOf0(xq)) ),
introduced(definition,[new_symbols(definition,[sQ1243_spl])],[split_symbol_definition]) ).
fof(f11473,plain,
( sQ1243_spl
| ~ aNaturalNumber0(aDimensionOf0(xq)) ),
inference(component_clause,[status(thm)],[f11471]) ).
fof(f11474,definition,
( sQ1244_spl
<=> aDimensionOf0(xq) = sK0_skl(aDimensionOf0(xt)) ),
introduced(definition,[new_symbols(definition,[sQ1244_spl])],[split_symbol_definition]) ).
fof(f11475,plain,
( ~ sQ1244_spl
| aDimensionOf0(xq) = sK0_skl(aDimensionOf0(xt)) ),
inference(component_clause,[status(thm)],[f11474]) ).
fof(f11477,definition,
( sQ1245_spl
<=> szszuzczcdt0(aDimensionOf0(xq)) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ1245_spl])],[split_symbol_definition]) ).
fof(f11478,plain,
( ~ sQ1245_spl
| szszuzczcdt0(aDimensionOf0(xq)) = sz00 ),
inference(component_clause,[status(thm)],[f11477]) ).
fof(f11480,plain,
( ~ sQ564_spl
| sQ1245_spl
| sQ1244_spl
| ~ sQ1243_spl ),
inference(split_clause,[status(thm)],[f11454,f11471,f11474,f11477,f3877]) ).
fof(f11492,plain,
( sQ1243_spl
| ~ aVector0(xq) ),
inference(resolution,[status(thm)],[f11473,f134]) ).
fof(f11493,plain,
( sQ1243_spl
| ~ sQ174_spl ),
inference(split_clause,[status(thm)],[f11492,f1294,f11471]) ).
fof(f11496,plain,
( ~ sQ566_spl
| szszuzczcdt0(aDimensionOf0(xp)) = sz00
| aDimensionOf0(xp) = sK0_skl(aDimensionOf0(xt))
| ~ aNaturalNumber0(aDimensionOf0(xp)) ),
inference(paramodulation,[status(thm)],[f3891,f10032]) ).
fof(f11497,plain,
( ~ sQ566_spl
| iLess0(aDimensionOf0(xp),aDimensionOf0(xt))
| ~ aNaturalNumber0(aDimensionOf0(xp)) ),
inference(paramodulation,[status(thm)],[f3891,f74]) ).
fof(f11513,definition,
( sQ1251_spl
<=> aNaturalNumber0(aDimensionOf0(xp)) ),
introduced(definition,[new_symbols(definition,[sQ1251_spl])],[split_symbol_definition]) ).
fof(f11515,plain,
( sQ1251_spl
| ~ aNaturalNumber0(aDimensionOf0(xp)) ),
inference(component_clause,[status(thm)],[f11513]) ).
fof(f11516,definition,
( sQ1252_spl
<=> aDimensionOf0(xp) = sK0_skl(aDimensionOf0(xt)) ),
introduced(definition,[new_symbols(definition,[sQ1252_spl])],[split_symbol_definition]) ).
fof(f11517,plain,
( ~ sQ1252_spl
| aDimensionOf0(xp) = sK0_skl(aDimensionOf0(xt)) ),
inference(component_clause,[status(thm)],[f11516]) ).
fof(f11519,definition,
( sQ1253_spl
<=> szszuzczcdt0(aDimensionOf0(xp)) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ1253_spl])],[split_symbol_definition]) ).
fof(f11520,plain,
( ~ sQ1253_spl
| szszuzczcdt0(aDimensionOf0(xp)) = sz00 ),
inference(component_clause,[status(thm)],[f11519]) ).
fof(f11522,plain,
( ~ sQ566_spl
| sQ1253_spl
| sQ1252_spl
| ~ sQ1251_spl ),
inference(split_clause,[status(thm)],[f11496,f11513,f11516,f11519,f3884]) ).
fof(f11523,definition,
( sQ1254_spl
<=> iLess0(aDimensionOf0(xp),aDimensionOf0(xt)) ),
introduced(definition,[new_symbols(definition,[sQ1254_spl])],[split_symbol_definition]) ).
fof(f11526,plain,
( ~ sQ566_spl
| sQ1254_spl
| ~ sQ1251_spl ),
inference(split_clause,[status(thm)],[f11497,f11513,f11523,f3884]) ).
fof(f11548,plain,
( sQ1251_spl
| ~ aVector0(xp) ),
inference(resolution,[status(thm)],[f11515,f134]) ).
fof(f11549,plain,
( sQ1251_spl
| ~ sQ176_spl ),
inference(split_clause,[status(thm)],[f11548,f1301,f11513]) ).
fof(f11743,plain,
( ~ sQ1245_spl
| ~ sQ564_spl
| aDimensionOf0(xt) = sz00 ),
inference(forward_demodulation,[status(thm)],[f3878,f11478]) ).
fof(f11744,plain,
( ~ sQ1245_spl
| ~ sQ564_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11743,f370]) ).
fof(f11745,plain,
( ~ sQ1245_spl
| ~ sQ564_spl ),
inference(contradiction_clause,[status(thm)],[f11744]) ).
fof(f12653,plain,
( ~ sQ1252_spl
| ~ sQ1244_spl
| aDimensionOf0(xp) = aDimensionOf0(xq) ),
inference(forward_demodulation,[status(thm)],[f11475,f11517]) ).
fof(f12655,plain,
( ~ sQ1252_spl
| ~ sQ1244_spl
| sdtlseqdt0(sdtasdt0(sdtasasdt0(xp,xq),sdtasasdt0(xp,xq)),sdtasdt0(sdtasasdt0(xp,xp),sdtasasdt0(xq,xq)))
| ~ iLess0(aDimensionOf0(xp),aDimensionOf0(xt))
| ~ aVector0(xq)
| ~ aVector0(xp) ),
inference(resolution,[status(thm)],[f12653,f4745]) ).
fof(f12675,definition,
( sQ1328_spl
<=> sdtlseqdt0(sdtasdt0(sdtasasdt0(xp,xq),sdtasasdt0(xp,xq)),sdtasdt0(sdtasasdt0(xp,xp),sdtasasdt0(xq,xq))) ),
introduced(definition,[new_symbols(definition,[sQ1328_spl])],[split_symbol_definition]) ).
fof(f12676,plain,
( ~ sQ1328_spl
| sdtlseqdt0(sdtasdt0(sdtasasdt0(xp,xq),sdtasasdt0(xp,xq)),sdtasdt0(sdtasasdt0(xp,xp),sdtasasdt0(xq,xq))) ),
inference(component_clause,[status(thm)],[f12675]) ).
fof(f12678,plain,
( ~ sQ1252_spl
| ~ sQ1244_spl
| sQ1328_spl
| ~ sQ1254_spl
| ~ sQ174_spl
| ~ sQ176_spl ),
inference(split_clause,[status(thm)],[f12655,f1301,f1294,f11523,f12675,f11474,f11516]) ).
fof(f13217,plain,
( ~ sQ1253_spl
| ~ aNaturalNumber0(aDimensionOf0(xp)) ),
inference(resolution,[status(thm)],[f11520,f64]) ).
fof(f13225,plain,
( ~ sQ1253_spl
| ~ sQ1251_spl ),
inference(split_clause,[status(thm)],[f13217,f11513,f11519]) ).
fof(f13245,plain,
( ~ sQ1328_spl
| sdtlseqdt0(sdtasdt0(xE,sdtasasdt0(xp,xq)),sdtasdt0(sdtasasdt0(xp,xp),sdtasasdt0(xq,xq))) ),
inference(forward_demodulation,[status(thm)],[f175,f12676]) ).
fof(f13246,plain,
( ~ sQ1328_spl
| sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(sdtasasdt0(xp,xp),sdtasasdt0(xq,xq))) ),
inference(forward_demodulation,[status(thm)],[f175,f13245]) ).
fof(f13247,plain,
( ~ sQ1328_spl
| sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,sdtasasdt0(xq,xq))) ),
inference(forward_demodulation,[status(thm)],[f171,f13246]) ).
fof(f13248,plain,
( ~ sQ1328_spl
| sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)) ),
inference(forward_demodulation,[status(thm)],[f173,f13247]) ).
fof(f13249,plain,
( ~ sQ1328_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13248,f190]) ).
fof(f13250,plain,
~ sQ1328_spl,
inference(contradiction_clause,[status(thm)],[f13249]) ).
fof(f13251,plain,
$false,
inference(sat_refutation,[status(thm)],[f380,f1309,f1311,f2501,f2503,f3880,f3887,f3890,f11480,f11493,f11522,f11526,f11549,f11745,f12678,f13225,f13250]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG052+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n009.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 04:15:58 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 38.63/5.36 % Refutation found
% 38.63/5.36 % SZS status Theorem for theBenchmark: Theorem is valid
% 38.63/5.36 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.54/5.91 % Elapsed time: 5.531205 seconds
% 3.54/5.91 % CPU time: 39.775610 seconds
% 3.54/5.91 % Total memory used: 255.196 MB
% 3.54/5.91 % Net memory used: 242.935 MB
%------------------------------------------------------------------------------