A paper I'm reading says the following:
Plaisted [3] showed that it is possible to write formally correct PROLOG programs using first-order predicate-calculus semantics and yet derive nonsense results such as 3 < 2.
It is referring to the fact that Prologs didn't use the occurs check back then (the 1980s).
Unfortunately, the paper it cites is behind a paywall. I'd still like to see an example such as this. Intuitively, it feels like the omission of the occurs check just expands the universe of structures to include circular ones (but this intuition must be wrong, according to the author).
I hope this example isn't
smaller(3, 2) :- X = f(X).
That would be disappointing.
Here is the example from the paper in modern syntax:
three_less_than_two :-
less_than(s(X), X).
less_than(X, s(X)).
Indeed we get:
?- three_less_than_two.
true.
Because:
?- less_than(s(X), X).
X = s(s(X)).
Specifically, this explains the choice of 3 and 2 in the query: Given X = s(s(X)) the value of s(X) is "three-ish" (it contains three occurrences of s if you don't unfold the inner X), while X itself is "two-ish".
Enabling the occurs check gets us back to logical behavior:
?- set_prolog_flag(occurs_check, true).
true.
?- three_less_than_two.
false.
?- less_than(s(X), X).
false.
So this is indeed along the lines of
arbitrary_statement :-
arbitrary_unification_without_occurs_check.