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