SMT formula very hard to solve, even though its size is rather small

pls.py

#!/usr/bin/env python3
import z3

a = z3.BitVec("a", 8)
b = z3.BitVec("b", 8)
c = z3.BitVec("c", 8)
d = z3.BitVec("d", 8)
e = z3.BitVec("e", 8)

solver = z3.SolverFor("QF_BV")

#e1 = -(~a)*~(e*d)
#e2 = ~a + ~a*e*d

e1 = (c + d*d - -d)*(c - b ^ d)*(d ^ c)
e2 = ((d ^ c)*(d ^ c - b) & (d + ~d ^ d + c + d*d))* (d + c + d*d & ~((d ^ c)*(d ^ c - b))) + (d + c + d*d & (d ^ c)*(d ^ c - b))* ((d ^ c)*(d ^ c - b) | d + c + d*d)

expr = (e1 != e2)
print(expr.sexpr())

print(solver.check(expr))

'''
(set-logic QF_BV)

; run with: z3 --smt2 pls.smt2

; -(~a)*~(e*d) 
; ~a + ~a*e*d


(declare-fun a () (_ BitVec 8))
(declare-fun b () (_ BitVec 8))
(declare-fun c () (_ BitVec 8))
(declare-fun d () (_ BitVec 8))
(declare-fun e () (_ BitVec 8))


;(assert (not (=
;(assert (distinct
;  (bvmul (bvneg (bvnot a)) (bvnot (bvmul e d)))
;  (bvadd (bvnot a) (bvmul (bvnot a) e d))
;))
;)

(assert
(let ((a!1 (bvmul (bvsub (bvadd c (bvmul d d)) (bvneg d))
                  (bvxor (bvsub c b) d)
                  (bvxor d c)))
      (a!2 (bvand (bvmul (bvxor d c) (bvxor d (bvsub c b)))
                  (bvxor (bvadd d (bvnot d)) (bvadd d c (bvmul d d)))))
      (a!3 (bvnot (bvmul (bvxor d c) (bvxor d (bvsub c b)))))
      (a!5 (bvand (bvadd d c (bvmul d d))
                  (bvmul (bvxor d c) (bvxor d (bvsub c b)))))
      (a!6 (bvor (bvmul (bvxor d c) (bvxor d (bvsub c b)))
                 (bvadd d c (bvmul d d)))))
(let ((a!4 (bvmul a!2 (bvand (bvadd d c (bvmul d d)) a!3))))
  (distinct a!1 (bvadd a!4 (bvmul a!5 a!6)))))
)


(check-sat)
'''