log6 35.7 KB
Newer Older
Christian Müller's avatar
aalta  
Christian Müller committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
please input the formula:
f is:
(!StoB_REQ1 & (!BtoR_REQ0 & (!RtoB_ACK0 & ((false R (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0)))) & (!BtoR_REQ1 & (!RtoB_ACK1 & ((false R (true U ((BtoR_REQ1 & RtoB_ACK1) | (!BtoR_REQ1 & !RtoB_ACK1)))) & (!StoB_REQ0 & ((false R (StoB_REQ0 | (BtoS_ACK0 | X!BtoS_ACK0))) & ((false R (!StoB_REQ0 | (!BtoS_ACK0 | XBtoS_ACK0))) & ((false R (StoB_REQ1 | (X!StoB_REQ1 | X!BtoS_ACK1))) & ((false R (StoB_REQ1 | (BtoS_ACK1 | X!BtoS_ACK1))) & ((false R (!StoB_REQ1 | (!BtoS_ACK1 | XBtoS_ACK1))) & ((false R (RtoB_ACK0 | (!BtoR_REQ0 | XBtoR_REQ0))) & ((false R (RtoB_ACK1 | (!BtoR_REQ1 | XBtoR_REQ1))) & (!FULL & (EMPTY & (!BtoS_ACK0 & ((false R (!BtoS_ACK0 | X!StoB_REQ0)) & (!BtoS_ACK1 & ((false R (!BtoS_ACK1 | X!StoB_REQ1)) & ((false R (BtoR_REQ0 | X!RtoB_ACK0)) & ((false R (BtoR_REQ1 | X!RtoB_ACK1)) & (!ENQ & (!DEQ & (!SLC0 & ((false R (!BtoS_ACK0 | !BtoS_ACK1)) & ((false R (!BtoR_REQ0 | !BtoR_REQ1)) & ((false R (!RtoB_ACK0 | X!BtoR_REQ0)) & ((false R (!RtoB_ACK1 | X!BtoR_REQ1)) & (stateG7_1 & (!stateG7_0 & ((false R (!EMPTY | !DEQ)) & (!stateG12 & ((false R (true U ((StoB_REQ0 & BtoS_ACK0) | (!StoB_REQ0 & !BtoS_ACK0)))) & ((false R (true U ((StoB_REQ1 & BtoS_ACK1) | (!StoB_REQ1 & !BtoS_ACK1)))) & ((false R (true U !stateG12)) & ((false R (((!ENQ | !DEQ) & (ENQ | DEQ)) | (((FULL & XFULL) | (!FULL & X!FULL)) & ((!EMPTY & X!EMPTY) | (EMPTY & XEMPTY))))) & ((false R (ENQ | (!DEQ | X!FULL))) & ((false R (!ENQ | (DEQ | X!EMPTY))) & ((false R (!BtoR_REQ1 | (!RtoB_ACK1 | XRtoB_ACK1))) & ((false R (!BtoR_REQ0 | (!RtoB_ACK0 | XRtoB_ACK0))) & ((false R (!StoB_REQ1 | (BtoS_ACK1 | XStoB_REQ1))) & ((false R (!StoB_REQ0 | (BtoS_ACK0 | XStoB_REQ0))) & ((false R (StoB_REQ0 | (X!StoB_REQ0 | X!BtoS_ACK0))) & ((false R (!DEQ | (!stateG12 | X!stateG12))) & ((false R (DEQ | (!stateG12 | XstateG12))) & ((false R (EMPTY | (DEQ | (stateG12 | XstateG12)))) & ((false R (!DEQ | (stateG12 | X!stateG12))) & ((false R (!EMPTY | (stateG12 | X!stateG12))) & ((false R (!FULL | (!ENQ | DEQ))) & ((false R ((RtoB_ACK0 & X!RtoB_ACK0) | ((RtoB_ACK1 & X!RtoB_ACK1) | X!DEQ))) & ((false R (!RtoB_ACK1 | (XRtoB_ACK1 | XDEQ))) & ((false R (!RtoB_ACK0 | (XRtoB_ACK0 | XDEQ))) & ((false R ((!BtoS_ACK1 & XBtoS_ACK1) | ((!BtoS_ACK0 & XBtoS_ACK0) | X!ENQ))) & ((false R ((!BtoS_ACK1 & (XBtoS_ACK1 & XSLC0)) | (X!SLC0 & (BtoS_ACK1 | X!BtoS_ACK1)))) & ((false R (BtoS_ACK1 | (XENQ | X!BtoS_ACK1))) & ((false R (BtoS_ACK0 | (X!BtoS_ACK0 | X!SLC0))) & ((false R (BtoS_ACK0 | (X!BtoS_ACK0 | XENQ))) & ((false R (!BtoR_REQ1 | (!stateG7_0 | !stateG7_1))) & ((false R (!BtoR_REQ0 | (stateG7_1 | !stateG7_0))) & ((false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_0 | (X(stateG7_1 & !stateG7_0) | !stateG7_1))))) & ((false R (!BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | (stateG7_0 | X(!stateG7_0 & !stateG7_1)))))) & ((false R (BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(stateG7_1 & stateG7_0))))) & ((false R (BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | X(stateG7_0 & !stateG7_1))))) & ((false R (!BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(!stateG7_0 & !stateG7_1))))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_1 | X(stateG7_1 & !stateG7_0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

cf is:
(!StoB_REQ1 & (!BtoR_REQ0 & (!RtoB_ACK0 & (!BtoR_REQ1 & (!RtoB_ACK1 & (!StoB_REQ0 & (!FULL & (EMPTY & (!BtoS_ACK0 & (!BtoS_ACK1 & (!ENQ & (!DEQ & (!SLC0 & ((!BtoS_ACK0 | !BtoS_ACK1) & ((!BtoR_REQ0 | !BtoR_REQ1) & (stateG7_1 & (!stateG7_0 & ((!EMPTY | !DEQ) & (!stateG12 & ((((!ENQ | !DEQ) & (ENQ | DEQ)) | ((FULL | !FULL) & (!EMPTY | EMPTY))) & ((!FULL | (!ENQ | DEQ)) & ((!BtoR_REQ1 | (!stateG7_0 | !stateG7_1)) & (!BtoR_REQ0 | (stateG7_1 | !stateG7_0))))))))))))))))))))))))

1, -2, 3, -4, 5, -6, 7, -8, 9, -10, 11, -12, 13, -14, 15, 16, 17, -18, 19, -20, 21, -22, 23, -24, 25, -26, 27, 28, 29, 30, 31, 32, 33, -34, 35, 36, 37, -38, 39, 40, 41, -42, 43, -44, -45, 46, 47, 48, 49, -50, 51, 52, -53, -54, 
{!stateG7_0,!StoB_REQ0,!BtoS_ACK0,!stateG12,!FULL,!BtoS_ACK1,!StoB_REQ1,!SLC0,!RtoB_ACK0,!RtoB_ACK1,!DEQ,!BtoR_REQ0,!BtoR_REQ1,EMPTY,!ENQ,stateG7_1,}
pf is:
(((FOR_UNTIL_1379310663376409 | (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0)))) & (false R (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0))))) & (((FOR_UNTIL_1379310663423513 | (true U ((BtoR_REQ1 & RtoB_ACK1) | (!BtoR_REQ1 & !RtoB_ACK1)))) & (false R (true U ((BtoR_REQ1 & RtoB_ACK1) | (!BtoR_REQ1 & !RtoB_ACK1))))) & ((!BtoS_ACK0 & (false R (StoB_REQ0 | (BtoS_ACK0 | X!BtoS_ACK0)))) & ((false R (!StoB_REQ0 | (!BtoS_ACK0 | XBtoS_ACK0))) & (((!StoB_REQ1 | !BtoS_ACK1) & (false R (StoB_REQ1 | (X!StoB_REQ1 | X!BtoS_ACK1)))) & ((!BtoS_ACK1 & (false R (StoB_REQ1 | (BtoS_ACK1 | X!BtoS_ACK1)))) & ((false R (!StoB_REQ1 | (!BtoS_ACK1 | XBtoS_ACK1))) & ((false R (RtoB_ACK0 | (!BtoR_REQ0 | XBtoR_REQ0))) & ((false R (RtoB_ACK1 | (!BtoR_REQ1 | XBtoR_REQ1))) & ((false R (!BtoS_ACK0 | X!StoB_REQ0)) & ((false R (!BtoS_ACK1 | X!StoB_REQ1)) & ((!RtoB_ACK0 & (false R (BtoR_REQ0 | X!RtoB_ACK0))) & ((!RtoB_ACK1 & (false R (BtoR_REQ1 | X!RtoB_ACK1))) & ((false R (!BtoS_ACK0 | !BtoS_ACK1)) & ((false R (!BtoR_REQ0 | !BtoR_REQ1)) & ((false R (!RtoB_ACK0 | X!BtoR_REQ0)) & ((false R (!RtoB_ACK1 | X!BtoR_REQ1)) & ((false R (!EMPTY | !DEQ)) & (((FOR_UNTIL_1379310674209817 | (true U ((StoB_REQ0 & BtoS_ACK0) | (!StoB_REQ0 & !BtoS_ACK0)))) & (false R (true U ((StoB_REQ0 & BtoS_ACK0) | (!StoB_REQ0 & !BtoS_ACK0))))) & (((FOR_UNTIL_1379310674229273 | (true U ((StoB_REQ1 & BtoS_ACK1) | (!StoB_REQ1 & !BtoS_ACK1)))) & (false R (true U ((StoB_REQ1 & BtoS_ACK1) | (!StoB_REQ1 & !BtoS_ACK1))))) & (((FOR_UNTIL_1379310674344473 | (true U !stateG12)) & (false R (true U !stateG12))) & (((!FULL & EMPTY) & (false R (((!ENQ | !DEQ) & (ENQ | DEQ)) | (((FULL & XFULL) | (!FULL & X!FULL)) & ((!EMPTY & X!EMPTY) | (EMPTY & XEMPTY)))))) & ((false R (ENQ | (!DEQ | X!FULL))) & ((false R (!ENQ | (DEQ | X!EMPTY))) & ((false R (!BtoR_REQ1 | (!RtoB_ACK1 | XRtoB_ACK1))) & ((false R (!BtoR_REQ0 | (!RtoB_ACK0 | XRtoB_ACK0))) & ((false R (!StoB_REQ1 | (BtoS_ACK1 | XStoB_REQ1))) & ((false R (!StoB_REQ0 | (BtoS_ACK0 | XStoB_REQ0))) & (((!StoB_REQ0 | !BtoS_ACK0) & (false R (StoB_REQ0 | (X!StoB_REQ0 | X!BtoS_ACK0)))) & ((false R (!DEQ | (!stateG12 | X!stateG12))) & ((false R (DEQ | (!stateG12 | XstateG12))) & ((false R (EMPTY | (DEQ | (stateG12 | XstateG12)))) & ((false R (!DEQ | (stateG12 | X!stateG12))) & ((!stateG12 & (false R (!EMPTY | (stateG12 | X!stateG12)))) & ((false R (!FULL | (!ENQ | DEQ))) & ((!DEQ & (false R ((RtoB_ACK0 & X!RtoB_ACK0) | ((RtoB_ACK1 & X!RtoB_ACK1) | X!DEQ)))) & ((false R (!RtoB_ACK1 | (XRtoB_ACK1 | XDEQ))) & ((false R (!RtoB_ACK0 | (XRtoB_ACK0 | XDEQ))) & (((BtoS_ACK1 | (BtoS_ACK0 | !ENQ)) & (false R ((!BtoS_ACK1 & XBtoS_ACK1) | ((!BtoS_ACK0 & XBtoS_ACK0) | X!ENQ)))) & ((((BtoS_ACK1 & SLC0) | (!SLC0 & !BtoS_ACK1)) & (false R ((!BtoS_ACK1 & (XBtoS_ACK1 & XSLC0)) | (X!SLC0 & (BtoS_ACK1 | X!BtoS_ACK1))))) & (((ENQ | !BtoS_ACK1) & (false R (BtoS_ACK1 | (XENQ | X!BtoS_ACK1)))) & (((!BtoS_ACK0 | !SLC0) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | X!SLC0)))) & (((!BtoS_ACK0 | ENQ) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | XENQ)))) & ((false R (!BtoR_REQ1 | (!stateG7_0 | !stateG7_1))) & ((false R (!BtoR_REQ0 | (stateG7_1 | !stateG7_0))) & ((false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_0 | (X(stateG7_1 & !stateG7_0) | !stateG7_1))))) & ((false R (!BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | (stateG7_0 | X(!stateG7_0 & !stateG7_1)))))) & (((stateG7_1 & stateG7_0) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(stateG7_1 & stateG7_0)))))) & ((false R (BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | X(stateG7_0 & !stateG7_1))))) & ((false R (!BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(!stateG7_0 & !stateG7_1))))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_1 | X(stateG7_1 & !stateG7_0)))))))))))))))))))))))))))))))))))))))))))))))))))))))

1, 2, 3, 4, 5, -6, 7, 8, 9, 10, 11, 12, -13, 14, 15, -16, 17, 18, 19, 20, 21, 22, 23, -24, -25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, -41, 42, 43, 44, -45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, -62, 63, 64, 65, 66, 67, -68, 69, 70, 71, 72, 73, -74, 75, 76, 77, 78, -79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, -97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, -108, 109, 110, 111, 112, 113, -114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, -125, 126, 127, 128, 129, -130, 131, -132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 
nx is:
((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((false R (ENQ | (!DEQ | X!FULL))) & !StoB_REQ0) & (false R (!BtoR_REQ0 | !BtoR_REQ1))) & (false R (!RtoB_ACK1 | X!BtoR_REQ1))) & !BtoS_ACK0) & !SLC0) & (false R ((!BtoS_ACK1 & XBtoS_ACK1) | ((!BtoS_ACK0 & XBtoS_ACK0) | X!ENQ)))) & !RtoB_ACK1) & stateG7_0) & (false R (StoB_REQ1 | (BtoS_ACK1 | X!BtoS_ACK1)))) & (false R (!BtoR_REQ1 | (!RtoB_ACK1 | XRtoB_ACK1)))) & (false R (!BtoR_REQ1 | (!stateG7_0 | !stateG7_1)))) & (false R (DEQ | (!stateG12 | XstateG12)))) & FOR_UNTIL_1379310674344473) & (false R (!RtoB_ACK1 | (XRtoB_ACK1 | XDEQ)))) & (false R (StoB_REQ0 | (BtoS_ACK0 | X!BtoS_ACK0)))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_1 | X(stateG7_1 & !stateG7_0)))))) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | X!SLC0)))) & !stateG12) & (false R (StoB_REQ0 | (X!StoB_REQ0 | X!BtoS_ACK0)))) & (false R (!FULL | (!ENQ | DEQ)))) & !FULL) & (false R ((!BtoS_ACK1 & (XBtoS_ACK1 & XSLC0)) | (X!SLC0 & (BtoS_ACK1 | X!BtoS_ACK1))))) & (false R (!EMPTY | !DEQ))) & (false R (!StoB_REQ1 | (BtoS_ACK1 | XStoB_REQ1)))) & !StoB_REQ1) & (false R (true U !stateG12))) & (false R (BtoR_REQ0 | X!RtoB_ACK0))) & stateG7_1) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | (stateG7_0 | X(!stateG7_0 & !stateG7_1))))))) & (false R (StoB_REQ1 | (X!StoB_REQ1 | X!BtoS_ACK1)))) & FOR_UNTIL_1379310674229273) & (false R (!StoB_REQ1 | (!BtoS_ACK1 | XBtoS_ACK1)))) & (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0)))) & (false R (!StoB_REQ0 | (!BtoS_ACK0 | XBtoS_ACK0)))) & (false R (EMPTY | (DEQ | (stateG12 | XstateG12))))) & (false R (!ENQ | (DEQ | X!EMPTY)))) & (false R (((!ENQ | !DEQ) & (ENQ | DEQ)) | (((FULL & XFULL) | (!FULL & X!FULL)) & ((!EMPTY & X!EMPTY) | (EMPTY & XEMPTY)))))) & (false R (RtoB_ACK1 | (!BtoR_REQ1 | XBtoR_REQ1)))) & (false R (!BtoS_ACK0 | X!StoB_REQ0))) & (false R (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0))))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_0 | (X(stateG7_1 & !stateG7_0) | !stateG7_1)))))) & (false R (!EMPTY | (stateG12 | X!stateG12)))) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | X(stateG7_0 & !stateG7_1)))))) & (false R (!BtoS_ACK0 | !BtoS_ACK1))) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(stateG7_1 & stateG7_0)))))) & (false R (!RtoB_ACK0 | (XRtoB_ACK0 | XDEQ)))) & (false R (!RtoB_ACK0 | X!BtoR_REQ0))) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | XENQ)))) & (false R (!DEQ | (!stateG12 | X!stateG12)))) & (false R (!BtoS_ACK1 | X!StoB_REQ1))) & (false R (BtoR_REQ1 | X!RtoB_ACK1))) & (false R ((RtoB_ACK0 & X!RtoB_ACK0) | ((RtoB_ACK1 & X!RtoB_ACK1) | X!DEQ)))) & (false R (BtoS_ACK1 | (XENQ | X!BtoS_ACK1)))) & (false R (!StoB_REQ0 | (BtoS_ACK0 | XStoB_REQ0)))) & FOR_UNTIL_1379310663423513) & (false R (true U ((BtoR_REQ1 & RtoB_ACK1) | (!BtoR_REQ1 & !RtoB_ACK1))))) & (false R (RtoB_ACK0 | (!BtoR_REQ0 | XBtoR_REQ0)))) & !ENQ) & (false R (!BtoR_REQ0 | (!RtoB_ACK0 | XRtoB_ACK0)))) & (false R (!BtoR_REQ0 | (stateG7_1 | !stateG7_0)))) & (false R (true U ((StoB_REQ1 & BtoS_ACK1) | (!StoB_REQ1 & !BtoS_ACK1))))) & FOR_UNTIL_1379310674209817) & EMPTY) & !BtoS_ACK1) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(!stateG7_0 & !stateG7_1)))))) & (false R (true U ((StoB_REQ0 & BtoS_ACK0) | (!StoB_REQ0 & !BtoS_ACK0))))) & (false R (!DEQ | (stateG12 | X!stateG12)))) & !RtoB_ACK0) & !DEQ)

