%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP498-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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.11s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP498-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.53 % Computer : n006.cluster.edu
% 0.11/0.53 % Model : x86_64 x86_64
% 0.11/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.53 % Memory : 8046.5625MB
% 0.11/0.53 % OS : Linux 6.8.0-71-generic
% 0.11/0.53 % CPULimit : 300
% 0.11/0.53 % WCLimit : 300
% 0.11/0.53 % DateTime : Sun Sep 20 20:14:29 UTC 2026
% 0.11/0.53 % CPUTime :
% 0.11/0.54 % Drodi V4.1.1
% 0.11/0.58 % Refutation found
% 0.11/0.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.11/0.58 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.58 fof(f1,axiom,(
% 0.11/0.58 (![A,B,C]: (double_divide(double_divide(identity,double_divide(A,double_divide(B,identity))),double_divide(double_divide(B,double_divide(C,A)),identity)) = C ))),
% 0.11/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.58 fof(f2,axiom,(
% 0.11/0.58 (![A,B]: (multiply(A,B) = double_divide(double_divide(B,A),identity) ))),
% 0.11/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.58 fof(f3,axiom,(
% 0.11/0.58 (![A]: (inverse(A) = double_divide(A,identity) ))),
% 0.11/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.58 fof(f4,axiom,(
% 0.11/0.58 (![A]: (identity = double_divide(A,inverse(A)) ))),
% 0.11/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.58 fof(f5,negated_conjecture,(
% 0.11/0.58 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 0.11/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.58 fof(f6,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(identity,double_divide(X0,double_divide(X1,identity))),double_divide(double_divide(X1,double_divide(X2,X0)),identity))=X2)),
% 0.11/0.58 inference(cnf_transformation,[status(thm)],[f1])).
% 0.11/0.58 fof(f7,plain,(
% 0.11/0.58 ![X0,X1]: (multiply(X0,X1)=double_divide(double_divide(X1,X0),identity))),
% 0.11/0.58 inference(cnf_transformation,[status(thm)],[f2])).
% 0.11/0.58 fof(f8,plain,(
% 0.11/0.58 ![X0]: (inverse(X0)=double_divide(X0,identity))),
% 0.11/0.58 inference(cnf_transformation,[status(thm)],[f3])).
% 0.11/0.58 fof(f9,plain,(
% 0.11/0.58 ![X0]: (identity=double_divide(X0,inverse(X0)))),
% 0.11/0.58 inference(cnf_transformation,[status(thm)],[f4])).
% 0.11/0.58 fof(f10,plain,(
% 0.11/0.58 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 0.11/0.58 inference(cnf_transformation,[status(thm)],[f5])).
% 0.11/0.58 fof(f11,definition,(
% 0.11/0.58 sF1_fnc=multiply(a3,b3)),
% 0.11/0.58 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.11/0.58 fof(f12,definition,(
% 0.11/0.58 sF0_fnc=multiply(sF1_fnc,c3)),
% 0.11/0.58 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.11/0.58 fof(f13,definition,(
% 0.11/0.58 sF3_fnc=multiply(b3,c3)),
% 0.11/0.58 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 0.11/0.58 fof(f14,definition,(
% 0.11/0.58 sF2_fnc=multiply(a3,sF3_fnc)),
% 0.11/0.58 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 0.11/0.58 fof(f15,plain,(
% 0.11/0.58 ~sF0_fnc=sF2_fnc),
% 0.11/0.58 inference(definition_folding,[],[f10,f14,f13,f12,f11])).
% 0.11/0.58 fof(f16,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(identity,double_divide(X0,double_divide(X1,identity))),multiply(double_divide(X2,X0),X1))=X2)),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f7,f6])).
% 0.11/0.58 fof(f17,plain,(
% 0.11/0.58 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f8,f7])).
% 0.11/0.58 fof(f18,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(identity,double_divide(X0,inverse(X1))),multiply(double_divide(X2,X0),X1))=X2)),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f8,f16])).
% 0.11/0.58 fof(f19,plain,(
% 0.11/0.58 ![X0]: (multiply(inverse(X0),X0)=inverse(identity))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f9,f17])).
% 0.11/0.58 fof(f20,plain,(
% 0.11/0.58 ![X0]: (multiply(identity,X0)=inverse(inverse(X0)))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f8,f17])).
% 0.11/0.58 fof(f21,plain,(
% 0.11/0.58 ![X0,X1]: (identity=double_divide(double_divide(X0,X1),multiply(X1,X0)))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f17,f9])).
% 0.11/0.58 fof(f24,plain,(
% 0.11/0.58 ![X0,X1]: (multiply(identity,double_divide(X0,X1))=inverse(multiply(X1,X0)))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f17,f20])).
% 0.11/0.58 fof(f37,plain,(
% 0.11/0.58 identity=double_divide(double_divide(c3,sF1_fnc),sF0_fnc)),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f12,f21])).
% 0.11/0.58 fof(f39,plain,(
% 0.11/0.58 identity=double_divide(double_divide(b3,a3),sF1_fnc)),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f11,f21])).
% 0.11/0.58 fof(f48,plain,(
% 0.11/0.58 identity=inverse(identity)),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f21,f18])).
% 0.11/0.58 fof(f49,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(double_divide(identity,identity),multiply(double_divide(X0,X1),X1))=X0)),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f9,f18])).
% 0.11/0.58 fof(f51,plain,(
% 0.11/0.58 ![X0,X1,X2,X3]: (double_divide(double_divide(identity,double_divide(X0,multiply(X1,X2))),multiply(double_divide(X3,X0),double_divide(X2,X1)))=X3)),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f17,f18])).
% 0.11/0.58 fof(f52,plain,(
% 0.11/0.58 ![X0,X1,X2,X3]: (double_divide(double_divide(identity,double_divide(multiply(double_divide(X0,X1),X2),inverse(X3))),multiply(X0,X3))=double_divide(identity,double_divide(X1,inverse(X2))))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f18,f18])).
% 0.11/0.58 fof(f57,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(double_divide(identity,double_divide(identity,inverse(X0))),multiply(inverse(X1),X0))=X1)),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f8,f18])).
% 0.11/0.58 fof(f60,plain,(
% 0.11/0.58 ![X0,X1,X2]: (multiply(multiply(double_divide(X0,X1),X2),double_divide(identity,double_divide(X1,inverse(X2))))=inverse(X0))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f18,f17])).
% 0.11/0.58 fof(f61,plain,(
% 0.11/0.58 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f48,f19])).
% 0.11/0.58 fof(f65,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(inverse(identity),multiply(double_divide(X0,X1),X1))=X0)),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f8,f49])).
% 0.11/0.58 fof(f66,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(identity,multiply(double_divide(X0,X1),X1))=X0)),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f48,f65])).
% 0.11/0.58 fof(f107,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(identity,multiply(X0,multiply(double_divide(X0,X1),X2)))=double_divide(identity,double_divide(X1,inverse(X2))))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f18,f66])).
% 0.11/0.58 fof(f108,plain,(
% 0.11/0.58 double_divide(identity,multiply(identity,sF0_fnc))=double_divide(c3,sF1_fnc)),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f37,f66])).
% 0.11/0.58 fof(f110,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(identity,multiply(identity,multiply(X0,X1)))=double_divide(X1,X0))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f21,f66])).
% 0.11/0.58 fof(f112,plain,(
% 0.11/0.58 ![X0]: (double_divide(identity,multiply(identity,inverse(X0)))=X0)),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f9,f66])).
% 0.11/0.58 fof(f116,plain,(
% 0.11/0.58 ![X0,X1]: (multiply(multiply(double_divide(X0,X1),X1),identity)=inverse(X0))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f66,f17])).
% 0.11/0.58 fof(f131,plain,(
% 0.11/0.58 double_divide(identity,multiply(identity,sF1_fnc))=double_divide(b3,a3)),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f39,f66])).
% 0.11/0.58 fof(f157,plain,(
% 0.11/0.58 ![X0]: (multiply(multiply(identity,inverse(X0)),identity)=inverse(X0))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f112,f17])).
% 0.11/0.58 fof(f187,plain,(
% 0.11/0.58 ![X0,X1,X2,X3]: (double_divide(double_divide(identity,double_divide(multiply(X0,X1),multiply(X2,X3))),multiply(identity,double_divide(X3,X2)))=double_divide(X1,X0))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f21,f51])).
% 0.11/0.58 fof(f237,plain,(
% 0.11/0.58 ![X0,X1,X2,X3]: (double_divide(double_divide(identity,double_divide(multiply(X0,X1),multiply(X2,X3))),inverse(multiply(X2,X3)))=double_divide(X1,X0))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f24,f187])).
% 0.11/0.58 fof(f284,plain,(
% 0.11/0.58 ![X0,X1]: (multiply(multiply(identity,multiply(X0,X1)),identity)=inverse(double_divide(X1,X0)))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f17,f157])).
% 0.11/0.58 fof(f291,plain,(
% 0.11/0.58 ![X0,X1]: (multiply(multiply(identity,multiply(X0,X1)),identity)=multiply(X0,X1))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f17,f284])).
% 0.11/0.58 fof(f443,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(identity,double_divide(multiply(inverse(X0),X1),inverse(X2))),multiply(X0,X2))=double_divide(identity,double_divide(identity,inverse(X1))))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f8,f52])).
% 0.11/0.58 fof(f580,plain,(
% 0.11/0.58 ![X0,X1,X2,X3]: (double_divide(double_divide(identity,double_divide(multiply(double_divide(identity,X0),X1),inverse(double_divide(X2,X3)))),inverse(multiply(X3,X2)))=double_divide(identity,double_divide(X0,inverse(X1))))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f24,f52])).
% 0.11/0.58 fof(f607,plain,(
% 0.11/0.58 ![X0,X1,X2,X3]: (double_divide(double_divide(identity,double_divide(multiply(double_divide(identity,X0),X1),multiply(X2,X3))),inverse(multiply(X2,X3)))=double_divide(identity,double_divide(X0,inverse(X1))))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f17,f580])).
% 0.11/0.58 fof(f613,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(identity,double_divide(multiply(inverse(X0),X1),inverse(X2))),multiply(X0,X2))=double_divide(X1,double_divide(identity,identity)))),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f654,f443])).
% 0.11/0.58 fof(f614,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(double_divide(X0,double_divide(identity,identity)),multiply(inverse(X1),X0))=X1)),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f654,f57])).
% 0.11/0.58 fof(f652,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(identity,multiply(X0,multiply(double_divide(X0,X1),X2)))=double_divide(X2,double_divide(identity,X1)))),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f654,f107])).
% 0.11/0.58 fof(f653,plain,(
% 0.11/0.58 ![X0,X1,X2]: (multiply(multiply(double_divide(X0,X1),X2),double_divide(X2,double_divide(identity,X1)))=inverse(X0))),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f654,f60])).
% 0.11/0.58 fof(f654,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(X0,double_divide(identity,X1))=double_divide(identity,double_divide(X1,inverse(X0))))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f237,f607])).
% 0.11/0.58 fof(f664,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(identity,multiply(inverse(X1),X2))),multiply(X1,X0))=double_divide(X2,double_divide(identity,identity)))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f654,f613])).
% 0.11/0.58 fof(f665,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(identity,multiply(inverse(X1),X2))),multiply(X1,X0))=double_divide(X2,inverse(identity)))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f8,f664])).
% 0.11/0.58 fof(f666,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(identity,multiply(inverse(X1),X2))),multiply(X1,X0))=double_divide(X2,identity))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f48,f665])).
% 0.11/0.58 fof(f667,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(identity,multiply(inverse(X1),X2))),multiply(X1,X0))=inverse(X2))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f8,f666])).
% 0.11/0.58 fof(f668,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(double_divide(X0,inverse(identity)),multiply(inverse(X1),X0))=X1)),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f8,f614])).
% 0.11/0.58 fof(f669,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(double_divide(X0,identity),multiply(inverse(X1),X0))=X1)),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f48,f668])).
% 0.11/0.58 fof(f670,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(inverse(X0),multiply(inverse(X1),X0))=X1)),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f8,f669])).
% 0.11/0.58 fof(f686,plain,(
% 0.11/0.58 ![X0]: (double_divide(inverse(X0),identity)=X0)),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f61,f670])).
% 0.11/0.58 fof(f700,plain,(
% 0.11/0.58 ![X0]: (multiply(identity,X0)=X0)),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f701,f20])).
% 0.11/0.58 fof(f701,plain,(
% 0.11/0.58 ![X0]: (inverse(inverse(X0))=X0)),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f8,f686])).
% 0.11/0.58 fof(f712,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(X0,X1)=inverse(multiply(X1,X0)))),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f700,f24])).
% 0.11/0.58 fof(f719,plain,(
% 0.11/0.58 ![X0]: (double_divide(identity,inverse(X0))=X0)),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f700,f112])).
% 0.11/0.58 fof(f724,plain,(
% 0.11/0.58 double_divide(identity,sF1_fnc)=double_divide(b3,a3)),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f700,f131])).
% 0.11/0.58 fof(f727,plain,(
% 0.11/0.58 ![X0,X1]: (multiply(multiply(X0,X1),identity)=multiply(X0,X1))),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f700,f291])).
% 0.11/0.58 fof(f728,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(identity,multiply(X0,X1))=double_divide(X1,X0))),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f700,f110])).
% 0.11/0.58 fof(f732,plain,(
% 0.11/0.58 double_divide(identity,sF0_fnc)=double_divide(c3,sF1_fnc)),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f700,f108])).
% 0.11/0.58 fof(f783,plain,(
% 0.11/0.58 ![X0,X1]: (multiply(double_divide(X0,X1),X1)=inverse(X0))),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f727,f116])).
% 0.11/0.58 fof(f788,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(X0,double_divide(X1,X0))=X1)),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f728,f66])).
% 0.11/0.58 fof(f789,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(X1,inverse(X2))),multiply(X2,X0))=inverse(X1))),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f728,f667])).
% 0.11/0.58 fof(f802,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(multiply(double_divide(X0,X1),X2),X0)=double_divide(X2,double_divide(identity,X1)))),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f728,f652])).
% 0.11/0.58 fof(f922,plain,(
% 0.11/0.58 ![X0,X1,X2,X3]: (double_divide(multiply(double_divide(X0,X1),double_divide(X2,X3)),X0)=double_divide(identity,double_divide(X1,multiply(X3,X2))))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f51,f788])).
% 0.11/0.58 fof(f924,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(double_divide(X0,X1),X0)=X1)),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f788,f788])).
% 0.11/0.58 fof(f935,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),double_divide(identity,X2))=double_divide(identity,double_divide(X2,multiply(X1,X0))))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f802,f922])).
% 0.11/0.58 fof(f965,plain,(
% 0.11/0.58 ![X0]: (double_divide(identity,X0)=inverse(X0))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f701,f719])).
% 0.11/0.58 fof(f978,plain,(
% 0.11/0.58 ![X0,X1,X2,X3]: (double_divide(inverse(double_divide(X0,multiply(X1,X2))),multiply(double_divide(X3,X0),double_divide(X2,X1)))=X3)),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f965,f51])).
% 0.11/0.58 fof(f979,plain,(
% 0.11/0.58 ![X0,X1,X2]: (multiply(multiply(double_divide(X0,X1),X2),double_divide(X2,inverse(X1)))=inverse(X0))),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f965,f653])).
% 0.11/0.58 fof(f989,plain,(
% 0.11/0.58 inverse(sF0_fnc)=double_divide(c3,sF1_fnc)),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f965,f732])).
% 0.11/0.58 fof(f999,plain,(
% 0.11/0.58 inverse(sF1_fnc)=double_divide(b3,a3)),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f965,f724])).
% 0.11/0.58 fof(f1011,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(X0,double_divide(identity,X1))=inverse(double_divide(X1,inverse(X0))))),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f965,f654])).
% 0.11/0.58 fof(f1012,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),double_divide(identity,X2))=inverse(double_divide(X2,multiply(X1,X0))))),
% 0.11/0.58 inference(backward_demodulation,[status(thm)],[f965,f935])).
% 0.11/0.58 fof(f1041,plain,(
% 0.11/0.58 ![X0,X1,X2,X3]: (double_divide(multiply(multiply(X0,X1),X2),multiply(double_divide(X3,X2),double_divide(X1,X0)))=X3)),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f17,f978])).
% 0.11/0.58 fof(f1064,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(X0,inverse(X1))=inverse(double_divide(X1,inverse(X0))))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f965,f1011])).
% 0.11/0.58 fof(f1075,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(X0,inverse(X1))=multiply(inverse(X0),X1))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f17,f1064])).
% 0.11/0.58 fof(f1076,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),inverse(X2))=inverse(double_divide(X2,multiply(X1,X0))))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f965,f1012])).
% 0.11/0.58 fof(f1077,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),inverse(X2))=multiply(multiply(X1,X0),X2))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f17,f1076])).
% 0.11/0.58 fof(f1148,plain,(
% 0.11/0.58 ![X0,X1]: (multiply(X0,double_divide(X0,X1))=inverse(X1))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f924,f17])).
% 0.11/0.58 fof(f1186,plain,(
% 0.11/0.58 ![X0,X1,X2,X3]: (double_divide(X0,multiply(multiply(X1,X2),X3))=multiply(double_divide(X0,X3),double_divide(X2,X1)))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f1041,f924])).
% 0.11/0.58 fof(f1326,plain,(
% 0.11/0.58 ![X0]: (multiply(multiply(inverse(sF1_fnc),X0),double_divide(X0,inverse(a3)))=inverse(b3))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f999,f979])).
% 0.11/0.58 fof(f1355,plain,(
% 0.11/0.58 ![X0]: (multiply(double_divide(sF1_fnc,inverse(X0)),double_divide(X0,inverse(a3)))=inverse(b3))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f1075,f1326])).
% 0.11/0.58 fof(f1356,plain,(
% 0.11/0.58 ![X0]: (double_divide(sF1_fnc,multiply(multiply(inverse(a3),X0),inverse(X0)))=inverse(b3))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f1186,f1355])).
% 0.11/0.58 fof(f1357,plain,(
% 0.11/0.58 ![X0]: (double_divide(sF1_fnc,multiply(double_divide(a3,inverse(X0)),inverse(X0)))=inverse(b3))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f1075,f1356])).
% 0.11/0.58 fof(f1358,plain,(
% 0.11/0.58 double_divide(sF1_fnc,inverse(a3))=inverse(b3)),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f783,f1357])).
% 0.11/0.58 fof(f1560,plain,(
% 0.11/0.58 ![X0,X1]: (double_divide(inverse(X0),inverse(X1))=multiply(X0,X1))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f701,f1075])).
% 0.11/0.58 fof(f1646,plain,(
% 0.11/0.58 ![X0,X1,X2]: (multiply(inverse(X0),multiply(X1,X2))=inverse(double_divide(X2,double_divide(X0,inverse(X1)))))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f789,f783])).
% 0.11/0.58 fof(f1703,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(X0,inverse(multiply(X1,X2)))=inverse(double_divide(X2,double_divide(X0,inverse(X1)))))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f1075,f1646])).
% 0.11/0.58 fof(f1704,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(X0,double_divide(X1,X2))=inverse(double_divide(X1,double_divide(X0,inverse(X2)))))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f712,f1703])).
% 0.11/0.58 fof(f1708,plain,(
% 0.11/0.58 ![X0,X1,X2]: (double_divide(X0,double_divide(X1,X2))=multiply(double_divide(X0,inverse(X2)),X1))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f17,f1704])).
% 0.11/0.58 fof(f2102,plain,(
% 0.11/0.58 ![X0]: (double_divide(inverse(b3),inverse(X0))=multiply(multiply(inverse(a3),sF1_fnc),X0))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f1358,f1077])).
% 0.11/0.58 fof(f2150,plain,(
% 0.11/0.58 ![X0]: (multiply(b3,X0)=multiply(multiply(inverse(a3),sF1_fnc),X0))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f1560,f2102])).
% 0.11/0.58 fof(f2151,plain,(
% 0.11/0.58 ![X0]: (multiply(b3,X0)=multiply(double_divide(a3,inverse(sF1_fnc)),X0))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f1075,f2150])).
% 0.11/0.58 fof(f2152,plain,(
% 0.11/0.58 ![X0]: (multiply(b3,X0)=double_divide(a3,double_divide(X0,sF1_fnc)))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f1708,f2151])).
% 0.11/0.58 fof(f2329,plain,(
% 0.11/0.58 multiply(b3,c3)=double_divide(a3,inverse(sF0_fnc))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f989,f2152])).
% 0.11/0.58 fof(f2340,plain,(
% 0.11/0.58 sF3_fnc=double_divide(a3,inverse(sF0_fnc))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f13,f2329])).
% 0.11/0.58 fof(f2480,plain,(
% 0.11/0.58 multiply(a3,sF3_fnc)=inverse(inverse(sF0_fnc))),
% 0.11/0.58 inference(paramodulation,[status(thm)],[f2340,f1148])).
% 0.11/0.58 fof(f2487,plain,(
% 0.11/0.58 sF2_fnc=inverse(inverse(sF0_fnc))),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f14,f2480])).
% 0.11/0.58 fof(f2488,plain,(
% 0.11/0.58 sF2_fnc=sF0_fnc),
% 0.11/0.58 inference(forward_demodulation,[status(thm)],[f701,f2487])).
% 0.11/0.58 fof(f2489,plain,(
% 0.11/0.58 $false),
% 0.11/0.58 inference(forward_subsumption_resolution,[status(thm)],[f2488,f15])).
% 0.11/0.58 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.62 % Elapsed time: 0.082788 seconds
% 0.15/0.62 % CPU time: 0.329188 seconds
% 0.15/0.62 % Total memory used: 11.048 MB
% 0.15/0.62 % Net memory used: 10.639 MB
%------------------------------------------------------------------------------