%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP108-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 : 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:35:39 PM UTC 2026
% Result : Unsatisfiable 1.23s 0.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP108-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.11/0.37 % Computer : n001.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 20 20:03:14 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 1.23/0.63 % Refutation found
% 1.23/0.63 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.23/0.63 % SZS output start CNFRefutation for theBenchmark
% 1.23/0.63 fof(f1,axiom,(
% 1.23/0.63 (![X,Y,Z]: (inverse(double_divide(inverse(double_divide(X,inverse(double_divide(Y,double_divide(X,Z))))),Z)) = Y ))),
% 1.23/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.23/0.63 fof(f2,axiom,(
% 1.23/0.63 (![X,Y]: (multiply(X,Y) = inverse(double_divide(Y,X)) ))),
% 1.23/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.23/0.63 fof(f3,negated_conjecture,(
% 1.23/0.63 ( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)| multiply(multiply(inverse(b2),b2),a2) != a2| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))| multiply(a4,b4) != multiply(b4,a4) ) ),
% 1.23/0.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.23/0.63 fof(f4,plain,(
% 1.23/0.63 ![X0,X1,X2]: (inverse(double_divide(inverse(double_divide(X0,inverse(double_divide(X1,double_divide(X0,X2))))),X2))=X1)),
% 1.23/0.63 inference(cnf_transformation,[status(thm)],[f1])).
% 1.23/0.63 fof(f5,plain,(
% 1.23/0.63 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 1.23/0.63 inference(cnf_transformation,[status(thm)],[f2])).
% 1.23/0.63 fof(f6,plain,(
% 1.23/0.63 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|~multiply(multiply(inverse(b2),b2),a2)=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))|~multiply(a4,b4)=multiply(b4,a4)),
% 1.23/0.63 inference(cnf_transformation,[status(thm)],[f3])).
% 1.23/0.63 fof(f7,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(X0,inverse(double_divide(X1,inverse(double_divide(X2,double_divide(X1,X0))))))=X2)),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f5,f4])).
% 1.23/0.63 fof(f8,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(X0,multiply(inverse(double_divide(X1,double_divide(X2,X0))),X2))=X1)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f5,f7])).
% 1.23/0.63 fof(f9,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(X0,multiply(multiply(double_divide(X1,X0),X2),X1))=X2)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f5,f8])).
% 1.23/0.63 fof(f10,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(X0,multiply(X1,X2))=multiply(multiply(double_divide(X3,double_divide(X2,X0)),X1),X3))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f9,f9])).
% 1.23/0.63 fof(f12,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(double_divide(X0,X1),multiply(X1,multiply(X2,X0)))=X2)),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f10,f9])).
% 1.23/0.63 fof(f14,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(double_divide(multiply(X0,X1),double_divide(X1,X2)),X0)=X2)),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f12,f12])).
% 1.23/0.63 fof(f15,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,multiply(double_divide(multiply(X1,X0),double_divide(X2,X3)),X4)),multiply(X3,multiply(X4,X2)))=X1)),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f10,f12])).
% 1.23/0.63 fof(f17,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(multiply(X0,multiply(X1,X2)),X3),multiply(X3,X1))=double_divide(X2,X0))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f12,f12])).
% 1.23/0.63 fof(f18,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,X1),multiply(X1,multiply(X2,multiply(X3,X4))))=multiply(double_divide(X0,double_divide(X4,X2)),X3))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f10,f12])).
% 1.23/0.63 fof(f30,plain,(
% 1.23/0.63 ![X0,X1,X2]: (X0=double_divide(X1,multiply(double_divide(multiply(X2,X1),X0),X2)))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f14,f17])).
% 1.23/0.63 fof(f32,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,X1),multiply(X1,X2))=double_divide(X3,double_divide(multiply(multiply(X2,X3),X4),double_divide(X4,X0))))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f14,f17])).
% 1.23/0.63 fof(f55,plain,(
% 1.23/0.63 ![X0,X1,X2]: (X0=double_divide(multiply(X1,X2),double_divide(X2,multiply(X0,X1))))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f17,f30])).
% 1.23/0.63 fof(f57,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(multiply(X0,multiply(X1,X2)),X3),X0)=double_divide(X2,multiply(X3,X1)))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f30,f30])).
% 1.23/0.63 fof(f68,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(multiply(double_divide(multiply(X0,X1),X2),X0),X1)=inverse(X2))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f30,f5])).
% 1.23/0.63 fof(f89,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(double_divide(X0,multiply(X1,X2)),multiply(X2,X0))=inverse(X1))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f55,f5])).
% 1.23/0.63 fof(f97,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,multiply(double_divide(X1,double_divide(X2,X3)),X4)),multiply(X3,multiply(X4,X2)))=double_divide(multiply(X0,X5),double_divide(X5,X1)))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f14,f15])).
% 1.23/0.63 fof(f144,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,multiply(double_divide(multiply(X1,X0),double_divide(X2,multiply(double_divide(multiply(X3,multiply(X4,X2)),X5),X3))),X4)),inverse(X5))=X1)),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f68,f15])).
% 1.23/0.63 fof(f155,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(X0,X1),multiply(X1,inverse(X2)))=multiply(double_divide(multiply(X3,X0),X2),X3))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f68,f12])).
% 1.23/0.63 fof(f158,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,multiply(double_divide(multiply(X1,X0),double_divide(X2,double_divide(X2,multiply(X3,X4)))),X4)),inverse(X3))=X1)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f57,f144])).
% 1.23/0.63 fof(f161,plain,(
% 1.23/0.63 ![X0,X1,X2]: (X0=inverse(double_divide(multiply(X0,multiply(X1,X2)),double_divide(X2,X1))))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f15,f89])).
% 1.23/0.63 fof(f166,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(X0,inverse(X1)),multiply(multiply(X2,X3),X0))=inverse(double_divide(X3,multiply(X1,X2))))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f89,f89])).
% 1.23/0.63 fof(f168,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(X0,inverse(X1)),multiply(X2,X0))=inverse(multiply(double_divide(multiply(X3,X2),X1),X3)))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f68,f89])).
% 1.23/0.63 fof(f184,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(inverse(X0),X1),double_divide(X2,multiply(X0,X3))),multiply(X3,X2))=inverse(X1))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f89,f68])).
% 1.23/0.63 fof(f189,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (X0=double_divide(multiply(X1,X2),multiply(double_divide(inverse(X3),X0),double_divide(X2,multiply(X3,X1)))))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f89,f30])).
% 1.23/0.63 fof(f192,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(inverse(X0),double_divide(multiply(X1,X2),X3)),double_divide(X2,multiply(X0,X1)))=X3)),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f89,f14])).
% 1.23/0.63 fof(f193,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(multiply(X0,X1),X2),multiply(X2,inverse(X3)))=double_divide(X1,multiply(X3,X0)))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f89,f12])).
% 1.23/0.63 fof(f194,plain,(
% 1.23/0.63 ![X0,X1,X2]: (X0=multiply(double_divide(X1,X2),multiply(X0,multiply(X2,X1))))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f5,f161])).
% 1.23/0.63 fof(f198,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(X0,inverse(X1)),multiply(multiply(X2,X3),X0))=multiply(multiply(X1,X2),X3))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f5,f166])).
% 1.23/0.63 fof(f204,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (X0=multiply(X1,multiply(X0,multiply(double_divide(X2,multiply(X1,X3)),multiply(X3,X2)))))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f55,f194])).
% 1.23/0.63 fof(f206,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (double_divide(multiply(X0,multiply(X1,X2)),X3)=multiply(double_divide(X1,X3),double_divide(X2,X0)))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f17,f194])).
% 1.23/0.63 fof(f207,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (double_divide(multiply(multiply(X0,X1),X2),double_divide(X2,X3))=multiply(double_divide(X1,X0),X3))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f14,f194])).
% 1.23/0.63 fof(f208,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4]: (double_divide(X0,multiply(double_divide(multiply(X1,X0),double_divide(X2,X3)),X4))=multiply(double_divide(multiply(X4,X2),X3),X1))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f15,f194])).
% 1.23/0.63 fof(f209,plain,(
% 1.23/0.63 ![X0,X1,X2]: (double_divide(X0,multiply(X1,X2))=multiply(double_divide(X0,X2),inverse(X1)))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f89,f194])).
% 1.23/0.63 fof(f211,plain,(
% 1.23/0.63 ![X0,X1,X2]: (double_divide(X0,X1)=multiply(double_divide(multiply(X2,X0),X1),X2))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f12,f194])).
% 1.23/0.63 fof(f213,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4]: (multiply(double_divide(multiply(X0,X1),double_divide(X2,X3)),X4)=multiply(double_divide(X1,X0),multiply(X3,multiply(X4,X2))))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f10,f194])).
% 1.23/0.63 fof(f244,plain,(
% 1.23/0.63 ![X0,X1]: (X0=multiply(X1,multiply(X0,inverse(X1))))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f89,f204])).
% 1.23/0.63 fof(f279,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(X0,X1),double_divide(X2,X3)),X3)=double_divide(X2,multiply(X1,X0)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f206,f57])).
% 1.23/0.63 fof(f290,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(X0,X1),multiply(X1,X2))=double_divide(X3,multiply(double_divide(X3,X2),X0)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f207,f32])).
% 1.23/0.63 fof(f298,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(multiply(X0,X1),double_divide(X1,multiply(X2,X0))),X3),inverse(X2))=X3)),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f208,f158])).
% 1.23/0.63 fof(f309,plain,(
% 1.23/0.63 ![X0,X1]: (double_divide(X0,double_divide(X0,X1))=X1)),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f211,f14])).
% 1.23/0.63 fof(f310,plain,(
% 1.23/0.63 ![X0,X1]: (multiply(double_divide(X0,X1),X0)=inverse(X1))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f211,f68])).
% 1.23/0.63 fof(f313,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(double_divide(X0,inverse(X1)),multiply(X2,X0))=inverse(double_divide(X2,X1)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f211,f168])).
% 1.23/0.63 fof(f314,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(double_divide(X0,X1),multiply(X1,inverse(X2)))=double_divide(X0,X2))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f211,f155])).
% 1.23/0.63 fof(f392,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(X0,X1),multiply(multiply(X2,X1),multiply(X3,X0))),inverse(X2))=X3)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f213,f298])).
% 1.23/0.63 fof(f401,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f402,f198])).
% 1.23/0.63 fof(f402,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(double_divide(X0,inverse(X1)),multiply(X2,X0))=multiply(X1,X2))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f5,f313])).
% 1.23/0.63 fof(f403,plain,(
% 1.23/0.63 ![X0,X1,X2]: (double_divide(multiply(X0,X1),X2)=double_divide(X1,multiply(X2,X0)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f314,f193])).
% 1.23/0.63 fof(f414,plain,(
% 1.23/0.63 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|~multiply(multiply(inverse(b2),b2),a2)=a2|~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))|~multiply(a4,b4)=multiply(b4,a4)),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f401,f6])).
% 1.23/0.63 fof(f415,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(X0,multiply(X1,X2))=multiply(double_divide(X3,double_divide(X2,X0)),multiply(X1,X3)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f401,f10])).
% 1.23/0.63 fof(f421,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(inverse(X0),X1),multiply(double_divide(X2,multiply(X0,X3)),multiply(X3,X2)))=inverse(X1))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f401,f184])).
% 1.23/0.63 fof(f435,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(X0,X1),multiply(multiply(multiply(X2,X1),multiply(X3,X0)),inverse(X2)))=X3)),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f401,f392])).
% 1.23/0.63 fof(f442,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(X0,X1),multiply(double_divide(X2,X3),X3))=double_divide(X2,multiply(X1,X0)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f401,f279])).
% 1.23/0.63 fof(f467,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (double_divide(multiply(X0,multiply(X1,X2)),double_divide(X2,X3))=multiply(double_divide(X1,X0),X3))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f401,f207])).
% 1.23/0.63 fof(f470,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (double_divide(multiply(X0,X1),multiply(X2,X3))=multiply(double_divide(X0,X2),double_divide(X1,X3)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f403,f206])).
% 1.23/0.63 fof(f471,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (X0=double_divide(X1,multiply(multiply(double_divide(inverse(X2),X0),double_divide(X1,multiply(X2,X3))),X3)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f403,f189])).
% 1.23/0.63 fof(f485,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,multiply(double_divide(X1,X2),X3)),X4)=multiply(double_divide(X0,X3),multiply(X2,multiply(X4,X1))))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f403,f213])).
% 1.23/0.63 fof(f487,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,multiply(double_divide(X1,double_divide(X2,X3)),X4)),multiply(X3,multiply(X4,X2)))=double_divide(X5,multiply(double_divide(X5,X1),X0)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f403,f97])).
% 1.23/0.63 fof(f503,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(inverse(X0),double_divide(X1,multiply(X2,X3))),double_divide(X1,multiply(X0,X3)))=X2)),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f403,f192])).
% 1.23/0.63 fof(f505,plain,(
% 1.23/0.63 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|~multiply(inverse(b2),multiply(b2,a2))=a2|~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))|~multiply(a4,b4)=multiply(b4,a4)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f401,f414])).
% 1.23/0.63 fof(f506,plain,(
% 1.23/0.63 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|~multiply(inverse(b2),multiply(b2,a2))=a2|~multiply(a4,b4)=multiply(b4,a4)),
% 1.23/0.63 inference(trivial_equality_resolution,[status(thm)],[f505])).
% 1.23/0.63 fof(f514,plain,(
% 1.23/0.63 ![X0,X1]: (multiply(double_divide(inverse(X0),X1),inverse(X0))=inverse(X1))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f89,f421])).
% 1.23/0.63 fof(f515,plain,(
% 1.23/0.63 ![X0,X1]: (double_divide(inverse(X0),multiply(X0,X1))=inverse(X1))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f209,f514])).
% 1.23/0.63 fof(f537,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(X0,X1),multiply(multiply(X2,X1),multiply(multiply(X3,X0),inverse(X2))))=X3)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f401,f435])).
% 1.23/0.63 fof(f538,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(X0,X1),multiply(X2,multiply(X1,multiply(multiply(X3,X0),inverse(X2)))))=X3)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f401,f537])).
% 1.23/0.63 fof(f539,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(X0,X1),multiply(X2,multiply(X1,multiply(X3,multiply(X0,inverse(X2))))))=X3)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f401,f538])).
% 1.23/0.63 fof(f578,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(X0,double_divide(X1,X2)),double_divide(X1,X3))=multiply(double_divide(X0,X3),X2))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f206,f467])).
% 1.23/0.63 fof(f579,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (double_divide(X0,multiply(multiply(X1,X2),X3))=multiply(double_divide(X3,X1),double_divide(X0,X2)))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f403,f470])).
% 1.23/0.63 fof(f589,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (double_divide(X0,multiply(X1,multiply(X2,X3)))=multiply(double_divide(X3,X1),double_divide(X0,X2)))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f401,f579])).
% 1.23/0.63 fof(f590,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (X0=double_divide(X1,multiply(double_divide(inverse(X2),X0),multiply(double_divide(X1,multiply(X2,X3)),X3))))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f401,f471])).
% 1.23/0.63 fof(f591,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (X0=multiply(double_divide(X1,double_divide(inverse(X2),X0)),double_divide(X3,double_divide(X3,multiply(X2,X1)))))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f589,f590])).
% 1.23/0.63 fof(f592,plain,(
% 1.23/0.63 ![X0,X1,X2]: (X0=multiply(double_divide(X1,double_divide(inverse(X2),X0)),multiply(X2,X1)))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f309,f591])).
% 1.23/0.63 fof(f593,plain,(
% 1.23/0.63 ![X0,X1]: (X0=multiply(X0,multiply(X1,inverse(X1))))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f415,f592])).
% 1.23/0.63 fof(f635,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,X1),multiply(double_divide(X2,X3),multiply(multiply(X3,multiply(X1,X2)),X4)))=double_divide(X5,multiply(double_divide(X5,X4),X0)))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f485,f487])).
% 1.23/0.63 fof(f636,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,X1),multiply(double_divide(X2,X3),multiply(X3,multiply(multiply(X1,X2),X4))))=double_divide(X5,multiply(double_divide(X5,X4),X0)))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f401,f635])).
% 1.23/0.63 fof(f637,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(X0,X1),multiply(double_divide(X2,X3),multiply(X3,multiply(X1,multiply(X2,X4)))))=double_divide(X5,multiply(double_divide(X5,X4),X0)))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f401,f636])).
% 1.23/0.63 fof(f638,plain,(
% 1.23/0.63 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,X1),multiply(double_divide(X2,double_divide(X3,X1)),X2))=double_divide(X4,multiply(double_divide(X4,X3),X0)))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f18,f637])).
% 1.23/0.63 fof(f639,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(double_divide(X0,X1),inverse(double_divide(X2,X1)))=double_divide(X3,multiply(double_divide(X3,X2),X0)))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f310,f638])).
% 1.23/0.63 fof(f640,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (double_divide(X0,multiply(double_divide(X1,X2),X2))=double_divide(X3,multiply(double_divide(X3,X1),X0)))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f209,f639])).
% 1.23/0.63 fof(f668,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(double_divide(inverse(X0),multiply(X0,X1)),multiply(X2,X1))=X2)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f578,f503])).
% 1.23/0.63 fof(f669,plain,(
% 1.23/0.63 ![X0,X1]: (multiply(inverse(X0),multiply(X1,X0))=X1)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f515,f668])).
% 1.23/0.63 fof(f724,plain,(
% 1.23/0.63 ![X0,X1]: (double_divide(inverse(X0),X1)=multiply(X0,inverse(X1)))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f310,f244])).
% 1.23/0.63 fof(f792,plain,(
% 1.23/0.63 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),X0)=inverse(X1))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f669,f669])).
% 1.23/0.63 fof(f794,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(inverse(multiply(X0,multiply(X1,X2))),X0)=double_divide(X2,X1))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f194,f669])).
% 1.23/0.63 fof(f800,plain,(
% 1.23/0.63 ![X0,X1]: (inverse(X0)=multiply(double_divide(X0,X1),X1))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f669,f194])).
% 1.23/0.63 fof(f801,plain,(
% 1.23/0.63 ![X0,X1]: (multiply(double_divide(X0,inverse(X0)),X1)=X1)),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f669,f12])).
% 1.23/0.63 fof(f813,plain,(
% 1.23/0.63 ![X0,X1]: (inverse(multiply(X0,X1))=double_divide(X1,X0))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f792,f794])).
% 1.23/0.63 fof(f821,plain,(
% 1.23/0.63 ![X0,X1,X2]: (double_divide(X0,inverse(X1))=double_divide(X2,multiply(double_divide(X2,X1),X0)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f800,f640])).
% 1.23/0.63 fof(f823,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(double_divide(X0,X1),inverse(X2))=double_divide(X2,multiply(X1,X0)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f800,f442])).
% 1.23/0.63 fof(f842,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(double_divide(X0,X1),multiply(X1,X2))=double_divide(X0,inverse(X2)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f821,f290])).
% 1.23/0.63 fof(f849,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (double_divide(X0,inverse(multiply(X1,multiply(X2,X3))))=multiply(double_divide(X0,double_divide(X3,X1)),X2))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f842,f18])).
% 1.23/0.63 fof(f854,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (double_divide(X0,double_divide(multiply(X1,X2),X3))=multiply(double_divide(X0,double_divide(X2,X3)),X1))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f813,f849])).
% 1.23/0.63 fof(f858,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (double_divide(X0,double_divide(X1,multiply(X2,X3)))=multiply(double_divide(X0,double_divide(X1,X2)),X3))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f403,f854])).
% 1.23/0.63 fof(f868,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(X0,multiply(inverse(X1),X2))=multiply(double_divide(multiply(X3,X1),double_divide(X2,X0)),X3))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f669,f415])).
% 1.23/0.63 fof(f872,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(X0,multiply(double_divide(X1,X2),X3))=multiply(double_divide(X1,double_divide(X3,X0)),inverse(X2)))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f310,f415])).
% 1.23/0.63 fof(f876,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (double_divide(X0,double_divide(X1,X2))=multiply(double_divide(X0,X3),multiply(X2,multiply(X3,X1))))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f415,f194])).
% 1.23/0.63 fof(f883,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(X0,multiply(inverse(X1),X2))=multiply(double_divide(X1,multiply(double_divide(X2,X0),X3)),X3))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f403,f868])).
% 1.23/0.63 fof(f888,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(X0,multiply(inverse(X1),multiply(X2,multiply(X1,inverse(X0)))))=X2)),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f894,f539])).
% 1.23/0.63 fof(f894,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(X0,multiply(inverse(X1),X2))=multiply(double_divide(X1,X3),multiply(X0,multiply(X3,X2))))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f485,f883])).
% 1.23/0.63 fof(f906,plain,(
% 1.23/0.63 ![X0,X1,X2]: (double_divide(X0,inverse(X1))=multiply(X1,multiply(double_divide(X0,X2),X2)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f908,f821])).
% 1.23/0.63 fof(f908,plain,(
% 1.23/0.63 ![X0,X1,X2,X3]: (multiply(X0,multiply(double_divide(X1,X2),X3))=double_divide(X2,multiply(double_divide(X3,X0),X1)))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f823,f872])).
% 1.23/0.63 fof(f918,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(X0,multiply(inverse(X1),X2))=double_divide(X1,double_divide(X2,X0)))),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f876,f894])).
% 1.23/0.63 fof(f953,plain,(
% 1.23/0.63 ![X0,X1]: (multiply(multiply(X0,inverse(X0)),X1)=X1)),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f955,f801])).
% 1.23/0.63 fof(f955,plain,(
% 1.23/0.63 ![X0,X1]: (double_divide(X0,inverse(X1))=multiply(X1,inverse(X0)))),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f800,f906])).
% 1.23/0.63 fof(f961,plain,(
% 1.23/0.63 ![X0,X1,X2]: (double_divide(X0,double_divide(multiply(X1,multiply(X0,inverse(X2))),X2))=X1)),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f918,f888])).
% 1.23/0.63 fof(f978,plain,(
% 1.23/0.63 ![X0,X1]: (multiply(X0,multiply(inverse(X0),X1))=X1)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f401,f953])).
% 1.23/0.63 fof(f981,plain,(
% 1.23/0.63 ![X0,X1]: (double_divide(X0,double_divide(X1,X0))=X1)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f918,f978])).
% 1.23/0.63 fof(f993,plain,(
% 1.23/0.63 ![X0,X1,X2]: (double_divide(X0,double_divide(multiply(X0,inverse(X1)),multiply(X1,X2)))=X2)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f403,f961])).
% 1.23/0.63 fof(f994,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(double_divide(X0,double_divide(multiply(X0,inverse(X1)),X1)),X2)=X2)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f858,f993])).
% 1.23/0.63 fof(f995,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(double_divide(X0,double_divide(inverse(X1),multiply(X1,X0))),X2)=X2)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f403,f994])).
% 1.23/0.63 fof(f996,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(multiply(double_divide(X0,double_divide(inverse(X1),X1)),X0),X2)=X2)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f858,f995])).
% 1.23/0.63 fof(f997,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(double_divide(X0,double_divide(inverse(X1),X1)),multiply(X0,X2))=X2)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f401,f996])).
% 1.23/0.63 fof(f998,plain,(
% 1.23/0.63 ![X0,X1,X2]: (multiply(double_divide(X0,multiply(X1,inverse(X1))),multiply(X0,X2))=X2)),
% 1.23/0.63 inference(forward_demodulation,[status(thm)],[f724,f997])).
% 1.23/0.63 fof(f1017,plain,(
% 1.23/0.63 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X0,X1)))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f981,f310])).
% 1.23/0.63 fof(f1366,plain,(
% 1.23/0.63 ![X0,X1]: (inverse(X0)=double_divide(X0,multiply(X1,inverse(X1))))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f593,f800])).
% 1.23/0.63 fof(f1378,plain,(
% 1.23/0.63 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=X1)),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f1366,f998])).
% 1.23/0.63 fof(f1380,plain,(
% 1.23/0.63 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|~a2=a2|~multiply(a4,b4)=multiply(b4,a4)),
% 1.23/0.63 inference(backward_demodulation,[status(thm)],[f1378,f506])).
% 1.23/0.63 fof(f1381,plain,(
% 1.23/0.63 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|~multiply(a4,b4)=multiply(b4,a4)),
% 1.23/0.63 inference(trivial_equality_resolution,[status(thm)],[f1380])).
% 1.23/0.63 fof(f1404,plain,(
% 1.23/0.63 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f5,f1017])).
% 1.23/0.63 fof(f1416,plain,(
% 1.23/0.63 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)),
% 1.23/0.63 inference(backward_subsumption_resolution,[status(thm)],[f1381,f1404])).
% 1.23/0.63 fof(f1466,plain,(
% 1.23/0.63 ![X0,X1]: (multiply(inverse(X0),X0)=multiply(X1,inverse(X1)))),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f593,f1378])).
% 1.23/0.63 fof(f1486,plain,(
% 1.23/0.63 ~multiply(a1,inverse(a1))=multiply(inverse(b1),b1)),
% 1.23/0.63 inference(paramodulation,[status(thm)],[f1404,f1416])).
% 1.23/0.63 fof(f1488,plain,(
% 1.23/0.63 $false),
% 1.23/0.63 inference(forward_subsumption_resolution,[status(thm)],[f1486,f1466])).
% 1.23/0.63 % SZS output end CNFRefutation for theBenchmark.p
% 1.23/0.65 % Elapsed time: 0.260066 seconds
% 1.23/0.65 % CPU time: 1.847552 seconds
% 1.23/0.65 % Total memory used: 99.098 MB
% 1.23/0.65 % Net memory used: 98.091 MB
%------------------------------------------------------------------------------