Finite Witness

A tiny first order model checker over a directed graph and one unary predicate. Write a sentence, then see a small structure and an assignment that makes it true or false.