%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG081+1 : 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 : n002.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.13s 5.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG081+1 : 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.09/5.36 % Computer : n002.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 04:21:22 UTC 2026
% 0.09/5.36 % CPUTime :
% 0.09/5.37 % Drodi V4.1.1
% 0.13/5.50 % Refutation found
% 0.13/5.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/5.50 % SZS output start CNFRefutation for theBenchmark
% 0.13/5.50 fof(f9,axiom,(
% 0.13/5.50 aScalar0(sz0z00) ),
% 0.13/5.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.50 fof(f13,axiom,(
% 0.13/5.50 (! [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.13/5.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.50 fof(f20,axiom,(
% 0.13/5.50 (! [W0] :( aScalar0(W0)=> sdtlseqdt0(W0,W0) ) )),
% 0.13/5.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.50 fof(f35,axiom,(
% 0.13/5.50 (! [W0,W1] :( ( aVector0(W0)& aVector0(W1) )=> ( ( aDimensionOf0(W0) = aDimensionOf0(W1)& aDimensionOf0(W1) = sz00 )=> sdtasasdt0(W0,W1) = sz0z00 ) ) )),
% 0.13/5.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.50 fof(f38,hypothesis,(
% 0.13/5.50 ( aVector0(xs)& aVector0(xt) ) ),
% 0.13/5.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.50 fof(f40,hypothesis,(
% 0.13/5.50 aDimensionOf0(xs) = aDimensionOf0(xt) ),
% 0.13/5.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.50 fof(f41,conjecture,(
% 0.13/5.50 ( ( aDimensionOf0(xs) != sz00=> (? [W0] :( aVector0(W0)& W0 = sziznziztdt0(xs)& (? [W1] :( aVector0(W1)& 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.13/5.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.50 fof(f42,negated_conjecture,(
% 0.13/5.50 ~(( ( aDimensionOf0(xs) != sz00=> (? [W0] :( aVector0(W0)& W0 = sziznziztdt0(xs)& (? [W1] :( aVector0(W1)& 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.13/5.50 inference(negated_conjecture,[status(cth)],[f41])).
% 0.13/5.50 fof(f63,plain,(
% 0.13/5.50 aScalar0(sz0z00)),
% 0.13/5.50 inference(cnf_transformation,[status(thm)],[f9])).
% 0.13/5.50 fof(f70,plain,(
% 0.13/5.50 ![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.13/5.50 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.13/5.50 fof(f73,plain,(
% 0.13/5.50 ![X0]: (~aScalar0(X0)|sdtasdt0(X0,sz0z00)=sz0z00)),
% 0.13/5.50 inference(cnf_transformation,[status(thm)],[f70])).
% 0.13/5.50 fof(f96,plain,(
% 0.13/5.50 ![W0]: (~aScalar0(W0)|sdtlseqdt0(W0,W0))),
% 0.13/5.50 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.13/5.50 fof(f97,plain,(
% 0.13/5.50 ![X0]: (~aScalar0(X0)|sdtlseqdt0(X0,X0))),
% 0.13/5.50 inference(cnf_transformation,[status(thm)],[f96])).
% 0.13/5.50 fof(f135,plain,(
% 0.13/5.50 ![W0,W1]: ((~aVector0(W0)|~aVector0(W1))|((~aDimensionOf0(W0)=aDimensionOf0(W1)|~aDimensionOf0(W1)=sz00)|sdtasasdt0(W0,W1)=sz0z00))),
% 0.13/5.50 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.13/5.50 fof(f136,plain,(
% 0.13/5.50 ![X0,X1]: (~aVector0(X0)|~aVector0(X1)|~aDimensionOf0(X0)=aDimensionOf0(X1)|~aDimensionOf0(X1)=sz00|sdtasasdt0(X0,X1)=sz0z00)),
% 0.13/5.50 inference(cnf_transformation,[status(thm)],[f135])).
% 0.13/5.50 fof(f141,plain,(
% 0.13/5.50 aVector0(xs)),
% 0.13/5.50 inference(cnf_transformation,[status(thm)],[f38])).
% 0.13/5.50 fof(f142,plain,(
% 0.13/5.50 aVector0(xt)),
% 0.13/5.50 inference(cnf_transformation,[status(thm)],[f38])).
% 0.13/5.50 fof(f145,plain,(
% 0.13/5.50 aDimensionOf0(xs)=aDimensionOf0(xt)),
% 0.13/5.50 inference(cnf_transformation,[status(thm)],[f40])).
% 0.13/5.50 fof(f146,plain,(
% 0.13/5.50 ((aDimensionOf0(xs)=sz00|(?[W0]: ((aVector0(W0)&W0=sziznziztdt0(xs))&(?[W1]: ((aVector0(W1)&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.13/5.50 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.13/5.50 fof(f147,plain,(
% 0.13/5.50 (aDimensionOf0(xs)=sz00|(?[W0]: ((aVector0(W0)&W0=sziznziztdt0(xs))&(?[W1]: ((aVector0(W1)&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.13/5.50 inference(miniscoping,[status(thm)],[f146])).
% 0.13/5.50 fof(f148,plain,(
% 0.13/5.50 (aDimensionOf0(xs)=sz00|((aVector0(sK2_skl)&sK2_skl=sziznziztdt0(xs))&((aVector0(sK3_skl)&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.13/5.50 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.13/5.50 fof(f180,plain,(
% 0.13/5.50 aDimensionOf0(xs)=sz00|sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))),
% 0.13/5.50 inference(cnf_transformation,[status(thm)],[f148])).
% 0.13/5.50 fof(f181,plain,(
% 0.13/5.50 ~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))),
% 0.13/5.50 inference(cnf_transformation,[status(thm)],[f148])).
% 0.13/5.50 fof(f197,definition,(
% 0.13/5.50 sQ4_spl <=> (aDimensionOf0(xs)=sz00)),
% 0.13/5.50 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/5.50 fof(f198,plain,(
% 0.13/5.50 aDimensionOf0(xs)=sz00|~sQ4_spl),
% 0.13/5.50 inference(component_clause,[status(thm)],[f197])).
% 0.13/5.50 fof(f324,definition,(
% 0.13/5.50 sQ36_spl <=> (sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt))))),
% 0.13/5.50 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.13/5.50 fof(f325,plain,(
% 0.13/5.50 sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sdtasasdt0(xs,xs),sdtasasdt0(xt,xt)))|~sQ36_spl),
% 0.13/5.50 inference(component_clause,[status(thm)],[f324])).
% 0.13/5.50 fof(f327,plain,(
% 0.13/5.50 sQ4_spl|sQ36_spl),
% 0.13/5.50 inference(split_clause,[status(thm)],[f180,f197,f324])).
% 0.13/5.50 fof(f340,plain,(
% 0.13/5.50 sz00=aDimensionOf0(xt)|~sQ4_spl),
% 0.13/5.50 inference(forward_demodulation,[status(thm)],[f198,f145])).
% 0.13/5.50 fof(f346,plain,(
% 0.13/5.50 sdtlseqdt0(sz0z00,sz0z00)),
% 0.13/5.50 inference(resolution,[status(thm)],[f63,f97])).
% 0.13/5.50 fof(f385,definition,(
% 0.13/5.50 sQ46_spl <=> (sz0z00=sdtasasdt0(xs,xs))),
% 0.13/5.50 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.13/5.50 fof(f386,plain,(
% 0.13/5.50 sz0z00=sdtasasdt0(xs,xs)|~sQ46_spl),
% 0.13/5.50 inference(component_clause,[status(thm)],[f385])).
% 0.13/5.50 fof(f395,definition,(
% 0.13/5.50 sQ49_spl <=> (sz0z00=sdtasasdt0(xt,xt))),
% 0.13/5.50 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.13/5.50 fof(f396,plain,(
% 0.13/5.50 sz0z00=sdtasasdt0(xt,xt)|~sQ49_spl),
% 0.13/5.50 inference(component_clause,[status(thm)],[f395])).
% 0.13/5.50 fof(f416,plain,(
% 0.13/5.50 sdtasdt0(sz0z00,sz0z00)=sz0z00),
% 0.13/5.50 inference(resolution,[status(thm)],[f73,f63])).
% 0.13/5.50 fof(f461,plain,(
% 0.13/5.50 ~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sz0z00,sdtasasdt0(xt,xt)))|~sQ46_spl),
% 0.13/5.50 inference(forward_demodulation,[status(thm)],[f386,f181])).
% 0.13/5.50 fof(f467,definition,(
% 0.13/5.50 sQ57_spl <=> (aDimensionOf0(xt)=sz00)),
% 0.13/5.50 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.13/5.50 fof(f468,plain,(
% 0.13/5.50 aDimensionOf0(xt)=sz00|~sQ57_spl),
% 0.13/5.50 inference(component_clause,[status(thm)],[f467])).
% 0.13/5.50 fof(f574,plain,(
% 0.13/5.50 sQ57_spl|~sQ4_spl),
% 0.13/5.50 inference(split_clause,[status(thm)],[f340,f467,f197])).
% 0.13/5.50 fof(f607,plain,(
% 0.13/5.50 ![X0]: (~aVector0(X0)|~aDimensionOf0(xt)=aDimensionOf0(X0)|~aDimensionOf0(X0)=sz00|sdtasasdt0(xt,X0)=sz0z00)),
% 0.13/5.50 inference(resolution,[status(thm)],[f136,f142])).
% 0.13/5.50 fof(f608,plain,(
% 0.13/5.50 ![X0]: (~aVector0(X0)|~aDimensionOf0(xs)=aDimensionOf0(X0)|~aDimensionOf0(X0)=sz00|sdtasasdt0(xs,X0)=sz0z00)),
% 0.13/5.50 inference(resolution,[status(thm)],[f136,f141])).
% 0.13/5.50 fof(f625,plain,(
% 0.13/5.50 $false|~sQ36_spl),
% 0.13/5.50 inference(forward_subsumption_resolution,[status(thm)],[f325,f181])).
% 0.13/5.50 fof(f626,plain,(
% 0.13/5.50 ~sQ36_spl),
% 0.13/5.50 inference(contradiction_clause,[status(thm)],[f625])).
% 0.13/5.50 fof(f979,plain,(
% 0.13/5.50 aDimensionOf0(xs)=sz00|~sQ57_spl),
% 0.13/5.50 inference(forward_demodulation,[status(thm)],[f468,f145])).
% 0.13/5.50 fof(f1744,plain,(
% 0.13/5.50 ![X0]: (~aVector0(X0)|~sz00=aDimensionOf0(X0)|~aDimensionOf0(X0)=sz00|sdtasasdt0(xt,X0)=sz0z00|~sQ57_spl)),
% 0.13/5.50 inference(forward_demodulation,[status(thm)],[f468,f607])).
% 0.13/5.50 fof(f1745,plain,(
% 0.13/5.50 ![X0]: (~aVector0(X0)|~sz00=aDimensionOf0(X0)|sdtasasdt0(xt,X0)=sz0z00|~sQ57_spl)),
% 0.13/5.50 inference(duplicate_literals_removal,[status(thm)],[f1744])).
% 0.13/5.50 fof(f1746,plain,(
% 0.13/5.50 ~sz00=aDimensionOf0(xt)|sdtasasdt0(xt,xt)=sz0z00|~sQ57_spl),
% 0.13/5.50 inference(resolution,[status(thm)],[f1745,f142])).
% 0.13/5.50 fof(f1748,plain,(
% 0.13/5.50 ~sQ57_spl|sQ49_spl),
% 0.13/5.50 inference(split_clause,[status(thm)],[f1746,f467,f395])).
% 0.13/5.50 fof(f1759,plain,(
% 0.13/5.50 ![X0]: (~aVector0(X0)|~sz00=aDimensionOf0(X0)|~aDimensionOf0(X0)=sz00|sdtasasdt0(xs,X0)=sz0z00|~sQ57_spl)),
% 0.13/5.50 inference(forward_demodulation,[status(thm)],[f979,f608])).
% 0.13/5.50 fof(f1760,plain,(
% 0.13/5.50 ![X0]: (~aVector0(X0)|~sz00=aDimensionOf0(X0)|sdtasasdt0(xs,X0)=sz0z00|~sQ57_spl)),
% 0.13/5.50 inference(duplicate_literals_removal,[status(thm)],[f1759])).
% 0.13/5.50 fof(f1761,plain,(
% 0.13/5.50 ~sz00=aDimensionOf0(xt)|sdtasasdt0(xs,xt)=sz0z00|~sQ57_spl),
% 0.13/5.50 inference(resolution,[status(thm)],[f1760,f142])).
% 0.13/5.50 fof(f1762,plain,(
% 0.13/5.50 ~sz00=aDimensionOf0(xs)|sdtasasdt0(xs,xs)=sz0z00|~sQ57_spl),
% 0.13/5.50 inference(resolution,[status(thm)],[f1760,f141])).
% 0.13/5.50 fof(f1763,definition,(
% 0.13/5.50 sQ167_spl <=> (sdtasasdt0(xs,xt)=sz0z00)),
% 0.13/5.50 introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition])).
% 0.13/5.50 fof(f1764,plain,(
% 0.13/5.50 sdtasasdt0(xs,xt)=sz0z00|~sQ167_spl),
% 0.13/5.50 inference(component_clause,[status(thm)],[f1763])).
% 0.13/5.50 fof(f1766,plain,(
% 0.13/5.50 ~sQ57_spl|sQ167_spl),
% 0.13/5.50 inference(split_clause,[status(thm)],[f1761,f467,f1763])).
% 0.13/5.50 fof(f1767,plain,(
% 0.13/5.50 ~sQ4_spl|sQ46_spl|~sQ57_spl),
% 0.13/5.50 inference(split_clause,[status(thm)],[f1762,f197,f385,f467])).
% 0.13/5.50 fof(f1768,plain,(
% 0.13/5.50 ~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sdtasdt0(sz0z00,sz0z00))|~sQ49_spl|~sQ46_spl),
% 0.13/5.50 inference(forward_demodulation,[status(thm)],[f396,f461])).
% 0.13/5.50 fof(f1769,plain,(
% 0.13/5.50 ~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sdtasasdt0(xs,xt)),sz0z00)|~sQ49_spl|~sQ46_spl),
% 0.13/5.50 inference(forward_demodulation,[status(thm)],[f416,f1768])).
% 0.13/5.50 fof(f1771,plain,(
% 0.13/5.50 ~sdtlseqdt0(sdtasdt0(sdtasasdt0(xs,xt),sz0z00),sz0z00)|~sQ167_spl|~sQ49_spl|~sQ46_spl),
% 0.13/5.50 inference(backward_demodulation,[status(thm)],[f1764,f1769])).
% 0.13/5.50 fof(f1774,plain,(
% 0.13/5.50 ~sdtlseqdt0(sdtasdt0(sz0z00,sz0z00),sz0z00)|~sQ167_spl|~sQ49_spl|~sQ46_spl),
% 0.13/5.50 inference(forward_demodulation,[status(thm)],[f1764,f1771])).
% 0.13/5.50 fof(f1775,plain,(
% 0.13/5.50 ~sdtlseqdt0(sz0z00,sz0z00)|~sQ167_spl|~sQ49_spl|~sQ46_spl),
% 0.13/5.50 inference(forward_demodulation,[status(thm)],[f416,f1774])).
% 0.13/5.50 fof(f1776,plain,(
% 0.13/5.50 $false|~sQ167_spl|~sQ49_spl|~sQ46_spl),
% 0.13/5.50 inference(forward_subsumption_resolution,[status(thm)],[f1775,f346])).
% 0.13/5.50 fof(f1777,plain,(
% 0.13/5.50 ~sQ167_spl|~sQ49_spl|~sQ46_spl),
% 0.13/5.50 inference(contradiction_clause,[status(thm)],[f1776])).
% 0.13/5.50 fof(f1778,plain,(
% 0.13/5.50 $false),
% 0.13/5.50 inference(sat_refutation,[status(thm)],[f327,f574,f626,f1748,f1766,f1767,f1777])).
% 0.13/5.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/5.52 % Elapsed time: 0.150312 seconds
% 0.13/5.52 % CPU time: 0.955583 seconds
% 0.13/5.52 % Total memory used: 122.358 MB
% 0.13/5.52 % Net memory used: 120.947 MB
%------------------------------------------------------------------------------