(sorts t1, t2, t3, t4, u1, u2
sorts t2, t4 < u1; t3, t4 < u2
op a : t2
op a : t3
op a : t4,
[def a])
3.10-3.11: ### Hint: redeclared sort 't3'
5.6-5.7: ### Hint: redeclared sort 't4'
5.10-5.11: ### Hint: redeclared sort 't2'