%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP014-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:35:26 PM UTC 2026
% Result : Unsatisfiable 91.77s 12.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP014-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n004.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 19:53:36 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 91.77/12.03 % Refutation found
% 91.77/12.03 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 91.77/12.03 % SZS output start CNFRefutation for theBenchmark
% 91.77/12.03 fof(f1,axiom,(
% 91.77/12.03 (![X,Y,W,Z]: (multiply(X,inverse(multiply(multiply(inverse(multiply(inverse(Y),multiply(inverse(X),W))),Z),inverse(multiply(Y,Z))))) = W ))),
% 91.77/12.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 91.77/12.03 fof(f2,negated_conjecture,(
% 91.77/12.03 multiply(a,multiply(b,c)) != multiply(multiply(a,b),c) ),
% 91.77/12.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 91.77/12.03 fof(f3,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),X3),inverse(multiply(X1,X3)))))=X2)),
% 91.77/12.03 inference(cnf_transformation,[status(thm)],[f1])).
% 91.77/12.03 fof(f4,plain,(
% 91.77/12.03 ~multiply(a,multiply(b,c))=multiply(multiply(a,b),c)),
% 91.77/12.03 inference(cnf_transformation,[status(thm)],[f2])).
% 91.77/12.03 fof(f10,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(inverse(multiply(inverse(X2),multiply(inverse(X0),X4)))),X1))),X5),inverse(multiply(X3,X5)))))))))=X4)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f3,f3])).
% 91.77/12.03 fof(f11,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3)))))=inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X2))),X5),inverse(multiply(X4,X5)))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f3,f3])).
% 91.77/12.03 fof(f12,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X1),X4))),X5),inverse(multiply(X3,X5))))),inverse(X4))))=X2)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f3,f3])).
% 91.77/12.03 fof(f14,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(multiply(inverse(multiply(inverse(X7),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(multiply(inverse(X2),multiply(inverse(X0),X8)))),X1)))),X3)))),X5))),X9),inverse(multiply(X7,X9)))))))))))))))))=X8)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f10,f10])).
% 91.77/12.03 fof(f15,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(X0,inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(inverse(inverse(multiply(inverse(X2),multiply(inverse(X0),X3))))),X4))),X5),inverse(multiply(X1,X5)))),inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(X6),X4)),X7),inverse(multiply(X6,X7)))))))))=X3)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f3,f10])).
% 91.77/12.03 fof(f24,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X1),X4))),X5),inverse(multiply(X3,X5))))),inverse(X4))))=inverse(multiply(multiply(inverse(multiply(inverse(X6),multiply(inverse(inverse(X0)),X2))),inverse(multiply(multiply(inverse(multiply(inverse(X7),multiply(inverse(X6),X8))),X9),inverse(multiply(X7,X9))))),inverse(X8))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f12,f12])).
% 91.77/12.03 fof(f43,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (X0=inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(inverse(X2)),multiply(inverse(X2),X0)))),X3),inverse(multiply(X1,X3)))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f3,f11])).
% 91.77/12.03 fof(f53,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (multiply(X0,inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(inverse(inverse(X2))),X3))),X4),inverse(multiply(X1,X4))))),X5),inverse(multiply(X2,X5)))))=inverse(multiply(multiply(inverse(multiply(inverse(X6),multiply(inverse(inverse(X0)),inverse(multiply(multiply(inverse(multiply(inverse(X7),X3)),X8),inverse(multiply(X7,X8))))))),X9),inverse(multiply(X6,X9)))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f11,f11])).
% 91.77/12.03 fof(f72,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))),inverse(multiply(multiply(inverse(multiply(inverse(X4),X5)),X6),inverse(multiply(X4,X6)))))=inverse(multiply(multiply(inverse(multiply(inverse(X7),multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X8),X2)),X9),inverse(multiply(X8,X9)))))),X5))),X10),inverse(multiply(X7,X10)))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f11,f11])).
% 91.77/12.03 fof(f98,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))))=X2)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f11,f3])).
% 91.77/12.03 fof(f116,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(inverse(X0),multiply(X0,inverse(inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X3)),X4)),X5)),inverse(multiply(X2,X4))))),X3))),X6),inverse(multiply(X1,X6)))))))=X5)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f11,f98])).
% 91.77/12.03 fof(f142,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(X2),X3)),X4),inverse(multiply(X2,X4)))))),X5),inverse(multiply(X1,X5)))))=inverse(multiply(multiply(inverse(X3),X6),inverse(multiply(inverse(inverse(X0)),X6)))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f98,f11])).
% 91.77/12.03 fof(f149,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X1),X4))),X5),inverse(multiply(X3,X5))))),inverse(X4))))=multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X6),X2)),X7),inverse(multiply(X6,X7))))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f98,f12])).
% 91.77/12.03 fof(f230,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6]: (X0=inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X2),multiply(inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(inverse(X4)),multiply(inverse(X4),X2)))),X5),inverse(multiply(X3,X5)))),X0)))),X6),inverse(multiply(X1,X6)))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f43,f43])).
% 91.77/12.03 fof(f233,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7]: (inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X0),X4))),X5),inverse(multiply(X3,X5))))),inverse(X4)))=inverse(multiply(multiply(inverse(multiply(inverse(X6),multiply(inverse(inverse(X1)),X2))),X7),inverse(multiply(X6,X7)))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f12,f43])).
% 91.77/12.03 fof(f253,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(inverse(X0),multiply(X0,X1))=multiply(inverse(inverse(X2)),multiply(inverse(X2),X1)))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f43,f98])).
% 91.77/12.03 fof(f282,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (X0=inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X2),multiply(X2,X0)))),X3),inverse(multiply(X1,X3)))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f43,f230])).
% 91.77/12.03 fof(f299,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(inverse(X0),multiply(X0,X1))=multiply(inverse(X2),multiply(X2,X1)))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f253,f253])).
% 91.77/12.03 fof(f350,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X3),inverse(multiply(inverse(X0),X3)))))=X2)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f253,f3])).
% 91.77/12.03 fof(f383,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,X2)))=multiply(inverse(X3),multiply(X3,multiply(X0,X2))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f299,f299])).
% 91.77/12.03 fof(f407,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X1,X2)),inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(X0),X4)),X2))))))=X4)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f299,f3])).
% 91.77/12.03 fof(f488,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X1,X2)),inverse(multiply(inverse(X0),multiply(multiply(inverse(X3),multiply(X3,X4)),X2))))))=X4)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f299,f350])).
% 91.77/12.03 fof(f1003,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(multiply(inverse(X2),multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(X3),X4)),X5),inverse(multiply(X3,X5)))))),inverse(X4))))=X1)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f98,f488])).
% 91.77/12.03 fof(f1079,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(X2,inverse(X2))))=X1)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f98,f1003])).
% 91.77/12.03 fof(f1094,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,X2))),inverse(multiply(X3,inverse(X3))))=multiply(X0,X2))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f383,f1079])).
% 91.77/12.03 fof(f1118,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X1,inverse(multiply(X2,inverse(X2))))),inverse(multiply(inverse(X0),X3)))))=X3)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1079,f407])).
% 91.77/12.03 fof(f1123,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X2),inverse(multiply(inverse(X0),multiply(multiply(inverse(X3),multiply(X3,X4)),inverse(multiply(X5,inverse(X5)))))))))=X4)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1079,f488])).
% 91.77/12.03 fof(f1141,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X2),inverse(multiply(inverse(X0),X3)))))=X3)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f1079,f1123])).
% 91.77/12.03 fof(f1460,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X2),inverse(X3))))=inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(X8,inverse(multiply(X9,inverse(multiply(multiply(inverse(multiply(inverse(X10),multiply(inverse(inverse(multiply(inverse(X9),multiply(inverse(inverse(multiply(inverse(X7),multiply(inverse(inverse(multiply(inverse(X5),multiply(inverse(inverse(X0)),X3)))),X4)))),X6)))),X8))),X11),inverse(multiply(X10,X11)))))))))))))))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f14,f1141])).
% 91.77/12.03 fof(f1488,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(X8,inverse(multiply(multiply(inverse(multiply(inverse(X9),multiply(inverse(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(X1),X10)))),X3)))),X5)))),X7))),X11),inverse(multiply(X9,X11))))))))))))))))),inverse(X10)))))=X2)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f14,f98])).
% 91.77/12.03 fof(f1490,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(X8,inverse(multiply(multiply(inverse(multiply(inverse(X9),multiply(inverse(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(X1),X10)))),X3)))),X5)))),X7))),X11),inverse(multiply(X9,X11))))))))))))))))),inverse(X10))))=inverse(multiply(multiply(inverse(multiply(inverse(X12),multiply(inverse(inverse(X0)),X2))),X13),inverse(multiply(X12,X13)))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f14,f11])).
% 91.77/12.03 fof(f1577,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12]: (multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))),inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(inverse(multiply(inverse(X5),multiply(multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X6),X2)),X7),inverse(multiply(X6,X7))))),X8))))),X9))),X10),inverse(multiply(X4,X10)))),inverse(multiply(X5,inverse(multiply(multiply(inverse(multiply(inverse(X11),X9)),X12),inverse(multiply(X11,X12)))))))))=X8)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f11,f15])).
% 91.77/12.03 fof(f1743,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,inverse(inverse(multiply(X1,inverse(X1)))))=inverse(inverse(X0)))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1079,f1118])).
% 91.77/12.03 fof(f1824,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(inverse(X0),multiply(multiply(inverse(inverse(X0)),X1),inverse(multiply(X2,inverse(X2)))))=X1)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1118,f98])).
% 91.77/12.03 fof(f1868,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,inverse(inverse(inverse(inverse(inverse(multiply(X1,inverse(X1))))))))=inverse(inverse(X0)))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1743,f1743])).
% 91.77/12.03 fof(f1869,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X2),X3)),X4),inverse(multiply(X2,X4))))),X3))),X5),inverse(multiply(X1,X5)))))))=inverse(inverse(X0)))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f11,f1743])).
% 91.77/12.03 fof(f1890,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(inverse(inverse(inverse(multiply(inverse(X1),multiply(X1,X2))))),inverse(multiply(inverse(X0),inverse(inverse(multiply(X3,inverse(X3)))))))))=X2)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1743,f350])).
% 91.77/12.03 fof(f1911,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(inverse(inverse(inverse(multiply(X2,inverse(X2)))))))=X1)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1743,f1079])).
% 91.77/12.03 fof(f1917,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(multiply(inverse(X0),inverse(inverse(X0))),inverse(multiply(X1,inverse(X1))))=inverse(inverse(multiply(X2,inverse(X2)))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1743,f1079])).
% 91.77/12.03 fof(f1946,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(inverse(inverse(multiply(inverse(X1),multiply(X1,X2))))),inverse(inverse(inverse(inverse(X0)))))))=X2)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f1743,f1890])).
% 91.77/12.03 fof(f1975,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,inverse(inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(X1,inverse(X1)))))))))))=inverse(inverse(X0)))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1743,f1868])).
% 91.77/12.03 fof(f2084,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(inverse(inverse(inverse(multiply(X1,inverse(X1)))))))=inverse(multiply(multiply(inverse(multiply(inverse(X2),X0)),X3),inverse(multiply(X2,X3)))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f98,f1911])).
% 91.77/12.03 fof(f2095,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(multiply(inverse(inverse(X0)),X1),inverse(inverse(inverse(inverse(multiply(X2,inverse(X2)))))))=multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X3),X1)),X4),inverse(multiply(X3,X4))))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f98,f1911])).
% 91.77/12.03 fof(f2102,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(multiply(inverse(X0),X1),inverse(inverse(inverse(inverse(multiply(X2,inverse(X2)))))))=inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(X3,X4))),X4),inverse(multiply(inverse(X0),X1)))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1141,f1911])).
% 91.77/12.03 fof(f2110,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (multiply(multiply(inverse(X0),X1),inverse(inverse(inverse(inverse(multiply(X2,inverse(X2)))))))=inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(X8,inverse(multiply(multiply(inverse(multiply(inverse(X9),multiply(inverse(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(X0),X1)))),X3)))),X5)))),X7))),X10),inverse(multiply(X9,X10)))))))))))))))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f14,f1911])).
% 91.77/12.03 fof(f2128,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(inverse(inverse(multiply(inverse(X0),multiply(X0,X1)))),multiply(inverse(X2),multiply(X2,inverse(inverse(inverse(inverse(multiply(X3,inverse(X3)))))))))=multiply(inverse(X4),multiply(X4,X1)))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1911,f383])).
% 91.77/12.03 fof(f2146,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,multiply(multiply(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X2),multiply(X2,X0)))),X3),inverse(multiply(X1,X3))))),X4),inverse(multiply(X5,inverse(X5)))))=X4)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f282,f1824])).
% 91.77/12.03 fof(f2246,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,multiply(multiply(inverse(X0),X1),inverse(multiply(X2,inverse(X2)))))=X1)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f282,f2146])).
% 91.77/12.03 fof(f2280,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (multiply(X0,multiply(X1,inverse(multiply(X2,inverse(X2)))))=inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(X8,inverse(multiply(multiply(inverse(multiply(inverse(X9),multiply(inverse(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X1)))),X3)))),X5)))),X7))),X10),inverse(multiply(X9,X10)))))))))))))))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f14,f2246])).
% 91.77/12.03 fof(f2329,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(multiply(inverse(X0),X1),inverse(inverse(inverse(inverse(multiply(X2,inverse(X2)))))))=multiply(multiply(inverse(X0),X1),inverse(multiply(X3,inverse(X3)))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f2246,f1911])).
% 91.77/12.03 fof(f2532,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(X1,inverse(X1))))))))))=inverse(inverse(X0)))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1917,f1868])).
% 91.77/12.03 fof(f2533,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,inverse(inverse(inverse(inverse(multiply(X1,inverse(X1)))))))=inverse(inverse(X0)))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1917,f1743])).
% 91.77/12.03 fof(f2542,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(multiply(inverse(inverse(X0)),multiply(inverse(multiply(inverse(X1),inverse(inverse(X1)))),inverse(inverse(multiply(X2,inverse(X2)))))),inverse(multiply(X3,inverse(X3))))=multiply(X0,inverse(multiply(X4,inverse(X4)))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1917,f1094])).
% 91.77/12.03 fof(f2548,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(inverse(inverse(X0)),multiply(inverse(multiply(inverse(X1),inverse(inverse(X1)))),inverse(inverse(multiply(X2,inverse(X2))))))=multiply(inverse(X3),multiply(X3,multiply(X0,inverse(multiply(X4,inverse(X4)))))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1917,f383])).
% 91.77/12.03 fof(f2564,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,multiply(multiply(inverse(X1),inverse(inverse(X1))),inverse(multiply(X2,inverse(X2)))))=inverse(inverse(X0)))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1917,f1743])).
% 91.77/12.03 fof(f2569,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(multiply(inverse(X0),X1),inverse(multiply(inverse(multiply(X2,inverse(X2))),multiply(multiply(inverse(X3),inverse(inverse(X3))),inverse(multiply(X4,inverse(X4))))))))=X1)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1917,f2246])).
% 91.77/12.03 fof(f2571,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(inverse(inverse(inverse(multiply(inverse(multiply(X2,inverse(X2))),multiply(multiply(inverse(X3),inverse(inverse(X3))),inverse(multiply(X4,inverse(X4))))))))))=X1)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1917,f1911])).
% 91.77/12.03 fof(f2609,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(X0,X1))=multiply(multiply(multiply(inverse(X2),inverse(inverse(X2))),inverse(multiply(X3,inverse(X3)))),multiply(inverse(multiply(X4,inverse(X4))),X1)))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f1917,f299])).
% 91.77/12.03 fof(f2655,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (inverse(inverse(multiply(inverse(inverse(X0)),X1)))=multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X2),X1)),X3),inverse(multiply(X2,X3))))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2533,f2095])).
% 91.77/12.03 fof(f2662,plain,(
% 91.77/12.03 ![X0,X1,X2]: (inverse(inverse(multiply(inverse(X0),X1)))=multiply(multiply(inverse(X0),X1),inverse(multiply(X2,inverse(X2)))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2533,f2329])).
% 91.77/12.03 fof(f2664,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (inverse(inverse(multiply(inverse(X0),X1)))=inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(multiply(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X7),multiply(inverse(inverse(multiply(inverse(X5),multiply(inverse(inverse(multiply(inverse(X3),multiply(inverse(X0),X1)))),X2)))),X4)))),X6))),X9),inverse(multiply(X8,X9)))))))))))))))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2533,f2110])).
% 91.77/12.03 fof(f2671,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (inverse(inverse(multiply(inverse(X0),X1)))=inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(X2,X3))),X3),inverse(multiply(inverse(X0),X1)))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2533,f2102])).
% 91.77/12.03 fof(f2677,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(inverse(inverse(multiply(inverse(X0),multiply(X0,X1)))),multiply(inverse(X2),inverse(inverse(X2))))=multiply(inverse(X3),multiply(X3,X1)))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2533,f2128])).
% 91.77/12.03 fof(f2679,plain,(
% 91.77/12.03 ![X0,X1,X2]: (inverse(inverse(X0))=inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2533,f2084])).
% 91.77/12.03 fof(f2684,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(multiply(inverse(inverse(X0)),inverse(inverse(inverse(multiply(inverse(X1),inverse(inverse(X1))))))),inverse(multiply(X2,inverse(X2))))=multiply(X0,inverse(multiply(X3,inverse(X3)))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f1743,f2542])).
% 91.77/12.03 fof(f2693,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(inverse(inverse(X0)),inverse(inverse(inverse(multiply(inverse(X1),inverse(inverse(X1)))))))=multiply(inverse(X2),multiply(X2,multiply(X0,inverse(multiply(X3,inverse(X3)))))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f1743,f2548])).
% 91.77/12.03 fof(f2703,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,multiply(multiply(inverse(X0),X1),inverse(inverse(inverse(inverse(multiply(X2,inverse(X2))))))))=X1)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2564,f2569])).
% 91.77/12.03 fof(f2705,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,inverse(inverse(multiply(inverse(X0),X1))))=X1)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2533,f2703])).
% 91.77/12.03 fof(f2706,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(inverse(inverse(inverse(inverse(inverse(inverse(multiply(X2,inverse(X2))))))))))=X1)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2564,f2571])).
% 91.77/12.03 fof(f2725,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(inverse(inverse(X0)))))))=X1)),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2740,f1946])).
% 91.77/12.03 fof(f2740,plain,(
% 91.77/12.03 ![X0,X1]: (inverse(inverse(multiply(inverse(X0),multiply(X0,X1))))=X1)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2532,f2706])).
% 91.77/12.03 fof(f2770,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(X0,inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(inverse(inverse(X2))),X3))),X4),inverse(multiply(X1,X4))))),X5),inverse(multiply(X2,X5)))))=inverse(multiply(multiply(inverse(multiply(inverse(X6),inverse(inverse(multiply(inverse(inverse(inverse(inverse(X0)))),X3))))),X7),inverse(multiply(X6,X7)))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2655,f53])).
% 91.77/12.03 fof(f2794,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5]: (inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))))),multiply(inverse(X0),X3)))),inverse(X3)))=inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X1)),X2))),X5),inverse(multiply(X4,X5)))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2655,f233])).
% 91.77/12.03 fof(f2801,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X1),X4))),X5),inverse(multiply(X3,X5))))),inverse(X4))))=inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(X0)),X2))))),multiply(inverse(X6),X7)))),inverse(X7))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2655,f24])).
% 91.77/12.03 fof(f2831,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X1),X2)))),multiply(inverse(X1),X3)))),inverse(X3))))=multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X4),X2)),X5),inverse(multiply(X4,X5))))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2655,f149])).
% 91.77/12.03 fof(f2865,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(inverse(inverse(inverse(multiply(inverse(inverse(inverse(X1))),X2)))),X3),inverse(multiply(X1,X3)))))=inverse(multiply(multiply(inverse(X2),X4),inverse(multiply(inverse(inverse(X0)),X4)))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2655,f142])).
% 91.77/12.03 fof(f2872,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (inverse(inverse(multiply(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))))),X4)))=inverse(multiply(multiply(inverse(multiply(inverse(X5),multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X6),X2)),X7),inverse(multiply(X6,X7)))))),X4))),X8),inverse(multiply(X5,X8)))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2655,f72])).
% 91.77/12.03 fof(f3005,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(X0,multiply(X1,inverse(multiply(X2,inverse(X2)))))=inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(inverse(inverse(multiply(inverse(inverse(X8)),multiply(inverse(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X1)))),X3)))),X5)))),X7))))))))))))))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2655,f2280])).
% 91.77/12.03 fof(f3016,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X2),inverse(X3))))=inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(X8,inverse(inverse(inverse(multiply(inverse(inverse(X9)),multiply(inverse(inverse(multiply(inverse(X9),multiply(inverse(inverse(multiply(inverse(X7),multiply(inverse(inverse(multiply(inverse(X5),multiply(inverse(inverse(X0)),X3)))),X4)))),X6)))),X8))))))))))))))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2655,f1460])).
% 91.77/12.03 fof(f3023,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(inverse(inverse(multiply(inverse(inverse(X8)),multiply(inverse(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(X1),X9)))),X3)))),X5)))),X7)))))))))))))))),inverse(X9))))=inverse(multiply(multiply(inverse(multiply(inverse(X10),multiply(inverse(inverse(X0)),X2))),X11),inverse(multiply(X10,X11)))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2655,f1490])).
% 91.77/12.03 fof(f3025,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(inverse(inverse(multiply(inverse(inverse(X8)),multiply(inverse(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(X1),X9)))),X3)))),X5)))),X7)))))))))))))))),inverse(X9)))))=X2)),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2655,f1488])).
% 91.77/12.03 fof(f3291,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))),inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(inverse(multiply(inverse(X5),multiply(multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X6),X2)),X7),inverse(multiply(X6,X7))))),X8))))),X9))),X10),inverse(multiply(X4,X10)))),inverse(inverse(inverse(multiply(inverse(inverse(X5)),X9)))))))=X8)),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2655,f1577])).
% 91.77/12.03 fof(f3435,plain,(
% 91.77/12.03 ![X0,X1,X2]: (inverse(inverse(multiply(inverse(inverse(X0)),inverse(inverse(inverse(multiply(inverse(X1),inverse(inverse(X1)))))))))=multiply(X0,inverse(multiply(X2,inverse(X2)))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2662,f2684])).
% 91.77/12.03 fof(f3468,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(X0,X1))=multiply(inverse(inverse(multiply(inverse(X2),inverse(inverse(X2))))),multiply(inverse(multiply(X3,inverse(X3))),X1)))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2662,f2609])).
% 91.77/12.03 fof(f3530,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7]: (inverse(inverse(multiply(inverse(X0),X1)))=inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(inverse(inverse(multiply(inverse(inverse(X7)),multiply(inverse(inverse(multiply(inverse(X7),multiply(inverse(inverse(multiply(inverse(X5),multiply(inverse(inverse(multiply(inverse(X3),multiply(inverse(X0),X1)))),X2)))),X4)))),X6))))))))))))))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2655,f2664])).
% 91.77/12.03 fof(f3725,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,multiply(inverse(X1),inverse(inverse(X1))))=multiply(inverse(X2),multiply(X2,X0)))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2740,f2677])).
% 91.77/12.03 fof(f3766,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(inverse(inverse(inverse(multiply(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))),X2))))))=inverse(inverse(X0)))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2679,f1869])).
% 91.77/12.03 fof(f3778,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(X0,inverse(inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X2)),X3)),X4)),inverse(multiply(X1,X3))))),X2))))))=X4)),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f2679,f116])).
% 91.77/12.03 fof(f3870,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(multiply(inverse(inverse(inverse(multiply(inverse(inverse(inverse(X1))),X2)))),X3),inverse(multiply(X1,X3)))))=inverse(multiply(multiply(inverse(multiply(inverse(X4),inverse(inverse(multiply(inverse(inverse(inverse(inverse(X0)))),X2))))),X5),inverse(multiply(X4,X5)))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2679,f2770])).
% 91.77/12.03 fof(f3872,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(inverse(inverse(multiply(inverse(inverse(inverse(X1))),X2)))),X3),inverse(multiply(X1,X3)))))=inverse(inverse(inverse(inverse(multiply(inverse(inverse(inverse(inverse(X0)))),X2))))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2679,f3870])).
% 91.77/12.03 fof(f3908,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))))),multiply(inverse(X0),X3)))),inverse(X3)))=inverse(inverse(multiply(inverse(inverse(X1)),X2))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2679,f2794])).
% 91.77/12.03 fof(f3933,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X1),X2)))),multiply(inverse(X1),X3)))),inverse(X3))))=inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X2))))),multiply(inverse(X4),X5)))),inverse(X5))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2655,f2801])).
% 91.77/12.03 fof(f3935,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X1),X2)))),multiply(inverse(X1),X3)))),inverse(X3))))=inverse(inverse(multiply(inverse(inverse(X0)),X2))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f3908,f3933])).
% 91.77/12.03 fof(f3989,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (inverse(inverse(multiply(inverse(inverse(X0)),X1)))=multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X2),X1)),X3),inverse(multiply(X2,X3))))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f3935,f2831])).
% 91.77/12.03 fof(f4023,plain,(
% 91.77/12.03 ![X0,X1]: (inverse(inverse(multiply(inverse(inverse(X0)),X1)))=multiply(X0,inverse(inverse(X1))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2679,f3989])).
% 91.77/12.03 fof(f4172,plain,(
% 91.77/12.03 ![X0,X1,X2]: (inverse(inverse(inverse(inverse(multiply(inverse(inverse(inverse(inverse(X0)))),X1)))))=inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(inverse(inverse(X0)),X2)))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f3872,f2865])).
% 91.77/12.03 fof(f4173,plain,(
% 91.77/12.03 ![X0,X1,X2]: (inverse(inverse(multiply(inverse(inverse(X0)),inverse(inverse(X1)))))=inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(inverse(inverse(X0)),X2)))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4023,f4172])).
% 91.77/12.03 fof(f4179,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,inverse(inverse(inverse(inverse(X1)))))=inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(inverse(inverse(X0)),X2)))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4023,f4173])).
% 91.77/12.03 fof(f4206,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))),inverse(inverse(X4)))=inverse(multiply(multiply(inverse(multiply(inverse(X5),multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X6),X2)),X7),inverse(multiply(X6,X7)))))),X4))),X8),inverse(multiply(X5,X8)))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4023,f2872])).
% 91.77/12.03 fof(f4207,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))),inverse(inverse(X4)))=inverse(inverse(multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X5),X2)),X6),inverse(multiply(X5,X6)))))),X4))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2679,f4206])).
% 91.77/12.03 fof(f4208,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))),inverse(inverse(X4)))=inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(inverse(X1)),X2)))),X4))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2655,f4207])).
% 91.77/12.03 fof(f4211,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))),inverse(inverse(X4)))=multiply(inverse(multiply(inverse(inverse(X1)),X2)),inverse(inverse(X4))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4023,f4208])).
% 91.77/12.03 fof(f4650,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,multiply(X1,inverse(multiply(X2,inverse(X2)))))=inverse(inverse(multiply(inverse(inverse(X0)),X1))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f3530,f3005])).
% 91.77/12.03 fof(f4675,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(inverse(inverse(X0)),inverse(inverse(inverse(multiply(inverse(X1),inverse(inverse(X1)))))))=multiply(inverse(X2),multiply(X2,inverse(inverse(X0)))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f4678,f2693])).
% 91.77/12.03 fof(f4678,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,multiply(X1,inverse(multiply(X2,inverse(X2)))))=multiply(X0,inverse(inverse(X1))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4023,f4650])).
% 91.77/12.03 fof(f4749,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X2),inverse(X3))))=inverse(inverse(multiply(inverse(inverse(X0)),X3))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f3530,f3016])).
% 91.77/12.03 fof(f4757,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X2),inverse(X3))))=multiply(X0,inverse(inverse(X3))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4023,f4749])).
% 91.77/12.03 fof(f4774,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(inverse(multiply(inverse(X1),X3)))),inverse(X3))))=inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X2))),X5),inverse(multiply(X4,X5)))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f3530,f3023])).
% 91.77/12.03 fof(f4775,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(inverse(multiply(inverse(X1),X3)))),inverse(X3))))=inverse(inverse(multiply(inverse(inverse(X0)),X2))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2679,f4774])).
% 91.77/12.03 fof(f4778,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(inverse(multiply(inverse(X1),X3)))),inverse(X3))))=multiply(X0,inverse(inverse(X2))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4023,f4775])).
% 91.77/12.03 fof(f4783,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(inverse(multiply(inverse(X1),X3)))),inverse(X3)))))=X2)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f3530,f3025])).
% 91.77/12.03 fof(f4786,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(inverse(X0),multiply(X0,inverse(inverse(X1))))=X1)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4778,f4783])).
% 91.77/12.03 fof(f5651,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X4),multiply(multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X5),X2)),X6),inverse(multiply(X5,X6))))),X7))))),X8))),inverse(inverse(inverse(multiply(inverse(inverse(X4)),X8)))))))=X7)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2679,f3291])).
% 91.77/12.03 fof(f5652,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))),inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X5),X2)),X6),inverse(multiply(X5,X6))))),X7))),inverse(inverse(X8))),inverse(inverse(inverse(multiply(inverse(inverse(X4)),X8)))))))=X7)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4023,f5651])).
% 91.77/12.03 fof(f5653,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))),inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(multiply(inverse(inverse(X1)),X2))),X5))),inverse(inverse(X6))),inverse(inverse(inverse(multiply(inverse(inverse(X4)),X6)))))))=X5)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2655,f5652])).
% 91.77/12.03 fof(f5654,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))),inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(multiply(X1,inverse(inverse(X2))),X5))),inverse(inverse(X6))),inverse(inverse(inverse(multiply(inverse(inverse(X4)),X6)))))))=X5)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4023,f5653])).
% 91.77/12.03 fof(f5655,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))),inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(multiply(X1,inverse(inverse(X2))),X5))),inverse(inverse(X6))),inverse(multiply(X4,inverse(inverse(X6)))))))=X5)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4023,f5654])).
% 91.77/12.03 fof(f5656,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (inverse(inverse(multiply(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))))),multiply(multiply(X1,inverse(inverse(X2))),X4))))=X4)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2655,f5655])).
% 91.77/12.03 fof(f5657,plain,(
% 91.77/12.03 ![X0,X1,X2,X3,X4]: (multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3))),inverse(inverse(multiply(multiply(X1,inverse(inverse(X2))),X4))))=X4)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4023,f5656])).
% 91.77/12.03 fof(f5658,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(inverse(X0)),X1)),inverse(inverse(multiply(multiply(X0,inverse(inverse(X1))),X2))))=X2)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4211,f5657])).
% 91.77/12.03 fof(f6061,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,inverse(inverse(inverse(inverse(inverse(multiply(inverse(X1),inverse(inverse(X1)))))))))=multiply(X0,inverse(multiply(X2,inverse(X2)))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4023,f3435])).
% 91.77/12.03 fof(f6086,plain,(
% 91.77/12.03 ![X0,X1]: (inverse(inverse(X0))=multiply(X0,inverse(multiply(X1,inverse(X1)))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f1868,f6061])).
% 91.77/12.03 fof(f6527,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,inverse(inverse(multiply(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))),inverse(inverse(X2))))))=inverse(inverse(X0)))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4023,f3766])).
% 91.77/12.03 fof(f6551,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),X3)),inverse(multiply(X0,X2))))),X1))=X3)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4786,f3778])).
% 91.77/12.03 fof(f6757,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(inverse(inverse(X0)),inverse(inverse(inverse(multiply(inverse(X1),inverse(inverse(X1)))))))=X0)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f4786,f4675])).
% 91.77/12.03 fof(f6935,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(inverse(inverse(X0)),X1)=multiply(inverse(X2),multiply(X2,multiply(X0,inverse(inverse(X1))))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f4786,f383])).
% 91.77/12.03 fof(f6946,plain,(
% 91.77/12.03 ![X0,X1]: (inverse(inverse(X0))=multiply(X0,inverse(inverse(inverse(multiply(X1,inverse(X1)))))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f6086,f6086])).
% 91.77/12.03 fof(f6962,plain,(
% 91.77/12.03 ![X0]: (inverse(inverse(inverse(inverse(X0))))=X0)),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f6946,f6757])).
% 91.77/12.03 fof(f6974,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,inverse(inverse(inverse(inverse(multiply(X1,inverse(X1)))))))=inverse(inverse(X0)))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f6962,f1975])).
% 91.77/12.03 fof(f7021,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,X1)=inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(inverse(inverse(X0)),X2)))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f6962,f4179])).
% 91.77/12.03 fof(f7022,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),X0)))=X1)),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f6962,f2725])).
% 91.77/12.03 fof(f7027,plain,(
% 91.77/12.03 ![X0,X1]: (inverse(inverse(X0))=multiply(inverse(X1),multiply(X1,X0)))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7028,f3725])).
% 91.77/12.03 fof(f7028,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,multiply(X1,inverse(X1)))=inverse(inverse(X0)))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f6962,f6974])).
% 91.77/12.03 fof(f7108,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=inverse(inverse(multiply(X0,inverse(inverse(X1))))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7027,f6935])).
% 91.77/12.03 fof(f7179,plain,(
% 91.77/12.03 ![X0,X1,X2]: (inverse(inverse(X0))=multiply(inverse(inverse(multiply(inverse(X1),inverse(inverse(X1))))),multiply(inverse(multiply(X2,inverse(X2))),X0)))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7027,f3468])).
% 91.77/12.03 fof(f7193,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(inverse(inverse(inverse(X1))),X1),inverse(X2))))=multiply(X0,inverse(inverse(X2))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7027,f4757])).
% 91.77/12.03 fof(f7208,plain,(
% 91.77/12.03 ![X0,X1,X2]: (inverse(inverse(multiply(inverse(X0),X1)))=inverse(multiply(multiply(inverse(inverse(inverse(X2))),X2),inverse(multiply(inverse(X0),X1)))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7027,f2671])).
% 91.77/12.03 fof(f7300,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (multiply(X0,multiply(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))),X2))=inverse(inverse(X0)))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7108,f6527])).
% 91.77/12.03 fof(f7442,plain,(
% 91.77/12.03 ![X0,X1,X2]: (inverse(inverse(X0))=multiply(multiply(inverse(inverse(inverse(X1))),X1),multiply(inverse(multiply(X2,inverse(X2))),X0)))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f7108,f7179])).
% 91.77/12.03 fof(f7554,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,multiply(inverse(inverse(inverse(X1))),X1))=inverse(inverse(X0)))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f2679,f7300])).
% 91.77/12.03 fof(f7598,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(inverse(multiply(X0,inverse(X0))),inverse(inverse(inverse(inverse(X1)))))=X1)),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f6086,f7022])).
% 91.77/12.03 fof(f7602,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,inverse(inverse(X1)))=inverse(multiply(inverse(X1),inverse(X0))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f7022,f2705])).
% 91.77/12.03 fof(f7624,plain,(
% 91.77/12.03 ![X0,X1]: (inverse(inverse(X0))=multiply(multiply(inverse(inverse(inverse(X1))),X1),X0))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7626,f7442])).
% 91.77/12.03 fof(f7626,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(inverse(multiply(X0,inverse(X0))),X1)=X1)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f6962,f7598])).
% 91.77/12.03 fof(f7651,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (inverse(multiply(inverse(multiply(multiply(X0,X1),inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X2)),X1)),X3))))),X2))=X3)),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7602,f6551])).
% 91.77/12.03 fof(f7673,plain,(
% 91.77/12.03 ![X0,X1]: (inverse(inverse(multiply(inverse(X0),X1)))=inverse(inverse(inverse(inverse(multiply(inverse(X0),X1))))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7624,f7208])).
% 91.77/12.03 fof(f7674,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,inverse(inverse(inverse(inverse(X1)))))=multiply(X0,inverse(inverse(X1))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7624,f7193])).
% 91.77/12.03 fof(f7692,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=multiply(X0,inverse(inverse(X1))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7727,f4023])).
% 91.77/12.03 fof(f7696,plain,(
% 91.77/12.03 ![X0,X1,X2,X3]: (inverse(multiply(inverse(multiply(multiply(X0,X1),multiply(inverse(multiply(inverse(multiply(inverse(X0),X2)),X1)),X3))),X2))=X3)),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7727,f7651])).
% 91.77/12.03 fof(f7727,plain,(
% 91.77/12.03 ![X0,X1]: (inverse(inverse(multiply(inverse(X0),X1)))=multiply(inverse(X0),X1))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f6962,f7673])).
% 91.77/12.03 fof(f7733,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(inverse(X0)),X1)),multiply(multiply(X0,inverse(inverse(X1))),X2))=X2)),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7784,f5658])).
% 91.77/12.03 fof(f7770,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,X1)=inverse(multiply(inverse(X1),inverse(X0))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7784,f7602])).
% 91.77/12.03 fof(f7784,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,X1)=multiply(X0,inverse(inverse(X1))))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f6962,f7674])).
% 91.77/12.03 fof(f7806,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,multiply(inverse(X1),X1))=inverse(inverse(X0)))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7813,f7554])).
% 91.77/12.03 fof(f7811,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,X1)=inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(X0,X2)))))),
% 91.77/12.03 inference(backward_demodulation,[status(thm)],[f7813,f7021])).
% 91.77/12.03 fof(f7813,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=multiply(X0,X1))),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f7784,f7692])).
% 91.77/12.03 fof(f7885,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(inverse(multiply(X0,X1)),multiply(multiply(X0,inverse(inverse(X1))),X2))=X2)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f7813,f7733])).
% 91.77/12.03 fof(f7886,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(inverse(multiply(X0,X1)),multiply(multiply(X0,X1),X2))=X2)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f7784,f7885])).
% 91.77/12.03 fof(f7896,plain,(
% 91.77/12.03 ![X0]: (inverse(inverse(X0))=X0)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f7027,f7886])).
% 91.77/12.03 fof(f7989,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(X0,multiply(inverse(X1),X1))=X0)),
% 91.77/12.03 inference(forward_demodulation,[status(thm)],[f7896,f7806])).
% 91.77/12.03 fof(f8341,plain,(
% 91.77/12.03 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,X1)),X2))=multiply(inverse(multiply(inverse(X0),X2)),X1))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f7989,f7696])).
% 91.77/12.03 fof(f8735,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,multiply(inverse(X1),inverse(X2)))=inverse(multiply(multiply(X2,X1),inverse(X0))))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f7770,f7770])).
% 91.77/12.03 fof(f8738,plain,(
% 91.77/12.03 ![X0,X1]: (multiply(inverse(X0),X1)=inverse(multiply(inverse(X1),X0)))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f7896,f7770])).
% 91.77/12.03 fof(f8757,plain,(
% 91.77/12.03 ![X0,X1]: (inverse(multiply(X0,X1))=multiply(inverse(X1),inverse(X0)))),
% 91.77/12.03 inference(paramodulation,[status(thm)],[f7770,f7896])).
% 91.77/12.03 fof(f8763,plain,(
% 91.77/12.03 ![X0,X1,X2]: (multiply(X0,X1)=multiply(multiply(X0,X2),multiply(inverse(X2),inverse(inverse(X1)))))),
% 91.77/12.04 inference(backward_demodulation,[status(thm)],[f8735,f7811])).
% 91.77/12.04 fof(f8793,plain,(
% 91.77/12.04 ![X0,X1,X2]: (multiply(inverse(X0),multiply(X1,X2))=multiply(inverse(multiply(inverse(X1),X0)),X2))),
% 91.77/12.04 inference(backward_demodulation,[status(thm)],[f8738,f8341])).
% 91.77/12.04 fof(f8836,plain,(
% 91.77/12.04 ![X0,X1,X2]: (multiply(X0,X1)=multiply(multiply(X0,X2),inverse(multiply(inverse(X1),X2))))),
% 91.77/12.04 inference(forward_demodulation,[status(thm)],[f8757,f8763])).
% 91.77/12.04 fof(f8838,plain,(
% 91.77/12.04 ![X0,X1,X2]: (multiply(X0,X1)=multiply(multiply(X0,X2),multiply(inverse(X2),X1)))),
% 91.77/12.04 inference(forward_demodulation,[status(thm)],[f8738,f8836])).
% 91.77/12.04 fof(f8916,plain,(
% 91.77/12.04 ![X0,X1,X2]: (multiply(inverse(X0),multiply(X1,X2))=multiply(multiply(inverse(X0),X1),X2))),
% 91.77/12.04 inference(forward_demodulation,[status(thm)],[f8738,f8793])).
% 91.77/12.04 fof(f9399,plain,(
% 91.77/12.04 ![X0,X1,X2,X3]: (multiply(multiply(X0,X1),X2)=multiply(multiply(X0,X3),multiply(inverse(multiply(inverse(X1),X3)),X2)))),
% 91.77/12.04 inference(paramodulation,[status(thm)],[f8838,f8838])).
% 91.77/12.04 fof(f9440,plain,(
% 91.77/12.04 ![X0,X1,X2,X3]: (multiply(multiply(X0,X1),X2)=multiply(multiply(X0,X3),multiply(multiply(inverse(X3),X1),X2)))),
% 91.77/12.04 inference(forward_demodulation,[status(thm)],[f8738,f9399])).
% 91.77/12.04 fof(f9441,plain,(
% 91.77/12.04 ![X0,X1,X2,X3]: (multiply(multiply(X0,X1),X2)=multiply(multiply(X0,X3),multiply(inverse(X3),multiply(X1,X2))))),
% 91.77/12.04 inference(forward_demodulation,[status(thm)],[f8916,f9440])).
% 91.77/12.04 fof(f9442,plain,(
% 91.77/12.04 ~multiply(a,multiply(b,c))=multiply(a,multiply(b,c))),
% 91.77/12.04 inference(backward_demodulation,[status(thm)],[f9453,f4])).
% 91.77/12.04 fof(f9453,plain,(
% 91.77/12.04 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 91.77/12.04 inference(forward_demodulation,[status(thm)],[f8838,f9441])).
% 91.77/12.04 fof(f9496,plain,(
% 91.77/12.04 $false),
% 91.77/12.04 inference(trivial_equality_resolution,[status(thm)],[f9442])).
% 91.77/12.04 % SZS output end CNFRefutation for theBenchmark.p
% 47.84/13.43 % Elapsed time: 12.849996 seconds
% 47.84/13.43 % CPU time: 56.285610 seconds
% 47.84/13.43 % Total memory used: 3.285 GB
% 47.84/13.43 % Net memory used: 3.254 GB
%------------------------------------------------------------------------------