Reachability problems: =============================== error_40 reachable via input sequence [H, C, H, I, J, K, O, E, I, L] --------------- error_41 reachable via input sequence [H, C, H, I, J, K, O, E, K, I] --------------- error_45 reachable via input sequence [H, C, H, I, J, K, I, K, B, I] --------------- error_59 reachable via input sequence [H, C, H, I, J, K, I, F, M, B] --------------- error_62 reachable via input sequence [H, C, H, I, J, K, I, F, K, F] --------------- error_66 reachable via input sequence [H, C, H, I, J, K, O, E, L, D] --------------- error_98 reachable via input sequence [H, C, H, I, J, K, I, F, I, H] --------------- 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ] ([oY, iG, oZ, iI, oV, iH, oS, iM, oZ, iE, oS, 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 satisfied. --------------- 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 [iH, oV, iC, oY] ([iH, oU, iI, oS, iJ, oY, iK, oS, iI, oW, iK, oV, iH, oZ, iO, oX])* --------------- 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 [iH, oV, iC, oY, iN, oS, iE, oS, iM] ([oR, iN, oR, iE, oR, iB, oR, iN, oW, iL, oY, 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 [iH, oV, iC, oY, iN, oS, iE, oS, iM, oR] ([iN, oR, iE, oR, iH, oY, iI, oU, iB, 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 satisfied. --------------- 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iM, oS, iA] ([oX, iC, oU, iH, oX, iI, oZ, iA])* --------------- Formula: (! oQ WU iO) "input O always precedes output Q" Formula is satisfied. --------------- Formula: (false R (oV & (! ! oR | (! oX WU (iF | oR))))) "input F precedes output X after output V until output R" Formula is not satisfied! An error path is [iH, oV, iC, oY] ([iH, oU, iI, oS, iJ, oY, iK, oS, iI, oW, iK, oV, iH, oZ, iO, oX])* --------------- 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 [iH, oV, iC, oY, iN, oS, iE, oS, iM] ([oR, iN, oR, iE, oR, iB, oR, iN, oW, iL, oY, iM])* --------------- Formula: (! (true U iC) | ((! iN | (! iC U (oZ & ! iC))) U iC)) "output Z responds to input N before input C" Formula is satisfied. --------------- 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 [iH, oV, iC, oY, iH, oU, iI, oS, iE, oV, iH, oY, iH, oY, iG, oX, iO, oW, iF] ([oV, iH, oU, iA, oY, iA, oY, iI, oY, iH, oU, iI, oS, iE, oV, iH, oY, iH, oY, iG, oX, iO, oW, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iE, oV, iH] ([oY, iJ, oP, iB, oU, iB, oR, iF, oP, iO, oY, iH, oU, iI, oS, iE, oV, iH])* --------------- Formula: (! oU WU iH) "input H always precedes output U" Formula is satisfied. --------------- 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iM, oS, iE, oW, iG, oW, iF, oU] ([iA, oW, iL, oS, iM, oP, iE, oP, iJ, oV, iG, oY, iH, oU, iI, oS, iJ, oY, iM, oS, iE, oW, iG, oW, iF, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iK, oS, iF] ([oP, iK, oW, iL, oX, iJ, oP, 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 [iH, oV, iC, oY, iN, oS, iE, oS, iM, oR, iN, oR, iE, oR, iG, oU] ([iA, oP, iC, oY, iM, oS, iM, oR, iN, oR, iE, oR, iG, oU])* --------------- Formula: (false R (! oT | (false R (! iK | ((oS & ! oP) & X (! oP U oQ)))))) "output S, output Q without output P responds to input K after output T" Formula is 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 not satisfied! An error path is [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iK] ([oS, iO, oX, iE, oW, iK, oV, iO, oR, iK])* --------------- Formula: (false R (! iG | ((! iO | (! iD U (((oU & ! iD) & ! oT) & X ((! iD & ! oT) U oP)))) U (iD | (false R (! iO | ((oU & ! oT) & X (! oT U oP)))))))) "output U, output P without output T responds to input O after input G until input D" Formula is not satisfied! An error path is [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iJ, oP, iG, oW, iO] ([oR, iL, oY, iC, oZ, iJ, oY, iH, oU, iI, oS, iJ, oY, iJ, oP, iG, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iM, oS, iF, oU] ([iC, oU, iH, oY, iI, oR, iM, oY, iH, oU, iI, oS, iJ, oY, iM, oS, iF, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iG, oZ, iG, oP, iI, oU, iC] ([oZ, iO, oS, iH, oY, iL, oY, iH, oU, iI, oS, iJ, oY, iG, oZ, iG, oP, iI, oU, 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 [iH, oV, iC, oY] ([iH, oU, iI, oS, iJ, oY, iK, oS, iI, oW, iK, oV, iH, oZ, iO, oX])* --------------- 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 [iH, oV, iC, oY, iN, oS, iE] ([oS, iM, oR, iN, oR, iA, oY, iI, oW, iH, oV, iG, oV, 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 [iH, oV, iC, oY, iN] ([oS, iE, oS, iE, oV, iC, oY, iA, oU, iO, oS, iF, oR, iJ, oY, 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 [iH, oV, iC, oY, iN, oS, iE, oS, iE, oV, iC, oY, iA, oU, iM] ([oU, iC, oS, iM, oZ, iF, oS, iE, oV, iC, oY, iA, oU, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iJ, oP, iI, oW, iE, oX, iA] ([oV, iG, oS, iE, oY, iH, oU, iI, oS, iJ, oY, iJ, oP, iI, oW, iE, oX, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iJ, oP] ([iG, oW, iA, oY, iK, oV, iC, oS, iL, oY, iH, oU, iI, oS, iJ, oY, iJ, oP])* --------------- Formula: (! (true U (oX & X (true U oT))) | (! oX U iK)) "input K always precedes output X, output T" Formula is satisfied. --------------- Formula: (false R (! (iI & (true U iK)) | ((iN & (! X (! iK U iJ) | X (! iK U (iJ & (true U oR))))) U iK))) "output R responds to input N, input J between input I and input K" Formula is not satisfied! An error path is [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iK] ([oS, iO, oX, iE, oW, iK, oV, iO, oR, iK])* --------------- Formula: ((false R ! oR) | (true U (oR & (! oS WU iI)))) "input I precedes output S after output R" Formula is not satisfied! An error path is [iH, oV, iC, oY, iN, oS, iE, oS, iE, oV, iM, oP, iL, oR, iC, oS] ([iN, oY, iH, oR, iC, 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 not satisfied! An error path is [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iK] ([oS, iI, oW, iF, oX, iI, oU, iG, oR, iJ, oY, iK])* --------------- 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 satisfied. --------------- 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 [iH, oV, iC, oY, iN, oS, iE, oS, iO, oP, iG] ([oY, iB, oU, iN, oP, iC, oZ, iK, oP, 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 [iH, oV, iC, oY, iN, oS, iE, oS, iM, oR] ([iN, oR, iE, oR, iH, oY, iI, oU, iB, 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 [iH, oV, iC, oY, iN, oS, iE] ([oS, iM, oR, iN, oR, iA, oY, iI, oW, iH, oV, iG, 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 [iH, oV, iC, oY] ([iH, oU, iI, oS, iJ, oY, iK, oS, iI, oW, iK, oV, iH, oZ, iO, oX])* --------------- 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 satisfied. --------------- 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 satisfied. --------------- 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iJ, oP, iJ, oP, iL] ([oZ, iE, oX, iB, oX, iO, oY, iH, oU, iI, oS, iJ, oY, iJ, oP, iJ, oP, iL])* --------------- Formula: (false R (! iG | (true U oU))) "output U always responds to input G" Formula is not satisfied! An error path is [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iG] ([oZ, iI, oV, iH, oS, iM, oZ, iE, oS, iJ, 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 [iH, oV, iC, oY, iN, oS, iE, oS, iM] ([oR, iN, oR, iE, oR, iB, oR, iN, oW, iL, 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 satisfied. --------------- 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 [iH, oV, iC, oY, iN, oS, iE, oS, iN, oU, iO, oR, iH, oU, iL] ([oR, iN, oS, iJ, oY, iO, oR, iH, oU, 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 [iH, oV, iC, oY] ([iH, oU, iI, oS, iJ, oY, iK, oS, iI, oW, iK, oV, iH, oZ, iO, oX])* --------------- 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 [iH, oV, iC, oY, iN, oS, iE, oS, iE, oV, iE, oW, iL] ([oZ, iN, oY, iE, oX, iO, oY, iN, oS, iE, oS, iE, oV, iE, oW, iL])* --------------- Formula: (false R (! iI | (true U oZ))) "output Z always responds to input I" Formula is not satisfied! An error path is [iH, oV, iC, oY, iH, oU, iI] ([oS, iJ, oY, iK, oS, iI, oW, iK, oV, iB, oV, iH, oW, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iK, oS, iF] ([oP, iK, oW, iL, oX, iJ, oP, iF])* --------------- Formula: (! oV WU iF) "input F always precedes output V" Formula is not satisfied! An error path is [iH, oV, iC, oY] ([iH, oU, iI, oS, iJ, oY, iK, oS, iI, oW, iK, oV, iH, oZ, iO, oX])* --------------- 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 satisfied. --------------- 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 [iH, oV, iC, oY, iN, oS, iE, oS, iO] ([oP, iC, oZ, iA, oP, iJ, oR, iF, oY, iE, oS, 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 [iH, oV, iC, oY, iN, oS, iE, oS, iE, oV, iE, oW] ([iA, oW, iN, oY, iK, oS, iF, oV, iE, 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 satisfied. --------------- Formula: (false R (! iK | (true U ((oR & ! oT) & X (! oT U oX))))) "output R, output X without output T always responds to input K" Formula is not satisfied! An error path is [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iK] ([oS, iI, oW, iK, oV, iB, oV, iH, oW, iI, oS, iJ, oY, iK])* --------------- Formula: (! (true U iD) | (! ((oS & ! iD) & X (! iD U (oT & ! iD))) U (iD | oQ))) "output Q precedes output S, output T before input D" Formula is satisfied. --------------- Formula: ((false R ! iJ) | (! iJ U (iJ & (! (true U oQ) | (! oQ U ((iA & ! oQ) & X (! oQ U iL))))))) "input A, input L precedes output Q after input J" Formula is satisfied. --------------- Formula: (! (true U iD) | ((! iE | (! iD U (((oP & ! iD) & ! oX) & X ((! iD & ! oX) U oW)))) U iD)) "output P, output W without output X responds to input E before input D" Formula is satisfied. --------------- Formula: (false R (! oP | (false R (iG & (! X (true U iH) | X (! iH U (iH & (true U oW)))))))) "output W responds to input G, input H after output P" Formula is not satisfied! An error path is [iH, oV, iC, oY, iN, oS, iE, oS, iO, oP] ([iC, oZ, iA, oP, iJ, oR, iF, oY, iA, oP])* --------------- 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 [iH, oV, iC, oY] ([iH, oU, iI, oS, iJ, oY, iK, oS, iI, oW, iK, oV, iH, oZ, iO, oX])* --------------- 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 not satisfied! An error path is [iH, oV, iC, oY, iH, oU, iI, oS, iE, oV, iH, oY, iJ, oP, iC, oR, iB, oR, iB, oY, iM, oS, iF] ([oV, iM, oS, iF])* --------------- 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 not satisfied! An error path is [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iK, oS, iN, oV, iL, oU, iB, oZ, iH, oS, iJ] ([oY, iB, oU, iN, oP, iC, oZ, iJ])* --------------- 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 [iH, oV, iC, oY, iN, oS, iE, oS, iE, oV, iE, oW] ([iA, oW, iN, oY, iK, oS, iF, oV, iE, 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 [iH, oV, iC, oY] ([iH, oU, iI, oS, iJ, oY, iK, oS, iI, oW, iK, oV, iH, oZ, iO, oX])* --------------- 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 satisfied. --------------- 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 satisfied. --------------- Formula: (! (true U iB) | ((! iO | (! iB U ((oP & ! iB) & X (! iB U oX)))) U iB)) "output P, output X responds to input O before input B" Formula is not satisfied! An error path is [iH, oV, iC, oY, iN, oS, iE, oS, iO, oP, iC, oZ, iB] ([oR, iN, oP, iK, oP, iG, oP, iC, oZ, iB])* --------------- Formula: (false R (! oZ | (false R (! iB | (true U oW))))) "output W responds to input B after output Z" Formula is not satisfied! An error path is [iH, oV, iC, oY, iN, oS, iE, oS, iO, oP, iC, oZ, iB] ([oR, iN, oP, iK, oP, iG, oP, iC, oZ, iB])* --------------- Formula: (false R (! (oW & (true U iF)) | ((iG & (! X (! iF U iN) | X (! iF U (iN & (true U oV))))) U iF))) "output V responds to input G, input N between output W and input F" Formula is not satisfied! An error path is [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iK, oS, iI, oW, iF] ([oX, iI, oU, iG, oR, iJ, oY, iK, oS, iI, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iG, oZ, iI, oV, iH, oS] ([iL, oV, iK, oR, iH, 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 not satisfied! An error path is [iH, oV, iC, oY, iN, oS, iE, oS, iE, oV, iM, oP, iH, oY, iB] ([oX, iA, oV, iA, oP, iH, oS, iE, oS, iE, oV, iM, oP, iH, oY, iB])* --------------- Formula: (false R (iO & (! X (true U iJ) | X (true U (iJ & (true U oZ)))))) "output Z always responds to input O, input J" Formula is not satisfied! An error path is [iH, oV, iC, oY] ([iH, oU, iI, oS, iJ, oY, iK, oS, iI, oW, iK, oV, iH, oZ, iO, oX])* --------------- 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iG, oZ, iI, oV, iH, oS, iL] ([oV, iK, oR, iH, oS, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iM, oS, iE, oW, iM, oP, iM, oU] ([iH, oZ, iH, oY, iH, oU, iI, oS, iJ, oY, iM, oS, iE, oW, iM, oP, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iK, oS, iO, oX] ([iE, oW, iK, oV, iO, oR, iK, oS, iO, 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 [iH, oV, iC, oY, iN, oS, iE, oS, iM, oR, iN, oR, iA, oY, iJ] ([oW, iG, oZ, iE, 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 satisfied. --------------- 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 [iH, oV, iC, oY, iN, oS, iE, oS, iM, oR] ([iN, oR, iE, oR, iH, oY, iI, oU, iB, 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 not satisfied! An error path is [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iK, oS, iO, oX, iE, oW, iK, oV, iF, oZ] ([iJ, oS, iB, oU, iL, oX])* --------------- 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 [iH, oV, iC, oY, iN, oS, iE, oS, iE, oV, iE, oW] ([iA, oW, iN, oY, iK, oS, iF, oV, iE, 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 [iH, oV, iC, oY, iN, oS, iE, oS, iO, oP, iC, oZ, iI] ([oU, iA, oY, iA, oY, iF, oZ, 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 [iH, oV, iC, oY, iN, oS, iE, oS, iE, oV, iC, oY, iA, oU, iN, oR] ([iH, oU, iK, oZ, iO, oS, iE, oV, iC, oY, iA, oU, iN, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iJ, oP, iJ, oP, iA, oZ, iF, oS, iO] ([oR, iL, oS, iE, oV, iC, oY, iA, oU, iO, oS, iF, oR, iJ, oY, iH, oU, iI, oS, iJ, oY, iJ, oP, iJ, oP, iA, oZ, iF, oS, iO])* --------------- Formula: (false R (iK & (! ! iF | (! oZ WU (iI | iF))))) "input I precedes output Z after input K until input F" Formula is not satisfied! An error path is [iH, oV, iC, oY] ([iH, oU, iI, oS, iJ, oY, iK, oS, iI, oW, iK, oV, iH, oZ, iO, oX])* --------------- Formula: (false R (! (iL & (true U oZ)) | ((! iB | (! oZ U (((oW & ! oZ) & ! oT) & X ((! oZ & ! oT) U oY)))) U oZ))) "output W, output Y without output T responds to input B betwen input L and output Z" Formula is not satisfied! An error path is [iH, oV, iC, oY, iN, oS, iE, oS, iE, oV, iM, oP, iL, oR, iB, oZ] ([iB, oP, iO, oY, iM, oS, iE, oV, iM, oP, iL, oR, iB, oZ])* --------------- Formula: (! (true U iE) | ((! iC | (! iE U ((oZ & ! iE) & X (! iE U oT)))) U iE)) "output Z, output T responds to input C before input E" Formula is not satisfied! An error path is [iH, oV, iC, oY, iN, oS, iE] ([oS, iM, oR, iN, oR, iA, oY, iI, oW, iH, oV, iG, oV, 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 [iH, oV, iC, oY, iN, oS, iE, oS, iM, oR, iN, oR, iA, oY, iJ, oW, iG, oZ, iN, oR, iA, oU] ([iA, oY, iF, oP, iN, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iK, oS, iI, oW, iF] ([oX, iI, oU, iG, oR, iJ, oY, iK, oS, iI, oW, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iM, oS, iE, oW, iI, oR] ([iK, oR, iN, oY, iE, oZ, iG, oP, iI, oP, iL, oY, iH, oU, iI, oS, iJ, oY, iM, oS, iE, oW, iI, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iJ, oP, iG, oW] ([iA, oY, iK, oV, iC, oS, iL, oY, iH, oU, iI, oS, iJ, oY, iJ, oP, iG, 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 satisfied. --------------- Formula: (false R (! iB | (true U ((oV & ! oS) & X (! oS U oX))))) "output V, output X without output S always responds to input B" Formula is not satisfied! An error path is [iH, oV, iC, oY, iN, oS, iE, oS, iO, oP, iC, oZ, iB] ([oR, iN, oP, iK, oP, iG, oP, iC, oZ, iB])* --------------- Formula: (false R (! iE | ((! iN | (! iO U ((oX & ! iO) & X (! iO U oT)))) U (iO | (false R (! iN | (oX & X (true U oT)))))))) "output X, output T responds to input N after input E until input O" Formula is not satisfied! An error path is [iH, oV, iC, oY, iN, oS, iE, oS, iN] ([oU, iO, oR, iH, oU, iF, oW, iB, oY, iH, oV, iE, oS, 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 [iH, oV, iC, oY, iH, oU, iI, oS, iJ, oY, iG] ([oZ, iI, oV, iH, oS, iM, oZ, iE, oS, iJ, 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. --------------- 27 constraints satisfied, 73 unsatisfied.