f is:
((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((false R (ENQ | (!DEQ | X!FULL))) & !StoB_REQ0) & (false R (!BtoR_REQ0 | !BtoR_REQ1))) & (false R (!RtoB_ACK1 | X!BtoR_REQ1))) & !BtoS_ACK0) & !SLC0) & (false R ((!BtoS_ACK1 & XBtoS_ACK1) | ((!BtoS_ACK0 & XBtoS_ACK0) | X!ENQ)))) & !RtoB_ACK1) & stateG7_0) & (false R (StoB_REQ1 | (BtoS_ACK1 | X!BtoS_ACK1)))) & (false R (!BtoR_REQ1 | (!RtoB_ACK1 | XRtoB_ACK1)))) & (false R (!BtoR_REQ1 | (!stateG7_0 | !stateG7_1)))) & (false R (DEQ | (!stateG12 | XstateG12)))) & FOR_UNTIL_1379310674344473) & (false R (!RtoB_ACK1 | (XRtoB_ACK1 | XDEQ)))) & (false R (StoB_REQ0 | (BtoS_ACK0 | X!BtoS_ACK0)))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_1 | X(stateG7_1 & !stateG7_0)))))) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | X!SLC0)))) & !stateG12) & (false R (StoB_REQ0 | (X!StoB_REQ0 | X!BtoS_ACK0)))) & (false R (!FULL | (!ENQ | DEQ)))) & !FULL) & (false R ((!BtoS_ACK1 & (XBtoS_ACK1 & XSLC0)) | (X!SLC0 & (BtoS_ACK1 | X!BtoS_ACK1))))) & (false R (!EMPTY | !DEQ))) & (false R (!StoB_REQ1 | (BtoS_ACK1 | XStoB_REQ1)))) & !StoB_REQ1) & (false R (true U !stateG12))) & (false R (BtoR_REQ0 | X!RtoB_ACK0))) & stateG7_1) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | (stateG7_0 | X(!stateG7_0 & !stateG7_1))))))) & (false R (StoB_REQ1 | (X!StoB_REQ1 | X!BtoS_ACK1)))) & FOR_UNTIL_1379310674229273) & (false R (!StoB_REQ1 | (!BtoS_ACK1 | XBtoS_ACK1)))) & (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0)))) & (false R (!StoB_REQ0 | (!BtoS_ACK0 | XBtoS_ACK0)))) & (false R (EMPTY | (DEQ | (stateG12 | XstateG12))))) & (false R (!ENQ | (DEQ | X!EMPTY)))) & (false R (((!ENQ | !DEQ) & (ENQ | DEQ)) | (((FULL & XFULL) | (!FULL & X!FULL)) & ((!EMPTY & X!EMPTY) | (EMPTY & XEMPTY)))))) & (false R (RtoB_ACK1 | (!BtoR_REQ1 | XBtoR_REQ1)))) & (false R (!BtoS_ACK0 | X!StoB_REQ0))) & (false R (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0))))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_0 | (X(stateG7_1 & !stateG7_0) | !stateG7_1)))))) & (false R (!EMPTY | (stateG12 | X!stateG12)))) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | X(stateG7_0 & !stateG7_1)))))) & (false R (!BtoS_ACK0 | !BtoS_ACK1))) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(stateG7_1 & stateG7_0)))))) & (false R (!RtoB_ACK0 | (XRtoB_ACK0 | XDEQ)))) & (false R (!RtoB_ACK0 | X!BtoR_REQ0))) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | XENQ)))) & (false R (!DEQ | (!stateG12 | X!stateG12)))) & (false R (!BtoS_ACK1 | X!StoB_REQ1))) & (false R (BtoR_REQ1 | X!RtoB_ACK1))) & (false R ((RtoB_ACK0 & X!RtoB_ACK0) | ((RtoB_ACK1 & X!RtoB_ACK1) | X!DEQ)))) & (false R (BtoS_ACK1 | (XENQ | X!BtoS_ACK1)))) & (false R (!StoB_REQ0 | (BtoS_ACK0 | XStoB_REQ0)))) & FOR_UNTIL_1379310663423513) & (false R (true U ((BtoR_REQ1 & RtoB_ACK1) | (!BtoR_REQ1 & !RtoB_ACK1))))) & (false R (RtoB_ACK0 | (!BtoR_REQ0 | XBtoR_REQ0)))) & !ENQ) & (false R (!BtoR_REQ0 | (!RtoB_ACK0 | XRtoB_ACK0)))) & (false R (!BtoR_REQ0 | (stateG7_1 | !stateG7_0)))) & (false R (true U ((StoB_REQ1 & BtoS_ACK1) | (!StoB_REQ1 & !BtoS_ACK1))))) & FOR_UNTIL_1379310674209817) & EMPTY) & !BtoS_ACK1) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(!stateG7_0 & !stateG7_1)))))) & (false R (true U ((StoB_REQ0 & BtoS_ACK0) | (!StoB_REQ0 & !BtoS_ACK0))))) & (false R (!DEQ | (stateG12 | X!stateG12)))) & !RtoB_ACK0) & !DEQ)

