Seems you are totally off topic and not talking about the two Liars
from the riddle, namely this here what Alice in the forest hears
from the animals:
Lion: Yesterday was one of my lying days.
Unicorn: Yesterday was one of my lying days.
Thats why my predicate is called two_liars/6. First liar is Lion,
the second liar is Unicorn, in total we have two liars.
There is a bug somewhere in your reasoning or how you enter
the formula or how you use your system to check for antinomy.
Since you make a quite far off claim.
But the riddle gives a hint that it is satisfiable. Even uniquely
satisfiable, since the riddle says:
From these statements, Alice, who was a bright girl, was able to
deduce the day of the week. What was it?
You can also verify satisfiable via my Prolog code:
Or via library(clpb) by using the predicate which has this documentation:
labeling(+Vs)
Assigns truth values to the variables Vs such that all constraints are satisfied.
So if I use this SAT solver predicate I also find that it is satisfiable:
