%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP477-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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 234.44s 29.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP477-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n003.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sun Sep 20 20:15:46 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.36 % Drodi V4.1.1
% 234.44/29.97 % Refutation found
% 234.44/29.97 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 234.44/29.97 % SZS output start CNFRefutation for theBenchmark
% 234.44/29.97 fof(f1,axiom,(
% 234.44/29.97 (![A,B,C,D]: (divide(inverse(divide(divide(divide(A,B),C),divide(D,C))),divide(B,A)) = D ))),
% 234.44/29.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 234.44/29.97 fof(f2,axiom,(
% 234.44/29.97 (![A,B]: (multiply(A,B) = divide(A,inverse(B)) ))),
% 234.44/29.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 234.44/29.97 fof(f3,negated_conjecture,(
% 234.44/29.97 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 234.44/29.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 234.44/29.97 fof(f4,plain,(
% 234.44/29.97 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(divide(X0,X1),X2),divide(X3,X2))),divide(X1,X0))=X3)),
% 234.44/29.97 inference(cnf_transformation,[status(thm)],[f1])).
% 234.44/29.97 fof(f5,plain,(
% 234.44/29.97 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 234.44/29.97 inference(cnf_transformation,[status(thm)],[f2])).
% 234.44/29.97 fof(f6,plain,(
% 234.44/29.97 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 234.44/29.97 inference(cnf_transformation,[status(thm)],[f3])).
% 234.44/29.97 fof(f12,plain,(
% 234.44/29.97 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(X0,X1),X2),divide(X3,inverse(X2)))),divide(X1,X0))=X3)),
% 234.44/29.97 inference(paramodulation,[status(thm)],[f5,f4])).
% 234.44/29.97 fof(f13,plain,(
% 234.44/29.97 ![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)),
% 234.44/29.97 inference(paramodulation,[status(thm)],[f4,f4])).
% 234.44/29.97 fof(f15,plain,(
% 234.44/29.97 ![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))))),
% 234.44/29.97 inference(paramodulation,[status(thm)],[f4,f4])).
% 234.44/29.97 fof(f19,plain,(
% 234.44/29.97 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(X0,X1),X2),multiply(X3,X2))),divide(X1,X0))=X3)),
% 234.44/29.97 inference(forward_demodulation,[status(thm)],[f5,f12])).
% 234.44/29.97 fof(f20,plain,(
% 234.44/29.97 ![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)),
% 234.44/29.97 inference(forward_demodulation,[status(thm)],[f5,f13])).
% 234.44/29.97 fof(f23,plain,(
% 234.44/29.97 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(multiply(X0,X1),multiply(X2,X1))),divide(divide(X3,X4),inverse(divide(multiply(divide(X4,X3),X5),multiply(X0,X5)))))=X2)),
% 234.44/29.97 inference(paramodulation,[status(thm)],[f19,f19])).
% 234.44/29.97 fof(f32,plain,(
% 234.44/29.97 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(multiply(X0,X1),multiply(X2,X1))),multiply(divide(X3,X4),divide(multiply(divide(X4,X3),X5),multiply(X0,X5))))=X2)),
% 234.44/29.97 inference(forward_demodulation,[status(thm)],[f5,f23])).
% 234.44/29.97 fof(f86,plain,(
% 234.44/29.97 ![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)),
% 234.44/29.97 inference(paramodulation,[status(thm)],[f20,f19])).
% 234.44/29.97 fof(f103,plain,(
% 234.44/29.97 ![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)),
% 234.44/29.97 inference(forward_demodulation,[status(thm)],[f5,f86])).
% 234.44/29.97 fof(f197,plain,(
% 234.44/29.97 ![X0,X1,X2,X3]: (X0=inverse(divide(divide(divide(X1,X2),X3),divide(divide(X0,divide(X2,X1)),X3))))),
% 234.44/29.97 inference(paramodulation,[status(thm)],[f4,f15])).
% 234.44/29.97 fof(f227,plain,(
% 234.44/29.97 ![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)))),
% 234.44/29.97 inference(paramodulation,[status(thm)],[f15,f15])).
% 234.44/29.97 fof(f265,plain,(
% 234.44/29.97 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(divide(divide(divide(X0,X1),divide(X2,X3)),X4)),divide(X1,X0)),divide(X2,X3))=X4)),
% 234.44/29.97 inference(paramodulation,[status(thm)],[f15,f4])).
% 234.44/29.97 fof(f334,plain,(
% 234.44/29.97 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(X1,X2),X3),divide(divide(X0,divide(X2,X1)),inverse(X3)))))),
% 234.44/29.97 inference(paramodulation,[status(thm)],[f5,f197])).
% 234.44/29.97 fof(f363,plain,(
% 234.44/29.97 ![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)))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f197,f20])).
% 234.44/29.99 fof(f369,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(X1,X2),X3),multiply(divide(X0,divide(X2,X1)),X3))))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f5,f334])).
% 234.44/29.99 fof(f398,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(multiply(X1,X2),X3),multiply(divide(X0,divide(inverse(X2),X1)),X3))))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f5,f369])).
% 234.44/29.99 fof(f412,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(inverse(X1),X2),X3),multiply(divide(X0,multiply(X2,X1)),X3))))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f5,f369])).
% 234.44/29.99 fof(f648,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(multiply(inverse(X1),X2),X3),multiply(divide(X0,multiply(inverse(X2),X1)),X3))))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f5,f398])).
% 234.44/29.99 fof(f687,plain,(
% 234.44/29.99 ![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))))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f20,f412])).
% 234.44/29.99 fof(f698,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (inverse(divide(divide(X0,X1),divide(X2,X1)))=inverse(divide(multiply(X0,X3),multiply(X2,X3))))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f4,f687])).
% 234.44/29.99 fof(f732,plain,(
% 234.44/29.99 ![X0,X1,X2,X3,X4,X5,X6]: (inverse(divide(multiply(X0,X1),multiply(X2,X1)))=inverse(divide(multiply(divide(inverse(divide(multiply(divide(X3,X4),X5),multiply(X0,X5))),divide(X4,X3)),X6),multiply(X2,X6))))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f32,f412])).
% 234.44/29.99 fof(f779,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (inverse(divide(multiply(X0,X1),multiply(X2,X1)))=inverse(divide(multiply(X0,X3),multiply(X2,X3))))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f19,f732])).
% 234.44/29.99 fof(f2195,plain,(
% 234.44/29.99 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(multiply(multiply(inverse(X1),X2),X3),multiply(divide(X4,multiply(inverse(X2),X1)),X3)))=divide(X0,X4))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f648,f5])).
% 234.44/29.99 fof(f4157,plain,(
% 234.44/29.99 ![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)),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f265,f265])).
% 234.44/29.99 fof(f4339,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(divide(divide(X0,X1),X2),X3)),divide(X1,X0)),X2)=X3)),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f265,f4157])).
% 234.44/29.99 fof(f4417,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (multiply(divide(inverse(divide(divide(divide(X0,X1),inverse(X2)),X3)),divide(X1,X0)),X2)=X3)),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f5,f4339])).
% 234.44/29.99 fof(f4427,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (divide(divide(inverse(multiply(divide(divide(X0,X1),X2),X3)),divide(X1,X0)),X2)=inverse(X3))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f5,f4339])).
% 234.44/29.99 fof(f4571,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (multiply(divide(inverse(divide(multiply(divide(X0,X1),X2),X3)),divide(X1,X0)),X2)=X3)),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f5,f4417])).
% 234.44/29.99 fof(f6087,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (multiply(divide(inverse(divide(multiply(multiply(X0,X1),X2),X3)),divide(inverse(X1),X0)),X2)=X3)),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f5,f4571])).
% 234.44/29.99 fof(f6597,plain,(
% 234.44/29.99 ![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)),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f4427,f4339])).
% 234.44/29.99 fof(f6765,plain,(
% 234.44/29.99 ![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)),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f5,f6597])).
% 234.44/29.99 fof(f7549,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (multiply(divide(inverse(divide(multiply(multiply(inverse(X0),X1),X2),X3)),multiply(inverse(X1),X0)),X2)=X3)),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f5,f6087])).
% 234.44/29.99 fof(f53381,plain,(
% 234.44/29.99 ![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))))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f363,f7549])).
% 234.44/29.99 fof(f54169,plain,(
% 234.44/29.99 ![X0,X1,X2,X3,X4]: (divide(X0,X1)=multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(divide(X1,X0),X4))))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f7549,f53381])).
% 234.44/29.99 fof(f54508,plain,(
% 234.44/29.99 ![X0,X1,X2,X3,X4]: (divide(X0,X1)=multiply(multiply(X2,X3),divide(divide(divide(inverse(X3),X2),X4),divide(divide(X1,X0),X4))))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f5,f54169])).
% 234.44/29.99 fof(f56086,plain,(
% 234.44/29.99 ![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)),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f54508,f103])).
% 234.44/29.99 fof(f56311,plain,(
% 234.44/29.99 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(X0,X1),multiply(X2,divide(divide(X3,X4),divide(divide(X1,X0),X4))))),X3)=X2)),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f20,f56086])).
% 234.44/29.99 fof(f60900,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(X0,X1),divide(X0,X1))),divide(X2,X3))=divide(X3,X2))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f54169,f56311])).
% 234.44/29.99 fof(f61958,plain,(
% 234.44/29.99 ![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))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f6765,f60900])).
% 234.44/29.99 fof(f62591,plain,(
% 234.44/29.99 ![X0,X1,X2]: (divide(inverse(divide(X0,X0)),divide(X1,X2))=divide(X2,X1))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f6765,f61958])).
% 234.44/29.99 fof(f63150,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X0)),divide(X1,X2))=divide(divide(X2,X1),inverse(divide(X3,X3))))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f62591,f62591])).
% 234.44/29.99 fof(f63151,plain,(
% 234.44/29.99 ![X0,X1,X2]: (divide(inverse(divide(X0,X0)),multiply(X1,X2))=divide(inverse(X2),X1))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f5,f62591])).
% 234.44/29.99 fof(f63639,plain,(
% 234.44/29.99 ![X0,X1,X2]: (divide(X0,X1)=divide(divide(X0,X1),inverse(divide(X2,X2))))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f62591,f63150])).
% 234.44/29.99 fof(f63640,plain,(
% 234.44/29.99 ![X0,X1,X2]: (divide(X0,X1)=multiply(divide(X0,X1),divide(X2,X2)))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f5,f63639])).
% 234.44/29.99 fof(f63870,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(X0,X1),divide(X2,X2)),X3)),divide(X1,X0))=X3)),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f4571,f63640])).
% 234.44/29.99 fof(f63887,plain,(
% 234.44/29.99 ![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)))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f6765,f63640])).
% 234.44/29.99 fof(f63999,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (X0=inverse(divide(divide(inverse(X1),X2),multiply(divide(X0,multiply(X2,X1)),divide(X3,X3)))))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f63640,f412])).
% 234.44/29.99 fof(f64199,plain,(
% 234.44/29.99 ![X0,X1,X2]: (divide(inverse(divide(divide(X0,X1),X2)),divide(X1,X0))=X2)),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f63640,f63870])).
% 234.44/29.99 fof(f64207,plain,(
% 234.44/29.99 ![X0,X1]: (X0=multiply(X0,divide(X1,X1)))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f6765,f63887])).
% 234.44/29.99 fof(f64282,plain,(
% 234.44/29.99 ![X0,X1,X2]: (X0=inverse(divide(divide(inverse(X1),X2),divide(X0,multiply(X2,X1)))))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f63640,f63999])).
% 234.44/29.99 fof(f64390,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(multiply(X0,X1),divide(X2,X2)),X3)),divide(inverse(X1),X0))=X3)),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f6087,f64207])).
% 234.44/29.99 fof(f64404,plain,(
% 234.44/29.99 ![X0,X1]: (X0=multiply(X0,multiply(inverse(X1),X1)))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f5,f64207])).
% 234.44/29.99 fof(f64683,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (inverse(divide(multiply(X0,X1),multiply(X2,X1)))=inverse(divide(multiply(X0,divide(X3,X3)),X2)))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f64207,f779])).
% 234.44/29.99 fof(f64687,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (inverse(divide(divide(X0,X1),divide(X2,X1)))=inverse(divide(multiply(X0,divide(X3,X3)),X2)))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f64207,f698])).
% 234.44/29.99 fof(f64710,plain,(
% 234.44/29.99 ![X0,X1,X2]: (divide(inverse(divide(multiply(X0,X1),X2)),divide(inverse(X1),X0))=X2)),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f64207,f64390])).
% 234.44/29.99 fof(f64845,plain,(
% 234.44/29.99 ![X0,X1,X2]: (inverse(divide(multiply(X0,X1),multiply(X2,X1)))=inverse(divide(X0,X2)))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f64207,f64683])).
% 234.44/29.99 fof(f64849,plain,(
% 234.44/29.99 ![X0,X1,X2]: (inverse(divide(divide(X0,X1),divide(X2,X1)))=inverse(divide(X0,X2)))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f64207,f64687])).
% 234.44/29.99 fof(f194838,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (inverse(divide(divide(inverse(X0),X1),divide(X2,multiply(X1,X0))))=inverse(divide(inverse(divide(X3,X3)),X2)))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f63151,f64849])).
% 234.44/29.99 fof(f194985,plain,(
% 234.44/29.99 ![X0,X1]: (X0=inverse(divide(inverse(divide(X1,X1)),X0)))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f64282,f194838])).
% 234.44/29.99 fof(f195045,plain,(
% 234.44/29.99 ![X0,X1]: (divide(inverse(X0),X1)=inverse(multiply(X1,X0)))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f64710,f194985])).
% 234.44/29.99 fof(f195047,plain,(
% 234.44/29.99 ![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))))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f227,f194985])).
% 234.44/29.99 fof(f195186,plain,(
% 234.44/29.99 ![X0,X1,X2,X3]: (divide(X0,X1)=inverse(divide(inverse(divide(divide(X2,X3),divide(X1,X0))),divide(X3,X2))))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f64849,f195047])).
% 234.44/29.99 fof(f195187,plain,(
% 234.44/29.99 ![X0,X1]: (divide(X0,X1)=inverse(divide(X1,X0)))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f64199,f195186])).
% 234.44/29.99 fof(f195244,plain,(
% 234.44/29.99 ![X0,X1,X2]: (divide(multiply(X0,X1),multiply(X2,X1))=inverse(divide(X2,X0)))),
% 234.44/29.99 inference(backward_demodulation,[status(thm)],[f195187,f64845])).
% 234.44/29.99 fof(f195336,plain,(
% 234.44/29.99 ![X0,X1,X2]: (divide(multiply(X0,X1),multiply(X2,X1))=divide(X0,X2))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f195187,f195244])).
% 234.44/29.99 fof(f196314,plain,(
% 234.44/29.99 ![X0,X1]: (divide(inverse(multiply(inverse(X0),X0)),X1)=inverse(X1))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f64404,f195045])).
% 234.44/29.99 fof(f196329,plain,(
% 234.44/29.99 ![X0,X1]: (divide(inverse(divide(X0,X0)),X1)=inverse(X1))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f64207,f195045])).
% 234.44/29.99 fof(f196376,plain,(
% 234.44/29.99 ![X0,X1]: (divide(divide(inverse(X0),inverse(X0)),X1)=inverse(X1))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f195045,f196314])).
% 234.44/29.99 fof(f196377,plain,(
% 234.44/29.99 ![X0,X1]: (divide(multiply(inverse(X0),X0),X1)=inverse(X1))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f5,f196376])).
% 234.44/29.99 fof(f196412,plain,(
% 234.44/29.99 ![X0,X1]: (divide(divide(X0,X0),X1)=inverse(X1))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f195187,f196329])).
% 234.44/29.99 fof(f196527,plain,(
% 234.44/29.99 ![X0,X1]: (multiply(divide(X0,X0),X1)=inverse(inverse(X1)))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f5,f196412])).
% 234.44/29.99 fof(f196568,plain,(
% 234.44/29.99 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(multiply(multiply(inverse(X1),X2),X3),multiply(inverse(multiply(inverse(X2),X1)),X3)))=divide(X0,divide(X4,X4)))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f196412,f2195])).
% 234.44/29.99 fof(f196650,plain,(
% 234.44/29.99 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(multiply(multiply(inverse(X1),X2),X3),multiply(divide(inverse(X1),inverse(X2)),X3)))=divide(X0,divide(X4,X4)))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f195045,f196568])).
% 234.44/29.99 fof(f196651,plain,(
% 234.44/29.99 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(multiply(multiply(inverse(X1),X2),X3),multiply(multiply(inverse(X1),X2),X3)))=divide(X0,divide(X4,X4)))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f5,f196650])).
% 234.44/29.99 fof(f196652,plain,(
% 234.44/29.99 ![X0,X1]: (X0=divide(X0,divide(X1,X1)))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f64207,f196651])).
% 234.44/29.99 fof(f196700,plain,(
% 234.44/29.99 ![X0,X1]: (X0=divide(X0,multiply(inverse(X1),X1)))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f5,f196652])).
% 234.44/29.99 fof(f198734,plain,(
% 234.44/29.99 ![X0,X1]: (divide(X0,multiply(inverse(X1),X1))=inverse(inverse(X0)))),
% 234.44/29.99 inference(paramodulation,[status(thm)],[f196377,f195187])).
% 234.44/29.99 fof(f198885,plain,(
% 234.44/29.99 ![X0]: (X0=inverse(inverse(X0)))),
% 234.44/29.99 inference(forward_demodulation,[status(thm)],[f196700,f198734])).
% 221.07/30.14 fof(f199350,plain,(
% 221.07/30.14 ![X0,X1]: (multiply(X0,inverse(X1))=divide(X0,X1))),
% 221.07/30.14 inference(paramodulation,[status(thm)],[f198885,f5])).
% 221.07/30.14 fof(f200953,plain,(
% 221.07/30.14 ![X0,X1]: (multiply(divide(X0,X0),X1)=X1)),
% 221.07/30.14 inference(forward_demodulation,[status(thm)],[f198885,f196527])).
% 221.07/30.14 fof(f200979,plain,(
% 221.07/30.14 ![X0,X1]: (multiply(multiply(inverse(X0),X0),X1)=X1)),
% 221.07/30.14 inference(paramodulation,[status(thm)],[f196700,f200953])).
% 221.07/30.14 fof(f203420,plain,(
% 221.07/30.14 ![X0,X1,X2]: (divide(multiply(X0,X1),X1)=divide(X0,multiply(inverse(X2),X2)))),
% 221.07/30.14 inference(paramodulation,[status(thm)],[f200979,f195336])).
% 221.07/30.14 fof(f203535,plain,(
% 221.07/30.14 ![X0,X1]: (divide(multiply(X0,X1),X1)=X0)),
% 221.07/30.14 inference(forward_demodulation,[status(thm)],[f196700,f203420])).
% 221.07/30.14 fof(f204033,plain,(
% 221.07/30.14 ![X0,X1]: (multiply(multiply(X0,inverse(X1)),X1)=X0)),
% 221.07/30.14 inference(paramodulation,[status(thm)],[f5,f203535])).
% 221.07/30.14 fof(f204144,plain,(
% 221.07/30.14 ![X0,X1]: (multiply(divide(X0,X1),X1)=X0)),
% 221.07/30.14 inference(forward_demodulation,[status(thm)],[f199350,f204033])).
% 221.07/30.14 fof(f204162,plain,(
% 221.07/30.14 ![X0,X1,X2]: (multiply(divide(X0,X1),multiply(X1,X2))=multiply(X0,X2))),
% 221.07/30.14 inference(paramodulation,[status(thm)],[f195336,f204144])).
% 221.07/30.14 fof(f209365,plain,(
% 221.07/30.14 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 221.07/30.14 inference(paramodulation,[status(thm)],[f203535,f204162])).
% 221.07/30.14 fof(f210728,plain,(
% 221.07/30.14 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))),
% 221.07/30.14 inference(backward_demodulation,[status(thm)],[f209365,f6])).
% 221.07/30.14 fof(f210758,plain,(
% 221.07/30.14 $false),
% 221.07/30.14 inference(trivial_equality_resolution,[status(thm)],[f210728])).
% 221.07/30.14 % SZS output end CNFRefutation for theBenchmark.p
% 33.70/32.32 % Elapsed time: 31.951507 seconds
% 33.70/32.32 % CPU time: 253.025789 seconds
% 33.70/32.32 % Total memory used: 59.435 GB
% 33.70/32.32 % Net memory used: 59.421 GB
%------------------------------------------------------------------------------