%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP660-11 : 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 : n019.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 45.76s 6.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP660-11 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n019.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Sun Sep 20 20:30:05 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.43 % Drodi V4.1.1
% 45.76/6.83 % Refutation found
% 45.76/6.83 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 45.76/6.83 % SZS output start CNFRefutation for theBenchmark
% 45.76/6.83 fof(f1,axiom,(
% 45.76/6.83 (![A,B]: (mult(A,ld(A,B)) = B ))),
% 45.76/6.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.76/6.83 fof(f2,axiom,(
% 45.76/6.83 (![A,B]: (ld(A,mult(A,B)) = B ))),
% 45.76/6.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.76/6.83 fof(f3,axiom,(
% 45.76/6.83 (![A,B]: (mult(rd(A,B),B) = A ))),
% 45.76/6.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.76/6.83 fof(f4,axiom,(
% 45.76/6.83 (![A,B]: (rd(mult(A,B),B) = A ))),
% 45.76/6.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.76/6.83 fof(f5,axiom,(
% 45.76/6.83 (![A,B,C]: (mult(mult(mult(A,B),C),A) = mult(A,mult(B,mult(C,A))) ))),
% 45.76/6.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.76/6.83 fof(f6,negated_conjecture,(
% 45.76/6.83 mult(x0,rd(x1,x1)) != x0 ),
% 45.76/6.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 45.76/6.83 fof(f7,plain,(
% 45.76/6.83 ![X0,X1]: (mult(X0,ld(X0,X1))=X1)),
% 45.76/6.83 inference(cnf_transformation,[status(thm)],[f1])).
% 45.76/6.83 fof(f8,plain,(
% 45.76/6.83 ![X0,X1]: (ld(X0,mult(X0,X1))=X1)),
% 45.76/6.83 inference(cnf_transformation,[status(thm)],[f2])).
% 45.76/6.83 fof(f9,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(X0,X1),X1)=X0)),
% 45.76/6.83 inference(cnf_transformation,[status(thm)],[f3])).
% 45.76/6.83 fof(f10,plain,(
% 45.76/6.83 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 45.76/6.83 inference(cnf_transformation,[status(thm)],[f4])).
% 45.76/6.83 fof(f11,plain,(
% 45.76/6.83 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X2),X0)=mult(X0,mult(X1,mult(X2,X0))))),
% 45.76/6.83 inference(cnf_transformation,[status(thm)],[f5])).
% 45.76/6.83 fof(f12,plain,(
% 45.76/6.83 ~mult(x0,rd(x1,x1))=x0),
% 45.76/6.83 inference(cnf_transformation,[status(thm)],[f6])).
% 45.76/6.83 fof(f18,plain,(
% 45.76/6.83 ![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)))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f11,f11])).
% 45.76/6.83 fof(f20,plain,(
% 45.76/6.83 ![X0,X1,X2]: (mult(mult(X0,X1),rd(X0,X2))=mult(rd(X0,X2),mult(X2,mult(X1,rd(X0,X2)))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f9,f11])).
% 45.76/6.83 fof(f21,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(mult(X0,mult(X1,mult(X2,X0))),X0)=mult(mult(X0,X1),X2))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f11,f10])).
% 45.76/6.83 fof(f24,plain,(
% 45.76/6.83 ![X0,X1,X2]: (mult(mult(X0,rd(X1,rd(X0,X2))),rd(X0,X2))=mult(rd(X0,X2),mult(X2,X1)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f9,f20])).
% 45.76/6.83 fof(f27,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(mult(mult(X0,X1),rd(X0,X2)),mult(X2,mult(X1,rd(X0,X2))))=rd(X0,X2))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f20,f10])).
% 45.76/6.83 fof(f38,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(mult(rd(X0,X1),mult(X1,X2)),rd(X0,X1))=mult(X0,rd(X2,rd(X0,X1))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f24,f10])).
% 45.76/6.83 fof(f54,plain,(
% 45.76/6.83 ![X0,X1,X2]: (mult(mult(X0,mult(X1,X2)),mult(X0,X1))=mult(mult(X0,X1),mult(rd(X2,X0),mult(X0,mult(X0,X1)))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f9,f18])).
% 45.76/6.83 fof(f84,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(mult(X0,mult(X1,X2)),rd(mult(X0,X1),X1))=mult(mult(X0,X1),rd(X2,rd(mult(X0,X1),X1))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f10,f38])).
% 45.76/6.83 fof(f101,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(mult(X0,mult(X1,X2)),X0)=mult(mult(X0,X1),rd(X2,rd(mult(X0,X1),X1))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f10,f84])).
% 45.76/6.83 fof(f102,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(mult(X0,mult(X1,X2)),X0)=mult(mult(X0,X1),rd(X2,X0)))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f10,f101])).
% 45.76/6.83 fof(f131,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(rd(mult(X0,mult(X1,X2)),X0),rd(X2,X0))=mult(X0,X1))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f102,f10])).
% 45.76/6.83 fof(f137,plain,(
% 45.76/6.83 ![X0,X1]: (rd(mult(X0,X1),rd(X1,mult(X0,X1)))=mult(mult(X0,X1),X0))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f10,f131])).
% 45.76/6.83 fof(f147,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(rd(mult(X0,X1),X0),rd(X2,X0))=mult(X0,rd(X1,X2)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f9,f131])).
% 45.76/6.83 fof(f188,plain,(
% 45.76/6.83 ![X0,X1]: (rd(X0,rd(X1,X0))=mult(X0,rd(X0,X1)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f10,f147])).
% 45.76/6.83 fof(f194,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(rd(X0,rd(X0,X1)),rd(X2,rd(X0,X1)))=mult(rd(X0,X1),rd(X1,X2)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f9,f147])).
% 45.76/6.83 fof(f243,plain,(
% 45.76/6.83 ![X0,X1]: (rd(rd(X0,rd(X1,X0)),rd(X0,X1))=X0)),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f188,f10])).
% 45.76/6.83 fof(f248,plain,(
% 45.76/6.83 ![X0,X1]: (rd(rd(rd(X0,X1),X0),rd(rd(X0,X1),rd(X0,rd(X1,X0))))=rd(X0,X1))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f243,f243])).
% 45.76/6.83 fof(f250,plain,(
% 45.76/6.83 ![X0,X1]: (rd(rd(X0,X1),rd(X0,mult(X1,X0)))=X0)),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f10,f243])).
% 45.76/6.83 fof(f257,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(rd(mult(rd(X0,X1),X2),rd(X0,X1)),X0)=mult(rd(X0,X1),rd(X2,rd(X0,rd(X1,X0)))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f243,f147])).
% 45.76/6.83 fof(f288,plain,(
% 45.76/6.83 ![X0,X1]: (rd(X0,rd(mult(X0,X1),mult(X1,mult(X0,X1))))=mult(X0,X1))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f10,f250])).
% 45.76/6.83 fof(f298,plain,(
% 45.76/6.83 ![X0,X1]: (rd(rd(rd(X0,mult(X1,X0)),X0),rd(rd(X0,mult(X1,X0)),rd(X0,X1)))=rd(X0,mult(X1,X0)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f250,f243])).
% 45.76/6.83 fof(f299,plain,(
% 45.76/6.83 ![X0,X1]: (rd(rd(X0,X1),rd(rd(X0,mult(X1,X0)),rd(X0,X1)))=mult(rd(X0,X1),X0))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f250,f188])).
% 45.76/6.83 fof(f419,plain,(
% 45.76/6.83 ![X0,X1]: (rd(mult(X0,X1),rd(rd(X1,mult(X0,X1)),mult(X0,X1)))=mult(mult(X0,X1),mult(mult(X0,X1),X0)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f137,f188])).
% 45.76/6.83 fof(f627,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(rd(rd(X0,X1),X0),rd(X2,rd(rd(X0,X1),rd(X0,mult(X1,X0)))))=mult(rd(rd(X0,X1),rd(X0,mult(X1,X0))),rd(rd(X0,mult(X1,X0)),X2)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f250,f194])).
% 45.76/6.83 fof(f635,plain,(
% 45.76/6.83 ![X0,X1]: (rd(rd(X0,rd(X0,mult(X1,X0))),X0)=mult(rd(X0,mult(X1,X0)),rd(mult(X1,X0),rd(X0,X1))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f250,f194])).
% 45.76/6.83 fof(f672,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(rd(rd(X0,X1),X0),rd(X2,X0))=mult(rd(rd(X0,X1),rd(X0,mult(X1,X0))),rd(rd(X0,mult(X1,X0)),X2)))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f250,f627])).
% 45.76/6.83 fof(f673,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(rd(rd(X0,X1),X0),rd(X2,X0))=mult(X0,rd(rd(X0,mult(X1,X0)),X2)))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f250,f672])).
% 45.76/6.83 fof(f866,plain,(
% 45.76/6.83 ![X0,X1,X2,X3]: (rd(mult(mult(X0,X1),X2),rd(X3,X0))=mult(X0,rd(mult(X1,mult(X2,X0)),X3)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f21,f147])).
% 45.76/6.83 fof(f936,plain,(
% 45.76/6.83 ![X0,X1]: (ld(rd(X0,X1),X0)=X1)),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f9,f8])).
% 45.76/6.83 fof(f942,plain,(
% 45.76/6.83 ![X0,X1]: (ld(X0,rd(X0,X1))=rd(X0,mult(X1,X0)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f250,f936])).
% 45.76/6.83 fof(f947,plain,(
% 45.76/6.83 ![X0,X1]: (ld(mult(X0,X1),X0)=rd(mult(X0,X1),mult(X1,mult(X0,X1))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f288,f936])).
% 45.76/6.83 fof(f978,plain,(
% 45.76/6.83 ![X0,X1]: (rd(mult(X0,ld(X0,X1)),rd(ld(X0,X1),X1))=mult(mult(X0,ld(X0,X1)),X0))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f7,f137])).
% 45.76/6.83 fof(f986,plain,(
% 45.76/6.83 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(X2,mult(ld(X2,X0),mult(X1,X2))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f7,f11])).
% 45.76/6.83 fof(f987,plain,(
% 45.76/6.83 ![X0,X1]: (rd(X0,ld(X1,X0))=X1)),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f7,f10])).
% 45.76/6.83 fof(f994,plain,(
% 45.76/6.83 ![X0,X1]: (rd(X0,rd(ld(X1,X0),X0))=mult(mult(X1,ld(X1,X0)),X1))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f7,f978])).
% 45.76/6.83 fof(f996,plain,(
% 45.76/6.83 ![X0,X1]: (rd(X0,rd(ld(X1,X0),X0))=mult(X0,X1))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f7,f994])).
% 45.76/6.83 fof(f1008,plain,(
% 45.76/6.83 ![X0,X1]: (ld(rd(X0,X1),X0)=rd(rd(X0,X1),mult(rd(X0,mult(X1,X0)),rd(X0,X1))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f250,f942])).
% 45.76/6.83 fof(f1020,plain,(
% 45.76/6.83 ![X0,X1]: (X0=rd(rd(X1,X0),mult(rd(X1,mult(X0,X1)),rd(X1,X0))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f936,f1008])).
% 45.76/6.83 fof(f1250,plain,(
% 45.76/6.83 ![X0,X1]: (ld(X0,rd(X1,X0))=mult(rd(X1,mult(X0,X1)),rd(X1,X0)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f1020,f936])).
% 45.76/6.83 fof(f1257,plain,(
% 45.76/6.83 ![X0,X1]: (rd(rd(mult(rd(X0,mult(X1,X0)),rd(X0,X1)),X1),rd(mult(rd(X0,mult(X1,X0)),rd(X0,X1)),rd(X0,X1)))=mult(rd(X0,mult(X1,X0)),rd(X0,X1)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f1020,f243])).
% 45.76/6.83 fof(f1347,plain,(
% 45.76/6.83 ![X0,X1]: (rd(rd(ld(X0,rd(X1,X0)),X0),rd(mult(rd(X1,mult(X0,X1)),rd(X1,X0)),rd(X1,X0)))=mult(rd(X1,mult(X0,X1)),rd(X1,X0)))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f1250,f1257])).
% 45.76/6.83 fof(f1348,plain,(
% 45.76/6.83 ![X0,X1]: (rd(rd(ld(X0,rd(X1,X0)),X0),rd(X1,mult(X0,X1)))=mult(rd(X1,mult(X0,X1)),rd(X1,X0)))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f10,f1347])).
% 45.76/6.83 fof(f1349,plain,(
% 45.76/6.83 ![X0,X1]: (rd(rd(ld(X0,rd(X1,X0)),X0),rd(X1,mult(X0,X1)))=ld(X0,rd(X1,X0)))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f1250,f1348])).
% 45.76/6.83 fof(f1373,plain,(
% 45.76/6.83 ![X0,X1]: (ld(X0,rd(mult(X1,X0),X0))=mult(ld(mult(X1,X0),X1),rd(mult(X1,X0),X0)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f947,f1250])).
% 45.76/6.83 fof(f1381,plain,(
% 45.76/6.83 ![X0,X1]: (ld(rd(X0,X1),rd(X1,rd(X0,X1)))=mult(rd(X1,X0),rd(X1,rd(X0,X1))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f9,f1250])).
% 45.76/6.83 fof(f1411,plain,(
% 45.76/6.83 ![X0,X1]: (ld(X0,X1)=mult(ld(mult(X1,X0),X1),rd(mult(X1,X0),X0)))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f10,f1373])).
% 45.76/6.83 fof(f1412,plain,(
% 45.76/6.83 ![X0,X1]: (ld(X0,X1)=mult(ld(mult(X1,X0),X1),X1))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f10,f1411])).
% 45.76/6.83 fof(f1507,plain,(
% 45.76/6.83 ![X0,X1]: (rd(ld(X0,X1),X1)=ld(mult(X1,X0),X1))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f1412,f10])).
% 45.76/6.83 fof(f1853,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(X0,X1),mult(rd(X1,X0),rd(X1,rd(X0,X1))))=rd(X1,rd(X0,X1)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f1381,f7])).
% 45.76/6.83 fof(f1918,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(rd(X0,mult(X1,X0)),rd(X0,X1)),mult(X0,rd(rd(X0,X1),rd(rd(X0,mult(X1,X0)),rd(X0,X1)))))=rd(rd(X0,X1),rd(rd(X0,mult(X1,X0)),rd(X0,X1))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f250,f1853])).
% 45.76/6.83 fof(f1999,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(rd(X0,mult(X1,X0)),rd(X0,X1)),mult(X0,mult(rd(X0,X1),X0)))=rd(rd(X0,X1),rd(rd(X0,mult(X1,X0)),rd(X0,X1))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f299,f1918])).
% 45.76/6.83 fof(f2000,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(rd(X0,mult(X1,X0)),rd(X0,X1)),mult(X0,mult(rd(X0,X1),X0)))=mult(rd(X0,X1),X0))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f299,f1999])).
% 45.76/6.83 fof(f2091,plain,(
% 45.76/6.83 ![X0]: (rd(rd(rd(rd(X0,X0),X0),rd(X0,X0)),rd(X0,X0))=rd(rd(X0,X0),X0))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f248,f248])).
% 45.76/6.83 fof(f2275,plain,(
% 45.76/6.83 ![X0]: (ld(rd(rd(rd(rd(X0,X0),X0),rd(X0,X0)),rd(X0,X0)),rd(rd(X0,X0),rd(rd(X0,X0),X0)))=mult(rd(rd(X0,X0),rd(rd(rd(X0,X0),X0),rd(X0,X0))),rd(rd(X0,X0),rd(rd(rd(rd(X0,X0),X0),rd(X0,X0)),rd(X0,X0)))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f2091,f1381])).
% 45.76/6.83 fof(f2289,plain,(
% 45.76/6.83 ![X0]: (rd(rd(rd(X0,X0),rd(rd(X0,X0),X0)),rd(rd(X0,X0),rd(rd(rd(X0,X0),X0),rd(X0,X0))))=rd(X0,X0))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f2091,f243])).
% 45.76/6.83 fof(f2297,plain,(
% 45.76/6.83 ![X0]: (mult(rd(rd(X0,X0),X0),rd(X0,X0))=rd(rd(rd(X0,X0),X0),rd(X0,X0)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f2091,f9])).
% 45.76/6.83 fof(f2325,plain,(
% 45.76/6.83 ![X0]: (ld(rd(rd(X0,X0),X0),rd(rd(X0,X0),rd(rd(X0,X0),X0)))=mult(rd(rd(X0,X0),rd(rd(rd(X0,X0),X0),rd(X0,X0))),rd(rd(X0,X0),rd(rd(rd(rd(X0,X0),X0),rd(X0,X0)),rd(X0,X0)))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f2091,f2275])).
% 45.76/6.83 fof(f2327,plain,(
% 45.76/6.83 ![X0]: (ld(rd(rd(X0,X0),X0),rd(rd(X0,X0),rd(rd(X0,X0),X0)))=mult(rd(rd(X0,X0),rd(rd(rd(X0,X0),X0),rd(X0,X0))),rd(rd(X0,X0),rd(rd(X0,X0),X0))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f2091,f2325])).
% 45.76/6.83 fof(f2384,plain,(
% 45.76/6.83 ![X0,X1]: (rd(mult(rd(X0,rd(rd(X1,X1),X1)),rd(rd(rd(X1,X1),X1),rd(X1,X1))),rd(X0,rd(rd(X1,X1),X1)))=mult(X0,rd(rd(X1,X1),rd(X0,rd(rd(X1,X1),X1)))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f2297,f38])).
% 45.76/6.83 fof(f2640,plain,(
% 45.76/6.83 ![X0,X1,X2]: (ld(X0,mult(mult(X1,X2),X0))=mult(ld(X0,X1),mult(X2,X0)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f986,f8])).
% 45.76/6.83 fof(f3003,plain,(
% 45.76/6.83 ![X0,X1,X2]: (rd(mult(rd(X0,rd(X1,X0)),rd(X0,X2)),mult(X2,mult(rd(X0,X1),rd(X0,X2))))=rd(X0,X2))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f188,f27])).
% 45.76/6.83 fof(f3023,plain,(
% 45.76/6.83 ![X0]: (rd(mult(mult(X0,rd(rd(X0,X0),X0)),rd(X0,X0)),mult(X0,rd(rd(rd(X0,X0),X0),rd(X0,X0))))=rd(X0,X0))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f2297,f27])).
% 45.76/6.83 fof(f3118,plain,(
% 45.76/6.83 ![X0]: (rd(rd(mult(X0,mult(rd(rd(X0,X0),X0),X0)),X0),mult(X0,rd(rd(rd(X0,X0),X0),rd(X0,X0))))=rd(X0,X0))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f102,f3023])).
% 45.76/6.83 fof(f3119,plain,(
% 45.76/6.83 ![X0]: (rd(rd(mult(X0,rd(X0,X0)),X0),mult(X0,rd(rd(rd(X0,X0),X0),rd(X0,X0))))=rd(X0,X0))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f9,f3118])).
% 45.76/6.83 fof(f3120,plain,(
% 45.76/6.83 ![X0]: (rd(rd(rd(X0,rd(X0,X0)),X0),mult(X0,rd(rd(rd(X0,X0),X0),rd(X0,X0))))=rd(X0,X0))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f188,f3119])).
% 45.76/6.83 fof(f3773,plain,(
% 45.76/6.83 ![X0,X1,X2]: (ld(mult(X0,X1),mult(mult(X0,mult(X1,X2)),mult(X0,X1)))=mult(rd(X2,X0),mult(X0,mult(X0,X1))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f54,f8])).
% 45.76/6.83 fof(f3872,plain,(
% 45.76/6.83 ![X0,X1,X2]: (mult(ld(mult(X0,X1),X0),mult(mult(X1,X2),mult(X0,X1)))=mult(rd(X2,X0),mult(X0,mult(X0,X1))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f2640,f3773])).
% 45.76/6.83 fof(f3873,plain,(
% 45.76/6.83 ![X0,X1,X2]: (mult(rd(ld(X0,X1),X1),mult(mult(X0,X2),mult(X1,X0)))=mult(rd(X2,X1),mult(X1,mult(X1,X0))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f1507,f3872])).
% 45.76/6.83 fof(f5304,plain,(
% 45.76/6.83 ![X0]: (rd(rd(rd(X0,X0),rd(rd(X0,X0),mult(rd(rd(X0,X0),X0),rd(X0,X0)))),rd(X0,X0))=mult(rd(rd(X0,X0),rd(rd(rd(X0,X0),X0),rd(X0,X0))),rd(mult(rd(rd(X0,X0),X0),rd(X0,X0)),rd(rd(X0,X0),rd(rd(X0,X0),X0)))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f2297,f635])).
% 45.76/6.83 fof(f5398,plain,(
% 45.76/6.83 ![X0]: (rd(rd(rd(X0,X0),rd(rd(X0,X0),rd(rd(rd(X0,X0),X0),rd(X0,X0)))),rd(X0,X0))=mult(rd(rd(X0,X0),rd(rd(rd(X0,X0),X0),rd(X0,X0))),rd(mult(rd(rd(X0,X0),X0),rd(X0,X0)),rd(rd(X0,X0),rd(rd(X0,X0),X0)))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f2297,f5304])).
% 45.76/6.83 fof(f5399,plain,(
% 45.76/6.83 ![X0]: (rd(rd(rd(X0,X0),rd(rd(X0,X0),rd(rd(rd(X0,X0),X0),rd(X0,X0)))),rd(X0,X0))=mult(rd(rd(X0,X0),rd(rd(rd(X0,X0),X0),rd(X0,X0))),rd(rd(rd(rd(X0,X0),X0),rd(X0,X0)),rd(rd(X0,X0),rd(rd(X0,X0),X0)))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f2297,f5398])).
% 45.76/6.83 fof(f6118,plain,(
% 45.76/6.83 ![X0]: (mult(rd(rd(X0,mult(X0,X0)),rd(X0,X0)),mult(X0,X0))=mult(rd(X0,X0),X0))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f9,f2000])).
% 45.76/6.83 fof(f6281,plain,(
% 45.76/6.83 ![X0]: (mult(rd(rd(X0,mult(X0,X0)),rd(X0,X0)),mult(X0,X0))=X0)),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f9,f6118])).
% 45.76/6.83 fof(f6499,plain,(
% 45.76/6.83 ![X0]: (rd(X0,mult(X0,X0))=rd(rd(X0,mult(X0,X0)),rd(X0,X0)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f6281,f10])).
% 45.76/6.83 fof(f6668,plain,(
% 45.76/6.83 ![X0]: (rd(rd(rd(X0,mult(X0,X0)),rd(rd(X0,mult(X0,X0)),mult(rd(X0,X0),rd(X0,mult(X0,X0))))),rd(X0,mult(X0,X0)))=mult(rd(rd(X0,mult(X0,X0)),mult(rd(X0,X0),rd(X0,mult(X0,X0)))),rd(mult(rd(X0,X0),rd(X0,mult(X0,X0))),rd(X0,mult(X0,X0)))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f6499,f635])).
% 45.76/6.83 fof(f6701,plain,(
% 45.76/6.83 ![X0]: (ld(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))=rd(rd(X0,mult(X0,X0)),mult(rd(X0,X0),rd(X0,mult(X0,X0)))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f6499,f942])).
% 45.76/6.83 fof(f6702,plain,(
% 45.76/6.83 ![X0]: (ld(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))=rd(X0,X0))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f6499,f936])).
% 45.76/6.83 fof(f6747,plain,(
% 45.76/6.83 ![X0]: (rd(rd(rd(X0,mult(X0,X0)),rd(rd(X0,mult(X0,X0)),mult(rd(X0,X0),rd(X0,mult(X0,X0))))),rd(X0,mult(X0,X0)))=mult(rd(rd(X0,mult(X0,X0)),mult(rd(X0,X0),rd(X0,mult(X0,X0)))),rd(X0,X0)))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f10,f6668])).
% 45.76/6.83 fof(f6846,plain,(
% 45.76/6.83 ![X0]: (rd(rd(rd(X0,mult(X0,X0)),rd(rd(X0,mult(X0,X0)),mult(rd(X0,X0),rd(X0,mult(X0,X0))))),rd(X0,mult(X0,X0)))=mult(ld(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0))),rd(X0,X0)))),
% 45.76/6.83 inference(backward_demodulation,[status(thm)],[f6701,f6747])).
% 45.76/6.83 fof(f6849,plain,(
% 45.76/6.83 ![X0]: (rd(X0,X0)=rd(rd(X0,mult(X0,X0)),mult(rd(X0,X0),rd(X0,mult(X0,X0)))))),
% 45.76/6.83 inference(backward_demodulation,[status(thm)],[f6702,f6701])).
% 45.76/6.83 fof(f6890,plain,(
% 45.76/6.83 ![X0]: (rd(rd(rd(X0,mult(X0,X0)),ld(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))),rd(X0,mult(X0,X0)))=mult(ld(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0))),rd(X0,X0)))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f6701,f6846])).
% 45.76/6.83 fof(f6891,plain,(
% 45.76/6.83 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))=mult(ld(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0))),rd(X0,X0)))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f987,f6890])).
% 45.76/6.83 fof(f6894,plain,(
% 45.76/6.83 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))=mult(rd(X0,X0),rd(X0,X0)))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f6702,f6891])).
% 45.76/6.83 fof(f7128,plain,(
% 45.76/6.83 ![X0]: (mult(mult(rd(X0,X0),rd(X0,X0)),rd(X0,mult(X0,X0)))=rd(X0,mult(X0,X0)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f6894,f9])).
% 45.76/6.83 fof(f8431,plain,(
% 45.76/6.83 ![X0]: (mult(mult(X0,mult(rd(X0,X0),rd(X0,X0))),rd(X0,mult(X0,X0)))=mult(rd(X0,mult(X0,X0)),mult(mult(X0,X0),rd(X0,mult(X0,X0)))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f7128,f20])).
% 45.76/6.83 fof(f10361,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(ld(rd(X0,X0),rd(rd(X0,X0),X0)),rd(rd(X0,X0),X0)),mult(mult(rd(X0,X0),X1),rd(rd(rd(X0,X0),X0),rd(X0,X0))))=mult(rd(X1,rd(rd(X0,X0),X0)),mult(rd(rd(X0,X0),X0),mult(rd(rd(X0,X0),X0),rd(X0,X0)))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f2297,f3873])).
% 45.76/6.83 fof(f10460,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(rd(rd(X0,X0),mult(X0,rd(X0,X0))),rd(rd(X0,X0),X0)),mult(mult(rd(X0,X0),X1),rd(rd(rd(X0,X0),X0),rd(X0,X0))))=mult(rd(X1,rd(rd(X0,X0),X0)),mult(rd(rd(X0,X0),X0),mult(rd(rd(X0,X0),X0),rd(X0,X0)))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f942,f10361])).
% 45.76/6.83 fof(f10461,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(rd(rd(X0,X0),rd(X0,rd(X0,X0))),rd(rd(X0,X0),X0)),mult(mult(rd(X0,X0),X1),rd(rd(rd(X0,X0),X0),rd(X0,X0))))=mult(rd(X1,rd(rd(X0,X0),X0)),mult(rd(rd(X0,X0),X0),mult(rd(rd(X0,X0),X0),rd(X0,X0)))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f188,f10460])).
% 45.76/6.83 fof(f10462,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(X0,X0),mult(mult(rd(X0,X0),X1),rd(rd(rd(X0,X0),X0),rd(X0,X0))))=mult(rd(X1,rd(rd(X0,X0),X0)),mult(rd(rd(X0,X0),X0),mult(rd(rd(X0,X0),X0),rd(X0,X0)))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f243,f10461])).
% 45.76/6.83 fof(f10463,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(X0,X0),rd(mult(rd(X0,X0),mult(X1,rd(rd(X0,X0),X0))),rd(X0,X0)))=mult(rd(X1,rd(rd(X0,X0),X0)),mult(rd(rd(X0,X0),X0),mult(rd(rd(X0,X0),X0),rd(X0,X0)))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f102,f10462])).
% 45.76/6.83 fof(f10464,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(X0,X0),rd(mult(rd(X0,X0),mult(X1,rd(rd(X0,X0),X0))),rd(X0,X0)))=mult(rd(X1,rd(rd(X0,X0),X0)),mult(rd(rd(X0,X0),X0),rd(rd(rd(X0,X0),X0),rd(X0,X0)))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f2297,f10463])).
% 45.76/6.83 fof(f10466,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(X0,X0),rd(mult(rd(X0,X0),mult(X1,rd(rd(X0,X0),X0))),rd(X0,X0)))=mult(rd(X1,rd(rd(X0,X0),X0)),rd(rd(rd(X0,X0),X0),rd(rd(X0,X0),rd(rd(X0,X0),X0)))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f188,f10464])).
% 45.76/6.83 fof(f11082,plain,(
% 45.76/6.83 ![X0]: (rd(X0,mult(X0,mult(rd(X0,X0),rd(X0,X0))))=rd(X0,X0))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f9,f3003])).
% 45.76/6.83 fof(f11572,plain,(
% 45.76/6.83 ![X0]: (rd(rd(X0,mult(X0,X0)),mult(rd(X0,mult(X0,X0)),mult(mult(rd(X0,X0),rd(X0,X0)),rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0))))))=rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f6894,f11082])).
% 45.76/6.83 fof(f11626,plain,(
% 45.76/6.83 ![X0]: (ld(rd(X0,X0),X0)=mult(X0,mult(rd(X0,X0),rd(X0,X0))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f11082,f936])).
% 45.76/6.83 fof(f11644,plain,(
% 45.76/6.83 ![X0]: (rd(rd(X0,mult(X0,X0)),mult(rd(X0,mult(X0,X0)),mult(mult(rd(X0,X0),rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0)))))=rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f6894,f11572])).
% 45.76/6.83 fof(f11645,plain,(
% 45.76/6.83 ![X0]: (rd(rd(X0,mult(X0,X0)),mult(rd(X0,mult(X0,X0)),mult(mult(rd(X0,X0),rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0)))))=mult(rd(X0,X0),rd(X0,X0)))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f6894,f11644])).
% 45.76/6.83 fof(f11823,plain,(
% 45.76/6.83 ![X0]: (mult(X0,rd(X0,mult(X0,X0)))=mult(rd(X0,mult(X0,X0)),mult(mult(X0,X0),rd(X0,mult(X0,X0)))))),
% 45.76/6.83 inference(backward_demodulation,[status(thm)],[f11824,f8431])).
% 45.76/6.83 fof(f11824,plain,(
% 45.76/6.83 ![X0]: (X0=mult(X0,mult(rd(X0,X0),rd(X0,X0))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f936,f11626])).
% 45.76/6.83 fof(f11942,plain,(
% 45.76/6.83 ![X0]: (rd(X0,rd(mult(X0,X0),X0))=mult(rd(X0,mult(X0,X0)),mult(mult(X0,X0),rd(X0,mult(X0,X0)))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f188,f11823])).
% 45.76/6.83 fof(f11944,plain,(
% 45.76/6.83 ![X0]: (rd(X0,X0)=mult(rd(X0,mult(X0,X0)),mult(mult(X0,X0),rd(X0,mult(X0,X0)))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f10,f11942])).
% 45.76/6.83 fof(f11947,plain,(
% 45.76/6.83 ![X0]: (rd(X0,mult(X0,X0))=mult(rd(X0,mult(X0,X0)),mult(mult(rd(X0,X0),rd(X0,X0)),rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0))))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f6894,f11824])).
% 45.76/6.83 fof(f12000,plain,(
% 45.76/6.83 ![X0]: (ld(X0,X0)=mult(rd(X0,X0),rd(X0,X0)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f11824,f8])).
% 45.76/6.83 fof(f12016,plain,(
% 45.76/6.83 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))=mult(rd(X0,X0),rd(X0,X0)))),
% 45.76/6.83 inference(backward_demodulation,[status(thm)],[f12017,f11645])).
% 45.76/6.83 fof(f12017,plain,(
% 45.76/6.83 ![X0]: (rd(X0,mult(X0,X0))=mult(rd(X0,mult(X0,X0)),mult(mult(rd(X0,X0),rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0)))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f6894,f11947])).
% 45.76/6.83 fof(f12115,plain,(
% 45.76/6.83 ![X0]: (mult(ld(X0,X0),rd(X0,mult(X0,X0)))=rd(X0,mult(X0,X0)))),
% 45.76/6.83 inference(backward_demodulation,[status(thm)],[f12000,f7128])).
% 45.76/6.83 fof(f12244,plain,(
% 45.76/6.83 ![X0]: (rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))=ld(X0,X0))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f12000,f12016])).
% 45.76/6.83 fof(f12538,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(ld(rd(X0,X0),rd(X0,X0)),rd(X0,X0)),mult(mult(rd(X0,X0),X1),ld(X0,X0)))=mult(rd(X1,rd(X0,X0)),mult(rd(X0,X0),mult(rd(X0,X0),rd(X0,X0)))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f12000,f3873])).
% 45.76/6.83 fof(f12572,plain,(
% 45.76/6.83 ![X0]: (rd(ld(rd(X0,X0),rd(X0,X0)),rd(X0,X0))=ld(ld(X0,X0),rd(X0,X0)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f12000,f1507])).
% 45.76/6.83 fof(f12575,plain,(
% 45.76/6.83 ![X0,X1]: (rd(mult(rd(X0,X0),mult(X1,ld(X0,X0))),rd(X0,X0))=mult(mult(rd(X0,X0),X1),rd(X0,X0)))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f12000,f21])).
% 45.76/6.83 fof(f12582,plain,(
% 45.76/6.83 ![X0,X1]: (rd(mult(rd(X0,X0),mult(rd(X0,X0),X1)),rd(X0,X0))=mult(ld(X0,X0),rd(X1,rd(X0,X0))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f12000,f102])).
% 45.76/6.83 fof(f12620,plain,(
% 45.76/6.83 ![X0,X1]: (mult(rd(ld(rd(X0,X0),rd(X0,X0)),rd(X0,X0)),mult(mult(rd(X0,X0),X1),ld(X0,X0)))=mult(rd(X1,rd(X0,X0)),mult(rd(X0,X0),ld(X0,X0))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f12000,f12538])).
% 45.76/6.83 fof(f12683,plain,(
% 45.76/6.83 ![X0,X1]: (mult(ld(ld(X0,X0),rd(X0,X0)),mult(mult(rd(X0,X0),X1),ld(X0,X0)))=mult(rd(X1,rd(X0,X0)),mult(rd(X0,X0),ld(X0,X0))))),
% 45.76/6.83 inference(backward_demodulation,[status(thm)],[f12572,f12620])).
% 45.76/6.83 fof(f12705,plain,(
% 45.76/6.83 ![X0]: (rd(rd(X0,X0),rd(X0,mult(X0,X0)))=mult(X0,rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f11944,f38])).
% 45.76/6.83 fof(f12763,plain,(
% 45.76/6.83 ![X0]: (X0=mult(X0,rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f250,f12705])).
% 45.76/6.83 fof(f12764,plain,(
% 45.76/6.83 ![X0]: (X0=rd(rd(rd(X0,X0),X0),rd(rd(X0,mult(X0,X0)),X0)))),
% 45.76/6.83 inference(forward_demodulation,[status(thm)],[f673,f12763])).
% 45.76/6.83 fof(f13198,plain,(
% 45.76/6.83 ![X0]: (mult(X0,rd(rd(X0,mult(X0,X0)),X0))=rd(rd(X0,X0),X0))),
% 45.76/6.83 inference(paramodulation,[status(thm)],[f12764,f9])).
% 45.76/6.83 fof(f13342,plain,(
% 45.76/6.83 ![X0]: (rd(rd(rd(X0,X0),rd(rd(X0,X0),rd(rd(rd(X0,X0),X0),rd(X0,X0)))),rd(X0,X0))=mult(rd(rd(X0,X0),rd(rd(rd(X0,X0),X0),rd(X0,X0))),rd(rd(rd(X0,X0),X0),rd(rd(X0,X0),rd(rd(X0,X0),X0)))))),
% 45.76/6.83 inference(backward_demodulation,[status(thm)],[f13372,f5399])).
% 45.76/6.83 fof(f13349,plain,(
% 45.76/6.83 ![X0]: (rd(rd(rd(X0,rd(X0,X0)),X0),mult(X0,rd(rd(X0,X0),X0)))=rd(X0,X0))),
% 45.76/6.83 inference(backward_demodulation,[status(thm)],[f13372,f3120])).
% 45.76/6.83 fof(f13357,plain,(
% 45.76/6.83 ![X0,X1]: (rd(mult(rd(X0,rd(rd(X1,X1),X1)),rd(rd(X1,X1),X1)),rd(X0,rd(rd(X1,X1),X1)))=mult(X0,rd(rd(X1,X1),rd(X0,rd(rd(X1,X1),X1)))))),
% 45.76/6.83 inference(backward_demodulation,[status(thm)],[f13372,f2384])).
% 45.76/6.83 fof(f13368,plain,(
% 45.76/6.83 ![X0]: (rd(rd(rd(X0,X0),rd(rd(X0,X0),X0)),rd(rd(X0,X0),rd(rd(X0,X0),X0)))=rd(X0,X0))),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f13372,f2289])).
% 45.76/6.84 fof(f13371,plain,(
% 45.76/6.84 ![X0]: (ld(rd(rd(X0,X0),X0),rd(rd(X0,X0),rd(rd(X0,X0),X0)))=mult(rd(rd(X0,X0),rd(rd(X0,X0),X0)),rd(rd(X0,X0),rd(rd(X0,X0),X0))))),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f13372,f2327])).
% 45.76/6.84 fof(f13372,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(X0,X0),X0),rd(X0,X0))=rd(rd(X0,X0),X0))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f673,f13198])).
% 45.76/6.84 fof(f13423,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(X0,X0),rd(rd(X0,X0),rd(rd(X0,X0),X0))),rd(X0,X0))=mult(rd(rd(X0,X0),rd(rd(rd(X0,X0),X0),rd(X0,X0))),rd(rd(rd(X0,X0),X0),rd(rd(X0,X0),rd(rd(X0,X0),X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13372,f13342])).
% 45.76/6.84 fof(f13424,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(X0,X0),rd(rd(X0,X0),rd(rd(X0,X0),X0))),rd(X0,X0))=mult(rd(rd(X0,X0),rd(rd(X0,X0),X0)),rd(rd(rd(X0,X0),X0),rd(rd(X0,X0),rd(rd(X0,X0),X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13372,f13423])).
% 45.76/6.84 fof(f13425,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(X0,X0),rd(rd(X0,X0),rd(rd(X0,X0),X0))),rd(X0,X0))=mult(rd(X0,X0),rd(mult(rd(X0,X0),mult(rd(X0,X0),rd(rd(X0,X0),X0))),rd(X0,X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f10466,f13424])).
% 45.76/6.84 fof(f13426,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(X0,X0),rd(rd(X0,X0),rd(rd(X0,X0),X0))),rd(X0,X0))=mult(rd(X0,X0),mult(ld(X0,X0),rd(rd(rd(X0,X0),X0),rd(X0,X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f12582,f13425])).
% 45.76/6.84 fof(f13427,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(X0,X0),rd(rd(X0,X0),rd(rd(X0,X0),X0))),rd(X0,X0))=mult(rd(X0,X0),mult(ld(X0,X0),rd(rd(X0,X0),X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13372,f13426])).
% 45.76/6.84 fof(f13434,plain,(
% 45.76/6.84 ![X0,X1]: (rd(X0,rd(X0,rd(rd(X1,X1),X1)))=mult(X0,rd(rd(X1,X1),rd(X0,rd(rd(X1,X1),X1)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f9,f13357])).
% 45.76/6.84 fof(f13446,plain,(
% 45.76/6.84 ![X0]: (mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0)))=rd(X0,X0))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f194,f13368])).
% 45.76/6.84 fof(f13483,plain,(
% 45.76/6.84 ![X0]: (rd(mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0))),rd(rd(rd(X0,rd(X0,X0)),mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0)))),rd(X0,X0)))=mult(mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0))),mult(mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0))),rd(rd(X0,X0),X0))))),
% 45.76/6.84 inference(paramodulation,[status(thm)],[f13446,f419])).
% 45.76/6.84 fof(f13491,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(X0,rd(X0,X0)),rd(rd(X0,rd(X0,X0)),mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0))))),rd(X0,rd(X0,X0)))=mult(rd(rd(X0,rd(X0,X0)),mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0)))),rd(rd(X0,X0),rd(rd(X0,rd(X0,X0)),rd(rd(X0,X0),X0)))))),
% 45.76/6.84 inference(paramodulation,[status(thm)],[f13446,f635])).
% 45.76/6.84 fof(f13493,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(rd(X0,rd(X0,X0)),mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0)))),rd(X0,rd(X0,X0))),rd(rd(rd(X0,rd(X0,X0)),rd(X0,X0)),rd(rd(X0,rd(X0,X0)),rd(rd(X0,X0),X0))))=rd(rd(X0,rd(X0,X0)),mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0)))))),
% 45.76/6.84 inference(paramodulation,[status(thm)],[f13446,f298])).
% 45.76/6.84 fof(f13507,plain,(
% 45.76/6.84 ![X0]: (ld(rd(rd(X0,X0),X0),rd(X0,X0))=rd(X0,rd(X0,X0)))),
% 45.76/6.84 inference(paramodulation,[status(thm)],[f13446,f8])).
% 45.76/6.84 fof(f13551,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),rd(rd(rd(X0,rd(X0,X0)),mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0)))),rd(X0,X0)))=mult(mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0))),mult(mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0))),rd(rd(X0,X0),X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13446,f13483])).
% 45.76/6.84 fof(f13552,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),rd(rd(rd(X0,rd(X0,X0)),rd(X0,X0)),rd(X0,X0)))=mult(mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0))),mult(mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0))),rd(rd(X0,X0),X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13446,f13551])).
% 45.76/6.84 fof(f13553,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),rd(X0,rd(X0,X0)))=mult(mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0))),mult(mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0))),rd(rd(X0,X0),X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f243,f13552])).
% 45.76/6.84 fof(f13554,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),rd(X0,rd(X0,X0)))=mult(rd(X0,X0),mult(mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0))),rd(rd(X0,X0),X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13446,f13553])).
% 45.76/6.84 fof(f13555,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),rd(X0,rd(X0,X0)))=mult(rd(X0,X0),mult(rd(X0,X0),rd(rd(X0,X0),X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13446,f13554])).
% 45.76/6.84 fof(f13556,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),rd(X0,rd(X0,X0)))=mult(rd(X0,X0),rd(rd(X0,X0),rd(X0,rd(X0,X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f188,f13555])).
% 45.76/6.84 fof(f13557,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),rd(X0,rd(X0,X0)))=rd(rd(mult(rd(X0,X0),rd(X0,X0)),rd(X0,X0)),X0))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f257,f13556])).
% 45.76/6.84 fof(f13572,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),rd(X0,rd(X0,X0)))=rd(rd(X0,X0),X0))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f10,f13557])).
% 45.76/6.84 fof(f13607,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(X0,rd(X0,X0)),rd(rd(X0,rd(X0,X0)),rd(X0,X0))),rd(X0,rd(X0,X0)))=mult(rd(rd(X0,rd(X0,X0)),mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0)))),rd(rd(X0,X0),rd(rd(X0,rd(X0,X0)),rd(rd(X0,X0),X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13446,f13491])).
% 45.76/6.84 fof(f13608,plain,(
% 45.76/6.84 ![X0]: (rd(mult(rd(X0,X0),rd(X0,rd(X0,rd(X0,X0)))),rd(X0,rd(X0,X0)))=mult(rd(rd(X0,rd(X0,X0)),mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0)))),rd(rd(X0,X0),rd(rd(X0,rd(X0,X0)),rd(rd(X0,X0),X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f194,f13607])).
% 45.76/6.84 fof(f13609,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(mult(rd(X0,X0),X0),rd(X0,X0)),X0),rd(X0,rd(X0,X0)))=mult(rd(rd(X0,rd(X0,X0)),mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0)))),rd(rd(X0,X0),rd(rd(X0,rd(X0,X0)),rd(rd(X0,X0),X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f257,f13608])).
% 45.76/6.84 fof(f13610,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(X0,rd(X0,X0)),X0),rd(X0,rd(X0,X0)))=mult(rd(rd(X0,rd(X0,X0)),mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0)))),rd(rd(X0,X0),rd(rd(X0,rd(X0,X0)),rd(rd(X0,X0),X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f9,f13609])).
% 45.76/6.84 fof(f13611,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(X0,rd(X0,X0)),X0),rd(X0,rd(X0,X0)))=mult(rd(rd(X0,rd(X0,X0)),rd(X0,X0)),rd(rd(X0,X0),rd(rd(X0,rd(X0,X0)),rd(rd(X0,X0),X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13446,f13610])).
% 45.76/6.84 fof(f13612,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(X0,rd(X0,X0)),X0),rd(X0,rd(X0,X0)))=mult(X0,rd(rd(X0,X0),rd(rd(X0,rd(X0,X0)),rd(rd(X0,X0),X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f243,f13611])).
% 45.76/6.84 fof(f13619,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(rd(X0,rd(X0,X0)),rd(X0,X0)),rd(X0,rd(X0,X0))),rd(rd(rd(X0,rd(X0,X0)),rd(X0,X0)),rd(rd(X0,rd(X0,X0)),rd(rd(X0,X0),X0))))=rd(rd(X0,rd(X0,X0)),mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13446,f13493])).
% 45.76/6.84 fof(f13620,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,rd(X0,rd(X0,X0))),rd(rd(rd(X0,rd(X0,X0)),rd(X0,X0)),rd(rd(X0,rd(X0,X0)),rd(rd(X0,X0),X0))))=rd(rd(X0,rd(X0,X0)),mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f243,f13619])).
% 45.76/6.84 fof(f13621,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,rd(X0,rd(X0,X0))),rd(X0,rd(rd(X0,rd(X0,X0)),rd(rd(X0,X0),X0))))=rd(rd(X0,rd(X0,X0)),mult(rd(rd(X0,X0),X0),rd(X0,rd(X0,X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f243,f13620])).
% 45.76/6.84 fof(f13622,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,rd(X0,rd(X0,X0))),rd(X0,rd(rd(X0,rd(X0,X0)),rd(rd(X0,X0),X0))))=rd(rd(X0,rd(X0,X0)),rd(X0,X0)))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13446,f13621])).
% 45.76/6.84 fof(f13623,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,rd(X0,rd(X0,X0))),rd(X0,rd(rd(X0,rd(X0,X0)),rd(rd(X0,X0),X0))))=X0)),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f243,f13622])).
% 45.76/6.84 fof(f13660,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,rd(X0,rd(X0,X0))),rd(X0,rd(X0,rd(rd(X0,X0),X0))))=X0)),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f13707,f13623])).
% 45.76/6.84 fof(f13661,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(X0,rd(X0,X0)),X0),rd(X0,rd(X0,X0)))=mult(X0,rd(rd(X0,X0),rd(X0,rd(rd(X0,X0),X0)))))),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f13707,f13612])).
% 45.76/6.84 fof(f13672,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),mult(X0,rd(rd(X0,X0),X0)))=rd(X0,X0))),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f13707,f13349])).
% 45.76/6.84 fof(f13707,plain,(
% 45.76/6.84 ![X0]: (X0=rd(X0,rd(X0,X0)))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f936,f13507])).
% 45.76/6.84 fof(f13798,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),rd(X0,rd(X0,rd(rd(X0,X0),X0))))=X0)),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13707,f13660])).
% 45.76/6.84 fof(f13799,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),rd(X0,rd(X0,X0)))=mult(X0,rd(rd(X0,X0),rd(X0,rd(rd(X0,X0),X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13707,f13661])).
% 45.76/6.84 fof(f13800,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),X0)=mult(X0,rd(rd(X0,X0),rd(X0,rd(rd(X0,X0),X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13572,f13799])).
% 45.76/6.84 fof(f13801,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),rd(rd(X0,X0),X0))=X0)),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f13803,f13798])).
% 45.76/6.84 fof(f13803,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),X0)=rd(X0,rd(X0,rd(rd(X0,X0),X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13434,f13800])).
% 45.76/6.84 fof(f13926,plain,(
% 45.76/6.84 ![X0]: (ld(rd(rd(X0,X0),X0),rd(rd(X0,X0),rd(rd(X0,X0),X0)))=mult(rd(rd(X0,X0),rd(rd(X0,X0),X0)),X0))),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f13801,f13371])).
% 45.76/6.84 fof(f13931,plain,(
% 45.76/6.84 ![X0]: (rd(rd(rd(X0,X0),X0),rd(X0,X0))=mult(rd(X0,X0),mult(ld(X0,X0),rd(rd(X0,X0),X0))))),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f13801,f13427])).
% 45.76/6.84 fof(f13942,plain,(
% 45.76/6.84 ![X0]: (ld(rd(rd(X0,X0),X0),X0)=mult(rd(rd(X0,X0),rd(rd(X0,X0),X0)),X0))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13801,f13926])).
% 45.76/6.84 fof(f13949,plain,(
% 45.76/6.84 ![X0]: (ld(rd(rd(X0,X0),X0),X0)=mult(X0,X0))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13801,f13942])).
% 45.76/6.84 fof(f13959,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),X0)=mult(rd(X0,X0),mult(ld(X0,X0),rd(rd(X0,X0),X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13372,f13931])).
% 45.76/6.84 fof(f13978,plain,(
% 45.76/6.84 ![X0]: (rd(X0,mult(X0,X0))=rd(rd(X0,X0),X0))),
% 45.76/6.84 inference(paramodulation,[status(thm)],[f13949,f987])).
% 45.76/6.84 fof(f13999,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),X0)=mult(rd(X0,X0),mult(ld(X0,X0),rd(X0,mult(X0,X0)))))),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f13978,f13959])).
% 45.76/6.84 fof(f14006,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),mult(X0,rd(X0,mult(X0,X0))))=rd(X0,X0))),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f13978,f13672])).
% 45.76/6.84 fof(f14146,plain,(
% 45.76/6.84 ![X0]: (rd(X0,mult(X0,X0))=mult(rd(X0,X0),mult(ld(X0,X0),rd(X0,mult(X0,X0)))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13978,f13999])).
% 45.76/6.84 fof(f14147,plain,(
% 45.76/6.84 ![X0]: (rd(X0,X0)=rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0))))),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f14189,f6849])).
% 45.76/6.84 fof(f14189,plain,(
% 45.76/6.84 ![X0]: (rd(X0,mult(X0,X0))=mult(rd(X0,X0),rd(X0,mult(X0,X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f12115,f14146])).
% 45.76/6.84 fof(f14197,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),rd(X0,rd(mult(X0,X0),X0)))=rd(X0,X0))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f188,f14006])).
% 45.76/6.84 fof(f14211,plain,(
% 45.76/6.84 ![X0]: (rd(rd(X0,X0),rd(X0,X0))=rd(X0,X0))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f10,f14197])).
% 45.76/6.84 fof(f14801,plain,(
% 45.76/6.84 ![X0]: (rd(X0,X0)=ld(X0,X0))),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f14147,f12244])).
% 45.76/6.84 fof(f15130,plain,(
% 45.76/6.84 ![X0,X1]: (mult(ld(ld(X0,X0),rd(X0,X0)),mult(mult(rd(X0,X0),X1),ld(X0,X0)))=mult(rd(X1,rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0))))),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f14801,f12683])).
% 45.76/6.84 fof(f15136,plain,(
% 45.76/6.84 ![X0,X1]: (rd(mult(rd(X0,X0),mult(X1,rd(X0,X0))),rd(X0,X0))=mult(mult(rd(X0,X0),X1),rd(X0,X0)))),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f14801,f12575])).
% 45.76/6.84 fof(f15500,plain,(
% 45.76/6.84 ![X0,X1]: (mult(ld(rd(X0,X0),rd(X0,X0)),mult(mult(rd(X0,X0),X1),ld(X0,X0)))=mult(rd(X1,rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f14801,f15130])).
% 45.76/6.84 fof(f15501,plain,(
% 45.76/6.84 ![X0,X1]: (mult(rd(rd(X0,X0),rd(X0,X0)),mult(mult(rd(X0,X0),X1),ld(X0,X0)))=mult(rd(X1,rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f14801,f15500])).
% 45.76/6.84 fof(f15502,plain,(
% 45.76/6.84 ![X0,X1]: (mult(rd(X0,X0),mult(mult(rd(X0,X0),X1),ld(X0,X0)))=mult(rd(X1,rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f14211,f15501])).
% 45.76/6.84 fof(f15503,plain,(
% 45.76/6.84 ![X0,X1]: (mult(rd(X0,X0),mult(mult(rd(X0,X0),X1),rd(X0,X0)))=mult(rd(X1,rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f14801,f15502])).
% 45.76/6.84 fof(f15504,plain,(
% 45.76/6.84 ![X0,X1]: (mult(rd(X0,X0),mult(mult(rd(X0,X0),X1),rd(X0,X0)))=mult(rd(X1,rd(X0,X0)),ld(X0,X0)))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f12000,f15503])).
% 45.76/6.84 fof(f15505,plain,(
% 45.76/6.84 ![X0,X1]: (mult(rd(X0,X0),mult(mult(rd(X0,X0),X1),rd(X0,X0)))=mult(rd(X1,rd(X0,X0)),rd(X0,X0)))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f14801,f15504])).
% 45.76/6.84 fof(f15506,plain,(
% 45.76/6.84 ![X0,X1]: (mult(rd(X0,X0),mult(mult(rd(X0,X0),X1),rd(X0,X0)))=X1)),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f9,f15505])).
% 45.76/6.84 fof(f22256,plain,(
% 45.76/6.84 ![X0,X1]: (rd(X0,rd(X1,rd(X0,X0)))=mult(rd(X0,X0),rd(X0,X1)))),
% 45.76/6.84 inference(paramodulation,[status(thm)],[f13707,f194])).
% 45.76/6.84 fof(f25761,plain,(
% 45.76/6.84 ![X0,X1]: (mult(rd(X0,X0),mult(mult(rd(rd(X0,X0),rd(X0,X0)),X1),rd(rd(X0,X0),rd(X0,X0))))=X1)),
% 45.76/6.84 inference(paramodulation,[status(thm)],[f14211,f15506])).
% 45.76/6.84 fof(f25765,plain,(
% 45.76/6.84 ![X0,X1]: (mult(rd(X0,X0),mult(X1,rd(X0,X0)))=mult(mult(rd(X0,X0),X1),rd(X0,X0)))),
% 45.76/6.84 inference(paramodulation,[status(thm)],[f15506,f15506])).
% 45.76/6.84 fof(f25774,plain,(
% 45.76/6.84 ![X0,X1]: (mult(rd(X0,X0),mult(X1,rd(X0,X0)))=ld(rd(X0,X0),X1))),
% 45.76/6.84 inference(paramodulation,[status(thm)],[f7,f15506])).
% 45.76/6.84 fof(f25794,plain,(
% 45.76/6.84 ![X0,X1]: (rd(mult(rd(X0,X0),X1),rd(X0,X0))=mult(mult(rd(X0,X0),rd(X0,X0)),mult(rd(X0,X0),X1)))),
% 45.76/6.84 inference(paramodulation,[status(thm)],[f15506,f21])).
% 45.76/6.84 fof(f25796,plain,(
% 45.76/6.84 ![X0,X1]: (mult(mult(rd(X0,X0),X1),mult(rd(X0,X0),rd(X0,X0)))=mult(mult(rd(X0,X0),rd(X0,X0)),mult(mult(rd(X0,X0),X1),mult(rd(X0,X0),mult(rd(X0,X0),rd(X0,X0))))))),
% 45.76/6.84 inference(paramodulation,[status(thm)],[f15506,f18])).
% 45.76/6.84 fof(f25827,plain,(
% 45.76/6.84 ![X0,X1]: (rd(rd(ld(rd(X0,X0),rd(mult(mult(rd(X0,X0),X1),rd(X0,X0)),rd(X0,X0))),rd(X0,X0)),rd(mult(mult(rd(X0,X0),X1),rd(X0,X0)),X1))=ld(rd(X0,X0),rd(mult(mult(rd(X0,X0),X1),rd(X0,X0)),rd(X0,X0))))),
% 45.76/6.84 inference(paramodulation,[status(thm)],[f15506,f1349])).
% 45.76/6.84 fof(f25850,plain,(
% 45.76/6.84 ![X0,X1]: (mult(rd(X0,X0),mult(mult(rd(X0,X0),X1),rd(rd(X0,X0),rd(X0,X0))))=X1)),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f14211,f25761])).
% 45.76/6.84 fof(f25851,plain,(
% 45.76/6.84 ![X0,X1]: (mult(rd(X0,X0),rd(mult(rd(X0,X0),mult(X1,rd(X0,X0))),rd(X0,X0)))=X1)),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f102,f25850])).
% 45.76/6.84 fof(f25852,plain,(
% 45.76/6.84 ![X0,X1]: (rd(mult(mult(rd(X0,X0),rd(X0,X0)),X1),rd(rd(X0,X0),rd(X0,X0)))=X1)),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f866,f25851])).
% 45.76/6.84 fof(f25853,plain,(
% 45.76/6.84 ![X0,X1]: (rd(mult(rd(X0,rd(X0,rd(X0,X0))),X1),rd(rd(X0,X0),rd(X0,X0)))=X1)),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f22256,f25852])).
% 45.76/6.84 fof(f25854,plain,(
% 45.76/6.84 ![X0,X1]: (rd(mult(rd(X0,X0),X1),rd(rd(X0,X0),rd(X0,X0)))=X1)),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13707,f25853])).
% 45.76/6.84 fof(f25859,plain,(
% 45.76/6.84 ![X0,X1]: (mult(X0,rd(X1,X1))=mult(mult(rd(X1,X1),X0),rd(X1,X1)))),
% 45.76/6.84 inference(backward_demodulation,[status(thm)],[f25866,f15136])).
% 45.76/6.84 fof(f25866,plain,(
% 45.76/6.84 ![X0,X1]: (rd(mult(rd(X0,X0),X1),rd(X0,X0))=X1)),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f14211,f25854])).
% 45.76/6.84 fof(f25980,plain,(
% 45.76/6.84 ![X0,X1]: (X0=mult(mult(rd(X1,X1),rd(X1,X1)),mult(rd(X1,X1),X0)))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f25866,f25794])).
% 45.76/6.84 fof(f25981,plain,(
% 45.76/6.84 ![X0,X1]: (X0=mult(rd(X1,rd(X1,rd(X1,X1))),mult(rd(X1,X1),X0)))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f22256,f25980])).
% 45.76/6.84 fof(f25989,plain,(
% 45.76/6.84 ![X0,X1]: (X0=mult(rd(X1,X1),mult(rd(X1,X1),X0)))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13707,f25981])).
% 45.76/6.84 fof(f25999,plain,(
% 45.76/6.84 ![X0,X1]: (mult(mult(rd(X0,X0),X1),rd(X0,rd(X0,rd(X0,X0))))=mult(mult(rd(X0,X0),rd(X0,X0)),mult(mult(rd(X0,X0),X1),mult(rd(X0,X0),mult(rd(X0,X0),rd(X0,X0))))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f22256,f25796])).
% 45.76/6.84 fof(f26000,plain,(
% 45.76/6.84 ![X0,X1]: (mult(mult(rd(X0,X0),X1),rd(X0,X0))=mult(mult(rd(X0,X0),rd(X0,X0)),mult(mult(rd(X0,X0),X1),mult(rd(X0,X0),mult(rd(X0,X0),rd(X0,X0))))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13707,f25999])).
% 45.76/6.84 fof(f26001,plain,(
% 45.76/6.84 ![X0,X1]: (mult(rd(X0,X0),mult(X1,rd(X0,X0)))=mult(mult(rd(X0,X0),rd(X0,X0)),mult(mult(rd(X0,X0),X1),mult(rd(X0,X0),mult(rd(X0,X0),rd(X0,X0))))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f25765,f26000])).
% 45.76/6.84 fof(f26002,plain,(
% 45.76/6.84 ![X0,X1]: (ld(rd(X0,X0),X1)=mult(mult(rd(X0,X0),rd(X0,X0)),mult(mult(rd(X0,X0),X1),mult(rd(X0,X0),mult(rd(X0,X0),rd(X0,X0))))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f25774,f26001])).
% 45.76/6.84 fof(f26003,plain,(
% 45.76/6.84 ![X0,X1]: (ld(rd(X0,X0),X1)=mult(rd(X0,rd(X0,rd(X0,X0))),mult(mult(rd(X0,X0),X1),mult(rd(X0,X0),mult(rd(X0,X0),rd(X0,X0))))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f22256,f26002])).
% 45.76/6.84 fof(f26004,plain,(
% 45.76/6.84 ![X0,X1]: (ld(rd(X0,X0),X1)=mult(rd(X0,X0),mult(mult(rd(X0,X0),X1),mult(rd(X0,X0),mult(rd(X0,X0),rd(X0,X0))))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f13707,f26003])).
% 45.76/6.84 fof(f26005,plain,(
% 45.76/6.84 ![X0,X1]: (ld(rd(X0,X0),X1)=mult(rd(X0,X0),mult(mult(rd(X0,X0),X1),rd(X0,X0))))),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f25989,f26004])).
% 45.76/6.84 fof(f26017,plain,(
% 45.76/6.84 ![X0,X1]: (ld(rd(X0,X0),X1)=X1)),
% 45.76/6.84 inference(forward_demodulation,[status(thm)],[f15506,f26005])).
% 45.76/6.84 fof(f26369,plain,(
% 45.76/6.84 ![X0,X1]: (rd(rd(rd(mult(mult(rd(X0,X0),X1),rd(X0,X0)),rd(X0,X0)),rd(X0,X0)),rd(mult(mult(rd(X0,X0),X1),rd(X0,X0)),X1))=ld(rd(X0,X0),rd(mult(mult(rd(X0,X0),X1),rd(X0,X0)),rd(X0,X0))))),
% 49.99/6.94 inference(forward_demodulation,[status(thm)],[f26017,f25827])).
% 49.99/6.94 fof(f26370,plain,(
% 49.99/6.94 ![X0,X1]: (rd(rd(mult(rd(X0,X0),X1),rd(X0,X0)),rd(mult(mult(rd(X0,X0),X1),rd(X0,X0)),X1))=ld(rd(X0,X0),rd(mult(mult(rd(X0,X0),X1),rd(X0,X0)),rd(X0,X0))))),
% 49.99/6.94 inference(forward_demodulation,[status(thm)],[f10,f26369])).
% 49.99/6.94 fof(f26371,plain,(
% 49.99/6.94 ![X0,X1]: (rd(X0,rd(mult(mult(rd(X1,X1),X0),rd(X1,X1)),X0))=ld(rd(X1,X1),rd(mult(mult(rd(X1,X1),X0),rd(X1,X1)),rd(X1,X1))))),
% 49.99/6.94 inference(forward_demodulation,[status(thm)],[f25866,f26370])).
% 49.99/6.94 fof(f26372,plain,(
% 49.99/6.94 ![X0,X1]: (rd(X0,rd(mult(rd(X1,X1),mult(X0,rd(X1,X1))),X0))=ld(rd(X1,X1),rd(mult(mult(rd(X1,X1),X0),rd(X1,X1)),rd(X1,X1))))),
% 49.99/6.94 inference(forward_demodulation,[status(thm)],[f25765,f26371])).
% 49.99/6.94 fof(f26373,plain,(
% 49.99/6.94 ![X0,X1]: (rd(X0,rd(ld(rd(X1,X1),X0),X0))=ld(rd(X1,X1),rd(mult(mult(rd(X1,X1),X0),rd(X1,X1)),rd(X1,X1))))),
% 49.99/6.94 inference(forward_demodulation,[status(thm)],[f25774,f26372])).
% 49.99/6.94 fof(f26374,plain,(
% 49.99/6.94 ![X0,X1]: (mult(X0,rd(X1,X1))=ld(rd(X1,X1),rd(mult(mult(rd(X1,X1),X0),rd(X1,X1)),rd(X1,X1))))),
% 49.99/6.94 inference(forward_demodulation,[status(thm)],[f996,f26373])).
% 49.99/6.94 fof(f26375,plain,(
% 49.99/6.94 ![X0,X1]: (mult(X0,rd(X1,X1))=rd(mult(mult(rd(X1,X1),X0),rd(X1,X1)),rd(X1,X1)))),
% 49.99/6.94 inference(forward_demodulation,[status(thm)],[f26017,f26374])).
% 49.99/6.94 fof(f26421,plain,(
% 49.99/6.94 ![X0,X1]: (mult(X0,rd(X1,X1))=mult(rd(X1,X1),X0))),
% 49.99/6.94 inference(forward_demodulation,[status(thm)],[f10,f26375])).
% 49.99/6.94 fof(f26564,plain,(
% 49.99/6.94 ![X0,X1]: (mult(X0,rd(X1,X1))=mult(rd(X1,X1),mult(rd(X1,X1),X0)))),
% 49.99/6.94 inference(forward_demodulation,[status(thm)],[f26421,f25859])).
% 49.99/6.94 fof(f26565,plain,(
% 49.99/6.94 ~x0=x0),
% 49.99/6.94 inference(backward_demodulation,[status(thm)],[f26591,f12])).
% 49.99/6.94 fof(f26591,plain,(
% 49.99/6.94 ![X0,X1]: (mult(X0,rd(X1,X1))=X0)),
% 49.99/6.94 inference(forward_demodulation,[status(thm)],[f25989,f26564])).
% 49.99/6.94 fof(f27129,plain,(
% 49.99/6.94 $false),
% 49.99/6.94 inference(trivial_equality_resolution,[status(thm)],[f26565])).
% 49.99/6.94 % SZS output end CNFRefutation for theBenchmark.p
% 113.46/29.52 % Elapsed time: 28.879971 seconds
% 113.46/29.52 % CPU time: 147.724799 seconds
% 113.46/29.52 % Total memory used: 71.118 GB
% 113.46/29.52 % Net memory used: 71.117 GB
%------------------------------------------------------------------------------