↑ Up

Drodi---4.1.1.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Drodi---4.1.1
% Problem  : GRP122-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 : n016.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:34 PM UTC 2026

% Result   : Unsatisfiable 76.08s 10.19s
% Output   : CNFRefutation 76.08s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   92
%            Number of leaves      :    7
% Syntax   : Number of formulae    :  409 ( 409 unt;   4 def)
%            Number of atoms       :  409 ( 408 equ)
%            Maximal formula atoms :    1 (   1 avg)
%            Number of connectives :    3 (   3   ~;   0   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    5 (   3 avg)
%            Maximal term depth    :   14 (   2 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :    9 (   9 usr;   8 con; 0-2 aty)
%            Number of variables   :  672 ( 672   !;   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(multiply(a,b),c) != multiply(a,multiply(b,c)),
    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(multiply(a,b),c) != multiply(a,multiply(b,c)),
    inference(cnf_transformation,[status(thm)],[f3]) ).

fof(f7,definition,
    sF1_fnc = multiply(a,b),
    introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).

fof(f8,definition,
    sF0_fnc = multiply(sF1_fnc,c),
    introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).

fof(f9,definition,
    sF3_fnc = multiply(b,c),
    introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).

fof(f10,definition,
    sF2_fnc = multiply(a,sF3_fnc),
    introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).

fof(f11,plain,
    sF0_fnc != sF2_fnc,
    inference(definition_folding,[],[f6,f10,f9,f8,f7]) ).

fof(f12,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(f13,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(f18,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(f20,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(f21,plain,
    ! [X0] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(identity,identity))) = identity,
    inference(forward_demodulation,[status(thm)],[f5,f18]) ).

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

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

fof(f25,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)],[f22,f4]) ).

fof(f30,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,f25]) ).

fof(f31,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,f30]) ).

fof(f33,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)],[f23,f23]) ).

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

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

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

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

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

fof(f189,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)],[f52,f12]) ).

fof(f200,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)],[f12,f4]) ).

fof(f204,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)],[f12,f23]) ).

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

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

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

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

fof(f298,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,f204]) ).

fof(f299,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,f298]) ).

fof(f300,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,f299]) ).

fof(f301,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,f300]) ).

fof(f302,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,f301]) ).

fof(f303,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,f302]) ).

fof(f304,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,f303]) ).

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

fof(f320,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)],[f13,f305]) ).

fof(f321,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)],[f40,f305]) ).

fof(f324,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)],[f22,f305]) ).

fof(f325,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)],[f23,f305]) ).

fof(f326,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,f305]) ).

fof(f342,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,f320]) ).

fof(f348,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)],[f40,f342]) ).

fof(f355,plain,
    ! [X0] : multiply(identity,multiply(X0,identity)) = multiply(multiply(identity,X0),identity),
    inference(forward_demodulation,[status(thm)],[f305,f321]) ).

fof(f363,plain,
    ! [X0] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))) = identity,
    inference(backward_demodulation,[status(thm)],[f368,f22]) ).

fof(f368,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,f324]) ).

fof(f369,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity))) = X1,
    inference(backward_demodulation,[status(thm)],[f325,f23]) ).

fof(f458,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)],[f355,f305]) ).

fof(f481,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)],[f355,f458]) ).

fof(f493,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)],[f355,f363]) ).

fof(f517,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)],[f355,f493]) ).

fof(f541,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)],[f355,f369]) ).

fof(f618,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)],[f211,f355]) ).

fof(f619,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)],[f211,f305]) ).

fof(f633,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)],[f355,f618]) ).

fof(f634,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,f619]) ).

fof(f636,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)],[f355,f634]) ).

fof(f710,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)],[f31,f369]) ).

fof(f753,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)],[f33,f710]) ).

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

fof(f1009,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)],[f541,f12]) ).

fof(f1045,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)],[f997,f541]) ).

fof(f1080,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,f1045]) ).

fof(f1210,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)],[f633,f305]) ).

fof(f1211,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)],[f633,f12]) ).

fof(f1225,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,f1210]) ).

fof(f1227,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)],[f355,f1225]) ).

fof(f1228,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)],[f1227,f1211]) ).

fof(f1229,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)],[f1227,f1228]) ).

fof(f1230,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)],[f1227,f1229]) ).

fof(f1231,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)],[f1227,f1230]) ).

fof(f1232,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)],[f1227,f1231]) ).

fof(f1233,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)],[f1227,f1232]) ).

fof(f1234,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)],[f1227,f1233]) ).

fof(f1235,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)],[f1227,f1234]) ).

fof(f1236,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)],[f1227,f1235]) ).

fof(f1237,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)],[f33,f1236]) ).

fof(f2969,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)],[f52,f348]) ).

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

fof(f2983,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)],[f517,f348]) ).

fof(f3000,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(multiply(identity,multiply(identity,identity)),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))))),
    inference(paramodulation,[status(thm)],[f363,f348]) ).

fof(f3009,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)],[f355,f2969]) ).

fof(f3010,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,f3009]) ).

fof(f3011,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,f3010]) ).

fof(f3012,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,f3011]) ).

fof(f3014,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,f3012]) ).

fof(f3075,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(identity,multiply(X0,X1)),identity)),identity))) = multiply(multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
    inference(forward_demodulation,[status(thm)],[f355,f2982]) ).

fof(f3076,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(X0,X1)),identity),identity)))) = multiply(multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
    inference(forward_demodulation,[status(thm)],[f355,f3075]) ).

fof(f3077,plain,
    ! [X0,X1] : multiply(identity,multiply(X0,X1)) = multiply(multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
    inference(forward_demodulation,[status(thm)],[f52,f3076]) ).

fof(f3080,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(backward_demodulation,[status(thm)],[f3082,f1009]) ).

fof(f3082,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)],[f52,f3077]) ).

fof(f3083,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)],[f355,f2983]) ).

fof(f3084,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)],[f355,f3083]) ).

fof(f3085,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)],[f52,f3084]) ).

fof(f3086,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,f3085]) ).

fof(f3087,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,f3086]) ).

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

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

fof(f3162,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)],[f3014,f305]) ).

fof(f3301,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,f3162]) ).

fof(f3316,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)],[f636,f636]) ).

fof(f3330,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)],[f636,f305]) ).

fof(f3339,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)],[f355,f3316]) ).

fof(f3340,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)],[f355,f3339]) ).

fof(f3342,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)],[f3416,f12]) ).

fof(f3373,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)],[f3416,f1237]) ).

fof(f3374,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)],[f3416,f189]) ).

fof(f3416,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)],[f52,f3340]) ).

fof(f3477,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)],[f305,f3330]) ).

fof(f3686,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,X1)) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X2,multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity)))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity))),multiply(X1,identity)),identity))))),
    inference(paramodulation,[status(thm)],[f369,f3342]) ).

fof(f3983,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)],[f517,f326]) ).

