FindProof---0.1.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : FindProof---0.1
% Problem  : GRP655+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300

% Computer : n010.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 : Fri Sep 25 01:27:54 PM UTC 2026

% Result   : Theorem 87.66s 13.13s
% Output   : Proof 87.66s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :  182
%            Number of leaves      :    7
% Syntax   : Number of formulae    : 1023 (1018 unt;   0 def)
%            Number of atoms       : 1028 (1027 equ)
%            Maximal formula atoms :    2 (   1 avg)
%            Number of connectives :   21 (  16   ~;   3   |;   2   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    5 (   1 avg)
%            Maximal term depth    :   11 (   2 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :    8 (   8 usr;   4 con; 0-4 aty)
%            Number of variables   : 2260 (   2 sgn  37   !;   2   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f4,axiom,
    ! [C,B,A] : mult(A,mult(B,mult(C,B))) = mult(mult(mult(A,B),C),B),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f05) ).

fof(f4_nnf,plain,
    ! [C,B,A] : mult(A,mult(B,mult(C,B))) = mult(mult(mult(A,B),C),B),
    inference(nnf_transformation,[status(thm)],[f4]) ).

fof(f4_sk,plain,
    ! [A,B,C] : mult(A,mult(B,mult(C,B))) = mult(mult(mult(A,B),C),B),
    inference(skolemisation,[status(esa)],[f4_nnf]) ).

cnf(c4,plain,
    mult(X2,mult(X1,mult(X0,X1))) = mult(mult(mult(X2,X1),X0),X1),
    inference(cnf_transformation,[status(esa)],[f4_sk]) ).

cnf(t5,plain,
    mult(mult(mult(X1,X2),X3),X2) = mult(X1,mult(X2,mult(X3,X2))),
    inference(equality_encoding,[status(esa)],[c4]) ).

cnf(t14,plain,
    mult(mult(mult(X1,X2),X3),X2) = mult(X1,mult(X2,mult(X3,X2))),
    inference(orient,[status(thm)],[t5]) ).

fof(f2,axiom,
    ! [B,A] : mult(rd(A,B),B) = A,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f03) ).

fof(f2_nnf,plain,
    ! [B,A] : mult(rd(A,B),B) = A,
    inference(nnf_transformation,[status(thm)],[f2]) ).

fof(f2_sk,plain,
    ! [A,B] : mult(rd(A,B),B) = A,
    inference(skolemisation,[status(esa)],[f2_nnf]) ).

cnf(c2,plain,
    mult(rd(X1,X0),X0) = X1,
    inference(cnf_transformation,[status(esa)],[f2_sk]) ).

cnf(t3,plain,
    mult(rd(X1,X2),X2) = X1,
    inference(equality_encoding,[status(esa)],[c2]) ).

cnf(t8,plain,
    mult(rd(X1,X2),X2) = X1,
    inference(orient,[status(thm)],[t3]) ).

cnf(t17,plain,
    mult(rd(X1,X2),mult(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
    inference(cp,[status(thm)],[t14,t8]) ).

cnf(t25,plain,
    mult(rd(X1,X2),mult(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
    inference(orient,[status(thm)],[t17]) ).

fof(f1,axiom,
    ! [B,A] : ld(A,mult(A,B)) = B,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f02) ).

fof(f1_nnf,plain,
    ! [B,A] : ld(A,mult(A,B)) = B,
    inference(nnf_transformation,[status(thm)],[f1]) ).

fof(f1_sk,plain,
    ! [A,B] : ld(A,mult(A,B)) = B,
    inference(skolemisation,[status(esa)],[f1_nnf]) ).

cnf(c1,plain,
    ld(X1,mult(X1,X0)) = X0,
    inference(cnf_transformation,[status(esa)],[f1_sk]) ).

cnf(t1,plain,
    ld(X1,mult(X1,X2)) = X2,
    inference(equality_encoding,[status(esa)],[c1]) ).

cnf(t9,plain,
    ld(X1,mult(X1,X2)) = X2,
    inference(orient,[status(thm)],[t1]) ).

cnf(t31,plain,
    mult(X1,mult(X2,X1)) = ld(rd(X3,X1),mult(mult(X3,X2),X1)),
    inference(cp,[status(thm)],[t9,t25]) ).

cnf(t71,plain,
    ld(rd(X1,X2),mult(mult(X1,X3),X2)) = mult(X2,mult(X3,X2)),
    inference(orient,[status(thm)],[t31]) ).

fof(f0,axiom,
    ! [B,A] : mult(A,ld(A,B)) = B,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f01) ).

fof(f0_nnf,plain,
    ! [B,A] : mult(A,ld(A,B)) = B,
    inference(nnf_transformation,[status(thm)],[f0]) ).

fof(f0_sk,plain,
    ! [A,B] : mult(A,ld(A,B)) = B,
    inference(skolemisation,[status(esa)],[f0_nnf]) ).

cnf(c0,plain,
    mult(X1,ld(X1,X0)) = X0,
    inference(cnf_transformation,[status(esa)],[f0_sk]) ).

cnf(t2,plain,
    mult(X1,ld(X1,X2)) = X2,
    inference(equality_encoding,[status(esa)],[c0]) ).

cnf(t7,plain,
    mult(X1,ld(X1,X2)) = X2,
    inference(orient,[status(thm)],[t2]) ).

cnf(t76,plain,
    mult(X1,mult(ld(X2,X3),X1)) = ld(rd(X2,X1),mult(X3,X1)),
    inference(cp,[status(thm)],[t71,t7]) ).

cnf(t83,plain,
    ld(rd(X1,X2),mult(X3,X2)) = mult(X2,mult(ld(X1,X3),X2)),
    inference(orient,[status(thm)],[t76]) ).

cnf(t10,plain,
    X1 = ld(rd(X2,X1),X2),
    inference(cp,[status(thm)],[t9,t8]) ).

cnf(t23,plain,
    ld(rd(X1,X2),X1) = X2,
    inference(orient,[status(thm)],[t10]) ).

cnf(t84,plain,
    mult(X1,mult(ld(mult(X2,X1),X2),X1)) = X1,
    inference(cp,[status(thm)],[t83,t23]) ).

cnf(t96,plain,
    mult(X1,mult(ld(mult(X2,X1),X2),X1)) = X1,
    inference(orient,[status(thm)],[t84]) ).

cnf(t106,plain,
    mult(ld(mult(X1,X2),X1),X2) = ld(X2,X2),
    inference(cp,[status(thm)],[t9,t96]) ).

cnf(t114,plain,
    mult(ld(mult(X1,X2),X1),X2) = ld(X2,X2),
    inference(orient,[status(thm)],[t106]) ).

cnf(t128,plain,
    mult(mult(X1,ld(mult(X2,X3),X2)),X3) = mult(rd(X1,X3),mult(X3,ld(X3,X3))),
    inference(cp,[status(thm)],[t25,t114]) ).

cnf(t221181,plain,
    mult(mult(X1,ld(mult(X2,X3),X2)),X3) = mult(rd(X1,X3),X3),
    inference(step,[status(thm)],[t128,t7]) ).

cnf(t221182,plain,
    mult(mult(X1,ld(mult(X2,X3),X2)),X3) = X1,
    inference(step,[status(thm)],[t221181,t8]) ).

cnf(t154,plain,
    mult(mult(X1,ld(mult(X2,X3),X2)),X3) = X1,
    inference(orient,[status(thm)],[t221182]) ).

cnf(t159,plain,
    rd(X1,ld(mult(X2,X3),X2)) = mult(X1,X3),
    inference(cp,[status(thm)],[t154,t8]) ).

cnf(t179,plain,
    rd(X1,ld(mult(X2,X3),X2)) = mult(X1,X3),
    inference(orient,[status(thm)],[t159]) ).

cnf(t181,plain,
    mult(X1,ld(X2,X3)) = rd(X1,ld(X3,X2)),
    inference(cp,[status(thm)],[t179,t7]) ).

cnf(t196,plain,
    mult(X1,ld(X2,X3)) = rd(X1,ld(X3,X2)),
    inference(orient,[status(thm)],[t181]) ).

fof(f3,axiom,
    ! [B,A] : rd(mult(A,B),B) = A,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f04) ).

fof(f3_nnf,plain,
    ! [B,A] : rd(mult(A,B),B) = A,
    inference(nnf_transformation,[status(thm)],[f3]) ).

fof(f3_sk,plain,
    ! [A,B] : rd(mult(A,B),B) = A,
    inference(skolemisation,[status(esa)],[f3_nnf]) ).

cnf(c3,plain,
    rd(mult(X1,X0),X0) = X1,
    inference(cnf_transformation,[status(esa)],[f3_sk]) ).

cnf(t4,plain,
    rd(mult(X1,X2),X2) = X1,
    inference(equality_encoding,[status(esa)],[c3]) ).

cnf(t12,plain,
    rd(mult(X1,X2),X2) = X1,
    inference(orient,[status(thm)],[t4]) ).

cnf(t29,plain,
    mult(mult(X1,rd(X2,X3)),X3) = mult(rd(X1,X3),mult(X3,X2)),
    inference(cp,[status(thm)],[t25,t8]) ).

cnf(t34,plain,
    mult(mult(X1,rd(X2,X3)),X3) = mult(rd(X1,X3),mult(X3,X2)),
    inference(orient,[status(thm)],[t29]) ).

cnf(t38,plain,
    mult(X1,rd(X2,X3)) = rd(mult(rd(X1,X3),mult(X3,X2)),X3),
    inference(cp,[status(thm)],[t12,t34]) ).

cnf(t399,plain,
    rd(mult(rd(X1,X2),mult(X2,X3)),X2) = mult(X1,rd(X3,X2)),
    inference(orient,[status(thm)],[t38]) ).

cnf(t119,plain,
    ld(X1,X1) = mult(ld(X2,rd(X2,X1)),X1),
    inference(cp,[status(thm)],[t114,t8]) ).

cnf(t131,plain,
    mult(ld(X1,rd(X1,X2)),X2) = ld(X2,X2),
    inference(orient,[status(thm)],[t119]) ).

cnf(t410,plain,
    mult(X1,rd(X2,ld(X3,rd(X3,X2)))) = rd(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),ld(X3,rd(X3,X2))),
    inference(cp,[status(thm)],[t399,t131]) ).

cnf(t187,plain,
    mult(X1,X2) = rd(X1,ld(X3,rd(X3,X2))),
    inference(cp,[status(thm)],[t179,t8]) ).

cnf(t216,plain,
    rd(X1,ld(X2,rd(X2,X3))) = mult(X1,X3),
    inference(orient,[status(thm)],[t187]) ).

cnf(t221187,plain,
    mult(X1,mult(X2,X2)) = rd(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),ld(X3,rd(X3,X2))),
    inference(step,[status(thm)],[t410,t216]) ).