cf is:
((((((((((((((((((((((((!StoB_REQ0 & (!BtoR_REQ0 | !BtoR_REQ1)) & !BtoS_ACK0) & !SLC0) & !RtoB_ACK1) & stateG7_0) & (!BtoR_REQ1 | (!stateG7_0 | !stateG7_1))) & FOR_UNTIL_1379310674344473) & !stateG12) & (!FULL | (!ENQ | DEQ))) & !FULL) & (!EMPTY | !DEQ)) & !StoB_REQ1) & stateG7_1) & FOR_UNTIL_1379310674229273) & (((!ENQ | !DEQ) & (ENQ | DEQ)) | ((FULL | !FULL) & (!EMPTY | EMPTY)))) & (!BtoS_ACK0 | !BtoS_ACK1)) & FOR_UNTIL_1379310663423513) & !ENQ) & (!BtoR_REQ0 | (stateG7_1 | !stateG7_0))) & FOR_UNTIL_1379310674209817) & EMPTY) & !BtoS_ACK1) & !RtoB_ACK0) & !DEQ)

1, 2, -3, 4, -5, 6, -7, 8, 9, 10, 11, 12, 13, 14, -15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, -27, 28, 29, 30, -31, 32, 33, 34, -35, 36, 37, 38, 39, 40, 41, 42, -43, 44, -45, 46, -47, -48, 49, -50, -51, -52, -53, -54, 55, -56, -57, 58, 59, -60, 
{!StoB_REQ0,!BtoS_ACK0,stateG7_0,!stateG12,FOR_UNTIL_1379310674209817,FOR_UNTIL_1379310663423513,!FULL,!BtoS_ACK1,!StoB_REQ1,!SLC0,!RtoB_ACK1,!RtoB_ACK0,!BtoR_REQ1,!BtoR_REQ0,!DEQ,EMPTY,FOR_UNTIL_1379310674344473,FOR_UNTIL_1379310674229273,!ENQ,stateG7_1,}
pf is:
((((((((((((((((((((((((((((((((((((((((((((((((((((false R (ENQ | (!DEQ | X!FULL))) & (false R (!BtoR_REQ0 | !BtoR_REQ1))) & (false R (!RtoB_ACK1 | X!BtoR_REQ1))) & ((BtoS_ACK1 | (BtoS_ACK0 | !ENQ)) & (false R ((!BtoS_ACK1 & XBtoS_ACK1) | ((!BtoS_ACK0 & XBtoS_ACK0) | X!ENQ))))) & (!BtoS_ACK1 & (false R (StoB_REQ1 | (BtoS_ACK1 | X!BtoS_ACK1))))) & (false R (!BtoR_REQ1 | (!RtoB_ACK1 | XRtoB_ACK1)))) & (false R (!BtoR_REQ1 | (!stateG7_0 | !stateG7_1)))) & (false R (DEQ | (!stateG12 | XstateG12)))) & (false R (!RtoB_ACK1 | (XRtoB_ACK1 | XDEQ)))) & (!BtoS_ACK0 & (false R (StoB_REQ0 | (BtoS_ACK0 | X!BtoS_ACK0))))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_1 | X(stateG7_1 & !stateG7_0)))))) & ((!BtoS_ACK0 | !SLC0) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | X!SLC0))))) & ((!StoB_REQ0 | !BtoS_ACK0) & (false R (StoB_REQ0 | (X!StoB_REQ0 | X!BtoS_ACK0))))) & (false R (!FULL | (!ENQ | DEQ)))) & (((BtoS_ACK1 & SLC0) | (!SLC0 & !BtoS_ACK1)) & (false R ((!BtoS_ACK1 & (XBtoS_ACK1 & XSLC0)) | (X!SLC0 & (BtoS_ACK1 | X!BtoS_ACK1)))))) & (false R (!EMPTY | !DEQ))) & (false R (!StoB_REQ1 | (BtoS_ACK1 | XStoB_REQ1)))) & ((FOR_UNTIL_1379310674344473 | (true U !stateG12)) & (false R (true U !stateG12)))) & (!RtoB_ACK0 & (false R (BtoR_REQ0 | X!RtoB_ACK0)))) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | (stateG7_0 | X(!stateG7_0 & !stateG7_1))))))) & ((!StoB_REQ1 | !BtoS_ACK1) & (false R (StoB_REQ1 | (X!StoB_REQ1 | X!BtoS_ACK1))))) & (false R (!StoB_REQ1 | (!BtoS_ACK1 | XBtoS_ACK1)))) & (FOR_UNTIL_1379310663376409 | (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0))))) & (false R (!StoB_REQ0 | (!BtoS_ACK0 | XBtoS_ACK0)))) & (false R (EMPTY | (DEQ | (stateG12 | XstateG12))))) & (false R (!ENQ | (DEQ | X!EMPTY)))) & ((!FULL & EMPTY) & (false R (((!ENQ | !DEQ) & (ENQ | DEQ)) | (((FULL & XFULL) | (!FULL & X!FULL)) & ((!EMPTY & X!EMPTY) | (EMPTY & XEMPTY))))))) & (false R (RtoB_ACK1 | (!BtoR_REQ1 | XBtoR_REQ1)))) & (false R (!BtoS_ACK0 | X!StoB_REQ0))) & ((FOR_UNTIL_1379310663376409 | (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0)))) & (false R (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0)))))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_0 | (X(stateG7_1 & !stateG7_0) | !stateG7_1)))))) & (!stateG12 & (false R (!EMPTY | (stateG12 | X!stateG12))))) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | X(stateG7_0 & !stateG7_1)))))) & (false R (!BtoS_ACK0 | !BtoS_ACK1))) & ((stateG7_1 & stateG7_0) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(stateG7_1 & stateG7_0))))))) & (false R (!RtoB_ACK0 | (XRtoB_ACK0 | XDEQ)))) & (false R (!RtoB_ACK0 | X!BtoR_REQ0))) & ((!BtoS_ACK0 | ENQ) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | XENQ))))) & (false R (!DEQ | (!stateG12 | X!stateG12)))) & (false R (!BtoS_ACK1 | X!StoB_REQ1))) & (!RtoB_ACK1 & (false R (BtoR_REQ1 | X!RtoB_ACK1)))) & (!DEQ & (false R ((RtoB_ACK0 & X!RtoB_ACK0) | ((RtoB_ACK1 & X!RtoB_ACK1) | X!DEQ))))) & ((ENQ | !BtoS_ACK1) & (false R (BtoS_ACK1 | (XENQ | X!BtoS_ACK1))))) & (false R (!StoB_REQ0 | (BtoS_ACK0 | XStoB_REQ0)))) & ((FOR_UNTIL_1379310663423513 | (true U ((BtoR_REQ1 & RtoB_ACK1) | (!BtoR_REQ1 & !RtoB_ACK1)))) & (false R (true U ((BtoR_REQ1 & RtoB_ACK1) | (!BtoR_REQ1 & !RtoB_ACK1)))))) & (false R (RtoB_ACK0 | (!BtoR_REQ0 | XBtoR_REQ0)))) & (false R (!BtoR_REQ0 | (!RtoB_ACK0 | XRtoB_ACK0)))) & (false R (!BtoR_REQ0 | (stateG7_1 | !stateG7_0)))) & ((FOR_UNTIL_1379310674229273 | (true U ((StoB_REQ1 & BtoS_ACK1) | (!StoB_REQ1 & !BtoS_ACK1)))) & (false R (true U ((StoB_REQ1 & BtoS_ACK1) | (!StoB_REQ1 & !BtoS_ACK1)))))) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(!stateG7_0 & !stateG7_1)))))) & ((FOR_UNTIL_1379310674209817 | (true U ((StoB_REQ0 & BtoS_ACK0) | (!StoB_REQ0 & !BtoS_ACK0)))) & (false R (true U ((StoB_REQ0 & BtoS_ACK0) | (!StoB_REQ0 & !BtoS_ACK0)))))) & (false R (!DEQ | (stateG12 | X!stateG12))))

