%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP205-1 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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 117.54s 20.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP205-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/5.54 % Computer : n006.cluster.edu
% 0.12/5.54 % Model : x86_64 x86_64
% 0.12/5.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.54 % Memory : 8046.5625MB
% 0.12/5.54 % OS : Linux 6.8.0-71-generic
% 0.12/5.54 % CPULimit : 300
% 0.12/5.54 % WCLimit : 300
% 0.12/5.54 % DateTime : Sun Sep 20 20:06:03 UTC 2026
% 0.12/5.55 % CPUTime :
% 0.12/5.55 % Drodi V4.1.1
% 117.54/20.51 % Refutation found
% 117.54/20.51 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 117.54/20.51 % SZS output start CNFRefutation for theBenchmark
% 117.54/20.51 fof(f1,axiom,(
% 117.54/20.51 (![X]: (multiply(identity,X) = X ))),
% 117.54/20.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.54/20.51 fof(f2,axiom,(
% 117.54/20.51 (![X]: (multiply(X,identity) = X ))),
% 117.54/20.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.54/20.51 fof(f3,axiom,(
% 117.54/20.51 (![X,Y]: (multiply(X,left_division(X,Y)) = Y ))),
% 117.54/20.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.54/20.51 fof(f4,axiom,(
% 117.54/20.51 (![X,Y]: (left_division(X,multiply(X,Y)) = Y ))),
% 117.54/20.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.54/20.51 fof(f5,axiom,(
% 117.54/20.51 (![X,Y]: (multiply(right_division(X,Y),Y) = X ))),
% 117.54/20.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.54/20.51 fof(f6,axiom,(
% 117.54/20.51 (![X,Y]: (right_division(multiply(X,Y),Y) = X ))),
% 117.54/20.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.54/20.51 fof(f7,axiom,(
% 117.54/20.51 (![X]: (multiply(X,right_inverse(X)) = identity ))),
% 117.54/20.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.54/20.51 fof(f8,axiom,(
% 117.54/20.51 (![X]: (multiply(left_inverse(X),X) = identity ))),
% 117.54/20.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.54/20.51 fof(f9,axiom,(
% 117.54/20.51 (![X,Y,Z]: (multiply(multiply(multiply(X,Y),X),Z) = multiply(X,multiply(Y,multiply(X,Z))) ))),
% 117.54/20.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.54/20.51 fof(f10,negated_conjecture,(
% 117.54/20.51 multiply(x,multiply(multiply(y,z),x)) != multiply(multiply(x,y),multiply(z,x)) ),
% 117.54/20.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.54/20.51 fof(f11,plain,(
% 117.54/20.51 ![X0]: (multiply(identity,X0)=X0)),
% 117.54/20.51 inference(cnf_transformation,[status(thm)],[f1])).
% 117.54/20.51 fof(f12,plain,(
% 117.54/20.51 ![X0]: (multiply(X0,identity)=X0)),
% 117.54/20.51 inference(cnf_transformation,[status(thm)],[f2])).
% 117.54/20.51 fof(f13,plain,(
% 117.54/20.51 ![X0,X1]: (multiply(X0,left_division(X0,X1))=X1)),
% 117.54/20.51 inference(cnf_transformation,[status(thm)],[f3])).
% 117.54/20.51 fof(f14,plain,(
% 117.54/20.51 ![X0,X1]: (left_division(X0,multiply(X0,X1))=X1)),
% 117.54/20.51 inference(cnf_transformation,[status(thm)],[f4])).
% 117.54/20.51 fof(f15,plain,(
% 117.54/20.51 ![X0,X1]: (multiply(right_division(X0,X1),X1)=X0)),
% 117.54/20.51 inference(cnf_transformation,[status(thm)],[f5])).
% 117.54/20.51 fof(f16,plain,(
% 117.54/20.51 ![X0,X1]: (right_division(multiply(X0,X1),X1)=X0)),
% 117.54/20.51 inference(cnf_transformation,[status(thm)],[f6])).
% 117.54/20.51 fof(f17,plain,(
% 117.54/20.51 ![X0]: (multiply(X0,right_inverse(X0))=identity)),
% 117.54/20.51 inference(cnf_transformation,[status(thm)],[f7])).
% 117.54/20.51 fof(f18,plain,(
% 117.54/20.51 ![X0]: (multiply(left_inverse(X0),X0)=identity)),
% 117.54/20.51 inference(cnf_transformation,[status(thm)],[f8])).
% 117.54/20.51 fof(f19,plain,(
% 117.54/20.51 ![X0,X1,X2]: (multiply(multiply(multiply(X0,X1),X0),X2)=multiply(X0,multiply(X1,multiply(X0,X2))))),
% 117.54/20.51 inference(cnf_transformation,[status(thm)],[f9])).
% 117.54/20.51 fof(f20,plain,(
% 117.54/20.51 ~multiply(x,multiply(multiply(y,z),x))=multiply(multiply(x,y),multiply(z,x))),
% 117.54/20.51 inference(cnf_transformation,[status(thm)],[f10])).
% 117.54/20.51 fof(f37,plain,(
% 117.54/20.51 ![X0]: (right_division(X0,X0)=identity)),
% 117.54/20.51 inference(paramodulation,[status(thm)],[f11,f16])).
% 117.54/20.51 fof(f38,plain,(
% 117.54/20.51 ![X0,X1]: (right_division(X0,left_division(X1,X0))=X1)),
% 117.54/20.51 inference(paramodulation,[status(thm)],[f13,f16])).
% 117.54/20.51 fof(f44,plain,(
% 117.54/20.51 ![X0,X1]: (left_division(right_division(X0,X1),X0)=X1)),
% 117.54/20.51 inference(paramodulation,[status(thm)],[f15,f14])).
% 117.54/20.51 fof(f48,plain,(
% 117.54/20.51 ![X0]: (right_division(identity,right_inverse(X0))=X0)),
% 117.54/20.51 inference(paramodulation,[status(thm)],[f17,f16])).
% 117.54/20.51 fof(f49,plain,(
% 117.54/20.51 ![X0]: (left_division(X0,identity)=right_inverse(X0))),
% 117.54/20.51 inference(paramodulation,[status(thm)],[f17,f14])).
% 117.54/20.51 fof(f53,plain,(
% 117.54/20.51 ![X0]: (right_division(identity,X0)=left_inverse(X0))),
% 117.54/20.51 inference(paramodulation,[status(thm)],[f18,f16])).
% 117.54/20.51 fof(f57,plain,(
% 117.54/20.51 ![X0,X1,X2]: (X0=multiply(X1,multiply(X2,multiply(X1,left_division(multiply(multiply(X1,X2),X1),X0)))))),
% 117.54/20.51 inference(paramodulation,[status(thm)],[f13,f19])).
% 117.54/20.51 fof(f58,plain,(
% 117.54/20.51 ![X0,X1]: (multiply(multiply(X0,X1),X0)=multiply(X0,multiply(X1,multiply(X0,identity))))),
% 117.54/20.51 inference(paramodulation,[status(thm)],[f12,f19])).
% 117.54/20.51 fof(f67,plain,(
% 117.54/20.51 ![X0,X1]: (multiply(multiply(X0,X0),X1)=multiply(X0,multiply(identity,multiply(X0,X1))))),
% 117.54/20.51 inference(paramodulation,[status(thm)],[f12,f19])).
% 117.54/20.51 fof(f71,plain,(
% 117.54/20.51 ![X0,X1,X2]: (right_division(multiply(X0,multiply(X1,multiply(X0,X2))),X2)=multiply(multiply(X0,X1),X0))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f19,f16])).
% 117.54/20.52 fof(f73,plain,(
% 117.54/20.52 ![X0,X1]: (multiply(multiply(X0,X1),X0)=multiply(X0,multiply(X1,X0)))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f12,f58])).
% 117.54/20.52 fof(f82,plain,(
% 117.54/20.52 ![X0,X1]: (multiply(multiply(X0,X0),X1)=multiply(X0,multiply(X0,X1)))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f11,f67])).
% 117.54/20.52 fof(f94,plain,(
% 117.54/20.52 ![X0,X1]: (right_division(multiply(X0,multiply(X1,X0)),X0)=multiply(X0,X1))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f73,f16])).
% 117.54/20.52 fof(f106,plain,(
% 117.54/20.52 ![X0,X1]: (X0=multiply(X1,multiply(X1,left_division(multiply(X1,X1),X0))))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f13,f82])).
% 117.54/20.52 fof(f129,plain,(
% 117.54/20.52 ![X0]: (right_division(multiply(X0,identity),X0)=multiply(X0,left_inverse(X0)))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f18,f94])).
% 117.54/20.52 fof(f130,plain,(
% 117.54/20.52 ![X0,X1]: (right_division(multiply(X0,X1),X0)=multiply(X0,right_division(X1,X0)))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f15,f94])).
% 117.54/20.52 fof(f132,plain,(
% 117.54/20.52 ![X0]: (right_division(multiply(right_inverse(X0),identity),right_inverse(X0))=multiply(right_inverse(X0),X0))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f17,f94])).
% 117.54/20.52 fof(f138,plain,(
% 117.54/20.52 ![X0]: (right_division(X0,X0)=multiply(X0,left_inverse(X0)))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f12,f129])).
% 117.54/20.52 fof(f139,plain,(
% 117.54/20.52 ![X0]: (identity=multiply(X0,left_inverse(X0)))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f37,f138])).
% 117.54/20.52 fof(f141,plain,(
% 117.54/20.52 ![X0]: (right_division(right_inverse(X0),right_inverse(X0))=multiply(right_inverse(X0),X0))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f12,f132])).
% 117.54/20.52 fof(f142,plain,(
% 117.54/20.52 ![X0]: (identity=multiply(right_inverse(X0),X0))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f37,f141])).
% 117.54/20.52 fof(f152,plain,(
% 117.54/20.52 ![X0]: (right_division(identity,left_inverse(X0))=X0)),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f139,f16])).
% 117.54/20.52 fof(f183,plain,(
% 117.54/20.52 ![X0,X1]: (left_division(X0,X1)=multiply(X0,left_division(multiply(X0,X0),X1)))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f106,f14])).
% 117.54/20.52 fof(f319,plain,(
% 117.54/20.52 ![X0,X1]: (right_division(X0,X1)=multiply(X1,right_division(multiply(X1,left_division(multiply(X1,X1),X0)),X1)))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f106,f130])).
% 117.54/20.52 fof(f334,plain,(
% 117.54/20.52 ![X0,X1]: (right_division(X0,X1)=multiply(X1,multiply(X1,right_division(left_division(multiply(X1,X1),X0),X1))))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f130,f319])).
% 117.54/20.52 fof(f398,plain,(
% 117.54/20.52 ![X0,X1,X2]: (right_division(multiply(X0,multiply(X1,multiply(X0,X2))),X2)=multiply(X0,multiply(X1,X0)))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f73,f71])).
% 117.54/20.52 fof(f891,plain,(
% 117.54/20.52 ![X0]: (left_inverse(right_inverse(X0))=X0)),
% 117.54/20.52 inference(backward_demodulation,[status(thm)],[f53,f48])).
% 117.54/20.52 fof(f1031,plain,(
% 117.54/20.52 ![X0]: (left_inverse(left_inverse(X0))=X0)),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f53,f152])).
% 117.54/20.52 fof(f1033,plain,(
% 117.54/20.52 ![X0]: (left_inverse(X0)=right_inverse(X0))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f891,f1031])).
% 117.54/20.52 fof(f1039,plain,(
% 117.54/20.52 ![X0]: (right_inverse(left_inverse(X0))=X0)),
% 117.54/20.52 inference(backward_demodulation,[status(thm)],[f1033,f1031])).
% 117.54/20.52 fof(f1047,plain,(
% 117.54/20.52 ![X0]: (right_inverse(right_inverse(X0))=X0)),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f1033,f1039])).
% 117.54/20.52 fof(f1053,plain,(
% 117.54/20.52 ![X0,X1,X2]: (X0=multiply(X1,multiply(X2,multiply(X1,left_division(multiply(X1,multiply(X2,X1)),X0)))))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f73,f57])).
% 117.54/20.52 fof(f1098,plain,(
% 117.54/20.52 ![X0,X1,X2]: (left_division(X0,X1)=multiply(X2,multiply(X0,left_division(multiply(X0,multiply(X2,X0)),X1))))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f1053,f14])).
% 117.54/20.52 fof(f1157,plain,(
% 117.54/20.52 ![X0,X1]: (left_division(X0,X1)=multiply(right_inverse(X0),multiply(X0,left_division(multiply(X0,identity),X1))))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f142,f1098])).
% 117.54/20.52 fof(f1161,plain,(
% 117.54/20.52 ![X0,X1,X2]: (left_division(X0,X1)=multiply(right_division(X2,X0),multiply(X0,left_division(multiply(X0,X2),X1))))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f15,f1098])).
% 117.54/20.52 fof(f1202,plain,(
% 117.54/20.52 ![X0,X1]: (left_division(X0,X1)=multiply(right_inverse(X0),multiply(X0,left_division(X0,X1))))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f12,f1157])).
% 117.54/20.52 fof(f1203,plain,(
% 117.54/20.52 ![X0,X1]: (left_division(X0,X1)=multiply(right_inverse(X0),X1))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f13,f1202])).
% 117.54/20.52 fof(f1365,plain,(
% 117.54/20.52 ![X0,X1,X2]: (left_division(X0,X1)=multiply(multiply(X0,right_division(X2,X0)),multiply(X0,left_division(multiply(X0,multiply(X0,X2)),X1))))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f130,f1161])).
% 117.54/20.52 fof(f2097,plain,(
% 117.54/20.52 ![X0,X1,X2]: (left_division(X0,multiply(multiply(X0,multiply(X0,X1)),X2))=multiply(multiply(X0,right_division(X1,X0)),multiply(X0,X2)))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f14,f1365])).
% 117.54/20.52 fof(f3342,plain,(
% 117.54/20.52 ![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)))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f183,f2097])).
% 117.54/20.52 fof(f3446,plain,(
% 117.54/20.52 ![X0,X1,X2]: (left_division(X0,multiply(X1,X2))=multiply(multiply(X0,right_division(left_division(multiply(X0,X0),X1),X0)),multiply(X0,X2)))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f13,f3342])).
% 117.54/20.52 fof(f5541,plain,(
% 117.54/20.52 ![X0,X1]: (left_division(X0,multiply(X1,right_inverse(X0)))=multiply(multiply(X0,right_division(left_division(multiply(X0,X0),X1),X0)),identity))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f17,f3446])).
% 117.54/20.52 fof(f5692,plain,(
% 117.54/20.52 ![X0,X1]: (left_division(X0,multiply(X1,right_inverse(X0)))=multiply(X0,right_division(left_division(multiply(X0,X0),X1),X0)))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f12,f5541])).
% 117.54/20.52 fof(f5764,plain,(
% 117.54/20.52 ![X0,X1]: (right_division(X0,X1)=multiply(X1,left_division(X1,multiply(X0,right_inverse(X1)))))),
% 117.54/20.52 inference(backward_demodulation,[status(thm)],[f5692,f334])).
% 117.54/20.52 fof(f5820,plain,(
% 117.54/20.52 ![X0,X1]: (right_division(X0,X1)=multiply(X0,right_inverse(X1)))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f13,f5764])).
% 117.54/20.52 fof(f5919,plain,(
% 117.54/20.52 ![X0,X1]: (right_division(multiply(X0,X0),X1)=multiply(X0,multiply(X0,right_inverse(X1))))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f82,f5820])).
% 117.54/20.52 fof(f5923,plain,(
% 117.54/20.52 ![X0,X1]: (right_division(X0,right_inverse(X1))=multiply(X0,X1))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f1047,f5820])).
% 117.54/20.52 fof(f5971,plain,(
% 117.54/20.52 ![X0,X1]: (right_division(multiply(X0,X0),X1)=multiply(X0,right_division(X0,X1)))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f5820,f5919])).
% 117.54/20.52 fof(f6051,plain,(
% 117.54/20.52 ![X0,X1,X2]: (multiply(X0,multiply(X1,X0))=multiply(multiply(X0,multiply(X1,multiply(X0,right_inverse(X2)))),X2))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f398,f5923])).
% 117.54/20.52 fof(f6053,plain,(
% 117.54/20.52 ![X0,X1]: (multiply(right_inverse(X0),right_division(X1,right_inverse(X0)))=multiply(multiply(right_inverse(X0),X1),X0))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f130,f5923])).
% 117.54/20.52 fof(f6079,plain,(
% 117.54/20.52 ![X0,X1,X2]: (multiply(X0,multiply(X1,X0))=multiply(multiply(X0,multiply(X1,right_division(X0,X2))),X2))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f5820,f6051])).
% 117.54/20.52 fof(f6081,plain,(
% 117.54/20.52 ![X0,X1]: (left_division(X0,right_division(X1,right_inverse(X0)))=multiply(multiply(right_inverse(X0),X1),X0))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f1203,f6053])).
% 117.54/20.52 fof(f6082,plain,(
% 117.54/20.52 ![X0,X1]: (left_division(X0,multiply(X1,X0))=multiply(multiply(right_inverse(X0),X1),X0))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f5923,f6081])).
% 117.54/20.52 fof(f6083,plain,(
% 117.54/20.52 ![X0,X1]: (left_division(X0,multiply(X1,X0))=multiply(left_division(X0,X1),X0))),
% 117.54/20.52 inference(forward_demodulation,[status(thm)],[f1203,f6082])).
% 117.54/20.52 fof(f6154,plain,(
% 117.54/20.52 ![X0]: (identity=multiply(X0,right_division(X0,multiply(X0,X0))))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f37,f5971])).
% 117.54/20.52 fof(f6249,plain,(
% 117.54/20.52 ![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))))),
% 117.54/20.52 inference(paramodulation,[status(thm)],[f6154,f1098])).
% 117.54/20.52 fof(f6323,plain,(
% 117.54/20.52 ![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))))),
% 107.95/20.66 inference(forward_demodulation,[status(thm)],[f12,f6249])).
% 107.95/20.66 fof(f6324,plain,(
% 107.95/20.66 ![X0,X1]: (left_division(right_division(X0,multiply(X0,X0)),X1)=multiply(X0,X1))),
% 107.95/20.66 inference(forward_demodulation,[status(thm)],[f13,f6323])).
% 107.95/20.66 fof(f6446,plain,(
% 107.95/20.66 ![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))))),
% 107.95/20.66 inference(paramodulation,[status(thm)],[f6154,f6083])).
% 107.95/20.66 fof(f6494,plain,(
% 107.95/20.66 ![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))))),
% 107.95/20.66 inference(forward_demodulation,[status(thm)],[f49,f6446])).
% 107.95/20.66 fof(f6495,plain,(
% 107.95/20.66 ![X0]: (right_inverse(right_division(X0,multiply(X0,X0)))=multiply(multiply(X0,X0),right_division(X0,multiply(X0,X0))))),
% 107.95/20.66 inference(forward_demodulation,[status(thm)],[f44,f6494])).
% 107.95/20.66 fof(f6496,plain,(
% 107.95/20.66 ![X0]: (right_inverse(right_division(X0,multiply(X0,X0)))=multiply(X0,multiply(X0,right_division(X0,multiply(X0,X0)))))),
% 107.95/20.66 inference(forward_demodulation,[status(thm)],[f82,f6495])).
% 107.95/20.66 fof(f6497,plain,(
% 107.95/20.66 ![X0]: (right_inverse(right_division(X0,multiply(X0,X0)))=multiply(X0,identity))),
% 107.95/20.66 inference(forward_demodulation,[status(thm)],[f6154,f6496])).
% 107.95/20.66 fof(f6498,plain,(
% 107.95/20.66 ![X0]: (right_inverse(right_division(X0,multiply(X0,X0)))=X0)),
% 107.95/20.66 inference(forward_demodulation,[status(thm)],[f12,f6497])).
% 107.95/20.66 fof(f6537,plain,(
% 107.95/20.66 ![X0,X1]: (right_division(X0,X1)=multiply(X0,right_division(X1,multiply(X1,X1))))),
% 107.95/20.66 inference(paramodulation,[status(thm)],[f6498,f5923])).
% 107.95/20.66 fof(f6835,plain,(
% 107.95/20.66 ![X0,X1]: (right_division(X0,multiply(X1,X0))=right_division(X1,multiply(X1,X1)))),
% 107.95/20.66 inference(paramodulation,[status(thm)],[f6324,f38])).
% 107.95/20.66 fof(f7662,plain,(
% 107.95/20.66 ![X0,X1,X2]: (right_division(X0,X1)=multiply(X0,right_division(X2,multiply(X1,X2))))),
% 107.95/20.66 inference(paramodulation,[status(thm)],[f6835,f6537])).
% 107.95/20.66 fof(f9755,plain,(
% 107.95/20.66 ![X0,X1,X2]: (multiply(X0,multiply(X1,X0))=multiply(multiply(X0,right_division(X1,X2)),multiply(X2,X0)))),
% 107.95/20.66 inference(paramodulation,[status(thm)],[f7662,f6079])).
% 107.95/20.66 fof(f31095,plain,(
% 107.95/20.66 ![X0,X1,X2]: (multiply(X0,multiply(multiply(X1,X2),X0))=multiply(multiply(X0,X1),multiply(X2,X0)))),
% 107.95/20.66 inference(paramodulation,[status(thm)],[f16,f9755])).
% 107.95/20.66 fof(f67365,plain,(
% 107.95/20.66 ~multiply(x,multiply(multiply(y,z),x))=multiply(x,multiply(multiply(y,z),x))),
% 107.95/20.66 inference(backward_demodulation,[status(thm)],[f31095,f20])).
% 107.95/20.66 fof(f67662,plain,(
% 107.95/20.66 $false),
% 107.95/20.66 inference(trivial_equality_resolution,[status(thm)],[f67365])).
% 107.95/20.66 % SZS output end CNFRefutation for theBenchmark.p
% 9.00/20.83 % Elapsed time: 15.261807 seconds
% 9.00/20.83 % CPU time: 120.180897 seconds
% 9.00/20.83 % Total memory used: 1.601 GB
% 9.00/20.83 % Net memory used: 1.587 GB
%------------------------------------------------------------------------------