FindProof---0.1.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : FindProof---0.1
% Problem  : GRP655-10 : TPTP v9.3.1. Released v8.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300

% Computer : n016.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Fri Sep 25 01:27:51 PM UTC 2026

% Result   : Unsatisfiable 16.37s 14.40s
% Output   : CNFRefutation 16.37s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :  181
%            Number of leaves      :    8
% Syntax   : Number of clauses     :  998 ( 998 unt;   0 nHn;   6 RR)
%            Number of literals    :  998 ( 997 equ;   3 neg)
%            Maximal clause size   :    1 (   1 avg)
%            Maximal term depth    :   11 (   2 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :    9 (   9 usr;   2 con; 0-2 aty)
%            Number of variables   : 2211 (   0 sgn)

% Comments : 
%------------------------------------------------------------------------------
cnf(eg0,negated_conjecture,
    tuple(mult(X0,x1(X0)),mult(x1_2(X0),X0)) != tuple(x1(X0),x1_2(X0)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

cnf(t6,plain,
    eq(tuple(mult(X1,x1(X1)),mult(x1_2(X1),X1)),tuple(x1(X1),x1_2(X1))) = efalse,
    inference(equality_encoding,[status(esa)],[eg0]) ).

cnf(t22,plain,
    eq(tuple(mult(X1,x1(X1)),mult(x1_2(X1),X1)),tuple(x1(X1),x1_2(X1))) = efalse,
    inference(orient,[status(thm)],[t6]) ).

cnf(t4,axiom,
    rd(mult(X1,X2),X2) = X1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

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

cnf(t5,axiom,
    mult(mult(mult(X1,X2),X3),X2) = mult(X1,mult(X2,mult(X3,X2))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

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

cnf(t3,axiom,
    mult(rd(X1,X2),X2) = X1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

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

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

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

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(t39,plain,
    mult(X1,rd(X2,X3)) = rd(mult(rd(X1,X3),mult(X3,X2)),X3),
    inference(cp,[status(thm)],[t9,t34]) ).

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

cnf(t1,axiom,
    ld(X1,mult(X1,X2)) = X2,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

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

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

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

cnf(t2,axiom,
    mult(X1,ld(X1,X2)) = X2,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

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(t12,plain,
    X1 = ld(rd(X2,X1),X2),
    inference(cp,[status(thm)],[t11,t8]) ).

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

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

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

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

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

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(t411,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)],[t400,t131]) ).

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(t221223,plain,
    mult(mult(X1,ld(mult(X2,X3),X2)),X3) = mult(rd(X1,X3),X3),
    inference(step,[status(thm)],[t128,t7]) ).

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

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

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(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(t221228,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)],[t411,t216]) ).

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

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]) ).

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

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

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

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

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

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

cnf(t221232,plain,
    rd(X1,ld(X2,X2)) = mult(X1,rd(X2,X2)),
    inference(step,[status(thm)],[t582,t400]) ).

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

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

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

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

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

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

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

cnf(t221248,plain,
    rd(rd(X1,rd(X2,X2)),rd(X2,X2)) = X1,
    inference(step,[status(thm)],[t598,t616]) ).

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

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

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

cnf(t621,plain,
    X1 = rd(X1,rd(X1,X1)),
    inference(cp,[status(thm)],[t23,t616]) ).

cnf(t636,plain,
    rd(X1,rd(X1,X1)) = X1,
    inference(orient,[status(thm)],[t621]) ).

cnf(t641,plain,
    mult(X1,rd(X2,rd(X1,X1))) = rd(mult(X1,mult(rd(X1,X1),X2)),rd(X1,X1)),
    inference(cp,[status(thm)],[t400,t636]) ).

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

cnf(t40058,plain,
    mult(X1,mult(rd(X1,X1),X2)) = rd(mult(X1,rd(X2,rd(X1,X1))),rd(X1,X1)),
    inference(cp,[status(thm)],[t687,t39945]) ).

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

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(t104729,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(t637,plain,
    ld(X1,rd(X1,X2)) = rd(ld(X1,rd(X1,X2)),mult(ld(X1,rd(X1,X2)),X2)),
    inference(cp,[status(thm)],[t636,t216]) ).

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

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

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

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

cnf(t104819,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)],[t104729,t1668]) ).

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

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(t639,plain,
    rd(mult(X1,mult(rd(X2,X2),X2)),rd(X2,X2)) = mult(mult(X1,rd(X2,X2)),X2),
    inference(cp,[status(thm)],[t56,t636]) ).

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

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

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

cnf(t222158,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)],[t104819,t902]) ).

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

cnf(t479,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)],[t11,t479]) ).

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

cnf(t508,plain,
    mult(ld(X1,rd(mult(rd(X1,X2),X3),X2)),X2) = ld(X2,X3),
    inference(cp,[status(thm)],[t506,t11]) ).

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

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

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

cnf(t3768,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)],[t3761,t216]) ).

cnf(t221369,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)],[t3768,t216]) ).

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

cnf(t221371,plain,
    mult(ld(ld(X1,rd(X1,X2)),X3),X2) = ld(Y3,mult(Y3,mult(X2,mult(X3,X2)))),
    inference(step,[status(thm)],[t221370,t13]) ).

cnf(t221372,plain,
    mult(ld(ld(X1,rd(X1,X2)),X3),X2) = mult(X2,mult(X3,X2)),
    inference(step,[status(thm)],[t221371,t11]) ).

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

cnf(t3852,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)],[t3823,t216]) ).

cnf(t221376,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)],[t3852,t196]) ).

cnf(t221377,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)],[t221376,t24]) ).

cnf(t221378,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)],[t221377,t196]) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(t4679,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)],[t4628,t350]) ).

cnf(t221389,plain,
    ld(X2,mult(X1,X2)) = rd(mult(ld(mult(X1,X2),X1),X1),ld(X3,rd(X3,X2))),
    inference(step,[status(thm)],[t4679,t11]) ).

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

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

cnf(t4891,plain,
    mult(mult(ld(etrue,rd(etrue,X1)),X2),X1) = ld(X1,mult(X2,X1)),
    inference(orient,[status(thm)],[t221391]) ).

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

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

cnf(t4908,plain,
    ld(X1,mult(X2,X1)) = mult(mult(ld(X3,rd(X3,X1)),X2),X1),
    inference(cp,[status(thm)],[t4891,t391]) ).

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

cnf(t222159,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)],[t222158,t5118]) ).

cnf(t221240,plain,
    mult(rd(X1,rd(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
    inference(step,[status(thm)],[t569,t616]) ).

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

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

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

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

cnf(t222160,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)],[t222159,t903]) ).

cnf(t640,plain,
    mult(ld(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),ld(X1,X2)),
    inference(cp,[status(thm)],[t506,t636]) ).

cnf(t221236,plain,
    mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
    inference(step,[status(thm)],[t592,t616]) ).

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

cnf(t221691,plain,
    rd(ld(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),ld(X1,X2)),
    inference(step,[status(thm)],[t640,t619]) ).

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

cnf(t222161,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)],[t222160,t39789]) ).

cnf(t222162,plain,
    ld(rd(X2,X2),ld(X2,mult(X3,X2))) = ld(X2,mult(mult(rd(X2,X2),X3),X2)),
    inference(step,[status(thm)],[t222161,t5118]) ).

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

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

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

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

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

cnf(t221243,plain,
    rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
    inference(step,[status(thm)],[t310,t616]) ).

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

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

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

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

cnf(t221238,plain,
    ld(X1,rd(X1,X2)) = rd(rd(X2,X2),X2),
    inference(step,[status(thm)],[t322,t616]) ).

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

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

cnf(t1016,plain,
    rd(mult(rd(X1,X1),X1),rd(X1,X1)) = mult(ld(X2,rd(X2,X1)),mult(X1,X1)),
    inference(cp,[status(thm)],[t902,t999]) ).

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

cnf(t221267,plain,
    X1 = mult(ld(X2,rd(X2,X1)),mult(X1,X1)),
    inference(step,[status(thm)],[t221266,t636]) ).

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

cnf(t1045,plain,
    mult(X1,X1) = ld(ld(X2,rd(X2,X1)),X1),
    inference(cp,[status(thm)],[t11,t1028]) ).

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

cnf(t1058,plain,
    mult(X1,X1) = ld(rd(rd(X1,X1),X1),X1),
    inference(cp,[status(thm)],[t1056,t999]) ).

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

cnf(t1085,plain,
    rd(rd(X1,X1),X1) = rd(X1,mult(X1,X1)),
    inference(cp,[status(thm)],[t23,t1078]) ).

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

cnf(t221270,plain,
    rd(X1,rd(X2,mult(X2,X2))) = mult(X1,X2),
    inference(step,[status(thm)],[t654,t1091]) ).

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

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

cnf(t105377,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)],[t105369,t1178]) ).

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

cnf(t431,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)],[t11,t431]) ).

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

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

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

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

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

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

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

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

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

