How does the transformation work? First, what is xor ⊕? Xor ⊕ is true if exactly one or its two arguments is true. It is hence the dual of biimplication/equality, which is true if precisely zero or two of its two arguments become true. Hence, ((b ∧ d) ⊕ (¬c ∨ a)) and ¬((b ∧ d) ↔ (¬c ∨ a)) are equal.
Note that there are two negation symbols on the right of ⊢. One is part of the substituted formula. The other one flips sides. In sequent calculus, you find satisfying assignments (i.e. counterexamples to unsatisfiability) by putting the formula in question to the left. A negation in sequent calculus means a switch of sides. That's why our online tool added a second negation and started on the right. It is equivalent to not adding a negation to this formula and starting on the left.
