Interface ConditionInsight

Every atom of ConditionInsight.frontier in source order — the flat unmet frontier. Empty when the condition is satisfied. Which atoms are single-fix sufficient is each entry's AtomInsight.pivotal.

The unmet frontier as a clause tree — what still stands between the current state and satisfaction: an unsatisfied all keeps its unmet members, a failing any keeps every member (any one of those suffices). Satisfied subtrees are pruned and a group left with one member collapses to it, so the tree's connectives stay truthful after pruning. Absent when the condition is satisfied.

The condition's verdict, exactly as the engine computes it.