%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG049+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 : n005.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 28.01s 4.32s
% Output : CNFRefutation 28.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 70
% Syntax : Number of formulae : 287 ( 63 unt; 51 def)
% Number of atoms : 662 ( 151 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 583 ( 208 ~; 246 |; 52 &)
% ( 52 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 57 ( 55 usr; 51 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-2 aty)
% Number of variables : 105 ( 103 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( szszuzczcdt0(W0) != sz00
& aNaturalNumber0(szszuzczcdt0(W0)) ) ),
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(f9,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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(f12,axiom,
! [W0] :
( aScalar0(W0)
=> aScalar0(smndt0(W0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [W0] :
( aScalar0(W0)
=> sdtlseqdt0(W0,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [W0,W1] :
( ( aScalar0(W1)
& aScalar0(W0) )
=> ( ( sdtlseqdt0(sz0z00,W1)
& sdtlseqdt0(sz0z00,W0) )
=> ( sdtlseqdt0(sz0z00,sdtasdt0(W0,W1))
& sdtlseqdt0(sz0z00,sdtpldt0(W0,W1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [W0] :
( aVector0(W0)
=> aNaturalNumber0(aDimensionOf0(W0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aVector0(W0) )
=> aScalar0(sdtlbdtrb0(W0,W1)) ),
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(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(f36,axiom,
! [W0,W1] :
( ( aVector0(W1)
& aVector0(W0) )
=> ( ( aDimensionOf0(W1) != sz00
& aDimensionOf0(W0) = aDimensionOf0(W1) )
=> sdtasasdt0(W0,W1) = sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,hypothesis,
aVector0(xs),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
! [W0] :
( aVector0(W0)
=> ( iLess0(aDimensionOf0(W0),aDimensionOf0(xs))
=> sdtlseqdt0(sz0z00,sdtasasdt0(W0,W0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
( ! [W0] :
( aNaturalNumber0(W0)
=> sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0) )
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& aVector0(sziznziztdt0(xs))
& ! [W0] :
( aNaturalNumber0(W0)
=> sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0) )
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& aVector0(sziznziztdt0(xs)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
( sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
& ! [W0] :
( aNaturalNumber0(W0)
=> sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0) )
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& aVector0(sziznziztdt0(xs))
& ! [W0] :
( aNaturalNumber0(W0)
=> sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0) )
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& aVector0(sziznziztdt0(xs)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,conjecture,
sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,negated_conjecture,
~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
inference(negated_conjecture,[status(cth)],[f42]) ).
fof(f47,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f48,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aNaturalNumber0(szszuzczcdt0(W0)) )
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f49,plain,
! [X0] :
( aNaturalNumber0(szszuzczcdt0(X0))
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f50,plain,
! [X0] :
( szszuzczcdt0(X0) != sz00
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f59,plain,
! [W0] :
( iLess0(W0,szszuzczcdt0(W0))
| ~ aNaturalNumber0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f60,plain,
! [X0] :
( iLess0(X0,szszuzczcdt0(X0))
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f64,plain,
aScalar0(sz0z00),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f65,plain,
! [W0,W1] :
( aScalar0(sdtpldt0(W0,W1))
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f66,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f67,plain,
! [W0,W1] :
( aScalar0(sdtasdt0(W0,W1))
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f68,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
! [W0] :
( aScalar0(smndt0(W0))
| ~ aScalar0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f70,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f97,plain,
! [W0] :
( sdtlseqdt0(W0,W0)
| ~ aScalar0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f98,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f109,plain,
! [W0,W1] :
( ( sdtlseqdt0(sz0z00,sdtasdt0(W0,W1))
& sdtlseqdt0(sz0z00,sdtpldt0(W0,W1)) )
| ~ sdtlseqdt0(sz0z00,W1)
| ~ sdtlseqdt0(sz0z00,W0)
| ~ aScalar0(W1)
| ~ aScalar0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f110,plain,
! [X0,X1] :
( sdtlseqdt0(sz0z00,sdtpldt0(X0,X1))
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f119,plain,
! [W0] :
( aNaturalNumber0(aDimensionOf0(W0))
| ~ aVector0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f120,plain,
! [X0] :
( aNaturalNumber0(aDimensionOf0(X0))
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
! [W0,W1] :
( aScalar0(sdtlbdtrb0(W0,W1))
| ~ aNaturalNumber0(W1)
| ~ aVector0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f122,plain,
! [X0,X1] :
( aScalar0(sdtlbdtrb0(X0,X1))
| ~ aNaturalNumber0(X1)
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,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(f124,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)],[f123]) ).
fof(f125,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)],[f124]) ).
fof(f126,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))],[f125]) ).
fof(f127,plain,
! [X0,X1] :
( aVector0(X1)
| X1 != sziznziztdt0(X0)
| aDimensionOf0(X0) = sz00
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f134,plain,
! [W0,W1] :
( aScalar0(sdtasasdt0(W0,W1))
| aDimensionOf0(W0) != aDimensionOf0(W1)
| ~ aVector0(W1)
| ~ aVector0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f135,plain,
! [X0,X1] :
( aScalar0(sdtasasdt0(X0,X1))
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X1)
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f136,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(f137,plain,
! [X0,X1] :
( sdtasasdt0(X0,X1) = sz0z00
| aDimensionOf0(X1) != sz00
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X1)
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f138,plain,
! [W0,W1] :
( sdtasasdt0(W0,W1) = sdtpldt0(sdtasasdt0(sziznziztdt0(W0),sziznziztdt0(W1)),sdtasdt0(sdtlbdtrb0(W0,aDimensionOf0(W0)),sdtlbdtrb0(W1,aDimensionOf0(W1))))
| aDimensionOf0(W1) = sz00
| aDimensionOf0(W0) != aDimensionOf0(W1)
| ~ aVector0(W1)
| ~ aVector0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f139,plain,
! [X0,X1] :
( sdtasasdt0(X0,X1) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(X1)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(X1,aDimensionOf0(X1))))
| aDimensionOf0(X1) = sz00
| aDimensionOf0(X0) != aDimensionOf0(X1)
| ~ aVector0(X1)
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f140,plain,
aVector0(xs),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f141,plain,
! [W0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(W0,W0))
| ~ iLess0(aDimensionOf0(W0),aDimensionOf0(xs))
| ~ aVector0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f142,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ iLess0(aDimensionOf0(X0),aDimensionOf0(xs))
| ~ aVector0(X0) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f144,plain,
( ! [W0] :
( sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0)
| ~ aNaturalNumber0(W0) )
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& aVector0(sziznziztdt0(xs))
& ! [W0] :
( sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0)
| ~ aNaturalNumber0(W0) )
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& aVector0(sziznziztdt0(xs)) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f145,plain,
aVector0(sziznziztdt0(xs)),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f146,plain,
szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f151,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
& ! [W0] :
( sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0)
| ~ aNaturalNumber0(W0) )
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& aVector0(sziznziztdt0(xs))
& ! [W0] :
( sdtlbdtrb0(sziznziztdt0(xs),W0) = sdtlbdtrb0(xs,W0)
| ~ aNaturalNumber0(W0) )
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& aVector0(sziznziztdt0(xs)) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f158,plain,
sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f159,plain,
~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f175,plain,
! [X0] :
( aVector0(sziznziztdt0(X0))
| aDimensionOf0(X0) = sz00
| ~ aVector0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f127]) ).
fof(f183,plain,
sdtlseqdt0(sz0z00,sz0z00),
inference(resolution,[status(thm)],[f98,f64]) ).
fof(f217,definition,
( sQ10_spl
<=> sdtlseqdt0(sz0z00,sz0z00) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f219,plain,
( sQ10_spl
| ~ sdtlseqdt0(sz0z00,sz0z00) ),
inference(component_clause,[status(thm)],[f217]) ).
fof(f240,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f219,f183]) ).
fof(f241,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f240]) ).
fof(f268,plain,
! [X0] :
( aScalar0(sdtpldt0(X0,sz0z00))
| ~ aScalar0(X0) ),
inference(resolution,[status(thm)],[f66,f64]) ).
fof(f273,plain,
! [X0] :
( aScalar0(sdtasasdt0(X0,X0))
| ~ aVector0(X0)
| ~ aVector0(X0) ),
inference(equality_resolution,[status(thm)],[f135]) ).
fof(f274,plain,
! [X0] :
( aScalar0(sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f273]) ).
fof(f275,plain,
aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))),
inference(resolution,[status(thm)],[f274,f145]) ).
fof(f276,plain,
aScalar0(sdtasasdt0(xs,xs)),
inference(resolution,[status(thm)],[f274,f140]) ).
fof(f278,plain,
aScalar0(smndt0(sdtasasdt0(xs,xs))),
inference(resolution,[status(thm)],[f276,f70]) ).
fof(f286,plain,
sdtlseqdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)),
inference(resolution,[status(thm)],[f276,f98]) ).
fof(f299,plain,
! [X0] :
( sdtasasdt0(X0,xs) = sz0z00
| aDimensionOf0(xs) != sz00
| aDimensionOf0(X0) != aDimensionOf0(xs)
| ~ aVector0(X0) ),
inference(resolution,[status(thm)],[f137,f140]) ).
fof(f307,definition,
! [X0] :
( sQ22_spl
<=> ( sdtasasdt0(X0,xs) = sz0z00
| aDimensionOf0(X0) != aDimensionOf0(xs)
| ~ aVector0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f308,plain,
! [X0] :
( ~ sQ22_spl
| sdtasasdt0(X0,xs) = sz0z00
| aDimensionOf0(X0) != aDimensionOf0(xs)
| ~ aVector0(X0) ),
inference(component_clause,[status(thm)],[f307]) ).
fof(f310,definition,
( sQ23_spl
<=> aDimensionOf0(xs) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f313,plain,
( ~ sQ23_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f299,f307,f310]) ).
fof(f315,plain,
! [X0] :
( sdtasasdt0(X0,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
| aDimensionOf0(xs) = sz00
| aDimensionOf0(X0) != aDimensionOf0(xs)
| ~ aVector0(X0) ),
inference(resolution,[status(thm)],[f139,f140]) ).
fof(f320,definition,
! [X0] :
( sQ25_spl
<=> ( sdtasasdt0(X0,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
| aDimensionOf0(X0) != aDimensionOf0(xs)
| ~ aVector0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f321,plain,
! [X0] :
( ~ sQ25_spl
| sdtasasdt0(X0,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(X0),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(X0,aDimensionOf0(X0)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
| aDimensionOf0(X0) != aDimensionOf0(xs)
| ~ aVector0(X0) ),
inference(component_clause,[status(thm)],[f320]) ).
fof(f323,plain,
( sQ23_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f315,f320,f310]) ).
fof(f336,plain,
aScalar0(sdtpldt0(sdtasasdt0(xs,xs),sz0z00)),
inference(resolution,[status(thm)],[f268,f276]) ).
fof(f352,plain,
aScalar0(smndt0(smndt0(sdtasasdt0(xs,xs)))),
inference(resolution,[status(thm)],[f278,f70]) ).
fof(f386,plain,
! [X0] :
( aScalar0(sdtlbdtrb0(xs,X0))
| ~ aNaturalNumber0(X0) ),
inference(resolution,[status(thm)],[f122,f140]) ).
fof(f390,plain,
aScalar0(sdtlbdtrb0(xs,sz00)),
inference(resolution,[status(thm)],[f386,f47]) ).
fof(f450,definition,
( sQ33_spl
<=> sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f451,plain,
( ~ sQ33_spl
| sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))) ),
inference(component_clause,[status(thm)],[f450]) ).
fof(f508,plain,
aScalar0(sdtpldt0(sdtlbdtrb0(xs,sz00),sz0z00)),
inference(resolution,[status(thm)],[f390,f268]) ).
fof(f514,plain,
aScalar0(smndt0(sdtlbdtrb0(xs,sz00))),
inference(resolution,[status(thm)],[f390,f70]) ).
fof(f522,plain,
sdtlseqdt0(sdtlbdtrb0(xs,sz00),sdtlbdtrb0(xs,sz00)),
inference(resolution,[status(thm)],[f390,f98]) ).
fof(f700,plain,
( ~ sQ22_spl
| sdtasasdt0(xs,xs) = sz0z00
| aDimensionOf0(xs) != aDimensionOf0(xs) ),
inference(resolution,[status(thm)],[f308,f140]) ).
fof(f708,definition,
( sQ62_spl
<=> aDimensionOf0(xs) = aDimensionOf0(xs) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f710,plain,
( sQ62_spl
| aDimensionOf0(xs) != aDimensionOf0(xs) ),
inference(component_clause,[status(thm)],[f708]) ).
fof(f711,definition,
( sQ63_spl
<=> sdtasasdt0(xs,xs) = sz0z00 ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f712,plain,
( ~ sQ63_spl
| sdtasasdt0(xs,xs) = sz0z00 ),
inference(component_clause,[status(thm)],[f711]) ).
fof(f714,plain,
( ~ sQ22_spl
| sQ63_spl
| ~ sQ62_spl ),
inference(split_clause,[status(thm)],[f700,f708,f711,f307]) ).
fof(f715,plain,
( sQ62_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f710]) ).
fof(f716,plain,
sQ62_spl,
inference(contradiction_clause,[status(thm)],[f715]) ).
fof(f720,plain,
( ~ sQ63_spl
| ~ sdtlseqdt0(sz0z00,sz0z00) ),
inference(backward_demodulation,[status(thm)],[f712,f159]) ).
fof(f722,plain,
( ~ sQ63_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f720,f217,f711]) ).
fof(f811,plain,
( ~ sQ25_spl
| sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
| aDimensionOf0(xs) != aDimensionOf0(xs) ),
inference(resolution,[status(thm)],[f321,f140]) ).
fof(f816,definition,
( sQ71_spl
<=> sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f817,plain,
( ~ sQ71_spl
| sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ),
inference(component_clause,[status(thm)],[f816]) ).
fof(f819,plain,
( ~ sQ25_spl
| sQ71_spl
| ~ sQ62_spl ),
inference(split_clause,[status(thm)],[f811,f708,f816,f320]) ).
fof(f872,plain,
( iLess0(aDimensionOf0(sziznziztdt0(xs)),aDimensionOf0(xs))
| ~ aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs))) ),
inference(paramodulation,[status(thm)],[f146,f60]) ).
fof(f874,plain,
( aNaturalNumber0(aDimensionOf0(xs))
| ~ aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs))) ),
inference(paramodulation,[status(thm)],[f146,f49]) ).
fof(f875,definition,
( sQ74_spl
<=> aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs))) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f877,plain,
( sQ74_spl
| ~ aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs))) ),
inference(component_clause,[status(thm)],[f875]) ).
fof(f878,definition,
( sQ75_spl
<=> iLess0(aDimensionOf0(sziznziztdt0(xs)),aDimensionOf0(xs)) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f879,plain,
( ~ sQ75_spl
| iLess0(aDimensionOf0(sziznziztdt0(xs)),aDimensionOf0(xs)) ),
inference(component_clause,[status(thm)],[f878]) ).
fof(f881,plain,
( sQ75_spl
| ~ sQ74_spl ),
inference(split_clause,[status(thm)],[f872,f875,f878]) ).
fof(f883,definition,
( sQ76_spl
<=> aNaturalNumber0(aDimensionOf0(xs)) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f884,plain,
( ~ sQ76_spl
| aNaturalNumber0(aDimensionOf0(xs)) ),
inference(component_clause,[status(thm)],[f883]) ).
fof(f886,plain,
( sQ76_spl
| ~ sQ74_spl ),
inference(split_clause,[status(thm)],[f874,f875,f883]) ).
fof(f887,plain,
( sQ74_spl
| ~ aVector0(sziznziztdt0(xs)) ),
inference(resolution,[status(thm)],[f877,f120]) ).
fof(f888,plain,
( sQ74_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f887,f145]) ).
fof(f889,plain,
sQ74_spl,
inference(contradiction_clause,[status(thm)],[f888]) ).
fof(f896,plain,
( aVector0(sziznziztdt0(xs))
| aDimensionOf0(xs) = sz00 ),
inference(resolution,[status(thm)],[f175,f140]) ).
fof(f901,definition,
( sQ79_spl
<=> aVector0(sziznziztdt0(xs)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f904,plain,
( sQ79_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f896,f310,f901]) ).
fof(f957,plain,
( ~ sQ76_spl
| aScalar0(sdtlbdtrb0(xs,aDimensionOf0(xs))) ),
inference(resolution,[status(thm)],[f884,f386]) ).
fof(f1191,plain,
! [X0] :
( ~ sQ76_spl
| aScalar0(sdtasdt0(X0,sdtlbdtrb0(xs,aDimensionOf0(xs))))
| ~ aScalar0(X0) ),
inference(resolution,[status(thm)],[f957,f68]) ).
fof(f1491,plain,
aScalar0(smndt0(smndt0(sdtlbdtrb0(xs,sz00)))),
inference(resolution,[status(thm)],[f514,f70]) ).
fof(f1699,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtpldt0(X0,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))
| ~ aScalar0(X0) ),
inference(resolution,[status(thm)],[f158,f110]) ).
fof(f1713,definition,
! [X0] :
( sQ136_spl
<=> ( sdtlseqdt0(sz0z00,sdtpldt0(X0,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f1714,plain,
! [X0] :
( ~ sQ136_spl
| sdtlseqdt0(sz0z00,sdtpldt0(X0,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))
| ~ sdtlseqdt0(sz0z00,X0)
| ~ aScalar0(X0) ),
inference(component_clause,[status(thm)],[f1713]) ).
fof(f1716,definition,
( sQ137_spl
<=> aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1718,plain,
( sQ137_spl
| ~ aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ),
inference(component_clause,[status(thm)],[f1716]) ).
fof(f1719,plain,
( ~ sQ137_spl
| sQ136_spl ),
inference(split_clause,[status(thm)],[f1699,f1713,f1716]) ).
fof(f2496,plain,
( ~ sQ75_spl
| sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))
| ~ aVector0(sziznziztdt0(xs)) ),
inference(resolution,[status(thm)],[f879,f142]) ).
fof(f2497,plain,
( ~ sQ75_spl
| sQ33_spl
| ~ sQ79_spl ),
inference(split_clause,[status(thm)],[f2496,f901,f450,f878]) ).
fof(f2964,definition,
( sQ249_spl
<=> aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))) ),
introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition]) ).
fof(f2966,plain,
( sQ249_spl
| ~ aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))) ),
inference(component_clause,[status(thm)],[f2964]) ).
fof(f3976,plain,
( sQ249_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2966,f275]) ).
fof(f3977,plain,
sQ249_spl,
inference(contradiction_clause,[status(thm)],[f3976]) ).
fof(f4464,definition,
( sQ373_spl
<=> szszuzczcdt0(aDimensionOf0(xs)) = szszuzczcdt0(aDimensionOf0(xs)) ),
introduced(definition,[new_symbols(definition,[sQ373_spl])],[split_symbol_definition]) ).
fof(f4466,plain,
( sQ373_spl
| szszuzczcdt0(aDimensionOf0(xs)) != szszuzczcdt0(aDimensionOf0(xs)) ),
inference(component_clause,[status(thm)],[f4464]) ).
fof(f4469,plain,
( sQ373_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4466]) ).
fof(f4470,plain,
sQ373_spl,
inference(contradiction_clause,[status(thm)],[f4469]) ).
fof(f5334,definition,
( sQ427_spl
<=> sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))) = sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))) ),
introduced(definition,[new_symbols(definition,[sQ427_spl])],[split_symbol_definition]) ).
fof(f5336,plain,
( sQ427_spl
| sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))) != sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))) ),
inference(component_clause,[status(thm)],[f5334]) ).
fof(f5365,plain,
( sQ427_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f5336]) ).
fof(f5366,plain,
sQ427_spl,
inference(contradiction_clause,[status(thm)],[f5365]) ).
fof(f5472,definition,
( sQ454_spl
<=> sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00)) = sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00)) ),
introduced(definition,[new_symbols(definition,[sQ454_spl])],[split_symbol_definition]) ).
fof(f5474,plain,
( sQ454_spl
| sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00)) != sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00)) ),
inference(component_clause,[status(thm)],[f5472]) ).
fof(f5506,plain,
( sQ454_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f5474]) ).
fof(f5507,plain,
sQ454_spl,
inference(contradiction_clause,[status(thm)],[f5506]) ).
fof(f6843,definition,
( sQ545_spl
<=> sdtasdt0(sdtpldt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtpldt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) = sdtasdt0(sdtpldt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtpldt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) ),
introduced(definition,[new_symbols(definition,[sQ545_spl])],[split_symbol_definition]) ).
fof(f6845,plain,
( sQ545_spl
| sdtasdt0(sdtpldt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtpldt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) != sdtasdt0(sdtpldt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtpldt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) ),
inference(component_clause,[status(thm)],[f6843]) ).
fof(f6877,plain,
( sQ545_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f6845]) ).
fof(f6878,plain,
sQ545_spl,
inference(contradiction_clause,[status(thm)],[f6877]) ).
fof(f6933,definition,
( sQ555_spl
<=> aVector0(xs) ),
introduced(definition,[new_symbols(definition,[sQ555_spl])],[split_symbol_definition]) ).
fof(f6935,plain,
( sQ555_spl
| ~ aVector0(xs) ),
inference(component_clause,[status(thm)],[f6933]) ).
fof(f6937,plain,
( sQ555_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6935,f140]) ).
fof(f6938,plain,
sQ555_spl,
inference(contradiction_clause,[status(thm)],[f6937]) ).
fof(f7467,definition,
( sQ582_spl
<=> sdtasdt0(sdtlbdtrb0(xs,szszuzczcdt0(sz00)),sdtlbdtrb0(xs,szszuzczcdt0(sz00))) = sdtasdt0(sdtlbdtrb0(xs,szszuzczcdt0(sz00)),sdtlbdtrb0(xs,szszuzczcdt0(sz00))) ),
introduced(definition,[new_symbols(definition,[sQ582_spl])],[split_symbol_definition]) ).
fof(f7469,plain,
( sQ582_spl
| sdtasdt0(sdtlbdtrb0(xs,szszuzczcdt0(sz00)),sdtlbdtrb0(xs,szszuzczcdt0(sz00))) != sdtasdt0(sdtlbdtrb0(xs,szszuzczcdt0(sz00)),sdtlbdtrb0(xs,szszuzczcdt0(sz00))) ),
inference(component_clause,[status(thm)],[f7467]) ).
fof(f7495,plain,
( sQ582_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f7469]) ).
fof(f7496,plain,
sQ582_spl,
inference(contradiction_clause,[status(thm)],[f7495]) ).
fof(f7736,definition,
( sQ601_spl
<=> sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)) = sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)) ),
introduced(definition,[new_symbols(definition,[sQ601_spl])],[split_symbol_definition]) ).
fof(f7738,plain,
( sQ601_spl
| sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)) != sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)) ),
inference(component_clause,[status(thm)],[f7736]) ).
fof(f7770,plain,
( sQ601_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f7738]) ).
fof(f7771,plain,
sQ601_spl,
inference(contradiction_clause,[status(thm)],[f7770]) ).
fof(f8028,definition,
( sQ645_spl
<=> sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))) = sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))) ),
introduced(definition,[new_symbols(definition,[sQ645_spl])],[split_symbol_definition]) ).
fof(f8030,plain,
( sQ645_spl
| sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))) != sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))) ),
inference(component_clause,[status(thm)],[f8028]) ).
fof(f8059,plain,
( sQ645_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f8030]) ).
fof(f8060,plain,
sQ645_spl,
inference(contradiction_clause,[status(thm)],[f8059]) ).
fof(f8259,definition,
( sQ690_spl
<=> sdtasdt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) = sdtasdt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) ),
introduced(definition,[new_symbols(definition,[sQ690_spl])],[split_symbol_definition]) ).
fof(f8261,plain,
( sQ690_spl
| sdtasdt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) != sdtasdt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) ),
inference(component_clause,[status(thm)],[f8259]) ).
fof(f8293,plain,
( sQ690_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f8261]) ).
fof(f8294,plain,
sQ690_spl,
inference(contradiction_clause,[status(thm)],[f8293]) ).
fof(f8698,definition,
( sQ724_spl
<=> aNaturalNumber0(szszuzczcdt0(sz00)) ),
introduced(definition,[new_symbols(definition,[sQ724_spl])],[split_symbol_definition]) ).
fof(f8700,plain,
( sQ724_spl
| ~ aNaturalNumber0(szszuzczcdt0(sz00)) ),
inference(component_clause,[status(thm)],[f8698]) ).
fof(f8740,definition,
( sQ732_spl
<=> sz00 = szszuzczcdt0(sz00) ),
introduced(definition,[new_symbols(definition,[sQ732_spl])],[split_symbol_definition]) ).
fof(f8741,plain,
( ~ sQ732_spl
| sz00 = szszuzczcdt0(sz00) ),
inference(component_clause,[status(thm)],[f8740]) ).
fof(f8924,definition,
( sQ752_spl
<=> szszuzczcdt0(szszuzczcdt0(sz00)) = szszuzczcdt0(szszuzczcdt0(sz00)) ),
introduced(definition,[new_symbols(definition,[sQ752_spl])],[split_symbol_definition]) ).
fof(f8926,plain,
( sQ752_spl
| szszuzczcdt0(szszuzczcdt0(sz00)) != szszuzczcdt0(szszuzczcdt0(sz00)) ),
inference(component_clause,[status(thm)],[f8924]) ).
fof(f8952,plain,
( sQ752_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f8926]) ).
fof(f8953,plain,
sQ752_spl,
inference(contradiction_clause,[status(thm)],[f8952]) ).
fof(f9004,definition,
( sQ765_spl
<=> szszuzczcdt0(szszuzczcdt0(aDimensionOf0(xs))) = szszuzczcdt0(szszuzczcdt0(aDimensionOf0(xs))) ),
introduced(definition,[new_symbols(definition,[sQ765_spl])],[split_symbol_definition]) ).
fof(f9006,plain,
( sQ765_spl
| szszuzczcdt0(szszuzczcdt0(aDimensionOf0(xs))) != szszuzczcdt0(szszuzczcdt0(aDimensionOf0(xs))) ),
inference(component_clause,[status(thm)],[f9004]) ).
fof(f9011,plain,
( sQ765_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f9006]) ).
fof(f9012,plain,
sQ765_spl,
inference(contradiction_clause,[status(thm)],[f9011]) ).
fof(f9916,definition,
( sQ833_spl
<=> sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sz0z00),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sz0z00)) = sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sz0z00),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sz0z00)) ),
introduced(definition,[new_symbols(definition,[sQ833_spl])],[split_symbol_definition]) ).
fof(f9918,plain,
( sQ833_spl
| sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sz0z00),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sz0z00)) != sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sz0z00),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sz0z00)) ),
inference(component_clause,[status(thm)],[f9916]) ).
fof(f9950,plain,
( sQ833_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f9918]) ).
fof(f9951,plain,
sQ833_spl,
inference(contradiction_clause,[status(thm)],[f9950]) ).
fof(f10079,definition,
( sQ858_spl
<=> sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) = sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) ),
introduced(definition,[new_symbols(definition,[sQ858_spl])],[split_symbol_definition]) ).
fof(f10081,plain,
( sQ858_spl
| sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) != sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) ),
inference(component_clause,[status(thm)],[f10079]) ).
fof(f10113,plain,
( sQ858_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10081]) ).
fof(f10114,plain,
sQ858_spl,
inference(contradiction_clause,[status(thm)],[f10113]) ).
fof(f10203,definition,
( sQ882_spl
<=> sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))) = sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))) ),
introduced(definition,[new_symbols(definition,[sQ882_spl])],[split_symbol_definition]) ).
fof(f10205,plain,
( sQ882_spl
| sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))) != sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))) ),
inference(component_clause,[status(thm)],[f10203]) ).
fof(f10237,plain,
( sQ882_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10205]) ).
fof(f10238,plain,
sQ882_spl,
inference(contradiction_clause,[status(thm)],[f10237]) ).
fof(f10305,definition,
( sQ902_spl
<=> sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))) = sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))) ),
introduced(definition,[new_symbols(definition,[sQ902_spl])],[split_symbol_definition]) ).
fof(f10307,plain,
( sQ902_spl
| sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))) != sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))) ),
inference(component_clause,[status(thm)],[f10305]) ).
fof(f10339,plain,
( sQ902_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10307]) ).
fof(f10340,plain,
sQ902_spl,
inference(contradiction_clause,[status(thm)],[f10339]) ).
fof(f10506,definition,
( sQ930_spl
<=> sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))) = sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))) ),
introduced(definition,[new_symbols(definition,[sQ930_spl])],[split_symbol_definition]) ).
fof(f10508,plain,
( sQ930_spl
| sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))) != sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))) ),
inference(component_clause,[status(thm)],[f10506]) ).
fof(f10540,plain,
( sQ930_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10508]) ).
fof(f10541,plain,
sQ930_spl,
inference(contradiction_clause,[status(thm)],[f10540]) ).
fof(f10732,definition,
( sQ968_spl
<=> sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)))) = sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)))) ),
introduced(definition,[new_symbols(definition,[sQ968_spl])],[split_symbol_definition]) ).
fof(f10734,plain,
( sQ968_spl
| sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)))) != sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00))),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)))) ),
inference(component_clause,[status(thm)],[f10732]) ).
fof(f10763,plain,
( sQ968_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f10734]) ).
fof(f10764,plain,
sQ968_spl,
inference(contradiction_clause,[status(thm)],[f10763]) ).
fof(f10969,definition,
( sQ997_spl
<=> aScalar0(sdtpldt0(sdtasasdt0(xs,xs),sz0z00)) ),
introduced(definition,[new_symbols(definition,[sQ997_spl])],[split_symbol_definition]) ).
fof(f10971,plain,
( sQ997_spl
| ~ aScalar0(sdtpldt0(sdtasasdt0(xs,xs),sz0z00)) ),
inference(component_clause,[status(thm)],[f10969]) ).
fof(f10977,plain,
( sQ997_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10971,f336]) ).
fof(f10978,plain,
sQ997_spl,
inference(contradiction_clause,[status(thm)],[f10977]) ).
fof(f11045,definition,
( sQ1011_spl
<=> sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sz0z00),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sz0z00)) = sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sz0z00),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sz0z00)) ),
introduced(definition,[new_symbols(definition,[sQ1011_spl])],[split_symbol_definition]) ).
fof(f11047,plain,
( sQ1011_spl
| sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sz0z00),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sz0z00)) != sdtasdt0(sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sz0z00),sdtasdt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sz0z00)),sz0z00)) ),
inference(component_clause,[status(thm)],[f11045]) ).
fof(f11079,plain,
( sQ1011_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f11047]) ).
fof(f11080,plain,
sQ1011_spl,
inference(contradiction_clause,[status(thm)],[f11079]) ).
fof(f11782,definition,
( sQ1082_spl
<=> sdtasdt0(sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sz0z00),sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sz0z00)) = sdtasdt0(sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sz0z00),sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sz0z00)) ),
introduced(definition,[new_symbols(definition,[sQ1082_spl])],[split_symbol_definition]) ).
fof(f11784,plain,
( sQ1082_spl
| sdtasdt0(sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sz0z00),sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sz0z00)) != sdtasdt0(sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sz0z00),sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sz0z00)) ),
inference(component_clause,[status(thm)],[f11782]) ).
fof(f11816,plain,
( sQ1082_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f11784]) ).
fof(f11817,plain,
sQ1082_spl,
inference(contradiction_clause,[status(thm)],[f11816]) ).
fof(f11902,definition,
( sQ1103_spl
<=> sdtasdt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00),sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00)) = sdtasdt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00),sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00)) ),
introduced(definition,[new_symbols(definition,[sQ1103_spl])],[split_symbol_definition]) ).
fof(f11904,plain,
( sQ1103_spl
| sdtasdt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00),sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00)) != sdtasdt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00),sdtpldt0(sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sz0z00)) ),
inference(component_clause,[status(thm)],[f11902]) ).
fof(f11936,plain,
( sQ1103_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f11904]) ).
fof(f11937,plain,
sQ1103_spl,
inference(contradiction_clause,[status(thm)],[f11936]) ).
fof(f12248,definition,
( sQ1137_spl
<=> aScalar0(smndt0(smndt0(sdtasasdt0(xs,xs)))) ),
introduced(definition,[new_symbols(definition,[sQ1137_spl])],[split_symbol_definition]) ).
fof(f12250,plain,
( sQ1137_spl
| ~ aScalar0(smndt0(smndt0(sdtasasdt0(xs,xs)))) ),
inference(component_clause,[status(thm)],[f12248]) ).
fof(f12256,plain,
( sQ1137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12250,f352]) ).
fof(f12257,plain,
sQ1137_spl,
inference(contradiction_clause,[status(thm)],[f12256]) ).
fof(f12558,definition,
( sQ1183_spl
<=> aScalar0(sdtpldt0(sdtlbdtrb0(xs,sz00),sz0z00)) ),
introduced(definition,[new_symbols(definition,[sQ1183_spl])],[split_symbol_definition]) ).
fof(f12560,plain,
( sQ1183_spl
| ~ aScalar0(sdtpldt0(sdtlbdtrb0(xs,sz00),sz0z00)) ),
inference(component_clause,[status(thm)],[f12558]) ).
fof(f12566,plain,
( sQ1183_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12560,f508]) ).
fof(f12567,plain,
sQ1183_spl,
inference(contradiction_clause,[status(thm)],[f12566]) ).
fof(f13718,definition,
( sQ1231_spl
<=> aScalar0(smndt0(smndt0(sdtlbdtrb0(xs,sz00)))) ),
introduced(definition,[new_symbols(definition,[sQ1231_spl])],[split_symbol_definition]) ).
fof(f13720,plain,
( sQ1231_spl
| ~ aScalar0(smndt0(smndt0(sdtlbdtrb0(xs,sz00)))) ),
inference(component_clause,[status(thm)],[f13718]) ).
fof(f13726,plain,
( sQ1231_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13720,f1491]) ).
fof(f13727,plain,
sQ1231_spl,
inference(contradiction_clause,[status(thm)],[f13726]) ).
fof(f13729,plain,
( ~ sQ136_spl
| ~ sQ33_spl
| sdtlseqdt0(sz0z00,sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))
| ~ aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))) ),
inference(resolution,[status(thm)],[f451,f1714]) ).
fof(f13754,definition,
( sQ1234_spl
<=> sdtlseqdt0(sz0z00,sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) ),
introduced(definition,[new_symbols(definition,[sQ1234_spl])],[split_symbol_definition]) ).
fof(f13755,plain,
( ~ sQ1234_spl
| sdtlseqdt0(sz0z00,sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) ),
inference(component_clause,[status(thm)],[f13754]) ).
fof(f13757,plain,
( ~ sQ136_spl
| ~ sQ33_spl
| sQ1234_spl
| ~ sQ249_spl ),
inference(split_clause,[status(thm)],[f13729,f2964,f13754,f450,f1713]) ).
fof(f13795,definition,
( sQ1244_spl
<=> sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))) = sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))) ),
introduced(definition,[new_symbols(definition,[sQ1244_spl])],[split_symbol_definition]) ).
fof(f13797,plain,
( sQ1244_spl
| sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))) != sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))) ),
inference(component_clause,[status(thm)],[f13795]) ).
fof(f13823,plain,
( sQ1244_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f13797]) ).
fof(f13824,plain,
sQ1244_spl,
inference(contradiction_clause,[status(thm)],[f13823]) ).
fof(f13825,plain,
( ~ sQ1234_spl
| ~ sQ71_spl
| sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ),
inference(forward_demodulation,[status(thm)],[f817,f13755]) ).
fof(f13826,plain,
( ~ sQ1234_spl
| ~ sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13825,f159]) ).
fof(f13827,plain,
( ~ sQ1234_spl
| ~ sQ71_spl ),
inference(contradiction_clause,[status(thm)],[f13826]) ).
fof(f13906,plain,
( ~ sQ732_spl
| ~ aNaturalNumber0(sz00) ),
inference(resolution,[status(thm)],[f8741,f50]) ).
fof(f13913,plain,
( sQ724_spl
| ~ aNaturalNumber0(sz00) ),
inference(resolution,[status(thm)],[f8700,f49]) ).
fof(f13914,plain,
( sQ724_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13913,f47]) ).
fof(f13915,plain,
sQ724_spl,
inference(contradiction_clause,[status(thm)],[f13914]) ).
fof(f14342,definition,
( sQ1272_spl
<=> sdtasdt0(sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) = sdtasdt0(sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) ),
introduced(definition,[new_symbols(definition,[sQ1272_spl])],[split_symbol_definition]) ).
fof(f14344,plain,
( sQ1272_spl
| sdtasdt0(sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) != sdtasdt0(sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))),sdtpldt0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))) ),
inference(component_clause,[status(thm)],[f14342]) ).
fof(f14376,plain,
( sQ1272_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f14344]) ).
fof(f14377,plain,
sQ1272_spl,
inference(contradiction_clause,[status(thm)],[f14376]) ).
fof(f15414,definition,
( sQ1320_spl
<=> sdtasdt0(sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))) = sdtasdt0(sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))) ),
introduced(definition,[new_symbols(definition,[sQ1320_spl])],[split_symbol_definition]) ).
fof(f15416,plain,
( sQ1320_spl
| sdtasdt0(sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))) != sdtasdt0(sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs))) ),
inference(component_clause,[status(thm)],[f15414]) ).
fof(f15448,plain,
( sQ1320_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f15416]) ).
fof(f15449,plain,
sQ1320_spl,
inference(contradiction_clause,[status(thm)],[f15448]) ).
fof(f15548,definition,
( sQ1340_spl
<=> sdtlseqdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)) ),
introduced(definition,[new_symbols(definition,[sQ1340_spl])],[split_symbol_definition]) ).
fof(f15550,plain,
( sQ1340_spl
| ~ sdtlseqdt0(sdtasasdt0(xs,xs),sdtasasdt0(xs,xs)) ),
inference(component_clause,[status(thm)],[f15548]) ).
fof(f15556,plain,
( sQ1340_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15550,f286]) ).
fof(f15557,plain,
sQ1340_spl,
inference(contradiction_clause,[status(thm)],[f15556]) ).
fof(f16249,plain,
( ~ sQ732_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13906,f47]) ).
fof(f16250,plain,
~ sQ732_spl,
inference(contradiction_clause,[status(thm)],[f16249]) ).
fof(f16903,definition,
( sQ1379_spl
<=> sdtasdt0(smndt0(sdtlbdtrb0(xs,aDimensionOf0(xs))),smndt0(sdtlbdtrb0(xs,aDimensionOf0(xs)))) = sdtasdt0(smndt0(sdtlbdtrb0(xs,aDimensionOf0(xs))),smndt0(sdtlbdtrb0(xs,aDimensionOf0(xs)))) ),
introduced(definition,[new_symbols(definition,[sQ1379_spl])],[split_symbol_definition]) ).
fof(f16905,plain,
( sQ1379_spl
| sdtasdt0(smndt0(sdtlbdtrb0(xs,aDimensionOf0(xs))),smndt0(sdtlbdtrb0(xs,aDimensionOf0(xs)))) != sdtasdt0(smndt0(sdtlbdtrb0(xs,aDimensionOf0(xs))),smndt0(sdtlbdtrb0(xs,aDimensionOf0(xs)))) ),
inference(component_clause,[status(thm)],[f16903]) ).
fof(f16931,plain,
( sQ1379_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f16905]) ).
fof(f16932,plain,
sQ1379_spl,
inference(contradiction_clause,[status(thm)],[f16931]) ).
fof(f16965,definition,
( sQ1385_spl
<=> sdtlseqdt0(sdtlbdtrb0(xs,sz00),sdtlbdtrb0(xs,sz00)) ),
introduced(definition,[new_symbols(definition,[sQ1385_spl])],[split_symbol_definition]) ).
fof(f16967,plain,
( sQ1385_spl
| ~ sdtlseqdt0(sdtlbdtrb0(xs,sz00),sdtlbdtrb0(xs,sz00)) ),
inference(component_clause,[status(thm)],[f16965]) ).
fof(f16970,plain,
( sQ1385_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16967,f522]) ).
fof(f16971,plain,
sQ1385_spl,
inference(contradiction_clause,[status(thm)],[f16970]) ).
fof(f17038,definition,
( sQ1397_spl
<=> sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,sz00),sdtlbdtrb0(xs,sz00)),sdtasdt0(sdtlbdtrb0(xs,sz00),sdtlbdtrb0(xs,sz00))) = sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,sz00),sdtlbdtrb0(xs,sz00)),sdtasdt0(sdtlbdtrb0(xs,sz00),sdtlbdtrb0(xs,sz00))) ),
introduced(definition,[new_symbols(definition,[sQ1397_spl])],[split_symbol_definition]) ).
fof(f17040,plain,
( sQ1397_spl
| sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,sz00),sdtlbdtrb0(xs,sz00)),sdtasdt0(sdtlbdtrb0(xs,sz00),sdtlbdtrb0(xs,sz00))) != sdtasdt0(sdtasdt0(sdtlbdtrb0(xs,sz00),sdtlbdtrb0(xs,sz00)),sdtasdt0(sdtlbdtrb0(xs,sz00),sdtlbdtrb0(xs,sz00))) ),
inference(component_clause,[status(thm)],[f17038]) ).
fof(f17069,plain,
( sQ1397_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f17040]) ).
fof(f17070,plain,
sQ1397_spl,
inference(contradiction_clause,[status(thm)],[f17069]) ).
fof(f20451,definition,
( sQ1512_spl
<=> sdtasdt0(sdtlbdtrb0(xs,sK0_skl(sz00)),sdtlbdtrb0(xs,sK0_skl(sz00))) = sdtasdt0(sdtlbdtrb0(xs,sK0_skl(sz00)),sdtlbdtrb0(xs,sK0_skl(sz00))) ),
introduced(definition,[new_symbols(definition,[sQ1512_spl])],[split_symbol_definition]) ).
fof(f20453,plain,
( sQ1512_spl
| sdtasdt0(sdtlbdtrb0(xs,sK0_skl(sz00)),sdtlbdtrb0(xs,sK0_skl(sz00))) != sdtasdt0(sdtlbdtrb0(xs,sK0_skl(sz00)),sdtlbdtrb0(xs,sK0_skl(sz00))) ),
inference(component_clause,[status(thm)],[f20451]) ).
fof(f20480,plain,
( sQ1512_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f20453]) ).
fof(f20481,plain,
sQ1512_spl,
inference(contradiction_clause,[status(thm)],[f20480]) ).
fof(f21356,plain,
( ~ sQ76_spl
| aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ),
inference(resolution,[status(thm)],[f1191,f957]) ).
fof(f21361,plain,
( ~ sQ76_spl
| sQ137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21356,f1718]) ).
fof(f21362,plain,
( ~ sQ76_spl
| sQ137_spl ),
inference(contradiction_clause,[status(thm)],[f21361]) ).
fof(f21363,plain,
$false,
inference(sat_refutation,[status(thm)],[f241,f313,f323,f714,f716,f722,f819,f881,f886,f889,f904,f1719,f2497,f3977,f4470,f5366,f5507,f6878,f6938,f7496,f7771,f8060,f8294,f8953,f9012,f9951,f10114,f10238,f10340,f10541,f10764,f10978,f11080,f11817,f11937,f12257,f12567,f13727,f13757,f13824,f13827,f13915,f14377,f15449,f15557,f16250,f16932,f16971,f17070,f20481,f21362]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG049+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n005.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 04:15:18 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 28.01/4.32 % Refutation found
% 28.01/4.32 % SZS status Theorem for theBenchmark: Theorem is valid
% 28.01/4.32 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 28.01/4.35 % Elapsed time: 3.973160 seconds
% 28.01/4.35 % CPU time: 31.204168 seconds
% 28.01/4.35 % Total memory used: 286.101 MB
% 28.01/4.35 % Net memory used: 271.346 MB
%------------------------------------------------------------------------------