Reachability problems: =============================== error_2 reachable via input sequence [O, F, N, B, L, G, L, H, E] --------------- error_3 reachable via input sequence [O, F, N, B, L, A, H, C, F] --------------- error_5 reachable via input sequence [O, F, N, A, H, H, G, E, L] --------------- error_7 reachable via input sequence [O, F, N, B, L, L, L, G, A] --------------- error_8 reachable via input sequence [O, F, N, B, L, K, N, O, C] --------------- error_13 reachable via input sequence [O, F, N, B, L, K, B, G, E] --------------- error_19 reachable via input sequence [O, F, N, B, L, L, L, M, O] --------------- error_20 reachable via input sequence [O, F, N, B, L, G, G, O, E] --------------- error_24 reachable via input sequence [O, F, N, B, L, K, N, K, M] --------------- error_30 reachable via input sequence [O, F, N, B, L, G, E, L, L] --------------- error_31 reachable via input sequence [O, F, N, B, L, G, L, M, L] --------------- error_32 reachable via input sequence [O, F, N, B, L, A, L, N, F] --------------- error_34 reachable via input sequence [O, F, N, B, L, K, B, C, G] --------------- error_36 reachable via input sequence [O, F, N, A, H, H, G, G, M] --------------- error_40 reachable via input sequence [O, F, N, B, L, K, L, C, G] --------------- error_48 reachable via input sequence [O, F, N, A, H, H, A, L, J] --------------- error_59 reachable via input sequence [O, F, N, B, L, K, N, A, L] --------------- error_64 reachable via input sequence [O, F, N, B, L, K, B, H, C] --------------- error_69 reachable via input sequence [O, F, N, B, L, L, L, K, B] --------------- error_71 reachable via input sequence [O, F, N, B, L, A, L, G, O] --------------- error_74 reachable via input sequence [O, F, N, B, L, A, G, N, O] --------------- error_75 reachable via input sequence [O, F, N, B, L, K, O, O, G] --------------- error_79 reachable via input sequence [O, F, N, B, L, L, L, E, K] --------------- error_80 reachable via input sequence [O, F, N, B, L, K, O, H, H] --------------- error_85 reachable via input sequence [O, F, N, B, L, A, L, A, L] --------------- error_91 reachable via input sequence [O, F, N, B, L, A, H, N, M] --------------- error_92 reachable via input sequence [O, F, N, A, H, H, G, L, J] --------------- error_98 reachable via input sequence [O, F, N, B, L, G, E, N, F] --------------- All other errors unreachable LTL problems: =============================== Formula: (! (true U iJ) | (! oY U (oZ | iJ))) "output Z precedes output Y before input J" Formula is satisfied. --------------- Formula: (false R (! oP | ((! ((oT & ! oV) & X (! oV U (oY & ! oV))) U (oV | iC)) | (false R ! (oT & X (true U oY)))))) "input C precedes output T, output Y after output P until output V" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iL, oW, iE, oP, iN, oT, iB, oR, iG, oY] ([iC, oS, iK, oP, iE, oU, iA, oU])* --------------- Formula: (false R (iD & (! X (true U iC) | X (true U (iC & (true U oU)))))) "output U always responds to input D, input C" Formula is not satisfied! An error path is [iO, oT, iK, oV] ([iI, oS, iG, oZ, iN, oX, iB, oY, iG, oU, iI, oP])* --------------- Formula: (false R (! oS | ((! iM | (! oX U (((oQ & ! oX) & ! oU) & X ((! oX & ! oU) U oY)))) U (oX | (false R (! iM | ((oQ & ! oU) & X (! oU U oY)))))))) "output Q, output Y without output U responds to input M after output S until output X" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iM] ([oZ, iB, oT, iL, oP, iG, oV, iC, oS, iM])* --------------- Formula: (! (true U oR) | (! oR U ((iH & ! oR) & X (! oR U oQ)))) "input H, output Q always precedes output R" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR] ([iA, oV, iE, oS, iB, oX, iC, oY, iC, oU])* --------------- Formula: ((false R ! iI) | (! iI U (iI & (! (true U oQ) | (! oQ U ((iC & ! oQ) & X (! oQ U oW))))))) "input C, output W precedes output Q after input I" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iI, oT, iA, oQ] ([iA, oR, iG, oZ, iB, oT, iH, oV, iA, oQ])* --------------- Formula: (! (true U iA) | ((! iH | (! iA U (((oS & ! iA) & ! oP) & X ((! iA & ! oP) U oR)))) U iA)) "output S, output R without output P responds to input H before input A" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iA] ([oV, iE, oS, iB, oX, iC, oY, iC, oU, iA])* --------------- Formula: (! oQ WU iO) "input O always precedes output Q" Formula is satisfied. --------------- Formula: (false R (oV & (! ! oR | (! oX WU (iF | oR))))) "input F precedes output X after output V until output R" Formula is not satisfied! An error path is [iO, oT, iK, oV] ([iI, oS, iG, oZ, iN, oX, iB, oY, iG, oU, iI, oP])* --------------- Formula: (! (true U iM) | ((iH & (! X (! iM U iA) | X (! iM U (iA & (true U oV))))) U iM)) "output V responds to input H, input A before input M" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iM] ([oZ, iB, oT, iL, oP, iG, oV, iC, oS, iM])* --------------- Formula: (! (true U iC) | ((! iN | (! iC U (oZ & ! iC))) U iC)) "output Z responds to input N before input C" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iN, oX, iC] ([oU, iB, oX, iI, oW, iG, oR, iC])* --------------- Formula: (false R (! oX | (false R (! iF | ((oY & ! oT) & X (! oT U oQ)))))) "output Y, output Q without output T responds to input F after output X" Formula is satisfied. --------------- Formula: (false R (! oS | ((! iH | (! iM U ((oZ & ! iM) & X (! iM U oR)))) U (iM | (false R (! iH | (oZ & X (true U oR)))))))) "output Z, output R responds to input H after output S until input M" Formula is not satisfied! An error path is [iO, oT, iF, oU, iN, oX, iA, oS, iH, oR] ([iI, oY, iI, oR, iM, oW, iC, oR])* --------------- Formula: (! oU WU iH) "input H always precedes output U" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR] ([iA, oV, iE, oS, iB, oX, iC, oY, iC, oU])* --------------- Formula: (false R (! iE | ((! ((oW & ! iL) & X (! iL U (oU & ! iL))) U (iL | oT)) | (false R ! (oW & X (true U oU)))))) "output T precedes output W, output U after input E until input L" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iE, oW, iH, oT, iK, oU] ([iA, oZ, iH, oV, iK, oU])* --------------- Formula: (false R (! iH | ((! iF | (! iO U ((oR & ! iO) & X (! iO U oY)))) U (iO | (false R (! iF | (oR & X (true U oY)))))))) "output R, output Y responds to input F after input H until input O" Formula is satisfied. --------------- Formula: (false R (! ((iM & ! oU) & (true U oU)) | (! oR U (iK | oU)))) "input K precedes output R between input M and output U" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iM, oZ, iH, oR, iN, oY, iC, oU] ([iA, oY, iH, oR, iN, oY, iC, oU])* --------------- Formula: (false R (! oT | (false R (! iK | ((oS & ! oP) & X (! oP U oQ)))))) "output S, output Q without output P responds to input K after output T" Formula is not satisfied! An error path is [iO, oT, iK, oV] ([iI, oS, iG, oZ, iN, oX, iB, oY, iG, oU, iI, oP])* --------------- Formula: (! (true U iK) | ((! iI | (! iK U (((oQ & ! iK) & ! oW) & X ((! iK & ! oW) U oV)))) U iK)) "output Q, output V without output W responds to input I before input K" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iI, oT, iA, oQ, iK] ([oR, iE, oS, iH, oZ, iE, oY, iA, oQ, iK])* --------------- Formula: (false R (! iG | ((! iO | (! iD U (((oU & ! iD) & ! oT) & X ((! iD & ! oT) U oP)))) U (iD | (false R (! iO | ((oU & ! oT) & X (! oT U oP)))))))) "output U, output P without output T responds to input O after input G until input D" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iK, oT, iG, oR, iO] ([oS, iB, oS, iA, oS, iI, oS, iK, oT, iG, oR, iO])* --------------- Formula: ((false R ! iM) | (! iM U (iM & (! (true U oU) | (! oU U ((iI & ! oU) & X (! oU U oT))))))) "input I, output T precedes output U after input M" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iB, oX, iM, oX, iO, oU] ([iM, oX, iH, oP])* --------------- Formula: (false R (! iG | ((! iC | (! oR U (((oU & ! oR) & ! oQ) & X ((! oR & ! oQ) U oV)))) U (oR | (false R (! iC | ((oU & ! oQ) & X (! oQ U oV)))))))) "output U, output V without output Q responds to input C after input G until output R" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iG, oZ, iN, oX, iC] ([oQ, iB, oP, iG, oU, iB, oY, iG, oU, iK, oQ, iC])* --------------- Formula: (false R (iH & (! ! iC | ((! iN | (! iC U (oQ & ! iC))) WU iC)))) "output Q responds to input N after input H until input C" Formula is not satisfied! An error path is [iO, oT, iK, oV] ([iI, oS, iG, oZ, iN, oX, iB, oY, iG, oU, iI, oP])* --------------- Formula: (false R (! iE | (true U ((oV & ! oT) & X (! oT U oZ))))) "output V, output Z without output T always responds to input E" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iE] ([oW, iB, oX, iK, oS, iC, oU, iL, oY, iE])* --------------- Formula: (false R (! iN | (true U ((oW & ! oP) & X (! oP U oU))))) "output W, output U without output P always responds to input N" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iN] ([oX, iC, oU, iB, oX, iC, oX, iN, oT, iN])* --------------- Formula: (! (true U iM) | ((! iA | (! iM U (((oW & ! iM) & ! oV) & X ((! iM & ! oV) U oZ)))) U iM)) "output W, output Z without output V responds to input A before input M" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iA, oV, iK, oQ, iM] ([oQ, iI, oU, iG, oS, iM])* --------------- Formula: (false R (! oX | (false R (! iA | (oP & X (true U oT)))))) "output P, output T responds to input A after output X" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iB, oX, iA] ([oW, iN, oR, iI, oX, iL, oV, iA])* --------------- Formula: (! (true U iD) | ((iO & (! X (! iD U iI) | X (! iD U (iI & (true U oW))))) U iD)) "output W responds to input O, input I before input D" Formula is satisfied. --------------- Formula: (false R (! oY | (! (true U oP) | (! oP U (iN | ((oX & ! oP) & X (! oP U oZ))))))) "output X, output Z precedes output P after output Y until input N" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iA, oV, iL, oV, iG, oY, iE, oP] ([iC, oS, iG, oY, iE, oP])* --------------- Formula: (! (true U (oX & X (true U oT))) | (! oX U iK)) "input K always precedes output X, output T" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iN, oX, iE, oR, iN, oT] ([iC, oQ, iE, oT, iN, oT])* --------------- Formula: (false R (! (iI & (true U iK)) | ((iN & (! X (! iK U iJ) | X (! iK U (iJ & (true U oR))))) U iK))) "output R responds to input N, input J between input I and input K" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iK] ([oT, iG, oR, iK, oR, iC, oY, iL, oW, iK])* --------------- Formula: ((false R ! oR) | (true U (oR & (! oS WU iI)))) "input I precedes output S after output R" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iA, oV, iE, oS] ([iB, oX, iO, oW, iL, oZ])* --------------- Formula: (false R (! iJ | (false R (! iK | (oX & X (true U oV)))))) "output X, output V responds to input K after input J" Formula is satisfied. --------------- Formula: (false R (! iL | (! (true U oT) | (! oT U (iK | ((oY & ! oT) & X (! oT U oR))))))) "output Y, output R precedes output T after input L until input K" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iL, oW, iE, oP, iN, oT] ([iB, oR, iK, oT])* --------------- Formula: (false R (! (iC & (true U iG)) | ((! iO | (! iG U ((oY & ! iG) & X (! iG U oQ)))) U iG))) "output Y, output Q responds to input O between input C and input G" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iK, oT, iI, oV, iC, oY, iO, oU, iG] ([oW, iI, oV, iC, oY, iO, oU, iG])* --------------- Formula: (false R (! (oV & (true U oR)) | ((iF & (! X (! oR U iO) | X (! oR U (iO & (true U oS))))) U oR))) "output S responds to input F, input O between output V and output R" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iK, oT, iG, oR] ([iC, oV, iG, oZ, iB, oY])* --------------- Formula: (false R (! (oV & (true U iE)) | ((iD & (! X (! iE U iA) | X (! iE U (iA & (true U oY))))) U iE))) "output Y responds to input D, input A between output V and input E" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iA, oV, iE] ([oS, iB, oX, iC, oY, iC, oU, iA, oV, iE])* --------------- Formula: (false R (! iC | (true U ((oT & ! oP) & X (! oP U oY))))) "output T, output Y without output P always responds to input C" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iL, oW, iC] ([oS, iK, oP, iE, oU, iA, oU, iC])* --------------- Formula: (! (true U oY) | (! oQ U (oY | ((iM & ! oQ) & X (! oQ U oV))))) "input M, output V precedes output Q before output Y" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iI, oT, iA, oQ, iA, oR, iN, oY] ([iC, oQ, iG, oY, iI, oT, iA, oQ, iA, oR, iN, oY])* --------------- Formula: (false R (! oQ | ((! iO | (! iJ U (((oZ & ! iJ) & ! oV) & X ((! iJ & ! oV) U oU)))) U (iJ | (false R (! iO | ((oZ & ! oV) & X (! oV U oU)))))))) "output Z, output U without output V responds to input O after output Q until input J" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iA, oV, iK, oQ, iN, oU, iO] ([oQ, iM, oZ, iO])* --------------- Formula: (! (true U iL) | ((! iH | (! iL U (oV & ! iL))) U iL)) "output V responds to input H before input L" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iL] ([oW, iC, oS, iK, oP, iM, oS, iE, oY, iL])* --------------- Formula: (false R (! iG | (true U oU))) "output U always responds to input G" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iG] ([oZ, iN, oX, iC, oQ, iC, oS, iL, oY, iG])* --------------- Formula: (! (true U iM) | ((iC & (! X (! iM U iF) | X (! iM U (iF & (true U oT))))) U iM)) "output T responds to input C, input F before input M" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iM] ([oZ, iB, oT, iL, oP, iG, oV, iC, oS, iM])* --------------- Formula: (false R (! iD | ((! ((oW & ! iH) & X (! iH U (oQ & ! iH))) U (iH | iO)) | (false R ! (oW & X (true U oQ)))))) "input O precedes output W, output Q after input D until input H" Formula is satisfied. --------------- Formula: ((false R ! oQ) | (! oQ U (oQ & (! (true U (oX & X (true U oZ))) | (! oX U oT))))) "output T precedes output X, output Z after output Q" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iA, oV, iK, oQ, iA, oR, iM, oX] ([iE, oT, iN, oU, iO, oQ, iO, oZ, iA, oR, iM, oX])* --------------- Formula: (! (true U iL) | (! oU U (iL | ((iM & ! oU) & X (! oU U iH))))) "input M, input H precedes output U before input L" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iL] ([oW, iC, oS, iK, oP, iM, oS, iE, oY, iL])* --------------- Formula: ((false R ! iD) | (true U (iD & (! oV WU iG)))) "input G precedes output V after input D" Formula is satisfied. --------------- Formula: (false R (iI & (! ! oP | (! oQ WU (oX | oP))))) "output X precedes output Q after input I until output P" Formula is not satisfied! An error path is [iO, oT, iK, oV] ([iI, oS, iG, oZ, iN, oX, iB, oY, iG, oU, iI, oP])* --------------- Formula: (false R (! iE | (false R (! iL | (true U oU))))) "output U responds to input L after input E" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iE, oW, iN, oR, iL] ([oW, iK, oW, iK, oV, iL])* --------------- Formula: (false R (! iI | (true U oZ))) "output Z always responds to input I" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI] ([oS, iK, oT, iG, oR, iK, oR, iI, oY, iA, oV, iI])* --------------- Formula: (false R (! iF | ((iC & (! X (! iJ U iB) | X (! iJ U (iB & (true U oQ))))) U (iJ | (false R (iC & (! X (! iJ U iB) | X (! iJ U (iB & (true U oQ)))))))))) "output Q responds to input C, input B after input F until input J" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR] ([iA, oV, iE, oS, iB, oX, iC, oY, iC, oU])* --------------- Formula: (! oV WU iF) "input F always precedes output V" Formula is not satisfied! An error path is [iO, oT, iK, oV] ([iI, oS, iG, oZ, iN, oX, iB, oY, iG, oU, iI, oP])* --------------- Formula: (! (true U iF) | ((! iD | (! iF U (oT & ! iF))) U iF)) "output T responds to input D before input F" Formula is satisfied. --------------- Formula: (! (true U oQ) | ((iO & (! X (! oQ U iK) | X (! oQ U (iK & (true U oV))))) U oQ)) "output V responds to input O, input K before output Q" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iA, oV, iK, oQ] ([iA, oR, iM, oX, iE, oT])* --------------- Formula: (! (true U iO) | ((! iE | (! iO U (((oR & ! iO) & ! oW) & X ((! iO & ! oW) U oP)))) U iO)) "output R, output P without output W responds to input E before input O" Formula is satisfied. --------------- Formula: (! (true U oW) | ((! iN | (! oW U ((oQ & ! oW) & X (! oW U oX)))) U oW)) "output Q, output X responds to input N before output W" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iN, oX, iG, oS, iG, oW] ([iG, oY, iE, oQ, iN, oX, iG, oS, iG, oW])* --------------- Formula: ((false R ! iF) | (! iF U (iF & (! (true U oQ) | (! oQ U ((iC & ! oQ) & X (! oQ U iA))))))) "input C, input A precedes output Q after input F" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iA, oV, iK, oQ] ([iA, oR, iM, oX, iE, oT])* --------------- Formula: (false R (! iK | (true U ((oR & ! oT) & X (! oT U oX))))) "output R, output X without output T always responds to input K" Formula is not satisfied! An error path is [iO, oT, iK, oV] ([iI, oS, iG, oZ, iN, oX, iB, oY, iG, oU, iI, oP])* --------------- Formula: (! (true U iD) | (! ((oS & ! iD) & X (! iD U (oT & ! iD))) U (iD | oQ))) "output Q precedes output S, output T before input D" Formula is satisfied. --------------- Formula: ((false R ! iJ) | (! iJ U (iJ & (! (true U oQ) | (! oQ U ((iA & ! oQ) & X (! oQ U iL))))))) "input A, input L precedes output Q after input J" Formula is satisfied. --------------- Formula: (! (true U iD) | ((! iE | (! iD U (((oP & ! iD) & ! oX) & X ((! iD & ! oX) U oW)))) U iD)) "output P, output W without output X responds to input E before input D" Formula is satisfied. --------------- Formula: (false R (! oP | (false R (iG & (! X (true U iH) | X (! iH U (iH & (true U oW)))))))) "output W responds to input G, input H after output P" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iI, oP] ([iB, oU, iL, oX, iC, oT, iB, oR])* --------------- Formula: (false R (! iG | (false R (! iD | ((oR & ! oX) & X (! oX U oY)))))) "output R, output Y without output X responds to input D after input G" Formula is satisfied. --------------- Formula: (false R (oW & (! ! oV | (! oT WU (iH | oV))))) "input H precedes output T after output W until output V" Formula is not satisfied! An error path is [iO, oT, iK, oV] ([iI, oS, iG, oZ, iN, oX, iB, oY, iG, oU, iI, oP])* --------------- Formula: (false R (! iD | (false R (iH & (! X (true U iL) | X (! iL U (iL & (true U oZ)))))))) "output Z responds to input H, input L after input D" Formula is satisfied. --------------- Formula: (false R (! (iB & (true U iF)) | (! ((oR & ! iF) & X (! iF U (oS & ! iF))) U (iF | oV)))) "output V precedes output R, output S between input B and input F" Formula is satisfied. --------------- Formula: (false R (! (iB & (true U iJ)) | (! oS U (iJ | ((iD & ! oS) & X (! oS U oW)))))) "input D, output W precedes output S between input B and input J" Formula is satisfied. --------------- Formula: (! (true U oW) | (! oW U ((iD & ! oW) & X (! oW U iF)))) "input D, input F always precedes output W" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW] ([iB, oX, iL, oV, iA, oS, iG, oZ, iO, oY])* --------------- Formula: (! (true U iC) | ((iN & (! X (! iC U iK) | X (! iC U (iK & (true U oR))))) U iC)) "output R responds to input N, input K before input C" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iL, oW, iC] ([oS, iK, oP, iE, oU, iA, oU, iC])* --------------- Formula: (! (true U oS) | (! oW U (oS | ((oY & ! oW) & X (! oW U iA))))) "output Y, input A precedes output W before output S" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iL, oW, iC, oS] ([iK, oP, iE, oU, iN, oP])* --------------- Formula: (false R (! oT | (false R (! iH | (oZ & X (true U oY)))))) "output Z, output Y responds to input H after output T" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR] ([iA, oV, iE, oS, iB, oX, iC, oY, iC, oU])* --------------- Formula: (! (true U iB) | ((! iO | (! iB U ((oP & ! iB) & X (! iB U oX)))) U iB)) "output P, output X responds to input O before input B" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iB] ([oX, iL, oV, iA, oS, iG, oZ, iO, oY, iB])* --------------- Formula: (false R (! oZ | (false R (! iB | (true U oW))))) "output W responds to input B after output Z" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iM, oZ, iB] ([oT, iL, oP, iG, oV, iC, oS, iM, oZ, iB])* --------------- Formula: (false R (! (oW & (true U iF)) | ((iG & (! X (! iF U iN) | X (! iF U (iN & (true U oV))))) U iF))) "output V responds to input G, input N between output W and input F" Formula is satisfied. --------------- Formula: (false R (! iH | ((! ((oZ & ! iB) & X (! iB U (oS & ! iB))) U (iB | iD)) | (false R ! (oZ & X (true U oS)))))) "input D precedes output Z, output S after input H until input B" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iN, oX, iE, oR, iN, oT, iE, oZ, iO, oS] ([iC, oR, iE, oZ])* --------------- Formula: (false R (! iM | (false R (! iB | (oR & X (true U oW)))))) "output R, output W responds to input B after input M" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iM, oZ, iB] ([oT, iL, oP, iG, oV, iC, oS, iM, oZ, iB])* --------------- Formula: (false R (iO & (! X (true U iJ) | X (true U (iJ & (true U oZ)))))) "output Z always responds to input O, input J" Formula is not satisfied! An error path is [iO, oT, iK, oV] ([iI, oS, iG, oZ, iN, oX, iB, oY, iG, oU, iI, oP])* --------------- Formula: (false R (! ((oZ & ! iL) & (true U iL)) | (! oV U (iM | iL)))) "input M precedes output V between output Z and input L" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iM, oZ, iH, oR, iN, oY, iG, oV, iL] ([oV, iN, oY, iG, oV, iL])* --------------- Formula: (false R (! (oW & (true U oU)) | ((! iM | (! oU U (((oX & ! oU) & ! oT) & X ((! oU & ! oT) U oR)))) U oU))) "output X, output R without output T responds to input M betwen output W and output U" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iB, oX, iM, oX, iO, oU] ([iM, oX, iH, oP])* --------------- Formula: (false R (! oX | ((iJ & (! X (! oW U iE) | X (! oW U (iE & (true U oU))))) U (oW | (false R (iJ & (! X (! oW U iE) | X (! oW U (iE & (true U oU)))))))))) "output U responds to input J, input E after output X until output W" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iN, oX] ([iC, oU, iB, oX, iI, oW, iG, oR])* --------------- Formula: (false R (! iA | ((! iJ | (! iI U (((oX & ! iI) & ! oP) & X ((! iI & ! oP) U oR)))) U (iI | (false R (! iJ | ((oX & ! oP) & X (! oP U oR)))))))) "output X, output R without output P responds to input J after input A until input I" Formula is satisfied. --------------- Formula: (false R (! ((oQ & ! iO) & (true U iO)) | (! oP U (oR | iO)))) "output R precedes output P between output Q and input O" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iL, oX, iK, oQ, iE, oT, iG, oP, iO] ([oR, iI, oS, iL, oX, iK, oQ, iE, oT, iG, oP, iO])* --------------- Formula: (! (true U oR) | (! oR U ((oV & ! oR) & X (! oR U iJ)))) "output V, input J always precedes output R" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR] ([iA, oV, iE, oS, iB, oX, iC, oY, iC, oU])* --------------- Formula: (false R (! (iE & (true U oZ)) | ((! iK | (! oZ U (((oQ & ! oZ) & ! oY) & X ((! oZ & ! oY) U oX)))) U oZ))) "output Q, output X without output Y responds to input K betwen input E and output Z" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iE, oW, iH, oT, iK, oU, iA, oZ] ([iC, oT, iE, oW, iH, oT, iK, oU, iA, oZ])* --------------- Formula: (! (true U oW) | (! oW U ((iN & ! oW) & X (! oW U iI)))) "input N, input I always precedes output W" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW] ([iB, oX, iL, oV, iA, oS, iG, oZ, iO, oY])* --------------- Formula: (false R (! oZ | (false R (! iI | (true U oS))))) "output S responds to input I after output Z" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iI, oP, iH, oZ, iE, oV, iI] ([oY, iH, oW, iI])* --------------- Formula: (! (true U oR) | ((! iA | (! oR U (((oP & ! oR) & ! oS) & X ((! oR & ! oS) U oV)))) U oR)) "output P, output V without output S responds to input A before output R" Formula is not satisfied! An error path is [iO, oT, iF, oU, iN, oX, iA, oS, iH, oR] ([iI, oY, iI, oR, iM, oW, iC, oR])* --------------- Formula: (false R (! (oP & (true U iO)) | ((! iA | (! iO U ((oY & ! iO) & X (! iO U oX)))) U iO))) "output Y, output X responds to input A between output P and input O" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iO, oP, iA, oS, iG, oR, iC, oS, iO] ([oY, iA, oS, iG, oR, iC, oS, iO])* --------------- Formula: (false R (iK & (! ! iF | (! oZ WU (iI | iF))))) "input I precedes output Z after input K until input F" Formula is not satisfied! An error path is [iO, oT, iK, oV] ([iI, oS, iG, oZ, iN, oX, iB, oY, iG, oU, iI, oP])* --------------- Formula: (false R (! (iL & (true U oZ)) | ((! iB | (! oZ U (((oW & ! oZ) & ! oT) & X ((! oZ & ! oT) U oY)))) U oZ))) "output W, output Y without output T responds to input B betwen input L and output Z" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iL, oX, iA, oV, iB, oU, iC, oZ] ([iB, oR, iA, oV, iB, oU, iC, oZ])* --------------- Formula: (! (true U iE) | ((! iC | (! iE U ((oZ & ! iE) & X (! iE U oT)))) U iE)) "output Z, output T responds to input C before input E" Formula is not satisfied! An error path is [iO, oT, iF, oU, iH, oR, iN, oX, iC, oU, iE] ([oY, iL, oU, iL, oW, iE])* --------------- Formula: (false R (! (oW & (true U oU)) | (! ((oZ & ! oU) & X (! oU U (oR & ! oU))) U (oU | iA)))) "input A precedes output Z, output R between output W and output U" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iE, oW, iH, oT, iG, oZ, iC, oX, iO, oR, iK, oU] ([iA, oZ, iH, oV, iK, oU])* --------------- Formula: (false R (! oW | (false R (! iF | (true U oZ))))) "output Z responds to input F after output W" Formula is satisfied. --------------- Formula: ((false R ! iI) | (! iI U (iI & (! (true U oR) | (! oR U ((iC & ! oR) & X (! oR U oS))))))) "input C, output S precedes output R after input I" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iK, oT, iG, oR] ([iC, oV, iG, oZ, iB, oY])* --------------- Formula: (! (true U oW) | ((! iI | (! oW U ((oR & ! oW) & X (! oW U oU)))) U oW)) "output R, output U responds to input I before output W" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iK, oT, iI, oV, iE, oW] ([iH, oU, iA, oR])* --------------- Formula: (false R (! oQ | (false R (! iF | ((oS & ! oP) & X (! oP U oY)))))) "output S, output Y without output P responds to input F after output Q" Formula is satisfied. --------------- Formula: (false R (! iB | (true U ((oV & ! oS) & X (! oS U oX))))) "output V, output X without output S always responds to input B" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iB] ([oX, iL, oV, iA, oS, iG, oZ, iO, oY, iB])* --------------- Formula: (false R (! iE | ((! iN | (! iO U ((oX & ! iO) & X (! iO U oT)))) U (iO | (false R (! iN | (oX & X (true U oT)))))))) "output X, output T responds to input N after input E until input O" Formula is not satisfied! An error path is [iO, oT, iF, oU, iO, oW, iE, oW, iN] ([oR, iE, oU, iB, oZ, iK, oY, iN])* --------------- Formula: (false R (! iG | (true U ((oP & ! oV) & X (! oV U oU))))) "output P, output U without output V always responds to input G" Formula is not satisfied! An error path is [iO, oT, iK, oV, iI, oS, iG] ([oZ, iN, oX, iC, oQ, iC, oS, iL, oY, iG])* --------------- Formula: (! (true U oY) | (! ((oQ & ! oY) & X (! oY U (oZ & ! oY))) U (oY | oT))) "output T precedes output Q, output Z before output Y" Formula is satisfied. --------------- 22 constraints satisfied, 78 unsatisfied.