%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP432-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 : n020.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 18.35s 2.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP432-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n020.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 20:13:47 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 18.35/2.80 % Refutation found
% 18.35/2.80 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 18.35/2.80 % SZS output start CNFRefutation for theBenchmark
% 18.35/2.80 fof(f1,axiom,(
% 18.35/2.80 (![A,B,C,D]: (multiply(A,inverse(multiply(B,multiply(multiply(multiply(C,inverse(C)),inverse(multiply(D,B))),A)))) = D ))),
% 18.35/2.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.35/2.80 fof(f2,negated_conjecture,(
% 18.35/2.80 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 18.35/2.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.35/2.80 fof(f3,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))),X0))))=X3)),
% 18.35/2.80 inference(cnf_transformation,[status(thm)],[f1])).
% 18.35/2.80 fof(f4,plain,(
% 18.35/2.80 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 18.35/2.80 inference(cnf_transformation,[status(thm)],[f2])).
% 18.35/2.80 fof(f10,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,X5)))))),inverse(multiply(X5,X2)))=X4)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f3,f3])).
% 18.35/2.80 fof(f11,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))),multiply(X4,inverse(X4))),multiply(X2,X0))))=X3)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f3,f3])).
% 18.35/2.80 fof(f12,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))),X4))),multiply(multiply(multiply(X5,inverse(X5)),inverse(X3)),X0))))=X4)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f3,f3])).
% 18.35/2.80 fof(f13,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,X1))),multiply(X5,inverse(X5))),X0))))=multiply(X4,multiply(X6,inverse(X6))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f11,f11])).
% 18.35/2.80 fof(f14,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(X3,X0))))=multiply(multiply(multiply(X4,inverse(X4)),inverse(multiply(X1,X3))),multiply(X5,inverse(X5))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f3,f11])).
% 18.35/2.80 fof(f44,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X4))),multiply(X5,inverse(X5))))),multiply(X6,inverse(X6))),multiply(X7,X0))))=inverse(multiply(multiply(X3,multiply(X8,inverse(X8))),multiply(X4,X7))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f14,f11])).
% 18.35/2.80 fof(f46,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(X1,inverse(multiply(multiply(X2,multiply(X3,inverse(X3))),multiply(X4,X1)))),multiply(X2,X0))))=X4)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f14,f11])).
% 18.35/2.80 fof(f47,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,multiply(X2,inverse(multiply(multiply(X3,multiply(X4,inverse(X4))),multiply(X1,X2)))))))=X3)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f14,f3])).
% 18.35/2.80 fof(f110,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,X2)))=multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,X2))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f11,f47])).
% 18.35/2.80 fof(f146,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(multiply(X0,inverse(X0)),inverse(X1))=multiply(multiply(X2,inverse(X2)),inverse(multiply(inverse(multiply(X3,multiply(multiply(multiply(X4,inverse(X4)),inverse(multiply(X5,X3))),multiply(multiply(X6,inverse(X6)),inverse(multiply(X1,X7)))))),inverse(multiply(X7,X5))))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f10,f110])).
% 18.35/2.80 fof(f193,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,inverse(X3))))),multiply(X4,X0))))=multiply(multiply(multiply(X5,inverse(X5)),inverse(multiply(X1,X4))),multiply(X6,inverse(X6))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f110,f14])).
% 18.35/2.80 fof(f199,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(X1,X2)),inverse(multiply(multiply(X3,multiply(X4,inverse(X4))),multiply(multiply(X5,inverse(X5)),inverse(multiply(X1,X2)))))),multiply(X3,X0))))=multiply(X6,inverse(X6)))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f110,f46])).
% 18.35/2.80 fof(f243,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(multiply(X0,inverse(X0)),inverse(X1))=multiply(multiply(X2,inverse(X2)),inverse(X1)))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f10,f146])).
% 18.35/2.80 fof(f253,plain,(
% 18.35/2.80 ![X0,X1]: (multiply(X0,inverse(X0))=multiply(X1,inverse(X1)))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f46,f199])).
% 18.35/2.80 fof(f267,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(multiply(X1,inverse(X1)),multiply(X2,inverse(X2))),multiply(X3,X0))))=inverse(X3))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f253,f11])).
% 18.35/2.80 fof(f268,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(X1),multiply(multiply(X2,inverse(X2)),X0))))=X1)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f253,f3])).
% 18.35/2.80 fof(f289,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,inverse(X2)))),multiply(X3,inverse(X3))),multiply(X4,X0))))=inverse(X4))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f253,f11])).
% 18.35/2.80 fof(f333,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X0))),inverse(multiply(inverse(X1),multiply(X2,inverse(X2)))))=X1)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f253,f268])).
% 18.35/2.80 fof(f363,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(X0,inverse(X0))=multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,inverse(X2)))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f253,f243])).
% 18.35/2.80 fof(f418,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,inverse(multiply(multiply(multiply(X1,inverse(X1)),multiply(X2,inverse(X2))),multiply(inverse(X3),X0))))=multiply(multiply(multiply(X4,inverse(X4)),inverse(multiply(multiply(X5,inverse(X5)),inverse(X3)))),multiply(X6,inverse(X6))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f243,f14])).
% 18.35/2.80 fof(f470,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (inverse(inverse(X0))=multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(multiply(X2,inverse(X2)),inverse(X0)))),multiply(X3,inverse(X3))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f267,f418])).
% 18.35/2.80 fof(f512,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(X0))),inverse(multiply(inverse(X1),multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,inverse(X3)))))))=X1)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f363,f268])).
% 18.35/2.80 fof(f533,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),multiply(multiply(X3,inverse(X3)),inverse(multiply(multiply(X4,inverse(X4)),inverse(multiply(X5,inverse(X5))))))))),inverse(multiply(inverse(X6),X2)))=X6)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f363,f10])).
% 18.35/2.80 fof(f536,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(inverse(X0),inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,inverse(X4)))))))=multiply(multiply(multiply(X5,inverse(X5)),inverse(multiply(X1,X0))),multiply(X6,inverse(X6))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f363,f14])).
% 18.35/2.80 fof(f538,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,inverse(X3)))))),multiply(X4,inverse(X4))),multiply(X5,X0))))=inverse(X5))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f363,f11])).
% 18.35/2.80 fof(f568,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(inverse(multiply(X2,inverse(X2))),X0))),multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,multiply(X5,inverse(X5)))))))),inverse(multiply(X6,inverse(X6))))=X4)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f363,f10])).
% 18.35/2.80 fof(f574,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,inverse(X2)))),multiply(X3,inverse(X3))),multiply(multiply(X4,inverse(X4)),X0))))=inverse(multiply(X5,inverse(X5))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f363,f11])).
% 18.35/2.80 fof(f577,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),multiply(X2,X0))))=inverse(X2))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f470,f538])).
% 18.35/2.80 fof(f582,plain,(
% 18.35/2.80 ![X0,X1]: (inverse(multiply(X0,inverse(X0)))=inverse(multiply(X1,inverse(X1))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f289,f574])).
% 18.35/2.80 fof(f587,plain,(
% 18.35/2.80 ![X0,X1,X2]: (inverse(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,inverse(X1)))))=inverse(multiply(X2,inverse(X2))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f243,f582])).
% 18.35/2.80 fof(f666,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(multiply(X2,inverse(X2)),X0))),X3))=X3)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f268,f12])).
% 18.35/2.80 fof(f799,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(X0,multiply(X1,inverse(X1)))=multiply(X0,multiply(X2,inverse(X2))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f13,f13])).
% 18.35/2.80 fof(f829,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(X2)),multiply(X3,inverse(X3))),multiply(X4,inverse(X4))),multiply(multiply(X5,multiply(X6,inverse(X6))),X0))))=multiply(inverse(multiply(X7,multiply(multiply(multiply(X8,inverse(X8)),inverse(multiply(X2,X7))),X5))),multiply(X9,inverse(X9))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f12,f13])).
% 18.35/2.80 fof(f884,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(X2,multiply(X3,inverse(X3))))),multiply(multiply(multiply(X4,inverse(X4)),inverse(X5)),X0))))=inverse(multiply(multiply(X6,multiply(X7,inverse(X7))),multiply(multiply(multiply(multiply(X8,inverse(X8)),inverse(multiply(X2,X6))),multiply(X9,inverse(X9))),multiply(multiply(X10,inverse(X10)),inverse(multiply(X5,X1)))))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f13,f12])).
% 18.35/2.80 fof(f956,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(X0,multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,inverse(X2)))))=multiply(X0,multiply(X3,inverse(X3))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f243,f799])).
% 18.35/2.80 fof(f1240,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,inverse(X1)))),inverse(multiply(X2,inverse(X2))))),inverse(multiply(inverse(X3),multiply(X4,inverse(X4)))))=X3)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f587,f333])).
% 18.35/2.80 fof(f1344,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X0))),multiply(X1,inverse(X1)))=inverse(multiply(X2,inverse(X2))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f363,f666])).
% 18.35/2.80 fof(f1358,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))),multiply(X4,inverse(X4))))=inverse(multiply(multiply(X2,multiply(X5,inverse(X5))),multiply(X3,multiply(multiply(X6,inverse(X6)),inverse(multiply(multiply(X7,inverse(X7)),X0)))))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f14,f666])).
% 18.35/2.80 fof(f1359,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,X1)=inverse(multiply(X2,multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,X2))),multiply(multiply(X4,inverse(X4)),inverse(multiply(multiply(X5,inverse(X5)),X0)))))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f3,f666])).
% 18.35/2.80 fof(f1363,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X0))),multiply(multiply(X1,inverse(X1)),X2))=X2)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f363,f666])).
% 18.35/2.80 fof(f1399,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(inverse(multiply(multiply(X0,multiply(X1,inverse(X1))),multiply(multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X0))),multiply(X4,inverse(X4))),multiply(X5,inverse(X5))))),multiply(multiply(multiply(X6,inverse(X6)),inverse(multiply(X3,multiply(X7,inverse(X7))))),X8))=X8)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f13,f666])).
% 18.35/2.80 fof(f1417,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(X0))),inverse(inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(multiply(X2,inverse(X2)),inverse(X3)))))))=X3)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f666,f333])).
% 18.35/2.80 fof(f1457,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(multiply(inverse(multiply(X0,inverse(X0))),X1),inverse(multiply(inverse(X2),X1)))=X2)),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f1359,f533])).
% 18.35/2.80 fof(f1547,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),multiply(X2,inverse(X2)))))))=X1)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f333,f1457])).
% 18.35/2.80 fof(f1747,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(multiply(X0,inverse(X0)),inverse(multiply(inverse(multiply(X1,inverse(X1))),multiply(multiply(X2,inverse(X2)),inverse(multiply(multiply(X3,multiply(X4,inverse(X4))),inverse(multiply(X5,inverse(X5)))))))))=X3)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f1344,f47])).
% 18.35/2.80 fof(f1834,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(multiply(X0,inverse(X0)),inverse(inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),inverse(multiply(X3,inverse(X3)))))))=X1)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f1363,f1747])).
% 18.35/2.80 fof(f1842,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(X1))=multiply(X2,multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(multiply(X4,inverse(X4)),X2))),multiply(multiply(X5,inverse(X5)),inverse(multiply(X1,inverse(X0)))))))),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f10,f1547])).
% 18.35/2.80 fof(f1843,plain,(
% 18.35/2.80 ![X0,X1]: (multiply(inverse(multiply(X0,inverse(X0))),inverse(inverse(X1)))=X1)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f577,f1547])).
% 18.35/2.80 fof(f1854,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(multiply(X2,inverse(X2)),inverse(multiply(multiply(X3,inverse(X3)),inverse(X0)))))))))=X1)),
% 18.35/2.80 inference(paramodulation,[status(thm)],[f666,f1547])).
% 18.35/2.80 fof(f1961,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X0))),inverse(inverse(multiply(X1,inverse(multiply(X2,inverse(X2)))))))=X1)),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2085,f1417])).
% 18.35/2.80 fof(f1962,plain,(
% 18.35/2.80 ![X0,X1,X2]: (inverse(inverse(X0))=multiply(multiply(X0,inverse(multiply(X1,inverse(X1)))),multiply(X2,inverse(X2))))),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2085,f470])).
% 18.35/2.80 fof(f2033,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(inverse(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,inverse(X1))))),inverse(multiply(inverse(X2),multiply(X3,inverse(X3)))))=X2)),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2085,f1240])).
% 18.35/2.80 fof(f2043,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(X0,multiply(X1,inverse(X1)))=multiply(X0,multiply(X2,inverse(X2))))),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2085,f956])).
% 18.35/2.80 fof(f2059,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(X0),inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(X3,inverse(X3)))))=multiply(multiply(multiply(X4,inverse(X4)),inverse(multiply(X1,X0))),multiply(X5,inverse(X5))))),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2085,f536])).
% 18.35/2.80 fof(f2064,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X0))),inverse(multiply(inverse(X1),multiply(X2,inverse(X2)))))=X1)),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2085,f512])).
% 18.35/2.80 fof(f2077,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(X3,X0))))=multiply(multiply(multiply(X4,inverse(X4)),inverse(multiply(X1,X3))),multiply(X5,inverse(X5))))),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2085,f193])).
% 18.35/2.80 fof(f2085,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(X0,inverse(X1))=multiply(multiply(X2,inverse(X2)),inverse(multiply(X1,inverse(X0)))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f666,f1842])).
% 18.35/2.80 fof(f2098,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(multiply(X0,inverse(multiply(X2,inverse(X2)))))))))=X1)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2085,f1854])).
% 18.35/2.80 fof(f2177,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(multiply(X0,inverse(X0)),inverse(inverse(multiply(X1,multiply(X2,inverse(X2))))))=X1)),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2191,f1834])).
% 18.35/2.80 fof(f2180,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(inverse(multiply(X2,inverse(X2))),X0))),multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,multiply(X5,inverse(X5))))))))=X4)),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2191,f568])).
% 18.35/2.80 fof(f2183,plain,(
% 18.35/2.80 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),inverse(inverse(X0)))))=X1)),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2191,f2098])).
% 18.35/2.80 fof(f2191,plain,(
% 18.35/2.80 ![X0,X1]: (multiply(X0,inverse(multiply(X1,inverse(X1))))=X0)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f1843,f1961])).
% 18.35/2.80 fof(f2196,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(X3,X0))))=inverse(inverse(multiply(multiply(X4,inverse(X4)),inverse(multiply(X1,X3))))))),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2629,f14])).
% 18.35/2.80 fof(f2214,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(inverse(multiply(multiply(X0,multiply(X1,inverse(X1))),inverse(inverse(multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X0))),multiply(X4,inverse(X4))))))),multiply(multiply(multiply(X5,inverse(X5)),inverse(multiply(X3,multiply(X6,inverse(X6))))),X7))=X7)),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2629,f1399])).
% 18.35/2.80 fof(f2225,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(X0,inverse(multiply(inverse(inverse(multiply(multiply(multiply(X1,inverse(X1)),inverse(X2)),multiply(X3,inverse(X3))))),multiply(multiply(X4,multiply(X5,inverse(X5))),X0))))=multiply(inverse(multiply(X6,multiply(multiply(multiply(X7,inverse(X7)),inverse(multiply(X2,X6))),X4))),multiply(X8,inverse(X8))))),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2629,f829])).
% 18.35/2.80 fof(f2253,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(X0,inverse(multiply(inverse(inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X4))),multiply(X5,inverse(X5))))))),multiply(X6,X0))))=inverse(multiply(multiply(X3,multiply(X7,inverse(X7))),multiply(X4,X6))))),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2629,f44])).
% 18.35/2.80 fof(f2307,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,inverse(inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))))))=inverse(multiply(multiply(X2,multiply(X4,inverse(X4))),multiply(X3,multiply(multiply(X5,inverse(X5)),inverse(multiply(multiply(X6,inverse(X6)),X0)))))))),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2629,f1358])).
% 18.35/2.80 fof(f2338,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(X2,multiply(X3,inverse(X3))))),multiply(multiply(multiply(X4,inverse(X4)),inverse(X5)),X0))))=inverse(multiply(multiply(X6,multiply(X7,inverse(X7))),multiply(inverse(inverse(multiply(multiply(X8,inverse(X8)),inverse(multiply(X2,X6))))),multiply(multiply(X9,inverse(X9)),inverse(multiply(X5,X1)))))))),
% 18.35/2.80 inference(backward_demodulation,[status(thm)],[f2629,f884])).
% 18.35/2.80 fof(f2629,plain,(
% 18.35/2.80 ![X0,X1]: (inverse(inverse(X0))=multiply(X0,multiply(X1,inverse(X1))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2191,f1962])).
% 18.35/2.80 fof(f2753,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X0))),inverse(multiply(inverse(X1),multiply(X2,inverse(X2)))))=X1)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2085,f2033])).
% 18.35/2.80 fof(f2754,plain,(
% 18.35/2.80 ![X0,X1]: (multiply(inverse(multiply(X0,inverse(X0))),inverse(inverse(inverse(inverse(X1)))))=X1)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2629,f2753])).
% 18.35/2.80 fof(f2819,plain,(
% 18.35/2.80 ![X0]: (inverse(inverse(X0))=X0)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f1843,f2754])).
% 18.35/2.80 fof(f2837,plain,(
% 18.35/2.80 ![X0,X1]: (inverse(inverse(X0))=multiply(X0,multiply(X1,inverse(X1))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2629,f2043])).
% 18.35/2.80 fof(f2838,plain,(
% 18.35/2.80 ![X0,X1]: (X0=multiply(X0,multiply(X1,inverse(X1))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2819,f2837])).
% 18.35/2.80 fof(f2868,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),inverse(multiply(X1,multiply(X2,inverse(X2)))))=multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,X0))),multiply(X4,inverse(X4))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f2059])).
% 18.35/2.80 fof(f2869,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(inverse(X0),inverse(X1))=multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X1,X0))),multiply(X3,inverse(X3))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f2868])).
% 18.35/2.80 fof(f2921,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(inverse(X0),inverse(X1))=multiply(multiply(X2,inverse(X2)),inverse(multiply(X1,X0))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f2869])).
% 18.35/2.80 fof(f2933,plain,(
% 18.35/2.80 ![X0,X1]: (multiply(inverse(multiply(X0,inverse(X0))),inverse(inverse(X1)))=X1)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f2064])).
% 18.35/2.80 fof(f2940,plain,(
% 18.35/2.80 ![X0,X1]: (multiply(inverse(multiply(X0,inverse(X0))),X1)=X1)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2819,f2933])).
% 18.35/2.80 fof(f2956,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(X1,multiply(X2,X0))))=multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,X2))),multiply(X4,inverse(X4))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f2077])).
% 18.35/2.80 fof(f2957,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,multiply(X2,X0))))=multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,X2))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f2956])).
% 18.35/2.80 fof(f2967,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(X0,inverse(multiply(X1,multiply(X2,X0))))=multiply(inverse(X2),inverse(X1)))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2921,f2957])).
% 18.35/2.80 fof(f2998,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(multiply(X0,inverse(X0)),multiply(X1,multiply(X2,inverse(X2))))=X1)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2819,f2177])).
% 18.35/2.80 fof(f3004,plain,(
% 18.35/2.80 ![X0,X1]: (multiply(multiply(X0,inverse(X0)),X1)=X1)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f2998])).
% 18.35/2.80 fof(f3009,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (inverse(multiply(X0,multiply(multiply(inverse(X0),inverse(inverse(multiply(X1,inverse(X1))))),multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X4,inverse(X4))))))))=X3)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2921,f2180])).
% 18.35/2.80 fof(f3010,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (inverse(multiply(X0,multiply(multiply(inverse(X0),multiply(X1,inverse(X1))),multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X4,inverse(X4))))))))=X3)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2819,f3009])).
% 18.35/2.80 fof(f3011,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (inverse(multiply(X0,multiply(inverse(X0),multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(X3,inverse(X3))))))))=X2)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f3010])).
% 18.35/2.80 fof(f3012,plain,(
% 18.35/2.80 ![X0,X1,X2]: (inverse(multiply(X0,multiply(inverse(X0),multiply(inverse(multiply(X1,inverse(X1))),inverse(X2)))))=X2)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2921,f3011])).
% 18.35/2.80 fof(f3015,plain,(
% 18.35/2.80 ![X0,X1]: (inverse(multiply(X0,multiply(inverse(X0),inverse(X1))))=X1)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2940,f3012])).
% 18.35/2.80 fof(f3021,plain,(
% 18.35/2.80 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),X0)))=X1)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2819,f2183])).
% 18.35/2.80 fof(f3050,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(inverse(X0),inverse(multiply(X1,multiply(X2,inverse(X2)))))=inverse(inverse(multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,X0))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2967,f2196])).
% 18.35/2.80 fof(f3051,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(inverse(X0),inverse(X1))=inverse(inverse(multiply(multiply(X2,inverse(X2)),inverse(multiply(X1,X0))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f3050])).
% 18.35/2.80 fof(f3052,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(inverse(X0),inverse(X1))=multiply(multiply(X2,inverse(X2)),inverse(multiply(X1,X0))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2819,f3051])).
% 18.35/2.80 fof(f3061,plain,(
% 18.35/2.80 ![X0,X1]: (multiply(inverse(X0),inverse(X1))=inverse(multiply(X1,X0)))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3004,f3052])).
% 18.35/2.80 fof(f3158,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),multiply(X3,inverse(X3))))))),multiply(multiply(multiply(X4,inverse(X4)),inverse(multiply(X2,multiply(X5,inverse(X5))))),X6))=X6)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f2214])).
% 18.35/2.80 fof(f3159,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),multiply(X3,inverse(X3))))),multiply(multiply(multiply(X4,inverse(X4)),inverse(multiply(X2,multiply(X5,inverse(X5))))),X6))=X6)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2819,f3158])).
% 18.35/2.80 fof(f3160,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(X0,multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))))),multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X2,multiply(X4,inverse(X4))))),X5))=X5)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f3159])).
% 18.35/2.80 fof(f3161,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(X0,multiply(inverse(X0),inverse(X1)))),multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X1,multiply(X3,inverse(X3))))),X4))=X4)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2921,f3160])).
% 18.35/2.80 fof(f3162,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X0,multiply(X2,inverse(X2))))),X3))=X3)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3015,f3161])).
% 18.35/2.80 fof(f3163,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(X0,multiply(multiply(inverse(multiply(X1,inverse(X1))),inverse(X0)),X2))=X2)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2921,f3162])).
% 18.35/2.80 fof(f3164,plain,(
% 18.35/2.80 ![X0,X1]: (multiply(X0,multiply(inverse(X0),X1))=X1)),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2940,f3163])).
% 18.35/2.80 fof(f3247,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(inverse(multiply(X0,multiply(X1,inverse(X1)))),inverse(inverse(inverse(multiply(multiply(multiply(X2,inverse(X2)),inverse(X3)),multiply(X4,inverse(X4)))))))=multiply(inverse(multiply(X5,multiply(multiply(multiply(X6,inverse(X6)),inverse(multiply(X3,X5))),X0))),multiply(X7,inverse(X7))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2967,f2225])).
% 18.35/2.80 fof(f3248,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (inverse(multiply(inverse(inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(X1)),multiply(X2,inverse(X2))))),multiply(X3,multiply(X4,inverse(X4)))))=multiply(inverse(multiply(X5,multiply(multiply(multiply(X6,inverse(X6)),inverse(multiply(X1,X5))),X3))),multiply(X7,inverse(X7))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3061,f3247])).
% 18.35/2.80 fof(f3249,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (inverse(multiply(multiply(multiply(multiply(X0,inverse(X0)),inverse(X1)),multiply(X2,inverse(X2))),multiply(X3,multiply(X4,inverse(X4)))))=multiply(inverse(multiply(X5,multiply(multiply(multiply(X6,inverse(X6)),inverse(multiply(X1,X5))),X3))),multiply(X7,inverse(X7))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2819,f3248])).
% 18.35/2.80 fof(f3250,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(X1)),multiply(X2,multiply(X3,inverse(X3)))))=multiply(inverse(multiply(X4,multiply(multiply(multiply(X5,inverse(X5)),inverse(multiply(X1,X4))),X2))),multiply(X6,inverse(X6))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f3249])).
% 18.35/2.80 fof(f3251,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (inverse(multiply(inverse(X0),multiply(X1,multiply(X2,inverse(X2)))))=multiply(inverse(multiply(X3,multiply(multiply(multiply(X4,inverse(X4)),inverse(multiply(X0,X3))),X1))),multiply(X5,inverse(X5))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3004,f3250])).
% 18.35/2.80 fof(f3252,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (inverse(multiply(inverse(X0),X1))=multiply(inverse(multiply(X2,multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,X2))),X1))),multiply(X4,inverse(X4))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f3251])).
% 18.35/2.80 fof(f3253,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (inverse(multiply(inverse(X0),X1))=inverse(multiply(X2,multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,X2))),X1))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f3252])).
% 18.35/2.80 fof(f3254,plain,(
% 18.35/2.80 ![X0,X1,X2]: (inverse(multiply(inverse(X0),X1))=inverse(multiply(X2,multiply(multiply(inverse(X2),inverse(X0)),X1))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2921,f3253])).
% 18.35/2.80 fof(f3256,plain,(
% 18.35/2.80 ![X0,X1,X2]: (inverse(multiply(inverse(X0),X1))=inverse(multiply(X2,multiply(inverse(multiply(X0,X2)),X1))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3061,f3254])).
% 18.35/2.80 fof(f3455,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(inverse(X0),inverse(inverse(inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X4))),multiply(X5,inverse(X5)))))))))=inverse(multiply(multiply(X3,multiply(X6,inverse(X6))),multiply(X4,X0))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2967,f2253])).
% 18.35/2.80 fof(f3456,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (inverse(multiply(inverse(inverse(multiply(multiply(X0,inverse(X0)),inverse(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))),multiply(X4,inverse(X4))))))),X5))=inverse(multiply(multiply(X2,multiply(X6,inverse(X6))),multiply(X3,X5))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3061,f3455])).
% 18.35/2.80 fof(f3457,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))),multiply(X4,inverse(X4))))),X5))=inverse(multiply(multiply(X2,multiply(X6,inverse(X6))),multiply(X3,X5))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2819,f3456])).
% 18.35/2.80 fof(f3458,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (inverse(multiply(multiply(inverse(multiply(X0,inverse(X0))),inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))))),X4))=inverse(multiply(multiply(X2,multiply(X5,inverse(X5))),multiply(X3,X4))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2921,f3457])).
% 18.35/2.80 fof(f3459,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (inverse(multiply(inverse(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,X2)))),X3))=inverse(multiply(multiply(X1,multiply(X4,inverse(X4))),multiply(X2,X3))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2940,f3458])).
% 18.35/2.80 fof(f3460,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (inverse(multiply(inverse(multiply(inverse(X0),inverse(X1))),X2))=inverse(multiply(multiply(X1,multiply(X3,inverse(X3))),multiply(X0,X2))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2921,f3459])).
% 18.35/2.80 fof(f3461,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (inverse(multiply(inverse(inverse(multiply(X0,X1))),X2))=inverse(multiply(multiply(X0,multiply(X3,inverse(X3))),multiply(X1,X2))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3061,f3460])).
% 18.35/2.80 fof(f3462,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (inverse(multiply(multiply(X0,X1),X2))=inverse(multiply(multiply(X0,multiply(X3,inverse(X3))),multiply(X1,X2))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2819,f3461])).
% 18.35/2.80 fof(f3467,plain,(
% 18.35/2.80 ![X0,X1,X2]: (inverse(multiply(multiply(X0,X1),X2))=inverse(multiply(X0,multiply(X1,X2))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f3462])).
% 18.35/2.80 fof(f3942,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))))=inverse(multiply(multiply(X2,multiply(X4,inverse(X4))),multiply(X3,multiply(multiply(X5,inverse(X5)),inverse(multiply(multiply(X6,inverse(X6)),X0)))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2819,f2307])).
% 18.35/2.80 fof(f3943,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,multiply(inverse(X1),inverse(X2)))=inverse(multiply(multiply(X2,multiply(X3,inverse(X3))),multiply(X1,multiply(multiply(X4,inverse(X4)),inverse(multiply(multiply(X5,inverse(X5)),X0)))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2921,f3942])).
% 18.35/2.80 fof(f3944,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(X1,X2)))=inverse(multiply(multiply(X1,multiply(X3,inverse(X3))),multiply(X2,multiply(multiply(X4,inverse(X4)),inverse(multiply(multiply(X5,inverse(X5)),X0)))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3061,f3943])).
% 18.35/2.80 fof(f3945,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(X1,X2)))=inverse(multiply(X1,multiply(multiply(X3,inverse(X3)),multiply(X2,multiply(multiply(X4,inverse(X4)),inverse(multiply(multiply(X5,inverse(X5)),X0))))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3467,f3944])).
% 18.35/2.80 fof(f3946,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(X1,X2)))=inverse(multiply(X1,multiply(X2,multiply(multiply(X3,inverse(X3)),inverse(multiply(multiply(X4,inverse(X4)),X0)))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3004,f3945])).
% 18.35/2.80 fof(f3947,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,X2)))=inverse(multiply(X1,multiply(X2,multiply(inverse(X0),inverse(multiply(X3,inverse(X3))))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2921,f3946])).
% 18.35/2.80 fof(f3948,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,X2)))=inverse(multiply(X1,multiply(X2,inverse(multiply(multiply(X3,inverse(X3)),X0))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3061,f3947])).
% 18.35/2.80 fof(f3949,plain,(
% 18.35/2.80 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,X2)))=inverse(multiply(X1,multiply(X2,inverse(multiply(X3,multiply(inverse(X3),X0)))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3467,f3948])).
% 18.35/2.80 fof(f3950,plain,(
% 18.35/2.80 ![X0,X1,X2]: (multiply(X0,inverse(multiply(X1,X2)))=inverse(multiply(X1,multiply(X2,inverse(X0)))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3164,f3949])).
% 18.35/2.80 fof(f4301,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(inverse(multiply(multiply(X0,inverse(X0)),inverse(X1))),inverse(inverse(multiply(X2,multiply(X3,multiply(X4,inverse(X4)))))))=inverse(multiply(multiply(X5,multiply(X6,inverse(X6))),multiply(inverse(inverse(multiply(multiply(X7,inverse(X7)),inverse(multiply(X3,X5))))),multiply(multiply(X8,inverse(X8)),inverse(multiply(X1,X2)))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2967,f2338])).
% 18.35/2.80 fof(f4302,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (inverse(multiply(inverse(multiply(X0,multiply(X1,multiply(X2,inverse(X2))))),multiply(multiply(X3,inverse(X3)),inverse(X4))))=inverse(multiply(multiply(X5,multiply(X6,inverse(X6))),multiply(inverse(inverse(multiply(multiply(X7,inverse(X7)),inverse(multiply(X1,X5))))),multiply(multiply(X8,inverse(X8)),inverse(multiply(X4,X0)))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3061,f4301])).
% 18.35/2.80 fof(f4303,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(X2,multiply(X3,inverse(X3))))),multiply(X4,inverse(X4)))))=inverse(multiply(multiply(X5,multiply(X6,inverse(X6))),multiply(inverse(inverse(multiply(multiply(X7,inverse(X7)),inverse(multiply(X2,X5))))),multiply(multiply(X8,inverse(X8)),inverse(multiply(X0,X1)))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3950,f4302])).
% 18.35/2.80 fof(f4304,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (multiply(X0,multiply(X1,inverse(multiply(inverse(multiply(X2,multiply(X3,multiply(X4,inverse(X4))))),X1))))=inverse(multiply(multiply(X5,multiply(X6,inverse(X6))),multiply(inverse(inverse(multiply(multiply(X7,inverse(X7)),inverse(multiply(X3,X5))))),multiply(multiply(X8,inverse(X8)),inverse(multiply(X0,X2)))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3950,f4303])).
% 18.35/2.80 fof(f4305,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(X0,multiply(X1,multiply(X2,multiply(X3,inverse(X3)))))=inverse(multiply(multiply(X4,multiply(X5,inverse(X5))),multiply(inverse(inverse(multiply(multiply(X6,inverse(X6)),inverse(multiply(X2,X4))))),multiply(multiply(X7,inverse(X7)),inverse(multiply(X0,X1)))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3021,f4304])).
% 18.35/2.80 fof(f4306,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,multiply(X1,X2))=inverse(multiply(multiply(X3,multiply(X4,inverse(X4))),multiply(inverse(inverse(multiply(multiply(X5,inverse(X5)),inverse(multiply(X2,X3))))),multiply(multiply(X6,inverse(X6)),inverse(multiply(X0,X1)))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f2838,f4305])).
% 18.35/2.80 fof(f4307,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,multiply(X1,X2))=inverse(multiply(X3,multiply(multiply(X4,inverse(X4)),multiply(inverse(inverse(multiply(multiply(X5,inverse(X5)),inverse(multiply(X2,X3))))),multiply(multiply(X6,inverse(X6)),inverse(multiply(X0,X1))))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3467,f4306])).
% 18.35/2.80 fof(f4308,plain,(
% 18.35/2.80 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,multiply(X1,X2))=inverse(multiply(X3,multiply(inverse(inverse(multiply(multiply(X4,inverse(X4)),inverse(multiply(X2,X3))))),multiply(multiply(X5,inverse(X5)),inverse(multiply(X0,X1)))))))),
% 18.35/2.80 inference(forward_demodulation,[status(thm)],[f3004,f4307])).
% 19.15/2.84 fof(f4309,plain,(
% 19.15/2.84 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,multiply(X1,X2))=inverse(multiply(X3,multiply(multiply(multiply(X4,inverse(X4)),inverse(multiply(X2,X3))),multiply(multiply(X5,inverse(X5)),inverse(multiply(X0,X1)))))))),
% 19.15/2.84 inference(forward_demodulation,[status(thm)],[f2819,f4308])).
% 19.15/2.84 fof(f4310,plain,(
% 19.15/2.84 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(X1,X2))=inverse(multiply(X3,multiply(multiply(inverse(X3),inverse(X2)),multiply(multiply(X4,inverse(X4)),inverse(multiply(X0,X1)))))))),
% 19.15/2.84 inference(forward_demodulation,[status(thm)],[f2921,f4309])).
% 19.15/2.84 fof(f4311,plain,(
% 19.15/2.84 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(X1,X2))=inverse(multiply(X3,multiply(inverse(multiply(X2,X3)),multiply(multiply(X4,inverse(X4)),inverse(multiply(X0,X1)))))))),
% 19.15/2.84 inference(forward_demodulation,[status(thm)],[f3061,f4310])).
% 19.15/2.84 fof(f4312,plain,(
% 19.15/2.84 ![X0,X1,X2,X3]: (multiply(X0,multiply(X1,X2))=inverse(multiply(inverse(X2),multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,X1))))))),
% 19.15/2.84 inference(forward_demodulation,[status(thm)],[f3256,f4311])).
% 19.15/2.84 fof(f4313,plain,(
% 19.15/2.84 ![X0,X1,X2,X3]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),inverse(multiply(inverse(X2),multiply(X3,inverse(X3))))))),
% 19.15/2.84 inference(forward_demodulation,[status(thm)],[f3950,f4312])).
% 19.15/2.84 fof(f4314,plain,(
% 19.15/2.84 ![X0,X1,X2,X3]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),multiply(X3,inverse(multiply(inverse(X2),X3)))))),
% 19.15/2.84 inference(forward_demodulation,[status(thm)],[f3950,f4313])).
% 19.15/2.84 fof(f4315,plain,(
% 19.15/2.84 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))),
% 19.15/2.84 inference(backward_demodulation,[status(thm)],[f4327,f4])).
% 19.15/2.84 fof(f4327,plain,(
% 19.15/2.84 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 19.15/2.84 inference(forward_demodulation,[status(thm)],[f3021,f4314])).
% 19.15/2.84 fof(f8106,plain,(
% 19.15/2.84 $false),
% 19.15/2.84 inference(trivial_equality_resolution,[status(thm)],[f4315])).
% 19.15/2.84 % SZS output end CNFRefutation for theBenchmark.p
% 10.53/8.73 % Elapsed time: 8.369783 seconds
% 10.53/8.73 % CPU time: 65.642012 seconds
% 10.53/8.73 % Total memory used: 36.854 GB
% 10.53/8.73 % Net memory used: 36.852 GB
%------------------------------------------------------------------------------