%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP492-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 : n001.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:43 PM UTC 2026
% Result : Unsatisfiable 0.08s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP492-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n001.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 20:20:28 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.08/0.41 % Refutation found
% 0.08/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.08/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.41 fof(f1,axiom,(
% 0.08/0.41 (![A,B,C]: (double_divide(double_divide(identity,A),double_divide(identity,double_divide(double_divide(double_divide(A,B),identity),double_divide(C,B)))) = C ))),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f2,axiom,(
% 0.08/0.41 (![A,B]: (multiply(A,B) = double_divide(double_divide(B,A),identity) ))),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f3,axiom,(
% 0.08/0.41 (![A]: (inverse(A) = double_divide(A,identity) ))),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f4,axiom,(
% 0.08/0.41 (![A]: (identity = double_divide(A,inverse(A)) ))),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f5,negated_conjecture,(
% 0.08/0.41 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f6,plain,(
% 0.08/0.41 ![X0,X1,X2]: (double_divide(double_divide(identity,X0),double_divide(identity,double_divide(double_divide(double_divide(X0,X1),identity),double_divide(X2,X1))))=X2)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f1])).
% 0.08/0.41 fof(f7,plain,(
% 0.08/0.41 ![X0,X1]: (multiply(X0,X1)=double_divide(double_divide(X1,X0),identity))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f2])).
% 0.08/0.41 fof(f8,plain,(
% 0.08/0.41 ![X0]: (inverse(X0)=double_divide(X0,identity))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.08/0.41 fof(f9,plain,(
% 0.08/0.41 ![X0]: (identity=double_divide(X0,inverse(X0)))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.08/0.41 fof(f10,plain,(
% 0.08/0.41 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f5])).
% 0.08/0.41 fof(f11,definition,(
% 0.08/0.41 sF1_fnc=multiply(a3,b3)),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.08/0.41 fof(f12,definition,(
% 0.08/0.41 sF0_fnc=multiply(sF1_fnc,c3)),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.08/0.41 fof(f13,definition,(
% 0.08/0.41 sF3_fnc=multiply(b3,c3)),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 0.08/0.41 fof(f14,definition,(
% 0.08/0.41 sF2_fnc=multiply(a3,sF3_fnc)),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 0.08/0.41 fof(f15,plain,(
% 0.08/0.41 ~sF0_fnc=sF2_fnc),
% 0.08/0.41 inference(definition_folding,[],[f10,f14,f13,f12,f11])).
% 0.08/0.41 fof(f16,plain,(
% 0.08/0.41 ![X0,X1,X2]: (double_divide(double_divide(identity,X0),double_divide(identity,double_divide(multiply(X1,X0),double_divide(X2,X1))))=X2)),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f7,f6])).
% 0.08/0.41 fof(f17,plain,(
% 0.08/0.41 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f8,f7])).
% 0.08/0.41 fof(f18,plain,(
% 0.08/0.41 ![X0]: (multiply(inverse(X0),X0)=inverse(identity))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f9,f17])).
% 0.08/0.41 fof(f19,plain,(
% 0.08/0.41 ![X0]: (multiply(identity,X0)=inverse(inverse(X0)))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f8,f17])).
% 0.08/0.41 fof(f20,plain,(
% 0.08/0.41 ![X0,X1]: (identity=double_divide(double_divide(X0,X1),multiply(X1,X0)))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f17,f9])).
% 0.08/0.41 fof(f23,plain,(
% 0.08/0.41 ![X0,X1]: (multiply(identity,double_divide(X0,X1))=inverse(multiply(X1,X0)))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f17,f19])).
% 0.08/0.41 fof(f37,plain,(
% 0.08/0.41 identity=double_divide(double_divide(sF3_fnc,a3),sF2_fnc)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f14,f20])).
% 0.08/0.41 fof(f38,plain,(
% 0.08/0.41 identity=double_divide(double_divide(b3,a3),sF1_fnc)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f11,f20])).
% 0.08/0.41 fof(f47,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(identity,double_divide(identity,double_divide(multiply(X0,inverse(identity)),double_divide(X1,X0))))=X1)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f9,f16])).
% 0.08/0.41 fof(f48,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(inverse(identity),double_divide(identity,double_divide(multiply(X0,identity),double_divide(X1,X0))))=X1)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f8,f16])).
% 0.08/0.41 fof(f50,plain,(
% 0.08/0.41 ![X0]: (double_divide(double_divide(identity,c3),double_divide(identity,double_divide(sF3_fnc,double_divide(X0,b3))))=X0)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f13,f16])).
% 0.08/0.41 fof(f51,plain,(
% 0.08/0.41 ![X0]: (double_divide(double_divide(identity,c3),double_divide(identity,double_divide(sF0_fnc,double_divide(X0,sF1_fnc))))=X0)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f12,f16])).
% 0.08/0.41 fof(f58,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(double_divide(identity,X0),double_divide(identity,double_divide(multiply(inverse(X1),X0),identity)))=X1)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f9,f16])).
% 0.08/0.41 fof(f66,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(double_divide(identity,X0),double_divide(identity,inverse(multiply(inverse(X1),X0))))=X1)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f58])).
% 0.08/0.41 fof(f101,plain,(
% 0.08/0.41 ![X0]: (double_divide(identity,double_divide(identity,double_divide(multiply(inverse(X0),inverse(identity)),identity)))=X0)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f9,f47])).
% 0.08/0.41 fof(f106,plain,(
% 0.08/0.41 ![X0,X1]: (multiply(double_divide(identity,double_divide(multiply(X0,inverse(identity)),double_divide(X1,X0))),identity)=inverse(X1))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f47,f17])).
% 0.08/0.41 fof(f116,plain,(
% 0.08/0.41 ![X0]: (double_divide(identity,double_divide(identity,inverse(multiply(inverse(X0),inverse(identity)))))=X0)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f101])).
% 0.08/0.41 fof(f231,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(inverse(identity),double_divide(identity,double_divide(multiply(double_divide(identity,double_divide(multiply(X0,inverse(identity)),double_divide(X1,X0))),identity),X1)))=identity)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f47,f48])).
% 0.08/0.41 fof(f232,plain,(
% 0.08/0.41 double_divide(inverse(identity),double_divide(identity,double_divide(multiply(sF1_fnc,identity),identity)))=double_divide(b3,a3)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f38,f48])).
% 0.08/0.41 fof(f233,plain,(
% 0.08/0.41 double_divide(inverse(identity),double_divide(identity,double_divide(multiply(sF2_fnc,identity),identity)))=double_divide(sF3_fnc,a3)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f37,f48])).
% 0.08/0.41 fof(f237,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(inverse(identity),double_divide(identity,double_divide(multiply(multiply(X0,X1),identity),identity)))=double_divide(X1,X0))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f20,f48])).
% 0.08/0.41 fof(f240,plain,(
% 0.08/0.41 ![X0]: (double_divide(inverse(identity),double_divide(identity,double_divide(multiply(inverse(X0),identity),identity)))=X0)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f9,f48])).
% 0.08/0.41 fof(f247,plain,(
% 0.08/0.41 ![X0,X1]: (multiply(double_divide(identity,double_divide(multiply(X0,identity),double_divide(X1,X0))),inverse(identity))=inverse(X1))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f48,f17])).
% 0.08/0.41 fof(f249,plain,(
% 0.08/0.41 ![X0]: (double_divide(inverse(identity),double_divide(identity,double_divide(inverse(X0),X0)))=identity)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f106,f231])).
% 0.08/0.41 fof(f250,plain,(
% 0.08/0.41 double_divide(inverse(identity),double_divide(identity,inverse(multiply(sF1_fnc,identity))))=double_divide(b3,a3)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f232])).
% 0.08/0.41 fof(f251,plain,(
% 0.08/0.41 double_divide(inverse(identity),double_divide(identity,inverse(multiply(sF2_fnc,identity))))=double_divide(sF3_fnc,a3)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f233])).
% 0.08/0.41 fof(f255,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(inverse(identity),double_divide(identity,inverse(multiply(multiply(X0,X1),identity))))=double_divide(X1,X0))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f237])).
% 0.08/0.41 fof(f259,plain,(
% 0.08/0.41 ![X0]: (double_divide(inverse(identity),double_divide(identity,inverse(multiply(inverse(X0),identity))))=X0)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f240])).
% 0.08/0.41 fof(f277,plain,(
% 0.08/0.41 double_divide(inverse(identity),double_divide(identity,inverse(inverse(identity))))=identity),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f8,f249])).
% 0.08/0.41 fof(f283,plain,(
% 0.08/0.41 ![X0]: (multiply(identity,identity)=inverse(multiply(double_divide(identity,double_divide(inverse(X0),X0)),inverse(identity))))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f249,f23])).
% 0.08/0.41 fof(f284,plain,(
% 0.08/0.41 ![X0]: (double_divide(identity,double_divide(identity,double_divide(multiply(double_divide(identity,double_divide(inverse(X0),X0)),inverse(identity)),identity)))=inverse(identity))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f249,f47])).
% 0.08/0.41 fof(f288,plain,(
% 0.08/0.41 double_divide(inverse(identity),double_divide(identity,multiply(identity,identity)))=identity),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f19,f277])).
% 0.08/0.41 fof(f290,plain,(
% 0.08/0.41 ![X0]: (double_divide(identity,double_divide(identity,inverse(multiply(double_divide(identity,double_divide(inverse(X0),X0)),inverse(identity)))))=inverse(identity))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f284])).
% 0.08/0.41 fof(f291,plain,(
% 0.08/0.41 double_divide(identity,double_divide(identity,multiply(identity,identity)))=inverse(identity)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f283,f290])).
% 0.08/0.41 fof(f408,plain,(
% 0.08/0.41 ![X0]: (double_divide(identity,double_divide(identity,double_divide(multiply(double_divide(identity,inverse(multiply(inverse(X0),identity))),inverse(identity)),X0)))=inverse(identity))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f259,f47])).
% 0.08/0.41 fof(f411,plain,(
% 0.08/0.41 ![X0]: (multiply(double_divide(identity,inverse(multiply(inverse(X0),identity))),inverse(identity))=inverse(X0))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f259,f17])).
% 0.08/0.41 fof(f417,plain,(
% 0.08/0.41 ![X0]: (double_divide(identity,double_divide(identity,double_divide(inverse(X0),X0)))=inverse(identity))),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f411,f408])).
% 0.08/0.41 fof(f452,plain,(
% 0.08/0.41 double_divide(double_divide(identity,c3),double_divide(identity,double_divide(sF0_fnc,identity)))=double_divide(b3,a3)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f38,f51])).
% 0.08/0.41 fof(f460,plain,(
% 0.08/0.41 double_divide(double_divide(identity,c3),double_divide(identity,inverse(sF0_fnc)))=double_divide(b3,a3)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f452])).
% 0.08/0.41 fof(f491,plain,(
% 0.08/0.41 ![X0]: (double_divide(double_divide(identity,X0),double_divide(identity,inverse(inverse(identity))))=X0)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f18,f66])).
% 0.08/0.41 fof(f498,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(identity,double_divide(identity,double_divide(multiply(double_divide(identity,inverse(multiply(inverse(X0),X1))),inverse(identity)),X0)))=double_divide(identity,X1))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f66,f47])).
% 0.08/0.41 fof(f502,plain,(
% 0.08/0.41 ![X0]: (double_divide(double_divide(identity,X0),double_divide(identity,multiply(identity,identity)))=X0)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f19,f491])).
% 0.08/0.41 fof(f513,plain,(
% 0.08/0.41 ![X0]: (double_divide(X0,double_divide(identity,multiply(identity,identity)))=double_divide(identity,inverse(multiply(inverse(X0),inverse(identity)))))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f116,f502])).
% 0.08/0.41 fof(f514,plain,(
% 0.08/0.41 double_divide(inverse(identity),double_divide(identity,multiply(identity,identity)))=double_divide(identity,multiply(identity,identity))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f291,f502])).
% 0.08/0.41 fof(f516,plain,(
% 0.08/0.41 ![X0]: (double_divide(inverse(identity),double_divide(identity,multiply(identity,identity)))=double_divide(identity,double_divide(inverse(X0),X0)))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f417,f502])).
% 0.08/0.41 fof(f519,plain,(
% 0.08/0.41 double_divide(inverse(identity),double_divide(identity,multiply(identity,identity)))=identity),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f8,f502])).
% 0.08/0.41 fof(f526,plain,(
% 0.08/0.41 ![X0]: (multiply(double_divide(identity,multiply(identity,identity)),double_divide(identity,X0))=inverse(X0))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f502,f17])).
% 0.08/0.41 fof(f527,plain,(
% 0.08/0.41 ![X0]: (double_divide(identity,double_divide(X0,double_divide(identity,multiply(identity,identity))))=X0)),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f513,f116])).
% 0.08/0.41 fof(f531,plain,(
% 0.08/0.41 ![X0]: (double_divide(double_divide(identity,X0),identity)=X0)),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f543,f502])).
% 0.08/0.41 fof(f543,plain,(
% 0.08/0.41 identity=double_divide(identity,multiply(identity,identity))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f288,f514])).
% 0.08/0.41 fof(f561,plain,(
% 0.08/0.41 ![X0]: (identity=double_divide(identity,double_divide(inverse(X0),X0)))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f288,f516])).
% 0.08/0.41 fof(f569,plain,(
% 0.08/0.41 double_divide(inverse(identity),identity)=identity),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f543,f519])).
% 0.08/0.41 fof(f570,plain,(
% 0.08/0.41 inverse(inverse(identity))=identity),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f569])).
% 0.08/0.41 fof(f571,plain,(
% 0.08/0.41 identity=double_divide(identity,identity)),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f577,f543])).
% 0.08/0.41 fof(f577,plain,(
% 0.08/0.41 multiply(identity,identity)=identity),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f19,f570])).
% 0.08/0.41 fof(f590,plain,(
% 0.08/0.41 ![X0]: (multiply(identity,double_divide(identity,X0))=inverse(X0))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f543,f526])).
% 0.08/0.41 fof(f592,plain,(
% 0.08/0.41 double_divide(inverse(identity),double_divide(identity,inverse(sF1_fnc)))=double_divide(b3,a3)),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f600,f250])).
% 0.08/0.41 fof(f593,plain,(
% 0.08/0.41 double_divide(inverse(identity),double_divide(identity,inverse(sF2_fnc)))=double_divide(sF3_fnc,a3)),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f600,f251])).
% 0.08/0.41 fof(f596,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(inverse(identity),double_divide(identity,inverse(multiply(X0,X1))))=double_divide(X1,X0))),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f600,f255])).
% 0.08/0.41 fof(f600,plain,(
% 0.08/0.41 ![X0]: (inverse(multiply(X0,identity))=inverse(X0))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f23,f590])).
% 0.08/0.41 fof(f601,plain,(
% 0.08/0.41 ![X0]: (double_divide(identity,double_divide(X0,identity))=X0)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f543,f527])).
% 0.08/0.41 fof(f603,plain,(
% 0.08/0.41 double_divide(double_divide(identity,c3),sF0_fnc)=double_divide(b3,a3)),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f619,f460])).
% 0.08/0.41 fof(f612,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(identity,double_divide(identity,double_divide(multiply(multiply(inverse(X0),X1),inverse(identity)),X0)))=double_divide(identity,X1))),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f619,f498])).
% 0.08/0.41 fof(f619,plain,(
% 0.08/0.41 ![X0]: (double_divide(identity,inverse(X0))=X0)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f601])).
% 0.08/0.41 fof(f627,plain,(
% 0.08/0.41 ![X0]: (inverse(double_divide(identity,X0))=X0)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f531])).
% 0.08/0.41 fof(f636,plain,(
% 0.08/0.41 ![X0,X1]: (multiply(double_divide(identity,double_divide(X0,double_divide(X1,X0))),inverse(identity))=inverse(X1))),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f637,f247])).
% 0.08/0.41 fof(f637,plain,(
% 0.08/0.41 ![X0]: (multiply(X0,identity)=X0)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f17,f627])).
% 0.08/0.41 fof(f701,plain,(
% 0.08/0.41 identity=inverse(identity)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f571])).
% 0.08/0.41 fof(f710,plain,(
% 0.08/0.41 double_divide(identity,double_divide(identity,inverse(sF1_fnc)))=double_divide(b3,a3)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f701,f592])).
% 0.08/0.41 fof(f712,plain,(
% 0.08/0.41 double_divide(identity,sF1_fnc)=double_divide(b3,a3)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f619,f710])).
% 0.08/0.41 fof(f713,plain,(
% 0.08/0.41 double_divide(identity,double_divide(identity,inverse(sF2_fnc)))=double_divide(sF3_fnc,a3)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f701,f593])).
% 0.08/0.41 fof(f715,plain,(
% 0.08/0.41 double_divide(identity,sF2_fnc)=double_divide(sF3_fnc,a3)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f619,f713])).
% 0.08/0.41 fof(f721,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(identity,double_divide(identity,inverse(multiply(X0,X1))))=double_divide(X1,X0))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f701,f596])).
% 0.08/0.41 fof(f722,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(identity,multiply(X0,X1))=double_divide(X1,X0))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f619,f721])).
% 0.08/0.41 fof(f727,plain,(
% 0.08/0.41 double_divide(double_divide(identity,c3),sF0_fnc)=double_divide(identity,sF1_fnc)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f712,f603])).
% 0.08/0.41 fof(f737,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(identity,double_divide(identity,double_divide(multiply(multiply(inverse(X0),X1),identity),X0)))=double_divide(identity,X1))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f701,f612])).
% 0.08/0.41 fof(f738,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(identity,double_divide(identity,double_divide(multiply(inverse(X0),X1),X0)))=double_divide(identity,X1))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f637,f737])).
% 0.08/0.41 fof(f751,plain,(
% 0.08/0.41 ![X0,X1]: (multiply(double_divide(identity,double_divide(X0,double_divide(X1,X0))),identity)=inverse(X1))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f701,f636])).
% 0.08/0.41 fof(f753,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(identity,double_divide(X0,double_divide(X1,X0)))=inverse(X1))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f637,f751])).
% 0.08/0.41 fof(f815,plain,(
% 0.08/0.41 ![X0]: (identity=double_divide(double_divide(identity,X0),X0))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f637,f20])).
% 0.08/0.41 fof(f876,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(double_divide(identity,X0),double_divide(identity,double_divide(multiply(X1,X0),identity)))=double_divide(identity,X1))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f815,f16])).
% 0.08/0.41 fof(f878,plain,(
% 0.08/0.41 ![X0]: (multiply(X0,double_divide(identity,X0))=inverse(identity))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f815,f17])).
% 0.08/0.41 fof(f890,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(double_divide(identity,X0),double_divide(identity,inverse(multiply(X1,X0))))=double_divide(identity,X1))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f876])).
% 0.08/0.41 fof(f898,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(double_divide(identity,X0),multiply(X1,X0))=double_divide(identity,X1))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f619,f890])).
% 0.08/0.41 fof(f905,plain,(
% 0.08/0.41 ![X0]: (multiply(X0,double_divide(identity,X0))=identity)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f701,f878])).
% 0.08/0.41 fof(f1038,plain,(
% 0.08/0.41 ![X0]: (multiply(double_divide(inverse(X0),X0),identity)=identity)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f561,f905])).
% 0.08/0.41 fof(f1041,plain,(
% 0.08/0.41 ![X0]: (multiply(identity,identity)=inverse(multiply(double_divide(inverse(X0),X0),identity)))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f561,f23])).
% 0.08/0.41 fof(f1048,plain,(
% 0.08/0.41 ![X0]: (double_divide(inverse(X0),X0)=identity)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f637,f1038])).
% 0.08/0.41 fof(f1054,plain,(
% 0.08/0.41 ![X0]: (identity=inverse(multiply(double_divide(inverse(X0),X0),identity)))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f637,f1041])).
% 0.08/0.41 fof(f1055,plain,(
% 0.08/0.41 ![X0]: (identity=inverse(double_divide(inverse(X0),X0)))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f637,f1054])).
% 0.08/0.41 fof(f1056,plain,(
% 0.08/0.41 ![X0]: (identity=multiply(X0,inverse(X0)))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f17,f1055])).
% 0.08/0.41 fof(f1079,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(double_divide(identity,inverse(X0)),double_divide(identity,double_divide(identity,double_divide(X1,X0))))=X1)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f1056,f16])).
% 0.08/0.41 fof(f1101,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(X0,double_divide(identity,double_divide(identity,double_divide(X1,X0))))=X1)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f619,f1079])).
% 0.08/0.41 fof(f1111,plain,(
% 0.08/0.41 double_divide(double_divide(identity,c3),double_divide(identity,double_divide(sF0_fnc,identity)))=inverse(sF1_fnc)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f1048,f51])).
% 0.08/0.41 fof(f1115,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(double_divide(identity,X0),double_divide(identity,double_divide(multiply(X1,X0),identity)))=inverse(X1))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f1048,f16])).
% 0.08/0.41 fof(f1129,plain,(
% 0.08/0.41 double_divide(double_divide(identity,c3),double_divide(identity,inverse(sF0_fnc)))=inverse(sF1_fnc)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f1111])).
% 0.08/0.41 fof(f1130,plain,(
% 0.08/0.41 inverse(sF1_fnc)=double_divide(identity,sF1_fnc)),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f1131,f727])).
% 0.08/0.41 fof(f1131,plain,(
% 0.08/0.41 double_divide(double_divide(identity,c3),sF0_fnc)=inverse(sF1_fnc)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f619,f1129])).
% 0.08/0.41 fof(f1138,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(double_divide(identity,X0),double_divide(identity,inverse(multiply(X1,X0))))=inverse(X1))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f8,f1115])).
% 0.08/0.41 fof(f1139,plain,(
% 0.08/0.41 ![X0]: (inverse(X0)=double_divide(identity,X0))),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f1140,f898])).
% 0.08/0.41 fof(f1140,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(double_divide(identity,X0),multiply(X1,X0))=inverse(X1))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f619,f1138])).
% 0.08/0.41 fof(f1146,plain,(
% 0.08/0.41 inverse(sF1_fnc)=double_divide(b3,a3)),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f1130,f712])).
% 0.08/0.41 fof(f1155,plain,(
% 0.08/0.41 inverse(sF2_fnc)=double_divide(sF3_fnc,a3)),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f1139,f715])).
% 0.08/0.41 fof(f1156,plain,(
% 0.08/0.41 ![X0]: (inverse(inverse(X0))=X0)),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f1139,f619])).
% 0.08/0.41 fof(f1160,plain,(
% 0.08/0.41 ![X0]: (double_divide(inverse(c3),double_divide(identity,double_divide(sF3_fnc,double_divide(X0,b3))))=X0)),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f1139,f50])).
% 0.08/0.41 fof(f1168,plain,(
% 0.08/0.41 ![X0,X1]: (inverse(multiply(X0,X1))=double_divide(X1,X0))),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f1139,f722])).
% 0.08/0.41 fof(f1184,plain,(
% 0.08/0.41 ![X0,X1]: (inverse(double_divide(identity,double_divide(multiply(inverse(X0),X1),X0)))=double_divide(identity,X1))),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f1139,f738])).
% 0.08/0.41 fof(f1188,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(X0,inverse(double_divide(identity,double_divide(X1,X0))))=X1)),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f1139,f1101])).
% 0.08/0.41 fof(f1197,plain,(
% 0.08/0.41 ![X0,X1]: (inverse(double_divide(X0,double_divide(X1,X0)))=inverse(X1))),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f1139,f753])).
% 0.08/0.41 fof(f1223,plain,(
% 0.08/0.41 ![X0]: (double_divide(inverse(c3),inverse(double_divide(sF3_fnc,double_divide(X0,b3))))=X0)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f1139,f1160])).
% 0.08/0.41 fof(f1224,plain,(
% 0.08/0.41 ![X0]: (double_divide(inverse(c3),multiply(double_divide(X0,b3),sF3_fnc))=X0)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f17,f1223])).
% 0.08/0.41 fof(f1274,plain,(
% 0.08/0.41 ![X0,X1]: (multiply(double_divide(multiply(inverse(X0),X1),X0),identity)=double_divide(identity,X1))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f17,f1184])).
% 0.08/0.41 fof(f1275,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(multiply(inverse(X0),X1),X0)=double_divide(identity,X1))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f637,f1274])).
% 0.08/0.41 fof(f1276,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(multiply(inverse(X0),X1),X0)=inverse(X1))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f1139,f1275])).
% 0.08/0.41 fof(f1286,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(X0,multiply(double_divide(X1,X0),identity))=X1)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f17,f1188])).
% 0.08/0.41 fof(f1289,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(X0,double_divide(X1,X0))=X1)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f637,f1286])).
% 0.08/0.41 fof(f1314,plain,(
% 0.08/0.41 ![X0,X1]: (multiply(double_divide(X0,X1),X1)=inverse(X0))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f17,f1197])).
% 0.08/0.41 fof(f1412,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(double_divide(X0,X1),X0)=X1)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f1289,f1289])).
% 0.08/0.41 fof(f1438,plain,(
% 0.08/0.41 ![X0,X1]: (multiply(X0,double_divide(X0,X1))=inverse(X1))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f1412,f17])).
% 0.08/0.41 fof(f1700,plain,(
% 0.08/0.41 ![X0]: (double_divide(inverse(c3),multiply(X0,sF3_fnc))=double_divide(b3,X0))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f1412,f1224])).
% 0.08/0.41 fof(f1886,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(inverse(X0),X1)=inverse(double_divide(inverse(X1),X0)))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f1438,f1276])).
% 0.08/0.41 fof(f1889,plain,(
% 0.08/0.41 ![X0,X1,X2]: (double_divide(multiply(double_divide(X0,X1),X2),multiply(X1,X0))=inverse(X2))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f1168,f1276])).
% 0.08/0.41 fof(f1896,plain,(
% 0.08/0.41 ![X0,X1]: (multiply(inverse(X0),X1)=inverse(multiply(inverse(X1),X0)))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f1276,f1314])).
% 0.08/0.41 fof(f1918,plain,(
% 0.08/0.41 ![X0,X1]: (double_divide(inverse(X0),X1)=multiply(X0,inverse(X1)))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f17,f1886])).
% 0.08/0.41 fof(f1941,plain,(
% 0.08/0.41 ![X0,X1]: (multiply(inverse(X0),X1)=double_divide(X0,inverse(X1)))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f1168,f1896])).
% 0.08/0.41 fof(f2060,plain,(
% 0.08/0.41 ![X0,X1,X2]: (double_divide(inverse(X0),multiply(X1,X2))=inverse(double_divide(double_divide(X2,X1),X0)))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f1438,f1889])).
% 0.08/0.41 fof(f2108,plain,(
% 0.08/0.41 ![X0]: (multiply(c3,double_divide(sF3_fnc,X0))=double_divide(b3,X0))),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f2114,f1700])).
% 0.08/0.41 fof(f2114,plain,(
% 0.08/0.41 ![X0,X1,X2]: (double_divide(inverse(X0),multiply(X1,X2))=multiply(X0,double_divide(X2,X1)))),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f17,f2060])).
% 0.08/0.41 fof(f2265,plain,(
% 0.08/0.41 ![X0,X1]: (multiply(X0,X1)=double_divide(inverse(X0),inverse(X1)))),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f1156,f1941])).
% 0.08/0.41 fof(f2572,plain,(
% 0.08/0.41 multiply(c3,inverse(sF2_fnc))=double_divide(b3,a3)),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f1155,f2108])).
% 0.08/0.41 fof(f2583,plain,(
% 0.08/0.41 double_divide(inverse(c3),sF2_fnc)=double_divide(b3,a3)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f1918,f2572])).
% 0.08/0.41 fof(f2584,plain,(
% 0.08/0.41 double_divide(inverse(c3),sF2_fnc)=inverse(sF1_fnc)),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f1146,f2583])).
% 0.08/0.41 fof(f2599,plain,(
% 0.08/0.41 double_divide(inverse(sF1_fnc),inverse(c3))=sF2_fnc),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f2584,f1412])).
% 0.08/0.41 fof(f2621,plain,(
% 0.08/0.41 multiply(sF1_fnc,c3)=sF2_fnc),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f2265,f2599])).
% 0.08/0.41 fof(f2622,plain,(
% 0.08/0.41 sF0_fnc=sF2_fnc),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f12,f2621])).
% 0.08/0.41 fof(f2623,plain,(
% 0.08/0.41 $false),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f2622,f15])).
% 0.08/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.08/0.43 % Elapsed time: 0.062701 seconds
% 0.08/0.43 % CPU time: 0.339161 seconds
% 0.08/0.43 % Total memory used: 19.699 MB
% 0.08/0.43 % Net memory used: 18.906 MB
%------------------------------------------------------------------------------