fof(f4028,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))))),
    inference(paramodulation,[status(thm)],[f363,f326]) ).

fof(f4035,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,f3983]) ).

fof(f4036,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)],[f355,f4035]) ).

fof(f4037,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)],[f355,f4036]) ).

fof(f4038,plain,
    ! [X0] : multiply(multiply(identity,X0),multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))) = identity,
    inference(backward_demodulation,[status(thm)],[f4042,f517]) ).

fof(f4040,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)],[f4042,f3087]) ).

fof(f4042,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)],[f3301,f4037]) ).

fof(f4127,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)],[f4042,f4040]) ).

fof(f4128,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)],[f4042,f4127]) ).

fof(f4140,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)],[f355,f4038]) ).

fof(f4229,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)],[f355,f4140]) ).

fof(f4231,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)],[f4042,f4229]) ).

fof(f4281,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)],[f4231,f326]) ).

fof(f4395,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)],[f355,f4281]) ).

fof(f4396,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)],[f355,f4395]) ).

fof(f4687,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)],[f355,f481]) ).

fof(f4986,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)],[f355,f4687]) ).

fof(f5084,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)],[f200,f3477]) ).

fof(f5093,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)],[f200,f355]) ).

fof(f5393,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,f5084]) ).

fof(f5394,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)],[f355,f5393]) ).

fof(f5395,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)],[f355,f5394]) ).

fof(f5396,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,f5395]) ).

fof(f5397,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,f5396]) ).

fof(f5398,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,f5397]) ).

fof(f5399,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)],[f355,f5398]) ).

fof(f5400,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)],[f355,f5399]) ).

fof(f5409,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)],[f5411,f3416]) ).

fof(f5411,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)],[f52,f5400]) ).

fof(f5498,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,f5093]) ).

fof(f5499,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,f5498]) ).

fof(f5500,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,f5499]) ).

fof(f5501,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,f5500]) ).

fof(f5541,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)],[f5409,f3342]) ).

fof(f5596,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)],[f5409,f3373]) ).

fof(f5597,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)],[f5409,f3374]) ).

fof(f5633,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)],[f5541,f3080]) ).

fof(f5640,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,X1)) = multiply(X0,multiply(multiply(X0,X2),multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity))),multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity)))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity))),multiply(X1,identity)),identity))))),
    inference(backward_demodulation,[status(thm)],[f5541,f3686]) ).

fof(f5714,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(X1,identity))) = multiply(X0,multiply(multiply(X0,X1),identity)),
    inference(forward_demodulation,[status(thm)],[f52,f5596]) ).

fof(f5724,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)],[f5728,f5541]) ).

fof(f5728,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)],[f52,f5597]) ).

fof(f5749,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)],[f1080,f5633]) ).

fof(f5762,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)],[f5771,f4396]) ).

fof(f5771,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)],[f52,f5749]) ).

fof(f5836,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)],[f5771,f5762]) ).

fof(f5839,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)],[f5841,f4986]) ).

fof(f5841,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)],[f4128,f5836]) ).

fof(f5912,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)],[f5714,f305]) ).

fof(f6034,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)],[f6052,f3301]) ).

fof(f6052,plain,
    ! [X0,X1] : multiply(multiply(X0,X1),identity) = multiply(multiply(X0,identity),multiply(X1,identity)),
    inference(forward_demodulation,[status(thm)],[f305,f5912]) ).

fof(f6089,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)],[f6052,f6034]) ).

fof(f6090,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)],[f6052,f6089]) ).

fof(f6091,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)],[f6052,f6090]) ).

fof(f6120,plain,
    ! [X0,X1] : multiply(multiply(multiply(identity,X0),X1),identity) = multiply(multiply(identity,multiply(X0,identity)),multiply(X1,identity)),
    inference(paramodulation,[status(thm)],[f355,f6052]) ).

fof(f6125,plain,
    ! [X0,X1] : multiply(multiply(X0,multiply(identity,X1)),identity) = multiply(multiply(X0,identity),multiply(identity,multiply(X1,identity))),
    inference(paramodulation,[status(thm)],[f355,f6052]) ).

fof(f6127,plain,
    ! [X0,X1] : multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),identity))),identity) = multiply(multiply(X0,identity),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))),
    inference(paramodulation,[status(thm)],[f368,f6052]) ).

fof(f6145,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)],[f6052,f305]) ).

fof(f6267,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)],[f6052,f6145]) ).

fof(f6268,plain,
    ! [X0,X1] : multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity)),identity) = X1,
    inference(forward_demodulation,[status(thm)],[f6052,f6267]) ).

fof(f6334,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(identity,multiply(multiply(multiply(identity,X1),multiply(identity,X2)),X3))) = multiply(X0,multiply(multiply(identity,multiply(identity,multiply(X1,X2))),multiply(identity,X3))),
    inference(paramodulation,[status(thm)],[f5771,f5771]) ).

fof(f6379,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)],[f5771,f305]) ).

fof(f6400,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,X1)) = multiply(X0,multiply(multiply(X0,X2),multiply(identity,multiply(multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity)),multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity)))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity))),multiply(X1,identity)),identity))))),
    inference(backward_demodulation,[status(thm)],[f6401,f5640]) ).

fof(f6401,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(identity,multiply(multiply(multiply(identity,X1),multiply(identity,X2)),X3))) = multiply(X0,multiply(identity,multiply(multiply(identity,multiply(X1,X2)),X3))),
    inference(forward_demodulation,[status(thm)],[f5771,f6334]) ).

fof(f6519,plain,
    ! [X0] : multiply(multiply(multiply(identity,multiply(identity,X0)),multiply(multiply(identity,multiply(multiply(identity,X0),multiply(identity,X0))),identity)),multiply(X0,identity)) = identity,
    inference(backward_demodulation,[status(thm)],[f6556,f5839]) ).

fof(f6556,plain,
    ! [X0,X1] : multiply(identity,multiply(X0,X1)) = multiply(multiply(identity,X0),multiply(identity,X1)),
    inference(forward_demodulation,[status(thm)],[f305,f6379]) ).

fof(f6566,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,X1)) = multiply(X0,multiply(multiply(X0,X2),multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(X0,X2),identity),identity),multiply(multiply(multiply(X0,X2),identity),identity)))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity))),multiply(X1,identity)),identity))))),
    inference(forward_demodulation,[status(thm)],[f5771,f6400]) ).

fof(f6567,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,X1)) = multiply(X0,multiply(multiply(X0,X2),multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(X0,X2),identity),multiply(multiply(X0,X2),identity)),identity))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity))),multiply(X1,identity)),identity))))),
    inference(forward_demodulation,[status(thm)],[f6052,f6566]) ).

fof(f6568,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,X1)) = multiply(X0,multiply(multiply(X0,X2),multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(X0,X2),multiply(X0,X2)),identity),identity))),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity))),multiply(X1,identity)),identity))))),
    inference(forward_demodulation,[status(thm)],[f6052,f6567]) ).