cnf(t221188,plain,
    mult(X1,mult(X2,X2)) = mult(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
    inference(step,[status(thm)],[t221187,t216]) ).

cnf(t221189,plain,
    mult(X1,mult(X2,X2)) = mult(rd(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
    inference(step,[status(thm)],[t221188,t196]) ).

cnf(t221190,plain,
    mult(X1,mult(X2,X2)) = mult(rd(mult(X1,X2),ld(X2,X2)),X2),
    inference(step,[status(thm)],[t221189,t216]) ).

cnf(t540,plain,
    mult(rd(mult(X1,X2),ld(X2,X2)),X2) = mult(X1,mult(X2,X2)),
    inference(orient,[status(thm)],[t221190]) ).

cnf(t551,plain,
    mult(rd(X1,X2),mult(X2,X2)) = mult(rd(X1,ld(X2,X2)),X2),
    inference(cp,[status(thm)],[t540,t8]) ).

cnf(t568,plain,
    mult(rd(X1,ld(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
    inference(orient,[status(thm)],[t551]) ).

cnf(t580,plain,
    rd(X1,ld(X2,X2)) = rd(mult(rd(X1,X2),mult(X2,X2)),X2),
    inference(cp,[status(thm)],[t12,t568]) ).

cnf(t221191,plain,
    rd(X1,ld(X2,X2)) = mult(X1,rd(X2,X2)),
    inference(step,[status(thm)],[t580,t399]) ).

cnf(t591,plain,
    mult(X1,rd(X2,X2)) = rd(X1,ld(X2,X2)),
    inference(orient,[status(thm)],[t221191]) ).

cnf(t603,plain,
    rd(X1,X1) = ld(X2,rd(X2,ld(X1,X1))),
    inference(cp,[status(thm)],[t9,t591]) ).

cnf(t208,plain,
    ld(X1,X2) = ld(X3,rd(X3,ld(X2,X1))),
    inference(cp,[status(thm)],[t9,t196]) ).

cnf(t225,plain,
    ld(X1,rd(X1,ld(X2,X3))) = ld(X3,X2),
    inference(orient,[status(thm)],[t208]) ).

cnf(t221192,plain,
    rd(X1,X1) = ld(X1,X1),
    inference(step,[status(thm)],[t603,t225]) ).

cnf(t614,plain,
    ld(X1,X1) = rd(X1,X1),
    inference(orient,[status(thm)],[t221192]) ).

cnf(t597,plain,
    rd(rd(X1,rd(X2,X2)),ld(X2,X2)) = X1,
    inference(cp,[status(thm)],[t591,t8]) ).

cnf(t221207,plain,
    rd(rd(X1,rd(X2,X2)),rd(X2,X2)) = X1,
    inference(step,[status(thm)],[t597,t614]) ).

cnf(t684,plain,
    rd(rd(X1,rd(X2,X2)),rd(X2,X2)) = X1,
    inference(orient,[status(thm)],[t221207]) ).

cnf(t13,plain,
    X1 = rd(X2,ld(X1,X2)),
    inference(cp,[status(thm)],[t12,t7]) ).

cnf(t24,plain,
    rd(X1,ld(X2,X1)) = X2,
    inference(orient,[status(thm)],[t13]) ).

cnf(t619,plain,
    X1 = rd(X1,rd(X1,X1)),
    inference(cp,[status(thm)],[t24,t614]) ).

cnf(t634,plain,
    rd(X1,rd(X1,X1)) = X1,
    inference(orient,[status(thm)],[t619]) ).

cnf(t639,plain,
    mult(X1,rd(X2,rd(X1,X1))) = rd(mult(X1,mult(rd(X1,X1),X2)),rd(X1,X1)),
    inference(cp,[status(thm)],[t399,t634]) ).

cnf(t39913,plain,
    rd(mult(X1,mult(rd(X1,X1),X2)),rd(X1,X1)) = mult(X1,rd(X2,rd(X1,X1))),
    inference(orient,[status(thm)],[t639]) ).

cnf(t40026,plain,
    mult(X1,mult(rd(X1,X1),X2)) = rd(mult(X1,rd(X2,rd(X1,X1))),rd(X1,X1)),
    inference(cp,[status(thm)],[t684,t39913]) ).

cnf(t81265,plain,
    rd(mult(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = mult(X1,mult(rd(X1,X1),X2)),
    inference(orient,[status(thm)],[t40026]) ).

cnf(t42,plain,
    mult(rd(mult(X1,rd(X2,rd(X3,Y3))),Y3),mult(Y3,X3)) = mult(mult(rd(X1,rd(X3,Y3)),mult(rd(X3,Y3),X2)),Y3),
    inference(cp,[status(thm)],[t34,t34]) ).

cnf(t104691,plain,
    mult(mult(rd(X1,rd(X2,X3)),mult(rd(X2,X3),Y3)),X3) = mult(rd(mult(X1,rd(Y3,rd(X2,X3))),X3),mult(X3,X2)),
    inference(orient,[status(thm)],[t42]) ).

cnf(t635,plain,
    ld(X1,rd(X1,X2)) = rd(ld(X1,rd(X1,X2)),mult(ld(X1,rd(X1,X2)),X2)),
    inference(cp,[status(thm)],[t634,t216]) ).

cnf(t221193,plain,
    mult(ld(X1,rd(X1,X2)),X2) = rd(X2,X2),
    inference(step,[status(thm)],[t131,t614]) ).

cnf(t615,plain,
    mult(ld(X1,rd(X1,X2)),X2) = rd(X2,X2),
    inference(orient,[status(thm)],[t221193]) ).

cnf(t221260,plain,
    ld(X1,rd(X1,X2)) = rd(ld(X1,rd(X1,X2)),rd(X2,X2)),
    inference(step,[status(thm)],[t635,t615]) ).

cnf(t1664,plain,
    rd(ld(X1,rd(X1,X2)),rd(X2,X2)) = ld(X1,rd(X1,X2)),
    inference(orient,[status(thm)],[t221260]) ).

cnf(t104781,plain,
    mult(rd(mult(ld(X1,rd(X1,X2)),rd(X3,rd(X2,X2))),X2),mult(X2,X2)) = mult(mult(ld(X1,rd(X1,X2)),mult(rd(X2,X2),X3)),X2),
    inference(cp,[status(thm)],[t104691,t1664]) ).

cnf(t18,plain,
    mult(mult(X1,X2),X3) = rd(mult(X1,mult(X2,mult(X3,X2))),X2),
    inference(cp,[status(thm)],[t12,t14]) ).

cnf(t44,plain,
    rd(mult(X1,mult(X2,mult(X3,X2))),X2) = mult(mult(X1,X2),X3),
    inference(orient,[status(thm)],[t18]) ).

cnf(t51,plain,
    mult(mult(X1,X2),rd(X3,X2)) = rd(mult(X1,mult(X2,X3)),X2),
    inference(cp,[status(thm)],[t44,t8]) ).

cnf(t56,plain,
    mult(mult(X1,X2),rd(X3,X2)) = rd(mult(X1,mult(X2,X3)),X2),
    inference(orient,[status(thm)],[t51]) ).

cnf(t637,plain,
    rd(mult(X1,mult(rd(X2,X2),X2)),rd(X2,X2)) = mult(mult(X1,rd(X2,X2)),X2),
    inference(cp,[status(thm)],[t56,t634]) ).

cnf(t221213,plain,
    rd(mult(X1,X2),rd(X2,X2)) = mult(mult(X1,rd(X2,X2)),X2),
    inference(step,[status(thm)],[t637,t8]) ).

cnf(t221214,plain,
    rd(mult(X1,X2),rd(X2,X2)) = mult(rd(X1,X2),mult(X2,X2)),
    inference(step,[status(thm)],[t221213,t34]) ).

cnf(t899,plain,
    mult(rd(X1,X2),mult(X2,X2)) = rd(mult(X1,X2),rd(X2,X2)),
    inference(orient,[status(thm)],[t221214]) ).

cnf(t222117,plain,
    rd(mult(mult(ld(X1,rd(X1,X2)),rd(X3,rd(X2,X2))),X2),rd(X2,X2)) = mult(mult(ld(X1,rd(X1,X2)),mult(rd(X2,X2),X3)),X2),
    inference(step,[status(thm)],[t104781,t899]) ).

cnf(t93,plain,
    mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
    inference(cp,[status(thm)],[t83,t8]) ).

cnf(t478,plain,
    mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
    inference(orient,[status(thm)],[t93]) ).

cnf(t494,plain,
    mult(ld(X1,rd(X2,X3)),X3) = ld(X3,ld(rd(X1,X3),X2)),
    inference(cp,[status(thm)],[t9,t478]) ).

cnf(t505,plain,
    ld(X1,ld(rd(X2,X1),X3)) = mult(ld(X2,rd(X3,X1)),X1),
    inference(orient,[status(thm)],[t494]) ).

cnf(t507,plain,
    mult(ld(X1,rd(mult(rd(X1,X2),X3),X2)),X2) = ld(X2,X3),
    inference(cp,[status(thm)],[t505,t9]) ).

cnf(t3671,plain,
    mult(ld(X1,rd(mult(rd(X1,X2),X3),X2)),X2) = ld(X2,X3),
    inference(orient,[status(thm)],[t507]) ).

cnf(t3727,plain,
    ld(X1,rd(mult(rd(X1,X2),X3),X2)) = rd(ld(X2,X3),X2),
    inference(cp,[status(thm)],[t12,t3671]) ).

cnf(t3755,plain,
    ld(X1,rd(mult(rd(X1,X2),X3),X2)) = rd(ld(X2,X3),X2),
    inference(orient,[status(thm)],[t3727]) ).

cnf(t3762,plain,
    rd(ld(ld(X1,rd(X1,X2)),X3),ld(X1,rd(X1,X2))) = ld(Y3,mult(mult(rd(Y3,ld(X1,rd(X1,X2))),X3),X2)),
    inference(cp,[status(thm)],[t3755,t216]) ).

cnf(t221328,plain,
    mult(ld(ld(X1,rd(X1,X2)),X3),X2) = ld(Y3,mult(mult(rd(Y3,ld(X1,rd(X1,X2))),X3),X2)),
    inference(step,[status(thm)],[t3762,t216]) ).

cnf(t221329,plain,
    mult(ld(ld(X1,rd(X1,X2)),X3),X2) = ld(Y3,mult(mult(mult(Y3,X2),X3),X2)),
    inference(step,[status(thm)],[t221328,t216]) ).

cnf(t221330,plain,
    mult(ld(ld(X1,rd(X1,X2)),X3),X2) = ld(Y3,mult(Y3,mult(X2,mult(X3,X2)))),
    inference(step,[status(thm)],[t221329,t14]) ).

cnf(t221331,plain,
    mult(ld(ld(X1,rd(X1,X2)),X3),X2) = mult(X2,mult(X3,X2)),
    inference(step,[status(thm)],[t221330,t9]) ).

cnf(t3817,plain,
    mult(ld(ld(X1,rd(X1,X2)),X3),X2) = mult(X2,mult(X3,X2)),
    inference(orient,[status(thm)],[t221331]) ).

cnf(t3846,plain,
    mult(ld(X1,rd(X1,X2)),mult(X3,ld(X1,rd(X1,X2)))) = mult(ld(ld(Y3,mult(Y3,X2)),X3),ld(X1,rd(X1,X2))),
    inference(cp,[status(thm)],[t3817,t216]) ).

cnf(t221335,plain,
    mult(ld(X1,rd(X1,X2)),rd(X3,ld(rd(X1,X2),X1))) = mult(ld(ld(Y3,mult(Y3,X2)),X3),ld(X1,rd(X1,X2))),
    inference(step,[status(thm)],[t3846,t196]) ).

cnf(t221336,plain,
    mult(ld(X1,rd(X1,X2)),rd(X3,X2)) = mult(ld(ld(Y3,mult(Y3,X2)),X3),ld(X1,rd(X1,X2))),
    inference(step,[status(thm)],[t221335,t23]) ).

cnf(t221337,plain,
    mult(ld(X1,rd(X1,X2)),rd(X3,X2)) = rd(ld(ld(Y3,mult(Y3,X2)),X3),ld(rd(X1,X2),X1)),
    inference(step,[status(thm)],[t221336,t196]) ).

cnf(t221338,plain,
    mult(ld(X1,rd(X1,X2)),rd(X3,X2)) = rd(ld(X2,X3),ld(rd(X1,X2),X1)),
    inference(step,[status(thm)],[t221337,t9]) ).

cnf(t221339,plain,
    mult(ld(X1,rd(X1,X2)),rd(X3,X2)) = rd(ld(X2,X3),X2),
    inference(step,[status(thm)],[t221338,t23]) ).

cnf(t4017,plain,
    mult(ld(X1,rd(X1,X2)),rd(X3,X2)) = rd(ld(X2,X3),X2),
    inference(orient,[status(thm)],[t221339]) ).

cnf(t4064,plain,
    rd(ld(ld(X1,X2),X2),ld(X1,X2)) = mult(ld(X3,rd(X3,ld(X1,X2))),X1),
    inference(cp,[status(thm)],[t4017,t24]) ).

cnf(t221341,plain,
    rd(ld(ld(X1,X2),X2),ld(X1,X2)) = mult(ld(X2,X1),X1),
    inference(step,[status(thm)],[t4064,t225]) ).

cnf(t4279,plain,
    rd(ld(ld(X1,X2),X2),ld(X1,X2)) = mult(ld(X2,X1),X1),
    inference(orient,[status(thm)],[t221341]) ).

cnf(t4323,plain,
    ld(ld(X1,X2),X2) = mult(mult(ld(X2,X1),X1),ld(X1,X2)),
    inference(cp,[status(thm)],[t8,t4279]) ).

cnf(t221346,plain,
    ld(ld(X1,X2),X2) = rd(mult(ld(X2,X1),X1),ld(X2,X1)),
    inference(step,[status(thm)],[t4323,t196]) ).

cnf(t4621,plain,
    rd(mult(ld(X1,X2),X2),ld(X1,X2)) = ld(ld(X2,X1),X1),
    inference(orient,[status(thm)],[t221346]) ).

cnf(t221,plain,
    ld(X1,rd(X1,X2)) = ld(mult(X3,X2),X3),
    inference(cp,[status(thm)],[t23,t216]) ).

cnf(t349,plain,
    ld(X1,rd(X1,X2)) = ld(mult(X3,X2),X3),
    inference(orient,[status(thm)],[t221]) ).

cnf(t4672,plain,
    ld(ld(X1,mult(X1,X2)),mult(X1,X2)) = rd(mult(ld(mult(X1,X2),X1),X1),ld(X3,rd(X3,X2))),
    inference(cp,[status(thm)],[t4621,t349]) ).

cnf(t221348,plain,
    ld(X2,mult(X1,X2)) = rd(mult(ld(mult(X1,X2),X1),X1),ld(X3,rd(X3,X2))),
    inference(step,[status(thm)],[t4672,t9]) ).

cnf(t221349,plain,
    ld(X2,mult(X1,X2)) = mult(mult(ld(mult(X1,X2),X1),X1),X2),
    inference(step,[status(thm)],[t221348,t216]) ).

cnf(t221350,plain,
    ld(X2,mult(X1,X2)) = mult(mult(ld(true,rd(true,X2)),X1),X2),
    inference(step,[status(thm)],[t221349,t349]) ).

cnf(t4884,plain,
    mult(mult(ld(true,rd(true,X1)),X2),X1) = ld(X1,mult(X2,X1)),
    inference(orient,[status(thm)],[t221350]) ).

cnf(t229,plain,
    ld(X1,rd(X1,X2)) = ld(X3,rd(X3,X2)),
    inference(cp,[status(thm)],[t225,t23]) ).

cnf(t390,plain,
    ld(X1,rd(X1,X2)) = ld(X3,rd(X3,X2)),
    inference(orient,[status(thm)],[t229]) ).

cnf(t4901,plain,
    ld(X1,mult(X2,X1)) = mult(mult(ld(X3,rd(X3,X1)),X2),X1),
    inference(cp,[status(thm)],[t4884,t390]) ).

cnf(t5111,plain,
    mult(mult(ld(X1,rd(X1,X2)),X3),X2) = ld(X2,mult(X3,X2)),
    inference(orient,[status(thm)],[t4901]) ).

cnf(t222118,plain,
    rd(ld(X2,mult(rd(X3,rd(X2,X2)),X2)),rd(X2,X2)) = mult(mult(ld(X1,rd(X1,X2)),mult(rd(X2,X2),X3)),X2),
    inference(step,[status(thm)],[t222117,t5111]) ).

cnf(t221199,plain,
    mult(rd(X1,rd(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
    inference(step,[status(thm)],[t568,t614]) ).

cnf(t629,plain,
    mult(rd(X1,rd(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
    inference(rw,[status(thm)],[t221199]) ).

cnf(t782,plain,
    mult(rd(X1,rd(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
    inference(orient,[status(thm)],[t629]) ).

cnf(t221215,plain,
    mult(rd(X1,rd(X2,X2)),X2) = rd(mult(X1,X2),rd(X2,X2)),
    inference(step,[status(thm)],[t782,t899]) ).

cnf(t900,plain,
    mult(rd(X1,rd(X2,X2)),X2) = rd(mult(X1,X2),rd(X2,X2)),
    inference(orient,[status(thm)],[t221215]) ).

cnf(t222119,plain,
    rd(ld(X2,rd(mult(X3,X2),rd(X2,X2))),rd(X2,X2)) = mult(mult(ld(X1,rd(X1,X2)),mult(rd(X2,X2),X3)),X2),
    inference(step,[status(thm)],[t222118,t900]) ).

cnf(t638,plain,
    mult(ld(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),ld(X1,X2)),
    inference(cp,[status(thm)],[t505,t634]) ).

cnf(t221195,plain,
    mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
    inference(step,[status(thm)],[t591,t614]) ).

cnf(t617,plain,
    mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
    inference(orient,[status(thm)],[t221195]) ).

cnf(t221650,plain,
    rd(ld(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),ld(X1,X2)),
    inference(step,[status(thm)],[t638,t617]) ).

cnf(t39757,plain,
    rd(ld(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),ld(X1,X2)),
    inference(orient,[status(thm)],[t221650]) ).

cnf(t222120,plain,
    ld(rd(X2,X2),ld(X2,mult(X3,X2))) = mult(mult(ld(X1,rd(X1,X2)),mult(rd(X2,X2),X3)),X2),
    inference(step,[status(thm)],[t222119,t39757]) ).

cnf(t222121,plain,
    ld(rd(X2,X2),ld(X2,mult(X3,X2))) = ld(X2,mult(mult(rd(X2,X2),X3),X2)),
    inference(step,[status(thm)],[t222120,t5111]) ).

cnf(t105331,plain,
    ld(rd(X1,X1),ld(X1,mult(X2,X1))) = ld(X1,mult(mult(rd(X1,X1),X2),X1)),
    inference(orient,[status(thm)],[t222121]) ).

cnf(t123,plain,
    ld(mult(X1,X2),X1) = rd(ld(X2,X2),X2),
    inference(cp,[status(thm)],[t12,t114]) ).

cnf(t270,plain,
    ld(mult(X1,X2),X1) = rd(ld(X2,X2),X2),
    inference(orient,[status(thm)],[t123]) ).

cnf(t281,plain,
    mult(X1,X2) = rd(X1,rd(ld(X2,X2),X2)),
    inference(cp,[status(thm)],[t24,t270]) ).

cnf(t309,plain,
    rd(X1,rd(ld(X2,X2),X2)) = mult(X1,X2),
    inference(orient,[status(thm)],[t281]) ).

cnf(t221202,plain,
    rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
    inference(step,[status(thm)],[t309,t614]) ).

cnf(t631,plain,
    rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
    inference(rw,[status(thm)],[t221202]) ).

cnf(t652,plain,
    rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
    inference(orient,[status(thm)],[t631]) ).

cnf(t136,plain,
    ld(X1,rd(X1,X2)) = rd(ld(X2,X2),X2),
    inference(cp,[status(thm)],[t12,t131]) ).

cnf(t321,plain,
    ld(X1,rd(X1,X2)) = rd(ld(X2,X2),X2),
    inference(orient,[status(thm)],[t136]) ).

cnf(t221197,plain,
    ld(X1,rd(X1,X2)) = rd(rd(X2,X2),X2),
    inference(step,[status(thm)],[t321,t614]) ).

cnf(t627,plain,
    ld(X1,rd(X1,X2)) = rd(rd(X2,X2),X2),
    inference(rw,[status(thm)],[t221197]) ).

cnf(t996,plain,
    ld(X1,rd(X1,X2)) = rd(rd(X2,X2),X2),
    inference(orient,[status(thm)],[t627]) ).

cnf(t1013,plain,
    rd(mult(rd(X1,X1),X1),rd(X1,X1)) = mult(ld(X2,rd(X2,X1)),mult(X1,X1)),
    inference(cp,[status(thm)],[t899,t996]) ).

cnf(t221225,plain,
    rd(X1,rd(X1,X1)) = mult(ld(X2,rd(X2,X1)),mult(X1,X1)),
    inference(step,[status(thm)],[t1013,t8]) ).

cnf(t221226,plain,
    X1 = mult(ld(X2,rd(X2,X1)),mult(X1,X1)),
    inference(step,[status(thm)],[t221225,t634]) ).

cnf(t1025,plain,
    mult(ld(X1,rd(X1,X2)),mult(X2,X2)) = X2,
    inference(orient,[status(thm)],[t221226]) ).

cnf(t1043,plain,
    mult(X1,X1) = ld(ld(X2,rd(X2,X1)),X1),
    inference(cp,[status(thm)],[t9,t1025]) ).

cnf(t1053,plain,
    ld(ld(X1,rd(X1,X2)),X2) = mult(X2,X2),
    inference(orient,[status(thm)],[t1043]) ).

cnf(t1055,plain,
    mult(X1,X1) = ld(rd(rd(X1,X1),X1),X1),
    inference(cp,[status(thm)],[t1053,t996]) ).

cnf(t1075,plain,
    ld(rd(rd(X1,X1),X1),X1) = mult(X1,X1),
    inference(orient,[status(thm)],[t1055]) ).

cnf(t1082,plain,
    rd(rd(X1,X1),X1) = rd(X1,mult(X1,X1)),
    inference(cp,[status(thm)],[t24,t1075]) ).

cnf(t1088,plain,
    rd(rd(X1,X1),X1) = rd(X1,mult(X1,X1)),
    inference(orient,[status(thm)],[t1082]) ).

cnf(t221229,plain,
    rd(X1,rd(X2,mult(X2,X2))) = mult(X1,X2),
    inference(step,[status(thm)],[t652,t1088]) ).

cnf(t1112,plain,
    rd(X1,rd(X2,mult(X2,X2))) = mult(X1,X2),
    inference(rw,[status(thm)],[t221229]) ).

cnf(t1174,plain,
    rd(X1,rd(X2,mult(X2,X2))) = mult(X1,X2),
    inference(orient,[status(thm)],[t1112]) ).

cnf(t105339,plain,
    ld(rd(X1,mult(X1,X1)),mult(mult(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),X2),rd(X1,mult(X1,X1)))) = ld(mult(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),
    inference(cp,[status(thm)],[t105331,t1174]) ).

cnf(t87,plain,
    mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
    inference(cp,[status(thm)],[t83,t12]) ).

cnf(t430,plain,
    mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
    inference(orient,[status(thm)],[t87]) ).

cnf(t447,plain,
    mult(ld(mult(X1,X2),X3),X2) = ld(X2,ld(X1,mult(X3,X2))),
    inference(cp,[status(thm)],[t9,t430]) ).

cnf(t457,plain,
    ld(X1,ld(X2,mult(X3,X1))) = mult(ld(mult(X2,X1),X3),X1),
    inference(orient,[status(thm)],[t447]) ).

cnf(t459,plain,
    mult(ld(mult(rd(mult(X1,X2),X3),X2),X1),X2) = ld(X2,X3),
    inference(cp,[status(thm)],[t457,t23]) ).

cnf(t2852,plain,
    mult(ld(mult(rd(mult(X1,X2),X3),X2),X1),X2) = ld(X2,X3),
    inference(orient,[status(thm)],[t459]) ).

cnf(t280,plain,
    rd(X1,ld(X2,mult(X2,X3))) = mult(X1,rd(ld(X3,X3),X3)),
    inference(cp,[status(thm)],[t196,t270]) ).

cnf(t221185,plain,
    rd(X1,X3) = mult(X1,rd(ld(X3,X3),X3)),
    inference(step,[status(thm)],[t280,t9]) ).

cnf(t292,plain,
    mult(X1,rd(ld(X2,X2),X2)) = rd(X1,X2),
    inference(orient,[status(thm)],[t221185]) ).

cnf(t221203,plain,
    mult(X1,rd(rd(X2,X2),X2)) = rd(X1,X2),
    inference(step,[status(thm)],[t292,t614]) ).

cnf(t632,plain,
    mult(X1,rd(rd(X2,X2),X2)) = rd(X1,X2),
    inference(rw,[status(thm)],[t221203]) ).

cnf(t669,plain,
    mult(X1,rd(rd(X2,X2),X2)) = rd(X1,X2),
    inference(orient,[status(thm)],[t632]) ).

cnf(t221228,plain,
    mult(X1,rd(X2,mult(X2,X2))) = rd(X1,X2),
    inference(step,[status(thm)],[t669,t1088]) ).

cnf(t1111,plain,
    mult(X1,rd(X2,mult(X2,X2))) = rd(X1,X2),
    inference(rw,[status(thm)],[t221228]) ).

cnf(t1132,plain,
    mult(X1,rd(X2,mult(X2,X2))) = rd(X1,X2),
    inference(orient,[status(thm)],[t1111]) ).

cnf(t2856,plain,
    ld(rd(X1,mult(X1,X1)),X2) = rd(ld(mult(rd(mult(X3,rd(X1,mult(X1,X1))),X2),rd(X1,mult(X1,X1))),X3),X1),
    inference(cp,[status(thm)],[t2852,t1132]) ).

cnf(t221294,plain,
    ld(rd(X1,mult(X1,X1)),X2) = rd(ld(rd(rd(mult(X3,rd(X1,mult(X1,X1))),X2),X1),X3),X1),
    inference(step,[status(thm)],[t2856,t1132]) ).

cnf(t221295,plain,
    ld(rd(X1,mult(X1,X1)),X2) = rd(ld(rd(rd(rd(X3,X1),X2),X1),X3),X1),
    inference(step,[status(thm)],[t221294,t1132]) ).

cnf(t482,plain,
    ld(rd(rd(rd(X1,X2),X3),X2),X1) = mult(X2,mult(X3,X2)),
    inference(cp,[status(thm)],[t478,t23]) ).

cnf(t1511,plain,
    ld(rd(rd(rd(X1,X2),X3),X2),X1) = mult(X2,mult(X3,X2)),
    inference(orient,[status(thm)],[t482]) ).

cnf(t1542,plain,
    rd(rd(rd(X1,X2),X3),X2) = rd(X1,mult(X2,mult(X3,X2))),
    inference(cp,[status(thm)],[t24,t1511]) ).

cnf(t1548,plain,
    rd(rd(rd(X1,X2),X3),X2) = rd(X1,mult(X2,mult(X3,X2))),
    inference(orient,[status(thm)],[t1542]) ).

cnf(t221296,plain,
    ld(rd(X1,mult(X1,X1)),X2) = rd(ld(rd(X3,mult(X1,mult(X2,X1))),X3),X1),
    inference(step,[status(thm)],[t221295,t1548]) ).

cnf(t221297,plain,
    ld(rd(X1,mult(X1,X1)),X2) = rd(mult(X1,mult(X2,X1)),X1),
    inference(step,[status(thm)],[t221296,t23]) ).

cnf(t2930,plain,
    ld(rd(X1,mult(X1,X1)),X2) = rd(mult(X1,mult(X2,X1)),X1),
    inference(orient,[status(thm)],[t221297]) ).

cnf(t222122,plain,
    rd(mult(X1,mult(mult(mult(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),X2),rd(X1,mult(X1,X1))),X1)),X1) = ld(mult(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),
    inference(step,[status(thm)],[t105339,t2930]) ).

cnf(t222123,plain,
    rd(mult(X1,mult(rd(mult(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),X2),X1),X1)),X1) = ld(mult(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),
    inference(step,[status(thm)],[t222122,t1132]) ).

cnf(t222124,plain,
    rd(mult(X1,mult(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),X2)),X1) = ld(mult(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),
    inference(step,[status(thm)],[t222123,t8]) ).

cnf(t222125,plain,
    rd(mult(X1,mult(mult(rd(X1,mult(X1,X1)),X1),X2)),X1) = ld(mult(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),
    inference(step,[status(thm)],[t222124,t1174]) ).

cnf(t1582,plain,
    rd(rd(X1,X2),X3) = mult(rd(X1,mult(X2,mult(X3,X2))),X2),
    inference(cp,[status(thm)],[t8,t1548]) ).

cnf(t2564,plain,
    mult(rd(X1,mult(X2,mult(X3,X2))),X2) = rd(rd(X1,X2),X3),
    inference(orient,[status(thm)],[t1582]) ).

cnf(t2596,plain,
    rd(rd(X1,X2),rd(X3,X2)) = mult(rd(X1,mult(X2,X3)),X2),
    inference(cp,[status(thm)],[t2564,t8]) ).

cnf(t2624,plain,
    mult(rd(X1,mult(X2,X3)),X2) = rd(rd(X1,X2),rd(X3,X2)),
    inference(orient,[status(thm)],[t2596]) ).

cnf(t222126,plain,
    rd(mult(X1,mult(rd(rd(X1,X1),rd(X1,X1)),X2)),X1) = ld(mult(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),
    inference(step,[status(thm)],[t222125,t2624]) ).

cnf(t902,plain,
    rd(mult(X1,rd(rd(X2,X2),X2)),rd(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))) = mult(mult(X1,X2),mult(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))),
    inference(cp,[status(thm)],[t899,t652]) ).

cnf(t221218,plain,
    rd(rd(X1,X2),rd(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))) = mult(mult(X1,X2),mult(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))),
    inference(step,[status(thm)],[t902,t669]) ).

cnf(t221219,plain,
    rd(rd(X1,X2),mult(rd(rd(X2,X2),X2),X2)) = mult(mult(X1,X2),mult(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))),
    inference(step,[status(thm)],[t221218,t652]) ).

cnf(t221220,plain,
    rd(rd(X1,X2),rd(X2,X2)) = mult(mult(X1,X2),mult(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))),
    inference(step,[status(thm)],[t221219,t8]) ).

cnf(t221221,plain,
    rd(rd(X1,X2),rd(X2,X2)) = mult(mult(X1,X2),rd(rd(rd(X2,X2),X2),X2)),
    inference(step,[status(thm)],[t221220,t669]) ).

cnf(t221222,plain,
    rd(rd(X1,X2),rd(X2,X2)) = rd(mult(X1,mult(X2,rd(rd(X2,X2),X2))),X2),
    inference(step,[status(thm)],[t221221,t56]) ).

cnf(t221223,plain,
    rd(rd(X1,X2),rd(X2,X2)) = rd(mult(X1,rd(X2,X2)),X2),
    inference(step,[status(thm)],[t221222,t669]) ).

cnf(t221224,plain,
    rd(rd(X1,X2),rd(X2,X2)) = rd(rd(X1,rd(X2,X2)),X2),
    inference(step,[status(thm)],[t221223,t617]) ).

cnf(t964,plain,
    rd(rd(X1,rd(X2,X2)),X2) = rd(rd(X1,X2),rd(X2,X2)),
    inference(orient,[status(thm)],[t221224]) ).

cnf(t965,plain,
    rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
    inference(cp,[status(thm)],[t964,t634]) ).

cnf(t989,plain,
    rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
    inference(orient,[status(thm)],[t965]) ).

cnf(t222127,plain,
    rd(mult(X1,mult(rd(X1,X1),X2)),X1) = ld(mult(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),
    inference(step,[status(thm)],[t222126,t989]) ).

cnf(t222128,plain,
    rd(mult(X1,mult(rd(X1,X1),X2)),X1) = ld(rd(rd(X1,X1),rd(X1,X1)),ld(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),
    inference(step,[status(thm)],[t222127,t2624]) ).

cnf(t222129,plain,
    rd(mult(X1,mult(rd(X1,X1),X2)),X1) = ld(rd(X1,X1),ld(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),
    inference(step,[status(thm)],[t222128,t989]) ).

cnf(t222130,plain,
    rd(mult(X1,mult(rd(X1,X1),X2)),X1) = ld(rd(X1,X1),rd(mult(X1,mult(mult(X2,rd(X1,mult(X1,X1))),X1)),X1)),
    inference(step,[status(thm)],[t222129,t2930]) ).

cnf(t222131,plain,
    rd(mult(X1,mult(rd(X1,X1),X2)),X1) = ld(rd(X1,X1),rd(mult(X1,mult(rd(X2,X1),X1)),X1)),
    inference(step,[status(thm)],[t222130,t1132]) ).

cnf(t222132,plain,
    rd(mult(X1,mult(rd(X1,X1),X2)),X1) = ld(rd(X1,X1),rd(mult(X1,X2),X1)),
    inference(step,[status(thm)],[t222131,t8]) ).

cnf(t105627,plain,
    ld(rd(X1,X1),rd(mult(X1,X2),X1)) = rd(mult(X1,mult(rd(X1,X1),X2)),X1),
    inference(orient,[status(thm)],[t222132]) ).

cnf(t105651,plain,
    rd(mult(X1,mult(rd(X1,X1),mult(X1,mult(X2,X1)))),X1) = ld(rd(X1,X1),mult(mult(X1,X1),X2)),
    inference(cp,[status(thm)],[t105627,t44]) ).

cnf(t222138,plain,
    rd(mult(X1,mult(mult(X1,X2),X1)),X1) = ld(rd(X1,X1),mult(mult(X1,X1),X2)),
    inference(step,[status(thm)],[t105651,t25]) ).

cnf(t106492,plain,
    ld(rd(X1,X1),mult(mult(X1,X1),X2)) = rd(mult(X1,mult(mult(X1,X2),X1)),X1),
    inference(orient,[status(thm)],[t222138]) ).

cnf(t106590,plain,
    rd(mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1)))),rd(X1,mult(X1,X1))) = ld(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),mult(rd(rd(X1,mult(X1,X1)),X1),X2)),
    inference(cp,[status(thm)],[t106492,t1132]) ).

cnf(t222150,plain,
    mult(mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1)))),X1) = ld(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),mult(rd(rd(X1,mult(X1,X1)),X1),X2)),
    inference(step,[status(thm)],[t106590,t1174]) ).

cnf(t3822,plain,
    mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))) = rd(ld(ld(X3,rd(X3,rd(X1,mult(X1,X1)))),X2),X1),
    inference(cp,[status(thm)],[t3817,t1132]) ).

cnf(t221332,plain,
    mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(ld(X3,rd(X3,rd(X1,mult(X1,X1)))),X2),X1),
    inference(step,[status(thm)],[t3822,t1132]) ).

cnf(t221333,plain,
    mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(ld(X3,mult(X3,X1)),X2),X1),
    inference(step,[status(thm)],[t221332,t1174]) ).

cnf(t221334,plain,
    mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(X1,X2),X1),
    inference(step,[status(thm)],[t221333,t9]) ).

cnf(t3906,plain,
    mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(X1,X2),X1),
    inference(orient,[status(thm)],[t221334]) ).

cnf(t3936,plain,
    rd(ld(X1,mult(X2,X1)),X1) = mult(rd(X1,mult(X1,X1)),X2),
    inference(cp,[status(thm)],[t3906,t12]) ).

cnf(t3965,plain,
    mult(rd(X1,mult(X1,X1)),X2) = rd(ld(X1,mult(X2,X1)),X1),
    inference(orient,[status(thm)],[t3936]) ).

cnf(t222151,plain,
    mult(rd(ld(X1,mult(mult(mult(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1))),X1)),X1),X1) = ld(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),mult(rd(rd(X1,mult(X1,X1)),X1),X2)),
    inference(step,[status(thm)],[t222150,t3965]) ).

cnf(t222152,plain,
    ld(X1,mult(mult(mult(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1))),X1)) = ld(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),mult(rd(rd(X1,mult(X1,X1)),X1),X2)),
    inference(step,[status(thm)],[t222151,t8]) ).

cnf(t222153,plain,
    ld(X1,mult(rd(mult(rd(X1,mult(X1,X1)),X2),X1),X1)) = ld(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),mult(rd(rd(X1,mult(X1,X1)),X1),X2)),
    inference(step,[status(thm)],[t222152,t1132]) ).

cnf(t222154,plain,
    ld(X1,mult(rd(X1,mult(X1,X1)),X2)) = ld(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),mult(rd(rd(X1,mult(X1,X1)),X1),X2)),
    inference(step,[status(thm)],[t222153,t8]) ).

cnf(t222155,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),mult(rd(rd(X1,mult(X1,X1)),X1),X2)),
    inference(step,[status(thm)],[t222154,t3965]) ).

cnf(t222156,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(mult(rd(X1,mult(X1,X1)),X1),mult(rd(rd(X1,mult(X1,X1)),X1),X2)),
    inference(step,[status(thm)],[t222155,t1174]) ).

cnf(t222157,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(rd(rd(X1,X1),rd(X1,X1)),mult(rd(rd(X1,mult(X1,X1)),X1),X2)),
    inference(step,[status(thm)],[t222156,t2624]) ).

cnf(t222158,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(rd(X1,X1),mult(rd(rd(X1,mult(X1,X1)),X1),X2)),
    inference(step,[status(thm)],[t222157,t989]) ).

cnf(t1550,plain,
    rd(X1,mult(X2,mult(rd(X2,X2),X2))) = rd(rd(rd(X1,X2),X2),rd(X2,X2)),
    inference(cp,[status(thm)],[t1548,t964]) ).

cnf(t221290,plain,
    rd(X1,mult(X2,X2)) = rd(rd(rd(X1,X2),X2),rd(X2,X2)),
    inference(step,[status(thm)],[t1550,t8]) ).

cnf(t2329,plain,
    rd(rd(rd(X1,X2),X2),rd(X2,X2)) = rd(X1,mult(X2,X2)),
    inference(orient,[status(thm)],[t221290]) ).

cnf(t2356,plain,
    rd(rd(X1,X2),mult(X2,mult(rd(X2,X2),X2))) = rd(rd(X1,mult(X2,X2)),X2),
    inference(cp,[status(thm)],[t1548,t2329]) ).

cnf(t221291,plain,
    rd(rd(X1,X2),mult(X2,X2)) = rd(rd(X1,mult(X2,X2)),X2),
    inference(step,[status(thm)],[t2356,t8]) ).

cnf(t2378,plain,
    rd(rd(X1,mult(X2,X2)),X2) = rd(rd(X1,X2),mult(X2,X2)),
    inference(orient,[status(thm)],[t221291]) ).

cnf(t222159,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(rd(X1,X1),mult(rd(rd(X1,X1),mult(X1,X1)),X2)),
    inference(step,[status(thm)],[t222158,t2378]) ).

cnf(t1553,plain,
    rd(X1,mult(X1,mult(X1,X1))) = rd(rd(X1,mult(X1,X1)),X1),
    inference(cp,[status(thm)],[t1548,t1088]) ).

cnf(t137,plain,
    X1 = ld(ld(X2,rd(X2,X1)),ld(X1,X1)),
    inference(cp,[status(thm)],[t9,t131]) ).

cnf(t233,plain,
    ld(ld(X1,rd(X1,X2)),ld(X2,X2)) = X2,
    inference(orient,[status(thm)],[t137]) ).

cnf(t221204,plain,
    ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
    inference(step,[status(thm)],[t233,t614]) ).

cnf(t633,plain,
    ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
    inference(rw,[status(thm)],[t221204]) ).

cnf(t694,plain,
    ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
    inference(orient,[status(thm)],[t633]) ).

cnf(t697,plain,
    rd(rd(X1,X1),X1) = ld(ld(X2,mult(X2,X1)),rd(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1))),
    inference(cp,[status(thm)],[t694,t652]) ).

cnf(t221208,plain,
    rd(rd(X1,X1),X1) = ld(X1,rd(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1))),
    inference(step,[status(thm)],[t697,t9]) ).

cnf(t221209,plain,
    rd(rd(X1,X1),X1) = ld(X1,mult(rd(rd(X1,X1),X1),X1)),
    inference(step,[status(thm)],[t221208,t652]) ).

cnf(t221210,plain,
    rd(rd(X1,X1),X1) = ld(X1,rd(X1,X1)),
    inference(step,[status(thm)],[t221209,t8]) ).

cnf(t751,plain,
    ld(X1,rd(X1,X1)) = rd(rd(X1,X1),X1),
    inference(orient,[status(thm)],[t221210]) ).

cnf(t785,plain,
    mult(rd(X1,X1),mult(X1,X1)) = mult(X1,X1),
    inference(cp,[status(thm)],[t782,t634]) ).

cnf(t807,plain,
    mult(rd(X1,X1),mult(X1,X1)) = mult(X1,X1),
    inference(orient,[status(thm)],[t785]) ).

cnf(t815,plain,
    rd(X1,X1) = rd(mult(X1,X1),mult(X1,X1)),
    inference(cp,[status(thm)],[t12,t807]) ).

cnf(t825,plain,
    rd(mult(X1,X1),mult(X1,X1)) = rd(X1,X1),
    inference(orient,[status(thm)],[t815]) ).

cnf(t834,plain,
    rd(rd(mult(X1,X1),mult(X1,X1)),mult(X1,X1)) = ld(mult(X1,X1),rd(X1,X1)),
    inference(cp,[status(thm)],[t751,t825]) ).

cnf(t221217,plain,
    rd(rd(X1,X1),mult(X1,X1)) = ld(mult(X1,X1),rd(X1,X1)),
    inference(step,[status(thm)],[t834,t825]) ).

cnf(t928,plain,
    ld(mult(X1,X1),rd(X1,X1)) = rd(rd(X1,X1),mult(X1,X1)),
    inference(orient,[status(thm)],[t221217]) ).

cnf(t468,plain,
    mult(ld(mult(X1,X2),rd(X3,X2)),X2) = ld(X2,ld(X1,X3)),
    inference(cp,[status(thm)],[t457,t8]) ).

cnf(t1370,plain,
    mult(ld(mult(X1,X2),rd(X3,X2)),X2) = ld(X2,ld(X1,X3)),
    inference(orient,[status(thm)],[t468]) ).

cnf(t1413,plain,
    ld(mult(X1,X2),rd(X3,X2)) = rd(ld(X2,ld(X1,X3)),X2),
    inference(cp,[status(thm)],[t12,t1370]) ).

cnf(t1429,plain,
    ld(mult(X1,X2),rd(X3,X2)) = rd(ld(X2,ld(X1,X3)),X2),
    inference(orient,[status(thm)],[t1413]) ).

