MAYBE Time: 0.008478 TRS: { mark cons1(X1, X2) -> cons1(mark X1, mark X2), mark cons(X1, X2) -> cons(mark X1, X2), mark from X -> a__from mark X, mark s X -> s mark X, mark 2nd X -> a__2nd mark X, a__2nd X -> 2nd X, a__2nd cons1(X, cons(Y, Z)) -> mark Y, a__2nd cons(X, X1) -> a__2nd cons1(mark X, mark X1), a__from X -> cons(mark X, from s X), a__from X -> from X} DP: DP: { mark# cons1(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X, mark# from X -> a__from# mark X, mark# s X -> mark# X, mark# 2nd X -> mark# X, mark# 2nd X -> a__2nd# mark X, a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, a__2nd# cons(X, X1) -> mark# X, a__2nd# cons(X, X1) -> mark# X1, a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__from# X -> mark# X} TRS: { mark cons1(X1, X2) -> cons1(mark X1, mark X2), mark cons(X1, X2) -> cons(mark X1, X2), mark from X -> a__from mark X, mark s X -> s mark X, mark 2nd X -> a__2nd mark X, a__2nd X -> 2nd X, a__2nd cons1(X, cons(Y, Z)) -> mark Y, a__2nd cons(X, X1) -> a__2nd cons1(mark X, mark X1), a__from X -> cons(mark X, from s X), a__from X -> from X} EDG: {(mark# from X -> mark# X, mark# 2nd X -> a__2nd# mark X) (mark# from X -> mark# X, mark# 2nd X -> mark# X) (mark# from X -> mark# X, mark# s X -> mark# X) (mark# from X -> mark# X, mark# from X -> a__from# mark X) (mark# from X -> mark# X, mark# from X -> mark# X) (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (mark# 2nd X -> mark# X, mark# 2nd X -> a__2nd# mark X) (mark# 2nd X -> mark# X, mark# 2nd X -> mark# X) (mark# 2nd X -> mark# X, mark# s X -> mark# X) (mark# 2nd X -> mark# X, mark# from X -> a__from# mark X) (mark# 2nd X -> mark# X, mark# from X -> mark# X) (mark# 2nd X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# 2nd X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (mark# 2nd X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# 2nd X -> a__2nd# mark X) (a__from# X -> mark# X, mark# 2nd X -> mark# X) (a__from# X -> mark# X, mark# s X -> mark# X) (a__from# X -> mark# X, mark# from X -> a__from# mark X) (a__from# X -> mark# X, mark# from X -> mark# X) (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# 2nd X -> a__2nd# mark X) (mark# cons(X1, X2) -> mark# X1, mark# 2nd X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1)) (a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__2nd# cons(X, X1) -> mark# X1) (a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__2nd# cons(X, X1) -> mark# X) (a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__2nd# cons1(X, cons(Y, Z)) -> mark# Y) (mark# from X -> a__from# mark X, a__from# X -> mark# X) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons1(X, cons(Y, Z)) -> mark# Y) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> mark# X) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> mark# X1) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1)) (mark# cons1(X1, X2) -> mark# X2, mark# cons1(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X2, mark# cons1(X1, X2) -> mark# X2) (mark# cons1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# cons1(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# cons1(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# cons1(X1, X2) -> mark# X2, mark# 2nd X -> mark# X) (mark# cons1(X1, X2) -> mark# X2, mark# 2nd X -> a__2nd# mark X) (a__2nd# cons(X, X1) -> mark# X1, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X1, mark# cons1(X1, X2) -> mark# X2) (a__2nd# cons(X, X1) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X1, mark# from X -> mark# X) (a__2nd# cons(X, X1) -> mark# X1, mark# from X -> a__from# mark X) (a__2nd# cons(X, X1) -> mark# X1, mark# s X -> mark# X) (a__2nd# cons(X, X1) -> mark# X1, mark# 2nd X -> mark# X) (a__2nd# cons(X, X1) -> mark# X1, mark# 2nd X -> a__2nd# mark X) (mark# cons1(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X2) (mark# cons1(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# cons1(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# cons1(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons1(X1, X2) -> mark# X1, mark# 2nd X -> mark# X) (mark# cons1(X1, X2) -> mark# X1, mark# 2nd X -> a__2nd# mark X) (a__2nd# cons(X, X1) -> mark# X, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X, mark# cons1(X1, X2) -> mark# X2) (a__2nd# cons(X, X1) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X, mark# from X -> mark# X) (a__2nd# cons(X, X1) -> mark# X, mark# from X -> a__from# mark X) (a__2nd# cons(X, X1) -> mark# X, mark# s X -> mark# X) (a__2nd# cons(X, X1) -> mark# X, mark# 2nd X -> mark# X) (a__2nd# cons(X, X1) -> mark# X, mark# 2nd X -> a__2nd# mark X) (mark# s X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# from X -> mark# X) (mark# s X -> mark# X, mark# from X -> a__from# mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# 2nd X -> mark# X) (mark# s X -> mark# X, mark# 2nd X -> a__2nd# mark X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons1(X1, X2) -> mark# X2) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# from X -> mark# X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# from X -> a__from# mark X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# s X -> mark# X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# 2nd X -> mark# X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# 2nd X -> a__2nd# mark X)} EDG: {(mark# from X -> mark# X, mark# 2nd X -> a__2nd# mark X) (mark# from X -> mark# X, mark# 2nd X -> mark# X) (mark# from X -> mark# X, mark# s X -> mark# X) (mark# from X -> mark# X, mark# from X -> a__from# mark X) (mark# from X -> mark# X, mark# from X -> mark# X) (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (mark# 2nd X -> mark# X, mark# 2nd X -> a__2nd# mark X) (mark# 2nd X -> mark# X, mark# 2nd X -> mark# X) (mark# 2nd X -> mark# X, mark# s X -> mark# X) (mark# 2nd X -> mark# X, mark# from X -> a__from# mark X) (mark# 2nd X -> mark# X, mark# from X -> mark# X) (mark# 2nd X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# 2nd X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (mark# 2nd X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# 2nd X -> a__2nd# mark X) (a__from# X -> mark# X, mark# 2nd X -> mark# X) (a__from# X -> mark# X, mark# s X -> mark# X) (a__from# X -> mark# X, mark# from X -> a__from# mark X) (a__from# X -> mark# X, mark# from X -> mark# X) (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# 2nd X -> a__2nd# mark X) (mark# cons(X1, X2) -> mark# X1, mark# 2nd X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__2nd# cons1(X, cons(Y, Z)) -> mark# Y) (mark# from X -> a__from# mark X, a__from# X -> mark# X) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons1(X, cons(Y, Z)) -> mark# Y) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> mark# X) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> mark# X1) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1)) (mark# cons1(X1, X2) -> mark# X2, mark# cons1(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X2, mark# cons1(X1, X2) -> mark# X2) (mark# cons1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# cons1(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# cons1(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# cons1(X1, X2) -> mark# X2, mark# 2nd X -> mark# X) (mark# cons1(X1, X2) -> mark# X2, mark# 2nd X -> a__2nd# mark X) (a__2nd# cons(X, X1) -> mark# X1, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X1, mark# cons1(X1, X2) -> mark# X2) (a__2nd# cons(X, X1) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X1, mark# from X -> mark# X) (a__2nd# cons(X, X1) -> mark# X1, mark# from X -> a__from# mark X) (a__2nd# cons(X, X1) -> mark# X1, mark# s X -> mark# X) (a__2nd# cons(X, X1) -> mark# X1, mark# 2nd X -> mark# X) (a__2nd# cons(X, X1) -> mark# X1, mark# 2nd X -> a__2nd# mark X) (mark# cons1(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X2) (mark# cons1(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# cons1(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# cons1(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons1(X1, X2) -> mark# X1, mark# 2nd X -> mark# X) (mark# cons1(X1, X2) -> mark# X1, mark# 2nd X -> a__2nd# mark X) (a__2nd# cons(X, X1) -> mark# X, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X, mark# cons1(X1, X2) -> mark# X2) (a__2nd# cons(X, X1) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X, mark# from X -> mark# X) (a__2nd# cons(X, X1) -> mark# X, mark# from X -> a__from# mark X) (a__2nd# cons(X, X1) -> mark# X, mark# s X -> mark# X) (a__2nd# cons(X, X1) -> mark# X, mark# 2nd X -> mark# X) (a__2nd# cons(X, X1) -> mark# X, mark# 2nd X -> a__2nd# mark X) (mark# s X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# from X -> mark# X) (mark# s X -> mark# X, mark# from X -> a__from# mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# 2nd X -> mark# X) (mark# s X -> mark# X, mark# 2nd X -> a__2nd# mark X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons1(X1, X2) -> mark# X2) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# from X -> mark# X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# from X -> a__from# mark X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# s X -> mark# X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# 2nd X -> mark# X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# 2nd X -> a__2nd# mark X)} EDG: {(mark# from X -> mark# X, mark# 2nd X -> a__2nd# mark X) (mark# from X -> mark# X, mark# 2nd X -> mark# X) (mark# from X -> mark# X, mark# s X -> mark# X) (mark# from X -> mark# X, mark# from X -> a__from# mark X) (mark# from X -> mark# X, mark# from X -> mark# X) (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (mark# 2nd X -> mark# X, mark# 2nd X -> a__2nd# mark X) (mark# 2nd X -> mark# X, mark# 2nd X -> mark# X) (mark# 2nd X -> mark# X, mark# s X -> mark# X) (mark# 2nd X -> mark# X, mark# from X -> a__from# mark X) (mark# 2nd X -> mark# X, mark# from X -> mark# X) (mark# 2nd X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# 2nd X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (mark# 2nd X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# 2nd X -> a__2nd# mark X) (a__from# X -> mark# X, mark# 2nd X -> mark# X) (a__from# X -> mark# X, mark# s X -> mark# X) (a__from# X -> mark# X, mark# from X -> a__from# mark X) (a__from# X -> mark# X, mark# from X -> mark# X) (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# 2nd X -> a__2nd# mark X) (mark# cons(X1, X2) -> mark# X1, mark# 2nd X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__2nd# cons1(X, cons(Y, Z)) -> mark# Y) (mark# from X -> a__from# mark X, a__from# X -> mark# X) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons1(X, cons(Y, Z)) -> mark# Y) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> mark# X) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> mark# X1) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1)) (mark# cons1(X1, X2) -> mark# X2, mark# cons1(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X2, mark# cons1(X1, X2) -> mark# X2) (mark# cons1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# cons1(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# cons1(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# cons1(X1, X2) -> mark# X2, mark# 2nd X -> mark# X) (mark# cons1(X1, X2) -> mark# X2, mark# 2nd X -> a__2nd# mark X) (a__2nd# cons(X, X1) -> mark# X1, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X1, mark# cons1(X1, X2) -> mark# X2) (a__2nd# cons(X, X1) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X1, mark# from X -> mark# X) (a__2nd# cons(X, X1) -> mark# X1, mark# from X -> a__from# mark X) (a__2nd# cons(X, X1) -> mark# X1, mark# s X -> mark# X) (a__2nd# cons(X, X1) -> mark# X1, mark# 2nd X -> mark# X) (a__2nd# cons(X, X1) -> mark# X1, mark# 2nd X -> a__2nd# mark X) (mark# cons1(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X2) (mark# cons1(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# cons1(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# cons1(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons1(X1, X2) -> mark# X1, mark# 2nd X -> mark# X) (mark# cons1(X1, X2) -> mark# X1, mark# 2nd X -> a__2nd# mark X) (a__2nd# cons(X, X1) -> mark# X, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X, mark# cons1(X1, X2) -> mark# X2) (a__2nd# cons(X, X1) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X, mark# from X -> mark# X) (a__2nd# cons(X, X1) -> mark# X, mark# from X -> a__from# mark X) (a__2nd# cons(X, X1) -> mark# X, mark# s X -> mark# X) (a__2nd# cons(X, X1) -> mark# X, mark# 2nd X -> mark# X) (a__2nd# cons(X, X1) -> mark# X, mark# 2nd X -> a__2nd# mark X) (mark# s X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# from X -> mark# X) (mark# s X -> mark# X, mark# from X -> a__from# mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# 2nd X -> mark# X) (mark# s X -> mark# X, mark# 2nd X -> a__2nd# mark X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons1(X1, X2) -> mark# X2) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# from X -> mark# X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# from X -> a__from# mark X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# s X -> mark# X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# 2nd X -> mark# X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# 2nd X -> a__2nd# mark X)} EDG: {(mark# from X -> mark# X, mark# 2nd X -> a__2nd# mark X) (mark# from X -> mark# X, mark# 2nd X -> mark# X) (mark# from X -> mark# X, mark# s X -> mark# X) (mark# from X -> mark# X, mark# from X -> a__from# mark X) (mark# from X -> mark# X, mark# from X -> mark# X) (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (mark# 2nd X -> mark# X, mark# 2nd X -> a__2nd# mark X) (mark# 2nd X -> mark# X, mark# 2nd X -> mark# X) (mark# 2nd X -> mark# X, mark# s X -> mark# X) (mark# 2nd X -> mark# X, mark# from X -> a__from# mark X) (mark# 2nd X -> mark# X, mark# from X -> mark# X) (mark# 2nd X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# 2nd X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (mark# 2nd X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# 2nd X -> a__2nd# mark X) (a__from# X -> mark# X, mark# 2nd X -> mark# X) (a__from# X -> mark# X, mark# s X -> mark# X) (a__from# X -> mark# X, mark# from X -> a__from# mark X) (a__from# X -> mark# X, mark# from X -> mark# X) (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# 2nd X -> a__2nd# mark X) (mark# cons(X1, X2) -> mark# X1, mark# 2nd X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__2nd# cons1(X, cons(Y, Z)) -> mark# Y) (mark# from X -> a__from# mark X, a__from# X -> mark# X) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons1(X, cons(Y, Z)) -> mark# Y) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> mark# X) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> mark# X1) (mark# 2nd X -> a__2nd# mark X, a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1)) (mark# cons1(X1, X2) -> mark# X2, mark# cons1(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X2, mark# cons1(X1, X2) -> mark# X2) (mark# cons1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# cons1(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# cons1(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# cons1(X1, X2) -> mark# X2, mark# 2nd X -> mark# X) (mark# cons1(X1, X2) -> mark# X2, mark# 2nd X -> a__2nd# mark X) (a__2nd# cons(X, X1) -> mark# X1, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X1, mark# cons1(X1, X2) -> mark# X2) (a__2nd# cons(X, X1) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X1, mark# from X -> mark# X) (a__2nd# cons(X, X1) -> mark# X1, mark# from X -> a__from# mark X) (a__2nd# cons(X, X1) -> mark# X1, mark# s X -> mark# X) (a__2nd# cons(X, X1) -> mark# X1, mark# 2nd X -> mark# X) (a__2nd# cons(X, X1) -> mark# X1, mark# 2nd X -> a__2nd# mark X) (mark# cons1(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X2) (mark# cons1(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons1(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# cons1(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# cons1(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons1(X1, X2) -> mark# X1, mark# 2nd X -> mark# X) (mark# cons1(X1, X2) -> mark# X1, mark# 2nd X -> a__2nd# mark X) (a__2nd# cons(X, X1) -> mark# X, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X, mark# cons1(X1, X2) -> mark# X2) (a__2nd# cons(X, X1) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__2nd# cons(X, X1) -> mark# X, mark# from X -> mark# X) (a__2nd# cons(X, X1) -> mark# X, mark# from X -> a__from# mark X) (a__2nd# cons(X, X1) -> mark# X, mark# s X -> mark# X) (a__2nd# cons(X, X1) -> mark# X, mark# 2nd X -> mark# X) (a__2nd# cons(X, X1) -> mark# X, mark# 2nd X -> a__2nd# mark X) (mark# s X -> mark# X, mark# cons1(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# cons1(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# from X -> mark# X) (mark# s X -> mark# X, mark# from X -> a__from# mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# 2nd X -> mark# X) (mark# s X -> mark# X, mark# 2nd X -> a__2nd# mark X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons1(X1, X2) -> mark# X1) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons1(X1, X2) -> mark# X2) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# from X -> mark# X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# from X -> a__from# mark X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# s X -> mark# X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# 2nd X -> mark# X) (a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, mark# 2nd X -> a__2nd# mark X)} STATUS: arrows: 0.491124 SCCS (1): Scc: { mark# cons1(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X, mark# from X -> a__from# mark X, mark# s X -> mark# X, mark# 2nd X -> mark# X, mark# 2nd X -> a__2nd# mark X, a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, a__2nd# cons(X, X1) -> mark# X, a__2nd# cons(X, X1) -> mark# X1, a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__from# X -> mark# X} SCC (13): Strict: { mark# cons1(X1, X2) -> mark# X1, mark# cons1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X, mark# from X -> a__from# mark X, mark# s X -> mark# X, mark# 2nd X -> mark# X, mark# 2nd X -> a__2nd# mark X, a__2nd# cons1(X, cons(Y, Z)) -> mark# Y, a__2nd# cons(X, X1) -> mark# X, a__2nd# cons(X, X1) -> mark# X1, a__2nd# cons(X, X1) -> a__2nd# cons1(mark X, mark X1), a__from# X -> mark# X} Weak: { mark cons1(X1, X2) -> cons1(mark X1, mark X2), mark cons(X1, X2) -> cons(mark X1, X2), mark from X -> a__from mark X, mark s X -> s mark X, mark 2nd X -> a__2nd mark X, a__2nd X -> 2nd X, a__2nd cons1(X, cons(Y, Z)) -> mark Y, a__2nd cons(X, X1) -> a__2nd cons1(mark X, mark X1), a__from X -> cons(mark X, from s X), a__from X -> from X} Open