%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP571-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:50 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP571-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n001.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 20 20:22:27 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.36 % Drodi V4.1.1
% 0.13/0.45 % Refutation found
% 0.13/0.45 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.45 fof(f1,axiom,(
% 0.13/0.45 (![A,B,C]: (double_divide(double_divide(A,double_divide(double_divide(B,double_divide(A,C)),double_divide(C,identity))),double_divide(identity,identity)) = B ))),
% 0.13/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f2,axiom,(
% 0.13/0.45 (![A,B]: (multiply(A,B) = double_divide(double_divide(B,A),identity) ))),
% 0.13/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f3,axiom,(
% 0.13/0.45 (![A]: (inverse(A) = double_divide(A,identity) ))),
% 0.13/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f4,axiom,(
% 0.13/0.45 (![A]: (identity = double_divide(A,inverse(A)) ))),
% 0.13/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f5,negated_conjecture,(
% 0.13/0.45 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 0.13/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.45 fof(f6,plain,(
% 0.13/0.45 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(X2,identity))),double_divide(identity,identity))=X1)),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.45 fof(f7,plain,(
% 0.13/0.45 ![X0,X1]: (multiply(X0,X1)=double_divide(double_divide(X1,X0),identity))),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.45 fof(f8,plain,(
% 0.13/0.45 ![X0]: (inverse(X0)=double_divide(X0,identity))),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.45 fof(f9,plain,(
% 0.13/0.45 ![X0]: (identity=double_divide(X0,inverse(X0)))),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.45 fof(f10,plain,(
% 0.13/0.45 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 0.13/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.45 fof(f16,plain,(
% 0.13/0.45 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(X2,identity))),inverse(identity))=X1)),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f8,f6])).
% 0.13/0.45 fof(f17,plain,(
% 0.13/0.45 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f8,f7])).
% 0.13/0.45 fof(f18,plain,(
% 0.13/0.45 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),inverse(X2))),inverse(identity))=X1)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f8,f16])).
% 0.13/0.45 fof(f20,plain,(
% 0.13/0.45 ![X0,X1]: (identity=double_divide(double_divide(X0,X1),multiply(X1,X0)))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f17,f9])).
% 0.13/0.45 fof(f26,plain,(
% 0.13/0.45 ![X0,X1]: (multiply(multiply(X0,X1),double_divide(X1,X0))=inverse(identity))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f20,f17])).
% 0.13/0.45 fof(f48,plain,(
% 0.13/0.45 ![X0,X1,X2,X3]: (double_divide(double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),inverse(X2))),double_divide(double_divide(X3,X1),inverse(inverse(identity)))),inverse(identity))=X3)),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f18,f18])).
% 0.13/0.45 fof(f50,plain,(
% 0.13/0.45 ![X0,X1]: (double_divide(double_divide(X0,double_divide(double_divide(X1,identity),inverse(inverse(X0)))),inverse(identity))=X1)),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f9,f18])).
% 0.13/0.45 fof(f51,plain,(
% 0.13/0.45 ![X0,X1]: (double_divide(double_divide(X0,double_divide(double_divide(X1,inverse(X0)),inverse(identity))),inverse(identity))=X1)),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f8,f18])).
% 0.13/0.45 fof(f57,plain,(
% 0.13/0.45 ![X0,X1]: (double_divide(double_divide(X0,double_divide(inverse(X1),inverse(inverse(X0)))),inverse(identity))=X1)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f8,f50])).
% 0.13/0.45 fof(f60,plain,(
% 0.13/0.45 ![X0]: (double_divide(double_divide(X0,identity),inverse(identity))=X0)),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f9,f57])).
% 0.13/0.45 fof(f61,plain,(
% 0.13/0.45 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(multiply(X1,X2),inverse(inverse(X0)))),inverse(identity))=double_divide(X2,X1))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f17,f57])).
% 0.13/0.45 fof(f67,plain,(
% 0.13/0.45 ![X0]: (double_divide(inverse(X0),inverse(identity))=X0)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f8,f60])).
% 0.13/0.45 fof(f74,plain,(
% 0.13/0.45 ![X0]: (multiply(inverse(identity),inverse(X0))=inverse(X0))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f67,f17])).
% 0.13/0.45 fof(f77,plain,(
% 0.13/0.45 ![X0,X1]: (multiply(inverse(identity),multiply(X0,X1))=inverse(double_divide(X1,X0)))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f17,f74])).
% 0.13/0.45 fof(f80,plain,(
% 0.13/0.45 ![X0,X1]: (multiply(inverse(identity),multiply(X0,X1))=multiply(X0,X1))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f17,f77])).
% 0.13/0.45 fof(f87,plain,(
% 0.13/0.45 ![X0,X1,X2,X3]: (double_divide(double_divide(double_divide(double_divide(X0,X1),double_divide(double_divide(X2,identity),inverse(multiply(X1,X0)))),double_divide(double_divide(X3,X2),inverse(inverse(identity)))),inverse(identity))=X3)),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f20,f48])).
% 0.13/0.45 fof(f91,plain,(
% 0.13/0.45 ![X0,X1,X2]: (double_divide(double_divide(double_divide(X0,double_divide(double_divide(inverse(identity),double_divide(X0,X1)),inverse(X1))),double_divide(X2,inverse(inverse(identity)))),inverse(identity))=inverse(X2))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f67,f48])).
% 0.13/0.45 fof(f92,plain,(
% 0.13/0.45 ![X0,X1,X2,X3,X4,X5]: (double_divide(double_divide(double_divide(X0,double_divide(double_divide(inverse(identity),double_divide(X0,X1)),inverse(X1))),double_divide(X2,inverse(inverse(identity)))),inverse(identity))=double_divide(double_divide(X3,double_divide(double_divide(X4,double_divide(X3,X5)),inverse(X5))),double_divide(double_divide(X2,X4),inverse(inverse(identity)))))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f48,f48])).
% 0.13/0.45 fof(f93,plain,(
% 0.13/0.45 ![X0,X1,X2,X3]: (double_divide(double_divide(double_divide(X0,double_divide(double_divide(inverse(identity),double_divide(X0,X1)),inverse(X1))),double_divide(X2,inverse(inverse(identity)))),inverse(identity))=double_divide(X3,double_divide(inverse(X2),inverse(inverse(X3)))))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f57,f48])).
% 0.13/0.45 fof(f94,plain,(
% 0.13/0.45 ![X0,X1,X2,X3,X4]: (double_divide(double_divide(double_divide(X0,double_divide(double_divide(inverse(identity),double_divide(X0,X1)),inverse(X1))),double_divide(X2,inverse(inverse(identity)))),inverse(identity))=double_divide(X3,double_divide(double_divide(X2,double_divide(X3,X4)),inverse(X4))))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f18,f48])).
% 0.13/0.45 fof(f95,plain,(
% 0.13/0.45 ![X0,X1,X2,X3]: (double_divide(double_divide(double_divide(X0,double_divide(double_divide(multiply(X1,X2),double_divide(X0,X3)),inverse(X3))),double_divide(identity,inverse(inverse(identity)))),inverse(identity))=double_divide(X2,X1))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f20,f48])).
% 0.13/0.45 fof(f96,plain,(
% 0.13/0.45 ![X0,X1,X2]: (double_divide(double_divide(double_divide(X0,double_divide(double_divide(inverse(X1),double_divide(X0,X2)),inverse(X2))),double_divide(identity,inverse(inverse(identity)))),inverse(identity))=X1)),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f9,f48])).
% 0.13/0.45 fof(f102,plain,(
% 0.13/0.45 ![X0,X1,X2,X3]: (double_divide(double_divide(double_divide(double_divide(X0,X1),double_divide(inverse(X2),inverse(multiply(X1,X0)))),double_divide(double_divide(X3,X2),inverse(inverse(identity)))),inverse(identity))=X3)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f8,f87])).
% 0.13/0.45 fof(f107,plain,(
% 0.13/0.45 ![X0,X1,X2,X3]: (inverse(X0)=double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),inverse(X3))),double_divide(double_divide(X0,X2),inverse(inverse(identity)))))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f91,f92])).
% 0.13/0.45 fof(f112,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(X1,double_divide(inverse(X0),inverse(inverse(X1)))))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f91,f93])).
% 0.13/0.45 fof(f114,plain,(
% 0.13/0.45 ![X0]: (double_divide(double_divide(inverse(inverse(identity)),double_divide(X0,inverse(inverse(identity)))),inverse(identity))=inverse(X0))),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f117,f91])).
% 0.13/0.45 fof(f115,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(inverse(X1),double_divide(double_divide(X0,X1),inverse(inverse(identity)))))),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f117,f107])).
% 0.13/0.45 fof(f117,plain,(
% 0.13/0.45 ![X0,X1,X2]: (inverse(X0)=double_divide(X1,double_divide(double_divide(X0,double_divide(X1,X2)),inverse(X2))))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f91,f94])).
% 0.13/0.45 fof(f118,plain,(
% 0.13/0.45 ![X0,X1]: (double_divide(double_divide(inverse(multiply(X0,X1)),double_divide(identity,inverse(inverse(identity)))),inverse(identity))=double_divide(X1,X0))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f117,f95])).
% 0.13/0.45 fof(f119,plain,(
% 0.13/0.45 ![X0]: (double_divide(double_divide(inverse(inverse(X0)),double_divide(identity,inverse(inverse(identity)))),inverse(identity))=X0)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f117,f96])).
% 0.13/0.45 fof(f130,plain,(
% 0.13/0.45 ![X0]: (double_divide(double_divide(identity,double_divide(X0,inverse(identity))),inverse(identity))=inverse(X0))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f67,f51])).
% 0.13/0.45 fof(f131,plain,(
% 0.13/0.45 ![X0,X1]: (double_divide(double_divide(identity,double_divide(X0,inverse(identity))),inverse(identity))=double_divide(X1,double_divide(double_divide(X0,inverse(X1)),inverse(identity))))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f51,f51])).
% 0.13/0.45 fof(f133,plain,(
% 0.13/0.45 ![X0,X1,X2]: (double_divide(double_divide(double_divide(X0,X1),double_divide(double_divide(X2,multiply(X1,X0)),inverse(identity))),inverse(identity))=X2)),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f17,f51])).
% 0.13/0.45 fof(f139,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(X1,double_divide(double_divide(X0,inverse(X1)),inverse(identity))))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f130,f131])).
% 0.13/0.45 fof(f250,plain,(
% 0.13/0.45 ![X0,X1,X2,X3,X4]: (double_divide(double_divide(double_divide(double_divide(X0,X1),double_divide(multiply(X2,X3),inverse(multiply(X1,X0)))),double_divide(double_divide(X4,double_divide(X3,X2)),inverse(inverse(identity)))),inverse(identity))=X4)),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f17,f102])).
% 0.13/0.45 fof(f255,plain,(
% 0.13/0.45 ![X0,X1,X2]: (double_divide(double_divide(double_divide(double_divide(X0,X1),double_divide(inverse(inverse(identity)),inverse(multiply(X1,X0)))),double_divide(X2,inverse(inverse(identity)))),inverse(identity))=inverse(X2))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f67,f102])).
% 0.13/0.45 fof(f258,plain,(
% 0.13/0.45 ![X0,X1,X2,X3,X4]: (double_divide(double_divide(double_divide(double_divide(X0,X1),double_divide(inverse(inverse(identity)),inverse(multiply(X1,X0)))),double_divide(double_divide(X2,X3),inverse(inverse(identity)))),inverse(identity))=double_divide(X4,double_divide(multiply(X3,X2),inverse(inverse(X4)))))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f61,f102])).
% 0.13/0.45 fof(f307,plain,(
% 0.13/0.45 ![X0,X1,X2]: (inverse(double_divide(X0,X1))=double_divide(X2,double_divide(multiply(X1,X0),inverse(inverse(X2)))))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f255,f258])).
% 0.13/0.45 fof(f310,plain,(
% 0.13/0.45 ![X0,X1,X2]: (multiply(X0,X1)=double_divide(X2,double_divide(multiply(X0,X1),inverse(inverse(X2)))))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f17,f307])).
% 0.13/0.45 fof(f345,plain,(
% 0.13/0.45 ![X0,X1]: (double_divide(double_divide(inverse(inverse(identity)),double_divide(identity,inverse(inverse(identity)))),inverse(identity))=double_divide(double_divide(X0,X1),multiply(X1,X0)))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f26,f118])).
% 0.13/0.45 fof(f346,plain,(
% 0.13/0.45 ![X0,X1]: (double_divide(double_divide(inverse(multiply(X0,X1)),double_divide(identity,inverse(inverse(identity)))),inverse(identity))=double_divide(multiply(X0,X1),inverse(identity)))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f80,f118])).
% 0.13/0.45 fof(f347,plain,(
% 0.13/0.45 ![X0]: (double_divide(double_divide(inverse(inverse(X0)),double_divide(identity,inverse(inverse(identity)))),inverse(identity))=double_divide(inverse(X0),inverse(identity)))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f74,f118])).
% 0.13/0.45 fof(f353,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(identity)=double_divide(double_divide(X0,X1),multiply(X1,X0)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f114,f345])).
% 0.13/0.45 fof(f360,plain,(
% 0.13/0.45 ![X0,X1,X2,X3,X4]: (double_divide(double_divide(double_divide(double_divide(X0,X1),double_divide(multiply(X2,X3),inverse(multiply(X1,X0)))),double_divide(double_divide(X4,double_divide(X3,X2)),inverse(inverse(identity)))),identity)=X4)),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f370,f250])).
% 0.13/0.45 fof(f362,plain,(
% 0.13/0.45 ![X0,X1,X2]: (double_divide(double_divide(double_divide(X0,X1),double_divide(double_divide(X2,multiply(X1,X0)),inverse(identity))),identity)=X2)),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f370,f133])).
% 0.13/0.45 fof(f363,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(X1,double_divide(double_divide(X0,inverse(X1)),identity)))),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f370,f139])).
% 0.13/0.45 fof(f365,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(inverse(X1),double_divide(double_divide(X0,X1),inverse(identity))))),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f370,f115])).
% 0.13/0.45 fof(f370,plain,(
% 0.13/0.45 inverse(identity)=identity),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f20,f353])).
% 0.13/0.45 fof(f371,plain,(
% 0.13/0.45 ![X0,X1]: (double_divide(X0,X1)=double_divide(multiply(X1,X0),inverse(identity)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f118,f346])).
% 0.13/0.45 fof(f372,plain,(
% 0.13/0.45 ![X0,X1]: (double_divide(X0,X1)=double_divide(multiply(X1,X0),identity))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f370,f371])).
% 0.13/0.45 fof(f374,plain,(
% 0.13/0.45 ![X0,X1]: (double_divide(X0,X1)=inverse(multiply(X1,X0)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f8,f372])).
% 0.13/0.45 fof(f375,plain,(
% 0.13/0.45 ![X0]: (X0=double_divide(inverse(X0),inverse(identity)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f119,f347])).
% 0.13/0.45 fof(f376,plain,(
% 0.13/0.45 ![X0]: (X0=double_divide(inverse(X0),identity))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f370,f375])).
% 0.13/0.45 fof(f378,plain,(
% 0.13/0.45 ![X0,X1,X2]: (multiply(X0,X1)=double_divide(X2,double_divide(multiply(X0,X1),X2)))),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f380,f310])).
% 0.13/0.45 fof(f379,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(X1,double_divide(inverse(X0),X1)))),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f380,f112])).
% 0.13/0.45 fof(f380,plain,(
% 0.13/0.45 ![X0]: (X0=inverse(inverse(X0)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f8,f376])).
% 0.13/0.45 fof(f415,plain,(
% 0.13/0.45 ![X0,X1,X2,X3,X4]: (inverse(double_divide(double_divide(double_divide(X0,X1),double_divide(multiply(X2,X3),inverse(multiply(X1,X0)))),double_divide(double_divide(X4,double_divide(X3,X2)),inverse(inverse(identity)))))=X4)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f8,f360])).
% 0.13/0.45 fof(f416,plain,(
% 0.13/0.45 ![X0,X1,X2,X3,X4]: (multiply(double_divide(double_divide(X0,double_divide(X1,X2)),inverse(inverse(identity))),double_divide(double_divide(X3,X4),double_divide(multiply(X2,X1),inverse(multiply(X4,X3)))))=X0)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f17,f415])).
% 0.13/0.45 fof(f417,plain,(
% 0.13/0.45 ![X0,X1,X2,X3,X4]: (multiply(double_divide(double_divide(X0,double_divide(X1,X2)),identity),double_divide(double_divide(X3,X4),double_divide(multiply(X2,X1),inverse(multiply(X4,X3)))))=X0)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f380,f416])).
% 0.13/0.45 fof(f418,plain,(
% 0.13/0.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(double_divide(X0,double_divide(X1,X2))),double_divide(double_divide(X3,X4),double_divide(multiply(X2,X1),inverse(multiply(X4,X3)))))=X0)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f8,f417])).
% 0.13/0.45 fof(f419,plain,(
% 0.13/0.45 ![X0,X1,X2,X3,X4]: (multiply(multiply(double_divide(X0,X1),X2),double_divide(double_divide(X3,X4),double_divide(multiply(X1,X0),inverse(multiply(X4,X3)))))=X2)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f17,f418])).
% 0.13/0.45 fof(f420,plain,(
% 0.13/0.45 ![X0,X1,X2,X3,X4]: (multiply(multiply(double_divide(X0,X1),X2),double_divide(double_divide(X3,X4),double_divide(multiply(X1,X0),double_divide(X3,X4))))=X2)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f374,f419])).
% 0.13/0.45 fof(f424,plain,(
% 0.13/0.45 ![X0,X1,X2]: (inverse(double_divide(double_divide(X0,X1),double_divide(double_divide(X2,multiply(X1,X0)),inverse(identity))))=X2)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f8,f362])).
% 0.13/0.45 fof(f425,plain,(
% 0.13/0.45 ![X0,X1,X2]: (multiply(double_divide(double_divide(X0,multiply(X1,X2)),inverse(identity)),double_divide(X2,X1))=X0)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f17,f424])).
% 0.13/0.45 fof(f426,plain,(
% 0.13/0.45 ![X0,X1,X2]: (multiply(double_divide(double_divide(X0,multiply(X1,X2)),identity),double_divide(X2,X1))=X0)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f370,f425])).
% 0.13/0.45 fof(f427,plain,(
% 0.13/0.45 ![X0,X1,X2]: (multiply(inverse(double_divide(X0,multiply(X1,X2))),double_divide(X2,X1))=X0)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f8,f426])).
% 0.13/0.45 fof(f428,plain,(
% 0.13/0.45 ![X0,X1,X2]: (multiply(multiply(multiply(X0,X1),X2),double_divide(X1,X0))=X2)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f17,f427])).
% 0.13/0.45 fof(f429,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(X1,inverse(double_divide(X0,inverse(X1)))))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f8,f363])).
% 0.13/0.45 fof(f430,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(X1,multiply(inverse(X1),X0)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f17,f429])).
% 0.13/0.45 fof(f435,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(inverse(X1),double_divide(double_divide(X0,X1),identity)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f370,f365])).
% 0.13/0.45 fof(f436,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(inverse(X1),inverse(double_divide(X0,X1))))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f8,f435])).
% 0.13/0.45 fof(f437,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(inverse(X1),multiply(X1,X0)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f17,f436])).
% 0.13/0.45 fof(f456,plain,(
% 0.13/0.45 ![X0,X1,X2]: (multiply(multiply(double_divide(X0,X1),X2),multiply(X1,X0))=X2)),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f378,f420])).
% 0.13/0.45 fof(f482,plain,(
% 0.13/0.45 ![X0,X1,X2]: (multiply(X0,double_divide(X0,multiply(X1,X2)))=double_divide(X2,X1))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f428,f428])).
% 0.13/0.45 fof(f509,plain,(
% 0.13/0.45 ![X0,X1]: (multiply(multiply(inverse(X0),X1),X0)=inverse(inverse(X1)))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f430,f17])).
% 0.13/0.45 fof(f517,plain,(
% 0.13/0.45 ![X0,X1]: (multiply(multiply(inverse(X0),X1),X0)=X1)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f380,f509])).
% 0.13/0.45 fof(f579,plain,(
% 0.13/0.45 ![X0,X1,X2]: (inverse(X0)=double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(inverse(X1),inverse(inverse(X2)))))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f117,f117])).
% 0.13/0.45 fof(f596,plain,(
% 0.13/0.45 ![X0,X1,X2]: (inverse(X0)=double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(inverse(X1),X2)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f380,f579])).
% 0.13/0.45 fof(f622,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(inverse(X0))=double_divide(X1,double_divide(X0,X1)))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f380,f379])).
% 0.13/0.45 fof(f625,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(inverse(X1),double_divide(inverse(X1),inverse(X0))))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f379,f117])).
% 0.13/0.45 fof(f636,plain,(
% 0.13/0.45 ![X0,X1]: (X0=double_divide(X1,double_divide(X0,X1)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f380,f622])).
% 0.13/0.45 fof(f904,plain,(
% 0.13/0.45 ![X0,X1]: (multiply(inverse(X0),inverse(X1))=double_divide(X1,X0))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f437,f482])).
% 0.13/0.45 fof(f907,plain,(
% 0.13/0.45 ![X0,X1]: (multiply(X0,inverse(X1))=double_divide(X1,inverse(X0)))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f430,f482])).
% 0.13/0.45 fof(f916,plain,(
% 0.13/0.45 ![X0,X1,X2,X3]: (multiply(double_divide(X0,X1),multiply(X2,X3))=double_divide(double_divide(X3,X2),multiply(X1,X0)))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f482,f456])).
% 0.13/0.45 fof(f934,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(inverse(X1),multiply(X0,inverse(inverse(X1)))))),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f907,f625])).
% 0.13/0.45 fof(f981,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=double_divide(inverse(X1),multiply(X0,X1)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f380,f934])).
% 0.13/0.45 fof(f1049,plain,(
% 0.13/0.45 ![X0,X1]: (X0=double_divide(double_divide(X1,X0),X1))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f636,f636])).
% 0.13/0.45 fof(f1086,plain,(
% 0.13/0.45 ![X0,X1]: (multiply(inverse(X0),X1)=double_divide(inverse(X1),X0))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f430,f1049])).
% 0.13/0.45 fof(f1103,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=multiply(inverse(multiply(X0,X1)),X1))),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f1086,f981])).
% 0.13/0.45 fof(f1108,plain,(
% 0.13/0.45 ![X0,X1,X2]: (inverse(X0)=double_divide(double_divide(X1,double_divide(X0,X2)),multiply(inverse(X2),X1)))),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f1086,f596])).
% 0.13/0.45 fof(f1125,plain,(
% 0.13/0.45 ![X0,X1]: (inverse(X0)=multiply(double_divide(X1,X0),X1))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f374,f1103])).
% 0.13/0.45 fof(f1127,plain,(
% 0.13/0.45 ![X0,X1,X2]: (inverse(X0)=multiply(double_divide(X1,inverse(X2)),multiply(double_divide(X0,X2),X1)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f916,f1108])).
% 0.13/0.46 fof(f1128,plain,(
% 0.13/0.46 ![X0,X1,X2]: (inverse(X0)=multiply(multiply(X1,inverse(X2)),multiply(double_divide(X0,X1),X2)))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f907,f1127])).
% 0.13/0.46 fof(f1391,plain,(
% 0.13/0.46 ![X0,X1]: (inverse(double_divide(X0,X1))=multiply(X0,X1))),
% 0.13/0.46 inference(paramodulation,[status(thm)],[f636,f1125])).
% 0.13/0.46 fof(f1395,plain,(
% 0.13/0.46 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=X1)),
% 0.13/0.46 inference(paramodulation,[status(thm)],[f1125,f456])).
% 0.13/0.46 fof(f1497,plain,(
% 0.13/0.46 ![X0,X1,X2]: (inverse(X0)=multiply(X1,multiply(double_divide(X0,multiply(inverse(inverse(X2)),X1)),X2)))),
% 0.13/0.46 inference(paramodulation,[status(thm)],[f517,f1128])).
% 0.13/0.46 fof(f1525,plain,(
% 0.13/0.46 ![X0,X1,X2]: (inverse(X0)=multiply(X1,multiply(double_divide(X0,multiply(X2,X1)),X2)))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f380,f1497])).
% 0.13/0.46 fof(f1904,plain,(
% 0.13/0.46 ![X0,X1,X2]: (multiply(inverse(X0),multiply(X1,X2))=double_divide(double_divide(X2,X1),X0))),
% 0.13/0.46 inference(paramodulation,[status(thm)],[f17,f904])).
% 0.13/0.46 fof(f1926,plain,(
% 0.13/0.46 ![X0,X1]: (double_divide(double_divide(X0,X1),X1)=X0)),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f1904,f1395])).
% 0.13/0.46 fof(f2877,plain,(
% 0.13/0.46 ![X0,X1,X2]: (inverse(double_divide(X0,multiply(X1,X2)))=multiply(X2,multiply(X0,X1)))),
% 0.13/0.46 inference(paramodulation,[status(thm)],[f1926,f1525])).
% 0.13/0.46 fof(f2878,plain,(
% 0.13/0.46 ![X0,X1,X2]: (inverse(double_divide(multiply(X0,X1),X2))=multiply(X1,multiply(X2,X0)))),
% 0.13/0.46 inference(paramodulation,[status(thm)],[f1049,f1525])).
% 0.13/0.46 fof(f2923,plain,(
% 0.13/0.46 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(X2,multiply(X0,X1)))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1391,f2877])).
% 0.13/0.46 fof(f2927,plain,(
% 0.13/0.46 ~multiply(b3,multiply(c3,a3))=multiply(a3,multiply(b3,c3))),
% 0.13/0.46 inference(backward_demodulation,[status(thm)],[f2984,f10])).
% 0.13/0.46 fof(f2984,plain,(
% 0.13/0.46 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X1,multiply(X2,X0)))),
% 0.13/0.46 inference(forward_demodulation,[status(thm)],[f1391,f2878])).
% 0.13/0.46 fof(f3069,plain,(
% 0.13/0.46 $false),
% 0.13/0.46 inference(forward_subsumption_resolution,[status(thm)],[f2927,f2923])).
% 0.13/0.46 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.47 % Elapsed time: 0.111438 seconds
% 0.13/0.47 % CPU time: 0.747043 seconds
% 0.13/0.47 % Total memory used: 27.769 MB
% 0.13/0.47 % Net memory used: 26.358 MB
%------------------------------------------------------------------------------