↑ Up

Drodi---4.1.1.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Drodi---4.1.1
% Problem  : GRP052-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p

% Computer : n013.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 235.15s 30.12s
% Output   : CNFRefutation 31.40s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   68
%            Number of leaves      :    5
% Syntax   : Number of formulae    :  329 ( 314 unt;   3 def)
%            Number of atoms       :  347 ( 325 equ)
%            Maximal formula atoms :    3 (   1 avg)
%            Number of connectives :   33 (  15   ~;  15   |;   0   &)
%                                         (   3 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   11 (   6 avg)
%            Maximal term depth    :   26 (   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   : 1579 (1579   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,axiom,
    ! [Z,Y,X] : multiply(Z,inverse(multiply(multiply(multiply(inverse(Y),Y),inverse(multiply(inverse(multiply(Z,inverse(Y))),X))),Y))) = X,
    file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).

fof(f3,plain,
    ! [X0,X1,X2] : X0 = multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X1,inverse(X2))),X0))),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] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),inverse(X0))),X3))),X0)) = multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))),
    inference(paramodulation,[status(thm)],[f3,f3]) ).

fof(f16,plain,
    ! [X0,X1,X2,X3] : X0 = multiply(X1,inverse(multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X1,inverse(X2))),X3))),X2)),multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X1,inverse(X2))),X3))),X2)),inverse(multiply(inverse(X3),X0))),multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X1,inverse(X2))),X3))),X2)))),
    inference(paramodulation,[status(thm)],[f3,f3]) ).

fof(f25,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(multiply(multiply(inverse(inverse(X0)),inverse(X0)),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),inverse(inverse(X0)))),X3))),inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(X4)),X0))) = inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))),inverse(X5))),X4))),X5)),
    inference(paramodulation,[status(thm)],[f15,f15]) ).

fof(f30,plain,
    ! [X0,X1,X2,X3] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),inverse(X0))),multiply(inverse(multiply(X1,inverse(X2))),X3)))),X0)) = X3,
    inference(paramodulation,[status(thm)],[f3,f15]) ).

fof(f33,plain,
    ! [X0,X1,X2,X3,X4,X5] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))))),inverse(X0))),X4))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))),inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))),inverse(X4)),inverse(X2))),inverse(X5))),X3))),X5)))),
    inference(paramodulation,[status(thm)],[f15,f15]) ).

fof(f38,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),inverse(X0))),multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X5))),inverse(X3))),X6))),X3)))),X0)) = multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),multiply(X4,inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(X6)),X5)))),X2))),
    inference(paramodulation,[status(thm)],[f15,f15]) ).

fof(f39,plain,
    ! [X0,X1,X2] : X0 = multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X0)),X2)))),
    inference(paramodulation,[status(thm)],[f15,f3]) ).

fof(f40,plain,
    ! [X0,X1,X2,X3,X4] : X0 = multiply(multiply(multiply(inverse(inverse(X1)),inverse(X1)),inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),inverse(inverse(X1)))),X4))),inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(multiply(X2,inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X4)),X3))),X0))),X1))),
    inference(paramodulation,[status(thm)],[f15,f3]) ).

fof(f82,plain,
    ! [X0,X1,X2,X3,X4,X5] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(inverse(X1)),inverse(X1)),inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),inverse(inverse(X1)))),multiply(inverse(multiply(X2,inverse(X3))),X4)))),inverse(X1))),inverse(X0))),multiply(X4,X5)))),X0)) = X5,
    inference(paramodulation,[status(thm)],[f30,f30]) ).

fof(f112,plain,
    ! [X0,X1,X2] : X0 = inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X0)))),X1)),
    inference(forward_demodulation,[status(thm)],[f30,f82]) ).

fof(f142,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X2)) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,X2)),
    inference(paramodulation,[status(thm)],[f112,f39]) ).

fof(f183,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(X1,X2)) = multiply(inverse(multiply(X3,inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(X1,inverse(X4))),X0))),X4)))),multiply(X3,X2)),
    inference(paramodulation,[status(thm)],[f3,f142]) ).

fof(f200,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(X0,inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X3)))),X1)))),multiply(X0,X4)) = multiply(inverse(multiply(X5,X3)),multiply(X5,X4)),
    inference(paramodulation,[status(thm)],[f112,f142]) ).

fof(f233,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(X3,X1)),multiply(X3,X2)),
    inference(forward_demodulation,[status(thm)],[f183,f200]) ).

fof(f248,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(multiply(X3,X1)),multiply(X3,X4))) = multiply(inverse(multiply(X5,X2)),multiply(X5,multiply(X0,X4))),
    inference(paramodulation,[status(thm)],[f233,f233]) ).

fof(f256,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(X3,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,X3)))),X2)),
    inference(paramodulation,[status(thm)],[f112,f233]) ).

fof(f259,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),multiply(inverse(multiply(X3,X1)),X4)) = multiply(inverse(multiply(X5,multiply(X3,X2))),multiply(X5,X4)),
    inference(paramodulation,[status(thm)],[f233,f233]) ).

fof(f265,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X3,inverse(X2))),X4))),X2)))) = multiply(inverse(multiply(X3,X1)),X4),
    inference(paramodulation,[status(thm)],[f3,f233]) ).

fof(f301,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(multiply(X3,X1)),multiply(X3,X4)))),multiply(inverse(multiply(X5,X2)),multiply(X5,X6))) = multiply(inverse(multiply(X7,multiply(X8,multiply(X0,X4)))),multiply(X7,multiply(X8,X6))),
    inference(paramodulation,[status(thm)],[f248,f248]) ).

fof(f304,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(X0),multiply(inverse(multiply(X1,X2)),multiply(X1,X3))) = multiply(inverse(multiply(X4,inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(multiply(X6,X2)),inverse(X5))),X0))),X5)))),multiply(X4,multiply(X6,X3))),
    inference(paramodulation,[status(thm)],[f3,f248]) ).

fof(f395,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(inverse(multiply(X1,X2)),multiply(X1,X3))) = multiply(inverse(X0),multiply(inverse(multiply(X4,X2)),multiply(X4,X3))),
    inference(forward_demodulation,[status(thm)],[f183,f304]) ).

fof(f411,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,multiply(inverse(multiply(X1,X2)),multiply(X1,X3))) = multiply(inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(X5,inverse(X4))),multiply(X5,X0)))),X4)),multiply(inverse(multiply(X6,X2)),multiply(X6,X3))),
    inference(paramodulation,[status(thm)],[f112,f395]) ).

fof(f528,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,multiply(inverse(multiply(X1,X2)),multiply(X1,X3))) = multiply(X0,multiply(inverse(multiply(X4,X2)),multiply(X4,X3))),
    inference(forward_demodulation,[status(thm)],[f112,f411]) ).

fof(f710,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),X3) = multiply(inverse(multiply(X4,multiply(X5,X2))),multiply(X4,inverse(multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(multiply(inverse(multiply(X5,X1)),inverse(X6))),X3))),X6)))),
    inference(paramodulation,[status(thm)],[f3,f259]) ).

fof(f714,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] : multiply(inverse(multiply(X0,multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3))),X4))),multiply(X0,X5)) = multiply(inverse(multiply(inverse(multiply(X6,multiply(inverse(multiply(X7,X2)),X8))),multiply(X6,X4))),multiply(inverse(multiply(inverse(multiply(X9,multiply(X7,X3))),multiply(X9,X8))),X5)),
    inference(paramodulation,[status(thm)],[f259,f259]) ).

fof(f738,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))))),multiply(inverse(multiply(X4,X1)),X5)) = multiply(inverse(X3),multiply(inverse(multiply(X4,inverse(X2))),X5)),
    inference(paramodulation,[status(thm)],[f39,f259]) ).

fof(f766,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,multiply(X1,X3))) = multiply(inverse(multiply(X4,multiply(X5,X2))),multiply(X4,multiply(X5,X3))),
    inference(paramodulation,[status(thm)],[f259,f248]) ).

fof(f828,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),X3) = multiply(inverse(multiply(inverse(multiply(X4,X1)),multiply(X4,X2))),X3),
    inference(forward_demodulation,[status(thm)],[f265,f710]) ).

fof(f960,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1)),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1)),inverse(multiply(inverse(X2),X3))),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1))),multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1)),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1)),inverse(multiply(inverse(X2),X3))),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1))),inverse(X4)),multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1)),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1)),inverse(multiply(inverse(X2),X3))),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1))))) = inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(X3),inverse(X5))),X4))),X5)),
    inference(paramodulation,[status(thm)],[f16,f15]) ).

fof(f1259,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,X5))),X1)),multiply(inverse(multiply(inverse(multiply(X6,X4)),multiply(X6,X5))),X7))) = multiply(inverse(multiply(X8,X2)),multiply(X8,multiply(X0,X7))),
    inference(paramodulation,[status(thm)],[f828,f248]) ).

fof(f1560,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] : multiply(inverse(multiply(X0,multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3))),X4))),multiply(X0,multiply(inverse(multiply(X5,multiply(X6,X3))),multiply(X5,X7)))) = multiply(inverse(multiply(X8,multiply(X9,X4))),multiply(X8,multiply(X9,multiply(inverse(multiply(X6,X2)),X7)))),
    inference(paramodulation,[status(thm)],[f259,f766]) ).

fof(f1677,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),X3)),multiply(inverse(multiply(X4,multiply(X5,X2))),multiply(X4,multiply(X5,X6)))) = multiply(inverse(multiply(inverse(multiply(X0,X7)),X3)),multiply(inverse(multiply(X8,X7)),multiply(X8,multiply(X1,X6)))),
    inference(paramodulation,[status(thm)],[f766,f248]) ).

fof(f1698,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X2,multiply(X3,X4)))) = multiply(inverse(multiply(inverse(multiply(X2,multiply(X3,X5))),X1)),multiply(inverse(multiply(X6,multiply(X7,X5))),multiply(X6,multiply(X7,X4)))),
    inference(paramodulation,[status(thm)],[f766,f233]) ).

fof(f1821,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X0)))),inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(X4,inverse(X3))),X5))),X3)))) = multiply(inverse(multiply(X4,X1)),X5),
    inference(paramodulation,[status(thm)],[f3,f256]) ).

fof(f1822,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(multiply(X0,X1)),inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X3))),inverse(X2))),X4))),X2))) = multiply(X5,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X6,inverse(X1))),multiply(X6,X5)))),inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X4)),X3)))),
    inference(paramodulation,[status(thm)],[f15,f256]) ).

fof(f1864,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),X3))),X1)),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),X3))),X1)),inverse(multiply(inverse(X3),multiply(X2,X0)))),X4)) = multiply(inverse(multiply(X5,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),X3))),X1))),multiply(X5,X4)),
    inference(paramodulation,[status(thm)],[f3,f256]) ).

fof(f1868,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X3)))),X1))),multiply(X0,X4)) = multiply(X5,multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X3)))),X1)),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X3)))),X1)),inverse(multiply(inverse(multiply(X6,X3)),multiply(X6,X5)))),X4)),
    inference(paramodulation,[status(thm)],[f112,f256]) ).

