MAYBE Time: 1.027789 TRS: { mark cons(X1, X2) -> active cons(mark X1, X2), mark 0() -> active 0(), mark zeros() -> active zeros(), mark and(X1, X2) -> active and(mark X1, X2), mark tt() -> active tt(), mark length X -> active length mark X, mark nil() -> active nil(), mark s X -> active s mark X, cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), active zeros() -> mark cons(0(), zeros()), active and(tt(), X) -> mark X, active length cons(N, L) -> mark s length L, active length nil() -> mark 0(), and(X1, mark X2) -> and(X1, X2), and(X1, active X2) -> and(X1, X2), and(mark X1, X2) -> and(X1, X2), and(active X1, X2) -> and(X1, X2), length mark X -> length X, length active X -> length X, s mark X -> s X, s active X -> s X} DP: DP: { mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2), mark# cons(X1, X2) -> active# cons(mark X1, X2), mark# 0() -> active# 0(), mark# zeros() -> active# zeros(), mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2), mark# and(X1, X2) -> and#(mark X1, X2), mark# tt() -> active# tt(), mark# length X -> mark# X, mark# length X -> active# length mark X, mark# length X -> length# mark X, mark# nil() -> active# nil(), mark# s X -> mark# X, mark# s X -> active# s mark X, mark# s X -> s# mark X, cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2), active# zeros() -> mark# cons(0(), zeros()), active# zeros() -> cons#(0(), zeros()), active# and(tt(), X) -> mark# X, active# length cons(N, L) -> mark# s length L, active# length cons(N, L) -> length# L, active# length cons(N, L) -> s# length L, active# length nil() -> mark# 0(), and#(X1, mark X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2), length# mark X -> length# X, length# active X -> length# X, s# mark X -> s# X, s# active X -> s# X} TRS: { mark cons(X1, X2) -> active cons(mark X1, X2), mark 0() -> active 0(), mark zeros() -> active zeros(), mark and(X1, X2) -> active and(mark X1, X2), mark tt() -> active tt(), mark length X -> active length mark X, mark nil() -> active nil(), mark s X -> active s mark X, cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), active zeros() -> mark cons(0(), zeros()), active and(tt(), X) -> mark X, active length cons(N, L) -> mark s length L, active length nil() -> mark 0(), and(X1, mark X2) -> and(X1, X2), and(X1, active X2) -> and(X1, X2), and(mark X1, X2) -> and(X1, X2), and(active X1, X2) -> and(X1, X2), length mark X -> length X, length active X -> length X, s mark X -> s X, s active X -> s X} EDG: { (mark# and(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# and(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# and(X1, X2) -> mark# X1, mark# length X -> length# mark X) (mark# and(X1, X2) -> mark# X1, mark# length X -> active# length mark X) (mark# and(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# tt() -> active# tt()) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# zeros() -> active# zeros()) (mark# and(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# zeros() -> active# zeros(), active# length nil() -> mark# 0()) (mark# zeros() -> active# zeros(), active# length cons(N, L) -> s# length L) (mark# zeros() -> active# zeros(), active# length cons(N, L) -> length# L) (mark# zeros() -> active# zeros(), active# length cons(N, L) -> mark# s length L) (mark# zeros() -> active# zeros(), active# and(tt(), X) -> mark# X) (mark# zeros() -> active# zeros(), active# zeros() -> cons#(0(), zeros())) (mark# zeros() -> active# zeros(), active# zeros() -> mark# cons(0(), zeros())) (mark# nil() -> active# nil(), active# length nil() -> mark# 0()) (mark# nil() -> active# nil(), active# length cons(N, L) -> s# length L) (mark# nil() -> active# nil(), active# length cons(N, L) -> length# L) (mark# nil() -> active# nil(), active# length cons(N, L) -> mark# s length L) (mark# nil() -> active# nil(), active# and(tt(), X) -> mark# X) (mark# nil() -> active# nil(), active# zeros() -> cons#(0(), zeros())) (mark# nil() -> active# nil(), active# zeros() -> mark# cons(0(), zeros())) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# length nil() -> mark# 0()) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# length cons(N, L) -> s# length L) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# length cons(N, L) -> length# L) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# length cons(N, L) -> mark# s length L) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# and(tt(), X) -> mark# X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# zeros() -> cons#(0(), zeros())) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# zeros() -> mark# cons(0(), zeros())) (active# zeros() -> cons#(0(), zeros()), cons#(active X1, X2) -> cons#(X1, X2)) (active# zeros() -> cons#(0(), zeros()), cons#(mark X1, X2) -> cons#(X1, X2)) (active# zeros() -> cons#(0(), zeros()), cons#(X1, active X2) -> cons#(X1, X2)) (active# zeros() -> cons#(0(), zeros()), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# s X -> mark# X, mark# s X -> s# mark X) (mark# s X -> mark# X, mark# s X -> active# s mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# nil() -> active# nil()) (mark# s X -> mark# X, mark# length X -> length# mark X) (mark# s X -> mark# X, mark# length X -> active# length mark X) (mark# s X -> mark# X, mark# length X -> mark# X) (mark# s X -> mark# X, mark# tt() -> active# tt()) (mark# s X -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2)) (mark# s X -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2)) (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# zeros() -> active# zeros()) (mark# s X -> mark# X, mark# 0() -> active# 0()) (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (length# mark X -> length# X, length# active X -> length# X) (length# mark X -> length# X, length# mark X -> length# X) (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (active# zeros() -> mark# cons(0(), zeros()), mark# s X -> s# mark X) (active# zeros() -> mark# cons(0(), zeros()), mark# s X -> active# s mark X) (active# zeros() -> mark# cons(0(), zeros()), mark# s X -> mark# X) (active# zeros() -> mark# cons(0(), zeros()), mark# nil() -> active# nil()) (active# zeros() -> mark# cons(0(), zeros()), mark# length X -> length# mark X) (active# zeros() -> mark# cons(0(), zeros()), mark# length X -> active# length mark X) (active# zeros() -> mark# cons(0(), zeros()), mark# length X -> mark# X) (active# zeros() -> mark# cons(0(), zeros()), mark# tt() -> active# tt()) (active# zeros() -> mark# cons(0(), zeros()), mark# and(X1, X2) -> and#(mark X1, X2)) (active# zeros() -> mark# cons(0(), zeros()), mark# and(X1, X2) -> active# and(mark X1, X2)) (active# zeros() -> mark# cons(0(), zeros()), mark# and(X1, X2) -> mark# X1) (active# zeros() -> mark# cons(0(), zeros()), mark# zeros() -> active# zeros()) (active# zeros() -> mark# cons(0(), zeros()), mark# 0() -> active# 0()) (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> mark# X1) (mark# s X -> active# s mark X, active# length nil() -> mark# 0()) (mark# s X -> active# s mark X, active# length cons(N, L) -> s# length L) (mark# s X -> active# s mark X, active# length cons(N, L) -> length# L) (mark# s X -> active# s mark X, active# length cons(N, L) -> mark# s length L) (mark# s X -> active# s mark X, active# and(tt(), X) -> mark# X) (mark# s X -> active# s mark X, active# zeros() -> cons#(0(), zeros())) (mark# s X -> active# s mark X, active# zeros() -> mark# cons(0(), zeros())) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (and#(X1, mark X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2)) (and#(X1, mark X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2)) (and#(X1, mark X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2)) (and#(X1, mark X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2)) (and#(mark X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2)) (and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2)) (and#(mark X1, X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2)) (and#(mark X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2)) (active# length cons(N, L) -> length# L, length# active X -> length# X) (active# length cons(N, L) -> length# L, length# mark X -> length# X) (mark# length X -> length# mark X, length# active X -> length# X) (mark# length X -> length# mark X, length# mark X -> length# X) (mark# s X -> s# mark X, s# mark X -> s# X) (mark# s X -> s# mark X, s# active X -> s# X) (active# length cons(N, L) -> s# length L, s# mark X -> s# X) (active# length cons(N, L) -> s# length L, s# active X -> s# X) (and#(active X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2)) (and#(active X1, X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2)) (and#(active X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2)) (and#(active X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2)) (and#(X1, active X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2)) (and#(X1, active X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2)) (and#(X1, active X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2)) (and#(X1, active X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (active# length cons(N, L) -> mark# s length L, mark# cons(X1, X2) -> mark# X1) (active# length cons(N, L) -> mark# s length L, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# length cons(N, L) -> mark# s length L, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# length cons(N, L) -> mark# s length L, mark# 0() -> active# 0()) (active# length cons(N, L) -> mark# s length L, mark# zeros() -> active# zeros()) (active# length cons(N, L) -> mark# s length L, mark# and(X1, X2) -> mark# X1) (active# length cons(N, L) -> mark# s length L, mark# and(X1, X2) -> active# and(mark X1, X2)) (active# length cons(N, L) -> mark# s length L, mark# and(X1, X2) -> and#(mark X1, X2)) (active# length cons(N, L) -> mark# s length L, mark# tt() -> active# tt()) (active# length cons(N, L) -> mark# s length L, mark# length X -> mark# X) (active# length cons(N, L) -> mark# s length L, mark# length X -> active# length mark X) (active# length cons(N, L) -> mark# s length L, mark# length X -> length# mark X) (active# length cons(N, L) -> mark# s length L, mark# nil() -> active# nil()) (active# length cons(N, L) -> mark# s length L, mark# s X -> mark# X) (active# length cons(N, L) -> mark# s length L, mark# s X -> active# s mark X) (active# length cons(N, L) -> mark# s length L, mark# s X -> s# mark X) (mark# length X -> active# length mark X, active# zeros() -> mark# cons(0(), zeros())) (mark# length X -> active# length mark X, active# zeros() -> cons#(0(), zeros())) (mark# length X -> active# length mark X, active# and(tt(), X) -> mark# X) (mark# length X -> active# length mark X, active# length cons(N, L) -> mark# s length L) (mark# length X -> active# length mark X, active# length cons(N, L) -> length# L) (mark# length X -> active# length mark X, active# length cons(N, L) -> s# length L) (mark# length X -> active# length mark X, active# length nil() -> mark# 0()) (mark# and(X1, X2) -> and#(mark X1, X2), and#(X1, mark X2) -> and#(X1, X2)) (mark# and(X1, X2) -> and#(mark X1, X2), and#(X1, active X2) -> and#(X1, X2)) (mark# and(X1, X2) -> and#(mark X1, X2), and#(mark X1, X2) -> and#(X1, X2)) (mark# and(X1, X2) -> and#(mark X1, X2), and#(active X1, X2) -> and#(X1, X2)) (s# active X -> s# X, s# mark X -> s# X) (s# active X -> s# X, s# active X -> s# X) (length# active X -> length# X, length# mark X -> length# X) (length# active X -> length# X, length# active X -> length# X) (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1) (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# and(tt(), X) -> mark# X, mark# 0() -> active# 0()) (active# and(tt(), X) -> mark# X, mark# zeros() -> active# zeros()) (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2)) (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2)) (active# and(tt(), X) -> mark# X, mark# tt() -> active# tt()) (active# and(tt(), X) -> mark# X, mark# length X -> mark# X) (active# and(tt(), X) -> mark# X, mark# length X -> active# length mark X) (active# and(tt(), X) -> mark# X, mark# length X -> length# mark X) (active# and(tt(), X) -> mark# X, mark# nil() -> active# nil()) (active# and(tt(), X) -> mark# X, mark# s X -> mark# X) (active# and(tt(), X) -> mark# X, mark# s X -> active# s mark X) (active# and(tt(), X) -> mark# X, mark# s X -> s# mark X) (mark# length X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# length X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# length X -> mark# X, mark# 0() -> active# 0()) (mark# length X -> mark# X, mark# zeros() -> active# zeros()) (mark# length X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2)) (mark# length X -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2)) (mark# length X -> mark# X, mark# tt() -> active# tt()) (mark# length X -> mark# X, mark# length X -> mark# X) (mark# length X -> mark# X, mark# length X -> active# length mark X) (mark# length X -> mark# X, mark# length X -> length# mark X) (mark# length X -> mark# X, mark# nil() -> active# nil()) (mark# length X -> mark# X, mark# s X -> mark# X) (mark# length X -> mark# X, mark# s X -> active# s mark X) (mark# length X -> mark# X, mark# s X -> s# mark X) (mark# and(X1, X2) -> active# and(mark X1, X2), active# zeros() -> mark# cons(0(), zeros())) (mark# and(X1, X2) -> active# and(mark X1, X2), active# zeros() -> cons#(0(), zeros())) (mark# and(X1, X2) -> active# and(mark X1, X2), active# and(tt(), X) -> mark# X) (mark# and(X1, X2) -> active# and(mark X1, X2), active# length cons(N, L) -> mark# s length L) (mark# and(X1, X2) -> active# and(mark X1, X2), active# length cons(N, L) -> length# L) (mark# and(X1, X2) -> active# and(mark X1, X2), active# length cons(N, L) -> s# length L) (mark# and(X1, X2) -> active# and(mark X1, X2), active# length nil() -> mark# 0()) (active# length nil() -> mark# 0(), mark# cons(X1, X2) -> mark# X1) (active# length nil() -> mark# 0(), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# length nil() -> mark# 0(), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# length nil() -> mark# 0(), mark# 0() -> active# 0()) (active# length nil() -> mark# 0(), mark# zeros() -> active# zeros()) (active# length nil() -> mark# 0(), mark# and(X1, X2) -> mark# X1) (active# length nil() -> mark# 0(), mark# and(X1, X2) -> active# and(mark X1, X2)) (active# length nil() -> mark# 0(), mark# and(X1, X2) -> and#(mark X1, X2)) (active# length nil() -> mark# 0(), mark# tt() -> active# tt()) (active# length nil() -> mark# 0(), mark# length X -> mark# X) (active# length nil() -> mark# 0(), mark# length X -> active# length mark X) (active# length nil() -> mark# 0(), mark# length X -> length# mark X) (active# length nil() -> mark# 0(), mark# nil() -> active# nil()) (active# length nil() -> mark# 0(), mark# s X -> mark# X) (active# length nil() -> mark# 0(), mark# s X -> active# s mark X) (active# length nil() -> mark# 0(), mark# s X -> s# mark X) (mark# tt() -> active# tt(), active# zeros() -> mark# cons(0(), zeros())) (mark# tt() -> active# tt(), active# zeros() -> cons#(0(), zeros())) (mark# tt() -> active# tt(), active# and(tt(), X) -> mark# X) (mark# tt() -> active# tt(), active# length cons(N, L) -> mark# s length L) (mark# tt() -> active# tt(), active# length cons(N, L) -> length# L) (mark# tt() -> active# tt(), active# length cons(N, L) -> s# length L) (mark# tt() -> active# tt(), active# length nil() -> mark# 0()) (mark# 0() -> active# 0(), active# zeros() -> mark# cons(0(), zeros())) (mark# 0() -> active# 0(), active# zeros() -> cons#(0(), zeros())) (mark# 0() -> active# 0(), active# and(tt(), X) -> mark# X) (mark# 0() -> active# 0(), active# length cons(N, L) -> mark# s length L) (mark# 0() -> active# 0(), active# length cons(N, L) -> length# L) (mark# 0() -> active# 0(), active# length cons(N, L) -> s# length L) (mark# 0() -> active# 0(), active# length nil() -> mark# 0()) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> active# zeros()) (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# tt() -> active# tt()) (mark# cons(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# length X -> active# length mark X) (mark# cons(X1, X2) -> mark# X1, mark# length X -> length# mark X) (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X) } EDG: { (mark# and(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# and(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# and(X1, X2) -> mark# X1, mark# length X -> length# mark X) (mark# and(X1, X2) -> mark# X1, mark# length X -> active# length mark X) (mark# and(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# tt() -> active# tt()) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# zeros() -> active# zeros()) (mark# and(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# zeros() -> active# zeros(), active# zeros() -> cons#(0(), zeros())) (mark# zeros() -> active# zeros(), active# zeros() -> mark# cons(0(), zeros())) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# length nil() -> mark# 0()) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# length cons(N, L) -> s# length L) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# length cons(N, L) -> length# L) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# length cons(N, L) -> mark# s length L) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# and(tt(), X) -> mark# X) (mark# s X -> mark# X, mark# s X -> s# mark X) (mark# s X -> mark# X, mark# s X -> active# s mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# nil() -> active# nil()) (mark# s X -> mark# X, mark# length X -> length# mark X) (mark# s X -> mark# X, mark# length X -> active# length mark X) (mark# s X -> mark# X, mark# length X -> mark# X) (mark# s X -> mark# X, mark# tt() -> active# tt()) (mark# s X -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2)) (mark# s X -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2)) (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# zeros() -> active# zeros()) (mark# s X -> mark# X, mark# 0() -> active# 0()) (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (length# mark X -> length# X, length# active X -> length# X) (length# mark X -> length# X, length# mark X -> length# X) (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> mark# X1) (mark# s X -> active# s mark X, active# length nil() -> mark# 0()) (mark# s X -> active# s mark X, active# length cons(N, L) -> s# length L) (mark# s X -> active# s mark X, active# length cons(N, L) -> length# L) (mark# s X -> active# s mark X, active# length cons(N, L) -> mark# s length L) (mark# s X -> active# s mark X, active# and(tt(), X) -> mark# X) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (and#(X1, mark X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2)) (and#(X1, mark X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2)) (and#(X1, mark X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2)) (and#(X1, mark X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2)) (and#(mark X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2)) (and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2)) (and#(mark X1, X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2)) (and#(mark X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2)) (mark# length X -> length# mark X, length# active X -> length# X) (mark# length X -> length# mark X, length# mark X -> length# X) (mark# s X -> s# mark X, s# mark X -> s# X) (mark# s X -> s# mark X, s# active X -> s# X) (active# length cons(N, L) -> s# length L, s# mark X -> s# X) (active# length cons(N, L) -> s# length L, s# active X -> s# X) (and#(active X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2)) (and#(active X1, X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2)) (and#(active X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2)) (and#(active X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2)) (and#(X1, active X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2)) (and#(X1, active X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2)) (and#(X1, active X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2)) (and#(X1, active X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (active# length cons(N, L) -> mark# s length L, mark# cons(X1, X2) -> mark# X1) (active# length cons(N, L) -> mark# s length L, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# length cons(N, L) -> mark# s length L, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# length cons(N, L) -> mark# s length L, mark# and(X1, X2) -> mark# X1) (active# length cons(N, L) -> mark# s length L, mark# and(X1, X2) -> active# and(mark X1, X2)) (active# length cons(N, L) -> mark# s length L, mark# and(X1, X2) -> and#(mark X1, X2)) (active# length cons(N, L) -> mark# s length L, mark# length X -> mark# X) (active# length cons(N, L) -> mark# s length L, mark# length X -> active# length mark X) (active# length cons(N, L) -> mark# s length L, mark# length X -> length# mark X) (active# length cons(N, L) -> mark# s length L, mark# s X -> mark# X) (active# length cons(N, L) -> mark# s length L, mark# s X -> active# s mark X) (active# length cons(N, L) -> mark# s length L, mark# s X -> s# mark X) (mark# length X -> active# length mark X, active# and(tt(), X) -> mark# X) (mark# length X -> active# length mark X, active# length cons(N, L) -> mark# s length L) (mark# length X -> active# length mark X, active# length cons(N, L) -> length# L) (mark# length X -> active# length mark X, active# length cons(N, L) -> s# length L) (mark# length X -> active# length mark X, active# length nil() -> mark# 0()) (mark# and(X1, X2) -> and#(mark X1, X2), and#(mark X1, X2) -> and#(X1, X2)) (mark# and(X1, X2) -> and#(mark X1, X2), and#(active X1, X2) -> and#(X1, X2)) (s# active X -> s# X, s# mark X -> s# X) (s# active X -> s# X, s# active X -> s# X) (length# active X -> length# X, length# mark X -> length# X) (length# active X -> length# X, length# active X -> length# X) (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1) (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# and(tt(), X) -> mark# X, mark# 0() -> active# 0()) (active# and(tt(), X) -> mark# X, mark# zeros() -> active# zeros()) (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2)) (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2)) (active# and(tt(), X) -> mark# X, mark# tt() -> active# tt()) (active# and(tt(), X) -> mark# X, mark# length X -> mark# X) (active# and(tt(), X) -> mark# X, mark# length X -> active# length mark X) (active# and(tt(), X) -> mark# X, mark# length X -> length# mark X) (active# and(tt(), X) -> mark# X, mark# nil() -> active# nil()) (active# and(tt(), X) -> mark# X, mark# s X -> mark# X) (active# and(tt(), X) -> mark# X, mark# s X -> active# s mark X) (active# and(tt(), X) -> mark# X, mark# s X -> s# mark X) (mark# length X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# length X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# length X -> mark# X, mark# 0() -> active# 0()) (mark# length X -> mark# X, mark# zeros() -> active# zeros()) (mark# length X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2)) (mark# length X -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2)) (mark# length X -> mark# X, mark# tt() -> active# tt()) (mark# length X -> mark# X, mark# length X -> mark# X) (mark# length X -> mark# X, mark# length X -> active# length mark X) (mark# length X -> mark# X, mark# length X -> length# mark X) (mark# length X -> mark# X, mark# nil() -> active# nil()) (mark# length X -> mark# X, mark# s X -> mark# X) (mark# length X -> mark# X, mark# s X -> active# s mark X) (mark# length X -> mark# X, mark# s X -> s# mark X) (mark# and(X1, X2) -> active# and(mark X1, X2), active# and(tt(), X) -> mark# X) (mark# and(X1, X2) -> active# and(mark X1, X2), active# length cons(N, L) -> mark# s length L) (mark# and(X1, X2) -> active# and(mark X1, X2), active# length cons(N, L) -> length# L) (mark# and(X1, X2) -> active# and(mark X1, X2), active# length cons(N, L) -> s# length L) (mark# and(X1, X2) -> active# and(mark X1, X2), active# length nil() -> mark# 0()) (active# length nil() -> mark# 0(), mark# 0() -> active# 0()) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> active# zeros()) (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# tt() -> active# tt()) (mark# cons(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# length X -> active# length mark X) (mark# cons(X1, X2) -> mark# X1, mark# length X -> length# mark X) (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X) } STATUS: arrows: 0.897959 SCCS (3): Scc: { mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2), mark# zeros() -> active# zeros(), mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2), mark# length X -> mark# X, mark# length X -> active# length mark X, mark# s X -> mark# X, mark# s X -> active# s mark X, active# zeros() -> mark# cons(0(), zeros()), active# and(tt(), X) -> mark# X, active# length cons(N, L) -> mark# s length L} Scc: { s# mark X -> s# X, s# active X -> s# X} Scc: { length# mark X -> length# X, length# active X -> length# X} SCC (12): Strict: { mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2), mark# zeros() -> active# zeros(), mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2), mark# length X -> mark# X, mark# length X -> active# length mark X, mark# s X -> mark# X, mark# s X -> active# s mark X, active# zeros() -> mark# cons(0(), zeros()), active# and(tt(), X) -> mark# X, active# length cons(N, L) -> mark# s length L} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark 0() -> active 0(), mark zeros() -> active zeros(), mark and(X1, X2) -> active and(mark X1, X2), mark tt() -> active tt(), mark length X -> active length mark X, mark nil() -> active nil(), mark s X -> active s mark X, cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), active zeros() -> mark cons(0(), zeros()), active and(tt(), X) -> mark X, active length cons(N, L) -> mark s length L, active length nil() -> mark 0(), and(X1, mark X2) -> and(X1, X2), and(X1, active X2) -> and(X1, X2), and(mark X1, X2) -> and(X1, X2), and(active X1, X2) -> and(X1, X2), length mark X -> length X, length active X -> length X, s mark X -> s X, s active X -> s X} Open SCC (2): Strict: { s# mark X -> s# X, s# active X -> s# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark 0() -> active 0(), mark zeros() -> active zeros(), mark and(X1, X2) -> active and(mark X1, X2), mark tt() -> active tt(), mark length X -> active length mark X, mark nil() -> active nil(), mark s X -> active s mark X, cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), active zeros() -> mark cons(0(), zeros()), active and(tt(), X) -> mark X, active length cons(N, L) -> mark s length L, active length nil() -> mark 0(), and(X1, mark X2) -> and(X1, X2), and(X1, active X2) -> and(X1, X2), and(mark X1, X2) -> and(X1, X2), and(active X1, X2) -> and(X1, X2), length mark X -> length X, length active X -> length X, s mark X -> s X, s active X -> s X} Open SCC (2): Strict: { length# mark X -> length# X, length# active X -> length# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark 0() -> active 0(), mark zeros() -> active zeros(), mark and(X1, X2) -> active and(mark X1, X2), mark tt() -> active tt(), mark length X -> active length mark X, mark nil() -> active nil(), mark s X -> active s mark X, cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), active zeros() -> mark cons(0(), zeros()), active and(tt(), X) -> mark X, active length cons(N, L) -> mark s length L, active length nil() -> mark 0(), and(X1, mark X2) -> and(X1, X2), and(X1, active X2) -> and(X1, X2), and(mark X1, X2) -> and(X1, X2), and(active X1, X2) -> and(X1, X2), length mark X -> length X, length active X -> length X, s mark X -> s X, s active X -> s X} Open