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