cnf(t221249,plain,
    rd(ld(X1,ld(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
    inference(step,[status(thm)],[t928,t1429]) ).

cnf(t221250,plain,
    rd(ld(X1,rd(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
    inference(step,[status(thm)],[t221249,t614]) ).

cnf(t1479,plain,
    rd(ld(X1,rd(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
    inference(rw,[status(thm)],[t221250]) ).

cnf(t699,plain,
    ld(X1,rd(X1,X2)) = ld(ld(X3,mult(X3,X2)),rd(ld(X1,rd(X1,X2)),ld(X1,rd(X1,X2)))),
    inference(cp,[status(thm)],[t694,t216]) ).

cnf(t221245,plain,
    ld(X1,rd(X1,X2)) = ld(X2,rd(ld(X1,rd(X1,X2)),ld(X1,rd(X1,X2)))),
    inference(step,[status(thm)],[t699,t9]) ).

cnf(t221246,plain,
    ld(X1,rd(X1,X2)) = ld(X2,mult(ld(X1,rd(X1,X2)),X2)),
    inference(step,[status(thm)],[t221245,t216]) ).

cnf(t221247,plain,
    ld(X1,rd(X1,X2)) = ld(X2,rd(X2,X2)),
    inference(step,[status(thm)],[t221246,t615]) ).

cnf(t1189,plain,
    rd(X1,mult(X1,X1)) = ld(ld(X2,mult(X2,X1)),rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1)))),
    inference(cp,[status(thm)],[t694,t1174]) ).

cnf(t221230,plain,
    rd(X1,mult(X1,X1)) = ld(X1,rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1)))),
    inference(step,[status(thm)],[t1189,t9]) ).

cnf(t221231,plain,
    rd(X1,mult(X1,X1)) = ld(X1,mult(rd(X1,mult(X1,X1)),X1)),
    inference(step,[status(thm)],[t221230,t1174]) ).

cnf(t1095,plain,
    rd(X1,X1) = mult(rd(X1,mult(X1,X1)),X1),
    inference(cp,[status(thm)],[t8,t1088]) ).

cnf(t1113,plain,
    mult(rd(X1,mult(X1,X1)),X1) = rd(X1,X1),
    inference(orient,[status(thm)],[t1095]) ).

cnf(t221232,plain,
    rd(X1,mult(X1,X1)) = ld(X1,rd(X1,X1)),
    inference(step,[status(thm)],[t221231,t1113]) ).

cnf(t1196,plain,
    ld(X1,rd(X1,X1)) = rd(X1,mult(X1,X1)),
    inference(orient,[status(thm)],[t221232]) ).

cnf(t221248,plain,
    ld(X1,rd(X1,X2)) = rd(X2,mult(X2,X2)),
    inference(step,[status(thm)],[t221247,t1196]) ).

cnf(t1332,plain,
    ld(X1,rd(X1,X2)) = rd(X2,mult(X2,X2)),
    inference(orient,[status(thm)],[t221248]) ).

cnf(t221251,plain,
    rd(rd(X1,mult(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
    inference(step,[status(thm)],[t1479,t1332]) ).

cnf(t1480,plain,
    rd(rd(X1,mult(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
    inference(orient,[status(thm)],[t221251]) ).

cnf(t221254,plain,
    rd(X1,mult(X1,mult(X1,X1))) = rd(rd(X1,X1),mult(X1,X1)),
    inference(step,[status(thm)],[t1553,t1480]) ).

cnf(t1605,plain,
    rd(rd(X1,X1),mult(X1,X1)) = rd(X1,mult(X1,mult(X1,X1))),
    inference(orient,[status(thm)],[t221254]) ).

cnf(t222160,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(rd(X1,X1),mult(rd(X1,mult(X1,mult(X1,X1))),X2)),
    inference(step,[status(thm)],[t222159,t1605]) ).

cnf(t3903,plain,
    ld(rd(ld(X1,rd(X1,X2)),X2),X3) = mult(X2,mult(X2,mult(rd(X3,X2),X2))),
    inference(cp,[status(thm)],[t478,t3817]) ).

cnf(t221340,plain,
    ld(rd(ld(X1,rd(X1,X2)),X2),X3) = mult(X2,mult(X2,X3)),
    inference(step,[status(thm)],[t3903,t8]) ).

cnf(t4111,plain,
    ld(rd(ld(X1,rd(X1,X2)),X2),X3) = mult(X2,mult(X2,X3)),
    inference(orient,[status(thm)],[t221340]) ).

cnf(t4116,plain,
    mult(X1,mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3))) = X3,
    inference(cp,[status(thm)],[t4111,t9]) ).

cnf(t19776,plain,
    mult(X1,mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3))) = X3,
    inference(orient,[status(thm)],[t4116]) ).

cnf(t19880,plain,
    mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3)) = ld(X1,X3),
    inference(cp,[status(thm)],[t9,t19776]) ).

cnf(t19952,plain,
    mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3)) = ld(X1,X3),
    inference(orient,[status(thm)],[t19880]) ).

cnf(t20056,plain,
    mult(rd(ld(X1,rd(X1,X2)),X2),X3) = ld(X2,ld(X2,X3)),
    inference(cp,[status(thm)],[t9,t19952]) ).

cnf(t20144,plain,
    mult(rd(ld(X1,rd(X1,X2)),X2),X3) = ld(X2,ld(X2,X3)),
    inference(orient,[status(thm)],[t20056]) ).

cnf(t20244,plain,
    rd(ld(X1,ld(rd(ld(X2,rd(X2,X3)),X3),Y3)),X1) = ld(ld(X3,ld(X3,X1)),rd(Y3,X1)),
    inference(cp,[status(thm)],[t1429,t20144]) ).

cnf(t221512,plain,
    rd(ld(X1,mult(X3,mult(X3,Y3))),X1) = ld(ld(X3,ld(X3,X1)),rd(Y3,X1)),
    inference(step,[status(thm)],[t20244,t4111]) ).

cnf(t21483,plain,
    ld(ld(X1,ld(X1,X2)),rd(X3,X2)) = rd(ld(X2,mult(X1,mult(X1,X3))),X2),
    inference(orient,[status(thm)],[t221512]) ).

cnf(t21631,plain,
    ld(X1,ld(X1,X2)) = rd(rd(X3,X2),rd(ld(X2,mult(X1,mult(X1,X3))),X2)),
    inference(cp,[status(thm)],[t24,t21483]) ).

cnf(t2904,plain,
    ld(mult(rd(mult(X1,X2),X3),X2),X1) = rd(ld(X2,X3),X2),
    inference(cp,[status(thm)],[t12,t2852]) ).

cnf(t3000,plain,
    ld(mult(rd(mult(X1,X2),X3),X2),X1) = rd(ld(X2,X3),X2),
    inference(orient,[status(thm)],[t2904]) ).

cnf(t3045,plain,
    mult(rd(mult(X1,X2),X3),X2) = rd(X1,rd(ld(X2,X3),X2)),
    inference(cp,[status(thm)],[t24,t3000]) ).

cnf(t3101,plain,
    mult(rd(mult(X1,X2),X3),X2) = rd(X1,rd(ld(X2,X3),X2)),
    inference(orient,[status(thm)],[t3045]) ).

cnf(t3137,plain,
    rd(rd(X1,X2),rd(ld(X2,X3),X2)) = mult(rd(X1,X3),X2),
    inference(cp,[status(thm)],[t3101,t8]) ).

cnf(t3289,plain,
    rd(rd(X1,X2),rd(ld(X2,X3),X2)) = mult(rd(X1,X3),X2),
    inference(orient,[status(thm)],[t3137]) ).

cnf(t221513,plain,
    ld(X1,ld(X1,X2)) = mult(rd(X3,mult(X1,mult(X1,X3))),X2),
    inference(step,[status(thm)],[t21631,t3289]) ).

cnf(t21684,plain,
    mult(rd(X1,mult(X2,mult(X2,X1))),X3) = ld(X2,ld(X2,X3)),
    inference(orient,[status(thm)],[t221513]) ).

cnf(t222161,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(rd(X1,X1),ld(X1,ld(X1,X2))),
    inference(step,[status(thm)],[t222160,t21684]) ).

cnf(t108254,plain,
    ld(rd(X1,X1),ld(X1,ld(X1,X2))) = ld(X1,rd(ld(X1,mult(X2,X1)),X1)),
    inference(orient,[status(thm)],[t222161]) ).

cnf(t1562,plain,
    rd(X1,mult(ld(X2,X1),mult(X3,ld(X2,X1)))) = rd(rd(X2,X3),ld(X2,X1)),
    inference(cp,[status(thm)],[t1548,t24]) ).

cnf(t221696,plain,
    rd(X1,mult(ld(X2,X1),rd(X3,ld(X1,X2)))) = rd(rd(X2,X3),ld(X2,X1)),
    inference(step,[status(thm)],[t1562,t196]) ).

cnf(t3820,plain,
    mult(ld(X1,X2),mult(X3,ld(X1,X2))) = rd(ld(ld(Y3,rd(Y3,ld(X1,X2))),X3),ld(X2,X1)),
    inference(cp,[status(thm)],[t3817,t196]) ).

cnf(t221426,plain,
    mult(ld(X1,X2),rd(X3,ld(X2,X1))) = rd(ld(ld(Y3,rd(Y3,ld(X1,X2))),X3),ld(X2,X1)),
    inference(step,[status(thm)],[t3820,t196]) ).

cnf(t221427,plain,
    mult(ld(X1,X2),rd(X3,ld(X2,X1))) = rd(ld(ld(X2,X1),X3),ld(X2,X1)),
    inference(step,[status(thm)],[t221426,t225]) ).

cnf(t13647,plain,
    mult(ld(X1,X2),rd(X3,ld(X2,X1))) = rd(ld(ld(X2,X1),X3),ld(X2,X1)),
    inference(orient,[status(thm)],[t221427]) ).

cnf(t221697,plain,
    rd(X1,rd(ld(ld(X1,X2),X3),ld(X1,X2))) = rd(rd(X2,X3),ld(X2,X1)),
    inference(step,[status(thm)],[t221696,t13647]) ).

cnf(t45473,plain,
    rd(X1,rd(ld(ld(X1,X2),X3),ld(X1,X2))) = rd(rd(X2,X3),ld(X2,X1)),
    inference(orient,[status(thm)],[t221697]) ).

cnf(t86,plain,
    mult(ld(X1,X2),mult(ld(X2,X3),ld(X1,X2))) = ld(X1,mult(X3,ld(X1,X2))),
    inference(cp,[status(thm)],[t83,t24]) ).

cnf(t221629,plain,
    mult(ld(X1,X2),rd(ld(X2,X3),ld(X2,X1))) = ld(X1,mult(X3,ld(X1,X2))),
    inference(step,[status(thm)],[t86,t196]) ).

cnf(t221630,plain,
    rd(ld(ld(X2,X1),ld(X2,X3)),ld(X2,X1)) = ld(X1,mult(X3,ld(X1,X2))),
    inference(step,[status(thm)],[t221629,t13647]) ).

cnf(t221631,plain,
    rd(ld(ld(X2,X1),ld(X2,X3)),ld(X2,X1)) = ld(X1,rd(X3,ld(X2,X1))),
    inference(step,[status(thm)],[t221630,t196]) ).

cnf(t35101,plain,
    rd(ld(ld(X1,X2),ld(X1,X3)),ld(X1,X2)) = ld(X2,rd(X3,ld(X1,X2))),
    inference(orient,[status(thm)],[t221631]) ).

cnf(t45475,plain,
    rd(rd(X1,ld(X2,X3)),ld(X1,X2)) = rd(X2,ld(X1,rd(X3,ld(X2,X1)))),
    inference(cp,[status(thm)],[t45473,t35101]) ).

cnf(t45803,plain,
    rd(rd(X1,ld(X2,X3)),ld(X1,X2)) = rd(X2,ld(X1,rd(X3,ld(X2,X1)))),
    inference(orient,[status(thm)],[t45475]) ).

cnf(t596,plain,
    rd(mult(X1,X2),ld(X2,X2)) = rd(mult(X1,mult(X2,X2)),X2),
    inference(cp,[status(thm)],[t591,t56]) ).

cnf(t221211,plain,
    rd(mult(X1,X2),rd(X2,X2)) = rd(mult(X1,mult(X2,X2)),X2),
    inference(step,[status(thm)],[t596,t614]) ).

cnf(t757,plain,
    rd(mult(X1,mult(X2,X2)),X2) = rd(mult(X1,X2),rd(X2,X2)),
    inference(orient,[status(thm)],[t221211]) ).

cnf(t767,plain,
    mult(X1,mult(X2,X2)) = mult(rd(mult(X1,X2),rd(X2,X2)),X2),
    inference(cp,[status(thm)],[t8,t757]) ).

cnf(t221261,plain,
    mult(X1,mult(X2,X2)) = rd(mult(mult(X1,X2),X2),rd(X2,X2)),
    inference(step,[status(thm)],[t767,t900]) ).

cnf(t1724,plain,
    rd(mult(mult(X1,X2),X2),rd(X2,X2)) = mult(X1,mult(X2,X2)),
    inference(orient,[status(thm)],[t221261]) ).

cnf(t1757,plain,
    rd(mult(mult(mult(X1,X2),X2),X2),rd(X2,X2)) = mult(mult(X1,mult(X2,X2)),X2),
    inference(cp,[status(thm)],[t900,t1724]) ).

cnf(t221262,plain,
    mult(mult(X1,X2),mult(X2,X2)) = mult(mult(X1,mult(X2,X2)),X2),
    inference(step,[status(thm)],[t1757,t1724]) ).

cnf(t1772,plain,
    mult(mult(X1,mult(X2,X2)),X2) = mult(mult(X1,X2),mult(X2,X2)),
    inference(orient,[status(thm)],[t221262]) ).

cnf(t620,plain,
    mult(ld(X1,rd(rd(X1,X2),X2)),X2) = ld(X2,rd(rd(X1,X2),rd(X1,X2))),
    inference(cp,[status(thm)],[t505,t614]) ).

cnf(t9065,plain,
    ld(X1,rd(rd(X2,X1),rd(X2,X1))) = mult(ld(X2,rd(rd(X2,X1),X1)),X1),
    inference(orient,[status(thm)],[t620]) ).

cnf(t9104,plain,
    mult(ld(rd(X1,rd(X2,X2)),rd(rd(rd(X1,rd(X2,X2)),rd(X2,X2)),rd(X2,X2))),rd(X2,X2)) = ld(rd(X2,X2),rd(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2)))),
    inference(cp,[status(thm)],[t9065,t684]) ).

cnf(t221385,plain,
    rd(ld(rd(X1,rd(X2,X2)),rd(rd(rd(X1,rd(X2,X2)),rd(X2,X2)),rd(X2,X2))),rd(X2,X2)) = ld(rd(X2,X2),rd(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2)))),
    inference(step,[status(thm)],[t9104,t617]) ).

cnf(t221386,plain,
    rd(ld(rd(X1,rd(X2,X2)),rd(X1,mult(rd(X2,X2),mult(rd(X2,X2),rd(X2,X2))))),rd(X2,X2)) = ld(rd(X2,X2),rd(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2)))),
    inference(step,[status(thm)],[t221385,t1548]) ).

cnf(t613,plain,
    ld(X1,rd(X1,rd(X2,X2))) = ld(rd(X3,ld(X2,X2)),X3),
    inference(cp,[status(thm)],[t349,t591]) ).

cnf(t221205,plain,
    ld(X1,rd(X1,rd(X2,X2))) = ld(X2,X2),
    inference(step,[status(thm)],[t613,t23]) ).

cnf(t221206,plain,
    ld(X1,rd(X1,rd(X2,X2))) = rd(X2,X2),
    inference(step,[status(thm)],[t221205,t614]) ).

cnf(t644,plain,
    ld(X1,rd(X1,rd(X2,X2))) = rd(X2,X2),
    inference(orient,[status(thm)],[t221206]) ).

cnf(t4127,plain,
    mult(rd(X1,X1),mult(rd(X1,X1),X2)) = ld(rd(rd(X1,X1),rd(X1,X1)),X2),
    inference(cp,[status(thm)],[t4111,t644]) ).

cnf(t221342,plain,
    mult(rd(X1,X1),mult(rd(X1,X1),X2)) = ld(rd(X1,X1),X2),
    inference(step,[status(thm)],[t4127,t989]) ).

cnf(t4356,plain,
    mult(rd(X1,X1),mult(rd(X1,X1),X2)) = ld(rd(X1,X1),X2),
    inference(orient,[status(thm)],[t221342]) ).

cnf(t221387,plain,
    rd(ld(rd(X1,rd(X2,X2)),rd(X1,ld(rd(X2,X2),rd(X2,X2)))),rd(X2,X2)) = ld(rd(X2,X2),rd(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2)))),
    inference(step,[status(thm)],[t221386,t4356]) ).

cnf(t221388,plain,
    rd(ld(rd(X1,rd(X2,X2)),rd(X1,rd(rd(X2,X2),rd(X2,X2)))),rd(X2,X2)) = ld(rd(X2,X2),rd(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2)))),
    inference(step,[status(thm)],[t221387,t614]) ).

cnf(t221389,plain,
    rd(ld(rd(X1,rd(X2,X2)),rd(X1,rd(X2,X2))),rd(X2,X2)) = ld(rd(X2,X2),rd(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2)))),
    inference(step,[status(thm)],[t221388,t989]) ).

cnf(t221390,plain,
    rd(rd(rd(X1,rd(X2,X2)),rd(X1,rd(X2,X2))),rd(X2,X2)) = ld(rd(X2,X2),rd(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2)))),
    inference(step,[status(thm)],[t221389,t614]) ).

cnf(t221391,plain,
    rd(X1,mult(rd(X2,X2),mult(rd(X1,rd(X2,X2)),rd(X2,X2)))) = ld(rd(X2,X2),rd(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2)))),
    inference(step,[status(thm)],[t221390,t1548]) ).

cnf(t221392,plain,
    rd(X1,mult(rd(X2,X2),X1)) = ld(rd(X2,X2),rd(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2)))),
    inference(step,[status(thm)],[t221391,t8]) ).

cnf(t221393,plain,
    rd(X1,mult(rd(X2,X2),X1)) = ld(rd(X2,X2),rd(X1,X1)),
    inference(step,[status(thm)],[t221392,t684]) ).

cnf(t9193,plain,
    ld(rd(X1,X1),rd(X2,X2)) = rd(X2,mult(rd(X1,X1),X2)),
    inference(orient,[status(thm)],[t221393]) ).

cnf(t9231,plain,
    mult(ld(X1,rd(rd(X2,X2),X1)),X1) = ld(X1,rd(X2,mult(rd(X1,X1),X2))),
    inference(cp,[status(thm)],[t505,t9193]) ).

cnf(t15265,plain,
    ld(X1,rd(X2,mult(rd(X1,X1),X2))) = mult(ld(X1,rd(rd(X2,X2),X1)),X1),
    inference(orient,[status(thm)],[t9231]) ).

cnf(t20177,plain,
    ld(mult(rd(X1,X1),X1),ld(mult(rd(X1,X1),X1),X2)) = mult(rd(mult(ld(X1,rd(rd(X1,X1),X1)),X1),mult(rd(X1,X1),X1)),X2),
    inference(cp,[status(thm)],[t20144,t15265]) ).

cnf(t221501,plain,
    ld(X1,ld(mult(rd(X1,X1),X1),X2)) = mult(rd(mult(ld(X1,rd(rd(X1,X1),X1)),X1),mult(rd(X1,X1),X1)),X2),
    inference(step,[status(thm)],[t20177,t8]) ).

cnf(t221502,plain,
    ld(X1,ld(X1,X2)) = mult(rd(mult(ld(X1,rd(rd(X1,X1),X1)),X1),mult(rd(X1,X1),X1)),X2),
    inference(step,[status(thm)],[t221501,t8]) ).

cnf(t221503,plain,
    ld(X1,ld(X1,X2)) = mult(rd(mult(ld(X1,rd(X1,mult(X1,X1))),X1),mult(rd(X1,X1),X1)),X2),
    inference(step,[status(thm)],[t221502,t1088]) ).

cnf(t1187,plain,
    mult(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))) = ld(ld(X2,mult(X2,X1)),rd(X1,mult(X1,X1))),
    inference(cp,[status(thm)],[t1053,t1174]) ).

cnf(t221237,plain,
    rd(rd(X1,mult(X1,X1)),X1) = ld(ld(X2,mult(X2,X1)),rd(X1,mult(X1,X1))),
    inference(step,[status(thm)],[t1187,t1132]) ).

cnf(t221238,plain,
    rd(rd(X1,mult(X1,X1)),X1) = ld(X1,rd(X1,mult(X1,X1))),
    inference(step,[status(thm)],[t221237,t9]) ).

cnf(t1274,plain,
    ld(X1,rd(X1,mult(X1,X1))) = rd(rd(X1,mult(X1,X1)),X1),
    inference(orient,[status(thm)],[t221238]) ).

cnf(t221252,plain,
    ld(X1,rd(X1,mult(X1,X1))) = rd(rd(X1,X1),mult(X1,X1)),
    inference(step,[status(thm)],[t1274,t1480]) ).

cnf(t1481,plain,
    ld(X1,rd(X1,mult(X1,X1))) = rd(rd(X1,X1),mult(X1,X1)),
    inference(orient,[status(thm)],[t221252]) ).

cnf(t221255,plain,
    ld(X1,rd(X1,mult(X1,X1))) = rd(X1,mult(X1,mult(X1,X1))),
    inference(step,[status(thm)],[t1481,t1605]) ).

cnf(t1606,plain,
    ld(X1,rd(X1,mult(X1,X1))) = rd(X1,mult(X1,mult(X1,X1))),
    inference(orient,[status(thm)],[t221255]) ).

cnf(t221504,plain,
    ld(X1,ld(X1,X2)) = mult(rd(mult(rd(X1,mult(X1,mult(X1,X1))),X1),mult(rd(X1,X1),X1)),X2),
    inference(step,[status(thm)],[t221503,t1606]) ).

cnf(t221505,plain,
    ld(X1,ld(X1,X2)) = mult(rd(rd(rd(X1,X1),X1),mult(rd(X1,X1),X1)),X2),
    inference(step,[status(thm)],[t221504,t2564]) ).

cnf(t221506,plain,
    ld(X1,ld(X1,X2)) = mult(rd(rd(X1,mult(X1,X1)),mult(rd(X1,X1),X1)),X2),
    inference(step,[status(thm)],[t221505,t1088]) ).

cnf(t221507,plain,
    ld(X1,ld(X1,X2)) = mult(rd(rd(X1,mult(X1,X1)),X1),X2),
    inference(step,[status(thm)],[t221506,t8]) ).

cnf(t221508,plain,
    ld(X1,ld(X1,X2)) = mult(rd(rd(X1,X1),mult(X1,X1)),X2),
    inference(step,[status(thm)],[t221507,t2378]) ).

cnf(t221509,plain,
    ld(X1,ld(X1,X2)) = mult(rd(X1,mult(X1,mult(X1,X1))),X2),
    inference(step,[status(thm)],[t221508,t1605]) ).

cnf(t20451,plain,
    mult(rd(X1,mult(X1,mult(X1,X1))),X2) = ld(X1,ld(X1,X2)),
    inference(orient,[status(thm)],[t221509]) ).

cnf(t835,plain,
    mult(X1,X1) = rd(mult(X1,X1),rd(X1,X1)),
    inference(cp,[status(thm)],[t634,t825]) ).

cnf(t850,plain,
    rd(mult(X1,X1),rd(X1,X1)) = mult(X1,X1),
    inference(orient,[status(thm)],[t835]) ).

cnf(t3010,plain,
    rd(ld(X1,rd(X1,X1)),X1) = ld(mult(mult(X1,X1),X1),X1),
    inference(cp,[status(thm)],[t3000,t850]) ).

cnf(t221301,plain,
    rd(rd(X1,mult(X1,X1)),X1) = ld(mult(mult(X1,X1),X1),X1),
    inference(step,[status(thm)],[t3010,t1332]) ).

cnf(t221302,plain,
    rd(rd(X1,X1),mult(X1,X1)) = ld(mult(mult(X1,X1),X1),X1),
    inference(step,[status(thm)],[t221301,t2378]) ).

cnf(t221303,plain,
    rd(X1,mult(X1,mult(X1,X1))) = ld(mult(mult(X1,X1),X1),X1),
    inference(step,[status(thm)],[t221302,t1605]) ).

cnf(t859,plain,
    mult(rd(mult(X1,X1),X1),mult(X1,X1)) = mult(mult(X1,X1),X1),
    inference(cp,[status(thm)],[t782,t850]) ).

cnf(t221212,plain,
    mult(X1,mult(X1,X1)) = mult(mult(X1,X1),X1),
    inference(step,[status(thm)],[t859,t12]) ).

cnf(t865,plain,
    mult(mult(X1,X1),X1) = mult(X1,mult(X1,X1)),
    inference(orient,[status(thm)],[t221212]) ).

cnf(t221304,plain,
    rd(X1,mult(X1,mult(X1,X1))) = ld(mult(X1,mult(X1,X1)),X1),
    inference(step,[status(thm)],[t221303,t865]) ).

cnf(t221305,plain,
    rd(X1,mult(X1,mult(X1,X1))) = ld(true,rd(true,mult(X1,X1))),
    inference(step,[status(thm)],[t221304,t349]) ).

cnf(t3051,plain,
    rd(X1,mult(X1,mult(X1,X1))) = ld(true,rd(true,mult(X1,X1))),
    inference(orient,[status(thm)],[t221305]) ).

cnf(t20481,plain,
    ld(X1,ld(X1,X2)) = mult(ld(true,rd(true,mult(X1,X1))),X2),
    inference(cp,[status(thm)],[t20451,t3051]) ).

cnf(t20713,plain,
    mult(ld(true,rd(true,mult(X1,X1))),X2) = ld(X1,ld(X1,X2)),
    inference(orient,[status(thm)],[t20481]) ).

cnf(t20741,plain,
    ld(X1,ld(X1,X2)) = mult(ld(X3,rd(X3,mult(X1,X1))),X2),
    inference(cp,[status(thm)],[t20713,t390]) ).

cnf(t20980,plain,
    mult(ld(X1,rd(X1,mult(X2,X2))),X3) = ld(X2,ld(X2,X3)),
    inference(orient,[status(thm)],[t20741]) ).

cnf(t21242,plain,
    ld(mult(X1,X1),mult(X2,mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),mult(X1,X1)),
    inference(cp,[status(thm)],[t5111,t20980]) ).

cnf(t23083,plain,
    ld(mult(X1,X1),mult(X2,mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),mult(X1,X1)),
    inference(orient,[status(thm)],[t21242]) ).

cnf(t3966,plain,
    rd(ld(X1,mult(mult(mult(X1,X1),mult(X2,mult(X1,X1))),X1)),X1) = mult(mult(X1,X2),mult(X1,X1)),
    inference(cp,[status(thm)],[t3965,t25]) ).

cnf(t221729,plain,
    rd(ld(X1,mult(X1,mult(X1,mult(mult(X2,mult(X1,X1)),X1)))),X1) = mult(mult(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t3966,t14]) ).

cnf(t21794,plain,
    X1 = ld(rd(X2,mult(X3,mult(X3,X2))),ld(X3,ld(X3,X1))),
    inference(cp,[status(thm)],[t9,t21684]) ).

cnf(t29010,plain,
    ld(rd(X1,mult(X2,mult(X2,X1))),ld(X2,ld(X2,X3))) = X3,
    inference(orient,[status(thm)],[t21794]) ).

cnf(t29127,plain,
    mult(X1,X2) = ld(rd(X3,mult(X1,mult(X1,X3))),ld(X1,X2)),
    inference(cp,[status(thm)],[t29010,t9]) ).

cnf(t29397,plain,
    ld(rd(X1,mult(X2,mult(X2,X1))),ld(X2,X3)) = mult(X2,X3),
    inference(orient,[status(thm)],[t29127]) ).

cnf(t29506,plain,
    mult(X1,mult(X1,X2)) = ld(rd(X3,mult(X1,mult(X1,X3))),X2),
    inference(cp,[status(thm)],[t29397,t9]) ).

cnf(t29625,plain,
    ld(rd(X1,mult(X2,mult(X2,X1))),X3) = mult(X2,mult(X2,X3)),
    inference(orient,[status(thm)],[t29506]) ).

cnf(t29798,plain,
    mult(ld(mult(rd(X1,mult(X2,mult(X2,X1))),X3),Y3),X3) = ld(X3,mult(X2,mult(X2,mult(Y3,X3)))),
    inference(cp,[status(thm)],[t457,t29625]) ).

cnf(t221587,plain,
    mult(ld(ld(X2,ld(X2,X3)),Y3),X3) = ld(X3,mult(X2,mult(X2,mult(Y3,X3)))),
    inference(step,[status(thm)],[t29798,t21684]) ).

cnf(t30075,plain,
    ld(X1,mult(X2,mult(X2,mult(X3,X1)))) = mult(ld(ld(X2,ld(X2,X1)),X3),X1),
    inference(orient,[status(thm)],[t221587]) ).

cnf(t221730,plain,
    rd(mult(ld(ld(X1,ld(X1,X1)),mult(X2,mult(X1,X1))),X1),X1) = mult(mult(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t221729,t30075]) ).

cnf(t221731,plain,
    ld(ld(X1,ld(X1,X1)),mult(X2,mult(X1,X1))) = mult(mult(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t221730,t12]) ).

