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