%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP660+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 28.59s 4.09s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP660+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n009.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:30:12 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 28.59/4.09 % Refutation found
% 28.59/4.09 % SZS status Theorem for theBenchmark: Theorem is valid
% 28.59/4.09 % SZS output start CNFRefutation for theBenchmark
% 28.59/4.09 fof(f1,axiom,(
% 28.59/4.09 (! [B,A] : mult(A,ld(A,B)) = B )),
% 28.59/4.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.59/4.09 fof(f2,axiom,(
% 28.59/4.09 (! [B,A] : ld(A,mult(A,B)) = B )),
% 28.59/4.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.59/4.09 fof(f3,axiom,(
% 28.59/4.09 (! [B,A] : mult(rd(A,B),B) = A )),
% 28.59/4.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.59/4.09 fof(f4,axiom,(
% 28.59/4.09 (! [B,A] : rd(mult(A,B),B) = A )),
% 28.59/4.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.59/4.09 fof(f5,axiom,(
% 28.59/4.09 (! [C,B,A] : mult(mult(mult(A,B),C),A) = mult(A,mult(B,mult(C,A))) )),
% 28.59/4.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.59/4.09 fof(f6,conjecture,(
% 28.59/4.09 (! [X0,X1] :( mult(X0,rd(X1,X1)) = X0& mult(rd(X1,X1),X0) = X0 ) )),
% 28.59/4.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.59/4.09 fof(f7,negated_conjecture,(
% 28.59/4.09 ~((! [X0,X1] :( mult(X0,rd(X1,X1)) = X0& mult(rd(X1,X1),X0) = X0 ) ))),
% 28.59/4.09 inference(negated_conjecture,[status(cth)],[f6])).
% 28.59/4.09 fof(f8,plain,(
% 28.59/4.09 ![X0,X1]: (mult(X0,ld(X0,X1))=X1)),
% 28.59/4.09 inference(cnf_transformation,[status(thm)],[f1])).
% 28.59/4.09 fof(f9,plain,(
% 28.59/4.09 ![X0,X1]: (ld(X0,mult(X0,X1))=X1)),
% 28.59/4.09 inference(cnf_transformation,[status(thm)],[f2])).
% 28.59/4.09 fof(f10,plain,(
% 28.59/4.09 ![X0,X1]: (mult(rd(X0,X1),X1)=X0)),
% 28.59/4.09 inference(cnf_transformation,[status(thm)],[f3])).
% 28.59/4.09 fof(f11,plain,(
% 28.59/4.09 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 28.59/4.09 inference(cnf_transformation,[status(thm)],[f4])).
% 28.59/4.09 fof(f12,plain,(
% 28.59/4.09 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X2),X0)=mult(X0,mult(X1,mult(X2,X0))))),
% 28.59/4.09 inference(cnf_transformation,[status(thm)],[f5])).
% 28.59/4.09 fof(f13,plain,(
% 28.59/4.09 (?[X0,X1]: (~mult(X0,rd(X1,X1))=X0|~mult(rd(X1,X1),X0)=X0))),
% 28.59/4.09 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 28.59/4.09 fof(f14,plain,(
% 28.59/4.09 (?[X0,X1]: ~mult(X0,rd(X1,X1))=X0)|(?[X0,X1]: ~mult(rd(X1,X1),X0)=X0)),
% 28.59/4.09 inference(miniscoping,[status(thm)],[f13])).
% 28.59/4.09 fof(f15,plain,(
% 28.59/4.09 ~mult(sK0_skl,rd(sK1_skl,sK1_skl))=sK0_skl|~mult(rd(sK3_skl,sK3_skl),sK2_skl)=sK2_skl),
% 28.59/4.09 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])).
% 28.59/4.09 fof(f16,plain,(
% 28.59/4.09 ~mult(sK0_skl,rd(sK1_skl,sK1_skl))=sK0_skl|~mult(rd(sK3_skl,sK3_skl),sK2_skl)=sK2_skl),
% 28.59/4.09 inference(cnf_transformation,[status(thm)],[f15])).
% 28.59/4.09 fof(f19,plain,(
% 28.59/4.09 ![X0,X1]: (ld(rd(X0,X1),X0)=X1)),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f10,f9])).
% 28.59/4.09 fof(f21,plain,(
% 28.59/4.09 ![X0,X1]: (rd(X0,ld(X1,X0))=X1)),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f8,f11])).
% 28.59/4.09 fof(f24,plain,(
% 28.59/4.09 ![X0,X1,X2]: (mult(X0,X1)=mult(X1,mult(X2,mult(ld(mult(X1,X2),X0),X1))))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f8,f12])).
% 28.59/4.09 fof(f26,plain,(
% 28.59/4.09 ![X0,X1,X2]: (mult(mult(X0,X1),rd(X0,X2))=mult(rd(X0,X2),mult(X2,mult(X1,rd(X0,X2)))))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f10,f12])).
% 28.59/4.09 fof(f27,plain,(
% 28.59/4.09 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(X2,mult(ld(X2,X0),mult(X1,X2))))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f8,f12])).
% 28.59/4.09 fof(f28,plain,(
% 28.59/4.09 ![X0,X1,X2]: (rd(mult(X0,mult(X1,mult(X2,X0))),X0)=mult(mult(X0,X1),X2))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f12,f11])).
% 28.59/4.09 fof(f44,plain,(
% 28.59/4.09 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(X2,mult(ld(mult(X0,X2),X1),X0)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f24,f9])).
% 28.59/4.09 fof(f55,plain,(
% 28.59/4.09 ![X0,X1,X2]: (mult(mult(X0,rd(X1,X2)),X2)=mult(X2,mult(ld(X2,X0),X1)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f10,f27])).
% 28.59/4.09 fof(f61,plain,(
% 28.59/4.09 ![X0,X1,X2]: (ld(X0,mult(mult(X1,X2),X0))=mult(ld(X0,X1),mult(X2,X0)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f27,f9])).
% 28.59/4.09 fof(f64,plain,(
% 28.59/4.09 ![X0,X1,X2]: (rd(mult(X0,X1),X0)=mult(mult(X0,rd(X1,mult(X2,X0))),X2))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f10,f28])).
% 28.59/4.09 fof(f65,plain,(
% 28.59/4.09 ![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)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f27,f28])).
% 28.59/4.09 fof(f67,plain,(
% 28.59/4.09 ![X0,X1,X2]: (rd(mult(X0,mult(X1,X2)),X0)=mult(mult(X0,X1),rd(X2,X0)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f10,f28])).
% 28.59/4.09 fof(f69,plain,(
% 28.59/4.09 ![X0,X1,X2]: (rd(mult(ld(X0,X1),mult(X2,X1)),ld(X0,X1))=mult(mult(ld(X0,X1),X2),X0))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f8,f28])).
% 28.59/4.09 fof(f106,plain,(
% 28.59/4.09 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(ld(X0,X2),mult(ld(X2,X1),X0)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f8,f44])).
% 28.59/4.09 fof(f120,plain,(
% 28.59/4.09 ![X0,X1,X2]: (ld(X0,ld(X1,mult(X2,X1)))=mult(ld(mult(X1,X0),X2),X1))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f44,f9])).
% 28.59/4.09 fof(f151,plain,(
% 28.59/4.09 ![X0,X1,X2]: (rd(mult(X0,mult(ld(X0,X1),X2)),X0)=mult(X1,rd(X2,X0)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f55,f11])).
% 28.59/4.09 fof(f264,plain,(
% 28.59/4.09 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(ld(X0,rd(X1,X2)),mult(X2,X0)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f10,f61])).
% 28.59/4.09 fof(f325,plain,(
% 28.59/4.09 ![X0,X1,X2]: (rd(rd(mult(X0,X1),X0),X2)=mult(X0,rd(X1,mult(X2,X0))))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f64,f11])).
% 28.59/4.09 fof(f615,plain,(
% 28.59/4.09 ![X0,X1]: (ld(X0,X1)=mult(ld(mult(X1,X0),X1),X1))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f9,f120])).
% 28.59/4.09 fof(f622,plain,(
% 28.59/4.09 ![X0,X1,X2]: (ld(X0,ld(X1,X2))=mult(ld(mult(X1,X0),rd(X2,X1)),X1))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f10,f120])).
% 28.59/4.09 fof(f651,plain,(
% 28.59/4.09 ![X0,X1]: (ld(X0,rd(X1,X0))=mult(ld(X1,rd(X1,X0)),rd(X1,X0)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f10,f615])).
% 28.59/4.09 fof(f654,plain,(
% 28.59/4.09 ![X0,X1]: (ld(ld(X0,X1),X0)=mult(ld(X1,X0),X0))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f8,f615])).
% 28.59/4.09 fof(f677,plain,(
% 28.59/4.09 ![X0,X1]: (rd(ld(X0,X1),X1)=ld(mult(X1,X0),X1))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f615,f11])).
% 28.59/4.09 fof(f743,plain,(
% 28.59/4.09 ![X0,X1]: (rd(X0,mult(ld(X1,X0),X0))=ld(X0,X1))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f654,f21])).
% 28.59/4.09 fof(f840,plain,(
% 28.59/4.09 ![X0,X1]: (rd(ld(X0,rd(X1,X0)),rd(X1,X0))=ld(X1,rd(X1,X0)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f10,f677])).
% 28.59/4.09 fof(f851,plain,(
% 28.59/4.09 ![X0,X1]: (rd(X0,rd(ld(X1,X0),X0))=mult(X0,X1))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f677,f21])).
% 28.59/4.09 fof(f872,plain,(
% 28.59/4.09 ![X0,X1]: (rd(X0,mult(X1,X0))=ld(X0,rd(X0,X1)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f19,f743])).
% 28.59/4.09 fof(f885,plain,(
% 28.59/4.09 ![X0,X1]: (rd(ld(X0,rd(X1,X0)),rd(X1,X0))=rd(X1,mult(X0,X1)))),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f872,f840])).
% 28.59/4.09 fof(f886,plain,(
% 28.59/4.09 ![X0,X1]: (ld(X0,rd(X1,X0))=mult(rd(X1,mult(X0,X1)),rd(X1,X0)))),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f872,f651])).
% 28.59/4.09 fof(f898,plain,(
% 28.59/4.09 ![X0,X1]: (rd(X0,rd(X1,X0))=mult(X0,rd(X0,X1)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f19,f851])).
% 28.59/4.09 fof(f901,plain,(
% 28.59/4.09 ![X0,X1]: (rd(mult(X0,X1),rd(X1,mult(X0,X1)))=mult(mult(X0,X1),X0))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f9,f851])).
% 28.59/4.09 fof(f930,plain,(
% 28.59/4.09 ![X0,X1]: (rd(rd(X0,X1),rd(X0,mult(X1,X0)))=X0)),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f872,f21])).
% 28.59/4.09 fof(f1072,plain,(
% 28.59/4.09 ![X0,X1]: (rd(rd(X0,rd(X1,X0)),rd(X0,X1))=X0)),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f898,f11])).
% 28.59/4.09 fof(f1813,plain,(
% 28.59/4.09 ![X0,X1,X2]: (ld(ld(X0,X1),mult(X2,ld(X0,X1)))=mult(ld(ld(X0,X1),rd(X2,X0)),X1))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f8,f264])).
% 28.59/4.09 fof(f1847,plain,(
% 28.59/4.09 ![X0,X1,X2]: (rd(ld(X0,mult(X1,X0)),mult(X2,X0))=ld(X0,rd(X1,X2)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f264,f11])).
% 28.59/4.09 fof(f1937,plain,(
% 28.59/4.09 ![X0,X1,X2]: (rd(rd(mult(X0,X1),X0),rd(X2,X0))=mult(X0,rd(X1,X2)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f10,f325])).
% 28.59/4.09 fof(f1943,plain,(
% 28.59/4.09 ![X0,X1,X2]: (rd(rd(mult(ld(X0,X1),X2),ld(X0,X1)),X0)=mult(ld(X0,X1),rd(X2,X1)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f8,f325])).
% 28.59/4.09 fof(f2444,plain,(
% 28.59/4.09 ![X0,X1]: (ld(X0,ld(X1,mult(X1,X0)))=mult(rd(mult(X1,X0),mult(X1,mult(X1,X0))),X1))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f872,f622])).
% 28.59/4.09 fof(f2462,plain,(
% 28.59/4.09 ![X0,X1,X2]: (ld(ld(X0,X1),ld(X0,X2))=mult(ld(X1,rd(X2,X0)),X0))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f8,f622])).
% 28.59/4.09 fof(f2509,plain,(
% 28.59/4.09 ![X0,X1]: (ld(X0,X0)=mult(rd(mult(X1,X0),mult(X1,mult(X1,X0))),X1))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f9,f2444])).
% 28.59/4.09 fof(f3849,plain,(
% 28.59/4.09 ![X0,X1]: (rd(mult(ld(X0,X1),X1),ld(X1,X0))=mult(mult(ld(X0,X1),X1),ld(X0,X1)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f743,f901])).
% 28.59/4.09 fof(f5600,plain,(
% 28.59/4.09 ![X0]: (ld(X0,X0)=mult(rd(mult(ld(X0,X0),X0),ld(X0,mult(X0,X0))),ld(X0,X0)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f106,f2509])).
% 28.59/4.09 fof(f5679,plain,(
% 28.59/4.09 ![X0,X1]: (rd(ld(X0,X0),X1)=rd(mult(X1,X0),mult(X1,mult(X1,X0))))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f2509,f11])).
% 28.59/4.09 fof(f5717,plain,(
% 28.59/4.09 ![X0]: (ld(X0,X0)=mult(rd(mult(ld(X0,X0),X0),X0),ld(X0,X0)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f9,f5600])).
% 28.59/4.09 fof(f5718,plain,(
% 28.59/4.09 ![X0]: (ld(X0,X0)=mult(ld(X0,X0),ld(X0,X0)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f11,f5717])).
% 28.59/4.09 fof(f6346,plain,(
% 28.59/4.09 ![X0]: (ld(ld(X0,X0),mult(X0,ld(X0,X0)))=mult(ld(ld(X0,X0),X0),ld(X0,X0)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f5718,f106])).
% 28.59/4.09 fof(f6353,plain,(
% 28.59/4.09 ![X0,X1]: (rd(ld(ld(X0,X0),mult(X1,ld(X0,X0))),ld(X0,X0))=ld(ld(X0,X0),rd(X1,ld(X0,X0))))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f5718,f1847])).
% 28.59/4.09 fof(f6356,plain,(
% 28.59/4.09 ![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)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f5718,f65])).
% 28.59/4.09 fof(f6387,plain,(
% 28.59/4.09 ![X0,X1]: (ld(ld(X0,X0),mult(X1,ld(X0,X0)))=mult(ld(X0,X0),mult(ld(ld(X0,X0),X1),ld(X0,X0))))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f5718,f44])).
% 28.59/4.09 fof(f6390,plain,(
% 28.59/4.09 ![X0,X1]: (rd(mult(ld(X0,X0),mult(X1,ld(X0,X0))),ld(X0,X0))=mult(mult(ld(X0,X0),X1),ld(X0,X0)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f5718,f28])).
% 28.59/4.09 fof(f6391,plain,(
% 28.59/4.09 ![X0,X1]: (mult(mult(X0,ld(X1,X1)),ld(X1,X1))=mult(ld(X1,X1),mult(ld(ld(X1,X1),X0),ld(X1,X1))))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f5718,f27])).
% 28.59/4.09 fof(f6393,plain,(
% 28.59/4.09 ![X0]: (rd(ld(X0,X0),ld(X0,X0))=ld(X0,X0))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f5718,f11])).
% 28.59/4.09 fof(f6394,plain,(
% 28.59/4.09 ![X0]: (ld(ld(X0,X0),ld(X0,X0))=ld(X0,X0))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f5718,f9])).
% 28.59/4.09 fof(f6416,plain,(
% 28.59/4.09 ![X0]: (mult(ld(ld(X0,X0),rd(X0,X0)),X0)=mult(ld(ld(X0,X0),X0),ld(X0,X0)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f1813,f6346])).
% 28.59/4.09 fof(f6417,plain,(
% 28.59/4.09 ![X0]: (mult(ld(ld(X0,X0),rd(X0,X0)),X0)=mult(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f654,f6416])).
% 28.59/4.09 fof(f6418,plain,(
% 28.59/4.09 ![X0]: (mult(ld(ld(X0,X0),rd(X0,X0)),X0)=rd(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f3849,f6417])).
% 28.59/4.09 fof(f6424,plain,(
% 28.59/4.09 ![X0,X1]: (rd(mult(ld(ld(X0,X0),rd(X1,X0)),X0),ld(X0,X0))=ld(ld(X0,X0),rd(X1,ld(X0,X0))))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f1813,f6353])).
% 28.59/4.09 fof(f6428,plain,(
% 28.59/4.09 ![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)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f5718,f6356])).
% 28.59/4.09 fof(f6429,plain,(
% 28.59/4.09 ![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)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f5718,f6428])).
% 28.59/4.09 fof(f6430,plain,(
% 28.59/4.09 ![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)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f5718,f6429])).
% 28.59/4.09 fof(f6431,plain,(
% 28.59/4.09 ![X0,X1]: (rd(mult(ld(X0,X0),mult(mult(X1,ld(X0,X0)),ld(X0,X0))),ld(X0,X0))=X1)),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f8,f6430])).
% 28.59/4.09 fof(f6495,plain,(
% 28.59/4.09 ![X0,X1]: (mult(ld(ld(X0,X0),rd(X1,X0)),X0)=mult(ld(X0,X0),mult(ld(ld(X0,X0),X1),ld(X0,X0))))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f1813,f6387])).
% 28.59/4.09 fof(f6496,plain,(
% 28.59/4.09 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,ld(X0,X0))),ld(X0,X0))=X1)),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f6390,f6431])).
% 28.59/4.09 fof(f6497,plain,(
% 28.59/4.09 ![X0,X1]: (mult(ld(ld(X0,X0),rd(X1,X0)),X0)=mult(mult(X1,ld(X0,X0)),ld(X0,X0)))),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f6391,f6495])).
% 28.59/4.09 fof(f6507,plain,(
% 28.59/4.09 ![X0]: (mult(ld(X0,rd(X0,X0)),X0)=ld(X0,X0))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f2462,f6394])).
% 28.59/4.09 fof(f6508,plain,(
% 28.59/4.09 ![X0]: (mult(rd(X0,mult(X0,X0)),X0)=ld(X0,X0))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f872,f6507])).
% 28.59/4.09 fof(f6518,plain,(
% 28.59/4.09 ![X0,X1]: (rd(mult(mult(X0,ld(X1,X1)),ld(X1,X1)),ld(X1,X1))=ld(ld(X1,X1),rd(X0,ld(X1,X1))))),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f6497,f6424])).
% 28.59/4.09 fof(f6519,plain,(
% 28.59/4.09 ![X0]: (mult(mult(X0,ld(X0,X0)),ld(X0,X0))=rd(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f6497,f6418])).
% 28.59/4.09 fof(f6523,plain,(
% 28.59/4.09 ![X0,X1]: (mult(X0,ld(X1,X1))=ld(ld(X1,X1),rd(X0,ld(X1,X1))))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f11,f6518])).
% 28.59/4.09 fof(f6524,plain,(
% 28.59/4.09 ![X0]: (mult(X0,ld(X0,X0))=rd(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f8,f6519])).
% 28.59/4.09 fof(f6525,plain,(
% 28.59/4.09 ![X0]: (X0=rd(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f8,f6524])).
% 28.59/4.09 fof(f6703,plain,(
% 28.59/4.09 ![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)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f6508,f1937])).
% 28.59/4.09 fof(f6707,plain,(
% 28.59/4.09 ![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)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f6508,f65])).
% 28.59/4.09 fof(f6742,plain,(
% 28.59/4.09 ![X0,X1]: (mult(mult(X0,rd(X1,mult(X1,X1))),X1)=mult(X1,mult(ld(X1,X0),ld(X1,X1))))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f6508,f27])).
% 28.59/4.09 fof(f6744,plain,(
% 28.59/4.09 ![X0]: (rd(ld(X0,X0),X0)=rd(X0,mult(X0,X0)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f6508,f11])).
% 28.59/4.09 fof(f6763,plain,(
% 28.59/4.09 ![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)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f6508,f6707])).
% 28.59/4.09 fof(f6764,plain,(
% 28.59/4.09 ![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)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f69,f6763])).
% 28.59/4.09 fof(f6765,plain,(
% 28.59/4.09 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)=mult(mult(ld(X0,X0),X0),ld(X0,X1)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f6508,f6764])).
% 28.59/4.09 fof(f7011,plain,(
% 28.59/4.09 ![X0,X1]: (rd(X0,rd(X1,ld(X0,X0)))=mult(ld(X0,X0),rd(X0,X1)))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f6525,f1937])).
% 28.59/4.09 fof(f7015,plain,(
% 28.59/4.09 ![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))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f6525,f886])).
% 28.59/4.09 fof(f7016,plain,(
% 28.59/4.09 ![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))))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f6525,f885])).
% 28.59/4.09 fof(f7021,plain,(
% 28.59/4.09 ![X0]: (rd(rd(ld(X0,X0),X0),rd(ld(X0,X0),mult(ld(X0,X0),X0)))=ld(X0,X0))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f6525,f1072])).
% 28.59/4.09 fof(f7051,plain,(
% 28.59/4.09 ![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))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f6523,f7015])).
% 28.59/4.09 fof(f7052,plain,(
% 28.59/4.09 ![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))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f3849,f7051])).
% 28.59/4.09 fof(f7053,plain,(
% 28.59/4.09 ![X0]: (X0=mult(rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))),X0))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f6525,f7052])).
% 28.59/4.09 fof(f7054,plain,(
% 28.59/4.09 ![X0]: (X0=mult(rd(ld(X0,X0),ld(X0,X0)),X0))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f5679,f7053])).
% 28.59/4.09 fof(f7058,plain,(
% 28.59/4.09 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)=mult(X0,ld(X0,X1)))),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f7059,f6765])).
% 28.59/4.09 fof(f7059,plain,(
% 28.59/4.09 ![X0]: (X0=mult(ld(X0,X0),X0))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f6393,f7054])).
% 28.59/4.09 fof(f7060,plain,(
% 28.59/4.09 ![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))))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f6523,f7016])).
% 28.59/4.09 fof(f7061,plain,(
% 28.59/4.09 ![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))))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f3849,f7060])).
% 28.59/4.09 fof(f7062,plain,(
% 28.59/4.09 ![X0]: (mult(ld(X0,X0),rd(X0,X0))=rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f1943,f7061])).
% 28.59/4.09 fof(f7063,plain,(
% 28.59/4.09 ![X0]: (rd(X0,rd(X0,ld(X0,X0)))=rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f7011,f7062])).
% 28.59/4.09 fof(f7064,plain,(
% 28.59/4.09 ![X0]: (rd(X0,X0)=rd(mult(ld(X0,X0),X0),mult(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f21,f7063])).
% 28.59/4.09 fof(f7065,plain,(
% 28.59/4.09 ![X0]: (rd(X0,X0)=ld(X0,X0))),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f7066,f6393])).
% 28.59/4.09 fof(f7066,plain,(
% 28.59/4.09 ![X0]: (rd(X0,X0)=rd(ld(X0,X0),ld(X0,X0)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f5679,f7064])).
% 28.59/4.09 fof(f7079,plain,(
% 28.59/4.09 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(ld(X0,X0),mult(ld(X0,X0),X0)))=ld(X0,X0))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f6744,f7021])).
% 28.59/4.09 fof(f7080,plain,(
% 28.59/4.09 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(ld(X0,X0),X0))=ld(X0,X0))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f7059,f7079])).
% 28.59/4.09 fof(f7081,plain,(
% 28.59/4.09 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))=ld(X0,X0))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f6744,f7080])).
% 28.59/4.09 fof(f7101,plain,(
% 28.59/4.09 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)=X1)),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f8,f7058])).
% 28.59/4.09 fof(f7141,plain,(
% 28.59/4.09 ![X0,X1]: (mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)=X1)),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f7065,f7101])).
% 28.59/4.09 fof(f7143,plain,(
% 28.59/4.09 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))=rd(X0,X0))),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f7065,f7081])).
% 28.59/4.09 fof(f7157,plain,(
% 28.59/4.09 ![X0,X1]: (mult(mult(X0,rd(X1,mult(X1,X1))),X1)=mult(X1,mult(ld(X1,X0),rd(X1,X1))))),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f7065,f6742])).
% 28.59/4.09 fof(f7168,plain,(
% 28.59/4.09 ![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)))),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f7065,f6703])).
% 28.59/4.09 fof(f7172,plain,(
% 28.59/4.09 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,ld(X0,X0))),rd(X0,X0))=X1)),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f7065,f6496])).
% 28.59/4.09 fof(f7220,plain,(
% 28.59/4.09 ![X0,X1]: (rd(X0,rd(X1,rd(X0,mult(X0,X0))))=mult(rd(X0,mult(X0,X0)),rd(X0,X1)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f930,f7168])).
% 28.59/4.09 fof(f7226,plain,(
% 28.59/4.09 ![X0,X1]: (mult(mult(rd(X0,X0),mult(X1,ld(X0,X0))),rd(X0,X0))=X1)),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f7065,f7172])).
% 28.59/4.09 fof(f7227,plain,(
% 28.59/4.09 ![X0,X1]: (mult(mult(rd(X0,X0),mult(X1,rd(X0,X0))),rd(X0,X0))=X1)),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f7065,f7226])).
% 28.59/4.09 fof(f11272,plain,(
% 28.59/4.09 ![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)))))))),
% 28.59/4.09 inference(paramodulation,[status(thm)],[f7141,f7141])).
% 28.59/4.09 fof(f11396,plain,(
% 28.59/4.09 ![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)))))))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f7143,f11272])).
% 28.59/4.09 fof(f11397,plain,(
% 28.59/4.09 ![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))))))))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f7220,f11396])).
% 28.59/4.09 fof(f11398,plain,(
% 28.59/4.09 ![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))))))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f901,f11397])).
% 28.59/4.09 fof(f11399,plain,(
% 28.59/4.09 ![X0,X1]: (mult(rd(X0,X0),mult(mult(X1,rd(X0,mult(X0,X0))),X0))=X1)),
% 28.59/4.09 inference(backward_demodulation,[status(thm)],[f11403,f7141])).
% 28.59/4.09 fof(f11403,plain,(
% 28.59/4.09 ![X0,X1]: (mult(mult(rd(X0,X0),X1),X0)=mult(rd(X0,X0),mult(X1,X0)))),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f930,f11398])).
% 28.59/4.09 fof(f11614,plain,(
% 28.59/4.09 ![X0,X1]: (mult(rd(X0,X0),mult(X0,mult(ld(X0,X1),rd(X0,X0))))=X1)),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f7157,f11399])).
% 28.59/4.09 fof(f11615,plain,(
% 28.59/4.09 ![X0,X1]: (mult(mult(X0,ld(X0,X1)),rd(X0,X0))=X1)),
% 28.59/4.09 inference(forward_demodulation,[status(thm)],[f26,f11614])).
% 25.84/4.15 fof(f11616,plain,(
% 25.84/4.15 ![X0,X1]: (rd(mult(X0,mult(ld(X0,X1),X0)),X0)=X1)),
% 25.84/4.15 inference(forward_demodulation,[status(thm)],[f67,f11615])).
% 25.84/4.15 fof(f11617,plain,(
% 25.84/4.15 ~sK0_skl=sK0_skl|~mult(rd(sK3_skl,sK3_skl),sK2_skl)=sK2_skl),
% 25.84/4.15 inference(backward_demodulation,[status(thm)],[f11658,f16])).
% 25.84/4.15 fof(f11639,plain,(
% 25.84/4.15 ![X0,X1]: (mult(rd(X0,X0),mult(X1,rd(X0,X0)))=X1)),
% 25.84/4.15 inference(backward_demodulation,[status(thm)],[f11658,f7227])).
% 25.84/4.15 fof(f11658,plain,(
% 25.84/4.15 ![X0,X1]: (mult(X0,rd(X1,X1))=X0)),
% 25.84/4.15 inference(forward_demodulation,[status(thm)],[f151,f11616])).
% 25.84/4.15 fof(f11746,plain,(
% 25.84/4.15 ~mult(rd(sK3_skl,sK3_skl),sK2_skl)=sK2_skl),
% 25.84/4.15 inference(trivial_equality_resolution,[status(thm)],[f11617])).
% 25.84/4.15 fof(f11850,plain,(
% 25.84/4.15 ~sK2_skl=sK2_skl),
% 25.84/4.15 inference(backward_demodulation,[status(thm)],[f11867,f11746])).
% 25.84/4.15 fof(f11867,plain,(
% 25.84/4.15 ![X0,X1]: (mult(rd(X0,X0),X1)=X1)),
% 25.84/4.15 inference(forward_demodulation,[status(thm)],[f11658,f11639])).
% 25.84/4.15 fof(f12385,plain,(
% 25.84/4.15 $false),
% 25.84/4.15 inference(trivial_equality_resolution,[status(thm)],[f11850])).
% 25.84/4.15 % SZS output end CNFRefutation for theBenchmark.p
% 25.84/4.17 % Elapsed time: 3.793954 seconds
% 25.84/4.17 % CPU time: 29.737063 seconds
% 25.84/4.17 % Total memory used: 619.888 MB
% 25.84/4.17 % Net memory used: 612.940 MB
%------------------------------------------------------------------------------