Drodi---4.1.1.UNS-CRf.s

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

% Computer : n017.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:06:24 PM UTC 2026

% Result   : Unsatisfiable 214.83s 27.68s
% Output   : CNFRefutation 144.76s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)

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

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

fof(f3,axiom,
    ! [X] : add(X,inverse(X)) = n1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f4,axiom,
    ! [X,Y,Z] : pixley(X,Y,Z) = add(multiply(X,inverse(Y)),add(multiply(X,Z),multiply(inverse(Y),Z))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f5,axiom,
    ! [X,Y] : pixley(X,X,Y) = Y,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f6,axiom,
    ! [X,Y] : pixley(X,Y,Y) = X,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f7,axiom,
    ! [X,Y] : pixley(X,Y,X) = X,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

fof(f8,negated_conjecture,
    add(a,multiply(b,c)) != multiply(add(a,b),add(a,c)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

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

fof(f10,plain,
    ! [X0,X1,X2] : multiply(X0,add(X1,X2)) = add(multiply(X1,X0),multiply(X2,X0)),
    inference(cnf_transformation,[status(thm)],[f2]) ).

fof(f11,plain,
    ! [X0] : add(X0,inverse(X0)) = n1,
    inference(cnf_transformation,[status(thm)],[f3]) ).

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

fof(f13,plain,
    ! [X0,X1] : pixley(X0,X0,X1) = X1,
    inference(cnf_transformation,[status(thm)],[f5]) ).

fof(f14,plain,
    ! [X0,X1] : pixley(X0,X1,X1) = X0,
    inference(cnf_transformation,[status(thm)],[f6]) ).

fof(f15,plain,
    ! [X0,X1] : pixley(X0,X1,X0) = X0,
    inference(cnf_transformation,[status(thm)],[f7]) ).

fof(f16,plain,
    add(a,multiply(b,c)) != multiply(add(a,b),add(a,c)),
    inference(cnf_transformation,[status(thm)],[f8]) ).

fof(f23,plain,
    ! [X0,X1,X2] : pixley(X0,X1,X2) = add(multiply(X0,inverse(X1)),multiply(X2,add(X0,inverse(X1)))),
    inference(forward_demodulation,[status(thm)],[f10,f12]) ).

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

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

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

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

fof(f28,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,multiply(X1,add(X2,X3))),multiply(multiply(X3,X1),X0)) = multiply(multiply(X3,X1),X0),
    inference(paramodulation,[status(thm)],[f10,f26]) ).

fof(f31,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,X1),add(X2,multiply(X1,add(X3,X0)))) = add(multiply(X2,multiply(X0,X1)),multiply(X0,X1)),
    inference(paramodulation,[status(thm)],[f26,f10]) ).

fof(f32,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,X1),add(multiply(X1,add(X2,X0)),X3)) = add(multiply(X0,X1),multiply(X3,multiply(X0,X1))),
    inference(paramodulation,[status(thm)],[f26,f10]) ).

fof(f33,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(multiply(X2,X1),X1)) = multiply(X1,add(X2,add(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f25,f27]) ).

fof(f34,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(multiply(X2,X1),X1)) = add(multiply(X2,X1),X1),
    inference(forward_demodulation,[status(thm)],[f25,f33]) ).

fof(f39,plain,
    ! [X0,X1,X2] : pixley(add(X0,inverse(X1)),X1,X2) = add(inverse(X1),multiply(X2,add(add(X0,inverse(X1)),inverse(X1)))),
    inference(paramodulation,[status(thm)],[f9,f23]) ).

fof(f41,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,pixley(X1,X2,X3)),multiply(multiply(X3,add(X1,inverse(X2))),X0)) = multiply(multiply(X3,add(X1,inverse(X2))),X0),
    inference(paramodulation,[status(thm)],[f23,f26]) ).

fof(f42,plain,
    ! [X0,X1,X2] : multiply(pixley(X0,X1,X2),multiply(X2,add(X0,inverse(X1)))) = multiply(X2,add(X0,inverse(X1))),
    inference(paramodulation,[status(thm)],[f23,f9]) ).

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

fof(f49,plain,
    ! [X0,X1,X2] : multiply(add(multiply(X0,X1),X1),multiply(X1,add(X2,X1))) = multiply(X1,add(X2,X1)),
    inference(paramodulation,[status(thm)],[f34,f26]) ).

fof(f58,plain,
    ! [X0,X1] : multiply(add(X0,X1),add(X1,X1)) = add(X1,X1),
    inference(forward_demodulation,[status(thm)],[f9,f47]) ).

fof(f61,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X2)),add(multiply(X2,X0),multiply(X2,X0))) = add(multiply(X2,X0),multiply(X2,X0)),
    inference(paramodulation,[status(thm)],[f10,f58]) ).

fof(f64,plain,
    ! [X0,X1] : multiply(add(X0,X0),multiply(X0,add(X1,X0))) = multiply(X0,add(X1,X0)),
    inference(paramodulation,[status(thm)],[f58,f26]) ).

fof(f67,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(X1,add(X2,X0))) = add(multiply(X1,add(X0,X0)),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f58,f10]) ).

fof(f68,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(add(X1,X0),X2)) = add(add(X0,X0),multiply(X2,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f58,f10]) ).

fof(f71,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X2)),multiply(X0,add(X2,X2))) = add(multiply(X2,X0),multiply(X2,X0)),
    inference(forward_demodulation,[status(thm)],[f10,f61]) ).

fof(f72,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X2)),multiply(X0,add(X2,X2))) = multiply(X0,add(X2,X2)),
    inference(forward_demodulation,[status(thm)],[f10,f71]) ).

fof(f81,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X0)),add(X2,add(X0,X0))) = add(multiply(X2,multiply(X0,add(X1,X0))),multiply(X0,add(X1,X0))),
    inference(paramodulation,[status(thm)],[f64,f10]) ).

fof(f82,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X0)),add(add(X0,X0),X2)) = add(multiply(X0,add(X1,X0)),multiply(X2,multiply(X0,add(X1,X0)))),
    inference(paramodulation,[status(thm)],[f64,f10]) ).

fof(f125,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,multiply(X1,add(X2,X1))),add(multiply(X1,add(X2,X1)),multiply(X1,add(X2,X1)))) = add(multiply(add(multiply(X3,X1),X1),multiply(X1,add(X2,X1))),multiply(X1,add(X2,X1))),
    inference(paramodulation,[status(thm)],[f49,f34]) ).

fof(f128,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,add(X1,X0)),add(add(multiply(X2,X0),X0),X3)) = add(multiply(X0,add(X1,X0)),multiply(X3,multiply(X0,add(X1,X0)))),
    inference(paramodulation,[status(thm)],[f49,f10]) ).

fof(f131,plain,
    ! [X0,X1,X2] : add(multiply(X0,add(X1,X0)),multiply(X0,add(X1,X0))) = add(multiply(add(multiply(X2,X0),X0),multiply(X0,add(X1,X0))),multiply(X0,add(X1,X0))),
    inference(forward_demodulation,[status(thm)],[f58,f125]) ).

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

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

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

fof(f138,plain,
    ! [X0,X1] : add(X0,X0) = multiply(multiply(X0,add(X1,X0)),add(add(X0,X0),add(X0,X0))),
    inference(backward_demodulation,[status(thm)],[f139,f134]) ).

fof(f139,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,add(X1,X0)),add(add(multiply(X2,X0),X0),X3)) = multiply(multiply(X0,add(X1,X0)),add(add(X0,X0),X3)),
    inference(forward_demodulation,[status(thm)],[f82,f128]) ).

fof(f178,plain,
    ! [X0,X1,X2] : multiply(multiply(add(X0,X1),add(X2,X1)),add(X1,X1)) = multiply(add(X0,X1),add(X1,X1)),
    inference(paramodulation,[status(thm)],[f58,f72]) ).

fof(f200,plain,
    ! [X0,X1,X2] : multiply(multiply(add(X0,X1),add(X2,X1)),add(X1,X1)) = add(X1,X1),
    inference(forward_demodulation,[status(thm)],[f58,f178]) ).

fof(f238,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,add(X1,inverse(X2))),add(pixley(X1,X2,X0),X3)) = add(multiply(X0,add(X1,inverse(X2))),multiply(X3,multiply(X0,add(X1,inverse(X2))))),
    inference(paramodulation,[status(thm)],[f23,f24]) ).

fof(f242,plain,
    ! [X0,X1,X2] : pixley(add(X0,X1),X2,X1) = add(multiply(add(X0,X1),inverse(X2)),add(X1,multiply(inverse(X2),X1))),
    inference(paramodulation,[status(thm)],[f24,f23]) ).

fof(f245,plain,
    ! [X0] : add(X0,X0) = multiply(add(X0,multiply(X0,X0)),add(add(X0,X0),add(X0,X0))),
    inference(paramodulation,[status(thm)],[f24,f138]) ).

fof(f246,plain,
    ! [X0,X1,X2] : multiply(add(multiply(X0,X1),X1),add(X1,multiply(X1,X1))) = multiply(X1,add(add(X2,X1),X1)),
    inference(paramodulation,[status(thm)],[f24,f49]) ).

fof(f247,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X0,multiply(X0,X0))) = multiply(X0,add(add(X1,X0),X0)),
    inference(paramodulation,[status(thm)],[f24,f64]) ).

fof(f251,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(add(add(X0,X1),X2),add(X3,X1)),add(X1,multiply(X2,X1))) = multiply(X1,add(add(X0,X1),X2)),
    inference(paramodulation,[status(thm)],[f24,f26]) ).

fof(f252,plain,
    ! [X0,X1,X2,X3] : multiply(add(add(X0,X1),X2),add(X3,X1)) = add(multiply(X3,add(add(X0,X1),X2)),add(X1,multiply(X2,X1))),
    inference(paramodulation,[status(thm)],[f24,f10]) ).

fof(f253,plain,
    ! [X0,X1,X2,X3] : multiply(add(add(X0,X1),X2),add(X1,X3)) = add(add(X1,multiply(X2,X1)),multiply(X3,add(add(X0,X1),X2))),
    inference(paramodulation,[status(thm)],[f24,f10]) ).

fof(f259,plain,
    ! [X0,X1] : multiply(add(multiply(X0,X1),X1),add(X1,multiply(X1,X1))) = add(X1,multiply(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f24,f246]) ).

fof(f260,plain,
    ! [X0] : multiply(add(X0,X0),add(X0,multiply(X0,X0))) = add(X0,multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f24,f247]) ).

fof(f262,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(add(add(X0,X1),X2),add(X3,X1)),add(X1,multiply(X2,X1))) = add(X1,multiply(X2,X1)),
    inference(forward_demodulation,[status(thm)],[f24,f251]) ).

fof(f272,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(add(X0,add(X1,X2)),add(X3,X2)),add(multiply(X0,X2),X2)) = multiply(X2,add(X0,add(X1,X2))),
    inference(paramodulation,[status(thm)],[f25,f26]) ).

fof(f273,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,add(X1,X2)),add(X3,X2)) = add(multiply(X3,add(X0,add(X1,X2))),add(multiply(X0,X2),X2)),
    inference(paramodulation,[status(thm)],[f25,f10]) ).

fof(f274,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,add(X1,X2)),add(X2,X3)) = add(add(multiply(X0,X2),X2),multiply(X3,add(X0,add(X1,X2)))),
    inference(paramodulation,[status(thm)],[f25,f10]) ).

fof(f290,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(add(X0,add(X1,X2)),add(X3,X2)),add(multiply(X0,X2),X2)) = add(multiply(X0,X2),X2),
    inference(forward_demodulation,[status(thm)],[f25,f272]) ).

fof(f293,plain,
    ! [X0,X1] : pixley(X0,X0,X1) = add(multiply(X0,inverse(X0)),multiply(X1,n1)),
    inference(paramodulation,[status(thm)],[f11,f23]) ).

fof(f306,plain,
    ! [X0] : multiply(n1,inverse(X0)) = inverse(X0),
    inference(paramodulation,[status(thm)],[f11,f9]) ).

fof(f307,plain,
    ! [X0,X1] : X0 = add(multiply(X1,inverse(X1)),multiply(X0,n1)),
    inference(forward_demodulation,[status(thm)],[f13,f293]) ).

fof(f314,plain,
    ! [X0,X1] : pixley(n1,X0,X1) = add(inverse(X0),multiply(X1,add(n1,inverse(X0)))),
    inference(paramodulation,[status(thm)],[f306,f23]) ).

fof(f323,plain,
    ! [X0] : X0 = add(inverse(n1),multiply(X0,n1)),
    inference(paramodulation,[status(thm)],[f306,f307]) ).

fof(f334,plain,
    ! [X0] : multiply(X0,add(multiply(X0,n1),multiply(X0,n1))) = add(multiply(X0,n1),multiply(X0,n1)),
    inference(paramodulation,[status(thm)],[f307,f58]) ).

fof(f355,plain,
    ! [X0] : multiply(X0,multiply(n1,add(X0,X0))) = add(multiply(X0,n1),multiply(X0,n1)),
    inference(forward_demodulation,[status(thm)],[f10,f334]) ).

fof(f356,plain,
    ! [X0] : multiply(X0,multiply(n1,add(X0,X0))) = multiply(n1,add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f10,f355]) ).

fof(f387,plain,
    ! [X0,X1] : multiply(add(X0,multiply(X0,X0)),add(X1,add(X0,X0))) = add(multiply(X1,add(X0,multiply(X0,X0))),add(X0,multiply(X0,X0))),
    inference(paramodulation,[status(thm)],[f260,f10]) ).

fof(f388,plain,
    ! [X0,X1] : multiply(add(X0,multiply(X0,X0)),add(add(X0,X0),X1)) = add(add(X0,multiply(X0,X0)),multiply(X1,add(X0,multiply(X0,X0)))),
    inference(paramodulation,[status(thm)],[f260,f10]) ).

fof(f467,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),multiply(X0,add(X1,X1))) = multiply(add(multiply(X0,add(X1,X1)),multiply(X0,add(X1,X1))),add(add(multiply(X0,add(X1,X1)),multiply(X0,add(X1,X1))),add(multiply(X0,add(X1,X1)),multiply(X0,add(X1,X1))))),
    inference(paramodulation,[status(thm)],[f72,f245]) ).

fof(f470,plain,
    ! [X0,X1] : add(multiply(X0,X1),multiply(X0,X1)) = multiply(add(multiply(X0,X1),multiply(multiply(X0,X1),multiply(X0,X1))),add(multiply(X1,add(X0,X0)),add(multiply(X0,X1),multiply(X0,X1)))),
    inference(paramodulation,[status(thm)],[f10,f245]) ).

fof(f480,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X1)) = multiply(add(multiply(X1,add(X0,X0)),multiply(X1,add(X0,X0))),add(add(multiply(X1,add(X0,X0)),multiply(X1,add(X0,X0))),add(multiply(X1,add(X0,X0)),multiply(X1,add(X0,X0))))),
    inference(forward_demodulation,[status(thm)],[f10,f467]) ).

fof(f481,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X1)) = add(add(multiply(X1,add(X0,X0)),multiply(X1,add(X0,X0))),multiply(add(multiply(X1,add(X0,X0)),multiply(X1,add(X0,X0))),add(multiply(X1,add(X0,X0)),multiply(X1,add(X0,X0))))),
    inference(forward_demodulation,[status(thm)],[f68,f480]) ).

fof(f482,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X1)) = add(multiply(add(X0,X0),add(X1,X1)),multiply(add(multiply(X1,add(X0,X0)),multiply(X1,add(X0,X0))),add(multiply(X1,add(X0,X0)),multiply(X1,add(X0,X0))))),
    inference(forward_demodulation,[status(thm)],[f10,f481]) ).

fof(f483,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X1)) = add(multiply(add(X0,X0),add(X1,X1)),add(multiply(X1,add(X0,X0)),multiply(X1,add(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f58,f482]) ).

fof(f484,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X1)) = add(multiply(add(X0,X0),add(X1,X1)),multiply(add(X0,X0),add(X1,X1))),
    inference(forward_demodulation,[status(thm)],[f10,f483]) ).

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

fof(f488,plain,
    ! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(add(multiply(X1,X0),multiply(multiply(X1,X0),multiply(X1,X0))),add(multiply(X0,add(X1,X1)),add(multiply(X1,X0),multiply(X1,X0)))),
    inference(forward_demodulation,[status(thm)],[f10,f470]) ).

fof(f489,plain,
    ! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(add(multiply(X1,X0),multiply(multiply(X1,X0),multiply(X1,X0))),add(multiply(X0,add(X1,X1)),multiply(X0,add(X1,X1)))),
    inference(forward_demodulation,[status(thm)],[f10,f488]) ).

fof(f490,plain,
    ! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(add(multiply(X1,X0),multiply(multiply(X1,X0),multiply(X1,X0))),multiply(add(X1,X1),add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f10,f489]) ).

fof(f633,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,multiply(X1,X1))),add(add(X1,multiply(X1,X1)),add(X1,multiply(X1,X1)))) = add(multiply(add(multiply(X2,X1),X1),add(X1,multiply(X1,X1))),add(X1,multiply(X1,X1))),
    inference(paramodulation,[status(thm)],[f259,f34]) ).

fof(f636,plain,
    ! [X0,X1,X2] : multiply(add(X0,multiply(X0,X0)),add(add(multiply(X1,X0),X0),X2)) = add(add(X0,multiply(X0,X0)),multiply(X2,add(X0,multiply(X0,X0)))),
    inference(paramodulation,[status(thm)],[f259,f10]) ).

fof(f653,plain,
    ! [X0,X1] : add(add(X0,multiply(X0,X0)),add(X0,multiply(X0,X0))) = add(multiply(add(multiply(X1,X0),X0),add(X0,multiply(X0,X0))),add(X0,multiply(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f58,f633]) ).

fof(f654,plain,
    ! [X0,X1] : add(add(X0,multiply(X0,X0)),add(X0,multiply(X0,X0))) = multiply(add(X0,multiply(X0,X0)),add(add(multiply(X1,X0),X0),add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f387,f653]) ).

fof(f658,plain,
    ! [X0] : add(add(X0,multiply(X0,X0)),add(X0,multiply(X0,X0))) = multiply(add(X0,multiply(X0,X0)),add(add(X0,X0),add(X0,X0))),
    inference(backward_demodulation,[status(thm)],[f659,f654]) ).

fof(f659,plain,
    ! [X0,X1,X2] : multiply(add(X0,multiply(X0,X0)),add(add(multiply(X1,X0),X0),X2)) = multiply(add(X0,multiply(X0,X0)),add(add(X0,X0),X2)),
    inference(forward_demodulation,[status(thm)],[f388,f636]) ).

fof(f660,plain,
    ! [X0] : add(add(X0,multiply(X0,X0)),add(X0,multiply(X0,X0))) = add(X0,X0),
    inference(forward_demodulation,[status(thm)],[f245,f658]) ).

fof(f669,plain,
    ! [X0] : multiply(multiply(X0,X0),add(X0,X0)) = add(multiply(X0,X0),multiply(add(X0,multiply(X0,X0)),multiply(X0,X0))),
    inference(paramodulation,[status(thm)],[f660,f24]) ).

fof(f721,plain,
    ! [X0] : multiply(multiply(X0,X0),add(X0,X0)) = add(multiply(X0,X0),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f9,f669]) ).

fof(f723,plain,
    ! [X0] : multiply(multiply(X0,X0),add(X0,X0)) = multiply(X0,add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f10,f721]) ).

fof(f809,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,multiply(X0,X0))) = add(multiply(X1,add(X0,X0)),multiply(X0,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f723,f10]) ).

fof(f810,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(multiply(X0,X0),X1)) = add(multiply(X0,add(X0,X0)),multiply(X1,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f723,f10]) ).

fof(f820,plain,
    ! [X0] : multiply(add(X0,X0),add(X0,X0)) = add(X0,multiply(X0,X0)),
    inference(backward_demodulation,[status(thm)],[f822,f260]) ).

fof(f822,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,multiply(X0,X0))) = multiply(add(X0,X0),add(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f10,f809]) ).

fof(f823,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(multiply(X0,X0),X1)) = multiply(add(X0,X0),add(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f10,f810]) ).

fof(f824,plain,
    ! [X0] : add(add(X0,multiply(X0,X0)),add(X0,X0)) = add(X0,X0),
    inference(backward_demodulation,[status(thm)],[f857,f660]) ).

fof(f829,plain,
    ! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(add(multiply(X1,X0),multiply(X1,X0)),multiply(add(X1,X1),add(X0,X0))),
    inference(backward_demodulation,[status(thm)],[f857,f490]) ).

fof(f857,plain,
    ! [X0] : add(X0,X0) = add(X0,multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f58,f820]) ).

fof(f858,plain,
    ! [X0,X1] : add(X0,X0) = multiply(multiply(X0,add(X1,X0)),add(X0,X0)),
    inference(backward_demodulation,[status(thm)],[f867,f138]) ).

fof(f863,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X1)) = multiply(add(X1,X1),add(X0,X0)),
    inference(backward_demodulation,[status(thm)],[f867,f485]) ).

fof(f867,plain,
    ! [X0] : add(add(X0,X0),add(X0,X0)) = add(X0,X0),
    inference(forward_demodulation,[status(thm)],[f857,f824]) ).

fof(f872,plain,
    ! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(multiply(X0,add(X1,X1)),multiply(add(X1,X1),add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f10,f829]) ).

