%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP683+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 : n008.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 12:37:10 PM UTC 2026
% Result : Theorem 0.13s 0.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP683+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n008.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 20:33:54 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 0.13/0.79 % Refutation found
% 0.13/0.79 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.79 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.79 fof(f1,axiom,(
% 0.13/0.79 (! [A] : ld(A,mult(A,A)) = A )),
% 0.13/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.79 fof(f2,axiom,(
% 0.13/0.79 (! [A] : rd(mult(A,A),A) = A )),
% 0.13/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.79 fof(f3,axiom,(
% 0.13/0.79 (! [B,A] : mult(A,ld(A,B)) = ld(A,mult(A,B)) )),
% 0.13/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.79 fof(f4,axiom,(
% 0.13/0.79 (! [B,A] : mult(rd(A,B),B) = rd(mult(A,B),B) )),
% 0.13/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.79 fof(f5,axiom,(
% 0.13/0.79 (! [D,C,B,A] : ld(ld(A,B),mult(ld(A,B),mult(C,D))) = mult(ld(A,mult(A,C)),D) )),
% 0.13/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.79 fof(f6,axiom,(
% 0.13/0.79 (! [D,C,B,A] : rd(mult(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,rd(mult(B,D),D)) )),
% 0.13/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.79 fof(f7,axiom,(
% 0.13/0.79 (! [B,A] : ld(A,mult(A,ld(B,B))) = rd(mult(rd(A,A),B),B) )),
% 0.13/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.79 fof(f8,conjecture,(
% 0.13/0.79 (! [X3,X4,X5] :( mult(X3,ld(X4,mult(X4,X5))) = mult(X3,X5)& mult(rd(mult(X3,X4),X4),X5) = mult(X3,X5) ) )),
% 0.13/0.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.79 fof(f9,negated_conjecture,(
% 0.13/0.79 ~((! [X3,X4,X5] :( mult(X3,ld(X4,mult(X4,X5))) = mult(X3,X5)& mult(rd(mult(X3,X4),X4),X5) = mult(X3,X5) ) ))),
% 0.13/0.79 inference(negated_conjecture,[status(cth)],[f8])).
% 0.13/0.79 fof(f10,plain,(
% 0.13/0.79 ![X0]: (ld(X0,mult(X0,X0))=X0)),
% 0.13/0.79 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.79 fof(f11,plain,(
% 0.13/0.79 ![X0]: (rd(mult(X0,X0),X0)=X0)),
% 0.13/0.79 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.79 fof(f12,plain,(
% 0.13/0.79 ![X0,X1]: (mult(X0,ld(X0,X1))=ld(X0,mult(X0,X1)))),
% 0.13/0.79 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.79 fof(f13,plain,(
% 0.13/0.79 ![X0,X1]: (mult(rd(X0,X1),X1)=rd(mult(X0,X1),X1))),
% 0.13/0.79 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.79 fof(f14,plain,(
% 0.13/0.79 ![X0,X1,X2,X3]: (ld(ld(X0,X1),mult(ld(X0,X1),mult(X2,X3)))=mult(ld(X0,mult(X0,X2)),X3))),
% 0.13/0.79 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.79 fof(f15,plain,(
% 0.13/0.79 ![X0,X1,X2,X3]: (rd(mult(mult(X0,X1),rd(X2,X3)),rd(X2,X3))=mult(X0,rd(mult(X1,X3),X3)))),
% 0.13/0.79 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.79 fof(f16,plain,(
% 0.13/0.79 ![X0,X1]: (ld(X0,mult(X0,ld(X1,X1)))=rd(mult(rd(X0,X0),X1),X1))),
% 0.13/0.79 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.79 fof(f17,plain,(
% 0.13/0.79 (?[X3,X4,X5]: (~mult(X3,ld(X4,mult(X4,X5)))=mult(X3,X5)|~mult(rd(mult(X3,X4),X4),X5)=mult(X3,X5)))),
% 0.13/0.79 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.13/0.79 fof(f18,plain,(
% 0.13/0.79 (?[X3,X4,X5]: ~mult(X3,ld(X4,mult(X4,X5)))=mult(X3,X5))|(?[X3,X4,X5]: ~mult(rd(mult(X3,X4),X4),X5)=mult(X3,X5))),
% 0.13/0.79 inference(miniscoping,[status(thm)],[f17])).
% 0.13/0.79 fof(f19,plain,(
% 0.13/0.79 ~mult(sK0_skl,ld(sK1_skl,mult(sK1_skl,sK2_skl)))=mult(sK0_skl,sK2_skl)|~mult(rd(mult(sK3_skl,sK4_skl),sK4_skl),sK5_skl)=mult(sK3_skl,sK5_skl)),
% 0.13/0.79 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(X3,sK0_skl),skolemize(X4,sK1_skl),skolemize(X5,sK2_skl),skolemize(X3,sK3_skl),skolemize(X4,sK4_skl),skolemize(X5,sK5_skl)],[f18])).
% 0.13/0.79 fof(f20,plain,(
% 0.13/0.79 ~mult(sK0_skl,ld(sK1_skl,mult(sK1_skl,sK2_skl)))=mult(sK0_skl,sK2_skl)|~mult(rd(mult(sK3_skl,sK4_skl),sK4_skl),sK5_skl)=mult(sK3_skl,sK5_skl)),
% 0.13/0.79 inference(cnf_transformation,[status(thm)],[f19])).
% 0.13/0.79 fof(f21,plain,(
% 0.13/0.79 ![X0]: (mult(X0,ld(X0,X0))=X0)),
% 0.13/0.79 inference(backward_demodulation,[status(thm)],[f12,f10])).
% 0.13/0.79 fof(f22,plain,(
% 0.13/0.79 ![X0]: (mult(rd(X0,X0),X0)=X0)),
% 0.13/0.79 inference(backward_demodulation,[status(thm)],[f13,f11])).
% 0.13/0.79 fof(f23,plain,(
% 0.13/0.79 ![X0,X1,X2,X3]: (mult(ld(X0,X1),ld(ld(X0,X1),mult(X2,X3)))=mult(ld(X0,mult(X0,X2)),X3))),
% 0.13/0.79 inference(forward_demodulation,[status(thm)],[f12,f14])).
% 0.13/0.79 fof(f24,plain,(
% 0.13/0.79 ![X0,X1,X2,X3]: (mult(ld(X0,X1),ld(ld(X0,X1),mult(X2,X3)))=mult(mult(X0,ld(X0,X2)),X3))),
% 0.13/0.79 inference(forward_demodulation,[status(thm)],[f12,f23])).
% 0.13/0.79 fof(f25,plain,(
% 0.13/0.79 ![X0,X1,X2,X3]: (mult(rd(mult(X0,X1),rd(X2,X3)),rd(X2,X3))=mult(X0,rd(mult(X1,X3),X3)))),
% 0.13/0.79 inference(forward_demodulation,[status(thm)],[f13,f15])).
% 0.13/0.79 fof(f26,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(rd(mult(X0,X1),rd(X2,X3)),rd(X2,X3))=mult(X0,mult(rd(X1,X3),X3)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f13,f25])).
% 0.13/0.80 fof(f27,plain,(
% 0.13/0.80 ![X0,X1]: (mult(X0,ld(X0,ld(X1,X1)))=rd(mult(rd(X0,X0),X1),X1))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f12,f16])).
% 0.13/0.80 fof(f28,plain,(
% 0.13/0.80 ![X0,X1]: (mult(X0,ld(X0,ld(X1,X1)))=mult(rd(rd(X0,X0),X1),X1))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f13,f27])).
% 0.13/0.80 fof(f29,plain,(
% 0.13/0.80 ~mult(sK0_skl,mult(sK1_skl,ld(sK1_skl,sK2_skl)))=mult(sK0_skl,sK2_skl)|~mult(rd(mult(sK3_skl,sK4_skl),sK4_skl),sK5_skl)=mult(sK3_skl,sK5_skl)),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f12,f20])).
% 0.13/0.80 fof(f30,plain,(
% 0.13/0.80 ~mult(sK0_skl,mult(sK1_skl,ld(sK1_skl,sK2_skl)))=mult(sK0_skl,sK2_skl)|~mult(mult(rd(sK3_skl,sK4_skl),sK4_skl),sK5_skl)=mult(sK3_skl,sK5_skl)),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f13,f29])).
% 0.13/0.80 fof(f32,plain,(
% 0.13/0.80 ![X0]: (mult(X0,ld(X0,ld(X0,X0)))=ld(X0,X0))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f21,f12])).
% 0.13/0.80 fof(f33,plain,(
% 0.13/0.80 ![X0]: (mult(rd(rd(X0,X0),X0),X0)=rd(X0,X0))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f22,f13])).
% 0.13/0.80 fof(f34,plain,(
% 0.13/0.80 ![X0]: (mult(rd(X0,ld(X0,X0)),ld(X0,X0))=rd(X0,ld(X0,X0)))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f21,f13])).
% 0.13/0.80 fof(f35,plain,(
% 0.13/0.80 ![X0]: (mult(X0,ld(X0,ld(X0,X0)))=rd(X0,X0))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f28,f33])).
% 0.13/0.80 fof(f36,plain,(
% 0.13/0.80 ![X0]: (mult(ld(X0,X0),X0)=X0)),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f39,f22])).
% 0.13/0.80 fof(f38,plain,(
% 0.13/0.80 ![X0,X1]: (mult(X0,ld(X0,ld(X1,X1)))=mult(rd(ld(X0,X0),X1),X1))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f39,f28])).
% 0.13/0.80 fof(f39,plain,(
% 0.13/0.80 ![X0]: (ld(X0,X0)=rd(X0,X0))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f32,f35])).
% 0.13/0.80 fof(f42,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(mult(X0,ld(X0,X1)),ld(ld(X0,mult(X0,X1)),mult(X2,X3)))=mult(mult(X0,ld(X0,X2)),X3))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f12,f24])).
% 0.13/0.80 fof(f49,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),mult(X2,X3)))=mult(mult(X0,ld(X0,X2)),X3))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f12,f42])).
% 0.13/0.80 fof(f52,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(ld(X0,X1),ld(ld(X0,X1),X2))=mult(mult(X0,ld(X0,ld(X2,X2))),X2))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f36,f24])).
% 0.13/0.80 fof(f71,plain,(
% 0.13/0.80 ![X0]: (mult(X0,ld(X0,ld(ld(X0,X0),ld(X0,X0))))=mult(ld(ld(X0,X0),ld(X0,X0)),ld(X0,X0)))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f39,f38])).
% 0.13/0.80 fof(f74,plain,(
% 0.13/0.80 ![X0,X1]: (mult(rd(rd(ld(X0,X0),X1),X1),X1)=rd(mult(X0,ld(X0,ld(X1,X1))),X1))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f38,f13])).
% 0.13/0.80 fof(f76,plain,(
% 0.13/0.80 ![X0]: (mult(X0,ld(X0,ld(ld(X0,X0),ld(X0,X0))))=ld(X0,X0))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f36,f71])).
% 0.13/0.80 fof(f94,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(rd(X0,rd(X1,X2)),rd(X1,X2))=mult(X0,mult(rd(ld(X0,X0),X2),X2)))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f21,f26])).
% 0.13/0.80 fof(f108,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(rd(X0,rd(X1,X2)),rd(X1,X2))=mult(X0,mult(X0,ld(X0,ld(X2,X2)))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f38,f94])).
% 0.13/0.80 fof(f121,plain,(
% 0.13/0.80 ![X0,X1]: (mult(ld(X0,X1),ld(ld(X0,X1),ld(X0,X0)))=mult(ld(X0,X0),ld(X0,X0)))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f76,f52])).
% 0.13/0.80 fof(f123,plain,(
% 0.13/0.80 ![X0,X1]: (mult(ld(ld(X0,X0),X1),ld(ld(ld(X0,X0),X1),X0))=mult(ld(X0,X0),X0))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f21,f52])).
% 0.13/0.80 fof(f128,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(ld(X0,X1),ld(ld(X0,X1),ld(ld(X0,X1),X2)))=ld(ld(X0,X1),mult(mult(X0,ld(X0,ld(X2,X2))),X2)))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f52,f12])).
% 0.13/0.80 fof(f131,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(rd(mult(X0,ld(X0,ld(X1,X1))),X1),X1)=rd(mult(ld(X0,X2),ld(ld(X0,X2),X1)),X1))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f52,f13])).
% 0.13/0.80 fof(f137,plain,(
% 0.13/0.80 ![X0,X1]: (mult(ld(ld(X0,X0),X1),ld(ld(ld(X0,X0),X1),X0))=X0)),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f36,f123])).
% 0.13/0.80 fof(f142,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(mult(rd(rd(ld(X0,X0),X1),X1),X1),X1)=rd(mult(ld(X0,X2),ld(ld(X0,X2),X1)),X1))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f74,f131])).
% 0.13/0.80 fof(f228,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(X0,ld(mult(X0,ld(X0,X0)),mult(X1,X2)))=mult(mult(X0,ld(X0,X1)),X2))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f21,f49])).
% 0.13/0.80 fof(f243,plain,(
% 0.13/0.80 ![X0,X1,X2,X3,X4]: (mult(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),mult(ld(X2,X3),ld(ld(X2,X3),X4))))=mult(mult(X0,ld(X0,mult(X2,ld(X2,ld(X4,X4))))),X4))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f52,f49])).
% 0.13/0.80 fof(f248,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),X2))=mult(mult(X0,ld(X0,ld(ld(X2,X2),X3))),ld(ld(ld(X2,X2),X3),X2)))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f137,f49])).
% 0.13/0.80 fof(f261,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),mult(X2,X3))))=ld(mult(X0,ld(X0,X1)),mult(mult(X0,ld(X0,X2)),X3)))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f49,f12])).
% 0.13/0.80 fof(f273,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(ld(X0,X1),ld(ld(X0,X1),X2))=mult(X0,ld(X0,mult(ld(X2,X2),X2))))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f303,f52])).
% 0.13/0.80 fof(f291,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(ld(X0,X1),ld(ld(X0,X1),ld(ld(X0,X1),X2)))=ld(ld(X0,X1),mult(X0,ld(X0,mult(ld(X2,X2),X2)))))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f303,f128])).
% 0.13/0.80 fof(f303,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(X0,ld(X0,mult(X1,X2)))=mult(mult(X0,ld(X0,X1)),X2))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f21,f228])).
% 0.13/0.80 fof(f358,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(mult(X0,ld(X0,ld(X1,X2))),ld(ld(X1,X2),X3))=mult(mult(X0,ld(X0,mult(X1,ld(X1,ld(X3,X3))))),X3))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f49,f243])).
% 0.13/0.80 fof(f359,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(ld(X1,X2),ld(ld(X1,X2),X3))))=mult(mult(X0,ld(X0,mult(X1,ld(X1,ld(X3,X3))))),X3))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f303,f358])).
% 0.13/0.80 fof(f360,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(ld(X1,X2),ld(ld(X1,X2),X3))))=mult(X0,ld(X0,mult(mult(X1,ld(X1,ld(X3,X3))),X3))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f303,f359])).
% 0.13/0.80 fof(f361,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(ld(X1,X2),ld(ld(X1,X2),X3))))=mult(X0,ld(X0,mult(X1,ld(X1,mult(ld(X3,X3),X3))))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f303,f360])).
% 0.13/0.80 fof(f362,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(ld(X1,X2),ld(ld(X1,X2),X3))))=mult(X0,ld(X0,mult(X1,ld(X1,X3)))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f36,f361])).
% 0.13/0.80 fof(f377,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),X2))))=mult(mult(X0,ld(X0,ld(ld(X2,X2),X3))),ld(ld(ld(X2,X2),X3),X2)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f303,f248])).
% 0.13/0.80 fof(f378,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),X2))))=mult(X0,ld(X0,mult(ld(ld(X2,X2),X3),ld(ld(ld(X2,X2),X3),X2)))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f303,f377])).
% 0.13/0.80 fof(f379,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),X2))))=mult(X0,ld(X0,mult(ld(X2,X2),ld(ld(X2,X2),X2)))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f362,f378])).
% 0.13/0.80 fof(f380,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),X2))))=mult(X0,ld(X0,mult(X2,ld(X2,X2)))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f362,f379])).
% 0.13/0.80 fof(f383,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),X2))))=mult(X0,ld(X0,X2)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f21,f380])).
% 0.13/0.80 fof(f424,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),mult(X2,X3))))))=ld(mult(X0,ld(X0,X1)),mult(mult(X0,ld(X0,X2)),X3)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f303,f261])).
% 0.13/0.80 fof(f425,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(X0,ld(X0,ld(mult(X0,ld(X0,X1)),mult(X2,X3))))=ld(mult(X0,ld(X0,X1)),mult(mult(X0,ld(X0,X2)),X3)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f383,f424])).
% 0.13/0.80 fof(f426,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(X0,ld(X0,ld(mult(X0,ld(X0,X1)),mult(X2,X3))))=ld(mult(X0,ld(X0,X1)),mult(X0,ld(X0,mult(X2,X3)))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f303,f425])).
% 0.13/0.80 fof(f438,plain,(
% 0.13/0.80 ![X0]: (mult(X0,ld(X0,ld(X0,X0)))=mult(ld(X0,X0),ld(X0,X0)))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f443,f121])).
% 0.13/0.80 fof(f441,plain,(
% 0.13/0.80 ![X0,X1]: (mult(mult(rd(rd(ld(X0,X0),X1),X1),X1),X1)=rd(mult(X0,ld(X0,X1)),X1))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f443,f142])).
% 0.13/0.80 fof(f443,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(ld(X0,X1),ld(ld(X0,X1),X2))=mult(X0,ld(X0,X2)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f36,f273])).
% 0.13/0.80 fof(f473,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(X0,ld(X0,ld(ld(X0,X1),X2)))=ld(ld(X0,X1),mult(X0,ld(X0,mult(ld(X2,X2),X2)))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f443,f291])).
% 0.13/0.80 fof(f474,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(X0,ld(X0,ld(ld(X0,X1),X2)))=ld(ld(X0,X1),mult(X0,ld(X0,X2))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f36,f473])).
% 0.13/0.80 fof(f490,plain,(
% 0.13/0.80 ![X0]: (ld(X0,X0)=mult(ld(X0,X0),ld(X0,X0)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f32,f438])).
% 0.13/0.80 fof(f507,plain,(
% 0.13/0.80 ![X0]: (mult(rd(ld(X0,X0),ld(X0,X0)),ld(X0,X0))=rd(ld(X0,X0),ld(X0,X0)))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f490,f13])).
% 0.13/0.80 fof(f512,plain,(
% 0.13/0.80 ![X0]: (mult(X0,ld(X0,ld(ld(X0,X0),ld(X0,X0))))=rd(ld(X0,X0),ld(X0,X0)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f38,f507])).
% 0.13/0.80 fof(f513,plain,(
% 0.13/0.80 ![X0]: (ld(X0,X0)=rd(ld(X0,X0),ld(X0,X0)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f76,f512])).
% 0.13/0.80 fof(f522,plain,(
% 0.13/0.80 ![X0]: (ld(X0,X0)=ld(ld(X0,X0),ld(X0,X0)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f39,f513])).
% 0.13/0.80 fof(f575,plain,(
% 0.13/0.80 ![X0,X1]: (mult(X0,ld(X0,mult(X0,X1)))=mult(X0,X1))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f21,f303])).
% 0.13/0.80 fof(f585,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),X2))=ld(mult(X0,ld(X0,X1)),mult(X0,ld(X0,mult(X1,X2)))))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f303,f12])).
% 0.13/0.80 fof(f595,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(rd(X0,rd(X1,X2)),rd(X1,X2))=mult(X0,ld(X2,X2)))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f598,f108])).
% 0.13/0.80 fof(f598,plain,(
% 0.13/0.80 ![X0,X1]: (mult(X0,mult(X0,ld(X0,X1)))=mult(X0,X1))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f12,f575])).
% 0.13/0.80 fof(f616,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),X2))))=ld(mult(X0,ld(X0,X1)),mult(X0,ld(X0,mult(X1,X2)))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f303,f585])).
% 0.13/0.80 fof(f617,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(X0,ld(X0,X1))=ld(mult(X0,ld(X0,X2)),mult(X0,ld(X0,mult(X2,X1)))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f383,f616])).
% 0.13/0.80 fof(f618,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(X0,ld(X0,X1))=mult(X0,ld(X0,ld(mult(X0,ld(X0,X2)),mult(X2,X1)))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f426,f617])).
% 0.13/0.80 fof(f620,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(mult(X0,X1),ld(X2,X2))=mult(X0,mult(rd(X1,X2),X2)))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f595,f26])).
% 0.13/0.80 fof(f661,plain,(
% 0.13/0.80 ![X0,X1]: (ld(X0,X1)=mult(X0,ld(X0,ld(X0,X1))))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f21,f443])).
% 0.13/0.80 fof(f674,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(ld(X0,X1),mult(X0,ld(X0,X2)))=mult(ld(X0,X1),X2))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f443,f598])).
% 0.13/0.80 fof(f697,plain,(
% 0.13/0.80 ![X0,X1,X2]: (ld(mult(X0,ld(X0,X1)),X2)=mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),X2))))))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f303,f661])).
% 0.13/0.80 fof(f698,plain,(
% 0.13/0.80 ![X0,X1,X2]: (ld(ld(X0,X1),X2)=mult(X0,ld(X0,ld(ld(X0,X1),X2))))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f443,f661])).
% 0.13/0.80 fof(f711,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(X0,ld(X0,X1))=ld(mult(X0,ld(X0,X2)),mult(X2,X1)))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f713,f618])).
% 0.13/0.80 fof(f713,plain,(
% 0.13/0.80 ![X0,X1,X2]: (ld(mult(X0,ld(X0,X1)),X2)=mult(X0,ld(X0,ld(mult(X0,ld(X0,X1)),X2))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f383,f697])).
% 0.13/0.80 fof(f717,plain,(
% 0.13/0.80 ![X0,X1,X2]: (ld(ld(X0,X1),X2)=ld(ld(X0,X1),mult(X0,ld(X0,X2))))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f698,f474])).
% 0.13/0.80 fof(f807,plain,(
% 0.13/0.80 ![X0,X1]: (mult(ld(rd(X0,X1),rd(X0,X1)),rd(X0,X1))=mult(rd(X0,X1),ld(X1,X1)))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f39,f595])).
% 0.13/0.80 fof(f810,plain,(
% 0.13/0.80 ![X0,X1]: (mult(rd(X0,ld(X1,X1)),rd(X1,X1))=mult(X0,ld(X1,X1)))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f39,f595])).
% 0.13/0.80 fof(f823,plain,(
% 0.13/0.80 ![X0,X1]: (rd(X0,X1)=mult(rd(X0,X1),ld(X1,X1)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f36,f807])).
% 0.13/0.80 fof(f828,plain,(
% 0.13/0.80 ![X0]: (mult(X0,ld(X0,X0))=rd(X0,ld(X0,X0)))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f832,f34])).
% 0.13/0.80 fof(f832,plain,(
% 0.13/0.80 ![X0,X1]: (mult(rd(X0,ld(X1,X1)),ld(X1,X1))=mult(X0,ld(X1,X1)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f39,f810])).
% 0.13/0.80 fof(f841,plain,(
% 0.13/0.80 ![X0]: (X0=rd(X0,ld(X0,X0)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f21,f828])).
% 0.13/0.80 fof(f853,plain,(
% 0.13/0.80 ![X0,X1]: (mult(rd(X0,rd(X1,ld(X1,X1))),X1)=mult(X0,ld(ld(X1,X1),ld(X1,X1))))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f841,f595])).
% 0.13/0.80 fof(f860,plain,(
% 0.13/0.80 ![X0,X1]: (mult(rd(X0,X1),X1)=mult(X0,ld(ld(X1,X1),ld(X1,X1))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f841,f853])).
% 0.13/0.80 fof(f863,plain,(
% 0.13/0.80 ![X0,X1]: (mult(X0,ld(X0,ld(X1,X1)))=mult(ld(X0,X0),ld(X1,X1)))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f891,f38])).
% 0.13/0.80 fof(f864,plain,(
% 0.13/0.80 ~mult(sK0_skl,mult(sK1_skl,ld(sK1_skl,sK2_skl)))=mult(sK0_skl,sK2_skl)|~mult(mult(sK3_skl,ld(sK4_skl,sK4_skl)),sK5_skl)=mult(sK3_skl,sK5_skl)),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f891,f30])).
% 0.13/0.80 fof(f865,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(X0,ld(rd(X1,X2),rd(X1,X2)))=mult(X0,ld(X2,X2)))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f891,f595])).
% 0.13/0.80 fof(f866,plain,(
% 0.13/0.80 ![X0,X1]: (mult(X0,ld(X1,X1))=rd(mult(X0,X1),X1))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f891,f13])).
% 0.13/0.80 fof(f873,plain,(
% 0.13/0.80 ![X0,X1]: (mult(mult(rd(ld(X0,X0),X1),ld(X1,X1)),X1)=rd(mult(X0,ld(X0,X1)),X1))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f891,f441])).
% 0.13/0.80 fof(f890,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(mult(X0,X1),ld(X2,X2))=mult(X0,mult(X1,ld(X2,X2))))),
% 0.13/0.80 inference(backward_demodulation,[status(thm)],[f891,f620])).
% 0.13/0.80 fof(f891,plain,(
% 0.13/0.80 ![X0,X1]: (mult(rd(X0,X1),X1)=mult(X0,ld(X1,X1)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f522,f860])).
% 0.13/0.80 fof(f909,plain,(
% 0.13/0.80 ![X0,X1]: (mult(rd(ld(X0,X0),X1),X1)=rd(mult(X0,ld(X0,X1)),X1))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f823,f873])).
% 0.13/0.80 fof(f911,plain,(
% 0.13/0.80 ![X0,X1]: (mult(X0,ld(X0,ld(X1,X1)))=rd(mult(X0,ld(X0,X1)),X1))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f38,f909])).
% 0.13/0.80 fof(f955,plain,(
% 0.13/0.80 ![X0,X1]: (mult(mult(X0,ld(X1,X1)),X1)=mult(mult(X0,X1),ld(X1,X1)))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f866,f891])).
% 0.13/0.80 fof(f967,plain,(
% 0.13/0.80 ![X0,X1]: (mult(mult(X0,ld(X1,X1)),X1)=mult(X0,mult(X1,ld(X1,X1))))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f890,f955])).
% 0.13/0.80 fof(f968,plain,(
% 0.13/0.80 ![X0,X1]: (mult(mult(X0,ld(X1,X1)),X1)=mult(X0,X1))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f21,f967])).
% 0.13/0.80 fof(f1134,plain,(
% 0.13/0.80 ![X0,X1]: (mult(mult(X0,ld(X0,ld(X1,X1))),X1)=mult(ld(X0,X0),X1))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f863,f968])).
% 0.13/0.80 fof(f1154,plain,(
% 0.13/0.80 ![X0,X1]: (mult(X0,ld(X0,mult(ld(X1,X1),X1)))=mult(ld(X0,X0),X1))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f303,f1134])).
% 0.13/0.80 fof(f1159,plain,(
% 0.13/0.80 ![X0,X1]: (mult(X0,ld(X0,X1))=mult(ld(X0,X0),X1))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f36,f1154])).
% 0.13/0.80 fof(f1206,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(mult(X0,mult(X1,ld(X2,X2))),X2)=mult(mult(X0,X1),X2))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f890,f968])).
% 0.13/0.80 fof(f1264,plain,(
% 0.13/0.80 ![X0,X1]: (mult(X0,ld(X0,ld(ld(X0,X0),X1)))=mult(X0,ld(X0,X1)))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f443,f1159])).
% 0.13/0.80 fof(f1292,plain,(
% 0.13/0.80 ![X0,X1]: (ld(ld(X0,X0),X1)=mult(X0,ld(X0,X1)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f698,f1264])).
% 0.13/0.80 fof(f1505,plain,(
% 0.13/0.80 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(X1,ld(X1,X2))))=ld(mult(X0,ld(X0,ld(X1,X3))),mult(ld(X1,X3),X2)))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f674,f711])).
% 0.13/0.80 fof(f1513,plain,(
% 0.13/0.80 ![X0,X1]: (mult(X0,ld(X0,ld(X1,X1)))=ld(mult(X0,ld(X0,X1)),X1))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f21,f711])).
% 0.13/0.80 fof(f1562,plain,(
% 0.13/0.80 ![X0,X1,X2]: (mult(X0,ld(X0,mult(X1,ld(X1,X2))))=mult(X0,ld(X0,X2)))),
% 0.13/0.80 inference(forward_demodulation,[status(thm)],[f711,f1505])).
% 0.13/0.80 fof(f1629,plain,(
% 0.13/0.80 ![X0,X1,X2]: (ld(ld(ld(X0,X0),X1),X2)=ld(mult(X0,ld(X0,X1)),mult(ld(X0,X0),ld(ld(X0,X0),X2))))),
% 0.13/0.80 inference(paramodulation,[status(thm)],[f1292,f717])).
% 0.13/0.80 fof(f1662,plain,(
% 0.13/0.80 ![X0,X1,X2]: (ld(mult(X0,ld(X0,X1)),X2)=ld(mult(X0,ld(X0,X1)),mult(ld(X0,X0),ld(ld(X0,X0),X2))))),
% 0.13/0.81 inference(forward_demodulation,[status(thm)],[f1292,f1629])).
% 0.13/0.81 fof(f1668,plain,(
% 0.13/0.81 ![X0,X1,X2]: (ld(mult(X0,ld(X0,X1)),X2)=ld(mult(X0,ld(X0,X1)),mult(X0,ld(X0,X2))))),
% 0.13/0.81 inference(forward_demodulation,[status(thm)],[f443,f1662])).
% 0.13/0.81 fof(f1982,plain,(
% 0.13/0.81 ![X0,X1,X2]: (mult(X0,ld(rd(mult(X1,ld(X1,X2)),X2),mult(X1,ld(X1,ld(X2,X2)))))=mult(X0,ld(X2,X2)))),
% 0.13/0.81 inference(paramodulation,[status(thm)],[f911,f865])).
% 0.13/0.81 fof(f2029,plain,(
% 0.13/0.81 ![X0,X1,X2]: (mult(X0,ld(mult(X1,ld(X1,ld(X2,X2))),mult(X1,ld(X1,ld(X2,X2)))))=mult(X0,ld(X2,X2)))),
% 0.13/0.81 inference(forward_demodulation,[status(thm)],[f911,f1982])).
% 0.13/0.81 fof(f2030,plain,(
% 0.13/0.81 ![X0,X1,X2]: (mult(X0,ld(mult(X1,ld(X1,ld(X2,X2))),ld(X2,X2)))=mult(X0,ld(X2,X2)))),
% 0.13/0.81 inference(forward_demodulation,[status(thm)],[f1668,f2029])).
% 0.13/0.81 fof(f2031,plain,(
% 0.13/0.81 ![X0,X1,X2]: (mult(X0,mult(X1,ld(X1,ld(ld(X2,X2),ld(X2,X2)))))=mult(X0,ld(X2,X2)))),
% 0.13/0.81 inference(forward_demodulation,[status(thm)],[f1513,f2030])).
% 0.13/0.81 fof(f2032,plain,(
% 0.13/0.81 ![X0,X1,X2]: (mult(X0,mult(X1,ld(X1,mult(X2,ld(X2,ld(X2,X2))))))=mult(X0,ld(X2,X2)))),
% 0.13/0.81 inference(forward_demodulation,[status(thm)],[f1292,f2031])).
% 0.13/0.81 fof(f2037,plain,(
% 0.13/0.81 ![X0,X1,X2]: (mult(X0,mult(X1,ld(X1,ld(X2,X2))))=mult(X0,ld(X2,X2)))),
% 0.13/0.81 inference(forward_demodulation,[status(thm)],[f1562,f2032])).
% 0.13/0.81 fof(f2376,plain,(
% 0.13/0.81 ![X0,X1,X2]: (mult(mult(X0,mult(X1,ld(X1,ld(X2,X2)))),X2)=mult(mult(X0,ld(X1,X1)),X2))),
% 0.13/0.81 inference(paramodulation,[status(thm)],[f1159,f1206])).
% 0.13/0.81 fof(f2424,plain,(
% 0.13/0.81 ![X0,X1,X2]: (mult(mult(X0,ld(X1,X1)),X1)=mult(mult(X0,ld(X2,X2)),X1))),
% 0.13/0.81 inference(forward_demodulation,[status(thm)],[f2037,f2376])).
% 0.13/0.81 fof(f2425,plain,(
% 0.13/0.81 ~mult(sK0_skl,mult(sK1_skl,ld(sK1_skl,sK2_skl)))=mult(sK0_skl,sK2_skl)|~mult(sK3_skl,sK5_skl)=mult(sK3_skl,sK5_skl)),
% 0.13/0.81 inference(backward_demodulation,[status(thm)],[f2435,f864])).
% 0.13/0.81 fof(f2435,plain,(
% 0.13/0.81 ![X0,X1,X2]: (mult(X0,X1)=mult(mult(X0,ld(X2,X2)),X1))),
% 0.13/0.81 inference(forward_demodulation,[status(thm)],[f968,f2424])).
% 0.13/0.81 fof(f2478,plain,(
% 0.13/0.81 ~mult(sK0_skl,mult(sK1_skl,ld(sK1_skl,sK2_skl)))=mult(sK0_skl,sK2_skl)),
% 0.13/0.81 inference(trivial_equality_resolution,[status(thm)],[f2425])).
% 0.13/0.81 fof(f3099,plain,(
% 0.13/0.81 ![X0,X1,X2]: (mult(X0,mult(X0,ld(X0,X1)))=mult(X0,mult(X2,ld(X2,X1))))),
% 0.13/0.81 inference(paramodulation,[status(thm)],[f1562,f598])).
% 0.13/0.81 fof(f3182,plain,(
% 0.13/0.81 ~mult(sK0_skl,sK2_skl)=mult(sK0_skl,sK2_skl)),
% 0.13/0.81 inference(backward_demodulation,[status(thm)],[f3192,f2478])).
% 0.13/0.81 fof(f3192,plain,(
% 0.13/0.81 ![X0,X1,X2]: (mult(X0,X1)=mult(X0,mult(X2,ld(X2,X1))))),
% 0.13/0.81 inference(forward_demodulation,[status(thm)],[f598,f3099])).
% 0.13/0.81 fof(f3236,plain,(
% 0.13/0.81 $false),
% 0.13/0.81 inference(trivial_equality_resolution,[status(thm)],[f3182])).
% 0.13/0.81 % SZS output end CNFRefutation for theBenchmark.p
% 1.24/0.83 % Elapsed time: 0.450417 seconds
% 1.24/0.83 % CPU time: 3.302621 seconds
% 1.24/0.83 % Total memory used: 103.608 MB
% 1.24/0.83 % Net memory used: 102.053 MB
%------------------------------------------------------------------------------