Reachability problems: =============================== error_1 reachable via input sequence [G, B, J, J, D, J] --------------- error_3 reachable via input sequence [G, B, J, C, H, A] --------------- error_5 reachable via input sequence [G, B, J, C, J, D] --------------- error_6 reachable via input sequence [G, B, J, C, H, I] --------------- error_12 reachable via input sequence [G, B, J, C, H, F] --------------- error_17 reachable via input sequence [G, B, J, J, G, H] --------------- error_20 reachable via input sequence [G, B, J, C, J, B] --------------- error_24 reachable via input sequence [G, B, J, J, D, E] --------------- error_26 reachable via input sequence [G, B, J, J, J, C] --------------- error_30 reachable via input sequence [G, B, J, C, H, B] --------------- error_32 reachable via input sequence [G, B, J, J, G, E] --------------- error_33 reachable via input sequence [G, B, J, J, D, A] --------------- error_37 reachable via input sequence [G, B, J, J, D, I] --------------- error_38 reachable via input sequence [G, B, J, J, D, B] --------------- error_39 reachable via input sequence [G, B, J, C, J, I] --------------- error_46 reachable via input sequence [G, B, J, J, J, E] --------------- error_49 reachable via input sequence [G, B, J, J, G, A] --------------- error_51 reachable via input sequence [G, B, J, J, G, G] --------------- error_53 reachable via input sequence [G, B, J, C, J, E] --------------- error_56 reachable via input sequence [G, B, J, C, H, G] --------------- error_66 reachable via input sequence [G, B, J, C, J, H] --------------- error_69 reachable via input sequence [G, B, J, J, G, J] --------------- error_71 reachable via input sequence [G, B, J, J, D, H] --------------- error_72 reachable via input sequence [G, B, J, C, H, C] --------------- error_75 reachable via input sequence [G, B, J, J, J, A] --------------- error_79 reachable via input sequence [G, B, J, J, G, D] --------------- error_80 reachable via input sequence [G, B, J, C, H, H] --------------- error_83 reachable via input sequence [G, B, J, J, J, D] --------------- error_85 reachable via input sequence [G, B, J, C, J, F] --------------- error_87 reachable via input sequence [G, B, J, J, G, I] --------------- error_88 reachable via input sequence [G, B, J, J, J, I] --------------- error_91 reachable via input sequence [G, B, J, C, H, E] --------------- error_92 reachable via input sequence [G, B, J, C, J, G] --------------- error_93 reachable via input sequence [G, B, J, J, G, B] --------------- error_96 reachable via input sequence [G, B, J, C, H, D] --------------- All other errors unreachable LTL problems: =============================== Formula: (! (true U oV) | (! oV U ((oY & ! oV) & X (! oV U oQ)))) "output Y, output Q always precedes output V" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iF, oQ, iI, oV] ([iC, oU, iD, oQ, iF, oQ, iI, oV])* --------------- Formula: (! (true U oY) | (! ((oX & ! oY) & X (! oY U (oZ & ! oY))) U (oY | oT))) "output T precedes output X, output Z before output Y" Formula is satisfied. --------------- Formula: (false R (! (iG & (true U oO)) | (! oS U (oO | ((oU & ! oS) & X (! oS U oV)))))) "output U, output V precedes output S between input G and output O" Formula is satisfied. --------------- Formula: (false R (! iB | (false R (! iE | ((oV & ! oP) & X (! oP U oU)))))) "output V, output U without output P responds to input E after input B" Formula is satisfied. --------------- Formula: (false R (! (oP & (true U iI)) | (! oZ U (iI | ((oW & ! oZ) & X (! oZ U iE)))))) "output W, input E precedes output Z between output P and input I" Formula is satisfied. --------------- Formula: (false R (! iC | (false R (! iF | (oR & X (true U oT)))))) "output R, output T responds to input F after input C" Formula is not satisfied! An error path is [iE, oZ, iA, oQ, iG, oY, iC, oW, iF] ([oX, iH, oY, iC, oW, iF])* --------------- Formula: (false R (! iH | ((! iD | (! oQ U (((oP & ! oQ) & ! oV) & X ((! oQ & ! oV) U oR)))) U (oQ | (false R (! iD | ((oP & ! oV) & X (! oV U oR)))))))) "output P, output R without output V responds to input D after input H until output Q" Formula is not satisfied! An error path is [iA, oZ, iH, oX, iI, oT, iD] ([oW, iH, oQ, iB, oX, iB, oX, iI, oT, iD])* --------------- Formula: (false R (! oP | (false R (! iI | (oQ & X (true U oS)))))) "output Q, output S responds to input I after output P" Formula is not satisfied! An error path is [iE, oZ, iB, oP, iC, oX, iD, oT, iI, oV] ([iD, oV])* --------------- Formula: (false R (iD & (! ! iH | (! oP WU (iG | iH))))) "input G precedes output P after input D until input H" Formula is not satisfied! An error path is [iA, oZ] ([iH, oX, iG, oP, iA, oX, iG, oX, iJ, oT])* --------------- Formula: (! (true U oO) | (! oO U ((iE & ! oO) & X (! oO U oW)))) "input E, output W always precedes output O" Formula is satisfied. --------------- Formula: (false R (! (iF & (true U oT)) | ((! iJ | (! oT U ((oQ & ! oT) & X (! oT U oV)))) U oT))) "output Q, output V responds to input J between input F and output T" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iF, oQ, iF, oS, iB, oV, iJ, oQ, iF, oQ, iA, oT] ([iA, oY, iH, oT])* --------------- Formula: ((false R ! iD) | (! iD U (iD & (! (true U oR) | (! oR U ((oY & ! oR) & X (! oR U oQ))))))) "output Y, output Q precedes output R after input D" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iJ, oU, iG, oX, iF, oR] ([iA, oQ, iJ, oU, iG, oX, iF, oR])* --------------- Formula: (false R (! iE | (true U oT))) "output T always responds to input E" Formula is not satisfied! An error path is [iE, oZ, iA, oQ] ([iG, oY, iC, oW, iF, oX, iB, oQ])* --------------- Formula: (false R (! iG | (true U (oQ & X (true U oO))))) "output Q, output O always responds to input G" Formula is not satisfied! An error path is [iA, oZ, iH, oX, iG] ([oP, iA, oX, iA, oP, iD, oT, iB, oX, iG])* --------------- Formula: (false R (! oQ | ((iC & (! X (! oS U iF) | X (! oS U (iF & (true U oY))))) U (oS | (false R (iC & (! X (! oS U iF) | X (! oS U (iF & (true U oY)))))))))) "output Y responds to input C, input F after output Q until output S" Formula is not satisfied! An error path is [iA, oZ, iD, oQ] ([iF, oQ, iA, oT, iA, oY, iJ, oQ])* --------------- Formula: (false R (! iH | (true U oX))) "output X always responds to input H" Formula is not satisfied! An error path is [iE, oZ, iH, oY] ([iB, oU, iB, oW, iA, oY, iB, oY])* --------------- Formula: ((false R ! oO) | (! oO U (oO & (! (true U (oZ & X (true U oW))) | (! oZ U iB))))) "input B precedes output Z, output W after output O" Formula is satisfied. --------------- Formula: (false R (! iE | (false R (! iJ | (oX & X (true U oV)))))) "output X, output V responds to input J after input E" Formula is not satisfied! An error path is [iE, oZ, iH, oY, iB, oU, iF, oR, iJ] ([oV, iA, oR, iJ])* --------------- Formula: (false R (oX & (! ! oY | ((! iE | (! oY U (oV & ! oY))) WU oY)))) "output V responds to input E after output X until output Y" Formula is not satisfied! An error path is [iA, oZ] ([iH, oX, iG, oP, iA, oX, iG, oX, iJ, oT])* --------------- Formula: (false R (! (oZ & (true U oW)) | (! oV U (oW | ((oP & ! oV) & X (! oV U oQ)))))) "output P, output Q precedes output V between output Z and output W" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iJ, oU, iB, oT, iG, oV, iJ, oT, iB, oW] ([iC, oQ, iJ, oU, iB, oT, iB, oW])* --------------- Formula: (false R (! iG | ((! iI | (! iD U ((oX & ! iD) & X (! iD U oV)))) U (iD | (false R (! iI | (oX & X (true U oV)))))))) "output X, output V responds to input I after input G until input D" Formula is not satisfied! An error path is [iG, oT, iB, oW, iI, oR] ([iC, oQ, iC, oP, iG, oT])* --------------- Formula: (! oS WU oU) "output U always precedes output S" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iF, oQ, iF, oS] ([iB, oV, iA, oQ, iF, oS])* --------------- Formula: (! (true U oZ) | (! oS U (oZ | ((oU & ! oS) & X (! oS U iG))))) "output U, input G precedes output S before output Z" Formula is satisfied. --------------- Formula: (! oP WU iG) "input G always precedes output P" Formula is not satisfied! An error path is [iE, oZ, iB, oP] ([iC, oX, iA, oT, iB, oT, iH, oP])* --------------- Formula: ((false R ! iJ) | (! iJ U (iJ & (! (true U (oW & X (true U oU))) | (! oW U oO))))) "output O precedes output W, output U after input J" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iJ, oU, iB, oT, iB, oW] ([iC, oQ, iJ, oU, iB, oT, iB, oW])* --------------- Formula: ((false R ! iD) | (true U (iD & (! oR WU oZ)))) "output Z precedes output R after input D" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iJ, oU, iG, oX, iF, oR] ([iA, oQ, iJ, oU, iG, oX, iF, oR])* --------------- Formula: (! (true U oO) | ((! iG | (! oO U (oZ & ! oO))) U oO)) "output Z responds to input G before output O" Formula is satisfied. --------------- Formula: (false R (iI & (! X (true U iF) | X (true U (iF & (true U oV)))))) "output V always responds to input I, input F" Formula is not satisfied! An error path is [iA, oZ] ([iH, oX, iG, oP, iA, oX, iG, oX, iJ, oT])* --------------- Formula: (false R (! ((iC & ! oV) & (true U oV)) | (! oZ U (oQ | oV)))) "output Q precedes output Z between input C and output V" Formula is satisfied. --------------- Formula: (! (true U oY) | (! oP U (oY | ((iD & ! oP) & X (! oP U oO))))) "input D, output O precedes output P before output Y" Formula is not satisfied! An error path is [iA, oZ, iH, oX, iI, oT, iI, oP, iF, oY] ([iG, oU, iF, oY])* --------------- Formula: (false R (! iC | (true U ((oY & ! oV) & X (! oV U oZ))))) "output Y, output Z without output V always responds to input C" Formula is not satisfied! An error path is [iE, oZ, iB, oP, iC] ([oX, iA, oT, iB, oT, iH, oP, iC])* --------------- Formula: (! (true U oP) | (! ((oW & ! oP) & X (! oP U (oZ & ! oP))) U (oP | oT))) "output T precedes output W, output Z before output P" Formula is satisfied. --------------- Formula: (false R (! oY | ((! ((oT & ! iD) & X (! iD U (oO & ! iD))) U (iD | oZ)) | (false R ! (oT & X (true U oO)))))) "output Z precedes output T, output O after output Y until input D" Formula is satisfied. --------------- Formula: (false R (! (oR & (true U oV)) | (! ((oU & ! oV) & X (! oV U (oQ & ! oV))) U (oV | iJ)))) "input J precedes output U, output Q between output R and output V" Formula is not satisfied! An error path is [iE, oZ, iH, oY, iB, oU, iF, oR, iA, oY, iC, oU, iC, oQ, iB, oV] ([iB, oV])* --------------- Formula: (false R (! (oR & (true U oV)) | (! ((oX & ! oV) & X (! oV U (oY & ! oV))) U (oV | iI)))) "input I precedes output X, output Y between output R and output V" Formula is not satisfied! An error path is [iB, oW, iA, oT, iB, oU, iG, oR, iG, oX, iH, oU, iD, oY, iJ, oV] ([iD, oV])* --------------- Formula: (! (true U oR) | (! oV U (iF | oR))) "input F precedes output V before output R" Formula is not satisfied! An error path is [iA, oZ, iB, oY, iC, oT, iI, oV, iD, oR, iB, oT] ([iB, oQ, iJ, oU, iB, oT, iC, oX])* --------------- Formula: (! (true U (oT & X (true U oU))) | (! oT U iF)) "input F always precedes output T, output U" Formula is not satisfied! An error path is [iB, oW, iA, oT, iB, oU] ([iD, oY, iB, oS, iH, oU])* --------------- Formula: (! (true U (oT & X (true U oZ))) | (! oT U iJ)) "input J always precedes output T, output Z" Formula is satisfied. --------------- Formula: (false R (! (iF & (true U oY)) | ((! iJ | (! oY U (((oU & ! oY) & ! oW) & X ((! oY & ! oW) U oO)))) U oY))) "output U, output O without output W responds to input J betwen input F and output Y" Formula is not satisfied! An error path is [iE, oZ, iH, oY, iB, oU, iF, oR, iJ, oV, iC, oY] ([iB, oU, iB, oW, iA, oY, iB, oY])* --------------- Formula: (false R (! oT | (false R (iF & (! X (true U iE) | X (! iE U (iE & (true U oS)))))))) "output S responds to input F, input E after output T" Formula is not satisfied! An error path is [iB, oW, iA, oT] ([iB, oU, iG, oR, iA, oU, iD, oT])* --------------- Formula: (false R (! (oR & (true U iB)) | (! oW U (iB | ((oQ & ! oW) & X (! oW U oX)))))) "output Q, output X precedes output W between output R and input B" Formula is not satisfied! An error path is [iA, oZ, iH, oX, iJ, oY, iA, oR, iH, oW, iC, oW, iB] ([oY, iB, oU, iB, oW, iH, oV, iB])* --------------- Formula: (false R (! iA | ((! iB | (! iE U (((oP & ! iE) & ! oT) & X ((! iE & ! oT) U oR)))) U (iE | (false R (! iB | ((oP & ! oT) & X (! oT U oR)))))))) "output P, output R without output T responds to input B after input A until input E" Formula is not satisfied! An error path is [iB, oW, iA, oT, iB] ([oU, iG, oR, iA, oU, iD, oT, iB])* --------------- Formula: (false R (! iG | (true U ((oU & ! oY) & X (! oY U oP))))) "output U, output P without output Y always responds to input G" Formula is not satisfied! An error path is [iA, oZ, iH, oX, iG] ([oP, iA, oX, iG, oX, iJ, oT, iH, oX, iI, oT, iG, oY, iI, oR, iF, oR, iG])* --------------- Formula: (! (true U oW) | (! oW U ((oR & ! oW) & X (! oW U oV)))) "output R, output V always precedes output W" Formula is not satisfied! An error path is [iB, oW, iA, oT] ([iB, oU, iG, oR, iA, oU, iD, oT])* --------------- Formula: (false R (iH & (! X (true U iJ) | X (true U (iJ & (true U oX)))))) "output X always responds to input H, input J" Formula is not satisfied! An error path is [iA, oZ] ([iH, oX, iG, oP, iA, oX, iG, oX, iJ, oT])* --------------- Formula: (false R (! (oR & (true U iH)) | (! oZ U (iH | ((iA & ! oZ) & X (! oZ U iE)))))) "input A, input E precedes output Z between output R and input H" Formula is satisfied. --------------- Formula: (false R (! ((iF & ! iI) & (true U iI)) | (! oU U (oT | iI)))) "output T precedes output U between input F and input I" Formula is not satisfied! An error path is [iE, oZ, iH, oY, iB, oU, iF, oR, iB, oU, iI] ([oY, iB, oU, iF, oR, iB, oU, iI])* --------------- Formula: (false R (! oT | ((! ((oW & ! iA) & X (! iA U (oU & ! iA))) U (iA | oS)) | (false R ! (oW & X (true U oU)))))) "output S precedes output W, output U after output T until input A" Formula is not satisfied! An error path is [iG, oT, iB, oW, iC, oQ, iJ, oU] ([iH, oX, iG, oP])* --------------- Formula: ((false R ! iA) | (! iA U (iA & (! (true U (oX & X (true U oO))) | (! oX U oW))))) "output W precedes output X, output O after input A" Formula is satisfied. --------------- Formula: (false R (iF & (! X (true U iI) | X (true U (iI & (true U oP)))))) "output P always responds to input F, input I" Formula is not satisfied! An error path is [iA, oZ] ([iH, oX, iG, oP, iA, oX, iG, oX, iJ, oT])* --------------- Formula: (! (true U oU) | (! oZ U (oP | oU))) "output P precedes output Z before output U" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iJ, oU] ([iB, oT, iB, oW, iJ, oU])* --------------- Formula: (false R (iA & (! ! oR | (! oV WU (iD | oR))))) "input D precedes output V after input A until output R" Formula is not satisfied! An error path is [iA, oZ] ([iH, oX, iG, oP, iA, oX, iG, oX, iJ, oT])* --------------- Formula: (false R (! iH | (false R (! iF | ((oZ & ! oP) & X (! oP U oR)))))) "output Z, output R without output P responds to input F after input H" Formula is not satisfied! An error path is [iE, oZ, iH, oY, iB, oU, iF] ([oR, iA, oY, iC, oU, iF])* --------------- Formula: (false R (iB & (! X (true U iE) | X (true U (iE & (true U oU)))))) "output U always responds to input B, input E" Formula is not satisfied! An error path is [iA, oZ] ([iH, oX, iG, oP, iA, oX, iG, oX, iJ, oT])* --------------- Formula: (false R (! oU | ((! ((oR & ! iD) & X (! iD U (oT & ! iD))) U (iD | oZ)) | (false R ! (oR & X (true U oT)))))) "output Z precedes output R, output T after output U until input D" Formula is not satisfied! An error path is [iB, oW, iA, oT, iB, oU, iG, oR, iF, oR, iA, oT] ([iB, oU, iG, oR, iA, oU, iD, oT])* --------------- Formula: (false R (! oZ | ((! iI | (! iC U ((oT & ! iC) & X (! iC U oQ)))) U (iC | (false R (! iI | (oT & X (true U oQ)))))))) "output T, output Q responds to input I after output Z until input C" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iI] ([oX, iI, oX, iG, oS, iJ, oQ, iI])* --------------- Formula: (false R (! iE | (false R (! iD | (oY & X (true U oS)))))) "output Y, output S responds to input D after input E" Formula is not satisfied! An error path is [iE, oZ, iB, oP, iC, oX, iD] ([oT, iC, oX, iA, oP, iC, oX, iD])* --------------- Formula: (false R (! oV | ((iE & (! X (! oQ U iD) | X (! oQ U (iD & (true U oW))))) U (oQ | (false R (iE & (! X (! oQ U iD) | X (! oQ U (iD & (true U oW)))))))))) "output W responds to input E, input D after output V until output Q" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iF, oQ, iI, oV] ([iC, oU, iD, oQ, iF, oQ, iI, oV])* --------------- Formula: (false R (! iB | (true U oW))) "output W always responds to input B" Formula is not satisfied! An error path is [iE, oZ, iB, oP] ([iC, oX, iA, oT, iB, oT, iH, oP])* --------------- Formula: (! (true U (oP & X (true U oV))) | (! oP U oT)) "output T always precedes output P, output V" Formula is not satisfied! An error path is [iE, oZ, iB, oP, iC, oX, iD, oT, iI, oV] ([iD, oV])* --------------- Formula: (false R (! (oR & (true U oS)) | ((! iB | (! oS U ((oY & ! oS) & X (! oS U oX)))) U oS))) "output Y, output X responds to input B between output R and output S" Formula is not satisfied! An error path is [iA, oZ, iH, oX, iJ, oY, iA, oR, iB, oS] ([iB, oX, iJ, oY, iA, oR, iB, oS])* --------------- Formula: (false R (! ((iC & ! iI) & (true U iI)) | (! oU U (iB | iI)))) "input B precedes output U between input C and input I" Formula is not satisfied! An error path is [iG, oT, iB, oW, iC, oQ, iG, oS, iH, oU, iI, oP] ([iD, oX, iG, oS])* --------------- Formula: (false R (! iH | (true U oQ))) "output Q always responds to input H" Formula is not satisfied! An error path is [iA, oZ, iH] ([oX, iG, oP, iA, oX, iG, oX, iJ, oT, iH])* --------------- Formula: (! (true U oO) | (! ((oT & ! oO) & X (! oO U (oQ & ! oO))) U (oO | iE))) "input E precedes output T, output Q before output O" Formula is satisfied. --------------- Formula: (! (true U iB) | ((! iH | (! iB U (oY & ! iB))) U iB)) "output Y responds to input H before input B" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iF, oQ, iH, oQ, iC, oX, iB] ([oQ, iC, oX, iB])* --------------- Formula: (false R (iB & (! X (true U iE) | X (true U (iE & (true U oR)))))) "output R always responds to input B, input E" Formula is not satisfied! An error path is [iA, oZ] ([iH, oX, iG, oP, iA, oX, iG, oX, iJ, oT])* --------------- Formula: (! (true U iA) | (! oX U (oS | iA))) "output S precedes output X before input A" Formula is not satisfied! An error path is [iE, oZ, iB, oP, iC, oX, iA] ([oT, iB, oT, iH, oP, iC, oX, iA])* --------------- Formula: (! (true U iH) | ((! iA | (! iH U (((oT & ! iH) & ! oZ) & X ((! iH & ! oZ) U oU)))) U iH)) "output T, output U without output Z responds to input A before input H" Formula is not satisfied! An error path is [iA, oZ, iH] ([oX, iG, oP, iA, oX, iG, oX, iJ, oT, iH])* --------------- Formula: (false R (! (iA & (true U iH)) | (! ((oV & ! iH) & X (! iH U (oS & ! iH))) U (iH | oT)))) "output T precedes output V, output S between input A and input H" Formula is not satisfied! An error path is [iE, oZ, iB, oP, iC, oX, iD, oT, iA, oV, iD, oX, iA, oS, iH] ([oY, iB, oU, iB, oW, iF, oS, iH])* --------------- Formula: (false R (! (oX & (true U iA)) | ((! iF | (! iA U (((oP & ! iA) & ! oW) & X ((! iA & ! oW) U oY)))) U iA))) "output P, output Y without output W responds to input F betwen output X and input A" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iJ, oU, iG, oX, iF, oR, iA] ([oQ, iJ, oU, iG, oX, iF, oR, iA])* --------------- Formula: (false R (oQ & (! ! oR | ((! iD | (! oR U (oY & ! oR))) WU oR)))) "output Y responds to input D after output Q until output R" Formula is not satisfied! An error path is [iA, oZ] ([iH, oX, iG, oP, iA, oX, iG, oX, iJ, oT])* --------------- Formula: (! (true U iJ) | ((! iD | (! iJ U (((oV & ! iJ) & ! oZ) & X ((! iJ & ! oZ) U oU)))) U iJ)) "output V, output U without output Z responds to input D before input J" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iJ] ([oU, iB, oT, iB, oW, iC, oQ, iJ])* --------------- Formula: ((false R ! iE) | (! iE U (iE & (! (true U (oV & X (true U oT))) | (! oV U iB))))) "input B precedes output V, output T after input E" Formula is satisfied. --------------- Formula: ((false R ! iA) | (true U (iA & (! oT WU oX)))) "output X precedes output T after input A" Formula is not satisfied! An error path is [iB, oW, iA, oT] ([iB, oU, iG, oR, iA, oU, iD, oT])* --------------- Formula: (false R (! oR | (false R (! iF | ((oO & ! oX) & X (! oX U oZ)))))) "output O, output Z without output X responds to input F after output R" Formula is not satisfied! An error path is [iB, oW, iA, oT, iB, oU, iG, oR, iF] ([oR, iH, oR, iF])* --------------- Formula: (false R (! iG | (false R (! iE | ((oO & ! oY) & X (! oY U oQ)))))) "output O, output Q without output Y responds to input E after input G" Formula is satisfied. --------------- Formula: (! (true U oR) | ((! iB | (! oR U (((oV & ! oR) & ! oP) & X ((! oR & ! oP) U oZ)))) U oR)) "output V, output Z without output P responds to input B before output R" Formula is not satisfied! An error path is [iB, oW, iA, oT, iG, oR] ([iI, oP, iF, oV, iD, oT, iB, oQ, iF, oQ, iA, oT, iG, oX, iD, oX, iH, oU, iG, oR, iA, oU, iD, oT, iG, oR])* --------------- Formula: (! (true U (oT & X (true U oY))) | (! oT U oU)) "output U always precedes output T, output Y" Formula is not satisfied! An error path is [iA, oZ, iH, oX, iI, oT, iG, oY] ([iC, oT, iD, oQ, iG, oY])* --------------- Formula: (false R (! iI | ((! iB | (! oY U ((oV & ! oY) & X (! oY U oQ)))) U (oY | (false R (! iB | (oV & X (true U oQ)))))))) "output V, output Q responds to input B after input I until output Y" Formula is not satisfied! An error path is [iG, oT, iB, oW, iI, oR, iB] ([oY, iG, oY, iB, oX, iB])* --------------- Formula: (false R (! oS | (false R (! iH | (true U oW))))) "output W responds to input H after output S" Formula is not satisfied! An error path is [iB, oW, iA, oT, iB, oU, iD, oY, iB, oS, iH] ([oU, iD, oY, iB, oS, iH])* --------------- Formula: (! (true U (oZ & X (true U oO))) | (! oZ U iD)) "input D always precedes output Z, output O" Formula is satisfied. --------------- Formula: (false R (! iF | (true U ((oZ & ! oW) & X (! oW U oR))))) "output Z, output R without output W always responds to input F" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iF] ([oQ, iA, oT, iA, oY, iJ, oQ, iF])* --------------- Formula: (false R (! (oU & (true U oQ)) | ((! iF | (! oQ U ((oV & ! oQ) & X (! oQ U oW)))) U oQ))) "output V, output W responds to input F between output U and output Q" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iJ, oU, iG, oX, iF, oR, iA, oQ] ([iF, oQ, iA, oT, iA, oY, iJ, oQ])* --------------- Formula: (! oT WU iF) "input F always precedes output T" Formula is not satisfied! An error path is [iB, oW, iA, oT] ([iB, oU, iG, oR, iA, oU, iD, oT])* --------------- Formula: (false R (oP & (! ! oX | ((! iJ | (! oX U (oQ & ! oX))) WU oX)))) "output Q responds to input J after output P until output X" Formula is not satisfied! An error path is [iA, oZ] ([iH, oX, iG, oP, iA, oX, iG, oX, iJ, oT])* --------------- Formula: (! oX WU oZ) "output Z always precedes output X" Formula is not satisfied! An error path is [iB, oW, iA, oT, iB, oU, iG, oR, iG, oX] ([iA, oX])* --------------- Formula: (false R (! iB | ((! iH | (! oV U (((oZ & ! oV) & ! oW) & X ((! oV & ! oW) U oY)))) U (oV | (false R (! iH | ((oZ & ! oW) & X (! oW U oY)))))))) "output Z, output Y without output W responds to input H after input B until output V" Formula is not satisfied! An error path is [iE, oZ, iH, oY, iB, oU, iB, oW, iH] ([oV, iB, oY, iB, oU, iB, oW, iH])* --------------- Formula: (false R (! ((oW & ! iH) & (true U iH)) | (! oV U (iJ | iH)))) "input J precedes output V between output W and input H" Formula is not satisfied! An error path is [iG, oT, iB, oW, iG, oX, iI, oV, iI, oQ, iH, oT] ([iF, oT, iJ, oT])* --------------- Formula: (false R (! iC | (true U oS))) "output S always responds to input C" Formula is not satisfied! An error path is [iE, oZ, iB, oP, iC] ([oX, iA, oT, iB, oT, iH, oP, iC])* --------------- Formula: (false R (! (iC & (true U oR)) | (! ((oZ & ! oR) & X (! oR U (oO & ! oR))) U (oR | iJ)))) "input J precedes output Z, output O between input C and output R" Formula is satisfied. --------------- Formula: (false R (oO & (! ! oW | ((! iJ | (! oW U (oT & ! oW))) WU oW)))) "output T responds to input J after output O until output W" Formula is not satisfied! An error path is [iA, oZ] ([iH, oX, iG, oP, iA, oX, iG, oX, iJ, oT])* --------------- Formula: (false R (! oY | (false R (! iH | (true U oQ))))) "output Q responds to input H after output Y" Formula is not satisfied! An error path is [iE, oZ, iA, oQ, iG, oY, iC, oW, iH] ([oV, iI, oW, iH])* --------------- Formula: (false R (! oV | ((! ((oU & ! iI) & X (! iI U (oZ & ! iI))) U (iI | oP)) | (false R ! (oU & X (true U oZ)))))) "output P precedes output U, output Z after output V until input I" Formula is satisfied. --------------- Formula: (false R (! oR | (false R (! iE | (oP & X (true U oT)))))) "output P, output T responds to input E after output R" Formula is satisfied. --------------- Formula: (false R (! oY | (false R (! iG | (oV & X (true U oQ)))))) "output V, output Q responds to input G after output Y" Formula is not satisfied! An error path is [iB, oW, iA, oT, iB, oU, iD, oY, iG] ([oQ, iD, oU, iD, oY, iG])* --------------- Formula: (! (true U oX) | ((! iG | (! oX U (oV & ! oX))) U oX)) "output V responds to input G before output X" Formula is not satisfied! An error path is [iA, oZ, iD, oQ, iJ, oU, iG, oX] ([iF, oR, iA, oQ, iJ, oU, iG, oX])* --------------- Formula: (false R (! iE | (true U (oW & X (true U oU))))) "output W, output U always responds to input E" Formula is not satisfied! An error path is [iE, oZ, iA, oQ] ([iG, oY, iC, oW, iF, oX, iB, oQ])* --------------- Formula: ((false R ! oZ) | (true U (oZ & (! oX WU oS)))) "output S precedes output X after output Z" Formula is not satisfied! An error path is [iA, oZ, iH, oX] ([iG, oP, iA, oX, iA, oP, iD, oT, iB, oX])* --------------- Formula: (! (true U oV) | (! ((oY & ! oV) & X (! oV U (oQ & ! oV))) U (oV | iA))) "input A precedes output Y, output Q before output V" Formula is not satisfied! An error path is [iE, oZ, iH, oY, iB, oU, iC, oQ, iB, oV] ([iB, oV])* --------------- Formula: (false R (iG & (! ! oS | ((! iB | (! oS U (oV & ! oS))) WU oS)))) "output V responds to input B after input G until output S" Formula is not satisfied! An error path is [iA, oZ] ([iH, oX, iG, oP, iA, oX, iG, oX, iJ, oT])* --------------- 21 constraints satisfied, 79 unsatisfied.