fof(f1885,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(X4,inverse(X3))),X5))),X3)),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X4,inverse(X1))),X5))),X2)),
    inference(paramodulation,[status(thm)],[f3,f256]) ).

fof(f1954,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2)))),X0)) = multiply(X3,inverse(multiply(multiply(multiply(inverse(X4),X4),multiply(X5,inverse(multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(multiply(X5,inverse(X6))),inverse(multiply(inverse(multiply(X3,inverse(X4))),inverse(X0)))))),X6)))),X4))),
    inference(paramodulation,[status(thm)],[f256,f38]) ).

fof(f1996,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,multiply(multiply(multiply(X1,multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,X1)))),X2)),inverse(multiply(inverse(multiply(X4,X1)),multiply(X4,X0)))),X5)) = multiply(inverse(multiply(X6,multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,X1)))),X2))),multiply(X6,X5)),
    inference(forward_demodulation,[status(thm)],[f112,f1868]) ).

fof(f2003,plain,
    ! [X0,X1,X2,X3,X4] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2)))),X0)) = multiply(X3,inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(X3,inverse(X4))),inverse(X0)))),X4))),
    inference(forward_demodulation,[status(thm)],[f3,f1954]) ).

fof(f2004,plain,
    ! [X0,X1,X2] : inverse(X0) = inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2)))),X0)),
    inference(forward_demodulation,[status(thm)],[f3,f2003]) ).

fof(f2082,plain,
    ! [X0,X1,X2,X3] : inverse(X0) = inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X1,inverse(X2))),X3))),X2)))),X3))),X0)),
    inference(paramodulation,[status(thm)],[f3,f2004]) ).

fof(f2136,plain,
    ! [X0,X1] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X1),X1))),X0)) = inverse(X0),
    inference(forward_demodulation,[status(thm)],[f3,f2082]) ).

fof(f2250,plain,
    ! [X0,X1,X2] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X2))),
    inference(paramodulation,[status(thm)],[f2136,f39]) ).

fof(f2261,plain,
    ! [X0,X1,X2] : X0 = multiply(multiply(multiply(inverse(inverse(X1)),inverse(X1)),inverse(multiply(inverse(X2),X2))),inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),X0))),X1))),
    inference(paramodulation,[status(thm)],[f2136,f3]) ).

fof(f2287,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X1),X1))),X0) = multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X0)),X3)))),
    inference(paramodulation,[status(thm)],[f2136,f39]) ).

fof(f2345,plain,
    ! [X0,X1] : multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X1),X1))),X0) = X0,
    inference(forward_demodulation,[status(thm)],[f39,f2287]) ).

fof(f2415,plain,
    ! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,X0)),multiply(X1,X0)),
    inference(paramodulation,[status(thm)],[f2345,f256]) ).

fof(f2431,plain,
    ! [X0,X1,X2] : X0 = multiply(inverse(multiply(multiply(multiply(inverse(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X0)),X1))),inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X0)),X1))),inverse(multiply(inverse(X2),X2))),inverse(X1))),inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X0)),X1))),
    inference(paramodulation,[status(thm)],[f2345,f39]) ).

fof(f2509,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1)),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1)),inverse(X3)),multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1)),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1)),inverse(multiply(inverse(X2),X4))),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X2))),X1))))) = inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(X4),inverse(X5))),X3))),X5)),
    inference(backward_demodulation,[status(thm)],[f2415,f960]) ).

fof(f2566,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),X3))),X1))),multiply(X0,X4)) = multiply(X5,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X3),multiply(X2,X5)))),X4)),
    inference(backward_demodulation,[status(thm)],[f2415,f1864]) ).

fof(f2611,plain,
    ! [X0,X1] : multiply(inverse(inverse(X0)),inverse(X0)) = multiply(inverse(X1),X1),
    inference(backward_demodulation,[status(thm)],[f2415,f2250]) ).

fof(f2705,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X3))),X1)),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X3))),X1)),inverse(multiply(inverse(X3),X4))),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X0,inverse(X1))),X3))),X1))))) = inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(X4),inverse(X5))),X2))),X5)),
    inference(forward_demodulation,[status(thm)],[f2415,f2509]) ).

fof(f2706,plain,
    ! [X0,X1,X2,X3,X4,X5] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(X1),inverse(X0))),X2))),X0)) = multiply(X3,inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(X2)),multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(X5),X1))),multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(X3,inverse(X4))),X5))),X4))))),
    inference(forward_demodulation,[status(thm)],[f2415,f2705]) ).

fof(f2742,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(X0),inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,X0)))),X1))) = multiply(inverse(X3),X3),
    inference(paramodulation,[status(thm)],[f112,f2611]) ).

fof(f2782,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(inverse(X1)),X0)))),X3)) = multiply(inverse(multiply(X4,X1)),multiply(X4,X3)),
    inference(paramodulation,[status(thm)],[f2611,f256]) ).

fof(f2788,plain,
    ! [X0,X1,X2] : multiply(inverse(inverse(X0)),inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(X1),X1)),X2))),X0))) = X2,
    inference(paramodulation,[status(thm)],[f2611,f3]) ).

fof(f2835,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(inverse(multiply(X1,X2)),multiply(X1,X2))) = multiply(X0,multiply(inverse(inverse(X3)),inverse(X3))),
    inference(paramodulation,[status(thm)],[f2611,f528]) ).

fof(f2843,plain,
    ! [X0,X1,X2] : X0 = multiply(multiply(multiply(inverse(inverse(X1)),inverse(X1)),inverse(multiply(inverse(X2),X2))),X0),
    inference(paramodulation,[status(thm)],[f2611,f2345]) ).

fof(f2850,plain,
    ! [X0,X1,X2,X3] : X0 = multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(multiply(multiply(inverse(inverse(X3)),inverse(X3)),inverse(X0)),X2)))),
    inference(paramodulation,[status(thm)],[f2611,f39]) ).

fof(f2882,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(inverse(X4)),inverse(X4))),multiply(inverse(X1),X2))),X3),
    inference(paramodulation,[status(thm)],[f2611,f828]) ).

fof(f2893,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(X1),multiply(X2,X3))) = multiply(inverse(multiply(inverse(multiply(X2,X4)),X1)),multiply(inverse(multiply(X5,X4)),multiply(X5,X3))),
    inference(paramodulation,[status(thm)],[f2611,f248]) ).

fof(f2895,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X2,X3))) = multiply(inverse(multiply(inverse(multiply(X2,X4)),X1)),multiply(inverse(multiply(inverse(inverse(X5)),inverse(X5))),multiply(inverse(X4),X3))),
    inference(paramodulation,[status(thm)],[f2611,f248]) ).

fof(f2898,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(X1),X2)) = multiply(inverse(multiply(X3,X1)),multiply(X3,X2)),
    inference(paramodulation,[status(thm)],[f2611,f233]) ).

fof(f2911,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(inverse(X1),X1)) = multiply(X0,multiply(inverse(inverse(X2)),inverse(X2))),
    inference(forward_demodulation,[status(thm)],[f2415,f2835]) ).

fof(f2913,plain,
    ! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
    inference(forward_demodulation,[status(thm)],[f112,f2742]) ).

fof(f2923,plain,
    ! [X0,X1] : X0 = multiply(inverse(inverse(X1)),inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X0)),X1))),
    inference(backward_demodulation,[status(thm)],[f2843,f2431]) ).

fof(f2925,plain,
    ! [X0,X1] : X0 = inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),X0))),X1)),
    inference(backward_demodulation,[status(thm)],[f2843,f2261]) ).

fof(f2934,plain,
    ! [X0,X1] : X0 = multiply(inverse(multiply(inverse(X1),X1)),X0),
    inference(backward_demodulation,[status(thm)],[f2923,f2788]) ).

fof(f2948,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(multiply(X3,X1)),multiply(X3,X4))) = multiply(inverse(X2),multiply(X0,X4)),
    inference(backward_demodulation,[status(thm)],[f2934,f2893]) ).

fof(f2949,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(X1),X2),
    inference(backward_demodulation,[status(thm)],[f2934,f2898]) ).

fof(f2950,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X2,X3))) = multiply(inverse(multiply(inverse(multiply(X2,X4)),X1)),multiply(inverse(X4),X3)),
    inference(backward_demodulation,[status(thm)],[f2934,f2895]) ).

fof(f2951,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),X3) = multiply(inverse(multiply(inverse(X1),X2)),X3),
    inference(backward_demodulation,[status(thm)],[f2934,f2882]) ).

fof(f2959,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),X0))),X2)) = multiply(inverse(multiply(X3,X1)),multiply(X3,X2)),
    inference(backward_demodulation,[status(thm)],[f2934,f2782]) ).

fof(f2973,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),multiply(inverse(multiply(X3,X1)),X4)) = multiply(inverse(multiply(X5,multiply(X6,multiply(X3,X2)))),multiply(X5,multiply(X6,X4))),
    inference(backward_demodulation,[status(thm)],[f2948,f301]) ).

fof(f3049,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),X3)),multiply(inverse(multiply(X4,multiply(X5,X2))),multiply(X4,multiply(X5,X6)))) = multiply(inverse(X3),multiply(X0,multiply(X1,X6))),
    inference(backward_demodulation,[status(thm)],[f2948,f1677]) ).

fof(f3099,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(X1,multiply(X2,X3))) = multiply(inverse(multiply(X4,X0)),multiply(X4,multiply(X1,multiply(X2,X3)))),
    inference(backward_demodulation,[status(thm)],[f3049,f1698]) ).

fof(f3104,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),X3)),multiply(inverse(multiply(X4,multiply(X5,X2))),multiply(X4,X6))) = multiply(inverse(multiply(X7,multiply(X8,X3))),multiply(X7,multiply(X8,multiply(inverse(multiply(X5,X1)),X6)))),
    inference(backward_demodulation,[status(thm)],[f3099,f1560]) ).

fof(f3136,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(inverse(multiply(X0,multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3))),X4))),multiply(X0,X5)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X6,X2)),X7)),X4)),multiply(inverse(multiply(inverse(multiply(X8,multiply(X6,X3))),multiply(X8,X7))),X5)),
    inference(backward_demodulation,[status(thm)],[f2951,f714]) ).

fof(f3171,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(inverse(X0),inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X1)))),multiply(inverse(multiply(X3,X0)),X4)) = multiply(inverse(X2),multiply(inverse(multiply(X3,inverse(X1))),X4)),
    inference(backward_demodulation,[status(thm)],[f2951,f738]) ).

fof(f3268,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,X5))),X1)),multiply(inverse(multiply(inverse(X4),X5)),X6))) = multiply(inverse(multiply(X7,X2)),multiply(X7,multiply(X0,X6))),
    inference(backward_demodulation,[status(thm)],[f2951,f1259]) ).

fof(f3296,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(multiply(inverse(multiply(inverse(X3),X4)),X1)),multiply(inverse(multiply(inverse(X3),X4)),X5))) = multiply(inverse(multiply(X6,X2)),multiply(X6,multiply(X0,X5))),
    inference(forward_demodulation,[status(thm)],[f2951,f3268]) ).

