Reachability problems: =============================== error_5 reachable via input sequence [B, D, K, E, S, O, R, E] --------------- error_6 reachable via input sequence [B, D, K, E, P, C, A, Q] --------------- error_11 reachable via input sequence [B, D, K, E, S, O, H, M] --------------- error_13 reachable via input sequence [B, D, K, E, S, K, R, D] --------------- error_16 reachable via input sequence [B, D, K, E, S, C, L, F] --------------- error_18 reachable via input sequence [B, D, K, E, S, O, P, J] --------------- error_21 reachable via input sequence [B, D, K, E, S, S, E, J] --------------- error_24 reachable via input sequence [B, D, K, E, S, K, P, C] --------------- error_25 reachable via input sequence [B, D, K, E, S, O, A, B] --------------- error_31 reachable via input sequence [B, D, K, E, P, N, S, O] --------------- error_37 reachable via input sequence [B, D, K, E, P, N, D, D] --------------- error_39 reachable via input sequence [B, D, K, E, B, E, P, G] --------------- error_40 reachable via input sequence [B, D, K, E, S, S, K, G] --------------- error_51 reachable via input sequence [B, D, K, E, S, K, G, L] --------------- error_55 reachable via input sequence [B, D, K, E, P, N, M, M] --------------- error_56 reachable via input sequence [B, D, K, E, B, P, G, Q] --------------- error_63 reachable via input sequence [B, D, K, E, S, K, I, S] --------------- error_73 reachable via input sequence [B, D, K, E, S, S, H, D] --------------- error_74 reachable via input sequence [B, D, K, E, P, N, L, K] --------------- error_77 reachable via input sequence [B, D, K, E, P, C, L, Q] --------------- error_84 reachable via input sequence [B, D, K, E, B, E, A, C] --------------- error_90 reachable via input sequence [B, D, K, E, P, C, R, D] --------------- error_91 reachable via input sequence [B, D, K, E, P, C, E, F] --------------- 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 [iB, oW, iD, oY, iB, oU, iF, oX] ([iR, oW, iG, oW, iT, oV, iT, oW, iD, oY, iB, oU, iF, 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 not satisfied! An error path is [iB, oW, iK, oW, iO, oV, iB, oW, iI, oY, iN, oU, iF, oV, iB, oY, iP] ([oV, iN, oU, iT, oY, iR, oY, iI, oW, 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 [iT, oU, iR, oU, iA, oY, iO] ([oX, iS, oU, iA, oU, iH, oX, iH, oY, 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 not satisfied! An error path is [iT, oU, iR, oU, iD, oW, iP, oU, iN, oW] ([iI, oY, iM, oU, iD, oU, iD, oW, iP, oU, iN, oW])* --------------- 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 [iT, oU, iR, oU, iA, oY, iH, oY, iH, oV, iI, oV, iA, oU, iS, oU, iB] ([oW, iF, oY, iB, oW, iN, oY, iH, oX, iB, oX, iO, 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 [iT, oU, iR, oU, iD, oW, iA, oU, iC, oX, iB, oU] ([iS, oX, iE, oY, iS, oU, iR, oU, iD, oW, iA, oU, iC, oX, iB, 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 satisfied. --------------- 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 [iB, oW] ([iD, oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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, oW, iD, oY] ([iB, oU, iP, oU, iT, oV, iR, oV, iI, oW, iC, oU])* --------------- 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 [iB, oW, iT, oX, iS, oV, iK, oX, iK, oX, iM, oW, iG] ([oW, iT, oX, iK, oX, iM, oW, 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 [iT, oU, iR, oU, iD, oW, iP, oU, iK] ([oX, iD, oY, iA, oW, iJ, oU, iR, oU, iD, oW, iP, oU, 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 [iB, oW] ([iD, oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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 [iB, oW] ([iD, oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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 [iB, oW, iD, oY, iB, oU, iP] ([oU, iT, oV, iR, oV, iI, oW, iC, oU, iB, oU, 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 [iT, oU, iB, oW, iL, oY, iD, oU, iD, oV, iM, oW, iE, oY] ([iP, oY])* --------------- 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 satisfied. --------------- 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 [iB, oW, iT, oX, iS, oV, iK] ([oX, iK, oX, iR, oV, iL, oV, iA, 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 [iT, oU, iR, oU, iA] ([oY, iO, oX, iF, oW, iD, oV, iO, oU, iD, oU, 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 [iB, oW, iT, oX, iS, oV, iF, oX, iF, oX, iP] ([oV, iD, oV, iR, oX, iF, 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 [iB, oW] ([iD, oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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, oW, iD, oY] ([iB, oU, iP, oU, iT, oV, iR, oV, iI, oW, iC, oU])* --------------- 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 [iB, oW, iL, oV, iK, oU, iT] ([oU, iN, oU, iH, oW, iS, oY, iS, oV, iL, oV, iK, oU, 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 [iB, oW, iT, oX, iS, oV, iR, oY, iL, oU, iH, oW, iJ] ([oX, iG, oX, iF, oX, iN, oX, iK, oV, iB, oW, iR, oY, iA, oX, iS, oV, iR, oY, iL, oU, iH, oW, 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 [iT, oU, iB, oW, iK, oY, iH, oV, iR, oV] ([iH, oV, iS, oU, iA, oY, iH, oV, iR, oV])* --------------- 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 [iB, oW, iT, oX, iS, oV, iF, oX, iF, oX, iI] ([oV, iD, oW, iM, oX, 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 [iT, oU, iB, oW, iL, oY, iE, oW, iA, oX, iF, oY] ([iC, oW, iR, oX, iF, 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 not satisfied! An error path is [iT, oU, iR, oU, iA, oY, iO, oX, iN, oX, iD, oY, iK, oX, iF] ([oX, iN, oX, iD, oY, iK, oX, iF])* --------------- 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 satisfied. --------------- 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 [iB, oW] ([iD, oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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 [iB, oW, iT, oX] ([iS, oV, iK, oX, iK, oX, iM, oW, iG, oW, iG, 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 [iB, oW, iL, oV, iK, oU] ([iE, oX, iR, oW, iL, oU, iT, oY, iT, oY, iK, 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 [iB, oW] ([iD, oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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 [iT, oU, iR, oU, iL, oU, iP, oY, iA, oX, iC, oV, iT] ([oV, iD, oX, iC, oV, 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 [iB, oW] ([iD, oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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 [iB, oW, iT, oX] ([iS, oV, iF, oX, iF, oX, iE, oY, iA, oW, iR, 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 [iB, oW, iD] ([oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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 [iB, oW, iT, oX, iS, oV, iF, oX, iG, oY, iK] ([oW, iP, oY, iE, oY, 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 [iB, oW, iK, oW, iO, oV, iC, oU, iI, oW, iA, oX, iM] ([oX, iO, oY, iC, oU, iI, oW, iA, 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 [iB, oW] ([iD, oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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 [iB, oW, iK, oW, iO, oV] ([iB, oW, iS, oY, iK, oW, iF, oV, iR, oW])* --------------- 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 [iB, oW, iT, oX, iS, oV, iF, oX, iF, oX, iI] ([oV, iD, oW, iM, oX, 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 [iT, oU, iR, oU, iA] ([oY, iO, oX, iF, oW, iD, oV, iO, oU, iD, oU, 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 [iB, oW, iD] ([oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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 [iT, oU, iB, oW, iL, oY, iA, oY, iG, oU, iJ] ([oX, iA, oV, iA, oU, 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 [iB, oW, iL, oV, iK, oU, iN, oU, iC, oY, iO, oU, iH] ([oX, iS, oU, iC, oY, iO, oU, iH])* --------------- Formula: (! (true U iG) | ((! iD | (! iG U (oZ & ! iG))) U iG)) "output Z responds to input D before input G" Formula is not satisfied! An error path is [iT, oU, iR, oU, iD, oW, iP, oU, iG] ([oW, iF, oU, iD, oY, iI, oU, iH, oU, iR, oU, iD, oW, iP, oU, iG])* --------------- 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 not satisfied! An error path is [iB, oW, iT, oX, iS, oV, iN, oU, iA, oY, iJ] ([oV, iN, oV, iM, oY, iJ])* --------------- 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 [iB, oW, iT, oX, iS, oV, iF, oX, iG, oY, iG, oX, iR] ([oX, iM, oY, iG, oX, 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 [iB, oW, iD, oY, iH, oX, iR, oY, iJ] ([oU, iT, oU, iO, oW, iS, oY, iD, oY, iH, oX, iR, oY, iJ])* --------------- Formula: (! (true U iH) | ((! iQ | (! iH U (oV & ! iH))) U iH)) "output V responds to input Q before input H" Formula is satisfied. --------------- Formula: (! oX WU iM) "input M always precedes output X" Formula is not satisfied! An error path is [iB, oW, iT, oX] ([iS, oV, iF, oX, iF, oX, iE, oY, iA, oW, iR, 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 [iT, oU, iB, oW, iF, oY, iS, oU, iJ] ([oV, iN, oY, iK, oU, iF, oU, 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 [iB, oW, iK, oW, iO, oV, iC, oU, iP, oV, iE, oX, iB] ([oU, iS, oY, iP, oV, iE, 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 [iT, oU, iR, oU, iD, oW, iS, oX, iB] ([oW, iN, oY, iG, oY, iF, oU, iR, oU, iD, oW, iS, oX, 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 [iB, oW, iL, oV, iK] ([oU, iE, oX, iR, oW, iL, oU, iT, oY, iT, oY, iK])* --------------- Formula: (false R (! iP | (true U oV))) "output V always responds to input P" Formula is not satisfied! An error path is [iT, oU, iR, oU, iD, oW, iP] ([oU, iN, oW, iI, oY, iM, oU, iD, oU, iD, oW, 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 [iT, oU, iR, oU, iD, oW, iS, oX, iB] ([oW, iN, oY, iG, oY, iF, oU, iR, oU, iD, oW, iS, oX, 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 [iT, oU, iB, oW, iF] ([oY, iS, oU, iJ, oV, iN, oY, iS, oU, iG, 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 satisfied. --------------- 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 [iB, oW, iT, oX, iS, oV, iF, oX, iK, oY, iC] ([oX, iR, oV, iF, oV, iF, oX, iK, oY, 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 [iB, oW] ([iD, oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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 [iB, oW, iD, oY, iH, oX, iR] ([oY, iJ, oU, iT, oU, iO, oW, iS, oY, iD, oY, iH, 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 [iT, oU, iR, oU, iL, oU, iP, oY, iA, oX, iC, oV, iK] ([oV, iO, oV, 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 [iT, oU, iR, oU, iD, oW, iA, oU, iC] ([oX, iF, oX, iP, oY, iD, oU, iR, oU, iD, oW, iA, 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 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 [iT, oU, iR, oU, iA, oY, iO, oX, iM, oX, iS, oV, iG] ([oY, iJ, oU, iR, oU, iA, oY, iO, oX, iM, oX, iS, oV, iG])* --------------- Formula: (! (true U iE) | (! oU U (iT | iE))) "input T precedes output U before input E" Formula is not satisfied! An error path is [iB, oW, iL, oV, iK, oU, iE] ([oX, iR, oW, iL, oU, iT, oY, iT, oY, iK, 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 [iB, oW] ([iD, oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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 [iT, oU] ([iB, oW, iF, oY, iB, oW, iN, oY, iH, oX, iB, oX, iO, oU])* --------------- 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 [iB, oW, iL, oV, iK, oU, iE, oX] ([iC, oW, iE, oY, iN, oV, iE, oU])* --------------- 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 [iB, oW, iT, oX, iS, oV, iF, oX, iG] ([oY, iG, oX, iH, oU, iP, oX, 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 [iT, oU, iB, oW, iL, oY, iE] ([oW, iA, oX, iF, oY, iD, oU, iA, 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 [iB, oW] ([iD, oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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 [iT, oU] ([iB, oW, iF, oY, iB, oW, iN, oY, iH, oX, iB, oX, iO, oU])* --------------- 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 [iB, oW, iL, oV, iK, oU, iN, oU, iC, oY, iF] ([oV, iM, oU, iN, oU, iC, oY, 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 [iT, oU] ([iB, oW, iF, oY, iB, oW, iN, oY, iH, oX, iB, oX, iO, oU])* --------------- 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 [iB, oW] ([iD, oY, iB, oU, iF, oX, iR, oW, iG, oW, iT, oV, iT, 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 [iB, oW, iD, oY, iH, oX, iR, oY, iJ] ([oU, iT, oU, iO, oW, iS, oY, iD, oY, iH, oX, iR, oY, iJ])* --------------- 28 constraints satisfied, 72 unsatisfied.