cnf(t221269,plain,
    mult(X1,rd(X2,mult(X2,X2))) = rd(X1,X2),
    inference(step,[status(thm)],[t671,t1091]) ).

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

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

cnf(t2862,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)],[t2858,t1135]) ).

cnf(t221335,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)],[t2862,t1135]) ).

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

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

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

cnf(t1546,plain,
    rd(rd(rd(X1,X2),X3),X2) = rd(X1,mult(X2,mult(X3,X2))),
    inference(cp,[status(thm)],[t23,t1515]) ).

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

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

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

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

cnf(t222163,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)],[t105377,t2936]) ).

cnf(t222164,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)],[t222163,t1135]) ).

cnf(t222165,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)],[t222164,t8]) ).

cnf(t222166,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)],[t222165,t1178]) ).

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

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

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

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

cnf(t222167,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)],[t222166,t2630]) ).

cnf(t905,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)],[t902,t654]) ).

cnf(t221259,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)],[t905,t671]) ).

cnf(t221260,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)],[t221259,t654]) ).

cnf(t221261,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)],[t221260,t8]) ).

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

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

cnf(t221264,plain,
    rd(rd(X1,X2),rd(X2,X2)) = rd(mult(X1,rd(X2,X2)),X2),
    inference(step,[status(thm)],[t221263,t671]) ).

cnf(t221265,plain,
    rd(rd(X1,X2),rd(X2,X2)) = rd(rd(X1,rd(X2,X2)),X2),
    inference(step,[status(thm)],[t221264,t619]) ).

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

cnf(t968,plain,
    rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
    inference(cp,[status(thm)],[t967,t636]) ).

cnf(t992,plain,
    rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
    inference(orient,[status(thm)],[t968]) ).

cnf(t222168,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)],[t222167,t992]) ).

cnf(t222169,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)],[t222168,t2630]) ).

cnf(t222170,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)],[t222169,t992]) ).

cnf(t222171,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)],[t222170,t2936]) ).

cnf(t222172,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)],[t222171,t1135]) ).

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

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

cnf(t105689,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)],[t105665,t44]) ).

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

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

cnf(t106628,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)],[t106530,t1135]) ).

cnf(t222191,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)],[t106628,t1178]) ).

cnf(t3828,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)],[t3823,t1135]) ).

cnf(t221373,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)],[t3828,t1135]) ).

cnf(t221374,plain,
    mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(ld(X3,mult(X3,X1)),X2),X1),
    inference(step,[status(thm)],[t221373,t1178]) ).

cnf(t221375,plain,
    mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(X1,X2),X1),
    inference(step,[status(thm)],[t221374,t11]) ).

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

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

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

cnf(t222192,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)],[t222191,t3971]) ).

cnf(t222193,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)],[t222192,t8]) ).

cnf(t222194,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)],[t222193,t1135]) ).

cnf(t222195,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)],[t222194,t8]) ).

cnf(t222196,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)],[t222195,t3971]) ).

cnf(t222197,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)],[t222196,t1178]) ).

cnf(t222198,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)],[t222197,t2630]) ).

cnf(t222199,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)],[t222198,t992]) ).

cnf(t1554,plain,
    rd(X1,mult(X2,mult(rd(X2,X2),X2))) = rd(rd(rd(X1,X2),X2),rd(X2,X2)),
    inference(cp,[status(thm)],[t1552,t967]) ).

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

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

cnf(t2362,plain,
    rd(rd(X1,X2),mult(X2,mult(rd(X2,X2),X2))) = rd(rd(X1,mult(X2,X2)),X2),
    inference(cp,[status(thm)],[t1552,t2335]) ).

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

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

cnf(t222200,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)],[t222199,t2384]) ).

cnf(t1557,plain,
    rd(X1,mult(X1,mult(X1,X1))) = rd(rd(X1,mult(X1,X1)),X1),
    inference(cp,[status(thm)],[t1552,t1091]) ).

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

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

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

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

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

cnf(t700,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)],[t697,t654]) ).

cnf(t221249,plain,
    rd(rd(X1,X1),X1) = ld(X1,rd(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1))),
    inference(step,[status(thm)],[t700,t11]) ).

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

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

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

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

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

cnf(t818,plain,
    rd(X1,X1) = rd(mult(X1,X1),mult(X1,X1)),
    inference(cp,[status(thm)],[t9,t810]) ).

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

cnf(t837,plain,
    rd(rd(mult(X1,X1),mult(X1,X1)),mult(X1,X1)) = ld(mult(X1,X1),rd(X1,X1)),
    inference(cp,[status(thm)],[t754,t828]) ).

cnf(t221258,plain,
    rd(rd(X1,X1),mult(X1,X1)) = ld(mult(X1,X1),rd(X1,X1)),
    inference(step,[status(thm)],[t837,t828]) ).

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

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

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

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

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

cnf(t221290,plain,
    rd(ld(X1,ld(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
    inference(step,[status(thm)],[t931,t1433]) ).

cnf(t221291,plain,
    rd(ld(X1,rd(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
    inference(step,[status(thm)],[t221290,t616]) ).

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

cnf(t702,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)],[t697,t216]) ).

cnf(t221286,plain,
    ld(X1,rd(X1,X2)) = ld(X2,rd(ld(X1,rd(X1,X2)),ld(X1,rd(X1,X2)))),
    inference(step,[status(thm)],[t702,t11]) ).

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

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

cnf(t1193,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)],[t697,t1178]) ).

cnf(t221271,plain,
    rd(X1,mult(X1,X1)) = ld(X1,rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1)))),
    inference(step,[status(thm)],[t1193,t11]) ).

cnf(t221272,plain,
    rd(X1,mult(X1,X1)) = ld(X1,mult(rd(X1,mult(X1,X1)),X1)),
    inference(step,[status(thm)],[t221271,t1178]) ).

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

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

cnf(t221273,plain,
    rd(X1,mult(X1,X1)) = ld(X1,rd(X1,X1)),
    inference(step,[status(thm)],[t221272,t1116]) ).

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

cnf(t221289,plain,
    ld(X1,rd(X1,X2)) = rd(X2,mult(X2,X2)),
    inference(step,[status(thm)],[t221288,t1200]) ).

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

cnf(t221292,plain,
    rd(rd(X1,mult(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
    inference(step,[status(thm)],[t1483,t1336]) ).

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

cnf(t221295,plain,
    rd(X1,mult(X1,mult(X1,X1))) = rd(rd(X1,X1),mult(X1,X1)),
    inference(step,[status(thm)],[t1557,t1484]) ).

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

cnf(t222201,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)],[t222200,t1609]) ).

cnf(t3907,plain,
    ld(rd(ld(X1,rd(X1,X2)),X2),X3) = mult(X2,mult(X2,mult(rd(X3,X2),X2))),
    inference(cp,[status(thm)],[t479,t3823]) ).

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

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

cnf(t4123,plain,
    mult(X1,mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3))) = X3,
    inference(cp,[status(thm)],[t4118,t11]) ).

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

cnf(t19899,plain,
    mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3)) = ld(X1,X3),
    inference(cp,[status(thm)],[t11,t19796]) ).

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

cnf(t20075,plain,
    mult(rd(ld(X1,rd(X1,X2)),X2),X3) = ld(X2,ld(X2,X3)),
    inference(cp,[status(thm)],[t11,t19972]) ).

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

cnf(t20264,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)],[t1433,t20164]) ).

cnf(t221553,plain,
    rd(ld(X1,mult(X3,mult(X3,Y3))),X1) = ld(ld(X3,ld(X3,X1)),rd(Y3,X1)),
    inference(step,[status(thm)],[t20264,t4118]) ).

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

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

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

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

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

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

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

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

cnf(t221554,plain,
    ld(X1,ld(X1,X2)) = mult(rd(X3,mult(X1,mult(X1,X3))),X2),
    inference(step,[status(thm)],[t21655,t3295]) ).

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

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

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

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

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

cnf(t3826,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)],[t3823,t196]) ).

cnf(t221467,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)],[t3826,t196]) ).

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

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

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

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

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,t23]) ).

cnf(t221670,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(t221671,plain,
    rd(ld(ld(X2,X1),ld(X2,X3)),ld(X2,X1)) = ld(X1,mult(X3,ld(X1,X2))),
    inference(step,[status(thm)],[t221670,t13661]) ).

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

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

cnf(t45508,plain,
    rd(rd(X1,ld(X2,X3)),ld(X1,X2)) = rd(X2,ld(X1,rd(X3,ld(X2,X1)))),
    inference(cp,[status(thm)],[t45506,t35133]) ).

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

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

cnf(t221252,plain,
    rd(mult(X1,X2),rd(X2,X2)) = rd(mult(X1,mult(X2,X2)),X2),
    inference(step,[status(thm)],[t597,t616]) ).

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

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

cnf(t221302,plain,
    mult(X1,mult(X2,X2)) = rd(mult(mult(X1,X2),X2),rd(X2,X2)),
    inference(step,[status(thm)],[t770,t903]) ).

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

cnf(t1761,plain,
    rd(mult(mult(mult(X1,X2),X2),X2),rd(X2,X2)) = mult(mult(X1,mult(X2,X2)),X2),
    inference(cp,[status(thm)],[t903,t1728]) ).

cnf(t221303,plain,
    mult(mult(X1,X2),mult(X2,X2)) = mult(mult(X1,mult(X2,X2)),X2),
    inference(step,[status(thm)],[t1761,t1728]) ).

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

cnf(t622,plain,
    mult(ld(X1,rd(rd(X1,X2),X2)),X2) = ld(X2,rd(rd(X1,X2),rd(X1,X2))),
    inference(cp,[status(thm)],[t506,t616]) ).

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

cnf(t9114,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)],[t9075,t687]) ).

