%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP002-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:24 PM UTC 2026
% Result : Unsatisfiable 0.13s 5.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP002-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/5.36 % Computer : n008.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.36 % CPULimit : 300
% 0.08/5.36 % WCLimit : 300
% 0.08/5.36 % DateTime : Sun Sep 20 19:54:16 UTC 2026
% 0.08/5.36 % CPUTime :
% 0.08/5.37 % Drodi V4.1.1
% 0.13/5.63 % Refutation found
% 0.13/5.63 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/5.63 % SZS output start CNFRefutation for theBenchmark
% 0.13/5.63 fof(f1,axiom,(
% 0.13/5.63 (![X]: (multiply(identity,X) = X ))),
% 0.13/5.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/5.63 fof(f2,axiom,(
% 0.13/5.63 (![X]: (multiply(inverse(X),X) = identity ))),
% 0.13/5.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/5.63 fof(f3,axiom,(
% 0.13/5.63 (![X,Y,Z]: (multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ))),
% 0.13/5.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/5.63 fof(f4,axiom,(
% 0.13/5.63 (![X]: (multiply(X,identity) = X ))),
% 0.13/5.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/5.63 fof(f5,axiom,(
% 0.13/5.63 (![X]: (multiply(X,inverse(X)) = identity ))),
% 0.13/5.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/5.63 fof(f6,axiom,(
% 0.13/5.63 (![X,Y]: (commutator(X,Y) = multiply(X,multiply(Y,multiply(inverse(X),inverse(Y)))) ))),
% 0.13/5.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/5.63 fof(f7,hypothesis,(
% 0.13/5.63 (![X]: (multiply(X,multiply(X,X)) = identity ))),
% 0.13/5.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/5.63 fof(f8,negated_conjecture,(
% 0.13/5.63 commutator(commutator(a,b),b) != identity ),
% 0.13/5.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/5.63 fof(f9,plain,(
% 0.13/5.63 ![X0]: (multiply(identity,X0)=X0)),
% 0.13/5.63 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/5.63 fof(f10,plain,(
% 0.13/5.63 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 0.13/5.63 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/5.63 fof(f11,plain,(
% 0.13/5.63 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 0.13/5.63 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/5.63 fof(f12,plain,(
% 0.13/5.63 ![X0]: (multiply(X0,identity)=X0)),
% 0.13/5.63 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/5.63 fof(f13,plain,(
% 0.13/5.63 ![X0]: (multiply(X0,inverse(X0))=identity)),
% 0.13/5.63 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/5.63 fof(f14,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,X1)=multiply(X0,multiply(X1,multiply(inverse(X0),inverse(X1)))))),
% 0.13/5.63 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/5.63 fof(f15,plain,(
% 0.13/5.63 ![X0]: (multiply(X0,multiply(X0,X0))=identity)),
% 0.13/5.63 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/5.63 fof(f16,plain,(
% 0.13/5.63 ~commutator(commutator(a,b),b)=identity),
% 0.13/5.63 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/5.63 fof(f33,plain,(
% 0.13/5.63 ![X0,X1]: (identity=multiply(X0,multiply(X1,inverse(multiply(X0,X1)))))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f13,f11])).
% 0.13/5.63 fof(f36,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(identity,X0)=multiply(inverse(X1),multiply(X1,X0)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f10,f11])).
% 0.13/5.63 fof(f39,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(identity,X0)=multiply(X1,multiply(inverse(X1),X0)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f13,f11])).
% 0.13/5.63 fof(f48,plain,(
% 0.13/5.63 ![X0,X1]: (X0=multiply(inverse(X1),multiply(X1,X0)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f9,f36])).
% 0.13/5.63 fof(f51,plain,(
% 0.13/5.63 ![X0,X1]: (X0=multiply(X1,multiply(inverse(X1),X0)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f9,f39])).
% 0.13/5.63 fof(f57,plain,(
% 0.13/5.63 ![X0]: (X0=multiply(inverse(inverse(X0)),identity))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f10,f48])).
% 0.13/5.63 fof(f59,plain,(
% 0.13/5.63 ![X0]: (multiply(X0,X0)=multiply(inverse(X0),identity))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f15,f48])).
% 0.13/5.63 fof(f65,plain,(
% 0.13/5.63 ![X0]: (X0=inverse(inverse(X0)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f12,f57])).
% 0.13/5.63 fof(f68,plain,(
% 0.13/5.63 ![X0]: (multiply(X0,X0)=inverse(X0))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f12,f59])).
% 0.13/5.63 fof(f82,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(inverse(X0),X1)=multiply(X0,multiply(X0,X1)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f68,f11])).
% 0.13/5.63 fof(f138,plain,(
% 0.13/5.63 ![X0,X1,X2]: (commutator(multiply(X0,X1),X2)=multiply(X0,multiply(X1,multiply(X2,multiply(inverse(multiply(X0,X1)),inverse(X2))))))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f11,f14])).
% 0.13/5.63 fof(f238,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(X0,inverse(multiply(X1,X0)))=multiply(inverse(X1),identity))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f33,f48])).
% 0.13/5.63 fof(f273,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(X0,inverse(multiply(X1,X0)))=inverse(X1))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f12,f238])).
% 0.13/5.63 fof(f286,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),X1)=multiply(X0,multiply(inverse(X1),multiply(inverse(multiply(X0,X1)),inverse(X1)))))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f82,f138])).
% 0.13/5.63 fof(f419,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),inverse(inverse(X0)))=inverse(X1))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f273,f273])).
% 0.13/5.63 fof(f425,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,multiply(X1,inverse(X0)))=multiply(X0,multiply(multiply(X1,inverse(X0)),inverse(X1))))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f273,f14])).
% 0.13/5.63 fof(f426,plain,(
% 0.13/5.63 ![X0,X1]: (inverse(multiply(X0,inverse(X1)))=multiply(X1,inverse(X0)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f273,f51])).
% 0.13/5.63 fof(f430,plain,(
% 0.13/5.63 ![X0,X1]: (inverse(multiply(X0,X1))=multiply(inverse(X1),inverse(X0)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f273,f48])).
% 0.13/5.63 fof(f451,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),X0)=inverse(X1))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f65,f419])).
% 0.13/5.63 fof(f457,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,multiply(X1,inverse(X0)))=multiply(X0,multiply(X1,multiply(inverse(X0),inverse(X1)))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f11,f425])).
% 0.13/5.63 fof(f459,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,multiply(X1,inverse(X0)))=commutator(X0,X1))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f14,f457])).
% 0.13/5.63 fof(f463,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,X1)=multiply(X0,multiply(X1,inverse(multiply(X1,X0)))))),
% 0.13/5.63 inference(backward_demodulation,[status(thm)],[f430,f14])).
% 0.13/5.63 fof(f469,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),X1)=multiply(X0,multiply(inverse(X1),inverse(multiply(X1,multiply(X0,X1))))))),
% 0.13/5.63 inference(backward_demodulation,[status(thm)],[f430,f286])).
% 0.13/5.63 fof(f478,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),X1)=multiply(X0,inverse(multiply(multiply(X1,multiply(X0,X1)),X1))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f430,f469])).
% 0.13/5.63 fof(f479,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),X1)=multiply(X0,inverse(multiply(X1,multiply(multiply(X0,X1),X1)))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f11,f478])).
% 0.13/5.63 fof(f480,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),X1)=multiply(X0,inverse(multiply(X1,multiply(X0,multiply(X1,X1))))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f11,f479])).
% 0.13/5.63 fof(f481,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),X1)=multiply(X0,inverse(multiply(X1,multiply(X0,inverse(X1))))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f68,f480])).
% 0.13/5.63 fof(f493,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(inverse(X0),X1)=inverse(multiply(inverse(X1),X0)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f51,f451])).
% 0.13/5.63 fof(f502,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(inverse(inverse(multiply(X0,X1))),X0)=multiply(inverse(multiply(X0,X1)),inverse(X1)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f451,f82])).
% 0.13/5.63 fof(f519,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(multiply(X0,X1),X0)=multiply(inverse(multiply(X0,X1)),inverse(X1)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f65,f502])).
% 0.13/5.63 fof(f520,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(X0,multiply(X1,X0))=multiply(inverse(multiply(X0,X1)),inverse(X1)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f11,f519])).
% 0.13/5.63 fof(f521,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(X0,multiply(X1,X0))=inverse(multiply(X1,multiply(X0,X1))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f430,f520])).
% 0.13/5.63 fof(f533,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),inverse(X0))=commutator(multiply(X0,X1),X1))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f273,f459])).
% 0.13/5.63 fof(f547,plain,(
% 0.13/5.63 ![X0,X1,X2]: (inverse(multiply(X0,multiply(X1,inverse(X2))))=multiply(X2,inverse(multiply(X0,X1))))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f11,f426])).
% 0.13/5.63 fof(f567,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),X1)=multiply(X0,multiply(X1,inverse(multiply(X1,X0)))))),
% 0.13/5.63 inference(backward_demodulation,[status(thm)],[f547,f481])).
% 0.13/5.63 fof(f596,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),inverse(X0))=commutator(X0,X1))),
% 0.13/5.63 inference(backward_demodulation,[status(thm)],[f597,f533])).
% 0.13/5.63 fof(f597,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),X1)=commutator(X0,X1))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f463,f567])).
% 0.13/5.63 fof(f601,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,multiply(X1,X0))=commutator(inverse(X1),multiply(X1,X0)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f48,f597])).
% 0.13/5.63 fof(f619,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,inverse(inverse(X1)))=commutator(inverse(X1),multiply(X1,X0)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f48,f596])).
% 0.13/5.63 fof(f629,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(inverse(X0),X1),X0)=commutator(inverse(X0),X1))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f65,f596])).
% 0.13/5.63 fof(f634,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,multiply(X1,X0))=commutator(X0,X1))),
% 0.13/5.63 inference(backward_demodulation,[status(thm)],[f635,f601])).
% 0.13/5.63 fof(f635,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,X1)=commutator(inverse(X1),multiply(X1,X0)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f65,f619])).
% 0.13/5.63 fof(f656,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,inverse(multiply(X0,X1)))=multiply(X0,multiply(inverse(multiply(X0,X1)),inverse(inverse(X1)))))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f451,f463])).
% 0.13/5.63 fof(f661,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,inverse(multiply(X0,X1))),X1)=multiply(multiply(X0,inverse(multiply(X0,X1))),multiply(X1,inverse(commutator(X1,X0)))))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f463,f463])).
% 0.13/5.63 fof(f662,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),X0)=multiply(multiply(X0,X1),multiply(X0,inverse(multiply(inverse(X0),X1)))))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f82,f463])).
% 0.13/5.63 fof(f679,plain,(
% 0.13/5.63 ![X0,X1,X2]: (multiply(commutator(X0,X1),X2)=multiply(X0,multiply(multiply(X1,inverse(multiply(X1,X0))),X2)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f463,f11])).
% 0.13/5.63 fof(f696,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,inverse(multiply(X0,X1)))=multiply(X0,inverse(multiply(inverse(X1),multiply(X0,X1)))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f430,f656])).
% 0.13/5.63 fof(f697,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,inverse(multiply(X0,X1)))=multiply(X0,multiply(inverse(multiply(X0,X1)),X1)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f493,f696])).
% 0.13/5.63 fof(f707,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,inverse(multiply(X0,X1))),X1)=multiply(X0,multiply(inverse(multiply(X0,X1)),multiply(X1,inverse(commutator(X1,X0))))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f11,f661])).
% 0.13/5.63 fof(f708,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),X0)=multiply(X0,multiply(X1,multiply(X0,inverse(multiply(inverse(X0),X1))))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f11,f662])).
% 0.13/5.63 fof(f709,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),X0)=multiply(X0,multiply(X1,multiply(X0,multiply(inverse(X1),X0)))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f493,f708])).
% 0.13/5.63 fof(f734,plain,(
% 0.13/5.63 ![X0,X1,X2]: (multiply(commutator(X0,X1),X2)=multiply(X0,multiply(X1,multiply(inverse(multiply(X1,X0)),X2))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f11,f679])).
% 0.13/5.63 fof(f737,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,inverse(X1))=commutator(X0,inverse(multiply(X0,X1))))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f451,f634])).
% 0.13/5.63 fof(f749,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,inverse(X1))=multiply(X0,multiply(inverse(multiply(X0,X1)),X1)))),
% 0.13/5.63 inference(backward_demodulation,[status(thm)],[f737,f697])).
% 0.13/5.63 fof(f768,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,inverse(multiply(X0,X1))),X1)=commutator(inverse(X1),commutator(X1,X0)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f463,f635])).
% 0.13/5.63 fof(f787,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(inverse(X0),commutator(X0,X1))=multiply(X1,multiply(inverse(multiply(X1,X0)),multiply(X0,inverse(commutator(X0,X1))))))),
% 0.13/5.63 inference(backward_demodulation,[status(thm)],[f768,f707])).
% 0.13/5.63 fof(f824,plain,(
% 0.13/5.63 ![X0,X1,X2]: (multiply(inverse(multiply(X0,X1)),X2)=multiply(inverse(X1),multiply(inverse(X0),X2)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f430,f11])).
% 0.13/5.63 fof(f876,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(inverse(multiply(X0,inverse(multiply(X0,inverse(X1))))),X1)=inverse(commutator(inverse(X1),X0)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f463,f493])).
% 0.13/5.63 fof(f910,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(multiply(multiply(X0,inverse(X1)),inverse(X0)),X1)=inverse(commutator(inverse(X1),X0)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f426,f876])).
% 0.13/5.63 fof(f911,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(multiply(X0,inverse(X1)),multiply(inverse(X0),X1))=inverse(commutator(inverse(X1),X0)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f11,f910])).
% 0.13/5.63 fof(f912,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(X0,multiply(inverse(X1),multiply(inverse(X0),X1)))=inverse(commutator(inverse(X1),X0)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f11,f911])).
% 0.13/5.63 fof(f913,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(X0,multiply(inverse(multiply(X0,X1)),X1))=inverse(commutator(inverse(X1),X0)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f824,f912])).
% 0.13/5.63 fof(f914,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,inverse(X1))=inverse(commutator(inverse(X1),X0)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f749,f913])).
% 0.13/5.63 fof(f955,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),inverse(X0))=inverse(commutator(X1,X0)))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f635,f914])).
% 0.13/5.63 fof(f982,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(inverse(X0),commutator(X0,X1))=multiply(X1,multiply(inverse(multiply(X1,X0)),multiply(X0,commutator(X1,X0)))))),
% 0.13/5.63 inference(backward_demodulation,[status(thm)],[f984,f787])).
% 0.13/5.63 fof(f984,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,X1)=inverse(commutator(X1,X0)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f596,f955])).
% 0.13/5.63 fof(f1021,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(commutator(X0,X1),commutator(X1,X0))=identity)),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f984,f13])).
% 0.13/5.63 fof(f2437,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(multiply(X0,X1),multiply(inverse(X0),X1))=inverse(multiply(X0,multiply(multiply(X0,X1),X0))))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f82,f521])).
% 0.13/5.63 fof(f2575,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(X0,multiply(X1,multiply(inverse(X0),X1)))=inverse(multiply(X0,multiply(multiply(X0,X1),X0))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f11,f2437])).
% 0.13/5.63 fof(f2576,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(X0,multiply(X1,multiply(inverse(X0),X1)))=inverse(multiply(X0,multiply(X0,multiply(X1,X0)))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f11,f2575])).
% 0.13/5.63 fof(f2577,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(X0,multiply(X1,multiply(inverse(X0),X1)))=inverse(multiply(inverse(X0),multiply(X1,X0))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f82,f2576])).
% 0.13/5.63 fof(f2578,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),X0)=multiply(X0,multiply(inverse(multiply(X0,X1)),X1)))),
% 0.13/5.63 inference(backward_demodulation,[status(thm)],[f2579,f709])).
% 0.13/5.63 fof(f2579,plain,(
% 0.13/5.63 ![X0,X1]: (multiply(X0,multiply(X1,multiply(inverse(X0),X1)))=multiply(inverse(multiply(X1,X0)),X0))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f493,f2577])).
% 0.13/5.63 fof(f2788,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(X0,X1),X0)=commutator(X0,inverse(X1)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f749,f2578])).
% 0.13/5.63 fof(f2821,plain,(
% 0.13/5.63 ![X0,X1,X2]: (multiply(commutator(X0,inverse(X1)),X2)=multiply(X0,multiply(inverse(X1),multiply(multiply(inverse(X0),X1),X2))))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f493,f734])).
% 0.13/5.63 fof(f2950,plain,(
% 0.13/5.63 ![X0,X1,X2]: (multiply(commutator(X0,inverse(X1)),X2)=multiply(X0,multiply(inverse(X1),multiply(inverse(X0),multiply(X1,X2)))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f11,f2821])).
% 0.13/5.63 fof(f2951,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(inverse(X0),commutator(X0,X1))=multiply(commutator(X1,inverse(X0)),commutator(X1,X0)))),
% 0.13/5.63 inference(backward_demodulation,[status(thm)],[f2953,f982])).
% 0.13/5.63 fof(f2953,plain,(
% 0.13/5.63 ![X0,X1,X2]: (multiply(commutator(X0,inverse(X1)),X2)=multiply(X0,multiply(inverse(multiply(X0,X1)),multiply(X1,X2))))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f824,f2950])).
% 0.13/5.63 fof(f3156,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,X1)=commutator(X1,inverse(multiply(inverse(X1),X0))))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f51,f2788])).
% 0.13/5.63 fof(f3163,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(multiply(inverse(X0),X1),X0)=commutator(X0,inverse(multiply(X0,X1))))),
% 0.13/5.63 inference(paramodulation,[status(thm)],[f82,f2788])).
% 0.13/5.63 fof(f3200,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(X0,X1)=commutator(X1,multiply(inverse(X0),X1)))),
% 0.13/5.63 inference(forward_demodulation,[status(thm)],[f493,f3156])).
% 0.13/5.63 fof(f3238,plain,(
% 0.13/5.63 ![X0,X1]: (commutator(inverse(X0),commutator(X0,X1))=multiply(commutator(X0,X1),commutator(X1,X0)))),
% 0.13/5.63 inference(backward_demodulation,[status(thm)],[f3248,f2951])).
% 0.13/5.63 fof(f3248,plain,(
% 0.13/5.66 ![X0,X1]: (commutator(X0,X1)=commutator(X1,inverse(X0)))),
% 0.13/5.66 inference(forward_demodulation,[status(thm)],[f634,f3200])).
% 0.13/5.66 fof(f3262,plain,(
% 0.13/5.66 ![X0,X1]: (commutator(inverse(X0),X1)=commutator(X0,inverse(multiply(X0,X1))))),
% 0.13/5.66 inference(forward_demodulation,[status(thm)],[f629,f3163])).
% 0.13/5.66 fof(f3263,plain,(
% 0.13/5.66 ![X0,X1]: (commutator(inverse(X0),X1)=commutator(X0,inverse(X1)))),
% 0.13/5.66 inference(forward_demodulation,[status(thm)],[f737,f3262])).
% 0.13/5.66 fof(f3298,plain,(
% 0.13/5.66 ![X0,X1]: (commutator(inverse(X0),X1)=commutator(X1,X0))),
% 0.13/5.66 inference(forward_demodulation,[status(thm)],[f3248,f3263])).
% 0.13/5.66 fof(f3379,plain,(
% 0.13/5.66 ![X0,X1]: (commutator(commutator(X0,X1),X0)=multiply(commutator(X0,X1),commutator(X1,X0)))),
% 0.13/5.66 inference(forward_demodulation,[status(thm)],[f3298,f3238])).
% 0.13/5.66 fof(f3382,plain,(
% 0.13/5.66 ![X0,X1]: (commutator(commutator(X0,X1),X0)=identity)),
% 0.13/5.66 inference(forward_demodulation,[status(thm)],[f1021,f3379])).
% 0.13/5.66 fof(f3475,plain,(
% 0.13/5.66 ![X0,X1]: (commutator(commutator(X0,X1),X1)=identity)),
% 0.13/5.66 inference(paramodulation,[status(thm)],[f3248,f3382])).
% 0.13/5.66 fof(f3499,plain,(
% 0.13/5.66 ~identity=identity),
% 0.13/5.66 inference(backward_demodulation,[status(thm)],[f3475,f16])).
% 0.13/5.66 fof(f3512,plain,(
% 0.13/5.66 $false),
% 0.13/5.66 inference(trivial_equality_resolution,[status(thm)],[f3499])).
% 0.13/5.66 % SZS output end CNFRefutation for theBenchmark.p
% 10.32/6.87 % Elapsed time: 1.277459 seconds
% 10.32/6.87 % CPU time: 1.011842 seconds
% 10.32/6.87 % Total memory used: 27.350 MB
% 10.32/6.87 % Net memory used: 26.752 MB
%------------------------------------------------------------------------------