(note TQC3)
(minLang thf)
;thf(lObligation_THFTYPE_i_type, type, lObligation_THFTYPE_i: $i).
;thf(lPermission_THFTYPE_i_type, type, lPermission_THFTYPE_i: $i).
;thf(lProhibition_THFTYPE_i_type, type, lProhibition_THFTYPE_i: $i).
;thf(lATPbook_THFTYPE_i_type, type, lATPbook_THFTYPE_i: $i).
;thf(lAdam_THFTYPE_i_type, type, lAdam_THFTYPE_i: $i).

;thf(modalAttribute_THFTYPE_IoioI_type, type, modalAttribute_THFTYPE_IoioI: ($o > ($i > $o))).
;thf(authors_THFTYPE_IoioI_type, type, authors_THFTYPE_IoioI: ($i > $i > $o)).

;thf(t22,axiom,((! [A:$o]: ((modalAttribute_THFTYPE_IoioI @ A @ lPermission_THFTYPE_i) =>
;  (~ (modalAttribute_THFTYPE_IoioI @ (~ (A)) @ lObligation_THFTYPE_i)))))).

;thf(t23,axiom,((! [A:$o]: ((modalAttribute_THFTYPE_IoioI @ A @ lObligation_THFTYPE_i) =>
;  (modalAttribute_THFTYPE_IoioI @ A @ lPermission_THFTYPE_i))))).

;thf(t21,axiom,((! [A:$o]: ((modalAttribute_THFTYPE_IoioI @ A @ lProhibition_THFTYPE_i) => (modalAttribute_THFTYPE_IoioI @ (~ (A)) @ lObligation_THFTYPE_i))))).

;thf(t2,axiom,((modalAttribute_THFTYPE_IoioI @ (authors_THFTYPE_IoioI @ lAdam_THFTYPE_i @  lATPbook_THFTYPE_i) @ lObligation_THFTYPE_i))).

;thf(t1,conjecture,((? [B:$o]: (modalAttribute_THFTYPE_IoioI @ B @ lPermission_THFTYPE_i)))).

(=>
  (modalAttribute ?A Permission)
  (not
    (modalAttribute
      (not ?A)
      Obligation)))

(=>
  (modalAttribute ?A Obligation)
  (modalAttribute ?A Permission))

(=>
  (modalAttribute ?A Prohibition)
  (modalAttribute
    (not ?A)
    Obligation))

(modalAttribute
  (authors Adam ATPbook)
  Obligation)

(query (modalAttribute ?B Permission))

(answer yes)