cnf(t221426,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)],[t9114,t619]) ).

cnf(t221427,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)],[t221426,t1552]) ).

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

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

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

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

cnf(t4134,plain,
    mult(rd(X1,X1),mult(rd(X1,X1),X2)) = ld(rd(rd(X1,X1),rd(X1,X1)),X2),
    inference(cp,[status(thm)],[t4118,t646]) ).

cnf(t221383,plain,
    mult(rd(X1,X1),mult(rd(X1,X1),X2)) = ld(rd(X1,X1),X2),
    inference(step,[status(thm)],[t4134,t992]) ).

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

cnf(t221428,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)],[t221427,t4363]) ).

cnf(t221429,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)],[t221428,t616]) ).

cnf(t221430,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)],[t221429,t992]) ).

cnf(t221431,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)],[t221430,t616]) ).

cnf(t221432,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)],[t221431,t1552]) ).

cnf(t221433,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)],[t221432,t8]) ).

cnf(t221434,plain,
    rd(X1,mult(rd(X2,X2),X1)) = ld(rd(X2,X2),rd(X1,X1)),
    inference(step,[status(thm)],[t221433,t687]) ).

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

cnf(t9241,plain,
    mult(ld(X1,rd(rd(X2,X2),X1)),X1) = ld(X1,rd(X2,mult(rd(X1,X1),X2))),
    inference(cp,[status(thm)],[t506,t9203]) ).

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

cnf(t20197,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)],[t20164,t15280]) ).

cnf(t221542,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)],[t20197,t8]) ).

cnf(t221543,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)],[t221542,t8]) ).

cnf(t221544,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)],[t221543,t1091]) ).

cnf(t1191,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)],[t1056,t1178]) ).

cnf(t221278,plain,
    rd(rd(X1,mult(X1,X1)),X1) = ld(ld(X2,mult(X2,X1)),rd(X1,mult(X1,X1))),
    inference(step,[status(thm)],[t1191,t1135]) ).

cnf(t221279,plain,
    rd(rd(X1,mult(X1,X1)),X1) = ld(X1,rd(X1,mult(X1,X1))),
    inference(step,[status(thm)],[t221278,t11]) ).

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

cnf(t221293,plain,
    ld(X1,rd(X1,mult(X1,X1))) = rd(rd(X1,X1),mult(X1,X1)),
    inference(step,[status(thm)],[t1278,t1484]) ).

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

cnf(t221296,plain,
    ld(X1,rd(X1,mult(X1,X1))) = rd(X1,mult(X1,mult(X1,X1))),
    inference(step,[status(thm)],[t1485,t1609]) ).

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

cnf(t221545,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)],[t221544,t1610]) ).

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

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

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

cnf(t221549,plain,
    ld(X1,ld(X1,X2)) = mult(rd(rd(X1,X1),mult(X1,X1)),X2),
    inference(step,[status(thm)],[t221548,t2384]) ).

cnf(t221550,plain,
    ld(X1,ld(X1,X2)) = mult(rd(X1,mult(X1,mult(X1,X1))),X2),
    inference(step,[status(thm)],[t221549,t1609]) ).

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

cnf(t838,plain,
    mult(X1,X1) = rd(mult(X1,X1),rd(X1,X1)),
    inference(cp,[status(thm)],[t636,t828]) ).

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

cnf(t3016,plain,
    rd(ld(X1,rd(X1,X1)),X1) = ld(mult(mult(X1,X1),X1),X1),
    inference(cp,[status(thm)],[t3006,t853]) ).

cnf(t221342,plain,
    rd(rd(X1,mult(X1,X1)),X1) = ld(mult(mult(X1,X1),X1),X1),
    inference(step,[status(thm)],[t3016,t1336]) ).

cnf(t221343,plain,
    rd(rd(X1,X1),mult(X1,X1)) = ld(mult(mult(X1,X1),X1),X1),
    inference(step,[status(thm)],[t221342,t2384]) ).

cnf(t221344,plain,
    rd(X1,mult(X1,mult(X1,X1))) = ld(mult(mult(X1,X1),X1),X1),
    inference(step,[status(thm)],[t221343,t1609]) ).

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

cnf(t221253,plain,
    mult(X1,mult(X1,X1)) = mult(mult(X1,X1),X1),
    inference(step,[status(thm)],[t862,t9]) ).

cnf(t868,plain,
    mult(mult(X1,X1),X1) = mult(X1,mult(X1,X1)),
    inference(orient,[status(thm)],[t221253]) ).

cnf(t221345,plain,
    rd(X1,mult(X1,mult(X1,X1))) = ld(mult(X1,mult(X1,X1)),X1),
    inference(step,[status(thm)],[t221344,t868]) ).

cnf(t221346,plain,
    rd(X1,mult(X1,mult(X1,X1))) = ld(etrue,rd(etrue,mult(X1,X1))),
    inference(step,[status(thm)],[t221345,t350]) ).

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

cnf(t20502,plain,
    ld(X1,ld(X1,X2)) = mult(ld(etrue,rd(etrue,mult(X1,X1))),X2),
    inference(cp,[status(thm)],[t20472,t3057]) ).

cnf(t20735,plain,
    mult(ld(etrue,rd(etrue,mult(X1,X1))),X2) = ld(X1,ld(X1,X2)),
    inference(orient,[status(thm)],[t20502]) ).

cnf(t20763,plain,
    ld(X1,ld(X1,X2)) = mult(ld(X3,rd(X3,mult(X1,X1))),X2),
    inference(cp,[status(thm)],[t20735,t391]) ).

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

cnf(t21263,plain,
    ld(mult(X1,X1),mult(X2,mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),mult(X1,X1)),
    inference(cp,[status(thm)],[t5118,t21003]) ).

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

cnf(t3972,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)],[t3971,t25]) ).

cnf(t221770,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)],[t3972,t13]) ).

cnf(t21817,plain,
    X1 = ld(rd(X2,mult(X3,mult(X3,X2))),ld(X3,ld(X3,X1))),
    inference(cp,[status(thm)],[t11,t21708]) ).

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

cnf(t29158,plain,
    mult(X1,X2) = ld(rd(X3,mult(X1,mult(X1,X3))),ld(X1,X2)),
    inference(cp,[status(thm)],[t29041,t11]) ).

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

cnf(t29537,plain,
    mult(X1,mult(X1,X2)) = ld(rd(X3,mult(X1,mult(X1,X3))),X2),
    inference(cp,[status(thm)],[t29428,t11]) ).

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

cnf(t29829,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)],[t458,t29656]) ).

cnf(t221628,plain,
    mult(ld(ld(X2,ld(X2,X3)),Y3),X3) = ld(X3,mult(X2,mult(X2,mult(Y3,X3)))),
    inference(step,[status(thm)],[t29829,t21708]) ).

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

cnf(t221771,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)],[t221770,t30106]) ).

cnf(t221772,plain,
    ld(ld(X1,ld(X1,X1)),mult(X2,mult(X1,X1))) = mult(mult(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t221771,t9]) ).

cnf(t221773,plain,
    ld(ld(X1,rd(X1,X1)),mult(X2,mult(X1,X1))) = mult(mult(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t221772,t616]) ).

cnf(t221774,plain,
    ld(rd(X1,mult(X1,X1)),mult(X2,mult(X1,X1))) = mult(mult(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t221773,t1336]) ).

cnf(t221775,plain,
    rd(mult(X1,mult(mult(X2,mult(X1,X1)),X1)),X1) = mult(mult(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t221774,t2936]) ).

cnf(t221776,plain,
    rd(mult(X1,mult(mult(X2,X1),mult(X1,X1))),X1) = mult(mult(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t221775,t1776]) ).

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

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

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

cnf(t54636,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)],[t23109,t54494]) ).

cnf(t221778,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)],[t54636,t11]) ).

cnf(t221779,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)],[t221778,t1433]) ).

cnf(t221780,plain,
    mult(ld(X1,rd(X2,X1)),mult(X1,X1)) = rd(ld(X1,mult(X2,mult(X1,X1))),X1),
    inference(step,[status(thm)],[t221779,t11]) ).

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

