Reachability problems: =============================== error_18 reachable via input sequence [A, B, C, C, E, A, A, F, A] --------------- error_51 reachable via input sequence [A, B, C, C, E, A, A, B, A] --------------- error_32 reachable via input sequence [A, B, C, C, E, A, A, D, A] --------------- error_4 reachable via input sequence [A, B, C, C, E, A, A, C, A] --------------- error_57 reachable via input sequence [B, D, C, D, C, E, B, F, A] --------------- error_16 reachable via input sequence [B, D, C, D, C, E, B, B, A] --------------- error_53 reachable via input sequence [B, D, C, D, C, E, B, C, A] --------------- error_5 reachable via input sequence [A, B, C, C, E, A, A, E, F, A] --------------- error_29 reachable via input sequence [A, B, C, C, E, A, A, E, B, A] --------------- error_27 reachable via input sequence [A, B, C, C, E, A, A, E, D, A] --------------- error_39 reachable via input sequence [A, B, C, C, E, A, A, E, C, A] --------------- error_46 reachable via input sequence [A, B, C, C, E, A, A, E, E, A] --------------- error_56 reachable via input sequence [A, B, C, C, E, A, A, A, F, A] --------------- error_50 reachable via input sequence [A, B, C, C, E, A, A, A, B, A] --------------- error_31 reachable via input sequence [A, B, C, C, E, A, A, A, D, A] --------------- error_48 reachable via input sequence [A, B, C, C, E, A, A, A, C, A] --------------- error_47 reachable via input sequence [A, B, C, C, E, A, A, E, A, F, A] --------------- error_19 reachable via input sequence [A, B, C, C, E, A, A, E, A, B, A] --------------- error_22 reachable via input sequence [A, B, C, C, E, A, A, E, A, A, A] --------------- error_10 reachable via input sequence [A, B, C, C, E, A, A, E, A, C, A] --------------- error_43 reachable via input sequence [A, B, C, C, E, A, A, E, A, E, A] --------------- error_49 reachable via input sequence [A, B, C, C, E, A, A, A, A, F, A] --------------- error_33 reachable via input sequence [A, B, C, C, E, A, A, A, A, A, A] --------------- error_0 reachable via input sequence [A, B, C, C, E, A, A, A, A, D, A] --------------- error_41 reachable via input sequence [A, B, C, C, E, A, A, A, A, E, A] --------------- All other errors unreachable LTL problems: =============================== Formula: (false R (! iE | (false R ! oU))) "output U does never occur after input E" Formula is not satisfied! An error path is [iB, oY, iD, oW, iE, oX, iA, oU, iA, oZ] ([iA, iA, oW, iB, oZ, iD, oZ])* --------------- Formula: (false R (! (iF & ! iA) | (! iA U (oW & ! iA)))) "output W occurs after input F until input A" Formula is satisfied. --------------- Formula: (! (true U oZ) | (! oW U (iD | oZ))) "input D precedes output W before output Z" Formula is not satisfied! An error path is [iB, oY, iE, oW, iA, oZ] ([iE, oW, iC, oZ, iE, oX, iA, oW])* --------------- Formula: (! (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" Formula is not satisfied! An error path is [iE, oV, iB, oW, iA, oW, iC, iA, oW, iA, oX] ([iA, oX])* --------------- Formula: (true U oV) "output V occurs eventually" Formula is not satisfied! An error path is [iA, oY] ([iB, oX, iC, oX, iE, oZ, iA, oW])* --------------- Formula: (! oZ WU oU) "output Z does never occur before output U" Formula is not satisfied! An error path is [iA, oY, iE, oZ] ([iA, oV, iA, oV])* --------------- Formula: (! oZ WU iD) "input D precedes output Z" Formula is not satisfied! An error path is [iA, oY, iE, oZ] ([iA, oV, iA, oV])* --------------- Formula: (! oX WU oW) "output W precedes output X" Formula is not satisfied! An error path is [iA, oY, iB, oX] ([iC, oX, iE, oZ, iA, oW, iB, oX])* --------------- Formula: (false R (! ((iF & ! iE) & (true U iE)) | (! oW U iE))) "output W does never occur between input F and input E" Formula is satisfied. --------------- Formula: (false R (! oV | (false R ! oZ))) "output Z does never occur after output V" Formula is not satisfied! An error path is [iE, oV, iC, oZ] ([iA, oX, iB, oZ])* --------------- Formula: (! (true U oZ) | (! oX U (oW | oZ))) "output W precedes output X before output Z" Formula is not satisfied! An error path is [iA, oY, iB, oX, iD, oZ] ([iA, oX, iC, oW, iB, oX, iD, oZ])* --------------- Formula: (! oY WU oX) "output X precedes output Y" Formula is not satisfied! An error path is [iA, oY] ([iB, oX, iC, oX, iE, oZ, iA, oW])* --------------- Formula: (! (true U oY) | (! oW U (iB | oY))) "input B precedes output W before output Y" Formula is not satisfied! An error path is [iE, oV, iA, oW, iD, oY, iA, oZ] ([iA, oW, iE, oW, iD, oZ, iD, iD, iD, oY, iC, oZ, iA, iD, oX])* --------------- Formula: (! oU WU oZ) "output U does never occur before output Z" Formula is not satisfied! An error path is [iC, oU] ([iA, oW, iB, oZ, iD, oZ, iA])* --------------- Formula: (false R (! (iA & ! iC) | (! iC WU (oV & ! iC)))) "output V occurs between input A and input C" Formula is not satisfied! An error path is [iA, oY, iC] ([oY, iA, oW, iE, oW, iC, oZ, iA, oW, iC])* --------------- Formula: (! iE WU (oW & ! iE)) "output W occurs before input E" Formula is not satisfied! An error path is [iE, oV] ([iA, oW, iB, oW, iA, oW])* --------------- Formula: (false R (! (iE & ! oV) | (! oW WU oV))) "output W does never occur after input E until output V" Formula is not satisfied! An error path is [iA, oY, iD, oX, iE, oW] ([iB, oW, iA, oY, iE, oZ, iE, oW, iD, oX, iE, oW])* --------------- Formula: (! iA WU (oZ & ! iA)) "output Z occurs before input A" Formula is not satisfied! An error path is [iA, oY] ([iB, oX, iC, oX, iE, oZ, iA, oW])* --------------- Formula: (false R (! (iB & ! oV) | (! oV U (oW & ! oV)))) "output W occurs after input B until output V" Formula is not satisfied! An error path is [iC, oU, iB] ([oY, iA, oZ, iA, oZ, iB])* --------------- Formula: (! oY WU iA) "output Y does never occur before input A" Formula is not satisfied! An error path is [iB, oY] ([iA, oZ, iD, oX, iC, oZ, iA, oW])* --------------- Formula: (true U oV) "output V occurs eventually" Formula is not satisfied! An error path is [iA, oY] ([iB, oX, iC, oX, iE, oZ, iA, oW])* --------------- 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 [iA, oY, iD] ([oX, iD, oZ, iD, oX, iD, oW, iD])* --------------- Formula: (false R (! (oZ & ! iA) | (! iA U (oW & ! iA)))) "output W occurs after output Z until input A" Formula is not satisfied! An error path is [iA, oY, iE, oZ] ([iA, oV, iA, oV])* --------------- Formula: (false R (! (iC & ! oW) | (! oV WU oW))) "output V does never occur after input C until output W" Formula is satisfied. --------------- Formula: (! (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" Formula is not satisfied! An error path is [iC, oU, iE, oZ, iE, oZ, iA, oZ, iD, oW] ([iA, oZ])* --------------- Formula: (false R (! (oV & ! iF) | (! oW WU iF))) "output W does never occur after output V until input F" Formula is not satisfied! An error path is [iE, oV, iA, oW] ([iA, oW, iA, oX])* --------------- Formula: (! oZ WU oW) "output W precedes output Z" Formula is not satisfied! An error path is [iA, oY, iE, oZ] ([iA, oV, iA, oV])* --------------- Formula: (false R (! iA | (true U oX))) "output X responds to input A" Formula is not satisfied! An error path is [iA, oY] ([iC, oY, iA, oW, iE, oW, iC, oZ, iA, oW])* --------------- Formula: (false R (! iB | (true U oZ))) "output Z responds to input B" Formula is not satisfied! An error path is [iE, oV, iB] ([oW, iA, oW, iD, oW, iB])* --------------- Formula: (false R (! oY | (true U oZ))) "output Z responds to output Y" Formula is satisfied. --------------- Formula: (! (true U oY) | ((! oU & ! oY) U (oY | ((oU & ! oY) U (oY | ((! oU & ! oY) U (oY | ((oU & ! oY) U (oY | (! oU U oY)))))))))) "output U occurs at most twice before output Y" Formula is not satisfied! An error path is [iC, oU, iD, oU, iC, oU, iD, oW, iB, oY] ([iA, oZ, iA, oZ, iB, oY])* --------------- Formula: ((false R ! iF) | (true U (iF & (true U oU)))) "output U occurs after input F" Formula is satisfied. --------------- Formula: (! iB WU (oV & ! iB)) "output V occurs before input B" Formula is not satisfied! An error path is [iB, oY] ([iA, oZ, iD, oX, iC, oZ, iA, oW])* --------------- Formula: (false R (! iF | (false R ! oX))) "output X does never occur after input F" Formula is satisfied. --------------- Formula: (! (true U oY) | (! oZ U (iB | oY))) "input B precedes output Z before output Y" Formula is not satisfied! An error path is [iC, oU, iE, oZ, iA, oY] ([iA, oW, iE, oZ, iA, iC, iC, oZ, iD, oZ, iE, oZ, iA, oY])* --------------- Formula: (false R (! ((oX & ! oV) & (true U oV)) | (! oW U oV))) "output W does never occur between output X and output V" Formula is not satisfied! An error path is [iA, oY, iD, oX, iD, oZ, iC, oW, iB, oV] ([iB, oV, iB, oZ])* --------------- Formula: (false R (! (iE & ! oZ) | (! oV WU oZ))) "output V does never occur after input E until output Z" Formula is not satisfied! An error path is [iE, oV] ([iA, oW, iB, oW, iA, oW])* --------------- Formula: (false R (! (iA & ! oU) | (! oU U (oV & ! oU)))) "output V occurs after input A until output U" Formula is not satisfied! An error path is [iA, oY] ([iB, oX, iC, oX, iE, oZ, iA, oW])* --------------- Formula: (! (true U oZ) | (! oX U (iB | oZ))) "input B precedes output X before output Z" Formula is not satisfied! An error path is [iA, oY, iD, oX, iD, oZ] ([iC, oW, iD, oX, iA, oZ, iE, oY, iC, oW, iD, oX, iD, oZ])* --------------- Formula: ((false R ! iD) | (true U (iD & (true U oV)))) "output V occurs after input D" Formula is not satisfied! An error path is [iA, oY, iD] ([oX, iD, oZ, iD, oX, iD, oW, iD])* --------------- Formula: (false R (! (iF & ! iD) | (! iD WU (oW & ! iD)))) "output W occurs between input F and input D" Formula is satisfied. --------------- Formula: ((false R ! iB) | (true U (iB & (true U oY)))) "output Y occurs after input B" Formula is not satisfied! An error path is [iA, oY, iB] ([oX, iC, oX, iE, oZ, iA, oW, iB])* --------------- Formula: (false R (! (oW & ! iB) | (! iB U (oU & ! iB)))) "output U occurs after output W until input B" Formula is not satisfied! An error path is [iC, oU, iA, oW] ([iA, oZ, iC, oW, iD, oZ, iA, oW])* --------------- Formula: (! oW WU (oX & ! oW)) "output X occurs before output W" Formula is not satisfied! An error path is [iC, oU, iA, oW] ([iA, oZ, iC, oW, iA, oU, iA, oW])* --------------- Formula: (false R (! (oY & ! iF) | (! iF U (oU & ! iF)))) "output U occurs after output Y until input F" Formula is not satisfied! An error path is [iA, oY] ([iB, oX, iC, oX, iE, oZ, iA, oW])* --------------- Formula: (false R (! (iB & ! iC) | (! iC U (oX & ! iC)))) "output X occurs after input B until input C" Formula is not satisfied! An error path is [iC, oU, iB] ([oY, iA, oZ, iA, oZ, iB])* --------------- Formula: (false R (! (oV & ! oY) | (! oY WU (oU & ! oY)))) "output U occurs between output V and output Y" Formula is not satisfied! An error path is [iE, oV, iB, oW, iE, oY] ([iE, oY, iD, oX, iE, oZ, iC, oW, iA, oW, iB, oW, iE, oY])* --------------- Formula: (! oY WU (oW & ! oY)) "output W occurs before output Y" Formula is not satisfied! An error path is [iA, oY] ([iB, oX, iC, oX, iE, oZ, iA, oW])* --------------- Formula: (false R (! iE | (false R ! oV))) "output V does never occur after input E" Formula is not satisfied! An error path is [iE, oV] ([iA, oW, iB, oW, iA, oW])* --------------- Formula: (false R (! iB | (false R ! oU))) "output U does never occur after input B" Formula is not satisfied! An error path is [iC, oU, iC, oZ, iB, oU] ([iA, oU, iB, oU])* --------------- Formula: (! iC WU (oW & ! iC)) "output W occurs before input C" Formula is not satisfied! An error path is [iC, oU] ([iA, oW, iB, oZ, iD, oZ, iA])* --------------- Formula: (false R (! (oW & ! oY) | (! oV WU oY))) "output V does never occur after output W until output Y" Formula is not satisfied! An error path is [iE, oV, iB, oW, iD, oV] ([iA, oW, iB, oW, iD, oV])* --------------- Formula: (! oX WU iB) "input B precedes output X" Formula is not satisfied! An error path is [iA, oY, iD, oX] ([iB, oW, iD, oZ, iC, oW, iB, oV, iE, oX, iB, oW, iE, oY, iC, oW, iD, oX])* --------------- Formula: ((false R ! iE) | (true U (iE & (true U oZ)))) "output Z occurs after input E" Formula is not satisfied! An error path is [iE, oV] ([iA, oW, iB, oW, iA, oW])* --------------- Formula: (false R (! iC | (true U oV))) "output V responds to input C" Formula is not satisfied! An error path is [iC, oU] ([iA, oW, iB, oZ, iD, oZ, iA])* --------------- Formula: (false R (! oW | (true U oY))) "output Y responds to output W" Formula is not satisfied! An error path is [iC, oU, iA, oW] ([iA, oZ, iC, oW, iA, oU, iA, oW])* --------------- Formula: (false R (! (iF & ! iB) | (! iB WU (oW & ! iB)))) "output W occurs between input F and input B" 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 [iC, oU, iE, oZ, iE, oZ, iE, oZ, iC, oX] ([iA, iC, oZ, iD, oZ, iE, oZ, iE, oZ, iC, oX])* --------------- Formula: (! oY WU iE) "input E precedes output Y" Formula is not satisfied! An error path is [iA, oY] ([iB, oX, iC, oX, iE, oZ, iA, oW])* --------------- Formula: (false R (! ((oZ & ! iF) & (true U iF)) | (! oX U iF))) "output X does never occur between output Z and input F" Formula is satisfied. --------------- Formula: (false R (! iA | (false R ! oU))) "output U does never occur after input A" Formula is not satisfied! An error path is [iC, oU, iC, oZ, iA, oU] ([iA, oX, iD, oZ, iC, oZ, iA, oU])* --------------- Formula: (! oW WU (oY & ! oW)) "output Y occurs before output W" Formula is not satisfied! An error path is [iC, oU, iA, oW] ([iA, oZ, iC, oW, iA, oU, iA, oW])* --------------- Formula: (false R (! iC | (false R ! oZ))) "output Z does never occur after input C" Formula is not satisfied! An error path is [iB, oY, iC, oZ] ([iA, oY, iA, oZ, iB, oX, iA, oZ])* --------------- Formula: (! oV WU iA) "output V does never occur before input A" Formula is not satisfied! An error path is [iE, oV] ([iA, oW, iB, oW, iA, oW])* --------------- Formula: ((false R ! iF) | (true U (iF & (true U oZ)))) "output Z occurs after input F" Formula is satisfied. --------------- Formula: (true U oY) "output Y occurs eventually" Formula is not satisfied! An error path is [iC, oU] ([iA, oW, iB, oZ, iD, oZ, iA])* --------------- Formula: (false R (! (iC & ! oU) | (! oZ WU oU))) "output Z does never occur after input C until output U" Formula is not satisfied! An error path is [iB, oY, iC, oZ] ([iA, oY, iA, oZ, iB, oX, iA, oZ])* --------------- Formula: (! iF WU (oV & ! iF)) "output V occurs before input F" Formula is satisfied. --------------- Formula: (! oV WU (oV WU (! oV WU (oV WU (false R ! oV))))) "output V occurs at most twice" Formula is not satisfied! An error path is [iE, oV, iA] ([oW, iB, oW, iA, oW, iB, oW, iD, oV, iA, oW, iA])* --------------- 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 [iA, oY, iB] ([oX, iC, oX, iC, oW, iE, oY, iA, oZ, iC, oW, 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 [iC, oU, iA] ([oW, iA, oZ, iC, oW, iA, oU, iA])* --------------- Formula: (true U oY) "output Y occurs eventually" Formula is not satisfied! An error path is [iC, oU] ([iA, oW, iB, oZ, iD, oZ, iA])* --------------- 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 [iA, oY, iB] ([oX, iC, oX, iC, oW, iE, oY, iA, oZ, iC, oW, iB])* --------------- Formula: ((false R ! iF) | (true U (iF & (true U oY)))) "output Y occurs after input F" Formula is satisfied. --------------- Formula: (false R (! (oY & ! iC) | (! oV WU iC))) "output V does never occur after output Y until input C" Formula is not satisfied! An error path is [iA, oY, iE, oZ, iA, oV] ([iA, oV, iA, oV])* --------------- Formula: (false R (! ((iA & ! iE) & (true U iE)) | (! oZ U iE))) "output Z does never occur between input A and input E" Formula is not satisfied! An error path is [iB, oY, iE, oW, iA, oZ, iE] ([oW, iC, oZ, iE, oX, iA, oW, iE])* --------------- 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 not satisfied! An error path is [iA, oY, iC, oY, iC, oY, iE] ([oX, iB, oZ, iC, oW, iB, oW, iB, oW, iE, oY, iC, oW, iC, oY, iC, oY, iE])* --------------- Formula: (false R (! iC | (false R ! oZ))) "output Z does never occur after input C" Formula is not satisfied! An error path is [iB, oY, iC, oZ] ([iA, oY, iA, oZ, iB, oX, iA, oZ])* --------------- Formula: (true U oZ) "output Z occurs eventually" Formula is not satisfied! An error path is [iC, oU] ([iD, oU, iC, oU, iD, oW])* --------------- Formula: ((false R ! oU) | (true U (oU & (true U oW)))) "output W occurs after output U" Formula is not satisfied! An error path is [iC, oU] ([iB, oY, iA, oZ, iA, oZ])* --------------- Formula: (false R (! (iB & ! iF) | (! iF U (oZ & ! iF)))) "output Z occurs after input B until input F" Formula is not satisfied! An error path is [iE, oV, iB] ([oW, iA, oW, iD, oW, iB])* --------------- Formula: (false R (! (iD & ! oU) | (! oV WU oU))) "output V does never occur after input D until output U" Formula is not satisfied! An error path is [iE, oV, iB, oW, iD, oV] ([iA, oW, iB, oW, iD, oV])* --------------- Formula: (false R (! ((oU & ! oW) & (true U oW)) | (! oZ U oW))) "output Z does never occur between output U and output W" Formula is not satisfied! An error path is [iC, oU, iC, oZ, iC, oW] ([iA, oX, iA, oZ, iC, oW])* --------------- Formula: (! (true U oW) | ((! oU & ! oW) U (oW | ((oU & ! oW) U (oW | ((! oU & ! oW) U (oW | ((oU & ! oW) U (oW | (! oU U oW)))))))))) "output U occurs at most twice before output W" Formula is not satisfied! An error path is [iC, oU, iD, oU, iC, oU, iC, oW] ([iC, oZ, iC, oU, iC, oW])* --------------- Formula: (false R (! ((iC & ! oV) & (true U oV)) | (! oZ U oV))) "output Z does never occur between input C and output V" Formula is not satisfied! An error path is [iA, oY, iB, oX, iC, oX, iB, oZ, iB, oW, iB, oV] ([iB, oZ, iB, oV])* --------------- Formula: (false R (! oV | (true U oX))) "output X responds to output V" Formula is not satisfied! An error path is [iE, oV] ([iA, oW, iB, oW, iA, oW])* --------------- Formula: (false R (! (oY & ! oU) | (! oX WU oU))) "output X does never occur after output Y until output U" Formula is not satisfied! An error path is [iA, oY, iB, oX] ([iC, oX, iE, oZ, iA, oW, iB, oX])* --------------- Formula: (! (true U oV) | (! oZ U (oY | oV))) "output Y precedes output Z before output V" Formula is satisfied. --------------- Formula: (! oZ WU iB) "output Z does never occur before input B" Formula is not satisfied! An error path is [iA, oY, iE, oZ] ([iA, oV, iA, oV])* --------------- Formula: (! oW WU oX) "output W does never occur before output X" Formula is not satisfied! An error path is [iC, oU, iA, oW] ([iA, oZ, iC, oW, iA, oU, iA, oW])* --------------- Formula: (! oZ WU oY) "output Z does never occur before output Y" Formula is not satisfied! An error path is [iC, oU, iC, oZ] ([iA, oU, iA, oX, iD, oZ, iC, oZ])* --------------- Formula: (! (true U iE) | ((! oW & ! iE) U (iE | ((oW & ! iE) U (iE | ((! oW & ! iE) U (iE | ((oW & ! iE) U (iE | (! oW U iE)))))))))) "output W occurs at most twice before input E" Formula is not satisfied! An error path is [iA, oY, iA, oW, iB, oW, iA, oZ, iA, iA, oW, iE] ([oW, iD, oZ, iE, oZ, iE])* --------------- Formula: (! oX WU iC) "output X does never occur before input C" Formula is not satisfied! An error path is [iA, oY, iB, oX] ([iC, oX, iE, oZ, iA, oW, iB, oX])* --------------- Formula: (! oV WU (oV WU (! oV WU (oV WU (false R ! oV))))) "output V occurs at most twice" Formula is not satisfied! An error path is [iE, oV, iA] ([oW, iB, oW, iA, oW, iB, oW, iD, oV, iA, oW, iA])* --------------- Formula: (false R (! iB | (false R ! oW))) "output W does never occur after input B" Formula is not satisfied! An error path is [iE, oV, iB, oW] ([iA, oW, iA, oZ])* --------------- Formula: (! oU WU oY) "output U does never occur before output Y" Formula is not satisfied! An error path is [iC, oU] ([iA, oW, iB, oZ, iD, oZ, iA])* --------------- Formula: (false R (! (iD & ! iC) | (! oU WU iC))) "output U does never occur after input D until input C" Formula is not satisfied! An error path is [iC, oU, iD, oU] ([iA, oZ, iD, oZ])* --------------- Formula: (true U oW) "output W occurs eventually" Formula is not satisfied! An error path is [iC, oU] ([iB, oY, iA, oZ, iA, oZ])* --------------- Formula: (false R (! (iE & ! oX) | (! oU WU oX))) "output U does never occur after input E until output X" Formula is satisfied. --------------- Formula: (false R (! (oU & ! iD) | (! iD WU (oX & ! iD)))) "output X occurs between output U and input D" Formula is not satisfied! An error path is [iC, oU, iD] ([oU, iC, oU, iD, oW, iD])* --------------- 14 constraints satisfied, 86 unsatisfied.