cnf(t221732,plain,
    ld(ld(X1,rd(X1,X1)),mult(X2,mult(X1,X1))) = mult(mult(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t221731,t614]) ).

cnf(t221733,plain,
    ld(rd(X1,mult(X1,X1)),mult(X2,mult(X1,X1))) = mult(mult(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t221732,t1332]) ).

cnf(t221734,plain,
    rd(mult(X1,mult(mult(X2,mult(X1,X1)),X1)),X1) = mult(mult(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t221733,t2930]) ).

cnf(t221735,plain,
    rd(mult(X1,mult(mult(X2,X1),mult(X1,X1))),X1) = mult(mult(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t221734,t1772]) ).

cnf(t54159,plain,
    rd(mult(X1,mult(mult(X2,X1),mult(X1,X1))),X1) = mult(mult(X1,X2),mult(X1,X1)),
    inference(orient,[status(thm)],[t221735]) ).

cnf(t54252,plain,
    mult(mult(X1,rd(X2,X1)),mult(X1,X1)) = rd(mult(X1,mult(X2,mult(X1,X1))),X1),
    inference(cp,[status(thm)],[t54159,t8]) ).

cnf(t54461,plain,
    mult(mult(X1,rd(X2,X1)),mult(X1,X1)) = rd(mult(X1,mult(X2,mult(X1,X1))),X1),
    inference(orient,[status(thm)],[t54252]) ).

cnf(t54603,plain,
    mult(ld(X1,ld(X1,mult(X1,rd(X2,X1)))),mult(X1,X1)) = ld(mult(X1,X1),rd(mult(X1,mult(X2,mult(X1,X1))),X1)),
    inference(cp,[status(thm)],[t23083,t54461]) ).

cnf(t221737,plain,
    mult(ld(X1,rd(X2,X1)),mult(X1,X1)) = ld(mult(X1,X1),rd(mult(X1,mult(X2,mult(X1,X1))),X1)),
    inference(step,[status(thm)],[t54603,t9]) ).

cnf(t221738,plain,
    mult(ld(X1,rd(X2,X1)),mult(X1,X1)) = rd(ld(X1,ld(X1,mult(X1,mult(X2,mult(X1,X1))))),X1),
    inference(step,[status(thm)],[t221737,t1429]) ).

cnf(t221739,plain,
    mult(ld(X1,rd(X2,X1)),mult(X1,X1)) = rd(ld(X1,mult(X2,mult(X1,X1))),X1),
    inference(step,[status(thm)],[t221738,t9]) ).

cnf(t54946,plain,
    mult(ld(X1,rd(X2,X1)),mult(X1,X1)) = rd(ld(X1,mult(X2,mult(X1,X1))),X1),
    inference(orient,[status(thm)],[t221739]) ).

cnf(t55132,plain,
    mult(mult(ld(X1,rd(X2,X1)),X1),mult(X1,X1)) = mult(rd(ld(X1,mult(X2,mult(X1,X1))),X1),X1),
    inference(cp,[status(thm)],[t1772,t54946]) ).

cnf(t221984,plain,
    mult(mult(ld(X1,rd(X2,X1)),X1),mult(X1,X1)) = ld(X1,mult(X2,mult(X1,X1))),
    inference(step,[status(thm)],[t55132,t8]) ).

cnf(t90218,plain,
    mult(mult(ld(X1,rd(X2,X1)),X1),mult(X1,X1)) = ld(X1,mult(X2,mult(X1,X1))),
    inference(orient,[status(thm)],[t221984]) ).

cnf(t90264,plain,
    ld(X1,mult(mult(rd(X1,X1),X2),mult(X1,X1))) = mult(mult(rd(ld(X1,X2),X1),X1),mult(X1,X1)),
    inference(cp,[status(thm)],[t90218,t3755]) ).

cnf(t222108,plain,
    ld(X1,mult(mult(rd(X1,X1),X2),mult(X1,X1))) = mult(ld(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t90264,t8]) ).

cnf(t103013,plain,
    ld(X1,mult(mult(rd(X1,X1),X2),mult(X1,X1))) = mult(ld(X1,X2),mult(X1,X1)),
    inference(orient,[status(thm)],[t222108]) ).

cnf(t103024,plain,
    mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = ld(X1,mult(rd(rd(X1,X1),mult(X1,X1)),mult(mult(X1,X1),X2))),
    inference(cp,[status(thm)],[t103013,t34]) ).

cnf(t2956,plain,
    mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = ld(mult(X1,X1),rd(mult(X1,mult(X2,X1)),X1)),
    inference(cp,[status(thm)],[t505,t2930]) ).

cnf(t221714,plain,
    mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = rd(ld(X1,ld(X1,mult(X1,mult(X2,X1)))),X1),
    inference(step,[status(thm)],[t2956,t1429]) ).

cnf(t20252,plain,
    mult(rd(ld(X1,rd(X1,X2)),X2),mult(X3,mult(Y3,X3))) = mult(mult(ld(X2,ld(X2,X3)),Y3),X3),
    inference(cp,[status(thm)],[t14,t20144]) ).

cnf(t221517,plain,
    ld(X2,ld(X2,mult(X3,mult(Y3,X3)))) = mult(mult(ld(X2,ld(X2,X3)),Y3),X3),
    inference(step,[status(thm)],[t20252,t20144]) ).

cnf(t22210,plain,
    ld(X1,ld(X1,mult(X2,mult(X3,X2)))) = mult(mult(ld(X1,ld(X1,X2)),X3),X2),
    inference(orient,[status(thm)],[t221517]) ).

cnf(t221715,plain,
    mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = rd(mult(mult(ld(X1,ld(X1,X1)),X2),X1),X1),
    inference(step,[status(thm)],[t221714,t22210]) ).

cnf(t221716,plain,
    mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = mult(ld(X1,ld(X1,X1)),X2),
    inference(step,[status(thm)],[t221715,t12]) ).

cnf(t221717,plain,
    mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = mult(ld(X1,rd(X1,X1)),X2),
    inference(step,[status(thm)],[t221716,t614]) ).

cnf(t221718,plain,
    mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = mult(rd(X1,mult(X1,X1)),X2),
    inference(step,[status(thm)],[t221717,t1332]) ).

cnf(t221719,plain,
    mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = rd(ld(X1,mult(X2,X1)),X1),
    inference(step,[status(thm)],[t221718,t3965]) ).

cnf(t50564,plain,
    mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = rd(ld(X1,mult(X2,X1)),X1),
    inference(orient,[status(thm)],[t221719]) ).

cnf(t222238,plain,
    rd(ld(X1,mult(X2,X1)),X1) = ld(X1,mult(rd(rd(X1,X1),mult(X1,X1)),mult(mult(X1,X1),X2))),
    inference(step,[status(thm)],[t103024,t50564]) ).

cnf(t222239,plain,
    rd(ld(X1,mult(X2,X1)),X1) = ld(X1,mult(rd(X1,mult(X1,mult(X1,X1))),mult(mult(X1,X1),X2))),
    inference(step,[status(thm)],[t222238,t1605]) ).

cnf(t222240,plain,
    rd(ld(X1,mult(X2,X1)),X1) = ld(X1,ld(X1,ld(X1,mult(mult(X1,X1),X2)))),
    inference(step,[status(thm)],[t222239,t21684]) ).

cnf(t116935,plain,
    ld(X1,ld(X1,ld(X1,mult(mult(X1,X1),X2)))) = rd(ld(X1,mult(X2,X1)),X1),
    inference(orient,[status(thm)],[t222240]) ).

cnf(t223,plain,
    mult(rd(X1,ld(X2,rd(X2,X3))),mult(ld(X2,rd(X2,X3)),Y3)) = mult(mult(X1,mult(Y3,X3)),ld(X2,rd(X2,X3))),
    inference(cp,[status(thm)],[t34,t216]) ).

cnf(t221638,plain,
    mult(mult(X1,X3),mult(ld(X2,rd(X2,X3)),Y3)) = mult(mult(X1,mult(Y3,X3)),ld(X2,rd(X2,X3))),
    inference(step,[status(thm)],[t223,t216]) ).

cnf(t221639,plain,
    mult(mult(X1,X3),mult(ld(X2,rd(X2,X3)),Y3)) = rd(mult(X1,mult(Y3,X3)),ld(rd(X2,X3),X2)),
    inference(step,[status(thm)],[t221638,t196]) ).

cnf(t221640,plain,
    mult(mult(X1,X3),mult(ld(X2,rd(X2,X3)),Y3)) = rd(mult(X1,mult(Y3,X3)),X3),
    inference(step,[status(thm)],[t221639,t23]) ).

cnf(t36653,plain,
    mult(mult(X1,X2),mult(ld(X3,rd(X3,X2)),Y3)) = rd(mult(X1,mult(Y3,X2)),X2),
    inference(orient,[status(thm)],[t221640]) ).

cnf(t116964,plain,
    rd(ld(X1,mult(mult(ld(X2,rd(X2,X1)),X3),X1)),X1) = ld(X1,ld(X1,ld(X1,rd(mult(X1,mult(X3,X1)),X1)))),
    inference(cp,[status(thm)],[t116935,t36653]) ).

cnf(t222241,plain,
    rd(ld(X1,ld(X1,mult(X3,X1))),X1) = ld(X1,ld(X1,ld(X1,rd(mult(X1,mult(X3,X1)),X1)))),
    inference(step,[status(thm)],[t116964,t5111]) ).

cnf(t222242,plain,
    rd(mult(ld(mult(X1,X1),X3),X1),X1) = ld(X1,ld(X1,ld(X1,rd(mult(X1,mult(X3,X1)),X1)))),
    inference(step,[status(thm)],[t222241,t457]) ).

cnf(t222243,plain,
    ld(mult(X1,X1),X3) = ld(X1,ld(X1,ld(X1,rd(mult(X1,mult(X3,X1)),X1)))),
    inference(step,[status(thm)],[t222242,t12]) ).

cnf(t21778,plain,
    ld(rd(X1,X2),ld(rd(X1,X2),X3)) = mult(rd(X2,mult(rd(X1,X2),X1)),X3),
    inference(cp,[status(thm)],[t21684,t8]) ).

cnf(t23507,plain,
    ld(rd(X1,X2),ld(rd(X1,X2),X3)) = mult(rd(X2,mult(rd(X1,X2),X1)),X3),
    inference(orient,[status(thm)],[t21778]) ).

cnf(t105520,plain,
    mult(rd(X1,mult(rd(X1,X1),X1)),ld(X1,mult(X2,X1))) = ld(rd(X1,X1),ld(X1,mult(mult(rd(X1,X1),X2),X1))),
    inference(cp,[status(thm)],[t23507,t105331]) ).

cnf(t222133,plain,
    rd(rd(X1,mult(rd(X1,X1),X1)),ld(mult(X2,X1),X1)) = ld(rd(X1,X1),ld(X1,mult(mult(rd(X1,X1),X2),X1))),
    inference(step,[status(thm)],[t105520,t196]) ).

cnf(t222134,plain,
    rd(rd(X1,X1),ld(mult(X2,X1),X1)) = ld(rd(X1,X1),ld(X1,mult(mult(rd(X1,X1),X2),X1))),
    inference(step,[status(thm)],[t222133,t8]) ).

cnf(t222135,plain,
    rd(rd(X1,X1),ld(mult(X2,X1),X1)) = ld(X1,mult(mult(rd(X1,X1),mult(rd(X1,X1),X2)),X1)),
    inference(step,[status(thm)],[t222134,t105331]) ).

cnf(t222136,plain,
    rd(rd(X1,X1),ld(mult(X2,X1),X1)) = ld(X1,mult(ld(rd(X1,X1),X2),X1)),
    inference(step,[status(thm)],[t222135,t4356]) ).

cnf(t105925,plain,
    ld(X1,mult(ld(rd(X1,X1),X2),X1)) = rd(rd(X1,X1),ld(mult(X2,X1),X1)),
    inference(orient,[status(thm)],[t222136]) ).

cnf(t1444,plain,
    rd(ld(X1,ld(ld(X2,rd(X2,X1)),X3)),X1) = ld(rd(X1,X1),rd(X3,X1)),
    inference(cp,[status(thm)],[t1429,t615]) ).

cnf(t42598,plain,
    rd(ld(X1,ld(ld(X2,rd(X2,X1)),X3)),X1) = ld(rd(X1,X1),rd(X3,X1)),
    inference(orient,[status(thm)],[t1444]) ).

cnf(t4643,plain,
    ld(ld(X1,rd(X1,X2)),rd(X1,X2)) = rd(mult(X2,X1),ld(rd(X1,X2),X1)),
    inference(cp,[status(thm)],[t4621,t23]) ).

cnf(t221347,plain,
    ld(ld(X1,rd(X1,X2)),rd(X1,X2)) = rd(mult(X2,X1),X2),
    inference(step,[status(thm)],[t4643,t23]) ).

cnf(t4799,plain,
    ld(ld(X1,rd(X1,X2)),rd(X1,X2)) = rd(mult(X2,X1),X2),
    inference(orient,[status(thm)],[t221347]) ).

cnf(t4808,plain,
    rd(mult(X1,X2),X1) = ld(ld(X3,rd(X3,X1)),rd(X2,X1)),
    inference(cp,[status(thm)],[t4799,t390]) ).

cnf(t5016,plain,
    ld(ld(X1,rd(X1,X2)),rd(X3,X2)) = rd(mult(X2,X3),X2),
    inference(orient,[status(thm)],[t4808]) ).

cnf(t42609,plain,
    ld(rd(X1,X1),rd(rd(X2,X1),X1)) = rd(ld(X1,rd(mult(X1,X2),X1)),X1),
    inference(cp,[status(thm)],[t42598,t5016]) ).

cnf(t42874,plain,
    ld(rd(X1,X1),rd(rd(X2,X1),X1)) = rd(ld(X1,rd(mult(X1,X2),X1)),X1),
    inference(orient,[status(thm)],[t42609]) ).

cnf(t105981,plain,
    rd(rd(X1,X1),ld(mult(rd(rd(X2,X1),X1),X1),X1)) = ld(X1,mult(rd(ld(X1,rd(mult(X1,X2),X1)),X1),X1)),
    inference(cp,[status(thm)],[t105925,t42874]) ).

cnf(t222147,plain,
    rd(rd(X1,X1),ld(rd(X2,X1),X1)) = ld(X1,mult(rd(ld(X1,rd(mult(X1,X2),X1)),X1),X1)),
    inference(step,[status(thm)],[t105981,t8]) ).

cnf(t222148,plain,
    rd(rd(X1,X1),ld(rd(X2,X1),X1)) = ld(X1,ld(X1,rd(mult(X1,X2),X1))),
    inference(step,[status(thm)],[t222147,t8]) ).

cnf(t107699,plain,
    ld(X1,ld(X1,rd(mult(X1,X2),X1))) = rd(rd(X1,X1),ld(rd(X2,X1),X1)),
    inference(orient,[status(thm)],[t222148]) ).

cnf(t222244,plain,
    ld(mult(X1,X1),X3) = ld(X1,rd(rd(X1,X1),ld(rd(mult(X3,X1),X1),X1))),
    inference(step,[status(thm)],[t222243,t107699]) ).

cnf(t222245,plain,
    ld(mult(X1,X1),X3) = ld(X1,rd(rd(X1,X1),ld(X3,X1))),
    inference(step,[status(thm)],[t222244,t12]) ).

cnf(t117221,plain,
    ld(X1,rd(rd(X1,X1),ld(X2,X1))) = ld(mult(X1,X1),X2),
    inference(orient,[status(thm)],[t222245]) ).

cnf(t117395,plain,
    ld(mult(X1,X1),rd(X1,X2)) = ld(X1,rd(rd(X1,X1),X2)),
    inference(cp,[status(thm)],[t117221,t23]) ).

cnf(t117572,plain,
    ld(mult(X1,X1),rd(X1,X2)) = ld(X1,rd(rd(X1,X1),X2)),
    inference(orient,[status(thm)],[t117395]) ).

cnf(t117761,plain,
    mult(X1,X1) = rd(rd(X1,X2),ld(X1,rd(rd(X1,X1),X2))),
    inference(cp,[status(thm)],[t24,t117572]) ).

cnf(t119730,plain,
    rd(rd(X1,X2),ld(X1,rd(rd(X1,X1),X2))) = mult(X1,X1),
    inference(orient,[status(thm)],[t117761]) ).

cnf(t119989,plain,
    rd(X1,ld(rd(X1,X2),rd(rd(rd(X1,X1),X2),ld(X1,rd(X1,X2))))) = rd(mult(X1,X1),ld(rd(X1,X2),X1)),
    inference(cp,[status(thm)],[t45803,t119730]) ).

cnf(t222255,plain,
    rd(X1,ld(rd(X1,X2),mult(rd(rd(X1,X1),X2),X2))) = rd(mult(X1,X1),ld(rd(X1,X2),X1)),
    inference(step,[status(thm)],[t119989,t216]) ).

cnf(t222256,plain,
    rd(X1,ld(rd(X1,X2),rd(X1,X1))) = rd(mult(X1,X1),ld(rd(X1,X2),X1)),
    inference(step,[status(thm)],[t222255,t8]) ).

cnf(t222257,plain,
    rd(X1,ld(rd(X1,X2),rd(X1,X1))) = rd(mult(X1,X1),X2),
    inference(step,[status(thm)],[t222256,t23]) ).

cnf(t120117,plain,
    rd(X1,ld(rd(X1,X2),rd(X1,X1))) = rd(mult(X1,X1),X2),
    inference(orient,[status(thm)],[t222257]) ).

cnf(t120397,plain,
    ld(rd(X1,X1),rd(X1,X2)) = ld(X1,rd(mult(X1,X1),X2)),
    inference(cp,[status(thm)],[t225,t120117]) ).

cnf(t121774,plain,
    ld(rd(X1,X1),rd(X1,X2)) = ld(X1,rd(mult(X1,X1),X2)),
    inference(orient,[status(thm)],[t120397]) ).

cnf(t121815,plain,
    ld(X1,rd(mult(X1,X1),rd(X2,mult(X2,X2)))) = ld(rd(X1,X1),mult(X1,X2)),
    inference(cp,[status(thm)],[t121774,t1174]) ).

cnf(t222265,plain,
    ld(X1,mult(mult(X1,X1),X2)) = ld(rd(X1,X1),mult(X1,X2)),
    inference(step,[status(thm)],[t121815,t1174]) ).

cnf(t122326,plain,
    ld(rd(X1,X1),mult(X1,X2)) = ld(X1,mult(mult(X1,X1),X2)),
    inference(orient,[status(thm)],[t222265]) ).

cnf(t122511,plain,
    mult(ld(X1,rd(mult(X1,X2),X1)),X1) = ld(X1,ld(X1,mult(mult(X1,X1),X2))),
    inference(cp,[status(thm)],[t505,t122326]) ).

cnf(t128403,plain,
    ld(X1,ld(X1,mult(mult(X1,X1),X2))) = mult(ld(X1,rd(mult(X1,X2),X1)),X1),
    inference(orient,[status(thm)],[t122511]) ).

cnf(t128503,plain,
    ld(X1,rd(ld(X1,mult(mult(mult(X1,X1),X2),X1)),X1)) = ld(rd(X1,X1),mult(ld(X1,rd(mult(X1,X2),X1)),X1)),
    inference(cp,[status(thm)],[t108254,t128403]) ).

cnf(t222288,plain,
    ld(X1,rd(ld(X1,mult(X1,mult(X1,mult(X2,X1)))),X1)) = ld(rd(X1,X1),mult(ld(X1,rd(mult(X1,X2),X1)),X1)),
    inference(step,[status(thm)],[t128503,t14]) ).

cnf(t222289,plain,
    ld(X1,rd(mult(ld(ld(X1,ld(X1,X1)),X2),X1),X1)) = ld(rd(X1,X1),mult(ld(X1,rd(mult(X1,X2),X1)),X1)),
    inference(step,[status(thm)],[t222288,t30075]) ).

cnf(t222290,plain,
    ld(X1,ld(ld(X1,ld(X1,X1)),X2)) = ld(rd(X1,X1),mult(ld(X1,rd(mult(X1,X2),X1)),X1)),
    inference(step,[status(thm)],[t222289,t12]) ).

cnf(t222291,plain,
    ld(X1,ld(ld(X1,rd(X1,X1)),X2)) = ld(rd(X1,X1),mult(ld(X1,rd(mult(X1,X2),X1)),X1)),
    inference(step,[status(thm)],[t222290,t614]) ).

cnf(t222292,plain,
    ld(X1,ld(rd(X1,mult(X1,X1)),X2)) = ld(rd(X1,X1),mult(ld(X1,rd(mult(X1,X2),X1)),X1)),
    inference(step,[status(thm)],[t222291,t1332]) ).

cnf(t222293,plain,
    ld(X1,rd(mult(X1,mult(X2,X1)),X1)) = ld(rd(X1,X1),mult(ld(X1,rd(mult(X1,X2),X1)),X1)),
    inference(step,[status(thm)],[t222292,t2930]) ).

cnf(t1099,plain,
    mult(ld(rd(X1,X1),rd(X2,X1)),X1) = ld(X1,ld(rd(X1,mult(X1,X1)),X2)),
    inference(cp,[status(thm)],[t505,t1088]) ).

cnf(t221395,plain,
    mult(ld(rd(X1,X1),rd(X2,X1)),X1) = ld(X1,rd(mult(X1,mult(X2,X1)),X1)),
    inference(step,[status(thm)],[t1099,t2930]) ).

cnf(t9967,plain,
    ld(X1,rd(mult(X1,mult(X2,X1)),X1)) = mult(ld(rd(X1,X1),rd(X2,X1)),X1),
    inference(orient,[status(thm)],[t221395]) ).

cnf(t222294,plain,
    mult(ld(rd(X1,X1),rd(X2,X1)),X1) = ld(rd(X1,X1),mult(ld(X1,rd(mult(X1,X2),X1)),X1)),
    inference(step,[status(thm)],[t222293,t9967]) ).

cnf(t222295,plain,
    mult(ld(rd(X1,X1),rd(X2,X1)),X1) = mult(X1,mult(ld(X1,ld(X1,rd(mult(X1,X2),X1))),X1)),
    inference(step,[status(thm)],[t222294,t83]) ).

cnf(t117833,plain,
    ld(rd(X1,X2),mult(X1,X1)) = ld(X3,rd(X3,ld(X1,rd(rd(X1,X1),X2)))),
    inference(cp,[status(thm)],[t225,t117572]) ).

cnf(t222247,plain,
    ld(rd(X1,X2),mult(X1,X1)) = ld(rd(rd(X1,X1),X2),X1),
    inference(step,[status(thm)],[t117833,t225]) ).

cnf(t118211,plain,
    ld(rd(rd(X1,X1),X2),X1) = ld(rd(X1,X2),mult(X1,X1)),
    inference(orient,[status(thm)],[t222247]) ).

cnf(t118285,plain,
    rd(rd(X1,X1),X2) = rd(X1,ld(rd(X1,X2),mult(X1,X1))),
    inference(cp,[status(thm)],[t24,t118211]) ).

cnf(t118669,plain,
    rd(X1,ld(rd(X1,X2),mult(X1,X1))) = rd(rd(X1,X1),X2),
    inference(orient,[status(thm)],[t118285]) ).

cnf(t118694,plain,
    rd(rd(X1,X1),ld(X2,X1)) = rd(X1,ld(X2,mult(X1,X1))),
    inference(cp,[status(thm)],[t118669,t24]) ).

cnf(t119031,plain,
    rd(rd(X1,X1),ld(X2,X1)) = rd(X1,ld(X2,mult(X1,X1))),
    inference(orient,[status(thm)],[t118694]) ).

cnf(t222251,plain,
    ld(X1,ld(X1,rd(mult(X1,X2),X1))) = rd(X1,ld(rd(X2,X1),mult(X1,X1))),
    inference(step,[status(thm)],[t107699,t119031]) ).

cnf(t222252,plain,
    ld(X1,ld(X1,rd(mult(X1,X2),X1))) = rd(X1,mult(X1,mult(ld(X2,X1),X1))),
    inference(step,[status(thm)],[t222251,t83]) ).

cnf(t119034,plain,
    ld(X1,ld(X1,rd(mult(X1,X2),X1))) = rd(X1,mult(X1,mult(ld(X2,X1),X1))),
    inference(orient,[status(thm)],[t222252]) ).

cnf(t222296,plain,
    mult(ld(rd(X1,X1),rd(X2,X1)),X1) = mult(X1,mult(rd(X1,mult(X1,mult(ld(X2,X1),X1))),X1)),
    inference(step,[status(thm)],[t222295,t119034]) ).

cnf(t222297,plain,
    mult(ld(rd(X1,X1),rd(X2,X1)),X1) = mult(X1,rd(rd(X1,X1),ld(X2,X1))),
    inference(step,[status(thm)],[t222296,t2564]) ).

cnf(t222298,plain,
    mult(ld(rd(X1,X1),rd(X2,X1)),X1) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
    inference(step,[status(thm)],[t222297,t119031]) ).

cnf(t129467,plain,
    mult(ld(rd(X1,X1),rd(X2,X1)),X1) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
    inference(orient,[status(thm)],[t222298]) ).

cnf(t129674,plain,
    mult(X1,rd(X1,ld(mult(X2,X1),mult(X1,X1)))) = mult(ld(rd(X1,X1),X2),X1),
    inference(cp,[status(thm)],[t129467,t12]) ).

cnf(t160240,plain,
    mult(X1,rd(X1,ld(mult(X2,X1),mult(X1,X1)))) = mult(ld(rd(X1,X1),X2),X1),
    inference(orient,[status(thm)],[t129674]) ).

cnf(t1092,plain,
    mult(X1,mult(ld(rd(X1,X1),X2),X1)) = ld(rd(X1,mult(X1,X1)),mult(X2,X1)),
    inference(cp,[status(thm)],[t83,t1088]) ).

cnf(t221394,plain,
    mult(X1,mult(ld(rd(X1,X1),X2),X1)) = rd(mult(X1,mult(mult(X2,X1),X1)),X1),
    inference(step,[status(thm)],[t1092,t2930]) ).

cnf(t9867,plain,
    mult(X1,mult(ld(rd(X1,X1),X2),X1)) = rd(mult(X1,mult(mult(X2,X1),X1)),X1),
    inference(orient,[status(thm)],[t221394]) ).

cnf(t105706,plain,
    rd(mult(X1,mult(rd(X1,X1),rd(X2,mult(X2,X2)))),X1) = ld(rd(X1,X1),rd(rd(X1,X2),X1)),
    inference(cp,[status(thm)],[t105627,t1132]) ).

cnf(t222139,plain,
    rd(mult(X1,rd(rd(X1,X1),X2)),X1) = ld(rd(X1,X1),rd(rd(X1,X2),X1)),
    inference(step,[status(thm)],[t105706,t1132]) ).

cnf(t106744,plain,
    ld(rd(X1,X1),rd(rd(X1,X2),X1)) = rd(mult(X1,rd(rd(X1,X1),X2)),X1),
    inference(orient,[status(thm)],[t222139]) ).

cnf(t107080,plain,
    rd(mult(X1,mult(mult(rd(rd(X1,X2),X1),X1),X1)),X1) = mult(X1,mult(rd(mult(X1,rd(rd(X1,X1),X2)),X1),X1)),
    inference(cp,[status(thm)],[t9867,t106744]) ).

cnf(t222163,plain,
    rd(mult(X1,mult(rd(X1,X2),X1)),X1) = mult(X1,mult(rd(mult(X1,rd(rd(X1,X1),X2)),X1),X1)),
    inference(step,[status(thm)],[t107080,t8]) ).

