%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP058-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:32:25 PM UTC 2026
% Result : Unsatisfiable 47.17s 12.06s
% Output : CNFRefutation 47.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 2
% Syntax : Number of formulae : 197 ( 193 unt; 0 def)
% Number of atoms : 204 ( 203 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 19 ( 12 ~; 7 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 943 ( 943 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,Z,U] : multiply(X,inverse(multiply(Y,multiply(multiply(multiply(Z,inverse(Z)),inverse(multiply(U,Y))),X)))) = U,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))),X0)))) = X3,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f4,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f5,plain,
! [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,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f6,plain,
! [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,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f7,plain,
! [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,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f8,plain,
! [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))),
inference(paramodulation,[status(thm)],[f6,f6]) ).
fof(f9,plain,
! [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))),
inference(paramodulation,[status(thm)],[f3,f6]) ).
fof(f19,plain,
! [X0,X1,X2,X3,X4,X5] : X0 = multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,multiply(X2,multiply(X4,inverse(X4))))))))),multiply(X5,inverse(X5))),
inference(paramodulation,[status(thm)],[f3,f9]) ).
fof(f21,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] : multiply(multiply(X0,inverse(X0)),inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(X3,inverse(multiply(multiply(X4,multiply(X5,inverse(X5))),multiply(X6,X3))))))) = multiply(multiply(multiply(X7,inverse(X7)),inverse(multiply(X1,multiply(multiply(X8,inverse(X8)),inverse(multiply(X4,X6)))))),multiply(X9,inverse(X9))),
inference(paramodulation,[status(thm)],[f9,f9]) ).
fof(f39,plain,
! [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))),
inference(paramodulation,[status(thm)],[f9,f6]) ).
fof(f41,plain,
! [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,
inference(paramodulation,[status(thm)],[f9,f6]) ).
fof(f42,plain,
! [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,
inference(paramodulation,[status(thm)],[f9,f3]) ).
fof(f77,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(X1,multiply(X2,X0)))) = multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,multiply(X2,multiply(X4,inverse(X4)))))),
inference(paramodulation,[status(thm)],[f3,f41]) ).
fof(f79,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(X0,inverse(multiply(multiply(inverse(multiply(X1,X2)),inverse(multiply(multiply(X3,multiply(X4,inverse(X4))),X5))),multiply(X3,X0)))) = inverse(multiply(X6,multiply(multiply(multiply(X7,inverse(X7)),inverse(multiply(X2,X6))),multiply(multiply(X8,inverse(X8)),inverse(multiply(X5,X1)))))),
inference(paramodulation,[status(thm)],[f5,f41]) ).
fof(f105,plain,
! [X0,X1,X2,X3] : multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,X2))) = multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,X2))),
inference(paramodulation,[status(thm)],[f6,f42]) ).
fof(f141,plain,
! [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))))),
inference(paramodulation,[status(thm)],[f5,f105]) ).
fof(f188,plain,
! [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))),
inference(paramodulation,[status(thm)],[f105,f9]) ).
fof(f194,plain,
! [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)),
inference(paramodulation,[status(thm)],[f105,f41]) ).
fof(f238,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(X0)),inverse(X1)) = multiply(multiply(X2,inverse(X2)),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f5,f141]) ).
fof(f248,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = multiply(X1,inverse(X1)),
inference(forward_demodulation,[status(thm)],[f41,f194]) ).
fof(f262,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(multiply(X1,inverse(X1)),multiply(X2,inverse(X2))),multiply(X3,X0)))) = inverse(X3),
inference(paramodulation,[status(thm)],[f248,f6]) ).
fof(f263,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(inverse(X1),multiply(multiply(X2,inverse(X2)),X0)))) = X1,
inference(paramodulation,[status(thm)],[f248,f3]) ).
fof(f328,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(X0))),inverse(multiply(inverse(X1),multiply(X2,inverse(X2))))) = X1,
inference(paramodulation,[status(thm)],[f248,f263]) ).
fof(f358,plain,
! [X0,X1,X2] : multiply(X0,inverse(X0)) = multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,inverse(X2)))),
inference(paramodulation,[status(thm)],[f248,f238]) ).
fof(f413,plain,
! [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))),
inference(paramodulation,[status(thm)],[f238,f9]) ).
fof(f465,plain,
! [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))),
inference(forward_demodulation,[status(thm)],[f262,f413]) ).
fof(f528,plain,
! [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,
inference(paramodulation,[status(thm)],[f358,f5]) ).
fof(f531,plain,
! [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))),
inference(paramodulation,[status(thm)],[f358,f9]) ).
fof(f533,plain,
! [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),
inference(paramodulation,[status(thm)],[f358,f6]) ).
fof(f572,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),multiply(X2,X0)))) = inverse(X2),
inference(forward_demodulation,[status(thm)],[f465,f533]) ).
fof(f661,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(multiply(X2,inverse(X2)),X0))),X3)) = X3,
inference(paramodulation,[status(thm)],[f263,f7]) ).
fof(f753,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),X3))),inverse(multiply(multiply(multiply(multiply(X4,inverse(X4)),inverse(X5)),multiply(X6,inverse(X6))),X2))) = inverse(multiply(X7,multiply(multiply(multiply(X8,inverse(X8)),inverse(multiply(X5,X7))),X3))),
inference(paramodulation,[status(thm)],[f7,f5]) ).
fof(f853,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] : multiply(X0,inverse(multiply(multiply(inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))),multiply(X4,inverse(X4))),multiply(X2,X5))),multiply(X6,inverse(X6))),multiply(multiply(multiply(multiply(X7,inverse(X7)),inverse(X3)),multiply(X8,inverse(X8))),X0)))) = multiply(X5,multiply(X9,inverse(X9))),
inference(paramodulation,[status(thm)],[f6,f8]) ).
fof(f933,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] : multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(X3,inverse(X3)),X0)))) = multiply(multiply(multiply(X4,inverse(X4)),inverse(multiply(X5,inverse(multiply(multiply(X6,multiply(X7,inverse(X7))),multiply(multiply(multiply(multiply(X8,inverse(X8)),inverse(multiply(X1,X6))),multiply(X9,inverse(X9))),X5)))))),multiply(X10,inverse(X10))),
inference(paramodulation,[status(thm)],[f8,f9]) ).
fof(f936,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] : multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,inverse(multiply(multiply(X3,multiply(X4,inverse(X4))),multiply(multiply(multiply(multiply(X5,inverse(X5)),inverse(multiply(X6,X3))),multiply(X7,inverse(X7))),X2)))))),multiply(X8,inverse(X8))),multiply(X6,X0)))) = multiply(X9,inverse(X9)),
inference(paramodulation,[status(thm)],[f8,f6]) ).
fof(f1130,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(inverse(multiply(multiply(X0,multiply(X1,inverse(X1))),multiply(multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X0))),multiply(X4,inverse(X4))),X5))),inverse(multiply(inverse(inverse(multiply(X6,inverse(X6)))),multiply(X3,multiply(X7,inverse(X7)))))) = inverse(X5),
inference(paramodulation,[status(thm)],[f8,f572]) ).
fof(f1151,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(inverse(multiply(X0,inverse(X0)))),multiply(X1,multiply(X2,inverse(X2))))),inverse(multiply(inverse(X3),inverse(X1)))) = X3,
inference(paramodulation,[status(thm)],[f572,f263]) ).
fof(f1354,plain,
! [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)))))),
inference(paramodulation,[status(thm)],[f3,f661]) ).
fof(f1355,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,inverse(X2))))) = inverse(multiply(multiply(X3,inverse(X3)),inverse(multiply(multiply(X4,inverse(X4)),X0)))),
inference(paramodulation,[status(thm)],[f358,f661]) ).
fof(f1412,plain,
! [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,
inference(paramodulation,[status(thm)],[f661,f328]) ).
fof(f1420,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(multiply(X0,inverse(X0)),inverse(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(multiply(X2,inverse(X2)),multiply(X3,multiply(X4,inverse(X4)))))),multiply(X5,inverse(X5))))) = X3,
inference(paramodulation,[status(thm)],[f661,f42]) ).
fof(f1452,plain,
! [X0,X1,X2] : multiply(multiply(inverse(multiply(X0,inverse(X0))),X1),inverse(multiply(inverse(X2),X1))) = X2,
inference(backward_demodulation,[status(thm)],[f1354,f528]) ).
fof(f1542,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),multiply(X2,inverse(X2))))))) = X1,
inference(paramodulation,[status(thm)],[f328,f1452]) ).
fof(f1675,plain,
! [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)))))),
inference(paramodulation,[status(thm)],[f5,f1542]) ).
fof(f1676,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(X0))),inverse(inverse(X1))) = X1,
inference(paramodulation,[status(thm)],[f572,f1542]) ).
fof(f1734,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),multiply(X2,inverse(X2)))))),inverse(multiply(multiply(X3,multiply(X4,inverse(X4))),X0))) = multiply(multiply(multiply(X5,inverse(X5)),inverse(multiply(X3,X1))),multiply(X6,inverse(X6))),
inference(paramodulation,[status(thm)],[f1542,f9]) ).
fof(f1736,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(X2)),multiply(X3,inverse(X3))),multiply(X4,X0)))) = inverse(multiply(inverse(X2),inverse(multiply(inverse(X4),multiply(X5,inverse(X5)))))),
inference(paramodulation,[status(thm)],[f1542,f6]) ).
fof(f1785,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(X0))),inverse(inverse(multiply(X1,inverse(multiply(X2,inverse(X2))))))) = X1,
inference(backward_demodulation,[status(thm)],[f1899,f1412]) ).
fof(f1786,plain,
! [X0,X1,X2] : inverse(inverse(X0)) = multiply(multiply(X0,inverse(multiply(X1,inverse(X1)))),multiply(X2,inverse(X2))),
inference(backward_demodulation,[status(thm)],[f1899,f465]) ).
fof(f1791,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(X0,inverse(multiply(multiply(multiply(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,X1))),multiply(X5,inverse(X5))),X6)),inverse(X6)),multiply(X7,inverse(X7))),multiply(X4,X0)))) = multiply(X8,inverse(X8)),
inference(backward_demodulation,[status(thm)],[f1899,f936]) ).
fof(f1792,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] : multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(X3,inverse(X3)),X0)))) = multiply(multiply(multiply(multiply(X4,multiply(X5,inverse(X5))),multiply(multiply(multiply(multiply(X6,inverse(X6)),inverse(multiply(X1,X4))),multiply(X7,inverse(X7))),X8)),inverse(X8)),multiply(X9,inverse(X9))),
inference(backward_demodulation,[status(thm)],[f1899,f933]) ).
fof(f1823,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(X1,inverse(X1))) = inverse(multiply(multiply(X2,inverse(X2)),inverse(multiply(multiply(X3,inverse(X3)),X0)))),
inference(backward_demodulation,[status(thm)],[f1899,f1355]) ).
fof(f1873,plain,
! [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))),
inference(backward_demodulation,[status(thm)],[f1899,f531]) ).
fof(f1891,plain,
! [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))),
inference(backward_demodulation,[status(thm)],[f1899,f188]) ).
fof(f1899,plain,
! [X0,X1,X2] : multiply(X0,inverse(X1)) = multiply(multiply(X2,inverse(X2)),inverse(multiply(X1,inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f661,f1675]) ).
fof(f1959,plain,
! [X0,X1] : multiply(X0,inverse(multiply(X1,inverse(X1)))) = X0,
inference(forward_demodulation,[status(thm)],[f1676,f1785]) ).
fof(f1964,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(X0))),inverse(inverse(inverse(inverse(X1))))) = X1,
inference(backward_demodulation,[status(thm)],[f2343,f328]) ).
fof(f2007,plain,
! [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))),
inference(backward_demodulation,[status(thm)],[f2343,f39]) ).
fof(f2024,plain,
! [X0,X1,X2,X3,X4] : multiply(multiply(X0,inverse(X0)),inverse(inverse(inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(multiply(X2,inverse(X2)),multiply(X3,multiply(X4,inverse(X4)))))))))) = X3,
inference(backward_demodulation,[status(thm)],[f2343,f1420]) ).
fof(f2030,plain,
! [X0,X1,X2,X3,X4] : X0 = inverse(inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,multiply(X2,multiply(X4,inverse(X4))))))))))),
inference(backward_demodulation,[status(thm)],[f2343,f19]) ).
fof(f2032,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(multiply(X0,inverse(X0)),inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(X3,inverse(multiply(multiply(X4,multiply(X5,inverse(X5))),multiply(X6,X3))))))) = inverse(inverse(multiply(multiply(X7,inverse(X7)),inverse(multiply(X1,multiply(multiply(X8,inverse(X8)),inverse(multiply(X4,X6)))))))),
inference(backward_demodulation,[status(thm)],[f2343,f21]) ).
fof(f2042,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),multiply(X2,inverse(X2)))))),inverse(multiply(multiply(X3,multiply(X4,inverse(X4))),X0))) = inverse(inverse(multiply(multiply(X5,inverse(X5)),inverse(multiply(X3,X1))))),
inference(backward_demodulation,[status(thm)],[f2343,f1734]) ).
fof(f2066,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(multiply(multiply(X0,multiply(X1,inverse(X1))),multiply(inverse(inverse(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X0))))),X4))),inverse(multiply(inverse(inverse(multiply(X5,inverse(X5)))),multiply(X3,multiply(X6,inverse(X6)))))) = inverse(X4),
inference(backward_demodulation,[status(thm)],[f2343,f1130]) ).
fof(f2091,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))))),multiply(X2,X4))),multiply(X5,inverse(X5))),multiply(multiply(multiply(multiply(X6,inverse(X6)),inverse(X3)),multiply(X7,inverse(X7))),X0)))) = multiply(X4,multiply(X8,inverse(X8))),
inference(backward_demodulation,[status(thm)],[f2343,f853]) ).
fof(f2151,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(inverse(inverse(multiply(multiply(X1,inverse(X1)),inverse(X2)))),multiply(X3,X0)))) = inverse(multiply(inverse(X2),inverse(multiply(inverse(X3),multiply(X4,inverse(X4)))))),
inference(backward_demodulation,[status(thm)],[f2343,f1736]) ).
fof(f2175,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),X3))),inverse(multiply(inverse(inverse(multiply(multiply(X4,inverse(X4)),inverse(X5)))),X2))) = inverse(multiply(X6,multiply(multiply(multiply(X7,inverse(X7)),inverse(multiply(X5,X6))),X3))),
inference(backward_demodulation,[status(thm)],[f2343,f753]) ).
fof(f2278,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(inverse(multiply(X0,inverse(X0)))),inverse(inverse(X1)))),inverse(multiply(inverse(X2),inverse(X1)))) = X2,
inference(backward_demodulation,[status(thm)],[f2343,f1151]) ).
fof(f2337,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(X0,inverse(multiply(multiply(inverse(multiply(X1,X2)),inverse(multiply(inverse(inverse(X3)),X4))),multiply(X3,X0)))) = inverse(multiply(X5,multiply(multiply(multiply(X6,inverse(X6)),inverse(multiply(X2,X5))),multiply(multiply(X7,inverse(X7)),inverse(multiply(X4,X1)))))),
inference(backward_demodulation,[status(thm)],[f2343,f79]) ).
fof(f2339,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,multiply(X2,X0)))) = multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,inverse(inverse(X2))))),
inference(backward_demodulation,[status(thm)],[f2343,f77]) ).
fof(f2343,plain,
! [X0,X1] : inverse(inverse(X0)) = multiply(X0,multiply(X1,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f1959,f1786]) ).
fof(f2349,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(X0,inverse(multiply(inverse(inverse(multiply(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,X1))),multiply(X5,inverse(X5))),X6)),inverse(X6)))),multiply(X4,X0)))) = multiply(X7,inverse(X7)),
inference(forward_demodulation,[status(thm)],[f2343,f1791]) ).
fof(f2350,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,inverse(multiply(inverse(inverse(multiply(multiply(inverse(inverse(X1)),multiply(multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))),multiply(X4,inverse(X4))),X5)),inverse(X5)))),multiply(X3,X0)))) = multiply(X6,inverse(X6)),
inference(forward_demodulation,[status(thm)],[f2343,f2349]) ).
fof(f2351,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(inverse(inverse(multiply(multiply(inverse(inverse(X1)),multiply(inverse(inverse(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))))),X4)),inverse(X4)))),multiply(X3,X0)))) = multiply(X5,inverse(X5)),
inference(forward_demodulation,[status(thm)],[f2343,f2350]) ).
fof(f2352,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(X0,inverse(multiply(inverse(inverse(X1)),multiply(multiply(X2,inverse(X2)),X0)))) = multiply(multiply(multiply(multiply(X3,multiply(X4,inverse(X4))),multiply(multiply(multiply(multiply(X5,inverse(X5)),inverse(multiply(X1,X3))),multiply(X6,inverse(X6))),X7)),inverse(X7)),multiply(X8,inverse(X8))),
inference(forward_demodulation,[status(thm)],[f2343,f1792]) ).
fof(f2353,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(X0) = multiply(multiply(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,X1))),multiply(X4,inverse(X4))),X5)),inverse(X5)),multiply(X6,inverse(X6))),
inference(forward_demodulation,[status(thm)],[f263,f2352]) ).
fof(f2354,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(X0) = inverse(inverse(multiply(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,X1))),multiply(X4,inverse(X4))),X5)),inverse(X5)))),
inference(forward_demodulation,[status(thm)],[f2343,f2353]) ).
fof(f2355,plain,
! [X0,X1,X2,X3,X4] : inverse(X0) = inverse(inverse(multiply(multiply(inverse(inverse(X1)),multiply(multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X0,X1))),multiply(X3,inverse(X3))),X4)),inverse(X4)))),
inference(forward_demodulation,[status(thm)],[f2343,f2354]) ).
fof(f2356,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(inverse(X1),multiply(X1,X0)))) = multiply(X2,inverse(X2)),
inference(backward_demodulation,[status(thm)],[f2357,f2351]) ).
fof(f2357,plain,
! [X0,X1,X2,X3] : inverse(X0) = inverse(inverse(multiply(multiply(inverse(inverse(X1)),multiply(inverse(inverse(multiply(multiply(X2,inverse(X2)),inverse(multiply(X0,X1))))),X3)),inverse(X3)))),
inference(forward_demodulation,[status(thm)],[f2343,f2355]) ).
fof(f2398,plain,
! [X0,X1,X2] : inverse(inverse(X0)) = inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(multiply(X2,inverse(X2)),X0)))),
inference(forward_demodulation,[status(thm)],[f2343,f1823]) ).
fof(f2463,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(X0),inverse(inverse(inverse(multiply(X1,multiply(X2,inverse(X2))))))) = multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,X0))),multiply(X4,inverse(X4))),
inference(forward_demodulation,[status(thm)],[f2343,f1873]) ).
fof(f2464,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),inverse(inverse(inverse(inverse(inverse(X1)))))) = multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X1,X0))),multiply(X3,inverse(X3))),
inference(forward_demodulation,[status(thm)],[f2343,f2463]) ).
fof(f2475,plain,
! [X0,X1,X2] : multiply(inverse(X0),inverse(inverse(inverse(inverse(inverse(X1)))))) = inverse(inverse(multiply(multiply(X2,inverse(X2)),inverse(multiply(X1,X0))))),
inference(forward_demodulation,[status(thm)],[f2343,f2464]) ).
fof(f2480,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(inverse(inverse(X1)),multiply(X2,X0)))) = multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,X2))),multiply(X4,inverse(X4))),
inference(forward_demodulation,[status(thm)],[f2343,f1891]) ).
fof(f2481,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(inverse(X1)),multiply(X2,X0)))) = inverse(inverse(multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,X2))))),
inference(forward_demodulation,[status(thm)],[f2343,f2480]) ).
fof(f2487,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(inverse(inverse(X1)),multiply(X2,X0)))) = multiply(inverse(X2),inverse(inverse(inverse(inverse(inverse(X1)))))),
inference(forward_demodulation,[status(thm)],[f2475,f2481]) ).
fof(f2565,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f1676,f1964]) ).
fof(f2841,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(X0),inverse(inverse(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))),
inference(forward_demodulation,[status(thm)],[f2487,f2007]) ).
fof(f2842,plain,
! [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))),
inference(forward_demodulation,[status(thm)],[f2565,f2841]) ).
fof(f2843,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(X0),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))),
inference(forward_demodulation,[status(thm)],[f2565,f2842]) ).
fof(f2844,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(inverse(X0),inverse(multiply(multiply(X1,inverse(X1)),inverse(inverse(inverse(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X4))))))))) = inverse(multiply(multiply(X3,multiply(X5,inverse(X5))),multiply(X4,X0))),
inference(forward_demodulation,[status(thm)],[f2343,f2843]) ).
fof(f2845,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(inverse(X0),inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X4))))))) = inverse(multiply(multiply(X3,multiply(X5,inverse(X5))),multiply(X4,X0))),
inference(forward_demodulation,[status(thm)],[f2565,f2844]) ).
fof(f2846,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),inverse(inverse(inverse(multiply(X1,X2))))) = inverse(multiply(multiply(X1,multiply(X3,inverse(X3))),multiply(X2,X0))),
inference(forward_demodulation,[status(thm)],[f2398,f2845]) ).
fof(f2847,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),inverse(multiply(X1,X2))) = inverse(multiply(multiply(X1,multiply(X3,inverse(X3))),multiply(X2,X0))),
inference(forward_demodulation,[status(thm)],[f2565,f2846]) ).
fof(f2848,plain,
! [X0,X1,X2] : multiply(inverse(X0),inverse(multiply(X1,X2))) = inverse(multiply(inverse(inverse(X1)),multiply(X2,X0))),
inference(forward_demodulation,[status(thm)],[f2343,f2847]) ).
fof(f2879,plain,
! [X0,X1,X2] : multiply(inverse(X0),inverse(multiply(X1,X2))) = inverse(multiply(X1,multiply(X2,X0))),
inference(forward_demodulation,[status(thm)],[f2565,f2848]) ).
fof(f2995,plain,
! [X0,X1,X2,X3,X4] : multiply(multiply(X0,inverse(X0)),inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(multiply(X2,inverse(X2)),multiply(X3,multiply(X4,inverse(X4)))))))) = X3,
inference(forward_demodulation,[status(thm)],[f2565,f2024]) ).
fof(f2996,plain,
! [X0,X1,X2,X3] : multiply(multiply(multiply(X0,inverse(X0)),multiply(X1,multiply(X2,inverse(X2)))),inverse(multiply(X3,inverse(X3)))) = X1,
inference(forward_demodulation,[status(thm)],[f1899,f2995]) ).
fof(f2997,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(X0)),multiply(X1,multiply(X2,inverse(X2)))) = X1,
inference(forward_demodulation,[status(thm)],[f1959,f2996]) ).
fof(f2998,plain,
! [X0,X1] : multiply(multiply(X0,inverse(X0)),inverse(inverse(X1))) = X1,
inference(forward_demodulation,[status(thm)],[f2343,f2997]) ).
fof(f3050,plain,
! [X0,X1] : multiply(multiply(X0,inverse(X0)),X1) = X1,
inference(forward_demodulation,[status(thm)],[f2565,f2998]) ).
fof(f3070,plain,
! [X0,X1,X2,X3] : X0 = multiply(inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(X0,multiply(X2,multiply(X3,inverse(X3))))))),inverse(inverse(inverse(inverse(inverse(X2)))))),
inference(forward_demodulation,[status(thm)],[f2475,f2030]) ).
fof(f3071,plain,
! [X0,X1,X2] : X0 = multiply(inverse(inverse(multiply(X0,multiply(X1,multiply(X2,inverse(X2)))))),inverse(inverse(inverse(inverse(inverse(X1)))))),
inference(forward_demodulation,[status(thm)],[f3050,f3070]) ).
fof(f3072,plain,
! [X0,X1,X2] : X0 = multiply(multiply(X0,multiply(X1,multiply(X2,inverse(X2)))),inverse(inverse(inverse(inverse(inverse(X1)))))),
inference(forward_demodulation,[status(thm)],[f2565,f3071]) ).
fof(f3073,plain,
! [X0,X1] : X0 = multiply(multiply(X0,inverse(inverse(X1))),inverse(inverse(inverse(inverse(inverse(X1)))))),
inference(forward_demodulation,[status(thm)],[f2343,f3072]) ).
fof(f3074,plain,
! [X0,X1] : X0 = multiply(multiply(X0,X1),inverse(inverse(inverse(inverse(inverse(X1)))))),
inference(forward_demodulation,[status(thm)],[f2565,f3073]) ).
fof(f3075,plain,
! [X0,X1] : X0 = multiply(multiply(X0,X1),inverse(inverse(inverse(X1)))),
inference(forward_demodulation,[status(thm)],[f2565,f3074]) ).
fof(f3076,plain,
! [X0,X1] : X0 = multiply(multiply(X0,X1),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f2565,f3075]) ).
fof(f3088,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(multiply(X0,multiply(X1,inverse(X1))),multiply(X2,inverse(multiply(multiply(X3,multiply(X4,inverse(X4))),multiply(X5,X2)))))) = inverse(inverse(multiply(multiply(X6,inverse(X6)),inverse(multiply(X0,multiply(multiply(X7,inverse(X7)),inverse(multiply(X3,X5)))))))),
inference(forward_demodulation,[status(thm)],[f3050,f2032]) ).
fof(f3089,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(inverse(inverse(X0)),multiply(X1,inverse(multiply(multiply(X2,multiply(X3,inverse(X3))),multiply(X4,X1)))))) = inverse(inverse(multiply(multiply(X5,inverse(X5)),inverse(multiply(X0,multiply(multiply(X6,inverse(X6)),inverse(multiply(X2,X4)))))))),
inference(forward_demodulation,[status(thm)],[f2343,f3088]) ).
fof(f3090,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(X0,multiply(X1,inverse(multiply(multiply(X2,multiply(X3,inverse(X3))),multiply(X4,X1)))))) = inverse(inverse(multiply(multiply(X5,inverse(X5)),inverse(multiply(X0,multiply(multiply(X6,inverse(X6)),inverse(multiply(X2,X4)))))))),
inference(forward_demodulation,[status(thm)],[f2565,f3089]) ).
fof(f3091,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(multiply(X0,multiply(X1,inverse(multiply(inverse(inverse(X2)),multiply(X3,X1)))))) = inverse(inverse(multiply(multiply(X4,inverse(X4)),inverse(multiply(X0,multiply(multiply(X5,inverse(X5)),inverse(multiply(X2,X3)))))))),
inference(forward_demodulation,[status(thm)],[f2343,f3090]) ).
fof(f3092,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(X0,multiply(inverse(X1),inverse(inverse(inverse(inverse(inverse(X2)))))))) = inverse(inverse(multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,multiply(multiply(X4,inverse(X4)),inverse(multiply(X2,X1)))))))),
inference(forward_demodulation,[status(thm)],[f2487,f3091]) ).
fof(f3093,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(X0,multiply(inverse(X1),inverse(inverse(inverse(X2)))))) = inverse(inverse(multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,multiply(multiply(X4,inverse(X4)),inverse(multiply(X2,X1)))))))),
inference(forward_demodulation,[status(thm)],[f2565,f3092]) ).
fof(f3094,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(X0,multiply(inverse(X1),inverse(X2)))) = inverse(inverse(multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,multiply(multiply(X4,inverse(X4)),inverse(multiply(X2,X1)))))))),
inference(forward_demodulation,[status(thm)],[f2565,f3093]) ).
fof(f3095,plain,
! [X0,X1,X2,X3] : inverse(multiply(X0,multiply(inverse(X1),inverse(X2)))) = multiply(inverse(multiply(multiply(X3,inverse(X3)),inverse(multiply(X2,X1)))),inverse(inverse(inverse(inverse(inverse(X0)))))),
inference(forward_demodulation,[status(thm)],[f2475,f3094]) ).
fof(f3096,plain,
! [X0,X1,X2] : inverse(multiply(X0,multiply(inverse(X1),inverse(X2)))) = multiply(inverse(inverse(multiply(X2,X1))),inverse(inverse(inverse(inverse(inverse(X0)))))),
inference(forward_demodulation,[status(thm)],[f3050,f3095]) ).
fof(f3097,plain,
! [X0,X1,X2] : inverse(multiply(X0,multiply(inverse(X1),inverse(X2)))) = multiply(multiply(X2,X1),inverse(inverse(inverse(inverse(inverse(X0)))))),
inference(forward_demodulation,[status(thm)],[f2565,f3096]) ).
fof(f3098,plain,
! [X0,X1,X2] : inverse(multiply(X0,multiply(inverse(X1),inverse(X2)))) = multiply(multiply(X2,X1),inverse(inverse(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f2565,f3097]) ).
fof(f3100,plain,
! [X0,X1,X2] : inverse(multiply(X0,multiply(inverse(X1),inverse(X2)))) = multiply(multiply(X2,X1),inverse(X0)),
inference(forward_demodulation,[status(thm)],[f2565,f3098]) ).
fof(f3184,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(multiply(multiply(X0,multiply(X1,inverse(X1))),multiply(X2,multiply(inverse(X2),inverse(multiply(inverse(X3),multiply(X4,inverse(X4)))))))) = inverse(inverse(multiply(multiply(X5,inverse(X5)),inverse(multiply(X0,X3))))),
inference(forward_demodulation,[status(thm)],[f2879,f2042]) ).
fof(f3185,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(inverse(X0)),multiply(X1,multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(X3,inverse(X3)))))))) = inverse(inverse(multiply(multiply(X4,inverse(X4)),inverse(multiply(X0,X2))))),
inference(forward_demodulation,[status(thm)],[f2343,f3184]) ).
fof(f3186,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(X0,multiply(X1,multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(X3,inverse(X3)))))))) = inverse(inverse(multiply(multiply(X4,inverse(X4)),inverse(multiply(X0,X2))))),
inference(forward_demodulation,[status(thm)],[f2565,f3185]) ).
fof(f3187,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(X0,multiply(X1,inverse(multiply(inverse(X2),multiply(multiply(X3,inverse(X3)),X1)))))) = inverse(inverse(multiply(multiply(X4,inverse(X4)),inverse(multiply(X0,X2))))),
inference(forward_demodulation,[status(thm)],[f2879,f3186]) ).
fof(f3188,plain,
! [X0,X1,X2] : inverse(multiply(X0,X1)) = inverse(inverse(multiply(multiply(X2,inverse(X2)),inverse(multiply(X0,X1))))),
inference(forward_demodulation,[status(thm)],[f263,f3187]) ).
fof(f3189,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = multiply(inverse(X1),inverse(inverse(inverse(inverse(inverse(X0)))))),
inference(forward_demodulation,[status(thm)],[f2475,f3188]) ).
fof(f3190,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = multiply(inverse(X1),inverse(inverse(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f2565,f3189]) ).
fof(f3202,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = multiply(inverse(X1),inverse(X0)),
inference(forward_demodulation,[status(thm)],[f2565,f3190]) ).
fof(f3392,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(inverse(inverse(multiply(X0,inverse(X0)))),multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(X3,multiply(X4,inverse(X4))),multiply(inverse(inverse(multiply(multiply(X5,inverse(X5)),inverse(multiply(X1,X3))))),X6))))) = inverse(X6),
inference(forward_demodulation,[status(thm)],[f2879,f2066]) ).
fof(f3393,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(multiply(X0,inverse(X0)),multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(X3,multiply(X4,inverse(X4))),multiply(inverse(inverse(multiply(multiply(X5,inverse(X5)),inverse(multiply(X1,X3))))),X6))))) = inverse(X6),
inference(forward_demodulation,[status(thm)],[f2565,f3392]) ).
fof(f3394,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(multiply(multiply(X0,multiply(X1,inverse(X1))),multiply(multiply(X2,multiply(X3,inverse(X3))),multiply(inverse(inverse(multiply(multiply(X4,inverse(X4)),inverse(multiply(X0,X2))))),X5)))) = inverse(X5),
inference(forward_demodulation,[status(thm)],[f3050,f3393]) ).
fof(f3395,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(inverse(X0)),multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(inverse(inverse(multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,X1))))),X4)))) = inverse(X4),
inference(forward_demodulation,[status(thm)],[f2343,f3394]) ).
fof(f3396,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(X0,multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(inverse(inverse(multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,X1))))),X4)))) = inverse(X4),
inference(forward_demodulation,[status(thm)],[f2565,f3395]) ).
fof(f3397,plain,
! [X0,X1,X2,X3] : inverse(multiply(X0,multiply(inverse(inverse(X1)),multiply(inverse(inverse(multiply(multiply(X2,inverse(X2)),inverse(multiply(X0,X1))))),X3)))) = inverse(X3),
inference(forward_demodulation,[status(thm)],[f2343,f3396]) ).
fof(f3398,plain,
! [X0,X1,X2,X3] : inverse(multiply(X0,multiply(X1,multiply(inverse(inverse(multiply(multiply(X2,inverse(X2)),inverse(multiply(X0,X1))))),X3)))) = inverse(X3),
inference(forward_demodulation,[status(thm)],[f2565,f3397]) ).
fof(f3399,plain,
! [X0,X1,X2] : inverse(multiply(X0,multiply(X1,multiply(multiply(inverse(X1),inverse(inverse(inverse(inverse(inverse(X0)))))),X2)))) = inverse(X2),
inference(forward_demodulation,[status(thm)],[f2475,f3398]) ).
fof(f3400,plain,
! [X0,X1,X2] : inverse(multiply(X0,multiply(X1,multiply(inverse(multiply(inverse(inverse(inverse(inverse(X0)))),X1)),X2)))) = inverse(X2),
inference(forward_demodulation,[status(thm)],[f3202,f3399]) ).
fof(f3401,plain,
! [X0,X1,X2] : inverse(multiply(X0,multiply(X1,multiply(inverse(multiply(inverse(inverse(X0)),X1)),X2)))) = inverse(X2),
inference(forward_demodulation,[status(thm)],[f2565,f3400]) ).
fof(f3402,plain,
! [X0,X1,X2] : inverse(multiply(X0,multiply(X1,multiply(inverse(multiply(X0,X1)),X2)))) = inverse(X2),
inference(forward_demodulation,[status(thm)],[f2565,f3401]) ).
fof(f3683,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(X0,inverse(multiply(inverse(inverse(inverse(multiply(inverse(inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))))),multiply(X2,X4))))),multiply(multiply(multiply(multiply(X5,inverse(X5)),inverse(X3)),multiply(X6,inverse(X6))),X0)))) = multiply(X4,multiply(X7,inverse(X7))),
inference(forward_demodulation,[status(thm)],[f2343,f2091]) ).
fof(f3684,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(X1)),multiply(X2,inverse(X2)))),inverse(inverse(inverse(inverse(inverse(inverse(multiply(inverse(inverse(multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,X1))))),multiply(X4,X5))))))))) = multiply(X5,multiply(X6,inverse(X6))),
inference(forward_demodulation,[status(thm)],[f2487,f3683]) ).
fof(f3685,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(inverse(inverse(inverse(inverse(inverse(multiply(inverse(inverse(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,X2))))),multiply(X1,X3))))))),multiply(multiply(multiply(X4,inverse(X4)),inverse(X2)),multiply(X5,inverse(X5))))) = multiply(X3,multiply(X6,inverse(X6))),
inference(forward_demodulation,[status(thm)],[f3202,f3684]) ).
fof(f3686,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(inverse(inverse(inverse(multiply(inverse(inverse(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,X2))))),multiply(X1,X3))))),multiply(multiply(multiply(X4,inverse(X4)),inverse(X2)),multiply(X5,inverse(X5))))) = multiply(X3,multiply(X6,inverse(X6))),
inference(forward_demodulation,[status(thm)],[f2565,f3685]) ).
fof(f3687,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(inverse(multiply(inverse(inverse(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,X2))))),multiply(X1,X3))),multiply(multiply(multiply(X4,inverse(X4)),inverse(X2)),multiply(X5,inverse(X5))))) = multiply(X3,multiply(X6,inverse(X6))),
inference(forward_demodulation,[status(thm)],[f2565,f3686]) ).
fof(f3688,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(multiply(inverse(multiply(multiply(inverse(X0),inverse(inverse(inverse(inverse(inverse(X1)))))),multiply(X1,X2))),multiply(multiply(multiply(X3,inverse(X3)),inverse(X0)),multiply(X4,inverse(X4))))) = multiply(X2,multiply(X5,inverse(X5))),
inference(forward_demodulation,[status(thm)],[f2475,f3687]) ).
fof(f3689,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(inverse(inverse(X0)))),X1)),multiply(X0,X2))),multiply(multiply(multiply(X3,inverse(X3)),inverse(X1)),multiply(X4,inverse(X4))))) = multiply(X2,multiply(X5,inverse(X5))),
inference(forward_demodulation,[status(thm)],[f3202,f3688]) ).
fof(f3690,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),X1)),multiply(X0,X2))),multiply(multiply(multiply(X3,inverse(X3)),inverse(X1)),multiply(X4,inverse(X4))))) = multiply(X2,multiply(X5,inverse(X5))),
inference(forward_demodulation,[status(thm)],[f2565,f3689]) ).
fof(f3691,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),multiply(multiply(multiply(X3,inverse(X3)),inverse(X1)),multiply(X4,inverse(X4))))) = multiply(X2,multiply(X5,inverse(X5))),
inference(forward_demodulation,[status(thm)],[f2565,f3690]) ).
fof(f3692,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),inverse(inverse(multiply(multiply(X3,inverse(X3)),inverse(X1)))))) = multiply(X2,multiply(X4,inverse(X4))),
inference(forward_demodulation,[status(thm)],[f2343,f3691]) ).
fof(f3693,plain,
! [X0,X1,X2,X3,X4] : inverse(inverse(multiply(inverse(multiply(multiply(X0,inverse(X0)),inverse(X1))),multiply(inverse(multiply(X2,X1)),multiply(X2,X3))))) = multiply(X3,multiply(X4,inverse(X4))),
inference(forward_demodulation,[status(thm)],[f3202,f3692]) ).
fof(f3694,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(multiply(X0,inverse(X0)),inverse(X1))),multiply(inverse(multiply(X2,X1)),multiply(X2,X3))) = multiply(X3,multiply(X4,inverse(X4))),
inference(forward_demodulation,[status(thm)],[f2565,f3693]) ).
fof(f3695,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(X0)),multiply(inverse(multiply(X1,X0)),multiply(X1,X2))) = multiply(X2,multiply(X3,inverse(X3))),
inference(forward_demodulation,[status(thm)],[f3050,f3694]) ).
fof(f3696,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(inverse(multiply(X1,X0)),multiply(X1,X2))) = multiply(X2,multiply(X3,inverse(X3))),
inference(forward_demodulation,[status(thm)],[f2565,f3695]) ).
fof(f3697,plain,
! [X0,X1,X2] : multiply(X0,multiply(inverse(multiply(X1,X0)),multiply(X1,X2))) = inverse(inverse(X2)),
inference(forward_demodulation,[status(thm)],[f2343,f3696]) ).
fof(f3698,plain,
! [X0,X1,X2] : multiply(X0,multiply(inverse(multiply(X1,X0)),multiply(X1,X2))) = X2,
inference(forward_demodulation,[status(thm)],[f2565,f3697]) ).
fof(f4284,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),inverse(inverse(inverse(inverse(inverse(multiply(multiply(X1,inverse(X1)),inverse(X2)))))))) = inverse(multiply(inverse(X2),inverse(multiply(inverse(X0),multiply(X3,inverse(X3)))))),
inference(forward_demodulation,[status(thm)],[f2487,f2151]) ).
fof(f4285,plain,
! [X0,X1,X2,X3] : inverse(multiply(inverse(inverse(inverse(inverse(multiply(multiply(X0,inverse(X0)),inverse(X1)))))),X2)) = inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(X3,inverse(X3)))))),
inference(forward_demodulation,[status(thm)],[f3202,f4284]) ).
fof(f4286,plain,
! [X0,X1,X2,X3] : inverse(multiply(inverse(inverse(multiply(multiply(X0,inverse(X0)),inverse(X1)))),X2)) = inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(X3,inverse(X3)))))),
inference(forward_demodulation,[status(thm)],[f2565,f4285]) ).
fof(f4287,plain,
! [X0,X1,X2,X3] : inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(X1)),X2)) = inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(X3,inverse(X3)))))),
inference(forward_demodulation,[status(thm)],[f2565,f4286]) ).
fof(f4288,plain,
! [X0,X1,X2] : inverse(multiply(inverse(X0),X1)) = inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),multiply(X2,inverse(X2)))))),
inference(forward_demodulation,[status(thm)],[f3050,f4287]) ).
fof(f4289,plain,
! [X0,X1,X2] : inverse(multiply(inverse(X0),X1)) = inverse(inverse(multiply(inverse(X1),multiply(multiply(X2,inverse(X2)),X0)))),
inference(forward_demodulation,[status(thm)],[f2879,f4288]) ).
fof(f4290,plain,
! [X0,X1,X2] : inverse(multiply(inverse(X0),X1)) = multiply(inverse(X1),multiply(multiply(X2,inverse(X2)),X0)),
inference(forward_demodulation,[status(thm)],[f2565,f4289]) ).
fof(f4299,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X1)) = multiply(inverse(X1),X0),
inference(forward_demodulation,[status(thm)],[f3050,f4290]) ).
fof(f4540,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(inverse(inverse(multiply(multiply(X0,inverse(X0)),inverse(X1)))),multiply(X2,multiply(X3,multiply(multiply(multiply(X4,inverse(X4)),inverse(multiply(X2,X3))),X5))))) = inverse(multiply(X6,multiply(multiply(multiply(X7,inverse(X7)),inverse(multiply(X1,X6))),X5))),
inference(forward_demodulation,[status(thm)],[f2879,f2175]) ).
fof(f4541,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X0,X1))),X3)))),inverse(multiply(multiply(X4,inverse(X4)),inverse(X5)))) = inverse(multiply(X6,multiply(multiply(multiply(X7,inverse(X7)),inverse(multiply(X5,X6))),X3))),
inference(forward_demodulation,[status(thm)],[f4299,f4540]) ).
fof(f4542,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(multiply(X0,inverse(X0)),multiply(inverse(X1),multiply(X2,multiply(X3,multiply(multiply(multiply(X4,inverse(X4)),inverse(multiply(X2,X3))),X5)))))) = inverse(multiply(X6,multiply(multiply(multiply(X7,inverse(X7)),inverse(multiply(X1,X6))),X5))),
inference(forward_demodulation,[status(thm)],[f2879,f4541]) ).
fof(f4543,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(inverse(X0),multiply(X1,multiply(X2,multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,X2))),X4))))) = inverse(multiply(X5,multiply(multiply(multiply(X6,inverse(X6)),inverse(multiply(X0,X5))),X4))),
inference(forward_demodulation,[status(thm)],[f3050,f4542]) ).
fof(f4544,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X0,X1))),X3)))),X4) = inverse(multiply(X5,multiply(multiply(multiply(X6,inverse(X6)),inverse(multiply(X4,X5))),X3))),
inference(forward_demodulation,[status(thm)],[f4299,f4543]) ).
fof(f4545,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(X0,multiply(X1,multiply(inverse(multiply(X0,X1)),X2)))),X3) = inverse(multiply(X4,multiply(multiply(multiply(X5,inverse(X5)),inverse(multiply(X3,X4))),X2))),
inference(forward_demodulation,[status(thm)],[f3050,f4544]) ).
fof(f4546,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),X1) = inverse(multiply(X2,multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X1,X2))),X0))),
inference(forward_demodulation,[status(thm)],[f3402,f4545]) ).
fof(f4549,plain,
! [X0,X1,X2] : multiply(inverse(X0),X1) = inverse(multiply(X2,multiply(inverse(multiply(X1,X2)),X0))),
inference(forward_demodulation,[status(thm)],[f3050,f4546]) ).
fof(f5190,plain,
! [X0,X1,X2] : inverse(multiply(inverse(X0),multiply(inverse(X1),multiply(inverse(inverse(multiply(X2,inverse(X2)))),inverse(inverse(X1)))))) = X0,
inference(forward_demodulation,[status(thm)],[f2879,f2278]) ).
fof(f5191,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(inverse(X0))))),X2) = X2,
inference(forward_demodulation,[status(thm)],[f4299,f5190]) ).
fof(f5192,plain,
! [X0,X1,X2] : multiply(multiply(inverse(multiply(inverse(inverse(multiply(X0,inverse(X0)))),inverse(inverse(X1)))),X1),X2) = X2,
inference(forward_demodulation,[status(thm)],[f4299,f5191]) ).
fof(f5193,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(inverse(inverse(X0))),inverse(multiply(X1,inverse(X1)))),X0),X2) = X2,
inference(forward_demodulation,[status(thm)],[f4299,f5192]) ).
fof(f5194,plain,
! [X0,X1,X2] : multiply(multiply(inverse(multiply(X0,multiply(inverse(X0),inverse(inverse(X1))))),X1),X2) = X2,
inference(forward_demodulation,[status(thm)],[f2879,f5193]) ).
fof(f5195,plain,
! [X0,X1,X2] : multiply(multiply(multiply(multiply(inverse(X0),X1),inverse(X1)),X0),X2) = X2,
inference(forward_demodulation,[status(thm)],[f3100,f5194]) ).
fof(f5196,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(backward_demodulation,[status(thm)],[f5197,f4]) ).
fof(f5197,plain,
! [X0,X1] : multiply(multiply(inverse(X0),X0),X1) = X1,
inference(forward_demodulation,[status(thm)],[f3076,f5195]) ).
fof(f5649,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(X0,inverse(multiply(inverse(multiply(inverse(inverse(X1)),multiply(X2,multiply(X3,X4)))),multiply(X1,X0)))) = inverse(multiply(X5,multiply(multiply(multiply(X6,inverse(X6)),inverse(multiply(X4,X5))),multiply(multiply(X7,inverse(X7)),inverse(multiply(X2,X3)))))),
inference(forward_demodulation,[status(thm)],[f2879,f2337]) ).
fof(f5650,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(X0,multiply(inverse(multiply(X1,X0)),multiply(inverse(inverse(X1)),multiply(X2,multiply(X3,X4))))) = inverse(multiply(X5,multiply(multiply(multiply(X6,inverse(X6)),inverse(multiply(X4,X5))),multiply(multiply(X7,inverse(X7)),inverse(multiply(X2,X3)))))),
inference(forward_demodulation,[status(thm)],[f4299,f5649]) ).
fof(f5651,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(X0,multiply(inverse(multiply(X1,X0)),multiply(X1,multiply(X2,multiply(X3,X4))))) = inverse(multiply(X5,multiply(multiply(multiply(X6,inverse(X6)),inverse(multiply(X4,X5))),multiply(multiply(X7,inverse(X7)),inverse(multiply(X2,X3)))))),
inference(forward_demodulation,[status(thm)],[f2565,f5650]) ).
fof(f5652,plain,
! [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)))))),
inference(forward_demodulation,[status(thm)],[f3698,f5651]) ).
fof(f5653,plain,
! [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)))))),
inference(forward_demodulation,[status(thm)],[f3050,f5652]) ).
fof(f5654,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(X1,X2)) = multiply(inverse(multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,X1)))),X2),
inference(forward_demodulation,[status(thm)],[f4549,f5653]) ).
fof(f5655,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(inverse(inverse(multiply(X0,X1))),X2),
inference(forward_demodulation,[status(thm)],[f3050,f5654]) ).
fof(f5656,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X0,X1),X2),
inference(forward_demodulation,[status(thm)],[f2565,f5655]) ).
fof(f5663,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(X1,multiply(X2,X0)))) = multiply(inverse(X2),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f1899,f2339]) ).
fof(f5667,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(X1,multiply(X2,X0)))) = inverse(multiply(X1,X2)),
inference(forward_demodulation,[status(thm)],[f3202,f5663]) ).
fof(f5689,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X0)) = multiply(X1,inverse(X1)),
inference(forward_demodulation,[status(thm)],[f5667,f2356]) ).
fof(f5690,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(X1,inverse(X1)),
inference(forward_demodulation,[status(thm)],[f4299,f5689]) ).
fof(f6418,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(trivial_equality_resolution,[status(thm)],[f5196]) ).
fof(f6419,plain,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
inference(forward_subsumption_resolution,[status(thm)],[f6418,f5656]) ).
fof(f6445,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(paramodulation,[status(thm)],[f5690,f5690]) ).
fof(f6456,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f6419,f6445]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP058-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.55 % Computer : n002.cluster.edu
% 0.10/5.55 % Model : x86_64 x86_64
% 0.10/5.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.55 % Memory : 8046.5625MB
% 0.10/5.55 % OS : Linux 6.8.0-71-generic
% 0.10/5.55 % CPULimit : 300
% 0.10/5.55 % WCLimit : 300
% 0.10/5.55 % DateTime : Sun Sep 20 19:59:09 UTC 2026
% 0.10/5.55 % CPUTime :
% 0.10/5.56 % Drodi V4.1.1
% 47.17/12.06 % Refutation found
% 47.17/12.06 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 47.17/12.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 20.93/12.20 % Elapsed time: 6.630045 seconds
% 20.93/12.20 % CPU time: 51.957815 seconds
% 20.93/12.20 % Total memory used: 361.232 MB
% 20.93/12.20 % Net memory used: 358.248 MB
%------------------------------------------------------------------------------