1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, -106, 107, -108, -109, 110, 111, 112, 113, -114, 115, 116, -117, 118, 119, -120, 121, 122, 123, 124, -125, -126, 127, 128, 129, -130, 131, -132, 133, 134, -135, 136, 137, 138, -139, 140, 141, 142, 143, 144, 145, 146, -147, 148, -149, 150, 151, 152, 153, 154, 155, -156, 157, 158, 159, -160, 161, 162, 163, -164, 
nx is:
((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((false R (ENQ | (!DEQ | X!FULL))) & !StoB_REQ0) & (false R (!BtoR_REQ0 | !BtoR_REQ1))) & (false R (!RtoB_ACK1 | X!BtoR_REQ1))) & FOR_UNTIL_1379310663376409) & !BtoS_ACK0) & !SLC0) & (false R ((!BtoS_ACK1 & XBtoS_ACK1) | ((!BtoS_ACK0 & XBtoS_ACK0) | X!ENQ)))) & !RtoB_ACK1) & stateG7_0) & (false R (StoB_REQ1 | (BtoS_ACK1 | X!BtoS_ACK1)))) & (false R (!BtoR_REQ1 | (!RtoB_ACK1 | XRtoB_ACK1)))) & (false R (!BtoR_REQ1 | (!stateG7_0 | !stateG7_1)))) & (false R (DEQ | (!stateG12 | XstateG12)))) & FOR_UNTIL_1379310674344473) & (false R (!RtoB_ACK1 | (XRtoB_ACK1 | XDEQ)))) & (false R (StoB_REQ0 | (BtoS_ACK0 | X!BtoS_ACK0)))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_1 | X(stateG7_1 & !stateG7_0)))))) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | X!SLC0)))) & !stateG12) & (false R (StoB_REQ0 | (X!StoB_REQ0 | X!BtoS_ACK0)))) & (false R (!FULL | (!ENQ | DEQ)))) & !FULL) & (false R ((!BtoS_ACK1 & (XBtoS_ACK1 & XSLC0)) | (X!SLC0 & (BtoS_ACK1 | X!BtoS_ACK1))))) & (false R (!EMPTY | !DEQ))) & (false R (!StoB_REQ1 | (BtoS_ACK1 | XStoB_REQ1)))) & !StoB_REQ1) & (false R (true U !stateG12))) & (false R (BtoR_REQ0 | X!RtoB_ACK0))) & stateG7_1) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | (stateG7_0 | X(!stateG7_0 & !stateG7_1))))))) & (false R (StoB_REQ1 | (X!StoB_REQ1 | X!BtoS_ACK1)))) & FOR_UNTIL_1379310674229273) & (false R (!StoB_REQ1 | (!BtoS_ACK1 | XBtoS_ACK1)))) & (false R (!StoB_REQ0 | (!BtoS_ACK0 | XBtoS_ACK0)))) & (false R (EMPTY | (DEQ | (stateG12 | XstateG12))))) & (false R (!ENQ | (DEQ | X!EMPTY)))) & (false R (((!ENQ | !DEQ) & (ENQ | DEQ)) | (((FULL & XFULL) | (!FULL & X!FULL)) & ((!EMPTY & X!EMPTY) | (EMPTY & XEMPTY)))))) & (false R (RtoB_ACK1 | (!BtoR_REQ1 | XBtoR_REQ1)))) & (false R (!BtoS_ACK0 | X!StoB_REQ0))) & (false R (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0))))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_0 | (X(stateG7_1 & !stateG7_0) | !stateG7_1)))))) & (false R (!EMPTY | (stateG12 | X!stateG12)))) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | X(stateG7_0 & !stateG7_1)))))) & (false R (!BtoS_ACK0 | !BtoS_ACK1))) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(stateG7_1 & stateG7_0)))))) & (false R (!RtoB_ACK0 | (XRtoB_ACK0 | XDEQ)))) & (false R (!RtoB_ACK0 | X!BtoR_REQ0))) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | XENQ)))) & (false R (!DEQ | (!stateG12 | X!stateG12)))) & (false R (!BtoS_ACK1 | X!StoB_REQ1))) & (false R (BtoR_REQ1 | X!RtoB_ACK1))) & (false R ((RtoB_ACK0 & X!RtoB_ACK0) | ((RtoB_ACK1 & X!RtoB_ACK1) | X!DEQ)))) & (false R (BtoS_ACK1 | (XENQ | X!BtoS_ACK1)))) & (false R (!StoB_REQ0 | (BtoS_ACK0 | XStoB_REQ0)))) & FOR_UNTIL_1379310663423513) & (false R (true U ((BtoR_REQ1 & RtoB_ACK1) | (!BtoR_REQ1 & !RtoB_ACK1))))) & (false R (RtoB_ACK0 | (!BtoR_REQ0 | XBtoR_REQ0)))) & !ENQ) & (false R (!BtoR_REQ0 | (!RtoB_ACK0 | XRtoB_ACK0)))) & (false R (!BtoR_REQ0 | (stateG7_1 | !stateG7_0)))) & (false R (true U ((StoB_REQ1 & BtoS_ACK1) | (!StoB_REQ1 & !BtoS_ACK1))))) & FOR_UNTIL_1379310674209817) & EMPTY) & !BtoS_ACK1) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(!stateG7_0 & !stateG7_1)))))) & (false R (true U ((StoB_REQ0 & BtoS_ACK0) | (!StoB_REQ0 & !BtoS_ACK0))))) & (false R (!DEQ | (stateG12 | X!stateG12)))) & !RtoB_ACK0) & !DEQ)

