Typed Higher-order Logic (THF)

New logic features

Problem

In logic

In TPTP format

Challenge problem

Andrew, Betty, and Charlie are (different) people. Andrew loves himself, Betty does not love herself. Selfish love is a relationship between two (different) people in which the second person loves themself (and the first person is ignored). Prove that there exists a property of a person that is true for Andrew but not for Betty.