%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP057-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 : 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:32:24 PM UTC 2026
% Result : Unsatisfiable 227.22s 29.24s
% Output : CNFRefutation 227.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 5
% Syntax : Number of formulae : 236 ( 221 unt; 3 def)
% Number of atoms : 254 ( 232 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 33 ( 15 ~; 15 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 33 ( 4 avg)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 980 ( 980 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,Z,U] : multiply(X,inverse(multiply(multiply(inverse(multiply(inverse(Y),multiply(inverse(X),Z))),U),inverse(multiply(Y,U))))) = Z,
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(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),X3),inverse(multiply(X1,X3))))) = X2,
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,definition,
( sQ0_spl
<=> multiply(inverse(a1),a1) = multiply(inverse(b1),b1) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f7,plain,
( sQ0_spl
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(component_clause,[status(thm)],[f5]) ).
fof(f8,definition,
( sQ1_spl
<=> multiply(multiply(inverse(b2),b2),a2) = a2 ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f10,plain,
( sQ1_spl
| multiply(multiply(inverse(b2),b2),a2) != a2 ),
inference(component_clause,[status(thm)],[f8]) ).
fof(f11,definition,
( sQ2_spl
<=> multiply(multiply(a3,b3),c3) = multiply(a3,multiply(b3,c3)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f13,plain,
( sQ2_spl
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
inference(component_clause,[status(thm)],[f11]) ).
fof(f14,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f4,f5,f8,f11]) ).
fof(f15,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(inverse(multiply(inverse(X2),multiply(inverse(X0),X4)))),X1))),X5),inverse(multiply(X3,X5))))))))) = X4,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f16,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X2))),X5),inverse(multiply(X4,X5)))),
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f19,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(multiply(inverse(multiply(inverse(X7),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(multiply(inverse(X2),multiply(inverse(X0),X8)))),X1)))),X3)))),X5))),X9),inverse(multiply(X7,X9))))))))))))))))) = X8,
inference(paramodulation,[status(thm)],[f15,f15]) ).
fof(f29,plain,
! [X0,X1,X2,X3] : X0 = inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(inverse(X2)),multiply(inverse(X2),X0)))),X3),inverse(multiply(X1,X3)))),
inference(paramodulation,[status(thm)],[f3,f16]) ).
fof(f70,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3)))))) = X2,
inference(paramodulation,[status(thm)],[f16,f3]) ).
fof(f82,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(X0),multiply(X0,inverse(inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X3)),X4)),X5)),inverse(multiply(X2,X4))))),X3))),X6),inverse(multiply(X1,X6))))))) = X5,
inference(paramodulation,[status(thm)],[f16,f70]) ).
fof(f124,plain,
! [X0,X1,X2,X3,X4,X5,X6] : X0 = inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X2),multiply(inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(inverse(X4)),multiply(inverse(X4),X2)))),X5),inverse(multiply(X3,X5)))),X0)))),X6),inverse(multiply(X1,X6)))),
inference(paramodulation,[status(thm)],[f29,f29]) ).
fof(f141,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,X1)) = multiply(inverse(inverse(X2)),multiply(inverse(X2),X1)),
inference(paramodulation,[status(thm)],[f29,f70]) ).
fof(f159,plain,
! [X0,X1,X2,X3] : X0 = inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X2),multiply(X2,X0)))),X3),inverse(multiply(X1,X3)))),
inference(forward_demodulation,[status(thm)],[f29,f124]) ).
fof(f221,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,X1)) = multiply(inverse(X2),multiply(X2,X1)),
inference(paramodulation,[status(thm)],[f141,f141]) ).
fof(f267,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X3),inverse(multiply(inverse(X0),X3))))) = X2,
inference(paramodulation,[status(thm)],[f141,f3]) ).
fof(f299,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,X2))) = multiply(inverse(X3),multiply(X3,multiply(X0,X2))),
inference(paramodulation,[status(thm)],[f221,f221]) ).
fof(f321,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X1,X2)),inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(X0),X4)),X2)))))) = X4,
inference(paramodulation,[status(thm)],[f221,f3]) ).
fof(f322,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X1,X2)),inverse(multiply(X3,multiply(multiply(inverse(X3),X4),X2))))))) = X4,
inference(paramodulation,[status(thm)],[f221,f70]) ).
fof(f333,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X3),inverse(multiply(X4,X3)))))) = multiply(X4,X2),
inference(paramodulation,[status(thm)],[f221,f70]) ).
fof(f415,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,X2))) = multiply(inverse(inverse(X0)),multiply(inverse(X3),multiply(X3,X2))),
inference(paramodulation,[status(thm)],[f299,f299]) ).
fof(f512,plain,
! [X0,X1,X2,X3,X4] : X0 = inverse(multiply(multiply(inverse(X1),multiply(X1,X2)),inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(X4),multiply(X4,X0))),X2))))),
inference(paramodulation,[status(thm)],[f221,f159]) ).
fof(f619,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X1,X2)),inverse(multiply(inverse(X0),multiply(multiply(inverse(X3),multiply(X3,X4)),X2)))))) = X4,
inference(paramodulation,[status(thm)],[f221,f267]) ).
fof(f767,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(X0),multiply(inverse(X1),multiply(X1,X2))) = multiply(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X4),multiply(X4,X0)))),X5),inverse(multiply(X3,X5))))),multiply(inverse(X6),multiply(X6,X2))),
inference(paramodulation,[status(thm)],[f159,f415]) ).
fof(f892,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(inverse(X1),multiply(X1,X2))) = multiply(inverse(X0),multiply(inverse(X3),multiply(X3,X2))),
inference(forward_demodulation,[status(thm)],[f159,f767]) ).
fof(f927,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,multiply(inverse(X1),multiply(X1,X2))) = multiply(inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X4),multiply(X4,X0)))),X5),inverse(multiply(X3,X5)))),multiply(inverse(X6),multiply(X6,X2))),
inference(paramodulation,[status(thm)],[f159,f892]) ).
fof(f1068,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(inverse(X1),multiply(X1,X2))) = multiply(X0,multiply(inverse(X3),multiply(X3,X2))),
inference(forward_demodulation,[status(thm)],[f159,f927]) ).
fof(f1193,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(X0,multiply(inverse(X1),multiply(X1,X2)))) = multiply(inverse(X3),multiply(X3,multiply(inverse(X4),multiply(X4,X2)))),
inference(paramodulation,[status(thm)],[f1068,f221]) ).
fof(f1864,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(multiply(inverse(X3),multiply(X3,X4)),inverse(multiply(X5,multiply(multiply(inverse(X5),multiply(inverse(X1),X6)),X4)))))),inverse(X6))))) = X2,
inference(paramodulation,[status(thm)],[f321,f70]) ).
fof(f2303,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(X3,X2)))))) = inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(X8,inverse(multiply(X9,inverse(multiply(multiply(inverse(multiply(inverse(X10),multiply(inverse(inverse(multiply(inverse(X9),multiply(inverse(inverse(multiply(inverse(X7),multiply(inverse(inverse(multiply(inverse(X5),multiply(inverse(inverse(X3)),X1)))),X4)))),X6)))),X8))),X11),inverse(multiply(X10,X11)))))))))))))))),
inference(paramodulation,[status(thm)],[f19,f70]) ).
fof(f2454,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X1,X2)),inverse(multiply(X3,multiply(multiply(inverse(X4),multiply(X4,X5)),X2))))))) = multiply(X3,X5),
inference(paramodulation,[status(thm)],[f221,f322]) ).
fof(f2585,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(inverse(X0),multiply(X0,inverse(inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(multiply(inverse(X2),multiply(X2,X3))),inverse(multiply(X4,X5))))),X6))),X7),inverse(multiply(X1,X7))))))) = multiply(multiply(inverse(multiply(inverse(X4),X6)),X5),X3),
inference(paramodulation,[status(thm)],[f16,f333]) ).
fof(f2626,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(inverse(X1)),X2)),X3),inverse(multiply(X4,X3)))))) = multiply(X4,multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X5),X2)),X6),inverse(multiply(X5,X6)))))),
inference(paramodulation,[status(thm)],[f70,f333]) ).
fof(f3413,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(multiply(inverse(X2),multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(X3),X4)),X5),inverse(multiply(X3,X5)))))),inverse(X4)))) = X1,
inference(paramodulation,[status(thm)],[f70,f619]) ).
fof(f3489,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(multiply(inverse(X6),multiply(X6,X7)),inverse(multiply(inverse(inverse(multiply(inverse(X5),multiply(inverse(inverse(X0)),X2)))),multiply(multiply(inverse(X8),multiply(X8,X4)),X7))))))))),
inference(paramodulation,[status(thm)],[f619,f16]) ).
fof(f3504,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(X3,X2))))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),inverse(multiply(multiply(inverse(X5),multiply(X5,X6)),inverse(multiply(inverse(inverse(X3)),multiply(multiply(inverse(X7),multiply(X7,X1)),X6)))))))),X8),inverse(multiply(X4,X8)))),
inference(paramodulation,[status(thm)],[f619,f16]) ).
fof(f3505,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(inverse(multiply(inverse(X2),X4))),X1))),X5),inverse(multiply(X3,X5))))))))) = inverse(multiply(multiply(inverse(X6),multiply(X6,X7)),inverse(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X8),multiply(X8,X4)),X7))))),
inference(paramodulation,[status(thm)],[f619,f15]) ).
fof(f3522,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X4,X3)))))) = multiply(X4,inverse(multiply(multiply(inverse(X5),multiply(X5,X6)),inverse(multiply(inverse(X1),multiply(multiply(inverse(X7),multiply(X7,X2)),X6)))))),
inference(paramodulation,[status(thm)],[f619,f333]) ).
fof(f3536,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(inverse(X2),multiply(multiply(inverse(X3),multiply(X3,X4)),X1))))) = inverse(multiply(multiply(inverse(multiply(inverse(X5),multiply(inverse(X2),X4))),X6),inverse(multiply(X5,X6)))),
inference(paramodulation,[status(thm)],[f619,f159]) ).
fof(f3549,plain,
! [X0,X1,X2] : multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(X2,inverse(X2)))) = X1,
inference(forward_demodulation,[status(thm)],[f70,f3413]) ).
fof(f3632,plain,
! [X0,X1,X2,X3] : X0 = inverse(multiply(multiply(inverse(X1),multiply(X1,inverse(multiply(X2,inverse(X2))))),inverse(multiply(inverse(X3),multiply(X3,X0))))),
inference(paramodulation,[status(thm)],[f3549,f512]) ).
fof(f3637,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(X0),multiply(X0,X1))),X1) = multiply(inverse(multiply(inverse(X2),multiply(X2,X3))),X3),
inference(paramodulation,[status(thm)],[f3549,f333]) ).
fof(f3647,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X2),inverse(multiply(X3,multiply(multiply(inverse(X3),X4),inverse(multiply(X5,inverse(X5)))))))))) = X4,
inference(paramodulation,[status(thm)],[f3549,f322]) ).
fof(f3662,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(inverse(X0)),multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X2)) = multiply(inverse(X3),multiply(X3,multiply(X0,inverse(multiply(X4,inverse(X4)))))),
inference(paramodulation,[status(thm)],[f3549,f299]) ).
fof(f3797,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(X4,X5))),X5),inverse(multiply(inverse(inverse(X0)),X2)))),
inference(paramodulation,[status(thm)],[f3637,f16]) ).
fof(f3801,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X2),inverse(multiply(X3,X4)))))) = multiply(X3,X4),
inference(paramodulation,[status(thm)],[f3637,f333]) ).
fof(f3843,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(inverse(multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X3),inverse(multiply(X4,X3)))))))),multiply(inverse(multiply(inverse(X5),multiply(X5,X6))),X6)) = multiply(X4,X2),
inference(paramodulation,[status(thm)],[f3637,f333]) ).
fof(f3968,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(inverse(X0),X1),inverse(multiply(X2,inverse(X2))))) = X1,
inference(backward_demodulation,[status(thm)],[f3801,f3647]) ).
fof(f3974,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(multiply(X0,X1))),multiply(inverse(multiply(inverse(X2),multiply(X2,X3))),X3)) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f333,f3843]) ).
fof(f4177,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(inverse(X0)),multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X2)) = multiply(multiply(inverse(X3),multiply(X3,X0)),inverse(multiply(X4,inverse(X4)))),
inference(paramodulation,[status(thm)],[f3549,f3974]) ).
fof(f4355,plain,
! [X0,X1,X2] : X0 = multiply(inverse(X1),multiply(X1,multiply(X0,inverse(multiply(X2,inverse(X2)))))),
inference(backward_demodulation,[status(thm)],[f4357,f3662]) ).
fof(f4357,plain,
! [X0,X1,X2] : multiply(inverse(inverse(X0)),multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X2)) = X0,
inference(forward_demodulation,[status(thm)],[f3549,f4177]) ).
fof(f4423,plain,
! [X0,X1,X2,X3,X4,X5] : X0 = multiply(inverse(X1),multiply(X1,multiply(X0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(X3),multiply(X3,X4)))),X5),inverse(multiply(X2,X5))),X4))))),
inference(paramodulation,[status(thm)],[f159,f4355]) ).
fof(f4466,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(X1,inverse(X1)))) = multiply(X0,inverse(multiply(X2,inverse(X2)))),
inference(paramodulation,[status(thm)],[f4355,f3549]) ).
fof(f4483,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(X0)),X1) = multiply(inverse(X2),multiply(X2,multiply(X0,multiply(X1,inverse(multiply(X3,inverse(X3))))))),
inference(paramodulation,[status(thm)],[f4355,f299]) ).
fof(f4499,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(X0,multiply(inverse(X1),multiply(X1,inverse(multiply(X2,inverse(X2))))))) = multiply(inverse(inverse(inverse(X3))),X3),
inference(paramodulation,[status(thm)],[f4355,f1193]) ).
fof(f4555,plain,
! [X0,X1] : multiply(inverse(inverse(inverse(X0))),X0) = multiply(inverse(inverse(inverse(X1))),X1),
inference(forward_demodulation,[status(thm)],[f4483,f4499]) ).
fof(f4627,plain,
! [X0,X1,X2] : X0 = multiply(inverse(inverse(inverse(inverse(multiply(X0,inverse(multiply(X1,inverse(X1)))))))),multiply(inverse(inverse(inverse(X2))),X2)),
inference(paramodulation,[status(thm)],[f4555,f4355]) ).
fof(f4634,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),X2),inverse(multiply(X0,X2)))))))),multiply(inverse(inverse(inverse(X3))),X3)) = X1,
inference(paramodulation,[status(thm)],[f4555,f70]) ).
fof(f4647,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X3),inverse(multiply(inverse(inverse(inverse(X4))),X4)))))) = multiply(inverse(inverse(inverse(X3))),X2),
inference(paramodulation,[status(thm)],[f4555,f333]) ).
fof(f4652,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(inverse(inverse(inverse(inverse(X1)))),multiply(inverse(inverse(inverse(X2))),X2)),inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(X0),X4)),X1)))))) = X4,
inference(paramodulation,[status(thm)],[f4555,f321]) ).
fof(f4664,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(X0)),multiply(inverse(inverse(inverse(inverse(X1)))),multiply(inverse(inverse(inverse(X2))),X2))) = multiply(inverse(X3),multiply(X3,multiply(X0,X1))),
inference(paramodulation,[status(thm)],[f4555,f299]) ).
fof(f4665,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,X1)) = multiply(inverse(inverse(inverse(inverse(X1)))),multiply(inverse(inverse(inverse(X2))),X2)),
inference(paramodulation,[status(thm)],[f4555,f221]) ).
fof(f4667,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(inverse(inverse(inverse(X1)))),X2)),X1),inverse(multiply(inverse(inverse(inverse(X3))),X3)))))) = X2,
inference(paramodulation,[status(thm)],[f4555,f70]) ).
fof(f4668,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = inverse(multiply(multiply(inverse(multiply(inverse(inverse(inverse(inverse(X4)))),multiply(inverse(inverse(X0)),X2))),X4),inverse(multiply(inverse(inverse(inverse(X5))),X5)))),
inference(paramodulation,[status(thm)],[f4555,f16]) ).
fof(f4671,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(inverse(inverse(inverse(X1)))),multiply(inverse(X0),X2))),X1),inverse(multiply(inverse(inverse(inverse(X3))),X3))))) = X2,
inference(paramodulation,[status(thm)],[f4555,f3]) ).
fof(f4911,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(inverse(X0),multiply(X0,multiply(inverse(X1),multiply(X1,multiply(inverse(multiply(inverse(X2),multiply(X2,X3))),X3))))) = multiply(inverse(X4),multiply(X4,multiply(inverse(inverse(inverse(X5))),X5))),
inference(paramodulation,[status(thm)],[f4357,f1193]) ).
fof(f4927,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(inverse(inverse(X1))),X2)),multiply(inverse(multiply(inverse(X3),multiply(X3,X4))),X4)),inverse(X1)))) = inverse(multiply(multiply(inverse(multiply(inverse(X5),multiply(inverse(inverse(X0)),X2))),X6),inverse(multiply(X5,X6)))),
inference(paramodulation,[status(thm)],[f4357,f16]) ).
fof(f5036,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(X1,inverse(X1)))),inverse(multiply(X2,inverse(X2))))) = inverse(multiply(X3,inverse(X3))),
inference(paramodulation,[status(thm)],[f4466,f3968]) ).
fof(f5055,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),inverse(X3)),inverse(multiply(X4,inverse(X4))))))) = multiply(X3,X2),
inference(paramodulation,[status(thm)],[f4466,f333]) ).
fof(f5199,plain,
! [X0,X1] : inverse(multiply(X0,inverse(X0))) = inverse(multiply(X1,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f3968,f5036]) ).
fof(f5307,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(multiply(X0,inverse(X0)))),multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X2)) = multiply(X3,inverse(X3)),
inference(paramodulation,[status(thm)],[f5199,f4357]) ).
fof(f5361,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(X0,X1)) = multiply(inverse(multiply(X2,inverse(X2))),multiply(multiply(X3,inverse(X3)),X1)),
inference(paramodulation,[status(thm)],[f5199,f221]) ).
fof(f5463,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = multiply(X1,inverse(X1)),
inference(forward_demodulation,[status(thm)],[f4357,f5307]) ).
fof(f5521,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X1,inverse(multiply(inverse(X2),multiply(X2,X3))))),inverse(multiply(inverse(X0),multiply(X4,inverse(X4))))))) = X3,
inference(paramodulation,[status(thm)],[f5463,f619]) ).
fof(f5522,plain,
! [X0,X1] : multiply(X0,multiply(X1,inverse(X1))) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f5463,f3968]) ).
fof(f5525,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),X2),inverse(multiply(X0,X2)))),multiply(X3,inverse(X3))) = X1,
inference(paramodulation,[status(thm)],[f5463,f70]) ).
fof(f5565,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X2,inverse(X2)))) = multiply(inverse(X3),multiply(X3,multiply(X0,inverse(X1)))),
inference(paramodulation,[status(thm)],[f5463,f299]) ).
fof(f5566,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,inverse(X1))) = multiply(inverse(X1),multiply(X2,inverse(X2))),
inference(paramodulation,[status(thm)],[f5463,f221]) ).
fof(f5666,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X1,inverse(multiply(inverse(X2),multiply(X2,X3))))),inverse(inverse(inverse(inverse(X0))))))) = X3,
inference(backward_demodulation,[status(thm)],[f5522,f5521]) ).
fof(f5678,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),multiply(inverse(inverse(inverse(X1))),X1)) = X0,
inference(backward_demodulation,[status(thm)],[f5680,f4634]) ).
fof(f5680,plain,
! [X0,X1,X2] : inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),X2),inverse(multiply(X0,X2)))))) = X1,
inference(forward_demodulation,[status(thm)],[f5522,f5525]) ).
fof(f5722,plain,
! [X0,X1,X2,X3,X4] : X0 = multiply(inverse(inverse(X0)),inverse(inverse(inverse(multiply(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X2),multiply(X2,X3)))),X4),inverse(multiply(X1,X4))),X3))))),
inference(backward_demodulation,[status(thm)],[f5735,f4423]) ).
fof(f5735,plain,
! [X0,X1,X2] : multiply(inverse(inverse(X0)),inverse(inverse(inverse(X1)))) = multiply(inverse(X2),multiply(X2,multiply(X0,inverse(X1)))),
inference(forward_demodulation,[status(thm)],[f5522,f5565]) ).
fof(f5742,plain,
! [X0,X1,X2] : inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(inverse(inverse(inverse(X0)))),X1)),X0),inverse(multiply(inverse(inverse(inverse(X2))),X2)))))) = X1,
inference(backward_demodulation,[status(thm)],[f5937,f4667]) ).
fof(f5759,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(inverse(X0)),X1)),X2),inverse(multiply(X3,X2)))))) = multiply(X3,multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X4),X1)),X5),inverse(multiply(X4,X5)))))),
inference(backward_demodulation,[status(thm)],[f5937,f2626]) ).
fof(f5783,plain,
! [X0,X1,X2,X3] : inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(X0,X1))),inverse(X2)),inverse(multiply(X3,inverse(X3))))))) = multiply(X2,X1),
inference(backward_demodulation,[status(thm)],[f5937,f5055]) ).
fof(f5798,plain,
! [X0,X1,X2,X3] : inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(X0,X1))),X2),inverse(multiply(inverse(inverse(inverse(X3))),X3)))))) = multiply(inverse(inverse(inverse(X2))),X1),
inference(backward_demodulation,[status(thm)],[f5937,f4647]) ).
fof(f5811,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),inverse(multiply(multiply(inverse(X2),multiply(X2,X3)),inverse(multiply(X4,multiply(multiply(inverse(X4),multiply(inverse(X0),X5)),X3)))))),inverse(X5))))) = X1,
inference(backward_demodulation,[status(thm)],[f5937,f1864]) ).
fof(f5817,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),X2),inverse(multiply(X3,X2)))))) = multiply(X3,inverse(multiply(multiply(inverse(X4),multiply(X4,X5)),inverse(multiply(inverse(X0),multiply(multiply(inverse(X6),multiply(X6,X1)),X5)))))),
inference(backward_demodulation,[status(thm)],[f5937,f3522]) ).
fof(f5862,plain,
! [X0,X1,X2,X3,X4] : inverse(inverse(inverse(multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(X2,multiply(multiply(inverse(X3),multiply(X3,X4)),X1))))))) = multiply(X2,X4),
inference(backward_demodulation,[status(thm)],[f5937,f2454]) ).
fof(f5884,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] : inverse(inverse(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))))) = inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(X8,inverse(multiply(multiply(inverse(multiply(inverse(X9),multiply(inverse(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(X2)),X0)))),X3)))),X5)))),X7))),X10),inverse(multiply(X9,X10)))))))))))))))),
inference(backward_demodulation,[status(thm)],[f5937,f2303]) ).
fof(f5932,plain,
! [X0,X1,X2] : X0 = inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(X1))))),inverse(multiply(inverse(X2),multiply(X2,X0))))),
inference(backward_demodulation,[status(thm)],[f5937,f3632]) ).
fof(f5933,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X2)),X3)),X4)),inverse(multiply(X1,X3))))),X2))),X5),inverse(multiply(X0,X5))))))) = X4,
inference(backward_demodulation,[status(thm)],[f5937,f82]) ).
fof(f5934,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),inverse(multiply(X3,X4))))),X5))),X6),inverse(multiply(X0,X6))))))) = multiply(multiply(inverse(multiply(inverse(X3),X5)),X4),X2),
inference(backward_demodulation,[status(thm)],[f5937,f2585]) ).
fof(f5937,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,inverse(X1))) = inverse(inverse(inverse(X1))),
inference(forward_demodulation,[status(thm)],[f5522,f5566]) ).
fof(f5984,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(inverse(inverse(inverse(multiply(inverse(X1),multiply(X1,X2))))),inverse(inverse(inverse(inverse(X0))))))) = X2,
inference(forward_demodulation,[status(thm)],[f5937,f5666]) ).
fof(f5989,plain,
! [X0,X1] : X0 = inverse(inverse(multiply(X0,inverse(multiply(X1,inverse(X1)))))),
inference(backward_demodulation,[status(thm)],[f5678,f4627]) ).
fof(f5994,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = inverse(inverse(X1)),
inference(backward_demodulation,[status(thm)],[f5678,f4665]) ).
fof(f5995,plain,
! [X0,X1,X2] : multiply(inverse(inverse(X0)),inverse(inverse(X1))) = multiply(inverse(X2),multiply(X2,multiply(X0,X1))),
inference(backward_demodulation,[status(thm)],[f5678,f4664]) ).
fof(f6001,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(X0),X3)),X1)))))) = X3,
inference(backward_demodulation,[status(thm)],[f5678,f4652]) ).
fof(f6030,plain,
! [X0,X1,X2,X3] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),X3)),inverse(multiply(X0,X2))))),X1)) = X3,
inference(forward_demodulation,[status(thm)],[f5680,f5933]) ).
fof(f6031,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),multiply(X0,X1))),inverse(multiply(X2,X3))))),X4)) = multiply(multiply(inverse(multiply(inverse(X2),X4)),X3),X1),
inference(forward_demodulation,[status(thm)],[f5680,f5934]) ).
fof(f6032,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(inverse(X0),multiply(X0,X1))),inverse(X2))) = multiply(X2,X1),
inference(backward_demodulation,[status(thm)],[f5989,f5783]) ).
fof(f6236,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X2))))) = multiply(inverse(X3),multiply(X3,multiply(inverse(inverse(inverse(X4))),X4))),
inference(backward_demodulation,[status(thm)],[f5994,f4911]) ).
fof(f6455,plain,
! [X0,X1,X2,X3] : inverse(multiply(inverse(inverse(multiply(inverse(inverse(inverse(X0))),inverse(multiply(X1,X2))))),X3)) = multiply(multiply(inverse(multiply(inverse(X1),X3)),X2),X0),
inference(backward_demodulation,[status(thm)],[f5994,f6031]) ).
fof(f6456,plain,
! [X0,X1] : X0 = inverse(multiply(inverse(inverse(inverse(multiply(X1,inverse(X1))))),inverse(inverse(inverse(X0))))),
inference(backward_demodulation,[status(thm)],[f5994,f5932]) ).
fof(f6497,plain,
! [X0,X1,X2,X3] : inverse(inverse(inverse(multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(X2,multiply(inverse(inverse(X3)),X1))))))) = multiply(X2,X3),
inference(backward_demodulation,[status(thm)],[f5994,f5862]) ).
fof(f6514,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),X2),inverse(multiply(X3,X2)))))) = multiply(X3,inverse(multiply(multiply(inverse(X4),multiply(X4,X5)),inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X5)))))),
inference(backward_demodulation,[status(thm)],[f5994,f5817]) ).
fof(f6515,plain,
! [X0,X1,X2,X3,X4] : inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),inverse(multiply(inverse(inverse(X2)),inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(X0),X4)),X2)))))),inverse(X4))))) = X1,
inference(backward_demodulation,[status(thm)],[f5994,f5811]) ).
fof(f6522,plain,
! [X0,X1,X2] : inverse(inverse(inverse(multiply(multiply(inverse(inverse(inverse(X0))),X1),inverse(multiply(inverse(inverse(inverse(X2))),X2)))))) = multiply(inverse(inverse(inverse(X1))),X0),
inference(backward_demodulation,[status(thm)],[f5994,f5798]) ).
fof(f6559,plain,
! [X0,X1,X2,X3] : X0 = multiply(inverse(inverse(X0)),inverse(inverse(inverse(multiply(multiply(multiply(inverse(multiply(inverse(X1),inverse(inverse(X2)))),X3),inverse(multiply(X1,X3))),X2))))),
inference(backward_demodulation,[status(thm)],[f5994,f5722]) ).
fof(f6564,plain,
! [X0,X1] : multiply(X0,inverse(multiply(inverse(inverse(inverse(inverse(inverse(X1))))),inverse(inverse(inverse(inverse(X0))))))) = X1,
inference(backward_demodulation,[status(thm)],[f5994,f5984]) ).
fof(f6577,plain,
! [X0,X1,X2] : inverse(inverse(X0)) = multiply(inverse(multiply(X1,inverse(X1))),multiply(multiply(X2,inverse(X2)),X0)),
inference(backward_demodulation,[status(thm)],[f5994,f5361]) ).
fof(f6604,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(inverse(inverse(X1))),X2)),multiply(inverse(inverse(inverse(X3))),X3)),inverse(X1)))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X2))),X5),inverse(multiply(X4,X5)))),
inference(backward_demodulation,[status(thm)],[f5994,f4927]) ).
fof(f6684,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = inverse(multiply(multiply(inverse(inverse(inverse(X4))),X4),inverse(multiply(inverse(inverse(X0)),X2)))),
inference(backward_demodulation,[status(thm)],[f5994,f3797]) ).
fof(f6729,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(inverse(X2),multiply(inverse(inverse(X3)),X1))))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(X2),X3))),X5),inverse(multiply(X4,X5)))),
inference(backward_demodulation,[status(thm)],[f5994,f3536]) ).
fof(f6739,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(inverse(multiply(inverse(X2),X4))),X1))),X5),inverse(multiply(X3,X5))))))))) = inverse(multiply(multiply(inverse(X6),multiply(X6,X7)),inverse(multiply(inverse(inverse(X0)),multiply(inverse(inverse(X4)),X7))))),
inference(backward_demodulation,[status(thm)],[f5994,f3505]) ).
fof(f6740,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(X3,X2))))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),inverse(multiply(multiply(inverse(X5),multiply(X5,X6)),inverse(multiply(inverse(inverse(X3)),multiply(inverse(inverse(X1)),X6)))))))),X7),inverse(multiply(X4,X7)))),
inference(backward_demodulation,[status(thm)],[f5994,f3504]) ).
fof(f6749,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(multiply(inverse(X6),multiply(X6,X7)),inverse(multiply(inverse(inverse(multiply(inverse(X5),multiply(inverse(inverse(X0)),X2)))),multiply(inverse(inverse(X4)),X7))))))))),
inference(backward_demodulation,[status(thm)],[f5994,f3489]) ).
fof(f7119,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),inverse(inverse(X1))) = inverse(inverse(multiply(X0,X1))),
inference(forward_demodulation,[status(thm)],[f5994,f5995]) ).
fof(f7148,plain,
! [X0,X1] : inverse(multiply(inverse(inverse(inverse(X0))),inverse(X1))) = multiply(X1,X0),
inference(forward_demodulation,[status(thm)],[f5994,f6032]) ).
fof(f7427,plain,
! [X0,X1,X2,X3] : inverse(inverse(inverse(inverse(multiply(inverse(multiply(inverse(X0),multiply(X0,X1))),X1))))) = multiply(inverse(X2),multiply(X2,multiply(inverse(inverse(inverse(X3))),X3))),
inference(forward_demodulation,[status(thm)],[f5937,f6236]) ).
fof(f7428,plain,
! [X0,X1,X2] : inverse(inverse(inverse(inverse(multiply(inverse(inverse(inverse(X0))),X0))))) = multiply(inverse(X1),multiply(X1,multiply(inverse(inverse(inverse(X2))),X2))),
inference(forward_demodulation,[status(thm)],[f5994,f7427]) ).
fof(f7429,plain,
! [X0,X1] : inverse(inverse(inverse(inverse(multiply(inverse(inverse(inverse(X0))),X0))))) = inverse(inverse(multiply(inverse(inverse(inverse(X1))),X1))),
inference(forward_demodulation,[status(thm)],[f5994,f7428]) ).
fof(f7742,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = inverse(inverse(multiply(inverse(multiply(multiply(inverse(inverse(inverse(X4))),X4),inverse(multiply(inverse(inverse(inverse(X5))),X5)))),multiply(inverse(inverse(X0)),X2)))),
inference(backward_demodulation,[status(thm)],[f8223,f4668]) ).
fof(f7743,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(inverse(multiply(inverse(multiply(multiply(inverse(inverse(inverse(X1))),X1),inverse(multiply(inverse(inverse(inverse(X2))),X2)))),multiply(inverse(X0),X3))))) = X3,
inference(backward_demodulation,[status(thm)],[f8223,f4671]) ).
fof(f7744,plain,
! [X0,X1,X2] : inverse(inverse(inverse(inverse(multiply(inverse(multiply(multiply(inverse(inverse(inverse(X0))),X0),inverse(multiply(inverse(inverse(inverse(X1))),X1)))),X2))))) = X2,
inference(backward_demodulation,[status(thm)],[f8223,f5742]) ).
fof(f7793,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(inverse(inverse(inverse(multiply(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))),X3))))) = multiply(X2,multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5)))))),
inference(backward_demodulation,[status(thm)],[f8223,f5759]) ).
fof(f7958,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] : inverse(inverse(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))))) = inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(X8,inverse(inverse(multiply(inverse(multiply(multiply(X9,X10),inverse(multiply(X9,X10)))),multiply(inverse(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(X2)),X0)))),X3)))),X5)))),X7)))))))))))))))),
inference(backward_demodulation,[status(thm)],[f8223,f5884]) ).
fof(f8223,plain,
! [X0,X1,X2,X3] : inverse(multiply(inverse(multiply(multiply(X0,X1),X2)),X3)) = multiply(multiply(inverse(multiply(inverse(X0),X3)),X1),X2),
inference(forward_demodulation,[status(thm)],[f7148,f6455]) ).
fof(f8224,plain,
! [X0,X1] : X0 = multiply(inverse(inverse(X0)),multiply(X1,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f7148,f6456]) ).
fof(f8230,plain,
! [X0,X1] : multiply(inverse(inverse(inverse(X0))),X0) = inverse(inverse(multiply(inverse(inverse(inverse(X1))),X1))),
inference(backward_demodulation,[status(thm)],[f8245,f7429]) ).
fof(f8245,plain,
! [X0] : X0 = inverse(inverse(inverse(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f5522,f8224]) ).
fof(f8292,plain,
! [X0,X1,X2] : inverse(inverse(inverse(multiply(inverse(inverse(X0)),inverse(multiply(X1,multiply(inverse(inverse(X2)),X0))))))) = multiply(X1,X2),
inference(forward_demodulation,[status(thm)],[f5994,f6497]) ).
fof(f8312,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(inverse(inverse(inverse(multiply(inverse(multiply(multiply(X0,X1),inverse(multiply(X2,X1)))),X3))))) = multiply(X2,inverse(multiply(multiply(inverse(X4),multiply(X4,X5)),inverse(multiply(inverse(X0),multiply(inverse(inverse(X3)),X5)))))),
inference(forward_demodulation,[status(thm)],[f8223,f6514]) ).
fof(f8313,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(multiply(X0,X1),inverse(multiply(X2,X1)))),X3) = multiply(X2,inverse(multiply(multiply(inverse(X4),multiply(X4,X5)),inverse(multiply(inverse(X0),multiply(inverse(inverse(X3)),X5)))))),
inference(forward_demodulation,[status(thm)],[f8245,f8312]) ).
fof(f8314,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(multiply(X0,X1),inverse(multiply(X2,X1)))),X3) = multiply(X2,inverse(multiply(inverse(inverse(X4)),inverse(multiply(inverse(X0),multiply(inverse(inverse(X3)),X4)))))),
inference(forward_demodulation,[status(thm)],[f5994,f8313]) ).
fof(f8315,plain,
! [X0,X1,X2,X3,X4] : inverse(inverse(inverse(inverse(multiply(inverse(multiply(multiply(X0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(X0),X3)),X1)))))),inverse(X3))),X4))))) = X4,
inference(forward_demodulation,[status(thm)],[f8223,f6515]) ).
fof(f8316,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(multiply(X0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(X0),X3)),X1)))))),inverse(X3))),X4) = X4,
inference(forward_demodulation,[status(thm)],[f8245,f8315]) ).
fof(f8344,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(X0))),X1) = X1,
inference(forward_demodulation,[status(thm)],[f6001,f8316]) ).
fof(f8468,plain,
! [X0,X1,X2,X3] : X0 = inverse(inverse(multiply(X0,inverse(multiply(multiply(multiply(inverse(multiply(inverse(X1),inverse(inverse(X2)))),X3),inverse(multiply(X1,X3))),X2))))),
inference(forward_demodulation,[status(thm)],[f7119,f6559]) ).
fof(f8469,plain,
! [X0,X1,X2,X3] : X0 = inverse(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(multiply(X1,X2),inverse(multiply(X1,X2)))),inverse(inverse(X3)))),X3))))),
inference(forward_demodulation,[status(thm)],[f8223,f8468]) ).
fof(f8470,plain,
! [X0,X1] : inverse(multiply(inverse(inverse(inverse(X0))),X1)) = multiply(inverse(inverse(inverse(X1))),X0),
inference(backward_demodulation,[status(thm)],[f8471,f6522]) ).
fof(f8471,plain,
! [X0,X1] : X0 = inverse(inverse(multiply(X0,inverse(multiply(inverse(inverse(inverse(X1))),X1))))),
inference(forward_demodulation,[status(thm)],[f8344,f8469]) ).
fof(f8474,plain,
! [X0,X1] : multiply(X0,multiply(inverse(inverse(inverse(X0))),inverse(inverse(X1)))) = X1,
inference(forward_demodulation,[status(thm)],[f7148,f6564]) ).
fof(f8479,plain,
! [X0,X1] : multiply(X0,inverse(inverse(multiply(inverse(X0),X1)))) = X1,
inference(forward_demodulation,[status(thm)],[f7119,f8474]) ).
fof(f8500,plain,
! [X0,X1] : inverse(inverse(X0)) = multiply(multiply(X1,inverse(X1)),X0),
inference(forward_demodulation,[status(thm)],[f8344,f6577]) ).
fof(f8559,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(inverse(multiply(inverse(multiply(multiply(inverse(inverse(X1)),multiply(inverse(inverse(inverse(X2))),X2)),inverse(X1))),X3)))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X3))),X5),inverse(multiply(X4,X5)))),
inference(forward_demodulation,[status(thm)],[f8223,f6604]) ).
fof(f8560,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(inverse(multiply(inverse(multiply(X1,inverse(X1))),X2)))) = inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(inverse(X0)),X2))),X4),inverse(multiply(X3,X4)))),
inference(forward_demodulation,[status(thm)],[f5678,f8559]) ).
fof(f8561,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(inverse(X1))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),X3),inverse(multiply(X2,X3)))),
inference(forward_demodulation,[status(thm)],[f8344,f8560]) ).
fof(f8562,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(inverse(X1))) = inverse(inverse(multiply(inverse(multiply(multiply(X2,X3),inverse(multiply(X2,X3)))),multiply(inverse(inverse(X0)),X1)))),
inference(forward_demodulation,[status(thm)],[f8223,f8561]) ).
fof(f8588,plain,
! [X0,X1] : multiply(X0,inverse(inverse(X1))) = inverse(inverse(multiply(inverse(inverse(X0)),X1))),
inference(forward_demodulation,[status(thm)],[f8344,f8562]) ).
fof(f8807,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(inverse(multiply(inverse(multiply(multiply(X1,X2),inverse(multiply(X1,X2)))),X3)))) = inverse(multiply(multiply(inverse(inverse(inverse(X4))),X4),inverse(multiply(inverse(inverse(X0)),X3)))),
inference(forward_demodulation,[status(thm)],[f8223,f6684]) ).
fof(f8808,plain,
! [X0,X1,X2] : multiply(X0,inverse(inverse(X1))) = inverse(multiply(multiply(inverse(inverse(inverse(X2))),X2),inverse(multiply(inverse(inverse(X0)),X1)))),
inference(forward_demodulation,[status(thm)],[f8344,f8807]) ).
fof(f8917,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),multiply(inverse(inverse(X2)),X0))))) = inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X1),X2))),X4),inverse(multiply(X3,X4)))),
inference(forward_demodulation,[status(thm)],[f5994,f6729]) ).
fof(f8918,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),multiply(inverse(inverse(X2)),X0))))) = inverse(inverse(multiply(inverse(multiply(multiply(X3,X4),inverse(multiply(X3,X4)))),multiply(inverse(X1),X2)))),
inference(forward_demodulation,[status(thm)],[f8223,f8917]) ).
fof(f8925,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(multiply(X0,X1),inverse(multiply(X2,X1)))),X3) = multiply(X2,inverse(inverse(multiply(inverse(X0),X3)))),
inference(backward_demodulation,[status(thm)],[f8928,f8314]) ).
fof(f8928,plain,
! [X0,X1,X2] : inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),multiply(inverse(inverse(X2)),X0))))) = inverse(inverse(multiply(inverse(X1),X2))),
inference(forward_demodulation,[status(thm)],[f8344,f8918]) ).
fof(f8966,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(inverse(multiply(inverse(multiply(multiply(X3,X4),inverse(multiply(X3,X4)))),multiply(inverse(inverse(multiply(inverse(X2),X5))),X1))))))))) = inverse(multiply(multiply(inverse(X6),multiply(X6,X7)),inverse(multiply(inverse(inverse(X0)),multiply(inverse(inverse(X5)),X7))))),
inference(forward_demodulation,[status(thm)],[f8223,f6739]) ).
fof(f8967,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X2),X3))),X1)))))))) = inverse(multiply(multiply(inverse(X4),multiply(X4,X5)),inverse(multiply(inverse(inverse(X0)),multiply(inverse(inverse(X3)),X5))))),
inference(forward_demodulation,[status(thm)],[f8344,f8966]) ).
fof(f8968,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X3),inverse(inverse(X1)))))))) = inverse(multiply(multiply(inverse(X4),multiply(X4,X5)),inverse(multiply(inverse(inverse(X0)),multiply(inverse(inverse(X3)),X5))))),
inference(forward_demodulation,[status(thm)],[f8588,f8967]) ).
fof(f8969,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X3),inverse(inverse(X1)))))))) = inverse(multiply(inverse(inverse(X4)),inverse(multiply(inverse(inverse(X0)),multiply(inverse(inverse(X3)),X4))))),
inference(forward_demodulation,[status(thm)],[f5994,f8968]) ).
fof(f8970,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X3),inverse(inverse(X1)))))))) = inverse(inverse(multiply(inverse(inverse(X0)),X3))),
inference(forward_demodulation,[status(thm)],[f8928,f8969]) ).
fof(f8977,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X3),inverse(inverse(X1)))))))) = multiply(X0,inverse(inverse(X3))),
inference(forward_demodulation,[status(thm)],[f8588,f8970]) ).
fof(f8978,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(X3,X2))))) = inverse(inverse(multiply(inverse(multiply(multiply(X4,X5),inverse(multiply(X4,X5)))),multiply(inverse(inverse(X0)),inverse(multiply(multiply(inverse(X6),multiply(X6,X7)),inverse(multiply(inverse(inverse(X3)),multiply(inverse(inverse(X1)),X7))))))))),
inference(forward_demodulation,[status(thm)],[f8223,f6740]) ).
fof(f8979,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(X3,X2))))) = inverse(inverse(multiply(inverse(inverse(X0)),inverse(multiply(multiply(inverse(X4),multiply(X4,X5)),inverse(multiply(inverse(inverse(X3)),multiply(inverse(inverse(X1)),X5)))))))),
inference(forward_demodulation,[status(thm)],[f8344,f8978]) ).
fof(f8980,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(X3,X2))))) = multiply(X0,inverse(inverse(inverse(multiply(multiply(inverse(X4),multiply(X4,X5)),inverse(multiply(inverse(inverse(X3)),multiply(inverse(inverse(X1)),X5)))))))),
inference(forward_demodulation,[status(thm)],[f8588,f8979]) ).
fof(f8981,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(X3,X2))))) = multiply(X0,inverse(inverse(inverse(multiply(inverse(inverse(X4)),inverse(multiply(inverse(inverse(X3)),multiply(inverse(inverse(X1)),X4)))))))),
inference(forward_demodulation,[status(thm)],[f5994,f8980]) ).
fof(f8988,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(X3,X2))))) = multiply(X0,multiply(inverse(inverse(X3)),X1)),
inference(forward_demodulation,[status(thm)],[f8292,f8981]) ).
fof(f9034,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,multiply(inverse(inverse(X1)),multiply(inverse(X1),X2))) = inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(multiply(inverse(X5),multiply(X5,X6)),inverse(multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X2)))),multiply(inverse(inverse(X3)),X6))))))))),
inference(forward_demodulation,[status(thm)],[f8988,f6749]) ).
fof(f9035,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(inverse(X1))) = inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(multiply(inverse(X4),multiply(X4,X5)),inverse(multiply(inverse(inverse(multiply(inverse(X3),multiply(inverse(inverse(X0)),X1)))),multiply(inverse(inverse(X2)),X5))))))))),
inference(forward_demodulation,[status(thm)],[f5994,f9034]) ).
fof(f9036,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(inverse(X1))) = inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(inverse(X4)),inverse(multiply(inverse(inverse(multiply(inverse(X3),multiply(inverse(inverse(X0)),X1)))),multiply(inverse(inverse(X2)),X4))))))))),
inference(forward_demodulation,[status(thm)],[f5994,f9035]) ).
fof(f9037,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(inverse(X1))) = inverse(multiply(X2,inverse(multiply(X3,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X3),multiply(inverse(inverse(X0)),X1)))),X2))))))),
inference(forward_demodulation,[status(thm)],[f8928,f9036]) ).
fof(f9038,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(inverse(X1))) = inverse(multiply(X2,inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(inverse(X0)),X1)),inverse(inverse(X2))))))),
inference(forward_demodulation,[status(thm)],[f8588,f9037]) ).
fof(f10724,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,multiply(inverse(inverse(X1)),multiply(inverse(X1),X2))) = inverse(inverse(multiply(inverse(multiply(multiply(inverse(inverse(inverse(X3))),X3),inverse(multiply(inverse(inverse(inverse(X4))),X4)))),multiply(inverse(inverse(X0)),X2)))),
inference(forward_demodulation,[status(thm)],[f8988,f7742]) ).
fof(f10725,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(inverse(X1))) = inverse(inverse(multiply(inverse(multiply(multiply(inverse(inverse(inverse(X2))),X2),inverse(multiply(inverse(inverse(inverse(X3))),X3)))),multiply(inverse(inverse(X0)),X1)))),
inference(forward_demodulation,[status(thm)],[f5994,f10724]) ).
fof(f10726,plain,
! [X0,X1,X2] : multiply(X0,inverse(inverse(X1))) = inverse(inverse(multiply(multiply(inverse(X2),inverse(inverse(X2))),multiply(inverse(inverse(X0)),X1)))),
inference(forward_demodulation,[status(thm)],[f8808,f10725]) ).
fof(f10727,plain,
! [X0,X1] : multiply(X0,inverse(inverse(X1))) = inverse(inverse(inverse(inverse(multiply(inverse(inverse(X0)),X1))))),
inference(forward_demodulation,[status(thm)],[f8500,f10726]) ).
fof(f10786,plain,
! [X0,X1,X2,X3] : inverse(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),X3)),inverse(multiply(X0,X2))),inverse(inverse(X1)))) = X3,
inference(backward_demodulation,[status(thm)],[f10849,f6030]) ).
fof(f10849,plain,
! [X0,X1] : multiply(X0,inverse(inverse(X1))) = multiply(inverse(inverse(X0)),X1),
inference(forward_demodulation,[status(thm)],[f8245,f10727]) ).
fof(f10850,plain,
! [X0,X1,X2] : multiply(X0,inverse(inverse(multiply(multiply(inverse(X1),inverse(inverse(X1))),multiply(inverse(X0),X2))))) = X2,
inference(forward_demodulation,[status(thm)],[f8808,f7743]) ).
fof(f10851,plain,
! [X0,X1] : multiply(X0,inverse(inverse(inverse(inverse(multiply(inverse(X0),X1)))))) = X1,
inference(forward_demodulation,[status(thm)],[f8500,f10850]) ).
fof(f10852,plain,
! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(forward_demodulation,[status(thm)],[f8245,f10851]) ).
fof(f10853,plain,
! [X0,X1,X2] : multiply(inverse(multiply(multiply(inverse(inverse(inverse(X0))),X0),inverse(multiply(inverse(inverse(inverse(X1))),X1)))),X2) = X2,
inference(forward_demodulation,[status(thm)],[f8245,f7744]) ).
fof(f10854,plain,
! [X0,X1] : multiply(multiply(inverse(X0),inverse(inverse(X0))),X1) = X1,
inference(forward_demodulation,[status(thm)],[f8808,f10853]) ).
fof(f10891,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f8500,f10854]) ).
fof(f11147,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))),X3) = multiply(X2,multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X4),X3)),X5),inverse(multiply(X4,X5)))))),
inference(forward_demodulation,[status(thm)],[f8245,f7793]) ).
fof(f11148,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))),X3) = multiply(X2,multiply(X0,multiply(inverse(inverse(X4)),multiply(inverse(X4),X3)))),
inference(forward_demodulation,[status(thm)],[f8988,f11147]) ).
fof(f11149,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))),X3) = multiply(X2,multiply(X0,multiply(X4,inverse(inverse(multiply(inverse(X4),X3)))))),
inference(forward_demodulation,[status(thm)],[f10849,f11148]) ).
fof(f11150,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))),X3) = multiply(X2,multiply(X0,X3)),
inference(forward_demodulation,[status(thm)],[f8479,f11149]) ).
fof(f12645,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] : inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))) = inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(X8,inverse(inverse(multiply(inverse(multiply(multiply(X9,X10),inverse(multiply(X9,X10)))),multiply(inverse(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(X2)),X0)))),X3)))),X5)))),X7)))))))))))))))),
inference(forward_demodulation,[status(thm)],[f10891,f7958]) ).
fof(f12646,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] : inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))) = inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(X8,multiply(inverse(multiply(multiply(X9,X10),inverse(multiply(X9,X10)))),multiply(inverse(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(X2)),X0)))),X3)))),X5)))),X7)))))))))))))),
inference(forward_demodulation,[status(thm)],[f10891,f12645]) ).
fof(f12647,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))) = inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(X8,multiply(inverse(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(X2)),X0)))),X3)))),X5)))),X7))))))))))))),
inference(forward_demodulation,[status(thm)],[f8344,f12646]) ).
fof(f12648,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))) = inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(X8,multiply(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(X2)),X0)))),X3)))),X5)),inverse(inverse(X7))))))))))))))),
inference(forward_demodulation,[status(thm)],[f10849,f12647]) ).
fof(f12649,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))) = inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(X2)),X0)))),X3)))),X5))))))))))),
inference(forward_demodulation,[status(thm)],[f8977,f12648]) ).
fof(f12650,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))) = inverse(multiply(X3,inverse(multiply(X4,inverse(multiply(X5,inverse(multiply(X6,multiply(multiply(inverse(X6),multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(X2)),X0)))),X3)),inverse(inverse(X5))))))))))),
inference(forward_demodulation,[status(thm)],[f8588,f12649]) ).
fof(f12651,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))) = inverse(multiply(X3,inverse(multiply(X4,inverse(inverse(multiply(inverse(inverse(multiply(inverse(X4),multiply(inverse(inverse(X2)),X0)))),X3))))))),
inference(forward_demodulation,[status(thm)],[f8977,f12650]) ).
fof(f12652,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))) = inverse(multiply(X3,inverse(multiply(X4,multiply(multiply(inverse(X4),multiply(inverse(inverse(X2)),X0)),inverse(inverse(X3))))))),
inference(forward_demodulation,[status(thm)],[f8588,f12651]) ).
fof(f12653,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))) = multiply(X2,inverse(inverse(X0))),
inference(forward_demodulation,[status(thm)],[f9038,f12652]) ).
fof(f12655,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(backward_demodulation,[status(thm)],[f12656,f11150]) ).
fof(f12656,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))) = multiply(X2,X0),
inference(forward_demodulation,[status(thm)],[f10891,f12653]) ).
fof(f14586,plain,
! [X0,X1] : multiply(inverse(X0),inverse(inverse(X0))) = inverse(inverse(multiply(inverse(inverse(inverse(X1))),X1))),
inference(forward_demodulation,[status(thm)],[f10849,f8230]) ).
fof(f14587,plain,
! [X0,X1] : multiply(inverse(X0),X0) = inverse(inverse(multiply(inverse(inverse(inverse(X1))),X1))),
inference(forward_demodulation,[status(thm)],[f10891,f14586]) ).
fof(f14588,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),inverse(inverse(X1))),
inference(forward_demodulation,[status(thm)],[f8588,f14587]) ).
fof(f14589,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(forward_demodulation,[status(thm)],[f10891,f14588]) ).
fof(f14768,plain,
! [X0,X1] : inverse(multiply(inverse(X0),inverse(inverse(X1)))) = multiply(inverse(inverse(inverse(X1))),X0),
inference(forward_demodulation,[status(thm)],[f10849,f8470]) ).
fof(f14769,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X1)) = multiply(inverse(inverse(inverse(X1))),X0),
inference(forward_demodulation,[status(thm)],[f10891,f14768]) ).
fof(f14770,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X1)) = multiply(inverse(X1),inverse(inverse(X0))),
inference(forward_demodulation,[status(thm)],[f10849,f14769]) ).
fof(f14780,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X1)) = multiply(inverse(X1),X0),
inference(forward_demodulation,[status(thm)],[f10891,f14770]) ).
fof(f15136,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(multiply(X0,X1),inverse(multiply(X2,X1)))),X3) = multiply(X2,multiply(inverse(X0),X3)),
inference(forward_demodulation,[status(thm)],[f10891,f8925]) ).
fof(f15428,plain,
! [X0,X1,X2,X3] : inverse(inverse(multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(X0),X1)),X2),inverse(multiply(X0,X2))),inverse(inverse(X1)))),X3))) = X3,
inference(forward_demodulation,[status(thm)],[f8223,f10786]) ).
fof(f15429,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(X0),X1)),X2),inverse(multiply(X0,X2))),inverse(inverse(X1)))),X3) = X3,
inference(forward_demodulation,[status(thm)],[f10891,f15428]) ).
fof(f15430,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(multiply(X0,X1),inverse(multiply(X0,X1)))),X2)),inverse(inverse(X2)))),X3) = X3,
inference(forward_demodulation,[status(thm)],[f8223,f15429]) ).
fof(f15431,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(inverse(inverse(X0))),multiply(inverse(multiply(multiply(X1,X2),inverse(multiply(X1,X2)))),X0)),X3) = X3,
inference(forward_demodulation,[status(thm)],[f14780,f15430]) ).
fof(f15432,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(X0),inverse(inverse(multiply(inverse(multiply(multiply(X1,X2),inverse(multiply(X1,X2)))),X0)))),X3) = X3,
inference(forward_demodulation,[status(thm)],[f10849,f15431]) ).
fof(f15433,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(X0),multiply(inverse(multiply(multiply(X1,X2),inverse(multiply(X1,X2)))),X0)),X3) = X3,
inference(forward_demodulation,[status(thm)],[f10891,f15432]) ).
fof(f15434,plain,
! [X0,X1,X2] : multiply(multiply(inverse(X0),multiply(X1,multiply(inverse(X1),X0))),X2) = X2,
inference(forward_demodulation,[status(thm)],[f15136,f15433]) ).
fof(f15435,plain,
! [X0,X1] : multiply(multiply(inverse(X0),X0),X1) = X1,
inference(forward_demodulation,[status(thm)],[f10852,f15434]) ).
fof(f15719,plain,
( sQ2_spl
| multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)) ),
inference(backward_demodulation,[status(thm)],[f12655,f13]) ).
fof(f15728,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(backward_demodulation,[status(thm)],[f12655,f15435]) ).
fof(f15767,plain,
( sQ2_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f15719]) ).
fof(f15768,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f15767]) ).
fof(f15805,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7,f14589]) ).
fof(f15806,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f15805]) ).
fof(f15808,plain,
( sQ1_spl
| multiply(inverse(b2),multiply(b2,a2)) != a2 ),
inference(forward_demodulation,[status(thm)],[f12655,f10]) ).
fof(f15809,plain,
( sQ1_spl
| a2 != a2 ),
inference(forward_demodulation,[status(thm)],[f15728,f15808]) ).
fof(f15810,plain,
( sQ1_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f15809]) ).
fof(f15811,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f15810]) ).
fof(f15812,plain,
$false,
inference(sat_refutation,[status(thm)],[f14,f15768,f15806,f15811]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP057-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.56 % Computer : n020.cluster.edu
% 0.08/0.56 % Model : x86_64 x86_64
% 0.08/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.56 % Memory : 8046.5625MB
% 0.08/0.56 % OS : Linux 6.8.0-71-generic
% 0.08/0.56 % CPULimit : 300
% 0.08/0.56 % WCLimit : 300
% 0.08/0.56 % DateTime : Sun Sep 20 19:57:03 UTC 2026
% 0.08/0.56 % CPUTime :
% 0.08/0.57 % Drodi V4.1.1
% 227.22/29.24 % Refutation found
% 227.22/29.24 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 227.22/29.24 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 114.40/29.38 % Elapsed time: 28.800681 seconds
% 114.40/29.38 % CPU time: 228.350315 seconds
% 114.40/29.38 % Total memory used: 1.093 GB
% 114.40/29.38 % Net memory used: 1.060 GB
%------------------------------------------------------------------------------