  We characterize all common notions of behavioral equivalence by one
6-dimensional energy game, where energies bound capabilities of an attacker
trying to tell processes apart. The defender-winning initial credits
exhaustively determine which preorders and equivalences from the (strong)
linear-time--branching-time spectrum relate processes.
  The time complexity is exponential, which is optimal due to trace equivalence
being covered. This complexity improves drastically on our recent approach for
deciding groups of equivalences where exponential sets of distinguishing HML
formulas are constructed on top of a super-exponential reachability game. In
experiments using the VLTS benchmarks, the algorithm performs on par with the
best similarity algorithm.
