Drodi---4.1.1.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : Drodi---4.1.1
% Problem  : GRP120-1 : TPTP v9.3.1. Released v1.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n015.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:33 PM UTC 2026

% Result   : Unsatisfiable 13.51s 2.30s
% Output   : CNFRefutation 13.51s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   73
%            Number of leaves      :    3
% Syntax   : Number of formulae    :  315 ( 315 unt;   0 def)
%            Number of atoms       :  315 ( 314 equ)
%            Maximal formula atoms :    1 (   1 avg)
%            Number of connectives :    3 (   3   ~;   0   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    4 (   3 avg)
%            Maximal term depth    :   14 (   2 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :    3 (   3 usr;   2 con; 0-2 aty)
%            Number of variables   :  470 ( 470   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,axiom,
    ! [Y,X,Z] : multiply(Y,multiply(multiply(Y,multiply(multiply(Y,Y),multiply(X,Z))),multiply(Z,multiply(Z,Z)))) = X,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f2,axiom,
    multiply(identity,identity) = identity,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f3,negated_conjecture,
    multiply(identity,a) != a,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f4,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,X2))),multiply(X2,multiply(X2,X2)))) = X1,
    inference(cnf_transformation,[status(thm)],[f1]) ).

fof(f5,plain,
    multiply(identity,identity) = identity,
    inference(cnf_transformation,[status(thm)],[f2]) ).

fof(f6,plain,
    multiply(identity,a) != a,
    inference(cnf_transformation,[status(thm)],[f3]) ).

fof(f9,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,X1),multiply(multiply(X2,multiply(X2,X2)),multiply(multiply(X2,multiply(X2,X2)),multiply(X2,multiply(X2,X2)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,X2))),
    inference(paramodulation,[status(thm)],[f4,f4]) ).

fof(f10,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X0,X1))),multiply(X1,multiply(X1,X1)))) = X0,
    inference(paramodulation,[status(thm)],[f5,f4]) ).

fof(f11,plain,
    ! [X0] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(identity,multiply(identity,identity)))) = identity,
    inference(paramodulation,[status(thm)],[f5,f4]) ).

fof(f13,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,identity))),multiply(identity,identity))) = X1,
    inference(paramodulation,[status(thm)],[f5,f4]) ).

fof(f14,plain,
    ! [X0] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(identity,identity))) = identity,
    inference(forward_demodulation,[status(thm)],[f5,f11]) ).

fof(f15,plain,
    ! [X0] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f5,f14]) ).

fof(f16,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,identity))),identity)) = X1,
    inference(forward_demodulation,[status(thm)],[f5,f13]) ).

fof(f18,plain,
    ! [X0] : multiply(X0,multiply(multiply(X0,identity),multiply(identity,multiply(identity,identity)))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),identity)),
    inference(paramodulation,[status(thm)],[f15,f4]) ).

fof(f23,plain,
    ! [X0] : multiply(X0,multiply(multiply(X0,identity),multiply(identity,identity))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),identity)),
    inference(forward_demodulation,[status(thm)],[f5,f18]) ).

fof(f24,plain,
    ! [X0] : multiply(X0,multiply(multiply(X0,identity),identity)) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),identity)),
    inference(forward_demodulation,[status(thm)],[f5,f23]) ).

fof(f26,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X1),identity)) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
    inference(paramodulation,[status(thm)],[f16,f16]) ).

fof(f27,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X0,identity))),identity)) = X0,
    inference(paramodulation,[status(thm)],[f5,f16]) ).

fof(f33,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,X0),identity)) = multiply(identity,multiply(identity,multiply(X0,identity))),
    inference(paramodulation,[status(thm)],[f27,f27]) ).

fof(f38,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,identity)),identity))) = X0,
    inference(backward_demodulation,[status(thm)],[f33,f27]) ).

fof(f45,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))) = X0,
    inference(forward_demodulation,[status(thm)],[f33,f38]) ).

fof(f73,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X0,X1))),multiply(multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))),multiply(multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))))) = multiply(X1,multiply(X1,X1)),
    inference(paramodulation,[status(thm)],[f9,f4]) ).

fof(f76,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(multiply(identity,multiply(identity,identity)),multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))),identity)) = X1,
    inference(paramodulation,[status(thm)],[f9,f16]) ).

fof(f127,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(multiply(identity,identity),multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))),identity)) = X1,
    inference(forward_demodulation,[status(thm)],[f5,f76]) ).

fof(f128,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))),identity)) = X1,
    inference(forward_demodulation,[status(thm)],[f5,f127]) ).

fof(f129,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(multiply(identity,identity),multiply(identity,multiply(identity,identity)))))),identity)) = X1,
    inference(forward_demodulation,[status(thm)],[f5,f128]) ).

fof(f130,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity)))))),identity)) = X1,
    inference(forward_demodulation,[status(thm)],[f5,f129]) ).

fof(f131,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(identity,multiply(identity,identity))))),identity)) = X1,
    inference(forward_demodulation,[status(thm)],[f5,f130]) ).

fof(f132,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(identity,identity)))),identity)) = X1,
    inference(forward_demodulation,[status(thm)],[f5,f131]) ).

fof(f133,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,identity))),identity)) = X1,
    inference(forward_demodulation,[status(thm)],[f5,f132]) ).

fof(f134,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),identity)),identity)) = X1,
    inference(forward_demodulation,[status(thm)],[f5,f133]) ).

fof(f136,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))))),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)),
    inference(paramodulation,[status(thm)],[f45,f9]) ).

fof(f151,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,multiply(multiply(identity,X0),identity)),identity)) = X0,
    inference(paramodulation,[status(thm)],[f5,f134]) ).

fof(f158,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity),
    inference(paramodulation,[status(thm)],[f15,f134]) ).

fof(f159,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,identity))),identity),
    inference(paramodulation,[status(thm)],[f16,f134]) ).

fof(f160,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,X2))),multiply(X2,multiply(X2,X2))),
    inference(paramodulation,[status(thm)],[f4,f134]) ).

fof(f168,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X0),identity),identity))) = X0,
    inference(forward_demodulation,[status(thm)],[f33,f151]) ).

fof(f177,plain,
    ! [X0] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))) = identity,
    inference(backward_demodulation,[status(thm)],[f181,f15]) ).

fof(f181,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity),
    inference(forward_demodulation,[status(thm)],[f5,f158]) ).

fof(f182,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity))) = X1,
    inference(backward_demodulation,[status(thm)],[f159,f16]) ).

fof(f264,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(identity,identity),multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(X0,X1))),identity),identity))) = multiply(multiply(identity,X0),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
    inference(paramodulation,[status(thm)],[f9,f168]) ).

