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