∀x (Model(x) ∧ Summarization(x) ∧ OnlyUseInputDocument(x) → Faithful(x))
∀x (Model(x) ∧ Extractive(x) → Model(x) ∧ Summarization(x))
∀x (Model(x) ∧ Extractive(x) → OnlyUseInputDocument(x))
∃x (Model(x) ∧ Extractive(x) ∧ ¬Faithful(x))