First-order Logic (FOF)

New logic features

Problem

In logic

In TPTP format

Challenge problem

If somone is good looking then one of their parents is good looking. If someone's oldest sibling is good looking then that someone is good looking. The (only) parents of Geoff are Bob and Maggie. Bob is not Maggie. The oldest sibling of Geoff is Jill. Geoff is not Jill. Jill is good looking, Bob is not. Therefore, Maggie is good looking.

Non-theorems