fof(f283,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(X0,X1))),identity),identity))) = multiply(multiply(identity,X0),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
    inference(forward_demodulation,[status(thm)],[f5,f264]) ).

fof(f284,plain,
    ! [X0,X1] : multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(X0,X1)) = multiply(multiply(identity,X0),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
    inference(forward_demodulation,[status(thm)],[f168,f283]) ).

fof(f285,plain,
    ! [X0,X1] : multiply(multiply(identity,multiply(identity,identity)),multiply(X0,X1)) = multiply(multiply(identity,X0),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
    inference(forward_demodulation,[status(thm)],[f5,f284]) ).

fof(f286,plain,
    ! [X0,X1] : multiply(multiply(identity,identity),multiply(X0,X1)) = multiply(multiply(identity,X0),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
    inference(forward_demodulation,[status(thm)],[f5,f285]) ).

fof(f287,plain,
    ! [X0,X1] : multiply(identity,multiply(X0,X1)) = multiply(multiply(identity,X0),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
    inference(forward_demodulation,[status(thm)],[f5,f286]) ).

fof(f337,plain,
    ! [X0] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X0,identity))),identity)),identity)) = multiply(multiply(identity,X0),identity),
    inference(paramodulation,[status(thm)],[f33,f134]) ).

fof(f377,plain,
    ! [X0] : multiply(identity,multiply(X0,identity)) = multiply(multiply(identity,X0),identity),
    inference(forward_demodulation,[status(thm)],[f134,f337]) ).

fof(f411,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X1,identity))),identity))) = multiply(identity,X1),
    inference(paramodulation,[status(thm)],[f377,f182]) ).

fof(f412,plain,
    ! [X0] : multiply(multiply(identity,X0),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(identity,multiply(X0,identity)),identity))) = identity,
    inference(paramodulation,[status(thm)],[f377,f177]) ).

fof(f414,plain,
    ! [X0] : multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(multiply(identity,X0),multiply(multiply(identity,multiply(X0,identity)),identity)),identity)) = identity,
    inference(paramodulation,[status(thm)],[f377,f134]) ).

fof(f450,plain,
    ! [X0] : multiply(multiply(identity,X0),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity)))) = identity,
    inference(forward_demodulation,[status(thm)],[f377,f412]) ).

fof(f452,plain,
    ! [X0] : multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(multiply(identity,X0),multiply(identity,multiply(multiply(X0,identity),identity))),identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f377,f414]) ).

fof(f462,plain,
    ! [X0,X1] : multiply(multiply(identity,identity),multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1))) = X0,
    inference(paramodulation,[status(thm)],[f9,f10]) ).

fof(f481,plain,
    ! [X0,X1] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(X0,identity)),identity)) = multiply(multiply(identity,multiply(identity,multiply(X0,X1))),multiply(X1,multiply(X1,X1))),
    inference(paramodulation,[status(thm)],[f10,f134]) ).

fof(f484,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1))) = X0,
    inference(forward_demodulation,[status(thm)],[f5,f462]) ).

fof(f485,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(identity,multiply(identity,identity)),multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1))) = X0,
    inference(forward_demodulation,[status(thm)],[f5,f484]) ).

fof(f486,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(identity,identity),multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1))) = X0,
    inference(forward_demodulation,[status(thm)],[f5,f485]) ).

fof(f487,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1))) = X0,
    inference(forward_demodulation,[status(thm)],[f5,f486]) ).

fof(f525,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(identity,multiply(X0,identity)),identity)) = multiply(multiply(identity,multiply(identity,multiply(X0,X1))),multiply(X1,multiply(X1,X1))),
    inference(forward_demodulation,[status(thm)],[f5,f481]) ).

fof(f529,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(multiply(identity,multiply(identity,multiply(X0,X1))),multiply(X1,multiply(X1,X1))),
    inference(forward_demodulation,[status(thm)],[f377,f525]) ).

fof(f552,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1)),identity)) = multiply(X0,identity),
    inference(paramodulation,[status(thm)],[f487,f377]) ).

fof(f553,plain,
    ! [X0,X1] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(X0,identity)),identity)) = multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1)),
    inference(paramodulation,[status(thm)],[f487,f134]) ).

fof(f567,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),identity))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f377,f552]) ).

fof(f568,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(identity,multiply(X0,identity)),identity)) = multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1)),
    inference(forward_demodulation,[status(thm)],[f5,f553]) ).

fof(f570,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1)),
    inference(forward_demodulation,[status(thm)],[f377,f568]) ).

fof(f585,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X1,identity)))),multiply(multiply(identity,multiply(identity,identity)),multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))) = multiply(identity,X1),
    inference(paramodulation,[status(thm)],[f9,f411]) ).

fof(f594,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(identity,X1),multiply(multiply(X2,multiply(X2,X2)),multiply(multiply(X2,multiply(X2,X2)),multiply(X2,multiply(X2,X2)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X1,identity))),identity)),X2))),
    inference(paramodulation,[status(thm)],[f411,f9]) ).

fof(f595,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X1,identity)))),multiply(multiply(identity,identity),multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))) = multiply(identity,X1),
    inference(forward_demodulation,[status(thm)],[f5,f585]) ).

fof(f596,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X1,identity)))),multiply(identity,multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))) = multiply(identity,X1),
    inference(forward_demodulation,[status(thm)],[f5,f595]) ).

fof(f597,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X1,identity)))),multiply(identity,multiply(multiply(identity,identity),multiply(identity,multiply(identity,identity)))))) = multiply(identity,X1),
    inference(forward_demodulation,[status(thm)],[f5,f596]) ).

fof(f598,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X1,identity)))),multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity)))))) = multiply(identity,X1),
    inference(forward_demodulation,[status(thm)],[f5,f597]) ).

fof(f599,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X1,identity)))),multiply(identity,multiply(identity,multiply(identity,identity))))) = multiply(identity,X1),
    inference(forward_demodulation,[status(thm)],[f5,f598]) ).

fof(f600,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X1,identity)))),multiply(identity,multiply(identity,identity)))) = multiply(identity,X1),
    inference(forward_demodulation,[status(thm)],[f5,f599]) ).

fof(f601,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X1,identity)))),multiply(identity,identity))) = multiply(identity,X1),
    inference(forward_demodulation,[status(thm)],[f5,f600]) ).

fof(f602,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X1,identity)))),identity)) = multiply(identity,X1),
    inference(forward_demodulation,[status(thm)],[f5,f601]) ).

fof(f621,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,multiply(X1,X2))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X1,identity))),identity)),X2))),
    inference(forward_demodulation,[status(thm)],[f287,f594]) ).

