The Output of X1 is Off
[21] (=> (= (Type ?g) XOR)
(<=> (= (Signal (Out 1 ?g)) On)
(not (= (Signal (In 1 ?g) (Signal (In 2 ?g)))))) {Given}
[22] (=> (= (Type X1) XOR)
(<=> (= (Signal (Out 1 X1)) On)
(not (= (Signal (In 1 X1) (Signal (In 2 X1)))))) {[21]: Univ. Elim.}
[23] (= (Type X1) XOR) {Given}
[24] (<=> (= (Signal (Out 1 X1)) On)
(not (= (Signal (In 1 X1) (Signal (In 2 X1))))) {[22],[23]; M. P.}
[25] (=> (= (Signal (Out 1 X1)) On)
(not (= (Signal (In 1 X1) (Signal (In 2 X1))))) {[24]: And Elim.}
[26] (not (= (Signal (Out 1 X1)) On)) {[13],[25]: M. T.}
[27] (or (= (Signal ?t) On) (= (Signal ?t) Off)) {Given}
[28] (or (= (Signal X1) On) (= (Signal X1) Off)) {[27]: Univ. Elim.}
[29] (= (Signal (Out 1 X1)) Off) {[26],[28]: U. Res.}