Reachability problems: =============================== error_0 reachable via input sequence [G, O, E, Q, H, C, H, L, S, C] --------------- error_3 reachable via input sequence [G, O, E, Q, H, J, J, A, I, T] --------------- error_5 reachable via input sequence [G, O, E, Q, H, J, E, P, L, L] --------------- error_6 reachable via input sequence [G, O, E, Q, F, P, T, E, C, E] --------------- error_9 reachable via input sequence [G, O, E, Q, H, C, K, P, I, E] --------------- error_10 reachable via input sequence [G, O, E, Q, H, J, J, J, Q, K] --------------- error_11 reachable via input sequence [G, O, E, Q, H, C, K, S, A, T] --------------- error_12 reachable via input sequence [G, O, E, Q, H, C, B, K, T, T] --------------- error_16 reachable via input sequence [G, O, E, Q, F, J, K, P, R, J] --------------- error_18 reachable via input sequence [G, O, E, Q, F, P, T, C, E, S] --------------- error_19 reachable via input sequence [G, O, E, Q, H, C, H, L, J, D] --------------- error_21 reachable via input sequence [G, O, E, Q, F, J, K, M, I, Q] --------------- error_22 reachable via input sequence [G, O, E, Q, F, J, K, P, I, J] --------------- error_27 reachable via input sequence [G, O, E, Q, H, J, E, J, A, Q] --------------- error_29 reachable via input sequence [G, O, E, Q, F, P, T, C, L, C] --------------- error_32 reachable via input sequence [G, O, E, Q, F, P, I, R, I, C] --------------- error_34 reachable via input sequence [G, O, E, Q, F, P, T, C, A, L] --------------- error_38 reachable via input sequence [G, O, E, Q, H, C, K, P, Q, M] --------------- error_39 reachable via input sequence [G, O, E, Q, H, J, E, D, J, A] --------------- error_40 reachable via input sequence [G, O, E, Q, H, J, E, P, S, J] --------------- error_43 reachable via input sequence [G, O, E, Q, H, J, J, O, P, S] --------------- error_44 reachable via input sequence [G, O, E, Q, F, P, T, T, H, R] --------------- error_50 reachable via input sequence [G, O, E, Q, H, C, R, K, C, M] --------------- error_51 reachable via input sequence [G, O, E, Q, H, C, R, K, M, K] --------------- error_52 reachable via input sequence [G, O, E, Q, F, P, I, R, C, O] --------------- error_55 reachable via input sequence [G, O, E, Q, F, P, H, C, B, E] --------------- error_56 reachable via input sequence [G, O, E, Q, H, J, J, O, B, H] --------------- error_57 reachable via input sequence [G, O, E, Q, H, J, E, D, D, C] --------------- error_58 reachable via input sequence [G, O, E, Q, F, P, T, K, B, Q] --------------- error_60 reachable via input sequence [G, O, E, Q, H, J, J, M, G, H] --------------- error_62 reachable via input sequence [G, O, E, Q, H, C, B, K, C, D] --------------- error_64 reachable via input sequence [G, O, E, Q, F, J, K, H, S, B] --------------- error_65 reachable via input sequence [G, O, E, Q, H, C, K, S, Q, E] --------------- error_66 reachable via input sequence [G, O, E, Q, H, J, E, J, I, D] --------------- error_67 reachable via input sequence [G, O, E, Q, F, P, T, T, J, M] --------------- error_68 reachable via input sequence [G, O, E, Q, H, C, H, L, B, F] --------------- error_70 reachable via input sequence [G, O, E, Q, H, J, E, D, Q, E] --------------- error_71 reachable via input sequence [G, O, E, Q, H, C, K, P, A, Q] --------------- error_75 reachable via input sequence [G, O, E, Q, F, P, H, C, D, D] --------------- error_77 reachable via input sequence [G, O, E, Q, H, C, R, G, H, M] --------------- error_78 reachable via input sequence [G, O, E, Q, H, C, K, P, D, I] --------------- error_79 reachable via input sequence [G, O, E, Q, H, J, J, J, P, O] --------------- error_80 reachable via input sequence [G, O, E, Q, H, J, J, J, C, B] --------------- error_83 reachable via input sequence [G, O, E, Q, F, J, K, P, S, H] --------------- error_84 reachable via input sequence [G, O, E, Q, F, P, T, E, I, G] --------------- error_85 reachable via input sequence [G, O, E, Q, F, J, K, M, P, H] --------------- error_86 reachable via input sequence [G, O, E, Q, H, J, J, O, O, L] --------------- error_88 reachable via input sequence [G, O, E, Q, F, J, K, P, F, B] --------------- error_89 reachable via input sequence [G, O, E, Q, H, J, E, D, A, L] --------------- error_90 reachable via input sequence [G, O, E, Q, H, C, R, K, D, B] --------------- error_92 reachable via input sequence [G, O, E, Q, F, J, K, M, O, G] --------------- error_93 reachable via input sequence [G, O, E, Q, H, C, H, L, F, R] --------------- error_95 reachable via input sequence [G, O, E, Q, F, P, T, T, R, Q] --------------- error_96 reachable via input sequence [G, O, E, Q, H, C, K, K, B, Q] --------------- error_97 reachable via input sequence [G, O, E, Q, H, C, B, K, A, J] --------------- error_98 reachable via input sequence [G, O, E, Q, H, J, J, M, P, L] --------------- error_99 reachable via input sequence [G, O, E, Q, H, J, J, O, F, G] --------------- All other errors unreachable LTL problems: =============================== Formula: (! (true U (oU & X (true U oX))) | (! oU U iM)) "input M always precedes output U, output X" Formula is satisfied. --------------- Formula: (false R (! ((iI & ! iP) & (true U iP)) | ((! iF | (! iP U (oX & ! iP))) U iP))) "output X responds to input F between input I and input P" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iP, oY, iR, oW, iI, oY, iF, oV, iA, oV, iP] ([oY, iP, oY, iR, oW, iI, oY, iF, oV, iA, oV, iP])* --------------- Formula: (false R (! oZ | ((! iQ | (! iK U ((oY & ! iK) & X (! iK U oW)))) U (iK | (false R (! iQ | (oY & X (true U oW)))))))) "output Y, output W responds to input Q after output Z until input K" Formula is satisfied. --------------- Formula: (! (true U iO) | (! ((oZ & ! iO) & X (! iO U (oU & ! iO))) U (iO | iM))) "input M precedes output Z, output U before input O" Formula is satisfied. --------------- Formula: (false R (! iR | ((! iO | (! iC U (((oW & ! iC) & ! oX) & X ((! iC & ! oX) U oU)))) U (iC | (false R (! iO | ((oW & ! oX) & X (! oX U oU)))))))) "output W, output U without output X responds to input O after input R until input C" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iP, oY, iR, oW, iL, oV, iO] ([oY, iQ, oV, iF, oW, iR, oW, iL, oV, iO])* --------------- Formula: ((false R ! iN) | (! iN U (iN & (! (true U (oW & X (true U oU))) | (! oW U iQ))))) "input Q precedes output W, output U after input N" Formula is satisfied. --------------- Formula: (false R (! ((iG & ! iQ) & (true U iQ)) | (! oU U (iJ | iQ)))) "input J precedes output U between input G and input Q" Formula is satisfied. --------------- Formula: (! (true U iB) | (! ((oV & ! iB) & X (! iB U (oU & ! iB))) U (iB | iO))) "input O precedes output V, output U before input B" Formula is satisfied. --------------- Formula: (false R (! ((iC & ! oU) & (true U oU)) | (! oX U (iD | oU)))) "input D precedes output X between input C and output U" Formula is satisfied. --------------- Formula: (false R (! iT | ((! iQ | (! iE U (((oU & ! iE) & ! oV) & X ((! iE & ! oV) U oY)))) U (iE | (false R (! iQ | ((oU & ! oV) & X (! oV U oY)))))))) "output U, output Y without output V responds to input Q after input T until input E" Formula is not satisfied! An error path is [iG, oW, iF, oV, iG, oX, iS, oY, iT, oW, iP, oW, iQ] ([oY, iH, oY, iT, oY, iF, oV, iG, oX, iS, oY, iT, oW, iP, oW, iQ])* --------------- Formula: (false R (iT & (! X (true U iD) | X (true U (iD & (true U oW)))))) "output W always responds to input T, input D" Formula is not satisfied! An error path is [iG, oW] ([iF, oV, iE, oW, iC, oY, iF, oY, iI, oW, iF, oV, iR, oX, iI, oW])* --------------- Formula: (! (true U oY) | (! oY U ((iR & ! oY) & X (! oY U iH)))) "input R, input H always precedes output Y" Formula is not satisfied! An error path is [iG, oW, iH, oY] ([iP, oY, iF, oW, iG, oY, iD, oV, iK, oW, iF, oW, iF, oY])* --------------- Formula: (false R (! iM | (false R (! iG | (true U oU))))) "output U responds to input G after input M" Formula is not satisfied! An error path is [iG, oW, iF, oV, iG, oX, iS, oY, iM, oV, iS, oX, iG] ([oY, iL, oW, iC, oY, iS, oX, iG])* --------------- Formula: (false R (! (iN & (true U iQ)) | ((! iL | (! iQ U ((oY & ! iQ) & X (! iQ U oZ)))) U iQ))) "output Y, output Z responds to input L between input N and input Q" Formula is satisfied. --------------- Formula: (false R (! oZ | ((! iP | (! iE U (((oU & ! iE) & ! oV) & X ((! iE & ! oV) U oX)))) U (iE | (false R (! iP | ((oU & ! oV) & X (! oV U oX)))))))) "output U, output X without output V responds to input P after output Z until input E" Formula is satisfied. --------------- Formula: (false R (! iR | (false R (! iK | ((oZ & ! oW) & X (! oW U oY)))))) "output Z, output Y without output W responds to input K after input R" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iC, oY, iR, oX, iQ, oX, iK] ([oV, iM, oW, iB, oX, iR, oX, iQ, oX, iK])* --------------- Formula: (false R (iP & (! X (true U iB) | X (true U (iB & (true U oV)))))) "output V always responds to input P, input B" Formula is not satisfied! An error path is [iG, oW] ([iF, oV, iE, oW, iC, oY, iF, oY, iI, oW, iF, oV, iR, oX, iI, oW])* --------------- Formula: (! (true U iM) | (! oZ U (oX | iM))) "output X precedes output Z before input M" Formula is satisfied. --------------- Formula: (false R (! oZ | (false R (! iP | (oW & X (true U oU)))))) "output W, output U responds to input P after output Z" Formula is satisfied. --------------- Formula: (false R (oY & (! ! iH | ((! iM | (! iH U (oW & ! iH))) WU iH)))) "output W responds to input M after output Y until input H" Formula is not satisfied! An error path is [iG, oW] ([iF, oV, iE, oW, iC, oY, iF, oY, iI, oW, iF, oV, iR, oX, iI, oW])* --------------- Formula: (false R (! (iJ & (true U iE)) | (! ((oZ & ! iE) & X (! iE U (oW & ! iE))) U (iE | iP)))) "input P precedes output Z, output W between input J and input E" Formula is satisfied. --------------- Formula: (false R (! iP | (true U ((oY & ! oW) & X (! oW U oZ))))) "output Y, output Z without output W always responds to input P" Formula is not satisfied! An error path is [iG, oW, iH, oY, iP] ([oY, iF, oW, iG, oY, iD, oV, iK, oW, iF, oW, iF, oY, iP])* --------------- Formula: (false R (! iM | (false R (! iE | (true U oW))))) "output W responds to input E after input M" Formula is not satisfied! An error path is [iG, oW, iH, oY, iP, oY, iF, oW, iM, oY, iO, oX, iE] ([oX, iP, oX, iJ, oY, iE])* --------------- Formula: (false R (! iQ | (false R (! iE | (oZ & X (true U oU)))))) "output Z, output U responds to input E after input Q" Formula is not satisfied! An error path is [iG, oW, iO, oW, iE, oX, iQ, oX, iG, oV, iE] ([oX, iD, oX, iQ, oX, iQ, oY, iE, oV, iE])* --------------- Formula: (false R (! iS | (false R (! iK | (oU & X (true U oZ)))))) "output U, output Z responds to input K after input S" Formula is not satisfied! An error path is [iG, oW, iF, oV, iM, oX, iI, oX, iS, oX, iK] ([oV, iP, oX, iE, oW, iS, oW, iK])* --------------- Formula: (false R (! iA | ((iI & (! X (! iO U iC) | X (! iO U (iC & (true U oV))))) U (iO | (false R (iI & (! X (! iO U iC) | X (! iO U (iC & (true U oV)))))))))) "output V responds to input I, input C after input A until input O" Formula is not satisfied! An error path is [iG, oW, iO, oW, iA] ([oW, iH, oW, iS, oX, iF, oX, iM, oW, iT, oY, iT, oV, iF, oW, iA])* --------------- Formula: (! (true U (oZ & X (true U oU))) | (! oZ U iR)) "input R always precedes output Z, output U" Formula is satisfied. --------------- Formula: (false R (! iS | (false R (! iP | ((oX & ! oU) & X (! oU U oY)))))) "output X, output Y without output U responds to input P after input S" Formula is not satisfied! An error path is [iG, oW, iF, oV, iG, oX, iS, oY, iT, oW, iP] ([oW, iK, oY, iK, oW, iI, oX, iP])* --------------- Formula: (false R (! (iQ & (true U iF)) | (! oU U (iF | ((iT & ! oU) & X (! oU U iR)))))) "input T, input R precedes output U between input Q and input F" Formula is satisfied. --------------- Formula: (false R (iK & (! ! oW | (! oZ WU (iM | oW))))) "input M precedes output Z after input K until output W" Formula is not satisfied! An error path is [iG, oW] ([iF, oV, iE, oW, iC, oY, iF, oY, iI, oW, iF, oV, iR, oX, iI, oW])* --------------- Formula: (! (true U oY) | ((iQ & (! X (! oY U iI) | X (! oY U (iI & (true U oW))))) U oY)) "output W responds to input Q, input I before output Y" Formula is not satisfied! An error path is [iG, oW, iH, oY] ([iP, oY, iF, oW, iG, oY, iD, oV, iK, oW, iF, oW, iF, oY])* --------------- Formula: ((false R ! iG) | (true U (iG & (! oZ WU iE)))) "input E precedes output Z after input G" Formula is satisfied. --------------- Formula: (false R (! oZ | (! (true U oX) | (! oX U (oU | ((iF & ! oX) & X (! oX U iK))))))) "input F, input K precedes output X after output Z until output U" Formula is satisfied. --------------- Formula: (false R (! oV | ((! iT | (! iA U ((oW & ! iA) & X (! iA U oU)))) U (iA | (false R (! iT | (oW & X (true U oU)))))))) "output W, output U responds to input T after output V until input A" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iC, oY, iT] ([oX, iT, oW, iC, oY, iO, oV, iL, oY, iT])* --------------- Formula: (! (true U iS) | (! ((oZ & ! iS) & X (! iS U (oY & ! iS))) U (iS | iD))) "input D precedes output Z, output Y before input S" Formula is satisfied. --------------- Formula: (! (true U iJ) | (! ((oX & ! iJ) & X (! iJ U (oW & ! iJ))) U (iJ | iI))) "input I precedes output X, output W before input J" Formula is not satisfied! An error path is [iG, oW, iF, oV, iM, oX, iO, oW, iO, oV, iJ] ([oV, iI, oY, iD, oW, iS, oV, iJ])* --------------- Formula: ((false R ! iR) | (! iR U (iR & (! (true U oV) | (! oV U ((iL & ! oV) & X (! oV U iG))))))) "input L, input G precedes output V after input R" Formula is not satisfied! An error path is [iG, oW, iF, oV, iM, oX, iI, oX, iR, oV] ([iC, oX, iR, oY, iI, oY, iL, oW])* --------------- Formula: (false R (! iB | ((! iI | (! iK U (((oU & ! iK) & ! oW) & X ((! iK & ! oW) U oV)))) U (iK | (false R (! iI | ((oU & ! oW) & X (! oW U oV)))))))) "output U, output V without output W responds to input I after input B until input K" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iE, oX, iB, oY, iC, oV, iF, oY, iI] ([oW, iP, oY, iB, oY, iS, oW, iA, oV, iS, oX, iA, oX, iC, oV, iF, oY, iI])* --------------- Formula: (false R (! (iE & (true U oY)) | ((! iA | (! oY U (((oW & ! oY) & ! oX) & X ((! oY & ! oX) U oZ)))) U oY))) "output W, output Z without output X responds to input A betwen input E and output Y" Formula is not satisfied! An error path is [iG, oW, iO, oW, iE, oX, iL, oX, iA, oW, iC, oY] ([iB, oW, iL, oY, iF, oX, iH, oY, iO, oW, iE, oX, iL, oX, iA, oW, iC, oY])* --------------- Formula: (false R (! (iO & (true U iF)) | ((! iN | (! iF U (((oX & ! iF) & ! oW) & X ((! iF & ! oW) U oV)))) U iF))) "output X, output V without output W responds to input N betwen input O and input F" Formula is satisfied. --------------- Formula: (! (true U iQ) | ((! iH | (! iQ U ((oZ & ! iQ) & X (! iQ U oU)))) U iQ)) "output Z, output U responds to input H before input Q" Formula is not satisfied! An error path is [iG, oW, iH, oY, iP, oY, iF, oW, iQ] ([oW, iD, oV, iF, oX, iA, oV, iK, oY, iQ])* --------------- Formula: (false R (! (iG & (true U iE)) | (! ((oU & ! iE) & X (! iE U (oZ & ! iE))) U (iE | iT)))) "input T precedes output U, output Z between input G and input E" Formula is satisfied. --------------- Formula: (false R (! oW | (false R (iN & (! X (true U iR) | X (! iR U (iR & (true U oZ)))))))) "output Z responds to input N, input R after output W" Formula is not satisfied! An error path is [iG, oW] ([iF, oV, iE, oW, iC, oY, iF, oY, iI, oW, iF, oV, iR, oX, iI, oW])* --------------- Formula: ((false R ! iB) | (true U (iB & (! oX WU iF)))) "input F precedes output X after input B" Formula is not satisfied! An error path is [iG, oW, iH, oY, iP, oY, iS, oX, iJ, oW, iB, oX] ([iK, oY, iL, oY, iO, oW, iB, oX])* --------------- Formula: ((false R ! iL) | (true U (iL & (! oU WU iJ)))) "input J precedes output U after input L" Formula is satisfied. --------------- Formula: (false R (iE & (! ! iA | ((! iK | (! iA U (oW & ! iA))) WU iA)))) "output W responds to input K after input E until input A" Formula is not satisfied! An error path is [iG, oW] ([iF, oV, iE, oW, iC, oY, iF, oY, iI, oW, iF, oV, iR, oX, iI, oW])* --------------- Formula: (false R (! (iL & (true U iT)) | ((! iA | (! iT U (((oV & ! iT) & ! oX) & X ((! iT & ! oX) U oU)))) U iT))) "output V, output U without output X responds to input A betwen input L and input T" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iC, oY, iT, oX, iL, oY, iP, oY, iA, oX, iT] ([oX, iF, oV, iE, oW, iC, oY, iT, oX, iL, oY, iP, oY, iA, oX, iT])* --------------- Formula: (! (true U iL) | (! ((oZ & ! iL) & X (! iL U (oY & ! iL))) U (iL | iC))) "input C precedes output Z, output Y before input L" Formula is satisfied. --------------- Formula: (false R (iQ & (! X (true U iE) | X (true U (iE & (true U oW)))))) "output W always responds to input Q, input E" Formula is not satisfied! An error path is [iG, oW] ([iF, oV, iE, oW, iC, oY, iF, oY, iI, oW, iF, oV, iR, oX, iI, oW])* --------------- Formula: (false R (! iN | (true U oY))) "output Y always responds to input N" Formula is satisfied. --------------- Formula: ((false R ! oZ) | (true U (oZ & (! oV WU iG)))) "input G precedes output V after output Z" Formula is satisfied. --------------- Formula: (! oX WU iE) "input E always precedes output X" Formula is not satisfied! An error path is [iG, oW, iF, oV, iG, oX] ([iS, oY, iF, oY, iJ, oV, iE, oW, iK, oW, iJ, oX])* --------------- Formula: (! (true U iD) | ((iI & (! X (! iD U iH) | X (! iD U (iH & (true U oY))))) U iD)) "output Y responds to input I, input H before input D" Formula is not satisfied! An error path is [iG, oW, iH, oY, iP, oY, iF, oW, iG, oY, iD] ([oV, iQ, oW, iR, oW, iL, oW, iD])* --------------- Formula: (false R (! iG | ((! iK | (! iS U ((oZ & ! iS) & X (! iS U oU)))) U (iS | (false R (! iK | (oZ & X (true U oU)))))))) "output Z, output U responds to input K after input G until input S" Formula is not satisfied! An error path is [iG, oW, iO, oW, iA, oW, iG, oX, iK] ([oV, iG, oX, iG, oY, iJ, oW, iB, oY, iT, oV, iJ, oV, iI, oY, iR, oW, iP, oV, iO, oW, iA, oW, iG, oX, iK])* --------------- Formula: (false R (! iI | ((! iM | (! oY U ((oU & ! oY) & X (! oY U oV)))) U (oY | (false R (! iM | (oU & X (true U oV)))))))) "output U, output V responds to input M after input I until output Y" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iP, oY, iR, oW, iL, oV, iI, oX, iM] ([oW, iI, oW, iJ, oW, iA, oY, iC, oW, iH, oY, iE, oW, iO, oW, iE, oX, iL, oX, iA, oW, iH, oW, iD, oX, iO, oW, iE, oY, iO, oW, iI, oX, iM])* --------------- Formula: (false R (iH & (! ! iF | ((! iE | (! iF U (oY & ! iF))) WU iF)))) "output Y responds to input E after input H until input F" Formula is not satisfied! An error path is [iG, oW] ([iF, oV, iE, oW, iC, oY, iF, oY, iI, oW, iF, oV, iR, oX, iI, oW])* --------------- Formula: ((false R ! iO) | (! iO U (iO & (! (true U oV) | (! oV U ((iJ & ! oV) & X (! oV U iA))))))) "input J, input A precedes output V after input O" Formula is not satisfied! An error path is [iG, oW, iO, oW, iL, oV] ([iM, oW, iJ, oX, iH, oV, iL, oW, iA, oV, iP, oY, iG, oX, iO, oW, iL, oV])* --------------- Formula: ((false R ! iH) | (! iH U (iH & (! (true U (oZ & X (true U oU))) | (! oZ U iP))))) "input P precedes output Z, output U after input H" Formula is satisfied. --------------- Formula: (false R (! iI | (true U oY))) "output Y always responds to input I" Formula is not satisfied! An error path is [iG, oW, iF, oV, iM, oX, iI] ([oX, iR, oV, iC, oX, iF, oW, iA, oW, iG, oV, iI])* --------------- Formula: (! (true U (oV & X (true U oZ))) | (! oV U iR)) "input R always precedes output V, output Z" Formula is satisfied. --------------- Formula: (false R (! iA | (false R (iK & (! X (true U iG) | X (! iG U (iG & (true U oV)))))))) "output V responds to input K, input G after input A" Formula is not satisfied! An error path is [iG, oW, iO, oW, iA] ([oW, iH, oW, iS, oX, iF, oX, iM, oW, iT, oY, iT, oV, iF, oW, iA])* --------------- Formula: (! (true U iD) | ((iJ & (! X (! iD U iI) | X (! iD U (iI & (true U oY))))) U iD)) "output Y responds to input J, input I before input D" Formula is not satisfied! An error path is [iG, oW, iH, oY, iP, oY, iF, oW, iG, oY, iD] ([oV, iQ, oW, iR, oW, iL, oW, iD])* --------------- Formula: (! (true U iJ) | ((! iG | (! iJ U (((oY & ! iJ) & ! oX) & X ((! iJ & ! oX) U oV)))) U iJ)) "output Y, output V without output X responds to input G before input J" Formula is not satisfied! An error path is [iG, oW, iH, oY, iP, oY, iS, oX, iJ] ([oW, iB, oX, iP, oY, iJ, oY, iQ, oV, iJ])* --------------- Formula: (false R (! iK | (false R (! iH | (true U oV))))) "output V responds to input H after input K" Formula is not satisfied! An error path is [iG, oW, iH, oY, iP, oY, iF, oW, iG, oY, iK, oX, iC, oW, iH] ([oX, iE, oX, iH, oY, iP, oY, iF, oW, iG, oY, iK, oX, iC, oW, iH])* --------------- Formula: (! (true U iG) | ((! iD | (! iG U (oZ & ! iG))) U iG)) "output Z responds to input D before input G" Formula is satisfied. --------------- Formula: (false R (! (iN & (true U iJ)) | ((iI & (! X (! iJ U iM) | X (! iJ U (iM & (true U oX))))) U iJ))) "output X responds to input I, input M between input N and input J" Formula is satisfied. --------------- Formula: (false R (! (oX & (true U iR)) | ((! iG | (! iR U (((oW & ! iR) & ! oZ) & X ((! iR & ! oZ) U oY)))) U iR))) "output W, output Y without output Z responds to input G betwen output X and input R" Formula is not satisfied! An error path is [iG, oW, iF, oV, iG, oX, iS, oY, iM, oV, iS, oX, iG, oY, iR] ([oW, iM, oX, iM, oV, iS, oX, iG, oY, iR])* --------------- Formula: (false R (! iJ | (false R (iQ & (! X (true U iK) | X (! iK U (iK & (true U oX)))))))) "output X responds to input Q, input K after input J" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iP, oY, iJ] ([oW, iA, oY, iC, oW, iH, oY, iJ, oW, iJ])* --------------- Formula: (! (true U iH) | ((! iQ | (! iH U (oV & ! iH))) U iH)) "output V responds to input Q before input H" Formula is not satisfied! An error path is [iG, oW, iO, oW, iE, oX, iQ, oX, iH] ([oV, iC, oV, iB, oX, iK, oV, iT, oW, iH, oV, iO, oW, iE, oX, iQ, oX, iH])* --------------- Formula: (! oX WU iM) "input M always precedes output X" Formula is not satisfied! An error path is [iG, oW, iF, oV, iG, oX] ([iS, oY, iF, oY, iJ, oV, iE, oW, iK, oW, iJ, oX])* --------------- Formula: (! (true U iJ) | (! oU U (iJ | ((iP & ! oU) & X (! oU U iI))))) "input P, input I precedes output U before input J" Formula is satisfied. --------------- Formula: (false R (! ((oV & ! iB) & (true U iB)) | (! oX U (iR | iB)))) "input R precedes output X between output V and input B" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iE, oX, iB] ([oY, iA, oX, iK, oW, iF, oY, iC, oY, iB])* --------------- Formula: (! (true U iB) | (! oW U (iS | iB))) "input S precedes output W before input B" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iE, oX, iB] ([oY, iA, oX, iK, oW, iF, oY, iC, oY, iB])* --------------- Formula: (! (true U iK) | ((iT & (! X (! iK U iQ) | X (! iK U (iQ & (true U oV))))) U iK)) "output V responds to input T, input Q before input K" Formula is not satisfied! An error path is [iG, oW, iO, oW, iA, oW, iG, oX, iK] ([oV, iG, oX, iG, oY, iJ, oW, iB, oY, iT, oV, iJ, oV, iI, oY, iR, oW, iP, oV, iO, oW, iA, oW, iG, oX, iK])* --------------- Formula: (false R (! iP | (true U oV))) "output V always responds to input P" Formula is not satisfied! An error path is [iG, oW, iH, oY, iP] ([oY, iF, oW, iG, oY, iK, oX, iC, oW, iL, oX, iG, oY, iP])* --------------- Formula: (false R (! oX | (false R (! iB | (oV & X (true U oU)))))) "output V, output U responds to input B after output X" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iE, oX, iB] ([oY, iA, oX, iK, oW, iF, oY, iC, oY, iB])* --------------- Formula: (false R (! iF | (false R (iG & (! X (true U iJ) | X (! iJ U (iJ & (true U oX)))))))) "output X responds to input G, input J after input F" Formula is not satisfied! An error path is [iG, oW, iF] ([oV, iE, oW, iC, oY, iF, oY, iI, oW, iF, oV, iR, oX, iI, oW, iF])* --------------- Formula: (false R (! iQ | ((! iS | (! iA U ((oV & ! iA) & X (! iA U oU)))) U (iA | (false R (! iS | (oV & X (true U oU)))))))) "output V, output U responds to input S after input Q until input A" Formula is not satisfied! An error path is [iG, oW, iH, oY, iP, oY, iF, oW, iG, oY, iQ, oV, iS] ([oX, iG, oX, iL, oV, iQ, oV, iS])* --------------- Formula: (false R (! (iH & (true U iQ)) | ((! iG | (! iQ U ((oU & ! iQ) & X (! iQ U oV)))) U iQ))) "output U, output V responds to input G between input H and input Q" Formula is not satisfied! An error path is [iG, oW, iH, oY, iP, oY, iF, oW, iG, oY, iQ] ([oV, iR, oX, iC, oW, iL, oY, iQ])* --------------- Formula: (false R (! iF | ((! iC | (! iO U (((oV & ! iO) & ! oX) & X ((! iO & ! oX) U oY)))) U (iO | (false R (! iC | ((oV & ! oX) & X (! oX U oY)))))))) "output V, output Y without output X responds to input C after input F until input O" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iC] ([oY, iF, oY, iI, oW, iF, oV, iR, oX, iS, oW, iC])* --------------- Formula: (false R (iH & (! X (true U iO) | X (true U (iO & (true U oX)))))) "output X always responds to input H, input O" Formula is not satisfied! An error path is [iG, oW] ([iF, oV, iE, oW, iC, oY, iF, oY, iI, oW, iF, oV, iR, oX, iI, oW])* --------------- Formula: (false R (! oY | (false R (! iR | (oV & X (true U oZ)))))) "output V, output Z responds to input R after output Y" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iC, oY, iR] ([oX, iQ, oX, iB, oY, iD, oY, iE, oY, iR])* --------------- Formula: (false R (! iP | (false R (! iK | (true U oX))))) "output X responds to input K after input P" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iP, oY, iJ, oW, iA, oY, iK] ([oV, iC, oW, iC, oY, iE, oW, iP, oY, iJ, oW, iA, oY, iK])* --------------- Formula: (false R (! iD | (false R (! iC | ((oX & ! oU) & X (! oU U oY)))))) "output X, output Y without output U responds to input C after input D" Formula is not satisfied! An error path is [iG, oW, iF, oV, iM, oX, iO, oW, iO, oV, iJ, oV, iD, oX, iC] ([oV, iG, oV, iO, oW, iO, oV, iJ, oV, iD, oX, iC])* --------------- Formula: (! (true U oZ) | ((iQ & (! X (! oZ U iC) | X (! oZ U (iC & (true U oU))))) U oZ)) "output U responds to input Q, input C before output Z" Formula is satisfied. --------------- Formula: (false R (! (iM & (true U iG)) | (! oV U (iG | ((iO & ! oV) & X (! oV U iQ)))))) "input O, input Q precedes output V between input M and input G" Formula is not satisfied! An error path is [iG, oW, iF, oV, iG, oX, iS, oY, iM, oV, iS, oX, iG] ([oY, iL, oW, iC, oY, iS, oX, iG])* --------------- Formula: (! (true U iE) | (! oU U (iT | iE))) "input T precedes output U before input E" Formula is satisfied. --------------- Formula: (false R (oZ & (! ! iM | ((! iB | (! iM U (oY & ! iM))) WU iM)))) "output Y responds to input B after output Z until input M" Formula is not satisfied! An error path is [iG, oW] ([iF, oV, iE, oW, iC, oY, iF, oY, iI, oW, iF, oV, iR, oX, iI, oW])* --------------- Formula: (! (true U oU) | (! oU U ((iA & ! oU) & X (! oU U iM)))) "input A, input M always precedes output U" Formula is satisfied. --------------- Formula: ((false R ! iK) | (! iK U (iK & (! (true U oX) | (! oX U ((oY & ! oX) & X (! oX U iD))))))) "output Y, input D precedes output X after input K" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iP, oY, iJ, oW, iK, oX] ([iK, oY, iD, oW, iF, oV, iK, oX])* --------------- Formula: (false R (! oV | (false R (! iG | ((oY & ! oW) & X (! oW U oZ)))))) "output Y, output Z without output W responds to input G after output V" Formula is not satisfied! An error path is [iG, oW, iF, oV, iG] ([oX, iS, oY, iF, oY, iJ, oV, iE, oW, iK, oW, iO, oY, iG])* --------------- Formula: (false R (! iT | (false R (! iE | (oX & X (true U oY)))))) "output X, output Y responds to input E after input T" Formula is not satisfied! An error path is [iG, oW, iF, oV, iG, oX, iS, oY, iT, oW, iE] ([oY, iF, oV, iP, oW, iI, oX, iT, oW, iE])* --------------- Formula: (false R (iC & (! X (true U iP) | X (true U (iP & (true U oZ)))))) "output Z always responds to input C, input P" Formula is not satisfied! An error path is [iG, oW] ([iF, oV, iE, oW, iC, oY, iF, oY, iI, oW, iF, oV, iR, oX, iI, oW])* --------------- Formula: (! (true U oU) | (! oU U ((oV & ! oU) & X (! oU U iA)))) "output V, input A always precedes output U" Formula is satisfied. --------------- Formula: (false R (! iC | (false R (! iF | ((oV & ! oY) & X (! oY U oZ)))))) "output V, output Z without output Y responds to input F after input C" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iC, oY, iF] ([oY, iL, oY, iS, oV, iP, oY, iR, oX, iF])* --------------- Formula: (false R (! iQ | ((! ((oU & ! iL) & X (! iL U (oX & ! iL))) U (iL | iI)) | (false R ! (oU & X (true U oX)))))) "input I precedes output U, output X after input Q until input L" Formula is satisfied. --------------- Formula: (false R (! iT | (true U oV))) "output V always responds to input T" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iC, oY, iT] ([oX, iT, oW, iP, oX, iD, oY, iI, oX, iT])* --------------- Formula: (false R (iT & (! ! iS | (! oX WU (oZ | iS))))) "output Z precedes output X after input T until input S" Formula is not satisfied! An error path is [iG, oW] ([iF, oV, iE, oW, iC, oY, iF, oY, iI, oW, iF, oV, iR, oX, iI, oW])* --------------- Formula: (! (true U oY) | (! oZ U (iM | oY))) "input M precedes output Z before output Y" Formula is satisfied. --------------- Formula: (false R (! iJ | (true U (oY & X (true U oV))))) "output Y, output V always responds to input J" Formula is not satisfied! An error path is [iG, oW, iF, oV, iE, oW, iP, oY, iJ] ([oW, iA, oY, iC, oW, iH, oY, iJ, oW, iJ])* --------------- 34 constraints satisfied, 66 unsatisfied.