fof(f629,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,X1)),identity))) = multiply(identity,multiply(identity,multiply(multiply(identity,identity),multiply(identity,multiply(X1,identity))))),
    inference(paramodulation,[status(thm)],[f602,f411]) ).

fof(f660,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,X1)),identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity))))),
    inference(forward_demodulation,[status(thm)],[f5,f629]) ).

fof(f689,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),identity)))) = multiply(X0,multiply(multiply(X0,X0),identity)),
    inference(paramodulation,[status(thm)],[f181,f45]) ).

fof(f691,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),identity))),multiply(multiply(identity,multiply(identity,identity)),multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),
    inference(paramodulation,[status(thm)],[f181,f9]) ).

fof(f736,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),identity))),multiply(multiply(identity,identity),multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f691]) ).

fof(f737,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),identity))),multiply(identity,multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f736]) ).

fof(f738,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),identity))),multiply(identity,multiply(multiply(identity,identity),multiply(identity,multiply(identity,identity)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f737]) ).

fof(f739,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),identity))),multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f738]) ).

fof(f740,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),identity))),multiply(identity,multiply(identity,multiply(identity,identity))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f739]) ).

fof(f741,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),identity))),multiply(identity,multiply(identity,identity)))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f740]) ).

fof(f742,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),identity))),multiply(identity,identity))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f741]) ).

fof(f743,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),identity))),identity)) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f742]) ).

fof(f749,plain,
    ! [X0] : multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(X0,multiply(multiply(X0,identity),identity)),identity)) = multiply(X0,X0),
    inference(paramodulation,[status(thm)],[f24,f134]) ).

fof(f750,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(X0,multiply(multiply(X0,identity),identity)),identity))) = multiply(multiply(X0,X0),multiply(X0,X0)),
    inference(paramodulation,[status(thm)],[f24,f182]) ).

fof(f793,plain,
    ! [X0] : multiply(X0,multiply(multiply(X0,multiply(X0,multiply(multiply(X0,identity),identity))),identity)) = multiply(multiply(X0,X0),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f26,f750]) ).

fof(f879,plain,
    ! [X0] : multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),identity))),identity)) = multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),
    inference(paramodulation,[status(thm)],[f181,f793]) ).

fof(f935,plain,
    ! [X0] : multiply(multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),
    inference(paramodulation,[status(thm)],[f181,f749]) ).

fof(f987,plain,
    ! [X0,X1] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(multiply(X0,identity),identity)),identity)) = multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),identity)),
    inference(paramodulation,[status(thm)],[f567,f134]) ).

fof(f988,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
    inference(paramodulation,[status(thm)],[f567,f9]) ).

fof(f1002,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(identity,multiply(multiply(X0,identity),identity)),identity)) = multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),identity)),
    inference(forward_demodulation,[status(thm)],[f5,f987]) ).

fof(f1004,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),identity),identity))) = multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),identity)),
    inference(forward_demodulation,[status(thm)],[f377,f1002]) ).

fof(f1005,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
    inference(forward_demodulation,[status(thm)],[f1004,f988]) ).

fof(f1006,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
    inference(forward_demodulation,[status(thm)],[f1004,f1005]) ).

fof(f1007,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
    inference(forward_demodulation,[status(thm)],[f1004,f1006]) ).

fof(f1008,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
    inference(forward_demodulation,[status(thm)],[f1004,f1007]) ).

fof(f1009,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
    inference(forward_demodulation,[status(thm)],[f1004,f1008]) ).

fof(f1010,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
    inference(forward_demodulation,[status(thm)],[f1004,f1009]) ).

fof(f1011,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
    inference(forward_demodulation,[status(thm)],[f1004,f1010]) ).

fof(f1012,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(multiply(multiply(identity,multiply(X1,multiply(X2,multiply(X2,X2)))),X2),identity)))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
    inference(forward_demodulation,[status(thm)],[f1004,f1011]) ).

fof(f1013,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))),
    inference(forward_demodulation,[status(thm)],[f1004,f1012]) ).

fof(f1014,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity))))))))) = multiply(X0,multiply(multiply(X0,X1),identity)),
    inference(forward_demodulation,[status(thm)],[f26,f1013]) ).

fof(f1307,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1)))))),identity),identity))) = multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),X1)),
    inference(paramodulation,[status(thm)],[f570,f570]) ).

fof(f1317,plain,
    ! [X0,X1] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),identity)),identity)) = multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),
    inference(paramodulation,[status(thm)],[f570,f134]) ).

fof(f1326,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(X0,multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),identity)),identity))) = multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),X1)),
    inference(forward_demodulation,[status(thm)],[f377,f1307]) ).

fof(f1327,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),identity),identity)))) = multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),X1)),
    inference(forward_demodulation,[status(thm)],[f377,f1326]) ).

fof(f1328,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X1),identity),identity))),X2))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,X2))),
    inference(backward_demodulation,[status(thm)],[f1372,f9]) ).

fof(f1340,plain,
    ! [X0,X1] : multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity)))))) = multiply(X0,multiply(multiply(X0,X1),identity)),
    inference(backward_demodulation,[status(thm)],[f1372,f1014]) ).

fof(f1341,plain,
    ! [X0,X1] : multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)),
    inference(backward_demodulation,[status(thm)],[f1372,f136]) ).

fof(f1372,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))) = multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),X1)),
    inference(forward_demodulation,[status(thm)],[f45,f1327]) ).

fof(f1406,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(X0,identity),identity)) = multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),
    inference(forward_demodulation,[status(thm)],[f134,f1317]) ).

fof(f1605,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,identity),identity))) = multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
    inference(paramodulation,[status(thm)],[f45,f529]) ).

fof(f1613,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X0),identity),identity))) = multiply(multiply(identity,multiply(identity,identity)),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity)))))),
    inference(paramodulation,[status(thm)],[f450,f529]) ).

fof(f1629,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity)))) = multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f377,f1605]) ).

fof(f1630,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,identity))) = multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f1629]) ).

fof(f1631,plain,
    ! [X0] : multiply(identity,multiply(identity,identity)) = multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f1630]) ).

fof(f1632,plain,
    ! [X0] : multiply(identity,identity) = multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f1631]) ).

fof(f1634,plain,
    ! [X0] : identity = multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f1632]) ).

fof(f1675,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,identity)),identity))) = multiply(multiply(identity,multiply(identity,identity)),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity)))))),
    inference(forward_demodulation,[status(thm)],[f377,f1613]) ).

