; simple problem to check that 'and' retains its semantics when part of a formula that is
; an argument to the 'knows' predicate

(note TQC1)
(file tinySUMO.kif)
(file tinyHOL.kif)
(minLang thf)
(regen true)
(time 60)

; works with tinySUMO in THF

; thf(ax241,axiom,((knows_THFTYPE_IiooI @ lBill_THFTYPE_i @ ((father_THFTYPE_IiioI @ lBill_THFTYPE_i @ lJoe_THFTYPE_i) & (father_THFTYPE_IiioI @ lBill_THFTYPE_i @ lJane_THFTYPE_i))))).

; thf(conj,conjecture, (( (knows_THFTYPE_IiooI @ lBill_THFTYPE_i @ (father_THFTYPE_IiioI @ lBill_THFTYPE_i @ lJoe_THFTYPE_i)) ))).

(knows Bill
  (and
    (father Bill Joe)
    (father Bill Jane)))

(query (knows Bill (father Bill Joe)))

(answer yes)