An Implmentation of a Free-variable Tableaux for KLM Preferential Logic P of Nonmonotonic Reasoning: the Theorem Prover FreeP 1.0