Reachability problems: =============================== error_9 reachable via input sequence [F, F, D, G, J, G, B, H] --------------- error_23 reachable via input sequence [F, F, D, G, J, G, B, D] --------------- error_57 reachable via input sequence [F, F, D, G, J, G, B, B] --------------- error_66 reachable via input sequence [F, F, D, G, J, G, B, A] --------------- error_80 reachable via input sequence [F, F, D, G, J, G, B, 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 [iF, oW, iF, oR, iD, oR, iC, oW, iF, oV] ([iA, oV, iD, oY, iE, oX, iD, oR, iC, oW, iF, 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, oW, iF, oR, iC, oW, iJ, oX, iG, oW, iG, oZ, iB, oT, iF, oW, iJ, oY] ([iA, oW, iB, oW, iJ, 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 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 not satisfied! An error path is [iF, oW, iF, oR, iJ, oQ, iA, oT, iB, oZ, iE] ([oW, iE, oV, iJ, oZ, iE])* --------------- 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 [iF, oW, iF, oR, iC, oW, iF] ([oZ, iC, oY, iC, oR, iF, oZ, iB, 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 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, oW, iF, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR])* --------------- 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, oW, iF, oR, iJ, oQ, iA, oT, iC, oO] ([iB, oY, iG, oW, iC, 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, oW, iF, oR, iJ, oQ, iA, oT] ([iA, oX, iA, oR, iE, oZ, iB, oR, iJ, oQ, iA, 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, oW, iF, oR, iD, oR] ([iC, oW, iB, oR, iA, oZ, iA, oY, iE, oR, iD, oR])* --------------- Formula: (false R (! iE | (true U oT))) "output T always responds to input E" Formula is not satisfied! An error path is [iF, oW, iF, oR, iC, oW, iF, oZ, iE] ([oY, iB, oO, iC, oZ, iA, oZ, iE])* --------------- 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 [iF, oW, iF, oR, iC, oW, iG] ([oY, iD, oT, iJ, oW, iA, oX, iA, oW, 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 [iF, oW, iF, oR, iJ, oQ] ([iA, oT, iB, oZ, iD, oY, iA, oV, iE, 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, oW, iF, oR, iJ, oQ, iA, oT, iC, oO, iF, oZ] ([iA, oZ, iF, oR, iJ, oQ, iA, oT, iB, oZ, iA, oR, iD, oW, iC, oT, iC, oO, iF, 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 not satisfied! An error path is [iF, oW, iF, oR, iJ, oQ, iA, oT, iJ, oX, iE, oO, iJ] ([oO, iC, oO, 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 [iF, oW, iF, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR])* --------------- 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, oW, iF, oR, iJ, oQ, iD, oZ, iJ, oV, iB, oW] ([iD, oW, iD, 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 satisfied. --------------- Formula: (! oS WU oU) "output U always precedes output S" Formula is satisfied. --------------- 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 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 satisfied. --------------- 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, oW, iF, oR, iD, oR] ([iC, oW, iB, oR, iA, oZ, iA, oY, iE, oR, iD, 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, oW, iF, oR, iC, oW, iJ, oX, iF, oW, iG, oT, iJ, oO] ([iA, oW, iG, oT, iJ, 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, oW, iF, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR])* --------------- 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, oW, iF, oR, iC, oW, iF, oZ, iF, oO, iA, oQ, iB, oV] ([iD, oW, iF, oZ, iF, oO, iA, oQ, iB, 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 [iF, oW, iF, oR, iC] ([oW, iF, oZ, iF, oO, iA, oQ, iA, oW, iB, oR, 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 [iF, oW, iF, oR, iJ, oQ, iA, oT, iB, oZ, iD, oY, iG, oO, iB, oT, iC, oO] ([iB, oY, iG, oW, iC, 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 satisfied. --------------- 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 [iF, oW, iF, oR, iC, oW, iJ, oX, iC, oX, iF, oY, iC, oV] ([iA, oX, iC, oX, iF, oY, iC, oV])* --------------- Formula: (! (true U oR) | (! oV U (iF | oR))) "input F precedes output V before output R" Formula is satisfied. --------------- Formula: (! (true U (oT & X (true U oU))) | (! oT U iF)) "input F always precedes output T, output U" Formula is satisfied. --------------- 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, oW, iF, oR, iC, oW, iG, oY, iD, oT, iJ, oW, iF, oZ] ([iC, 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, oW, iF, oR, iC, oW, iJ, oX, iG, oW, iJ, oY] ([iA, oW, iB, oW, iJ, 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, oW, iF, oR, iJ, oQ, iA, oT] ([iA, oX, iA, oR, iE, oZ, iB, oR, iJ, oQ, iA, 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 [iF, oW, iF, oR, iC, oW, iJ, oX, iB] ([oW, iC, oQ, iC, oO, iG, oX, 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, oW, iF, oR, iJ, oQ, iA, oT, iB] ([oZ, iA, oR, iB, oZ, iB, 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 [iF, oW, iF, oR, iC, oW, iG] ([oY, iD, oT, iJ, oW, iA, oX, iA, oW, 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 [iF, oW, iF, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR])* --------------- 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, oW, iF, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR])* --------------- 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 satisfied. --------------- 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 satisfied. --------------- 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, oW, iF, oR, iJ, oQ, iA, oT, iA, oX] ([iA, oR, iE, oZ, iB, oR, iJ, oQ, iA, oT, iB, oZ, iD, oY, iG, oO, iB, oT, 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, oW, iF, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR])* --------------- Formula: (! (true U oU) | (! oZ U (oP | oU))) "output P precedes output Z before output U" Formula is satisfied. --------------- 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, oW, iF, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR])* --------------- 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, oW, iF, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR])* --------------- 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 satisfied. --------------- 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 satisfied. --------------- 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 [iF, oW, iF, oR, iJ, oQ, iD, oZ, iE, oR, iD] ([oQ, iD, oQ, iB, oR, 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 [iF, oW, iF, oR, iD, oR, iC, oW, iF, oV] ([iA, oV, iD, oY, iE, oX, iD, oR, iC, oW, iF, oV])* --------------- Formula: (false R (! iB | (true U oW))) "output W always responds to input B" Formula is not satisfied! An error path is [iF, oW, iF, oR, iJ, oQ, iB] ([oX, iA, oZ, iE, oT, iC, oR, iG, oQ, 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 satisfied. --------------- 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 satisfied. --------------- 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, oW, iF, oR, iC, oW, iJ, oX, iF, oW, iC, oT, iC, oQ, iD, oW, iB, oO] ([iC, oY, iG, oX, iF, 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, oW, iF, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR])* --------------- 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, oW, iF, oR, iJ, oQ, iB, oX, iA] ([oZ, iE, oT, iC, oR, iG, oQ, iB, 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 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, oW, iF, oR, iC, oW, iJ, oX, iC, oX, iF, oY, iA] ([oO, iD, oX, iC, oX, iF, oY, 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, oW, iF, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR])* --------------- 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, oW, iF, oR, iD, oR, iG, oX, iJ] ([oR, iG, oT, iA, oO, iB, oW, iE, oR, iD, oR, iG, 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 not satisfied! An error path is [iF, oW, iF, oR, iC, oW, iJ, oX, iF, oW, iB, oO, iE, oV] ([iD, oR, iC, oW, iJ, oX, iF, oW, iC, oT, iC, oQ, iD, oW, iB, oO, iE, oV])* --------------- 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, oW, iF, oR, iJ, oQ, iA, oT] ([iB, oZ, iA, oR, iB, oZ, iB, 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 [iF, oW, iF, oR, iC, oW, iF] ([oZ, iC, oY, iC, oR, iF, oZ, iB, oW, 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 not satisfied! An error path is [iF, oW, iF, oR, iC, oW, iJ, oX, iG, oW, iG, oZ, iE] ([oR, iA, oW, iJ, oX, iG, oW, iG, oZ, iE])* --------------- 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 satisfied. --------------- 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, oW, iF, oR, iJ, oQ, iA, oT, iB, oZ, iD, oY] ([iA, oV, iA, oZ, iD, 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 satisfied. --------------- 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, oW, iF, oR, iC, oW, iF, oZ, iF, oO] ([iA, oQ, iA, oW, iG, 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, oW, iF, oR] ([iC, oW, iF, oZ, iF, oO, iA, oQ, iA, oW, iB, oR])* --------------- 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 satisfied. --------------- Formula: (! oT WU iF) "input F always precedes output T" Formula is satisfied. --------------- 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, oW, iF, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR])* --------------- Formula: (! oX WU oZ) "output Z always precedes output X" Formula is not satisfied! An error path is [iF, oW, iF, oR, iC, oW, iJ, oX] ([iB, oW, iC, oQ, iC, oO, iG, 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 [iF, oW, iF, oR, iC] ([oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR, 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, oW, iF, oR, iC, oW, iF, oZ, iE, oY, iB, oO, iC, oZ, iG, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, 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, oW, iF, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR])* --------------- 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 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 not satisfied! An error path is [iF, oW, iF, oR, iC, oW, iF, oZ, iE] ([oY, iB, oO, iC, oZ, iA, oZ, iE])* --------------- 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 [iF, oW, iF, oR, iC, oW, iF, oZ, iE, oY, iG] ([oQ, iC, oQ, iE, oR, iC, oW, iF, oZ, iE, 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, oW, iF, oR, iD, oR, iG, oX] ([iJ, oR, iG, oT, iA, oO, iB, oW, iE, oR, iD, oR, 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 [iF, oW, iF, oR, iC, oW, iF, oZ, iE] ([oY, iB, oO, iC, oZ, iA, oZ, iE])* --------------- 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, oW, iF, oR, iJ, oQ, iD, oZ, iE, oR, iF, oX] ([iA, oX, iA, oR, iF, 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, oW, iF, oR, iC, oW, iF, oZ, iF, oO, iG, oY, iB, oW, iA, oO, iA, oQ, iB, oV] ([iD, oW, iF, oZ, iF, oO, iA, oQ, 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 [iF, oW, iF, oR] ([iC, oW, iF, oZ, iC, oY, iC, oR, iC, oY, iE, oR])* --------------- 38 constraints satisfied, 62 unsatisfied.