fof(f927,plain,
    ! [X0] : multiply(add(X0,X0),add(multiply(X0,X0),multiply(X0,X0))) = add(multiply(X0,X0),multiply(X0,X0)),
    inference(paramodulation,[status(thm)],[f857,f58]) ).

fof(f928,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(multiply(X1,multiply(X0,X0)),multiply(X0,X0))) = add(multiply(X1,multiply(X0,X0)),multiply(X0,X0)),
    inference(paramodulation,[status(thm)],[f857,f34]) ).

fof(f929,plain,
    ! [X0,X1] : multiply(multiply(X0,add(X1,X1)),multiply(multiply(X1,X1),X0)) = multiply(multiply(X1,X1),X0),
    inference(paramodulation,[status(thm)],[f857,f26]) ).

fof(f961,plain,
    ! [X0] : multiply(add(X0,X0),add(X0,multiply(X0,X0))) = add(multiply(X0,X0),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f823,f927]) ).

fof(f962,plain,
    ! [X0] : multiply(add(X0,X0),add(X0,X0)) = add(multiply(X0,X0),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f822,f961]) ).

fof(f963,plain,
    ! [X0] : add(X0,X0) = add(multiply(X0,X0),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f58,f962]) ).

fof(f970,plain,
    ! [X0] : add(X0,X0) = multiply(X0,add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f10,f963]) ).

fof(f971,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(multiply(X1,multiply(X0,X0)),X0)) = add(multiply(X1,multiply(X0,X0)),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f822,f928]) ).

fof(f977,plain,
    ! [X0,X1] : add(multiply(X0,X1),multiply(X0,X1)) = multiply(multiply(X0,X1),multiply(X1,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f10,f970]) ).

fof(f990,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X0)) = add(multiply(X1,add(X0,X0)),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f970,f10]) ).

fof(f991,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X0,X1)) = add(add(X0,X0),multiply(X1,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f970,f10]) ).

fof(f992,plain,
    ! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(add(X1,X1),add(X0,X0)),
    inference(backward_demodulation,[status(thm)],[f994,f872]) ).

fof(f994,plain,
    ! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(multiply(X1,X0),multiply(X0,add(X1,X1))),
    inference(forward_demodulation,[status(thm)],[f10,f977]) ).

fof(f1013,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(X1,add(X2,X0))) = multiply(add(X0,X0),add(X1,X0)),
    inference(backward_demodulation,[status(thm)],[f990,f67]) ).

fof(f1018,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(add(X1,X0),X2)) = multiply(add(X0,X0),add(X0,X2)),
    inference(backward_demodulation,[status(thm)],[f991,f68]) ).

fof(f1021,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X1)) = multiply(X0,add(X1,X1)),
    inference(backward_demodulation,[status(thm)],[f992,f863]) ).

fof(f1041,plain,
    ! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(X1,add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f992,f1021]) ).

fof(f1133,plain,
    ! [X0,X1] : multiply(add(X0,X0),multiply(add(X0,X0),add(X1,add(X0,X0)))) = multiply(add(X0,X0),add(X1,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f867,f64]) ).

fof(f1136,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(multiply(X1,add(X0,X0)),add(X0,X0))) = add(multiply(X1,add(X0,X0)),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f867,f34]) ).

fof(f1137,plain,
    ! [X0,X1] : multiply(multiply(X0,add(X1,X1)),multiply(add(X1,X1),X0)) = multiply(add(X1,X1),X0),
    inference(paramodulation,[status(thm)],[f867,f26]) ).

fof(f1173,plain,
    ! [X0,X1] : multiply(add(X0,X0),multiply(add(X0,X0),add(X1,X0))) = multiply(add(X0,X0),add(X1,add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f1013,f1133]) ).

fof(f1174,plain,
    ! [X0,X1] : multiply(add(X0,X0),multiply(add(X0,X0),add(X1,X0))) = multiply(add(X0,X0),add(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f1013,f1173]) ).

fof(f1176,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(multiply(X1,add(X0,X0)),X0)) = add(multiply(X1,add(X0,X0)),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f1013,f1136]) ).

fof(f1177,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(multiply(X1,add(X0,X0)),X0)) = multiply(add(X0,X0),add(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f990,f1176]) ).

fof(f1187,plain,
    ! [X0] : add(multiply(X0,X0),multiply(X0,X0)) = multiply(multiply(multiply(X0,X0),add(X0,X0)),add(multiply(X0,X0),multiply(X0,X0))),
    inference(paramodulation,[status(thm)],[f857,f858]) ).

fof(f1214,plain,
    ! [X0] : multiply(X0,add(X0,X0)) = multiply(multiply(multiply(X0,X0),add(X0,X0)),add(multiply(X0,X0),multiply(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f10,f1187]) ).

fof(f1215,plain,
    ! [X0] : add(X0,X0) = multiply(multiply(multiply(X0,X0),add(X0,X0)),add(multiply(X0,X0),multiply(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f970,f1214]) ).

fof(f1216,plain,
    ! [X0] : add(X0,X0) = multiply(multiply(multiply(X0,X0),add(X0,X0)),multiply(X0,add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f10,f1215]) ).

fof(f1217,plain,
    ! [X0] : add(X0,X0) = multiply(multiply(multiply(X0,X0),add(X0,X0)),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f970,f1216]) ).

fof(f1268,plain,
    ! [X0,X1] : multiply(add(X0,add(X1,X1)),add(add(X1,X1),add(X1,X1))) = add(multiply(multiply(multiply(X1,X1),add(X1,X1)),add(X1,X1)),add(X1,X1)),
    inference(paramodulation,[status(thm)],[f1217,f34]) ).

fof(f1292,plain,
    ! [X0] : add(add(X0,X0),add(X0,X0)) = add(multiply(multiply(multiply(X0,X0),add(X0,X0)),add(X0,X0)),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f58,f1268]) ).

fof(f1293,plain,
    ! [X0] : add(X0,X0) = add(multiply(multiply(multiply(X0,X0),add(X0,X0)),add(X0,X0)),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f867,f1292]) ).

fof(f1294,plain,
    ! [X0] : add(X0,X0) = multiply(add(X0,X0),add(multiply(multiply(X0,X0),add(X0,X0)),X0)),
    inference(forward_demodulation,[status(thm)],[f990,f1293]) ).

fof(f1295,plain,
    ! [X0] : add(X0,X0) = multiply(add(X0,X0),add(multiply(X0,X0),X0)),
    inference(forward_demodulation,[status(thm)],[f1177,f1294]) ).

fof(f1296,plain,
    ! [X0] : add(X0,X0) = add(multiply(X0,X0),X0),
    inference(forward_demodulation,[status(thm)],[f34,f1295]) ).

fof(f1346,plain,
    ! [X0,X1,X2] : multiply(X0,add(multiply(X1,X2),multiply(X1,X2))) = multiply(multiply(X2,add(X1,X1)),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f10,f992]) ).

fof(f1348,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),add(X2,X2)) = multiply(add(X2,X2),multiply(X1,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f10,f992]) ).

fof(f1389,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(multiply(X1,add(X2,X2)),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f10,f1346]) ).

fof(f1555,plain,
    ! [X0,X1] : multiply(X0,multiply(X1,add(X0,inverse(X1)))) = multiply(X1,add(X0,inverse(X1))),
    inference(paramodulation,[status(thm)],[f14,f42]) ).

fof(f1842,plain,
    ! [X0] : multiply(multiply(X0,X0),add(X0,X0)) = multiply(add(X0,X0),add(multiply(X0,X0),X0)),
    inference(paramodulation,[status(thm)],[f992,f822]) ).

fof(f1850,plain,
    ! [X0,X1] : multiply(add(X0,X0),multiply(X0,add(X1,X0))) = multiply(add(X0,X0),add(multiply(X1,X0),X0)),
    inference(paramodulation,[status(thm)],[f10,f822]) ).

fof(f1867,plain,
    ! [X0] : multiply(multiply(X0,X0),add(X0,X0)) = add(multiply(X0,X0),X0),
    inference(forward_demodulation,[status(thm)],[f34,f1842]) ).

fof(f1877,plain,
    ! [X0] : multiply(multiply(X0,X0),add(X0,X0)) = add(X0,X0),
    inference(forward_demodulation,[status(thm)],[f1296,f1867]) ).

fof(f1893,plain,
    ! [X0,X1] : multiply(X0,add(X1,X0)) = multiply(add(X0,X0),add(multiply(X1,X0),X0)),
    inference(forward_demodulation,[status(thm)],[f64,f1850]) ).

fof(f1920,plain,
    ! [X0,X1] : multiply(X0,add(X1,X0)) = add(multiply(X1,X0),X0),
    inference(forward_demodulation,[status(thm)],[f34,f1893]) ).

fof(f2038,plain,
    ! [X0] : multiply(multiply(X0,X0),add(X0,X0)) = add(multiply(X0,multiply(X0,X0)),multiply(X0,X0)),
    inference(paramodulation,[status(thm)],[f857,f1920]) ).

fof(f2048,plain,
    ! [X0,X1] : multiply(add(multiply(X0,X1),X1),multiply(X1,X1)) = multiply(X1,X1),
    inference(paramodulation,[status(thm)],[f1920,f26]) ).

fof(f2051,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(X2,X1)) = add(multiply(X2,add(X0,X1)),add(multiply(X0,X1),X1)),
    inference(paramodulation,[status(thm)],[f1920,f10]) ).

fof(f2052,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(X1,X2)) = add(add(multiply(X0,X1),X1),multiply(X2,add(X0,X1))),
    inference(paramodulation,[status(thm)],[f1920,f10]) ).

fof(f2074,plain,
    ! [X0] : add(X0,X0) = add(multiply(X0,multiply(X0,X0)),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f1877,f2038]) ).

fof(f2209,plain,
    ! [X0,X1] : multiply(add(X0,multiply(X1,X1)),add(X1,X1)) = add(multiply(X1,multiply(X1,X1)),multiply(X1,X1)),
    inference(paramodulation,[status(thm)],[f2074,f34]) ).

fof(f2258,plain,
    ! [X0,X1] : multiply(add(X0,multiply(X1,X1)),add(X1,X1)) = add(X1,X1),
    inference(forward_demodulation,[status(thm)],[f2074,f2209]) ).

fof(f2334,plain,
    ! [X0,X1] : multiply(add(X0,X0),multiply(add(X1,multiply(X0,X0)),add(X0,X0))) = multiply(add(X1,multiply(X0,X0)),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f2258,f72]) ).

fof(f2361,plain,
    ! [X0,X1] : multiply(multiply(X0,add(X1,multiply(X0,X0))),add(X0,X0)) = multiply(add(X1,multiply(X0,X0)),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f1348,f2334]) ).

fof(f2362,plain,
    ! [X0,X1] : multiply(multiply(X0,add(X1,multiply(X0,X0))),add(X0,X0)) = add(X0,X0),
    inference(forward_demodulation,[status(thm)],[f2258,f2361]) ).

fof(f2474,plain,
    ! [X0] : multiply(add(X0,multiply(multiply(X0,X0),X0)),add(X0,X0)) = add(X0,X0),
    inference(paramodulation,[status(thm)],[f24,f2362]) ).

fof(f2752,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,X1),multiply(add(X2,X0),add(X3,X1))) = add(multiply(multiply(X3,add(X2,X0)),multiply(X0,X1)),multiply(X0,X1)),
    inference(paramodulation,[status(thm)],[f10,f31]) ).

fof(f2755,plain,
    ! [X0,X1] : multiply(multiply(X0,add(X1,X0)),add(add(X1,X0),add(X1,X0))) = add(multiply(add(X1,X0),multiply(X0,add(X1,X0))),multiply(X0,add(X1,X0))),
    inference(paramodulation,[status(thm)],[f857,f31]) ).

fof(f2892,plain,
    ! [X0,X1] : multiply(add(multiply(X0,X1),X1),add(add(X0,X1),add(X0,X1))) = add(multiply(add(X0,X1),multiply(X1,add(X0,X1))),multiply(X1,add(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f1920,f2755]) ).

fof(f2893,plain,
    ! [X0,X1] : multiply(add(multiply(X0,X1),X1),add(add(X0,X1),add(X0,X1))) = add(multiply(add(X0,X1),add(multiply(X0,X1),X1)),multiply(X1,add(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f1920,f2892]) ).

fof(f2894,plain,
    ! [X0,X1] : multiply(add(multiply(X0,X1),X1),add(add(X0,X1),add(X0,X1))) = add(add(multiply(X0,X1),X1),multiply(X1,add(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f34,f2893]) ).

fof(f2895,plain,
    ! [X0,X1] : multiply(add(multiply(X0,X1),X1),add(add(X0,X1),add(X0,X1))) = multiply(add(X0,X1),add(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f2052,f2894]) ).

fof(f2898,plain,
    ! [X0,X1] : multiply(add(multiply(X0,X1),X1),add(add(X0,X1),add(X0,X1))) = add(X1,X1),
    inference(forward_demodulation,[status(thm)],[f58,f2895]) ).

fof(f2951,plain,
    ! [X0,X1,X2,X3] : add(multiply(multiply(X0,add(X1,X2)),multiply(X2,X0)),multiply(X2,X0)) = add(multiply(X2,X0),multiply(multiply(X0,add(X3,X2)),multiply(X2,X0))),
    inference(paramodulation,[status(thm)],[f31,f32]) ).

fof(f2984,plain,
    ! [X0,X1] : multiply(multiply(X0,add(X1,X0)),add(add(X1,X0),add(X1,X0))) = add(multiply(X0,add(X1,X0)),multiply(add(X1,X0),multiply(X0,add(X1,X0)))),
    inference(paramodulation,[status(thm)],[f1296,f32]) ).

fof(f2987,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),n1) = add(multiply(X0,X1),multiply(inverse(multiply(X1,add(X2,X0))),multiply(X0,X1))),
    inference(paramodulation,[status(thm)],[f11,f32]) ).

fof(f3039,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,X1),multiply(add(X2,X0),add(X1,X1))) = add(multiply(X0,X1),multiply(multiply(X1,add(X3,X0)),multiply(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f2752,f2951]) ).

fof(f3040,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(add(X2,X0),add(X1,X1))) = add(multiply(X0,X1),multiply(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f26,f3039]) ).

fof(f3042,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(add(X2,X0),add(X1,X1))) = multiply(X1,add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f10,f3040]) ).

fof(f3134,plain,
    ! [X0,X1] : multiply(add(multiply(X0,X1),X1),add(add(X0,X1),add(X0,X1))) = add(multiply(X1,add(X0,X1)),multiply(add(X0,X1),multiply(X1,add(X0,X1)))),
    inference(forward_demodulation,[status(thm)],[f1920,f2984]) ).

fof(f3135,plain,
    ! [X0,X1] : add(X0,X0) = add(multiply(X0,add(X1,X0)),multiply(add(X1,X0),multiply(X0,add(X1,X0)))),
    inference(forward_demodulation,[status(thm)],[f2898,f3134]) ).

fof(f3136,plain,
    ! [X0,X1] : add(X0,X0) = add(add(multiply(X1,X0),X0),multiply(add(X1,X0),multiply(X0,add(X1,X0)))),
    inference(forward_demodulation,[status(thm)],[f1920,f3135]) ).

fof(f3137,plain,
    ! [X0,X1] : add(X0,X0) = add(add(multiply(X1,X0),X0),multiply(add(X1,X0),add(multiply(X1,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1920,f3136]) ).

fof(f3138,plain,
    ! [X0,X1] : add(X0,X0) = add(add(multiply(X1,X0),X0),add(multiply(X1,X0),X0)),
    inference(forward_demodulation,[status(thm)],[f34,f3137]) ).

fof(f3405,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(X2,X2)) = multiply(add(multiply(X0,X2),X2),multiply(add(X0,add(X1,X2)),add(X2,X2))),
    inference(paramodulation,[status(thm)],[f25,f994]) ).

fof(f3437,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X1)),add(X2,multiply(X1,X0))) = add(multiply(X2,multiply(X0,add(X1,X1))),multiply(X0,add(X1,X1))),
    inference(paramodulation,[status(thm)],[f994,f10]) ).

fof(f3678,plain,
    ! [X0,X1,X2] : multiply(add(multiply(X0,X0),X1),add(X2,add(X0,X0))) = add(multiply(X2,add(multiply(X0,X0),X1)),multiply(add(X0,X0),add(X0,X1))),
    inference(paramodulation,[status(thm)],[f823,f10]) ).

fof(f4160,plain,
    ! [X0] : multiply(add(multiply(X0,X0),X0),multiply(multiply(X0,X0),X0)) = multiply(multiply(X0,X0),X0),
    inference(paramodulation,[status(thm)],[f1920,f929]) ).

fof(f4218,plain,
    ! [X0] : multiply(add(X0,X0),multiply(multiply(X0,X0),X0)) = multiply(multiply(X0,X0),X0),
    inference(forward_demodulation,[status(thm)],[f1296,f4160]) ).

fof(f4336,plain,
    ! [X0,X1] : multiply(multiply(multiply(X0,X0),X0),add(X1,add(X0,X0))) = add(multiply(X1,multiply(multiply(X0,X0),X0)),multiply(multiply(X0,X0),X0)),
    inference(paramodulation,[status(thm)],[f4218,f10]) ).

fof(f4646,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,add(X1,X2)),add(X3,add(X2,X2))) = add(multiply(X3,add(X0,add(X1,X2))),multiply(add(X2,X2),add(X0,X2))),
    inference(paramodulation,[status(thm)],[f1013,f10]) ).

fof(f4647,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,add(X1,X2)),add(add(X2,X2),X3)) = add(multiply(add(X2,X2),add(X0,X2)),multiply(X3,add(X0,add(X1,X2)))),
    inference(paramodulation,[status(thm)],[f1013,f10]) ).

fof(f4829,plain,
    ! [X0,X1] : multiply(add(X0,X0),multiply(add(X0,X0),add(X0,X1))) = multiply(add(X0,X0),add(X0,multiply(X1,add(X0,X0)))),
    inference(paramodulation,[status(thm)],[f991,f1018]) ).

fof(f4858,plain,
    ! [X0,X1,X2] : multiply(pixley(add(X0,X1),X2,add(X1,X1)),multiply(add(X1,X1),add(X1,inverse(X2)))) = multiply(add(X1,X1),add(add(X0,X1),inverse(X2))),
    inference(paramodulation,[status(thm)],[f1018,f42]) ).

fof(f5006,plain,
    ! [X0,X1,X2] : multiply(pixley(add(X0,X1),X2,add(X1,X1)),multiply(add(X1,X1),add(X1,inverse(X2)))) = multiply(add(X1,X1),add(X1,inverse(X2))),
    inference(forward_demodulation,[status(thm)],[f1018,f4858]) ).

fof(f5064,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(multiply(add(X1,X0),add(X2,X0)),X0)) = add(add(X0,X0),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f200,f990]) ).

fof(f5078,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(add(X1,X1),X0)) = add(multiply(X0,add(X1,X1)),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f992,f990]) ).

fof(f5081,plain,
    ! [X0,X1] : multiply(add(add(X0,X1),add(X0,X1)),add(X1,add(X0,X1))) = add(add(X1,multiply(add(X0,X1),X1)),add(add(X0,X1),add(X0,X1))),
    inference(paramodulation,[status(thm)],[f24,f990]) ).

fof(f5098,plain,
    ! [X0,X1] : multiply(X0,multiply(add(X0,X0),add(X1,X0))) = add(multiply(multiply(X1,add(X0,X0)),X0),X0),
    inference(paramodulation,[status(thm)],[f990,f25]) ).

fof(f5133,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(multiply(add(X1,X0),add(X2,X0)),X0)) = add(X0,X0),
    inference(forward_demodulation,[status(thm)],[f867,f5064]) ).

fof(f5221,plain,
    ! [X0,X1] : multiply(add(add(X0,X1),add(X0,X1)),add(X1,add(X0,X1))) = add(add(X1,X1),add(add(X0,X1),add(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f9,f5081]) ).

fof(f5320,plain,
    ! [X0] : multiply(add(X0,X0),multiply(add(X0,X0),add(X0,multiply(multiply(X0,X0),X0)))) = multiply(add(X0,X0),add(X0,multiply(multiply(X0,X0),X0))),
    inference(paramodulation,[status(thm)],[f2474,f1137]) ).

fof(f5326,plain,
    ! [X0,X1] : multiply(multiply(X0,add(X1,X1)),multiply(add(X0,X0),add(X1,X1))) = multiply(add(X0,X0),add(X1,X1)),
    inference(paramodulation,[status(thm)],[f992,f1137]) ).

fof(f5395,plain,
    ! [X0] : multiply(add(X0,X0),add(X0,multiply(multiply(multiply(X0,X0),X0),add(X0,X0)))) = multiply(add(X0,X0),add(X0,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f4829,f5320]) ).

fof(f5404,plain,
    ! [X0,X1] : multiply(multiply(X0,add(X1,X1)),multiply(X1,add(X0,X0))) = multiply(add(X0,X0),add(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f992,f5326]) ).

fof(f5405,plain,
    ! [X0,X1] : multiply(multiply(X0,add(X1,X1)),multiply(X1,add(X0,X0))) = multiply(X1,add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f992,f5404]) ).

fof(f5995,plain,
    ! [X0,X1] : pixley(add(multiply(X0,multiply(X0,X0)),multiply(X0,X0)),X1,multiply(X0,X0)) = add(multiply(add(X0,X0),inverse(X1)),add(multiply(X0,X0),multiply(inverse(X1),multiply(X0,X0)))),
    inference(paramodulation,[status(thm)],[f2074,f242]) ).

