MAYBE Time: 0.053046 TRS: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} DP: DP: { sent# up x -> sent# x, rec# sent x -> sent# rec x, rec# sent x -> rec# x, rec# rec x -> sent# rec x, rec# no x -> sent# rec x, rec# no x -> rec# x, rec# up x -> rec# x, rec# bot() -> sent# bot(), no# up x -> no# x, top# sent up x -> rec# x, top# sent up x -> top# check rec x, top# sent up x -> check# rec x, top# rec up x -> rec# x, top# rec up x -> top# check rec x, top# rec up x -> check# rec x, top# no up x -> rec# x, top# no up x -> top# check rec x, top# no up x -> check# rec x, check# sent x -> sent# check x, check# sent x -> check# x, check# rec x -> rec# check x, check# rec x -> check# x, check# no x -> no# check x, check# no x -> check# x, check# up x -> check# x} TRS: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} UR: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} EDG: {(sent# up x -> sent# x, sent# up x -> sent# x) (rec# no x -> rec# x, rec# bot() -> sent# bot()) (rec# no x -> rec# x, rec# up x -> rec# x) (rec# no x -> rec# x, rec# no x -> rec# x) (rec# no x -> rec# x, rec# no x -> sent# rec x) (rec# no x -> rec# x, rec# rec x -> sent# rec x) (rec# no x -> rec# x, rec# sent x -> rec# x) (rec# no x -> rec# x, rec# sent x -> sent# rec x) (no# up x -> no# x, no# up x -> no# x) (top# rec up x -> rec# x, rec# bot() -> sent# bot()) (top# rec up x -> rec# x, rec# up x -> rec# x) (top# rec up x -> rec# x, rec# no x -> rec# x) (top# rec up x -> rec# x, rec# no x -> sent# rec x) (top# rec up x -> rec# x, rec# rec x -> sent# rec x) (top# rec up x -> rec# x, rec# sent x -> rec# x) (top# rec up x -> rec# x, rec# sent x -> sent# rec x) (check# sent x -> check# x, check# up x -> check# x) (check# sent x -> check# x, check# no x -> check# x) (check# sent x -> check# x, check# no x -> no# check x) (check# sent x -> check# x, check# rec x -> check# x) (check# sent x -> check# x, check# rec x -> rec# check x) (check# sent x -> check# x, check# sent x -> check# x) (check# sent x -> check# x, check# sent x -> sent# check x) (check# no x -> check# x, check# up x -> check# x) (check# no x -> check# x, check# no x -> check# x) (check# no x -> check# x, check# no x -> no# check x) (check# no x -> check# x, check# rec x -> check# x) (check# no x -> check# x, check# rec x -> rec# check x) (check# no x -> check# x, check# sent x -> check# x) (check# no x -> check# x, check# sent x -> sent# check x) (top# sent up x -> top# check rec x, top# no up x -> check# rec x) (top# sent up x -> top# check rec x, top# no up x -> top# check rec x) (top# sent up x -> top# check rec x, top# no up x -> rec# x) (top# sent up x -> top# check rec x, top# rec up x -> check# rec x) (top# sent up x -> top# check rec x, top# rec up x -> top# check rec x) (top# sent up x -> top# check rec x, top# rec up x -> rec# x) (top# sent up x -> top# check rec x, top# sent up x -> check# rec x) (top# sent up x -> top# check rec x, top# sent up x -> top# check rec x) (top# sent up x -> top# check rec x, top# sent up x -> rec# x) (top# no up x -> top# check rec x, top# no up x -> check# rec x) (top# no up x -> top# check rec x, top# no up x -> top# check rec x) (top# no up x -> top# check rec x, top# no up x -> rec# x) (top# no up x -> top# check rec x, top# rec up x -> check# rec x) (top# no up x -> top# check rec x, top# rec up x -> top# check rec x) (top# no up x -> top# check rec x, top# rec up x -> rec# x) (top# no up x -> top# check rec x, top# sent up x -> check# rec x) (top# no up x -> top# check rec x, top# sent up x -> top# check rec x) (top# no up x -> top# check rec x, top# sent up x -> rec# x) (rec# rec x -> sent# rec x, sent# up x -> sent# x) (top# sent up x -> check# rec x, check# up x -> check# x) (top# sent up x -> check# rec x, check# no x -> check# x) (top# sent up x -> check# rec x, check# no x -> no# check x) (top# sent up x -> check# rec x, check# rec x -> check# x) (top# sent up x -> check# rec x, check# rec x -> rec# check x) (top# sent up x -> check# rec x, check# sent x -> check# x) (top# sent up x -> check# rec x, check# sent x -> sent# check x) (top# no up x -> check# rec x, check# up x -> check# x) (top# no up x -> check# rec x, check# no x -> check# x) (top# no up x -> check# rec x, check# no x -> no# check x) (top# no up x -> check# rec x, check# rec x -> check# x) (top# no up x -> check# rec x, check# rec x -> rec# check x) (top# no up x -> check# rec x, check# sent x -> check# x) (top# no up x -> check# rec x, check# sent x -> sent# check x) (check# rec x -> rec# check x, rec# bot() -> sent# bot()) (check# rec x -> rec# check x, rec# up x -> rec# x) (check# rec x -> rec# check x, rec# no x -> rec# x) (check# rec x -> rec# check x, rec# no x -> sent# rec x) (check# rec x -> rec# check x, rec# rec x -> sent# rec x) (check# rec x -> rec# check x, rec# sent x -> rec# x) (check# rec x -> rec# check x, rec# sent x -> sent# rec x) (check# no x -> no# check x, no# up x -> no# x) (check# sent x -> sent# check x, sent# up x -> sent# x) (top# rec up x -> check# rec x, check# sent x -> sent# check x) (top# rec up x -> check# rec x, check# sent x -> check# x) (top# rec up x -> check# rec x, check# rec x -> rec# check x) (top# rec up x -> check# rec x, check# rec x -> check# x) (top# rec up x -> check# rec x, check# no x -> no# check x) (top# rec up x -> check# rec x, check# no x -> check# x) (top# rec up x -> check# rec x, check# up x -> check# x) (rec# no x -> sent# rec x, sent# up x -> sent# x) (rec# sent x -> sent# rec x, sent# up x -> sent# x) (top# rec up x -> top# check rec x, top# sent up x -> rec# x) (top# rec up x -> top# check rec x, top# sent up x -> top# check rec x) (top# rec up x -> top# check rec x, top# sent up x -> check# rec x) (top# rec up x -> top# check rec x, top# rec up x -> rec# x) (top# rec up x -> top# check rec x, top# rec up x -> top# check rec x) (top# rec up x -> top# check rec x, top# rec up x -> check# rec x) (top# rec up x -> top# check rec x, top# no up x -> rec# x) (top# rec up x -> top# check rec x, top# no up x -> top# check rec x) (top# rec up x -> top# check rec x, top# no up x -> check# rec x) (check# up x -> check# x, check# sent x -> sent# check x) (check# up x -> check# x, check# sent x -> check# x) (check# up x -> check# x, check# rec x -> rec# check x) (check# up x -> check# x, check# rec x -> check# x) (check# up x -> check# x, check# no x -> no# check x) (check# up x -> check# x, check# no x -> check# x) (check# up x -> check# x, check# up x -> check# x) (check# rec x -> check# x, check# sent x -> sent# check x) (check# rec x -> check# x, check# sent x -> check# x) (check# rec x -> check# x, check# rec x -> rec# check x) (check# rec x -> check# x, check# rec x -> check# x) (check# rec x -> check# x, check# no x -> no# check x) (check# rec x -> check# x, check# no x -> check# x) (check# rec x -> check# x, check# up x -> check# x) (top# no up x -> rec# x, rec# sent x -> sent# rec x) (top# no up x -> rec# x, rec# sent x -> rec# x) (top# no up x -> rec# x, rec# rec x -> sent# rec x) (top# no up x -> rec# x, rec# no x -> sent# rec x) (top# no up x -> rec# x, rec# no x -> rec# x) (top# no up x -> rec# x, rec# up x -> rec# x) (top# no up x -> rec# x, rec# bot() -> sent# bot()) (top# sent up x -> rec# x, rec# sent x -> sent# rec x) (top# sent up x -> rec# x, rec# sent x -> rec# x) (top# sent up x -> rec# x, rec# rec x -> sent# rec x) (top# sent up x -> rec# x, rec# no x -> sent# rec x) (top# sent up x -> rec# x, rec# no x -> rec# x) (top# sent up x -> rec# x, rec# up x -> rec# x) (top# sent up x -> rec# x, rec# bot() -> sent# bot()) (rec# up x -> rec# x, rec# sent x -> sent# rec x) (rec# up x -> rec# x, rec# sent x -> rec# x) (rec# up x -> rec# x, rec# rec x -> sent# rec x) (rec# up x -> rec# x, rec# no x -> sent# rec x) (rec# up x -> rec# x, rec# no x -> rec# x) (rec# up x -> rec# x, rec# up x -> rec# x) (rec# up x -> rec# x, rec# bot() -> sent# bot()) (rec# sent x -> rec# x, rec# sent x -> sent# rec x) (rec# sent x -> rec# x, rec# sent x -> rec# x) (rec# sent x -> rec# x, rec# rec x -> sent# rec x) (rec# sent x -> rec# x, rec# no x -> sent# rec x) (rec# sent x -> rec# x, rec# no x -> rec# x) (rec# sent x -> rec# x, rec# up x -> rec# x) (rec# sent x -> rec# x, rec# bot() -> sent# bot()) (rec# bot() -> sent# bot(), sent# up x -> sent# x)} EDG: {(sent# up x -> sent# x, sent# up x -> sent# x) (rec# no x -> rec# x, rec# bot() -> sent# bot()) (rec# no x -> rec# x, rec# up x -> rec# x) (rec# no x -> rec# x, rec# no x -> rec# x) (rec# no x -> rec# x, rec# no x -> sent# rec x) (rec# no x -> rec# x, rec# rec x -> sent# rec x) (rec# no x -> rec# x, rec# sent x -> rec# x) (rec# no x -> rec# x, rec# sent x -> sent# rec x) (no# up x -> no# x, no# up x -> no# x) (top# rec up x -> rec# x, rec# bot() -> sent# bot()) (top# rec up x -> rec# x, rec# up x -> rec# x) (top# rec up x -> rec# x, rec# no x -> rec# x) (top# rec up x -> rec# x, rec# no x -> sent# rec x) (top# rec up x -> rec# x, rec# rec x -> sent# rec x) (top# rec up x -> rec# x, rec# sent x -> rec# x) (top# rec up x -> rec# x, rec# sent x -> sent# rec x) (check# sent x -> check# x, check# up x -> check# x) (check# sent x -> check# x, check# no x -> check# x) (check# sent x -> check# x, check# no x -> no# check x) (check# sent x -> check# x, check# rec x -> check# x) (check# sent x -> check# x, check# rec x -> rec# check x) (check# sent x -> check# x, check# sent x -> check# x) (check# sent x -> check# x, check# sent x -> sent# check x) (check# no x -> check# x, check# up x -> check# x) (check# no x -> check# x, check# no x -> check# x) (check# no x -> check# x, check# no x -> no# check x) (check# no x -> check# x, check# rec x -> check# x) (check# no x -> check# x, check# rec x -> rec# check x) (check# no x -> check# x, check# sent x -> check# x) (check# no x -> check# x, check# sent x -> sent# check x) (top# sent up x -> top# check rec x, top# no up x -> check# rec x) (top# sent up x -> top# check rec x, top# no up x -> top# check rec x) (top# sent up x -> top# check rec x, top# no up x -> rec# x) (top# sent up x -> top# check rec x, top# rec up x -> check# rec x) (top# sent up x -> top# check rec x, top# rec up x -> top# check rec x) (top# sent up x -> top# check rec x, top# rec up x -> rec# x) (top# sent up x -> top# check rec x, top# sent up x -> check# rec x) (top# sent up x -> top# check rec x, top# sent up x -> top# check rec x) (top# sent up x -> top# check rec x, top# sent up x -> rec# x) (top# no up x -> top# check rec x, top# no up x -> check# rec x) (top# no up x -> top# check rec x, top# no up x -> top# check rec x) (top# no up x -> top# check rec x, top# no up x -> rec# x) (top# no up x -> top# check rec x, top# rec up x -> check# rec x) (top# no up x -> top# check rec x, top# rec up x -> top# check rec x) (top# no up x -> top# check rec x, top# rec up x -> rec# x) (top# no up x -> top# check rec x, top# sent up x -> check# rec x) (top# no up x -> top# check rec x, top# sent up x -> top# check rec x) (top# no up x -> top# check rec x, top# sent up x -> rec# x) (rec# rec x -> sent# rec x, sent# up x -> sent# x) (top# sent up x -> check# rec x, check# up x -> check# x) (top# sent up x -> check# rec x, check# no x -> check# x) (top# sent up x -> check# rec x, check# no x -> no# check x) (top# sent up x -> check# rec x, check# rec x -> check# x) (top# sent up x -> check# rec x, check# rec x -> rec# check x) (top# sent up x -> check# rec x, check# sent x -> check# x) (top# sent up x -> check# rec x, check# sent x -> sent# check x) (top# no up x -> check# rec x, check# up x -> check# x) (top# no up x -> check# rec x, check# no x -> check# x) (top# no up x -> check# rec x, check# no x -> no# check x) (top# no up x -> check# rec x, check# rec x -> check# x) (top# no up x -> check# rec x, check# rec x -> rec# check x) (top# no up x -> check# rec x, check# sent x -> check# x) (top# no up x -> check# rec x, check# sent x -> sent# check x) (check# rec x -> rec# check x, rec# up x -> rec# x) (check# rec x -> rec# check x, rec# no x -> rec# x) (check# rec x -> rec# check x, rec# no x -> sent# rec x) (check# rec x -> rec# check x, rec# rec x -> sent# rec x) (check# rec x -> rec# check x, rec# sent x -> rec# x) (check# rec x -> rec# check x, rec# sent x -> sent# rec x) (check# no x -> no# check x, no# up x -> no# x) (check# sent x -> sent# check x, sent# up x -> sent# x) (top# rec up x -> check# rec x, check# sent x -> sent# check x) (top# rec up x -> check# rec x, check# sent x -> check# x) (top# rec up x -> check# rec x, check# rec x -> rec# check x) (top# rec up x -> check# rec x, check# rec x -> check# x) (top# rec up x -> check# rec x, check# no x -> no# check x) (top# rec up x -> check# rec x, check# no x -> check# x) (top# rec up x -> check# rec x, check# up x -> check# x) (rec# no x -> sent# rec x, sent# up x -> sent# x) (rec# sent x -> sent# rec x, sent# up x -> sent# x) (top# rec up x -> top# check rec x, top# sent up x -> rec# x) (top# rec up x -> top# check rec x, top# sent up x -> top# check rec x) (top# rec up x -> top# check rec x, top# sent up x -> check# rec x) (top# rec up x -> top# check rec x, top# rec up x -> rec# x) (top# rec up x -> top# check rec x, top# rec up x -> top# check rec x) (top# rec up x -> top# check rec x, top# rec up x -> check# rec x) (top# rec up x -> top# check rec x, top# no up x -> rec# x) (top# rec up x -> top# check rec x, top# no up x -> top# check rec x) (top# rec up x -> top# check rec x, top# no up x -> check# rec x) (check# up x -> check# x, check# sent x -> sent# check x) (check# up x -> check# x, check# sent x -> check# x) (check# up x -> check# x, check# rec x -> rec# check x) (check# up x -> check# x, check# rec x -> check# x) (check# up x -> check# x, check# no x -> no# check x) (check# up x -> check# x, check# no x -> check# x) (check# up x -> check# x, check# up x -> check# x) (check# rec x -> check# x, check# sent x -> sent# check x) (check# rec x -> check# x, check# sent x -> check# x) (check# rec x -> check# x, check# rec x -> rec# check x) (check# rec x -> check# x, check# rec x -> check# x) (check# rec x -> check# x, check# no x -> no# check x) (check# rec x -> check# x, check# no x -> check# x) (check# rec x -> check# x, check# up x -> check# x) (top# no up x -> rec# x, rec# sent x -> sent# rec x) (top# no up x -> rec# x, rec# sent x -> rec# x) (top# no up x -> rec# x, rec# rec x -> sent# rec x) (top# no up x -> rec# x, rec# no x -> sent# rec x) (top# no up x -> rec# x, rec# no x -> rec# x) (top# no up x -> rec# x, rec# up x -> rec# x) (top# no up x -> rec# x, rec# bot() -> sent# bot()) (top# sent up x -> rec# x, rec# sent x -> sent# rec x) (top# sent up x -> rec# x, rec# sent x -> rec# x) (top# sent up x -> rec# x, rec# rec x -> sent# rec x) (top# sent up x -> rec# x, rec# no x -> sent# rec x) (top# sent up x -> rec# x, rec# no x -> rec# x) (top# sent up x -> rec# x, rec# up x -> rec# x) (top# sent up x -> rec# x, rec# bot() -> sent# bot()) (rec# up x -> rec# x, rec# sent x -> sent# rec x) (rec# up x -> rec# x, rec# sent x -> rec# x) (rec# up x -> rec# x, rec# rec x -> sent# rec x) (rec# up x -> rec# x, rec# no x -> sent# rec x) (rec# up x -> rec# x, rec# no x -> rec# x) (rec# up x -> rec# x, rec# up x -> rec# x) (rec# up x -> rec# x, rec# bot() -> sent# bot()) (rec# sent x -> rec# x, rec# sent x -> sent# rec x) (rec# sent x -> rec# x, rec# sent x -> rec# x) (rec# sent x -> rec# x, rec# rec x -> sent# rec x) (rec# sent x -> rec# x, rec# no x -> sent# rec x) (rec# sent x -> rec# x, rec# no x -> rec# x) (rec# sent x -> rec# x, rec# up x -> rec# x) (rec# sent x -> rec# x, rec# bot() -> sent# bot())} EDG: {(top# sent up x -> top# check rec x, top# no up x -> check# rec x) (top# sent up x -> top# check rec x, top# no up x -> top# check rec x) (top# sent up x -> top# check rec x, top# no up x -> rec# x) (top# sent up x -> top# check rec x, top# rec up x -> check# rec x) (top# sent up x -> top# check rec x, top# rec up x -> top# check rec x) (top# sent up x -> top# check rec x, top# rec up x -> rec# x) (top# sent up x -> top# check rec x, top# sent up x -> check# rec x) (top# sent up x -> top# check rec x, top# sent up x -> top# check rec x) (top# sent up x -> top# check rec x, top# sent up x -> rec# x) (top# no up x -> top# check rec x, top# no up x -> check# rec x) (top# no up x -> top# check rec x, top# no up x -> top# check rec x) (top# no up x -> top# check rec x, top# no up x -> rec# x) (top# no up x -> top# check rec x, top# rec up x -> check# rec x) (top# no up x -> top# check rec x, top# rec up x -> top# check rec x) (top# no up x -> top# check rec x, top# rec up x -> rec# x) (top# no up x -> top# check rec x, top# sent up x -> check# rec x) (top# no up x -> top# check rec x, top# sent up x -> top# check rec x) (top# no up x -> top# check rec x, top# sent up x -> rec# x) (rec# rec x -> sent# rec x, sent# up x -> sent# x) (top# sent up x -> check# rec x, check# up x -> check# x) (top# sent up x -> check# rec x, check# no x -> check# x) (top# sent up x -> check# rec x, check# no x -> no# check x) (top# sent up x -> check# rec x, check# rec x -> check# x) (top# sent up x -> check# rec x, check# rec x -> rec# check x) (top# sent up x -> check# rec x, check# sent x -> check# x) (top# sent up x -> check# rec x, check# sent x -> sent# check x) (top# no up x -> check# rec x, check# up x -> check# x) (top# no up x -> check# rec x, check# no x -> check# x) (top# no up x -> check# rec x, check# no x -> no# check x) (top# no up x -> check# rec x, check# rec x -> check# x) (top# no up x -> check# rec x, check# rec x -> rec# check x) (top# no up x -> check# rec x, check# sent x -> check# x) (top# no up x -> check# rec x, check# sent x -> sent# check x) (check# rec x -> rec# check x, rec# up x -> rec# x) (check# rec x -> rec# check x, rec# no x -> rec# x) (check# rec x -> rec# check x, rec# no x -> sent# rec x) (check# rec x -> rec# check x, rec# rec x -> sent# rec x) (check# rec x -> rec# check x, rec# sent x -> rec# x) (check# rec x -> rec# check x, rec# sent x -> sent# rec x) (check# no x -> no# check x, no# up x -> no# x) (check# sent x -> sent# check x, sent# up x -> sent# x) (top# rec up x -> check# rec x, check# sent x -> sent# check x) (top# rec up x -> check# rec x, check# sent x -> check# x) (top# rec up x -> check# rec x, check# rec x -> rec# check x) (top# rec up x -> check# rec x, check# rec x -> check# x) (top# rec up x -> check# rec x, check# no x -> no# check x) (top# rec up x -> check# rec x, check# no x -> check# x) (top# rec up x -> check# rec x, check# up x -> check# x) (rec# no x -> sent# rec x, sent# up x -> sent# x) (rec# sent x -> sent# rec x, sent# up x -> sent# x) (top# rec up x -> top# check rec x, top# sent up x -> rec# x) (top# rec up x -> top# check rec x, top# sent up x -> top# check rec x) (top# rec up x -> top# check rec x, top# sent up x -> check# rec x) (top# rec up x -> top# check rec x, top# rec up x -> rec# x) (top# rec up x -> top# check rec x, top# rec up x -> top# check rec x) (top# rec up x -> top# check rec x, top# rec up x -> check# rec x) (top# rec up x -> top# check rec x, top# no up x -> rec# x) (top# rec up x -> top# check rec x, top# no up x -> top# check rec x) (top# rec up x -> top# check rec x, top# no up x -> check# rec x)} EDG: {(top# sent up x -> top# check rec x, top# rec up x -> check# rec x) (top# sent up x -> top# check rec x, top# rec up x -> top# check rec x) (top# sent up x -> top# check rec x, top# rec up x -> rec# x) (top# sent up x -> top# check rec x, top# sent up x -> check# rec x) (top# sent up x -> top# check rec x, top# sent up x -> top# check rec x) (top# sent up x -> top# check rec x, top# sent up x -> rec# x) (top# no up x -> top# check rec x, top# rec up x -> check# rec x) (top# no up x -> top# check rec x, top# rec up x -> top# check rec x) (top# no up x -> top# check rec x, top# rec up x -> rec# x) (top# no up x -> top# check rec x, top# sent up x -> check# rec x) (top# no up x -> top# check rec x, top# sent up x -> top# check rec x) (top# no up x -> top# check rec x, top# sent up x -> rec# x) (rec# rec x -> sent# rec x, sent# up x -> sent# x) (top# sent up x -> check# rec x, check# up x -> check# x) (top# sent up x -> check# rec x, check# rec x -> check# x) (top# sent up x -> check# rec x, check# rec x -> rec# check x) (top# sent up x -> check# rec x, check# sent x -> check# x) (top# sent up x -> check# rec x, check# sent x -> sent# check x) (top# no up x -> check# rec x, check# up x -> check# x) (top# no up x -> check# rec x, check# rec x -> check# x) (top# no up x -> check# rec x, check# rec x -> rec# check x) (top# no up x -> check# rec x, check# sent x -> check# x) (top# no up x -> check# rec x, check# sent x -> sent# check x) (check# rec x -> rec# check x, rec# up x -> rec# x) (check# rec x -> rec# check x, rec# no x -> rec# x) (check# rec x -> rec# check x, rec# no x -> sent# rec x) (check# rec x -> rec# check x, rec# rec x -> sent# rec x) (check# rec x -> rec# check x, rec# sent x -> rec# x) (check# rec x -> rec# check x, rec# sent x -> sent# rec x) (check# no x -> no# check x, no# up x -> no# x) (check# sent x -> sent# check x, sent# up x -> sent# x) (top# rec up x -> check# rec x, check# sent x -> sent# check x) (top# rec up x -> check# rec x, check# sent x -> check# x) (top# rec up x -> check# rec x, check# rec x -> rec# check x) (top# rec up x -> check# rec x, check# rec x -> check# x) (top# rec up x -> check# rec x, check# up x -> check# x) (rec# no x -> sent# rec x, sent# up x -> sent# x) (rec# sent x -> sent# rec x, sent# up x -> sent# x) (top# rec up x -> top# check rec x, top# sent up x -> rec# x) (top# rec up x -> top# check rec x, top# sent up x -> top# check rec x) (top# rec up x -> top# check rec x, top# sent up x -> check# rec x) (top# rec up x -> top# check rec x, top# rec up x -> rec# x) (top# rec up x -> top# check rec x, top# rec up x -> top# check rec x) (top# rec up x -> top# check rec x, top# rec up x -> check# rec x)} STATUS: arrows: 0.929600 SCCS (1): Scc: {top# sent up x -> top# check rec x, top# rec up x -> top# check rec x} SCC (2): Strict: {top# sent up x -> top# check rec x, top# rec up x -> top# check rec x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [sent](x0) = x0, [rec](x0) = x0 + 1, [no](x0) = x0 + 1, [up](x0) = x0 + 1, [top](x0) = 0, [check](x0) = x0, [bot] = 0, [top#](x0) = x0 Strict: top# rec up x -> top# check rec x 2 + 1x >= 1 + 1x top# sent up x -> top# check rec x 1 + 1x >= 1 + 1x Weak: check up x -> up check x 1 + 1x >= 1 + 1x check no x -> no check x 1 + 1x >= 1 + 1x check no x -> no x 1 + 1x >= 1 + 1x check rec x -> rec check x 1 + 1x >= 1 + 1x check sent x -> sent check x 0 + 1x >= 0 + 1x top no up x -> top check rec x 0 + 0x >= 0 + 0x top rec up x -> top check rec x 0 + 0x >= 0 + 0x top sent up x -> top check rec x 0 + 0x >= 0 + 0x no up x -> up no x 2 + 1x >= 2 + 1x rec bot() -> up sent bot() 1 >= 1 rec up x -> up rec x 2 + 1x >= 2 + 1x rec no x -> sent rec x 2 + 1x >= 1 + 1x rec rec x -> sent rec x 2 + 1x >= 1 + 1x rec sent x -> sent rec x 1 + 1x >= 1 + 1x sent up x -> up sent x 1 + 1x >= 1 + 1x SCCS (1): Scc: {top# sent up x -> top# check rec x} SCC (1): Strict: {top# sent up x -> top# check rec x} Weak: { sent up x -> up sent x, rec sent x -> sent rec x, rec rec x -> sent rec x, rec no x -> sent rec x, rec up x -> up rec x, rec bot() -> up sent bot(), no up x -> up no x, top sent up x -> top check rec x, top rec up x -> top check rec x, top no up x -> top check rec x, check sent x -> sent check x, check rec x -> rec check x, check no x -> no x, check no x -> no check x, check up x -> up check x} Fail