Making this a community wiki. Here are a few that come to mind, some more obvious than others, with a theme, and not described in detail. May add more later.

1. A simply typed $\lambda$-term whose computation in the $\lambda\sigma$-calculus does not always terminate. [[Mellies (1995)](https://link.springer.com/chapter/10.1007/BFb0014062)]

2. $\lambda U$ and $\lambda U^-$ are non-normalizing PTSs which are functional and non-dependent. [Girard (1972)]

3. The non-functional PTS with sorts $\{1, 2, 3\}$ and axioms $1 : 2$ and $1 : 3$ does not satisfy type correctness.

3. The PTS with sorts $\mathbb N$, no rules, and axioms
$$
\mathcal A = \{(i: n) : \text{the $i$th Turing machine halts on $i$ in $n$ steps}\}
$$
is strongly normalizing and functional but has undecidable type checking [[Pollack, 1992](https://wonks.github.io/type-theory-reading-group/papers/proc92.pdf#page=274)]. But any functional PTS with finite sorts has decidable type checking [[Jutting, 1993](https://www.sciencedirect.com/science/article/pii/S0890540183710382)].

4. Impredicative type theory with proof-irrelevant propositional equality is not weakly normalizing. [Abel, Coquand (2020)]

5. Tight reduction (i.e., $\beta$-reduction on terms with type-annotation application and abstraction) does not satisfy CR on non-well-typed terms.

6. Cyclic F (i.e., F with the additional axiom $\square : *$) is strongly normalizing and has cyclic axioms.