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