%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG081+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:18 PM UTC 2026
% Result : Theorem 0.12s 10.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG081+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/10.36 % Computer : n020.cluster.edu
% 0.07/10.36 % Model : x86_64 x86_64
% 0.07/10.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/10.36 % Memory : 8046.5625MB
% 0.07/10.36 % OS : Linux 6.8.0-71-generic
% 0.07/10.36 % CPULimit : 300
% 0.07/10.36 % WCLimit : 300
% 0.07/10.36 % DateTime : Mon Sep 21 04:19:29 UTC 2026
% 0.07/10.37 % CPUTime :
% 0.07/10.38 % Drodi V4.1.1
% 0.12/10.45 % Refutation found
% 0.12/10.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/10.45 % SZS output start CNFRefutation for theBenchmark
% 0.12/10.45 fof(f9,axiom,(
% 0.12/10.45 aScalar0(sz0z00) ),
% 0.12/10.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/10.45 fof(f13,axiom,(
% 0.12/10.45 (! [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 ) ) )),
% 0.12/10.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/10.45 fof(f20,axiom,(
% 0.12/10.45 (! [W0] :( aScalar0(W0)=> sdtlseqdt0(W0,W0) ) )),
% 0.12/10.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/10.45 fof(f35,axiom,(
% 0.12/10.45 (! [W0,W1] :( ( aVector0(W0)& aVector0(W1) )=> ( ( aDimensionOf0(W0) = aDimensionOf0(W1)& aDimensionOf0(W1) = sz00 )=> sdtasasdt0(W0,W1) = sz0z00 ) ) )),
% 0.12/10.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/10.45 fof(f38,hypothesis,(
% 0.12/10.45 ( aVector0(xs)& aVector0(xt) ) ),
% 0.12/10.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/10.45 fof(f40,hypothesis,(
% 0.12/10.45 aDimensionOf0(xs) = aDimensionOf0(xt) ),
% 0.12/10.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/10.45 fof(f41,conjecture,(
% 0.12/10.45 ( ( aDimensionOf0(xs) != sz00=> (? [W0] :( aVector0(W0)& szszuzczcdt0(aDimensionOf0(W0)) = aDimensionOf0(xs)& (! [W1] :( aNaturalNumber0(W1)=> sdtlbdtrb0(W0,W1) = sdtlbdtrb0(xs,W1) ))& W0 = sziznziztdt0(xs)& (? [W1] :( aVector0(W1)& szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(xt)& (! [W2] :( aNaturalNumber0(W2)=> sdtlbdtrb0(W1,W2) = sdtlbdtrb0(xt,W2) ))& W1 = sziznziztdt0(xt)& (? [W2] :( aScalar0(W2)& W2 = sdtlbdtrb0(xs,aDimensionOf0(xs))& (? [W3] :( aScalar0(W3)& W3 = sdtlbdtrb0(xt,aDimensionOf0(xt))& (? [W4] :( aScalar0(W4)& W4 = sdtasasdt0(W0,W0)& (? [W5] :( aScalar0(W5)& W5 = sdtasasdt0(W1,W1)& (? [W6] :( aScalar0(W6)& W6 = sdtasasdt0(W0,W1)& (? [W7] :( aScalar0(W7)& W7 = sdtasdt0(W2,W2)& (? [W8] :( aScalar0(W8)& W8 = sdtasdt0(W3,W3)& (? [W9] :( aScalar0(W9)& W9 = sdtasdt0(W2,W3)& (? [W10] :( aScalar0(W10)& W10 = sdtasdt0(W4,W8)& (? [W11] :( aScalar0(W11)& W11 = sdtasdt0(W6,W9)& (? [W12] :( aScalar0(W12)& W12 = sdtasdt0(W7,W5)& (? [W13] :( aScalar0(W13)& W13 = sdtasdt0(W10,W12)& sdtlseqdt0(sdtasdt0(W6,W6),sdtasdt0(W4,W5))& sdtlseqdt0(sdtpldt0(W11,W11),sdtpldt0(W10,W12))& sdtlseqdt0(sdtasdt0(sdtpldt0(W6,W9),sdtpldt0(W6,W9)),sdtasdt0(sdtpldt0(W4,W7),sdtpldt0(W5,W8)))& 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))) ) ),
% 0.12/10.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/10.45 fof(f42,negated_conjecture,(
% 0.12/10.45 ~(( ( aDimensionOf0(xs) != sz00=> (? [W0] :( aVector0(W0)& szszuzczcdt0(aDimensionOf0(W0)) = aDimensionOf0(xs)& (! [W1] :( aNaturalNumber0(W1)=> sdtlbdtrb0(W0,W1) = sdtlbdtrb0(xs,W1) ))& W0 = sziznziztdt0(xs)& (? [W1] :( aVector0(W1)& szszuzczcdt0(aDimensionOf0(W1)) = aDimensionOf0(xt)& (! [W2] :( aNaturalNumber0(W2)=> sdtlbdtrb0(W1,W2) = sdtlbdtrb0(xt,W2) ))& W1 = sziznziztdt0(xt)& (? [W2] :( aScalar0(W2)& W2 = sdtlbdtrb0(xs,aDimensionOf0(xs))& (? [W3] :( aScalar0(W3)& W3 = sdtlbdtrb0(xt,aDimensionOf0(xt))& (? [W4] :( aScalar0(W4)& W4 = sdtasasdt0(W0,W0)& (? [W5] :( aScalar0(W5)& W5 = sdtasasdt0(W1,W1)& (? [W6] :( aScalar0(W6)& W6 = sdtasasdt0(W0,W1)& (? [W7] :( aScalar0(W7)& W7 = sdtasdt0(W2,W2)& (? [W8] :( aScalar0(W8)& W8 = sdtasdt0(W3,W3)& (? [W9] :( aScalar0(W9)& W9 = sdtasdt0(W2,W3)& (? [W10] :( aScalar0(W10)& W10 = sdtasdt0(W4,W8)& (? [W11] :( aScalar0(W11)& W11 = sdtasdt0(W6,W9)& (? [W12] :( aScalar0(W12)& W12 = sdtasdt0(W7,W5)& (? [W13] :( aScalar0(W13)& W13 = sdtasdt0(W10,W12)& sdtlseqdt0(sdtasdt0(W6,W6),sdtasdt0(W4,W5))& sdtlseqdt0(sdtpldt0(W11,W11),sdtpldt0(W10,W12))& sdtlseqdt0(sdtasdt0(sdtpldt0(W6,W9),sdtpldt0(W6,W9)),sdtasdt0(sdtpldt0(W4,W7),sdtpldt0(W5,W8)))& 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))) ) )),
% 0.12/10.45 inference(negated_conjecture,[status(cth)],[f41])).
% 0.12/10.45 fof(f63,plain,(
% 0.12/10.45 aScalar0(sz0z00)),
% 0.12/10.45 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/10.45 fof(f70,plain,(
% 0.12/10.45 ![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))),
% 0.12/10.45 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.12/10.45 fof(f73,plain,(
% 0.12/10.45 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sz0z00)=sz0z00)),
% 0.12/10.45 inference(cnf_transformation,[status(thm)],[f70])).
% 0.12/10.45 fof(f96,plain,(
% 0.12/10.45 ![W0]: (~aScalar0(W0)|sdtlseqdt0(W0,W0))),
% 0.12/10.45 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.12/10.45 fof(f97,plain,(
% 0.12/10.45 ![X0]: (~aScalar0(X0)|sdtlseqdt0(X0,X0))),
% 0.12/10.45 inference(cnf_transformation,[status(thm)],[f96])).
% 0.12/10.45 fof(f135,plain,(
% 0.12/10.45 ![W0,W1]: ((~aVector0(W0)|~aVector0(W1))|((~aDimensionOf0(W0)=aDimensionOf0(W1)|~aDimensionOf0(W1)=sz00)|sdtasasdt0(W0,W1)=sz0z00))),
% 0.12/10.45 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.12/10.45 fof(f136,plain,(
% 0.12/10.45 ![X0,X1]: (~aVector0(X0)|~aVector0(X1)|~aDimensionOf0(X0)=aDimensionOf0(X1)|~aDimensionOf0(X1)=sz00|sdtasasdt0(X0,X1)=sz0z00)),
% 0.12/10.45 inference(cnf_transformation,[status(thm)],[f135])).
% 0.12/10.45 fof(f141,plain,(
% 0.12/10.45 aVector0(xs)),
% 0.12/10.45 inference(cnf_transformation,[status(thm)],[f38])).
% 0.12/10.45 fof(f142,plain,(
% 0.12/10.45 aVector0(xt)),
% 0.12/10.45 inference(cnf_transformation,[status(thm)],[f38])).
% 0.12/10.45 fof(f145,plain,(
% 0.12/10.45 aDimensionOf0(xs)=aDimensionOf0(xt)),
% 0.12/10.45 inference(cnf_transformation,[status(thm)],[f40])).
% 0.12/10.45 fof(f146,plain,(
% 0.12/10.45 ((aDimensionOf0(xs)=sz00|(?[W0]: ((((aVector0(W0)&szszuzczcdt0(aDimensionOf0(W0))=aDimensionOf0(xs))&(![W1]: (~aNaturalNumber0(W1)|sdtlbdtrb0(W0,W1)=sdtlbdtrb0(xs,W1))))&W0=sziznziztdt0(xs))&(?[W1]: ((((aVector0(W1)&szszuzczcdt0(aDimensionOf0(W1))=aDimensionOf0(xt))&(![W2]: (~aNaturalNumber0(W2)|sdtlbdtrb0(W1,W2)=sdtlbdtrb0(xt,W2))))&W1=sziznziztdt0(xt))&(?[W2]: ((aScalar0(W2)&W2=sdtlbdtrb0(xs,aDimensionOf0(xs)))&(?[W3]: ((aScalar0(W3)&W3=sdtlbdtrb0(xt,aDimensionOf0(xt)))&(?[W4]: ((aScalar0(W4)&W4=sdtasasdt0(W0,W0))&(?[W5]: ((aScalar0(W5)&W5=sdtasasdt0(W1,W1))&(?[W6]: ((aScalar0(W6)&W6=sdtasasdt0(W0,W1))&(?[W7]: ((aScalar0(W7)&W7=sdtasdt0(W2,W2))&(?[W8]: ((aScalar0(W8)&W8=sdtasdt0(W3,W3))&(?[W9]: ((aScalar0(W9)&W9=sdtasdt0(W2,W3))&(?[W10]: ((aScalar0(W10)&W10=sdtasdt0(W4,W8))&(?[W11]: ((aScalar0(W11)&W11=sdtasdt0(W6,W9))&(?[W12]: ((aScalar0(W12)&W12=sdtasdt0(W7,W5))&(?[W13]: (((((aScalar0(W13)&W13=sdtasdt0(W10,W12))&sdtlseqdt0(sdtasdt0(W6,W6),sdtasdt0(W4,W5)))&sdtlseqdt0(sdtpldt0(W11,W11),sdtpldt0(W10,W12)))&sdtlseqdt0(sdtasdt0(sdtpldt0(W6,W9),sdtpldt0(W6,W9)),sdtasdt0(sdtpldt0(W4,W7),sdtpldt0(W5,W8))))&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))))),
% 0.12/10.45 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.12/10.45 fof(f147,plain,(
% 0.12/10.45 (aDimensionOf0(xs)=sz00|(?[W0]: ((((aVector0(W0)&szszuzczcdt0(aDimensionOf0(W0))=aDimensionOf0(xs))&(![W1]: (~aNaturalNumber0(W1)|sdtlbdtrb0(W0,W1)=sdtlbdtrb0(xs,W1))))&W0=sziznziztdt0(xs))&(?[W1]: ((((aVector0(W1)&szszuzczcdt0(aDimensionOf0(W1))=aDimensionOf0(xt))&(![W2]: (~aNaturalNumber0(W2)|sdtlbdtrb0(W1,W2)=sdtlbdtrb0(xt,W2))))&W1=sziznziztdt0(xt))&(?[W2]: ((aScalar0(W2)&W2=sdtlbdtrb0(xs,aDimensionOf0(xs)))&(?[W3]: ((aScalar0(W3)&W3=sdtlbdtrb0(xt,aDimensionOf0(xt)))&(?[W4]: ((aScalar0(W4)&W4=sdtasasdt0(W0,W0))&(?[W5]: ((aScalar0(W5)&W5=sdtasasdt0(W1,W1))&(?[W6]: ((aScalar0(W6)&W6=sdtasasdt0(W0,W1))&(?[W7]: ((aScalar0(W7)&W7=sdtasdt0(W2,W2))&(?[W8]: ((aScalar0(W8)&W8=sdtasdt0(W3,W3))&(?[W9]: ((aScalar0(W9)&W9=sdtasdt0(W2,W3))&(?[W10]: ((aScalar0(W10)&W10=sdtasdt0(W4,W8))&(?[W11]: ((aScalar0(W11)&W11=sdtasdt0(W6,W9))&(?[W12]: ((aScalar0(W12)&W12=sdtasdt0(W7,W5))&(((((?[W13]: (aScalar0(W13)&W13=sdtasdt0(W10,W12)))&sdtlseqdt0(sdtasdt0(W6,W6),sdtasdt0(W4,W5)))&sdtlseqdt0(sdtpldt0(W11,W11),sdtpldt0(W10,W12)))&sdtlseqdt0(sdtasdt0(sdtpldt0(W6,W9),sdtpldt0(W6,W9)),sdtasdt0(sdtpldt0(W4,W7),sdtpldt0(W5,W8))))&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)))),
% 0.12/10.45 inference(miniscoping,[status(thm)],[f146])).
% 0.12/10.45 fof(f148,plain,(
% 0.12/10.45 (aDimensionOf0(xs)=sz00|((((aVector0(sK2_skl)&szszuzczcdt0(aDimensionOf0(sK2_skl))=aDimensionOf0(xs))&(![W1]: (~aNaturalNumber0(W1)|sdtlbdtrb0(sK2_skl,W1)=sdtlbdtrb0(xs,W1))))&sK2_skl=sziznziztdt0(xs))&((((aVector0(sK3_skl)&szszuzczcdt0(aDimensionOf0(sK3_skl))=aDimensionOf0(xt))&(![W2]: (~aNaturalNumber0(W2)|sdtlbdtrb0(sK3_skl,W2)=sdtlbdtrb0(xt,W2))))&sK3_skl=sziznziztdt0(xt))&((aScalar0(sK4_skl)&sK4_skl=sdtlbdtrb0(xs,aDimensionOf0(xs)))&((aScalar0(sK5_skl)&sK5_skl=sdtlbdtrb0(xt,aDimensionOf0(xt)))&((aScalar0(sK6_skl)&sK6_skl=sdtasasdt0(sK2_skl,sK2_skl))&((aScalar0(sK7_skl)&sK7_skl=sdtasasdt0(sK3_skl,sK3_skl))&((aScalar0(sK8_skl)&sK8_skl=sdtasasdt0(sK2_skl,sK3_skl))&((aScalar0(sK9_skl)&sK9_skl=sdtasdt0(sK4_skl,sK4_skl))&((aScalar0(sK10_skl)&sK10_skl=sdtasdt0(sK5_skl,sK5_skl))&((aScalar0(sK11_skl)&sK11_skl=sdtasdt0(sK4_skl,sK5_skl))&((aScalar0(sK12_skl)&sK12_skl=sdtasdt0(sK6_skl,sK10_skl))&((aScalar0(sK13_skl)&sK13_skl=sdtasdt0(sK8_skl,sK11_skl))&((aScalar0(sK14_skl)&sK14_skl=sdtasdt0(sK9_skl,sK7_skl))&(((((aScalar0(sK15_skl)&sK15_skl=sdtasdt0(sK12_skl,sK14_skl))&sdtlseqdt0(sdtasdt0(sK8_skl,sK8_skl),sdtasdt0(sK6_skl,sK7_skl)))&sdtlseqdt0(sdtpldt0(sK13_skl,sK13_skl),sdtpldt0(sK12_skl,sK14_skl)))&sdtlseqdt0(sdtasdt0(sdtpldt0(sK8_skl,sK11_skl),sdtpldt0(sK8_skl,sK11_skl)),sdtasdt0(sdtpldt0(sK6_skl,sK9_skl),sdtpldt0(sK7_skl,sK10_skl))))&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)))),
% 0.12/10.45 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])).
% 0.12/10.45 fof(f184,plain,(
% 0.12/10.45 aDimensionOf0(xs)=sz00|sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))),
% 0.12/10.45 inference(cnf_transformation,[status(thm)],[f148])).
% 0.12/10.45 fof(f185,plain,(
% 0.12/10.45 ~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))),
% 0.12/10.45 inference(cnf_transformation,[status(thm)],[f148])).
% 0.12/10.45 fof(f201,definition,(
% 0.12/10.45 sQ4_spl <=> (aDimensionOf0(xs)=sz00)),
% 0.12/10.45 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/10.45 fof(f202,plain,(
% 0.12/10.45 aDimensionOf0(xs)=sz00|~sQ4_spl),
% 0.12/10.45 inference(component_clause,[status(thm)],[f201])).
% 0.12/10.45 fof(f344,definition,(
% 0.12/10.45 sQ40_spl <=> (sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))))),
% 0.12/10.45 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.12/10.45 fof(f345,plain,(
% 0.12/10.45 sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))|~sQ40_spl),
% 0.12/10.45 inference(component_clause,[status(thm)],[f344])).
% 0.12/10.45 fof(f347,plain,(
% 0.12/10.45 sQ4_spl|sQ40_spl),
% 0.12/10.45 inference(split_clause,[status(thm)],[f184,f201,f344])).
% 0.12/10.45 fof(f387,plain,(
% 0.12/10.45 sdtlseqdt0(sz0z00,sz0z00)),
% 0.12/10.45 inference(resolution,[status(thm)],[f97,f63])).
% 0.12/10.45 fof(f403,definition,(
% 0.12/10.45 sQ47_spl <=> (aDimensionOf0(xt)=sz00)),
% 0.12/10.45 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.12/10.45 fof(f404,plain,(
% 0.12/10.45 aDimensionOf0(xt)=sz00|~sQ47_spl),
% 0.12/10.45 inference(component_clause,[status(thm)],[f403])).
% 0.12/10.45 fof(f417,plain,(
% 0.12/10.45 sz00=aDimensionOf0(xt)|~sQ4_spl),
% 0.12/10.45 inference(forward_demodulation,[status(thm)],[f202,f145])).
% 0.12/10.45 fof(f419,plain,(
% 0.12/10.45 sdtasdt0(sz0z00,sz0z00)=sz0z00),
% 0.12/10.45 inference(resolution,[status(thm)],[f73,f63])).
% 0.12/10.45 fof(f640,plain,(
% 0.12/10.45 ![X0]: (~aVector0(X0)|~aDimensionOf0(xt)=aDimensionOf0(X0)|~aDimensionOf0(X0)=sz00|sdtasasdt0(xt,X0)=sz0z00)),
% 0.12/10.45 inference(resolution,[status(thm)],[f136,f142])).
% 0.12/10.45 fof(f641,plain,(
% 0.12/10.45 ![X0]: (~aVector0(X0)|~aDimensionOf0(xs)=aDimensionOf0(X0)|~aDimensionOf0(X0)=sz00|sdtasasdt0(xs,X0)=sz0z00)),
% 0.12/10.45 inference(resolution,[status(thm)],[f136,f141])).
% 0.12/10.45 fof(f644,plain,(
% 0.12/10.45 ![X0]: (~aVector0(X0)|~sz00=aDimensionOf0(X0)|~aDimensionOf0(X0)=sz00|sdtasasdt0(xs,X0)=sz0z00|~sQ4_spl)),
% 0.12/10.45 inference(forward_demodulation,[status(thm)],[f202,f641])).
% 0.12/10.45 fof(f645,plain,(
% 0.12/10.45 ![X0]: (~aVector0(X0)|~sz00=aDimensionOf0(X0)|sdtasasdt0(xs,X0)=sz0z00|~sQ4_spl)),
% 0.12/10.45 inference(duplicate_literals_removal,[status(thm)],[f644])).
% 0.12/10.45 fof(f706,plain,(
% 0.12/10.45 $false|~sQ40_spl),
% 0.12/10.45 inference(forward_subsumption_resolution,[status(thm)],[f345,f185])).
% 0.12/10.45 fof(f707,plain,(
% 0.12/10.45 ~sQ40_spl),
% 0.12/10.45 inference(contradiction_clause,[status(thm)],[f706])).
% 0.12/10.45 fof(f708,plain,(
% 0.12/10.45 sQ47_spl|~sQ4_spl),
% 0.12/10.45 inference(split_clause,[status(thm)],[f417,f403,f201])).
% 0.12/10.45 fof(f792,plain,(
% 0.12/10.45 ~sz00=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sz0z00|~sQ4_spl),
% 0.12/10.45 inference(resolution,[status(thm)],[f645,f142])).
% 0.12/10.45 fof(f793,plain,(
% 0.12/10.45 ~sz00=aDimensionOf0(xs)|sdtasasdt0(xs,xs)=sz0z00|~sQ4_spl),
% 0.12/10.45 inference(resolution,[status(thm)],[f645,f141])).
% 0.12/10.45 fof(f794,definition,(
% 0.12/10.45 sQ83_spl <=> (sdtasasdt0(xs,xt)=sz0z00)),
% 0.12/10.45 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.12/10.45 fof(f795,plain,(
% 0.12/10.45 sdtasasdt0(xs,xt)=sz0z00|~sQ83_spl),
% 0.12/10.45 inference(component_clause,[status(thm)],[f794])).
% 0.12/10.45 fof(f797,plain,(
% 0.12/10.45 ~sQ47_spl|sQ83_spl|~sQ4_spl),
% 0.12/10.45 inference(split_clause,[status(thm)],[f792,f403,f794,f201])).
% 0.12/10.45 fof(f798,definition,(
% 0.12/10.45 sQ84_spl <=> (sdtasasdt0(xs,xs)=sz0z00)),
% 0.12/10.45 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 0.12/10.45 fof(f799,plain,(
% 0.12/10.45 sdtasasdt0(xs,xs)=sz0z00|~sQ84_spl),
% 0.12/10.45 inference(component_clause,[status(thm)],[f798])).
% 0.12/10.45 fof(f801,plain,(
% 0.12/10.45 ~sQ4_spl|sQ84_spl),
% 0.12/10.45 inference(split_clause,[status(thm)],[f793,f201,f798])).
% 0.12/10.45 fof(f832,plain,(
% 0.12/10.45 ~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sz0z00),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))|~sQ83_spl),
% 0.12/10.45 inference(backward_demodulation,[status(thm)],[f795,f185])).
% 0.12/10.45 fof(f833,plain,(
% 0.12/10.45 ~sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))|~sQ83_spl),
% 0.12/10.45 inference(forward_demodulation,[status(thm)],[f795,f832])).
% 0.12/10.45 fof(f834,plain,(
% 0.12/10.45 ~sdtlseqdt0(sz0z00,sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))|~sQ83_spl),
% 0.12/10.45 inference(forward_demodulation,[status(thm)],[f419,f833])).
% 0.12/10.45 fof(f845,plain,(
% 0.12/10.45 ~sdtlseqdt0(sz0z00,sdtasdt0(sz0z00,sdtasasdt0(xt,xt)))|~sQ84_spl|~sQ83_spl),
% 0.12/10.45 inference(backward_demodulation,[status(thm)],[f799,f834])).
% 0.12/10.45 fof(f1084,definition,(
% 0.12/10.45 sQ109_spl <=> (sz0z00=sdtasasdt0(xt,xt))),
% 0.12/10.45 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.12/10.45 fof(f1085,plain,(
% 0.12/10.45 sz0z00=sdtasasdt0(xt,xt)|~sQ109_spl),
% 0.12/10.45 inference(component_clause,[status(thm)],[f1084])).
% 0.12/10.45 fof(f1128,plain,(
% 0.12/10.45 ![X0]: (~aVector0(X0)|~sz00=aDimensionOf0(X0)|~aDimensionOf0(X0)=sz00|sdtasasdt0(xt,X0)=sz0z00|~sQ47_spl)),
% 0.12/10.45 inference(forward_demodulation,[status(thm)],[f404,f640])).
% 0.12/10.45 fof(f1129,plain,(
% 0.12/10.45 ![X0]: (~aVector0(X0)|~sz00=aDimensionOf0(X0)|sdtasasdt0(xt,X0)=sz0z00|~sQ47_spl)),
% 0.12/10.45 inference(duplicate_literals_removal,[status(thm)],[f1128])).
% 0.12/10.45 fof(f1130,plain,(
% 0.12/10.45 ~sz00=aDimensionOf0(xt)|sdtasasdt0(xt,xt)=sz0z00|~sQ47_spl),
% 0.12/10.45 inference(resolution,[status(thm)],[f1129,f142])).
% 0.12/10.45 fof(f1132,plain,(
% 0.12/10.45 ~sQ47_spl|sQ109_spl),
% 0.12/10.45 inference(split_clause,[status(thm)],[f1130,f403,f1084])).
% 0.12/10.45 fof(f1147,plain,(
% 0.12/10.45 ~sdtlseqdt0(sz0z00,sdtasdt0(sz0z00,sz0z00))|~sQ109_spl|~sQ84_spl|~sQ83_spl),
% 0.12/10.45 inference(backward_demodulation,[status(thm)],[f1085,f845])).
% 0.12/10.45 fof(f1148,plain,(
% 0.12/10.45 ~sdtlseqdt0(sz0z00,sz0z00)|~sQ109_spl|~sQ84_spl|~sQ83_spl),
% 0.12/10.45 inference(forward_demodulation,[status(thm)],[f419,f1147])).
% 0.12/10.45 fof(f1149,plain,(
% 0.12/10.45 $false|~sQ109_spl|~sQ84_spl|~sQ83_spl),
% 0.12/10.45 inference(forward_subsumption_resolution,[status(thm)],[f1148,f387])).
% 0.12/10.46 fof(f1150,plain,(
% 0.12/10.46 ~sQ109_spl|~sQ84_spl|~sQ83_spl),
% 0.12/10.46 inference(contradiction_clause,[status(thm)],[f1149])).
% 0.12/10.46 fof(f1151,plain,(
% 0.12/10.46 $false),
% 0.12/10.46 inference(sat_refutation,[status(thm)],[f347,f707,f708,f797,f801,f1132,f1150])).
% 0.12/10.46 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/10.48 % Elapsed time: 0.094286 seconds
% 0.12/10.48 % CPU time: 0.502952 seconds
% 0.12/10.48 % Total memory used: 113.907 MB
% 0.12/10.48 % Net memory used: 113.310 MB
%------------------------------------------------------------------------------