fof(f6051,plain,
    ! [X0,X1] : pixley(add(X0,X0),X1,multiply(X0,X0)) = add(multiply(add(X0,X0),inverse(X1)),add(multiply(X0,X0),multiply(inverse(X1),multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f2074,f5995]) ).

fof(f6091,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,X1),add(multiply(X2,X3),multiply(X2,X3))) = multiply(multiply(X3,add(X2,X2)),multiply(X1,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f10,f1348]) ).

fof(f6109,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X1)),add(X2,X2)) = multiply(add(X2,X2),multiply(X0,add(X1,X1))),
    inference(paramodulation,[status(thm)],[f992,f1348]) ).

fof(f6110,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X0)),add(X2,X2)) = multiply(add(X2,X2),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f58,f1348]) ).

fof(f6114,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),add(X1,X1)) = multiply(add(X1,X1),add(multiply(X0,X0),X0)),
    inference(paramodulation,[status(thm)],[f1920,f1348]) ).

fof(f6115,plain,
    ! [X0,X1,X2] : multiply(multiply(add(X0,X0),X1),add(X2,X2)) = multiply(add(X2,X2),multiply(X1,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f867,f1348]) ).

fof(f6157,plain,
    ! [X0,X1] : multiply(multiply(X0,X1),multiply(X0,add(X1,X1))) = multiply(X1,add(X0,X0)),
    inference(backward_demodulation,[status(thm)],[f6158,f5405]) ).

fof(f6158,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,X1),multiply(X2,add(X3,X3))) = multiply(multiply(X2,add(X3,X3)),multiply(X1,add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f10,f6091]) ).

fof(f6211,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(add(X0,X0),multiply(X1,add(X2,X2))),
    inference(forward_demodulation,[status(thm)],[f1389,f6109]) ).

fof(f6222,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(multiply(X2,X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f1348,f6211]) ).

fof(f6223,plain,
    ! [X0,X1,X2] : multiply(add(multiply(X0,X1),X1),add(X2,X2)) = multiply(add(X2,X2),add(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f1920,f6110]) ).

fof(f6226,plain,
    ! [X0,X1,X2] : multiply(add(multiply(X0,X1),X1),add(X2,X2)) = multiply(X1,add(X2,X2)),
    inference(forward_demodulation,[status(thm)],[f992,f6223]) ).

fof(f6233,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),add(X1,X1)) = multiply(add(X1,X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f1296,f6114]) ).

fof(f6237,plain,
    ! [X0,X1] : multiply(multiply(X0,X0),add(X1,X1)) = multiply(X0,add(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f992,f6233]) ).

fof(f6249,plain,
    ! [X0,X1,X2] : multiply(multiply(add(X0,X0),X1),add(X2,X2)) = multiply(multiply(X0,X1),add(X2,X2)),
    inference(forward_demodulation,[status(thm)],[f1348,f6115]) ).

fof(f6385,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X0),multiply(X1,add(X2,X2))) = multiply(X0,add(multiply(X2,X1),multiply(X2,X1))),
    inference(paramodulation,[status(thm)],[f10,f6237]) ).

fof(f6405,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,multiply(X1,X1)),add(X2,X2)) = multiply(add(X2,X2),multiply(X1,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f6237,f1348]) ).

fof(f6417,plain,
    ! [X0,X1] : multiply(multiply(X0,add(X1,X1)),multiply(X1,multiply(X0,X0))) = multiply(X1,multiply(X0,X0)),
    inference(paramodulation,[status(thm)],[f6237,f26]) ).

fof(f6425,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(X1,multiply(X2,X2))) = add(multiply(X1,add(X0,X0)),multiply(X2,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f6237,f10]) ).

fof(f6426,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(multiply(X1,X1),X2)) = add(multiply(X1,add(X0,X0)),multiply(X2,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f6237,f10]) ).

fof(f6465,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X0),multiply(X1,add(X2,X2))) = multiply(X0,multiply(X1,add(X2,X2))),
    inference(forward_demodulation,[status(thm)],[f10,f6385]) ).

fof(f6536,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,multiply(X1,X1)),add(X2,X2)) = multiply(multiply(X0,X1),add(X2,X2)),
    inference(forward_demodulation,[status(thm)],[f1348,f6405]) ).

fof(f6571,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(X1,multiply(X2,X2))) = multiply(add(X0,X0),add(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f10,f6425]) ).

fof(f6574,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(multiply(X1,X1),X2)) = multiply(add(X0,X0),add(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f10,f6426]) ).

fof(f6655,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X1)),add(X2,multiply(X0,X1))) = add(multiply(X2,multiply(X0,add(X1,X1))),multiply(X1,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f6157,f10]) ).

fof(f6656,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X1)),add(multiply(X0,X1),X2)) = add(multiply(X1,add(X0,X0)),multiply(X2,multiply(X0,add(X1,X1)))),
    inference(paramodulation,[status(thm)],[f6157,f10]) ).

fof(f7238,plain,
    ! [X0,X1,X2,X3] : multiply(add(multiply(multiply(X0,X1),X2),multiply(multiply(X0,X1),X2)),add(X3,X3)) = multiply(multiply(multiply(X0,X1),X2),add(X3,X3)),
    inference(paramodulation,[status(thm)],[f28,f6226]) ).

fof(f7240,plain,
    ! [X0,X1,X2] : multiply(add(multiply(multiply(X0,X0),X1),multiply(multiply(X0,X0),X1)),add(X2,X2)) = multiply(multiply(multiply(X0,X0),X1),add(X2,X2)),
    inference(paramodulation,[status(thm)],[f929,f6226]) ).

fof(f7267,plain,
    ! [X0,X1,X2,X3] : multiply(add(multiply(X0,X1),X1),multiply(X2,add(X3,X3))) = multiply(X1,add(multiply(X3,X2),multiply(X3,X2))),
    inference(paramodulation,[status(thm)],[f10,f6226]) ).

fof(f7304,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(X1,add(multiply(X2,X3),X3))) = add(multiply(X1,add(X0,X0)),multiply(X3,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f6226,f10]) ).

fof(f7305,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(add(multiply(X1,X2),X2),X3)) = add(multiply(X2,add(X0,X0)),multiply(X3,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f6226,f10]) ).

fof(f7349,plain,
    ! [X0,X1,X2,X3] : multiply(X0,add(multiply(multiply(X1,X2),X3),multiply(multiply(X1,X2),X3))) = multiply(multiply(multiply(X1,X2),X3),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f992,f7238]) ).

fof(f7350,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(X1,add(multiply(X2,X3),multiply(X2,X3)))) = multiply(multiply(multiply(X2,X3),X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f10,f7349]) ).

fof(f7360,plain,
    ! [X0] : multiply(add(X0,X0),add(X0,multiply(X0,multiply(X0,multiply(X0,add(X0,X0)))))) = multiply(add(X0,X0),add(X0,multiply(multiply(X0,X0),X0))),
    inference(backward_demodulation,[status(thm)],[f7362,f5395]) ).

fof(f7362,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(X1,multiply(X2,add(X3,X3)))) = multiply(multiply(multiply(X3,X2),X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f10,f7350]) ).

fof(f7367,plain,
    ! [X0,X1,X2] : multiply(X0,add(multiply(multiply(X1,X1),X2),multiply(multiply(X1,X1),X2))) = multiply(multiply(multiply(X1,X1),X2),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f992,f7240]) ).

fof(f7368,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(multiply(X2,X2),multiply(X2,X2)))) = multiply(multiply(multiply(X2,X2),X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f10,f7367]) ).

fof(f7369,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,multiply(X2,add(X2,X2)))) = multiply(multiply(multiply(X2,X2),X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f10,f7368]) ).

fof(f7370,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(multiply(X2,X2),X2))) = multiply(multiply(multiply(X2,X2),X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f1920,f7369]) ).

fof(f7371,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(multiply(multiply(X2,X2),X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f1296,f7370]) ).

fof(f7424,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(X2,X2)) = multiply(X2,multiply(add(X0,add(X1,X2)),add(X2,X2))),
    inference(backward_demodulation,[status(thm)],[f7425,f3405]) ).

fof(f7425,plain,
    ! [X0,X1,X2,X3] : multiply(add(multiply(X0,X1),X1),multiply(X2,add(X3,X3))) = multiply(X1,multiply(X2,add(X3,X3))),
    inference(forward_demodulation,[status(thm)],[f10,f7267]) ).

fof(f7493,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(X1,add(multiply(X2,X3),X3))) = multiply(add(X0,X0),add(X1,X3)),
    inference(forward_demodulation,[status(thm)],[f10,f7304]) ).

fof(f7495,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(add(multiply(X1,X2),X2),X3)) = multiply(add(X0,X0),add(X2,X3)),
    inference(forward_demodulation,[status(thm)],[f10,f7305]) ).

fof(f7525,plain,
    ! [X0] : multiply(add(X0,X0),add(X0,multiply(X0,multiply(X0,add(multiply(X0,X0),X0))))) = multiply(add(X0,X0),add(X0,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1920,f7360]) ).

fof(f7526,plain,
    ! [X0] : multiply(add(X0,X0),add(X0,multiply(X0,add(multiply(multiply(X0,X0),X0),X0)))) = multiply(add(X0,X0),add(X0,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1920,f7525]) ).

fof(f7527,plain,
    ! [X0] : multiply(add(X0,X0),add(X0,add(multiply(multiply(multiply(X0,X0),X0),X0),X0))) = multiply(add(X0,X0),add(X0,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1920,f7526]) ).

fof(f7528,plain,
    ! [X0] : multiply(add(X0,X0),add(X0,X0)) = multiply(add(X0,X0),add(X0,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1013,f7527]) ).

fof(f7529,plain,
    ! [X0] : multiply(X0,add(X0,X0)) = multiply(add(X0,X0),add(X0,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f992,f7528]) ).

fof(f7530,plain,
    ! [X0] : add(multiply(X0,X0),X0) = multiply(add(X0,X0),add(X0,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1920,f7529]) ).

fof(f7531,plain,
    ! [X0] : add(X0,X0) = multiply(add(X0,X0),add(X0,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1296,f7530]) ).

fof(f8037,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(multiply(X1,add(X2,X2)),add(X3,X3))) = multiply(multiply(X3,multiply(X1,add(X2,X2))),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f1389,f1389]) ).

fof(f8083,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(multiply(X1,add(X2,X2)),X0)) = add(multiply(X0,multiply(X1,add(X2,X2))),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f1389,f990]) ).

fof(f8105,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(multiply(X1,add(X2,X2)),X3)) = add(multiply(X0,multiply(X1,add(X2,X2))),multiply(X3,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f1389,f10]) ).

fof(f8147,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(X1,multiply(X2,add(X3,X3)))) = multiply(multiply(X1,multiply(X2,add(X3,X3))),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f1389,f8037]) ).

fof(f8288,plain,
    ! [X0,X1] : add(multiply(X0,multiply(X1,add(X0,X0))),add(X0,X0)) = multiply(add(X0,X0),add(X1,X0)),
    inference(backward_demodulation,[status(thm)],[f8083,f1177]) ).

fof(f8901,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),multiply(add(X1,add(X2,X0)),add(add(X0,X0),add(X0,X0)))) = multiply(add(X0,X0),add(add(X2,X0),add(X2,X0))),
    inference(paramodulation,[status(thm)],[f58,f3042]) ).

fof(f8905,plain,
    ! [X0,X1,X2,X3] : multiply(add(multiply(X0,X1),X1),multiply(add(X2,X1),add(add(X0,add(X3,X1)),add(X0,add(X3,X1))))) = multiply(add(X0,add(X3,X1)),add(X1,X1)),
    inference(paramodulation,[status(thm)],[f25,f3042]) ).

fof(f8938,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X1)),multiply(add(X2,X0),add(X1,X1))) = multiply(add(X1,X1),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f867,f3042]) ).

fof(f9123,plain,
    ! [X0,X1,X2] : multiply(multiply(add(X0,X0),add(X1,add(X2,X0))),add(X0,X0)) = multiply(add(X0,X0),add(add(X2,X0),add(X2,X0))),
    inference(forward_demodulation,[status(thm)],[f1348,f8901]) ).

fof(f9124,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,add(X2,X0))),add(X0,X0)) = multiply(add(X0,X0),add(add(X2,X0),add(X2,X0))),
    inference(forward_demodulation,[status(thm)],[f6249,f9123]) ).

fof(f9125,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(add(X1,add(X2,X0)),add(X0,X0))) = multiply(add(X0,X0),add(add(X2,X0),add(X2,X0))),
    inference(forward_demodulation,[status(thm)],[f6222,f9124]) ).

fof(f9126,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(X2,X2)) = multiply(add(X2,X2),add(add(X1,X2),add(X1,X2))),
    inference(forward_demodulation,[status(thm)],[f7424,f9125]) ).

fof(f9127,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(X2,X2)) = multiply(add(X2,X2),add(X2,add(X1,X2))),
    inference(forward_demodulation,[status(thm)],[f1018,f9126]) ).

fof(f9128,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(X2,X2)) = multiply(add(X2,X2),add(X2,X2)),
    inference(forward_demodulation,[status(thm)],[f1013,f9127]) ).

fof(f9129,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(X2,X2)) = multiply(X2,add(X2,X2)),
    inference(forward_demodulation,[status(thm)],[f992,f9128]) ).

fof(f9130,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(X2,X2)) = add(multiply(X2,X2),X2),
    inference(forward_demodulation,[status(thm)],[f1920,f9129]) ).

fof(f9145,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(X2,X2)) = add(X2,X2),
    inference(forward_demodulation,[status(thm)],[f1296,f9130]) ).

fof(f9152,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(add(X1,X0),add(add(X2,add(X3,X0)),add(X2,add(X3,X0))))) = multiply(add(X2,add(X3,X0)),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f7425,f8905]) ).

fof(f9153,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(add(X0,add(X1,X2)),add(X3,X2)),add(X2,X2)) = multiply(add(X0,add(X1,X2)),add(X2,X2)),
    inference(forward_demodulation,[status(thm)],[f6222,f9152]) ).

fof(f9156,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(add(X0,add(X1,X2)),add(X3,X2)),add(X2,X2)) = add(X2,X2),
    inference(forward_demodulation,[status(thm)],[f9145,f9153]) ).

fof(f9235,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X2)),multiply(X2,add(X0,X0))) = multiply(add(X0,X0),add(X2,X2)),
    inference(forward_demodulation,[status(thm)],[f6158,f8938]) ).

fof(f9237,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X2)),multiply(X2,add(X0,X0))) = multiply(X2,add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f992,f9235]) ).

fof(f9284,plain,
    ! [X0] : multiply(add(X0,X0),add(X0,multiply(multiply(X0,X0),X0))) = add(X0,multiply(multiply(X0,X0),X0)),
    inference(paramodulation,[status(thm)],[f2258,f262]) ).

fof(f9418,plain,
    ! [X0] : add(X0,X0) = add(X0,multiply(multiply(X0,X0),X0)),
    inference(forward_demodulation,[status(thm)],[f7531,f9284]) ).

fof(f9730,plain,
    ! [X0,X1,X2] : multiply(add(add(X0,X1),add(X0,X1)),add(add(X2,X2),X1)) = add(multiply(add(X0,X1),add(X2,X2)),add(X1,multiply(add(X0,X1),X1))),
    inference(paramodulation,[status(thm)],[f992,f252]) ).

fof(f9765,plain,
    ! [X0,X1,X2] : multiply(add(add(X0,X1),X1),add(X2,X1)) = add(multiply(X2,add(add(X0,X1),X1)),add(X1,X1)),
    inference(paramodulation,[status(thm)],[f857,f252]) ).

fof(f9843,plain,
    ! [X0,X1,X2] : multiply(add(add(X0,X1),add(X0,X1)),add(add(X2,X2),X1)) = add(multiply(add(X0,X1),add(X2,X2)),add(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f9,f9730]) ).

fof(f10009,plain,
    ! [X0,X1,X2] : multiply(add(add(X0,X1),add(X0,X1)),add(X1,add(X2,X2))) = add(add(X1,multiply(add(X0,X1),X1)),multiply(add(X0,X1),add(X2,X2))),
    inference(paramodulation,[status(thm)],[f992,f253]) ).

fof(f10132,plain,
    ! [X0,X1,X2] : multiply(add(add(X0,X1),add(X0,X1)),add(X1,add(X2,X2))) = add(add(X1,X1),multiply(add(X0,X1),add(X2,X2))),
    inference(forward_demodulation,[status(thm)],[f9,f10009]) ).

fof(f10250,plain,
    ! [X0,X1] : multiply(add(multiply(multiply(X0,X0),X0),multiply(multiply(X0,X0),X0)),add(X1,add(X0,X0))) = multiply(add(multiply(multiply(X0,X0),X0),multiply(multiply(X0,X0),X0)),add(X1,multiply(multiply(X0,X0),X0))),
    inference(paramodulation,[status(thm)],[f9418,f1013]) ).

fof(f10265,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(multiply(X1,multiply(multiply(X0,X0),X0)),multiply(multiply(X0,X0),X0))) = add(multiply(X1,multiply(multiply(X0,X0),X0)),multiply(multiply(X0,X0),X0)),
    inference(paramodulation,[status(thm)],[f9418,f34]) ).

fof(f10363,plain,
    ! [X0,X1] : multiply(multiply(X0,add(multiply(X0,X0),multiply(X0,X0))),add(X1,add(X0,X0))) = multiply(add(multiply(multiply(X0,X0),X0),multiply(multiply(X0,X0),X0)),add(X1,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f10,f10250]) ).

fof(f10364,plain,
    ! [X0,X1] : multiply(multiply(multiply(X0,X0),add(X0,X0)),add(X1,add(X0,X0))) = multiply(add(multiply(multiply(X0,X0),X0),multiply(multiply(X0,X0),X0)),add(X1,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1041,f10363]) ).

fof(f10365,plain,
    ! [X0,X1] : multiply(multiply(X0,add(X0,X0)),add(X1,add(X0,X0))) = multiply(add(multiply(multiply(X0,X0),X0),multiply(multiply(X0,X0),X0)),add(X1,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f6237,f10364]) ).

fof(f10366,plain,
    ! [X0,X1] : multiply(add(multiply(X0,X0),X0),add(X1,add(X0,X0))) = multiply(add(multiply(multiply(X0,X0),X0),multiply(multiply(X0,X0),X0)),add(X1,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1920,f10365]) ).

fof(f10367,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,add(X0,X0))) = multiply(add(multiply(multiply(X0,X0),X0),multiply(multiply(X0,X0),X0)),add(X1,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1296,f10366]) ).

fof(f10368,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X0)) = multiply(add(multiply(multiply(X0,X0),X0),multiply(multiply(X0,X0),X0)),add(X1,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1013,f10367]) ).

fof(f10369,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X0)) = multiply(multiply(X0,add(multiply(X0,X0),multiply(X0,X0))),add(X1,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f10,f10368]) ).

fof(f10370,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X0)) = multiply(multiply(multiply(X0,X0),add(X0,X0)),add(X1,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1041,f10369]) ).

fof(f10371,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X0)) = multiply(multiply(X0,add(X0,X0)),add(X1,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f6237,f10370]) ).

fof(f10372,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X0)) = multiply(add(multiply(X0,X0),X0),add(X1,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1920,f10371]) ).

fof(f10373,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X0)) = multiply(add(X0,X0),add(X1,multiply(multiply(X0,X0),X0))),
    inference(forward_demodulation,[status(thm)],[f1296,f10372]) ).

fof(f10455,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(multiply(X1,multiply(multiply(X0,X0),X0)),X0)) = add(multiply(X1,multiply(multiply(X0,X0),X0)),multiply(multiply(X0,X0),X0)),
    inference(forward_demodulation,[status(thm)],[f10373,f10265]) ).

fof(f10456,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(multiply(X1,multiply(multiply(X0,X0),X0)),X0)) = multiply(multiply(multiply(X0,X0),X0),add(X1,add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f4336,f10455]) ).

fof(f10889,plain,
    ! [X0,X1,X2] : multiply(multiply(add(X0,add(X1,X2)),X2),add(X2,X2)) = multiply(X2,add(add(X0,add(X1,X2)),add(X0,add(X1,X2)))),
    inference(paramodulation,[status(thm)],[f9145,f6157]) ).

fof(f11026,plain,
    ! [X0,X1,X2] : multiply(multiply(add(X0,add(X1,X2)),X2),add(X2,X2)) = multiply(add(X0,add(X1,X2)),add(X2,X2)),
    inference(forward_demodulation,[status(thm)],[f1041,f10889]) ).

fof(f11029,plain,
    ! [X0,X1,X2] : multiply(multiply(add(X0,add(X1,X2)),X2),add(X2,X2)) = add(X2,X2),
    inference(forward_demodulation,[status(thm)],[f9145,f11026]) ).

fof(f11982,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(multiply(add(X1,add(X2,X0)),X0),X0)) = add(add(X0,X0),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f11029,f990]) ).

fof(f12157,plain,
    ! [X0,X1,X2] : add(multiply(add(X0,add(X1,X2)),X2),X2) = add(add(X2,X2),add(X2,X2)),
    inference(forward_demodulation,[status(thm)],[f34,f11982]) ).

