Reachability problems: =============================== error_47 reachable via input sequence [E, C, D] --------------- error_62 reachable via input sequence [C, C, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, A, C, A, C] --------------- error_29 reachable via input sequence [C, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, A, C, B] --------------- error_12 reachable via input sequence [C, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, A] --------------- error_58 reachable via input sequence [C, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, A, A, B] --------------- error_49 reachable via input sequence [C, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, D] --------------- error_6 reachable via input sequence [C, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, A, E, C, D] --------------- error_7 reachable via input sequence [C, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, C] --------------- error_17 reachable via input sequence [C, C, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, A, C, E, D] --------------- error_89 reachable via input sequence [C, C, D] --------------- error_51 reachable via input sequence [C, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, A, C, C] --------------- error_84 reachable via input sequence [C, A, B] --------------- error_21 reachable via input sequence [C, C, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, A, E, C, A] --------------- error_95 reachable via input sequence [C, C, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, A, C, D] --------------- error_75 reachable via input sequence [C, A, C, D] --------------- error_86 reachable via input sequence [C, C, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, C, C, A, A, A, A] --------------- error_5 reachable via input sequence [C, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, A, D] --------------- error_97 reachable via input sequence [C, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, E, A, C, C, C, A, A, A, C, E] --------------- All other errors unreachable LTL problems: =============================== Formula: (false R (! (oY & (true U iE)) | ((! iA | (! iE U (((oX & ! iE) & ! oW) & X ((! iE & ! oW) U oV)))) U iE))) "output X, output V without output W responds to input A betwen output Y and input E" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iA, oS, iE] ([oW, iA, oS, iE])* --------------- Formula: (! (true U iB) | (! oW U (iB | ((oT & ! oW) & X (! oW U oZ))))) "output T, output Z precedes output W before input B" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iC, oV, iA, oW, iA, oT, iB] ([oU, iA, oT, iE, oU, iB])* --------------- Formula: (false R (! iB | ((! ((oV & ! iE) & X (! iE U (oU & ! iE))) U (iE | oW)) | (false R ! (oV & X (true U oU)))))) "output W precedes output V, output U after input B until input E" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA, oT, iE, oU, iB, oU, iC, oU, iA, oV, iC, oU] ([iA, oT, iE, oU, iB, oU])* --------------- Formula: (false R (! (iB & (true U oU)) | ((! iD | (! oU U ((oT & ! oU) & X (! oU U oY)))) U oU))) "output T, output Y responds to input D between input B and output U" Formula is satisfied. --------------- Formula: (! (true U oZ) | ((! iB | (! oZ U (oV & ! oZ))) U oZ)) "output V responds to input B before output Z" Formula is satisfied. --------------- Formula: (false R (! oY | (false R (! iA | ((oW & ! oV) & X (! oV U oX)))))) "output W, output X without output V responds to input A after output Y" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iA] ([oS, iE, oW, iA])* --------------- Formula: (false R (! (oY & (true U oT)) | ((! iA | (! oT U (((oV & ! oT) & ! oU) & X ((! oT & ! oU) U oZ)))) U oT))) "output V, output Z without output U responds to input A betwen output Y and output T" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iC, oV, iA, oW, iA, oT] ([iA, oU])* --------------- Formula: (false R (! iC | (true U ((oV & ! oT) & X (! oT U oU))))) "output V, output U without output T always responds to input C" Formula is not satisfied! An error path is [iE, oX, iC] ([oU, iA, oT, iE, oU, iC, oX, iC])* --------------- Formula: ((false R ! iA) | (true U (iA & (! oT WU oW)))) "output W precedes output T after input A" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA, oT] ([iE, oU, iB, oU, iA, oT])* --------------- Formula: (false R (! oZ | (! (true U oT) | (! oT U (oU | ((iE & ! oT) & X (! oT U iD))))))) "input E, input D precedes output T after output Z until output U" Formula is satisfied. --------------- Formula: (false R (! oZ | ((iB & (! X (! iE U iD) | X (! iE U (iD & (true U oY))))) U (iE | (false R (iB & (! X (! iE U iD) | X (! iE U (iD & (true U oY)))))))))) "output Y responds to input B, input D after output Z until input E" Formula is satisfied. --------------- Formula: (false R (! ((oW & ! oT) & (true U oT)) | ((! iC | (! oT U (oU & ! oT))) U oT))) "output U responds to input C between output W and output T" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iA, oS, iE, oW, iC, oV, iE, oT] ([iA, oU])* --------------- Formula: (false R (! (oS & (true U oU)) | ((iA & (! X (! oU U iE) | X (! oU U (iE & (true U oV))))) U oU))) "output V responds to input A, input E between output S and output U" Formula is not satisfied! An error path is [iC, oS, iC, oV, iC, oX, iC, oS, iE, oU] ([iA, oS, iC, oV, iC, oX, iC, oS, iE, oU])* --------------- Formula: (! (true U iD) | (! ((oV & ! iD) & X (! iD U (oW & ! iD))) U (iD | oZ))) "output Z precedes output V, output W before input D" Formula is satisfied. --------------- Formula: (! (true U iC) | ((! iE | (! iC U ((oV & ! iC) & X (! iC U oZ)))) U iC)) "output V, output Z responds to input E before input C" Formula is not satisfied! An error path is [iE, oX, iC] ([oU, iA, oT, iE, oU, iC, oX, iC])* --------------- Formula: (! (true U oV) | (! oX U (oV | ((iE & ! oX) & X (! oX U oZ))))) "input E, output Z precedes output X before output V" Formula is not satisfied! An error path is [iE, oX, iC, oU, iC, oU, iA, oV] ([iA, oV])* --------------- Formula: (false R (! iA | (false R (! iE | (true U oW))))) "output W responds to input E after input A" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA, oT, iE] ([oU, iB, oU, iA, oT, iE])* --------------- Formula: (! (true U oW) | ((! iC | (! oW U ((oS & ! oW) & X (! oW U oU)))) U oW)) "output S, output U responds to input C before output W" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iA, oS, iE, oW] ([iA, oS, iE, oW])* --------------- Formula: (false R (! (iE & (true U iD)) | (! ((oT & ! iD) & X (! iD U (oS & ! iD))) U (iD | oY)))) "output Y precedes output T, output S between input E and input D" Formula is satisfied. --------------- Formula: (false R (! ((oX & ! oS) & (true U oS)) | ((! iC | (! oS U (oU & ! oS))) U oS))) "output U responds to input C between output X and output S" Formula is not satisfied! An error path is [iC, oS, iC, oV, iC, oX, iC, oS] ([iA, oW, iC, oX, iC, oS])* --------------- Formula: (! (true U (oU & X (true U oV))) | (! oU U iB)) "input B always precedes output U, output V" Formula is not satisfied! An error path is [iE, oX, iC, oU, iC, oU, iA, oV] ([iA, oV])* --------------- Formula: (false R (! iC | (true U (oV & X (true U oY))))) "output V, output Y always responds to input C" Formula is not satisfied! An error path is [iC, oS] ([iC, oV, iC, oX, iC, oS, iE, oU, iA, oS])* --------------- Formula: (false R (! (oY & (true U iA)) | ((iE & (! X (! iA U iB) | X (! iA U (iB & (true U oT))))) U iA))) "output T responds to input E, input B between output Y and input A" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iA] ([oS, iE, oW, iA])* --------------- Formula: (! (true U oT) | ((! iA | (! oT U ((oY & ! oT) & X (! oT U oX)))) U oT)) "output Y, output X responds to input A before output T" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA, oT] ([iE, oU, iB, oU, iA, oT])* --------------- Formula: (false R (! (oY & (true U oW)) | (! oS U (oW | ((iB & ! oS) & X (! oS U oX)))))) "input B, output X precedes output S between output Y and output W" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iA, oS, iE, oW] ([iA, oS, iE, oW])* --------------- Formula: (false R (! iB | (true U oT))) "output T always responds to input B" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA, oT, iE, oU, iB, oU] ([iC, oU, iA, oV, iC, oU])* --------------- Formula: (false R (! ((iC & ! iD) & (true U iD)) | (! oT U (oU | iD)))) "output U precedes output T between input C and input D" Formula is satisfied. --------------- Formula: (false R (! (oY & (true U oV)) | (! oX U (oV | ((iB & ! oX) & X (! oX U oS)))))) "input B, output S precedes output X between output Y and output V" Formula is satisfied. --------------- Formula: (false R (! (oX & (true U oU)) | ((! iA | (! oU U (((oV & ! oU) & ! oY) & X ((! oU & ! oY) U oS)))) U oU))) "output V, output S without output Y responds to input A betwen output X and output U" Formula is not satisfied! An error path is [iC, oS, iC, oV, iC, oX, iC, oS, iA, oW, iC, oX, iC, oS, iE, oU] ([iA, oS, iC, oV, iC, oX, iC, oS, iE, oU])* --------------- Formula: (false R (! oZ | (false R (! iE | (oT & X (true U oV)))))) "output T, output V responds to input E after output Z" Formula is satisfied. --------------- Formula: (false R (! oS | ((! ((oY & ! iC) & X (! iC U (oX & ! iC))) U (iC | iB)) | (false R ! (oY & X (true U oX)))))) "input B precedes output Y, output X after output S until input C" Formula is satisfied. --------------- Formula: (false R (! oZ | (false R (! iC | ((oW & ! oS) & X (! oS U oV)))))) "output W, output V without output S responds to input C after output Z" Formula is satisfied. --------------- Formula: (false R (! (iB & (true U iC)) | ((iA & (! X (! iC U iE) | X (! iC U (iE & (true U oT))))) U iC))) "output T responds to input A, input E between input B and input C" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA, oT, iE, oU, iB, oU, iC] ([oU, iA, oV, iC, oU, iC])* --------------- Formula: (false R (! (oW & (true U iD)) | ((! iB | (! iD U (((oX & ! iD) & ! oU) & X ((! iD & ! oU) U oS)))) U iD))) "output X, output S without output U responds to input B betwen output W and input D" Formula is satisfied. --------------- Formula: (false R (oT & (! ! iA | ((! iE | (! iA U (oX & ! iA))) WU iA)))) "output X responds to input E after output T until input A" Formula is not satisfied! An error path is [iC, oS] ([iC, oV, iC, oX, iC, oS, iE, oU, iA, oS])* --------------- Formula: (false R (! (oT & (true U oV)) | (! oS U (oV | ((iC & ! oS) & X (! oS U iA)))))) "input C, input A precedes output S between output T and output V" Formula is satisfied. --------------- Formula: (false R (! oZ | ((! iA | (! oV U (((oX & ! oV) & ! oU) & X ((! oV & ! oU) U oY)))) U (oV | (false R (! iA | ((oX & ! oU) & X (! oU U oY)))))))) "output X, output Y without output U responds to input A after output Z until output V" Formula is satisfied. --------------- Formula: (false R (! iD | (true U ((oS & ! oU) & X (! oU U oW))))) "output S, output W without output U always responds to input D" Formula is satisfied. --------------- Formula: (false R (! oY | ((! ((oX & ! iB) & X (! iB U (oT & ! iB))) U (iB | oZ)) | (false R ! (oX & X (true U oT)))))) "output Z precedes output X, output T after output Y until input B" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iC, oV, iE, oT, iC, oX, iC, oU, iA, oT] ([iE, oU, iB, oU, iA, oT])* --------------- Formula: (false R (! iE | (true U oS))) "output S always responds to input E" Formula is not satisfied! An error path is [iE, oX] ([iC, oU, iA, oT, iE, oU, iC, oX])* --------------- Formula: (false R (! (iC & (true U oS)) | ((! iE | (! oS U (((oX & ! oS) & ! oV) & X ((! oS & ! oV) U oU)))) U oS))) "output X, output U without output V responds to input E betwen input C and output S" Formula is not satisfied! An error path is [iE, oX, iC, oU, iC, oU, iE, oS] ([iC, oS])* --------------- Formula: (false R (! oW | ((! iC | (! oY U (((oZ & ! oY) & ! oT) & X ((! oY & ! oT) U oS)))) U (oY | (false R (! iC | ((oZ & ! oT) & X (! oT U oS)))))))) "output Z, output S without output T responds to input C after output W until output Y" Formula is not satisfied! An error path is [iC, oS, iC, oV, iC, oX, iC, oS, iA, oW, iC] ([oX, iC, oS, iA, oW, iC])* --------------- Formula: (false R (! ((iC & ! oZ) & (true U oZ)) | (! oU U (oV | oZ)))) "output V precedes output U between input C and output Z" Formula is satisfied. --------------- Formula: (! (true U oY) | ((iD & (! X (! oY U iE) | X (! oY U (iE & (true U oS))))) U oY)) "output S responds to input D, input E before output Y" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY] ([iA, oS, iE, oW])* --------------- Formula: (false R (! oU | ((! ((oZ & ! iC) & X (! iC U (oS & ! iC))) U (iC | oW)) | (false R ! (oZ & X (true U oS)))))) "output W precedes output Z, output S after output U until input C" Formula is satisfied. --------------- Formula: (false R (! ((oX & ! oS) & (true U oS)) | ((! iE | (! oS U (oW & ! oS))) U oS))) "output W responds to input E between output X and output S" Formula is not satisfied! An error path is [iE, oX, iC, oU, iC, oU, iE, oS] ([iC, oS])* --------------- Formula: (false R (! oW | (false R (! iE | ((oU & ! oY) & X (! oY U oV)))))) "output U, output V without output Y responds to input E after output W" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iC, oV, iA, oW, iE, oY] ([iC, oS])* --------------- Formula: (false R (! oV | (false R (iD & (! X (true U iB) | X (! iB U (iB & (true U oX)))))))) "output X responds to input D, input B after output V" Formula is not satisfied! An error path is [iC, oS, iC, oV] ([iC, oX, iC, oS, iA, oW])* --------------- Formula: ((false R ! iA) | (true U (iA & (! oS WU iB)))) "input B precedes output S after input A" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iA, oS] ([iE, oW, iA, oS])* --------------- Formula: (false R (! iD | (true U oX))) "output X always responds to input D" Formula is satisfied. --------------- Formula: ((false R ! iC) | (! iC U (iC & (! (true U oS) | (! oS U ((iB & ! oS) & X (! oS U oZ))))))) "input B, output Z precedes output S after input C" Formula is not satisfied! An error path is [iC, oS] ([iC, oV, iC, oX, iC, oS, iE, oU, iA, oS])* --------------- Formula: (false R (! (iD & (true U iA)) | (! ((oX & ! iA) & X (! iA U (oW & ! iA))) U (iA | iB)))) "input B precedes output X, output W between input D and input A" Formula is satisfied. --------------- Formula: (false R (! iE | (true U oT))) "output T always responds to input E" Formula is not satisfied! An error path is [iE, oX, iC, oU] ([iC, oU, iA, oV, iC, oU])* --------------- Formula: ((false R ! iC) | (! iC U (iC & (! (true U (oT & X (true U oV))) | (! oT U iD))))) "input D precedes output T, output V after input C" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA, oT] ([iE, oU, iB, oU, iC, oU, iA, oV, iC, oU, iA, oT])* --------------- Formula: (false R (! iA | ((iD & (! X (! oX U iC) | X (! oX U (iC & (true U oZ))))) U (oX | (false R (iD & (! X (! oX U iC) | X (! oX U (iC & (true U oZ)))))))))) "output Z responds to input D, input C after input A until output X" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA] ([oT, iE, oU, iB, oU, iA])* --------------- Formula: (false R (oW & (! ! iE | (! oV WU (iB | iE))))) "input B precedes output V after output W until input E" Formula is not satisfied! An error path is [iC, oS] ([iC, oV, iC, oX, iC, oS, iE, oU, iA, oS])* --------------- Formula: (false R (! oW | ((! ((oX & ! iE) & X (! iE U (oV & ! iE))) U (iE | iD)) | (false R ! (oX & X (true U oV)))))) "input D precedes output X, output V after output W until input E" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iC, oV, iA, oW, iA, oT, iC, oX, iC, oU, iC, oU, iA, oV] ([iA, oV])* --------------- Formula: (! (true U oW) | (! oV U (oW | ((iD & ! oV) & X (! oV U iA))))) "input D, input A precedes output V before output W" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iA, oS, iE, oW] ([iA, oS, iE, oW])* --------------- Formula: (false R (! oU | ((! ((oY & ! iB) & X (! iB U (oS & ! iB))) U (iB | iA)) | (false R ! (oY & X (true U oS)))))) "input A precedes output Y, output S after output U until input B" Formula is satisfied. --------------- Formula: (! (true U oU) | (! oV U (oU | ((iB & ! oV) & X (! oV U iA))))) "input B, input A precedes output V before output U" Formula is not satisfied! An error path is [iC, oS, iC, oV, iC, oX, iC, oS, iE, oU] ([iA, oS, iC, oV, iC, oX, iC, oS, iE, oU])* --------------- Formula: (false R (! iE | (true U ((oX & ! oY) & X (! oY U oV))))) "output X, output V without output Y always responds to input E" Formula is not satisfied! An error path is [iE, oX] ([iC, oU, iA, oT, iE, oU, iC, oX])* --------------- Formula: ((false R ! oZ) | (! oZ U (oZ & (! (true U (oY & X (true U oW))) | (! oY U iC))))) "input C precedes output Y, output W after output Z" Formula is satisfied. --------------- Formula: (false R (oT & (! ! iD | (! oY WU (oX | iD))))) "output X precedes output Y after output T until input D" Formula is not satisfied! An error path is [iC, oS] ([iC, oV, iC, oX, iC, oS, iE, oU, iA, oS])* --------------- Formula: (! (true U oW) | ((iD & (! X (! oW U iE) | X (! oW U (iE & (true U oX))))) U oW)) "output X responds to input D, input E before output W" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iA, oS, iE, oW] ([iA, oS, iE, oW])* --------------- Formula: (! (true U iA) | (! ((oX & ! iA) & X (! iA U (oS & ! iA))) U (iA | oY))) "output Y precedes output X, output S before input A" Formula is not satisfied! An error path is [iC, oS, iC, oV, iC, oX, iC, oS, iA] ([oW, iC, oX, iC, oS, iA])* --------------- Formula: (false R (! iB | (false R (! iD | (true U oW))))) "output W responds to input D after input B" Formula is satisfied. --------------- Formula: (false R (iD & (! X (true U iA) | X (true U (iA & (true U oZ)))))) "output Z always responds to input D, input A" Formula is not satisfied! An error path is [iC, oS] ([iC, oV, iC, oX, iC, oS, iE, oU, iA, oS])* --------------- Formula: (false R (! iE | ((iA & (! X (! oT U iD) | X (! oT U (iD & (true U oZ))))) U (oT | (false R (iA & (! X (! oT U iD) | X (! oT U (iD & (true U oZ)))))))))) "output Z responds to input A, input D after input E until output T" Formula is not satisfied! An error path is [iE, oX] ([iC, oU, iA, oT, iE, oU, iC, oX])* --------------- Formula: (! oZ WU iA) "input A always precedes output Z" Formula is satisfied. --------------- Formula: (false R (! iE | (! (true U oU) | (! oU U (oV | ((iB & ! oU) & X (! oU U oY))))))) "input B, output Y precedes output U after input E until output V" Formula is not satisfied! An error path is [iE, oX, iC, oU] ([iA, oT, iE, oU, iB, oU])* --------------- Formula: (false R (oZ & (! ! iD | (! oV WU (oY | iD))))) "output Y precedes output V after output Z until input D" Formula is not satisfied! An error path is [iC, oS] ([iC, oV, iC, oX, iC, oS, iE, oU, iA, oS])* --------------- Formula: (false R (! oZ | ((! iE | (! iD U (((oS & ! iD) & ! oT) & X ((! iD & ! oT) U oY)))) U (iD | (false R (! iE | ((oS & ! oT) & X (! oT U oY)))))))) "output S, output Y without output T responds to input E after output Z until input D" Formula is satisfied. --------------- Formula: (! (true U oW) | (! oX U (oW | ((oS & ! oX) & X (! oX U iC))))) "output S, input C precedes output X before output W" Formula is satisfied. --------------- Formula: (false R (! iA | (false R (iE & (! X (true U iD) | X (! iD U (iD & (true U oV)))))))) "output V responds to input E, input D after input A" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA] ([oT, iE, oU, iB, oU, iA])* --------------- Formula: (false R (! oS | (! (true U oT) | (! oT U (iA | ((oU & ! oT) & X (! oT U oW))))))) "output U, output W precedes output T after output S until input A" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iA, oS, iE, oW, iC, oV, iE, oT] ([iA, oU])* --------------- Formula: (false R (! (oU & (true U oT)) | ((iD & (! X (! oT U iA) | X (! oT U (iA & (true U oW))))) U oT))) "output W responds to input D, input A between output U and output T" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA, oT] ([iE, oU, iB, oU, iA, oT])* --------------- Formula: (! (true U iA) | (! oX U (iE | iA))) "input E precedes output X before input A" Formula is not satisfied! An error path is [iC, oS, iC, oV, iC, oX, iC, oS, iA] ([oW, iC, oX, iC, oS, iA])* --------------- Formula: (false R (! iB | ((! iC | (! oW U ((oV & ! oW) & X (! oW U oZ)))) U (oW | (false R (! iC | (oV & X (true U oZ)))))))) "output V, output Z responds to input C after input B until output W" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA, oT, iE, oU, iB, oU, iC] ([oU, iA, oV, iC, oU, iC])* --------------- Formula: (false R (! iA | (false R (! iD | (true U oW))))) "output W responds to input D after input A" Formula is satisfied. --------------- Formula: (false R (! (iA & (true U oS)) | ((iE & (! X (! oS U iC) | X (! oS U (iC & (true U oY))))) U oS))) "output Y responds to input E, input C between input A and output S" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iA, oS] ([iE, oW, iA, oS])* --------------- Formula: (! oV WU oY) "output Y always precedes output V" Formula is not satisfied! An error path is [iC, oS, iC, oV] ([iC, oX, iC, oS, iA, oW])* --------------- Formula: (! (true U iD) | (! oU U (iD | ((iB & ! oU) & X (! oU U oX))))) "input B, output X precedes output U before input D" Formula is satisfied. --------------- Formula: (false R (! iA | ((! iD | (! iE U ((oS & ! iE) & X (! iE U oY)))) U (iE | (false R (! iD | (oS & X (true U oY)))))))) "output S, output Y responds to input D after input A until input E" Formula is satisfied. --------------- Formula: (false R (! oT | (false R (! iE | (oV & X (true U oS)))))) "output V, output S responds to input E after output T" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA, oT, iE] ([oU, iB, oU, iA, oT, iE])* --------------- Formula: (false R (! ((oW & ! iB) & (true U iB)) | (! oT U (oU | iB)))) "output U precedes output T between output W and input B" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iC, oV, iA, oW, iA, oT, iB] ([oU, iA, oT, iE, oU, iB])* --------------- Formula: (false R (! iC | (true U ((oW & ! oU) & X (! oU U oT))))) "output W, output T without output U always responds to input C" Formula is not satisfied! An error path is [iC, oS] ([iC, oV, iC, oX, iC, oS, iE, oU, iA, oS])* --------------- Formula: (false R (! (iB & (true U oY)) | (! ((oX & ! oY) & X (! oY U (oS & ! oY))) U (oY | iE)))) "input E precedes output X, output S between input B and output Y" Formula is satisfied. --------------- Formula: (false R (! iA | (true U ((oU & ! oZ) & X (! oZ U oY))))) "output U, output Y without output Z always responds to input A" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA] ([oT, iE, oU, iB, oU, iA])* --------------- Formula: (false R (! (iB & (true U iC)) | (! oT U (iC | ((oZ & ! oT) & X (! oT U oY)))))) "output Z, output Y precedes output T between input B and input C" Formula is not satisfied! An error path is [iE, oX, iC, oU, iA, oT, iE, oU, iB, oU, iA, oT, iE, oU, iC] ([oX, iC, oU, iA, oT, iE, oU, iC])* --------------- Formula: (! (true U oX) | ((iA & (! X (! oX U iB) | X (! oX U (iB & (true U oV))))) U oX)) "output V responds to input A, input B before output X" Formula is not satisfied! An error path is [iE, oX] ([iC, oU, iA, oT, iE, oU, iC, oX])* --------------- Formula: (! (true U oZ) | (! oZ U ((oU & ! oZ) & X (! oZ U oX)))) "output U, output X always precedes output Z" Formula is satisfied. --------------- Formula: (! (true U oU) | (! oU U ((oT & ! oU) & X (! oU U oZ)))) "output T, output Z always precedes output U" Formula is not satisfied! An error path is [iE, oX, iC, oU] ([iA, oT, iE, oU, iB, oU])* --------------- Formula: (! (true U iC) | (! oU U (iC | ((oS & ! oU) & X (! oU U iD))))) "output S, input D precedes output U before input C" Formula is satisfied. --------------- Formula: ((false R ! iE) | (true U (iE & (! oW WU oT)))) "output T precedes output W after input E" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iA, oS, iE, oW] ([iA, oS, iE, oW])* --------------- Formula: (! (true U iA) | (! ((oU & ! iA) & X (! iA U (oW & ! iA))) U (iA | oZ))) "output Z precedes output U, output W before input A" Formula is satisfied. --------------- Formula: (! (true U oS) | ((! iE | (! oS U ((oV & ! oS) & X (! oS U oY)))) U oS)) "output V, output Y responds to input E before output S" Formula is not satisfied! An error path is [iE, oX, iC, oU, iC, oU, iE, oS] ([iC, oS])* --------------- Formula: ((false R ! iB) | (true U (iB & (! oZ WU iD)))) "input D precedes output Z after input B" Formula is satisfied. --------------- Formula: (! (true U (oY & X (true U oW))) | (! oY U iE)) "input E always precedes output Y, output W" Formula is not satisfied! An error path is [iC, oS, iC, oV, iA, oY, iA, oS, iE, oW] ([iA, oS, iE, oW])* --------------- Formula: (false R (! oZ | (false R (! iE | (true U oY))))) "output Y responds to input E after output Z" Formula is satisfied. --------------- Formula: (false R (! iD | ((! ((oW & ! iC) & X (! iC U (oZ & ! iC))) U (iC | iB)) | (false R ! (oW & X (true U oZ)))))) "input B precedes output W, output Z after input D until input C" Formula is satisfied. --------------- 35 constraints satisfied, 65 unsatisfied.