%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP489-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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:42 PM UTC 2026
% Result : Unsatisfiable 0.16s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP489-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n026.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Sun Sep 20 20:17:37 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 0.16/0.59 % Refutation found
% 0.16/0.59 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.16/0.59 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.59 fof(f1,axiom,(
% 0.16/0.59 (![A,B,C]: (double_divide(A,double_divide(double_divide(double_divide(identity,double_divide(double_divide(A,identity),double_divide(B,C))),B),identity)) = C ))),
% 0.16/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.59 fof(f2,axiom,(
% 0.16/0.59 (![A,B]: (multiply(A,B) = double_divide(double_divide(B,A),identity) ))),
% 0.16/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.59 fof(f3,axiom,(
% 0.16/0.59 (![A]: (inverse(A) = double_divide(A,identity) ))),
% 0.16/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.59 fof(f4,axiom,(
% 0.16/0.59 (![A]: (identity = double_divide(A,inverse(A)) ))),
% 0.16/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.59 fof(f5,negated_conjecture,(
% 0.16/0.59 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 0.16/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.59 fof(f6,plain,(
% 0.16/0.59 ![X0,X1,X2]: (double_divide(X0,double_divide(double_divide(double_divide(identity,double_divide(double_divide(X0,identity),double_divide(X1,X2))),X1),identity))=X2)),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f1])).
% 0.16/0.59 fof(f7,plain,(
% 0.16/0.59 ![X0,X1]: (multiply(X0,X1)=double_divide(double_divide(X1,X0),identity))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f2])).
% 0.16/0.59 fof(f8,plain,(
% 0.16/0.59 ![X0]: (inverse(X0)=double_divide(X0,identity))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f3])).
% 0.16/0.59 fof(f9,plain,(
% 0.16/0.59 ![X0]: (identity=double_divide(X0,inverse(X0)))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.59 fof(f10,plain,(
% 0.16/0.59 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 0.16/0.59 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/0.59 fof(f11,definition,(
% 0.16/0.59 sF1_fnc=multiply(a3,b3)),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.16/0.59 fof(f12,definition,(
% 0.16/0.59 sF0_fnc=multiply(sF1_fnc,c3)),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.16/0.59 fof(f13,definition,(
% 0.16/0.59 sF3_fnc=multiply(b3,c3)),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 0.16/0.59 fof(f14,definition,(
% 0.16/0.59 sF2_fnc=multiply(a3,sF3_fnc)),
% 0.16/0.59 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 0.16/0.59 fof(f15,plain,(
% 0.16/0.59 ~sF0_fnc=sF2_fnc),
% 0.16/0.59 inference(definition_folding,[],[f10,f14,f13,f12,f11])).
% 0.16/0.59 fof(f16,plain,(
% 0.16/0.59 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(double_divide(X0,identity),double_divide(X1,X2)))))=X2)),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f7,f6])).
% 0.16/0.59 fof(f17,plain,(
% 0.16/0.59 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f8,f7])).
% 0.16/0.59 fof(f18,plain,(
% 0.16/0.59 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),double_divide(X1,X2)))))=X2)),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f8,f16])).
% 0.16/0.59 fof(f19,plain,(
% 0.16/0.59 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,X1),multiply(X2,double_divide(identity,double_divide(multiply(X1,X0),double_divide(X2,X3)))))=X3)),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f17,f18])).
% 0.16/0.59 fof(f20,plain,(
% 0.16/0.59 ![X0,X1,X2,X3]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),X2))))=multiply(X3,double_divide(identity,double_divide(inverse(X1),double_divide(X3,X2)))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f18,f18])).
% 0.16/0.59 fof(f21,plain,(
% 0.16/0.59 ![X0,X1,X2]: (multiply(multiply(X0,double_divide(identity,double_divide(inverse(X1),double_divide(X0,X2)))),X1)=inverse(X2))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f18,f17])).
% 0.16/0.59 fof(f26,plain,(
% 0.16/0.59 ![X0,X1]: (double_divide(double_divide(sF3_fnc,a3),multiply(X0,double_divide(identity,double_divide(sF2_fnc,double_divide(X0,X1)))))=X1)),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f14,f19])).
% 0.16/0.59 fof(f49,plain,(
% 0.16/0.59 ![X0,X1,X2,X3]: (multiply(multiply(X0,double_divide(identity,double_divide(inverse(X1),X2))),X1)=inverse(multiply(X3,double_divide(identity,double_divide(inverse(X0),double_divide(X3,X2))))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f20,f17])).
% 0.16/0.59 fof(f57,plain,(
% 0.16/0.59 ![X0,X1]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),inverse(X1)))))=identity)),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f8,f18])).
% 0.16/0.59 fof(f58,plain,(
% 0.16/0.59 ![X0]: (multiply(identity,X0)=inverse(inverse(X0)))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f8,f17])).
% 0.16/0.59 fof(f62,plain,(
% 0.16/0.59 ![X0,X1]: (identity=double_divide(double_divide(X0,X1),multiply(X1,X0)))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f17,f9])).
% 0.16/0.59 fof(f63,plain,(
% 0.16/0.59 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,identity)))=multiply(X2,double_divide(identity,double_divide(inverse(X1),double_divide(X2,inverse(inverse(X0)))))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f9,f20])).
% 0.16/0.59 fof(f64,plain,(
% 0.16/0.59 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),inverse(X2)))))=multiply(X2,double_divide(identity,double_divide(inverse(X1),identity))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f9,f20])).
% 0.16/0.59 fof(f67,plain,(
% 0.16/0.59 ![X0,X1]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),identity))))=inverse(X1))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f9,f18])).
% 0.16/0.59 fof(f68,plain,(
% 0.16/0.59 ![X0]: (multiply(inverse(X0),X0)=inverse(identity))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f9,f17])).
% 0.16/0.59 fof(f69,plain,(
% 0.16/0.59 ![X0,X1,X2]: (double_divide(X0,multiply(X1,inverse(identity)))=multiply(X2,double_divide(identity,double_divide(inverse(X1),double_divide(X2,inverse(inverse(X0)))))))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f8,f63])).
% 0.16/0.59 fof(f70,plain,(
% 0.16/0.59 ![X0]: (multiply(X0,double_divide(identity,inverse(inverse(X0))))=identity)),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f71,f57])).
% 0.16/0.59 fof(f71,plain,(
% 0.16/0.59 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),inverse(X2)))))=multiply(X2,double_divide(identity,inverse(inverse(X1)))))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f8,f64])).
% 0.16/0.59 fof(f74,plain,(
% 0.16/0.59 ![X0,X1]: (double_divide(X0,multiply(X1,double_divide(identity,inverse(inverse(X0)))))=inverse(X1))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f8,f67])).
% 0.16/0.59 fof(f82,plain,(
% 0.16/0.59 ![X0,X1]: (double_divide(X0,inverse(inverse(double_divide(identity,double_divide(inverse(X0),double_divide(identity,X1))))))=X1)),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f58,f18])).
% 0.16/0.59 fof(f83,plain,(
% 0.16/0.59 ![X0,X1,X2]: (double_divide(X0,inverse(inverse(double_divide(identity,double_divide(inverse(X0),X1)))))=multiply(X2,double_divide(identity,double_divide(inverse(identity),double_divide(X2,X1)))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f58,f20])).
% 0.16/0.59 fof(f86,plain,(
% 0.16/0.59 ![X0,X1]: (double_divide(X0,inverse(multiply(double_divide(inverse(X0),double_divide(identity,X1)),identity)))=X1)),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f17,f82])).
% 0.16/0.59 fof(f87,plain,(
% 0.16/0.59 ![X0,X1,X2]: (double_divide(X0,inverse(multiply(double_divide(inverse(X0),X1),identity)))=multiply(X2,double_divide(identity,double_divide(inverse(identity),double_divide(X2,X1)))))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f17,f83])).
% 0.16/0.59 fof(f97,plain,(
% 0.16/0.59 identity=double_divide(double_divide(c3,b3),sF3_fnc)),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f13,f62])).
% 0.16/0.59 fof(f102,plain,(
% 0.16/0.59 ![X0,X1,X2,X3]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),multiply(X2,X3)))))=multiply(double_divide(X3,X2),double_divide(identity,double_divide(inverse(X1),identity))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f62,f20])).
% 0.16/0.59 fof(f117,plain,(
% 0.16/0.59 ![X0,X1,X2,X3]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),multiply(X2,X3)))))=multiply(double_divide(X3,X2),double_divide(identity,inverse(inverse(X1)))))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f8,f102])).
% 0.16/0.59 fof(f124,plain,(
% 0.16/0.59 ![X0,X1]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),sF3_fnc))))=multiply(double_divide(c3,b3),double_divide(identity,double_divide(inverse(X1),identity))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f97,f20])).
% 0.16/0.59 fof(f129,plain,(
% 0.16/0.59 ![X0,X1]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),sF3_fnc))))=multiply(double_divide(c3,b3),double_divide(identity,inverse(inverse(X1)))))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f8,f124])).
% 0.16/0.59 fof(f162,plain,(
% 0.16/0.59 ![X0,X1,X2]: (double_divide(X0,inverse(X1))=inverse(multiply(X2,double_divide(identity,double_divide(inverse(double_divide(identity,inverse(inverse(X0)))),double_divide(X2,X1))))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f21,f74])).
% 0.16/0.59 fof(f163,plain,(
% 0.16/0.59 ![X0]: (double_divide(X0,inverse(inverse(double_divide(identity,inverse(inverse(X0))))))=inverse(identity))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f58,f74])).
% 0.16/0.59 fof(f164,plain,(
% 0.16/0.59 ![X0]: (double_divide(X0,inverse(identity))=inverse(inverse(double_divide(identity,inverse(inverse(X0))))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f68,f74])).
% 0.16/0.59 fof(f166,plain,(
% 0.16/0.59 ![X0,X1,X2,X3]: (double_divide(X0,multiply(X1,double_divide(identity,inverse(X2))))=multiply(X3,double_divide(identity,double_divide(inverse(X1),double_divide(X3,multiply(X2,double_divide(identity,inverse(inverse(inverse(X0))))))))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f74,f20])).
% 0.16/0.59 fof(f167,plain,(
% 0.16/0.59 ![X0,X1,X2]: (multiply(multiply(X0,double_divide(identity,double_divide(inverse(X1),inverse(X2)))),X1)=inverse(multiply(X2,double_divide(identity,inverse(inverse(X0))))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f74,f21])).
% 0.16/0.59 fof(f174,plain,(
% 0.16/0.59 ![X0,X1,X2]: (double_divide(X0,inverse(X1))=inverse(multiply(X2,double_divide(identity,double_divide(multiply(inverse(inverse(X0)),identity),double_divide(X2,X1))))))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f17,f162])).
% 0.16/0.59 fof(f175,plain,(
% 0.16/0.59 ![X0]: (double_divide(X0,inverse(multiply(inverse(inverse(X0)),identity)))=inverse(identity))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f17,f163])).
% 0.16/0.59 fof(f176,plain,(
% 0.16/0.59 ![X0]: (double_divide(X0,double_divide(X0,inverse(identity)))=inverse(identity))),
% 0.16/0.59 inference(backward_demodulation,[status(thm)],[f177,f175])).
% 0.16/0.59 fof(f177,plain,(
% 0.16/0.59 ![X0]: (double_divide(X0,inverse(identity))=inverse(multiply(inverse(inverse(X0)),identity)))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f17,f164])).
% 0.16/0.59 fof(f187,plain,(
% 0.16/0.59 ![X0,X1,X2]: (double_divide(double_divide(double_divide(identity,inverse(inverse(X0))),X0),multiply(X1,double_divide(identity,double_divide(identity,double_divide(X1,X2)))))=X2)),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f70,f19])).
% 0.16/0.59 fof(f350,plain,(
% 0.16/0.59 ![X0,X1]: (double_divide(double_divide(sF3_fnc,a3),multiply(X0,double_divide(identity,double_divide(sF2_fnc,inverse(X1)))))=multiply(X1,double_divide(identity,inverse(inverse(X0)))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f74,f26])).
% 0.16/0.59 fof(f388,plain,(
% 0.16/0.59 ![X0,X1]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),inverse(identity)))))=multiply(inverse(X1),double_divide(identity,inverse(identity))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f176,f20])).
% 0.16/0.59 fof(f391,plain,(
% 0.16/0.59 ![X0]: (double_divide(double_divide(sF3_fnc,a3),multiply(X0,double_divide(identity,double_divide(sF2_fnc,inverse(identity)))))=double_divide(X0,inverse(identity)))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f176,f26])).
% 0.16/0.59 fof(f394,plain,(
% 0.16/0.59 ![X0,X1]: (multiply(multiply(X0,double_divide(identity,double_divide(inverse(X1),inverse(identity)))),X1)=inverse(double_divide(X0,inverse(identity))))),
% 0.16/0.59 inference(paramodulation,[status(thm)],[f176,f21])).
% 0.16/0.59 fof(f406,plain,(
% 0.16/0.59 ![X0]: (multiply(identity,double_divide(identity,inverse(inverse(X0))))=multiply(inverse(X0),double_divide(identity,inverse(identity))))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f71,f388])).
% 0.16/0.59 fof(f407,plain,(
% 0.16/0.59 ![X0]: (inverse(inverse(double_divide(identity,inverse(inverse(X0)))))=multiply(inverse(X0),double_divide(identity,inverse(identity))))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f58,f406])).
% 0.16/0.59 fof(f408,plain,(
% 0.16/0.59 ![X0]: (inverse(multiply(inverse(inverse(X0)),identity))=multiply(inverse(X0),double_divide(identity,inverse(identity))))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f17,f407])).
% 0.16/0.59 fof(f409,plain,(
% 0.16/0.59 ![X0]: (double_divide(X0,inverse(identity))=multiply(inverse(X0),double_divide(identity,inverse(identity))))),
% 0.16/0.59 inference(forward_demodulation,[status(thm)],[f177,f408])).
% 0.16/0.60 fof(f411,plain,(
% 0.16/0.60 ![X0]: (multiply(inverse(X0),identity)=inverse(multiply(inverse(inverse(X0)),identity)))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f413,f177])).
% 0.16/0.60 fof(f413,plain,(
% 0.16/0.60 ![X0]: (double_divide(X0,inverse(identity))=multiply(inverse(X0),identity))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f9,f409])).
% 0.16/0.60 fof(f417,plain,(
% 0.16/0.60 ![X0]: (multiply(identity,double_divide(identity,inverse(inverse(X0))))=double_divide(X0,inverse(identity)))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f350,f391])).
% 0.16/0.60 fof(f418,plain,(
% 0.16/0.60 ![X0]: (inverse(inverse(double_divide(identity,inverse(inverse(X0)))))=double_divide(X0,inverse(identity)))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f58,f417])).
% 0.16/0.60 fof(f419,plain,(
% 0.16/0.60 ![X0]: (inverse(multiply(inverse(inverse(X0)),identity))=double_divide(X0,inverse(identity)))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f17,f418])).
% 0.16/0.60 fof(f420,plain,(
% 0.16/0.60 ![X0]: (inverse(multiply(inverse(inverse(X0)),identity))=multiply(inverse(X0),identity))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f413,f419])).
% 0.16/0.60 fof(f429,plain,(
% 0.16/0.60 ![X0]: (inverse(multiply(identity,double_divide(identity,inverse(inverse(X0)))))=inverse(double_divide(X0,inverse(identity))))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f167,f394])).
% 0.16/0.60 fof(f430,plain,(
% 0.16/0.60 ![X0]: (inverse(inverse(inverse(double_divide(identity,inverse(inverse(X0))))))=inverse(double_divide(X0,inverse(identity))))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f58,f429])).
% 0.16/0.60 fof(f431,plain,(
% 0.16/0.60 ![X0]: (inverse(inverse(multiply(inverse(inverse(X0)),identity)))=inverse(double_divide(X0,inverse(identity))))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f17,f430])).
% 0.16/0.60 fof(f432,plain,(
% 0.16/0.60 ![X0]: (inverse(multiply(inverse(X0),identity))=inverse(double_divide(X0,inverse(identity))))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f420,f431])).
% 0.16/0.60 fof(f434,plain,(
% 0.16/0.60 ![X0]: (inverse(multiply(inverse(X0),identity))=multiply(inverse(identity),X0))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f17,f432])).
% 0.16/0.60 fof(f451,plain,(
% 0.16/0.60 ![X0]: (multiply(inverse(X0),identity)=multiply(inverse(identity),inverse(X0)))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f434,f411])).
% 0.16/0.60 fof(f452,plain,(
% 0.16/0.60 identity=multiply(inverse(identity),identity)),
% 0.16/0.60 inference(paramodulation,[status(thm)],[f9,f413])).
% 0.16/0.60 fof(f465,plain,(
% 0.16/0.60 ![X0]: (double_divide(X0,identity)=multiply(inverse(X0),identity))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f482,f413])).
% 0.16/0.60 fof(f471,plain,(
% 0.16/0.60 ![X0]: (multiply(inverse(X0),identity)=multiply(identity,inverse(X0)))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f482,f451])).
% 0.16/0.60 fof(f479,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,inverse(multiply(double_divide(inverse(X0),X1),identity)))=multiply(X2,double_divide(identity,double_divide(identity,double_divide(X2,X1)))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f482,f87])).
% 0.16/0.60 fof(f481,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,multiply(X1,identity))=multiply(X2,double_divide(identity,double_divide(inverse(X1),double_divide(X2,inverse(inverse(X0)))))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f482,f69])).
% 0.16/0.60 fof(f482,plain,(
% 0.16/0.60 identity=inverse(identity)),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f68,f452])).
% 0.16/0.60 fof(f510,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,inverse(X1))=inverse(multiply(X2,double_divide(identity,double_divide(inverse(inverse(X0)),double_divide(X2,X1))))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f520,f174])).
% 0.16/0.60 fof(f520,plain,(
% 0.16/0.60 ![X0]: (inverse(X0)=multiply(inverse(X0),identity))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f8,f465])).
% 0.16/0.60 fof(f521,plain,(
% 0.16/0.60 ![X0]: (inverse(X0)=multiply(identity,inverse(X0)))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f520,f471])).
% 0.16/0.60 fof(f522,plain,(
% 0.16/0.60 ![X0,X1,X2,X3]: (double_divide(X0,multiply(X1,double_divide(identity,inverse(X2))))=multiply(X3,double_divide(identity,double_divide(inverse(X1),double_divide(X3,multiply(X2,double_divide(identity,inverse(X0))))))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f523,f166])).
% 0.16/0.60 fof(f523,plain,(
% 0.16/0.60 ![X0]: (inverse(X0)=inverse(inverse(inverse(X0))))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f58,f521])).
% 0.16/0.60 fof(f538,plain,(
% 0.16/0.60 ![X0,X1]: (multiply(multiply(X0,double_divide(identity,double_divide(identity,double_divide(X0,X1)))),identity)=inverse(X1))),
% 0.16/0.60 inference(paramodulation,[status(thm)],[f482,f21])).
% 0.16/0.60 fof(f541,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(identity,multiply(X0,double_divide(identity,double_divide(identity,X1))))=multiply(X2,double_divide(identity,double_divide(inverse(X0),double_divide(X2,X1)))))),
% 0.16/0.60 inference(paramodulation,[status(thm)],[f482,f20])).
% 0.16/0.60 fof(f542,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(identity,multiply(X0,double_divide(identity,double_divide(identity,double_divide(X0,X1)))))=X1)),
% 0.16/0.60 inference(paramodulation,[status(thm)],[f482,f18])).
% 0.16/0.60 fof(f552,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),X2))))=double_divide(identity,multiply(X1,double_divide(identity,double_divide(identity,X2)))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f541,f20])).
% 0.16/0.60 fof(f556,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(X0,inverse(X1))=inverse(double_divide(identity,multiply(inverse(X0),double_divide(identity,double_divide(identity,X1))))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f541,f510])).
% 0.16/0.60 fof(f558,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(X0,multiply(X1,identity))=double_divide(identity,multiply(X1,double_divide(identity,double_divide(identity,inverse(inverse(X0)))))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f541,f481])).
% 0.16/0.60 fof(f559,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,inverse(X2))))=double_divide(identity,multiply(X1,double_divide(identity,double_divide(identity,multiply(X2,double_divide(identity,inverse(X0))))))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f541,f522])).
% 0.16/0.60 fof(f570,plain,(
% 0.16/0.60 ![X0,X1,X2]: (multiply(multiply(X0,double_divide(identity,double_divide(inverse(X1),X2))),X1)=inverse(double_divide(identity,multiply(X0,double_divide(identity,double_divide(identity,X2))))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f541,f49])).
% 0.16/0.60 fof(f582,plain,(
% 0.16/0.60 ![X0]: (double_divide(identity,multiply(X0,double_divide(identity,double_divide(identity,sF3_fnc))))=multiply(double_divide(c3,b3),double_divide(identity,inverse(inverse(X0)))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f552,f129])).
% 0.16/0.60 fof(f583,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(identity,multiply(X0,double_divide(identity,double_divide(identity,inverse(X1)))))=multiply(X1,double_divide(identity,inverse(inverse(X0)))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f552,f71])).
% 0.16/0.60 fof(f584,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(identity,multiply(X0,double_divide(identity,double_divide(identity,multiply(X1,X2)))))=multiply(double_divide(X2,X1),double_divide(identity,inverse(inverse(X0)))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f552,f117])).
% 0.16/0.60 fof(f590,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(X0,inverse(X1))=multiply(multiply(inverse(X0),double_divide(identity,double_divide(identity,X1))),identity))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f17,f556])).
% 0.16/0.60 fof(f618,plain,(
% 0.16/0.60 ![X0,X1]: (multiply(multiply(X0,double_divide(identity,double_divide(identity,inverse(X1)))),identity)=inverse(multiply(X1,double_divide(identity,inverse(inverse(X0))))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f620,f167])).
% 0.16/0.60 fof(f620,plain,(
% 0.16/0.60 ![X0,X1,X2]: (multiply(multiply(X0,double_divide(identity,double_divide(inverse(X1),X2))),X1)=multiply(multiply(X0,double_divide(identity,double_divide(identity,X2))),identity))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f17,f570])).
% 0.16/0.60 fof(f629,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(X0,multiply(X1,identity))=multiply(inverse(X0),double_divide(identity,inverse(inverse(X1)))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f583,f558])).
% 0.16/0.60 fof(f631,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,inverse(X2))))=multiply(double_divide(double_divide(identity,inverse(X0)),X2),double_divide(identity,inverse(inverse(X1)))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f584,f559])).
% 0.16/0.60 fof(f647,plain,(
% 0.16/0.60 ![X0,X1]: (inverse(double_divide(X0,X1))=multiply(multiply(X1,X0),identity))),
% 0.16/0.60 inference(paramodulation,[status(thm)],[f17,f520])).
% 0.16/0.60 fof(f653,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(X0,inverse(X1))=multiply(inverse(X0),double_divide(identity,double_divide(identity,X1))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f662,f590])).
% 0.16/0.60 fof(f658,plain,(
% 0.16/0.60 ![X0,X1]: (multiply(X0,double_divide(identity,double_divide(identity,inverse(X1))))=inverse(multiply(X1,double_divide(identity,inverse(inverse(X0))))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f662,f618])).
% 0.16/0.60 fof(f659,plain,(
% 0.16/0.60 ![X0,X1]: (multiply(X0,double_divide(identity,double_divide(identity,double_divide(X0,X1))))=inverse(X1))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f662,f538])).
% 0.16/0.60 fof(f662,plain,(
% 0.16/0.60 ![X0,X1]: (multiply(X0,X1)=multiply(multiply(X0,X1),identity))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f17,f647])).
% 0.16/0.60 fof(f664,plain,(
% 0.16/0.60 ![X0]: (double_divide(identity,inverse(X0))=X0)),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f659,f542])).
% 0.16/0.60 fof(f665,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(X0,inverse(multiply(double_divide(inverse(X0),X1),identity)))=inverse(X1))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f659,f479])).
% 0.16/0.60 fof(f666,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(double_divide(double_divide(identity,inverse(inverse(X0))),X0),inverse(X1))=X1)),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f659,f187])).
% 0.16/0.60 fof(f667,plain,(
% 0.16/0.60 ![X0]: (multiply(X0,inverse(X0))=identity)),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f664,f70])).
% 0.16/0.60 fof(f675,plain,(
% 0.16/0.60 ![X0,X1]: (multiply(X0,double_divide(identity,double_divide(identity,inverse(X1))))=inverse(multiply(X1,inverse(X0))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f664,f658])).
% 0.16/0.60 fof(f676,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,inverse(X2))))=multiply(double_divide(double_divide(identity,inverse(X0)),X2),inverse(X1)))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f664,f631])).
% 0.16/0.60 fof(f678,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(X0,multiply(X1,identity))=multiply(inverse(X0),inverse(X1)))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f664,f629])).
% 0.16/0.60 fof(f680,plain,(
% 0.16/0.60 ![X0]: (double_divide(identity,multiply(X0,double_divide(identity,double_divide(identity,sF3_fnc))))=multiply(double_divide(c3,b3),inverse(X0)))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f664,f582])).
% 0.16/0.60 fof(f694,plain,(
% 0.16/0.60 ![X0]: (inverse(double_divide(identity,X0))=X0)),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f665,f86])).
% 0.16/0.60 fof(f695,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(double_divide(inverse(X0),X0),inverse(X1))=X1)),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f664,f666])).
% 0.16/0.60 fof(f697,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(X0,inverse(X1))=inverse(multiply(double_divide(identity,X1),inverse(inverse(X0)))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f727,f653])).
% 0.16/0.60 fof(f715,plain,(
% 0.16/0.60 ![X0,X1]: (inverse(multiply(double_divide(identity,double_divide(X0,X1)),inverse(X0)))=inverse(X1))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f727,f659])).
% 0.16/0.60 fof(f721,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,multiply(X1,double_divide(identity,double_divide(inverse(X0),X2))))=double_divide(identity,inverse(multiply(double_divide(identity,X2),inverse(X1)))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f727,f552])).
% 0.16/0.60 fof(f723,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(identity,inverse(multiply(double_divide(identity,X0),inverse(X1))))=multiply(X2,double_divide(identity,double_divide(inverse(X1),double_divide(X2,X0)))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f727,f541])).
% 0.16/0.60 fof(f727,plain,(
% 0.16/0.60 ![X0,X1]: (multiply(X0,double_divide(identity,X1))=inverse(multiply(X1,inverse(X0))))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f664,f675])).
% 0.16/0.60 fof(f728,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,inverse(multiply(inverse(X1),inverse(X2))))=multiply(double_divide(double_divide(identity,inverse(X0)),X1),inverse(X2)))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f727,f676])).
% 0.16/0.60 fof(f729,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,inverse(multiply(inverse(X1),inverse(X2))))=multiply(double_divide(X0,X1),inverse(X2)))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f664,f728])).
% 0.16/0.60 fof(f739,plain,(
% 0.16/0.60 ![X0]: (double_divide(identity,inverse(multiply(double_divide(identity,sF3_fnc),inverse(X0))))=multiply(double_divide(c3,b3),inverse(X0)))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f727,f680])).
% 0.16/0.60 fof(f740,plain,(
% 0.16/0.60 ![X0]: (multiply(double_divide(identity,sF3_fnc),inverse(X0))=multiply(double_divide(c3,b3),inverse(X0)))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f664,f739])).
% 0.16/0.60 fof(f774,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(X0,X1)=multiply(inverse(X0),inverse(X1)))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f775,f678])).
% 0.16/0.60 fof(f775,plain,(
% 0.16/0.60 ![X0]: (multiply(X0,identity)=X0)),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f17,f694])).
% 0.16/0.60 fof(f839,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,inverse(multiply(double_divide(inverse(X0),X1),inverse(X2))))=double_divide(identity,inverse(multiply(double_divide(identity,X1),inverse(X2)))))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f727,f721])).
% 0.16/0.60 fof(f840,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,inverse(multiply(double_divide(inverse(X0),X1),inverse(X2))))=multiply(double_divide(identity,X1),inverse(X2)))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f664,f839])).
% 0.16/0.60 fof(f844,plain,(
% 0.16/0.60 ![X0,X1,X2]: (multiply(double_divide(identity,X0),inverse(X1))=multiply(X2,double_divide(identity,double_divide(inverse(X1),double_divide(X2,X0)))))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f664,f723])).
% 0.16/0.60 fof(f845,plain,(
% 0.16/0.60 ![X0,X1,X2]: (multiply(double_divide(identity,X0),inverse(X1))=inverse(multiply(double_divide(inverse(X1),double_divide(X2,X0)),inverse(X2))))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f727,f844])).
% 0.16/0.60 fof(f873,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,inverse(double_divide(X1,X2)))=multiply(double_divide(X0,X1),inverse(X2)))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f774,f729])).
% 0.16/0.60 fof(f875,plain,(
% 0.16/0.60 ![X0,X1]: (inverse(double_divide(identity,multiply(X0,double_divide(X0,X1))))=inverse(X1))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f906,f715])).
% 0.16/0.60 fof(f879,plain,(
% 0.16/0.60 ![X0]: (double_divide(identity,multiply(X0,sF3_fnc))=multiply(double_divide(c3,b3),inverse(X0)))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f906,f740])).
% 0.16/0.60 fof(f882,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(X0,inverse(X1))=inverse(double_divide(identity,multiply(inverse(X0),X1))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f906,f697])).
% 0.16/0.60 fof(f883,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(identity,multiply(X0,X1))=inverse(multiply(double_divide(inverse(X0),double_divide(X2,X1)),inverse(X2))))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f906,f845])).
% 0.16/0.60 fof(f884,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,inverse(multiply(double_divide(inverse(X0),X1),inverse(X2))))=double_divide(identity,multiply(X2,X1)))),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f906,f840])).
% 0.16/0.60 fof(f906,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(X0,multiply(X1,X2))=multiply(double_divide(X0,X2),inverse(X1)))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f17,f873])).
% 0.16/0.60 fof(f908,plain,(
% 0.16/0.60 ![X0,X1]: (multiply(multiply(X0,double_divide(X0,X1)),identity)=inverse(X1))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f17,f875])).
% 0.16/0.60 fof(f910,plain,(
% 0.16/0.60 ![X0,X1]: (multiply(X0,double_divide(X0,X1))=inverse(X1))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f662,f908])).
% 0.16/0.60 fof(f914,plain,(
% 0.16/0.60 ![X0]: (double_divide(identity,multiply(X0,sF3_fnc))=double_divide(c3,multiply(X0,b3)))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f906,f879])).
% 0.16/0.60 fof(f916,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(X0,inverse(X1))=multiply(multiply(inverse(X0),X1),identity))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f17,f882])).
% 0.16/0.60 fof(f918,plain,(
% 0.16/0.60 ![X0,X1]: (multiply(inverse(double_divide(inverse(X0),X0)),X1)=X1)),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f921,f695])).
% 0.16/0.60 fof(f921,plain,(
% 0.16/0.60 ![X0,X1]: (double_divide(X0,inverse(X1))=multiply(inverse(X0),X1))),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f662,f916])).
% 0.16/0.60 fof(f922,plain,(
% 0.16/0.60 ![X0,X1,X2]: (double_divide(identity,multiply(X0,X1))=inverse(double_divide(inverse(X0),multiply(X2,double_divide(X2,X1)))))),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f906,f883])).
% 0.16/0.61 fof(f923,plain,(
% 0.16/0.61 ![X0,X1,X2]: (double_divide(identity,multiply(X0,X1))=multiply(multiply(X2,double_divide(X2,X1)),inverse(X0)))),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f17,f922])).
% 0.16/0.61 fof(f924,plain,(
% 0.16/0.61 ![X0,X1]: (double_divide(identity,multiply(X0,X1))=multiply(inverse(X1),inverse(X0)))),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f910,f923])).
% 0.16/0.61 fof(f926,plain,(
% 0.16/0.61 ![X0]: (double_divide(sF3_fnc,X0)=double_divide(c3,multiply(X0,b3)))),
% 0.16/0.61 inference(backward_demodulation,[status(thm)],[f930,f914])).
% 0.16/0.61 fof(f930,plain,(
% 0.16/0.61 ![X0,X1]: (double_divide(identity,multiply(X0,X1))=double_divide(X1,X0))),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f774,f924])).
% 0.16/0.61 fof(f931,plain,(
% 0.16/0.61 ![X0,X1,X2]: (multiply(inverse(X0),multiply(double_divide(inverse(X0),X1),inverse(X2)))=double_divide(identity,multiply(X2,X1)))),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f921,f884])).
% 0.16/0.61 fof(f932,plain,(
% 0.16/0.61 ![X0,X1,X2]: (multiply(inverse(X0),double_divide(inverse(X0),multiply(X1,X2)))=double_divide(identity,multiply(X1,X2)))),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f906,f931])).
% 0.16/0.61 fof(f933,plain,(
% 0.16/0.61 ![X0,X1]: (inverse(multiply(X0,X1))=double_divide(identity,multiply(X0,X1)))),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f910,f932])).
% 0.16/0.61 fof(f935,plain,(
% 0.16/0.61 ![X0,X1]: (inverse(multiply(X0,X1))=double_divide(X1,X0))),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f930,f933])).
% 0.16/0.61 fof(f1003,plain,(
% 0.16/0.61 ![X0,X1]: (multiply(multiply(X0,inverse(X0)),X1)=X1)),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f17,f918])).
% 0.16/0.61 fof(f1004,plain,(
% 0.16/0.61 ![X0]: (X0=inverse(inverse(X0)))),
% 0.16/0.61 inference(backward_demodulation,[status(thm)],[f1005,f58])).
% 0.16/0.61 fof(f1005,plain,(
% 0.16/0.61 ![X0]: (multiply(identity,X0)=X0)),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f667,f1003])).
% 0.16/0.61 fof(f1086,plain,(
% 0.16/0.61 inverse(sF0_fnc)=double_divide(c3,sF1_fnc)),
% 0.16/0.61 inference(paramodulation,[status(thm)],[f12,f935])).
% 0.16/0.61 fof(f1087,plain,(
% 0.16/0.61 inverse(sF2_fnc)=double_divide(sF3_fnc,a3)),
% 0.16/0.61 inference(paramodulation,[status(thm)],[f14,f935])).
% 0.16/0.61 fof(f1810,plain,(
% 0.16/0.61 double_divide(sF3_fnc,a3)=double_divide(c3,sF1_fnc)),
% 0.16/0.61 inference(paramodulation,[status(thm)],[f11,f926])).
% 0.16/0.61 fof(f1821,plain,(
% 0.16/0.61 inverse(sF2_fnc)=double_divide(c3,sF1_fnc)),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f1087,f1810])).
% 0.16/0.61 fof(f1825,plain,(
% 0.16/0.61 inverse(sF2_fnc)=inverse(sF0_fnc)),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f1086,f1821])).
% 0.16/0.61 fof(f1842,plain,(
% 0.16/0.61 sF2_fnc=inverse(inverse(sF0_fnc))),
% 0.16/0.61 inference(paramodulation,[status(thm)],[f1825,f1004])).
% 0.16/0.61 fof(f1858,plain,(
% 0.16/0.61 sF2_fnc=sF0_fnc),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f1004,f1842])).
% 0.16/0.61 fof(f1859,plain,(
% 0.16/0.61 $false),
% 0.16/0.61 inference(forward_subsumption_resolution,[status(thm)],[f1858,f15])).
% 0.16/0.61 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.63 % Elapsed time: 0.171773 seconds
% 0.16/0.63 % CPU time: 0.978546 seconds
% 0.16/0.63 % Total memory used: 32.118 MB
% 0.16/0.63 % Net memory used: 29.858 MB
%------------------------------------------------------------------------------