fof(f12159,plain,
    ! [X0,X1,X2] : add(multiply(add(X0,add(X1,X2)),X2),X2) = add(X2,X2),
    inference(forward_demodulation,[status(thm)],[f867,f12157]) ).

fof(f13767,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(add(X1,X1),add(X2,X2))) = multiply(multiply(X1,add(X2,X2)),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f1389,f6249]) ).

fof(f13779,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(multiply(X0,X1),add(X2,X2)),add(X3,X3)) = multiply(multiply(X2,multiply(X1,add(X0,X0))),add(X3,X3)),
    inference(paramodulation,[status(thm)],[f1348,f6249]) ).

fof(f13795,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(multiply(X0,add(X1,X1)),X2),add(X3,X3)) = multiply(multiply(multiply(X1,X0),X2),add(X3,X3)),
    inference(paramodulation,[status(thm)],[f10,f6249]) ).

fof(f13856,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(X1,multiply(add(X2,X2),X3))) = add(multiply(X1,add(X0,X0)),multiply(multiply(X2,X3),add(X0,X0))),
    inference(paramodulation,[status(thm)],[f6249,f10]) ).

fof(f13857,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(multiply(add(X1,X1),X2),X3)) = add(multiply(multiply(X1,X2),add(X0,X0)),multiply(X3,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f6249,f10]) ).

fof(f13869,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(multiply(X2,add(X1,X1)),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f992,f13767]) ).

fof(f13870,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(X0,multiply(X2,add(X1,X1))),
    inference(forward_demodulation,[status(thm)],[f1389,f13869]) ).

fof(f13907,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(multiply(X1,X2),add(X3,X3))) = multiply(multiply(X3,multiply(X2,add(X1,X1))),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f1389,f13779]) ).

fof(f13908,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(multiply(X1,X2),add(X3,X3))) = multiply(X0,multiply(X3,multiply(X2,add(X1,X1)))),
    inference(forward_demodulation,[status(thm)],[f8147,f13907]) ).

fof(f14132,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(X1,multiply(add(X2,X2),X3))) = multiply(add(X0,X0),add(X1,multiply(X2,X3))),
    inference(forward_demodulation,[status(thm)],[f10,f13856]) ).

fof(f14139,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(multiply(add(X1,X1),X2),X3)) = multiply(add(X0,X0),add(multiply(X1,X2),X3)),
    inference(forward_demodulation,[status(thm)],[f10,f13857]) ).

fof(f14257,plain,
    ! [X0,X1,X2] : multiply(multiply(add(X0,add(X1,multiply(n1,add(X0,X0)))),add(X2,multiply(n1,add(X0,X0)))),add(multiply(n1,add(X0,X0)),multiply(n1,add(X0,X0)))) = add(multiply(X0,multiply(n1,add(X0,X0))),multiply(n1,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f356,f290]) ).

fof(f14529,plain,
    ! [X0] : add(multiply(n1,add(X0,X0)),multiply(n1,add(X0,X0))) = add(multiply(X0,multiply(n1,add(X0,X0))),multiply(n1,add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f9156,f14257]) ).

fof(f14530,plain,
    ! [X0] : multiply(add(X0,X0),add(n1,n1)) = add(multiply(X0,multiply(n1,add(X0,X0))),multiply(n1,add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f10,f14529]) ).

fof(f14531,plain,
    ! [X0] : multiply(n1,add(X0,X0)) = add(multiply(X0,multiply(n1,add(X0,X0))),multiply(n1,add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f992,f14530]) ).

fof(f14532,plain,
    ! [X0] : multiply(n1,add(X0,X0)) = multiply(add(X0,X0),add(multiply(n1,add(X0,X0)),n1)),
    inference(forward_demodulation,[status(thm)],[f8105,f14531]) ).

fof(f14654,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(add(X2,X2),X2)) = add(multiply(add(X2,X2),add(X0,X2)),add(multiply(X0,X2),X2)),
    inference(paramodulation,[status(thm)],[f1013,f273]) ).

fof(f14816,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(add(X2,X2),X2)) = multiply(add(X0,X2),add(add(X2,X2),X2)),
    inference(forward_demodulation,[status(thm)],[f2051,f14654]) ).

fof(f16127,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(multiply(X1,multiply(X2,X2)),X0)) = add(multiply(multiply(X1,X2),add(X0,X0)),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f6536,f990]) ).

fof(f16153,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(X1,multiply(X2,multiply(X3,X3)))) = add(multiply(X1,add(X0,X0)),multiply(multiply(X2,X3),add(X0,X0))),
    inference(paramodulation,[status(thm)],[f6536,f10]) ).

fof(f16154,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(multiply(X1,multiply(X2,X2)),X3)) = add(multiply(multiply(X1,X2),add(X0,X0)),multiply(X3,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f6536,f10]) ).

fof(f16394,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(multiply(X1,X0),X0)) = add(multiply(X1,multiply(X0,X0)),multiply(X0,X0)),
    inference(backward_demodulation,[status(thm)],[f16395,f971]) ).

fof(f16395,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(multiply(X1,multiply(X2,X2)),X0)) = multiply(add(X0,X0),add(multiply(X1,X2),X0)),
    inference(forward_demodulation,[status(thm)],[f990,f16127]) ).

fof(f16444,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(X1,multiply(X2,multiply(X3,X3)))) = multiply(add(X0,X0),add(X1,multiply(X2,X3))),
    inference(forward_demodulation,[status(thm)],[f10,f16153]) ).

fof(f16448,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(multiply(X1,multiply(X2,X2)),X3)) = multiply(add(X0,X0),add(multiply(X1,X2),X3)),
    inference(forward_demodulation,[status(thm)],[f10,f16154]) ).

fof(f16519,plain,
    ! [X0,X1] : add(multiply(X0,X1),X1) = add(multiply(X0,multiply(X1,X1)),multiply(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f34,f16394]) ).

fof(f16547,plain,
    ! [X0,X1] : add(multiply(add(X0,X0),add(X1,X1)),add(X1,X1)) = add(multiply(multiply(X1,add(X1,X1)),add(X0,X0)),multiply(add(X1,X1),add(X1,X1))),
    inference(paramodulation,[status(thm)],[f1348,f16519]) ).

fof(f16693,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(add(X1,X1),X0)) = add(multiply(multiply(X0,add(X0,X0)),add(X1,X1)),multiply(add(X0,X0),add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f990,f16547]) ).

fof(f16694,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),add(X0,X0)) = add(multiply(multiply(X0,add(X0,X0)),add(X1,X1)),multiply(add(X0,X0),add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f5078,f16693]) ).

fof(f16695,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),add(X0,X0)) = add(multiply(X1,multiply(X0,add(X0,X0))),multiply(add(X0,X0),add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f1389,f16694]) ).

fof(f16696,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),add(X0,X0)) = add(multiply(X1,add(multiply(X0,X0),X0)),multiply(add(X0,X0),add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f1920,f16695]) ).

fof(f16697,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),add(X0,X0)) = multiply(add(multiply(X0,X0),X0),add(X1,add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f3678,f16696]) ).

fof(f16698,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),add(X0,X0)) = multiply(add(X0,X0),add(X1,add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f1296,f16697]) ).

fof(f16703,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),add(X0,X0)) = multiply(add(X0,X0),add(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f1013,f16698]) ).

fof(f17969,plain,
    ! [X0,X1] : multiply(add(X0,multiply(add(X1,X0),X0)),multiply(add(X1,X0),multiply(X0,X0))) = multiply(add(X1,X0),multiply(X0,X0)),
    inference(paramodulation,[status(thm)],[f24,f6417]) ).

fof(f18017,plain,
    ! [X0,X1,X2] : multiply(multiply(multiply(X0,multiply(X1,X1)),add(X2,multiply(X1,add(X0,X0)))),multiply(X0,multiply(X1,X1))) = multiply(multiply(X1,add(X0,X0)),multiply(X0,multiply(X1,X1))),
    inference(paramodulation,[status(thm)],[f6417,f26]) ).

fof(f18054,plain,
    ! [X0,X1] : multiply(add(X0,X0),multiply(add(X1,X0),multiply(X0,X0))) = multiply(add(X1,X0),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f9,f17969]) ).

fof(f18304,plain,
    ! [X0,X1,X2] : multiply(multiply(multiply(X0,multiply(X1,X1)),add(X2,multiply(X1,add(X0,X0)))),multiply(X0,multiply(X1,X1))) = multiply(X0,multiply(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f6417,f18017]) ).

fof(f18336,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(X1,multiply(add(X2,X2),multiply(add(X2,X2),add(X2,X2))))) = multiply(add(X0,X0),add(X1,multiply(add(X2,X2),add(X2,X2)))),
    inference(paramodulation,[status(thm)],[f6465,f6571]) ).

fof(f18411,plain,
    ! [X0,X1,X2] : multiply(add(multiply(add(X0,X0),add(X1,X2)),add(X1,multiply(X2,X2))),multiply(add(X1,multiply(X2,X2)),add(X1,multiply(X2,X2)))) = multiply(add(X1,multiply(X2,X2)),add(X1,multiply(X2,X2))),
    inference(paramodulation,[status(thm)],[f6571,f2048]) ).

fof(f18518,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(X1,multiply(X2,multiply(add(X2,X2),add(X2,X2))))) = multiply(add(X0,X0),add(X1,multiply(add(X2,X2),add(X2,X2)))),
    inference(forward_demodulation,[status(thm)],[f14132,f18336]) ).

fof(f18519,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(X1,multiply(X2,add(X2,X2)))) = multiply(add(X0,X0),add(X1,multiply(add(X2,X2),add(X2,X2)))),
    inference(forward_demodulation,[status(thm)],[f16444,f18518]) ).

fof(f18520,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(X1,add(multiply(X2,X2),X2))) = multiply(add(X0,X0),add(X1,multiply(add(X2,X2),add(X2,X2)))),
    inference(forward_demodulation,[status(thm)],[f1920,f18519]) ).

fof(f18521,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(X1,X2)) = multiply(add(X0,X0),add(X1,multiply(add(X2,X2),add(X2,X2)))),
    inference(forward_demodulation,[status(thm)],[f7493,f18520]) ).

fof(f18522,plain,
    ! [X0,X1,X2] : multiply(add(add(X0,X1),add(X0,X1)),add(X1,X2)) = add(add(X1,X1),multiply(add(X0,X1),add(X2,X2))),
    inference(backward_demodulation,[status(thm)],[f18530,f10132]) ).

fof(f18530,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(X1,X2)) = multiply(add(X0,X0),add(X1,add(X2,X2))),
    inference(forward_demodulation,[status(thm)],[f6571,f18521]) ).

fof(f19065,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(multiply(add(X1,X1),multiply(add(X1,X1),add(X1,X1))),X2)) = multiply(add(X0,X0),add(multiply(add(X1,X1),add(X1,X1)),X2)),
    inference(paramodulation,[status(thm)],[f6465,f6574]) ).

fof(f19255,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(multiply(X1,multiply(add(X1,X1),add(X1,X1))),X2)) = multiply(add(X0,X0),add(multiply(add(X1,X1),add(X1,X1)),X2)),
    inference(forward_demodulation,[status(thm)],[f14139,f19065]) ).

fof(f19256,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(multiply(X1,add(X1,X1)),X2)) = multiply(add(X0,X0),add(multiply(add(X1,X1),add(X1,X1)),X2)),
    inference(forward_demodulation,[status(thm)],[f16448,f19255]) ).

fof(f19257,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(add(multiply(X1,X1),X1),X2)) = multiply(add(X0,X0),add(multiply(add(X1,X1),add(X1,X1)),X2)),
    inference(forward_demodulation,[status(thm)],[f1920,f19256]) ).

fof(f19258,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(X1,X2)) = multiply(add(X0,X0),add(multiply(add(X1,X1),add(X1,X1)),X2)),
    inference(forward_demodulation,[status(thm)],[f7495,f19257]) ).

fof(f19259,plain,
    ! [X0,X1,X2] : multiply(add(add(X0,X1),add(X0,X1)),add(X2,X1)) = add(multiply(add(X0,X1),add(X2,X2)),add(X1,X1)),
    inference(backward_demodulation,[status(thm)],[f19275,f9843]) ).

fof(f19275,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(X1,X2)) = multiply(add(X0,X0),add(add(X1,X1),X2)),
    inference(forward_demodulation,[status(thm)],[f6574,f19258]) ).

fof(f20686,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(X2,add(X2,X2))) = add(add(multiply(X0,X2),X2),multiply(add(X2,X2),add(X0,X2))),
    inference(paramodulation,[status(thm)],[f1013,f274]) ).

fof(f20854,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(X2,add(X2,X2))) = multiply(add(X0,X2),add(X2,add(X2,X2))),
    inference(forward_demodulation,[status(thm)],[f2052,f20686]) ).

fof(f21307,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(add(multiply(X2,X2),multiply(X2,X2)),add(multiply(X2,X2),multiply(X2,X2))))) = multiply(multiply(multiply(add(multiply(X2,X2),multiply(X2,X2)),add(X2,multiply(X2,X2))),X1),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f6574,f7371]) ).

fof(f21552,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(multiply(X2,X2),multiply(X2,X2)))) = multiply(multiply(multiply(add(multiply(X2,X2),multiply(X2,X2)),add(X2,multiply(X2,X2))),X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f867,f21307]) ).

fof(f21553,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,multiply(X2,add(X2,X2)))) = multiply(multiply(multiply(add(multiply(X2,X2),multiply(X2,X2)),add(X2,multiply(X2,X2))),X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f10,f21552]) ).

fof(f21554,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(multiply(X2,X2),X2))) = multiply(multiply(multiply(add(multiply(X2,X2),multiply(X2,X2)),add(X2,multiply(X2,X2))),X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f1920,f21553]) ).

fof(f21555,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(multiply(multiply(add(multiply(X2,X2),multiply(X2,X2)),add(X2,multiply(X2,X2))),X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f1296,f21554]) ).

fof(f21556,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(multiply(multiply(add(multiply(X2,X2),multiply(X2,X2)),add(X2,X2)),X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f6571,f21555]) ).

fof(f21557,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(multiply(multiply(X2,add(multiply(X2,X2),multiply(X2,X2))),X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f13795,f21556]) ).

fof(f21559,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(multiply(multiply(multiply(X2,X2),X2),X1),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f13795,f21557]) ).

fof(f23957,plain,
    ! [X0,X1,X2] : add(multiply(X0,multiply(X1,add(X2,X2))),add(X0,X0)) = multiply(add(X0,X0),add(multiply(X2,X1),X0)),
    inference(paramodulation,[status(thm)],[f10,f16703]) ).

fof(f23978,plain,
    ! [X0,X1] : multiply(add(X0,X0),multiply(add(X0,X0),add(X1,X0))) = multiply(add(X0,X0),add(multiply(X0,add(X1,X1)),X0)),
    inference(paramodulation,[status(thm)],[f16703,f1013]) ).

fof(f23979,plain,
    ! [X0,X1] : multiply(X0,multiply(add(X0,X0),add(X1,X0))) = add(multiply(multiply(X0,add(X1,X1)),X0),X0),
    inference(paramodulation,[status(thm)],[f16703,f25]) ).

fof(f24144,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(multiply(X0,X1),X0)) = multiply(add(X0,X0),add(X1,X0)),
    inference(backward_demodulation,[status(thm)],[f23957,f8288]) ).

fof(f24185,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X0)) = multiply(add(X0,X0),add(multiply(X0,add(X1,X1)),X0)),
    inference(forward_demodulation,[status(thm)],[f1174,f23978]) ).

fof(f24186,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X0)) = add(multiply(X0,multiply(X0,add(X1,X1))),add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f8083,f24185]) ).

fof(f24187,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X0)) = multiply(add(X0,X0),add(multiply(X1,X0),X0)),
    inference(forward_demodulation,[status(thm)],[f23957,f24186]) ).

fof(f24188,plain,
    ! [X0,X1,X2] : add(multiply(multiply(add(X0,X1),add(X2,X1)),X1),X1) = add(X1,X1),
    inference(backward_demodulation,[status(thm)],[f24325,f5133]) ).

fof(f24206,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X0)),add(X1,X0)) = add(add(X0,X0),add(add(X1,X0),add(X1,X0))),
    inference(backward_demodulation,[status(thm)],[f24325,f5221]) ).

fof(f24216,plain,
    ! [X0,X1] : add(multiply(multiply(X0,multiply(multiply(X1,X1),X1)),X1),X1) = multiply(multiply(multiply(X1,X1),X1),add(X0,add(X1,X1))),
    inference(backward_demodulation,[status(thm)],[f24325,f10456]) ).

fof(f24308,plain,
    ! [X0,X1] : multiply(X0,add(multiply(X1,X0),X0)) = add(multiply(multiply(X1,add(X0,X0)),X0),X0),
    inference(backward_demodulation,[status(thm)],[f24325,f5098]) ).

fof(f24311,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,add(X1,X2)),add(add(X2,X2),X3)) = add(add(multiply(X0,X2),X2),multiply(X3,add(X0,add(X1,X2)))),
    inference(backward_demodulation,[status(thm)],[f24325,f4647]) ).

fof(f24312,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,add(X1,X2)),add(X3,add(X2,X2))) = add(multiply(X3,add(X0,add(X1,X2))),add(multiply(X0,X2),X2)),
    inference(backward_demodulation,[status(thm)],[f24325,f4646]) ).

fof(f24325,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X1,X0)) = add(multiply(X1,X0),X0),
    inference(forward_demodulation,[status(thm)],[f34,f24187]) ).

fof(f24326,plain,
    ! [X0,X1] : add(multiply(multiply(X0,add(X1,X1)),X1),X1) = add(multiply(multiply(X1,add(X0,X0)),X1),X1),
    inference(forward_demodulation,[status(thm)],[f5098,f23979]) ).

fof(f24506,plain,
    ! [X0,X1] : add(multiply(multiply(X0,X1),X0),X0) = multiply(add(X0,X0),add(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f24325,f24144]) ).

fof(f24509,plain,
    ! [X0,X1] : add(multiply(multiply(X0,add(X1,X1)),X1),X1) = add(multiply(add(X0,X0),X1),X1),
    inference(backward_demodulation,[status(thm)],[f24511,f24326]) ).

fof(f24511,plain,
    ! [X0,X1] : add(multiply(multiply(X0,X1),X0),X0) = add(multiply(X1,X0),X0),
    inference(forward_demodulation,[status(thm)],[f24325,f24506]) ).

fof(f24530,plain,
    ! [X0,X1] : add(add(multiply(X0,X1),X1),add(X0,X1)) = add(add(X1,X1),add(add(X0,X1),add(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f1920,f24206]) ).

fof(f24630,plain,
    ! [X0,X1] : add(multiply(multiply(X0,X1),X1),X1) = add(multiply(multiply(X0,add(X1,X1)),X1),X1),
    inference(forward_demodulation,[status(thm)],[f1920,f24308]) ).

fof(f24635,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(X2,X2)) = multiply(add(X0,X2),add(add(X2,X2),X2)),
    inference(backward_demodulation,[status(thm)],[f24636,f14816]) ).

fof(f24636,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,add(X1,X2)),add(add(X2,X2),X3)) = multiply(add(X0,add(X1,X2)),add(X2,X3)),
    inference(forward_demodulation,[status(thm)],[f274,f24311]) ).

fof(f24642,plain,
    ! [X0,X1,X2] : multiply(add(X0,add(X1,X2)),add(X2,X2)) = multiply(add(X0,X2),add(X2,add(X2,X2))),
    inference(backward_demodulation,[status(thm)],[f24645,f20854]) ).

fof(f24645,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,add(X1,X2)),add(X3,add(X2,X2))) = multiply(add(X0,add(X1,X2)),add(X3,X2)),
    inference(forward_demodulation,[status(thm)],[f273,f24312]) ).

fof(f24661,plain,
    ! [X0,X1] : add(multiply(multiply(X0,X1),X1),X1) = add(multiply(add(X0,X0),X1),X1),
    inference(forward_demodulation,[status(thm)],[f24630,f24509]) ).

fof(f24675,plain,
    ! [X0,X1] : add(X0,X0) = multiply(add(X1,X0),add(add(X0,X0),X0)),
    inference(forward_demodulation,[status(thm)],[f9145,f24635]) ).

fof(f24677,plain,
    ! [X0,X1] : add(X0,X0) = multiply(add(X1,X0),add(X0,add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f9145,f24642]) ).

fof(f24723,plain,
    ! [X0,X1] : multiply(add(X0,X0),multiply(add(X0,X0),add(add(X1,X0),add(X1,X0)))) = multiply(add(X0,X0),add(add(X1,X0),add(X1,X0))),
    inference(paramodulation,[status(thm)],[f24677,f9237]) ).

fof(f24882,plain,
    ! [X0,X1] : multiply(multiply(add(X0,X1),add(X1,X1)),add(X1,X1)) = multiply(add(X1,X1),add(add(X0,X1),add(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f1348,f24723]) ).

fof(f24883,plain,
    ! [X0,X1] : add(X0,X0) = multiply(add(X0,X0),add(add(X1,X0),add(X1,X0))),
    inference(forward_demodulation,[status(thm)],[f200,f24882]) ).

fof(f24884,plain,
    ! [X0,X1] : add(X0,X0) = multiply(add(X0,X0),add(X0,add(X1,X0))),
    inference(forward_demodulation,[status(thm)],[f1018,f24883]) ).

fof(f24971,plain,
    ! [X0,X1,X2] : multiply(multiply(add(X0,X1),add(X1,X1)),add(X2,add(X1,X1))) = add(multiply(X2,multiply(add(X0,X1),add(X1,X1))),multiply(add(X0,X1),add(X1,X1))),
    inference(paramodulation,[status(thm)],[f24884,f31]) ).

fof(f25148,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(X1,add(X0,X0))) = add(multiply(X1,multiply(add(X2,X0),add(X0,X0))),multiply(add(X2,X0),add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f58,f24971]) ).

