%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP475-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 : n005.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:41 PM UTC 2026
% Result : Unsatisfiable 210.49s 27.00s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP475-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 20:14:04 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 210.49/27.00 % Refutation found
% 210.49/27.00 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 210.49/27.00 % SZS output start CNFRefutation for theBenchmark
% 210.49/27.00 fof(f1,axiom,(
% 210.49/27.00 (![A,B,C,D]: (divide(inverse(divide(divide(divide(A,B),C),divide(D,C))),divide(B,A)) = D ))),
% 210.49/27.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 210.49/27.00 fof(f2,axiom,(
% 210.49/27.00 (![A,B]: (multiply(A,B) = divide(A,inverse(B)) ))),
% 210.49/27.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 210.49/27.00 fof(f3,negated_conjecture,(
% 210.49/27.00 multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
% 210.49/27.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 210.49/27.00 fof(f4,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(divide(X0,X1),X2),divide(X3,X2))),divide(X1,X0))=X3)),
% 210.49/27.00 inference(cnf_transformation,[status(thm)],[f1])).
% 210.49/27.00 fof(f5,plain,(
% 210.49/27.00 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 210.49/27.00 inference(cnf_transformation,[status(thm)],[f2])).
% 210.49/27.00 fof(f6,plain,(
% 210.49/27.00 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)),
% 210.49/27.00 inference(cnf_transformation,[status(thm)],[f3])).
% 210.49/27.00 fof(f12,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(X0,X1),X2),divide(X3,inverse(X2)))),divide(X1,X0))=X3)),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f5,f4])).
% 210.49/27.00 fof(f13,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(X0,X1),divide(X2,X1))),divide(divide(X3,X4),inverse(divide(divide(divide(X4,X3),X5),divide(X0,X5)))))=X2)),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f4,f4])).
% 210.49/27.00 fof(f15,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(divide(X0,X1),divide(X2,X3)),X4)),divide(X1,X0))=inverse(divide(divide(divide(X3,X2),X5),divide(X4,X5))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f4,f4])).
% 210.49/27.00 fof(f19,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(X0,X1),X2),multiply(X3,X2))),divide(X1,X0))=X3)),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f5,f12])).
% 210.49/27.00 fof(f20,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(X0,X1),divide(X2,X1))),multiply(divide(X3,X4),divide(divide(divide(X4,X3),X5),divide(X0,X5))))=X2)),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f5,f13])).
% 210.49/27.00 fof(f86,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(divide(multiply(divide(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(X3,X2))),inverse(divide(divide(X3,X4),divide(X5,X4)))),X6),multiply(X7,X6))),X5)=X7)),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f20,f19])).
% 210.49/27.00 fof(f103,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(divide(multiply(multiply(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(X3,X2))),divide(divide(X3,X4),divide(X5,X4))),X6),multiply(X7,X6))),X5)=X7)),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f5,f86])).
% 210.49/27.00 fof(f197,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (X0=inverse(divide(divide(divide(X1,X2),X3),divide(divide(X0,divide(X2,X1)),X3))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f4,f15])).
% 210.49/27.00 fof(f227,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5,X6]: (divide(inverse(divide(divide(divide(X0,X1),divide(X2,X3)),X4)),divide(X1,X0))=divide(inverse(divide(divide(divide(X5,X6),divide(X2,X3)),X4)),divide(X6,X5)))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f15,f15])).
% 210.49/27.00 fof(f265,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(divide(divide(divide(X0,X1),divide(X2,X3)),X4)),divide(X1,X0)),divide(X2,X3))=X4)),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f15,f4])).
% 210.49/27.00 fof(f334,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(X1,X2),X3),divide(divide(X0,divide(X2,X1)),inverse(X3)))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f5,f197])).
% 210.49/27.00 fof(f363,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5]: (divide(X0,multiply(divide(X1,X2),divide(divide(divide(X2,X1),X3),divide(divide(X4,X5),X3))))=divide(X0,divide(X5,X4)))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f197,f20])).
% 210.49/27.00 fof(f369,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(X1,X2),X3),multiply(divide(X0,divide(X2,X1)),X3))))),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f5,f334])).
% 210.49/27.00 fof(f412,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(inverse(X1),X2),X3),multiply(divide(X0,multiply(X2,X1)),X3))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f5,f369])).
% 210.49/27.00 fof(f687,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5,X6]: (inverse(divide(divide(X0,X1),divide(X2,X1)))=inverse(divide(multiply(divide(inverse(divide(divide(divide(X3,X4),X5),divide(X0,X5))),divide(X4,X3)),X6),multiply(X2,X6))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f20,f412])).
% 210.49/27.00 fof(f698,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (inverse(divide(divide(X0,X1),divide(X2,X1)))=inverse(divide(multiply(X0,X3),multiply(X2,X3))))),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f4,f687])).
% 210.49/27.00 fof(f4157,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(divide(inverse(divide(divide(divide(X0,X1),X2),X3)),divide(X1,X0)),divide(divide(inverse(divide(divide(divide(X4,X5),divide(X6,X7)),X2)),divide(X5,X4)),divide(X6,X7)))=X3)),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f265,f265])).
% 210.49/27.00 fof(f4339,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(divide(divide(X0,X1),X2),X3)),divide(X1,X0)),X2)=X3)),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f265,f4157])).
% 210.49/27.00 fof(f4417,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (multiply(divide(inverse(divide(divide(divide(X0,X1),inverse(X2)),X3)),divide(X1,X0)),X2)=X3)),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f5,f4339])).
% 210.49/27.00 fof(f4427,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (divide(divide(inverse(multiply(divide(divide(X0,X1),X2),X3)),divide(X1,X0)),X2)=inverse(X3))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f5,f4339])).
% 210.49/27.00 fof(f4571,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (multiply(divide(inverse(divide(multiply(divide(X0,X1),X2),X3)),divide(X1,X0)),X2)=X3)),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f5,f4417])).
% 210.49/27.00 fof(f6053,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (multiply(divide(inverse(multiply(multiply(divide(X0,X1),X2),X3)),divide(X1,X0)),X2)=inverse(X3))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f5,f4571])).
% 210.49/27.00 fof(f6087,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (multiply(divide(inverse(divide(multiply(multiply(X0,X1),X2),X3)),divide(inverse(X1),X0)),X2)=X3)),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f5,f4571])).
% 210.49/27.00 fof(f6597,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(divide(inverse(X0),X1)),divide(divide(X2,X3),inverse(multiply(divide(divide(X3,X2),X4),X0)))),X4)=X1)),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f4427,f4339])).
% 210.49/27.00 fof(f6765,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(divide(inverse(X0),X1)),multiply(divide(X2,X3),multiply(divide(divide(X3,X2),X4),X0))),X4)=X1)),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f5,f6597])).
% 210.49/27.00 fof(f7311,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4]: (X0=inverse(divide(inverse(X1),multiply(divide(X0,multiply(divide(X2,X3),multiply(multiply(divide(X3,X2),X4),X1))),X4))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f6053,f412])).
% 210.49/27.00 fof(f7549,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (multiply(divide(inverse(divide(multiply(multiply(inverse(X0),X1),X2),X3)),multiply(inverse(X1),X0)),X2)=X3)),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f5,f6087])).
% 210.49/27.00 fof(f53381,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(divide(inverse(divide(multiply(multiply(inverse(X0),X1),X2),divide(X3,X4))),multiply(inverse(X1),X0)),X2)=multiply(divide(X5,X6),divide(divide(divide(X6,X5),X7),divide(divide(X4,X3),X7))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f363,f7549])).
% 210.49/27.00 fof(f54169,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4]: (divide(X0,X1)=multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(divide(X1,X0),X4))))),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f7549,f53381])).
% 210.49/27.00 fof(f54508,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4]: (divide(X0,X1)=multiply(multiply(X2,X3),divide(divide(divide(inverse(X3),X2),X4),divide(divide(X1,X0),X4))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f5,f54169])).
% 210.49/27.00 fof(f56086,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (divide(inverse(divide(divide(X0,X1),multiply(X2,divide(divide(divide(inverse(divide(divide(X3,X4),divide(X5,X4))),multiply(divide(X6,X7),divide(divide(divide(X7,X6),X8),divide(X3,X8)))),X9),divide(divide(X1,X0),X9))))),X5)=X2)),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f54508,f103])).
% 210.49/27.00 fof(f56311,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(X0,X1),multiply(X2,divide(divide(X3,X4),divide(divide(X1,X0),X4))))),X3)=X2)),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f20,f56086])).
% 210.49/27.00 fof(f60900,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(X0,X1),divide(X0,X1))),divide(X2,X3))=divide(X3,X2))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f54169,f56311])).
% 210.49/27.00 fof(f61958,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5,X6]: (divide(inverse(divide(X0,divide(divide(inverse(divide(inverse(X1),X0)),multiply(divide(X2,X3),multiply(divide(divide(X3,X2),X4),X1))),X4))),divide(X5,X6))=divide(X6,X5))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f6765,f60900])).
% 210.49/27.00 fof(f62591,plain,(
% 210.49/27.00 ![X0,X1,X2]: (divide(inverse(divide(X0,X0)),divide(X1,X2))=divide(X2,X1))),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f6765,f61958])).
% 210.49/27.00 fof(f63150,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X0)),divide(X1,X2))=divide(divide(X2,X1),inverse(divide(X3,X3))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f62591,f62591])).
% 210.49/27.00 fof(f63151,plain,(
% 210.49/27.00 ![X0,X1,X2]: (divide(inverse(divide(X0,X0)),multiply(X1,X2))=divide(inverse(X2),X1))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f5,f62591])).
% 210.49/27.00 fof(f63639,plain,(
% 210.49/27.00 ![X0,X1,X2]: (divide(X0,X1)=divide(divide(X0,X1),inverse(divide(X2,X2))))),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f62591,f63150])).
% 210.49/27.00 fof(f63640,plain,(
% 210.49/27.00 ![X0,X1,X2]: (divide(X0,X1)=multiply(divide(X0,X1),divide(X2,X2)))),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f5,f63639])).
% 210.49/27.00 fof(f63870,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(X0,X1),divide(X2,X2)),X3)),divide(X1,X0))=X3)),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f4571,f63640])).
% 210.49/27.00 fof(f63887,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5]: (divide(divide(inverse(divide(inverse(X0),X1)),multiply(divide(X2,X3),multiply(divide(divide(X3,X2),X4),X0))),X4)=multiply(X1,divide(X5,X5)))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f6765,f63640])).
% 210.49/27.00 fof(f63999,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (X0=inverse(divide(divide(inverse(X1),X2),multiply(divide(X0,multiply(X2,X1)),divide(X3,X3)))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f63640,f412])).
% 210.49/27.00 fof(f64199,plain,(
% 210.49/27.00 ![X0,X1,X2]: (divide(inverse(divide(divide(X0,X1),X2)),divide(X1,X0))=X2)),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f63640,f63870])).
% 210.49/27.00 fof(f64207,plain,(
% 210.49/27.00 ![X0,X1]: (X0=multiply(X0,divide(X1,X1)))),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f6765,f63887])).
% 210.49/27.00 fof(f64282,plain,(
% 210.49/27.00 ![X0,X1,X2]: (X0=inverse(divide(divide(inverse(X1),X2),divide(X0,multiply(X2,X1)))))),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f63640,f63999])).
% 210.49/27.00 fof(f64687,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (inverse(divide(divide(X0,X1),divide(X2,X1)))=inverse(divide(multiply(X0,divide(X3,X3)),X2)))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f64207,f698])).
% 210.49/27.00 fof(f64849,plain,(
% 210.49/27.00 ![X0,X1,X2]: (inverse(divide(divide(X0,X1),divide(X2,X1)))=inverse(divide(X0,X2)))),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f64207,f64687])).
% 210.49/27.00 fof(f157772,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4]: (inverse(divide(X0,X0))=inverse(divide(inverse(X1),multiply(divide(inverse(multiply(multiply(divide(X2,X3),X4),X1)),divide(X3,X2)),X4))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f63151,f7311])).
% 210.49/27.00 fof(f158426,plain,(
% 210.49/27.00 ![X0,X1]: (inverse(divide(X0,X0))=inverse(divide(inverse(X1),inverse(X1))))),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f6053,f157772])).
% 210.49/27.00 fof(f158427,plain,(
% 210.49/27.00 ![X0,X1]: (inverse(divide(X0,X0))=inverse(multiply(inverse(X1),X1)))),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f5,f158426])).
% 210.49/27.00 fof(f160401,plain,(
% 210.49/27.00 ![X0,X1]: (inverse(divide(X0,X0))=inverse(inverse(divide(X1,X1))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f64207,f158427])).
% 210.49/27.00 fof(f164820,plain,(
% 210.49/27.00 ![X0,X1]: (inverse(inverse(divide(X0,X0)))=inverse(inverse(divide(X1,X1))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f160401,f160401])).
% 210.49/27.00 fof(f194838,plain,(
% 210.49/27.00 ![X0,X1,X2,X3]: (inverse(divide(divide(inverse(X0),X1),divide(X2,multiply(X1,X0))))=inverse(divide(inverse(divide(X3,X3)),X2)))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f63151,f64849])).
% 210.49/27.00 fof(f194985,plain,(
% 210.49/27.00 ![X0,X1]: (X0=inverse(divide(inverse(divide(X1,X1)),X0)))),
% 210.49/27.00 inference(forward_demodulation,[status(thm)],[f64282,f194838])).
% 210.49/27.00 fof(f195047,plain,(
% 210.49/27.00 ![X0,X1,X2,X3,X4,X5]: (divide(X0,X1)=inverse(divide(inverse(divide(divide(divide(X2,X3),divide(X4,X5)),divide(divide(X1,X0),divide(X4,X5)))),divide(X3,X2))))),
% 210.49/27.00 inference(paramodulation,[status(thm)],[f227,f194985])).
% 210.49/27.00 fof(f195186,plain,(
% 39.99/27.21 ![X0,X1,X2,X3]: (divide(X0,X1)=inverse(divide(inverse(divide(divide(X2,X3),divide(X1,X0))),divide(X3,X2))))),
% 39.99/27.21 inference(forward_demodulation,[status(thm)],[f64849,f195047])).
% 39.99/27.21 fof(f195187,plain,(
% 39.99/27.21 ![X0,X1]: (divide(X0,X1)=inverse(divide(X1,X0)))),
% 39.99/27.21 inference(forward_demodulation,[status(thm)],[f64199,f195186])).
% 39.99/27.21 fof(f195274,plain,(
% 39.99/27.21 ![X0,X1]: (inverse(inverse(divide(X0,X0)))=inverse(divide(X1,X1)))),
% 39.99/27.21 inference(backward_demodulation,[status(thm)],[f195187,f164820])).
% 39.99/27.21 fof(f195340,plain,(
% 39.99/27.21 ![X0,X1]: (inverse(divide(X0,X0))=inverse(divide(X1,X1)))),
% 39.99/27.21 inference(forward_demodulation,[status(thm)],[f195187,f195274])).
% 39.99/27.21 fof(f195341,plain,(
% 39.99/27.21 ![X0,X1]: (divide(X0,X0)=inverse(divide(X1,X1)))),
% 39.99/27.21 inference(forward_demodulation,[status(thm)],[f195187,f195340])).
% 39.99/27.21 fof(f195342,plain,(
% 39.99/27.21 ![X0,X1]: (divide(X0,X0)=divide(X1,X1))),
% 39.99/27.21 inference(forward_demodulation,[status(thm)],[f195187,f195341])).
% 39.99/27.21 fof(f195359,plain,(
% 39.99/27.21 ![X0,X1]: (multiply(inverse(X0),X0)=divide(X1,X1))),
% 39.99/27.21 inference(paramodulation,[status(thm)],[f5,f195342])).
% 39.99/27.21 fof(f196029,plain,(
% 39.99/27.21 ![X0]: (~multiply(inverse(a1),a1)=divide(X0,X0))),
% 39.99/27.21 inference(paramodulation,[status(thm)],[f195359,f6])).
% 39.99/27.21 fof(f196222,plain,(
% 39.99/27.21 $false),
% 39.99/27.21 inference(forward_subsumption_resolution,[status(thm)],[f196029,f195359])).
% 39.99/27.21 % SZS output end CNFRefutation for theBenchmark.p
% 39.99/27.25 % Elapsed time: 26.871616 seconds
% 39.99/27.25 % CPU time: 212.833849 seconds
% 39.99/27.25 % Total memory used: 1.342 GB
% 39.99/27.25 % Net memory used: 1.321 GB
%------------------------------------------------------------------------------