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