fof(f25149,plain,
    ! [X0,X1,X2] : add(multiply(X0,add(X1,X1)),add(X1,X1)) = add(multiply(X0,multiply(add(X2,X1),add(X1,X1))),multiply(add(X2,X1),add(X1,X1))),
    inference(forward_demodulation,[status(thm)],[f1920,f25148]) ).

fof(f25150,plain,
    ! [X0,X1,X2] : add(multiply(X0,add(X1,X1)),add(X1,X1)) = multiply(multiply(add(X2,X1),add(X1,X1)),add(X0,multiply(X1,add(X2,X1)))),
    inference(forward_demodulation,[status(thm)],[f3437,f25149]) ).

fof(f25151,plain,
    ! [X0,X1,X2] : add(multiply(X0,add(X1,X1)),add(X1,X1)) = multiply(add(X1,X1),add(X0,multiply(X1,add(X2,X1)))),
    inference(forward_demodulation,[status(thm)],[f58,f25150]) ).

fof(f25152,plain,
    ! [X0,X1,X2] : add(multiply(X0,add(X1,X1)),add(X1,X1)) = multiply(add(X1,X1),add(X0,add(multiply(X2,X1),X1))),
    inference(forward_demodulation,[status(thm)],[f1920,f25151]) ).

fof(f25153,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),add(X1,X1)) = multiply(add(X1,X1),add(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f7493,f25152]) ).

fof(f25155,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),add(X1,X1)) = add(multiply(X0,X1),X1),
    inference(forward_demodulation,[status(thm)],[f24325,f25153]) ).

fof(f25251,plain,
    ! [X0,X1,X2] : multiply(add(add(add(X0,X1),add(X0,X1)),add(X0,X1)),add(X1,add(X2,add(X0,X1)))) = add(add(multiply(add(add(X0,X1),add(X0,X1)),X1),X1),add(add(X0,X1),add(X0,X1))),
    inference(paramodulation,[status(thm)],[f24675,f274]) ).

fof(f25294,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(multiply(add(add(X0,X0),X0),add(X1,add(X2,X0))),X3)) = add(multiply(add(X2,X0),add(add(X0,X0),X0)),multiply(X3,multiply(add(X2,X0),add(add(X0,X0),X0)))),
    inference(paramodulation,[status(thm)],[f24675,f32]) ).

fof(f25306,plain,
    ! [X0,X1,X2] : multiply(add(add(X0,X0),X0),add(X1,add(X2,X0))) = add(multiply(X1,add(add(X0,X0),X0)),add(X0,X0)),
    inference(paramodulation,[status(thm)],[f24675,f10]) ).

fof(f25419,plain,
    ! [X0,X1,X2] : multiply(add(add(add(X0,X1),add(X0,X1)),add(X0,X1)),add(X1,add(X2,add(X0,X1)))) = add(add(X1,X1),add(add(X0,X1),add(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f12159,f25251]) ).

fof(f25420,plain,
    ! [X0,X1,X2] : multiply(add(add(add(X0,X1),add(X0,X1)),add(X0,X1)),add(X1,add(X2,add(X0,X1)))) = add(add(multiply(X0,X1),X1),add(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f24530,f25419]) ).

fof(f25523,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(multiply(add(add(X0,X0),X0),add(X1,add(X2,X0))),X3)) = add(add(X0,X0),multiply(X3,multiply(add(X2,X0),add(add(X0,X0),X0)))),
    inference(forward_demodulation,[status(thm)],[f24675,f25294]) ).

fof(f25524,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(multiply(add(add(X0,X0),X0),add(X1,add(X2,X0))),X3)) = add(add(X0,X0),multiply(X3,add(X0,X0))),
    inference(forward_demodulation,[status(thm)],[f24675,f25523]) ).

fof(f25525,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X0),add(multiply(add(add(X0,X0),X0),add(X1,add(X2,X0))),X3)) = multiply(add(X0,X0),add(X0,X3)),
    inference(forward_demodulation,[status(thm)],[f991,f25524]) ).

fof(f25547,plain,
    ! [X0,X1] : multiply(add(add(add(X0,X1),add(X0,X1)),add(X0,X1)),add(X1,add(X0,X1))) = add(add(multiply(X0,X1),X1),add(X0,X1)),
    inference(backward_demodulation,[status(thm)],[f25553,f25420]) ).

fof(f25551,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(multiply(add(add(X0,X0),X0),add(X1,X0)),X2)) = multiply(add(X0,X0),add(X0,X2)),
    inference(backward_demodulation,[status(thm)],[f25553,f25525]) ).

fof(f25553,plain,
    ! [X0,X1,X2] : multiply(add(add(X0,X0),X0),add(X1,add(X2,X0))) = multiply(add(add(X0,X0),X0),add(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f9765,f25306]) ).

fof(f25564,plain,
    ! [X0,X1] : add(multiply(X0,X1),X1) = add(multiply(multiply(X0,X1),X1),X1),
    inference(paramodulation,[status(thm)],[f34,f24325]) ).

fof(f25570,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X1)),add(X2,multiply(X1,X0))) = add(multiply(X2,multiply(X1,X0)),multiply(X1,X0)),
    inference(paramodulation,[status(thm)],[f10,f24325]) ).

fof(f25698,plain,
    ! [X0,X1] : add(multiply(X0,X1),X1) = add(multiply(add(X0,X0),X1),X1),
    inference(backward_demodulation,[status(thm)],[f25564,f24661]) ).

fof(f26581,plain,
    ! [X0,X1] : add(multiply(add(X0,X0),add(X1,multiply(X1,X1))),add(multiply(X1,X1),multiply(X1,X1))) = add(multiply(add(X0,X0),multiply(X1,X1)),multiply(X1,X1)),
    inference(paramodulation,[status(thm)],[f6574,f25155]) ).

fof(f26692,plain,
    ! [X0,X1] : add(multiply(add(X0,X0),add(X1,X1)),add(multiply(X1,X1),multiply(X1,X1))) = add(multiply(add(X0,X0),multiply(X1,X1)),multiply(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f6571,f26581]) ).

fof(f26693,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),add(multiply(X0,X0),multiply(X0,X0))) = add(multiply(add(X1,X1),multiply(X0,X0)),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f992,f26692]) ).

fof(f26694,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),multiply(X0,add(X0,X0))) = add(multiply(add(X1,X1),multiply(X0,X0)),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f10,f26693]) ).

fof(f26695,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),add(multiply(X0,X0),X0)) = add(multiply(add(X1,X1),multiply(X0,X0)),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f1920,f26694]) ).

fof(f26696,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),add(X0,X0)) = add(multiply(add(X1,X1),multiply(X0,X0)),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f1296,f26695]) ).

fof(f26697,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),add(X0,X0)) = add(multiply(add(X1,X1),X0),X0),
    inference(forward_demodulation,[status(thm)],[f16519,f26696]) ).

fof(f26698,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),add(X0,X0)) = add(multiply(X1,X0),X0),
    inference(forward_demodulation,[status(thm)],[f25698,f26697]) ).

fof(f26969,plain,
    ! [X0] : add(X0,n1) = add(inverse(n1),n1),
    inference(paramodulation,[status(thm)],[f9,f323]) ).

fof(f26971,plain,
    ! [X0] : multiply(add(X0,X0),n1) = multiply(add(X0,X0),add(inverse(n1),n1)),
    inference(paramodulation,[status(thm)],[f323,f6571]) ).

fof(f27019,plain,
    ! [X0] : multiply(n1,add(X0,X0)) = multiply(add(X0,X0),add(inverse(n1),n1)),
    inference(backward_demodulation,[status(thm)],[f26969,f14532]) ).

fof(f27130,plain,
    ! [X0] : multiply(n1,add(X0,X0)) = multiply(add(X0,X0),n1),
    inference(forward_demodulation,[status(thm)],[f26971,f27019]) ).

fof(f27537,plain,
    multiply(n1,add(n1,n1)) = n1,
    inference(paramodulation,[status(thm)],[f9,f27130]) ).

fof(f27545,plain,
    ! [X0,X1] : add(X0,X0) = add(multiply(X1,inverse(X1)),multiply(n1,add(X0,X0))),
    inference(paramodulation,[status(thm)],[f27130,f307]) ).

fof(f27565,plain,
    add(multiply(n1,n1),n1) = n1,
    inference(forward_demodulation,[status(thm)],[f1920,f27537]) ).

fof(f27582,plain,
    add(n1,n1) = n1,
    inference(forward_demodulation,[status(thm)],[f1296,f27565]) ).

fof(f27654,plain,
    ! [X0] : add(multiply(multiply(add(X0,n1),n1),n1),n1) = add(n1,n1),
    inference(paramodulation,[status(thm)],[f27582,f24188]) ).

fof(f27703,plain,
    ! [X0,X1] : multiply(add(multiply(X0,X1),X1),n1) = multiply(X1,add(n1,n1)),
    inference(paramodulation,[status(thm)],[f27582,f6226]) ).

fof(f27705,plain,
    ! [X0] : multiply(multiply(X0,X0),n1) = multiply(X0,add(n1,n1)),
    inference(paramodulation,[status(thm)],[f27582,f6237]) ).

fof(f27726,plain,
    ! [X0] : multiply(X0,add(n1,n1)) = multiply(n1,add(X0,X0)),
    inference(paramodulation,[status(thm)],[f27582,f992]) ).

fof(f27750,plain,
    ! [X0] : add(multiply(add(X0,n1),n1),n1) = add(n1,n1),
    inference(forward_demodulation,[status(thm)],[f25564,f27654]) ).

fof(f27751,plain,
    add(inverse(n1),n1) = add(n1,n1),
    inference(forward_demodulation,[status(thm)],[f26969,f27750]) ).

fof(f27759,plain,
    ! [X0] : add(X0,n1) = n1,
    inference(backward_demodulation,[status(thm)],[f27760,f26969]) ).

fof(f27760,plain,
    add(inverse(n1),n1) = n1,
    inference(forward_demodulation,[status(thm)],[f27582,f27751]) ).

fof(f27825,plain,
    ! [X0,X1] : multiply(add(multiply(X0,X1),X1),n1) = multiply(X1,n1),
    inference(forward_demodulation,[status(thm)],[f27582,f27703]) ).

fof(f27832,plain,
    ! [X0] : multiply(multiply(X0,X0),n1) = multiply(X0,n1),
    inference(forward_demodulation,[status(thm)],[f27582,f27705]) ).

fof(f27878,plain,
    ! [X0,X1] : add(X0,X0) = add(multiply(X1,inverse(X1)),multiply(X0,n1)),
    inference(backward_demodulation,[status(thm)],[f27922,f27545]) ).

fof(f27922,plain,
    ! [X0] : multiply(X0,n1) = multiply(n1,add(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f27582,f27726]) ).

fof(f28005,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(multiply(multiply(X2,X2),X1),X0),
    inference(backward_demodulation,[status(thm)],[f29179,f7371]) ).

fof(f28021,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(multiply(X1,add(X2,X2)),X0),
    inference(backward_demodulation,[status(thm)],[f29179,f1389]) ).

fof(f28025,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),add(X2,X2)) = multiply(add(X2,X2),multiply(X1,X0)),
    inference(backward_demodulation,[status(thm)],[f29179,f1348]) ).

fof(f28028,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X0,X1)) = add(add(X0,X0),multiply(X1,X0)),
    inference(backward_demodulation,[status(thm)],[f29179,f991]) ).

fof(f28031,plain,
    ! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(multiply(X1,X0),multiply(X0,X1)),
    inference(backward_demodulation,[status(thm)],[f29179,f994]) ).

fof(f28034,plain,
    ! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(add(X1,X1),X0),
    inference(backward_demodulation,[status(thm)],[f29179,f992]) ).

fof(f28052,plain,
    ! [X0,X1] : add(X0,X0) = add(multiply(X1,X0),X0),
    inference(backward_demodulation,[status(thm)],[f29179,f3138]) ).

fof(f28129,plain,
    ! [X0,X1] : multiply(add(add(X0,X1),add(X0,X1)),add(X1,add(X0,X1))) = add(add(multiply(X0,X1),X1),add(X0,X1)),
    inference(backward_demodulation,[status(thm)],[f29179,f25547]) ).

fof(f28136,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(X2,X1)) = add(multiply(add(X0,X1),add(X2,X2)),add(X1,X1)),
    inference(backward_demodulation,[status(thm)],[f29179,f19259]) ).

fof(f28137,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(X1,X2)) = add(add(X1,X1),multiply(add(X0,X1),add(X2,X2))),
    inference(backward_demodulation,[status(thm)],[f29179,f18522]) ).

fof(f28163,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),X0) = add(multiply(X1,X0),X0),
    inference(backward_demodulation,[status(thm)],[f29179,f26698]) ).

fof(f28222,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),add(X2,multiply(X1,X0))) = add(multiply(X2,multiply(X1,X0)),multiply(X1,X0)),
    inference(backward_demodulation,[status(thm)],[f29179,f25570]) ).

fof(f28223,plain,
    ! [X0,X1,X2] : multiply(add(X0,X0),add(multiply(add(add(X0,X0),X0),add(X1,X0)),X2)) = multiply(X0,add(X0,X2)),
    inference(backward_demodulation,[status(thm)],[f29179,f25551]) ).

fof(f28304,plain,
    ! [X0,X1] : add(multiply(multiply(X0,multiply(multiply(X1,X1),X1)),X1),X1) = multiply(multiply(multiply(X1,X1),X1),add(X0,X1)),
    inference(backward_demodulation,[status(thm)],[f29179,f24216]) ).

fof(f28434,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(multiply(multiply(multiply(X2,X2),X2),X1),X0),
    inference(backward_demodulation,[status(thm)],[f29179,f21559]) ).

fof(f28558,plain,
    ! [X0,X1,X2] : multiply(add(multiply(X0,add(X1,X2)),add(X1,multiply(X2,X2))),multiply(add(X1,multiply(X2,X2)),add(X1,multiply(X2,X2)))) = multiply(add(X1,multiply(X2,X2)),add(X1,multiply(X2,X2))),
    inference(backward_demodulation,[status(thm)],[f29179,f18411]) ).

fof(f28577,plain,
    ! [X0,X1,X2] : multiply(multiply(multiply(X0,multiply(X1,X1)),add(X2,multiply(X1,X0))),multiply(X0,multiply(X1,X1))) = multiply(X0,multiply(X1,X1)),
    inference(backward_demodulation,[status(thm)],[f29179,f18304]) ).

fof(f28587,plain,
    ! [X0,X1] : multiply(X0,multiply(add(X1,X0),multiply(X0,X0))) = multiply(add(X1,X0),multiply(X0,X0)),
    inference(backward_demodulation,[status(thm)],[f29179,f18054]) ).

fof(f28761,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(multiply(X1,X2),add(X3,X3))) = multiply(X0,multiply(X3,multiply(X2,X1))),
    inference(backward_demodulation,[status(thm)],[f29179,f13908]) ).

fof(f28763,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X2))) = multiply(X0,multiply(X2,X1)),
    inference(backward_demodulation,[status(thm)],[f29179,f13870]) ).

fof(f29009,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(X1,multiply(X2,add(X3,X3)))) = multiply(multiply(multiply(X3,X2),X1),X0),
    inference(backward_demodulation,[status(thm)],[f29179,f7362]) ).

fof(f29023,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X1)),add(multiply(X0,X1),X2)) = add(multiply(X1,add(X0,X0)),multiply(X2,multiply(X0,X1))),
    inference(backward_demodulation,[status(thm)],[f29179,f6656]) ).

fof(f29024,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X1)),add(X2,multiply(X0,X1))) = add(multiply(X2,multiply(X0,add(X1,X1))),multiply(X1,X0)),
    inference(backward_demodulation,[status(thm)],[f29179,f6655]) ).

fof(f29052,plain,
    ! [X0,X1] : pixley(add(X0,X0),X1,multiply(X0,X0)) = add(multiply(X0,inverse(X1)),add(multiply(X0,X0),multiply(inverse(X1),multiply(X0,X0)))),
    inference(backward_demodulation,[status(thm)],[f29179,f6051]) ).

fof(f29070,plain,
    ! [X0,X1,X2] : multiply(pixley(add(X0,X1),X2,add(X1,X1)),multiply(add(X1,X1),add(X1,inverse(X2)))) = multiply(X1,add(X1,inverse(X2))),
    inference(backward_demodulation,[status(thm)],[f29179,f5006]) ).

fof(f29179,plain,
    ! [X0] : add(X0,X0) = X0,
    inference(forward_demodulation,[status(thm)],[f307,f27878]) ).

fof(f29275,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(multiply(X2,X2),X1),X0),
    inference(forward_demodulation,[status(thm)],[f29179,f28005]) ).

fof(f29291,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X1,add(X2,X2)),X0),
    inference(forward_demodulation,[status(thm)],[f29179,f28021]) ).

fof(f29292,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(multiply(X0,X1),X2),multiply(X2,multiply(X1,add(X3,X0)))) = multiply(multiply(X0,X1),X2),
    inference(backward_demodulation,[status(thm)],[f29417,f28]) ).

fof(f29293,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(X1,add(X2,X0))) = multiply(X0,X1),
    inference(backward_demodulation,[status(thm)],[f29417,f26]) ).

fof(f29296,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),n1) = add(multiply(X0,X1),multiply(multiply(X0,X1),inverse(multiply(X1,add(X2,X0))))),
    inference(backward_demodulation,[status(thm)],[f29417,f2987]) ).

fof(f29414,plain,
    ! [X0] : multiply(n1,multiply(X0,X0)) = multiply(X0,n1),
    inference(backward_demodulation,[status(thm)],[f29417,f27832]) ).

fof(f29417,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X1,X2),X0),
    inference(forward_demodulation,[status(thm)],[f29179,f29291]) ).

fof(f29421,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(add(X2,X2),multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f29179,f28025]) ).

fof(f29424,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(X2,multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f29179,f29421]) ).

fof(f29427,plain,
    ! [X0,X1] : multiply(X0,add(X0,X1)) = add(add(X0,X0),multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f29179,f28028]) ).

fof(f29432,plain,
    ! [X0,X1] : multiply(X0,add(X0,X1)) = add(X0,multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f29179,f29427]) ).

fof(f29439,plain,
    ! [X0,X1] : multiply(X0,X1) = multiply(multiply(X1,X0),multiply(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f29179,f28031]) ).

fof(f29442,plain,
    ! [X0,X1] : multiply(X0,X1) = multiply(add(X1,X1),X0),
    inference(forward_demodulation,[status(thm)],[f29179,f28034]) ).

fof(f29496,plain,
    ! [X0,X1] : multiply(n1,add(multiply(X0,X1),X1)) = multiply(X1,n1),
    inference(backward_demodulation,[status(thm)],[f29504,f27825]) ).

fof(f29504,plain,
    ! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
    inference(forward_demodulation,[status(thm)],[f29179,f29442]) ).

fof(f29542,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,add(X1,X2)),add(X3,X2)) = add(multiply(X3,add(X0,add(X1,X2))),X2),
    inference(backward_demodulation,[status(thm)],[f29628,f273]) ).

fof(f29628,plain,
    ! [X0,X1] : X0 = add(multiply(X1,X0),X0),
    inference(forward_demodulation,[status(thm)],[f29179,f28052]) ).

fof(f29733,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X0)),add(X1,X0)) = add(add(multiply(X1,X0),X0),add(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f24325,f28129]) ).

fof(f29734,plain,
    ! [X0,X1] : add(X0,X1) = add(add(multiply(X0,X1),X1),add(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f29628,f29733]) ).

fof(f29735,plain,
    ! [X0,X1] : add(X0,X1) = add(X1,add(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f29628,f29734]) ).

fof(f29761,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(X2,X1)) = add(multiply(add(X0,X1),X2),add(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f29179,f28136]) ).

fof(f29769,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(X2,X1)) = add(multiply(add(X0,X1),X2),X1),
    inference(forward_demodulation,[status(thm)],[f29179,f29761]) ).

fof(f29770,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(X1,X2)) = add(X1,multiply(add(X0,X1),add(X2,X2))),
    inference(forward_demodulation,[status(thm)],[f29179,f28137]) ).

fof(f29772,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(X1,X2)) = add(X1,multiply(add(X0,X1),X2)),
    inference(forward_demodulation,[status(thm)],[f29179,f29770]) ).

fof(f29816,plain,
    ! [X0,X1] : add(multiply(X0,X1),X0) = add(multiply(X1,X0),X0),
    inference(forward_demodulation,[status(thm)],[f29179,f28163]) ).

fof(f29817,plain,
    ! [X0,X1] : add(multiply(X0,X1),X0) = X0,
    inference(forward_demodulation,[status(thm)],[f29628,f29816]) ).

fof(f29926,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),add(X2,multiply(X1,X0))) = multiply(X1,X0),
    inference(forward_demodulation,[status(thm)],[f29628,f28222]) ).

fof(f29927,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X0,X1)) = multiply(X0,add(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f25551,f28223]) ).

