%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP660-12 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:37:06 PM UTC 2026
% Result : Unsatisfiable 67.38s 8.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP660-12 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n002.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:32:32 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 67.38/8.94 % Refutation found
% 67.38/8.94 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 67.38/8.94 % SZS output start CNFRefutation for theBenchmark
% 67.38/8.94 fof(f1,axiom,(
% 67.38/8.94 (![A,B]: (mult(A,ld(A,B)) = B ))),
% 67.38/8.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 67.38/8.94 fof(f2,axiom,(
% 67.38/8.94 (![A,B]: (ld(A,mult(A,B)) = B ))),
% 67.38/8.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 67.38/8.94 fof(f3,axiom,(
% 67.38/8.94 (![A,B]: (mult(rd(A,B),B) = A ))),
% 67.38/8.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 67.38/8.94 fof(f4,axiom,(
% 67.38/8.94 (![A,B]: (rd(mult(A,B),B) = A ))),
% 67.38/8.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 67.38/8.94 fof(f5,axiom,(
% 67.38/8.94 (![A,B,C]: (mult(mult(mult(A,B),C),A) = mult(A,mult(B,mult(C,A))) ))),
% 67.38/8.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 67.38/8.94 fof(f6,negated_conjecture,(
% 67.38/8.94 mult(rd(x1,x1),x0) != x0 ),
% 67.38/8.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 67.38/8.94 fof(f7,plain,(
% 67.38/8.94 ![X0,X1]: (mult(X0,ld(X0,X1))=X1)),
% 67.38/8.94 inference(cnf_transformation,[status(thm)],[f1])).
% 67.38/8.94 fof(f8,plain,(
% 67.38/8.94 ![X0,X1]: (ld(X0,mult(X0,X1))=X1)),
% 67.38/8.94 inference(cnf_transformation,[status(thm)],[f2])).
% 67.38/8.94 fof(f9,plain,(
% 67.38/8.94 ![X0,X1]: (mult(rd(X0,X1),X1)=X0)),
% 67.38/8.94 inference(cnf_transformation,[status(thm)],[f3])).
% 67.38/8.94 fof(f10,plain,(
% 67.38/8.94 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 67.38/8.94 inference(cnf_transformation,[status(thm)],[f4])).
% 67.38/8.94 fof(f11,plain,(
% 67.38/8.94 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X2),X0)=mult(X0,mult(X1,mult(X2,X0))))),
% 67.38/8.94 inference(cnf_transformation,[status(thm)],[f5])).
% 67.38/8.94 fof(f12,plain,(
% 67.38/8.94 ~mult(rd(x1,x1),x0)=x0),
% 67.38/8.94 inference(cnf_transformation,[status(thm)],[f6])).
% 67.38/8.94 fof(f18,plain,(
% 67.38/8.94 ![X0,X1]: (ld(rd(X0,X1),X0)=X1)),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f9,f8])).
% 67.38/8.94 fof(f20,plain,(
% 67.38/8.94 ![X0,X1]: (rd(X0,ld(X1,X0))=X1)),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f7,f10])).
% 67.38/8.94 fof(f29,plain,(
% 67.38/8.94 ![X0,X1,X2]: (mult(X0,X1)=mult(X1,mult(X2,mult(ld(mult(X1,X2),X0),X1))))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f7,f11])).
% 67.38/8.94 fof(f31,plain,(
% 67.38/8.94 ![X0,X1,X2]: (mult(mult(X0,X1),rd(X0,X2))=mult(rd(X0,X2),mult(X2,mult(X1,rd(X0,X2)))))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f9,f11])).
% 67.38/8.94 fof(f32,plain,(
% 67.38/8.94 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(X2,mult(ld(X2,X0),mult(X1,X2))))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f7,f11])).
% 67.38/8.94 fof(f33,plain,(
% 67.38/8.94 ![X0,X1,X2]: (rd(mult(X0,mult(X1,mult(X2,X0))),X0)=mult(mult(X0,X1),X2))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f11,f10])).
% 67.38/8.94 fof(f34,plain,(
% 67.38/8.94 ![X0,X1,X2]: (ld(mult(mult(X0,X1),X2),mult(X0,mult(X1,mult(X2,X0))))=X0)),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f11,f8])).
% 67.38/8.94 fof(f43,plain,(
% 67.38/8.94 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(X2,mult(ld(mult(X0,X2),X1),X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f29,f8])).
% 67.38/8.94 fof(f54,plain,(
% 67.38/8.94 ![X0,X1,X2]: (mult(mult(X0,rd(X1,X2)),X2)=mult(X2,mult(ld(X2,X0),X1)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f9,f32])).
% 67.38/8.94 fof(f60,plain,(
% 67.38/8.94 ![X0,X1,X2]: (ld(X0,mult(mult(X1,X2),X0))=mult(ld(X0,X1),mult(X2,X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f32,f8])).
% 67.38/8.94 fof(f63,plain,(
% 67.38/8.94 ![X0,X1,X2]: (rd(mult(X0,X1),X0)=mult(mult(X0,rd(X1,mult(X2,X0))),X2))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f9,f33])).
% 67.38/8.94 fof(f64,plain,(
% 67.38/8.94 ![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)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f32,f33])).
% 67.38/8.94 fof(f66,plain,(
% 67.38/8.94 ![X0,X1,X2]: (rd(mult(X0,mult(X1,X2)),X0)=mult(mult(X0,X1),rd(X2,X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f9,f33])).
% 67.38/8.94 fof(f73,plain,(
% 67.38/8.94 ![X0,X1,X2]: (mult(mult(mult(X0,X1),mult(X2,X0)),rd(X1,mult(X0,X1)))=mult(mult(mult(X0,X1),X1),ld(X1,X2)))),
% 67.38/8.94 inference(backward_demodulation,[status(thm)],[f66,f64])).
% 67.38/8.94 fof(f81,plain,(
% 67.38/8.94 ![X0,X1,X2,X3]: (ld(mult(mult(X0,mult(X1,mult(X2,X0))),X3),mult(mult(mult(X0,X1),X2),mult(X0,mult(X3,mult(mult(X0,X1),X2)))))=mult(mult(X0,X1),X2))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f11,f34])).
% 67.38/8.94 fof(f88,plain,(
% 67.38/8.94 ![X0,X1,X2]: (ld(mult(mult(mult(X0,X1),X1),ld(X1,X2)),mult(mult(X0,X1),mult(mult(X2,X0),X1)))=mult(X0,X1))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f32,f34])).
% 67.38/8.94 fof(f90,plain,(
% 67.38/8.94 ![X0,X1,X2]: (ld(mult(mult(X0,X1),rd(X2,X0)),mult(X0,mult(X1,X2)))=X0)),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f9,f34])).
% 67.38/8.94 fof(f111,plain,(
% 67.38/8.94 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(ld(X0,X2),mult(ld(X2,X1),X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f7,f43])).
% 67.38/8.94 fof(f122,plain,(
% 67.38/8.94 ![X0,X1,X2]: (ld(X0,ld(X1,mult(X2,X1)))=mult(ld(mult(X1,X0),X2),X1))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f43,f8])).
% 67.38/8.94 fof(f259,plain,(
% 67.38/8.94 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(ld(X0,rd(X1,X2)),mult(X2,X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f9,f60])).
% 67.38/8.94 fof(f295,plain,(
% 67.38/8.94 ![X0,X1,X2]: (rd(mult(X0,X1),X0)=mult(mult(X0,rd(X1,X2)),rd(X2,X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f9,f63])).
% 67.38/8.94 fof(f298,plain,(
% 67.38/8.94 ![X0,X1,X2]: (rd(mult(ld(X0,X1),X2),ld(X0,X1))=mult(mult(ld(X0,X1),rd(X2,X1)),X0))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f7,f63])).
% 67.38/8.94 fof(f317,plain,(
% 67.38/8.94 ![X0,X1,X2]: (rd(rd(mult(X0,X1),X0),X2)=mult(X0,rd(X1,mult(X2,X0))))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f63,f10])).
% 67.38/8.94 fof(f331,plain,(
% 67.38/8.94 ![X0,X1]: (mult(X0,X1)=mult(mult(mult(X0,X1),X0),rd(X1,mult(X0,X1))))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f10,f66])).
% 67.38/8.94 fof(f346,plain,(
% 67.38/8.94 ![X0,X1,X2]: (rd(mult(X0,X1),X0)=mult(mult(X0,X2),rd(ld(X2,X1),X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f7,f66])).
% 67.38/8.94 fof(f630,plain,(
% 67.38/8.94 ![X0,X1]: (ld(X0,X1)=mult(ld(mult(X1,X0),X1),X1))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f8,f122])).
% 67.38/8.94 fof(f637,plain,(
% 67.38/8.94 ![X0,X1,X2]: (ld(X0,ld(X1,X2))=mult(ld(mult(X1,X0),rd(X2,X1)),X1))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f9,f122])).
% 67.38/8.94 fof(f665,plain,(
% 67.38/8.94 ![X0,X1]: (ld(X0,rd(X1,X0))=mult(ld(X1,rd(X1,X0)),rd(X1,X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f9,f630])).
% 67.38/8.94 fof(f668,plain,(
% 67.38/8.94 ![X0,X1]: (ld(ld(X0,X1),X0)=mult(ld(X1,X0),X0))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f7,f630])).
% 67.38/8.94 fof(f694,plain,(
% 67.38/8.94 ![X0,X1]: (rd(ld(X0,X1),X1)=ld(mult(X1,X0),X1))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f630,f10])).
% 67.38/8.94 fof(f766,plain,(
% 67.38/8.94 ![X0,X1]: (rd(X0,mult(ld(X1,X0),X0))=ld(X0,X1))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f668,f20])).
% 67.38/8.94 fof(f781,plain,(
% 67.38/8.94 ![X0,X1]: (rd(ld(X0,rd(X1,X0)),rd(X1,X0))=ld(X1,rd(X1,X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f9,f694])).
% 67.38/8.94 fof(f792,plain,(
% 67.38/8.94 ![X0,X1]: (rd(X0,rd(ld(X1,X0),X0))=mult(X0,X1))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f694,f20])).
% 67.38/8.94 fof(f807,plain,(
% 67.38/8.94 ![X0,X1]: (rd(X0,mult(mult(ld(X1,X0),X0),X0))=ld(X0,ld(X0,X1)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f668,f766])).
% 67.38/8.94 fof(f811,plain,(
% 67.38/8.94 ![X0,X1]: (rd(X0,mult(X1,X0))=ld(X0,rd(X0,X1)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f18,f766])).
% 67.38/8.94 fof(f814,plain,(
% 67.38/8.94 ![X0,X1]: (rd(mult(X0,X1),mult(X1,mult(X0,X1)))=ld(mult(X0,X1),X0))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f8,f766])).
% 67.38/8.94 fof(f824,plain,(
% 67.38/8.94 ![X0,X1]: (rd(ld(X0,rd(X1,X0)),rd(X1,X0))=rd(X1,mult(X0,X1)))),
% 67.38/8.94 inference(backward_demodulation,[status(thm)],[f811,f781])).
% 67.38/8.94 fof(f825,plain,(
% 67.38/8.94 ![X0,X1]: (ld(X0,rd(X1,X0))=mult(rd(X1,mult(X0,X1)),rd(X1,X0)))),
% 67.38/8.94 inference(backward_demodulation,[status(thm)],[f811,f665])).
% 67.38/8.94 fof(f826,plain,(
% 67.38/8.94 ![X0,X1]: (rd(mult(X0,X1),mult(X1,mult(X0,X1)))=rd(ld(X1,X0),X0))),
% 67.38/8.94 inference(forward_demodulation,[status(thm)],[f694,f814])).
% 67.38/8.94 fof(f931,plain,(
% 67.38/8.94 ![X0,X1]: (rd(X0,rd(X1,X0))=mult(X0,rd(X0,X1)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f18,f792])).
% 67.38/8.94 fof(f968,plain,(
% 67.38/8.94 ![X0,X1]: (rd(rd(X0,X1),rd(X0,mult(X1,X0)))=X0)),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f811,f20])).
% 67.38/8.94 fof(f969,plain,(
% 67.38/8.94 ![X0,X1]: (mult(X0,rd(X0,mult(X1,X0)))=rd(X0,X1))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f811,f7])).
% 67.38/8.94 fof(f977,plain,(
% 67.38/8.94 ![X0,X1]: (rd(rd(X0,X1),mult(X1,rd(X1,X0)))=mult(rd(X0,X1),rd(rd(X0,X1),X1)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f931,f931])).
% 67.38/8.94 fof(f979,plain,(
% 67.38/8.94 ![X0,X1]: (rd(ld(X0,X1),X0)=mult(ld(X0,X1),rd(ld(X0,X1),X1)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f20,f931])).
% 67.38/8.94 fof(f1013,plain,(
% 67.38/8.94 ![X0,X1]: (rd(rd(ld(X0,X1),X0),rd(ld(X0,X1),X1))=ld(X0,X1))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f7,f968])).
% 67.38/8.94 fof(f1068,plain,(
% 67.38/8.94 ![X0,X1,X2]: (rd(mult(X0,rd(X1,X2)),X0)=mult(mult(X0,X1),rd(rd(X1,mult(X2,X1)),X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f969,f66])).
% 67.38/8.94 fof(f1459,plain,(
% 67.38/8.94 ![X0,X1,X2]: (ld(ld(X0,X1),mult(X2,ld(X0,X1)))=mult(ld(ld(X0,X1),rd(X2,X0)),X1))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f7,f259])).
% 67.38/8.94 fof(f1491,plain,(
% 67.38/8.94 ![X0,X1,X2]: (rd(ld(X0,mult(X1,X0)),mult(X2,X0))=ld(X0,rd(X1,X2)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f259,f10])).
% 67.38/8.94 fof(f1658,plain,(
% 67.38/8.94 ![X0,X1,X2]: (rd(rd(X0,X1),X2)=mult(X1,rd(ld(X1,X0),mult(X2,X1))))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f7,f317])).
% 67.38/8.94 fof(f1924,plain,(
% 67.38/8.94 ![X0,X1,X2]: (rd(mult(rd(X0,X1),X2),rd(X0,X1))=mult(X0,rd(ld(X1,X2),rd(X0,X1))))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f9,f346])).
% 67.38/8.94 fof(f2662,plain,(
% 67.38/8.94 ![X0,X1]: (ld(X0,ld(X1,mult(X1,X0)))=mult(rd(mult(X1,X0),mult(X1,mult(X1,X0))),X1))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f811,f637])).
% 67.38/8.94 fof(f2681,plain,(
% 67.38/8.94 ![X0,X1,X2]: (ld(ld(X0,X1),ld(X0,X2))=mult(ld(X1,rd(X2,X0)),X0))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f7,f637])).
% 67.38/8.94 fof(f2735,plain,(
% 67.38/8.94 ![X0,X1]: (ld(X0,X0)=mult(rd(mult(X1,X0),mult(X1,mult(X1,X0))),X1))),
% 67.38/8.94 inference(forward_demodulation,[status(thm)],[f8,f2662])).
% 67.38/8.94 fof(f3563,plain,(
% 67.38/8.94 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(X0,X0))=rd(X0,mult(X0,X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f811,f824])).
% 67.38/8.94 fof(f4965,plain,(
% 67.38/8.94 ![X0,X1,X2]: (rd(rd(X0,X1),rd(X2,X1))=mult(X1,rd(ld(X1,X0),X2)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f9,f1658])).
% 67.38/8.94 fof(f5491,plain,(
% 67.38/8.94 ![X0]: (ld(X0,X0)=mult(rd(mult(ld(X0,X0),X0),ld(X0,mult(X0,X0))),ld(X0,X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f111,f2735])).
% 67.38/8.94 fof(f5624,plain,(
% 67.38/8.94 ![X0]: (ld(X0,X0)=mult(rd(mult(ld(X0,X0),X0),X0),ld(X0,X0)))),
% 67.38/8.94 inference(forward_demodulation,[status(thm)],[f8,f5491])).
% 67.38/8.94 fof(f5625,plain,(
% 67.38/8.94 ![X0]: (ld(X0,X0)=mult(ld(X0,X0),ld(X0,X0)))),
% 67.38/8.94 inference(forward_demodulation,[status(thm)],[f10,f5624])).
% 67.38/8.94 fof(f5794,plain,(
% 67.38/8.94 ![X0]: (ld(ld(X0,X0),mult(X0,ld(X0,X0)))=mult(ld(ld(X0,X0),X0),ld(X0,X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f5625,f111])).
% 67.38/8.94 fof(f5801,plain,(
% 67.38/8.94 ![X0]: (rd(mult(ld(X0,X0),ld(X0,X0)),mult(ld(X0,X0),ld(X0,X0)))=rd(ld(ld(X0,X0),ld(X0,X0)),ld(X0,X0)))),
% 67.38/8.94 inference(paramodulation,[status(thm)],[f5625,f826])).
% 67.38/8.94 fof(f5810,plain,(
% 67.38/8.95 ![X0]: (mult(ld(X0,X0),ld(X0,X0))=mult(mult(ld(X0,X0),ld(X0,X0)),rd(ld(X0,X0),mult(ld(X0,X0),ld(X0,X0)))))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f5625,f331])).
% 67.38/8.95 fof(f5816,plain,(
% 67.38/8.95 ![X0]: (rd(ld(ld(X0,X0),ld(X0,X0)),ld(X0,X0))=ld(ld(X0,X0),ld(X0,X0)))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f5625,f694])).
% 67.38/8.95 fof(f5823,plain,(
% 67.38/8.95 ![X0,X1]: (rd(mult(ld(X0,X0),X1),ld(X0,X0))=mult(mult(ld(X0,X0),rd(X1,ld(X0,X0))),ld(X0,X0)))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f5625,f63])).
% 67.38/8.95 fof(f5829,plain,(
% 67.38/8.95 ![X0,X1]: (ld(ld(X0,X0),mult(X1,ld(X0,X0)))=mult(ld(X0,X0),mult(ld(ld(X0,X0),X1),ld(X0,X0))))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f5625,f43])).
% 67.38/8.95 fof(f5832,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(X0,ld(X1,X1)),ld(X1,X1))=mult(ld(X1,X1),mult(ld(ld(X1,X1),X0),ld(X1,X1))))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f5625,f32])).
% 67.38/8.95 fof(f5833,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(ld(X0,X0),X1),ld(X0,X0))=mult(ld(X0,X0),mult(ld(X0,X0),mult(X1,ld(X0,X0)))))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f5625,f11])).
% 67.38/8.95 fof(f5854,plain,(
% 67.38/8.95 ![X0]: (mult(ld(ld(X0,X0),rd(X0,X0)),X0)=mult(ld(ld(X0,X0),X0),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f1459,f5794])).
% 67.38/8.95 fof(f5855,plain,(
% 67.38/8.95 ![X0]: (mult(ld(ld(X0,X0),rd(X0,X0)),X0)=mult(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f668,f5854])).
% 67.38/8.95 fof(f5862,plain,(
% 67.38/8.95 ![X0]: (rd(ld(X0,X0),mult(ld(X0,X0),ld(X0,X0)))=rd(ld(ld(X0,X0),ld(X0,X0)),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f5625,f5801])).
% 67.38/8.95 fof(f5863,plain,(
% 67.38/8.95 ![X0]: (rd(ld(X0,X0),ld(X0,X0))=rd(ld(ld(X0,X0),ld(X0,X0)),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f5625,f5862])).
% 67.38/8.95 fof(f5864,plain,(
% 67.38/8.95 ![X0]: (rd(ld(X0,X0),ld(X0,X0))=rd(mult(ld(X0,rd(X0,X0)),X0),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f2681,f5863])).
% 67.38/8.95 fof(f5865,plain,(
% 67.38/8.95 ![X0]: (rd(ld(X0,X0),ld(X0,X0))=rd(mult(rd(X0,mult(X0,X0)),X0),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f811,f5864])).
% 67.38/8.95 fof(f5890,plain,(
% 67.38/8.95 ![X0]: (ld(X0,X0)=mult(mult(ld(X0,X0),ld(X0,X0)),rd(ld(X0,X0),mult(ld(X0,X0),ld(X0,X0)))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f5625,f5810])).
% 67.38/8.95 fof(f5891,plain,(
% 67.38/8.95 ![X0]: (ld(X0,X0)=mult(ld(X0,X0),rd(ld(X0,X0),mult(ld(X0,X0),ld(X0,X0)))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f5625,f5890])).
% 67.38/8.95 fof(f5895,plain,(
% 67.38/8.95 ![X0]: (ld(X0,X0)=rd(ld(X0,X0),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f969,f5891])).
% 67.38/8.95 fof(f5902,plain,(
% 67.38/8.95 ![X0]: (rd(mult(ld(X0,rd(X0,X0)),X0),ld(X0,X0))=ld(ld(X0,X0),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f2681,f5816])).
% 67.38/8.95 fof(f5903,plain,(
% 67.38/8.95 ![X0]: (rd(mult(rd(X0,mult(X0,X0)),X0),ld(X0,X0))=ld(ld(X0,X0),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f811,f5902])).
% 67.38/8.95 fof(f5904,plain,(
% 67.38/8.95 ![X0]: (rd(ld(X0,X0),ld(X0,X0))=ld(ld(X0,X0),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f5865,f5903])).
% 67.38/8.95 fof(f5905,plain,(
% 67.38/8.95 ![X0]: (ld(X0,X0)=ld(ld(X0,X0),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f5895,f5904])).
% 67.38/8.95 fof(f5906,plain,(
% 67.38/8.95 ![X0]: (ld(X0,X0)=mult(ld(X0,rd(X0,X0)),X0))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f2681,f5905])).
% 67.38/8.95 fof(f5908,plain,(
% 67.38/8.95 ![X0]: (ld(X0,X0)=mult(rd(X0,mult(X0,X0)),X0))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f811,f5906])).
% 67.38/8.95 fof(f5916,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(ld(X0,X0),rd(X1,X0)),X0)=mult(mult(ld(X0,X0),rd(X1,ld(X0,X0))),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f298,f5823])).
% 67.38/8.95 fof(f5917,plain,(
% 67.38/8.95 ![X0,X1]: (mult(X0,mult(ld(X0,ld(X0,X0)),X1))=mult(mult(ld(X0,X0),rd(X1,ld(X0,X0))),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f54,f5916])).
% 67.38/8.95 fof(f5918,plain,(
% 67.38/8.95 ![X0,X1]: (mult(X0,mult(ld(X0,ld(X0,X0)),X1))=mult(ld(X0,X0),mult(ld(ld(X0,X0),ld(X0,X0)),X1)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f54,f5917])).
% 67.38/8.95 fof(f5919,plain,(
% 67.38/8.95 ![X0,X1]: (mult(X0,mult(ld(X0,ld(X0,X0)),X1))=mult(ld(X0,X0),mult(mult(ld(X0,rd(X0,X0)),X0),X1)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f2681,f5918])).
% 67.38/8.95 fof(f5920,plain,(
% 67.38/8.95 ![X0,X1]: (mult(X0,mult(ld(X0,ld(X0,X0)),X1))=mult(ld(X0,X0),mult(mult(rd(X0,mult(X0,X0)),X0),X1)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f811,f5919])).
% 67.38/8.95 fof(f5923,plain,(
% 67.38/8.95 ![X0,X1]: (mult(X0,mult(ld(X0,ld(X0,X0)),X1))=mult(ld(X0,X0),mult(ld(X0,X0),X1)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f5908,f5920])).
% 67.38/8.95 fof(f5934,plain,(
% 67.38/8.95 ![X0,X1]: (mult(ld(ld(X0,X0),rd(X1,X0)),X0)=mult(ld(X0,X0),mult(ld(ld(X0,X0),X1),ld(X0,X0))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f1459,f5829])).
% 67.38/8.95 fof(f5936,plain,(
% 67.38/8.95 ![X0,X1]: (mult(ld(ld(X0,X0),rd(X1,X0)),X0)=mult(mult(X1,ld(X0,X0)),ld(X0,X0)))),
% 67.38/8.95 inference(backward_demodulation,[status(thm)],[f5832,f5934])).
% 67.38/8.95 fof(f5938,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(ld(X0,X0),X1),ld(X0,X0))=mult(X0,mult(ld(X0,ld(X0,X0)),mult(X1,ld(X0,X0)))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f5923,f5833])).
% 67.38/8.95 fof(f5948,plain,(
% 67.38/8.95 ![X0]: (mult(mult(X0,ld(X0,X0)),ld(X0,X0))=mult(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 67.38/8.95 inference(backward_demodulation,[status(thm)],[f5936,f5855])).
% 67.38/8.95 fof(f5951,plain,(
% 67.38/8.95 ![X0]: (mult(X0,ld(X0,X0))=mult(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f7,f5948])).
% 67.38/8.95 fof(f5952,plain,(
% 67.38/8.95 ![X0]: (X0=mult(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f7,f5951])).
% 67.38/8.95 fof(f6452,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(mult(rd(X0,mult(X0,X0)),X0),mult(X1,rd(X0,mult(X0,X0)))),rd(X0,ld(X0,X0)))=mult(mult(mult(rd(X0,mult(X0,X0)),X0),X0),ld(X0,X1)))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f5908,f73])).
% 67.38/8.95 fof(f6492,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(X0,rd(X1,mult(X1,X1))),X1)=mult(X1,mult(ld(X1,X0),ld(X1,X1))))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f5908,f32])).
% 67.38/8.95 fof(f6494,plain,(
% 67.38/8.95 ![X0]: (rd(ld(X0,X0),X0)=rd(X0,mult(X0,X0)))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f5908,f10])).
% 67.38/8.95 fof(f6510,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),rd(X0,ld(X0,X0)))=mult(mult(mult(rd(X0,mult(X0,X0)),X0),X0),ld(X0,X1)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f5908,f6452])).
% 67.38/8.95 fof(f6511,plain,(
% 67.38/8.95 ![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)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f20,f6510])).
% 67.38/8.95 fof(f6512,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)=mult(mult(ld(X0,X0),X0),ld(X0,X1)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f5908,f6511])).
% 67.38/8.95 fof(f6583,plain,(
% 67.38/8.95 ![X0]: (mult(ld(X0,X0),X0)=mult(X0,rd(X0,mult(ld(X0,X0),X0))))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f5952,f331])).
% 67.38/8.95 fof(f6597,plain,(
% 67.38/8.95 ![X0]: (ld(mult(ld(X0,X0),X0),rd(ld(X0,X0),mult(ld(X0,X0),X0)))=mult(rd(ld(X0,X0),X0),rd(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f5952,f825])).
% 67.38/8.95 fof(f6608,plain,(
% 67.38/8.95 ![X0,X1]: (rd(rd(X0,mult(ld(X0,X0),X0)),X1)=mult(mult(ld(X0,X0),X0),rd(ld(X0,X0),mult(X1,mult(ld(X0,X0),X0)))))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f5952,f317])).
% 67.38/8.95 fof(f6655,plain,(
% 67.38/8.95 ![X0]: (mult(ld(X0,X0),X0)=rd(X0,ld(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f969,f6583])).
% 67.38/8.95 fof(f6657,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)=mult(X0,ld(X0,X1)))),
% 67.38/8.95 inference(backward_demodulation,[status(thm)],[f6658,f6512])).
% 67.38/8.95 fof(f6658,plain,(
% 67.38/8.95 ![X0]: (mult(ld(X0,X0),X0)=X0)),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f20,f6655])).
% 67.38/8.95 fof(f6701,plain,(
% 67.38/8.95 ![X0]: (ld(X0,rd(ld(X0,X0),mult(ld(X0,X0),X0)))=mult(rd(ld(X0,X0),X0),rd(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6658,f6597])).
% 67.38/8.95 fof(f6702,plain,(
% 67.38/8.95 ![X0]: (ld(X0,rd(ld(X0,X0),X0))=mult(rd(ld(X0,X0),X0),rd(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6658,f6701])).
% 67.38/8.95 fof(f6703,plain,(
% 67.38/8.95 ![X0]: (ld(X0,rd(X0,mult(X0,X0)))=mult(rd(ld(X0,X0),X0),rd(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6494,f6702])).
% 67.38/8.95 fof(f6704,plain,(
% 67.38/8.95 ![X0]: (rd(X0,mult(mult(X0,X0),X0))=mult(rd(ld(X0,X0),X0),rd(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f811,f6703])).
% 67.38/8.95 fof(f6705,plain,(
% 67.38/8.95 ![X0]: (rd(X0,mult(mult(X0,X0),X0))=mult(rd(X0,mult(X0,X0)),rd(ld(X0,X0),mult(ld(X0,X0),X0))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6494,f6704])).
% 67.38/8.95 fof(f6706,plain,(
% 67.38/8.95 ![X0]: (rd(X0,mult(mult(X0,X0),X0))=mult(rd(X0,mult(X0,X0)),rd(ld(X0,X0),X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6658,f6705])).
% 67.38/8.95 fof(f6707,plain,(
% 67.38/8.95 ![X0]: (rd(X0,mult(mult(X0,X0),X0))=mult(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6494,f6706])).
% 67.38/8.95 fof(f6746,plain,(
% 67.38/8.95 ![X0,X1]: (rd(ld(X0,X0),X1)=mult(mult(ld(X0,X0),X0),rd(ld(X0,X0),mult(X1,mult(ld(X0,X0),X0)))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f766,f6608])).
% 67.38/8.95 fof(f6747,plain,(
% 67.38/8.95 ![X0,X1]: (rd(ld(X0,X0),X1)=mult(X0,rd(ld(X0,X0),mult(X1,mult(ld(X0,X0),X0)))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6658,f6746])).
% 67.38/8.95 fof(f6748,plain,(
% 67.38/8.95 ![X0,X1]: (rd(ld(X0,X0),X1)=mult(X0,rd(ld(X0,X0),mult(X1,X0))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6658,f6747])).
% 67.38/8.95 fof(f6758,plain,(
% 67.38/8.95 ![X0]: (rd(rd(X0,X0),X0)=rd(X0,mult(X0,X0)))),
% 67.38/8.95 inference(backward_demodulation,[status(thm)],[f6764,f6494])).
% 67.38/8.95 fof(f6764,plain,(
% 67.38/8.95 ![X0,X1]: (rd(ld(X0,X0),X1)=rd(rd(X0,X0),X1))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f1658,f6748])).
% 67.38/8.95 fof(f6828,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(ld(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)=X1)),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f7,f6657])).
% 67.38/8.95 fof(f6834,plain,(
% 67.38/8.95 ![X0]: (rd(X0,mult(X0,X0))=ld(X0,ld(X0,X0)))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f6658,f807])).
% 67.38/8.95 fof(f6836,plain,(
% 67.38/8.95 ![X0]: (rd(X0,X0)=ld(X0,X0))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f6658,f766])).
% 67.38/8.95 fof(f6864,plain,(
% 67.38/8.95 ![X0,X1]: (rd(mult(ld(X0,X0),X1),ld(X0,X0))=mult(X0,rd(ld(X0,X1),ld(X0,X0))))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f6658,f346])).
% 67.38/8.95 fof(f6865,plain,(
% 67.38/8.95 ![X0]: (mult(ld(X0,X0),X0)=mult(mult(mult(ld(X0,X0),X0),ld(X0,X0)),rd(X0,X0)))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f6658,f331])).
% 67.38/8.95 fof(f6899,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(ld(X0,X0),X1),ld(X0,X0))=mult(X0,mult(rd(X0,mult(X0,X0)),mult(X1,ld(X0,X0)))))),
% 67.38/8.95 inference(backward_demodulation,[status(thm)],[f6834,f5938])).
% 67.38/8.95 fof(f6901,plain,(
% 67.38/8.95 ![X0,X1]: (mult(X0,mult(rd(X0,mult(X0,X0)),X1))=mult(ld(X0,X0),mult(ld(X0,X0),X1)))),
% 67.38/8.95 inference(backward_demodulation,[status(thm)],[f6834,f5923])).
% 67.38/8.95 fof(f6905,plain,(
% 67.38/8.95 ![X0]: (ld(X0,X0)=mult(ld(X0,X0),rd(X0,X0)))),
% 67.38/8.95 inference(backward_demodulation,[status(thm)],[f6836,f5625])).
% 67.38/8.95 fof(f6935,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)=X1)),
% 67.38/8.95 inference(backward_demodulation,[status(thm)],[f6836,f6828])).
% 67.38/8.95 fof(f6945,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(X0,rd(X1,mult(X1,X1))),X1)=mult(X1,mult(ld(X1,X0),rd(X1,X1))))),
% 67.38/8.95 inference(backward_demodulation,[status(thm)],[f6836,f6492])).
% 67.38/8.95 fof(f7074,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(ld(X0,X0),rd(X1,X0)),X0)=mult(X0,rd(ld(X0,X1),ld(X0,X0))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f298,f6864])).
% 67.38/8.95 fof(f7075,plain,(
% 67.38/8.95 ![X0,X1]: (mult(X0,mult(ld(X0,ld(X0,X0)),X1))=mult(X0,rd(ld(X0,X1),ld(X0,X0))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f54,f7074])).
% 67.38/8.95 fof(f7076,plain,(
% 67.38/8.95 ![X0,X1]: (mult(X0,mult(rd(X0,mult(X0,X0)),X1))=mult(X0,rd(ld(X0,X1),ld(X0,X0))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6834,f7075])).
% 67.38/8.95 fof(f7077,plain,(
% 67.38/8.95 ![X0,X1]: (mult(X0,mult(rd(X0,mult(X0,X0)),X1))=mult(X0,rd(ld(X0,X1),rd(X0,X0))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6836,f7076])).
% 67.38/8.95 fof(f7078,plain,(
% 67.38/8.95 ![X0]: (X0=mult(mult(mult(ld(X0,X0),X0),ld(X0,X0)),rd(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6658,f6865])).
% 67.38/8.95 fof(f7079,plain,(
% 67.38/8.95 ![X0]: (X0=mult(mult(X0,ld(X0,X0)),rd(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6658,f7078])).
% 67.38/8.95 fof(f7082,plain,(
% 67.38/8.95 ![X0]: (X0=mult(X0,rd(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f7,f7079])).
% 67.38/8.95 fof(f7154,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(rd(X0,X0),X1),ld(X0,X0))=mult(X0,mult(rd(X0,mult(X0,X0)),mult(X1,ld(X0,X0)))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6836,f6899])).
% 67.38/8.95 fof(f7155,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(rd(X0,X0),X1),rd(X0,X0))=mult(X0,mult(rd(X0,mult(X0,X0)),mult(X1,ld(X0,X0)))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6836,f7154])).
% 67.38/8.95 fof(f7156,plain,(
% 67.38/8.95 ![X0,X1]: (mult(mult(rd(X0,X0),X1),rd(X0,X0))=mult(X0,mult(rd(X0,mult(X0,X0)),mult(X1,rd(X0,X0)))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6836,f7155])).
% 67.38/8.95 fof(f7162,plain,(
% 67.38/8.95 ![X0,X1]: (mult(X0,mult(rd(X0,mult(X0,X0)),X1))=mult(rd(X0,X0),mult(ld(X0,X0),X1)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6836,f6901])).
% 67.38/8.95 fof(f7163,plain,(
% 67.38/8.95 ![X0,X1]: (mult(X0,mult(rd(X0,mult(X0,X0)),X1))=mult(rd(X0,X0),mult(rd(X0,X0),X1)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6836,f7162])).
% 67.38/8.95 fof(f7167,plain,(
% 67.38/8.95 ![X0]: (rd(X0,X0)=mult(ld(X0,X0),rd(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6836,f6905])).
% 67.38/8.95 fof(f7168,plain,(
% 67.38/8.95 ![X0]: (rd(X0,X0)=mult(rd(X0,X0),rd(X0,X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6836,f7167])).
% 67.38/8.95 fof(f7277,plain,(
% 67.38/8.95 ![X0]: (rd(ld(X0,X0),X0)=mult(ld(X0,X0),rd(rd(X0,X0),X0)))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f6836,f979])).
% 67.38/8.95 fof(f7317,plain,(
% 67.38/8.95 ![X0]: (rd(rd(X0,X0),X0)=mult(ld(X0,X0),rd(rd(X0,X0),X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6836,f7277])).
% 67.38/8.95 fof(f7318,plain,(
% 67.38/8.95 ![X0]: (rd(X0,mult(X0,X0))=mult(ld(X0,X0),rd(rd(X0,X0),X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6758,f7317])).
% 67.38/8.95 fof(f7319,plain,(
% 67.38/8.95 ![X0]: (rd(X0,mult(X0,X0))=mult(rd(X0,X0),rd(rd(X0,X0),X0)))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6836,f7318])).
% 67.38/8.95 fof(f7320,plain,(
% 67.38/8.95 ![X0]: (rd(X0,mult(X0,X0))=mult(rd(X0,X0),rd(X0,mult(X0,X0))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f6758,f7319])).
% 67.38/8.95 fof(f7714,plain,(
% 67.38/8.95 ![X0]: (mult(mult(X0,X0),rd(X0,X0))=mult(rd(X0,X0),mult(X0,X0)))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f7082,f31])).
% 67.38/8.95 fof(f7736,plain,(
% 67.38/8.95 ![X0]: (mult(X0,rd(X0,X0))=mult(mult(X0,X0),rd(rd(X0,X0),mult(X0,rd(X0,X0)))))),
% 67.38/8.95 inference(paramodulation,[status(thm)],[f7082,f331])).
% 67.38/8.95 fof(f7838,plain,(
% 67.38/8.95 ![X0]: (X0=mult(mult(X0,X0),rd(rd(X0,X0),mult(X0,rd(X0,X0)))))),
% 67.38/8.95 inference(forward_demodulation,[status(thm)],[f7082,f7736])).
% 67.38/8.96 fof(f7839,plain,(
% 67.38/8.96 ![X0]: (X0=mult(mult(X0,X0),mult(rd(X0,X0),rd(rd(X0,X0),X0))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f977,f7838])).
% 67.38/8.96 fof(f7840,plain,(
% 67.38/8.96 ![X0]: (X0=mult(mult(X0,X0),mult(rd(X0,X0),rd(X0,mult(X0,X0)))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f6758,f7839])).
% 67.38/8.96 fof(f7841,plain,(
% 67.38/8.96 ![X0]: (X0=mult(mult(X0,X0),rd(X0,mult(X0,X0))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f7320,f7840])).
% 67.38/8.96 fof(f7943,plain,(
% 67.38/8.96 ![X0]: (ld(rd(X0,mult(X0,X0)),rd(X0,X0))=X0)),
% 67.38/8.96 inference(paramodulation,[status(thm)],[f6758,f18])).
% 67.38/8.96 fof(f8462,plain,(
% 67.38/8.96 ![X0]: (ld(rd(X0,mult(X0,X0)),X0)=mult(ld(rd(X0,mult(X0,X0)),X0),mult(X0,rd(X0,mult(X0,X0)))))),
% 67.38/8.96 inference(paramodulation,[status(thm)],[f7841,f60])).
% 67.38/8.96 fof(f8536,plain,(
% 67.38/8.96 ![X0]: (mult(X0,X0)=mult(ld(rd(X0,mult(X0,X0)),X0),mult(X0,rd(X0,mult(X0,X0)))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f18,f8462])).
% 67.38/8.96 fof(f8537,plain,(
% 67.38/8.96 ![X0]: (mult(X0,X0)=mult(mult(X0,X0),mult(X0,rd(X0,mult(X0,X0)))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f18,f8536])).
% 67.38/8.96 fof(f8539,plain,(
% 67.38/8.96 ![X0]: (mult(X0,X0)=mult(rd(X0,X0),mult(X0,X0)))),
% 67.38/8.96 inference(backward_demodulation,[status(thm)],[f8540,f7714])).
% 67.38/8.96 fof(f8540,plain,(
% 67.38/8.96 ![X0]: (mult(X0,X0)=mult(mult(X0,X0),rd(X0,X0)))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f969,f8537])).
% 67.38/8.96 fof(f9237,plain,(
% 67.38/8.96 ![X0]: (ld(mult(X0,X0),mult(X0,mult(X0,X0)))=X0)),
% 67.38/8.96 inference(paramodulation,[status(thm)],[f8540,f90])).
% 67.38/8.96 fof(f9243,plain,(
% 67.38/8.96 ![X0]: (mult(mult(X0,X0),X0)=mult(X0,mult(X0,mult(rd(X0,X0),X0))))),
% 67.38/8.96 inference(paramodulation,[status(thm)],[f8540,f11])).
% 67.38/8.96 fof(f9331,plain,(
% 67.38/8.96 ![X0]: (rd(X0,mult(X0,mult(X0,X0)))=mult(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0))))),
% 67.38/8.96 inference(backward_demodulation,[status(thm)],[f9333,f6707])).
% 67.38/8.96 fof(f9333,plain,(
% 67.38/8.96 ![X0]: (mult(mult(X0,X0),X0)=mult(X0,mult(X0,X0)))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f9,f9243])).
% 67.38/8.96 fof(f9474,plain,(
% 67.38/8.96 ![X0,X1]: (rd(ld(mult(X0,X0),mult(X1,mult(X0,X0))),mult(X0,X0))=ld(mult(X0,X0),rd(X1,rd(X0,X0))))),
% 67.38/8.96 inference(paramodulation,[status(thm)],[f8539,f1491])).
% 67.38/8.96 fof(f9666,plain,(
% 67.38/8.96 ![X0,X1]: (rd(X0,mult(X1,mult(X0,X0)))=ld(mult(X0,X0),rd(X0,X1)))),
% 67.38/8.96 inference(paramodulation,[status(thm)],[f9237,f1491])).
% 67.38/8.96 fof(f9671,plain,(
% 67.38/8.96 ![X0]: (rd(rd(ld(mult(X0,X0),mult(X0,mult(X0,X0))),mult(X0,X0)),rd(X0,mult(X0,mult(X0,X0))))=ld(mult(X0,X0),mult(X0,mult(X0,X0))))),
% 67.38/8.96 inference(paramodulation,[status(thm)],[f9237,f1013])).
% 67.38/8.96 fof(f9706,plain,(
% 67.38/8.96 ![X0]: (rd(ld(mult(X0,X0),rd(X0,rd(X0,X0))),rd(X0,mult(X0,mult(X0,X0))))=ld(mult(X0,X0),mult(X0,mult(X0,X0))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f9474,f9671])).
% 67.38/8.96 fof(f9707,plain,(
% 67.38/8.96 ![X0]: (rd(rd(X0,mult(rd(X0,X0),mult(X0,X0))),rd(X0,mult(X0,mult(X0,X0))))=ld(mult(X0,X0),mult(X0,mult(X0,X0))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f9666,f9706])).
% 67.38/8.96 fof(f9708,plain,(
% 67.38/8.96 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,mult(X0,X0))))=ld(mult(X0,X0),mult(X0,mult(X0,X0))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f8539,f9707])).
% 67.38/8.96 fof(f9709,plain,(
% 67.38/8.96 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,mult(X0,X0))))=X0)),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f9237,f9708])).
% 67.38/8.96 fof(f11134,plain,(
% 67.38/8.96 ![X0,X1]: (rd(mult(rd(X0,X0),X1),rd(X0,X0))=mult(mult(rd(X0,X0),rd(X1,rd(X0,mult(X0,X0)))),rd(X0,mult(X0,X0))))),
% 67.38/8.96 inference(paramodulation,[status(thm)],[f3563,f295])).
% 67.38/8.96 fof(f11238,plain,(
% 67.38/8.96 ![X0,X1]: (mult(X0,rd(ld(X0,X1),rd(X0,X0)))=mult(mult(rd(X0,X0),rd(X1,rd(X0,mult(X0,X0)))),rd(X0,mult(X0,X0))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f1924,f11134])).
% 67.38/8.96 fof(f11239,plain,(
% 67.38/8.96 ![X0,X1]: (mult(X0,mult(rd(X0,mult(X0,X0)),X1))=mult(mult(rd(X0,X0),rd(X1,rd(X0,mult(X0,X0)))),rd(X0,mult(X0,X0))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f7077,f11238])).
% 67.38/8.96 fof(f11240,plain,(
% 67.38/8.96 ![X0,X1]: (mult(X0,mult(rd(X0,mult(X0,X0)),X1))=mult(rd(X0,mult(X0,X0)),mult(ld(rd(X0,mult(X0,X0)),rd(X0,X0)),X1)))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f54,f11239])).
% 67.38/8.96 fof(f11247,plain,(
% 67.38/8.96 ![X0,X1]: (mult(X0,mult(rd(X0,mult(X0,X0)),X1))=mult(rd(X0,mult(X0,X0)),mult(X0,X1)))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f7943,f11240])).
% 67.38/8.96 fof(f14654,plain,(
% 67.38/8.96 ![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)))))))),
% 67.38/8.96 inference(paramodulation,[status(thm)],[f6935,f6935])).
% 67.38/8.96 fof(f14670,plain,(
% 67.38/8.96 ![X0,X1]: (mult(mult(rd(rd(X0,X0),rd(X0,X0)),mult(X1,rd(rd(X0,X0),rd(X0,X0)))),rd(X0,X0))=X1)),
% 67.38/8.96 inference(paramodulation,[status(thm)],[f7168,f6935])).
% 67.38/8.96 fof(f14672,plain,(
% 67.38/8.96 ![X0,X1]: (ld(mult(mult(mult(mult(X0,rd(X1,mult(X1,X1))),X1),X1),ld(X1,rd(X1,X1))),mult(mult(mult(X0,rd(X1,mult(X1,X1))),X1),X0))=mult(mult(X0,rd(X1,mult(X1,X1))),X1))),
% 67.38/8.96 inference(paramodulation,[status(thm)],[f6935,f88])).
% 67.38/8.96 fof(f14674,plain,(
% 67.38/8.96 ![X0,X1,X2]: (ld(mult(mult(rd(X0,X0),mult(mult(X1,rd(X0,mult(X0,X0))),mult(X0,rd(X0,X0)))),X2),mult(mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0),mult(rd(X0,X0),mult(X2,X1))))=mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0))),
% 67.38/8.96 inference(paramodulation,[status(thm)],[f6935,f81])).
% 67.38/8.96 fof(f14675,plain,(
% 67.38/8.96 ![X0,X1,X2]: (ld(mult(mult(rd(X0,X0),mult(mult(X1,rd(X0,mult(X0,X0))),mult(X0,rd(X0,X0)))),X2),mult(X1,mult(rd(X0,X0),mult(X2,mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)))))=mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0))),
% 67.38/8.96 inference(paramodulation,[status(thm)],[f6935,f81])).
% 67.38/8.96 fof(f14795,plain,(
% 67.38/8.96 ![X0,X1]: (mult(mult(rd(X0,X0),X1),X0)=mult(mult(mult(X0,X0),rd(ld(mult(X0,X0),X0),X0)),mult(X1,rd(rd(X0,mult(X0,X0)),mult(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f4965,f14654])).
% 67.38/8.96 fof(f14796,plain,(
% 67.38/8.96 ![X0,X1]: (mult(mult(rd(X0,X0),X1),X0)=mult(mult(mult(X0,X0),rd(rd(ld(X0,X0),X0),X0)),mult(X1,rd(rd(X0,mult(X0,X0)),mult(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f694,f14795])).
% 67.38/8.96 fof(f14797,plain,(
% 67.38/8.96 ![X0,X1]: (mult(mult(rd(X0,X0),X1),X0)=mult(mult(mult(X0,X0),rd(rd(rd(X0,X0),X0),X0)),mult(X1,rd(rd(X0,mult(X0,X0)),mult(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f6836,f14796])).
% 67.38/8.96 fof(f14798,plain,(
% 67.38/8.96 ![X0,X1]: (mult(mult(rd(X0,X0),X1),X0)=mult(mult(mult(X0,X0),rd(rd(X0,mult(X0,X0)),X0)),mult(X1,rd(rd(X0,mult(X0,X0)),mult(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f6758,f14797])).
% 67.38/8.96 fof(f14799,plain,(
% 67.38/8.96 ![X0,X1]: (mult(mult(rd(X0,X0),X1),X0)=mult(rd(mult(X0,rd(X0,X0)),X0),mult(X1,rd(rd(X0,mult(X0,X0)),mult(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f1068,f14798])).
% 67.38/8.96 fof(f14800,plain,(
% 67.38/8.96 ![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)))))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f7082,f14799])).
% 67.38/8.96 fof(f14801,plain,(
% 67.38/8.96 ![X0,X1]: (mult(mult(rd(X0,X0),X1),X0)=mult(rd(X0,X0),mult(X1,rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,mult(X0,X0)))))))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f9331,f14800])).
% 67.38/8.96 fof(f14809,plain,(
% 67.38/8.96 ![X0,X1]: (mult(mult(rd(X0,X0),X1),X0)=mult(rd(X0,X0),mult(X1,X0)))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f9709,f14801])).
% 67.38/8.96 fof(f14885,plain,(
% 67.38/8.96 ![X0,X1]: (mult(rd(rd(X0,X0),rd(X0,X0)),mult(mult(X1,rd(rd(X0,X0),rd(X0,X0))),rd(X0,X0)))=X1)),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f14809,f14670])).
% 67.38/8.96 fof(f14886,plain,(
% 67.38/8.96 ![X0,X1]: (mult(mult(X0,rd(ld(X0,X0),X0)),mult(mult(X1,rd(rd(X0,X0),rd(X0,X0))),rd(X0,X0)))=X1)),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f4965,f14885])).
% 67.38/8.96 fof(f14887,plain,(
% 67.38/8.96 ![X0,X1]: (mult(mult(X0,rd(rd(X0,X0),X0)),mult(mult(X1,rd(rd(X0,X0),rd(X0,X0))),rd(X0,X0)))=X1)),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f6836,f14886])).
% 67.38/8.96 fof(f14888,plain,(
% 67.38/8.96 ![X0,X1]: (mult(mult(X0,rd(X0,mult(X0,X0))),mult(mult(X1,rd(rd(X0,X0),rd(X0,X0))),rd(X0,X0)))=X1)),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f6758,f14887])).
% 67.38/8.96 fof(f14889,plain,(
% 67.38/8.96 ![X0,X1]: (mult(rd(X0,X0),mult(mult(X1,rd(rd(X0,X0),rd(X0,X0))),rd(X0,X0)))=X1)),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f969,f14888])).
% 67.38/8.96 fof(f14890,plain,(
% 67.38/8.96 ![X0,X1]: (mult(rd(X0,X0),mult(rd(X0,X0),mult(ld(rd(X0,X0),X1),rd(X0,X0))))=X1)),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f54,f14889])).
% 67.38/8.96 fof(f14891,plain,(
% 67.38/8.96 ![X0,X1]: (mult(X0,mult(rd(X0,mult(X0,X0)),mult(ld(rd(X0,X0),X1),rd(X0,X0))))=X1)),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f7163,f14890])).
% 67.38/8.96 fof(f14892,plain,(
% 67.38/8.96 ![X0,X1]: (mult(mult(rd(X0,X0),ld(rd(X0,X0),X1)),rd(X0,X0))=X1)),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f7156,f14891])).
% 67.38/8.96 fof(f14990,plain,(
% 67.38/8.96 ![X0,X1]: (mult(X0,rd(X1,X1))=X0)),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f7,f14892])).
% 67.38/8.96 fof(f14997,plain,(
% 67.38/8.96 ![X0,X1]: (ld(mult(mult(mult(X0,mult(ld(X0,X1),rd(X0,X0))),X0),ld(X0,rd(X0,X0))),mult(mult(mult(X1,rd(X0,mult(X0,X0))),X0),X1))=mult(mult(X1,rd(X0,mult(X0,X0))),X0))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f6945,f14672])).
% 67.38/8.96 fof(f14998,plain,(
% 67.38/8.96 ![X0,X1]: (ld(mult(mult(mult(X0,ld(X0,X1)),X0),ld(X0,rd(X0,X0))),mult(mult(mult(X1,rd(X0,mult(X0,X0))),X0),X1))=mult(mult(X1,rd(X0,mult(X0,X0))),X0))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f14990,f14997])).
% 67.38/8.96 fof(f14999,plain,(
% 67.38/8.96 ![X0,X1]: (ld(mult(mult(X0,X1),ld(X1,rd(X1,X1))),mult(mult(mult(X0,rd(X1,mult(X1,X1))),X1),X0))=mult(mult(X0,rd(X1,mult(X1,X1))),X1))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f7,f14998])).
% 67.38/8.96 fof(f15000,plain,(
% 67.38/8.96 ![X0,X1]: (ld(mult(mult(X0,X1),rd(X1,mult(X1,X1))),mult(mult(mult(X0,rd(X1,mult(X1,X1))),X1),X0))=mult(mult(X0,rd(X1,mult(X1,X1))),X1))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f811,f14999])).
% 67.38/8.96 fof(f15001,plain,(
% 67.38/8.96 ![X0,X1]: (ld(mult(mult(X0,X1),rd(X1,mult(X1,X1))),mult(X0,mult(rd(X1,mult(X1,X1)),mult(X1,X0))))=mult(mult(X0,rd(X1,mult(X1,X1))),X1))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f11,f15000])).
% 67.38/8.96 fof(f15002,plain,(
% 67.38/8.96 ![X0,X1]: (ld(mult(mult(X0,X1),rd(X1,mult(X1,X1))),mult(X0,mult(X1,mult(rd(X1,mult(X1,X1)),X0))))=mult(mult(X0,rd(X1,mult(X1,X1))),X1))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f11247,f15001])).
% 67.38/8.96 fof(f15003,plain,(
% 67.38/8.96 ![X0,X1]: (X0=mult(mult(X0,rd(X1,mult(X1,X1))),X1))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f34,f15002])).
% 67.38/8.96 fof(f15005,plain,(
% 67.38/8.96 ![X0,X1,X2]: (ld(mult(mult(rd(X0,X0),mult(mult(X1,rd(X0,mult(X0,X0))),X0)),X2),mult(mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0),mult(rd(X0,X0),mult(X2,X1))))=mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f7082,f14674])).
% 67.38/8.96 fof(f15006,plain,(
% 67.38/8.96 ![X0,X1,X2]: (ld(mult(mult(rd(X0,X0),X1),X2),mult(mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0),mult(rd(X0,X0),mult(X2,X1))))=mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f15003,f15005])).
% 67.38/8.96 fof(f15007,plain,(
% 67.38/8.96 ![X0,X1,X2]: (ld(mult(mult(rd(X0,X0),X1),X2),mult(X1,mult(rd(X0,X0),mult(X2,X1))))=mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f6935,f15006])).
% 67.38/8.96 fof(f15008,plain,(
% 67.38/8.96 ![X0,X1,X2]: (ld(mult(mult(rd(X0,X0),X1),X2),mult(X1,mult(rd(X0,X0),mult(X2,X1))))=X1)),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f6935,f15007])).
% 67.38/8.96 fof(f15009,plain,(
% 67.38/8.96 ![X0,X1,X2]: (ld(mult(mult(rd(X0,X0),mult(mult(X1,rd(X0,mult(X0,X0))),X0)),X2),mult(X1,mult(rd(X0,X0),mult(X2,mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)))))=mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f7082,f14675])).
% 67.38/8.96 fof(f15010,plain,(
% 67.38/8.96 ![X0,X1,X2]: (ld(mult(mult(rd(X0,X0),X1),X2),mult(X1,mult(rd(X0,X0),mult(X2,mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0)))))=mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f15003,f15009])).
% 67.38/8.96 fof(f15011,plain,(
% 67.38/8.96 ![X0,X1,X2]: (ld(mult(mult(rd(X0,X0),X1),X2),mult(X1,mult(rd(X0,X0),mult(X2,X1))))=mult(mult(rd(X0,X0),mult(X1,rd(X0,mult(X0,X0)))),X0))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f6935,f15010])).
% 67.38/8.96 fof(f15012,plain,(
% 67.38/8.96 ![X0,X1]: (X0=mult(mult(rd(X1,X1),mult(X0,rd(X1,mult(X1,X1)))),X1))),
% 67.38/8.96 inference(forward_demodulation,[status(thm)],[f15008,f15011])).
% 67.38/8.96 fof(f15013,plain,(
% 67.38/8.96 ![X0,X1]: (X0=mult(rd(X1,X1),mult(mult(X0,rd(X1,mult(X1,X1))),X1)))),
% 63.60/9.17 inference(forward_demodulation,[status(thm)],[f14809,f15012])).
% 63.60/9.17 fof(f15014,plain,(
% 63.60/9.17 ~x0=x0),
% 63.60/9.17 inference(backward_demodulation,[status(thm)],[f15084,f12])).
% 63.60/9.17 fof(f15084,plain,(
% 63.60/9.17 ![X0,X1]: (X0=mult(rd(X1,X1),X0))),
% 63.60/9.17 inference(forward_demodulation,[status(thm)],[f15003,f15013])).
% 63.60/9.17 fof(f16306,plain,(
% 63.60/9.17 $false),
% 63.60/9.17 inference(trivial_equality_resolution,[status(thm)],[f15014])).
% 63.60/9.17 % SZS output end CNFRefutation for theBenchmark.p
% 50.05/10.33 % Elapsed time: 9.747752 seconds
% 50.05/10.33 % CPU time: 31.030279 seconds
% 50.05/10.33 % Total memory used: 436.049 MB
% 50.05/10.33 % Net memory used: 431.916 MB
%------------------------------------------------------------------------------