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)]

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 unicity.

4. 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]. But any functional PTS with finite sorts has decidable type checking [Jutting, 1993].

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

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

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

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)]

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 unicity.

4. 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]. But any functional PTS with finite sorts has decidable type checking [Jutting, 1993].

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

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

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

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)]

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.

4. 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]. But any functional PTS with finite sorts has decidable type checking [Jutting, 1993].

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

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

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

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)]

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 unicity.

4. 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]. But any functional PTS with finite sorts has decidable type checking [Jutting, 1993].

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

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

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