fof(f29928,plain,
    ! [X0,X1] : add(X0,multiply(add(X0,X0),X1)) = multiply(X0,add(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f29772,f29927]) ).

fof(f29929,plain,
    ! [X0,X1] : add(X0,multiply(X0,X1)) = multiply(X0,add(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f29179,f29928]) ).

fof(f29930,plain,
    ! [X0,X1] : add(X0,multiply(X0,X1)) = add(X0,multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f29432,f29929]) ).

fof(f30222,plain,
    ! [X0,X1] : X0 = multiply(multiply(multiply(X0,X0),X0),add(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f29628,f28304]) ).

fof(f30223,plain,
    ! [X0,X1] : X0 = multiply(add(X1,X0),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f29275,f30222]) ).

fof(f30525,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(multiply(multiply(X2,X2),X2),X1),X0),
    inference(forward_demodulation,[status(thm)],[f29179,f28434]) ).

fof(f30526,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X1,multiply(X2,X2)),X0),
    inference(forward_demodulation,[status(thm)],[f29275,f30525]) ).

fof(f30872,plain,
    ! [X0,X1] : add(X0,multiply(X1,X1)) = multiply(add(X0,multiply(X1,X1)),add(X0,multiply(X1,X1))),
    inference(forward_demodulation,[status(thm)],[f30223,f28558]) ).

fof(f30873,plain,
    ! [X0,X1] : add(X0,multiply(X1,X1)) = add(multiply(add(X0,multiply(X1,X1)),X0),multiply(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f29769,f30872]) ).

fof(f30874,plain,
    ! [X0,X1] : add(X0,multiply(X1,X1)) = add(multiply(X0,add(X0,multiply(X1,X1))),multiply(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f29504,f30873]) ).

fof(f30875,plain,
    ! [X0,X1] : add(X0,multiply(X1,X1)) = add(add(X0,multiply(multiply(X1,X1),X0)),multiply(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f29432,f30874]) ).

fof(f30901,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,multiply(X1,X1)),multiply(add(X2,multiply(X1,X0)),multiply(X0,multiply(X1,X1)))) = multiply(X0,multiply(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f29424,f28577]) ).

fof(f30902,plain,
    ! [X0,X1,X2] : multiply(multiply(add(X0,multiply(X1,X2)),multiply(X2,multiply(X1,X1))),multiply(X2,X1)) = multiply(X2,multiply(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f30526,f30901]) ).

fof(f30903,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(multiply(X0,multiply(X1,X1)),add(X2,multiply(X1,X0)))) = multiply(X0,multiply(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f29424,f30902]) ).

fof(f30904,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(add(X2,multiply(X1,X0)),multiply(X0,X1))) = multiply(X0,multiply(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f30526,f30903]) ).

fof(f30905,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(multiply(X1,X0),add(X2,multiply(X1,X0)))) = multiply(X0,multiply(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f29424,f30904]) ).

fof(f30906,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),add(multiply(X2,multiply(X1,X0)),multiply(X1,X0))) = multiply(X0,multiply(X1,X1)),
    inference(forward_demodulation,[status(thm)],[f1920,f30905]) ).

fof(f30918,plain,
    ! [X0,X1] : multiply(X0,X1) = multiply(X1,multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f29926,f30906]) ).

fof(f30979,plain,
    ! [X0,X1] : multiply(X0,X0) = multiply(add(X1,X0),multiply(X0,X0)),
    inference(forward_demodulation,[status(thm)],[f30223,f28587]) ).

fof(f30992,plain,
    ! [X0,X1] : add(X0,multiply(X1,X1)) = add(add(X0,multiply(multiply(X1,X1),X0)),X1),
    inference(backward_demodulation,[status(thm)],[f31036,f30875]) ).

fof(f31036,plain,
    ! [X0] : multiply(X0,X0) = X0,
    inference(forward_demodulation,[status(thm)],[f30223,f30979]) ).

fof(f31660,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(multiply(X1,X2),X3)) = multiply(X0,multiply(X3,multiply(X2,X1))),
    inference(forward_demodulation,[status(thm)],[f29179,f28761]) ).

fof(f31666,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(X0,multiply(X2,X1)),
    inference(forward_demodulation,[status(thm)],[f29179,f28763]) ).

fof(f32619,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(X1,multiply(X2,X3))) = multiply(multiply(multiply(X3,X2),X1),X0),
    inference(forward_demodulation,[status(thm)],[f29179,f29009]) ).

fof(f32681,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),add(multiply(X0,X1),X2)) = add(multiply(X1,add(X0,X0)),multiply(X2,multiply(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f29179,f29023]) ).

fof(f32682,plain,
    ! [X0,X1,X2] : add(multiply(X0,X1),multiply(X2,multiply(X0,X1))) = add(multiply(X1,add(X0,X0)),multiply(X2,multiply(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f29432,f32681]) ).

fof(f32683,plain,
    ! [X0,X1,X2] : add(multiply(X0,X1),multiply(X2,multiply(X0,X1))) = add(multiply(X1,X0),multiply(X2,multiply(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f29179,f32682]) ).

fof(f32684,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),add(X2,multiply(X0,X1))) = add(multiply(X2,multiply(X0,add(X1,X1))),multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f29179,f29024]) ).

fof(f32685,plain,
    ! [X0,X1,X2] : add(multiply(X0,multiply(X1,X2)),multiply(X1,X2)) = add(multiply(X0,multiply(X1,add(X2,X2))),multiply(X2,X1)),
    inference(forward_demodulation,[status(thm)],[f1920,f32684]) ).

fof(f32686,plain,
    ! [X0,X1,X2] : multiply(X0,X1) = add(multiply(X2,multiply(X0,add(X1,X1))),multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f29628,f32685]) ).

fof(f32687,plain,
    ! [X0,X1,X2] : multiply(X0,X1) = add(multiply(X2,multiply(X0,X1)),multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f29179,f32686]) ).

fof(f32742,plain,
    ! [X0,X1] : pixley(X0,X1,multiply(X0,X0)) = add(multiply(X0,inverse(X1)),add(multiply(X0,X0),multiply(inverse(X1),multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f29179,f29052]) ).

fof(f32743,plain,
    ! [X0,X1] : pixley(X0,X1,X0) = add(multiply(X0,inverse(X1)),add(multiply(X0,X0),multiply(inverse(X1),multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f31036,f32742]) ).

fof(f32744,plain,
    ! [X0,X1] : X0 = add(multiply(X0,inverse(X1)),add(multiply(X0,X0),multiply(inverse(X1),multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f15,f32743]) ).

fof(f32745,plain,
    ! [X0,X1] : X0 = add(multiply(X0,inverse(X1)),add(X0,multiply(inverse(X1),multiply(X0,X0)))),
    inference(forward_demodulation,[status(thm)],[f31036,f32744]) ).

fof(f32746,plain,
    ! [X0,X1] : X0 = add(multiply(X0,inverse(X1)),add(X0,multiply(X0,inverse(X1)))),
    inference(forward_demodulation,[status(thm)],[f30918,f32745]) ).

fof(f32747,plain,
    ! [X0,X1] : X0 = add(X0,multiply(X0,inverse(X1))),
    inference(forward_demodulation,[status(thm)],[f29735,f32746]) ).

fof(f32811,plain,
    ! [X0,X1] : multiply(add(X0,X0),add(X0,inverse(X1))) = multiply(X0,add(X0,inverse(X1))),
    inference(forward_demodulation,[status(thm)],[f5006,f29070]) ).

fof(f32812,plain,
    ! [X0,X1] : add(X0,multiply(add(X0,X0),inverse(X1))) = multiply(X0,add(X0,inverse(X1))),
    inference(forward_demodulation,[status(thm)],[f29772,f32811]) ).

fof(f32813,plain,
    ! [X0,X1] : add(X0,multiply(X0,inverse(X1))) = multiply(X0,add(X0,inverse(X1))),
    inference(forward_demodulation,[status(thm)],[f29179,f32812]) ).

fof(f32814,plain,
    ! [X0,X1] : X0 = multiply(X0,add(X0,inverse(X1))),
    inference(forward_demodulation,[status(thm)],[f32747,f32813]) ).

fof(f32826,plain,
    ! [X0,X1] : X0 = add(X0,multiply(inverse(X1),X0)),
    inference(forward_demodulation,[status(thm)],[f29432,f32814]) ).

fof(f33381,plain,
    ! [X0,X1,X2] : multiply(n1,multiply(X0,X1)) = add(multiply(X1,X0),multiply(multiply(X1,X0),inverse(multiply(X0,add(X2,X1))))),
    inference(forward_demodulation,[status(thm)],[f29424,f29296]) ).

fof(f33383,plain,
    ! [X0,X1] : multiply(n1,multiply(X0,X1)) = multiply(X1,X0),
    inference(forward_demodulation,[status(thm)],[f32747,f33381]) ).

fof(f33644,plain,
    ! [X0] : multiply(X0,X0) = multiply(X0,n1),
    inference(forward_demodulation,[status(thm)],[f33383,f29414]) ).

fof(f33645,plain,
    ! [X0] : X0 = add(inverse(n1),X0),
    inference(backward_demodulation,[status(thm)],[f33675,f323]) ).

fof(f33647,plain,
    ! [X0,X1] : X0 = add(multiply(X1,inverse(X1)),X0),
    inference(backward_demodulation,[status(thm)],[f33675,f307]) ).

fof(f33675,plain,
    ! [X0] : X0 = multiply(X0,n1),
    inference(forward_demodulation,[status(thm)],[f31036,f33644]) ).

fof(f33846,plain,
    ! [X0] : multiply(n1,X0) = multiply(X0,n1),
    inference(forward_demodulation,[status(thm)],[f29628,f29496]) ).

fof(f33853,plain,
    ! [X0] : multiply(n1,X0) = X0,
    inference(forward_demodulation,[status(thm)],[f33675,f33846]) ).

fof(f34102,plain,
    ! [X0,X1] : add(X0,X1) = add(add(X0,multiply(multiply(X1,X1),X0)),X1),
    inference(forward_demodulation,[status(thm)],[f31036,f30992]) ).

fof(f34109,plain,
    ! [X0,X1] : add(X0,X1) = add(add(X0,multiply(X1,X0)),X1),
    inference(forward_demodulation,[status(thm)],[f31036,f34102]) ).

fof(f34329,plain,
    ! [X0,X1,X2] : multiply(add(add(X0,X0),X1),add(X0,X2)) = add(add(X0,multiply(X1,X0)),multiply(X2,add(X0,X1))),
    inference(paramodulation,[status(thm)],[f29179,f253]) ).

fof(f34330,plain,
    ! [X0,X1,X2] : multiply(add(add(X0,X0),X1),add(X2,X0)) = add(multiply(X2,add(X0,X1)),add(X0,multiply(X1,X0))),
    inference(paramodulation,[status(thm)],[f29179,f252]) ).

fof(f34365,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(X0,X2)) = add(add(X0,multiply(X1,X0)),multiply(X2,add(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f29179,f34329]) ).

fof(f34366,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(X2,X0)) = add(multiply(X2,add(X0,X1)),add(X0,multiply(X1,X0))),
    inference(forward_demodulation,[status(thm)],[f29179,f34330]) ).

fof(f34392,plain,
    ! [X0,X1] : multiply(X0,add(X1,X0)) = add(multiply(X1,X0),X0),
    inference(paramodulation,[status(thm)],[f31036,f10]) ).

fof(f34429,plain,
    ! [X0,X1] : multiply(X0,add(X1,X0)) = X0,
    inference(forward_demodulation,[status(thm)],[f29628,f34392]) ).

fof(f34447,plain,
    ! [X0] : pixley(n1,X0,n1) = add(inverse(X0),add(n1,inverse(X0))),
    inference(paramodulation,[status(thm)],[f33853,f314]) ).

fof(f34463,plain,
    ! [X0,X1] : multiply(X0,add(n1,X1)) = add(X0,multiply(X1,X0)),
    inference(paramodulation,[status(thm)],[f33853,f10]) ).

fof(f34474,plain,
    ! [X0] : n1 = add(inverse(X0),add(n1,inverse(X0))),
    inference(forward_demodulation,[status(thm)],[f15,f34447]) ).

fof(f34475,plain,
    ! [X0,X1] : pixley(n1,X0,X1) = add(inverse(X0),multiply(X1,n1)),
    inference(backward_demodulation,[status(thm)],[f34482,f314]) ).

fof(f34482,plain,
    ! [X0] : n1 = add(n1,inverse(X0)),
    inference(forward_demodulation,[status(thm)],[f29735,f34474]) ).

fof(f34527,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,add(X1,inverse(X2))),add(pixley(X1,X2,X0),X3)) = multiply(multiply(X0,add(X1,inverse(X2))),add(n1,X3)),
    inference(backward_demodulation,[status(thm)],[f34463,f238]) ).

fof(f34560,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),add(n1,X2)) = add(multiply(X1,X0),multiply(X2,multiply(X0,X1))),
    inference(backward_demodulation,[status(thm)],[f34463,f32683]) ).

fof(f34568,plain,
    ! [X0,X1] : pixley(n1,X0,X1) = add(inverse(X0),X1),
    inference(forward_demodulation,[status(thm)],[f33675,f34475]) ).

fof(f34687,plain,
    ! [X0,X1] : add(add(X0,multiply(X1,X0)),X0) = X0,
    inference(paramodulation,[status(thm)],[f24,f29817]) ).

fof(f34789,plain,
    ! [X0,X1] : add(X0,inverse(X1)) = add(add(X0,inverse(X1)),inverse(X1)),
    inference(paramodulation,[status(thm)],[f34429,f32826]) ).

fof(f34811,plain,
    ! [X0,X1,X2] : pixley(add(X0,inverse(X1)),X1,X2) = add(inverse(X1),multiply(X2,add(X0,inverse(X1)))),
    inference(backward_demodulation,[status(thm)],[f34789,f39]) ).

fof(f34863,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,add(X1,X2)),add(X3,multiply(X2,X0))) = add(multiply(X3,multiply(X0,add(X1,X2))),multiply(X2,X0)),
    inference(paramodulation,[status(thm)],[f29293,f10]) ).

fof(f34864,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,add(X1,X2)),add(multiply(X2,X0),X3)) = add(multiply(X2,X0),multiply(X3,multiply(X0,add(X1,X2)))),
    inference(paramodulation,[status(thm)],[f29293,f10]) ).

fof(f34902,plain,
    ! [X0,X1] : multiply(X0,inverse(X1)) = multiply(inverse(X1),add(X1,X0)),
    inference(paramodulation,[status(thm)],[f10,f33647]) ).

fof(f34907,plain,
    ! [X0] : inverse(multiply(X0,inverse(X0))) = n1,
    inference(paramodulation,[status(thm)],[f11,f33647]) ).

fof(f34945,plain,
    ! [X0,X1,X2] : pixley(add(add(X0,X1),inverse(X2)),X2,X1) = add(inverse(X2),add(X1,multiply(inverse(X2),X1))),
    inference(paramodulation,[status(thm)],[f24,f34811]) ).

fof(f34960,plain,
    ! [X0,X1,X2] : pixley(add(add(X0,X1),inverse(X2)),X2,X1) = add(inverse(X2),X1),
    inference(forward_demodulation,[status(thm)],[f32826,f34945]) ).

fof(f34988,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,pixley(X1,multiply(X2,inverse(X2)),X3)),multiply(multiply(X3,add(X1,n1)),X0)) = multiply(multiply(X3,add(X1,inverse(multiply(X2,inverse(X2))))),X0),
    inference(paramodulation,[status(thm)],[f34907,f41]) ).

fof(f34991,plain,
    ! [X0,X1,X2] : pixley(X0,multiply(X1,inverse(X1)),X2) = add(multiply(X0,inverse(multiply(X1,inverse(X1)))),multiply(X2,add(X0,n1))),
    inference(paramodulation,[status(thm)],[f34907,f23]) ).

fof(f35009,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(multiply(X0,add(X1,n1)),X2),multiply(pixley(X1,multiply(X3,inverse(X3)),X0),X2)) = multiply(multiply(X0,add(X1,inverse(multiply(X3,inverse(X3))))),X2),
    inference(forward_demodulation,[status(thm)],[f29424,f34988]) ).

fof(f35010,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(multiply(X0,n1),X1),multiply(pixley(X2,multiply(X3,inverse(X3)),X0),X1)) = multiply(multiply(X0,add(X2,inverse(multiply(X3,inverse(X3))))),X1),
    inference(forward_demodulation,[status(thm)],[f27759,f35009]) ).

fof(f35011,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,X1),multiply(pixley(X2,multiply(X3,inverse(X3)),X0),X1)) = multiply(multiply(X0,add(X2,inverse(multiply(X3,inverse(X3))))),X1),
    inference(forward_demodulation,[status(thm)],[f33675,f35010]) ).

fof(f35012,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,X1),multiply(pixley(X2,multiply(X3,inverse(X3)),X0),X1)) = multiply(multiply(X0,add(X2,n1)),X1),
    inference(forward_demodulation,[status(thm)],[f34907,f35011]) ).

fof(f35013,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,X1),multiply(pixley(X2,multiply(X3,inverse(X3)),X0),X1)) = multiply(multiply(X0,n1),X1),
    inference(forward_demodulation,[status(thm)],[f27759,f35012]) ).

fof(f35014,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,X1),multiply(pixley(X2,multiply(X3,inverse(X3)),X0),X1)) = multiply(X0,X1),
    inference(forward_demodulation,[status(thm)],[f33675,f35013]) ).

fof(f35021,plain,
    ! [X0,X1,X2] : pixley(X0,multiply(X1,inverse(X1)),X2) = add(multiply(X0,n1),multiply(X2,add(X0,n1))),
    inference(forward_demodulation,[status(thm)],[f34907,f34991]) ).

fof(f35022,plain,
    ! [X0,X1,X2] : pixley(X0,multiply(X1,inverse(X1)),X2) = add(X0,multiply(X2,add(X0,n1))),
    inference(forward_demodulation,[status(thm)],[f33675,f35021]) ).

fof(f35023,plain,
    ! [X0,X1,X2] : pixley(X0,multiply(X1,inverse(X1)),X2) = add(X0,multiply(X2,n1)),
    inference(forward_demodulation,[status(thm)],[f27759,f35022]) ).

fof(f35025,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(add(X2,X0),X1)) = multiply(X0,X1),
    inference(backward_demodulation,[status(thm)],[f35026,f35014]) ).

fof(f35026,plain,
    ! [X0,X1,X2] : pixley(X0,multiply(X1,inverse(X1)),X2) = add(X0,X2),
    inference(forward_demodulation,[status(thm)],[f33675,f35023]) ).

fof(f35205,plain,
    ! [X0] : multiply(X0,add(X0,inverse(n1))) = multiply(n1,add(X0,inverse(n1))),
    inference(paramodulation,[status(thm)],[f33853,f1555]) ).

fof(f35215,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X1,inverse(X1)),add(X0,n1))) = multiply(multiply(X1,inverse(X1)),add(X0,inverse(multiply(X1,inverse(X1))))),
    inference(paramodulation,[status(thm)],[f34907,f1555]) ).

fof(f35230,plain,
    ! [X0] : add(X0,multiply(inverse(n1),X0)) = multiply(n1,add(X0,inverse(n1))),
    inference(forward_demodulation,[status(thm)],[f29432,f35205]) ).

fof(f35231,plain,
    ! [X0] : X0 = multiply(n1,add(X0,inverse(n1))),
    inference(forward_demodulation,[status(thm)],[f32826,f35230]) ).

fof(f35232,plain,
    ! [X0] : X0 = add(X0,inverse(n1)),
    inference(forward_demodulation,[status(thm)],[f33853,f35231]) ).

fof(f35257,plain,
    ! [X0,X1] : multiply(X0,multiply(multiply(X1,inverse(X1)),n1)) = multiply(multiply(X1,inverse(X1)),add(X0,inverse(multiply(X1,inverse(X1))))),
    inference(forward_demodulation,[status(thm)],[f27759,f35215]) ).

fof(f35258,plain,
    ! [X0,X1] : multiply(X0,multiply(n1,multiply(inverse(X1),X1))) = multiply(multiply(X1,inverse(X1)),add(X0,inverse(multiply(X1,inverse(X1))))),
    inference(forward_demodulation,[status(thm)],[f31660,f35257]) ).

fof(f35259,plain,
    ! [X0,X1] : multiply(X0,multiply(inverse(X1),X1)) = multiply(multiply(X1,inverse(X1)),add(X0,inverse(multiply(X1,inverse(X1))))),
    inference(forward_demodulation,[status(thm)],[f33853,f35258]) ).

fof(f35260,plain,
    ! [X0,X1] : multiply(X0,multiply(X1,inverse(X1))) = multiply(multiply(X1,inverse(X1)),add(X0,inverse(multiply(X1,inverse(X1))))),
    inference(forward_demodulation,[status(thm)],[f31666,f35259]) ).

fof(f35261,plain,
    ! [X0,X1] : multiply(X0,multiply(X1,inverse(X1))) = multiply(multiply(X1,inverse(X1)),add(X0,n1)),
    inference(forward_demodulation,[status(thm)],[f34907,f35260]) ).

fof(f35262,plain,
    ! [X0,X1] : multiply(X0,multiply(X1,inverse(X1))) = multiply(multiply(X1,inverse(X1)),n1),
    inference(forward_demodulation,[status(thm)],[f27759,f35261]) ).

