Reachability problems: =============================== error_4 reachable via input sequence [F, F, N, A, L, G, A, E, M, O] --------------- error_8 reachable via input sequence [F, F, N, A, L, C, A, E, G, N, F] --------------- error_9 reachable via input sequence [F, F, N, A, L, G, A, E, A, B] --------------- error_10 reachable via input sequence [F, F, N, G, H, G, C, A, I, F, O] --------------- error_11 reachable via input sequence [F, F, N, A, L, C, A, N, I, M] --------------- error_13 reachable via input sequence [F, F, N, G, H, G, C, O, H, O, A] --------------- error_15 reachable via input sequence [F, F, N, G, H, G, C, A, I, H, N] --------------- error_16 reachable via input sequence [F, F, N, A, L, C, A, E, G, O, I] --------------- error_17 reachable via input sequence [F, F, N, A, L, C, A, E, G, I] --------------- error_19 reachable via input sequence [F, F, N, A, L, N, H, F, C, B] --------------- error_20 reachable via input sequence [F, F, N, A, L, G, A, O, F, O] --------------- error_23 reachable via input sequence [F, F, N, A, L, C, A, F, E, N] --------------- error_24 reachable via input sequence [F, F, N, A, L, G, A, O, N, F] --------------- error_28 reachable via input sequence [F, F, N, G, H, G, N, C, I, C, I] --------------- error_32 reachable via input sequence [F, F, N, A, L, E, J, G, I, K] --------------- error_33 reachable via input sequence [F, F, N, G, H, G, N, F, A, C, G] --------------- error_34 reachable via input sequence [F, F, N, G, H, G, C, C, J, O, A] --------------- error_38 reachable via input sequence [F, F, N, A, L, C, E, J, L, F] --------------- error_39 reachable via input sequence [F, F, N, A, L, C, A, F, C, K] --------------- error_43 reachable via input sequence [F, F, N, A, L, C, A, E, F, I] --------------- error_46 reachable via input sequence [F, F, N, A, L, N, H, F, H, J] --------------- error_49 reachable via input sequence [F, F, N, A, L, C, A, E, G, C, L] --------------- error_51 reachable via input sequence [F, F, N, A, L, E, J, L, O, N] --------------- error_54 reachable via input sequence [F, F, N, A, L, E, L, F, A, C] --------------- error_56 reachable via input sequence [F, F, N, A, L, E, J, L, F, K] --------------- error_58 reachable via input sequence [F, F, N, A, L, G, L, A, L, E] --------------- error_59 reachable via input sequence [F, F, N, A, L, N, H, F, F, C] --------------- error_60 reachable via input sequence [F, F, N, A, L, G, A, E, I, I] --------------- error_61 reachable via input sequence [F, F, N, G, H, G, N, A, L, I, L] --------------- error_63 reachable via input sequence [F, F, N, G, H, G, C, O, H, C, C] --------------- error_65 reachable via input sequence [F, F, N, A, L, G, A, H, F, H] --------------- error_66 reachable via input sequence [F, F, N, A, L, C, A, E, J, M] --------------- error_68 reachable via input sequence [F, F, N, A, L, G, A, O, C, D] --------------- error_69 reachable via input sequence [F, F, N, A, L, C, E, A, E, N] --------------- error_70 reachable via input sequence [F, F, N, A, L, G, L, N, M, N] --------------- error_71 reachable via input sequence [F, F, N, A, L, E, L, J, I, J] --------------- error_72 reachable via input sequence [F, F, N, A, L, C, A, F, N, K] --------------- error_73 reachable via input sequence [F, F, N, A, L, G, A, H, O, C] --------------- error_75 reachable via input sequence [F, F, N, A, L, G, A, E, E, A] --------------- error_82 reachable via input sequence [F, F, N, A, L, E, J, L, M, K] --------------- error_84 reachable via input sequence [F, F, N, A, L, E, J, L, C, D] --------------- error_85 reachable via input sequence [F, F, N, A, L, C, E, H, M, B] --------------- error_88 reachable via input sequence [F, F, N, A, L, E, L, E, N, F] --------------- error_89 reachable via input sequence [F, F, N, A, L, E, L, E, G, N] --------------- error_91 reachable via input sequence [F, F, N, G, H, G, N, C, H, A, C] --------------- error_92 reachable via input sequence [F, F, N, A, L, C, E, H, O, J] --------------- error_93 reachable via input sequence [F, F, N, A, L, C, A, N, E, G] --------------- error_94 reachable via input sequence [F, F, N, A, L, G, A, O, H, F] --------------- error_96 reachable via input sequence [F, F, N, A, L, C, E, H, H, J] --------------- error_97 reachable via input sequence [F, F, N, A, L, C, A, N, O, H] --------------- error_98 reachable via input sequence [F, F, N, A, L, C, A, E, C, J] --------------- All other errors unreachable LTL problems: =============================== Formula: (! (true U iJ) | (! oY U (oZ | iJ))) "output Z precedes output Y before input J" Formula is not satisfied! An error path is [iF, oQ, iF, oP, iN, oY, iH, oX, iJ] ([oP, iI, oY, iA, oV, iL, oZ, iO, oW, iE, oX, iJ])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iF, oQ, iJ, oT, iE, oU, iC, oY] ([iE, oR, iE, oY, iF, oQ, iJ, oT, iE, oU, iC, oY])* --------------- 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 [iF, oQ] ([iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iC, oX, iL, oR, iG, oW])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iG, oU, iA, oS, iM] ([oR, iA, oV, iE, oS, iH, oQ, iA, oS, iG, oU, iA, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iG, oU, iC, oR] ([iC, oS, iC, oY, iL, oP, iG, oR])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iG, oU, iJ, oP, iI, oW, iJ, oQ] ([iF, oX, iE, oQ, iF, oP, iN, oY, iA, oS, iG, oU, iJ, oP, iI, oW, iJ, 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 [iF, oQ, iF, oP, iN, oY, iH, oX, iJ, oP, iI, oY, iA] ([oV, iL, oZ, iA, oT, iA, oY, iA])* --------------- Formula: (! oQ WU iO) "input O always precedes output Q" Formula is not satisfied! An error path is [iF, oQ] ([iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iC, oX, iL, oR, iG, oW])* --------------- 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 [iF, oQ] ([iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iC, oX, iL, oR, iG, oW])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iH, oX, iO, oY, iM] ([oQ, iF, oV, iL, oT, iH, oX, iN, oY, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iC] ([oX, iJ, oZ, iN, oZ, iE, oW, iG, oT, iJ, oZ, iG, oY, iA, oS, 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 not satisfied! An error path is [iF, oQ, iF, oP, iN, oY, iA, oS, iF, oQ, iO, oX, iF] ([oY, iF, oT, iH, oS, iH, oX, iF])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iF, oQ, iF, oR, iH] ([oT, iA, oX, iE, oZ, iA, oY, iF, oR, iH])* --------------- Formula: (! oU WU iH) "input H always precedes output U" Formula is not satisfied! An error path is [iF, oQ, iF, oP, iN, oY, iA, oS, iG, oU] ([iA, oS, iH, oW, iJ, oV, iJ, oS, iL, oQ, iA, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iC, oX, iJ, oZ, iN, oZ, iE, oW, iI, oU] ([iA, oS, iN, oY, iA, oS, iC, oX, iJ, oZ, iN, oZ, iE, oW, iI, 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 not satisfied! An error path is [iF, oQ, iF, oP, iN, oY, iH, oX, iJ, oP, iJ, oX, iF] ([oY, iM, oS, iO, oU, iE, oX, iF])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iM, oR, iE, oQ, iC, oQ, iJ, oU] ([iA, oU, iN, oY, iL, oX, iF, oW, iJ, oZ])* --------------- 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 satisfied. --------------- 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 satisfied. --------------- 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 [iF, oQ, iF, oP, iN, oY, iG, oP, iC, oW, iO] ([oQ, iN, oX, iF, oT, iF, oX, iC, oW, 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 [iF, oQ, iF, oP, iN, oY, iH, oX, iJ, oP, iI, oY, iM, oU] ([iC, oQ, iC, oU, iC, oU])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iG, oP, iC] ([oW, iO, oQ, iA, oP, iA, oW, iI, oU, iF, oP, 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 [iF, oQ] ([iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iC, oX, iL, oR, iG, oW])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iL, oP, iE] ([oS, iJ, oT, iG, oV, iI, oX, iC, oQ, iA, oS, iL, oP, 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 [iF, oQ, iF, oP, iN] ([oY, iA, oS, iF, oQ, iF, oR, iL, oZ, iJ, oS, iC, oS, iN, oQ, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iG, oU, iA, oS, iM] ([oR, iA, oV, iE, oS, iH, oQ, iA, oS, iG, oU, iA, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iL, oP, iG, oX, iA] ([oU, iO, oT, iF, oW, iG, oZ, 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 [iF, oQ, iF, oP, iN, oY, iG, oP] ([iC, oW, iO, oQ, iA, oP, iA, oW, iI, oU, iF, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iF, oQ, iO, oX, iF, oY, iF, oT] ([iC, oU, iI, oY, iF, 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 satisfied. --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iG, oU, iC, oR, iC, oS] ([iC, oY, iL, oP, iM, oS])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iL, oP, iE, oS, iJ, oT] ([iG, oV, iI, oX, iC, oQ, iA, oS, iL, oP, iE, oS, iJ, 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 [iF, oQ, iF, oP, iN, oY, iG, oP, iC, oW, iO, oQ, iN, oX, iL, oU, iG] ([oZ, iH, oW, iO, oQ, iN, oX, iL, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iL, oP, iE, oS, iL, oV, iJ, oR] ([iI, oW, iE, oQ, iO, oY, iA, oS, iL, oP, iE, oS, iL, oV, iJ, oR])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iL, oP, iE, oS, iL, oV, iE] ([oV, iN, oZ, iO, oQ, iO, oY, iA, oS, iL, oP, iE, oS, iL, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iC] ([oX, iJ, oZ, iN, oZ, iE, oW, iE, oT, iJ, oT, iL, oP, iN, oY, iA, oS, 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 [iF, oQ, iF, oP, iN, oY] ([iA, oS, iF, oQ, iN, oU, iC, oZ, iF, oW, iJ, oS, iM, oQ])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iH, oX, iO] ([oY, iG, oU, iN, oX, iI, oT, iI, oW, iF, oX, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iH, oY, iL] ([oT, iF, oT, iH, oQ, iF, oQ, iN, oU, iH, oY, iL])* --------------- Formula: (false R (! iG | (true U oU))) "output U always responds to input G" Formula is not satisfied! An error path is [iF, oQ, iF, oP, iN, oY, iG] ([oP, iC, oW, iO, oQ, iA, oP, iM, oV, iN, oT, iF, 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 [iF, oQ, iF, oP, iN, oY, iH, oX, iO, oY, iM] ([oQ, iF, oV, iL, oT, iH, oX, iN, oY, 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 [iF, oQ, iF, oP, iN, oY, iH, oX] ([iJ, oP, iI, oY, iA, oV, iL, oZ, iO, oW, iE, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iG, oU, iN, oY, iL] ([oX, iF, oW, iM, oX, iL, 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 [iF, oQ] ([iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iC, oX, iL, oR, iG, oW])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iL, oP, iE, oS, iL] ([oV, iE, oV, iN, oZ, iO, oQ, iO, oY, iA, oS, iL, oP, iE, oS, iL])* --------------- Formula: (false R (! iI | (true U oZ))) "output Z always responds to input I" Formula is not satisfied! An error path is [iF, oQ, iF, oP, iN, oY, iG, oP, iI] ([oP, iL, oR, iE, oV, iG, oY, iJ, oW, iH, oP, 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 [iF, oQ] ([iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iC, oX, iL, oR, iG, oW])* --------------- Formula: (! oV WU iF) "input F always precedes output V" Formula is satisfied. --------------- 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 [iF, oQ] ([iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iC, oX, iL, oR, iG, oW])* --------------- 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 not satisfied! An error path is [iF, oQ, iF, oP, iN, oY, iA, oS, iF, oQ, iJ, oT, iF, oU, iE, oY, iO] ([oX, iF, oV, iE, oY, iA, oS, iF, oQ, iJ, oT, iF, oU, iE, oY, iO])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iG, oP, iC, oW] ([iO, oQ, iA, oP, iA, oW, iM, oT, iH, 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 [iF, oQ] ([iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iC, oX, iL, oR, iG, oW])* --------------- 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 satisfied. --------------- 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 not satisfied! An error path is [iF, oQ, iF, oP, iN, oY, iA, oS, iC, oX, iJ, oZ, iO, oQ] ([iE, oQ, iE, oR, iM, oW, iM, oS, iI, oT, iA, oY, iF, oY, iA, oS, iC, oX, iJ, oZ, iO, oQ])* --------------- 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 [iF, oQ, iF, oP] ([iN, oY, iA, oS, iF, oQ, iF, oR, iL, oZ, iJ, oS, iC, oS, iN, oQ])* --------------- 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 [iF, oQ] ([iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iC, oX, iL, oR, iG, oW])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iG, oP, iC, oW] ([iO, oQ, iA, oP, iA, oW, iM, oT, iH, oW])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iC] ([oX, iJ, oZ, iN, oZ, iE, oW, iG, oT, iJ, oZ, iG, oY, iA, oS, 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 [iF, oQ, iF, oP, iN, oY, iG, oP, iC, oW, iO, oQ, iN, oX, iA, oS] ([iE, oX, iL, oP, iC, oW, iO, oQ, iN, oX, iA, oS])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iF, oQ, iF, oR, iC, oT, iJ, oS, iH] ([oY, iC, oW, iJ, oQ, iF, oR, iC, oT, iJ, oS, iH])* --------------- 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 satisfied. --------------- Formula: (false R (! oZ | (false R (! iB | (true U oW))))) "output W responds to input B after output Z" Formula is satisfied. --------------- 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 not satisfied! An error path is [iF, oQ, iF, oP, iN, oY, iA, oS, iL, oP, iC, oR, iA, oW, iF] ([oZ, iC, oZ, iO, oT, iA, oS, iL, oP, iC, oR, iA, oW, iF])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iH, oX, iJ, oP, iI, oY, iI, oX, iA, oZ, iN, oS] ([iC, oY, iI, oX, iA, oZ, iN, oS])* --------------- 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 satisfied. --------------- 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 [iF, oQ] ([iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iC, oX, iL, oR, iG, oW])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iG, oU, iH, oV, iL] ([oQ, iC, oW, iO, oQ, iL, oY, iH, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iG, oU, iH, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iG, oU, iJ, oP, iI, oW, iN, oW, iM, oU] ([iA, oU, iJ, oP, iI, oW, iN, oW, iM, oU])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iH, oX] ([iJ, oP, iI, oY, iA, oV, iL, oZ, iO, oW, iE, oX])* --------------- 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 not satisfied! An error path is [iF, oQ, iF, oP, iN, oY, iA, oS, iC, oX, iJ] ([oZ, iN, oZ, iE, oW, iG, oT, iJ, oZ, iG, oY, iA, oS, iC, oX, iJ])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iH, oX, iO] ([oY, iG, oU, iN, oX, iI, oT, iI, oW, iF, oX, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iF, oQ, iF, oR] ([iC, oT, iI, oV, iN, oS, iH, oR])* --------------- 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 satisfied. --------------- 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 [iF, oQ, iF, oP, iN, oY, iG, oP, iC, oW] ([iO, oQ, iA, oP, iA, oW, iM, oT, iH, oW])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iC, oX, iJ, oZ, iN, oZ, iE, oW, iI] ([oU, iI, oT, iN, oZ, iE, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iF, oQ, iF, oR] ([iC, oT, iI, oV, iN, oS, iH, 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iF, oQ, iO] ([oX, iF, oY, iF, oT, iE, oS, iJ, oQ, 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 [iF, oQ] ([iF, oP, iN, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iC, oX, iL, oR, iG, oW])* --------------- 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 satisfied. --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iL, oP, iC, oR, iE] ([oP, iA, oQ, iE, oS, iJ, oW, iO, oY, iA, oS, iL, oP, iC, oR, 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 [iF, oQ, iF, oP, iN, oY, iH, oX, iJ, oP, iI, oY, iA, oV, iL, oZ, iO, oW, iN, oZ, iL, oR, iJ, oP, iI, oY, iM, oU] ([iC, oQ, iC, oU, iC, oU])* --------------- Formula: (false R (! oW | (false R (! iF | (true U oZ))))) "output Z responds to input F after output W" Formula is not satisfied! An error path is [iF, oQ, iF, oP, iN, oY, iG, oP, iC, oW, iO, oQ, iN, oX, iF] ([oT, iE, oY, iF, oX, iF])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iG, oP, iI, oP, iL, oR] ([iE, oV, iG, oY, iJ, oW, iH, oP, iI, oP, iL, oR])* --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iG, oU, iJ, oP, iI, oW] ([iJ, oQ, iF, oX, iE, oQ, iF, oP, iN, oY, iA, oS, iG, oU, iJ, oP, iI, oW])* --------------- 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 not satisfied! An error path is [iF, oQ, iF] ([oP, iN, oY, iA, oS, iF, oQ, iN, oU, iC, oZ, iC, oX, iL, oR, iG, oW, iF])* --------------- 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 satisfied. --------------- 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 [iF, oQ, iF, oP, iN, oY, iA, oS, iF, oQ, iJ, oT, iE, oU, iE, oV, iN] ([oW, iA, oX, iN, oY, iA, oS, iF, oQ, iJ, oT, iE, oU, iE, oV, 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 [iF, oQ, iF, oP, iN, oY, iG] ([oP, iC, oW, iO, oQ, iA, oP, iM, oV, iN, oT, iF, 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. --------------- 23 constraints satisfied, 77 unsatisfied.