cnf(t55165,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)],[t1776,t54979]) ).

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

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

cnf(t90302,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)],[t90256,t3761]) ).

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

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

cnf(t103062,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)],[t103051,t34]) ).

cnf(t2962,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)],[t506,t2936]) ).

cnf(t221755,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)],[t2962,t1433]) ).

cnf(t20272,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)],[t13,t20164]) ).

cnf(t221558,plain,
    ld(X2,ld(X2,mult(X3,mult(Y3,X3)))) = mult(mult(ld(X2,ld(X2,X3)),Y3),X3),
    inference(step,[status(thm)],[t20272,t20164]) ).

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

cnf(t221756,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)],[t221755,t22235]) ).

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

cnf(t221758,plain,
    mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = mult(ld(X1,rd(X1,X1)),X2),
    inference(step,[status(thm)],[t221757,t616]) ).

cnf(t221759,plain,
    mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = mult(rd(X1,mult(X1,X1)),X2),
    inference(step,[status(thm)],[t221758,t1336]) ).

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

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

cnf(t222279,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)],[t103062,t50597]) ).

cnf(t222280,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)],[t222279,t1609]) ).

cnf(t222281,plain,
    rd(ld(X1,mult(X2,X1)),X1) = ld(X1,ld(X1,ld(X1,mult(mult(X1,X1),X2)))),
    inference(step,[status(thm)],[t222280,t21708]) ).

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

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(t221679,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(t221680,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)],[t221679,t196]) ).

cnf(t221681,plain,
    mult(mult(X1,X3),mult(ld(X2,rd(X2,X3)),Y3)) = rd(mult(X1,mult(Y3,X3)),X3),
    inference(step,[status(thm)],[t221680,t24]) ).

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

cnf(t117002,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)],[t116973,t36685]) ).

cnf(t222282,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)],[t117002,t5118]) ).

cnf(t222283,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)],[t222282,t458]) ).

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

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

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

cnf(t105558,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)],[t23534,t105369]) ).

cnf(t222174,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)],[t105558,t196]) ).

cnf(t222175,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)],[t222174,t8]) ).

cnf(t222176,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)],[t222175,t105369]) ).

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

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

cnf(t1448,plain,
    rd(ld(X1,ld(ld(X2,rd(X2,X1)),X3)),X1) = ld(rd(X1,X1),rd(X3,X1)),
    inference(cp,[status(thm)],[t1433,t617]) ).

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

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

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

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

cnf(t4815,plain,
    rd(mult(X1,X2),X1) = ld(ld(X3,rd(X3,X1)),rd(X2,X1)),
    inference(cp,[status(thm)],[t4806,t391]) ).

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

cnf(t42642,plain,
    ld(rd(X1,X1),rd(rd(X2,X1),X1)) = rd(ld(X1,rd(mult(X1,X2),X1)),X1),
    inference(cp,[status(thm)],[t42631,t5023]) ).

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

cnf(t106019,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)],[t105963,t42907]) ).

cnf(t222188,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)],[t106019,t8]) ).

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

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

cnf(t222285,plain,
    ld(mult(X1,X1),X3) = ld(X1,rd(rd(X1,X1),ld(rd(mult(X3,X1),X1),X1))),
    inference(step,[status(thm)],[t222284,t107737]) ).

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

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

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

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

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

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

cnf(t120027,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)],[t45836,t119768]) ).

cnf(t222296,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)],[t120027,t216]) ).

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

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

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

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

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

cnf(t121853,plain,
    ld(X1,rd(mult(X1,X1),rd(X2,mult(X2,X2)))) = ld(rd(X1,X1),mult(X1,X2)),
    inference(cp,[status(thm)],[t121812,t1178]) ).

cnf(t222306,plain,
    ld(X1,mult(mult(X1,X1),X2)) = ld(rd(X1,X1),mult(X1,X2)),
    inference(step,[status(thm)],[t121853,t1178]) ).

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

cnf(t122549,plain,
    mult(ld(X1,rd(mult(X1,X2),X1)),X1) = ld(X1,ld(X1,mult(mult(X1,X1),X2))),
    inference(cp,[status(thm)],[t506,t122364]) ).

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

cnf(t128541,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)],[t108292,t128441]) ).

cnf(t222329,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)],[t128541,t13]) ).

cnf(t222330,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)],[t222329,t30106]) ).

cnf(t222331,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)],[t222330,t9]) ).

cnf(t222332,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)],[t222331,t616]) ).

cnf(t222333,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)],[t222332,t1336]) ).

cnf(t222334,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)],[t222333,t2936]) ).

cnf(t1102,plain,
    mult(ld(rd(X1,X1),rd(X2,X1)),X1) = ld(X1,ld(rd(X1,mult(X1,X1)),X2)),
    inference(cp,[status(thm)],[t506,t1091]) ).

cnf(t221436,plain,
    mult(ld(rd(X1,X1),rd(X2,X1)),X1) = ld(X1,rd(mult(X1,mult(X2,X1)),X1)),
    inference(step,[status(thm)],[t1102,t2936]) ).

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

cnf(t222335,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)],[t222334,t9977]) ).

cnf(t222336,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)],[t222335,t83]) ).

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

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

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

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

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

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

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

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

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

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

cnf(t222337,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)],[t222336,t119072]) ).

cnf(t222338,plain,
    mult(ld(rd(X1,X1),rd(X2,X1)),X1) = mult(X1,rd(rd(X1,X1),ld(X2,X1))),
    inference(step,[status(thm)],[t222337,t2570]) ).

cnf(t222339,plain,
    mult(ld(rd(X1,X1),rd(X2,X1)),X1) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
    inference(step,[status(thm)],[t222338,t119069]) ).

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

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

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

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

cnf(t221435,plain,
    mult(X1,mult(ld(rd(X1,X1),X2),X1)) = rd(mult(X1,mult(mult(X2,X1),X1)),X1),
    inference(step,[status(thm)],[t1095,t2936]) ).

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

cnf(t105744,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)],[t105665,t1135]) ).

cnf(t222180,plain,
    rd(mult(X1,rd(rd(X1,X1),X2)),X1) = ld(rd(X1,X1),rd(rd(X1,X2),X1)),
    inference(step,[status(thm)],[t105744,t1135]) ).

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

cnf(t107118,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)],[t9877,t106782]) ).

cnf(t222204,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)],[t107118,t8]) ).

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

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

cnf(t108928,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)],[t108859,t1178]) ).

cnf(t222234,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)],[t108928,t1178]) ).

cnf(t222235,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)],[t222234,t3971]) ).

cnf(t222236,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)],[t222235,t8]) ).

cnf(t222237,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)],[t222236,t1135]) ).

cnf(t1569,plain,
    rd(rd(X1,X1),mult(X1,mult(X2,X1))) = rd(rd(rd(X1,mult(X1,X1)),X2),X1),
    inference(cp,[status(thm)],[t1552,t1091]) ).

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

cnf(t222238,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)],[t222237,t11286]) ).

cnf(t222239,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)],[t222238,t2570]) ).

cnf(t222240,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)],[t222239,t1091]) ).

cnf(t222241,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)],[t222240,t3971]) ).

cnf(t222242,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)],[t222241,t3971]) ).

cnf(t222243,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)],[t222242,t8]) ).

cnf(t222244,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)],[t222243,t458]) ).

cnf(t222245,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)],[t222244,t9]) ).

cnf(t222246,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)],[t222245,t2630]) ).

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

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

cnf(t110242,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)],[t110205,t3295]) ).

cnf(t3310,plain,
    mult(rd(rd(X1,X1),X2),X1) = rd(rd(X1,mult(X1,X1)),rd(ld(X1,X2),X1)),
    inference(cp,[status(thm)],[t3295,t1091]) ).

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

cnf(t222254,plain,
    ld(X1,mult(rd(rd(X1,X1),X2),X1)) = ld(mult(X1,X1),mult(rd(X1,X2),X1)),
    inference(step,[status(thm)],[t110242,t52201]) ).

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

cnf(t111393,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,t111112]) ).

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

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

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

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

cnf(t160283,plain,
    mult(ld(rd(X1,X1),rd(X1,X2)),X1) = mult(X1,mult(rd(rd(X1,X1),X2),X1)),
    inference(cp,[status(thm)],[t160278,t141930]) ).

cnf(t222568,plain,
    mult(ld(X1,rd(mult(X1,X1),X2)),X1) = mult(X1,mult(rd(rd(X1,X1),X2),X1)),
    inference(step,[status(thm)],[t160283,t121812]) ).

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

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

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

cnf(t108541,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,t108292]) ).

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

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

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

cnf(t105950,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)],[t9877,t105665]) ).

cnf(t222186,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)],[t105950,t8]) ).

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

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

cnf(t107532,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)],[t107442,t1178]) ).

cnf(t222206,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)],[t107532,t1178]) ).

cnf(t222207,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)],[t222206,t3971]) ).