fof(f35270,plain,
    ! [X0,X1] : multiply(X0,multiply(X1,inverse(X1))) = multiply(X1,inverse(X1)),
    inference(forward_demodulation,[status(thm)],[f33675,f35262]) ).

fof(f35359,plain,
    ! [X0,X1] : add(add(multiply(X0,X1),multiply(X0,X1)),multiply(X0,X1)) = multiply(X0,X1),
    inference(paramodulation,[status(thm)],[f29439,f34687]) ).

fof(f35441,plain,
    ! [X0,X1] : add(multiply(X0,add(X1,X1)),multiply(X1,X0)) = multiply(X1,X0),
    inference(forward_demodulation,[status(thm)],[f10,f35359]) ).

fof(f35448,plain,
    ! [X0,X1] : add(multiply(X0,X1),multiply(X1,X0)) = multiply(X1,X0),
    inference(forward_demodulation,[status(thm)],[f29179,f35441]) ).

fof(f35471,plain,
    ! [X0,X1] : multiply(multiply(X0,inverse(X0)),X1) = add(multiply(X0,inverse(X0)),multiply(X1,multiply(X0,inverse(X0)))),
    inference(paramodulation,[status(thm)],[f33647,f29432]) ).

fof(f35519,plain,
    ! [X0,X1] : multiply(multiply(X0,inverse(X0)),X1) = multiply(X1,multiply(X0,inverse(X0))),
    inference(forward_demodulation,[status(thm)],[f33647,f35471]) ).

fof(f35522,plain,
    ! [X0,X1] : multiply(multiply(X0,inverse(X0)),X1) = multiply(X0,inverse(X0)),
    inference(forward_demodulation,[status(thm)],[f35270,f35519]) ).

fof(f35610,plain,
    ! [X0,X1,X2] : multiply(multiply(multiply(X0,X1),X2),multiply(X2,add(X0,multiply(X1,X0)))) = multiply(multiply(X0,X1),X2),
    inference(paramodulation,[status(thm)],[f29930,f29293]) ).

fof(f36087,plain,
    ! [X0,X1,X2] : multiply(multiply(multiply(X0,add(X1,X0)),X2),multiply(X2,add(X1,X0))) = multiply(multiply(X0,add(X1,X0)),X2),
    inference(paramodulation,[status(thm)],[f31036,f29292]) ).

fof(f36201,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X2)),multiply(X0,multiply(add(X1,X2),X2))) = multiply(multiply(X2,add(X1,X2)),X0),
    inference(forward_demodulation,[status(thm)],[f32619,f36087]) ).

fof(f36202,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X2)),multiply(X0,multiply(X2,add(X1,X2)))) = multiply(multiply(X2,add(X1,X2)),X0),
    inference(forward_demodulation,[status(thm)],[f31666,f36201]) ).

fof(f36203,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X2)),multiply(X0,X2)) = multiply(multiply(X2,add(X1,X2)),X0),
    inference(forward_demodulation,[status(thm)],[f34429,f36202]) ).

fof(f36204,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(add(X2,X1),X0)) = multiply(multiply(X1,add(X2,X1)),X0),
    inference(forward_demodulation,[status(thm)],[f29424,f36203]) ).

fof(f36207,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(add(X2,X1),X0)) = multiply(X1,X0),
    inference(forward_demodulation,[status(thm)],[f34429,f36204]) ).

fof(f36635,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(inverse(X0),X2)) = add(multiply(X1,inverse(X0)),multiply(X2,add(X0,X1))),
    inference(paramodulation,[status(thm)],[f34902,f10]) ).

fof(f36849,plain,
    ! [X0,X1] : multiply(X0,inverse(X0)) = multiply(X1,inverse(X1)),
    inference(paramodulation,[status(thm)],[f35270,f35522]) ).

fof(f36960,plain,
    ! [X0] : inverse(n1) = multiply(X0,inverse(X0)),
    inference(paramodulation,[status(thm)],[f33853,f36849]) ).

fof(f37218,plain,
    ! [X0,X1] : multiply(inverse(X0),add(X1,X0)) = add(multiply(X1,inverse(X0)),inverse(n1)),
    inference(paramodulation,[status(thm)],[f36960,f10]) ).

fof(f37248,plain,
    ! [X0,X1] : multiply(inverse(X0),add(X1,X0)) = multiply(X1,inverse(X0)),
    inference(forward_demodulation,[status(thm)],[f35232,f37218]) ).

fof(f37273,plain,
    ! [X0] : multiply(inverse(inverse(X0)),n1) = multiply(X0,inverse(inverse(X0))),
    inference(paramodulation,[status(thm)],[f11,f37248]) ).

fof(f37276,plain,
    ! [X0,X1] : add(X0,X1) = add(add(X0,X1),multiply(X0,inverse(X1))),
    inference(paramodulation,[status(thm)],[f37248,f32826]) ).

fof(f37346,plain,
    ! [X0] : inverse(inverse(X0)) = multiply(X0,inverse(inverse(X0))),
    inference(forward_demodulation,[status(thm)],[f33675,f37273]) ).

fof(f37407,plain,
    ! [X0] : X0 = add(X0,inverse(inverse(X0))),
    inference(paramodulation,[status(thm)],[f37346,f32747]) ).

fof(f37424,plain,
    ! [X0,X1] : multiply(inverse(inverse(X0)),add(X1,X0)) = add(multiply(X1,inverse(inverse(X0))),inverse(inverse(X0))),
    inference(paramodulation,[status(thm)],[f37346,f10]) ).

fof(f37463,plain,
    ! [X0,X1] : multiply(inverse(inverse(X0)),add(X1,X0)) = inverse(inverse(X0)),
    inference(forward_demodulation,[status(thm)],[f29628,f37424]) ).

fof(f37522,plain,
    ! [X0,X1] : pixley(add(X0,inverse(inverse(X0))),inverse(X0),X1) = add(inverse(inverse(X0)),multiply(X1,X0)),
    inference(paramodulation,[status(thm)],[f37407,f34811]) ).

fof(f37524,plain,
    ! [X0,X1] : multiply(pixley(X0,inverse(X0),X1),multiply(X1,X0)) = multiply(X1,add(X0,inverse(inverse(X0)))),
    inference(paramodulation,[status(thm)],[f37407,f42]) ).

fof(f37552,plain,
    ! [X0,X1] : pixley(X0,inverse(X0),X1) = add(inverse(inverse(X0)),multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f37407,f37522]) ).

fof(f37555,plain,
    ! [X0,X1] : multiply(multiply(X0,X1),pixley(X0,inverse(X0),X1)) = multiply(X1,add(X0,inverse(inverse(X0)))),
    inference(forward_demodulation,[status(thm)],[f29424,f37524]) ).

fof(f37556,plain,
    ! [X0,X1] : multiply(multiply(X0,X1),pixley(X0,inverse(X0),X1)) = multiply(X1,X0),
    inference(forward_demodulation,[status(thm)],[f37407,f37555]) ).

fof(f38061,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,add(X1,multiply(X2,X1))),add(X3,multiply(X1,X2))) = add(multiply(X3,add(X0,add(X1,multiply(X1,X2)))),multiply(X1,X2)),
    inference(paramodulation,[status(thm)],[f29930,f29542]) ).

fof(f38939,plain,
    ! [X0] : add(n1,X0) = add(add(n1,X0),inverse(X0)),
    inference(paramodulation,[status(thm)],[f33853,f37276]) ).

fof(f39487,plain,
    ! [X0,X1] : add(inverse(inverse(X0)),multiply(add(X1,X0),inverse(inverse(X0)))) = multiply(add(X1,X0),inverse(inverse(X0))),
    inference(paramodulation,[status(thm)],[f37463,f35448]) ).

fof(f39491,plain,
    ! [X0,X1] : add(inverse(inverse(X0)),inverse(inverse(X0))) = add(inverse(inverse(X0)),multiply(add(X1,X0),inverse(inverse(X0)))),
    inference(paramodulation,[status(thm)],[f37463,f29930]) ).

fof(f39557,plain,
    ! [X0,X1] : multiply(inverse(inverse(X0)),add(n1,add(X1,X0))) = multiply(add(X1,X0),inverse(inverse(X0))),
    inference(forward_demodulation,[status(thm)],[f34463,f39487]) ).

fof(f39562,plain,
    ! [X0,X1] : inverse(inverse(X0)) = add(inverse(inverse(X0)),multiply(add(X1,X0),inverse(inverse(X0)))),
    inference(forward_demodulation,[status(thm)],[f29179,f39491]) ).

fof(f39563,plain,
    ! [X0,X1] : inverse(inverse(X0)) = multiply(inverse(inverse(X0)),add(n1,add(X1,X0))),
    inference(forward_demodulation,[status(thm)],[f34463,f39562]) ).

fof(f39566,plain,
    ! [X0,X1] : inverse(inverse(X0)) = multiply(add(X1,X0),inverse(inverse(X0))),
    inference(forward_demodulation,[status(thm)],[f39557,f39563]) ).

fof(f40765,plain,
    ! [X0,X1,X2,X3] : inverse(inverse(add(X0,multiply(X1,X0)))) = multiply(multiply(add(add(X2,X0),X1),add(X3,X0)),inverse(inverse(add(X0,multiply(X1,X0))))),
    inference(paramodulation,[status(thm)],[f252,f39566]) ).

fof(f40821,plain,
    ! [X0,X1,X2,X3] : inverse(inverse(add(X0,multiply(X1,X0)))) = multiply(inverse(inverse(add(X0,multiply(X1,X0)))),multiply(add(X2,X0),add(add(X3,X0),X1))),
    inference(forward_demodulation,[status(thm)],[f29424,f40765]) ).

fof(f40921,plain,
    ! [X0,X1,X2] : add(multiply(X0,X1),X2) = add(add(multiply(X0,X1),multiply(X2,multiply(X1,X0))),X2),
    inference(paramodulation,[status(thm)],[f31666,f34109]) ).

fof(f41003,plain,
    ! [X0,X1,X2] : add(multiply(X0,X1),X2) = add(multiply(multiply(X1,X0),add(n1,X2)),X2),
    inference(forward_demodulation,[status(thm)],[f34560,f40921]) ).

fof(f41166,plain,
    ! [X0,X1,X2,X3,X4] : multiply(add(X0,multiply(X1,X2)),add(X3,multiply(X2,X1))) = add(multiply(X3,add(X0,add(multiply(X4,multiply(X1,X2)),multiply(X2,X1)))),multiply(X2,X1)),
    inference(paramodulation,[status(thm)],[f32687,f29542]) ).

fof(f41356,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,multiply(X1,X2)),add(X3,multiply(X2,X1))) = add(multiply(X3,add(X0,multiply(X1,X2))),multiply(X2,X1)),
    inference(forward_demodulation,[status(thm)],[f32687,f41166]) ).

fof(f41593,plain,
    ! [X0,X1,X2,X3] : multiply(add(add(X0,X1),multiply(X2,X3)),add(X1,multiply(X3,X2))) = add(add(X1,multiply(multiply(X2,X3),X1)),multiply(X2,X3)),
    inference(paramodulation,[status(thm)],[f29926,f253]) ).

fof(f41792,plain,
    ! [X0,X1,X2,X3] : add(multiply(X0,add(add(X1,X0),multiply(X2,X3))),multiply(X3,X2)) = add(add(X0,multiply(multiply(X2,X3),X0)),multiply(X2,X3)),
    inference(forward_demodulation,[status(thm)],[f41356,f41593]) ).

fof(f41793,plain,
    ! [X0,X1,X2] : add(add(X0,multiply(multiply(X1,X2),X0)),multiply(X2,X1)) = add(add(X0,multiply(multiply(X1,X2),X0)),multiply(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f24,f41792]) ).

fof(f41794,plain,
    ! [X0,X1,X2] : add(add(X0,multiply(multiply(X1,X2),X0)),multiply(X2,X1)) = add(X0,multiply(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f34109,f41793]) ).

fof(f42470,plain,
    ! [X0] : n1 = add(inverse(X0),X0),
    inference(paramodulation,[status(thm)],[f14,f34568]) ).

fof(f45432,plain,
    ! [X0,X1,X2] : multiply(multiply(multiply(X0,X1),X2),multiply(add(X1,multiply(X1,X0)),X2)) = multiply(multiply(X0,X1),X2),
    inference(paramodulation,[status(thm)],[f29930,f35025]) ).

fof(f45725,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(pixley(X1,inverse(X1),X0),multiply(X0,add(X2,X1)))) = multiply(multiply(X1,X0),pixley(X1,inverse(X1),X0)),
    inference(paramodulation,[status(thm)],[f37556,f29292]) ).

fof(f45825,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(pixley(X1,inverse(X1),X0),multiply(X0,add(X2,X1)))) = multiply(X0,X1),
    inference(forward_demodulation,[status(thm)],[f37556,f45725]) ).

fof(f47434,plain,
    ! [X0,X1] : add(add(X0,X1),inverse(X1)) = add(inverse(X1),X1),
    inference(paramodulation,[status(thm)],[f14,f34960]) ).

fof(f47435,plain,
    ! [X0] : pixley(add(n1,X0),X0,X0) = add(inverse(X0),X0),
    inference(paramodulation,[status(thm)],[f38939,f34960]) ).

fof(f47499,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,add(add(add(X1,X0),inverse(X2)),inverse(X2))),add(add(inverse(X2),X0),X3)) = multiply(multiply(X0,add(add(add(X1,X0),inverse(X2)),inverse(X2))),add(n1,X3)),
    inference(paramodulation,[status(thm)],[f34960,f34527]) ).

fof(f47509,plain,
    ! [X0,X1] : add(add(X0,X1),inverse(X1)) = n1,
    inference(forward_demodulation,[status(thm)],[f42470,f47434]) ).

fof(f47510,plain,
    ! [X0] : add(n1,X0) = add(inverse(X0),X0),
    inference(forward_demodulation,[status(thm)],[f14,f47435]) ).

fof(f47666,plain,
    ! [X0,X1,X2] : add(multiply(X0,X1),X2) = add(multiply(multiply(X1,X0),n1),X2),
    inference(backward_demodulation,[status(thm)],[f47829,f41003]) ).

fof(f47829,plain,
    ! [X0] : add(n1,X0) = n1,
    inference(forward_demodulation,[status(thm)],[f42470,f47510]) ).

fof(f47860,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(X0,add(add(X1,X0),inverse(X2))),add(add(inverse(X2),X0),X3)) = multiply(multiply(X0,add(add(add(X1,X0),inverse(X2)),inverse(X2))),add(n1,X3)),
    inference(forward_demodulation,[status(thm)],[f34789,f47499]) ).

fof(f47861,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,multiply(inverse(X1),X0)),add(add(inverse(X1),X0),X2)) = multiply(multiply(X0,add(add(add(X3,X0),inverse(X1)),inverse(X1))),add(n1,X2)),
    inference(forward_demodulation,[status(thm)],[f24,f47860]) ).

fof(f47862,plain,
    ! [X0,X1,X2,X3] : multiply(X0,add(add(inverse(X1),X0),X2)) = multiply(multiply(X0,add(add(add(X3,X0),inverse(X1)),inverse(X1))),add(n1,X2)),
    inference(forward_demodulation,[status(thm)],[f32826,f47861]) ).

fof(f47863,plain,
    ! [X0,X1,X2,X3] : add(X0,multiply(X1,X0)) = multiply(multiply(X0,add(add(add(X2,X0),inverse(X3)),inverse(X3))),add(n1,X1)),
    inference(forward_demodulation,[status(thm)],[f24,f47862]) ).

fof(f47864,plain,
    ! [X0,X1,X2,X3] : add(X0,multiply(X1,X0)) = multiply(multiply(X0,add(add(X2,X0),inverse(X3))),add(n1,X1)),
    inference(forward_demodulation,[status(thm)],[f34789,f47863]) ).

fof(f47865,plain,
    ! [X0,X1,X2] : add(X0,multiply(X1,X0)) = multiply(add(X0,multiply(inverse(X2),X0)),add(n1,X1)),
    inference(forward_demodulation,[status(thm)],[f24,f47864]) ).

fof(f47866,plain,
    ! [X0,X1] : add(X0,multiply(X1,X0)) = multiply(X0,add(n1,X1)),
    inference(forward_demodulation,[status(thm)],[f32826,f47865]) ).

fof(f47867,plain,
    ! [X0,X1] : add(X0,multiply(X1,X0)) = multiply(X0,n1),
    inference(forward_demodulation,[status(thm)],[f47829,f47866]) ).

fof(f47872,plain,
    ! [X0,X1] : add(X0,multiply(X0,X1)) = X0,
    inference(backward_demodulation,[status(thm)],[f48032,f29930]) ).

fof(f47875,plain,
    ! [X0,X1,X2,X3] : multiply(add(add(X0,X1),X2),add(X1,X3)) = add(X1,multiply(X3,add(add(X0,X1),X2))),
    inference(backward_demodulation,[status(thm)],[f48032,f253]) ).

fof(f47876,plain,
    ! [X0,X1,X2,X3] : multiply(add(add(X0,X1),X2),add(X3,X1)) = add(multiply(X3,add(add(X0,X1),X2)),X1),
    inference(backward_demodulation,[status(thm)],[f48032,f252]) ).

fof(f47885,plain,
    ! [X0,X1,X2] : add(X0,multiply(X1,X2)) = add(X0,multiply(X2,X1)),
    inference(backward_demodulation,[status(thm)],[f48032,f41794]) ).

fof(f47945,plain,
    ! [X0,X1,X2,X3] : inverse(inverse(add(X0,multiply(X1,X0)))) = multiply(inverse(inverse(X0)),multiply(add(X2,X0),add(add(X3,X0),X1))),
    inference(backward_demodulation,[status(thm)],[f48032,f40821]) ).

fof(f47980,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X1),add(X2,multiply(X1,X3))) = add(multiply(X2,add(X0,add(X1,multiply(X1,X3)))),multiply(X1,X3)),
    inference(backward_demodulation,[status(thm)],[f48032,f38061]) ).

fof(f48008,plain,
    ! [X0,X1,X2] : multiply(multiply(multiply(X0,X1),X2),multiply(X2,X0)) = multiply(multiply(X0,X1),X2),
    inference(backward_demodulation,[status(thm)],[f48032,f35610]) ).

fof(f48015,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(X2,X0)) = add(multiply(X2,add(X0,X1)),X0),
    inference(backward_demodulation,[status(thm)],[f48032,f34366]) ).

fof(f48016,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),add(X0,X2)) = add(X0,multiply(X2,add(X0,X1))),
    inference(backward_demodulation,[status(thm)],[f48032,f34365]) ).

fof(f48032,plain,
    ! [X0,X1] : add(X0,multiply(X1,X0)) = X0,
    inference(forward_demodulation,[status(thm)],[f33675,f47867]) ).

fof(f48308,plain,
    ! [X0,X1,X2] : add(multiply(X0,X1),X2) = add(multiply(X1,X0),X2),
    inference(forward_demodulation,[status(thm)],[f33675,f47666]) ).

fof(f48612,plain,
    ! [X0,X1,X2] : multiply(multiply(multiply(X0,X1),X2),multiply(X1,X2)) = multiply(multiply(X0,X1),X2),
    inference(backward_demodulation,[status(thm)],[f47872,f45432]) ).

fof(f48792,plain,
    ! [X0,X1,X2,X3] : inverse(inverse(X0)) = multiply(inverse(inverse(X0)),multiply(add(X1,X0),add(add(X2,X0),X3))),
    inference(forward_demodulation,[status(thm)],[f48032,f47945]) ).

fof(f48861,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X1),add(X2,multiply(X1,X3))) = add(multiply(X2,add(X0,X1)),multiply(X1,X3)),
    inference(forward_demodulation,[status(thm)],[f47872,f47980]) ).

fof(f48917,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(X0,multiply(X2,X1))) = multiply(multiply(X1,X2),X0),
    inference(forward_demodulation,[status(thm)],[f32619,f48008]) ).

fof(f48925,plain,
    add(a,multiply(b,c)) != add(a,multiply(c,add(a,b))),
    inference(backward_demodulation,[status(thm)],[f48016,f16]) ).

fof(f49044,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(X1,multiply(X0,X2))) = multiply(multiply(X2,X0),X1),
    inference(forward_demodulation,[status(thm)],[f32619,f48612]) ).

fof(f49139,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,n1),add(multiply(X1,X0),X2)) = add(multiply(X1,X0),multiply(X2,multiply(X0,add(n1,X1)))),
    inference(paramodulation,[status(thm)],[f47829,f34864]) ).

fof(f49210,plain,
    ! [X0,X1,X2] : multiply(X0,add(multiply(X1,X0),X2)) = add(multiply(X1,X0),multiply(X2,multiply(X0,add(n1,X1)))),
    inference(forward_demodulation,[status(thm)],[f33675,f49139]) ).

fof(f49211,plain,
    ! [X0,X1,X2] : multiply(X0,add(multiply(X1,X0),X2)) = add(multiply(X1,X0),multiply(X2,multiply(X0,n1))),
    inference(forward_demodulation,[status(thm)],[f47829,f49210]) ).

fof(f49212,plain,
    ! [X0,X1,X2] : multiply(X0,add(multiply(X1,X0),X2)) = add(multiply(X1,X0),multiply(X2,X0)),
    inference(forward_demodulation,[status(thm)],[f33675,f49211]) ).

