Reachability problems: =============================== error_51 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, A, A] --------------- error_48 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, B, A] --------------- error_6 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, D, A] --------------- error_27 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, E, A] --------------- error_33 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, A, A] --------------- error_47 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, C, A] --------------- error_31 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, D, A] --------------- error_54 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, E, A] --------------- error_49 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, F, A] --------------- error_17 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, B, A] --------------- error_58 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, C, A] --------------- error_37 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, D, A] --------------- error_42 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, E, A] --------------- error_57 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, F, A] --------------- error_15 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, A, A, A] --------------- error_12 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, A, B, A] --------------- error_0 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, A, C, A] --------------- error_7 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, A, E, A] --------------- error_41 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, A, F, A] --------------- error_21 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, A, D, A, A] --------------- error_38 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, A, D, B, A] --------------- error_53 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, A, D, C, A] --------------- error_30 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, A, D, E, A] --------------- error_56 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, A, D, D, E, A] --------------- error_9 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, A, D, F, E, A] --------------- error_52 reachable via input sequence [A, C, C, B, A, D, D, F, C, C, F, B, B, F, D, C, B, A, D, F, F, A] --------------- All other errors unreachable LTL problems: =============================== Formula: (false R ! oU) "output U does never occur" Formula is not satisfied! An error path is [iA, oZ, iB, oU] ([iA, oY, iF, oY, iF, oX, iD, iD, oX])* --------------- Formula: (false R (! oV | (false R ! oZ))) "output Z does never occur after output V" Formula is satisfied. --------------- Formula: (true U oZ) "output Z occurs eventually" Formula is not satisfied! An error path is [iD, oY] ([iB, oW, iA, oX, iD, oW, iB, oU, iB])* --------------- Formula: (! oY WU oX) "output X precedes output Y" Formula is not satisfied! An error path is [iD, oY] ([iA, oZ, iB, oZ, iD, oW, iA, oW, iB, oY])* --------------- Formula: (! oV WU oY) "output Y precedes output V" Formula is satisfied. --------------- Formula: (! (true U iE) | ((! oY & ! iE) U (iE | ((oY & ! iE) U (iE | ((! oY & ! iE) U (iE | ((oY & ! iE) U (iE | (! oY U iE)))))))))) "output Y occurs at most twice before input E" Formula is satisfied. --------------- Formula: (false R (! (oZ & ! oU) | (! oU WU (oX & ! oU)))) "output X occurs between output Z and output U" Formula is not satisfied! An error path is [iA, oZ, iB, oU] ([iA, oY, iF, oY, iF, oX, iD, iD, oX])* --------------- Formula: (! oZ WU iD) "output Z does never occur before input D" Formula is not satisfied! An error path is [iA, oZ] ([iA, oY, iB, oW, iD, oY, iF, oZ])* --------------- Formula: (false R (! oX | (true U oY))) "output Y responds to output X" Formula is not satisfied! An error path is [iB, oZ, iC, oX] ([iA, oU, iF, oX, iD, oZ, iC])* --------------- Formula: (! (true U iF) | (! oZ U (oX | iF))) "output X precedes output Z before input F" Formula is not satisfied! An error path is [iA, oZ, iF] ([oZ, iF, oX, iA, oZ, iF, oY, iD, iF])* --------------- Formula: (false R (! (oU & ! oV) | (! oV U (oY & ! oV)))) "output Y occurs after output U until output V" Formula is not satisfied! An error path is [iA, oZ, iB, oU] ([iC, oW, iA, oW, iB, oX, iF, oU, iB, oX, iF, oZ, iA, iF, iA, oZ, iB, oU])* --------------- Formula: (! (true U oX) | ((! oV & ! oX) U (oX | ((oV & ! oX) U (oX | ((! oV & ! oX) U (oX | ((oV & ! oX) U (oX | (! oV U oX)))))))))) "output V occurs at most twice before output X" Formula is satisfied. --------------- Formula: (! oZ WU (oV & ! oZ)) "output V occurs before output Z" Formula is not satisfied! An error path is [iA, oZ] ([iA, oY, iB, oW, iD, oY, iF, oZ])* --------------- Formula: (false R ! oY) "output Y does never occur" Formula is not satisfied! An error path is [iD, oY] ([iA, oZ, iB, oZ, iD, oW, iA, oW, iB, oY])* --------------- Formula: (! oZ WU (oZ WU (! oZ WU (oZ WU (false R ! oZ))))) "output Z occurs at most twice" Formula is not satisfied! An error path is [iA, oZ, iA] ([oY, iB, oW, iD, oY, iF, oZ, iA])* --------------- Formula: (! oV WU oW) "output V does never occur before output W" Formula is satisfied. --------------- Formula: (false R (! iF | (false R ! oV))) "output V does never occur after input F" Formula is satisfied. --------------- Formula: (false R ! oY) "output Y does never occur" Formula is not satisfied! An error path is [iD, oY] ([iA, oZ, iB, oZ, iD, oW, iA, oW, iB, oY])* --------------- Formula: (! oU WU oW) "output W precedes output U" Formula is not satisfied! An error path is [iA, oZ, iB, oU] ([iA, oY, iF, oY, iF, oX, iD, iD, oX])* --------------- Formula: (true U oW) "output W occurs eventually" Formula is not satisfied! An error path is [iA, oZ] ([iA, oY, iD, oZ, iA, oX, iA, oZ])* --------------- Formula: (! oU WU iF) "input F precedes output U" Formula is not satisfied! An error path is [iA, oZ, iB, oU] ([iA, oY, iF, oY, iF, oX, iD, iD, oX])* --------------- Formula: (false R (! ((iA & ! oV) & (true U oV)) | (! oY U oV))) "output Y does never occur between input A and output V" Formula is satisfied. --------------- Formula: (false R (! (iB & ! iF) | (! iF WU (oU & ! iF)))) "output U occurs between input B and input F" Formula is not satisfied! An error path is [iB, oZ, iF] ([oZ, iA, oY, iA, oX, iA, oU, iF])* --------------- Formula: (! oW WU oV) "output V precedes output W" Formula is not satisfied! An error path is [iA, oZ, iC, oW] ([iA, oW, iB, oX, iB, oZ, iF])* --------------- Formula: (false R (! (iC & ! oY) | (! oY WU (oX & ! oY)))) "output X occurs between input C and output Y" Formula is satisfied. --------------- Formula: (false R (! (oZ & ! oY) | (! oY U (oX & ! oY)))) "output X occurs after output Z until output Y" Formula is not satisfied! An error path is [iA, oZ] ([iA, oY, iB, oW, iD, oY, iF, oZ])* --------------- Formula: (false R (! (iF & ! oY) | (! oY WU (oX & ! oY)))) "output X occurs between input F and output Y" Formula is not satisfied! An error path is [iA, oZ, iF, oZ, iB, oY] ([iA, oX, iD, oU, iB, oZ, iB, oY])* --------------- Formula: (! (true U oZ) | (! oX U (iC | oZ))) "input C precedes output X before output Z" Formula is not satisfied! An error path is [iD, oY, iB, oW, iA, oX, iB, oY, iF, oZ] ([iA, iD, oW, iB, oZ, iF, oW, iA, oX, iB, oY, iF, oZ])* --------------- Formula: (false R (! (iD & ! iB) | (! iB U (oU & ! iB)))) "output U occurs after input D until input B" Formula is not satisfied! An error path is [iD, oY] ([iA, oZ, iB, oZ, iD, oW, iA, oW, iB, oY])* --------------- Formula: (! oY WU (oY WU (! oY WU (oY WU (false R ! oY))))) "output Y occurs at most twice" Formula is not satisfied! An error path is [iD, oY, iA] ([oZ, iB, oZ, iD, oW, iA, oW, iB, oY, iA])* --------------- Formula: (! oZ WU iB) "output Z does never occur before input B" Formula is not satisfied! An error path is [iA, oZ] ([iA, oY, iB, oW, iD, oY, iF, oZ])* --------------- Formula: (false R (! iC | (false R ! oU))) "output U does never occur after input C" Formula is not satisfied! An error path is [iA, oZ, iC, oW, iD, oU] ([iA, oU, iA, oX, iD, oZ, iA, oW, iB, oX, iB, oZ, iF, iD, oU])* --------------- Formula: ((false R ! oZ) | (true U (oZ & (true U oW)))) "output W occurs after output Z" Formula is not satisfied! An error path is [iA, oZ] ([iA, oY, iD, oZ, iA, oX, iA, oZ])* --------------- Formula: (false R (! iB | (false R ! oW))) "output W does never occur after input B" Formula is not satisfied! An error path is [iB, oZ, iA, oW] ([iA, oU, iA, oX, iA, oW])* --------------- Formula: (! oV WU (oV WU (! oV WU (oV WU (false R ! oV))))) "output V occurs at most twice" Formula is satisfied. --------------- Formula: (false R (! (iE & ! iF) | (! iF U (oX & ! iF)))) "output X occurs after input E until input F" Formula is satisfied. --------------- Formula: (false R (! iC | (true U oZ))) "output Z responds to input C" Formula is satisfied. --------------- Formula: ((false R ! oY) | (true U (oY & (true U oX)))) "output X occurs after output Y" Formula is not satisfied! An error path is [iD, oY] ([iA, oZ, iB, oZ, iD, oW, iA, oW, iB, oY])* --------------- Formula: (! (true U iD) | (! oV U (iC | iD))) "input C precedes output V before input D" Formula is satisfied. --------------- Formula: (! (true U oV) | (! oU U (iE | oV))) "input E precedes output U before output V" Formula is satisfied. --------------- Formula: ((false R ! oU) | (true U (oU & (true U oY)))) "output Y occurs after output U" Formula is not satisfied! An error path is [iA, oZ, iB, oU] ([iC, oW, iA, oW, iB, oX, iF, oU, iB, oX, iF, oZ, iA, iF, iA, oZ, iB, oU])* --------------- Formula: (false R ! oY) "output Y does never occur" Formula is not satisfied! An error path is [iD, oY] ([iA, oZ, iB, oZ, iD, oW, iA, oW, iB, oY])* --------------- Formula: (false R (! iE | (true U oY))) "output Y responds to input E" Formula is satisfied. --------------- Formula: (false R (! ((oZ & ! iA) & (true U iA)) | (! oW U iA))) "output W does never occur between output Z and input A" Formula is not satisfied! An error path is [iA, oZ, iC, oW, iA] ([oW, iB, oX, iB, oZ, iF, iA])* --------------- Formula: (! (true U iB) | ((! oU & ! iB) U (iB | ((oU & ! iB) U (iB | ((! oU & ! iB) U (iB | ((oU & ! iB) U (iB | (! oU U iB)))))))))) "output U occurs at most twice before input B" Formula is not satisfied! An error path is [iD, oY, iC, oZ, iF, oU, iA, oU, iC, oU, iB] ([oZ, iF, oU, iA, oU, iC, oU, iB])* --------------- Formula: (false R (! ((oV & ! iE) & (true U iE)) | (! oZ U iE))) "output Z does never occur between output V and input E" Formula is satisfied. --------------- Formula: (false R (! (iB & ! iF) | (! iF WU (oZ & ! iF)))) "output Z occurs between input B and input F" Formula is not satisfied! An error path is [iD, oY, iB, oW, iF] ([oW, iF, oY, iB, oW, iF, oW, iF])* --------------- Formula: (! oW WU iE) "input E precedes output W" Formula is not satisfied! An error path is [iA, oZ, iC, oW] ([iA, oW, iB, oX, iB, oZ, iF])* --------------- Formula: (false R (! ((iE & ! iA) & (true U iA)) | (! oV U iA))) "output V does never occur between input E and input A" Formula is satisfied. --------------- Formula: (false R (! iF | (true U oX))) "output X responds to input F" Formula is not satisfied! An error path is [iF, oZ] ([iA, oW, iA, oW, iB, oY, iF, oZ])* --------------- Formula: (false R (! (iE & ! oU) | (! oY WU oU))) "output Y does never occur after input E until output U" Formula is satisfied. --------------- Formula: (false R (! ((oV & ! iF) & (true U iF)) | (! oZ U iF))) "output Z does never occur between output V and input F" Formula is satisfied. --------------- Formula: (! oY WU iB) "input B precedes output Y" Formula is not satisfied! An error path is [iD, oY] ([iA, oZ, iB, oZ, iD, oW, iA, oW, iB, oY])* --------------- Formula: (! oW WU iB) "output W does never occur before input B" Formula is not satisfied! An error path is [iA, oZ, iC, oW] ([iA, oW, iB, oX, iB, oZ, iF])* --------------- Formula: (false R ! oX) "output X does never occur" Formula is not satisfied! An error path is [iB, oZ, iC, oX] ([iA, oU, iF, oX, iD, oZ, iC])* --------------- Formula: (! (true U oZ) | ((! oV & ! oZ) U (oZ | ((oV & ! oZ) U (oZ | ((! oV & ! oZ) U (oZ | ((oV & ! oZ) U (oZ | (! oV U oZ)))))))))) "output V occurs at most twice before output Z" Formula is satisfied. --------------- Formula: (! (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" Formula is not satisfied! An error path is [iB, oZ, iF, oZ, iD, oZ, iB, oX] ([iA, oX])* --------------- Formula: (false R (! (oX & ! iF) | (! iF WU (oW & ! iF)))) "output W occurs between output X and input F" Formula is not satisfied! An error path is [iB, oZ, iC, oX, iF] ([oX, iB, oU, iA, oZ, iC, oX, iF])* --------------- Formula: (false R (! iF | (true U oX))) "output X responds to input F" Formula is not satisfied! An error path is [iF, oZ] ([iA, oW, iA, oW, iB, oY, iF, oZ])* --------------- Formula: (! oY WU iB) "input B precedes output Y" Formula is not satisfied! An error path is [iD, oY] ([iA, oZ, iB, oZ, iD, oW, iA, oW, iB, oY])* --------------- Formula: (false R (! (iA & ! iC) | (! iC WU (oY & ! iC)))) "output Y occurs between input A and input C" Formula is not satisfied! An error path is [iA, oZ, iC] ([oW, iD, oU, iC, oZ, iF, oX, iD, oW, iD, oU, iC])* --------------- Formula: (! oX WU (oW & ! oX)) "output W occurs before output X" Formula is not satisfied! An error path is [iB, oZ, iC, oX] ([iA, oU, iF, oX, iD, oZ, iC])* --------------- Formula: (! (true U iD) | ((! oU & ! iD) U (iD | ((oU & ! iD) U (iD | ((! oU & ! iD) U (iD | ((oU & ! iD) U (iD | (! oU U iD)))))))))) "output U occurs at most twice before input D" Formula is not satisfied! An error path is [iA, oZ, iB, oU, iB, oY, iB, oU, iF, oU, iD] ([oY, iA, oU, iA, oX, iF, oW, iB, oY, iF, oZ, iF, iA, iD])* --------------- Formula: (false R (! ((iF & ! iB) & (true U iB)) | (! oV U iB))) "output V does never occur between input F and input B" Formula is satisfied. --------------- Formula: (false R (! (oY & ! iD) | (! iD U (oV & ! iD)))) "output V occurs after output Y until input D" Formula is not satisfied! An error path is [iD, oY] ([iA, oZ, iB, oZ, iD, oW, iA, oW, iB, oY])* --------------- Formula: (! oX WU (oX WU (! oX WU (oX WU (false R ! oX))))) "output X occurs at most twice" Formula is not satisfied! An error path is [iB, oZ, iC, oX, iA] ([oU, iF, oX, iD, oZ, iC, iA])* --------------- Formula: (false R ! oU) "output U does never occur" Formula is not satisfied! An error path is [iA, oZ, iB, oU] ([iA, oY, iF, oY, iF, oX, iD, iD, oX])* --------------- Formula: (! oV WU iC) "input C precedes output V" Formula is satisfied. --------------- Formula: (false R (! (oU & ! iB) | (! oZ WU iB))) "output Z does never occur after output U until input B" Formula is not satisfied! An error path is [iA, oZ, iB, oU, iA, oY, iA, oZ] ([iA, oX, iD, iF, oW, iD, oU, iB, oU, iA, oY, iA, oZ])* --------------- Formula: (false R (! iC | (true U oY))) "output Y responds to input C" Formula is not satisfied! An error path is [iA, oZ, iC] ([oW, iD, oU, iC, oZ, iF, oX, iD, oW, iD, oU, iC])* --------------- Formula: (false R (! (oX & ! iD) | (! iD U (oV & ! iD)))) "output V occurs after output X until input D" Formula is not satisfied! An error path is [iB, oZ, iC, oX] ([iA, oU, iF, oX, iD, oZ, iC])* --------------- Formula: (false R (! ((iA & ! iB) & (true U iB)) | (! oW U iB))) "output W does never occur between input A and input B" Formula is not satisfied! An error path is [iA, oZ, iC, oW, iB] ([oZ, iC, oZ, iD, oX, iC, iB])* --------------- Formula: (! oZ WU iD) "output Z does never occur before input D" Formula is not satisfied! An error path is [iA, oZ] ([iA, oY, iB, oW, iD, oY, iF, oZ])* --------------- Formula: (! iB WU (oX & ! iB)) "output X occurs before input B" Formula is not satisfied! An error path is [iB, oZ] ([iA, oW, iA, oU, iA, oX, iB, oZ])* --------------- Formula: (false R ! oY) "output Y does never occur" Formula is not satisfied! An error path is [iD, oY] ([iA, oZ, iB, oZ, iD, oW, iA, oW, iB, oY])* --------------- Formula: (! (true U iE) | (! oX U (iA | iE))) "input A precedes output X before input E" Formula is satisfied. --------------- Formula: (false R (! (iA & ! oV) | (! oV WU (oU & ! oV)))) "output U occurs between input A and output V" Formula is satisfied. --------------- Formula: (! (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" Formula is not satisfied! An error path is [iD, oY, iB, oW, iB, oU, iF, oU, iF, oU, iF, oZ] ([iB, oW, iA, oX, iA, oX])* --------------- Formula: (false R (! ((oZ & ! iE) & (true U iE)) | (! oX U iE))) "output X does never occur between output Z and input E" Formula is satisfied. --------------- Formula: (! iD WU (oY & ! iD)) "output Y occurs before input D" Formula is not satisfied! An error path is [iD, oY] ([iA, oZ, iB, oZ, iD, oW, iA, oW, iB, oY])* --------------- Formula: (false R (! (iD & ! oZ) | (! oZ U (oX & ! oZ)))) "output X occurs after input D until output Z" Formula is not satisfied! An error path is [iD, oY] ([iA, oZ, iB, oZ, iD, oW, iA, oW, iB, oY])* --------------- Formula: ((false R ! oZ) | (true U (oZ & (true U oY)))) "output Y occurs after output Z" Formula is not satisfied! An error path is [iA, oZ] ([iB, oU, iC, oW, iA, oW, iB, oX, iF, oU, iB, oX, iF, oZ, iA, iF, iA, oZ])* --------------- Formula: (! oY WU iC) "output Y does never occur before input C" Formula is not satisfied! An error path is [iD, oY] ([iA, oZ, iB, oZ, iD, oW, iA, oW, iB, oY])* --------------- Formula: (true U oW) "output W occurs eventually" Formula is not satisfied! An error path is [iA, oZ] ([iA, oY, iD, oZ, iA, oX, iA, oZ])* --------------- Formula: (! oV WU oX) "output V does never occur before output X" Formula is satisfied. --------------- Formula: (false R (! oV | (false R ! oZ))) "output Z does never occur after output V" Formula is satisfied. --------------- Formula: (false R (! oX | (true U oW))) "output W responds to output X" Formula is not satisfied! An error path is [iB, oZ, iC, oX] ([iA, oU, iF, oX, iD, oZ, iC])* --------------- Formula: (! (true U iE) | (! oW U (oZ | iE))) "output Z precedes output W before input E" Formula is satisfied. --------------- Formula: (false R (! (oW & ! oU) | (! oZ WU oU))) "output Z does never occur after output W until output U" Formula is not satisfied! An error path is [iA, oZ, iC, oW, iB, oZ] ([iA, oX, iC, oZ, iF, oW, iA, oW, iD, oX, iD, oZ, iB, iC, oX, iD, oZ, iA, oW, iF, oW, iF, oZ, iD, oW, iA, oZ, iC, oW, iB, oZ])* --------------- Formula: (false R (! (iB & ! oU) | (! oW WU oU))) "output W does never occur after input B until output U" Formula is not satisfied! An error path is [iB, oZ, iA, oW] ([iA, oU, iA, oX, iA, oW])* --------------- Formula: (false R (! (iF & ! oX) | (! oX U (oZ & ! oX)))) "output Z occurs after input F until output X" Formula is not satisfied! An error path is [iF, oZ, iF] ([oU, iA, oX, iD, oU, iF, oY, iF])* --------------- Formula: (! (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" Formula is satisfied. --------------- Formula: (false R (! ((oV & ! oX) & (true U oX)) | (! oW U oX))) "output W does never occur between output V and output X" Formula is satisfied. --------------- Formula: (false R ! oV) "output V does never occur" Formula is satisfied. --------------- Formula: ((false R ! oY) | (true U (oY & (true U oZ)))) "output Z occurs after output Y" Formula is not satisfied! An error path is [iD, oY] ([iB, oW, iA, oX, iD, oW, iB, oU, iB])* --------------- Formula: (! oU WU (oU WU (! oU WU (oU WU (false R ! oU))))) "output U occurs at most twice" Formula is not satisfied! An error path is [iA, oZ, iB, oU, iA] ([oY, iF, oY, iA, oU, iB, oZ, iB, oU, iA])* --------------- Formula: (false R (! (iE & ! oZ) | (! oZ WU (oX & ! oZ)))) "output X occurs between input E and output Z" Formula is satisfied. --------------- Formula: (false R (! (iB & ! oZ) | (! oX WU oZ))) "output X does never occur after input B until output Z" Formula is not satisfied! An error path is [iA, oZ, iD, oY, iB, oX] ([iA, oZ, iB, oX, iF, iB, oX])* --------------- Formula: ((false R ! iB) | (true U (iB & (true U oX)))) "output X occurs after input B" Formula is not satisfied! An error path is [iB, oZ] ([iA, oW, iB, oW, iB, oU, iD, oY])* --------------- Formula: (false R (! iC | (true U oU))) "output U responds to input C" Formula is not satisfied! An error path is [iA, oZ, iC] ([oW, iA, oW, iB, oX, iD, oZ, iB, iF, iD, iA, oY, iF, oX, iF, oZ, iC])* --------------- 31 constraints satisfied, 69 unsatisfied.