%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP579-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 : n004.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:51 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP579-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.09/0.35 % Computer : n004.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 20:17:06 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.47 % Refutation found
% 0.12/0.47 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.47 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.47 fof(f1,axiom,(
% 0.12/0.47 (![A,B,C]: (double_divide(double_divide(A,double_divide(double_divide(double_divide(B,A),C),double_divide(B,identity))),double_divide(identity,identity)) = C ))),
% 0.12/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.47 fof(f2,axiom,(
% 0.12/0.47 (![A,B]: (multiply(A,B) = double_divide(double_divide(B,A),identity) ))),
% 0.12/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.47 fof(f3,axiom,(
% 0.12/0.47 (![A]: (inverse(A) = double_divide(A,identity) ))),
% 0.12/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.47 fof(f4,axiom,(
% 0.12/0.47 (![A]: (identity = double_divide(A,inverse(A)) ))),
% 0.12/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.47 fof(f5,negated_conjecture,(
% 0.12/0.47 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 0.12/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.47 fof(f6,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),double_divide(X1,identity))),double_divide(identity,identity))=X2)),
% 0.12/0.47 inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.47 fof(f7,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(X0,X1)=double_divide(double_divide(X1,X0),identity))),
% 0.12/0.47 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.47 fof(f8,plain,(
% 0.12/0.47 ![X0]: (inverse(X0)=double_divide(X0,identity))),
% 0.12/0.47 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.47 fof(f9,plain,(
% 0.12/0.47 ![X0]: (identity=double_divide(X0,inverse(X0)))),
% 0.12/0.47 inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.47 fof(f10,plain,(
% 0.12/0.47 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 0.12/0.47 inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.47 fof(f16,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),double_divide(X1,identity))),inverse(identity))=X2)),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f8,f6])).
% 0.12/0.47 fof(f17,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f8,f7])).
% 0.12/0.47 fof(f18,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),inverse(X1))),inverse(identity))=X2)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f16])).
% 0.12/0.47 fof(f19,plain,(
% 0.12/0.47 ![X0]: (multiply(identity,X0)=inverse(inverse(X0)))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f8,f17])).
% 0.12/0.47 fof(f20,plain,(
% 0.12/0.47 ![X0,X1]: (identity=double_divide(double_divide(X0,X1),multiply(X1,X0)))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f17,f9])).
% 0.12/0.47 fof(f21,plain,(
% 0.12/0.47 ![X0]: (multiply(inverse(X0),X0)=inverse(identity))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f9,f17])).
% 0.12/0.47 fof(f48,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),inverse(identity))=double_divide(double_divide(double_divide(X2,double_divide(identity,X0)),X1),inverse(X2)))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f18,f18])).
% 0.12/0.47 fof(f50,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(double_divide(X0,double_divide(identity,inverse(X1))),inverse(identity))=multiply(X0,X1))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f20,f18])).
% 0.12/0.47 fof(f52,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(double_divide(X0,double_divide(inverse(double_divide(X1,X0)),inverse(X1))),inverse(identity))=identity)),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f8,f18])).
% 0.12/0.47 fof(f53,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(X0,X1),inverse(double_divide(X2,double_divide(double_divide(double_divide(X3,X2),X0),inverse(X3)))))),inverse(identity))=X1)),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f18,f18])).
% 0.12/0.47 fof(f57,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,double_divide(double_divide(double_divide(double_divide(X1,X2),X0),X3),multiply(X2,X1))),inverse(identity))=X3)),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f17,f18])).
% 0.12/0.47 fof(f60,plain,(
% 0.12/0.47 ![X0,X1,X2]: (multiply(inverse(identity),double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),inverse(X1))))=inverse(X2))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f18,f17])).
% 0.12/0.47 fof(f62,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(double_divide(X0,double_divide(multiply(X0,X1),inverse(X1))),inverse(identity))=identity)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f17,f52])).
% 0.12/0.47 fof(f63,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(double_divide(X2,X3),X0),inverse(X2)),X3))),inverse(identity))=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f17,f53])).
% 0.12/0.47 fof(f67,plain,(
% 0.12/0.47 ![X0]: (double_divide(double_divide(X0,identity),inverse(identity))=multiply(X0,identity))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f9,f50])).
% 0.12/0.47 fof(f69,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(double_divide(X0,multiply(double_divide(identity,X0),X1)),inverse(identity))=double_divide(identity,inverse(X1)))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f50,f18])).
% 0.12/0.47 fof(f74,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(inverse(identity),double_divide(X0,double_divide(identity,inverse(X1))))=inverse(multiply(X0,X1)))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f50,f17])).
% 0.12/0.47 fof(f75,plain,(
% 0.12/0.47 ![X0]: (double_divide(inverse(X0),inverse(identity))=multiply(X0,identity))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f67])).
% 0.12/0.47 fof(f79,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(multiply(X0,X1),inverse(identity))=multiply(double_divide(X1,X0),identity))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f17,f75])).
% 0.12/0.47 fof(f116,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(double_divide(double_divide(multiply(X0,X1),inverse(X1)),double_divide(identity,inverse(X0))),inverse(identity))=inverse(identity))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f62,f18])).
% 0.12/0.47 fof(f125,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(double_divide(multiply(X0,X1),inverse(X1)),X0)=inverse(identity))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f50,f116])).
% 0.12/0.47 fof(f130,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(double_divide(inverse(identity),identity),inverse(identity))=double_divide(double_divide(double_divide(X0,X1),X1),inverse(X0)))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f20,f63])).
% 0.12/0.47 fof(f157,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(identity,X0),inverse(X2)),inverse(X2)))),inverse(identity))=X1)),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f9,f63])).
% 0.12/0.47 fof(f158,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(inverse(X2),X0),inverse(X2)),identity))),inverse(identity))=X1)),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f8,f63])).
% 0.12/0.47 fof(f164,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (multiply(inverse(identity),double_divide(inverse(identity),double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(double_divide(X2,X3),X0),inverse(X2)),X3))))=inverse(X1))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f63,f17])).
% 0.12/0.47 fof(f165,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(inverse(inverse(identity)),inverse(identity))=double_divide(double_divide(double_divide(X0,X1),X1),inverse(X0)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f130])).
% 0.12/0.47 fof(f166,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(inverse(identity),identity)=double_divide(double_divide(double_divide(X0,X1),X1),inverse(X0)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f75,f165])).
% 0.12/0.47 fof(f167,plain,(
% 0.12/0.47 ![X0,X1]: (inverse(identity)=double_divide(double_divide(double_divide(X0,X1),X1),inverse(X0)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f21,f166])).
% 0.12/0.47 fof(f211,plain,(
% 0.12/0.47 ![X0,X1]: (inverse(identity)=double_divide(double_divide(identity,inverse(identity)),inverse(double_divide(X0,double_divide(multiply(X0,X1),inverse(X1))))))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f62,f167])).
% 0.12/0.47 fof(f219,plain,(
% 0.12/0.47 ![X0]: (double_divide(double_divide(X0,inverse(identity)),inverse(identity))=X0)),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f167,f18])).
% 0.12/0.47 fof(f222,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(double_divide(X0,double_divide(inverse(identity),inverse(double_divide(X1,X0)))),inverse(identity))=inverse(X1))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f167,f18])).
% 0.12/0.47 fof(f225,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(inverse(identity),X1),inverse(double_divide(double_divide(X0,X2),X2)))),inverse(identity))=X1)),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f167,f18])).
% 0.12/0.47 fof(f244,plain,(
% 0.12/0.47 ![X0,X1]: (inverse(identity)=double_divide(identity,inverse(double_divide(X0,double_divide(multiply(X0,X1),inverse(X1))))))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f9,f211])).
% 0.12/0.47 fof(f245,plain,(
% 0.12/0.47 ![X0,X1]: (inverse(identity)=double_divide(identity,multiply(double_divide(multiply(X0,X1),inverse(X1)),X0)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f17,f244])).
% 0.12/0.47 fof(f246,plain,(
% 0.12/0.47 inverse(identity)=double_divide(identity,inverse(identity))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f125,f245])).
% 0.12/0.47 fof(f251,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(multiply(X0,X1),identity)=multiply(double_divide(X1,X0),identity))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f312,f79])).
% 0.12/0.47 fof(f253,plain,(
% 0.12/0.47 ![X0]: (double_divide(inverse(X0),identity)=multiply(X0,identity))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f312,f75])).
% 0.12/0.47 fof(f254,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(double_divide(X0,double_divide(identity,inverse(X1))),identity)=multiply(X0,X1))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f312,f50])).
% 0.12/0.47 fof(f255,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),inverse(X1))),identity)=X2)),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f312,f18])).
% 0.12/0.47 fof(f272,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (multiply(inverse(identity),double_divide(identity,double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(double_divide(X2,X3),X0),inverse(X2)),X3))))=inverse(X1))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f312,f164])).
% 0.12/0.47 fof(f274,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(inverse(X2),X0),inverse(X2)),identity))),identity)=X1)),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f312,f158])).
% 0.12/0.47 fof(f275,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(identity,X0),inverse(X2)),inverse(X2)))),identity)=X1)),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f312,f157])).
% 0.12/0.47 fof(f300,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(identity,double_divide(X0,double_divide(identity,inverse(X1))))=inverse(multiply(X0,X1)))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f312,f74])).
% 0.12/0.47 fof(f303,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(double_divide(X0,multiply(double_divide(identity,X0),X1)),identity)=double_divide(identity,inverse(X1)))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f312,f69])).
% 0.12/0.47 fof(f305,plain,(
% 0.12/0.47 ![X0,X1,X2]: (multiply(identity,double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),inverse(X1))))=inverse(X2))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f312,f60])).
% 0.12/0.47 fof(f306,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,double_divide(double_divide(double_divide(double_divide(X1,X2),X0),X3),multiply(X2,X1))),identity)=X3)),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f312,f57])).
% 0.12/0.47 fof(f311,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),identity)=double_divide(double_divide(double_divide(X2,double_divide(identity,X0)),X1),inverse(X2)))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f312,f48])).
% 0.12/0.47 fof(f312,plain,(
% 0.12/0.47 inverse(identity)=identity),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f9,f246])).
% 0.12/0.47 fof(f332,plain,(
% 0.12/0.47 ![X0]: (double_divide(double_divide(X0,identity),inverse(identity))=X0)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f312,f219])).
% 0.12/0.47 fof(f333,plain,(
% 0.12/0.47 ![X0]: (double_divide(inverse(X0),inverse(identity))=X0)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f332])).
% 0.12/0.47 fof(f334,plain,(
% 0.12/0.47 ![X0]: (double_divide(inverse(X0),identity)=X0)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f312,f333])).
% 0.12/0.47 fof(f338,plain,(
% 0.12/0.47 ![X0]: (inverse(inverse(X0))=X0)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f334])).
% 0.12/0.47 fof(f346,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(double_divide(X0,double_divide(identity,inverse(double_divide(X1,X0)))),inverse(identity))=inverse(X1))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f312,f222])).
% 0.12/0.47 fof(f347,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(X0,double_divide(X1,X0))=inverse(X1))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f50,f346])).
% 0.12/0.47 fof(f360,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X1),inverse(double_divide(double_divide(X0,X2),X2)))),inverse(identity))=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f312,f225])).
% 0.12/0.47 fof(f361,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X1),multiply(X2,double_divide(X0,X2)))),inverse(identity))=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f17,f360])).
% 0.12/0.47 fof(f362,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X1),inverse(X0))),inverse(identity))=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f347,f361])).
% 0.12/0.47 fof(f363,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X1),inverse(X0))),identity)=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f312,f362])).
% 0.12/0.47 fof(f364,plain,(
% 0.12/0.47 ![X0,X1]: (inverse(double_divide(inverse(X0),double_divide(double_divide(identity,X1),inverse(X0))))=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f363])).
% 0.12/0.47 fof(f366,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(double_divide(double_divide(identity,X0),inverse(X1)),inverse(X1))=X0)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f17,f364])).
% 0.12/0.47 fof(f400,plain,(
% 0.12/0.47 ![X0,X1]: (inverse(multiply(X0,X1))=multiply(double_divide(X1,X0),identity))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f251])).
% 0.12/0.47 fof(f403,plain,(
% 0.12/0.47 ![X0]: (inverse(inverse(X0))=multiply(X0,identity))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f253])).
% 0.12/0.47 fof(f405,plain,(
% 0.12/0.47 ![X0,X1]: (inverse(multiply(X0,X1))=double_divide(X1,X0))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f408,f400])).
% 0.12/0.47 fof(f408,plain,(
% 0.12/0.47 ![X0]: (X0=multiply(X0,identity))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f338,f403])).
% 0.12/0.47 fof(f409,plain,(
% 0.12/0.47 ![X0,X1]: (inverse(double_divide(X0,double_divide(identity,inverse(X1))))=multiply(X0,X1))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f254])).
% 0.12/0.47 fof(f410,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(double_divide(identity,inverse(X0)),X1)=multiply(X1,X0))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f17,f409])).
% 0.12/0.47 fof(f411,plain,(
% 0.12/0.47 ![X0,X1,X2]: (inverse(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),inverse(X1))))=X2)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f255])).
% 0.12/0.47 fof(f414,plain,(
% 0.12/0.47 ![X0,X1,X2]: (multiply(double_divide(double_divide(double_divide(X0,X1),X2),inverse(X0)),X1)=X2)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f17,f411])).
% 0.12/0.47 fof(f441,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (multiply(identity,double_divide(identity,double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(double_divide(X2,X3),X0),inverse(X2)),X3))))=inverse(X1))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f312,f272])).
% 0.12/0.47 fof(f442,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (inverse(inverse(double_divide(identity,double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(double_divide(X2,X3),X0),inverse(X2)),X3)))))=inverse(X1))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f19,f441])).
% 0.12/0.47 fof(f443,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (double_divide(identity,double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(double_divide(X2,X3),X0),inverse(X2)),X3)))=inverse(X1))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f338,f442])).
% 0.12/0.47 fof(f444,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(identity,double_divide(double_divide(X0,X1),X0))=inverse(X1))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f414,f443])).
% 0.12/0.47 fof(f449,plain,(
% 0.12/0.47 ![X0,X1,X2]: (inverse(double_divide(inverse(identity),double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(inverse(X2),X0),inverse(X2)),identity))))=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f274])).
% 0.12/0.47 fof(f450,plain,(
% 0.12/0.47 ![X0,X1,X2]: (multiply(double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(inverse(X2),X0),inverse(X2)),identity)),inverse(identity))=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f17,f449])).
% 0.12/0.47 fof(f451,plain,(
% 0.12/0.47 ![X0,X1,X2]: (multiply(double_divide(double_divide(X0,X1),inverse(multiply(inverse(X2),double_divide(inverse(X2),X0)))),inverse(identity))=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f400,f450])).
% 0.12/0.47 fof(f452,plain,(
% 0.12/0.47 ![X0,X1,X2]: (multiply(double_divide(double_divide(X0,X1),inverse(multiply(inverse(X2),double_divide(inverse(X2),X0)))),identity)=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f312,f451])).
% 0.12/0.47 fof(f453,plain,(
% 0.12/0.47 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(inverse(X0),double_divide(inverse(X0),X1))),double_divide(X1,X2)))=X2)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f400,f452])).
% 0.12/0.47 fof(f454,plain,(
% 0.12/0.47 ![X0,X1,X2]: (inverse(double_divide(inverse(identity),double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(identity,X0),inverse(X2)),inverse(X2)))))=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f275])).
% 0.12/0.47 fof(f455,plain,(
% 0.12/0.47 ![X0,X1,X2]: (multiply(double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(identity,X0),inverse(X2)),inverse(X2))),inverse(identity))=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f17,f454])).
% 0.12/0.47 fof(f456,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(double_divide(double_divide(X0,X1),X0),inverse(identity))=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f366,f455])).
% 0.12/0.47 fof(f457,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(double_divide(double_divide(X0,X1),X0),identity)=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f312,f456])).
% 0.12/0.47 fof(f458,plain,(
% 0.12/0.47 ![X0,X1]: (inverse(multiply(X0,double_divide(X0,X1)))=X1)),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f459,f453])).
% 0.12/0.47 fof(f459,plain,(
% 0.12/0.47 ![X0,X1]: (inverse(multiply(X0,double_divide(X0,X1)))=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f400,f457])).
% 0.12/0.47 fof(f598,plain,(
% 0.12/0.47 ![X0,X1]: (inverse(inverse(double_divide(X0,double_divide(identity,inverse(X1)))))=inverse(multiply(X0,X1)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f19,f300])).
% 0.12/0.47 fof(f601,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(X0,double_divide(identity,inverse(X1)))=inverse(multiply(X0,X1)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f338,f598])).
% 0.12/0.47 fof(f611,plain,(
% 0.12/0.47 ![X0,X1]: (inverse(double_divide(X0,multiply(double_divide(identity,X0),X1)))=double_divide(identity,inverse(X1)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f303])).
% 0.12/0.47 fof(f613,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(multiply(double_divide(identity,X0),X1),X0)=double_divide(identity,inverse(X1)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f17,f611])).
% 0.12/0.47 fof(f617,plain,(
% 0.12/0.47 ![X0,X1,X2]: (inverse(inverse(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),inverse(X1)))))=inverse(X2))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f19,f305])).
% 0.12/0.47 fof(f620,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),inverse(X1)))=inverse(X2))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f338,f617])).
% 0.12/0.47 fof(f621,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (inverse(double_divide(X0,double_divide(double_divide(double_divide(double_divide(X1,X2),X0),X3),multiply(X2,X1))))=X3)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f306])).
% 0.12/0.47 fof(f623,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (multiply(double_divide(double_divide(double_divide(double_divide(X0,X1),X2),X3),multiply(X1,X0)),X2)=X3)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f17,f621])).
% 0.12/0.47 fof(f636,plain,(
% 0.12/0.47 ![X0,X1,X2]: (inverse(double_divide(X0,X1))=double_divide(double_divide(double_divide(X2,double_divide(identity,X0)),X1),inverse(X2)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f8,f311])).
% 0.12/0.47 fof(f637,plain,(
% 0.12/0.47 ![X0,X1,X2]: (multiply(X0,X1)=double_divide(double_divide(double_divide(X2,double_divide(identity,X1)),X0),inverse(X2)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f17,f636])).
% 0.12/0.47 fof(f648,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(X0,double_divide(identity,inverse(X1)))=double_divide(X1,X0))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f405,f601])).
% 0.12/0.47 fof(f650,plain,(
% 0.12/0.47 ![X0]: (double_divide(identity,X0)=inverse(X0))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f651,f444])).
% 0.12/0.47 fof(f651,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(double_divide(X0,X1),X0)=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f405,f458])).
% 0.12/0.47 fof(f659,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(X0,inverse(inverse(X1)))=double_divide(X1,X0))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f650,f648])).
% 0.12/0.47 fof(f660,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(multiply(double_divide(identity,X0),X1),X0)=inverse(inverse(X1)))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f650,f613])).
% 0.12/0.47 fof(f662,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=multiply(X1,X0))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f650,f410])).
% 0.12/0.47 fof(f667,plain,(
% 0.12/0.47 ![X0,X1,X2]: (multiply(X0,X1)=double_divide(double_divide(double_divide(X2,inverse(X1)),X0),inverse(X2)))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f650,f637])).
% 0.12/0.47 fof(f670,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(X0,X1)=double_divide(X1,X0))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f338,f659])).
% 0.12/0.47 fof(f671,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(multiply(inverse(X0),X1),X0)=inverse(inverse(X1)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f650,f660])).
% 0.12/0.47 fof(f672,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(multiply(inverse(X0),X1),X0)=X1)),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f338,f671])).
% 0.12/0.47 fof(f674,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f338,f662])).
% 0.12/0.47 fof(f714,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(X0,double_divide(X0,X1))=inverse(X1))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f651,f17])).
% 0.12/0.47 fof(f733,plain,(
% 0.12/0.47 ![X0,X1]: (X0=double_divide(X1,double_divide(X1,X0)))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f651,f670])).
% 0.12/0.47 fof(f751,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X0,X1)))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f670,f17])).
% 0.12/0.47 fof(f775,plain,(
% 0.12/0.47 ~multiply(multiply(b3,a3),c3)=multiply(a3,multiply(b3,c3))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f674,f10])).
% 0.12/0.47 fof(f837,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(X0,double_divide(identity,inverse(X1)))=inverse(multiply(X0,X1)))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f20,f620])).
% 0.12/0.47 fof(f839,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (double_divide(X0,double_divide(inverse(X1),inverse(X2)))=inverse(double_divide(double_divide(double_divide(X3,double_divide(X2,X0)),X1),inverse(X3))))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f620,f620])).
% 0.12/0.47 fof(f859,plain,(
% 0.12/0.47 ![X0,X1,X2]: (double_divide(inverse(X0),X1)=double_divide(double_divide(double_divide(X2,X1),X0),inverse(X2)))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f620,f651])).
% 0.12/0.47 fof(f864,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(X0,inverse(inverse(X1)))=inverse(multiply(X0,X1)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f650,f837])).
% 0.12/0.47 fof(f865,plain,(
% 0.12/0.47 ![X0,X1]: (double_divide(X0,X1)=inverse(multiply(X0,X1)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f338,f864])).
% 0.12/0.47 fof(f866,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (double_divide(X0,double_divide(inverse(X1),inverse(X2)))=multiply(inverse(X3),double_divide(double_divide(X3,double_divide(X2,X0)),X1)))),
% 0.12/0.47 inference(forward_demodulation,[status(thm)],[f17,f839])).
% 0.12/0.47 fof(f891,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(X0,X1)=double_divide(inverse(X0),inverse(X1)))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f859,f667])).
% 0.12/0.47 fof(f899,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (double_divide(X0,multiply(X1,X2))=multiply(inverse(X3),double_divide(double_divide(X3,double_divide(X2,X0)),X1)))),
% 0.12/0.47 inference(backward_demodulation,[status(thm)],[f891,f866])).
% 0.12/0.47 fof(f1046,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (multiply(double_divide(X0,multiply(X1,X2)),X3)=double_divide(double_divide(double_divide(X2,X1),X3),X0))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f733,f623])).
% 0.12/0.47 fof(f1139,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(X0,multiply(inverse(X0),X1))=X1)),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f674,f672])).
% 0.12/0.47 fof(f1453,plain,(
% 0.12/0.47 ![X0,X1]: (multiply(X0,inverse(X1))=double_divide(inverse(X0),X1))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f714,f1139])).
% 0.12/0.47 fof(f1957,plain,(
% 0.12/0.47 ![X0,X1,X2,X3]: (inverse(double_divide(X0,multiply(X1,X2)))=double_divide(double_divide(double_divide(X3,double_divide(X2,X0)),X1),inverse(X3)))),
% 0.12/0.47 inference(paramodulation,[status(thm)],[f899,f405])).
% 0.12/0.48 fof(f2047,plain,(
% 0.12/0.48 ![X0,X1,X2,X3]: (multiply(X0,multiply(X1,X2))=double_divide(double_divide(double_divide(X3,double_divide(X2,X0)),X1),inverse(X3)))),
% 0.12/0.48 inference(forward_demodulation,[status(thm)],[f751,f1957])).
% 0.12/0.48 fof(f2048,plain,(
% 0.12/0.48 ![X0,X1,X2,X3]: (multiply(X0,multiply(X1,X2))=multiply(double_divide(inverse(X3),multiply(double_divide(X2,X0),X3)),X1))),
% 0.12/0.48 inference(forward_demodulation,[status(thm)],[f1046,f2047])).
% 0.12/0.48 fof(f2049,plain,(
% 0.12/0.48 ![X0,X1,X2,X3]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X3,inverse(multiply(double_divide(X2,X0),X3))),X1))),
% 0.12/0.48 inference(forward_demodulation,[status(thm)],[f1453,f2048])).
% 0.12/0.48 fof(f2050,plain,(
% 0.12/0.48 ![X0,X1,X2,X3]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X3,double_divide(double_divide(X2,X0),X3)),X1))),
% 0.12/0.48 inference(forward_demodulation,[status(thm)],[f865,f2049])).
% 0.12/0.48 fof(f2051,plain,(
% 0.12/0.48 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(inverse(double_divide(X2,X0)),X1))),
% 0.12/0.48 inference(forward_demodulation,[status(thm)],[f347,f2050])).
% 0.12/0.48 fof(f2054,plain,(
% 0.12/0.48 ~multiply(a3,multiply(c3,b3))=multiply(a3,multiply(b3,c3))),
% 0.12/0.48 inference(backward_demodulation,[status(thm)],[f2094,f775])).
% 0.12/0.48 fof(f2094,plain,(
% 0.12/0.48 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X2,X0),X1))),
% 0.12/0.48 inference(forward_demodulation,[status(thm)],[f751,f2051])).
% 0.12/0.48 fof(f2258,plain,(
% 0.12/0.48 ~multiply(a3,multiply(c3,b3))=multiply(a3,multiply(c3,b3))),
% 0.12/0.48 inference(paramodulation,[status(thm)],[f674,f2054])).
% 0.12/0.48 fof(f2260,plain,(
% 0.12/0.48 $false),
% 0.12/0.48 inference(trivial_equality_resolution,[status(thm)],[f2258])).
% 0.12/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.50 % Elapsed time: 0.127039 seconds
% 0.12/0.50 % CPU time: 0.883158 seconds
% 0.12/0.50 % Total memory used: 38.531 MB
% 0.12/0.50 % Net memory used: 32.546 MB
%------------------------------------------------------------------------------