Help: satisfy_all on CNF significantly slower than DNF

[Cerebus]

I know I'm probably missing something simple and stupid, but here's the stage:

• Expression is an alternating nest:

Or(
  And(
    Or(
      And(var, var, ...),
      And(var, var, ...),
      ...
    ),
    Or(And(...),...),
    ...
  ),
  And(Or(And(...),...), ...),
  ...
)

• list(x.satisfy_all()) on the un-normalized expression as the baseline
• list(x.to_dnf().satisfy_all()) runs ~20x faster
• list(x.to_cnf().satisfy_all()) runs >100x slower

The times for to_cnf() and to_dnf() are fine, in that this isn't the source of the time difference.

The CNF expression should be foisted off on PicoSAT, and since that's in C I expected that to be a lot faster. What am I missing?