fof(f3354,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(X1,X2)) = multiply(inverse(multiply(X3,X0)),multiply(X3,multiply(X1,X2))),
    inference(forward_demodulation,[status(thm)],[f2948,f3296]) ).

fof(f3393,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,multiply(multiply(multiply(X1,multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,X1)))),X2)),inverse(multiply(inverse(multiply(X4,X1)),multiply(X4,X0)))),X5)) = multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,X1)))),X2)),X5),
    inference(backward_demodulation,[status(thm)],[f2949,f1996]) ).

fof(f3394,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),multiply(X3,X0)))),X4)) = multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X3,inverse(X1))),X2))),X1)),X4),
    inference(backward_demodulation,[status(thm)],[f2949,f2566]) ).

fof(f3507,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(X0,X1)),inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X3))),inverse(X2))),X4))),X2))) = multiply(X5,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),X5))),inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X4)),X3)))),
    inference(backward_demodulation,[status(thm)],[f2949,f1822]) ).

fof(f3508,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),X0))),inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X3,inverse(X2))),X4))),X2)))) = multiply(inverse(multiply(X3,X1)),X4),
    inference(backward_demodulation,[status(thm)],[f2949,f1821]) ).

fof(f3555,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(X0),X1) = multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X3,inverse(X2))),X4))),X2)),multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(X3,inverse(X0))),X4))),X1)),
    inference(backward_demodulation,[status(thm)],[f2949,f1885]) ).

fof(f3567,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(inverse(X0),X1)),multiply(inverse(multiply(X2,X0)),X3)) = multiply(inverse(multiply(X4,multiply(X5,multiply(X2,X1)))),multiply(X4,multiply(X5,X3))),
    inference(forward_demodulation,[status(thm)],[f2951,f2973]) ).

fof(f3568,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(inverse(X0),X1)),multiply(inverse(multiply(X2,X0)),X3)) = multiply(inverse(multiply(X4,multiply(X2,X1))),multiply(X4,X3)),
    inference(forward_demodulation,[status(thm)],[f3354,f3567]) ).

fof(f3572,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,X1)),X2) = multiply(inverse(multiply(inverse(X3),X1)),multiply(inverse(multiply(X0,X3)),X2)),
    inference(forward_demodulation,[status(thm)],[f2949,f3568]) ).

fof(f3586,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(X1,X2)) = multiply(inverse(multiply(inverse(multiply(X1,X3)),X0)),multiply(inverse(X3),X2)),
    inference(forward_demodulation,[status(thm)],[f3354,f2950]) ).

fof(f3607,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),X0))),X2)) = multiply(inverse(X1),X2),
    inference(forward_demodulation,[status(thm)],[f2949,f2959]) ).

fof(f3655,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,X1)),X2) = multiply(inverse(X1),inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(X0,inverse(X3))),X2))),X3))),
    inference(forward_demodulation,[status(thm)],[f3607,f3508]) ).

fof(f3664,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X2))),X3) = multiply(X4,multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(inverse(X2)),X4))),inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X3)),X1)))),
    inference(forward_demodulation,[status(thm)],[f3655,f3507]) ).

fof(f3665,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(inverse(X0)),X1)),X2) = multiply(X3,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),X3))),inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(X2)),X0)))),
    inference(forward_demodulation,[status(thm)],[f2951,f3664]) ).

fof(f3673,plain,
    ! [X0,X1,X2,X3,X4,X5] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))))),inverse(X0))),X4))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(inverse(X2)),inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2)))),X3),inverse(X4)),inverse(X2))),inverse(X5))),X3))),X5)))),
    inference(backward_demodulation,[status(thm)],[f3678,f33]) ).

fof(f3678,plain,
    ! [X0,X1,X2] : multiply(inverse(X0),inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X1))) = multiply(inverse(multiply(inverse(inverse(X1)),X0)),X2),
    inference(forward_demodulation,[status(thm)],[f3607,f3665]) ).

fof(f3745,plain,
    ! [X0,X1,X2] : X0 = multiply(inverse(inverse(X1)),inverse(multiply(multiply(multiply(inverse(inverse(X2)),inverse(X2)),inverse(X0)),X1))),
    inference(forward_demodulation,[status(thm)],[f2949,f2850]) ).

fof(f3918,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),X3)),X4) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X5,X1)),X6)),X3)),multiply(inverse(multiply(inverse(multiply(X7,multiply(X5,X2))),multiply(X7,X6))),X4)),
    inference(forward_demodulation,[status(thm)],[f2949,f3136]) ).

fof(f3919,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),X3) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,X0)),X5)),X2)),multiply(inverse(multiply(inverse(multiply(X6,multiply(X4,X1))),multiply(X6,X5))),X3)),
    inference(forward_demodulation,[status(thm)],[f2951,f3918]) ).

fof(f3920,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),X3) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,X0)),X5)),X2)),multiply(inverse(multiply(inverse(multiply(X4,X1)),X5)),X3)),
    inference(forward_demodulation,[status(thm)],[f2951,f3919]) ).

fof(f3948,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),multiply(inverse(multiply(X3,multiply(X4,X1))),multiply(X3,X5))) = multiply(inverse(multiply(X6,multiply(X7,X2))),multiply(X6,multiply(X7,multiply(inverse(multiply(X4,X0)),X5)))),
    inference(forward_demodulation,[status(thm)],[f2951,f3104]) ).

fof(f3949,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),multiply(inverse(multiply(X3,X1)),X4)) = multiply(inverse(multiply(X5,multiply(X6,X2))),multiply(X5,multiply(X6,multiply(inverse(multiply(X3,X0)),X4)))),
    inference(forward_demodulation,[status(thm)],[f2949,f3948]) ).

fof(f3950,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),multiply(inverse(multiply(X3,X1)),X4)) = multiply(inverse(multiply(X5,X2)),multiply(X5,multiply(inverse(multiply(X3,X0)),X4))),
    inference(forward_demodulation,[status(thm)],[f3099,f3949]) ).

fof(f3951,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),X3) = multiply(inverse(X2),multiply(inverse(multiply(inverse(multiply(X4,X1)),multiply(X4,X0))),X3)),
    inference(backward_demodulation,[status(thm)],[f3953,f3920]) ).

fof(f3953,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(inverse(multiply(X1,X2)),X3)) = multiply(inverse(multiply(inverse(multiply(inverse(X2),X4)),X0)),multiply(inverse(multiply(X1,X4)),X3)),
    inference(forward_demodulation,[status(thm)],[f3354,f3950]) ).

fof(f3974,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X1)))),X3) = multiply(inverse(X2),multiply(inverse(multiply(X0,inverse(X1))),X3)),
    inference(forward_demodulation,[status(thm)],[f3572,f3171]) ).

fof(f4079,plain,
    ! [X0,X1,X2,X3,X4,X5] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))))),inverse(X0))),X4))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X3),multiply(inverse(multiply(inverse(inverse(X2)),inverse(X2))),X3)),inverse(X4)),inverse(X2))),inverse(X5))),X3))),X5)))),
    inference(forward_demodulation,[status(thm)],[f3974,f3673]) ).

fof(f4080,plain,
    ! [X0,X1,X2,X3,X4,X5] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))))),inverse(X0))),X4))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X4)),inverse(X2))),inverse(X5))),X3))),X5)))),
    inference(forward_demodulation,[status(thm)],[f2934,f4079]) ).

fof(f4127,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),X3) = multiply(inverse(X2),multiply(inverse(multiply(inverse(X1),X0)),X3)),
    inference(forward_demodulation,[status(thm)],[f2951,f3951]) ).

fof(f4933,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,multiply(multiply(multiply(X1,multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(inverse(X2)),X1))),X2)),inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,X0)))),X4)) = multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,X1)))),X2)),X4),
    inference(forward_demodulation,[status(thm)],[f2949,f3393]) ).

fof(f4934,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X2,X3)),multiply(X2,X0)))),X4)) = multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X5,inverse(X1))),multiply(X5,X3)))),X1)),X4),
    inference(forward_demodulation,[status(thm)],[f3607,f4933]) ).

fof(f4935,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),X0))),X3)) = multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,X2)))),X1)),X3),
    inference(forward_demodulation,[status(thm)],[f2949,f4934]) ).

fof(f4942,plain,
    ! [X0,X1,X2,X3] : multiply(X0,X1) = multiply(X2,multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(X0),X2))),X1)),
    inference(forward_demodulation,[status(thm)],[f112,f4935]) ).

fof(f5099,plain,
    ! [X0,X1,X2] : X0 = multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),X2))),X0),
    inference(paramodulation,[status(thm)],[f2913,f2345]) ).

fof(f5104,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X3))) = inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X3))),inverse(X4))),X2))),X4)),
    inference(paramodulation,[status(thm)],[f2913,f15]) ).

fof(f5106,plain,
    ! [X0,X1,X2,X3] : X0 = multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(X1,inverse(X3))),X0))),X3))),
    inference(paramodulation,[status(thm)],[f2913,f3]) ).

fof(f5214,plain,
    ! [X0,X1,X2] : multiply(inverse(X0),X1) = multiply(inverse(multiply(inverse(X1),X0)),multiply(inverse(X2),X2)),
    inference(paramodulation,[status(thm)],[f2913,f2949]) ).

fof(f5254,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(inverse(X1),X1)) = multiply(X0,multiply(inverse(X2),X2)),
    inference(paramodulation,[status(thm)],[f2913,f2911]) ).

fof(f5440,plain,
    ! [X0,X1,X2] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(inverse(X1)),X2))),X1)) = X2,
    inference(paramodulation,[status(thm)],[f2913,f2925]) ).

fof(f5497,plain,
    ! [X0,X1,X2,X3,X4] : X0 = inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),X0))),multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(inverse(X4)),X2))),X4))),
    inference(paramodulation,[status(thm)],[f5440,f5440]) ).

fof(f5537,plain,
    ! [X0,X1,X2,X3,X4] : multiply(multiply(inverse(X0),X0),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),X3))),X4)) = multiply(multiply(inverse(X3),X2),X4),
    inference(paramodulation,[status(thm)],[f5214,f4942]) ).

fof(f5538,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(X0)),X2)) = multiply(multiply(inverse(X3),X3),X2),
    inference(paramodulation,[status(thm)],[f2934,f4942]) ).

fof(f5550,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),X3))),X4)) = multiply(inverse(multiply(X3,X0)),multiply(X2,X4)),
    inference(paramodulation,[status(thm)],[f4942,f2949]) ).

fof(f5551,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(X0,X1)),multiply(X2,X3)) = multiply(inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(X0),X2))),X1)),X3),
    inference(paramodulation,[status(thm)],[f4942,f2949]) ).

fof(f5595,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(X0),X1) = multiply(inverse(multiply(multiply(X2,inverse(X3)),X3)),multiply(X4,multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(X2,inverse(X0))),X4))),X1))),
    inference(backward_demodulation,[status(thm)],[f5551,f3555]) ).

fof(f5596,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),multiply(X3,X0)))),X4)) = multiply(inverse(multiply(multiply(X3,inverse(X1)),X1)),multiply(X2,X4)),
    inference(backward_demodulation,[status(thm)],[f5551,f3394]) ).

