Thank you for your question! I'm really glad to see that this exercise is already being worked on!

It looks to me that you are entering the solution for x ↔ (y1 ∧ y2) or x <-> (y1 & y2). Please note that the circonflexe ^ is XOR or ⊕.

Out of curiosity: Which online tools did you use to verify your solution and how did you do so? I used the Embedded Systems Group's teaching tools on propositional logic. As an output, I used the truth table, and as an input used entered the variables x,y1,y2 and the formulas

(¬x ∨ y1) ∧ (¬x ∨ y2) ∧ (¬y1 ∨ ¬y2 ∨ x);
x <-> (y1 ^ y2)

The result was this truth table:

x | y1 | y2 | (!x|y1)&(!x|y2)&(!y1|!y2|x) | x<->!(y1<->y2) |
---|

0 | 0 | 0 | 1 | 1 |
---|

0 | 0 | 1 | 1 | 0 |
---|

0 | 1 | 0 | 1 | 0 |
---|

0 | 1 | 1 | 0 | 1 |
---|

1 | 0 | 0 | 0 | 0 |
---|

1 | 0 | 1 | 0 | 1 |
---|

1 | 1 | 0 | 0 | 1 |
---|

1 | 1 | 1 | 1 | 0 |
---|

You can see that only for two assignments the formulas evaluate to the same result. Another way of telling these formulas apart would have been connecting the two formulas with ↔ and checking it for tautology. The following sequent calculus proof tree is generated for an XOR between the two formulas. (Note that XOR is precisely the negation of ↔.)

From the green leaves, you can tell that the new xor-formula is satisfiable which means that its operands differ.

Here is another trick on reading the resulting cnf: A → B is the same as (¬A ∨ B), hence your formula can be read as

(X → Y1) ∧ (X → Y2) ∧ (¬X → (¬Y1 ∨ ¬Y2))

This means that there three if-statements:

- if Y is satisfied, Y1 is satisfied too
- if Y is satisfied, Y2 is satisfied too
- if Y is not satisfied, at least one of Y1, Y2 is not satisfied

One can easily tell that this this the conjunction ∧.