cnf(t222208,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)],[t222207,t8]) ).

cnf(t222209,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)],[t222208,t1135]) ).

cnf(t222210,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)],[t222209,t8]) ).

cnf(t222211,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)],[t222210,t3971]) ).

cnf(t222212,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)],[t222211,t3971]) ).

cnf(t222213,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)],[t222212,t3971]) ).

cnf(t222214,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)],[t222213,t8]) ).

cnf(t222215,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)],[t222214,t458]) ).

cnf(t222216,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)],[t222215,t9]) ).

cnf(t222217,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)],[t222216,t2630]) ).

cnf(t222218,plain,
    ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(mult(X1,X1),mult(rd(X1,X1),X2)),
    inference(step,[status(thm)],[t222217,t992]) ).

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

cnf(t109319,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,t109133]) ).

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

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

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

cnf(t222419,plain,
    ld(mult(rd(X1,X1),rd(X2,X1)),mult(X1,X1)) = ld(rd(ld(X1,X2),X1),X1),
    inference(step,[status(thm)],[t110043,t110787]) ).

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

cnf(t140772,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)],[t123877,t140472]) ).

cnf(t117446,plain,
    ld(mult(X1,X1),mult(X1,X2)) = ld(X1,rd(rd(X1,X1),ld(X3,rd(X3,X2)))),
    inference(cp,[status(thm)],[t117259,t350]) ).

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

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

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

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

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

cnf(t222420,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)],[t140772,t118480]) ).

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

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

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

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

cnf(t140948,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)],[t140837,t4201]) ).

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

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

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

cnf(t222614,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)],[t140948,t55661]) ).

cnf(t222615,plain,
    ld(rd(rd(X1,mult(X1,X1)),X2),rd(X1,X1)) = ld(rd(X1,X2),mult(X1,X1)),
    inference(step,[status(thm)],[t222614,t1135]) ).

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

cnf(t9207,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)],[t9203,t1178]) ).

cnf(t221885,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)],[t9207,t1135]) ).

cnf(t221886,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)],[t221885,t2630]) ).

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

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

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

cnf(t168315,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)],[t168309,t63916]) ).

cnf(t9212,plain,
    rd(rd(X1,X1),mult(rd(X2,X2),rd(X1,X1))) = ld(rd(X2,X2),rd(X1,X1)),
    inference(cp,[status(thm)],[t9203,t992]) ).

cnf(t221896,plain,
    rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = ld(rd(X2,X2),rd(X1,X1)),
    inference(step,[status(thm)],[t9212,t619]) ).

cnf(t221897,plain,
    rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = rd(X1,mult(rd(X2,X2),X1)),
    inference(step,[status(thm)],[t221896,t9203]) ).

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

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

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

cnf(t222795,plain,
    ld(rd(X1,rd(rd(X2,X2),X1)),mult(X1,X1)) = rd(rd(X2,X2),rd(X1,X1)),
    inference(step,[status(thm)],[t168315,t94702]) ).

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

cnf(t198433,plain,
    rd(X1,rd(rd(X2,X2),X1)) = rd(mult(X1,X1),rd(rd(X2,X2),rd(X1,X1))),
    inference(cp,[status(thm)],[t23,t198305]) ).

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

cnf(t214783,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)],[t160696,t214572]) ).

cnf(t222906,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)],[t214783,t64760]) ).

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

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

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

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

cnf(t85035,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)],[t85028,t216]) ).

cnf(t221990,plain,
    ld(X1,rd(rd(rd(X1,X2),X3),X2)) = ld(mult(mult(X1,X3),X2),rd(X1,X2)),
    inference(step,[status(thm)],[t85035,t24]) ).

cnf(t221991,plain,
    ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = ld(mult(mult(X1,X3),X2),rd(X1,X2)),
    inference(step,[status(thm)],[t221990,t1552]) ).

cnf(t221992,plain,
    ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = rd(ld(X2,ld(mult(X1,X3),X1)),X2),
    inference(step,[status(thm)],[t221991,t1433]) ).

cnf(t221993,plain,
    ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = rd(ld(X2,ld(etrue,rd(etrue,X3))),X2),
    inference(step,[status(thm)],[t221992,t350]) ).

cnf(t85414,plain,
    ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = rd(ld(X2,ld(etrue,rd(etrue,X3))),X2),
    inference(orient,[status(thm)],[t221993]) ).

cnf(t85484,plain,
    rd(ld(rd(X1,mult(X1,X1)),ld(etrue,rd(etrue,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)],[t85414,t3971]) ).

cnf(t221998,plain,
    mult(ld(rd(X1,mult(X1,X1)),ld(etrue,rd(etrue,X2))),X1) = ld(X3,rd(X3,rd(ld(X1,mult(mult(X2,rd(X1,mult(X1,X1))),X1)),X1))),
    inference(step,[status(thm)],[t85484,t1178]) ).

cnf(t221999,plain,
    mult(rd(mult(X1,mult(ld(etrue,rd(etrue,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)],[t221998,t2936]) ).

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

cnf(t222001,plain,
    mult(X1,mult(ld(etrue,rd(etrue,X2)),X1)) = ld(X3,rd(X3,rd(ld(X1,mult(rd(X2,X1),X1)),X1))),
    inference(step,[status(thm)],[t222000,t1135]) ).

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

cnf(t86105,plain,
    ld(X1,rd(X1,rd(ld(X2,X3),X2))) = mult(X2,mult(ld(etrue,rd(etrue,X3)),X2)),
    inference(orient,[status(thm)],[t222002]) ).

cnf(t86198,plain,
    mult(X1,mult(ld(etrue,rd(etrue,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)],[t86105,t15280]) ).

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

cnf(t221898,plain,
    rd(X2,mult(rd(X1,X1),X2)) = ld(X3,rd(X3,rd(X1,mult(rd(X2,X2),X1)))),
    inference(step,[status(thm)],[t9244,t9203]) ).

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

cnf(t222142,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)],[t86198,t64964]) ).

cnf(t222143,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)],[t222142,t9]) ).

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

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

cnf(t222907,plain,
    ld(rd(rd(X2,X2),X1),X1) = mult(ld(X1,rd(X1,rd(rd(X2,X2),X1))),X1),
    inference(step,[status(thm)],[t222906,t100771]) ).

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

cnf(t9217,plain,
    rd(X1,X1) = rd(rd(X2,X2),rd(X2,mult(rd(X1,X1),X2))),
    inference(cp,[status(thm)],[t23,t9203]) ).

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

cnf(t219289,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)],[t219231,t9252]) ).

cnf(t222908,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)],[t219289,t9252]) ).

cnf(t15325,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)],[t15280,t992]) ).

cnf(t221927,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)],[t15325,t619]) ).

cnf(t5031,plain,
    rd(mult(rd(X1,X1),X2),rd(X1,X1)) = ld(rd(X1,X1),rd(X2,rd(X1,X1))),
    inference(cp,[status(thm)],[t5023,t646]) ).

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

cnf(t221928,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)],[t221927,t14660]) ).

cnf(t221929,plain,
    mult(rd(X1,X1),rd(X2,X2)) = ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))),
    inference(step,[status(thm)],[t221928,t687]) ).

cnf(t221930,plain,
    rd(rd(X1,X1),rd(X2,X2)) = ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))),
    inference(step,[status(thm)],[t221929,t619]) ).

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

cnf(t222909,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)],[t222908,t68297]) ).

cnf(t9202,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)],[t3823,t9075]) ).

cnf(t221876,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)],[t9202,t216]) ).

cnf(t221877,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)],[t221876,t3107]) ).

cnf(t221878,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)],[t221877,t216]) ).

cnf(t221879,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)],[t221878,t196]) ).

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

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

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

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

cnf(t221880,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)],[t221879,t8447]) ).

cnf(t221881,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)],[t221880,t216]) ).

cnf(t221882,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)],[t221881,t8]) ).

cnf(t221883,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)],[t221882,t216]) ).

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

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

cnf(t63696,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)],[t63683,t216]) ).

cnf(t222043,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)],[t63696,t196]) ).

cnf(t222044,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)],[t222043,t196]) ).

cnf(t222045,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)],[t222044,t24]) ).

cnf(t222046,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)],[t222045,t24]) ).

cnf(t222047,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)],[t222046,t3823]) ).

cnf(t222048,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)],[t222047,t196]) ).

cnf(t222049,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)],[t222048,t8447]) ).

cnf(t222050,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)],[t222049,t216]) ).

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

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

cnf(t222910,plain,
    rd(rd(X2,X2),rd(X1,X1)) = ld(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2))),
    inference(step,[status(thm)],[t222909,t93691]) ).

cnf(t222911,plain,
    rd(rd(X2,X2),rd(X1,X1)) = ld(X1,X1),
    inference(step,[status(thm)],[t222910,t687]) ).

cnf(t222912,plain,
    rd(rd(X2,X2),rd(X1,X1)) = rd(X1,X1),
    inference(step,[status(thm)],[t222911,t616]) ).

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

