Tiny FO Lab

Edit a tiny structure with two unary predicates and one binary relation, then check first-order formulas against it. If your formula has free variables, you can set them or let the tool search for witnesses and counterexamples.