 thf(sortForObjects, type, (object: $tType)).  thf(sortForTimes, type, (time: $tType)).  thf(constantDawn, type, (dawn: time)).  thf(constantToday, type, (today: time)).  thf(constantIsExistsAt, type,    (existsAt: object\(&gt;\)time\(&gt;\)$o)).  thf(constantPrecedesTo, type,    (precedesTo: time\(&gt;\)time\(&gt;\)$o)).  thf(axiom1, axiom, (![X:time]:    ((?[Y:object]: (existsAt @Y@X))   =\(&gt;\) (![Z:time]: ((precedesTo @Z@X)    =\(&gt;\) (?[V:object]: (existsAt @V@Z))))))).  thf(axiom2, axiom,    (?[Y:object]: (existsAt @Y@today))).  thf(axiom3, axiom,    (![Y:time]: (precedesTo @dawn@Y))).  thf(conjecture1, conjecture,    (?[X:object]: (existsAt @X@dawn))). 