The case-study can be tested by executing tamarin prover with each of the files.

When using the recommended installation the following lines should work (one at a time).

~/.local/bin/tamarin-prover not_loading.spthy
~/.local/bin/tamarin-prover with_sorts_loading.spthy