(! oV WU iA) input A precedes output V ---------------------------------------- (false R (! (iE & ! iF) | (! iF WU (oY & ! iF)))) output Y occurs between input E and input F ---------------------------------------- (false R (! (oV & ! oW) | (! oW U (oU & ! oW)))) output U occurs after output V until output W ---------------------------------------- (false R (! iF | (false R ! oV))) output V does never occur after input F ---------------------------------------- (! (true U iF) | ((! oX & ! iF) U (iF | ((oX & ! iF) U (iF | ((! oX & ! iF) U (iF | ((oX & ! iF) U (iF | (! oX U iF)))))))))) output X occurs at most twice before input F ---------------------------------------- (! (true U oV) | ((! oX & ! oV) U (oV | ((oX & ! oV) U (oV | ((! oX & ! oV) U (oV | ((oX & ! oV) U (oV | (! oX U oV)))))))))) output X occurs at most twice before output V ---------------------------------------- (! oY WU (oV & ! oY)) output V occurs before output Y ---------------------------------------- (false R (! (iD & ! iA) | (! iA WU (oX & ! iA)))) output X occurs between input D and input A ---------------------------------------- (! oV WU (oY & ! oV)) output Y occurs before output V ---------------------------------------- (false R (! ((oU & ! iF) & (true U iF)) | (! oZ U iF))) output Z does never occur between output U and input F ---------------------------------------- (false R (! (iB & ! iD) | (! iD U (oY & ! iD)))) output Y occurs after input B until input D ---------------------------------------- (! (true U oW) | (! oZ U (iF | oW))) input F precedes output Z before output W ---------------------------------------- (false R (! oU | (true U oZ))) output Z responds to output U ---------------------------------------- (! oU WU oW) output U does never occur before output W ---------------------------------------- (false R ! oV) output V does never occur ---------------------------------------- (false R (! (iD & ! oW) | (! oW WU (oZ & ! oW)))) output Z occurs between input D and output W ---------------------------------------- ((false R ! oZ) | (true U (oZ & (true U oX)))) output X occurs after output Z ---------------------------------------- (! oX WU (oY & ! oX)) output Y occurs before output X ---------------------------------------- (false R (! (oX & ! iC) | (! oV WU iC))) output V does never occur after output X until input C ---------------------------------------- (false R (! oV | (true U oX))) output X responds to output V ---------------------------------------- (false R (! iB | (false R ! oZ))) output Z does never occur after input B ---------------------------------------- (! (true U iB) | (! oU U (iE | iB))) input E precedes output U before input B ---------------------------------------- (! oX WU (oX WU (! oX WU (oX WU (false R ! oX))))) output X occurs at most twice ---------------------------------------- (false R (! ((oW & ! oU) & (true U oU)) | (! oV U oU))) output V does never occur between output W and output U ---------------------------------------- (false R (! ((iB & ! iC) & (true U iC)) | (! oU U iC))) output U does never occur between input B and input C ---------------------------------------- (true U oZ) output Z occurs eventually ---------------------------------------- (false R ! oU) output U does never occur ---------------------------------------- (false R (! (oW & ! iE) | (! iE U (oY & ! iE)))) output Y occurs after output W until input E ---------------------------------------- (false R (! iC | (true U oW))) output W responds to input C ---------------------------------------- (false R ! oZ) output Z does never occur ---------------------------------------- (false R (! (oZ & ! iE) | (! iE WU (oW & ! iE)))) output W occurs between output Z and input E ---------------------------------------- (false R (! ((iA & ! iE) & (true U iE)) | (! oW U iE))) output W does never occur between input A and input E ---------------------------------------- (false R (! (oX & ! iD) | (! oU WU iD))) output U does never occur after output X until input D ---------------------------------------- (false R (! (oU & ! oX) | (! oZ WU oX))) output Z does never occur after output U until output X ---------------------------------------- (false R (! (oY & ! iF) | (! iF U (oX & ! iF)))) output X occurs after output Y until input F ---------------------------------------- (false R (! (oY & ! oW) | (! oW U (oV & ! oW)))) output V occurs after output Y until output W ---------------------------------------- (true U oU) output U occurs eventually ---------------------------------------- (false R (! (iE & ! iB) | (! oW WU iB))) output W does never occur after input E until input B ---------------------------------------- (! (true U oX) | ((! oU & ! oX) U (oX | ((oU & ! oX) U (oX | ((! oU & ! oX) U (oX | ((oU & ! oX) U (oX | (! oU U oX)))))))))) output U occurs at most twice before output X ---------------------------------------- (true U oX) output X occurs eventually ---------------------------------------- (! oX WU (oV & ! oX)) output V occurs before output X ---------------------------------------- (! (true U iB) | (! oZ U (oV | iB))) output V precedes output Z before input B ---------------------------------------- (false R (! iF | (true U oW))) output W responds to input F ---------------------------------------- (! (true U oV) | (! oZ U (iA | oV))) input A precedes output Z before output V ---------------------------------------- (! oU WU (oU WU (! oU WU (oU WU (false R ! oU))))) output U occurs at most twice ---------------------------------------- ((false R ! iC) | (true U (iC & (true U oZ)))) output Z occurs after input C ---------------------------------------- (! oW WU iF) output W does never occur before input F ---------------------------------------- ((false R ! iF) | (true U (iF & (true U oY)))) output Y occurs after input F ---------------------------------------- (! (true U oY) | (! oZ U (iA | oY))) input A precedes output Z before output Y ---------------------------------------- (! (true U iF) | (! oY U (iC | iF))) input C precedes output Y before input F ---------------------------------------- (false R (! iA | (true U oV))) output V responds to input A ---------------------------------------- (! (true U iE) | ((! oW & ! iE) U (iE | ((oW & ! iE) U (iE | ((! oW & ! iE) U (iE | ((oW & ! iE) U (iE | (! oW U iE)))))))))) output W occurs at most twice before input E ---------------------------------------- (! iA WU (oU & ! iA)) output U occurs before input A ---------------------------------------- (true U oX) output X occurs eventually ---------------------------------------- (! (true U iD) | (! oZ U (iE | iD))) input E precedes output Z before input D ---------------------------------------- (false R (! (iD & ! oY) | (! oY U (oX & ! oY)))) output X occurs after input D until output Y ---------------------------------------- ((false R ! iD) | (true U (iD & (true U oU)))) output U occurs after input D ---------------------------------------- (false R (! oW | (false R ! oV))) output V does never occur after output W ---------------------------------------- (true U oU) output U occurs eventually ---------------------------------------- (false R (! ((iD & ! oY) & (true U oY)) | (! oU U oY))) output U does never occur between input D and output Y ---------------------------------------- (false R (! oU | (false R ! oW))) output W does never occur after output U ---------------------------------------- (false R (! oW | (false R ! oV))) output V does never occur after output W ---------------------------------------- (! oX WU (oX WU (! oX WU (oX WU (false R ! oX))))) output X occurs at most twice ---------------------------------------- (false R (! (iA & ! iD) | (! iD U (oZ & ! iD)))) output Z occurs after input A until input D ---------------------------------------- (! (true U iD) | ((! oV & ! iD) U (iD | ((oV & ! iD) U (iD | ((! oV & ! iD) U (iD | ((oV & ! iD) U (iD | (! oV U iD)))))))))) output V occurs at most twice before input D ---------------------------------------- (false R (! oV | (false R ! oU))) output U does never occur after output V ---------------------------------------- (! oZ WU oW) output Z does never occur before output W ---------------------------------------- (false R (! ((oZ & ! oU) & (true U oU)) | (! oX U oU))) output X does never occur between output Z and output U ---------------------------------------- (false R (! oU | (false R ! oZ))) output Z does never occur after output U ---------------------------------------- (false R (! (iF & ! oU) | (! oU U (oV & ! oU)))) output V occurs after input F until output U ---------------------------------------- (false R (! (iB & ! iA) | (! oV WU iA))) output V does never occur after input B until input A ---------------------------------------- (false R (! iD | (false R ! oW))) output W does never occur after input D ---------------------------------------- (false R (! (oW & ! iA) | (! iA U (oZ & ! iA)))) output Z occurs after output W until input A ---------------------------------------- (false R ! oY) output Y does never occur ---------------------------------------- (false R (! oU | (true U oZ))) output Z responds to output U ---------------------------------------- (false R (! iC | (true U oW))) output W responds to input C ---------------------------------------- (true U oZ) output Z occurs eventually ---------------------------------------- (false R (! (iC & ! iB) | (! iB U (oU & ! iB)))) output U occurs after input C until input B ---------------------------------------- (! oX WU (oX WU (! oX WU (oX WU (false R ! oX))))) output X occurs at most twice ---------------------------------------- (false R ! oY) output Y does never occur ---------------------------------------- (false R (! (oZ & ! oY) | (! oY WU (oU & ! oY)))) output U occurs between output Z and output Y ---------------------------------------- (false R (! iF | (false R ! oX))) output X does never occur after input F ---------------------------------------- (false R (! ((iC & ! oV) & (true U oV)) | (! oY U oV))) output Y does never occur between input C and output V ---------------------------------------- (false R (! ((oV & ! oU) & (true U oU)) | (! oZ U oU))) output Z does never occur between output V and output U ---------------------------------------- (false R (! oV | (false R ! oU))) output U does never occur after output V ---------------------------------------- (false R (! ((iA & ! iF) & (true U iF)) | (! oX U iF))) output X does never occur between input A and input F ---------------------------------------- (! (true U iA) | ((! oX & ! iA) U (iA | ((oX & ! iA) U (iA | ((! oX & ! iA) U (iA | ((oX & ! iA) U (iA | (! oX U iA)))))))))) output X occurs at most twice before input A ---------------------------------------- (false R (! ((oV & ! iB) & (true U iB)) | (! oX U iB))) output X does never occur between output V and input B ---------------------------------------- (! iF WU (oX & ! iF)) output X occurs before input F ---------------------------------------- ((false R ! iF) | (true U (iF & (true U oU)))) output U occurs after input F ---------------------------------------- (! (true U iA) | (! oY U (iF | iA))) input F precedes output Y before input A ---------------------------------------- (false R (! (oW & ! oU) | (! oZ WU oU))) output Z does never occur after output W until output U ---------------------------------------- (true U oV) output V occurs eventually ---------------------------------------- (false R (! iD | (true U oV))) output V responds to input D ---------------------------------------- (! oV WU (oV WU (! oV WU (oV WU (false R ! oV))))) output V occurs at most twice ---------------------------------------- (false R (! (iB & ! iC) | (! oX WU iC))) output X does never occur after input B until input C ---------------------------------------- (false R (! (iE & ! oU) | (! oU U (oX & ! oU)))) output X occurs after input E until output U ---------------------------------------- (false R (! (oX & ! iA) | (! oZ WU iA))) output Z does never occur after output X until input A ---------------------------------------- (false R (! ((iE & ! oW) & (true U oW)) | (! oV U oW))) output V does never occur between input E and output W ---------------------------------------- ((false R ! oU) | (true U (oU & (true U oW)))) output W occurs after output U ----------------------------------------