Typed eXtended First-order Logic (TXF)

New logic features

Problem

In logic

In TPTP format

Challenge problem

Jon is the owner of Odie. Odie bit Jon twice! If a dog bites a person more than once, and (s)he is not the owner of the dog, the (s)he hates the owner of the dog. If a dog bites a person at least once then the person chases the dog, else the person feeds the dog. Jon says that a dog he does not own bit him. Jon tells the truth. Prove that there exists a dog that Jon chases and another person that Jon hates.