I am told "SO-Horn = P".
Determining whether or not a graph is bipartite is in P.
Therefore there should be a SO-Horn query for it.
I'm still new to all this, but here's a SO query I came up with that hopefully defines bipartiteness:
There exist R,B such that: [for all x R(x) xor B(x)] and [for all x,y E(x,y) implies ((R(x) and B(y)) or (R(y) and B(x)))]
(Every x is red or blue; if there's an edge between x and y, then x and y must be different)
But that's not SO-Horn.