%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP701-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 : n001.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:28:05 PM UTC 2026
% Result : Unsatisfiable 32.08s 5.07s
% Output : CNFRefutation 32.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 225
% Number of leaves : 11
% Syntax : Number of clauses : 970 ( 970 unt; 0 nHn; 4 RR)
% Number of literals : 970 ( 969 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 1880 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t4]) ).
cnf(t9,axiom,
mult(mult(mult(X1,X2),X1),mult(X1,X3)) = mult(X1,mult(mult(mult(X2,X1),X1),X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t24,plain,
mult(mult(mult(X1,X2),X1),mult(X1,X3)) = mult(X1,mult(mult(mult(X2,X1),X1),X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t5,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t10,plain,
mult(X1,ld(X1,X2)) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t25,plain,
mult(X1,mult(mult(mult(ld(X1,X2),X1),X1),X3)) = mult(mult(X2,X1),mult(X1,X3)),
inference(cp,[status(thm)],[t24,t10]) ).
cnf(t431,plain,
mult(X1,mult(mult(mult(ld(X1,X2),X1),X1),X3)) = mult(mult(X2,X1),mult(X1,X3)),
inference(orient,[status(thm)],[t25]) ).
cnf(t7,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t16,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t0,axiom,
mult(X1,unit) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
mult(X1,unit) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t29,plain,
mult(X1,mult(mult(mult(X2,X1),X1),unit)) = mult(mult(mult(X1,X2),X1),X1),
inference(cp,[status(thm)],[t24,t11]) ).
cnf(t114669,plain,
mult(X1,mult(mult(X2,X1),X1)) = mult(mult(mult(X1,X2),X1),X1),
inference(step,[status(thm)],[t29,t11]) ).
cnf(t144,plain,
mult(mult(mult(X1,X2),X1),X1) = mult(X1,mult(mult(X2,X1),X1)),
inference(orient,[status(thm)],[t114669]) ).
cnf(t148,plain,
mult(X1,mult(mult(ld(X1,X2),X1),X1)) = mult(mult(X2,X1),X1),
inference(cp,[status(thm)],[t144,t10]) ).
cnf(t558,plain,
mult(X1,mult(mult(ld(X1,X2),X1),X1)) = mult(mult(X2,X1),X1),
inference(orient,[status(thm)],[t148]) ).
cnf(t570,plain,
mult(mult(ld(X1,X2),X1),X1) = ld(X1,mult(mult(X2,X1),X1)),
inference(cp,[status(thm)],[t20,t558]) ).
cnf(t700,plain,
ld(X1,mult(mult(X2,X1),X1)) = mult(mult(ld(X1,X2),X1),X1),
inference(orient,[status(thm)],[t570]) ).
cnf(t6,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t14,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t714,plain,
mult(mult(ld(X1,rd(X2,X1)),X1),X1) = ld(X1,mult(X2,X1)),
inference(cp,[status(thm)],[t700,t14]) ).
cnf(t2029,plain,
mult(mult(ld(X1,rd(X2,X1)),X1),X1) = ld(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t714]) ).
cnf(t2053,plain,
mult(ld(X1,rd(X2,X1)),X1) = rd(ld(X1,mult(X2,X1)),X1),
inference(cp,[status(thm)],[t16,t2029]) ).
cnf(t2074,plain,
mult(ld(X1,rd(X2,X1)),X1) = rd(ld(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t2053]) ).
cnf(t2098,plain,
ld(X1,rd(X2,X1)) = rd(rd(ld(X1,mult(X2,X1)),X1),X1),
inference(cp,[status(thm)],[t16,t2074]) ).
cnf(t2846,plain,
rd(rd(ld(X1,mult(X2,X1)),X1),X1) = ld(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t2098]) ).
cnf(t2879,plain,
ld(X1,rd(rd(X2,X1),X1)) = rd(rd(ld(X1,X2),X1),X1),
inference(cp,[status(thm)],[t2846,t14]) ).
cnf(t2897,plain,
ld(X1,rd(rd(X2,X1),X1)) = rd(rd(ld(X1,X2),X1),X1),
inference(orient,[status(thm)],[t2879]) ).
cnf(t2931,plain,
mult(mult(rd(rd(X1,X2),X2),X2),mult(X2,X3)) = mult(X2,mult(mult(mult(rd(rd(ld(X2,X1),X2),X2),X2),X2),X3)),
inference(cp,[status(thm)],[t431,t2897]) ).
cnf(t114810,plain,
mult(rd(X1,X2),mult(X2,X3)) = mult(X2,mult(mult(mult(rd(rd(ld(X2,X1),X2),X2),X2),X2),X3)),
inference(step,[status(thm)],[t2931,t14]) ).
cnf(t114811,plain,
mult(rd(X1,X2),mult(X2,X3)) = mult(X2,mult(mult(rd(ld(X2,X1),X2),X2),X3)),
inference(step,[status(thm)],[t114810,t14]) ).
cnf(t114812,plain,
mult(rd(X1,X2),mult(X2,X3)) = mult(X2,mult(ld(X2,X1),X3)),
inference(step,[status(thm)],[t114811,t14]) ).
cnf(t2932,plain,
mult(rd(X1,X2),mult(X2,X3)) = mult(X2,mult(ld(X2,X1),X3)),
inference(orient,[status(thm)],[t114812]) ).
cnf(t2,axiom,
mult(X1,i(X1)) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t36,plain,
mult(X1,i(X1)) = unit,
inference(orient,[status(thm)],[t2]) ).
cnf(t2967,plain,
mult(X1,mult(ld(X1,X2),i(X1))) = mult(rd(X2,X1),unit),
inference(cp,[status(thm)],[t2932,t36]) ).
cnf(t114813,plain,
mult(X1,mult(ld(X1,X2),i(X1))) = rd(X2,X1),
inference(step,[status(thm)],[t2967,t11]) ).
cnf(t3034,plain,
mult(X1,mult(ld(X1,X2),i(X1))) = rd(X2,X1),
inference(orient,[status(thm)],[t114813]) ).
cnf(t3039,plain,
rd(mult(X1,X2),X1) = mult(X1,mult(X2,i(X1))),
inference(cp,[status(thm)],[t3034,t20]) ).
cnf(t3082,plain,
mult(X1,mult(X2,i(X1))) = rd(mult(X1,X2),X1),
inference(orient,[status(thm)],[t3039]) ).
cnf(t3105,plain,
mult(X1,i(X2)) = ld(X2,rd(mult(X2,X1),X2)),
inference(cp,[status(thm)],[t20,t3082]) ).
cnf(t8,axiom,
mult(mult(X1,mult(X2,mult(X2,X3))),X2) = mult(mult(X1,X2),mult(X2,mult(X3,X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t42,plain,
mult(mult(X1,mult(X2,mult(X2,X3))),X2) = mult(mult(X1,X2),mult(X2,mult(X3,X2))),
inference(orient,[status(thm)],[t8]) ).
cnf(t1,axiom,
mult(unit,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t12,plain,
mult(unit,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t45,plain,
mult(mult(unit,X1),mult(X1,mult(X2,X1))) = mult(mult(X1,mult(X1,X2)),X1),
inference(cp,[status(thm)],[t42,t12]) ).
cnf(t114670,plain,
mult(X1,mult(X1,mult(X2,X1))) = mult(mult(X1,mult(X1,X2)),X1),
inference(step,[status(thm)],[t45,t12]) ).
cnf(t164,plain,
mult(mult(X1,mult(X1,X2)),X1) = mult(X1,mult(X1,mult(X2,X1))),
inference(orient,[status(thm)],[t114670]) ).
cnf(t177,plain,
mult(X1,mult(X1,X2)) = rd(mult(X1,mult(X1,mult(X2,X1))),X1),
inference(cp,[status(thm)],[t16,t164]) ).
cnf(t1793,plain,
rd(mult(X1,mult(X1,mult(X2,X1))),X1) = mult(X1,mult(X1,X2)),
inference(orient,[status(thm)],[t177]) ).
cnf(t1823,plain,
mult(X1,mult(X1,rd(X2,X1))) = rd(mult(X1,mult(X1,X2)),X1),
inference(cp,[status(thm)],[t1793,t14]) ).
cnf(t1837,plain,
mult(X1,mult(X1,rd(X2,X1))) = rd(mult(X1,mult(X1,X2)),X1),
inference(orient,[status(thm)],[t1823]) ).
cnf(t1861,plain,
mult(X1,rd(X2,X1)) = ld(X1,rd(mult(X1,mult(X1,X2)),X1)),
inference(cp,[status(thm)],[t20,t1837]) ).
cnf(t2659,plain,
ld(X1,rd(mult(X1,mult(X1,X2)),X1)) = mult(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t1861]) ).
cnf(t2669,plain,
mult(X1,rd(ld(X1,X2),X1)) = ld(X1,rd(mult(X1,X2),X1)),
inference(cp,[status(thm)],[t2659,t10]) ).
cnf(t2709,plain,
ld(X1,rd(mult(X1,X2),X1)) = mult(X1,rd(ld(X1,X2),X1)),
inference(orient,[status(thm)],[t2669]) ).
cnf(t114814,plain,
mult(X1,i(X2)) = mult(X2,rd(ld(X2,X1),X2)),
inference(step,[status(thm)],[t3105,t2709]) ).
cnf(t3130,plain,
mult(X1,rd(ld(X1,X2),X1)) = mult(X2,i(X1)),
inference(orient,[status(thm)],[t114814]) ).
cnf(t3137,plain,
mult(mult(X1,X2),i(X1)) = mult(X1,rd(X2,X1)),
inference(cp,[status(thm)],[t3130,t20]) ).
cnf(t3182,plain,
mult(mult(X1,X2),i(X1)) = mult(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t3137]) ).
cnf(t39,plain,
X1 = rd(unit,i(X1)),
inference(cp,[status(thm)],[t16,t36]) ).
cnf(t3,axiom,
mult(i(X1),X1) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t58,plain,
mult(i(X1),X1) = unit,
inference(orient,[status(thm)],[t3]) ).
cnf(t61,plain,
i(X1) = rd(unit,X1),
inference(cp,[status(thm)],[t16,t58]) ).
cnf(t70,plain,
rd(unit,X1) = i(X1),
inference(orient,[status(thm)],[t61]) ).
cnf(t114664,plain,
X1 = i(i(X1)),
inference(step,[status(thm)],[t39,t70]) ).
cnf(t71,plain,
i(i(X1)) = X1,
inference(orient,[status(thm)],[t114664]) ).
cnf(t3220,plain,
mult(i(X1),rd(X2,i(X1))) = mult(mult(i(X1),X2),X1),
inference(cp,[status(thm)],[t3182,t71]) ).
cnf(t4609,plain,
mult(i(X1),rd(X2,i(X1))) = mult(mult(i(X1),X2),X1),
inference(orient,[status(thm)],[t3220]) ).
cnf(t4637,plain,
rd(X1,i(X2)) = ld(i(X2),mult(mult(i(X2),X1),X2)),
inference(cp,[status(thm)],[t20,t4609]) ).
cnf(t6685,plain,
ld(i(X1),mult(mult(i(X1),X2),X1)) = rd(X2,i(X1)),
inference(orient,[status(thm)],[t4637]) ).
cnf(t6689,plain,
rd(mult(X1,mult(X1,X2)),i(X1)) = ld(i(X1),mult(mult(i(X1),X1),mult(X1,mult(X2,X1)))),
inference(cp,[status(thm)],[t6685,t42]) ).
cnf(t166,plain,
mult(X1,mult(X1,mult(ld(X1,X2),X1))) = mult(mult(X1,X2),X1),
inference(cp,[status(thm)],[t164,t10]) ).
cnf(t805,plain,
mult(X1,mult(X1,mult(ld(X1,X2),X1))) = mult(mult(X1,X2),X1),
inference(orient,[status(thm)],[t166]) ).
cnf(t815,plain,
mult(X1,mult(ld(X1,X2),X1)) = ld(X1,mult(mult(X1,X2),X1)),
inference(cp,[status(thm)],[t20,t805]) ).
cnf(t827,plain,
ld(X1,mult(mult(X1,X2),X1)) = mult(X1,mult(ld(X1,X2),X1)),
inference(orient,[status(thm)],[t815]) ).
cnf(t48,plain,
mult(mult(X1,X2),mult(X2,mult(unit,X2))) = mult(mult(X1,mult(X2,X2)),X2),
inference(cp,[status(thm)],[t42,t11]) ).
cnf(t114671,plain,
mult(mult(X1,X2),mult(X2,X2)) = mult(mult(X1,mult(X2,X2)),X2),
inference(step,[status(thm)],[t48,t12]) ).
cnf(t185,plain,
mult(mult(X1,mult(X2,X2)),X2) = mult(mult(X1,X2),mult(X2,X2)),
inference(orient,[status(thm)],[t114671]) ).
cnf(t186,plain,
mult(mult(i(mult(X1,X1)),X1),mult(X1,X1)) = mult(unit,X1),
inference(cp,[status(thm)],[t185,t58]) ).
cnf(t114673,plain,
mult(mult(i(mult(X1,X1)),X1),mult(X1,X1)) = X1,
inference(step,[status(thm)],[t186,t12]) ).
cnf(t215,plain,
mult(mult(i(mult(X1,X1)),X1),mult(X1,X1)) = X1,
inference(orient,[status(thm)],[t114673]) ).
cnf(t222,plain,
mult(i(mult(X1,X1)),X1) = rd(X1,mult(X1,X1)),
inference(cp,[status(thm)],[t16,t215]) ).
cnf(t229,plain,
mult(i(mult(X1,X1)),X1) = rd(X1,mult(X1,X1)),
inference(orient,[status(thm)],[t222]) ).
cnf(t234,plain,
i(mult(X1,X1)) = rd(rd(X1,mult(X1,X1)),X1),
inference(cp,[status(thm)],[t16,t229]) ).
cnf(t242,plain,
rd(rd(X1,mult(X1,X1)),X1) = i(mult(X1,X1)),
inference(orient,[status(thm)],[t234]) ).
cnf(t26,plain,
mult(X1,mult(mult(mult(unit,X1),X1),X2)) = mult(mult(X1,X1),mult(X1,X2)),
inference(cp,[status(thm)],[t24,t11]) ).
cnf(t114665,plain,
mult(X1,mult(mult(X1,X1),X2)) = mult(mult(X1,X1),mult(X1,X2)),
inference(step,[status(thm)],[t26,t12]) ).
cnf(t74,plain,
mult(mult(X1,X1),mult(X1,X2)) = mult(X1,mult(mult(X1,X1),X2)),
inference(orient,[status(thm)],[t114665]) ).
cnf(t76,plain,
mult(X1,mult(mult(X1,X1),ld(X1,X2))) = mult(mult(X1,X1),X2),
inference(cp,[status(thm)],[t74,t10]) ).
cnf(t260,plain,
mult(X1,mult(mult(X1,X1),ld(X1,X2))) = mult(mult(X1,X1),X2),
inference(orient,[status(thm)],[t76]) ).
cnf(t269,plain,
mult(mult(X1,X1),ld(X1,X2)) = ld(X1,mult(mult(X1,X1),X2)),
inference(cp,[status(thm)],[t20,t260]) ).
cnf(t276,plain,
ld(X1,mult(mult(X1,X1),X2)) = mult(mult(X1,X1),ld(X1,X2)),
inference(orient,[status(thm)],[t269]) ).
cnf(t75,plain,
mult(X1,mult(mult(X1,X1),i(X1))) = mult(mult(X1,X1),unit),
inference(cp,[status(thm)],[t74,t36]) ).
cnf(t114667,plain,
mult(X1,mult(mult(X1,X1),i(X1))) = mult(X1,X1),
inference(step,[status(thm)],[t75,t11]) ).
cnf(t103,plain,
mult(X1,mult(mult(X1,X1),i(X1))) = mult(X1,X1),
inference(orient,[status(thm)],[t114667]) ).
cnf(t107,plain,
mult(mult(X1,X1),i(X1)) = ld(X1,mult(X1,X1)),
inference(cp,[status(thm)],[t20,t103]) ).
cnf(t114668,plain,
mult(mult(X1,X1),i(X1)) = X1,
inference(step,[status(thm)],[t107,t20]) ).
cnf(t112,plain,
mult(mult(X1,X1),i(X1)) = X1,
inference(orient,[status(thm)],[t114668]) ).
cnf(t277,plain,
mult(mult(X1,X1),ld(X1,i(X1))) = ld(X1,X1),
inference(cp,[status(thm)],[t276,t112]) ).
cnf(t21,plain,
unit = ld(X1,X1),
inference(cp,[status(thm)],[t20,t11]) ).
cnf(t68,plain,
ld(X1,X1) = unit,
inference(orient,[status(thm)],[t21]) ).
cnf(t114675,plain,
mult(mult(X1,X1),ld(X1,i(X1))) = unit,
inference(step,[status(thm)],[t277,t68]) ).
cnf(t287,plain,
mult(mult(X1,X1),ld(X1,i(X1))) = unit,
inference(orient,[status(thm)],[t114675]) ).
cnf(t292,plain,
ld(X1,i(X1)) = ld(mult(X1,X1),unit),
inference(cp,[status(thm)],[t20,t287]) ).
cnf(t38,plain,
i(X1) = ld(X1,unit),
inference(cp,[status(thm)],[t20,t36]) ).
cnf(t69,plain,
ld(X1,unit) = i(X1),
inference(orient,[status(thm)],[t38]) ).
cnf(t114676,plain,
ld(X1,i(X1)) = i(mult(X1,X1)),
inference(step,[status(thm)],[t292,t69]) ).
cnf(t300,plain,
i(mult(X1,X1)) = ld(X1,i(X1)),
inference(orient,[status(thm)],[t114676]) ).
cnf(t114677,plain,
rd(rd(X1,mult(X1,X1)),X1) = ld(X1,i(X1)),
inference(step,[status(thm)],[t242,t300]) ).
cnf(t301,plain,
rd(rd(X1,mult(X1,X1)),X1) = ld(X1,i(X1)),
inference(orient,[status(thm)],[t114677]) ).
cnf(t114680,plain,
mult(ld(X1,i(X1)),X1) = rd(X1,mult(X1,X1)),
inference(step,[status(thm)],[t229,t300]) ).
cnf(t321,plain,
mult(ld(X1,i(X1)),X1) = rd(X1,mult(X1,X1)),
inference(rw,[status(thm)],[t114680]) ).
cnf(t380,plain,
mult(ld(X1,i(X1)),X1) = rd(X1,mult(X1,X1)),
inference(orient,[status(thm)],[t321]) ).
cnf(t559,plain,
mult(mult(i(X1),X1),X1) = mult(X1,mult(rd(X1,mult(X1,X1)),X1)),
inference(cp,[status(thm)],[t558,t380]) ).
cnf(t114692,plain,
mult(unit,X1) = mult(X1,mult(rd(X1,mult(X1,X1)),X1)),
inference(step,[status(thm)],[t559,t58]) ).
cnf(t114693,plain,
X1 = mult(X1,mult(rd(X1,mult(X1,X1)),X1)),
inference(step,[status(thm)],[t114692,t12]) ).
cnf(t579,plain,
mult(X1,mult(rd(X1,mult(X1,X1)),X1)) = X1,
inference(orient,[status(thm)],[t114693]) ).
cnf(t583,plain,
mult(rd(X1,mult(X1,X1)),X1) = ld(X1,X1),
inference(cp,[status(thm)],[t20,t579]) ).
cnf(t114694,plain,
mult(rd(X1,mult(X1,X1)),X1) = unit,
inference(step,[status(thm)],[t583,t68]) ).
cnf(t592,plain,
mult(rd(X1,mult(X1,X1)),X1) = unit,
inference(orient,[status(thm)],[t114694]) ).
cnf(t597,plain,
rd(X1,mult(X1,X1)) = rd(unit,X1),
inference(cp,[status(thm)],[t16,t592]) ).
cnf(t114695,plain,
rd(X1,mult(X1,X1)) = i(X1),
inference(step,[status(thm)],[t597,t70]) ).
cnf(t605,plain,
rd(X1,mult(X1,X1)) = i(X1),
inference(orient,[status(thm)],[t114695]) ).
cnf(t114699,plain,
rd(i(X1),X1) = ld(X1,i(X1)),
inference(step,[status(thm)],[t301,t605]) ).
cnf(t613,plain,
rd(i(X1),X1) = ld(X1,i(X1)),
inference(rw,[status(thm)],[t114699]) ).
cnf(t630,plain,
ld(X1,i(X1)) = rd(i(X1),X1),
inference(orient,[status(thm)],[t613]) ).
cnf(t637,plain,
i(X1) = mult(X1,rd(i(X1),X1)),
inference(cp,[status(thm)],[t10,t630]) ).
cnf(t653,plain,
mult(X1,rd(i(X1),X1)) = i(X1),
inference(orient,[status(thm)],[t637]) ).
cnf(t831,plain,
mult(X1,mult(ld(X1,rd(i(X1),X1)),X1)) = ld(X1,mult(i(X1),X1)),
inference(cp,[status(thm)],[t827,t653]) ).
cnf(t114727,plain,
mult(X1,mult(ld(X1,rd(i(X1),X1)),X1)) = ld(X1,unit),
inference(step,[status(thm)],[t831,t58]) ).
cnf(t114728,plain,
mult(X1,mult(ld(X1,rd(i(X1),X1)),X1)) = i(X1),
inference(step,[status(thm)],[t114727,t69]) ).
cnf(t911,plain,
mult(X1,mult(ld(X1,rd(i(X1),X1)),X1)) = i(X1),
inference(orient,[status(thm)],[t114728]) ).
cnf(t916,plain,
mult(ld(X1,rd(i(X1),X1)),X1) = ld(X1,i(X1)),
inference(cp,[status(thm)],[t20,t911]) ).
cnf(t114729,plain,
mult(ld(X1,rd(i(X1),X1)),X1) = rd(i(X1),X1),
inference(step,[status(thm)],[t916,t630]) ).
cnf(t925,plain,
mult(ld(X1,rd(i(X1),X1)),X1) = rd(i(X1),X1),
inference(orient,[status(thm)],[t114729]) ).
cnf(t931,plain,
ld(X1,rd(i(X1),X1)) = rd(rd(i(X1),X1),X1),
inference(cp,[status(thm)],[t16,t925]) ).
cnf(t942,plain,
ld(X1,rd(i(X1),X1)) = rd(rd(i(X1),X1),X1),
inference(orient,[status(thm)],[t931]) ).
cnf(t948,plain,
rd(i(X1),X1) = mult(X1,rd(rd(i(X1),X1),X1)),
inference(cp,[status(thm)],[t10,t942]) ).
cnf(t1002,plain,
mult(X1,rd(rd(i(X1),X1),X1)) = rd(i(X1),X1),
inference(orient,[status(thm)],[t948]) ).
cnf(t1014,plain,
mult(mult(X1,X2),mult(X2,mult(rd(rd(i(X2),X2),X2),X2))) = mult(mult(X1,mult(X2,rd(i(X2),X2))),X2),
inference(cp,[status(thm)],[t42,t1002]) ).
cnf(t114743,plain,
mult(mult(X1,X2),mult(X2,rd(i(X2),X2))) = mult(mult(X1,mult(X2,rd(i(X2),X2))),X2),
inference(step,[status(thm)],[t1014,t14]) ).
cnf(t114744,plain,
mult(mult(X1,X2),i(X2)) = mult(mult(X1,mult(X2,rd(i(X2),X2))),X2),
inference(step,[status(thm)],[t114743,t653]) ).
cnf(t114745,plain,
mult(mult(X1,X2),i(X2)) = mult(mult(X1,i(X2)),X2),
inference(step,[status(thm)],[t114744,t653]) ).
cnf(t1017,plain,
mult(mult(X1,i(X2)),X2) = mult(mult(X1,X2),i(X2)),
inference(orient,[status(thm)],[t114745]) ).
cnf(t1033,plain,
mult(X1,i(X2)) = rd(mult(mult(X1,X2),i(X2)),X2),
inference(cp,[status(thm)],[t16,t1017]) ).
cnf(t1174,plain,
rd(mult(mult(X1,X2),i(X2)),X2) = mult(X1,i(X2)),
inference(orient,[status(thm)],[t1033]) ).
cnf(t3184,plain,
mult(X1,rd(rd(ld(X1,X2),X1),X1)) = mult(mult(X2,i(X1)),i(X1)),
inference(cp,[status(thm)],[t3182,t3130]) ).
cnf(t158,plain,
mult(mult(X1,X2),X1) = rd(mult(X1,mult(mult(X2,X1),X1)),X1),
inference(cp,[status(thm)],[t16,t144]) ).
cnf(t760,plain,
rd(mult(X1,mult(mult(X2,X1),X1)),X1) = mult(mult(X1,X2),X1),
inference(orient,[status(thm)],[t158]) ).
cnf(t779,plain,
mult(mult(X1,rd(X2,X1)),X1) = rd(mult(X1,mult(X2,X1)),X1),
inference(cp,[status(thm)],[t760,t14]) ).
cnf(t783,plain,
mult(mult(X1,rd(X2,X1)),X1) = rd(mult(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t779]) ).
cnf(t795,plain,
mult(X1,rd(X2,X1)) = rd(rd(mult(X1,mult(X2,X1)),X1),X1),
inference(cp,[status(thm)],[t16,t783]) ).
cnf(t2118,plain,
rd(rd(mult(X1,mult(X2,X1)),X1),X1) = mult(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t795]) ).
cnf(t2149,plain,
mult(X1,rd(rd(X2,X1),X1)) = rd(rd(mult(X1,X2),X1),X1),
inference(cp,[status(thm)],[t2118,t14]) ).
cnf(t2212,plain,
mult(X1,rd(rd(X2,X1),X1)) = rd(rd(mult(X1,X2),X1),X1),
inference(orient,[status(thm)],[t2149]) ).
cnf(t114817,plain,
rd(rd(mult(X1,ld(X1,X2)),X1),X1) = mult(mult(X2,i(X1)),i(X1)),
inference(step,[status(thm)],[t3184,t2212]) ).
cnf(t114818,plain,
rd(rd(X2,X1),X1) = mult(mult(X2,i(X1)),i(X1)),
inference(step,[status(thm)],[t114817,t10]) ).
cnf(t3384,plain,
mult(mult(X1,i(X2)),i(X2)) = rd(rd(X1,X2),X2),
inference(orient,[status(thm)],[t114818]) ).
cnf(t3418,plain,
mult(mult(X1,i(X2)),i(i(X2))) = rd(mult(rd(rd(X1,X2),X2),i(i(X2))),i(X2)),
inference(cp,[status(thm)],[t1174,t3384]) ).
cnf(t114819,plain,
mult(mult(X1,i(X2)),X2) = rd(mult(rd(rd(X1,X2),X2),i(i(X2))),i(X2)),
inference(step,[status(thm)],[t3418,t71]) ).
cnf(t114820,plain,
mult(mult(X1,X2),i(X2)) = rd(mult(rd(rd(X1,X2),X2),i(i(X2))),i(X2)),
inference(step,[status(thm)],[t114819,t1017]) ).
cnf(t114821,plain,
mult(mult(X1,X2),i(X2)) = rd(mult(rd(rd(X1,X2),X2),X2),i(X2)),
inference(step,[status(thm)],[t114820,t71]) ).
cnf(t114822,plain,
mult(mult(X1,X2),i(X2)) = rd(rd(X1,X2),i(X2)),
inference(step,[status(thm)],[t114821,t14]) ).
cnf(t3441,plain,
mult(mult(X1,X2),i(X2)) = rd(rd(X1,X2),i(X2)),
inference(orient,[status(thm)],[t114822]) ).
cnf(t3466,plain,
rd(rd(mult(mult(X1,X2),X1),X1),i(X1)) = mult(mult(X1,mult(mult(X2,X1),X1)),i(X1)),
inference(cp,[status(thm)],[t3441,t144]) ).
cnf(t114827,plain,
rd(mult(X1,X2),i(X1)) = mult(mult(X1,mult(mult(X2,X1),X1)),i(X1)),
inference(step,[status(thm)],[t3466,t16]) ).
cnf(t114828,plain,
rd(mult(X1,X2),i(X1)) = mult(X1,rd(mult(mult(X2,X1),X1),X1)),
inference(step,[status(thm)],[t114827,t3182]) ).
cnf(t114829,plain,
rd(mult(X1,X2),i(X1)) = mult(X1,mult(X2,X1)),
inference(step,[status(thm)],[t114828,t16]) ).
cnf(t3519,plain,
rd(mult(X1,X2),i(X1)) = mult(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t114829]) ).
cnf(t114915,plain,
mult(X1,mult(mult(X1,X2),X1)) = ld(i(X1),mult(mult(i(X1),X1),mult(X1,mult(X2,X1)))),
inference(step,[status(thm)],[t6689,t3519]) ).
cnf(t114916,plain,
mult(X1,mult(mult(X1,X2),X1)) = ld(i(X1),mult(unit,mult(X1,mult(X2,X1)))),
inference(step,[status(thm)],[t114915,t58]) ).
cnf(t114917,plain,
mult(X1,mult(mult(X1,X2),X1)) = ld(i(X1),mult(X1,mult(X2,X1))),
inference(step,[status(thm)],[t114916,t12]) ).
cnf(t951,plain,
mult(mult(rd(i(X1),X1),X1),mult(X1,X2)) = mult(X1,mult(mult(mult(rd(rd(i(X1),X1),X1),X1),X1),X2)),
inference(cp,[status(thm)],[t431,t942]) ).
cnf(t114740,plain,
mult(i(X1),mult(X1,X2)) = mult(X1,mult(mult(mult(rd(rd(i(X1),X1),X1),X1),X1),X2)),
inference(step,[status(thm)],[t951,t14]) ).
cnf(t114741,plain,
mult(i(X1),mult(X1,X2)) = mult(X1,mult(mult(rd(i(X1),X1),X1),X2)),
inference(step,[status(thm)],[t114740,t14]) ).
cnf(t114742,plain,
mult(i(X1),mult(X1,X2)) = mult(X1,mult(i(X1),X2)),
inference(step,[status(thm)],[t114741,t14]) ).
cnf(t966,plain,
mult(i(X1),mult(X1,X2)) = mult(X1,mult(i(X1),X2)),
inference(orient,[status(thm)],[t114742]) ).
cnf(t974,plain,
mult(X1,mult(i(X1),ld(X1,X2))) = mult(i(X1),X2),
inference(cp,[status(thm)],[t966,t10]) ).
cnf(t1102,plain,
mult(X1,mult(i(X1),ld(X1,X2))) = mult(i(X1),X2),
inference(orient,[status(thm)],[t974]) ).
cnf(t1118,plain,
mult(i(X1),ld(X1,X2)) = ld(X1,mult(i(X1),X2)),
inference(cp,[status(thm)],[t20,t1102]) ).
cnf(t1130,plain,
ld(X1,mult(i(X1),X2)) = mult(i(X1),ld(X1,X2)),
inference(orient,[status(thm)],[t1118]) ).
cnf(t1139,plain,
mult(i(i(X1)),ld(i(X1),X2)) = ld(i(X1),mult(X1,X2)),
inference(cp,[status(thm)],[t1130,t71]) ).
cnf(t114756,plain,
mult(X1,ld(i(X1),X2)) = ld(i(X1),mult(X1,X2)),
inference(step,[status(thm)],[t1139,t71]) ).
cnf(t1146,plain,
ld(i(X1),mult(X1,X2)) = mult(X1,ld(i(X1),X2)),
inference(orient,[status(thm)],[t114756]) ).
cnf(t114918,plain,
mult(X1,mult(mult(X1,X2),X1)) = mult(X1,ld(i(X1),mult(X2,X1))),
inference(step,[status(thm)],[t114917,t1146]) ).
cnf(t8013,plain,
mult(X1,ld(i(X1),mult(X2,X1))) = mult(X1,mult(mult(X1,X2),X1)),
inference(orient,[status(thm)],[t114918]) ).
cnf(t8087,plain,
ld(i(X1),mult(X2,X1)) = ld(X1,mult(X1,mult(mult(X1,X2),X1))),
inference(cp,[status(thm)],[t20,t8013]) ).
cnf(t114927,plain,
ld(i(X1),mult(X2,X1)) = mult(mult(X1,X2),X1),
inference(step,[status(thm)],[t8087,t20]) ).
cnf(t8213,plain,
ld(i(X1),mult(X2,X1)) = mult(mult(X1,X2),X1),
inference(orient,[status(thm)],[t114927]) ).
cnf(t2119,plain,
mult(X1,rd(mult(mult(ld(X1,X2),X1),X1),X1)) = rd(rd(mult(mult(X2,X1),mult(X1,X1)),X1),X1),
inference(cp,[status(thm)],[t2118,t431]) ).
cnf(t114791,plain,
mult(X1,mult(ld(X1,X2),X1)) = rd(rd(mult(mult(X2,X1),mult(X1,X1)),X1),X1),
inference(step,[status(thm)],[t2119,t16]) ).
cnf(t197,plain,
mult(X1,mult(X2,X2)) = rd(mult(mult(X1,X2),mult(X2,X2)),X2),
inference(cp,[status(thm)],[t16,t185]) ).
cnf(t1878,plain,
rd(mult(mult(X1,X2),mult(X2,X2)),X2) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t197]) ).
cnf(t114792,plain,
mult(X1,mult(ld(X1,X2),X1)) = rd(mult(X2,mult(X1,X1)),X1),
inference(step,[status(thm)],[t114791,t1878]) ).
cnf(t2165,plain,
mult(X1,mult(ld(X1,X2),X1)) = rd(mult(X2,mult(X1,X1)),X1),
inference(orient,[status(thm)],[t114792]) ).
cnf(t114793,plain,
ld(X1,mult(mult(X1,X2),X1)) = rd(mult(X2,mult(X1,X1)),X1),
inference(step,[status(thm)],[t827,t2165]) ).
cnf(t2166,plain,
ld(X1,mult(mult(X1,X2),X1)) = rd(mult(X2,mult(X1,X1)),X1),
inference(orient,[status(thm)],[t114793]) ).
cnf(t2196,plain,
rd(mult(mult(ld(X1,X2),X1),mult(X1,X1)),X1) = ld(X1,mult(rd(mult(X2,mult(X1,X1)),X1),X1)),
inference(cp,[status(thm)],[t2166,t2165]) ).
cnf(t114800,plain,
mult(ld(X1,X2),mult(X1,X1)) = ld(X1,mult(rd(mult(X2,mult(X1,X1)),X1),X1)),
inference(step,[status(thm)],[t2196,t1878]) ).
cnf(t114801,plain,
mult(ld(X1,X2),mult(X1,X1)) = ld(X1,mult(X2,mult(X1,X1))),
inference(step,[status(thm)],[t114800,t14]) ).
cnf(t2361,plain,
ld(X1,mult(X2,mult(X1,X1))) = mult(ld(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t114801]) ).
cnf(t3133,plain,
mult(mult(X1,mult(X2,X2)),i(X2)) = mult(X2,rd(mult(ld(X2,X1),mult(X2,X2)),X2)),
inference(cp,[status(thm)],[t3130,t2361]) ).
cnf(t3530,plain,
mult(X1,mult(ld(X1,X2),X1)) = rd(X2,i(X1)),
inference(cp,[status(thm)],[t3519,t10]) ).
cnf(t114830,plain,
rd(mult(X2,mult(X1,X1)),X1) = rd(X2,i(X1)),
inference(step,[status(thm)],[t3530,t2165]) ).
cnf(t3578,plain,
rd(mult(X1,mult(X2,X2)),X2) = rd(X1,i(X2)),
inference(orient,[status(thm)],[t114830]) ).
cnf(t114843,plain,
mult(mult(X1,mult(X2,X2)),i(X2)) = mult(X2,rd(ld(X2,X1),i(X2))),
inference(step,[status(thm)],[t3133,t3578]) ).
cnf(t835,plain,
mult(X1,mult(ld(X1,ld(X1,X2)),X1)) = ld(X1,mult(X2,X1)),
inference(cp,[status(thm)],[t827,t10]) ).
cnf(t114802,plain,
rd(mult(ld(X1,X2),mult(X1,X1)),X1) = ld(X1,mult(X2,X1)),
inference(step,[status(thm)],[t835,t2165]) ).
cnf(t2391,plain,
rd(mult(ld(X1,X2),mult(X1,X1)),X1) = ld(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t114802]) ).
cnf(t114835,plain,
rd(ld(X1,X2),i(X1)) = ld(X1,mult(X2,X1)),
inference(step,[status(thm)],[t2391,t3578]) ).
cnf(t3619,plain,
rd(ld(X1,X2),i(X1)) = ld(X1,mult(X2,X1)),
inference(rw,[status(thm)],[t114835]) ).
cnf(t3678,plain,
rd(ld(X1,X2),i(X1)) = ld(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t3619]) ).
cnf(t114844,plain,
mult(mult(X1,mult(X2,X2)),i(X2)) = mult(X2,ld(X2,mult(X1,X2))),
inference(step,[status(thm)],[t114843,t3678]) ).
cnf(t114845,plain,
mult(mult(X1,mult(X2,X2)),i(X2)) = mult(X1,X2),
inference(step,[status(thm)],[t114844,t10]) ).
cnf(t3874,plain,
mult(mult(X1,mult(X2,X2)),i(X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t114845]) ).
cnf(t3887,plain,
mult(rd(X1,mult(X2,X2)),X2) = mult(X1,i(X2)),
inference(cp,[status(thm)],[t3874,t14]) ).
cnf(t3923,plain,
mult(rd(X1,mult(X2,X2)),X2) = mult(X1,i(X2)),
inference(orient,[status(thm)],[t3887]) ).
cnf(t8239,plain,
mult(mult(X1,rd(X2,mult(X1,X1))),X1) = ld(i(X1),mult(X2,i(X1))),
inference(cp,[status(thm)],[t8213,t3923]) ).
cnf(t1195,plain,
mult(rd(X1,X2),i(X2)) = rd(mult(X1,i(X2)),X2),
inference(cp,[status(thm)],[t1174,t14]) ).
cnf(t1208,plain,
mult(rd(X1,X2),i(X2)) = rd(mult(X1,i(X2)),X2),
inference(orient,[status(thm)],[t1195]) ).
cnf(t1219,plain,
rd(mult(X1,i(i(X2))),i(X2)) = mult(rd(X1,i(X2)),X2),
inference(cp,[status(thm)],[t1208,t71]) ).
cnf(t114772,plain,
rd(mult(X1,X2),i(X2)) = mult(rd(X1,i(X2)),X2),
inference(step,[status(thm)],[t1219,t71]) ).
cnf(t1248,plain,
mult(rd(X1,i(X2)),X2) = rd(mult(X1,X2),i(X2)),
inference(orient,[status(thm)],[t114772]) ).
cnf(t3088,plain,
rd(mult(X1,rd(X2,i(i(X1)))),X1) = mult(X1,rd(mult(X2,i(X1)),i(i(X1)))),
inference(cp,[status(thm)],[t3082,t1248]) ).
cnf(t114884,plain,
rd(mult(X1,rd(X2,X1)),X1) = mult(X1,rd(mult(X2,i(X1)),i(i(X1)))),
inference(step,[status(thm)],[t3088,t71]) ).
cnf(t3948,plain,
rd(X1,mult(X2,X2)) = rd(mult(X1,i(X2)),X2),
inference(cp,[status(thm)],[t16,t3923]) ).
cnf(t3978,plain,
rd(mult(X1,i(X2)),X2) = rd(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t3948]) ).
cnf(t3985,plain,
rd(mult(X1,X2),mult(X1,X1)) = rd(mult(X1,rd(X2,X1)),X1),
inference(cp,[status(thm)],[t3978,t3182]) ).
cnf(t5428,plain,
rd(mult(X1,rd(X2,X1)),X1) = rd(mult(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t3985]) ).
cnf(t114885,plain,
rd(mult(X1,X2),mult(X1,X1)) = mult(X1,rd(mult(X2,i(X1)),i(i(X1)))),
inference(step,[status(thm)],[t114884,t5428]) ).
cnf(t3607,plain,
mult(X1,mult(X2,X2)) = mult(rd(X1,i(X2)),X2),
inference(cp,[status(thm)],[t14,t3578]) ).
cnf(t114838,plain,
mult(X1,mult(X2,X2)) = rd(mult(X1,X2),i(X2)),
inference(step,[status(thm)],[t3607,t1248]) ).
cnf(t3622,plain,
rd(mult(X1,X2),i(X2)) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t114838]) ).
cnf(t114886,plain,
rd(mult(X1,X2),mult(X1,X1)) = mult(X1,mult(X2,mult(i(X1),i(X1)))),
inference(step,[status(thm)],[t114885,t3622]) ).
cnf(t117,plain,
mult(X1,X1) = rd(X1,i(X1)),
inference(cp,[status(thm)],[t16,t112]) ).
cnf(t121,plain,
rd(X1,i(X1)) = mult(X1,X1),
inference(orient,[status(thm)],[t117]) ).
cnf(t122,plain,
mult(i(X1),i(X1)) = rd(i(X1),X1),
inference(cp,[status(thm)],[t121,t71]) ).
cnf(t126,plain,
mult(i(X1),i(X1)) = rd(i(X1),X1),
inference(orient,[status(thm)],[t122]) ).
cnf(t114887,plain,
rd(mult(X1,X2),mult(X1,X1)) = mult(X1,mult(X2,rd(i(X1),X1))),
inference(step,[status(thm)],[t114886,t126]) ).
cnf(t3664,plain,
mult(X1,mult(i(X2),i(X2))) = rd(mult(X1,i(X2)),X2),
inference(cp,[status(thm)],[t3622,t71]) ).
cnf(t114841,plain,
mult(X1,rd(i(X2),X2)) = rd(mult(X1,i(X2)),X2),
inference(step,[status(thm)],[t3664,t126]) ).
cnf(t3751,plain,
mult(X1,rd(i(X2),X2)) = rd(mult(X1,i(X2)),X2),
inference(orient,[status(thm)],[t114841]) ).
cnf(t114848,plain,
mult(X1,rd(i(X2),X2)) = rd(X1,mult(X2,X2)),
inference(step,[status(thm)],[t3751,t3978]) ).
cnf(t3981,plain,
mult(X1,rd(i(X2),X2)) = rd(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t114848]) ).
cnf(t114888,plain,
rd(mult(X1,X2),mult(X1,X1)) = mult(X1,rd(X2,mult(X1,X1))),
inference(step,[status(thm)],[t114887,t3981]) ).
cnf(t7020,plain,
mult(X1,rd(X2,mult(X1,X1))) = rd(mult(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t114888]) ).
cnf(t114971,plain,
mult(rd(mult(X1,X2),mult(X1,X1)),X1) = ld(i(X1),mult(X2,i(X1))),
inference(step,[status(thm)],[t8239,t7020]) ).
cnf(t114972,plain,
mult(mult(X1,X2),i(X1)) = ld(i(X1),mult(X2,i(X1))),
inference(step,[status(thm)],[t114971,t3923]) ).
cnf(t114973,plain,
mult(X1,rd(X2,X1)) = ld(i(X1),mult(X2,i(X1))),
inference(step,[status(thm)],[t114972,t3182]) ).
cnf(t3696,plain,
ld(i(X1),mult(X2,i(X1))) = rd(ld(i(X1),X2),X1),
inference(cp,[status(thm)],[t3678,t71]) ).
cnf(t4760,plain,
ld(i(X1),mult(X2,i(X1))) = rd(ld(i(X1),X2),X1),
inference(orient,[status(thm)],[t3696]) ).
cnf(t114974,plain,
mult(X1,rd(X2,X1)) = rd(ld(i(X1),X2),X1),
inference(step,[status(thm)],[t114973,t4760]) ).
cnf(t8691,plain,
rd(ld(i(X1),X2),X1) = mult(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t114974]) ).
cnf(t2117,plain,
mult(mult(rd(X1,X2),X2),mult(X2,X3)) = mult(X2,mult(mult(rd(ld(X2,mult(X1,X2)),X2),X2),X3)),
inference(cp,[status(thm)],[t431,t2074]) ).
cnf(t115243,plain,
mult(X1,mult(X2,X3)) = mult(X2,mult(mult(rd(ld(X2,mult(X1,X2)),X2),X2),X3)),
inference(step,[status(thm)],[t2117,t14]) ).
cnf(t115244,plain,
mult(X1,mult(X2,X3)) = mult(X2,mult(ld(X2,mult(X1,X2)),X3)),
inference(step,[status(thm)],[t115243,t14]) ).
cnf(t28394,plain,
mult(X1,mult(ld(X1,mult(X2,X1)),X3)) = mult(X2,mult(X1,X3)),
inference(orient,[status(thm)],[t115244]) ).
cnf(t28546,plain,
mult(ld(X1,mult(X2,X1)),X3) = ld(X1,mult(X2,mult(X1,X3))),
inference(cp,[status(thm)],[t20,t28394]) ).
cnf(t28990,plain,
ld(X1,mult(X2,mult(X1,X3))) = mult(ld(X1,mult(X2,X1)),X3),
inference(orient,[status(thm)],[t28546]) ).
cnf(t29023,plain,
mult(ld(X1,mult(i(mult(X1,X2)),X1)),X2) = ld(X1,unit),
inference(cp,[status(thm)],[t28990,t58]) ).
cnf(t115273,plain,
mult(ld(X1,mult(i(mult(X1,X2)),X1)),X2) = i(X1),
inference(step,[status(thm)],[t29023,t69]) ).
cnf(t30779,plain,
mult(ld(X1,mult(i(mult(X1,X2)),X1)),X2) = i(X1),
inference(orient,[status(thm)],[t115273]) ).
cnf(t30910,plain,
ld(X1,mult(i(mult(X1,X2)),X1)) = rd(i(X1),X2),
inference(cp,[status(thm)],[t16,t30779]) ).
cnf(t41534,plain,
ld(X1,mult(i(mult(X1,X2)),X1)) = rd(i(X1),X2),
inference(orient,[status(thm)],[t30910]) ).
cnf(t41712,plain,
mult(X1,rd(mult(i(mult(i(X1),X2)),i(X1)),X1)) = rd(rd(i(i(X1)),X2),X1),
inference(cp,[status(thm)],[t8691,t41534]) ).
cnf(t115408,plain,
mult(X1,rd(i(mult(i(X1),X2)),mult(X1,X1))) = rd(rd(i(i(X1)),X2),X1),
inference(step,[status(thm)],[t41712,t3978]) ).
cnf(t115409,plain,
rd(mult(X1,i(mult(i(X1),X2))),mult(X1,X1)) = rd(rd(i(i(X1)),X2),X1),
inference(step,[status(thm)],[t115408,t7020]) ).
cnf(t31,plain,
mult(X1,X2) = ld(mult(mult(X1,X3),X1),mult(X1,mult(mult(mult(X3,X1),X1),X2))),
inference(cp,[status(thm)],[t20,t24]) ).
cnf(t9579,plain,
ld(mult(mult(X1,X2),X1),mult(X1,mult(mult(mult(X2,X1),X1),X3))) = mult(X1,X3),
inference(orient,[status(thm)],[t31]) ).
cnf(t9681,plain,
mult(X1,i(mult(mult(X2,X1),X1))) = ld(mult(mult(X1,X2),X1),mult(X1,unit)),
inference(cp,[status(thm)],[t9579,t36]) ).
cnf(t115115,plain,
mult(X1,i(mult(mult(X2,X1),X1))) = ld(mult(mult(X1,X2),X1),X1),
inference(step,[status(thm)],[t9681,t11]) ).
cnf(t14921,plain,
mult(X1,i(mult(mult(X2,X1),X1))) = ld(mult(mult(X1,X2),X1),X1),
inference(orient,[status(thm)],[t115115]) ).
cnf(t114823,plain,
mult(mult(X1,i(X2)),X2) = rd(rd(X1,X2),i(X2)),
inference(step,[status(thm)],[t1017,t3441]) ).
cnf(t3442,plain,
mult(mult(X1,i(X2)),X2) = rd(rd(X1,X2),i(X2)),
inference(orient,[status(thm)],[t114823]) ).
cnf(t14965,plain,
ld(mult(mult(X1,mult(X2,i(X1))),X1),X1) = mult(X1,i(mult(rd(rd(X2,X1),i(X1)),X1))),
inference(cp,[status(thm)],[t14921,t3442]) ).
cnf(t115133,plain,
ld(mult(rd(mult(X1,X2),X1),X1),X1) = mult(X1,i(mult(rd(rd(X2,X1),i(X1)),X1))),
inference(step,[status(thm)],[t14965,t3082]) ).
cnf(t115134,plain,
ld(mult(X1,X2),X1) = mult(X1,i(mult(rd(rd(X2,X1),i(X1)),X1))),
inference(step,[status(thm)],[t115133,t14]) ).
cnf(t114839,plain,
mult(rd(X1,i(X2)),X2) = mult(X1,mult(X2,X2)),
inference(step,[status(thm)],[t1248,t3622]) ).
cnf(t3623,plain,
mult(rd(X1,i(X2)),X2) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t114839]) ).
cnf(t115135,plain,
ld(mult(X1,X2),X1) = mult(X1,i(mult(rd(X2,X1),mult(X1,X1)))),
inference(step,[status(thm)],[t115134,t3623]) ).
cnf(t115136,plain,
ld(mult(X1,X2),X1) = mult(X1,i(mult(X1,mult(ld(X1,X2),X1)))),
inference(step,[status(thm)],[t115135,t2932]) ).
cnf(t114833,plain,
mult(X1,mult(ld(X1,X2),X1)) = rd(X2,i(X1)),
inference(step,[status(thm)],[t2165,t3578]) ).
cnf(t3581,plain,
mult(X1,mult(ld(X1,X2),X1)) = rd(X2,i(X1)),
inference(orient,[status(thm)],[t114833]) ).
cnf(t115137,plain,
ld(mult(X1,X2),X1) = mult(X1,i(rd(X2,i(X1)))),
inference(step,[status(thm)],[t115136,t3581]) ).
cnf(t17163,plain,
mult(X1,i(rd(X2,i(X1)))) = ld(mult(X1,X2),X1),
inference(orient,[status(thm)],[t115137]) ).
cnf(t1260,plain,
rd(X1,i(X2)) = rd(rd(mult(X1,X2),i(X2)),X2),
inference(cp,[status(thm)],[t16,t1248]) ).
cnf(t1429,plain,
rd(rd(mult(X1,X2),i(X2)),X2) = rd(X1,i(X2)),
inference(orient,[status(thm)],[t1260]) ).
cnf(t1451,plain,
rd(rd(X1,X2),i(X2)) = rd(rd(X1,i(X2)),X2),
inference(cp,[status(thm)],[t1429,t14]) ).
cnf(t1463,plain,
rd(rd(X1,i(X2)),X2) = rd(rd(X1,X2),i(X2)),
inference(orient,[status(thm)],[t1451]) ).
cnf(t3705,plain,
rd(rd(ld(X1,X2),X1),i(X1)) = rd(ld(X1,mult(X2,X1)),X1),
inference(cp,[status(thm)],[t1463,t3678]) ).
cnf(t7598,plain,
rd(rd(ld(X1,X2),X1),i(X1)) = rd(ld(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t3705]) ).
cnf(t3155,plain,
rd(ld(X1,X2),X1) = ld(X1,mult(X2,i(X1))),
inference(cp,[status(thm)],[t20,t3130]) ).
cnf(t3356,plain,
ld(X1,mult(X2,i(X1))) = rd(ld(X1,X2),X1),
inference(orient,[status(thm)],[t3155]) ).
cnf(t3368,plain,
rd(ld(X1,rd(X2,i(X1))),X1) = ld(X1,X2),
inference(cp,[status(thm)],[t3356,t14]) ).
cnf(t4224,plain,
rd(ld(X1,rd(X2,i(X1))),X1) = ld(X1,X2),
inference(orient,[status(thm)],[t3368]) ).
cnf(t3398,plain,
rd(rd(X1,i(X2)),i(X2)) = mult(mult(X1,X2),i(i(X2))),
inference(cp,[status(thm)],[t3384,t71]) ).
cnf(t114842,plain,
rd(rd(X1,i(X2)),i(X2)) = mult(mult(X1,X2),X2),
inference(step,[status(thm)],[t3398,t71]) ).
cnf(t3847,plain,
rd(rd(X1,i(X2)),i(X2)) = mult(mult(X1,X2),X2),
inference(orient,[status(thm)],[t114842]) ).
cnf(t4233,plain,
ld(X1,rd(X2,i(X1))) = rd(ld(X1,mult(mult(X2,X1),X1)),X1),
inference(cp,[status(thm)],[t4224,t3847]) ).
cnf(t114860,plain,
ld(X1,rd(X2,i(X1))) = rd(mult(mult(ld(X1,X2),X1),X1),X1),
inference(step,[status(thm)],[t4233,t700]) ).
cnf(t114861,plain,
ld(X1,rd(X2,i(X1))) = mult(ld(X1,X2),X1),
inference(step,[status(thm)],[t114860,t16]) ).
cnf(t4255,plain,
ld(X1,rd(X2,i(X1))) = mult(ld(X1,X2),X1),
inference(orient,[status(thm)],[t114861]) ).
cnf(t4266,plain,
mult(ld(i(X1),X2),i(X1)) = ld(i(X1),rd(X2,X1)),
inference(cp,[status(thm)],[t4255,t71]) ).
cnf(t4853,plain,
mult(ld(i(X1),X2),i(X1)) = ld(i(X1),rd(X2,X1)),
inference(orient,[status(thm)],[t4266]) ).
cnf(t8036,plain,
mult(i(X1),mult(mult(i(X1),ld(i(X1),X2)),i(X1))) = mult(i(X1),ld(i(i(X1)),ld(i(X1),rd(X2,X1)))),
inference(cp,[status(thm)],[t8013,t4853]) ).
cnf(t3562,plain,
mult(i(X1),mult(X2,i(X1))) = rd(mult(i(X1),X2),X1),
inference(cp,[status(thm)],[t3519,t71]) ).
cnf(t4697,plain,
mult(i(X1),mult(X2,i(X1))) = rd(mult(i(X1),X2),X1),
inference(orient,[status(thm)],[t3562]) ).
cnf(t114919,plain,
rd(mult(i(X1),mult(i(X1),ld(i(X1),X2))),X1) = mult(i(X1),ld(i(i(X1)),ld(i(X1),rd(X2,X1)))),
inference(step,[status(thm)],[t8036,t4697]) ).
cnf(t114920,plain,
rd(mult(i(X1),X2),X1) = mult(i(X1),ld(i(i(X1)),ld(i(X1),rd(X2,X1)))),
inference(step,[status(thm)],[t114919,t10]) ).
cnf(t1154,plain,
mult(X1,ld(i(X1),ld(X1,X2))) = ld(i(X1),X2),
inference(cp,[status(thm)],[t1146,t10]) ).
cnf(t1339,plain,
mult(X1,ld(i(X1),ld(X1,X2))) = ld(i(X1),X2),
inference(orient,[status(thm)],[t1154]) ).
cnf(t114921,plain,
rd(mult(i(X1),X2),X1) = ld(i(i(X1)),rd(X2,X1)),
inference(step,[status(thm)],[t114920,t1339]) ).
cnf(t114922,plain,
rd(mult(i(X1),X2),X1) = ld(X1,rd(X2,X1)),
inference(step,[status(thm)],[t114921,t71]) ).
cnf(t8133,plain,
rd(mult(i(X1),X2),X1) = ld(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t114922]) ).
cnf(t8139,plain,
ld(X1,rd(rd(X2,i(X1)),X1)) = rd(mult(mult(i(X1),X2),X1),X1),
inference(cp,[status(thm)],[t8133,t4609]) ).
cnf(t114977,plain,
ld(X1,rd(rd(X2,X1),i(X1))) = rd(mult(mult(i(X1),X2),X1),X1),
inference(step,[status(thm)],[t8139,t1463]) ).
cnf(t114978,plain,
mult(ld(X1,rd(X2,X1)),X1) = rd(mult(mult(i(X1),X2),X1),X1),
inference(step,[status(thm)],[t114977,t4255]) ).
cnf(t114979,plain,
rd(ld(X1,mult(X2,X1)),X1) = rd(mult(mult(i(X1),X2),X1),X1),
inference(step,[status(thm)],[t114978,t2074]) ).
cnf(t114980,plain,
rd(ld(X1,mult(X2,X1)),X1) = mult(i(X1),X2),
inference(step,[status(thm)],[t114979,t16]) ).
cnf(t8749,plain,
rd(ld(X1,mult(X2,X1)),X1) = mult(i(X1),X2),
inference(orient,[status(thm)],[t114980]) ).
cnf(t114983,plain,
rd(rd(ld(X1,X2),X1),i(X1)) = mult(i(X1),X2),
inference(step,[status(thm)],[t7598,t8749]) ).
cnf(t8752,plain,
rd(rd(ld(X1,X2),X1),i(X1)) = mult(i(X1),X2),
inference(orient,[status(thm)],[t114983]) ).
cnf(t17175,plain,
ld(mult(X1,rd(ld(X1,X2),X1)),X1) = mult(X1,i(mult(i(X1),X2))),
inference(cp,[status(thm)],[t17163,t8752]) ).
cnf(t115143,plain,
ld(mult(X2,i(X1)),X1) = mult(X1,i(mult(i(X1),X2))),
inference(step,[status(thm)],[t17175,t3130]) ).
cnf(t18624,plain,
mult(X1,i(mult(i(X1),X2))) = ld(mult(X2,i(X1)),X1),
inference(orient,[status(thm)],[t115143]) ).
cnf(t115410,plain,
rd(ld(mult(X2,i(X1)),X1),mult(X1,X1)) = rd(rd(i(i(X1)),X2),X1),
inference(step,[status(thm)],[t115409,t18624]) ).
cnf(t8147,plain,
ld(X1,rd(rd(rd(X2,i(X1)),i(X1)),X1)) = rd(rd(rd(mult(i(X1),X2),i(X1)),i(X1)),X1),
inference(cp,[status(thm)],[t8133,t2212]) ).
cnf(t114942,plain,
ld(X1,rd(rd(rd(X2,i(X1)),X1),i(X1))) = rd(rd(rd(mult(i(X1),X2),i(X1)),i(X1)),X1),
inference(step,[status(thm)],[t8147,t1463]) ).
cnf(t114943,plain,
mult(ld(X1,rd(rd(X2,i(X1)),X1)),X1) = rd(rd(rd(mult(i(X1),X2),i(X1)),i(X1)),X1),
inference(step,[status(thm)],[t114942,t4255]) ).
cnf(t114944,plain,
rd(ld(X1,mult(rd(X2,i(X1)),X1)),X1) = rd(rd(rd(mult(i(X1),X2),i(X1)),i(X1)),X1),
inference(step,[status(thm)],[t114943,t2074]) ).
cnf(t114945,plain,
rd(ld(X1,mult(X2,mult(X1,X1))),X1) = rd(rd(rd(mult(i(X1),X2),i(X1)),i(X1)),X1),
inference(step,[status(thm)],[t114944,t3623]) ).
cnf(t114946,plain,
rd(mult(ld(X1,X2),mult(X1,X1)),X1) = rd(rd(rd(mult(i(X1),X2),i(X1)),i(X1)),X1),
inference(step,[status(thm)],[t114945,t2361]) ).
cnf(t114947,plain,
rd(ld(X1,X2),i(X1)) = rd(rd(rd(mult(i(X1),X2),i(X1)),i(X1)),X1),
inference(step,[status(thm)],[t114946,t3578]) ).
cnf(t114948,plain,
ld(X1,mult(X2,X1)) = rd(rd(rd(mult(i(X1),X2),i(X1)),i(X1)),X1),
inference(step,[status(thm)],[t114947,t3678]) ).
cnf(t114949,plain,
ld(X1,mult(X2,X1)) = rd(rd(rd(mult(i(X1),X2),i(X1)),X1),i(X1)),
inference(step,[status(thm)],[t114948,t1463]) ).
cnf(t114950,plain,
ld(X1,mult(X2,X1)) = rd(rd(rd(mult(i(X1),X2),X1),i(X1)),i(X1)),
inference(step,[status(thm)],[t114949,t1463]) ).
cnf(t114951,plain,
ld(X1,mult(X2,X1)) = mult(mult(rd(mult(i(X1),X2),X1),X1),X1),
inference(step,[status(thm)],[t114950,t3847]) ).
cnf(t114952,plain,
ld(X1,mult(X2,X1)) = mult(mult(i(X1),X2),X1),
inference(step,[status(thm)],[t114951,t14]) ).
cnf(t8394,plain,
mult(mult(i(X1),X2),X1) = ld(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t114952]) ).
cnf(t114953,plain,
mult(i(X1),rd(X2,i(X1))) = ld(X1,mult(X2,X1)),
inference(step,[status(thm)],[t4609,t8394]) ).
cnf(t8395,plain,
mult(i(X1),rd(X2,i(X1))) = ld(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t114953]) ).
cnf(t14996,plain,
ld(mult(mult(X1,rd(X2,X1)),X1),X1) = mult(X1,i(mult(X2,X1))),
inference(cp,[status(thm)],[t14921,t14]) ).
cnf(t8203,plain,
rd(rd(mult(i(i(X1)),X2),X1),i(X1)) = rd(ld(i(X1),rd(X2,i(X1))),X1),
inference(cp,[status(thm)],[t1463,t8133]) ).
cnf(t114990,plain,
rd(rd(mult(X1,X2),X1),i(X1)) = rd(ld(i(X1),rd(X2,i(X1))),X1),
inference(step,[status(thm)],[t8203,t71]) ).
cnf(t3139,plain,
mult(mult(mult(X1,X2),X1),i(X1)) = mult(X1,rd(rd(mult(X2,mult(X1,X1)),X1),X1)),
inference(cp,[status(thm)],[t3130,t2166]) ).
cnf(t114897,plain,
rd(rd(mult(X1,X2),X1),i(X1)) = mult(X1,rd(rd(mult(X2,mult(X1,X1)),X1),X1)),
inference(step,[status(thm)],[t3139,t3441]) ).
cnf(t114898,plain,
rd(rd(mult(X1,X2),X1),i(X1)) = rd(rd(mult(X1,mult(X2,mult(X1,X1))),X1),X1),
inference(step,[status(thm)],[t114897,t2212]) ).
cnf(t1879,plain,
mult(mult(X1,X2),mult(X1,X1)) = rd(mult(X1,mult(mult(mult(X2,X1),X1),X1)),X1),
inference(cp,[status(thm)],[t1878,t24]) ).
cnf(t114790,plain,
mult(mult(X1,X2),mult(X1,X1)) = mult(mult(X1,mult(X2,X1)),X1),
inference(step,[status(thm)],[t1879,t760]) ).
cnf(t1925,plain,
mult(mult(X1,mult(X2,X1)),X1) = mult(mult(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t114790]) ).
cnf(t1964,plain,
mult(X1,mult(X2,X1)) = rd(mult(mult(X1,X2),mult(X1,X1)),X1),
inference(cp,[status(thm)],[t16,t1925]) ).
cnf(t2172,plain,
rd(mult(mult(mult(X1,X2),X1),mult(X1,X1)),X1) = mult(X1,mult(rd(mult(X2,mult(X1,X1)),X1),X1)),
inference(cp,[status(thm)],[t2165,t2166]) ).
cnf(t114796,plain,
mult(mult(X1,X2),mult(X1,X1)) = mult(X1,mult(rd(mult(X2,mult(X1,X1)),X1),X1)),
inference(step,[status(thm)],[t2172,t1878]) ).
cnf(t114797,plain,
mult(mult(X1,X2),mult(X1,X1)) = mult(X1,mult(X2,mult(X1,X1))),
inference(step,[status(thm)],[t114796,t14]) ).
cnf(t2257,plain,
mult(mult(X1,X2),mult(X1,X1)) = mult(X1,mult(X2,mult(X1,X1))),
inference(orient,[status(thm)],[t114797]) ).
cnf(t114809,plain,
mult(X1,mult(X2,X1)) = rd(mult(X1,mult(X2,mult(X1,X1))),X1),
inference(step,[status(thm)],[t1964,t2257]) ).
cnf(t2808,plain,
rd(mult(X1,mult(X2,mult(X1,X1))),X1) = mult(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t114809]) ).
cnf(t114899,plain,
rd(rd(mult(X1,X2),X1),i(X1)) = rd(mult(X1,mult(X2,X1)),X1),
inference(step,[status(thm)],[t114898,t2808]) ).
cnf(t7261,plain,
rd(rd(mult(X1,X2),X1),i(X1)) = rd(mult(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t114899]) ).
cnf(t114991,plain,
rd(mult(X1,mult(X2,X1)),X1) = rd(ld(i(X1),rd(X2,i(X1))),X1),
inference(step,[status(thm)],[t114990,t7261]) ).
cnf(t3700,plain,
ld(X1,X2) = mult(ld(X1,mult(X2,X1)),i(X1)),
inference(cp,[status(thm)],[t14,t3678]) ).
cnf(t4304,plain,
mult(ld(X1,mult(X2,X1)),i(X1)) = ld(X1,X2),
inference(orient,[status(thm)],[t3700]) ).
cnf(t4338,plain,
ld(X1,rd(X2,X1)) = mult(ld(X1,X2),i(X1)),
inference(cp,[status(thm)],[t4304,t14]) ).
cnf(t4378,plain,
mult(ld(X1,X2),i(X1)) = ld(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t4338]) ).
cnf(t4396,plain,
ld(i(X1),rd(X2,i(X1))) = mult(ld(i(X1),X2),X1),
inference(cp,[status(thm)],[t4378,t71]) ).
cnf(t4908,plain,
ld(i(X1),rd(X2,i(X1))) = mult(ld(i(X1),X2),X1),
inference(orient,[status(thm)],[t4396]) ).
cnf(t114992,plain,
rd(mult(X1,mult(X2,X1)),X1) = rd(mult(ld(i(X1),X2),X1),X1),
inference(step,[status(thm)],[t114991,t4908]) ).
cnf(t114993,plain,
rd(mult(X1,mult(X2,X1)),X1) = ld(i(X1),X2),
inference(step,[status(thm)],[t114992,t16]) ).
cnf(t8887,plain,
rd(mult(X1,mult(X2,X1)),X1) = ld(i(X1),X2),
inference(orient,[status(thm)],[t114993]) ).
cnf(t114996,plain,
mult(mult(X1,rd(X2,X1)),X1) = ld(i(X1),X2),
inference(step,[status(thm)],[t783,t8887]) ).
cnf(t8890,plain,
mult(mult(X1,rd(X2,X1)),X1) = ld(i(X1),X2),
inference(orient,[status(thm)],[t114996]) ).
cnf(t115116,plain,
ld(ld(i(X1),X2),X1) = mult(X1,i(mult(X2,X1))),
inference(step,[status(thm)],[t14996,t8890]) ).
cnf(t15117,plain,
ld(ld(i(X1),X2),X1) = mult(X1,i(mult(X2,X1))),
inference(orient,[status(thm)],[t115116]) ).
cnf(t114831,plain,
ld(X1,mult(mult(X1,X2),X1)) = rd(X2,i(X1)),
inference(step,[status(thm)],[t2166,t3578]) ).
cnf(t3579,plain,
ld(X1,mult(mult(X1,X2),X1)) = rd(X2,i(X1)),
inference(orient,[status(thm)],[t114831]) ).
cnf(t15141,plain,
mult(X1,i(mult(mult(mult(i(X1),X2),i(X1)),X1))) = ld(rd(X2,i(i(X1))),X1),
inference(cp,[status(thm)],[t15117,t3579]) ).
cnf(t115117,plain,
mult(X1,i(rd(rd(mult(i(X1),X2),X1),i(X1)))) = ld(rd(X2,i(i(X1))),X1),
inference(step,[status(thm)],[t15141,t3442]) ).
cnf(t115118,plain,
mult(X1,i(rd(ld(X1,rd(X2,X1)),i(X1)))) = ld(rd(X2,i(i(X1))),X1),
inference(step,[status(thm)],[t115117,t8133]) ).
cnf(t115119,plain,
mult(X1,i(ld(X1,mult(rd(X2,X1),X1)))) = ld(rd(X2,i(i(X1))),X1),
inference(step,[status(thm)],[t115118,t3678]) ).
cnf(t115120,plain,
mult(X1,i(ld(X1,X2))) = ld(rd(X2,i(i(X1))),X1),
inference(step,[status(thm)],[t115119,t14]) ).
cnf(t115121,plain,
mult(X1,i(ld(X1,X2))) = ld(rd(X2,X1),X1),
inference(step,[status(thm)],[t115120,t71]) ).
cnf(t15178,plain,
mult(X1,i(ld(X1,X2))) = ld(rd(X2,X1),X1),
inference(orient,[status(thm)],[t115121]) ).
cnf(t15260,plain,
i(ld(X1,X2)) = ld(X1,ld(rd(X2,X1),X1)),
inference(cp,[status(thm)],[t20,t15178]) ).
cnf(t22,plain,
X1 = ld(rd(X2,X1),X2),
inference(cp,[status(thm)],[t20,t14]) ).
cnf(t73,plain,
ld(rd(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t22]) ).
cnf(t17,plain,
X1 = rd(X2,ld(X1,X2)),
inference(cp,[status(thm)],[t16,t10]) ).
cnf(t72,plain,
rd(X1,ld(X2,X1)) = X2,
inference(orient,[status(thm)],[t17]) ).
cnf(t8149,plain,
ld(X1,rd(mult(i(i(X1)),ld(i(X1),X2)),X1)) = rd(mult(i(i(X1)),X2),X1),
inference(cp,[status(thm)],[t8133,t1102]) ).
cnf(t114955,plain,
ld(X1,rd(mult(X1,ld(i(X1),X2)),X1)) = rd(mult(i(i(X1)),X2),X1),
inference(step,[status(thm)],[t8149,t71]) ).
cnf(t114815,plain,
ld(X1,rd(mult(X1,X2),X1)) = mult(X2,i(X1)),
inference(step,[status(thm)],[t2709,t3130]) ).
cnf(t3131,plain,
ld(X1,rd(mult(X1,X2),X1)) = mult(X2,i(X1)),
inference(orient,[status(thm)],[t114815]) ).
cnf(t114956,plain,
mult(ld(i(X1),X2),i(X1)) = rd(mult(i(i(X1)),X2),X1),
inference(step,[status(thm)],[t114955,t3131]) ).
cnf(t114957,plain,
ld(i(X1),rd(X2,X1)) = rd(mult(i(i(X1)),X2),X1),
inference(step,[status(thm)],[t114956,t4853]) ).
cnf(t114958,plain,
ld(i(X1),rd(X2,X1)) = rd(mult(X1,X2),X1),
inference(step,[status(thm)],[t114957,t71]) ).
cnf(t8480,plain,
ld(i(X1),rd(X2,X1)) = rd(mult(X1,X2),X1),
inference(orient,[status(thm)],[t114958]) ).
cnf(t15127,plain,
mult(X1,i(mult(rd(X2,X1),X1))) = ld(rd(mult(X1,X2),X1),X1),
inference(cp,[status(thm)],[t15117,t8480]) ).
cnf(t115123,plain,
mult(X1,i(X2)) = ld(rd(mult(X1,X2),X1),X1),
inference(step,[status(thm)],[t15127,t14]) ).
cnf(t15362,plain,
ld(rd(mult(X1,X2),X1),X1) = mult(X1,i(X2)),
inference(orient,[status(thm)],[t115123]) ).
cnf(t15446,plain,
rd(mult(X1,X2),X1) = rd(X1,mult(X1,i(X2))),
inference(cp,[status(thm)],[t72,t15362]) ).
cnf(t15470,plain,
rd(X1,mult(X1,i(X2))) = rd(mult(X1,X2),X1),
inference(orient,[status(thm)],[t15446]) ).
cnf(t15502,plain,
rd(mult(X1,i(X2)),X1) = rd(X1,mult(X1,X2)),
inference(cp,[status(thm)],[t15470,t71]) ).
cnf(t15539,plain,
rd(mult(X1,i(X2)),X1) = rd(X1,mult(X1,X2)),
inference(orient,[status(thm)],[t15502]) ).
cnf(t15542,plain,
rd(X1,mult(X1,ld(X1,X2))) = rd(ld(rd(X2,X1),X1),X1),
inference(cp,[status(thm)],[t15539,t15178]) ).
cnf(t115124,plain,
rd(X1,X2) = rd(ld(rd(X2,X1),X1),X1),
inference(step,[status(thm)],[t15542,t10]) ).
cnf(t15649,plain,
rd(ld(rd(X1,X2),X2),X2) = rd(X2,X1),
inference(orient,[status(thm)],[t115124]) ).
cnf(t15702,plain,
rd(X1,mult(X2,X1)) = rd(ld(X2,X1),X1),
inference(cp,[status(thm)],[t15649,t16]) ).
cnf(t15776,plain,
rd(ld(X1,X2),X2) = rd(X2,mult(X1,X2)),
inference(orient,[status(thm)],[t15702]) ).
cnf(t15835,plain,
rd(X1,mult(rd(X1,X2),X1)) = rd(X2,X1),
inference(cp,[status(thm)],[t15776,t73]) ).
cnf(t15906,plain,
rd(X1,mult(rd(X1,X2),X1)) = rd(X2,X1),
inference(orient,[status(thm)],[t15835]) ).
cnf(t15975,plain,
mult(rd(X1,X2),X1) = ld(rd(X2,X1),X1),
inference(cp,[status(thm)],[t73,t15906]) ).
cnf(t16007,plain,
ld(rd(X1,X2),X2) = mult(rd(X2,X1),X2),
inference(orient,[status(thm)],[t15975]) ).
cnf(t115132,plain,
i(ld(X1,X2)) = ld(X1,mult(rd(X1,X2),X1)),
inference(step,[status(thm)],[t15260,t16007]) ).
cnf(t16439,plain,
ld(X1,mult(rd(X1,X2),X1)) = i(ld(X1,X2)),
inference(orient,[status(thm)],[t115132]) ).
cnf(t15845,plain,
ld(X1,X2) = mult(rd(X2,mult(X1,X2)),X2),
inference(cp,[status(thm)],[t14,t15776]) ).
cnf(t16097,plain,
mult(rd(X1,mult(X2,X1)),X1) = ld(X2,X1),
inference(orient,[status(thm)],[t15845]) ).
cnf(t16443,plain,
i(ld(X1,mult(X2,X1))) = ld(X1,ld(X2,X1)),
inference(cp,[status(thm)],[t16439,t16097]) ).
cnf(t16569,plain,
i(ld(X1,mult(X2,X1))) = ld(X1,ld(X2,X1)),
inference(orient,[status(thm)],[t16443]) ).
cnf(t16571,plain,
ld(X1,ld(mult(X1,X2),X1)) = i(rd(X2,i(X1))),
inference(cp,[status(thm)],[t16569,t3579]) ).
cnf(t17605,plain,
ld(X1,ld(mult(X1,X2),X1)) = i(rd(X2,i(X1))),
inference(orient,[status(thm)],[t16571]) ).
cnf(t4002,plain,
rd(X1,mult(i(X2),i(X2))) = rd(mult(X1,X2),i(X2)),
inference(cp,[status(thm)],[t3978,t71]) ).
cnf(t114852,plain,
rd(X1,rd(i(X2),X2)) = rd(mult(X1,X2),i(X2)),
inference(step,[status(thm)],[t4002,t126]) ).
cnf(t114853,plain,
rd(X1,rd(i(X2),X2)) = mult(X1,mult(X2,X2)),
inference(step,[status(thm)],[t114852,t3622]) ).
cnf(t4022,plain,
rd(X1,rd(i(X2),X2)) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t114853]) ).
cnf(t4036,plain,
rd(i(X1),X1) = ld(mult(X2,mult(X1,X1)),X2),
inference(cp,[status(thm)],[t73,t4022]) ).
cnf(t4060,plain,
ld(mult(X1,mult(X2,X2)),X1) = rd(i(X2),X2),
inference(orient,[status(thm)],[t4036]) ).
cnf(t17607,plain,
i(rd(mult(X1,X1),i(X2))) = ld(X2,rd(i(X1),X1)),
inference(cp,[status(thm)],[t17605,t4060]) ).
cnf(t18769,plain,
i(rd(mult(X1,X1),i(X2))) = ld(X2,rd(i(X1),X1)),
inference(orient,[status(thm)],[t17607]) ).
cnf(t114846,plain,
mult(rd(X1,X2),i(X2)) = rd(X1,mult(X2,X2)),
inference(step,[status(thm)],[t1208,t3978]) ).
cnf(t3979,plain,
mult(rd(X1,X2),i(X2)) = rd(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t114846]) ).
cnf(t16446,plain,
i(ld(X1,rd(i(X2),X2))) = ld(X1,mult(mult(X1,mult(X2,X2)),X1)),
inference(cp,[status(thm)],[t16439,t4022]) ).
cnf(t115139,plain,
i(ld(X1,rd(i(X2),X2))) = rd(mult(X2,X2),i(X1)),
inference(step,[status(thm)],[t16446,t3579]) ).
cnf(t18170,plain,
i(ld(X1,rd(i(X2),X2))) = rd(mult(X2,X2),i(X1)),
inference(orient,[status(thm)],[t115139]) ).
cnf(t18189,plain,
rd(mult(i(X1),i(X1)),i(X2)) = i(ld(X2,rd(X1,i(X1)))),
inference(cp,[status(thm)],[t18170,t71]) ).
cnf(t115144,plain,
rd(rd(i(X1),X1),i(X2)) = i(ld(X2,rd(X1,i(X1)))),
inference(step,[status(thm)],[t18189,t126]) ).
cnf(t115145,plain,
rd(rd(i(X1),X1),i(X2)) = i(ld(X2,mult(X1,X1))),
inference(step,[status(thm)],[t115144,t121]) ).
cnf(t18947,plain,
rd(rd(i(X1),X1),i(X2)) = i(ld(X2,mult(X1,X1))),
inference(orient,[status(thm)],[t115145]) ).
cnf(t18974,plain,
rd(rd(i(X1),X1),mult(i(X2),i(X2))) = mult(i(ld(X2,mult(X1,X1))),i(i(X2))),
inference(cp,[status(thm)],[t3979,t18947]) ).
cnf(t115204,plain,
rd(rd(i(X1),X1),rd(i(X2),X2)) = mult(i(ld(X2,mult(X1,X1))),i(i(X2))),
inference(step,[status(thm)],[t18974,t126]) ).
cnf(t115205,plain,
mult(rd(i(X1),X1),mult(X2,X2)) = mult(i(ld(X2,mult(X1,X1))),i(i(X2))),
inference(step,[status(thm)],[t115204,t4022]) ).
cnf(t3150,plain,
mult(X1,mult(rd(ld(X1,X2),X1),mult(X1,X1))) = mult(mult(X2,i(X1)),mult(X1,X1)),
inference(cp,[status(thm)],[t2257,t3130]) ).
cnf(t114854,plain,
mult(X1,mult(X1,mult(ld(X1,ld(X1,X2)),X1))) = mult(mult(X2,i(X1)),mult(X1,X1)),
inference(step,[status(thm)],[t3150,t2932]) ).
cnf(t114855,plain,
mult(X1,rd(ld(X1,X2),i(X1))) = mult(mult(X2,i(X1)),mult(X1,X1)),
inference(step,[status(thm)],[t114854,t3581]) ).
cnf(t114856,plain,
mult(X1,ld(X1,mult(X2,X1))) = mult(mult(X2,i(X1)),mult(X1,X1)),
inference(step,[status(thm)],[t114855,t3678]) ).
cnf(t114857,plain,
mult(X2,X1) = mult(mult(X2,i(X1)),mult(X1,X1)),
inference(step,[status(thm)],[t114856,t10]) ).
cnf(t4119,plain,
mult(mult(X1,i(X2)),mult(X2,X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t114857]) ).
cnf(t4130,plain,
mult(X1,i(X2)) = mult(mult(X1,X2),mult(i(X2),i(X2))),
inference(cp,[status(thm)],[t4119,t71]) ).
cnf(t114858,plain,
mult(X1,i(X2)) = mult(mult(X1,X2),rd(i(X2),X2)),
inference(step,[status(thm)],[t4130,t126]) ).
cnf(t114859,plain,
mult(X1,i(X2)) = rd(mult(X1,X2),mult(X2,X2)),
inference(step,[status(thm)],[t114858,t3981]) ).
cnf(t4170,plain,
rd(mult(X1,X2),mult(X2,X2)) = mult(X1,i(X2)),
inference(orient,[status(thm)],[t114859]) ).
cnf(t829,plain,
mult(X1,mult(ld(X1,mult(X1,mult(X1,X2))),X1)) = ld(X1,mult(mult(X1,X1),mult(X1,mult(X2,X1)))),
inference(cp,[status(thm)],[t827,t42]) ).
cnf(t114724,plain,
mult(X1,mult(mult(X1,X2),X1)) = ld(X1,mult(mult(X1,X1),mult(X1,mult(X2,X1)))),
inference(step,[status(thm)],[t829,t20]) ).
cnf(t114725,plain,
mult(X1,mult(mult(X1,X2),X1)) = mult(mult(X1,X1),ld(X1,mult(X1,mult(X2,X1)))),
inference(step,[status(thm)],[t114724,t276]) ).
cnf(t114726,plain,
mult(X1,mult(mult(X1,X2),X1)) = mult(mult(X1,X1),mult(X2,X1)),
inference(step,[status(thm)],[t114725,t20]) ).
cnf(t854,plain,
mult(mult(X1,X1),mult(X2,X1)) = mult(X1,mult(mult(X1,X2),X1)),
inference(orient,[status(thm)],[t114726]) ).
cnf(t872,plain,
mult(X1,mult(mult(X1,rd(X2,X1)),X1)) = mult(mult(X1,X1),X2),
inference(cp,[status(thm)],[t854,t14]) ).
cnf(t114803,plain,
mult(X1,rd(mult(X1,mult(X2,X1)),X1)) = mult(mult(X1,X1),X2),
inference(step,[status(thm)],[t872,t783]) ).
cnf(t2490,plain,
mult(X1,rd(mult(X1,mult(X2,X1)),X1)) = mult(mult(X1,X1),X2),
inference(orient,[status(thm)],[t114803]) ).
cnf(t2535,plain,
rd(mult(X1,mult(X2,X1)),X1) = ld(X1,mult(mult(X1,X1),X2)),
inference(cp,[status(thm)],[t20,t2490]) ).
cnf(t114804,plain,
rd(mult(X1,mult(X2,X1)),X1) = mult(mult(X1,X1),ld(X1,X2)),
inference(step,[status(thm)],[t2535,t276]) ).
cnf(t2610,plain,
mult(mult(X1,X1),ld(X1,X2)) = rd(mult(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t114804]) ).
cnf(t114805,plain,
ld(X1,mult(mult(X1,X1),X2)) = rd(mult(X1,mult(X2,X1)),X1),
inference(step,[status(thm)],[t276,t2610]) ).
cnf(t2611,plain,
ld(X1,mult(mult(X1,X1),X2)) = rd(mult(X1,mult(X2,X1)),X1),
inference(orient,[status(thm)],[t114805]) ).
cnf(t3138,plain,
mult(mult(mult(X1,X1),X2),i(X1)) = mult(X1,rd(rd(mult(X1,mult(X2,X1)),X1),X1)),
inference(cp,[status(thm)],[t3130,t2611]) ).
cnf(t114889,plain,
mult(mult(mult(X1,X1),X2),i(X1)) = rd(rd(mult(X1,mult(X1,mult(X2,X1))),X1),X1),
inference(step,[status(thm)],[t3138,t2212]) ).
cnf(t114890,plain,
mult(mult(mult(X1,X1),X2),i(X1)) = rd(mult(X1,mult(X1,X2)),X1),
inference(step,[status(thm)],[t114889,t1793]) ).
cnf(t7083,plain,
mult(mult(mult(X1,X1),X2),i(X1)) = rd(mult(X1,mult(X1,X2)),X1),
inference(orient,[status(thm)],[t114890]) ).
cnf(t7113,plain,
mult(mult(mult(X1,X1),X2),i(i(X1))) = rd(rd(mult(X1,mult(X1,X2)),X1),mult(i(X1),i(X1))),
inference(cp,[status(thm)],[t4170,t7083]) ).
cnf(t114891,plain,
mult(mult(mult(X1,X1),X2),X1) = rd(rd(mult(X1,mult(X1,X2)),X1),mult(i(X1),i(X1))),
inference(step,[status(thm)],[t7113,t71]) ).
cnf(t114892,plain,
mult(mult(mult(X1,X1),X2),X1) = rd(rd(mult(X1,mult(X1,X2)),X1),rd(i(X1),X1)),
inference(step,[status(thm)],[t114891,t126]) ).
cnf(t114893,plain,
mult(mult(mult(X1,X1),X2),X1) = mult(rd(mult(X1,mult(X1,X2)),X1),mult(X1,X1)),
inference(step,[status(thm)],[t114892,t4022]) ).
cnf(t114894,plain,
mult(mult(mult(X1,X1),X2),X1) = mult(X1,mult(ld(X1,mult(X1,mult(X1,X2))),X1)),
inference(step,[status(thm)],[t114893,t2932]) ).
cnf(t114895,plain,
mult(mult(mult(X1,X1),X2),X1) = rd(mult(X1,mult(X1,X2)),i(X1)),
inference(step,[status(thm)],[t114894,t3581]) ).
cnf(t114896,plain,
mult(mult(mult(X1,X1),X2),X1) = mult(X1,mult(mult(X1,X2),X1)),
inference(step,[status(thm)],[t114895,t3519]) ).
cnf(t7169,plain,
mult(mult(mult(X1,X1),X2),X1) = mult(X1,mult(mult(X1,X2),X1)),
inference(orient,[status(thm)],[t114896]) ).
cnf(t8770,plain,
mult(i(X1),mult(mult(X1,X1),X2)) = rd(ld(X1,mult(X1,mult(mult(X1,X2),X1))),X1),
inference(cp,[status(thm)],[t8749,t7169]) ).
cnf(t115010,plain,
mult(i(X1),mult(mult(X1,X1),X2)) = rd(mult(mult(X1,X2),X1),X1),
inference(step,[status(thm)],[t8770,t20]) ).
cnf(t115011,plain,
mult(i(X1),mult(mult(X1,X1),X2)) = mult(X1,X2),
inference(step,[status(thm)],[t115010,t16]) ).
cnf(t9083,plain,
mult(i(X1),mult(mult(X1,X1),X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t115011]) ).
cnf(t9121,plain,
mult(mult(X1,X1),X2) = ld(i(X1),mult(X1,X2)),
inference(cp,[status(thm)],[t20,t9083]) ).
cnf(t115012,plain,
mult(mult(X1,X1),X2) = mult(X1,ld(i(X1),X2)),
inference(step,[status(thm)],[t9121,t1146]) ).
cnf(t9150,plain,
mult(X1,ld(i(X1),X2)) = mult(mult(X1,X1),X2),
inference(orient,[status(thm)],[t115012]) ).
cnf(t9165,plain,
mult(mult(i(X1),i(X1)),X2) = mult(i(X1),ld(X1,X2)),
inference(cp,[status(thm)],[t9150,t71]) ).
cnf(t115016,plain,
mult(rd(i(X1),X1),X2) = mult(i(X1),ld(X1,X2)),
inference(step,[status(thm)],[t9165,t126]) ).
cnf(t9216,plain,
mult(rd(i(X1),X1),X2) = mult(i(X1),ld(X1,X2)),
inference(orient,[status(thm)],[t115016]) ).
cnf(t115000,plain,
rd(rd(mult(X1,X2),X1),i(X1)) = ld(i(X1),X2),
inference(step,[status(thm)],[t7261,t8887]) ).
cnf(t8894,plain,
rd(rd(mult(X1,X2),X1),i(X1)) = ld(i(X1),X2),
inference(orient,[status(thm)],[t115000]) ).
cnf(t9279,plain,
ld(i(rd(i(X1),X1)),X2) = rd(rd(mult(i(X1),ld(X1,X2)),rd(i(X1),X1)),i(rd(i(X1),X1))),
inference(cp,[status(thm)],[t8894,t9216]) ).
cnf(t303,plain,
ld(i(X1),i(i(X1))) = i(rd(i(X1),X1)),
inference(cp,[status(thm)],[t300,t126]) ).
cnf(t114682,plain,
ld(i(X1),X1) = i(rd(i(X1),X1)),
inference(step,[status(thm)],[t303,t71]) ).
cnf(t340,plain,
i(rd(i(X1),X1)) = ld(i(X1),X1),
inference(orient,[status(thm)],[t114682]) ).
cnf(t610,plain,
mult(X1,X1) = ld(i(X1),X1),
inference(cp,[status(thm)],[t73,t605]) ).
cnf(t614,plain,
ld(i(X1),X1) = mult(X1,X1),
inference(orient,[status(thm)],[t610]) ).
cnf(t114700,plain,
i(rd(i(X1),X1)) = mult(X1,X1),
inference(step,[status(thm)],[t340,t614]) ).
cnf(t615,plain,
i(rd(i(X1),X1)) = mult(X1,X1),
inference(orient,[status(thm)],[t114700]) ).
cnf(t115017,plain,
ld(mult(X1,X1),X2) = rd(rd(mult(i(X1),ld(X1,X2)),rd(i(X1),X1)),i(rd(i(X1),X1))),
inference(step,[status(thm)],[t9279,t615]) ).
cnf(t115018,plain,
ld(mult(X1,X1),X2) = rd(mult(mult(i(X1),ld(X1,X2)),mult(X1,X1)),i(rd(i(X1),X1))),
inference(step,[status(thm)],[t115017,t4022]) ).
cnf(t115019,plain,
ld(mult(X1,X1),X2) = rd(mult(mult(i(X1),ld(X1,X2)),mult(X1,X1)),mult(X1,X1)),
inference(step,[status(thm)],[t115018,t615]) ).
cnf(t115020,plain,
ld(mult(X1,X1),X2) = mult(i(X1),ld(X1,X2)),
inference(step,[status(thm)],[t115019,t16]) ).
cnf(t9370,plain,
mult(i(X1),ld(X1,X2)) = ld(mult(X1,X1),X2),
inference(orient,[status(thm)],[t115020]) ).
cnf(t115023,plain,
mult(rd(i(X1),X1),X2) = ld(mult(X1,X1),X2),
inference(step,[status(thm)],[t9216,t9370]) ).
cnf(t9373,plain,
mult(rd(i(X1),X1),X2) = ld(mult(X1,X1),X2),
inference(orient,[status(thm)],[t115023]) ).
cnf(t115206,plain,
ld(mult(X1,X1),mult(X2,X2)) = mult(i(ld(X2,mult(X1,X1))),i(i(X2))),
inference(step,[status(thm)],[t115205,t9373]) ).
cnf(t115207,plain,
ld(mult(X1,X1),mult(X2,X2)) = mult(i(ld(X2,mult(X1,X1))),X2),
inference(step,[status(thm)],[t115206,t71]) ).
cnf(t26724,plain,
mult(i(ld(X1,mult(X2,X2))),X1) = ld(mult(X2,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t115207]) ).
cnf(t30824,plain,
i(i(ld(X1,mult(X2,X2)))) = mult(ld(i(ld(X1,mult(X2,X2))),mult(i(ld(mult(X2,X2),mult(X1,X1))),i(ld(X1,mult(X2,X2))))),X1),
inference(cp,[status(thm)],[t30779,t26724]) ).
cnf(t115274,plain,
ld(X1,mult(X2,X2)) = mult(ld(i(ld(X1,mult(X2,X2))),mult(i(ld(mult(X2,X2),mult(X1,X1))),i(ld(X1,mult(X2,X2))))),X1),
inference(step,[status(thm)],[t30824,t71]) ).
cnf(t114975,plain,
ld(i(X1),mult(X2,i(X1))) = mult(X1,rd(X2,X1)),
inference(step,[status(thm)],[t4760,t8691]) ).
cnf(t8692,plain,
ld(i(X1),mult(X2,i(X1))) = mult(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t114975]) ).
cnf(t115275,plain,
ld(X1,mult(X2,X2)) = mult(mult(ld(X1,mult(X2,X2)),rd(i(ld(mult(X2,X2),mult(X1,X1))),ld(X1,mult(X2,X2)))),X1),
inference(step,[status(thm)],[t115274,t8692]) ).
cnf(t114711,plain,
i(mult(X1,X1)) = rd(i(X1),X1),
inference(step,[status(thm)],[t300,t630]) ).
cnf(t631,plain,
i(mult(X1,X1)) = rd(i(X1),X1),
inference(orient,[status(thm)],[t114711]) ).
cnf(t18965,plain,
i(ld(mult(X1,X1),mult(X2,X2))) = rd(rd(i(X2),X2),rd(i(X1),X1)),
inference(cp,[status(thm)],[t18947,t631]) ).
cnf(t115202,plain,
i(ld(mult(X1,X1),mult(X2,X2))) = mult(rd(i(X2),X2),mult(X1,X1)),
inference(step,[status(thm)],[t18965,t4022]) ).
cnf(t115203,plain,
i(ld(mult(X1,X1),mult(X2,X2))) = ld(mult(X2,X2),mult(X1,X1)),
inference(step,[status(thm)],[t115202,t9373]) ).
cnf(t26507,plain,
i(ld(mult(X1,X1),mult(X2,X2))) = ld(mult(X2,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t115203]) ).
cnf(t115276,plain,
ld(X1,mult(X2,X2)) = mult(mult(ld(X1,mult(X2,X2)),rd(ld(mult(X1,X1),mult(X2,X2)),ld(X1,mult(X2,X2)))),X1),
inference(step,[status(thm)],[t115275,t26507]) ).
cnf(t9440,plain,
i(X1) = rd(ld(mult(X1,X1),X2),ld(X1,X2)),
inference(cp,[status(thm)],[t16,t9370]) ).
cnf(t11456,plain,
rd(ld(mult(X1,X1),X2),ld(X1,X2)) = i(X1),
inference(orient,[status(thm)],[t9440]) ).
cnf(t115277,plain,
ld(X1,mult(X2,X2)) = mult(mult(ld(X1,mult(X2,X2)),i(X1)),X1),
inference(step,[status(thm)],[t115276,t11456]) ).
cnf(t115278,plain,
ld(X1,mult(X2,X2)) = mult(ld(X1,rd(mult(X2,X2),X1)),X1),
inference(step,[status(thm)],[t115277,t4378]) ).
cnf(t114981,plain,
mult(ld(X1,rd(X2,X1)),X1) = mult(i(X1),X2),
inference(step,[status(thm)],[t2074,t8749]) ).
cnf(t8750,plain,
mult(ld(X1,rd(X2,X1)),X1) = mult(i(X1),X2),
inference(orient,[status(thm)],[t114981]) ).
cnf(t115279,plain,
ld(X1,mult(X2,X2)) = mult(i(X1),mult(X2,X2)),
inference(step,[status(thm)],[t115278,t8750]) ).
cnf(t31024,plain,
mult(i(X1),mult(X2,X2)) = ld(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t115279]) ).
cnf(t31142,plain,
mult(mult(X1,X1),i(i(X2))) = ld(i(X2),rd(ld(X2,mult(X1,X1)),i(X2))),
inference(cp,[status(thm)],[t3131,t31024]) ).
cnf(t115283,plain,
mult(mult(X1,X1),X2) = ld(i(X2),rd(ld(X2,mult(X1,X1)),i(X2))),
inference(step,[status(thm)],[t31142,t71]) ).
cnf(t8161,plain,
ld(i(X1),rd(X2,i(X1))) = rd(mult(X1,X2),i(X1)),
inference(cp,[status(thm)],[t8133,t71]) ).
cnf(t114961,plain,
mult(ld(i(X1),X2),X1) = rd(mult(X1,X2),i(X1)),
inference(step,[status(thm)],[t8161,t4908]) ).
cnf(t114962,plain,
mult(ld(i(X1),X2),X1) = mult(X1,mult(X2,X1)),
inference(step,[status(thm)],[t114961,t3519]) ).
cnf(t8528,plain,
mult(ld(i(X1),X2),X1) = mult(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t114962]) ).
cnf(t114963,plain,
ld(i(X1),rd(X2,i(X1))) = mult(X1,mult(X2,X1)),
inference(step,[status(thm)],[t4908,t8528]) ).
cnf(t8529,plain,
ld(i(X1),rd(X2,i(X1))) = mult(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t114963]) ).
cnf(t115284,plain,
mult(mult(X1,X1),X2) = mult(X2,mult(ld(X2,mult(X1,X1)),X2)),
inference(step,[status(thm)],[t115283,t8529]) ).
cnf(t115285,plain,
mult(mult(X1,X1),X2) = rd(mult(X1,X1),i(X2)),
inference(step,[status(thm)],[t115284,t3581]) ).
cnf(t31274,plain,
rd(mult(X1,X1),i(X2)) = mult(mult(X1,X1),X2),
inference(orient,[status(thm)],[t115285]) ).
cnf(t115288,plain,
i(mult(mult(X1,X1),X2)) = ld(X2,rd(i(X1),X1)),
inference(step,[status(thm)],[t18769,t31274]) ).
cnf(t31359,plain,
i(mult(mult(X1,X1),X2)) = ld(X2,rd(i(X1),X1)),
inference(rw,[status(thm)],[t115288]) ).
cnf(t31046,plain,
ld(X1,mult(i(X2),i(X2))) = mult(i(X1),rd(i(X2),X2)),
inference(cp,[status(thm)],[t31024,t126]) ).
cnf(t115316,plain,
ld(X1,rd(i(X2),X2)) = mult(i(X1),rd(i(X2),X2)),
inference(step,[status(thm)],[t31046,t126]) ).
cnf(t115317,plain,
ld(X1,rd(i(X2),X2)) = rd(i(X1),mult(X2,X2)),
inference(step,[status(thm)],[t115316,t3981]) ).
cnf(t32454,plain,
ld(X1,rd(i(X2),X2)) = rd(i(X1),mult(X2,X2)),
inference(orient,[status(thm)],[t115317]) ).
cnf(t115319,plain,
i(mult(mult(X1,X1),X2)) = rd(i(X2),mult(X1,X1)),
inference(step,[status(thm)],[t31359,t32454]) ).
cnf(t32804,plain,
i(mult(mult(X1,X1),X2)) = rd(i(X2),mult(X1,X1)),
inference(orient,[status(thm)],[t115319]) ).
cnf(t114998,plain,
mult(mult(X1,X1),ld(X1,X2)) = ld(i(X1),X2),
inference(step,[status(thm)],[t2610,t8887]) ).
cnf(t8892,plain,
mult(mult(X1,X1),ld(X1,X2)) = ld(i(X1),X2),
inference(orient,[status(thm)],[t114998]) ).
cnf(t32808,plain,
rd(i(ld(X1,X2)),mult(X1,X1)) = i(ld(i(X1),X2)),
inference(cp,[status(thm)],[t32804,t8892]) ).
cnf(t1955,plain,
mult(mult(X1,rd(X2,X1)),mult(X1,X1)) = mult(mult(X1,X2),X1),
inference(cp,[status(thm)],[t1925,t14]) ).
cnf(t114807,plain,
mult(X1,mult(rd(X2,X1),mult(X1,X1))) = mult(mult(X1,X2),X1),
inference(step,[status(thm)],[t1955,t2257]) ).
cnf(t1907,plain,
mult(rd(X1,X2),mult(X2,X2)) = rd(mult(X1,mult(X2,X2)),X2),
inference(cp,[status(thm)],[t1878,t14]) ).
cnf(t1984,plain,
mult(rd(X1,X2),mult(X2,X2)) = rd(mult(X1,mult(X2,X2)),X2),
inference(orient,[status(thm)],[t1907]) ).
cnf(t114808,plain,
mult(X1,rd(mult(X2,mult(X1,X1)),X1)) = mult(mult(X1,X2),X1),
inference(step,[status(thm)],[t114807,t1984]) ).
cnf(t2756,plain,
mult(X1,rd(mult(X2,mult(X1,X1)),X1)) = mult(mult(X1,X2),X1),
inference(orient,[status(thm)],[t114808]) ).
cnf(t114837,plain,
mult(X1,rd(X2,i(X1))) = mult(mult(X1,X2),X1),
inference(step,[status(thm)],[t2756,t3578]) ).
cnf(t3621,plain,
mult(X1,rd(X2,i(X1))) = mult(mult(X1,X2),X1),
inference(rw,[status(thm)],[t114837]) ).
cnf(t3711,plain,
mult(X1,rd(X2,i(X1))) = mult(mult(X1,X2),X1),
inference(orient,[status(thm)],[t3621]) ).
cnf(t3720,plain,
mult(mult(i(X1),X2),i(X1)) = mult(i(X1),rd(X2,X1)),
inference(cp,[status(thm)],[t3711,t71]) ).
cnf(t4794,plain,
mult(mult(i(X1),X2),i(X1)) = mult(i(X1),rd(X2,X1)),
inference(orient,[status(thm)],[t3720]) ).
cnf(t3395,plain,
rd(rd(rd(X1,i(X2)),X2),X2) = mult(X1,i(X2)),
inference(cp,[status(thm)],[t3384,t14]) ).
cnf(t114862,plain,
rd(rd(rd(X1,X2),i(X2)),X2) = mult(X1,i(X2)),
inference(step,[status(thm)],[t3395,t1463]) ).
cnf(t114863,plain,
rd(rd(rd(X1,X2),X2),i(X2)) = mult(X1,i(X2)),
inference(step,[status(thm)],[t114862,t1463]) ).
cnf(t4938,plain,
rd(rd(rd(X1,X2),X2),i(X2)) = mult(X1,i(X2)),
inference(orient,[status(thm)],[t114863]) ).
cnf(t8188,plain,
mult(mult(i(X1),X2),i(X1)) = rd(rd(ld(X1,rd(X2,X1)),X1),i(X1)),
inference(cp,[status(thm)],[t4938,t8133]) ).
cnf(t114965,plain,
mult(i(X1),rd(X2,X1)) = rd(rd(ld(X1,rd(X2,X1)),X1),i(X1)),
inference(step,[status(thm)],[t8188,t4794]) ).
cnf(t114966,plain,
mult(i(X1),rd(X2,X1)) = rd(ld(X1,mult(rd(X2,X1),X1)),X1),
inference(step,[status(thm)],[t114965,t7598]) ).
cnf(t114967,plain,
mult(i(X1),rd(X2,X1)) = rd(ld(X1,X2),X1),
inference(step,[status(thm)],[t114966,t14]) ).
cnf(t8618,plain,
mult(i(X1),rd(X2,X1)) = rd(ld(X1,X2),X1),
inference(orient,[status(thm)],[t114967]) ).
cnf(t114968,plain,
mult(mult(i(X1),X2),i(X1)) = rd(ld(X1,X2),X1),
inference(step,[status(thm)],[t4794,t8618]) ).
cnf(t8619,plain,
mult(mult(i(X1),X2),i(X1)) = rd(ld(X1,X2),X1),
inference(orient,[status(thm)],[t114968]) ).
cnf(t16550,plain,
mult(i(X1),rd(X1,X2)) = rd(i(ld(X1,X2)),X1),
inference(cp,[status(thm)],[t8749,t16439]) ).
cnf(t17013,plain,
mult(i(X1),rd(X1,X2)) = rd(i(ld(X1,X2)),X1),
inference(orient,[status(thm)],[t16550]) ).
cnf(t17144,plain,
rd(ld(X1,rd(X1,X2)),X1) = mult(rd(i(ld(X1,X2)),X1),i(X1)),
inference(cp,[status(thm)],[t8619,t17013]) ).
cnf(t115199,plain,
rd(ld(X1,rd(X1,X2)),X1) = rd(i(ld(X1,X2)),mult(X1,X1)),
inference(step,[status(thm)],[t17144,t3979]) ).
cnf(t26164,plain,
rd(i(ld(X1,X2)),mult(X1,X1)) = rd(ld(X1,rd(X1,X2)),X1),
inference(orient,[status(thm)],[t115199]) ).
cnf(t115324,plain,
rd(ld(X1,rd(X1,X2)),X1) = i(ld(i(X1),X2)),
inference(step,[status(thm)],[t32808,t26164]) ).
cnf(t33612,plain,
rd(ld(X1,rd(X1,X2)),X1) = i(ld(i(X1),X2)),
inference(orient,[status(thm)],[t115324]) ).
cnf(t33759,plain,
ld(X1,mult(ld(i(X1),rd(i(X1),X2)),X1)) = mult(i(X1),i(ld(i(i(X1)),X2))),
inference(cp,[status(thm)],[t8395,t33612]) ).
cnf(t115376,plain,
ld(X1,mult(X1,mult(rd(i(X1),X2),X1))) = mult(i(X1),i(ld(i(i(X1)),X2))),
inference(step,[status(thm)],[t33759,t8528]) ).
cnf(t115377,plain,
mult(rd(i(X1),X2),X1) = mult(i(X1),i(ld(i(i(X1)),X2))),
inference(step,[status(thm)],[t115376,t20]) ).
cnf(t115378,plain,
mult(rd(i(X1),X2),X1) = mult(i(X1),i(ld(X1,X2))),
inference(step,[status(thm)],[t115377,t71]) ).
cnf(t37515,plain,
mult(i(X1),i(ld(X1,X2))) = mult(rd(i(X1),X2),X1),
inference(orient,[status(thm)],[t115378]) ).
cnf(t37616,plain,
mult(rd(i(i(X1)),mult(X2,X1)),i(X1)) = mult(i(i(X1)),i(mult(mult(X1,X2),X1))),
inference(cp,[status(thm)],[t37515,t8213]) ).
cnf(t115379,plain,
mult(rd(X1,mult(X2,X1)),i(X1)) = mult(i(i(X1)),i(mult(mult(X1,X2),X1))),
inference(step,[status(thm)],[t37616,t71]) ).
cnf(t15843,plain,
rd(ld(X1,X2),mult(X2,X2)) = mult(rd(X2,mult(X1,X2)),i(X2)),
inference(cp,[status(thm)],[t3979,t15776]) ).
cnf(t24164,plain,
mult(rd(X1,mult(X2,X1)),i(X1)) = rd(ld(X2,X1),mult(X1,X1)),
inference(orient,[status(thm)],[t15843]) ).
cnf(t115380,plain,
rd(ld(X2,X1),mult(X1,X1)) = mult(i(i(X1)),i(mult(mult(X1,X2),X1))),
inference(step,[status(thm)],[t115379,t24164]) ).
cnf(t115381,plain,
rd(ld(X2,X1),mult(X1,X1)) = mult(X1,i(mult(mult(X1,X2),X1))),
inference(step,[status(thm)],[t115380,t71]) ).
cnf(t115013,plain,
ld(i(X1),mult(X1,X2)) = mult(mult(X1,X1),X2),
inference(step,[status(thm)],[t1146,t9150]) ).
cnf(t9151,plain,
ld(i(X1),mult(X1,X2)) = mult(mult(X1,X1),X2),
inference(orient,[status(thm)],[t115013]) ).
cnf(t15124,plain,
mult(X1,i(mult(mult(X1,X2),X1))) = ld(mult(mult(X1,X1),X2),X1),
inference(cp,[status(thm)],[t15117,t9151]) ).
cnf(t22951,plain,
mult(X1,i(mult(mult(X1,X2),X1))) = ld(mult(mult(X1,X1),X2),X1),
inference(orient,[status(thm)],[t15124]) ).
cnf(t33770,plain,
mult(i(X1),ld(X1,rd(X1,X2))) = mult(ld(X1,i(ld(i(X1),X2))),X1),
inference(cp,[status(thm)],[t8750,t33612]) ).
cnf(t115331,plain,
ld(mult(X1,X1),rd(X1,X2)) = mult(ld(X1,i(ld(i(X1),X2))),X1),
inference(step,[status(thm)],[t33770,t9370]) ).
cnf(t8897,plain,
ld(i(X1),ld(X1,X2)) = rd(rd(X2,i(X1)),X1),
inference(cp,[status(thm)],[t8887,t3581]) ).
cnf(t1355,plain,
ld(i(X1),ld(X1,X2)) = ld(X1,ld(i(X1),X2)),
inference(cp,[status(thm)],[t20,t1339]) ).
cnf(t1370,plain,
ld(i(X1),ld(X1,X2)) = ld(X1,ld(i(X1),X2)),
inference(orient,[status(thm)],[t1355]) ).
cnf(t115002,plain,
ld(X1,ld(i(X1),X2)) = rd(rd(X2,i(X1)),X1),
inference(step,[status(thm)],[t8897,t1370]) ).
cnf(t115003,plain,
ld(X1,ld(i(X1),X2)) = rd(rd(X2,X1),i(X1)),
inference(step,[status(thm)],[t115002,t1463]) ).
cnf(t8982,plain,
ld(X1,ld(i(X1),X2)) = rd(rd(X2,X1),i(X1)),
inference(orient,[status(thm)],[t115003]) ).
cnf(t16549,plain,
rd(rd(mult(rd(i(X1),X2),i(X1)),X1),i(X1)) = ld(X1,i(ld(i(X1),X2))),
inference(cp,[status(thm)],[t8982,t16439]) ).
cnf(t115141,plain,
rd(rd(rd(i(X1),X2),mult(X1,X1)),i(X1)) = ld(X1,i(ld(i(X1),X2))),
inference(step,[status(thm)],[t16549,t3978]) ).
cnf(t3597,plain,
rd(rd(X1,mult(X2,X2)),i(X2)) = rd(X1,X2),
inference(cp,[status(thm)],[t3578,t14]) ).
cnf(t4276,plain,
rd(rd(X1,mult(X2,X2)),i(X2)) = rd(X1,X2),
inference(orient,[status(thm)],[t3597]) ).
cnf(t115142,plain,
rd(rd(i(X1),X2),X1) = ld(X1,i(ld(i(X1),X2))),
inference(step,[status(thm)],[t115141,t4276]) ).
cnf(t18462,plain,
ld(X1,i(ld(i(X1),X2))) = rd(rd(i(X1),X2),X1),
inference(orient,[status(thm)],[t115142]) ).
cnf(t115332,plain,
ld(mult(X1,X1),rd(X1,X2)) = mult(rd(rd(i(X1),X2),X1),X1),
inference(step,[status(thm)],[t115331,t18462]) ).
cnf(t115333,plain,
ld(mult(X1,X1),rd(X1,X2)) = rd(i(X1),X2),
inference(step,[status(thm)],[t115332,t14]) ).
cnf(t33943,plain,
ld(mult(X1,X1),rd(X1,X2)) = rd(i(X1),X2),
inference(orient,[status(thm)],[t115333]) ).
cnf(t33958,plain,
rd(i(X1),ld(X2,X1)) = ld(mult(X1,X1),X2),
inference(cp,[status(thm)],[t33943,t72]) ).
cnf(t34098,plain,
rd(i(X1),ld(X2,X1)) = ld(mult(X1,X1),X2),
inference(orient,[status(thm)],[t33958]) ).
cnf(t34112,plain,
ld(mult(i(X1),i(X1)),X2) = rd(X1,ld(X2,i(X1))),
inference(cp,[status(thm)],[t34098,t71]) ).
cnf(t115336,plain,
ld(rd(i(X1),X1),X2) = rd(X1,ld(X2,i(X1))),
inference(step,[status(thm)],[t34112,t126]) ).
cnf(t9379,plain,
ld(mult(i(X1),i(X1)),X2) = mult(X1,ld(i(X1),X2)),
inference(cp,[status(thm)],[t9370,t71]) ).
cnf(t115025,plain,
ld(rd(i(X1),X1),X2) = mult(X1,ld(i(X1),X2)),
inference(step,[status(thm)],[t9379,t126]) ).
cnf(t115026,plain,
ld(rd(i(X1),X1),X2) = mult(mult(X1,X1),X2),
inference(step,[status(thm)],[t115025,t9150]) ).
cnf(t9476,plain,
ld(rd(i(X1),X1),X2) = mult(mult(X1,X1),X2),
inference(orient,[status(thm)],[t115026]) ).
cnf(t115337,plain,
mult(mult(X1,X1),X2) = rd(X1,ld(X2,i(X1))),
inference(step,[status(thm)],[t115336,t9476]) ).
cnf(t34258,plain,
rd(X1,ld(X2,i(X1))) = mult(mult(X1,X1),X2),
inference(orient,[status(thm)],[t115337]) ).
cnf(t34292,plain,
ld(X1,i(X2)) = ld(mult(mult(X2,X2),X1),X2),
inference(cp,[status(thm)],[t73,t34258]) ).
cnf(t34659,plain,
ld(mult(mult(X1,X1),X2),X1) = ld(X2,i(X1)),
inference(orient,[status(thm)],[t34292]) ).
cnf(t115346,plain,
mult(X1,i(mult(mult(X1,X2),X1))) = ld(X2,i(X1)),
inference(step,[status(thm)],[t22951,t34659]) ).
cnf(t34660,plain,
mult(X1,i(mult(mult(X1,X2),X1))) = ld(X2,i(X1)),
inference(orient,[status(thm)],[t115346]) ).
cnf(t115382,plain,
rd(ld(X2,X1),mult(X1,X1)) = ld(X2,i(X1)),
inference(step,[status(thm)],[t115381,t34660]) ).
cnf(t37767,plain,
rd(ld(X1,X2),mult(X2,X2)) = ld(X1,i(X2)),
inference(orient,[status(thm)],[t115382]) ).
cnf(t115411,plain,
ld(mult(X2,i(X1)),i(X1)) = rd(rd(i(i(X1)),X2),X1),
inference(step,[status(thm)],[t115410,t37767]) ).
cnf(t3154,plain,
mult(X1,mult(mult(X1,X1),rd(ld(X1,X2),X1))) = mult(mult(X1,X1),mult(X2,i(X1))),
inference(cp,[status(thm)],[t74,t3130]) ).
cnf(t2525,plain,
mult(mult(X1,X1),rd(X2,X1)) = mult(X1,rd(mult(X1,X2),X1)),
inference(cp,[status(thm)],[t2490,t14]) ).
cnf(t2562,plain,
mult(mult(X1,X1),rd(X2,X1)) = mult(X1,rd(mult(X1,X2),X1)),
inference(orient,[status(thm)],[t2525]) ).
cnf(t7267,plain,
rd(mult(X1,mult(mult(X1,rd(X2,X1)),X1)),X1) = rd(rd(rd(mult(X1,mult(X1,X2)),X1),X1),i(X1)),
inference(cp,[status(thm)],[t7261,t1837]) ).
cnf(t114900,plain,
rd(mult(X1,rd(mult(X1,mult(X2,X1)),X1)),X1) = rd(rd(rd(mult(X1,mult(X1,X2)),X1),X1),i(X1)),
inference(step,[status(thm)],[t7267,t783]) ).
cnf(t114901,plain,
rd(mult(mult(X1,X1),X2),X1) = rd(rd(rd(mult(X1,mult(X1,X2)),X1),X1),i(X1)),
inference(step,[status(thm)],[t114900,t2490]) ).
cnf(t114902,plain,
rd(mult(mult(X1,X1),X2),X1) = mult(mult(X1,mult(X1,X2)),i(X1)),
inference(step,[status(thm)],[t114901,t4938]) ).
cnf(t114903,plain,
rd(mult(mult(X1,X1),X2),X1) = mult(X1,rd(mult(X1,X2),X1)),
inference(step,[status(thm)],[t114902,t3182]) ).
cnf(t7344,plain,
mult(X1,rd(mult(X1,X2),X1)) = rd(mult(mult(X1,X1),X2),X1),
inference(orient,[status(thm)],[t114903]) ).
cnf(t114904,plain,
mult(mult(X1,X1),rd(X2,X1)) = rd(mult(mult(X1,X1),X2),X1),
inference(step,[status(thm)],[t2562,t7344]) ).
cnf(t7345,plain,
mult(mult(X1,X1),rd(X2,X1)) = rd(mult(mult(X1,X1),X2),X1),
inference(orient,[status(thm)],[t114904]) ).
cnf(t114908,plain,
mult(X1,rd(mult(mult(X1,X1),ld(X1,X2)),X1)) = mult(mult(X1,X1),mult(X2,i(X1))),
inference(step,[status(thm)],[t3154,t7345]) ).
cnf(t114909,plain,
mult(X1,rd(rd(mult(X1,mult(X2,X1)),X1),X1)) = mult(mult(X1,X1),mult(X2,i(X1))),
inference(step,[status(thm)],[t114908,t2610]) ).
cnf(t114910,plain,
mult(X1,mult(X1,rd(X2,X1))) = mult(mult(X1,X1),mult(X2,i(X1))),
inference(step,[status(thm)],[t114909,t2118]) ).
cnf(t114911,plain,
rd(mult(X1,mult(X1,X2)),X1) = mult(mult(X1,X1),mult(X2,i(X1))),
inference(step,[status(thm)],[t114910,t1837]) ).
cnf(t7456,plain,
mult(mult(X1,X1),mult(X2,i(X1))) = rd(mult(X1,mult(X1,X2)),X1),
inference(orient,[status(thm)],[t114911]) ).
cnf(t34674,plain,
ld(mult(X1,i(X2)),i(X2)) = ld(rd(mult(X2,mult(X2,X1)),X2),X2),
inference(cp,[status(thm)],[t34659,t7456]) ).
cnf(t115399,plain,
ld(mult(X1,i(X2)),i(X2)) = mult(rd(X2,mult(X2,mult(X2,X1))),X2),
inference(step,[status(thm)],[t34674,t16007]) ).
cnf(t15133,plain,
mult(X1,i(mult(rd(X2,i(i(X1))),X1))) = ld(mult(ld(i(X1),X2),i(X1)),X1),
inference(cp,[status(thm)],[t15117,t4255]) ).
cnf(t115128,plain,
mult(X1,i(mult(rd(X2,X1),X1))) = ld(mult(ld(i(X1),X2),i(X1)),X1),
inference(step,[status(thm)],[t15133,t71]) ).
cnf(t115129,plain,
mult(X1,i(X2)) = ld(mult(ld(i(X1),X2),i(X1)),X1),
inference(step,[status(thm)],[t115128,t14]) ).
cnf(t114959,plain,
mult(ld(i(X1),X2),i(X1)) = rd(mult(X1,X2),X1),
inference(step,[status(thm)],[t4853,t8480]) ).
cnf(t8481,plain,
mult(ld(i(X1),X2),i(X1)) = rd(mult(X1,X2),X1),
inference(orient,[status(thm)],[t114959]) ).
cnf(t115130,plain,
mult(X1,i(X2)) = ld(rd(mult(X1,X2),X1),X1),
inference(step,[status(thm)],[t115129,t8481]) ).
cnf(t115131,plain,
mult(X1,i(X2)) = mult(rd(X1,mult(X1,X2)),X1),
inference(step,[status(thm)],[t115130,t16007]) ).
cnf(t16267,plain,
mult(rd(X1,mult(X1,X2)),X1) = mult(X1,i(X2)),
inference(orient,[status(thm)],[t115131]) ).
cnf(t115400,plain,
ld(mult(X1,i(X2)),i(X2)) = mult(X2,i(mult(X2,X1))),
inference(step,[status(thm)],[t115399,t16267]) ).
cnf(t40606,plain,
ld(mult(X1,i(X2)),i(X2)) = mult(X2,i(mult(X2,X1))),
inference(orient,[status(thm)],[t115400]) ).
cnf(t115412,plain,
mult(X1,i(mult(X1,X2))) = rd(rd(i(i(X1)),X2),X1),
inference(step,[status(thm)],[t115411,t40606]) ).
cnf(t115413,plain,
mult(X1,i(mult(X1,X2))) = rd(rd(X1,X2),X1),
inference(step,[status(thm)],[t115412,t71]) ).
cnf(t41985,plain,
mult(X1,i(mult(X1,X2))) = rd(rd(X1,X2),X1),
inference(orient,[status(thm)],[t115413]) ).
cnf(t42121,plain,
i(mult(X1,X2)) = ld(X1,rd(rd(X1,X2),X1)),
inference(cp,[status(thm)],[t20,t41985]) ).
cnf(t44150,plain,
ld(X1,rd(rd(X1,X2),X1)) = i(mult(X1,X2)),
inference(orient,[status(thm)],[t42121]) ).
cnf(t37925,plain,
rd(ld(X1,X2),X2) = rd(ld(X1,i(X2)),i(X2)),
inference(cp,[status(thm)],[t4276,t37767]) ).
cnf(t115390,plain,
rd(X2,mult(X1,X2)) = rd(ld(X1,i(X2)),i(X2)),
inference(step,[status(thm)],[t37925,t15776]) ).
cnf(t115391,plain,
rd(X2,mult(X1,X2)) = rd(i(X2),mult(X1,i(X2))),
inference(step,[status(thm)],[t115390,t15776]) ).
cnf(t39634,plain,
rd(i(X1),mult(X2,i(X1))) = rd(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t115391]) ).
cnf(t44213,plain,
i(mult(i(X1),mult(X2,i(X1)))) = ld(i(X1),rd(rd(X1,mult(X2,X1)),i(X1))),
inference(cp,[status(thm)],[t44150,t39634]) ).
cnf(t114923,plain,
mult(i(X1),mult(X2,i(X1))) = ld(X1,rd(X2,X1)),
inference(step,[status(thm)],[t4697,t8133]) ).
cnf(t8134,plain,
mult(i(X1),mult(X2,i(X1))) = ld(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t114923]) ).
cnf(t115454,plain,
i(ld(X1,rd(X2,X1))) = ld(i(X1),rd(rd(X1,mult(X2,X1)),i(X1))),
inference(step,[status(thm)],[t44213,t8134]) ).
cnf(t115455,plain,
i(ld(X1,rd(X2,X1))) = mult(X1,mult(rd(X1,mult(X2,X1)),X1)),
inference(step,[status(thm)],[t115454,t8529]) ).
cnf(t115456,plain,
i(ld(X1,rd(X2,X1))) = mult(X1,ld(X2,X1)),
inference(step,[status(thm)],[t115455,t16097]) ).
cnf(t44679,plain,
i(ld(X1,rd(X2,X1))) = mult(X1,ld(X2,X1)),
inference(orient,[status(thm)],[t115456]) ).
cnf(t44728,plain,
mult(X1,ld(ld(i(X1),X2),X1)) = i(ld(X1,mult(X1,rd(X2,X1)))),
inference(cp,[status(thm)],[t44679,t8691]) ).
cnf(t115537,plain,
mult(X1,mult(X1,i(mult(X2,X1)))) = i(ld(X1,mult(X1,rd(X2,X1)))),
inference(step,[status(thm)],[t44728,t15117]) ).
cnf(t115538,plain,
mult(X1,mult(X1,i(mult(X2,X1)))) = i(rd(X2,X1)),
inference(step,[status(thm)],[t115537,t20]) ).
cnf(t55287,plain,
mult(X1,mult(X1,i(mult(X2,X1)))) = i(rd(X2,X1)),
inference(orient,[status(thm)],[t115538]) ).
cnf(t31146,plain,
rd(mult(X1,X1),i(i(X2))) = ld(i(X2),mult(ld(X2,mult(X1,X1)),i(X2))),
inference(cp,[status(thm)],[t3579,t31024]) ).
cnf(t115289,plain,
rd(mult(X1,X1),X2) = ld(i(X2),mult(ld(X2,mult(X1,X1)),i(X2))),
inference(step,[status(thm)],[t31146,t71]) ).
cnf(t115290,plain,
rd(mult(X1,X1),X2) = mult(X2,rd(ld(X2,mult(X1,X1)),X2)),
inference(step,[status(thm)],[t115289,t8692]) ).
cnf(t115291,plain,
rd(mult(X1,X1),X2) = mult(mult(X1,X1),i(X2)),
inference(step,[status(thm)],[t115290,t3130]) ).
cnf(t31360,plain,
mult(mult(X1,X1),i(X2)) = rd(mult(X1,X1),X2),
inference(orient,[status(thm)],[t115291]) ).
cnf(t31482,plain,
rd(i(X1),i(mult(X2,X2))) = ld(mult(X2,X2),mult(rd(mult(X2,X2),X1),mult(X2,X2))),
inference(cp,[status(thm)],[t3579,t31360]) ).
cnf(t115309,plain,
rd(i(X1),rd(i(X2),X2)) = ld(mult(X2,X2),mult(rd(mult(X2,X2),X1),mult(X2,X2))),
inference(step,[status(thm)],[t31482,t631]) ).
cnf(t115310,plain,
mult(i(X1),mult(X2,X2)) = ld(mult(X2,X2),mult(rd(mult(X2,X2),X1),mult(X2,X2))),
inference(step,[status(thm)],[t115309,t4022]) ).
cnf(t115311,plain,
ld(X1,mult(X2,X2)) = ld(mult(X2,X2),mult(rd(mult(X2,X2),X1),mult(X2,X2))),
inference(step,[status(thm)],[t115310,t31024]) ).
cnf(t115312,plain,
ld(X1,mult(X2,X2)) = i(ld(mult(X2,X2),X1)),
inference(step,[status(thm)],[t115311,t16439]) ).
cnf(t31975,plain,
i(ld(mult(X1,X1),X2)) = ld(X2,mult(X1,X1)),
inference(orient,[status(thm)],[t115312]) ).
cnf(t34049,plain,
ld(rd(X1,X2),mult(X1,X1)) = i(rd(i(X1),X2)),
inference(cp,[status(thm)],[t31975,t33943]) ).
cnf(t36107,plain,
ld(rd(X1,X2),mult(X1,X1)) = i(rd(i(X1),X2)),
inference(orient,[status(thm)],[t34049]) ).
cnf(t36187,plain,
i(rd(i(mult(X1,X2)),X2)) = ld(X1,mult(mult(X1,X2),mult(X1,X2))),
inference(cp,[status(thm)],[t36107,t16]) ).
cnf(t115401,plain,
i(rd(i(mult(X1,X2)),X2)) = mult(ld(X1,mult(mult(X1,X2),X1)),X2),
inference(step,[status(thm)],[t36187,t28990]) ).
cnf(t115402,plain,
i(rd(i(mult(X1,X2)),X2)) = mult(rd(X2,i(X1)),X2),
inference(step,[status(thm)],[t115401,t3579]) ).
cnf(t40731,plain,
i(rd(i(mult(X1,X2)),X2)) = mult(rd(X2,i(X1)),X2),
inference(orient,[status(thm)],[t115402]) ).
cnf(t40873,plain,
rd(i(mult(X1,X2)),X2) = i(mult(rd(X2,i(X1)),X2)),
inference(cp,[status(thm)],[t71,t40731]) ).
cnf(t41068,plain,
i(mult(rd(X1,i(X2)),X1)) = rd(i(mult(X2,X1)),X1),
inference(orient,[status(thm)],[t40873]) ).
cnf(t55297,plain,
i(rd(rd(X1,i(X2)),X1)) = mult(X1,mult(X1,rd(i(mult(X2,X1)),X1))),
inference(cp,[status(thm)],[t55287,t41068]) ).
cnf(t115539,plain,
i(rd(rd(X1,i(X2)),X1)) = rd(mult(X1,mult(X1,i(mult(X2,X1)))),X1),
inference(step,[status(thm)],[t55297,t1837]) ).
cnf(t115540,plain,
i(rd(rd(X1,i(X2)),X1)) = rd(i(rd(X2,X1)),X1),
inference(step,[status(thm)],[t115539,t55287]) ).
cnf(t55548,plain,
i(rd(rd(X1,i(X2)),X1)) = rd(i(rd(X2,X1)),X1),
inference(orient,[status(thm)],[t115540]) ).
cnf(t55629,plain,
rd(i(rd(i(X1),X2)),X2) = i(rd(rd(X2,X1),X2)),
inference(cp,[status(thm)],[t55548,t71]) ).
cnf(t55905,plain,
rd(i(rd(i(X1),X2)),X2) = i(rd(rd(X2,X1),X2)),
inference(orient,[status(thm)],[t55629]) ).
cnf(t56067,plain,
mult(i(X1),i(rd(i(X2),X1))) = mult(ld(X1,i(rd(rd(X1,X2),X1))),X1),
inference(cp,[status(thm)],[t8750,t55905]) ).
cnf(t8803,plain,
rd(mult(mult(X1,X1),ld(X1,mult(X2,X1))),X1) = mult(mult(X1,X1),mult(i(X1),X2)),
inference(cp,[status(thm)],[t7345,t8749]) ).
cnf(t115032,plain,
rd(ld(i(X1),mult(X2,X1)),X1) = mult(mult(X1,X1),mult(i(X1),X2)),
inference(step,[status(thm)],[t8803,t8892]) ).
cnf(t115033,plain,
rd(mult(mult(X1,X2),X1),X1) = mult(mult(X1,X1),mult(i(X1),X2)),
inference(step,[status(thm)],[t115032,t8213]) ).
cnf(t115034,plain,
mult(X1,X2) = mult(mult(X1,X1),mult(i(X1),X2)),
inference(step,[status(thm)],[t115033,t16]) ).
cnf(t9995,plain,
mult(mult(X1,X1),mult(i(X1),X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t115034]) ).
cnf(t34667,plain,
ld(mult(i(X1),X2),i(X1)) = ld(mult(X1,X2),X1),
inference(cp,[status(thm)],[t34659,t9995]) ).
cnf(t14959,plain,
ld(mult(mult(i(X1),mult(X2,X1)),i(X1)),i(X1)) = mult(i(X1),i(mult(rd(rd(X2,X1),i(X1)),i(X1)))),
inference(cp,[status(thm)],[t14921,t3441]) ).
cnf(t115151,plain,
ld(rd(ld(X1,mult(X2,X1)),X1),i(X1)) = mult(i(X1),i(mult(rd(rd(X2,X1),i(X1)),i(X1)))),
inference(step,[status(thm)],[t14959,t8619]) ).
cnf(t115152,plain,
ld(mult(i(X1),X2),i(X1)) = mult(i(X1),i(mult(rd(rd(X2,X1),i(X1)),i(X1)))),
inference(step,[status(thm)],[t115151,t8749]) ).
cnf(t115153,plain,
ld(mult(i(X1),X2),i(X1)) = mult(i(X1),i(rd(X2,X1))),
inference(step,[status(thm)],[t115152,t14]) ).
cnf(t19660,plain,
ld(mult(i(X1),X2),i(X1)) = mult(i(X1),i(rd(X2,X1))),
inference(orient,[status(thm)],[t115153]) ).
cnf(t115366,plain,
mult(i(X1),i(rd(X2,X1))) = ld(mult(X1,X2),X1),
inference(step,[status(thm)],[t34667,t19660]) ).
cnf(t36644,plain,
mult(i(X1),i(rd(X2,X1))) = ld(mult(X1,X2),X1),
inference(orient,[status(thm)],[t115366]) ).
cnf(t115541,plain,
ld(mult(X1,i(X2)),X1) = mult(ld(X1,i(rd(rd(X1,X2),X1))),X1),
inference(step,[status(thm)],[t56067,t36644]) ).
cnf(t41612,plain,
rd(i(i(X1)),ld(X1,X2)) = ld(i(X1),mult(i(ld(mult(X1,X1),X2)),i(X1))),
inference(cp,[status(thm)],[t41534,t9370]) ).
cnf(t115403,plain,
rd(X1,ld(X1,X2)) = ld(i(X1),mult(i(ld(mult(X1,X1),X2)),i(X1))),
inference(step,[status(thm)],[t41612,t71]) ).
cnf(t115404,plain,
rd(X1,ld(X1,X2)) = mult(X1,rd(i(ld(mult(X1,X1),X2)),X1)),
inference(step,[status(thm)],[t115403,t8692]) ).
cnf(t115405,plain,
rd(X1,ld(X1,X2)) = mult(X1,rd(ld(X2,mult(X1,X1)),X1)),
inference(step,[status(thm)],[t115404,t31975]) ).
cnf(t31141,plain,
rd(i(X1),i(X2)) = rd(ld(X1,mult(X2,X2)),X2),
inference(cp,[status(thm)],[t3578,t31024]) ).
cnf(t33118,plain,
rd(ld(X1,mult(X2,X2)),X2) = rd(i(X1),i(X2)),
inference(orient,[status(thm)],[t31141]) ).
cnf(t115406,plain,
rd(X1,ld(X1,X2)) = mult(X1,rd(i(X2),i(X1))),
inference(step,[status(thm)],[t115405,t33118]) ).
cnf(t115407,plain,
rd(X1,ld(X1,X2)) = mult(mult(X1,i(X2)),X1),
inference(step,[status(thm)],[t115406,t3711]) ).
cnf(t41741,plain,
mult(mult(X1,i(X2)),X1) = rd(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t115407]) ).
cnf(t41812,plain,
rd(X1,ld(X1,i(X2))) = mult(mult(X1,X2),X1),
inference(cp,[status(thm)],[t41741,t71]) ).
cnf(t42274,plain,
rd(X1,ld(X1,i(X2))) = mult(mult(X1,X2),X1),
inference(orient,[status(thm)],[t41812]) ).
cnf(t42330,plain,
ld(X1,i(X2)) = ld(mult(mult(X1,X2),X1),X1),
inference(cp,[status(thm)],[t73,t42274]) ).
cnf(t45946,plain,
ld(mult(mult(X1,X2),X1),X1) = ld(X1,i(X2)),
inference(orient,[status(thm)],[t42330]) ).
cnf(t45952,plain,
ld(X1,i(rd(X2,X1))) = ld(ld(i(X1),X2),X1),
inference(cp,[status(thm)],[t45946,t8890]) ).
cnf(t115466,plain,
ld(X1,i(rd(X2,X1))) = mult(X1,i(mult(X2,X1))),
inference(step,[status(thm)],[t45952,t15117]) ).
cnf(t46120,plain,
ld(X1,i(rd(X2,X1))) = mult(X1,i(mult(X2,X1))),
inference(orient,[status(thm)],[t115466]) ).
cnf(t115542,plain,
ld(mult(X1,i(X2)),X1) = mult(mult(X1,i(mult(rd(X1,X2),X1))),X1),
inference(step,[status(thm)],[t115541,t46120]) ).
cnf(t115543,plain,
ld(mult(X1,i(X2)),X1) = rd(X1,ld(X1,mult(rd(X1,X2),X1))),
inference(step,[status(thm)],[t115542,t41741]) ).
cnf(t115544,plain,
ld(mult(X1,i(X2)),X1) = rd(X1,i(ld(X1,X2))),
inference(step,[status(thm)],[t115543,t16439]) ).
cnf(t56090,plain,
ld(mult(X1,i(X2)),X1) = rd(X1,i(ld(X1,X2))),
inference(orient,[status(thm)],[t115544]) ).
cnf(t56092,plain,
rd(X1,i(ld(X1,mult(X1,X2)))) = ld(rd(rd(X1,X2),X1),X1),
inference(cp,[status(thm)],[t56090,t41985]) ).
cnf(t115545,plain,
rd(X1,i(X2)) = ld(rd(rd(X1,X2),X1),X1),
inference(step,[status(thm)],[t56092,t20]) ).
cnf(t115546,plain,
rd(X1,i(X2)) = mult(rd(X1,rd(X1,X2)),X1),
inference(step,[status(thm)],[t115545,t16007]) ).
cnf(t56254,plain,
mult(rd(X1,rd(X1,X2)),X1) = rd(X1,i(X2)),
inference(orient,[status(thm)],[t115546]) ).
cnf(t56268,plain,
rd(X1,i(ld(X2,X1))) = mult(rd(X1,X2),X1),
inference(cp,[status(thm)],[t56254,t72]) ).
cnf(t56529,plain,
rd(X1,i(ld(X2,X1))) = mult(rd(X1,X2),X1),
inference(orient,[status(thm)],[t56268]) ).
cnf(t56689,plain,
i(mult(X1,i(ld(X2,X1)))) = ld(X1,rd(mult(rd(X1,X2),X1),X1)),
inference(cp,[status(thm)],[t44150,t56529]) ).
cnf(t115566,plain,
i(mult(X1,i(ld(X2,X1)))) = ld(X1,rd(X1,X2)),
inference(step,[status(thm)],[t56689,t16]) ).
cnf(t61005,plain,
i(mult(X1,i(ld(X2,X1)))) = ld(X1,rd(X1,X2)),
inference(orient,[status(thm)],[t115566]) ).
cnf(t115367,plain,
ld(mult(i(X1),X2),i(X1)) = ld(mult(X1,X2),X1),
inference(step,[status(thm)],[t19660,t36644]) ).
cnf(t36645,plain,
ld(mult(i(X1),X2),i(X1)) = ld(mult(X1,X2),X1),
inference(orient,[status(thm)],[t115367]) ).
cnf(t61071,plain,
ld(i(X1),rd(i(X1),mult(i(X1),X2))) = i(mult(i(X1),i(ld(mult(X1,X2),X1)))),
inference(cp,[status(thm)],[t61005,t36645]) ).
cnf(t16552,plain,
mult(X1,mult(mult(rd(i(X1),X2),i(X1)),X1)) = mult(i(ld(i(X1),X2)),X1),
inference(cp,[status(thm)],[t8528,t16439]) ).
cnf(t115161,plain,
mult(X1,rd(rd(rd(i(X1),X2),X1),i(X1))) = mult(i(ld(i(X1),X2)),X1),
inference(step,[status(thm)],[t16552,t3442]) ).
cnf(t115162,plain,
mult(mult(X1,rd(rd(i(X1),X2),X1)),X1) = mult(i(ld(i(X1),X2)),X1),
inference(step,[status(thm)],[t115161,t3711]) ).
cnf(t115163,plain,
ld(i(X1),rd(i(X1),X2)) = mult(i(ld(i(X1),X2)),X1),
inference(step,[status(thm)],[t115162,t8890]) ).
cnf(t20082,plain,
ld(i(X1),rd(i(X1),X2)) = mult(i(ld(i(X1),X2)),X1),
inference(orient,[status(thm)],[t115163]) ).
cnf(t33707,plain,
ld(X1,rd(X1,X2)) = mult(i(ld(i(X1),X2)),X1),
inference(cp,[status(thm)],[t14,t33612]) ).
cnf(t35786,plain,
mult(i(ld(i(X1),X2)),X1) = ld(X1,rd(X1,X2)),
inference(orient,[status(thm)],[t33707]) ).
cnf(t115354,plain,
ld(i(X1),rd(i(X1),X2)) = ld(X1,rd(X1,X2)),
inference(step,[status(thm)],[t20082,t35786]) ).
cnf(t35787,plain,
ld(i(X1),rd(i(X1),X2)) = ld(X1,rd(X1,X2)),
inference(orient,[status(thm)],[t115354]) ).
cnf(t115701,plain,
ld(X1,rd(X1,mult(i(X1),X2))) = i(mult(i(X1),i(ld(mult(X1,X2),X1)))),
inference(step,[status(thm)],[t61071,t35787]) ).
cnf(t3098,plain,
rd(mult(i(X1),X2),i(X1)) = mult(i(X1),mult(X2,X1)),
inference(cp,[status(thm)],[t3082,t71]) ).
cnf(t4569,plain,
rd(mult(i(X1),X2),i(X1)) = mult(i(X1),mult(X2,X1)),
inference(orient,[status(thm)],[t3098]) ).
cnf(t8145,plain,
ld(X1,rd(rd(X2,mult(i(X1),i(X1))),X1)) = rd(rd(mult(i(X1),X2),mult(i(X1),i(X1))),X1),
inference(cp,[status(thm)],[t8133,t7020]) ).
cnf(t114931,plain,
ld(X1,rd(rd(X2,rd(i(X1),X1)),X1)) = rd(rd(mult(i(X1),X2),mult(i(X1),i(X1))),X1),
inference(step,[status(thm)],[t8145,t126]) ).
cnf(t114932,plain,
ld(X1,rd(mult(X2,mult(X1,X1)),X1)) = rd(rd(mult(i(X1),X2),mult(i(X1),i(X1))),X1),
inference(step,[status(thm)],[t114931,t4022]) ).
cnf(t114933,plain,
ld(X1,rd(X2,i(X1))) = rd(rd(mult(i(X1),X2),mult(i(X1),i(X1))),X1),
inference(step,[status(thm)],[t114932,t3578]) ).
cnf(t114934,plain,
mult(ld(X1,X2),X1) = rd(rd(mult(i(X1),X2),mult(i(X1),i(X1))),X1),
inference(step,[status(thm)],[t114933,t4255]) ).
cnf(t114935,plain,
mult(ld(X1,X2),X1) = rd(rd(mult(i(X1),X2),rd(i(X1),X1)),X1),
inference(step,[status(thm)],[t114934,t126]) ).
cnf(t114936,plain,
mult(ld(X1,X2),X1) = rd(mult(mult(i(X1),X2),mult(X1,X1)),X1),
inference(step,[status(thm)],[t114935,t4022]) ).
cnf(t114937,plain,
mult(ld(X1,X2),X1) = rd(mult(i(X1),X2),i(X1)),
inference(step,[status(thm)],[t114936,t3578]) ).
cnf(t114938,plain,
mult(ld(X1,X2),X1) = mult(i(X1),mult(X2,X1)),
inference(step,[status(thm)],[t114937,t4569]) ).
cnf(t8294,plain,
mult(i(X1),mult(X2,X1)) = mult(ld(X1,X2),X1),
inference(orient,[status(thm)],[t114938]) ).
cnf(t114939,plain,
rd(mult(i(X1),X2),i(X1)) = mult(ld(X1,X2),X1),
inference(step,[status(thm)],[t4569,t8294]) ).
cnf(t8295,plain,
rd(mult(i(X1),X2),i(X1)) = mult(ld(X1,X2),X1),
inference(orient,[status(thm)],[t114939]) ).
cnf(t15540,plain,
rd(i(X1),mult(i(X1),X2)) = mult(ld(X1,i(X2)),X1),
inference(cp,[status(thm)],[t15539,t8295]) ).
cnf(t18089,plain,
rd(i(X1),mult(i(X1),X2)) = mult(ld(X1,i(X2)),X1),
inference(orient,[status(thm)],[t15540]) ).
cnf(t34002,plain,
rd(i(i(X1)),mult(i(X1),X2)) = ld(mult(i(X1),i(X1)),mult(ld(X1,i(X2)),X1)),
inference(cp,[status(thm)],[t33943,t18089]) ).
cnf(t115338,plain,
rd(X1,mult(i(X1),X2)) = ld(mult(i(X1),i(X1)),mult(ld(X1,i(X2)),X1)),
inference(step,[status(thm)],[t34002,t71]) ).
cnf(t115339,plain,
rd(X1,mult(i(X1),X2)) = ld(rd(i(X1),X1),mult(ld(X1,i(X2)),X1)),
inference(step,[status(thm)],[t115338,t126]) ).
cnf(t115340,plain,
rd(X1,mult(i(X1),X2)) = mult(mult(X1,X1),mult(ld(X1,i(X2)),X1)),
inference(step,[status(thm)],[t115339,t9476]) ).
cnf(t115341,plain,
rd(X1,mult(i(X1),X2)) = mult(X1,mult(mult(X1,ld(X1,i(X2))),X1)),
inference(step,[status(thm)],[t115340,t854]) ).
cnf(t115342,plain,
rd(X1,mult(i(X1),X2)) = mult(X1,mult(i(X2),X1)),
inference(step,[status(thm)],[t115341,t10]) ).
cnf(t34341,plain,
mult(X1,mult(i(X2),X1)) = rd(X1,mult(i(X1),X2)),
inference(orient,[status(thm)],[t115342]) ).
cnf(t34422,plain,
mult(i(X1),X2) = ld(X2,rd(X2,mult(i(X2),X1))),
inference(cp,[status(thm)],[t20,t34341]) ).
cnf(t54104,plain,
ld(X1,rd(X1,mult(i(X1),X2))) = mult(i(X2),X1),
inference(orient,[status(thm)],[t34422]) ).
cnf(t115702,plain,
mult(i(X2),X1) = i(mult(i(X1),i(ld(mult(X1,X2),X1)))),
inference(step,[status(thm)],[t115701,t54104]) ).
cnf(t56676,plain,
i(ld(X1,X2)) = ld(mult(rd(X2,X1),X2),X2),
inference(cp,[status(thm)],[t73,t56529]) ).
cnf(t58282,plain,
ld(mult(rd(X1,X2),X1),X1) = i(ld(X2,X1)),
inference(orient,[status(thm)],[t56676]) ).
cnf(t58288,plain,
i(ld(mult(X1,X2),X1)) = ld(mult(X1,i(X2)),X1),
inference(cp,[status(thm)],[t58282,t16267]) ).
cnf(t115549,plain,
i(ld(mult(X1,X2),X1)) = rd(X1,i(ld(X1,X2))),
inference(step,[status(thm)],[t58288,t56090]) ).
cnf(t59287,plain,
i(ld(mult(X1,X2),X1)) = rd(X1,i(ld(X1,X2))),
inference(orient,[status(thm)],[t115549]) ).
cnf(t115703,plain,
mult(i(X2),X1) = i(mult(i(X1),rd(X1,i(ld(X1,X2))))),
inference(step,[status(thm)],[t115702,t59287]) ).
cnf(t115704,plain,
mult(i(X2),X1) = i(rd(i(ld(X1,i(ld(X1,X2)))),X1)),
inference(step,[status(thm)],[t115703,t17013]) ).
cnf(t8251,plain,
mult(mult(i(X1),mult(X2,i(X1))),i(X1)) = ld(i(i(X1)),rd(rd(X2,X1),X1)),
inference(cp,[status(thm)],[t8213,t3384]) ).
cnf(t115086,plain,
mult(i(X1),rd(mult(X2,i(X1)),X1)) = ld(i(i(X1)),rd(rd(X2,X1),X1)),
inference(step,[status(thm)],[t8251,t4794]) ).
cnf(t115087,plain,
mult(i(X1),rd(X2,mult(X1,X1))) = ld(i(i(X1)),rd(rd(X2,X1),X1)),
inference(step,[status(thm)],[t115086,t3978]) ).
cnf(t115088,plain,
mult(i(X1),rd(X2,mult(X1,X1))) = ld(X1,rd(rd(X2,X1),X1)),
inference(step,[status(thm)],[t115087,t71]) ).
cnf(t115089,plain,
mult(i(X1),rd(X2,mult(X1,X1))) = rd(rd(ld(X1,X2),X1),X1),
inference(step,[status(thm)],[t115088,t2897]) ).
cnf(t13451,plain,
mult(i(X1),rd(X2,mult(X1,X1))) = rd(rd(ld(X1,X2),X1),X1),
inference(orient,[status(thm)],[t115089]) ).
cnf(t42067,plain,
rd(rd(i(X1),rd(X2,mult(X1,X1))),i(X1)) = mult(i(X1),i(rd(rd(ld(X1,X2),X1),X1))),
inference(cp,[status(thm)],[t41985,t13451]) ).
cnf(t33763,plain,
mult(ld(X1,ld(i(X1),rd(i(X1),X2))),X1) = ld(X1,i(ld(i(i(X1)),X2))),
inference(cp,[status(thm)],[t4255,t33612]) ).
cnf(t115394,plain,
mult(rd(rd(rd(i(X1),X2),X1),i(X1)),X1) = ld(X1,i(ld(i(i(X1)),X2))),
inference(step,[status(thm)],[t33763,t8982]) ).
cnf(t115395,plain,
mult(rd(rd(i(X1),X2),X1),mult(X1,X1)) = ld(X1,i(ld(i(i(X1)),X2))),
inference(step,[status(thm)],[t115394,t3623]) ).
cnf(t115396,plain,
mult(X1,mult(ld(X1,rd(i(X1),X2)),X1)) = ld(X1,i(ld(i(i(X1)),X2))),
inference(step,[status(thm)],[t115395,t2932]) ).
cnf(t115397,plain,
rd(rd(i(X1),X2),i(X1)) = ld(X1,i(ld(i(i(X1)),X2))),
inference(step,[status(thm)],[t115396,t3581]) ).
cnf(t115398,plain,
rd(rd(i(X1),X2),i(X1)) = ld(X1,i(ld(X1,X2))),
inference(step,[status(thm)],[t115397,t71]) ).
cnf(t40285,plain,
rd(rd(i(X1),X2),i(X1)) = ld(X1,i(ld(X1,X2))),
inference(orient,[status(thm)],[t115398]) ).
cnf(t115424,plain,
ld(X1,i(ld(X1,rd(X2,mult(X1,X1))))) = mult(i(X1),i(rd(rd(ld(X1,X2),X1),X1))),
inference(step,[status(thm)],[t42067,t40285]) ).
cnf(t4382,plain,
ld(X1,rd(mult(X2,i(X1)),X1)) = mult(rd(ld(X1,X2),X1),i(X1)),
inference(cp,[status(thm)],[t4378,t3356]) ).
cnf(t114878,plain,
ld(X1,rd(X2,mult(X1,X1))) = mult(rd(ld(X1,X2),X1),i(X1)),
inference(step,[status(thm)],[t4382,t3978]) ).
cnf(t114879,plain,
ld(X1,rd(X2,mult(X1,X1))) = rd(ld(X1,X2),mult(X1,X1)),
inference(step,[status(thm)],[t114878,t3979]) ).
cnf(t5859,plain,
ld(X1,rd(X2,mult(X1,X1))) = rd(ld(X1,X2),mult(X1,X1)),
inference(orient,[status(thm)],[t114879]) ).
cnf(t115425,plain,
ld(X1,i(rd(ld(X1,X2),mult(X1,X1)))) = mult(i(X1),i(rd(rd(ld(X1,X2),X1),X1))),
inference(step,[status(thm)],[t115424,t5859]) ).
cnf(t31041,plain,
ld(i(X1),mult(X2,X2)) = mult(X1,mult(X2,X2)),
inference(cp,[status(thm)],[t31024,t71]) ).
cnf(t31179,plain,
ld(i(X1),mult(X2,X2)) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t31041]) ).
cnf(t31200,plain,
mult(X1,mult(i(X2),i(X2))) = ld(i(X1),rd(i(X2),X2)),
inference(cp,[status(thm)],[t31179,t126]) ).
cnf(t115294,plain,
mult(X1,rd(i(X2),X2)) = ld(i(X1),rd(i(X2),X2)),
inference(step,[status(thm)],[t31200,t126]) ).
cnf(t115295,plain,
rd(X1,mult(X2,X2)) = ld(i(X1),rd(i(X2),X2)),
inference(step,[status(thm)],[t115294,t3981]) ).
cnf(t16574,plain,
ld(i(X1),ld(X2,i(X1))) = i(mult(X1,rd(X2,X1))),
inference(cp,[status(thm)],[t16569,t8692]) ).
cnf(t18552,plain,
ld(i(X1),ld(X2,i(X1))) = i(mult(X1,rd(X2,X1))),
inference(orient,[status(thm)],[t16574]) ).
cnf(t18561,plain,
i(mult(X1,rd(mult(i(X1),mult(X2,X2)),X1))) = ld(i(X1),rd(i(X2),X2)),
inference(cp,[status(thm)],[t18552,t4060]) ).
cnf(t115146,plain,
i(mult(X1,ld(X1,rd(mult(X2,X2),X1)))) = ld(i(X1),rd(i(X2),X2)),
inference(step,[status(thm)],[t18561,t8133]) ).
cnf(t115147,plain,
i(rd(mult(X2,X2),X1)) = ld(i(X1),rd(i(X2),X2)),
inference(step,[status(thm)],[t115146,t10]) ).
cnf(t19027,plain,
ld(i(X1),rd(i(X2),X2)) = i(rd(mult(X2,X2),X1)),
inference(orient,[status(thm)],[t115147]) ).
cnf(t115296,plain,
rd(X1,mult(X2,X2)) = i(rd(mult(X2,X2),X1)),
inference(step,[status(thm)],[t115295,t19027]) ).
cnf(t31518,plain,
i(rd(mult(X1,X1),X2)) = rd(X2,mult(X1,X1)),
inference(orient,[status(thm)],[t115296]) ).
cnf(t31527,plain,
rd(mult(rd(mult(X1,X1),X2),mult(X1,X1)),mult(X1,X1)) = i(rd(X2,mult(X1,X1))),
inference(cp,[status(thm)],[t31518,t15906]) ).
cnf(t115315,plain,
rd(mult(X1,X1),X2) = i(rd(X2,mult(X1,X1))),
inference(step,[status(thm)],[t31527,t16]) ).
cnf(t32225,plain,
i(rd(X1,mult(X2,X2))) = rd(mult(X2,X2),X1),
inference(orient,[status(thm)],[t115315]) ).
cnf(t115426,plain,
ld(X1,rd(mult(X1,X1),ld(X1,X2))) = mult(i(X1),i(rd(rd(ld(X1,X2),X1),X1))),
inference(step,[status(thm)],[t115425,t32225]) ).
cnf(t114994,plain,
ld(X1,mult(mult(X1,X1),X2)) = ld(i(X1),X2),
inference(step,[status(thm)],[t2611,t8887]) ).
cnf(t8888,plain,
ld(X1,mult(mult(X1,X1),X2)) = ld(i(X1),X2),
inference(orient,[status(thm)],[t114994]) ).
cnf(t31484,plain,
ld(i(X1),i(X2)) = ld(X1,rd(mult(X1,X1),X2)),
inference(cp,[status(thm)],[t8888,t31360]) ).
cnf(t33200,plain,
ld(X1,rd(mult(X1,X1),X2)) = ld(i(X1),i(X2)),
inference(orient,[status(thm)],[t31484]) ).
cnf(t115427,plain,
ld(i(X1),i(ld(X1,X2))) = mult(i(X1),i(rd(rd(ld(X1,X2),X1),X1))),
inference(step,[status(thm)],[t115426,t33200]) ).
cnf(t115004,plain,
ld(i(X1),ld(X1,X2)) = rd(rd(X2,X1),i(X1)),
inference(step,[status(thm)],[t1370,t8982]) ).
cnf(t8983,plain,
ld(i(X1),ld(X1,X2)) = rd(rd(X2,X1),i(X1)),
inference(orient,[status(thm)],[t115004]) ).
cnf(t16512,plain,
rd(rd(mult(rd(X1,X2),X1),X1),i(X1)) = ld(i(X1),i(ld(X1,X2))),
inference(cp,[status(thm)],[t8983,t16439]) ).
cnf(t115140,plain,
rd(rd(X1,X2),i(X1)) = ld(i(X1),i(ld(X1,X2))),
inference(step,[status(thm)],[t16512,t16]) ).
cnf(t18347,plain,
ld(i(X1),i(ld(X1,X2))) = rd(rd(X1,X2),i(X1)),
inference(orient,[status(thm)],[t115140]) ).
cnf(t115428,plain,
rd(rd(X1,X2),i(X1)) = mult(i(X1),i(rd(rd(ld(X1,X2),X1),X1))),
inference(step,[status(thm)],[t115427,t18347]) ).
cnf(t115429,plain,
rd(rd(X1,X2),i(X1)) = ld(mult(X1,rd(ld(X1,X2),X1)),X1),
inference(step,[status(thm)],[t115428,t36644]) ).
cnf(t115430,plain,
rd(rd(X1,X2),i(X1)) = ld(mult(X2,i(X1)),X1),
inference(step,[status(thm)],[t115429,t3130]) ).
cnf(t43099,plain,
ld(mult(X1,i(X2)),X2) = rd(rd(X2,X1),i(X2)),
inference(orient,[status(thm)],[t115430]) ).
cnf(t43126,plain,
rd(rd(X1,rd(X2,mult(i(X1),i(X1)))),i(X1)) = ld(mult(X2,i(i(X1))),X1),
inference(cp,[status(thm)],[t43099,t3923]) ).
cnf(t115435,plain,
rd(rd(X1,rd(X2,rd(i(X1),X1))),i(X1)) = ld(mult(X2,i(i(X1))),X1),
inference(step,[status(thm)],[t43126,t126]) ).
cnf(t115436,plain,
rd(rd(X1,mult(X2,mult(X1,X1))),i(X1)) = ld(mult(X2,i(i(X1))),X1),
inference(step,[status(thm)],[t115435,t4022]) ).
cnf(t37864,plain,
ld(rd(X1,X2),i(X1)) = rd(X2,mult(X1,X1)),
inference(cp,[status(thm)],[t37767,t73]) ).
cnf(t37942,plain,
ld(rd(X1,X2),i(X1)) = rd(X2,mult(X1,X1)),
inference(orient,[status(thm)],[t37864]) ).
cnf(t38052,plain,
rd(X1,mult(i(X2),i(X2))) = ld(rd(i(X2),X1),X2),
inference(cp,[status(thm)],[t37942,t71]) ).
cnf(t115385,plain,
rd(X1,rd(i(X2),X2)) = ld(rd(i(X2),X1),X2),
inference(step,[status(thm)],[t38052,t126]) ).
cnf(t115386,plain,
mult(X1,mult(X2,X2)) = ld(rd(i(X2),X1),X2),
inference(step,[status(thm)],[t115385,t4022]) ).
cnf(t38110,plain,
ld(rd(i(X1),X2),X1) = mult(X2,mult(X1,X1)),
inference(orient,[status(thm)],[t115386]) ).
cnf(t38155,plain,
rd(i(X1),X2) = rd(X1,mult(X2,mult(X1,X1))),
inference(cp,[status(thm)],[t72,t38110]) ).
cnf(t39186,plain,
rd(X1,mult(X2,mult(X1,X1))) = rd(i(X1),X2),
inference(orient,[status(thm)],[t38155]) ).
cnf(t115437,plain,
rd(rd(i(X1),X2),i(X1)) = ld(mult(X2,i(i(X1))),X1),
inference(step,[status(thm)],[t115436,t39186]) ).
cnf(t115438,plain,
ld(X1,i(ld(X1,X2))) = ld(mult(X2,i(i(X1))),X1),
inference(step,[status(thm)],[t115437,t40285]) ).
cnf(t115439,plain,
ld(X1,i(ld(X1,X2))) = ld(mult(X2,X1),X1),
inference(step,[status(thm)],[t115438,t71]) ).
cnf(t43232,plain,
ld(X1,i(ld(X1,X2))) = ld(mult(X2,X1),X1),
inference(orient,[status(thm)],[t115439]) ).
cnf(t115705,plain,
mult(i(X2),X1) = i(rd(i(ld(mult(X2,X1),X1)),X1)),
inference(step,[status(thm)],[t115704,t43232]) ).
cnf(t58289,plain,
i(ld(mult(X1,X2),X2)) = ld(ld(X1,X2),X2),
inference(cp,[status(thm)],[t58282,t16097]) ).
cnf(t58477,plain,
i(ld(mult(X1,X2),X2)) = ld(ld(X1,X2),X2),
inference(orient,[status(thm)],[t58289]) ).
cnf(t115706,plain,
mult(i(X2),X1) = i(rd(ld(ld(X2,X1),X1),X1)),
inference(step,[status(thm)],[t115705,t58477]) ).
cnf(t115707,plain,
mult(i(X2),X1) = i(rd(X1,mult(ld(X2,X1),X1))),
inference(step,[status(thm)],[t115706,t15776]) ).
cnf(t56386,plain,
rd(X1,rd(X1,X2)) = rd(rd(X1,i(X2)),X1),
inference(cp,[status(thm)],[t16,t56254]) ).
cnf(t56773,plain,
rd(rd(X1,i(X2)),X1) = rd(X1,rd(X1,X2)),
inference(orient,[status(thm)],[t56386]) ).
cnf(t115547,plain,
i(rd(X1,rd(X1,X2))) = rd(i(rd(X2,X1)),X1),
inference(step,[status(thm)],[t55548,t56773]) ).
cnf(t56957,plain,
i(rd(X1,rd(X1,X2))) = rd(i(rd(X2,X1)),X1),
inference(rw,[status(thm)],[t115547]) ).
cnf(t57516,plain,
i(rd(X1,rd(X1,X2))) = rd(i(rd(X2,X1)),X1),
inference(orient,[status(thm)],[t56957]) ).
cnf(t57655,plain,
rd(X1,rd(X1,X2)) = i(rd(i(rd(X2,X1)),X1)),
inference(cp,[status(thm)],[t71,t57516]) ).
cnf(t61627,plain,
i(rd(i(rd(X1,X2)),X2)) = rd(X2,rd(X2,X1)),
inference(orient,[status(thm)],[t57655]) ).
cnf(t61741,plain,
rd(X1,rd(X1,mult(X2,X1))) = i(rd(i(X2),X1)),
inference(cp,[status(thm)],[t61627,t16]) ).
cnf(t65177,plain,
rd(X1,rd(X1,mult(X2,X1))) = i(rd(i(X2),X1)),
inference(orient,[status(thm)],[t61741]) ).
cnf(t56430,plain,
ld(X1,ld(rd(X1,rd(X1,X2)),X1)) = i(ld(X1,rd(X1,i(X2)))),
inference(cp,[status(thm)],[t16569,t56254]) ).
cnf(t115564,plain,
ld(X1,rd(X1,X2)) = i(ld(X1,rd(X1,i(X2)))),
inference(step,[status(thm)],[t56430,t73]) ).
cnf(t56431,plain,
i(ld(X1,rd(X1,X2))) = ld(X1,rd(X1,i(X2))),
inference(cp,[status(thm)],[t16439,t56254]) ).
cnf(t57120,plain,
i(ld(X1,rd(X1,X2))) = ld(X1,rd(X1,i(X2))),
inference(orient,[status(thm)],[t56431]) ).
cnf(t43344,plain,
i(ld(X1,X2)) = mult(X1,ld(mult(X2,X1),X1)),
inference(cp,[status(thm)],[t10,t43232]) ).
cnf(t46965,plain,
mult(X1,ld(mult(X2,X1),X1)) = i(ld(X1,X2)),
inference(orient,[status(thm)],[t43344]) ).
cnf(t58424,plain,
i(ld(X1,rd(X1,X2))) = mult(X1,i(ld(X2,X1))),
inference(cp,[status(thm)],[t46965,t58282]) ).
cnf(t115550,plain,
ld(X1,rd(X1,i(X2))) = mult(X1,i(ld(X2,X1))),
inference(step,[status(thm)],[t58424,t57120]) ).
cnf(t59682,plain,
ld(X1,rd(X1,i(X2))) = mult(X1,i(ld(X2,X1))),
inference(orient,[status(thm)],[t115550]) ).
cnf(t115551,plain,
i(ld(X1,rd(X1,X2))) = mult(X1,i(ld(X2,X1))),
inference(step,[status(thm)],[t57120,t59682]) ).
cnf(t59683,plain,
i(ld(X1,rd(X1,X2))) = mult(X1,i(ld(X2,X1))),
inference(orient,[status(thm)],[t115551]) ).
cnf(t115565,plain,
ld(X1,rd(X1,X2)) = mult(X1,i(ld(i(X2),X1))),
inference(step,[status(thm)],[t115564,t59683]) ).
cnf(t60706,plain,
mult(X1,i(ld(i(X2),X1))) = ld(X1,rd(X1,X2)),
inference(orient,[status(thm)],[t115565]) ).
cnf(t60833,plain,
i(ld(i(X1),X2)) = ld(X2,ld(X2,rd(X2,X1))),
inference(cp,[status(thm)],[t20,t60706]) ).
cnf(t64718,plain,
ld(X1,ld(X1,rd(X1,X2))) = i(ld(i(X2),X1)),
inference(orient,[status(thm)],[t60833]) ).
cnf(t64740,plain,
i(ld(i(i(ld(X1,X2))),X2)) = ld(X2,ld(X2,mult(rd(X2,X1),X2))),
inference(cp,[status(thm)],[t64718,t56529]) ).
cnf(t115575,plain,
i(ld(ld(X1,X2),X2)) = ld(X2,ld(X2,mult(rd(X2,X1),X2))),
inference(step,[status(thm)],[t64740,t71]) ).
cnf(t58303,plain,
i(ld(ld(X1,X2),X2)) = ld(mult(X1,X2),X2),
inference(cp,[status(thm)],[t58282,t72]) ).
cnf(t58883,plain,
i(ld(ld(X1,X2),X2)) = ld(mult(X1,X2),X2),
inference(orient,[status(thm)],[t58303]) ).
cnf(t115576,plain,
ld(mult(X1,X2),X2) = ld(X2,ld(X2,mult(rd(X2,X1),X2))),
inference(step,[status(thm)],[t115575,t58883]) ).
cnf(t4260,plain,
mult(ld(X1,ld(X1,X2)),X1) = ld(X1,ld(X1,mult(X2,X1))),
inference(cp,[status(thm)],[t4255,t3678]) ).
cnf(t5807,plain,
ld(X1,ld(X1,mult(X2,X1))) = mult(ld(X1,ld(X1,X2)),X1),
inference(orient,[status(thm)],[t4260]) ).
cnf(t115577,plain,
ld(mult(X1,X2),X2) = mult(ld(X2,ld(X2,rd(X2,X1))),X2),
inference(step,[status(thm)],[t115576,t5807]) ).
cnf(t115578,plain,
ld(mult(X1,X2),X2) = mult(i(ld(i(X1),X2)),X2),
inference(step,[status(thm)],[t115577,t64718]) ).
cnf(t65573,plain,
mult(i(ld(i(X1),X2)),X2) = ld(mult(X1,X2),X2),
inference(orient,[status(thm)],[t115578]) ).
cnf(t65712,plain,
i(rd(i(i(ld(i(X1),X2))),X2)) = rd(X2,rd(X2,ld(mult(X1,X2),X2))),
inference(cp,[status(thm)],[t65177,t65573]) ).
cnf(t115580,plain,
i(rd(ld(i(X1),X2),X2)) = rd(X2,rd(X2,ld(mult(X1,X2),X2))),
inference(step,[status(thm)],[t65712,t71]) ).
cnf(t115581,plain,
i(rd(X2,mult(i(X1),X2))) = rd(X2,rd(X2,ld(mult(X1,X2),X2))),
inference(step,[status(thm)],[t115580,t15776]) ).
cnf(t115582,plain,
i(rd(X2,mult(i(X1),X2))) = rd(X2,mult(X1,X2)),
inference(step,[status(thm)],[t115581,t72]) ).
cnf(t67308,plain,
i(rd(X1,mult(i(X2),X1))) = rd(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t115582]) ).
cnf(t67405,plain,
rd(X1,mult(i(X2),X1)) = i(rd(X1,mult(X2,X1))),
inference(cp,[status(thm)],[t67308,t71]) ).
cnf(t67698,plain,
i(rd(X1,mult(X2,X1))) = rd(X1,mult(i(X2),X1)),
inference(orient,[status(thm)],[t67405]) ).
cnf(t115708,plain,
mult(i(X2),X1) = rd(X1,mult(i(ld(X2,X1)),X1)),
inference(step,[status(thm)],[t115707,t67698]) ).
cnf(t85483,plain,
rd(X1,mult(i(ld(X2,X1)),X1)) = mult(i(X2),X1),
inference(orient,[status(thm)],[t115708]) ).
cnf(t9122,plain,
i(X1) = rd(mult(X1,X2),mult(mult(X1,X1),X2)),
inference(cp,[status(thm)],[t16,t9083]) ).
cnf(t11099,plain,
rd(mult(X1,X2),mult(mult(X1,X1),X2)) = i(X1),
inference(orient,[status(thm)],[t9122]) ).
cnf(t47,plain,
mult(mult(X1,X2),mult(X2,mult(ld(X2,X3),X2))) = mult(mult(X1,mult(X2,X3)),X2),
inference(cp,[status(thm)],[t42,t10]) ).
cnf(t115645,plain,
mult(mult(X1,X2),rd(X3,i(X2))) = mult(mult(X1,mult(X2,X3)),X2),
inference(step,[status(thm)],[t47,t3581]) ).
cnf(t77361,plain,
mult(mult(X1,X2),rd(X3,i(X2))) = mult(mult(X1,mult(X2,X3)),X2),
inference(orient,[status(thm)],[t115645]) ).
cnf(t77518,plain,
mult(mult(X1,mult(X2,mult(i(X2),mult(X3,i(X2))))),X2) = mult(mult(X1,X2),ld(i(i(X2)),X3)),
inference(cp,[status(thm)],[t77361,t8887]) ).
cnf(t8755,plain,
mult(i(X1),mult(X1,X2)) = rd(rd(X2,i(X1)),X1),
inference(cp,[status(thm)],[t8749,t3579]) ).
cnf(t114985,plain,
mult(X1,mult(i(X1),X2)) = rd(rd(X2,i(X1)),X1),
inference(step,[status(thm)],[t8755,t966]) ).
cnf(t114986,plain,
mult(X1,mult(i(X1),X2)) = rd(rd(X2,X1),i(X1)),
inference(step,[status(thm)],[t114985,t1463]) ).
cnf(t8835,plain,
mult(X1,mult(i(X1),X2)) = rd(rd(X2,X1),i(X1)),
inference(orient,[status(thm)],[t114986]) ).
cnf(t115904,plain,
mult(mult(X1,rd(rd(mult(X3,i(X2)),X2),i(X2))),X2) = mult(mult(X1,X2),ld(i(i(X2)),X3)),
inference(step,[status(thm)],[t77518,t8835]) ).
cnf(t115905,plain,
mult(mult(X1,rd(rd(X3,mult(X2,X2)),i(X2))),X2) = mult(mult(X1,X2),ld(i(i(X2)),X3)),
inference(step,[status(thm)],[t115904,t3978]) ).
cnf(t115906,plain,
mult(mult(X1,rd(X3,X2)),X2) = mult(mult(X1,X2),ld(i(i(X2)),X3)),
inference(step,[status(thm)],[t115905,t4276]) ).
cnf(t115907,plain,
mult(mult(X1,rd(X3,X2)),X2) = mult(mult(X1,X2),ld(X2,X3)),
inference(step,[status(thm)],[t115906,t71]) ).
cnf(t112632,plain,
mult(mult(X1,rd(X2,X3)),X3) = mult(mult(X1,X3),ld(X3,X2)),
inference(orient,[status(thm)],[t115907]) ).
cnf(t112959,plain,
i(rd(X1,X2)) = rd(mult(rd(X1,X2),X2),mult(mult(rd(X1,X2),X2),ld(X2,X1))),
inference(cp,[status(thm)],[t11099,t112632]) ).
cnf(t115910,plain,
i(rd(X1,X2)) = rd(X1,mult(mult(rd(X1,X2),X2),ld(X2,X1))),
inference(step,[status(thm)],[t112959,t14]) ).
cnf(t115911,plain,
i(rd(X1,X2)) = rd(X1,mult(X1,ld(X2,X1))),
inference(step,[status(thm)],[t115910,t14]) ).
cnf(t41565,plain,
rd(i(X1),ld(X1,X2)) = ld(X1,mult(i(X2),X1)),
inference(cp,[status(thm)],[t41534,t10]) ).
cnf(t42389,plain,
ld(X1,mult(i(X2),X1)) = rd(i(X1),ld(X1,X2)),
inference(orient,[status(thm)],[t41565]) ).
cnf(t42530,plain,
mult(X1,mult(mult(i(X2),i(X1)),X1)) = mult(rd(i(i(X1)),ld(i(X1),X2)),X1),
inference(cp,[status(thm)],[t8528,t42389]) ).
cnf(t115482,plain,
mult(X1,rd(rd(i(X2),X1),i(X1))) = mult(rd(i(i(X1)),ld(i(X1),X2)),X1),
inference(step,[status(thm)],[t42530,t3442]) ).
cnf(t115483,plain,
mult(mult(X1,rd(i(X2),X1)),X1) = mult(rd(i(i(X1)),ld(i(X1),X2)),X1),
inference(step,[status(thm)],[t115482,t3711]) ).
cnf(t115484,plain,
ld(i(X1),i(X2)) = mult(rd(i(i(X1)),ld(i(X1),X2)),X1),
inference(step,[status(thm)],[t115483,t8890]) ).
cnf(t115485,plain,
ld(i(X1),i(X2)) = mult(rd(X1,ld(i(X1),X2)),X1),
inference(step,[status(thm)],[t115484,t71]) ).
cnf(t16031,plain,
mult(rd(X1,ld(i(X1),X2)),X1) = ld(mult(X1,rd(X2,X1)),X1),
inference(cp,[status(thm)],[t16007,t8691]) ).
cnf(t24354,plain,
mult(rd(X1,ld(i(X1),X2)),X1) = ld(mult(X1,rd(X2,X1)),X1),
inference(orient,[status(thm)],[t16031]) ).
cnf(t115486,plain,
ld(i(X1),i(X2)) = ld(mult(X1,rd(X2,X1)),X1),
inference(step,[status(thm)],[t115485,t24354]) ).
cnf(t47845,plain,
ld(mult(X1,rd(X2,X1)),X1) = ld(i(X1),i(X2)),
inference(orient,[status(thm)],[t115486]) ).
cnf(t59288,plain,
rd(X1,i(ld(X1,rd(X2,X1)))) = i(ld(i(X1),i(X2))),
inference(cp,[status(thm)],[t59287,t47845]) ).
cnf(t115614,plain,
rd(X1,mult(X1,ld(X2,X1))) = i(ld(i(X1),i(X2))),
inference(step,[status(thm)],[t59288,t44679]) ).
cnf(t72338,plain,
rd(X1,mult(X1,ld(X2,X1))) = i(ld(i(X1),i(X2))),
inference(orient,[status(thm)],[t115614]) ).
cnf(t115912,plain,
i(rd(X1,X2)) = i(ld(i(X1),i(X2))),
inference(step,[status(thm)],[t115911,t72338]) ).
cnf(t113078,plain,
i(ld(i(X1),i(X2))) = i(rd(X1,X2)),
inference(orient,[status(thm)],[t115912]) ).
cnf(t113598,plain,
mult(i(i(X1)),i(X2)) = rd(i(X2),mult(i(rd(X1,X2)),i(X2))),
inference(cp,[status(thm)],[t85483,t113078]) ).
cnf(t115915,plain,
mult(X1,i(X2)) = rd(i(X2),mult(i(rd(X1,X2)),i(X2))),
inference(step,[status(thm)],[t113598,t71]) ).
cnf(t115916,plain,
mult(X1,i(X2)) = rd(X2,mult(i(rd(X1,X2)),X2)),
inference(step,[status(thm)],[t115915,t39634]) ).
cnf(t61637,plain,
rd(X1,rd(X1,i(mult(X2,X1)))) = i(rd(mult(rd(X1,i(X2)),X1),X1)),
inference(cp,[status(thm)],[t61627,t40731]) ).
cnf(t56433,plain,
rd(rd(X1,X2),X1) = rd(X1,rd(X1,i(X2))),
inference(cp,[status(thm)],[t15906,t56254]) ).
cnf(t56958,plain,
rd(X1,rd(X1,i(X2))) = rd(rd(X1,X2),X1),
inference(orient,[status(thm)],[t56433]) ).
cnf(t115573,plain,
rd(rd(X1,mult(X2,X1)),X1) = i(rd(mult(rd(X1,i(X2)),X1),X1)),
inference(step,[status(thm)],[t61637,t56958]) ).
cnf(t115574,plain,
rd(rd(X1,mult(X2,X1)),X1) = i(rd(X1,i(X2))),
inference(step,[status(thm)],[t115573,t16]) ).
cnf(t64948,plain,
rd(rd(X1,mult(X2,X1)),X1) = i(rd(X1,i(X2))),
inference(orient,[status(thm)],[t115574]) ).
cnf(t65072,plain,
rd(X1,mult(X2,X1)) = mult(i(rd(X1,i(X2))),X1),
inference(cp,[status(thm)],[t14,t64948]) ).
cnf(t66053,plain,
mult(i(rd(X1,i(X2))),X1) = rd(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t65072]) ).
cnf(t66158,plain,
rd(X1,mult(i(X2),X1)) = mult(i(rd(X1,X2)),X1),
inference(cp,[status(thm)],[t66053,t71]) ).
cnf(t66350,plain,
mult(i(rd(X1,X2)),X1) = rd(X1,mult(i(X2),X1)),
inference(orient,[status(thm)],[t66158]) ).
cnf(t57526,plain,
rd(i(rd(mult(rd(X1,X2),X1),X1)),X1) = i(rd(X1,rd(X2,X1))),
inference(cp,[status(thm)],[t57516,t15906]) ).
cnf(t115548,plain,
rd(i(rd(X1,X2)),X1) = i(rd(X1,rd(X2,X1))),
inference(step,[status(thm)],[t57526,t16]) ).
cnf(t57902,plain,
i(rd(X1,rd(X2,X1))) = rd(i(rd(X1,X2)),X1),
inference(orient,[status(thm)],[t115548]) ).
cnf(t66353,plain,
rd(X1,mult(i(rd(X2,X1)),X1)) = mult(rd(i(rd(X1,X2)),X1),X1),
inference(cp,[status(thm)],[t66350,t57902]) ).
cnf(t115709,plain,
rd(X1,mult(i(rd(X2,X1)),X1)) = i(rd(X1,X2)),
inference(step,[status(thm)],[t66353,t14]) ).
cnf(t85715,plain,
rd(X1,mult(i(rd(X2,X1)),X1)) = i(rd(X1,X2)),
inference(orient,[status(thm)],[t115709]) ).
cnf(t115917,plain,
mult(X1,i(X2)) = i(rd(X2,X1)),
inference(step,[status(thm)],[t115916,t85715]) ).
cnf(t113669,plain,
i(rd(X1,X2)) = mult(X2,i(X1)),
inference(orient,[status(thm)],[t115917]) ).
cnf(t115948,plain,
rd(X1,rd(X1,mult(X2,X1))) = mult(X1,i(i(X2))),
inference(step,[status(thm)],[t65177,t113669]) ).
cnf(t115949,plain,
rd(X1,rd(X1,mult(X2,X1))) = mult(X1,X2),
inference(step,[status(thm)],[t115948,t71]) ).
cnf(t113690,plain,
rd(X1,rd(X1,mult(X2,X1))) = mult(X1,X2),
inference(orient,[status(thm)],[t115949]) ).
cnf(t113719,plain,
mult(rd(X1,mult(X2,X1)),i(X1)) = i(mult(X1,X2)),
inference(cp,[status(thm)],[t113669,t113690]) ).
cnf(t115383,plain,
mult(rd(X1,mult(X2,X1)),i(X1)) = ld(X2,i(X1)),
inference(step,[status(thm)],[t24164,t37767]) ).
cnf(t37768,plain,
mult(rd(X1,mult(X2,X1)),i(X1)) = ld(X2,i(X1)),
inference(orient,[status(thm)],[t115383]) ).
cnf(t116121,plain,
ld(X2,i(X1)) = i(mult(X1,X2)),
inference(step,[status(thm)],[t113719,t37768]) ).
cnf(t114195,plain,
i(mult(X1,X2)) = ld(X2,i(X1)),
inference(orient,[status(thm)],[t116121]) ).
cnf(goal_0,negated_conjecture,
mult(a,i(mult(b,a))) != i(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
mult(a,ld(a,i(b))) != i(b),
inference(rw,[status(thm)],[goal_0,t114195]) ).
cnf(g0_1,plain,
i(b) != i(b),
inference(rw,[status(thm)],[g0_0,t10]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP701-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 15:50:37 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 32.08/5.07 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 32.08/5.07 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------