(note TQC2b)
(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(lForm_THFTYPE_o_type, type, lForm_THFTYPE_o: $o).

;thf(modalAttribute_THFTYPE_IoioI_type, type, modalAttribute_THFTYPE_IoioI: ($o > ($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 @ lForm_THFTYPE_o @ 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 Form Obligation)

(query (modalAttribute ?B Permission))

(answer yes)