%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP576-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:50 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP576-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n026.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sun Sep 20 20:19:52 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.36 % Drodi V4.1.1
% 0.13/0.41 % Refutation found
% 0.13/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.41 fof(f1,axiom,(
% 0.13/0.41 (![A,B,C]: (double_divide(double_divide(A,double_divide(double_divide(B,double_divide(C,A)),double_divide(C,identity))),double_divide(identity,identity)) = B ))),
% 0.13/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f2,axiom,(
% 0.13/0.41 (![A,B]: (multiply(A,B) = double_divide(double_divide(B,A),identity) ))),
% 0.13/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f3,axiom,(
% 0.13/0.41 (![A]: (inverse(A) = double_divide(A,identity) ))),
% 0.13/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f4,axiom,(
% 0.13/0.41 (![A]: (identity = double_divide(A,inverse(A)) ))),
% 0.13/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f5,negated_conjecture,(
% 0.13/0.41 multiply(a,b) != multiply(b,a) ),
% 0.13/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.41 fof(f6,plain,(
% 0.13/0.41 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X2,X0)),double_divide(X2,identity))),double_divide(identity,identity))=X1)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.41 fof(f7,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(X0,X1)=double_divide(double_divide(X1,X0),identity))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.41 fof(f8,plain,(
% 0.13/0.41 ![X0]: (inverse(X0)=double_divide(X0,identity))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.41 fof(f9,plain,(
% 0.13/0.41 ![X0]: (identity=double_divide(X0,inverse(X0)))),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.41 fof(f10,plain,(
% 0.13/0.41 ~multiply(a,b)=multiply(b,a)),
% 0.13/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.41 fof(f14,plain,(
% 0.13/0.41 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X2,X0)),double_divide(X2,identity))),inverse(identity))=X1)),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f8,f6])).
% 0.13/0.41 fof(f15,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f8,f7])).
% 0.13/0.41 fof(f16,plain,(
% 0.13/0.41 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X2,X0)),inverse(X2))),inverse(identity))=X1)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f14])).
% 0.13/0.41 fof(f17,plain,(
% 0.13/0.41 ![X0]: (multiply(identity,X0)=inverse(inverse(X0)))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f8,f15])).
% 0.13/0.41 fof(f18,plain,(
% 0.13/0.41 ![X0,X1]: (identity=double_divide(double_divide(X0,X1),multiply(X1,X0)))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f15,f9])).
% 0.13/0.41 fof(f19,plain,(
% 0.13/0.41 ![X0]: (multiply(inverse(X0),X0)=inverse(identity))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f9,f15])).
% 0.13/0.41 fof(f47,plain,(
% 0.13/0.41 ![X0,X1,X2]: (double_divide(double_divide(multiply(X0,X1),double_divide(double_divide(X2,identity),inverse(double_divide(X1,X0)))),inverse(identity))=X2)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f18,f16])).
% 0.13/0.41 fof(f50,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(double_divide(X2,X3),X0)),multiply(X3,X2))),inverse(identity))=X1)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f15,f16])).
% 0.13/0.41 fof(f53,plain,(
% 0.13/0.41 ![X0,X1,X2]: (multiply(inverse(identity),double_divide(X0,double_divide(double_divide(X1,double_divide(X2,X0)),inverse(X2))))=inverse(X1))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f16,f15])).
% 0.13/0.41 fof(f55,plain,(
% 0.13/0.41 ![X0,X1,X2]: (double_divide(double_divide(multiply(X0,X1),double_divide(inverse(X2),inverse(double_divide(X1,X0)))),inverse(identity))=X2)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f47])).
% 0.13/0.41 fof(f56,plain,(
% 0.13/0.41 ![X0,X1,X2]: (double_divide(double_divide(multiply(X0,X1),double_divide(inverse(X2),multiply(X0,X1))),inverse(identity))=X2)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f15,f55])).
% 0.13/0.41 fof(f83,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(inverse(identity),double_divide(inverse(X0),double_divide(double_divide(X1,identity),inverse(X0))))=inverse(X1))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f9,f53])).
% 0.13/0.41 fof(f84,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(inverse(identity),double_divide(identity,double_divide(double_divide(X0,inverse(X1)),inverse(X1))))=inverse(X0))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f8,f53])).
% 0.13/0.41 fof(f94,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(inverse(identity),double_divide(inverse(X0),double_divide(inverse(X1),inverse(X0))))=inverse(X1))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f83])).
% 0.13/0.41 fof(f100,plain,(
% 0.13/0.41 ![X0]: (multiply(inverse(identity),double_divide(inverse(inverse(X0)),identity))=inverse(X0))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f9,f94])).
% 0.13/0.41 fof(f108,plain,(
% 0.13/0.41 ![X0]: (multiply(inverse(identity),inverse(inverse(inverse(X0))))=inverse(X0))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f100])).
% 0.13/0.41 fof(f119,plain,(
% 0.13/0.41 ![X0]: (identity=double_divide(double_divide(inverse(inverse(inverse(X0))),inverse(identity)),inverse(X0)))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f108,f18])).
% 0.13/0.41 fof(f215,plain,(
% 0.13/0.41 multiply(inverse(identity),double_divide(identity,identity))=inverse(inverse(inverse(inverse(identity))))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f119,f84])).
% 0.13/0.41 fof(f216,plain,(
% 0.13/0.41 ![X0]: (multiply(inverse(identity),double_divide(identity,double_divide(identity,inverse(X0))))=inverse(double_divide(inverse(inverse(inverse(X0))),inverse(identity))))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f119,f84])).
% 0.13/0.41 fof(f229,plain,(
% 0.13/0.41 multiply(inverse(identity),inverse(identity))=inverse(inverse(inverse(inverse(identity))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f215])).
% 0.13/0.41 fof(f230,plain,(
% 0.13/0.41 ![X0]: (multiply(inverse(identity),double_divide(identity,double_divide(identity,inverse(X0))))=multiply(inverse(identity),inverse(inverse(inverse(X0)))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f15,f216])).
% 0.13/0.41 fof(f231,plain,(
% 0.13/0.41 ![X0]: (multiply(inverse(identity),double_divide(identity,double_divide(identity,inverse(X0))))=inverse(X0))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f108,f230])).
% 0.13/0.41 fof(f253,plain,(
% 0.13/0.41 identity=double_divide(double_divide(inverse(identity),inverse(identity)),inverse(inverse(inverse(inverse(identity)))))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f229,f18])).
% 0.13/0.41 fof(f285,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (multiply(inverse(identity),double_divide(identity,double_divide(X0,inverse(identity))))=inverse(double_divide(X1,double_divide(double_divide(X0,double_divide(double_divide(X2,X3),X1)),multiply(X3,X2)))))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f50,f84])).
% 0.13/0.41 fof(f317,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (multiply(inverse(identity),double_divide(identity,double_divide(X0,inverse(identity))))=multiply(double_divide(double_divide(X0,double_divide(double_divide(X1,X2),X3)),multiply(X2,X1)),X3))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f15,f285])).
% 0.13/0.41 fof(f438,plain,(
% 0.13/0.41 multiply(inverse(identity),double_divide(identity,identity))=inverse(identity)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f9,f231])).
% 0.13/0.41 fof(f449,plain,(
% 0.13/0.41 inverse(identity)=inverse(inverse(inverse(inverse(identity))))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f450,f229])).
% 0.13/0.41 fof(f450,plain,(
% 0.13/0.41 multiply(inverse(identity),inverse(identity))=inverse(identity)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f438])).
% 0.13/0.41 fof(f458,plain,(
% 0.13/0.41 identity=double_divide(double_divide(inverse(identity),inverse(identity)),inverse(identity))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f449,f253])).
% 0.13/0.41 fof(f461,plain,(
% 0.13/0.41 multiply(inverse(identity),double_divide(identity,identity))=inverse(inverse(identity))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f458,f84])).
% 0.13/0.41 fof(f472,plain,(
% 0.13/0.41 multiply(inverse(identity),inverse(identity))=inverse(inverse(identity))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f461])).
% 0.13/0.41 fof(f474,plain,(
% 0.13/0.41 inverse(identity)=inverse(inverse(identity))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f450,f472])).
% 0.13/0.41 fof(f507,plain,(
% 0.13/0.41 ![X0,X1]: (double_divide(double_divide(multiply(X0,X1),double_divide(inverse(identity),multiply(X0,X1))),inverse(identity))=inverse(identity))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f474,f56])).
% 0.13/0.41 fof(f529,plain,(
% 0.13/0.41 ![X0]: (multiply(identity,double_divide(identity,double_divide(identity,inverse(X0))))=inverse(X0))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f571,f231])).
% 0.13/0.41 fof(f531,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(double_divide(X2,X3),X0)),multiply(X3,X2))),identity)=X1)),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f571,f50])).
% 0.13/0.41 fof(f541,plain,(
% 0.13/0.41 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X2,X0)),inverse(X2))),identity)=X1)),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f571,f16])).
% 0.13/0.41 fof(f543,plain,(
% 0.13/0.41 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f571,f19])).
% 0.13/0.41 fof(f556,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (multiply(inverse(identity),double_divide(identity,double_divide(X0,identity)))=multiply(double_divide(double_divide(X0,double_divide(double_divide(X1,X2),X3)),multiply(X2,X1)),X3))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f571,f317])).
% 0.13/0.41 fof(f571,plain,(
% 0.13/0.41 identity=inverse(identity)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f56,f507])).
% 0.13/0.41 fof(f583,plain,(
% 0.13/0.41 ![X0]: (inverse(inverse(double_divide(identity,double_divide(identity,inverse(X0)))))=inverse(X0))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f17,f529])).
% 0.13/0.41 fof(f584,plain,(
% 0.13/0.41 ![X0]: (inverse(multiply(double_divide(identity,inverse(X0)),identity))=inverse(X0))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f15,f583])).
% 0.13/0.41 fof(f593,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (inverse(double_divide(X0,double_divide(double_divide(X1,double_divide(double_divide(X2,X3),X0)),multiply(X3,X2))))=X1)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f531])).
% 0.13/0.41 fof(f594,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (multiply(double_divide(double_divide(X0,double_divide(double_divide(X1,X2),X3)),multiply(X2,X1)),X3)=X0)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f15,f593])).
% 0.13/0.41 fof(f615,plain,(
% 0.13/0.41 ![X0,X1,X2]: (inverse(double_divide(X0,double_divide(double_divide(X1,double_divide(X2,X0)),inverse(X2))))=X1)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f541])).
% 0.13/0.41 fof(f616,plain,(
% 0.13/0.41 ![X0,X1,X2]: (multiply(double_divide(double_divide(X0,double_divide(X1,X2)),inverse(X1)),X2)=X0)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f15,f615])).
% 0.13/0.41 fof(f668,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (multiply(identity,double_divide(identity,double_divide(X0,identity)))=multiply(double_divide(double_divide(X0,double_divide(double_divide(X1,X2),X3)),multiply(X2,X1)),X3))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f571,f556])).
% 0.13/0.41 fof(f669,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (inverse(inverse(double_divide(identity,double_divide(X0,identity))))=multiply(double_divide(double_divide(X0,double_divide(double_divide(X1,X2),X3)),multiply(X2,X1)),X3))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f17,f668])).
% 0.13/0.41 fof(f670,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (inverse(multiply(double_divide(X0,identity),identity))=multiply(double_divide(double_divide(X0,double_divide(double_divide(X1,X2),X3)),multiply(X2,X1)),X3))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f15,f669])).
% 0.13/0.41 fof(f671,plain,(
% 0.13/0.41 ![X0,X1,X2,X3]: (inverse(multiply(inverse(X0),identity))=multiply(double_divide(double_divide(X0,double_divide(double_divide(X1,X2),X3)),multiply(X2,X1)),X3))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f670])).
% 0.13/0.41 fof(f673,plain,(
% 0.13/0.41 ![X0]: (inverse(multiply(inverse(X0),identity))=X0)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f594,f671])).
% 0.13/0.41 fof(f741,plain,(
% 0.13/0.41 ![X0]: (inverse(multiply(X0,identity))=multiply(inverse(X0),identity))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f673,f673])).
% 0.13/0.41 fof(f743,plain,(
% 0.13/0.41 ![X0,X1]: (inverse(multiply(multiply(X0,X1),identity))=double_divide(X1,X0))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f15,f673])).
% 0.13/0.41 fof(f744,plain,(
% 0.13/0.41 ![X0]: (multiply(X0,multiply(inverse(X0),identity))=identity)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f673,f543])).
% 0.13/0.41 fof(f745,plain,(
% 0.13/0.41 ![X0]: (identity=double_divide(multiply(inverse(X0),identity),X0))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f673,f9])).
% 0.13/0.41 fof(f746,plain,(
% 0.13/0.41 ![X0]: (inverse(inverse(multiply(X0,identity)))=X0)),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f741,f673])).
% 0.13/0.41 fof(f750,plain,(
% 0.13/0.41 ![X0]: (multiply(X0,inverse(multiply(X0,identity)))=identity)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f741,f744])).
% 0.13/0.41 fof(f751,plain,(
% 0.13/0.41 ![X0]: (identity=double_divide(inverse(multiply(X0,identity)),X0))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f741,f745])).
% 0.13/0.41 fof(f814,plain,(
% 0.13/0.41 ![X0,X1]: (inverse(multiply(double_divide(X0,X1),identity))=multiply(multiply(X1,X0),identity))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f15,f741])).
% 0.13/0.41 fof(f830,plain,(
% 0.13/0.41 ![X0]: (multiply(multiply(inverse(X0),identity),identity)=inverse(X0))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f814,f584])).
% 0.13/0.41 fof(f836,plain,(
% 0.13/0.41 ![X0]: (multiply(inverse(multiply(X0,identity)),identity)=inverse(X0))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f741,f830])).
% 0.13/0.41 fof(f837,plain,(
% 0.13/0.41 ![X0]: (inverse(multiply(multiply(X0,identity),identity))=inverse(X0))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f741,f836])).
% 0.13/0.41 fof(f844,plain,(
% 0.13/0.41 ![X0]: (double_divide(identity,X0)=inverse(X0))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f743,f837])).
% 0.13/0.41 fof(f856,plain,(
% 0.13/0.41 ![X0]: (multiply(X0,identity)=inverse(inverse(X0)))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f844,f15])).
% 0.13/0.41 fof(f860,plain,(
% 0.13/0.41 ![X0]: (identity=double_divide(inverse(inverse(inverse(X0))),X0))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f856,f751])).
% 0.13/0.41 fof(f861,plain,(
% 0.13/0.41 ![X0]: (multiply(X0,inverse(inverse(inverse(X0))))=identity)),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f856,f750])).
% 0.13/0.41 fof(f870,plain,(
% 0.13/0.41 ![X0]: (inverse(inverse(inverse(inverse(X0))))=X0)),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f856,f746])).
% 0.13/0.41 fof(f971,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(double_divide(identity,inverse(X0)),X1)=inverse(inverse(inverse(double_divide(X0,X1)))))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f860,f616])).
% 0.13/0.41 fof(f974,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(double_divide(double_divide(X0,inverse(X1)),inverse(identity)),X1)=X0)),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f844,f616])).
% 0.13/0.41 fof(f986,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=inverse(inverse(inverse(double_divide(X0,X1)))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f844,f971])).
% 0.13/0.41 fof(f987,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=inverse(inverse(multiply(X1,X0))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f15,f986])).
% 0.13/0.41 fof(f991,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(double_divide(double_divide(X0,inverse(X1)),identity),X1)=X0)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f571,f974])).
% 0.13/0.41 fof(f992,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(inverse(double_divide(X0,inverse(X1))),X1)=X0)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f8,f991])).
% 0.13/0.41 fof(f994,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(multiply(inverse(X0),X1),X0)=X1)),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f15,f992])).
% 0.13/0.41 fof(f1160,plain,(
% 0.13/0.41 ![X0]: (multiply(identity,X0)=inverse(inverse(inverse(inverse(X0)))))),
% 0.13/0.41 inference(paramodulation,[status(thm)],[f861,f994])).
% 0.13/0.41 fof(f1172,plain,(
% 0.13/0.41 ![X0]: (inverse(inverse(X0))=inverse(inverse(inverse(inverse(X0)))))),
% 0.13/0.41 inference(forward_demodulation,[status(thm)],[f17,f1160])).
% 0.13/0.41 fof(f1183,plain,(
% 0.13/0.41 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=multiply(X1,X0))),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f1186,f987])).
% 0.13/0.41 fof(f1186,plain,(
% 0.13/0.41 ![X0]: (inverse(inverse(X0))=X0)),
% 0.13/0.42 inference(forward_demodulation,[status(thm)],[f870,f1172])).
% 0.13/0.42 fof(f1197,plain,(
% 0.13/0.42 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 0.13/0.42 inference(forward_demodulation,[status(thm)],[f1186,f1183])).
% 0.13/0.42 fof(f1198,plain,(
% 0.13/0.42 $false),
% 0.13/0.42 inference(backward_subsumption_resolution,[status(thm)],[f10,f1197])).
% 0.13/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 9.51/1.63 % Elapsed time: 1.049658 seconds
% 9.51/1.63 % CPU time: 0.178949 seconds
% 9.51/1.63 % Total memory used: 7.243 MB
% 9.51/1.63 % Net memory used: 6.811 MB
%------------------------------------------------------------------------------