fof(f5692,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(multiply(X0,inverse(X1)),X1)),multiply(multiply(X0,inverse(X2)),X3)) = multiply(inverse(X2),X3),
    inference(forward_demodulation,[status(thm)],[f4942,f5595]) ).

fof(f5734,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,multiply(X1,X2)) = multiply(multiply(inverse(X3),X3),multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(X1),multiply(multiply(inverse(X5),X5),inverse(X0))))),X2)),
    inference(paramodulation,[status(thm)],[f4942,f5538]) ).

fof(f5761,plain,
    ! [X0,X1,X2,X3,X4] : multiply(multiply(multiply(inverse(X0),X0),inverse(inverse(inverse(X1)))),X2) = inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(multiply(inverse(X4),X4),X2))),X1)),
    inference(paramodulation,[status(thm)],[f5538,f5440]) ).

fof(f5768,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(multiply(inverse(X0),X0),X1)),multiply(X2,X3)) = multiply(inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(X2)),X1)),X3),
    inference(paramodulation,[status(thm)],[f5538,f2949]) ).

fof(f5784,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(X1,X2)) = multiply(multiply(inverse(multiply(multiply(inverse(X3),X3),inverse(X0))),X1),X2),
    inference(forward_demodulation,[status(thm)],[f5537,f5734]) ).

fof(f5861,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,multiply(X1,multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X3),multiply(inverse(multiply(multiply(inverse(X4),X4),inverse(X0))),X1)))),X5))) = multiply(X3,X5),
    inference(paramodulation,[status(thm)],[f4942,f5784]) ).

fof(f5865,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(inverse(inverse(X0)),X1),X2) = multiply(X0,multiply(multiply(multiply(inverse(X3),X3),X1),X2)),
    inference(paramodulation,[status(thm)],[f2949,f5784]) ).

fof(f5869,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,multiply(multiply(multiply(multiply(inverse(X1),X1),inverse(inverse(multiply(multiply(inverse(X2),X2),inverse(X0))))),X3),X4)) = multiply(multiply(multiply(inverse(X5),X5),X3),X4),
    inference(paramodulation,[status(thm)],[f5538,f5784]) ).

fof(f5870,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,multiply(multiply(inverse(X1),X1),X2)) = multiply(multiply(inverse(multiply(multiply(inverse(X3),X3),inverse(X0))),multiply(inverse(X4),X4)),X2),
    inference(paramodulation,[status(thm)],[f5254,f5784]) ).

fof(f5898,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(multiply(inverse(X1),X1),X2)) = multiply(X0,multiply(multiply(inverse(X3),X3),X2)),
    inference(forward_demodulation,[status(thm)],[f5784,f5870]) ).

fof(f5900,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(X1),X1),inverse(X0))),inverse(X2)),X2)),multiply(X3,X4))) = multiply(X3,X4),
    inference(forward_demodulation,[status(thm)],[f5596,f5861]) ).

fof(f5901,plain,
    ! [X0,X1,X2,X3] : multiply(X0,X1) = multiply(X2,multiply(inverse(multiply(X2,multiply(inverse(X3),X3))),multiply(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f5784,f5900]) ).

fof(f5908,plain,
    ! [X0,X1,X2] : multiply(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X0))),X2) = multiply(X1,X2),
    inference(backward_demodulation,[status(thm)],[f5865,f4942]) ).

fof(f5913,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(inverse(inverse(inverse(X0))),inverse(multiply(inverse(X1),X2))),X3) = multiply(inverse(multiply(X2,X0)),multiply(X1,X3)),
    inference(backward_demodulation,[status(thm)],[f5865,f5550]) ).

fof(f5962,plain,
    ! [X0,X1,X2,X3] : inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X1),X2))))),inverse(multiply(inverse(inverse(X3)),X1))),X3)) = X2,
    inference(backward_demodulation,[status(thm)],[f5865,f5497]) ).

fof(f5975,plain,
    ! [X0,X1,X2,X3,X4,X5] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(X1),inverse(X0))),X2))),X0)) = multiply(X3,inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(X2)),multiply(multiply(inverse(inverse(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(X5),X1))))),inverse(multiply(inverse(multiply(X3,inverse(X4))),X5))),X4)))),
    inference(backward_demodulation,[status(thm)],[f5865,f2706]) ).

fof(f6412,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(X0),X0)),X1) = multiply(X2,multiply(inverse(multiply(X2,multiply(inverse(X3),X3))),X1)),
    inference(paramodulation,[status(thm)],[f2934,f5901]) ).

fof(f6452,plain,
    ! [X0,X1,X2] : X0 = multiply(X1,multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),X0)),
    inference(forward_demodulation,[status(thm)],[f2934,f6412]) ).

fof(f6498,plain,
    ! [X0,X1,X2,X3,X4] : X0 = multiply(X1,multiply(X2,multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(X3),X3),inverse(X1))),X2),multiply(inverse(X4),X4))),X0))),
    inference(paramodulation,[status(thm)],[f5784,f6452]) ).

fof(f6560,plain,
    ! [X0,X1,X2,X3] : X0 = multiply(X1,multiply(X2,multiply(inverse(multiply(X1,multiply(X2,multiply(inverse(X3),X3)))),X0))),
    inference(forward_demodulation,[status(thm)],[f5784,f6498]) ).

fof(f6989,plain,
    ! [X0,X1,X2,X3,X4] : multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(inverse(multiply(X1,multiply(inverse(X2),X2)))),X3))),multiply(X1,multiply(X3,X4))) = X4,
    inference(paramodulation,[status(thm)],[f5440,f6560]) ).

fof(f7141,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(multiply(inverse(X0),X0),X1),X2) = multiply(multiply(inverse(inverse(inverse(multiply(inverse(X3),X3)))),X1),X2),
    inference(paramodulation,[status(thm)],[f2934,f5865]) ).

fof(f7149,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(multiply(inverse(inverse(X0)),X1),multiply(multiply(multiply(inverse(X2),X2),X3),X4)) = multiply(X0,multiply(multiply(inverse(inverse(multiply(multiply(inverse(X5),X5),X1))),X3),X4)),
    inference(paramodulation,[status(thm)],[f5865,f5865]) ).

fof(f7189,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X0),X0),X1),X2)))),X1),X3) = multiply(inverse(X2),X3),
    inference(paramodulation,[status(thm)],[f5865,f2949]) ).

fof(f7280,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(inverse(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),inverse(X2)))),inverse(multiply(inverse(X3),X4))))),inverse(multiply(inverse(multiply(X0,inverse(X1))),X3))),X1))) = inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(X4),inverse(X5))),X2))),X5)),
    inference(backward_demodulation,[status(thm)],[f7283,f5975]) ).

fof(f7283,plain,
    ! [X0,X1,X2,X3,X4] : multiply(multiply(inverse(inverse(multiply(inverse(inverse(X0)),X1))),X2),X3) = multiply(X0,multiply(multiply(inverse(inverse(multiply(multiply(inverse(X4),X4),X1))),X2),X3)),
    inference(forward_demodulation,[status(thm)],[f5865,f7149]) ).

fof(f7341,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : X0 = multiply(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),X2))),inverse(multiply(multiply(inverse(X1),X1),X2))),inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),inverse(inverse(multiply(multiply(inverse(X1),X1),X2))))),X5))),inverse(multiply(multiply(multiply(inverse(multiply(multiply(inverse(X1),X1),X2)),multiply(multiply(inverse(X1),X1),X2)),inverse(multiply(multiply(X3,inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(X5)),X4))),X0))),multiply(multiply(inverse(X6),X6),X2)))),
    inference(paramodulation,[status(thm)],[f5898,f40]) ).

fof(f7471,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : X0 = multiply(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),X2))),inverse(multiply(multiply(inverse(X1),X1),X2))),inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),inverse(inverse(multiply(multiply(inverse(X1),X1),X2))))),X5))),inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(multiply(X3,inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(X5)),X4))),X0))),multiply(multiply(inverse(X6),X6),X2)))),
    inference(forward_demodulation,[status(thm)],[f2949,f7341]) ).

fof(f7590,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(X0,X1)),multiply(multiply(multiply(inverse(X2),X2),X3),X4)) = multiply(inverse(multiply(inverse(X5),X1)),multiply(multiply(inverse(inverse(inverse(multiply(X0,X5)))),X3),X4)),
    inference(paramodulation,[status(thm)],[f5865,f3572]) ).

fof(f7684,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(inverse(X0),X1)),multiply(multiply(inverse(inverse(inverse(multiply(X2,X0)))),X3),X4)) = multiply(multiply(inverse(inverse(inverse(multiply(X2,X1)))),X3),X4),
    inference(forward_demodulation,[status(thm)],[f5865,f7590]) ).

fof(f7875,plain,
    ! [X0,X1,X2,X3] : X0 = multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(multiply(multiply(inverse(inverse(X2)),inverse(X2)),inverse(X0)),multiply(inverse(X3),X3)))),
    inference(paramodulation,[status(thm)],[f5254,f3745]) ).

fof(f7885,plain,
    ! [X0,X1,X2,X3,X4] : X0 = multiply(inverse(inverse(X1)),inverse(multiply(multiply(multiply(inverse(X2),inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(inverse(X4)),X2))),X4))),inverse(X0)),X1))),
    inference(paramodulation,[status(thm)],[f5440,f3745]) ).

fof(f7895,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(X0),inverse(multiply(multiply(multiply(inverse(inverse(X1)),inverse(X1)),inverse(X2)),X3))) = multiply(inverse(multiply(inverse(inverse(X3)),X0)),X2),
    inference(paramodulation,[status(thm)],[f3745,f2949]) ).

fof(f7903,plain,
    ! [X0,X1,X2] : X0 = multiply(inverse(inverse(X1)),inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X0)),X1))),
    inference(forward_demodulation,[status(thm)],[f5440,f7885]) ).

fof(f7905,plain,
    ! [X0,X1,X2] : X0 = multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X2),X2)))),X0),
    inference(forward_demodulation,[status(thm)],[f7895,f7875]) ).

fof(f7945,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X4)))) = multiply(inverse(multiply(inverse(multiply(X1,inverse(X4))),X0)),X3),
    inference(paramodulation,[status(thm)],[f7903,f3586]) ).

fof(f7946,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(X0,inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X3)))),X4) = multiply(inverse(X2),multiply(inverse(multiply(X0,inverse(X3))),X4)),
    inference(paramodulation,[status(thm)],[f7903,f3572]) ).

fof(f7951,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(inverse(X0)),X1)),X2) = multiply(inverse(X1),inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X2)),X0))),
    inference(paramodulation,[status(thm)],[f7903,f2949]) ).

fof(f7952,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(inverse(inverse(X1)),X2)) = multiply(inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X0)),X1))),X2),
    inference(paramodulation,[status(thm)],[f7903,f2949]) ).

fof(f8042,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(inverse(multiply(X1,multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X3),X3))))),X4)) = multiply(inverse(multiply(X1,X0)),X4),
    inference(paramodulation,[status(thm)],[f7905,f3572]) ).