f is:
((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((false R (ENQ | (!DEQ | X!FULL))) & !StoB_REQ0) & (false R (!BtoR_REQ0 | !BtoR_REQ1))) & (false R (!RtoB_ACK1 | X!BtoR_REQ1))) & FOR_UNTIL_1379310663376409) & !BtoS_ACK0) & !SLC0) & (false R ((!BtoS_ACK1 & XBtoS_ACK1) | ((!BtoS_ACK0 & XBtoS_ACK0) | X!ENQ)))) & !RtoB_ACK1) & stateG7_0) & (false R (StoB_REQ1 | (BtoS_ACK1 | X!BtoS_ACK1)))) & (false R (!BtoR_REQ1 | (!RtoB_ACK1 | XRtoB_ACK1)))) & (false R (!BtoR_REQ1 | (!stateG7_0 | !stateG7_1)))) & (false R (DEQ | (!stateG12 | XstateG12)))) & FOR_UNTIL_1379310674344473) & (false R (!RtoB_ACK1 | (XRtoB_ACK1 | XDEQ)))) & (false R (StoB_REQ0 | (BtoS_ACK0 | X!BtoS_ACK0)))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_1 | X(stateG7_1 & !stateG7_0)))))) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | X!SLC0)))) & !stateG12) & (false R (StoB_REQ0 | (X!StoB_REQ0 | X!BtoS_ACK0)))) & (false R (!FULL | (!ENQ | DEQ)))) & !FULL) & (false R ((!BtoS_ACK1 & (XBtoS_ACK1 & XSLC0)) | (X!SLC0 & (BtoS_ACK1 | X!BtoS_ACK1))))) & (false R (!EMPTY | !DEQ))) & (false R (!StoB_REQ1 | (BtoS_ACK1 | XStoB_REQ1)))) & !StoB_REQ1) & (false R (true U !stateG12))) & (false R (BtoR_REQ0 | X!RtoB_ACK0))) & stateG7_1) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | (stateG7_0 | X(!stateG7_0 & !stateG7_1))))))) & (false R (StoB_REQ1 | (X!StoB_REQ1 | X!BtoS_ACK1)))) & FOR_UNTIL_1379310674229273) & (false R (!StoB_REQ1 | (!BtoS_ACK1 | XBtoS_ACK1)))) & (false R (!StoB_REQ0 | (!BtoS_ACK0 | XBtoS_ACK0)))) & (false R (EMPTY | (DEQ | (stateG12 | XstateG12))))) & (false R (!ENQ | (DEQ | X!EMPTY)))) & (false R (((!ENQ | !DEQ) & (ENQ | DEQ)) | (((FULL & XFULL) | (!FULL & X!FULL)) & ((!EMPTY & X!EMPTY) | (EMPTY & XEMPTY)))))) & (false R (RtoB_ACK1 | (!BtoR_REQ1 | XBtoR_REQ1)))) & (false R (!BtoS_ACK0 | X!StoB_REQ0))) & (false R (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0))))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_0 | (X(stateG7_1 & !stateG7_0) | !stateG7_1)))))) & (false R (!EMPTY | (stateG12 | X!stateG12)))) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | X(stateG7_0 & !stateG7_1)))))) & (false R (!BtoS_ACK0 | !BtoS_ACK1))) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(stateG7_1 & stateG7_0)))))) & (false R (!RtoB_ACK0 | (XRtoB_ACK0 | XDEQ)))) & (false R (!RtoB_ACK0 | X!BtoR_REQ0))) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | XENQ)))) & (false R (!DEQ | (!stateG12 | X!stateG12)))) & (false R (!BtoS_ACK1 | X!StoB_REQ1))) & (false R (BtoR_REQ1 | X!RtoB_ACK1))) & (false R ((RtoB_ACK0 & X!RtoB_ACK0) | ((RtoB_ACK1 & X!RtoB_ACK1) | X!DEQ)))) & (false R (BtoS_ACK1 | (XENQ | X!BtoS_ACK1)))) & (false R (!StoB_REQ0 | (BtoS_ACK0 | XStoB_REQ0)))) & FOR_UNTIL_1379310663423513) & (false R (true U ((BtoR_REQ1 & RtoB_ACK1) | (!BtoR_REQ1 & !RtoB_ACK1))))) & (false R (RtoB_ACK0 | (!BtoR_REQ0 | XBtoR_REQ0)))) & !ENQ) & (false R (!BtoR_REQ0 | (!RtoB_ACK0 | XRtoB_ACK0)))) & (false R (!BtoR_REQ0 | (stateG7_1 | !stateG7_0)))) & (false R (true U ((StoB_REQ1 & BtoS_ACK1) | (!StoB_REQ1 & !BtoS_ACK1))))) & FOR_UNTIL_1379310674209817) & EMPTY) & !BtoS_ACK1) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(!stateG7_0 & !stateG7_1)))))) & (false R (true U ((StoB_REQ0 & BtoS_ACK0) | (!StoB_REQ0 & !BtoS_ACK0))))) & (false R (!DEQ | (stateG12 | X!stateG12)))) & !RtoB_ACK0) & !DEQ)