cnf(t222164,plain,
    rd(mult(X1,mult(rd(X1,X2),X1)),X1) = mult(X1,mult(X1,rd(rd(X1,X1),X2))),
    inference(step,[status(thm)],[t222163,t8]) ).

cnf(t108821,plain,
    mult(X1,mult(X1,rd(rd(X1,X1),X2))) = rd(mult(X1,mult(rd(X1,X2),X1)),X1),
    inference(orient,[status(thm)],[t222164]) ).

cnf(t108890,plain,
    rd(mult(rd(X1,mult(X1,X1)),mult(rd(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1)))),rd(X1,mult(X1,X1))) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),rd(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(cp,[status(thm)],[t108821,t1174]) ).

cnf(t222193,plain,
    mult(mult(rd(X1,mult(X1,X1)),mult(rd(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1)))),X1) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),rd(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(step,[status(thm)],[t108890,t1174]) ).

cnf(t222194,plain,
    mult(rd(ld(X1,mult(mult(rd(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1))),X1)),X1),X1) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),rd(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(step,[status(thm)],[t222193,t3965]) ).

cnf(t222195,plain,
    ld(X1,mult(mult(rd(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1))),X1)) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),rd(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(step,[status(thm)],[t222194,t8]) ).

cnf(t222196,plain,
    ld(X1,mult(rd(rd(rd(X1,mult(X1,X1)),X2),X1),X1)) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),rd(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(step,[status(thm)],[t222195,t1132]) ).

cnf(t1565,plain,
    rd(rd(X1,X1),mult(X1,mult(X2,X1))) = rd(rd(rd(X1,mult(X1,X1)),X2),X1),
    inference(cp,[status(thm)],[t1548,t1088]) ).

cnf(t11274,plain,
    rd(rd(rd(X1,mult(X1,X1)),X2),X1) = rd(rd(X1,X1),mult(X1,mult(X2,X1))),
    inference(orient,[status(thm)],[t1565]) ).

cnf(t222197,plain,
    ld(X1,mult(rd(rd(X1,X1),mult(X1,mult(X2,X1))),X1)) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),rd(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(step,[status(thm)],[t222196,t11274]) ).

cnf(t222198,plain,
    ld(X1,rd(rd(rd(X1,X1),X1),X2)) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),rd(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(step,[status(thm)],[t222197,t2564]) ).

cnf(t222199,plain,
    ld(X1,rd(rd(X1,mult(X1,X1)),X2)) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),rd(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(step,[status(thm)],[t222198,t1088]) ).

cnf(t222200,plain,
    ld(X1,rd(rd(X1,mult(X1,X1)),X2)) = rd(ld(X1,mult(mult(rd(X1,mult(X1,X1)),rd(mult(rd(X1,mult(X1,X1)),X1),X2)),X1)),X1),
    inference(step,[status(thm)],[t222199,t3965]) ).

cnf(t222201,plain,
    ld(X1,rd(rd(X1,mult(X1,X1)),X2)) = rd(ld(X1,mult(rd(ld(X1,mult(rd(mult(rd(X1,mult(X1,X1)),X1),X2),X1)),X1),X1)),X1),
    inference(step,[status(thm)],[t222200,t3965]) ).

cnf(t222202,plain,
    ld(X1,rd(rd(X1,mult(X1,X1)),X2)) = rd(ld(X1,ld(X1,mult(rd(mult(rd(X1,mult(X1,X1)),X1),X2),X1))),X1),
    inference(step,[status(thm)],[t222201,t8]) ).

cnf(t222203,plain,
    ld(X1,rd(rd(X1,mult(X1,X1)),X2)) = rd(mult(ld(mult(X1,X1),rd(mult(rd(X1,mult(X1,X1)),X1),X2)),X1),X1),
    inference(step,[status(thm)],[t222202,t457]) ).

cnf(t222204,plain,
    ld(X1,rd(rd(X1,mult(X1,X1)),X2)) = ld(mult(X1,X1),rd(mult(rd(X1,mult(X1,X1)),X1),X2)),
    inference(step,[status(thm)],[t222203,t12]) ).

cnf(t222205,plain,
    ld(X1,rd(rd(X1,mult(X1,X1)),X2)) = ld(mult(X1,X1),rd(rd(rd(X1,X1),rd(X1,X1)),X2)),
    inference(step,[status(thm)],[t222204,t2624]) ).

cnf(t222206,plain,
    ld(X1,rd(rd(X1,mult(X1,X1)),X2)) = ld(mult(X1,X1),rd(rd(X1,X1),X2)),
    inference(step,[status(thm)],[t222205,t989]) ).

cnf(t110167,plain,
    ld(mult(X1,X1),rd(rd(X1,X1),X2)) = ld(X1,rd(rd(X1,mult(X1,X1)),X2)),
    inference(orient,[status(thm)],[t222206]) ).

cnf(t110204,plain,
    ld(X1,rd(rd(X1,mult(X1,X1)),rd(ld(X1,X2),X1))) = ld(mult(X1,X1),mult(rd(X1,X2),X1)),
    inference(cp,[status(thm)],[t110167,t3289]) ).

cnf(t3304,plain,
    mult(rd(rd(X1,X1),X2),X1) = rd(rd(X1,mult(X1,X1)),rd(ld(X1,X2),X1)),
    inference(cp,[status(thm)],[t3289,t1088]) ).

cnf(t52168,plain,
    rd(rd(X1,mult(X1,X1)),rd(ld(X1,X2),X1)) = mult(rd(rd(X1,X1),X2),X1),
    inference(orient,[status(thm)],[t3304]) ).

cnf(t222213,plain,
    ld(X1,mult(rd(rd(X1,X1),X2),X1)) = ld(mult(X1,X1),mult(rd(X1,X2),X1)),
    inference(step,[status(thm)],[t110204,t52168]) ).

cnf(t111074,plain,
    ld(mult(X1,X1),mult(rd(X1,X2),X1)) = ld(X1,mult(rd(rd(X1,X1),X2),X1)),
    inference(orient,[status(thm)],[t222213]) ).

cnf(t111355,plain,
    ld(mult(rd(X1,X2),X1),mult(X1,X1)) = ld(X3,rd(X3,ld(X1,mult(rd(rd(X1,X1),X2),X1)))),
    inference(cp,[status(thm)],[t225,t111074]) ).

cnf(t222219,plain,
    ld(mult(rd(X1,X2),X1),mult(X1,X1)) = ld(mult(rd(rd(X1,X1),X2),X1),X1),
    inference(step,[status(thm)],[t111355,t225]) ).

cnf(t111948,plain,
    ld(mult(rd(rd(X1,X1),X2),X1),X1) = ld(mult(rd(X1,X2),X1),mult(X1,X1)),
    inference(orient,[status(thm)],[t222219]) ).

cnf(t112044,plain,
    mult(rd(rd(X1,X1),X2),X1) = rd(X1,ld(mult(rd(X1,X2),X1),mult(X1,X1))),
    inference(cp,[status(thm)],[t24,t111948]) ).

cnf(t141892,plain,
    rd(X1,ld(mult(rd(X1,X2),X1),mult(X1,X1))) = mult(rd(rd(X1,X1),X2),X1),
    inference(orient,[status(thm)],[t112044]) ).

cnf(t160245,plain,
    mult(ld(rd(X1,X1),rd(X1,X2)),X1) = mult(X1,mult(rd(rd(X1,X1),X2),X1)),
    inference(cp,[status(thm)],[t160240,t141892]) ).

cnf(t222527,plain,
    mult(ld(X1,rd(mult(X1,X1),X2)),X1) = mult(X1,mult(rd(rd(X1,X1),X2),X1)),
    inference(step,[status(thm)],[t160245,t121774]) ).

cnf(t160658,plain,
    mult(ld(X1,rd(mult(X1,X1),X2)),X1) = mult(X1,mult(rd(rd(X1,X1),X2),X1)),
    inference(orient,[status(thm)],[t222527]) ).

cnf(t119222,plain,
    ld(X1,X2) = ld(rd(X2,ld(X1,mult(X2,X2))),rd(X2,X2)),
    inference(cp,[status(thm)],[t23,t119031]) ).

cnf(t123839,plain,
    ld(rd(X1,ld(X2,mult(X1,X1))),rd(X1,X1)) = ld(X2,X1),
    inference(orient,[status(thm)],[t119222]) ).

cnf(t108503,plain,
    ld(ld(X1,ld(X1,X2)),rd(X1,X1)) = ld(X3,rd(X3,ld(X1,rd(ld(X1,mult(X2,X1)),X1)))),
    inference(cp,[status(thm)],[t225,t108254]) ).

cnf(t222192,plain,
    ld(ld(X1,ld(X1,X2)),rd(X1,X1)) = ld(rd(ld(X1,mult(X2,X1)),X1),X1),
    inference(step,[status(thm)],[t108503,t225]) ).

cnf(t109858,plain,
    ld(rd(ld(X1,mult(X2,X1)),X1),X1) = ld(ld(X1,ld(X1,X2)),rd(X1,X1)),
    inference(orient,[status(thm)],[t222192]) ).

cnf(t110005,plain,
    ld(ld(X1,ld(X1,rd(X2,X1))),rd(X1,X1)) = ld(rd(ld(X1,X2),X1),X1),
    inference(cp,[status(thm)],[t109858,t8]) ).

cnf(t105912,plain,
    rd(mult(X1,mult(mult(rd(mult(X1,X2),X1),X1),X1)),X1) = mult(X1,mult(rd(mult(X1,mult(rd(X1,X1),X2)),X1),X1)),
    inference(cp,[status(thm)],[t9867,t105627]) ).

cnf(t222145,plain,
    rd(mult(X1,mult(mult(X1,X2),X1)),X1) = mult(X1,mult(rd(mult(X1,mult(rd(X1,X1),X2)),X1),X1)),
    inference(step,[status(thm)],[t105912,t8]) ).

cnf(t222146,plain,
    rd(mult(X1,mult(mult(X1,X2),X1)),X1) = mult(X1,mult(X1,mult(rd(X1,X1),X2))),
    inference(step,[status(thm)],[t222145,t8]) ).

cnf(t107404,plain,
    mult(X1,mult(X1,mult(rd(X1,X1),X2))) = rd(mult(X1,mult(mult(X1,X2),X1)),X1),
    inference(orient,[status(thm)],[t222146]) ).

cnf(t107494,plain,
    rd(mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1)))),rd(X1,mult(X1,X1))) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(cp,[status(thm)],[t107404,t1174]) ).

cnf(t222165,plain,
    mult(mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1)))),X1) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(step,[status(thm)],[t107494,t1174]) ).

cnf(t222166,plain,
    mult(rd(ld(X1,mult(mult(mult(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1))),X1)),X1),X1) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(step,[status(thm)],[t222165,t3965]) ).

cnf(t222167,plain,
    ld(X1,mult(mult(mult(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1))),X1)) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(step,[status(thm)],[t222166,t8]) ).

cnf(t222168,plain,
    ld(X1,mult(rd(mult(rd(X1,mult(X1,X1)),X2),X1),X1)) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(step,[status(thm)],[t222167,t1132]) ).

cnf(t222169,plain,
    ld(X1,mult(rd(X1,mult(X1,X1)),X2)) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(step,[status(thm)],[t222168,t8]) ).

cnf(t222170,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X1),X2))),
    inference(step,[status(thm)],[t222169,t3965]) ).

cnf(t222171,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = rd(ld(X1,mult(mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X1),X2)),X1)),X1),
    inference(step,[status(thm)],[t222170,t3965]) ).

cnf(t222172,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = rd(ld(X1,mult(rd(ld(X1,mult(mult(mult(rd(X1,mult(X1,X1)),X1),X2),X1)),X1),X1)),X1),
    inference(step,[status(thm)],[t222171,t3965]) ).

cnf(t222173,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = rd(ld(X1,ld(X1,mult(mult(mult(rd(X1,mult(X1,X1)),X1),X2),X1))),X1),
    inference(step,[status(thm)],[t222172,t8]) ).

cnf(t222174,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = rd(mult(ld(mult(X1,X1),mult(mult(rd(X1,mult(X1,X1)),X1),X2)),X1),X1),
    inference(step,[status(thm)],[t222173,t457]) ).

cnf(t222175,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(mult(X1,X1),mult(mult(rd(X1,mult(X1,X1)),X1),X2)),
    inference(step,[status(thm)],[t222174,t12]) ).

cnf(t222176,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(mult(X1,X1),mult(rd(rd(X1,X1),rd(X1,X1)),X2)),
    inference(step,[status(thm)],[t222175,t2624]) ).

cnf(t222177,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(mult(X1,X1),mult(rd(X1,X1),X2)),
    inference(step,[status(thm)],[t222176,t989]) ).

cnf(t109095,plain,
    ld(mult(X1,X1),mult(rd(X1,X1),X2)) = ld(X1,rd(ld(X1,mult(X2,X1)),X1)),
    inference(orient,[status(thm)],[t222177]) ).

cnf(t109281,plain,
    ld(mult(rd(X1,X1),X2),mult(X1,X1)) = ld(X3,rd(X3,ld(X1,rd(ld(X1,mult(X2,X1)),X1)))),
    inference(cp,[status(thm)],[t225,t109095]) ).

cnf(t222209,plain,
    ld(mult(rd(X1,X1),X2),mult(X1,X1)) = ld(rd(ld(X1,mult(X2,X1)),X1),X1),
    inference(step,[status(thm)],[t109281,t225]) ).

cnf(t222210,plain,
    ld(mult(rd(X1,X1),X2),mult(X1,X1)) = ld(ld(X1,ld(X1,X2)),rd(X1,X1)),
    inference(step,[status(thm)],[t222209,t109858]) ).

cnf(t110749,plain,
    ld(ld(X1,ld(X1,X2)),rd(X1,X1)) = ld(mult(rd(X1,X1),X2),mult(X1,X1)),
    inference(orient,[status(thm)],[t222210]) ).

cnf(t222378,plain,
    ld(mult(rd(X1,X1),rd(X2,X1)),mult(X1,X1)) = ld(rd(ld(X1,X2),X1),X1),
    inference(step,[status(thm)],[t110005,t110749]) ).

cnf(t140434,plain,
    ld(mult(rd(X1,X1),rd(X2,X1)),mult(X1,X1)) = ld(rd(ld(X1,X2),X1),X1),
    inference(orient,[status(thm)],[t222378]) ).

cnf(t140734,plain,
    ld(mult(rd(X1,X1),rd(X2,X1)),X1) = ld(rd(X1,ld(rd(ld(X1,X2),X1),X1)),rd(X1,X1)),
    inference(cp,[status(thm)],[t123839,t140434]) ).

cnf(t117408,plain,
    ld(mult(X1,X1),mult(X1,X2)) = ld(X1,rd(rd(X1,X1),ld(X3,rd(X3,X2)))),
    inference(cp,[status(thm)],[t117221,t349]) ).

cnf(t222246,plain,
    ld(mult(X1,X1),mult(X1,X2)) = ld(X1,mult(rd(X1,X1),X2)),
    inference(step,[status(thm)],[t117408,t216]) ).

cnf(t117926,plain,
    ld(mult(X1,X1),mult(X1,X2)) = ld(X1,mult(rd(X1,X1),X2)),
    inference(orient,[status(thm)],[t222246]) ).

cnf(t118127,plain,
    ld(mult(X1,X2),mult(X1,X1)) = ld(X3,rd(X3,ld(X1,mult(rd(X1,X1),X2)))),
    inference(cp,[status(thm)],[t225,t117926]) ).

cnf(t222248,plain,
    ld(mult(X1,X2),mult(X1,X1)) = ld(mult(rd(X1,X1),X2),X1),
    inference(step,[status(thm)],[t118127,t225]) ).

cnf(t118442,plain,
    ld(mult(rd(X1,X1),X2),X1) = ld(mult(X1,X2),mult(X1,X1)),
    inference(orient,[status(thm)],[t222248]) ).

cnf(t222379,plain,
    ld(mult(X1,rd(X2,X1)),mult(X1,X1)) = ld(rd(X1,ld(rd(ld(X1,X2),X1),X1)),rd(X1,X1)),
    inference(step,[status(thm)],[t140734,t118442]) ).

cnf(t222380,plain,
    ld(mult(X1,rd(X2,X1)),mult(X1,X1)) = ld(rd(ld(X1,X2),X1),rd(X1,X1)),
    inference(step,[status(thm)],[t222379,t24]) ).

cnf(t140799,plain,
    ld(mult(X1,rd(X2,X1)),mult(X1,X1)) = ld(rd(ld(X1,X2),X1),rd(X1,X1)),
    inference(orient,[status(thm)],[t222380]) ).

cnf(t3987,plain,
    rd(X1,mult(X1,X1)) = rd(rd(ld(X1,mult(X2,X1)),X1),X2),
    inference(cp,[status(thm)],[t12,t3965]) ).

cnf(t4194,plain,
    rd(rd(ld(X1,mult(X2,X1)),X1),X2) = rd(X1,mult(X1,X1)),
    inference(orient,[status(thm)],[t3987]) ).

cnf(t140910,plain,
    ld(rd(ld(X1,rd(ld(X2,mult(X1,X2)),X2)),X1),rd(X1,X1)) = ld(mult(X1,rd(X2,mult(X2,X2))),mult(X1,X1)),
    inference(cp,[status(thm)],[t140799,t4194]) ).

cnf(t3971,plain,
    rd(ld(X1,mult(rd(X2,mult(X2,X2)),X1)),X1) = rd(rd(X1,mult(X1,X1)),X2),
    inference(cp,[status(thm)],[t3965,t1132]) ).

cnf(t221740,plain,
    rd(ld(X1,rd(ld(X2,mult(X1,X2)),X2)),X1) = rd(rd(X1,mult(X1,X1)),X2),
    inference(step,[status(thm)],[t3971,t3965]) ).

cnf(t55628,plain,
    rd(ld(X1,rd(ld(X2,mult(X1,X2)),X2)),X1) = rd(rd(X1,mult(X1,X1)),X2),
    inference(orient,[status(thm)],[t221740]) ).

cnf(t222573,plain,
    ld(rd(rd(X1,mult(X1,X1)),X2),rd(X1,X1)) = ld(mult(X1,rd(X2,mult(X2,X2))),mult(X1,X1)),
    inference(step,[status(thm)],[t140910,t55628]) ).

cnf(t222574,plain,
    ld(rd(rd(X1,mult(X1,X1)),X2),rd(X1,X1)) = ld(rd(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t222573,t1132]) ).

cnf(t168271,plain,
    ld(rd(rd(X1,mult(X1,X1)),X2),rd(X1,X1)) = ld(rd(X1,X2),mult(X1,X1)),
    inference(orient,[status(thm)],[t222574]) ).

cnf(t9197,plain,
    rd(rd(X1,mult(X1,X1)),mult(rd(X2,X2),rd(X1,mult(X1,X1)))) = ld(rd(X2,X2),mult(rd(X1,mult(X1,X1)),X1)),
    inference(cp,[status(thm)],[t9193,t1174]) ).

cnf(t221844,plain,
    rd(rd(X1,mult(X1,X1)),rd(rd(X2,X2),X1)) = ld(rd(X2,X2),mult(rd(X1,mult(X1,X1)),X1)),
    inference(step,[status(thm)],[t9197,t1132]) ).

cnf(t221845,plain,
    rd(rd(X1,mult(X1,X1)),rd(rd(X2,X2),X1)) = ld(rd(X2,X2),rd(rd(X1,X1),rd(X1,X1))),
    inference(step,[status(thm)],[t221844,t2624]) ).

cnf(t221846,plain,
    rd(rd(X1,mult(X1,X1)),rd(rd(X2,X2),X1)) = ld(rd(X2,X2),rd(X1,X1)),
    inference(step,[status(thm)],[t221845,t989]) ).

cnf(t221847,plain,
    rd(rd(X1,mult(X1,X1)),rd(rd(X2,X2),X1)) = rd(X1,mult(rd(X2,X2),X1)),
    inference(step,[status(thm)],[t221846,t9193]) ).

cnf(t63883,plain,
    rd(rd(X1,mult(X1,X1)),rd(rd(X2,X2),X1)) = rd(X1,mult(rd(X2,X2),X1)),
    inference(orient,[status(thm)],[t221847]) ).

cnf(t168277,plain,
    ld(rd(X1,rd(rd(X2,X2),X1)),mult(X1,X1)) = ld(rd(X1,mult(rd(X2,X2),X1)),rd(X1,X1)),
    inference(cp,[status(thm)],[t168271,t63883]) ).

cnf(t9202,plain,
    rd(rd(X1,X1),mult(rd(X2,X2),rd(X1,X1))) = ld(rd(X2,X2),rd(X1,X1)),
    inference(cp,[status(thm)],[t9193,t989]) ).

cnf(t221855,plain,
    rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = ld(rd(X2,X2),rd(X1,X1)),
    inference(step,[status(thm)],[t9202,t617]) ).

cnf(t221856,plain,
    rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = rd(X1,mult(rd(X2,X2),X1)),
    inference(step,[status(thm)],[t221855,t9193]) ).

cnf(t64727,plain,
    rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = rd(X1,mult(rd(X2,X2),X1)),
    inference(orient,[status(thm)],[t221856]) ).

cnf(t64788,plain,
    rd(rd(X1,X1),rd(X2,X2)) = ld(rd(X2,mult(rd(X1,X1),X2)),rd(X2,X2)),
    inference(cp,[status(thm)],[t23,t64727]) ).

cnf(t94664,plain,
    ld(rd(X1,mult(rd(X2,X2),X1)),rd(X1,X1)) = rd(rd(X2,X2),rd(X1,X1)),
    inference(orient,[status(thm)],[t64788]) ).

cnf(t222754,plain,
    ld(rd(X1,rd(rd(X2,X2),X1)),mult(X1,X1)) = rd(rd(X2,X2),rd(X1,X1)),
    inference(step,[status(thm)],[t168277,t94664]) ).

cnf(t198267,plain,
    ld(rd(X1,rd(rd(X2,X2),X1)),mult(X1,X1)) = rd(rd(X2,X2),rd(X1,X1)),
    inference(orient,[status(thm)],[t222754]) ).

cnf(t198395,plain,
    rd(X1,rd(rd(X2,X2),X1)) = rd(mult(X1,X1),rd(rd(X2,X2),rd(X1,X1))),
    inference(cp,[status(thm)],[t24,t198267]) ).

cnf(t214534,plain,
    rd(mult(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = rd(X1,rd(rd(X2,X2),X1)),
    inference(orient,[status(thm)],[t198395]) ).

cnf(t214745,plain,
    mult(X1,mult(rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))),X1)) = mult(ld(X1,rd(X1,rd(rd(X2,X2),X1))),X1),
    inference(cp,[status(thm)],[t160658,t214534]) ).

cnf(t222865,plain,
    mult(X1,mult(rd(X1,mult(rd(X2,X2),X1)),X1)) = mult(ld(X1,rd(X1,rd(rd(X2,X2),X1))),X1),
    inference(step,[status(thm)],[t214745,t64727]) ).

cnf(t45804,plain,
    rd(X1,ld(X2,rd(rd(X1,X3),ld(X1,X2)))) = rd(mult(X2,X3),ld(X2,X1)),
    inference(cp,[status(thm)],[t45803,t216]) ).

cnf(t84558,plain,
    rd(X1,ld(X2,rd(rd(X1,X3),ld(X1,X2)))) = rd(mult(X2,X3),ld(X2,X1)),
    inference(orient,[status(thm)],[t45804]) ).

cnf(t84832,plain,
    ld(X1,rd(rd(X2,X3),ld(X2,X1))) = ld(rd(mult(X1,X3),ld(X1,X2)),X2),
    inference(cp,[status(thm)],[t23,t84558]) ).

cnf(t84991,plain,
    ld(rd(mult(X1,X2),ld(X1,X3)),X3) = ld(X1,rd(rd(X3,X2),ld(X3,X1))),
    inference(orient,[status(thm)],[t84832]) ).

cnf(t84998,plain,
    ld(X1,rd(rd(rd(X1,X2),X3),ld(rd(X1,X2),X1))) = ld(mult(mult(X1,X3),X2),rd(X1,X2)),
    inference(cp,[status(thm)],[t84991,t216]) ).

cnf(t221949,plain,
    ld(X1,rd(rd(rd(X1,X2),X3),X2)) = ld(mult(mult(X1,X3),X2),rd(X1,X2)),
    inference(step,[status(thm)],[t84998,t23]) ).

cnf(t221950,plain,
    ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = ld(mult(mult(X1,X3),X2),rd(X1,X2)),
    inference(step,[status(thm)],[t221949,t1548]) ).

cnf(t221951,plain,
    ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = rd(ld(X2,ld(mult(X1,X3),X1)),X2),
    inference(step,[status(thm)],[t221950,t1429]) ).

cnf(t221952,plain,
    ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = rd(ld(X2,ld(true,rd(true,X3))),X2),
    inference(step,[status(thm)],[t221951,t349]) ).

cnf(t85377,plain,
    ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = rd(ld(X2,ld(true,rd(true,X3))),X2),
    inference(orient,[status(thm)],[t221952]) ).

cnf(t85447,plain,
    rd(ld(rd(X1,mult(X1,X1)),ld(true,rd(true,X2))),rd(X1,mult(X1,X1))) = ld(X3,rd(X3,rd(ld(X1,mult(mult(X2,rd(X1,mult(X1,X1))),X1)),X1))),
    inference(cp,[status(thm)],[t85377,t3965]) ).

cnf(t221957,plain,
    mult(ld(rd(X1,mult(X1,X1)),ld(true,rd(true,X2))),X1) = ld(X3,rd(X3,rd(ld(X1,mult(mult(X2,rd(X1,mult(X1,X1))),X1)),X1))),
    inference(step,[status(thm)],[t85447,t1174]) ).

cnf(t221958,plain,
    mult(rd(mult(X1,mult(ld(true,rd(true,X2)),X1)),X1),X1) = ld(X3,rd(X3,rd(ld(X1,mult(mult(X2,rd(X1,mult(X1,X1))),X1)),X1))),
    inference(step,[status(thm)],[t221957,t2930]) ).

cnf(t221959,plain,
    mult(X1,mult(ld(true,rd(true,X2)),X1)) = ld(X3,rd(X3,rd(ld(X1,mult(mult(X2,rd(X1,mult(X1,X1))),X1)),X1))),
    inference(step,[status(thm)],[t221958,t8]) ).

cnf(t221960,plain,
    mult(X1,mult(ld(true,rd(true,X2)),X1)) = ld(X3,rd(X3,rd(ld(X1,mult(rd(X2,X1),X1)),X1))),
    inference(step,[status(thm)],[t221959,t1132]) ).

cnf(t221961,plain,
    mult(X1,mult(ld(true,rd(true,X2)),X1)) = ld(X3,rd(X3,rd(ld(X1,X2),X1))),
    inference(step,[status(thm)],[t221960,t8]) ).

cnf(t86068,plain,
    ld(X1,rd(X1,rd(ld(X2,X3),X2))) = mult(X2,mult(ld(true,rd(true,X3)),X2)),
    inference(orient,[status(thm)],[t221961]) ).

cnf(t86161,plain,
    mult(X1,mult(ld(true,rd(true,rd(X2,mult(rd(X1,X1),X2)))),X1)) = ld(X3,rd(X3,rd(mult(ld(X1,rd(rd(X2,X2),X1)),X1),X1))),
    inference(cp,[status(thm)],[t86068,t15265]) ).

cnf(t9234,plain,
    ld(rd(X1,X1),rd(X2,X2)) = ld(X3,rd(X3,rd(X1,mult(rd(X2,X2),X1)))),
    inference(cp,[status(thm)],[t225,t9193]) ).

cnf(t221857,plain,
    rd(X2,mult(rd(X1,X1),X2)) = ld(X3,rd(X3,rd(X1,mult(rd(X2,X2),X1)))),
    inference(step,[status(thm)],[t9234,t9193]) ).

