I am learning TLAPS proofs by following the "official" examples released with TLAPS.
I notice that sometimes we need to explicitly specify the backend provers,
like "BY IsaM("force")", "BY Z3", "BY SMT", and so on.
But, I have no idea which one/ones to choose (and in which situations).
What are the strengths/weaknesses of these backend provers?
Are there any instructions on when and how to explicitly specify some (which?) backend provers?