%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP072-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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 73.93s 9.92s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP072-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n007.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Sun Sep 20 19:54:20 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 73.93/9.92 % Refutation found
% 73.93/9.92 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 73.93/9.92 % SZS output start CNFRefutation for theBenchmark
% 73.93/9.92 fof(f1,axiom,(
% 73.93/9.92 (![X,Y,Z,U]: (divide(divide(inverse(divide(X,Y)),divide(divide(Z,U),X)),divide(U,Z)) = Y ))),
% 73.93/9.92 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 73.93/9.92 fof(f2,axiom,(
% 73.93/9.92 (![X,Y]: (multiply(X,Y) = divide(X,inverse(Y)) ))),
% 73.93/9.92 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 73.93/9.92 fof(f3,negated_conjecture,(
% 73.93/9.92 ( 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)) ) ),
% 73.93/9.92 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 73.93/9.92 fof(f4,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0)),divide(X3,X2))=X1)),
% 73.93/9.92 inference(cnf_transformation,[status(thm)],[f1])).
% 73.93/9.92 fof(f5,plain,(
% 73.93/9.92 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 73.93/9.92 inference(cnf_transformation,[status(thm)],[f2])).
% 73.93/9.92 fof(f6,plain,(
% 73.93/9.92 ~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))),
% 73.93/9.92 inference(cnf_transformation,[status(thm)],[f3])).
% 73.93/9.92 fof(f7,definition,(
% 73.93/9.92 sQ0_spl <=> (multiply(inverse(a1),a1)=multiply(inverse(b1),b1))),
% 73.93/9.92 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 73.93/9.92 fof(f9,plain,(
% 73.93/9.92 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|sQ0_spl),
% 73.93/9.92 inference(component_clause,[status(thm)],[f7])).
% 73.93/9.92 fof(f10,definition,(
% 73.93/9.92 sQ1_spl <=> (multiply(multiply(inverse(b2),b2),a2)=a2)),
% 73.93/9.92 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 73.93/9.92 fof(f12,plain,(
% 73.93/9.92 ~multiply(multiply(inverse(b2),b2),a2)=a2|sQ1_spl),
% 73.93/9.92 inference(component_clause,[status(thm)],[f10])).
% 73.93/9.92 fof(f13,definition,(
% 73.93/9.92 sQ2_spl <=> (multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3)))),
% 73.93/9.92 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 73.93/9.92 fof(f15,plain,(
% 73.93/9.92 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))|sQ2_spl),
% 73.93/9.92 inference(component_clause,[status(thm)],[f13])).
% 73.93/9.92 fof(f16,plain,(
% 73.93/9.92 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 73.93/9.92 inference(split_clause,[status(thm)],[f6,f7,f10,f13])).
% 73.93/9.92 fof(f17,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4,X5]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(divide(X4,X5),X3)))),divide(X2,X1))=divide(X5,X4))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f4,f4])).
% 73.93/9.92 fof(f18,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(divide(inverse(multiply(X0,X1)),divide(divide(X2,X3),X0)),divide(X3,X2))=inverse(X1))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f5,f4])).
% 73.93/9.92 fof(f20,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(inverse(X0),X1)),multiply(divide(X2,X3),X0)),divide(X3,X2))=X1)),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f5,f4])).
% 73.93/9.92 fof(f24,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(divide(inverse(X2),X3),X0)),multiply(X3,X2))=X1)),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f5,f4])).
% 73.93/9.92 fof(f28,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(divide(inverse(multiply(inverse(X0),X1)),multiply(divide(X2,X3),X0)),divide(X3,X2))=inverse(X1))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f5,f18])).
% 73.93/9.92 fof(f31,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(divide(inverse(multiply(X0,X1)),divide(multiply(X2,X3),X0)),divide(inverse(X3),X2))=inverse(X1))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f5,f18])).
% 73.93/9.92 fof(f54,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(divide(inverse(divide(X0,X1)),divide(divide(X2,X3),divide(inverse(X4),divide(divide(X5,X6),divide(inverse(divide(X7,X4)),divide(divide(X1,X0),X7)))))),divide(X3,X2))=divide(X6,X5))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f4,f17])).
% 73.93/9.92 fof(f57,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4,X5,X6]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(divide(X3,X4),X0)),inverse(X5)))),divide(X2,X1))=divide(divide(divide(X4,X3),X6),inverse(multiply(X6,X5))))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f18,f17])).
% 73.93/9.92 fof(f63,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(divide(X4,X5),X3)))),divide(X2,X1))=divide(divide(X6,X7),divide(inverse(X8),divide(divide(X7,X6),divide(inverse(divide(X9,X8)),divide(divide(X5,X4),X9))))))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f17,f17])).
% 73.93/9.92 fof(f83,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4,X5,X6]: (divide(divide(inverse(X0),divide(divide(X1,X2),multiply(inverse(divide(divide(X3,X4),X0)),X5))),divide(X2,X1))=divide(divide(divide(X4,X3),X6),inverse(multiply(X6,X5))))),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f5,f57])).
% 73.93/9.92 fof(f84,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4,X5,X6]: (divide(divide(inverse(X0),divide(divide(X1,X2),multiply(inverse(divide(divide(X3,X4),X0)),X5))),divide(X2,X1))=multiply(divide(divide(X4,X3),X6),multiply(X6,X5)))),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f5,f83])).
% 73.93/9.92 fof(f87,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4,X5]: (divide(X0,X1)=divide(divide(X2,X3),divide(inverse(X4),divide(divide(X3,X2),divide(inverse(divide(X5,X4)),divide(divide(X0,X1),X5))))))),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f17,f63])).
% 73.93/9.92 fof(f96,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(inverse(X0),X1)),multiply(multiply(X2,X3),X0)),divide(inverse(X3),X2))=X1)),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f5,f20])).
% 73.93/9.92 fof(f97,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4,X5]: (divide(divide(inverse(divide(inverse(X0),X1)),multiply(divide(divide(X2,X3),divide(inverse(multiply(X4,X5)),divide(divide(X3,X2),X4))),X0)),inverse(X5))=X1)),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f18,f20])).
% 73.93/9.92 fof(f115,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4,X5]: (multiply(divide(inverse(divide(inverse(X0),X1)),multiply(divide(divide(X2,X3),divide(inverse(multiply(X4,X5)),divide(divide(X3,X2),X4))),X0)),X5)=X1)),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f5,f97])).
% 73.93/9.92 fof(f190,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(divide(inverse(multiply(inverse(X0),X1)),multiply(multiply(X2,X3),X0)),divide(inverse(X3),X2))=inverse(X1))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f5,f28])).
% 73.93/9.92 fof(f234,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(divide(inverse(multiply(X0,X1)),divide(multiply(inverse(X2),X3),X0)),multiply(inverse(X3),X2))=inverse(X1))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f5,f31])).
% 73.93/9.92 fof(f316,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(inverse(X0),X1)),multiply(multiply(inverse(X2),X3),X0)),multiply(inverse(X3),X2))=X1)),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f5,f96])).
% 73.93/9.92 fof(f789,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(divide(inverse(multiply(inverse(X0),X1)),multiply(multiply(inverse(X2),X3),X0)),multiply(inverse(X3),X2))=inverse(X1))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f5,f190])).
% 73.93/9.92 fof(f1369,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(divide(multiply(inverse(X0),X1),X2)),inverse(X3)),multiply(divide(multiply(inverse(X1),X0),X4),multiply(X4,X3)))=X2)),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f234,f24])).
% 73.93/9.92 fof(f1418,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4]: (divide(multiply(inverse(divide(multiply(inverse(X0),X1),X2)),X3),multiply(divide(multiply(inverse(X1),X0),X4),multiply(X4,X3)))=X2)),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f5,f1369])).
% 73.93/9.92 fof(f11911,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4]: (multiply(divide(divide(X0,X1),X2),multiply(X2,X3))=multiply(divide(divide(X0,X1),X4),multiply(X4,X3)))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f84,f84])).
% 73.93/9.92 fof(f12719,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(divide(X0,X1),multiply(X1,X2))=multiply(divide(divide(multiply(inverse(divide(multiply(inverse(X3),X4),X0)),X5),multiply(divide(multiply(inverse(X4),X3),X6),multiply(X6,X5))),X7),multiply(X7,X2)))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f1418,f11911])).
% 73.93/9.92 fof(f13014,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (multiply(divide(X0,X1),multiply(X1,X2))=multiply(divide(X0,X3),multiply(X3,X2)))),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f1418,f12719])).
% 73.93/9.92 fof(f13184,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (multiply(multiply(X0,X1),multiply(inverse(X1),X2))=multiply(divide(X0,X3),multiply(X3,X2)))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f5,f13014])).
% 73.93/9.92 fof(f18818,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(X1,X0)),divide(X2,X3))=divide(X3,X2))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f87,f54])).
% 73.93/9.92 fof(f23391,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4,X5]: (divide(divide(inverse(divide(X0,X1)),divide(X1,X0)),divide(X2,X3))=divide(divide(X3,X2),divide(inverse(divide(X4,X5)),divide(X5,X4))))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f18818,f18818])).
% 73.93/9.92 fof(f23733,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(X0,X1)=divide(divide(X0,X1),divide(inverse(divide(X2,X3)),divide(X3,X2))))),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f18818,f23391])).
% 73.93/9.92 fof(f23915,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4,X5,X6]: (divide(multiply(inverse(divide(multiply(inverse(X0),X1),X2)),X3),multiply(divide(multiply(inverse(X1),X0),X4),multiply(X4,X3)))=divide(X2,divide(inverse(divide(X5,X6)),divide(X6,X5))))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f1418,f23733])).
% 73.93/9.92 fof(f24421,plain,(
% 73.93/9.92 ![X0,X1,X2]: (X0=divide(X0,divide(inverse(divide(X1,X2)),divide(X2,X1))))),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f1418,f23915])).
% 73.93/9.92 fof(f24688,plain,(
% 73.93/9.92 ![X0,X1,X2]: (X0=divide(X0,inverse(divide(divide(X1,X2),inverse(divide(X2,X1))))))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f24421,f24421])).
% 73.93/9.92 fof(f25208,plain,(
% 73.93/9.92 ![X0,X1,X2]: (X0=multiply(X0,divide(divide(X1,X2),inverse(divide(X2,X1)))))),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f5,f24688])).
% 73.93/9.92 fof(f25209,plain,(
% 73.93/9.92 ![X0,X1,X2]: (X0=multiply(X0,multiply(divide(X1,X2),divide(X2,X1))))),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f5,f25208])).
% 73.93/9.92 fof(f26397,plain,(
% 73.93/9.92 ![X0,X1,X2]: (X0=multiply(X0,multiply(multiply(X1,X2),divide(inverse(X2),X1))))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f5,f25209])).
% 73.93/9.92 fof(f26469,plain,(
% 73.93/9.92 ![X0,X1,X2]: (X0=multiply(X0,multiply(divide(inverse(X1),X2),multiply(X2,X1))))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f5,f25209])).
% 73.93/9.92 fof(f26482,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4]: (multiply(multiply(X0,X1),inverse(X1))=multiply(divide(X0,X2),multiply(X2,multiply(divide(X3,X4),divide(X4,X3)))))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f25209,f13184])).
% 73.93/9.92 fof(f26555,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4]: (multiply(divide(X0,X1),multiply(X1,multiply(divide(X2,X3),divide(X3,X2))))=multiply(divide(X0,X4),X4))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f25209,f13014])).
% 73.93/9.92 fof(f26628,plain,(
% 73.93/9.92 ![X0,X1,X2]: (multiply(multiply(X0,X1),inverse(X1))=multiply(divide(X0,X2),X2))),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f25209,f26482])).
% 73.93/9.92 fof(f26643,plain,(
% 73.93/9.92 ![X0,X1,X2]: (multiply(divide(X0,X1),X1)=multiply(divide(X0,X2),X2))),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f25209,f26555])).
% 73.93/9.92 fof(f28269,plain,(
% 73.93/9.92 ![X0,X1,X2]: (X0=multiply(X0,divide(inverse(divide(X1,X2)),divide(X2,X1))))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f25209,f26469])).
% 73.93/9.92 fof(f28723,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(X0,divide(inverse(divide(X1,X2)),divide(X2,X1)))=multiply(multiply(X0,X3),inverse(X3)))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f26628,f28269])).
% 73.93/9.92 fof(f28724,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(X0,divide(inverse(divide(X1,X2)),divide(X2,X1)))=multiply(divide(X0,X3),X3))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f26643,f28269])).
% 73.93/9.92 fof(f29028,plain,(
% 73.93/9.92 ![X0,X1]: (X0=multiply(multiply(X0,X1),inverse(X1)))),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f24421,f28723])).
% 73.93/9.92 fof(f29029,plain,(
% 73.93/9.92 ![X0,X1]: (X0=multiply(divide(X0,X1),X1))),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f24421,f28724])).
% 73.93/9.92 fof(f30279,plain,(
% 73.93/9.92 ![X0,X1,X2]: (X0=divide(X0,multiply(divide(X1,X2),divide(X2,X1))))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f25209,f29029])).
% 73.93/9.92 fof(f31007,plain,(
% 73.93/9.92 ![X0,X1]: (divide(X0,X1)=multiply(X0,inverse(X1)))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f29029,f29028])).
% 73.93/9.92 fof(f31081,plain,(
% 73.93/9.92 ![X0,X1]: (X0=divide(multiply(X0,X1),X1))),
% 73.93/9.92 inference(backward_demodulation,[status(thm)],[f31007,f29028])).
% 73.93/9.92 fof(f31112,plain,(
% 73.93/9.92 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(inverse(X0),X1)),multiply(multiply(inverse(X2),X3),X0)),multiply(inverse(X3),X2))=inverse(inverse(X1)))),
% 73.93/9.92 inference(paramodulation,[status(thm)],[f31007,f789])).
% 73.93/9.92 fof(f31244,plain,(
% 73.93/9.92 ![X0]: (X0=inverse(inverse(X0)))),
% 73.93/9.92 inference(forward_demodulation,[status(thm)],[f316,f31112])).
% 73.93/9.92 fof(f36897,plain,(
% 73.93/9.92 ![X0,X1,X2,X3,X4]: (multiply(inverse(divide(inverse(divide(divide(inverse(multiply(X0,X1)),divide(divide(X2,X3),X0)),divide(X3,X2))),X4)),X1)=X4)),
% 73.93/9.98 inference(paramodulation,[status(thm)],[f30279,f115])).
% 73.93/9.98 fof(f37328,plain,(
% 73.93/9.98 ![X0,X1]: (multiply(inverse(divide(inverse(inverse(X0)),X1)),X0)=X1)),
% 73.93/9.98 inference(forward_demodulation,[status(thm)],[f18,f36897])).
% 73.93/9.98 fof(f37329,plain,(
% 73.93/9.98 ![X0,X1]: (multiply(inverse(divide(X0,X1)),X0)=X1)),
% 73.93/9.98 inference(forward_demodulation,[status(thm)],[f31244,f37328])).
% 73.93/9.98 fof(f39564,plain,(
% 73.93/9.98 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=X1)),
% 73.93/9.98 inference(paramodulation,[status(thm)],[f31081,f37329])).
% 73.93/9.98 fof(f39810,plain,(
% 73.93/9.98 ![X0,X1]: (multiply(X0,multiply(inverse(X0),X1))=X1)),
% 73.93/9.98 inference(paramodulation,[status(thm)],[f31244,f39564])).
% 73.93/9.98 fof(f39869,plain,(
% 73.93/9.98 ![X0,X1]: (inverse(X0)=divide(X1,multiply(X0,X1)))),
% 73.93/9.98 inference(paramodulation,[status(thm)],[f39564,f31081])).
% 73.93/9.98 fof(f40294,plain,(
% 73.93/9.98 ![X0,X1,X2]: (X0=multiply(X0,multiply(inverse(X1),multiply(multiply(X1,inverse(X2)),X2))))),
% 73.93/9.98 inference(paramodulation,[status(thm)],[f39869,f26469])).
% 73.93/9.98 fof(f40295,plain,(
% 73.93/9.98 ![X0,X1,X2]: (X0=multiply(X0,multiply(multiply(multiply(X1,inverse(X2)),X2),inverse(X1))))),
% 73.93/9.98 inference(paramodulation,[status(thm)],[f39869,f26397])).
% 73.93/9.98 fof(f40389,plain,(
% 73.93/9.98 ![X0,X1,X2]: (X0=multiply(X0,multiply(inverse(X1),multiply(divide(X1,X2),X2))))),
% 73.93/9.98 inference(forward_demodulation,[status(thm)],[f31007,f40294])).
% 73.93/9.98 fof(f40390,plain,(
% 73.93/9.98 ![X0,X1]: (X0=multiply(X0,multiply(inverse(X1),X1)))),
% 73.93/9.98 inference(forward_demodulation,[status(thm)],[f29029,f40389])).
% 73.93/9.98 fof(f40391,plain,(
% 73.93/9.98 ![X0,X1,X2]: (X0=multiply(X0,divide(multiply(multiply(X1,inverse(X2)),X2),X1)))),
% 73.93/9.98 inference(forward_demodulation,[status(thm)],[f31007,f40295])).
% 73.93/9.98 fof(f40392,plain,(
% 73.93/9.98 ![X0,X1,X2]: (X0=multiply(X0,divide(multiply(divide(X1,X2),X2),X1)))),
% 73.93/9.98 inference(forward_demodulation,[status(thm)],[f31007,f40391])).
% 73.93/9.98 fof(f40393,plain,(
% 73.93/9.98 ![X0,X1]: (X0=multiply(X0,divide(X1,X1)))),
% 73.93/9.98 inference(forward_demodulation,[status(thm)],[f29029,f40392])).
% 73.93/9.98 fof(f40469,plain,(
% 73.93/9.98 ![X0,X1]: (multiply(X0,inverse(X0))=divide(X1,X1))),
% 73.93/9.98 inference(paramodulation,[status(thm)],[f40393,f39810])).
% 73.93/9.98 fof(f40549,plain,(
% 73.93/9.98 ![X0,X1]: (divide(X0,X0)=divide(X1,X1))),
% 73.93/9.98 inference(forward_demodulation,[status(thm)],[f31007,f40469])).
% 73.93/9.98 fof(f41479,plain,(
% 73.93/9.98 ![X0,X1]: (X0=multiply(divide(X1,X1),X0))),
% 73.93/9.98 inference(paramodulation,[status(thm)],[f40549,f29029])).
% 73.93/9.98 fof(f41977,plain,(
% 73.93/9.98 ![X0,X1,X2]: (multiply(X0,X1)=multiply(divide(X0,X2),multiply(X2,X1)))),
% 73.93/9.98 inference(paramodulation,[status(thm)],[f13014,f41479])).
% 73.93/9.98 fof(f42168,plain,(
% 73.93/9.98 ![X0,X1]: (multiply(inverse(X0),X0)=multiply(inverse(X1),X1))),
% 73.93/9.98 inference(paramodulation,[status(thm)],[f40390,f39564])).
% 73.93/9.98 fof(f56526,plain,(
% 73.93/9.98 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 73.93/9.98 inference(paramodulation,[status(thm)],[f31081,f41977])).
% 73.93/9.98 fof(f70016,plain,(
% 73.93/9.98 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))|sQ2_spl),
% 73.93/9.98 inference(backward_demodulation,[status(thm)],[f56526,f15])).
% 73.93/9.98 fof(f70071,plain,(
% 73.93/9.98 $false|sQ2_spl),
% 73.93/9.98 inference(trivial_equality_resolution,[status(thm)],[f70016])).
% 73.93/9.98 fof(f70072,plain,(
% 73.93/9.98 sQ2_spl),
% 73.93/9.98 inference(contradiction_clause,[status(thm)],[f70071])).
% 73.93/9.98 fof(f70121,plain,(
% 73.93/9.98 $false|sQ0_spl),
% 73.93/9.98 inference(forward_subsumption_resolution,[status(thm)],[f9,f42168])).
% 73.93/9.98 fof(f70122,plain,(
% 73.93/9.98 sQ0_spl),
% 73.93/9.98 inference(contradiction_clause,[status(thm)],[f70121])).
% 73.93/9.98 fof(f70123,plain,(
% 73.93/9.98 ~multiply(inverse(b2),multiply(b2,a2))=a2|sQ1_spl),
% 73.93/9.98 inference(forward_demodulation,[status(thm)],[f56526,f12])).
% 73.93/9.98 fof(f70124,plain,(
% 73.93/9.98 ~a2=a2|sQ1_spl),
% 73.93/9.98 inference(forward_demodulation,[status(thm)],[f39564,f70123])).
% 73.93/9.98 fof(f70125,plain,(
% 73.93/9.98 $false|sQ1_spl),
% 73.93/9.98 inference(trivial_equality_resolution,[status(thm)],[f70124])).
% 73.93/9.98 fof(f70126,plain,(
% 73.93/9.98 sQ1_spl),
% 73.93/9.98 inference(contradiction_clause,[status(thm)],[f70125])).
% 73.93/9.98 fof(f70127,plain,(
% 73.93/9.98 $false),
% 73.93/9.98 inference(sat_refutation,[status(thm)],[f16,f70072,f70122,f70126])).
% 73.93/9.98 % SZS output end CNFRefutation for theBenchmark.p
% 2.18/10.02 % Elapsed time: 9.574998 seconds
% 2.18/10.02 % CPU time: 75.368709 seconds
% 2.18/10.02 % Total memory used: 829.992 MB
% 2.18/10.02 % Net memory used: 822.707 MB
%------------------------------------------------------------------------------