fof(f6569,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,X1)) = multiply(X0,multiply(multiply(X0,X2),multiply(multiply(multiply(X0,X2),multiply(X0,X2)),multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity))),multiply(X1,identity)),identity))))),
    inference(forward_demodulation,[status(thm)],[f5409,f6568]) ).

fof(f6570,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,X1)) = multiply(X0,multiply(multiply(X0,X2),multiply(multiply(multiply(X0,X2),identity),multiply(multiply(X0,X2),multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X2),identity),identity))),multiply(X1,identity)),identity))))),
    inference(forward_demodulation,[status(thm)],[f5724,f6569]) ).

fof(f6649,plain,
    ! [X0] : multiply(multiply(multiply(identity,multiply(identity,X0)),multiply(identity,multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity))),multiply(X0,identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f355,f6519]) ).

fof(f6650,plain,
    ! [X0] : multiply(multiply(identity,multiply(multiply(identity,X0),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity))),multiply(X0,identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f6556,f6649]) ).

fof(f6651,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)],[f6556,f6650]) ).

fof(f6652,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)],[f355,f6651]) ).

fof(f6653,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(X0,identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f5771,f6652]) ).

fof(f6795,plain,
    ! [X0,X1] : multiply(multiply(identity,X0),multiply(multiply(identity,multiply(X0,X0)),multiply(multiply(multiply(identity,X0),multiply(X1,identity)),identity))) = X1,
    inference(paramodulation,[status(thm)],[f6556,f369]) ).

fof(f6798,plain,
    ! [X0,X1] : multiply(multiply(identity,multiply(X0,X0)),multiply(multiply(multiply(identity,X0),multiply(multiply(multiply(identity,X0),X1),identity)),identity)) = X1,
    inference(paramodulation,[status(thm)],[f6556,f305]) ).

fof(f6970,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)],[f6268,f305]) ).

fof(f6971,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)],[f6268,f6052]) ).

fof(f6972,plain,
    ! [X0,X1,X2] : multiply(multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity)),X2),identity) = multiply(X1,multiply(X2,identity)),
    inference(paramodulation,[status(thm)],[f6268,f6052]) ).

fof(f6973,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)],[f6268,f325]) ).

fof(f6977,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity))) = multiply(multiply(X2,X2),multiply(multiply(X2,multiply(multiply(X2,identity),X1)),identity)),
    inference(paramodulation,[status(thm)],[f6268,f369]) ).

fof(f6979,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)],[f6268,f52]) ).

fof(f6982,plain,
    ! [X0,X1] : multiply(multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity)),multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity))),multiply(multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity)),multiply(X1,identity)),identity)) = identity,
    inference(paramodulation,[status(thm)],[f6268,f305]) ).

fof(f7090,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)],[f6268,f6973]) ).

fof(f7097,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity)))),
    inference(backward_demodulation,[status(thm)],[f6979,f6977]) ).

fof(f7102,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)],[f6979,f6971]) ).

fof(f7109,plain,
    ! [X0,X1] : multiply(multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))),multiply(multiply(X1,X1),multiply(multiply(X1,multiply(multiply(X1,identity),X0)),identity))),multiply(multiply(multiply(multiply(X1,X1),multiply(multiply(X1,multiply(multiply(X1,identity),X0)),identity)),multiply(X0,identity)),identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f6979,f6982]) ).

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

fof(f7111,plain,
    ! [X0,X1] : multiply(multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X0,identity))),multiply(identity,multiply(identity,multiply(X0,identity))))),multiply(multiply(multiply(multiply(X1,X1),multiply(multiply(X1,multiply(multiply(X1,identity),X0)),identity)),multiply(X0,identity)),identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f6556,f7110]) ).

fof(f7112,plain,
    ! [X0,X1] : multiply(multiply(identity,multiply(multiply(identity,identity),multiply(multiply(identity,multiply(X0,identity)),multiply(identity,multiply(X0,identity))))),multiply(multiply(multiply(multiply(X1,X1),multiply(multiply(X1,multiply(multiply(X1,identity),X0)),identity)),multiply(X0,identity)),identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f5724,f7111]) ).

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

fof(f7114,plain,
    ! [X0,X1] : multiply(multiply(identity,multiply(identity,multiply(multiply(identity,identity),multiply(multiply(X0,identity),multiply(X0,identity))))),multiply(multiply(multiply(multiply(X1,X1),multiply(multiply(X1,multiply(multiply(X1,identity),X0)),identity)),multiply(X0,identity)),identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f5724,f7113]) ).

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

fof(f7116,plain,
    ! [X0,X1] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,X0),identity)))),multiply(multiply(multiply(multiply(X1,X1),multiply(multiply(X1,multiply(multiply(X1,identity),X0)),identity)),multiply(X0,identity)),identity)) = identity,
    inference(forward_demodulation,[status(thm)],[f6052,f7115]) ).

fof(f7117,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,X0),identity)))),multiply(X0,multiply(multiply(X0,identity),identity))) = identity,
    inference(forward_demodulation,[status(thm)],[f6972,f7116]) ).

fof(f7270,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)],[f5724,f305]) ).

fof(f7369,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,identity),multiply(X1,X2)) = multiply(multiply(X0,X1),multiply(identity,X2)),
    inference(forward_demodulation,[status(thm)],[f305,f7270]) ).

fof(f7444,plain,
    ! [X0] : multiply(multiply(X0,identity),sF3_fnc) = multiply(multiply(X0,b),multiply(identity,c)),
    inference(paramodulation,[status(thm)],[f9,f7369]) ).

fof(f7464,plain,
    ! [X0,X1,X2] : multiply(multiply(multiply(identity,X0),identity),multiply(multiply(identity,X1),X2)) = multiply(multiply(identity,multiply(X0,X1)),multiply(identity,X2)),
    inference(paramodulation,[status(thm)],[f6556,f7369]) ).

fof(f7476,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,identity),multiply(X1,multiply(identity,multiply(identity,multiply(multiply(X2,identity),identity))))) = multiply(multiply(X0,X1),X2),
    inference(paramodulation,[status(thm)],[f52,f7369]) ).

fof(f7552,plain,
    ! [X0,X1,X2] : multiply(multiply(identity,multiply(X0,identity)),multiply(multiply(identity,X1),X2)) = multiply(multiply(identity,multiply(X0,X1)),multiply(identity,X2)),
    inference(forward_demodulation,[status(thm)],[f355,f7464]) ).

fof(f7555,plain,
    ! [X0,X1,X2] : multiply(multiply(identity,multiply(X0,identity)),multiply(multiply(identity,X1),X2)) = multiply(identity,multiply(multiply(X0,X1),X2)),
    inference(forward_demodulation,[status(thm)],[f6556,f7552]) ).

fof(f7696,plain,
    multiply(multiply(a,identity),sF3_fnc) = multiply(sF1_fnc,multiply(identity,c)),
    inference(paramodulation,[status(thm)],[f7,f7444]) ).

