Yices 1.0.38 no counterexample between depths: [0, 12].