cnf(t219823,plain,
    mult(X1,mult(rd(X1,X1),rd(X2,X2))) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
    inference(cp,[status(thm)],[t81301,t219611]) ).

cnf(t222936,plain,
    mult(X1,rd(rd(X1,X1),rd(X2,X2))) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
    inference(step,[status(thm)],[t219823,t619]) ).

cnf(t222937,plain,
    mult(X1,rd(X2,X2)) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
    inference(step,[status(thm)],[t222936,t219611]) ).

cnf(t222938,plain,
    rd(X1,rd(X2,X2)) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
    inference(step,[status(thm)],[t222937,t619]) ).

cnf(t222939,plain,
    rd(X1,rd(X2,X2)) = X1,
    inference(step,[status(thm)],[t222938,t9]) ).

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

cnf(t515,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)],[t506,t216]) ).

cnf(t221685,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)],[t515,t196]) ).

cnf(t221686,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)],[t221685,t216]) ).

cnf(t221687,plain,
    rd(ld(X1,mult(X2,Y3)),Y3) = ld(ld(X3,rd(X3,Y3)),ld(mult(X1,Y3),X2)),
    inference(step,[status(thm)],[t221686,t24]) ).

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

cnf(t222325,plain,
    ld(X1,mult(ld(X1,rd(mult(X1,X2),X1)),X1)) = rd(ld(X1,mult(X2,X1)),X1),
    inference(step,[status(thm)],[t116973,t128441]) ).

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

cnf(t3979,plain,
    rd(ld(X1,mult(X2,X1)),X1) = mult(ld(X3,rd(X3,X1)),X2),
    inference(cp,[status(thm)],[t3971,t1336]) ).

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

cnf(t90597,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)],[t32890,t90256]) ).

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

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

cnf(t222150,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)],[t90597,t8706]) ).

cnf(t1062,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)],[t1056,t216]) ).

cnf(t221275,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)],[t1062,t196]) ).

cnf(t221276,plain,
    rd(ld(X1,rd(X1,X2)),X2) = ld(ld(X3,mult(X3,X2)),ld(X1,rd(X1,X2))),
    inference(step,[status(thm)],[t221275,t24]) ).

cnf(t221277,plain,
    rd(ld(X1,rd(X1,X2)),X2) = ld(X2,ld(X1,rd(X1,X2))),
    inference(step,[status(thm)],[t221276,t11]) ).

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

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

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

cnf(t221655,plain,
    ld(X1,ld(X2,rd(X2,X1))) = rd(etrue,mult(X1,mult(X1,etrue))),
    inference(step,[status(thm)],[t1257,t33342]) ).

cnf(t33343,plain,
    ld(X1,ld(X2,rd(X2,X1))) = rd(etrue,mult(X1,mult(X1,etrue))),
    inference(orient,[status(thm)],[t221655]) ).

cnf(t4394,plain,
    rd(ld(X1,mult(rd(X1,X1),X2)),X1) = ld(X1,rd(ld(rd(X1,X1),X2),X1)),
    inference(cp,[status(thm)],[t3761,t4363]) ).

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

cnf(t33498,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)],[t14185,t33342]) ).

cnf(t221657,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)],[t33498,t1091]) ).

cnf(t221658,plain,
    rd(ld(X1,rd(rd(X1,X1),X1)),X1) = ld(X1,rd(X2,mult(X1,mult(X1,X2)))),
    inference(step,[status(thm)],[t221657,t1135]) ).

cnf(t221659,plain,
    rd(ld(X1,rd(X1,mult(X1,X1))),X1) = ld(X1,rd(X2,mult(X1,mult(X1,X2)))),
    inference(step,[status(thm)],[t221658,t1091]) ).

cnf(t1577,plain,
    rd(mult(X1,X2),mult(X2,mult(X3,X2))) = rd(rd(X1,X3),X2),
    inference(cp,[status(thm)],[t1552,t9]) ).

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

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

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

cnf(t2955,plain,
    rd(X1,mult(X1,X1)) = rd(X2,rd(mult(X1,mult(X2,X1)),X1)),
    inference(cp,[status(thm)],[t23,t2936]) ).

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

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

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

cnf(t3454,plain,
    rd(mult(rd(X1,X2),X2),mult(X2,mult(X2,X1))) = rd(rd(X2,mult(X2,X2)),X2),
    inference(cp,[status(thm)],[t2499,t3394]) ).

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

cnf(t221652,plain,
    rd(X1,mult(X2,mult(X2,X1))) = rd(rd(X2,X2),mult(X2,X2)),
    inference(step,[status(thm)],[t221651,t2384]) ).

cnf(t221653,plain,
    rd(X1,mult(X2,mult(X2,X1))) = rd(X2,mult(X2,mult(X2,X2))),
    inference(step,[status(thm)],[t221652,t1609]) ).

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

cnf(t32622,plain,
    ld(X1,rd(X1,mult(X2,mult(X2,X2)))) = ld(X2,rd(X3,mult(X2,mult(X2,X3)))),
    inference(cp,[status(thm)],[t391,t32436]) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(t17885,plain,
    X1 = ld(rd(X2,mult(X1,mult(rd(mult(X1,X2),X1),X1))),rd(X1,mult(X1,X1))),
    inference(cp,[status(thm)],[t17788,t3394]) ).

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

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

cnf(t26379,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)],[t24891,t26254]) ).

cnf(t221603,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)],[t26379,t21708]) ).

cnf(t21005,plain,
    ld(X1,ld(X1,rd(X2,mult(X1,X1)))) = rd(ld(mult(X1,X1),X2),mult(X1,X1)),
    inference(cp,[status(thm)],[t21003,t4024]) ).

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

cnf(t221604,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)],[t221603,t22693]) ).

cnf(t221605,plain,
    rd(ld(etrue,rd(etrue,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)],[t221604,t350]) ).

cnf(t221606,plain,
    rd(ld(etrue,rd(etrue,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)],[t221605,t21708]) ).

cnf(t221607,plain,
    rd(ld(etrue,rd(etrue,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)],[t221606,t21708]) ).

cnf(t221608,plain,
    rd(ld(etrue,rd(etrue,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)],[t221607,t22693]) ).

cnf(t221609,plain,
    rd(ld(etrue,rd(etrue,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)],[t221608,t22693]) ).

cnf(t221610,plain,
    rd(ld(etrue,rd(etrue,X2)),mult(X2,X2)) = ld(mult(rd(X2,ld(mult(X2,X2),X2)),mult(X2,X2)),X2),
    inference(step,[status(thm)],[t221609,t3295]) ).

cnf(t221611,plain,
    rd(ld(etrue,rd(etrue,X2)),mult(X2,X2)) = ld(mult(mult(X2,X2),mult(X2,X2)),X2),
    inference(step,[status(thm)],[t221610,t23]) ).

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

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

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

cnf(t1283,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)],[t1222,t1278]) ).

cnf(t221280,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)],[t1283,t216]) ).

cnf(t221281,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)],[t221280,t24]) ).

cnf(t221282,plain,
    mult(mult(X1,X1),mult(X1,X1)) = ld(rd(rd(X1,mult(X1,X1)),X1),mult(X1,X1)),
    inference(step,[status(thm)],[t221281,t24]) ).

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

cnf(t221284,plain,
    mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(mult(X1,X1),X1)),
    inference(step,[status(thm)],[t221283,t24]) ).

cnf(t221285,plain,
    mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(X1,mult(X1,X1))),
    inference(step,[status(thm)],[t221284,t868]) ).

cnf(t1297,plain,
    mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(X1,mult(X1,X1))),
    inference(orient,[status(thm)],[t221285]) ).

cnf(t221612,plain,
    rd(ld(etrue,rd(etrue,X2)),mult(X2,X2)) = ld(mult(X2,mult(X2,mult(X2,X2))),X2),
    inference(step,[status(thm)],[t221611,t1297]) ).

cnf(t221613,plain,
    rd(ld(etrue,rd(etrue,X2)),mult(X2,X2)) = ld(etrue,rd(etrue,mult(X2,mult(X2,X2)))),
    inference(step,[status(thm)],[t221612,t350]) ).

cnf(t26929,plain,
    ld(etrue,rd(etrue,mult(X1,mult(X1,X1)))) = rd(ld(etrue,rd(etrue,X1)),mult(X1,X1)),
    inference(orient,[status(thm)],[t221613]) ).

cnf(t26931,plain,
    rd(ld(etrue,rd(etrue,X1)),mult(X1,X1)) = ld(X2,rd(X2,mult(X1,mult(X1,X1)))),
    inference(cp,[status(thm)],[t26929,t391]) ).

cnf(t28126,plain,
    ld(X1,rd(X1,mult(X2,mult(X2,X2)))) = rd(ld(etrue,rd(etrue,X2)),mult(X2,X2)),
    inference(orient,[status(thm)],[t26931]) ).