fof(f1676,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))) = multiply(multiply(identity,multiply(identity,identity)),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity)))))),
    inference(forward_demodulation,[status(thm)],[f377,f1675]) ).

fof(f1677,plain,
    ! [X0] : X0 = multiply(multiply(identity,multiply(identity,identity)),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity)))))),
    inference(forward_demodulation,[status(thm)],[f45,f1676]) ).

fof(f1678,plain,
    ! [X0] : X0 = multiply(multiply(identity,identity),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity)))))),
    inference(forward_demodulation,[status(thm)],[f5,f1677]) ).

fof(f1679,plain,
    ! [X0] : X0 = multiply(identity,multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity)))))),
    inference(forward_demodulation,[status(thm)],[f5,f1678]) ).

fof(f1750,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,identity)),identity)) = multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity))),
    inference(paramodulation,[status(thm)],[f1634,f134]) ).

fof(f1908,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)) = multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity))),
    inference(forward_demodulation,[status(thm)],[f5,f1750]) ).

fof(f2010,plain,
    ! [X0] : multiply(multiply(multiply(identity,multiply(identity,X0)),multiply(identity,multiply(identity,X0))),multiply(multiply(multiply(identity,multiply(identity,X0)),multiply(identity,multiply(multiply(identity,multiply(X0,identity)),identity))),identity)) = identity,
    inference(paramodulation,[status(thm)],[f377,f452]) ).

fof(f2218,plain,
    ! [X0] : multiply(multiply(multiply(identity,multiply(identity,X0)),multiply(identity,multiply(identity,X0))),multiply(multiply(multiply(identity,multiply(identity,X0)),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f377,f2010]) ).

fof(f2278,plain,
    ! [X0] : multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(multiply(identity,X0),multiply(identity,identity)),identity)) = multiply(identity,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
    inference(paramodulation,[status(thm)],[f450,f160]) ).

fof(f2320,plain,
    ! [X0] : multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(multiply(identity,X0),identity),identity)) = multiply(identity,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f2278]) ).

fof(f2321,plain,
    ! [X0] : multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(identity,multiply(X0,identity)),identity)) = multiply(identity,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f377,f2320]) ).

fof(f2322,plain,
    ! [X0] : multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f377,f2321]) ).

fof(f2323,plain,
    ! [X0] : multiply(multiply(identity,X0),multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))) = identity,
    inference(backward_demodulation,[status(thm)],[f2327,f450]) ).

fof(f2324,plain,
    ! [X0] : X0 = multiply(identity,multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))))),
    inference(backward_demodulation,[status(thm)],[f2327,f1679]) ).

fof(f2327,plain,
    ! [X0] : multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),
    inference(forward_demodulation,[status(thm)],[f1908,f2322]) ).

fof(f2405,plain,
    ! [X0] : X0 = multiply(identity,multiply(multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))))),
    inference(forward_demodulation,[status(thm)],[f2327,f2324]) ).

fof(f2406,plain,
    ! [X0] : X0 = multiply(identity,multiply(multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),multiply(multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))))),
    inference(forward_demodulation,[status(thm)],[f2327,f2405]) ).

fof(f2418,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,X0)),multiply(identity,multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(identity,multiply(X0,identity)),identity)))) = identity,
    inference(paramodulation,[status(thm)],[f377,f2323]) ).

fof(f2489,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,X0)),multiply(identity,multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))))) = identity,
    inference(forward_demodulation,[status(thm)],[f377,f2418]) ).

fof(f2491,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,X0)),multiply(identity,multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))))) = identity,
    inference(forward_demodulation,[status(thm)],[f2327,f2489]) ).

fof(f2580,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(identity,multiply(identity,X1)),identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),multiply(identity,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))))))),
    inference(paramodulation,[status(thm)],[f2491,f160]) ).

fof(f2663,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(multiply(identity,X1),identity))),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),multiply(identity,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))))))),
    inference(forward_demodulation,[status(thm)],[f377,f2580]) ).

fof(f2664,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(identity,multiply(X1,identity)))),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),multiply(identity,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))))))),
    inference(forward_demodulation,[status(thm)],[f377,f2663]) ).

fof(f3096,plain,
    ! [X0] : multiply(identity,multiply(multiply(multiply(multiply(identity,identity),multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0))),identity),identity)) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
    inference(paramodulation,[status(thm)],[f73,f1406]) ).

fof(f3103,plain,
    ! [X0] : multiply(identity,multiply(multiply(multiply(multiply(identity,identity),multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
    inference(paramodulation,[status(thm)],[f73,f377]) ).

fof(f3348,plain,
    ! [X0] : multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0))),identity),identity)) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f5,f3096]) ).

fof(f3349,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0)),identity)),identity)) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f377,f3348]) ).

fof(f3350,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0)),identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f377,f3349]) ).

fof(f3351,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(identity,multiply(identity,identity)),multiply(identity,X0)),identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f5,f3350]) ).

fof(f3352,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(identity,identity),multiply(identity,X0)),identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f5,f3351]) ).

fof(f3353,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(identity,X0)),identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f5,f3352]) ).

fof(f3354,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(identity,X0),identity)),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f377,f3353]) ).

fof(f3355,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X0),identity),identity)))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f377,f3354]) ).

fof(f3361,plain,
    ! [X0,X1] : multiply(X0,multiply(identity,X1)) = multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),X1)),
    inference(backward_demodulation,[status(thm)],[f3362,f1372]) ).

fof(f3362,plain,
    ! [X0] : multiply(identity,X0) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f45,f3355]) ).

fof(f3421,plain,
    ! [X0] : multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
    inference(forward_demodulation,[status(thm)],[f5,f3103]) ).

fof(f3422,plain,
    ! [X0] : multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(identity,multiply(identity,identity)),multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
    inference(forward_demodulation,[status(thm)],[f5,f3421]) ).

fof(f3423,plain,
    ! [X0] : multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(identity,identity),multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
    inference(forward_demodulation,[status(thm)],[f5,f3422]) ).

fof(f3424,plain,
    ! [X0] : multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
    inference(forward_demodulation,[status(thm)],[f5,f3423]) ).

fof(f3450,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,X1),multiply(identity,X2))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,X2))),
    inference(backward_demodulation,[status(thm)],[f3361,f1328]) ).

fof(f3485,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X1,identity),identity),identity)))))) = multiply(X0,multiply(multiply(X0,X1),identity)),
    inference(backward_demodulation,[status(thm)],[f3361,f1340]) ).

fof(f3486,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)),
    inference(backward_demodulation,[status(thm)],[f3361,f1341]) ).

