%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : GRP691-1 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Jul 15 06:44:43 AM UTC 2025
% Result : Unsatisfiable 157.06s 157.30s
% Output : CNFRefutation 157.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 14
% Syntax : Number of clauses : 590 ( 590 unt; 0 nHn; 72 RR)
% Number of literals : 590 ( 589 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 763 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
mult(op_d,i(mult(a,op_d))) != i(a),
file('theBenchmark.p',goals) ).
cnf(c1,axiom,
mult(X,unit) = X,
file('theBenchmark.p',c05) ).
cnf(c2,axiom,
mult(unit,X) = X,
file('theBenchmark.p',c06) ).
cnf(c3,axiom,
mult(op_d,op_d) = op_e,
file('theBenchmark.p',c12) ).
cnf(c4,axiom,
mult(op_e,op_e) = op_f,
file('theBenchmark.p',c13) ).
cnf(c5,axiom,
mult(X,i(X)) = unit,
file('theBenchmark.p',c10) ).
cnf(c7,axiom,
mult(i(X),X) = unit,
file('theBenchmark.p',c09) ).
cnf(c8,axiom,
rd(mult(X,Y),Y) = X,
file('theBenchmark.p',c04) ).
cnf(c10,plain,
rd(X,unit) = X,
inference(equational,[status(thm)],[c1,c8]) ).
cnf(c11,plain,
rd(op_f,op_e) = op_e,
inference(equational,[status(thm)],[c4,c8]) ).
cnf(c12,plain,
rd(op_e,op_d) = op_d,
inference(equational,[status(thm)],[c3,c8]) ).
cnf(c13,plain,
rd(unit,X) = i(X),
inference(equational,[status(thm)],[c7,c8]) ).
cnf(c14,plain,
i(i(X)) = X,
inference(equational,[status(thm)],[c5,c8,c13]) ).
cnf(c15,axiom,
mult(rd(X,Y),Y) = X,
file('theBenchmark.p',c03) ).
cnf(c16,axiom,
mult(X,ld(X,Y)) = Y,
file('theBenchmark.p',c01) ).
cnf(c18,axiom,
ld(X,mult(X,Y)) = Y,
file('theBenchmark.p',c02) ).
cnf(c19,plain,
ld(X,X) = unit,
inference(equational,[status(thm)],[c1,c18]) ).
cnf(c20,plain,
ld(op_d,op_e) = op_d,
inference(equational,[status(thm)],[c3,c18]) ).
cnf(c22,plain,
ld(X,unit) = i(X),
inference(equational,[status(thm)],[c5,c18]) ).
cnf(c23,axiom,
mult(op_c,mult(op_c,op_c)) = op_d,
file('theBenchmark.p',c11) ).
cnf(c24,plain,
mult(op_c,op_c) = ld(op_c,op_d),
inference(equational,[status(thm)],[c18,c23]) ).
cnf(c25,plain,
ld(rd(X,Y),X) = Y,
inference(equational,[status(thm)],[c15,c18]) ).
cnf(c26,plain,
rd(X,ld(Y,X)) = Y,
inference(equational,[status(thm)],[c8,c16]) ).
cnf(c29,axiom,
mult(mult(X,Y),Z) = mult(mult(X,Z),ld(Z,mult(Y,Z))),
file('theBenchmark.p',c08) ).
cnf(c30,plain,
mult(mult(X,Y),ld(Y,mult(Z,Y))) = mult(mult(X,Z),Y),
inference(equational,[status(thm)],[c29]) ).
cnf(c31,plain,
mult(mult(i(X),Y),X) = ld(X,mult(Y,X)),
inference(equational,[status(thm)],[c2,c7,c30]) ).
cnf(c32,plain,
mult(mult(X,i(Y)),Y) = mult(mult(X,Y),i(Y)),
inference(equational,[status(thm)],[c5,c14,c22,c30]) ).
cnf(c33,plain,
mult(mult(X,X),i(X)) = X,
inference(equational,[status(thm)],[c2,c5,c32]) ).
cnf(c34,plain,
mult(op_e,i(op_d)) = op_d,
inference(equational,[status(thm)],[c3,c33]) ).
cnf(c35,plain,
ld(op_e,op_d) = i(op_d),
inference(equational,[status(thm)],[c18,c34]) ).
cnf(c36,plain,
mult(op_f,i(op_e)) = op_e,
inference(equational,[status(thm)],[c4,c33]) ).
cnf(c37,plain,
ld(op_f,op_e) = i(op_e),
inference(equational,[status(thm)],[c18,c36]) ).
cnf(c38,plain,
rd(X,i(X)) = mult(X,X),
inference(equational,[status(thm)],[c8,c33]) ).
cnf(c41,plain,
mult(i(X),i(X)) = rd(i(X),X),
inference(equational,[status(thm)],[c14,c38]) ).
cnf(c42,plain,
mult(ld(op_c,op_d),i(op_c)) = op_c,
inference(equational,[status(thm)],[c24,c33]) ).
cnf(c43,plain,
rd(ld(X,mult(Y,X)),X) = mult(i(X),Y),
inference(equational,[status(thm)],[c8,c31]) ).
cnf(c44,plain,
mult(i(X),rd(Y,X)) = rd(ld(X,Y),X),
inference(equational,[status(thm)],[c15,c43]) ).
cnf(c45,plain,
ld(i(X),mult(Y,i(X))) = mult(mult(X,Y),i(X)),
inference(equational,[status(thm)],[c2,c5,c30]) ).
cnf(c50,plain,
mult(mult(op_e,op_d),i(op_d)) = op_e,
inference(equational,[status(thm)],[c3,c32,c34]) ).
cnf(c51,plain,
rd(op_e,i(op_d)) = mult(op_e,op_d),
inference(equational,[status(thm)],[c8,c50]) ).
cnf(c53,plain,
mult(mult(rd(X,Y),Z),Y) = mult(X,ld(Y,mult(Z,Y))),
inference(equational,[status(thm)],[c15,c30]) ).
cnf(c54,plain,
mult(mult(X,rd(Y,Z)),Z) = mult(mult(X,Z),ld(Z,Y)),
inference(equational,[status(thm)],[c15,c30]) ).
cnf(c55,plain,
mult(op_e,ld(op_d,mult(X,op_d))) = mult(mult(op_d,X),op_d),
inference(equational,[status(thm)],[c3,c30]) ).
cnf(c56,plain,
mult(op_f,ld(op_e,mult(X,op_e))) = mult(mult(op_e,X),op_e),
inference(equational,[status(thm)],[c4,c30]) ).
cnf(c57,plain,
ld(op_f,mult(mult(op_e,X),op_e)) = ld(op_e,mult(X,op_e)),
inference(equational,[status(thm)],[c18,c56]) ).
cnf(c58,plain,
ld(op_e,mult(mult(op_d,X),op_d)) = ld(op_d,mult(X,op_d)),
inference(equational,[status(thm)],[c18,c55]) ).
cnf(c59,plain,
ld(X,mult(ld(i(X),Y),X)) = mult(Y,X),
inference(equational,[status(thm)],[c16,c31]) ).
cnf(c60,plain,
mult(ld(i(X),Y),X) = mult(X,mult(Y,X)),
inference(equational,[status(thm)],[c16,c59]) ).
cnf(c65,axiom,
mult(X,mult(Y,Z)) = mult(rd(mult(X,Y),X),mult(X,Z)),
file('theBenchmark.p',c07) ).
cnf(c66,plain,
mult(rd(mult(X,Y),X),mult(X,Z)) = mult(X,mult(Y,Z)),
inference(equational,[status(thm)],[c65]) ).
cnf(c67,plain,
mult(X,mult(Y,i(X))) = rd(mult(X,Y),X),
inference(equational,[status(thm)],[c1,c5,c66]) ).
cnf(c68,plain,
rd(op_d,op_c) = ld(op_c,op_d),
inference(equational,[status(thm)],[c16,c24,c42,c67]) ).
cnf(c69,plain,
rd(mult(op_d,op_e),op_d) = op_e,
inference(equational,[status(thm)],[c3,c34,c67]) ).
cnf(c70,plain,
mult(op_d,op_e) = mult(op_e,op_d),
inference(equational,[status(thm)],[c15,c69]) ).
cnf(c71,plain,
mult(i(op_d),op_e) = op_d,
inference(equational,[status(thm)],[c12,c18,c44,c69]) ).
cnf(c72,plain,
rd(op_d,op_e) = i(op_d),
inference(equational,[status(thm)],[c8,c71]) ).
cnf(c73,plain,
rd(mult(op_e,op_f),op_e) = op_f,
inference(equational,[status(thm)],[c4,c36,c67]) ).
cnf(c74,plain,
mult(op_e,op_f) = mult(op_f,op_e),
inference(equational,[status(thm)],[c15,c73]) ).
cnf(c75,plain,
mult(i(op_e),op_f) = op_e,
inference(equational,[status(thm)],[c11,c18,c44,c73]) ).
cnf(c76,plain,
rd(op_e,op_f) = i(op_e),
inference(equational,[status(thm)],[c8,c75]) ).
cnf(c77,plain,
mult(i(X),mult(X,Y)) = mult(X,mult(i(X),Y)),
inference(equational,[status(thm)],[c5,c13,c66]) ).
cnf(c78,plain,
mult(X,rd(i(X),X)) = i(X),
inference(equational,[status(thm)],[c1,c5,c41,c77]) ).
cnf(c79,plain,
ld(op_d,i(op_d)) = i(op_e),
inference(equational,[status(thm)],[c7,c15,c22,c58,c78]) ).
cnf(c80,plain,
ld(op_e,i(op_e)) = i(op_f),
inference(equational,[status(thm)],[c7,c15,c22,c57,c78]) ).
cnf(c81,plain,
rd(i(X),X) = ld(X,i(X)),
inference(equational,[status(thm)],[c18,c78]) ).
cnf(c82,plain,
ld(i(X),X) = mult(X,X),
inference(equational,[status(thm)],[c14,c38,c81]) ).
cnf(c83,plain,
mult(op_e,i(op_f)) = i(op_e),
inference(equational,[status(thm)],[c16,c80]) ).
cnf(c84,plain,
mult(op_d,i(op_e)) = i(op_d),
inference(equational,[status(thm)],[c16,c79]) ).
cnf(c85,plain,
mult(i(op_c),ld(op_c,op_d)) = op_c,
inference(equational,[status(thm)],[c1,c7,c24,c77]) ).
cnf(c88,plain,
rd(i(op_d),i(op_e)) = op_d,
inference(equational,[status(thm)],[c26,c79]) ).
cnf(c89,plain,
rd(i(op_e),i(op_f)) = op_e,
inference(equational,[status(thm)],[c26,c80]) ).
cnf(c92,plain,
rd(mult(op_e,op_d),op_e) = op_d,
inference(equational,[status(thm)],[c34,c67,c84]) ).
cnf(c94,plain,
rd(mult(op_f,op_e),op_f) = op_e,
inference(equational,[status(thm)],[c36,c67,c83]) ).
cnf(c95,plain,
mult(i(op_f),op_e) = i(op_e),
inference(equational,[status(thm)],[c18,c44,c76,c94]) ).
cnf(c97,plain,
mult(ld(op_c,op_d),op_c) = op_d,
inference(equational,[status(thm)],[c15,c68]) ).
cnf(c98,plain,
mult(op_f,i(op_d)) = mult(op_e,op_d),
inference(equational,[status(thm)],[c34,c35,c56,c70,c71]) ).
cnf(c99,plain,
mult(ld(X,i(X)),X) = i(X),
inference(equational,[status(thm)],[c15,c81]) ).
cnf(c100,plain,
ld(X,rd(mult(X,Y),X)) = mult(Y,i(X)),
inference(equational,[status(thm)],[c18,c67]) ).
cnf(c101,plain,
ld(i(op_c),ld(op_c,op_d)) = op_d,
inference(equational,[status(thm)],[c14,c24,c38,c85,c97,c100]) ).
cnf(c102,plain,
mult(op_d,op_c) = mult(op_c,op_d),
inference(equational,[status(thm)],[c60,c97,c101]) ).
cnf(c105,plain,
ld(op_d,mult(op_c,op_d)) = op_c,
inference(equational,[status(thm)],[c18,c102]) ).
cnf(c110,plain,
mult(i(op_e),i(op_f)) = ld(op_f,i(op_e)),
inference(equational,[status(thm)],[c36,c76,c100]) ).
cnf(c111,plain,
mult(ld(X,Y),i(X)) = ld(X,rd(Y,X)),
inference(equational,[status(thm)],[c16,c100]) ).
cnf(c113,plain,
mult(i(op_f),i(op_e)) = ld(op_e,i(op_f)),
inference(equational,[status(thm)],[c80,c81,c111]) ).
cnf(c114,plain,
rd(mult(i(X),Y),i(X)) = mult(i(X),mult(Y,X)),
inference(equational,[status(thm)],[c1,c7,c66]) ).
cnf(c119,plain,
mult(rd(X,Y),mult(Y,Z)) = mult(Y,mult(ld(Y,X),Z)),
inference(equational,[status(thm)],[c16,c66]) ).
cnf(c120,plain,
mult(rd(mult(X,Y),X),Z) = mult(X,mult(Y,ld(X,Z))),
inference(equational,[status(thm)],[c16,c66]) ).
cnf(c121,plain,
ld(op_d,mult(op_e,op_d)) = op_e,
inference(equational,[status(thm)],[c25,c92]) ).
cnf(c122,plain,
ld(op_e,mult(op_f,op_e)) = op_f,
inference(equational,[status(thm)],[c4,c31,c75]) ).
cnf(c125,plain,
rd(mult(X,mult(X,X)),X) = mult(X,X),
inference(equational,[status(thm)],[c33,c67]) ).
cnf(c128,plain,
mult(mult(X,op_e),op_f) = mult(mult(X,op_f),op_e),
inference(equational,[status(thm)],[c18,c54,c73]) ).
cnf(c130,plain,
mult(mult(X,op_d),op_e) = mult(mult(X,op_e),op_d),
inference(equational,[status(thm)],[c18,c54,c69]) ).
cnf(c131,plain,
mult(mult(op_e,op_d),op_d) = op_f,
inference(equational,[status(thm)],[c3,c4,c70,c130]) ).
cnf(c132,plain,
mult(op_e,op_d) = rd(op_f,op_d),
inference(equational,[status(thm)],[c8,c131]) ).
cnf(c133,plain,
mult(op_d,mult(op_e,X)) = mult(op_e,mult(op_d,X)),
inference(equational,[status(thm)],[c66,c69]) ).
cnf(c134,plain,
rd(rd(op_f,op_d),op_d) = op_e,
inference(equational,[status(thm)],[c1,c5,c67,c70,c132,c133]) ).
cnf(c136,plain,
mult(op_d,mult(op_c,X)) = mult(op_c,mult(op_d,X)),
inference(equational,[status(thm)],[c8,c66,c102]) ).
cnf(c138,plain,
ld(ld(X,i(X)),i(X)) = X,
inference(equational,[status(thm)],[c25,c81]) ).
cnf(c139,plain,
ld(i(op_e),i(op_d)) = op_d,
inference(equational,[status(thm)],[c79,c138]) ).
cnf(c140,plain,
ld(i(op_f),i(op_e)) = op_e,
inference(equational,[status(thm)],[c80,c138]) ).
cnf(c141,plain,
ld(op_e,rd(op_f,op_d)) = op_d,
inference(equational,[status(thm)],[c59,c70,c71,c132,c139]) ).
cnf(c145,plain,
mult(mult(op_f,op_e),i(op_f)) = op_e,
inference(equational,[status(thm)],[c32,c74,c75,c83]) ).
cnf(c146,plain,
rd(op_e,i(op_f)) = mult(op_f,op_e),
inference(equational,[status(thm)],[c8,c145]) ).
cnf(c154,plain,
mult(op_d,mult(ld(op_d,X),op_d)) = mult(rd(X,op_d),op_e),
inference(equational,[status(thm)],[c3,c119]) ).
cnf(c155,plain,
mult(op_e,mult(ld(op_e,X),op_e)) = mult(rd(X,op_e),op_f),
inference(equational,[status(thm)],[c4,c119]) ).
cnf(c156,plain,
mult(i(op_d),op_f) = rd(op_f,op_d),
inference(equational,[status(thm)],[c35,c71,c72,c132,c155]) ).
cnf(c157,plain,
ld(op_d,mult(op_f,op_d)) = op_f,
inference(equational,[status(thm)],[c15,c31,c156]) ).
cnf(c158,plain,
rd(op_f,op_d) = ld(op_d,op_f),
inference(equational,[status(thm)],[c8,c98,c111,c132,c157]) ).
cnf(c159,plain,
mult(op_d,op_f) = mult(op_f,op_d),
inference(equational,[status(thm)],[c16,c157]) ).
cnf(c162,plain,
rd(mult(X,rd(Y,i(X))),X) = mult(X,Y),
inference(equational,[status(thm)],[c15,c67]) ).
cnf(c163,plain,
rd(ld(op_d,op_f),op_e) = op_d,
inference(equational,[status(thm)],[c34,c88,c132,c158,c162]) ).
cnf(c164,plain,
mult(X,rd(Y,i(X))) = mult(mult(X,Y),X),
inference(equational,[status(thm)],[c15,c162]) ).
cnf(c166,plain,
ld(op_d,ld(op_d,op_f)) = op_e,
inference(equational,[status(thm)],[c25,c163]) ).
cnf(c168,plain,
ld(op_e,ld(op_d,op_f)) = op_d,
inference(equational,[status(thm)],[c25,c134,c158]) ).
cnf(c170,plain,
mult(X,mult(i(X),Y)) = rd(rd(Y,i(X)),X),
inference(equational,[status(thm)],[c18,c44,c77,c162]) ).
cnf(c171,plain,
rd(ld(op_d,op_f),op_d) = op_e,
inference(equational,[status(thm)],[c3,c51,c71,c132,c158,c170]) ).
cnf(c174,plain,
mult(op_f,ld(op_e,i(op_f))) = i(op_e),
inference(equational,[status(thm)],[c14,c36,c77,c95,c113]) ).
cnf(c175,plain,
ld(op_e,i(op_f)) = ld(op_f,i(op_e)),
inference(equational,[status(thm)],[c18,c174]) ).
cnf(c180,plain,
mult(ld(op_f,i(op_e)),op_e) = i(op_f),
inference(equational,[status(thm)],[c31,c80,c95,c110]) ).
cnf(c188,plain,
mult(mult(X,X),ld(X,i(X))) = unit,
inference(equational,[status(thm)],[c7,c54,c78]) ).
cnf(c190,plain,
i(ld(X,i(X))) = mult(X,X),
inference(equational,[status(thm)],[c8,c13,c188]) ).
cnf(c195,plain,
rd(rd(mult(X,Y),i(Y)),Y) = rd(X,i(Y)),
inference(equational,[status(thm)],[c16,c60,c77,c114,c170]) ).
cnf(c196,plain,
mult(rd(X,i(Y)),Y) = rd(mult(X,Y),i(Y)),
inference(equational,[status(thm)],[c15,c195]) ).
cnf(c197,plain,
rd(rd(X,i(Y)),Y) = rd(rd(X,Y),i(Y)),
inference(equational,[status(thm)],[c15,c195]) ).
cnf(c199,plain,
rd(ld(X,Y),i(X)) = ld(X,mult(Y,X)),
inference(equational,[status(thm)],[c14,c15,c31,c44,c162,c196]) ).
cnf(c204,plain,
mult(rd(X,Y),i(Y)) = rd(mult(X,i(Y)),Y),
inference(equational,[status(thm)],[c14,c196]) ).
cnf(c210,plain,
rd(mult(mult(X,Y),i(Y)),Y) = mult(X,i(Y)),
inference(equational,[status(thm)],[c8,c32]) ).
cnf(c211,plain,
rd(X,ld(X,i(X))) = mult(X,mult(X,X)),
inference(equational,[status(thm)],[c1,c7,c77,c78,c81,c190,c210]) ).
cnf(c213,plain,
mult(mult(i(X),Y),i(X)) = rd(ld(X,Y),X),
inference(equational,[status(thm)],[c8,c31,c111,c210]) ).
cnf(c217,plain,
ld(mult(X,mult(X,X)),X) = ld(X,i(X)),
inference(equational,[status(thm)],[c25,c211]) ).
cnf(c218,plain,
ld(op_c,i(op_c)) = ld(op_d,op_c),
inference(equational,[status(thm)],[c23,c217]) ).
cnf(c219,plain,
i(ld(op_d,op_c)) = ld(op_c,op_d),
inference(equational,[status(thm)],[c24,c190,c218]) ).
cnf(c221,plain,
mult(ld(op_d,op_c),op_c) = i(op_c),
inference(equational,[status(thm)],[c99,c218]) ).
cnf(c222,plain,
mult(ld(op_d,op_c),op_d) = op_c,
inference(equational,[status(thm)],[c42,c77,c97,c219,c221]) ).
cnf(c223,plain,
rd(op_c,op_d) = ld(op_d,op_c),
inference(equational,[status(thm)],[c8,c222]) ).
cnf(c224,plain,
rd(mult(X,mult(Y,X)),X) = ld(i(X),Y),
inference(equational,[status(thm)],[c8,c60]) ).
cnf(c227,plain,
ld(i(X),rd(Y,X)) = rd(mult(X,Y),X),
inference(equational,[status(thm)],[c15,c224]) ).
cnf(c228,plain,
ld(X,mult(mult(X,Y),X)) = rd(Y,i(X)),
inference(equational,[status(thm)],[c18,c164]) ).
cnf(c263,plain,
ld(op_d,mult(ld(op_d,X),op_d)) = ld(op_e,mult(X,op_d)),
inference(equational,[status(thm)],[c16,c58]) ).
cnf(c269,plain,
ld(op_e,mult(ld(op_e,X),op_e)) = ld(op_f,mult(X,op_e)),
inference(equational,[status(thm)],[c16,c57]) ).
cnf(c270,plain,
ld(op_e,mult(rd(X,op_e),op_f)) = mult(ld(op_e,X),op_e),
inference(equational,[status(thm)],[c18,c155]) ).
cnf(c272,plain,
ld(op_d,mult(rd(X,op_d),op_e)) = mult(ld(op_d,X),op_d),
inference(equational,[status(thm)],[c18,c154]) ).
cnf(c275,plain,
mult(mult(X,Y),i(Y)) = ld(Y,ld(i(Y),X)),
inference(equational,[status(thm)],[c100,c224]) ).
cnf(c282,plain,
mult(mult(X,Y),i(X)) = rd(ld(i(X),Y),X),
inference(equational,[status(thm)],[c32,c45,c67,c224]) ).
cnf(c285,plain,
mult(i(X),mult(Y,X)) = ld(X,rd(Y,i(X))),
inference(equational,[status(thm)],[c15,c114,c170,c196,c197,c228]) ).
cnf(c305,plain,
rd(mult(X,mult(Y,Z)),mult(X,Z)) = rd(mult(X,Y),X),
inference(equational,[status(thm)],[c8,c66]) ).
cnf(c306,plain,
rd(X,mult(X,i(Y))) = rd(mult(X,Y),X),
inference(equational,[status(thm)],[c1,c5,c305]) ).
cnf(c307,plain,
rd(mult(X,i(Y)),X) = rd(X,mult(X,Y)),
inference(equational,[status(thm)],[c1,c7,c305]) ).
cnf(c311,plain,
rd(mult(X,op_e),mult(X,op_d)) = rd(mult(X,op_d),X),
inference(equational,[status(thm)],[c3,c305]) ).
cnf(c312,plain,
rd(mult(X,op_f),mult(X,op_e)) = rd(mult(X,op_e),X),
inference(equational,[status(thm)],[c4,c305]) ).
cnf(c313,plain,
ld(rd(mult(X,Y),X),X) = mult(X,i(Y)),
inference(equational,[status(thm)],[c25,c306]) ).
cnf(c314,plain,
mult(X,i(ld(X,Y))) = ld(rd(Y,X),X),
inference(equational,[status(thm)],[c16,c313]) ).
cnf(c315,plain,
mult(rd(X,mult(X,Y)),X) = mult(X,i(Y)),
inference(equational,[status(thm)],[c15,c307]) ).
cnf(c316,plain,
mult(rd(X,Y),X) = ld(rd(Y,X),X),
inference(equational,[status(thm)],[c16,c314,c315]) ).
cnf(c325,plain,
rd(mult(X,rd(Y,Z)),X) = rd(mult(X,Y),mult(X,Z)),
inference(equational,[status(thm)],[c15,c305]) ).
cnf(c326,plain,
rd(ld(rd(X,Y),Y),Y) = rd(Y,X),
inference(equational,[status(thm)],[c8,c15,c316,c325]) ).
cnf(c327,plain,
rd(ld(X,Y),Y) = rd(Y,mult(X,Y)),
inference(equational,[status(thm)],[c8,c326]) ).
cnf(c330,plain,
rd(mult(op_d,mult(X,op_d)),op_e) = rd(mult(op_d,X),op_d),
inference(equational,[status(thm)],[c3,c305]) ).
cnf(c334,plain,
rd(mult(op_e,mult(X,op_e)),op_f) = rd(mult(op_e,X),op_e),
inference(equational,[status(thm)],[c4,c305]) ).
cnf(c335,plain,
ld(X,rd(X,mult(X,Y))) = mult(i(Y),i(X)),
inference(equational,[status(thm)],[c100,c307]) ).
cnf(c347,plain,
rd(mult(rd(X,op_d),op_e),X) = rd(X,rd(X,op_d)),
inference(equational,[status(thm)],[c15,c311]) ).
cnf(c350,plain,
rd(mult(rd(X,op_e),op_f),X) = rd(X,rd(X,op_e)),
inference(equational,[status(thm)],[c15,c312]) ).
cnf(c351,plain,
rd(mult(op_f,op_d),ld(op_d,op_f)) = op_e,
inference(equational,[status(thm)],[c12,c70,c132,c158,c159,c163,c171,c347,c350]) ).
cnf(c365,plain,
mult(X,i(mult(Y,X))) = ld(ld(i(X),Y),X),
inference(equational,[status(thm)],[c59,c60,c224,c314]) ).
cnf(c369,plain,
mult(X,ld(Y,i(X))) = i(rd(mult(X,Y),X)),
inference(equational,[status(thm)],[c5,c13,c67,c162,c325,c327]) ).
cnf(c373,plain,
rd(i(X),mult(i(X),Y)) = ld(X,rd(i(Y),i(X))),
inference(equational,[status(thm)],[c114,c285,c307]) ).
cnf(c377,plain,
rd(ld(i(X),Y),i(X)) = mult(mult(X,Y),X),
inference(equational,[status(thm)],[c14,c213]) ).
cnf(c378,plain,
mult(X,ld(i(X),Y)) = ld(i(X),mult(X,Y)),
inference(equational,[status(thm)],[c162,c224,c377]) ).
cnf(c379,plain,
mult(X,i(rd(Y,i(X)))) = ld(mult(X,Y),X),
inference(equational,[status(thm)],[c162,c313]) ).
cnf(c382,plain,
mult(i(ld(X,Y)),i(X)) = ld(X,rd(X,Y)),
inference(equational,[status(thm)],[c16,c335]) ).
cnf(c383,plain,
ld(mult(X,Y),mult(mult(X,Z),Y)) = ld(Y,mult(Z,Y)),
inference(equational,[status(thm)],[c18,c30]) ).
cnf(c384,plain,
ld(X,mult(i(Y),X)) = ld(mult(Y,X),X),
inference(equational,[status(thm)],[c2,c5,c383]) ).
cnf(c385,plain,
ld(mult(i(X),Y),Y) = ld(Y,mult(X,Y)),
inference(equational,[status(thm)],[c2,c7,c383]) ).
cnf(c387,plain,
ld(mult(op_d,X),mult(op_e,X)) = ld(X,mult(op_d,X)),
inference(equational,[status(thm)],[c3,c383]) ).
cnf(c396,plain,
ld(mult(op_e,X),mult(op_f,X)) = ld(X,mult(op_e,X)),
inference(equational,[status(thm)],[c4,c383]) ).
cnf(c397,plain,
rd(X,ld(X,mult(Y,X))) = mult(i(Y),X),
inference(equational,[status(thm)],[c26,c385]) ).
cnf(c399,plain,
mult(i(rd(X,Y)),Y) = rd(Y,ld(Y,X)),
inference(equational,[status(thm)],[c15,c397]) ).
cnf(c400,plain,
mult(X,ld(mult(Y,X),X)) = mult(i(Y),X),
inference(equational,[status(thm)],[c16,c384]) ).
cnf(c401,plain,
mult(X,ld(Y,X)) = rd(X,ld(X,Y)),
inference(equational,[status(thm)],[c15,c399,c400]) ).
cnf(c403,plain,
ld(mult(X,Y),mult(Z,Y)) = ld(Y,mult(ld(X,Z),Y)),
inference(equational,[status(thm)],[c16,c383]) ).
cnf(c407,plain,
rd(X,mult(mult(Y,X),X)) = mult(i(X),i(Y)),
inference(equational,[status(thm)],[c43,c327,c384]) ).
cnf(c410,plain,
ld(X,mult(op_e,ld(op_d,X))) = ld(ld(op_d,X),X),
inference(equational,[status(thm)],[c16,c387]) ).
cnf(c414,plain,
ld(X,mult(op_f,ld(op_e,X))) = ld(ld(op_e,X),X),
inference(equational,[status(thm)],[c16,c396]) ).
cnf(c415,plain,
ld(ld(op_d,op_f),mult(op_f,op_d)) = op_e,
inference(equational,[status(thm)],[c20,c132,c158,c166,c168,c410,c414]) ).
cnf(c422,plain,
ld(op_d,mult(ld(X,op_d),op_d)) = ld(mult(X,op_d),op_e),
inference(equational,[status(thm)],[c3,c403]) ).
cnf(c429,plain,
ld(op_e,mult(ld(X,op_e),op_e)) = ld(mult(X,op_e),op_f),
inference(equational,[status(thm)],[c4,c403]) ).
cnf(c430,plain,
rd(i(X),i(op_e)) = ld(mult(op_e,X),op_f),
inference(equational,[status(thm)],[c1,c19,c120,c228,c313,c429]) ).
cnf(c431,plain,
ld(mult(op_e,i(X)),op_f) = rd(X,i(op_e)),
inference(equational,[status(thm)],[c14,c430]) ).
cnf(c432,plain,
mult(i(mult(X,Y)),X) = rd(X,rd(Y,i(X))),
inference(equational,[status(thm)],[c162,c164,c228,c399]) ).
cnf(c433,plain,
mult(mult(i(X),Y),Y) = ld(mult(i(Y),X),Y),
inference(equational,[status(thm)],[c43,c316,c397]) ).
cnf(c440,plain,
rd(ld(i(X),i(Y)),X) = ld(mult(Y,i(X)),i(X)),
inference(equational,[status(thm)],[c45,c282,c384]) ).
cnf(c449,plain,
ld(X,rd(X,ld(X,Y))) = ld(Y,X),
inference(equational,[status(thm)],[c15,c384,c399]) ).
cnf(c450,plain,
ld(mult(X,Y),X) = ld(X,rd(X,Y)),
inference(equational,[status(thm)],[c18,c449]) ).
cnf(c453,plain,
rd(X,ld(X,rd(X,Y))) = mult(X,Y),
inference(equational,[status(thm)],[c25,c401]) ).
cnf(c457,plain,
ld(mult(i(X),i(Y)),X) = mult(mult(Y,X),X),
inference(equational,[status(thm)],[c25,c407]) ).
cnf(c459,plain,
mult(i(X),i(rd(Y,X))) = rd(X,mult(Y,X)),
inference(equational,[status(thm)],[c18,c53,c407]) ).
cnf(c462,plain,
mult(i(ld(i(X),Y)),X) = rd(X,mult(Y,X)),
inference(equational,[status(thm)],[c59,c397]) ).
cnf(c464,plain,
ld(i(X),rd(Y,i(X))) = mult(X,mult(Y,X)),
inference(equational,[status(thm)],[c14,c60,c111]) ).
cnf(c465,plain,
ld(i(X),ld(X,Y)) = ld(X,ld(i(X),Y)),
inference(equational,[status(thm)],[c14,c16,c31,c32,c224,c275,c464]) ).
cnf(c466,plain,
rd(rd(mult(op_e,X),op_e),op_e) = rd(ld(i(op_e),X),op_f),
inference(equational,[status(thm)],[c16,c32,c67,c275,c334]) ).
cnf(c470,plain,
mult(op_f,ld(mult(X,op_e),op_e)) = mult(mult(op_e,i(X)),op_e),
inference(equational,[status(thm)],[c56,c384]) ).
cnf(c481,plain,
ld(X,mult(ld(Y,i(X)),X)) = i(mult(Y,X)),
inference(equational,[status(thm)],[c7,c22,c403]) ).
cnf(c482,plain,
mult(op_e,i(mult(X,op_d))) = rd(op_d,X),
inference(equational,[status(thm)],[c18,c55,c369,c399,c481]) ).
cnf(c483,plain,
ld(op_e,rd(op_d,X)) = i(mult(X,op_d)),
inference(equational,[status(thm)],[c18,c482]) ).
cnf(c485,plain,
rd(op_d,rd(X,op_d)) = mult(op_e,i(X)),
inference(equational,[status(thm)],[c15,c482]) ).
cnf(c486,plain,
mult(op_f,i(mult(X,op_e))) = rd(op_e,X),
inference(equational,[status(thm)],[c18,c56,c369,c399,c481]) ).
cnf(c487,plain,
ld(op_f,rd(op_e,X)) = i(mult(X,op_e)),
inference(equational,[status(thm)],[c18,c486]) ).
cnf(c488,plain,
rd(op_e,rd(X,op_e)) = mult(op_f,i(X)),
inference(equational,[status(thm)],[c15,c486]) ).
cnf(c490,plain,
mult(ld(X,i(Y)),Y) = ld(ld(i(Y),X),Y),
inference(equational,[status(thm)],[c16,c365,c481]) ).
cnf(c492,plain,
ld(ld(X,i(Y)),Y) = mult(Y,mult(X,Y)),
inference(equational,[status(thm)],[c8,c14,c314,c481]) ).
cnf(c494,plain,
mult(ld(X,Y),i(Y)) = ld(ld(Y,X),i(Y)),
inference(equational,[status(thm)],[c14,c490]) ).
cnf(c500,plain,
i(mult(ld(X,op_e),op_e)) = ld(op_f,X),
inference(equational,[status(thm)],[c26,c487]) ).
cnf(c501,plain,
mult(ld(X,op_e),op_e) = i(ld(op_f,X)),
inference(equational,[status(thm)],[c14,c500]) ).
cnf(c502,plain,
i(mult(ld(X,op_d),op_d)) = ld(op_e,X),
inference(equational,[status(thm)],[c26,c483]) ).
cnf(c505,plain,
mult(ld(X,op_d),op_d) = i(ld(op_e,X)),
inference(equational,[status(thm)],[c14,c502]) ).
cnf(c506,plain,
ld(mult(op_f,i(X)),op_e) = rd(X,op_e),
inference(equational,[status(thm)],[c25,c488]) ).
cnf(c508,plain,
i(mult(rd(i(X),Y),X)) = ld(X,mult(Y,X)),
inference(equational,[status(thm)],[c25,c481]) ).
cnf(c509,plain,
mult(rd(i(X),Y),X) = i(ld(X,mult(Y,X))),
inference(equational,[status(thm)],[c14,c508]) ).
cnf(c510,plain,
rd(ld(X,op_d),op_e) = i(mult(op_d,X)),
inference(equational,[status(thm)],[c5,c8,c13,c314,c325,c330,c509]) ).
cnf(c513,plain,
rd(ld(X,op_e),op_f) = i(mult(op_e,X)),
inference(equational,[status(thm)],[c5,c8,c13,c314,c325,c334,c509]) ).
cnf(c520,plain,
rd(rd(ld(X,Y),X),i(X)) = mult(i(X),Y),
inference(equational,[status(thm)],[c14,c44,c162]) ).
cnf(c535,plain,
i(ld(X,ld(Y,X))) = ld(X,mult(Y,X)),
inference(equational,[status(thm)],[c8,c31,c60,c314,c453,c509]) ).
cnf(c568,plain,
rd(X,mult(X,mult(Y,X))) = ld(Y,i(X)),
inference(equational,[status(thm)],[c8,c60,c327,c490]) ).
cnf(c574,plain,
rd(rd(X,ld(X,Y)),X) = i(rd(Y,X)),
inference(equational,[status(thm)],[c14,c16,c67,c369,c401,c490]) ).
cnf(c575,plain,
i(rd(rd(X,Y),X)) = rd(mult(X,Y),X),
inference(equational,[status(thm)],[c453,c574]) ).
cnf(c577,plain,
i(rd(mult(X,Y),X)) = rd(rd(X,Y),X),
inference(equational,[status(thm)],[c18,c574]) ).
cnf(c579,plain,
ld(X,ld(rd(Y,X),X)) = i(ld(X,Y)),
inference(equational,[status(thm)],[c8,c199,c316,c382]) ).
cnf(c581,plain,
i(ld(X,mult(Y,X))) = ld(X,ld(Y,X)),
inference(equational,[status(thm)],[c8,c579]) ).
cnf(c583,plain,
ld(mult(X,X),mult(X,mult(X,X))) = X,
inference(equational,[status(thm)],[c14,c18,c38,c78,c385]) ).
cnf(c584,plain,
rd(op_f,rd(X,i(op_e))) = mult(op_e,i(X)),
inference(equational,[status(thm)],[c26,c431]) ).
cnf(c597,plain,
rd(i(X),ld(i(X),Y)) = rd(i(mult(Y,X)),X),
inference(equational,[status(thm)],[c43,c401,c481]) ).
cnf(c598,plain,
rd(i(ld(X,Y)),X) = rd(i(X),rd(Y,X)),
inference(equational,[status(thm)],[c14,c15,c213,c228,c597]) ).
cnf(c600,plain,
rd(i(X),rd(X,Y)) = rd(ld(X,Y),X),
inference(equational,[status(thm)],[c14,c326,c579,c598]) ).
cnf(c603,plain,
rd(ld(X,ld(Y,X)),X) = rd(i(X),Y),
inference(equational,[status(thm)],[c18,c31,c581,c597]) ).
cnf(c606,plain,
mult(i(X),mult(Y,i(X))) = ld(X,rd(Y,X)),
inference(equational,[status(thm)],[c14,c60,c111]) ).
cnf(c612,plain,
ld(mult(X,op_c),ld(op_c,op_d)) = ld(op_c,mult(ld(X,op_c),op_c)),
inference(equational,[status(thm)],[c24,c403]) ).
cnf(c614,plain,
mult(rd(X,ld(X,Y)),i(X)) = i(mult(Y,i(X))),
inference(equational,[status(thm)],[c5,c22,c45,c401,c403]) ).
cnf(c619,plain,
ld(ld(X,Y),i(X)) = ld(X,i(rd(Y,X))),
inference(equational,[status(thm)],[c14,c365,c574,c606,c614]) ).
cnf(c621,plain,
mult(X,i(mult(Y,i(X)))) = rd(mult(X,X),Y),
inference(equational,[status(thm)],[c16,c67,c325,c614]) ).
cnf(c628,plain,
i(rd(ld(i(X),Y),X)) = mult(rd(X,Y),i(X)),
inference(equational,[status(thm)],[c18,c282,c614]) ).
cnf(c629,plain,
ld(X,rd(rd(X,Y),X)) = ld(Y,i(X)),
inference(equational,[status(thm)],[c60,c459,c568,c606,c628]) ).
cnf(c632,plain,
mult(mult(X,X),mult(X,Y)) = mult(X,mult(mult(X,X),Y)),
inference(equational,[status(thm)],[c18,c119,c125]) ).
cnf(c642,plain,
ld(i(op_e),ld(op_f,i(op_e))) = i(op_f),
inference(equational,[status(thm)],[c36,c80,c113,c175,c384]) ).
cnf(c647,plain,
mult(ld(op_d,mult(X,op_d)),op_d) = ld(op_d,mult(X,op_e)),
inference(equational,[status(thm)],[c8,c272]) ).
cnf(c649,plain,
i(ld(op_e,mult(X,op_d))) = ld(op_d,mult(i(X),op_e)),
inference(equational,[status(thm)],[c384,c505,c647]) ).
cnf(c651,plain,
mult(op_e,ld(op_f,mult(X,op_e))) = mult(ld(op_e,X),op_e),
inference(equational,[status(thm)],[c16,c269]) ).
cnf(c652,plain,
mult(ld(op_e,mult(X,op_e)),op_e) = ld(op_e,mult(X,op_f)),
inference(equational,[status(thm)],[c8,c270]) ).
cnf(c653,plain,
rd(op_e,mult(X,op_f)) = ld(op_e,i(X)),
inference(equational,[status(thm)],[c8,c16,c568,c619,c652]) ).
cnf(c656,plain,
mult(op_d,ld(op_e,mult(X,op_d))) = mult(ld(op_d,X),op_d),
inference(equational,[status(thm)],[c16,c263]) ).
cnf(c657,plain,
ld(ld(op_d,X),op_d) = mult(i(X),op_e),
inference(equational,[status(thm)],[c8,c16,c315,c316,c649,c656]) ).
cnf(c658,plain,
mult(i(mult(op_d,X)),op_e) = ld(X,op_d),
inference(equational,[status(thm)],[c18,c657]) ).
cnf(c660,plain,
mult(op_e,ld(mult(X,op_e),op_f)) = i(ld(op_f,X)),
inference(equational,[status(thm)],[c16,c429,c501]) ).
cnf(c661,plain,
ld(op_e,i(ld(op_f,X))) = ld(mult(X,op_e),op_f),
inference(equational,[status(thm)],[c18,c660]) ).
cnf(c662,plain,
i(ld(op_f,rd(X,op_e))) = mult(op_e,ld(X,op_f)),
inference(equational,[status(thm)],[c15,c660]) ).
cnf(c666,plain,
ld(ld(rd(X,op_d),op_d),op_e) = ld(op_d,mult(X,op_d)),
inference(equational,[status(thm)],[c25,c316,c422]) ).
cnf(c671,plain,
ld(ld(rd(X,op_e),op_e),op_f) = ld(op_e,mult(X,op_e)),
inference(equational,[status(thm)],[c25,c316,c429]) ).
cnf(c672,plain,
ld(ld(i(op_e),X),op_f) = mult(i(X),op_e),
inference(equational,[status(thm)],[c16,c18,c32,c60,c275,c440,c492,c671]) ).
cnf(c677,plain,
rd(op_f,mult(i(X),op_e)) = ld(i(op_e),X),
inference(equational,[status(thm)],[c26,c672]) ).
cnf(c678,plain,
rd(op_f,mult(X,op_e)) = ld(i(op_e),i(X)),
inference(equational,[status(thm)],[c14,c677]) ).
cnf(c679,plain,
mult(i(X),ld(X,Y)) = ld(X,mult(i(X),Y)),
inference(equational,[status(thm)],[c14,c378]) ).
cnf(c696,plain,
ld(X,rd(mult(X,X),Y)) = i(mult(Y,i(X))),
inference(equational,[status(thm)],[c18,c621]) ).
cnf(c697,plain,
i(mult(X,i(op_d))) = ld(op_d,rd(op_e,X)),
inference(equational,[status(thm)],[c3,c696]) ).
cnf(c698,plain,
i(mult(X,i(op_e))) = ld(op_e,rd(op_f,X)),
inference(equational,[status(thm)],[c4,c696]) ).
cnf(c701,plain,
rd(rd(X,mult(Y,X)),X) = i(ld(i(X),Y)),
inference(equational,[status(thm)],[c8,c462]) ).
cnf(c708,plain,
ld(X,rd(rd(Y,X),i(X))) = mult(i(X),Y),
inference(equational,[status(thm)],[c15,c111,c114,c197,c285]) ).
cnf(c710,plain,
ld(X,ld(i(X),mult(X,Y))) = ld(i(X),Y),
inference(equational,[status(thm)],[c15,c45,c164,c275]) ).
cnf(c714,plain,
rd(mult(X,op_d),i(op_e)) = ld(rd(op_d,X),op_f),
inference(equational,[status(thm)],[c431,c482]) ).
cnf(c720,plain,
rd(ld(X,ld(i(X),Y)),X) = mult(Y,i(X)),
inference(equational,[status(thm)],[c16,c44,c45,c282]) ).
cnf(c721,plain,
i(mult(op_e,ld(X,op_f))) = ld(op_f,rd(X,op_e)),
inference(equational,[status(thm)],[c14,c662]) ).
cnf(c734,plain,
i(mult(op_d,rd(op_d,X))) = rd(X,op_e),
inference(equational,[status(thm)],[c25,c510]) ).
cnf(c735,plain,
mult(op_d,rd(op_d,X)) = i(rd(X,op_e)),
inference(equational,[status(thm)],[c14,c734]) ).
cnf(c736,plain,
rd(i(ld(op_f,X)),op_e) = ld(X,op_e),
inference(equational,[status(thm)],[c16,c500,c501,c506]) ).
cnf(c737,plain,
mult(X,mult(ld(X,Y),ld(X,Z))) = mult(rd(Y,X),Z),
inference(equational,[status(thm)],[c16,c119]) ).
cnf(c738,plain,
mult(ld(X,Y),ld(X,Z)) = ld(X,mult(rd(Y,X),Z)),
inference(equational,[status(thm)],[c18,c737]) ).
cnf(c739,plain,
mult(op_c,ld(op_d,X)) = ld(op_d,mult(op_c,X)),
inference(equational,[status(thm)],[c8,c105,c738]) ).
cnf(c745,plain,
mult(op_e,ld(op_d,X)) = ld(op_d,mult(op_e,X)),
inference(equational,[status(thm)],[c121,c132,c158,c171,c738]) ).
cnf(c747,plain,
mult(op_f,ld(op_e,X)) = ld(op_e,mult(op_f,X)),
inference(equational,[status(thm)],[c8,c122,c738]) ).
cnf(c748,plain,
mult(op_d,ld(op_e,X)) = ld(op_e,mult(op_d,X)),
inference(equational,[status(thm)],[c141,c158,c163,c738]) ).
cnf(c754,plain,
mult(X,ld(mult(X,X),Y)) = ld(mult(X,X),mult(X,Y)),
inference(equational,[status(thm)],[c8,c305,c583,c738]) ).
cnf(c755,plain,
mult(op_e,ld(op_f,X)) = ld(op_f,mult(op_e,X)),
inference(equational,[status(thm)],[c4,c754]) ).
cnf(c757,plain,
mult(X,mult(ld(X,mult(Y,X)),Z)) = mult(Y,mult(X,Z)),
inference(equational,[status(thm)],[c8,c119]) ).
cnf(c758,plain,
mult(i(op_d),mult(op_e,X)) = mult(op_e,mult(i(op_d),X)),
inference(equational,[status(thm)],[c3,c34,c82,c757]) ).
cnf(c760,plain,
mult(ld(X,mult(Y,X)),Z) = ld(X,mult(Y,mult(X,Z))),
inference(equational,[status(thm)],[c18,c757]) ).
cnf(c762,plain,
mult(i(mult(op_e,X)),op_f) = ld(X,op_e),
inference(equational,[status(thm)],[c15,c513]) ).
cnf(c763,plain,
ld(ld(op_e,X),op_e) = mult(i(X),op_f),
inference(equational,[status(thm)],[c16,c762]) ).
cnf(c764,plain,
i(mult(op_e,rd(op_e,X))) = rd(X,op_f),
inference(equational,[status(thm)],[c25,c513]) ).
cnf(c767,plain,
mult(op_e,rd(op_e,X)) = i(rd(X,op_f)),
inference(equational,[status(thm)],[c14,c764]) ).
cnf(c770,plain,
rd(i(X),mult(Y,i(X))) = ld(X,rd(X,Y)),
inference(equational,[status(thm)],[c14,c382,c462]) ).
cnf(c771,plain,
rd(mult(mult(X,Y),ld(Y,Z)),Y) = mult(X,rd(Z,Y)),
inference(equational,[status(thm)],[c8,c54]) ).
cnf(c772,plain,
mult(rd(X,Y),rd(Z,Y)) = rd(mult(X,ld(Y,Z)),Y),
inference(equational,[status(thm)],[c15,c771]) ).
cnf(c773,plain,
mult(rd(X,op_d),op_e) = rd(mult(X,op_e),op_d),
inference(equational,[status(thm)],[c69,c70,c132,c158,c166,c772]) ).
cnf(c774,plain,
mult(rd(X,op_e),op_f) = rd(mult(X,op_f),op_e),
inference(equational,[status(thm)],[c73,c74,c122,c772]) ).
cnf(c777,plain,
mult(rd(X,op_f),op_e) = rd(mult(X,op_e),op_f),
inference(equational,[status(thm)],[c18,c94,c772]) ).
cnf(c778,plain,
mult(X,rd(mult(Y,Z),Y)) = rd(mult(mult(X,Y),Z),Y),
inference(equational,[status(thm)],[c18,c771]) ).
cnf(c779,plain,
rd(ld(op_e,mult(op_f,X)),op_e) = mult(op_e,rd(X,op_e)),
inference(equational,[status(thm)],[c4,c747,c771]) ).
cnf(c780,plain,
rd(ld(op_d,mult(op_e,X)),op_d) = mult(op_d,rd(X,op_d)),
inference(equational,[status(thm)],[c3,c745,c771]) ).
cnf(c781,plain,
mult(rd(X,i(op_e)),op_d) = ld(rd(op_d,X),op_f),
inference(equational,[status(thm)],[c88,c139,c714,c772]) ).
cnf(c785,plain,
mult(rd(X,i(op_f)),op_e) = rd(mult(X,op_e),i(op_f)),
inference(equational,[status(thm)],[c89,c140,c772]) ).
cnf(c791,plain,
mult(op_d,rd(ld(op_e,X),op_d)) = rd(ld(op_d,X),op_d),
inference(equational,[status(thm)],[c16,c780]) ).
cnf(c792,plain,
ld(op_d,ld(op_e,X)) = ld(op_e,ld(op_d,X)),
inference(equational,[status(thm)],[c15,c58,c791]) ).
cnf(c793,plain,
mult(op_e,rd(ld(op_f,X),op_e)) = rd(ld(op_e,X),op_e),
inference(equational,[status(thm)],[c16,c779]) ).
cnf(c794,plain,
ld(op_e,ld(op_f,X)) = ld(op_f,ld(op_e,X)),
inference(equational,[status(thm)],[c15,c57,c793]) ).
cnf(c805,plain,
rd(mult(X,ld(Y,mult(Z,Y))),Y) = mult(rd(X,Y),Z),
inference(equational,[status(thm)],[c8,c53]) ).
cnf(c807,plain,
mult(rd(X,i(op_d)),op_e) = rd(mult(X,op_e),i(op_d)),
inference(equational,[status(thm)],[c3,c34,c82,c805]) ).
cnf(c808,plain,
mult(rd(X,i(op_e)),op_f) = rd(mult(X,op_f),i(op_e)),
inference(equational,[status(thm)],[c4,c36,c82,c805]) ).
cnf(c814,plain,
rd(mult(X,Y),mult(X,ld(Z,Y))) = rd(mult(X,Z),X),
inference(equational,[status(thm)],[c16,c305]) ).
cnf(c817,plain,
i(mult(i(X),ld(Y,X))) = ld(X,rd(Y,i(X))),
inference(equational,[status(thm)],[c7,c13,c114,c285,c814]) ).
cnf(c819,plain,
rd(op_e,rd(op_d,ld(op_d,X))) = rd(mult(op_d,X),op_d),
inference(equational,[status(thm)],[c3,c401,c814]) ).
cnf(c820,plain,
rd(op_f,rd(op_e,ld(op_e,X))) = rd(mult(op_e,X),op_e),
inference(equational,[status(thm)],[c4,c401,c814]) ).
cnf(c826,plain,
ld(rd(mult(op_e,X),op_e),op_f) = rd(op_e,ld(op_e,X)),
inference(equational,[status(thm)],[c25,c820]) ).
cnf(c827,plain,
rd(mult(op_e,mult(op_e,X)),op_e) = rd(op_f,rd(op_e,X)),
inference(equational,[status(thm)],[c18,c820]) ).
cnf(c829,plain,
rd(mult(op_d,mult(op_d,X)),op_d) = rd(op_e,rd(op_d,X)),
inference(equational,[status(thm)],[c18,c819]) ).
cnf(c831,plain,
rd(i(rd(X,op_f)),op_e) = rd(op_f,mult(op_e,X)),
inference(equational,[status(thm)],[c453,c767,c820]) ).
cnf(c835,plain,
ld(i(X),i(rd(Y,X))) = rd(mult(X,X),Y),
inference(equational,[status(thm)],[c16,c224,c325,c399]) ).
cnf(c839,plain,
rd(ld(op_f,mult(X,op_e)),op_e) = ld(op_e,mult(i(op_e),X)),
inference(equational,[status(thm)],[c43,c269,c679]) ).
cnf(c852,plain,
rd(op_d,ld(op_e,mult(X,op_d))) = mult(i(ld(op_d,X)),op_d),
inference(equational,[status(thm)],[c263,c397]) ).
cnf(c854,plain,
ld(op_e,ld(op_e,mult(X,op_e))) = ld(op_f,rd(X,i(op_e))),
inference(equational,[status(thm)],[c15,c31,c196,c269,c708]) ).
cnf(c863,plain,
rd(mult(mult(op_f,X),op_e),op_f) = mult(op_f,mult(X,i(op_e))),
inference(equational,[status(thm)],[c36,c66,c777]) ).
cnf(c866,plain,
rd(op_d,ld(op_d,mult(op_e,X))) = mult(op_d,rd(i(X),op_d)),
inference(equational,[status(thm)],[c326,c450,c485,c780]) ).
cnf(c867,plain,
mult(op_d,rd(i(op_d),X)) = rd(op_d,rd(X,i(op_d))),
inference(equational,[status(thm)],[c55,c228,c581,c603,c866]) ).
cnf(c868,plain,
rd(op_e,ld(op_e,mult(op_f,X))) = mult(op_e,rd(i(X),op_e)),
inference(equational,[status(thm)],[c326,c450,c488,c779]) ).
cnf(c869,plain,
mult(op_e,rd(i(op_e),X)) = rd(op_e,rd(X,i(op_e))),
inference(equational,[status(thm)],[c56,c228,c581,c603,c868]) ).
cnf(c873,plain,
mult(i(X),rd(X,mult(X,Y))) = rd(i(Y),X),
inference(equational,[status(thm)],[c18,c44,c307]) ).
cnf(c900,plain,
mult(i(rd(X,mult(X,Y))),X) = rd(X,i(Y)),
inference(equational,[status(thm)],[c18,c315,c397]) ).
cnf(c902,plain,
mult(i(rd(X,Y)),X) = rd(X,i(ld(X,Y))),
inference(equational,[status(thm)],[c16,c900]) ).
cnf(c903,plain,
rd(rd(mult(X,Y),X),mult(Y,i(X))) = X,
inference(equational,[status(thm)],[c8,c67]) ).
cnf(c905,plain,
ld(mult(i(X),Y),ld(X,mult(Y,X))) = X,
inference(equational,[status(thm)],[c18,c31]) ).
cnf(c907,plain,
rd(mult(X,X),mult(i(Y),X)) = ld(i(X),Y),
inference(equational,[status(thm)],[c224,c400,c814]) ).
cnf(c908,plain,
rd(mult(X,X),mult(Y,X)) = ld(i(X),i(Y)),
inference(equational,[status(thm)],[c14,c907]) ).
cnf(c962,plain,
mult(mult(X,i(op_e)),op_f) = mult(mult(X,op_f),i(op_e)),
inference(equational,[status(thm)],[c30,c37,c75]) ).
cnf(c966,plain,
ld(X,rd(mult(i(X),Y),X)) = rd(ld(X,ld(X,Y)),X),
inference(equational,[status(thm)],[c14,c111,c710,c720]) ).
cnf(c971,plain,
mult(i(rd(X,op_f)),op_e) = mult(op_f,i(ld(op_e,X))),
inference(equational,[status(thm)],[c14,c25,c470,c767,c902]) ).
cnf(c972,plain,
rd(rd(rd(X,Y),Y),i(Y)) = mult(Y,rd(ld(Y,X),Y)),
inference(equational,[status(thm)],[c14,c44,c162,c170,c197]) ).
cnf(c976,plain,
mult(ld(i(X),Y),mult(X,Z)) = mult(X,mult(mult(Y,X),Z)),
inference(equational,[status(thm)],[c59,c757]) ).
cnf(c978,plain,
mult(op_e,mult(mult(X,op_e),op_e)) = mult(ld(i(op_e),X),op_f),
inference(equational,[status(thm)],[c4,c976]) ).
cnf(c979,plain,
mult(op_e,ld(i(op_f),X)) = ld(i(op_f),mult(op_e,X)),
inference(equational,[status(thm)],[c89,c140,c738]) ).
cnf(c983,plain,
mult(rd(X,Y),ld(i(Y),Z)) = rd(mult(X,mult(Z,Y)),Y),
inference(equational,[status(thm)],[c59,c805]) ).
cnf(c986,plain,
rd(mult(op_f,mult(X,op_e)),op_e) = ld(i(op_e),mult(op_e,X)),
inference(equational,[status(thm)],[c11,c378,c983]) ).
cnf(c987,plain,
mult(rd(X,op_e),i(op_f)) = rd(mult(X,i(op_f)),op_e),
inference(equational,[status(thm)],[c180,c642,c983]) ).
cnf(c993,plain,
mult(X,mult(rd(Y,i(X)),Z)) = mult(mult(X,Y),mult(X,Z)),
inference(equational,[status(thm)],[c18,c119,c162]) ).
cnf(c994,plain,
mult(mult(X,mult(Y,X)),X) = mult(mult(X,Y),mult(X,X)),
inference(equational,[status(thm)],[c164,c196,c993]) ).
cnf(c1012,plain,
mult(mult(i(X),Y),rd(Z,X)) = rd(ld(X,mult(Y,Z)),X),
inference(equational,[status(thm)],[c8,c31,c738,c771]) ).
cnf(c1014,plain,
rd(ld(op_e,mult(X,op_f)),op_e) = ld(op_e,mult(X,op_e)),
inference(equational,[status(thm)],[c11,c31,c1012]) ).
cnf(c1024,plain,
mult(mult(X,ld(i(Y),Z)),Y) = mult(mult(X,Y),mult(Z,Y)),
inference(equational,[status(thm)],[c30,c59]) ).
cnf(c1025,plain,
mult(mult(X,i(op_f)),op_e) = mult(mult(X,op_e),i(op_f)),
inference(equational,[status(thm)],[c180,c642,c1024]) ).
cnf(c1030,plain,
mult(op_d,mult(mult(op_d,X),op_d)) = mult(op_e,mult(X,op_d)),
inference(equational,[status(thm)],[c55,c59,c60,c378]) ).
cnf(c1031,plain,
rd(mult(op_e,mult(X,op_d)),op_e) = rd(op_e,rd(op_d,X)),
inference(equational,[status(thm)],[c330,c829,c1030]) ).
cnf(c1032,plain,
rd(op_e,ld(X,i(op_d))) = ld(i(op_e),mult(op_d,X)),
inference(equational,[status(thm)],[c3,c224,c568,c994,c1031]) ).
cnf(c1048,plain,
ld(op_e,ld(op_e,ld(i(op_e),X))) = ld(op_f,mult(op_e,X)),
inference(equational,[status(thm)],[c15,c32,c57,c67,c275]) ).
cnf(c1050,plain,
ld(op_f,mult(op_e,mult(op_e,X))) = ld(op_e,ld(i(op_e),X)),
inference(equational,[status(thm)],[c16,c755,c1048]) ).
cnf(c1053,plain,
mult(op_e,mult(mult(op_e,X),op_e)) = mult(op_f,mult(X,op_e)),
inference(equational,[status(thm)],[c56,c59,c60,c378]) ).
cnf(c1054,plain,
rd(mult(op_f,mult(X,op_e)),op_f) = rd(op_f,rd(op_e,X)),
inference(equational,[status(thm)],[c334,c827,c1053]) ).
cnf(c1055,plain,
rd(op_f,ld(X,i(op_e))) = ld(i(op_f),mult(op_e,X)),
inference(equational,[status(thm)],[c4,c224,c568,c994,c1054]) ).
cnf(c1057,plain,
mult(op_f,mult(ld(op_e,X),op_e)) = mult(op_e,mult(X,op_e)),
inference(equational,[status(thm)],[c16,c1053]) ).
cnf(c1060,plain,
mult(op_e,rd(ld(op_e,X),op_e)) = rd(mult(X,op_e),op_f),
inference(equational,[status(thm)],[c16,c31,c170,c197,c334,c972]) ).
cnf(c1062,plain,
ld(op_e,rd(mult(X,op_e),op_f)) = rd(ld(op_e,X),op_e),
inference(equational,[status(thm)],[c18,c1060]) ).
cnf(c1064,plain,
rd(mult(mult(X,op_f),op_e),op_f) = mult(X,op_e),
inference(equational,[status(thm)],[c16,c1014,c1060]) ).
cnf(c1066,plain,
rd(mult(mult(X,op_e),op_e),op_f) = rd(rd(X,op_e),i(op_e)),
inference(equational,[status(thm)],[c43,c170,c197,c1060]) ).
cnf(c1067,plain,
rd(op_f,ld(op_e,i(X))) = ld(i(op_f),mult(X,op_e)),
inference(equational,[status(thm)],[c227,c653,c1054,c1064]) ).
cnf(c1068,plain,
rd(i(op_f),rd(X,op_f)) = rd(op_e,rd(X,i(op_e))),
inference(equational,[status(thm)],[c501,c598,c603,c869,c1060]) ).
cnf(c1069,plain,
mult(op_d,rd(ld(op_d,X),op_d)) = rd(mult(X,op_d),op_e),
inference(equational,[status(thm)],[c16,c31,c170,c197,c330,c972]) ).
cnf(c1078,plain,
rd(i(op_e),rd(X,op_e)) = rd(op_d,rd(X,i(op_d))),
inference(equational,[status(thm)],[c505,c598,c603,c867,c1069]) ).
cnf(c1103,plain,
i(ld(op_d,rd(op_e,X))) = mult(X,i(op_d)),
inference(equational,[status(thm)],[c14,c697]) ).
cnf(c1104,plain,
i(ld(op_e,rd(op_f,X))) = mult(X,i(op_e)),
inference(equational,[status(thm)],[c14,c698]) ).
cnf(c1114,plain,
mult(X,i(rd(i(X),Y))) = ld(i(mult(X,Y)),X),
inference(equational,[status(thm)],[c8,c164,c326,c369,c379]) ).
cnf(c1124,plain,
ld(op_d,ld(op_d,mult(X,op_e))) = ld(op_e,mult(mult(X,op_d),op_d)),
inference(equational,[status(thm)],[c3,c263,c760]) ).
cnf(c1129,plain,
mult(i(mult(X,op_e)),op_e) = ld(op_e,i(ld(op_e,X))),
inference(equational,[status(thm)],[c263,c449,c505,c581,c657,c852,c1124]) ).
cnf(c1130,plain,
rd(i(ld(op_e,X)),op_f) = ld(X,i(op_e)),
inference(equational,[status(thm)],[c16,c60,c327,c334,c365,c568,c1129]) ).
cnf(c1140,plain,
ld(op_e,ld(op_e,mult(op_f,X))) = rd(rd(X,op_e),i(op_e)),
inference(equational,[status(thm)],[c4,c54,c747,c777,c1060,c1066]) ).
cnf(c1141,plain,
i(rd(rd(X,op_e),i(op_e))) = rd(ld(mult(op_e,X),op_f),op_e),
inference(equational,[status(thm)],[c170,c197,c327,c384,c407,c430,c433,c513,c1060]) ).
cnf(c1142,plain,
i(mult(i(op_e),X)) = rd(ld(X,op_f),op_e),
inference(equational,[status(thm)],[c16,c520,c1141]) ).
cnf(c1143,plain,
i(rd(ld(X,op_f),op_e)) = mult(i(op_e),X),
inference(equational,[status(thm)],[c14,c1142]) ).
cnf(c1159,plain,
ld(X,rd(rd(X,Y),i(X))) = i(mult(i(X),Y)),
inference(equational,[status(thm)],[c25,c817]) ).
cnf(c1162,plain,
mult(X,i(mult(i(X),Y))) = rd(rd(X,Y),i(X)),
inference(equational,[status(thm)],[c16,c1159]) ).
cnf(c1164,plain,
mult(ld(X,op_f),i(op_e)) = i(ld(op_e,X)),
inference(equational,[status(thm)],[c18,c100,c164,c227,c767,c971,c1050,c1142,c1162]) ).
cnf(c1171,plain,
rd(rd(mult(X,Y),X),X) = rd(X,rd(mult(X,X),Y)),
inference(equational,[status(thm)],[c67,c306,c621]) ).
cnf(c1173,plain,
rd(ld(i(op_e),X),op_f) = rd(op_e,rd(op_f,X)),
inference(equational,[status(thm)],[c4,c466,c1171]) ).
cnf(c1175,plain,
i(rd(ld(op_e,X),op_f)) = mult(rd(op_f,X),op_e),
inference(equational,[status(thm)],[c4,c14,c487,c662,c767,c826,c1171]) ).
cnf(c1185,plain,
mult(ld(op_d,rd(X,op_d)),op_d) = ld(op_e,mult(op_d,X)),
inference(equational,[status(thm)],[c15,c656,c748]) ).
cnf(c1186,plain,
ld(ld(i(op_d),X),op_d) = ld(op_e,i(rd(X,op_e))),
inference(equational,[status(thm)],[c490,c629,c735,c1185]) ).
cnf(c1188,plain,
mult(rd(op_f,rd(op_e,X)),op_e) = mult(op_e,mult(op_e,X)),
inference(equational,[status(thm)],[c15,c827]) ).
cnf(c1199,plain,
ld(op_d,mult(mult(X,op_d),op_d)) = ld(ld(X,op_d),op_e),
inference(equational,[status(thm)],[c8,c666]) ).
cnf(c1201,plain,
rd(op_f,mult(op_f,mult(X,op_e))) = rd(rd(op_e,X),op_f),
inference(equational,[status(thm)],[c307,c486]) ).
cnf(c1202,plain,
rd(ld(X,i(op_e)),op_f) = ld(mult(op_e,X),i(op_f)),
inference(equational,[status(thm)],[c4,c568,c994,c1201]) ).
cnf(c1210,plain,
ld(op_e,rd(ld(op_e,X),op_e)) = rd(ld(op_f,X),op_e),
inference(equational,[status(thm)],[c15,c44,c839]) ).
cnf(c1219,plain,
rd(ld(op_f,mult(op_e,X)),op_e) = ld(op_e,rd(X,op_e)),
inference(equational,[status(thm)],[c16,c227,c710,c755,c793]) ).
cnf(c1221,plain,
mult(ld(op_e,rd(X,op_e)),op_e) = ld(op_f,mult(op_e,X)),
inference(equational,[status(thm)],[c15,c651,c755]) ).
cnf(c1222,plain,
ld(ld(i(op_e),X),op_e) = ld(op_f,i(rd(X,op_f))),
inference(equational,[status(thm)],[c490,c629,c767,c1221]) ).
cnf(c1223,plain,
ld(op_f,mult(op_e,mult(X,op_e))) = mult(ld(op_e,X),op_e),
inference(equational,[status(thm)],[c18,c1057]) ).
cnf(c1238,plain,
rd(ld(op_e,rd(X,op_e)),op_e) = ld(op_e,rd(X,op_f)),
inference(equational,[status(thm)],[c15,c1062]) ).
cnf(c1248,plain,
rd(i(X),ld(X,rd(Y,X))) = ld(Y,X),
inference(equational,[status(thm)],[c8,c14,c111,c199,c314,c459]) ).
cnf(c1251,plain,
rd(op_d,rd(X,i(op_d))) = rd(op_f,rd(X,i(op_f))),
inference(equational,[status(thm)],[c18,c432,c763,c779,c1078,c1248]) ).
cnf(c1272,plain,
mult(rd(X,i(Y)),mult(Y,Y)) = rd(mult(X,mult(Y,Y)),i(Y)),
inference(equational,[status(thm)],[c33,c82,c805]) ).
cnf(c1288,plain,
ld(i(op_e),mult(op_d,X)) = rd(op_f,ld(X,op_d)),
inference(equational,[status(thm)],[c4,c14,c658,c908]) ).
cnf(c1292,plain,
ld(op_f,rd(X,i(op_e))) = mult(ld(op_f,X),op_e),
inference(equational,[status(thm)],[c500,c535,c854,c1129]) ).
cnf(c1297,plain,
mult(ld(op_f,X),op_e) = ld(ld(X,op_f),op_e),
inference(equational,[status(thm)],[c14,c199,c373,c568,c854,c1164,c1292]) ).
cnf(c1299,plain,
ld(i(X),rd(i(X),Y)) = rd(X,mult(Y,X)),
inference(equational,[status(thm)],[c14,c379,c450,c459]) ).
cnf(c1300,plain,
mult(mult(X,i(Y)),i(Y)) = ld(mult(Y,i(X)),i(Y)),
inference(equational,[status(thm)],[c14,c457]) ).
cnf(c1305,plain,
i(mult(rd(op_f,X),op_e)) = rd(ld(op_e,X),op_f),
inference(equational,[status(thm)],[c14,c1175]) ).
cnf(c1313,plain,
rd(mult(mult(X,op_e),i(op_f)),op_e) = mult(X,i(op_f)),
inference(equational,[status(thm)],[c80,c81,c771]) ).
cnf(c1332,plain,
rd(mult(mult(X,op_f),i(op_e)),op_f) = mult(X,i(op_e)),
inference(equational,[status(thm)],[c36,c76,c778]) ).
cnf(c1333,plain,
mult(rd(op_f,X),i(op_e)) = ld(rd(X,op_f),i(op_e)),
inference(equational,[status(thm)],[c316,c1130,c1164,c1332]) ).
cnf(c1334,plain,
rd(rd(X,op_f),i(op_e)) = mult(X,i(op_e)),
inference(equational,[status(thm)],[c14,c26,c701,c1104,c1333]) ).
cnf(c1335,plain,
mult(op_e,rd(X,op_f)) = rd(op_e,rd(op_f,X)),
inference(equational,[status(thm)],[c67,c162,c466,c1173,c1334]) ).
cnf(c1337,plain,
mult(mult(X,op_f),i(op_e)) = rd(X,i(op_e)),
inference(equational,[status(thm)],[c4,c15,c962,c1272,c1334]) ).
cnf(c1338,plain,
rd(op_f,mult(X,op_f)) = ld(op_e,rd(op_e,X)),
inference(equational,[status(thm)],[c4,c379,c450,c621,c1337]) ).
cnf(c1340,plain,
ld(op_e,ld(op_e,X)) = mult(i(op_f),X),
inference(equational,[status(thm)],[c14,c26,c433,c653,c1338]) ).
cnf(c1341,plain,
mult(op_e,mult(op_e,X)) = ld(i(op_f),X),
inference(equational,[status(thm)],[c224,c575,c1175,c1188,c1338]) ).
cnf(c1342,plain,
ld(op_e,rd(op_e,rd(op_f,X))) = rd(X,op_f),
inference(equational,[status(thm)],[c26,c770,c1333]) ).
cnf(c1343,plain,
rd(rd(X,i(op_e)),op_f) = mult(X,i(op_e)),
inference(equational,[status(thm)],[c100,c306,c584,c1342]) ).
cnf(c1345,plain,
rd(X,mult(i(Y),i(X))) = mult(X,mult(X,Y)),
inference(equational,[status(thm)],[c335,c453]) ).
cnf(c1347,plain,
rd(X,mult(Y,ld(Z,ld(Y,X)))) = rd(mult(Y,Z),Y),
inference(equational,[status(thm)],[c16,c814]) ).
cnf(c1348,plain,
rd(op_d,mult(ld(X,op_c),op_c)) = ld(i(op_c),X),
inference(equational,[status(thm)],[c16,c224,c612,c1347]) ).
cnf(c1350,plain,
ld(i(op_c),rd(op_c,X)) = rd(op_d,mult(X,op_c)),
inference(equational,[status(thm)],[c25,c1348]) ).
cnf(c1351,plain,
mult(X,ld(Y,ld(X,Z))) = ld(rd(mult(X,Y),X),Z),
inference(equational,[status(thm)],[c25,c1347]) ).
cnf(c1352,plain,
ld(op_e,ld(i(op_e),X)) = ld(op_f,ld(i(op_f),X)),
inference(equational,[status(thm)],[c4,c11,c755,c1048,c1341,c1351]) ).
cnf(c1354,plain,
mult(X,rd(ld(X,Y),X)) = rd(mult(Y,X),mult(X,X)),
inference(equational,[status(thm)],[c170,c197,c905,c972,c1347]) ).
cnf(c1355,plain,
mult(op_f,mult(X,i(op_e))) = ld(i(op_f),rd(X,op_e)),
inference(equational,[status(thm)],[c4,c779,c863,c1341,c1354]) ).
cnf(c1364,plain,
i(mult(op_e,mult(i(X),op_e))) = ld(op_e,rd(X,op_e)),
inference(equational,[status(thm)],[c4,c16,c60,c227,c487,c678,c1050,c1335,c1354]) ).
cnf(c1365,plain,
mult(op_e,mult(i(X),op_e)) = i(ld(op_e,rd(X,op_e))),
inference(equational,[status(thm)],[c14,c1364]) ).
cnf(c1366,plain,
rd(rd(X,op_e),i(op_f)) = mult(X,op_e),
inference(equational,[status(thm)],[c25,c26,c384,c598,c826,c1078,c1251,c1365]) ).
cnf(c1367,plain,
mult(mult(X,op_e),op_e) = rd(X,i(op_f)),
inference(equational,[status(thm)],[c15,c785,c1366]) ).
cnf(c1368,plain,
mult(op_f,rd(X,op_e)) = rd(op_f,rd(op_e,X)),
inference(equational,[status(thm)],[c162,c1054,c1366]) ).
cnf(c1375,plain,
rd(op_e,ld(op_e,ld(X,op_f))) = ld(op_e,mult(X,op_e)),
inference(equational,[status(thm)],[c4,c11,c401,c854,c1292,c1297,c1351]) ).
cnf(c1380,plain,
ld(rd(mult(X,Y),X),mult(X,Z)) = mult(X,ld(Y,Z)),
inference(equational,[status(thm)],[c25,c814]) ).
cnf(c1382,plain,
mult(op_f,ld(i(op_e),X)) = ld(i(op_e),mult(op_f,X)),
inference(equational,[status(thm)],[c36,c76,c1380]) ).
cnf(c1383,plain,
rd(ld(i(op_f),X),op_e) = rd(op_f,rd(op_e,X)),
inference(equational,[status(thm)],[c14,c213,c227,c228,c820,c1341,c1368,c1382]) ).
cnf(c1384,plain,
mult(X,ld(ld(X,Y),Z)) = ld(rd(Y,X),mult(X,Z)),
inference(equational,[status(thm)],[c16,c1380]) ).
cnf(c1390,plain,
ld(rd(mult(op_e,X),op_e),op_d) = mult(op_e,ld(X,i(op_d))),
inference(equational,[status(thm)],[c34,c1380]) ).
cnf(c1391,plain,
ld(rd(mult(op_f,X),op_f),op_e) = mult(op_f,ld(X,i(op_e))),
inference(equational,[status(thm)],[c36,c1380]) ).
cnf(c1394,plain,
mult(mult(X,X),ld(X,Y)) = ld(X,mult(mult(X,X),Y)),
inference(equational,[status(thm)],[c8,c305,c583,c1384]) ).
cnf(c1395,plain,
ld(op_e,ld(i(op_f),X)) = mult(op_e,X),
inference(equational,[status(thm)],[c4,c16,c1048,c1352,c1394]) ).
cnf(c1396,plain,
rd(X,ld(X,ld(X,Y))) = ld(rd(Y,X),mult(X,X)),
inference(equational,[status(thm)],[c401,c1384]) ).
cnf(c1397,plain,
ld(op_e,rd(X,i(op_f))) = ld(ld(X,op_e),op_f),
inference(equational,[status(thm)],[c4,c661,c736,c1367,c1375,c1396]) ).
cnf(c1401,plain,
ld(i(op_f),rd(X,i(op_e))) = mult(op_f,mult(X,op_e)),
inference(equational,[status(thm)],[c14,c100,c114,c285,c465,c710,c747,c1352,c1382]) ).
cnf(c1405,plain,
ld(i(op_e),mult(op_f,X)) = ld(i(op_f),mult(op_e,X)),
inference(equational,[status(thm)],[c14,c15,c43,c45,c282,c1382,c1401]) ).
cnf(c1406,plain,
ld(i(op_e),rd(op_e,X)) = i(mult(X,i(op_f))),
inference(equational,[status(thm)],[c365,c465,c486,c696,c835,c1222,c1405]) ).
cnf(c1410,plain,
ld(ld(i(op_f),X),op_e) = mult(i(X),i(op_e)),
inference(equational,[status(thm)],[c335,c449,c1395]) ).
cnf(c1411,plain,
ld(op_e,mult(X,i(op_f))) = rd(ld(op_e,X),op_f),
inference(equational,[status(thm)],[c14,c59,c111,c487,c755,c1305,c1335,c1395]) ).
cnf(c1413,plain,
mult(mult(X,op_e),i(op_f)) = rd(X,op_e),
inference(equational,[status(thm)],[c14,c16,c227,c382,c600,c1025,c1406]) ).
cnf(c1414,plain,
rd(rd(X,op_e),op_e) = mult(X,i(op_f)),
inference(equational,[status(thm)],[c1313,c1413]) ).
cnf(c1415,plain,
mult(rd(mult(X,Y),mult(X,Z)),X) = mult(X,rd(Y,Z)),
inference(equational,[status(thm)],[c15,c325]) ).
cnf(c1418,plain,
mult(rd(op_e,mult(op_d,X)),op_d) = i(rd(X,op_e)),
inference(equational,[status(thm)],[c3,c735,c1415]) ).
cnf(c1419,plain,
mult(rd(op_f,mult(op_e,X)),op_e) = i(rd(X,op_f)),
inference(equational,[status(thm)],[c4,c767,c1415]) ).
cnf(c1420,plain,
mult(rd(mult(X,Y),Z),X) = mult(X,rd(Y,ld(X,Z))),
inference(equational,[status(thm)],[c16,c1415]) ).
cnf(c1421,plain,
mult(rd(X,mult(Y,Z)),Y) = mult(Y,rd(ld(Y,X),Z)),
inference(equational,[status(thm)],[c16,c1415]) ).
cnf(c1422,plain,
mult(mult(op_e,X),i(op_f)) = rd(op_e,rd(op_f,X)),
inference(equational,[status(thm)],[c14,c100,c365,c575,c1222,c1335,c1419]) ).
cnf(c1423,plain,
rd(op_e,mult(X,op_e)) = ld(op_f,rd(op_f,X)),
inference(equational,[status(thm)],[c26,c382,c660,c1422]) ).
cnf(c1426,plain,
rd(mult(mult(op_f,X),op_f),op_e) = mult(op_f,rd(X,i(op_e))),
inference(equational,[status(thm)],[c36,c774,c1415]) ).
cnf(c1432,plain,
mult(X,rd(ld(X,i(X)),Y)) = i(rd(Y,i(X))),
inference(equational,[status(thm)],[c78,c81,c228,c509,c1415]) ).
cnf(c1438,plain,
rd(op_d,rd(op_e,mult(op_d,X))) = mult(op_e,rd(X,op_e)),
inference(equational,[status(thm)],[c14,c482,c1418]) ).
cnf(c1444,plain,
rd(op_f,ld(op_f,ld(X,op_e))) = mult(mult(op_e,X),op_f),
inference(equational,[status(thm)],[c8,c56,c128,c199,c401,c1367,c1397,c1426]) ).
cnf(c1448,plain,
mult(i(rd(X,Y)),i(Y)) = rd(i(mult(X,i(Y))),Y),
inference(equational,[status(thm)],[c14,c82,c213,c696,c1432]) ).
cnf(c1449,plain,
ld(op_e,rd(op_e,rd(X,op_f))) = rd(op_f,X),
inference(equational,[status(thm)],[c8,c111,c382,c1175,c1238,c1411,c1414,c1448]) ).
cnf(c1450,plain,
ld(X,mult(ld(rd(Y,X),Z),X)) = ld(Y,mult(Z,X)),
inference(equational,[status(thm)],[c15,c403]) ).
cnf(c1451,plain,
ld(mult(X,Y),mult(X,X)) = rd(i(Y),i(X)),
inference(equational,[status(thm)],[c228,c313,c1450]) ).
cnf(c1452,plain,
mult(ld(rd(X,Y),Z),Y) = mult(Y,ld(X,mult(Z,Y))),
inference(equational,[status(thm)],[c16,c1450]) ).
cnf(c1453,plain,
rd(i(ld(X,Y)),i(X)) = ld(Y,mult(X,X)),
inference(equational,[status(thm)],[c16,c1451]) ).
cnf(c1461,plain,
ld(X,mult(ld(Y,rd(Z,X)),X)) = ld(mult(Y,X),Z),
inference(equational,[status(thm)],[c15,c403]) ).
cnf(c1462,plain,
mult(ld(X,rd(Y,Z)),Z) = mult(Z,ld(mult(X,Z),Y)),
inference(equational,[status(thm)],[c16,c1461]) ).
cnf(c1465,plain,
ld(X,ld(ld(i(X),Y),X)) = i(mult(Y,X)),
inference(equational,[status(thm)],[c13,c22,c490,c1461]) ).
cnf(c1472,plain,
mult(i(op_e),mult(X,op_f)) = ld(ld(X,op_e),op_f),
inference(equational,[status(thm)],[c43,c195,c199,c652,c1367,c1397]) ).
cnf(c1479,plain,
ld(op_f,ld(op_e,rd(op_e,X))) = ld(op_e,i(mult(X,op_e))),
inference(equational,[status(thm)],[c327,c481,c770,c854]) ).
cnf(c1480,plain,
ld(ld(op_e,rd(op_e,X)),op_f) = mult(X,op_f),
inference(equational,[status(thm)],[c18,c449,c464,c1067,c1367,c1479]) ).
cnf(c1481,plain,
mult(ld(op_e,X),op_f) = ld(ld(X,op_e),op_f),
inference(equational,[status(thm)],[c449,c1480]) ).
cnf(c1506,plain,
mult(op_e,ld(mult(op_e,X),op_f)) = mult(mult(op_e,i(X)),op_e),
inference(equational,[status(thm)],[c14,c44,c377,c430]) ).
cnf(c1507,plain,
rd(mult(op_e,X),i(op_f)) = mult(op_e,mult(X,op_f)),
inference(equational,[status(thm)],[c14,c164,c379,c450,c1367,c1480,c1506]) ).
cnf(c1509,plain,
ld(i(op_f),mult(op_e,X)) = mult(mult(op_f,op_e),X),
inference(equational,[status(thm)],[c15,c45,c146,c282,c805,c979,c1507]) ).
cnf(c1511,plain,
rd(op_e,ld(op_e,ld(X,op_e))) = ld(i(rd(X,op_e)),op_f),
inference(equational,[status(thm)],[c401,c574,c826]) ).
cnf(c1512,plain,
ld(op_e,mult(rd(op_e,X),op_f)) = mult(i(ld(op_e,X)),op_e),
inference(equational,[status(thm)],[c316,c579,c652]) ).
cnf(c1513,plain,
i(rd(ld(op_f,X),op_e)) = mult(rd(op_e,X),op_f),
inference(equational,[status(thm)],[c16,c1210,c1365,c1512]) ).
cnf(c1514,plain,
mult(ld(X,i(op_e)),op_f) = i(ld(op_e,X)),
inference(equational,[status(thm)],[c8,c568,c1223,c1513]) ).
cnf(c1515,plain,
mult(op_f,rd(i(op_e),X)) = i(rd(X,op_e)),
inference(equational,[status(thm)],[c18,c37,c1421,c1513]) ).
cnf(c1525,plain,
mult(ld(X,rd(Y,i(X))),X) = ld(X,mult(mult(Y,X),X)),
inference(equational,[status(thm)],[c14,c31,c67,c114,c285]) ).
cnf(c1526,plain,
rd(X,ld(i(X),i(Y))) = rd(ld(i(X),Y),X),
inference(equational,[status(thm)],[c10,c14,c19,c32,c60,c227,c282,c401,c490,c710,c1300,c1420,c1525]) ).
cnf(c1528,plain,
mult(i(mult(i(X),Y)),X) = ld(Y,mult(X,X)),
inference(equational,[status(thm)],[c18,c316,c1159,c1452,c1525]) ).
cnf(c1531,plain,
ld(X,ld(X,ld(i(X),Y))) = ld(mult(X,X),mult(X,Y)),
inference(equational,[status(thm)],[c14,c15,c32,c195,c275,c754,c1462,c1525]) ).
cnf(c1532,plain,
ld(op_f,rd(op_f,rd(op_e,X))) = rd(X,op_e),
inference(equational,[status(thm)],[c4,c16,c513,c721,c1060,c1219,c1297,c1352,c1383,c1531]) ).
cnf(c1534,plain,
ld(op_f,ld(i(op_e),X)) = mult(i(op_e),X),
inference(equational,[status(thm)],[c14,c43,c397,c678,c1532]) ).
cnf(c1537,plain,
ld(op_f,i(rd(X,op_e))) = rd(i(op_e),X),
inference(equational,[status(thm)],[c26,c603,c1511,c1532]) ).
cnf(c1539,plain,
mult(op_f,mult(i(op_e),X)) = ld(i(op_e),X),
inference(equational,[status(thm)],[c16,c1534]) ).
cnf(c1540,plain,
ld(op_f,mult(X,i(op_e))) = rd(ld(op_f,X),op_e),
inference(equational,[status(thm)],[c14,c44,c59,c111,c679,c1210,c1534]) ).
cnf(c1549,plain,
ld(rd(ld(i(X),Y),X),X) = ld(i(X),i(Y)),
inference(equational,[status(thm)],[c25,c1526]) ).
cnf(c1551,plain,
ld(op_f,rd(mult(op_e,X),op_e)) = rd(ld(op_e,X),op_e),
inference(equational,[status(thm)],[c820,c1532]) ).
cnf(c1552,plain,
mult(mult(op_e,i(X)),op_e) = i(rd(ld(op_e,X),op_e)),
inference(equational,[status(thm)],[c662,c1506,c1551]) ).
cnf(c1578,plain,
rd(rd(X,op_e),i(op_e)) = rd(rd(X,op_f),i(op_f)),
inference(equational,[status(thm)],[c15,c77,c170,c197,c747,c966,c1057,c1340]) ).
cnf(c1586,plain,
ld(op_e,mult(op_f,mult(X,op_f))) = mult(ld(i(op_e),X),op_f),
inference(equational,[status(thm)],[c4,c747,c760,c978,c1057]) ).
cnf(c1590,plain,
ld(op_d,mult(rd(op_d,X),op_e)) = mult(i(ld(op_d,X)),op_d),
inference(equational,[status(thm)],[c316,c579,c647]) ).
cnf(c1627,plain,
mult(op_e,rd(mult(X,op_f),op_e)) = ld(i(op_e),mult(X,op_e)),
inference(equational,[status(thm)],[c16,c652,c747,c779,c986]) ).
cnf(c1628,plain,
mult(ld(i(op_e),X),op_f) = mult(op_e,rd(X,i(op_f))),
inference(equational,[status(thm)],[c4,c54,c60,c747,c1367,c1586,c1627]) ).
cnf(c1629,plain,
rd(rd(X,i(op_f)),op_e) = mult(X,op_e),
inference(equational,[status(thm)],[c18,c60,c1014,c1628]) ).
cnf(c1634,plain,
ld(rd(op_f,rd(op_e,X)),op_e) = mult(op_e,i(mult(op_e,X))),
inference(equational,[status(thm)],[c313,c827]) ).
cnf(c1635,plain,
ld(op_e,rd(op_f,rd(op_e,X))) = rd(ld(i(op_e),X),op_e),
inference(equational,[status(thm)],[c100,c282,c827]) ).
cnf(c1689,plain,
mult(op_f,ld(ld(X,op_f),op_e)) = rd(X,i(op_e)),
inference(equational,[status(thm)],[c4,c15,c170,c196,c197,c470,c1142,c1143,c1528]) ).
cnf(c1690,plain,
rd(rd(op_f,X),i(op_e)) = mult(op_f,ld(X,op_e)),
inference(equational,[status(thm)],[c25,c1689]) ).
cnf(c1699,plain,
ld(op_f,mult(mult(op_f,op_e),X)) = ld(i(op_e),X),
inference(equational,[status(thm)],[c224,c568,c1055,c1509,c1532]) ).
cnf(c1709,plain,
ld(ld(rd(X,op_f),op_e),op_f) = mult(i(op_e),X),
inference(equational,[status(thm)],[c708,c1397,c1578]) ).
cnf(c1712,plain,
rd(op_f,mult(i(op_e),X)) = ld(rd(X,op_f),op_e),
inference(equational,[status(thm)],[c26,c1709]) ).
cnf(c1738,plain,
ld(op_e,ld(op_d,mult(op_f,X))) = ld(i(op_d),X),
inference(equational,[status(thm)],[c4,c15,c54,c282,c747,c792,c1103,c1438,c1590]) ).
cnf(c1739,plain,
ld(i(op_d),mult(op_d,X)) = ld(op_e,mult(op_f,X)),
inference(equational,[status(thm)],[c70,c132,c158,c171,c378,c1351,c1738]) ).
cnf(c1759,plain,
mult(op_e,ld(ld(X,op_e),op_f)) = rd(X,i(op_f)),
inference(equational,[status(thm)],[c8,c155,c197,c774,c808,c1367,c1397,c1525,c1578]) ).
cnf(c1763,plain,
ld(i(op_e),ld(ld(X,op_e),op_f)) = mult(X,op_f),
inference(equational,[status(thm)],[c18,c464,c710,c1352,c1759]) ).
cnf(c1764,plain,
ld(i(op_e),ld(X,op_f)) = mult(rd(op_e,X),op_f),
inference(equational,[status(thm)],[c25,c1763]) ).
cnf(c1766,plain,
ld(i(op_e),ld(i(op_e),X)) = mult(op_f,X),
inference(equational,[status(thm)],[c10,c19,c450,c1055,c1391,c1420,c1509,c1699,c1763]) ).
cnf(c1767,plain,
mult(i(mult(op_f,X)),op_e) = ld(X,i(op_e)),
inference(equational,[status(thm)],[c60,c462,c568,c1766]) ).
cnf(c1775,plain,
mult(op_e,mult(mult(op_e,X),op_f)) = mult(mult(op_f,X),op_f),
inference(equational,[status(thm)],[c4,c164,c401,c632,c1444,c1759]) ).
cnf(c1790,plain,
mult(rd(op_e,rd(op_f,X)),op_f) = ld(i(op_e),X),
inference(equational,[status(thm)],[c25,c1764]) ).
cnf(c1794,plain,
rd(rd(mult(X,op_e),op_d),i(op_d)) = mult(op_d,ld(ld(X,op_d),op_e)),
inference(equational,[status(thm)],[c154,c197,c773,c807,c1199,c1525]) ).
cnf(c1828,plain,
i(ld(op_e,rd(X,op_f))) = mult(op_f,ld(X,op_e)),
inference(equational,[status(thm)],[c199,c316,c579,c1449,c1690]) ).
cnf(c1834,plain,
ld(X,mult(ld(i(X),Y),Z)) = mult(mult(Y,X),ld(X,Z)),
inference(equational,[status(thm)],[c59,c60,c224,c738]) ).
cnf(c1838,plain,
mult(ld(op_e,mult(op_f,X)),op_d) = mult(op_e,mult(X,op_d)),
inference(equational,[status(thm)],[c1,c19,c55,c378,c1739,c1834]) ).
cnf(c1839,plain,
mult(X,ld(op_d,op_f)) = ld(rd(op_d,X),op_f),
inference(equational,[status(thm)],[c16,c56,c132,c158,c228,c760,c781,c1838]) ).
cnf(c1859,plain,
rd(ld(op_e,i(X)),op_f) = ld(mult(X,op_e),i(op_f)),
inference(equational,[status(thm)],[c14,c16,c199,c1202,c1549]) ).
cnf(c1872,plain,
mult(X,ld(rd(Y,i(X)),Z)) = ld(mult(X,Y),mult(X,Z)),
inference(equational,[status(thm)],[c8,c164,c1380]) ).
cnf(c1879,plain,
rd(mult(mult(X,Y),i(Z)),Y) = mult(X,rd(Y,mult(Y,Z))),
inference(equational,[status(thm)],[c307,c778]) ).
cnf(c1880,plain,
i(rd(mult(op_e,X),op_f)) = rd(mult(op_f,i(X)),op_e),
inference(equational,[status(thm)],[c4,c767,c1879]) ).
cnf(c1882,plain,
mult(op_e,i(mult(op_e,X))) = rd(i(rd(X,op_e)),op_e),
inference(equational,[status(thm)],[c14,c513,c1114,c1515,c1880]) ).
cnf(c2029,plain,
ld(X,rd(mult(X,Y),mult(X,Z))) = mult(rd(Y,Z),i(X)),
inference(equational,[status(thm)],[c100,c325]) ).
cnf(c2030,plain,
ld(rd(X,i(Y)),i(Y)) = ld(Y,i(mult(Y,X))),
inference(equational,[status(thm)],[c5,c13,c316,c2029]) ).
cnf(c2043,plain,
mult(i(mult(X,Y)),i(X)) = ld(Y,ld(X,i(X))),
inference(equational,[status(thm)],[c41,c81,c111,c227,c307,c335,c465,c1450,c2030]) ).
cnf(c2048,plain,
mult(rd(X,i(op_e)),i(op_f)) = ld(op_f,rd(mult(op_f,X),op_e)),
inference(equational,[status(thm)],[c36,c2029]) ).
cnf(c2049,plain,
mult(rd(ld(op_c,op_d),X),op_c) = rd(op_d,ld(op_c,mult(X,op_c))),
inference(equational,[status(thm)],[c14,c31,c85,c1350,c2029]) ).
cnf(c2052,plain,
mult(mult(i(op_e),X),i(op_f)) = rd(ld(op_e,X),op_f),
inference(equational,[status(thm)],[c14,c44,c162,c466,c487,c820,c1173,c1305,c1368,c2048]) ).
cnf(c2071,plain,
ld(op_f,ld(rd(X,op_f),op_e)) = mult(i(X),op_e),
inference(equational,[status(thm)],[c199,c397,c770,c1068,c1712,c2052]) ).
cnf(c2080,plain,
mult(rd(X,ld(Y,Z)),i(Y)) = ld(Y,rd(mult(Y,X),Z)),
inference(equational,[status(thm)],[c16,c2029]) ).
cnf(c2087,plain,
rd(ld(op_f,i(X)),op_e) = ld(mult(X,op_f),i(op_e)),
inference(equational,[status(thm)],[c224,c1410,c1540,c1767,c2071]) ).
cnf(c2088,plain,
mult(rd(ld(X,Y),Z),i(X)) = ld(X,rd(Y,mult(X,Z))),
inference(equational,[status(thm)],[c16,c2029]) ).
cnf(c2089,plain,
rd(ld(X,rd(Y,X)),X) = ld(X,rd(Y,mult(X,X))),
inference(equational,[status(thm)],[c111,c204,c2088]) ).
cnf(c2100,plain,
rd(i(ld(i(X),Y)),X) = ld(Y,ld(X,i(X))),
inference(equational,[status(thm)],[c14,c41,c81,c1453]) ).
cnf(c2101,plain,
rd(mult(mult(X,Y),Z),ld(Z,mult(Y,Z))) = mult(X,Z),
inference(equational,[status(thm)],[c8,c30]) ).
cnf(c2102,plain,
rd(mult(X,Y),ld(Y,mult(Z,Y))) = mult(rd(X,Z),Y),
inference(equational,[status(thm)],[c15,c2101]) ).
cnf(c2103,plain,
mult(rd(rd(X,Y),Z),Y) = rd(X,ld(Y,mult(Z,Y))),
inference(equational,[status(thm)],[c15,c2102]) ).
cnf(c2104,plain,
mult(rd(X,rd(Y,Z)),Z) = rd(mult(X,Z),ld(Z,Y)),
inference(equational,[status(thm)],[c15,c2102]) ).
cnf(c2105,plain,
mult(ld(op_e,rd(X,op_f)),op_e) = ld(op_e,rd(X,op_e)),
inference(equational,[status(thm)],[c18,c74,c270,c2103]) ).
cnf(c2107,plain,
mult(op_f,i(ld(i(op_e),X))) = ld(rd(X,op_f),i(op_e)),
inference(equational,[status(thm)],[c36,c45,c282,c488,c1333,c2102]) ).
cnf(c2150,plain,
mult(ld(i(op_e),X),i(op_f)) = ld(i(op_e),rd(X,op_f)),
inference(equational,[status(thm)],[c16,c747,c986,c1368,c1414,c1635,c2105]) ).
cnf(c2152,plain,
ld(ld(X,i(op_f)),i(op_e)) = ld(i(op_f),rd(X,op_e)),
inference(equational,[status(thm)],[c14,c15,c619,c698,c1104,c1355,c1465,c1859,c2107]) ).
cnf(c2163,plain,
rd(mult(X,Y),rd(Z,i(Y))) = mult(Y,rd(ld(Y,X),Z)),
inference(equational,[status(thm)],[c162,c164,c228,c1421,c2104]) ).
cnf(c2164,plain,
mult(i(op_c),rd(op_d,X)) = rd(op_c,rd(X,op_c)),
inference(equational,[status(thm)],[c14,c42,c101,c2163]) ).
cnf(c2202,plain,
mult(X,mult(mult(Y,X),ld(X,Z))) = mult(ld(i(X),Y),Z),
inference(equational,[status(thm)],[c59,c60,c224,c737]) ).
cnf(c2203,plain,
mult(ld(i(op_e),X),i(op_e)) = mult(op_e,rd(X,op_e)),
inference(equational,[status(thm)],[c80,c1413,c2202]) ).
cnf(c2235,plain,
mult(mult(X,Y),ld(mult(Z,Y),Y)) = mult(mult(X,i(Z)),Y),
inference(equational,[status(thm)],[c30,c384]) ).
cnf(c2239,plain,
mult(mult(X,i(op_e)),i(op_f)) = mult(mult(X,i(op_f)),i(op_e)),
inference(equational,[status(thm)],[c36,c80,c2235]) ).
cnf(c2269,plain,
mult(rd(X,mult(X,Y)),mult(X,Z)) = mult(X,mult(i(Y),Z)),
inference(equational,[status(thm)],[c18,c119,c307]) ).
cnf(c2273,plain,
mult(rd(op_f,mult(op_f,X)),op_e) = ld(i(op_f),rd(i(X),op_e)),
inference(equational,[status(thm)],[c36,c1355,c2269]) ).
cnf(c2274,plain,
ld(i(op_f),rd(i(op_e),X)) = ld(op_e,rd(op_f,X)),
inference(equational,[status(thm)],[c56,c60,c432,c581,c603,c678,c698,c767,c1343,c2273]) ).
cnf(c2280,plain,
rd(mult(X,ld(mult(Y,Z),Z)),Z) = mult(rd(X,Z),i(Y)),
inference(equational,[status(thm)],[c384,c805]) ).
cnf(c2282,plain,
rd(i(rd(ld(op_e,X),op_e)),op_e) = mult(op_e,i(X)),
inference(equational,[status(thm)],[c11,c470,c1552,c2280]) ).
cnf(c2303,plain,
mult(op_c,rd(op_c,ld(op_c,X))) = rd(op_d,ld(op_c,mult(X,op_c))),
inference(equational,[status(thm)],[c24,c1420,c2049]) ).
cnf(c2304,plain,
mult(op_c,mult(op_c,mult(op_c,X))) = rd(op_d,i(X)),
inference(equational,[status(thm)],[c13,c18,c19,c335,c1345,c1421,c2303]) ).
cnf(c2305,plain,
rd(op_d,i(mult(op_d,X))) = i(rd(i(X),op_e)),
inference(equational,[status(thm)],[c136,c735,c2304]) ).
cnf(c2306,plain,
ld(rd(op_d,i(X)),op_c) = ld(X,ld(op_d,op_c)),
inference(equational,[status(thm)],[c218,c335,c450,c2043,c2304]) ).
cnf(c2355,plain,
rd(op_f,mult(op_e,mult(X,op_e))) = ld(rd(mult(op_f,X),op_e),op_e),
inference(equational,[status(thm)],[c314,c777,c831,c1140,c1578,c1629,c2282]) ).
cnf(c2409,plain,
mult(op_e,rd(rd(X,op_f),op_e)) = rd(op_e,rd(op_f,rd(X,op_e))),
inference(equational,[status(thm)],[c1422,c2150,c2203,c2239]) ).
cnf(c2550,plain,
mult(ld(ld(op_c,op_d),X),op_c) = ld(op_d,mult(op_c,mult(X,op_c))),
inference(equational,[status(thm)],[c68,c739,c1452]) ).
cnf(c2551,plain,
ld(op_c,ld(op_d,mult(op_c,X))) = ld(op_d,X),
inference(equational,[status(thm)],[c15,c97,c1461,c2550]) ).
cnf(c2569,plain,
rd(i(ld(i(op_e),X)),i(op_f)) = ld(X,op_e),
inference(equational,[status(thm)],[c18,c228,c1514,c1828,c2107]) ).
cnf(c2578,plain,
rd(ld(rd(op_d,X),op_f),op_e) = ld(rd(op_d,rd(X,op_e)),op_f),
inference(equational,[status(thm)],[c351,c415,c1839,c2104]) ).
cnf(c2614,plain,
rd(X,ld(X,rd(Y,i(X)))) = rd(i(Y),i(X)),
inference(equational,[status(thm)],[c401,c1451,c1872]) ).
cnf(c2616,plain,
rd(ld(X,rd(Y,i(X))),mult(Y,X)) = i(X),
inference(equational,[status(thm)],[c14,c114,c285,c903]) ).
cnf(c2757,plain,
ld(rd(i(op_e),X),i(op_f)) = ld(rd(op_f,X),op_e),
inference(equational,[status(thm)],[c26,c449,c1299,c1481,c2274]) ).
cnf(c2818,plain,
rd(i(rd(op_d,X)),i(op_c)) = rd(X,ld(op_c,op_d)),
inference(equational,[status(thm)],[c14,c16,c24,c600,c873,c2089,c2164]) ).
cnf(c2819,plain,
ld(i(rd(i(X),op_e)),op_f) = rd(ld(X,op_f),op_e),
inference(equational,[status(thm)],[c26,c510,c2305,c2578]) ).
cnf(c2820,plain,
ld(rd(op_f,i(X)),op_e) = ld(X,i(op_e)),
inference(equational,[status(thm)],[c15,c494,c619,c987,c1537,c2087,c2757,c2819]) ).
cnf(c2821,plain,
ld(rd(op_f,X),op_e) = ld(i(X),i(op_e)),
inference(equational,[status(thm)],[c14,c2820]) ).
cnf(c2822,plain,
ld(op_f,mult(op_e,X)) = mult(i(op_e),X),
inference(equational,[status(thm)],[c18,c60,c1450,c2821]) ).
cnf(c2825,plain,
ld(i(op_e),X) = mult(op_e,X),
inference(equational,[status(thm)],[c16,c1539,c2822]) ).
cnf(c2826,plain,
rd(X,i(op_f)) = mult(X,op_f),
inference(equational,[status(thm)],[c228,c450,c1472,c1480,c1775,c2822]) ).
cnf(c2827,plain,
ld(i(op_f),X) = mult(op_f,X),
inference(equational,[status(thm)],[c14,c15,c43,c45,c282,c2826]) ).
cnf(c2830,plain,
rd(X,i(op_e)) = mult(X,op_e),
inference(equational,[status(thm)],[c14,c16,c100,c114,c285,c2825]) ).
cnf(c2832,plain,
ld(i(ld(X,i(op_f))),op_f) = i(X),
inference(equational,[status(thm)],[c8,c80,c672,c2100,c2819]) ).
cnf(c2833,plain,
i(ld(X,i(op_f))) = rd(op_f,i(X)),
inference(equational,[status(thm)],[c26,c2832]) ).
cnf(c2840,plain,
i(rd(op_f,i(X))) = ld(X,i(op_f)),
inference(equational,[status(thm)],[c14,c2833]) ).
cnf(c2857,plain,
rd(op_e,ld(X,i(op_e))) = rd(op_f,i(X)),
inference(equational,[status(thm)],[c26,c2820]) ).
cnf(c2858,plain,
rd(mult(op_f,X),op_e) = rd(op_f,rd(op_e,X)),
inference(equational,[status(thm)],[c4,c369,c575,c577,c778,c1368,c1634,c2152,c2821,c2827,c2840,c2857]) ).
cnf(c2860,plain,
mult(mult(op_e,X),op_f) = mult(op_e,mult(X,op_f)),
inference(equational,[status(thm)],[c14,c1444,c1507,c2569,c2614,c2825]) ).
cnf(c2866,plain,
mult(op_e,rd(X,op_e)) = rd(mult(op_e,X),op_e),
inference(equational,[status(thm)],[c15,c227,c774,c1790,c2409,c2860]) ).
cnf(c2882,plain,
mult(rd(op_f,X),op_e) = mult(op_f,ld(X,op_e)),
inference(equational,[status(thm)],[c767,c826,c1175,c1238,c1506,c1552,c1828,c2866]) ).
cnf(c2887,plain,
ld(op_e,rd(op_f,X)) = i(rd(X,op_e)),
inference(equational,[status(thm)],[c15,c16,c450,c794,c1423,c1634,c1882,c2355,c2858,c2882]) ).
cnf(c2946,plain,
rd(ld(ld(X,op_d),op_e),mult(X,op_e)) = i(op_d),
inference(equational,[status(thm)],[c15,c18,c1794,c2616]) ).
cnf(c2947,plain,
rd(mult(op_d,X),mult(op_e,X)) = i(op_d),
inference(equational,[status(thm)],[c10,c14,c19,c450,c510,c1032,c1288,c1390,c1420,c2887,c2946]) ).
cnf(c2948,plain,
mult(op_e,mult(i(op_d),X)) = mult(op_d,X),
inference(equational,[status(thm)],[c15,c758,c2947]) ).
cnf(c2956,plain,
ld(op_e,i(rd(X,op_e))) = ld(op_f,rd(op_f,X)),
inference(equational,[status(thm)],[c14,c41,c79,c81,c365,c621,c869,c1186,c1423,c2830,c2948]) ).
cnf(c3538,plain,
ld(i(X),ld(op_d,op_c)) = ld(rd(op_d,X),op_c),
inference(equational,[status(thm)],[c14,c2306]) ).
cnf(c3539,plain,
mult(ld(op_d,op_c),X) = ld(op_d,mult(op_c,X)),
inference(equational,[status(thm)],[c18,c59,c1452,c3538]) ).
cnf(c4186,plain,
ld(op_c,rd(mult(op_c,X),op_d)) = i(rd(op_d,X)),
inference(equational,[status(thm)],[c15,c2080,c2818]) ).
cnf(c4187,plain,
i(mult(X,op_d)) = ld(op_d,i(X)),
inference(equational,[status(thm)],[c26,c223,c2280,c2551,c3539,c4186]) ).
cnf(c4216,plain,
ld(op_f,rd(op_f,X)) = i(X),
inference(equational,[status(thm)],[c16,c365,c1186,c2956,c4187]) ).
cnf(g1,plain,
mult(op_d,i(mult(a,op_d))) = i(a),
inference(equational,[status(thm)],[c365,c1186,c2956,c4216]) ).
cnf(g2,plain,
$false,
inference(resolution,[status(thm)],[g0,g1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP691-1 : TPTP v9.0.0. Released v4.0.0.
% 0.11/0.12 % Command : run_Leo-III %s %d THM
% 0.12/0.33 % Computer : n012.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Jul 14 08:53:04 EDT 2025
% 0.12/0.33 % CPUTime :
% 157.06/157.30 % SZS status Unsatisfiable
% 157.06/157.30 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------