Monadic predicate logic (with identity) is decidable (Boolos, Burgess, and Jeffrey 2007, Ch. 21. The result goes back to Löwenheim-Skolem 1915).
This website lets you check whether a formula is a theorem. If it's not a theorem, you will be shown a counter-example.
@x(Ax>(Ax*Bx))You can add logical symbols by clicking the buttons above, or by using this correspondence:
|Logical symbol||Keyboard character|