fof(f3524,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,multiply(X1,X2))) = multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X1,identity))),identity))),multiply(identity,X2))),
    inference(backward_demodulation,[status(thm)],[f3450,f621]) ).

fof(f3527,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),identity))),identity)) = multiply(X0,multiply(multiply(X0,multiply(X1,X1)),multiply(identity,multiply(multiply(X1,identity),identity)))),
    inference(backward_demodulation,[status(thm)],[f3450,f743]) ).

fof(f3562,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(X1,identity))) = multiply(X0,multiply(multiply(X0,X1),identity)),
    inference(forward_demodulation,[status(thm)],[f45,f3485]) ).

fof(f3565,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,X1),multiply(identity,X2))) = multiply(X0,multiply(multiply(X0,identity),multiply(X1,X2))),
    inference(backward_demodulation,[status(thm)],[f3569,f3450]) ).

fof(f3569,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),X1)) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)),
    inference(forward_demodulation,[status(thm)],[f45,f3486]) ).

fof(f3589,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,multiply(X1,X2))) = multiply(X0,multiply(multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))))),multiply(identity,X2))),
    inference(forward_demodulation,[status(thm)],[f660,f3524]) ).

fof(f3603,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(identity,multiply(X1,identity)))),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),multiply(identity,multiply(multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))),multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))))))),
    inference(backward_demodulation,[status(thm)],[f3611,f2664]) ).

fof(f3611,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,multiply(X1,X2))) = multiply(X0,multiply(multiply(identity,X1),multiply(identity,X2))),
    inference(forward_demodulation,[status(thm)],[f45,f3589]) ).

fof(f3639,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),identity))),identity)) = multiply(X0,multiply(multiply(X0,identity),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),
    inference(backward_demodulation,[status(thm)],[f3565,f3527]) ).

fof(f3666,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(identity,multiply(X1,identity)))),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(identity,multiply(multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))),multiply(multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))),multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))))))),
    inference(forward_demodulation,[status(thm)],[f3611,f3603]) ).

fof(f3668,plain,
    ! [X0] : multiply(multiply(multiply(identity,multiply(identity,X0)),multiply(multiply(multiply(identity,multiply(identity,X0)),multiply(identity,multiply(identity,X0))),identity)),multiply(X0,identity)) = identity,
    inference(backward_demodulation,[status(thm)],[f3670,f2218]) ).

fof(f3670,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(identity,multiply(X1,identity)))),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),X1),
    inference(forward_demodulation,[status(thm)],[f2406,f3666]) ).

fof(f3765,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,multiply(multiply(X0,identity),multiply(X1,X2))),identity)),identity)) = multiply(multiply(X0,X1),multiply(identity,X2)),
    inference(paramodulation,[status(thm)],[f3565,f134]) ).

fof(f3896,plain,
    ! [X0] : multiply(multiply(multiply(identity,multiply(identity,X0)),multiply(multiply(multiply(identity,identity),multiply(multiply(identity,X0),multiply(identity,X0))),identity)),multiply(X0,identity)) = identity,
    inference(backward_demodulation,[status(thm)],[f3926,f3668]) ).

fof(f3926,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,identity),multiply(X1,X2)) = multiply(multiply(X0,X1),multiply(identity,X2)),
    inference(forward_demodulation,[status(thm)],[f134,f3765]) ).

fof(f4112,plain,
    ! [X0] : multiply(multiply(multiply(identity,multiply(identity,X0)),multiply(multiply(multiply(identity,identity),multiply(identity,multiply(X0,X0))),identity)),multiply(X0,identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f3611,f3896]) ).

fof(f4113,plain,
    ! [X0] : multiply(multiply(multiply(identity,multiply(identity,X0)),multiply(multiply(identity,multiply(identity,multiply(X0,X0))),identity)),multiply(X0,identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f5,f4112]) ).

fof(f4114,plain,
    ! [X0] : multiply(multiply(multiply(identity,multiply(identity,X0)),multiply(identity,multiply(multiply(identity,multiply(X0,X0)),identity))),multiply(X0,identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f377,f4113]) ).

fof(f4115,plain,
    ! [X0] : multiply(multiply(multiply(identity,identity),multiply(multiply(identity,X0),multiply(multiply(identity,multiply(X0,X0)),identity))),multiply(X0,identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f3926,f4114]) ).

fof(f4116,plain,
    ! [X0] : multiply(multiply(identity,multiply(multiply(identity,X0),multiply(multiply(identity,multiply(X0,X0)),identity))),multiply(X0,identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f5,f4115]) ).

fof(f4117,plain,
    ! [X0] : multiply(multiply(identity,multiply(multiply(identity,X0),multiply(identity,multiply(multiply(X0,X0),identity)))),multiply(X0,identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f377,f4116]) ).

fof(f4118,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(X0,identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f3611,f4117]) ).

fof(f4194,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))))),multiply(identity,identity))) = X0,
    inference(paramodulation,[status(thm)],[f4118,f182]) ).

fof(f4198,plain,
    ! [X0] : multiply(multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(identity,identity)),identity)) = multiply(X0,identity),
    inference(paramodulation,[status(thm)],[f4118,f134]) ).

fof(f4240,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),identity),multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),identity))) = X0,
    inference(forward_demodulation,[status(thm)],[f3565,f4194]) ).

fof(f4241,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))))),identity)) = X0,
    inference(forward_demodulation,[status(thm)],[f3562,f4240]) ).

fof(f4242,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(multiply(multiply(identity,identity),multiply(multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))))),identity)) = X0,
    inference(forward_demodulation,[status(thm)],[f3926,f4241]) ).

fof(f4243,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(multiply(multiply(identity,identity),multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))))),identity)) = X0,
    inference(forward_demodulation,[status(thm)],[f3611,f4242]) ).

fof(f4244,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(multiply(identity,multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))))),identity)) = X0,
    inference(forward_demodulation,[status(thm)],[f5,f4243]) ).

fof(f4245,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(identity,multiply(multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),identity))) = X0,
    inference(forward_demodulation,[status(thm)],[f377,f4244]) ).

fof(f4246,plain,
    ! [X0] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),identity))) = X0,
    inference(forward_demodulation,[status(thm)],[f3926,f4245]) ).

fof(f4247,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),identity))) = X0,
    inference(forward_demodulation,[status(thm)],[f5,f4246]) ).

fof(f4248,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),multiply(identity,multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),identity)))) = X0,
    inference(forward_demodulation,[status(thm)],[f377,f4247]) ).

fof(f4249,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,identity),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),identity)))) = X0,
    inference(forward_demodulation,[status(thm)],[f3565,f4248]) ).

