%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP660+3 : 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 : n014.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:06 PM UTC 2026
% Result : Theorem 27.73s 3.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP660+3 : 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.11/0.36 % Computer : n014.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 20 20:29:50 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 27.73/3.97 % Refutation found
% 27.73/3.97 % SZS status Theorem for theBenchmark: Theorem is valid
% 27.73/3.97 % SZS output start CNFRefutation for theBenchmark
% 27.73/3.97 fof(f1,axiom,(
% 27.73/3.97 (! [B,A] : mult(A,ld(A,B)) = B )),
% 27.73/3.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.73/3.97 fof(f2,axiom,(
% 27.73/3.97 (! [B,A] : ld(A,mult(A,B)) = B )),
% 27.73/3.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.73/3.97 fof(f3,axiom,(
% 27.73/3.97 (! [B,A] : mult(rd(A,B),B) = A )),
% 27.73/3.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.73/3.97 fof(f4,axiom,(
% 27.73/3.97 (! [B,A] : rd(mult(A,B),B) = A )),
% 27.73/3.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.73/3.97 fof(f5,axiom,(
% 27.73/3.97 (! [C,B,A] : mult(mult(mult(A,B),C),A) = mult(A,mult(B,mult(C,A))) )),
% 27.73/3.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.73/3.97 fof(f6,conjecture,(
% 27.73/3.97 (! [X0,X1] :( mult(X0,ld(X1,X1)) = X0& mult(ld(X1,X1),X0) = X0 ) )),
% 27.73/3.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.73/3.97 fof(f7,negated_conjecture,(
% 27.73/3.97 ~((! [X0,X1] :( mult(X0,ld(X1,X1)) = X0& mult(ld(X1,X1),X0) = X0 ) ))),
% 27.73/3.97 inference(negated_conjecture,[status(cth)],[f6])).
% 27.73/3.97 fof(f8,plain,(
% 27.73/3.97 ![X0,X1]: (mult(X0,ld(X0,X1))=X1)),
% 27.73/3.97 inference(cnf_transformation,[status(thm)],[f1])).
% 27.73/3.97 fof(f9,plain,(
% 27.73/3.97 ![X0,X1]: (ld(X0,mult(X0,X1))=X1)),
% 27.73/3.97 inference(cnf_transformation,[status(thm)],[f2])).
% 27.73/3.97 fof(f10,plain,(
% 27.73/3.97 ![X0,X1]: (mult(rd(X0,X1),X1)=X0)),
% 27.73/3.97 inference(cnf_transformation,[status(thm)],[f3])).
% 27.73/3.97 fof(f11,plain,(
% 27.73/3.97 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 27.73/3.97 inference(cnf_transformation,[status(thm)],[f4])).
% 27.73/3.97 fof(f12,plain,(
% 27.73/3.97 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X2),X0)=mult(X0,mult(X1,mult(X2,X0))))),
% 27.73/3.97 inference(cnf_transformation,[status(thm)],[f5])).
% 27.73/3.97 fof(f13,plain,(
% 27.73/3.97 (?[X0,X1]: (~mult(X0,ld(X1,X1))=X0|~mult(ld(X1,X1),X0)=X0))),
% 27.73/3.97 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 27.73/3.97 fof(f14,plain,(
% 27.73/3.97 (?[X0,X1]: ~mult(X0,ld(X1,X1))=X0)|(?[X0,X1]: ~mult(ld(X1,X1),X0)=X0)),
% 27.73/3.97 inference(miniscoping,[status(thm)],[f13])).
% 27.73/3.97 fof(f15,plain,(
% 27.73/3.97 ~mult(sK0_skl,ld(sK1_skl,sK1_skl))=sK0_skl|~mult(ld(sK3_skl,sK3_skl),sK2_skl)=sK2_skl),
% 27.73/3.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl),skolemize(X0,sK2_skl),skolemize(X1,sK3_skl)],[f14])).
% 27.73/3.97 fof(f16,plain,(
% 27.73/3.97 ~mult(sK0_skl,ld(sK1_skl,sK1_skl))=sK0_skl|~mult(ld(sK3_skl,sK3_skl),sK2_skl)=sK2_skl),
% 27.73/3.97 inference(cnf_transformation,[status(thm)],[f15])).
% 27.73/3.97 fof(f19,plain,(
% 27.73/3.97 ![X0,X1]: (ld(rd(X0,X1),X0)=X1)),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f10,f9])).
% 27.73/3.97 fof(f21,plain,(
% 27.73/3.97 ![X0,X1]: (rd(X0,ld(X1,X0))=X1)),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f8,f11])).
% 27.73/3.97 fof(f24,plain,(
% 27.73/3.97 ![X0,X1,X2]: (mult(X0,X1)=mult(X1,mult(X2,mult(ld(mult(X1,X2),X0),X1))))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f8,f12])).
% 27.73/3.97 fof(f26,plain,(
% 27.73/3.97 ![X0,X1,X2]: (mult(mult(X0,X1),rd(X0,X2))=mult(rd(X0,X2),mult(X2,mult(X1,rd(X0,X2)))))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f10,f12])).
% 27.73/3.97 fof(f27,plain,(
% 27.73/3.97 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(X2,mult(ld(X2,X0),mult(X1,X2))))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f8,f12])).
% 27.73/3.97 fof(f28,plain,(
% 27.73/3.97 ![X0,X1,X2]: (rd(mult(X0,mult(X1,mult(X2,X0))),X0)=mult(mult(X0,X1),X2))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f12,f11])).
% 27.73/3.97 fof(f44,plain,(
% 27.73/3.97 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(X2,mult(ld(mult(X0,X2),X1),X0)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f24,f9])).
% 27.73/3.97 fof(f55,plain,(
% 27.73/3.97 ![X0,X1,X2]: (mult(mult(X0,rd(X1,X2)),X2)=mult(X2,mult(ld(X2,X0),X1)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f10,f27])).
% 27.73/3.97 fof(f61,plain,(
% 27.73/3.97 ![X0,X1,X2]: (ld(X0,mult(mult(X1,X2),X0))=mult(ld(X0,X1),mult(X2,X0)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f27,f9])).
% 27.73/3.97 fof(f64,plain,(
% 27.73/3.97 ![X0,X1,X2]: (rd(mult(X0,X1),X0)=mult(mult(X0,rd(X1,mult(X2,X0))),X2))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f10,f28])).
% 27.73/3.97 fof(f65,plain,(
% 27.73/3.97 ![X0,X1,X2]: (rd(mult(mult(X0,X1),mult(mult(X2,X0),X1)),mult(X0,X1))=mult(mult(mult(X0,X1),X1),ld(X1,X2)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f27,f28])).
% 27.73/3.97 fof(f67,plain,(
% 27.73/3.97 ![X0,X1,X2]: (rd(mult(X0,mult(X1,X2)),X0)=mult(mult(X0,X1),rd(X2,X0)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f10,f28])).
% 27.73/3.97 fof(f69,plain,(
% 27.73/3.97 ![X0,X1,X2]: (rd(mult(ld(X0,X1),mult(X2,X1)),ld(X0,X1))=mult(mult(ld(X0,X1),X2),X0))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f8,f28])).
% 27.73/3.97 fof(f106,plain,(
% 27.73/3.97 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(ld(X0,X2),mult(ld(X2,X1),X0)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f8,f44])).
% 27.73/3.97 fof(f120,plain,(
% 27.73/3.97 ![X0,X1,X2]: (ld(X0,ld(X1,mult(X2,X1)))=mult(ld(mult(X1,X0),X2),X1))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f44,f9])).
% 27.73/3.97 fof(f151,plain,(
% 27.73/3.97 ![X0,X1,X2]: (rd(mult(X0,mult(ld(X0,X1),X2)),X0)=mult(X1,rd(X2,X0)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f55,f11])).
% 27.73/3.97 fof(f264,plain,(
% 27.73/3.97 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(ld(X0,rd(X1,X2)),mult(X2,X0)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f10,f61])).
% 27.73/3.97 fof(f325,plain,(
% 27.73/3.97 ![X0,X1,X2]: (rd(rd(mult(X0,X1),X0),X2)=mult(X0,rd(X1,mult(X2,X0))))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f64,f11])).
% 27.73/3.97 fof(f615,plain,(
% 27.73/3.97 ![X0,X1]: (ld(X0,X1)=mult(ld(mult(X1,X0),X1),X1))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f9,f120])).
% 27.73/3.97 fof(f622,plain,(
% 27.73/3.97 ![X0,X1,X2]: (ld(X0,ld(X1,X2))=mult(ld(mult(X1,X0),rd(X2,X1)),X1))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f10,f120])).
% 27.73/3.97 fof(f651,plain,(
% 27.73/3.97 ![X0,X1]: (ld(X0,rd(X1,X0))=mult(ld(X1,rd(X1,X0)),rd(X1,X0)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f10,f615])).
% 27.73/3.97 fof(f654,plain,(
% 27.73/3.97 ![X0,X1]: (ld(ld(X0,X1),X0)=mult(ld(X1,X0),X0))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f8,f615])).
% 27.73/3.97 fof(f677,plain,(
% 27.73/3.97 ![X0,X1]: (rd(ld(X0,X1),X1)=ld(mult(X1,X0),X1))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f615,f11])).
% 27.73/3.97 fof(f743,plain,(
% 27.73/3.97 ![X0,X1]: (rd(X0,mult(ld(X1,X0),X0))=ld(X0,X1))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f654,f21])).
% 27.73/3.97 fof(f840,plain,(
% 27.73/3.97 ![X0,X1]: (rd(ld(X0,rd(X1,X0)),rd(X1,X0))=ld(X1,rd(X1,X0)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f10,f677])).
% 27.73/3.97 fof(f851,plain,(
% 27.73/3.97 ![X0,X1]: (rd(X0,rd(ld(X1,X0),X0))=mult(X0,X1))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f677,f21])).
% 27.73/3.97 fof(f872,plain,(
% 27.73/3.97 ![X0,X1]: (rd(X0,mult(X1,X0))=ld(X0,rd(X0,X1)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f19,f743])).
% 27.73/3.97 fof(f885,plain,(
% 27.73/3.97 ![X0,X1]: (rd(ld(X0,rd(X1,X0)),rd(X1,X0))=rd(X1,mult(X0,X1)))),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f872,f840])).
% 27.73/3.97 fof(f886,plain,(
% 27.73/3.97 ![X0,X1]: (ld(X0,rd(X1,X0))=mult(rd(X1,mult(X0,X1)),rd(X1,X0)))),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f872,f651])).
% 27.73/3.97 fof(f898,plain,(
% 27.73/3.97 ![X0,X1]: (rd(X0,rd(X1,X0))=mult(X0,rd(X0,X1)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f19,f851])).
% 27.73/3.97 fof(f901,plain,(
% 27.73/3.97 ![X0,X1]: (rd(mult(X0,X1),rd(X1,mult(X0,X1)))=mult(mult(X0,X1),X0))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f9,f851])).
% 27.73/3.97 fof(f930,plain,(
% 27.73/3.97 ![X0,X1]: (rd(rd(X0,X1),rd(X0,mult(X1,X0)))=X0)),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f872,f21])).
% 27.73/3.97 fof(f1072,plain,(
% 27.73/3.97 ![X0,X1]: (rd(rd(X0,rd(X1,X0)),rd(X0,X1))=X0)),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f898,f11])).
% 27.73/3.97 fof(f1813,plain,(
% 27.73/3.97 ![X0,X1,X2]: (ld(ld(X0,X1),mult(X2,ld(X0,X1)))=mult(ld(ld(X0,X1),rd(X2,X0)),X1))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f8,f264])).
% 27.73/3.97 fof(f1847,plain,(
% 27.73/3.97 ![X0,X1,X2]: (rd(ld(X0,mult(X1,X0)),mult(X2,X0))=ld(X0,rd(X1,X2)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f264,f11])).
% 27.73/3.97 fof(f1937,plain,(
% 27.73/3.97 ![X0,X1,X2]: (rd(rd(mult(X0,X1),X0),rd(X2,X0))=mult(X0,rd(X1,X2)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f10,f325])).
% 27.73/3.97 fof(f1943,plain,(
% 27.73/3.97 ![X0,X1,X2]: (rd(rd(mult(ld(X0,X1),X2),ld(X0,X1)),X0)=mult(ld(X0,X1),rd(X2,X1)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f8,f325])).
% 27.73/3.97 fof(f2444,plain,(
% 27.73/3.97 ![X0,X1]: (ld(X0,ld(X1,mult(X1,X0)))=mult(rd(mult(X1,X0),mult(X1,mult(X1,X0))),X1))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f872,f622])).
% 27.73/3.97 fof(f2462,plain,(
% 27.73/3.97 ![X0,X1,X2]: (ld(ld(X0,X1),ld(X0,X2))=mult(ld(X1,rd(X2,X0)),X0))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f8,f622])).
% 27.73/3.97 fof(f2509,plain,(
% 27.73/3.97 ![X0,X1]: (ld(X0,X0)=mult(rd(mult(X1,X0),mult(X1,mult(X1,X0))),X1))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f9,f2444])).
% 27.73/3.97 fof(f3849,plain,(
% 27.73/3.97 ![X0,X1]: (rd(mult(ld(X0,X1),X1),ld(X1,X0))=mult(mult(ld(X0,X1),X1),ld(X0,X1)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f743,f901])).
% 27.73/3.97 fof(f5600,plain,(
% 27.73/3.97 ![X0]: (ld(X0,X0)=mult(rd(mult(ld(X0,X0),X0),ld(X0,mult(X0,X0))),ld(X0,X0)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f106,f2509])).
% 27.73/3.97 fof(f5679,plain,(
% 27.73/3.97 ![X0,X1]: (rd(ld(X0,X0),X1)=rd(mult(X1,X0),mult(X1,mult(X1,X0))))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f2509,f11])).
% 27.73/3.97 fof(f5717,plain,(
% 27.73/3.97 ![X0]: (ld(X0,X0)=mult(rd(mult(ld(X0,X0),X0),X0),ld(X0,X0)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f9,f5600])).
% 27.73/3.97 fof(f5718,plain,(
% 27.73/3.97 ![X0]: (ld(X0,X0)=mult(ld(X0,X0),ld(X0,X0)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f11,f5717])).
% 27.73/3.97 fof(f6346,plain,(
% 27.73/3.97 ![X0]: (ld(ld(X0,X0),mult(X0,ld(X0,X0)))=mult(ld(ld(X0,X0),X0),ld(X0,X0)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f5718,f106])).
% 27.73/3.97 fof(f6353,plain,(
% 27.73/3.97 ![X0,X1]: (rd(ld(ld(X0,X0),mult(X1,ld(X0,X0))),ld(X0,X0))=ld(ld(X0,X0),rd(X1,ld(X0,X0))))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f5718,f1847])).
% 27.73/3.97 fof(f6356,plain,(
% 27.73/3.97 ![X0,X1]: (rd(mult(mult(ld(X0,X0),ld(X0,X0)),mult(mult(X1,ld(X0,X0)),ld(X0,X0))),ld(X0,X0))=mult(mult(mult(ld(X0,X0),ld(X0,X0)),ld(X0,X0)),ld(ld(X0,X0),X1)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f5718,f65])).
% 27.73/3.97 fof(f6387,plain,(
% 27.73/3.97 ![X0,X1]: (ld(ld(X0,X0),mult(X1,ld(X0,X0)))=mult(ld(X0,X0),mult(ld(ld(X0,X0),X1),ld(X0,X0))))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f5718,f44])).
% 27.73/3.97 fof(f6390,plain,(
% 27.73/3.97 ![X0,X1]: (rd(mult(ld(X0,X0),mult(X1,ld(X0,X0))),ld(X0,X0))=mult(mult(ld(X0,X0),X1),ld(X0,X0)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f5718,f28])).
% 27.73/3.97 fof(f6391,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(X0,ld(X1,X1)),ld(X1,X1))=mult(ld(X1,X1),mult(ld(ld(X1,X1),X0),ld(X1,X1))))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f5718,f27])).
% 27.73/3.97 fof(f6393,plain,(
% 27.73/3.97 ![X0]: (rd(ld(X0,X0),ld(X0,X0))=ld(X0,X0))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f5718,f11])).
% 27.73/3.97 fof(f6394,plain,(
% 27.73/3.97 ![X0]: (ld(ld(X0,X0),ld(X0,X0))=ld(X0,X0))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f5718,f9])).
% 27.73/3.97 fof(f6416,plain,(
% 27.73/3.97 ![X0]: (mult(ld(ld(X0,X0),rd(X0,X0)),X0)=mult(ld(ld(X0,X0),X0),ld(X0,X0)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f1813,f6346])).
% 27.73/3.97 fof(f6417,plain,(
% 27.73/3.97 ![X0]: (mult(ld(ld(X0,X0),rd(X0,X0)),X0)=mult(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f654,f6416])).
% 27.73/3.97 fof(f6418,plain,(
% 27.73/3.97 ![X0]: (mult(ld(ld(X0,X0),rd(X0,X0)),X0)=rd(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f3849,f6417])).
% 27.73/3.97 fof(f6424,plain,(
% 27.73/3.97 ![X0,X1]: (rd(mult(ld(ld(X0,X0),rd(X1,X0)),X0),ld(X0,X0))=ld(ld(X0,X0),rd(X1,ld(X0,X0))))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f1813,f6353])).
% 27.73/3.97 fof(f6428,plain,(
% 27.73/3.97 ![X0,X1]: (rd(mult(ld(X0,X0),mult(mult(X1,ld(X0,X0)),ld(X0,X0))),ld(X0,X0))=mult(mult(mult(ld(X0,X0),ld(X0,X0)),ld(X0,X0)),ld(ld(X0,X0),X1)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f5718,f6356])).
% 27.73/3.97 fof(f6429,plain,(
% 27.73/3.97 ![X0,X1]: (rd(mult(ld(X0,X0),mult(mult(X1,ld(X0,X0)),ld(X0,X0))),ld(X0,X0))=mult(mult(ld(X0,X0),ld(X0,X0)),ld(ld(X0,X0),X1)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f5718,f6428])).
% 27.73/3.97 fof(f6430,plain,(
% 27.73/3.97 ![X0,X1]: (rd(mult(ld(X0,X0),mult(mult(X1,ld(X0,X0)),ld(X0,X0))),ld(X0,X0))=mult(ld(X0,X0),ld(ld(X0,X0),X1)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f5718,f6429])).
% 27.73/3.97 fof(f6431,plain,(
% 27.73/3.97 ![X0,X1]: (rd(mult(ld(X0,X0),mult(mult(X1,ld(X0,X0)),ld(X0,X0))),ld(X0,X0))=X1)),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f8,f6430])).
% 27.73/3.97 fof(f6495,plain,(
% 27.73/3.97 ![X0,X1]: (mult(ld(ld(X0,X0),rd(X1,X0)),X0)=mult(ld(X0,X0),mult(ld(ld(X0,X0),X1),ld(X0,X0))))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f1813,f6387])).
% 27.73/3.97 fof(f6496,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,ld(X0,X0))),ld(X0,X0))=X1)),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f6390,f6431])).
% 27.73/3.97 fof(f6497,plain,(
% 27.73/3.97 ![X0,X1]: (mult(ld(ld(X0,X0),rd(X1,X0)),X0)=mult(mult(X1,ld(X0,X0)),ld(X0,X0)))),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f6391,f6495])).
% 27.73/3.97 fof(f6507,plain,(
% 27.73/3.97 ![X0]: (mult(ld(X0,rd(X0,X0)),X0)=ld(X0,X0))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f2462,f6394])).
% 27.73/3.97 fof(f6508,plain,(
% 27.73/3.97 ![X0]: (mult(rd(X0,mult(X0,X0)),X0)=ld(X0,X0))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f872,f6507])).
% 27.73/3.97 fof(f6518,plain,(
% 27.73/3.97 ![X0,X1]: (rd(mult(mult(X0,ld(X1,X1)),ld(X1,X1)),ld(X1,X1))=ld(ld(X1,X1),rd(X0,ld(X1,X1))))),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f6497,f6424])).
% 27.73/3.97 fof(f6519,plain,(
% 27.73/3.97 ![X0]: (mult(mult(X0,ld(X0,X0)),ld(X0,X0))=rd(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f6497,f6418])).
% 27.73/3.97 fof(f6523,plain,(
% 27.73/3.97 ![X0,X1]: (mult(X0,ld(X1,X1))=ld(ld(X1,X1),rd(X0,ld(X1,X1))))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f11,f6518])).
% 27.73/3.97 fof(f6524,plain,(
% 27.73/3.97 ![X0]: (mult(X0,ld(X0,X0))=rd(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f8,f6519])).
% 27.73/3.97 fof(f6525,plain,(
% 27.73/3.97 ![X0]: (X0=rd(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f8,f6524])).
% 27.73/3.97 fof(f6703,plain,(
% 27.73/3.97 ![X0,X1]: (rd(rd(ld(X0,X0),rd(X0,mult(X0,X0))),rd(X1,rd(X0,mult(X0,X0))))=mult(rd(X0,mult(X0,X0)),rd(X0,X1)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f6508,f1937])).
% 27.73/3.97 fof(f6707,plain,(
% 27.73/3.97 ![X0,X1]: (rd(mult(mult(rd(X0,mult(X0,X0)),X0),mult(mult(X1,rd(X0,mult(X0,X0))),X0)),ld(X0,X0))=mult(mult(mult(rd(X0,mult(X0,X0)),X0),X0),ld(X0,X1)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f6508,f65])).
% 27.73/3.97 fof(f6742,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(X0,rd(X1,mult(X1,X1))),X1)=mult(X1,mult(ld(X1,X0),ld(X1,X1))))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f6508,f27])).
% 27.73/3.97 fof(f6744,plain,(
% 27.73/3.97 ![X0]: (rd(ld(X0,X0),X0)=rd(X0,mult(X0,X0)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f6508,f11])).
% 27.73/3.97 fof(f6763,plain,(
% 27.73/3.97 ![X0,X1]: (rd(mult(ld(X0,X0),mult(mult(X1,rd(X0,mult(X0,X0))),X0)),ld(X0,X0))=mult(mult(mult(rd(X0,mult(X0,X0)),X0),X0),ld(X0,X1)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f6508,f6707])).
% 27.73/3.97 fof(f6764,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)=mult(mult(mult(rd(X0,mult(X0,X0)),X0),X0),ld(X0,X1)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f69,f6763])).
% 27.73/3.97 fof(f6765,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)=mult(mult(ld(X0,X0),X0),ld(X0,X1)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f6508,f6764])).
% 27.73/3.97 fof(f7011,plain,(
% 27.73/3.97 ![X0,X1]: (rd(X0,rd(X1,ld(X0,X0)))=mult(ld(X0,X0),rd(X0,X1)))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f6525,f1937])).
% 27.73/3.97 fof(f7015,plain,(
% 27.73/3.97 ![X0]: (ld(ld(X0,X0),rd(mult(ld(X0,X0),X0),ld(X0,X0)))=mult(rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))),X0))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f6525,f886])).
% 27.73/3.97 fof(f7016,plain,(
% 27.73/3.97 ![X0]: (rd(ld(ld(X0,X0),rd(mult(ld(X0,X0),X0),ld(X0,X0))),X0)=rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f6525,f885])).
% 27.73/3.97 fof(f7021,plain,(
% 27.73/3.97 ![X0]: (rd(rd(ld(X0,X0),X0),rd(ld(X0,X0),mult(ld(X0,X0),X0)))=ld(X0,X0))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f6525,f1072])).
% 27.73/3.97 fof(f7051,plain,(
% 27.73/3.97 ![X0]: (mult(mult(ld(X0,X0),X0),ld(X0,X0))=mult(rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))),X0))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f6523,f7015])).
% 27.73/3.97 fof(f7052,plain,(
% 27.73/3.97 ![X0]: (rd(mult(ld(X0,X0),X0),ld(X0,X0))=mult(rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))),X0))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f3849,f7051])).
% 27.73/3.97 fof(f7053,plain,(
% 27.73/3.97 ![X0]: (X0=mult(rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))),X0))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f6525,f7052])).
% 27.73/3.97 fof(f7054,plain,(
% 27.73/3.97 ![X0]: (X0=mult(rd(ld(X0,X0),ld(X0,X0)),X0))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f5679,f7053])).
% 27.73/3.97 fof(f7058,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)=mult(X0,ld(X0,X1)))),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f7059,f6765])).
% 27.73/3.97 fof(f7059,plain,(
% 27.73/3.97 ![X0]: (X0=mult(ld(X0,X0),X0))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f6393,f7054])).
% 27.73/3.97 fof(f7060,plain,(
% 27.73/3.97 ![X0]: (rd(mult(mult(ld(X0,X0),X0),ld(X0,X0)),X0)=rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f6523,f7016])).
% 27.73/3.97 fof(f7061,plain,(
% 27.73/3.97 ![X0]: (rd(rd(mult(ld(X0,X0),X0),ld(X0,X0)),X0)=rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f3849,f7060])).
% 27.73/3.97 fof(f7062,plain,(
% 27.73/3.97 ![X0]: (mult(ld(X0,X0),rd(X0,X0))=rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f1943,f7061])).
% 27.73/3.97 fof(f7063,plain,(
% 27.73/3.97 ![X0]: (rd(X0,rd(X0,ld(X0,X0)))=rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f7011,f7062])).
% 27.73/3.97 fof(f7064,plain,(
% 27.73/3.97 ![X0]: (rd(X0,X0)=rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f21,f7063])).
% 27.73/3.97 fof(f7065,plain,(
% 27.73/3.97 ![X0]: (rd(X0,X0)=ld(X0,X0))),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f7066,f6393])).
% 27.73/3.97 fof(f7066,plain,(
% 27.73/3.97 ![X0]: (rd(X0,X0)=rd(ld(X0,X0),ld(X0,X0)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f5679,f7064])).
% 27.73/3.97 fof(f7079,plain,(
% 27.73/3.97 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(ld(X0,X0),mult(ld(X0,X0),X0)))=ld(X0,X0))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f6744,f7021])).
% 27.73/3.97 fof(f7080,plain,(
% 27.73/3.97 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(ld(X0,X0),X0))=ld(X0,X0))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f7059,f7079])).
% 27.73/3.97 fof(f7081,plain,(
% 27.73/3.97 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))=ld(X0,X0))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f6744,f7080])).
% 27.73/3.97 fof(f7101,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)=X1)),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f8,f7058])).
% 27.73/3.97 fof(f7102,plain,(
% 27.73/3.97 ~mult(sK0_skl,ld(sK1_skl,sK1_skl))=sK0_skl|~mult(rd(sK3_skl,sK3_skl),sK2_skl)=sK2_skl),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f7065,f16])).
% 27.73/3.97 fof(f7142,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)=X1)),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f7065,f7101])).
% 27.73/3.97 fof(f7144,plain,(
% 27.73/3.97 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))=rd(X0,X0))),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f7065,f7081])).
% 27.73/3.97 fof(f7158,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(X0,rd(X1,mult(X1,X1))),X1)=mult(X1,mult(ld(X1,X0),rd(X1,X1))))),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f7065,f6742])).
% 27.73/3.97 fof(f7169,plain,(
% 27.73/3.97 ![X0,X1]: (rd(rd(rd(X0,X0),rd(X0,mult(X0,X0))),rd(X1,rd(X0,mult(X0,X0))))=mult(rd(X0,mult(X0,X0)),rd(X0,X1)))),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f7065,f6703])).
% 27.73/3.97 fof(f7173,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,ld(X0,X0))),rd(X0,X0))=X1)),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f7065,f6496])).
% 27.73/3.97 fof(f7200,plain,(
% 27.73/3.97 ~mult(sK0_skl,rd(sK1_skl,sK1_skl))=sK0_skl|~mult(rd(sK3_skl,sK3_skl),sK2_skl)=sK2_skl),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f7065,f7102])).
% 27.73/3.97 fof(f7222,plain,(
% 27.73/3.97 ![X0,X1]: (rd(X0,rd(X1,rd(X0,mult(X0,X0))))=mult(rd(X0,mult(X0,X0)),rd(X0,X1)))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f930,f7169])).
% 27.73/3.97 fof(f7228,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(rd(X0,X0),mult(X1,ld(X0,X0))),rd(X0,X0))=X1)),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f7065,f7173])).
% 27.73/3.97 fof(f7229,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(rd(X0,X0),mult(X1,rd(X0,X0))),rd(X0,X0))=X1)),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f7065,f7228])).
% 27.73/3.97 fof(f10951,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(rd(X0,X0),X1),X0)=mult(rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0))),mult(X1,rd(rd(X0,mult(X0,X0)),mult(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))))))),
% 27.73/3.97 inference(paramodulation,[status(thm)],[f7142,f7142])).
% 27.73/3.97 fof(f11071,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(rd(X0,X0),X1),X0)=mult(rd(X0,X0),mult(X1,rd(rd(X0,mult(X0,X0)),mult(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))))))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f7144,f10951])).
% 27.73/3.97 fof(f11072,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(rd(X0,X0),X1),X0)=mult(rd(X0,X0),mult(X1,rd(rd(X0,mult(X0,X0)),rd(X0,rd(mult(X0,X0),rd(X0,mult(X0,X0))))))))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f7222,f11071])).
% 27.73/3.97 fof(f11073,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(rd(X0,X0),X1),X0)=mult(rd(X0,X0),mult(X1,rd(rd(X0,mult(X0,X0)),rd(X0,mult(mult(X0,X0),X0))))))),
% 27.73/3.97 inference(forward_demodulation,[status(thm)],[f901,f11072])).
% 27.73/3.97 fof(f11074,plain,(
% 27.73/3.97 ![X0,X1]: (mult(rd(X0,X0),mult(mult(X1,rd(X0,mult(X0,X0))),X0))=X1)),
% 27.73/3.97 inference(backward_demodulation,[status(thm)],[f11078,f7142])).
% 27.73/3.97 fof(f11078,plain,(
% 27.73/3.97 ![X0,X1]: (mult(mult(rd(X0,X0),X1),X0)=mult(rd(X0,X0),mult(X1,X0)))),
% 10.14/4.04 inference(forward_demodulation,[status(thm)],[f930,f11073])).
% 10.14/4.04 fof(f11278,plain,(
% 10.14/4.04 ![X0,X1]: (mult(rd(X0,X0),mult(X0,mult(ld(X0,X1),rd(X0,X0))))=X1)),
% 10.14/4.04 inference(forward_demodulation,[status(thm)],[f7158,f11074])).
% 10.14/4.04 fof(f11279,plain,(
% 10.14/4.04 ![X0,X1]: (mult(mult(X0,ld(X0,X1)),rd(X0,X0))=X1)),
% 10.14/4.04 inference(forward_demodulation,[status(thm)],[f26,f11278])).
% 10.14/4.04 fof(f11280,plain,(
% 10.14/4.04 ![X0,X1]: (rd(mult(X0,mult(ld(X0,X1),X0)),X0)=X1)),
% 10.14/4.04 inference(forward_demodulation,[status(thm)],[f67,f11279])).
% 10.14/4.04 fof(f11281,plain,(
% 10.14/4.04 ~sK0_skl=sK0_skl|~mult(rd(sK3_skl,sK3_skl),sK2_skl)=sK2_skl),
% 10.14/4.04 inference(backward_demodulation,[status(thm)],[f11319,f7200])).
% 10.14/4.04 fof(f11283,plain,(
% 10.14/4.04 ![X0,X1]: (mult(rd(X0,X0),mult(X1,rd(X0,X0)))=X1)),
% 10.14/4.04 inference(backward_demodulation,[status(thm)],[f11319,f7229])).
% 10.14/4.04 fof(f11319,plain,(
% 10.14/4.04 ![X0,X1]: (mult(X0,rd(X1,X1))=X0)),
% 10.14/4.04 inference(forward_demodulation,[status(thm)],[f151,f11280])).
% 10.14/4.04 fof(f11407,plain,(
% 10.14/4.04 ~mult(rd(sK3_skl,sK3_skl),sK2_skl)=sK2_skl),
% 10.14/4.04 inference(trivial_equality_resolution,[status(thm)],[f11281])).
% 10.14/4.04 fof(f11408,plain,(
% 10.14/4.04 ~sK2_skl=sK2_skl),
% 10.14/4.04 inference(backward_demodulation,[status(thm)],[f11435,f11407])).
% 10.14/4.04 fof(f11435,plain,(
% 10.14/4.04 ![X0,X1]: (mult(rd(X0,X0),X1)=X1)),
% 10.14/4.04 inference(forward_demodulation,[status(thm)],[f11319,f11283])).
% 10.14/4.04 fof(f11771,plain,(
% 10.14/4.04 $false),
% 10.14/4.04 inference(trivial_equality_resolution,[status(thm)],[f11408])).
% 10.14/4.04 % SZS output end CNFRefutation for theBenchmark.p
% 10.14/4.04 % Elapsed time: 3.654055 seconds
% 10.14/4.04 % CPU time: 28.627984 seconds
% 10.14/4.04 % Total memory used: 628.627 MB
% 10.14/4.04 % Net memory used: 622.770 MB
%------------------------------------------------------------------------------