cf is:
(((((((((((((((((((((((((!StoB_REQ0 & (!BtoR_REQ0 | !BtoR_REQ1)) & FOR_UNTIL_1379310663376409) & !BtoS_ACK0) & !SLC0) & !RtoB_ACK1) & stateG7_0) & (!BtoR_REQ1 | (!stateG7_0 | !stateG7_1))) & FOR_UNTIL_1379310674344473) & !stateG12) & (!FULL | (!ENQ | DEQ))) & !FULL) & (!EMPTY | !DEQ)) & !StoB_REQ1) & stateG7_1) & FOR_UNTIL_1379310674229273) & (((!ENQ | !DEQ) & (ENQ | DEQ)) | ((FULL | !FULL) & (!EMPTY | EMPTY)))) & (!BtoS_ACK0 | !BtoS_ACK1)) & FOR_UNTIL_1379310663423513) & !ENQ) & (!BtoR_REQ0 | (stateG7_1 | !stateG7_0))) & FOR_UNTIL_1379310674209817) & EMPTY) & !BtoS_ACK1) & !RtoB_ACK0) & !DEQ)

1, 2, -3, 4, -5, 6, -7, 8, 9, 10, 11, 12, 13, 14, -15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, -27, 28, 29, 30, -31, 32, 33, 34, -35, 36, 37, 38, 39, 40, 41, 42, -43, 44, -45, 46, -47, 48, 49, -50, 51, -52, -53, -54, -55, -56, 57, -58, -59, 60, 61, -62, 
{!StoB_REQ0,!BtoS_ACK0,stateG7_0,!stateG12,FOR_UNTIL_1379310674209817,FOR_UNTIL_1379310663423513,!FULL,!BtoS_ACK1,!StoB_REQ1,!SLC0,!RtoB_ACK1,!RtoB_ACK0,!BtoR_REQ1,!BtoR_REQ0,!DEQ,EMPTY,FOR_UNTIL_1379310674344473,FOR_UNTIL_1379310674229273,FOR_UNTIL_1379310663376409,!ENQ,stateG7_1,}
pf is:
(((((((((((((((((((((((((((((((((((((((((((((((((((false R (ENQ | (!DEQ | X!FULL))) & (false R (!BtoR_REQ0 | !BtoR_REQ1))) & (false R (!RtoB_ACK1 | X!BtoR_REQ1))) & ((BtoS_ACK1 | (BtoS_ACK0 | !ENQ)) & (false R ((!BtoS_ACK1 & XBtoS_ACK1) | ((!BtoS_ACK0 & XBtoS_ACK0) | X!ENQ))))) & (!BtoS_ACK1 & (false R (StoB_REQ1 | (BtoS_ACK1 | X!BtoS_ACK1))))) & (false R (!BtoR_REQ1 | (!RtoB_ACK1 | XRtoB_ACK1)))) & (false R (!BtoR_REQ1 | (!stateG7_0 | !stateG7_1)))) & (false R (DEQ | (!stateG12 | XstateG12)))) & (false R (!RtoB_ACK1 | (XRtoB_ACK1 | XDEQ)))) & (!BtoS_ACK0 & (false R (StoB_REQ0 | (BtoS_ACK0 | X!BtoS_ACK0))))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_1 | X(stateG7_1 & !stateG7_0)))))) & ((!BtoS_ACK0 | !SLC0) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | X!SLC0))))) & ((!StoB_REQ0 | !BtoS_ACK0) & (false R (StoB_REQ0 | (X!StoB_REQ0 | X!BtoS_ACK0))))) & (false R (!FULL | (!ENQ | DEQ)))) & (((BtoS_ACK1 & SLC0) | (!SLC0 & !BtoS_ACK1)) & (false R ((!BtoS_ACK1 & (XBtoS_ACK1 & XSLC0)) | (X!SLC0 & (BtoS_ACK1 | X!BtoS_ACK1)))))) & (false R (!EMPTY | !DEQ))) & (false R (!StoB_REQ1 | (BtoS_ACK1 | XStoB_REQ1)))) & ((FOR_UNTIL_1379310674344473 | (true U !stateG12)) & (false R (true U !stateG12)))) & (!RtoB_ACK0 & (false R (BtoR_REQ0 | X!RtoB_ACK0)))) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | (stateG7_0 | X(!stateG7_0 & !stateG7_1))))))) & ((!StoB_REQ1 | !BtoS_ACK1) & (false R (StoB_REQ1 | (X!StoB_REQ1 | X!BtoS_ACK1))))) & (false R (!StoB_REQ1 | (!BtoS_ACK1 | XBtoS_ACK1)))) & (false R (!StoB_REQ0 | (!BtoS_ACK0 | XBtoS_ACK0)))) & (false R (EMPTY | (DEQ | (stateG12 | XstateG12))))) & (false R (!ENQ | (DEQ | X!EMPTY)))) & ((!FULL & EMPTY) & (false R (((!ENQ | !DEQ) & (ENQ | DEQ)) | (((FULL & XFULL) | (!FULL & X!FULL)) & ((!EMPTY & X!EMPTY) | (EMPTY & XEMPTY))))))) & (false R (RtoB_ACK1 | (!BtoR_REQ1 | XBtoR_REQ1)))) & (false R (!BtoS_ACK0 | X!StoB_REQ0))) & ((FOR_UNTIL_1379310663376409 | (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0)))) & (false R (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0)))))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_0 | (X(stateG7_1 & !stateG7_0) | !stateG7_1)))))) & (!stateG12 & (false R (!EMPTY | (stateG12 | X!stateG12))))) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | X(stateG7_0 & !stateG7_1)))))) & (false R (!BtoS_ACK0 | !BtoS_ACK1))) & ((stateG7_1 & stateG7_0) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(stateG7_1 & stateG7_0))))))) & (false R (!RtoB_ACK0 | (XRtoB_ACK0 | XDEQ)))) & (false R (!RtoB_ACK0 | X!BtoR_REQ0))) & ((!BtoS_ACK0 | ENQ) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | XENQ))))) & (false R (!DEQ | (!stateG12 | X!stateG12)))) & (false R (!BtoS_ACK1 | X!StoB_REQ1))) & (!RtoB_ACK1 & (false R (BtoR_REQ1 | X!RtoB_ACK1)))) & (!DEQ & (false R ((RtoB_ACK0 & X!RtoB_ACK0) | ((RtoB_ACK1 & X!RtoB_ACK1) | X!DEQ))))) & ((ENQ | !BtoS_ACK1) & (false R (BtoS_ACK1 | (XENQ | X!BtoS_ACK1))))) & (false R (!StoB_REQ0 | (BtoS_ACK0 | XStoB_REQ0)))) & ((FOR_UNTIL_1379310663423513 | (true U ((BtoR_REQ1 & RtoB_ACK1) | (!BtoR_REQ1 & !RtoB_ACK1)))) & (false R (true U ((BtoR_REQ1 & RtoB_ACK1) | (!BtoR_REQ1 & !RtoB_ACK1)))))) & (false R (RtoB_ACK0 | (!BtoR_REQ0 | XBtoR_REQ0)))) & (false R (!BtoR_REQ0 | (!RtoB_ACK0 | XRtoB_ACK0)))) & (false R (!BtoR_REQ0 | (stateG7_1 | !stateG7_0)))) & ((FOR_UNTIL_1379310674229273 | (true U ((StoB_REQ1 & BtoS_ACK1) | (!StoB_REQ1 & !BtoS_ACK1)))) & (false R (true U ((StoB_REQ1 & BtoS_ACK1) | (!StoB_REQ1 & !BtoS_ACK1)))))) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(!stateG7_0 & !stateG7_1)))))) & ((FOR_UNTIL_1379310674209817 | (true U ((StoB_REQ0 & BtoS_ACK0) | (!StoB_REQ0 & !BtoS_ACK0)))) & (false R (true U ((StoB_REQ0 & BtoS_ACK0) | (!StoB_REQ0 & !BtoS_ACK0)))))) & (false R (!DEQ | (stateG12 | X!stateG12))))