fof(f8062,plain,
    ! [X0,X1] : multiply(multiply(multiply(identity,multiply(identity,multiply(X0,multiply(identity,multiply(identity,identity))))),X1),identity) = multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),multiply(X1,identity)),
    inference(paramodulation,[status(thm)],[f3477,f6120]) ).

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

fof(f8107,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(identity,X1)) = multiply(X0,multiply(multiply(X0,X2),multiply(multiply(multiply(X0,X2),identity),multiply(multiply(X0,X2),multiply(multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(X0,X2),identity))),X1),identity),identity))))),
    inference(backward_demodulation,[status(thm)],[f8109,f6570]) ).

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

fof(f8427,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)],[f6653,f305]) ).

fof(f8537,plain,
    ! [X0] : multiply(multiply(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)],[f6556,f8427]) ).

fof(f8538,plain,
    ! [X0] : multiply(multiply(identity,multiply(multiply(identity,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)],[f5724,f8537]) ).

fof(f8539,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,f8538]) ).

fof(f8540,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)],[f6556,f8539]) ).

fof(f8541,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)],[f355,f8540]) ).

fof(f8542,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)],[f6556,f8541]) ).

fof(f8543,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)],[f355,f8542]) ).

fof(f8544,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)],[f355,f8543]) ).

fof(f8545,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)],[f5724,f8544]) ).

fof(f8546,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)],[f6127,f8545]) ).

fof(f8547,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)],[f355,f8546]) ).

fof(f8548,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)],[f7090,f8547]) ).

fof(f8549,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)],[f7090,f8548]) ).

fof(f8577,plain,
    ! [X0,X1] : multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(multiply(identity,X0),X1),identity)) = multiply(multiply(multiply(identity,X0),multiply(multiply(identity,multiply(X0,X0)),X1)),identity),
    inference(paramodulation,[status(thm)],[f6556,f7090]) ).

fof(f8594,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)],[f7090,f6052]) ).

fof(f8599,plain,
    ! [X0,X1] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity)),identity)))) = multiply(X0,multiply(multiply(X0,X0),X1)),
    inference(paramodulation,[status(thm)],[f7090,f52]) ).

fof(f8682,plain,
    ! [X0,X1] : multiply(multiply(identity,multiply(X0,X0)),multiply(multiply(multiply(identity,X0),X1),identity)) = multiply(multiply(multiply(identity,X0),multiply(multiply(identity,multiply(X0,X0)),X1)),identity),
    inference(forward_demodulation,[status(thm)],[f6556,f8577]) ).

fof(f8763,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(X0,identity),identity)) = multiply(multiply(identity,multiply(X0,multiply(identity,X1))),multiply(X1,multiply(X1,X1))),
    inference(paramodulation,[status(thm)],[f5411,f3477]) ).

fof(f8768,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)],[f5411,f348]) ).

fof(f8920,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)],[f8922,f5501]) ).

fof(f8922,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)],[f6091,f8768]) ).

fof(f8956,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)],[f355,f8920]) ).

fof(f8957,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)],[f355,f8956]) ).

fof(f8989,plain,
    ! [X0] : multiply(X0,multiply(multiply(X0,X0),identity)) = multiply(multiply(X0,multiply(X0,X0)),identity),
    inference(forward_demodulation,[status(thm)],[f8599,f8957]) ).

fof(f9438,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)],[f5411,f8989]) ).

fof(f9445,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity)) = multiply(X0,X0),
    inference(paramodulation,[status(thm)],[f8989,f305]) ).

fof(f9452,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)],[f8989,f6052]) ).

fof(f9453,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)],[f8989,f6052]) ).

fof(f9464,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)],[f355,f9438]) ).

fof(f9658,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(identity,X1))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),identity),multiply(multiply(X0,X0),X1))),
    inference(paramodulation,[status(thm)],[f5724,f5728]) ).

fof(f9698,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)],[f5728,f305]) ).

fof(f9811,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)],[f6970,f9698]) ).

fof(f9812,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)],[f6052,f9811]) ).

fof(f10064,plain,
    ! [X0,X1,X2] : multiply(multiply(identity,multiply(X0,identity)),multiply(multiply(multiply(identity,X1),X2),identity)) = multiply(identity,multiply(multiply(X0,multiply(X1,identity)),multiply(X2,identity))),
    inference(paramodulation,[status(thm)],[f6120,f7555]) ).

fof(f10066,plain,
    ! [X0,X1,X2] : multiply(multiply(identity,multiply(X0,identity)),multiply(identity,multiply(X1,X2))) = multiply(identity,multiply(multiply(X0,X1),multiply(identity,X2))),
    inference(paramodulation,[status(thm)],[f6556,f7555]) ).

fof(f10135,plain,
    ! [X0,X1] : multiply(multiply(identity,multiply(X0,X0)),multiply(multiply(multiply(identity,X0),X1),identity)) = multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X1,identity))),
    inference(backward_demodulation,[status(thm)],[f10136,f8682]) ).

fof(f10136,plain,
    ! [X0,X1,X2] : multiply(multiply(multiply(identity,X0),multiply(multiply(identity,X1),X2)),identity) = multiply(identity,multiply(multiply(X0,multiply(X1,identity)),multiply(X2,identity))),
    inference(forward_demodulation,[status(thm)],[f6120,f10064]) ).

fof(f10140,plain,
    ! [X0,X1,X2] : multiply(identity,multiply(multiply(X0,identity),multiply(X1,X2))) = multiply(identity,multiply(multiply(X0,X1),multiply(identity,X2))),
    inference(forward_demodulation,[status(thm)],[f6556,f10066]) ).

fof(f10342,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(identity,X0),X1),identity)),identity)) = X1,
    inference(backward_demodulation,[status(thm)],[f10347,f6798]) ).

fof(f10345,plain,
    ! [X0,X1] : multiply(multiply(identity,X0),multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X1,identity)),identity))) = X1,
    inference(backward_demodulation,[status(thm)],[f10347,f6795]) ).

fof(f10347,plain,
    ! [X0,X1] : multiply(multiply(identity,multiply(X0,X0)),multiply(multiply(multiply(identity,X0),X1),identity)) = multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),X1),identity)),
    inference(forward_demodulation,[status(thm)],[f9453,f10135]) ).

fof(f10351,plain,
    ! [X0,X1] : multiply(identity,multiply(X0,multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X1,identity)),identity))) = X1,
    inference(forward_demodulation,[status(thm)],[f6556,f10345]) ).

fof(f10354,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(X0,multiply(multiply(multiply(X0,identity),multiply(multiply(X0,identity),multiply(X0,identity))),multiply(X1,identity))),identity)) = X1,
    inference(paramodulation,[status(thm)],[f6052,f10351]) ).

fof(f10363,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(identity,X0),multiply(X1,identity)),identity))) = X1,
    inference(paramodulation,[status(thm)],[f5411,f10351]) ).

