%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP082-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:35:36 PM UTC 2026
% Result : Unsatisfiable 35.90s 4.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP082-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 19:52:41 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 35.90/4.97 % Refutation found
% 35.90/4.97 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 35.90/4.97 % SZS output start CNFRefutation for theBenchmark
% 35.90/4.97 fof(f1,axiom,(
% 35.90/4.97 (![X,Y,Z,U]: (double_divide(inverse(X),inverse(double_divide(inverse(double_divide(X,double_divide(Y,Z))),double_divide(U,double_divide(Y,U))))) = Z ))),
% 35.90/4.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.90/4.97 fof(f2,axiom,(
% 35.90/4.97 (![X,Y]: (multiply(X,Y) = inverse(double_divide(Y,X)) ))),
% 35.90/4.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.90/4.97 fof(f3,negated_conjecture,(
% 35.90/4.97 ( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)| multiply(multiply(inverse(b2),b2),a2) != a2| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ) ),
% 35.90/4.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 35.90/4.97 fof(f4,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,double_divide(X1,X2))),double_divide(X3,double_divide(X1,X3)))))=X2)),
% 35.90/4.97 inference(cnf_transformation,[status(thm)],[f1])).
% 35.90/4.97 fof(f5,plain,(
% 35.90/4.97 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 35.90/4.97 inference(cnf_transformation,[status(thm)],[f2])).
% 35.90/4.97 fof(f6,plain,(
% 35.90/4.97 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|~multiply(multiply(inverse(b2),b2),a2)=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 35.90/4.97 inference(cnf_transformation,[status(thm)],[f3])).
% 35.90/4.97 fof(f7,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(X2,X1)),inverse(double_divide(X0,double_divide(X2,X3)))))=X3)),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f5,f4])).
% 35.90/4.97 fof(f8,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,X3),X0)))=X3)),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5,f7])).
% 35.90/4.97 fof(f9,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(multiply(X0,X1),multiply(double_divide(X2,double_divide(X3,X2)),multiply(double_divide(X3,X4),double_divide(X1,X0))))=X4)),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f5,f8])).
% 35.90/4.97 fof(f10,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(double_divide(multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,X3),X4)),X3),multiply(double_divide(inverse(X4),X5),X0)))=X5)),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f8,f8])).
% 35.90/4.97 fof(f11,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(X3,X0)))=multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X3),X2)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f8,f8])).
% 35.90/4.97 fof(f12,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),X3)),inverse(X3))=inverse(X2))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f8,f5])).
% 35.90/4.97 fof(f13,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(double_divide(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),X3)),X2),multiply(double_divide(inverse(X3),X4),X5)),inverse(X5))=inverse(X4))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f8,f12])).
% 35.90/4.97 fof(f14,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3))=inverse(multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X2),X1))))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f8,f12])).
% 35.90/4.97 fof(f15,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),double_divide(X3,X4))),multiply(X4,X3))=inverse(X2))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f5,f12])).
% 35.90/4.97 fof(f69,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (X0=multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,double_divide(inverse(X3),X0)),X3)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f8,f11])).
% 35.90/4.97 fof(f71,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6]: (double_divide(inverse(X0),double_divide(inverse(X1),multiply(double_divide(X2,double_divide(inverse(X0),X2)),multiply(X3,X1))))=multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,double_divide(inverse(X6),X3)),X6)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f11,f11])).
% 35.90/4.97 fof(f115,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(inverse(X0),double_divide(inverse(X1),multiply(double_divide(X2,double_divide(inverse(X0),X2)),multiply(X3,X1))))=X3)),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f69,f71])).
% 35.90/4.97 fof(f140,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(inverse(multiply(double_divide(X0,double_divide(inverse(X1),X2)),X1)),multiply(double_divide(X3,double_divide(X4,X3)),X2))=double_divide(X0,X4))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f69,f8])).
% 35.90/4.97 fof(f158,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),double_divide(inverse(multiply(double_divide(X1,double_divide(inverse(X2),X3)),X2)),multiply(double_divide(X4,double_divide(inverse(X0),X4)),X3)))=double_divide(X5,double_divide(X1,X5)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f69,f115])).
% 35.90/4.97 fof(f161,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),double_divide(inverse(inverse(X1)),multiply(double_divide(X2,double_divide(inverse(X0),X2)),inverse(X3))))=multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X3),X1)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f12,f115])).
% 35.90/4.97 fof(f184,plain,(
% 35.90/4.97 ![X0,X1,X2]: (double_divide(inverse(X0),double_divide(X1,inverse(X0)))=double_divide(X2,double_divide(X1,X2)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f140,f158])).
% 35.90/4.97 fof(f190,plain,(
% 35.90/4.97 ![X0,X1,X2]: (double_divide(X0,double_divide(X1,X0))=double_divide(X2,double_divide(X1,X2)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f184,f184])).
% 35.90/4.97 fof(f278,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,X1),double_divide(X2,double_divide(X0,X2)))=double_divide(X3,double_divide(X1,X3)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f190,f190])).
% 35.90/4.97 fof(f294,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (X0=multiply(double_divide(X1,double_divide(X0,X1)),multiply(double_divide(X2,double_divide(inverse(X3),X2)),X3)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f190,f69])).
% 35.90/4.97 fof(f318,plain,(
% 35.90/4.97 ![X0,X1,X2]: (multiply(double_divide(X0,X1),X1)=inverse(double_divide(X2,double_divide(X0,X2))))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f190,f5])).
% 35.90/4.97 fof(f379,plain,(
% 35.90/4.97 ![X0,X1,X2]: (multiply(double_divide(X0,X1),X1)=multiply(double_divide(X0,X2),X2))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5,f318])).
% 35.90/4.97 fof(f390,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,X2))=multiply(double_divide(X2,X3),X3))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f190,f379])).
% 35.90/4.97 fof(f404,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(multiply(X0,X1),multiply(double_divide(X2,double_divide(X3,X2)),multiply(double_divide(X3,X4),X4)))=double_divide(X1,X0))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f379,f9])).
% 35.90/4.97 fof(f408,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,X3),X3)))=X0)),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f379,f8])).
% 35.90/4.97 fof(f433,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(X0,double_divide(X1,double_divide(inverse(X2),X1)))=double_divide(X3,double_divide(double_divide(inverse(X4),multiply(double_divide(X5,double_divide(inverse(X2),X5)),multiply(X0,X4))),X3)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f115,f278])).
% 35.90/4.97 fof(f436,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(X0,double_divide(X1,double_divide(inverse(X2),X1)))=double_divide(X3,double_divide(multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X0),X2)),X3)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f8,f278])).
% 35.90/4.97 fof(f467,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(X0,inverse(X1))=multiply(double_divide(X2,double_divide(double_divide(X0,X3),X2)),multiply(double_divide(X4,double_divide(X3,X4)),X1)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f278,f69])).
% 35.90/4.97 fof(f564,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(double_divide(X0,double_divide(multiply(X1,X2),X0)),X3)=multiply(double_divide(multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X3),double_divide(X2,X1))),X6),X6))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f9,f390])).
% 35.90/4.97 fof(f568,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,double_divide(inverse(X1),X0)),X2)=multiply(double_divide(multiply(double_divide(X3,double_divide(X4,X3)),multiply(double_divide(X4,X2),X1)),X5),X5))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f8,f390])).
% 35.90/4.97 fof(f609,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6,X7]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(double_divide(X3,double_divide(X4,X3)),double_divide(X4,X5))))=multiply(double_divide(X6,double_divide(X7,X6)),multiply(double_divide(X7,double_divide(X5,X0)),X2)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f390,f11])).
% 35.90/4.97 fof(f697,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(double_divide(X2,X3),X1)),multiply(double_divide(X4,double_divide(X3,X4)),double_divide(X5,double_divide(X2,X5)))))=X0)),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f278,f408])).
% 35.90/4.97 fof(f721,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(X0,double_divide(X1,double_divide(inverse(X0),X1)))=double_divide(X2,double_divide(multiply(double_divide(X3,double_divide(X4,X3)),multiply(double_divide(X4,X5),X5)),X2)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f408,f278])).
% 35.90/4.97 fof(f742,plain,(
% 35.90/4.97 ![X0,X1,X2]: (double_divide(inverse(X0),double_divide(X1,inverse(double_divide(X2,double_divide(X1,X2)))))=X0)),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f467,f697])).
% 35.90/4.97 fof(f743,plain,(
% 35.90/4.97 ![X0,X1,X2]: (double_divide(inverse(X0),double_divide(X1,multiply(double_divide(X1,X2),X2)))=X0)),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5,f742])).
% 35.90/4.97 fof(f747,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(multiply(X0,X1),double_divide(X2,multiply(double_divide(X2,X3),X3)))=double_divide(X1,X0))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f5,f743])).
% 35.90/4.97 fof(f749,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(inverse(X0),double_divide(X1,multiply(double_divide(X2,double_divide(X3,X2)),double_divide(X3,X1))))=X0)),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f390,f743])).
% 35.90/4.97 fof(f778,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (multiply(double_divide(inverse(X0),X1),X1)=multiply(X0,double_divide(X2,multiply(double_divide(X2,X3),X3))))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f743,f379])).
% 35.90/4.97 fof(f780,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(X0,double_divide(inverse(X1),X0))=double_divide(double_divide(X2,multiply(double_divide(X2,X3),X3)),X1))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f743,f190])).
% 35.90/4.97 fof(f890,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6,X7]: (double_divide(inverse(X0),double_divide(inverse(inverse(X1)),multiply(double_divide(X2,double_divide(inverse(X0),X2)),inverse(X3))))=multiply(double_divide(multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X6),X7)),X6),multiply(double_divide(inverse(X7),X3),X1)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f13,f115])).
% 35.90/4.97 fof(f1091,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(double_divide(multiply(X0,X1),X2),X2)=multiply(double_divide(X1,X0),double_divide(X3,multiply(double_divide(X3,X4),X4))))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f747,f379])).
% 35.90/4.97 fof(f1223,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6,X7]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(double_divide(inverse(X3),X4),X0)))=multiply(double_divide(X5,double_divide(X4,X5)),multiply(double_divide(double_divide(X6,multiply(double_divide(X6,X7),X7)),X3),X2)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f780,f11])).
% 35.90/4.97 fof(f1250,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (X0=multiply(double_divide(X1,double_divide(inverse(double_divide(X0,double_divide(X2,multiply(double_divide(X2,X3),X3)))),X1)),multiply(double_divide(X4,double_divide(inverse(X5),X4)),X5)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f780,f294])).
% 35.90/4.97 fof(f1264,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3))=inverse(multiply(double_divide(X4,double_divide(double_divide(X5,multiply(double_divide(X5,X6),X6)),X4)),multiply(double_divide(X7,double_divide(inverse(X2),X7)),X1))))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f780,f14])).
% 35.90/4.97 fof(f1288,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),double_divide(X3,double_divide(inverse(X4),X3)))),multiply(X4,double_divide(X5,multiply(double_divide(X5,X6),X6))))=inverse(X2))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f780,f15])).
% 35.90/4.97 fof(f1324,plain,(
% 35.90/4.97 ![X0,X1,X2]: (X0=inverse(double_divide(X0,double_divide(X1,multiply(double_divide(X1,X2),X2)))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f294,f1250])).
% 35.90/4.97 fof(f1336,plain,(
% 35.90/4.97 ![X0,X1,X2]: (X0=multiply(double_divide(X1,multiply(double_divide(X1,X2),X2)),X0))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5,f1324])).
% 35.90/4.97 fof(f1373,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (X0=multiply(double_divide(X1,multiply(double_divide(X2,double_divide(X3,X2)),double_divide(X3,X1))),X0))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f390,f1336])).
% 35.90/4.97 fof(f1381,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (X0=multiply(double_divide(inverse(X1),multiply(X1,double_divide(X2,multiply(double_divide(X2,X3),X3)))),X0))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f743,f1336])).
% 35.90/4.97 fof(f1406,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(X2,X1)),X0))=multiply(double_divide(X2,X3),X3))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f1336,f8])).
% 35.90/4.97 fof(f2434,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(multiply(double_divide(X3,double_divide(X4,X3)),double_divide(X4,X5)),X0)))=multiply(double_divide(X6,double_divide(X5,X6)),X2))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f1373,f11])).
% 35.90/4.97 fof(f2629,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(inverse(X0),X1),X1)=multiply(X0,double_divide(X2,double_divide(inverse(multiply(double_divide(double_divide(X3,multiply(double_divide(X3,X4),X4)),X5),X5)),X2))))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f780,f778])).
% 35.90/4.97 fof(f2693,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,double_divide(X3,multiply(double_divide(X3,X4),X4)))),inverse(X5))=inverse(multiply(double_divide(X6,double_divide(X7,X6)),multiply(double_divide(X7,double_divide(inverse(X2),X5)),X1))))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f778,f14])).
% 35.90/4.97 fof(f2694,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),double_divide(inverse(X1),multiply(double_divide(X2,double_divide(inverse(X0),X2)),multiply(X3,double_divide(X4,multiply(double_divide(X4,X5),X5))))))=double_divide(inverse(X3),X1))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f778,f115])).
% 35.90/4.97 fof(f2695,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6,X7]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(X3,double_divide(X4,multiply(double_divide(X4,X5),X5)))))=multiply(double_divide(X6,double_divide(X7,X6)),multiply(double_divide(X7,double_divide(inverse(X3),X0)),X2)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f778,f11])).
% 35.90/4.97 fof(f2705,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (X0=multiply(double_divide(multiply(double_divide(X1,X2),X2),multiply(double_divide(inverse(double_divide(X3,double_divide(X1,X3))),X4),X4)),X0))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f778,f1373])).
% 35.90/4.97 fof(f2773,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (X0=multiply(double_divide(multiply(double_divide(X1,X2),X2),multiply(double_divide(multiply(double_divide(X1,X3),X3),X4),X4)),X0))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5,f2705])).
% 35.90/4.97 fof(f2936,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(inverse(double_divide(X0,X1)),multiply(double_divide(X1,X2),X2))=multiply(double_divide(X0,X3),X3))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f390,f1406])).
% 35.90/4.97 fof(f3046,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(double_divide(X2,X3),X3))=multiply(double_divide(multiply(double_divide(X4,double_divide(X2,X4)),X1),X5),X5))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f1406,f390])).
% 35.90/4.97 fof(f3050,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(multiply(double_divide(X0,X1),X1),double_divide(X2,double_divide(inverse(X3),X2)))=double_divide(X4,double_divide(multiply(double_divide(X5,double_divide(X0,X5)),X3),X4)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f1406,f278])).
% 35.90/4.97 fof(f3056,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6,X7]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(multiply(double_divide(X3,double_divide(X4,X3)),X5),X0)))=multiply(double_divide(X6,double_divide(inverse(X5),X6)),multiply(multiply(double_divide(X4,X7),X7),X2)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f1406,f11])).
% 35.90/4.97 fof(f3117,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(multiply(X0,X1),multiply(double_divide(X0,X2),X2))=multiply(double_divide(X1,X3),X3))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5,f2936])).
% 35.90/4.97 fof(f3143,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(X0,multiply(double_divide(double_divide(X1,multiply(double_divide(X1,X2),X2)),X3),X3))=multiply(double_divide(X0,X4),X4))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f1336,f3117])).
% 35.90/4.97 fof(f3249,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(multiply(double_divide(X2,X3),X3),X4)),inverse(X4))=inverse(multiply(double_divide(X5,double_divide(multiply(X2,X6),X5)),multiply(multiply(double_divide(X6,X7),X7),X1))))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f3117,f14])).
% 35.90/4.97 fof(f3268,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6,X7]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(multiply(double_divide(X3,X4),X4),X0)))=multiply(double_divide(X5,double_divide(multiply(X3,X6),X5)),multiply(multiply(double_divide(X6,X7),X7),X2)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f3117,f11])).
% 35.90/4.97 fof(f3463,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (X0=multiply(multiply(double_divide(inverse(double_divide(double_divide(X1,multiply(double_divide(X1,X2),X2)),double_divide(X3,multiply(double_divide(X3,X4),X4)))),X5),X5),X0))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f3143,f1381])).
% 35.90/4.97 fof(f3468,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6]: (X0=multiply(double_divide(X1,double_divide(X0,X1)),multiply(double_divide(multiply(double_divide(double_divide(X2,multiply(double_divide(X2,X3),X3)),X4),X4),multiply(double_divide(inverse(X5),X6),X6)),X5)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f3143,f294])).
% 35.90/4.97 fof(f3473,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(inverse(X0),multiply(double_divide(double_divide(X1,multiply(double_divide(X1,X2),X2)),X3),X3))=X0)),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f3143,f749])).
% 35.90/4.97 fof(f3495,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6]: (X0=multiply(double_divide(multiply(double_divide(double_divide(X1,multiply(double_divide(X1,X2),X2)),X3),X3),multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X6),X6))),X0))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f3143,f1373])).
% 35.90/4.97 fof(f3541,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(multiply(double_divide(double_divide(X0,multiply(double_divide(X0,X1),X1)),X2),X2),X3)=inverse(multiply(double_divide(X3,X4),X4)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f3143,f5])).
% 35.90/4.97 fof(f3542,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,double_divide(X1,multiply(double_divide(X1,X2),X2)))=double_divide(inverse(X0),multiply(double_divide(double_divide(X3,multiply(double_divide(X3,X4),X4)),X5),X5)))),
% 35.90/4.97 inference(paramodulation,[status(thm)],[f3143,f1381])).
% 35.90/4.97 fof(f3611,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (X0=multiply(multiply(double_divide(multiply(double_divide(X1,multiply(double_divide(X1,X2),X2)),double_divide(X3,multiply(double_divide(X3,X4),X4))),X5),X5),X0))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5,f3463])).
% 35.90/4.97 fof(f3614,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (X0=multiply(multiply(double_divide(double_divide(X1,multiply(double_divide(X1,X2),X2)),X3),X3),X0))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f1336,f3611])).
% 35.90/4.97 fof(f3641,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3))=inverse(multiply(double_divide(X4,double_divide(inverse(X2),X4)),X1)))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3646,f1264])).
% 35.90/4.97 fof(f3646,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (X0=multiply(double_divide(X1,double_divide(double_divide(X2,multiply(double_divide(X2,X3),X3)),X1)),X0))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f404,f3495])).
% 35.90/4.97 fof(f3661,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(double_divide(inverse(X0),X1),X1)=multiply(X0,double_divide(X2,double_divide(double_divide(X3,multiply(double_divide(X3,X4),X4)),X2))))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3676,f2629])).
% 35.90/4.97 fof(f3676,plain,(
% 35.90/4.97 ![X0,X1]: (X0=inverse(multiply(double_divide(X0,X1),X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f3614,f3541])).
% 35.90/4.97 fof(f3678,plain,(
% 35.90/4.97 ![X0,X1]: (multiply(double_divide(inverse(X0),X1),X1)=X0)),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3784,f778])).
% 35.90/4.97 fof(f3718,plain,(
% 35.90/4.97 ![X0,X1,X2]: (multiply(double_divide(multiply(X0,X1),X2),X2)=double_divide(X1,X0))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3784,f1091])).
% 35.90/4.97 fof(f3749,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),X3))=multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,double_divide(inverse(X3),X0)),X2)))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3784,f2695])).
% 35.90/4.97 fof(f3750,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(inverse(X0),double_divide(inverse(X1),multiply(double_divide(X2,double_divide(inverse(X0),X2)),X3)))=double_divide(inverse(X3),X1))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3784,f2694])).
% 35.90/4.97 fof(f3751,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),X2),inverse(X3))=inverse(multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,double_divide(inverse(X2),X3)),X1))))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3784,f2693])).
% 35.90/4.97 fof(f3778,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),double_divide(X3,double_divide(inverse(X4),X3)))),X4)=inverse(X2))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3784,f1288])).
% 35.90/4.97 fof(f3784,plain,(
% 35.90/4.97 ![X0,X1,X2]: (multiply(X0,double_divide(X1,multiply(double_divide(X1,X2),X2)))=X0)),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f3473,f3542])).
% 35.90/4.97 fof(f3994,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (X0=multiply(X0,double_divide(X1,double_divide(double_divide(X2,multiply(double_divide(X2,X3),X3)),X1))))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3678,f3661])).
% 35.90/4.97 fof(f4002,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (X0=multiply(double_divide(X1,double_divide(X0,X1)),multiply(double_divide(multiply(double_divide(double_divide(X2,multiply(double_divide(X2,X3),X3)),X4),X4),X5),X5)))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3678,f3468])).
% 35.90/4.97 fof(f4066,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,double_divide(multiply(X1,X2),X0)),X3)=double_divide(multiply(double_divide(X4,X3),double_divide(X2,X1)),double_divide(X5,double_divide(X4,X5))))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3718,f564])).
% 35.90/4.97 fof(f4069,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,double_divide(inverse(X1),X0)),X2)=double_divide(multiply(double_divide(X3,X2),X1),double_divide(X4,double_divide(X3,X4))))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3718,f568])).
% 35.90/4.97 fof(f4070,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(double_divide(X2,X3),X3))=double_divide(X1,double_divide(X4,double_divide(X2,X4))))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3718,f3046])).
% 35.90/4.97 fof(f4075,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (X0=multiply(double_divide(multiply(double_divide(X1,X2),X2),double_divide(X3,double_divide(X1,X3))),X0))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3718,f2773])).
% 35.90/4.97 fof(f4118,plain,(
% 35.90/4.97 ![X0,X1]: (double_divide(inverse(multiply(X0,X1)),X1)=X0)),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3750,f115])).
% 35.90/4.97 fof(f4120,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(inverse(X0)),inverse(X1))=multiply(double_divide(multiply(double_divide(X2,double_divide(X3,X2)),multiply(double_divide(X3,X4),X5)),X4),multiply(double_divide(inverse(X5),X0),X1)))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3750,f890])).
% 35.90/4.97 fof(f4121,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(inverse(inverse(X0)),inverse(X1))=multiply(double_divide(X2,double_divide(X3,X2)),multiply(double_divide(X3,X0),X1)))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f3750,f161])).
% 35.90/4.97 fof(f4164,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (X0=multiply(double_divide(X1,double_divide(X0,X1)),double_divide(X2,double_divide(double_divide(X3,multiply(double_divide(X3,X4),X4)),X2))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f3718,f4002])).
% 35.90/4.97 fof(f4165,plain,(
% 35.90/4.97 ![X0,X1,X2]: (inverse(X0)=double_divide(double_divide(X1,multiply(double_divide(X1,X2),X2)),X0))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f780])).
% 35.90/4.97 fof(f4166,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(multiply(inverse(X0),multiply(X1,X2)),inverse(X2))=inverse(multiply(double_divide(X3,double_divide(X4,X3)),multiply(double_divide(X4,X1),X0))))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f14])).
% 35.90/4.97 fof(f4178,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(inverse(X0),multiply(double_divide(multiply(X1,multiply(double_divide(X1,X2),X3)),X2),multiply(double_divide(inverse(X3),X4),X0)))=X4)),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f10])).
% 35.90/4.97 fof(f4183,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(X0,double_divide(X1,double_divide(inverse(X2),X1)))=double_divide(inverse(X3),multiply(double_divide(X4,double_divide(inverse(X2),X4)),multiply(X0,X3))))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f433])).
% 35.90/4.97 fof(f4220,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(X0,double_divide(X1,double_divide(inverse(X0),X1)))=multiply(double_divide(X2,double_divide(X3,X2)),multiply(double_divide(X3,X4),X4)))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f721])).
% 35.90/4.97 fof(f4221,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(X0,double_divide(X1,double_divide(inverse(X2),X1)))=multiply(double_divide(X3,double_divide(X4,X3)),multiply(double_divide(X4,X0),X2)))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f436])).
% 35.90/4.97 fof(f4222,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(multiply(double_divide(X0,X1),X1),double_divide(X2,double_divide(inverse(X3),X2)))=multiply(double_divide(X4,double_divide(X0,X4)),X3))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f3050])).
% 35.90/4.97 fof(f4236,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(multiply(double_divide(X3,X4),X4),X0)))=multiply(multiply(X3,X5),multiply(multiply(double_divide(X5,X6),X6),X2)))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f3268])).
% 35.90/4.97 fof(f4239,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(multiply(double_divide(X2,X3),X3),X4)),inverse(X4))=inverse(multiply(multiply(X2,X5),multiply(multiply(double_divide(X5,X6),X6),X1))))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f3249])).
% 35.90/4.97 fof(f4278,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),inverse(X3))),X3)=inverse(X2))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f3778])).
% 35.90/4.97 fof(f4287,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(multiply(inverse(X0),X1),inverse(X2))=inverse(multiply(double_divide(X3,double_divide(X4,X3)),multiply(double_divide(X4,double_divide(inverse(X1),X2)),X0))))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f3751])).
% 35.90/4.97 fof(f4289,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(inverse(X0),multiply(inverse(X1),X2))=multiply(double_divide(X3,double_divide(X4,X3)),multiply(double_divide(X4,double_divide(inverse(X2),X0)),X1)))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f3749])).
% 35.90/4.97 fof(f4298,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3))=inverse(multiply(inverse(X2),X1)))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f3641])).
% 35.90/4.97 fof(f4335,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6]: (double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(multiply(double_divide(X3,double_divide(X4,X3)),X5),X0)))=multiply(inverse(X5),multiply(multiply(double_divide(X4,X6),X6),X2)))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f3056])).
% 35.90/4.97 fof(f4363,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(inverse(X1),multiply(multiply(double_divide(X2,double_divide(X3,X2)),double_divide(X3,X4)),X0)))=multiply(double_divide(X5,double_divide(X4,X5)),X1))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f2434])).
% 35.90/4.97 fof(f4388,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6]: (double_divide(inverse(X0),multiply(inverse(X1),multiply(double_divide(inverse(X2),X3),X0)))=multiply(double_divide(X4,double_divide(X3,X4)),multiply(double_divide(double_divide(X5,multiply(double_divide(X5,X6),X6)),X2),X1)))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f1223])).
% 35.90/4.97 fof(f4482,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5,X6]: (double_divide(inverse(X0),multiply(inverse(X1),multiply(double_divide(X2,double_divide(X3,X2)),double_divide(X3,X4))))=multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(X6,double_divide(X4,X0)),X1)))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f4937,f609])).
% 35.90/4.97 fof(f4937,plain,(
% 35.90/4.97 ![X0,X1]: (X0=double_divide(X1,double_divide(X0,X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f3994,f4164])).
% 35.90/4.97 fof(f5010,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(multiply(X0,X1),X2)=double_divide(multiply(double_divide(X3,X2),double_divide(X1,X0)),double_divide(X4,double_divide(X3,X4))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4066])).
% 35.90/4.97 fof(f5011,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (multiply(multiply(X0,X1),X2)=double_divide(multiply(double_divide(X3,X2),double_divide(X1,X0)),X3))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f5010])).
% 35.90/4.97 fof(f5016,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (multiply(inverse(X0),X1)=double_divide(multiply(double_divide(X2,X1),X0),double_divide(X3,double_divide(X2,X3))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4069])).
% 35.90/4.97 fof(f5021,plain,(
% 35.90/4.97 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(inverse(double_divide(X1,X0)),X2))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f5026,f5011])).
% 35.90/4.97 fof(f5026,plain,(
% 35.90/4.97 ![X0,X1,X2]: (multiply(inverse(X0),X1)=double_divide(multiply(double_divide(X2,X1),X0),X2))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f5016])).
% 35.90/4.97 fof(f5027,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(double_divide(X1,X2),X2))=double_divide(X0,double_divide(X3,double_divide(X1,X3))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4070])).
% 35.90/4.97 fof(f5028,plain,(
% 35.90/4.97 ![X0,X1,X2]: (multiply(inverse(X0),multiply(double_divide(X1,X2),X2))=double_divide(X0,X1))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f5027])).
% 35.90/4.97 fof(f5035,plain,(
% 35.90/4.97 ![X0,X1,X2]: (X0=multiply(double_divide(multiply(double_divide(X1,X2),X2),X1),X0))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4075])).
% 35.90/4.97 fof(f5036,plain,(
% 35.90/4.97 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|~a2=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 35.90/4.97 inference(backward_demodulation,[status(thm)],[f5037,f6])).
% 35.90/4.97 fof(f5037,plain,(
% 35.90/4.97 ![X0,X1]: (X0=multiply(multiply(inverse(X1),X1),X0))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5026,f5035])).
% 35.90/4.97 fof(f5084,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(inverse(inverse(X0)),inverse(X1))=multiply(double_divide(multiply(X2,multiply(double_divide(X2,X3),X4)),X3),multiply(double_divide(inverse(X4),X0),X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4120])).
% 35.90/4.97 fof(f5110,plain,(
% 35.90/4.97 ![X0,X1,X2]: (double_divide(inverse(inverse(X0)),inverse(X1))=multiply(X2,multiply(double_divide(X2,X0),X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4121])).
% 35.90/4.97 fof(f5252,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (multiply(multiply(inverse(X0),multiply(X1,X2)),inverse(X2))=inverse(multiply(X3,multiply(double_divide(X3,X1),X0))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4166])).
% 35.90/4.97 fof(f5253,plain,(
% 35.90/4.97 ![X0,X1,X2]: (multiply(multiply(inverse(X0),multiply(X1,X2)),inverse(X2))=inverse(double_divide(inverse(inverse(X1)),inverse(X0))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5110,f5252])).
% 35.90/4.97 fof(f5254,plain,(
% 35.90/4.97 ![X0,X1,X2]: (multiply(multiply(inverse(X0),multiply(X1,X2)),inverse(X2))=multiply(inverse(X0),inverse(inverse(X1))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5,f5253])).
% 35.90/4.97 fof(f5267,plain,(
% 35.90/4.97 ![X0,X1]: (double_divide(inverse(X0),double_divide(inverse(inverse(X1)),inverse(X0)))=X1)),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5084,f4178])).
% 35.90/4.97 fof(f5273,plain,(
% 35.90/4.97 ![X0]: (inverse(inverse(X0))=X0)),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f5267])).
% 35.90/4.97 fof(f5283,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(X0,inverse(X1))=double_divide(inverse(X2),multiply(double_divide(X3,double_divide(inverse(X1),X3)),multiply(X0,X2))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4183])).
% 35.90/4.97 fof(f5284,plain,(
% 35.90/4.97 ![X0,X1,X2]: (double_divide(X0,inverse(X1))=double_divide(inverse(X2),multiply(inverse(X1),multiply(X0,X2))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f5283])).
% 35.90/4.97 fof(f5383,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(X0,inverse(X0))=multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,X3),X3)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4220])).
% 35.90/4.97 fof(f5384,plain,(
% 35.90/4.97 ![X0,X1,X2]: (double_divide(X0,inverse(X0))=multiply(X1,multiply(double_divide(X1,X2),X2)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f5383])).
% 35.90/4.97 fof(f5385,plain,(
% 35.90/4.97 ![X0,X1]: (double_divide(X0,inverse(X0))=double_divide(inverse(inverse(X1)),inverse(X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5110,f5384])).
% 35.90/4.97 fof(f5386,plain,(
% 35.90/4.97 ![X0,X1]: (double_divide(X0,inverse(X0))=double_divide(X1,inverse(X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5273,f5385])).
% 35.90/4.97 fof(f5387,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(X0,inverse(X1))=multiply(double_divide(X2,double_divide(X3,X2)),multiply(double_divide(X3,X0),X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4221])).
% 35.90/4.97 fof(f5388,plain,(
% 35.90/4.97 ![X0,X1,X2]: (double_divide(X0,inverse(X1))=multiply(X2,multiply(double_divide(X2,X0),X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f5387])).
% 35.90/4.97 fof(f5389,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(multiply(double_divide(X0,X1),X1),inverse(X2))=multiply(double_divide(X3,double_divide(X0,X3)),X2))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4222])).
% 35.90/4.97 fof(f5390,plain,(
% 35.90/4.97 ![X0,X1,X2]: (double_divide(multiply(double_divide(X0,X1),X1),inverse(X2))=multiply(X0,X2))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f5389])).
% 35.90/4.97 fof(f5396,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(inverse(X1),multiply(multiply(double_divide(X2,X3),X3),X0)))=multiply(multiply(X2,X4),multiply(multiply(double_divide(X4,X5),X5),X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4236])).
% 35.90/4.97 fof(f5397,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(multiply(double_divide(X0,X1),X1),inverse(X2))=multiply(multiply(X0,X3),multiply(multiply(double_divide(X3,X4),X4),X2)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5284,f5396])).
% 35.90/4.97 fof(f5403,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (multiply(X0,X1)=multiply(multiply(X0,X2),multiply(multiply(double_divide(X2,X3),X3),X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5390,f5397])).
% 35.90/4.97 fof(f5417,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(inverse(X0),multiply(multiply(double_divide(X1,X2),X2),X3)),inverse(X3))=inverse(multiply(multiply(X1,X4),multiply(multiply(double_divide(X4,X5),X5),X0))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4239])).
% 35.90/4.97 fof(f5418,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),inverse(inverse(multiply(double_divide(X1,X2),X2))))=inverse(multiply(multiply(X1,X3),multiply(multiply(double_divide(X3,X4),X4),X0))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5254,f5417])).
% 35.90/4.97 fof(f5419,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(double_divide(X1,X2),X2))=inverse(multiply(multiply(X1,X3),multiply(multiply(double_divide(X3,X4),X4),X0))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5273,f5418])).
% 35.90/4.97 fof(f5420,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(X0,X1)=inverse(multiply(multiply(X1,X2),multiply(multiply(double_divide(X2,X3),X3),X0))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5028,f5419])).
% 35.90/4.97 fof(f5425,plain,(
% 35.90/4.97 ![X0,X1]: (double_divide(X0,X1)=inverse(multiply(X1,X0)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5403,f5420])).
% 35.90/4.97 fof(f5534,plain,(
% 35.90/4.97 ![X0,X1,X2]: (multiply(multiply(X0,multiply(double_divide(X0,X1),inverse(X2))),X2)=inverse(X1))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4278])).
% 35.90/4.97 fof(f5535,plain,(
% 35.90/4.97 ![X0,X1]: (multiply(double_divide(X0,inverse(inverse(X1))),X1)=inverse(X0))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5388,f5534])).
% 35.90/4.97 fof(f5614,plain,(
% 35.90/4.97 ![X0,X1]: (multiply(double_divide(X0,X1),X1)=inverse(X0))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5273,f5535])).
% 35.90/4.97 fof(f5624,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (multiply(multiply(inverse(X0),X1),inverse(X2))=double_divide(multiply(double_divide(X3,double_divide(inverse(X1),X2)),X0),double_divide(X4,double_divide(X3,X4))))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5425,f4287])).
% 35.90/4.97 fof(f5625,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (multiply(multiply(inverse(X0),X1),inverse(X2))=double_divide(multiply(double_divide(X3,double_divide(inverse(X1),X2)),X0),X3))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f5624])).
% 35.90/4.97 fof(f5627,plain,(
% 35.90/4.97 ![X0,X1,X2]: (multiply(multiply(inverse(X0),X1),inverse(X2))=multiply(inverse(X0),double_divide(inverse(X1),X2)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5026,f5625])).
% 35.90/4.97 fof(f5628,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(inverse(X0),multiply(inverse(X1),X2))=multiply(X3,multiply(double_divide(X3,double_divide(inverse(X2),X0)),X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4289])).
% 35.90/4.97 fof(f5629,plain,(
% 35.90/4.97 ![X0,X1,X2]: (double_divide(inverse(X0),multiply(inverse(X1),X2))=double_divide(double_divide(inverse(X2),X0),inverse(X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5388,f5628])).
% 35.90/4.97 fof(f5637,plain,(
% 35.90/4.97 ![X0,X1,X2]: (multiply(multiply(inverse(X0),multiply(X1,X2)),inverse(X2))=inverse(multiply(inverse(X1),X0)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4298])).
% 35.90/4.97 fof(f5638,plain,(
% 35.90/4.97 ![X0,X1,X2]: (multiply(inverse(X0),double_divide(inverse(multiply(X1,X2)),X2))=inverse(multiply(inverse(X1),X0)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5627,f5637])).
% 35.90/4.97 fof(f5639,plain,(
% 35.90/4.97 ![X0,X1]: (multiply(inverse(X0),X1)=inverse(multiply(inverse(X1),X0)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4118,f5638])).
% 35.90/4.97 fof(f5659,plain,(
% 35.90/4.97 ![X0,X1]: (multiply(inverse(X0),X1)=double_divide(X0,inverse(X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5425,f5639])).
% 35.90/4.97 fof(f5812,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(inverse(X1),multiply(multiply(double_divide(X2,double_divide(X3,X2)),X4),X0)))=multiply(inverse(X4),multiply(multiply(double_divide(X3,X5),X5),X1)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f4335])).
% 35.90/4.97 fof(f5813,plain,(
% 35.90/4.97 ![X0,X1,X2,X3,X4]: (double_divide(multiply(double_divide(X0,double_divide(X1,X0)),X2),inverse(X3))=multiply(inverse(X2),multiply(multiply(double_divide(X1,X4),X4),X3)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f5284,f5812])).
% 35.90/4.97 fof(f5814,plain,(
% 35.90/4.97 ![X0,X1,X2,X3]: (double_divide(multiply(X0,X1),inverse(X2))=multiply(inverse(X1),multiply(multiply(double_divide(X0,X3),X3),X2)))),
% 35.90/4.97 inference(forward_demodulation,[status(thm)],[f4937,f5813])).
% 35.90/4.97 fof(f5815,plain,(
% 35.90/4.98 ![X0,X1,X2,X3]: (double_divide(multiply(X0,X1),inverse(X2))=double_divide(X1,inverse(multiply(multiply(double_divide(X0,X3),X3),X2))))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5659,f5814])).
% 35.90/4.98 fof(f5816,plain,(
% 35.90/4.98 ![X0,X1,X2,X3]: (double_divide(multiply(X0,X1),inverse(X2))=double_divide(X1,double_divide(X2,multiply(double_divide(X0,X3),X3))))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5425,f5815])).
% 35.90/4.98 fof(f5818,plain,(
% 35.90/4.98 ![X0,X1,X2]: (double_divide(multiply(X0,X1),inverse(X2))=double_divide(X1,double_divide(X2,inverse(X0))))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5614,f5816])).
% 35.90/4.98 fof(f5942,plain,(
% 35.90/4.98 ![X0,X1,X2,X3,X4]: (double_divide(multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,X2)),inverse(X3))=multiply(double_divide(X4,double_divide(X2,X4)),X3))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5284,f4363])).
% 35.90/4.98 fof(f5943,plain,(
% 35.90/4.98 ![X0,X1,X2,X3,X4]: (double_divide(double_divide(X0,X1),double_divide(X2,inverse(double_divide(X3,double_divide(X0,X3)))))=multiply(double_divide(X4,double_divide(X1,X4)),X2))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5818,f5942])).
% 35.90/4.98 fof(f5944,plain,(
% 35.90/4.98 ![X0,X1,X2,X3,X4]: (double_divide(double_divide(X0,X1),double_divide(X2,multiply(double_divide(X0,X3),X3)))=multiply(double_divide(X4,double_divide(X1,X4)),X2))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5,f5943])).
% 35.90/4.98 fof(f5945,plain,(
% 35.90/4.98 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,X1),double_divide(X2,inverse(X0)))=multiply(double_divide(X3,double_divide(X1,X3)),X2))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5614,f5944])).
% 35.90/4.98 fof(f5947,plain,(
% 35.90/4.98 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),double_divide(X2,inverse(X0)))=multiply(X1,X2))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f4937,f5945])).
% 35.90/4.98 fof(f6068,plain,(
% 35.90/4.98 ![X0,X1,X2,X3,X4,X5]: (double_divide(double_divide(inverse(X0),X1),inverse(X2))=multiply(double_divide(X3,double_divide(X1,X3)),multiply(double_divide(double_divide(X4,multiply(double_divide(X4,X5),X5)),X0),X2)))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5284,f4388])).
% 35.90/4.98 fof(f6069,plain,(
% 35.90/4.98 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),multiply(inverse(X1),X2))=multiply(double_divide(X3,double_divide(X0,X3)),multiply(double_divide(double_divide(X4,multiply(double_divide(X4,X5),X5)),X2),X1)))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5629,f6068])).
% 35.90/4.98 fof(f6070,plain,(
% 35.90/4.98 ![X0,X1,X2,X3,X4,X5]: (double_divide(inverse(X0),double_divide(X1,inverse(X2)))=multiply(double_divide(X3,double_divide(X0,X3)),multiply(double_divide(double_divide(X4,multiply(double_divide(X4,X5),X5)),X2),X1)))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5659,f6069])).
% 35.90/4.98 fof(f6071,plain,(
% 35.90/4.98 ![X0,X1,X2,X3,X4]: (double_divide(inverse(X0),double_divide(X1,inverse(X2)))=multiply(X0,multiply(double_divide(double_divide(X3,multiply(double_divide(X3,X4),X4)),X2),X1)))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f4937,f6070])).
% 35.90/4.98 fof(f6072,plain,(
% 35.90/4.98 ![X0,X1,X2]: (double_divide(inverse(X0),double_divide(X1,inverse(X2)))=multiply(X0,multiply(inverse(X2),X1)))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f4165,f6071])).
% 35.90/4.98 fof(f6073,plain,(
% 35.90/4.98 ![X0,X1,X2]: (double_divide(inverse(X0),double_divide(X1,inverse(X2)))=multiply(X0,double_divide(X2,inverse(X1))))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5659,f6072])).
% 35.90/4.98 fof(f6792,plain,(
% 35.90/4.98 ![X0,X1,X2,X3,X4,X5,X6]: (double_divide(inverse(X0),double_divide(X1,inverse(multiply(double_divide(X2,double_divide(X3,X2)),double_divide(X3,X4)))))=multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(X6,double_divide(X4,X0)),X1)))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5659,f4482])).
% 35.90/4.98 fof(f6793,plain,(
% 35.90/4.98 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,double_divide(multiply(double_divide(X1,double_divide(X2,X1)),double_divide(X2,X3)),inverse(X4)))=multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(X6,double_divide(X3,X0)),X4)))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f6073,f6792])).
% 35.90/4.98 fof(f6794,plain,(
% 35.90/4.98 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,double_divide(double_divide(X1,X2),double_divide(X3,inverse(double_divide(X4,double_divide(X1,X4))))))=multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(X6,double_divide(X2,X0)),X3)))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5818,f6793])).
% 35.90/4.98 fof(f6795,plain,(
% 35.90/4.98 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,double_divide(double_divide(X1,X2),double_divide(X3,multiply(double_divide(X1,X4),X4))))=multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(X6,double_divide(X2,X0)),X3)))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5,f6794])).
% 35.90/4.98 fof(f6796,plain,(
% 35.90/4.98 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,double_divide(double_divide(X1,X2),double_divide(X3,inverse(X1))))=multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,double_divide(X2,X0)),X3)))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5614,f6795])).
% 35.90/4.98 fof(f6797,plain,(
% 35.90/4.98 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(X1,X2))=multiply(double_divide(X3,double_divide(X4,X3)),multiply(double_divide(X4,double_divide(X1,X0)),X2)))),
% 35.90/4.98 inference(forward_demodulation,[status(thm)],[f5947,f6796])).
% 35.90/5.02 fof(f6798,plain,(
% 35.90/5.02 ![X0,X1,X2,X3]: (multiply(X0,multiply(X1,X2))=multiply(X3,multiply(double_divide(X3,double_divide(X1,X0)),X2)))),
% 35.90/5.02 inference(forward_demodulation,[status(thm)],[f4937,f6797])).
% 35.90/5.02 fof(f6800,plain,(
% 35.90/5.02 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=double_divide(double_divide(X1,X0),inverse(X2)))),
% 35.90/5.02 inference(forward_demodulation,[status(thm)],[f5388,f6798])).
% 35.90/5.02 fof(f9272,plain,(
% 35.90/5.02 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=double_divide(double_divide(X1,X0),inverse(X2)))),
% 35.90/5.02 inference(forward_demodulation,[status(thm)],[f5659,f5021])).
% 35.90/5.02 fof(f9293,plain,(
% 35.90/5.02 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 35.90/5.02 inference(forward_demodulation,[status(thm)],[f6800,f9272])).
% 35.90/5.02 fof(f9300,plain,(
% 35.90/5.02 ~double_divide(a1,inverse(a1))=multiply(inverse(b1),b1)|~a2=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 35.90/5.02 inference(forward_demodulation,[status(thm)],[f5659,f5036])).
% 35.90/5.02 fof(f9301,plain,(
% 35.90/5.02 ~double_divide(a1,inverse(a1))=double_divide(b1,inverse(b1))|~a2=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 35.90/5.02 inference(forward_demodulation,[status(thm)],[f5659,f9300])).
% 35.90/5.02 fof(f9302,plain,(
% 35.90/5.02 ~double_divide(a1,inverse(a1))=double_divide(b1,inverse(b1))|~a2=a2|~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))),
% 35.90/5.02 inference(forward_demodulation,[status(thm)],[f9293,f9301])).
% 35.90/5.02 fof(f9303,plain,(
% 35.90/5.02 ~double_divide(a1,inverse(a1))=double_divide(b1,inverse(b1))),
% 35.90/5.02 inference(trivial_equality_resolution,[status(thm)],[f9302])).
% 35.90/5.02 fof(f9304,plain,(
% 35.90/5.02 $false),
% 35.90/5.02 inference(forward_subsumption_resolution,[status(thm)],[f9303,f5386])).
% 35.90/5.02 % SZS output end CNFRefutation for theBenchmark.p
% 35.90/5.04 % Elapsed time: 4.653396 seconds
% 35.90/5.04 % CPU time: 36.664957 seconds
% 35.90/5.04 % Total memory used: 295.608 MB
% 35.90/5.04 % Net memory used: 291.755 MB
%------------------------------------------------------------------------------