fof(f4251,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),identity)))) = X0,
    inference(forward_demodulation,[status(thm)],[f5,f4249]) ).

fof(f4270,plain,
    ! [X0] : multiply(multiply(multiply(identity,identity),multiply(multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(identity,identity)),identity)) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f3926,f4198]) ).

fof(f4271,plain,
    ! [X0] : multiply(multiply(multiply(identity,identity),multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(identity,identity)),identity)) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f3611,f4270]) ).

fof(f4272,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))))),multiply(multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(identity,identity)),identity)) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f5,f4271]) ).

fof(f4273,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))))),multiply(multiply(multiply(identity,identity),multiply(multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),identity)),identity)) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f3926,f4272]) ).

fof(f4274,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))))),multiply(multiply(identity,multiply(multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),identity)),identity)) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f5,f4273]) ).

fof(f4275,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))))),multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),identity),identity))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f377,f4274]) ).

fof(f4276,plain,
    ! [X0] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(multiply(multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),identity),identity))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f3926,f4275]) ).

fof(f4277,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(multiply(multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),identity),identity))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f5,f4276]) ).

fof(f4278,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity)),identity))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f377,f4277]) ).

fof(f4279,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(identity,multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity),identity)))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f377,f4278]) ).

fof(f4280,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,identity),multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity),identity)))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f3565,f4279]) ).

fof(f4281,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),identity))),identity)) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f3639,f4280]) ).

fof(f4282,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),identity)),identity))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f377,f4281]) ).

fof(f4283,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity),identity)))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f181,f4282]) ).

fof(f4284,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),identity)))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f181,f4283]) ).

fof(f4325,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X1),identity)),identity)),identity)) = multiply(multiply(X0,identity),multiply(X1,identity)),
    inference(paramodulation,[status(thm)],[f3562,f134]) ).

fof(f4487,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)) = multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),multiply(X0,identity)),identity)),
    inference(backward_demodulation,[status(thm)],[f4511,f1908]) ).

fof(f4511,plain,
    ! [X0,X1] : multiply(multiply(X0,X1),identity) = multiply(multiply(X0,identity),multiply(X1,identity)),
    inference(forward_demodulation,[status(thm)],[f134,f4325]) ).

fof(f4531,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)) = multiply(multiply(multiply(X0,identity),multiply(multiply(X0,identity),multiply(X0,identity))),identity),
    inference(forward_demodulation,[status(thm)],[f4511,f4487]) ).

fof(f4532,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)) = multiply(multiply(multiply(X0,identity),multiply(multiply(X0,X0),identity)),identity),
    inference(forward_demodulation,[status(thm)],[f4511,f4531]) ).

fof(f4533,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)) = multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity),
    inference(forward_demodulation,[status(thm)],[f4511,f4532]) ).

fof(f4598,plain,
    ! [X0,X1] : multiply(multiply(multiply(X0,identity),multiply(X0,identity)),multiply(multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity),identity)) = X1,
    inference(paramodulation,[status(thm)],[f4511,f134]) ).

fof(f4736,plain,
    ! [X0,X1] : multiply(multiply(multiply(X0,X0),identity),multiply(multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity),identity)) = X1,
    inference(forward_demodulation,[status(thm)],[f4511,f4598]) ).

fof(f4737,plain,
    ! [X0,X1] : multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity)),identity) = X1,
    inference(forward_demodulation,[status(thm)],[f4511,f4736]) ).

fof(f5128,plain,
    ! [X0,X1] : multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),X1),identity)) = multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity),
    inference(paramodulation,[status(thm)],[f4737,f134]) ).

fof(f5133,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,multiply(multiply(X1,X1),multiply(multiply(X1,multiply(multiply(X1,identity),X2)),identity))),identity) = multiply(multiply(X0,identity),X2),
    inference(paramodulation,[status(thm)],[f4737,f4511]) ).

fof(f5138,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(multiply(X1,X1),multiply(multiply(X1,multiply(multiply(X1,identity),X2)),identity)),identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),X2)),identity),
    inference(paramodulation,[status(thm)],[f4737,f159]) ).

fof(f5144,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))) = multiply(multiply(X1,X1),multiply(multiply(X1,multiply(multiply(X1,identity),X0)),identity)),
    inference(paramodulation,[status(thm)],[f4737,f45]) ).

fof(f5267,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),X1)),identity),
    inference(forward_demodulation,[status(thm)],[f4737,f5138]) ).

fof(f5281,plain,
    ! [X0,X1] : multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity))))),identity) = multiply(multiply(X0,identity),X1),
    inference(backward_demodulation,[status(thm)],[f5144,f5133]) ).

fof(f5673,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,multiply(identity,multiply(X1,X2))),identity)),identity)) = multiply(multiply(identity,X1),multiply(identity,X2)),
    inference(paramodulation,[status(thm)],[f3611,f134]) ).

fof(f5887,plain,
    ! [X0,X1] : multiply(identity,multiply(X0,X1)) = multiply(multiply(identity,X0),multiply(identity,X1)),
    inference(forward_demodulation,[status(thm)],[f134,f5673]) ).

fof(f6105,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity))) = multiply(multiply(identity,multiply(identity,multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),
    inference(paramodulation,[status(thm)],[f3362,f529]) ).

fof(f6198,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
    inference(backward_demodulation,[status(thm)],[f6200,f3424]) ).

fof(f6200,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))) = multiply(multiply(identity,multiply(identity,multiply(identity,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),
    inference(forward_demodulation,[status(thm)],[f4533,f6105]) ).

fof(f6221,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),identity))) = multiply(multiply(X0,multiply(X0,X0)),identity),
    inference(forward_demodulation,[status(thm)],[f377,f6198]) ).

fof(f6222,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),identity)))) = multiply(multiply(X0,multiply(X0,X0)),identity),
    inference(forward_demodulation,[status(thm)],[f377,f6221]) ).

fof(f6248,plain,
    ! [X0] : multiply(X0,multiply(multiply(X0,X0),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
    inference(forward_demodulation,[status(thm)],[f689,f6222]) ).

fof(f6261,plain,
    ! [X0] : multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),identity)) = multiply(multiply(identity,X0),identity),
    inference(paramodulation,[status(thm)],[f3362,f6248]) ).

fof(f6266,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity)) = multiply(X0,X0),
    inference(paramodulation,[status(thm)],[f6248,f134]) ).

fof(f6271,plain,
    ! [X0,X1] : multiply(multiply(X0,multiply(X1,multiply(X1,X1))),identity) = multiply(multiply(X0,identity),multiply(X1,multiply(multiply(X1,X1),identity))),
    inference(paramodulation,[status(thm)],[f6248,f4511]) ).

