%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG049+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:05:13 PM UTC 2026
% Result : Theorem 11.71s 1.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG049+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 04:15:42 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 11.71/1.99 % Refutation found
% 11.71/1.99 % SZS status Theorem for theBenchmark: Theorem is valid
% 11.71/1.99 % SZS output start CNFRefutation for theBenchmark
% 11.71/1.99 fof(f9,axiom,(
% 11.71/1.99 aScalar0(sz0z00) ),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f11,axiom,(
% 11.71/1.99 (! [W0,W1] :( ( aScalar0(W0)& aScalar0(W1) )=> aScalar0(sdtasdt0(W0,W1)) ) )),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f13,axiom,(
% 11.71/1.99 (! [W0] :( aScalar0(W0)=> ( sdtpldt0(W0,sz0z00) = W0& sdtpldt0(sz0z00,W0) = W0& sdtasdt0(W0,sz0z00) = sz0z00& sdtasdt0(sz0z00,W0) = sz0z00& sdtpldt0(W0,smndt0(W0)) = sz0z00& sdtpldt0(smndt0(W0),W0) = sz0z00& smndt0(smndt0(W0)) = W0& smndt0(sz0z00) = sz0z00 ) ) )),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f23,axiom,(
% 11.71/1.99 (! [W0,W1,W2,W3] :( ( aScalar0(W0)& aScalar0(W1)& aScalar0(W2)& aScalar0(W3) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W2,W3) )=> sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W3)) ) ) )),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f30,axiom,(
% 11.71/1.99 (! [W0] :( aVector0(W0)=> aNaturalNumber0(aDimensionOf0(W0)) ) )),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f31,axiom,(
% 11.71/1.99 (! [W0,W1] :( ( aVector0(W0)& aNaturalNumber0(W1) )=> aScalar0(sdtlbdtrb0(W0,W1)) ) )),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f32,definition,(
% 11.71/1.99 (! [W0] :( aVector0(W0)=> ( aDimensionOf0(W0) != sz00=> (! [W1] :( W1 = sziznziztdt0(W0)<=> ( aVector0(W1)& szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(W0)& (! [W2] :( aNaturalNumber0(W2)=> sdtlbdtrb0(W1,W2) = sdtlbdtrb0(W0,W2) ) )) ) )) ) )),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f33,axiom,(
% 11.71/1.99 (! [W0,W1] :( ( aVector0(W0)& aVector0(W1) )=> ( ( aDimensionOf0(W0) = aDimensionOf0(W1)& aDimensionOf0(W1) != sz00 )=> aDimensionOf0(sziznziztdt0(W0)) = aDimensionOf0(sziznziztdt0(W1)) ) ) )),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f34,axiom,(
% 11.71/1.99 (! [W0,W1] :( ( aVector0(W0)& aVector0(W1) )=> ( aDimensionOf0(W0) = aDimensionOf0(W1)=> aScalar0(sdtasasdt0(W0,W1)) ) ) )),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f37,hypothesis,(
% 11.71/1.99 aVector0(xs) ),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f39,hypothesis,(
% 11.71/1.99 aDimensionOf0(xs) != sz00 ),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f40,hypothesis,(
% 11.71/1.99 sdtasasdt0(xs,xs) = sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f41,hypothesis,(
% 11.71/1.99 ( sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))& sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))) ) ),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f42,conjecture,(
% 11.71/1.99 sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) ),
% 11.71/1.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.71/1.99 fof(f43,negated_conjecture,(
% 11.71/1.99 ~(sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)) )),
% 11.71/1.99 inference(negated_conjecture,[status(cth)],[f42])).
% 11.71/1.99 fof(f64,plain,(
% 11.71/1.99 aScalar0(sz0z00)),
% 11.71/1.99 inference(cnf_transformation,[status(thm)],[f9])).
% 11.71/1.99 fof(f67,plain,(
% 11.71/1.99 ![W0,W1]: ((~aScalar0(W0)|~aScalar0(W1))|aScalar0(sdtasdt0(W0,W1)))),
% 11.71/1.99 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 11.71/1.99 fof(f68,plain,(
% 11.71/1.99 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|aScalar0(sdtasdt0(X0,X1)))),
% 11.71/1.99 inference(cnf_transformation,[status(thm)],[f67])).
% 11.71/1.99 fof(f71,plain,(
% 11.71/1.99 ![W0]: (~aScalar0(W0)|(((((((sdtpldt0(W0,sz0z00)=W0&sdtpldt0(sz0z00,W0)=W0)&sdtasdt0(W0,sz0z00)=sz0z00)&sdtasdt0(sz0z00,W0)=sz0z00)&sdtpldt0(W0,smndt0(W0))=sz0z00)&sdtpldt0(smndt0(W0),W0)=sz0z00)&smndt0(smndt0(W0))=W0)&smndt0(sz0z00)=sz0z00))),
% 11.71/1.99 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 11.71/1.99 fof(f72,plain,(
% 11.71/1.99 ![X0]: (~aScalar0(X0)|sdtpldt0(X0,sz0z00)=X0)),
% 11.71/1.99 inference(cnf_transformation,[status(thm)],[f71])).
% 11.71/1.99 fof(f103,plain,(
% 11.71/1.99 ![W0,W1,W2,W3]: ((((~aScalar0(W0)|~aScalar0(W1))|~aScalar0(W2))|~aScalar0(W3))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W2,W3))|sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W3))))),
% 11.71/1.99 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 11.71/2.01 fof(f104,plain,(
% 11.71/2.01 ![X0,X1,X2,X3]: (~aScalar0(X0)|~aScalar0(X1)|~aScalar0(X2)|~aScalar0(X3)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X2,X3)|sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3)))),
% 11.71/2.01 inference(cnf_transformation,[status(thm)],[f103])).
% 11.71/2.01 fof(f119,plain,(
% 11.71/2.01 ![W0]: (~aVector0(W0)|aNaturalNumber0(aDimensionOf0(W0)))),
% 11.71/2.01 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 11.71/2.01 fof(f120,plain,(
% 11.71/2.01 ![X0]: (~aVector0(X0)|aNaturalNumber0(aDimensionOf0(X0)))),
% 11.71/2.01 inference(cnf_transformation,[status(thm)],[f119])).
% 11.71/2.01 fof(f121,plain,(
% 11.71/2.01 ![W0,W1]: ((~aVector0(W0)|~aNaturalNumber0(W1))|aScalar0(sdtlbdtrb0(W0,W1)))),
% 11.71/2.01 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 11.71/2.01 fof(f122,plain,(
% 11.71/2.01 ![X0,X1]: (~aVector0(X0)|~aNaturalNumber0(X1)|aScalar0(sdtlbdtrb0(X0,X1)))),
% 11.71/2.01 inference(cnf_transformation,[status(thm)],[f121])).
% 11.71/2.01 fof(f123,plain,(
% 11.71/2.01 ![W0]: (~aVector0(W0)|(aDimensionOf0(W0)=sz00|(![W1]: (W1=sziznziztdt0(W0)<=>((aVector0(W1)&szszuzczcdt0(aDimensionOf0(W1))=aDimensionOf0(W0))&(![W2]: (~aNaturalNumber0(W2)|sdtlbdtrb0(W1,W2)=sdtlbdtrb0(W0,W2))))))))),
% 11.71/2.01 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 11.71/2.01 fof(f124,plain,(
% 11.71/2.01 ![W0]: (~aVector0(W0)|(aDimensionOf0(W0)=sz00|(![W1]: ((~W1=sziznziztdt0(W0)|((aVector0(W1)&szszuzczcdt0(aDimensionOf0(W1))=aDimensionOf0(W0))&(![W2]: (~aNaturalNumber0(W2)|sdtlbdtrb0(W1,W2)=sdtlbdtrb0(W0,W2)))))&(W1=sziznziztdt0(W0)|((~aVector0(W1)|~szszuzczcdt0(aDimensionOf0(W1))=aDimensionOf0(W0))|(?[W2]: (aNaturalNumber0(W2)&~sdtlbdtrb0(W1,W2)=sdtlbdtrb0(W0,W2)))))))))),
% 11.71/2.01 inference(NNF_transformation,[status(thm)],[f123])).
% 11.71/2.01 fof(f125,plain,(
% 11.71/2.01 ![W0]: (~aVector0(W0)|(aDimensionOf0(W0)=sz00|((![W1]: (~W1=sziznziztdt0(W0)|((aVector0(W1)&szszuzczcdt0(aDimensionOf0(W1))=aDimensionOf0(W0))&(![W2]: (~aNaturalNumber0(W2)|sdtlbdtrb0(W1,W2)=sdtlbdtrb0(W0,W2))))))&(![W1]: (W1=sziznziztdt0(W0)|((~aVector0(W1)|~szszuzczcdt0(aDimensionOf0(W1))=aDimensionOf0(W0))|(?[W2]: (aNaturalNumber0(W2)&~sdtlbdtrb0(W1,W2)=sdtlbdtrb0(W0,W2)))))))))),
% 11.71/2.01 inference(miniscoping,[status(thm)],[f124])).
% 11.71/2.01 fof(f126,plain,(
% 11.71/2.01 ![W0]: (~aVector0(W0)|(aDimensionOf0(W0)=sz00|((![W1]: (~W1=sziznziztdt0(W0)|((aVector0(W1)&szszuzczcdt0(aDimensionOf0(W1))=aDimensionOf0(W0))&(![W2]: (~aNaturalNumber0(W2)|sdtlbdtrb0(W1,W2)=sdtlbdtrb0(W0,W2))))))&(![W1]: (W1=sziznziztdt0(W0)|((~aVector0(W1)|~szszuzczcdt0(aDimensionOf0(W1))=aDimensionOf0(W0))|(aNaturalNumber0(sK1_skl(W1,W0))&~sdtlbdtrb0(W1,sK1_skl(W1,W0))=sdtlbdtrb0(W0,sK1_skl(W1,W0)))))))))),
% 11.71/2.01 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f125])).
% 11.71/2.01 fof(f127,plain,(
% 11.71/2.01 ![X0,X1]: (~aVector0(X0)|aDimensionOf0(X0)=sz00|~X1=sziznziztdt0(X0)|aVector0(X1))),
% 11.71/2.01 inference(cnf_transformation,[status(thm)],[f126])).
% 11.71/2.01 fof(f132,plain,(
% 11.71/2.01 ![W0,W1]: ((~aVector0(W0)|~aVector0(W1))|((~aDimensionOf0(W0)=aDimensionOf0(W1)|aDimensionOf0(W1)=sz00)|aDimensionOf0(sziznziztdt0(W0))=aDimensionOf0(sziznziztdt0(W1))))),
% 11.71/2.01 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 11.71/2.01 fof(f133,plain,(
% 11.71/2.01 ![X0,X1]: (~aVector0(X0)|~aVector0(X1)|~aDimensionOf0(X0)=aDimensionOf0(X1)|aDimensionOf0(X1)=sz00|aDimensionOf0(sziznziztdt0(X0))=aDimensionOf0(sziznziztdt0(X1)))),
% 11.71/2.01 inference(cnf_transformation,[status(thm)],[f132])).
% 11.71/2.01 fof(f134,plain,(
% 11.71/2.01 ![W0,W1]: ((~aVector0(W0)|~aVector0(W1))|(~aDimensionOf0(W0)=aDimensionOf0(W1)|aScalar0(sdtasasdt0(W0,W1))))),
% 11.71/2.01 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 11.71/2.01 fof(f135,plain,(
% 11.71/2.01 ![X0,X1]: (~aVector0(X0)|~aVector0(X1)|~aDimensionOf0(X0)=aDimensionOf0(X1)|aScalar0(sdtasasdt0(X0,X1)))),
% 11.71/2.01 inference(cnf_transformation,[status(thm)],[f134])).
% 11.71/2.01 fof(f140,plain,(
% 11.71/2.01 aVector0(xs)),
% 11.71/2.01 inference(cnf_transformation,[status(thm)],[f37])).
% 11.71/2.01 fof(f143,plain,(
% 11.71/2.01 ~aDimensionOf0(xs)=sz00),
% 11.71/2.01 inference(cnf_transformation,[status(thm)],[f39])).
% 11.71/2.01 fof(f144,plain,(
% 11.71/2.01 sdtasasdt0(xs,xs)=sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),
% 11.71/2.01 inference(cnf_transformation,[status(thm)],[f40])).
% 11.71/2.01 fof(f145,plain,(
% 11.71/2.01 sdtlseqdt0(sz0z00,sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))),
% 11.71/2.01 inference(cnf_transformation,[status(thm)],[f41])).
% 11.71/2.01 fof(f146,plain,(
% 11.71/2.01 sdtlseqdt0(sz0z00,sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),
% 11.71/2.01 inference(cnf_transformation,[status(thm)],[f41])).
% 11.71/2.01 fof(f147,plain,(
% 11.71/2.01 ~sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs))),
% 11.71/2.01 inference(cnf_transformation,[status(thm)],[f43])).
% 11.71/2.01 fof(f179,definition,(
% 11.71/2.01 sQ6_spl <=> (aScalar0(sz0z00))),
% 11.71/2.01 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 11.71/2.01 fof(f181,plain,(
% 11.71/2.01 ~aScalar0(sz0z00)|sQ6_spl),
% 11.71/2.01 inference(component_clause,[status(thm)],[f179])).
% 11.71/2.01 fof(f195,plain,(
% 11.71/2.01 $false|sQ6_spl),
% 11.71/2.01 inference(forward_subsumption_resolution,[status(thm)],[f181,f64])).
% 11.71/2.01 fof(f196,plain,(
% 11.71/2.01 sQ6_spl),
% 11.71/2.01 inference(contradiction_clause,[status(thm)],[f195])).
% 11.71/2.01 fof(f244,plain,(
% 11.71/2.01 sdtpldt0(sz0z00,sz0z00)=sz0z00),
% 11.71/2.01 inference(resolution,[status(thm)],[f72,f64])).
% 11.71/2.01 fof(f257,plain,(
% 11.71/2.01 aNaturalNumber0(aDimensionOf0(xs))),
% 11.71/2.01 inference(resolution,[status(thm)],[f120,f140])).
% 11.71/2.01 fof(f264,definition,(
% 11.71/2.01 sQ17_spl <=> (aDimensionOf0(xs)=sz00)),
% 11.71/2.01 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 11.71/2.01 fof(f265,plain,(
% 11.71/2.01 aDimensionOf0(xs)=sz00|~sQ17_spl),
% 11.71/2.01 inference(component_clause,[status(thm)],[f264])).
% 11.71/2.01 fof(f275,plain,(
% 11.71/2.01 $false|~sQ17_spl),
% 11.71/2.01 inference(forward_subsumption_resolution,[status(thm)],[f265,f143])).
% 11.71/2.01 fof(f276,plain,(
% 11.71/2.01 ~sQ17_spl),
% 11.71/2.01 inference(contradiction_clause,[status(thm)],[f275])).
% 11.71/2.01 fof(f324,definition,(
% 11.71/2.01 sQ26_spl <=> (aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs))))),
% 11.71/2.01 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 11.71/2.01 fof(f413,definition,(
% 11.71/2.01 sQ42_spl <=> (aDimensionOf0(xs)=aDimensionOf0(xs))),
% 11.71/2.01 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 11.71/2.01 fof(f415,plain,(
% 11.71/2.01 ~aDimensionOf0(xs)=aDimensionOf0(xs)|sQ42_spl),
% 11.71/2.01 inference(component_clause,[status(thm)],[f413])).
% 11.71/2.01 fof(f420,plain,(
% 11.71/2.01 $false|sQ42_spl),
% 11.71/2.01 inference(trivial_equality_resolution,[status(thm)],[f415])).
% 11.71/2.01 fof(f421,plain,(
% 11.71/2.01 sQ42_spl),
% 11.71/2.01 inference(contradiction_clause,[status(thm)],[f420])).
% 11.71/2.01 fof(f593,plain,(
% 11.71/2.01 ![X0,X1]: (~aScalar0(sz0z00)|~aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))|~aScalar0(X0)|~aScalar0(X1)|~sdtlseqdt0(X0,X1)|sdtlseqdt0(sdtpldt0(sz0z00,X0),sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),X1)))),
% 11.71/2.01 inference(resolution,[status(thm)],[f104,f145])).
% 11.71/2.01 fof(f599,definition,(
% 11.71/2.01 ![X0,X1]: (sQ62_spl <=> (~aScalar0(X0)|~aScalar0(X1)|~sdtlseqdt0(X0,X1)|sdtlseqdt0(sdtpldt0(sz0z00,X0),sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),X1))))),
% 11.71/2.01 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 11.71/2.01 fof(f600,plain,(
% 11.71/2.01 ![X0,X1]: (~aScalar0(X0)|~aScalar0(X1)|~sdtlseqdt0(X0,X1)|sdtlseqdt0(sdtpldt0(sz0z00,X0),sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),X1))|~sQ62_spl)),
% 11.71/2.01 inference(component_clause,[status(thm)],[f599])).
% 11.71/2.01 fof(f602,plain,(
% 11.71/2.01 ~sQ6_spl|~sQ26_spl|sQ62_spl),
% 11.71/2.01 inference(split_clause,[status(thm)],[f593,f179,f324,f599])).
% 11.71/2.01 fof(f617,plain,(
% 11.71/2.01 ![X0]: (~aNaturalNumber0(X0)|aScalar0(sdtlbdtrb0(xs,X0)))),
% 11.71/2.01 inference(resolution,[status(thm)],[f122,f140])).
% 11.71/2.01 fof(f618,plain,(
% 11.71/2.01 aScalar0(sdtlbdtrb0(xs,aDimensionOf0(xs)))),
% 11.71/2.01 inference(resolution,[status(thm)],[f617,f257])).
% 11.71/2.01 fof(f686,plain,(
% 11.71/2.01 ![X0]: (~aScalar0(X0)|aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),X0)))),
% 11.71/2.01 inference(resolution,[status(thm)],[f618,f68])).
% 11.71/2.01 fof(f832,plain,(
% 11.71/2.01 ![X0]: (aDimensionOf0(xs)=sz00|~X0=sziznziztdt0(xs)|aVector0(X0))),
% 11.71/2.01 inference(resolution,[status(thm)],[f127,f140])).
% 11.71/2.01 fof(f833,definition,(
% 11.71/2.01 ![X0]: (sQ82_spl <=> (~X0=sziznziztdt0(xs)|aVector0(X0)))),
% 11.71/2.01 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 11.71/2.01 fof(f834,plain,(
% 11.71/2.01 ![X0]: (~X0=sziznziztdt0(xs)|aVector0(X0)|~sQ82_spl)),
% 11.71/2.01 inference(component_clause,[status(thm)],[f833])).
% 11.71/2.01 fof(f836,plain,(
% 11.71/2.01 sQ17_spl|sQ82_spl),
% 11.71/2.01 inference(split_clause,[status(thm)],[f832,f264,f833])).
% 11.71/2.01 fof(f847,plain,(
% 11.71/2.01 aVector0(sziznziztdt0(xs))|~sQ82_spl),
% 11.71/2.01 inference(equality_resolution,[status(thm)],[f834])).
% 6.12/2.02 fof(f865,plain,(
% 6.12/2.02 ![X0]: (~aVector0(X0)|~aDimensionOf0(sziznziztdt0(xs))=aDimensionOf0(X0)|aScalar0(sdtasasdt0(sziznziztdt0(xs),X0))|~sQ82_spl)),
% 6.12/2.02 inference(resolution,[status(thm)],[f847,f135])).
% 6.12/2.02 fof(f959,plain,(
% 6.12/2.02 ![X0]: (~aVector0(X0)|~aDimensionOf0(xs)=aDimensionOf0(X0)|aDimensionOf0(X0)=sz00|aDimensionOf0(sziznziztdt0(xs))=aDimensionOf0(sziznziztdt0(X0)))),
% 6.12/2.02 inference(resolution,[status(thm)],[f133,f140])).
% 6.12/2.02 fof(f1064,definition,(
% 6.12/2.02 sQ111_spl <=> (aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))),
% 6.12/2.02 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 6.12/2.02 fof(f1066,plain,(
% 6.12/2.02 ~aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))|sQ111_spl),
% 6.12/2.02 inference(component_clause,[status(thm)],[f1064])).
% 6.12/2.02 fof(f1268,plain,(
% 6.12/2.02 ~aScalar0(sz0z00)|~aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))|sdtlseqdt0(sdtpldt0(sz0z00,sz0z00),sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))|~sQ62_spl),
% 6.12/2.02 inference(resolution,[status(thm)],[f600,f146])).
% 6.12/2.02 fof(f1275,definition,(
% 6.12/2.02 sQ145_spl <=> (sdtlseqdt0(sdtpldt0(sz0z00,sz0z00),sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))))),
% 6.12/2.02 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 6.12/2.02 fof(f1276,plain,(
% 6.12/2.02 sdtlseqdt0(sdtpldt0(sz0z00,sz0z00),sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))|~sQ145_spl),
% 6.12/2.02 inference(component_clause,[status(thm)],[f1275])).
% 6.12/2.02 fof(f1278,plain,(
% 6.12/2.02 ~sQ6_spl|~sQ111_spl|sQ145_spl|~sQ62_spl),
% 6.12/2.02 inference(split_clause,[status(thm)],[f1268,f179,f1064,f1275,f599])).
% 6.12/2.02 fof(f1554,plain,(
% 6.12/2.02 ~aDimensionOf0(xs)=aDimensionOf0(xs)|aDimensionOf0(xs)=sz00|aDimensionOf0(sziznziztdt0(xs))=aDimensionOf0(sziznziztdt0(xs))),
% 6.12/2.02 inference(resolution,[status(thm)],[f959,f140])).
% 6.12/2.02 fof(f1563,definition,(
% 6.12/2.02 sQ172_spl <=> (aDimensionOf0(sziznziztdt0(xs))=aDimensionOf0(sziznziztdt0(xs)))),
% 6.12/2.02 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 6.12/2.02 fof(f1566,plain,(
% 6.12/2.02 ~sQ42_spl|sQ17_spl|sQ172_spl),
% 6.12/2.02 inference(split_clause,[status(thm)],[f1554,f413,f264,f1563])).
% 6.12/2.02 fof(f2481,plain,(
% 6.12/2.02 aScalar0(sdtlbdtrb0(xs,aDimensionOf0(xs)))),
% 6.12/2.02 inference(resolution,[status(thm)],[f257,f617])).
% 6.12/2.02 fof(f5940,plain,(
% 6.12/2.02 aScalar0(sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs))))),
% 6.12/2.02 inference(resolution,[status(thm)],[f686,f2481])).
% 6.12/2.02 fof(f5950,plain,(
% 6.12/2.02 $false|sQ111_spl),
% 6.12/2.02 inference(forward_subsumption_resolution,[status(thm)],[f5940,f1066])).
% 6.12/2.02 fof(f5951,plain,(
% 6.12/2.02 sQ111_spl),
% 6.12/2.02 inference(contradiction_clause,[status(thm)],[f5950])).
% 6.12/2.02 fof(f12891,plain,(
% 6.12/2.02 ~aDimensionOf0(sziznziztdt0(xs))=aDimensionOf0(sziznziztdt0(xs))|aScalar0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)))|~sQ82_spl),
% 6.12/2.02 inference(resolution,[status(thm)],[f865,f847])).
% 6.12/2.02 fof(f12897,plain,(
% 6.12/2.02 ~sQ172_spl|sQ26_spl|~sQ82_spl),
% 6.12/2.02 inference(split_clause,[status(thm)],[f12891,f1563,f324,f833])).
% 6.12/2.02 fof(f12903,plain,(
% 6.12/2.02 sdtlseqdt0(sz0z00,sdtpldt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),sdtasdt0(sdtlbdtrb0(xs,aDimensionOf0(xs)),sdtlbdtrb0(xs,aDimensionOf0(xs)))))|~sQ145_spl),
% 6.12/2.02 inference(forward_demodulation,[status(thm)],[f244,f1276])).
% 6.12/2.02 fof(f12904,plain,(
% 6.12/2.02 sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs))|~sQ145_spl),
% 6.12/2.02 inference(forward_demodulation,[status(thm)],[f144,f12903])).
% 6.12/2.02 fof(f12905,plain,(
% 6.12/2.02 $false|~sQ145_spl),
% 6.12/2.02 inference(forward_subsumption_resolution,[status(thm)],[f12904,f147])).
% 6.12/2.02 fof(f12906,plain,(
% 6.12/2.02 ~sQ145_spl),
% 6.12/2.02 inference(contradiction_clause,[status(thm)],[f12905])).
% 6.12/2.02 fof(f12907,plain,(
% 6.12/2.02 $false),
% 6.12/2.02 inference(sat_refutation,[status(thm)],[f196,f276,f421,f602,f836,f1278,f1566,f5951,f12897,f12906])).
% 6.12/2.02 % SZS output end CNFRefutation for theBenchmark.p
% 6.12/2.04 % Elapsed time: 1.649128 seconds
% 6.12/2.04 % CPU time: 12.726877 seconds
% 6.12/2.04 % Total memory used: 255.582 MB
% 6.12/2.04 % Net memory used: 245.702 MB
%------------------------------------------------------------------------------