cnf(t64931,plain,
    ld(X1,rd(X1,rd(X2,mult(rd(X3,X3),X2)))) = rd(X3,mult(rd(X2,X2),X3)),
    inference(orient,[status(thm)],[t221857]) ).

cnf(t222101,plain,
    mult(X1,mult(rd(X1,mult(rd(X2,X2),X1)),X1)) = ld(X3,rd(X3,rd(mult(ld(X1,rd(rd(X2,X2),X1)),X1),X1))),
    inference(step,[status(thm)],[t86161,t64931]) ).

cnf(t222102,plain,
    mult(X1,mult(rd(X1,mult(rd(X2,X2),X1)),X1)) = ld(X3,rd(X3,ld(X1,rd(rd(X2,X2),X1)))),
    inference(step,[status(thm)],[t222101,t12]) ).

cnf(t222103,plain,
    mult(X1,mult(rd(X1,mult(rd(X2,X2),X1)),X1)) = ld(rd(rd(X2,X2),X1),X1),
    inference(step,[status(thm)],[t222102,t225]) ).

cnf(t100733,plain,
    mult(X1,mult(rd(X1,mult(rd(X2,X2),X1)),X1)) = ld(rd(rd(X2,X2),X1),X1),
    inference(orient,[status(thm)],[t222103]) ).

cnf(t222866,plain,
    ld(rd(rd(X2,X2),X1),X1) = mult(ld(X1,rd(X1,rd(rd(X2,X2),X1))),X1),
    inference(step,[status(thm)],[t222865,t100733]) ).

cnf(t219193,plain,
    mult(ld(X1,rd(X1,rd(rd(X2,X2),X1))),X1) = ld(rd(rd(X2,X2),X1),X1),
    inference(orient,[status(thm)],[t222866]) ).

cnf(t9207,plain,
    rd(X1,X1) = rd(rd(X2,X2),rd(X2,mult(rd(X1,X1),X2))),
    inference(cp,[status(thm)],[t24,t9193]) ).

cnf(t9242,plain,
    rd(rd(X1,X1),rd(X1,mult(rd(X2,X2),X1))) = rd(X2,X2),
    inference(orient,[status(thm)],[t9207]) ).

cnf(t219251,plain,
    ld(rd(rd(X1,X1),rd(X1,mult(rd(X2,X2),X1))),rd(X1,mult(rd(X2,X2),X1))) = mult(ld(rd(X1,mult(rd(X2,X2),X1)),rd(rd(X1,mult(rd(X2,X2),X1)),rd(X2,X2))),rd(X1,mult(rd(X2,X2),X1))),
    inference(cp,[status(thm)],[t219193,t9242]) ).

cnf(t222867,plain,
    ld(rd(X2,X2),rd(X1,mult(rd(X2,X2),X1))) = mult(ld(rd(X1,mult(rd(X2,X2),X1)),rd(rd(X1,mult(rd(X2,X2),X1)),rd(X2,X2))),rd(X1,mult(rd(X2,X2),X1))),
    inference(step,[status(thm)],[t219251,t9242]) ).

cnf(t15310,plain,
    mult(ld(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))),
    inference(cp,[status(thm)],[t15265,t989]) ).

cnf(t221886,plain,
    rd(ld(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))),
    inference(step,[status(thm)],[t15310,t617]) ).

cnf(t5024,plain,
    rd(mult(rd(X1,X1),X2),rd(X1,X1)) = ld(rd(X1,X1),rd(X2,rd(X1,X1))),
    inference(cp,[status(thm)],[t5016,t644]) ).

cnf(t14646,plain,
    ld(rd(X1,X1),rd(X2,rd(X1,X1))) = rd(mult(rd(X1,X1),X2),rd(X1,X1)),
    inference(orient,[status(thm)],[t5024]) ).

cnf(t221887,plain,
    rd(rd(mult(rd(X1,X1),rd(X2,X2)),rd(X1,X1)),rd(X1,X1)) = ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))),
    inference(step,[status(thm)],[t221886,t14646]) ).

cnf(t221888,plain,
    mult(rd(X1,X1),rd(X2,X2)) = ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))),
    inference(step,[status(thm)],[t221887,t684]) ).

cnf(t221889,plain,
    rd(rd(X1,X1),rd(X2,X2)) = ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))),
    inference(step,[status(thm)],[t221888,t617]) ).

cnf(t68263,plain,
    ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))) = rd(rd(X1,X1),rd(X2,X2)),
    inference(orient,[status(thm)],[t221889]) ).

cnf(t222868,plain,
    rd(rd(X2,X2),rd(X1,X1)) = mult(ld(rd(X1,mult(rd(X2,X2),X1)),rd(rd(X1,mult(rd(X2,X2),X1)),rd(X2,X2))),rd(X1,mult(rd(X2,X2),X1))),
    inference(step,[status(thm)],[t222867,t68263]) ).

cnf(t9192,plain,
    mult(X1,mult(rd(rd(X2,ld(X3,rd(X3,X1))),rd(X2,ld(X3,rd(X3,X1)))),X1)) = mult(mult(ld(X2,rd(rd(X2,ld(X3,rd(X3,X1))),ld(X3,rd(X3,X1)))),ld(X3,rd(X3,X1))),X1),
    inference(cp,[status(thm)],[t3817,t9065]) ).

cnf(t221835,plain,
    mult(X1,mult(rd(mult(X2,X1),rd(X2,ld(X3,rd(X3,X1)))),X1)) = mult(mult(ld(X2,rd(rd(X2,ld(X3,rd(X3,X1))),ld(X3,rd(X3,X1)))),ld(X3,rd(X3,X1))),X1),
    inference(step,[status(thm)],[t9192,t216]) ).

cnf(t221836,plain,
    mult(X1,rd(X2,rd(ld(X1,rd(X2,ld(X3,rd(X3,X1)))),X1))) = mult(mult(ld(X2,rd(rd(X2,ld(X3,rd(X3,X1))),ld(X3,rd(X3,X1)))),ld(X3,rd(X3,X1))),X1),
    inference(step,[status(thm)],[t221835,t3101]) ).

cnf(t221837,plain,
    mult(X1,rd(X2,rd(ld(X1,mult(X2,X1)),X1))) = mult(mult(ld(X2,rd(rd(X2,ld(X3,rd(X3,X1))),ld(X3,rd(X3,X1)))),ld(X3,rd(X3,X1))),X1),
    inference(step,[status(thm)],[t221836,t216]) ).

cnf(t221838,plain,
    mult(X1,rd(X2,rd(ld(X1,mult(X2,X1)),X1))) = mult(rd(ld(X2,rd(rd(X2,ld(X3,rd(X3,X1))),ld(X3,rd(X3,X1)))),ld(rd(X3,X1),X3)),X1),
    inference(step,[status(thm)],[t221837,t196]) ).

cnf(t499,plain,
    mult(mult(X1,ld(X2,rd(X3,Y3))),Y3) = mult(rd(X1,Y3),ld(rd(X2,Y3),X3)),
    inference(cp,[status(thm)],[t25,t478]) ).

cnf(t221379,plain,
    mult(rd(X1,ld(rd(X3,Y3),X2)),Y3) = mult(rd(X1,Y3),ld(rd(X2,Y3),X3)),
    inference(step,[status(thm)],[t499,t196]) ).

cnf(t221380,plain,
    mult(rd(X1,ld(rd(X3,Y3),X2)),Y3) = rd(rd(X1,Y3),ld(X3,rd(X2,Y3))),
    inference(step,[status(thm)],[t221379,t196]) ).

cnf(t8439,plain,
    mult(rd(X1,ld(rd(X2,X3),Y3)),X3) = rd(rd(X1,X3),ld(X2,rd(Y3,X3))),
    inference(orient,[status(thm)],[t221380]) ).

cnf(t221839,plain,
    mult(X1,rd(X2,rd(ld(X1,mult(X2,X1)),X1))) = rd(rd(ld(X2,rd(rd(X2,ld(X3,rd(X3,X1))),ld(X3,rd(X3,X1)))),X1),ld(X3,rd(X3,X1))),
    inference(step,[status(thm)],[t221838,t8439]) ).

cnf(t221840,plain,
    mult(X1,rd(X2,rd(ld(X1,mult(X2,X1)),X1))) = mult(rd(ld(X2,rd(rd(X2,ld(X3,rd(X3,X1))),ld(X3,rd(X3,X1)))),X1),X1),
    inference(step,[status(thm)],[t221839,t216]) ).

cnf(t221841,plain,
    mult(X1,rd(X2,rd(ld(X1,mult(X2,X1)),X1))) = ld(X2,rd(rd(X2,ld(X3,rd(X3,X1))),ld(X3,rd(X3,X1)))),
    inference(step,[status(thm)],[t221840,t8]) ).

cnf(t221842,plain,
    mult(X1,rd(X2,rd(ld(X1,mult(X2,X1)),X1))) = ld(X2,mult(rd(X2,ld(X3,rd(X3,X1))),X1)),
    inference(step,[status(thm)],[t221841,t216]) ).

cnf(t221843,plain,
    mult(X1,rd(X2,rd(ld(X1,mult(X2,X1)),X1))) = ld(X2,mult(mult(X2,X1),X1)),
    inference(step,[status(thm)],[t221842,t216]) ).

cnf(t63650,plain,
    mult(X1,rd(X2,rd(ld(X1,mult(X2,X1)),X1))) = ld(X2,mult(mult(X2,X1),X1)),
    inference(orient,[status(thm)],[t221843]) ).

cnf(t63663,plain,
    ld(X1,mult(mult(X1,ld(X2,rd(X2,X3))),ld(X2,rd(X2,X3)))) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(ld(ld(X2,rd(X2,X3)),mult(X1,ld(X2,rd(X2,X3)))),X3))),
    inference(cp,[status(thm)],[t63650,t216]) ).

cnf(t222002,plain,
    ld(X1,rd(mult(X1,ld(X2,rd(X2,X3))),ld(rd(X2,X3),X2))) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(ld(ld(X2,rd(X2,X3)),mult(X1,ld(X2,rd(X2,X3)))),X3))),
    inference(step,[status(thm)],[t63663,t196]) ).

cnf(t222003,plain,
    ld(X1,rd(rd(X1,ld(rd(X2,X3),X2)),ld(rd(X2,X3),X2))) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(ld(ld(X2,rd(X2,X3)),mult(X1,ld(X2,rd(X2,X3)))),X3))),
    inference(step,[status(thm)],[t222002,t196]) ).

cnf(t222004,plain,
    ld(X1,rd(rd(X1,X3),ld(rd(X2,X3),X2))) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(ld(ld(X2,rd(X2,X3)),mult(X1,ld(X2,rd(X2,X3)))),X3))),
    inference(step,[status(thm)],[t222003,t23]) ).

cnf(t222005,plain,
    ld(X1,rd(rd(X1,X3),X3)) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(ld(ld(X2,rd(X2,X3)),mult(X1,ld(X2,rd(X2,X3)))),X3))),
    inference(step,[status(thm)],[t222004,t23]) ).

cnf(t222006,plain,
    ld(X1,rd(rd(X1,X3),X3)) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(X3,mult(mult(X1,ld(X2,rd(X2,X3))),X3)))),
    inference(step,[status(thm)],[t222005,t3817]) ).

cnf(t222007,plain,
    ld(X1,rd(rd(X1,X3),X3)) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(X3,mult(rd(X1,ld(rd(X2,X3),X2)),X3)))),
    inference(step,[status(thm)],[t222006,t196]) ).

cnf(t222008,plain,
    ld(X1,rd(rd(X1,X3),X3)) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(X3,rd(rd(X1,X3),ld(X2,rd(X2,X3)))))),
    inference(step,[status(thm)],[t222007,t8439]) ).

cnf(t222009,plain,
    ld(X1,rd(rd(X1,X3),X3)) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(X3,mult(rd(X1,X3),X3)))),
    inference(step,[status(thm)],[t222008,t216]) ).

cnf(t222010,plain,
    ld(X1,rd(rd(X1,X3),X3)) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(X3,X1))),
    inference(step,[status(thm)],[t222009,t8]) ).

cnf(t93653,plain,
    mult(ld(X1,rd(X1,X2)),rd(X3,mult(X2,X3))) = ld(X3,rd(rd(X3,X2),X2)),
    inference(orient,[status(thm)],[t222010]) ).

cnf(t222869,plain,
    rd(rd(X2,X2),rd(X1,X1)) = ld(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2))),
    inference(step,[status(thm)],[t222868,t93653]) ).

cnf(t222870,plain,
    rd(rd(X2,X2),rd(X1,X1)) = ld(X1,X1),
    inference(step,[status(thm)],[t222869,t684]) ).

cnf(t222871,plain,
    rd(rd(X2,X2),rd(X1,X1)) = rd(X1,X1),
    inference(step,[status(thm)],[t222870,t614]) ).

cnf(t219573,plain,
    rd(rd(X1,X1),rd(X2,X2)) = rd(X2,X2),
    inference(orient,[status(thm)],[t222871]) ).

cnf(t219785,plain,
    mult(X1,mult(rd(X1,X1),rd(X2,X2))) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
    inference(cp,[status(thm)],[t81265,t219573]) ).

cnf(t222895,plain,
    mult(X1,rd(rd(X1,X1),rd(X2,X2))) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
    inference(step,[status(thm)],[t219785,t617]) ).

cnf(t222896,plain,
    mult(X1,rd(X2,X2)) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
    inference(step,[status(thm)],[t222895,t219573]) ).

cnf(t222897,plain,
    rd(X1,rd(X2,X2)) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
    inference(step,[status(thm)],[t222896,t617]) ).

cnf(t222898,plain,
    rd(X1,rd(X2,X2)) = X1,
    inference(step,[status(thm)],[t222897,t12]) ).

cnf(t219881,plain,
    rd(X1,rd(X2,X2)) = X1,
    inference(orient,[status(thm)],[t222898]) ).

cnf(t0,plain,
    ifeq(X1,X1,X2,X3) = X2,
    introduced(definition) ).

cnf(t11,plain,
    ifeq(X1,X1,X2,X3) = X2,
    inference(orient,[status(thm)],[t0]) ).

cnf(t514,plain,
    mult(ld(X1,rd(X2,ld(X3,rd(X3,Y3)))),ld(X3,rd(X3,Y3))) = ld(ld(X3,rd(X3,Y3)),ld(mult(X1,Y3),X2)),
    inference(cp,[status(thm)],[t505,t216]) ).

cnf(t221644,plain,
    rd(ld(X1,rd(X2,ld(X3,rd(X3,Y3)))),ld(rd(X3,Y3),X3)) = ld(ld(X3,rd(X3,Y3)),ld(mult(X1,Y3),X2)),
    inference(step,[status(thm)],[t514,t196]) ).

cnf(t221645,plain,
    rd(ld(X1,mult(X2,Y3)),ld(rd(X3,Y3),X3)) = ld(ld(X3,rd(X3,Y3)),ld(mult(X1,Y3),X2)),
    inference(step,[status(thm)],[t221644,t216]) ).

cnf(t221646,plain,
    rd(ld(X1,mult(X2,Y3)),Y3) = ld(ld(X3,rd(X3,Y3)),ld(mult(X1,Y3),X2)),
    inference(step,[status(thm)],[t221645,t23]) ).

cnf(t39034,plain,
    ld(ld(X1,rd(X1,X2)),ld(mult(X3,X2),Y3)) = rd(ld(X3,mult(Y3,X2)),X2),
    inference(orient,[status(thm)],[t221646]) ).

cnf(t222284,plain,
    ld(X1,mult(ld(X1,rd(mult(X1,X2),X1)),X1)) = rd(ld(X1,mult(X2,X1)),X1),
    inference(step,[status(thm)],[t116935,t128403]) ).

cnf(t128657,plain,
    ld(X1,mult(ld(X1,rd(mult(X1,X2),X1)),X1)) = rd(ld(X1,mult(X2,X1)),X1),
    inference(rw,[status(thm)],[t222284]) ).

cnf(t3973,plain,
    rd(ld(X1,mult(X2,X1)),X1) = mult(ld(X3,rd(X3,X1)),X2),
    inference(cp,[status(thm)],[t3965,t1332]) ).

cnf(t32859,plain,
    rd(ld(X1,mult(X2,X1)),X1) = mult(ld(X3,rd(X3,X1)),X2),
    inference(orient,[status(thm)],[t3973]) ).

cnf(t90559,plain,
    mult(ld(X1,rd(X1,mult(X2,X2))),mult(ld(X2,rd(X3,X2)),X2)) = rd(ld(mult(X2,X2),ld(X2,mult(X3,mult(X2,X2)))),mult(X2,X2)),
    inference(cp,[status(thm)],[t32859,t90218]) ).

cnf(t522,plain,
    rd(X1,ld(ld(rd(X2,X3),Y3),X3)) = mult(X1,mult(ld(X2,rd(Y3,X3)),X3)),
    inference(cp,[status(thm)],[t196,t505]) ).

cnf(t8698,plain,
    mult(X1,mult(ld(X2,rd(X3,Y3)),Y3)) = rd(X1,ld(ld(rd(X2,Y3),X3),Y3)),
    inference(orient,[status(thm)],[t522]) ).

cnf(t222109,plain,
    rd(ld(X1,rd(X1,mult(X2,X2))),ld(ld(rd(X2,X2),X3),X2)) = rd(ld(mult(X2,X2),ld(X2,mult(X3,mult(X2,X2)))),mult(X2,X2)),
    inference(step,[status(thm)],[t90559,t8698]) ).

cnf(t1059,plain,
    mult(ld(X1,rd(X1,X2)),ld(X1,rd(X1,X2))) = ld(ld(X3,mult(X3,X2)),ld(X1,rd(X1,X2))),
    inference(cp,[status(thm)],[t1053,t216]) ).

cnf(t221234,plain,
    rd(ld(X1,rd(X1,X2)),ld(rd(X1,X2),X1)) = ld(ld(X3,mult(X3,X2)),ld(X1,rd(X1,X2))),
    inference(step,[status(thm)],[t1059,t196]) ).

cnf(t221235,plain,
    rd(ld(X1,rd(X1,X2)),X2) = ld(ld(X3,mult(X3,X2)),ld(X1,rd(X1,X2))),
    inference(step,[status(thm)],[t221234,t23]) ).

cnf(t221236,plain,
    rd(ld(X1,rd(X1,X2)),X2) = ld(X2,ld(X1,rd(X1,X2))),
    inference(step,[status(thm)],[t221235,t9]) ).

cnf(t1253,plain,
    ld(X1,ld(X2,rd(X2,X1))) = rd(ld(X2,rd(X2,X1)),X1),
    inference(orient,[status(thm)],[t221236]) ).

cnf(t4169,plain,
    rd(ld(X1,rd(X1,X2)),X2) = rd(X3,mult(X2,mult(X2,X3))),
    inference(cp,[status(thm)],[t24,t4111]) ).

cnf(t33310,plain,
    rd(ld(X1,rd(X1,X2)),X2) = rd(X3,mult(X2,mult(X2,X3))),
    inference(orient,[status(thm)],[t4169]) ).

cnf(t221614,plain,
    ld(X1,ld(X2,rd(X2,X1))) = rd(true,mult(X1,mult(X1,true))),
    inference(step,[status(thm)],[t1253,t33310]) ).

cnf(t33311,plain,
    ld(X1,ld(X2,rd(X2,X1))) = rd(true,mult(X1,mult(X1,true))),
    inference(orient,[status(thm)],[t221614]) ).

cnf(t4389,plain,
    rd(ld(X1,mult(rd(X1,X1),X2)),X1) = ld(X1,rd(ld(rd(X1,X1),X2),X1)),
    inference(cp,[status(thm)],[t3755,t4356]) ).

cnf(t14171,plain,
    ld(X1,rd(ld(rd(X1,X1),X2),X1)) = rd(ld(X1,mult(rd(X1,X1),X2)),X1),
    inference(orient,[status(thm)],[t4389]) ).

cnf(t33466,plain,
    rd(ld(X1,mult(rd(X1,X1),rd(rd(X1,X1),X1))),X1) = ld(X1,rd(X2,mult(X1,mult(X1,X2)))),
    inference(cp,[status(thm)],[t14171,t33310]) ).

cnf(t221616,plain,
    rd(ld(X1,mult(rd(X1,X1),rd(X1,mult(X1,X1)))),X1) = ld(X1,rd(X2,mult(X1,mult(X1,X2)))),
    inference(step,[status(thm)],[t33466,t1088]) ).

cnf(t221617,plain,
    rd(ld(X1,rd(rd(X1,X1),X1)),X1) = ld(X1,rd(X2,mult(X1,mult(X1,X2)))),
    inference(step,[status(thm)],[t221616,t1132]) ).

cnf(t221618,plain,
    rd(ld(X1,rd(X1,mult(X1,X1))),X1) = ld(X1,rd(X2,mult(X1,mult(X1,X2)))),
    inference(step,[status(thm)],[t221617,t1088]) ).

cnf(t1573,plain,
    rd(mult(X1,X2),mult(X2,mult(X3,X2))) = rd(rd(X1,X3),X2),
    inference(cp,[status(thm)],[t1548,t12]) ).

cnf(t2425,plain,
    rd(mult(X1,X2),mult(X2,mult(X3,X2))) = rd(rd(X1,X3),X2),
    inference(orient,[status(thm)],[t1573]) ).

cnf(t2465,plain,
    rd(rd(X1,rd(X2,X3)),X3) = rd(mult(X1,X3),mult(X3,X2)),
    inference(cp,[status(thm)],[t2425,t8]) ).

cnf(t2493,plain,
    rd(rd(X1,rd(X2,X3)),X3) = rd(mult(X1,X3),mult(X3,X2)),
    inference(orient,[status(thm)],[t2465]) ).

cnf(t2949,plain,
    rd(X1,mult(X1,X1)) = rd(X2,rd(mult(X1,mult(X2,X1)),X1)),
    inference(cp,[status(thm)],[t24,t2930]) ).

cnf(t3170,plain,
    rd(X1,rd(mult(X2,mult(X1,X2)),X2)) = rd(X2,mult(X2,X2)),
    inference(orient,[status(thm)],[t2949]) ).

cnf(t3195,plain,
    rd(X1,mult(X1,X1)) = rd(rd(X2,X1),rd(mult(X1,X2),X1)),
    inference(cp,[status(thm)],[t3170,t8]) ).

cnf(t3388,plain,
    rd(rd(X1,X2),rd(mult(X2,X1),X2)) = rd(X2,mult(X2,X2)),
    inference(orient,[status(thm)],[t3195]) ).

cnf(t3448,plain,
    rd(mult(rd(X1,X2),X2),mult(X2,mult(X2,X1))) = rd(rd(X2,mult(X2,X2)),X2),
    inference(cp,[status(thm)],[t2493,t3388]) ).

cnf(t221610,plain,
    rd(X1,mult(X2,mult(X2,X1))) = rd(rd(X2,mult(X2,X2)),X2),
    inference(step,[status(thm)],[t3448,t8]) ).

cnf(t221611,plain,
    rd(X1,mult(X2,mult(X2,X1))) = rd(rd(X2,X2),mult(X2,X2)),
    inference(step,[status(thm)],[t221610,t2378]) ).

cnf(t221612,plain,
    rd(X1,mult(X2,mult(X2,X1))) = rd(X2,mult(X2,mult(X2,X2))),
    inference(step,[status(thm)],[t221611,t1605]) ).

cnf(t32405,plain,
    rd(X1,mult(X2,mult(X2,X1))) = rd(X2,mult(X2,mult(X2,X2))),
    inference(orient,[status(thm)],[t221612]) ).

cnf(t32591,plain,
    ld(X1,rd(X1,mult(X2,mult(X2,X2)))) = ld(X2,rd(X3,mult(X2,mult(X2,X3)))),
    inference(cp,[status(thm)],[t390,t32405]) ).

cnf(t23561,plain,
    mult(rd(X1,mult(rd(X2,X1),X2)),X2) = ld(rd(X2,X1),X1),
    inference(cp,[status(thm)],[t23507,t23]) ).

cnf(t24079,plain,
    mult(rd(X1,mult(rd(X2,X1),X2)),X2) = ld(rd(X2,X1),X1),
    inference(orient,[status(thm)],[t23561]) ).

cnf(t24181,plain,
    rd(X1,mult(rd(X2,X1),X2)) = rd(ld(rd(X2,X1),X1),X2),
    inference(cp,[status(thm)],[t12,t24079]) ).

cnf(t24258,plain,
    rd(ld(rd(X1,X2),X2),X1) = rd(X2,mult(rd(X1,X2),X1)),
    inference(orient,[status(thm)],[t24181]) ).

cnf(t24303,plain,
    rd(X1,mult(rd(mult(X2,X1),X1),mult(X2,X1))) = rd(ld(X2,X1),mult(X2,X1)),
    inference(cp,[status(thm)],[t24258,t12]) ).

cnf(t221537,plain,
    rd(X1,mult(X2,mult(X2,X1))) = rd(ld(X2,X1),mult(X2,X1)),
    inference(step,[status(thm)],[t24303,t12]) ).

cnf(t24642,plain,
    rd(ld(X1,X2),mult(X1,X2)) = rd(X2,mult(X1,mult(X1,X2))),
    inference(orient,[status(thm)],[t221537]) ).

cnf(t24779,plain,
    mult(X1,X2) = ld(rd(X2,mult(X1,mult(X1,X2))),ld(X1,X2)),
    inference(cp,[status(thm)],[t23,t24642]) ).

cnf(t24863,plain,
    ld(rd(X1,mult(X2,mult(X2,X1))),ld(X2,X1)) = mult(X2,X1),
    inference(orient,[status(thm)],[t24779]) ).

cnf(t1581,plain,
    X1 = ld(rd(X2,mult(X1,mult(X3,X1))),rd(rd(X2,X1),X3)),
    inference(cp,[status(thm)],[t23,t1548]) ).

cnf(t17768,plain,
    ld(rd(X1,mult(X2,mult(X3,X2))),rd(rd(X1,X2),X3)) = X2,
    inference(orient,[status(thm)],[t1581]) ).

cnf(t17865,plain,
    X1 = ld(rd(X2,mult(X1,mult(rd(mult(X1,X2),X1),X1))),rd(X1,mult(X1,X1))),
    inference(cp,[status(thm)],[t17768,t3388]) ).

cnf(t221546,plain,
    X1 = ld(rd(X2,mult(X1,mult(X1,X2))),rd(X1,mult(X1,X1))),
    inference(step,[status(thm)],[t17865,t8]) ).

cnf(t26226,plain,
    ld(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))) = X2,
    inference(orient,[status(thm)],[t221546]) ).

cnf(t26351,plain,
    mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))) = ld(rd(rd(X2,mult(X2,X2)),mult(rd(X1,mult(X2,mult(X2,X1))),mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))))),X2),
    inference(cp,[status(thm)],[t24863,t26226]) ).

cnf(t221562,plain,
    ld(X2,ld(X2,rd(X2,mult(X2,X2)))) = ld(rd(rd(X2,mult(X2,X2)),mult(rd(X1,mult(X2,mult(X2,X1))),mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))))),X2),
    inference(step,[status(thm)],[t26351,t21684]) ).

cnf(t20982,plain,
    ld(X1,ld(X1,rd(X2,mult(X1,X1)))) = rd(ld(mult(X1,X1),X2),mult(X1,X1)),
    inference(cp,[status(thm)],[t20980,t4017]) ).

cnf(t22668,plain,
    ld(X1,ld(X1,rd(X2,mult(X1,X1)))) = rd(ld(mult(X1,X1),X2),mult(X1,X1)),
    inference(orient,[status(thm)],[t20982]) ).

