%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG081+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 : n006.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:54 PM UTC 2026
% Result : Theorem 0.12s 0.45s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 22
% Syntax : Number of formulae : 95 ( 12 unt; 14 def)
% Number of atoms : 452 ( 139 equ)
% Maximal formula atoms : 40 ( 4 avg)
% Number of connectives : 500 ( 143 ~; 141 |; 187 &)
% ( 14 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 53 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 15 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 18 con; 0-2 aty)
% Number of variables : 96 ( 40 !; 56 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [W0,W1] :
( ( aVector0(W1)
& aVector0(W0) )
=> ( aDimensionOf0(W0) = aDimensionOf0(W1)
=> aScalar0(sdtasasdt0(W0,W1)) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [W0] :
( aVector0(W0)
=> sdtlseqdt0(sz0z00,sdtasasdt0(W0,W0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
( aVector0(xt)
& aVector0(xs) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
aDimensionOf0(xs) = aDimensionOf0(xt),
file('/export/starexec/sandbox2/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)
& ! [W2] :
( aNaturalNumber0(W2)
=> sdtlbdtrb0(W1,W2) = sdtlbdtrb0(xt,W2) )
& szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(xt)
& aVector0(W1) )
& W0 = sziznziztdt0(xs)
& ! [W1] :
( aNaturalNumber0(W1)
=> sdtlbdtrb0(W0,W1) = sdtlbdtrb0(xs,W1) )
& szszuzczcdt0(aDimensionOf0(W0)) = aDimensionOf0(xs)
& aVector0(W0) ) )
=> sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
file('/export/starexec/sandbox2/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)
& ! [W2] :
( aNaturalNumber0(W2)
=> sdtlbdtrb0(W1,W2) = sdtlbdtrb0(xt,W2) )
& szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(xt)
& aVector0(W1) )
& W0 = sziznziztdt0(xs)
& ! [W1] :
( aNaturalNumber0(W1)
=> sdtlbdtrb0(W0,W1) = sdtlbdtrb0(xs,W1) )
& szszuzczcdt0(aDimensionOf0(W0)) = aDimensionOf0(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(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)
& ! [W2] :
( sdtlbdtrb0(W1,W2) = sdtlbdtrb0(xt,W2)
| ~ aNaturalNumber0(W2) )
& szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(xt)
& aVector0(W1) )
& W0 = sziznziztdt0(xs)
& ! [W1] :
( sdtlbdtrb0(W0,W1) = sdtlbdtrb0(xs,W1)
| ~ aNaturalNumber0(W1) )
& szszuzczcdt0(aDimensionOf0(W0)) = aDimensionOf0(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)
& ! [W2] :
( sdtlbdtrb0(W1,W2) = sdtlbdtrb0(xt,W2)
| ~ aNaturalNumber0(W2) )
& szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(xt)
& aVector0(W1) )
& W0 = sziznziztdt0(xs)
& ! [W1] :
( sdtlbdtrb0(W0,W1) = sdtlbdtrb0(xs,W1)
| ~ aNaturalNumber0(W1) )
& szszuzczcdt0(aDimensionOf0(W0)) = aDimensionOf0(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)
& ! [W2] :
( sdtlbdtrb0(sK3_skl,W2) = sdtlbdtrb0(xt,W2)
| ~ aNaturalNumber0(W2) )
& szszuzczcdt0(aDimensionOf0(sK3_skl)) = aDimensionOf0(xt)
& aVector0(sK3_skl)
& sK2_skl = sziznziztdt0(xs)
& ! [W1] :
( sdtlbdtrb0(sK2_skl,W1) = sdtlbdtrb0(xs,W1)
| ~ aNaturalNumber0(W1) )
& szszuzczcdt0(aDimensionOf0(sK2_skl)) = aDimensionOf0(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(f184,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(f185,plain,
~ sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f201,definition,
( sQ4_spl
<=> aDimensionOf0(xs) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f202,plain,
( ~ sQ4_spl
| aDimensionOf0(xs) = sz00 ),
inference(component_clause,[status(thm)],[f201]) ).
fof(f344,definition,
( sQ40_spl
<=> sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f345,plain,
( ~ sQ40_spl
| sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
inference(component_clause,[status(thm)],[f344]) ).
fof(f347,plain,
( sQ40_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f184,f201,f344]) ).
fof(f352,definition,
( sQ41_spl
<=> aVector0(xs) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f354,plain,
( sQ41_spl
| ~ aVector0(xs) ),
inference(component_clause,[status(thm)],[f352]) ).
fof(f359,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f354,f141]) ).
fof(f360,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f359]) ).
fof(f361,plain,
( ~ sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f345,f185]) ).
fof(f362,plain,
~ sQ40_spl,
inference(contradiction_clause,[status(thm)],[f361]) ).
fof(f365,plain,
( ~ sQ4_spl
| sz00 = aDimensionOf0(xt) ),
inference(forward_demodulation,[status(thm)],[f202,f145]) ).
fof(f367,definition,
( sQ43_spl
<=> aVector0(xt) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f369,plain,
( sQ43_spl
| ~ aVector0(xt) ),
inference(component_clause,[status(thm)],[f367]) ).
fof(f397,definition,
( sQ49_spl
<=> aScalar0(sz0z00) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f399,plain,
( sQ49_spl
| ~ aScalar0(sz0z00) ),
inference(component_clause,[status(thm)],[f397]) ).
fof(f421,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f399,f63]) ).
fof(f422,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f421]) ).
fof(f438,plain,
( sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f369,f142]) ).
fof(f439,plain,
sQ43_spl,
inference(contradiction_clause,[status(thm)],[f438]) ).
fof(f448,plain,
! [X0] :
( ~ sQ4_spl
| aScalar0(sdtasasdt0(xs,X0))
| sz00 != aDimensionOf0(X0)
| ~ aVector0(X0)
| ~ aVector0(xs) ),
inference(paramodulation,[status(thm)],[f202,f134]) ).
fof(f456,definition,
! [X0] :
( sQ57_spl
<=> ( aScalar0(sdtasasdt0(xs,X0))
| sz00 != aDimensionOf0(X0)
| ~ aVector0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f457,plain,
! [X0] :
( ~ sQ57_spl
| aScalar0(sdtasasdt0(xs,X0))
| sz00 != aDimensionOf0(X0)
| ~ aVector0(X0) ),
inference(component_clause,[status(thm)],[f456]) ).
fof(f459,plain,
( ~ sQ4_spl
| sQ57_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f448,f352,f456,f201]) ).
fof(f502,plain,
( ~ sQ4_spl
| ~ sQ57_spl
| aScalar0(sdtasasdt0(xs,xs))
| ~ aVector0(xs) ),
inference(resolution,[status(thm)],[f457,f202]) ).
fof(f510,definition,
( sQ65_spl
<=> aScalar0(sdtasasdt0(xs,xs)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f513,plain,
( ~ sQ4_spl
| ~ sQ57_spl
| sQ65_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f502,f352,f510,f456,f201]) ).
fof(f760,definition,
( sQ89_spl
<=> sdtlseqdt0(sz0z00,sz0z00) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f949,definition,
( sQ112_spl
<=> sdtasasdt0(xt,xt) = sdtasasdt0(xs,xt) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f950,plain,
( ~ sQ112_spl
| sdtasasdt0(xt,xt) = sdtasasdt0(xs,xt) ),
inference(component_clause,[status(thm)],[f949]) ).
fof(f951,plain,
( sQ112_spl
| sdtasasdt0(xt,xt) != sdtasasdt0(xs,xt) ),
inference(component_clause,[status(thm)],[f949]) ).
fof(f969,definition,
( sQ113_spl
<=> aDimensionOf0(xs) = aDimensionOf0(xt) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f971,plain,
( sQ113_spl
| aDimensionOf0(xs) != aDimensionOf0(xt) ),
inference(component_clause,[status(thm)],[f969]) ).
fof(f972,definition,
( sQ114_spl
<=> aDimensionOf0(xt) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f974,plain,
( sQ114_spl
| aDimensionOf0(xt) != sz00 ),
inference(component_clause,[status(thm)],[f972]) ).
fof(f975,definition,
( sQ115_spl
<=> sdtasasdt0(xt,xt) = sz0z00 ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f976,plain,
( ~ sQ115_spl
| sdtasasdt0(xt,xt) = sz0z00 ),
inference(component_clause,[status(thm)],[f975]) ).
fof(f977,plain,
( sQ115_spl
| sdtasasdt0(xt,xt) != sz0z00 ),
inference(component_clause,[status(thm)],[f975]) ).
fof(f979,plain,
( ~ sQ112_spl
| ~ sQ115_spl
| sz0z00 = sdtasasdt0(xs,xt) ),
inference(backward_demodulation,[status(thm)],[f976,f950]) ).
fof(f992,plain,
( ~ sQ115_spl
| sdtlseqdt0(sz0z00,sz0z00)
| ~ aVector0(xt) ),
inference(paramodulation,[status(thm)],[f976,f140]) ).
fof(f1008,definition,
( sQ119_spl
<=> aDimensionOf0(xt) = aDimensionOf0(xt) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1010,plain,
( sQ119_spl
| aDimensionOf0(xt) != aDimensionOf0(xt) ),
inference(component_clause,[status(thm)],[f1008]) ).
fof(f1021,plain,
( ~ sQ115_spl
| sQ89_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f992,f367,f760,f975]) ).
fof(f1022,plain,
( sQ114_spl
| ~ sQ4_spl
| sz00 != sz00 ),
inference(forward_demodulation,[status(thm)],[f365,f974]) ).
fof(f1023,plain,
( sQ114_spl
| ~ sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1022]) ).
fof(f1024,plain,
( sQ114_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f1023]) ).
fof(f1025,plain,
( sQ115_spl
| aDimensionOf0(xt) != sz00
| aDimensionOf0(xt) != aDimensionOf0(xt)
| ~ aVector0(xt)
| ~ aVector0(xt) ),
inference(resolution,[status(thm)],[f977,f136]) ).
fof(f1026,plain,
( sQ115_spl
| ~ sQ114_spl
| ~ sQ119_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f1025,f367,f1008,f972,f975]) ).
fof(f1027,plain,
( sQ119_spl
| ~ sQ4_spl
| sz00 != aDimensionOf0(xt) ),
inference(forward_demodulation,[status(thm)],[f365,f1010]) ).
fof(f1028,plain,
( sQ119_spl
| ~ sQ4_spl
| sz00 != sz00 ),
inference(forward_demodulation,[status(thm)],[f365,f1027]) ).
fof(f1029,plain,
( sQ119_spl
| ~ sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1028]) ).
fof(f1030,plain,
( sQ119_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f1029]) ).
fof(f1088,plain,
( ~ sQ112_spl
| ~ sQ115_spl
| ~ sdtlseqdt0(sdtasdt0(sz0z00,sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
inference(forward_demodulation,[status(thm)],[f979,f185]) ).
fof(f1089,plain,
( ~ sQ112_spl
| ~ sQ115_spl
| ~ sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))) ),
inference(forward_demodulation,[status(thm)],[f979,f1088]) ).
fof(f1090,plain,
( ~ sQ112_spl
| ~ sQ115_spl
| ~ sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(sdtasasdt0(xs,xs),sz0z00)) ),
inference(forward_demodulation,[status(thm)],[f976,f1089]) ).
fof(f1091,plain,
( ~ sQ112_spl
| ~ sQ115_spl
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs))
| ~ aScalar0(sz0z00)
| ~ aScalar0(sz0z00)
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ aScalar0(sz0z00) ),
inference(resolution,[status(thm)],[f1090,f105]) ).
fof(f1095,definition,
( sQ126_spl
<=> sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f1097,plain,
( sQ126_spl
| ~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ),
inference(component_clause,[status(thm)],[f1095]) ).
fof(f1098,plain,
( ~ sQ112_spl
| ~ sQ115_spl
| ~ sQ89_spl
| ~ sQ126_spl
| ~ sQ65_spl
| ~ sQ49_spl ),
inference(split_clause,[status(thm)],[f1091,f397,f510,f1095,f760,f975,f949]) ).
fof(f1115,plain,
( sQ112_spl
| ~ sQ115_spl
| sz0z00 != sdtasasdt0(xs,xt) ),
inference(forward_demodulation,[status(thm)],[f976,f951]) ).
fof(f1124,plain,
( sQ112_spl
| ~ sQ115_spl
| aDimensionOf0(xt) != sz00
| aDimensionOf0(xs) != aDimensionOf0(xt)
| ~ aVector0(xt)
| ~ aVector0(xs) ),
inference(resolution,[status(thm)],[f1115,f136]) ).
fof(f1125,plain,
( sQ112_spl
| ~ sQ115_spl
| ~ sQ114_spl
| ~ sQ113_spl
| ~ sQ43_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f1124,f352,f367,f969,f972,f975,f949]) ).
fof(f1126,plain,
( sQ113_spl
| ~ sQ4_spl
| sz00 != aDimensionOf0(xt) ),
inference(forward_demodulation,[status(thm)],[f202,f971]) ).
fof(f1127,plain,
( sQ113_spl
| ~ sQ4_spl
| sz00 != sz00 ),
inference(forward_demodulation,[status(thm)],[f365,f1126]) ).
fof(f1128,plain,
( sQ113_spl
| ~ sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1127]) ).
fof(f1129,plain,
( sQ113_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f1128]) ).
fof(f1158,plain,
( sQ126_spl
| ~ aVector0(xs) ),
inference(resolution,[status(thm)],[f1097,f140]) ).
fof(f1165,plain,
( sQ126_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f1158,f352,f1095]) ).
fof(f1181,plain,
$false,
inference(sat_refutation,[status(thm)],[f347,f360,f362,f422,f439,f459,f513,f1021,f1024,f1026,f1030,f1098,f1125,f1129,f1165]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG081+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n006.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:18:15 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.45 % Refutation found
% 0.12/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.47 % Elapsed time: 0.109286 seconds
% 0.12/0.47 % CPU time: 0.562702 seconds
% 0.12/0.47 % Total memory used: 115.392 MB
% 0.12/0.47 % Net memory used: 114.625 MB
%------------------------------------------------------------------------------