%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP584-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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 0.13s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP584-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.35 % Computer : n007.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Sun Sep 20 20:15:35 UTC 2026
% 0.11/0.35 % CPUTime :
% 0.11/0.36 % Drodi V4.1.1
% 0.13/0.40 % Refutation found
% 0.13/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.40 fof(f1,axiom,(
% 0.13/0.40 (![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 ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f2,axiom,(
% 0.13/0.40 (![A,B]: (multiply(A,B) = double_divide(double_divide(B,A),identity) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f3,axiom,(
% 0.13/0.40 (![A]: (inverse(A) = double_divide(A,identity) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f4,axiom,(
% 0.13/0.40 (![A]: (identity = double_divide(A,inverse(A)) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f5,negated_conjecture,(
% 0.13/0.40 multiply(a,b) != multiply(b,a) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f6,plain,(
% 0.13/0.40 ![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)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.40 fof(f7,plain,(
% 0.13/0.40 ![X0,X1]: (multiply(X0,X1)=double_divide(double_divide(X1,X0),identity))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.40 fof(f8,plain,(
% 0.13/0.40 ![X0]: (inverse(X0)=double_divide(X0,identity))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.40 fof(f9,plain,(
% 0.13/0.40 ![X0]: (identity=double_divide(X0,inverse(X0)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.40 fof(f10,plain,(
% 0.13/0.40 ~multiply(a,b)=multiply(b,a)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.40 fof(f14,plain,(
% 0.13/0.40 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))),inverse(identity))=X2)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f8,f6])).
% 0.13/0.40 fof(f15,plain,(
% 0.13/0.40 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f8,f7])).
% 0.13/0.40 fof(f16,plain,(
% 0.13/0.40 ![X0]: (multiply(identity,X0)=inverse(inverse(X0)))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f8,f15])).
% 0.13/0.40 fof(f17,plain,(
% 0.13/0.40 ![X0,X1]: (identity=double_divide(double_divide(X0,X1),multiply(X1,X0)))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f15,f9])).
% 0.13/0.40 fof(f18,plain,(
% 0.13/0.40 ![X0]: (multiply(inverse(X0),X0)=inverse(identity))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f9,f15])).
% 0.13/0.40 fof(f45,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(double_divide(X0,double_divide(identity,double_divide(X1,double_divide(inverse(identity),X0)))),inverse(identity))=X1)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f9,f14])).
% 0.13/0.40 fof(f46,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(double_divide(X0,double_divide(inverse(identity),double_divide(X1,double_divide(identity,X0)))),inverse(identity))=X1)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f8,f14])).
% 0.13/0.40 fof(f47,plain,(
% 0.13/0.40 ![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)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f14,f14])).
% 0.13/0.40 fof(f48,plain,(
% 0.13/0.40 ![X0,X1,X2]: (double_divide(double_divide(multiply(X0,X1),double_divide(double_divide(identity,double_divide(X1,X0)),double_divide(X2,identity))),inverse(identity))=X2)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f17,f14])).
% 0.13/0.40 fof(f49,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X0),double_divide(X1,identity))),inverse(identity))=X1)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f9,f14])).
% 0.13/0.40 fof(f50,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(identity,X0),double_divide(X1,inverse(X0)))),inverse(identity))=X1)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f8,f14])).
% 0.13/0.40 fof(f53,plain,(
% 0.13/0.40 ![X0,X1,X2]: (multiply(inverse(identity),double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))))=inverse(X2))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f14,f15])).
% 0.13/0.40 fof(f54,plain,(
% 0.13/0.40 ![X0,X1,X2]: (double_divide(double_divide(multiply(X0,X1),double_divide(double_divide(identity,double_divide(X1,X0)),inverse(X2))),inverse(identity))=X2)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f8,f48])).
% 0.13/0.40 fof(f55,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X0),inverse(X1))),inverse(identity))=X1)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f8,f49])).
% 0.13/0.40 fof(f58,plain,(
% 0.13/0.40 ![X0,X1]: (multiply(inverse(identity),double_divide(X0,double_divide(identity,double_divide(X1,double_divide(inverse(identity),X0)))))=inverse(X1))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f9,f53])).
% 0.13/0.40 fof(f75,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(double_divide(multiply(X0,X1),identity),inverse(identity))=double_divide(identity,double_divide(X1,X0)))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f9,f54])).
% 0.13/0.40 fof(f92,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(inverse(multiply(X0,X1)),inverse(identity))=double_divide(identity,double_divide(X1,X0)))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f8,f75])).
% 0.13/0.40 fof(f110,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(inverse(inverse(X0)),inverse(identity))=double_divide(identity,double_divide(double_divide(X1,double_divide(identity,double_divide(X0,double_divide(inverse(identity),X1)))),inverse(identity))))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f58,f92])).
% 0.13/0.40 fof(f119,plain,(
% 0.13/0.40 ![X0,X1]: (multiply(inverse(identity),inverse(multiply(X0,X1)))=inverse(double_divide(identity,double_divide(X1,X0))))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f92,f15])).
% 0.13/0.40 fof(f123,plain,(
% 0.13/0.40 ![X0]: (double_divide(inverse(inverse(X0)),inverse(identity))=double_divide(identity,X0))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f45,f110])).
% 0.13/0.40 fof(f131,plain,(
% 0.13/0.40 ![X0,X1]: (multiply(inverse(identity),inverse(multiply(X0,X1)))=multiply(double_divide(X1,X0),identity))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f15,f119])).
% 0.13/0.40 fof(f135,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,inverse(inverse(X0))),double_divide(X1,double_divide(identity,X0)))),inverse(identity))=X1)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f123,f14])).
% 0.13/0.40 fof(f138,plain,(
% 0.13/0.40 ![X0]: (multiply(inverse(identity),inverse(inverse(X0)))=inverse(double_divide(identity,X0)))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f123,f15])).
% 0.13/0.40 fof(f142,plain,(
% 0.13/0.40 ![X0]: (multiply(inverse(identity),inverse(inverse(X0)))=multiply(X0,identity))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f15,f138])).
% 0.13/0.40 fof(f182,plain,(
% 0.13/0.40 ![X0]: (double_divide(double_divide(inverse(identity),double_divide(inverse(identity),inverse(X0))),inverse(identity))=X0)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f8,f55])).
% 0.13/0.40 fof(f183,plain,(
% 0.13/0.40 ![X0,X1,X2]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X0),multiply(X1,X2))),inverse(identity))=double_divide(X2,X1))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f15,f55])).
% 0.13/0.40 fof(f256,plain,(
% 0.13/0.40 ![X0]: (double_divide(double_divide(multiply(double_divide(X0,double_divide(identity,identity)),inverse(identity)),X0),inverse(identity))=identity)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f46,f54])).
% 0.13/0.40 fof(f265,plain,(
% 0.13/0.40 ![X0]: (double_divide(double_divide(multiply(double_divide(X0,inverse(identity)),inverse(identity)),X0),inverse(identity))=identity)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f8,f256])).
% 0.13/0.40 fof(f273,plain,(
% 0.13/0.40 ![X0,X1,X2]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(inverse(identity),double_divide(double_divide(identity,inverse(inverse(X0))),double_divide(X1,double_divide(identity,X0))))),double_divide(X2,X1))),inverse(identity))=X2)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f123,f47])).
% 0.13/0.40 fof(f289,plain,(
% 0.13/0.40 ![X0,X1,X2]: (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(identity),double_divide(inverse(identity),inverse(X2))))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f182,f47])).
% 0.13/0.40 fof(f294,plain,(
% 0.13/0.40 ![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(X3,double_divide(identity,double_divide(X2,double_divide(inverse(identity),X3)))))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f45,f47])).
% 0.13/0.40 fof(f295,plain,(
% 0.13/0.40 ![X0,X1,X2,X3,X4]: (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(X3,double_divide(double_divide(identity,X4),double_divide(X2,double_divide(X4,X3)))))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f14,f47])).
% 0.13/0.40 fof(f339,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(inverse(identity),double_divide(inverse(identity),inverse(X0)))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(inverse(identity),X1)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f289,f294])).
% 0.13/0.40 fof(f347,plain,(
% 0.13/0.40 ![X0,X1,X2]: (double_divide(inverse(identity),double_divide(inverse(identity),inverse(X0)))=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f289,f295])).
% 0.13/0.40 fof(f403,plain,(
% 0.13/0.40 ![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)))))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f50,f50])).
% 0.13/0.40 fof(f404,plain,(
% 0.13/0.40 ![X0]: (double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),inverse(identity))=double_divide(inverse(identity),double_divide(inverse(identity),inverse(X0))))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f182,f50])).
% 0.13/0.40 fof(f405,plain,(
% 0.13/0.40 ![X0]: (double_divide(double_divide(identity,double_divide(double_divide(identity,X0),identity)),inverse(identity))=X0)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f9,f50])).
% 0.13/0.40 fof(f416,plain,(
% 0.13/0.40 ![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)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f8,f403])).
% 0.13/0.40 fof(f419,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(inverse(identity),double_divide(inverse(identity),inverse(X0)))=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f420,f416])).
% 0.13/0.40 fof(f420,plain,(
% 0.13/0.40 ![X0]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(inverse(identity),double_divide(inverse(identity),inverse(X0))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f8,f404])).
% 0.13/0.40 fof(f421,plain,(
% 0.13/0.40 ![X0]: (double_divide(double_divide(identity,inverse(double_divide(identity,X0))),inverse(identity))=X0)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f8,f405])).
% 0.13/0.40 fof(f422,plain,(
% 0.13/0.40 ![X0]: (double_divide(double_divide(identity,multiply(X0,identity)),inverse(identity))=X0)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f15,f421])).
% 0.13/0.40 fof(f433,plain,(
% 0.13/0.40 double_divide(double_divide(identity,inverse(identity)),inverse(identity))=inverse(identity)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f18,f422])).
% 0.13/0.40 fof(f438,plain,(
% 0.13/0.40 double_divide(identity,inverse(identity))=inverse(identity)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f9,f433])).
% 0.13/0.40 fof(f439,plain,(
% 0.13/0.40 ![X0]: (double_divide(double_divide(identity,multiply(X0,identity)),identity)=X0)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f422])).
% 0.13/0.40 fof(f441,plain,(
% 0.13/0.40 ![X0,X1]: (multiply(identity,inverse(multiply(X0,X1)))=multiply(double_divide(X1,X0),identity))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f131])).
% 0.13/0.40 fof(f442,plain,(
% 0.13/0.40 ![X0]: (multiply(identity,inverse(inverse(X0)))=multiply(X0,identity))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f142])).
% 0.13/0.40 fof(f443,plain,(
% 0.13/0.40 ![X0]: (double_divide(inverse(inverse(X0)),identity)=double_divide(identity,X0))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f123])).
% 0.13/0.40 fof(f444,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(inverse(multiply(X0,X1)),identity)=double_divide(identity,double_divide(X1,X0)))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f92])).
% 0.13/0.40 fof(f446,plain,(
% 0.13/0.40 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f18])).
% 0.13/0.40 fof(f447,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(inverse(identity),double_divide(identity,inverse(X0)))=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f419])).
% 0.13/0.40 fof(f450,plain,(
% 0.13/0.40 ![X0]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(inverse(identity),double_divide(identity,inverse(X0))))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f420])).
% 0.13/0.40 fof(f457,plain,(
% 0.13/0.40 ![X0,X1,X2]: (double_divide(inverse(identity),double_divide(identity,inverse(X0)))=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f347])).
% 0.13/0.40 fof(f458,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(inverse(identity),double_divide(inverse(identity),inverse(X0)))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f339])).
% 0.13/0.40 fof(f464,plain,(
% 0.13/0.40 ![X0,X1,X2]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(inverse(identity),double_divide(double_divide(identity,inverse(inverse(X0))),double_divide(X1,double_divide(identity,X0))))),double_divide(X2,X1))),identity)=X2)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f273])).
% 0.13/0.40 fof(f465,plain,(
% 0.13/0.40 ![X0]: (double_divide(double_divide(multiply(double_divide(X0,inverse(identity)),inverse(identity)),X0),identity)=identity)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f265])).
% 0.13/0.40 fof(f472,plain,(
% 0.13/0.40 ![X0,X1,X2]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X0),multiply(X1,X2))),identity)=double_divide(X2,X1))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f183])).
% 0.13/0.40 fof(f473,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,inverse(inverse(X0))),double_divide(X1,double_divide(identity,X0)))),identity)=X1)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f480,f135])).
% 0.13/0.40 fof(f480,plain,(
% 0.13/0.40 identity=inverse(identity)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f9,f438])).
% 0.13/0.40 fof(f495,plain,(
% 0.13/0.40 ![X0]: (inverse(double_divide(identity,multiply(X0,identity)))=X0)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f8,f439])).
% 0.13/0.40 fof(f497,plain,(
% 0.13/0.40 ![X0]: (multiply(multiply(X0,identity),identity)=X0)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f15,f495])).
% 0.13/0.40 fof(f502,plain,(
% 0.13/0.40 ![X0,X1]: (inverse(inverse(inverse(multiply(X0,X1))))=multiply(double_divide(X1,X0),identity))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f16,f441])).
% 0.13/0.40 fof(f503,plain,(
% 0.13/0.40 ![X0]: (inverse(inverse(inverse(inverse(X0))))=multiply(X0,identity))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f16,f442])).
% 0.13/0.40 fof(f504,plain,(
% 0.13/0.40 ![X0]: (double_divide(identity,inverse(X0))=multiply(X0,identity))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f506,f503])).
% 0.13/0.40 fof(f505,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(identity,multiply(X0,X1))=multiply(double_divide(X1,X0),identity))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f506,f502])).
% 0.13/0.40 fof(f506,plain,(
% 0.13/0.40 ![X0]: (inverse(inverse(inverse(X0)))=double_divide(identity,X0))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f8,f443])).
% 0.13/0.40 fof(f507,plain,(
% 0.13/0.40 ![X0,X1]: (inverse(inverse(multiply(X0,X1)))=double_divide(identity,double_divide(X1,X0)))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f8,f444])).
% 0.13/0.40 fof(f508,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(identity,double_divide(identity,inverse(X0)))=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f480,f447])).
% 0.13/0.40 fof(f509,plain,(
% 0.13/0.40 ![X0,X1]: (inverse(inverse(multiply(inverse(X0),identity)))=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f507,f508])).
% 0.13/0.40 fof(f510,plain,(
% 0.13/0.40 ![X0,X1]: (inverse(inverse(multiply(inverse(X0),identity)))=inverse(inverse(multiply(double_divide(X0,inverse(X1)),double_divide(identity,X1)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f507,f509])).
% 0.13/0.40 fof(f518,plain,(
% 0.13/0.40 ![X0]: (double_divide(inverse(inverse(multiply(X0,inverse(identity)))),inverse(identity))=double_divide(inverse(identity),double_divide(identity,inverse(X0))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f507,f450])).
% 0.13/0.40 fof(f519,plain,(
% 0.13/0.40 ![X0]: (double_divide(identity,multiply(X0,inverse(identity)))=double_divide(inverse(identity),double_divide(identity,inverse(X0))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f123,f518])).
% 0.13/0.40 fof(f520,plain,(
% 0.13/0.40 ![X0]: (double_divide(identity,multiply(X0,identity))=double_divide(inverse(identity),double_divide(identity,inverse(X0))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f480,f519])).
% 0.13/0.40 fof(f521,plain,(
% 0.13/0.40 ![X0]: (double_divide(identity,multiply(X0,identity))=double_divide(identity,double_divide(identity,inverse(X0))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f480,f520])).
% 0.13/0.40 fof(f523,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(identity,multiply(X0,identity))=inverse(inverse(multiply(double_divide(X0,inverse(X1)),double_divide(identity,X1)))))),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f524,f510])).
% 0.13/0.40 fof(f524,plain,(
% 0.13/0.40 ![X0]: (double_divide(identity,multiply(X0,identity))=inverse(inverse(multiply(inverse(X0),identity))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f507,f521])).
% 0.13/0.40 fof(f568,plain,(
% 0.13/0.40 ![X0,X1,X2]: (double_divide(identity,double_divide(identity,inverse(X0)))=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f480,f457])).
% 0.13/0.40 fof(f569,plain,(
% 0.13/0.40 ![X0,X1,X2]: (inverse(inverse(multiply(inverse(X0),identity)))=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f507,f568])).
% 0.13/0.40 fof(f570,plain,(
% 0.13/0.40 ![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)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f524,f569])).
% 0.13/0.40 fof(f571,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(identity,double_divide(inverse(identity),inverse(X0)))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f480,f458])).
% 0.13/0.40 fof(f572,plain,(
% 0.13/0.40 ![X0,X1]: (inverse(inverse(multiply(inverse(X0),inverse(identity))))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f507,f571])).
% 0.13/0.40 fof(f573,plain,(
% 0.13/0.40 ![X0,X1]: (inverse(inverse(multiply(inverse(X0),identity)))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f480,f572])).
% 0.13/0.40 fof(f574,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(identity,multiply(X0,identity))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f524,f573])).
% 0.13/0.40 fof(f575,plain,(
% 0.13/0.40 ![X0,X1]: (double_divide(identity,multiply(X0,identity))=double_divide(X1,inverse(inverse(multiply(double_divide(identity,X1),X0)))))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f507,f574])).
% 0.13/0.40 fof(f600,plain,(
% 0.13/0.40 ![X0,X1,X2]: (inverse(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(inverse(identity),double_divide(double_divide(identity,inverse(inverse(X0))),double_divide(X1,double_divide(identity,X0))))),double_divide(X2,X1))))=X2)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f8,f464])).
% 0.13/0.40 fof(f601,plain,(
% 0.13/0.40 ![X0,X1,X2]: (multiply(double_divide(double_divide(identity,double_divide(inverse(identity),double_divide(double_divide(identity,inverse(inverse(X0))),double_divide(X1,double_divide(identity,X0))))),double_divide(X2,X1)),inverse(identity))=X2)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f15,f600])).
% 0.13/0.40 fof(f602,plain,(
% 0.13/0.40 ![X0,X1,X2]: (multiply(double_divide(inverse(inverse(multiply(double_divide(double_divide(identity,inverse(inverse(X0))),double_divide(X1,double_divide(identity,X0))),inverse(identity)))),double_divide(X2,X1)),inverse(identity))=X2)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f507,f601])).
% 0.13/0.40 fof(f603,plain,(
% 0.13/0.40 ![X0,X1,X2]: (multiply(double_divide(inverse(inverse(multiply(double_divide(double_divide(identity,inverse(inverse(X0))),double_divide(X1,double_divide(identity,X0))),identity))),double_divide(X2,X1)),inverse(identity))=X2)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f480,f602])).
% 0.13/0.40 fof(f604,plain,(
% 0.13/0.40 ![X0,X1,X2]: (multiply(double_divide(inverse(inverse(multiply(double_divide(double_divide(identity,inverse(inverse(X0))),double_divide(X1,double_divide(identity,X0))),identity))),double_divide(X2,X1)),identity)=X2)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f480,f603])).
% 0.13/0.40 fof(f605,plain,(
% 0.13/0.40 ![X0]: (inverse(double_divide(multiply(double_divide(X0,inverse(identity)),inverse(identity)),X0))=identity)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f8,f465])).
% 0.13/0.40 fof(f606,plain,(
% 0.13/0.40 ![X0]: (multiply(X0,multiply(double_divide(X0,inverse(identity)),inverse(identity)))=identity)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f15,f605])).
% 0.13/0.40 fof(f607,plain,(
% 0.13/0.40 ![X0]: (multiply(X0,multiply(double_divide(X0,identity),inverse(identity)))=identity)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f480,f606])).
% 0.13/0.40 fof(f608,plain,(
% 0.13/0.40 ![X0]: (multiply(X0,multiply(inverse(X0),inverse(identity)))=identity)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f8,f607])).
% 0.13/0.40 fof(f609,plain,(
% 0.13/0.40 ![X0]: (multiply(X0,multiply(inverse(X0),identity))=identity)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f480,f608])).
% 0.13/0.41 fof(f639,plain,(
% 0.13/0.41 ![X0,X1,X2]: (inverse(double_divide(inverse(X0),double_divide(double_divide(identity,X0),multiply(X1,X2))))=double_divide(X2,X1))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f472])).
% 0.13/0.41 fof(f640,plain,(
% 0.13/0.41 ![X0,X1,X2]: (multiply(double_divide(double_divide(identity,X0),multiply(X1,X2)),inverse(X0))=double_divide(X2,X1))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f15,f639])).
% 0.13/0.41 fof(f641,plain,(
% 0.13/0.41 ![X0,X1]: (inverse(double_divide(inverse(identity),double_divide(double_divide(identity,inverse(inverse(X0))),double_divide(X1,double_divide(identity,X0)))))=X1)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f473])).
% 0.13/0.41 fof(f642,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(double_divide(double_divide(identity,inverse(inverse(X0))),double_divide(X1,double_divide(identity,X0))),inverse(identity))=X1)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f15,f641])).
% 0.13/0.41 fof(f643,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(double_divide(inverse(inverse(X0)),double_divide(X1,X0)),identity)=X1)),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f644,f604])).
% 0.13/0.41 fof(f644,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(double_divide(double_divide(identity,inverse(inverse(X0))),double_divide(X1,double_divide(identity,X0))),identity)=X1)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f480,f642])).
% 0.13/0.41 fof(f675,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(X1,inverse(inverse(multiply(double_divide(identity,X1),X0)))))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f505,f575])).
% 0.13/0.41 fof(f676,plain,(
% 0.13/0.41 ![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)))))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f505,f570])).
% 0.13/0.41 fof(f682,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=inverse(inverse(multiply(double_divide(X0,inverse(X1)),double_divide(identity,X1)))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f505,f523])).
% 0.13/0.41 fof(f702,plain,(
% 0.13/0.41 ![X0]: (inverse(inverse(double_divide(identity,X0)))=double_divide(identity,inverse(inverse(X0))))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f506,f506])).
% 0.13/0.41 fof(f708,plain,(
% 0.13/0.41 ![X0]: (inverse(multiply(X0,identity))=double_divide(identity,inverse(inverse(X0))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f15,f702])).
% 0.13/0.41 fof(f711,plain,(
% 0.13/0.41 ![X0]: (multiply(X0,inverse(multiply(X0,identity)))=identity)),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f712,f609])).
% 0.13/0.41 fof(f712,plain,(
% 0.13/0.41 ![X0]: (inverse(multiply(X0,identity))=multiply(inverse(X0),identity))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f504,f708])).
% 0.13/0.41 fof(f842,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(double_divide(double_divide(identity,X0),X1),inverse(X0))=double_divide(identity,multiply(X1,identity)))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f497,f640])).
% 0.13/0.41 fof(f847,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(double_divide(double_divide(identity,X0),identity),inverse(X0))=double_divide(inverse(multiply(X1,identity)),X1))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f711,f640])).
% 0.13/0.41 fof(f848,plain,(
% 0.13/0.41 ![X0,X1,X2]: (multiply(double_divide(double_divide(identity,inverse(inverse(X0))),multiply(X1,X2)),double_divide(identity,X0))=double_divide(X2,X1))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f506,f640])).
% 0.13/0.41 fof(f865,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(double_divide(double_divide(identity,X0),X1),inverse(X0))=multiply(double_divide(identity,X1),identity))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f505,f842])).
% 0.13/0.41 fof(f878,plain,(
% 0.13/0.41 ![X0]: (multiply(double_divide(identity,identity),identity)=double_divide(inverse(multiply(X0,identity)),X0))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f865,f847])).
% 0.13/0.41 fof(f879,plain,(
% 0.13/0.41 ![X0]: (multiply(inverse(identity),identity)=double_divide(inverse(multiply(X0,identity)),X0))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f878])).
% 0.13/0.41 fof(f880,plain,(
% 0.13/0.41 ![X0]: (identity=double_divide(inverse(multiply(X0,identity)),X0))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f446,f879])).
% 0.13/0.41 fof(f881,plain,(
% 0.13/0.41 ![X0,X1,X2]: (multiply(double_divide(multiply(inverse(X0),identity),multiply(X1,X2)),double_divide(identity,X0))=double_divide(X2,X1))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f504,f848])).
% 0.13/0.41 fof(f882,plain,(
% 0.13/0.41 ![X0,X1,X2]: (multiply(double_divide(inverse(multiply(X0,identity)),multiply(X1,X2)),double_divide(identity,X0))=double_divide(X2,X1))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f712,f881])).
% 0.13/0.41 fof(f954,plain,(
% 0.13/0.41 ![X0]: (multiply(double_divide(identity,inverse(multiply(inverse(X0),identity))),identity)=inverse(inverse(multiply(identity,double_divide(identity,X0)))))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f880,f682])).
% 0.13/0.41 fof(f973,plain,(
% 0.13/0.41 ![X0]: (multiply(multiply(multiply(inverse(X0),identity),identity),identity)=inverse(inverse(multiply(identity,double_divide(identity,X0)))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f504,f954])).
% 0.13/0.41 fof(f974,plain,(
% 0.13/0.41 ![X0]: (multiply(inverse(X0),identity)=inverse(inverse(multiply(identity,double_divide(identity,X0)))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f497,f973])).
% 0.13/0.41 fof(f975,plain,(
% 0.13/0.41 ![X0]: (inverse(multiply(X0,identity))=inverse(inverse(multiply(identity,double_divide(identity,X0)))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f712,f974])).
% 0.13/0.41 fof(f976,plain,(
% 0.13/0.41 ![X0]: (inverse(multiply(X0,identity))=inverse(inverse(inverse(inverse(double_divide(identity,X0))))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f16,f975])).
% 0.13/0.41 fof(f977,plain,(
% 0.13/0.41 ![X0]: (inverse(multiply(X0,identity))=double_divide(identity,inverse(double_divide(identity,X0))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f506,f976])).
% 0.13/0.41 fof(f987,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(double_divide(double_divide(identity,X0),X1),inverse(X0))=inverse(multiply(X1,identity)))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f994,f865])).
% 0.13/0.41 fof(f990,plain,(
% 0.13/0.41 ![X0,X1,X2]: (inverse(multiply(X0,identity))=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f994,f676])).
% 0.13/0.41 fof(f991,plain,(
% 0.13/0.41 ![X0,X1]: (inverse(multiply(X0,identity))=double_divide(X1,inverse(inverse(multiply(double_divide(identity,X1),X0)))))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f994,f675])).
% 0.13/0.41 fof(f994,plain,(
% 0.13/0.41 ![X0]: (inverse(multiply(X0,identity))=multiply(double_divide(identity,X0),identity))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f504,f977])).
% 0.13/0.41 fof(f1140,plain,(
% 0.13/0.41 ![X0]: (inverse(multiply(inverse(X0),identity))=multiply(multiply(X0,identity),identity))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f504,f994])).
% 0.13/0.41 fof(f1147,plain,(
% 0.13/0.41 ![X0]: (multiply(inverse(multiply(X0,identity)),identity)=double_divide(identity,X0))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f994,f497])).
% 0.13/0.41 fof(f1150,plain,(
% 0.13/0.41 ![X0]: (inverse(inverse(multiply(X0,identity)))=multiply(multiply(X0,identity),identity))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f712,f1140])).
% 0.13/0.41 fof(f1159,plain,(
% 0.13/0.41 ![X0]: (inverse(inverse(multiply(X0,identity)))=X0)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f497,f1150])).
% 0.13/0.41 fof(f1176,plain,(
% 0.13/0.41 ![X0]: (inverse(multiply(multiply(X0,identity),identity))=double_divide(identity,X0))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f712,f1147])).
% 0.13/0.41 fof(f1177,plain,(
% 0.13/0.41 ![X0]: (inverse(inverse(X0))=multiply(X0,identity))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f1198,f504])).
% 0.13/0.41 fof(f1183,plain,(
% 0.13/0.41 ![X0,X1]: (inverse(inverse(multiply(X0,X1)))=inverse(double_divide(X1,X0)))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f1198,f507])).
% 0.13/0.41 fof(f1187,plain,(
% 0.13/0.41 ![X0,X1]: (inverse(multiply(X0,identity))=double_divide(X1,inverse(inverse(multiply(inverse(X1),X0)))))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f1198,f991])).
% 0.13/0.41 fof(f1188,plain,(
% 0.13/0.41 ![X0,X1,X2]: (inverse(multiply(X0,identity))=double_divide(X1,double_divide(inverse(X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f1198,f990])).
% 0.13/0.41 fof(f1195,plain,(
% 0.13/0.41 ![X0,X1,X2]: (multiply(double_divide(inverse(multiply(X0,identity)),multiply(X1,X2)),inverse(X0))=double_divide(X2,X1))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f1198,f882])).
% 0.13/0.41 fof(f1198,plain,(
% 0.13/0.41 ![X0]: (inverse(X0)=double_divide(identity,X0))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f497,f1176])).
% 0.13/0.41 fof(f1215,plain,(
% 0.13/0.41 ![X0,X1]: (inverse(inverse(double_divide(inverse(inverse(X0)),double_divide(X1,X0))))=X1)),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f1177,f643])).
% 0.13/0.41 fof(f1221,plain,(
% 0.13/0.41 ![X0]: (inverse(inverse(inverse(inverse(X0))))=X0)),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f1177,f1159])).
% 0.13/0.41 fof(f1235,plain,(
% 0.13/0.41 ![X0,X1]: (inverse(inverse(multiply(X0,X1)))=multiply(X0,X1))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f15,f1183])).
% 0.13/0.41 fof(f1239,plain,(
% 0.13/0.41 ![X0,X1]: (inverse(inverse(inverse(X0)))=double_divide(X1,inverse(inverse(multiply(inverse(X1),X0)))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f1177,f1187])).
% 0.13/0.41 fof(f1240,plain,(
% 0.13/0.41 ![X0,X1]: (double_divide(identity,X0)=double_divide(X1,inverse(inverse(multiply(inverse(X1),X0)))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f506,f1239])).
% 0.13/0.41 fof(f1241,plain,(
% 0.13/0.41 ![X0,X1]: (inverse(X0)=double_divide(X1,inverse(inverse(multiply(inverse(X1),X0)))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f1198,f1240])).
% 0.13/0.41 fof(f1242,plain,(
% 0.13/0.41 ![X0,X1]: (inverse(X0)=double_divide(X1,multiply(inverse(X1),X0)))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f1235,f1241])).
% 0.13/0.41 fof(f1243,plain,(
% 0.13/0.41 ![X0,X1,X2]: (inverse(inverse(inverse(X0)))=double_divide(X1,double_divide(inverse(X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f1177,f1188])).
% 0.13/0.41 fof(f1244,plain,(
% 0.13/0.41 ![X0,X1,X2]: (double_divide(identity,X0)=double_divide(X1,double_divide(inverse(X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f506,f1243])).
% 0.13/0.41 fof(f1245,plain,(
% 0.13/0.41 ![X0,X1,X2]: (inverse(X0)=double_divide(X1,double_divide(inverse(X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f1198,f1244])).
% 0.13/0.41 fof(f1271,plain,(
% 0.13/0.41 ![X0,X1,X2]: (multiply(double_divide(inverse(inverse(inverse(X0))),multiply(X1,X2)),inverse(X0))=double_divide(X2,X1))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f1177,f1195])).
% 0.13/0.43 fof(f1272,plain,(
% 0.13/0.43 ![X0,X1,X2]: (multiply(double_divide(double_divide(identity,X0),multiply(X1,X2)),inverse(X0))=double_divide(X2,X1))),
% 0.13/0.43 inference(forward_demodulation,[status(thm)],[f506,f1271])).
% 0.13/0.43 fof(f1273,plain,(
% 0.13/0.43 ![X0,X1]: (inverse(multiply(multiply(X0,X1),identity))=double_divide(X1,X0))),
% 0.13/0.43 inference(forward_demodulation,[status(thm)],[f987,f1272])).
% 0.13/0.43 fof(f1274,plain,(
% 0.13/0.43 ![X0,X1]: (inverse(inverse(inverse(multiply(X0,X1))))=double_divide(X1,X0))),
% 0.13/0.43 inference(forward_demodulation,[status(thm)],[f1177,f1273])).
% 0.13/0.43 fof(f1275,plain,(
% 0.13/0.43 ![X0,X1]: (double_divide(identity,multiply(X0,X1))=double_divide(X1,X0))),
% 0.13/0.43 inference(forward_demodulation,[status(thm)],[f506,f1274])).
% 0.13/0.43 fof(f1277,plain,(
% 0.13/0.43 ![X0,X1]: (inverse(multiply(X0,X1))=double_divide(X1,X0))),
% 0.13/0.43 inference(forward_demodulation,[status(thm)],[f1198,f1275])).
% 0.13/0.43 fof(f1296,plain,(
% 0.13/0.43 ![X0,X1]: (inverse(multiply(double_divide(X0,X1),inverse(inverse(X1))))=X0)),
% 0.13/0.43 inference(forward_demodulation,[status(thm)],[f15,f1215])).
% 0.13/0.43 fof(f1297,plain,(
% 0.13/0.43 ![X0,X1]: (double_divide(inverse(inverse(X0)),double_divide(X1,X0))=X1)),
% 0.13/0.43 inference(forward_demodulation,[status(thm)],[f1277,f1296])).
% 0.13/0.43 fof(f1306,plain,(
% 0.13/0.43 ![X0]: (double_divide(identity,inverse(X0))=X0)),
% 0.13/0.43 inference(forward_demodulation,[status(thm)],[f506,f1221])).
% 0.13/0.43 fof(f1309,plain,(
% 0.13/0.43 ![X0,X1]: (double_divide(X0,double_divide(X1,X0))=X1)),
% 0.13/0.43 inference(backward_demodulation,[status(thm)],[f1310,f1297])).
% 0.13/0.43 fof(f1310,plain,(
% 0.13/0.43 ![X0]: (inverse(inverse(X0))=X0)),
% 0.13/0.43 inference(forward_demodulation,[status(thm)],[f1198,f1306])).
% 0.13/0.43 fof(f1449,plain,(
% 0.13/0.43 ![X0,X1]: (double_divide(double_divide(X0,X1),X0)=X1)),
% 0.13/0.43 inference(paramodulation,[status(thm)],[f1309,f1309])).
% 0.13/0.43 fof(f1485,plain,(
% 0.13/0.43 ![X0,X1]: (double_divide(inverse(X0),X1)=multiply(inverse(X1),X0))),
% 0.13/0.43 inference(paramodulation,[status(thm)],[f1242,f1449])).
% 0.13/0.43 fof(f1488,plain,(
% 0.13/0.43 ![X0,X1,X2]: (inverse(double_divide(double_divide(X0,X1),X2))=double_divide(X1,double_divide(inverse(X0),X2)))),
% 0.13/0.43 inference(paramodulation,[status(thm)],[f1449,f1245])).
% 0.13/0.43 fof(f1513,plain,(
% 0.13/0.43 ![X0,X1,X2]: (multiply(X0,double_divide(X1,X2))=double_divide(X2,double_divide(inverse(X1),X0)))),
% 0.13/0.43 inference(forward_demodulation,[status(thm)],[f15,f1488])).
% 0.13/0.43 fof(f1514,plain,(
% 0.13/0.43 ![X0,X1]: (inverse(X0)=multiply(X1,double_divide(X0,X1)))),
% 0.13/0.43 inference(backward_demodulation,[status(thm)],[f1515,f1242])).
% 0.13/0.43 fof(f1515,plain,(
% 0.13/0.43 ![X0,X1,X2]: (multiply(X0,double_divide(X1,X2))=double_divide(X2,multiply(inverse(X0),X1)))),
% 0.13/0.43 inference(forward_demodulation,[status(thm)],[f1485,f1513])).
% 0.13/0.43 fof(f1612,plain,(
% 0.13/0.43 ![X0,X1]: (inverse(double_divide(X0,X1))=multiply(X0,X1))),
% 0.13/0.43 inference(paramodulation,[status(thm)],[f1449,f1514])).
% 0.13/0.43 fof(f1820,plain,(
% 0.13/0.43 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 0.13/0.43 inference(paramodulation,[status(thm)],[f15,f1612])).
% 0.13/0.43 fof(f1835,plain,(
% 0.13/0.43 $false),
% 0.13/0.43 inference(backward_subsumption_resolution,[status(thm)],[f10,f1820])).
% 0.13/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.43 % Elapsed time: 0.067229 seconds
% 0.13/0.43 % CPU time: 0.376527 seconds
% 0.13/0.43 % Total memory used: 21.640 MB
% 0.13/0.43 % Net memory used: 20.183 MB
%------------------------------------------------------------------------------