...durch Einschränkung der Position der Quantoren.
in SMT-LIB: nur außen existentiell.
(benchmark check :logic QF_UF :extrafuns ((f U U)(g U U)(x U)(y U)) :formula (not (implies (= x y) (= (f(f(g x))) (f(f(g y)))) )) )
nicht erfüllbar, d. h. das Gegenteil ist allgemeingültig: