%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP103-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 : 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:35:38 PM UTC 2026
% Result : Unsatisfiable 0.95s 0.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP103-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n003.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sun Sep 20 19:59:00 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.45 % Drodi V4.1.1
% 0.95/0.88 % Refutation found
% 0.95/0.88 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.95/0.88 % SZS output start CNFRefutation for theBenchmark
% 0.95/0.88 fof(f1,axiom,(
% 0.95/0.88 (![X,Y,Z]: (double_divide(double_divide(X,double_divide(double_divide(identity,Y),double_divide(Z,double_divide(Y,X)))),double_divide(identity,identity)) = Z ))),
% 0.95/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.95/0.88 fof(f2,axiom,(
% 0.95/0.88 (![X,Y]: (multiply(X,Y) = double_divide(double_divide(Y,X),identity) ))),
% 0.95/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.95/0.88 fof(f3,axiom,(
% 0.95/0.88 (![X]: (inverse(X) = double_divide(X,identity) ))),
% 0.95/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.95/0.88 fof(f4,axiom,(
% 0.95/0.88 (![X]: (identity = double_divide(X,inverse(X)) ))),
% 0.95/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.95/0.88 fof(f5,negated_conjecture,(
% 0.95/0.88 ( multiply(inverse(a1),a1) != identity| multiply(identity,a2) != a2| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))| multiply(a4,b4) != multiply(b4,a4) ) ),
% 0.95/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.95/0.88 fof(f6,plain,(
% 0.95/0.88 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))),double_divide(identity,identity))=X2)),
% 0.95/0.88 inference(cnf_transformation,[status(thm)],[f1])).
% 0.95/0.88 fof(f7,plain,(
% 0.95/0.88 ![X0,X1]: (multiply(X0,X1)=double_divide(double_divide(X1,X0),identity))),
% 0.95/0.88 inference(cnf_transformation,[status(thm)],[f2])).
% 0.95/0.88 fof(f8,plain,(
% 0.95/0.88 ![X0]: (inverse(X0)=double_divide(X0,identity))),
% 0.95/0.88 inference(cnf_transformation,[status(thm)],[f3])).
% 0.95/0.88 fof(f9,plain,(
% 0.95/0.88 ![X0]: (identity=double_divide(X0,inverse(X0)))),
% 0.95/0.88 inference(cnf_transformation,[status(thm)],[f4])).
% 0.95/0.88 fof(f10,plain,(
% 0.95/0.88 ~multiply(inverse(a1),a1)=identity|~multiply(identity,a2)=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))|~multiply(a4,b4)=multiply(b4,a4)),
% 0.95/0.88 inference(cnf_transformation,[status(thm)],[f5])).
% 0.95/0.88 fof(f11,definition,(
% 0.95/0.88 sQ0_spl <=> (multiply(inverse(a1),a1)=identity)),
% 0.95/0.88 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.95/0.88 fof(f13,plain,(
% 0.95/0.88 ~multiply(inverse(a1),a1)=identity|sQ0_spl),
% 0.95/0.88 inference(component_clause,[status(thm)],[f11])).
% 0.95/0.88 fof(f14,definition,(
% 0.95/0.88 sQ1_spl <=> (multiply(identity,a2)=a2)),
% 0.95/0.88 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.95/0.88 fof(f16,plain,(
% 0.95/0.88 ~multiply(identity,a2)=a2|sQ1_spl),
% 0.95/0.88 inference(component_clause,[status(thm)],[f14])).
% 0.95/0.88 fof(f17,definition,(
% 0.95/0.88 sQ2_spl <=> (multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3)))),
% 0.95/0.88 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.95/0.88 fof(f19,plain,(
% 0.95/0.88 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))|sQ2_spl),
% 0.95/0.88 inference(component_clause,[status(thm)],[f17])).
% 0.95/0.88 fof(f20,definition,(
% 0.95/0.88 sQ3_spl <=> (multiply(a4,b4)=multiply(b4,a4))),
% 0.95/0.88 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.95/0.88 fof(f22,plain,(
% 0.95/0.88 ~multiply(a4,b4)=multiply(b4,a4)|sQ3_spl),
% 0.95/0.88 inference(component_clause,[status(thm)],[f20])).
% 0.95/0.88 fof(f23,plain,(
% 0.95/0.88 ~sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl),
% 0.95/0.88 inference(split_clause,[status(thm)],[f10,f11,f14,f17,f20])).
% 0.95/0.88 fof(f24,plain,(
% 0.95/0.88 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))),inverse(identity))=X2)),
% 0.95/0.88 inference(backward_demodulation,[status(thm)],[f8,f6])).
% 0.95/0.88 fof(f25,plain,(
% 0.95/0.88 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 0.95/0.88 inference(backward_demodulation,[status(thm)],[f8,f7])).
% 0.95/0.88 fof(f26,plain,(
% 0.95/0.88 ![X0]: (multiply(inverse(X0),X0)=inverse(identity))),
% 0.95/0.88 inference(paramodulation,[status(thm)],[f9,f25])).
% 0.95/0.88 fof(f27,plain,(
% 0.95/0.88 ![X0]: (multiply(identity,X0)=inverse(inverse(X0)))),
% 0.95/0.88 inference(paramodulation,[status(thm)],[f8,f25])).
% 0.95/0.88 fof(f28,plain,(
% 0.95/0.88 ![X0,X1]: (identity=double_divide(double_divide(X0,X1),multiply(X1,X0)))),
% 0.95/0.88 inference(paramodulation,[status(thm)],[f25,f9])).
% 0.95/0.88 fof(f30,plain,(
% 0.95/0.88 ![X0,X1]: (double_divide(double_divide(X0,double_divide(identity,double_divide(X1,double_divide(inverse(identity),X0)))),inverse(identity))=X1)),
% 0.95/0.88 inference(paramodulation,[status(thm)],[f9,f24])).
% 0.95/0.88 fof(f32,plain,(
% 0.95/0.88 ![X0,X1,X2,X3]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0))))),double_divide(X3,X2))),inverse(identity))=X3)),
% 0.95/0.88 inference(paramodulation,[status(thm)],[f24,f24])).
% 0.95/0.88 fof(f33,plain,(
% 0.95/0.88 ![X0,X1]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X0),double_divide(X1,identity))),inverse(identity))=X1)),
% 0.95/0.88 inference(paramodulation,[status(thm)],[f9,f24])).
% 0.95/0.88 fof(f34,plain,(
% 0.95/0.88 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(identity,X0),double_divide(X1,inverse(X0)))),inverse(identity))=X1)),
% 0.95/0.88 inference(paramodulation,[status(thm)],[f8,f24])).
% 0.95/0.88 fof(f36,plain,(
% 0.95/0.88 ![X0,X1]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X0),inverse(X1))),inverse(identity))=X1)),
% 0.95/0.88 inference(forward_demodulation,[status(thm)],[f8,f33])).
% 0.95/0.88 fof(f37,plain,(
% 0.95/0.88 ![X0]: (multiply(identity,inverse(X0))=inverse(multiply(identity,X0)))),
% 0.95/0.88 inference(paramodulation,[status(thm)],[f27,f27])).
% 0.95/0.88 fof(f38,plain,(
% 0.95/0.88 ![X0,X1]: (multiply(identity,double_divide(X0,X1))=inverse(multiply(X1,X0)))),
% 0.95/0.88 inference(paramodulation,[status(thm)],[f25,f27])).
% 0.95/0.88 fof(f40,plain,(
% 0.95/0.88 ![X0]: (identity=double_divide(inverse(X0),multiply(identity,X0)))),
% 0.95/0.88 inference(paramodulation,[status(thm)],[f27,f9])).
% 0.95/0.88 fof(f56,plain,(
% 0.95/0.88 ![X0,X1]: (double_divide(double_divide(multiply(identity,X0),double_divide(double_divide(identity,inverse(X0)),double_divide(X1,identity))),inverse(identity))=X1)),
% 0.95/0.88 inference(paramodulation,[status(thm)],[f40,f24])).
% 0.95/0.88 fof(f60,plain,(
% 0.95/0.88 ![X0,X1]: (double_divide(double_divide(multiply(identity,X0),double_divide(double_divide(identity,inverse(X0)),inverse(X1))),inverse(identity))=X1)),
% 0.95/0.88 inference(forward_demodulation,[status(thm)],[f8,f56])).
% 0.95/0.88 fof(f118,plain,(
% 0.95/0.88 ![X0,X1,X2,X3]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(multiply(X2,X3),double_divide(X1,X0))))),identity)),inverse(identity))=double_divide(X3,X2))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f28,f32])).
% 0.95/0.89 fof(f130,plain,(
% 0.95/0.89 ![X0,X1,X2,X3]: (double_divide(double_divide(inverse(identity),inverse(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(multiply(X2,X3),double_divide(X1,X0))))))),inverse(identity))=double_divide(X3,X2))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f118])).
% 0.95/0.89 fof(f132,plain,(
% 0.95/0.89 ![X0,X1,X2,X3]: (double_divide(double_divide(inverse(identity),multiply(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(multiply(X2,X3),double_divide(X1,X0)))),identity)),inverse(identity))=double_divide(X3,X2))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f130])).
% 0.95/0.89 fof(f168,plain,(
% 0.95/0.89 ![X0]: (double_divide(double_divide(inverse(X0),identity),inverse(identity))=double_divide(identity,X0))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f9,f36])).
% 0.95/0.89 fof(f175,plain,(
% 0.95/0.89 ![X0,X1,X2,X3]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(inverse(identity),double_divide(X1,X0))))),X2)),inverse(identity))=double_divide(inverse(X3),double_divide(double_divide(identity,X3),inverse(X2))))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f36,f32])).
% 0.95/0.89 fof(f188,plain,(
% 0.95/0.89 ![X0]: (double_divide(inverse(inverse(X0)),inverse(identity))=double_divide(identity,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f168])).
% 0.95/0.89 fof(f189,plain,(
% 0.95/0.89 ![X0]: (double_divide(multiply(identity,X0),inverse(identity))=double_divide(identity,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f27,f188])).
% 0.95/0.89 fof(f208,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),inverse(identity))=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f34,f34])).
% 0.95/0.89 fof(f209,plain,(
% 0.95/0.89 ![X0,X1,X2,X3]: (double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),inverse(identity))=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1))))),double_divide(X0,X3))))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f32,f34])).
% 0.95/0.89 fof(f212,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),inverse(identity))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(inverse(identity),X1)))))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f30,f34])).
% 0.95/0.89 fof(f213,plain,(
% 0.95/0.89 ![X0,X1,X2]: (double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),inverse(identity))=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f24,f34])).
% 0.95/0.89 fof(f214,plain,(
% 0.95/0.89 ![X0]: (double_divide(double_divide(identity,double_divide(double_divide(identity,X0),identity)),inverse(identity))=X0)),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f9,f34])).
% 0.95/0.89 fof(f216,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(identity,inverse(X0)),double_divide(X1,multiply(identity,X0)))),inverse(identity))=X1)),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f27,f34])).
% 0.95/0.89 fof(f225,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(inverse(identity),double_divide(identity,double_divide(double_divide(identity,X0),double_divide(X1,inverse(X0)))))=inverse(X1))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f34,f25])).
% 0.95/0.89 fof(f227,plain,(
% 0.95/0.89 ![X0]: (double_divide(double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)),inverse(identity))=X0)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f229,f34])).
% 0.95/0.89 fof(f229,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f208])).
% 0.95/0.89 fof(f235,plain,(
% 0.95/0.89 ![X0,X1,X2,X3]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1))))),double_divide(X0,X3))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f209])).
% 0.95/0.89 fof(f248,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(inverse(identity),X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f212])).
% 0.95/0.89 fof(f251,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),inverse(identity))),X0)),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f257,f175])).
% 0.95/0.89 fof(f254,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(inverse(identity),multiply(double_divide(double_divide(identity,double_divide(inverse(identity),multiply(X0,X1))),inverse(identity)),identity)),inverse(identity))=double_divide(X1,X0))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f257,f132])).
% 0.95/0.89 fof(f255,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),inverse(identity))),double_divide(X0,X1))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f257,f235])).
% 0.95/0.89 fof(f257,plain,(
% 0.95/0.89 ![X0,X1,X2]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f213])).
% 0.95/0.89 fof(f258,plain,(
% 0.95/0.89 ![X0]: (double_divide(double_divide(identity,inverse(double_divide(identity,X0))),inverse(identity))=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f214])).
% 0.95/0.89 fof(f259,plain,(
% 0.95/0.89 ![X0]: (double_divide(double_divide(identity,multiply(X0,identity)),inverse(identity))=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f258])).
% 0.95/0.89 fof(f271,plain,(
% 0.95/0.89 ![X0]: (multiply(inverse(identity),double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)))=inverse(X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f229,f225])).
% 0.95/0.89 fof(f310,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(inverse(multiply(X0,X1)),inverse(identity))=double_divide(identity,double_divide(X1,X0)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f38,f189])).
% 0.95/0.89 fof(f314,plain,(
% 0.95/0.89 ![X0]: (multiply(inverse(identity),multiply(identity,X0))=inverse(double_divide(identity,X0)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f189,f25])).
% 0.95/0.89 fof(f319,plain,(
% 0.95/0.89 ![X0]: (multiply(inverse(identity),multiply(identity,X0))=multiply(X0,identity))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f314])).
% 0.95/0.89 fof(f360,plain,(
% 0.95/0.89 double_divide(double_divide(identity,inverse(identity)),inverse(identity))=inverse(identity)),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f26,f259])).
% 0.95/0.89 fof(f361,plain,(
% 0.95/0.89 ![X0]: (double_divide(double_divide(inverse(multiply(X0,identity)),X0),inverse(identity))=identity)),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f259,f36])).
% 0.95/0.89 fof(f367,plain,(
% 0.95/0.89 double_divide(identity,inverse(identity))=inverse(identity)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f9,f360])).
% 0.95/0.89 fof(f368,plain,(
% 0.95/0.89 ![X0]: (double_divide(double_divide(identity,multiply(X0,identity)),identity)=X0)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f259])).
% 0.95/0.89 fof(f370,plain,(
% 0.95/0.89 ![X0]: (double_divide(multiply(identity,X0),identity)=double_divide(identity,X0))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f189])).
% 0.95/0.89 fof(f371,plain,(
% 0.95/0.89 ![X0]: (double_divide(double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)),identity)=X0)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f227])).
% 0.95/0.89 fof(f373,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X0),inverse(X1))),identity)=X1)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f36])).
% 0.95/0.89 fof(f375,plain,(
% 0.95/0.89 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f26])).
% 0.95/0.89 fof(f378,plain,(
% 0.95/0.89 ![X0]: (multiply(identity,multiply(identity,X0))=multiply(X0,identity))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f319])).
% 0.95/0.89 fof(f379,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(inverse(multiply(X0,X1)),identity)=double_divide(identity,double_divide(X1,X0)))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f310])).
% 0.95/0.89 fof(f381,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f255])).
% 0.95/0.89 fof(f382,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(inverse(identity),multiply(double_divide(double_divide(identity,double_divide(inverse(identity),multiply(X0,X1))),inverse(identity)),identity)),identity)=double_divide(X1,X0))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f254])).
% 0.95/0.89 fof(f384,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),inverse(identity))),X0)),identity)=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f251])).
% 0.95/0.89 fof(f385,plain,(
% 0.95/0.89 ![X0]: (multiply(inverse(identity),double_divide(double_divide(identity,double_divide(inverse(identity),X0)),identity))=inverse(X0))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f271])).
% 0.95/0.89 fof(f388,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(identity,inverse(X0)),double_divide(X1,multiply(identity,X0)))),identity)=X1)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f216])).
% 0.95/0.89 fof(f390,plain,(
% 0.95/0.89 ![X0,X1,X2]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),identity)=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f257])).
% 0.95/0.89 fof(f391,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f248])).
% 0.95/0.89 fof(f394,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(inverse(identity),X0)),identity)=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f229])).
% 0.95/0.89 fof(f411,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(multiply(identity,X0),double_divide(double_divide(identity,inverse(X0)),inverse(X1))),identity)=X1)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f412,f60])).
% 0.95/0.89 fof(f412,plain,(
% 0.95/0.89 identity=inverse(identity)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f9,f367])).
% 0.95/0.89 fof(f413,plain,(
% 0.95/0.89 ![X0]: (double_divide(double_divide(inverse(multiply(X0,identity)),X0),identity)=identity)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f361])).
% 0.95/0.89 fof(f414,plain,(
% 0.95/0.89 ![X0]: (inverse(double_divide(inverse(multiply(X0,identity)),X0))=identity)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f413])).
% 0.95/0.89 fof(f415,plain,(
% 0.95/0.89 ![X0]: (multiply(X0,inverse(multiply(X0,identity)))=identity)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f414])).
% 0.95/0.89 fof(f434,plain,(
% 0.95/0.89 ![X0]: (inverse(double_divide(identity,multiply(X0,identity)))=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f368])).
% 0.95/0.89 fof(f437,plain,(
% 0.95/0.89 ![X0]: (multiply(multiply(X0,identity),identity)=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f434])).
% 0.95/0.89 fof(f440,plain,(
% 0.95/0.89 ![X0]: (multiply(identity,inverse(X0))=double_divide(identity,X0))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f441,f37])).
% 0.95/0.89 fof(f441,plain,(
% 0.95/0.89 ![X0]: (inverse(multiply(identity,X0))=double_divide(identity,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f370])).
% 0.95/0.89 fof(f442,plain,(
% 0.95/0.89 ![X0]: (inverse(double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)))=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f371])).
% 0.95/0.89 fof(f443,plain,(
% 0.95/0.89 ![X0]: (multiply(inverse(identity),double_divide(identity,double_divide(inverse(identity),X0)))=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f442])).
% 0.95/0.89 fof(f444,plain,(
% 0.95/0.89 ![X0]: (multiply(identity,double_divide(identity,double_divide(inverse(identity),X0)))=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f443])).
% 0.95/0.89 fof(f445,plain,(
% 0.95/0.89 ![X0]: (inverse(multiply(double_divide(inverse(identity),X0),identity))=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f38,f444])).
% 0.95/0.89 fof(f446,plain,(
% 0.95/0.89 ![X0]: (inverse(multiply(double_divide(identity,X0),identity))=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f445])).
% 0.95/0.89 fof(f447,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(double_divide(inverse(X0),double_divide(double_divide(identity,X0),inverse(X1))))=X1)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f373])).
% 0.95/0.89 fof(f448,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(double_divide(identity,X0),inverse(X1)),inverse(X0))=X1)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f447])).
% 0.95/0.89 fof(f454,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(inverse(multiply(X0,X1)))=double_divide(identity,double_divide(X1,X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f379])).
% 0.95/0.89 fof(f455,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,double_divide(X0,identity))=multiply(X0,identity))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f456,f378])).
% 0.95/0.89 fof(f456,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(identity,multiply(X0,X1))=double_divide(identity,double_divide(X1,X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f27,f454])).
% 0.95/0.89 fof(f460,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(identity,X0)),inverse(identity))=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f381])).
% 0.95/0.89 fof(f461,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(identity,X0)),identity)=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f460])).
% 0.95/0.89 fof(f462,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(double_divide(identity,double_divide(identity,X0)))=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f461])).
% 0.95/0.89 fof(f463,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f462])).
% 0.95/0.89 fof(f464,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f463])).
% 0.95/0.89 fof(f465,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(double_divide(identity,inverse(double_divide(identity,double_divide(inverse(identity),X1)))),double_divide(X0,X1))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f464])).
% 0.95/0.89 fof(f466,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(inverse(identity),X1),identity)),double_divide(X0,X1))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f465])).
% 0.95/0.89 fof(f467,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,X1),identity)),double_divide(X0,X1))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f466])).
% 0.95/0.89 fof(f468,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(double_divide(inverse(identity),multiply(double_divide(double_divide(identity,double_divide(inverse(identity),multiply(X0,X1))),inverse(identity)),identity)))=double_divide(X1,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f382])).
% 0.95/0.89 fof(f469,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(multiply(double_divide(double_divide(identity,double_divide(inverse(identity),multiply(X0,X1))),inverse(identity)),identity),inverse(identity))=double_divide(X1,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f468])).
% 0.95/0.89 fof(f470,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(multiply(double_divide(double_divide(identity,double_divide(identity,multiply(X0,X1))),inverse(identity)),identity),inverse(identity))=double_divide(X1,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f469])).
% 0.95/0.89 fof(f471,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(multiply(double_divide(double_divide(identity,double_divide(identity,multiply(X0,X1))),identity),identity),inverse(identity))=double_divide(X1,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f470])).
% 0.95/0.89 fof(f472,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(multiply(inverse(double_divide(identity,double_divide(identity,multiply(X0,X1)))),identity),inverse(identity))=double_divide(X1,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f471])).
% 0.95/0.89 fof(f473,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(multiply(multiply(double_divide(identity,multiply(X0,X1)),identity),identity),inverse(identity))=double_divide(X1,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f472])).
% 0.95/0.89 fof(f474,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(identity,multiply(X0,X1)),inverse(identity))=double_divide(X1,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f437,f473])).
% 0.95/0.89 fof(f475,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(identity,multiply(X0,X1)),identity)=double_divide(X1,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f474])).
% 0.95/0.89 fof(f484,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),inverse(identity))),X0)))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f384])).
% 0.95/0.89 fof(f485,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),inverse(identity))),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f484])).
% 0.95/0.89 fof(f486,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(identity,inverse(identity))),inverse(identity))),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f485])).
% 0.95/0.89 fof(f487,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(double_divide(identity,double_divide(double_divide(identity,identity),inverse(identity))),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f9,f486])).
% 0.95/0.89 fof(f488,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f487])).
% 0.95/0.89 fof(f489,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(double_divide(identity,double_divide(identity,inverse(identity))),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f488])).
% 0.95/0.89 fof(f490,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(double_divide(identity,identity),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f9,f489])).
% 0.95/0.89 fof(f491,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(inverse(identity),X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f490])).
% 0.95/0.89 fof(f492,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(identity,X0),inverse(identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f491])).
% 0.95/0.89 fof(f493,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f492])).
% 0.95/0.89 fof(f494,plain,(
% 0.95/0.89 ![X0]: (multiply(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X0)),identity))=inverse(X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f385])).
% 0.95/0.89 fof(f495,plain,(
% 0.95/0.89 ![X0]: (inverse(multiply(identity,double_divide(identity,double_divide(inverse(identity),X0))))=inverse(X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f38,f494])).
% 0.95/0.89 fof(f496,plain,(
% 0.95/0.89 ![X0]: (multiply(identity,inverse(double_divide(identity,double_divide(inverse(identity),X0))))=inverse(X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f37,f495])).
% 0.95/0.89 fof(f497,plain,(
% 0.95/0.89 ![X0]: (multiply(identity,multiply(double_divide(inverse(identity),X0),identity))=inverse(X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f496])).
% 0.95/0.89 fof(f498,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,double_divide(identity,double_divide(inverse(identity),X0)))=inverse(X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f456,f497])).
% 0.95/0.89 fof(f499,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,double_divide(identity,double_divide(identity,X0)))=inverse(X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f498])).
% 0.95/0.89 fof(f515,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(double_divide(identity,double_divide(double_divide(identity,inverse(X0)),double_divide(X1,multiply(identity,X0)))))=X1)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f388])).
% 0.95/0.89 fof(f516,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(double_divide(identity,inverse(X0)),double_divide(X1,multiply(identity,X0))),identity)=X1)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f515])).
% 0.95/0.89 fof(f519,plain,(
% 0.95/0.89 ![X0,X1,X2]: (inverse(double_divide(identity,double_divide(inverse(identity),X0)))=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f390])).
% 0.95/0.89 fof(f520,plain,(
% 0.95/0.89 ![X0,X1,X2]: (multiply(double_divide(inverse(identity),X0),identity)=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f519])).
% 0.95/0.89 fof(f521,plain,(
% 0.95/0.89 ![X0,X1,X2]: (multiply(double_divide(identity,X0),identity)=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f520])).
% 0.95/0.89 fof(f522,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(identity,X0)),inverse(identity))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f391])).
% 0.95/0.89 fof(f523,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(identity,double_divide(identity,X0)),identity)=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f522])).
% 0.95/0.89 fof(f524,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(double_divide(identity,double_divide(identity,X0)))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f523])).
% 0.95/0.89 fof(f525,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f524])).
% 0.95/0.89 fof(f533,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(double_divide(identity,double_divide(inverse(identity),X0)))=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f394])).
% 0.95/0.89 fof(f534,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(inverse(identity),X0),identity)=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f533])).
% 0.95/0.89 fof(f535,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f534])).
% 0.95/0.89 fof(f580,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(double_divide(multiply(identity,X0),double_divide(double_divide(identity,inverse(X0)),inverse(X1))))=X1)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f411])).
% 0.95/0.89 fof(f581,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(double_divide(identity,inverse(X0)),inverse(X1)),multiply(identity,X0))=X1)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f580])).
% 0.95/0.89 fof(f589,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(multiply(X0,identity),inverse(X1)),multiply(identity,X0))=X1)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f594,f581])).
% 0.95/0.89 fof(f592,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(multiply(X0,identity),double_divide(X1,multiply(identity,X0))),identity)=X1)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f594,f516])).
% 0.95/0.89 fof(f594,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,inverse(X0))=multiply(X0,identity))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f455])).
% 0.95/0.89 fof(f624,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(double_divide(identity,X0),X1),inverse(X0))=multiply(double_divide(identity,X1),identity))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f446,f448])).
% 0.95/0.89 fof(f659,plain,(
% 0.95/0.89 ![X0]: (identity=double_divide(double_divide(identity,multiply(X0,identity)),X0))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f437,f28])).
% 0.95/0.89 fof(f712,plain,(
% 0.95/0.89 ![X0]: (multiply(double_divide(identity,X0),X0)=identity)),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f446,f415])).
% 0.95/0.89 fof(f821,plain,(
% 0.95/0.89 ![X0]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(double_divide(identity,identity),double_divide(X0,identity))))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f712,f467])).
% 0.95/0.89 fof(f826,plain,(
% 0.95/0.89 ![X0]: (multiply(double_divide(identity,inverse(X0)),identity)=double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,multiply(identity,X0)),identity)),identity)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f40,f467])).
% 0.95/0.89 fof(f827,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(identity,double_divide(X0,X1)),identity)=double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,multiply(X1,X0)),identity)),identity)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f28,f467])).
% 0.95/0.89 fof(f836,plain,(
% 0.95/0.89 ![X0]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(inverse(identity),double_divide(X0,identity))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f821])).
% 0.95/0.89 fof(f837,plain,(
% 0.95/0.89 ![X0]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(identity,double_divide(X0,identity))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f412,f836])).
% 0.95/0.89 fof(f838,plain,(
% 0.95/0.89 ![X0]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,double_divide(identity,inverse(X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f837])).
% 0.95/0.89 fof(f841,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,multiply(multiply(X0,X1),identity))=double_divide(X1,X0))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f852,f475])).
% 0.95/0.89 fof(f845,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(double_divide(identity,X0),X1),inverse(X0))=double_divide(identity,multiply(X1,identity)))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f852,f624])).
% 0.95/0.89 fof(f848,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,multiply(X0,identity))=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f852,f535])).
% 0.95/0.89 fof(f849,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,multiply(X0,identity))=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f852,f525])).
% 0.95/0.89 fof(f850,plain,(
% 0.95/0.89 ![X0,X1,X2]: (double_divide(identity,multiply(X0,identity))=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f852,f521])).
% 0.95/0.89 fof(f851,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,multiply(X0,identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f852,f493])).
% 0.95/0.89 fof(f852,plain,(
% 0.95/0.89 ![X0]: (multiply(double_divide(identity,X0),identity)=double_divide(identity,multiply(X0,identity)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f594,f838])).
% 0.95/0.89 fof(f869,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,multiply(identity,X0)),identity)),identity)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f852,f826])).
% 0.95/0.89 fof(f870,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=double_divide(identity,inverse(double_divide(identity,multiply(double_divide(identity,multiply(identity,X0)),identity)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f869])).
% 0.95/0.89 fof(f871,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=multiply(double_divide(identity,multiply(double_divide(identity,multiply(identity,X0)),identity)),identity))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f594,f870])).
% 0.95/0.89 fof(f872,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=double_divide(identity,double_divide(identity,multiply(identity,X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f475,f871])).
% 0.95/0.89 fof(f873,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,multiply(double_divide(X0,X1),identity))=double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,multiply(X1,X0)),identity)),identity)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f852,f827])).
% 0.95/0.89 fof(f874,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,multiply(double_divide(X0,X1),identity))=double_divide(identity,inverse(double_divide(identity,multiply(double_divide(identity,multiply(X1,X0)),identity)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f873])).
% 0.95/0.89 fof(f875,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,multiply(double_divide(X0,X1),identity))=multiply(double_divide(identity,multiply(double_divide(identity,multiply(X1,X0)),identity)),identity))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f594,f874])).
% 0.95/0.89 fof(f876,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,multiply(double_divide(X0,X1),identity))=double_divide(identity,double_divide(identity,multiply(X1,X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f475,f875])).
% 0.95/0.89 fof(f939,plain,(
% 0.95/0.89 ![X0]: (multiply(double_divide(identity,double_divide(identity,X0)),identity)=inverse(inverse(X0)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f499,f25])).
% 0.95/0.89 fof(f954,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(double_divide(identity,X0),identity))=inverse(inverse(X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f852,f939])).
% 0.95/0.89 fof(f955,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,double_divide(identity,multiply(X0,identity)))=inverse(inverse(X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f876,f954])).
% 0.95/0.89 fof(f960,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,double_divide(identity,multiply(X0,identity)))=multiply(identity,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f27,f955])).
% 0.95/0.89 fof(f964,plain,(
% 0.95/0.89 ![X0]: (multiply(identity,double_divide(identity,X0))=double_divide(identity,multiply(identity,X0)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f441,f440])).
% 0.95/0.89 fof(f977,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=double_divide(identity,inverse(multiply(X0,identity))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f980,f872])).
% 0.95/0.89 fof(f980,plain,(
% 0.95/0.89 ![X0]: (inverse(multiply(X0,identity))=double_divide(identity,multiply(identity,X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f38,f964])).
% 0.95/0.89 fof(f994,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=multiply(multiply(X0,identity),identity))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f594,f977])).
% 0.95/0.89 fof(f995,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f437,f994])).
% 0.95/0.89 fof(f1098,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(identity,X0))=multiply(inverse(X0),identity))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f27,f594])).
% 0.95/0.89 fof(f1099,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,multiply(X0,X1))=multiply(double_divide(X1,X0),identity))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f25,f594])).
% 0.95/0.89 fof(f1106,plain,(
% 0.95/0.89 ![X0]: (multiply(inverse(X0),identity)=inverse(multiply(X0,identity)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f594,f25])).
% 0.95/0.89 fof(f1115,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,multiply(double_divide(X0,multiply(identity,X1)),multiply(X1,identity)))=X0)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1099,f592])).
% 0.95/0.89 fof(f1211,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(identity,identity))=double_divide(X0,double_divide(identity,X0)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f712,f841])).
% 0.95/0.89 fof(f1223,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,double_divide(identity,double_divide(X0,X1)))=inverse(multiply(multiply(X1,X0),identity)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f841,f499])).
% 0.95/0.89 fof(f1229,plain,(
% 0.95/0.89 ![X0]: (multiply(inverse(identity),identity)=double_divide(X0,double_divide(identity,X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1098,f1211])).
% 0.95/0.89 fof(f1231,plain,(
% 0.95/0.89 ![X0]: (identity=double_divide(X0,double_divide(identity,X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f375,f1229])).
% 0.95/0.89 fof(f1255,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,double_divide(identity,double_divide(X0,X1)))=multiply(inverse(multiply(X1,X0)),identity))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1106,f1223])).
% 0.95/0.89 fof(f1297,plain,(
% 0.95/0.89 ![X0]: (multiply(identity,inverse(X0))=double_divide(identity,multiply(double_divide(identity,double_divide(identity,X0)),identity)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1231,f845])).
% 0.95/0.89 fof(f1301,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(multiply(X0,identity),X1),inverse(inverse(X0)))=double_divide(identity,multiply(X1,identity)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f594,f845])).
% 0.95/0.89 fof(f1309,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,multiply(double_divide(identity,multiply(X0,identity)),identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),X0)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f845,f841])).
% 0.95/0.89 fof(f1313,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,X0)=double_divide(identity,multiply(double_divide(identity,double_divide(identity,X0)),identity)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f440,f1297])).
% 0.95/0.89 fof(f1314,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,X0)=double_divide(identity,double_divide(identity,multiply(double_divide(identity,X0),identity))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1099,f1313])).
% 0.95/0.89 fof(f1315,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,X0)=multiply(identity,double_divide(identity,X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f960,f1314])).
% 0.95/0.89 fof(f1316,plain,(
% 0.95/0.89 ![X0]: (multiply(inverse(X0),identity)=double_divide(identity,X0))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1317,f1106])).
% 0.95/0.89 fof(f1317,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,X0)=inverse(multiply(X0,identity)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f38,f1315])).
% 0.95/0.89 fof(f1323,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(inverse(X0),identity))=X0)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1324,f589])).
% 0.95/0.89 fof(f1324,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(double_divide(multiply(X0,identity),X1),multiply(identity,X0))=double_divide(identity,multiply(X1,identity)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f27,f1301])).
% 0.95/0.89 fof(f1336,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,double_divide(identity,multiply(multiply(X0,identity),identity)))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1099,f1309])).
% 0.95/0.89 fof(f1337,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(identity,multiply(X0,identity))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f960,f1336])).
% 0.95/0.89 fof(f1338,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(X0,identity))=double_divide(identity,double_divide(identity,inverse(X0))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1339,f851])).
% 0.95/0.89 fof(f1339,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,double_divide(identity,X0))=double_divide(inverse(X1),double_divide(double_divide(identity,X1),X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f456,f1337])).
% 0.95/0.89 fof(f1344,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(identity,double_divide(identity,double_divide(X0,X1)))=double_divide(identity,multiply(X1,X0)))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1316,f1255])).
% 0.95/0.89 fof(f1352,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(identity,X0))=double_divide(identity,X0))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1316,f1098])).
% 0.95/0.89 fof(f1353,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,double_divide(identity,X0))=X0)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1316,f995])).
% 0.95/0.89 fof(f1355,plain,(
% 0.95/0.89 ![X0]: (multiply(X0,identity)=multiply(identity,X0))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1360,f960])).
% 0.95/0.89 fof(f1360,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,double_divide(identity,X0))=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1316,f1323])).
% 0.95/0.89 fof(f1362,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(multiply(X0,X1))=double_divide(X1,X0))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1375,f841])).
% 0.95/0.89 fof(f1369,plain,(
% 0.95/0.89 ![X0,X1,X2]: (inverse(X0)=double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1375,f850])).
% 0.95/0.89 fof(f1370,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(X0)=double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1375,f849])).
% 0.95/0.89 fof(f1371,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(X0)=double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1375,f848])).
% 0.95/0.89 fof(f1374,plain,(
% 0.95/0.89 ![X0]: (identity=double_divide(inverse(X0),X0))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1375,f659])).
% 0.95/0.89 fof(f1375,plain,(
% 0.95/0.89 ![X0]: (double_divide(identity,multiply(X0,identity))=inverse(X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1360,f1338])).
% 0.95/0.89 fof(f1376,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(multiply(X0,identity),double_divide(X1,multiply(identity,X0)))=X1)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1382,f1115])).
% 0.95/0.89 fof(f1382,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(X0,X1)=double_divide(identity,multiply(X1,X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1360,f1344])).
% 0.95/0.89 fof(f1386,plain,(
% 0.95/0.89 ![X0]: (double_divide(X0,identity)=double_divide(identity,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1382,f1352])).
% 0.95/0.89 fof(f1387,plain,(
% 0.95/0.89 ![X0]: (inverse(inverse(X0))=multiply(X0,identity))),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1409,f594])).
% 0.95/0.89 fof(f1409,plain,(
% 0.95/0.89 ![X0]: (inverse(X0)=double_divide(identity,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f1386])).
% 0.95/0.89 fof(f1410,plain,(
% 0.95/0.89 ![X0]: (inverse(double_divide(identity,X0))=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1409,f1353])).
% 0.95/0.89 fof(f1419,plain,(
% 0.95/0.89 ![X0]: (multiply(X0,identity)=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f1410])).
% 0.95/0.89 fof(f1427,plain,(
% 0.95/0.89 ![X0]: (X0=multiply(identity,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1419,f1355])).
% 0.95/0.89 fof(f1438,plain,(
% 0.95/0.89 ![X0,X1,X2]: (inverse(X0)=double_divide(X1,double_divide(inverse(X2),double_divide(X0,double_divide(X2,X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1409,f1369])).
% 0.95/0.89 fof(f1439,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(X0)=double_divide(X1,inverse(double_divide(X0,double_divide(identity,X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1409,f1370])).
% 0.95/0.89 fof(f1440,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(X0)=double_divide(X1,multiply(double_divide(identity,X1),X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f1439])).
% 0.95/0.89 fof(f1441,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(X0)=double_divide(X1,multiply(inverse(X1),X0)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1409,f1440])).
% 0.95/0.89 fof(f1442,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(X0)=inverse(double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1409,f1371])).
% 0.95/0.89 fof(f1443,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(X0)=multiply(double_divide(X0,inverse(X1)),double_divide(identity,X1)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f25,f1442])).
% 0.95/0.89 fof(f1445,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(X0)=multiply(double_divide(X0,inverse(X1)),inverse(X1)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1409,f1443])).
% 0.95/0.89 fof(f1448,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(X0,double_divide(X1,multiply(identity,X0)))=X1)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1419,f1376])).
% 0.95/0.89 fof(f1450,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(X0,double_divide(X1,X0))=X1)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1427,f1448])).
% 0.95/0.89 fof(f1460,plain,(
% 0.95/0.89 ![X0]: (inverse(inverse(X0))=X0)),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1419,f1387])).
% 0.95/0.89 fof(f1505,plain,(
% 0.95/0.89 ![X0,X1,X2,X3]: (inverse(X0)=double_divide(X1,double_divide(double_divide(X2,X3),double_divide(X0,double_divide(multiply(X3,X2),X1)))))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1362,f1438])).
% 0.95/0.89 fof(f1539,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(X0)=double_divide(inverse(X1),multiply(X1,X0)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1460,f1441])).
% 0.95/0.89 fof(f1542,plain,(
% 0.95/0.89 ![X0,X1,X2]: (inverse(X0)=double_divide(double_divide(X1,X2),multiply(multiply(X2,X1),X0)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f25,f1441])).
% 0.95/0.89 fof(f1584,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(X0)=multiply(double_divide(X0,X1),inverse(inverse(X1))))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1460,f1445])).
% 0.95/0.89 fof(f1598,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(X0)=multiply(double_divide(X0,X1),X1))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1460,f1584])).
% 0.95/0.89 fof(f1631,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(double_divide(X0,X1),X0)=X1)),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1450,f1450])).
% 0.95/0.89 fof(f1636,plain,(
% 0.95/0.89 ![X0,X1,X2]: (inverse(X0)=double_divide(double_divide(X1,X2),double_divide(inverse(X2),double_divide(X0,X1))))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1450,f1438])).
% 0.95/0.89 fof(f1653,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(inverse(double_divide(X0,X1)))=double_divide(X1,double_divide(inverse(X0),identity)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1374,f1438])).
% 0.95/0.89 fof(f1661,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(X0,X1)=double_divide(X1,double_divide(inverse(X0),identity)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1460,f1653])).
% 0.95/0.89 fof(f1662,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(X0,X1)=double_divide(X1,inverse(inverse(X0))))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f8,f1661])).
% 0.95/0.89 fof(f1669,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(X0,double_divide(X0,X1))=X1)),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f1670,f1631])).
% 0.95/0.89 fof(f1670,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(X0,X1)=double_divide(X1,X0))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f1460,f1662])).
% 0.95/0.89 fof(f1734,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X0,X1)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1670,f25])).
% 0.95/0.89 fof(f1764,plain,(
% 0.95/0.89 ![X0,X1,X2,X3]: (inverse(X0)=double_divide(double_divide(X1,multiply(X2,X3)),double_divide(double_divide(X3,X2),double_divide(X0,X1))))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1450,f1505])).
% 0.95/0.89 fof(f1855,plain,(
% 0.95/0.89 ![X0,X1]: (double_divide(X0,inverse(X1))=multiply(inverse(X0),X1))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1441,f1669])).
% 0.95/0.89 fof(f2140,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(X0)=multiply(X1,double_divide(X0,X1)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1669,f1598])).
% 0.95/0.89 fof(f2141,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(X0)=multiply(X1,double_divide(X1,X0)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1450,f1598])).
% 0.95/0.89 fof(f2194,plain,(
% 0.95/0.89 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),inverse(X2))=multiply(multiply(X1,X0),X2))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1542,f1669])).
% 0.95/0.89 fof(f2253,plain,(
% 0.95/0.89 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f25,f1734])).
% 0.95/0.89 fof(f2266,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(multiply(X0,X1))=double_divide(X0,X1))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1734,f1460])).
% 0.95/0.89 fof(f2271,plain,(
% 0.95/0.89 ~multiply(a4,b4)=multiply(a4,b4)|sQ3_spl),
% 0.95/0.89 inference(backward_demodulation,[status(thm)],[f2253,f22])).
% 0.95/0.89 fof(f2281,plain,(
% 0.95/0.89 $false|sQ3_spl),
% 0.95/0.89 inference(trivial_equality_resolution,[status(thm)],[f2271])).
% 0.95/0.89 fof(f2282,plain,(
% 0.95/0.89 sQ3_spl),
% 0.95/0.89 inference(contradiction_clause,[status(thm)],[f2281])).
% 0.95/0.89 fof(f2283,plain,(
% 0.95/0.89 ~multiply(c3,multiply(a3,b3))=multiply(a3,multiply(b3,c3))|sQ2_spl),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f2253,f19])).
% 0.95/0.89 fof(f2348,plain,(
% 0.95/0.89 ![X0,X1,X2]: (double_divide(double_divide(X0,X1),inverse(X2))=double_divide(inverse(X1),double_divide(X2,X0)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f1636,f1669])).
% 0.95/0.89 fof(f2416,plain,(
% 0.95/0.89 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=double_divide(inverse(X0),double_divide(X2,X1)))),
% 0.95/0.89 inference(forward_demodulation,[status(thm)],[f2194,f2348])).
% 0.95/0.89 fof(f2801,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(double_divide(X0,X1))=double_divide(inverse(X0),inverse(X1)))),
% 0.95/0.89 inference(paramodulation,[status(thm)],[f2141,f1539])).
% 0.95/0.89 fof(f2802,plain,(
% 0.95/0.89 ![X0,X1]: (inverse(double_divide(X0,X1))=double_divide(inverse(X1),inverse(X0)))),
% 0.95/0.91 inference(paramodulation,[status(thm)],[f2140,f1539])).
% 0.95/0.91 fof(f2826,plain,(
% 0.95/0.91 ![X0,X1]: (multiply(X0,X1)=double_divide(inverse(X0),inverse(X1)))),
% 0.95/0.91 inference(forward_demodulation,[status(thm)],[f1734,f2801])).
% 0.95/0.91 fof(f2827,plain,(
% 0.95/0.91 ![X0,X1]: (multiply(X0,X1)=double_divide(inverse(X1),inverse(X0)))),
% 0.95/0.91 inference(forward_demodulation,[status(thm)],[f1734,f2802])).
% 0.95/0.91 fof(f3002,plain,(
% 0.95/0.91 ![X0,X1,X2,X3]: (double_divide(double_divide(double_divide(X0,X1),double_divide(X2,X3)),inverse(X2))=double_divide(X3,multiply(X1,X0)))),
% 0.95/0.91 inference(paramodulation,[status(thm)],[f1764,f1450])).
% 0.95/0.91 fof(f3159,plain,(
% 0.95/0.91 ![X0,X1,X2,X3]: (double_divide(inverse(X0),double_divide(double_divide(X1,X2),double_divide(X0,X3)))=double_divide(X3,multiply(X2,X1)))),
% 0.95/0.91 inference(forward_demodulation,[status(thm)],[f1670,f3002])).
% 0.95/0.91 fof(f3160,plain,(
% 0.95/0.91 ![X0,X1,X2,X3]: (multiply(multiply(X0,double_divide(X0,X1)),double_divide(X2,X3))=double_divide(X1,multiply(X3,X2)))),
% 0.95/0.91 inference(forward_demodulation,[status(thm)],[f2416,f3159])).
% 0.95/0.91 fof(f3161,plain,(
% 0.95/0.91 ![X0,X1,X2]: (multiply(inverse(X0),double_divide(X1,X2))=double_divide(X0,multiply(X2,X1)))),
% 0.95/0.91 inference(forward_demodulation,[status(thm)],[f2141,f3160])).
% 0.95/0.91 fof(f3162,plain,(
% 0.95/0.91 ![X0,X1,X2]: (double_divide(X0,inverse(double_divide(X1,X2)))=double_divide(X0,multiply(X2,X1)))),
% 0.95/0.91 inference(forward_demodulation,[status(thm)],[f1855,f3161])).
% 0.95/0.91 fof(f3163,plain,(
% 0.95/0.91 ![X0,X1,X2]: (double_divide(X0,multiply(X1,X2))=double_divide(X0,multiply(X2,X1)))),
% 0.95/0.91 inference(forward_demodulation,[status(thm)],[f1734,f3162])).
% 0.95/0.91 fof(f3749,plain,(
% 0.95/0.91 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=double_divide(inverse(X0),double_divide(X1,X2)))),
% 0.95/0.91 inference(paramodulation,[status(thm)],[f2266,f2826])).
% 0.95/0.91 fof(f3776,plain,(
% 0.95/0.91 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X2,X1)))),
% 0.95/0.91 inference(backward_demodulation,[status(thm)],[f3749,f2416])).
% 0.95/0.91 fof(f4156,plain,(
% 0.95/0.91 ![X0,X1]: (multiply(inverse(X0),X1)=double_divide(inverse(X1),X0))),
% 0.95/0.91 inference(paramodulation,[status(thm)],[f1460,f2827])).
% 0.95/0.91 fof(f5778,plain,(
% 0.95/0.91 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=inverse(double_divide(X2,multiply(X1,X0))))),
% 0.95/0.91 inference(paramodulation,[status(thm)],[f3163,f25])).
% 0.95/0.91 fof(f5828,plain,(
% 0.95/0.91 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=inverse(double_divide(X1,multiply(X2,X0))))),
% 0.95/0.91 inference(forward_demodulation,[status(thm)],[f3776,f5778])).
% 0.95/0.91 fof(f5829,plain,(
% 0.95/0.91 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))|sQ2_spl),
% 0.95/0.91 inference(backward_demodulation,[status(thm)],[f5835,f2283])).
% 0.95/0.91 fof(f5835,plain,(
% 0.95/0.91 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(X1,multiply(X2,X0)))),
% 0.95/0.91 inference(forward_demodulation,[status(thm)],[f1734,f5828])).
% 0.95/0.91 fof(f5858,plain,(
% 0.95/0.91 $false|sQ2_spl),
% 0.95/0.91 inference(trivial_equality_resolution,[status(thm)],[f5829])).
% 0.95/0.91 fof(f5859,plain,(
% 0.95/0.91 sQ2_spl),
% 0.95/0.91 inference(contradiction_clause,[status(thm)],[f5858])).
% 0.95/0.91 fof(f5875,plain,(
% 0.95/0.91 ~double_divide(inverse(a1),a1)=identity|sQ0_spl),
% 0.95/0.91 inference(forward_demodulation,[status(thm)],[f4156,f13])).
% 0.95/0.91 fof(f5876,plain,(
% 0.95/0.91 ~double_divide(a1,inverse(a1))=identity|sQ0_spl),
% 0.95/0.91 inference(forward_demodulation,[status(thm)],[f1670,f5875])).
% 0.95/0.91 fof(f5877,plain,(
% 0.95/0.91 ~identity=identity|sQ0_spl),
% 0.95/0.91 inference(forward_demodulation,[status(thm)],[f9,f5876])).
% 0.95/0.91 fof(f5878,plain,(
% 0.95/0.91 $false|sQ0_spl),
% 0.95/0.91 inference(trivial_equality_resolution,[status(thm)],[f5877])).
% 0.95/0.91 fof(f5879,plain,(
% 0.95/0.91 sQ0_spl),
% 0.95/0.91 inference(contradiction_clause,[status(thm)],[f5878])).
% 0.95/0.91 fof(f5882,plain,(
% 0.95/0.91 ~a2=a2|sQ1_spl),
% 0.95/0.91 inference(forward_demodulation,[status(thm)],[f1427,f16])).
% 0.95/0.91 fof(f5883,plain,(
% 0.95/0.91 $false|sQ1_spl),
% 0.95/0.91 inference(trivial_equality_resolution,[status(thm)],[f5882])).
% 0.95/0.91 fof(f5884,plain,(
% 0.95/0.91 sQ1_spl),
% 0.95/0.91 inference(contradiction_clause,[status(thm)],[f5883])).
% 0.95/0.91 fof(f5885,plain,(
% 0.95/0.91 $false),
% 0.95/0.91 inference(sat_refutation,[status(thm)],[f23,f2282,f5859,f5879,f5884])).
% 0.95/0.91 % SZS output end CNFRefutation for theBenchmark.p
% 0.95/0.93 % Elapsed time: 0.472897 seconds
% 0.95/0.93 % CPU time: 3.196958 seconds
% 0.95/0.93 % Total memory used: 106.117 MB
% 0.95/0.93 % Net memory used: 104.040 MB
%------------------------------------------------------------------------------