Reachability problems: =============================== error_0 reachable via input sequence [G, C, G, C, I, A, E] --------------- error_1 reachable via input sequence [G, C, G, C, B, J, E] --------------- error_8 reachable via input sequence [G, C, G, C, I, I, H] --------------- error_9 reachable via input sequence [G, C, G, C, I, A, H] --------------- error_10 reachable via input sequence [G, C, G, C, C, B, D] --------------- error_13 reachable via input sequence [G, C, G, C, I, I, C] --------------- error_20 reachable via input sequence [G, C, G, C, I, A, A] --------------- error_21 reachable via input sequence [G, C, G, C, I, I, E] --------------- error_23 reachable via input sequence [G, C, G, C, C, B, I] --------------- error_24 reachable via input sequence [G, C, G, C, I, I, B] --------------- error_27 reachable via input sequence [G, C, G, C, I, I, I] --------------- error_31 reachable via input sequence [G, C, G, C, I, A, B] --------------- error_33 reachable via input sequence [G, C, G, C, B, J, F] --------------- error_37 reachable via input sequence [G, C, G, C, C, I, J] --------------- error_38 reachable via input sequence [G, C, G, C, C, I, D] --------------- error_39 reachable via input sequence [G, C, G, C, B, J, H] --------------- error_47 reachable via input sequence [G, C, G, C, I, I, F] --------------- error_51 reachable via input sequence [G, C, G, C, I, A, D] --------------- error_54 reachable via input sequence [G, C, G, C, C, I, E] --------------- error_55 reachable via input sequence [G, C, G, C, C, B, H] --------------- error_56 reachable via input sequence [G, C, G, C, C, I, B] --------------- error_59 reachable via input sequence [G, C, G, C, C, I, I] --------------- error_61 reachable via input sequence [G, C, G, C, B, J, J] --------------- error_63 reachable via input sequence [G, C, G, C, I, A, J] --------------- error_65 reachable via input sequence [G, C, G, C, B, J, B] --------------- error_67 reachable via input sequence [G, C, G, C, B, J, G] --------------- error_69 reachable via input sequence [G, C, G, C, C, B, E] --------------- error_71 reachable via input sequence [G, C, G, C, C, I, H] --------------- error_78 reachable via input sequence [G, C, G, C, I, I, D] --------------- error_79 reachable via input sequence [G, C, G, C, C, B, F] --------------- error_81 reachable via input sequence [G, C, G, C, B, J, I] --------------- error_83 reachable via input sequence [G, C, G, C, I, A, I] --------------- error_85 reachable via input sequence [G, C, G, C, C, I, F] --------------- error_87 reachable via input sequence [G, C, G, C, I, A, G] --------------- error_89 reachable via input sequence [G, C, G, C, B, J, D] --------------- error_91 reachable via input sequence [G, C, G, C, C, B, J] --------------- error_96 reachable via input sequence [G, C, G, C, I, A, C] --------------- 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 [iG, oV] ([iC, oY, iF, oS, iG, oS, iD, oO, iI, oT, 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 not satisfied! An error path is [iF, oQ, iD, oW, iD, oX, iJ, oO, iB, oU, iG, oZ, iD, oW, iA, oX, iC, oY] ([iA, oQ, iB, oX, iB, oQ, iD, oW, iA, oX, iC, oY])* --------------- 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 not satisfied! An error path is [iF, oQ, iG, oU, iC, oS, iI, oO] ([iB, oW, iB, oW, iI, oO])* --------------- 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 [iG, oV, iC, oY, iF] ([oS, iG, oS, iD, oO, iG, oO, iG, oY, 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 satisfied. --------------- 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 satisfied. --------------- 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- Formula: (! (true U oO) | (! oO U ((iE & ! oO) & X (! oO U oW)))) "input E, output W always precedes output O" Formula is not satisfied! An error path is [iF, oQ, iG, oU, iB, oO] ([iG, oX, iJ, oW, iA, oW, iB, oO])* --------------- 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 [iF, oQ, iI, oV, iF, oU, iI, oY, iJ, oO, iJ, oT] ([iA, oY, iJ, oO, iJ, 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 [iF, oQ, iD, oW, iD, oX, iI, oR] ([iJ, oS, iB, oT, iI, oR])* --------------- Formula: (false R (! iE | (true U oT))) "output T always responds to input E" Formula is satisfied. --------------- 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 [iG, oV] ([iC, oY, iF, oS, iG, oS, iJ, oQ, iG, oY, iI, oV])* --------------- 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- Formula: (false R (! iH | (true U oX))) "output X always responds to input H" Formula is satisfied. --------------- 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 not satisfied! An error path is [iF, oQ, iD, oW, iI, oZ, iB, oO, iI, oY, iG, oZ] ([iB, oO, iI, oY, iC, oO, iG, oW, iI, oZ, iB, oO, iI, oY, iG, oZ])* --------------- 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 satisfied. --------------- 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- 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 [iF, oQ, iI, oV, iF, oU, iC, oS, iB, oU, iF, oZ, iC, oV, iF, oU, iI, oY, iC, oW] ([iF, oX, iD, oV, iF, oU, iI, oY, iC, 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 [iF, oQ, iD, oW, iG, oX, iI] ([oX, iI, oU, iG, oS, iF, oX, iI])* --------------- Formula: (! oS WU oU) "output U always precedes output S" Formula is not satisfied! An error path is [iG, oV, iC, oY, iF, oS] ([iG, oS, iD, oO, iG, oO, iD, 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 not satisfied! An error path is [iF, oQ, iG, oU, iC, oS, iF, oU, iI, oZ] ([iA, oZ, iG, oS, iF, oU, iI, oZ])* --------------- Formula: (! oP WU iG) "input G always precedes output P" Formula is satisfied. --------------- 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 [iF, oQ, iD, oW, iG, oX, iI, oX, iJ, oW] ([iF, oQ, iJ, oW, iI, oX, iI, oU, iG, oS, iD, oX, iJ, 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 [iF, oQ, iD, oW, iD, oX, iI, oR] ([iJ, oS, iB, oT, iI, oR])* --------------- Formula: (! (true U oO) | ((! iG | (! oO U (oZ & ! oO))) U oO)) "output Z responds to input G before output O" Formula is not satisfied! An error path is [iF, oQ, iG, oU, iB, oO] ([iG, oX, iJ, oW, iA, oW, iB, oO])* --------------- 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- 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 not satisfied! An error path is [iF, oQ, iI, oV, iF, oU, iC, oS, iB, oU, iF, oZ, iC, oV] ([iF, oU, iC, oS, iB, oU, iF, oZ, iC, oV])* --------------- 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 satisfied. --------------- 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 [iG, oV, iC] ([oY, iF, oS, iG, oS, iD, oO, iI, oT, iI, oV, 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 not satisfied! An error path is [iG, oV, iC, oY, iG, oO, iG, oW, iI, oO, iG, oT, iG, oO] ([iB, oW, iG, oO, iG, oW, iI, oO])* --------------- 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 [iF, oQ, iD, oW, iG, oX, iI, oX, iC, oV, iG, oR, iC, oU, iI, oQ, iI, oV] ([iF, oU, iC, oS, iB, oU, iF, oZ, iC, 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 [iG, oV, iC, oY, iG, oO, iC, oR, iB, oX, iJ, oS, iA, oU, iJ, oY, iB, oV] ([iG, oU, iC, oS, iI, oO, iF, oY, iB, 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 [iG, oV, iC, oY, iG, oO, iB, oR] ([iC, oV, iI, oU, iI, oO, iB, oR])* --------------- 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 [iG, oV, iC, oY, iG, oO, iC, oR, iI, oW, iI, oT, iA, oU] ([iB, oY, iF, oS, iG, oS, iJ, oQ, iG, oY])* --------------- Formula: (! (true U (oT & X (true U oZ))) | (! oT U iJ)) "input J always precedes output T, output Z" Formula is not satisfied! An error path is [iF, oQ, iD, oW, iD, oX, iF, oT, iD, oT, iA, oY, iA, oQ, iD, oW, iI, oZ] ([iB, oO, iI, oY, iG, oZ, iD, oZ])* --------------- 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 [iF, oQ, iI, oV, iF, oU, iJ, oO, iG, oR, iD, oY] ([iB, oO, iG, oR, iD, 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 [iF, oQ, iD, oW, iD, oX, iF, oT] ([iD, oT, iA, oY, iA, oQ, iD, oW, iD, oX, iF, 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 [iG, oV, iC, oY, iG, oO, iB, oR, iG, oW, iG, oY, iB] ([oR, iG, oW, iG, oY, 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 [iF, oQ, iD, oW, iA, oX, iC, oY, iB] ([oU, iC, oQ, iD, oY, 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 [iG, oV] ([iC, oY, iF, oS, iG, oS, iD, oO, iI, oT, iI, oV])* --------------- 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 [iF, oQ, iD, oW] ([iA, oX, iC, oY, iB, oU, iA, oR, iF, oW])* --------------- 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- 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 [iF, oQ, iG, oU, iC, oS, iI] ([oO, iB, oW, iB, oW, iG, oS, 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 [iF, oQ, iG, oU, iC, oS, iI, oO, iI, oT, iG, oX, iC, oO, iB, oW, iF, oZ, iI, oU] ([iB, oO, iG, oX, iJ, oW, iB, oO, iA, oU])* --------------- 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 not satisfied! An error path is [iF, oQ, iD, oW, iA, oX] ([iC, oY, iJ, oO, iA, oT, iB, oY, iA, oQ, iB, oX, iB, oQ, iD, oW, iA, oX])* --------------- 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- Formula: (! (true U oU) | (! oZ U (oP | oU))) "output P precedes output Z before output U" Formula is not satisfied! An error path is [iF, oQ, iD, oW, iA, oX, iD, oY, iB, oQ, iJ, oZ, iG, oU] ([iB, 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- 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 satisfied. --------------- 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- 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 [iF, oQ, iI, oV, iF, oU, iJ, oO, iG, oR, iA, oT] ([iB, oO, iG, oR, iA, 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 [iF, oQ, iD, oW, iI, oZ, iB, oO, iI] ([oY, iG, oZ, iB, oO, 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 satisfied. --------------- 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 [iG, oV] ([iC, oY, iF, oS, iG, oS, iD, oO, iI, oT, iI, oV])* --------------- Formula: (false R (! iB | (true U oW))) "output W always responds to input B" Formula is not satisfied! An error path is [iF, oQ, iD, oW, iI, oZ, iB] ([oO, iI, oY, iG, oZ, iD, oZ, iB])* --------------- Formula: (! (true U (oP & X (true U oV))) | (! oP U oT)) "output T always precedes output P, output V" Formula is satisfied. --------------- 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 [iG, oV, iC, oY, iG, oO, iC, oR, iB, oX, iJ, oS] ([iA, oU, iG, oU, iC, oS, iF, oU, iI, oZ, iB, oY, iB, oU, iI, oY, iG, oO, iC, oR, iB, oX, iJ, 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 [iF, oQ, iG, oU, iC, oS, iF, oU, iI] ([oZ, iA, oZ, iG, oS, iF, oU, iI])* --------------- Formula: (false R (! iH | (true U oQ))) "output Q always responds to input H" Formula is satisfied. --------------- 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 not satisfied! An error path is [iF, oQ, iD, oW, iD, oX, iF, oT, iD, oT, iA, oY, iA, oQ, iG, oU, iB, oO] ([iG, oX, iJ, oW, iA, oW, iB, oO])* --------------- Formula: (! (true U iB) | ((! iH | (! iB U (oY & ! iB))) U iB)) "output Y responds to input H before input B" Formula is satisfied. --------------- 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- Formula: (! (true U iA) | (! oX U (oS | iA))) "output S precedes output X before input A" Formula is not satisfied! An error path is [iF, oQ, iD, oW, iD, oX, iJ, oO, iA] ([oS, iB, oO, iC, oW, iD, oX, iJ, oO, 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 satisfied. --------------- 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 satisfied. --------------- 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 [iF, oQ, iD, oW, iD, oX, iF, oT, iD, oT, iA] ([oY, iA, oQ, iD, oW, iD, oX, iF, oT, iD, oT, 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- 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 [iF, oQ, iD, oW, iD, oX, iJ] ([oO, iB, oU, iJ, oW, iD, oX, 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 [iF, oQ, iI, oV, iF, oU, iJ, oO, iG, oR, iA, oT] ([iB, oO, iG, oR, iA, 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 [iG, oV, iC, oY, iG, oO, iB, oR, iF] ([oV, iC, oS, iA, oO, iB, 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 [iG, oV, iC, oY, iG, oO, iB, oR] ([iC, oV, iI, oU, iI, oO, iB, 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 [iF, oQ, iD, oW, iD, oX, iF, oT, iD, oT, iA, oY] ([iA, oQ, iD, oW, iD, oX, iF, oT, iD, oT, iA, 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 [iF, oQ, iD, oW, iI, oZ, iB] ([oO, iI, oY, iG, oZ, iD, oZ, iB])* --------------- Formula: (false R (! oS | (false R (! iH | (true U oW))))) "output W responds to input H after output S" Formula is satisfied. --------------- Formula: (! (true U (oZ & X (true U oO))) | (! oZ U iD)) "input D always precedes output Z, output O" Formula is not satisfied! An error path is [iF, oQ, iG, oU, iC, oS, iI, oO, iB, oW, iF, oZ, iA, oO] ([iB, oW, iB, oW, iI, oO])* --------------- 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- 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 [iF, oQ, iG, oU, iC, oS, iF, oU, iG, oQ] ([iA, oS, iB, oQ])* --------------- Formula: (! oT WU iF) "input F always precedes output T" Formula is not satisfied! An error path is [iG, oV, iC, oY, iG, oO, iC, oR, iI, oW, iI, oT] ([iA, oU, iB, oY, iG, oO, iC, oR, iI, oW, iI, 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- Formula: (! oX WU oZ) "output Z always precedes output X" Formula is not satisfied! An error path is [iF, oQ, iD, oW, iA, oX] ([iC, oY, iB, oU, iA, oR, iF, oW, 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 satisfied. --------------- 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 satisfied. --------------- Formula: (false R (! iC | (true U oS))) "output S always responds to input C" Formula is not satisfied! An error path is [iG, oV, iC] ([oY, iG, oO, iB, oR, iC, oV, iI, oU, iA, oV, 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 not satisfied! An error path is [iF, oQ, iG, oU, iC, oS, iI, oO, iB, oW, iF, oZ, iA, oO, iC, oQ, iB, oR] ([iC, oO, iC, oQ, iB, oR])* --------------- 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- Formula: (false R (! oY | (false R (! iH | (true U oQ))))) "output Q responds to input H after output Y" Formula is satisfied. --------------- 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 not satisfied! An error path is [iF, oQ, iI, oV, iF, oU, iC, oS, iB, oU, iF, oZ] ([iA, oS, iB, oU, iF, oZ])* --------------- 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 [iG, oV, iC, oY, iG] ([oO, iB, oR, iF, oV, iI, oW, iA, 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 [iF, oQ, iD, oW, iG, oX] ([iI, oX, iI, oU, iG, oS, iF, oX])* --------------- Formula: (false R (! iE | (true U (oW & X (true U oU))))) "output W, output U always responds to input E" Formula is satisfied. --------------- 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 [iF, oQ, iD, oW, iA, oX, iD, oY, iG, oY, iD, oZ, iB, oW, iA, oX] ([iC, oY, iB, oU, iA, oR, iF, oW, iA, 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 [iF, oQ, iD, oW, iG, oX, iI, oX, iD, oO, iB, oY, iA, oQ, iI, oV] ([iF, oU, iC, oS, iB, oU, iF, oZ, iC, 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 [iF, oQ] ([iD, oW, iA, oX, iC, oY, iA, oQ, iB, oX, iB, oQ])* --------------- 26 constraints satisfied, 74 unsatisfied.