%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP073-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:35 PM UTC 2026
% Result : Unsatisfiable 223.86s 28.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP073-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n018.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 19:58:59 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 223.86/28.69 % Refutation found
% 223.86/28.69 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 223.86/28.69 % SZS output start CNFRefutation for theBenchmark
% 223.86/28.69 fof(f1,axiom,(
% 223.86/28.69 (![X,Y,Z,U]: (divide(inverse(divide(divide(divide(X,Y),Z),divide(U,Z))),divide(Y,X)) = U ))),
% 223.86/28.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 223.86/28.69 fof(f2,axiom,(
% 223.86/28.69 (![X,Y]: (multiply(X,Y) = divide(X,inverse(Y)) ))),
% 223.86/28.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 223.86/28.69 fof(f3,negated_conjecture,(
% 223.86/28.69 ( 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)) ) ),
% 223.86/28.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 223.86/28.69 fof(f4,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(divide(X0,X1),X2),divide(X3,X2))),divide(X1,X0))=X3)),
% 223.86/28.69 inference(cnf_transformation,[status(thm)],[f1])).
% 223.86/28.69 fof(f5,plain,(
% 223.86/28.69 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 223.86/28.69 inference(cnf_transformation,[status(thm)],[f2])).
% 223.86/28.69 fof(f6,plain,(
% 223.86/28.69 ~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))),
% 223.86/28.69 inference(cnf_transformation,[status(thm)],[f3])).
% 223.86/28.69 fof(f7,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(X0,X1),X2),divide(X3,inverse(X2)))),divide(X1,X0))=X3)),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f4])).
% 223.86/28.69 fof(f8,plain,(
% 223.86/28.69 ![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)),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f4,f4])).
% 223.86/28.69 fof(f10,plain,(
% 223.86/28.69 ![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))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f4,f4])).
% 223.86/28.69 fof(f14,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(X0,X1),X2),multiply(X3,X2))),divide(X1,X0))=X3)),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f5,f7])).
% 223.86/28.69 fof(f15,plain,(
% 223.86/28.69 ![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)),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f5,f8])).
% 223.86/28.69 fof(f81,plain,(
% 223.86/28.69 ![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)),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f15,f14])).
% 223.86/28.69 fof(f98,plain,(
% 223.86/28.69 ![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)),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f5,f81])).
% 223.86/28.69 fof(f249,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (X0=inverse(divide(divide(divide(X1,X2),X3),divide(divide(X0,divide(X2,X1)),X3))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f4,f10])).
% 223.86/28.69 fof(f285,plain,(
% 223.86/28.69 ![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)))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f10,f10])).
% 223.86/28.69 fof(f328,plain,(
% 223.86/28.69 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(divide(divide(divide(X0,X1),divide(X2,X3)),X4)),divide(X1,X0)),divide(X2,X3))=X4)),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f10,f4])).
% 223.86/28.69 fof(f536,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(X1,X2),X3),divide(divide(X0,divide(X2,X1)),inverse(X3)))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f249])).
% 223.86/28.69 fof(f548,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (X0=inverse(divide(divide(multiply(X1,X2),X3),divide(divide(X0,divide(inverse(X2),X1)),X3))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f249])).
% 223.86/28.69 fof(f572,plain,(
% 223.86/28.69 ![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)))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f249,f15])).
% 223.86/28.69 fof(f582,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(X1,X2),X3),multiply(divide(X0,divide(X2,X1)),X3))))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f5,f536])).
% 223.86/28.69 fof(f620,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(multiply(X1,X2),X3),multiply(divide(X0,divide(inverse(X2),X1)),X3))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f582])).
% 223.86/28.69 fof(f638,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(inverse(X1),X2),X3),multiply(divide(X0,multiply(X2,X1)),X3))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f582])).
% 223.86/28.69 fof(f694,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (X0=inverse(divide(divide(multiply(inverse(X1),X2),X3),divide(divide(X0,multiply(inverse(X2),X1)),X3))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f548])).
% 223.86/28.69 fof(f784,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(multiply(inverse(X1),X2),X3),multiply(divide(X0,multiply(inverse(X2),X1)),X3))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f620])).
% 223.86/28.69 fof(f832,plain,(
% 223.86/28.69 ![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))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f15,f638])).
% 223.86/28.69 fof(f849,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (inverse(divide(divide(X0,X1),divide(X2,X1)))=inverse(divide(multiply(X0,X3),multiply(X2,X3))))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f4,f832])).
% 223.86/28.69 fof(f972,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (inverse(divide(multiply(X0,X1),multiply(X2,X1)))=inverse(divide(multiply(X0,X3),multiply(X2,X3))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f849,f849])).
% 223.86/28.69 fof(f2108,plain,(
% 223.86/28.69 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(divide(multiply(inverse(X1),X2),X3),divide(divide(X4,multiply(inverse(X2),X1)),X3)))=divide(X0,X4))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f694,f5])).
% 223.86/28.69 fof(f2190,plain,(
% 223.86/28.69 ![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))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f784,f5])).
% 223.86/28.69 fof(f3521,plain,(
% 223.86/28.69 ![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)),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f328,f328])).
% 223.86/28.69 fof(f3688,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(divide(divide(X0,X1),X2),X3)),divide(X1,X0)),X2)=X3)),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f328,f3521])).
% 223.86/28.69 fof(f3759,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (multiply(divide(inverse(divide(divide(divide(X0,X1),inverse(X2)),X3)),divide(X1,X0)),X2)=X3)),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f3688])).
% 223.86/28.69 fof(f3769,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (divide(divide(inverse(multiply(divide(divide(X0,X1),X2),X3)),divide(X1,X0)),X2)=inverse(X3))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f3688])).
% 223.86/28.69 fof(f3902,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (multiply(divide(inverse(divide(multiply(divide(X0,X1),X2),X3)),divide(X1,X0)),X2)=X3)),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f5,f3759])).
% 223.86/28.69 fof(f5723,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (multiply(divide(inverse(multiply(multiply(divide(X0,X1),X2),X3)),divide(X1,X0)),X2)=inverse(X3))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f3902])).
% 223.86/28.69 fof(f5756,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (multiply(divide(inverse(divide(multiply(multiply(X0,X1),X2),X3)),divide(inverse(X1),X0)),X2)=X3)),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f3902])).
% 223.86/28.69 fof(f5987,plain,(
% 223.86/28.69 ![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)),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f3769,f3688])).
% 223.86/28.69 fof(f6149,plain,(
% 223.86/28.69 ![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)),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f5,f5987])).
% 223.86/28.69 fof(f7267,plain,(
% 223.86/28.69 ![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))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5723,f638])).
% 223.86/28.69 fof(f7505,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (multiply(divide(inverse(divide(multiply(multiply(inverse(X0),X1),X2),X3)),multiply(inverse(X1),X0)),X2)=X3)),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f5756])).
% 223.86/28.69 fof(f51539,plain,(
% 223.86/28.69 ![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))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f572,f7505])).
% 223.86/28.69 fof(f52311,plain,(
% 223.86/28.69 ![X0,X1,X2,X3,X4]: (divide(X0,X1)=multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(divide(X1,X0),X4))))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f7505,f51539])).
% 223.86/28.69 fof(f52643,plain,(
% 223.86/28.69 ![X0,X1,X2,X3,X4]: (divide(X0,X1)=multiply(multiply(X2,X3),divide(divide(divide(inverse(X3),X2),X4),divide(divide(X1,X0),X4))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f52311])).
% 223.86/28.69 fof(f52817,plain,(
% 223.86/28.69 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),X1)=multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(multiply(X1,X0),X4))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f52311])).
% 223.86/28.69 fof(f56084,plain,(
% 223.86/28.69 ![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)),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f52643,f98])).
% 223.86/28.69 fof(f56309,plain,(
% 223.86/28.69 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(X0,X1),multiply(X2,divide(divide(X3,X4),divide(divide(X1,X0),X4))))),X3)=X2)),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f15,f56084])).
% 223.86/28.69 fof(f59443,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(X0,X1),divide(X0,X1))),divide(X2,X3))=divide(X3,X2))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f52311,f56309])).
% 223.86/28.69 fof(f60488,plain,(
% 223.86/28.69 ![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))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f6149,f59443])).
% 223.86/28.69 fof(f61115,plain,(
% 223.86/28.69 ![X0,X1,X2]: (divide(inverse(divide(X0,X0)),divide(X1,X2))=divide(X2,X1))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f6149,f60488])).
% 223.86/28.69 fof(f61667,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X0)),divide(X1,X2))=divide(divide(X2,X1),inverse(divide(X3,X3))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f61115,f61115])).
% 223.86/28.69 fof(f61668,plain,(
% 223.86/28.69 ![X0,X1,X2]: (divide(inverse(divide(X0,X0)),multiply(X1,X2))=divide(inverse(X2),X1))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f61115])).
% 223.86/28.69 fof(f62151,plain,(
% 223.86/28.69 ![X0,X1,X2]: (divide(X0,X1)=divide(divide(X0,X1),inverse(divide(X2,X2))))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f61115,f61667])).
% 223.86/28.69 fof(f62152,plain,(
% 223.86/28.69 ![X0,X1,X2]: (divide(X0,X1)=multiply(divide(X0,X1),divide(X2,X2)))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f5,f62151])).
% 223.86/28.69 fof(f62380,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(X0,X1),divide(X2,X2)),X3)),divide(X1,X0))=X3)),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f3902,f62152])).
% 223.86/28.69 fof(f62397,plain,(
% 223.86/28.69 ![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)))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f6149,f62152])).
% 223.86/28.69 fof(f62508,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (X0=inverse(divide(divide(inverse(X1),X2),multiply(divide(X0,multiply(X2,X1)),divide(X3,X3)))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f62152,f638])).
% 223.86/28.69 fof(f62705,plain,(
% 223.86/28.69 ![X0,X1,X2]: (divide(inverse(divide(divide(X0,X1),X2)),divide(X1,X0))=X2)),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f62152,f62380])).
% 223.86/28.69 fof(f62713,plain,(
% 223.86/28.69 ![X0,X1]: (X0=multiply(X0,divide(X1,X1)))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f6149,f62397])).
% 223.86/28.69 fof(f62788,plain,(
% 223.86/28.69 ![X0,X1,X2]: (X0=inverse(divide(divide(inverse(X1),X2),divide(X0,multiply(X2,X1)))))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f62152,f62508])).
% 223.86/28.69 fof(f62894,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(multiply(X0,X1),divide(X2,X2)),X3)),divide(inverse(X1),X0))=X3)),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5756,f62713])).
% 223.86/28.69 fof(f62908,plain,(
% 223.86/28.69 ![X0,X1]: (X0=multiply(X0,multiply(inverse(X1),X1)))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f62713])).
% 223.86/28.69 fof(f63179,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (inverse(divide(multiply(X0,X1),multiply(X2,X1)))=inverse(divide(multiply(X0,divide(X3,X3)),X2)))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f62713,f972])).
% 223.86/28.69 fof(f63190,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (inverse(divide(divide(X0,X1),divide(X2,X1)))=inverse(divide(multiply(X0,divide(X3,X3)),X2)))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f62713,f849])).
% 223.86/28.69 fof(f63211,plain,(
% 223.86/28.69 ![X0,X1,X2]: (divide(inverse(divide(multiply(X0,X1),X2)),divide(inverse(X1),X0))=X2)),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f62713,f62894])).
% 223.86/28.69 fof(f63339,plain,(
% 223.86/28.69 ![X0,X1,X2]: (inverse(divide(multiply(X0,X1),multiply(X2,X1)))=inverse(divide(X0,X2)))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f62713,f63179])).
% 223.86/28.69 fof(f63350,plain,(
% 223.86/28.69 ![X0,X1,X2]: (inverse(divide(divide(X0,X1),divide(X2,X1)))=inverse(divide(X0,X2)))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f62713,f63190])).
% 223.86/28.69 fof(f154085,plain,(
% 223.86/28.69 ![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))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f61668,f7267])).
% 223.86/28.69 fof(f154730,plain,(
% 223.86/28.69 ![X0,X1]: (inverse(divide(X0,X0))=inverse(divide(inverse(X1),inverse(X1))))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f5723,f154085])).
% 223.86/28.69 fof(f154731,plain,(
% 223.86/28.69 ![X0,X1]: (inverse(divide(X0,X0))=inverse(multiply(inverse(X1),X1)))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f5,f154730])).
% 223.86/28.69 fof(f160385,plain,(
% 223.86/28.69 ![X0,X1]: (inverse(divide(X0,X0))=inverse(inverse(divide(X1,X1))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f62713,f154731])).
% 223.86/28.69 fof(f161243,plain,(
% 223.86/28.69 ![X0,X1]: (inverse(inverse(divide(X0,X0)))=inverse(inverse(divide(X1,X1))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f160385,f160385])).
% 223.86/28.69 fof(f193207,plain,(
% 223.86/28.69 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(X0,X1)),multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(X0,X4))))=X1)),
% 223.86/28.69 inference(backward_demodulation,[status(thm)],[f63350,f15])).
% 223.86/28.69 fof(f193260,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (inverse(divide(divide(inverse(X0),X1),divide(X2,multiply(X1,X0))))=inverse(divide(inverse(divide(X3,X3)),X2)))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f61668,f63350])).
% 223.86/28.69 fof(f193407,plain,(
% 223.86/28.69 ![X0,X1]: (X0=inverse(divide(inverse(divide(X1,X1)),X0)))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f62788,f193260])).
% 223.86/28.69 fof(f193467,plain,(
% 223.86/28.69 ![X0,X1]: (divide(inverse(X0),X1)=inverse(multiply(X1,X0)))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f63211,f193407])).
% 223.86/28.69 fof(f193469,plain,(
% 223.86/28.69 ![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))))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f285,f193407])).
% 223.86/28.69 fof(f193608,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (divide(X0,X1)=inverse(divide(inverse(divide(divide(X2,X3),divide(X1,X0))),divide(X3,X2))))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f63350,f193469])).
% 223.86/28.69 fof(f193609,plain,(
% 223.86/28.69 ![X0,X1]: (divide(X0,X1)=inverse(divide(X1,X0)))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f62705,f193608])).
% 223.86/28.69 fof(f193666,plain,(
% 223.86/28.69 ![X0,X1,X2]: (divide(multiply(X0,X1),multiply(X2,X1))=inverse(divide(X2,X0)))),
% 223.86/28.69 inference(backward_demodulation,[status(thm)],[f193609,f63339])).
% 223.86/28.69 fof(f193696,plain,(
% 223.86/28.69 ![X0,X1]: (inverse(inverse(divide(X0,X0)))=inverse(divide(X1,X1)))),
% 223.86/28.69 inference(backward_demodulation,[status(thm)],[f193609,f161243])).
% 223.86/28.69 fof(f193758,plain,(
% 223.86/28.69 ![X0,X1,X2]: (divide(multiply(X0,X1),multiply(X2,X1))=divide(X0,X2))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f193609,f193666])).
% 223.86/28.69 fof(f193762,plain,(
% 223.86/28.69 ![X0,X1]: (inverse(divide(X0,X0))=inverse(divide(X1,X1)))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f193609,f193696])).
% 223.86/28.69 fof(f193763,plain,(
% 223.86/28.69 ![X0,X1]: (divide(X0,X0)=inverse(divide(X1,X1)))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f193609,f193762])).
% 223.86/28.69 fof(f193764,plain,(
% 223.86/28.69 ![X0,X1]: (divide(X0,X0)=divide(X1,X1))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f193609,f193763])).
% 223.86/28.69 fof(f193781,plain,(
% 223.86/28.69 ![X0,X1]: (multiply(inverse(X0),X0)=divide(X1,X1))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f193764])).
% 223.86/28.69 fof(f194447,plain,(
% 223.86/28.69 ![X0,X1]: (multiply(inverse(X0),X0)=multiply(inverse(X1),X1))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f193781])).
% 223.86/28.69 fof(f194736,plain,(
% 223.86/28.69 ![X0,X1]: (divide(inverse(multiply(inverse(X0),X0)),X1)=inverse(X1))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f62908,f193467])).
% 223.86/28.69 fof(f194751,plain,(
% 223.86/28.69 ![X0,X1]: (divide(inverse(divide(X0,X0)),X1)=inverse(X1))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f62713,f193467])).
% 223.86/28.69 fof(f194798,plain,(
% 223.86/28.69 ![X0,X1]: (divide(divide(inverse(X0),inverse(X0)),X1)=inverse(X1))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f193467,f194736])).
% 223.86/28.69 fof(f194799,plain,(
% 223.86/28.69 ![X0,X1]: (divide(multiply(inverse(X0),X0),X1)=inverse(X1))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f5,f194798])).
% 223.86/28.69 fof(f194834,plain,(
% 223.86/28.69 ![X0,X1]: (divide(divide(X0,X0),X1)=inverse(X1))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f193609,f194751])).
% 223.86/28.69 fof(f194837,plain,(
% 223.86/28.69 ![X0,X1]: (multiply(divide(X0,X0),X1)=inverse(inverse(X1)))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f194834])).
% 223.86/28.69 fof(f194875,plain,(
% 223.86/28.69 ![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)))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f194834,f2190])).
% 223.86/28.69 fof(f194948,plain,(
% 223.86/28.69 ![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)))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f193467,f194875])).
% 223.86/28.69 fof(f194949,plain,(
% 223.86/28.69 ![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)))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f5,f194948])).
% 223.86/28.69 fof(f194950,plain,(
% 223.86/28.69 ![X0,X1]: (X0=divide(X0,divide(X1,X1)))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f62713,f194949])).
% 223.86/28.69 fof(f194997,plain,(
% 223.86/28.69 ![X0,X1]: (X0=divide(X0,multiply(inverse(X1),X1)))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f5,f194950])).
% 223.86/28.69 fof(f195147,plain,(
% 223.86/28.69 ![X0,X1,X2,X3,X4]: (divide(divide(X0,X1),multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(X1,X4))))=X0)),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f193609,f193207])).
% 223.86/28.69 fof(f195209,plain,(
% 223.86/28.69 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,divide(divide(multiply(inverse(X1),X2),multiply(divide(X3,X4),divide(divide(divide(X4,X3),X5),divide(multiply(inverse(X2),X1),X5)))),X6))=divide(X0,X6))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f195147,f2108])).
% 223.86/28.69 fof(f195293,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(multiply(inverse(X1),X2),divide(inverse(X1),inverse(X2))),X3))=divide(X0,X3))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f52817,f195209])).
% 223.86/28.69 fof(f195294,plain,(
% 223.86/28.69 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(multiply(inverse(X1),X2),multiply(inverse(X1),X2)),X3))=divide(X0,X3))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f5,f195293])).
% 223.86/28.69 fof(f195295,plain,(
% 223.86/28.69 ![X0,X1]: (multiply(X0,inverse(X1))=divide(X0,X1))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f194834,f195294])).
% 223.86/28.69 fof(f196428,plain,(
% 223.86/28.69 ~multiply(multiply(inverse(b2),b2),a2)=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 223.86/28.69 inference(backward_subsumption_resolution,[status(thm)],[f6,f194447])).
% 223.86/28.69 fof(f197154,plain,(
% 223.86/28.69 ![X0,X1]: (divide(X0,multiply(inverse(X1),X1))=inverse(inverse(X0)))),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f194799,f193609])).
% 223.86/28.69 fof(f197300,plain,(
% 223.86/28.69 ![X0]: (X0=inverse(inverse(X0)))),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f194997,f197154])).
% 223.86/28.69 fof(f197376,plain,(
% 223.86/28.69 ![X0,X1]: (multiply(divide(X0,X0),X1)=X1)),
% 223.86/28.69 inference(forward_demodulation,[status(thm)],[f197300,f194837])).
% 223.86/28.69 fof(f197403,plain,(
% 223.86/28.69 ![X0,X1]: (multiply(multiply(inverse(X0),X0),X1)=X1)),
% 223.86/28.69 inference(paramodulation,[status(thm)],[f194997,f197376])).
% 78.22/28.83 fof(f197541,plain,(
% 78.22/28.83 ~a2=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 78.22/28.83 inference(backward_demodulation,[status(thm)],[f197403,f196428])).
% 78.22/28.83 fof(f197625,plain,(
% 78.22/28.83 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 78.22/28.83 inference(trivial_equality_resolution,[status(thm)],[f197541])).
% 78.22/28.83 fof(f198979,plain,(
% 78.22/28.83 ![X0,X1,X2]: (divide(multiply(X0,X1),X1)=divide(X0,multiply(inverse(X2),X2)))),
% 78.22/28.83 inference(paramodulation,[status(thm)],[f197403,f193758])).
% 78.22/28.83 fof(f199094,plain,(
% 78.22/28.83 ![X0,X1]: (divide(multiply(X0,X1),X1)=X0)),
% 78.22/28.83 inference(forward_demodulation,[status(thm)],[f194997,f198979])).
% 78.22/28.83 fof(f199151,plain,(
% 78.22/28.83 ![X0,X1]: (multiply(multiply(X0,inverse(X1)),X1)=X0)),
% 78.22/28.83 inference(paramodulation,[status(thm)],[f5,f199094])).
% 78.22/28.83 fof(f199258,plain,(
% 78.22/28.83 ![X0,X1]: (multiply(divide(X0,X1),X1)=X0)),
% 78.22/28.83 inference(forward_demodulation,[status(thm)],[f195295,f199151])).
% 78.22/28.83 fof(f199275,plain,(
% 78.22/28.83 ![X0,X1,X2]: (multiply(divide(X0,X1),multiply(X1,X2))=multiply(X0,X2))),
% 78.22/28.83 inference(paramodulation,[status(thm)],[f193758,f199258])).
% 78.22/28.83 fof(f203752,plain,(
% 78.22/28.83 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 78.22/28.83 inference(paramodulation,[status(thm)],[f199094,f199275])).
% 78.22/28.83 fof(f204572,plain,(
% 78.22/28.83 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))),
% 78.22/28.83 inference(backward_demodulation,[status(thm)],[f203752,f197625])).
% 78.22/28.83 fof(f204603,plain,(
% 78.22/28.83 $false),
% 78.22/28.83 inference(trivial_equality_resolution,[status(thm)],[f204572])).
% 78.22/28.83 % SZS output end CNFRefutation for theBenchmark.p
% 78.22/28.88 % Elapsed time: 28.483679 seconds
% 78.22/28.88 % CPU time: 225.519796 seconds
% 78.22/28.88 % Total memory used: 1.536 GB
% 78.22/28.88 % Net memory used: 1.514 GB
%------------------------------------------------------------------------------