%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP094-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:37 PM UTC 2026
% Result : Unsatisfiable 0.14s 5.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP094-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n014.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Sun Sep 20 19:56:55 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 0.14/5.42 % Refutation found
% 0.14/5.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/5.42 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.42 fof(f1,axiom,(
% 0.14/5.42 (![X,Y,Z]: (divide(divide(identity,divide(X,Y)),divide(divide(Y,Z),X)) = Z ))),
% 0.14/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f2,axiom,(
% 0.14/5.42 (![X,Y]: (multiply(X,Y) = divide(X,divide(identity,Y)) ))),
% 0.14/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f3,axiom,(
% 0.14/5.42 (![X]: (inverse(X) = divide(identity,X) ))),
% 0.14/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f4,axiom,(
% 0.14/5.42 (![X]: (identity = divide(X,X) ))),
% 0.14/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f5,negated_conjecture,(
% 0.14/5.42 ( 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))| multiply(a4,b4) != multiply(b4,a4) ) ),
% 0.14/5.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.42 fof(f6,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(divide(identity,divide(X0,X1)),divide(divide(X1,X2),X0))=X2)),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/5.42 fof(f7,plain,(
% 0.14/5.42 ![X0,X1]: (multiply(X0,X1)=divide(X0,divide(identity,X1)))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/5.42 fof(f8,plain,(
% 0.14/5.42 ![X0]: (inverse(X0)=divide(identity,X0))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f3])).
% 0.14/5.42 fof(f9,plain,(
% 0.14/5.42 ![X0]: (identity=divide(X0,X0))),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/5.42 fof(f10,plain,(
% 0.14/5.42 ~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))|~multiply(a4,b4)=multiply(b4,a4)),
% 0.14/5.42 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.42 fof(f11,definition,(
% 0.14/5.42 sQ0_spl <=> (multiply(inverse(a1),a1)=multiply(inverse(b1),b1))),
% 0.14/5.42 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/5.42 fof(f13,plain,(
% 0.14/5.42 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|sQ0_spl),
% 0.14/5.42 inference(component_clause,[status(thm)],[f11])).
% 0.14/5.42 fof(f14,definition,(
% 0.14/5.42 sQ1_spl <=> (multiply(multiply(inverse(b2),b2),a2)=a2)),
% 0.14/5.42 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/5.42 fof(f16,plain,(
% 0.14/5.42 ~multiply(multiply(inverse(b2),b2),a2)=a2|sQ1_spl),
% 0.14/5.42 inference(component_clause,[status(thm)],[f14])).
% 0.14/5.42 fof(f17,definition,(
% 0.14/5.42 sQ2_spl <=> (multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3)))),
% 0.14/5.42 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/5.42 fof(f19,plain,(
% 0.14/5.42 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))|sQ2_spl),
% 0.14/5.42 inference(component_clause,[status(thm)],[f17])).
% 0.14/5.42 fof(f20,definition,(
% 0.14/5.42 sQ3_spl <=> (multiply(a4,b4)=multiply(b4,a4))),
% 0.14/5.42 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/5.42 fof(f22,plain,(
% 0.14/5.42 ~multiply(a4,b4)=multiply(b4,a4)|sQ3_spl),
% 0.14/5.42 inference(component_clause,[status(thm)],[f20])).
% 0.14/5.42 fof(f23,plain,(
% 0.14/5.42 ~sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl),
% 0.14/5.42 inference(split_clause,[status(thm)],[f10,f11,f14,f17,f20])).
% 0.14/5.42 fof(f24,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(inverse(divide(X0,X1)),divide(divide(X1,X2),X0))=X2)),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f8,f6])).
% 0.14/5.42 fof(f25,plain,(
% 0.14/5.42 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f8,f7])).
% 0.14/5.42 fof(f26,plain,(
% 0.14/5.42 inverse(identity)=identity),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f9,f8])).
% 0.14/5.42 fof(f28,plain,(
% 0.14/5.42 ![X0]: (multiply(identity,X0)=inverse(inverse(X0)))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f8,f25])).
% 0.14/5.42 fof(f33,plain,(
% 0.14/5.42 ![X0]: (multiply(X0,identity)=divide(X0,identity))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f26,f25])).
% 0.14/5.42 fof(f50,plain,(
% 0.14/5.42 ![X0,X1,X2,X3]: (divide(inverse(X0),divide(divide(divide(divide(X1,X0),X2),X3),inverse(divide(X2,X1))))=X3)),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f24,f24])).
% 0.14/5.42 fof(f51,plain,(
% 0.14/5.42 ![X0,X1]: (divide(inverse(inverse(X0)),divide(divide(X0,X1),identity))=X1)),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f8,f24])).
% 0.14/5.42 fof(f53,plain,(
% 0.14/5.42 ![X0,X1]: (divide(inverse(identity),divide(divide(X0,X1),X0))=X1)),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f9,f24])).
% 0.14/5.42 fof(f54,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(inverse(divide(inverse(X0),X1)),multiply(divide(X1,X2),X0))=X2)),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f25,f24])).
% 0.14/5.42 fof(f55,plain,(
% 0.14/5.42 ![X0,X1]: (divide(inverse(divide(divide(X0,X1),X0)),identity)=X1)),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f9,f24])).
% 0.14/5.42 fof(f58,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(inverse(divide(X0,X1)),divide(multiply(X1,X2),X0))=inverse(X2))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f25,f24])).
% 0.14/5.42 fof(f59,plain,(
% 0.14/5.42 ![X0,X1]: (divide(inverse(divide(X0,X1)),divide(identity,X0))=X1)),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f9,f24])).
% 0.14/5.42 fof(f60,plain,(
% 0.14/5.42 ![X0,X1,X2,X3]: (divide(inverse(X0),multiply(divide(divide(divide(X1,X0),X2),X3),divide(X2,X1)))=X3)),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f25,f50])).
% 0.14/5.42 fof(f61,plain,(
% 0.14/5.42 ![X0,X1]: (divide(identity,divide(divide(X0,X1),X0))=X1)),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f26,f53])).
% 0.14/5.42 fof(f62,plain,(
% 0.14/5.42 ![X0,X1]: (inverse(divide(divide(X0,X1),X0))=X1)),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f8,f61])).
% 0.14/5.42 fof(f63,plain,(
% 0.14/5.42 ![X0]: (multiply(X0,identity)=X0)),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f65,f33])).
% 0.14/5.42 fof(f64,plain,(
% 0.14/5.42 ![X0,X1]: (divide(inverse(inverse(X0)),divide(X0,X1))=X1)),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f65,f51])).
% 0.14/5.42 fof(f65,plain,(
% 0.14/5.42 ![X0]: (divide(X0,identity)=X0)),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f62,f55])).
% 0.14/5.42 fof(f68,plain,(
% 0.14/5.42 ![X0,X1]: (divide(inverse(divide(X0,X1)),inverse(X0))=X1)),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f8,f59])).
% 0.14/5.42 fof(f69,plain,(
% 0.14/5.42 ![X0,X1]: (multiply(inverse(divide(X0,X1)),X0)=X1)),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f25,f68])).
% 0.14/5.42 fof(f88,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(inverse(X0),multiply(identity,divide(X1,X2)))=divide(divide(X2,X0),X1))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f9,f60])).
% 0.14/5.42 fof(f103,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(inverse(X0),multiply(divide(divide(divide(X1,X0),X1),X2),identity))=X2)),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f9,f60])).
% 0.14/5.42 fof(f104,plain,(
% 0.14/5.42 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(X0,inverse(X1))),divide(X2,X0))=multiply(divide(divide(divide(X3,X1),X4),X2),divide(X4,X3)))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f60,f24])).
% 0.14/5.42 fof(f108,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(inverse(X0),inverse(inverse(divide(X1,X2))))=divide(divide(X2,X0),X1))),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f28,f88])).
% 0.14/5.42 fof(f109,plain,(
% 0.14/5.42 ![X0,X1,X2]: (multiply(inverse(X0),inverse(divide(X1,X2)))=divide(divide(X2,X0),X1))),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f25,f108])).
% 0.14/5.42 fof(f122,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(inverse(X0),divide(divide(divide(X1,X0),X1),X2))=X2)),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f63,f103])).
% 0.14/5.42 fof(f123,plain,(
% 0.14/5.42 ![X0,X1,X2,X3,X4]: (divide(inverse(multiply(X0,X1)),divide(X2,X0))=multiply(divide(divide(divide(X3,X1),X4),X2),divide(X4,X3)))),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f25,f104])).
% 0.14/5.42 fof(f125,plain,(
% 0.14/5.42 ![X0]: (inverse(divide(identity,X0))=X0)),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f63,f69])).
% 0.14/5.42 fof(f127,plain,(
% 0.14/5.42 ![X0,X1,X2,X3]: (multiply(inverse(X0),inverse(X1))=multiply(divide(divide(divide(X2,X1),X3),X0),divide(X3,X2)))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f60,f69])).
% 0.14/5.42 fof(f135,plain,(
% 0.14/5.42 ![X0,X1]: (divide(X0,divide(X0,X1))=X1)),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f136,f64])).
% 0.14/5.42 fof(f136,plain,(
% 0.14/5.42 ![X0]: (inverse(inverse(X0))=X0)),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f8,f125])).
% 0.14/5.42 fof(f138,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(inverse(multiply(X0,X1)),divide(X2,X0))=multiply(inverse(X2),inverse(X1)))),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f127,f123])).
% 0.14/5.42 fof(f150,plain,(
% 0.14/5.42 ![X0,X1]: (multiply(X0,inverse(X1))=divide(X0,X1))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f136,f25])).
% 0.14/5.42 fof(f151,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(inverse(X0),divide(X1,X2))=divide(divide(X2,X0),X1))),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f150,f109])).
% 0.14/5.42 fof(f155,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(inverse(multiply(X0,X1)),divide(X2,X0))=divide(inverse(X2),X1))),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f150,f138])).
% 0.14/5.42 fof(f161,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(divide(X0,divide(X0,X1)),multiply(X1,X2))=inverse(X2))),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f151,f58])).
% 0.14/5.42 fof(f163,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(divide(X0,X1),divide(divide(X2,X1),X2))=X0)),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f151,f122])).
% 0.14/5.42 fof(f165,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(divide(X0,multiply(X0,X1)),X2)=divide(inverse(X2),X1))),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f151,f155])).
% 0.14/5.42 fof(f171,plain,(
% 0.14/5.42 ![X0,X1]: (divide(inverse(X0),X1)=divide(inverse(X1),X0))),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f172,f165])).
% 0.14/5.42 fof(f172,plain,(
% 0.14/5.42 ![X0,X1]: (divide(X0,multiply(X0,X1))=inverse(X1))),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f135,f161])).
% 0.14/5.42 fof(f185,plain,(
% 0.14/5.42 ![X0,X1]: (multiply(inverse(X0),X1)=divide(X1,X0))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f135,f69])).
% 0.14/5.42 fof(f202,plain,(
% 0.14/5.42 ![X0,X1]: (inverse(divide(X0,X1))=divide(X1,X0))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f135,f62])).
% 0.14/5.42 fof(f206,plain,(
% 0.14/5.42 ![X0,X1,X2]: (multiply(X0,X1)=divide(X0,divide(divide(X2,X1),X2)))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f62,f150])).
% 0.14/5.42 fof(f213,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(divide(X0,inverse(X1)),multiply(divide(X0,X2),X1))=X2)),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f202,f54])).
% 0.14/5.42 fof(f218,plain,(
% 0.14/5.42 ![X0,X1]: (multiply(divide(X0,X1),X1)=X0)),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f206,f163])).
% 0.14/5.42 fof(f222,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(multiply(X0,X1),multiply(divide(X0,X2),X1))=X2)),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f25,f213])).
% 0.14/5.42 fof(f223,plain,(
% 0.14/5.42 ![X0,X1]: (divide(divide(X0,inverse(X1)),X1)=X0)),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f150,f218])).
% 0.14/5.42 fof(f226,plain,(
% 0.14/5.42 ![X0,X1]: (multiply(X0,divide(X1,X0))=X1)),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f135,f218])).
% 0.14/5.42 fof(f232,plain,(
% 0.14/5.42 ![X0,X1]: (divide(multiply(X0,X1),X1)=X0)),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f25,f223])).
% 0.14/5.42 fof(f250,plain,(
% 0.14/5.42 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f232,f226])).
% 0.14/5.42 fof(f258,plain,(
% 0.14/5.42 $false|sQ3_spl),
% 0.14/5.42 inference(backward_subsumption_resolution,[status(thm)],[f22,f250])).
% 0.14/5.42 fof(f261,plain,(
% 0.14/5.42 sQ3_spl),
% 0.14/5.42 inference(contradiction_clause,[status(thm)],[f258])).
% 0.14/5.42 fof(f325,plain,(
% 0.14/5.42 ![X0,X1]: (multiply(X0,X1)=divide(X1,inverse(X0)))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f136,f185])).
% 0.14/5.42 fof(f347,plain,(
% 0.14/5.42 ![X0,X1]: (inverse(multiply(X0,X1))=divide(inverse(X1),X0))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f25,f202])).
% 0.14/5.42 fof(f349,plain,(
% 0.14/5.42 ![X0,X1,X2]: (multiply(divide(X0,X1),X2)=divide(X2,divide(X1,X0)))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f202,f185])).
% 0.14/5.42 fof(f350,plain,(
% 0.14/5.42 ![X0,X1,X2]: (multiply(X0,divide(X1,X2))=divide(X0,divide(X2,X1)))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f202,f150])).
% 0.14/5.42 fof(f364,plain,(
% 0.14/5.42 ![X0,X1]: (divide(inverse(X0),X1)=inverse(multiply(X0,X1)))),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f347,f171])).
% 0.14/5.42 fof(f372,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(multiply(X0,X1),divide(X1,divide(X2,X0)))=X2)),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f349,f222])).
% 0.14/5.42 fof(f488,plain,(
% 0.14/5.42 ![X0,X1,X2]: (divide(multiply(X0,X1),X2)=divide(X1,divide(X2,X0)))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f372,f135])).
% 0.14/5.42 fof(f723,plain,(
% 0.14/5.42 ![X0,X1]: (inverse(multiply(X0,X1))=inverse(multiply(X1,X0)))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f347,f364])).
% 0.14/5.42 fof(f811,plain,(
% 0.14/5.42 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=divide(X2,inverse(multiply(X1,X0))))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f723,f325])).
% 0.14/5.42 fof(f829,plain,(
% 0.14/5.42 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(multiply(X1,X0),X2))),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f325,f811])).
% 0.14/5.42 fof(f901,plain,(
% 0.14/5.42 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=divide(X2,divide(inverse(X0),X1)))),
% 0.14/5.42 inference(paramodulation,[status(thm)],[f325,f488])).
% 0.14/5.42 fof(f934,plain,(
% 0.14/5.42 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=divide(X2,inverse(multiply(X0,X1))))),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f364,f901])).
% 0.14/5.42 fof(f935,plain,(
% 0.14/5.42 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))|sQ2_spl),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f939,f19])).
% 0.14/5.42 fof(f936,plain,(
% 0.14/5.42 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X1,multiply(X0,X2)))),
% 0.14/5.42 inference(backward_demodulation,[status(thm)],[f939,f829])).
% 0.14/5.42 fof(f939,plain,(
% 0.14/5.42 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f325,f934])).
% 0.14/5.42 fof(f980,plain,(
% 0.14/5.42 $false|sQ2_spl),
% 0.14/5.42 inference(trivial_equality_resolution,[status(thm)],[f935])).
% 0.14/5.42 fof(f981,plain,(
% 0.14/5.42 sQ2_spl),
% 0.14/5.42 inference(contradiction_clause,[status(thm)],[f980])).
% 0.14/5.42 fof(f982,plain,(
% 0.14/5.42 ~divide(a1,a1)=multiply(inverse(b1),b1)|sQ0_spl),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f185,f13])).
% 0.14/5.42 fof(f983,plain,(
% 0.14/5.42 ~identity=multiply(inverse(b1),b1)|sQ0_spl),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f9,f982])).
% 0.14/5.42 fof(f984,plain,(
% 0.14/5.42 ~identity=divide(b1,b1)|sQ0_spl),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f185,f983])).
% 0.14/5.42 fof(f985,plain,(
% 0.14/5.42 ~identity=identity|sQ0_spl),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f9,f984])).
% 0.14/5.42 fof(f986,plain,(
% 0.14/5.42 $false|sQ0_spl),
% 0.14/5.42 inference(trivial_equality_resolution,[status(thm)],[f985])).
% 0.14/5.42 fof(f987,plain,(
% 0.14/5.42 sQ0_spl),
% 0.14/5.42 inference(contradiction_clause,[status(thm)],[f986])).
% 0.14/5.42 fof(f989,plain,(
% 0.14/5.42 ~multiply(b2,multiply(inverse(b2),a2))=a2|sQ1_spl),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f936,f16])).
% 0.14/5.42 fof(f990,plain,(
% 0.14/5.42 ~multiply(b2,divide(a2,b2))=a2|sQ1_spl),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f185,f989])).
% 0.14/5.42 fof(f991,plain,(
% 0.14/5.42 ~divide(b2,divide(b2,a2))=a2|sQ1_spl),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f350,f990])).
% 0.14/5.42 fof(f992,plain,(
% 0.14/5.42 ~a2=a2|sQ1_spl),
% 0.14/5.42 inference(forward_demodulation,[status(thm)],[f135,f991])).
% 0.14/5.42 fof(f993,plain,(
% 0.14/5.42 $false|sQ1_spl),
% 0.14/5.42 inference(trivial_equality_resolution,[status(thm)],[f992])).
% 0.14/5.42 fof(f994,plain,(
% 0.14/5.42 sQ1_spl),
% 0.14/5.42 inference(contradiction_clause,[status(thm)],[f993])).
% 0.14/5.42 fof(f995,plain,(
% 0.14/5.42 $false),
% 0.14/5.42 inference(sat_refutation,[status(thm)],[f23,f261,f981,f987,f994])).
% 0.14/5.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.44 % Elapsed time: 0.071521 seconds
% 0.14/5.44 % CPU time: 0.324410 seconds
% 0.14/5.44 % Total memory used: 71.493 MB
% 0.14/5.44 % Net memory used: 70.758 MB
%------------------------------------------------------------------------------