fof(f49215,plain,
    ! [X0,X1,X2] : multiply(X0,add(multiply(X1,X0),X2)) = multiply(X0,add(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f10,f49212]) ).

fof(f49525,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,add(X1,X2)),X2) = add(multiply(X2,multiply(X0,add(X1,X2))),multiply(X2,X0)),
    inference(paramodulation,[status(thm)],[f47872,f34863]) ).

fof(f49529,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,multiply(X1,X2)),multiply(X1,X0)) = multiply(multiply(X1,X2),X0),
    inference(paramodulation,[status(thm)],[f47872,f36207]) ).

fof(f49585,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(add(X1,X0),X2)) = add(multiply(X0,multiply(X2,add(X1,X0))),multiply(X0,X2)),
    inference(forward_demodulation,[status(thm)],[f29424,f49525]) ).

fof(f49593,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(multiply(X0,X2),X1)) = multiply(multiply(X0,X2),X1),
    inference(forward_demodulation,[status(thm)],[f29424,f49529]) ).

fof(f49653,plain,
    ! [X0] : add(X0,inverse(inverse(inverse(X0)))) = n1,
    inference(paramodulation,[status(thm)],[f37407,f47509]) ).

fof(f50253,plain,
    ! [X0,X1] : pixley(X0,inverse(inverse(X0)),X1) = add(multiply(X0,inverse(inverse(inverse(X0)))),multiply(X1,n1)),
    inference(paramodulation,[status(thm)],[f49653,f23]) ).

fof(f50280,plain,
    ! [X0] : multiply(inverse(inverse(inverse(X0))),inverse(X0)) = multiply(inverse(X0),n1),
    inference(paramodulation,[status(thm)],[f49653,f34902]) ).

fof(f50311,plain,
    ! [X0,X1] : pixley(X0,inverse(inverse(X0)),X1) = add(multiply(X0,inverse(inverse(inverse(X0)))),X1),
    inference(forward_demodulation,[status(thm)],[f33675,f50253]) ).

fof(f50352,plain,
    ! [X0] : multiply(inverse(X0),inverse(inverse(inverse(X0)))) = multiply(inverse(X0),n1),
    inference(forward_demodulation,[status(thm)],[f29504,f50280]) ).

fof(f50353,plain,
    ! [X0] : inverse(inverse(inverse(X0))) = multiply(inverse(X0),n1),
    inference(forward_demodulation,[status(thm)],[f37346,f50352]) ).

fof(f50402,plain,
    ! [X0,X1] : pixley(X0,inverse(inverse(X0)),X1) = add(multiply(X0,inverse(X0)),X1),
    inference(backward_demodulation,[status(thm)],[f50432,f50311]) ).

fof(f50432,plain,
    ! [X0] : inverse(inverse(inverse(X0))) = inverse(X0),
    inference(forward_demodulation,[status(thm)],[f33675,f50353]) ).

fof(f50480,plain,
    ! [X0,X1] : pixley(X0,inverse(inverse(X0)),X1) = add(inverse(n1),X1),
    inference(forward_demodulation,[status(thm)],[f36960,f50402]) ).

fof(f50486,plain,
    ! [X0,X1] : pixley(X0,inverse(inverse(X0)),X1) = X1,
    inference(forward_demodulation,[status(thm)],[f33645,f50480]) ).

fof(f50506,plain,
    ! [X0] : X0 = inverse(inverse(X0)),
    inference(paramodulation,[status(thm)],[f14,f50486]) ).

fof(f50610,plain,
    ! [X0,X1,X2,X3] : inverse(inverse(X0)) = multiply(X0,multiply(add(X1,X0),add(add(X2,X0),X3))),
    inference(backward_demodulation,[status(thm)],[f50506,f48792]) ).

fof(f50657,plain,
    ! [X0,X1] : pixley(X0,inverse(X0),X1) = add(X0,multiply(X1,X0)),
    inference(backward_demodulation,[status(thm)],[f50506,f37552]) ).

fof(f50739,plain,
    ! [X0,X1,X2,X3] : X0 = multiply(X0,multiply(add(X1,X0),add(add(X2,X0),X3))),
    inference(forward_demodulation,[status(thm)],[f50506,f50610]) ).

fof(f50864,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(X1,multiply(X0,add(X2,X1)))) = multiply(X0,X1),
    inference(backward_demodulation,[status(thm)],[f50868,f45825]) ).

fof(f50868,plain,
    ! [X0,X1] : pixley(X0,inverse(X0),X1) = X0,
    inference(forward_demodulation,[status(thm)],[f48032,f50657]) ).

fof(f50935,plain,
    ! [X0,X1,X2] : multiply(multiply(add(X0,X1),X2),X1) = multiply(X2,X1),
    inference(forward_demodulation,[status(thm)],[f49044,f50864]) ).

fof(f50948,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(add(X1,X0),X2)) = add(multiply(X2,X0),multiply(X0,X2)),
    inference(backward_demodulation,[status(thm)],[f50950,f49585]) ).

fof(f50950,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,add(X2,X0))) = multiply(X1,X0),
    inference(forward_demodulation,[status(thm)],[f29424,f50935]) ).

fof(f50974,plain,
    ! [X0,X1,X2] : X0 = multiply(X0,add(add(X1,X0),X2)),
    inference(backward_demodulation,[status(thm)],[f50976,f50739]) ).

fof(f50976,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(add(X1,X0),X2)) = multiply(X0,X2),
    inference(forward_demodulation,[status(thm)],[f35448,f50948]) ).

fof(f51027,plain,
    ! [X0,X1] : multiply(X0,add(X1,inverse(X0))) = multiply(X1,inverse(inverse(X0))),
    inference(paramodulation,[status(thm)],[f50506,f37248]) ).

fof(f51029,plain,
    ! [X0,X1] : multiply(X0,inverse(inverse(X1))) = multiply(X1,add(inverse(X1),X0)),
    inference(paramodulation,[status(thm)],[f50506,f34902]) ).

fof(f51063,plain,
    ! [X0,X1] : multiply(X0,add(X1,inverse(X0))) = multiply(X1,X0),
    inference(forward_demodulation,[status(thm)],[f50506,f51027]) ).

fof(f51065,plain,
    ! [X0,X1] : multiply(X0,X1) = multiply(X1,add(inverse(X1),X0)),
    inference(forward_demodulation,[status(thm)],[f50506,f51029]) ).

fof(f51113,plain,
    ! [X0,X1] : pixley(add(X0,inverse(X1)),X1,X1) = add(inverse(X1),multiply(X0,X1)),
    inference(paramodulation,[status(thm)],[f51063,f34811]) ).

fof(f51192,plain,
    ! [X0,X1] : add(X0,inverse(X1)) = add(inverse(X1),multiply(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f14,f51113]) ).

fof(f51968,plain,
    ! [X0,X1] : X0 = multiply(X0,add(X0,X1)),
    inference(paramodulation,[status(thm)],[f33645,f50974]) ).

fof(f52190,plain,
    ! [X0,X1] : add(add(X0,X1),X0) = add(X0,X1),
    inference(paramodulation,[status(thm)],[f51968,f48032]) ).

fof(f52334,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X1),add(multiply(X0,X2),X3)) = add(multiply(X0,X2),multiply(X3,add(add(X0,multiply(X0,X2)),X1))),
    inference(paramodulation,[status(thm)],[f47872,f47875]) ).

fof(f52365,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(add(X0,X1),X2),add(X0,multiply(X1,add(add(X3,X0),X2)))) = multiply(X2,add(X0,X1)),
    inference(paramodulation,[status(thm)],[f47875,f36207]) ).

fof(f52457,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X1),add(multiply(X0,X2),X3)) = add(multiply(X0,X2),multiply(X3,add(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f47872,f52334]) ).

fof(f53222,plain,
    ! [X0,X1,X2] : multiply(X0,add(X1,X2)) = add(multiply(X1,X0),multiply(X0,X2)),
    inference(paramodulation,[status(thm)],[f10,f47885]) ).

fof(f54284,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(add(X0,X1),X2),add(multiply(X0,add(add(X3,X1),X2)),X1)) = multiply(X2,add(X0,X1)),
    inference(paramodulation,[status(thm)],[f47876,f36207]) ).

fof(f56093,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(X2,X1)) = multiply(X2,multiply(X0,X1)),
    inference(paramodulation,[status(thm)],[f48032,f50950]) ).

fof(f56263,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(X0,X2)) = multiply(multiply(X0,X1),X2),
    inference(backward_demodulation,[status(thm)],[f56093,f49593]) ).

fof(f56455,plain,
    ! [X0,X1,X2] : multiply(multiply(X0,X1),multiply(X2,X1)) = multiply(multiply(X1,X2),X0),
    inference(backward_demodulation,[status(thm)],[f56263,f48917]) ).

fof(f56542,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X1),multiply(add(multiply(X1,X2),X3),X2)) = add(multiply(X1,X2),multiply(X3,multiply(X2,add(X0,X1)))),
    inference(backward_demodulation,[status(thm)],[f56909,f34864]) ).

fof(f56658,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(add(multiply(X1,add(add(X2,X3),X0)),X3),add(X1,X3))) = multiply(X0,add(X1,X3)),
    inference(backward_demodulation,[status(thm)],[f56909,f54284]) ).

fof(f56661,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(add(X1,multiply(X2,add(add(X3,X1),X0))),add(X1,X2))) = multiply(X0,add(X1,X2)),
    inference(backward_demodulation,[status(thm)],[f56909,f52365]) ).

fof(f56909,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X2,X0),X1),
    inference(forward_demodulation,[status(thm)],[f56093,f56455]) ).

fof(f57084,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X1),multiply(X2,add(multiply(X1,X2),X3))) = add(multiply(X1,X2),multiply(X3,multiply(X2,add(X0,X1)))),
    inference(forward_demodulation,[status(thm)],[f31666,f56542]) ).

fof(f57101,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X1),multiply(X2,add(X1,X3))) = add(multiply(X1,X2),multiply(X3,multiply(X2,add(X0,X1)))),
    inference(forward_demodulation,[status(thm)],[f49215,f57084]) ).

fof(f57744,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(add(X1,X2),add(multiply(X1,add(add(X3,X2),X0)),X2))) = multiply(X0,add(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f31666,f56658]) ).

fof(f57745,plain,
    ! [X0,X1,X2,X3] : multiply(X0,add(multiply(X1,add(add(X2,X3),X0)),multiply(X3,add(X1,X3)))) = multiply(X0,add(X1,X3)),
    inference(forward_demodulation,[status(thm)],[f52457,f57744]) ).

fof(f57746,plain,
    ! [X0,X1,X2,X3] : multiply(X0,add(multiply(X1,add(add(X2,X3),X0)),X3)) = multiply(X0,add(X1,X3)),
    inference(forward_demodulation,[status(thm)],[f34429,f57745]) ).

fof(f57747,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(add(X1,X2),add(X1,multiply(X2,add(add(X3,X1),X0))))) = multiply(X0,add(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f31666,f56661]) ).

fof(f57748,plain,
    ! [X0,X1,X2,X3] : multiply(X0,add(multiply(X1,add(X1,X2)),multiply(X2,add(add(X3,X1),X0)))) = multiply(X0,add(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f48861,f57747]) ).

fof(f57749,plain,
    ! [X0,X1,X2,X3] : multiply(X0,add(X1,multiply(X2,add(add(X3,X1),X0)))) = multiply(X0,add(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f51968,f57748]) ).

fof(f58555,plain,
    ! [X0,X1,X2,X3] : multiply(multiply(add(X0,X1),X2),add(X1,X3)) = add(multiply(X1,X2),multiply(X3,multiply(add(X0,X1),X2))),
    inference(paramodulation,[status(thm)],[f50976,f10]) ).

fof(f58654,plain,
    ! [X0,X1,X2,X3] : multiply(X0,multiply(add(X1,X2),add(X3,X1))) = add(multiply(X1,X0),multiply(X2,multiply(add(X3,X1),X0))),
    inference(forward_demodulation,[status(thm)],[f56909,f58555]) ).

fof(f58656,plain,
    ! [X0,X1,X2,X3] : multiply(X0,add(multiply(X1,add(X2,X3)),X2)) = add(multiply(X2,X0),multiply(X3,multiply(add(X1,X2),X0))),
    inference(forward_demodulation,[status(thm)],[f48015,f58654]) ).

fof(f60377,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X1),multiply(X2,add(X1,X3))) = add(multiply(X1,X2),multiply(X3,multiply(add(X0,X1),X2))),
    inference(paramodulation,[status(thm)],[f31666,f57101]) ).

fof(f60385,plain,
    ! [X0,X1,X2] : multiply(add(X0,X1),multiply(n1,add(X1,X2))) = add(multiply(X1,n1),multiply(X2,add(X0,X1))),
    inference(paramodulation,[status(thm)],[f33853,f57101]) ).

fof(f60558,plain,
    ! [X0,X1,X2,X3] : multiply(add(X0,X1),multiply(X2,add(X1,X3))) = multiply(X2,add(multiply(X0,add(X1,X3)),X1)),
    inference(forward_demodulation,[status(thm)],[f58656,f60377]) ).

fof(f60577,plain,
    ! [X0,X1,X2] : multiply(n1,add(multiply(X0,add(X1,X2)),X1)) = add(multiply(X1,n1),multiply(X2,add(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f60558,f60385]) ).

fof(f60578,plain,
    ! [X0,X1,X2] : add(multiply(X0,add(X1,X2)),X1) = add(multiply(X1,n1),multiply(X2,add(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f33853,f60577]) ).

fof(f60586,plain,
    ! [X0,X1,X2] : add(multiply(X0,add(X1,X2)),X1) = add(X1,multiply(X2,add(X0,X1))),
    inference(forward_demodulation,[status(thm)],[f33675,f60578]) ).

fof(f60921,plain,
    ! [X0,X1,X2,X3] : multiply(X0,add(multiply(X1,X2),X3)) = add(multiply(X2,multiply(X0,X1)),multiply(X3,X0)),
    inference(paramodulation,[status(thm)],[f56909,f10]) ).

fof(f62773,plain,
    ! [X0,X1] : add(X0,inverse(inverse(X1))) = add(X1,multiply(X0,inverse(X1))),
    inference(paramodulation,[status(thm)],[f50506,f51192]) ).

fof(f62849,plain,
    ! [X0,X1] : add(X0,X1) = add(X1,multiply(X0,inverse(X1))),
    inference(forward_demodulation,[status(thm)],[f50506,f62773]) ).

fof(f62916,plain,
    ! [X0,X1] : add(X0,X1) = add(X1,multiply(inverse(X1),X0)),
    inference(paramodulation,[status(thm)],[f47885,f62849]) ).

fof(f63051,plain,
    ! [X0,X1] : add(add(X0,X1),X0) = add(X0,multiply(X1,inverse(X0))),
    inference(paramodulation,[status(thm)],[f34902,f62916]) ).

fof(f63138,plain,
    ! [X0,X1] : add(X0,X1) = add(X0,multiply(X1,inverse(X0))),
    inference(forward_demodulation,[status(thm)],[f52190,f63051]) ).

fof(f63323,plain,
    ! [X0,X1,X2,X3] : multiply(X0,add(X1,multiply(X2,add(add(X3,X1),X0)))) = multiply(X0,add(X2,X1)),
    inference(backward_demodulation,[status(thm)],[f63421,f57746]) ).

fof(f63392,plain,
    ! [X0,X1,X2] : add(X0,multiply(X1,add(X0,X2))) = add(X0,multiply(X2,add(X1,X0))),
    inference(backward_demodulation,[status(thm)],[f63421,f60586]) ).

fof(f63421,plain,
    ! [X0,X1] : add(X0,X1) = add(X1,X0),
    inference(forward_demodulation,[status(thm)],[f62849,f63138]) ).

fof(f63586,plain,
    ! [X0,X1,X2] : multiply(X0,add(X1,X2)) = multiply(X0,add(X2,X1)),
    inference(forward_demodulation,[status(thm)],[f57749,f63323]) ).

fof(f63624,plain,
    add(a,multiply(b,c)) != add(a,multiply(b,add(c,a))),
    inference(backward_demodulation,[status(thm)],[f63392,f48925]) ).

fof(f63671,plain,
    add(a,multiply(b,c)) != add(a,multiply(b,add(a,c))),
    inference(forward_demodulation,[status(thm)],[f63586,f63624]) ).

fof(f64949,plain,
    ! [X0,X1,X2] : add(add(X0,X1),X2) = add(X2,multiply(inverse(X2),add(X1,X0))),
    inference(paramodulation,[status(thm)],[f63586,f62916]) ).

fof(f65051,plain,
    ! [X0,X1,X2] : add(add(X0,X1),X2) = add(add(X1,X0),X2),
    inference(forward_demodulation,[status(thm)],[f62916,f64949]) ).

fof(f65483,plain,
    ! [X0,X1,X2] : add(X0,add(X1,X2)) = add(add(X2,X1),X0),
    inference(paramodulation,[status(thm)],[f63421,f65051]) ).

fof(f71030,plain,
    ! [X0,X1,X2] : multiply(X0,add(X1,X2)) = add(multiply(X0,X1),multiply(X0,X2)),
    inference(paramodulation,[status(thm)],[f29504,f53222]) ).

fof(f87290,plain,
    ! [X0,X1,X2] : multiply(add(X0,multiply(X0,X1)),add(inverse(X0),X2)) = add(multiply(multiply(X0,X1),inverse(X0)),multiply(X2,X0)),
    inference(paramodulation,[status(thm)],[f47872,f36635]) ).

fof(f87680,plain,
    ! [X0,X1,X2] : multiply(X0,add(inverse(X0),X1)) = add(multiply(multiply(X0,X2),inverse(X0)),multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f47872,f87290]) ).

fof(f87681,plain,
    ! [X0,X1,X2] : multiply(X0,X1) = add(multiply(multiply(X1,X2),inverse(X1)),multiply(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f51065,f87680]) ).

fof(f87682,plain,
    ! [X0,X1,X2] : multiply(X0,X1) = add(multiply(inverse(X1),multiply(X1,X2)),multiply(X0,X1)),
    inference(forward_demodulation,[status(thm)],[f48308,f87681]) ).

fof(f87683,plain,
    ! [X0,X1,X2] : multiply(X0,X1) = multiply(X1,add(multiply(X2,inverse(X1)),X0)),
    inference(forward_demodulation,[status(thm)],[f60921,f87682]) ).

fof(f88699,plain,
    ! [X0,X1,X2] : add(add(multiply(X0,inverse(inverse(X1))),X2),X1) = add(X1,multiply(X2,inverse(X1))),
    inference(paramodulation,[status(thm)],[f87683,f62916]) ).

fof(f88879,plain,
    ! [X0,X1,X2] : add(X0,add(X1,multiply(X2,inverse(inverse(X0))))) = add(X0,multiply(X1,inverse(X0))),
    inference(forward_demodulation,[status(thm)],[f65483,f88699]) ).

fof(f88880,plain,
    ! [X0,X1,X2] : add(X0,add(X1,multiply(X2,X0))) = add(X0,multiply(X1,inverse(X0))),
    inference(forward_demodulation,[status(thm)],[f50506,f88879]) ).

fof(f88889,plain,
    ! [X0,X1,X2] : add(X0,add(X1,multiply(X2,X0))) = add(X1,X0),
    inference(forward_demodulation,[status(thm)],[f62849,f88880]) ).

fof(f89317,plain,
    ! [X0,X1,X2] : add(X0,multiply(X1,add(X2,X0))) = add(multiply(X1,X2),X0),
    inference(paramodulation,[status(thm)],[f71030,f88889]) ).

fof(f89720,plain,
    ! [X0,X1,X2] : add(X0,multiply(X1,add(X0,X2))) = add(multiply(X2,X1),X0),
    inference(backward_demodulation,[status(thm)],[f89317,f63392]) ).

fof(f90613,plain,
    add(a,multiply(b,c)) != add(multiply(c,b),a),
    inference(backward_demodulation,[status(thm)],[f89720,f63671]) ).

fof(f91588,plain,
    add(a,multiply(b,c)) != add(a,multiply(c,b)),
    inference(forward_demodulation,[status(thm)],[f63421,f90613]) ).

fof(f91589,plain,
    add(a,multiply(b,c)) != add(a,multiply(b,c)),
    inference(forward_demodulation,[status(thm)],[f47885,f91588]) ).

fof(f91590,plain,
    $false,
    inference(trivial_equality_resolution,[status(thm)],[f91589]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : BOO023-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03  % Command  : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35  % Computer : n017.cluster.edu
% 0.08/0.35  % Model    : x86_64 x86_64
% 0.08/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35  % Memory   : 8046.5625MB
% 0.08/0.35  % OS       : Linux 6.8.0-71-generic
% 0.08/0.35  % CPULimit : 300
% 0.08/0.35  % WCLimit  : 300
% 0.08/0.35  % DateTime : Mon Sep 21 13:43:57 UTC 2026
% 0.08/0.36  % CPUTime  : 
% 0.08/0.36  % Drodi V4.1.1
% 214.83/27.68  % Refutation found
% 214.83/27.68  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 214.83/27.68  % SZS output start CNFRefutation for theBenchmark
% See solution above
% 119.32/28.96  % Elapsed time: 28.385610 seconds
% 119.32/28.96  % CPU time: 173.682467 seconds
% 119.32/28.96  % Total memory used: 893.785 MB
% 119.32/28.96  % Net memory used: 866.834 MB
%------------------------------------------------------------------------------