fof(f10403,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(X0,multiply(multiply(multiply(X0,identity),multiply(multiply(X0,X0),identity)),multiply(X1,identity))),identity)) = X1,
    inference(forward_demodulation,[status(thm)],[f6052,f10354]) ).

fof(f10404,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(X0,multiply(multiply(multiply(X0,multiply(X0,X0)),identity),multiply(X1,identity))),identity)) = X1,
    inference(forward_demodulation,[status(thm)],[f6052,f10403]) ).

fof(f10405,plain,
    ! [X0,X1] : multiply(identity,multiply(multiply(X0,multiply(multiply(multiply(X0,multiply(X0,X0)),X1),identity)),identity)) = X1,
    inference(forward_demodulation,[status(thm)],[f6052,f10404]) ).

fof(f11157,plain,
    ! [X0] : multiply(identity,multiply(multiply(X0,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),identity))),identity)) = multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),
    inference(paramodulation,[status(thm)],[f8989,f10405]) ).

fof(f11220,plain,
    ! [X0] : multiply(identity,X0) = multiply(multiply(X0,multiply(X0,X0)),multiply(identity,multiply(multiply(X0,multiply(identity,multiply(X0,identity))),identity))),
    inference(backward_demodulation,[status(thm)],[f11241,f5411]) ).

fof(f11233,plain,
    ! [X0] : multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(identity,multiply(multiply(X0,multiply(identity,multiply(X0,identity))),identity)),identity)) = multiply(identity,multiply(X0,identity)),
    inference(backward_demodulation,[status(thm)],[f11241,f9464]) ).

fof(f11241,plain,
    ! [X0] : multiply(identity,multiply(multiply(X0,multiply(identity,multiply(X0,identity))),identity)) = multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f9464,f11157]) ).

fof(f11360,plain,
    ! [X0] : multiply(identity,X0) = multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X0,identity))),identity))),
    inference(forward_demodulation,[status(thm)],[f7369,f11220]) ).

fof(f11361,plain,
    ! [X0] : multiply(identity,X0) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X0,identity))))),identity),
    inference(forward_demodulation,[status(thm)],[f8594,f11360]) ).

fof(f11423,plain,
    ! [X0] : multiply(multiply(X0,multiply(X0,X0)),multiply(identity,multiply(multiply(multiply(X0,multiply(identity,multiply(X0,identity))),identity),identity))) = multiply(identity,multiply(X0,identity)),
    inference(forward_demodulation,[status(thm)],[f355,f11233]) ).

fof(f11424,plain,
    ! [X0] : multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(multiply(multiply(X0,multiply(identity,multiply(X0,identity))),identity),identity))) = multiply(identity,multiply(X0,identity)),
    inference(forward_demodulation,[status(thm)],[f7369,f11423]) ).

fof(f11755,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(multiply(identity,X1),X2)) = multiply(identity,multiply(multiply(multiply(multiply(X3,multiply(X3,X3)),multiply(multiply(multiply(identity,X3),X0),identity)),X1),X2)),
    inference(paramodulation,[status(thm)],[f10342,f7555]) ).

fof(f12090,plain,
    ! [X0] : multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(multiply(identity,X0),identity),identity)))) = multiply(multiply(identity,X0),multiply(identity,X0)),
    inference(paramodulation,[status(thm)],[f7090,f10363]) ).

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

fof(f12125,plain,
    ! [X0,X1,X2] : multiply(identity,multiply(X0,multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(multiply(identity,X1),multiply(X2,identity)),identity)))) = multiply(multiply(identity,X0),X2),
    inference(paramodulation,[status(thm)],[f10363,f6556]) ).

fof(f12166,plain,
    ! [X0] : multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(identity,multiply(X0,X0)),multiply(multiply(multiply(identity,X0),identity),identity)))) = multiply(multiply(identity,X0),multiply(identity,X0)),
    inference(forward_demodulation,[status(thm)],[f6556,f12090]) ).

fof(f12167,plain,
    ! [X0] : multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)))) = multiply(multiply(identity,X0),multiply(identity,X0)),
    inference(forward_demodulation,[status(thm)],[f10347,f12166]) ).

fof(f12168,plain,
    ! [X0] : multiply(identity,multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)))) = multiply(multiply(identity,X0),multiply(identity,X0)),
    inference(forward_demodulation,[status(thm)],[f10140,f12167]) ).

fof(f12169,plain,
    ! [X0] : multiply(identity,multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity)))) = multiply(multiply(identity,X0),multiply(identity,X0)),
    inference(forward_demodulation,[status(thm)],[f8989,f12168]) ).

fof(f12170,plain,
    ! [X0] : multiply(identity,multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,X0),identity)))),identity)) = multiply(multiply(identity,X0),multiply(identity,X0)),
    inference(forward_demodulation,[status(thm)],[f8594,f12169]) ).

fof(f12171,plain,
    ! [X0] : multiply(identity,multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity))))),identity)) = multiply(multiply(identity,X0),multiply(identity,X0)),
    inference(forward_demodulation,[status(thm)],[f7097,f12170]) ).

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

fof(f12173,plain,
    ! [X0] : multiply(identity,multiply(multiply(X0,identity),X0)) = multiply(identity,multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f6556,f12172]) ).

fof(f12238,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,identity),multiply(multiply(identity,multiply(multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(multiply(identity,X1),multiply(X0,identity)),identity)),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(multiply(identity,X1),multiply(X0,identity)),identity)))),multiply(multiply(X0,multiply(X2,identity)),identity))) = X2,
    inference(forward_demodulation,[status(thm)],[f11755,f12102]) ).

fof(f12320,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,identity),multiply(multiply(multiply(identity,multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(multiply(identity,X1),multiply(X0,identity)),identity))),X0),multiply(multiply(X0,multiply(X2,identity)),identity))) = X2,
    inference(backward_demodulation,[status(thm)],[f12125,f12238]) ).

fof(f12344,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity))) = X1,
    inference(forward_demodulation,[status(thm)],[f10363,f12320]) ).

fof(f12346,plain,
    ! [X0,X1] : multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),multiply(X1,identity)))),identity) = X1,
    inference(forward_demodulation,[status(thm)],[f8594,f12344]) ).

fof(f12404,plain,
    ! [X0] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(multiply(identity,multiply(X0,X0)),identity)),identity)) = multiply(multiply(X0,identity),X0),
    inference(paramodulation,[status(thm)],[f12173,f305]) ).

fof(f12498,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,X0)),identity))),identity) = multiply(multiply(X0,identity),X0),
    inference(forward_demodulation,[status(thm)],[f6052,f12404]) ).

fof(f12499,plain,
    ! [X0] : multiply(identity,multiply(multiply(identity,multiply(multiply(identity,multiply(X0,X0)),identity)),identity)) = multiply(multiply(X0,identity),X0),
    inference(forward_demodulation,[status(thm)],[f355,f12498]) ).

