∀x ∀y (Man(x) ∧ Man(y) ∧ Taller(x, y) → CanBlock(x, y))
∀x (Man(x) ∧ SameClass(x, michael) ∧ ¬(x=michael) → Taller(michael, x))
∀x ∀y ∀z ((Taller(x, y) ∧ Taller(y, z)) → Taller(x, z))
Man(peter) ∧ Taller(peter, michael)
∀x (¬JumpWhenShooting(x) → CanBlock(michael, x))
¬CanBlock(michael, windy)
∀x (JumpWhenShooting(x) → GreatShooter(x))
∃x (Man(x) ∧ SameClass(x, michael) ∧ ¬Taller(peter, x))