fof(f8782,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(multiply(multiply(inverse(inverse(X0)),inverse(X0)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X2),X2)))),inverse(X3))),inverse(inverse(X0)))),X4))),inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(X5)),X0))) = inverse(multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X4)),X3)),inverse(X6))),X5))),X6)),
    inference(paramodulation,[status(thm)],[f7905,f25]) ).

fof(f8893,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(multiply(multiply(inverse(inverse(X0)),inverse(X0)),inverse(multiply(inverse(inverse(inverse(X0))),multiply(inverse(multiply(inverse(inverse(X1)),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X3),X3))))),X4)))),inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(X5)),X0))) = inverse(multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X4)),X1)),inverse(X6))),X5))),X6)),
    inference(forward_demodulation,[status(thm)],[f4127,f8782]) ).

fof(f8894,plain,
    ! [X0,X1,X2,X3,X4] : multiply(multiply(multiply(inverse(inverse(X0)),inverse(X0)),inverse(multiply(inverse(multiply(inverse(inverse(X1)),inverse(inverse(X0)))),X2))),inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(X3)),X0))) = inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X1)),inverse(X4))),X3))),X4)),
    inference(forward_demodulation,[status(thm)],[f8042,f8893]) ).

fof(f10655,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(multiply(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),X3),X4)))),X3),X4),inverse(X5)),multiply(multiply(multiply(inverse(X2),X2),X3),X4)))))),inverse(X0))),X6))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X7),X7),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(X6)),inverse(multiply(multiply(multiply(inverse(X2),X2),X3),X4)))),inverse(X7))),X5))),X7)))),
    inference(paramodulation,[status(thm)],[f5865,f4080]) ).

fof(f10727,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))))),inverse(X0))),X4))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(multiply(X5,multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(inverse(X7)),X5))),X7)),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X4)),inverse(X2))),inverse(multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(inverse(X7)),X5))),X7)))),X3))),multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(inverse(X7)),X5))),X7))))),
    inference(paramodulation,[status(thm)],[f5440,f4080]) ).

fof(f10789,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(inverse(X3)),X4))),X3)),multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(inverse(X3)),X4))),X3)),inverse(X5)),multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(inverse(X3)),X4))),X3)))))),inverse(X0))),X6))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X7),X7),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(X6)),X4)),inverse(X7))),X5))),X7)))),
    inference(paramodulation,[status(thm)],[f5440,f4080]) ).

fof(f10843,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(X2)),inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X4)),X3))))),inverse(X1))),X5))),X1)))),X2)) = inverse(inverse(multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(X5)),inverse(X3))),inverse(X6))),X4))),X6))),
    inference(paramodulation,[status(thm)],[f4080,f5440]) ).

fof(f10874,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(multiply(inverse(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),inverse(X3))),inverse(X0))),X1))),X0))))),inverse(inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X5),inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X1)),X3))))),inverse(X4))),X2))),X4)))),X6) = multiply(X5,X6),
    inference(paramodulation,[status(thm)],[f4080,f5908]) ).

fof(f10911,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(inverse(X1)),multiply(inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2)))),inverse(X4))),X5)))),X1)))),X4)) = inverse(inverse(multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X5)),inverse(X2))),inverse(X6))),X3))),X6))),
    inference(forward_demodulation,[status(thm)],[f4127,f10843]) ).

fof(f10912,plain,
    ! [X0,X1,X2,X3,X4,X5] : inverse(inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),inverse(X3))),inverse(X0))),X1))),X0))) = inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X1)),X3)))),inverse(X5))),X2))),X5)),
    inference(forward_demodulation,[status(thm)],[f5440,f10911]) ).

fof(f10933,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(multiply(inverse(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),inverse(X3))),inverse(X0))),X1))),X0))))),inverse(inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(inverse(X4)),multiply(inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X1)),X3)))),X5)),X2)))),X4)))),X6) = multiply(X5,X6),
    inference(forward_demodulation,[status(thm)],[f4127,f10874]) ).

fof(f10934,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(multiply(inverse(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),inverse(X3))),inverse(X0))),X1))),X0))))),inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X1)),X3)))),X4)),X2))),X5) = multiply(X4,X5),
    inference(forward_demodulation,[status(thm)],[f5440,f10933]) ).

fof(f10935,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(X0,inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X0)),inverse(X3))),inverse(X1))),X2))),X1)))),multiply(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X2)),X3)))),X4),X5)) = multiply(X4,X5),
    inference(forward_demodulation,[status(thm)],[f5913,f10934]) ).

fof(f10936,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(X1)),inverse(X2))),inverse(X3))),X0)),multiply(inverse(multiply(X1,inverse(X3))),multiply(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X0)),X2)))),X4),X5))) = multiply(X4,X5),
    inference(forward_demodulation,[status(thm)],[f7946,f10935]) ).

fof(f10937,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(X1)),multiply(multiply(multiply(inverse(X0),X0),inverse(X2)),inverse(X3)))),multiply(inverse(multiply(X2,inverse(X1))),multiply(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X0)),X3)))),X4),X5)))) = multiply(X4,X5),
    inference(forward_demodulation,[status(thm)],[f4127,f10936]) ).

fof(f10938,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(inverse(multiply(X1,multiply(multiply(multiply(inverse(X0),X0),inverse(X1)),inverse(X2)))),multiply(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X0)),X2)))),X3),X4))) = multiply(X3,X4),
    inference(forward_demodulation,[status(thm)],[f3572,f10937]) ).

fof(f10939,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(inverse(multiply(multiply(inverse(inverse(X1)),inverse(X1)),inverse(X2))),multiply(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X0)),X2)))),X3),X4))) = multiply(X3,X4),
    inference(forward_demodulation,[status(thm)],[f5865,f10938]) ).

fof(f11013,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),X3),X4)))),X3),X4),inverse(X5)))),X3),X4))))),inverse(X0))),X6))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X7),X7),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(X6)),inverse(multiply(multiply(multiply(inverse(X2),X2),X3),X4)))),inverse(X7))),X5))),X7)))),
    inference(forward_demodulation,[status(thm)],[f5865,f10655]) ).

fof(f11014,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X2),X2),inverse(X3)))),X4),X2))))),inverse(X0))),X5))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X5)),inverse(multiply(multiply(multiply(inverse(X7),X7),X4),X2)))),inverse(X6))),X3))),X6)))),
    inference(forward_demodulation,[status(thm)],[f7189,f11013]) ).

fof(f11053,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(inverse(X3)),X4))),X3)),multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(inverse(X3)),X4))),X3)),inverse(X5)))),inverse(multiply(inverse(inverse(X3)),X4))),X3))))),inverse(X0))),X6))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X7),X7),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(X6)),X4)),inverse(X7))),X5))),X7)))),
    inference(forward_demodulation,[status(thm)],[f5865,f10789]) ).

fof(f11054,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,inverse(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X4)),inverse(X1))),X2))),X1)))) = inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X6),X6),inverse(X2)))),inverse(multiply(inverse(inverse(X6)),X4))),X6))))),inverse(X5))),X3))),X5)),
    inference(forward_demodulation,[status(thm)],[f2949,f11053]) ).

fof(f11323,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))))),inverse(X0))),X4))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(X5,multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(inverse(X7)),X5))),X7)),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X4)),inverse(X2))),inverse(multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(inverse(X7)),X5))),X7)))),X3))))),inverse(multiply(inverse(inverse(X7)),X5))),X7)))),
    inference(forward_demodulation,[status(thm)],[f5865,f10727]) ).

fof(f11324,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))))),inverse(X0))),X4))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(multiply(inverse(inverse(X5)),inverse(multiply(inverse(inverse(X6)),X5))),X6),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X4)),inverse(X2))),inverse(multiply(multiply(multiply(inverse(X7),X7),inverse(multiply(inverse(inverse(X6)),X5))),X6)))),X3))))),inverse(multiply(inverse(inverse(X6)),X5))),X6)))),
    inference(forward_demodulation,[status(thm)],[f5865,f11323]) ).

fof(f11325,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))))),inverse(X0))),X4))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X4)),inverse(X2))),inverse(multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(inverse(X5)),X7))),X5)))),X3))))),inverse(multiply(inverse(inverse(X5)),X7))),X5)))),
    inference(forward_demodulation,[status(thm)],[f5908,f11324]) ).

fof(f11326,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))))),inverse(X0))),X4))),X0)) = multiply(X1,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(inverse(X5)),X6)),multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X4)),inverse(X2))),inverse(X5))),X3)))))),inverse(multiply(inverse(inverse(X5)),X6))),X5)))),
    inference(forward_demodulation,[status(thm)],[f7946,f11325]) ).

fof(f11327,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),inverse(X4))),X5)),X2))))),inverse(multiply(inverse(inverse(X1)),X5))),X1)))) = inverse(multiply(multiply(multiply(inverse(X6),X6),inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(X2)),X4))))),inverse(X6))),X3))),X6)),
    inference(forward_demodulation,[status(thm)],[f3572,f11326]) ).

fof(f11581,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(X0),X0)),multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X3)) = multiply(inverse(X2),X3),
    inference(paramodulation,[status(thm)],[f5099,f5692]) ).

fof(f11651,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(multiply(X0,inverse(X1)),X2)),multiply(multiply(X0,inverse(X3)),X4)) = multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(X3),X4)),
    inference(paramodulation,[status(thm)],[f5692,f3586]) ).

fof(f11749,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : X0 = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),inverse(inverse(multiply(multiply(inverse(X3),X3),X4))))),X5)),inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X5)),X2))),X0))),multiply(multiply(inverse(X6),X6),X4)))),
    inference(backward_demodulation,[status(thm)],[f12157,f7471]) ).

fof(f11772,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(inverse(X1)))),X2)),inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X3)),X1))) = inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(X2)),X0)),inverse(X4))),X3))),X4)),
    inference(backward_demodulation,[status(thm)],[f12157,f8894]) ).

fof(f11842,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(inverse(inverse(X0))),X1) = inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(multiply(multiply(inverse(X3),X3),X1))),X0)),
    inference(backward_demodulation,[status(thm)],[f12157,f5761]) ).

fof(f11846,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,multiply(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),inverse(X0)))),X2),X3)) = multiply(multiply(multiply(inverse(X4),X4),X2),X3),
    inference(backward_demodulation,[status(thm)],[f12157,f5869]) ).

fof(f11878,plain,
    ! [X0,X1,X2,X3] : X0 = multiply(inverse(multiply(inverse(inverse(multiply(X1,multiply(inverse(X2),X2)))),X3)),multiply(X1,multiply(X3,X0))),
    inference(backward_demodulation,[status(thm)],[f12157,f6989]) ).

fof(f11909,plain,
    ! [X0,X1,X2,X3,X4] : inverse(inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),inverse(X3))),inverse(X0))),X1))),X0))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X1)),X3)))),inverse(X4))),X2)),X4)),
    inference(backward_demodulation,[status(thm)],[f12157,f10912]) ).