cnf(t221563,plain,
    rd(ld(mult(X2,X2),X2),mult(X2,X2)) = ld(rd(rd(X2,mult(X2,X2)),mult(rd(X1,mult(X2,mult(X2,X1))),mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))))),X2),
    inference(step,[status(thm)],[t221562,t22668]) ).

cnf(t221564,plain,
    rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(rd(rd(X2,mult(X2,X2)),mult(rd(X1,mult(X2,mult(X2,X1))),mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))))),X2),
    inference(step,[status(thm)],[t221563,t349]) ).

cnf(t221565,plain,
    rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(rd(rd(X2,mult(X2,X2)),ld(X2,ld(X2,mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2)))))),X2),
    inference(step,[status(thm)],[t221564,t21684]) ).

cnf(t221566,plain,
    rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(rd(rd(X2,mult(X2,X2)),ld(X2,ld(X2,ld(X2,ld(X2,rd(X2,mult(X2,X2))))))),X2),
    inference(step,[status(thm)],[t221565,t21684]) ).

cnf(t221567,plain,
    rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(rd(rd(X2,mult(X2,X2)),ld(X2,ld(X2,rd(ld(mult(X2,X2),X2),mult(X2,X2))))),X2),
    inference(step,[status(thm)],[t221566,t22668]) ).

cnf(t221568,plain,
    rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(rd(rd(X2,mult(X2,X2)),rd(ld(mult(X2,X2),ld(mult(X2,X2),X2)),mult(X2,X2))),X2),
    inference(step,[status(thm)],[t221567,t22668]) ).

cnf(t221569,plain,
    rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(mult(rd(X2,ld(mult(X2,X2),X2)),mult(X2,X2)),X2),
    inference(step,[status(thm)],[t221568,t3289]) ).

cnf(t221570,plain,
    rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(mult(mult(X2,X2),mult(X2,X2)),X2),
    inference(step,[status(thm)],[t221569,t24]) ).

cnf(t1054,plain,
    mult(ld(X1,X2),ld(X1,X2)) = ld(ld(X2,X1),ld(X1,X2)),
    inference(cp,[status(thm)],[t1053,t225]) ).

cnf(t221233,plain,
    rd(ld(X1,X2),ld(X2,X1)) = ld(ld(X2,X1),ld(X1,X2)),
    inference(step,[status(thm)],[t1054,t196]) ).

cnf(t1218,plain,
    ld(ld(X1,X2),ld(X2,X1)) = rd(ld(X2,X1),ld(X1,X2)),
    inference(orient,[status(thm)],[t221233]) ).

cnf(t1279,plain,
    rd(ld(rd(X1,mult(X1,X1)),X1),ld(X1,rd(X1,mult(X1,X1)))) = ld(rd(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),X1)),
    inference(cp,[status(thm)],[t1218,t1274]) ).

cnf(t221239,plain,
    mult(ld(rd(X1,mult(X1,X1)),X1),mult(X1,X1)) = ld(rd(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),X1)),
    inference(step,[status(thm)],[t1279,t216]) ).

cnf(t221240,plain,
    mult(mult(X1,X1),mult(X1,X1)) = ld(rd(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),X1)),
    inference(step,[status(thm)],[t221239,t23]) ).

cnf(t221241,plain,
    mult(mult(X1,X1),mult(X1,X1)) = ld(rd(rd(X1,mult(X1,X1)),X1),mult(X1,X1)),
    inference(step,[status(thm)],[t221240,t23]) ).

cnf(t221242,plain,
    mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(ld(rd(X1,mult(X1,X1)),X1),X1)),
    inference(step,[status(thm)],[t221241,t83]) ).

cnf(t221243,plain,
    mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(mult(X1,X1),X1)),
    inference(step,[status(thm)],[t221242,t23]) ).

cnf(t221244,plain,
    mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(X1,mult(X1,X1))),
    inference(step,[status(thm)],[t221243,t865]) ).

cnf(t1293,plain,
    mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(X1,mult(X1,X1))),
    inference(orient,[status(thm)],[t221244]) ).

cnf(t221571,plain,
    rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(mult(X2,mult(X2,mult(X2,X2))),X2),
    inference(step,[status(thm)],[t221570,t1293]) ).

cnf(t221572,plain,
    rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(true,rd(true,mult(X2,mult(X2,X2)))),
    inference(step,[status(thm)],[t221571,t349]) ).

cnf(t26900,plain,
    ld(true,rd(true,mult(X1,mult(X1,X1)))) = rd(ld(true,rd(true,X1)),mult(X1,X1)),
    inference(orient,[status(thm)],[t221572]) ).

cnf(t26902,plain,
    rd(ld(true,rd(true,X1)),mult(X1,X1)) = ld(X2,rd(X2,mult(X1,mult(X1,X1)))),
    inference(cp,[status(thm)],[t26900,t390]) ).

cnf(t28095,plain,
    ld(X1,rd(X1,mult(X2,mult(X2,X2)))) = rd(ld(true,rd(true,X2)),mult(X2,X2)),
    inference(orient,[status(thm)],[t26902]) ).

cnf(t221613,plain,
    rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(X2,rd(X3,mult(X2,mult(X2,X3)))),
    inference(step,[status(thm)],[t32591,t28095]) ).

cnf(t32686,plain,
    ld(X1,rd(X2,mult(X1,mult(X1,X2)))) = rd(ld(true,rd(true,X1)),mult(X1,X1)),
    inference(orient,[status(thm)],[t221613]) ).

cnf(t221619,plain,
    rd(ld(X1,rd(X1,mult(X1,X1))),X1) = rd(ld(true,rd(true,X1)),mult(X1,X1)),
    inference(step,[status(thm)],[t221618,t32686]) ).

cnf(t33676,plain,
    rd(ld(X1,rd(X1,mult(X1,X1))),X1) = rd(ld(true,rd(true,X1)),mult(X1,X1)),
    inference(orient,[status(thm)],[t221619]) ).

cnf(t33770,plain,
    rd(true,mult(X1,mult(X1,true))) = ld(X1,ld(ld(X1,rd(X1,mult(X1,X1))),rd(ld(true,rd(true,X1)),mult(X1,X1)))),
    inference(cp,[status(thm)],[t33311,t33676]) ).

cnf(t221620,plain,
    rd(true,mult(X1,mult(X1,true))) = ld(X1,rd(mult(mult(X1,X1),ld(true,rd(true,X1))),mult(X1,X1))),
    inference(step,[status(thm)],[t33770,t5016]) ).

cnf(t221621,plain,
    rd(true,mult(X1,mult(X1,true))) = ld(X1,rd(rd(mult(X1,X1),ld(rd(true,X1),true)),mult(X1,X1))),
    inference(step,[status(thm)],[t221620,t196]) ).

cnf(t221622,plain,
    rd(true,mult(X1,mult(X1,true))) = ld(X1,rd(rd(mult(X1,X1),X1),mult(X1,X1))),
    inference(step,[status(thm)],[t221621,t23]) ).

cnf(t221623,plain,
    rd(true,mult(X1,mult(X1,true))) = ld(X1,rd(X1,mult(X1,X1))),
    inference(step,[status(thm)],[t221622,t12]) ).

cnf(t33808,plain,
    ld(X1,rd(X1,mult(X1,X1))) = rd(true,mult(X1,mult(X1,true))),
    inference(orient,[status(thm)],[t221623]) ).

cnf(t33813,plain,
    rd(true,mult(X1,mult(X1,true))) = ld(X2,rd(X2,mult(X1,X1))),
    inference(cp,[status(thm)],[t33808,t390]) ).

cnf(t33894,plain,
    ld(X1,rd(X1,mult(X2,X2))) = rd(true,mult(X2,mult(X2,true))),
    inference(orient,[status(thm)],[t33813]) ).

cnf(t222110,plain,
    rd(rd(true,mult(X2,mult(X2,true))),ld(ld(rd(X2,X2),X3),X2)) = rd(ld(mult(X2,X2),ld(X2,mult(X3,mult(X2,X2)))),mult(X2,X2)),
    inference(step,[status(thm)],[t222109,t33894]) ).

cnf(t21709,plain,
    ld(X1,ld(X1,ld(X2,X3))) = rd(rd(Y3,mult(X1,mult(X1,Y3))),ld(X3,X2)),
    inference(cp,[status(thm)],[t21684,t196]) ).

cnf(t70827,plain,
    rd(rd(X1,mult(X2,mult(X2,X1))),ld(X3,Y3)) = ld(X2,ld(X2,ld(Y3,X3))),
    inference(orient,[status(thm)],[t21709]) ).

cnf(t222111,plain,
    ld(X2,ld(X2,ld(X2,ld(rd(X2,X2),X3)))) = rd(ld(mult(X2,X2),ld(X2,mult(X3,mult(X2,X2)))),mult(X2,X2)),
    inference(step,[status(thm)],[t222110,t70827]) ).

cnf(t222112,plain,
    ld(X2,ld(X2,mult(ld(X2,rd(X3,X2)),X2))) = rd(ld(mult(X2,X2),ld(X2,mult(X3,mult(X2,X2)))),mult(X2,X2)),
    inference(step,[status(thm)],[t222111,t505]) ).

cnf(t222113,plain,
    mult(ld(mult(X2,X2),ld(X2,rd(X3,X2))),X2) = rd(ld(mult(X2,X2),ld(X2,mult(X3,mult(X2,X2)))),mult(X2,X2)),
    inference(step,[status(thm)],[t222112,t457]) ).

cnf(t222114,plain,
    mult(ld(mult(X2,X2),ld(X2,rd(X3,X2))),X2) = rd(mult(ld(mult(X2,mult(X2,X2)),X3),mult(X2,X2)),mult(X2,X2)),
    inference(step,[status(thm)],[t222113,t457]) ).

cnf(t222115,plain,
    mult(ld(mult(X2,X2),ld(X2,rd(X3,X2))),X2) = ld(mult(X2,mult(X2,X2)),X3),
    inference(step,[status(thm)],[t222114,t12]) ).

cnf(t103285,plain,
    mult(ld(mult(X1,X1),ld(X1,rd(X2,X1))),X1) = ld(mult(X1,mult(X1,X1)),X2),
    inference(orient,[status(thm)],[t222115]) ).

cnf(t103498,plain,
    ld(mult(X1,mult(X1,X1)),mult(X2,X1)) = mult(ld(mult(X1,X1),ld(X1,X2)),X1),
    inference(cp,[status(thm)],[t103285,t12]) ).

cnf(t103690,plain,
    ld(mult(X1,mult(X1,X1)),mult(X2,X1)) = mult(ld(mult(X1,X1),ld(X1,X2)),X1),
    inference(orient,[status(thm)],[t103498]) ).

cnf(t103921,plain,
    ld(mult(X1,X2),mult(X2,mult(X2,X2))) = ld(X3,rd(X3,mult(ld(mult(X2,X2),ld(X2,X1)),X2))),
    inference(cp,[status(thm)],[t225,t103690]) ).

cnf(t476,plain,
    ld(ld(X1,mult(X2,X3)),X3) = ld(Y3,rd(Y3,mult(ld(mult(X1,X3),X2),X3))),
    inference(cp,[status(thm)],[t225,t457]) ).

cnf(t38444,plain,
    ld(X1,rd(X1,mult(ld(mult(X2,X3),Y3),X3))) = ld(ld(X2,mult(Y3,X3)),X3),
    inference(orient,[status(thm)],[t476]) ).

cnf(t222116,plain,
    ld(mult(X1,X2),mult(X2,mult(X2,X2))) = ld(ld(X2,mult(ld(X2,X1),X2)),X2),
    inference(step,[status(thm)],[t103921,t38444]) ).

cnf(t104353,plain,
    ld(ld(X1,mult(ld(X1,X2),X1)),X1) = ld(mult(X2,X1),mult(X1,mult(X1,X1))),
    inference(orient,[status(thm)],[t222116]) ).

cnf(t104540,plain,
    ld(X1,mult(ld(X1,X2),X1)) = rd(X1,ld(mult(X2,X1),mult(X1,mult(X1,X1)))),
    inference(cp,[status(thm)],[t24,t104353]) ).

cnf(t130246,plain,
    rd(X1,ld(mult(X2,X1),mult(X1,mult(X1,X1)))) = ld(X1,mult(ld(X1,X2),X1)),
    inference(orient,[status(thm)],[t104540]) ).

cnf(t130374,plain,
    ld(X1,mult(ld(X1,rd(X2,X1)),X1)) = rd(X1,ld(X2,mult(X1,mult(X1,X1)))),
    inference(cp,[status(thm)],[t130246,t8]) ).

cnf(t130617,plain,
    ld(X1,mult(ld(X1,rd(X2,X1)),X1)) = rd(X1,ld(X2,mult(X1,mult(X1,X1)))),
    inference(orient,[status(thm)],[t130374]) ).

cnf(t222460,plain,
    rd(X1,ld(mult(X1,X2),mult(X1,mult(X1,X1)))) = rd(ld(X1,mult(X2,X1)),X1),
    inference(step,[status(thm)],[t128657,t130617]) ).

cnf(t154018,plain,
    rd(X1,ld(mult(X1,X2),mult(X1,mult(X1,X1)))) = rd(ld(X1,mult(X2,X1)),X1),
    inference(orient,[status(thm)],[t222460]) ).

cnf(t154297,plain,
    ld(mult(X1,mult(X1,X1)),mult(X1,X2)) = ld(X1,rd(ld(X1,mult(X2,X1)),X1)),
    inference(cp,[status(thm)],[t225,t154018]) ).

cnf(t154728,plain,
    ld(mult(X1,mult(X1,X1)),mult(X1,X2)) = ld(X1,rd(ld(X1,mult(X2,X1)),X1)),
    inference(orient,[status(thm)],[t154297]) ).

cnf(t154939,plain,
    rd(ld(X1,mult(mult(X1,X2),mult(X1,X1))),mult(X1,X1)) = ld(ld(X3,rd(X3,mult(X1,X1))),ld(X1,rd(ld(X1,mult(X2,X1)),X1))),
    inference(cp,[status(thm)],[t39034,t154728]) ).

cnf(t66,plain,
    mult(X1,X2) = rd(rd(mult(X1,mult(X2,X3)),X2),rd(X3,X2)),
    inference(cp,[status(thm)],[t12,t56]) ).

cnf(t2770,plain,
    rd(rd(mult(X1,mult(X2,X3)),X2),rd(X3,X2)) = mult(X1,X2),
    inference(orient,[status(thm)],[t66]) ).

cnf(t55175,plain,
    mult(ld(X1,rd(X2,X1)),X1) = rd(rd(rd(ld(X1,mult(X2,mult(X1,X1))),X1),X1),rd(X1,X1)),
    inference(cp,[status(thm)],[t2770,t54946]) ).

cnf(t221985,plain,
    mult(ld(X1,rd(X2,X1)),X1) = rd(ld(X1,mult(X2,mult(X1,X1))),mult(X1,X1)),
    inference(step,[status(thm)],[t55175,t2329]) ).

cnf(t90563,plain,
    rd(ld(X1,mult(X2,mult(X1,X1))),mult(X1,X1)) = mult(ld(X1,rd(X2,X1)),X1),
    inference(orient,[status(thm)],[t221985]) ).

cnf(t222479,plain,
    mult(ld(X1,rd(mult(X1,X2),X1)),X1) = ld(ld(X3,rd(X3,mult(X1,X1))),ld(X1,rd(ld(X1,mult(X2,X1)),X1))),
    inference(step,[status(thm)],[t154939,t90563]) ).

cnf(t222480,plain,
    mult(ld(X1,rd(mult(X1,X2),X1)),X1) = ld(rd(true,mult(X1,mult(X1,true))),ld(X1,rd(ld(X1,mult(X2,X1)),X1))),
    inference(step,[status(thm)],[t222479,t33894]) ).

cnf(t222481,plain,
    mult(ld(X1,rd(mult(X1,X2),X1)),X1) = mult(X1,rd(ld(X1,mult(X2,X1)),X1)),
    inference(step,[status(thm)],[t222480,t29397]) ).

cnf(t26,plain,
    mult(mult(X1,X2),ld(X3,X1)) = mult(X3,mult(ld(X3,X1),mult(X2,ld(X3,X1)))),
    inference(cp,[status(thm)],[t25,t24]) ).

cnf(t221399,plain,
    rd(mult(X1,X2),ld(X1,X3)) = mult(X3,mult(ld(X3,X1),mult(X2,ld(X3,X1)))),
    inference(step,[status(thm)],[t26,t196]) ).

cnf(t221400,plain,
    rd(mult(X1,X2),ld(X1,X3)) = mult(X3,mult(ld(X3,X1),rd(X2,ld(X1,X3)))),
    inference(step,[status(thm)],[t221399,t196]) ).

cnf(t10456,plain,
    mult(X1,mult(ld(X1,X2),rd(X3,ld(X2,X1)))) = rd(mult(X2,X3),ld(X2,X1)),
    inference(orient,[status(thm)],[t221400]) ).

cnf(t10506,plain,
    rd(mult(rd(X1,X2),X3),ld(rd(X1,X2),X1)) = mult(X1,mult(rd(X2,mult(X2,X2)),rd(X3,ld(rd(X1,X2),X1)))),
    inference(cp,[status(thm)],[t10456,t1332]) ).

cnf(t221401,plain,
    rd(mult(rd(X1,X2),X3),X2) = mult(X1,mult(rd(X2,mult(X2,X2)),rd(X3,ld(rd(X1,X2),X1)))),
    inference(step,[status(thm)],[t10506,t23]) ).

cnf(t221402,plain,
    rd(mult(rd(X1,X2),X3),X2) = mult(X1,rd(ld(X2,mult(rd(X3,ld(rd(X1,X2),X1)),X2)),X2)),
    inference(step,[status(thm)],[t221401,t3965]) ).

cnf(t221403,plain,
    rd(mult(rd(X1,X2),X3),X2) = mult(X1,rd(ld(X2,rd(rd(X3,X2),ld(X1,rd(X1,X2)))),X2)),
    inference(step,[status(thm)],[t221402,t8439]) ).

cnf(t221404,plain,
    rd(mult(rd(X1,X2),X3),X2) = mult(X1,rd(ld(X2,mult(rd(X3,X2),X2)),X2)),
    inference(step,[status(thm)],[t221403,t216]) ).

cnf(t221405,plain,
    rd(mult(rd(X1,X2),X3),X2) = mult(X1,rd(ld(X2,X3),X2)),
    inference(step,[status(thm)],[t221404,t8]) ).

cnf(t10629,plain,
    mult(X1,rd(ld(X2,X3),X2)) = rd(mult(rd(X1,X2),X3),X2),
    inference(orient,[status(thm)],[t221405]) ).

cnf(t222482,plain,
    mult(ld(X1,rd(mult(X1,X2),X1)),X1) = rd(mult(rd(X1,X1),mult(X2,X1)),X1),
    inference(step,[status(thm)],[t222481,t10629]) ).

cnf(t155725,plain,
    mult(ld(X1,rd(mult(X1,X2),X1)),X1) = rd(mult(rd(X1,X1),mult(X2,X1)),X1),
    inference(orient,[status(thm)],[t222482]) ).

cnf(t155928,plain,
    ld(X1,rd(mult(X1,X2),X1)) = rd(rd(mult(rd(X1,X1),mult(X2,X1)),X1),X1),
    inference(cp,[status(thm)],[t12,t155725]) ).

cnf(t187119,plain,
    rd(rd(mult(rd(X1,X1),mult(X2,X1)),X1),X1) = ld(X1,rd(mult(X1,X2),X1)),
    inference(orient,[status(thm)],[t155928]) ).

