• A ∧ B ⊢ B ∧ A
• P(a) ∧ P(b), a=c ∨ b=c ⊢ P(c)
• ∀x∃y R(x,y) → ∃y∀x R(x,y) ⊢ ∃x(∀y ¬R(x,y) ∨ ∀y R(y,x))

List of strings that should be recognized as variables (separated by commas):
(For example, using the default settings, having ∀x P(x) is allowed, but having ∀a P(a) is not, because a is not used for variables. With this setting, you can change which strings should be seen as a variable. All other strings that start with a lowercase letter will be seen as a constant or function symbol, depending on the context in which they are found.)

Rotate the proof by 180 degrees: ROTATE PROOF...