%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG081+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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.19s 0.68s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 26
% Syntax : Number of formulae : 112 ( 12 unt; 17 def)
% Number of atoms : 462 ( 116 equ)
% Maximal formula atoms : 34 ( 4 avg)
% Number of connectives : 495 ( 145 ~; 153 |; 168 &)
% ( 17 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 18 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 18 con; 0-2 aty)
% Number of variables : 89 ( 33 !; 56 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [W0,W1,W2,W3] :
( ( aScalar0(W3)
& aScalar0(W2)
& aScalar0(W1)
& aScalar0(W0) )
=> ( ( sdtlseqdt0(W2,W3)
& sdtlseqdt0(sz0z00,W2)
& sdtlseqdt0(W0,W1) )
=> sdtlseqdt0(sdtasdt0(W0,W2),sdtasdt0(W1,W3)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [W0,W1] :
( ( aScalar0(W1)
& aScalar0(W0) )
=> ( sdtlseqdt0(W1,W0)
| sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [W0,W1] :
( ( aVector0(W1)
& aVector0(W0) )
=> ( aDimensionOf0(W0) = aDimensionOf0(W1)
=> aScalar0(sdtasasdt0(W0,W1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [W0,W1] :
( ( aVector0(W1)
& aVector0(W0) )
=> ( ( aDimensionOf0(W1) = sz00
& aDimensionOf0(W0) = aDimensionOf0(W1) )
=> sdtasasdt0(W0,W1) = sz0z00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [W0] :
( aVector0(W0)
=> sdtlseqdt0(sz0z00,sdtasasdt0(W0,W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
( aVector0(xt)
& aVector0(xs) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
aDimensionOf0(xs) = aDimensionOf0(xt),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,conjecture,
( ( aDimensionOf0(xs) != sz00
=> ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( ? [W4] :
( ? [W5] :
( ? [W6] :
( ? [W7] :
( ? [W8] :
( ? [W9] :
( ? [W10] :
( ? [W11] :
( ? [W12] :
( ? [W13] :
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))
& sdtlseqdt0(sdtasdt0(sdtpldt0(W6,W9),sdtpldt0(W6,W9)),sdtasdt0(sdtpldt0(W4,W7),sdtpldt0(W5,W8)))
& sdtlseqdt0(sdtpldt0(W11,W11),sdtpldt0(W10,W12))
& sdtlseqdt0(sdtasdt0(W6,W6),sdtasdt0(W4,W5))
& W13 = sdtasdt0(W10,W12)
& aScalar0(W13) )
& W12 = sdtasdt0(W7,W5)
& aScalar0(W12) )
& W11 = sdtasdt0(W6,W9)
& aScalar0(W11) )
& W10 = sdtasdt0(W4,W8)
& aScalar0(W10) )
& W9 = sdtasdt0(W2,W3)
& aScalar0(W9) )
& W8 = sdtasdt0(W3,W3)
& aScalar0(W8) )
& W7 = sdtasdt0(W2,W2)
& aScalar0(W7) )
& W6 = sdtasasdt0(W0,W1)
& aScalar0(W6) )
& W5 = sdtasasdt0(W1,W1)
& aScalar0(W5) )
& W4 = sdtasasdt0(W0,W0)
& aScalar0(W4) )
& W3 = sdtlbdtrb0(xt,aDimensionOf0(xt))
& aScalar0(W3) )
& W2 = sdtlbdtrb0(xs,aDimensionOf0(xs))
& aScalar0(W2) )
& W1 = sziznziztdt0(xt)
& aVector0(W1) )
& W0 = sziznziztdt0(xs)
& aVector0(W0) ) )
=> sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
~ ( ( aDimensionOf0(xs) != sz00
=> ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( ? [W4] :
( ? [W5] :
( ? [W6] :
( ? [W7] :
( ? [W8] :
( ? [W9] :
( ? [W10] :
( ? [W11] :
( ? [W12] :
( ? [W13] :
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))
& sdtlseqdt0(sdtasdt0(sdtpldt0(W6,W9),sdtpldt0(W6,W9)),sdtasdt0(sdtpldt0(W4,W7),sdtpldt0(W5,W8)))
& sdtlseqdt0(sdtpldt0(W11,W11),sdtpldt0(W10,W12))
& sdtlseqdt0(sdtasdt0(W6,W6),sdtasdt0(W4,W5))
& W13 = sdtasdt0(W10,W12)
& aScalar0(W13) )
& W12 = sdtasdt0(W7,W5)
& aScalar0(W12) )
& W11 = sdtasdt0(W6,W9)
& aScalar0(W11) )
& W10 = sdtasdt0(W4,W8)
& aScalar0(W10) )
& W9 = sdtasdt0(W2,W3)
& aScalar0(W9) )
& W8 = sdtasdt0(W3,W3)
& aScalar0(W8) )
& W7 = sdtasdt0(W2,W2)
& aScalar0(W7) )
& W6 = sdtasasdt0(W0,W1)
& aScalar0(W6) )
& W5 = sdtasasdt0(W1,W1)
& aScalar0(W5) )
& W4 = sdtasasdt0(W0,W0)
& aScalar0(W4) )
& W3 = sdtlbdtrb0(xt,aDimensionOf0(xt))
& aScalar0(W3) )
& W2 = sdtlbdtrb0(xs,aDimensionOf0(xs))
& aScalar0(W2) )
& W1 = sziznziztdt0(xt)
& aVector0(W1) )
& W0 = sziznziztdt0(xs)
& aVector0(W0) ) )
=> sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
inference(negated_conjecture,[status(cth)],[f41]) ).
fof(f63,plain,
aScalar0(sz0z00),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f104,plain,
! [W0,W1,W2,W3] :
( sdtlseqdt0(sdtasdt0(W0,W2),sdtasdt0(W1,W3))
| ~ sdtlseqdt0(W2,W3)
| ~ sdtlseqdt0(sz0z00,W2)
| ~ sdtlseqdt0(W0,W1)
| ~ aScalar0(W3)
| ~ aScalar0(W2)
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f105,plain,
! [X0,X1,X2,X3] :
( sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3))
| ~ sdtlseqdt0(X2,X3)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ aScalar0(X3)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f106,plain,
! [W0,W1] :
( sdtlseqdt0(W1,W0)
| sdtlseqdt0(W0,W1)
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f107,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f133,plain,
! [W0,W1] :
( aScalar0(sdtasasdt0(W0,W1))
| aDimensionOf0(W0) != aDimensionOf0(W1)
| ~ aVector0(W1)
| ~ aVector0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f134,plain,
! [X0,X1] :
( aScalar0(sdtasasdt0(X0,X1))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X1)
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
! [W0,W1] :
( sdtasasdt0(W0,W1) = sz0z00
| aDimensionOf0(W1) != sz00
| aDimensionOf0(W0) != aDimensionOf0(W1)
| ~ aVector0(W1)
| ~ aVector0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f136,plain,
! [X0,X1] :
( sdtasasdt0(X0,X1) = sz0z00
| aDimensionOf0(X1) != sz00
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X1)
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f139,plain,
! [W0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(W0,W0))
| ~ aVector0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f140,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f141,plain,
aVector0(xs),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f142,plain,
aVector0(xt),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f145,plain,
aDimensionOf0(xs) = aDimensionOf0(xt),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f146,plain,
( ~ sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))
& ( ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( ? [W4] :
( ? [W5] :
( ? [W6] :
( ? [W7] :
( ? [W8] :
( ? [W9] :
( ? [W10] :
( ? [W11] :
( ? [W12] :
( ? [W13] :
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))
& sdtlseqdt0(sdtasdt0(sdtpldt0(W6,W9),sdtpldt0(W6,W9)),sdtasdt0(sdtpldt0(W4,W7),sdtpldt0(W5,W8)))
& sdtlseqdt0(sdtpldt0(W11,W11),sdtpldt0(W10,W12))
& sdtlseqdt0(sdtasdt0(W6,W6),sdtasdt0(W4,W5))
& W13 = sdtasdt0(W10,W12)
& aScalar0(W13) )
& W12 = sdtasdt0(W7,W5)
& aScalar0(W12) )
& W11 = sdtasdt0(W6,W9)
& aScalar0(W11) )
& W10 = sdtasdt0(W4,W8)
& aScalar0(W10) )
& W9 = sdtasdt0(W2,W3)
& aScalar0(W9) )
& W8 = sdtasdt0(W3,W3)
& aScalar0(W8) )
& W7 = sdtasdt0(W2,W2)
& aScalar0(W7) )
& W6 = sdtasasdt0(W0,W1)
& aScalar0(W6) )
& W5 = sdtasasdt0(W1,W1)
& aScalar0(W5) )
& W4 = sdtasasdt0(W0,W0)
& aScalar0(W4) )
& W3 = sdtlbdtrb0(xt,aDimensionOf0(xt))
& aScalar0(W3) )
& W2 = sdtlbdtrb0(xs,aDimensionOf0(xs))
& aScalar0(W2) )
& W1 = sziznziztdt0(xt)
& aVector0(W1) )
& W0 = sziznziztdt0(xs)
& aVector0(W0) )
| aDimensionOf0(xs) = sz00 ) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f147,plain,
( ~ sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))
& ( ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( ? [W4] :
( ? [W5] :
( ? [W6] :
( ? [W7] :
( ? [W8] :
( ? [W9] :
( ? [W10] :
( ? [W11] :
( ? [W12] :
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))
& sdtlseqdt0(sdtasdt0(sdtpldt0(W6,W9),sdtpldt0(W6,W9)),sdtasdt0(sdtpldt0(W4,W7),sdtpldt0(W5,W8)))
& sdtlseqdt0(sdtpldt0(W11,W11),sdtpldt0(W10,W12))
& sdtlseqdt0(sdtasdt0(W6,W6),sdtasdt0(W4,W5))
& ? [W13] :
( W13 = sdtasdt0(W10,W12)
& aScalar0(W13) )
& W12 = sdtasdt0(W7,W5)
& aScalar0(W12) )
& W11 = sdtasdt0(W6,W9)
& aScalar0(W11) )
& W10 = sdtasdt0(W4,W8)
& aScalar0(W10) )
& W9 = sdtasdt0(W2,W3)
& aScalar0(W9) )
& W8 = sdtasdt0(W3,W3)
& aScalar0(W8) )
& W7 = sdtasdt0(W2,W2)
& aScalar0(W7) )
& W6 = sdtasasdt0(W0,W1)
& aScalar0(W6) )
& W5 = sdtasasdt0(W1,W1)
& aScalar0(W5) )
& W4 = sdtasasdt0(W0,W0)
& aScalar0(W4) )
& W3 = sdtlbdtrb0(xt,aDimensionOf0(xt))
& aScalar0(W3) )
& W2 = sdtlbdtrb0(xs,aDimensionOf0(xs))
& aScalar0(W2) )
& W1 = sziznziztdt0(xt)
& aVector0(W1) )
& W0 = sziznziztdt0(xs)
& aVector0(W0) )
| aDimensionOf0(xs) = sz00 ) ),
inference(miniscoping,[status(thm)],[f146]) ).
fof(f148,plain,
( ~ sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))
& ( ( sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))
& sdtlseqdt0(sdtasdt0(sdtpldt0(sK8_skl,sK11_skl),sdtpldt0(sK8_skl,sK11_skl)),sdtasdt0(sdtpldt0(sK6_skl,sK9_skl),sdtpldt0(sK7_skl,sK10_skl)))
& sdtlseqdt0(sdtpldt0(sK13_skl,sK13_skl),sdtpldt0(sK12_skl,sK14_skl))
& sdtlseqdt0(sdtasdt0(sK8_skl,sK8_skl),sdtasdt0(sK6_skl,sK7_skl))
& sK15_skl = sdtasdt0(sK12_skl,sK14_skl)
& aScalar0(sK15_skl)
& sK14_skl = sdtasdt0(sK9_skl,sK7_skl)
& aScalar0(sK14_skl)
& sK13_skl = sdtasdt0(sK8_skl,sK11_skl)
& aScalar0(sK13_skl)
& sK12_skl = sdtasdt0(sK6_skl,sK10_skl)
& aScalar0(sK12_skl)
& sK11_skl = sdtasdt0(sK4_skl,sK5_skl)
& aScalar0(sK11_skl)
& sK10_skl = sdtasdt0(sK5_skl,sK5_skl)
& aScalar0(sK10_skl)
& sK9_skl = sdtasdt0(sK4_skl,sK4_skl)
& aScalar0(sK9_skl)
& sK8_skl = sdtasasdt0(sK2_skl,sK3_skl)
& aScalar0(sK8_skl)
& sK7_skl = sdtasasdt0(sK3_skl,sK3_skl)
& aScalar0(sK7_skl)
& sK6_skl = sdtasasdt0(sK2_skl,sK2_skl)
& aScalar0(sK6_skl)
& sK5_skl = sdtlbdtrb0(xt,aDimensionOf0(xt))
& aScalar0(sK5_skl)
& sK4_skl = sdtlbdtrb0(xs,aDimensionOf0(xs))
& aScalar0(sK4_skl)
& sK3_skl = sziznziztdt0(xt)
& aVector0(sK3_skl)
& sK2_skl = sziznziztdt0(xs)
& aVector0(sK2_skl) )
| aDimensionOf0(xs) = sz00 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl]),skolemize(W0,sK2_skl),skolemize(W1,sK3_skl),skolemize(W2,sK4_skl),skolemize(W3,sK5_skl),skolemize(W4,sK6_skl),skolemize(W5,sK7_skl),skolemize(W6,sK8_skl),skolemize(W7,sK9_skl),skolemize(W8,sK10_skl),skolemize(W9,sK11_skl),skolemize(W10,sK12_skl),skolemize(W11,sK13_skl),skolemize(W12,sK14_skl),skolemize(W13,sK15_skl)],[f147]) ).
fof(f180,plain,
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))
| aDimensionOf0(xs) = sz00 ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f181,plain,
~ sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f197,definition,
( sQ4_spl
<=> aDimensionOf0(xs) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f198,plain,
( ~ sQ4_spl
| aDimensionOf0(xs) = sz00 ),
inference(component_clause,[status(thm)],[f197]) ).
fof(f324,definition,
( sQ36_spl
<=> sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f325,plain,
( ~ sQ36_spl
| sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
inference(component_clause,[status(thm)],[f324]) ).
fof(f327,plain,
( sQ36_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f180,f197,f324]) ).
fof(f330,plain,
( ~ sQ4_spl
| sz00 = aDimensionOf0(xt) ),
inference(forward_demodulation,[status(thm)],[f198,f145]) ).
fof(f332,definition,
( sQ37_spl
<=> aScalar0(sz0z00) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f334,plain,
( sQ37_spl
| ~ aScalar0(sz0z00) ),
inference(component_clause,[status(thm)],[f332]) ).
fof(f358,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f334,f63]) ).
fof(f359,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f358]) ).
fof(f364,definition,
( sQ42_spl
<=> aVector0(xt) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f366,plain,
( sQ42_spl
| ~ aVector0(xt) ),
inference(component_clause,[status(thm)],[f364]) ).
fof(f368,definition,
( sQ43_spl
<=> aVector0(xs) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f370,plain,
( sQ43_spl
| ~ aVector0(xs) ),
inference(component_clause,[status(thm)],[f368]) ).
fof(f372,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f366,f142]) ).
fof(f373,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f372]) ).
fof(f374,plain,
( ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f325,f181]) ).
fof(f375,plain,
~ sQ36_spl,
inference(contradiction_clause,[status(thm)],[f374]) ).
fof(f431,definition,
( sQ50_spl
<=> aScalar0(sdtasasdt0(xs,xt)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f433,plain,
( sQ50_spl
| ~ aScalar0(sdtasasdt0(xs,xt)) ),
inference(component_clause,[status(thm)],[f431]) ).
fof(f436,definition,
( sQ51_spl
<=> aScalar0(sdtasasdt0(xs,xs)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f438,plain,
( sQ51_spl
| ~ aScalar0(sdtasasdt0(xs,xs)) ),
inference(component_clause,[status(thm)],[f436]) ).
fof(f439,definition,
( sQ52_spl
<=> aScalar0(sdtasasdt0(xt,xt)) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f441,plain,
( sQ52_spl
| ~ aScalar0(sdtasasdt0(xt,xt)) ),
inference(component_clause,[status(thm)],[f439]) ).
fof(f487,plain,
( ~ sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xt,xt))
| ~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xt))
| ~ sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xs))
| ~ aScalar0(sdtasasdt0(xt,xt))
| ~ aScalar0(sdtasasdt0(xs,xt))
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ aScalar0(sdtasasdt0(xs,xt)) ),
inference(resolution,[status(thm)],[f105,f181]) ).
fof(f490,definition,
( sQ61_spl
<=> sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xs)) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f492,plain,
( sQ61_spl
| ~ sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xs)) ),
inference(component_clause,[status(thm)],[f490]) ).
fof(f493,definition,
( sQ62_spl
<=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xt)) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f495,plain,
( sQ62_spl
| ~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xt)) ),
inference(component_clause,[status(thm)],[f493]) ).
fof(f496,definition,
( sQ63_spl
<=> sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xt,xt)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f498,plain,
( sQ63_spl
| ~ sdtlseqdt0(sdtasasdt0(xs,xt),sdtasasdt0(xt,xt)) ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f499,plain,
( ~ sQ63_spl
| ~ sQ62_spl
| ~ sQ61_spl
| ~ sQ52_spl
| ~ sQ51_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f487,f431,f436,f439,f490,f493,f496]) ).
fof(f519,plain,
( sQ62_spl
| sdtlseqdt0(sdtasasdt0(xs,xt),sz0z00)
| ~ aScalar0(sz0z00)
| ~ aScalar0(sdtasasdt0(xs,xt)) ),
inference(resolution,[status(thm)],[f495,f107]) ).
fof(f521,definition,
( sQ67_spl
<=> sdtlseqdt0(sdtasasdt0(xs,xt),sz0z00) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f522,plain,
( ~ sQ67_spl
| sdtlseqdt0(sdtasasdt0(xs,xt),sz0z00) ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f524,plain,
( sQ62_spl
| sQ67_spl
| ~ sQ37_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f519,f431,f332,f521,f493]) ).
fof(f541,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f370,f141]) ).
fof(f542,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f541]) ).
fof(f543,plain,
( sQ52_spl
| aDimensionOf0(xt) != aDimensionOf0(xt)
| ~ aVector0(xt)
| ~ aVector0(xt) ),
inference(resolution,[status(thm)],[f134,f441]) ).
fof(f544,plain,
( sQ51_spl
| aDimensionOf0(xs) != aDimensionOf0(xs)
| ~ aVector0(xs)
| ~ aVector0(xs) ),
inference(resolution,[status(thm)],[f134,f438]) ).
fof(f545,plain,
( sQ50_spl
| aDimensionOf0(xs) != aDimensionOf0(xt)
| ~ aVector0(xt)
| ~ aVector0(xs) ),
inference(resolution,[status(thm)],[f134,f433]) ).
fof(f546,definition,
( sQ71_spl
<=> aDimensionOf0(xt) = aDimensionOf0(xt) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f548,plain,
( sQ71_spl
| aDimensionOf0(xt) != aDimensionOf0(xt) ),
inference(component_clause,[status(thm)],[f546]) ).
fof(f549,plain,
( sQ52_spl
| ~ sQ71_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f543,f364,f546,f439]) ).
fof(f550,definition,
( sQ72_spl
<=> aDimensionOf0(xs) = aDimensionOf0(xs) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f552,plain,
( sQ72_spl
| aDimensionOf0(xs) != aDimensionOf0(xs) ),
inference(component_clause,[status(thm)],[f550]) ).
fof(f553,plain,
( sQ51_spl
| ~ sQ72_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f544,f368,f550,f436]) ).
fof(f554,definition,
( sQ73_spl
<=> aDimensionOf0(xs) = aDimensionOf0(xt) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f556,plain,
( sQ73_spl
| aDimensionOf0(xs) != aDimensionOf0(xt) ),
inference(component_clause,[status(thm)],[f554]) ).
fof(f557,plain,
( sQ50_spl
| ~ sQ73_spl
| ~ sQ42_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f545,f368,f364,f554,f431]) ).
fof(f558,plain,
( sQ71_spl
| ~ sQ4_spl
| sz00 != aDimensionOf0(xt) ),
inference(forward_demodulation,[status(thm)],[f330,f548]) ).
fof(f559,plain,
( sQ71_spl
| ~ sQ4_spl
| sz00 != sz00 ),
inference(forward_demodulation,[status(thm)],[f330,f558]) ).
fof(f560,plain,
( sQ71_spl
| ~ sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f559]) ).
fof(f561,plain,
( sQ71_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f560]) ).
fof(f562,plain,
( sQ72_spl
| ~ sQ4_spl
| sz00 != aDimensionOf0(xs) ),
inference(forward_demodulation,[status(thm)],[f198,f552]) ).
fof(f563,plain,
( sQ72_spl
| ~ sQ4_spl
| sz00 != sz00 ),
inference(forward_demodulation,[status(thm)],[f198,f562]) ).
fof(f564,plain,
( sQ72_spl
| ~ sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f563]) ).
fof(f565,plain,
( sQ72_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f564]) ).
fof(f566,plain,
( sQ73_spl
| ~ sQ4_spl
| sz00 != aDimensionOf0(xt) ),
inference(forward_demodulation,[status(thm)],[f198,f556]) ).
fof(f567,plain,
( sQ73_spl
| ~ sQ4_spl
| sz00 != sz00 ),
inference(forward_demodulation,[status(thm)],[f330,f566]) ).
fof(f568,plain,
( sQ73_spl
| ~ sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f567]) ).
fof(f569,plain,
( sQ73_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f568]) ).
fof(f599,definition,
( sQ77_spl
<=> sz0z00 = sdtasasdt0(xs,xt) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f600,plain,
( ~ sQ77_spl
| sz0z00 = sdtasasdt0(xs,xt) ),
inference(component_clause,[status(thm)],[f599]) ).
fof(f601,plain,
( sQ77_spl
| sz0z00 != sdtasasdt0(xs,xt) ),
inference(component_clause,[status(thm)],[f599]) ).
fof(f603,plain,
( ~ sQ67_spl
| ~ sQ77_spl
| sdtlseqdt0(sz0z00,sz0z00) ),
inference(backward_demodulation,[status(thm)],[f600,f522]) ).
fof(f609,definition,
( sQ78_spl
<=> aDimensionOf0(xt) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f611,plain,
( sQ78_spl
| aDimensionOf0(xt) != sz00 ),
inference(component_clause,[status(thm)],[f609]) ).
fof(f614,plain,
( sQ78_spl
| ~ sQ4_spl
| sz00 != sz00 ),
inference(forward_demodulation,[status(thm)],[f330,f611]) ).
fof(f615,plain,
( sQ78_spl
| ~ sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f614]) ).
fof(f616,plain,
( sQ78_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f615]) ).
fof(f649,plain,
( sQ63_spl
| ~ sQ77_spl
| ~ sdtlseqdt0(sz0z00,sdtasasdt0(xt,xt)) ),
inference(forward_demodulation,[status(thm)],[f600,f498]) ).
fof(f650,plain,
( sQ63_spl
| ~ sQ77_spl
| ~ aVector0(xt) ),
inference(resolution,[status(thm)],[f649,f140]) ).
fof(f653,plain,
( sQ63_spl
| ~ sQ77_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f650,f364,f599,f496]) ).
fof(f662,plain,
( sQ61_spl
| ~ sQ77_spl
| ~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ),
inference(forward_demodulation,[status(thm)],[f600,f492]) ).
fof(f844,plain,
( sQ61_spl
| ~ sQ77_spl
| ~ aVector0(xs) ),
inference(resolution,[status(thm)],[f662,f140]) ).
fof(f848,plain,
( sQ61_spl
| ~ sQ77_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f844,f368,f599,f490]) ).
fof(f862,plain,
( sQ62_spl
| ~ sQ77_spl
| ~ sdtlseqdt0(sz0z00,sz0z00) ),
inference(forward_demodulation,[status(thm)],[f600,f495]) ).
fof(f863,plain,
( sQ62_spl
| ~ sQ77_spl
| ~ sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f862,f603]) ).
fof(f864,plain,
( sQ62_spl
| ~ sQ77_spl
| ~ sQ67_spl ),
inference(contradiction_clause,[status(thm)],[f863]) ).
fof(f865,plain,
( sQ77_spl
| aDimensionOf0(xt) != sz00
| aDimensionOf0(xs) != aDimensionOf0(xt)
| ~ aVector0(xt)
| ~ aVector0(xs) ),
inference(resolution,[status(thm)],[f601,f136]) ).
fof(f866,plain,
( sQ77_spl
| ~ sQ78_spl
| ~ sQ73_spl
| ~ sQ42_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f865,f368,f364,f554,f609,f599]) ).
fof(f867,plain,
$false,
inference(sat_refutation,[status(thm)],[f327,f359,f373,f375,f499,f524,f542,f549,f553,f557,f561,f565,f569,f616,f653,f848,f864,f866]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG081+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.46 % Computer : n017.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Mon Sep 21 04:13:57 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.51 % Drodi V4.1.1
% 0.19/0.68 % Refutation found
% 0.19/0.68 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/0.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.24/0.72 % Elapsed time: 0.229645 seconds
% 0.24/0.72 % CPU time: 1.095814 seconds
% 0.24/0.72 % Total memory used: 110.318 MB
% 0.24/0.72 % Net memory used: 109.576 MB
%------------------------------------------------------------------------------