%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP660+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 : n012.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 109.03s 19.10s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP660+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/5.31 % Computer : n012.cluster.edu
% 0.03/5.31 % Model : x86_64 x86_64
% 0.03/5.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/5.31 % Memory : 8046.5625MB
% 0.03/5.31 % OS : Linux 6.8.0-71-generic
% 0.03/5.31 % CPULimit : 300
% 0.03/5.31 % WCLimit : 300
% 0.03/5.31 % DateTime : Sun Sep 20 20:29:59 UTC 2026
% 0.03/5.31 % CPUTime :
% 0.03/5.32 % Drodi V4.1.1
% 109.03/19.10 % Refutation found
% 109.03/19.10 % SZS status Theorem for theBenchmark: Theorem is valid
% 109.03/19.10 % SZS output start CNFRefutation for theBenchmark
% 109.03/19.10 fof(f1,axiom,(
% 109.03/19.10 (! [B,A] : mult(A,ld(A,B)) = B )),
% 109.03/19.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.03/19.10 fof(f2,axiom,(
% 109.03/19.10 (! [B,A] : ld(A,mult(A,B)) = B )),
% 109.03/19.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.03/19.10 fof(f3,axiom,(
% 109.03/19.10 (! [B,A] : mult(rd(A,B),B) = A )),
% 109.03/19.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.03/19.10 fof(f4,axiom,(
% 109.03/19.10 (! [B,A] : rd(mult(A,B),B) = A )),
% 109.03/19.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.03/19.10 fof(f5,axiom,(
% 109.03/19.10 (! [C,B,A] : mult(mult(mult(A,B),C),A) = mult(A,mult(B,mult(C,A))) )),
% 109.03/19.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.03/19.10 fof(f6,conjecture,(
% 109.03/19.10 (? [X0] :(! [X1] :( mult(X1,X0) = X1& mult(X0,X1) = X1 ) ))),
% 109.03/19.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.03/19.10 fof(f7,negated_conjecture,(
% 109.03/19.10 ~((? [X0] :(! [X1] :( mult(X1,X0) = X1& mult(X0,X1) = X1 ) )))),
% 109.03/19.10 inference(negated_conjecture,[status(cth)],[f6])).
% 109.03/19.10 fof(f8,plain,(
% 109.03/19.10 ![X0,X1]: (mult(X0,ld(X0,X1))=X1)),
% 109.03/19.10 inference(cnf_transformation,[status(thm)],[f1])).
% 109.03/19.10 fof(f9,plain,(
% 109.03/19.10 ![X0,X1]: (ld(X0,mult(X0,X1))=X1)),
% 109.03/19.10 inference(cnf_transformation,[status(thm)],[f2])).
% 109.03/19.10 fof(f10,plain,(
% 109.03/19.10 ![X0,X1]: (mult(rd(X0,X1),X1)=X0)),
% 109.03/19.10 inference(cnf_transformation,[status(thm)],[f3])).
% 109.03/19.10 fof(f11,plain,(
% 109.03/19.10 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 109.03/19.10 inference(cnf_transformation,[status(thm)],[f4])).
% 109.03/19.10 fof(f12,plain,(
% 109.03/19.10 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X2),X0)=mult(X0,mult(X1,mult(X2,X0))))),
% 109.03/19.10 inference(cnf_transformation,[status(thm)],[f5])).
% 109.03/19.10 fof(f13,plain,(
% 109.03/19.10 (![X0]: ?[X1]: (~mult(X1,X0)=X1|~mult(X0,X1)=X1))),
% 109.03/19.10 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 109.03/19.10 fof(f14,plain,(
% 109.03/19.10 ![X0]: ((?[X1]: ~mult(X1,X0)=X1)|(?[X1]: ~mult(X0,X1)=X1))),
% 109.03/19.10 inference(miniscoping,[status(thm)],[f13])).
% 109.03/19.10 fof(f15,plain,(
% 109.03/19.10 ![X0]: (~mult(sK0_skl(X0),X0)=sK0_skl(X0)|~mult(X0,sK1_skl(X0))=sK1_skl(X0))),
% 109.03/19.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X1,sK0_skl(X0)),skolemize(X1,sK1_skl(X0))],[f14])).
% 109.03/19.10 fof(f16,plain,(
% 109.03/19.10 ![X0]: (~mult(sK0_skl(X0),X0)=sK0_skl(X0)|~mult(X0,sK1_skl(X0))=sK1_skl(X0))),
% 109.03/19.10 inference(cnf_transformation,[status(thm)],[f15])).
% 109.03/19.10 fof(f19,plain,(
% 109.03/19.10 ![X0,X1]: (ld(rd(X0,X1),X0)=X1)),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10,f9])).
% 109.03/19.10 fof(f21,plain,(
% 109.03/19.10 ![X0,X1]: (rd(X0,ld(X1,X0))=X1)),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f8,f11])).
% 109.03/19.10 fof(f23,plain,(
% 109.03/19.10 ![X0,X1,X2]: (mult(mult(X0,mult(X1,mult(X2,X0))),mult(X0,X1))=mult(mult(X0,X1),mult(X2,mult(X0,mult(X0,X1)))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f12,f12])).
% 109.03/19.10 fof(f24,plain,(
% 109.03/19.10 ![X0,X1,X2]: (mult(X0,X1)=mult(X1,mult(X2,mult(ld(mult(X1,X2),X0),X1))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f8,f12])).
% 109.03/19.10 fof(f27,plain,(
% 109.03/19.10 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(X2,mult(ld(X2,X0),mult(X1,X2))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f8,f12])).
% 109.03/19.10 fof(f28,plain,(
% 109.03/19.10 ![X0,X1,X2]: (rd(mult(X0,mult(X1,mult(X2,X0))),X0)=mult(mult(X0,X1),X2))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f12,f11])).
% 109.03/19.10 fof(f44,plain,(
% 109.03/19.10 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(X2,mult(ld(mult(X0,X2),X1),X0)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f24,f9])).
% 109.03/19.10 fof(f58,plain,(
% 109.03/19.10 ![X0,X1,X2]: (mult(mult(ld(X0,X1),mult(X2,X1)),mult(ld(X0,X1),X2))=mult(mult(ld(X0,X1),X2),mult(X0,mult(ld(X0,X1),mult(ld(X0,X1),X2)))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f8,f23])).
% 109.03/19.10 fof(f84,plain,(
% 109.03/19.10 ![X0,X1,X2]: (mult(mult(X0,rd(X1,X2)),X2)=mult(X2,mult(ld(X2,X0),X1)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10,f27])).
% 109.03/19.10 fof(f94,plain,(
% 109.03/19.10 ![X0,X1,X2]: (ld(X0,mult(mult(X1,X2),X0))=mult(ld(X0,X1),mult(X2,X0)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f27,f9])).
% 109.03/19.10 fof(f105,plain,(
% 109.03/19.10 ![X0,X1,X2]: (rd(mult(X0,X1),X0)=mult(mult(X0,rd(X1,mult(X2,X0))),X2))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10,f28])).
% 109.03/19.10 fof(f153,plain,(
% 109.03/19.10 ![X0,X1,X2]: (ld(rd(X0,X1),mult(X2,rd(X0,X1)))=mult(X1,mult(ld(X0,X2),rd(X0,X1))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10,f44])).
% 109.03/19.10 fof(f156,plain,(
% 109.03/19.10 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(ld(X0,X2),mult(ld(X2,X1),X0)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f8,f44])).
% 109.03/19.10 fof(f174,plain,(
% 109.03/19.10 ![X0,X1,X2]: (ld(X0,ld(X1,mult(X2,X1)))=mult(ld(mult(X1,X0),X2),X1))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f44,f9])).
% 109.03/19.10 fof(f303,plain,(
% 109.03/19.10 ![X0,X1,X2]: (mult(X0,X1)=mult(X1,mult(ld(X1,rd(X0,rd(X2,X1))),X2)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10,f84])).
% 109.03/19.10 fof(f326,plain,(
% 109.03/19.10 ![X0,X1,X2]: (rd(mult(X0,mult(ld(X0,X1),X2)),X0)=mult(X1,rd(X2,X0)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f84,f11])).
% 109.03/19.10 fof(f390,plain,(
% 109.03/19.10 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(ld(X0,rd(X1,X2)),mult(X2,X0)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10,f94])).
% 109.03/19.10 fof(f461,plain,(
% 109.03/19.10 ![X0,X1,X2]: (rd(rd(mult(X0,X1),X0),X2)=mult(X0,rd(X1,mult(X2,X0))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f105,f11])).
% 109.03/19.10 fof(f710,plain,(
% 109.03/19.10 ![X0,X1]: (ld(X0,X1)=mult(ld(mult(X1,X0),X1),X1))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f9,f174])).
% 109.03/19.10 fof(f718,plain,(
% 109.03/19.10 ![X0,X1,X2]: (ld(X0,ld(X1,X2))=mult(ld(mult(X1,X0),rd(X2,X1)),X1))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10,f174])).
% 109.03/19.10 fof(f751,plain,(
% 109.03/19.10 ![X0,X1]: (ld(ld(X0,X1),X0)=mult(ld(X1,X0),X0))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f8,f710])).
% 109.03/19.10 fof(f775,plain,(
% 109.03/19.10 ![X0,X1]: (rd(ld(X0,X1),X1)=ld(mult(X1,X0),X1))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f710,f11])).
% 109.03/19.10 fof(f1235,plain,(
% 109.03/19.10 ![X0,X1]: (rd(X0,mult(ld(X1,X0),X0))=ld(X0,X1))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f751,f21])).
% 109.03/19.10 fof(f1263,plain,(
% 109.03/19.10 ![X0,X1]: (rd(X0,rd(ld(X1,X0),X0))=mult(X0,X1))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f775,f21])).
% 109.03/19.10 fof(f1284,plain,(
% 109.03/19.10 ![X0,X1]: (rd(X0,mult(X1,X0))=ld(X0,rd(X0,X1)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f19,f1235])).
% 109.03/19.10 fof(f1310,plain,(
% 109.03/19.10 ![X0,X1]: (rd(X0,rd(X1,X0))=mult(X0,rd(X0,X1)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f19,f1263])).
% 109.03/19.10 fof(f2144,plain,(
% 109.03/19.10 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(ld(X0,rd(X1,rd(X2,X0))),X2))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f303,f9])).
% 109.03/19.10 fof(f2354,plain,(
% 109.03/19.10 ![X0,X1,X2]: (rd(mult(X0,X1),X0)=mult(X2,rd(ld(ld(X0,X2),X1),X0)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f8,f326])).
% 109.03/19.10 fof(f2485,plain,(
% 109.03/19.10 ![X0,X1,X2]: (ld(ld(X0,X1),mult(X2,ld(X0,X1)))=mult(ld(ld(X0,X1),rd(X2,X0)),X1))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f8,f390])).
% 109.03/19.10 fof(f2526,plain,(
% 109.03/19.10 ![X0,X1,X2]: (rd(ld(X0,mult(X1,X0)),mult(X2,X0))=ld(X0,rd(X1,X2)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f390,f11])).
% 109.03/19.10 fof(f2910,plain,(
% 109.03/19.10 ![X0,X1,X2]: (rd(rd(mult(X0,X1),X0),rd(X2,X0))=mult(X0,rd(X1,X2)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10,f461])).
% 109.03/19.10 fof(f3382,plain,(
% 109.03/19.10 ![X0,X1]: (ld(X0,ld(X1,mult(X1,X0)))=mult(rd(mult(X1,X0),mult(X1,mult(X1,X0))),X1))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f1284,f718])).
% 109.03/19.10 fof(f3459,plain,(
% 109.03/19.10 ![X0,X1]: (ld(X0,X0)=mult(rd(mult(X1,X0),mult(X1,mult(X1,X0))),X1))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f9,f3382])).
% 109.03/19.10 fof(f7733,plain,(
% 109.03/19.10 ![X0,X1,X2]: (rd(ld(X0,mult(X1,X0)),X2)=ld(X0,rd(X1,rd(X2,X0))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f2144,f11])).
% 109.03/19.10 fof(f8086,plain,(
% 109.03/19.10 ![X0,X1,X2]: (ld(X0,rd(mult(X1,X2),X1))=rd(ld(ld(X1,X0),X2),X1))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f2354,f9])).
% 109.03/19.10 fof(f8915,plain,(
% 109.03/19.10 ![X0,X1,X2]: (rd(ld(X0,X1),mult(X2,X0))=ld(X0,rd(rd(X1,X0),X2)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10,f2526])).
% 109.03/19.10 fof(f9066,plain,(
% 109.03/19.10 ![X0,X1,X2]: (rd(rd(X0,X1),rd(X2,X1))=mult(X1,rd(ld(X1,X0),X2)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f8,f2910])).
% 109.03/19.10 fof(f10089,plain,(
% 109.03/19.10 ![X0]: (ld(X0,X0)=mult(rd(mult(ld(X0,X0),X0),ld(X0,mult(X0,X0))),ld(X0,X0)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f156,f3459])).
% 109.03/19.10 fof(f10230,plain,(
% 109.03/19.10 ![X0]: (ld(X0,X0)=mult(rd(mult(ld(X0,X0),X0),X0),ld(X0,X0)))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f9,f10089])).
% 109.03/19.10 fof(f10231,plain,(
% 109.03/19.10 ![X0]: (ld(X0,X0)=mult(ld(X0,X0),ld(X0,X0)))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f11,f10230])).
% 109.03/19.10 fof(f10520,plain,(
% 109.03/19.10 ![X0]: (mult(mult(ld(X0,X0),mult(ld(X0,X0),X0)),mult(ld(X0,X0),ld(X0,X0)))=mult(mult(ld(X0,X0),ld(X0,X0)),mult(X0,mult(ld(X0,X0),ld(X0,X0)))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10231,f58])).
% 109.03/19.10 fof(f10523,plain,(
% 109.03/19.10 ![X0]: (rd(mult(X0,ld(X0,X0)),X0)=mult(X0,rd(ld(X0,X0),X0)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10231,f326])).
% 109.03/19.10 fof(f10531,plain,(
% 109.03/19.10 ![X0,X1]: (rd(ld(ld(X0,X0),mult(X1,ld(X0,X0))),ld(X0,X0))=ld(ld(X0,X0),rd(X1,ld(X0,X0))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10231,f2526])).
% 109.03/19.10 fof(f10548,plain,(
% 109.03/19.10 ![X0,X1]: (rd(rd(mult(ld(X0,X0),X1),ld(X0,X0)),ld(X0,X0))=mult(ld(X0,X0),rd(X1,ld(X0,X0))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10231,f461])).
% 109.03/19.10 fof(f10569,plain,(
% 109.03/19.10 ![X0,X1]: (ld(ld(X0,X0),mult(X1,ld(X0,X0)))=mult(ld(X0,X0),mult(ld(ld(X0,X0),X1),ld(X0,X0))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10231,f44])).
% 109.03/19.10 fof(f10572,plain,(
% 109.03/19.10 ![X0,X1]: (rd(mult(ld(X0,X0),mult(X1,ld(X0,X0))),ld(X0,X0))=mult(mult(ld(X0,X0),X1),ld(X0,X0)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10231,f28])).
% 109.03/19.10 fof(f10573,plain,(
% 109.03/19.10 ![X0,X1]: (mult(mult(X0,ld(X1,X1)),ld(X1,X1))=mult(ld(X1,X1),mult(ld(ld(X1,X1),X0),ld(X1,X1))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10231,f27])).
% 109.03/19.10 fof(f10576,plain,(
% 109.03/19.10 ![X0,X1]: (mult(mult(ld(X0,X0),X1),ld(X0,X0))=mult(ld(X0,X0),mult(ld(X0,X0),mult(X1,ld(X0,X0)))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10231,f12])).
% 109.03/19.10 fof(f10595,plain,(
% 109.03/19.10 ![X0]: (mult(ld(X0,mult(X0,X0)),mult(ld(X0,X0),ld(X0,X0)))=mult(mult(ld(X0,X0),ld(X0,X0)),mult(X0,mult(ld(X0,X0),ld(X0,X0)))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f156,f10520])).
% 109.03/19.10 fof(f10596,plain,(
% 109.03/19.10 ![X0]: (mult(X0,mult(ld(X0,X0),ld(X0,X0)))=mult(mult(ld(X0,X0),ld(X0,X0)),mult(X0,mult(ld(X0,X0),ld(X0,X0)))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f9,f10595])).
% 109.03/19.10 fof(f10597,plain,(
% 109.03/19.10 ![X0]: (mult(X0,ld(X0,X0))=mult(mult(ld(X0,X0),ld(X0,X0)),mult(X0,mult(ld(X0,X0),ld(X0,X0)))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10231,f10596])).
% 109.03/19.10 fof(f10598,plain,(
% 109.03/19.10 ![X0]: (X0=mult(mult(ld(X0,X0),ld(X0,X0)),mult(X0,mult(ld(X0,X0),ld(X0,X0)))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f8,f10597])).
% 109.03/19.10 fof(f10599,plain,(
% 109.03/19.10 ![X0]: (X0=mult(ld(X0,X0),mult(X0,mult(ld(X0,X0),ld(X0,X0)))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10231,f10598])).
% 109.03/19.10 fof(f10600,plain,(
% 109.03/19.10 ![X0]: (X0=mult(ld(X0,X0),mult(X0,ld(X0,X0))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10231,f10599])).
% 109.03/19.10 fof(f10604,plain,(
% 109.03/19.10 ![X0]: (X0=mult(ld(X0,X0),X0))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f8,f10600])).
% 109.03/19.10 fof(f10614,plain,(
% 109.03/19.10 ![X0]: (rd(X0,X0)=mult(X0,rd(ld(X0,X0),X0)))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f8,f10523])).
% 109.03/19.10 fof(f10616,plain,(
% 109.03/19.10 ![X0]: (rd(X0,X0)=rd(rd(X0,X0),rd(X0,X0)))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f9066,f10614])).
% 109.03/19.10 fof(f10631,plain,(
% 109.03/19.10 ![X0,X1]: (rd(mult(ld(ld(X0,X0),rd(X1,X0)),X0),ld(X0,X0))=ld(ld(X0,X0),rd(X1,ld(X0,X0))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f2485,f10531])).
% 109.03/19.10 fof(f10750,plain,(
% 109.03/19.10 ![X0,X1]: (mult(ld(ld(X0,X0),rd(X1,X0)),X0)=mult(ld(X0,X0),mult(ld(ld(X0,X0),X1),ld(X0,X0))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f2485,f10569])).
% 109.03/19.10 fof(f10751,plain,(
% 109.03/19.10 ![X0,X1]: (mult(ld(ld(X0,X0),rd(X1,X0)),X0)=mult(mult(X1,ld(X0,X0)),ld(X0,X0)))),
% 109.03/19.10 inference(backward_demodulation,[status(thm)],[f10573,f10750])).
% 109.03/19.10 fof(f10777,plain,(
% 109.03/19.10 ![X0,X1]: (rd(mult(mult(X0,ld(X1,X1)),ld(X1,X1)),ld(X1,X1))=ld(ld(X1,X1),rd(X0,ld(X1,X1))))),
% 109.03/19.10 inference(backward_demodulation,[status(thm)],[f10751,f10631])).
% 109.03/19.10 fof(f10791,plain,(
% 109.03/19.10 ![X0,X1]: (mult(X0,ld(X1,X1))=ld(ld(X1,X1),rd(X0,ld(X1,X1))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f11,f10777])).
% 109.03/19.10 fof(f10799,plain,(
% 109.03/19.10 ![X0]: (rd(mult(X0,X0),X0)=mult(X0,rd(X0,X0)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10604,f326])).
% 109.03/19.10 fof(f10800,plain,(
% 109.03/19.10 ![X0]: (rd(X0,X0)=ld(X0,X0))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10604,f1235])).
% 109.03/19.10 fof(f10828,plain,(
% 109.03/19.10 ![X0,X1]: (rd(rd(X0,ld(X0,X0)),rd(X1,ld(X0,X0)))=mult(ld(X0,X0),rd(X0,X1)))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10604,f2910])).
% 109.03/19.10 fof(f10888,plain,(
% 109.03/19.10 ![X0]: (X0=mult(X0,rd(X0,X0)))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f11,f10799])).
% 109.03/19.10 fof(f10890,plain,(
% 109.03/19.10 ![X0]: (X0=rd(X0,rd(X0,X0)))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f1310,f10888])).
% 109.03/19.10 fof(f10915,plain,(
% 109.03/19.10 ![X0,X1]: (mult(X0,ld(X1,X1))=ld(ld(X1,X1),rd(X0,rd(X1,X1))))),
% 109.03/19.10 inference(backward_demodulation,[status(thm)],[f10800,f10791])).
% 109.03/19.10 fof(f10922,plain,(
% 109.03/19.10 ![X0,X1]: (mult(mult(ld(X0,X0),X1),ld(X0,X0))=mult(ld(X0,X0),mult(ld(X0,X0),mult(X1,rd(X0,X0)))))),
% 109.03/19.10 inference(backward_demodulation,[status(thm)],[f10800,f10576])).
% 109.03/19.10 fof(f10925,plain,(
% 109.03/19.10 ![X0,X1]: (rd(mult(ld(X0,X0),mult(X1,ld(X0,X0))),ld(X0,X0))=mult(mult(ld(X0,X0),X1),rd(X0,X0)))),
% 109.03/19.10 inference(backward_demodulation,[status(thm)],[f10800,f10572])).
% 109.03/19.10 fof(f10933,plain,(
% 109.03/19.10 ![X0,X1]: (rd(rd(mult(ld(X0,X0),X1),ld(X0,X0)),ld(X0,X0))=mult(ld(X0,X0),rd(X1,rd(X0,X0))))),
% 109.03/19.10 inference(backward_demodulation,[status(thm)],[f10800,f10548])).
% 109.03/19.10 fof(f11154,plain,(
% 109.03/19.10 ![X0,X1]: (rd(X0,rd(X1,ld(X0,X0)))=mult(ld(X0,X0),rd(X0,X1)))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f21,f10828])).
% 109.03/19.10 fof(f11155,plain,(
% 109.03/19.10 ![X0,X1]: (rd(X0,rd(X1,rd(X0,X0)))=mult(ld(X0,X0),rd(X0,X1)))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f11154])).
% 109.03/19.10 fof(f11156,plain,(
% 109.03/19.10 ![X0,X1]: (rd(X0,rd(X1,rd(X0,X0)))=mult(rd(X0,X0),rd(X0,X1)))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f11155])).
% 109.03/19.10 fof(f11449,plain,(
% 109.03/19.10 ![X0,X1]: (mult(X0,rd(X1,X1))=ld(ld(X1,X1),rd(X0,rd(X1,X1))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f10915])).
% 109.03/19.10 fof(f11450,plain,(
% 109.03/19.10 ![X0,X1]: (mult(X0,rd(X1,X1))=ld(rd(X1,X1),rd(X0,rd(X1,X1))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f11449])).
% 109.03/19.10 fof(f11484,plain,(
% 109.03/19.10 ![X0,X1]: (mult(mult(rd(X0,X0),X1),ld(X0,X0))=mult(ld(X0,X0),mult(ld(X0,X0),mult(X1,rd(X0,X0)))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f10922])).
% 109.03/19.10 fof(f11485,plain,(
% 109.03/19.10 ![X0,X1]: (mult(mult(rd(X0,X0),X1),rd(X0,X0))=mult(ld(X0,X0),mult(ld(X0,X0),mult(X1,rd(X0,X0)))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f11484])).
% 109.03/19.10 fof(f11486,plain,(
% 109.03/19.10 ![X0,X1]: (mult(mult(rd(X0,X0),X1),rd(X0,X0))=mult(rd(X0,X0),mult(ld(X0,X0),mult(X1,rd(X0,X0)))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f11485])).
% 109.03/19.10 fof(f11487,plain,(
% 109.03/19.10 ![X0,X1]: (mult(mult(rd(X0,X0),X1),rd(X0,X0))=mult(rd(X0,X0),mult(rd(X0,X0),mult(X1,rd(X0,X0)))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f11486])).
% 109.03/19.10 fof(f11499,plain,(
% 109.03/19.10 ![X0,X1]: (rd(mult(rd(X0,X0),mult(X1,ld(X0,X0))),ld(X0,X0))=mult(mult(ld(X0,X0),X1),rd(X0,X0)))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f10925])).
% 109.03/19.10 fof(f11500,plain,(
% 109.03/19.10 ![X0,X1]: (rd(mult(rd(X0,X0),mult(X1,rd(X0,X0))),ld(X0,X0))=mult(mult(ld(X0,X0),X1),rd(X0,X0)))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f11499])).
% 109.03/19.10 fof(f11501,plain,(
% 109.03/19.10 ![X0,X1]: (rd(mult(rd(X0,X0),mult(X1,rd(X0,X0))),rd(X0,X0))=mult(mult(ld(X0,X0),X1),rd(X0,X0)))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f11500])).
% 109.03/19.10 fof(f11502,plain,(
% 109.03/19.10 ![X0,X1]: (rd(mult(rd(X0,X0),mult(X1,rd(X0,X0))),rd(X0,X0))=mult(mult(rd(X0,X0),X1),rd(X0,X0)))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f11501])).
% 109.03/19.10 fof(f11537,plain,(
% 109.03/19.10 ![X0,X1]: (rd(rd(mult(rd(X0,X0),X1),ld(X0,X0)),ld(X0,X0))=mult(ld(X0,X0),rd(X1,rd(X0,X0))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f10933])).
% 109.03/19.10 fof(f11538,plain,(
% 109.03/19.10 ![X0,X1]: (rd(rd(mult(rd(X0,X0),X1),rd(X0,X0)),ld(X0,X0))=mult(ld(X0,X0),rd(X1,rd(X0,X0))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f11537])).
% 109.03/19.10 fof(f11539,plain,(
% 109.03/19.10 ![X0,X1]: (rd(rd(mult(rd(X0,X0),X1),rd(X0,X0)),rd(X0,X0))=mult(ld(X0,X0),rd(X1,rd(X0,X0))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f11538])).
% 109.03/19.10 fof(f11540,plain,(
% 109.03/19.10 ![X0,X1]: (rd(rd(mult(rd(X0,X0),X1),rd(X0,X0)),rd(X0,X0))=mult(rd(X0,X0),rd(X1,rd(X0,X0))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f10800,f11539])).
% 109.03/19.10 fof(f14575,plain,(
% 109.03/19.10 ![X0,X1]: (rd(ld(rd(X0,X0),mult(X1,rd(X0,X0))),rd(X0,X0))=ld(rd(X0,X0),rd(X1,rd(X0,X0))))),
% 109.03/19.10 inference(paramodulation,[status(thm)],[f10616,f7733])).
% 109.03/19.10 fof(f14669,plain,(
% 109.03/19.10 ![X0,X1]: (rd(mult(X0,mult(ld(X0,X1),rd(X0,X0))),rd(X0,X0))=ld(rd(X0,X0),rd(X1,rd(X0,X0))))),
% 109.03/19.10 inference(forward_demodulation,[status(thm)],[f153,f14575])).
% 109.03/19.10 fof(f14670,plain,(
% 109.03/19.10 ![X0,X1]: (rd(mult(X0,mult(ld(X0,X1),rd(X0,X0))),rd(X0,X0))=mult(X1,rd(X0,X0)))),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f11450,f14669])).
% 48.51/19.23 fof(f20711,plain,(
% 48.51/19.23 ![X0,X1]: (mult(rd(X0,rd(X1,X1)),rd(X1,X1))=rd(ld(rd(X1,X1),X0),mult(rd(X1,X1),rd(X1,X1))))),
% 48.51/19.23 inference(paramodulation,[status(thm)],[f8915,f11450])).
% 48.51/19.23 fof(f20712,plain,(
% 48.51/19.23 ![X0,X1]: (mult(mult(rd(X0,X0),X1),rd(X0,X0))=rd(ld(ld(rd(X0,X0),rd(X0,X0)),X1),rd(X0,X0)))),
% 48.51/19.23 inference(paramodulation,[status(thm)],[f8086,f11450])).
% 48.51/19.23 fof(f20729,plain,(
% 48.51/19.23 ![X0,X1]: (mult(mult(X0,rd(X1,X1)),rd(X1,X1))=ld(rd(X1,X1),X0))),
% 48.51/19.23 inference(paramodulation,[status(thm)],[f11,f11450])).
% 48.51/19.23 fof(f20740,plain,(
% 48.51/19.23 ![X0,X1]: (ld(rd(X0,X0),mult(X1,rd(X0,X0)))=mult(mult(X1,rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0))))),
% 48.51/19.23 inference(paramodulation,[status(thm)],[f11450,f390])).
% 48.51/19.23 fof(f20777,plain,(
% 48.51/19.23 ![X0,X1]: (mult(rd(X0,X0),mult(X1,rd(X0,X0)))=rd(X1,rd(X0,X0)))),
% 48.51/19.23 inference(paramodulation,[status(thm)],[f11450,f8])).
% 48.51/19.23 fof(f20778,plain,(
% 48.51/19.23 ![X0,X1]: (X0=rd(ld(rd(X1,X1),X0),mult(rd(X1,X1),rd(X1,X1))))),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f10,f20711])).
% 48.51/19.23 fof(f20779,plain,(
% 48.51/19.23 ![X0,X1]: (X0=rd(ld(rd(X1,X1),X0),rd(X1,rd(X1,rd(X1,X1)))))),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f11156,f20778])).
% 48.51/19.23 fof(f20780,plain,(
% 48.51/19.23 ![X0,X1]: (X0=rd(ld(rd(X1,X1),X0),rd(X1,X1)))),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f10890,f20779])).
% 48.51/19.23 fof(f20781,plain,(
% 48.51/19.23 ![X0,X1]: (mult(mult(rd(X0,X0),X1),rd(X0,X0))=rd(ld(rd(rd(X0,X0),rd(X0,X0)),X1),rd(X0,X0)))),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f10800,f20712])).
% 48.51/19.23 fof(f20782,plain,(
% 48.51/19.23 ![X0,X1]: (mult(mult(rd(X0,X0),X1),rd(X0,X0))=rd(ld(rd(X0,X0),X1),rd(X0,X0)))),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f10616,f20781])).
% 48.51/19.23 fof(f20787,plain,(
% 48.51/19.23 ![X0,X1]: (rd(mult(rd(X0,X0),mult(X1,rd(X0,X0))),rd(X0,X0))=X1)),
% 48.51/19.23 inference(backward_demodulation,[status(thm)],[f20789,f11502])).
% 48.51/19.23 fof(f20788,plain,(
% 48.51/19.23 ![X0,X1]: (X0=mult(rd(X1,X1),mult(rd(X1,X1),mult(X0,rd(X1,X1)))))),
% 48.51/19.23 inference(backward_demodulation,[status(thm)],[f20789,f11487])).
% 48.51/19.23 fof(f20789,plain,(
% 48.51/19.23 ![X0,X1]: (mult(mult(rd(X0,X0),X1),rd(X0,X0))=X1)),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f20780,f20782])).
% 48.51/19.23 fof(f20858,plain,(
% 48.51/19.23 ![X0,X1]: (mult(X0,mult(ld(X0,X1),rd(X0,X0)))=mult(mult(X1,rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0))))),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f153,f20740])).
% 48.51/19.23 fof(f20859,plain,(
% 48.51/19.23 ![X0,X1]: (mult(X0,mult(ld(X0,X1),rd(X0,X0)))=mult(mult(X1,rd(X0,X0)),rd(X0,rd(X0,rd(X0,X0)))))),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f11156,f20858])).
% 48.51/19.23 fof(f20860,plain,(
% 48.51/19.23 ![X0,X1]: (mult(X0,mult(ld(X0,X1),rd(X0,X0)))=mult(mult(X1,rd(X0,X0)),rd(X0,X0)))),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f10890,f20859])).
% 48.51/19.23 fof(f20865,plain,(
% 48.51/19.23 ![X0,X1]: (rd(ld(rd(X0,X0),X1),rd(X0,X0))=mult(X1,rd(X0,X0)))),
% 48.51/19.23 inference(backward_demodulation,[status(thm)],[f20872,f14670])).
% 48.51/19.23 fof(f20872,plain,(
% 48.51/19.23 ![X0,X1]: (mult(X0,mult(ld(X0,X1),rd(X0,X0)))=ld(rd(X0,X0),X1))),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f20729,f20860])).
% 48.51/19.23 fof(f20941,plain,(
% 48.51/19.23 ![X0,X1]: (mult(rd(X0,X0),X1)=mult(rd(X0,X0),rd(X1,rd(X0,X0))))),
% 48.51/19.23 inference(backward_demodulation,[status(thm)],[f20951,f11540])).
% 48.51/19.23 fof(f20951,plain,(
% 48.51/19.23 ![X0,X1]: (rd(rd(X0,rd(X1,X1)),rd(X1,X1))=X0)),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f20777,f20787])).
% 48.51/19.23 fof(f20953,plain,(
% 48.51/19.23 ![X0,X1]: (X0=mult(rd(X1,X1),rd(X0,rd(X1,X1))))),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f20777,f20788])).
% 48.51/19.23 fof(f21079,plain,(
% 48.51/19.23 ![X0,X1]: (X0=mult(X0,rd(X1,X1)))),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f20780,f20865])).
% 48.51/19.23 fof(f21242,plain,(
% 48.51/19.23 ![X0,X1]: (mult(rd(X0,X0),X1)=X1)),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f20953,f20941])).
% 48.51/19.23 fof(f22984,plain,(
% 48.51/19.23 ![X0]: (~mult(rd(X0,X0),sK1_skl(rd(X0,X0)))=sK1_skl(rd(X0,X0)))),
% 48.51/19.23 inference(resolution,[status(thm)],[f21079,f16])).
% 48.51/19.23 fof(f23092,plain,(
% 48.51/19.23 ![X0]: (~sK1_skl(rd(X0,X0))=sK1_skl(rd(X0,X0)))),
% 48.51/19.23 inference(forward_demodulation,[status(thm)],[f21242,f22984])).
% 48.51/19.23 fof(f23093,plain,(
% 48.51/19.23 $false),
% 48.51/19.23 inference(trivial_equality_resolution,[status(thm)],[f23092])).
% 48.51/19.23 % SZS output end CNFRefutation for theBenchmark.p
% 7.14/19.30 % Elapsed time: 13.970261 seconds
% 7.14/19.30 % CPU time: 110.357364 seconds
% 7.14/19.30 % Total memory used: 3.362 GB
% 7.14/19.30 % Net memory used: 3.326 GB
%------------------------------------------------------------------------------