%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP655+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.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:53 PM UTC 2026
% Result : Theorem 106.13s 13.89s
% Output : Proof 106.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 182
% Number of leaves : 7
% Syntax : Number of formulae : 1022 (1017 unt; 0 def)
% Number of atoms : 1027 (1026 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 20 ( 15 ~; 3 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-4 aty)
% Number of variables : 2260 ( 2 sgn 37 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [B,A] : ld(A,mult(A,B)) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f02) ).
fof(f1_nnf,plain,
! [B,A] : ld(A,mult(A,B)) = B,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] : ld(A,mult(A,B)) = B,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
ld(X1,mult(X1,X0)) = X0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t1,plain,
ld(X1,mult(X1,X2)) = X2,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t12,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t1]) ).
fof(f3,axiom,
! [B,A] : rd(mult(A,B),B) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f04) ).
fof(f3_nnf,plain,
! [B,A] : rd(mult(A,B),B) = A,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] : rd(mult(A,B),B) = A,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
rd(mult(X1,X0),X0) = X1,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t4,plain,
rd(mult(X1,X2),X2) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t9,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t4]) ).
fof(f4,axiom,
! [C,B,A] : mult(A,mult(B,mult(C,B))) = mult(mult(mult(A,B),C),B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f05) ).
fof(f4_nnf,plain,
! [C,B,A] : mult(A,mult(B,mult(C,B))) = mult(mult(mult(A,B),C),B),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C] : mult(A,mult(B,mult(C,B))) = mult(mult(mult(A,B),C),B),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
mult(X2,mult(X1,mult(X0,X1))) = mult(mult(mult(X2,X1),X0),X1),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t5,plain,
mult(mult(mult(X1,X2),X3),X2) = mult(X1,mult(X2,mult(X3,X2))),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t14,plain,
mult(mult(mult(X1,X2),X3),X2) = mult(X1,mult(X2,mult(X3,X2))),
inference(orient,[status(thm)],[t5]) ).
fof(f2,axiom,
! [B,A] : mult(rd(A,B),B) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f03) ).
fof(f2_nnf,plain,
! [B,A] : mult(rd(A,B),B) = A,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B] : mult(rd(A,B),B) = A,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
mult(rd(X1,X0),X0) = X1,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t3,plain,
mult(rd(X1,X2),X2) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t8,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t17,plain,
mult(rd(X1,X2),mult(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(cp,[status(thm)],[t14,t8]) ).
cnf(t25,plain,
mult(rd(X1,X2),mult(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(orient,[status(thm)],[t17]) ).
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(t398,plain,
rd(mult(rd(X1,X2),mult(X2,X3)),X2) = mult(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t39]) ).
cnf(t30,plain,
mult(X1,mult(X2,X1)) = ld(rd(X3,X1),mult(mult(X3,X2),X1)),
inference(cp,[status(thm)],[t12,t25]) ).
cnf(t71,plain,
ld(rd(X1,X2),mult(mult(X1,X3),X2)) = mult(X2,mult(X3,X2)),
inference(orient,[status(thm)],[t30]) ).
fof(f0,axiom,
! [B,A] : mult(A,ld(A,B)) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f01) ).
fof(f0_nnf,plain,
! [B,A] : mult(A,ld(A,B)) = B,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] : mult(A,ld(A,B)) = B,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
mult(X1,ld(X1,X0)) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t2,plain,
mult(X1,ld(X1,X2)) = X2,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t7,plain,
mult(X1,ld(X1,X2)) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t76,plain,
mult(X1,mult(ld(X2,X3),X1)) = ld(rd(X2,X1),mult(X3,X1)),
inference(cp,[status(thm)],[t71,t7]) ).
cnf(t83,plain,
ld(rd(X1,X2),mult(X3,X2)) = mult(X2,mult(ld(X1,X3),X2)),
inference(orient,[status(thm)],[t76]) ).
cnf(t13,plain,
X1 = ld(rd(X2,X1),X2),
inference(cp,[status(thm)],[t12,t8]) ).
cnf(t24,plain,
ld(rd(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t13]) ).
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)],[t12,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(t409,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)],[t398,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(t221180,plain,
mult(mult(X1,ld(mult(X2,X3),X2)),X3) = mult(rd(X1,X3),X3),
inference(step,[status(thm)],[t128,t7]) ).
cnf(t221181,plain,
mult(mult(X1,ld(mult(X2,X3),X2)),X3) = X1,
inference(step,[status(thm)],[t221180,t8]) ).
cnf(t154,plain,
mult(mult(X1,ld(mult(X2,X3),X2)),X3) = X1,
inference(orient,[status(thm)],[t221181]) ).
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(t215,plain,
rd(X1,ld(X2,rd(X2,X3))) = mult(X1,X3),
inference(orient,[status(thm)],[t187]) ).
cnf(t221185,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)],[t409,t215]) ).
cnf(t221186,plain,
mult(X1,mult(X2,X2)) = mult(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
inference(step,[status(thm)],[t221185,t215]) ).
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(t221187,plain,
mult(X1,mult(X2,X2)) = mult(rd(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
inference(step,[status(thm)],[t221186,t196]) ).
cnf(t221188,plain,
mult(X1,mult(X2,X2)) = mult(rd(mult(X1,X2),ld(X2,X2)),X2),
inference(step,[status(thm)],[t221187,t215]) ).
cnf(t539,plain,
mult(rd(mult(X1,X2),ld(X2,X2)),X2) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t221188]) ).
cnf(t550,plain,
mult(rd(X1,X2),mult(X2,X2)) = mult(rd(X1,ld(X2,X2)),X2),
inference(cp,[status(thm)],[t539,t8]) ).
cnf(t567,plain,
mult(rd(X1,ld(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
inference(orient,[status(thm)],[t550]) ).
cnf(t580,plain,
rd(X1,ld(X2,X2)) = rd(mult(rd(X1,X2),mult(X2,X2)),X2),
inference(cp,[status(thm)],[t9,t567]) ).
cnf(t221189,plain,
rd(X1,ld(X2,X2)) = mult(X1,rd(X2,X2)),
inference(step,[status(thm)],[t580,t398]) ).
cnf(t590,plain,
mult(X1,rd(X2,X2)) = rd(X1,ld(X2,X2)),
inference(orient,[status(thm)],[t221189]) ).
cnf(t601,plain,
rd(X1,X1) = ld(X2,rd(X2,ld(X1,X1))),
inference(cp,[status(thm)],[t12,t590]) ).
cnf(t207,plain,
ld(X1,X2) = ld(X3,rd(X3,ld(X2,X1))),
inference(cp,[status(thm)],[t12,t196]) ).
cnf(t224,plain,
ld(X1,rd(X1,ld(X2,X3))) = ld(X3,X2),
inference(orient,[status(thm)],[t207]) ).
cnf(t221191,plain,
rd(X1,X1) = ld(X1,X1),
inference(step,[status(thm)],[t601,t224]) ).
cnf(t614,plain,
ld(X1,X1) = rd(X1,X1),
inference(orient,[status(thm)],[t221191]) ).
cnf(t596,plain,
rd(rd(X1,rd(X2,X2)),ld(X2,X2)) = X1,
inference(cp,[status(thm)],[t590,t8]) ).
cnf(t221206,plain,
rd(rd(X1,rd(X2,X2)),rd(X2,X2)) = X1,
inference(step,[status(thm)],[t596,t614]) ).
cnf(t684,plain,
rd(rd(X1,rd(X2,X2)),rd(X2,X2)) = X1,
inference(orient,[status(thm)],[t221206]) ).
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(t619,plain,
X1 = rd(X1,rd(X1,X1)),
inference(cp,[status(thm)],[t23,t614]) ).
cnf(t634,plain,
rd(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t619]) ).
cnf(t639,plain,
mult(X1,rd(X2,rd(X1,X1))) = rd(mult(X1,mult(rd(X1,X1),X2)),rd(X1,X1)),
inference(cp,[status(thm)],[t398,t634]) ).
cnf(t39912,plain,
rd(mult(X1,mult(rd(X1,X1),X2)),rd(X1,X1)) = mult(X1,rd(X2,rd(X1,X1))),
inference(orient,[status(thm)],[t639]) ).
cnf(t40025,plain,
mult(X1,mult(rd(X1,X1),X2)) = rd(mult(X1,rd(X2,rd(X1,X1))),rd(X1,X1)),
inference(cp,[status(thm)],[t684,t39912]) ).
cnf(t81264,plain,
rd(mult(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = mult(X1,mult(rd(X1,X1),X2)),
inference(orient,[status(thm)],[t40025]) ).
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(t104690,plain,
mult(mult(rd(X1,rd(X2,X3)),mult(rd(X2,X3),Y3)),X3) = mult(rd(mult(X1,rd(Y3,rd(X2,X3))),X3),mult(X3,X2)),
inference(orient,[status(thm)],[t42]) ).
cnf(t635,plain,
ld(X1,rd(X1,X2)) = rd(ld(X1,rd(X1,X2)),mult(ld(X1,rd(X1,X2)),X2)),
inference(cp,[status(thm)],[t634,t215]) ).
cnf(t221192,plain,
mult(ld(X1,rd(X1,X2)),X2) = rd(X2,X2),
inference(step,[status(thm)],[t131,t614]) ).
cnf(t615,plain,
mult(ld(X1,rd(X1,X2)),X2) = rd(X2,X2),
inference(orient,[status(thm)],[t221192]) ).
cnf(t221259,plain,
ld(X1,rd(X1,X2)) = rd(ld(X1,rd(X1,X2)),rd(X2,X2)),
inference(step,[status(thm)],[t635,t615]) ).
cnf(t1664,plain,
rd(ld(X1,rd(X1,X2)),rd(X2,X2)) = ld(X1,rd(X1,X2)),
inference(orient,[status(thm)],[t221259]) ).
cnf(t104780,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)],[t104690,t1664]) ).
cnf(t19,plain,
mult(mult(X1,X2),X3) = rd(mult(X1,mult(X2,mult(X3,X2))),X2),
inference(cp,[status(thm)],[t9,t14]) ).
cnf(t44,plain,
rd(mult(X1,mult(X2,mult(X3,X2))),X2) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t19]) ).
cnf(t51,plain,
mult(mult(X1,X2),rd(X3,X2)) = rd(mult(X1,mult(X2,X3)),X2),
inference(cp,[status(thm)],[t44,t8]) ).
cnf(t56,plain,
mult(mult(X1,X2),rd(X3,X2)) = rd(mult(X1,mult(X2,X3)),X2),
inference(orient,[status(thm)],[t51]) ).
cnf(t637,plain,
rd(mult(X1,mult(rd(X2,X2),X2)),rd(X2,X2)) = mult(mult(X1,rd(X2,X2)),X2),
inference(cp,[status(thm)],[t56,t634]) ).
cnf(t221212,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(mult(X1,rd(X2,X2)),X2),
inference(step,[status(thm)],[t637,t8]) ).
cnf(t221213,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(rd(X1,X2),mult(X2,X2)),
inference(step,[status(thm)],[t221212,t34]) ).
cnf(t899,plain,
mult(rd(X1,X2),mult(X2,X2)) = rd(mult(X1,X2),rd(X2,X2)),
inference(orient,[status(thm)],[t221213]) ).
cnf(t222116,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)],[t104780,t899]) ).
cnf(t93,plain,
mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
inference(cp,[status(thm)],[t83,t8]) ).
cnf(t477,plain,
mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
inference(orient,[status(thm)],[t93]) ).
cnf(t492,plain,
mult(ld(X1,rd(X2,X3)),X3) = ld(X3,ld(rd(X1,X3),X2)),
inference(cp,[status(thm)],[t12,t477]) ).
cnf(t504,plain,
ld(X1,ld(rd(X2,X1),X3)) = mult(ld(X2,rd(X3,X1)),X1),
inference(orient,[status(thm)],[t492]) ).
cnf(t506,plain,
mult(ld(X1,rd(mult(rd(X1,X2),X3),X2)),X2) = ld(X2,X3),
inference(cp,[status(thm)],[t504,t12]) ).
cnf(t3671,plain,
mult(ld(X1,rd(mult(rd(X1,X2),X3),X2)),X2) = ld(X2,X3),
inference(orient,[status(thm)],[t506]) ).
cnf(t3728,plain,
ld(X1,rd(mult(rd(X1,X2),X3),X2)) = rd(ld(X2,X3),X2),
inference(cp,[status(thm)],[t9,t3671]) ).
cnf(t3755,plain,
ld(X1,rd(mult(rd(X1,X2),X3),X2)) = rd(ld(X2,X3),X2),
inference(orient,[status(thm)],[t3728]) ).
cnf(t3762,plain,
rd(ld(ld(X1,rd(X1,X2)),X3),ld(X1,rd(X1,X2))) = ld(Y3,mult(mult(rd(Y3,ld(X1,rd(X1,X2))),X3),X2)),
inference(cp,[status(thm)],[t3755,t215]) ).
cnf(t221327,plain,
mult(ld(ld(X1,rd(X1,X2)),X3),X2) = ld(Y3,mult(mult(rd(Y3,ld(X1,rd(X1,X2))),X3),X2)),
inference(step,[status(thm)],[t3762,t215]) ).
cnf(t221328,plain,
mult(ld(ld(X1,rd(X1,X2)),X3),X2) = ld(Y3,mult(mult(mult(Y3,X2),X3),X2)),
inference(step,[status(thm)],[t221327,t215]) ).
cnf(t221329,plain,
mult(ld(ld(X1,rd(X1,X2)),X3),X2) = ld(Y3,mult(Y3,mult(X2,mult(X3,X2)))),
inference(step,[status(thm)],[t221328,t14]) ).
cnf(t221330,plain,
mult(ld(ld(X1,rd(X1,X2)),X3),X2) = mult(X2,mult(X3,X2)),
inference(step,[status(thm)],[t221329,t12]) ).
cnf(t3817,plain,
mult(ld(ld(X1,rd(X1,X2)),X3),X2) = mult(X2,mult(X3,X2)),
inference(orient,[status(thm)],[t221330]) ).
cnf(t3846,plain,
mult(ld(X1,rd(X1,X2)),mult(X3,ld(X1,rd(X1,X2)))) = mult(ld(ld(Y3,mult(Y3,X2)),X3),ld(X1,rd(X1,X2))),
inference(cp,[status(thm)],[t3817,t215]) ).
cnf(t221334,plain,
mult(ld(X1,rd(X1,X2)),rd(X3,ld(rd(X1,X2),X1))) = mult(ld(ld(Y3,mult(Y3,X2)),X3),ld(X1,rd(X1,X2))),
inference(step,[status(thm)],[t3846,t196]) ).
cnf(t221335,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)],[t221334,t24]) ).
cnf(t221336,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)],[t221335,t196]) ).
cnf(t221337,plain,
mult(ld(X1,rd(X1,X2)),rd(X3,X2)) = rd(ld(X2,X3),ld(rd(X1,X2),X1)),
inference(step,[status(thm)],[t221336,t12]) ).
cnf(t221338,plain,
mult(ld(X1,rd(X1,X2)),rd(X3,X2)) = rd(ld(X2,X3),X2),
inference(step,[status(thm)],[t221337,t24]) ).
cnf(t4017,plain,
mult(ld(X1,rd(X1,X2)),rd(X3,X2)) = rd(ld(X2,X3),X2),
inference(orient,[status(thm)],[t221338]) ).
cnf(t4064,plain,
rd(ld(ld(X1,X2),X2),ld(X1,X2)) = mult(ld(X3,rd(X3,ld(X1,X2))),X1),
inference(cp,[status(thm)],[t4017,t23]) ).
cnf(t221340,plain,
rd(ld(ld(X1,X2),X2),ld(X1,X2)) = mult(ld(X2,X1),X1),
inference(step,[status(thm)],[t4064,t224]) ).
cnf(t4279,plain,
rd(ld(ld(X1,X2),X2),ld(X1,X2)) = mult(ld(X2,X1),X1),
inference(orient,[status(thm)],[t221340]) ).
cnf(t4323,plain,
ld(ld(X1,X2),X2) = mult(mult(ld(X2,X1),X1),ld(X1,X2)),
inference(cp,[status(thm)],[t8,t4279]) ).
cnf(t221345,plain,
ld(ld(X1,X2),X2) = rd(mult(ld(X2,X1),X1),ld(X2,X1)),
inference(step,[status(thm)],[t4323,t196]) ).
cnf(t4621,plain,
rd(mult(ld(X1,X2),X2),ld(X1,X2)) = ld(ld(X2,X1),X1),
inference(orient,[status(thm)],[t221345]) ).
cnf(t220,plain,
ld(X1,rd(X1,X2)) = ld(mult(X3,X2),X3),
inference(cp,[status(thm)],[t24,t215]) ).
cnf(t348,plain,
ld(X1,rd(X1,X2)) = ld(mult(X3,X2),X3),
inference(orient,[status(thm)],[t220]) ).
cnf(t4672,plain,
ld(ld(X1,mult(X1,X2)),mult(X1,X2)) = rd(mult(ld(mult(X1,X2),X1),X1),ld(X3,rd(X3,X2))),
inference(cp,[status(thm)],[t4621,t348]) ).
cnf(t221347,plain,
ld(X2,mult(X1,X2)) = rd(mult(ld(mult(X1,X2),X1),X1),ld(X3,rd(X3,X2))),
inference(step,[status(thm)],[t4672,t12]) ).
cnf(t221348,plain,
ld(X2,mult(X1,X2)) = mult(mult(ld(mult(X1,X2),X1),X1),X2),
inference(step,[status(thm)],[t221347,t215]) ).
cnf(t221349,plain,
ld(X2,mult(X1,X2)) = mult(mult(ld(true,rd(true,X2)),X1),X2),
inference(step,[status(thm)],[t221348,t348]) ).
cnf(t4884,plain,
mult(mult(ld(true,rd(true,X1)),X2),X1) = ld(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t221349]) ).
cnf(t228,plain,
ld(X1,rd(X1,X2)) = ld(X3,rd(X3,X2)),
inference(cp,[status(thm)],[t224,t24]) ).
cnf(t389,plain,
ld(X1,rd(X1,X2)) = ld(X3,rd(X3,X2)),
inference(orient,[status(thm)],[t228]) ).
cnf(t4901,plain,
ld(X1,mult(X2,X1)) = mult(mult(ld(X3,rd(X3,X1)),X2),X1),
inference(cp,[status(thm)],[t4884,t389]) ).
cnf(t5111,plain,
mult(mult(ld(X1,rd(X1,X2)),X3),X2) = ld(X2,mult(X3,X2)),
inference(orient,[status(thm)],[t4901]) ).
cnf(t222117,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)],[t222116,t5111]) ).
cnf(t221198,plain,
mult(rd(X1,rd(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
inference(step,[status(thm)],[t567,t614]) ).
cnf(t629,plain,
mult(rd(X1,rd(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
inference(rw,[status(thm)],[t221198]) ).
cnf(t782,plain,
mult(rd(X1,rd(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
inference(orient,[status(thm)],[t629]) ).
cnf(t221214,plain,
mult(rd(X1,rd(X2,X2)),X2) = rd(mult(X1,X2),rd(X2,X2)),
inference(step,[status(thm)],[t782,t899]) ).
cnf(t900,plain,
mult(rd(X1,rd(X2,X2)),X2) = rd(mult(X1,X2),rd(X2,X2)),
inference(orient,[status(thm)],[t221214]) ).
cnf(t222118,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)],[t222117,t900]) ).
cnf(t638,plain,
mult(ld(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),ld(X1,X2)),
inference(cp,[status(thm)],[t504,t634]) ).
cnf(t221194,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
inference(step,[status(thm)],[t590,t614]) ).
cnf(t617,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t221194]) ).
cnf(t221649,plain,
rd(ld(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),ld(X1,X2)),
inference(step,[status(thm)],[t638,t617]) ).
cnf(t39756,plain,
rd(ld(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),ld(X1,X2)),
inference(orient,[status(thm)],[t221649]) ).
cnf(t222119,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)],[t222118,t39756]) ).
cnf(t222120,plain,
ld(rd(X2,X2),ld(X2,mult(X3,X2))) = ld(X2,mult(mult(rd(X2,X2),X3),X2)),
inference(step,[status(thm)],[t222119,t5111]) ).
cnf(t105330,plain,
ld(rd(X1,X1),ld(X1,mult(X2,X1))) = ld(X1,mult(mult(rd(X1,X1),X2),X1)),
inference(orient,[status(thm)],[t222120]) ).
cnf(t124,plain,
ld(mult(X1,X2),X1) = rd(ld(X2,X2),X2),
inference(cp,[status(thm)],[t9,t114]) ).
cnf(t269,plain,
ld(mult(X1,X2),X1) = rd(ld(X2,X2),X2),
inference(orient,[status(thm)],[t124]) ).
cnf(t280,plain,
mult(X1,X2) = rd(X1,rd(ld(X2,X2),X2)),
inference(cp,[status(thm)],[t23,t269]) ).
cnf(t308,plain,
rd(X1,rd(ld(X2,X2),X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t280]) ).
cnf(t221201,plain,
rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
inference(step,[status(thm)],[t308,t614]) ).
cnf(t631,plain,
rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
inference(rw,[status(thm)],[t221201]) ).
cnf(t652,plain,
rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t631]) ).
cnf(t137,plain,
ld(X1,rd(X1,X2)) = rd(ld(X2,X2),X2),
inference(cp,[status(thm)],[t9,t131]) ).
cnf(t320,plain,
ld(X1,rd(X1,X2)) = rd(ld(X2,X2),X2),
inference(orient,[status(thm)],[t137]) ).
cnf(t221196,plain,
ld(X1,rd(X1,X2)) = rd(rd(X2,X2),X2),
inference(step,[status(thm)],[t320,t614]) ).
cnf(t627,plain,
ld(X1,rd(X1,X2)) = rd(rd(X2,X2),X2),
inference(rw,[status(thm)],[t221196]) ).
cnf(t996,plain,
ld(X1,rd(X1,X2)) = rd(rd(X2,X2),X2),
inference(orient,[status(thm)],[t627]) ).
cnf(t1013,plain,
rd(mult(rd(X1,X1),X1),rd(X1,X1)) = mult(ld(X2,rd(X2,X1)),mult(X1,X1)),
inference(cp,[status(thm)],[t899,t996]) ).
cnf(t221224,plain,
rd(X1,rd(X1,X1)) = mult(ld(X2,rd(X2,X1)),mult(X1,X1)),
inference(step,[status(thm)],[t1013,t8]) ).
cnf(t221225,plain,
X1 = mult(ld(X2,rd(X2,X1)),mult(X1,X1)),
inference(step,[status(thm)],[t221224,t634]) ).
cnf(t1025,plain,
mult(ld(X1,rd(X1,X2)),mult(X2,X2)) = X2,
inference(orient,[status(thm)],[t221225]) ).
cnf(t1042,plain,
mult(X1,X1) = ld(ld(X2,rd(X2,X1)),X1),
inference(cp,[status(thm)],[t12,t1025]) ).
cnf(t1053,plain,
ld(ld(X1,rd(X1,X2)),X2) = mult(X2,X2),
inference(orient,[status(thm)],[t1042]) ).
cnf(t1055,plain,
mult(X1,X1) = ld(rd(rd(X1,X1),X1),X1),
inference(cp,[status(thm)],[t1053,t996]) ).
cnf(t1075,plain,
ld(rd(rd(X1,X1),X1),X1) = mult(X1,X1),
inference(orient,[status(thm)],[t1055]) ).
cnf(t1082,plain,
rd(rd(X1,X1),X1) = rd(X1,mult(X1,X1)),
inference(cp,[status(thm)],[t23,t1075]) ).
cnf(t1088,plain,
rd(rd(X1,X1),X1) = rd(X1,mult(X1,X1)),
inference(orient,[status(thm)],[t1082]) ).
cnf(t221228,plain,
rd(X1,rd(X2,mult(X2,X2))) = mult(X1,X2),
inference(step,[status(thm)],[t652,t1088]) ).
cnf(t1112,plain,
rd(X1,rd(X2,mult(X2,X2))) = mult(X1,X2),
inference(rw,[status(thm)],[t221228]) ).
cnf(t1174,plain,
rd(X1,rd(X2,mult(X2,X2))) = mult(X1,X2),
inference(orient,[status(thm)],[t1112]) ).
cnf(t105338,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)],[t105330,t1174]) ).
cnf(t87,plain,
mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
inference(cp,[status(thm)],[t83,t9]) ).
cnf(t429,plain,
mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
inference(orient,[status(thm)],[t87]) ).
cnf(t445,plain,
mult(ld(mult(X1,X2),X3),X2) = ld(X2,ld(X1,mult(X3,X2))),
inference(cp,[status(thm)],[t12,t429]) ).
cnf(t456,plain,
ld(X1,ld(X2,mult(X3,X1))) = mult(ld(mult(X2,X1),X3),X1),
inference(orient,[status(thm)],[t445]) ).
cnf(t458,plain,
mult(ld(mult(rd(mult(X1,X2),X3),X2),X1),X2) = ld(X2,X3),
inference(cp,[status(thm)],[t456,t24]) ).
cnf(t2852,plain,
mult(ld(mult(rd(mult(X1,X2),X3),X2),X1),X2) = ld(X2,X3),
inference(orient,[status(thm)],[t458]) ).
cnf(t279,plain,
rd(X1,ld(X2,mult(X2,X3))) = mult(X1,rd(ld(X3,X3),X3)),
inference(cp,[status(thm)],[t196,t269]) ).
cnf(t221183,plain,
rd(X1,X3) = mult(X1,rd(ld(X3,X3),X3)),
inference(step,[status(thm)],[t279,t12]) ).
cnf(t291,plain,
mult(X1,rd(ld(X2,X2),X2)) = rd(X1,X2),
inference(orient,[status(thm)],[t221183]) ).
cnf(t221202,plain,
mult(X1,rd(rd(X2,X2),X2)) = rd(X1,X2),
inference(step,[status(thm)],[t291,t614]) ).
cnf(t632,plain,
mult(X1,rd(rd(X2,X2),X2)) = rd(X1,X2),
inference(rw,[status(thm)],[t221202]) ).
cnf(t669,plain,
mult(X1,rd(rd(X2,X2),X2)) = rd(X1,X2),
inference(orient,[status(thm)],[t632]) ).
cnf(t221227,plain,
mult(X1,rd(X2,mult(X2,X2))) = rd(X1,X2),
inference(step,[status(thm)],[t669,t1088]) ).
cnf(t1111,plain,
mult(X1,rd(X2,mult(X2,X2))) = rd(X1,X2),
inference(rw,[status(thm)],[t221227]) ).
cnf(t1132,plain,
mult(X1,rd(X2,mult(X2,X2))) = rd(X1,X2),
inference(orient,[status(thm)],[t1111]) ).
cnf(t2856,plain,
ld(rd(X1,mult(X1,X1)),X2) = rd(ld(mult(rd(mult(X3,rd(X1,mult(X1,X1))),X2),rd(X1,mult(X1,X1))),X3),X1),
inference(cp,[status(thm)],[t2852,t1132]) ).
cnf(t221293,plain,
ld(rd(X1,mult(X1,X1)),X2) = rd(ld(rd(rd(mult(X3,rd(X1,mult(X1,X1))),X2),X1),X3),X1),
inference(step,[status(thm)],[t2856,t1132]) ).
cnf(t221294,plain,
ld(rd(X1,mult(X1,X1)),X2) = rd(ld(rd(rd(rd(X3,X1),X2),X1),X3),X1),
inference(step,[status(thm)],[t221293,t1132]) ).
cnf(t481,plain,
ld(rd(rd(rd(X1,X2),X3),X2),X1) = mult(X2,mult(X3,X2)),
inference(cp,[status(thm)],[t477,t24]) ).
cnf(t1511,plain,
ld(rd(rd(rd(X1,X2),X3),X2),X1) = mult(X2,mult(X3,X2)),
inference(orient,[status(thm)],[t481]) ).
cnf(t1542,plain,
rd(rd(rd(X1,X2),X3),X2) = rd(X1,mult(X2,mult(X3,X2))),
inference(cp,[status(thm)],[t23,t1511]) ).
cnf(t1548,plain,
rd(rd(rd(X1,X2),X3),X2) = rd(X1,mult(X2,mult(X3,X2))),
inference(orient,[status(thm)],[t1542]) ).
cnf(t221295,plain,
ld(rd(X1,mult(X1,X1)),X2) = rd(ld(rd(X3,mult(X1,mult(X2,X1))),X3),X1),
inference(step,[status(thm)],[t221294,t1548]) ).
cnf(t221296,plain,
ld(rd(X1,mult(X1,X1)),X2) = rd(mult(X1,mult(X2,X1)),X1),
inference(step,[status(thm)],[t221295,t24]) ).
cnf(t2930,plain,
ld(rd(X1,mult(X1,X1)),X2) = rd(mult(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t221296]) ).
cnf(t222121,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)],[t105338,t2930]) ).
cnf(t222122,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)],[t222121,t1132]) ).
cnf(t222123,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)],[t222122,t8]) ).
cnf(t222124,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)],[t222123,t1174]) ).
cnf(t1582,plain,
rd(rd(X1,X2),X3) = mult(rd(X1,mult(X2,mult(X3,X2))),X2),
inference(cp,[status(thm)],[t8,t1548]) ).
cnf(t2564,plain,
mult(rd(X1,mult(X2,mult(X3,X2))),X2) = rd(rd(X1,X2),X3),
inference(orient,[status(thm)],[t1582]) ).
cnf(t2596,plain,
rd(rd(X1,X2),rd(X3,X2)) = mult(rd(X1,mult(X2,X3)),X2),
inference(cp,[status(thm)],[t2564,t8]) ).
cnf(t2624,plain,
mult(rd(X1,mult(X2,X3)),X2) = rd(rd(X1,X2),rd(X3,X2)),
inference(orient,[status(thm)],[t2596]) ).
cnf(t222125,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)],[t222124,t2624]) ).
cnf(t902,plain,
rd(mult(X1,rd(rd(X2,X2),X2)),rd(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))) = mult(mult(X1,X2),mult(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))),
inference(cp,[status(thm)],[t899,t652]) ).
cnf(t221217,plain,
rd(rd(X1,X2),rd(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))) = mult(mult(X1,X2),mult(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))),
inference(step,[status(thm)],[t902,t669]) ).
cnf(t221218,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)],[t221217,t652]) ).
cnf(t221219,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)],[t221218,t8]) ).
cnf(t221220,plain,
rd(rd(X1,X2),rd(X2,X2)) = mult(mult(X1,X2),rd(rd(rd(X2,X2),X2),X2)),
inference(step,[status(thm)],[t221219,t669]) ).
cnf(t221221,plain,
rd(rd(X1,X2),rd(X2,X2)) = rd(mult(X1,mult(X2,rd(rd(X2,X2),X2))),X2),
inference(step,[status(thm)],[t221220,t56]) ).
cnf(t221222,plain,
rd(rd(X1,X2),rd(X2,X2)) = rd(mult(X1,rd(X2,X2)),X2),
inference(step,[status(thm)],[t221221,t669]) ).
cnf(t221223,plain,
rd(rd(X1,X2),rd(X2,X2)) = rd(rd(X1,rd(X2,X2)),X2),
inference(step,[status(thm)],[t221222,t617]) ).
cnf(t964,plain,
rd(rd(X1,rd(X2,X2)),X2) = rd(rd(X1,X2),rd(X2,X2)),
inference(orient,[status(thm)],[t221223]) ).
cnf(t965,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(cp,[status(thm)],[t964,t634]) ).
cnf(t989,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t965]) ).
cnf(t222126,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)],[t222125,t989]) ).
cnf(t222127,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)],[t222126,t2624]) ).
cnf(t222128,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)],[t222127,t989]) ).
cnf(t222129,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)],[t222128,t2930]) ).
cnf(t222130,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)],[t222129,t1132]) ).
cnf(t222131,plain,
rd(mult(X1,mult(rd(X1,X1),X2)),X1) = ld(rd(X1,X1),rd(mult(X1,X2),X1)),
inference(step,[status(thm)],[t222130,t8]) ).
cnf(t105626,plain,
ld(rd(X1,X1),rd(mult(X1,X2),X1)) = rd(mult(X1,mult(rd(X1,X1),X2)),X1),
inference(orient,[status(thm)],[t222131]) ).
cnf(t105650,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)],[t105626,t44]) ).
cnf(t222137,plain,
rd(mult(X1,mult(mult(X1,X2),X1)),X1) = ld(rd(X1,X1),mult(mult(X1,X1),X2)),
inference(step,[status(thm)],[t105650,t25]) ).
cnf(t106491,plain,
ld(rd(X1,X1),mult(mult(X1,X1),X2)) = rd(mult(X1,mult(mult(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t222137]) ).
cnf(t106589,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)],[t106491,t1132]) ).
cnf(t222149,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)],[t106589,t1174]) ).
cnf(t3822,plain,
mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))) = rd(ld(ld(X3,rd(X3,rd(X1,mult(X1,X1)))),X2),X1),
inference(cp,[status(thm)],[t3817,t1132]) ).
cnf(t221331,plain,
mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(ld(X3,rd(X3,rd(X1,mult(X1,X1)))),X2),X1),
inference(step,[status(thm)],[t3822,t1132]) ).
cnf(t221332,plain,
mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(ld(X3,mult(X3,X1)),X2),X1),
inference(step,[status(thm)],[t221331,t1174]) ).
cnf(t221333,plain,
mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(X1,X2),X1),
inference(step,[status(thm)],[t221332,t12]) ).
cnf(t3906,plain,
mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(X1,X2),X1),
inference(orient,[status(thm)],[t221333]) ).
cnf(t3936,plain,
rd(ld(X1,mult(X2,X1)),X1) = mult(rd(X1,mult(X1,X1)),X2),
inference(cp,[status(thm)],[t3906,t9]) ).
cnf(t3965,plain,
mult(rd(X1,mult(X1,X1)),X2) = rd(ld(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t3936]) ).
cnf(t222150,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)],[t222149,t3965]) ).
cnf(t222151,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)],[t222150,t8]) ).
cnf(t222152,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)],[t222151,t1132]) ).
cnf(t222153,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)],[t222152,t8]) ).
cnf(t222154,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)],[t222153,t3965]) ).
cnf(t222155,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)],[t222154,t1174]) ).
cnf(t222156,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)],[t222155,t2624]) ).
cnf(t222157,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)],[t222156,t989]) ).
cnf(t1550,plain,
rd(X1,mult(X2,mult(rd(X2,X2),X2))) = rd(rd(rd(X1,X2),X2),rd(X2,X2)),
inference(cp,[status(thm)],[t1548,t964]) ).
cnf(t221289,plain,
rd(X1,mult(X2,X2)) = rd(rd(rd(X1,X2),X2),rd(X2,X2)),
inference(step,[status(thm)],[t1550,t8]) ).
cnf(t2329,plain,
rd(rd(rd(X1,X2),X2),rd(X2,X2)) = rd(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t221289]) ).
cnf(t2356,plain,
rd(rd(X1,X2),mult(X2,mult(rd(X2,X2),X2))) = rd(rd(X1,mult(X2,X2)),X2),
inference(cp,[status(thm)],[t1548,t2329]) ).
cnf(t221290,plain,
rd(rd(X1,X2),mult(X2,X2)) = rd(rd(X1,mult(X2,X2)),X2),
inference(step,[status(thm)],[t2356,t8]) ).
cnf(t2378,plain,
rd(rd(X1,mult(X2,X2)),X2) = rd(rd(X1,X2),mult(X2,X2)),
inference(orient,[status(thm)],[t221290]) ).
cnf(t222158,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)],[t222157,t2378]) ).
cnf(t1553,plain,
rd(X1,mult(X1,mult(X1,X1))) = rd(rd(X1,mult(X1,X1)),X1),
inference(cp,[status(thm)],[t1548,t1088]) ).
cnf(t136,plain,
X1 = ld(ld(X2,rd(X2,X1)),ld(X1,X1)),
inference(cp,[status(thm)],[t12,t131]) ).
cnf(t232,plain,
ld(ld(X1,rd(X1,X2)),ld(X2,X2)) = X2,
inference(orient,[status(thm)],[t136]) ).
cnf(t221203,plain,
ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
inference(step,[status(thm)],[t232,t614]) ).
cnf(t633,plain,
ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
inference(rw,[status(thm)],[t221203]) ).
cnf(t694,plain,
ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
inference(orient,[status(thm)],[t633]) ).
cnf(t697,plain,
rd(rd(X1,X1),X1) = ld(ld(X2,mult(X2,X1)),rd(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1))),
inference(cp,[status(thm)],[t694,t652]) ).
cnf(t221207,plain,
rd(rd(X1,X1),X1) = ld(X1,rd(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1))),
inference(step,[status(thm)],[t697,t12]) ).
cnf(t221208,plain,
rd(rd(X1,X1),X1) = ld(X1,mult(rd(rd(X1,X1),X1),X1)),
inference(step,[status(thm)],[t221207,t652]) ).
cnf(t221209,plain,
rd(rd(X1,X1),X1) = ld(X1,rd(X1,X1)),
inference(step,[status(thm)],[t221208,t8]) ).
cnf(t751,plain,
ld(X1,rd(X1,X1)) = rd(rd(X1,X1),X1),
inference(orient,[status(thm)],[t221209]) ).
cnf(t785,plain,
mult(rd(X1,X1),mult(X1,X1)) = mult(X1,X1),
inference(cp,[status(thm)],[t782,t634]) ).
cnf(t807,plain,
mult(rd(X1,X1),mult(X1,X1)) = mult(X1,X1),
inference(orient,[status(thm)],[t785]) ).
cnf(t815,plain,
rd(X1,X1) = rd(mult(X1,X1),mult(X1,X1)),
inference(cp,[status(thm)],[t9,t807]) ).
cnf(t825,plain,
rd(mult(X1,X1),mult(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t815]) ).
cnf(t834,plain,
rd(rd(mult(X1,X1),mult(X1,X1)),mult(X1,X1)) = ld(mult(X1,X1),rd(X1,X1)),
inference(cp,[status(thm)],[t751,t825]) ).
cnf(t221216,plain,
rd(rd(X1,X1),mult(X1,X1)) = ld(mult(X1,X1),rd(X1,X1)),
inference(step,[status(thm)],[t834,t825]) ).
cnf(t928,plain,
ld(mult(X1,X1),rd(X1,X1)) = rd(rd(X1,X1),mult(X1,X1)),
inference(orient,[status(thm)],[t221216]) ).
cnf(t467,plain,
mult(ld(mult(X1,X2),rd(X3,X2)),X2) = ld(X2,ld(X1,X3)),
inference(cp,[status(thm)],[t456,t8]) ).
cnf(t1370,plain,
mult(ld(mult(X1,X2),rd(X3,X2)),X2) = ld(X2,ld(X1,X3)),
inference(orient,[status(thm)],[t467]) ).
cnf(t1414,plain,
ld(mult(X1,X2),rd(X3,X2)) = rd(ld(X2,ld(X1,X3)),X2),
inference(cp,[status(thm)],[t9,t1370]) ).
cnf(t1429,plain,
ld(mult(X1,X2),rd(X3,X2)) = rd(ld(X2,ld(X1,X3)),X2),
inference(orient,[status(thm)],[t1414]) ).
cnf(t221248,plain,
rd(ld(X1,ld(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
inference(step,[status(thm)],[t928,t1429]) ).
cnf(t221249,plain,
rd(ld(X1,rd(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
inference(step,[status(thm)],[t221248,t614]) ).
cnf(t1479,plain,
rd(ld(X1,rd(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
inference(rw,[status(thm)],[t221249]) ).
cnf(t699,plain,
ld(X1,rd(X1,X2)) = ld(ld(X3,mult(X3,X2)),rd(ld(X1,rd(X1,X2)),ld(X1,rd(X1,X2)))),
inference(cp,[status(thm)],[t694,t215]) ).
cnf(t221244,plain,
ld(X1,rd(X1,X2)) = ld(X2,rd(ld(X1,rd(X1,X2)),ld(X1,rd(X1,X2)))),
inference(step,[status(thm)],[t699,t12]) ).
cnf(t221245,plain,
ld(X1,rd(X1,X2)) = ld(X2,mult(ld(X1,rd(X1,X2)),X2)),
inference(step,[status(thm)],[t221244,t215]) ).
cnf(t221246,plain,
ld(X1,rd(X1,X2)) = ld(X2,rd(X2,X2)),
inference(step,[status(thm)],[t221245,t615]) ).
cnf(t1189,plain,
rd(X1,mult(X1,X1)) = ld(ld(X2,mult(X2,X1)),rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1)))),
inference(cp,[status(thm)],[t694,t1174]) ).
cnf(t221229,plain,
rd(X1,mult(X1,X1)) = ld(X1,rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1)))),
inference(step,[status(thm)],[t1189,t12]) ).
cnf(t221230,plain,
rd(X1,mult(X1,X1)) = ld(X1,mult(rd(X1,mult(X1,X1)),X1)),
inference(step,[status(thm)],[t221229,t1174]) ).
cnf(t1095,plain,
rd(X1,X1) = mult(rd(X1,mult(X1,X1)),X1),
inference(cp,[status(thm)],[t8,t1088]) ).
cnf(t1113,plain,
mult(rd(X1,mult(X1,X1)),X1) = rd(X1,X1),
inference(orient,[status(thm)],[t1095]) ).
cnf(t221231,plain,
rd(X1,mult(X1,X1)) = ld(X1,rd(X1,X1)),
inference(step,[status(thm)],[t221230,t1113]) ).
cnf(t1196,plain,
ld(X1,rd(X1,X1)) = rd(X1,mult(X1,X1)),
inference(orient,[status(thm)],[t221231]) ).
cnf(t221247,plain,
ld(X1,rd(X1,X2)) = rd(X2,mult(X2,X2)),
inference(step,[status(thm)],[t221246,t1196]) ).
cnf(t1332,plain,
ld(X1,rd(X1,X2)) = rd(X2,mult(X2,X2)),
inference(orient,[status(thm)],[t221247]) ).
cnf(t221250,plain,
rd(rd(X1,mult(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
inference(step,[status(thm)],[t1479,t1332]) ).
cnf(t1480,plain,
rd(rd(X1,mult(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
inference(orient,[status(thm)],[t221250]) ).
cnf(t221253,plain,
rd(X1,mult(X1,mult(X1,X1))) = rd(rd(X1,X1),mult(X1,X1)),
inference(step,[status(thm)],[t1553,t1480]) ).
cnf(t1605,plain,
rd(rd(X1,X1),mult(X1,X1)) = rd(X1,mult(X1,mult(X1,X1))),
inference(orient,[status(thm)],[t221253]) ).
cnf(t222159,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)],[t222158,t1605]) ).
cnf(t3893,plain,
ld(rd(ld(X1,rd(X1,X2)),X2),X3) = mult(X2,mult(X2,mult(rd(X3,X2),X2))),
inference(cp,[status(thm)],[t477,t3817]) ).
cnf(t221339,plain,
ld(rd(ld(X1,rd(X1,X2)),X2),X3) = mult(X2,mult(X2,X3)),
inference(step,[status(thm)],[t3893,t8]) ).
cnf(t4111,plain,
ld(rd(ld(X1,rd(X1,X2)),X2),X3) = mult(X2,mult(X2,X3)),
inference(orient,[status(thm)],[t221339]) ).
cnf(t4116,plain,
mult(X1,mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3))) = X3,
inference(cp,[status(thm)],[t4111,t12]) ).
cnf(t19775,plain,
mult(X1,mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3))) = X3,
inference(orient,[status(thm)],[t4116]) ).
cnf(t19878,plain,
mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3)) = ld(X1,X3),
inference(cp,[status(thm)],[t12,t19775]) ).
cnf(t19951,plain,
mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3)) = ld(X1,X3),
inference(orient,[status(thm)],[t19878]) ).
cnf(t20054,plain,
mult(rd(ld(X1,rd(X1,X2)),X2),X3) = ld(X2,ld(X2,X3)),
inference(cp,[status(thm)],[t12,t19951]) ).
cnf(t20143,plain,
mult(rd(ld(X1,rd(X1,X2)),X2),X3) = ld(X2,ld(X2,X3)),
inference(orient,[status(thm)],[t20054]) ).
cnf(t20243,plain,
rd(ld(X1,ld(rd(ld(X2,rd(X2,X3)),X3),Y3)),X1) = ld(ld(X3,ld(X3,X1)),rd(Y3,X1)),
inference(cp,[status(thm)],[t1429,t20143]) ).
cnf(t221511,plain,
rd(ld(X1,mult(X3,mult(X3,Y3))),X1) = ld(ld(X3,ld(X3,X1)),rd(Y3,X1)),
inference(step,[status(thm)],[t20243,t4111]) ).
cnf(t21482,plain,
ld(ld(X1,ld(X1,X2)),rd(X3,X2)) = rd(ld(X2,mult(X1,mult(X1,X3))),X2),
inference(orient,[status(thm)],[t221511]) ).
cnf(t21630,plain,
ld(X1,ld(X1,X2)) = rd(rd(X3,X2),rd(ld(X2,mult(X1,mult(X1,X3))),X2)),
inference(cp,[status(thm)],[t23,t21482]) ).
cnf(t2905,plain,
ld(mult(rd(mult(X1,X2),X3),X2),X1) = rd(ld(X2,X3),X2),
inference(cp,[status(thm)],[t9,t2852]) ).
cnf(t3000,plain,
ld(mult(rd(mult(X1,X2),X3),X2),X1) = rd(ld(X2,X3),X2),
inference(orient,[status(thm)],[t2905]) ).
cnf(t3045,plain,
mult(rd(mult(X1,X2),X3),X2) = rd(X1,rd(ld(X2,X3),X2)),
inference(cp,[status(thm)],[t23,t3000]) ).
cnf(t3101,plain,
mult(rd(mult(X1,X2),X3),X2) = rd(X1,rd(ld(X2,X3),X2)),
inference(orient,[status(thm)],[t3045]) ).
cnf(t3137,plain,
rd(rd(X1,X2),rd(ld(X2,X3),X2)) = mult(rd(X1,X3),X2),
inference(cp,[status(thm)],[t3101,t8]) ).
cnf(t3289,plain,
rd(rd(X1,X2),rd(ld(X2,X3),X2)) = mult(rd(X1,X3),X2),
inference(orient,[status(thm)],[t3137]) ).
cnf(t221512,plain,
ld(X1,ld(X1,X2)) = mult(rd(X3,mult(X1,mult(X1,X3))),X2),
inference(step,[status(thm)],[t21630,t3289]) ).
cnf(t21683,plain,
mult(rd(X1,mult(X2,mult(X2,X1))),X3) = ld(X2,ld(X2,X3)),
inference(orient,[status(thm)],[t221512]) ).
cnf(t222160,plain,
ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(rd(X1,X1),ld(X1,ld(X1,X2))),
inference(step,[status(thm)],[t222159,t21683]) ).
cnf(t108253,plain,
ld(rd(X1,X1),ld(X1,ld(X1,X2))) = ld(X1,rd(ld(X1,mult(X2,X1)),X1)),
inference(orient,[status(thm)],[t222160]) ).
cnf(t1562,plain,
rd(X1,mult(ld(X2,X1),mult(X3,ld(X2,X1)))) = rd(rd(X2,X3),ld(X2,X1)),
inference(cp,[status(thm)],[t1548,t23]) ).
cnf(t221695,plain,
rd(X1,mult(ld(X2,X1),rd(X3,ld(X1,X2)))) = rd(rd(X2,X3),ld(X2,X1)),
inference(step,[status(thm)],[t1562,t196]) ).
cnf(t3820,plain,
mult(ld(X1,X2),mult(X3,ld(X1,X2))) = rd(ld(ld(Y3,rd(Y3,ld(X1,X2))),X3),ld(X2,X1)),
inference(cp,[status(thm)],[t3817,t196]) ).
cnf(t221425,plain,
mult(ld(X1,X2),rd(X3,ld(X2,X1))) = rd(ld(ld(Y3,rd(Y3,ld(X1,X2))),X3),ld(X2,X1)),
inference(step,[status(thm)],[t3820,t196]) ).
cnf(t221426,plain,
mult(ld(X1,X2),rd(X3,ld(X2,X1))) = rd(ld(ld(X2,X1),X3),ld(X2,X1)),
inference(step,[status(thm)],[t221425,t224]) ).
cnf(t13646,plain,
mult(ld(X1,X2),rd(X3,ld(X2,X1))) = rd(ld(ld(X2,X1),X3),ld(X2,X1)),
inference(orient,[status(thm)],[t221426]) ).
cnf(t221696,plain,
rd(X1,rd(ld(ld(X1,X2),X3),ld(X1,X2))) = rd(rd(X2,X3),ld(X2,X1)),
inference(step,[status(thm)],[t221695,t13646]) ).
cnf(t45472,plain,
rd(X1,rd(ld(ld(X1,X2),X3),ld(X1,X2))) = rd(rd(X2,X3),ld(X2,X1)),
inference(orient,[status(thm)],[t221696]) ).
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(t221628,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(t221629,plain,
rd(ld(ld(X2,X1),ld(X2,X3)),ld(X2,X1)) = ld(X1,mult(X3,ld(X1,X2))),
inference(step,[status(thm)],[t221628,t13646]) ).
cnf(t221630,plain,
rd(ld(ld(X2,X1),ld(X2,X3)),ld(X2,X1)) = ld(X1,rd(X3,ld(X2,X1))),
inference(step,[status(thm)],[t221629,t196]) ).
cnf(t35100,plain,
rd(ld(ld(X1,X2),ld(X1,X3)),ld(X1,X2)) = ld(X2,rd(X3,ld(X1,X2))),
inference(orient,[status(thm)],[t221630]) ).
cnf(t45474,plain,
rd(rd(X1,ld(X2,X3)),ld(X1,X2)) = rd(X2,ld(X1,rd(X3,ld(X2,X1)))),
inference(cp,[status(thm)],[t45472,t35100]) ).
cnf(t45802,plain,
rd(rd(X1,ld(X2,X3)),ld(X1,X2)) = rd(X2,ld(X1,rd(X3,ld(X2,X1)))),
inference(orient,[status(thm)],[t45474]) ).
cnf(t595,plain,
rd(mult(X1,X2),ld(X2,X2)) = rd(mult(X1,mult(X2,X2)),X2),
inference(cp,[status(thm)],[t590,t56]) ).
cnf(t221210,plain,
rd(mult(X1,X2),rd(X2,X2)) = rd(mult(X1,mult(X2,X2)),X2),
inference(step,[status(thm)],[t595,t614]) ).
cnf(t757,plain,
rd(mult(X1,mult(X2,X2)),X2) = rd(mult(X1,X2),rd(X2,X2)),
inference(orient,[status(thm)],[t221210]) ).
cnf(t767,plain,
mult(X1,mult(X2,X2)) = mult(rd(mult(X1,X2),rd(X2,X2)),X2),
inference(cp,[status(thm)],[t8,t757]) ).
cnf(t221260,plain,
mult(X1,mult(X2,X2)) = rd(mult(mult(X1,X2),X2),rd(X2,X2)),
inference(step,[status(thm)],[t767,t900]) ).
cnf(t1724,plain,
rd(mult(mult(X1,X2),X2),rd(X2,X2)) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t221260]) ).
cnf(t1757,plain,
rd(mult(mult(mult(X1,X2),X2),X2),rd(X2,X2)) = mult(mult(X1,mult(X2,X2)),X2),
inference(cp,[status(thm)],[t900,t1724]) ).
cnf(t221261,plain,
mult(mult(X1,X2),mult(X2,X2)) = mult(mult(X1,mult(X2,X2)),X2),
inference(step,[status(thm)],[t1757,t1724]) ).
cnf(t1772,plain,
mult(mult(X1,mult(X2,X2)),X2) = mult(mult(X1,X2),mult(X2,X2)),
inference(orient,[status(thm)],[t221261]) ).
cnf(t620,plain,
mult(ld(X1,rd(rd(X1,X2),X2)),X2) = ld(X2,rd(rd(X1,X2),rd(X1,X2))),
inference(cp,[status(thm)],[t504,t614]) ).
cnf(t9064,plain,
ld(X1,rd(rd(X2,X1),rd(X2,X1))) = mult(ld(X2,rd(rd(X2,X1),X1)),X1),
inference(orient,[status(thm)],[t620]) ).
cnf(t9103,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)],[t9064,t684]) ).
cnf(t221384,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)],[t9103,t617]) ).
cnf(t221385,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)],[t221384,t1548]) ).
cnf(t612,plain,
ld(X1,rd(X1,rd(X2,X2))) = ld(rd(X3,ld(X2,X2)),X3),
inference(cp,[status(thm)],[t348,t590]) ).
cnf(t221204,plain,
ld(X1,rd(X1,rd(X2,X2))) = ld(X2,X2),
inference(step,[status(thm)],[t612,t24]) ).
cnf(t221205,plain,
ld(X1,rd(X1,rd(X2,X2))) = rd(X2,X2),
inference(step,[status(thm)],[t221204,t614]) ).
cnf(t644,plain,
ld(X1,rd(X1,rd(X2,X2))) = rd(X2,X2),
inference(orient,[status(thm)],[t221205]) ).
cnf(t4127,plain,
mult(rd(X1,X1),mult(rd(X1,X1),X2)) = ld(rd(rd(X1,X1),rd(X1,X1)),X2),
inference(cp,[status(thm)],[t4111,t644]) ).
cnf(t221341,plain,
mult(rd(X1,X1),mult(rd(X1,X1),X2)) = ld(rd(X1,X1),X2),
inference(step,[status(thm)],[t4127,t989]) ).
cnf(t4356,plain,
mult(rd(X1,X1),mult(rd(X1,X1),X2)) = ld(rd(X1,X1),X2),
inference(orient,[status(thm)],[t221341]) ).
cnf(t221386,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)],[t221385,t4356]) ).
cnf(t221387,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)],[t221386,t614]) ).
cnf(t221388,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)],[t221387,t989]) ).
cnf(t221389,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)],[t221388,t614]) ).
cnf(t221390,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)],[t221389,t1548]) ).
cnf(t221391,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)],[t221390,t8]) ).
cnf(t221392,plain,
rd(X1,mult(rd(X2,X2),X1)) = ld(rd(X2,X2),rd(X1,X1)),
inference(step,[status(thm)],[t221391,t684]) ).
cnf(t9192,plain,
ld(rd(X1,X1),rd(X2,X2)) = rd(X2,mult(rd(X1,X1),X2)),
inference(orient,[status(thm)],[t221392]) ).
cnf(t9230,plain,
mult(ld(X1,rd(rd(X2,X2),X1)),X1) = ld(X1,rd(X2,mult(rd(X1,X1),X2))),
inference(cp,[status(thm)],[t504,t9192]) ).
cnf(t15264,plain,
ld(X1,rd(X2,mult(rd(X1,X1),X2))) = mult(ld(X1,rd(rd(X2,X2),X1)),X1),
inference(orient,[status(thm)],[t9230]) ).
cnf(t20176,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)],[t20143,t15264]) ).
cnf(t221500,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)],[t20176,t8]) ).
cnf(t221501,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)],[t221500,t8]) ).
cnf(t221502,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)],[t221501,t1088]) ).
cnf(t1187,plain,
mult(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))) = ld(ld(X2,mult(X2,X1)),rd(X1,mult(X1,X1))),
inference(cp,[status(thm)],[t1053,t1174]) ).
cnf(t221236,plain,
rd(rd(X1,mult(X1,X1)),X1) = ld(ld(X2,mult(X2,X1)),rd(X1,mult(X1,X1))),
inference(step,[status(thm)],[t1187,t1132]) ).
cnf(t221237,plain,
rd(rd(X1,mult(X1,X1)),X1) = ld(X1,rd(X1,mult(X1,X1))),
inference(step,[status(thm)],[t221236,t12]) ).
cnf(t1274,plain,
ld(X1,rd(X1,mult(X1,X1))) = rd(rd(X1,mult(X1,X1)),X1),
inference(orient,[status(thm)],[t221237]) ).
cnf(t221251,plain,
ld(X1,rd(X1,mult(X1,X1))) = rd(rd(X1,X1),mult(X1,X1)),
inference(step,[status(thm)],[t1274,t1480]) ).
cnf(t1481,plain,
ld(X1,rd(X1,mult(X1,X1))) = rd(rd(X1,X1),mult(X1,X1)),
inference(orient,[status(thm)],[t221251]) ).
cnf(t221254,plain,
ld(X1,rd(X1,mult(X1,X1))) = rd(X1,mult(X1,mult(X1,X1))),
inference(step,[status(thm)],[t1481,t1605]) ).
cnf(t1606,plain,
ld(X1,rd(X1,mult(X1,X1))) = rd(X1,mult(X1,mult(X1,X1))),
inference(orient,[status(thm)],[t221254]) ).
cnf(t221503,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)],[t221502,t1606]) ).
cnf(t221504,plain,
ld(X1,ld(X1,X2)) = mult(rd(rd(rd(X1,X1),X1),mult(rd(X1,X1),X1)),X2),
inference(step,[status(thm)],[t221503,t2564]) ).
cnf(t221505,plain,
ld(X1,ld(X1,X2)) = mult(rd(rd(X1,mult(X1,X1)),mult(rd(X1,X1),X1)),X2),
inference(step,[status(thm)],[t221504,t1088]) ).
cnf(t221506,plain,
ld(X1,ld(X1,X2)) = mult(rd(rd(X1,mult(X1,X1)),X1),X2),
inference(step,[status(thm)],[t221505,t8]) ).
cnf(t221507,plain,
ld(X1,ld(X1,X2)) = mult(rd(rd(X1,X1),mult(X1,X1)),X2),
inference(step,[status(thm)],[t221506,t2378]) ).
cnf(t221508,plain,
ld(X1,ld(X1,X2)) = mult(rd(X1,mult(X1,mult(X1,X1))),X2),
inference(step,[status(thm)],[t221507,t1605]) ).
cnf(t20450,plain,
mult(rd(X1,mult(X1,mult(X1,X1))),X2) = ld(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t221508]) ).
cnf(t835,plain,
mult(X1,X1) = rd(mult(X1,X1),rd(X1,X1)),
inference(cp,[status(thm)],[t634,t825]) ).
cnf(t850,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,X1),
inference(orient,[status(thm)],[t835]) ).
cnf(t3010,plain,
rd(ld(X1,rd(X1,X1)),X1) = ld(mult(mult(X1,X1),X1),X1),
inference(cp,[status(thm)],[t3000,t850]) ).
cnf(t221300,plain,
rd(rd(X1,mult(X1,X1)),X1) = ld(mult(mult(X1,X1),X1),X1),
inference(step,[status(thm)],[t3010,t1332]) ).
cnf(t221301,plain,
rd(rd(X1,X1),mult(X1,X1)) = ld(mult(mult(X1,X1),X1),X1),
inference(step,[status(thm)],[t221300,t2378]) ).
cnf(t221302,plain,
rd(X1,mult(X1,mult(X1,X1))) = ld(mult(mult(X1,X1),X1),X1),
inference(step,[status(thm)],[t221301,t1605]) ).
cnf(t859,plain,
mult(rd(mult(X1,X1),X1),mult(X1,X1)) = mult(mult(X1,X1),X1),
inference(cp,[status(thm)],[t782,t850]) ).
cnf(t221211,plain,
mult(X1,mult(X1,X1)) = mult(mult(X1,X1),X1),
inference(step,[status(thm)],[t859,t9]) ).
cnf(t865,plain,
mult(mult(X1,X1),X1) = mult(X1,mult(X1,X1)),
inference(orient,[status(thm)],[t221211]) ).
cnf(t221303,plain,
rd(X1,mult(X1,mult(X1,X1))) = ld(mult(X1,mult(X1,X1)),X1),
inference(step,[status(thm)],[t221302,t865]) ).
cnf(t221304,plain,
rd(X1,mult(X1,mult(X1,X1))) = ld(true,rd(true,mult(X1,X1))),
inference(step,[status(thm)],[t221303,t348]) ).
cnf(t3051,plain,
rd(X1,mult(X1,mult(X1,X1))) = ld(true,rd(true,mult(X1,X1))),
inference(orient,[status(thm)],[t221304]) ).
cnf(t20480,plain,
ld(X1,ld(X1,X2)) = mult(ld(true,rd(true,mult(X1,X1))),X2),
inference(cp,[status(thm)],[t20450,t3051]) ).
cnf(t20712,plain,
mult(ld(true,rd(true,mult(X1,X1))),X2) = ld(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t20480]) ).
cnf(t20740,plain,
ld(X1,ld(X1,X2)) = mult(ld(X3,rd(X3,mult(X1,X1))),X2),
inference(cp,[status(thm)],[t20712,t389]) ).
cnf(t20979,plain,
mult(ld(X1,rd(X1,mult(X2,X2))),X3) = ld(X2,ld(X2,X3)),
inference(orient,[status(thm)],[t20740]) ).
cnf(t21238,plain,
ld(mult(X1,X1),mult(X2,mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),mult(X1,X1)),
inference(cp,[status(thm)],[t5111,t20979]) ).
cnf(t23082,plain,
ld(mult(X1,X1),mult(X2,mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),mult(X1,X1)),
inference(orient,[status(thm)],[t21238]) ).
cnf(t3966,plain,
rd(ld(X1,mult(mult(mult(X1,X1),mult(X2,mult(X1,X1))),X1)),X1) = mult(mult(X1,X2),mult(X1,X1)),
inference(cp,[status(thm)],[t3965,t25]) ).
cnf(t221728,plain,
rd(ld(X1,mult(X1,mult(X1,mult(mult(X2,mult(X1,X1)),X1)))),X1) = mult(mult(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t3966,t14]) ).
cnf(t21792,plain,
X1 = ld(rd(X2,mult(X3,mult(X3,X2))),ld(X3,ld(X3,X1))),
inference(cp,[status(thm)],[t12,t21683]) ).
cnf(t29009,plain,
ld(rd(X1,mult(X2,mult(X2,X1))),ld(X2,ld(X2,X3))) = X3,
inference(orient,[status(thm)],[t21792]) ).
cnf(t29126,plain,
mult(X1,X2) = ld(rd(X3,mult(X1,mult(X1,X3))),ld(X1,X2)),
inference(cp,[status(thm)],[t29009,t12]) ).
cnf(t29396,plain,
ld(rd(X1,mult(X2,mult(X2,X1))),ld(X2,X3)) = mult(X2,X3),
inference(orient,[status(thm)],[t29126]) ).
cnf(t29505,plain,
mult(X1,mult(X1,X2)) = ld(rd(X3,mult(X1,mult(X1,X3))),X2),
inference(cp,[status(thm)],[t29396,t12]) ).
cnf(t29624,plain,
ld(rd(X1,mult(X2,mult(X2,X1))),X3) = mult(X2,mult(X2,X3)),
inference(orient,[status(thm)],[t29505]) ).
cnf(t29797,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)],[t456,t29624]) ).
cnf(t221586,plain,
mult(ld(ld(X2,ld(X2,X3)),Y3),X3) = ld(X3,mult(X2,mult(X2,mult(Y3,X3)))),
inference(step,[status(thm)],[t29797,t21683]) ).
cnf(t30074,plain,
ld(X1,mult(X2,mult(X2,mult(X3,X1)))) = mult(ld(ld(X2,ld(X2,X1)),X3),X1),
inference(orient,[status(thm)],[t221586]) ).
cnf(t221729,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)],[t221728,t30074]) ).
cnf(t221730,plain,
ld(ld(X1,ld(X1,X1)),mult(X2,mult(X1,X1))) = mult(mult(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t221729,t9]) ).
cnf(t221731,plain,
ld(ld(X1,rd(X1,X1)),mult(X2,mult(X1,X1))) = mult(mult(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t221730,t614]) ).
cnf(t221732,plain,
ld(rd(X1,mult(X1,X1)),mult(X2,mult(X1,X1))) = mult(mult(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t221731,t1332]) ).
cnf(t221733,plain,
rd(mult(X1,mult(mult(X2,mult(X1,X1)),X1)),X1) = mult(mult(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t221732,t2930]) ).
cnf(t221734,plain,
rd(mult(X1,mult(mult(X2,X1),mult(X1,X1))),X1) = mult(mult(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t221733,t1772]) ).
cnf(t54158,plain,
rd(mult(X1,mult(mult(X2,X1),mult(X1,X1))),X1) = mult(mult(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t221734]) ).
cnf(t54251,plain,
mult(mult(X1,rd(X2,X1)),mult(X1,X1)) = rd(mult(X1,mult(X2,mult(X1,X1))),X1),
inference(cp,[status(thm)],[t54158,t8]) ).
cnf(t54460,plain,
mult(mult(X1,rd(X2,X1)),mult(X1,X1)) = rd(mult(X1,mult(X2,mult(X1,X1))),X1),
inference(orient,[status(thm)],[t54251]) ).
cnf(t54602,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)],[t23082,t54460]) ).
cnf(t221736,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)],[t54602,t12]) ).
cnf(t221737,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)],[t221736,t1429]) ).
cnf(t221738,plain,
mult(ld(X1,rd(X2,X1)),mult(X1,X1)) = rd(ld(X1,mult(X2,mult(X1,X1))),X1),
inference(step,[status(thm)],[t221737,t12]) ).
cnf(t54945,plain,
mult(ld(X1,rd(X2,X1)),mult(X1,X1)) = rd(ld(X1,mult(X2,mult(X1,X1))),X1),
inference(orient,[status(thm)],[t221738]) ).
cnf(t55131,plain,
mult(mult(ld(X1,rd(X2,X1)),X1),mult(X1,X1)) = mult(rd(ld(X1,mult(X2,mult(X1,X1))),X1),X1),
inference(cp,[status(thm)],[t1772,t54945]) ).
cnf(t221983,plain,
mult(mult(ld(X1,rd(X2,X1)),X1),mult(X1,X1)) = ld(X1,mult(X2,mult(X1,X1))),
inference(step,[status(thm)],[t55131,t8]) ).
cnf(t90217,plain,
mult(mult(ld(X1,rd(X2,X1)),X1),mult(X1,X1)) = ld(X1,mult(X2,mult(X1,X1))),
inference(orient,[status(thm)],[t221983]) ).
cnf(t90263,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)],[t90217,t3755]) ).
cnf(t222107,plain,
ld(X1,mult(mult(rd(X1,X1),X2),mult(X1,X1))) = mult(ld(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t90263,t8]) ).
cnf(t103012,plain,
ld(X1,mult(mult(rd(X1,X1),X2),mult(X1,X1))) = mult(ld(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t222107]) ).
cnf(t103023,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)],[t103012,t34]) ).
cnf(t2956,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = ld(mult(X1,X1),rd(mult(X1,mult(X2,X1)),X1)),
inference(cp,[status(thm)],[t504,t2930]) ).
cnf(t221713,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = rd(ld(X1,ld(X1,mult(X1,mult(X2,X1)))),X1),
inference(step,[status(thm)],[t2956,t1429]) ).
cnf(t20251,plain,
mult(rd(ld(X1,rd(X1,X2)),X2),mult(X3,mult(Y3,X3))) = mult(mult(ld(X2,ld(X2,X3)),Y3),X3),
inference(cp,[status(thm)],[t14,t20143]) ).
cnf(t221516,plain,
ld(X2,ld(X2,mult(X3,mult(Y3,X3)))) = mult(mult(ld(X2,ld(X2,X3)),Y3),X3),
inference(step,[status(thm)],[t20251,t20143]) ).
cnf(t22209,plain,
ld(X1,ld(X1,mult(X2,mult(X3,X2)))) = mult(mult(ld(X1,ld(X1,X2)),X3),X2),
inference(orient,[status(thm)],[t221516]) ).
cnf(t221714,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)],[t221713,t22209]) ).
cnf(t221715,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = mult(ld(X1,ld(X1,X1)),X2),
inference(step,[status(thm)],[t221714,t9]) ).
cnf(t221716,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = mult(ld(X1,rd(X1,X1)),X2),
inference(step,[status(thm)],[t221715,t614]) ).
cnf(t221717,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = mult(rd(X1,mult(X1,X1)),X2),
inference(step,[status(thm)],[t221716,t1332]) ).
cnf(t221718,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = rd(ld(X1,mult(X2,X1)),X1),
inference(step,[status(thm)],[t221717,t3965]) ).
cnf(t50563,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = rd(ld(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t221718]) ).
cnf(t222237,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)],[t103023,t50563]) ).
cnf(t222238,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)],[t222237,t1605]) ).
cnf(t222239,plain,
rd(ld(X1,mult(X2,X1)),X1) = ld(X1,ld(X1,ld(X1,mult(mult(X1,X1),X2)))),
inference(step,[status(thm)],[t222238,t21683]) ).
cnf(t116934,plain,
ld(X1,ld(X1,ld(X1,mult(mult(X1,X1),X2)))) = rd(ld(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t222239]) ).
cnf(t222,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,t215]) ).
cnf(t221637,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)],[t222,t215]) ).
cnf(t221638,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)],[t221637,t196]) ).
cnf(t221639,plain,
mult(mult(X1,X3),mult(ld(X2,rd(X2,X3)),Y3)) = rd(mult(X1,mult(Y3,X3)),X3),
inference(step,[status(thm)],[t221638,t24]) ).
cnf(t36652,plain,
mult(mult(X1,X2),mult(ld(X3,rd(X3,X2)),Y3)) = rd(mult(X1,mult(Y3,X2)),X2),
inference(orient,[status(thm)],[t221639]) ).
cnf(t116963,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)],[t116934,t36652]) ).
cnf(t222240,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)],[t116963,t5111]) ).
cnf(t222241,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)],[t222240,t456]) ).
cnf(t222242,plain,
ld(mult(X1,X1),X3) = ld(X1,ld(X1,ld(X1,rd(mult(X1,mult(X3,X1)),X1)))),
inference(step,[status(thm)],[t222241,t9]) ).
cnf(t21777,plain,
ld(rd(X1,X2),ld(rd(X1,X2),X3)) = mult(rd(X2,mult(rd(X1,X2),X1)),X3),
inference(cp,[status(thm)],[t21683,t8]) ).
cnf(t23506,plain,
ld(rd(X1,X2),ld(rd(X1,X2),X3)) = mult(rd(X2,mult(rd(X1,X2),X1)),X3),
inference(orient,[status(thm)],[t21777]) ).
cnf(t105519,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)],[t23506,t105330]) ).
cnf(t222132,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)],[t105519,t196]) ).
cnf(t222133,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)],[t222132,t8]) ).
cnf(t222134,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)],[t222133,t105330]) ).
cnf(t222135,plain,
rd(rd(X1,X1),ld(mult(X2,X1),X1)) = ld(X1,mult(ld(rd(X1,X1),X2),X1)),
inference(step,[status(thm)],[t222134,t4356]) ).
cnf(t105924,plain,
ld(X1,mult(ld(rd(X1,X1),X2),X1)) = rd(rd(X1,X1),ld(mult(X2,X1),X1)),
inference(orient,[status(thm)],[t222135]) ).
cnf(t1444,plain,
rd(ld(X1,ld(ld(X2,rd(X2,X1)),X3)),X1) = ld(rd(X1,X1),rd(X3,X1)),
inference(cp,[status(thm)],[t1429,t615]) ).
cnf(t42597,plain,
rd(ld(X1,ld(ld(X2,rd(X2,X1)),X3)),X1) = ld(rd(X1,X1),rd(X3,X1)),
inference(orient,[status(thm)],[t1444]) ).
cnf(t4643,plain,
ld(ld(X1,rd(X1,X2)),rd(X1,X2)) = rd(mult(X2,X1),ld(rd(X1,X2),X1)),
inference(cp,[status(thm)],[t4621,t24]) ).
cnf(t221346,plain,
ld(ld(X1,rd(X1,X2)),rd(X1,X2)) = rd(mult(X2,X1),X2),
inference(step,[status(thm)],[t4643,t24]) ).
cnf(t4799,plain,
ld(ld(X1,rd(X1,X2)),rd(X1,X2)) = rd(mult(X2,X1),X2),
inference(orient,[status(thm)],[t221346]) ).
cnf(t4808,plain,
rd(mult(X1,X2),X1) = ld(ld(X3,rd(X3,X1)),rd(X2,X1)),
inference(cp,[status(thm)],[t4799,t389]) ).
cnf(t5016,plain,
ld(ld(X1,rd(X1,X2)),rd(X3,X2)) = rd(mult(X2,X3),X2),
inference(orient,[status(thm)],[t4808]) ).
cnf(t42608,plain,
ld(rd(X1,X1),rd(rd(X2,X1),X1)) = rd(ld(X1,rd(mult(X1,X2),X1)),X1),
inference(cp,[status(thm)],[t42597,t5016]) ).
cnf(t42873,plain,
ld(rd(X1,X1),rd(rd(X2,X1),X1)) = rd(ld(X1,rd(mult(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t42608]) ).
cnf(t105980,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)],[t105924,t42873]) ).
cnf(t222146,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)],[t105980,t8]) ).
cnf(t222147,plain,
rd(rd(X1,X1),ld(rd(X2,X1),X1)) = ld(X1,ld(X1,rd(mult(X1,X2),X1))),
inference(step,[status(thm)],[t222146,t8]) ).
cnf(t107698,plain,
ld(X1,ld(X1,rd(mult(X1,X2),X1))) = rd(rd(X1,X1),ld(rd(X2,X1),X1)),
inference(orient,[status(thm)],[t222147]) ).
cnf(t222243,plain,
ld(mult(X1,X1),X3) = ld(X1,rd(rd(X1,X1),ld(rd(mult(X3,X1),X1),X1))),
inference(step,[status(thm)],[t222242,t107698]) ).
cnf(t222244,plain,
ld(mult(X1,X1),X3) = ld(X1,rd(rd(X1,X1),ld(X3,X1))),
inference(step,[status(thm)],[t222243,t9]) ).
cnf(t117220,plain,
ld(X1,rd(rd(X1,X1),ld(X2,X1))) = ld(mult(X1,X1),X2),
inference(orient,[status(thm)],[t222244]) ).
cnf(t117394,plain,
ld(mult(X1,X1),rd(X1,X2)) = ld(X1,rd(rd(X1,X1),X2)),
inference(cp,[status(thm)],[t117220,t24]) ).
cnf(t117571,plain,
ld(mult(X1,X1),rd(X1,X2)) = ld(X1,rd(rd(X1,X1),X2)),
inference(orient,[status(thm)],[t117394]) ).
cnf(t117760,plain,
mult(X1,X1) = rd(rd(X1,X2),ld(X1,rd(rd(X1,X1),X2))),
inference(cp,[status(thm)],[t23,t117571]) ).
cnf(t119729,plain,
rd(rd(X1,X2),ld(X1,rd(rd(X1,X1),X2))) = mult(X1,X1),
inference(orient,[status(thm)],[t117760]) ).
cnf(t119988,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)],[t45802,t119729]) ).
cnf(t222254,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)],[t119988,t215]) ).
cnf(t222255,plain,
rd(X1,ld(rd(X1,X2),rd(X1,X1))) = rd(mult(X1,X1),ld(rd(X1,X2),X1)),
inference(step,[status(thm)],[t222254,t8]) ).
cnf(t222256,plain,
rd(X1,ld(rd(X1,X2),rd(X1,X1))) = rd(mult(X1,X1),X2),
inference(step,[status(thm)],[t222255,t24]) ).
cnf(t120116,plain,
rd(X1,ld(rd(X1,X2),rd(X1,X1))) = rd(mult(X1,X1),X2),
inference(orient,[status(thm)],[t222256]) ).
cnf(t120396,plain,
ld(rd(X1,X1),rd(X1,X2)) = ld(X1,rd(mult(X1,X1),X2)),
inference(cp,[status(thm)],[t224,t120116]) ).
cnf(t121773,plain,
ld(rd(X1,X1),rd(X1,X2)) = ld(X1,rd(mult(X1,X1),X2)),
inference(orient,[status(thm)],[t120396]) ).
cnf(t121814,plain,
ld(X1,rd(mult(X1,X1),rd(X2,mult(X2,X2)))) = ld(rd(X1,X1),mult(X1,X2)),
inference(cp,[status(thm)],[t121773,t1174]) ).
cnf(t222264,plain,
ld(X1,mult(mult(X1,X1),X2)) = ld(rd(X1,X1),mult(X1,X2)),
inference(step,[status(thm)],[t121814,t1174]) ).
cnf(t122325,plain,
ld(rd(X1,X1),mult(X1,X2)) = ld(X1,mult(mult(X1,X1),X2)),
inference(orient,[status(thm)],[t222264]) ).
cnf(t122510,plain,
mult(ld(X1,rd(mult(X1,X2),X1)),X1) = ld(X1,ld(X1,mult(mult(X1,X1),X2))),
inference(cp,[status(thm)],[t504,t122325]) ).
cnf(t128402,plain,
ld(X1,ld(X1,mult(mult(X1,X1),X2))) = mult(ld(X1,rd(mult(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t122510]) ).
cnf(t128502,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)],[t108253,t128402]) ).
cnf(t222287,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)],[t128502,t14]) ).
cnf(t222288,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)],[t222287,t30074]) ).
cnf(t222289,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)],[t222288,t9]) ).
cnf(t222290,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)],[t222289,t614]) ).
cnf(t222291,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)],[t222290,t1332]) ).
cnf(t222292,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)],[t222291,t2930]) ).
cnf(t1099,plain,
mult(ld(rd(X1,X1),rd(X2,X1)),X1) = ld(X1,ld(rd(X1,mult(X1,X1)),X2)),
inference(cp,[status(thm)],[t504,t1088]) ).
cnf(t221394,plain,
mult(ld(rd(X1,X1),rd(X2,X1)),X1) = ld(X1,rd(mult(X1,mult(X2,X1)),X1)),
inference(step,[status(thm)],[t1099,t2930]) ).
cnf(t9966,plain,
ld(X1,rd(mult(X1,mult(X2,X1)),X1)) = mult(ld(rd(X1,X1),rd(X2,X1)),X1),
inference(orient,[status(thm)],[t221394]) ).
cnf(t222293,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)],[t222292,t9966]) ).
cnf(t222294,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)],[t222293,t83]) ).
cnf(t117832,plain,
ld(rd(X1,X2),mult(X1,X1)) = ld(X3,rd(X3,ld(X1,rd(rd(X1,X1),X2)))),
inference(cp,[status(thm)],[t224,t117571]) ).
cnf(t222246,plain,
ld(rd(X1,X2),mult(X1,X1)) = ld(rd(rd(X1,X1),X2),X1),
inference(step,[status(thm)],[t117832,t224]) ).
cnf(t118210,plain,
ld(rd(rd(X1,X1),X2),X1) = ld(rd(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t222246]) ).
cnf(t118284,plain,
rd(rd(X1,X1),X2) = rd(X1,ld(rd(X1,X2),mult(X1,X1))),
inference(cp,[status(thm)],[t23,t118210]) ).
cnf(t118668,plain,
rd(X1,ld(rd(X1,X2),mult(X1,X1))) = rd(rd(X1,X1),X2),
inference(orient,[status(thm)],[t118284]) ).
cnf(t118693,plain,
rd(rd(X1,X1),ld(X2,X1)) = rd(X1,ld(X2,mult(X1,X1))),
inference(cp,[status(thm)],[t118668,t23]) ).
cnf(t119030,plain,
rd(rd(X1,X1),ld(X2,X1)) = rd(X1,ld(X2,mult(X1,X1))),
inference(orient,[status(thm)],[t118693]) ).
cnf(t222250,plain,
ld(X1,ld(X1,rd(mult(X1,X2),X1))) = rd(X1,ld(rd(X2,X1),mult(X1,X1))),
inference(step,[status(thm)],[t107698,t119030]) ).
cnf(t222251,plain,
ld(X1,ld(X1,rd(mult(X1,X2),X1))) = rd(X1,mult(X1,mult(ld(X2,X1),X1))),
inference(step,[status(thm)],[t222250,t83]) ).
cnf(t119033,plain,
ld(X1,ld(X1,rd(mult(X1,X2),X1))) = rd(X1,mult(X1,mult(ld(X2,X1),X1))),
inference(orient,[status(thm)],[t222251]) ).
cnf(t222295,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)],[t222294,t119033]) ).
cnf(t222296,plain,
mult(ld(rd(X1,X1),rd(X2,X1)),X1) = mult(X1,rd(rd(X1,X1),ld(X2,X1))),
inference(step,[status(thm)],[t222295,t2564]) ).
cnf(t222297,plain,
mult(ld(rd(X1,X1),rd(X2,X1)),X1) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
inference(step,[status(thm)],[t222296,t119030]) ).
cnf(t129466,plain,
mult(ld(rd(X1,X1),rd(X2,X1)),X1) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
inference(orient,[status(thm)],[t222297]) ).
cnf(t129673,plain,
mult(X1,rd(X1,ld(mult(X2,X1),mult(X1,X1)))) = mult(ld(rd(X1,X1),X2),X1),
inference(cp,[status(thm)],[t129466,t9]) ).
cnf(t160239,plain,
mult(X1,rd(X1,ld(mult(X2,X1),mult(X1,X1)))) = mult(ld(rd(X1,X1),X2),X1),
inference(orient,[status(thm)],[t129673]) ).
cnf(t1092,plain,
mult(X1,mult(ld(rd(X1,X1),X2),X1)) = ld(rd(X1,mult(X1,X1)),mult(X2,X1)),
inference(cp,[status(thm)],[t83,t1088]) ).
cnf(t221393,plain,
mult(X1,mult(ld(rd(X1,X1),X2),X1)) = rd(mult(X1,mult(mult(X2,X1),X1)),X1),
inference(step,[status(thm)],[t1092,t2930]) ).
cnf(t9866,plain,
mult(X1,mult(ld(rd(X1,X1),X2),X1)) = rd(mult(X1,mult(mult(X2,X1),X1)),X1),
inference(orient,[status(thm)],[t221393]) ).
cnf(t105705,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)],[t105626,t1132]) ).
cnf(t222138,plain,
rd(mult(X1,rd(rd(X1,X1),X2)),X1) = ld(rd(X1,X1),rd(rd(X1,X2),X1)),
inference(step,[status(thm)],[t105705,t1132]) ).
cnf(t106743,plain,
ld(rd(X1,X1),rd(rd(X1,X2),X1)) = rd(mult(X1,rd(rd(X1,X1),X2)),X1),
inference(orient,[status(thm)],[t222138]) ).
cnf(t107080,plain,
rd(mult(X1,mult(mult(rd(rd(X1,X2),X1),X1),X1)),X1) = mult(X1,mult(rd(mult(X1,rd(rd(X1,X1),X2)),X1),X1)),
inference(cp,[status(thm)],[t9866,t106743]) ).
cnf(t222162,plain,
rd(mult(X1,mult(rd(X1,X2),X1)),X1) = mult(X1,mult(rd(mult(X1,rd(rd(X1,X1),X2)),X1),X1)),
inference(step,[status(thm)],[t107080,t8]) ).
cnf(t222163,plain,
rd(mult(X1,mult(rd(X1,X2),X1)),X1) = mult(X1,mult(X1,rd(rd(X1,X1),X2))),
inference(step,[status(thm)],[t222162,t8]) ).
cnf(t108820,plain,
mult(X1,mult(X1,rd(rd(X1,X1),X2))) = rd(mult(X1,mult(rd(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t222163]) ).
cnf(t108889,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)],[t108820,t1174]) ).
cnf(t222192,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)],[t108889,t1174]) ).
cnf(t222193,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)],[t222192,t3965]) ).
cnf(t222194,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)],[t222193,t8]) ).
cnf(t222195,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)],[t222194,t1132]) ).
cnf(t1565,plain,
rd(rd(X1,X1),mult(X1,mult(X2,X1))) = rd(rd(rd(X1,mult(X1,X1)),X2),X1),
inference(cp,[status(thm)],[t1548,t1088]) ).
cnf(t11273,plain,
rd(rd(rd(X1,mult(X1,X1)),X2),X1) = rd(rd(X1,X1),mult(X1,mult(X2,X1))),
inference(orient,[status(thm)],[t1565]) ).
cnf(t222196,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)],[t222195,t11273]) ).
cnf(t222197,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)],[t222196,t2564]) ).
cnf(t222198,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)],[t222197,t1088]) ).
cnf(t222199,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)],[t222198,t3965]) ).
cnf(t222200,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)],[t222199,t3965]) ).
cnf(t222201,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)],[t222200,t8]) ).
cnf(t222202,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)],[t222201,t456]) ).
cnf(t222203,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)],[t222202,t9]) ).
cnf(t222204,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)],[t222203,t2624]) ).
cnf(t222205,plain,
ld(X1,rd(rd(X1,mult(X1,X1)),X2)) = ld(mult(X1,X1),rd(rd(X1,X1),X2)),
inference(step,[status(thm)],[t222204,t989]) ).
cnf(t110166,plain,
ld(mult(X1,X1),rd(rd(X1,X1),X2)) = ld(X1,rd(rd(X1,mult(X1,X1)),X2)),
inference(orient,[status(thm)],[t222205]) ).
cnf(t110203,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)],[t110166,t3289]) ).
cnf(t3304,plain,
mult(rd(rd(X1,X1),X2),X1) = rd(rd(X1,mult(X1,X1)),rd(ld(X1,X2),X1)),
inference(cp,[status(thm)],[t3289,t1088]) ).
cnf(t52167,plain,
rd(rd(X1,mult(X1,X1)),rd(ld(X1,X2),X1)) = mult(rd(rd(X1,X1),X2),X1),
inference(orient,[status(thm)],[t3304]) ).
cnf(t222212,plain,
ld(X1,mult(rd(rd(X1,X1),X2),X1)) = ld(mult(X1,X1),mult(rd(X1,X2),X1)),
inference(step,[status(thm)],[t110203,t52167]) ).
cnf(t111073,plain,
ld(mult(X1,X1),mult(rd(X1,X2),X1)) = ld(X1,mult(rd(rd(X1,X1),X2),X1)),
inference(orient,[status(thm)],[t222212]) ).
cnf(t111354,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)],[t224,t111073]) ).
cnf(t222218,plain,
ld(mult(rd(X1,X2),X1),mult(X1,X1)) = ld(mult(rd(rd(X1,X1),X2),X1),X1),
inference(step,[status(thm)],[t111354,t224]) ).
cnf(t111947,plain,
ld(mult(rd(rd(X1,X1),X2),X1),X1) = ld(mult(rd(X1,X2),X1),mult(X1,X1)),
inference(orient,[status(thm)],[t222218]) ).
cnf(t112043,plain,
mult(rd(rd(X1,X1),X2),X1) = rd(X1,ld(mult(rd(X1,X2),X1),mult(X1,X1))),
inference(cp,[status(thm)],[t23,t111947]) ).
cnf(t141891,plain,
rd(X1,ld(mult(rd(X1,X2),X1),mult(X1,X1))) = mult(rd(rd(X1,X1),X2),X1),
inference(orient,[status(thm)],[t112043]) ).
cnf(t160244,plain,
mult(ld(rd(X1,X1),rd(X1,X2)),X1) = mult(X1,mult(rd(rd(X1,X1),X2),X1)),
inference(cp,[status(thm)],[t160239,t141891]) ).
cnf(t222526,plain,
mult(ld(X1,rd(mult(X1,X1),X2)),X1) = mult(X1,mult(rd(rd(X1,X1),X2),X1)),
inference(step,[status(thm)],[t160244,t121773]) ).
cnf(t160657,plain,
mult(ld(X1,rd(mult(X1,X1),X2)),X1) = mult(X1,mult(rd(rd(X1,X1),X2),X1)),
inference(orient,[status(thm)],[t222526]) ).
cnf(t119221,plain,
ld(X1,X2) = ld(rd(X2,ld(X1,mult(X2,X2))),rd(X2,X2)),
inference(cp,[status(thm)],[t24,t119030]) ).
cnf(t123838,plain,
ld(rd(X1,ld(X2,mult(X1,X1))),rd(X1,X1)) = ld(X2,X1),
inference(orient,[status(thm)],[t119221]) ).
cnf(t108502,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)],[t224,t108253]) ).
cnf(t222191,plain,
ld(ld(X1,ld(X1,X2)),rd(X1,X1)) = ld(rd(ld(X1,mult(X2,X1)),X1),X1),
inference(step,[status(thm)],[t108502,t224]) ).
cnf(t109857,plain,
ld(rd(ld(X1,mult(X2,X1)),X1),X1) = ld(ld(X1,ld(X1,X2)),rd(X1,X1)),
inference(orient,[status(thm)],[t222191]) ).
cnf(t110004,plain,
ld(ld(X1,ld(X1,rd(X2,X1))),rd(X1,X1)) = ld(rd(ld(X1,X2),X1),X1),
inference(cp,[status(thm)],[t109857,t8]) ).
cnf(t105912,plain,
rd(mult(X1,mult(mult(rd(mult(X1,X2),X1),X1),X1)),X1) = mult(X1,mult(rd(mult(X1,mult(rd(X1,X1),X2)),X1),X1)),
inference(cp,[status(thm)],[t9866,t105626]) ).
cnf(t222144,plain,
rd(mult(X1,mult(mult(X1,X2),X1)),X1) = mult(X1,mult(rd(mult(X1,mult(rd(X1,X1),X2)),X1),X1)),
inference(step,[status(thm)],[t105912,t8]) ).
cnf(t222145,plain,
rd(mult(X1,mult(mult(X1,X2),X1)),X1) = mult(X1,mult(X1,mult(rd(X1,X1),X2))),
inference(step,[status(thm)],[t222144,t8]) ).
cnf(t107403,plain,
mult(X1,mult(X1,mult(rd(X1,X1),X2))) = rd(mult(X1,mult(mult(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t222145]) ).
cnf(t107493,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)],[t107403,t1174]) ).
cnf(t222164,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)],[t107493,t1174]) ).
cnf(t222165,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)],[t222164,t3965]) ).
cnf(t222166,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)],[t222165,t8]) ).
cnf(t222167,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)],[t222166,t1132]) ).
cnf(t222168,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)],[t222167,t8]) ).
cnf(t222169,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)],[t222168,t3965]) ).
cnf(t222170,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)],[t222169,t3965]) ).
cnf(t222171,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)],[t222170,t3965]) ).
cnf(t222172,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)],[t222171,t8]) ).
cnf(t222173,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)],[t222172,t456]) ).
cnf(t222174,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)],[t222173,t9]) ).
cnf(t222175,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)],[t222174,t2624]) ).
cnf(t222176,plain,
ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(mult(X1,X1),mult(rd(X1,X1),X2)),
inference(step,[status(thm)],[t222175,t989]) ).
cnf(t109094,plain,
ld(mult(X1,X1),mult(rd(X1,X1),X2)) = ld(X1,rd(ld(X1,mult(X2,X1)),X1)),
inference(orient,[status(thm)],[t222176]) ).
cnf(t109280,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)],[t224,t109094]) ).
cnf(t222208,plain,
ld(mult(rd(X1,X1),X2),mult(X1,X1)) = ld(rd(ld(X1,mult(X2,X1)),X1),X1),
inference(step,[status(thm)],[t109280,t224]) ).
cnf(t222209,plain,
ld(mult(rd(X1,X1),X2),mult(X1,X1)) = ld(ld(X1,ld(X1,X2)),rd(X1,X1)),
inference(step,[status(thm)],[t222208,t109857]) ).
cnf(t110748,plain,
ld(ld(X1,ld(X1,X2)),rd(X1,X1)) = ld(mult(rd(X1,X1),X2),mult(X1,X1)),
inference(orient,[status(thm)],[t222209]) ).
cnf(t222377,plain,
ld(mult(rd(X1,X1),rd(X2,X1)),mult(X1,X1)) = ld(rd(ld(X1,X2),X1),X1),
inference(step,[status(thm)],[t110004,t110748]) ).
cnf(t140433,plain,
ld(mult(rd(X1,X1),rd(X2,X1)),mult(X1,X1)) = ld(rd(ld(X1,X2),X1),X1),
inference(orient,[status(thm)],[t222377]) ).
cnf(t140733,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)],[t123838,t140433]) ).
cnf(t117407,plain,
ld(mult(X1,X1),mult(X1,X2)) = ld(X1,rd(rd(X1,X1),ld(X3,rd(X3,X2)))),
inference(cp,[status(thm)],[t117220,t348]) ).
cnf(t222245,plain,
ld(mult(X1,X1),mult(X1,X2)) = ld(X1,mult(rd(X1,X1),X2)),
inference(step,[status(thm)],[t117407,t215]) ).
cnf(t117925,plain,
ld(mult(X1,X1),mult(X1,X2)) = ld(X1,mult(rd(X1,X1),X2)),
inference(orient,[status(thm)],[t222245]) ).
cnf(t118126,plain,
ld(mult(X1,X2),mult(X1,X1)) = ld(X3,rd(X3,ld(X1,mult(rd(X1,X1),X2)))),
inference(cp,[status(thm)],[t224,t117925]) ).
cnf(t222247,plain,
ld(mult(X1,X2),mult(X1,X1)) = ld(mult(rd(X1,X1),X2),X1),
inference(step,[status(thm)],[t118126,t224]) ).
cnf(t118441,plain,
ld(mult(rd(X1,X1),X2),X1) = ld(mult(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t222247]) ).
cnf(t222378,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)],[t140733,t118441]) ).
cnf(t222379,plain,
ld(mult(X1,rd(X2,X1)),mult(X1,X1)) = ld(rd(ld(X1,X2),X1),rd(X1,X1)),
inference(step,[status(thm)],[t222378,t23]) ).
cnf(t140798,plain,
ld(mult(X1,rd(X2,X1)),mult(X1,X1)) = ld(rd(ld(X1,X2),X1),rd(X1,X1)),
inference(orient,[status(thm)],[t222379]) ).
cnf(t3987,plain,
rd(X1,mult(X1,X1)) = rd(rd(ld(X1,mult(X2,X1)),X1),X2),
inference(cp,[status(thm)],[t9,t3965]) ).
cnf(t4194,plain,
rd(rd(ld(X1,mult(X2,X1)),X1),X2) = rd(X1,mult(X1,X1)),
inference(orient,[status(thm)],[t3987]) ).
cnf(t140909,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)],[t140798,t4194]) ).
cnf(t3971,plain,
rd(ld(X1,mult(rd(X2,mult(X2,X2)),X1)),X1) = rd(rd(X1,mult(X1,X1)),X2),
inference(cp,[status(thm)],[t3965,t1132]) ).
cnf(t221739,plain,
rd(ld(X1,rd(ld(X2,mult(X1,X2)),X2)),X1) = rd(rd(X1,mult(X1,X1)),X2),
inference(step,[status(thm)],[t3971,t3965]) ).
cnf(t55627,plain,
rd(ld(X1,rd(ld(X2,mult(X1,X2)),X2)),X1) = rd(rd(X1,mult(X1,X1)),X2),
inference(orient,[status(thm)],[t221739]) ).
cnf(t222572,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)],[t140909,t55627]) ).
cnf(t222573,plain,
ld(rd(rd(X1,mult(X1,X1)),X2),rd(X1,X1)) = ld(rd(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t222572,t1132]) ).
cnf(t168270,plain,
ld(rd(rd(X1,mult(X1,X1)),X2),rd(X1,X1)) = ld(rd(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t222573]) ).
cnf(t9196,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)],[t9192,t1174]) ).
cnf(t221843,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)],[t9196,t1132]) ).
cnf(t221844,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)],[t221843,t2624]) ).
cnf(t221845,plain,
rd(rd(X1,mult(X1,X1)),rd(rd(X2,X2),X1)) = ld(rd(X2,X2),rd(X1,X1)),
inference(step,[status(thm)],[t221844,t989]) ).
cnf(t221846,plain,
rd(rd(X1,mult(X1,X1)),rd(rd(X2,X2),X1)) = rd(X1,mult(rd(X2,X2),X1)),
inference(step,[status(thm)],[t221845,t9192]) ).
cnf(t63882,plain,
rd(rd(X1,mult(X1,X1)),rd(rd(X2,X2),X1)) = rd(X1,mult(rd(X2,X2),X1)),
inference(orient,[status(thm)],[t221846]) ).
cnf(t168276,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)],[t168270,t63882]) ).
cnf(t9201,plain,
rd(rd(X1,X1),mult(rd(X2,X2),rd(X1,X1))) = ld(rd(X2,X2),rd(X1,X1)),
inference(cp,[status(thm)],[t9192,t989]) ).
cnf(t221854,plain,
rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = ld(rd(X2,X2),rd(X1,X1)),
inference(step,[status(thm)],[t9201,t617]) ).
cnf(t221855,plain,
rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = rd(X1,mult(rd(X2,X2),X1)),
inference(step,[status(thm)],[t221854,t9192]) ).
cnf(t64726,plain,
rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = rd(X1,mult(rd(X2,X2),X1)),
inference(orient,[status(thm)],[t221855]) ).
cnf(t64787,plain,
rd(rd(X1,X1),rd(X2,X2)) = ld(rd(X2,mult(rd(X1,X1),X2)),rd(X2,X2)),
inference(cp,[status(thm)],[t24,t64726]) ).
cnf(t94663,plain,
ld(rd(X1,mult(rd(X2,X2),X1)),rd(X1,X1)) = rd(rd(X2,X2),rd(X1,X1)),
inference(orient,[status(thm)],[t64787]) ).
cnf(t222753,plain,
ld(rd(X1,rd(rd(X2,X2),X1)),mult(X1,X1)) = rd(rd(X2,X2),rd(X1,X1)),
inference(step,[status(thm)],[t168276,t94663]) ).
cnf(t198266,plain,
ld(rd(X1,rd(rd(X2,X2),X1)),mult(X1,X1)) = rd(rd(X2,X2),rd(X1,X1)),
inference(orient,[status(thm)],[t222753]) ).
cnf(t198394,plain,
rd(X1,rd(rd(X2,X2),X1)) = rd(mult(X1,X1),rd(rd(X2,X2),rd(X1,X1))),
inference(cp,[status(thm)],[t23,t198266]) ).
cnf(t214533,plain,
rd(mult(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = rd(X1,rd(rd(X2,X2),X1)),
inference(orient,[status(thm)],[t198394]) ).
cnf(t214745,plain,
mult(X1,mult(rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))),X1)) = mult(ld(X1,rd(X1,rd(rd(X2,X2),X1))),X1),
inference(cp,[status(thm)],[t160657,t214533]) ).
cnf(t222864,plain,
mult(X1,mult(rd(X1,mult(rd(X2,X2),X1)),X1)) = mult(ld(X1,rd(X1,rd(rd(X2,X2),X1))),X1),
inference(step,[status(thm)],[t214745,t64726]) ).
cnf(t45803,plain,
rd(X1,ld(X2,rd(rd(X1,X3),ld(X1,X2)))) = rd(mult(X2,X3),ld(X2,X1)),
inference(cp,[status(thm)],[t45802,t215]) ).
cnf(t84557,plain,
rd(X1,ld(X2,rd(rd(X1,X3),ld(X1,X2)))) = rd(mult(X2,X3),ld(X2,X1)),
inference(orient,[status(thm)],[t45803]) ).
cnf(t84831,plain,
ld(X1,rd(rd(X2,X3),ld(X2,X1))) = ld(rd(mult(X1,X3),ld(X1,X2)),X2),
inference(cp,[status(thm)],[t24,t84557]) ).
cnf(t84990,plain,
ld(rd(mult(X1,X2),ld(X1,X3)),X3) = ld(X1,rd(rd(X3,X2),ld(X3,X1))),
inference(orient,[status(thm)],[t84831]) ).
cnf(t84997,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)],[t84990,t215]) ).
cnf(t221948,plain,
ld(X1,rd(rd(rd(X1,X2),X3),X2)) = ld(mult(mult(X1,X3),X2),rd(X1,X2)),
inference(step,[status(thm)],[t84997,t24]) ).
cnf(t221949,plain,
ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = ld(mult(mult(X1,X3),X2),rd(X1,X2)),
inference(step,[status(thm)],[t221948,t1548]) ).
cnf(t221950,plain,
ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = rd(ld(X2,ld(mult(X1,X3),X1)),X2),
inference(step,[status(thm)],[t221949,t1429]) ).
cnf(t221951,plain,
ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = rd(ld(X2,ld(true,rd(true,X3))),X2),
inference(step,[status(thm)],[t221950,t348]) ).
cnf(t85376,plain,
ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = rd(ld(X2,ld(true,rd(true,X3))),X2),
inference(orient,[status(thm)],[t221951]) ).
cnf(t85446,plain,
rd(ld(rd(X1,mult(X1,X1)),ld(true,rd(true,X2))),rd(X1,mult(X1,X1))) = ld(X3,rd(X3,rd(ld(X1,mult(mult(X2,rd(X1,mult(X1,X1))),X1)),X1))),
inference(cp,[status(thm)],[t85376,t3965]) ).
cnf(t221956,plain,
mult(ld(rd(X1,mult(X1,X1)),ld(true,rd(true,X2))),X1) = ld(X3,rd(X3,rd(ld(X1,mult(mult(X2,rd(X1,mult(X1,X1))),X1)),X1))),
inference(step,[status(thm)],[t85446,t1174]) ).
cnf(t221957,plain,
mult(rd(mult(X1,mult(ld(true,rd(true,X2)),X1)),X1),X1) = ld(X3,rd(X3,rd(ld(X1,mult(mult(X2,rd(X1,mult(X1,X1))),X1)),X1))),
inference(step,[status(thm)],[t221956,t2930]) ).
cnf(t221958,plain,
mult(X1,mult(ld(true,rd(true,X2)),X1)) = ld(X3,rd(X3,rd(ld(X1,mult(mult(X2,rd(X1,mult(X1,X1))),X1)),X1))),
inference(step,[status(thm)],[t221957,t8]) ).
cnf(t221959,plain,
mult(X1,mult(ld(true,rd(true,X2)),X1)) = ld(X3,rd(X3,rd(ld(X1,mult(rd(X2,X1),X1)),X1))),
inference(step,[status(thm)],[t221958,t1132]) ).
cnf(t221960,plain,
mult(X1,mult(ld(true,rd(true,X2)),X1)) = ld(X3,rd(X3,rd(ld(X1,X2),X1))),
inference(step,[status(thm)],[t221959,t8]) ).
cnf(t86067,plain,
ld(X1,rd(X1,rd(ld(X2,X3),X2))) = mult(X2,mult(ld(true,rd(true,X3)),X2)),
inference(orient,[status(thm)],[t221960]) ).
cnf(t86160,plain,
mult(X1,mult(ld(true,rd(true,rd(X2,mult(rd(X1,X1),X2)))),X1)) = ld(X3,rd(X3,rd(mult(ld(X1,rd(rd(X2,X2),X1)),X1),X1))),
inference(cp,[status(thm)],[t86067,t15264]) ).
cnf(t9233,plain,
ld(rd(X1,X1),rd(X2,X2)) = ld(X3,rd(X3,rd(X1,mult(rd(X2,X2),X1)))),
inference(cp,[status(thm)],[t224,t9192]) ).
cnf(t221856,plain,
rd(X2,mult(rd(X1,X1),X2)) = ld(X3,rd(X3,rd(X1,mult(rd(X2,X2),X1)))),
inference(step,[status(thm)],[t9233,t9192]) ).
cnf(t64930,plain,
ld(X1,rd(X1,rd(X2,mult(rd(X3,X3),X2)))) = rd(X3,mult(rd(X2,X2),X3)),
inference(orient,[status(thm)],[t221856]) ).
cnf(t222100,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)],[t86160,t64930]) ).
cnf(t222101,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)],[t222100,t9]) ).
cnf(t222102,plain,
mult(X1,mult(rd(X1,mult(rd(X2,X2),X1)),X1)) = ld(rd(rd(X2,X2),X1),X1),
inference(step,[status(thm)],[t222101,t224]) ).
cnf(t100732,plain,
mult(X1,mult(rd(X1,mult(rd(X2,X2),X1)),X1)) = ld(rd(rd(X2,X2),X1),X1),
inference(orient,[status(thm)],[t222102]) ).
cnf(t222865,plain,
ld(rd(rd(X2,X2),X1),X1) = mult(ld(X1,rd(X1,rd(rd(X2,X2),X1))),X1),
inference(step,[status(thm)],[t222864,t100732]) ).
cnf(t219192,plain,
mult(ld(X1,rd(X1,rd(rd(X2,X2),X1))),X1) = ld(rd(rd(X2,X2),X1),X1),
inference(orient,[status(thm)],[t222865]) ).
cnf(t9206,plain,
rd(X1,X1) = rd(rd(X2,X2),rd(X2,mult(rd(X1,X1),X2))),
inference(cp,[status(thm)],[t23,t9192]) ).
cnf(t9241,plain,
rd(rd(X1,X1),rd(X1,mult(rd(X2,X2),X1))) = rd(X2,X2),
inference(orient,[status(thm)],[t9206]) ).
cnf(t219250,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)],[t219192,t9241]) ).
cnf(t222866,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)],[t219250,t9241]) ).
cnf(t15309,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)],[t15264,t989]) ).
cnf(t221885,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)],[t15309,t617]) ).
cnf(t5024,plain,
rd(mult(rd(X1,X1),X2),rd(X1,X1)) = ld(rd(X1,X1),rd(X2,rd(X1,X1))),
inference(cp,[status(thm)],[t5016,t644]) ).
cnf(t14645,plain,
ld(rd(X1,X1),rd(X2,rd(X1,X1))) = rd(mult(rd(X1,X1),X2),rd(X1,X1)),
inference(orient,[status(thm)],[t5024]) ).
cnf(t221886,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)],[t221885,t14645]) ).
cnf(t221887,plain,
mult(rd(X1,X1),rd(X2,X2)) = ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))),
inference(step,[status(thm)],[t221886,t684]) ).
cnf(t221888,plain,
rd(rd(X1,X1),rd(X2,X2)) = ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))),
inference(step,[status(thm)],[t221887,t617]) ).
cnf(t68262,plain,
ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t221888]) ).
cnf(t222867,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)],[t222866,t68262]) ).
cnf(t9191,plain,
mult(X1,mult(rd(rd(X2,ld(X3,rd(X3,X1))),rd(X2,ld(X3,rd(X3,X1)))),X1)) = mult(mult(ld(X2,rd(rd(X2,ld(X3,rd(X3,X1))),ld(X3,rd(X3,X1)))),ld(X3,rd(X3,X1))),X1),
inference(cp,[status(thm)],[t3817,t9064]) ).
cnf(t221834,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)],[t9191,t215]) ).
cnf(t221835,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)],[t221834,t3101]) ).
cnf(t221836,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)],[t221835,t215]) ).
cnf(t221837,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)],[t221836,t196]) ).
cnf(t498,plain,
mult(mult(X1,ld(X2,rd(X3,Y3))),Y3) = mult(rd(X1,Y3),ld(rd(X2,Y3),X3)),
inference(cp,[status(thm)],[t25,t477]) ).
cnf(t221378,plain,
mult(rd(X1,ld(rd(X3,Y3),X2)),Y3) = mult(rd(X1,Y3),ld(rd(X2,Y3),X3)),
inference(step,[status(thm)],[t498,t196]) ).
cnf(t221379,plain,
mult(rd(X1,ld(rd(X3,Y3),X2)),Y3) = rd(rd(X1,Y3),ld(X3,rd(X2,Y3))),
inference(step,[status(thm)],[t221378,t196]) ).
cnf(t8438,plain,
mult(rd(X1,ld(rd(X2,X3),Y3)),X3) = rd(rd(X1,X3),ld(X2,rd(Y3,X3))),
inference(orient,[status(thm)],[t221379]) ).
cnf(t221838,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)],[t221837,t8438]) ).
cnf(t221839,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)],[t221838,t215]) ).
cnf(t221840,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)],[t221839,t8]) ).
cnf(t221841,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)],[t221840,t215]) ).
cnf(t221842,plain,
mult(X1,rd(X2,rd(ld(X1,mult(X2,X1)),X1))) = ld(X2,mult(mult(X2,X1),X1)),
inference(step,[status(thm)],[t221841,t215]) ).
cnf(t63649,plain,
mult(X1,rd(X2,rd(ld(X1,mult(X2,X1)),X1))) = ld(X2,mult(mult(X2,X1),X1)),
inference(orient,[status(thm)],[t221842]) ).
cnf(t63662,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)],[t63649,t215]) ).
cnf(t222001,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)],[t63662,t196]) ).
cnf(t222002,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)],[t222001,t196]) ).
cnf(t222003,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)],[t222002,t24]) ).
cnf(t222004,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)],[t222003,t24]) ).
cnf(t222005,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)],[t222004,t3817]) ).
cnf(t222006,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)],[t222005,t196]) ).
cnf(t222007,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)],[t222006,t8438]) ).
cnf(t222008,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)],[t222007,t215]) ).
cnf(t222009,plain,
ld(X1,rd(rd(X1,X3),X3)) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(X3,X1))),
inference(step,[status(thm)],[t222008,t8]) ).
cnf(t93652,plain,
mult(ld(X1,rd(X1,X2)),rd(X3,mult(X2,X3))) = ld(X3,rd(rd(X3,X2),X2)),
inference(orient,[status(thm)],[t222009]) ).
cnf(t222868,plain,
rd(rd(X2,X2),rd(X1,X1)) = ld(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2))),
inference(step,[status(thm)],[t222867,t93652]) ).
cnf(t222869,plain,
rd(rd(X2,X2),rd(X1,X1)) = ld(X1,X1),
inference(step,[status(thm)],[t222868,t684]) ).
cnf(t222870,plain,
rd(rd(X2,X2),rd(X1,X1)) = rd(X1,X1),
inference(step,[status(thm)],[t222869,t614]) ).
cnf(t219572,plain,
rd(rd(X1,X1),rd(X2,X2)) = rd(X2,X2),
inference(orient,[status(thm)],[t222870]) ).
cnf(t219785,plain,
mult(X1,mult(rd(X1,X1),rd(X2,X2))) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(cp,[status(thm)],[t81264,t219572]) ).
cnf(t222894,plain,
mult(X1,rd(rd(X1,X1),rd(X2,X2))) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(step,[status(thm)],[t219785,t617]) ).
cnf(t222895,plain,
mult(X1,rd(X2,X2)) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(step,[status(thm)],[t222894,t219572]) ).
cnf(t222896,plain,
rd(X1,rd(X2,X2)) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(step,[status(thm)],[t222895,t617]) ).
cnf(t222897,plain,
rd(X1,rd(X2,X2)) = X1,
inference(step,[status(thm)],[t222896,t9]) ).
cnf(t219880,plain,
rd(X1,rd(X2,X2)) = X1,
inference(orient,[status(thm)],[t222897]) ).
cnf(t0,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t11,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t513,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)],[t504,t215]) ).
cnf(t221643,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)],[t513,t196]) ).
cnf(t221644,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)],[t221643,t215]) ).
cnf(t221645,plain,
rd(ld(X1,mult(X2,Y3)),Y3) = ld(ld(X3,rd(X3,Y3)),ld(mult(X1,Y3),X2)),
inference(step,[status(thm)],[t221644,t24]) ).
cnf(t39033,plain,
ld(ld(X1,rd(X1,X2)),ld(mult(X3,X2),Y3)) = rd(ld(X3,mult(Y3,X2)),X2),
inference(orient,[status(thm)],[t221645]) ).
cnf(t222283,plain,
ld(X1,mult(ld(X1,rd(mult(X1,X2),X1)),X1)) = rd(ld(X1,mult(X2,X1)),X1),
inference(step,[status(thm)],[t116934,t128402]) ).
cnf(t128656,plain,
ld(X1,mult(ld(X1,rd(mult(X1,X2),X1)),X1)) = rd(ld(X1,mult(X2,X1)),X1),
inference(rw,[status(thm)],[t222283]) ).
cnf(t3973,plain,
rd(ld(X1,mult(X2,X1)),X1) = mult(ld(X3,rd(X3,X1)),X2),
inference(cp,[status(thm)],[t3965,t1332]) ).
cnf(t32858,plain,
rd(ld(X1,mult(X2,X1)),X1) = mult(ld(X3,rd(X3,X1)),X2),
inference(orient,[status(thm)],[t3973]) ).
cnf(t90558,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)],[t32858,t90217]) ).
cnf(t521,plain,
rd(X1,ld(ld(rd(X2,X3),Y3),X3)) = mult(X1,mult(ld(X2,rd(Y3,X3)),X3)),
inference(cp,[status(thm)],[t196,t504]) ).
cnf(t8697,plain,
mult(X1,mult(ld(X2,rd(X3,Y3)),Y3)) = rd(X1,ld(ld(rd(X2,Y3),X3),Y3)),
inference(orient,[status(thm)],[t521]) ).
cnf(t222108,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)],[t90558,t8697]) ).
cnf(t1059,plain,
mult(ld(X1,rd(X1,X2)),ld(X1,rd(X1,X2))) = ld(ld(X3,mult(X3,X2)),ld(X1,rd(X1,X2))),
inference(cp,[status(thm)],[t1053,t215]) ).
cnf(t221233,plain,
rd(ld(X1,rd(X1,X2)),ld(rd(X1,X2),X1)) = ld(ld(X3,mult(X3,X2)),ld(X1,rd(X1,X2))),
inference(step,[status(thm)],[t1059,t196]) ).
cnf(t221234,plain,
rd(ld(X1,rd(X1,X2)),X2) = ld(ld(X3,mult(X3,X2)),ld(X1,rd(X1,X2))),
inference(step,[status(thm)],[t221233,t24]) ).
cnf(t221235,plain,
rd(ld(X1,rd(X1,X2)),X2) = ld(X2,ld(X1,rd(X1,X2))),
inference(step,[status(thm)],[t221234,t12]) ).
cnf(t1253,plain,
ld(X1,ld(X2,rd(X2,X1))) = rd(ld(X2,rd(X2,X1)),X1),
inference(orient,[status(thm)],[t221235]) ).
cnf(t4169,plain,
rd(ld(X1,rd(X1,X2)),X2) = rd(X3,mult(X2,mult(X2,X3))),
inference(cp,[status(thm)],[t23,t4111]) ).
cnf(t33309,plain,
rd(ld(X1,rd(X1,X2)),X2) = rd(X3,mult(X2,mult(X2,X3))),
inference(orient,[status(thm)],[t4169]) ).
cnf(t221613,plain,
ld(X1,ld(X2,rd(X2,X1))) = rd(true,mult(X1,mult(X1,true))),
inference(step,[status(thm)],[t1253,t33309]) ).
cnf(t33310,plain,
ld(X1,ld(X2,rd(X2,X1))) = rd(true,mult(X1,mult(X1,true))),
inference(orient,[status(thm)],[t221613]) ).
cnf(t4387,plain,
rd(ld(X1,mult(rd(X1,X1),X2)),X1) = ld(X1,rd(ld(rd(X1,X1),X2),X1)),
inference(cp,[status(thm)],[t3755,t4356]) ).
cnf(t14170,plain,
ld(X1,rd(ld(rd(X1,X1),X2),X1)) = rd(ld(X1,mult(rd(X1,X1),X2)),X1),
inference(orient,[status(thm)],[t4387]) ).
cnf(t33467,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)],[t14170,t33309]) ).
cnf(t221615,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)],[t33467,t1088]) ).
cnf(t221616,plain,
rd(ld(X1,rd(rd(X1,X1),X1)),X1) = ld(X1,rd(X2,mult(X1,mult(X1,X2)))),
inference(step,[status(thm)],[t221615,t1132]) ).
cnf(t221617,plain,
rd(ld(X1,rd(X1,mult(X1,X1))),X1) = ld(X1,rd(X2,mult(X1,mult(X1,X2)))),
inference(step,[status(thm)],[t221616,t1088]) ).
cnf(t1573,plain,
rd(mult(X1,X2),mult(X2,mult(X3,X2))) = rd(rd(X1,X3),X2),
inference(cp,[status(thm)],[t1548,t9]) ).
cnf(t2425,plain,
rd(mult(X1,X2),mult(X2,mult(X3,X2))) = rd(rd(X1,X3),X2),
inference(orient,[status(thm)],[t1573]) ).
cnf(t2465,plain,
rd(rd(X1,rd(X2,X3)),X3) = rd(mult(X1,X3),mult(X3,X2)),
inference(cp,[status(thm)],[t2425,t8]) ).
cnf(t2493,plain,
rd(rd(X1,rd(X2,X3)),X3) = rd(mult(X1,X3),mult(X3,X2)),
inference(orient,[status(thm)],[t2465]) ).
cnf(t2949,plain,
rd(X1,mult(X1,X1)) = rd(X2,rd(mult(X1,mult(X2,X1)),X1)),
inference(cp,[status(thm)],[t23,t2930]) ).
cnf(t3170,plain,
rd(X1,rd(mult(X2,mult(X1,X2)),X2)) = rd(X2,mult(X2,X2)),
inference(orient,[status(thm)],[t2949]) ).
cnf(t3195,plain,
rd(X1,mult(X1,X1)) = rd(rd(X2,X1),rd(mult(X1,X2),X1)),
inference(cp,[status(thm)],[t3170,t8]) ).
cnf(t3388,plain,
rd(rd(X1,X2),rd(mult(X2,X1),X2)) = rd(X2,mult(X2,X2)),
inference(orient,[status(thm)],[t3195]) ).
cnf(t3448,plain,
rd(mult(rd(X1,X2),X2),mult(X2,mult(X2,X1))) = rd(rd(X2,mult(X2,X2)),X2),
inference(cp,[status(thm)],[t2493,t3388]) ).
cnf(t221609,plain,
rd(X1,mult(X2,mult(X2,X1))) = rd(rd(X2,mult(X2,X2)),X2),
inference(step,[status(thm)],[t3448,t8]) ).
cnf(t221610,plain,
rd(X1,mult(X2,mult(X2,X1))) = rd(rd(X2,X2),mult(X2,X2)),
inference(step,[status(thm)],[t221609,t2378]) ).
cnf(t221611,plain,
rd(X1,mult(X2,mult(X2,X1))) = rd(X2,mult(X2,mult(X2,X2))),
inference(step,[status(thm)],[t221610,t1605]) ).
cnf(t32404,plain,
rd(X1,mult(X2,mult(X2,X1))) = rd(X2,mult(X2,mult(X2,X2))),
inference(orient,[status(thm)],[t221611]) ).
cnf(t32590,plain,
ld(X1,rd(X1,mult(X2,mult(X2,X2)))) = ld(X2,rd(X3,mult(X2,mult(X2,X3)))),
inference(cp,[status(thm)],[t389,t32404]) ).
cnf(t23560,plain,
mult(rd(X1,mult(rd(X2,X1),X2)),X2) = ld(rd(X2,X1),X1),
inference(cp,[status(thm)],[t23506,t24]) ).
cnf(t24078,plain,
mult(rd(X1,mult(rd(X2,X1),X2)),X2) = ld(rd(X2,X1),X1),
inference(orient,[status(thm)],[t23560]) ).
cnf(t24181,plain,
rd(X1,mult(rd(X2,X1),X2)) = rd(ld(rd(X2,X1),X1),X2),
inference(cp,[status(thm)],[t9,t24078]) ).
cnf(t24257,plain,
rd(ld(rd(X1,X2),X2),X1) = rd(X2,mult(rd(X1,X2),X1)),
inference(orient,[status(thm)],[t24181]) ).
cnf(t24302,plain,
rd(X1,mult(rd(mult(X2,X1),X1),mult(X2,X1))) = rd(ld(X2,X1),mult(X2,X1)),
inference(cp,[status(thm)],[t24257,t9]) ).
cnf(t221536,plain,
rd(X1,mult(X2,mult(X2,X1))) = rd(ld(X2,X1),mult(X2,X1)),
inference(step,[status(thm)],[t24302,t9]) ).
cnf(t24641,plain,
rd(ld(X1,X2),mult(X1,X2)) = rd(X2,mult(X1,mult(X1,X2))),
inference(orient,[status(thm)],[t221536]) ).
cnf(t24778,plain,
mult(X1,X2) = ld(rd(X2,mult(X1,mult(X1,X2))),ld(X1,X2)),
inference(cp,[status(thm)],[t24,t24641]) ).
cnf(t24862,plain,
ld(rd(X1,mult(X2,mult(X2,X1))),ld(X2,X1)) = mult(X2,X1),
inference(orient,[status(thm)],[t24778]) ).
cnf(t1581,plain,
X1 = ld(rd(X2,mult(X1,mult(X3,X1))),rd(rd(X2,X1),X3)),
inference(cp,[status(thm)],[t24,t1548]) ).
cnf(t17767,plain,
ld(rd(X1,mult(X2,mult(X3,X2))),rd(rd(X1,X2),X3)) = X2,
inference(orient,[status(thm)],[t1581]) ).
cnf(t17864,plain,
X1 = ld(rd(X2,mult(X1,mult(rd(mult(X1,X2),X1),X1))),rd(X1,mult(X1,X1))),
inference(cp,[status(thm)],[t17767,t3388]) ).
cnf(t221545,plain,
X1 = ld(rd(X2,mult(X1,mult(X1,X2))),rd(X1,mult(X1,X1))),
inference(step,[status(thm)],[t17864,t8]) ).
cnf(t26225,plain,
ld(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))) = X2,
inference(orient,[status(thm)],[t221545]) ).
cnf(t26351,plain,
mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))) = ld(rd(rd(X2,mult(X2,X2)),mult(rd(X1,mult(X2,mult(X2,X1))),mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))))),X2),
inference(cp,[status(thm)],[t24862,t26225]) ).
cnf(t221561,plain,
ld(X2,ld(X2,rd(X2,mult(X2,X2)))) = ld(rd(rd(X2,mult(X2,X2)),mult(rd(X1,mult(X2,mult(X2,X1))),mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))))),X2),
inference(step,[status(thm)],[t26351,t21683]) ).
cnf(t20981,plain,
ld(X1,ld(X1,rd(X2,mult(X1,X1)))) = rd(ld(mult(X1,X1),X2),mult(X1,X1)),
inference(cp,[status(thm)],[t20979,t4017]) ).
cnf(t22667,plain,
ld(X1,ld(X1,rd(X2,mult(X1,X1)))) = rd(ld(mult(X1,X1),X2),mult(X1,X1)),
inference(orient,[status(thm)],[t20981]) ).
cnf(t221562,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)],[t221561,t22667]) ).
cnf(t221563,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(rd(rd(X2,mult(X2,X2)),mult(rd(X1,mult(X2,mult(X2,X1))),mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))))),X2),
inference(step,[status(thm)],[t221562,t348]) ).
cnf(t221564,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(rd(rd(X2,mult(X2,X2)),ld(X2,ld(X2,mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2)))))),X2),
inference(step,[status(thm)],[t221563,t21683]) ).
cnf(t221565,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(rd(rd(X2,mult(X2,X2)),ld(X2,ld(X2,ld(X2,ld(X2,rd(X2,mult(X2,X2))))))),X2),
inference(step,[status(thm)],[t221564,t21683]) ).
cnf(t221566,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(rd(rd(X2,mult(X2,X2)),ld(X2,ld(X2,rd(ld(mult(X2,X2),X2),mult(X2,X2))))),X2),
inference(step,[status(thm)],[t221565,t22667]) ).
cnf(t221567,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(rd(rd(X2,mult(X2,X2)),rd(ld(mult(X2,X2),ld(mult(X2,X2),X2)),mult(X2,X2))),X2),
inference(step,[status(thm)],[t221566,t22667]) ).
cnf(t221568,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(mult(rd(X2,ld(mult(X2,X2),X2)),mult(X2,X2)),X2),
inference(step,[status(thm)],[t221567,t3289]) ).
cnf(t221569,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(mult(mult(X2,X2),mult(X2,X2)),X2),
inference(step,[status(thm)],[t221568,t23]) ).
cnf(t1054,plain,
mult(ld(X1,X2),ld(X1,X2)) = ld(ld(X2,X1),ld(X1,X2)),
inference(cp,[status(thm)],[t1053,t224]) ).
cnf(t221232,plain,
rd(ld(X1,X2),ld(X2,X1)) = ld(ld(X2,X1),ld(X1,X2)),
inference(step,[status(thm)],[t1054,t196]) ).
cnf(t1218,plain,
ld(ld(X1,X2),ld(X2,X1)) = rd(ld(X2,X1),ld(X1,X2)),
inference(orient,[status(thm)],[t221232]) ).
cnf(t1279,plain,
rd(ld(rd(X1,mult(X1,X1)),X1),ld(X1,rd(X1,mult(X1,X1)))) = ld(rd(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),X1)),
inference(cp,[status(thm)],[t1218,t1274]) ).
cnf(t221238,plain,
mult(ld(rd(X1,mult(X1,X1)),X1),mult(X1,X1)) = ld(rd(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),X1)),
inference(step,[status(thm)],[t1279,t215]) ).
cnf(t221239,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)],[t221238,t24]) ).
cnf(t221240,plain,
mult(mult(X1,X1),mult(X1,X1)) = ld(rd(rd(X1,mult(X1,X1)),X1),mult(X1,X1)),
inference(step,[status(thm)],[t221239,t24]) ).
cnf(t221241,plain,
mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(ld(rd(X1,mult(X1,X1)),X1),X1)),
inference(step,[status(thm)],[t221240,t83]) ).
cnf(t221242,plain,
mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(mult(X1,X1),X1)),
inference(step,[status(thm)],[t221241,t24]) ).
cnf(t221243,plain,
mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(X1,mult(X1,X1))),
inference(step,[status(thm)],[t221242,t865]) ).
cnf(t1293,plain,
mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(X1,mult(X1,X1))),
inference(orient,[status(thm)],[t221243]) ).
cnf(t221570,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(mult(X2,mult(X2,mult(X2,X2))),X2),
inference(step,[status(thm)],[t221569,t1293]) ).
cnf(t221571,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(true,rd(true,mult(X2,mult(X2,X2)))),
inference(step,[status(thm)],[t221570,t348]) ).
cnf(t26899,plain,
ld(true,rd(true,mult(X1,mult(X1,X1)))) = rd(ld(true,rd(true,X1)),mult(X1,X1)),
inference(orient,[status(thm)],[t221571]) ).
cnf(t26901,plain,
rd(ld(true,rd(true,X1)),mult(X1,X1)) = ld(X2,rd(X2,mult(X1,mult(X1,X1)))),
inference(cp,[status(thm)],[t26899,t389]) ).
cnf(t28094,plain,
ld(X1,rd(X1,mult(X2,mult(X2,X2)))) = rd(ld(true,rd(true,X2)),mult(X2,X2)),
inference(orient,[status(thm)],[t26901]) ).
cnf(t221612,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(X2,rd(X3,mult(X2,mult(X2,X3)))),
inference(step,[status(thm)],[t32590,t28094]) ).
cnf(t32685,plain,
ld(X1,rd(X2,mult(X1,mult(X1,X2)))) = rd(ld(true,rd(true,X1)),mult(X1,X1)),
inference(orient,[status(thm)],[t221612]) ).
cnf(t221618,plain,
rd(ld(X1,rd(X1,mult(X1,X1))),X1) = rd(ld(true,rd(true,X1)),mult(X1,X1)),
inference(step,[status(thm)],[t221617,t32685]) ).
cnf(t33675,plain,
rd(ld(X1,rd(X1,mult(X1,X1))),X1) = rd(ld(true,rd(true,X1)),mult(X1,X1)),
inference(orient,[status(thm)],[t221618]) ).
cnf(t33769,plain,
rd(true,mult(X1,mult(X1,true))) = ld(X1,ld(ld(X1,rd(X1,mult(X1,X1))),rd(ld(true,rd(true,X1)),mult(X1,X1)))),
inference(cp,[status(thm)],[t33310,t33675]) ).
cnf(t221619,plain,
rd(true,mult(X1,mult(X1,true))) = ld(X1,rd(mult(mult(X1,X1),ld(true,rd(true,X1))),mult(X1,X1))),
inference(step,[status(thm)],[t33769,t5016]) ).
cnf(t221620,plain,
rd(true,mult(X1,mult(X1,true))) = ld(X1,rd(rd(mult(X1,X1),ld(rd(true,X1),true)),mult(X1,X1))),
inference(step,[status(thm)],[t221619,t196]) ).
cnf(t221621,plain,
rd(true,mult(X1,mult(X1,true))) = ld(X1,rd(rd(mult(X1,X1),X1),mult(X1,X1))),
inference(step,[status(thm)],[t221620,t24]) ).
cnf(t221622,plain,
rd(true,mult(X1,mult(X1,true))) = ld(X1,rd(X1,mult(X1,X1))),
inference(step,[status(thm)],[t221621,t9]) ).
cnf(t33807,plain,
ld(X1,rd(X1,mult(X1,X1))) = rd(true,mult(X1,mult(X1,true))),
inference(orient,[status(thm)],[t221622]) ).
cnf(t33812,plain,
rd(true,mult(X1,mult(X1,true))) = ld(X2,rd(X2,mult(X1,X1))),
inference(cp,[status(thm)],[t33807,t389]) ).
cnf(t33893,plain,
ld(X1,rd(X1,mult(X2,X2))) = rd(true,mult(X2,mult(X2,true))),
inference(orient,[status(thm)],[t33812]) ).
cnf(t222109,plain,
rd(rd(true,mult(X2,mult(X2,true))),ld(ld(rd(X2,X2),X3),X2)) = rd(ld(mult(X2,X2),ld(X2,mult(X3,mult(X2,X2)))),mult(X2,X2)),
inference(step,[status(thm)],[t222108,t33893]) ).
cnf(t21708,plain,
ld(X1,ld(X1,ld(X2,X3))) = rd(rd(Y3,mult(X1,mult(X1,Y3))),ld(X3,X2)),
inference(cp,[status(thm)],[t21683,t196]) ).
cnf(t70826,plain,
rd(rd(X1,mult(X2,mult(X2,X1))),ld(X3,Y3)) = ld(X2,ld(X2,ld(Y3,X3))),
inference(orient,[status(thm)],[t21708]) ).
cnf(t222110,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)],[t222109,t70826]) ).
cnf(t222111,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)],[t222110,t504]) ).
cnf(t222112,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)],[t222111,t456]) ).
cnf(t222113,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)],[t222112,t456]) ).
cnf(t222114,plain,
mult(ld(mult(X2,X2),ld(X2,rd(X3,X2))),X2) = ld(mult(X2,mult(X2,X2)),X3),
inference(step,[status(thm)],[t222113,t9]) ).
cnf(t103284,plain,
mult(ld(mult(X1,X1),ld(X1,rd(X2,X1))),X1) = ld(mult(X1,mult(X1,X1)),X2),
inference(orient,[status(thm)],[t222114]) ).
cnf(t103497,plain,
ld(mult(X1,mult(X1,X1)),mult(X2,X1)) = mult(ld(mult(X1,X1),ld(X1,X2)),X1),
inference(cp,[status(thm)],[t103284,t9]) ).
cnf(t103689,plain,
ld(mult(X1,mult(X1,X1)),mult(X2,X1)) = mult(ld(mult(X1,X1),ld(X1,X2)),X1),
inference(orient,[status(thm)],[t103497]) ).
cnf(t103920,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)],[t224,t103689]) ).
cnf(t475,plain,
ld(ld(X1,mult(X2,X3)),X3) = ld(Y3,rd(Y3,mult(ld(mult(X1,X3),X2),X3))),
inference(cp,[status(thm)],[t224,t456]) ).
cnf(t38443,plain,
ld(X1,rd(X1,mult(ld(mult(X2,X3),Y3),X3))) = ld(ld(X2,mult(Y3,X3)),X3),
inference(orient,[status(thm)],[t475]) ).
cnf(t222115,plain,
ld(mult(X1,X2),mult(X2,mult(X2,X2))) = ld(ld(X2,mult(ld(X2,X1),X2)),X2),
inference(step,[status(thm)],[t103920,t38443]) ).
cnf(t104352,plain,
ld(ld(X1,mult(ld(X1,X2),X1)),X1) = ld(mult(X2,X1),mult(X1,mult(X1,X1))),
inference(orient,[status(thm)],[t222115]) ).
cnf(t104539,plain,
ld(X1,mult(ld(X1,X2),X1)) = rd(X1,ld(mult(X2,X1),mult(X1,mult(X1,X1)))),
inference(cp,[status(thm)],[t23,t104352]) ).
cnf(t130245,plain,
rd(X1,ld(mult(X2,X1),mult(X1,mult(X1,X1)))) = ld(X1,mult(ld(X1,X2),X1)),
inference(orient,[status(thm)],[t104539]) ).
cnf(t130373,plain,
ld(X1,mult(ld(X1,rd(X2,X1)),X1)) = rd(X1,ld(X2,mult(X1,mult(X1,X1)))),
inference(cp,[status(thm)],[t130245,t8]) ).
cnf(t130616,plain,
ld(X1,mult(ld(X1,rd(X2,X1)),X1)) = rd(X1,ld(X2,mult(X1,mult(X1,X1)))),
inference(orient,[status(thm)],[t130373]) ).
cnf(t222459,plain,
rd(X1,ld(mult(X1,X2),mult(X1,mult(X1,X1)))) = rd(ld(X1,mult(X2,X1)),X1),
inference(step,[status(thm)],[t128656,t130616]) ).
cnf(t154017,plain,
rd(X1,ld(mult(X1,X2),mult(X1,mult(X1,X1)))) = rd(ld(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t222459]) ).
cnf(t154296,plain,
ld(mult(X1,mult(X1,X1)),mult(X1,X2)) = ld(X1,rd(ld(X1,mult(X2,X1)),X1)),
inference(cp,[status(thm)],[t224,t154017]) ).
cnf(t154727,plain,
ld(mult(X1,mult(X1,X1)),mult(X1,X2)) = ld(X1,rd(ld(X1,mult(X2,X1)),X1)),
inference(orient,[status(thm)],[t154296]) ).
cnf(t154938,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)],[t39033,t154727]) ).
cnf(t67,plain,
mult(X1,X2) = rd(rd(mult(X1,mult(X2,X3)),X2),rd(X3,X2)),
inference(cp,[status(thm)],[t9,t56]) ).
cnf(t2770,plain,
rd(rd(mult(X1,mult(X2,X3)),X2),rd(X3,X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t67]) ).
cnf(t55173,plain,
mult(ld(X1,rd(X2,X1)),X1) = rd(rd(rd(ld(X1,mult(X2,mult(X1,X1))),X1),X1),rd(X1,X1)),
inference(cp,[status(thm)],[t2770,t54945]) ).
cnf(t221984,plain,
mult(ld(X1,rd(X2,X1)),X1) = rd(ld(X1,mult(X2,mult(X1,X1))),mult(X1,X1)),
inference(step,[status(thm)],[t55173,t2329]) ).
cnf(t90562,plain,
rd(ld(X1,mult(X2,mult(X1,X1))),mult(X1,X1)) = mult(ld(X1,rd(X2,X1)),X1),
inference(orient,[status(thm)],[t221984]) ).
cnf(t222478,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)],[t154938,t90562]) ).
cnf(t222479,plain,
mult(ld(X1,rd(mult(X1,X2),X1)),X1) = ld(rd(true,mult(X1,mult(X1,true))),ld(X1,rd(ld(X1,mult(X2,X1)),X1))),
inference(step,[status(thm)],[t222478,t33893]) ).
cnf(t222480,plain,
mult(ld(X1,rd(mult(X1,X2),X1)),X1) = mult(X1,rd(ld(X1,mult(X2,X1)),X1)),
inference(step,[status(thm)],[t222479,t29396]) ).
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(t221398,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(t221399,plain,
rd(mult(X1,X2),ld(X1,X3)) = mult(X3,mult(ld(X3,X1),rd(X2,ld(X1,X3)))),
inference(step,[status(thm)],[t221398,t196]) ).
cnf(t10455,plain,
mult(X1,mult(ld(X1,X2),rd(X3,ld(X2,X1)))) = rd(mult(X2,X3),ld(X2,X1)),
inference(orient,[status(thm)],[t221399]) ).
cnf(t10505,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)],[t10455,t1332]) ).
cnf(t221400,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)],[t10505,t24]) ).
cnf(t221401,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)],[t221400,t3965]) ).
cnf(t221402,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)],[t221401,t8438]) ).
cnf(t221403,plain,
rd(mult(rd(X1,X2),X3),X2) = mult(X1,rd(ld(X2,mult(rd(X3,X2),X2)),X2)),
inference(step,[status(thm)],[t221402,t215]) ).
cnf(t221404,plain,
rd(mult(rd(X1,X2),X3),X2) = mult(X1,rd(ld(X2,X3),X2)),
inference(step,[status(thm)],[t221403,t8]) ).
cnf(t10628,plain,
mult(X1,rd(ld(X2,X3),X2)) = rd(mult(rd(X1,X2),X3),X2),
inference(orient,[status(thm)],[t221404]) ).
cnf(t222481,plain,
mult(ld(X1,rd(mult(X1,X2),X1)),X1) = rd(mult(rd(X1,X1),mult(X2,X1)),X1),
inference(step,[status(thm)],[t222480,t10628]) ).
cnf(t155724,plain,
mult(ld(X1,rd(mult(X1,X2),X1)),X1) = rd(mult(rd(X1,X1),mult(X2,X1)),X1),
inference(orient,[status(thm)],[t222481]) ).
cnf(t155928,plain,
ld(X1,rd(mult(X1,X2),X1)) = rd(rd(mult(rd(X1,X1),mult(X2,X1)),X1),X1),
inference(cp,[status(thm)],[t9,t155724]) ).
cnf(t187118,plain,
rd(rd(mult(rd(X1,X1),mult(X2,X1)),X1),X1) = ld(X1,rd(mult(X1,X2),X1)),
inference(orient,[status(thm)],[t155928]) ).
cnf(t219913,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)],[t219880,t187118]) ).
cnf(t223071,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)],[t219913,t219880]) ).
cnf(t223072,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)],[t223071,t219572]) ).
cnf(t222898,plain,
mult(X1,rd(X2,X2)) = X1,
inference(step,[status(thm)],[t617,t219880]) ).
cnf(t219881,plain,
mult(X1,rd(X2,X2)) = X1,
inference(orient,[status(thm)],[t222898]) ).
cnf(t223073,plain,
mult(rd(X1,X1),X2) = ld(rd(X1,X1),rd(mult(rd(X1,X1),X2),rd(X1,X1))),
inference(step,[status(thm)],[t223072,t219881]) ).
cnf(t223074,plain,
mult(rd(X1,X1),X2) = rd(mult(rd(X1,X1),mult(rd(X1,X1),X2)),rd(X1,X1)),
inference(step,[status(thm)],[t223073,t14645]) ).
cnf(t223075,plain,
mult(rd(X1,X1),X2) = mult(rd(X1,X1),mult(rd(X1,X1),X2)),
inference(step,[status(thm)],[t223074,t219880]) ).
cnf(t223076,plain,
mult(rd(X1,X1),X2) = ld(rd(X1,X1),X2),
inference(step,[status(thm)],[t223075,t4356]) ).
cnf(t106663,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)],[t504,t106491]) ).
cnf(t222298,plain,
ld(X1,rd(mult(X1,mult(X2,X1)),X1)) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
inference(step,[status(thm)],[t9966,t129466]) ).
cnf(t129467,plain,
ld(X1,rd(mult(X1,mult(X2,X1)),X1)) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
inference(orient,[status(thm)],[t222298]) ).
cnf(t222336,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)],[t106663,t129467]) ).
cnf(t118511,plain,
mult(rd(X1,X1),X2) = rd(X1,ld(mult(X1,X2),mult(X1,X1))),
inference(cp,[status(thm)],[t23,t118441]) ).
cnf(t119423,plain,
rd(X1,ld(mult(X1,X2),mult(X1,X1))) = mult(rd(X1,X1),X2),
inference(orient,[status(thm)],[t118511]) ).
cnf(t222337,plain,
mult(ld(X1,rd(mult(mult(X1,X1),X2),X1)),X1) = mult(X1,mult(rd(X1,X1),X2)),
inference(step,[status(thm)],[t222336,t119423]) ).
cnf(t134297,plain,
mult(ld(X1,rd(mult(mult(X1,X1),X2),X1)),X1) = mult(X1,mult(rd(X1,X1),X2)),
inference(orient,[status(thm)],[t222337]) ).
cnf(t134445,plain,
ld(X1,rd(mult(mult(X1,X1),X2),X1)) = rd(mult(X1,mult(rd(X1,X1),X2)),X1),
inference(cp,[status(thm)],[t9,t134297]) ).
cnf(t134622,plain,
ld(X1,rd(mult(mult(X1,X1),X2),X1)) = rd(mult(X1,mult(rd(X1,X1),X2)),X1),
inference(orient,[status(thm)],[t134445]) ).
cnf(t134634,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)],[t134622,t44]) ).
cnf(t222338,plain,
rd(mult(X1,mult(mult(X1,X2),X1)),X1) = ld(X1,mult(mult(mult(X1,X1),X1),X2)),
inference(step,[status(thm)],[t134634,t25]) ).
cnf(t222339,plain,
rd(mult(X1,mult(mult(X1,X2),X1)),X1) = ld(X1,mult(mult(X1,mult(X1,X1)),X2)),
inference(step,[status(thm)],[t222338,t865]) ).
cnf(t134910,plain,
ld(X1,mult(mult(X1,mult(X1,X1)),X2)) = rd(mult(X1,mult(mult(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t222339]) ).
cnf(t134924,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)],[t134910,t36652]) ).
cnf(t222341,plain,
rd(mult(X1,mult(mult(X1,mult(rd(true,mult(X1,mult(X1,true))),X3)),X1)),X1) = ld(X1,rd(mult(X1,mult(X3,mult(X1,X1))),mult(X1,X1))),
inference(step,[status(thm)],[t134924,t33893]) ).
cnf(t222342,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)],[t222341,t21683]) ).
cnf(t222343,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)],[t222342,t196]) ).
cnf(t222344,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)],[t222343,t23]) ).
cnf(t54675,plain,
mult(mult(X1,rd(X2,X1)),X1) = rd(rd(rd(mult(X1,mult(X2,mult(X1,X1))),X1),X1),rd(X1,X1)),
inference(cp,[status(thm)],[t2770,t54460]) ).
cnf(t221981,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)],[t54675,t34]) ).
cnf(t221982,plain,
mult(rd(X1,X1),mult(X1,X2)) = rd(mult(X1,mult(X2,mult(X1,X1))),mult(X1,X1)),
inference(step,[status(thm)],[t221981,t2329]) ).
cnf(t89915,plain,
rd(mult(X1,mult(X2,mult(X1,X1))),mult(X1,X1)) = mult(rd(X1,X1),mult(X1,X2)),
inference(orient,[status(thm)],[t221982]) ).
cnf(t222345,plain,
rd(mult(X1,mult(ld(X1,X3),X1)),X1) = ld(X1,mult(rd(X1,X1),mult(X1,X3))),
inference(step,[status(thm)],[t222344,t89915]) ).
cnf(t135473,plain,
ld(X1,mult(rd(X1,X1),mult(X1,X2))) = rd(mult(X1,mult(ld(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t222345]) ).
cnf(t135481,plain,
rd(mult(X1,mult(ld(X1,mult(X2,X1)),X1)),X1) = ld(X1,mult(mult(X1,X2),X1)),
inference(cp,[status(thm)],[t135473,t25]) ).
cnf(t165209,plain,
rd(mult(X1,mult(ld(X1,mult(X2,X1)),X1)),X1) = ld(X1,mult(mult(X1,X2),X1)),
inference(orient,[status(thm)],[t135481]) ).
cnf(t165569,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)],[t119033,t165209]) ).
cnf(t471,plain,
rd(X1,ld(ld(X2,mult(X3,Y3)),Y3)) = mult(X1,mult(ld(mult(X2,Y3),X3),Y3)),
inference(cp,[status(thm)],[t196,t456]) ).
cnf(t8237,plain,
mult(X1,mult(ld(mult(X2,X3),Y3),X3)) = rd(X1,ld(ld(X2,mult(Y3,X3)),X3)),
inference(orient,[status(thm)],[t471]) ).
cnf(t222741,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)],[t165569,t8237]) ).
cnf(t222742,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)],[t222741,t23]) ).
cnf(t222743,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)],[t222742,t456]) ).
cnf(t4130,plain,
mult(X1,mult(X1,X2)) = ld(rd(rd(X1,mult(X1,X1)),X1),X2),
inference(cp,[status(thm)],[t4111,t1332]) ).
cnf(t221342,plain,
mult(X1,mult(X1,X2)) = ld(rd(rd(X1,X1),mult(X1,X1)),X2),
inference(step,[status(thm)],[t4130,t2378]) ).
cnf(t221343,plain,
mult(X1,mult(X1,X2)) = ld(rd(X1,mult(X1,mult(X1,X1))),X2),
inference(step,[status(thm)],[t221342,t1605]) ).
cnf(t4400,plain,
ld(rd(X1,mult(X1,mult(X1,X1))),X2) = mult(X1,mult(X1,X2)),
inference(orient,[status(thm)],[t221343]) ).
cnf(t4413,plain,
mult(X1,mult(X1,X2)) = ld(ld(true,rd(true,mult(X1,X1))),X2),
inference(cp,[status(thm)],[t4400,t3051]) ).
cnf(t4745,plain,
ld(ld(true,rd(true,mult(X1,X1))),X2) = mult(X1,mult(X1,X2)),
inference(orient,[status(thm)],[t4413]) ).
cnf(t4756,plain,
mult(X1,mult(X1,X2)) = ld(ld(X3,rd(X3,mult(X1,X1))),X2),
inference(cp,[status(thm)],[t4745,t389]) ).
cnf(t4943,plain,
ld(ld(X1,rd(X1,mult(X2,X2))),X3) = mult(X2,mult(X2,X3)),
inference(orient,[status(thm)],[t4756]) ).
cnf(t5011,plain,
mult(mult(X1,X1),mult(X2,mult(X1,X1))) = mult(mult(X1,mult(X1,X2)),mult(X1,X1)),
inference(cp,[status(thm)],[t3817,t4943]) ).
cnf(t14257,plain,
mult(mult(X1,mult(X1,X2)),mult(X1,X1)) = mult(mult(X1,X1),mult(X2,mult(X1,X1))),
inference(orient,[status(thm)],[t5011]) ).
cnf(t89948,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)],[t89915,t14257]) ).
cnf(t222105,plain,
mult(rd(X1,X1),mult(X1,mult(X1,mult(X1,X2)))) = mult(mult(X1,mult(X1,X1)),X2),
inference(step,[status(thm)],[t89948,t44]) ).
cnf(t101525,plain,
mult(rd(X1,X1),mult(X1,mult(X1,mult(X1,X2)))) = mult(mult(X1,mult(X1,X1)),X2),
inference(orient,[status(thm)],[t222105]) ).
cnf(t101742,plain,
mult(X1,rd(mult(X1,mult(X1,X2)),X1)) = rd(mult(mult(X1,mult(X1,X1)),X2),X1),
inference(cp,[status(thm)],[t398,t101525]) ).
cnf(t102116,plain,
mult(X1,rd(mult(X1,mult(X1,X2)),X1)) = rd(mult(mult(X1,mult(X1,X1)),X2),X1),
inference(orient,[status(thm)],[t101742]) ).
cnf(t102275,plain,
rd(mult(X1,mult(X1,X2)),X1) = ld(X1,rd(mult(mult(X1,mult(X1,X1)),X2),X1)),
inference(cp,[status(thm)],[t12,t102116]) ).
cnf(t114891,plain,
ld(X1,rd(mult(mult(X1,mult(X1,X1)),X2),X1)) = rd(mult(X1,mult(X1,X2)),X1),
inference(orient,[status(thm)],[t102275]) ).
cnf(t114904,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)],[t114891,t44]) ).
cnf(t222407,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)],[t114904,t1772]) ).
cnf(t222408,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)],[t222407,t1293]) ).
cnf(t20179,plain,
ld(ld(X1,X2),ld(ld(X1,X2),X3)) = mult(rd(ld(X2,X1),ld(X1,X2)),X3),
inference(cp,[status(thm)],[t20143,t224]) ).
cnf(t21277,plain,
ld(ld(X1,X2),ld(ld(X1,X2),X3)) = mult(rd(ld(X2,X1),ld(X1,X2)),X3),
inference(orient,[status(thm)],[t20179]) ).
cnf(t21346,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)],[t21277,t4943]) ).
cnf(t221521,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)],[t21346,t215]) ).
cnf(t221522,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)],[t221521,t24]) ).
cnf(t221523,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)],[t221522,t1293]) ).
cnf(t221524,plain,
mult(mult(X2,mult(X2,mult(X2,X2))),X3) = mult(X2,mult(X2,mult(X2,mult(X2,X3)))),
inference(step,[status(thm)],[t221523,t4943]) ).
cnf(t23221,plain,
mult(mult(X1,mult(X1,mult(X1,X1))),X2) = mult(X1,mult(X1,mult(X1,mult(X1,X2)))),
inference(orient,[status(thm)],[t221524]) ).
cnf(t222409,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)],[t222408,t23221]) ).
cnf(t222410,plain,
rd(mult(X1,mult(X1,mult(X1,mult(X2,X1)))),X1) = mult(X1,mult(X1,mult(X1,X2))),
inference(step,[status(thm)],[t222409,t12]) ).
cnf(t143725,plain,
rd(mult(X1,mult(X1,mult(X1,mult(X2,X1)))),X1) = mult(X1,mult(X1,mult(X1,X2))),
inference(orient,[status(thm)],[t222410]) ).
cnf(t143733,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)],[t143725,t1174]) ).
cnf(t222600,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)],[t143733,t3965]) ).
cnf(t222601,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)],[t222600,t3965]) ).
cnf(t222602,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)],[t222601,t8]) ).
cnf(t222603,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)],[t222602,t456]) ).
cnf(t222604,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)],[t222603,t9]) ).
cnf(t222605,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)],[t222604,t3965]) ).
cnf(t222606,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)],[t222605,t1429]) ).
cnf(t222607,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)],[t222606,t456]) ).
cnf(t222608,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)],[t222607,t3965]) ).
cnf(t222609,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)],[t222608,t8]) ).
cnf(t222610,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)],[t222609,t3965]) ).
cnf(t222611,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)],[t222610,t8]) ).
cnf(t222612,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)],[t222611,t456]) ).
cnf(t222613,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)],[t222612,t3965]) ).
cnf(t222614,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)],[t222613,t1429]) ).
cnf(t222615,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)],[t222614,t8]) ).
cnf(t222616,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)],[t222615,t456]) ).
cnf(t222617,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)],[t222616,t1132]) ).
cnf(t222618,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)],[t222617,t1429]) ).
cnf(t222619,plain,
rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = ld(X1,ld(X1,ld(X1,X2))),
inference(step,[status(thm)],[t222618,t8]) ).
cnf(t174543,plain,
rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = ld(X1,ld(X1,ld(X1,X2))),
inference(orient,[status(thm)],[t222619]) ).
cnf(t174724,plain,
ld(X1,mult(ld(mult(X1,X1),X2),X1)) = mult(ld(X1,ld(X1,ld(X1,X2))),X1),
inference(cp,[status(thm)],[t8,t174543]) ).
cnf(t175454,plain,
ld(X1,mult(ld(mult(X1,X1),X2),X1)) = mult(ld(X1,ld(X1,ld(X1,X2))),X1),
inference(orient,[status(thm)],[t174724]) ).
cnf(t222744,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)],[t222743,t175454]) ).
cnf(t222745,plain,
rd(X1,ld(ld(X1,mult(X2,X1)),mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),X1),
inference(step,[status(thm)],[t222744,t12]) ).
cnf(t195157,plain,
rd(X1,ld(ld(X1,mult(X2,X1)),mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),X1),
inference(orient,[status(thm)],[t222745]) ).
cnf(t107734,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)],[t107698,t1174]) ).
cnf(t222177,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)],[t107734,t1174]) ).
cnf(t222178,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)],[t222177,t2624]) ).
cnf(t222179,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)],[t222178,t989]) ).
cnf(t222180,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)],[t222179,t1174]) ).
cnf(t1455,plain,
rd(ld(X1,ld(X2,rd(X1,X1))),X1) = ld(mult(X2,X1),rd(X1,mult(X1,X1))),
inference(cp,[status(thm)],[t1429,t1088]) ).
cnf(t11175,plain,
ld(mult(X1,X2),rd(X2,mult(X2,X2))) = rd(ld(X2,ld(X1,rd(X2,X2))),X2),
inference(orient,[status(thm)],[t1455]) ).
cnf(t222181,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)],[t222180,t11175]) ).
cnf(t222182,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)],[t222181,t3289]) ).
cnf(t222183,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)],[t222182,t2930]) ).
cnf(t222184,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)],[t222183,t2930]) ).
cnf(t222185,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)],[t222184,t8]) ).
cnf(t222186,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)],[t222185,t44]) ).
cnf(t222187,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)],[t222186,t3965]) ).
cnf(t222188,plain,
mult(rd(X1,ld(X2,rd(X1,X1))),X1) = mult(mult(X1,X1),ld(X1,mult(X2,X1))),
inference(step,[status(thm)],[t222187,t8]) ).
cnf(t222189,plain,
mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(mult(X1,X1),ld(mult(X2,X1),X1)),
inference(step,[status(thm)],[t222188,t196]) ).
cnf(t109354,plain,
mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(mult(X1,X1),ld(mult(X2,X1),X1)),
inference(orient,[status(thm)],[t222189]) ).
cnf(t120144,plain,
rd(mult(X1,X1),ld(X2,X1)) = rd(X1,ld(X2,rd(X1,X1))),
inference(cp,[status(thm)],[t120116,t23]) ).
cnf(t120509,plain,
rd(mult(X1,X1),ld(X2,X1)) = rd(X1,ld(X2,rd(X1,X1))),
inference(orient,[status(thm)],[t120144]) ).
cnf(t222259,plain,
mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(X1,ld(mult(X2,X1),rd(X1,X1))),
inference(step,[status(thm)],[t109354,t120509]) ).
cnf(t222260,plain,
mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(X1,rd(ld(X1,ld(X2,X1)),X1)),
inference(step,[status(thm)],[t222259,t1429]) ).
cnf(t120512,plain,
mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(X1,rd(ld(X1,ld(X2,X1)),X1)),
inference(orient,[status(thm)],[t222260]) ).
cnf(t195246,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)],[t195157,t120512]) ).
cnf(t222746,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)],[t195246,t224]) ).
cnf(t222747,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)],[t222746,t504]) ).
cnf(t1476,plain,
ld(rd(X1,X2),mult(X3,X2)) = ld(Y3,rd(Y3,rd(ld(X2,ld(X3,X1)),X2))),
inference(cp,[status(thm)],[t224,t1429]) ).
cnf(t221690,plain,
mult(X2,mult(ld(X1,X3),X2)) = ld(Y3,rd(Y3,rd(ld(X2,ld(X3,X1)),X2))),
inference(step,[status(thm)],[t1476,t83]) ).
cnf(t44094,plain,
ld(X1,rd(X1,rd(ld(X2,ld(X3,Y3)),X2))) = mult(X2,mult(ld(Y3,X3),X2)),
inference(orient,[status(thm)],[t221690]) ).
cnf(t222748,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)],[t222747,t44094]) ).
cnf(t222749,plain,
mult(mult(ld(X1,rd(X2,X1)),X1),X1) = mult(rd(X1,X1),mult(ld(X1,X2),X1)),
inference(step,[status(thm)],[t222748,t119423]) ).
cnf(t195615,plain,
mult(mult(ld(X1,rd(X2,X1)),X1),X1) = mult(rd(X1,X1),mult(ld(X1,X2),X1)),
inference(orient,[status(thm)],[t222749]) ).
cnf(t195912,plain,
mult(ld(X1,rd(X2,X1)),X1) = rd(mult(rd(X1,X1),mult(ld(X1,X2),X1)),X1),
inference(cp,[status(thm)],[t9,t195615]) ).
cnf(t212872,plain,
rd(mult(rd(X1,X1),mult(ld(X1,X2),X1)),X1) = mult(ld(X1,rd(X2,X1)),X1),
inference(orient,[status(thm)],[t195912]) ).
cnf(t219909,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)],[t219880,t212872]) ).
cnf(t223003,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)],[t219909,t989]) ).
cnf(t223004,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)],[t223003,t219881]) ).
cnf(t223005,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)],[t223004,t196]) ).
cnf(t223006,plain,
X2 = mult(ld(rd(X1,X1),rd(X2,rd(X1,X1))),rd(X1,X1)),
inference(step,[status(thm)],[t223005,t23]) ).
cnf(t223007,plain,
X2 = ld(rd(X1,X1),rd(X2,rd(X1,X1))),
inference(step,[status(thm)],[t223006,t219881]) ).
cnf(t223008,plain,
X2 = ld(rd(X1,X1),X2),
inference(step,[status(thm)],[t223007,t219880]) ).
cnf(t220379,plain,
ld(rd(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t223008]) ).
cnf(t223077,plain,
mult(rd(X1,X1),X2) = X2,
inference(step,[status(thm)],[t223076,t220379]) ).
cnf(t220830,plain,
mult(rd(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t223077]) ).
fof(f5,conjecture,
! [X0,X1] :
( mult(rd(X1,X1),X0) = X0
& mult(X0,rd(X1,X1)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f5_neg,negated_conjecture,
~ ! [X0,X1] :
( mult(rd(X1,X1),X0) = X0
& mult(X0,rd(X1,X1)) = X0 ),
inference(negated_conjecture,[status(cth)],[f5]) ).
fof(f5_nnf,plain,
? [X0,X1] :
( mult(rd(X1,X1),X0) != X0
| mult(X0,rd(X1,X1)) != X0 ),
inference(nnf_transformation,[status(thm)],[f5_neg]) ).
fof(f5_sk,plain,
( mult(rd(sk1,sk1),sk0) != sk0
| mult(sk0,rd(sk1,sk1)) != sk0 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f5_nnf]) ).
cnf(c5,plain,
( mult(rd(sk1,sk1),sk0) != sk0
| mult(sk0,rd(sk1,sk1)) != sk0 ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(g0_0,plain,
true != ifeq(mult(sk0,rd(sk1,sk1)),sk0,ifeq(mult(rd(sk1,sk1),sk0),sk0,false,true),true),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
true != ifeq(rd(sk0,ld(sk1,sk1)),sk0,ifeq(mult(rd(sk1,sk1),sk0),sk0,false,true),true),
inference(rw,[status(thm)],[g0_0]) ).
cnf(g0_2,plain,
true != ifeq(rd(sk0,rd(sk1,sk1)),sk0,ifeq(mult(rd(sk1,sk1),sk0),sk0,false,true),true),
inference(rw,[status(thm)],[g0_1,t614]) ).
cnf(g0_3,plain,
true != ifeq(sk0,sk0,ifeq(mult(rd(sk1,sk1),sk0),sk0,false,true),true),
inference(rw,[status(thm)],[g0_2,t219880]) ).
cnf(g0_4,plain,
true != ifeq(mult(rd(sk1,sk1),sk0),sk0,false,true),
inference(rw,[status(thm)],[g0_3,t11]) ).
cnf(g0_5,plain,
true != ifeq(sk0,sk0,false,true),
inference(rw,[status(thm)],[g0_4,t220830]) ).
cnf(g0_6,plain,
true != false,
inference(rw,[status(thm)],[g0_5,t11]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP655+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n018.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 15:32:47 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 106.13/13.89 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 106.13/13.89 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------