∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (assignment : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  c.reduce assignment = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth →
    Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) assignment