%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP503-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 : n015.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:44 PM UTC 2026
% Result : Unsatisfiable 56.36s 7.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP503-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 20:18:21 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 56.36/7.57 % Refutation found
% 56.36/7.57 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 56.36/7.57 % SZS output start CNFRefutation for theBenchmark
% 56.36/7.57 fof(f1,axiom,(
% 56.36/7.57 (![A,B,C,D]: (double_divide(double_divide(A,inverse(double_divide(B,C))),double_divide(inverse(B),inverse(double_divide(D,double_divide(A,D))))) = C ))),
% 56.36/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.36/7.57 fof(f2,axiom,(
% 56.36/7.57 (![A,B]: (multiply(A,B) = inverse(double_divide(B,A)) ))),
% 56.36/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.36/7.57 fof(f3,negated_conjecture,(
% 56.36/7.57 multiply(multiply(inverse(b2),b2),a2) != a2 ),
% 56.36/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 56.36/7.57 fof(f4,plain,(
% 56.36/7.57 ![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)),
% 56.36/7.57 inference(cnf_transformation,[status(thm)],[f1])).
% 56.36/7.57 fof(f5,plain,(
% 56.36/7.57 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 56.36/7.57 inference(cnf_transformation,[status(thm)],[f2])).
% 56.36/7.57 fof(f6,plain,(
% 56.36/7.57 ~multiply(multiply(inverse(b2),b2),a2)=a2),
% 56.36/7.57 inference(cnf_transformation,[status(thm)],[f3])).
% 56.36/7.57 fof(f11,plain,(
% 56.36/7.57 ![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)),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f5,f4])).
% 56.36/7.57 fof(f12,plain,(
% 56.36/7.57 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,multiply(X1,X2)),double_divide(inverse(X2),multiply(double_divide(X0,X3),X3)))=X1)),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f5,f11])).
% 56.36/7.57 fof(f13,plain,(
% 56.36/7.57 ![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)),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f5,f12])).
% 56.36/7.57 fof(f14,plain,(
% 56.36/7.57 ![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)),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f12,f12])).
% 56.36/7.57 fof(f15,plain,(
% 56.36/7.57 ![X0,X1,X2,X3]: (multiply(double_divide(inverse(X0),multiply(double_divide(X1,X2),X2)),double_divide(X1,multiply(X3,X0)))=inverse(X3))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f12,f5])).
% 56.36/7.57 fof(f16,plain,(
% 56.36/7.57 ![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))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f5,f15])).
% 56.36/7.57 fof(f18,plain,(
% 56.36/7.57 ![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))))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f15,f15])).
% 56.36/7.57 fof(f20,plain,(
% 56.36/7.57 ![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))))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f5,f18])).
% 56.36/7.57 fof(f21,plain,(
% 56.36/7.57 ![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)))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f5,f20])).
% 56.36/7.57 fof(f28,plain,(
% 56.36/7.57 ![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)),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f12,f13])).
% 56.36/7.57 fof(f69,plain,(
% 56.36/7.57 ![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)),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f14,f13])).
% 56.36/7.57 fof(f80,plain,(
% 56.36/7.57 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(X0,X1),X1),inverse(X2))=multiply(multiply(double_divide(X0,X3),X3),inverse(X2)))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f21,f21])).
% 56.36/7.57 fof(f139,plain,(
% 56.36/7.57 ![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))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f80,f14])).
% 56.36/7.57 fof(f157,plain,(
% 56.36/7.57 ![X0,X1,X2]: (multiply(double_divide(X0,X1),X1)=multiply(double_divide(X0,X2),X2))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f14,f139])).
% 56.36/7.57 fof(f168,plain,(
% 56.36/7.57 ![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))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f12,f157])).
% 56.36/7.57 fof(f184,plain,(
% 56.36/7.57 ![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))))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f157,f16])).
% 56.36/7.57 fof(f191,plain,(
% 56.36/7.57 ![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)))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f157,f15])).
% 56.36/7.57 fof(f212,plain,(
% 56.36/7.57 ![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))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f5,f184])).
% 56.36/7.57 fof(f214,plain,(
% 56.36/7.57 ![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))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f5,f191])).
% 56.36/7.57 fof(f731,plain,(
% 56.36/7.57 ![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))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f15,f168])).
% 56.36/7.57 fof(f864,plain,(
% 56.36/7.57 ![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))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f5,f731])).
% 56.36/7.57 fof(f4378,plain,(
% 56.36/7.57 ![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))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f157,f212])).
% 56.36/7.57 fof(f4511,plain,(
% 56.36/7.57 ![X0,X1,X2,X3]: (multiply(double_divide(X0,double_divide(X1,X0)),X2)=multiply(double_divide(X3,double_divide(X1,X3)),X2))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f212,f4378])).
% 56.36/7.57 fof(f4553,plain,(
% 56.36/7.57 ![X0,X1,X2,X3]: (multiply(double_divide(X0,X1),X1)=multiply(double_divide(X2,double_divide(X3,X2)),double_divide(X3,X0)))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f157,f4511])).
% 56.36/7.57 fof(f4685,plain,(
% 56.36/7.57 ![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)))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f4511,f28])).
% 56.36/7.57 fof(f4814,plain,(
% 56.36/7.57 ![X0,X1,X2]: (double_divide(X0,double_divide(X1,X0))=double_divide(X2,double_divide(X1,X2)))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f28,f4685])).
% 56.36/7.57 fof(f4885,plain,(
% 56.36/7.57 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,X1),double_divide(X2,double_divide(X0,X2)))=double_divide(X3,double_divide(X1,X3)))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f4814,f4814])).
% 56.36/7.57 fof(f6038,plain,(
% 56.36/7.57 ![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))))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f4553,f21])).
% 56.36/7.57 fof(f6084,plain,(
% 56.36/7.57 ![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))))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f5,f6038])).
% 56.36/7.57 fof(f6085,plain,(
% 56.36/7.57 ![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))))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f212,f6084])).
% 56.36/7.57 fof(f6086,plain,(
% 56.36/7.57 ![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)))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f5,f6085])).
% 56.36/7.57 fof(f15906,plain,(
% 56.36/7.57 ![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))))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f864,f6086])).
% 56.36/7.57 fof(f16369,plain,(
% 56.36/7.57 ![X0,X1,X2,X3]: (multiply(X0,X1)=multiply(multiply(X0,X1),multiply(X2,multiply(double_divide(X2,X3),X3))))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f864,f15906])).
% 56.36/7.57 fof(f16427,plain,(
% 56.36/7.57 ![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))))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f16,f16369])).
% 56.36/7.57 fof(f16621,plain,(
% 56.36/7.57 ![X0,X1,X2]: (inverse(X0)=multiply(inverse(X0),multiply(X1,multiply(double_divide(X1,X2),X2))))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f16,f16427])).
% 56.36/7.57 fof(f16774,plain,(
% 56.36/7.57 ![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))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f16621,f212])).
% 56.36/7.57 fof(f16807,plain,(
% 56.36/7.57 ![X0,X1,X2,X3]: (multiply(X0,X1)=multiply(double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),inverse(X0)),X1))),
% 56.36/7.57 inference(forward_demodulation,[status(thm)],[f214,f16774])).
% 56.36/7.57 fof(f17405,plain,(
% 56.36/7.57 ![X0,X1,X2,X3]: (multiply(X0,inverse(X0))=multiply(double_divide(multiply(X1,multiply(double_divide(X1,X2),X2)),X3),X3))),
% 56.36/7.57 inference(paramodulation,[status(thm)],[f157,f16807])).
% 56.36/7.57 fof(f17609,plain,(
% 56.36/7.57 ![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)))),
% 56.36/7.58 inference(paramodulation,[status(thm)],[f16807,f69])).
% 56.36/7.58 fof(f17728,plain,(
% 56.36/7.58 ![X0,X1,X2]: (X0=double_divide(multiply(X1,multiply(double_divide(X1,X2),X2)),inverse(X0)))),
% 56.36/7.58 inference(forward_demodulation,[status(thm)],[f69,f17609])).
% 56.36/7.58 fof(f18722,plain,(
% 56.36/7.58 ![X0,X1,X2,X3]: (double_divide(X0,X1)=double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),multiply(X1,X0)))),
% 56.36/7.58 inference(paramodulation,[status(thm)],[f5,f17728])).
% 56.36/7.58 fof(f22700,plain,(
% 56.36/7.58 ![X0,X1]: (multiply(X0,inverse(X0))=multiply(X1,inverse(X1)))),
% 56.36/7.58 inference(paramodulation,[status(thm)],[f17405,f17405])).
% 56.36/7.58 fof(f23017,plain,(
% 56.36/7.58 ![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)),
% 56.36/7.58 inference(paramodulation,[status(thm)],[f17405,f12])).
% 56.36/7.58 fof(f23213,plain,(
% 56.36/7.58 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),double_divide(inverse(X0),multiply(X2,inverse(X2))))=X1)),
% 52.01/7.63 inference(forward_demodulation,[status(thm)],[f18722,f23017])).
% 52.01/7.63 fof(f23340,plain,(
% 52.01/7.63 ![X0,X1,X2,X3]: (double_divide(inverse(X0),X0)=double_divide(multiply(X1,multiply(double_divide(X1,X2),X2)),multiply(X3,inverse(X3))))),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f22700,f18722])).
% 52.01/7.63 fof(f23375,plain,(
% 52.01/7.63 ![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))),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f22700,f212])).
% 52.01/7.63 fof(f23515,plain,(
% 52.01/7.63 ![X0,X1]: (double_divide(inverse(X0),X0)=double_divide(inverse(X1),X1))),
% 52.01/7.63 inference(forward_demodulation,[status(thm)],[f18722,f23340])).
% 52.01/7.63 fof(f23517,plain,(
% 52.01/7.63 ![X0,X1,X2]: (multiply(double_divide(inverse(X0),X0),X1)=multiply(double_divide(inverse(X2),X2),X1))),
% 52.01/7.63 inference(forward_demodulation,[status(thm)],[f212,f23375])).
% 52.01/7.63 fof(f26755,plain,(
% 52.01/7.63 ![X0,X1,X2]: (double_divide(double_divide(multiply(X0,inverse(X0)),X1),double_divide(inverse(X2),X2))=X1)),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f23515,f23213])).
% 52.01/7.63 fof(f31018,plain,(
% 52.01/7.63 ![X0,X1,X2]: (X0=multiply(X0,multiply(double_divide(multiply(X1,inverse(X1)),X2),X2)))),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f12,f26755])).
% 52.01/7.63 fof(f31616,plain,(
% 52.01/7.63 ![X0,X1]: (X0=double_divide(multiply(X1,inverse(X1)),inverse(X0)))),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f31018,f17728])).
% 52.01/7.63 fof(f32859,plain,(
% 52.01/7.63 ![X0,X1]: (X0=multiply(X0,multiply(X1,inverse(X1))))),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f31616,f31018])).
% 52.01/7.63 fof(f32860,plain,(
% 52.01/7.63 ![X0,X1]: (double_divide(X0,double_divide(inverse(X1),X1))=inverse(X0))),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f31616,f26755])).
% 52.01/7.63 fof(f32963,plain,(
% 52.01/7.63 ![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)))),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f31616,f4885])).
% 52.01/7.63 fof(f33055,plain,(
% 52.01/7.63 ![X0,X1]: (X0=double_divide(X1,double_divide(X0,X1)))),
% 52.01/7.63 inference(forward_demodulation,[status(thm)],[f26755,f32963])).
% 52.01/7.63 fof(f33259,plain,(
% 52.01/7.63 ![X0,X1]: (multiply(double_divide(X0,X1),X1)=inverse(X0))),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f33055,f5])).
% 52.01/7.63 fof(f34719,plain,(
% 52.01/7.63 ![X0,X1,X2]: (double_divide(double_divide(X0,multiply(X1,X2)),double_divide(inverse(X2),inverse(X0)))=X1)),
% 52.01/7.63 inference(backward_demodulation,[status(thm)],[f33259,f12])).
% 52.01/7.63 fof(f34865,plain,(
% 52.01/7.63 ![X0,X1]: (X0=inverse(double_divide(X1,multiply(X0,inverse(X1)))))),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f34719,f32860])).
% 52.01/7.63 fof(f34897,plain,(
% 52.01/7.63 ![X0,X1]: (X0=multiply(multiply(X0,inverse(X1)),X1))),
% 52.01/7.63 inference(forward_demodulation,[status(thm)],[f5,f34865])).
% 52.01/7.63 fof(f34918,plain,(
% 52.01/7.63 ![X0,X1]: (X0=multiply(multiply(X1,inverse(X1)),X0))),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f22700,f34897])).
% 52.01/7.63 fof(f34938,plain,(
% 52.01/7.63 ![X0,X1,X2]: (X0=multiply(multiply(double_divide(inverse(X1),X1),inverse(double_divide(inverse(X2),X2))),X0))),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f23517,f34918])).
% 52.01/7.63 fof(f34958,plain,(
% 52.01/7.63 ![X0,X1,X2]: (X0=multiply(multiply(double_divide(inverse(X1),X1),multiply(X2,inverse(X2))),X0))),
% 52.01/7.63 inference(forward_demodulation,[status(thm)],[f5,f34938])).
% 52.01/7.63 fof(f34959,plain,(
% 52.01/7.63 ![X0,X1]: (X0=multiply(double_divide(inverse(X1),X1),X0))),
% 52.01/7.63 inference(forward_demodulation,[status(thm)],[f32859,f34958])).
% 52.01/7.63 fof(f35041,plain,(
% 52.01/7.63 ![X0]: (X0=inverse(inverse(X0)))),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f33259,f34959])).
% 52.01/7.63 fof(f35093,plain,(
% 52.01/7.63 ![X0,X1]: (X0=multiply(multiply(inverse(X1),X1),X0))),
% 52.01/7.63 inference(paramodulation,[status(thm)],[f35041,f34918])).
% 52.01/7.63 fof(f35271,plain,(
% 52.01/7.63 ~a2=a2),
% 52.01/7.63 inference(backward_demodulation,[status(thm)],[f35093,f6])).
% 52.01/7.63 fof(f35305,plain,(
% 52.01/7.63 $false),
% 52.01/7.63 inference(trivial_equality_resolution,[status(thm)],[f35271])).
% 52.01/7.63 % SZS output end CNFRefutation for theBenchmark.p
% 52.01/7.68 % Elapsed time: 7.287190 seconds
% 52.01/7.68 % CPU time: 57.588379 seconds
% 52.01/7.68 % Total memory used: 489.140 MB
% 52.01/7.68 % Net memory used: 483.437 MB
%------------------------------------------------------------------------------