fof(f6272,plain,
    ! [X0,X1] : multiply(multiply(multiply(X0,multiply(X0,X0)),X1),identity) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X1,identity)),
    inference(paramodulation,[status(thm)],[f6248,f4511]) ).

fof(f6274,plain,
    ! [X0] : multiply(multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity)),identity)) = multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),
    inference(paramodulation,[status(thm)],[f6248,f749]) ).

fof(f6275,plain,
    ! [X0] : multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity))),identity)) = multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
    inference(paramodulation,[status(thm)],[f6248,f793]) ).

fof(f6281,plain,
    ! [X0] : multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),identity)) = multiply(identity,multiply(X0,identity)),
    inference(forward_demodulation,[status(thm)],[f377,f6261]) ).

fof(f6307,plain,
    ! [X0] : multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),identity)))),identity) = multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),
    inference(backward_demodulation,[status(thm)],[f6272,f879]) ).

fof(f6308,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),identity))) = X0,
    inference(backward_demodulation,[status(thm)],[f6272,f4251]) ).

fof(f6309,plain,
    ! [X0] : multiply(multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),identity),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),
    inference(backward_demodulation,[status(thm)],[f6272,f935]) ).

fof(f6312,plain,
    ! [X0] : multiply(multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),identity)) = multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f5267,f6274]) ).

fof(f6313,plain,
    ! [X0] : multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))),identity)) = multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f5267,f6275]) ).

fof(f6332,plain,
    ! [X0] : multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),identity))),identity) = multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),
    inference(forward_demodulation,[status(thm)],[f6272,f6307]) ).

fof(f6333,plain,
    ! [X0] : multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))),identity)),identity) = multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),
    inference(forward_demodulation,[status(thm)],[f6272,f6332]) ).

fof(f6334,plain,
    ! [X0] : multiply(multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),identity) = multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity)))),
    inference(forward_demodulation,[status(thm)],[f6313,f6333]) ).

fof(f6335,plain,
    ! [X0] : multiply(multiply(multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),identity),multiply(multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),identity),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),
    inference(forward_demodulation,[status(thm)],[f6334,f6309]) ).

fof(f6336,plain,
    ! [X0] : multiply(multiply(multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),identity)),identity) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),
    inference(forward_demodulation,[status(thm)],[f4511,f6335]) ).

fof(f6337,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),identity)),identity))) = X0,
    inference(backward_demodulation,[status(thm)],[f6343,f6308]) ).

fof(f6340,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),identity),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),identity)))) = multiply(X0,identity),
    inference(backward_demodulation,[status(thm)],[f6343,f4284]) ).

fof(f6343,plain,
    ! [X0] : multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),identity) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),
    inference(forward_demodulation,[status(thm)],[f6312,f6336]) ).

fof(f6348,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)))) = X0,
    inference(forward_demodulation,[status(thm)],[f5267,f6337]) ).

fof(f6349,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity)))) = X0,
    inference(forward_demodulation,[status(thm)],[f6248,f6348]) ).

fof(f6350,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))))) = X0,
    inference(forward_demodulation,[status(thm)],[f5267,f6349]) ).

fof(f6353,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),identity))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f4511,f6340]) ).

fof(f6481,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),X2))),identity) = multiply(multiply(X0,identity),multiply(multiply(X1,X1),multiply(multiply(X1,X2),identity))),
    inference(paramodulation,[status(thm)],[f5267,f4511]) ).

fof(f6653,plain,
    ! [X0,X1] : multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity)),identity)) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1),
    inference(paramodulation,[status(thm)],[f3569,f134]) ).

fof(f6737,plain,
    ! [X0,X1] : multiply(multiply(X0,multiply(multiply(X0,identity),multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity))),identity) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1),
    inference(forward_demodulation,[status(thm)],[f5128,f6653]) ).

fof(f6738,plain,
    ! [X0,X1] : multiply(multiply(X0,multiply(multiply(X0,multiply(X0,multiply(multiply(X0,identity),X1))),identity)),identity) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1),
    inference(forward_demodulation,[status(thm)],[f4511,f6737]) ).

fof(f7008,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,identity),identity)) = multiply(multiply(identity,multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),
    inference(paramodulation,[status(thm)],[f3361,f1406]) ).

fof(f7102,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,identity))) = multiply(multiply(identity,multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f377,f7008]) ).

fof(f7103,plain,
    ! [X0] : multiply(identity,multiply(identity,identity)) = multiply(multiply(identity,multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f7102]) ).

fof(f7104,plain,
    ! [X0] : multiply(identity,identity) = multiply(multiply(identity,multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f7103]) ).

fof(f7105,plain,
    ! [X0] : identity = multiply(multiply(identity,multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5,f7104]) ).

fof(f7106,plain,
    ! [X0] : identity = multiply(identity,multiply(multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))))),multiply(identity,multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f5887,f7105]) ).

fof(f7107,plain,
    ! [X0] : identity = multiply(identity,multiply(multiply(X0,identity),multiply(multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))),multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f3926,f7106]) ).

fof(f7108,plain,
    ! [X0] : identity = multiply(identity,multiply(multiply(X0,identity),multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))),multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f3361,f7107]) ).

fof(f7109,plain,
    ! [X0] : identity = multiply(identity,multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))),
    inference(forward_demodulation,[status(thm)],[f45,f7108]) ).

fof(f7110,plain,
    ! [X0] : identity = multiply(identity,multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity)),
    inference(forward_demodulation,[status(thm)],[f6481,f7109]) ).

fof(f7148,plain,
    ! [X0] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(identity,identity)),identity)) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
    inference(paramodulation,[status(thm)],[f7110,f134]) ).

fof(f7222,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(identity,identity))),identity) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
    inference(forward_demodulation,[status(thm)],[f4511,f7148]) ).

fof(f7223,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,multiply(identity,identity)),identity)) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
    inference(forward_demodulation,[status(thm)],[f377,f7222]) ).

fof(f7224,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,identity),identity))) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
    inference(forward_demodulation,[status(thm)],[f377,f7223]) ).

fof(f7225,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity)))) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
    inference(forward_demodulation,[status(thm)],[f377,f7224]) ).

fof(f7226,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,identity))) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
    inference(forward_demodulation,[status(thm)],[f5,f7225]) ).

fof(f7227,plain,
    ! [X0] : multiply(identity,multiply(identity,identity)) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
    inference(forward_demodulation,[status(thm)],[f5,f7226]) ).

