%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP502-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 : n017.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:43 PM UTC 2026
% Result : Unsatisfiable 57.47s 7.75s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP502-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n017.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 20:10:27 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 57.47/7.75 % Refutation found
% 57.47/7.75 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 57.47/7.75 % SZS output start CNFRefutation for theBenchmark
% 57.47/7.75 fof(f1,axiom,(
% 57.47/7.75 (![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 ))),
% 57.47/7.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.47/7.75 fof(f2,axiom,(
% 57.47/7.75 (![A,B]: (multiply(A,B) = inverse(double_divide(B,A)) ))),
% 57.47/7.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.47/7.75 fof(f3,negated_conjecture,(
% 57.47/7.75 multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
% 57.47/7.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 57.47/7.75 fof(f4,plain,(
% 57.47/7.75 ![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)),
% 57.47/7.75 inference(cnf_transformation,[status(thm)],[f1])).
% 57.47/7.75 fof(f5,plain,(
% 57.47/7.75 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 57.47/7.75 inference(cnf_transformation,[status(thm)],[f2])).
% 57.47/7.75 fof(f6,plain,(
% 57.47/7.75 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)),
% 57.47/7.75 inference(cnf_transformation,[status(thm)],[f3])).
% 57.47/7.75 fof(f12,plain,(
% 57.47/7.75 ![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)),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f5,f4])).
% 57.47/7.75 fof(f13,plain,(
% 57.47/7.75 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,multiply(X1,X2)),double_divide(inverse(X2),multiply(double_divide(X0,X3),X3)))=X1)),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f5,f12])).
% 57.47/7.75 fof(f14,plain,(
% 57.47/7.75 ![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)),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f5,f13])).
% 57.47/7.75 fof(f15,plain,(
% 57.47/7.75 ![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)),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f13,f13])).
% 57.47/7.75 fof(f16,plain,(
% 57.47/7.75 ![X0,X1,X2,X3]: (multiply(double_divide(inverse(X0),multiply(double_divide(X1,X2),X2)),double_divide(X1,multiply(X3,X0)))=inverse(X3))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f13,f5])).
% 57.47/7.75 fof(f17,plain,(
% 57.47/7.75 ![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))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f5,f16])).
% 57.47/7.75 fof(f19,plain,(
% 57.47/7.75 ![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))))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f16,f16])).
% 57.47/7.75 fof(f21,plain,(
% 57.47/7.75 ![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))))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f5,f19])).
% 57.47/7.75 fof(f22,plain,(
% 57.47/7.75 ![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)))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f5,f21])).
% 57.47/7.75 fof(f29,plain,(
% 57.47/7.75 ![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)),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f13,f14])).
% 57.47/7.75 fof(f70,plain,(
% 57.47/7.75 ![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)),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f15,f14])).
% 57.47/7.75 fof(f81,plain,(
% 57.47/7.75 ![X0,X1,X2,X3]: (multiply(multiply(double_divide(X0,X1),X1),inverse(X2))=multiply(multiply(double_divide(X0,X3),X3),inverse(X2)))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f22,f22])).
% 57.47/7.75 fof(f140,plain,(
% 57.47/7.75 ![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))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f81,f15])).
% 57.47/7.75 fof(f158,plain,(
% 57.47/7.75 ![X0,X1,X2]: (multiply(double_divide(X0,X1),X1)=multiply(double_divide(X0,X2),X2))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f15,f140])).
% 57.47/7.75 fof(f169,plain,(
% 57.47/7.75 ![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))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f13,f158])).
% 57.47/7.75 fof(f185,plain,(
% 57.47/7.75 ![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))))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f158,f17])).
% 57.47/7.75 fof(f192,plain,(
% 57.47/7.75 ![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)))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f158,f16])).
% 57.47/7.75 fof(f213,plain,(
% 57.47/7.75 ![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))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f5,f185])).
% 57.47/7.75 fof(f215,plain,(
% 57.47/7.75 ![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))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f5,f192])).
% 57.47/7.75 fof(f732,plain,(
% 57.47/7.75 ![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))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f16,f169])).
% 57.47/7.75 fof(f865,plain,(
% 57.47/7.75 ![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))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f5,f732])).
% 57.47/7.75 fof(f4379,plain,(
% 57.47/7.75 ![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))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f158,f213])).
% 57.47/7.75 fof(f4512,plain,(
% 57.47/7.75 ![X0,X1,X2,X3]: (multiply(double_divide(X0,double_divide(X1,X0)),X2)=multiply(double_divide(X3,double_divide(X1,X3)),X2))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f213,f4379])).
% 57.47/7.75 fof(f4554,plain,(
% 57.47/7.75 ![X0,X1,X2,X3]: (multiply(double_divide(X0,X1),X1)=multiply(double_divide(X2,double_divide(X3,X2)),double_divide(X3,X0)))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f158,f4512])).
% 57.47/7.75 fof(f4686,plain,(
% 57.47/7.75 ![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)))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f4512,f29])).
% 57.47/7.75 fof(f4815,plain,(
% 57.47/7.75 ![X0,X1,X2]: (double_divide(X0,double_divide(X1,X0))=double_divide(X2,double_divide(X1,X2)))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f29,f4686])).
% 57.47/7.75 fof(f4886,plain,(
% 57.47/7.75 ![X0,X1,X2,X3]: (double_divide(double_divide(X0,X1),double_divide(X2,double_divide(X0,X2)))=double_divide(X3,double_divide(X1,X3)))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f4815,f4815])).
% 57.47/7.75 fof(f6039,plain,(
% 57.47/7.75 ![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))))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f4554,f22])).
% 57.47/7.75 fof(f6085,plain,(
% 57.47/7.75 ![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))))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f5,f6039])).
% 57.47/7.75 fof(f6086,plain,(
% 57.47/7.75 ![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))))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f213,f6085])).
% 57.47/7.75 fof(f6087,plain,(
% 57.47/7.75 ![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)))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f5,f6086])).
% 57.47/7.75 fof(f15907,plain,(
% 57.47/7.75 ![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))))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f865,f6087])).
% 57.47/7.75 fof(f16370,plain,(
% 57.47/7.75 ![X0,X1,X2,X3]: (multiply(X0,X1)=multiply(multiply(X0,X1),multiply(X2,multiply(double_divide(X2,X3),X3))))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f865,f15907])).
% 57.47/7.75 fof(f16428,plain,(
% 57.47/7.75 ![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))))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f17,f16370])).
% 57.47/7.75 fof(f16622,plain,(
% 57.47/7.75 ![X0,X1,X2]: (inverse(X0)=multiply(inverse(X0),multiply(X1,multiply(double_divide(X1,X2),X2))))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f17,f16428])).
% 57.47/7.75 fof(f16775,plain,(
% 57.47/7.75 ![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))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f16622,f213])).
% 57.47/7.75 fof(f16808,plain,(
% 57.47/7.75 ![X0,X1,X2,X3]: (multiply(X0,X1)=multiply(double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),inverse(X0)),X1))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f215,f16775])).
% 57.47/7.75 fof(f17406,plain,(
% 57.47/7.75 ![X0,X1,X2,X3]: (multiply(X0,inverse(X0))=multiply(double_divide(multiply(X1,multiply(double_divide(X1,X2),X2)),X3),X3))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f158,f16808])).
% 57.47/7.75 fof(f17610,plain,(
% 57.47/7.75 ![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)))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f16808,f70])).
% 57.47/7.75 fof(f17729,plain,(
% 57.47/7.75 ![X0,X1,X2]: (X0=double_divide(multiply(X1,multiply(double_divide(X1,X2),X2)),inverse(X0)))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f70,f17610])).
% 57.47/7.75 fof(f18723,plain,(
% 57.47/7.75 ![X0,X1,X2,X3]: (double_divide(X0,X1)=double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),multiply(X1,X0)))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f5,f17729])).
% 57.47/7.75 fof(f22701,plain,(
% 57.47/7.75 ![X0,X1]: (multiply(X0,inverse(X0))=multiply(X1,inverse(X1)))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f17406,f17406])).
% 57.47/7.75 fof(f23018,plain,(
% 57.47/7.75 ![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)),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f17406,f13])).
% 57.47/7.75 fof(f23214,plain,(
% 57.47/7.75 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),double_divide(inverse(X0),multiply(X2,inverse(X2))))=X1)),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f18723,f23018])).
% 57.47/7.75 fof(f23341,plain,(
% 57.47/7.75 ![X0,X1,X2,X3]: (double_divide(inverse(X0),X0)=double_divide(multiply(X1,multiply(double_divide(X1,X2),X2)),multiply(X3,inverse(X3))))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f22701,f18723])).
% 57.47/7.75 fof(f23376,plain,(
% 57.47/7.75 ![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))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f22701,f213])).
% 57.47/7.75 fof(f23516,plain,(
% 57.47/7.75 ![X0,X1]: (double_divide(inverse(X0),X0)=double_divide(inverse(X1),X1))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f18723,f23341])).
% 57.47/7.75 fof(f23518,plain,(
% 57.47/7.75 ![X0,X1,X2]: (multiply(double_divide(inverse(X0),X0),X1)=multiply(double_divide(inverse(X2),X2),X1))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f213,f23376])).
% 57.47/7.75 fof(f26756,plain,(
% 57.47/7.75 ![X0,X1,X2]: (double_divide(double_divide(multiply(X0,inverse(X0)),X1),double_divide(inverse(X2),X2))=X1)),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f23516,f23214])).
% 57.47/7.75 fof(f31019,plain,(
% 57.47/7.75 ![X0,X1,X2]: (X0=multiply(X0,multiply(double_divide(multiply(X1,inverse(X1)),X2),X2)))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f13,f26756])).
% 57.47/7.75 fof(f31617,plain,(
% 57.47/7.75 ![X0,X1]: (X0=double_divide(multiply(X1,inverse(X1)),inverse(X0)))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f31019,f17729])).
% 57.47/7.75 fof(f32860,plain,(
% 57.47/7.75 ![X0,X1]: (X0=multiply(X0,multiply(X1,inverse(X1))))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f31617,f31019])).
% 57.47/7.75 fof(f32861,plain,(
% 57.47/7.75 ![X0,X1]: (double_divide(X0,double_divide(inverse(X1),X1))=inverse(X0))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f31617,f26756])).
% 57.47/7.75 fof(f32964,plain,(
% 57.47/7.75 ![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)))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f31617,f4886])).
% 57.47/7.75 fof(f33056,plain,(
% 57.47/7.75 ![X0,X1]: (X0=double_divide(X1,double_divide(X0,X1)))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f26756,f32964])).
% 57.47/7.75 fof(f33260,plain,(
% 57.47/7.75 ![X0,X1]: (multiply(double_divide(X0,X1),X1)=inverse(X0))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f33056,f5])).
% 57.47/7.75 fof(f34720,plain,(
% 57.47/7.75 ![X0,X1,X2]: (double_divide(double_divide(X0,multiply(X1,X2)),double_divide(inverse(X2),inverse(X0)))=X1)),
% 57.47/7.75 inference(backward_demodulation,[status(thm)],[f33260,f13])).
% 57.47/7.75 fof(f34866,plain,(
% 57.47/7.75 ![X0,X1]: (X0=inverse(double_divide(X1,multiply(X0,inverse(X1)))))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f34720,f32861])).
% 57.47/7.75 fof(f34898,plain,(
% 57.47/7.75 ![X0,X1]: (X0=multiply(multiply(X0,inverse(X1)),X1))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f5,f34866])).
% 57.47/7.75 fof(f34917,plain,(
% 57.47/7.75 ![X0,X1]: (double_divide(X0,inverse(X1))=multiply(inverse(X0),X1))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f33260,f34898])).
% 57.47/7.75 fof(f34919,plain,(
% 57.47/7.75 ![X0,X1]: (X0=multiply(multiply(X1,inverse(X1)),X0))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f22701,f34898])).
% 57.47/7.75 fof(f34939,plain,(
% 57.47/7.75 ![X0,X1,X2]: (X0=multiply(multiply(double_divide(inverse(X1),X1),inverse(double_divide(inverse(X2),X2))),X0))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f23518,f34919])).
% 57.47/7.75 fof(f34959,plain,(
% 57.47/7.75 ![X0,X1,X2]: (X0=multiply(multiply(double_divide(inverse(X1),X1),multiply(X2,inverse(X2))),X0))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f5,f34939])).
% 57.47/7.75 fof(f34960,plain,(
% 57.47/7.75 ![X0,X1]: (X0=multiply(double_divide(inverse(X1),X1),X0))),
% 57.47/7.75 inference(forward_demodulation,[status(thm)],[f32860,f34959])).
% 57.47/7.75 fof(f35042,plain,(
% 57.47/7.75 ![X0]: (X0=inverse(inverse(X0)))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f33260,f34960])).
% 57.47/7.75 fof(f35090,plain,(
% 57.47/7.75 ![X0,X1]: (X0=multiply(double_divide(X1,inverse(X1)),X0))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f35042,f34960])).
% 57.47/7.75 fof(f35245,plain,(
% 57.47/7.75 ![X0,X1]: (double_divide(X0,inverse(X0))=multiply(inverse(X1),X1))),
% 57.47/7.75 inference(paramodulation,[status(thm)],[f35090,f34898])).
% 57.47/7.75 fof(f36265,plain,(
% 57.47/7.75 ~multiply(inverse(a1),a1)=double_divide(b1,inverse(b1))),
% 57.47/7.75 inference(backward_demodulation,[status(thm)],[f34917,f6])).
% 58.38/7.81 fof(f36312,plain,(
% 58.38/7.81 ~double_divide(a1,inverse(a1))=double_divide(b1,inverse(b1))),
% 58.38/7.81 inference(forward_demodulation,[status(thm)],[f34917,f36265])).
% 58.38/7.81 fof(f39007,plain,(
% 58.38/7.81 ![X0,X1]: (double_divide(X0,inverse(X0))=double_divide(X1,inverse(X1)))),
% 58.38/7.81 inference(forward_demodulation,[status(thm)],[f34917,f35245])).
% 58.38/7.81 fof(f39008,plain,(
% 58.38/7.81 $false),
% 58.38/7.81 inference(backward_subsumption_resolution,[status(thm)],[f36312,f39007])).
% 58.38/7.81 % SZS output end CNFRefutation for theBenchmark.p
% 41.07/7.86 % Elapsed time: 7.491217 seconds
% 41.07/7.86 % CPU time: 59.129742 seconds
% 41.07/7.86 % Total memory used: 543.892 MB
% 41.07/7.86 % Net memory used: 539.075 MB
%------------------------------------------------------------------------------