%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG052+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 : n016.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 60.99s 8.10s
% Output : CNFRefutation 33.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 27
% Syntax : Number of formulae : 97 ( 23 unt; 14 def)
% Number of atoms : 280 ( 97 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 291 ( 108 ~; 121 |; 35 &)
% ( 15 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 14 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-2 aty)
% Number of variables : 50 ( 48 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> iLess0(W0,szszuzczcdt0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [W0] :
( aVector0(W0)
=> aNaturalNumber0(aDimensionOf0(W0)) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [W0,W1] :
( ( aVector0(W1)
& aVector0(W0) )
=> ( ( aDimensionOf0(W1) != sz00
& aDimensionOf0(W0) = aDimensionOf0(W1) )
=> aDimensionOf0(sziznziztdt0(W0)) = aDimensionOf0(sziznziztdt0(W1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
( aVector0(xt)
& aVector0(xs) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
aDimensionOf0(xs) = aDimensionOf0(xt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
aDimensionOf0(xs) != sz00,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
( xp = sziznziztdt0(xs)
& ! [W0] :
( aNaturalNumber0(W0)
=> sdtlbdtrb0(xp,W0) = sdtlbdtrb0(xs,W0) )
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& aVector0(xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,hypothesis,
( xq = sziznziztdt0(xt)
& ! [W0] :
( aNaturalNumber0(W0)
=> sdtlbdtrb0(xq,W0) = sdtlbdtrb0(xt,W0) )
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& aVector0(xq) ),
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(f56,conjecture,
sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,negated_conjecture,
~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(negated_conjecture,[status(cth)],[f56]) ).
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(f141,plain,
! [X0,X1] :
( aVector0(X1)
| X1 != sziznziztdt0(X0)
| aDimensionOf0(X0) = sz00
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f146,plain,
! [W0,W1] :
( aDimensionOf0(sziznziztdt0(W0)) = aDimensionOf0(sziznziztdt0(W1))
| aDimensionOf0(W1) = sz00
| aDimensionOf0(W0) != aDimensionOf0(W1)
| ~ aVector0(W1)
| ~ aVector0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f147,plain,
! [X0,X1] :
( aDimensionOf0(sziznziztdt0(X0)) = aDimensionOf0(sziznziztdt0(X1))
| aDimensionOf0(X1) = sz00
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X1)
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
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,
( xp = sziznziztdt0(xs)
& ! [W0] :
( sdtlbdtrb0(xp,W0) = sdtlbdtrb0(xs,W0)
| ~ aNaturalNumber0(W0) )
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& aVector0(xp) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f163,plain,
aVector0(xp),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f164,plain,
szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f166,plain,
xp = sziznziztdt0(xs),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f167,plain,
( xq = sziznziztdt0(xt)
& ! [W0] :
( sdtlbdtrb0(xq,W0) = sdtlbdtrb0(xt,W0)
| ~ aNaturalNumber0(W0) )
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& aVector0(xq) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f171,plain,
xq = sziznziztdt0(xt),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f177,plain,
xC = sdtasasdt0(xp,xp),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f179,plain,
xD = sdtasasdt0(xq,xq),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f181,plain,
xE = sdtasasdt0(xp,xq),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f196,plain,
~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f1290,definition,
( sQ105_spl
<=> aVector0(xt) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1292,plain,
( sQ105_spl
| ~ aVector0(xt) ),
inference(component_clause,[status(thm)],[f1290]) ).
fof(f1297,plain,
( sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1292,f157]) ).
fof(f1298,plain,
sQ105_spl,
inference(contradiction_clause,[status(thm)],[f1297]) ).
fof(f2758,plain,
( aVector0(xq)
| aDimensionOf0(xt) = sz00
| ~ aVector0(xt) ),
inference(resolution,[status(thm)],[f141,f171]) ).
fof(f2759,plain,
( aVector0(xp)
| aDimensionOf0(xs) = sz00
| ~ aVector0(xs) ),
inference(resolution,[status(thm)],[f141,f166]) ).
fof(f2767,definition,
( sQ319_spl
<=> aDimensionOf0(xt) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ319_spl])],[split_symbol_definition]) ).
fof(f2768,plain,
( ~ sQ319_spl
| aDimensionOf0(xt) = sz00 ),
inference(component_clause,[status(thm)],[f2767]) ).
fof(f2770,definition,
( sQ320_spl
<=> aVector0(xq) ),
introduced(definition,[new_symbols(definition,[sQ320_spl])],[split_symbol_definition]) ).
fof(f2773,plain,
( sQ320_spl
| sQ319_spl
| ~ sQ105_spl ),
inference(split_clause,[status(thm)],[f2758,f1290,f2767,f2770]) ).
fof(f2774,definition,
( sQ321_spl
<=> aVector0(xs) ),
introduced(definition,[new_symbols(definition,[sQ321_spl])],[split_symbol_definition]) ).
fof(f2776,plain,
( sQ321_spl
| ~ aVector0(xs) ),
inference(component_clause,[status(thm)],[f2774]) ).
fof(f2777,definition,
( sQ322_spl
<=> aDimensionOf0(xs) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ322_spl])],[split_symbol_definition]) ).
fof(f2778,plain,
( ~ sQ322_spl
| aDimensionOf0(xs) = sz00 ),
inference(component_clause,[status(thm)],[f2777]) ).
fof(f2780,definition,
( sQ323_spl
<=> aVector0(xp) ),
introduced(definition,[new_symbols(definition,[sQ323_spl])],[split_symbol_definition]) ).
fof(f2783,plain,
( sQ323_spl
| sQ322_spl
| ~ sQ321_spl ),
inference(split_clause,[status(thm)],[f2759,f2774,f2777,f2780]) ).
fof(f2792,plain,
( ~ sQ322_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2778,f161]) ).
fof(f2793,plain,
~ sQ322_spl,
inference(contradiction_clause,[status(thm)],[f2792]) ).
fof(f2794,plain,
( sQ321_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2776,f156]) ).
fof(f2795,plain,
sQ321_spl,
inference(contradiction_clause,[status(thm)],[f2794]) ).
fof(f3202,plain,
( ~ sQ319_spl
| aDimensionOf0(xs) = sz00 ),
inference(backward_demodulation,[status(thm)],[f2768,f160]) ).
fof(f3206,plain,
( ~ sQ319_spl
| sQ322_spl ),
inference(split_clause,[status(thm)],[f3202,f2777,f2767]) ).
fof(f3293,plain,
! [X0] :
( aDimensionOf0(xq) = aDimensionOf0(sziznziztdt0(X0))
| aDimensionOf0(X0) = sz00
| aDimensionOf0(xt) != aDimensionOf0(X0)
| ~ aVector0(X0)
| ~ aVector0(xt) ),
inference(paramodulation,[status(thm)],[f171,f147]) ).
fof(f3297,definition,
! [X0] :
( sQ385_spl
<=> ( aDimensionOf0(xq) = aDimensionOf0(sziznziztdt0(X0))
| aDimensionOf0(X0) = sz00
| aDimensionOf0(xt) != aDimensionOf0(X0)
| ~ aVector0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ385_spl])],[split_symbol_definition]) ).
fof(f3298,plain,
! [X0] :
( ~ sQ385_spl
| aDimensionOf0(xq) = aDimensionOf0(sziznziztdt0(X0))
| aDimensionOf0(X0) = sz00
| aDimensionOf0(xt) != aDimensionOf0(X0)
| ~ aVector0(X0) ),
inference(component_clause,[status(thm)],[f3297]) ).
fof(f3300,plain,
( sQ385_spl
| ~ sQ105_spl ),
inference(split_clause,[status(thm)],[f3293,f1290,f3297]) ).
fof(f3320,definition,
( sQ390_spl
<=> aDimensionOf0(xp) = aDimensionOf0(xq) ),
introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition]) ).
fof(f3906,plain,
! [X0] :
( sdtlseqdt0(sdtasdt0(sdtasasdt0(X0,xq),sdtasasdt0(X0,xq)),sdtasdt0(sdtasasdt0(X0,X0),xD))
| ~ iLess0(aDimensionOf0(X0),aDimensionOf0(xs))
| aDimensionOf0(X0) != aDimensionOf0(xq)
| ~ aVector0(xq)
| ~ aVector0(X0) ),
inference(paramodulation,[status(thm)],[f179,f159]) ).
fof(f3916,definition,
( sQ477_spl
<=> iLess0(aDimensionOf0(xp),aDimensionOf0(xs)) ),
introduced(definition,[new_symbols(definition,[sQ477_spl])],[split_symbol_definition]) ).
fof(f3935,definition,
! [X0] :
( sQ482_spl
<=> ( sdtlseqdt0(sdtasdt0(sdtasasdt0(X0,xq),sdtasasdt0(X0,xq)),sdtasdt0(sdtasasdt0(X0,X0),xD))
| ~ iLess0(aDimensionOf0(X0),aDimensionOf0(xs))
| aDimensionOf0(X0) != aDimensionOf0(xq)
| ~ aVector0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ482_spl])],[split_symbol_definition]) ).
fof(f3936,plain,
! [X0] :
( ~ sQ482_spl
| sdtlseqdt0(sdtasdt0(sdtasasdt0(X0,xq),sdtasasdt0(X0,xq)),sdtasdt0(sdtasasdt0(X0,X0),xD))
| ~ iLess0(aDimensionOf0(X0),aDimensionOf0(xs))
| aDimensionOf0(X0) != aDimensionOf0(xq)
| ~ aVector0(X0) ),
inference(component_clause,[status(thm)],[f3935]) ).
fof(f3938,plain,
( ~ sQ320_spl
| sQ482_spl ),
inference(split_clause,[status(thm)],[f3906,f3935,f2770]) ).
fof(f3947,plain,
( iLess0(aDimensionOf0(xp),aDimensionOf0(xs))
| ~ aNaturalNumber0(aDimensionOf0(xp)) ),
inference(paramodulation,[status(thm)],[f164,f74]) ).
fof(f3963,definition,
( sQ486_spl
<=> aNaturalNumber0(aDimensionOf0(xp)) ),
introduced(definition,[new_symbols(definition,[sQ486_spl])],[split_symbol_definition]) ).
fof(f3965,plain,
( sQ486_spl
| ~ aNaturalNumber0(aDimensionOf0(xp)) ),
inference(component_clause,[status(thm)],[f3963]) ).
fof(f3966,plain,
( sQ477_spl
| ~ sQ486_spl ),
inference(split_clause,[status(thm)],[f3947,f3963,f3916]) ).
fof(f5216,plain,
( sQ486_spl
| ~ aVector0(xp) ),
inference(resolution,[status(thm)],[f3965,f134]) ).
fof(f5217,plain,
( sQ486_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5216,f163]) ).
fof(f5218,plain,
sQ486_spl,
inference(contradiction_clause,[status(thm)],[f5217]) ).
fof(f9104,plain,
( ~ sQ482_spl
| sdtlseqdt0(sdtasdt0(xE,sdtasasdt0(xp,xq)),sdtasdt0(sdtasasdt0(xp,xp),xD))
| ~ iLess0(aDimensionOf0(xp),aDimensionOf0(xs))
| aDimensionOf0(xp) != aDimensionOf0(xq)
| ~ aVector0(xp) ),
inference(paramodulation,[status(thm)],[f181,f3936]) ).
fof(f9126,definition,
( sQ1089_spl
<=> sdtlseqdt0(sdtasdt0(xE,sdtasasdt0(xp,xq)),sdtasdt0(sdtasasdt0(xp,xp),xD)) ),
introduced(definition,[new_symbols(definition,[sQ1089_spl])],[split_symbol_definition]) ).
fof(f9127,plain,
( ~ sQ1089_spl
| sdtlseqdt0(sdtasdt0(xE,sdtasasdt0(xp,xq)),sdtasdt0(sdtasasdt0(xp,xp),xD)) ),
inference(component_clause,[status(thm)],[f9126]) ).
fof(f9129,plain,
( ~ sQ482_spl
| sQ1089_spl
| ~ sQ477_spl
| ~ sQ390_spl
| ~ sQ323_spl ),
inference(split_clause,[status(thm)],[f9104,f2780,f3320,f3916,f9126,f3935]) ).
fof(f9161,plain,
( ~ sQ1089_spl
| sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(sdtasasdt0(xp,xp),xD)) ),
inference(forward_demodulation,[status(thm)],[f181,f9127]) ).
fof(f9162,plain,
( ~ sQ1089_spl
| sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)) ),
inference(forward_demodulation,[status(thm)],[f177,f9161]) ).
fof(f9163,plain,
( ~ sQ1089_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9162,f196]) ).
fof(f9164,plain,
~ sQ1089_spl,
inference(contradiction_clause,[status(thm)],[f9163]) ).
fof(f16451,plain,
! [X0] :
( ~ sQ385_spl
| aDimensionOf0(xq) = aDimensionOf0(sziznziztdt0(X0))
| aDimensionOf0(X0) = sz00
| aDimensionOf0(xs) != aDimensionOf0(X0)
| ~ aVector0(X0) ),
inference(forward_demodulation,[status(thm)],[f160,f3298]) ).
fof(f16453,plain,
( ~ sQ385_spl
| aDimensionOf0(xq) = aDimensionOf0(xp)
| aDimensionOf0(xs) = sz00
| aDimensionOf0(xs) != aDimensionOf0(xs)
| ~ aVector0(xs) ),
inference(paramodulation,[status(thm)],[f166,f16451]) ).
fof(f16458,definition,
( sQ2050_spl
<=> aDimensionOf0(xs) = aDimensionOf0(xs) ),
introduced(definition,[new_symbols(definition,[sQ2050_spl])],[split_symbol_definition]) ).
fof(f16460,plain,
( sQ2050_spl
| aDimensionOf0(xs) != aDimensionOf0(xs) ),
inference(component_clause,[status(thm)],[f16458]) ).
fof(f16461,plain,
( ~ sQ385_spl
| sQ390_spl
| sQ322_spl
| ~ sQ2050_spl
| ~ sQ321_spl ),
inference(split_clause,[status(thm)],[f16453,f2774,f16458,f2777,f3320,f3297]) ).
fof(f16462,plain,
( sQ2050_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f16460]) ).
fof(f16463,plain,
sQ2050_spl,
inference(contradiction_clause,[status(thm)],[f16462]) ).
fof(f16464,plain,
$false,
inference(sat_refutation,[status(thm)],[f1298,f2773,f2783,f2793,f2795,f3206,f3300,f3938,f3966,f5218,f9129,f9164,f16461,f16463]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG052+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n016.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:20:22 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 60.99/8.10 % Refutation found
% 60.99/8.10 % SZS status Theorem for theBenchmark: Theorem is valid
% 60.99/8.10 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 33.93/8.16 % Elapsed time: 7.787869 seconds
% 33.93/8.16 % CPU time: 61.513705 seconds
% 33.93/8.16 % Total memory used: 331.984 MB
% 33.93/8.16 % Net memory used: 313.533 MB
%------------------------------------------------------------------------------