Cool. How are you generating the formulas? Iterating through each input possibility?
The 8th bit "explosion" is probably due to triggering the use of a 2nd path of 32bit addition.
The formulas for 32bit add (64 in, 32 out) get very large very quickly (
http://jlcooke.ca/btc/sha256_logred_formulas.html) due to carry bits. Result r_31 depends on a_31 .. a_0 and b_31 .. b_0.
To generate formulas, I do an in-order walk of the tree, and simplify at each level going up... although I'm not sure I fully understand your quesiton.
Quick update, I've been trying out Maple as a potential replacement for Mathematica. BooleanSimplify chokes on even 8 bits, but doing simplify( (arithmetic expression mod 2, {a*a-a, b*b-b, c*c-c, ....}) does way better. Maple seems to evaluate these expressions an order of magnitude faster than mathematica, although the resulting equations aren't as compact. It also consumed a modest 300 megs of memory for 8 bits. Still learning the maple syntax so things might improve.