%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP102-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:35:38 PM UTC 2026
% Result : Unsatisfiable 0.16s 5.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP102-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/5.38 % Computer : n016.cluster.edu
% 0.12/5.38 % Model : x86_64 x86_64
% 0.12/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.38 % Memory : 8046.5625MB
% 0.12/5.38 % OS : Linux 6.8.0-71-generic
% 0.12/5.38 % CPULimit : 300
% 0.12/5.38 % WCLimit : 300
% 0.12/5.38 % DateTime : Sun Sep 20 20:02:12 UTC 2026
% 0.12/5.38 % CPUTime :
% 0.12/5.39 % Drodi V4.1.1
% 0.16/5.60 % Refutation found
% 0.16/5.60 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.16/5.60 % SZS output start CNFRefutation for theBenchmark
% 0.16/5.60 fof(f1,axiom,(
% 0.16/5.60 (![X,Y,Z]: (double_divide(double_divide(X,double_divide(double_divide(double_divide(Y,X),Z),double_divide(Y,identity))),double_divide(identity,identity)) = Z ))),
% 0.16/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.60 fof(f2,axiom,(
% 0.16/5.60 (![X,Y]: (multiply(X,Y) = double_divide(double_divide(Y,X),identity) ))),
% 0.16/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.60 fof(f3,axiom,(
% 0.16/5.60 (![X]: (inverse(X) = double_divide(X,identity) ))),
% 0.16/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.60 fof(f4,axiom,(
% 0.16/5.60 (![X]: (identity = double_divide(X,inverse(X)) ))),
% 0.16/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.60 fof(f5,negated_conjecture,(
% 0.16/5.60 ( multiply(inverse(a1),a1) != identity| multiply(identity,a2) != a2| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))| multiply(a4,b4) != multiply(b4,a4) ) ),
% 0.16/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.60 fof(f6,plain,(
% 0.16/5.60 ![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.16/5.60 inference(cnf_transformation,[status(thm)],[f1])).
% 0.16/5.60 fof(f7,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(X0,X1)=double_divide(double_divide(X1,X0),identity))),
% 0.16/5.60 inference(cnf_transformation,[status(thm)],[f2])).
% 0.16/5.60 fof(f8,plain,(
% 0.16/5.60 ![X0]: (inverse(X0)=double_divide(X0,identity))),
% 0.16/5.60 inference(cnf_transformation,[status(thm)],[f3])).
% 0.16/5.60 fof(f9,plain,(
% 0.16/5.60 ![X0]: (identity=double_divide(X0,inverse(X0)))),
% 0.16/5.60 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/5.60 fof(f10,plain,(
% 0.16/5.60 ~multiply(inverse(a1),a1)=identity|~multiply(identity,a2)=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))|~multiply(a4,b4)=multiply(b4,a4)),
% 0.16/5.60 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/5.60 fof(f11,plain,(
% 0.16/5.60 ![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.16/5.60 inference(backward_demodulation,[status(thm)],[f8,f6])).
% 0.16/5.60 fof(f12,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f8,f7])).
% 0.16/5.60 fof(f13,plain,(
% 0.16/5.60 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),inverse(X1))),inverse(identity))=X2)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f8,f11])).
% 0.16/5.60 fof(f14,plain,(
% 0.16/5.60 ![X0]: (multiply(identity,X0)=inverse(inverse(X0)))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f8,f12])).
% 0.16/5.60 fof(f16,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(identity,double_divide(X0,X1))=inverse(multiply(X1,X0)))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f12,f14])).
% 0.16/5.60 fof(f18,plain,(
% 0.16/5.60 ![X0,X1]: (identity=double_divide(double_divide(X0,X1),multiply(X1,X0)))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f12,f9])).
% 0.16/5.60 fof(f19,plain,(
% 0.16/5.60 ![X0]: (multiply(inverse(X0),X0)=inverse(identity))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f9,f12])).
% 0.16/5.60 fof(f20,plain,(
% 0.16/5.60 ~inverse(identity)=identity|~multiply(identity,a2)=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))|~multiply(a4,b4)=multiply(b4,a4)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f19,f10])).
% 0.16/5.60 fof(f22,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(multiply(X0,X1),double_divide(X1,X0))=inverse(identity))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f12,f19])).
% 0.16/5.60 fof(f82,plain,(
% 0.16/5.60 ![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.16/5.60 inference(paramodulation,[status(thm)],[f13,f13])).
% 0.16/5.60 fof(f84,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(double_divide(X0,double_divide(identity,inverse(X1))),inverse(identity))=multiply(X0,X1))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f18,f13])).
% 0.16/5.60 fof(f87,plain,(
% 0.16/5.60 ![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.16/5.60 inference(paramodulation,[status(thm)],[f13,f13])).
% 0.16/5.60 fof(f93,plain,(
% 0.16/5.60 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(double_divide(inverse(X1),X0),X2),multiply(identity,X1))),inverse(identity))=X2)),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f14,f13])).
% 0.16/5.60 fof(f101,plain,(
% 0.16/5.60 ![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.16/5.60 inference(forward_demodulation,[status(thm)],[f12,f87])).
% 0.16/5.60 fof(f109,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(double_divide(X0,multiply(double_divide(identity,X0),X1)),inverse(identity))=double_divide(identity,inverse(X1)))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f18,f82])).
% 0.16/5.60 fof(f117,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(double_divide(double_divide(identity,X0),double_divide(double_divide(X0,X1),inverse(identity))),inverse(identity))=X1)),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f82,f13])).
% 0.16/5.60 fof(f181,plain,(
% 0.16/5.60 ![X0]: (double_divide(double_divide(X0,identity),inverse(identity))=multiply(X0,identity))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f9,f84])).
% 0.16/5.60 fof(f187,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(double_divide(inverse(X0),inverse(identity)),inverse(identity))=double_divide(multiply(X1,X0),inverse(X1)))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f84,f82])).
% 0.16/5.60 fof(f188,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(double_divide(double_divide(identity,inverse(X0)),double_divide(multiply(X1,X0),inverse(X1))),inverse(identity))=inverse(identity))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f84,f13])).
% 0.16/5.60 fof(f196,plain,(
% 0.16/5.60 ![X0]: (double_divide(inverse(X0),inverse(identity))=multiply(X0,identity))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f8,f181])).
% 0.16/5.60 fof(f200,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(multiply(X0,identity),inverse(identity))=double_divide(multiply(X1,X0),inverse(X1)))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f196,f187])).
% 0.16/5.60 fof(f207,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(multiply(X0,X1),inverse(identity))=multiply(double_divide(X1,X0),identity))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f12,f196])).
% 0.16/5.60 fof(f212,plain,(
% 0.16/5.60 ![X0]: (multiply(inverse(identity),inverse(X0))=inverse(multiply(X0,identity)))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f196,f12])).
% 0.16/5.60 fof(f215,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(multiply(X1,X0),inverse(X1)))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f207,f200])).
% 0.16/5.60 fof(f220,plain,(
% 0.16/5.60 ![X0]: (double_divide(double_divide(double_divide(identity,inverse(X0)),multiply(double_divide(identity,X0),identity)),inverse(identity))=inverse(identity))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f215,f188])).
% 0.16/5.60 fof(f230,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(identity),multiply(X0,X1))=inverse(multiply(double_divide(X1,X0),identity)))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f207,f12])).
% 0.16/5.60 fof(f237,plain,(
% 0.16/5.60 ![X0]: (multiply(double_divide(identity,X0),identity)=multiply(double_divide(X0,identity),identity))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f207,f215])).
% 0.16/5.60 fof(f242,plain,(
% 0.16/5.60 ![X0]: (multiply(double_divide(identity,X0),identity)=double_divide(inverse(identity),inverse(inverse(X0))))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f19,f215])).
% 0.16/5.60 fof(f251,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=inverse(multiply(double_divide(identity,X1),identity)))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f215,f12])).
% 0.16/5.60 fof(f253,plain,(
% 0.16/5.60 ![X0]: (double_divide(double_divide(double_divide(identity,inverse(X0)),multiply(inverse(X0),identity)),inverse(identity))=inverse(identity))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f254,f220])).
% 0.16/5.60 fof(f254,plain,(
% 0.16/5.60 ![X0]: (multiply(double_divide(identity,X0),identity)=multiply(inverse(X0),identity))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f8,f237])).
% 0.16/5.60 fof(f266,plain,(
% 0.16/5.60 ![X0]: (multiply(inverse(X0),identity)=double_divide(inverse(identity),inverse(inverse(X0))))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f254,f242])).
% 0.16/5.60 fof(f269,plain,(
% 0.16/5.60 ![X0]: (multiply(inverse(X0),identity)=double_divide(inverse(identity),multiply(identity,X0)))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f14,f266])).
% 0.16/5.60 fof(f278,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=multiply(inverse(identity),multiply(X1,identity)))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f230,f251])).
% 0.16/5.60 fof(f279,plain,(
% 0.16/5.60 double_divide(identity,inverse(identity))=inverse(identity)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f18,f253])).
% 0.16/5.60 fof(f280,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(multiply(X0,X1),identity)=multiply(double_divide(X1,X0),identity))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f207])).
% 0.16/5.60 fof(f281,plain,(
% 0.16/5.60 ![X0]: (double_divide(inverse(X0),identity)=multiply(X0,identity))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f196])).
% 0.16/5.60 fof(f282,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(double_divide(X0,double_divide(identity,inverse(X1))),identity)=multiply(X0,X1))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f84])).
% 0.16/5.60 fof(f285,plain,(
% 0.16/5.60 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),inverse(X1))),identity)=X2)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f13])).
% 0.16/5.60 fof(f287,plain,(
% 0.16/5.60 ~identity=identity|~multiply(identity,a2)=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))|~multiply(a4,b4)=multiply(b4,a4)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f20])).
% 0.16/5.60 fof(f288,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(multiply(X0,X1),double_divide(X1,X0))=identity)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f22])).
% 0.16/5.60 fof(f289,plain,(
% 0.16/5.60 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f19])).
% 0.16/5.60 fof(f290,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=multiply(identity,multiply(X1,identity)))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f278])).
% 0.16/5.60 fof(f293,plain,(
% 0.16/5.60 ![X0]: (multiply(inverse(X0),identity)=double_divide(identity,multiply(identity,X0)))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f269])).
% 0.16/5.60 fof(f300,plain,(
% 0.16/5.60 ![X0]: (multiply(identity,inverse(X0))=inverse(multiply(X0,identity)))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f212])).
% 0.16/5.60 fof(f309,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(double_divide(double_divide(identity,X0),double_divide(double_divide(X0,X1),inverse(identity))),identity)=X1)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f117])).
% 0.16/5.60 fof(f315,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(double_divide(X0,multiply(double_divide(identity,X0),X1)),identity)=double_divide(identity,inverse(X1)))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f109])).
% 0.16/5.60 fof(f319,plain,(
% 0.16/5.60 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(double_divide(inverse(X1),X0),X2),multiply(identity,X1))),identity)=X2)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f93])).
% 0.16/5.60 fof(f324,plain,(
% 0.16/5.60 ![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))),identity)=X1)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f328,f101])).
% 0.16/5.60 fof(f328,plain,(
% 0.16/5.60 identity=inverse(identity)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f9,f279])).
% 0.16/5.60 fof(f329,plain,(
% 0.16/5.60 ![X0]: (inverse(multiply(X0,identity))=multiply(inverse(X0),identity))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f330,f254])).
% 0.16/5.60 fof(f330,plain,(
% 0.16/5.60 ![X0,X1]: (inverse(multiply(X0,X1))=multiply(double_divide(X1,X0),identity))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f8,f280])).
% 0.16/5.60 fof(f331,plain,(
% 0.16/5.60 ![X0]: (inverse(inverse(X0))=multiply(X0,identity))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f8,f281])).
% 0.16/5.60 fof(f332,plain,(
% 0.16/5.60 ![X0,X1]: (inverse(double_divide(X0,double_divide(identity,inverse(X1))))=multiply(X0,X1))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f8,f282])).
% 0.16/5.60 fof(f333,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(double_divide(identity,inverse(X0)),X1)=multiply(X1,X0))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f12,f332])).
% 0.16/5.60 fof(f336,plain,(
% 0.16/5.60 ![X0,X1,X2]: (inverse(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),inverse(X1))))=X2)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f8,f285])).
% 0.16/5.60 fof(f337,plain,(
% 0.16/5.60 ![X0,X1,X2]: (multiply(double_divide(double_divide(double_divide(X0,X1),X2),inverse(X0)),X1)=X2)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f12,f336])).
% 0.16/5.60 fof(f338,plain,(
% 0.16/5.60 ~multiply(identity,a2)=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))|~multiply(a4,b4)=multiply(b4,a4)),
% 0.16/5.60 inference(trivial_equality_resolution,[status(thm)],[f287])).
% 0.16/5.60 fof(f378,plain,(
% 0.16/5.60 ![X0,X1]: (inverse(double_divide(double_divide(identity,X0),double_divide(double_divide(X0,X1),inverse(identity))))=X1)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f8,f309])).
% 0.16/5.60 fof(f379,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(double_divide(double_divide(X0,X1),inverse(identity)),double_divide(identity,X0))=X1)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f12,f378])).
% 0.16/5.60 fof(f380,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(double_divide(double_divide(X0,X1),identity),double_divide(identity,X0))=X1)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f328,f379])).
% 0.16/5.60 fof(f381,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(double_divide(X0,X1)),double_divide(identity,X0))=X1)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f8,f380])).
% 0.16/5.60 fof(f382,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(multiply(X0,X1),double_divide(identity,X1))=X0)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f12,f381])).
% 0.16/5.60 fof(f396,plain,(
% 0.16/5.60 ![X0,X1]: (inverse(double_divide(X0,multiply(double_divide(identity,X0),X1)))=double_divide(identity,inverse(X1)))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f8,f315])).
% 0.16/5.60 fof(f397,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(multiply(double_divide(identity,X0),X1),X0)=double_divide(identity,inverse(X1)))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f12,f396])).
% 0.16/5.60 fof(f406,plain,(
% 0.16/5.60 ![X0,X1,X2]: (inverse(double_divide(X0,double_divide(double_divide(double_divide(inverse(X1),X0),X2),multiply(identity,X1))))=X2)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f8,f319])).
% 0.16/5.60 fof(f407,plain,(
% 0.16/5.60 ![X0,X1,X2]: (multiply(double_divide(double_divide(double_divide(inverse(X0),X1),X2),multiply(identity,X0)),X1)=X2)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f12,f406])).
% 0.16/5.60 fof(f418,plain,(
% 0.16/5.60 ![X0,X1,X2,X3]: (inverse(double_divide(inverse(identity),double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(double_divide(X2,X3),X0),inverse(X2)),X3))))=X1)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f8,f324])).
% 0.16/5.60 fof(f419,plain,(
% 0.16/5.60 ![X0,X1,X2,X3]: (multiply(double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(double_divide(X2,X3),X0),inverse(X2)),X3)),inverse(identity))=X1)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f12,f418])).
% 0.16/5.60 fof(f420,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(double_divide(double_divide(X0,X1),X0),inverse(identity))=X1)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f337,f419])).
% 0.16/5.60 fof(f421,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(double_divide(double_divide(X0,X1),X0),identity)=X1)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f328,f420])).
% 0.16/5.60 fof(f424,plain,(
% 0.16/5.60 ![X0,X1]: (inverse(multiply(X0,double_divide(X0,X1)))=X1)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f330,f421])).
% 0.16/5.60 fof(f430,plain,(
% 0.16/5.60 ![X0]: (multiply(identity,inverse(X0))=double_divide(identity,multiply(identity,X0)))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f437,f293])).
% 0.16/5.60 fof(f437,plain,(
% 0.16/5.60 ![X0]: (multiply(identity,inverse(X0))=multiply(inverse(X0),identity))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f300,f329])).
% 0.16/5.60 fof(f512,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(identity,double_divide(identity,double_divide(X0,X1)))=multiply(X1,X0))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f288,f382])).
% 0.16/5.60 fof(f513,plain,(
% 0.16/5.60 ![X0]: (multiply(identity,double_divide(identity,X0))=inverse(X0))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f289,f382])).
% 0.16/5.60 fof(f516,plain,(
% 0.16/5.60 ![X0]: (multiply(multiply(X0,inverse(identity)),identity)=X0)),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f9,f382])).
% 0.16/5.60 fof(f521,plain,(
% 0.16/5.60 ![X0,X1]: (inverse(multiply(double_divide(X0,X1),identity))=multiply(X1,X0))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f16,f512])).
% 0.16/5.60 fof(f522,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(identity,inverse(double_divide(X0,X1)))=multiply(X1,X0))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f300,f521])).
% 0.16/5.60 fof(f530,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=multiply(X1,identity))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f531,f290])).
% 0.16/5.60 fof(f531,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(identity,multiply(X0,X1))=multiply(X0,X1))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f12,f522])).
% 0.16/5.60 fof(f532,plain,(
% 0.16/5.60 ![X0]: (multiply(identity,inverse(X0))=inverse(X0))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f533,f300])).
% 0.16/5.60 fof(f533,plain,(
% 0.16/5.60 ![X0]: (inverse(multiply(X0,identity))=inverse(X0))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f16,f513])).
% 0.16/5.60 fof(f537,plain,(
% 0.16/5.60 ![X0]: (multiply(multiply(X0,identity),identity)=X0)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f328,f516])).
% 0.16/5.60 fof(f554,plain,(
% 0.16/5.60 ![X0]: (inverse(X0)=double_divide(identity,multiply(identity,X0)))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f532,f430])).
% 0.16/5.60 fof(f555,plain,(
% 0.16/5.60 ![X0]: (inverse(X0)=multiply(inverse(X0),identity))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f532,f437])).
% 0.16/5.60 fof(f567,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(double_divide(double_divide(double_divide(identity,X0),X1),identity),X0)=X1)),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f328,f337])).
% 0.16/5.60 fof(f578,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(double_divide(double_divide(identity,X0),X1)),X0)=X1)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f8,f567])).
% 0.16/5.60 fof(f579,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(multiply(X0,double_divide(identity,X1)),X1)=X0)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f12,f578])).
% 0.16/5.60 fof(f675,plain,(
% 0.16/5.60 ![X0,X1]: (inverse(double_divide(X0,X1))=multiply(multiply(X1,X0),identity))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f12,f555])).
% 0.16/5.60 fof(f684,plain,(
% 0.16/5.60 ![X0]: (multiply(X0,identity)=X0)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f687,f537])).
% 0.16/5.60 fof(f687,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(X0,X1)=multiply(multiply(X0,X1),identity))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f12,f675])).
% 0.16/5.60 fof(f692,plain,(
% 0.16/5.60 ![X0,X1]: (inverse(multiply(X0,X1))=double_divide(X1,X0))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f684,f330])).
% 0.16/5.60 fof(f698,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=X1)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f684,f530])).
% 0.16/5.60 fof(f702,plain,(
% 0.16/5.60 ![X0]: (inverse(inverse(X0))=X0)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f684,f331])).
% 0.16/5.60 fof(f706,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(double_divide(X0,X1),X0)=X1)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f692,f424])).
% 0.16/5.60 fof(f714,plain,(
% 0.16/5.60 ![X0]: (multiply(identity,X0)=X0)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f702,f14])).
% 0.16/5.60 fof(f719,plain,(
% 0.16/5.60 ~a2=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))|~multiply(a4,b4)=multiply(b4,a4)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f714,f338])).
% 0.16/5.60 fof(f727,plain,(
% 0.16/5.60 ![X0]: (inverse(X0)=double_divide(identity,X0))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f714,f554])).
% 0.16/5.60 fof(f731,plain,(
% 0.16/5.60 ![X0,X1,X2]: (multiply(double_divide(double_divide(double_divide(inverse(X0),X1),X2),X0),X1)=X2)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f714,f407])).
% 0.16/5.60 fof(f734,plain,(
% 0.16/5.60 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))|~multiply(a4,b4)=multiply(b4,a4)),
% 0.16/5.60 inference(trivial_equality_resolution,[status(thm)],[f719])).
% 0.16/5.60 fof(f738,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(multiply(X0,X1),inverse(X1))=X0)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f727,f382])).
% 0.16/5.60 fof(f741,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(multiply(double_divide(identity,X0),X1),X0)=inverse(inverse(X1)))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f727,f397])).
% 0.16/5.60 fof(f742,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=multiply(X1,X0))),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f727,f333])).
% 0.16/5.60 fof(f754,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(multiply(X0,inverse(X1)),X1)=X0)),
% 0.16/5.60 inference(backward_demodulation,[status(thm)],[f727,f579])).
% 0.16/5.60 fof(f764,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(multiply(inverse(X0),X1),X0)=inverse(inverse(X1)))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f727,f741])).
% 0.16/5.60 fof(f765,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(multiply(inverse(X0),X1),X0)=multiply(identity,X1))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f14,f764])).
% 0.16/5.60 fof(f766,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(multiply(inverse(X0),X1),X0)=X1)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f714,f765])).
% 0.16/5.60 fof(f767,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(multiply(identity,X0),X1)=multiply(X1,X0))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f14,f742])).
% 0.16/5.60 fof(f768,plain,(
% 0.16/5.60 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 0.16/5.60 inference(backward_subsumption_resolution,[status(thm)],[f734,f769])).
% 0.16/5.60 fof(f769,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f714,f767])).
% 0.16/5.60 fof(f806,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(X0,double_divide(X1,X0))=X1)),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f706,f706])).
% 0.16/5.60 fof(f812,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(X0,double_divide(X0,X1))=inverse(X1))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f706,f12])).
% 0.16/5.60 fof(f844,plain,(
% 0.16/5.60 ~multiply(c3,multiply(a3,b3))=multiply(a3,multiply(b3,c3))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f769,f768])).
% 0.16/5.60 fof(f869,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(double_divide(X0,X1),X1)=inverse(X0))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f806,f12])).
% 0.16/5.60 fof(f1126,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(X0),X1)=double_divide(inverse(X1),X0))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f812,f766])).
% 0.16/5.60 fof(f1127,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(X0),inverse(double_divide(X1,X0)))=X1)),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f812,f738])).
% 0.16/5.60 fof(f1128,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(X0),inverse(X1))=double_divide(X0,X1))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f812,f698])).
% 0.16/5.60 fof(f1145,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(inverse(inverse(double_divide(X0,X1))),X1)=X0)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f1126,f1127])).
% 0.16/5.60 fof(f1146,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(double_divide(X0,X1),X1)=X0)),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f702,f1145])).
% 0.16/5.60 fof(f1147,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(inverse(inverse(X0)),X1)=double_divide(X1,X0))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f1126,f1128])).
% 0.16/5.60 fof(f1148,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(X0,X1)=double_divide(X1,X0))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f702,f1147])).
% 0.16/5.60 fof(f1167,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(X0,double_divide(X0,X1))=X1)),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f806,f1146])).
% 0.16/5.60 fof(f1177,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(X0,double_divide(X1,X0))=inverse(X1))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f1146,f12])).
% 0.16/5.60 fof(f1215,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X0,X1)))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f1148,f12])).
% 0.16/5.60 fof(f1272,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(X0),X1)=double_divide(X0,inverse(X1)))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f869,f754])).
% 0.16/5.60 fof(f1517,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(double_divide(identity,X0),X1)=multiply(X1,inverse(X0)))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f18,f731])).
% 0.16/5.60 fof(f1520,plain,(
% 0.16/5.60 ![X0,X1,X2]: (multiply(double_divide(X0,X1),X2)=double_divide(double_divide(inverse(X1),X2),X0))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f1167,f731])).
% 0.16/5.60 fof(f1538,plain,(
% 0.16/5.60 ![X0,X1,X2]: (multiply(X0,X1)=double_divide(double_divide(double_divide(inverse(X2),inverse(X1)),X0),X2))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f731,f754])).
% 0.16/5.60 fof(f1556,plain,(
% 0.16/5.60 ![X0,X1]: (multiply(inverse(X0),X1)=multiply(X1,inverse(X0)))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f727,f1517])).
% 0.16/5.60 fof(f1568,plain,(
% 0.16/5.60 ![X0,X1]: (double_divide(X0,inverse(X1))=multiply(X1,inverse(X0)))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f1272,f1556])).
% 0.16/5.60 fof(f1601,plain,(
% 0.16/5.60 ![X0,X1,X2]: (multiply(X0,X1)=double_divide(multiply(double_divide(X0,X2),inverse(X1)),X2))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f1520,f1538])).
% 0.16/5.60 fof(f1602,plain,(
% 0.16/5.60 ![X0,X1,X2]: (multiply(X0,X1)=double_divide(double_divide(X1,inverse(double_divide(X0,X2))),X2))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f1568,f1601])).
% 0.16/5.60 fof(f1603,plain,(
% 0.16/5.60 ![X0,X1,X2]: (multiply(X0,X1)=double_divide(double_divide(X1,multiply(X2,X0)),X2))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f12,f1602])).
% 0.16/5.60 fof(f4176,plain,(
% 0.16/5.60 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=inverse(double_divide(X2,multiply(X0,X1))))),
% 0.16/5.60 inference(paramodulation,[status(thm)],[f1603,f1177])).
% 0.16/5.60 fof(f4237,plain,(
% 0.16/5.60 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(X2,multiply(X0,X1)))),
% 0.16/5.60 inference(forward_demodulation,[status(thm)],[f1215,f4176])).
% 0.16/5.60 fof(f4238,plain,(
% 0.16/5.60 $false),
% 0.16/5.60 inference(backward_subsumption_resolution,[status(thm)],[f844,f4237])).
% 0.16/5.60 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/5.62 % Elapsed time: 0.224966 seconds
% 0.16/5.62 % CPU time: 1.591057 seconds
% 0.16/5.62 % Total memory used: 96.511 MB
% 0.16/5.62 % Net memory used: 94.666 MB
%------------------------------------------------------------------------------