System U/UU: sort relations for readability

Also document convention (inferred from older instances).
Fix syntax for relations in output

A PTS relation (s1, s2) should not be denoted as s1: s2, which suggests
a PTS axiom. This was discovered when it tripped Klaus.
Add negative example

From tsr-experiments. TODO: automate testing that this does not
typecheck.
Add negative example triggering "Internal error"

Suggested by Tillmann when discussing #108.