cnf(t221654,plain,
    rd(ld(etrue,rd(etrue,X2)),mult(X2,X2)) = ld(X2,rd(X3,mult(X2,mult(X2,X3)))),
    inference(step,[status(thm)],[t32622,t28126]) ).

cnf(t32717,plain,
    ld(X1,rd(X2,mult(X1,mult(X1,X2)))) = rd(ld(etrue,rd(etrue,X1)),mult(X1,X1)),
    inference(orient,[status(thm)],[t221654]) ).

cnf(t221660,plain,
    rd(ld(X1,rd(X1,mult(X1,X1))),X1) = rd(ld(etrue,rd(etrue,X1)),mult(X1,X1)),
    inference(step,[status(thm)],[t221659,t32717]) ).

cnf(t33708,plain,
    rd(ld(X1,rd(X1,mult(X1,X1))),X1) = rd(ld(etrue,rd(etrue,X1)),mult(X1,X1)),
    inference(orient,[status(thm)],[t221660]) ).

cnf(t33802,plain,
    rd(etrue,mult(X1,mult(X1,etrue))) = ld(X1,ld(ld(X1,rd(X1,mult(X1,X1))),rd(ld(etrue,rd(etrue,X1)),mult(X1,X1)))),
    inference(cp,[status(thm)],[t33343,t33708]) ).

cnf(t221661,plain,
    rd(etrue,mult(X1,mult(X1,etrue))) = ld(X1,rd(mult(mult(X1,X1),ld(etrue,rd(etrue,X1))),mult(X1,X1))),
    inference(step,[status(thm)],[t33802,t5023]) ).

cnf(t221662,plain,
    rd(etrue,mult(X1,mult(X1,etrue))) = ld(X1,rd(rd(mult(X1,X1),ld(rd(etrue,X1),etrue)),mult(X1,X1))),
    inference(step,[status(thm)],[t221661,t196]) ).

cnf(t221663,plain,
    rd(etrue,mult(X1,mult(X1,etrue))) = ld(X1,rd(rd(mult(X1,X1),X1),mult(X1,X1))),
    inference(step,[status(thm)],[t221662,t24]) ).

cnf(t221664,plain,
    rd(etrue,mult(X1,mult(X1,etrue))) = ld(X1,rd(X1,mult(X1,X1))),
    inference(step,[status(thm)],[t221663,t9]) ).

cnf(t33840,plain,
    ld(X1,rd(X1,mult(X1,X1))) = rd(etrue,mult(X1,mult(X1,etrue))),
    inference(orient,[status(thm)],[t221664]) ).

cnf(t33845,plain,
    rd(etrue,mult(X1,mult(X1,etrue))) = ld(X2,rd(X2,mult(X1,X1))),
    inference(cp,[status(thm)],[t33840,t391]) ).

cnf(t33926,plain,
    ld(X1,rd(X1,mult(X2,X2))) = rd(etrue,mult(X2,mult(X2,etrue))),
    inference(orient,[status(thm)],[t33845]) ).

cnf(t222151,plain,
    rd(rd(etrue,mult(X2,mult(X2,etrue))),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)],[t222150,t33926]) ).

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

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

cnf(t222152,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)],[t222151,t70862]) ).

cnf(t222153,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)],[t222152,t506]) ).

cnf(t222154,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)],[t222153,t458]) ).

cnf(t222155,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)],[t222154,t458]) ).

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

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

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

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

cnf(t103959,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,t103728]) ).

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

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

cnf(t222157,plain,
    ld(mult(X1,X2),mult(X2,mult(X2,X2))) = ld(ld(X2,mult(ld(X2,X1),X2)),X2),
    inference(step,[status(thm)],[t103959,t38476]) ).

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

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

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

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

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

cnf(t222501,plain,
    rd(X1,ld(mult(X1,X2),mult(X1,mult(X1,X1)))) = rd(ld(X1,mult(X2,X1)),X1),
    inference(step,[status(thm)],[t128695,t130655]) ).

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

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

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

cnf(t154977,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)],[t39066,t154766]) ).

cnf(t67,plain,
    mult(X1,X2) = rd(rd(mult(X1,mult(X2,X3)),X2),rd(X3,X2)),
    inference(cp,[status(thm)],[t9,t56]) ).

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

cnf(t55207,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)],[t2776,t54979]) ).

cnf(t222026,plain,
    mult(ld(X1,rd(X2,X1)),X1) = rd(ld(X1,mult(X2,mult(X1,X1))),mult(X1,X1)),
    inference(step,[status(thm)],[t55207,t2335]) ).

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

cnf(t222520,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)],[t154977,t90601]) ).

cnf(t222521,plain,
    mult(ld(X1,rd(mult(X1,X2),X1)),X1) = ld(rd(etrue,mult(X1,mult(X1,etrue))),ld(X1,rd(ld(X1,mult(X2,X1)),X1))),
    inference(step,[status(thm)],[t222520,t33926]) ).

cnf(t222522,plain,
    mult(ld(X1,rd(mult(X1,X2),X1)),X1) = mult(X1,rd(ld(X1,mult(X2,X1)),X1)),
    inference(step,[status(thm)],[t222521,t29428]) ).

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,t23]) ).

cnf(t221440,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(t221441,plain,
    rd(mult(X1,X2),ld(X1,X3)) = mult(X3,mult(ld(X3,X1),rd(X2,ld(X1,X3)))),
    inference(step,[status(thm)],[t221440,t196]) ).

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

cnf(t10517,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)],[t10467,t1336]) ).

cnf(t221442,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)],[t10517,t24]) ).

cnf(t221443,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)],[t221442,t3971]) ).

cnf(t221444,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)],[t221443,t8447]) ).

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

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

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

cnf(t222523,plain,
    mult(ld(X1,rd(mult(X1,X2),X1)),X1) = rd(mult(rd(X1,X1),mult(X2,X1)),X1),
    inference(step,[status(thm)],[t222522,t10640]) ).

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

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

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

cnf(t219952,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)],[t219919,t187157]) ).

cnf(t223113,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)],[t219952,t219919]) ).

cnf(t223114,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)],[t223113,t219611]) ).

cnf(t222940,plain,
    mult(X1,rd(X2,X2)) = X1,
    inference(step,[status(thm)],[t619,t219919]) ).

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

cnf(t223115,plain,
    mult(rd(X1,X1),X2) = ld(rd(X1,X1),rd(mult(rd(X1,X1),X2),rd(X1,X1))),
    inference(step,[status(thm)],[t223114,t219920]) ).

cnf(t223116,plain,
    mult(rd(X1,X1),X2) = rd(mult(rd(X1,X1),mult(rd(X1,X1),X2)),rd(X1,X1)),
    inference(step,[status(thm)],[t223115,t14660]) ).

cnf(t223117,plain,
    mult(rd(X1,X1),X2) = mult(rd(X1,X1),mult(rd(X1,X1),X2)),
    inference(step,[status(thm)],[t223116,t219919]) ).

cnf(t223118,plain,
    mult(rd(X1,X1),X2) = ld(rd(X1,X1),X2),
    inference(step,[status(thm)],[t223117,t4363]) ).

cnf(t106702,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)],[t506,t106530]) ).

cnf(t222340,plain,
    ld(X1,rd(mult(X1,mult(X2,X1)),X1)) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
    inference(step,[status(thm)],[t9977,t129505]) ).

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

cnf(t222378,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)],[t106702,t129506]) ).

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

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

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

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

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

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

cnf(t134673,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)],[t134661,t44]) ).

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

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

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

cnf(t134963,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)],[t134949,t36685]) ).

cnf(t222383,plain,
    rd(mult(X1,mult(mult(X1,mult(rd(etrue,mult(X1,mult(X1,etrue))),X3)),X1)),X1) = ld(X1,rd(mult(X1,mult(X3,mult(X1,X1))),mult(X1,X1))),
    inference(step,[status(thm)],[t134963,t33926]) ).

cnf(t222384,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)],[t222383,t21708]) ).

cnf(t222385,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)],[t222384,t196]) ).

cnf(t222386,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)],[t222385,t23]) ).

cnf(t54709,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)],[t2776,t54494]) ).

cnf(t222023,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)],[t54709,t34]) ).

cnf(t222024,plain,
    mult(rd(X1,X1),mult(X1,X2)) = rd(mult(X1,mult(X2,mult(X1,X1))),mult(X1,X1)),
    inference(step,[status(thm)],[t222023,t2335]) ).

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

cnf(t222387,plain,
    rd(mult(X1,mult(ld(X1,X3),X1)),X1) = ld(X1,mult(rd(X1,X1),mult(X1,X3))),
    inference(step,[status(thm)],[t222386,t89954]) ).

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

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

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

cnf(t165606,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)],[t119072,t165248]) ).

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

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

cnf(t222783,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)],[t165606,t8245]) ).

cnf(t222784,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)],[t222783,t23]) ).

cnf(t222785,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)],[t222784,t458]) ).

