%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP426-1 : TPTP v9.3.1. Released v2.6.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:37 PM UTC 2026
% Result : Unsatisfiable 151.05s 19.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP426-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n006.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 20:12:42 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 151.05/19.45 % Refutation found
% 151.05/19.45 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 151.05/19.45 % SZS output start CNFRefutation for theBenchmark
% 151.05/19.45 fof(f1,axiom,(
% 151.05/19.45 (![A,B,C]: (multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),C)))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C))) = B ))),
% 151.05/19.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 151.05/19.45 fof(f2,negated_conjecture,(
% 151.05/19.45 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 151.05/19.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 151.05/19.45 fof(f3,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X2),X2)))=X1)),
% 151.05/19.45 inference(cnf_transformation,[status(thm)],[f1])).
% 151.05/19.45 fof(f4,plain,(
% 151.05/19.45 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 151.05/19.45 inference(cnf_transformation,[status(thm)],[f2])).
% 151.05/19.45 fof(f10,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),inverse(multiply(inverse(X2),X2)))=X2)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3,f3])).
% 151.05/19.45 fof(f11,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X2)))),multiply(X3,inverse(X2))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3,f3])).
% 151.05/19.45 fof(f12,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X3),multiply(inverse(X2),X2))))),X1)),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))=X3)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3,f3])).
% 151.05/19.45 fof(f13,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))),inverse(multiply(inverse(X0),multiply(inverse(X3),X3))))),X2)),inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(X4),multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3)))))),multiply(inverse(X3),X3))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))),multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3)))))=X4)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f12,f12])).
% 151.05/19.45 fof(f14,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),inverse(multiply(inverse(X3),multiply(inverse(X2),X2))))),X2)),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))=X3)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3,f12])).
% 151.05/19.45 fof(f15,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))))),inverse(multiply(inverse(X3),multiply(inverse(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X5),X2)))),multiply(X4,inverse(X2)))),inverse(multiply(inverse(X1),multiply(inverse(X2),X2))))),X5))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))),multiply(inverse(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))))))=X3)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f12,f12])).
% 151.05/19.45 fof(f16,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X3),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))=X3)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3,f12])).
% 151.05/19.45 fof(f26,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))=inverse(multiply(inverse(X2),X2)))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3,f10])).
% 151.05/19.45 fof(f37,plain,(
% 151.05/19.45 ![X0,X1,X2]: (X0=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X2),X2)))),X2)))),multiply(X1,inverse(X2))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3,f11])).
% 151.05/19.45 fof(f38,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))=multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X2)))),multiply(X3,inverse(X2))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f11,f11])).
% 151.05/19.45 fof(f56,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X5,inverse(multiply(inverse(X4),X2)))),multiply(X5,inverse(X2)))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f11,f11])).
% 151.05/19.45 fof(f59,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2)))))),multiply(X3,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))=inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f11,f10])).
% 151.05/19.45 fof(f60,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))),inverse(multiply(inverse(X4),multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))))),multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))),multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))))=X4)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f11,f12])).
% 151.05/19.45 fof(f62,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X0)))),multiply(X1,inverse(X0)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X0),X0)))))),inverse(inverse(multiply(inverse(X0),X0)))))),inverse(inverse(multiply(inverse(X0),X0)))))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))=inverse(multiply(inverse(X0),X0)))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f11,f10])).
% 151.05/19.45 fof(f70,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))=X1)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f11,f3])).
% 151.05/19.45 fof(f71,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),multiply(X3,inverse(multiply(X0,inverse(X2)))))),inverse(multiply(X0,inverse(X2)))))),inverse(multiply(inverse(multiply(X0,inverse(X2))),multiply(X0,inverse(X2)))))=multiply(X0,inverse(X2)))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f11,f10])).
% 151.05/19.45 fof(f80,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))=multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),X2)))),multiply(X3,inverse(X2))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3,f38])).
% 151.05/19.45 fof(f85,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))),multiply(X4,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f11,f38])).
% 151.05/19.45 fof(f89,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))),multiply(X0,inverse(multiply(X4,inverse(X3)))))=multiply(inverse(multiply(X5,inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3)))))),multiply(X5,inverse(multiply(X4,inverse(X3))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f11,f38])).
% 151.05/19.45 fof(f197,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3)))),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))),multiply(inverse(X3),X3))))),X3))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f10,f37])).
% 151.05/19.45 fof(f209,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),inverse(multiply(inverse(X3),X3)))),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(multiply(X1,inverse(X3)))))=multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(multiply(X1,inverse(X3))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f37,f38])).
% 151.05/19.45 fof(f214,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,inverse(X3)))))),inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X3)))))=multiply(X2,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X3),X3)))),X3))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f37,f3])).
% 151.05/19.45 fof(f217,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,inverse(X3)))))=multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(multiply(X2,inverse(X3))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f37,f209])).
% 151.05/19.45 fof(f227,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X0)))),multiply(X2,inverse(X0)))),inverse(multiply(inverse(X1),multiply(inverse(X0),X0))))),X3)),inverse(multiply(inverse(X0),X0))))),inverse(multiply(inverse(X0),X0))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))))),multiply(X4,inverse(multiply(inverse(X0),X0)))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f12,f80])).
% 151.05/19.45 fof(f241,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),multiply(X3,inverse(multiply(X0,inverse(X2)))))),inverse(multiply(X0,inverse(X2)))))=multiply(inverse(multiply(X5,inverse(multiply(inverse(multiply(X0,inverse(X2))),multiply(X0,inverse(X2)))))),multiply(X5,inverse(multiply(X0,inverse(X2))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f11,f80])).
% 151.05/19.45 fof(f246,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))=multiply(inverse(multiply(X5,inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(X5,inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f11,f80])).
% 151.05/19.45 fof(f247,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3)))),inverse(multiply(inverse(X0),multiply(inverse(X3),X3))))),X3)),inverse(multiply(inverse(X3),X3))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))),multiply(X4,inverse(multiply(inverse(X3),X3)))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f10,f80])).
% 151.05/19.45 fof(f252,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(inverse(X2),X2))))),multiply(X1,inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X2),X2))))=multiply(inverse(X3),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X5),X2)))),multiply(X4,inverse(X2)))),inverse(multiply(inverse(X3),multiply(inverse(X2),X2))))),X5)),inverse(multiply(inverse(X2),X2)))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f12,f80])).
% 151.05/19.45 fof(f261,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(inverse(X2),X2))))),multiply(X1,inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X2),X2))))=multiply(inverse(multiply(inverse(multiply(inverse(X3),multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X3),X2)))),multiply(X4,inverse(X2)))),inverse(X2)))),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))),X2))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f10,f80])).
% 151.05/19.45 fof(f266,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3)))))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3)))))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(X5,inverse(multiply(inverse(X3),X3)))),multiply(X5,inverse(X3)))))),multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f80,f11])).
% 151.05/19.45 fof(f353,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(X3))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2))))=multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f11,f217])).
% 151.05/19.45 fof(f355,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))=multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X5),X6)))),multiply(X4,inverse(X6)))),inverse(multiply(inverse(X2),multiply(inverse(X6),X6))))),X5)),inverse(multiply(inverse(multiply(inverse(X6),X6)),multiply(inverse(X6),X6))))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f12,f217])).
% 151.05/19.45 fof(f480,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))=multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(X2))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f12,f355])).
% 151.05/19.45 fof(f506,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X3)))=multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X2)))),multiply(X4,inverse(X3))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3,f480])).
% 151.05/19.45 fof(f508,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X0)))),inverse(X3)))=multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),X0)))),multiply(X4,inverse(X3))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f10,f480])).
% 151.05/19.45 fof(f512,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(X3))),X1)=multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(multiply(inverse(X2),X2)))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3,f480])).
% 151.05/19.45 fof(f514,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),inverse(X3))),X2)=multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(multiply(inverse(X2),X2)))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f10,f480])).
% 151.05/19.45 fof(f533,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(X3))))),multiply(X1,inverse(inverse(X3))))),inverse(multiply(inverse(X0),multiply(inverse(inverse(X3)),inverse(X3)))))),X2)),inverse(multiply(inverse(inverse(X3)),inverse(X3)))))),inverse(multiply(inverse(X4),multiply(inverse(multiply(inverse(inverse(X3)),inverse(X3))),multiply(inverse(inverse(X3)),inverse(X3))))))),multiply(inverse(inverse(X3)),inverse(X3)))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(X3)),inverse(X3))),multiply(inverse(inverse(X3)),inverse(X3)))),multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(X3))))))=X4)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f480,f13])).
% 151.05/19.45 fof(f555,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (X0=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X3)))))),multiply(X4,inverse(X3)))))),multiply(X1,inverse(multiply(X4,inverse(X3))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f480,f37])).
% 151.05/19.45 fof(f568,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X3)))))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(X3))))),inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X3)))))))=multiply(inverse(multiply(X5,inverse(multiply(inverse(X1),multiply(X2,inverse(X3)))))),multiply(X5,inverse(multiply(X2,inverse(X3))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f480,f11])).
% 151.05/19.45 fof(f576,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(X2,inverse(X3)))))),multiply(X0,inverse(multiply(X2,inverse(X3)))))),inverse(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(X3)))))=X1)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f480,f3])).
% 151.05/19.45 fof(f577,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(multiply(X4,inverse(X3)))))),inverse(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(X3)))))=multiply(X4,inverse(X2)))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f480,f3])).
% 151.05/19.45 fof(f658,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3)))),inverse(multiply(inverse(X3),X3)))),X3)))=multiply(X0,inverse(X2)))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f214,f577])).
% 151.05/19.45 fof(f730,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X2),X2)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(X4)))),inverse(multiply(inverse(X4),X4)))),X4))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f658,f70])).
% 151.05/19.45 fof(f895,plain,(
% 151.05/19.45 ![X0,X1,X2]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(X2)))),inverse(multiply(inverse(X2),X2)))),X2))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f70,f730])).
% 151.05/19.45 fof(f989,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(multiply(X2,inverse(X3)))))),inverse(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(X3)))))),multiply(X2,inverse(X3))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f480,f895])).
% 151.05/19.45 fof(f1074,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(multiply(X2,inverse(X3)))))),inverse(multiply(inverse(X4),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X5,inverse(X4))),multiply(X5,inverse(inverse(X3))))),inverse(multiply(inverse(inverse(X3)),inverse(X3))))),inverse(X3)))))),multiply(X2,inverse(X3))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f895,f989])).
% 151.05/19.45 fof(f1098,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,inverse(X3)))))),inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X3)))))=multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(multiply(X2,inverse(X3)))))),inverse(multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(X3))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f989,f3])).
% 151.05/19.45 fof(f1110,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(multiply(X2,inverse(X3)))))),inverse(multiply(inverse(X4),X4)))),multiply(X2,inverse(X3))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f895,f1074])).
% 151.05/19.45 fof(f1125,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X2),X2)))),X2)))=X1)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f1133,f576])).
% 151.05/19.45 fof(f1133,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))),X2)))=multiply(inverse(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(multiply(X0,inverse(X2)))))),inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(X2))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f214,f1098])).
% 151.05/19.45 fof(f1150,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X2)),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))),multiply(inverse(X2),X2))))=X3)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f10,f1125])).
% 151.05/19.45 fof(f1170,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(X3,inverse(X4)))),inverse(multiply(inverse(X4),X4)))),X4))))=multiply(inverse(multiply(X3,inverse(X1))),X2))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f1125,f480])).
% 151.05/19.45 fof(f1171,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X2,inverse(X3)))),inverse(multiply(inverse(X3),X3)))),X3)))),multiply(X0,inverse(X4)))=multiply(inverse(X1),multiply(X2,inverse(X4))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f1125,f480])).
% 151.05/19.45 fof(f1207,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5,X6]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(X2)))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X5),X6)))),multiply(X4,inverse(X6)))),inverse(multiply(inverse(X2),multiply(inverse(X6),X6))))),X5)),inverse(multiply(inverse(multiply(inverse(X6),X6)),multiply(inverse(X6),X6))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f12,f1110])).
% 151.05/19.45 fof(f1249,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(X2)))),inverse(multiply(inverse(X3),X3)))),X2))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f12,f1207])).
% 151.05/19.45 fof(f1272,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),X0)=multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X3)))),inverse(multiply(inverse(X4),X4)))),X3))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3,f1249])).
% 151.05/19.45 fof(f1326,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(inverse(X2),X2))))),multiply(X1,inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X2),X2))))=multiply(inverse(X2),X2))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f1272,f261])).
% 151.05/19.45 fof(f1369,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(X0),X0)=multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X0)))),multiply(X2,inverse(X0)))),inverse(multiply(inverse(X1),multiply(inverse(X0),X0))))),X3)),inverse(multiply(inverse(X0),X0)))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f1326,f252])).
% 151.05/19.45 fof(f1379,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0))))))),multiply(inverse(inverse(X0)),inverse(X0)))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0)))),multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,inverse(X0))))))=X1)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f1369,f533])).
% 151.05/19.45 fof(f1397,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(inverse(X0),X0))))=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))))),multiply(X1,inverse(multiply(inverse(X0),X0)))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f1369,f227])).
% 151.05/19.45 fof(f1418,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))=multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f1397,f246])).
% 151.05/19.45 fof(f1421,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3)))),inverse(multiply(inverse(X0),multiply(inverse(X3),X3))))),X3)),inverse(multiply(inverse(X3),X3))))=multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(multiply(inverse(X3),X3)),inverse(multiply(inverse(X3),X3)))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f1397,f247])).
% 151.05/19.45 fof(f1459,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X0)))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),multiply(X4,inverse(X5)))),inverse(multiply(inverse(X5),X5)))),X5))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),X0)))),X3))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f10,f1170])).
% 151.05/19.45 fof(f1473,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X3)),inverse(multiply(inverse(X4),X4)))),X4))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(inverse(X4))))),inverse(multiply(inverse(X6),X6)))),inverse(X1))),X2))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f1249,f1170])).
% 151.05/19.45 fof(f1592,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X3)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X4),X4)),multiply(inverse(X4),X4))),multiply(inverse(multiply(inverse(X4),X4)),multiply(inverse(X4),X4)))))),multiply(inverse(multiply(inverse(X4),X4)),multiply(inverse(X4),X4))))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X5),multiply(inverse(multiply(inverse(multiply(X6,inverse(multiply(inverse(X5),X4)))),multiply(X6,inverse(X4)))),inverse(X4)))),inverse(multiply(inverse(X3),multiply(inverse(X4),X4))))),X4)),inverse(X1))),X2))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f14,f1170])).
% 151.05/19.45 fof(f1593,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3)))),inverse(multiply(inverse(X0),multiply(inverse(X3),X3))))),X3)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X4),multiply(X5,inverse(X6)))),inverse(multiply(inverse(X6),X6)))),X6))))=multiply(inverse(multiply(X5,inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))),X4))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f14,f1170])).
% 151.05/19.45 fof(f1596,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),inverse(multiply(inverse(X3),multiply(inverse(X2),X2))))),X2)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X4),X3)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))))=X4)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f14,f1125])).
% 151.05/19.45 fof(f1598,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))),multiply(X0,inverse(X2)))=multiply(inverse(X3),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X4),multiply(inverse(multiply(inverse(multiply(X5,inverse(multiply(inverse(X4),X1)))),multiply(X5,inverse(X1)))),inverse(X1)))),inverse(multiply(inverse(X3),multiply(inverse(X1),X1))))),X1)),inverse(X2))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f14,f480])).
% 151.05/19.45 fof(f1716,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X2),inverse(multiply(inverse(X1),X1)))),X1)))))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))))),inverse(multiply(inverse(X3),multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X5),inverse(X1))))),multiply(X4,inverse(inverse(X1))))),inverse(X2))),X5))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))),multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))))))=X3)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f37,f15])).
% 151.05/19.45 fof(f2334,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))),X2)))),multiply(X0,inverse(X3)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(multiply(X5,inverse(X2)))))),inverse(multiply(inverse(X6),X6)))),multiply(X5,inverse(X3))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f1249,f1171])).
% 151.05/19.45 fof(f2457,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5,X6]: (X0=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X2),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(X4))))),inverse(multiply(inverse(X5),X5)))),inverse(X4)))))),multiply(X6,inverse(X4)))))),multiply(X1,inverse(multiply(X6,inverse(X4))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f1249,f555])).
% 151.05/19.45 fof(f2512,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (X0=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X2),X2)))),multiply(X3,inverse(X4)))))),multiply(X1,inverse(multiply(X3,inverse(X4))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f1249,f2457])).
% 151.05/19.45 fof(f2546,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (inverse(multiply(inverse(X0),X0))=multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),inverse(multiply(inverse(X0),X0)))))),multiply(X2,inverse(inverse(multiply(inverse(X0),X0)))))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))))))),X3)),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f12,f2512])).
% 151.05/19.45 fof(f2547,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (inverse(multiply(inverse(X0),X0))=multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),inverse(multiply(inverse(X0),X0)))))),multiply(X3,inverse(inverse(multiply(inverse(X0),X0)))))),inverse(inverse(multiply(inverse(X0),X0)))))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))))))),inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f14,f2512])).
% 151.05/19.45 fof(f2549,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (X0=multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),multiply(inverse(X0),inverse(multiply(inverse(X3),X3))))))),multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(X0),inverse(multiply(inverse(X3),X3)))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3,f2512])).
% 151.05/19.45 fof(f2550,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (X0=multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),multiply(inverse(multiply(inverse(X2),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),multiply(inverse(X0),inverse(multiply(inverse(X1),X1))))))),multiply(X3,inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))))))),inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))))))),inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f10,f2512])).
% 151.05/19.45 fof(f2555,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (X0=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))),multiply(X2,inverse(X4)))))),multiply(X1,inverse(multiply(inverse(X0),inverse(X4))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f480,f2512])).
% 151.05/19.45 fof(f2566,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5,X6]: (X0=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X2),X2)))),X3)))),multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X5),X6)))),multiply(X4,inverse(X6)))),inverse(multiply(inverse(X3),multiply(inverse(X6),X6))))),X5)),inverse(multiply(inverse(multiply(inverse(X6),X6)),multiply(inverse(X6),X6))))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f12,f2512])).
% 151.05/19.45 fof(f2598,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))),multiply(X3,inverse(X4)))))),multiply(inverse(multiply(inverse(multiply(X5,inverse(X1))),multiply(X5,inverse(multiply(X0,inverse(multiply(X3,inverse(X4)))))))),inverse(multiply(X0,inverse(multiply(X3,inverse(X4)))))))),inverse(multiply(inverse(multiply(X0,inverse(multiply(X3,inverse(X4))))),multiply(X0,inverse(multiply(X3,inverse(X4)))))))=multiply(X0,inverse(multiply(X3,inverse(X4)))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f2512,f10])).
% 151.05/19.45 fof(f2600,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,inverse(multiply(X3,inverse(X4)))))))),inverse(multiply(inverse(multiply(X2,inverse(multiply(X3,inverse(X4))))),multiply(X2,inverse(multiply(X3,inverse(X4)))))))=multiply(X2,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X5),X5)))),multiply(X3,inverse(X4))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f2512,f3])).
% 151.05/19.45 fof(f2608,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))),inverse(multiply(inverse(X4),multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))))),multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))=X4)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f60])).
% 151.05/19.45 fof(f2609,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2)))))),multiply(X3,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))=inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f59])).
% 151.05/19.45 fof(f2621,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))))),inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X5,inverse(multiply(inverse(X4),X2)))),multiply(X5,inverse(X2)))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f56])).
% 151.05/19.45 fof(f2627,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X2),inverse(multiply(inverse(X1),X1)))),X1)))))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))))),inverse(multiply(inverse(X3),multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X5),inverse(X1))))),multiply(X4,inverse(inverse(X1))))),inverse(X2))),X5))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))))=X3)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f1716])).
% 151.05/19.45 fof(f2633,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3)))))))),inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(X5,inverse(multiply(inverse(X3),X3)))),multiply(X5,inverse(X3)))))),multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f266])).
% 151.05/19.45 fof(f2714,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))=multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),inverse(inverse(multiply(inverse(X3),X3))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f1418])).
% 151.05/19.45 fof(f2734,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(X3))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2))))=multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(inverse(multiply(inverse(X2),X2))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f353])).
% 151.05/19.45 fof(f2738,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2))))))),multiply(X3,inverse(multiply(X0,inverse(X2)))))),inverse(multiply(X0,inverse(X2)))))=multiply(inverse(multiply(X5,inverse(multiply(inverse(multiply(X0,inverse(X2))),multiply(X0,inverse(X2)))))),multiply(X5,inverse(multiply(X0,inverse(X2))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f241])).
% 151.05/19.45 fof(f2746,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(inverse(multiply(inverse(X3),X3))))))),multiply(X0,inverse(multiply(X4,inverse(X3)))))=multiply(inverse(multiply(X5,inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3)))))),multiply(X5,inverse(multiply(X4,inverse(X3))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f89])).
% 151.05/19.45 fof(f2747,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))),multiply(X4,inverse(inverse(inverse(multiply(inverse(X3),X3)))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f85])).
% 151.05/19.45 fof(f2749,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2))))))),multiply(X3,inverse(multiply(X0,inverse(X2)))))),inverse(multiply(X0,inverse(X2)))))),inverse(multiply(inverse(multiply(X0,inverse(X2))),multiply(X0,inverse(X2)))))=multiply(X0,inverse(X2)))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f71])).
% 151.05/19.45 fof(f2752,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X0)))),multiply(X1,inverse(X0)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(X0),X0)))))),inverse(inverse(multiply(inverse(X0),X0)))))),inverse(inverse(multiply(inverse(X0),X0)))))),inverse(inverse(multiply(inverse(X0),X0))))=inverse(multiply(inverse(X0),X0)))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f62])).
% 151.05/19.45 fof(f2761,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X2),X2))))=inverse(multiply(inverse(X2),X2)))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f26])).
% 151.05/19.45 fof(f2762,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X3),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2)))))=X3)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2763,f16])).
% 151.05/19.45 fof(f2763,plain,(
% 151.05/19.45 ![X0]: (inverse(multiply(inverse(X0),X0))=multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f1369,f2546])).
% 151.05/19.45 fof(f2764,plain,(
% 151.05/19.45 ![X0]: (inverse(multiply(inverse(X0),X0))=multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f1421,f2547])).
% 151.05/19.45 fof(f2765,plain,(
% 151.05/19.45 ![X0]: (inverse(multiply(inverse(X0),X0))=multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2764])).
% 151.05/19.45 fof(f2766,plain,(
% 151.05/19.45 ![X0]: (inverse(multiply(inverse(X0),X0))=multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2765])).
% 151.05/19.45 fof(f2767,plain,(
% 151.05/19.45 ![X0]: (inverse(multiply(inverse(X0),X0))=multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(inverse(multiply(inverse(X0),X0))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2766])).
% 151.05/19.45 fof(f2769,plain,(
% 151.05/19.45 ![X0,X1]: (X0=multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),multiply(inverse(X0),inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2549,f2550])).
% 151.05/19.45 fof(f2782,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (X0=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X2),X2)))),X3)))),multiply(X1,inverse(X3))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f12,f2566])).
% 151.05/19.45 fof(f2835,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(X4),multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))))),multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))=X4)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2608])).
% 151.05/19.45 fof(f2836,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(X4),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))),multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))=X4)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2835])).
% 151.05/19.45 fof(f2837,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(X4),inverse(inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))=X4)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2836])).
% 151.05/19.45 fof(f2838,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(X4),inverse(inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))=X4)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2837])).
% 151.05/19.45 fof(f2839,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(X4),inverse(inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))=X4)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2838])).
% 151.05/19.45 fof(f2841,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(X4),inverse(inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3))))))),inverse(inverse(inverse(multiply(inverse(X3),X3)))))=X4)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2839])).
% 151.05/19.45 fof(f2842,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2)))))),multiply(X3,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))=inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2609])).
% 151.05/19.45 fof(f2843,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2)))))),multiply(X3,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))=inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2842])).
% 151.05/19.45 fof(f2844,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2)))))),multiply(X3,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))=inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2843])).
% 151.05/19.45 fof(f2845,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2)))))),multiply(X3,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))=inverse(inverse(multiply(inverse(X2),X2))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2844])).
% 151.05/19.45 fof(f2978,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))))),inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X5,inverse(multiply(inverse(X4),X2)))),multiply(X5,inverse(X2)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2621])).
% 151.05/19.45 fof(f2979,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X5,inverse(multiply(inverse(X4),X2)))),multiply(X5,inverse(X2)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2978])).
% 151.05/19.45 fof(f2980,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X5,inverse(multiply(inverse(X4),X2)))),multiply(X5,inverse(X2)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2979])).
% 151.05/19.45 fof(f2981,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X5,inverse(multiply(inverse(X4),X2)))),multiply(X5,inverse(X2)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2980])).
% 151.05/19.45 fof(f2982,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X5,inverse(multiply(inverse(X4),X2)))),multiply(X5,inverse(X2)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2981])).
% 151.05/19.45 fof(f2983,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X5,inverse(multiply(inverse(X4),X2)))),multiply(X5,inverse(X2)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2982])).
% 151.05/19.45 fof(f2984,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(X5,inverse(multiply(inverse(X4),X2)))),multiply(X5,inverse(X2)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2983])).
% 151.05/19.45 fof(f2992,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X2),inverse(multiply(inverse(X1),X1)))),X1)))))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))))),inverse(multiply(inverse(X3),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X5),inverse(X1))))),multiply(X4,inverse(inverse(X1))))),inverse(X2))),X5))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))))=X3)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2627])).
% 151.05/19.45 fof(f2993,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X2),inverse(multiply(inverse(X1),X1)))),X1)))))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))))),inverse(multiply(inverse(X3),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X5),inverse(X1))))),multiply(X4,inverse(inverse(X1))))),inverse(X2))),X5))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))))=X3)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2992])).
% 151.05/19.45 fof(f2994,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X2),inverse(multiply(inverse(X1),X1)))),X1)))))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))))),inverse(multiply(inverse(X3),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X5),inverse(X1))))),multiply(X4,inverse(inverse(X1))))),inverse(X2))),X5))),inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))))=X3)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2993])).
% 151.05/19.45 fof(f3093,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3)))))))),inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))))))=multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2555,f2633])).
% 151.05/19.45 fof(f3400,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),inverse(multiply(inverse(X3),X3)))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))=multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),inverse(inverse(multiply(inverse(X3),X3))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2714])).
% 151.05/19.45 fof(f3401,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),inverse(multiply(inverse(X3),X3)))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3))))),inverse(inverse(multiply(inverse(X3),X3)))))=multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),inverse(inverse(multiply(inverse(X3),X3))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f3400])).
% 151.05/19.45 fof(f3402,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),inverse(multiply(inverse(X3),X3)))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3))))),inverse(inverse(multiply(inverse(X3),X3)))))=multiply(inverse(inverse(multiply(inverse(X3),X3))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),inverse(inverse(multiply(inverse(X3),X3))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f3401])).
% 151.05/19.45 fof(f3403,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),inverse(multiply(inverse(X3),X3)))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3))))),inverse(inverse(multiply(inverse(X3),X3)))))=multiply(inverse(inverse(multiply(inverse(X3),X3))),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(inverse(multiply(inverse(X3),X3))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f3402])).
% 151.05/19.45 fof(f3404,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),inverse(multiply(inverse(X3),X3)))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3))))),inverse(inverse(multiply(inverse(X3),X3)))))=inverse(multiply(inverse(X3),X3)))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2767,f3403])).
% 151.05/19.45 fof(f3475,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))),multiply(X4,inverse(inverse(inverse(multiply(inverse(X3),X3)))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2747])).
% 151.05/19.45 fof(f3476,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(inverse(multiply(inverse(X3),X3))))))),multiply(X4,inverse(inverse(inverse(multiply(inverse(X3),X3)))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f3475])).
% 151.05/19.45 fof(f3497,plain,(
% 151.05/19.45 ![X0]: (multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),inverse(inverse(multiply(inverse(X0),X0))))=inverse(multiply(inverse(X0),X0)))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f2761,f2752])).
% 151.05/19.45 fof(f3499,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X3),inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2)))))=X3)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f2762])).
% 151.05/19.45 fof(f3500,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X3),inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))=X3)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f3499])).
% 151.05/19.45 fof(f3501,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(X0),X0)=inverse(multiply(inverse(X1),X1)))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3502,f3404])).
% 151.05/19.45 fof(f3502,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X3),inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2))))),inverse(inverse(multiply(inverse(X2),X2))))=X3)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f3500])).
% 151.05/19.45 fof(f3505,plain,(
% 151.05/19.45 ![X0]: (multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(inverse(multiply(inverse(X0),X0))))=inverse(multiply(inverse(X0),X0)))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2763,f3497])).
% 151.05/19.45 fof(f3528,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X2,inverse(X3)))),inverse(multiply(inverse(X3),X3)))),X3)))),inverse(multiply(inverse(X0),X0)))=multiply(inverse(X1),multiply(X2,inverse(inverse(multiply(inverse(X0),X0))))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3505,f1171])).
% 151.05/19.45 fof(f3532,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X2,inverse(X3)))),inverse(multiply(inverse(X3),X3)))),X3))))=multiply(inverse(multiply(X2,inverse(inverse(multiply(inverse(X0),X0))))),X1))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3505,f1170])).
% 151.05/19.45 fof(f3536,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))=multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(X1))),inverse(multiply(inverse(X2),X2))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3505,f480])).
% 151.05/19.45 fof(f3537,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(inverse(multiply(inverse(X1),X1))))),multiply(X0,inverse(X2)))=multiply(inverse(inverse(multiply(inverse(X1),X1))),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(X2))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3505,f480])).
% 151.05/19.45 fof(f3542,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),X0)))))),inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))=X1)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3505,f3])).
% 151.05/19.45 fof(f3579,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X3),multiply(inverse(X2),X2))))),X1)),inverse(inverse(multiply(inverse(X4),X4))))=X3)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f12])).
% 151.05/19.45 fof(f3582,plain,(
% 151.05/19.45 ![X0,X1,X2]: (X0=multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X2),X2)))),X0))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f1249])).
% 151.05/19.45 fof(f3606,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(inverse(multiply(inverse(X3),X3))))=X1)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f3])).
% 151.05/19.45 fof(f3607,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(inverse(X1),X1))))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X2),X2)))=X2)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f3])).
% 151.05/19.45 fof(f3608,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X2,inverse(X3)))),inverse(multiply(inverse(X3),X3)))),X3))),inverse(X4)))=multiply(inverse(X1),multiply(X2,inverse(X4))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f1171])).
% 151.05/19.45 fof(f3609,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(X1,inverse(X2)))),inverse(multiply(inverse(X2),X2)))),X2))),inverse(X3))),inverse(multiply(inverse(X4),X4)))=multiply(inverse(multiply(X1,inverse(X3))),X0))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f1170])).
% 151.05/19.45 fof(f3614,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X2,inverse(X3)))),inverse(multiply(inverse(X3),X3)))),X3)))),inverse(multiply(inverse(X4),X4)))=multiply(inverse(X1),multiply(X2,inverse(X0))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f1171])).
% 151.05/19.45 fof(f3615,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X3),X3)))),X3)))),multiply(X0,inverse(X4)))=multiply(inverse(X1),multiply(inverse(inverse(X3)),inverse(X4))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f1171])).
% 151.05/19.45 fof(f3618,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(X3,inverse(X4)))),inverse(multiply(inverse(X4),X4)))),X4))))=multiply(inverse(multiply(X3,inverse(X1))),X2))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f1170])).
% 151.05/19.45 fof(f3623,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))=multiply(inverse(inverse(multiply(inverse(X3),X3))),multiply(inverse(inverse(X1)),inverse(X2))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f480])).
% 151.05/19.45 fof(f3637,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X1),X1)))=inverse(multiply(inverse(X0),X0)))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f3505])).
% 151.05/19.45 fof(f3649,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),multiply(inverse(X3),X3))=X1)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f3])).
% 151.05/19.45 fof(f3651,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(multiply(inverse(X0),X0),multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X2,inverse(X3)))),inverse(multiply(inverse(X3),X3)))),X3))),inverse(X4)))=multiply(inverse(X1),multiply(X2,inverse(X4))))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f1171])).
% 151.05/19.45 fof(f3672,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(X2),X2),X3)))),multiply(X1,inverse(X3)))),inverse(X3)))),inverse(multiply(inverse(X4),multiply(inverse(X3),X3))))),X3)),inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))=X4)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f14])).
% 151.05/19.45 fof(f3675,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(X3,multiply(inverse(X4),X4)))),inverse(multiply(inverse(multiply(inverse(X5),X5)),multiply(inverse(X5),X5))))),multiply(inverse(X5),X5)))))=multiply(inverse(multiply(X3,inverse(X1))),X2))),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f1170])).
% 151.05/19.45 fof(f3691,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(X2),X2),X3)))),multiply(X1,inverse(X3)))),inverse(X3)))),inverse(multiply(inverse(X3),X3)))=X3)),
% 151.05/19.45 inference(paramodulation,[status(thm)],[f3501,f10])).
% 151.05/19.45 fof(f3731,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(X0),multiply(X1,inverse(multiply(inverse(X2),X2))))=multiply(inverse(X0),multiply(X1,inverse(inverse(multiply(inverse(X2),X2))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3614,f3528])).
% 151.05/19.45 fof(f3734,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X1)))),X2)=multiply(inverse(multiply(X0,inverse(inverse(multiply(inverse(X1),X1))))),X2))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3618,f3532])).
% 151.05/19.45 fof(f3742,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X3)))))))),inverse(inverse(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(X3))))))=multiply(inverse(multiply(X5,inverse(multiply(inverse(X1),multiply(X2,inverse(X3)))))),multiply(X5,inverse(multiply(X2,inverse(X3))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3637,f568])).
% 151.05/19.45 fof(f3746,plain,(
% 151.05/19.45 ![X0,X1]: (X0=multiply(inverse(inverse(multiply(inverse(X1),X1))),X0))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3637,f3582])).
% 151.05/19.45 fof(f3747,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),X0)))))),inverse(multiply(inverse(X0),X0)))),inverse(inverse(multiply(inverse(X0),X0))))=X1)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3637,f3542])).
% 151.05/19.45 fof(f3800,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X2),inverse(multiply(inverse(X1),X1)))),X1)))))),multiply(X0,inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))))),inverse(multiply(inverse(X3),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1)))))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X5),inverse(X1))))),multiply(X4,inverse(inverse(X1))))),inverse(X2))),X5))),inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))))=X3)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3731,f2994])).
% 151.05/19.45 fof(f3814,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))))))),inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3)))),inverse(X3))))))=multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X3)))),multiply(X2,inverse(X3))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3731,f3093])).
% 151.05/19.45 fof(f3872,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(inverse(X2),X2))))=multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(X1))),inverse(multiply(inverse(X2),X2))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3731,f3536])).
% 151.05/19.45 fof(f3878,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(multiply(inverse(X2),X2))))),inverse(inverse(multiply(inverse(X2),X2))))))),multiply(X3,inverse(multiply(X0,inverse(X2)))))),inverse(multiply(X0,inverse(X2)))))),inverse(multiply(inverse(multiply(X0,inverse(X2))),multiply(X0,inverse(X2)))))=multiply(X0,inverse(X2)))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3731,f2749])).
% 151.05/19.45 fof(f3880,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(multiply(inverse(X3),X3))))),inverse(inverse(multiply(inverse(X3),X3))))))),multiply(X4,inverse(inverse(inverse(multiply(inverse(X3),X3)))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3731,f3476])).
% 151.05/19.45 fof(f3881,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(inverse(X3),X3))))),inverse(inverse(multiply(inverse(X3),X3))))))),multiply(X0,inverse(multiply(X4,inverse(X3)))))=multiply(inverse(multiply(X5,inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3)))))),multiply(X5,inverse(multiply(X4,inverse(X3))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3731,f2746])).
% 151.05/19.45 fof(f3884,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(multiply(inverse(X2),X2))))),inverse(inverse(multiply(inverse(X2),X2))))))),multiply(X3,inverse(multiply(X0,inverse(X2)))))),inverse(multiply(X0,inverse(X2)))))=multiply(inverse(multiply(X5,inverse(multiply(inverse(multiply(X0,inverse(X2))),multiply(X0,inverse(X2)))))),multiply(X5,inverse(multiply(X0,inverse(X2))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3731,f2738])).
% 151.05/19.45 fof(f3887,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(X3))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2))))=multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(multiply(inverse(X2),X2)))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3731,f2734])).
% 151.05/19.45 fof(f3902,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(X5,inverse(multiply(inverse(X4),X2)))),multiply(X5,inverse(X2)))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3731,f2984])).
% 151.05/19.45 fof(f3907,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(inverse(X2),X2))))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2)))))),multiply(X3,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))=inverse(inverse(multiply(inverse(X2),X2))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3731,f2845])).
% 151.05/19.45 fof(f3908,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(X4),inverse(inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(multiply(inverse(X3),X3)))))),inverse(inverse(inverse(multiply(inverse(X3),X3)))))=X4)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3731,f2841])).
% 151.05/19.45 fof(f3926,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X1)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X2),X2)))=X2)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3734,f3607])).
% 151.05/19.45 fof(f3930,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X1)))),multiply(X0,inverse(X2)))=multiply(inverse(inverse(multiply(inverse(X1),X1))),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(X2))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3734,f3537])).
% 151.05/19.45 fof(f3935,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X3))))))),inverse(inverse(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(X3))))))=multiply(inverse(multiply(X5,inverse(multiply(inverse(X1),multiply(X2,inverse(X3)))))),multiply(X5,inverse(multiply(X2,inverse(X3))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3731,f3742])).
% 151.05/19.45 fof(f3937,plain,(
% 151.05/19.45 ![X0]: (inverse(inverse(multiply(inverse(X0),X0)))=inverse(multiply(inverse(X0),X0)))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3746,f3505])).
% 151.05/19.45 fof(f3945,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(X1,inverse(X2)))),inverse(multiply(inverse(X2),X2)))),X2))),inverse(X3))=multiply(inverse(X0),multiply(X1,inverse(X3))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3746,f3608])).
% 151.05/19.45 fof(f3950,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X2,inverse(X3)))),inverse(multiply(inverse(X3),X3)))),X3)))=multiply(inverse(multiply(X2,inverse(X0))),X1))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3746,f3618])).
% 151.05/19.45 fof(f3951,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))=multiply(inverse(inverse(X1)),inverse(X2)))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3746,f3623])).
% 151.05/19.45 fof(f3962,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1)))),inverse(inverse(multiply(inverse(X1),X1))))=X0)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3746,f3747])).
% 151.05/19.45 fof(f4021,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),X0)))),X0))))),inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0)))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0)))))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X4),inverse(X0))))),multiply(X3,inverse(inverse(X0))))),inverse(X1))),X4))),inverse(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0))))))=X2)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f4119,f3800])).
% 151.05/19.45 fof(f4042,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2))),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))))),inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2))),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2))))))=multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f4119,f3814])).
% 151.05/19.45 fof(f4104,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X2)))))),inverse(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(X2))))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),multiply(X1,inverse(X2)))))),multiply(X4,inverse(multiply(X1,inverse(X2))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f4119,f3935])).
% 151.05/19.45 fof(f4117,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),inverse(X3))),X2)=multiply(inverse(inverse(X3)),inverse(multiply(inverse(X2),X2))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f4119,f514])).
% 151.05/19.45 fof(f4118,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(X3))),X1)=multiply(inverse(inverse(X3)),inverse(multiply(inverse(X2),X2))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f4119,f512])).
% 151.05/19.45 fof(f4119,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(inverse(X2),X2))))=multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3746,f3872])).
% 151.05/19.45 fof(f4131,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))),multiply(X3,inverse(multiply(X0,inverse(X2)))))),inverse(multiply(X0,inverse(X2)))))),inverse(multiply(inverse(multiply(X0,inverse(X2))),multiply(X0,inverse(X2)))))=multiply(X0,inverse(X2)))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4119,f3878])).
% 151.05/19.45 fof(f4133,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(inverse(X2)),inverse(multiply(inverse(X3),X3)))),inverse(inverse(multiply(inverse(X3),X3))))))),multiply(X4,inverse(inverse(inverse(multiply(inverse(X3),X3)))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4119,f3880])).
% 151.05/19.45 fof(f4134,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))))=inverse(X2))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f2782,f4133])).
% 151.05/19.45 fof(f4135,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))),multiply(X0,inverse(multiply(X3,inverse(X2)))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X2)))),multiply(X3,inverse(X2)))))),multiply(X4,inverse(multiply(X3,inverse(X2))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4119,f3881])).
% 151.05/19.45 fof(f4139,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))),multiply(X3,inverse(multiply(X0,inverse(X2)))))),inverse(multiply(X0,inverse(X2)))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(X0,inverse(X2))),multiply(X0,inverse(X2)))))),multiply(X4,inverse(multiply(X0,inverse(X2))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4119,f3884])).
% 151.05/19.45 fof(f4144,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(inverse(X2),X2))))),inverse(X3))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2))))=multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(multiply(inverse(X2),X2)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3731,f3887])).
% 151.05/19.45 fof(f4145,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X1)))),inverse(X2))),multiply(inverse(multiply(X3,inverse(multiply(inverse(X0),X1)))),multiply(X3,inverse(X1))))=multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(multiply(inverse(X1),X1)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4119,f4144])).
% 151.05/19.45 fof(f4149,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X1)))),inverse(X2))),multiply(inverse(multiply(X3,inverse(multiply(inverse(X0),X1)))),multiply(X3,inverse(X1))))=multiply(inverse(inverse(X2)),inverse(multiply(inverse(X1),X1))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4119,f4145])).
% 151.05/19.45 fof(f4173,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))=multiply(inverse(multiply(inverse(multiply(inverse(inverse(X3)),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X3),X2)))),multiply(X4,inverse(X2)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4119,f3902])).
% 151.05/19.45 fof(f4174,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))=multiply(inverse(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X2),X2))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4149,f4173])).
% 151.05/19.45 fof(f4182,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X1)))),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X0),X1)))),multiply(X3,inverse(X1)))))),multiply(X2,inverse(inverse(inverse(multiply(inverse(X1),X1))))))),inverse(inverse(inverse(multiply(inverse(X1),X1))))))),inverse(inverse(inverse(multiply(inverse(X1),X1)))))=inverse(inverse(multiply(inverse(X1),X1))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4119,f3907])).
% 151.05/19.45 fof(f4183,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X1)))),multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X1)))),multiply(X2,inverse(X1)))),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1))))),inverse(inverse(inverse(multiply(inverse(X1),X1)))))=inverse(inverse(multiply(inverse(X1),X1))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4174,f4182])).
% 151.05/19.45 fof(f4184,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X1)))),multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X1))))),inverse(inverse(inverse(multiply(inverse(X1),X1)))))=inverse(inverse(multiply(inverse(X1),X1))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3,f4183])).
% 151.05/19.45 fof(f4185,plain,(
% 151.05/19.45 ![X0]: (multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),inverse(inverse(inverse(multiply(inverse(X0),X0)))))=inverse(inverse(multiply(inverse(X0),X0))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4119,f4184])).
% 151.05/19.45 fof(f4189,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(inverse(multiply(inverse(X2),X2))))))),inverse(inverse(multiply(inverse(X2),X2))))=multiply(inverse(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X2),X2))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f4193,f4174])).
% 151.05/19.45 fof(f4193,plain,(
% 151.05/19.45 ![X0]: (inverse(inverse(inverse(multiply(inverse(X0),X0))))=inverse(inverse(multiply(inverse(X0),X0))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3582,f4185])).
% 151.05/19.45 fof(f4194,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),inverse(inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,inverse(multiply(inverse(X2),X2)))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))=X1)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4134,f3908])).
% 151.05/19.45 fof(f4195,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),inverse(inverse(multiply(inverse(X2),X2))))))),multiply(inverse(inverse(X0)),inverse(multiply(inverse(X2),X2))))),inverse(inverse(inverse(multiply(inverse(X2),X2)))))=X1)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4119,f4194])).
% 151.05/19.45 fof(f4196,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),inverse(inverse(multiply(inverse(X1),X1)))))),inverse(multiply(inverse(X1),X1)))),inverse(inverse(inverse(multiply(inverse(X1),X1)))))=X0)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4119,f4195])).
% 151.05/19.45 fof(f4197,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),inverse(inverse(multiply(inverse(X1),X1)))))),inverse(multiply(inverse(X1),X1)))),inverse(inverse(multiply(inverse(X1),X1))))=X0)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4193,f4196])).
% 151.05/19.45 fof(f4242,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X1)))),multiply(X0,inverse(X2)))=multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(X2)))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3746,f3930])).
% 151.05/19.45 fof(f4243,plain,(
% 151.05/19.45 ![X0,X1]: (X0=inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f4264,f2769])).
% 151.05/19.45 fof(f4246,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (inverse(X0)=multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),X4)))),multiply(X3,inverse(X4)))),inverse(X4)))),inverse(multiply(inverse(X1),multiply(inverse(X4),X4))))),X4)),inverse(X0))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f4264,f1598])).
% 151.05/19.45 fof(f4248,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2))))))),multiply(X3,inverse(multiply(X0,inverse(X2)))))),inverse(multiply(X0,inverse(X2)))))=inverse(multiply(X0,inverse(X2))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f4264,f4139])).
% 151.05/19.45 fof(f4256,plain,(
% 151.05/19.45 ![X0]: (multiply(inverse(inverse(X0)),inverse(multiply(inverse(X0),X0)))=X0)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f4264,f3926])).
% 151.05/19.45 fof(f4261,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X0)))),inverse(X3)))=inverse(X3))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f4264,f508])).
% 151.05/19.45 fof(f4262,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X3)))=inverse(X3))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f4264,f506])).
% 151.05/19.45 fof(f4264,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X1)))),multiply(X0,inverse(X2)))=inverse(X2))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3746,f4242])).
% 151.05/19.45 fof(f4273,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),inverse(inverse(multiply(inverse(X1),X1)))))),inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(X1),X1)))=X0)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3937,f4197])).
% 151.05/19.45 fof(f4282,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2)))))),multiply(X0,inverse(multiply(X3,inverse(X2)))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X2)))),multiply(X3,inverse(X2)))))),multiply(X4,inverse(multiply(X3,inverse(X2))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3937,f4135])).
% 151.05/19.45 fof(f4284,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2)))))),multiply(X3,inverse(multiply(X0,inverse(X2)))))),inverse(multiply(X0,inverse(X2)))))),inverse(multiply(inverse(multiply(X0,inverse(X2))),multiply(X0,inverse(X2)))))=multiply(X0,inverse(X2)))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3937,f4131])).
% 151.05/19.45 fof(f4289,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(X1),X1)))=X0)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3937,f3962])).
% 151.05/19.45 fof(f4290,plain,(
% 151.05/19.45 ![X0,X1]: (X0=multiply(inverse(multiply(inverse(X1),X1)),X0))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3937,f3746])).
% 151.05/19.45 fof(f4294,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X3),X3)))=X1)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3937,f3606])).
% 151.05/19.45 fof(f4296,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X3),multiply(inverse(X2),X2))))),X1)),inverse(multiply(inverse(X4),X4)))=X3)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3937,f3579])).
% 151.05/19.45 fof(f4309,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(multiply(inverse(X0),X0),multiply(inverse(X1),multiply(X2,inverse(X3))))=multiply(inverse(X1),multiply(X2,inverse(X3))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3945,f3651])).
% 151.05/19.45 fof(f4310,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(X0),multiply(X1,inverse(X2)))),inverse(multiply(inverse(X3),X3)))=multiply(inverse(multiply(X1,inverse(X2))),X0))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3945,f3609])).
% 151.05/19.45 fof(f4312,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),X2)),inverse(multiply(inverse(X3),X3)))=multiply(inverse(X2),multiply(X0,inverse(X1))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3950,f3614])).
% 151.05/19.45 fof(f4317,plain,(
% 151.05/19.45 ![X0,X1,X2]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X1))),inverse(multiply(inverse(X2),X2)))),X1))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f1249])).
% 151.05/19.45 fof(f4318,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))=multiply(inverse(inverse(X1)),inverse(X2)))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f480])).
% 151.05/19.45 fof(f4320,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0))))))),multiply(inverse(inverse(X0)),inverse(X0)))),inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,inverse(X0))))))=X1)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f1379])).
% 151.05/19.45 fof(f4332,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),X2))),inverse(X2))),inverse(X2)))),inverse(multiply(inverse(X2),X2)))=X2)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f3691])).
% 151.05/19.45 fof(f4333,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),X2))),inverse(X2))),inverse(X2)))),inverse(multiply(inverse(X3),multiply(inverse(X2),X2))))),X2)),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))=X3)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f3672])).
% 151.05/19.45 fof(f4335,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(X2),X2)))),X2))),inverse(X3))=multiply(inverse(X0),multiply(inverse(inverse(X2)),inverse(X3))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f3615])).
% 151.05/19.45 fof(f4348,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1))),inverse(X2))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,inverse(multiply(X4,inverse(X1)))))),inverse(multiply(inverse(X5),X5)))),multiply(X4,inverse(X2))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f2334])).
% 151.05/19.45 fof(f4401,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))),multiply(inverse(X2),X2))=X0)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f3649])).
% 151.05/19.45 fof(f4418,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))),inverse(X1)))),inverse(multiply(inverse(X2),multiply(inverse(X1),X1))))),X1)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X2)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))),multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))),multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))=X3)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f1596])).
% 151.05/19.45 fof(f4421,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X2))),inverse(X2))),inverse(X2)))),inverse(multiply(inverse(X0),multiply(inverse(X2),X2))))),X2)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),multiply(X4,inverse(X5)))),inverse(multiply(inverse(X5),X5)))),X5))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))),X3))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f1593])).
% 151.05/19.45 fof(f4422,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X3)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X4),X4)),multiply(inverse(X4),X4))),multiply(inverse(multiply(inverse(X4),X4)),multiply(inverse(X4),X4)))))),multiply(inverse(multiply(inverse(X4),X4)),multiply(inverse(X4),X4))))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X5),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X5),X4))),inverse(X4))),inverse(X4)))),inverse(multiply(inverse(X3),multiply(inverse(X4),X4))))),X4)),inverse(X1))),X2))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f1592])).
% 151.05/19.45 fof(f4426,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X0))),inverse(X0))),inverse(X0)))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(X3,inverse(X4)))),inverse(multiply(inverse(X4),X4)))),X4))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(X0),X0)))),X2))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f1459])).
% 151.05/19.45 fof(f4438,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))),inverse(X1)))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X1)),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))),multiply(inverse(X1),X1))))=X2)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f1150])).
% 151.05/19.45 fof(f4443,plain,(
% 151.05/19.45 ![X0,X1,X2]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X2))),inverse(X2))),inverse(X2)))),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))),multiply(inverse(X2),X2))))),X2))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f197])).
% 151.05/19.45 fof(f4447,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,inverse(multiply(X3,inverse(X4)))))))),inverse(multiply(inverse(inverse(multiply(X3,inverse(X4)))),inverse(multiply(X3,inverse(X4))))))=multiply(X2,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X5),X5)))),multiply(X3,inverse(X4))))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f2600])).
% 151.05/19.45 fof(f4449,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))),multiply(X3,inverse(X4)))))),multiply(inverse(multiply(inverse(multiply(X5,inverse(X1))),multiply(X5,inverse(multiply(X0,inverse(multiply(X3,inverse(X4)))))))),inverse(multiply(X0,inverse(multiply(X3,inverse(X4)))))))),inverse(multiply(inverse(inverse(multiply(X3,inverse(X4)))),inverse(multiply(X3,inverse(X4))))))=multiply(X0,inverse(multiply(X3,inverse(X4)))))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f2598])).
% 151.05/19.45 fof(f4453,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X2,multiply(inverse(X3),X3)))),inverse(multiply(inverse(multiply(inverse(X4),X4)),multiply(inverse(X4),X4))))),multiply(inverse(X4),X4))))=multiply(inverse(multiply(X2,inverse(X0))),X1))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f3675])).
% 151.05/19.45 fof(f4458,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(X3),X3)))),X3)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(X3))))),inverse(multiply(inverse(X5),X5)))),inverse(X0))),X1))),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f3951,f1473])).
% 151.05/19.45 fof(f4541,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),X0)))),X0))))),inverse(multiply(inverse(inverse(X0)),inverse(X0))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0)))))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X4),inverse(X0))))),multiply(X3,inverse(inverse(X0))))),inverse(X1))),X4))),inverse(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0))))))=X2)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3951,f4021])).
% 151.05/19.45 fof(f4542,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),X0)))),X0))))),inverse(multiply(inverse(inverse(X0)),inverse(X0))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(inverse(X0)),inverse(X0))))))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X4),inverse(X0))))),multiply(X3,inverse(inverse(X0))))),inverse(X1))),X4))),inverse(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0))))))=X2)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3951,f4541])).
% 151.05/19.45 fof(f4543,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),X0)))),X0))))),inverse(multiply(inverse(inverse(X0)),inverse(X0))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(inverse(X0)),inverse(X0))))))),multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),inverse(X0)))),inverse(inverse(X0)))),inverse(X1))),X3))),inverse(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0))))))=X2)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3951,f4542])).
% 151.05/19.45 fof(f4544,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),X0)))),X0))))),inverse(multiply(inverse(inverse(X0)),inverse(X0))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(inverse(X0)),inverse(X0))))))),multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),inverse(X0)))),inverse(inverse(X0)))),inverse(X1))),X3))),inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0)))))=X2)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3937,f4543])).
% 151.05/19.45 fof(f4545,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),X0)))),X0))))),inverse(multiply(inverse(inverse(X0)),inverse(X0))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(inverse(X0)),inverse(X0))))))),multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),inverse(X0)))),inverse(inverse(X0)))),inverse(X1))),X3))),inverse(multiply(inverse(inverse(X0)),inverse(X0))))=X2)),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3951,f4544])).
% 151.05/19.45 fof(f4601,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(inverse(X1)),inverse(X1))))),inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X1)))),multiply(X2,inverse(X1)))),inverse(X1))),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X1)))),multiply(X2,inverse(X1)))),inverse(X1))))))=multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X1)))),multiply(X2,inverse(X1))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3951,f4042])).
% 151.05/19.45 fof(f4602,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X1)))),multiply(X2,inverse(X1)))),inverse(X1))),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X1)))),multiply(X2,inverse(X1)))),inverse(X1)))))=multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X1)))),multiply(X2,inverse(X1))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3937,f4601])).
% 151.05/19.45 fof(f4603,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(inverse(X1)),inverse(X1))))=multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X1)))),multiply(X2,inverse(X1))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3951,f4602])).
% 151.05/19.45 fof(f4605,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(inverse(X1)),inverse(X1))))=multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1)))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3951,f4603])).
% 151.05/19.45 fof(f4894,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(inverse(X1)),inverse(X1))))),inverse(inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X1))))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(X0),multiply(X4,inverse(X1)))))),multiply(X3,inverse(multiply(X4,inverse(X1))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3951,f4104])).
% 151.05/19.45 fof(f4895,plain,(
% 151.05/19.45 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X1)))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(X0),multiply(X4,inverse(X1)))))),multiply(X3,inverse(multiply(X4,inverse(X1))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3937,f4894])).
% 151.05/19.45 fof(f4896,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(inverse(X1)),inverse(X1))))=multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),multiply(X3,inverse(X1)))))),multiply(X2,inverse(multiply(X3,inverse(X1))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3951,f4895])).
% 151.05/19.45 fof(f4897,plain,(
% 151.05/19.45 ![X0,X1,X2,X3]: (multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))=multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),multiply(X3,inverse(X1)))))),multiply(X2,inverse(multiply(X3,inverse(X1))))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4605,f4896])).
% 151.05/19.45 fof(f4900,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))=multiply(inverse(inverse(multiply(inverse(X0),multiply(X2,inverse(X1))))),inverse(multiply(X2,inverse(X1)))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3951,f4897])).
% 151.05/19.45 fof(f4933,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))),inverse(X1)))),inverse(X2))),X1)=multiply(inverse(inverse(X2)),inverse(multiply(inverse(X1),X1))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3951,f4117])).
% 151.05/19.45 fof(f4940,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),X0)))),X0))))),inverse(multiply(inverse(inverse(X0)),inverse(X0))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(inverse(X0)),inverse(X0))))))),multiply(inverse(inverse(X1)),inverse(multiply(inverse(inverse(X0)),inverse(X0)))))),inverse(multiply(inverse(inverse(X0)),inverse(X0))))=X2)),
% 151.05/19.45 inference(backward_demodulation,[status(thm)],[f4953,f4545])).
% 151.05/19.45 fof(f4953,plain,(
% 151.05/19.45 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))),inverse(X2))),X0)=multiply(inverse(inverse(X2)),inverse(multiply(inverse(X1),X1))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3951,f4118])).
% 151.05/19.45 fof(f4982,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(inverse(inverse(multiply(inverse(X1),X1)))))),inverse(inverse(multiply(inverse(X1),X1))))=multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3951,f4189])).
% 151.05/19.45 fof(f4983,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(inverse(multiply(inverse(X1),X1))))),inverse(inverse(multiply(inverse(X1),X1))))=multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f4193,f4982])).
% 151.05/19.45 fof(f4984,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X1)))),inverse(inverse(multiply(inverse(X1),X1))))=multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1))))),
% 151.05/19.45 inference(forward_demodulation,[status(thm)],[f3734,f4983])).
% 151.05/19.45 fof(f4998,plain,(
% 151.05/19.45 ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(X1),X1)))=multiply(inverse(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3937,f4984])).
% 151.05/19.46 fof(f5079,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (inverse(X0)=multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X3))),inverse(X3))),inverse(X3)))),inverse(multiply(inverse(X1),multiply(inverse(X3),X3))))),X3)),inverse(X0))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3951,f4246])).
% 151.05/19.46 fof(f5080,plain,(
% 151.05/19.46 ![X0,X1,X2]: (inverse(X0)=multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2)))),inverse(X0))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4933,f5079])).
% 151.05/19.46 fof(f5081,plain,(
% 151.05/19.46 ![X0,X1,X2]: (inverse(X0)=multiply(inverse(X1),multiply(inverse(multiply(inverse(X1),multiply(inverse(X2),X2))),inverse(X0))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4243,f5080])).
% 151.05/19.46 fof(f5085,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2)))),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(X0,inverse(X2))))),inverse(multiply(X0,inverse(X2)))))=inverse(multiply(X0,inverse(X2))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3951,f4248])).
% 151.05/19.46 fof(f5086,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(X0,inverse(X2))))),inverse(multiply(X0,inverse(X2)))))=inverse(multiply(X0,inverse(X2))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4243,f5085])).
% 151.05/19.46 fof(f5087,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2))))),inverse(multiply(X0,inverse(X2))))),inverse(multiply(X0,inverse(X2)))))=inverse(multiply(X0,inverse(X2))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3937,f5086])).
% 151.05/19.46 fof(f5088,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(X1),inverse(multiply(X0,inverse(X2))))),inverse(multiply(X0,inverse(X2)))))=inverse(multiply(X0,inverse(X2))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4243,f5087])).
% 151.05/19.46 fof(f5106,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X0))),inverse(X0))),inverse(X0)))),inverse(X2)))=inverse(X2))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3951,f4261])).
% 151.05/19.46 fof(f5112,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))),inverse(X2)))=inverse(X2))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3951,f4262])).
% 151.05/19.46 fof(f5161,plain,(
% 151.05/19.46 ![X0,X1]: (multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),inverse(inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1)))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4998,f4273])).
% 151.05/19.46 fof(f5162,plain,(
% 151.05/19.46 ![X0,X1]: (multiply(inverse(multiply(inverse(X0),inverse(inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1)))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4243,f5161])).
% 151.05/19.46 fof(f5163,plain,(
% 151.05/19.46 ![X0,X1]: (multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(X1),X1)))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3734,f5162])).
% 151.05/19.46 fof(f5199,plain,(
% 151.05/19.46 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),X1)))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4243,f5163])).
% 151.05/19.46 fof(f5244,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(X1),X1))))),inverse(multiply(X2,inverse(X1))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X1)))),multiply(X2,inverse(X1)))))),multiply(X3,inverse(multiply(X2,inverse(X1))))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3951,f4282])).
% 151.05/19.46 fof(f5245,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X1)))),inverse(multiply(X2,inverse(X1))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X1)))),multiply(X2,inverse(X1)))))),multiply(X3,inverse(multiply(X2,inverse(X1))))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4243,f5244])).
% 151.05/19.46 fof(f5246,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(inverse(X0),inverse(multiply(X1,inverse(X2))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))))),multiply(X3,inverse(multiply(X1,inverse(X2))))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4243,f5245])).
% 151.05/19.46 fof(f5247,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(X0),inverse(multiply(X1,inverse(X2))))=multiply(inverse(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2))))),inverse(multiply(X1,inverse(X2)))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3951,f5246])).
% 151.05/19.46 fof(f5248,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(X0),inverse(multiply(X1,inverse(X2))))=multiply(inverse(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),X2))),inverse(X2)))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4900,f5247])).
% 151.05/19.46 fof(f5255,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2)))))),multiply(X3,inverse(multiply(X0,inverse(X2)))))),inverse(multiply(X0,inverse(X2))))))=multiply(X0,inverse(X2)))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5199,f4284])).
% 151.05/19.46 fof(f5256,plain,(
% 151.05/19.46 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2)))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(X0,inverse(X2))))),inverse(multiply(X0,inverse(X2))))))=multiply(X0,inverse(X2)))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3951,f5255])).
% 151.05/19.46 fof(f5257,plain,(
% 151.05/19.46 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2)))),inverse(multiply(X0,inverse(X2))))),inverse(multiply(X0,inverse(X2))))))=multiply(X0,inverse(X2)))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4243,f5256])).
% 151.05/19.46 fof(f5258,plain,(
% 151.05/19.46 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(inverse(multiply(inverse(X1),inverse(multiply(X0,inverse(X2))))),inverse(multiply(X0,inverse(X2))))))=multiply(X0,inverse(X2)))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4243,f5257])).
% 151.05/19.46 fof(f5260,plain,(
% 151.05/19.46 ![X0,X1]: (inverse(inverse(multiply(X0,inverse(X1))))=multiply(X0,inverse(X1)))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5088,f5258])).
% 151.05/19.46 fof(f5278,plain,(
% 151.05/19.46 ![X0,X1]: (multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1)))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4998,f4289])).
% 151.05/19.46 fof(f5279,plain,(
% 151.05/19.46 ![X0,X1]: (inverse(inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(X1),X1)))))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5199,f5278])).
% 151.05/19.46 fof(f5280,plain,(
% 151.05/19.46 ![X0,X1]: (multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(X1),X1)))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5260,f5279])).
% 151.05/19.46 fof(f5281,plain,(
% 151.05/19.46 ![X0,X1]: (inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5199,f5280])).
% 151.05/19.46 fof(f5299,plain,(
% 151.05/19.46 ![X0]: (inverse(inverse(X0))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5199,f5281])).
% 151.05/19.46 fof(f5305,plain,(
% 151.05/19.46 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2))))=X1)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5199,f4294])).
% 151.05/19.46 fof(f5306,plain,(
% 151.05/19.46 ![X0,X1]: (inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1)))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3951,f5305])).
% 151.05/19.46 fof(f5307,plain,(
% 151.05/19.46 ![X0,X1]: (inverse(multiply(multiply(inverse(X0),X1),inverse(X1)))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5299,f5306])).
% 151.05/19.46 fof(f5311,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X3),multiply(inverse(X2),X2))))),X1))=X3)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5199,f4296])).
% 151.05/19.46 fof(f5312,plain,(
% 151.05/19.46 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))),inverse(multiply(inverse(X2),multiply(inverse(X1),X1))))),X0))=X2)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3951,f5311])).
% 151.05/19.46 fof(f5313,plain,(
% 151.05/19.46 ![X0,X1]: (inverse(multiply(inverse(inverse(multiply(inverse(X0),multiply(inverse(X1),X1)))),inverse(multiply(inverse(X1),X1))))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4953,f5312])).
% 151.05/19.46 fof(f5316,plain,(
% 151.05/19.46 ![X0,X1]: (inverse(multiply(inverse(X0),multiply(inverse(X1),X1)))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4243,f5313])).
% 151.05/19.46 fof(f5381,plain,(
% 151.05/19.46 ![X0,X1,X2]: (inverse(multiply(inverse(X0),multiply(X1,inverse(X2))))=multiply(inverse(multiply(X1,inverse(X2))),X0))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5199,f4310])).
% 151.05/19.46 fof(f5382,plain,(
% 151.05/19.46 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))=multiply(inverse(X2),multiply(X0,inverse(X1))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5199,f4312])).
% 151.05/19.46 fof(f5395,plain,(
% 151.05/19.46 ![X0,X1,X2]: (X0=multiply(multiply(inverse(inverse(multiply(inverse(X1),X1))),multiply(inverse(inverse(X0)),inverse(X2))),X2))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5382,f4317])).
% 151.05/19.46 fof(f5396,plain,(
% 151.05/19.46 ![X0,X1]: (X0=multiply(multiply(inverse(inverse(X0)),inverse(X1)),X1))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3746,f5395])).
% 151.05/19.46 fof(f5397,plain,(
% 151.05/19.46 ![X0,X1]: (X0=multiply(multiply(X0,inverse(X1)),X1))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5299,f5396])).
% 151.05/19.46 fof(f5398,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))=multiply(X1,inverse(X2)))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5299,f4318])).
% 151.05/19.46 fof(f5409,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0))))))),inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,inverse(X0))))))=X1)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5382,f4320])).
% 151.05/19.46 fof(f5410,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0)))))),inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,inverse(X0))))))=X1)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4290,f5409])).
% 151.05/19.46 fof(f5411,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X1))))))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4290,f5410])).
% 151.05/19.46 fof(f5412,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(X1))),multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X1))))))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5316,f5411])).
% 151.05/19.46 fof(f5413,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(X0,multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X2)))),multiply(inverse(inverse(X2)),inverse(X2))))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5382,f5412])).
% 151.05/19.46 fof(f5414,plain,(
% 151.05/19.46 ![X0,X1]: (multiply(X0,multiply(inverse(inverse(X1)),inverse(X1)))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4290,f5413])).
% 151.05/19.46 fof(f5415,plain,(
% 151.05/19.46 ![X0,X1]: (multiply(X0,multiply(X1,inverse(X1)))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5299,f5414])).
% 151.05/19.46 fof(f5515,plain,(
% 151.05/19.46 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),X2))),inverse(X2))),inverse(X2))))=X2)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5199,f4332])).
% 151.05/19.46 fof(f5516,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(multiply(inverse(X0),X0),X1))),inverse(X1))),inverse(X1))),multiply(inverse(X2),X2))=X1)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5381,f5515])).
% 151.05/19.46 fof(f5517,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(multiply(inverse(inverse(X0)),multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),X0))),inverse(X0))),multiply(inverse(X2),X2))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5382,f5516])).
% 151.05/19.46 fof(f5518,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(multiply(X0,multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),X0))),inverse(X0))),multiply(inverse(X2),X2))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5299,f5517])).
% 151.05/19.46 fof(f5519,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(multiply(X0,multiply(multiply(multiply(inverse(X1),X1),X0),inverse(X0))),multiply(inverse(X2),X2))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5299,f5518])).
% 151.05/19.46 fof(f5520,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),X2))),inverse(X2))),inverse(X2)))),inverse(multiply(inverse(X3),multiply(inverse(X2),X2))))),X2))=X3)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5199,f4333])).
% 151.05/19.46 fof(f5521,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(multiply(inverse(inverse(multiply(multiply(inverse(X2),X2),X0))),inverse(X0))),inverse(X0)))),inverse(multiply(inverse(X3),multiply(inverse(X0),X0)))))=X3)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5382,f5520])).
% 151.05/19.46 fof(f5522,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),X0))),inverse(X0))),inverse(X0))),multiply(inverse(X2),X2)),inverse(multiply(inverse(X3),multiply(inverse(X0),X0)))))=X3)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5381,f5521])).
% 151.05/19.46 fof(f5523,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(multiply(multiply(inverse(inverse(X0)),multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),X0))),inverse(X0))),multiply(inverse(X2),X2)),inverse(multiply(inverse(X3),multiply(inverse(X0),X0)))))=X3)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5382,f5522])).
% 151.05/19.46 fof(f5524,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(multiply(multiply(X0,multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),X0))),inverse(X0))),multiply(inverse(X2),X2)),inverse(multiply(inverse(X3),multiply(inverse(X0),X0)))))=X3)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5299,f5523])).
% 151.05/19.46 fof(f5525,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(multiply(multiply(X0,multiply(multiply(multiply(inverse(X1),X1),X0),inverse(X0))),multiply(inverse(X2),X2)),inverse(multiply(inverse(X3),multiply(inverse(X0),X0)))))=X3)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5299,f5524])).
% 151.05/19.46 fof(f5526,plain,(
% 151.05/19.46 ![X0,X1]: (multiply(inverse(X0),multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X0),X0)))))=X1)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5519,f5525])).
% 151.05/19.46 fof(f5528,plain,(
% 151.05/19.46 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=X1)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5316,f5526])).
% 151.05/19.46 fof(f5532,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(multiply(inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(X2),X2)))),X2),inverse(X3))=multiply(inverse(X0),multiply(inverse(inverse(X2)),inverse(X3))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5299,f4335])).
% 151.05/19.46 fof(f5533,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(multiply(multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))),X0),inverse(X3))=multiply(inverse(X1),multiply(inverse(inverse(X0)),inverse(X3))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5382,f5532])).
% 151.05/19.46 fof(f5534,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(multiply(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))),X2),inverse(X3))=multiply(inverse(X0),multiply(inverse(inverse(X2)),inverse(X3))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f3746,f5533])).
% 151.05/19.46 fof(f5535,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(multiply(inverse(X0),X1),inverse(X2))=multiply(inverse(X0),multiply(inverse(inverse(X1)),inverse(X2))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5199,f5534])).
% 151.05/19.46 fof(f5539,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(multiply(inverse(X0),X1),inverse(X2))=multiply(inverse(X0),multiply(X1,inverse(X2))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5299,f5535])).
% 151.05/19.46 fof(f5627,plain,(
% 151.05/19.46 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1),inverse(X2))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,inverse(multiply(X4,inverse(X1)))))),inverse(multiply(inverse(X5),X5)))),multiply(X4,inverse(X2))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5299,f4348])).
% 151.05/19.46 fof(f5628,plain,(
% 151.05/19.46 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),multiply(X1,inverse(X2)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,inverse(multiply(X4,inverse(X1)))))),inverse(multiply(inverse(X5),X5)))),multiply(X4,inverse(X2))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5539,f5627])).
% 151.05/19.46 fof(f5629,plain,(
% 151.05/19.46 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,multiply(X1,inverse(X2)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,inverse(multiply(X4,inverse(X1)))))),inverse(multiply(inverse(X5),X5)))),multiply(X4,inverse(X2))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4243,f5628])).
% 151.05/19.46 fof(f5630,plain,(
% 151.05/19.46 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(X1,inverse(X2)))=multiply(multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,inverse(multiply(X4,inverse(X1))))),multiply(X4,inverse(X2))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4243,f5629])).
% 151.05/19.46 fof(f5631,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(X0,multiply(X1,inverse(X2)))=multiply(multiply(X0,inverse(multiply(X3,inverse(X1)))),multiply(X3,inverse(X2))))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5398,f5630])).
% 151.05/19.46 fof(f6008,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(multiply(multiply(inverse(X0),X1),inverse(X1))),multiply(inverse(X2),X2))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5299,f4401])).
% 151.05/19.46 fof(f6015,plain,(
% 151.05/19.46 ![X0,X1]: (multiply(X0,multiply(inverse(X1),X1))=X0)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5307,f6008])).
% 151.05/19.46 fof(f6099,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X0))),inverse(X0))),inverse(X0)))),inverse(multiply(inverse(X2),multiply(inverse(X0),X0))))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X2)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))),multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))),multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))=X3)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5382,f4418])).
% 151.05/19.46 fof(f6100,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X0))),inverse(X0))),inverse(X0)))),inverse(multiply(inverse(X2),multiply(inverse(X0),X0)))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X2)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))),multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))),multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))))))=X3)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5539,f6099])).
% 151.05/19.46 fof(f6101,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X0))),inverse(X0))),inverse(X0)))),multiply(inverse(multiply(inverse(X2),multiply(inverse(X0),X0))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X2)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))),multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))),multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))))=X3)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5539,f6100])).
% 151.05/19.46 fof(f6102,plain,(
% 151.05/19.46 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X0))),inverse(X0))),inverse(X0))),X1),multiply(inverse(multiply(inverse(X2),multiply(inverse(X0),X0))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X2)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))),multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))),multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))))=X3)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5381,f6101])).
% 151.05/19.46 fof(f6103,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(X0),multiply(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X0),X0))),multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X0))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X1)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))),multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))),multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))))=X2)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4953,f6102])).
% 151.05/19.46 fof(f6104,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(X0),multiply(X0,multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X0))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X1)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))),multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))),multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))))=X2)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4256,f6103])).
% 151.05/19.46 fof(f6105,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X0)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))),multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))),multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))=X2)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5528,f6104])).
% 151.05/19.46 fof(f6106,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X0)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))))),multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))))=X1)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5316,f6105])).
% 151.05/19.46 fof(f6107,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(X0,multiply(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))),multiply(inverse(multiply(inverse(X2),X0)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))),multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))))=X2)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5382,f6106])).
% 151.05/19.46 fof(f6108,plain,(
% 151.05/19.46 ![X0,X1,X2]: (multiply(X0,multiply(inverse(multiply(inverse(X1),X0)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))))=X1)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4290,f6107])).
% 151.05/19.46 fof(f6113,plain,(
% 151.05/19.46 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),X0)))=X1)),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5199,f6108])).
% 151.05/19.46 fof(f6134,plain,(
% 151.05/19.46 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(X0),multiply(multiply(inverse(X1),multiply(inverse(multiply(inverse(X2),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X1))),inverse(X1))),inverse(X1)))),inverse(multiply(inverse(X0),multiply(inverse(X1),X1))))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),multiply(X4,inverse(X5)))),inverse(multiply(inverse(X5),X5)))),X5))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))),X3))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5382,f4421])).
% 151.05/19.46 fof(f6135,plain,(
% 151.05/19.46 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(X0),multiply(inverse(X1),multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X1))),inverse(X1))),inverse(X1)))),inverse(multiply(inverse(X0),multiply(inverse(X1),X1)))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),multiply(X4,inverse(X5)))),inverse(multiply(inverse(X5),X5)))),X5)))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))),X3))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5539,f6134])).
% 151.05/19.46 fof(f6136,plain,(
% 151.05/19.46 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(X0),multiply(inverse(X1),multiply(inverse(multiply(inverse(X2),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X1))),inverse(X1))),inverse(X1)))),multiply(inverse(multiply(inverse(X0),multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),multiply(X4,inverse(X5)))),inverse(multiply(inverse(X5),X5)))),X5))))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))),X3))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5539,f6135])).
% 151.05/19.46 fof(f6137,plain,(
% 151.05/19.46 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(X0),multiply(inverse(X1),multiply(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X1))),inverse(X1))),inverse(X1))),X2),multiply(inverse(multiply(inverse(X0),multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),multiply(X4,inverse(X5)))),inverse(multiply(inverse(X5),X5)))),X5))))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))),X3))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f5381,f6136])).
% 151.05/19.46 fof(f6138,plain,(
% 151.05/19.46 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(X1),multiply(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X1),X1))),multiply(inverse(multiply(inverse(X0),multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(X3,inverse(X4)))),inverse(multiply(inverse(X4),X4)))),X4))))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))),X2))),
% 151.05/19.46 inference(forward_demodulation,[status(thm)],[f4953,f6137])).
% 151.05/19.46 fof(f6139,plain,(
% 151.05/19.46 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(X1),multiply(X1,multiply(inverse(multiply(inverse(X0),multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(X3,inverse(X4)))),inverse(multiply(inverse(X4),X4)))),X4))))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))),X2))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f4256,f6138])).
% 151.05/19.47 fof(f6140,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(X0),multiply(inverse(X1),X1))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(X3,inverse(X4)))),inverse(multiply(inverse(X4),X4)))),X4))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))),X2))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5528,f6139])).
% 151.05/19.47 fof(f6141,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(X1,inverse(X2)))),inverse(multiply(inverse(X2),X2)))),X2))=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))),X0))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5081,f6140])).
% 151.05/19.47 fof(f6142,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(X2,inverse(X0)))),inverse(multiply(inverse(X0),X0))))=multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6141])).
% 151.05/19.47 fof(f6143,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (multiply(inverse(X0),inverse(multiply(inverse(X1),multiply(X2,inverse(X0)))))=multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5199,f6142])).
% 151.05/19.47 fof(f6144,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(inverse(multiply(X1,inverse(X0))),X2))=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))),X2))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5381,f6143])).
% 151.05/19.47 fof(f6154,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(multiply(X1,inverse(X0))),X2))=multiply(inverse(X1),X2))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5199,f6144])).
% 151.05/19.47 fof(f6155,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))),multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3)))))),multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3)))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X4),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X4),X3))),inverse(X3))),inverse(X3)))),inverse(multiply(inverse(X2),multiply(inverse(X3),X3))))),X3)),inverse(X0))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5398,f4422])).
% 151.05/19.47 fof(f6156,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))),multiply(inverse(multiply(inverse(X2),X3)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))),multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X4),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X4),X1))),inverse(X1))),inverse(X1)))),inverse(multiply(inverse(X3),multiply(inverse(X1),X1))))),X1)),inverse(X0))),X2))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6155])).
% 151.05/19.47 fof(f6157,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))),multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X4),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X4),X3))),inverse(X3))),inverse(X3)))),inverse(multiply(inverse(X2),multiply(inverse(X3),X3))))),X3)),inverse(X0))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f4290,f6156])).
% 151.05/19.47 fof(f6158,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(inverse(X1),X2)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X4))),inverse(X4))),inverse(X4)))),inverse(multiply(inverse(X2),multiply(inverse(X4),X4))))),X4)),inverse(X0))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5199,f6157])).
% 151.05/19.47 fof(f6159,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(inverse(X1),X2)))=multiply(inverse(multiply(multiply(inverse(X3),multiply(inverse(multiply(inverse(X4),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X4),X3))),inverse(X3))),inverse(X3)))),inverse(multiply(inverse(X2),multiply(inverse(X3),X3))))),inverse(X0))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6158])).
% 151.05/19.47 fof(f6160,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(inverse(X1),X2)))=multiply(inverse(multiply(inverse(X3),multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X4),X3))),inverse(X3))),inverse(X3)))),inverse(multiply(inverse(X2),multiply(inverse(X3),X3)))),inverse(X0)))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5539,f6159])).
% 151.05/19.47 fof(f6161,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(inverse(X1),X2)))=multiply(multiply(inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X4))),inverse(X4))),inverse(X4)))),inverse(multiply(inverse(X2),multiply(inverse(X4),X4)))),inverse(X0))),X4),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5381,f6160])).
% 151.05/19.47 fof(f6162,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(inverse(X1),X2)))=multiply(multiply(inverse(multiply(inverse(multiply(inverse(X3),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X4))),inverse(X4))),inverse(X4)))),multiply(inverse(multiply(inverse(X2),multiply(inverse(X4),X4))),inverse(X0)))),X4),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5539,f6161])).
% 151.05/19.47 fof(f6163,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(inverse(X1),X2)))=multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(inverse(X3),X3))),inverse(X0))),multiply(inverse(X4),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X4),X3))),inverse(X3))),inverse(X3)))),X3),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5381,f6162])).
% 151.05/19.47 fof(f6164,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(inverse(X1),X2)))=multiply(multiply(multiply(inverse(multiply(X2,inverse(X0))),multiply(inverse(X3),multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X4))),inverse(X4))),inverse(X4)))),X4),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5316,f6163])).
% 151.05/19.47 fof(f6165,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(inverse(X1),X2)))=multiply(multiply(multiply(inverse(multiply(X2,inverse(X0))),inverse(X3)),X3),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5112,f6164])).
% 151.05/19.47 fof(f6182,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(X1),X2)))=multiply(inverse(multiply(X2,inverse(X0))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5397,f6165])).
% 151.05/19.47 fof(f6207,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(X1,inverse(X2)))),inverse(multiply(inverse(X2),X2)))),X2))=multiply(inverse(multiply(X1,inverse(multiply(inverse(X3),X3)))),X0))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5106,f4426])).
% 151.05/19.47 fof(f6208,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(X2,inverse(X0)))),inverse(multiply(inverse(X0),X0))))=multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6207])).
% 151.05/19.47 fof(f6209,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (multiply(inverse(X0),inverse(multiply(inverse(X1),multiply(X2,inverse(X0)))))=multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5199,f6208])).
% 151.05/19.47 fof(f6210,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(inverse(multiply(X1,inverse(X0))),X2))=multiply(inverse(multiply(X1,inverse(multiply(inverse(X3),X3)))),X2))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5381,f6209])).
% 151.05/19.47 fof(f6211,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(inverse(X0),X1)=multiply(inverse(multiply(X0,inverse(multiply(inverse(X2),X2)))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6154,f6210])).
% 151.05/19.47 fof(f6212,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(inverse(X0),X1)=multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X1),X0))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6182,f6211])).
% 151.05/19.47 fof(f6213,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(inverse(X0),X1)=multiply(inverse(X2),multiply(X2,inverse(multiply(inverse(X1),X0)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5539,f6212])).
% 151.05/19.47 fof(f6222,plain,(
% 151.05/19.47 ![X0,X1]: (multiply(inverse(X0),X1)=inverse(multiply(inverse(X1),X0)))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5528,f6213])).
% 151.05/19.47 fof(f6322,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))),inverse(X1))),X0),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X1)),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))),multiply(inverse(X1),X1))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5381,f4438])).
% 151.05/19.47 fof(f6323,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))),inverse(X1))),multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X1)),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))),multiply(inverse(X1),X1)))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5539,f6322])).
% 151.05/19.47 fof(f6324,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X0)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))))),multiply(inverse(X0),X0))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X0))),inverse(X0))))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6182,f6323])).
% 151.05/19.47 fof(f6325,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(X0,multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X1),X0))),inverse(X0)))),multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X0)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))))),multiply(inverse(X0),X0))))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6324])).
% 151.05/19.47 fof(f6326,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(X0,multiply(multiply(inverse(inverse(multiply(inverse(X1),X0))),inverse(X0)),multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X0)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))))),multiply(inverse(X0),X0))))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5260,f6325])).
% 151.05/19.47 fof(f6327,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(X0,multiply(multiply(multiply(inverse(X1),X0),inverse(X0)),multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X0)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))))),multiply(inverse(X0),X0))))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5299,f6326])).
% 151.05/19.47 fof(f6328,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(X0,multiply(multiply(inverse(X1),multiply(X0,inverse(X0))),multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X0)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))))),multiply(inverse(X0),X0))))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5539,f6327])).
% 151.05/19.47 fof(f6329,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(X0,multiply(inverse(X1),multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X0)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))))),multiply(inverse(X0),X0))))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5415,f6328])).
% 151.05/19.47 fof(f6330,plain,(
% 151.05/19.47 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X0)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))))),multiply(inverse(X0),X0))))=X1)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5528,f6329])).
% 151.05/19.47 fof(f6331,plain,(
% 151.05/19.47 ![X0,X1]: (multiply(X0,multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(multiply(inverse(X1),X0)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))))))=X1)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6330])).
% 151.05/19.47 fof(f6332,plain,(
% 151.05/19.47 ![X0,X1]: (multiply(X0,multiply(inverse(multiply(inverse(X1),X0)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))=X1)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f4290,f6331])).
% 151.05/19.47 fof(f6333,plain,(
% 151.05/19.47 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),X0)))=X1)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5199,f6332])).
% 151.05/19.47 fof(f6335,plain,(
% 151.05/19.47 ![X0,X1]: (multiply(X0,multiply(inverse(X0),X1))=X1)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6222,f6333])).
% 151.05/19.47 fof(f6368,plain,(
% 151.05/19.47 ![X0,X1]: (X0=multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))),multiply(inverse(X1),X1)))),inverse(multiply(inverse(X1),X1))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f4933,f4443])).
% 151.05/19.47 fof(f6369,plain,(
% 151.05/19.47 ![X0,X1]: (X0=multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5248,f6368])).
% 151.05/19.47 fof(f6370,plain,(
% 151.05/19.47 ![X0,X1]: (X0=inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f4290,f6369])).
% 151.05/19.47 fof(f6371,plain,(
% 151.05/19.47 ![X0,X1]: (X0=multiply(inverse(inverse(multiply(inverse(X1),X1))),X0))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6222,f6370])).
% 151.05/19.47 fof(f6372,plain,(
% 151.05/19.47 ![X0,X1]: (X0=multiply(inverse(multiply(inverse(X1),X1)),X0))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f3937,f6371])).
% 151.05/19.47 fof(f6375,plain,(
% 151.05/19.47 ![X0,X1]: (X0=multiply(multiply(inverse(X1),X1),X0))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6222,f6372])).
% 151.05/19.47 fof(f6413,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,inverse(multiply(X3,inverse(X4))))))))=multiply(X2,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X5),X5)))),multiply(X3,inverse(X4))))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5199,f4447])).
% 151.05/19.47 fof(f6414,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(X3))))))),multiply(X0,inverse(X4)))=multiply(X1,inverse(multiply(inverse(multiply(inverse(X4),inverse(multiply(inverse(X5),X5)))),multiply(X2,inverse(X3))))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6413])).
% 151.05/19.47 fof(f6415,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(multiply(X0,inverse(multiply(X1,inverse(X2)))),inverse(X3))=multiply(X0,inverse(multiply(inverse(multiply(inverse(X3),inverse(multiply(inverse(X4),X4)))),multiply(X1,inverse(X2))))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5398,f6414])).
% 151.05/19.47 fof(f6416,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(multiply(X0,inverse(multiply(X1,inverse(X2)))),inverse(X3))=multiply(X0,multiply(inverse(multiply(X1,inverse(X2))),multiply(inverse(X3),inverse(multiply(inverse(X4),X4))))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6415])).
% 151.05/19.47 fof(f6417,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(multiply(X0,inverse(multiply(X1,inverse(X2)))),inverse(X3))=multiply(X0,multiply(X2,inverse(multiply(inverse(multiply(inverse(X3),inverse(multiply(inverse(X4),X4)))),X1)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6182,f6416])).
% 151.05/19.47 fof(f6418,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(multiply(X0,inverse(multiply(X1,inverse(X2)))),inverse(X3))=multiply(X0,multiply(X2,multiply(inverse(X1),multiply(inverse(X3),inverse(multiply(inverse(X4),X4)))))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6417])).
% 151.05/19.47 fof(f6419,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (multiply(multiply(X0,inverse(multiply(X1,inverse(X2)))),inverse(X3))=multiply(X0,multiply(X2,multiply(inverse(X1),inverse(X3)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5199,f6418])).
% 151.05/19.47 fof(f6437,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X2)))),multiply(X3,inverse(X4)))))),multiply(inverse(multiply(inverse(multiply(X5,inverse(X1))),multiply(X5,inverse(multiply(X0,inverse(multiply(X3,inverse(X4)))))))),inverse(multiply(X0,inverse(multiply(X3,inverse(X4))))))))=multiply(X0,inverse(multiply(X3,inverse(X4)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5199,f4449])).
% 151.05/19.47 fof(f6438,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,inverse(multiply(X3,inverse(X4)))))))),inverse(multiply(X2,inverse(multiply(X3,inverse(X4))))))),multiply(X2,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X5),X5)))),multiply(X3,inverse(X4))))))=multiply(X2,inverse(multiply(X3,inverse(X4)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6437])).
% 151.05/19.47 fof(f6439,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(X0,inverse(multiply(X1,inverse(X2)))),inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(X3),inverse(multiply(inverse(X4),X4)))),multiply(X1,inverse(X2)))))),inverse(multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(multiply(X0,inverse(multiply(X1,inverse(X2)))))))))))=multiply(X0,inverse(multiply(X1,inverse(X2)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6182,f6438])).
% 151.05/19.47 fof(f6440,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,multiply(X1,multiply(inverse(X2),inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(X3),inverse(multiply(inverse(X4),X4)))),multiply(X2,inverse(X1)))))),inverse(multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(multiply(X0,inverse(multiply(X2,inverse(X1)))))))))))))=multiply(X0,inverse(multiply(X2,inverse(X1)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6419,f6439])).
% 151.05/19.47 fof(f6441,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,multiply(X1,multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(multiply(X0,inverse(multiply(X2,inverse(X1))))))))),multiply(X0,inverse(multiply(inverse(multiply(inverse(X4),inverse(multiply(inverse(X5),X5)))),multiply(X2,inverse(X1)))))))))=multiply(X0,inverse(multiply(X2,inverse(X1)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6440])).
% 151.05/19.47 fof(f6442,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,multiply(X1,multiply(inverse(X2),multiply(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(multiply(X0,inverse(multiply(X2,inverse(X1))))))),multiply(X0,inverse(multiply(inverse(multiply(inverse(X4),inverse(multiply(inverse(X5),X5)))),multiply(X2,inverse(X1)))))))))=multiply(X0,inverse(multiply(X2,inverse(X1)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5299,f6441])).
% 151.05/19.47 fof(f6443,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(X1,multiply(inverse(X2),multiply(multiply(X3,inverse(multiply(X0,inverse(multiply(X2,inverse(X1)))))),multiply(X0,inverse(multiply(inverse(multiply(inverse(X3),inverse(multiply(inverse(X4),X4)))),multiply(X2,inverse(X1)))))))))=multiply(X0,inverse(multiply(X2,inverse(X1)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5398,f6442])).
% 151.05/19.47 fof(f6444,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(X1,multiply(inverse(X2),multiply(X3,multiply(multiply(X2,inverse(X1)),inverse(multiply(inverse(multiply(inverse(X3),inverse(multiply(inverse(X4),X4)))),multiply(X2,inverse(X1)))))))))=multiply(X0,inverse(multiply(X2,inverse(X1)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5631,f6443])).
% 151.05/19.47 fof(f6445,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(X1,multiply(inverse(X2),multiply(X3,multiply(inverse(X3),inverse(multiply(inverse(X4),X4)))))))=multiply(X0,inverse(multiply(X2,inverse(X1)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6113,f6444])).
% 151.05/19.47 fof(f6446,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (multiply(X0,multiply(X1,multiply(inverse(X2),inverse(multiply(inverse(X3),X3)))))=multiply(X0,inverse(multiply(X2,inverse(X1)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6335,f6445])).
% 151.05/19.47 fof(f6452,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(X0,multiply(X1,inverse(X2)))=multiply(X0,inverse(multiply(X2,inverse(X1)))))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5199,f6446])).
% 151.05/19.47 fof(f6494,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X2,multiply(inverse(X3),X3)))),inverse(multiply(inverse(multiply(inverse(X4),X4)),multiply(inverse(X4),X4))))),multiply(inverse(X4),X4))))=multiply(inverse(multiply(X2,inverse(X0))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5299,f4453])).
% 151.05/19.47 fof(f6495,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(multiply(inverse(X2),multiply(X3,multiply(inverse(X4),X4)))),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))))=multiply(inverse(multiply(X3,inverse(X0))),X2))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6494])).
% 151.05/19.47 fof(f6496,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(inverse(multiply(inverse(X1),multiply(X2,multiply(inverse(X3),X3)))),inverse(multiply(inverse(multiply(inverse(X4),X4)),multiply(inverse(X4),X4)))))=multiply(inverse(multiply(X2,inverse(X0))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f4290,f6495])).
% 151.05/19.47 fof(f6497,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(inverse(X1),multiply(X2,multiply(inverse(X3),X3)))))=multiply(inverse(multiply(X2,inverse(X0))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5199,f6496])).
% 151.05/19.47 fof(f6498,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (multiply(X0,multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),X3))=multiply(inverse(multiply(X1,inverse(X0))),X3))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6222,f6497])).
% 151.05/19.47 fof(f6499,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(X0,multiply(inverse(X1),X2))=multiply(inverse(multiply(X1,inverse(X0))),X2))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6015,f6498])).
% 151.05/19.47 fof(f6528,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(X3),X3)))),X3)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(X3))))),inverse(multiply(inverse(X5),X5)))),inverse(X0))),X1))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5299,f4458])).
% 151.05/19.47 fof(f6529,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,multiply(inverse(X1),multiply(inverse(multiply(inverse(X2),X3)),inverse(multiply(inverse(X1),X1)))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(inverse(X1))))),inverse(multiply(inverse(X5),X5)))),inverse(X0))),X2))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6528])).
% 151.05/19.47 fof(f6530,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,multiply(inverse(X1),inverse(multiply(inverse(X2),X3))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(inverse(X1))))),inverse(multiply(inverse(X5),X5)))),inverse(X0))),X2))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5199,f6529])).
% 151.05/19.47 fof(f6531,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,multiply(inverse(X1),multiply(inverse(X2),X3)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(X1))))),inverse(multiply(inverse(X5),X5)))),inverse(X0))),X3))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6222,f6530])).
% 151.05/19.47 fof(f6532,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,multiply(inverse(X1),multiply(inverse(X2),X3)))=multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(X1))))),inverse(multiply(inverse(X5),X5))))),X3)))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6499,f6531])).
% 151.05/19.47 fof(f6533,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,multiply(inverse(X1),multiply(inverse(X2),X3)))=multiply(X0,multiply(multiply(inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(X1))))),inverse(multiply(inverse(X5),X5))),X3)))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5260,f6532])).
% 151.05/19.47 fof(f6534,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(inverse(X1),multiply(inverse(X2),X3)))=multiply(X0,multiply(inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(X1))))),X3)))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5199,f6533])).
% 151.05/19.47 fof(f6535,plain,(
% 151.05/19.47 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(inverse(X1),multiply(inverse(X2),X3)))=multiply(X0,multiply(multiply(inverse(multiply(X4,inverse(inverse(X1)))),multiply(X4,inverse(X2))),X3)))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f6534])).
% 151.05/19.47 fof(f6536,plain,(
% 151.05/19.47 ![X0,X1,X2,X3]: (multiply(X0,multiply(inverse(X1),multiply(inverse(X2),X3)))=multiply(X0,multiply(multiply(inverse(X1),inverse(X2)),X3)))),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5398,f6535])).
% 151.05/19.47 fof(f7283,plain,(
% 151.05/19.47 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),X0)))),X0))))),inverse(multiply(inverse(inverse(X0)),inverse(X0))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(inverse(X0)),inverse(X0))))))),multiply(inverse(inverse(X1)),inverse(multiply(inverse(inverse(X0)),inverse(X0))))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5199,f4940])).
% 151.05/19.47 fof(f7284,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(inverse(X1)),inverse(X1))))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1))))),inverse(multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(inverse(X1)),inverse(X1)))))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5382,f7283])).
% 151.05/19.47 fof(f7285,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(inverse(inverse(X1))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),X0)))),X0))))),inverse(multiply(inverse(inverse(X0)),inverse(X0))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(inverse(X0)),inverse(X0))))))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6499,f7284])).
% 151.05/19.47 fof(f7286,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(inverse(inverse(inverse(X0))),multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1))))),inverse(multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(inverse(X1)),inverse(X1)))))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f4309,f7285])).
% 151.05/19.47 fof(f7287,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1))))),inverse(multiply(inverse(inverse(X1)),inverse(X1))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(inverse(X1)),inverse(X1)))))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f5299,f7286])).
% 151.05/19.47 fof(f7288,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(inverse(X0),multiply(multiply(inverse(inverse(X1)),inverse(X1)),multiply(inverse(inverse(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1)))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(inverse(X1)),inverse(X1))))))))=X2)),
% 151.05/19.47 inference(forward_demodulation,[status(thm)],[f6499,f7287])).
% 151.05/19.47 fof(f7289,plain,(
% 151.05/19.47 ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(inverse(X1)),multiply(inverse(X1),multiply(inverse(inverse(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1)))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(inverse(X1)),inverse(X1)))))))))=X2)),
% 151.05/19.48 inference(forward_demodulation,[status(thm)],[f6536,f7288])).
% 151.05/19.48 fof(f7290,plain,(
% 151.05/19.48 ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(inverse(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1)))))),inverse(multiply(inverse(X2),inverse(multiply(inverse(inverse(X1)),inverse(X1)))))))=X2)),
% 151.05/19.48 inference(forward_demodulation,[status(thm)],[f5528,f7289])).
% 151.05/19.48 fof(f7291,plain,(
% 151.05/19.48 ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(inverse(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1)))))),multiply(multiply(inverse(inverse(X1)),inverse(X1)),inverse(inverse(X2)))))=X2)),
% 151.05/19.48 inference(forward_demodulation,[status(thm)],[f6452,f7290])).
% 151.05/19.48 fof(f7292,plain,(
% 151.05/19.48 ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(inverse(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1)))))),multiply(inverse(inverse(X1)),multiply(inverse(X1),inverse(inverse(X2))))))=X2)),
% 151.05/19.48 inference(forward_demodulation,[status(thm)],[f6536,f7291])).
% 151.05/19.48 fof(f7293,plain,(
% 151.05/19.48 ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1)))),multiply(inverse(inverse(X1)),multiply(inverse(X1),inverse(inverse(X2))))))=X2)),
% 151.05/19.48 inference(forward_demodulation,[status(thm)],[f5299,f7292])).
% 151.05/19.48 fof(f7294,plain,(
% 151.05/19.48 ![X0,X1,X2]: (multiply(inverse(X0),multiply(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))),X1),multiply(inverse(inverse(inverse(X1))),multiply(inverse(inverse(X1)),multiply(inverse(X1),inverse(inverse(X2)))))))=X2)),
% 151.05/19.48 inference(forward_demodulation,[status(thm)],[f6499,f7293])).
% 151.05/19.48 fof(f7295,plain,(
% 151.05/19.48 ![X0,X1,X2]: (multiply(inverse(X0),multiply(multiply(multiply(inverse(X1),X1),multiply(inverse(inverse(X0)),X1)),multiply(inverse(inverse(inverse(X1))),multiply(inverse(inverse(X1)),multiply(inverse(X1),inverse(inverse(X2)))))))=X2)),
% 151.05/19.48 inference(forward_demodulation,[status(thm)],[f6499,f7294])).
% 151.05/19.48 fof(f7296,plain,(
% 151.05/19.48 ![X0,X1,X2]: (multiply(inverse(X0),multiply(multiply(inverse(inverse(X0)),X1),multiply(inverse(inverse(inverse(X1))),multiply(inverse(inverse(X1)),multiply(inverse(X1),inverse(inverse(X2)))))))=X2)),
% 151.05/19.48 inference(forward_demodulation,[status(thm)],[f6375,f7295])).
% 151.05/19.48 fof(f7297,plain,(
% 151.05/19.48 ![X0,X1,X2]: (multiply(inverse(X0),multiply(multiply(X0,X1),multiply(inverse(inverse(inverse(X1))),multiply(inverse(inverse(X1)),multiply(inverse(X1),inverse(inverse(X2)))))))=X2)),
% 151.05/19.48 inference(forward_demodulation,[status(thm)],[f5299,f7296])).
% 151.05/19.48 fof(f7298,plain,(
% 151.05/19.48 ![X0,X1,X2]: (multiply(inverse(X0),multiply(multiply(X0,X1),multiply(inverse(X1),inverse(inverse(X2)))))=X2)),
% 151.05/19.48 inference(forward_demodulation,[status(thm)],[f5528,f7297])).
% 151.05/19.48 fof(f7299,plain,(
% 151.05/19.48 ![X0,X1,X2]: (multiply(inverse(X0),multiply(multiply(X0,X1),multiply(inverse(X1),X2)))=X2)),
% 151.05/19.48 inference(forward_demodulation,[status(thm)],[f5299,f7298])).
% 151.05/19.48 fof(f8827,plain,(
% 151.05/19.48 ![X0,X1,X2]: (multiply(inverse(X0),multiply(multiply(X0,X1),X2))=multiply(X1,X2))),
% 151.05/19.48 inference(paramodulation,[status(thm)],[f5528,f7299])).
% 151.05/19.48 fof(f9401,plain,(
% 151.05/19.48 ![X0,X1,X2]: (multiply(inverse(inverse(X0)),multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 151.05/19.48 inference(paramodulation,[status(thm)],[f5528,f8827])).
% 151.05/19.48 fof(f9434,plain,(
% 151.05/19.48 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))),
% 151.05/19.48 inference(backward_demodulation,[status(thm)],[f9455,f4])).
% 151.05/19.48 fof(f9455,plain,(
% 151.05/19.48 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 151.05/19.48 inference(forward_demodulation,[status(thm)],[f5299,f9401])).
% 151.05/19.48 fof(f9482,plain,(
% 151.05/19.48 $false),
% 151.05/19.48 inference(trivial_equality_resolution,[status(thm)],[f9434])).
% 151.05/19.48 % SZS output end CNFRefutation for theBenchmark.p
% 9.72/19.73 % Elapsed time: 19.350264 seconds
% 9.72/19.73 % CPU time: 152.661351 seconds
% 9.72/19.73 % Total memory used: 874.426 MB
% 9.72/19.73 % Net memory used: 821.295 MB
%------------------------------------------------------------------------------