The Output of X1 is Off
(<=> (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] (and (<= (Signal (Out 1 X1) On) … ) {[24]: Bicond. Elim.}
(=> (Signal (Out 1 X1) On) … )
[26] (=> (Signal (Out 1 X1) On)
(not (Signal (In 1 X1) (Signal (In 2 X1))))) {[25]: And Elim.}
[27] (not (Signal (Out 1 X1) On)) {[14],[26]: M. T.}
[28] (or (Signal ?t On) (Signal ?t Off)) {Given}
[29] (or (Signal X1 On) (Signal X1 Off)) {[28]: Univ. Elim.}
[30] (Signal (Out 1 X1) Off) {[27],[29]: U. Res.}