YES Problem: and(P,forall()) -> forall() or(P,forall()) -> forall() and(forall(),P) -> forall() or(forall(),P) -> forall() not(forall()) -> exists() and(P,exists()) -> exists() or(P,exists()) -> exists() and(exists(),P) -> exists() or(exists(),P) -> exists() not(exists()) -> forall() Proof: Matrix Interpretation Processor: dim=3 interpretation: [0] [exists] = [0] [0], [1 0 0] [1] [not](x0) = [0 0 0]x0 + [0] [0 0 0] [0], [1 0 0] [1 0 0] [1] [or](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0] [0 0 0] [0 0 0] [0], [1 0 0] [1 0 0] [1] [and](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0] [0 0 0] [0 0 0] [0], [0] [forall] = [0] [0] orientation: [1 0 0] [1] [0] and(P,forall()) = [0 0 0]P + [0] >= [0] = forall() [0 0 0] [0] [0] [1 0 0] [1] [0] or(P,forall()) = [0 0 0]P + [0] >= [0] = forall() [0 0 0] [0] [0] [1 0 0] [1] [0] and(forall(),P) = [0 0 0]P + [0] >= [0] = forall() [0 0 0] [0] [0] [1 0 0] [1] [0] or(forall(),P) = [0 0 0]P + [0] >= [0] = forall() [0 0 0] [0] [0] [1] [0] not(forall()) = [0] >= [0] = exists() [0] [0] [1 0 0] [1] [0] and(P,exists()) = [0 0 0]P + [0] >= [0] = exists() [0 0 0] [0] [0] [1 0 0] [1] [0] or(P,exists()) = [0 0 0]P + [0] >= [0] = exists() [0 0 0] [0] [0] [1 0 0] [1] [0] and(exists(),P) = [0 0 0]P + [0] >= [0] = exists() [0 0 0] [0] [0] [1 0 0] [1] [0] or(exists(),P) = [0 0 0]P + [0] >= [0] = exists() [0 0 0] [0] [0] [1] [0] not(exists()) = [0] >= [0] = forall() [0] [0] problem: Qed