%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP099-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 : n020.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.25s 5.75s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP099-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/5.52 % Computer : n020.cluster.edu
% 0.20/5.52 % Model : x86_64 x86_64
% 0.20/5.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/5.52 % Memory : 8046.5625MB
% 0.20/5.52 % OS : Linux 6.8.0-71-generic
% 0.20/5.52 % CPULimit : 300
% 0.20/5.52 % WCLimit : 300
% 0.20/5.52 % DateTime : Sun Sep 20 19:58:22 UTC 2026
% 0.20/5.52 % CPUTime :
% 0.20/5.54 % Drodi V4.1.1
% 0.25/5.75 % Refutation found
% 0.25/5.75 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.25/5.75 % SZS output start CNFRefutation for theBenchmark
% 0.25/5.75 fof(f1,axiom,(
% 0.25/5.75 (![X,Y,Z]: (double_divide(double_divide(X,double_divide(double_divide(Y,double_divide(X,Z)),double_divide(identity,Z))),double_divide(identity,identity)) = Y ))),
% 0.25/5.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/5.75 fof(f2,axiom,(
% 0.25/5.75 (![X,Y]: (multiply(X,Y) = double_divide(double_divide(Y,X),identity) ))),
% 0.25/5.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/5.75 fof(f3,axiom,(
% 0.25/5.75 (![X]: (inverse(X) = double_divide(X,identity) ))),
% 0.25/5.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/5.75 fof(f4,axiom,(
% 0.25/5.75 (![X]: (identity = double_divide(X,inverse(X)) ))),
% 0.25/5.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/5.75 fof(f5,negated_conjecture,(
% 0.25/5.75 ( 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.25/5.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/5.75 fof(f6,plain,(
% 0.25/5.75 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),double_divide(identity,identity))=X1)),
% 0.25/5.75 inference(cnf_transformation,[status(thm)],[f1])).
% 0.25/5.75 fof(f7,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(X0,X1)=double_divide(double_divide(X1,X0),identity))),
% 0.25/5.75 inference(cnf_transformation,[status(thm)],[f2])).
% 0.25/5.75 fof(f8,plain,(
% 0.25/5.75 ![X0]: (inverse(X0)=double_divide(X0,identity))),
% 0.25/5.75 inference(cnf_transformation,[status(thm)],[f3])).
% 0.25/5.75 fof(f9,plain,(
% 0.25/5.75 ![X0]: (identity=double_divide(X0,inverse(X0)))),
% 0.25/5.75 inference(cnf_transformation,[status(thm)],[f4])).
% 0.25/5.75 fof(f10,plain,(
% 0.25/5.75 ~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.25/5.75 inference(cnf_transformation,[status(thm)],[f5])).
% 0.25/5.75 fof(f11,definition,(
% 0.25/5.75 sQ0_spl <=> (multiply(inverse(a1),a1)=identity)),
% 0.25/5.75 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.25/5.75 fof(f13,plain,(
% 0.25/5.75 ~multiply(inverse(a1),a1)=identity|sQ0_spl),
% 0.25/5.75 inference(component_clause,[status(thm)],[f11])).
% 0.25/5.75 fof(f14,definition,(
% 0.25/5.75 sQ1_spl <=> (multiply(identity,a2)=a2)),
% 0.25/5.75 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.25/5.75 fof(f16,plain,(
% 0.25/5.75 ~multiply(identity,a2)=a2|sQ1_spl),
% 0.25/5.75 inference(component_clause,[status(thm)],[f14])).
% 0.25/5.75 fof(f17,definition,(
% 0.25/5.75 sQ2_spl <=> (multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3)))),
% 0.25/5.75 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.25/5.75 fof(f19,plain,(
% 0.25/5.75 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))|sQ2_spl),
% 0.25/5.75 inference(component_clause,[status(thm)],[f17])).
% 0.25/5.75 fof(f20,definition,(
% 0.25/5.75 sQ3_spl <=> (multiply(a4,b4)=multiply(b4,a4))),
% 0.25/5.75 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.25/5.75 fof(f22,plain,(
% 0.25/5.75 ~multiply(a4,b4)=multiply(b4,a4)|sQ3_spl),
% 0.25/5.75 inference(component_clause,[status(thm)],[f20])).
% 0.25/5.75 fof(f23,plain,(
% 0.25/5.75 ~sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl),
% 0.25/5.75 inference(split_clause,[status(thm)],[f10,f11,f14,f17,f20])).
% 0.25/5.75 fof(f24,plain,(
% 0.25/5.75 ![X0,X1,X2]: (double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),inverse(identity))=X1)),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f8,f6])).
% 0.25/5.75 fof(f25,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(X0,X1)=inverse(double_divide(X1,X0)))),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f8,f7])).
% 0.25/5.75 fof(f26,plain,(
% 0.25/5.75 ![X0]: (multiply(inverse(X0),X0)=inverse(identity))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f9,f25])).
% 0.25/5.75 fof(f27,plain,(
% 0.25/5.75 ![X0]: (multiply(identity,X0)=inverse(inverse(X0)))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f8,f25])).
% 0.25/5.75 fof(f29,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(multiply(X0,X1),double_divide(X1,X0))=inverse(identity))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f25,f26])).
% 0.25/5.75 fof(f55,plain,(
% 0.25/5.75 ![X0,X1,X2,X3]: (double_divide(double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),double_divide(double_divide(X3,X1),double_divide(identity,inverse(identity)))),inverse(identity))=X3)),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f24,f24])).
% 0.25/5.75 fof(f58,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(X0,double_divide(double_divide(X1,inverse(X0)),double_divide(identity,identity))),inverse(identity))=X1)),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f8,f24])).
% 0.25/5.75 fof(f59,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,inverse(identity))),identity)),inverse(identity))=X1)),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f9,f24])).
% 0.25/5.75 fof(f64,plain,(
% 0.25/5.75 ![X0,X1,X2,X3]: (double_divide(double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),double_divide(double_divide(X3,X1),identity)),inverse(identity))=X3)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f9,f55])).
% 0.25/5.75 fof(f65,plain,(
% 0.25/5.75 ![X0,X1,X2,X3]: (double_divide(double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),inverse(double_divide(X3,X1))),inverse(identity))=X3)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f8,f64])).
% 0.25/5.75 fof(f66,plain,(
% 0.25/5.75 ![X0,X1,X2,X3]: (double_divide(double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),multiply(X1,X3)),inverse(identity))=X3)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f25,f65])).
% 0.25/5.75 fof(f69,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(X0,double_divide(double_divide(X1,inverse(X0)),inverse(identity))),inverse(identity))=X1)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f8,f58])).
% 0.25/5.75 fof(f70,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(X0,inverse(double_divide(X1,double_divide(X0,inverse(identity))))),inverse(identity))=X1)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f8,f59])).
% 0.25/5.75 fof(f71,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(X0,multiply(double_divide(X0,inverse(identity)),X1)),inverse(identity))=X1)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f25,f70])).
% 0.25/5.75 fof(f77,plain,(
% 0.25/5.75 ![X0]: (double_divide(double_divide(identity,multiply(identity,X0)),inverse(identity))=X0)),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f9,f71])).
% 0.25/5.75 fof(f82,plain,(
% 0.25/5.75 ![X0]: (double_divide(double_divide(identity,inverse(inverse(X0))),inverse(identity))=X0)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f27,f77])).
% 0.25/5.75 fof(f93,plain,(
% 0.25/5.75 ![X0]: (multiply(inverse(identity),double_divide(identity,inverse(inverse(X0))))=inverse(X0))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f82,f25])).
% 0.25/5.75 fof(f108,plain,(
% 0.25/5.75 ![X0,X1,X2,X3]: (double_divide(double_divide(double_divide(X0,double_divide(double_divide(multiply(X1,X2),double_divide(X0,X3)),double_divide(identity,X3))),inverse(identity)),inverse(identity))=double_divide(X2,X1))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f29,f66])).
% 0.25/5.75 fof(f110,plain,(
% 0.25/5.75 ![X0,X1,X2]: (double_divide(double_divide(double_divide(X0,double_divide(double_divide(inverse(X1),double_divide(X0,X2)),double_divide(identity,X2))),inverse(identity)),inverse(identity))=X1)),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f26,f66])).
% 0.25/5.75 fof(f134,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(multiply(X0,X1),inverse(identity))=double_divide(X1,X0))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f24,f108])).
% 0.25/5.75 fof(f135,plain,(
% 0.25/5.75 ![X0]: (double_divide(inverse(X0),inverse(identity))=X0)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f24,f110])).
% 0.25/5.75 fof(f142,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(inverse(X0),multiply(X0,X1)),inverse(identity))=X1)),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f135,f71])).
% 0.25/5.75 fof(f147,plain,(
% 0.25/5.75 ![X0]: (multiply(inverse(identity),inverse(X0))=inverse(X0))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f135,f25])).
% 0.25/5.75 fof(f201,plain,(
% 0.25/5.75 ![X0]: (double_divide(double_divide(inverse(identity),inverse(inverse(X0))),inverse(identity))=X0)),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f27,f142])).
% 0.25/5.75 fof(f203,plain,(
% 0.25/5.75 ![X0]: (double_divide(double_divide(inverse(inverse(identity)),inverse(X0)),inverse(identity))=inverse(X0))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f147,f142])).
% 0.25/5.75 fof(f240,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(inverse(identity),inverse(multiply(X0,X1))),inverse(identity))=double_divide(X1,X0))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f25,f201])).
% 0.25/5.75 fof(f256,plain,(
% 0.25/5.75 ![X0]: (double_divide(double_divide(inverse(inverse(identity)),inverse(X0)),inverse(identity))=double_divide(identity,inverse(inverse(X0))))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f93,f142])).
% 0.25/5.75 fof(f267,plain,(
% 0.25/5.75 ![X0]: (inverse(X0)=double_divide(identity,inverse(inverse(X0))))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f203,f256])).
% 0.25/5.75 fof(f280,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(X0,inverse(X1)),double_divide(identity,inverse(inverse(X1))))),inverse(identity))=X0)),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f267,f24])).
% 0.25/5.75 fof(f283,plain,(
% 0.25/5.75 ![X0]: (multiply(inverse(inverse(X0)),identity)=inverse(inverse(X0)))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f267,f25])).
% 0.25/5.75 fof(f288,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(X0,inverse(X1)),inverse(X1))),inverse(identity))=X0)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f267,f280])).
% 0.25/5.75 fof(f315,plain,(
% 0.25/5.75 ![X0]: (double_divide(double_divide(inverse(inverse(inverse(X0))),inverse(inverse(X0))),inverse(identity))=identity)),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f283,f142])).
% 0.25/5.75 fof(f327,plain,(
% 0.25/5.75 ![X0]: (double_divide(double_divide(inverse(X0),X0),inverse(identity))=inverse(identity))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f201,f69])).
% 0.25/5.75 fof(f331,plain,(
% 0.25/5.75 ![X0]: (double_divide(double_divide(identity,double_divide(X0,inverse(identity))),inverse(identity))=inverse(X0))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f135,f69])).
% 0.25/5.75 fof(f332,plain,(
% 0.25/5.75 ![X0]: (double_divide(double_divide(identity,double_divide(X0,inverse(identity))),inverse(identity))=double_divide(inverse(identity),inverse(inverse(X0))))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f201,f69])).
% 0.25/5.75 fof(f333,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(identity,double_divide(X0,inverse(identity))),inverse(identity))=double_divide(inverse(X1),multiply(X1,X0)))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f142,f69])).
% 0.25/5.75 fof(f337,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(identity,double_divide(X0,inverse(identity))),inverse(identity))=double_divide(X1,double_divide(double_divide(X0,inverse(X1)),inverse(identity))))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f69,f69])).
% 0.25/5.75 fof(f338,plain,(
% 0.25/5.75 ![X0,X1,X2]: (double_divide(double_divide(identity,double_divide(X0,inverse(identity))),inverse(identity))=double_divide(X1,double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(identity,X2))))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f24,f69])).
% 0.25/5.75 fof(f340,plain,(
% 0.25/5.75 ![X0,X1,X2]: (double_divide(double_divide(double_divide(X0,X1),double_divide(double_divide(X2,multiply(X1,X0)),inverse(identity))),inverse(identity))=X2)),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f25,f69])).
% 0.25/5.75 fof(f347,plain,(
% 0.25/5.75 inverse(identity)=identity),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f327,f315])).
% 0.25/5.75 fof(f352,plain,(
% 0.25/5.75 ![X0]: (double_divide(inverse(X0),inverse(identity))=X0)),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f356,f201])).
% 0.25/5.75 fof(f356,plain,(
% 0.25/5.75 ![X0]: (inverse(X0)=double_divide(inverse(identity),inverse(inverse(X0))))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f331,f332])).
% 0.25/5.75 fof(f361,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(X0)=double_divide(inverse(X1),multiply(X1,X0)))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f331,f333])).
% 0.25/5.75 fof(f379,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(X0)=double_divide(X1,double_divide(double_divide(X0,inverse(X1)),inverse(identity))))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f331,f337])).
% 0.25/5.75 fof(f387,plain,(
% 0.25/5.75 ![X0,X1,X2]: (inverse(X0)=double_divide(X1,double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(identity,X2))))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f331,f338])).
% 0.25/5.75 fof(f409,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(multiply(X0,X1),identity)=double_divide(X1,X0))),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f347,f134])).
% 0.25/5.75 fof(f413,plain,(
% 0.25/5.75 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f347,f26])).
% 0.25/5.75 fof(f414,plain,(
% 0.25/5.75 ![X0,X1,X2]: (double_divide(double_divide(double_divide(X0,X1),double_divide(double_divide(X2,multiply(X1,X0)),inverse(identity))),identity)=X2)),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f347,f340])).
% 0.25/5.75 fof(f415,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(X0)=double_divide(X1,double_divide(double_divide(X0,inverse(X1)),identity)))),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f347,f379])).
% 0.25/5.75 fof(f417,plain,(
% 0.25/5.75 ![X0]: (inverse(X0)=double_divide(identity,inverse(inverse(X0))))),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f347,f356])).
% 0.25/5.75 fof(f426,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(identity,double_divide(double_divide(X0,inverse(X1)),inverse(X1))),identity)=X0)),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f347,f288])).
% 0.25/5.75 fof(f431,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(inverse(identity),inverse(multiply(X0,X1))),identity)=double_divide(X1,X0))),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f347,f240])).
% 0.25/5.75 fof(f439,plain,(
% 0.25/5.75 ![X0]: (double_divide(inverse(X0),identity)=X0)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f347,f352])).
% 0.25/5.75 fof(f442,plain,(
% 0.25/5.75 ![X0]: (multiply(identity,X0)=X0)),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f443,f27])).
% 0.25/5.75 fof(f443,plain,(
% 0.25/5.75 ![X0]: (inverse(inverse(X0))=X0)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f8,f439])).
% 0.25/5.75 fof(f520,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(multiply(X0,X1))=double_divide(X1,X0))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f8,f409])).
% 0.25/5.75 fof(f523,plain,(
% 0.25/5.75 ![X0,X1,X2]: (inverse(double_divide(double_divide(X0,X1),double_divide(double_divide(X2,multiply(X1,X0)),inverse(identity))))=X2)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f8,f414])).
% 0.25/5.75 fof(f524,plain,(
% 0.25/5.75 ![X0,X1,X2]: (multiply(double_divide(double_divide(X0,multiply(X1,X2)),inverse(identity)),double_divide(X2,X1))=X0)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f25,f523])).
% 0.25/5.75 fof(f525,plain,(
% 0.25/5.75 ![X0,X1,X2]: (multiply(double_divide(double_divide(X0,multiply(X1,X2)),identity),double_divide(X2,X1))=X0)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f347,f524])).
% 0.25/5.75 fof(f526,plain,(
% 0.25/5.75 ![X0,X1,X2]: (multiply(inverse(double_divide(X0,multiply(X1,X2))),double_divide(X2,X1))=X0)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f8,f525])).
% 0.25/5.75 fof(f527,plain,(
% 0.25/5.75 ![X0,X1,X2]: (multiply(multiply(multiply(X0,X1),X2),double_divide(X1,X0))=X2)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f25,f526])).
% 0.25/5.75 fof(f528,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(X0)=double_divide(X1,inverse(double_divide(X0,inverse(X1)))))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f8,f415])).
% 0.25/5.75 fof(f529,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(X0)=double_divide(X1,multiply(inverse(X1),X0)))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f25,f528])).
% 0.25/5.75 fof(f532,plain,(
% 0.25/5.75 ![X0,X1,X2]: (inverse(X0)=double_divide(X1,double_divide(double_divide(X0,double_divide(X1,X2)),inverse(X2))))),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f533,f387])).
% 0.25/5.75 fof(f533,plain,(
% 0.25/5.75 ![X0]: (inverse(X0)=double_divide(identity,X0))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f443,f417])).
% 0.25/5.75 fof(f556,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(double_divide(identity,double_divide(double_divide(X0,inverse(X1)),inverse(X1))))=X0)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f8,f426])).
% 0.25/5.75 fof(f557,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(double_divide(double_divide(X0,inverse(X1)),inverse(X1)),identity)=X0)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f25,f556])).
% 0.25/5.75 fof(f570,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(double_divide(inverse(identity),inverse(multiply(X0,X1))))=double_divide(X1,X0))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f8,f431])).
% 0.25/5.75 fof(f571,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),inverse(identity))=double_divide(X1,X0))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f25,f570])).
% 0.25/5.75 fof(f572,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(double_divide(X0,X1),inverse(identity))=double_divide(X0,X1))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f520,f571])).
% 0.25/5.75 fof(f573,plain,(
% 0.25/5.75 ![X0,X1]: (double_divide(double_divide(X0,inverse(X1)),inverse(X1))=X0)),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f575,f557])).
% 0.25/5.75 fof(f575,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(double_divide(X0,X1),identity)=double_divide(X0,X1))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f347,f572])).
% 0.25/5.75 fof(f768,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(multiply(inverse(X0),X1),X0)=inverse(inverse(X1)))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f529,f25])).
% 0.25/5.75 fof(f780,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(multiply(inverse(X0),X1),X0)=X1)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f443,f768])).
% 0.25/5.75 fof(f789,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(X0,double_divide(X0,inverse(X1)))=X1)),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f780,f527])).
% 0.25/5.75 fof(f809,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(X0,double_divide(X0,X1))=inverse(X1))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f443,f789])).
% 0.25/5.75 fof(f814,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(double_divide(inverse(X0),inverse(X1)))=double_divide(X0,X1))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f789,f529])).
% 0.25/5.75 fof(f817,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(double_divide(X0,inverse(X1)))=double_divide(inverse(X0),X1))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f789,f361])).
% 0.25/5.75 fof(f830,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(inverse(X0),inverse(X1))=double_divide(X1,X0))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f25,f814])).
% 0.25/5.75 fof(f833,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(X0)=multiply(inverse(multiply(X1,X0)),X1))),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f839,f361])).
% 0.25/5.75 fof(f839,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(inverse(X0),X1)=double_divide(inverse(X1),X0))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f25,f817])).
% 0.25/5.75 fof(f844,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(X0)=multiply(double_divide(X0,X1),X1))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f520,f833])).
% 0.25/5.75 fof(f848,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(X0,inverse(X1))=inverse(multiply(inverse(X0),X1)))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f529,f809])).
% 0.25/5.75 fof(f856,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(inverse(X0))=double_divide(double_divide(X1,X0),X1))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f809,f520])).
% 0.25/5.75 fof(f862,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(X0,inverse(double_divide(X1,inverse(X0))))=X1)),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f867,f573])).
% 0.25/5.75 fof(f863,plain,(
% 0.25/5.75 ![X0,X1,X2]: (inverse(X0)=double_divide(X1,multiply(X2,inverse(double_divide(X0,double_divide(X1,X2))))))),
% 0.25/5.75 inference(backward_demodulation,[status(thm)],[f867,f532])).
% 0.25/5.75 fof(f867,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(X0,inverse(X1))=double_divide(X1,inverse(X0)))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f520,f848])).
% 0.25/5.75 fof(f873,plain,(
% 0.25/5.75 ![X0,X1]: (X0=double_divide(double_divide(X1,X0),X1))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f443,f856])).
% 0.25/5.75 fof(f880,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(X0,multiply(inverse(X0),X1))=X1)),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f25,f862])).
% 0.25/5.75 fof(f881,plain,(
% 0.25/5.75 ![X0,X1,X2]: (inverse(X0)=double_divide(X1,multiply(X2,multiply(double_divide(X1,X2),X0))))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f25,f863])).
% 0.25/5.75 fof(f1004,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(X0,X1)=multiply(inverse(inverse(X1)),X0))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f880,f780])).
% 0.25/5.75 fof(f1017,plain,(
% 0.25/5.75 $false|sQ3_spl),
% 0.25/5.75 inference(backward_subsumption_resolution,[status(thm)],[f22,f1018])).
% 0.25/5.75 fof(f1018,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 0.25/5.75 inference(forward_demodulation,[status(thm)],[f443,f1004])).
% 0.25/5.75 fof(f1026,plain,(
% 0.25/5.75 sQ3_spl),
% 0.25/5.75 inference(contradiction_clause,[status(thm)],[f1017])).
% 0.25/5.75 fof(f1027,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(X0)=multiply(X1,double_divide(X0,X1)))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f844,f1018])).
% 0.25/5.75 fof(f1058,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(multiply(X0,X1))=double_divide(X0,X1))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f1018,f520])).
% 0.25/5.75 fof(f1128,plain,(
% 0.25/5.75 ~multiply(c3,multiply(a3,b3))=multiply(a3,multiply(b3,c3))|sQ2_spl),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f1018,f19])).
% 0.25/5.75 fof(f1134,plain,(
% 0.25/5.75 ![X0,X1]: (inverse(double_divide(X0,X1))=multiply(X0,X1))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f873,f1027])).
% 0.25/5.75 fof(f1140,plain,(
% 0.25/5.75 ![X0,X1]: (multiply(inverse(X0),X1)=double_divide(X0,inverse(X1)))),
% 0.25/5.75 inference(paramodulation,[status(thm)],[f1027,f780])).
% 0.25/5.75 fof(f1321,plain,(
% 0.25/5.75 ![X0,X1,X2]: (inverse(multiply(inverse(double_divide(X0,X1)),X2))=double_divide(X0,multiply(X1,X2)))),
% 0.25/5.76 inference(paramodulation,[status(thm)],[f880,f881])).
% 0.25/5.76 fof(f1358,plain,(
% 0.25/5.76 ![X0,X1,X2]: (double_divide(X0,inverse(double_divide(X1,X2)))=double_divide(X1,multiply(X2,X0)))),
% 0.25/5.76 inference(forward_demodulation,[status(thm)],[f520,f1321])).
% 0.25/5.76 fof(f1360,plain,(
% 0.25/5.76 ![X0,X1,X2]: (multiply(inverse(X0),double_divide(X1,X2))=double_divide(X1,multiply(X2,X0)))),
% 0.25/5.76 inference(forward_demodulation,[status(thm)],[f1140,f1358])).
% 0.25/5.76 fof(f1597,plain,(
% 0.25/5.76 ![X0,X1,X2]: (multiply(inverse(X0),double_divide(X1,X2))=double_divide(multiply(X1,X2),X0))),
% 0.25/5.76 inference(paramodulation,[status(thm)],[f1058,f830])).
% 0.25/5.76 fof(f1624,plain,(
% 0.25/5.76 ![X0,X1,X2]: (double_divide(X0,multiply(X1,X2))=double_divide(multiply(X0,X1),X2))),
% 0.25/5.76 inference(forward_demodulation,[status(thm)],[f1360,f1597])).
% 0.25/5.76 fof(f3169,plain,(
% 0.25/5.76 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=inverse(double_divide(X1,multiply(X2,X0))))),
% 0.25/5.76 inference(paramodulation,[status(thm)],[f1624,f25])).
% 0.25/5.76 fof(f3210,plain,(
% 0.25/5.76 $false|sQ2_spl),
% 0.25/5.76 inference(backward_subsumption_resolution,[status(thm)],[f1128,f3211])).
% 0.25/5.76 fof(f3211,plain,(
% 0.25/5.76 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(X1,multiply(X2,X0)))),
% 0.25/5.76 inference(forward_demodulation,[status(thm)],[f1134,f3169])).
% 0.25/5.76 fof(f3212,plain,(
% 0.25/5.76 sQ2_spl),
% 0.25/5.76 inference(contradiction_clause,[status(thm)],[f3210])).
% 0.25/5.76 fof(f3213,plain,(
% 0.25/5.76 ~identity=identity|sQ0_spl),
% 0.25/5.76 inference(forward_demodulation,[status(thm)],[f413,f13])).
% 0.25/5.76 fof(f3214,plain,(
% 0.25/5.76 $false|sQ0_spl),
% 0.25/5.76 inference(trivial_equality_resolution,[status(thm)],[f3213])).
% 0.25/5.76 fof(f3215,plain,(
% 0.25/5.76 sQ0_spl),
% 0.25/5.76 inference(contradiction_clause,[status(thm)],[f3214])).
% 0.25/5.76 fof(f3216,plain,(
% 0.25/5.76 ~a2=a2|sQ1_spl),
% 0.25/5.76 inference(forward_demodulation,[status(thm)],[f442,f16])).
% 0.25/5.76 fof(f3217,plain,(
% 0.25/5.76 $false|sQ1_spl),
% 0.25/5.76 inference(trivial_equality_resolution,[status(thm)],[f3216])).
% 0.25/5.76 fof(f3218,plain,(
% 0.25/5.76 sQ1_spl),
% 0.25/5.76 inference(contradiction_clause,[status(thm)],[f3217])).
% 0.25/5.76 fof(f3219,plain,(
% 0.25/5.76 $false),
% 0.25/5.76 inference(sat_refutation,[status(thm)],[f23,f1026,f3212,f3215,f3218])).
% 0.25/5.76 % SZS output end CNFRefutation for theBenchmark.p
% 0.25/5.79 % Elapsed time: 0.253627 seconds
% 0.25/5.79 % CPU time: 1.502025 seconds
% 0.25/5.79 % Total memory used: 84.615 MB
% 0.25/5.79 % Net memory used: 83.733 MB
%------------------------------------------------------------------------------