1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, -104, 105, -106, -107, 108, 109, 110, 111, -112, 113, 114, -115, 116, 117, -118, 119, 120, 121, 122, -123, -124, 125, 126, 127, -128, 129, 130, -131, 132, 133, 134, 135, -136, -137, 138, 139, 140, 141, 142, 143, 144, -145, 146, -147, 148, 149, 150, 151, 152, 153, -154, 155, 156, 157, -158, 159, 160, 161, -162, 
nx is:
((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((false R (ENQ | (!DEQ | X!FULL))) & !StoB_REQ0) & (false R (!BtoR_REQ0 | !BtoR_REQ1))) & (false R (!RtoB_ACK1 | X!BtoR_REQ1))) & FOR_UNTIL_1379310663376409) & !BtoS_ACK0) & !SLC0) & (false R ((!BtoS_ACK1 & XBtoS_ACK1) | ((!BtoS_ACK0 & XBtoS_ACK0) | X!ENQ)))) & !RtoB_ACK1) & stateG7_0) & (false R (StoB_REQ1 | (BtoS_ACK1 | X!BtoS_ACK1)))) & (false R (!BtoR_REQ1 | (!RtoB_ACK1 | XRtoB_ACK1)))) & (false R (!BtoR_REQ1 | (!stateG7_0 | !stateG7_1)))) & (false R (DEQ | (!stateG12 | XstateG12)))) & FOR_UNTIL_1379310674344473) & (false R (!RtoB_ACK1 | (XRtoB_ACK1 | XDEQ)))) & (false R (StoB_REQ0 | (BtoS_ACK0 | X!BtoS_ACK0)))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_1 | X(stateG7_1 & !stateG7_0)))))) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | X!SLC0)))) & !stateG12) & (false R (StoB_REQ0 | (X!StoB_REQ0 | X!BtoS_ACK0)))) & (false R (!FULL | (!ENQ | DEQ)))) & !FULL) & (false R ((!BtoS_ACK1 & (XBtoS_ACK1 & XSLC0)) | (X!SLC0 & (BtoS_ACK1 | X!BtoS_ACK1))))) & (false R (!EMPTY | !DEQ))) & (false R (!StoB_REQ1 | (BtoS_ACK1 | XStoB_REQ1)))) & !StoB_REQ1) & (false R (true U !stateG12))) & (false R (BtoR_REQ0 | X!RtoB_ACK0))) & stateG7_1) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | (stateG7_0 | X(!stateG7_0 & !stateG7_1))))))) & (false R (StoB_REQ1 | (X!StoB_REQ1 | X!BtoS_ACK1)))) & FOR_UNTIL_1379310674229273) & (false R (!StoB_REQ1 | (!BtoS_ACK1 | XBtoS_ACK1)))) & (false R (!StoB_REQ0 | (!BtoS_ACK0 | XBtoS_ACK0)))) & (false R (EMPTY | (DEQ | (stateG12 | XstateG12))))) & (false R (!ENQ | (DEQ | X!EMPTY)))) & (false R (((!ENQ | !DEQ) & (ENQ | DEQ)) | (((FULL & XFULL) | (!FULL & X!FULL)) & ((!EMPTY & X!EMPTY) | (EMPTY & XEMPTY)))))) & (false R (RtoB_ACK1 | (!BtoR_REQ1 | XBtoR_REQ1)))) & (false R (!BtoS_ACK0 | X!StoB_REQ0))) & (false R (true U ((BtoR_REQ0 & RtoB_ACK0) | (!BtoR_REQ0 & !RtoB_ACK0))))) & (false R (BtoR_REQ0 | (!BtoR_REQ1 | (stateG7_0 | (X(stateG7_1 & !stateG7_0) | !stateG7_1)))))) & (false R (!EMPTY | (stateG12 | X!stateG12)))) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (stateG7_1 | X(stateG7_0 & !stateG7_1)))))) & (false R (!BtoS_ACK0 | !BtoS_ACK1))) & (false R (BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(stateG7_1 & stateG7_0)))))) & (false R (!RtoB_ACK0 | (XRtoB_ACK0 | XDEQ)))) & (false R (!RtoB_ACK0 | X!BtoR_REQ0))) & (false R (BtoS_ACK0 | (X!BtoS_ACK0 | XENQ)))) & (false R (!DEQ | (!stateG12 | X!stateG12)))) & (false R (!BtoS_ACK1 | X!StoB_REQ1))) & (false R (BtoR_REQ1 | X!RtoB_ACK1))) & (false R ((RtoB_ACK0 & X!RtoB_ACK0) | ((RtoB_ACK1 & X!RtoB_ACK1) | X!DEQ)))) & (false R (BtoS_ACK1 | (XENQ | X!BtoS_ACK1)))) & (false R (!StoB_REQ0 | (BtoS_ACK0 | XStoB_REQ0)))) & FOR_UNTIL_1379310663423513) & (false R (true U ((BtoR_REQ1 & RtoB_ACK1) | (!BtoR_REQ1 & !RtoB_ACK1))))) & (false R (RtoB_ACK0 | (!BtoR_REQ0 | XBtoR_REQ0)))) & !ENQ) & (false R (!BtoR_REQ0 | (!RtoB_ACK0 | XRtoB_ACK0)))) & (false R (!BtoR_REQ0 | (stateG7_1 | !stateG7_0)))) & (false R (true U ((StoB_REQ1 & BtoS_ACK1) | (!StoB_REQ1 & !BtoS_ACK1))))) & FOR_UNTIL_1379310674209817) & EMPTY) & !BtoS_ACK1) & (false R (!BtoR_REQ0 | (BtoR_REQ1 | (!stateG7_1 | X(!stateG7_0 & !stateG7_1)))))) & (false R (true U ((StoB_REQ0 & BtoS_ACK0) | (!StoB_REQ0 & !BtoS_ACK0))))) & (false R (!DEQ | (stateG12 | X!stateG12)))) & !RtoB_ACK0) & !DEQ)

sat