fof(f7228,plain,
    ! [X0] : multiply(identity,identity) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
    inference(forward_demodulation,[status(thm)],[f5,f7227]) ).

fof(f7230,plain,
    ! [X0] : multiply(multiply(X0,X0),identity) = multiply(X0,X0),
    inference(backward_demodulation,[status(thm)],[f7235,f6266]) ).

fof(f7235,plain,
    ! [X0] : identity = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
    inference(forward_demodulation,[status(thm)],[f5,f7228]) ).

fof(f7250,plain,
    ! [X0] : multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))) = multiply(identity,multiply(X0,identity)),
    inference(backward_demodulation,[status(thm)],[f7230,f6281]) ).

fof(f7261,plain,
    ! [X0] : identity = multiply(multiply(X0,multiply(X0,multiply(X0,X0))),identity),
    inference(backward_demodulation,[status(thm)],[f7230,f7235]) ).

fof(f7279,plain,
    ! [X0,X1] : multiply(multiply(X0,multiply(X1,multiply(X1,X1))),identity) = multiply(multiply(X0,identity),multiply(X1,multiply(X1,X1))),
    inference(backward_demodulation,[status(thm)],[f7230,f6271]) ).

fof(f7344,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))) = X0,
    inference(backward_demodulation,[status(thm)],[f7434,f45]) ).

fof(f7345,plain,
    ! [X0,X1] : multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,X1)))),identity) = multiply(multiply(X0,identity),X1),
    inference(backward_demodulation,[status(thm)],[f7434,f5281]) ).

fof(f7352,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))))) = multiply(X0,identity),
    inference(backward_demodulation,[status(thm)],[f7434,f6353]) ).

fof(f7434,plain,
    ! [X0] : multiply(identity,X0) = multiply(identity,multiply(X0,identity)),
    inference(forward_demodulation,[status(thm)],[f3362,f7250]) ).

fof(f7470,plain,
    ! [X0] : identity = multiply(multiply(X0,identity),multiply(X0,multiply(X0,X0))),
    inference(backward_demodulation,[status(thm)],[f7279,f7261]) ).

fof(f7540,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,X0))) = X0,
    inference(forward_demodulation,[status(thm)],[f7434,f7344]) ).

fof(f7544,plain,
    ! [X0] : multiply(X0,multiply(multiply(X0,identity),multiply(X0,multiply(multiply(X0,identity),identity)))) = multiply(multiply(X0,X0),multiply(X0,X0)),
    inference(backward_demodulation,[status(thm)],[f7618,f793]) ).

fof(f7587,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(multiply(X0,multiply(X0,multiply(multiply(X0,identity),X1))),identity)) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1),
    inference(backward_demodulation,[status(thm)],[f7618,f6738]) ).

fof(f7618,plain,
    ! [X0,X1] : multiply(multiply(X0,X1),identity) = multiply(multiply(X0,identity),X1),
    inference(forward_demodulation,[status(thm)],[f7540,f7345]) ).

fof(f7672,plain,
    ! [X0] : X0 = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f6350,f7352]) ).

fof(f8055,plain,
    ! [X0] : identity = multiply(X0,multiply(X0,multiply(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f7672,f7470]) ).

fof(f8161,plain,
    ! [X0] : multiply(X0,multiply(X0,multiply(X0,multiply(multiply(X0,identity),identity)))) = multiply(multiply(X0,X0),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f7672,f7544]) ).

fof(f8162,plain,
    ! [X0] : multiply(X0,multiply(X0,multiply(X0,multiply(X0,identity)))) = multiply(multiply(X0,X0),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f7672,f8161]) ).

fof(f8163,plain,
    ! [X0] : multiply(X0,multiply(X0,multiply(X0,X0))) = multiply(multiply(X0,X0),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f7672,f8162]) ).

fof(f8168,plain,
    ! [X0] : identity = multiply(multiply(X0,X0),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f8055,f8163]) ).

fof(f8487,plain,
    ! [X0,X1] : multiply(multiply(X0,multiply(X0,multiply(X0,multiply(multiply(X0,identity),X1)))),identity) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1),
    inference(forward_demodulation,[status(thm)],[f4511,f7587]) ).

fof(f8488,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(X0,multiply(X0,multiply(multiply(X0,identity),X1)))) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1),
    inference(forward_demodulation,[status(thm)],[f7618,f8487]) ).

fof(f8489,plain,
    ! [X0,X1] : multiply(X0,multiply(X0,multiply(X0,multiply(multiply(X0,identity),X1)))) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1),
    inference(forward_demodulation,[status(thm)],[f7672,f8488]) ).

fof(f8490,plain,
    ! [X0,X1] : multiply(X0,multiply(X0,multiply(X0,multiply(X0,X1)))) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1),
    inference(forward_demodulation,[status(thm)],[f7672,f8489]) ).

fof(f8491,plain,
    ! [X0,X1] : multiply(X0,multiply(X0,multiply(X0,multiply(X0,X1)))) = multiply(identity,X1),
    inference(forward_demodulation,[status(thm)],[f8168,f8490]) ).

fof(f9200,plain,
    ! [X0] : multiply(X0,identity) = multiply(identity,X0),
    inference(paramodulation,[status(thm)],[f8055,f8491]) ).

fof(f9229,plain,
    a != a,
    inference(backward_demodulation,[status(thm)],[f9280,f6]) ).

fof(f9280,plain,
    ! [X0] : X0 = multiply(identity,X0),
    inference(forward_demodulation,[status(thm)],[f7672,f9200]) ).

fof(f9331,plain,
    $false,
    inference(trivial_equality_resolution,[status(thm)],[f9229]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : GRP120-1 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.03  % Command  : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35  % Computer : n015.cluster.edu
% 0.10/0.35  % Model    : x86_64 x86_64
% 0.10/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35  % Memory   : 8046.5625MB
% 0.10/0.35  % OS       : Linux 6.8.0-71-generic
% 0.10/0.35  % CPULimit : 300
% 0.10/0.35  % WCLimit  : 300
% 0.10/0.35  % DateTime : Sun Sep 20 20:01:05 UTC 2026
% 0.10/0.35  % CPUTime  : 
% 0.10/0.36  % Drodi V4.1.1
% 13.51/2.30  % Refutation found
% 13.51/2.30  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 13.51/2.30  % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.82/2.37  % Elapsed time: 1.995588 seconds
% 8.82/2.37  % CPU time: 15.527052 seconds
% 8.82/2.37  % Total memory used: 394.617 MB
% 8.82/2.37  % Net memory used: 374.555 MB
%------------------------------------------------------------------------------