∀x (BatteryPoweredWatch(x) → ¬AutomaticWatch(x))
∀x (DigitalWatch(x) → BatteryPoweredWatch(x))
∃x (MechanicalWatch(x) ∧ AutomaticWatch(x))
∀x (SmartWatch(x) → DigitalWatch(x))
¬(DigitalWatch(moonwatch) ⊕ AutomaticWatch(moonwatch))
MechanicalWatch(moonwatch)) ∨ BatteryPoweredWatch(moonwatch) → ¬SmartWatch(moonwatch)