%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP083-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:36 PM UTC 2026
% Result : Unsatisfiable 79.02s 10.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP083-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 19:58:02 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 79.02/10.47 % Refutation found
% 79.02/10.47 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 79.02/10.47 % SZS output start CNFRefutation for theBenchmark
% 79.02/10.47 fof(f1,axiom,(
% 79.02/10.47 (![X,Y,Z,U]: (double_divide(double_divide(X,inverse(double_divide(Y,Z))),double_divide(inverse(Y),inverse(double_divide(U,double_divide(X,U))))) = Z ))),
% 79.02/10.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 79.02/10.47 fof(f2,axiom,(
% 79.02/10.47 (![X,Y]: (multiply(X,Y) = inverse(double_divide(Y,X)) ))),
% 79.02/10.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 79.02/10.47 fof(f3,negated_conjecture,(
% 79.02/10.47 ( 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)) ) ),
% 79.02/10.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 79.02/10.47 fof(f4,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,inverse(double_divide(X1,X2))),double_divide(inverse(X1),inverse(double_divide(X3,double_divide(X0,X3)))))=X2)),
% 79.02/10.47 inference(cnf_transformation,[status(thm)],[f1])).
% 79.02/10.47 fof(f5,plain,(
% 79.02/10.47 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 79.02/10.47 inference(cnf_transformation,[status(thm)],[f2])).
% 79.02/10.47 fof(f6,plain,(
% 79.02/10.47 ~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))),
% 79.02/10.47 inference(cnf_transformation,[status(thm)],[f3])).
% 79.02/10.47 fof(f7,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,multiply(X1,X2)),double_divide(inverse(X2),inverse(double_divide(X3,double_divide(X0,X3)))))=X1)),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f5,f4])).
% 79.02/10.47 fof(f8,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,multiply(X1,X2)),double_divide(inverse(X2),multiply(double_divide(X0,X3),X3)))=X1)),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f5,f7])).
% 79.02/10.47 fof(f9,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4]: (double_divide(double_divide(X0,multiply(X1,double_divide(X2,X3))),double_divide(multiply(X3,X2),multiply(double_divide(X0,X4),X4)))=X1)),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f5,f8])).
% 79.02/10.47 fof(f10,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5]: (double_divide(double_divide(double_divide(X0,multiply(X1,X2)),multiply(X3,X4)),double_divide(inverse(X4),multiply(X1,double_divide(inverse(X2),multiply(double_divide(X0,X5),X5)))))=X3)),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f8,f8])).
% 79.02/10.47 fof(f11,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (multiply(double_divide(inverse(X0),multiply(double_divide(X1,X2),X2)),double_divide(X1,multiply(X3,X0)))=inverse(X3))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f8,f5])).
% 79.02/10.47 fof(f12,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4]: (multiply(double_divide(multiply(X0,X1),multiply(double_divide(X2,X3),X3)),double_divide(X2,multiply(X4,double_divide(X1,X0))))=inverse(X4))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f5,f11])).
% 79.02/10.47 fof(f14,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(inverse(double_divide(X0,multiply(X1,X2))),multiply(double_divide(X3,X4),X4)),double_divide(X3,inverse(X1)))=inverse(double_divide(inverse(X2),multiply(double_divide(X0,X5),X5))))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f11,f11])).
% 79.02/10.47 fof(f16,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(multiply(multiply(X0,X1),X2),multiply(double_divide(X3,X4),X4)),double_divide(X3,inverse(X0)))=inverse(double_divide(inverse(X1),multiply(double_divide(X2,X5),X5))))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f5,f14])).
% 79.02/10.47 fof(f17,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(multiply(multiply(X0,X1),X2),multiply(double_divide(X3,X4),X4)),double_divide(X3,inverse(X0)))=multiply(multiply(double_divide(X2,X5),X5),inverse(X1)))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f5,f16])).
% 79.02/10.47 fof(f24,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5,X6]: (double_divide(double_divide(double_divide(X0,multiply(X1,X2)),multiply(X3,double_divide(X4,X5))),double_divide(multiply(X5,X4),multiply(X1,double_divide(inverse(X2),multiply(double_divide(X0,X6),X6)))))=X3)),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f8,f9])).
% 79.02/10.47 fof(f65,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (double_divide(double_divide(double_divide(double_divide(X0,multiply(X1,X2)),multiply(X3,X4)),multiply(X5,double_divide(X6,X7))),double_divide(multiply(X7,X6),multiply(X3,double_divide(inverse(X4),multiply(X1,double_divide(inverse(X2),multiply(double_divide(X0,X8),X8)))))))=X5)),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f10,f9])).
% 79.02/10.47 fof(f76,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(X0,X1),X1),inverse(X2))=multiply(multiply(double_divide(X0,X3),X3),inverse(X2)))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f17,f17])).
% 79.02/10.47 fof(f135,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (double_divide(double_divide(double_divide(X0,multiply(X1,X2)),multiply(multiply(double_divide(X3,X4),X4),inverse(X5))),double_divide(inverse(inverse(X5)),multiply(X1,double_divide(inverse(X2),multiply(double_divide(X0,X6),X6)))))=multiply(double_divide(X3,X7),X7))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f76,f10])).
% 79.02/10.47 fof(f153,plain,(
% 79.02/10.47 ![X0,X1,X2]: (multiply(double_divide(X0,X1),X1)=multiply(double_divide(X0,X2),X2))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f10,f135])).
% 79.02/10.47 fof(f164,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4]: (multiply(X0,double_divide(inverse(X1),multiply(double_divide(X2,X3),X3)))=multiply(double_divide(double_divide(X2,multiply(X0,X1)),X4),X4))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f8,f153])).
% 79.02/10.47 fof(f180,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(multiply(X0,X1),multiply(double_divide(X2,X3),X3)),double_divide(X2,multiply(double_divide(X4,X5),X5)))=inverse(double_divide(X4,double_divide(X1,X0))))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f153,f12])).
% 79.02/10.47 fof(f187,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4]: (multiply(double_divide(inverse(X0),multiply(double_divide(X1,X2),X2)),double_divide(X1,multiply(double_divide(X3,X4),X4)))=inverse(double_divide(X3,X0)))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f153,f11])).
% 79.02/10.47 fof(f208,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(multiply(X0,X1),multiply(double_divide(X2,X3),X3)),double_divide(X2,multiply(double_divide(X4,X5),X5)))=multiply(double_divide(X1,X0),X4))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f5,f180])).
% 79.02/10.47 fof(f210,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4]: (multiply(double_divide(inverse(X0),multiply(double_divide(X1,X2),X2)),double_divide(X1,multiply(double_divide(X3,X4),X4)))=multiply(X0,X3))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f5,f187])).
% 79.02/10.47 fof(f308,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4]: (inverse(double_divide(X0,X1))=multiply(double_divide(double_divide(X0,multiply(double_divide(inverse(X1),multiply(double_divide(inverse(X2),X3),X3)),X2)),X4),X4))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f11,f164])).
% 79.02/10.47 fof(f399,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4]: (multiply(X0,X1)=multiply(double_divide(double_divide(X1,multiply(double_divide(inverse(X0),multiply(double_divide(inverse(X2),X3),X3)),X2)),X4),X4))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f5,f308])).
% 79.02/10.47 fof(f4114,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(double_divide(multiply(double_divide(X0,X1),X1),multiply(double_divide(X2,X3),X3)),double_divide(X2,multiply(double_divide(X4,X5),X5)))=multiply(double_divide(X6,double_divide(X0,X6)),X4))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f153,f208])).
% 79.02/10.47 fof(f4243,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (multiply(double_divide(X0,double_divide(X1,X0)),X2)=multiply(double_divide(X3,double_divide(X1,X3)),X2))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f208,f4114])).
% 79.02/10.47 fof(f4282,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (multiply(double_divide(X0,X1),X1)=multiply(double_divide(X2,double_divide(X3,X2)),double_divide(X3,X0)))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f153,f4243])).
% 79.02/10.47 fof(f4410,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (double_divide(double_divide(double_divide(X0,multiply(X1,X2)),multiply(double_divide(X3,double_divide(X4,X3)),double_divide(X5,X6))),double_divide(multiply(X6,X5),multiply(X1,double_divide(inverse(X2),multiply(double_divide(X0,X7),X7)))))=double_divide(X8,double_divide(X4,X8)))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f4243,f24])).
% 79.02/10.47 fof(f4533,plain,(
% 79.02/10.47 ![X0,X1,X2]: (double_divide(X0,double_divide(X1,X0))=double_divide(X2,double_divide(X1,X2)))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f24,f4410])).
% 79.02/10.47 fof(f4599,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,X1),double_divide(X2,double_divide(X0,X2)))=double_divide(X3,double_divide(X1,X3)))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f4533,f4533])).
% 79.02/10.47 fof(f5784,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(double_divide(multiply(multiply(double_divide(X0,X1),X1),X2),multiply(double_divide(X3,X4),X4)),double_divide(X3,inverse(double_divide(X5,double_divide(X6,X5)))))=multiply(multiply(double_divide(X2,X7),X7),inverse(double_divide(X6,X0))))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f4282,f17])).
% 79.02/10.47 fof(f5827,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(double_divide(multiply(multiply(double_divide(X0,X1),X1),X2),multiply(double_divide(X3,X4),X4)),double_divide(X3,multiply(double_divide(X5,X6),X6)))=multiply(multiply(double_divide(X2,X7),X7),inverse(double_divide(X5,X0))))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f5,f5784])).
% 79.02/10.47 fof(f5828,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,multiply(double_divide(X1,X2),X2)),X3)=multiply(multiply(double_divide(X0,X4),X4),inverse(double_divide(X3,X1))))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f208,f5827])).
% 79.02/10.47 fof(f5829,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4]: (multiply(double_divide(X0,multiply(double_divide(X1,X2),X2)),X3)=multiply(multiply(double_divide(X0,X4),X4),multiply(X1,X3)))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f5,f5828])).
% 79.02/10.47 fof(f15868,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,X1)=multiply(multiply(double_divide(double_divide(X1,multiply(double_divide(inverse(X0),multiply(double_divide(inverse(X2),X3),X3)),X2)),X4),X4),multiply(X5,multiply(double_divide(X5,X6),X6))))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f399,f5829])).
% 79.02/10.47 fof(f16331,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (multiply(X0,X1)=multiply(multiply(X0,X1),multiply(X2,multiply(double_divide(X2,X3),X3))))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f399,f15868])).
% 79.02/10.47 fof(f16389,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(double_divide(multiply(X0,X1),multiply(double_divide(X2,X3),X3)),double_divide(X2,multiply(X4,double_divide(X1,X0))))=multiply(inverse(X4),multiply(X5,multiply(double_divide(X5,X6),X6))))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f12,f16331])).
% 79.02/10.47 fof(f16583,plain,(
% 79.02/10.47 ![X0,X1,X2]: (inverse(X0)=multiply(inverse(X0),multiply(X1,multiply(double_divide(X1,X2),X2))))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f12,f16389])).
% 79.02/10.47 fof(f16738,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(double_divide(inverse(X0),multiply(double_divide(X1,X2),X2)),double_divide(X1,multiply(double_divide(X3,X4),X4)))=multiply(double_divide(multiply(X5,multiply(double_divide(X5,X6),X6)),inverse(X0)),X3))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f16583,f208])).
% 79.02/10.47 fof(f16769,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (multiply(X0,X1)=multiply(double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),inverse(X0)),X1))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f210,f16738])).
% 79.02/10.47 fof(f17367,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (multiply(X0,inverse(X0))=multiply(double_divide(multiply(X1,multiply(double_divide(X1,X2),X2)),X3),X3))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f153,f16769])).
% 79.02/10.47 fof(f17571,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (double_divide(double_divide(double_divide(double_divide(X0,multiply(X1,X2)),multiply(X3,X4)),multiply(X5,double_divide(X6,X7))),double_divide(multiply(X7,X6),multiply(X3,double_divide(inverse(X4),multiply(X1,double_divide(inverse(X2),multiply(double_divide(X0,X8),X8)))))))=double_divide(multiply(X9,multiply(double_divide(X9,X10),X10)),inverse(X5)))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f16769,f65])).
% 79.02/10.47 fof(f17690,plain,(
% 79.02/10.47 ![X0,X1,X2]: (X0=double_divide(multiply(X1,multiply(double_divide(X1,X2),X2)),inverse(X0)))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f65,f17571])).
% 79.02/10.47 fof(f17835,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (double_divide(X0,X1)=double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),multiply(X1,X0)))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f5,f17690])).
% 79.02/10.47 fof(f21044,plain,(
% 79.02/10.47 ![X0,X1]: (multiply(X0,inverse(X0))=multiply(X1,inverse(X1)))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f17367,f17367])).
% 79.02/10.47 fof(f21351,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4]: (double_divide(double_divide(multiply(X0,multiply(double_divide(X0,X1),X1)),multiply(X2,X3)),double_divide(inverse(X3),multiply(X4,inverse(X4))))=X2)),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f17367,f8])).
% 79.02/10.47 fof(f21535,plain,(
% 79.02/10.47 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),double_divide(inverse(X0),multiply(X2,inverse(X2))))=X1)),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f17835,f21351])).
% 79.02/10.47 fof(f21650,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (double_divide(inverse(X0),X0)=double_divide(multiply(X1,multiply(double_divide(X1,X2),X2)),multiply(X3,inverse(X3))))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f21044,f17835])).
% 79.02/10.47 fof(f21685,plain,(
% 79.02/10.47 ![X0,X1,X2,X3,X4,X5]: (multiply(double_divide(multiply(X0,inverse(X0)),multiply(double_divide(X1,X2),X2)),double_divide(X1,multiply(double_divide(X3,X4),X4)))=multiply(double_divide(inverse(X5),X5),X3))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f21044,f208])).
% 79.02/10.47 fof(f21816,plain,(
% 79.02/10.47 ![X0,X1]: (double_divide(inverse(X0),X0)=double_divide(inverse(X1),X1))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f17835,f21650])).
% 79.02/10.47 fof(f21818,plain,(
% 79.02/10.47 ![X0,X1,X2]: (multiply(double_divide(inverse(X0),X0),X1)=multiply(double_divide(inverse(X2),X2),X1))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f208,f21685])).
% 79.02/10.47 fof(f25861,plain,(
% 79.02/10.47 ![X0,X1,X2]: (double_divide(double_divide(multiply(X0,inverse(X0)),X1),double_divide(inverse(X2),X2))=X1)),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f21816,f21535])).
% 79.02/10.47 fof(f30968,plain,(
% 79.02/10.47 ![X0,X1,X2]: (X0=multiply(X0,multiply(double_divide(multiply(X1,inverse(X1)),X2),X2)))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f8,f25861])).
% 79.02/10.47 fof(f31566,plain,(
% 79.02/10.47 ![X0,X1]: (X0=double_divide(multiply(X1,inverse(X1)),inverse(X0)))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f30968,f17690])).
% 79.02/10.47 fof(f31731,plain,(
% 79.02/10.47 ![X0,X1]: (X0=multiply(X0,multiply(X1,inverse(X1))))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f31566,f30968])).
% 79.02/10.47 fof(f31732,plain,(
% 79.02/10.47 ![X0,X1]: (double_divide(X0,double_divide(inverse(X1),X1))=inverse(X0))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f31566,f25861])).
% 79.02/10.47 fof(f31833,plain,(
% 79.02/10.47 ![X0,X1,X2,X3]: (double_divide(double_divide(multiply(X0,inverse(X0)),X1),double_divide(inverse(X2),X2))=double_divide(X3,double_divide(X1,X3)))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f31566,f4599])).
% 79.02/10.47 fof(f31925,plain,(
% 79.02/10.47 ![X0,X1]: (X0=double_divide(X1,double_divide(X0,X1)))),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f25861,f31833])).
% 79.02/10.47 fof(f32127,plain,(
% 79.02/10.47 ![X0,X1]: (multiply(double_divide(X0,X1),X1)=inverse(X0))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f31925,f5])).
% 79.02/10.47 fof(f32734,plain,(
% 79.02/10.47 ![X0,X1,X2]: (double_divide(double_divide(X0,multiply(X1,X2)),double_divide(inverse(X2),inverse(X0)))=X1)),
% 79.02/10.47 inference(backward_demodulation,[status(thm)],[f32127,f8])).
% 79.02/10.47 fof(f32882,plain,(
% 79.02/10.47 ![X0,X1]: (inverse(double_divide(X0,multiply(X1,inverse(X0))))=X1)),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f31732,f32734])).
% 79.02/10.47 fof(f32911,plain,(
% 79.02/10.47 ![X0,X1]: (multiply(multiply(X0,inverse(X1)),X1)=X0)),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f5,f32882])).
% 79.02/10.47 fof(f33069,plain,(
% 79.02/10.47 ![X0,X1]: (multiply(inverse(X0),X1)=double_divide(X0,inverse(X1)))),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f32127,f32911])).
% 79.02/10.47 fof(f33071,plain,(
% 79.02/10.47 ![X0,X1]: (multiply(multiply(X0,inverse(X0)),X1)=X1)),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f21044,f32911])).
% 79.02/10.47 fof(f33098,plain,(
% 79.02/10.47 ![X0,X1,X2]: (multiply(multiply(double_divide(inverse(X0),X0),inverse(double_divide(inverse(X1),X1))),X2)=X2)),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f21818,f33071])).
% 79.02/10.47 fof(f33123,plain,(
% 79.02/10.47 ![X0,X1,X2]: (multiply(multiply(double_divide(inverse(X0),X0),multiply(X1,inverse(X1))),X2)=X2)),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f5,f33098])).
% 79.02/10.47 fof(f33124,plain,(
% 79.02/10.47 ![X0,X1]: (multiply(double_divide(inverse(X0),X0),X1)=X1)),
% 79.02/10.47 inference(forward_demodulation,[status(thm)],[f31731,f33123])).
% 79.02/10.47 fof(f33189,plain,(
% 79.02/10.47 ![X0]: (inverse(inverse(X0))=X0)),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f32127,f33124])).
% 79.02/10.47 fof(f33243,plain,(
% 79.02/10.47 ![X0,X1]: (multiply(double_divide(X0,inverse(X0)),X1)=X1)),
% 79.02/10.47 inference(paramodulation,[status(thm)],[f33189,f33124])).
% 79.02/10.47 fof(f33246,plain,(
% 79.02/10.47 ![X0,X1]: (multiply(multiply(inverse(X0),X0),X1)=X1)),
% 79.02/10.53 inference(paramodulation,[status(thm)],[f33189,f33071])).
% 79.02/10.53 fof(f33332,plain,(
% 79.02/10.53 ![X0,X1]: (multiply(inverse(X0),X0)=double_divide(X1,inverse(X1)))),
% 79.02/10.53 inference(paramodulation,[status(thm)],[f33243,f32911])).
% 79.02/10.53 fof(f33361,plain,(
% 79.02/10.53 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|~a2=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 79.02/10.53 inference(backward_demodulation,[status(thm)],[f33246,f6])).
% 79.02/10.53 fof(f33396,plain,(
% 79.02/10.53 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 79.02/10.53 inference(trivial_equality_resolution,[status(thm)],[f33361])).
% 79.02/10.53 fof(f34281,plain,(
% 79.02/10.53 ~multiply(inverse(a1),a1)=double_divide(b1,inverse(b1))|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 79.02/10.53 inference(backward_demodulation,[status(thm)],[f33069,f33396])).
% 79.02/10.53 fof(f34295,plain,(
% 79.02/10.53 ![X0,X1]: (multiply(X0,X1)=double_divide(inverse(X0),inverse(X1)))),
% 79.02/10.53 inference(paramodulation,[status(thm)],[f33189,f33069])).
% 79.02/10.53 fof(f34328,plain,(
% 79.02/10.53 ~double_divide(a1,inverse(a1))=double_divide(b1,inverse(b1))|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 40.23/10.53 inference(forward_demodulation,[status(thm)],[f33069,f34281])).
% 40.23/10.53 fof(f37165,plain,(
% 40.23/10.53 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 40.23/10.53 inference(backward_subsumption_resolution,[status(thm)],[f34328,f37166])).
% 40.23/10.53 fof(f37166,plain,(
% 40.23/10.53 ![X0,X1]: (double_divide(X0,inverse(X0))=double_divide(X1,inverse(X1)))),
% 40.23/10.53 inference(forward_demodulation,[status(thm)],[f33069,f33332])).
% 40.23/10.53 fof(f41232,plain,(
% 40.23/10.53 ![X0,X1,X2]: (double_divide(double_divide(X0,multiply(X1,X2)),multiply(X2,X0))=X1)),
% 40.23/10.53 inference(backward_demodulation,[status(thm)],[f34295,f32734])).
% 40.23/10.53 fof(f41389,plain,(
% 40.23/10.53 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=inverse(double_divide(X2,multiply(X0,X1))))),
% 40.23/10.53 inference(paramodulation,[status(thm)],[f41232,f32127])).
% 40.23/10.53 fof(f41444,plain,(
% 40.23/10.53 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 40.23/10.53 inference(forward_demodulation,[status(thm)],[f5,f41389])).
% 40.23/10.53 fof(f48184,plain,(
% 40.23/10.53 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))),
% 40.23/10.53 inference(backward_demodulation,[status(thm)],[f41444,f37165])).
% 40.23/10.53 fof(f48292,plain,(
% 40.23/10.53 $false),
% 40.23/10.53 inference(trivial_equality_resolution,[status(thm)],[f48184])).
% 40.23/10.53 % SZS output end CNFRefutation for theBenchmark.p
% 40.23/10.57 % Elapsed time: 10.191046 seconds
% 40.23/10.57 % CPU time: 79.966487 seconds
% 40.23/10.57 % Total memory used: 442.895 MB
% 40.23/10.57 % Net memory used: 437.912 MB
%------------------------------------------------------------------------------