cnf(t219914,plain,
    rd(mult(rd(rd(X1,X1),rd(X1,X1)),mult(X2,rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),rd(mult(rd(X1,X1),X2),rd(X1,X1))),
    inference(cp,[status(thm)],[t219881,t187119]) ).

cnf(t223072,plain,
    mult(rd(rd(X1,X1),rd(X1,X1)),mult(X2,rd(X1,X1))) = ld(rd(X1,X1),rd(mult(rd(X1,X1),X2),rd(X1,X1))),
    inference(step,[status(thm)],[t219914,t219881]) ).

cnf(t223073,plain,
    mult(rd(X1,X1),mult(X2,rd(X1,X1))) = ld(rd(X1,X1),rd(mult(rd(X1,X1),X2),rd(X1,X1))),
    inference(step,[status(thm)],[t223072,t219573]) ).

cnf(t222899,plain,
    mult(X1,rd(X2,X2)) = X1,
    inference(step,[status(thm)],[t617,t219881]) ).

cnf(t219882,plain,
    mult(X1,rd(X2,X2)) = X1,
    inference(orient,[status(thm)],[t222899]) ).

cnf(t223074,plain,
    mult(rd(X1,X1),X2) = ld(rd(X1,X1),rd(mult(rd(X1,X1),X2),rd(X1,X1))),
    inference(step,[status(thm)],[t223073,t219882]) ).

cnf(t223075,plain,
    mult(rd(X1,X1),X2) = rd(mult(rd(X1,X1),mult(rd(X1,X1),X2)),rd(X1,X1)),
    inference(step,[status(thm)],[t223074,t14646]) ).

cnf(t223076,plain,
    mult(rd(X1,X1),X2) = mult(rd(X1,X1),mult(rd(X1,X1),X2)),
    inference(step,[status(thm)],[t223075,t219881]) ).

cnf(t223077,plain,
    mult(rd(X1,X1),X2) = ld(rd(X1,X1),X2),
    inference(step,[status(thm)],[t223076,t4356]) ).

cnf(t106664,plain,
    mult(ld(X1,rd(mult(mult(X1,X1),X2),X1)),X1) = ld(X1,rd(mult(X1,mult(mult(X1,X2),X1)),X1)),
    inference(cp,[status(thm)],[t505,t106492]) ).

cnf(t222299,plain,
    ld(X1,rd(mult(X1,mult(X2,X1)),X1)) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
    inference(step,[status(thm)],[t9967,t129467]) ).

cnf(t129468,plain,
    ld(X1,rd(mult(X1,mult(X2,X1)),X1)) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
    inference(orient,[status(thm)],[t222299]) ).

cnf(t222337,plain,
    mult(ld(X1,rd(mult(mult(X1,X1),X2),X1)),X1) = mult(X1,rd(X1,ld(mult(X1,X2),mult(X1,X1)))),
    inference(step,[status(thm)],[t106664,t129468]) ).

cnf(t118512,plain,
    mult(rd(X1,X1),X2) = rd(X1,ld(mult(X1,X2),mult(X1,X1))),
    inference(cp,[status(thm)],[t24,t118442]) ).

cnf(t119424,plain,
    rd(X1,ld(mult(X1,X2),mult(X1,X1))) = mult(rd(X1,X1),X2),
    inference(orient,[status(thm)],[t118512]) ).

cnf(t222338,plain,
    mult(ld(X1,rd(mult(mult(X1,X1),X2),X1)),X1) = mult(X1,mult(rd(X1,X1),X2)),
    inference(step,[status(thm)],[t222337,t119424]) ).

cnf(t134298,plain,
    mult(ld(X1,rd(mult(mult(X1,X1),X2),X1)),X1) = mult(X1,mult(rd(X1,X1),X2)),
    inference(orient,[status(thm)],[t222338]) ).

cnf(t134445,plain,
    ld(X1,rd(mult(mult(X1,X1),X2),X1)) = rd(mult(X1,mult(rd(X1,X1),X2)),X1),
    inference(cp,[status(thm)],[t12,t134298]) ).

cnf(t134623,plain,
    ld(X1,rd(mult(mult(X1,X1),X2),X1)) = rd(mult(X1,mult(rd(X1,X1),X2)),X1),
    inference(orient,[status(thm)],[t134445]) ).

cnf(t134635,plain,
    rd(mult(X1,mult(rd(X1,X1),mult(X1,mult(X2,X1)))),X1) = ld(X1,mult(mult(mult(X1,X1),X1),X2)),
    inference(cp,[status(thm)],[t134623,t44]) ).

cnf(t222339,plain,
    rd(mult(X1,mult(mult(X1,X2),X1)),X1) = ld(X1,mult(mult(mult(X1,X1),X1),X2)),
    inference(step,[status(thm)],[t134635,t25]) ).

cnf(t222340,plain,
    rd(mult(X1,mult(mult(X1,X2),X1)),X1) = ld(X1,mult(mult(X1,mult(X1,X1)),X2)),
    inference(step,[status(thm)],[t222339,t865]) ).

cnf(t134911,plain,
    ld(X1,mult(mult(X1,mult(X1,X1)),X2)) = rd(mult(X1,mult(mult(X1,X2),X1)),X1),
    inference(orient,[status(thm)],[t222340]) ).

cnf(t134925,plain,
    rd(mult(X1,mult(mult(X1,mult(ld(X2,rd(X2,mult(X1,X1))),X3)),X1)),X1) = ld(X1,rd(mult(X1,mult(X3,mult(X1,X1))),mult(X1,X1))),
    inference(cp,[status(thm)],[t134911,t36653]) ).

cnf(t222342,plain,
    rd(mult(X1,mult(mult(X1,mult(rd(true,mult(X1,mult(X1,true))),X3)),X1)),X1) = ld(X1,rd(mult(X1,mult(X3,mult(X1,X1))),mult(X1,X1))),
    inference(step,[status(thm)],[t134925,t33894]) ).

cnf(t222343,plain,
    rd(mult(X1,mult(mult(X1,ld(X1,ld(X1,X3))),X1)),X1) = ld(X1,rd(mult(X1,mult(X3,mult(X1,X1))),mult(X1,X1))),
    inference(step,[status(thm)],[t222342,t21684]) ).

cnf(t222344,plain,
    rd(mult(X1,mult(rd(X1,ld(ld(X1,X3),X1)),X1)),X1) = ld(X1,rd(mult(X1,mult(X3,mult(X1,X1))),mult(X1,X1))),
    inference(step,[status(thm)],[t222343,t196]) ).

cnf(t222345,plain,
    rd(mult(X1,mult(ld(X1,X3),X1)),X1) = ld(X1,rd(mult(X1,mult(X3,mult(X1,X1))),mult(X1,X1))),
    inference(step,[status(thm)],[t222344,t24]) ).

cnf(t54677,plain,
    mult(mult(X1,rd(X2,X1)),X1) = rd(rd(rd(mult(X1,mult(X2,mult(X1,X1))),X1),X1),rd(X1,X1)),
    inference(cp,[status(thm)],[t2770,t54461]) ).

cnf(t221982,plain,
    mult(rd(X1,X1),mult(X1,X2)) = rd(rd(rd(mult(X1,mult(X2,mult(X1,X1))),X1),X1),rd(X1,X1)),
    inference(step,[status(thm)],[t54677,t34]) ).

cnf(t221983,plain,
    mult(rd(X1,X1),mult(X1,X2)) = rd(mult(X1,mult(X2,mult(X1,X1))),mult(X1,X1)),
    inference(step,[status(thm)],[t221982,t2329]) ).

cnf(t89916,plain,
    rd(mult(X1,mult(X2,mult(X1,X1))),mult(X1,X1)) = mult(rd(X1,X1),mult(X1,X2)),
    inference(orient,[status(thm)],[t221983]) ).

cnf(t222346,plain,
    rd(mult(X1,mult(ld(X1,X3),X1)),X1) = ld(X1,mult(rd(X1,X1),mult(X1,X3))),
    inference(step,[status(thm)],[t222345,t89916]) ).

cnf(t135474,plain,
    ld(X1,mult(rd(X1,X1),mult(X1,X2))) = rd(mult(X1,mult(ld(X1,X2),X1)),X1),
    inference(orient,[status(thm)],[t222346]) ).

cnf(t135482,plain,
    rd(mult(X1,mult(ld(X1,mult(X2,X1)),X1)),X1) = ld(X1,mult(mult(X1,X2),X1)),
    inference(cp,[status(thm)],[t135474,t25]) ).

cnf(t165210,plain,
    rd(mult(X1,mult(ld(X1,mult(X2,X1)),X1)),X1) = ld(X1,mult(mult(X1,X2),X1)),
    inference(orient,[status(thm)],[t135482]) ).

cnf(t165568,plain,
    rd(X1,mult(X1,mult(ld(mult(ld(X1,mult(X2,X1)),X1),X1),X1))) = ld(X1,ld(X1,ld(X1,mult(mult(X1,X2),X1)))),
    inference(cp,[status(thm)],[t119034,t165210]) ).

cnf(t472,plain,
    rd(X1,ld(ld(X2,mult(X3,Y3)),Y3)) = mult(X1,mult(ld(mult(X2,Y3),X3),Y3)),
    inference(cp,[status(thm)],[t196,t457]) ).

cnf(t8238,plain,
    mult(X1,mult(ld(mult(X2,X3),Y3),X3)) = rd(X1,ld(ld(X2,mult(Y3,X3)),X3)),
    inference(orient,[status(thm)],[t472]) ).

cnf(t222742,plain,
    rd(X1,rd(X1,ld(ld(ld(X1,mult(X2,X1)),mult(X1,X1)),X1))) = ld(X1,ld(X1,ld(X1,mult(mult(X1,X2),X1)))),
    inference(step,[status(thm)],[t165568,t8238]) ).

cnf(t222743,plain,
    rd(X1,ld(ld(X1,mult(X2,X1)),mult(X1,X1))) = ld(X1,ld(X1,ld(X1,mult(mult(X1,X2),X1)))),
    inference(step,[status(thm)],[t222742,t24]) ).

cnf(t222744,plain,
    rd(X1,ld(ld(X1,mult(X2,X1)),mult(X1,X1))) = ld(X1,mult(ld(mult(X1,X1),mult(X1,X2)),X1)),
    inference(step,[status(thm)],[t222743,t457]) ).

cnf(t4130,plain,
    mult(X1,mult(X1,X2)) = ld(rd(rd(X1,mult(X1,X1)),X1),X2),
    inference(cp,[status(thm)],[t4111,t1332]) ).

cnf(t221343,plain,
    mult(X1,mult(X1,X2)) = ld(rd(rd(X1,X1),mult(X1,X1)),X2),
    inference(step,[status(thm)],[t4130,t2378]) ).

cnf(t221344,plain,
    mult(X1,mult(X1,X2)) = ld(rd(X1,mult(X1,mult(X1,X1))),X2),
    inference(step,[status(thm)],[t221343,t1605]) ).

cnf(t4400,plain,
    ld(rd(X1,mult(X1,mult(X1,X1))),X2) = mult(X1,mult(X1,X2)),
    inference(orient,[status(thm)],[t221344]) ).

cnf(t4413,plain,
    mult(X1,mult(X1,X2)) = ld(ld(true,rd(true,mult(X1,X1))),X2),
    inference(cp,[status(thm)],[t4400,t3051]) ).

cnf(t4745,plain,
    ld(ld(true,rd(true,mult(X1,X1))),X2) = mult(X1,mult(X1,X2)),
    inference(orient,[status(thm)],[t4413]) ).

cnf(t4756,plain,
    mult(X1,mult(X1,X2)) = ld(ld(X3,rd(X3,mult(X1,X1))),X2),
    inference(cp,[status(thm)],[t4745,t390]) ).

cnf(t4943,plain,
    ld(ld(X1,rd(X1,mult(X2,X2))),X3) = mult(X2,mult(X2,X3)),
    inference(orient,[status(thm)],[t4756]) ).

cnf(t5010,plain,
    mult(mult(X1,X1),mult(X2,mult(X1,X1))) = mult(mult(X1,mult(X1,X2)),mult(X1,X1)),
    inference(cp,[status(thm)],[t3817,t4943]) ).

cnf(t14258,plain,
    mult(mult(X1,mult(X1,X2)),mult(X1,X1)) = mult(mult(X1,X1),mult(X2,mult(X1,X1))),
    inference(orient,[status(thm)],[t5010]) ).

cnf(t89949,plain,
    mult(rd(X1,X1),mult(X1,mult(X1,mult(X1,X2)))) = rd(mult(X1,mult(mult(X1,X1),mult(X2,mult(X1,X1)))),mult(X1,X1)),
    inference(cp,[status(thm)],[t89916,t14258]) ).

cnf(t222106,plain,
    mult(rd(X1,X1),mult(X1,mult(X1,mult(X1,X2)))) = mult(mult(X1,mult(X1,X1)),X2),
    inference(step,[status(thm)],[t89949,t44]) ).

cnf(t101526,plain,
    mult(rd(X1,X1),mult(X1,mult(X1,mult(X1,X2)))) = mult(mult(X1,mult(X1,X1)),X2),
    inference(orient,[status(thm)],[t222106]) ).

cnf(t101743,plain,
    mult(X1,rd(mult(X1,mult(X1,X2)),X1)) = rd(mult(mult(X1,mult(X1,X1)),X2),X1),
    inference(cp,[status(thm)],[t399,t101526]) ).

cnf(t102117,plain,
    mult(X1,rd(mult(X1,mult(X1,X2)),X1)) = rd(mult(mult(X1,mult(X1,X1)),X2),X1),
    inference(orient,[status(thm)],[t101743]) ).

cnf(t102277,plain,
    rd(mult(X1,mult(X1,X2)),X1) = ld(X1,rd(mult(mult(X1,mult(X1,X1)),X2),X1)),
    inference(cp,[status(thm)],[t9,t102117]) ).

cnf(t114892,plain,
    ld(X1,rd(mult(mult(X1,mult(X1,X1)),X2),X1)) = rd(mult(X1,mult(X1,X2)),X1),
    inference(orient,[status(thm)],[t102277]) ).

cnf(t114905,plain,
    rd(mult(X1,mult(X1,mult(X1,mult(X2,X1)))),X1) = ld(X1,mult(mult(mult(X1,mult(X1,X1)),X1),X2)),
    inference(cp,[status(thm)],[t114892,t44]) ).

cnf(t222408,plain,
    rd(mult(X1,mult(X1,mult(X1,mult(X2,X1)))),X1) = ld(X1,mult(mult(mult(X1,X1),mult(X1,X1)),X2)),
    inference(step,[status(thm)],[t114905,t1772]) ).

cnf(t222409,plain,
    rd(mult(X1,mult(X1,mult(X1,mult(X2,X1)))),X1) = ld(X1,mult(mult(X1,mult(X1,mult(X1,X1))),X2)),
    inference(step,[status(thm)],[t222408,t1293]) ).

cnf(t20180,plain,
    ld(ld(X1,X2),ld(ld(X1,X2),X3)) = mult(rd(ld(X2,X1),ld(X1,X2)),X3),
    inference(cp,[status(thm)],[t20144,t225]) ).

cnf(t21278,plain,
    ld(ld(X1,X2),ld(ld(X1,X2),X3)) = mult(rd(ld(X2,X1),ld(X1,X2)),X3),
    inference(orient,[status(thm)],[t20180]) ).

cnf(t21347,plain,
    mult(rd(ld(rd(X1,mult(X2,X2)),X1),ld(X1,rd(X1,mult(X2,X2)))),X3) = ld(ld(X1,rd(X1,mult(X2,X2))),mult(X2,mult(X2,X3))),
    inference(cp,[status(thm)],[t21278,t4943]) ).

cnf(t221522,plain,
    mult(mult(ld(rd(X1,mult(X2,X2)),X1),mult(X2,X2)),X3) = ld(ld(X1,rd(X1,mult(X2,X2))),mult(X2,mult(X2,X3))),
    inference(step,[status(thm)],[t21347,t216]) ).

cnf(t221523,plain,
    mult(mult(mult(X2,X2),mult(X2,X2)),X3) = ld(ld(X1,rd(X1,mult(X2,X2))),mult(X2,mult(X2,X3))),
    inference(step,[status(thm)],[t221522,t23]) ).

cnf(t221524,plain,
    mult(mult(X2,mult(X2,mult(X2,X2))),X3) = ld(ld(X1,rd(X1,mult(X2,X2))),mult(X2,mult(X2,X3))),
    inference(step,[status(thm)],[t221523,t1293]) ).

cnf(t221525,plain,
    mult(mult(X2,mult(X2,mult(X2,X2))),X3) = mult(X2,mult(X2,mult(X2,mult(X2,X3)))),
    inference(step,[status(thm)],[t221524,t4943]) ).

cnf(t23222,plain,
    mult(mult(X1,mult(X1,mult(X1,X1))),X2) = mult(X1,mult(X1,mult(X1,mult(X1,X2)))),
    inference(orient,[status(thm)],[t221525]) ).

cnf(t222410,plain,
    rd(mult(X1,mult(X1,mult(X1,mult(X2,X1)))),X1) = ld(X1,mult(X1,mult(X1,mult(X1,mult(X1,X2))))),
    inference(step,[status(thm)],[t222409,t23222]) ).

cnf(t222411,plain,
    rd(mult(X1,mult(X1,mult(X1,mult(X2,X1)))),X1) = mult(X1,mult(X1,mult(X1,X2))),
    inference(step,[status(thm)],[t222410,t9]) ).

cnf(t143726,plain,
    rd(mult(X1,mult(X1,mult(X1,mult(X2,X1)))),X1) = mult(X1,mult(X1,mult(X1,X2))),
    inference(orient,[status(thm)],[t222411]) ).

cnf(t143734,plain,
    mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),X2))) = mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))))),X1),
    inference(cp,[status(thm)],[t143726,t1174]) ).

cnf(t222601,plain,
    rd(ld(X1,mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),X2)),X1)),X1) = mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))))),X1),
    inference(step,[status(thm)],[t143734,t3965]) ).

cnf(t222602,plain,
    rd(ld(X1,mult(rd(ld(X1,mult(mult(rd(X1,mult(X1,X1)),X2),X1)),X1),X1)),X1) = mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))))),X1),
    inference(step,[status(thm)],[t222601,t3965]) ).

cnf(t222603,plain,
    rd(ld(X1,ld(X1,mult(mult(rd(X1,mult(X1,X1)),X2),X1))),X1) = mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))))),X1),
    inference(step,[status(thm)],[t222602,t8]) ).

cnf(t222604,plain,
    rd(mult(ld(mult(X1,X1),mult(rd(X1,mult(X1,X1)),X2)),X1),X1) = mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))))),X1),
    inference(step,[status(thm)],[t222603,t457]) ).

cnf(t222605,plain,
    ld(mult(X1,X1),mult(rd(X1,mult(X1,X1)),X2)) = mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))))),X1),
    inference(step,[status(thm)],[t222604,t12]) ).

cnf(t222606,plain,
    ld(mult(X1,X1),rd(ld(X1,mult(X2,X1)),X1)) = mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))))),X1),
    inference(step,[status(thm)],[t222605,t3965]) ).

cnf(t222607,plain,
    rd(ld(X1,ld(X1,ld(X1,mult(X2,X1)))),X1) = mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))))),X1),
    inference(step,[status(thm)],[t222606,t1429]) ).

cnf(t222608,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))))),X1),
    inference(step,[status(thm)],[t222607,t457]) ).

cnf(t222609,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = mult(rd(ld(X1,mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),X1)),X1),X1),
    inference(step,[status(thm)],[t222608,t3965]) ).

cnf(t222610,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = ld(X1,mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),X1)),
    inference(step,[status(thm)],[t222609,t8]) ).

cnf(t222611,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = ld(X1,mult(rd(ld(X1,mult(mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))),X1)),X1),X1)),
    inference(step,[status(thm)],[t222610,t3965]) ).

cnf(t222612,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = ld(X1,ld(X1,mult(mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))),X1))),
    inference(step,[status(thm)],[t222611,t8]) ).

cnf(t222613,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = mult(ld(mult(X1,X1),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),X1),
    inference(step,[status(thm)],[t222612,t457]) ).

cnf(t222614,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = mult(ld(mult(X1,X1),rd(ld(X1,mult(mult(X2,rd(X1,mult(X1,X1))),X1)),X1)),X1),
    inference(step,[status(thm)],[t222613,t3965]) ).

cnf(t222615,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = mult(rd(ld(X1,ld(X1,ld(X1,mult(mult(X2,rd(X1,mult(X1,X1))),X1)))),X1),X1),
    inference(step,[status(thm)],[t222614,t1429]) ).

cnf(t222616,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = ld(X1,ld(X1,ld(X1,mult(mult(X2,rd(X1,mult(X1,X1))),X1)))),
    inference(step,[status(thm)],[t222615,t8]) ).

cnf(t222617,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = ld(X1,mult(ld(mult(X1,X1),mult(X2,rd(X1,mult(X1,X1)))),X1)),
    inference(step,[status(thm)],[t222616,t457]) ).

cnf(t222618,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = ld(X1,mult(ld(mult(X1,X1),rd(X2,X1)),X1)),
    inference(step,[status(thm)],[t222617,t1132]) ).

cnf(t222619,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = ld(X1,mult(rd(ld(X1,ld(X1,X2)),X1),X1)),
    inference(step,[status(thm)],[t222618,t1429]) ).

cnf(t222620,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = ld(X1,ld(X1,ld(X1,X2))),
    inference(step,[status(thm)],[t222619,t8]) ).

cnf(t174544,plain,
    rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = ld(X1,ld(X1,ld(X1,X2))),
    inference(orient,[status(thm)],[t222620]) ).

cnf(t174725,plain,
    ld(X1,mult(ld(mult(X1,X1),X2),X1)) = mult(ld(X1,ld(X1,ld(X1,X2))),X1),
    inference(cp,[status(thm)],[t8,t174544]) ).

cnf(t175455,plain,
    ld(X1,mult(ld(mult(X1,X1),X2),X1)) = mult(ld(X1,ld(X1,ld(X1,X2))),X1),
    inference(orient,[status(thm)],[t174725]) ).

cnf(t222745,plain,
    rd(X1,ld(ld(X1,mult(X2,X1)),mult(X1,X1))) = mult(ld(X1,ld(X1,ld(X1,mult(X1,X2)))),X1),
    inference(step,[status(thm)],[t222744,t175455]) ).

cnf(t222746,plain,
    rd(X1,ld(ld(X1,mult(X2,X1)),mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),X1),
    inference(step,[status(thm)],[t222745,t9]) ).

cnf(t195158,plain,
    rd(X1,ld(ld(X1,mult(X2,X1)),mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),X1),
    inference(orient,[status(thm)],[t222746]) ).

cnf(t107735,plain,
    rd(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),ld(rd(X2,rd(X1,mult(X1,X1))),rd(X1,mult(X1,X1)))) = ld(rd(X1,mult(X1,X1)),ld(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),X1))),
    inference(cp,[status(thm)],[t107699,t1174]) ).

cnf(t222178,plain,
    rd(mult(rd(X1,mult(X1,X1)),X1),ld(rd(X2,rd(X1,mult(X1,X1))),rd(X1,mult(X1,X1)))) = ld(rd(X1,mult(X1,X1)),ld(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),X1))),
    inference(step,[status(thm)],[t107735,t1174]) ).

cnf(t222179,plain,
    rd(rd(rd(X1,X1),rd(X1,X1)),ld(rd(X2,rd(X1,mult(X1,X1))),rd(X1,mult(X1,X1)))) = ld(rd(X1,mult(X1,X1)),ld(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),X1))),
    inference(step,[status(thm)],[t222178,t2624]) ).

cnf(t222180,plain,
    rd(rd(X1,X1),ld(rd(X2,rd(X1,mult(X1,X1))),rd(X1,mult(X1,X1)))) = ld(rd(X1,mult(X1,X1)),ld(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),X1))),
    inference(step,[status(thm)],[t222179,t989]) ).

cnf(t222181,plain,
    rd(rd(X1,X1),ld(mult(X2,X1),rd(X1,mult(X1,X1)))) = ld(rd(X1,mult(X1,X1)),ld(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),X1))),
    inference(step,[status(thm)],[t222180,t1174]) ).

cnf(t1455,plain,
    rd(ld(X1,ld(X2,rd(X1,X1))),X1) = ld(mult(X2,X1),rd(X1,mult(X1,X1))),
    inference(cp,[status(thm)],[t1429,t1088]) ).

cnf(t11176,plain,
    ld(mult(X1,X2),rd(X2,mult(X2,X2))) = rd(ld(X2,ld(X1,rd(X2,X2))),X2),
    inference(orient,[status(thm)],[t1455]) ).

cnf(t222182,plain,
    rd(rd(X1,X1),rd(ld(X1,ld(X2,rd(X1,X1))),X1)) = ld(rd(X1,mult(X1,X1)),ld(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),X1))),
    inference(step,[status(thm)],[t222181,t11176]) ).

cnf(t222183,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = ld(rd(X1,mult(X1,X1)),ld(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),X1))),
    inference(step,[status(thm)],[t222182,t3289]) ).

cnf(t222184,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(mult(X1,mult(ld(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),X1)),X1)),X1),
    inference(step,[status(thm)],[t222183,t2930]) ).

cnf(t222185,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(mult(X1,mult(rd(mult(X1,mult(mult(mult(rd(X1,mult(X1,X1)),X2),X1),X1)),X1),X1)),X1),
    inference(step,[status(thm)],[t222184,t2930]) ).

cnf(t222186,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(mult(X1,mult(X1,mult(mult(mult(rd(X1,mult(X1,X1)),X2),X1),X1))),X1),
    inference(step,[status(thm)],[t222185,t8]) ).

cnf(t222187,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = mult(mult(X1,X1),mult(mult(rd(X1,mult(X1,X1)),X2),X1)),
    inference(step,[status(thm)],[t222186,t44]) ).

cnf(t222188,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = mult(mult(X1,X1),mult(rd(ld(X1,mult(X2,X1)),X1),X1)),
    inference(step,[status(thm)],[t222187,t3965]) ).

cnf(t222189,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = mult(mult(X1,X1),ld(X1,mult(X2,X1))),
    inference(step,[status(thm)],[t222188,t8]) ).

cnf(t222190,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(mult(X1,X1),ld(mult(X2,X1),X1)),
    inference(step,[status(thm)],[t222189,t196]) ).

cnf(t109355,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(mult(X1,X1),ld(mult(X2,X1),X1)),
    inference(orient,[status(thm)],[t222190]) ).

cnf(t120145,plain,
    rd(mult(X1,X1),ld(X2,X1)) = rd(X1,ld(X2,rd(X1,X1))),
    inference(cp,[status(thm)],[t120117,t24]) ).

cnf(t120510,plain,
    rd(mult(X1,X1),ld(X2,X1)) = rd(X1,ld(X2,rd(X1,X1))),
    inference(orient,[status(thm)],[t120145]) ).

cnf(t222260,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(X1,ld(mult(X2,X1),rd(X1,X1))),
    inference(step,[status(thm)],[t109355,t120510]) ).

cnf(t222261,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(X1,rd(ld(X1,ld(X2,X1)),X1)),
    inference(step,[status(thm)],[t222260,t1429]) ).

cnf(t120513,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(X1,rd(ld(X1,ld(X2,X1)),X1)),
    inference(orient,[status(thm)],[t222261]) ).

cnf(t195247,plain,
    mult(ld(X1,ld(X1,rd(X1,ld(X2,rd(X1,X1))))),X1) = rd(X1,ld(ld(X1,rd(X1,rd(ld(X1,ld(X2,X1)),X1))),mult(X1,X1))),
    inference(cp,[status(thm)],[t195158,t120513]) ).

cnf(t222747,plain,
    mult(ld(X1,ld(rd(X1,X1),X2)),X1) = rd(X1,ld(ld(X1,rd(X1,rd(ld(X1,ld(X2,X1)),X1))),mult(X1,X1))),
    inference(step,[status(thm)],[t195247,t225]) ).

cnf(t222748,plain,
    mult(mult(ld(X1,rd(X2,X1)),X1),X1) = rd(X1,ld(ld(X1,rd(X1,rd(ld(X1,ld(X2,X1)),X1))),mult(X1,X1))),
    inference(step,[status(thm)],[t222747,t505]) ).

cnf(t1476,plain,
    ld(rd(X1,X2),mult(X3,X2)) = ld(Y3,rd(Y3,rd(ld(X2,ld(X3,X1)),X2))),
    inference(cp,[status(thm)],[t225,t1429]) ).

cnf(t221691,plain,
    mult(X2,mult(ld(X1,X3),X2)) = ld(Y3,rd(Y3,rd(ld(X2,ld(X3,X1)),X2))),
    inference(step,[status(thm)],[t1476,t83]) ).

cnf(t44095,plain,
    ld(X1,rd(X1,rd(ld(X2,ld(X3,Y3)),X2))) = mult(X2,mult(ld(Y3,X3),X2)),
    inference(orient,[status(thm)],[t221691]) ).

cnf(t222749,plain,
    mult(mult(ld(X1,rd(X2,X1)),X1),X1) = rd(X1,ld(mult(X1,mult(ld(X1,X2),X1)),mult(X1,X1))),
    inference(step,[status(thm)],[t222748,t44095]) ).

cnf(t222750,plain,
    mult(mult(ld(X1,rd(X2,X1)),X1),X1) = mult(rd(X1,X1),mult(ld(X1,X2),X1)),
    inference(step,[status(thm)],[t222749,t119424]) ).

cnf(t195616,plain,
    mult(mult(ld(X1,rd(X2,X1)),X1),X1) = mult(rd(X1,X1),mult(ld(X1,X2),X1)),
    inference(orient,[status(thm)],[t222750]) ).

cnf(t195912,plain,
    mult(ld(X1,rd(X2,X1)),X1) = rd(mult(rd(X1,X1),mult(ld(X1,X2),X1)),X1),
    inference(cp,[status(thm)],[t12,t195616]) ).

cnf(t212873,plain,
    rd(mult(rd(X1,X1),mult(ld(X1,X2),X1)),X1) = mult(ld(X1,rd(X2,X1)),X1),
    inference(orient,[status(thm)],[t195912]) ).

cnf(t219910,plain,
    mult(rd(rd(X1,X1),rd(X1,X1)),mult(ld(rd(X1,X1),X2),rd(X1,X1))) = mult(ld(rd(X1,X1),rd(X2,rd(X1,X1))),rd(X1,X1)),
    inference(cp,[status(thm)],[t219881,t212873]) ).

cnf(t223004,plain,
    mult(rd(X1,X1),mult(ld(rd(X1,X1),X2),rd(X1,X1))) = mult(ld(rd(X1,X1),rd(X2,rd(X1,X1))),rd(X1,X1)),
    inference(step,[status(thm)],[t219910,t989]) ).

cnf(t223005,plain,
    mult(rd(X1,X1),ld(rd(X1,X1),X2)) = mult(ld(rd(X1,X1),rd(X2,rd(X1,X1))),rd(X1,X1)),
    inference(step,[status(thm)],[t223004,t219882]) ).

cnf(t223006,plain,
    rd(rd(X1,X1),ld(X2,rd(X1,X1))) = mult(ld(rd(X1,X1),rd(X2,rd(X1,X1))),rd(X1,X1)),
    inference(step,[status(thm)],[t223005,t196]) ).

cnf(t223007,plain,
    X2 = mult(ld(rd(X1,X1),rd(X2,rd(X1,X1))),rd(X1,X1)),
    inference(step,[status(thm)],[t223006,t24]) ).

cnf(t223008,plain,
    X2 = ld(rd(X1,X1),rd(X2,rd(X1,X1))),
    inference(step,[status(thm)],[t223007,t219882]) ).

cnf(t223009,plain,
    X2 = ld(rd(X1,X1),X2),
    inference(step,[status(thm)],[t223008,t219881]) ).

cnf(t220380,plain,
    ld(rd(X1,X1),X2) = X2,
    inference(orient,[status(thm)],[t223009]) ).

cnf(t223078,plain,
    mult(rd(X1,X1),X2) = X2,
    inference(step,[status(thm)],[t223077,t220380]) ).

cnf(t220831,plain,
    mult(rd(X1,X1),X2) = X2,
    inference(orient,[status(thm)],[t223078]) ).

fof(f5,conjecture,
    ! [X0,X1] :
      ( mult(ld(X1,X1),X0) = X0
      & mult(X0,ld(X1,X1)) = X0 ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).

fof(f5_neg,negated_conjecture,
    ~ ! [X0,X1] :
        ( mult(ld(X1,X1),X0) = X0
        & mult(X0,ld(X1,X1)) = X0 ),
    inference(negated_conjecture,[status(cth)],[f5]) ).

fof(f5_nnf,plain,
    ? [X0,X1] :
      ( mult(ld(X1,X1),X0) != X0
      | mult(X0,ld(X1,X1)) != X0 ),
    inference(nnf_transformation,[status(thm)],[f5_neg]) ).

fof(f5_sk,plain,
    ( mult(ld(sk1,sk1),sk0) != sk0
    | mult(sk0,ld(sk1,sk1)) != sk0 ),
    inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f5_nnf]) ).

cnf(c5,plain,
    ( mult(ld(sk1,sk1),sk0) != sk0
    | mult(sk0,ld(sk1,sk1)) != sk0 ),
    inference(cnf_transformation,[status(esa)],[f5_sk]) ).

cnf(goal_0,negated_conjecture,
    true != false,
    inference(equality_encoding,[status(esa)],[c5]) ).

cnf(g0_0,plain,
    true != ifeq(mult(sk0,ld(sk1,sk1)),sk0,ifeq(mult(ld(sk1,sk1),sk0),sk0,false,true),true),
    inference(rw,[status(thm)],[goal_0]) ).

cnf(g0_1,plain,
    true != ifeq(rd(sk0,ld(sk1,sk1)),sk0,ifeq(mult(ld(sk1,sk1),sk0),sk0,false,true),true),
    inference(rw,[status(thm)],[g0_0,t196]) ).

cnf(g0_2,plain,
    true != ifeq(rd(sk0,ld(sk1,sk1)),sk0,ifeq(mult(rd(sk1,sk1),sk0),sk0,false,true),true),
    inference(rw,[status(thm)],[g0_1,t614]) ).

cnf(g0_3,plain,
    true != ifeq(rd(sk0,rd(sk1,sk1)),sk0,ifeq(mult(rd(sk1,sk1),sk0),sk0,false,true),true),
    inference(rw,[status(thm)],[g0_2,t614]) ).

cnf(g0_4,plain,
    true != ifeq(sk0,sk0,ifeq(mult(rd(sk1,sk1),sk0),sk0,false,true),true),
    inference(rw,[status(thm)],[g0_3,t219881]) ).

cnf(g0_5,plain,
    true != ifeq(mult(rd(sk1,sk1),sk0),sk0,false,true),
    inference(rw,[status(thm)],[g0_4,t11]) ).

cnf(g0_6,plain,
    true != ifeq(sk0,sk0,false,true),
    inference(rw,[status(thm)],[g0_5,t220831]) ).

cnf(g0_7,plain,
    true != false,
    inference(rw,[status(thm)],[g0_6,t11]) ).

cnf(contradiction_0,plain,
    $false,
    inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP655+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04  % Command  : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.35  % Computer : n010.cluster.edu
% 0.10/0.35  % Model    : x86_64 x86_64
% 0.10/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35  % Memory   : 8046.5625MB
% 0.10/0.35  % OS       : Linux 6.8.0-71-generic
% 0.10/0.35  % CPULimit : 300
% 0.10/0.35  % WCLimit  : 300
% 0.10/0.35  % DateTime : Wed Sep 23 15:30:42 UTC 2026
% 0.10/0.35  % CPUTime  : 
% 0.10/0.35  Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 87.66/13.13  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 87.66/13.13  % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------