logic THF.THF

spec test =

thf(numbers,type,(

num: $tType )).

thf(holdsDuring_THFTYPE_IiooI,type,(

holdsDuring_THFTYPE_IiooI: $i > $o > $o )).

thf(lAnna_THFTYPE_i,type,(

lAnna_THFTYPE_i: $i )).

thf(lBen_THFTYPE_i,type,(

lBen_THFTYPE_i: $i )).

thf(lBill_THFTYPE_i,type,(

lBill_THFTYPE_i: $i )).

thf(lBob_THFTYPE_i,type,(

lBob_THFTYPE_i: $i )).

thf(lMary_THFTYPE_i,type,(

lMary_THFTYPE_i: $i )).

thf(lSue_THFTYPE_i,type,(

lSue_THFTYPE_i: $i )).

thf(lYearFn_THFTYPE_IiiI,type,(

lYearFn_THFTYPE_IiiI: $i > $i )).

thf(likes_THFTYPE_IiioI,type,(

likes_THFTYPE_IiioI: $i > $i > $o )).

thf(n2009_THFTYPE_i,type,(

n2009_THFTYPE_i: $i )).

thf(parent_THFTYPE_IiioI,type,(

parent_THFTYPE_IiioI: $i > $i > $o )).

%----The translated axioms

thf(ax,axiom,

( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i ) )).

thf(ax_001,axiom,

( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i ) )).

thf(ax_002,axiom,

( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( ~ @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i ) ) )).

thf(ax_003,axiom,

( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i ) )).

thf(ax_004,axiom,

( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i ) )).

thf(ax_005,axiom,

( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( ~ @ ( parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBen_THFTYPE_i ) ) )).

thf(ax_006,axiom,

( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i ) )).

thf(ax_007,axiom,

( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i ) )).

thf(ax_008,axiom,

( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i ) )).

thf(ax_009,axiom,

( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i ) @ ( ~ @ ( likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i ) ) )).

%----The translated conjecture

thf(con,conjecture,(

? [R: $i > $i > $o,X: $i,Y: $i] :

( holdsDuring_THFTYPE_IiooI @ ( lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i )

@ ( ( R @ X @ lAnna_THFTYPE_i )

& ( ~ @ ( R @ Y @ lAnna_THFTYPE_i ) ) ) ) )).