fof(f11931,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X2),X2),inverse(X3)))),X4),X2))))),inverse(X0))),X5))),X0)) = multiply(X1,inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X5)),inverse(multiply(multiply(multiply(inverse(X6),X6),X4),X2)))),inverse(X7))),X3)),X7)))),
    inference(backward_demodulation,[status(thm)],[f12157,f11014]) ).

fof(f12006,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X3)),inverse(X4))),X1)),X4)))) = inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X6),X6),inverse(X1)))),inverse(multiply(inverse(inverse(X6)),X3))),X6))))),inverse(X5))),X2))),X5)),
    inference(backward_demodulation,[status(thm)],[f12157,f11054]) ).

fof(f12018,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),inverse(X4))),X5)),X2))))),inverse(multiply(inverse(inverse(X1)),X5))),X1)))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(X2)),X4))))),inverse(X6))),X3)),X6)),
    inference(backward_demodulation,[status(thm)],[f12157,f11327]) ).

fof(f12029,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X3))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X3))),inverse(X4))),X2)),X4)),
    inference(backward_demodulation,[status(thm)],[f12157,f5104]) ).

fof(f12034,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(inverse(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),inverse(X2)))),inverse(multiply(inverse(X3),X4))))),inverse(multiply(inverse(multiply(X0,inverse(X1))),X3))),X1))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(X4),inverse(X5))),X2)),X5)),
    inference(backward_demodulation,[status(thm)],[f12157,f7280]) ).

fof(f12076,plain,
    ! [X0,X1,X2] : X0 = multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),X0)),X2))),
    inference(backward_demodulation,[status(thm)],[f12157,f5106]) ).

fof(f12083,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,X1)),multiply(X2,X3)) = multiply(inverse(multiply(inverse(multiply(inverse(X0),X2)),X1)),X3),
    inference(backward_demodulation,[status(thm)],[f12157,f5551]) ).

fof(f12091,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(inverse(multiply(multiply(inverse(inverse(X1)),inverse(X1)),inverse(X2))),multiply(multiply(inverse(inverse(inverse(multiply(inverse(X0),X2)))),X3),X4))) = multiply(X3,X4),
    inference(backward_demodulation,[status(thm)],[f12157,f10939]) ).

fof(f12103,plain,
    ! [X0,X1,X2] : multiply(inverse(X0),inverse(multiply(inverse(X1),X2))) = multiply(inverse(multiply(inverse(inverse(X2)),X0)),X1),
    inference(backward_demodulation,[status(thm)],[f12157,f7951]) ).

fof(f12104,plain,
    ! [X0,X1,X2] : multiply(inverse(inverse(multiply(inverse(X0),X1))),X2) = multiply(inverse(X0),multiply(inverse(inverse(X1)),X2)),
    inference(backward_demodulation,[status(thm)],[f12157,f7952]) ).

fof(f12106,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),X2)),X3) = multiply(inverse(X2),multiply(X0,inverse(multiply(inverse(X3),X1)))),
    inference(backward_demodulation,[status(thm)],[f12157,f7945]) ).

fof(f12132,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(X0),X1)),X2) = multiply(inverse(multiply(multiply(inverse(X3),X3),X1)),multiply(X0,X2)),
    inference(backward_demodulation,[status(thm)],[f12157,f5768]) ).

fof(f12157,plain,
    ! [X0,X1,X2] : multiply(inverse(X0),X1) = multiply(multiply(multiply(inverse(X2),X2),inverse(X0)),X1),
    inference(forward_demodulation,[status(thm)],[f2934,f11581]) ).

fof(f12167,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),X2)),X3)) = multiply(inverse(multiply(X2,X0)),multiply(X1,X3)),
    inference(forward_demodulation,[status(thm)],[f4127,f12083]) ).

fof(f12311,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(inverse(X0),X1)))),X2)),inverse(X1))),X3)) = multiply(X2,X3),
    inference(backward_demodulation,[status(thm)],[f12132,f12091]) ).

fof(f12317,plain,
    ! [X0,X1,X2] : X0 = multiply(X1,inverse(multiply(inverse(X0),multiply(X1,inverse(multiply(inverse(X2),X2)))))),
    inference(forward_demodulation,[status(thm)],[f12106,f12076]) ).

fof(f12363,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(X0),X1)),multiply(multiply(inverse(inverse(inverse(multiply(inverse(X1),X0)))),X2),X3)) = multiply(X2,X3),
    inference(forward_demodulation,[status(thm)],[f12167,f12311]) ).

fof(f12365,plain,
    ! [X0,X1,X2] : multiply(multiply(multiply(inverse(X0),X0),X1),X2) = multiply(X1,X2),
    inference(backward_demodulation,[status(thm)],[f12366,f7141]) ).

fof(f12366,plain,
    ! [X0,X1,X2] : multiply(X0,X1) = multiply(multiply(inverse(inverse(inverse(multiply(inverse(X2),X2)))),X0),X1),
    inference(forward_demodulation,[status(thm)],[f7684,f12363]) ).

fof(f12636,plain,
    ! [X0,X1,X2] : multiply(multiply(inverse(inverse(X0)),X1),X2) = multiply(X0,multiply(X1,X2)),
    inference(backward_demodulation,[status(thm)],[f12365,f5865]) ).

fof(f13101,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(multiply(inverse(X0),X0),X1)),X2)) = multiply(inverse(inverse(inverse(X2))),X1),
    inference(forward_demodulation,[status(thm)],[f12157,f11842]) ).

fof(f13193,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : X0 = multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(inverse(multiply(multiply(inverse(X2),X2),X3)))),multiply(X4,inverse(X5)))),inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(multiply(X4,inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(X1)),X5))),X0))),multiply(multiply(inverse(X6),X6),X3))))),
    inference(forward_demodulation,[status(thm)],[f4127,f11749]) ).

fof(f13194,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : X0 = multiply(inverse(multiply(multiply(X1,inverse(X2)),X3)),multiply(inverse(inverse(multiply(multiply(inverse(X4),X4),X5))),inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))),X0))),multiply(multiply(inverse(X6),X6),X5))))),
    inference(forward_demodulation,[status(thm)],[f12167,f13193]) ).

fof(f13195,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : X0 = multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),X2))),inverse(multiply(multiply(inverse(X3),X3),X2)))),multiply(multiply(X4,inverse(X5)),X6))),multiply(multiply(X4,inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(X6)),X5))),X0)),
    inference(forward_demodulation,[status(thm)],[f7945,f13194]) ).

fof(f13196,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : X0 = multiply(inverse(multiply(multiply(X1,inverse(X2)),X3)),multiply(inverse(multiply(inverse(inverse(multiply(multiply(inverse(X4),X4),X5))),inverse(multiply(multiply(inverse(X6),X6),X5)))),multiply(multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))),X0))),
    inference(forward_demodulation,[status(thm)],[f4127,f13195]) ).

fof(f13197,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : X0 = multiply(inverse(multiply(inverse(multiply(multiply(inverse(X1),X1),X2)),multiply(multiply(X3,inverse(X4)),X5))),multiply(inverse(multiply(multiply(inverse(X6),X6),X2)),multiply(multiply(X3,inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(X5)),X4))),X0))),
    inference(forward_demodulation,[status(thm)],[f12167,f13196]) ).

fof(f13198,plain,
    ! [X0,X1,X2,X3,X4,X5] : X0 = multiply(multiply(inverse(inverse(inverse(multiply(multiply(X1,inverse(X2)),X3)))),X4),multiply(inverse(multiply(multiply(inverse(X5),X5),X4)),multiply(multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2))),X0))),
    inference(forward_demodulation,[status(thm)],[f13101,f13197]) ).

fof(f13199,plain,
    ! [X0,X1,X2,X3,X4] : X0 = multiply(multiply(inverse(inverse(inverse(multiply(multiply(X1,inverse(X2)),X3)))),X4),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2)))),X4)),X0)),
    inference(forward_demodulation,[status(thm)],[f12132,f13198]) ).

fof(f13200,plain,
    ! [X0,X1,X2,X3,X4] : X0 = multiply(multiply(inverse(inverse(inverse(multiply(multiply(X1,inverse(X2)),X3)))),X4),multiply(inverse(X4),multiply(X1,inverse(multiply(inverse(X0),multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2)))))),
    inference(forward_demodulation,[status(thm)],[f12106,f13199]) ).

fof(f13201,plain,
    ! [X0,X1,X2,X3,X4] : X0 = multiply(multiply(inverse(inverse(inverse(multiply(multiply(X1,inverse(X2)),X3)))),X4),multiply(inverse(X4),multiply(X1,inverse(multiply(multiply(inverse(inverse(inverse(X0))),inverse(X3)),X2))))),
    inference(forward_demodulation,[status(thm)],[f5865,f13200]) ).

fof(f13261,plain,
    ! [X0,X1,X2,X3,X4] : inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(X1)),inverse(X2))),inverse(X3))),X0)),X3))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X0)),X2)))),inverse(X4))),X1)),X4)),
    inference(forward_demodulation,[status(thm)],[f12157,f11909]) ).

fof(f13262,plain,
    ! [X0,X1,X2,X3,X4] : inverse(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(X1)),multiply(multiply(multiply(inverse(X0),X0),inverse(X2)),inverse(X3)))),X1)))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X0)),X3)))),inverse(X4))),X2)),X4)),
    inference(forward_demodulation,[status(thm)],[f4127,f13261]) ).

fof(f13263,plain,
    ! [X0,X1,X2,X3,X4] : inverse(inverse(multiply(inverse(multiply(multiply(multiply(multiply(inverse(X0),X0),inverse(X1)),inverse(X2)),X0)),multiply(inverse(X3),X3)))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X0)),X2)))),inverse(X4))),X1)),X4)),
    inference(forward_demodulation,[status(thm)],[f12167,f13262]) ).

fof(f13264,plain,
    ! [X0,X1,X2,X3,X4] : inverse(inverse(multiply(inverse(multiply(multiply(inverse(X0),inverse(X1)),X2)),multiply(inverse(X3),X3)))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X1)))),inverse(X4))),X0)),X4)),
    inference(forward_demodulation,[status(thm)],[f12157,f13263]) ).

fof(f13265,plain,
    ! [X0,X1,X2,X3,X4] : inverse(inverse(multiply(inverse(multiply(multiply(inverse(X0),inverse(X1)),X2)),multiply(inverse(X3),X3)))) = inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(X4)),inverse(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X1))))),X4))),
    inference(forward_demodulation,[status(thm)],[f4127,f13264]) ).

fof(f13266,plain,
    ! [X0,X1,X2,X3,X4] : inverse(inverse(multiply(inverse(multiply(multiply(inverse(X0),inverse(X1)),X2)),multiply(inverse(X3),X3)))) = inverse(multiply(inverse(multiply(inverse(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X1))),X0)),multiply(inverse(X4),X4))),
    inference(forward_demodulation,[status(thm)],[f12167,f13265]) ).

fof(f13267,plain,
    ! [X0,X1,X2,X3] : inverse(inverse(multiply(inverse(multiply(multiply(inverse(X0),inverse(X1)),X2)),multiply(inverse(X3),X3)))) = inverse(multiply(inverse(X0),inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X1)))),
    inference(forward_demodulation,[status(thm)],[f5214,f13266]) ).

