CONSTANTS
  Leaves <- MCLeaves
  LeafDocs <- MCLeafDocs
  Score <- MCScore
  PLK <- MCPLK1
  K = 3
  Filtered = FALSE
  TimeoutOn = TRUE
SPECIFICATION Spec
INVARIANT Sound
INVARIANT AllExactTopK
INVARIANT NoPhase1Loss