Reachability problems: =============================== error_1 reachable via input sequence [Q, R, K, T, C, R, R, I] --------------- error_13 reachable via input sequence [Q, R, K, D, S, J, J, K] --------------- error_14 reachable via input sequence [Q, R, K, D, M, J, Q, N] --------------- error_19 reachable via input sequence [Q, R, K, D, M, L, E, H] --------------- error_20 reachable via input sequence [Q, R, K, T, C, R, A, K] --------------- error_21 reachable via input sequence [Q, R, K, T, C, R, S, S] --------------- error_27 reachable via input sequence [Q, R, K, T, C, S, B, G] --------------- error_31 reachable via input sequence [Q, R, K, D, L, S, L, F] --------------- error_32 reachable via input sequence [Q, R, K, D, S, B, D, E] --------------- error_33 reachable via input sequence [Q, R, K, D, S, B, L, I] --------------- error_38 reachable via input sequence [Q, R, K, D, S, M, B, L] --------------- error_39 reachable via input sequence [Q, R, K, D, M, J, E, T] --------------- error_42 reachable via input sequence [Q, R, K, T, C, R, E, E] --------------- error_43 reachable via input sequence [Q, R, K, D, M, L, L, B] --------------- error_46 reachable via input sequence [Q, R, K, D, S, M, Q, B] --------------- error_48 reachable via input sequence [Q, R, K, D, S, M, K, R] --------------- error_49 reachable via input sequence [Q, R, K, D, L, E, P, T] --------------- error_52 reachable via input sequence [Q, R, K, T, C, S, S, K] --------------- error_54 reachable via input sequence [Q, R, K, D, S, J, T, M] --------------- error_60 reachable via input sequence [Q, R, K, D, O, S, D, O] --------------- error_61 reachable via input sequence [Q, R, K, D, M, L, F, H] --------------- error_63 reachable via input sequence [Q, R, K, D, S, B, H, N] --------------- error_69 reachable via input sequence [Q, R, K, D, S, M, J, P] --------------- error_71 reachable via input sequence [Q, R, K, D, L, S, F, K] --------------- error_77 reachable via input sequence [Q, R, K, D, L, E, J, F] --------------- error_78 reachable via input sequence [Q, R, K, D, S, J, O, P] --------------- error_79 reachable via input sequence [Q, R, K, D, S, B, P, G] --------------- error_81 reachable via input sequence [Q, R, K, D, L, S, H, I] --------------- error_85 reachable via input sequence [Q, R, K, D, O, S, T, S] --------------- error_86 reachable via input sequence [Q, R, K, D, L, K, F, K] --------------- error_95 reachable via input sequence [Q, R, K, D, L, S, B, J] --------------- error_97 reachable via input sequence [Q, R, K, D, O, R, M, A] --------------- 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 not satisfied! An error path is [iQ, oV, iA, oU, iB, oX] ([iA, oU, iR, oY, iB, oV, iC, oV, iT, oU, iB, oX])* --------------- 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 satisfied. --------------- 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 not satisfied! An error path is [iB, oU, iA, oZ, iQ] ([oZ, iT, oV, iF, oW, iD, oW, iQ, oY, iE, oW, iQ])* --------------- 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 not satisfied! An error path is [iF, oW, iA, oX, iD, oX, iE, oX, iL, oZ, iT, oU, iO] ([oV, iK, oZ, iR, oZ, iT, oU, iO])* --------------- 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 [iB, oU, iA, oZ, iR, oY, iK, oV, iA, oX, iO] ([oW, iO, oV, iM, oY, iA, oX, 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 not satisfied! An error path is [iQ, oV, iA, oU, iB] ([oX, iA, oU, iR, oY, iB, oV, iC, oV, iT, oU, iB])* --------------- 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 not satisfied! An error path is [iQ, oV, iJ, oV, iK, oW, iO, oZ, iE, oV, iC, oX, iL, oU] ([iB, oZ, iE, oV, iC, oX, iL, oU])* --------------- 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 [iF, oW, iD, oW, iK, oX, iK, oZ, iT, oV, iQ] ([oX, iT, oU, iS, oV, 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 [iQ, oV] ([iR, oW, iK, oZ, iT, oU, iK, oY, iF, oU, iF, oV, iQ, 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 [iB, oU, iA, oZ, iR, oY, iK, oV] ([iA, oX, iO, oW, iO, oV, iM, oY])* --------------- Formula: (false R (! iM | (false R (! iG | (true U oU))))) "output U responds to input G after input M" Formula is satisfied. --------------- 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 not satisfied! An error path is [iF, oW, iD, oW, iL, oX, iS, oZ, iP] ([oW, iL, oU, iJ, oY, iD, oV, iA, oW, iE, oU, iA, oY, iQ, oZ, iL, oV, iH, oZ, iC, oZ, iJ, oU, iH, oZ, iC, oW, iP, oW, iE, oV, iP, oZ, iP])* --------------- 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 [iQ, oV, iR, oW, iK] ([oZ, iT, oU, iK, oY, iF, oU, iF, oV, iQ, oW, iR, oW, 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 [iQ, oV] ([iR, oW, iK, oZ, iT, oU, iK, oY, iF, oU, iF, oV, iQ, oW])* --------------- Formula: (! (true U iM) | (! oZ U (oX | iM))) "output X precedes output Z before input M" Formula is not satisfied! An error path is [iF, oW, iQ, oZ, iC, oZ, iJ, oU, iE, oW, iM] ([oZ, iD, oZ, iH, oU, iS, oZ, iJ, oU, iE, oW, iM])* --------------- 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 not satisfied! An error path is [iF, oW, iD, oW, iL, oX, iS, oZ, iP] ([oW, iL, oU, iM, oX, iK, oX, iS, oZ, iP])* --------------- 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 [iQ, oV] ([iR, oW, iK, oZ, iT, oU, iK, oY, iF, oU, iF, oV, iQ, 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 not satisfied! An error path is [iF, oW, iQ, oZ, iC, oZ, iJ, oU, iH, oZ, iC, oW, iE] ([oY, iD, oZ, iJ, oU, iH, oY, iF, oU, iE, oU, iB, oZ, iE, oV, iD, oZ, iJ, oU, iH, oZ, iC, oW, iE])* --------------- 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 [iF, oW, iD, oW, iL, oX, iS, oZ, iP] ([oW, iL, oU, iM, oX, iK, oX, iS, oZ, 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 [iF, oW, iD, oW, iF, oU, iH, oY, iF, oU, iM, oV, iA, oV, iE] ([oX, iF, oX, iO, oX, iL, oY, iF, oU, iK, oU, iL, oV, iC, oU, iH, oY, iF, oU, iM, oV, iA, oV, 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 [iF, oW, iD, oW, iQ, oW, iS, oW, iE] ([oU, iS, oU, iB, oZ, iK, oV, iF, oW, iQ, oW, iS, oW, 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 [iF, oW, iD, oW, iL, oX, iK, oW, iF, oZ, iS, oV, iK] ([oZ, iT, oW, iF, oZ, iS, oV, 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 [iB, oU, iA, oZ] ([iQ, oZ, iT, oV, iF, oW, iD, oW, iQ, oY, iE, oW])* --------------- Formula: (! (true U (oZ & X (true U oU))) | (! oZ U iR)) "input R always precedes output Z, output U" Formula is not satisfied! An error path is [iF, oW, iQ, oZ, iC, oZ, iJ, oU] ([iE, oW, iM, oZ, iD, oZ, iH, oU, iS, oZ, iJ, oU])* --------------- 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 [iF, oW, iD, oW, iL, oX, iS, oZ, iP] ([oW, iL, oU, iM, oX, iK, oX, iS, oZ, 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 not satisfied! An error path is [iQ, oV, iA, oU, iD, oV, iQ, oZ, iF] ([oV, iD, oZ, iF, oV, iF, oU, iD, oV, iQ, oZ, iF])* --------------- 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 [iQ, oV] ([iR, oW, iK, oZ, iT, oU, iK, oY, iF, oU, iF, oV, iQ, 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 [iB, oU, iA, oZ, iR, oY, iK, oV] ([iA, oX, iO, oW, iO, oV, iM, 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 not satisfied! An error path is [iB, oU, iA, oZ, iQ, oZ, iJ, oV, iO, oX] ([iQ, oV, iF, oW, iL, oX])* --------------- 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 [iQ, oV, iR, oW, iK, oZ, iT] ([oU, iK, oY, iF, oU, iF, oV, iQ, oW, iR, oW, iK, oZ, 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 not satisfied! An error path is [iF, oW, iQ, oZ, iC, oZ, iL, oZ, iF, oY, iJ, oY, iS] ([oU, iL, oY, iS])* --------------- 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 [iF, oW, iD, oW, iL, oX, iK, oW, iE, oZ, iJ] ([oV, iK, oX, iT, oZ, 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 [iB, oU, iA, oZ, iR, oY, iK, oV] ([iA, oX, iO, oW, iO, oV, iM, oY])* --------------- 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 satisfied. --------------- 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 [iF, oW, iD, oW, iQ, oW, iS, oW, iE, oU, iA, oY] ([iM, oZ, iF, oV, iH, oW, iC, oY, iP, oY, iM, oU, iP, oW, iQ, oW, iS, oW, iE, oU, iA, 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 [iF, oW, iD, oW, iF, oU, iH, oY, iQ] ([oU, iF, oU, iA, oV, iS, oU, iH, 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 [iF, oW, iA, oX] ([iD, oX, iE, oX, iL, oZ, iM, oX, iB, oX, iD, oX])* --------------- 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 [iQ, oV, iA, oU, iB, oX] ([iA, oU, iR, oY, iB, oV, iC, oV, iT, oU, iB, oX])* --------------- Formula: ((false R ! iL) | (true U (iL & (! oU WU iJ)))) "input J precedes output U after input L" Formula is not satisfied! An error path is [iF, oW, iQ, oZ, iC, oZ, iL, oZ, iH, oU] ([iH, oU, iS, oV, iD, oZ, iH, oU])* --------------- 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 [iQ, oV] ([iR, oW, iK, oZ, iT, oU, iK, oY, iF, oU, iF, oV, iQ, 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 [iF, oW, iD, oW, iF, oU, iL, oV, iQ, oW, iB, oX, iA, oZ, iT] ([oW, iA, oW, iL, oY, iD, oX, iA, oU, iF, oX, iR, oU, iL, oV, iQ, oW, iB, oX, iA, oZ, 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 not satisfied! An error path is [iF, oW, iQ, oZ, iC, oZ, iJ, oU, iH, oZ, iC, oW, iE, oY, iL] ([oU, iD, oV, iB, oV, iD, oV, iH, oZ, iB, oU, iH, oY, iF, oU, iE, oU, iB, oZ, iE, oV, iD, oZ, iJ, oU, iH, oZ, iC, oW, iE, oY, iL])* --------------- 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 [iQ, oV] ([iR, oW, iK, oZ, iT, oU, iK, oY, iF, oU, iF, oV, iQ, 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 not satisfied! An error path is [iB, oU, iA, oZ, iQ, oZ, iT, oV] ([iF, oW, iO, oW, iF, oY, iM, oV])* --------------- Formula: (! oX WU iE) "input E always precedes output X" Formula is not satisfied! An error path is [iF, oW, iA, oX] ([iD, oX, iE, oX, iL, oZ, iM, oX, iB, oX, iD, 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 [iF, oW, iD, oW] ([iF, oU, iE, oV, iB, oV, iL, oW, iQ, oV, iM, oW])* --------------- 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 satisfied. --------------- 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 satisfied. --------------- 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 [iQ, oV] ([iR, oW, iK, oZ, iT, oU, iK, oY, iF, oU, iF, oV, iQ, 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 [iQ, oV, iJ, oV, iK, oW, iO, oZ, iE, oV] ([iC, oX, iL, oU, iB, oZ, iE, 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 not satisfied! An error path is [iF, oW, iQ, oZ, iC, oZ, iJ, oU, iH, oZ] ([iC, oW, iE, oY, iD, oZ, iJ, oU, iH, oY, iF, oU, iE, oU, iB, oZ, iE, oV, iD, oZ, iJ, oU, iH, oZ])* --------------- Formula: (false R (! iI | (true U oY))) "output Y always responds to input I" Formula is satisfied. --------------- Formula: (! (true U (oV & X (true U oZ))) | (! oV U iR)) "input R always precedes output V, output Z" Formula is not satisfied! An error path is [iQ, oV, iR, oW, iK, oZ] ([iT, oU, iK, oY, iF, oU, iF, oV, iQ, oW, iR, oW, iK, oZ])* --------------- 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 [iB, oU, iA, oZ] ([iQ, oZ, iT, oV, iF, oW, iD, oW, iQ, oY, iE, oW])* --------------- 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 [iF, oW, iD, oW] ([iF, oU, iE, oV, iB, oV, iL, oW, iQ, oV, iM, oW])* --------------- 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 satisfied. --------------- 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 [iF, oW, iD, oW, iK, oX, iK, oZ, iL, oZ, iH] ([oW, iS, oW, iD, oZ, 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 satisfied. --------------- 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 [iQ, oV, iJ, oV] ([iK, oW, iO, oZ, iB, oX, iF, oY, iB, oX, iH, oY])* --------------- 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 [iF, oW, iQ, oZ, iC, oZ, iJ, oU, iH] ([oZ, iF, oX, iE, oZ, iP, oW, iJ, oU, iH])* --------------- Formula: (! oX WU iM) "input M always precedes output X" Formula is not satisfied! An error path is [iF, oW, iA, oX] ([iD, oX, iE, oX, iL, oZ, iM, oX, iB, oX, iD, 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 not satisfied! An error path is [iF, oW, iD, oW, iF, oU, iH, oY, iJ] ([oX, iT, oU, iS, oV, iL, oZ, iT, oU, iH, oY, iJ])* --------------- 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 [iF, oW, iD, oW, iK, oX, iJ, oU, iR, oY, iB, oV, iK, oX, iB] ([oX, iJ, oU, iR, oY, iB, oV, iK, oX, 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 [iF, oW, iD, oW, iF, oU, iE, oV, iB] ([oV, iM, oU, iA, oZ, iC, oV, 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 [iF, oW, iD, oW, iK] ([oX, iJ, oU, iA, oV, iC, oZ, iH, oY, iP, oW, iK])* --------------- Formula: (false R (! iP | (true U oV))) "output V always responds to input P" Formula is not satisfied! An error path is [iF, oW, iD, oW, iL, oX, iS, oZ, iP] ([oW, iL, oU, iM, oX, iK, oX, iS, oZ, 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 [iF, oW, iA, oX, iD, oX, iE, oX, iT, oW, iB] ([oZ, iB, oU, iR, oW, 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 [iF, oW, iA, oX] ([iD, oX, iE, oX, iL, oZ, iM, oX, iB, oX, iD, oX])* --------------- 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 [iF, oW, iD, oW, iQ, oW, iS] ([oW, iD, oX, iD, oX, iP, oV, iM, oW, 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 satisfied. --------------- 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 [iF, oW, iQ, oZ, iC] ([oZ, iL, oZ, iH, oU, iH, oU, iS, oV, iH, oZ, 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 [iQ, oV] ([iR, oW, iK, oZ, iT, oU, iK, oY, iF, oU, iF, oV, iQ, 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 [iF, oW, iD, oW, iF, oU, iH, oY, iJ, oX, iR] ([oZ, iK, oZ, iD, oV, iM, oW, iF, oU, iH, oY, iJ, oX, 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 [iQ, oV, iA, oU, iB, oX, iD, oZ, iS, oV, iP, oV, iK, oY] ([iS, oV])* --------------- 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 [iF, oW, iD, oW, iF, oU, iC] ([oY, iA, oU, iL, oU, iK, oU, iH, oV, iB, oW, iF, oU, 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 not satisfied! An error path is [iB, oU, iA, oZ] ([iQ, oZ, iT, oV, iF, oW, iD, oW, iQ, oY, iE, oW])* --------------- 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 satisfied. --------------- Formula: (! (true U iE) | (! oU U (iT | iE))) "input T precedes output U before input E" Formula is not satisfied! An error path is [iF, oW, iD, oW, iF, oU, iE] ([oV, iB, oV, iD, oV, iH, oZ, iB, oU, iE])* --------------- 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 [iQ, oV] ([iR, oW, iK, oZ, iT, oU, iK, oY, iF, oU, iF, oV, iQ, oW])* --------------- Formula: (! (true U oU) | (! oU U ((iA & ! oU) & X (! oU U iM)))) "input A, input M always precedes output U" Formula is not satisfied! An error path is [iB, oU, iA, oZ] ([iQ, oZ, iT, oV, iF, oW, iD, oW, iQ, oY, iE, oW])* --------------- 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 [iF, oW, iD, oW, iK, oX] ([iJ, oU, iA, oV, iA, oX, iO, oW, iR, 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 satisfied. --------------- 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 [iF, oW, iD, oW, iF, oU, iH, oY, iT, oY, iE] ([oV, iD, oV, iA, oU, iH, oY, iT, oY, 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 [iQ, oV] ([iR, oW, iK, oZ, iT, oU, iK, oY, iF, oU, iF, oV, iQ, oW])* --------------- Formula: (! (true U oU) | (! oU U ((oV & ! oU) & X (! oU U iA)))) "output V, input A always precedes output U" Formula is not satisfied! An error path is [iB, oU, iA, oZ] ([iQ, oZ, iT, oV, iF, oW, iD, oW, iQ, oY, iE, oW])* --------------- 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 [iF, oW, iQ, oZ, iC, oZ, iL, oZ, iF] ([oY, iA, oV, iC, oY, iF, oZ, 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 not satisfied! An error path is [iQ, oV, iA, oU, iB, oX] ([iA, oU, iR, oY, iB, oV, iC, oV, iT, oU, iB, oX])* --------------- Formula: (false R (! iT | (true U oV))) "output V always responds to input T" Formula is not satisfied! An error path is [iF, oW, iA, oX, iD, oX, iE, oX, iT] ([oW, iB, oZ, iB, oU, iM, oX, iE, 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 [iQ, oV] ([iR, oW, iK, oZ, iT, oU, iK, oY, iF, oU, iF, oV, iQ, oW])* --------------- Formula: (! (true U oY) | (! oZ U (iM | oY))) "input M precedes output Z before output Y" Formula is not satisfied! An error path is [iB, oU, iA, oZ, iR, oY, iK, oV] ([iA, oX, iO, oW, iO, oV, iM, oY])* --------------- 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 [iQ, oV, iJ, oV] ([iK, oW, iO, oZ, iB, oX, iF, oY, iB, oX, iH, oY])* --------------- 20 constraints satisfied, 80 unsatisfied.