fof(f13272,plain,
    ! [X0,X1,X2,X3] : inverse(inverse(multiply(inverse(multiply(multiply(inverse(X0),inverse(X1)),X2)),multiply(inverse(X3),X3)))) = inverse(multiply(inverse(multiply(inverse(inverse(X1)),X0)),X2)),
    inference(forward_demodulation,[status(thm)],[f7951,f13267]) ).

fof(f13698,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),inverse(X2)))),X3),X1))))),inverse(X4))),X5)),X4)) = multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X5)),inverse(multiply(multiply(multiply(inverse(X6),X6),X3),X1)))),inverse(X7))),X2)),X7)))),
    inference(forward_demodulation,[status(thm)],[f12157,f11931]) ).

fof(f13699,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(X1)),multiply(X2,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X3),X3),inverse(X4)))),X5),X3)))))),X1))) = multiply(X2,inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(X0)),inverse(multiply(multiply(multiply(inverse(X6),X6),X5),X3)))),inverse(X7))),X4)),X7)))),
    inference(forward_demodulation,[status(thm)],[f4127,f13698]) ).

fof(f13700,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(inverse(multiply(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),inverse(X2)))),X3),X1)))),X4)),multiply(inverse(X5),X5))) = multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X4)),inverse(multiply(multiply(multiply(inverse(X6),X6),X3),X1)))),inverse(X7))),X2)),X7)))),
    inference(forward_demodulation,[status(thm)],[f12167,f13699]) ).

fof(f13701,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(inverse(multiply(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),inverse(X2)))),X3),X1)))),X4)),multiply(inverse(X5),X5))) = multiply(X0,inverse(inverse(multiply(inverse(X2),multiply(inverse(multiply(inverse(inverse(X6)),multiply(multiply(multiply(inverse(X2),X2),inverse(X4)),inverse(multiply(multiply(multiply(inverse(X7),X7),X3),X1))))),X6))))),
    inference(forward_demodulation,[status(thm)],[f4127,f13700]) ).

fof(f13702,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(inverse(multiply(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),inverse(X2)))),X3),X1)))),X4)),multiply(inverse(X5),X5))) = multiply(X0,inverse(inverse(multiply(inverse(multiply(multiply(multiply(multiply(inverse(X2),X2),inverse(X4)),inverse(multiply(multiply(multiply(inverse(X6),X6),X3),X1))),X2)),multiply(inverse(X7),X7))))),
    inference(forward_demodulation,[status(thm)],[f12167,f13701]) ).

fof(f13703,plain,
    ! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(inverse(multiply(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),inverse(X2)))),X3),X1)))),X4)),multiply(inverse(X5),X5))) = multiply(X0,inverse(inverse(multiply(inverse(multiply(multiply(inverse(X4),inverse(multiply(multiply(multiply(inverse(X6),X6),X3),X1))),X2)),multiply(inverse(X7),X7))))),
    inference(forward_demodulation,[status(thm)],[f12157,f13702]) ).

fof(f13704,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(inverse(multiply(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),inverse(X2)))),X3),X1)))),X4)),multiply(inverse(X5),X5))) = multiply(X0,inverse(multiply(inverse(multiply(inverse(inverse(multiply(multiply(multiply(inverse(X6),X6),X3),X1))),X4)),X2))),
    inference(forward_demodulation,[status(thm)],[f13272,f13703]) ).

fof(f13705,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(inverse(multiply(inverse(inverse(multiply(X1,X2))),X3)),X4))) = inverse(multiply(inverse(multiply(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X2),X2),inverse(X4)))),X1),X2)))),X3)),multiply(inverse(X5),X5))),
    inference(forward_demodulation,[status(thm)],[f12365,f13704]) ).

fof(f13706,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(X0),multiply(inverse(multiply(inverse(inverse(inverse(X1))),inverse(X2))),inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X3)),X1)))) = inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X0)),X2)),inverse(X4))),X3))),X4)),
    inference(forward_demodulation,[status(thm)],[f4127,f11772]) ).

fof(f13707,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(inverse(X0),X1)),multiply(inverse(inverse(X2)),inverse(multiply(multiply(multiply(inverse(X2),X2),inverse(X3)),X2)))) = inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(X1)),X0)),inverse(X4))),X3))),X4)),
    inference(forward_demodulation,[status(thm)],[f12167,f13706]) ).

fof(f13708,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(X1),X2))),X3) = inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X1)),inverse(X4))),X3))),X4)),
    inference(forward_demodulation,[status(thm)],[f7945,f13707]) ).

fof(f13709,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(inverse(X0),X1)),multiply(inverse(multiply(inverse(inverse(X2)),inverse(X2))),X3)) = inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(X1)),X0)),inverse(X4))),X3))),X4)),
    inference(forward_demodulation,[status(thm)],[f4127,f13708]) ).

fof(f13710,plain,
    ! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(inverse(X0),multiply(inverse(X1),X2))),multiply(inverse(X0),X3)) = inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X1)),inverse(X4))),X3))),X4)),
    inference(forward_demodulation,[status(thm)],[f12167,f13709]) ).

fof(f13711,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(X0),X1)),X2) = inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(X1)),X0)),inverse(X3))),X2))),X3)),
    inference(forward_demodulation,[status(thm)],[f2949,f13710]) ).

fof(f13712,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(X0),X1)),X2) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(multiply(multiply(inverse(X0),X0),inverse(X1)),X0)),inverse(X3))),X2)),X3)),
    inference(forward_demodulation,[status(thm)],[f12157,f13711]) ).

fof(f13713,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(X0),X1)),X2) = inverse(multiply(inverse(X2),multiply(inverse(multiply(inverse(inverse(X3)),multiply(multiply(multiply(inverse(X0),X0),inverse(X1)),X0))),X3))),
    inference(forward_demodulation,[status(thm)],[f4127,f13712]) ).

fof(f13714,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(X0),X1)),X2) = inverse(multiply(inverse(multiply(multiply(multiply(multiply(inverse(X0),X0),inverse(X1)),X0),X2)),multiply(inverse(X3),X3))),
    inference(forward_demodulation,[status(thm)],[f12167,f13713]) ).

fof(f13718,plain,
    ! [X0,X1,X2,X3] : inverse(multiply(inverse(multiply(multiply(inverse(X0),X1),X2)),multiply(inverse(X3),X3))) = multiply(inverse(multiply(inverse(X1),X0)),X2),
    inference(forward_demodulation,[status(thm)],[f12157,f13714]) ).

fof(f13850,plain,
    ! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(X1),X2))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X2))),inverse(X3))),X1)),X3)),
    inference(forward_demodulation,[status(thm)],[f12157,f12029]) ).

fof(f13851,plain,
    ! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(X1),X2))) = inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(X3)),multiply(X0,inverse(X2)))),X3))),
    inference(forward_demodulation,[status(thm)],[f4127,f13850]) ).

fof(f13858,plain,
    ! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(X1),X2))) = inverse(multiply(inverse(multiply(multiply(X0,inverse(X2)),X1)),multiply(inverse(X3),X3))),
    inference(forward_demodulation,[status(thm)],[f12167,f13851]) ).

fof(f13888,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X2),multiply(multiply(multiply(inverse(X3),X3),inverse(X4)),inverse(multiply(inverse(X3),X5)))))))),inverse(multiply(inverse(inverse(X1)),X2))),X1)))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(X3)),X5))))),inverse(X6))),X4)),X6)),
    inference(forward_demodulation,[status(thm)],[f12106,f12018]) ).

fof(f13889,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),inverse(multiply(inverse(X1),X3))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X1)),X3))))),inverse(X4))),X2)),X4)),
    inference(forward_demodulation,[status(thm)],[f5962,f13888]) ).

fof(f13890,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X3))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X2)),X3))))),inverse(X4))),X1)),X4)),
    inference(forward_demodulation,[status(thm)],[f12157,f13889]) ).

fof(f13891,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X3))))) = inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(X4)),multiply(X0,inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X2)),X3)))))),X4))),
    inference(forward_demodulation,[status(thm)],[f4127,f13890]) ).

fof(f13892,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X3))))) = inverse(multiply(inverse(multiply(multiply(X0,inverse(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X2)),X3)))),X1)),multiply(inverse(X4),X4))),
    inference(forward_demodulation,[status(thm)],[f12167,f13891]) ).

fof(f13893,plain,
    ! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(inverse(X2),X3))))) = multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(X2)),X3))))),
    inference(forward_demodulation,[status(thm)],[f13858,f13892]) ).

fof(f13905,plain,
    ! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(multiply(inverse(inverse(X1)),X2)),X3))) = multiply(X0,inverse(multiply(inverse(X2),inverse(multiply(inverse(X3),X1))))),
    inference(forward_demodulation,[status(thm)],[f7951,f13893]) ).

fof(f14179,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(inverse(inverse(multiply(inverse(inverse(X0)),inverse(X0)))),X1),X2) = multiply(multiply(multiply(inverse(X3),X3),X1),X2),
    inference(forward_demodulation,[status(thm)],[f7283,f11846]) ).

fof(f14180,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(inverse(inverse(X0)),multiply(inverse(inverse(inverse(X0))),X1)),X2) = multiply(multiply(multiply(inverse(X3),X3),X1),X2),
    inference(forward_demodulation,[status(thm)],[f12104,f14179]) ).

fof(f14181,plain,
    ! [X0,X1,X2] : multiply(multiply(inverse(inverse(X0)),multiply(inverse(inverse(inverse(X0))),X1)),X2) = multiply(X1,X2),
    inference(forward_demodulation,[status(thm)],[f12365,f14180]) ).

fof(f14227,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,inverse(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(X2)),multiply(multiply(multiply(inverse(X1),X1),inverse(X3)),X4))),X2))))) = inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X6),X6),inverse(X1)))),inverse(multiply(inverse(inverse(X6)),X4))),X6))))),inverse(X5))),X3))),X5)),
    inference(forward_demodulation,[status(thm)],[f4127,f12006]) ).

fof(f14228,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,inverse(inverse(multiply(inverse(multiply(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),X3),X1)),multiply(inverse(X4),X4))))) = inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X6),X6),inverse(X1)))),inverse(multiply(inverse(inverse(X6)),X3))),X6))))),inverse(X5))),X2))),X5)),
    inference(forward_demodulation,[status(thm)],[f12167,f14227]) ).

fof(f14229,plain,
    ! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,inverse(inverse(multiply(inverse(multiply(multiply(inverse(X1),X2),X3)),multiply(inverse(X4),X4))))) = inverse(multiply(multiply(multiply(inverse(X5),X5),inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X6),X6),inverse(X3)))),inverse(multiply(inverse(inverse(X6)),X2))),X6))))),inverse(X5))),X1))),X5)),
    inference(forward_demodulation,[status(thm)],[f12157,f14228]) ).

fof(f14230,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),X2)),X3))) = inverse(multiply(multiply(multiply(inverse(X4),X4),inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X5),X5),inverse(X3)))),inverse(multiply(inverse(inverse(X5)),X1))),X5))))),inverse(X4))),X2))),X4)),
    inference(forward_demodulation,[status(thm)],[f13718,f14229]) ).

