  The logic of the hide and seek game LHS was proposed to reason about search
missions and interactions between agents in pursuit-evasion environments. As
proved in literature, having an equality constant in the language of LHS
drastically increases its computational complexity: the satisfiability problem
for LHS with multiple relations is undecidable. In this work we improve the
existing result by showing that LHS with a single relation is undecidable. With
the existing findings, we provide a van Benthem style characterization theorem
for the expressive power of the logic. Finally, by `splitting' the language of
LHS-, a crucial fragment of LHS without the equality constant, into two
`isolated parts', we provide a complete Hilbert style proof system for LHS- and
prove that its satisfiability problem is decidable, whose proofs would indicate
significant differences between the proposals of LHS- and of ordinary product
logics. Although LHS and LHS- are frameworks for interactions of 2 agents, all
results in the article can be easily transferred to their generalizations for
settings with any n > 2 agents.