cnf(t4137,plain,
    mult(X1,mult(X1,X2)) = ld(rd(rd(X1,mult(X1,X1)),X1),X2),
    inference(cp,[status(thm)],[t4118,t1336]) ).

cnf(t221384,plain,
    mult(X1,mult(X1,X2)) = ld(rd(rd(X1,X1),mult(X1,X1)),X2),
    inference(step,[status(thm)],[t4137,t2384]) ).

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

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

cnf(t4420,plain,
    mult(X1,mult(X1,X2)) = ld(ld(etrue,rd(etrue,mult(X1,X1))),X2),
    inference(cp,[status(thm)],[t4407,t3057]) ).

cnf(t4752,plain,
    ld(ld(etrue,rd(etrue,mult(X1,X1))),X2) = mult(X1,mult(X1,X2)),
    inference(orient,[status(thm)],[t4420]) ).

cnf(t4763,plain,
    mult(X1,mult(X1,X2)) = ld(ld(X3,rd(X3,mult(X1,X1))),X2),
    inference(cp,[status(thm)],[t4752,t391]) ).

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

cnf(t5017,plain,
    mult(mult(X1,X1),mult(X2,mult(X1,X1))) = mult(mult(X1,mult(X1,X2)),mult(X1,X1)),
    inference(cp,[status(thm)],[t3823,t4950]) ).

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

cnf(t89987,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)],[t89954,t14272]) ).

cnf(t222147,plain,
    mult(rd(X1,X1),mult(X1,mult(X1,mult(X1,X2)))) = mult(mult(X1,mult(X1,X1)),X2),
    inference(step,[status(thm)],[t89987,t44]) ).

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

cnf(t101781,plain,
    mult(X1,rd(mult(X1,mult(X1,X2)),X1)) = rd(mult(mult(X1,mult(X1,X1)),X2),X1),
    inference(cp,[status(thm)],[t400,t101564]) ).

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

cnf(t102314,plain,
    rd(mult(X1,mult(X1,X2)),X1) = ld(X1,rd(mult(mult(X1,mult(X1,X1)),X2),X1)),
    inference(cp,[status(thm)],[t11,t102155]) ).

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

cnf(t114943,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)],[t114930,t44]) ).

cnf(t222449,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)],[t114943,t1776]) ).

cnf(t222450,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)],[t222449,t1297]) ).

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

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

cnf(t21371,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)],[t21302,t4950]) ).

cnf(t221563,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)],[t21371,t216]) ).

cnf(t221564,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)],[t221563,t24]) ).

cnf(t221565,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)],[t221564,t1297]) ).

cnf(t221566,plain,
    mult(mult(X2,mult(X2,mult(X2,X2))),X3) = mult(X2,mult(X2,mult(X2,mult(X2,X3)))),
    inference(step,[status(thm)],[t221565,t4950]) ).

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

cnf(t222451,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)],[t222450,t23248]) ).

cnf(t222452,plain,
    rd(mult(X1,mult(X1,mult(X1,mult(X2,X1)))),X1) = mult(X1,mult(X1,mult(X1,X2))),
    inference(step,[status(thm)],[t222451,t11]) ).

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

cnf(t143772,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)],[t143764,t1178]) ).

cnf(t222642,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)],[t143772,t3971]) ).

cnf(t222643,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)],[t222642,t3971]) ).

cnf(t222644,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)],[t222643,t8]) ).

cnf(t222645,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)],[t222644,t458]) ).

cnf(t222646,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)],[t222645,t9]) ).

cnf(t222647,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)],[t222646,t3971]) ).

cnf(t222648,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)],[t222647,t1433]) ).

cnf(t222649,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)],[t222648,t458]) ).

cnf(t222650,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)],[t222649,t3971]) ).

cnf(t222651,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)],[t222650,t8]) ).

cnf(t222652,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)],[t222651,t3971]) ).

cnf(t222653,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)],[t222652,t8]) ).

cnf(t222654,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)],[t222653,t458]) ).

cnf(t222655,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)],[t222654,t3971]) ).

cnf(t222656,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)],[t222655,t1433]) ).

cnf(t222657,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)],[t222656,t8]) ).

cnf(t222658,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)],[t222657,t458]) ).

cnf(t222659,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)],[t222658,t1135]) ).

cnf(t222660,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)],[t222659,t1433]) ).

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

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

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

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

cnf(t222786,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)],[t222785,t175493]) ).

cnf(t222787,plain,
    rd(X1,ld(ld(X1,mult(X2,X1)),mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),X1),
    inference(step,[status(thm)],[t222786,t11]) ).

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

cnf(t107773,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)],[t107737,t1178]) ).

cnf(t222219,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)],[t107773,t1178]) ).

cnf(t222220,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)],[t222219,t2630]) ).

cnf(t222221,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)],[t222220,t992]) ).

cnf(t222222,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)],[t222221,t1178]) ).

cnf(t1459,plain,
    rd(ld(X1,ld(X2,rd(X1,X1))),X1) = ld(mult(X2,X1),rd(X1,mult(X1,X1))),
    inference(cp,[status(thm)],[t1433,t1091]) ).

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

cnf(t222223,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)],[t222222,t11188]) ).

cnf(t222224,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)],[t222223,t3295]) ).

cnf(t222225,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)],[t222224,t2936]) ).

cnf(t222226,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)],[t222225,t2936]) ).

cnf(t222227,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)],[t222226,t8]) ).

cnf(t222228,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)],[t222227,t44]) ).

cnf(t222229,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)],[t222228,t3971]) ).

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

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

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

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

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

cnf(t222301,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(X1,ld(mult(X2,X1),rd(X1,X1))),
    inference(step,[status(thm)],[t109393,t120548]) ).

cnf(t222302,plain,
    mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(X1,rd(ld(X1,ld(X2,X1)),X1)),
    inference(step,[status(thm)],[t222301,t1433]) ).

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

cnf(t195285,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)],[t195196,t120551]) ).

cnf(t222788,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)],[t195285,t225]) ).

cnf(t222789,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)],[t222788,t506]) ).

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

cnf(t221732,plain,
    mult(X2,mult(ld(X1,X3),X2)) = ld(Y3,rd(Y3,rd(ld(X2,ld(X3,X1)),X2))),
    inference(step,[status(thm)],[t1480,t83]) ).

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

cnf(t222790,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)],[t222789,t44128]) ).

cnf(t222791,plain,
    mult(mult(ld(X1,rd(X2,X1)),X1),X1) = mult(rd(X1,X1),mult(ld(X1,X2),X1)),
    inference(step,[status(thm)],[t222790,t119462]) ).

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

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

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

cnf(t219948,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)],[t219919,t212911]) ).

cnf(t223045,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)],[t219948,t992]) ).

cnf(t223046,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)],[t223045,t219920]) ).

cnf(t223047,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)],[t223046,t196]) ).

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

cnf(t223049,plain,
    X2 = ld(rd(X1,X1),rd(X2,rd(X1,X1))),
    inference(step,[status(thm)],[t223048,t219920]) ).

cnf(t223050,plain,
    X2 = ld(rd(X1,X1),X2),
    inference(step,[status(thm)],[t223049,t219919]) ).

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

cnf(t223119,plain,
    mult(rd(X1,X1),X2) = X2,
    inference(step,[status(thm)],[t223118,t220418]) ).

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

cnf(t221030,plain,
    efalse = eq(tuple(x1(rd(X1,X1)),mult(x1_2(rd(X1,X1)),rd(X1,X1))),tuple(x1(rd(X1,X1)),x1_2(rd(X1,X1)))),
    inference(cp,[status(thm)],[t22,t220869]) ).

cnf(t223221,plain,
    efalse = eq(tuple(x1(rd(X1,X1)),x1_2(rd(X1,X1))),tuple(x1(rd(X1,X1)),x1_2(rd(X1,X1)))),
    inference(step,[status(thm)],[t221030,t219920]) ).

cnf(t0,plain,
    eq(X1,X1) = etrue,
    introduced(definition) ).

cnf(t21,plain,
    eq(X1,X1) = etrue,
    inference(orient,[status(thm)],[t0]) ).

cnf(t223222,plain,
    efalse = etrue,
    inference(step,[status(thm)],[t223221,t21]) ).

cnf(t221220,plain,
    efalse = etrue,
    inference(orient,[status(thm)],[t223222]) ).

cnf(goal_0,negated_conjecture,
    etrue != efalse,
    introduced(definition) ).

cnf(g0_0,plain,
    etrue != etrue,
    inference(rw,[status(thm)],[goal_0,t221220]) ).

cnf(contradiction_0,plain,
    $false,
    inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP655-10 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04  % Command  : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.35  % Computer : n016.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.36  % WCLimit  : 300
% 0.10/0.36  % DateTime : Wed Sep 23 15:34:55 UTC 2026
% 0.10/0.36  % CPUTime  : 
% 0.10/0.36  Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 16.37/14.40  % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.37/14.40  % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------