fof(f14231,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),X2)),X3))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X4),X4),inverse(X3)))),inverse(multiply(inverse(inverse(X4)),X1))),X4))))),inverse(X5))),X2)),X5)),
    inference(forward_demodulation,[status(thm)],[f12157,f14230]) ).

fof(f14232,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),X2)),X3))) = inverse(multiply(inverse(X2),multiply(inverse(multiply(inverse(inverse(X4)),multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X5),X5),inverse(X3)))),inverse(multiply(inverse(inverse(X5)),X1))),X5)))))),X4))),
    inference(forward_demodulation,[status(thm)],[f4127,f14231]) ).

fof(f14233,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),X2)),X3))) = inverse(multiply(inverse(multiply(multiply(X0,inverse(inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X4),X4),inverse(X3)))),inverse(multiply(inverse(inverse(X4)),X1))),X4)))),X2)),multiply(inverse(X5),X5))),
    inference(forward_demodulation,[status(thm)],[f12167,f14232]) ).

fof(f14234,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),X2)),X3))) = multiply(X0,inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(X4)),X1)),X4))),X2)),X3))),
    inference(forward_demodulation,[status(thm)],[f13705,f14233]) ).

fof(f14235,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),X2)),X3))) = multiply(X0,inverse(multiply(inverse(X2),inverse(multiply(inverse(X3),multiply(inverse(multiply(inverse(inverse(X4)),X1)),X4)))))),
    inference(forward_demodulation,[status(thm)],[f13905,f14234]) ).

fof(f14236,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),X2)),X3))) = multiply(X0,inverse(multiply(inverse(X2),inverse(multiply(inverse(multiply(X1,X3)),multiply(inverse(X4),X4)))))),
    inference(forward_demodulation,[status(thm)],[f12167,f14235]) ).

fof(f14279,plain,
    ! [X0,X1,X2,X3,X4] : X0 = multiply(inverse(multiply(multiply(X1,inverse(X2)),X3)),multiply(X4,multiply(inverse(X4),multiply(X1,inverse(multiply(multiply(inverse(inverse(inverse(X0))),inverse(X3)),X2)))))),
    inference(backward_demodulation,[status(thm)],[f12636,f13201]) ).

fof(f14374,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(inverse(inverse(inverse(X0))),X1),X2)) = multiply(X1,X2),
    inference(backward_demodulation,[status(thm)],[f12636,f14181]) ).

fof(f14849,plain,
    ! [X0,X1,X2,X3] : X0 = multiply(inverse(X1),inverse(multiply(inverse(multiply(X2,multiply(X1,X0))),multiply(X2,multiply(inverse(X3),X3))))),
    inference(backward_demodulation,[status(thm)],[f12103,f11878]) ).

fof(f14897,plain,
    ! [X0,X1,X2] : X0 = multiply(inverse(X1),inverse(multiply(inverse(multiply(X1,X0)),multiply(inverse(X2),X2)))),
    inference(forward_demodulation,[status(thm)],[f2949,f14849]) ).

fof(f15251,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(inverse(X0),multiply(X1,X2))) = multiply(X1,X2),
    inference(forward_demodulation,[status(thm)],[f12636,f14374]) ).

fof(f15515,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X1),X1),inverse(X2)))),inverse(multiply(inverse(X3),X4))),multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),X3)),X1)))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(X4),inverse(X5))),X2)),X5)),
    inference(forward_demodulation,[status(thm)],[f12636,f12034]) ).

fof(f15516,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(multiply(inverse(X1),X1),inverse(X2)),multiply(inverse(multiply(inverse(X3),X4)),multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),X3)),X1))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(X4),inverse(X5))),X2)),X5)),
    inference(forward_demodulation,[status(thm)],[f12636,f15515]) ).

fof(f15517,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(X2),X3)),multiply(inverse(multiply(inverse(multiply(X0,inverse(X4))),X2)),X4))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),inverse(X5))),X1)),X5)),
    inference(forward_demodulation,[status(thm)],[f12157,f15516]) ).

fof(f15518,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(inverse(multiply(X1,X2)),multiply(X3,multiply(inverse(multiply(inverse(multiply(X0,inverse(X4))),X3)),X4))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),inverse(X5))),X2)),X5)),
    inference(forward_demodulation,[status(thm)],[f12167,f15517]) ).

fof(f15519,plain,
    ! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(inverse(multiply(X1,X2)),multiply(X3,multiply(inverse(X3),multiply(X0,inverse(multiply(inverse(X4),X4)))))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),inverse(X5))),X2)),X5)),
    inference(forward_demodulation,[status(thm)],[f12106,f15518]) ).

fof(f15520,plain,
    ! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(inverse(multiply(X1,X2)),multiply(X0,inverse(multiply(inverse(X3),X3)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),inverse(X4))),X2)),X4)),
    inference(forward_demodulation,[status(thm)],[f15251,f15519]) ).

fof(f15521,plain,
    ! [X0,X1,X2] : multiply(X0,X1) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),inverse(X2))),X1)),X2)),
    inference(forward_demodulation,[status(thm)],[f12317,f15520]) ).

fof(f15522,plain,
    ! [X0,X1,X2] : multiply(X0,X1) = inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(inverse(X2)),X0)),X2))),
    inference(forward_demodulation,[status(thm)],[f4127,f15521]) ).

fof(f15523,plain,
    ! [X0,X1,X2] : multiply(multiply(inverse(X0),X1),X2) = multiply(inverse(multiply(inverse(X1),X0)),X2),
    inference(backward_demodulation,[status(thm)],[f15533,f13718]) ).

fof(f15525,plain,
    ! [X0,X1,X2] : multiply(X0,inverse(multiply(inverse(X1),X2))) = multiply(multiply(X0,inverse(X2)),X1),
    inference(backward_demodulation,[status(thm)],[f15533,f13858]) ).

fof(f15530,plain,
    ! [X0,X1] : X0 = multiply(inverse(X1),multiply(X1,X0)),
    inference(backward_demodulation,[status(thm)],[f15533,f14897]) ).

fof(f15532,plain,
    ! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),X2)),X3))) = multiply(X0,inverse(multiply(inverse(X2),multiply(X1,X3)))),
    inference(backward_demodulation,[status(thm)],[f15533,f14236]) ).

fof(f15533,plain,
    ! [X0,X1,X2] : multiply(X0,X1) = inverse(multiply(inverse(multiply(X0,X1)),multiply(inverse(X2),X2))),
    inference(forward_demodulation,[status(thm)],[f12167,f15522]) ).

fof(f15693,plain,
    ! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(X1),multiply(X2,X3)))) = multiply(X0,inverse(multiply(multiply(inverse(X1),X2),X3))),
    inference(forward_demodulation,[status(thm)],[f15523,f15532]) ).

fof(f16098,plain,
    ! [X0,X1,X2,X3] : X0 = multiply(inverse(multiply(multiply(X1,inverse(X2)),X3)),multiply(X1,inverse(multiply(multiply(inverse(inverse(inverse(X0))),inverse(X3)),X2)))),
    inference(forward_demodulation,[status(thm)],[f15251,f14279]) ).

fof(f16099,plain,
    ! [X0,X1,X2,X3] : X0 = multiply(inverse(multiply(multiply(X1,inverse(X2)),X3)),multiply(X1,inverse(multiply(inverse(inverse(inverse(X0))),multiply(inverse(X3),X2))))),
    inference(forward_demodulation,[status(thm)],[f15693,f16098]) ).

fof(f16100,plain,
    ! [X0,X1,X2,X3] : X0 = multiply(inverse(multiply(multiply(X1,inverse(X2)),X3)),multiply(multiply(X1,inverse(multiply(inverse(X3),X2))),inverse(inverse(X0)))),
    inference(forward_demodulation,[status(thm)],[f15525,f16099]) ).

fof(f16101,plain,
    ! [X0,X1,X2] : X0 = multiply(inverse(multiply(inverse(X1),X2)),multiply(inverse(multiply(inverse(X2),X1)),inverse(inverse(X0)))),
    inference(forward_demodulation,[status(thm)],[f11651,f16100]) ).

fof(f16102,plain,
    ! [X0,X1] : X0 = multiply(inverse(multiply(inverse(X1),X1)),inverse(inverse(X0))),
    inference(forward_demodulation,[status(thm)],[f3572,f16101]) ).

fof(f16120,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X0,X1),X2),
    inference(backward_demodulation,[status(thm)],[f16122,f12636]) ).

fof(f16122,plain,
    ! [X0] : inverse(inverse(X0)) = X0,
    inference(forward_demodulation,[status(thm)],[f2934,f16102]) ).

fof(f16854,plain,
    ( sQ2_spl
    | multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)) ),
    inference(backward_demodulation,[status(thm)],[f16120,f13]) ).

fof(f17637,plain,
    ( sQ2_spl
    | $false ),
    inference(trivial_equality_resolution,[status(thm)],[f16854]) ).

fof(f17638,plain,
    sQ2_spl,
    inference(contradiction_clause,[status(thm)],[f17637]) ).

fof(f17774,plain,
    ( sQ0_spl
    | $false ),
    inference(forward_subsumption_resolution,[status(thm)],[f7,f2913]) ).

fof(f17775,plain,
    sQ0_spl,
    inference(contradiction_clause,[status(thm)],[f17774]) ).

fof(f18008,plain,
    ( sQ1_spl
    | multiply(inverse(b2),multiply(b2,a2)) != a2 ),
    inference(forward_demodulation,[status(thm)],[f16120,f10]) ).

fof(f18009,plain,
    ( sQ1_spl
    | a2 != a2 ),
    inference(forward_demodulation,[status(thm)],[f15530,f18008]) ).

fof(f18010,plain,
    ( sQ1_spl
    | $false ),
    inference(trivial_equality_resolution,[status(thm)],[f18009]) ).

fof(f18011,plain,
    sQ1_spl,
    inference(contradiction_clause,[status(thm)],[f18010]) ).

fof(f18012,plain,
    $false,
    inference(sat_refutation,[status(thm)],[f14,f17638,f17775,f18011]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : GRP052-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04  % Command  : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.34  % Computer : n013.cluster.edu
% 0.09/0.34  % Model    : x86_64 x86_64
% 0.09/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34  % Memory   : 8046.5625MB
% 0.09/0.34  % OS       : Linux 6.8.0-71-generic
% 0.09/0.34  % CPULimit : 300
% 0.09/0.34  % WCLimit  : 300
% 0.09/0.34  % DateTime : Sun Sep 20 19:55:20 UTC 2026
% 0.09/0.34  % CPUTime  : 
% 0.09/0.35  % Drodi V4.1.1
% 235.15/30.12  % Refutation found
% 235.15/30.12  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 235.15/30.12  % SZS output start CNFRefutation for theBenchmark
% See solution above
% 31.40/30.47  % Elapsed time: 30.089050 seconds
% 31.40/30.47  % CPU time: 237.372288 seconds
% 31.40/30.47  % Total memory used: 1.794 GB
% 31.40/30.47  % Net memory used: 1.765 GB
%------------------------------------------------------------------------------