(sorts a, b, c, d, x

sorts x < a; a < d

op o : a

op o : a -> b

op o2 : a ->? b

pred p : a

pred p : b

pred q : a

pred q : b,

[forall v1 : a . o(v1) = o2(v1)])

11.6: ### Hint: redeclared sort 'a'

13.8: *** Error: expecting two arguments of equal sort

19.22: *** Error: no operation with 0 arguments found for 'c'