%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP655+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n003.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 53.44s 18.17s
% Output : Proof 53.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 186
% Number of leaves : 7
% Syntax : Number of formulae : 1023 (1018 unt; 0 def)
% Number of atoms : 1028 (1027 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 14 ( 9 ~; 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 : 7 ( 7 usr; 2 con; 0-4 aty)
% Number of variables : 2267 ( 2 sgn 37 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,conjecture,
? [X0] :
! [X1] :
( mult(X0,X1) = X1
& mult(X1,X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f5_neg,negated_conjecture,
~ ? [X0] :
! [X1] :
( mult(X0,X1) = X1
& mult(X1,X0) = X1 ),
inference(negated_conjecture,[status(cth)],[f5]) ).
fof(f5_nnf,plain,
! [X0] :
? [X1] :
( mult(X0,X1) != X1
| mult(X1,X0) != X1 ),
inference(nnf_transformation,[status(thm)],[f5_neg]) ).
fof(f5_sk,plain,
! [X0] :
( mult(X0,sk0(X0)) != sk0(X0)
| mult(sk0(X0),X0) != sk0(X0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f5_nnf]) ).
cnf(c5,plain,
( mult(X0,sk0(X0)) != sk0(X0)
| mult(sk0(X0),X0) != sk0(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t6,plain,
ifeq(mult(sk0(X1),X1),sk0(X1),ifeq(mult(X1,sk0(X1)),sk0(X1),false,true),true) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t22,plain,
ifeq(mult(sk0(X1),X1),sk0(X1),ifeq(mult(X1,sk0(X1)),sk0(X1),false,true),true) = true,
inference(orient,[status(thm)],[t6]) ).
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(t10,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)],[t10,t34]) ).
cnf(t400,plain,
rd(mult(rd(X1,X2),mult(X2,X3)),X2) = mult(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t39]) ).
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]) ).
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(t411,plain,
mult(X1,rd(X2,ld(X3,rd(X3,X2)))) = rd(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),ld(X3,rd(X3,X2))),
inference(cp,[status(thm)],[t400,t131]) ).
cnf(t128,plain,
mult(mult(X1,ld(mult(X2,X3),X2)),X3) = mult(rd(X1,X3),mult(X3,ld(X3,X3))),
inference(cp,[status(thm)],[t25,t114]) ).
cnf(t221222,plain,
mult(mult(X1,ld(mult(X2,X3),X2)),X3) = mult(rd(X1,X3),X3),
inference(step,[status(thm)],[t128,t7]) ).
cnf(t221223,plain,
mult(mult(X1,ld(mult(X2,X3),X2)),X3) = X1,
inference(step,[status(thm)],[t221222,t8]) ).
cnf(t154,plain,
mult(mult(X1,ld(mult(X2,X3),X2)),X3) = X1,
inference(orient,[status(thm)],[t221223]) ).
cnf(t159,plain,
rd(X1,ld(mult(X2,X3),X2)) = mult(X1,X3),
inference(cp,[status(thm)],[t154,t8]) ).
cnf(t179,plain,
rd(X1,ld(mult(X2,X3),X2)) = mult(X1,X3),
inference(orient,[status(thm)],[t159]) ).
cnf(t187,plain,
mult(X1,X2) = rd(X1,ld(X3,rd(X3,X2))),
inference(cp,[status(thm)],[t179,t8]) ).
cnf(t216,plain,
rd(X1,ld(X2,rd(X2,X3))) = mult(X1,X3),
inference(orient,[status(thm)],[t187]) ).
cnf(t221227,plain,
mult(X1,mult(X2,X2)) = rd(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),ld(X3,rd(X3,X2))),
inference(step,[status(thm)],[t411,t216]) ).
cnf(t221228,plain,
mult(X1,mult(X2,X2)) = mult(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
inference(step,[status(thm)],[t221227,t216]) ).
cnf(t181,plain,
mult(X1,ld(X2,X3)) = rd(X1,ld(X3,X2)),
inference(cp,[status(thm)],[t179,t7]) ).
cnf(t196,plain,
mult(X1,ld(X2,X3)) = rd(X1,ld(X3,X2)),
inference(orient,[status(thm)],[t181]) ).
cnf(t221229,plain,
mult(X1,mult(X2,X2)) = mult(rd(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
inference(step,[status(thm)],[t221228,t196]) ).
cnf(t221230,plain,
mult(X1,mult(X2,X2)) = mult(rd(mult(X1,X2),ld(X2,X2)),X2),
inference(step,[status(thm)],[t221229,t216]) ).
cnf(t541,plain,
mult(rd(mult(X1,X2),ld(X2,X2)),X2) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t221230]) ).
cnf(t552,plain,
mult(rd(X1,X2),mult(X2,X2)) = mult(rd(X1,ld(X2,X2)),X2),
inference(cp,[status(thm)],[t541,t8]) ).
cnf(t569,plain,
mult(rd(X1,ld(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
inference(orient,[status(thm)],[t552]) ).
cnf(t582,plain,
rd(X1,ld(X2,X2)) = rd(mult(rd(X1,X2),mult(X2,X2)),X2),
inference(cp,[status(thm)],[t10,t569]) ).
cnf(t221231,plain,
rd(X1,ld(X2,X2)) = mult(X1,rd(X2,X2)),
inference(step,[status(thm)],[t582,t400]) ).
cnf(t592,plain,
mult(X1,rd(X2,X2)) = rd(X1,ld(X2,X2)),
inference(orient,[status(thm)],[t221231]) ).
cnf(t598,plain,
rd(rd(X1,rd(X2,X2)),ld(X2,X2)) = X1,
inference(cp,[status(thm)],[t592,t8]) ).
cnf(t603,plain,
rd(X1,X1) = ld(X2,rd(X2,ld(X1,X1))),
inference(cp,[status(thm)],[t12,t592]) ).
cnf(t207,plain,
ld(X1,X2) = ld(X3,rd(X3,ld(X2,X1))),
inference(cp,[status(thm)],[t12,t196]) ).
cnf(t225,plain,
ld(X1,rd(X1,ld(X2,X3))) = ld(X3,X2),
inference(orient,[status(thm)],[t207]) ).
cnf(t221232,plain,
rd(X1,X1) = ld(X1,X1),
inference(step,[status(thm)],[t603,t225]) ).
cnf(t616,plain,
ld(X1,X1) = rd(X1,X1),
inference(orient,[status(thm)],[t221232]) ).
cnf(t221247,plain,
rd(rd(X1,rd(X2,X2)),rd(X2,X2)) = X1,
inference(step,[status(thm)],[t598,t616]) ).
cnf(t687,plain,
rd(rd(X1,rd(X2,X2)),rd(X2,X2)) = X1,
inference(orient,[status(thm)],[t221247]) ).
cnf(t11,plain,
X1 = rd(X2,ld(X1,X2)),
inference(cp,[status(thm)],[t10,t7]) ).
cnf(t23,plain,
rd(X1,ld(X2,X1)) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(t621,plain,
X1 = rd(X1,rd(X1,X1)),
inference(cp,[status(thm)],[t23,t616]) ).
cnf(t636,plain,
rd(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t621]) ).
cnf(t641,plain,
mult(X1,rd(X2,rd(X1,X1))) = rd(mult(X1,mult(rd(X1,X1),X2)),rd(X1,X1)),
inference(cp,[status(thm)],[t400,t636]) ).
cnf(t39945,plain,
rd(mult(X1,mult(rd(X1,X1),X2)),rd(X1,X1)) = mult(X1,rd(X2,rd(X1,X1))),
inference(orient,[status(thm)],[t641]) ).
cnf(t40058,plain,
mult(X1,mult(rd(X1,X1),X2)) = rd(mult(X1,rd(X2,rd(X1,X1))),rd(X1,X1)),
inference(cp,[status(thm)],[t687,t39945]) ).
cnf(t81301,plain,
rd(mult(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = mult(X1,mult(rd(X1,X1),X2)),
inference(orient,[status(thm)],[t40058]) ).
cnf(t42,plain,
mult(rd(mult(X1,rd(X2,rd(X3,Y3))),Y3),mult(Y3,X3)) = mult(mult(rd(X1,rd(X3,Y3)),mult(rd(X3,Y3),X2)),Y3),
inference(cp,[status(thm)],[t34,t34]) ).
cnf(t104729,plain,
mult(mult(rd(X1,rd(X2,X3)),mult(rd(X2,X3),Y3)),X3) = mult(rd(mult(X1,rd(Y3,rd(X2,X3))),X3),mult(X3,X2)),
inference(orient,[status(thm)],[t42]) ).
cnf(t637,plain,
ld(X1,rd(X1,X2)) = rd(ld(X1,rd(X1,X2)),mult(ld(X1,rd(X1,X2)),X2)),
inference(cp,[status(thm)],[t636,t216]) ).
cnf(t221233,plain,
mult(ld(X1,rd(X1,X2)),X2) = rd(X2,X2),
inference(step,[status(thm)],[t131,t616]) ).
cnf(t617,plain,
mult(ld(X1,rd(X1,X2)),X2) = rd(X2,X2),
inference(orient,[status(thm)],[t221233]) ).
cnf(t221300,plain,
ld(X1,rd(X1,X2)) = rd(ld(X1,rd(X1,X2)),rd(X2,X2)),
inference(step,[status(thm)],[t637,t617]) ).
cnf(t1668,plain,
rd(ld(X1,rd(X1,X2)),rd(X2,X2)) = ld(X1,rd(X1,X2)),
inference(orient,[status(thm)],[t221300]) ).
cnf(t104819,plain,
mult(rd(mult(ld(X1,rd(X1,X2)),rd(X3,rd(X2,X2))),X2),mult(X2,X2)) = mult(mult(ld(X1,rd(X1,X2)),mult(rd(X2,X2),X3)),X2),
inference(cp,[status(thm)],[t104729,t1668]) ).
cnf(t19,plain,
mult(mult(X1,X2),X3) = rd(mult(X1,mult(X2,mult(X3,X2))),X2),
inference(cp,[status(thm)],[t10,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(t639,plain,
rd(mult(X1,mult(rd(X2,X2),X2)),rd(X2,X2)) = mult(mult(X1,rd(X2,X2)),X2),
inference(cp,[status(thm)],[t56,t636]) ).
cnf(t221253,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(mult(X1,rd(X2,X2)),X2),
inference(step,[status(thm)],[t639,t8]) ).
cnf(t221254,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(rd(X1,X2),mult(X2,X2)),
inference(step,[status(thm)],[t221253,t34]) ).
cnf(t902,plain,
mult(rd(X1,X2),mult(X2,X2)) = rd(mult(X1,X2),rd(X2,X2)),
inference(orient,[status(thm)],[t221254]) ).
cnf(t222157,plain,
rd(mult(mult(ld(X1,rd(X1,X2)),rd(X3,rd(X2,X2))),X2),rd(X2,X2)) = mult(mult(ld(X1,rd(X1,X2)),mult(rd(X2,X2),X3)),X2),
inference(step,[status(thm)],[t104819,t902]) ).
cnf(t93,plain,
mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
inference(cp,[status(thm)],[t83,t8]) ).
cnf(t479,plain,
mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
inference(orient,[status(thm)],[t93]) ).
cnf(t494,plain,
mult(ld(X1,rd(X2,X3)),X3) = ld(X3,ld(rd(X1,X3),X2)),
inference(cp,[status(thm)],[t12,t479]) ).
cnf(t506,plain,
ld(X1,ld(rd(X2,X1),X3)) = mult(ld(X2,rd(X3,X1)),X1),
inference(orient,[status(thm)],[t494]) ).
cnf(t508,plain,
mult(ld(X1,rd(mult(rd(X1,X2),X3),X2)),X2) = ld(X2,X3),
inference(cp,[status(thm)],[t506,t12]) ).
cnf(t3677,plain,
mult(ld(X1,rd(mult(rd(X1,X2),X3),X2)),X2) = ld(X2,X3),
inference(orient,[status(thm)],[t508]) ).
cnf(t3734,plain,
ld(X1,rd(mult(rd(X1,X2),X3),X2)) = rd(ld(X2,X3),X2),
inference(cp,[status(thm)],[t10,t3677]) ).
cnf(t3761,plain,
ld(X1,rd(mult(rd(X1,X2),X3),X2)) = rd(ld(X2,X3),X2),
inference(orient,[status(thm)],[t3734]) ).
cnf(t3768,plain,
rd(ld(ld(X1,rd(X1,X2)),X3),ld(X1,rd(X1,X2))) = ld(Y3,mult(mult(rd(Y3,ld(X1,rd(X1,X2))),X3),X2)),
inference(cp,[status(thm)],[t3761,t216]) ).
cnf(t221368,plain,
mult(ld(ld(X1,rd(X1,X2)),X3),X2) = ld(Y3,mult(mult(rd(Y3,ld(X1,rd(X1,X2))),X3),X2)),
inference(step,[status(thm)],[t3768,t216]) ).
cnf(t221369,plain,
mult(ld(ld(X1,rd(X1,X2)),X3),X2) = ld(Y3,mult(mult(mult(Y3,X2),X3),X2)),
inference(step,[status(thm)],[t221368,t216]) ).
cnf(t221370,plain,
mult(ld(ld(X1,rd(X1,X2)),X3),X2) = ld(Y3,mult(Y3,mult(X2,mult(X3,X2)))),
inference(step,[status(thm)],[t221369,t14]) ).
cnf(t221371,plain,
mult(ld(ld(X1,rd(X1,X2)),X3),X2) = mult(X2,mult(X3,X2)),
inference(step,[status(thm)],[t221370,t12]) ).
cnf(t3823,plain,
mult(ld(ld(X1,rd(X1,X2)),X3),X2) = mult(X2,mult(X3,X2)),
inference(orient,[status(thm)],[t221371]) ).
cnf(t3852,plain,
mult(ld(X1,rd(X1,X2)),mult(X3,ld(X1,rd(X1,X2)))) = mult(ld(ld(Y3,mult(Y3,X2)),X3),ld(X1,rd(X1,X2))),
inference(cp,[status(thm)],[t3823,t216]) ).
cnf(t221375,plain,
mult(ld(X1,rd(X1,X2)),rd(X3,ld(rd(X1,X2),X1))) = mult(ld(ld(Y3,mult(Y3,X2)),X3),ld(X1,rd(X1,X2))),
inference(step,[status(thm)],[t3852,t196]) ).
cnf(t221376,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)],[t221375,t24]) ).
cnf(t221377,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)],[t221376,t196]) ).
cnf(t221378,plain,
mult(ld(X1,rd(X1,X2)),rd(X3,X2)) = rd(ld(X2,X3),ld(rd(X1,X2),X1)),
inference(step,[status(thm)],[t221377,t12]) ).
cnf(t221379,plain,
mult(ld(X1,rd(X1,X2)),rd(X3,X2)) = rd(ld(X2,X3),X2),
inference(step,[status(thm)],[t221378,t24]) ).
cnf(t4024,plain,
mult(ld(X1,rd(X1,X2)),rd(X3,X2)) = rd(ld(X2,X3),X2),
inference(orient,[status(thm)],[t221379]) ).
cnf(t4071,plain,
rd(ld(ld(X1,X2),X2),ld(X1,X2)) = mult(ld(X3,rd(X3,ld(X1,X2))),X1),
inference(cp,[status(thm)],[t4024,t23]) ).
cnf(t221381,plain,
rd(ld(ld(X1,X2),X2),ld(X1,X2)) = mult(ld(X2,X1),X1),
inference(step,[status(thm)],[t4071,t225]) ).
cnf(t4286,plain,
rd(ld(ld(X1,X2),X2),ld(X1,X2)) = mult(ld(X2,X1),X1),
inference(orient,[status(thm)],[t221381]) ).
cnf(t4330,plain,
ld(ld(X1,X2),X2) = mult(mult(ld(X2,X1),X1),ld(X1,X2)),
inference(cp,[status(thm)],[t8,t4286]) ).
cnf(t221386,plain,
ld(ld(X1,X2),X2) = rd(mult(ld(X2,X1),X1),ld(X2,X1)),
inference(step,[status(thm)],[t4330,t196]) ).
cnf(t4628,plain,
rd(mult(ld(X1,X2),X2),ld(X1,X2)) = ld(ld(X2,X1),X1),
inference(orient,[status(thm)],[t221386]) ).
cnf(t221,plain,
ld(X1,rd(X1,X2)) = ld(mult(X3,X2),X3),
inference(cp,[status(thm)],[t24,t216]) ).
cnf(t350,plain,
ld(X1,rd(X1,X2)) = ld(mult(X3,X2),X3),
inference(orient,[status(thm)],[t221]) ).
cnf(t4679,plain,
ld(ld(X1,mult(X1,X2)),mult(X1,X2)) = rd(mult(ld(mult(X1,X2),X1),X1),ld(X3,rd(X3,X2))),
inference(cp,[status(thm)],[t4628,t350]) ).
cnf(t221388,plain,
ld(X2,mult(X1,X2)) = rd(mult(ld(mult(X1,X2),X1),X1),ld(X3,rd(X3,X2))),
inference(step,[status(thm)],[t4679,t12]) ).
cnf(t221389,plain,
ld(X2,mult(X1,X2)) = mult(mult(ld(mult(X1,X2),X1),X1),X2),
inference(step,[status(thm)],[t221388,t216]) ).
cnf(t221390,plain,
ld(X2,mult(X1,X2)) = mult(mult(ld(true,rd(true,X2)),X1),X2),
inference(step,[status(thm)],[t221389,t350]) ).
cnf(t4891,plain,
mult(mult(ld(true,rd(true,X1)),X2),X1) = ld(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t221390]) ).
cnf(t229,plain,
ld(X1,rd(X1,X2)) = ld(X3,rd(X3,X2)),
inference(cp,[status(thm)],[t225,t24]) ).
cnf(t391,plain,
ld(X1,rd(X1,X2)) = ld(X3,rd(X3,X2)),
inference(orient,[status(thm)],[t229]) ).
cnf(t4908,plain,
ld(X1,mult(X2,X1)) = mult(mult(ld(X3,rd(X3,X1)),X2),X1),
inference(cp,[status(thm)],[t4891,t391]) ).
cnf(t5118,plain,
mult(mult(ld(X1,rd(X1,X2)),X3),X2) = ld(X2,mult(X3,X2)),
inference(orient,[status(thm)],[t4908]) ).
cnf(t222158,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)],[t222157,t5118]) ).
cnf(t221239,plain,
mult(rd(X1,rd(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
inference(step,[status(thm)],[t569,t616]) ).
cnf(t631,plain,
mult(rd(X1,rd(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
inference(rw,[status(thm)],[t221239]) ).
cnf(t785,plain,
mult(rd(X1,rd(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
inference(orient,[status(thm)],[t631]) ).
cnf(t221255,plain,
mult(rd(X1,rd(X2,X2)),X2) = rd(mult(X1,X2),rd(X2,X2)),
inference(step,[status(thm)],[t785,t902]) ).
cnf(t903,plain,
mult(rd(X1,rd(X2,X2)),X2) = rd(mult(X1,X2),rd(X2,X2)),
inference(orient,[status(thm)],[t221255]) ).
cnf(t222159,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)],[t222158,t903]) ).
cnf(t640,plain,
mult(ld(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),ld(X1,X2)),
inference(cp,[status(thm)],[t506,t636]) ).
cnf(t221235,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
inference(step,[status(thm)],[t592,t616]) ).
cnf(t619,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t221235]) ).
cnf(t221690,plain,
rd(ld(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),ld(X1,X2)),
inference(step,[status(thm)],[t640,t619]) ).
cnf(t39789,plain,
rd(ld(X1,rd(X2,rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),ld(X1,X2)),
inference(orient,[status(thm)],[t221690]) ).
cnf(t222160,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)],[t222159,t39789]) ).
cnf(t222161,plain,
ld(rd(X2,X2),ld(X2,mult(X3,X2))) = ld(X2,mult(mult(rd(X2,X2),X3),X2)),
inference(step,[status(thm)],[t222160,t5118]) ).
cnf(t105369,plain,
ld(rd(X1,X1),ld(X1,mult(X2,X1))) = ld(X1,mult(mult(rd(X1,X1),X2),X1)),
inference(orient,[status(thm)],[t222161]) ).
cnf(t124,plain,
ld(mult(X1,X2),X1) = rd(ld(X2,X2),X2),
inference(cp,[status(thm)],[t10,t114]) ).
cnf(t270,plain,
ld(mult(X1,X2),X1) = rd(ld(X2,X2),X2),
inference(orient,[status(thm)],[t124]) ).
cnf(t281,plain,
mult(X1,X2) = rd(X1,rd(ld(X2,X2),X2)),
inference(cp,[status(thm)],[t23,t270]) ).
cnf(t310,plain,
rd(X1,rd(ld(X2,X2),X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t281]) ).
cnf(t221242,plain,
rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
inference(step,[status(thm)],[t310,t616]) ).
cnf(t633,plain,
rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
inference(rw,[status(thm)],[t221242]) ).
cnf(t654,plain,
rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t633]) ).
cnf(t137,plain,
ld(X1,rd(X1,X2)) = rd(ld(X2,X2),X2),
inference(cp,[status(thm)],[t10,t131]) ).
cnf(t322,plain,
ld(X1,rd(X1,X2)) = rd(ld(X2,X2),X2),
inference(orient,[status(thm)],[t137]) ).
cnf(t221237,plain,
ld(X1,rd(X1,X2)) = rd(rd(X2,X2),X2),
inference(step,[status(thm)],[t322,t616]) ).
cnf(t629,plain,
ld(X1,rd(X1,X2)) = rd(rd(X2,X2),X2),
inference(rw,[status(thm)],[t221237]) ).
cnf(t999,plain,
ld(X1,rd(X1,X2)) = rd(rd(X2,X2),X2),
inference(orient,[status(thm)],[t629]) ).
cnf(t1016,plain,
rd(mult(rd(X1,X1),X1),rd(X1,X1)) = mult(ld(X2,rd(X2,X1)),mult(X1,X1)),
inference(cp,[status(thm)],[t902,t999]) ).
cnf(t221265,plain,
rd(X1,rd(X1,X1)) = mult(ld(X2,rd(X2,X1)),mult(X1,X1)),
inference(step,[status(thm)],[t1016,t8]) ).
cnf(t221266,plain,
X1 = mult(ld(X2,rd(X2,X1)),mult(X1,X1)),
inference(step,[status(thm)],[t221265,t636]) ).
cnf(t1028,plain,
mult(ld(X1,rd(X1,X2)),mult(X2,X2)) = X2,
inference(orient,[status(thm)],[t221266]) ).
cnf(t1045,plain,
mult(X1,X1) = ld(ld(X2,rd(X2,X1)),X1),
inference(cp,[status(thm)],[t12,t1028]) ).
cnf(t1056,plain,
ld(ld(X1,rd(X1,X2)),X2) = mult(X2,X2),
inference(orient,[status(thm)],[t1045]) ).
cnf(t1058,plain,
mult(X1,X1) = ld(rd(rd(X1,X1),X1),X1),
inference(cp,[status(thm)],[t1056,t999]) ).
cnf(t1078,plain,
ld(rd(rd(X1,X1),X1),X1) = mult(X1,X1),
inference(orient,[status(thm)],[t1058]) ).
cnf(t1085,plain,
rd(rd(X1,X1),X1) = rd(X1,mult(X1,X1)),
inference(cp,[status(thm)],[t23,t1078]) ).
cnf(t1091,plain,
rd(rd(X1,X1),X1) = rd(X1,mult(X1,X1)),
inference(orient,[status(thm)],[t1085]) ).
cnf(t221269,plain,
rd(X1,rd(X2,mult(X2,X2))) = mult(X1,X2),
inference(step,[status(thm)],[t654,t1091]) ).
cnf(t1115,plain,
rd(X1,rd(X2,mult(X2,X2))) = mult(X1,X2),
inference(rw,[status(thm)],[t221269]) ).
cnf(t1178,plain,
rd(X1,rd(X2,mult(X2,X2))) = mult(X1,X2),
inference(orient,[status(thm)],[t1115]) ).
cnf(t105377,plain,
ld(rd(X1,mult(X1,X1)),mult(mult(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),X2),rd(X1,mult(X1,X1)))) = ld(mult(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),
inference(cp,[status(thm)],[t105369,t1178]) ).
cnf(t87,plain,
mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
inference(cp,[status(thm)],[t83,t10]) ).
cnf(t431,plain,
mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
inference(orient,[status(thm)],[t87]) ).
cnf(t447,plain,
mult(ld(mult(X1,X2),X3),X2) = ld(X2,ld(X1,mult(X3,X2))),
inference(cp,[status(thm)],[t12,t431]) ).
cnf(t458,plain,
ld(X1,ld(X2,mult(X3,X1))) = mult(ld(mult(X2,X1),X3),X1),
inference(orient,[status(thm)],[t447]) ).
cnf(t460,plain,
mult(ld(mult(rd(mult(X1,X2),X3),X2),X1),X2) = ld(X2,X3),
inference(cp,[status(thm)],[t458,t24]) ).
cnf(t2858,plain,
mult(ld(mult(rd(mult(X1,X2),X3),X2),X1),X2) = ld(X2,X3),
inference(orient,[status(thm)],[t460]) ).
cnf(t280,plain,
rd(X1,ld(X2,mult(X2,X3))) = mult(X1,rd(ld(X3,X3),X3)),
inference(cp,[status(thm)],[t196,t270]) ).
cnf(t221225,plain,
rd(X1,X3) = mult(X1,rd(ld(X3,X3),X3)),
inference(step,[status(thm)],[t280,t12]) ).
cnf(t292,plain,
mult(X1,rd(ld(X2,X2),X2)) = rd(X1,X2),
inference(orient,[status(thm)],[t221225]) ).
cnf(t221243,plain,
mult(X1,rd(rd(X2,X2),X2)) = rd(X1,X2),
inference(step,[status(thm)],[t292,t616]) ).
cnf(t634,plain,
mult(X1,rd(rd(X2,X2),X2)) = rd(X1,X2),
inference(rw,[status(thm)],[t221243]) ).
cnf(t671,plain,
mult(X1,rd(rd(X2,X2),X2)) = rd(X1,X2),
inference(orient,[status(thm)],[t634]) ).
cnf(t221268,plain,
mult(X1,rd(X2,mult(X2,X2))) = rd(X1,X2),
inference(step,[status(thm)],[t671,t1091]) ).
cnf(t1114,plain,
mult(X1,rd(X2,mult(X2,X2))) = rd(X1,X2),
inference(rw,[status(thm)],[t221268]) ).
cnf(t1135,plain,
mult(X1,rd(X2,mult(X2,X2))) = rd(X1,X2),
inference(orient,[status(thm)],[t1114]) ).
cnf(t2862,plain,
ld(rd(X1,mult(X1,X1)),X2) = rd(ld(mult(rd(mult(X3,rd(X1,mult(X1,X1))),X2),rd(X1,mult(X1,X1))),X3),X1),
inference(cp,[status(thm)],[t2858,t1135]) ).
cnf(t221334,plain,
ld(rd(X1,mult(X1,X1)),X2) = rd(ld(rd(rd(mult(X3,rd(X1,mult(X1,X1))),X2),X1),X3),X1),
inference(step,[status(thm)],[t2862,t1135]) ).
cnf(t221335,plain,
ld(rd(X1,mult(X1,X1)),X2) = rd(ld(rd(rd(rd(X3,X1),X2),X1),X3),X1),
inference(step,[status(thm)],[t221334,t1135]) ).
cnf(t483,plain,
ld(rd(rd(rd(X1,X2),X3),X2),X1) = mult(X2,mult(X3,X2)),
inference(cp,[status(thm)],[t479,t24]) ).
cnf(t1515,plain,
ld(rd(rd(rd(X1,X2),X3),X2),X1) = mult(X2,mult(X3,X2)),
inference(orient,[status(thm)],[t483]) ).
cnf(t1546,plain,
rd(rd(rd(X1,X2),X3),X2) = rd(X1,mult(X2,mult(X3,X2))),
inference(cp,[status(thm)],[t23,t1515]) ).
cnf(t1552,plain,
rd(rd(rd(X1,X2),X3),X2) = rd(X1,mult(X2,mult(X3,X2))),
inference(orient,[status(thm)],[t1546]) ).
cnf(t221336,plain,
ld(rd(X1,mult(X1,X1)),X2) = rd(ld(rd(X3,mult(X1,mult(X2,X1))),X3),X1),
inference(step,[status(thm)],[t221335,t1552]) ).
cnf(t221337,plain,
ld(rd(X1,mult(X1,X1)),X2) = rd(mult(X1,mult(X2,X1)),X1),
inference(step,[status(thm)],[t221336,t24]) ).
cnf(t2936,plain,
ld(rd(X1,mult(X1,X1)),X2) = rd(mult(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t221337]) ).
cnf(t222162,plain,
rd(mult(X1,mult(mult(mult(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),X2),rd(X1,mult(X1,X1))),X1)),X1) = ld(mult(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1))))),
inference(step,[status(thm)],[t105377,t2936]) ).
cnf(t222163,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)],[t222162,t1135]) ).
cnf(t222164,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)],[t222163,t8]) ).
cnf(t222165,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)],[t222164,t1178]) ).
cnf(t1586,plain,
rd(rd(X1,X2),X3) = mult(rd(X1,mult(X2,mult(X3,X2))),X2),
inference(cp,[status(thm)],[t8,t1552]) ).
cnf(t2570,plain,
mult(rd(X1,mult(X2,mult(X3,X2))),X2) = rd(rd(X1,X2),X3),
inference(orient,[status(thm)],[t1586]) ).
cnf(t2602,plain,
rd(rd(X1,X2),rd(X3,X2)) = mult(rd(X1,mult(X2,X3)),X2),
inference(cp,[status(thm)],[t2570,t8]) ).
cnf(t2630,plain,
mult(rd(X1,mult(X2,X3)),X2) = rd(rd(X1,X2),rd(X3,X2)),
inference(orient,[status(thm)],[t2602]) ).
cnf(t222166,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)],[t222165,t2630]) ).
cnf(t905,plain,
rd(mult(X1,rd(rd(X2,X2),X2)),rd(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))) = mult(mult(X1,X2),mult(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))),
inference(cp,[status(thm)],[t902,t654]) ).
cnf(t221258,plain,
rd(rd(X1,X2),rd(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))) = mult(mult(X1,X2),mult(rd(rd(X2,X2),X2),rd(rd(X2,X2),X2))),
inference(step,[status(thm)],[t905,t671]) ).
cnf(t221259,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)],[t221258,t654]) ).
cnf(t221260,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)],[t221259,t8]) ).
cnf(t221261,plain,
rd(rd(X1,X2),rd(X2,X2)) = mult(mult(X1,X2),rd(rd(rd(X2,X2),X2),X2)),
inference(step,[status(thm)],[t221260,t671]) ).
cnf(t221262,plain,
rd(rd(X1,X2),rd(X2,X2)) = rd(mult(X1,mult(X2,rd(rd(X2,X2),X2))),X2),
inference(step,[status(thm)],[t221261,t56]) ).
cnf(t221263,plain,
rd(rd(X1,X2),rd(X2,X2)) = rd(mult(X1,rd(X2,X2)),X2),
inference(step,[status(thm)],[t221262,t671]) ).
cnf(t221264,plain,
rd(rd(X1,X2),rd(X2,X2)) = rd(rd(X1,rd(X2,X2)),X2),
inference(step,[status(thm)],[t221263,t619]) ).
cnf(t967,plain,
rd(rd(X1,rd(X2,X2)),X2) = rd(rd(X1,X2),rd(X2,X2)),
inference(orient,[status(thm)],[t221264]) ).
cnf(t968,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(cp,[status(thm)],[t967,t636]) ).
cnf(t992,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t968]) ).
cnf(t222167,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)],[t222166,t992]) ).
cnf(t222168,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)],[t222167,t2630]) ).
cnf(t222169,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)],[t222168,t992]) ).
cnf(t222170,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)],[t222169,t2936]) ).
cnf(t222171,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)],[t222170,t1135]) ).
cnf(t222172,plain,
rd(mult(X1,mult(rd(X1,X1),X2)),X1) = ld(rd(X1,X1),rd(mult(X1,X2),X1)),
inference(step,[status(thm)],[t222171,t8]) ).
cnf(t105665,plain,
ld(rd(X1,X1),rd(mult(X1,X2),X1)) = rd(mult(X1,mult(rd(X1,X1),X2)),X1),
inference(orient,[status(thm)],[t222172]) ).
cnf(t105689,plain,
rd(mult(X1,mult(rd(X1,X1),mult(X1,mult(X2,X1)))),X1) = ld(rd(X1,X1),mult(mult(X1,X1),X2)),
inference(cp,[status(thm)],[t105665,t44]) ).
cnf(t222178,plain,
rd(mult(X1,mult(mult(X1,X2),X1)),X1) = ld(rd(X1,X1),mult(mult(X1,X1),X2)),
inference(step,[status(thm)],[t105689,t25]) ).
cnf(t106530,plain,
ld(rd(X1,X1),mult(mult(X1,X1),X2)) = rd(mult(X1,mult(mult(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t222178]) ).
cnf(t106628,plain,
rd(mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1)))),rd(X1,mult(X1,X1))) = ld(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),mult(rd(rd(X1,mult(X1,X1)),X1),X2)),
inference(cp,[status(thm)],[t106530,t1135]) ).
cnf(t222190,plain,
mult(mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1)))),X1) = ld(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),mult(rd(rd(X1,mult(X1,X1)),X1),X2)),
inference(step,[status(thm)],[t106628,t1178]) ).
cnf(t3828,plain,
mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))) = rd(ld(ld(X3,rd(X3,rd(X1,mult(X1,X1)))),X2),X1),
inference(cp,[status(thm)],[t3823,t1135]) ).
cnf(t221372,plain,
mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(ld(X3,rd(X3,rd(X1,mult(X1,X1)))),X2),X1),
inference(step,[status(thm)],[t3828,t1135]) ).
cnf(t221373,plain,
mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(ld(X3,mult(X3,X1)),X2),X1),
inference(step,[status(thm)],[t221372,t1178]) ).
cnf(t221374,plain,
mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(X1,X2),X1),
inference(step,[status(thm)],[t221373,t12]) ).
cnf(t3912,plain,
mult(rd(X1,mult(X1,X1)),rd(X2,X1)) = rd(ld(X1,X2),X1),
inference(orient,[status(thm)],[t221374]) ).
cnf(t3942,plain,
rd(ld(X1,mult(X2,X1)),X1) = mult(rd(X1,mult(X1,X1)),X2),
inference(cp,[status(thm)],[t3912,t10]) ).
cnf(t3971,plain,
mult(rd(X1,mult(X1,X1)),X2) = rd(ld(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t3942]) ).
cnf(t222191,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)],[t222190,t3971]) ).
cnf(t222192,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)],[t222191,t8]) ).
cnf(t222193,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)],[t222192,t1135]) ).
cnf(t222194,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)],[t222193,t8]) ).
cnf(t222195,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)],[t222194,t3971]) ).
cnf(t222196,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)],[t222195,t1178]) ).
cnf(t222197,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)],[t222196,t2630]) ).
cnf(t222198,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)],[t222197,t992]) ).
cnf(t1554,plain,
rd(X1,mult(X2,mult(rd(X2,X2),X2))) = rd(rd(rd(X1,X2),X2),rd(X2,X2)),
inference(cp,[status(thm)],[t1552,t967]) ).
cnf(t221330,plain,
rd(X1,mult(X2,X2)) = rd(rd(rd(X1,X2),X2),rd(X2,X2)),
inference(step,[status(thm)],[t1554,t8]) ).
cnf(t2335,plain,
rd(rd(rd(X1,X2),X2),rd(X2,X2)) = rd(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t221330]) ).
cnf(t2362,plain,
rd(rd(X1,X2),mult(X2,mult(rd(X2,X2),X2))) = rd(rd(X1,mult(X2,X2)),X2),
inference(cp,[status(thm)],[t1552,t2335]) ).
cnf(t221331,plain,
rd(rd(X1,X2),mult(X2,X2)) = rd(rd(X1,mult(X2,X2)),X2),
inference(step,[status(thm)],[t2362,t8]) ).
cnf(t2384,plain,
rd(rd(X1,mult(X2,X2)),X2) = rd(rd(X1,X2),mult(X2,X2)),
inference(orient,[status(thm)],[t221331]) ).
cnf(t222199,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)],[t222198,t2384]) ).
cnf(t1557,plain,
rd(X1,mult(X1,mult(X1,X1))) = rd(rd(X1,mult(X1,X1)),X1),
inference(cp,[status(thm)],[t1552,t1091]) ).
cnf(t136,plain,
X1 = ld(ld(X2,rd(X2,X1)),ld(X1,X1)),
inference(cp,[status(thm)],[t12,t131]) ).
cnf(t233,plain,
ld(ld(X1,rd(X1,X2)),ld(X2,X2)) = X2,
inference(orient,[status(thm)],[t136]) ).
cnf(t221244,plain,
ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
inference(step,[status(thm)],[t233,t616]) ).
cnf(t635,plain,
ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
inference(rw,[status(thm)],[t221244]) ).
cnf(t697,plain,
ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
inference(orient,[status(thm)],[t635]) ).
cnf(t700,plain,
rd(rd(X1,X1),X1) = ld(ld(X2,mult(X2,X1)),rd(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1))),
inference(cp,[status(thm)],[t697,t654]) ).
cnf(t221248,plain,
rd(rd(X1,X1),X1) = ld(X1,rd(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1))),
inference(step,[status(thm)],[t700,t12]) ).
cnf(t221249,plain,
rd(rd(X1,X1),X1) = ld(X1,mult(rd(rd(X1,X1),X1),X1)),
inference(step,[status(thm)],[t221248,t654]) ).
cnf(t221250,plain,
rd(rd(X1,X1),X1) = ld(X1,rd(X1,X1)),
inference(step,[status(thm)],[t221249,t8]) ).
cnf(t754,plain,
ld(X1,rd(X1,X1)) = rd(rd(X1,X1),X1),
inference(orient,[status(thm)],[t221250]) ).
cnf(t788,plain,
mult(rd(X1,X1),mult(X1,X1)) = mult(X1,X1),
inference(cp,[status(thm)],[t785,t636]) ).
cnf(t810,plain,
mult(rd(X1,X1),mult(X1,X1)) = mult(X1,X1),
inference(orient,[status(thm)],[t788]) ).
cnf(t818,plain,
rd(X1,X1) = rd(mult(X1,X1),mult(X1,X1)),
inference(cp,[status(thm)],[t10,t810]) ).
cnf(t828,plain,
rd(mult(X1,X1),mult(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t818]) ).
cnf(t837,plain,
rd(rd(mult(X1,X1),mult(X1,X1)),mult(X1,X1)) = ld(mult(X1,X1),rd(X1,X1)),
inference(cp,[status(thm)],[t754,t828]) ).
cnf(t221257,plain,
rd(rd(X1,X1),mult(X1,X1)) = ld(mult(X1,X1),rd(X1,X1)),
inference(step,[status(thm)],[t837,t828]) ).
cnf(t931,plain,
ld(mult(X1,X1),rd(X1,X1)) = rd(rd(X1,X1),mult(X1,X1)),
inference(orient,[status(thm)],[t221257]) ).
cnf(t469,plain,
mult(ld(mult(X1,X2),rd(X3,X2)),X2) = ld(X2,ld(X1,X3)),
inference(cp,[status(thm)],[t458,t8]) ).
cnf(t1374,plain,
mult(ld(mult(X1,X2),rd(X3,X2)),X2) = ld(X2,ld(X1,X3)),
inference(orient,[status(thm)],[t469]) ).
cnf(t1418,plain,
ld(mult(X1,X2),rd(X3,X2)) = rd(ld(X2,ld(X1,X3)),X2),
inference(cp,[status(thm)],[t10,t1374]) ).
cnf(t1433,plain,
ld(mult(X1,X2),rd(X3,X2)) = rd(ld(X2,ld(X1,X3)),X2),
inference(orient,[status(thm)],[t1418]) ).
cnf(t221289,plain,
rd(ld(X1,ld(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
inference(step,[status(thm)],[t931,t1433]) ).
cnf(t221290,plain,
rd(ld(X1,rd(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
inference(step,[status(thm)],[t221289,t616]) ).
cnf(t1483,plain,
rd(ld(X1,rd(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
inference(rw,[status(thm)],[t221290]) ).
cnf(t702,plain,
ld(X1,rd(X1,X2)) = ld(ld(X3,mult(X3,X2)),rd(ld(X1,rd(X1,X2)),ld(X1,rd(X1,X2)))),
inference(cp,[status(thm)],[t697,t216]) ).
cnf(t221285,plain,
ld(X1,rd(X1,X2)) = ld(X2,rd(ld(X1,rd(X1,X2)),ld(X1,rd(X1,X2)))),
inference(step,[status(thm)],[t702,t12]) ).
cnf(t221286,plain,
ld(X1,rd(X1,X2)) = ld(X2,mult(ld(X1,rd(X1,X2)),X2)),
inference(step,[status(thm)],[t221285,t216]) ).
cnf(t221287,plain,
ld(X1,rd(X1,X2)) = ld(X2,rd(X2,X2)),
inference(step,[status(thm)],[t221286,t617]) ).
cnf(t1193,plain,
rd(X1,mult(X1,X1)) = ld(ld(X2,mult(X2,X1)),rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1)))),
inference(cp,[status(thm)],[t697,t1178]) ).
cnf(t221270,plain,
rd(X1,mult(X1,X1)) = ld(X1,rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1)))),
inference(step,[status(thm)],[t1193,t12]) ).
cnf(t221271,plain,
rd(X1,mult(X1,X1)) = ld(X1,mult(rd(X1,mult(X1,X1)),X1)),
inference(step,[status(thm)],[t221270,t1178]) ).
cnf(t1098,plain,
rd(X1,X1) = mult(rd(X1,mult(X1,X1)),X1),
inference(cp,[status(thm)],[t8,t1091]) ).
cnf(t1116,plain,
mult(rd(X1,mult(X1,X1)),X1) = rd(X1,X1),
inference(orient,[status(thm)],[t1098]) ).
cnf(t221272,plain,
rd(X1,mult(X1,X1)) = ld(X1,rd(X1,X1)),
inference(step,[status(thm)],[t221271,t1116]) ).
cnf(t1200,plain,
ld(X1,rd(X1,X1)) = rd(X1,mult(X1,X1)),
inference(orient,[status(thm)],[t221272]) ).
cnf(t221288,plain,
ld(X1,rd(X1,X2)) = rd(X2,mult(X2,X2)),
inference(step,[status(thm)],[t221287,t1200]) ).
cnf(t1336,plain,
ld(X1,rd(X1,X2)) = rd(X2,mult(X2,X2)),
inference(orient,[status(thm)],[t221288]) ).
cnf(t221291,plain,
rd(rd(X1,mult(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
inference(step,[status(thm)],[t1483,t1336]) ).
cnf(t1484,plain,
rd(rd(X1,mult(X1,X1)),X1) = rd(rd(X1,X1),mult(X1,X1)),
inference(orient,[status(thm)],[t221291]) ).
cnf(t221294,plain,
rd(X1,mult(X1,mult(X1,X1))) = rd(rd(X1,X1),mult(X1,X1)),
inference(step,[status(thm)],[t1557,t1484]) ).
cnf(t1609,plain,
rd(rd(X1,X1),mult(X1,X1)) = rd(X1,mult(X1,mult(X1,X1))),
inference(orient,[status(thm)],[t221294]) ).
cnf(t222200,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)],[t222199,t1609]) ).
cnf(t3907,plain,
ld(rd(ld(X1,rd(X1,X2)),X2),X3) = mult(X2,mult(X2,mult(rd(X3,X2),X2))),
inference(cp,[status(thm)],[t479,t3823]) ).
cnf(t221380,plain,
ld(rd(ld(X1,rd(X1,X2)),X2),X3) = mult(X2,mult(X2,X3)),
inference(step,[status(thm)],[t3907,t8]) ).
cnf(t4118,plain,
ld(rd(ld(X1,rd(X1,X2)),X2),X3) = mult(X2,mult(X2,X3)),
inference(orient,[status(thm)],[t221380]) ).
cnf(t4123,plain,
mult(X1,mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3))) = X3,
inference(cp,[status(thm)],[t4118,t12]) ).
cnf(t19796,plain,
mult(X1,mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3))) = X3,
inference(orient,[status(thm)],[t4123]) ).
cnf(t19899,plain,
mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3)) = ld(X1,X3),
inference(cp,[status(thm)],[t12,t19796]) ).
cnf(t19972,plain,
mult(X1,mult(rd(ld(X2,rd(X2,X1)),X1),X3)) = ld(X1,X3),
inference(orient,[status(thm)],[t19899]) ).
cnf(t20075,plain,
mult(rd(ld(X1,rd(X1,X2)),X2),X3) = ld(X2,ld(X2,X3)),
inference(cp,[status(thm)],[t12,t19972]) ).
cnf(t20164,plain,
mult(rd(ld(X1,rd(X1,X2)),X2),X3) = ld(X2,ld(X2,X3)),
inference(orient,[status(thm)],[t20075]) ).
cnf(t20264,plain,
rd(ld(X1,ld(rd(ld(X2,rd(X2,X3)),X3),Y3)),X1) = ld(ld(X3,ld(X3,X1)),rd(Y3,X1)),
inference(cp,[status(thm)],[t1433,t20164]) ).
cnf(t221552,plain,
rd(ld(X1,mult(X3,mult(X3,Y3))),X1) = ld(ld(X3,ld(X3,X1)),rd(Y3,X1)),
inference(step,[status(thm)],[t20264,t4118]) ).
cnf(t21507,plain,
ld(ld(X1,ld(X1,X2)),rd(X3,X2)) = rd(ld(X2,mult(X1,mult(X1,X3))),X2),
inference(orient,[status(thm)],[t221552]) ).
cnf(t21655,plain,
ld(X1,ld(X1,X2)) = rd(rd(X3,X2),rd(ld(X2,mult(X1,mult(X1,X3))),X2)),
inference(cp,[status(thm)],[t23,t21507]) ).
cnf(t2911,plain,
ld(mult(rd(mult(X1,X2),X3),X2),X1) = rd(ld(X2,X3),X2),
inference(cp,[status(thm)],[t10,t2858]) ).
cnf(t3006,plain,
ld(mult(rd(mult(X1,X2),X3),X2),X1) = rd(ld(X2,X3),X2),
inference(orient,[status(thm)],[t2911]) ).
cnf(t3051,plain,
mult(rd(mult(X1,X2),X3),X2) = rd(X1,rd(ld(X2,X3),X2)),
inference(cp,[status(thm)],[t23,t3006]) ).
cnf(t3107,plain,
mult(rd(mult(X1,X2),X3),X2) = rd(X1,rd(ld(X2,X3),X2)),
inference(orient,[status(thm)],[t3051]) ).
cnf(t3143,plain,
rd(rd(X1,X2),rd(ld(X2,X3),X2)) = mult(rd(X1,X3),X2),
inference(cp,[status(thm)],[t3107,t8]) ).
cnf(t3295,plain,
rd(rd(X1,X2),rd(ld(X2,X3),X2)) = mult(rd(X1,X3),X2),
inference(orient,[status(thm)],[t3143]) ).
cnf(t221553,plain,
ld(X1,ld(X1,X2)) = mult(rd(X3,mult(X1,mult(X1,X3))),X2),
inference(step,[status(thm)],[t21655,t3295]) ).
cnf(t21708,plain,
mult(rd(X1,mult(X2,mult(X2,X1))),X3) = ld(X2,ld(X2,X3)),
inference(orient,[status(thm)],[t221553]) ).
cnf(t222201,plain,
ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(rd(X1,X1),ld(X1,ld(X1,X2))),
inference(step,[status(thm)],[t222200,t21708]) ).
cnf(t108292,plain,
ld(rd(X1,X1),ld(X1,ld(X1,X2))) = ld(X1,rd(ld(X1,mult(X2,X1)),X1)),
inference(orient,[status(thm)],[t222201]) ).
cnf(t1566,plain,
rd(X1,mult(ld(X2,X1),mult(X3,ld(X2,X1)))) = rd(rd(X2,X3),ld(X2,X1)),
inference(cp,[status(thm)],[t1552,t23]) ).
cnf(t221736,plain,
rd(X1,mult(ld(X2,X1),rd(X3,ld(X1,X2)))) = rd(rd(X2,X3),ld(X2,X1)),
inference(step,[status(thm)],[t1566,t196]) ).
cnf(t3826,plain,
mult(ld(X1,X2),mult(X3,ld(X1,X2))) = rd(ld(ld(Y3,rd(Y3,ld(X1,X2))),X3),ld(X2,X1)),
inference(cp,[status(thm)],[t3823,t196]) ).
cnf(t221466,plain,
mult(ld(X1,X2),rd(X3,ld(X2,X1))) = rd(ld(ld(Y3,rd(Y3,ld(X1,X2))),X3),ld(X2,X1)),
inference(step,[status(thm)],[t3826,t196]) ).
cnf(t221467,plain,
mult(ld(X1,X2),rd(X3,ld(X2,X1))) = rd(ld(ld(X2,X1),X3),ld(X2,X1)),
inference(step,[status(thm)],[t221466,t225]) ).
cnf(t13661,plain,
mult(ld(X1,X2),rd(X3,ld(X2,X1))) = rd(ld(ld(X2,X1),X3),ld(X2,X1)),
inference(orient,[status(thm)],[t221467]) ).
cnf(t221737,plain,
rd(X1,rd(ld(ld(X1,X2),X3),ld(X1,X2))) = rd(rd(X2,X3),ld(X2,X1)),
inference(step,[status(thm)],[t221736,t13661]) ).
cnf(t45506,plain,
rd(X1,rd(ld(ld(X1,X2),X3),ld(X1,X2))) = rd(rd(X2,X3),ld(X2,X1)),
inference(orient,[status(thm)],[t221737]) ).
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(t221669,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(t221670,plain,
rd(ld(ld(X2,X1),ld(X2,X3)),ld(X2,X1)) = ld(X1,mult(X3,ld(X1,X2))),
inference(step,[status(thm)],[t221669,t13661]) ).
cnf(t221671,plain,
rd(ld(ld(X2,X1),ld(X2,X3)),ld(X2,X1)) = ld(X1,rd(X3,ld(X2,X1))),
inference(step,[status(thm)],[t221670,t196]) ).
cnf(t35133,plain,
rd(ld(ld(X1,X2),ld(X1,X3)),ld(X1,X2)) = ld(X2,rd(X3,ld(X1,X2))),
inference(orient,[status(thm)],[t221671]) ).
cnf(t45508,plain,
rd(rd(X1,ld(X2,X3)),ld(X1,X2)) = rd(X2,ld(X1,rd(X3,ld(X2,X1)))),
inference(cp,[status(thm)],[t45506,t35133]) ).
cnf(t45836,plain,
rd(rd(X1,ld(X2,X3)),ld(X1,X2)) = rd(X2,ld(X1,rd(X3,ld(X2,X1)))),
inference(orient,[status(thm)],[t45508]) ).
cnf(t597,plain,
rd(mult(X1,X2),ld(X2,X2)) = rd(mult(X1,mult(X2,X2)),X2),
inference(cp,[status(thm)],[t592,t56]) ).
cnf(t221251,plain,
rd(mult(X1,X2),rd(X2,X2)) = rd(mult(X1,mult(X2,X2)),X2),
inference(step,[status(thm)],[t597,t616]) ).
cnf(t760,plain,
rd(mult(X1,mult(X2,X2)),X2) = rd(mult(X1,X2),rd(X2,X2)),
inference(orient,[status(thm)],[t221251]) ).
cnf(t770,plain,
mult(X1,mult(X2,X2)) = mult(rd(mult(X1,X2),rd(X2,X2)),X2),
inference(cp,[status(thm)],[t8,t760]) ).
cnf(t221301,plain,
mult(X1,mult(X2,X2)) = rd(mult(mult(X1,X2),X2),rd(X2,X2)),
inference(step,[status(thm)],[t770,t903]) ).
cnf(t1728,plain,
rd(mult(mult(X1,X2),X2),rd(X2,X2)) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t221301]) ).
cnf(t1761,plain,
rd(mult(mult(mult(X1,X2),X2),X2),rd(X2,X2)) = mult(mult(X1,mult(X2,X2)),X2),
inference(cp,[status(thm)],[t903,t1728]) ).
cnf(t221302,plain,
mult(mult(X1,X2),mult(X2,X2)) = mult(mult(X1,mult(X2,X2)),X2),
inference(step,[status(thm)],[t1761,t1728]) ).
cnf(t1776,plain,
mult(mult(X1,mult(X2,X2)),X2) = mult(mult(X1,X2),mult(X2,X2)),
inference(orient,[status(thm)],[t221302]) ).
cnf(t622,plain,
mult(ld(X1,rd(rd(X1,X2),X2)),X2) = ld(X2,rd(rd(X1,X2),rd(X1,X2))),
inference(cp,[status(thm)],[t506,t616]) ).
cnf(t9075,plain,
ld(X1,rd(rd(X2,X1),rd(X2,X1))) = mult(ld(X2,rd(rd(X2,X1),X1)),X1),
inference(orient,[status(thm)],[t622]) ).
cnf(t9114,plain,
mult(ld(rd(X1,rd(X2,X2)),rd(rd(rd(X1,rd(X2,X2)),rd(X2,X2)),rd(X2,X2))),rd(X2,X2)) = ld(rd(X2,X2),rd(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2)))),
inference(cp,[status(thm)],[t9075,t687]) ).
cnf(t221425,plain,
rd(ld(rd(X1,rd(X2,X2)),rd(rd(rd(X1,rd(X2,X2)),rd(X2,X2)),rd(X2,X2))),rd(X2,X2)) = ld(rd(X2,X2),rd(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2)))),
inference(step,[status(thm)],[t9114,t619]) ).
cnf(t221426,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)],[t221425,t1552]) ).
cnf(t615,plain,
ld(X1,rd(X1,rd(X2,X2))) = ld(rd(X3,ld(X2,X2)),X3),
inference(cp,[status(thm)],[t350,t592]) ).
cnf(t221245,plain,
ld(X1,rd(X1,rd(X2,X2))) = ld(X2,X2),
inference(step,[status(thm)],[t615,t24]) ).
cnf(t221246,plain,
ld(X1,rd(X1,rd(X2,X2))) = rd(X2,X2),
inference(step,[status(thm)],[t221245,t616]) ).
cnf(t646,plain,
ld(X1,rd(X1,rd(X2,X2))) = rd(X2,X2),
inference(orient,[status(thm)],[t221246]) ).
cnf(t4134,plain,
mult(rd(X1,X1),mult(rd(X1,X1),X2)) = ld(rd(rd(X1,X1),rd(X1,X1)),X2),
inference(cp,[status(thm)],[t4118,t646]) ).
cnf(t221382,plain,
mult(rd(X1,X1),mult(rd(X1,X1),X2)) = ld(rd(X1,X1),X2),
inference(step,[status(thm)],[t4134,t992]) ).
cnf(t4363,plain,
mult(rd(X1,X1),mult(rd(X1,X1),X2)) = ld(rd(X1,X1),X2),
inference(orient,[status(thm)],[t221382]) ).
cnf(t221427,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)],[t221426,t4363]) ).
cnf(t221428,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)],[t221427,t616]) ).
cnf(t221429,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)],[t221428,t992]) ).
cnf(t221430,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)],[t221429,t616]) ).
cnf(t221431,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)],[t221430,t1552]) ).
cnf(t221432,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)],[t221431,t8]) ).
cnf(t221433,plain,
rd(X1,mult(rd(X2,X2),X1)) = ld(rd(X2,X2),rd(X1,X1)),
inference(step,[status(thm)],[t221432,t687]) ).
cnf(t9203,plain,
ld(rd(X1,X1),rd(X2,X2)) = rd(X2,mult(rd(X1,X1),X2)),
inference(orient,[status(thm)],[t221433]) ).
cnf(t9241,plain,
mult(ld(X1,rd(rd(X2,X2),X1)),X1) = ld(X1,rd(X2,mult(rd(X1,X1),X2))),
inference(cp,[status(thm)],[t506,t9203]) ).
cnf(t15280,plain,
ld(X1,rd(X2,mult(rd(X1,X1),X2))) = mult(ld(X1,rd(rd(X2,X2),X1)),X1),
inference(orient,[status(thm)],[t9241]) ).
cnf(t20197,plain,
ld(mult(rd(X1,X1),X1),ld(mult(rd(X1,X1),X1),X2)) = mult(rd(mult(ld(X1,rd(rd(X1,X1),X1)),X1),mult(rd(X1,X1),X1)),X2),
inference(cp,[status(thm)],[t20164,t15280]) ).
cnf(t221541,plain,
ld(X1,ld(mult(rd(X1,X1),X1),X2)) = mult(rd(mult(ld(X1,rd(rd(X1,X1),X1)),X1),mult(rd(X1,X1),X1)),X2),
inference(step,[status(thm)],[t20197,t8]) ).
cnf(t221542,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)],[t221541,t8]) ).
cnf(t221543,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)],[t221542,t1091]) ).
cnf(t1191,plain,
mult(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))) = ld(ld(X2,mult(X2,X1)),rd(X1,mult(X1,X1))),
inference(cp,[status(thm)],[t1056,t1178]) ).
cnf(t221277,plain,
rd(rd(X1,mult(X1,X1)),X1) = ld(ld(X2,mult(X2,X1)),rd(X1,mult(X1,X1))),
inference(step,[status(thm)],[t1191,t1135]) ).
cnf(t221278,plain,
rd(rd(X1,mult(X1,X1)),X1) = ld(X1,rd(X1,mult(X1,X1))),
inference(step,[status(thm)],[t221277,t12]) ).
cnf(t1278,plain,
ld(X1,rd(X1,mult(X1,X1))) = rd(rd(X1,mult(X1,X1)),X1),
inference(orient,[status(thm)],[t221278]) ).
cnf(t221292,plain,
ld(X1,rd(X1,mult(X1,X1))) = rd(rd(X1,X1),mult(X1,X1)),
inference(step,[status(thm)],[t1278,t1484]) ).
cnf(t1485,plain,
ld(X1,rd(X1,mult(X1,X1))) = rd(rd(X1,X1),mult(X1,X1)),
inference(orient,[status(thm)],[t221292]) ).
cnf(t221295,plain,
ld(X1,rd(X1,mult(X1,X1))) = rd(X1,mult(X1,mult(X1,X1))),
inference(step,[status(thm)],[t1485,t1609]) ).
cnf(t1610,plain,
ld(X1,rd(X1,mult(X1,X1))) = rd(X1,mult(X1,mult(X1,X1))),
inference(orient,[status(thm)],[t221295]) ).
cnf(t221544,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)],[t221543,t1610]) ).
cnf(t221545,plain,
ld(X1,ld(X1,X2)) = mult(rd(rd(rd(X1,X1),X1),mult(rd(X1,X1),X1)),X2),
inference(step,[status(thm)],[t221544,t2570]) ).
cnf(t221546,plain,
ld(X1,ld(X1,X2)) = mult(rd(rd(X1,mult(X1,X1)),mult(rd(X1,X1),X1)),X2),
inference(step,[status(thm)],[t221545,t1091]) ).
cnf(t221547,plain,
ld(X1,ld(X1,X2)) = mult(rd(rd(X1,mult(X1,X1)),X1),X2),
inference(step,[status(thm)],[t221546,t8]) ).
cnf(t221548,plain,
ld(X1,ld(X1,X2)) = mult(rd(rd(X1,X1),mult(X1,X1)),X2),
inference(step,[status(thm)],[t221547,t2384]) ).
cnf(t221549,plain,
ld(X1,ld(X1,X2)) = mult(rd(X1,mult(X1,mult(X1,X1))),X2),
inference(step,[status(thm)],[t221548,t1609]) ).
cnf(t20472,plain,
mult(rd(X1,mult(X1,mult(X1,X1))),X2) = ld(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t221549]) ).
cnf(t838,plain,
mult(X1,X1) = rd(mult(X1,X1),rd(X1,X1)),
inference(cp,[status(thm)],[t636,t828]) ).
cnf(t853,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,X1),
inference(orient,[status(thm)],[t838]) ).
cnf(t3016,plain,
rd(ld(X1,rd(X1,X1)),X1) = ld(mult(mult(X1,X1),X1),X1),
inference(cp,[status(thm)],[t3006,t853]) ).
cnf(t221341,plain,
rd(rd(X1,mult(X1,X1)),X1) = ld(mult(mult(X1,X1),X1),X1),
inference(step,[status(thm)],[t3016,t1336]) ).
cnf(t221342,plain,
rd(rd(X1,X1),mult(X1,X1)) = ld(mult(mult(X1,X1),X1),X1),
inference(step,[status(thm)],[t221341,t2384]) ).
cnf(t221343,plain,
rd(X1,mult(X1,mult(X1,X1))) = ld(mult(mult(X1,X1),X1),X1),
inference(step,[status(thm)],[t221342,t1609]) ).
cnf(t862,plain,
mult(rd(mult(X1,X1),X1),mult(X1,X1)) = mult(mult(X1,X1),X1),
inference(cp,[status(thm)],[t785,t853]) ).
cnf(t221252,plain,
mult(X1,mult(X1,X1)) = mult(mult(X1,X1),X1),
inference(step,[status(thm)],[t862,t10]) ).
cnf(t868,plain,
mult(mult(X1,X1),X1) = mult(X1,mult(X1,X1)),
inference(orient,[status(thm)],[t221252]) ).
cnf(t221344,plain,
rd(X1,mult(X1,mult(X1,X1))) = ld(mult(X1,mult(X1,X1)),X1),
inference(step,[status(thm)],[t221343,t868]) ).
cnf(t221345,plain,
rd(X1,mult(X1,mult(X1,X1))) = ld(true,rd(true,mult(X1,X1))),
inference(step,[status(thm)],[t221344,t350]) ).
cnf(t3057,plain,
rd(X1,mult(X1,mult(X1,X1))) = ld(true,rd(true,mult(X1,X1))),
inference(orient,[status(thm)],[t221345]) ).
cnf(t20502,plain,
ld(X1,ld(X1,X2)) = mult(ld(true,rd(true,mult(X1,X1))),X2),
inference(cp,[status(thm)],[t20472,t3057]) ).
cnf(t20735,plain,
mult(ld(true,rd(true,mult(X1,X1))),X2) = ld(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t20502]) ).
cnf(t20763,plain,
ld(X1,ld(X1,X2)) = mult(ld(X3,rd(X3,mult(X1,X1))),X2),
inference(cp,[status(thm)],[t20735,t391]) ).
cnf(t21003,plain,
mult(ld(X1,rd(X1,mult(X2,X2))),X3) = ld(X2,ld(X2,X3)),
inference(orient,[status(thm)],[t20763]) ).
cnf(t21263,plain,
ld(mult(X1,X1),mult(X2,mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),mult(X1,X1)),
inference(cp,[status(thm)],[t5118,t21003]) ).
cnf(t23109,plain,
ld(mult(X1,X1),mult(X2,mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),mult(X1,X1)),
inference(orient,[status(thm)],[t21263]) ).
cnf(t3972,plain,
rd(ld(X1,mult(mult(mult(X1,X1),mult(X2,mult(X1,X1))),X1)),X1) = mult(mult(X1,X2),mult(X1,X1)),
inference(cp,[status(thm)],[t3971,t25]) ).
cnf(t221769,plain,
rd(ld(X1,mult(X1,mult(X1,mult(mult(X2,mult(X1,X1)),X1)))),X1) = mult(mult(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t3972,t14]) ).
cnf(t21817,plain,
X1 = ld(rd(X2,mult(X3,mult(X3,X2))),ld(X3,ld(X3,X1))),
inference(cp,[status(thm)],[t12,t21708]) ).
cnf(t29041,plain,
ld(rd(X1,mult(X2,mult(X2,X1))),ld(X2,ld(X2,X3))) = X3,
inference(orient,[status(thm)],[t21817]) ).
cnf(t29158,plain,
mult(X1,X2) = ld(rd(X3,mult(X1,mult(X1,X3))),ld(X1,X2)),
inference(cp,[status(thm)],[t29041,t12]) ).
cnf(t29428,plain,
ld(rd(X1,mult(X2,mult(X2,X1))),ld(X2,X3)) = mult(X2,X3),
inference(orient,[status(thm)],[t29158]) ).
cnf(t29537,plain,
mult(X1,mult(X1,X2)) = ld(rd(X3,mult(X1,mult(X1,X3))),X2),
inference(cp,[status(thm)],[t29428,t12]) ).
cnf(t29656,plain,
ld(rd(X1,mult(X2,mult(X2,X1))),X3) = mult(X2,mult(X2,X3)),
inference(orient,[status(thm)],[t29537]) ).
cnf(t29829,plain,
mult(ld(mult(rd(X1,mult(X2,mult(X2,X1))),X3),Y3),X3) = ld(X3,mult(X2,mult(X2,mult(Y3,X3)))),
inference(cp,[status(thm)],[t458,t29656]) ).
cnf(t221627,plain,
mult(ld(ld(X2,ld(X2,X3)),Y3),X3) = ld(X3,mult(X2,mult(X2,mult(Y3,X3)))),
inference(step,[status(thm)],[t29829,t21708]) ).
cnf(t30106,plain,
ld(X1,mult(X2,mult(X2,mult(X3,X1)))) = mult(ld(ld(X2,ld(X2,X1)),X3),X1),
inference(orient,[status(thm)],[t221627]) ).
cnf(t221770,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)],[t221769,t30106]) ).
cnf(t221771,plain,
ld(ld(X1,ld(X1,X1)),mult(X2,mult(X1,X1))) = mult(mult(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t221770,t10]) ).
cnf(t221772,plain,
ld(ld(X1,rd(X1,X1)),mult(X2,mult(X1,X1))) = mult(mult(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t221771,t616]) ).
cnf(t221773,plain,
ld(rd(X1,mult(X1,X1)),mult(X2,mult(X1,X1))) = mult(mult(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t221772,t1336]) ).
cnf(t221774,plain,
rd(mult(X1,mult(mult(X2,mult(X1,X1)),X1)),X1) = mult(mult(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t221773,t2936]) ).
cnf(t221775,plain,
rd(mult(X1,mult(mult(X2,X1),mult(X1,X1))),X1) = mult(mult(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t221774,t1776]) ).
cnf(t54192,plain,
rd(mult(X1,mult(mult(X2,X1),mult(X1,X1))),X1) = mult(mult(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t221775]) ).
cnf(t54285,plain,
mult(mult(X1,rd(X2,X1)),mult(X1,X1)) = rd(mult(X1,mult(X2,mult(X1,X1))),X1),
inference(cp,[status(thm)],[t54192,t8]) ).
cnf(t54494,plain,
mult(mult(X1,rd(X2,X1)),mult(X1,X1)) = rd(mult(X1,mult(X2,mult(X1,X1))),X1),
inference(orient,[status(thm)],[t54285]) ).
cnf(t54636,plain,
mult(ld(X1,ld(X1,mult(X1,rd(X2,X1)))),mult(X1,X1)) = ld(mult(X1,X1),rd(mult(X1,mult(X2,mult(X1,X1))),X1)),
inference(cp,[status(thm)],[t23109,t54494]) ).
cnf(t221777,plain,
mult(ld(X1,rd(X2,X1)),mult(X1,X1)) = ld(mult(X1,X1),rd(mult(X1,mult(X2,mult(X1,X1))),X1)),
inference(step,[status(thm)],[t54636,t12]) ).
cnf(t221778,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)],[t221777,t1433]) ).
cnf(t221779,plain,
mult(ld(X1,rd(X2,X1)),mult(X1,X1)) = rd(ld(X1,mult(X2,mult(X1,X1))),X1),
inference(step,[status(thm)],[t221778,t12]) ).
cnf(t54979,plain,
mult(ld(X1,rd(X2,X1)),mult(X1,X1)) = rd(ld(X1,mult(X2,mult(X1,X1))),X1),
inference(orient,[status(thm)],[t221779]) ).
cnf(t55165,plain,
mult(mult(ld(X1,rd(X2,X1)),X1),mult(X1,X1)) = mult(rd(ld(X1,mult(X2,mult(X1,X1))),X1),X1),
inference(cp,[status(thm)],[t1776,t54979]) ).
cnf(t222024,plain,
mult(mult(ld(X1,rd(X2,X1)),X1),mult(X1,X1)) = ld(X1,mult(X2,mult(X1,X1))),
inference(step,[status(thm)],[t55165,t8]) ).
cnf(t90256,plain,
mult(mult(ld(X1,rd(X2,X1)),X1),mult(X1,X1)) = ld(X1,mult(X2,mult(X1,X1))),
inference(orient,[status(thm)],[t222024]) ).
cnf(t90302,plain,
ld(X1,mult(mult(rd(X1,X1),X2),mult(X1,X1))) = mult(mult(rd(ld(X1,X2),X1),X1),mult(X1,X1)),
inference(cp,[status(thm)],[t90256,t3761]) ).
cnf(t222148,plain,
ld(X1,mult(mult(rd(X1,X1),X2),mult(X1,X1))) = mult(ld(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t90302,t8]) ).
cnf(t103051,plain,
ld(X1,mult(mult(rd(X1,X1),X2),mult(X1,X1))) = mult(ld(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t222148]) ).
cnf(t103062,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = ld(X1,mult(rd(rd(X1,X1),mult(X1,X1)),mult(mult(X1,X1),X2))),
inference(cp,[status(thm)],[t103051,t34]) ).
cnf(t2962,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = ld(mult(X1,X1),rd(mult(X1,mult(X2,X1)),X1)),
inference(cp,[status(thm)],[t506,t2936]) ).
cnf(t221754,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = rd(ld(X1,ld(X1,mult(X1,mult(X2,X1)))),X1),
inference(step,[status(thm)],[t2962,t1433]) ).
cnf(t20272,plain,
mult(rd(ld(X1,rd(X1,X2)),X2),mult(X3,mult(Y3,X3))) = mult(mult(ld(X2,ld(X2,X3)),Y3),X3),
inference(cp,[status(thm)],[t14,t20164]) ).
cnf(t221557,plain,
ld(X2,ld(X2,mult(X3,mult(Y3,X3)))) = mult(mult(ld(X2,ld(X2,X3)),Y3),X3),
inference(step,[status(thm)],[t20272,t20164]) ).
cnf(t22235,plain,
ld(X1,ld(X1,mult(X2,mult(X3,X2)))) = mult(mult(ld(X1,ld(X1,X2)),X3),X2),
inference(orient,[status(thm)],[t221557]) ).
cnf(t221755,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)],[t221754,t22235]) ).
cnf(t221756,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = mult(ld(X1,ld(X1,X1)),X2),
inference(step,[status(thm)],[t221755,t10]) ).
cnf(t221757,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = mult(ld(X1,rd(X1,X1)),X2),
inference(step,[status(thm)],[t221756,t616]) ).
cnf(t221758,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = mult(rd(X1,mult(X1,X1)),X2),
inference(step,[status(thm)],[t221757,t1336]) ).
cnf(t221759,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = rd(ld(X1,mult(X2,X1)),X1),
inference(step,[status(thm)],[t221758,t3971]) ).
cnf(t50597,plain,
mult(ld(X1,rd(X2,mult(X1,X1))),mult(X1,X1)) = rd(ld(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t221759]) ).
cnf(t222278,plain,
rd(ld(X1,mult(X2,X1)),X1) = ld(X1,mult(rd(rd(X1,X1),mult(X1,X1)),mult(mult(X1,X1),X2))),
inference(step,[status(thm)],[t103062,t50597]) ).
cnf(t222279,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)],[t222278,t1609]) ).
cnf(t222280,plain,
rd(ld(X1,mult(X2,X1)),X1) = ld(X1,ld(X1,ld(X1,mult(mult(X1,X1),X2)))),
inference(step,[status(thm)],[t222279,t21708]) ).
cnf(t116973,plain,
ld(X1,ld(X1,ld(X1,mult(mult(X1,X1),X2)))) = rd(ld(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t222280]) ).
cnf(t223,plain,
mult(rd(X1,ld(X2,rd(X2,X3))),mult(ld(X2,rd(X2,X3)),Y3)) = mult(mult(X1,mult(Y3,X3)),ld(X2,rd(X2,X3))),
inference(cp,[status(thm)],[t34,t216]) ).
cnf(t221678,plain,
mult(mult(X1,X3),mult(ld(X2,rd(X2,X3)),Y3)) = mult(mult(X1,mult(Y3,X3)),ld(X2,rd(X2,X3))),
inference(step,[status(thm)],[t223,t216]) ).
cnf(t221679,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)],[t221678,t196]) ).
cnf(t221680,plain,
mult(mult(X1,X3),mult(ld(X2,rd(X2,X3)),Y3)) = rd(mult(X1,mult(Y3,X3)),X3),
inference(step,[status(thm)],[t221679,t24]) ).
cnf(t36685,plain,
mult(mult(X1,X2),mult(ld(X3,rd(X3,X2)),Y3)) = rd(mult(X1,mult(Y3,X2)),X2),
inference(orient,[status(thm)],[t221680]) ).
cnf(t117002,plain,
rd(ld(X1,mult(mult(ld(X2,rd(X2,X1)),X3),X1)),X1) = ld(X1,ld(X1,ld(X1,rd(mult(X1,mult(X3,X1)),X1)))),
inference(cp,[status(thm)],[t116973,t36685]) ).
cnf(t222281,plain,
rd(ld(X1,ld(X1,mult(X3,X1))),X1) = ld(X1,ld(X1,ld(X1,rd(mult(X1,mult(X3,X1)),X1)))),
inference(step,[status(thm)],[t117002,t5118]) ).
cnf(t222282,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)],[t222281,t458]) ).
cnf(t222283,plain,
ld(mult(X1,X1),X3) = ld(X1,ld(X1,ld(X1,rd(mult(X1,mult(X3,X1)),X1)))),
inference(step,[status(thm)],[t222282,t10]) ).
cnf(t21802,plain,
ld(rd(X1,X2),ld(rd(X1,X2),X3)) = mult(rd(X2,mult(rd(X1,X2),X1)),X3),
inference(cp,[status(thm)],[t21708,t8]) ).
cnf(t23534,plain,
ld(rd(X1,X2),ld(rd(X1,X2),X3)) = mult(rd(X2,mult(rd(X1,X2),X1)),X3),
inference(orient,[status(thm)],[t21802]) ).
cnf(t105558,plain,
mult(rd(X1,mult(rd(X1,X1),X1)),ld(X1,mult(X2,X1))) = ld(rd(X1,X1),ld(X1,mult(mult(rd(X1,X1),X2),X1))),
inference(cp,[status(thm)],[t23534,t105369]) ).
cnf(t222173,plain,
rd(rd(X1,mult(rd(X1,X1),X1)),ld(mult(X2,X1),X1)) = ld(rd(X1,X1),ld(X1,mult(mult(rd(X1,X1),X2),X1))),
inference(step,[status(thm)],[t105558,t196]) ).
cnf(t222174,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)],[t222173,t8]) ).
cnf(t222175,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)],[t222174,t105369]) ).
cnf(t222176,plain,
rd(rd(X1,X1),ld(mult(X2,X1),X1)) = ld(X1,mult(ld(rd(X1,X1),X2),X1)),
inference(step,[status(thm)],[t222175,t4363]) ).
cnf(t105963,plain,
ld(X1,mult(ld(rd(X1,X1),X2),X1)) = rd(rd(X1,X1),ld(mult(X2,X1),X1)),
inference(orient,[status(thm)],[t222176]) ).
cnf(t1448,plain,
rd(ld(X1,ld(ld(X2,rd(X2,X1)),X3)),X1) = ld(rd(X1,X1),rd(X3,X1)),
inference(cp,[status(thm)],[t1433,t617]) ).
cnf(t42631,plain,
rd(ld(X1,ld(ld(X2,rd(X2,X1)),X3)),X1) = ld(rd(X1,X1),rd(X3,X1)),
inference(orient,[status(thm)],[t1448]) ).
cnf(t4650,plain,
ld(ld(X1,rd(X1,X2)),rd(X1,X2)) = rd(mult(X2,X1),ld(rd(X1,X2),X1)),
inference(cp,[status(thm)],[t4628,t24]) ).
cnf(t221387,plain,
ld(ld(X1,rd(X1,X2)),rd(X1,X2)) = rd(mult(X2,X1),X2),
inference(step,[status(thm)],[t4650,t24]) ).
cnf(t4806,plain,
ld(ld(X1,rd(X1,X2)),rd(X1,X2)) = rd(mult(X2,X1),X2),
inference(orient,[status(thm)],[t221387]) ).
cnf(t4815,plain,
rd(mult(X1,X2),X1) = ld(ld(X3,rd(X3,X1)),rd(X2,X1)),
inference(cp,[status(thm)],[t4806,t391]) ).
cnf(t5023,plain,
ld(ld(X1,rd(X1,X2)),rd(X3,X2)) = rd(mult(X2,X3),X2),
inference(orient,[status(thm)],[t4815]) ).
cnf(t42642,plain,
ld(rd(X1,X1),rd(rd(X2,X1),X1)) = rd(ld(X1,rd(mult(X1,X2),X1)),X1),
inference(cp,[status(thm)],[t42631,t5023]) ).
cnf(t42907,plain,
ld(rd(X1,X1),rd(rd(X2,X1),X1)) = rd(ld(X1,rd(mult(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t42642]) ).
cnf(t106019,plain,
rd(rd(X1,X1),ld(mult(rd(rd(X2,X1),X1),X1),X1)) = ld(X1,mult(rd(ld(X1,rd(mult(X1,X2),X1)),X1),X1)),
inference(cp,[status(thm)],[t105963,t42907]) ).
cnf(t222187,plain,
rd(rd(X1,X1),ld(rd(X2,X1),X1)) = ld(X1,mult(rd(ld(X1,rd(mult(X1,X2),X1)),X1),X1)),
inference(step,[status(thm)],[t106019,t8]) ).
cnf(t222188,plain,
rd(rd(X1,X1),ld(rd(X2,X1),X1)) = ld(X1,ld(X1,rd(mult(X1,X2),X1))),
inference(step,[status(thm)],[t222187,t8]) ).
cnf(t107737,plain,
ld(X1,ld(X1,rd(mult(X1,X2),X1))) = rd(rd(X1,X1),ld(rd(X2,X1),X1)),
inference(orient,[status(thm)],[t222188]) ).
cnf(t222284,plain,
ld(mult(X1,X1),X3) = ld(X1,rd(rd(X1,X1),ld(rd(mult(X3,X1),X1),X1))),
inference(step,[status(thm)],[t222283,t107737]) ).
cnf(t222285,plain,
ld(mult(X1,X1),X3) = ld(X1,rd(rd(X1,X1),ld(X3,X1))),
inference(step,[status(thm)],[t222284,t10]) ).
cnf(t117259,plain,
ld(X1,rd(rd(X1,X1),ld(X2,X1))) = ld(mult(X1,X1),X2),
inference(orient,[status(thm)],[t222285]) ).
cnf(t117433,plain,
ld(mult(X1,X1),rd(X1,X2)) = ld(X1,rd(rd(X1,X1),X2)),
inference(cp,[status(thm)],[t117259,t24]) ).
cnf(t117610,plain,
ld(mult(X1,X1),rd(X1,X2)) = ld(X1,rd(rd(X1,X1),X2)),
inference(orient,[status(thm)],[t117433]) ).
cnf(t117799,plain,
mult(X1,X1) = rd(rd(X1,X2),ld(X1,rd(rd(X1,X1),X2))),
inference(cp,[status(thm)],[t23,t117610]) ).
cnf(t119768,plain,
rd(rd(X1,X2),ld(X1,rd(rd(X1,X1),X2))) = mult(X1,X1),
inference(orient,[status(thm)],[t117799]) ).
cnf(t120027,plain,
rd(X1,ld(rd(X1,X2),rd(rd(rd(X1,X1),X2),ld(X1,rd(X1,X2))))) = rd(mult(X1,X1),ld(rd(X1,X2),X1)),
inference(cp,[status(thm)],[t45836,t119768]) ).
cnf(t222295,plain,
rd(X1,ld(rd(X1,X2),mult(rd(rd(X1,X1),X2),X2))) = rd(mult(X1,X1),ld(rd(X1,X2),X1)),
inference(step,[status(thm)],[t120027,t216]) ).
cnf(t222296,plain,
rd(X1,ld(rd(X1,X2),rd(X1,X1))) = rd(mult(X1,X1),ld(rd(X1,X2),X1)),
inference(step,[status(thm)],[t222295,t8]) ).
cnf(t222297,plain,
rd(X1,ld(rd(X1,X2),rd(X1,X1))) = rd(mult(X1,X1),X2),
inference(step,[status(thm)],[t222296,t24]) ).
cnf(t120155,plain,
rd(X1,ld(rd(X1,X2),rd(X1,X1))) = rd(mult(X1,X1),X2),
inference(orient,[status(thm)],[t222297]) ).
cnf(t120435,plain,
ld(rd(X1,X1),rd(X1,X2)) = ld(X1,rd(mult(X1,X1),X2)),
inference(cp,[status(thm)],[t225,t120155]) ).
cnf(t121812,plain,
ld(rd(X1,X1),rd(X1,X2)) = ld(X1,rd(mult(X1,X1),X2)),
inference(orient,[status(thm)],[t120435]) ).
cnf(t121853,plain,
ld(X1,rd(mult(X1,X1),rd(X2,mult(X2,X2)))) = ld(rd(X1,X1),mult(X1,X2)),
inference(cp,[status(thm)],[t121812,t1178]) ).
cnf(t222305,plain,
ld(X1,mult(mult(X1,X1),X2)) = ld(rd(X1,X1),mult(X1,X2)),
inference(step,[status(thm)],[t121853,t1178]) ).
cnf(t122364,plain,
ld(rd(X1,X1),mult(X1,X2)) = ld(X1,mult(mult(X1,X1),X2)),
inference(orient,[status(thm)],[t222305]) ).
cnf(t122549,plain,
mult(ld(X1,rd(mult(X1,X2),X1)),X1) = ld(X1,ld(X1,mult(mult(X1,X1),X2))),
inference(cp,[status(thm)],[t506,t122364]) ).
cnf(t128441,plain,
ld(X1,ld(X1,mult(mult(X1,X1),X2))) = mult(ld(X1,rd(mult(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t122549]) ).
cnf(t128541,plain,
ld(X1,rd(ld(X1,mult(mult(mult(X1,X1),X2),X1)),X1)) = ld(rd(X1,X1),mult(ld(X1,rd(mult(X1,X2),X1)),X1)),
inference(cp,[status(thm)],[t108292,t128441]) ).
cnf(t222328,plain,
ld(X1,rd(ld(X1,mult(X1,mult(X1,mult(X2,X1)))),X1)) = ld(rd(X1,X1),mult(ld(X1,rd(mult(X1,X2),X1)),X1)),
inference(step,[status(thm)],[t128541,t14]) ).
cnf(t222329,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)],[t222328,t30106]) ).
cnf(t222330,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)],[t222329,t10]) ).
cnf(t222331,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)],[t222330,t616]) ).
cnf(t222332,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)],[t222331,t1336]) ).
cnf(t222333,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)],[t222332,t2936]) ).
cnf(t1102,plain,
mult(ld(rd(X1,X1),rd(X2,X1)),X1) = ld(X1,ld(rd(X1,mult(X1,X1)),X2)),
inference(cp,[status(thm)],[t506,t1091]) ).
cnf(t221435,plain,
mult(ld(rd(X1,X1),rd(X2,X1)),X1) = ld(X1,rd(mult(X1,mult(X2,X1)),X1)),
inference(step,[status(thm)],[t1102,t2936]) ).
cnf(t9977,plain,
ld(X1,rd(mult(X1,mult(X2,X1)),X1)) = mult(ld(rd(X1,X1),rd(X2,X1)),X1),
inference(orient,[status(thm)],[t221435]) ).
cnf(t222334,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)],[t222333,t9977]) ).
cnf(t222335,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)],[t222334,t83]) ).
cnf(t117871,plain,
ld(rd(X1,X2),mult(X1,X1)) = ld(X3,rd(X3,ld(X1,rd(rd(X1,X1),X2)))),
inference(cp,[status(thm)],[t225,t117610]) ).
cnf(t222287,plain,
ld(rd(X1,X2),mult(X1,X1)) = ld(rd(rd(X1,X1),X2),X1),
inference(step,[status(thm)],[t117871,t225]) ).
cnf(t118249,plain,
ld(rd(rd(X1,X1),X2),X1) = ld(rd(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t222287]) ).
cnf(t118323,plain,
rd(rd(X1,X1),X2) = rd(X1,ld(rd(X1,X2),mult(X1,X1))),
inference(cp,[status(thm)],[t23,t118249]) ).
cnf(t118707,plain,
rd(X1,ld(rd(X1,X2),mult(X1,X1))) = rd(rd(X1,X1),X2),
inference(orient,[status(thm)],[t118323]) ).
cnf(t118732,plain,
rd(rd(X1,X1),ld(X2,X1)) = rd(X1,ld(X2,mult(X1,X1))),
inference(cp,[status(thm)],[t118707,t23]) ).
cnf(t119069,plain,
rd(rd(X1,X1),ld(X2,X1)) = rd(X1,ld(X2,mult(X1,X1))),
inference(orient,[status(thm)],[t118732]) ).
cnf(t222291,plain,
ld(X1,ld(X1,rd(mult(X1,X2),X1))) = rd(X1,ld(rd(X2,X1),mult(X1,X1))),
inference(step,[status(thm)],[t107737,t119069]) ).
cnf(t222292,plain,
ld(X1,ld(X1,rd(mult(X1,X2),X1))) = rd(X1,mult(X1,mult(ld(X2,X1),X1))),
inference(step,[status(thm)],[t222291,t83]) ).
cnf(t119072,plain,
ld(X1,ld(X1,rd(mult(X1,X2),X1))) = rd(X1,mult(X1,mult(ld(X2,X1),X1))),
inference(orient,[status(thm)],[t222292]) ).
cnf(t222336,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)],[t222335,t119072]) ).
cnf(t222337,plain,
mult(ld(rd(X1,X1),rd(X2,X1)),X1) = mult(X1,rd(rd(X1,X1),ld(X2,X1))),
inference(step,[status(thm)],[t222336,t2570]) ).
cnf(t222338,plain,
mult(ld(rd(X1,X1),rd(X2,X1)),X1) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
inference(step,[status(thm)],[t222337,t119069]) ).
cnf(t129505,plain,
mult(ld(rd(X1,X1),rd(X2,X1)),X1) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
inference(orient,[status(thm)],[t222338]) ).
cnf(t129712,plain,
mult(X1,rd(X1,ld(mult(X2,X1),mult(X1,X1)))) = mult(ld(rd(X1,X1),X2),X1),
inference(cp,[status(thm)],[t129505,t10]) ).
cnf(t160278,plain,
mult(X1,rd(X1,ld(mult(X2,X1),mult(X1,X1)))) = mult(ld(rd(X1,X1),X2),X1),
inference(orient,[status(thm)],[t129712]) ).
cnf(t1095,plain,
mult(X1,mult(ld(rd(X1,X1),X2),X1)) = ld(rd(X1,mult(X1,X1)),mult(X2,X1)),
inference(cp,[status(thm)],[t83,t1091]) ).
cnf(t221434,plain,
mult(X1,mult(ld(rd(X1,X1),X2),X1)) = rd(mult(X1,mult(mult(X2,X1),X1)),X1),
inference(step,[status(thm)],[t1095,t2936]) ).
cnf(t9877,plain,
mult(X1,mult(ld(rd(X1,X1),X2),X1)) = rd(mult(X1,mult(mult(X2,X1),X1)),X1),
inference(orient,[status(thm)],[t221434]) ).
cnf(t105744,plain,
rd(mult(X1,mult(rd(X1,X1),rd(X2,mult(X2,X2)))),X1) = ld(rd(X1,X1),rd(rd(X1,X2),X1)),
inference(cp,[status(thm)],[t105665,t1135]) ).
cnf(t222179,plain,
rd(mult(X1,rd(rd(X1,X1),X2)),X1) = ld(rd(X1,X1),rd(rd(X1,X2),X1)),
inference(step,[status(thm)],[t105744,t1135]) ).
cnf(t106782,plain,
ld(rd(X1,X1),rd(rd(X1,X2),X1)) = rd(mult(X1,rd(rd(X1,X1),X2)),X1),
inference(orient,[status(thm)],[t222179]) ).
cnf(t107118,plain,
rd(mult(X1,mult(mult(rd(rd(X1,X2),X1),X1),X1)),X1) = mult(X1,mult(rd(mult(X1,rd(rd(X1,X1),X2)),X1),X1)),
inference(cp,[status(thm)],[t9877,t106782]) ).
cnf(t222203,plain,
rd(mult(X1,mult(rd(X1,X2),X1)),X1) = mult(X1,mult(rd(mult(X1,rd(rd(X1,X1),X2)),X1),X1)),
inference(step,[status(thm)],[t107118,t8]) ).
cnf(t222204,plain,
rd(mult(X1,mult(rd(X1,X2),X1)),X1) = mult(X1,mult(X1,rd(rd(X1,X1),X2))),
inference(step,[status(thm)],[t222203,t8]) ).
cnf(t108859,plain,
mult(X1,mult(X1,rd(rd(X1,X1),X2))) = rd(mult(X1,mult(rd(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t222204]) ).
cnf(t108928,plain,
rd(mult(rd(X1,mult(X1,X1)),mult(rd(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1)))),rd(X1,mult(X1,X1))) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),rd(mult(rd(X1,mult(X1,X1)),X1),X2))),
inference(cp,[status(thm)],[t108859,t1178]) ).
cnf(t222233,plain,
mult(mult(rd(X1,mult(X1,X1)),mult(rd(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1)))),X1) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),rd(mult(rd(X1,mult(X1,X1)),X1),X2))),
inference(step,[status(thm)],[t108928,t1178]) ).
cnf(t222234,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)],[t222233,t3971]) ).
cnf(t222235,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)],[t222234,t8]) ).
cnf(t222236,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)],[t222235,t1135]) ).
cnf(t1569,plain,
rd(rd(X1,X1),mult(X1,mult(X2,X1))) = rd(rd(rd(X1,mult(X1,X1)),X2),X1),
inference(cp,[status(thm)],[t1552,t1091]) ).
cnf(t11286,plain,
rd(rd(rd(X1,mult(X1,X1)),X2),X1) = rd(rd(X1,X1),mult(X1,mult(X2,X1))),
inference(orient,[status(thm)],[t1569]) ).
cnf(t222237,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)],[t222236,t11286]) ).
cnf(t222238,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)],[t222237,t2570]) ).
cnf(t222239,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)],[t222238,t1091]) ).
cnf(t222240,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)],[t222239,t3971]) ).
cnf(t222241,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)],[t222240,t3971]) ).
cnf(t222242,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)],[t222241,t8]) ).
cnf(t222243,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)],[t222242,t458]) ).
cnf(t222244,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)],[t222243,t10]) ).
cnf(t222245,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)],[t222244,t2630]) ).
cnf(t222246,plain,
ld(X1,rd(rd(X1,mult(X1,X1)),X2)) = ld(mult(X1,X1),rd(rd(X1,X1),X2)),
inference(step,[status(thm)],[t222245,t992]) ).
cnf(t110205,plain,
ld(mult(X1,X1),rd(rd(X1,X1),X2)) = ld(X1,rd(rd(X1,mult(X1,X1)),X2)),
inference(orient,[status(thm)],[t222246]) ).
cnf(t110242,plain,
ld(X1,rd(rd(X1,mult(X1,X1)),rd(ld(X1,X2),X1))) = ld(mult(X1,X1),mult(rd(X1,X2),X1)),
inference(cp,[status(thm)],[t110205,t3295]) ).
cnf(t3310,plain,
mult(rd(rd(X1,X1),X2),X1) = rd(rd(X1,mult(X1,X1)),rd(ld(X1,X2),X1)),
inference(cp,[status(thm)],[t3295,t1091]) ).
cnf(t52201,plain,
rd(rd(X1,mult(X1,X1)),rd(ld(X1,X2),X1)) = mult(rd(rd(X1,X1),X2),X1),
inference(orient,[status(thm)],[t3310]) ).
cnf(t222253,plain,
ld(X1,mult(rd(rd(X1,X1),X2),X1)) = ld(mult(X1,X1),mult(rd(X1,X2),X1)),
inference(step,[status(thm)],[t110242,t52201]) ).
cnf(t111112,plain,
ld(mult(X1,X1),mult(rd(X1,X2),X1)) = ld(X1,mult(rd(rd(X1,X1),X2),X1)),
inference(orient,[status(thm)],[t222253]) ).
cnf(t111393,plain,
ld(mult(rd(X1,X2),X1),mult(X1,X1)) = ld(X3,rd(X3,ld(X1,mult(rd(rd(X1,X1),X2),X1)))),
inference(cp,[status(thm)],[t225,t111112]) ).
cnf(t222259,plain,
ld(mult(rd(X1,X2),X1),mult(X1,X1)) = ld(mult(rd(rd(X1,X1),X2),X1),X1),
inference(step,[status(thm)],[t111393,t225]) ).
cnf(t111986,plain,
ld(mult(rd(rd(X1,X1),X2),X1),X1) = ld(mult(rd(X1,X2),X1),mult(X1,X1)),
inference(orient,[status(thm)],[t222259]) ).
cnf(t112082,plain,
mult(rd(rd(X1,X1),X2),X1) = rd(X1,ld(mult(rd(X1,X2),X1),mult(X1,X1))),
inference(cp,[status(thm)],[t23,t111986]) ).
cnf(t141930,plain,
rd(X1,ld(mult(rd(X1,X2),X1),mult(X1,X1))) = mult(rd(rd(X1,X1),X2),X1),
inference(orient,[status(thm)],[t112082]) ).
cnf(t160283,plain,
mult(ld(rd(X1,X1),rd(X1,X2)),X1) = mult(X1,mult(rd(rd(X1,X1),X2),X1)),
inference(cp,[status(thm)],[t160278,t141930]) ).
cnf(t222567,plain,
mult(ld(X1,rd(mult(X1,X1),X2)),X1) = mult(X1,mult(rd(rd(X1,X1),X2),X1)),
inference(step,[status(thm)],[t160283,t121812]) ).
cnf(t160696,plain,
mult(ld(X1,rd(mult(X1,X1),X2)),X1) = mult(X1,mult(rd(rd(X1,X1),X2),X1)),
inference(orient,[status(thm)],[t222567]) ).
cnf(t119260,plain,
ld(X1,X2) = ld(rd(X2,ld(X1,mult(X2,X2))),rd(X2,X2)),
inference(cp,[status(thm)],[t24,t119069]) ).
cnf(t123877,plain,
ld(rd(X1,ld(X2,mult(X1,X1))),rd(X1,X1)) = ld(X2,X1),
inference(orient,[status(thm)],[t119260]) ).
cnf(t108541,plain,
ld(ld(X1,ld(X1,X2)),rd(X1,X1)) = ld(X3,rd(X3,ld(X1,rd(ld(X1,mult(X2,X1)),X1)))),
inference(cp,[status(thm)],[t225,t108292]) ).
cnf(t222232,plain,
ld(ld(X1,ld(X1,X2)),rd(X1,X1)) = ld(rd(ld(X1,mult(X2,X1)),X1),X1),
inference(step,[status(thm)],[t108541,t225]) ).
cnf(t109896,plain,
ld(rd(ld(X1,mult(X2,X1)),X1),X1) = ld(ld(X1,ld(X1,X2)),rd(X1,X1)),
inference(orient,[status(thm)],[t222232]) ).
cnf(t110043,plain,
ld(ld(X1,ld(X1,rd(X2,X1))),rd(X1,X1)) = ld(rd(ld(X1,X2),X1),X1),
inference(cp,[status(thm)],[t109896,t8]) ).
cnf(t105950,plain,
rd(mult(X1,mult(mult(rd(mult(X1,X2),X1),X1),X1)),X1) = mult(X1,mult(rd(mult(X1,mult(rd(X1,X1),X2)),X1),X1)),
inference(cp,[status(thm)],[t9877,t105665]) ).
cnf(t222185,plain,
rd(mult(X1,mult(mult(X1,X2),X1)),X1) = mult(X1,mult(rd(mult(X1,mult(rd(X1,X1),X2)),X1),X1)),
inference(step,[status(thm)],[t105950,t8]) ).
cnf(t222186,plain,
rd(mult(X1,mult(mult(X1,X2),X1)),X1) = mult(X1,mult(X1,mult(rd(X1,X1),X2))),
inference(step,[status(thm)],[t222185,t8]) ).
cnf(t107442,plain,
mult(X1,mult(X1,mult(rd(X1,X1),X2))) = rd(mult(X1,mult(mult(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t222186]) ).
cnf(t107532,plain,
rd(mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1)))),rd(X1,mult(X1,X1))) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X1),X2))),
inference(cp,[status(thm)],[t107442,t1178]) ).
cnf(t222205,plain,
mult(mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),rd(X1,mult(X1,X1)))),X1) = mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X1),X2))),
inference(step,[status(thm)],[t107532,t1178]) ).
cnf(t222206,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)],[t222205,t3971]) ).
cnf(t222207,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)],[t222206,t8]) ).
cnf(t222208,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)],[t222207,t1135]) ).
cnf(t222209,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)],[t222208,t8]) ).
cnf(t222210,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)],[t222209,t3971]) ).
cnf(t222211,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)],[t222210,t3971]) ).
cnf(t222212,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)],[t222211,t3971]) ).
cnf(t222213,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)],[t222212,t8]) ).
cnf(t222214,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)],[t222213,t458]) ).
cnf(t222215,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)],[t222214,t10]) ).
cnf(t222216,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)],[t222215,t2630]) ).
cnf(t222217,plain,
ld(X1,rd(ld(X1,mult(X2,X1)),X1)) = ld(mult(X1,X1),mult(rd(X1,X1),X2)),
inference(step,[status(thm)],[t222216,t992]) ).
cnf(t109133,plain,
ld(mult(X1,X1),mult(rd(X1,X1),X2)) = ld(X1,rd(ld(X1,mult(X2,X1)),X1)),
inference(orient,[status(thm)],[t222217]) ).
cnf(t109319,plain,
ld(mult(rd(X1,X1),X2),mult(X1,X1)) = ld(X3,rd(X3,ld(X1,rd(ld(X1,mult(X2,X1)),X1)))),
inference(cp,[status(thm)],[t225,t109133]) ).
cnf(t222249,plain,
ld(mult(rd(X1,X1),X2),mult(X1,X1)) = ld(rd(ld(X1,mult(X2,X1)),X1),X1),
inference(step,[status(thm)],[t109319,t225]) ).
cnf(t222250,plain,
ld(mult(rd(X1,X1),X2),mult(X1,X1)) = ld(ld(X1,ld(X1,X2)),rd(X1,X1)),
inference(step,[status(thm)],[t222249,t109896]) ).
cnf(t110787,plain,
ld(ld(X1,ld(X1,X2)),rd(X1,X1)) = ld(mult(rd(X1,X1),X2),mult(X1,X1)),
inference(orient,[status(thm)],[t222250]) ).
cnf(t222418,plain,
ld(mult(rd(X1,X1),rd(X2,X1)),mult(X1,X1)) = ld(rd(ld(X1,X2),X1),X1),
inference(step,[status(thm)],[t110043,t110787]) ).
cnf(t140472,plain,
ld(mult(rd(X1,X1),rd(X2,X1)),mult(X1,X1)) = ld(rd(ld(X1,X2),X1),X1),
inference(orient,[status(thm)],[t222418]) ).
cnf(t140772,plain,
ld(mult(rd(X1,X1),rd(X2,X1)),X1) = ld(rd(X1,ld(rd(ld(X1,X2),X1),X1)),rd(X1,X1)),
inference(cp,[status(thm)],[t123877,t140472]) ).
cnf(t117446,plain,
ld(mult(X1,X1),mult(X1,X2)) = ld(X1,rd(rd(X1,X1),ld(X3,rd(X3,X2)))),
inference(cp,[status(thm)],[t117259,t350]) ).
cnf(t222286,plain,
ld(mult(X1,X1),mult(X1,X2)) = ld(X1,mult(rd(X1,X1),X2)),
inference(step,[status(thm)],[t117446,t216]) ).
cnf(t117964,plain,
ld(mult(X1,X1),mult(X1,X2)) = ld(X1,mult(rd(X1,X1),X2)),
inference(orient,[status(thm)],[t222286]) ).
cnf(t118165,plain,
ld(mult(X1,X2),mult(X1,X1)) = ld(X3,rd(X3,ld(X1,mult(rd(X1,X1),X2)))),
inference(cp,[status(thm)],[t225,t117964]) ).
cnf(t222288,plain,
ld(mult(X1,X2),mult(X1,X1)) = ld(mult(rd(X1,X1),X2),X1),
inference(step,[status(thm)],[t118165,t225]) ).
cnf(t118480,plain,
ld(mult(rd(X1,X1),X2),X1) = ld(mult(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t222288]) ).
cnf(t222419,plain,
ld(mult(X1,rd(X2,X1)),mult(X1,X1)) = ld(rd(X1,ld(rd(ld(X1,X2),X1),X1)),rd(X1,X1)),
inference(step,[status(thm)],[t140772,t118480]) ).
cnf(t222420,plain,
ld(mult(X1,rd(X2,X1)),mult(X1,X1)) = ld(rd(ld(X1,X2),X1),rd(X1,X1)),
inference(step,[status(thm)],[t222419,t23]) ).
cnf(t140837,plain,
ld(mult(X1,rd(X2,X1)),mult(X1,X1)) = ld(rd(ld(X1,X2),X1),rd(X1,X1)),
inference(orient,[status(thm)],[t222420]) ).
cnf(t3993,plain,
rd(X1,mult(X1,X1)) = rd(rd(ld(X1,mult(X2,X1)),X1),X2),
inference(cp,[status(thm)],[t10,t3971]) ).
cnf(t4201,plain,
rd(rd(ld(X1,mult(X2,X1)),X1),X2) = rd(X1,mult(X1,X1)),
inference(orient,[status(thm)],[t3993]) ).
cnf(t140948,plain,
ld(rd(ld(X1,rd(ld(X2,mult(X1,X2)),X2)),X1),rd(X1,X1)) = ld(mult(X1,rd(X2,mult(X2,X2))),mult(X1,X1)),
inference(cp,[status(thm)],[t140837,t4201]) ).
cnf(t3977,plain,
rd(ld(X1,mult(rd(X2,mult(X2,X2)),X1)),X1) = rd(rd(X1,mult(X1,X1)),X2),
inference(cp,[status(thm)],[t3971,t1135]) ).
cnf(t221780,plain,
rd(ld(X1,rd(ld(X2,mult(X1,X2)),X2)),X1) = rd(rd(X1,mult(X1,X1)),X2),
inference(step,[status(thm)],[t3977,t3971]) ).
cnf(t55661,plain,
rd(ld(X1,rd(ld(X2,mult(X1,X2)),X2)),X1) = rd(rd(X1,mult(X1,X1)),X2),
inference(orient,[status(thm)],[t221780]) ).
cnf(t222613,plain,
ld(rd(rd(X1,mult(X1,X1)),X2),rd(X1,X1)) = ld(mult(X1,rd(X2,mult(X2,X2))),mult(X1,X1)),
inference(step,[status(thm)],[t140948,t55661]) ).
cnf(t222614,plain,
ld(rd(rd(X1,mult(X1,X1)),X2),rd(X1,X1)) = ld(rd(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t222613,t1135]) ).
cnf(t168309,plain,
ld(rd(rd(X1,mult(X1,X1)),X2),rd(X1,X1)) = ld(rd(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t222614]) ).
cnf(t9207,plain,
rd(rd(X1,mult(X1,X1)),mult(rd(X2,X2),rd(X1,mult(X1,X1)))) = ld(rd(X2,X2),mult(rd(X1,mult(X1,X1)),X1)),
inference(cp,[status(thm)],[t9203,t1178]) ).
cnf(t221884,plain,
rd(rd(X1,mult(X1,X1)),rd(rd(X2,X2),X1)) = ld(rd(X2,X2),mult(rd(X1,mult(X1,X1)),X1)),
inference(step,[status(thm)],[t9207,t1135]) ).
cnf(t221885,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)],[t221884,t2630]) ).
cnf(t221886,plain,
rd(rd(X1,mult(X1,X1)),rd(rd(X2,X2),X1)) = ld(rd(X2,X2),rd(X1,X1)),
inference(step,[status(thm)],[t221885,t992]) ).
cnf(t221887,plain,
rd(rd(X1,mult(X1,X1)),rd(rd(X2,X2),X1)) = rd(X1,mult(rd(X2,X2),X1)),
inference(step,[status(thm)],[t221886,t9203]) ).
cnf(t63916,plain,
rd(rd(X1,mult(X1,X1)),rd(rd(X2,X2),X1)) = rd(X1,mult(rd(X2,X2),X1)),
inference(orient,[status(thm)],[t221887]) ).
cnf(t168315,plain,
ld(rd(X1,rd(rd(X2,X2),X1)),mult(X1,X1)) = ld(rd(X1,mult(rd(X2,X2),X1)),rd(X1,X1)),
inference(cp,[status(thm)],[t168309,t63916]) ).
cnf(t9212,plain,
rd(rd(X1,X1),mult(rd(X2,X2),rd(X1,X1))) = ld(rd(X2,X2),rd(X1,X1)),
inference(cp,[status(thm)],[t9203,t992]) ).
cnf(t221895,plain,
rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = ld(rd(X2,X2),rd(X1,X1)),
inference(step,[status(thm)],[t9212,t619]) ).
cnf(t221896,plain,
rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = rd(X1,mult(rd(X2,X2),X1)),
inference(step,[status(thm)],[t221895,t9203]) ).
cnf(t64760,plain,
rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = rd(X1,mult(rd(X2,X2),X1)),
inference(orient,[status(thm)],[t221896]) ).
cnf(t64821,plain,
rd(rd(X1,X1),rd(X2,X2)) = ld(rd(X2,mult(rd(X1,X1),X2)),rd(X2,X2)),
inference(cp,[status(thm)],[t24,t64760]) ).
cnf(t94702,plain,
ld(rd(X1,mult(rd(X2,X2),X1)),rd(X1,X1)) = rd(rd(X2,X2),rd(X1,X1)),
inference(orient,[status(thm)],[t64821]) ).
cnf(t222794,plain,
ld(rd(X1,rd(rd(X2,X2),X1)),mult(X1,X1)) = rd(rd(X2,X2),rd(X1,X1)),
inference(step,[status(thm)],[t168315,t94702]) ).
cnf(t198305,plain,
ld(rd(X1,rd(rd(X2,X2),X1)),mult(X1,X1)) = rd(rd(X2,X2),rd(X1,X1)),
inference(orient,[status(thm)],[t222794]) ).
cnf(t198433,plain,
rd(X1,rd(rd(X2,X2),X1)) = rd(mult(X1,X1),rd(rd(X2,X2),rd(X1,X1))),
inference(cp,[status(thm)],[t23,t198305]) ).
cnf(t214572,plain,
rd(mult(X1,X1),rd(rd(X2,X2),rd(X1,X1))) = rd(X1,rd(rd(X2,X2),X1)),
inference(orient,[status(thm)],[t198433]) ).
cnf(t214783,plain,
mult(X1,mult(rd(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))),X1)) = mult(ld(X1,rd(X1,rd(rd(X2,X2),X1))),X1),
inference(cp,[status(thm)],[t160696,t214572]) ).
cnf(t222905,plain,
mult(X1,mult(rd(X1,mult(rd(X2,X2),X1)),X1)) = mult(ld(X1,rd(X1,rd(rd(X2,X2),X1))),X1),
inference(step,[status(thm)],[t214783,t64760]) ).
cnf(t45837,plain,
rd(X1,ld(X2,rd(rd(X1,X3),ld(X1,X2)))) = rd(mult(X2,X3),ld(X2,X1)),
inference(cp,[status(thm)],[t45836,t216]) ).
cnf(t84595,plain,
rd(X1,ld(X2,rd(rd(X1,X3),ld(X1,X2)))) = rd(mult(X2,X3),ld(X2,X1)),
inference(orient,[status(thm)],[t45837]) ).
cnf(t84869,plain,
ld(X1,rd(rd(X2,X3),ld(X2,X1))) = ld(rd(mult(X1,X3),ld(X1,X2)),X2),
inference(cp,[status(thm)],[t24,t84595]) ).
cnf(t85028,plain,
ld(rd(mult(X1,X2),ld(X1,X3)),X3) = ld(X1,rd(rd(X3,X2),ld(X3,X1))),
inference(orient,[status(thm)],[t84869]) ).
cnf(t85035,plain,
ld(X1,rd(rd(rd(X1,X2),X3),ld(rd(X1,X2),X1))) = ld(mult(mult(X1,X3),X2),rd(X1,X2)),
inference(cp,[status(thm)],[t85028,t216]) ).
cnf(t221989,plain,
ld(X1,rd(rd(rd(X1,X2),X3),X2)) = ld(mult(mult(X1,X3),X2),rd(X1,X2)),
inference(step,[status(thm)],[t85035,t24]) ).
cnf(t221990,plain,
ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = ld(mult(mult(X1,X3),X2),rd(X1,X2)),
inference(step,[status(thm)],[t221989,t1552]) ).
cnf(t221991,plain,
ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = rd(ld(X2,ld(mult(X1,X3),X1)),X2),
inference(step,[status(thm)],[t221990,t1433]) ).
cnf(t221992,plain,
ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = rd(ld(X2,ld(true,rd(true,X3))),X2),
inference(step,[status(thm)],[t221991,t350]) ).
cnf(t85414,plain,
ld(X1,rd(X1,mult(X2,mult(X3,X2)))) = rd(ld(X2,ld(true,rd(true,X3))),X2),
inference(orient,[status(thm)],[t221992]) ).
cnf(t85484,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)],[t85414,t3971]) ).
cnf(t221997,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)],[t85484,t1178]) ).
cnf(t221998,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)],[t221997,t2936]) ).
cnf(t221999,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)],[t221998,t8]) ).
cnf(t222000,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)],[t221999,t1135]) ).
cnf(t222001,plain,
mult(X1,mult(ld(true,rd(true,X2)),X1)) = ld(X3,rd(X3,rd(ld(X1,X2),X1))),
inference(step,[status(thm)],[t222000,t8]) ).
cnf(t86105,plain,
ld(X1,rd(X1,rd(ld(X2,X3),X2))) = mult(X2,mult(ld(true,rd(true,X3)),X2)),
inference(orient,[status(thm)],[t222001]) ).
cnf(t86198,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)],[t86105,t15280]) ).
cnf(t9244,plain,
ld(rd(X1,X1),rd(X2,X2)) = ld(X3,rd(X3,rd(X1,mult(rd(X2,X2),X1)))),
inference(cp,[status(thm)],[t225,t9203]) ).
cnf(t221897,plain,
rd(X2,mult(rd(X1,X1),X2)) = ld(X3,rd(X3,rd(X1,mult(rd(X2,X2),X1)))),
inference(step,[status(thm)],[t9244,t9203]) ).
cnf(t64964,plain,
ld(X1,rd(X1,rd(X2,mult(rd(X3,X3),X2)))) = rd(X3,mult(rd(X2,X2),X3)),
inference(orient,[status(thm)],[t221897]) ).
cnf(t222141,plain,
mult(X1,mult(rd(X1,mult(rd(X2,X2),X1)),X1)) = ld(X3,rd(X3,rd(mult(ld(X1,rd(rd(X2,X2),X1)),X1),X1))),
inference(step,[status(thm)],[t86198,t64964]) ).
cnf(t222142,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)],[t222141,t10]) ).
cnf(t222143,plain,
mult(X1,mult(rd(X1,mult(rd(X2,X2),X1)),X1)) = ld(rd(rd(X2,X2),X1),X1),
inference(step,[status(thm)],[t222142,t225]) ).
cnf(t100771,plain,
mult(X1,mult(rd(X1,mult(rd(X2,X2),X1)),X1)) = ld(rd(rd(X2,X2),X1),X1),
inference(orient,[status(thm)],[t222143]) ).
cnf(t222906,plain,
ld(rd(rd(X2,X2),X1),X1) = mult(ld(X1,rd(X1,rd(rd(X2,X2),X1))),X1),
inference(step,[status(thm)],[t222905,t100771]) ).
cnf(t219231,plain,
mult(ld(X1,rd(X1,rd(rd(X2,X2),X1))),X1) = ld(rd(rd(X2,X2),X1),X1),
inference(orient,[status(thm)],[t222906]) ).
cnf(t9217,plain,
rd(X1,X1) = rd(rd(X2,X2),rd(X2,mult(rd(X1,X1),X2))),
inference(cp,[status(thm)],[t23,t9203]) ).
cnf(t9252,plain,
rd(rd(X1,X1),rd(X1,mult(rd(X2,X2),X1))) = rd(X2,X2),
inference(orient,[status(thm)],[t9217]) ).
cnf(t219289,plain,
ld(rd(rd(X1,X1),rd(X1,mult(rd(X2,X2),X1))),rd(X1,mult(rd(X2,X2),X1))) = mult(ld(rd(X1,mult(rd(X2,X2),X1)),rd(rd(X1,mult(rd(X2,X2),X1)),rd(X2,X2))),rd(X1,mult(rd(X2,X2),X1))),
inference(cp,[status(thm)],[t219231,t9252]) ).
cnf(t222907,plain,
ld(rd(X2,X2),rd(X1,mult(rd(X2,X2),X1))) = mult(ld(rd(X1,mult(rd(X2,X2),X1)),rd(rd(X1,mult(rd(X2,X2),X1)),rd(X2,X2))),rd(X1,mult(rd(X2,X2),X1))),
inference(step,[status(thm)],[t219289,t9252]) ).
cnf(t15325,plain,
mult(ld(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))),
inference(cp,[status(thm)],[t15280,t992]) ).
cnf(t221926,plain,
rd(ld(rd(X1,X1),rd(rd(X2,X2),rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))),
inference(step,[status(thm)],[t15325,t619]) ).
cnf(t5031,plain,
rd(mult(rd(X1,X1),X2),rd(X1,X1)) = ld(rd(X1,X1),rd(X2,rd(X1,X1))),
inference(cp,[status(thm)],[t5023,t646]) ).
cnf(t14660,plain,
ld(rd(X1,X1),rd(X2,rd(X1,X1))) = rd(mult(rd(X1,X1),X2),rd(X1,X1)),
inference(orient,[status(thm)],[t5031]) ).
cnf(t221927,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)],[t221926,t14660]) ).
cnf(t221928,plain,
mult(rd(X1,X1),rd(X2,X2)) = ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))),
inference(step,[status(thm)],[t221927,t687]) ).
cnf(t221929,plain,
rd(rd(X1,X1),rd(X2,X2)) = ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))),
inference(step,[status(thm)],[t221928,t619]) ).
cnf(t68297,plain,
ld(rd(X1,X1),rd(X2,mult(rd(X1,X1),X2))) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t221929]) ).
cnf(t222908,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)],[t222907,t68297]) ).
cnf(t9202,plain,
mult(X1,mult(rd(rd(X2,ld(X3,rd(X3,X1))),rd(X2,ld(X3,rd(X3,X1)))),X1)) = mult(mult(ld(X2,rd(rd(X2,ld(X3,rd(X3,X1))),ld(X3,rd(X3,X1)))),ld(X3,rd(X3,X1))),X1),
inference(cp,[status(thm)],[t3823,t9075]) ).
cnf(t221875,plain,
mult(X1,mult(rd(mult(X2,X1),rd(X2,ld(X3,rd(X3,X1)))),X1)) = mult(mult(ld(X2,rd(rd(X2,ld(X3,rd(X3,X1))),ld(X3,rd(X3,X1)))),ld(X3,rd(X3,X1))),X1),
inference(step,[status(thm)],[t9202,t216]) ).
cnf(t221876,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)],[t221875,t3107]) ).
cnf(t221877,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)],[t221876,t216]) ).
cnf(t221878,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)],[t221877,t196]) ).
cnf(t500,plain,
mult(mult(X1,ld(X2,rd(X3,Y3))),Y3) = mult(rd(X1,Y3),ld(rd(X2,Y3),X3)),
inference(cp,[status(thm)],[t25,t479]) ).
cnf(t221419,plain,
mult(rd(X1,ld(rd(X3,Y3),X2)),Y3) = mult(rd(X1,Y3),ld(rd(X2,Y3),X3)),
inference(step,[status(thm)],[t500,t196]) ).
cnf(t221420,plain,
mult(rd(X1,ld(rd(X3,Y3),X2)),Y3) = rd(rd(X1,Y3),ld(X3,rd(X2,Y3))),
inference(step,[status(thm)],[t221419,t196]) ).
cnf(t8447,plain,
mult(rd(X1,ld(rd(X2,X3),Y3)),X3) = rd(rd(X1,X3),ld(X2,rd(Y3,X3))),
inference(orient,[status(thm)],[t221420]) ).
cnf(t221879,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)],[t221878,t8447]) ).
cnf(t221880,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)],[t221879,t216]) ).
cnf(t221881,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)],[t221880,t8]) ).
cnf(t221882,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)],[t221881,t216]) ).
cnf(t221883,plain,
mult(X1,rd(X2,rd(ld(X1,mult(X2,X1)),X1))) = ld(X2,mult(mult(X2,X1),X1)),
inference(step,[status(thm)],[t221882,t216]) ).
cnf(t63683,plain,
mult(X1,rd(X2,rd(ld(X1,mult(X2,X1)),X1))) = ld(X2,mult(mult(X2,X1),X1)),
inference(orient,[status(thm)],[t221883]) ).
cnf(t63696,plain,
ld(X1,mult(mult(X1,ld(X2,rd(X2,X3))),ld(X2,rd(X2,X3)))) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(ld(ld(X2,rd(X2,X3)),mult(X1,ld(X2,rd(X2,X3)))),X3))),
inference(cp,[status(thm)],[t63683,t216]) ).
cnf(t222042,plain,
ld(X1,rd(mult(X1,ld(X2,rd(X2,X3))),ld(rd(X2,X3),X2))) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(ld(ld(X2,rd(X2,X3)),mult(X1,ld(X2,rd(X2,X3)))),X3))),
inference(step,[status(thm)],[t63696,t196]) ).
cnf(t222043,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)],[t222042,t196]) ).
cnf(t222044,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)],[t222043,t24]) ).
cnf(t222045,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)],[t222044,t24]) ).
cnf(t222046,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)],[t222045,t3823]) ).
cnf(t222047,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)],[t222046,t196]) ).
cnf(t222048,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)],[t222047,t8447]) ).
cnf(t222049,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)],[t222048,t216]) ).
cnf(t222050,plain,
ld(X1,rd(rd(X1,X3),X3)) = mult(ld(X2,rd(X2,X3)),rd(X1,mult(X3,X1))),
inference(step,[status(thm)],[t222049,t8]) ).
cnf(t93691,plain,
mult(ld(X1,rd(X1,X2)),rd(X3,mult(X2,X3))) = ld(X3,rd(rd(X3,X2),X2)),
inference(orient,[status(thm)],[t222050]) ).
cnf(t222909,plain,
rd(rd(X2,X2),rd(X1,X1)) = ld(X1,rd(rd(X1,rd(X2,X2)),rd(X2,X2))),
inference(step,[status(thm)],[t222908,t93691]) ).
cnf(t222910,plain,
rd(rd(X2,X2),rd(X1,X1)) = ld(X1,X1),
inference(step,[status(thm)],[t222909,t687]) ).
cnf(t222911,plain,
rd(rd(X2,X2),rd(X1,X1)) = rd(X1,X1),
inference(step,[status(thm)],[t222910,t616]) ).
cnf(t219611,plain,
rd(rd(X1,X1),rd(X2,X2)) = rd(X2,X2),
inference(orient,[status(thm)],[t222911]) ).
cnf(t219823,plain,
mult(X1,mult(rd(X1,X1),rd(X2,X2))) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(cp,[status(thm)],[t81301,t219611]) ).
cnf(t222935,plain,
mult(X1,rd(rd(X1,X1),rd(X2,X2))) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(step,[status(thm)],[t219823,t619]) ).
cnf(t222936,plain,
mult(X1,rd(X2,X2)) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(step,[status(thm)],[t222935,t219611]) ).
cnf(t222937,plain,
rd(X1,rd(X2,X2)) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(step,[status(thm)],[t222936,t619]) ).
cnf(t222938,plain,
rd(X1,rd(X2,X2)) = X1,
inference(step,[status(thm)],[t222937,t10]) ).
cnf(t219919,plain,
rd(X1,rd(X2,X2)) = X1,
inference(orient,[status(thm)],[t222938]) ).
cnf(t515,plain,
mult(ld(X1,rd(X2,ld(X3,rd(X3,Y3)))),ld(X3,rd(X3,Y3))) = ld(ld(X3,rd(X3,Y3)),ld(mult(X1,Y3),X2)),
inference(cp,[status(thm)],[t506,t216]) ).
cnf(t221684,plain,
rd(ld(X1,rd(X2,ld(X3,rd(X3,Y3)))),ld(rd(X3,Y3),X3)) = ld(ld(X3,rd(X3,Y3)),ld(mult(X1,Y3),X2)),
inference(step,[status(thm)],[t515,t196]) ).
cnf(t221685,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)],[t221684,t216]) ).
cnf(t221686,plain,
rd(ld(X1,mult(X2,Y3)),Y3) = ld(ld(X3,rd(X3,Y3)),ld(mult(X1,Y3),X2)),
inference(step,[status(thm)],[t221685,t24]) ).
cnf(t39066,plain,
ld(ld(X1,rd(X1,X2)),ld(mult(X3,X2),Y3)) = rd(ld(X3,mult(Y3,X2)),X2),
inference(orient,[status(thm)],[t221686]) ).
cnf(t222324,plain,
ld(X1,mult(ld(X1,rd(mult(X1,X2),X1)),X1)) = rd(ld(X1,mult(X2,X1)),X1),
inference(step,[status(thm)],[t116973,t128441]) ).
cnf(t128695,plain,
ld(X1,mult(ld(X1,rd(mult(X1,X2),X1)),X1)) = rd(ld(X1,mult(X2,X1)),X1),
inference(rw,[status(thm)],[t222324]) ).
cnf(t3979,plain,
rd(ld(X1,mult(X2,X1)),X1) = mult(ld(X3,rd(X3,X1)),X2),
inference(cp,[status(thm)],[t3971,t1336]) ).
cnf(t32890,plain,
rd(ld(X1,mult(X2,X1)),X1) = mult(ld(X3,rd(X3,X1)),X2),
inference(orient,[status(thm)],[t3979]) ).
cnf(t90597,plain,
mult(ld(X1,rd(X1,mult(X2,X2))),mult(ld(X2,rd(X3,X2)),X2)) = rd(ld(mult(X2,X2),ld(X2,mult(X3,mult(X2,X2)))),mult(X2,X2)),
inference(cp,[status(thm)],[t32890,t90256]) ).
cnf(t523,plain,
rd(X1,ld(ld(rd(X2,X3),Y3),X3)) = mult(X1,mult(ld(X2,rd(Y3,X3)),X3)),
inference(cp,[status(thm)],[t196,t506]) ).
cnf(t8706,plain,
mult(X1,mult(ld(X2,rd(X3,Y3)),Y3)) = rd(X1,ld(ld(rd(X2,Y3),X3),Y3)),
inference(orient,[status(thm)],[t523]) ).
cnf(t222149,plain,
rd(ld(X1,rd(X1,mult(X2,X2))),ld(ld(rd(X2,X2),X3),X2)) = rd(ld(mult(X2,X2),ld(X2,mult(X3,mult(X2,X2)))),mult(X2,X2)),
inference(step,[status(thm)],[t90597,t8706]) ).
cnf(t1062,plain,
mult(ld(X1,rd(X1,X2)),ld(X1,rd(X1,X2))) = ld(ld(X3,mult(X3,X2)),ld(X1,rd(X1,X2))),
inference(cp,[status(thm)],[t1056,t216]) ).
cnf(t221274,plain,
rd(ld(X1,rd(X1,X2)),ld(rd(X1,X2),X1)) = ld(ld(X3,mult(X3,X2)),ld(X1,rd(X1,X2))),
inference(step,[status(thm)],[t1062,t196]) ).
cnf(t221275,plain,
rd(ld(X1,rd(X1,X2)),X2) = ld(ld(X3,mult(X3,X2)),ld(X1,rd(X1,X2))),
inference(step,[status(thm)],[t221274,t24]) ).
cnf(t221276,plain,
rd(ld(X1,rd(X1,X2)),X2) = ld(X2,ld(X1,rd(X1,X2))),
inference(step,[status(thm)],[t221275,t12]) ).
cnf(t1257,plain,
ld(X1,ld(X2,rd(X2,X1))) = rd(ld(X2,rd(X2,X1)),X1),
inference(orient,[status(thm)],[t221276]) ).
cnf(t4176,plain,
rd(ld(X1,rd(X1,X2)),X2) = rd(X3,mult(X2,mult(X2,X3))),
inference(cp,[status(thm)],[t23,t4118]) ).
cnf(t33342,plain,
rd(ld(X1,rd(X1,X2)),X2) = rd(X3,mult(X2,mult(X2,X3))),
inference(orient,[status(thm)],[t4176]) ).
cnf(t221654,plain,
ld(X1,ld(X2,rd(X2,X1))) = rd(true,mult(X1,mult(X1,true))),
inference(step,[status(thm)],[t1257,t33342]) ).
cnf(t33343,plain,
ld(X1,ld(X2,rd(X2,X1))) = rd(true,mult(X1,mult(X1,true))),
inference(orient,[status(thm)],[t221654]) ).
cnf(t4394,plain,
rd(ld(X1,mult(rd(X1,X1),X2)),X1) = ld(X1,rd(ld(rd(X1,X1),X2),X1)),
inference(cp,[status(thm)],[t3761,t4363]) ).
cnf(t14185,plain,
ld(X1,rd(ld(rd(X1,X1),X2),X1)) = rd(ld(X1,mult(rd(X1,X1),X2)),X1),
inference(orient,[status(thm)],[t4394]) ).
cnf(t33498,plain,
rd(ld(X1,mult(rd(X1,X1),rd(rd(X1,X1),X1))),X1) = ld(X1,rd(X2,mult(X1,mult(X1,X2)))),
inference(cp,[status(thm)],[t14185,t33342]) ).
cnf(t221656,plain,
rd(ld(X1,mult(rd(X1,X1),rd(X1,mult(X1,X1)))),X1) = ld(X1,rd(X2,mult(X1,mult(X1,X2)))),
inference(step,[status(thm)],[t33498,t1091]) ).
cnf(t221657,plain,
rd(ld(X1,rd(rd(X1,X1),X1)),X1) = ld(X1,rd(X2,mult(X1,mult(X1,X2)))),
inference(step,[status(thm)],[t221656,t1135]) ).
cnf(t221658,plain,
rd(ld(X1,rd(X1,mult(X1,X1))),X1) = ld(X1,rd(X2,mult(X1,mult(X1,X2)))),
inference(step,[status(thm)],[t221657,t1091]) ).
cnf(t1577,plain,
rd(mult(X1,X2),mult(X2,mult(X3,X2))) = rd(rd(X1,X3),X2),
inference(cp,[status(thm)],[t1552,t10]) ).
cnf(t2431,plain,
rd(mult(X1,X2),mult(X2,mult(X3,X2))) = rd(rd(X1,X3),X2),
inference(orient,[status(thm)],[t1577]) ).
cnf(t2471,plain,
rd(rd(X1,rd(X2,X3)),X3) = rd(mult(X1,X3),mult(X3,X2)),
inference(cp,[status(thm)],[t2431,t8]) ).
cnf(t2499,plain,
rd(rd(X1,rd(X2,X3)),X3) = rd(mult(X1,X3),mult(X3,X2)),
inference(orient,[status(thm)],[t2471]) ).
cnf(t2955,plain,
rd(X1,mult(X1,X1)) = rd(X2,rd(mult(X1,mult(X2,X1)),X1)),
inference(cp,[status(thm)],[t23,t2936]) ).
cnf(t3176,plain,
rd(X1,rd(mult(X2,mult(X1,X2)),X2)) = rd(X2,mult(X2,X2)),
inference(orient,[status(thm)],[t2955]) ).
cnf(t3201,plain,
rd(X1,mult(X1,X1)) = rd(rd(X2,X1),rd(mult(X1,X2),X1)),
inference(cp,[status(thm)],[t3176,t8]) ).
cnf(t3394,plain,
rd(rd(X1,X2),rd(mult(X2,X1),X2)) = rd(X2,mult(X2,X2)),
inference(orient,[status(thm)],[t3201]) ).
cnf(t3454,plain,
rd(mult(rd(X1,X2),X2),mult(X2,mult(X2,X1))) = rd(rd(X2,mult(X2,X2)),X2),
inference(cp,[status(thm)],[t2499,t3394]) ).
cnf(t221650,plain,
rd(X1,mult(X2,mult(X2,X1))) = rd(rd(X2,mult(X2,X2)),X2),
inference(step,[status(thm)],[t3454,t8]) ).
cnf(t221651,plain,
rd(X1,mult(X2,mult(X2,X1))) = rd(rd(X2,X2),mult(X2,X2)),
inference(step,[status(thm)],[t221650,t2384]) ).
cnf(t221652,plain,
rd(X1,mult(X2,mult(X2,X1))) = rd(X2,mult(X2,mult(X2,X2))),
inference(step,[status(thm)],[t221651,t1609]) ).
cnf(t32436,plain,
rd(X1,mult(X2,mult(X2,X1))) = rd(X2,mult(X2,mult(X2,X2))),
inference(orient,[status(thm)],[t221652]) ).
cnf(t32622,plain,
ld(X1,rd(X1,mult(X2,mult(X2,X2)))) = ld(X2,rd(X3,mult(X2,mult(X2,X3)))),
inference(cp,[status(thm)],[t391,t32436]) ).
cnf(t23588,plain,
mult(rd(X1,mult(rd(X2,X1),X2)),X2) = ld(rd(X2,X1),X1),
inference(cp,[status(thm)],[t23534,t24]) ).
cnf(t24107,plain,
mult(rd(X1,mult(rd(X2,X1),X2)),X2) = ld(rd(X2,X1),X1),
inference(orient,[status(thm)],[t23588]) ).
cnf(t24210,plain,
rd(X1,mult(rd(X2,X1),X2)) = rd(ld(rd(X2,X1),X1),X2),
inference(cp,[status(thm)],[t10,t24107]) ).
cnf(t24286,plain,
rd(ld(rd(X1,X2),X2),X1) = rd(X2,mult(rd(X1,X2),X1)),
inference(orient,[status(thm)],[t24210]) ).
cnf(t24331,plain,
rd(X1,mult(rd(mult(X2,X1),X1),mult(X2,X1))) = rd(ld(X2,X1),mult(X2,X1)),
inference(cp,[status(thm)],[t24286,t10]) ).
cnf(t221577,plain,
rd(X1,mult(X2,mult(X2,X1))) = rd(ld(X2,X1),mult(X2,X1)),
inference(step,[status(thm)],[t24331,t10]) ).
cnf(t24670,plain,
rd(ld(X1,X2),mult(X1,X2)) = rd(X2,mult(X1,mult(X1,X2))),
inference(orient,[status(thm)],[t221577]) ).
cnf(t24807,plain,
mult(X1,X2) = ld(rd(X2,mult(X1,mult(X1,X2))),ld(X1,X2)),
inference(cp,[status(thm)],[t24,t24670]) ).
cnf(t24891,plain,
ld(rd(X1,mult(X2,mult(X2,X1))),ld(X2,X1)) = mult(X2,X1),
inference(orient,[status(thm)],[t24807]) ).
cnf(t1585,plain,
X1 = ld(rd(X2,mult(X1,mult(X3,X1))),rd(rd(X2,X1),X3)),
inference(cp,[status(thm)],[t24,t1552]) ).
cnf(t17788,plain,
ld(rd(X1,mult(X2,mult(X3,X2))),rd(rd(X1,X2),X3)) = X2,
inference(orient,[status(thm)],[t1585]) ).
cnf(t17885,plain,
X1 = ld(rd(X2,mult(X1,mult(rd(mult(X1,X2),X1),X1))),rd(X1,mult(X1,X1))),
inference(cp,[status(thm)],[t17788,t3394]) ).
cnf(t221586,plain,
X1 = ld(rd(X2,mult(X1,mult(X1,X2))),rd(X1,mult(X1,X1))),
inference(step,[status(thm)],[t17885,t8]) ).
cnf(t26254,plain,
ld(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))) = X2,
inference(orient,[status(thm)],[t221586]) ).
cnf(t26379,plain,
mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))) = ld(rd(rd(X2,mult(X2,X2)),mult(rd(X1,mult(X2,mult(X2,X1))),mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))))),X2),
inference(cp,[status(thm)],[t24891,t26254]) ).
cnf(t221602,plain,
ld(X2,ld(X2,rd(X2,mult(X2,X2)))) = ld(rd(rd(X2,mult(X2,X2)),mult(rd(X1,mult(X2,mult(X2,X1))),mult(rd(X1,mult(X2,mult(X2,X1))),rd(X2,mult(X2,X2))))),X2),
inference(step,[status(thm)],[t26379,t21708]) ).
cnf(t21005,plain,
ld(X1,ld(X1,rd(X2,mult(X1,X1)))) = rd(ld(mult(X1,X1),X2),mult(X1,X1)),
inference(cp,[status(thm)],[t21003,t4024]) ).
cnf(t22693,plain,
ld(X1,ld(X1,rd(X2,mult(X1,X1)))) = rd(ld(mult(X1,X1),X2),mult(X1,X1)),
inference(orient,[status(thm)],[t21005]) ).
cnf(t221603,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)],[t221602,t22693]) ).
cnf(t221604,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)],[t221603,t350]) ).
cnf(t221605,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)],[t221604,t21708]) ).
cnf(t221606,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)],[t221605,t21708]) ).
cnf(t221607,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)],[t221606,t22693]) ).
cnf(t221608,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)],[t221607,t22693]) ).
cnf(t221609,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)],[t221608,t3295]) ).
cnf(t221610,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(mult(mult(X2,X2),mult(X2,X2)),X2),
inference(step,[status(thm)],[t221609,t23]) ).
cnf(t1057,plain,
mult(ld(X1,X2),ld(X1,X2)) = ld(ld(X2,X1),ld(X1,X2)),
inference(cp,[status(thm)],[t1056,t225]) ).
cnf(t221273,plain,
rd(ld(X1,X2),ld(X2,X1)) = ld(ld(X2,X1),ld(X1,X2)),
inference(step,[status(thm)],[t1057,t196]) ).
cnf(t1222,plain,
ld(ld(X1,X2),ld(X2,X1)) = rd(ld(X2,X1),ld(X1,X2)),
inference(orient,[status(thm)],[t221273]) ).
cnf(t1283,plain,
rd(ld(rd(X1,mult(X1,X1)),X1),ld(X1,rd(X1,mult(X1,X1)))) = ld(rd(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),X1)),
inference(cp,[status(thm)],[t1222,t1278]) ).
cnf(t221279,plain,
mult(ld(rd(X1,mult(X1,X1)),X1),mult(X1,X1)) = ld(rd(rd(X1,mult(X1,X1)),X1),ld(rd(X1,mult(X1,X1)),X1)),
inference(step,[status(thm)],[t1283,t216]) ).
cnf(t221280,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)],[t221279,t24]) ).
cnf(t221281,plain,
mult(mult(X1,X1),mult(X1,X1)) = ld(rd(rd(X1,mult(X1,X1)),X1),mult(X1,X1)),
inference(step,[status(thm)],[t221280,t24]) ).
cnf(t221282,plain,
mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(ld(rd(X1,mult(X1,X1)),X1),X1)),
inference(step,[status(thm)],[t221281,t83]) ).
cnf(t221283,plain,
mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(mult(X1,X1),X1)),
inference(step,[status(thm)],[t221282,t24]) ).
cnf(t221284,plain,
mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(X1,mult(X1,X1))),
inference(step,[status(thm)],[t221283,t868]) ).
cnf(t1297,plain,
mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(X1,mult(X1,X1))),
inference(orient,[status(thm)],[t221284]) ).
cnf(t221611,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(mult(X2,mult(X2,mult(X2,X2))),X2),
inference(step,[status(thm)],[t221610,t1297]) ).
cnf(t221612,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(true,rd(true,mult(X2,mult(X2,X2)))),
inference(step,[status(thm)],[t221611,t350]) ).
cnf(t26929,plain,
ld(true,rd(true,mult(X1,mult(X1,X1)))) = rd(ld(true,rd(true,X1)),mult(X1,X1)),
inference(orient,[status(thm)],[t221612]) ).
cnf(t26931,plain,
rd(ld(true,rd(true,X1)),mult(X1,X1)) = ld(X2,rd(X2,mult(X1,mult(X1,X1)))),
inference(cp,[status(thm)],[t26929,t391]) ).
cnf(t28126,plain,
ld(X1,rd(X1,mult(X2,mult(X2,X2)))) = rd(ld(true,rd(true,X2)),mult(X2,X2)),
inference(orient,[status(thm)],[t26931]) ).
cnf(t221653,plain,
rd(ld(true,rd(true,X2)),mult(X2,X2)) = ld(X2,rd(X3,mult(X2,mult(X2,X3)))),
inference(step,[status(thm)],[t32622,t28126]) ).
cnf(t32717,plain,
ld(X1,rd(X2,mult(X1,mult(X1,X2)))) = rd(ld(true,rd(true,X1)),mult(X1,X1)),
inference(orient,[status(thm)],[t221653]) ).
cnf(t221659,plain,
rd(ld(X1,rd(X1,mult(X1,X1))),X1) = rd(ld(true,rd(true,X1)),mult(X1,X1)),
inference(step,[status(thm)],[t221658,t32717]) ).
cnf(t33708,plain,
rd(ld(X1,rd(X1,mult(X1,X1))),X1) = rd(ld(true,rd(true,X1)),mult(X1,X1)),
inference(orient,[status(thm)],[t221659]) ).
cnf(t33802,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)],[t33343,t33708]) ).
cnf(t221660,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)],[t33802,t5023]) ).
cnf(t221661,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)],[t221660,t196]) ).
cnf(t221662,plain,
rd(true,mult(X1,mult(X1,true))) = ld(X1,rd(rd(mult(X1,X1),X1),mult(X1,X1))),
inference(step,[status(thm)],[t221661,t24]) ).
cnf(t221663,plain,
rd(true,mult(X1,mult(X1,true))) = ld(X1,rd(X1,mult(X1,X1))),
inference(step,[status(thm)],[t221662,t10]) ).
cnf(t33840,plain,
ld(X1,rd(X1,mult(X1,X1))) = rd(true,mult(X1,mult(X1,true))),
inference(orient,[status(thm)],[t221663]) ).
cnf(t33845,plain,
rd(true,mult(X1,mult(X1,true))) = ld(X2,rd(X2,mult(X1,X1))),
inference(cp,[status(thm)],[t33840,t391]) ).
cnf(t33926,plain,
ld(X1,rd(X1,mult(X2,X2))) = rd(true,mult(X2,mult(X2,true))),
inference(orient,[status(thm)],[t33845]) ).
cnf(t222150,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)],[t222149,t33926]) ).
cnf(t21733,plain,
ld(X1,ld(X1,ld(X2,X3))) = rd(rd(Y3,mult(X1,mult(X1,Y3))),ld(X3,X2)),
inference(cp,[status(thm)],[t21708,t196]) ).
cnf(t70862,plain,
rd(rd(X1,mult(X2,mult(X2,X1))),ld(X3,Y3)) = ld(X2,ld(X2,ld(Y3,X3))),
inference(orient,[status(thm)],[t21733]) ).
cnf(t222151,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)],[t222150,t70862]) ).
cnf(t222152,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)],[t222151,t506]) ).
cnf(t222153,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)],[t222152,t458]) ).
cnf(t222154,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)],[t222153,t458]) ).
cnf(t222155,plain,
mult(ld(mult(X2,X2),ld(X2,rd(X3,X2))),X2) = ld(mult(X2,mult(X2,X2)),X3),
inference(step,[status(thm)],[t222154,t10]) ).
cnf(t103323,plain,
mult(ld(mult(X1,X1),ld(X1,rd(X2,X1))),X1) = ld(mult(X1,mult(X1,X1)),X2),
inference(orient,[status(thm)],[t222155]) ).
cnf(t103536,plain,
ld(mult(X1,mult(X1,X1)),mult(X2,X1)) = mult(ld(mult(X1,X1),ld(X1,X2)),X1),
inference(cp,[status(thm)],[t103323,t10]) ).
cnf(t103728,plain,
ld(mult(X1,mult(X1,X1)),mult(X2,X1)) = mult(ld(mult(X1,X1),ld(X1,X2)),X1),
inference(orient,[status(thm)],[t103536]) ).
cnf(t103959,plain,
ld(mult(X1,X2),mult(X2,mult(X2,X2))) = ld(X3,rd(X3,mult(ld(mult(X2,X2),ld(X2,X1)),X2))),
inference(cp,[status(thm)],[t225,t103728]) ).
cnf(t477,plain,
ld(ld(X1,mult(X2,X3)),X3) = ld(Y3,rd(Y3,mult(ld(mult(X1,X3),X2),X3))),
inference(cp,[status(thm)],[t225,t458]) ).
cnf(t38476,plain,
ld(X1,rd(X1,mult(ld(mult(X2,X3),Y3),X3))) = ld(ld(X2,mult(Y3,X3)),X3),
inference(orient,[status(thm)],[t477]) ).
cnf(t222156,plain,
ld(mult(X1,X2),mult(X2,mult(X2,X2))) = ld(ld(X2,mult(ld(X2,X1),X2)),X2),
inference(step,[status(thm)],[t103959,t38476]) ).
cnf(t104391,plain,
ld(ld(X1,mult(ld(X1,X2),X1)),X1) = ld(mult(X2,X1),mult(X1,mult(X1,X1))),
inference(orient,[status(thm)],[t222156]) ).
cnf(t104578,plain,
ld(X1,mult(ld(X1,X2),X1)) = rd(X1,ld(mult(X2,X1),mult(X1,mult(X1,X1)))),
inference(cp,[status(thm)],[t23,t104391]) ).
cnf(t130284,plain,
rd(X1,ld(mult(X2,X1),mult(X1,mult(X1,X1)))) = ld(X1,mult(ld(X1,X2),X1)),
inference(orient,[status(thm)],[t104578]) ).
cnf(t130412,plain,
ld(X1,mult(ld(X1,rd(X2,X1)),X1)) = rd(X1,ld(X2,mult(X1,mult(X1,X1)))),
inference(cp,[status(thm)],[t130284,t8]) ).
cnf(t130655,plain,
ld(X1,mult(ld(X1,rd(X2,X1)),X1)) = rd(X1,ld(X2,mult(X1,mult(X1,X1)))),
inference(orient,[status(thm)],[t130412]) ).
cnf(t222500,plain,
rd(X1,ld(mult(X1,X2),mult(X1,mult(X1,X1)))) = rd(ld(X1,mult(X2,X1)),X1),
inference(step,[status(thm)],[t128695,t130655]) ).
cnf(t154056,plain,
rd(X1,ld(mult(X1,X2),mult(X1,mult(X1,X1)))) = rd(ld(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t222500]) ).
cnf(t154335,plain,
ld(mult(X1,mult(X1,X1)),mult(X1,X2)) = ld(X1,rd(ld(X1,mult(X2,X1)),X1)),
inference(cp,[status(thm)],[t225,t154056]) ).
cnf(t154766,plain,
ld(mult(X1,mult(X1,X1)),mult(X1,X2)) = ld(X1,rd(ld(X1,mult(X2,X1)),X1)),
inference(orient,[status(thm)],[t154335]) ).
cnf(t154977,plain,
rd(ld(X1,mult(mult(X1,X2),mult(X1,X1))),mult(X1,X1)) = ld(ld(X3,rd(X3,mult(X1,X1))),ld(X1,rd(ld(X1,mult(X2,X1)),X1))),
inference(cp,[status(thm)],[t39066,t154766]) ).
cnf(t67,plain,
mult(X1,X2) = rd(rd(mult(X1,mult(X2,X3)),X2),rd(X3,X2)),
inference(cp,[status(thm)],[t10,t56]) ).
cnf(t2776,plain,
rd(rd(mult(X1,mult(X2,X3)),X2),rd(X3,X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t67]) ).
cnf(t55207,plain,
mult(ld(X1,rd(X2,X1)),X1) = rd(rd(rd(ld(X1,mult(X2,mult(X1,X1))),X1),X1),rd(X1,X1)),
inference(cp,[status(thm)],[t2776,t54979]) ).
cnf(t222025,plain,
mult(ld(X1,rd(X2,X1)),X1) = rd(ld(X1,mult(X2,mult(X1,X1))),mult(X1,X1)),
inference(step,[status(thm)],[t55207,t2335]) ).
cnf(t90601,plain,
rd(ld(X1,mult(X2,mult(X1,X1))),mult(X1,X1)) = mult(ld(X1,rd(X2,X1)),X1),
inference(orient,[status(thm)],[t222025]) ).
cnf(t222519,plain,
mult(ld(X1,rd(mult(X1,X2),X1)),X1) = ld(ld(X3,rd(X3,mult(X1,X1))),ld(X1,rd(ld(X1,mult(X2,X1)),X1))),
inference(step,[status(thm)],[t154977,t90601]) ).
cnf(t222520,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)],[t222519,t33926]) ).
cnf(t222521,plain,
mult(ld(X1,rd(mult(X1,X2),X1)),X1) = mult(X1,rd(ld(X1,mult(X2,X1)),X1)),
inference(step,[status(thm)],[t222520,t29428]) ).
cnf(t26,plain,
mult(mult(X1,X2),ld(X3,X1)) = mult(X3,mult(ld(X3,X1),mult(X2,ld(X3,X1)))),
inference(cp,[status(thm)],[t25,t23]) ).
cnf(t221439,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(t221440,plain,
rd(mult(X1,X2),ld(X1,X3)) = mult(X3,mult(ld(X3,X1),rd(X2,ld(X1,X3)))),
inference(step,[status(thm)],[t221439,t196]) ).
cnf(t10467,plain,
mult(X1,mult(ld(X1,X2),rd(X3,ld(X2,X1)))) = rd(mult(X2,X3),ld(X2,X1)),
inference(orient,[status(thm)],[t221440]) ).
cnf(t10517,plain,
rd(mult(rd(X1,X2),X3),ld(rd(X1,X2),X1)) = mult(X1,mult(rd(X2,mult(X2,X2)),rd(X3,ld(rd(X1,X2),X1)))),
inference(cp,[status(thm)],[t10467,t1336]) ).
cnf(t221441,plain,
rd(mult(rd(X1,X2),X3),X2) = mult(X1,mult(rd(X2,mult(X2,X2)),rd(X3,ld(rd(X1,X2),X1)))),
inference(step,[status(thm)],[t10517,t24]) ).
cnf(t221442,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)],[t221441,t3971]) ).
cnf(t221443,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)],[t221442,t8447]) ).
cnf(t221444,plain,
rd(mult(rd(X1,X2),X3),X2) = mult(X1,rd(ld(X2,mult(rd(X3,X2),X2)),X2)),
inference(step,[status(thm)],[t221443,t216]) ).
cnf(t221445,plain,
rd(mult(rd(X1,X2),X3),X2) = mult(X1,rd(ld(X2,X3),X2)),
inference(step,[status(thm)],[t221444,t8]) ).
cnf(t10640,plain,
mult(X1,rd(ld(X2,X3),X2)) = rd(mult(rd(X1,X2),X3),X2),
inference(orient,[status(thm)],[t221445]) ).
cnf(t222522,plain,
mult(ld(X1,rd(mult(X1,X2),X1)),X1) = rd(mult(rd(X1,X1),mult(X2,X1)),X1),
inference(step,[status(thm)],[t222521,t10640]) ).
cnf(t155763,plain,
mult(ld(X1,rd(mult(X1,X2),X1)),X1) = rd(mult(rd(X1,X1),mult(X2,X1)),X1),
inference(orient,[status(thm)],[t222522]) ).
cnf(t155967,plain,
ld(X1,rd(mult(X1,X2),X1)) = rd(rd(mult(rd(X1,X1),mult(X2,X1)),X1),X1),
inference(cp,[status(thm)],[t10,t155763]) ).
cnf(t187157,plain,
rd(rd(mult(rd(X1,X1),mult(X2,X1)),X1),X1) = ld(X1,rd(mult(X1,X2),X1)),
inference(orient,[status(thm)],[t155967]) ).
cnf(t219952,plain,
rd(mult(rd(rd(X1,X1),rd(X1,X1)),mult(X2,rd(X1,X1))),rd(X1,X1)) = ld(rd(X1,X1),rd(mult(rd(X1,X1),X2),rd(X1,X1))),
inference(cp,[status(thm)],[t219919,t187157]) ).
cnf(t223112,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),mult(X2,rd(X1,X1))) = ld(rd(X1,X1),rd(mult(rd(X1,X1),X2),rd(X1,X1))),
inference(step,[status(thm)],[t219952,t219919]) ).
cnf(t223113,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)],[t223112,t219611]) ).
cnf(t222939,plain,
mult(X1,rd(X2,X2)) = X1,
inference(step,[status(thm)],[t619,t219919]) ).
cnf(t219920,plain,
mult(X1,rd(X2,X2)) = X1,
inference(orient,[status(thm)],[t222939]) ).
cnf(t223114,plain,
mult(rd(X1,X1),X2) = ld(rd(X1,X1),rd(mult(rd(X1,X1),X2),rd(X1,X1))),
inference(step,[status(thm)],[t223113,t219920]) ).
cnf(t223115,plain,
mult(rd(X1,X1),X2) = rd(mult(rd(X1,X1),mult(rd(X1,X1),X2)),rd(X1,X1)),
inference(step,[status(thm)],[t223114,t14660]) ).
cnf(t223116,plain,
mult(rd(X1,X1),X2) = mult(rd(X1,X1),mult(rd(X1,X1),X2)),
inference(step,[status(thm)],[t223115,t219919]) ).
cnf(t223117,plain,
mult(rd(X1,X1),X2) = ld(rd(X1,X1),X2),
inference(step,[status(thm)],[t223116,t4363]) ).
cnf(t106702,plain,
mult(ld(X1,rd(mult(mult(X1,X1),X2),X1)),X1) = ld(X1,rd(mult(X1,mult(mult(X1,X2),X1)),X1)),
inference(cp,[status(thm)],[t506,t106530]) ).
cnf(t222339,plain,
ld(X1,rd(mult(X1,mult(X2,X1)),X1)) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
inference(step,[status(thm)],[t9977,t129505]) ).
cnf(t129506,plain,
ld(X1,rd(mult(X1,mult(X2,X1)),X1)) = mult(X1,rd(X1,ld(X2,mult(X1,X1)))),
inference(orient,[status(thm)],[t222339]) ).
cnf(t222377,plain,
mult(ld(X1,rd(mult(mult(X1,X1),X2),X1)),X1) = mult(X1,rd(X1,ld(mult(X1,X2),mult(X1,X1)))),
inference(step,[status(thm)],[t106702,t129506]) ).
cnf(t118550,plain,
mult(rd(X1,X1),X2) = rd(X1,ld(mult(X1,X2),mult(X1,X1))),
inference(cp,[status(thm)],[t23,t118480]) ).
cnf(t119462,plain,
rd(X1,ld(mult(X1,X2),mult(X1,X1))) = mult(rd(X1,X1),X2),
inference(orient,[status(thm)],[t118550]) ).
cnf(t222378,plain,
mult(ld(X1,rd(mult(mult(X1,X1),X2),X1)),X1) = mult(X1,mult(rd(X1,X1),X2)),
inference(step,[status(thm)],[t222377,t119462]) ).
cnf(t134336,plain,
mult(ld(X1,rd(mult(mult(X1,X1),X2),X1)),X1) = mult(X1,mult(rd(X1,X1),X2)),
inference(orient,[status(thm)],[t222378]) ).
cnf(t134484,plain,
ld(X1,rd(mult(mult(X1,X1),X2),X1)) = rd(mult(X1,mult(rd(X1,X1),X2)),X1),
inference(cp,[status(thm)],[t10,t134336]) ).
cnf(t134661,plain,
ld(X1,rd(mult(mult(X1,X1),X2),X1)) = rd(mult(X1,mult(rd(X1,X1),X2)),X1),
inference(orient,[status(thm)],[t134484]) ).
cnf(t134673,plain,
rd(mult(X1,mult(rd(X1,X1),mult(X1,mult(X2,X1)))),X1) = ld(X1,mult(mult(mult(X1,X1),X1),X2)),
inference(cp,[status(thm)],[t134661,t44]) ).
cnf(t222379,plain,
rd(mult(X1,mult(mult(X1,X2),X1)),X1) = ld(X1,mult(mult(mult(X1,X1),X1),X2)),
inference(step,[status(thm)],[t134673,t25]) ).
cnf(t222380,plain,
rd(mult(X1,mult(mult(X1,X2),X1)),X1) = ld(X1,mult(mult(X1,mult(X1,X1)),X2)),
inference(step,[status(thm)],[t222379,t868]) ).
cnf(t134949,plain,
ld(X1,mult(mult(X1,mult(X1,X1)),X2)) = rd(mult(X1,mult(mult(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t222380]) ).
cnf(t134963,plain,
rd(mult(X1,mult(mult(X1,mult(ld(X2,rd(X2,mult(X1,X1))),X3)),X1)),X1) = ld(X1,rd(mult(X1,mult(X3,mult(X1,X1))),mult(X1,X1))),
inference(cp,[status(thm)],[t134949,t36685]) ).
cnf(t222382,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)],[t134963,t33926]) ).
cnf(t222383,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)],[t222382,t21708]) ).
cnf(t222384,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)],[t222383,t196]) ).
cnf(t222385,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)],[t222384,t23]) ).
cnf(t54709,plain,
mult(mult(X1,rd(X2,X1)),X1) = rd(rd(rd(mult(X1,mult(X2,mult(X1,X1))),X1),X1),rd(X1,X1)),
inference(cp,[status(thm)],[t2776,t54494]) ).
cnf(t222022,plain,
mult(rd(X1,X1),mult(X1,X2)) = rd(rd(rd(mult(X1,mult(X2,mult(X1,X1))),X1),X1),rd(X1,X1)),
inference(step,[status(thm)],[t54709,t34]) ).
cnf(t222023,plain,
mult(rd(X1,X1),mult(X1,X2)) = rd(mult(X1,mult(X2,mult(X1,X1))),mult(X1,X1)),
inference(step,[status(thm)],[t222022,t2335]) ).
cnf(t89954,plain,
rd(mult(X1,mult(X2,mult(X1,X1))),mult(X1,X1)) = mult(rd(X1,X1),mult(X1,X2)),
inference(orient,[status(thm)],[t222023]) ).
cnf(t222386,plain,
rd(mult(X1,mult(ld(X1,X3),X1)),X1) = ld(X1,mult(rd(X1,X1),mult(X1,X3))),
inference(step,[status(thm)],[t222385,t89954]) ).
cnf(t135512,plain,
ld(X1,mult(rd(X1,X1),mult(X1,X2))) = rd(mult(X1,mult(ld(X1,X2),X1)),X1),
inference(orient,[status(thm)],[t222386]) ).
cnf(t135520,plain,
rd(mult(X1,mult(ld(X1,mult(X2,X1)),X1)),X1) = ld(X1,mult(mult(X1,X2),X1)),
inference(cp,[status(thm)],[t135512,t25]) ).
cnf(t165248,plain,
rd(mult(X1,mult(ld(X1,mult(X2,X1)),X1)),X1) = ld(X1,mult(mult(X1,X2),X1)),
inference(orient,[status(thm)],[t135520]) ).
cnf(t165606,plain,
rd(X1,mult(X1,mult(ld(mult(ld(X1,mult(X2,X1)),X1),X1),X1))) = ld(X1,ld(X1,ld(X1,mult(mult(X1,X2),X1)))),
inference(cp,[status(thm)],[t119072,t165248]) ).
cnf(t473,plain,
rd(X1,ld(ld(X2,mult(X3,Y3)),Y3)) = mult(X1,mult(ld(mult(X2,Y3),X3),Y3)),
inference(cp,[status(thm)],[t196,t458]) ).
cnf(t8245,plain,
mult(X1,mult(ld(mult(X2,X3),Y3),X3)) = rd(X1,ld(ld(X2,mult(Y3,X3)),X3)),
inference(orient,[status(thm)],[t473]) ).
cnf(t222782,plain,
rd(X1,rd(X1,ld(ld(ld(X1,mult(X2,X1)),mult(X1,X1)),X1))) = ld(X1,ld(X1,ld(X1,mult(mult(X1,X2),X1)))),
inference(step,[status(thm)],[t165606,t8245]) ).
cnf(t222783,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)],[t222782,t23]) ).
cnf(t222784,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)],[t222783,t458]) ).
cnf(t4137,plain,
mult(X1,mult(X1,X2)) = ld(rd(rd(X1,mult(X1,X1)),X1),X2),
inference(cp,[status(thm)],[t4118,t1336]) ).
cnf(t221383,plain,
mult(X1,mult(X1,X2)) = ld(rd(rd(X1,X1),mult(X1,X1)),X2),
inference(step,[status(thm)],[t4137,t2384]) ).
cnf(t221384,plain,
mult(X1,mult(X1,X2)) = ld(rd(X1,mult(X1,mult(X1,X1))),X2),
inference(step,[status(thm)],[t221383,t1609]) ).
cnf(t4407,plain,
ld(rd(X1,mult(X1,mult(X1,X1))),X2) = mult(X1,mult(X1,X2)),
inference(orient,[status(thm)],[t221384]) ).
cnf(t4420,plain,
mult(X1,mult(X1,X2)) = ld(ld(true,rd(true,mult(X1,X1))),X2),
inference(cp,[status(thm)],[t4407,t3057]) ).
cnf(t4752,plain,
ld(ld(true,rd(true,mult(X1,X1))),X2) = mult(X1,mult(X1,X2)),
inference(orient,[status(thm)],[t4420]) ).
cnf(t4763,plain,
mult(X1,mult(X1,X2)) = ld(ld(X3,rd(X3,mult(X1,X1))),X2),
inference(cp,[status(thm)],[t4752,t391]) ).
cnf(t4950,plain,
ld(ld(X1,rd(X1,mult(X2,X2))),X3) = mult(X2,mult(X2,X3)),
inference(orient,[status(thm)],[t4763]) ).
cnf(t5017,plain,
mult(mult(X1,X1),mult(X2,mult(X1,X1))) = mult(mult(X1,mult(X1,X2)),mult(X1,X1)),
inference(cp,[status(thm)],[t3823,t4950]) ).
cnf(t14272,plain,
mult(mult(X1,mult(X1,X2)),mult(X1,X1)) = mult(mult(X1,X1),mult(X2,mult(X1,X1))),
inference(orient,[status(thm)],[t5017]) ).
cnf(t89987,plain,
mult(rd(X1,X1),mult(X1,mult(X1,mult(X1,X2)))) = rd(mult(X1,mult(mult(X1,X1),mult(X2,mult(X1,X1)))),mult(X1,X1)),
inference(cp,[status(thm)],[t89954,t14272]) ).
cnf(t222146,plain,
mult(rd(X1,X1),mult(X1,mult(X1,mult(X1,X2)))) = mult(mult(X1,mult(X1,X1)),X2),
inference(step,[status(thm)],[t89987,t44]) ).
cnf(t101564,plain,
mult(rd(X1,X1),mult(X1,mult(X1,mult(X1,X2)))) = mult(mult(X1,mult(X1,X1)),X2),
inference(orient,[status(thm)],[t222146]) ).
cnf(t101781,plain,
mult(X1,rd(mult(X1,mult(X1,X2)),X1)) = rd(mult(mult(X1,mult(X1,X1)),X2),X1),
inference(cp,[status(thm)],[t400,t101564]) ).
cnf(t102155,plain,
mult(X1,rd(mult(X1,mult(X1,X2)),X1)) = rd(mult(mult(X1,mult(X1,X1)),X2),X1),
inference(orient,[status(thm)],[t101781]) ).
cnf(t102314,plain,
rd(mult(X1,mult(X1,X2)),X1) = ld(X1,rd(mult(mult(X1,mult(X1,X1)),X2),X1)),
inference(cp,[status(thm)],[t12,t102155]) ).
cnf(t114930,plain,
ld(X1,rd(mult(mult(X1,mult(X1,X1)),X2),X1)) = rd(mult(X1,mult(X1,X2)),X1),
inference(orient,[status(thm)],[t102314]) ).
cnf(t114943,plain,
rd(mult(X1,mult(X1,mult(X1,mult(X2,X1)))),X1) = ld(X1,mult(mult(mult(X1,mult(X1,X1)),X1),X2)),
inference(cp,[status(thm)],[t114930,t44]) ).
cnf(t222448,plain,
rd(mult(X1,mult(X1,mult(X1,mult(X2,X1)))),X1) = ld(X1,mult(mult(mult(X1,X1),mult(X1,X1)),X2)),
inference(step,[status(thm)],[t114943,t1776]) ).
cnf(t222449,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)],[t222448,t1297]) ).
cnf(t20200,plain,
ld(ld(X1,X2),ld(ld(X1,X2),X3)) = mult(rd(ld(X2,X1),ld(X1,X2)),X3),
inference(cp,[status(thm)],[t20164,t225]) ).
cnf(t21302,plain,
ld(ld(X1,X2),ld(ld(X1,X2),X3)) = mult(rd(ld(X2,X1),ld(X1,X2)),X3),
inference(orient,[status(thm)],[t20200]) ).
cnf(t21371,plain,
mult(rd(ld(rd(X1,mult(X2,X2)),X1),ld(X1,rd(X1,mult(X2,X2)))),X3) = ld(ld(X1,rd(X1,mult(X2,X2))),mult(X2,mult(X2,X3))),
inference(cp,[status(thm)],[t21302,t4950]) ).
cnf(t221562,plain,
mult(mult(ld(rd(X1,mult(X2,X2)),X1),mult(X2,X2)),X3) = ld(ld(X1,rd(X1,mult(X2,X2))),mult(X2,mult(X2,X3))),
inference(step,[status(thm)],[t21371,t216]) ).
cnf(t221563,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)],[t221562,t24]) ).
cnf(t221564,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)],[t221563,t1297]) ).
cnf(t221565,plain,
mult(mult(X2,mult(X2,mult(X2,X2))),X3) = mult(X2,mult(X2,mult(X2,mult(X2,X3)))),
inference(step,[status(thm)],[t221564,t4950]) ).
cnf(t23248,plain,
mult(mult(X1,mult(X1,mult(X1,X1))),X2) = mult(X1,mult(X1,mult(X1,mult(X1,X2)))),
inference(orient,[status(thm)],[t221565]) ).
cnf(t222450,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)],[t222449,t23248]) ).
cnf(t222451,plain,
rd(mult(X1,mult(X1,mult(X1,mult(X2,X1)))),X1) = mult(X1,mult(X1,mult(X1,X2))),
inference(step,[status(thm)],[t222450,t12]) ).
cnf(t143764,plain,
rd(mult(X1,mult(X1,mult(X1,mult(X2,X1)))),X1) = mult(X1,mult(X1,mult(X1,X2))),
inference(orient,[status(thm)],[t222451]) ).
cnf(t143772,plain,
mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),X2))) = mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))))),X1),
inference(cp,[status(thm)],[t143764,t1178]) ).
cnf(t222641,plain,
rd(ld(X1,mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),X2)),X1)),X1) = mult(mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(rd(X1,mult(X1,X1)),mult(X2,rd(X1,mult(X1,X1)))))),X1),
inference(step,[status(thm)],[t143772,t3971]) ).
cnf(t222642,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)],[t222641,t3971]) ).
cnf(t222643,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)],[t222642,t8]) ).
cnf(t222644,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)],[t222643,t458]) ).
cnf(t222645,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)],[t222644,t10]) ).
cnf(t222646,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)],[t222645,t3971]) ).
cnf(t222647,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)],[t222646,t1433]) ).
cnf(t222648,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)],[t222647,t458]) ).
cnf(t222649,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)],[t222648,t3971]) ).
cnf(t222650,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)],[t222649,t8]) ).
cnf(t222651,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)],[t222650,t3971]) ).
cnf(t222652,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)],[t222651,t8]) ).
cnf(t222653,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)],[t222652,t458]) ).
cnf(t222654,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)],[t222653,t3971]) ).
cnf(t222655,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)],[t222654,t1433]) ).
cnf(t222656,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)],[t222655,t8]) ).
cnf(t222657,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)],[t222656,t458]) ).
cnf(t222658,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)],[t222657,t1135]) ).
cnf(t222659,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)],[t222658,t1433]) ).
cnf(t222660,plain,
rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = ld(X1,ld(X1,ld(X1,X2))),
inference(step,[status(thm)],[t222659,t8]) ).
cnf(t174582,plain,
rd(ld(X1,mult(ld(mult(X1,X1),X2),X1)),X1) = ld(X1,ld(X1,ld(X1,X2))),
inference(orient,[status(thm)],[t222660]) ).
cnf(t174763,plain,
ld(X1,mult(ld(mult(X1,X1),X2),X1)) = mult(ld(X1,ld(X1,ld(X1,X2))),X1),
inference(cp,[status(thm)],[t8,t174582]) ).
cnf(t175493,plain,
ld(X1,mult(ld(mult(X1,X1),X2),X1)) = mult(ld(X1,ld(X1,ld(X1,X2))),X1),
inference(orient,[status(thm)],[t174763]) ).
cnf(t222785,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)],[t222784,t175493]) ).
cnf(t222786,plain,
rd(X1,ld(ld(X1,mult(X2,X1)),mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),X1),
inference(step,[status(thm)],[t222785,t12]) ).
cnf(t195196,plain,
rd(X1,ld(ld(X1,mult(X2,X1)),mult(X1,X1))) = mult(ld(X1,ld(X1,X2)),X1),
inference(orient,[status(thm)],[t222786]) ).
cnf(t107773,plain,
rd(rd(rd(X1,mult(X1,X1)),rd(X1,mult(X1,X1))),ld(rd(X2,rd(X1,mult(X1,X1))),rd(X1,mult(X1,X1)))) = ld(rd(X1,mult(X1,X1)),ld(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),X1))),
inference(cp,[status(thm)],[t107737,t1178]) ).
cnf(t222218,plain,
rd(mult(rd(X1,mult(X1,X1)),X1),ld(rd(X2,rd(X1,mult(X1,X1))),rd(X1,mult(X1,X1)))) = ld(rd(X1,mult(X1,X1)),ld(rd(X1,mult(X1,X1)),mult(mult(rd(X1,mult(X1,X1)),X2),X1))),
inference(step,[status(thm)],[t107773,t1178]) ).
cnf(t222219,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)],[t222218,t2630]) ).
cnf(t222220,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)],[t222219,t992]) ).
cnf(t222221,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)],[t222220,t1178]) ).
cnf(t1459,plain,
rd(ld(X1,ld(X2,rd(X1,X1))),X1) = ld(mult(X2,X1),rd(X1,mult(X1,X1))),
inference(cp,[status(thm)],[t1433,t1091]) ).
cnf(t11188,plain,
ld(mult(X1,X2),rd(X2,mult(X2,X2))) = rd(ld(X2,ld(X1,rd(X2,X2))),X2),
inference(orient,[status(thm)],[t1459]) ).
cnf(t222222,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)],[t222221,t11188]) ).
cnf(t222223,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)],[t222222,t3295]) ).
cnf(t222224,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)],[t222223,t2936]) ).
cnf(t222225,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)],[t222224,t2936]) ).
cnf(t222226,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)],[t222225,t8]) ).
cnf(t222227,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)],[t222226,t44]) ).
cnf(t222228,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)],[t222227,t3971]) ).
cnf(t222229,plain,
mult(rd(X1,ld(X2,rd(X1,X1))),X1) = mult(mult(X1,X1),ld(X1,mult(X2,X1))),
inference(step,[status(thm)],[t222228,t8]) ).
cnf(t222230,plain,
mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(mult(X1,X1),ld(mult(X2,X1),X1)),
inference(step,[status(thm)],[t222229,t196]) ).
cnf(t109393,plain,
mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(mult(X1,X1),ld(mult(X2,X1),X1)),
inference(orient,[status(thm)],[t222230]) ).
cnf(t120183,plain,
rd(mult(X1,X1),ld(X2,X1)) = rd(X1,ld(X2,rd(X1,X1))),
inference(cp,[status(thm)],[t120155,t23]) ).
cnf(t120548,plain,
rd(mult(X1,X1),ld(X2,X1)) = rd(X1,ld(X2,rd(X1,X1))),
inference(orient,[status(thm)],[t120183]) ).
cnf(t222300,plain,
mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(X1,ld(mult(X2,X1),rd(X1,X1))),
inference(step,[status(thm)],[t109393,t120548]) ).
cnf(t222301,plain,
mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(X1,rd(ld(X1,ld(X2,X1)),X1)),
inference(step,[status(thm)],[t222300,t1433]) ).
cnf(t120551,plain,
mult(rd(X1,ld(X2,rd(X1,X1))),X1) = rd(X1,rd(ld(X1,ld(X2,X1)),X1)),
inference(orient,[status(thm)],[t222301]) ).
cnf(t195285,plain,
mult(ld(X1,ld(X1,rd(X1,ld(X2,rd(X1,X1))))),X1) = rd(X1,ld(ld(X1,rd(X1,rd(ld(X1,ld(X2,X1)),X1))),mult(X1,X1))),
inference(cp,[status(thm)],[t195196,t120551]) ).
cnf(t222787,plain,
mult(ld(X1,ld(rd(X1,X1),X2)),X1) = rd(X1,ld(ld(X1,rd(X1,rd(ld(X1,ld(X2,X1)),X1))),mult(X1,X1))),
inference(step,[status(thm)],[t195285,t225]) ).
cnf(t222788,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)],[t222787,t506]) ).
cnf(t1480,plain,
ld(rd(X1,X2),mult(X3,X2)) = ld(Y3,rd(Y3,rd(ld(X2,ld(X3,X1)),X2))),
inference(cp,[status(thm)],[t225,t1433]) ).
cnf(t221731,plain,
mult(X2,mult(ld(X1,X3),X2)) = ld(Y3,rd(Y3,rd(ld(X2,ld(X3,X1)),X2))),
inference(step,[status(thm)],[t1480,t83]) ).
cnf(t44128,plain,
ld(X1,rd(X1,rd(ld(X2,ld(X3,Y3)),X2))) = mult(X2,mult(ld(Y3,X3),X2)),
inference(orient,[status(thm)],[t221731]) ).
cnf(t222789,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)],[t222788,t44128]) ).
cnf(t222790,plain,
mult(mult(ld(X1,rd(X2,X1)),X1),X1) = mult(rd(X1,X1),mult(ld(X1,X2),X1)),
inference(step,[status(thm)],[t222789,t119462]) ).
cnf(t195654,plain,
mult(mult(ld(X1,rd(X2,X1)),X1),X1) = mult(rd(X1,X1),mult(ld(X1,X2),X1)),
inference(orient,[status(thm)],[t222790]) ).
cnf(t195951,plain,
mult(ld(X1,rd(X2,X1)),X1) = rd(mult(rd(X1,X1),mult(ld(X1,X2),X1)),X1),
inference(cp,[status(thm)],[t10,t195654]) ).
cnf(t212911,plain,
rd(mult(rd(X1,X1),mult(ld(X1,X2),X1)),X1) = mult(ld(X1,rd(X2,X1)),X1),
inference(orient,[status(thm)],[t195951]) ).
cnf(t219948,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),mult(ld(rd(X1,X1),X2),rd(X1,X1))) = mult(ld(rd(X1,X1),rd(X2,rd(X1,X1))),rd(X1,X1)),
inference(cp,[status(thm)],[t219919,t212911]) ).
cnf(t223044,plain,
mult(rd(X1,X1),mult(ld(rd(X1,X1),X2),rd(X1,X1))) = mult(ld(rd(X1,X1),rd(X2,rd(X1,X1))),rd(X1,X1)),
inference(step,[status(thm)],[t219948,t992]) ).
cnf(t223045,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)],[t223044,t219920]) ).
cnf(t223046,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)],[t223045,t196]) ).
cnf(t223047,plain,
X2 = mult(ld(rd(X1,X1),rd(X2,rd(X1,X1))),rd(X1,X1)),
inference(step,[status(thm)],[t223046,t23]) ).
cnf(t223048,plain,
X2 = ld(rd(X1,X1),rd(X2,rd(X1,X1))),
inference(step,[status(thm)],[t223047,t219920]) ).
cnf(t223049,plain,
X2 = ld(rd(X1,X1),X2),
inference(step,[status(thm)],[t223048,t219919]) ).
cnf(t220418,plain,
ld(rd(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t223049]) ).
cnf(t223118,plain,
mult(rd(X1,X1),X2) = X2,
inference(step,[status(thm)],[t223117,t220418]) ).
cnf(t220869,plain,
mult(rd(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t223118]) ).
cnf(t221030,plain,
true = ifeq(mult(sk0(rd(X1,X1)),rd(X1,X1)),sk0(rd(X1,X1)),ifeq(sk0(rd(X1,X1)),sk0(rd(X1,X1)),false,true),true),
inference(cp,[status(thm)],[t22,t220869]) ).
cnf(t223220,plain,
true = ifeq(sk0(rd(X1,X1)),sk0(rd(X1,X1)),ifeq(sk0(rd(X1,X1)),sk0(rd(X1,X1)),false,true),true),
inference(step,[status(thm)],[t221030,t219920]) ).
cnf(t0,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t9,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t223221,plain,
true = ifeq(sk0(rd(X1,X1)),sk0(rd(X1,X1)),false,true),
inference(step,[status(thm)],[t223220,t9]) ).
cnf(t223222,plain,
true = false,
inference(step,[status(thm)],[t223221,t9]) ).
cnf(t221220,plain,
false = true,
inference(orient,[status(thm)],[t223222]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t221220]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP655+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/10.38 % Computer : n003.cluster.edu
% 0.10/10.38 % Model : x86_64 x86_64
% 0.10/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.38 % Memory : 8046.5625MB
% 0.10/10.38 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Wed Sep 23 15:32:29 UTC 2026
% 0.10/10.38 % CPUTime :
% 0.10/10.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 53.44/18.17 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 53.44/18.17 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------