(set-logic QF_UF)
(declare-sort S 0)
(declare-fun f (S) S)
(declare-fun g (S) S)
(declare-fun h (S) S)
(declare-fun x1 () S)
(declare-fun x2 () S)
(assert (= (f (g (h (f x1)))) (h (g (f (h x2))))))
(assert (= (g (g (h (f x1)))) (h (g (g (h x2))))))
(check-sat)