%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP202-1 : TPTP v9.3.1. Released v2.2.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:36:15 PM UTC 2026
% Result : Unsatisfiable 85.54s 11.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP202-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.49 % Computer : n008.cluster.edu
% 0.17/0.49 % Model : x86_64 x86_64
% 0.17/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.49 % Memory : 8046.5625MB
% 0.17/0.49 % OS : Linux 6.8.0-71-generic
% 0.17/0.49 % CPULimit : 300
% 0.17/0.49 % WCLimit : 300
% 0.17/0.49 % DateTime : Sun Sep 20 20:06:55 UTC 2026
% 0.17/0.50 % CPUTime :
% 0.17/0.52 % Drodi V4.1.1
% 85.54/11.94 % Refutation found
% 85.54/11.94 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 85.54/11.94 % SZS output start CNFRefutation for theBenchmark
% 85.54/11.94 fof(f1,axiom,(
% 85.54/11.94 (![X]: (multiply(identity,X) = X ))),
% 85.54/11.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 85.54/11.94 fof(f2,axiom,(
% 85.54/11.94 (![X]: (multiply(X,identity) = X ))),
% 85.54/11.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 85.54/11.94 fof(f3,axiom,(
% 85.54/11.94 (![X,Y]: (multiply(X,left_division(X,Y)) = Y ))),
% 85.54/11.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 85.54/11.94 fof(f4,axiom,(
% 85.54/11.94 (![X,Y]: (left_division(X,multiply(X,Y)) = Y ))),
% 85.54/11.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 85.54/11.94 fof(f5,axiom,(
% 85.54/11.94 (![X,Y]: (multiply(right_division(X,Y),Y) = X ))),
% 85.54/11.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 85.54/11.94 fof(f6,axiom,(
% 85.54/11.94 (![X,Y]: (right_division(multiply(X,Y),Y) = X ))),
% 85.54/11.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 85.54/11.94 fof(f7,axiom,(
% 85.54/11.94 (![X]: (multiply(X,right_inverse(X)) = identity ))),
% 85.54/11.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 85.54/11.94 fof(f8,axiom,(
% 85.54/11.94 (![X]: (multiply(left_inverse(X),X) = identity ))),
% 85.54/11.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 85.54/11.94 fof(f9,axiom,(
% 85.54/11.94 (![X,Y,Z]: (multiply(multiply(multiply(X,Y),X),Z) = multiply(X,multiply(Y,multiply(X,Z))) ))),
% 85.54/11.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 85.54/11.94 fof(f10,negated_conjecture,(
% 85.54/11.94 multiply(multiply(a,multiply(b,c)),a) != multiply(multiply(a,b),multiply(c,a)) ),
% 85.54/11.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 85.54/11.94 fof(f11,plain,(
% 85.54/11.94 ![X0]: (multiply(identity,X0)=X0)),
% 85.54/11.94 inference(cnf_transformation,[status(thm)],[f1])).
% 85.54/11.94 fof(f12,plain,(
% 85.54/11.94 ![X0]: (multiply(X0,identity)=X0)),
% 85.54/11.94 inference(cnf_transformation,[status(thm)],[f2])).
% 85.54/11.94 fof(f13,plain,(
% 85.54/11.94 ![X0,X1]: (multiply(X0,left_division(X0,X1))=X1)),
% 85.54/11.94 inference(cnf_transformation,[status(thm)],[f3])).
% 85.54/11.94 fof(f14,plain,(
% 85.54/11.94 ![X0,X1]: (left_division(X0,multiply(X0,X1))=X1)),
% 85.54/11.94 inference(cnf_transformation,[status(thm)],[f4])).
% 85.54/11.94 fof(f15,plain,(
% 85.54/11.94 ![X0,X1]: (multiply(right_division(X0,X1),X1)=X0)),
% 85.54/11.94 inference(cnf_transformation,[status(thm)],[f5])).
% 85.54/11.94 fof(f16,plain,(
% 85.54/11.94 ![X0,X1]: (right_division(multiply(X0,X1),X1)=X0)),
% 85.54/11.94 inference(cnf_transformation,[status(thm)],[f6])).
% 85.54/11.94 fof(f17,plain,(
% 85.54/11.94 ![X0]: (multiply(X0,right_inverse(X0))=identity)),
% 85.54/11.94 inference(cnf_transformation,[status(thm)],[f7])).
% 85.54/11.94 fof(f18,plain,(
% 85.54/11.94 ![X0]: (multiply(left_inverse(X0),X0)=identity)),
% 85.54/11.94 inference(cnf_transformation,[status(thm)],[f8])).
% 85.54/11.94 fof(f19,plain,(
% 85.54/11.94 ![X0,X1,X2]: (multiply(multiply(multiply(X0,X1),X0),X2)=multiply(X0,multiply(X1,multiply(X0,X2))))),
% 85.54/11.94 inference(cnf_transformation,[status(thm)],[f9])).
% 85.54/11.94 fof(f20,plain,(
% 85.54/11.94 ~multiply(multiply(a,multiply(b,c)),a)=multiply(multiply(a,b),multiply(c,a))),
% 85.54/11.94 inference(cnf_transformation,[status(thm)],[f10])).
% 85.54/11.94 fof(f37,plain,(
% 85.54/11.94 ![X0]: (right_division(X0,X0)=identity)),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f11,f16])).
% 85.54/11.94 fof(f38,plain,(
% 85.54/11.94 ![X0,X1]: (right_division(X0,left_division(X1,X0))=X1)),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f13,f16])).
% 85.54/11.94 fof(f44,plain,(
% 85.54/11.94 ![X0,X1]: (left_division(right_division(X0,X1),X0)=X1)),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f15,f14])).
% 85.54/11.94 fof(f48,plain,(
% 85.54/11.94 ![X0]: (right_division(identity,right_inverse(X0))=X0)),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f17,f16])).
% 85.54/11.94 fof(f49,plain,(
% 85.54/11.94 ![X0]: (left_division(X0,identity)=right_inverse(X0))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f17,f14])).
% 85.54/11.94 fof(f53,plain,(
% 85.54/11.94 ![X0]: (right_division(identity,X0)=left_inverse(X0))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f18,f16])).
% 85.54/11.94 fof(f57,plain,(
% 85.54/11.94 ![X0,X1,X2]: (X0=multiply(X1,multiply(X2,multiply(X1,left_division(multiply(multiply(X1,X2),X1),X0)))))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f13,f19])).
% 85.54/11.94 fof(f58,plain,(
% 85.54/11.94 ![X0,X1]: (multiply(multiply(X0,X1),X0)=multiply(X0,multiply(X1,multiply(X0,identity))))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f12,f19])).
% 85.54/11.94 fof(f67,plain,(
% 85.54/11.94 ![X0,X1]: (multiply(multiply(X0,X0),X1)=multiply(X0,multiply(identity,multiply(X0,X1))))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f12,f19])).
% 85.54/11.94 fof(f71,plain,(
% 85.54/11.94 ![X0,X1,X2]: (right_division(multiply(X0,multiply(X1,multiply(X0,X2))),X2)=multiply(multiply(X0,X1),X0))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f19,f16])).
% 85.54/11.94 fof(f73,plain,(
% 85.54/11.94 ![X0,X1]: (multiply(multiply(X0,X1),X0)=multiply(X0,multiply(X1,X0)))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f12,f58])).
% 85.54/11.94 fof(f82,plain,(
% 85.54/11.94 ![X0,X1]: (multiply(multiply(X0,X0),X1)=multiply(X0,multiply(X0,X1)))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f11,f67])).
% 85.54/11.94 fof(f94,plain,(
% 85.54/11.94 ![X0,X1]: (right_division(multiply(X0,multiply(X1,X0)),X0)=multiply(X0,X1))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f73,f16])).
% 85.54/11.94 fof(f106,plain,(
% 85.54/11.94 ![X0,X1]: (X0=multiply(X1,multiply(X1,left_division(multiply(X1,X1),X0))))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f13,f82])).
% 85.54/11.94 fof(f129,plain,(
% 85.54/11.94 ![X0]: (right_division(multiply(X0,identity),X0)=multiply(X0,left_inverse(X0)))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f18,f94])).
% 85.54/11.94 fof(f130,plain,(
% 85.54/11.94 ![X0,X1]: (right_division(multiply(X0,X1),X0)=multiply(X0,right_division(X1,X0)))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f15,f94])).
% 85.54/11.94 fof(f132,plain,(
% 85.54/11.94 ![X0]: (right_division(multiply(right_inverse(X0),identity),right_inverse(X0))=multiply(right_inverse(X0),X0))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f17,f94])).
% 85.54/11.94 fof(f138,plain,(
% 85.54/11.94 ![X0]: (right_division(X0,X0)=multiply(X0,left_inverse(X0)))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f12,f129])).
% 85.54/11.94 fof(f139,plain,(
% 85.54/11.94 ![X0]: (identity=multiply(X0,left_inverse(X0)))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f37,f138])).
% 85.54/11.94 fof(f141,plain,(
% 85.54/11.94 ![X0]: (right_division(right_inverse(X0),right_inverse(X0))=multiply(right_inverse(X0),X0))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f12,f132])).
% 85.54/11.94 fof(f142,plain,(
% 85.54/11.94 ![X0]: (identity=multiply(right_inverse(X0),X0))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f37,f141])).
% 85.54/11.94 fof(f152,plain,(
% 85.54/11.94 ![X0]: (right_division(identity,left_inverse(X0))=X0)),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f139,f16])).
% 85.54/11.94 fof(f158,plain,(
% 85.54/11.94 ~multiply(a,multiply(multiply(b,c),a))=multiply(multiply(a,b),multiply(c,a))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f73,f20])).
% 85.54/11.94 fof(f184,plain,(
% 85.54/11.94 ![X0,X1]: (left_division(X0,X1)=multiply(X0,left_division(multiply(X0,X0),X1)))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f106,f14])).
% 85.54/11.94 fof(f320,plain,(
% 85.54/11.94 ![X0,X1]: (right_division(X0,X1)=multiply(X1,right_division(multiply(X1,left_division(multiply(X1,X1),X0)),X1)))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f106,f130])).
% 85.54/11.94 fof(f335,plain,(
% 85.54/11.94 ![X0,X1]: (right_division(X0,X1)=multiply(X1,multiply(X1,right_division(left_division(multiply(X1,X1),X0),X1))))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f130,f320])).
% 85.54/11.94 fof(f399,plain,(
% 85.54/11.94 ![X0,X1,X2]: (right_division(multiply(X0,multiply(X1,multiply(X0,X2))),X2)=multiply(X0,multiply(X1,X0)))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f73,f71])).
% 85.54/11.94 fof(f892,plain,(
% 85.54/11.94 ![X0]: (left_inverse(right_inverse(X0))=X0)),
% 85.54/11.94 inference(backward_demodulation,[status(thm)],[f53,f48])).
% 85.54/11.94 fof(f1032,plain,(
% 85.54/11.94 ![X0]: (left_inverse(left_inverse(X0))=X0)),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f53,f152])).
% 85.54/11.94 fof(f1034,plain,(
% 85.54/11.94 ![X0]: (left_inverse(X0)=right_inverse(X0))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f892,f1032])).
% 85.54/11.94 fof(f1040,plain,(
% 85.54/11.94 ![X0]: (right_inverse(left_inverse(X0))=X0)),
% 85.54/11.94 inference(backward_demodulation,[status(thm)],[f1034,f1032])).
% 85.54/11.94 fof(f1048,plain,(
% 85.54/11.94 ![X0]: (right_inverse(right_inverse(X0))=X0)),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f1034,f1040])).
% 85.54/11.94 fof(f1054,plain,(
% 85.54/11.94 ![X0,X1,X2]: (X0=multiply(X1,multiply(X2,multiply(X1,left_division(multiply(X1,multiply(X2,X1)),X0)))))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f73,f57])).
% 85.54/11.94 fof(f1099,plain,(
% 85.54/11.94 ![X0,X1,X2]: (left_division(X0,X1)=multiply(X2,multiply(X0,left_division(multiply(X0,multiply(X2,X0)),X1))))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f1054,f14])).
% 85.54/11.94 fof(f1158,plain,(
% 85.54/11.94 ![X0,X1]: (left_division(X0,X1)=multiply(right_inverse(X0),multiply(X0,left_division(multiply(X0,identity),X1))))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f142,f1099])).
% 85.54/11.94 fof(f1162,plain,(
% 85.54/11.94 ![X0,X1,X2]: (left_division(X0,X1)=multiply(right_division(X2,X0),multiply(X0,left_division(multiply(X0,X2),X1))))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f15,f1099])).
% 85.54/11.94 fof(f1203,plain,(
% 85.54/11.94 ![X0,X1]: (left_division(X0,X1)=multiply(right_inverse(X0),multiply(X0,left_division(X0,X1))))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f12,f1158])).
% 85.54/11.94 fof(f1204,plain,(
% 85.54/11.94 ![X0,X1]: (left_division(X0,X1)=multiply(right_inverse(X0),X1))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f13,f1203])).
% 85.54/11.94 fof(f1366,plain,(
% 85.54/11.94 ![X0,X1,X2]: (left_division(X0,X1)=multiply(multiply(X0,right_division(X2,X0)),multiply(X0,left_division(multiply(X0,multiply(X0,X2)),X1))))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f130,f1162])).
% 85.54/11.94 fof(f2098,plain,(
% 85.54/11.94 ![X0,X1,X2]: (left_division(X0,multiply(multiply(X0,multiply(X0,X1)),X2))=multiply(multiply(X0,right_division(X1,X0)),multiply(X0,X2)))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f14,f1366])).
% 85.54/11.94 fof(f3343,plain,(
% 85.54/11.94 ![X0,X1,X2]: (left_division(X0,multiply(multiply(X0,left_division(X0,X1)),X2))=multiply(multiply(X0,right_division(left_division(multiply(X0,X0),X1),X0)),multiply(X0,X2)))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f184,f2098])).
% 85.54/11.94 fof(f3447,plain,(
% 85.54/11.94 ![X0,X1,X2]: (left_division(X0,multiply(X1,X2))=multiply(multiply(X0,right_division(left_division(multiply(X0,X0),X1),X0)),multiply(X0,X2)))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f13,f3343])).
% 85.54/11.94 fof(f5542,plain,(
% 85.54/11.94 ![X0,X1]: (left_division(X0,multiply(X1,right_inverse(X0)))=multiply(multiply(X0,right_division(left_division(multiply(X0,X0),X1),X0)),identity))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f17,f3447])).
% 85.54/11.94 fof(f5693,plain,(
% 85.54/11.94 ![X0,X1]: (left_division(X0,multiply(X1,right_inverse(X0)))=multiply(X0,right_division(left_division(multiply(X0,X0),X1),X0)))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f12,f5542])).
% 85.54/11.94 fof(f5765,plain,(
% 85.54/11.94 ![X0,X1]: (right_division(X0,X1)=multiply(X1,left_division(X1,multiply(X0,right_inverse(X1)))))),
% 85.54/11.94 inference(backward_demodulation,[status(thm)],[f5693,f335])).
% 85.54/11.94 fof(f5821,plain,(
% 85.54/11.94 ![X0,X1]: (right_division(X0,X1)=multiply(X0,right_inverse(X1)))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f13,f5765])).
% 85.54/11.94 fof(f5920,plain,(
% 85.54/11.94 ![X0,X1]: (right_division(multiply(X0,X0),X1)=multiply(X0,multiply(X0,right_inverse(X1))))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f82,f5821])).
% 85.54/11.94 fof(f5924,plain,(
% 85.54/11.94 ![X0,X1]: (right_division(X0,right_inverse(X1))=multiply(X0,X1))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f1048,f5821])).
% 85.54/11.94 fof(f5972,plain,(
% 85.54/11.94 ![X0,X1]: (right_division(multiply(X0,X0),X1)=multiply(X0,right_division(X0,X1)))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f5821,f5920])).
% 85.54/11.94 fof(f6052,plain,(
% 85.54/11.94 ![X0,X1,X2]: (multiply(X0,multiply(X1,X0))=multiply(multiply(X0,multiply(X1,multiply(X0,right_inverse(X2)))),X2))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f399,f5924])).
% 85.54/11.94 fof(f6054,plain,(
% 85.54/11.94 ![X0,X1]: (multiply(right_inverse(X0),right_division(X1,right_inverse(X0)))=multiply(multiply(right_inverse(X0),X1),X0))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f130,f5924])).
% 85.54/11.94 fof(f6080,plain,(
% 85.54/11.94 ![X0,X1,X2]: (multiply(X0,multiply(X1,X0))=multiply(multiply(X0,multiply(X1,right_division(X0,X2))),X2))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f5821,f6052])).
% 85.54/11.94 fof(f6082,plain,(
% 85.54/11.94 ![X0,X1]: (left_division(X0,right_division(X1,right_inverse(X0)))=multiply(multiply(right_inverse(X0),X1),X0))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f1204,f6054])).
% 85.54/11.94 fof(f6083,plain,(
% 85.54/11.94 ![X0,X1]: (left_division(X0,multiply(X1,X0))=multiply(multiply(right_inverse(X0),X1),X0))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f5924,f6082])).
% 85.54/11.94 fof(f6084,plain,(
% 85.54/11.94 ![X0,X1]: (left_division(X0,multiply(X1,X0))=multiply(left_division(X0,X1),X0))),
% 85.54/11.94 inference(forward_demodulation,[status(thm)],[f1204,f6083])).
% 85.54/11.94 fof(f6155,plain,(
% 85.54/11.94 ![X0]: (identity=multiply(X0,right_division(X0,multiply(X0,X0))))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f37,f5972])).
% 85.54/11.94 fof(f6250,plain,(
% 85.54/11.94 ![X0,X1]: (left_division(right_division(X0,multiply(X0,X0)),X1)=multiply(X0,multiply(right_division(X0,multiply(X0,X0)),left_division(multiply(right_division(X0,multiply(X0,X0)),identity),X1))))),
% 85.54/11.94 inference(paramodulation,[status(thm)],[f6155,f1099])).
% 88.44/12.06 fof(f6324,plain,(
% 88.44/12.06 ![X0,X1]: (left_division(right_division(X0,multiply(X0,X0)),X1)=multiply(X0,multiply(right_division(X0,multiply(X0,X0)),left_division(right_division(X0,multiply(X0,X0)),X1))))),
% 88.44/12.06 inference(forward_demodulation,[status(thm)],[f12,f6250])).
% 88.44/12.06 fof(f6325,plain,(
% 88.44/12.06 ![X0,X1]: (left_division(right_division(X0,multiply(X0,X0)),X1)=multiply(X0,X1))),
% 88.44/12.06 inference(forward_demodulation,[status(thm)],[f13,f6324])).
% 88.44/12.06 fof(f6447,plain,(
% 88.44/12.06 ![X0]: (left_division(right_division(X0,multiply(X0,X0)),identity)=multiply(left_division(right_division(X0,multiply(X0,X0)),X0),right_division(X0,multiply(X0,X0))))),
% 88.44/12.06 inference(paramodulation,[status(thm)],[f6155,f6084])).
% 88.44/12.06 fof(f6495,plain,(
% 88.44/12.06 ![X0]: (right_inverse(right_division(X0,multiply(X0,X0)))=multiply(left_division(right_division(X0,multiply(X0,X0)),X0),right_division(X0,multiply(X0,X0))))),
% 88.44/12.06 inference(forward_demodulation,[status(thm)],[f49,f6447])).
% 88.44/12.06 fof(f6496,plain,(
% 88.44/12.06 ![X0]: (right_inverse(right_division(X0,multiply(X0,X0)))=multiply(multiply(X0,X0),right_division(X0,multiply(X0,X0))))),
% 88.44/12.06 inference(forward_demodulation,[status(thm)],[f44,f6495])).
% 88.44/12.06 fof(f6497,plain,(
% 88.44/12.06 ![X0]: (right_inverse(right_division(X0,multiply(X0,X0)))=multiply(X0,multiply(X0,right_division(X0,multiply(X0,X0)))))),
% 88.44/12.06 inference(forward_demodulation,[status(thm)],[f82,f6496])).
% 88.44/12.06 fof(f6498,plain,(
% 88.44/12.06 ![X0]: (right_inverse(right_division(X0,multiply(X0,X0)))=multiply(X0,identity))),
% 88.44/12.06 inference(forward_demodulation,[status(thm)],[f6155,f6497])).
% 88.44/12.06 fof(f6499,plain,(
% 88.44/12.06 ![X0]: (right_inverse(right_division(X0,multiply(X0,X0)))=X0)),
% 88.44/12.06 inference(forward_demodulation,[status(thm)],[f12,f6498])).
% 88.44/12.06 fof(f6538,plain,(
% 88.44/12.06 ![X0,X1]: (right_division(X0,X1)=multiply(X0,right_division(X1,multiply(X1,X1))))),
% 88.44/12.06 inference(paramodulation,[status(thm)],[f6499,f5924])).
% 88.44/12.06 fof(f6836,plain,(
% 88.44/12.06 ![X0,X1]: (right_division(X0,multiply(X1,X0))=right_division(X1,multiply(X1,X1)))),
% 88.44/12.06 inference(paramodulation,[status(thm)],[f6325,f38])).
% 88.44/12.06 fof(f7663,plain,(
% 88.44/12.06 ![X0,X1,X2]: (right_division(X0,X1)=multiply(X0,right_division(X2,multiply(X1,X2))))),
% 88.44/12.06 inference(paramodulation,[status(thm)],[f6836,f6538])).
% 88.44/12.06 fof(f9756,plain,(
% 88.44/12.06 ![X0,X1,X2]: (multiply(X0,multiply(X1,X0))=multiply(multiply(X0,right_division(X1,X2)),multiply(X2,X0)))),
% 88.44/12.06 inference(paramodulation,[status(thm)],[f7663,f6080])).
% 88.44/12.06 fof(f31096,plain,(
% 88.44/12.06 ![X0,X1,X2]: (multiply(X0,multiply(multiply(X1,X2),X0))=multiply(multiply(X0,X1),multiply(X2,X0)))),
% 88.44/12.06 inference(paramodulation,[status(thm)],[f16,f9756])).
% 88.44/12.06 fof(f67366,plain,(
% 88.44/12.06 ~multiply(a,multiply(multiply(b,c),a))=multiply(a,multiply(multiply(b,c),a))),
% 88.44/12.06 inference(backward_demodulation,[status(thm)],[f31096,f158])).
% 88.44/12.06 fof(f67663,plain,(
% 88.44/12.06 $false),
% 88.44/12.06 inference(trivial_equality_resolution,[status(thm)],[f67366])).
% 88.44/12.06 % SZS output end CNFRefutation for theBenchmark.p
% 8.85/12.38 % Elapsed time: 11.817723 seconds
% 8.85/12.38 % CPU time: 90.013930 seconds
% 8.85/12.38 % Total memory used: 1.055 GB
% 8.85/12.38 % Net memory used: 1.045 GB
%------------------------------------------------------------------------------