fof(f12500,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(X0,X0)),identity),identity))) = multiply(multiply(X0,identity),X0),
    inference(forward_demodulation,[status(thm)],[f355,f12499]) ).

fof(f12501,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(X0,X0),identity)),identity))) = multiply(multiply(X0,identity),X0),
    inference(forward_demodulation,[status(thm)],[f355,f12500]) ).

fof(f12502,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X0),identity),identity)))) = multiply(multiply(X0,identity),X0),
    inference(forward_demodulation,[status(thm)],[f355,f12501]) ).

fof(f12511,plain,
    ! [X0] : multiply(X0,X0) = multiply(multiply(X0,identity),X0),
    inference(forward_demodulation,[status(thm)],[f52,f12502]) ).

fof(f12577,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X1,identity),identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,X1))),multiply(X1,multiply(X1,X1))),
    inference(paramodulation,[status(thm)],[f12511,f326]) ).

fof(f12766,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X1,identity),identity)),identity)) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity)),
    inference(forward_demodulation,[status(thm)],[f326,f12577]) ).

fof(f12809,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(identity,X1)) = multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(multiply(multiply(multiply(X0,identity),X0),identity),multiply(multiply(multiply(X0,identity),X0),multiply(multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),X0),identity))),X1),identity),identity))))),
    inference(paramodulation,[status(thm)],[f12511,f8107]) ).

fof(f13182,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(identity,X1)) = multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),identity),multiply(multiply(multiply(X0,identity),X0),multiply(multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),X0),identity))),X1),identity),identity))))),
    inference(forward_demodulation,[status(thm)],[f12511,f12809]) ).

fof(f13183,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(identity,X1)) = multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),identity),multiply(multiply(X0,X0),multiply(multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),X0),identity))),X1),identity),identity))))),
    inference(forward_demodulation,[status(thm)],[f12511,f13182]) ).

fof(f13184,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(identity,X1)) = multiply(multiply(X0,identity),multiply(X0,multiply(multiply(X0,identity),multiply(identity,multiply(multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),X0),identity))),X1),identity),identity))))),
    inference(forward_demodulation,[status(thm)],[f9658,f13183]) ).

fof(f13185,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(identity,X1)) = multiply(multiply(X0,identity),multiply(X0,multiply(multiply(X0,multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),X0),identity))),X1),identity))),identity))),
    inference(forward_demodulation,[status(thm)],[f6125,f13184]) ).

fof(f13186,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(identity,X1)) = multiply(multiply(X0,identity),multiply(X0,multiply(multiply(X0,multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(multiply(X0,X0),identity))),X1),identity))),identity))),
    inference(forward_demodulation,[status(thm)],[f12511,f13185]) ).

fof(f14435,plain,
    ! [X0] : multiply(multiply(X0,multiply(X0,multiply(multiply(X0,identity),multiply(X0,identity)))),identity) = identity,
    inference(paramodulation,[status(thm)],[f5724,f12346]) ).

fof(f14447,plain,
    ! [X0,X1] : multiply(multiply(X0,multiply(X0,X1)),identity) = multiply(X0,multiply(multiply(X0,X1),identity)),
    inference(paramodulation,[status(thm)],[f305,f12346]) ).

fof(f14465,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity)) = multiply(X0,multiply(multiply(X0,X0),multiply(X1,identity))),
    inference(paramodulation,[status(thm)],[f12346,f305]) ).

fof(f14521,plain,
    ! [X0] : multiply(multiply(X0,X0),identity) = multiply(X0,X0),
    inference(backward_demodulation,[status(thm)],[f14524,f9445]) ).

fof(f14524,plain,
    ! [X0] : multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),identity))),identity) = identity,
    inference(forward_demodulation,[status(thm)],[f6052,f14435]) ).

fof(f14552,plain,
    ! [X0] : multiply(X0,multiply(X0,multiply(multiply(X0,multiply(multiply(X0,identity),identity)),identity))) = multiply(multiply(X0,X0),multiply(X0,X0)),
    inference(backward_demodulation,[status(thm)],[f14447,f753]) ).

fof(f14566,plain,
    ! [X0,X1] : multiply(multiply(X0,multiply(X0,multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity))),identity) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1),
    inference(backward_demodulation,[status(thm)],[f14447,f9812]) ).

fof(f14692,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))) = multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity),
    inference(backward_demodulation,[status(thm)],[f14465,f6970]) ).

fof(f14717,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,identity))),identity)))) = multiply(X0,identity),
    inference(backward_demodulation,[status(thm)],[f14465,f8549]) ).

fof(f14723,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(X1,multiply(multiply(X1,X1),multiply(identity,identity)))))),
    inference(backward_demodulation,[status(thm)],[f14465,f4028]) ).

fof(f14725,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),multiply(X0,multiply(multiply(X0,X0),multiply(identity,identity)))))),
    inference(backward_demodulation,[status(thm)],[f14465,f3123]) ).

fof(f14755,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(multiply(X1,identity),identity),identity))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity)),
    inference(backward_demodulation,[status(thm)],[f14465,f12766]) ).

fof(f14997,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(identity,X1)) = multiply(multiply(X0,identity),multiply(X0,multiply(multiply(X0,multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(X0,X0))),X1),identity))),identity))),
    inference(backward_demodulation,[status(thm)],[f14521,f13186]) ).

fof(f15016,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)],[f14521,f9452]) ).

fof(f15028,plain,
    ! [X0] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,X0)))),multiply(X0,multiply(multiply(X0,identity),identity))) = identity,
    inference(backward_demodulation,[status(thm)],[f14521,f7117]) ).

fof(f15057,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity)),identity)) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1),
    inference(forward_demodulation,[status(thm)],[f14447,f14566]) ).

fof(f15225,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,identity),multiply(X1,identity))) = multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity),
    inference(forward_demodulation,[status(thm)],[f5728,f14692]) ).

fof(f15252,plain,
    ! [X0] : multiply(X0,multiply(X0,multiply(X0,multiply(multiply(X0,identity),identity)))) = multiply(multiply(X0,X0),multiply(X0,X0)),
    inference(backward_demodulation,[status(thm)],[f15254,f14552]) ).

fof(f15253,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X1),identity))),identity)) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1),
    inference(backward_demodulation,[status(thm)],[f15254,f15057]) ).

fof(f15254,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X1),identity)) = multiply(multiply(X0,multiply(multiply(X0,identity),X1)),identity),
    inference(forward_demodulation,[status(thm)],[f6052,f15225]) ).

fof(f15409,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(multiply(X0,X0),identity))),multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,identity))),identity)))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f14521,f14717]) ).

fof(f15410,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),multiply(identity,identity))),identity)))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f14521,f15409]) ).

fof(f15411,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(X0,multiply(identity,multiply(X0,identity))),identity)),multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,identity))),identity)))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f11241,f15410]) ).

