%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP583-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:36:51 PM UTC 2026
% Result : Unsatisfiable 1.27s 0.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP583-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 20:20:16 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 1.27/0.65 % Refutation found
% 1.27/0.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.27/0.65 % SZS output start CNFRefutation for theBenchmark
% 1.27/0.65 fof(f1,axiom,(
% 1.27/0.65 (![A,B,C]: (double_divide(double_divide(A,double_divide(double_divide(identity,B),double_divide(C,double_divide(B,A)))),double_divide(identity,identity)) = C ))),
% 1.27/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.27/0.65 fof(f2,axiom,(
% 1.27/0.65 (![A,B]: (multiply(A,B) = double_divide(double_divide(B,A),identity) ))),
% 1.27/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.27/0.65 fof(f3,axiom,(
% 1.27/0.65 (![A]: (inverse(A) = double_divide(A,identity) ))),
% 1.27/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.27/0.65 fof(f4,axiom,(
% 1.27/0.65 (![A]: (identity = double_divide(A,inverse(A)) ))),
% 1.27/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.27/0.65 fof(f5,negated_conjecture,(
% 1.27/0.65 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 1.27/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.27/0.65 fof(f6,plain,(
% 1.27/0.65 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))),double_divide(identity,identity))=X2)),
% 1.27/0.65 inference(cnf_transformation,[status(thm)],[f1])).
% 1.27/0.65 fof(f7,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(X0,X1)=double_divide(double_divide(X1,X0),identity))),
% 1.27/0.65 inference(cnf_transformation,[status(thm)],[f2])).
% 1.27/0.65 fof(f8,plain,(
% 1.27/0.65 ![X0]: (inverse(X0)=double_divide(X0,identity))),
% 1.27/0.65 inference(cnf_transformation,[status(thm)],[f3])).
% 1.27/0.65 fof(f9,plain,(
% 1.27/0.65 ![X0]: (identity=double_divide(X0,inverse(X0)))),
% 1.27/0.65 inference(cnf_transformation,[status(thm)],[f4])).
% 1.27/0.65 fof(f10,plain,(
% 1.27/0.65 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 1.27/0.65 inference(cnf_transformation,[status(thm)],[f5])).
% 1.27/0.65 fof(f16,plain,(
% 1.27/0.65 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))),inverse(identity))=X2)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f8,f6])).
% 1.27/0.65 fof(f17,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f8,f7])).
% 1.27/0.65 fof(f18,plain,(
% 1.27/0.65 ![X0]: (multiply(inverse(X0),X0)=inverse(identity))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f9,f17])).
% 1.27/0.65 fof(f19,plain,(
% 1.27/0.65 ![X0]: (multiply(identity,X0)=inverse(inverse(X0)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f8,f17])).
% 1.27/0.65 fof(f20,plain,(
% 1.27/0.65 ![X0,X1]: (identity=double_divide(double_divide(X0,X1),multiply(X1,X0)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f17,f9])).
% 1.27/0.65 fof(f22,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(X0,double_divide(identity,double_divide(X1,double_divide(inverse(identity),X0)))),inverse(identity))=X1)),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f9,f16])).
% 1.27/0.65 fof(f24,plain,(
% 1.27/0.65 ![X0,X1,X2,X3]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0))))),double_divide(X3,X2))),inverse(identity))=X3)),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f16,f16])).
% 1.27/0.65 fof(f25,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X0),double_divide(X1,identity))),inverse(identity))=X1)),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f9,f16])).
% 1.27/0.65 fof(f26,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(identity,X0),double_divide(X1,inverse(X0)))),inverse(identity))=X1)),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f8,f16])).
% 1.27/0.65 fof(f28,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X0),inverse(X1))),inverse(identity))=X1)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f25])).
% 1.27/0.65 fof(f29,plain,(
% 1.27/0.65 ![X0]: (multiply(identity,inverse(X0))=inverse(multiply(identity,X0)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f19,f19])).
% 1.27/0.65 fof(f30,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(identity,double_divide(X0,X1))=inverse(multiply(X1,X0)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f17,f19])).
% 1.27/0.65 fof(f32,plain,(
% 1.27/0.65 ![X0]: (identity=double_divide(inverse(X0),multiply(identity,X0)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f19,f9])).
% 1.27/0.65 fof(f48,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(multiply(identity,X0),double_divide(double_divide(identity,inverse(X0)),double_divide(X1,identity))),inverse(identity))=X1)),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f32,f16])).
% 1.27/0.65 fof(f52,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(multiply(identity,X0),double_divide(double_divide(identity,inverse(X0)),inverse(X1))),inverse(identity))=X1)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f48])).
% 1.27/0.65 fof(f110,plain,(
% 1.27/0.65 ![X0,X1,X2,X3]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(multiply(X2,X3),double_divide(X1,X0))))),identity)),inverse(identity))=double_divide(X3,X2))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f20,f24])).
% 1.27/0.65 fof(f122,plain,(
% 1.27/0.65 ![X0,X1,X2,X3]: (double_divide(double_divide(inverse(identity),inverse(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(multiply(X2,X3),double_divide(X1,X0))))))),inverse(identity))=double_divide(X3,X2))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f110])).
% 1.27/0.65 fof(f124,plain,(
% 1.27/0.65 ![X0,X1,X2,X3]: (double_divide(double_divide(inverse(identity),multiply(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(multiply(X2,X3),double_divide(X1,X0)))),identity)),inverse(identity))=double_divide(X3,X2))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f122])).
% 1.27/0.65 fof(f160,plain,(
% 1.27/0.65 ![X0]: (double_divide(double_divide(inverse(X0),identity),inverse(identity))=double_divide(identity,X0))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f9,f28])).
% 1.27/0.65 fof(f167,plain,(
% 1.27/0.65 ![X0,X1,X2,X3]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(inverse(identity),double_divide(X1,X0))))),X2)),inverse(identity))=double_divide(inverse(X3),double_divide(double_divide(identity,X3),inverse(X2))))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f28,f24])).
% 1.27/0.65 fof(f180,plain,(
% 1.27/0.65 ![X0]: (double_divide(inverse(inverse(X0)),inverse(identity))=double_divide(identity,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f160])).
% 1.27/0.65 fof(f181,plain,(
% 1.27/0.65 ![X0]: (double_divide(multiply(identity,X0),inverse(identity))=double_divide(identity,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f19,f180])).
% 1.27/0.65 fof(f200,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),inverse(identity))=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f26,f26])).
% 1.27/0.65 fof(f201,plain,(
% 1.27/0.65 ![X0,X1,X2,X3]: (double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),inverse(identity))=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1))))),double_divide(X0,X3))))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f24,f26])).
% 1.27/0.65 fof(f204,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),inverse(identity))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(inverse(identity),X1)))))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f22,f26])).
% 1.27/0.65 fof(f205,plain,(
% 1.27/0.65 ![X0,X1,X2]: (double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),inverse(identity))=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f16,f26])).
% 1.27/0.65 fof(f206,plain,(
% 1.27/0.65 ![X0]: (double_divide(double_divide(identity,double_divide(double_divide(identity,X0),identity)),inverse(identity))=X0)),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f9,f26])).
% 1.27/0.65 fof(f208,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(identity,inverse(X0)),double_divide(X1,multiply(identity,X0)))),inverse(identity))=X1)),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f19,f26])).
% 1.27/0.65 fof(f217,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(inverse(identity),double_divide(identity,double_divide(double_divide(identity,X0),double_divide(X1,inverse(X0)))))=inverse(X1))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f26,f17])).
% 1.27/0.65 fof(f219,plain,(
% 1.27/0.65 ![X0]: (double_divide(double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)),inverse(identity))=X0)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f221,f26])).
% 1.27/0.65 fof(f221,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f200])).
% 1.27/0.65 fof(f227,plain,(
% 1.27/0.65 ![X0,X1,X2,X3]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1))))),double_divide(X0,X3))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f201])).
% 1.27/0.65 fof(f240,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(inverse(identity),X1)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f204])).
% 1.27/0.65 fof(f243,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),inverse(identity))),X0)),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f249,f167])).
% 1.27/0.65 fof(f246,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(inverse(identity),multiply(double_divide(double_divide(identity,double_divide(inverse(identity),multiply(X0,X1))),inverse(identity)),identity)),inverse(identity))=double_divide(X1,X0))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f249,f124])).
% 1.27/0.65 fof(f247,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),inverse(identity))),double_divide(X0,X1))))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f249,f227])).
% 1.27/0.65 fof(f249,plain,(
% 1.27/0.65 ![X0,X1,X2]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f205])).
% 1.27/0.65 fof(f250,plain,(
% 1.27/0.65 ![X0]: (double_divide(double_divide(identity,inverse(double_divide(identity,X0))),inverse(identity))=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f206])).
% 1.27/0.65 fof(f251,plain,(
% 1.27/0.65 ![X0]: (double_divide(double_divide(identity,multiply(X0,identity)),inverse(identity))=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f250])).
% 1.27/0.65 fof(f263,plain,(
% 1.27/0.65 ![X0]: (multiply(inverse(identity),double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)))=inverse(X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f221,f217])).
% 1.27/0.65 fof(f302,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(inverse(multiply(X0,X1)),inverse(identity))=double_divide(identity,double_divide(X1,X0)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f30,f181])).
% 1.27/0.65 fof(f306,plain,(
% 1.27/0.65 ![X0]: (multiply(inverse(identity),multiply(identity,X0))=inverse(double_divide(identity,X0)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f181,f17])).
% 1.27/0.65 fof(f311,plain,(
% 1.27/0.65 ![X0]: (multiply(inverse(identity),multiply(identity,X0))=multiply(X0,identity))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f306])).
% 1.27/0.65 fof(f352,plain,(
% 1.27/0.65 double_divide(double_divide(identity,inverse(identity)),inverse(identity))=inverse(identity)),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f18,f251])).
% 1.27/0.65 fof(f353,plain,(
% 1.27/0.65 ![X0]: (double_divide(double_divide(inverse(multiply(X0,identity)),X0),inverse(identity))=identity)),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f251,f28])).
% 1.27/0.65 fof(f359,plain,(
% 1.27/0.65 double_divide(identity,inverse(identity))=inverse(identity)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f9,f352])).
% 1.27/0.65 fof(f360,plain,(
% 1.27/0.65 ![X0]: (double_divide(double_divide(identity,multiply(X0,identity)),identity)=X0)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f251])).
% 1.27/0.65 fof(f362,plain,(
% 1.27/0.65 ![X0]: (double_divide(multiply(identity,X0),identity)=double_divide(identity,X0))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f181])).
% 1.27/0.65 fof(f363,plain,(
% 1.27/0.65 ![X0]: (double_divide(double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)),identity)=X0)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f219])).
% 1.27/0.65 fof(f365,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X0),inverse(X1))),identity)=X1)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f28])).
% 1.27/0.65 fof(f367,plain,(
% 1.27/0.65 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f18])).
% 1.27/0.65 fof(f370,plain,(
% 1.27/0.65 ![X0]: (multiply(identity,multiply(identity,X0))=multiply(X0,identity))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f311])).
% 1.27/0.65 fof(f371,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(inverse(multiply(X0,X1)),identity)=double_divide(identity,double_divide(X1,X0)))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f302])).
% 1.27/0.65 fof(f373,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f247])).
% 1.27/0.65 fof(f374,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(inverse(identity),multiply(double_divide(double_divide(identity,double_divide(inverse(identity),multiply(X0,X1))),inverse(identity)),identity)),identity)=double_divide(X1,X0))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f246])).
% 1.27/0.65 fof(f376,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),inverse(identity))),X0)),identity)=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f243])).
% 1.27/0.65 fof(f377,plain,(
% 1.27/0.65 ![X0]: (multiply(inverse(identity),double_divide(double_divide(identity,double_divide(inverse(identity),X0)),identity))=inverse(X0))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f263])).
% 1.27/0.65 fof(f380,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(identity,inverse(X0)),double_divide(X1,multiply(identity,X0)))),identity)=X1)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f208])).
% 1.27/0.65 fof(f382,plain,(
% 1.27/0.65 ![X0,X1,X2]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),identity)=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f249])).
% 1.27/0.65 fof(f383,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f240])).
% 1.27/0.65 fof(f403,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(multiply(identity,X0),double_divide(double_divide(identity,inverse(X0)),inverse(X1))),identity)=X1)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f404,f52])).
% 1.27/0.65 fof(f404,plain,(
% 1.27/0.65 identity=inverse(identity)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f9,f359])).
% 1.27/0.65 fof(f405,plain,(
% 1.27/0.65 ![X0]: (double_divide(double_divide(inverse(multiply(X0,identity)),X0),identity)=identity)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f353])).
% 1.27/0.65 fof(f406,plain,(
% 1.27/0.65 ![X0]: (inverse(double_divide(inverse(multiply(X0,identity)),X0))=identity)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f405])).
% 1.27/0.65 fof(f407,plain,(
% 1.27/0.65 ![X0]: (multiply(X0,inverse(multiply(X0,identity)))=identity)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f406])).
% 1.27/0.65 fof(f426,plain,(
% 1.27/0.65 ![X0]: (inverse(double_divide(identity,multiply(X0,identity)))=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f360])).
% 1.27/0.65 fof(f429,plain,(
% 1.27/0.65 ![X0]: (multiply(multiply(X0,identity),identity)=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f426])).
% 1.27/0.65 fof(f432,plain,(
% 1.27/0.65 ![X0]: (multiply(identity,inverse(X0))=double_divide(identity,X0))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f433,f29])).
% 1.27/0.65 fof(f433,plain,(
% 1.27/0.65 ![X0]: (inverse(multiply(identity,X0))=double_divide(identity,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f362])).
% 1.27/0.65 fof(f434,plain,(
% 1.27/0.65 ![X0]: (inverse(double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)))=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f363])).
% 1.27/0.65 fof(f435,plain,(
% 1.27/0.65 ![X0]: (multiply(inverse(identity),double_divide(identity,double_divide(inverse(identity),X0)))=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f434])).
% 1.27/0.65 fof(f436,plain,(
% 1.27/0.65 ![X0]: (multiply(identity,double_divide(identity,double_divide(inverse(identity),X0)))=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f435])).
% 1.27/0.65 fof(f437,plain,(
% 1.27/0.65 ![X0]: (inverse(multiply(double_divide(inverse(identity),X0),identity))=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f30,f436])).
% 1.27/0.65 fof(f438,plain,(
% 1.27/0.65 ![X0]: (inverse(multiply(double_divide(identity,X0),identity))=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f437])).
% 1.27/0.65 fof(f439,plain,(
% 1.27/0.65 ![X0,X1]: (inverse(double_divide(inverse(X0),double_divide(double_divide(identity,X0),inverse(X1))))=X1)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f365])).
% 1.27/0.65 fof(f440,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(double_divide(identity,X0),inverse(X1)),inverse(X0))=X1)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f439])).
% 1.27/0.65 fof(f446,plain,(
% 1.27/0.65 ![X0,X1]: (inverse(inverse(multiply(X0,X1)))=double_divide(identity,double_divide(X1,X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f371])).
% 1.27/0.65 fof(f447,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,double_divide(X0,identity))=multiply(X0,identity))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f448,f370])).
% 1.27/0.65 fof(f448,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(identity,multiply(X0,X1))=double_divide(identity,double_divide(X1,X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f19,f446])).
% 1.27/0.65 fof(f452,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(identity,X0)),inverse(identity))=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f373])).
% 1.27/0.65 fof(f453,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(identity,X0)),identity)=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f452])).
% 1.27/0.65 fof(f454,plain,(
% 1.27/0.65 ![X0,X1]: (inverse(double_divide(identity,double_divide(identity,X0)))=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f453])).
% 1.27/0.65 fof(f455,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f454])).
% 1.27/0.65 fof(f456,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f455])).
% 1.27/0.65 fof(f457,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(double_divide(identity,inverse(double_divide(identity,double_divide(inverse(identity),X1)))),double_divide(X0,X1))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f456])).
% 1.27/0.65 fof(f458,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(inverse(identity),X1),identity)),double_divide(X0,X1))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f457])).
% 1.27/0.65 fof(f459,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,X1),identity)),double_divide(X0,X1))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f458])).
% 1.27/0.65 fof(f460,plain,(
% 1.27/0.65 ![X0,X1]: (inverse(double_divide(inverse(identity),multiply(double_divide(double_divide(identity,double_divide(inverse(identity),multiply(X0,X1))),inverse(identity)),identity)))=double_divide(X1,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f374])).
% 1.27/0.65 fof(f461,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(multiply(double_divide(double_divide(identity,double_divide(inverse(identity),multiply(X0,X1))),inverse(identity)),identity),inverse(identity))=double_divide(X1,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f460])).
% 1.27/0.65 fof(f462,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(multiply(double_divide(double_divide(identity,double_divide(identity,multiply(X0,X1))),inverse(identity)),identity),inverse(identity))=double_divide(X1,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f461])).
% 1.27/0.65 fof(f463,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(multiply(double_divide(double_divide(identity,double_divide(identity,multiply(X0,X1))),identity),identity),inverse(identity))=double_divide(X1,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f462])).
% 1.27/0.65 fof(f464,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(multiply(inverse(double_divide(identity,double_divide(identity,multiply(X0,X1)))),identity),inverse(identity))=double_divide(X1,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f463])).
% 1.27/0.65 fof(f465,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(multiply(multiply(double_divide(identity,multiply(X0,X1)),identity),identity),inverse(identity))=double_divide(X1,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f464])).
% 1.27/0.65 fof(f466,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(identity,multiply(X0,X1)),inverse(identity))=double_divide(X1,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f429,f465])).
% 1.27/0.65 fof(f467,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(identity,multiply(X0,X1)),identity)=double_divide(X1,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f466])).
% 1.27/0.65 fof(f476,plain,(
% 1.27/0.65 ![X0,X1]: (inverse(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),inverse(identity))),X0)))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f376])).
% 1.27/0.65 fof(f477,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),inverse(identity))),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f476])).
% 1.27/0.65 fof(f478,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(identity,inverse(identity))),inverse(identity))),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f477])).
% 1.27/0.65 fof(f479,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(double_divide(identity,double_divide(double_divide(identity,identity),inverse(identity))),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f9,f478])).
% 1.27/0.65 fof(f480,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f479])).
% 1.27/0.65 fof(f481,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(double_divide(identity,double_divide(identity,inverse(identity))),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f480])).
% 1.27/0.65 fof(f482,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(double_divide(identity,identity),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f9,f481])).
% 1.27/0.65 fof(f483,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(inverse(identity),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f482])).
% 1.27/0.65 fof(f484,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(identity,X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f483])).
% 1.27/0.65 fof(f485,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f484])).
% 1.27/0.65 fof(f486,plain,(
% 1.27/0.65 ![X0]: (multiply(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X0)),identity))=inverse(X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f377])).
% 1.27/0.65 fof(f487,plain,(
% 1.27/0.65 ![X0]: (inverse(multiply(identity,double_divide(identity,double_divide(inverse(identity),X0))))=inverse(X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f30,f486])).
% 1.27/0.65 fof(f488,plain,(
% 1.27/0.65 ![X0]: (multiply(identity,inverse(double_divide(identity,double_divide(inverse(identity),X0))))=inverse(X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f29,f487])).
% 1.27/0.65 fof(f489,plain,(
% 1.27/0.65 ![X0]: (multiply(identity,multiply(double_divide(inverse(identity),X0),identity))=inverse(X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f488])).
% 1.27/0.65 fof(f490,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,double_divide(identity,double_divide(inverse(identity),X0)))=inverse(X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f448,f489])).
% 1.27/0.65 fof(f491,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,double_divide(identity,double_divide(identity,X0)))=inverse(X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f490])).
% 1.27/0.65 fof(f507,plain,(
% 1.27/0.65 ![X0,X1]: (inverse(double_divide(identity,double_divide(double_divide(identity,inverse(X0)),double_divide(X1,multiply(identity,X0)))))=X1)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f380])).
% 1.27/0.65 fof(f508,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(double_divide(identity,inverse(X0)),double_divide(X1,multiply(identity,X0))),identity)=X1)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f507])).
% 1.27/0.65 fof(f511,plain,(
% 1.27/0.65 ![X0,X1,X2]: (inverse(double_divide(identity,double_divide(inverse(identity),X0)))=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f382])).
% 1.27/0.65 fof(f512,plain,(
% 1.27/0.65 ![X0,X1,X2]: (multiply(double_divide(inverse(identity),X0),identity)=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f511])).
% 1.27/0.65 fof(f513,plain,(
% 1.27/0.65 ![X0,X1,X2]: (multiply(double_divide(identity,X0),identity)=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f512])).
% 1.27/0.65 fof(f514,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(identity,X0)),inverse(identity))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f383])).
% 1.27/0.65 fof(f515,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(identity,double_divide(identity,X0)),identity)=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f514])).
% 1.27/0.65 fof(f516,plain,(
% 1.27/0.65 ![X0,X1]: (inverse(double_divide(identity,double_divide(identity,X0)))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f515])).
% 1.27/0.65 fof(f517,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f516])).
% 1.27/0.65 fof(f572,plain,(
% 1.27/0.65 ![X0,X1]: (inverse(double_divide(multiply(identity,X0),double_divide(double_divide(identity,inverse(X0)),inverse(X1))))=X1)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f403])).
% 1.27/0.65 fof(f573,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(double_divide(identity,inverse(X0)),inverse(X1)),multiply(identity,X0))=X1)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f572])).
% 1.27/0.65 fof(f581,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(multiply(X0,identity),inverse(X1)),multiply(identity,X0))=X1)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f586,f573])).
% 1.27/0.65 fof(f584,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(multiply(X0,identity),double_divide(X1,multiply(identity,X0))),identity)=X1)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f586,f508])).
% 1.27/0.65 fof(f586,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,inverse(X0))=multiply(X0,identity))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f447])).
% 1.27/0.65 fof(f616,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(double_divide(identity,X0),X1),inverse(X0))=multiply(double_divide(identity,X1),identity))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f438,f440])).
% 1.27/0.65 fof(f651,plain,(
% 1.27/0.65 ![X0]: (identity=double_divide(double_divide(identity,multiply(X0,identity)),X0))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f429,f20])).
% 1.27/0.65 fof(f704,plain,(
% 1.27/0.65 ![X0]: (multiply(double_divide(identity,X0),X0)=identity)),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f438,f407])).
% 1.27/0.65 fof(f813,plain,(
% 1.27/0.65 ![X0]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(double_divide(identity,identity),double_divide(X0,identity))))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f704,f459])).
% 1.27/0.65 fof(f818,plain,(
% 1.27/0.65 ![X0]: (multiply(double_divide(identity,inverse(X0)),identity)=double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,multiply(identity,X0)),identity)),identity)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f32,f459])).
% 1.27/0.65 fof(f819,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(identity,double_divide(X0,X1)),identity)=double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,multiply(X1,X0)),identity)),identity)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f20,f459])).
% 1.27/0.65 fof(f828,plain,(
% 1.27/0.65 ![X0]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(inverse(identity),double_divide(X0,identity))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f813])).
% 1.27/0.65 fof(f829,plain,(
% 1.27/0.65 ![X0]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(identity,double_divide(X0,identity))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f404,f828])).
% 1.27/0.65 fof(f830,plain,(
% 1.27/0.65 ![X0]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(identity,inverse(X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f829])).
% 1.27/0.65 fof(f833,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,multiply(multiply(X0,X1),identity))=double_divide(X1,X0))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f844,f467])).
% 1.27/0.65 fof(f837,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(double_divide(identity,X0),X1),inverse(X0))=double_divide(identity,multiply(X1,identity)))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f844,f616])).
% 1.27/0.65 fof(f841,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,multiply(X0,identity))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f844,f517])).
% 1.27/0.65 fof(f842,plain,(
% 1.27/0.65 ![X0,X1,X2]: (double_divide(identity,multiply(X0,identity))=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f844,f513])).
% 1.27/0.65 fof(f843,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,multiply(X0,identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f844,f485])).
% 1.27/0.65 fof(f844,plain,(
% 1.27/0.65 ![X0]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,multiply(X0,identity)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f586,f830])).
% 1.27/0.65 fof(f861,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,multiply(identity,X0)),identity)),identity)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f844,f818])).
% 1.27/0.65 fof(f862,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=double_divide(identity,inverse(double_divide(identity,multiply(double_divide(identity,multiply(identity,X0)),identity)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f861])).
% 1.27/0.65 fof(f863,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=multiply(double_divide(identity,multiply(double_divide(identity,multiply(identity,X0)),identity)),identity))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f586,f862])).
% 1.27/0.65 fof(f864,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=double_divide(identity,double_divide(identity,multiply(identity,X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f467,f863])).
% 1.27/0.65 fof(f865,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,multiply(double_divide(X0,X1),identity))=double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,multiply(X1,X0)),identity)),identity)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f844,f819])).
% 1.27/0.65 fof(f866,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,multiply(double_divide(X0,X1),identity))=double_divide(identity,inverse(double_divide(identity,multiply(double_divide(identity,multiply(X1,X0)),identity)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f865])).
% 1.27/0.65 fof(f867,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,multiply(double_divide(X0,X1),identity))=multiply(double_divide(identity,multiply(double_divide(identity,multiply(X1,X0)),identity)),identity))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f586,f866])).
% 1.27/0.65 fof(f868,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,multiply(double_divide(X0,X1),identity))=double_divide(identity,double_divide(identity,multiply(X1,X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f467,f867])).
% 1.27/0.65 fof(f931,plain,(
% 1.27/0.65 ![X0]: (multiply(double_divide(identity,double_divide(identity,X0)),identity)=inverse(inverse(X0)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f491,f17])).
% 1.27/0.65 fof(f946,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(double_divide(identity,X0),identity))=inverse(inverse(X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f844,f931])).
% 1.27/0.65 fof(f947,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,double_divide(identity,multiply(X0,identity)))=inverse(inverse(X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f868,f946])).
% 1.27/0.65 fof(f952,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,double_divide(identity,multiply(X0,identity)))=multiply(identity,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f19,f947])).
% 1.27/0.65 fof(f956,plain,(
% 1.27/0.65 ![X0]: (multiply(identity,double_divide(identity,X0))=double_divide(identity,multiply(identity,X0)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f433,f432])).
% 1.27/0.65 fof(f969,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=double_divide(identity,inverse(multiply(X0,identity))))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f972,f864])).
% 1.27/0.65 fof(f972,plain,(
% 1.27/0.65 ![X0]: (inverse(multiply(X0,identity))=double_divide(identity,multiply(identity,X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f30,f956])).
% 1.27/0.65 fof(f986,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=multiply(multiply(X0,identity),identity))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f586,f969])).
% 1.27/0.65 fof(f987,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f429,f986])).
% 1.27/0.65 fof(f1090,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(identity,X0))=multiply(inverse(X0),identity))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f19,f586])).
% 1.27/0.65 fof(f1091,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,multiply(X0,X1))=multiply(double_divide(X1,X0),identity))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f17,f586])).
% 1.27/0.65 fof(f1098,plain,(
% 1.27/0.65 ![X0]: (multiply(inverse(X0),identity)=inverse(multiply(X0,identity)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f586,f17])).
% 1.27/0.65 fof(f1107,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,multiply(double_divide(X0,multiply(identity,X1)),multiply(X1,identity)))=X0)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1091,f584])).
% 1.27/0.65 fof(f1203,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(identity,identity))=double_divide(X0,double_divide(identity,X0)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f704,f833])).
% 1.27/0.65 fof(f1215,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,double_divide(identity,double_divide(X0,X1)))=inverse(multiply(multiply(X1,X0),identity)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f833,f491])).
% 1.27/0.65 fof(f1221,plain,(
% 1.27/0.65 ![X0]: (multiply(inverse(identity),identity)=double_divide(X0,double_divide(identity,X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1090,f1203])).
% 1.27/0.65 fof(f1223,plain,(
% 1.27/0.65 ![X0]: (identity=double_divide(X0,double_divide(identity,X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f367,f1221])).
% 1.27/0.65 fof(f1247,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,double_divide(identity,double_divide(X0,X1)))=multiply(inverse(multiply(X1,X0)),identity))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1098,f1215])).
% 1.27/0.65 fof(f1289,plain,(
% 1.27/0.65 ![X0]: (multiply(identity,inverse(X0))=double_divide(identity,multiply(double_divide(identity,double_divide(identity,X0)),identity)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1223,f837])).
% 1.27/0.65 fof(f1293,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(multiply(X0,identity),X1),inverse(inverse(X0)))=double_divide(identity,multiply(X1,identity)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f586,f837])).
% 1.27/0.65 fof(f1301,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,multiply(double_divide(identity,multiply(X0,identity)),identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),X0)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f837,f833])).
% 1.27/0.65 fof(f1305,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,X0)=double_divide(identity,multiply(double_divide(identity,double_divide(identity,X0)),identity)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f432,f1289])).
% 1.27/0.65 fof(f1306,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,X0)=double_divide(identity,double_divide(identity,multiply(double_divide(identity,X0),identity))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1091,f1305])).
% 1.27/0.65 fof(f1307,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,X0)=multiply(identity,double_divide(identity,X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f952,f1306])).
% 1.27/0.65 fof(f1308,plain,(
% 1.27/0.65 ![X0]: (multiply(inverse(X0),identity)=double_divide(identity,X0))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1309,f1098])).
% 1.27/0.65 fof(f1309,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,X0)=inverse(multiply(X0,identity)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f30,f1307])).
% 1.27/0.65 fof(f1315,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=X0)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1316,f581])).
% 1.27/0.65 fof(f1316,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(multiply(X0,identity),X1),multiply(identity,X0))=double_divide(identity,multiply(X1,identity)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f19,f1293])).
% 1.27/0.65 fof(f1328,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,double_divide(identity,multiply(multiply(X0,identity),identity)))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1091,f1301])).
% 1.27/0.65 fof(f1329,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(identity,multiply(X0,identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f952,f1328])).
% 1.27/0.65 fof(f1330,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(X0,identity))=double_divide(identity,double_divide(identity,inverse(X0))))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1331,f843])).
% 1.27/0.65 fof(f1331,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,double_divide(identity,X0))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f448,f1329])).
% 1.27/0.65 fof(f1336,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(identity,double_divide(identity,double_divide(X0,X1)))=double_divide(identity,multiply(X1,X0)))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1308,f1247])).
% 1.27/0.65 fof(f1344,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(identity,X0))=double_divide(identity,X0))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1308,f1090])).
% 1.27/0.65 fof(f1345,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,double_divide(identity,X0))=X0)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1308,f987])).
% 1.27/0.65 fof(f1347,plain,(
% 1.27/0.65 ![X0]: (multiply(X0,identity)=multiply(identity,X0))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1352,f952])).
% 1.27/0.65 fof(f1349,plain,(
% 1.27/0.65 ![X0,X1]: (X0=double_divide(inverse(X1),double_divide(double_divide(identity,X1),X0)))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1352,f1331])).
% 1.27/0.65 fof(f1352,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,double_divide(identity,X0))=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1308,f1315])).
% 1.27/0.65 fof(f1356,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(multiply(X0,identity),X1),multiply(identity,X0))=inverse(X1))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1367,f1316])).
% 1.27/0.65 fof(f1361,plain,(
% 1.27/0.65 ![X0,X1,X2]: (inverse(X0)=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1367,f842])).
% 1.27/0.65 fof(f1362,plain,(
% 1.27/0.65 ![X0,X1]: (inverse(X0)=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1367,f841])).
% 1.27/0.65 fof(f1366,plain,(
% 1.27/0.65 ![X0]: (identity=double_divide(inverse(X0),X0))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1367,f651])).
% 1.27/0.65 fof(f1367,plain,(
% 1.27/0.65 ![X0]: (double_divide(identity,multiply(X0,identity))=inverse(X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1352,f1330])).
% 1.27/0.65 fof(f1368,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(multiply(X0,identity),double_divide(X1,multiply(identity,X0)))=X1)),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1374,f1107])).
% 1.27/0.65 fof(f1374,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(X0,X1)=double_divide(identity,multiply(X1,X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1352,f1336])).
% 1.27/0.65 fof(f1378,plain,(
% 1.27/0.65 ![X0]: (double_divide(X0,identity)=double_divide(identity,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1374,f1344])).
% 1.27/0.65 fof(f1379,plain,(
% 1.27/0.65 ![X0]: (inverse(inverse(X0))=multiply(X0,identity))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1401,f586])).
% 1.27/0.65 fof(f1401,plain,(
% 1.27/0.65 ![X0]: (inverse(X0)=double_divide(identity,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f1378])).
% 1.27/0.65 fof(f1402,plain,(
% 1.27/0.65 ![X0]: (inverse(double_divide(identity,X0))=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1401,f1345])).
% 1.27/0.65 fof(f1411,plain,(
% 1.27/0.65 ![X0]: (multiply(X0,identity)=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f1402])).
% 1.27/0.65 fof(f1419,plain,(
% 1.27/0.65 ![X0]: (X0=multiply(identity,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1411,f1347])).
% 1.27/0.65 fof(f1421,plain,(
% 1.27/0.65 ![X0,X1]: (X0=double_divide(inverse(X1),double_divide(inverse(X1),X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1401,f1349])).
% 1.27/0.65 fof(f1424,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(X0,X1),multiply(identity,X0))=inverse(X1))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1411,f1356])).
% 1.27/0.65 fof(f1426,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(double_divide(X0,X1),X0)=inverse(X1))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1419,f1424])).
% 1.27/0.65 fof(f1430,plain,(
% 1.27/0.65 ![X0,X1,X2]: (inverse(X0)=double_divide(X1,double_divide(inverse(X2),double_divide(X0,double_divide(X2,X1)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1401,f1361])).
% 1.27/0.65 fof(f1431,plain,(
% 1.27/0.65 ![X0,X1]: (inverse(X0)=double_divide(X1,inverse(double_divide(X0,double_divide(identity,X1)))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1401,f1362])).
% 1.27/0.65 fof(f1432,plain,(
% 1.27/0.65 ![X0,X1]: (inverse(X0)=double_divide(X1,multiply(double_divide(identity,X1),X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f1431])).
% 1.27/0.65 fof(f1433,plain,(
% 1.27/0.65 ![X0,X1]: (inverse(X0)=double_divide(X1,multiply(inverse(X1),X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1401,f1432])).
% 1.27/0.65 fof(f1440,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(X0,double_divide(X1,multiply(identity,X0)))=X1)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1411,f1368])).
% 1.27/0.65 fof(f1442,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(X0,double_divide(X1,X0))=X1)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1419,f1440])).
% 1.27/0.65 fof(f1452,plain,(
% 1.27/0.65 ![X0]: (inverse(inverse(X0))=X0)),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1411,f1379])).
% 1.27/0.65 fof(f1500,plain,(
% 1.27/0.65 ![X0,X1,X2]: (inverse(X0)=double_divide(double_divide(X1,double_divide(X2,X0)),double_divide(inverse(inverse(X2)),inverse(X1))))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1430,f1430])).
% 1.27/0.65 fof(f1512,plain,(
% 1.27/0.65 ![X0,X1,X2]: (inverse(X0)=double_divide(double_divide(X1,double_divide(X2,X0)),double_divide(X2,inverse(X1))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1452,f1500])).
% 1.27/0.65 fof(f1534,plain,(
% 1.27/0.65 ![X0,X1,X2]: (inverse(X0)=double_divide(double_divide(X1,X2),multiply(multiply(X2,X1),X0)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f17,f1433])).
% 1.27/0.65 fof(f1623,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(double_divide(X0,X1),X0)=X1)),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1442,f1442])).
% 1.27/0.65 fof(f1645,plain,(
% 1.27/0.65 ![X0,X1]: (inverse(inverse(double_divide(X0,X1)))=double_divide(X1,double_divide(inverse(X0),identity)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1366,f1430])).
% 1.27/0.65 fof(f1653,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(X0,X1)=double_divide(X1,double_divide(inverse(X0),identity)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1452,f1645])).
% 1.27/0.65 fof(f1654,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(X0,X1)=double_divide(X1,inverse(inverse(X0))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f8,f1653])).
% 1.27/0.65 fof(f1655,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(X0,X1)=double_divide(X1,X0))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1452,f1654])).
% 1.27/0.65 fof(f1665,plain,(
% 1.27/0.65 ![X0,X1]: (X0=double_divide(X1,double_divide(inverse(inverse(X1)),X0)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1452,f1421])).
% 1.27/0.65 fof(f1671,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=double_divide(inverse(X0),inverse(X1)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1433,f1421])).
% 1.27/0.65 fof(f1672,plain,(
% 1.27/0.65 ![X0,X1,X2]: (double_divide(inverse(X0),double_divide(X1,double_divide(X0,inverse(X2))))=double_divide(inverse(X2),inverse(X1)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1430,f1421])).
% 1.27/0.65 fof(f1685,plain,(
% 1.27/0.65 ![X0,X1,X2]: (inverse(X0)=double_divide(double_divide(inverse(X1),X2),double_divide(inverse(inverse(X1)),double_divide(X0,X2))))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1421,f1430])).
% 1.27/0.65 fof(f1692,plain,(
% 1.27/0.65 ![X0,X1]: (X0=double_divide(X1,double_divide(X1,X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1452,f1665])).
% 1.27/0.65 fof(f1699,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(X0,X1)=double_divide(inverse(X0),inverse(X1)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1452,f1671])).
% 1.27/0.65 fof(f1700,plain,(
% 1.27/0.65 ![X0,X1,X2]: (double_divide(inverse(X0),double_divide(X1,double_divide(X0,inverse(X2))))=multiply(X2,X1))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1699,f1672])).
% 1.27/0.65 fof(f1713,plain,(
% 1.27/0.65 ![X0,X1,X2]: (inverse(X0)=double_divide(double_divide(inverse(X1),X2),double_divide(X1,double_divide(X0,X2))))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1452,f1685])).
% 1.27/0.65 fof(f1721,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(inverse(X0),X1)=multiply(inverse(X1),X0))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1433,f1623])).
% 1.27/0.65 fof(f1722,plain,(
% 1.27/0.65 ![X0,X1,X2]: (double_divide(inverse(X0),X1)=double_divide(inverse(X2),double_divide(X0,double_divide(X2,X1))))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1430,f1623])).
% 1.27/0.65 fof(f1726,plain,(
% 1.27/0.65 ![X0,X1,X2]: (inverse(double_divide(double_divide(X0,X1),X2))=double_divide(X1,double_divide(inverse(X0),X2)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1623,f1430])).
% 1.27/0.65 fof(f1732,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(X0,double_divide(X0,X1))=inverse(X1))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1623,f17])).
% 1.27/0.65 fof(f1743,plain,(
% 1.27/0.65 ![X0,X1]: (double_divide(inverse(X0),inverse(X1))=multiply(X1,X0))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f1722,f1700])).
% 1.27/0.65 fof(f1750,plain,(
% 1.27/0.65 ![X0,X1,X2]: (multiply(X0,double_divide(X1,X2))=double_divide(X2,double_divide(inverse(X1),X0)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f17,f1726])).
% 1.27/0.65 fof(f1816,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X0,X1)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1655,f17])).
% 1.27/0.65 fof(f2181,plain,(
% 1.27/0.65 ![X0,X1,X2]: (double_divide(double_divide(X0,inverse(X1)),inverse(X2))=double_divide(X1,double_divide(X0,X2)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1512,f1442])).
% 1.27/0.65 fof(f2423,plain,(
% 1.27/0.65 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=double_divide(double_divide(X1,X0),inverse(X2)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1534,f1692])).
% 1.27/0.65 fof(f2425,plain,(
% 1.27/0.65 ![X0,X1,X2]: (double_divide(inverse(X0),double_divide(X1,X2))=multiply(multiply(X2,X1),X0))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1534,f1623])).
% 1.27/0.65 fof(f2487,plain,(
% 1.27/0.65 ![X0,X1,X2]: (multiply(multiply(inverse(X0),X1),X2)=double_divide(X0,double_divide(X1,X2)))),
% 1.27/0.65 inference(backward_demodulation,[status(thm)],[f2423,f2181])).
% 1.27/0.65 fof(f2506,plain,(
% 1.27/0.65 ![X0,X1,X2]: (multiply(double_divide(inverse(X0),X1),X2)=double_divide(X1,double_divide(X0,X2)))),
% 1.27/0.65 inference(forward_demodulation,[status(thm)],[f1721,f2487])).
% 1.27/0.65 fof(f2556,plain,(
% 1.27/0.65 ![X0,X1]: (multiply(inverse(X0),X1)=double_divide(X0,inverse(X1)))),
% 1.27/0.65 inference(paramodulation,[status(thm)],[f1452,f1699])).
% 1.27/0.66 fof(f2688,plain,(
% 1.27/0.66 ![X0,X1,X2]: (multiply(double_divide(inverse(X0),X1),inverse(X2))=inverse(double_divide(X0,double_divide(X2,X1))))),
% 1.27/0.66 inference(paramodulation,[status(thm)],[f1713,f1732])).
% 1.27/0.66 fof(f2692,plain,(
% 1.27/0.66 ![X0,X1,X2]: (multiply(inverse(X0),double_divide(inverse(X1),X2))=inverse(double_divide(X1,double_divide(X0,X2))))),
% 1.27/0.66 inference(paramodulation,[status(thm)],[f1713,f1426])).
% 1.27/0.66 fof(f2770,plain,(
% 1.27/0.66 ![X0,X1,X2]: (double_divide(X0,double_divide(X1,inverse(X2)))=inverse(double_divide(X1,double_divide(X2,X0))))),
% 1.27/0.66 inference(forward_demodulation,[status(thm)],[f2506,f2688])).
% 1.27/0.66 fof(f2777,plain,(
% 1.27/0.66 ![X0,X1,X2]: (double_divide(X0,double_divide(X1,inverse(X2)))=multiply(X1,double_divide(X2,X0)))),
% 1.27/0.66 inference(forward_demodulation,[status(thm)],[f1816,f2770])).
% 1.27/0.66 fof(f2789,plain,(
% 1.27/0.66 ![X0,X1,X2]: (double_divide(X0,inverse(double_divide(inverse(X1),X2)))=inverse(double_divide(X1,double_divide(X0,X2))))),
% 1.27/0.66 inference(forward_demodulation,[status(thm)],[f2556,f2692])).
% 1.27/0.66 fof(f2790,plain,(
% 1.27/0.66 ![X0,X1,X2]: (double_divide(X0,multiply(inverse(X1),X2))=inverse(double_divide(X1,double_divide(X0,X2))))),
% 1.27/0.66 inference(forward_demodulation,[status(thm)],[f1816,f2789])).
% 1.27/0.66 fof(f2791,plain,(
% 1.27/0.66 ![X0,X1,X2]: (double_divide(X0,double_divide(X1,inverse(X2)))=inverse(double_divide(X1,double_divide(X0,X2))))),
% 1.27/0.66 inference(forward_demodulation,[status(thm)],[f2556,f2790])).
% 1.27/0.66 fof(f2792,plain,(
% 1.27/0.66 ![X0,X1,X2]: (multiply(X0,double_divide(X1,X2))=inverse(double_divide(X0,double_divide(X2,X1))))),
% 1.27/0.66 inference(forward_demodulation,[status(thm)],[f2777,f2791])).
% 1.27/0.66 fof(f2793,plain,(
% 1.27/0.66 ![X0,X1,X2]: (multiply(X0,double_divide(X1,X2))=multiply(X0,double_divide(X2,X1)))),
% 1.27/0.66 inference(forward_demodulation,[status(thm)],[f1816,f2792])).
% 1.27/0.66 fof(f2985,plain,(
% 1.27/0.66 ![X0,X1,X2]: (multiply(X0,double_divide(inverse(X1),X2))=double_divide(X2,double_divide(X1,X0)))),
% 1.27/0.66 inference(paramodulation,[status(thm)],[f1452,f1750])).
% 1.27/0.66 fof(f4870,plain,(
% 1.27/0.66 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(X0,double_divide(inverse(X1),inverse(X2))))),
% 1.27/0.67 inference(paramodulation,[status(thm)],[f1743,f2793])).
% 1.27/0.67 fof(f4952,plain,(
% 1.27/0.67 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 1.27/0.67 inference(backward_demodulation,[status(thm)],[f4954,f2425])).
% 1.27/0.67 fof(f4954,plain,(
% 1.27/0.67 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=double_divide(inverse(X2),double_divide(X1,X0)))),
% 1.27/0.67 inference(forward_demodulation,[status(thm)],[f2985,f4870])).
% 1.27/0.67 fof(f5032,plain,(
% 1.27/0.67 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))),
% 1.27/0.67 inference(backward_demodulation,[status(thm)],[f4952,f10])).
% 1.27/0.67 fof(f5055,plain,(
% 1.27/0.67 $false),
% 1.27/0.67 inference(trivial_equality_resolution,[status(thm)],[f5032])).
% 1.27/0.67 % SZS output end CNFRefutation for theBenchmark.p
% 1.27/0.67 % Elapsed time: 0.299416 seconds
% 1.27/0.67 % CPU time: 2.184218 seconds
% 1.27/0.67 % Total memory used: 52.098 MB
% 1.27/0.67 % Net memory used: 46.954 MB
%------------------------------------------------------------------------------