(declare-fun f ()