fof(f15412,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(identity,multiply(X0,identity)))),multiply(X0,multiply(multiply(X0,X0),multiply(identity,identity)))),identity))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f6120,f15411]) ).

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

fof(f15414,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(identity,multiply(X0,identity)))),multiply(X0,multiply(X0,X0))),identity))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f14521,f15413]) ).

fof(f15450,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,identity),identity))) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(X1,multiply(multiply(X1,X1),multiply(identity,identity)))))),
    inference(forward_demodulation,[status(thm)],[f14465,f14723]) ).

fof(f15451,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(X1,multiply(multiply(X1,X1),multiply(identity,identity)))))),
    inference(forward_demodulation,[status(thm)],[f14521,f15450]) ).

fof(f15452,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X1,multiply(multiply(X1,X1),multiply(identity,identity))),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(X1,multiply(multiply(X1,X1),multiply(identity,identity)))))),
    inference(forward_demodulation,[status(thm)],[f14465,f15451]) ).

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

fof(f15454,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(X1,multiply(multiply(X1,X1),multiply(identity,identity)))))),
    inference(forward_demodulation,[status(thm)],[f14521,f15453]) ).

fof(f15455,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(multiply(X1,X1),multiply(identity,identity))),multiply(X1,multiply(multiply(X1,X1),multiply(identity,identity)))))),
    inference(forward_demodulation,[status(thm)],[f14465,f15454]) ).

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

fof(f15457,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(multiply(X1,X1),multiply(identity,identity)))))),
    inference(forward_demodulation,[status(thm)],[f14521,f15456]) ).

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

fof(f15459,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
    inference(forward_demodulation,[status(thm)],[f14521,f15458]) ).

fof(f15460,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X1,multiply(X1,X1)),multiply(identity,multiply(multiply(X1,multiply(identity,multiply(X1,identity))),identity)))),
    inference(forward_demodulation,[status(thm)],[f11241,f15459]) ).

fof(f15461,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X1,identity),multiply(multiply(X1,X1),multiply(multiply(X1,multiply(identity,multiply(X1,identity))),identity)))),
    inference(forward_demodulation,[status(thm)],[f7369,f15460]) ).

fof(f15462,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X1,multiply(X1,multiply(multiply(X1,X1),multiply(identity,multiply(X1,identity))))),identity)),
    inference(forward_demodulation,[status(thm)],[f8594,f15461]) ).

fof(f15463,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,identity),identity))) = multiply(multiply(X0,multiply(X0,X0)),multiply(identity,X1)),
    inference(forward_demodulation,[status(thm)],[f11361,f15462]) ).

fof(f15501,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,identity),identity))) = multiply(multiply(X0,identity),multiply(multiply(X0,X0),X1)),
    inference(forward_demodulation,[status(thm)],[f7369,f15463]) ).

fof(f15517,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,identity))),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),multiply(X0,multiply(multiply(X0,X0),multiply(identity,identity)))))),
    inference(forward_demodulation,[status(thm)],[f14465,f14725]) ).

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

fof(f15519,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),multiply(X0,multiply(multiply(X0,X0),multiply(identity,identity)))))),
    inference(forward_demodulation,[status(thm)],[f14521,f15518]) ).

fof(f15520,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,identity))),multiply(X0,multiply(multiply(X0,X0),multiply(identity,identity)))))),
    inference(forward_demodulation,[status(thm)],[f14465,f15519]) ).

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

fof(f15522,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(multiply(X0,X0),multiply(identity,identity)))))),
    inference(forward_demodulation,[status(thm)],[f14521,f15521]) ).

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

fof(f15524,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))))),
    inference(forward_demodulation,[status(thm)],[f14521,f15523]) ).

fof(f15525,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(identity,multiply(multiply(X0,multiply(identity,multiply(X0,identity))),identity)))),
    inference(forward_demodulation,[status(thm)],[f11241,f15524]) ).

fof(f15526,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X0,identity))),identity)))),
    inference(forward_demodulation,[status(thm)],[f10140,f15525]) ).

fof(f15527,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X0,identity))))),identity)),
    inference(forward_demodulation,[status(thm)],[f8594,f15526]) ).

fof(f15530,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,X0))) = X0,
    inference(backward_demodulation,[status(thm)],[f15557,f52]) ).

fof(f15552,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,identity),multiply(X1,multiply(identity,multiply(identity,X2)))) = multiply(multiply(X0,X1),X2),
    inference(backward_demodulation,[status(thm)],[f15557,f7476]) ).

fof(f15556,plain,
    ! [X0,X1] : multiply(X0,multiply(identity,X1)) = multiply(identity,multiply(multiply(identity,multiply(identity,X0)),X1)),
    inference(backward_demodulation,[status(thm)],[f15557,f5409]) ).

fof(f15557,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(identity,X0)),
    inference(forward_demodulation,[status(thm)],[f11361,f15527]) ).

fof(f15661,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(X1,identity))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity)),
    inference(forward_demodulation,[status(thm)],[f15501,f14755]) ).

fof(f15662,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(X1,identity))) = multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,identity),identity))),
    inference(forward_demodulation,[status(thm)],[f14465,f15661]) ).

fof(f15664,plain,
    ! [X0] : multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X0,identity))),identity))) = multiply(identity,multiply(X0,identity)),
    inference(backward_demodulation,[status(thm)],[f15666,f11424]) ).

fof(f15666,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(X1,identity))) = multiply(multiply(X0,identity),multiply(multiply(X0,X0),X1)),
    inference(forward_demodulation,[status(thm)],[f15501,f15662]) ).

fof(f15889,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(identity,multiply(X0,identity)))),identity),multiply(X0,multiply(X0,X0))))) = multiply(X0,identity),
    inference(backward_demodulation,[status(thm)],[f15016,f15414]) ).

fof(f15938,plain,
    ! [X0,X1] : multiply(X0,multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X1),identity)),identity))) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1),
    inference(forward_demodulation,[status(thm)],[f14447,f15253]) ).

fof(f15966,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(X0,multiply(multiply(X0,identity),identity))) = identity,
    inference(backward_demodulation,[status(thm)],[f15530,f15028]) ).

fof(f16030,plain,
    ! [X0] : multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X0,identity))))),identity) = multiply(identity,multiply(X0,identity)),
    inference(forward_demodulation,[status(thm)],[f8594,f15664]) ).

fof(f16042,plain,
    ! [X0,X1] : multiply(multiply(X0,identity),multiply(identity,X1)) = multiply(multiply(X0,identity),multiply(X0,multiply(multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X0,X0))),X1))),identity))),
    inference(backward_demodulation,[status(thm)],[f16082,f14997]) ).

fof(f16082,plain,
    ! [X0] : multiply(identity,X0) = multiply(identity,multiply(X0,identity)),
    inference(forward_demodulation,[status(thm)],[f11361,f16030]) ).

fof(f16136,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(X0,multiply(identity,multiply(X0,identity))),identity)),multiply(X0,multiply(X0,X0))))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f355,f15889]) ).

fof(f16137,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,multiply(identity,multiply(X0,identity)))),multiply(X0,multiply(X0,X0))))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f16082,f16136]) ).

fof(f16138,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,multiply(identity,X0))),multiply(X0,multiply(X0,X0))))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f16082,f16137]) ).

fof(f16139,plain,
    ! [X0] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))) = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f8763,f16138]) ).

fof(f16141,plain,
    multiply(a,sF3_fnc) = multiply(sF1_fnc,multiply(identity,c)),
    inference(backward_demodulation,[status(thm)],[f16393,f7696]) ).

fof(f16150,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X0,X1),multiply(identity,X2)),
    inference(backward_demodulation,[status(thm)],[f16393,f7369]) ).

fof(f16280,plain,
    ! [X0] : multiply(X0,multiply(X0,multiply(X0,multiply(X0,identity)))) = multiply(multiply(X0,X0),multiply(X0,X0)),
    inference(backward_demodulation,[status(thm)],[f16393,f15252]) ).

fof(f16318,plain,
    ! [X0,X1] : multiply(X0,multiply(X0,multiply(X0,multiply(multiply(X0,X1),identity)))) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1),
    inference(backward_demodulation,[status(thm)],[f16393,f15938]) ).

fof(f16338,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,multiply(identity,multiply(identity,X2)))) = multiply(multiply(X0,X1),X2),
    inference(backward_demodulation,[status(thm)],[f16393,f15552]) ).

fof(f16393,plain,
    ! [X0] : X0 = multiply(X0,identity),
    inference(forward_demodulation,[status(thm)],[f52,f16139]) ).

fof(f16460,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(X0,multiply(X0,identity))) = identity,
    inference(forward_demodulation,[status(thm)],[f16393,f15966]) ).

fof(f16461,plain,
    ! [X0] : multiply(multiply(X0,X0),multiply(X0,X0)) = identity,
    inference(forward_demodulation,[status(thm)],[f16393,f16460]) ).

fof(f16623,plain,
    ! [X0,X1] : multiply(X0,multiply(identity,X1)) = multiply(multiply(X0,identity),multiply(X0,multiply(multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X0,X0))),X1))),identity))),
    inference(forward_demodulation,[status(thm)],[f16393,f16042]) ).

fof(f16624,plain,
    ! [X0,X1] : multiply(X0,multiply(identity,X1)) = multiply(X0,multiply(X0,multiply(multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X0,X0))),X1))),identity))),
    inference(forward_demodulation,[status(thm)],[f16393,f16623]) ).

fof(f16625,plain,
    ! [X0,X1] : multiply(X0,multiply(identity,X1)) = multiply(X0,multiply(X0,multiply(X0,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X0,X0))),X1))))),
    inference(forward_demodulation,[status(thm)],[f16393,f16624]) ).

fof(f16626,plain,
    ! [X0,X1] : multiply(X0,multiply(identity,X1)) = multiply(X0,multiply(X0,multiply(X0,multiply(multiply(X0,X0),multiply(identity,X1))))),
    inference(forward_demodulation,[status(thm)],[f15556,f16625]) ).

fof(f16780,plain,
    sF2_fnc = multiply(sF1_fnc,multiply(identity,c)),
    inference(forward_demodulation,[status(thm)],[f10,f16141]) ).

fof(f16822,plain,
    ! [X0,X1] : multiply(X0,multiply(identity,X1)) = multiply(X0,multiply(X0,multiply(X0,multiply(X0,multiply(X0,X1))))),
    inference(backward_demodulation,[status(thm)],[f16150,f16626]) ).

fof(f17330,plain,
    ! [X0] : multiply(X0,multiply(X0,multiply(X0,X0))) = multiply(multiply(X0,X0),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f16393,f16280]) ).

fof(f17336,plain,
    ! [X0] : multiply(X0,multiply(X0,multiply(X0,X0))) = identity,
    inference(forward_demodulation,[status(thm)],[f16461,f17330]) ).

fof(f17505,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)],[f16393,f16318]) ).

fof(f17506,plain,
    ! [X0,X1] : multiply(X0,multiply(X0,multiply(X0,multiply(X0,X1)))) = multiply(identity,X1),
    inference(forward_demodulation,[status(thm)],[f16461,f17505]) ).

fof(f17723,plain,
    ! [X0,X1] : multiply(X0,multiply(identity,X1)) = multiply(identity,multiply(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f17506,f16822]) ).

fof(f17967,plain,
    ! [X0] : multiply(X0,identity) = multiply(identity,multiply(X0,multiply(identity,multiply(identity,identity)))),
    inference(paramodulation,[status(thm)],[f17336,f17723]) ).

fof(f17975,plain,
    multiply(sF1_fnc,multiply(identity,c)) = multiply(identity,sF0_fnc),
    inference(paramodulation,[status(thm)],[f8,f17723]) ).

fof(f18023,plain,
    ! [X0] : X0 = multiply(identity,multiply(X0,multiply(identity,multiply(identity,identity)))),
    inference(forward_demodulation,[status(thm)],[f16393,f17967]) ).

fof(f18024,plain,
    ! [X0] : X0 = multiply(multiply(identity,X0),identity),
    inference(forward_demodulation,[status(thm)],[f16338,f18023]) ).

fof(f18056,plain,
    ! [X0] : X0 = multiply(identity,X0),
    inference(forward_demodulation,[status(thm)],[f16393,f18024]) ).

fof(f18067,plain,
    sF2_fnc = multiply(identity,sF0_fnc),
    inference(forward_demodulation,[status(thm)],[f16780,f17975]) ).

fof(f18068,plain,
    sF2_fnc = sF0_fnc,
    inference(forward_demodulation,[status(thm)],[f18056,f18067]) ).

fof(f18069,plain,
    $false,
    inference(forward_subsumption_resolution,[status(thm)],[f18068,f11]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP122-1 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04  % Command  : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36  % Computer : n016.cluster.edu
% 0.09/0.36  % Model    : x86_64 x86_64
% 0.09/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36  % Memory   : 8046.5625MB
% 0.09/0.36  % OS       : Linux 6.8.0-71-generic
% 0.09/0.37  % CPULimit : 300
% 0.09/0.37  % WCLimit  : 300
% 0.09/0.37  % DateTime : Sun Sep 20 20:02:23 UTC 2026
% 0.09/0.37  % CPUTime  : 
% 0.09/0.38  % Drodi V4.1.1
% 76.08/10.19  % Refutation found
% 76.08/10.19  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 76.08/10.19  % SZS output start CNFRefutation for theBenchmark
% See solution above
% 19.04/14.26  % Elapsed time: 13.885394 seconds
% 19.04/14.26  % CPU time: 99.574150 seconds
% 19.04/14.26  % Total memory used: 18.845 GB
% 19.04/14.26  % Net memory used: 18.819 GB
%------------------------------------------------------------------------------