MAYBE Time: 0.205627 TRS: { mark and(X1, X2) -> active and(mark X1, X2), mark true() -> active true(), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark add(X1, X2) -> active add(mark X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), mark cons(X1, X2) -> active cons(X1, X2), mark from X -> active from X, active and(true(), X) -> mark X, active and(false(), Y) -> mark false(), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active add(0(), X) -> mark X, active add(s X, Y) -> mark s add(X, Y), active first(0(), X) -> mark nil(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active from X -> mark cons(X, from s X), 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), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), s mark X -> s X, s active X -> s X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2), 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), from mark X -> from X, from active X -> from X} DP: DP: { mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2), mark# and(X1, X2) -> and#(mark X1, X2), mark# true() -> active# true(), mark# false() -> active# false(), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, X2), mark# add(X1, X2) -> add#(mark X1, X2), mark# 0() -> active# 0(), mark# s X -> active# s X, mark# nil() -> active# nil(), mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> active# first(mark X1, mark X2), mark# first(X1, X2) -> first#(mark X1, mark X2), mark# cons(X1, X2) -> active# cons(X1, X2), mark# from X -> active# from X, active# and(true(), X) -> mark# X, active# and(false(), Y) -> mark# false(), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# add(0(), X) -> mark# X, active# add(s X, Y) -> mark# s add(X, Y), active# add(s X, Y) -> add#(X, Y), active# add(s X, Y) -> s# add(X, Y), active# first(0(), X) -> mark# nil(), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), active# first(s X, cons(Y, Z)) -> first#(X, Z), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), active# from X -> mark# cons(X, from s X), active# from X -> s# X, active# from X -> cons#(X, from s X), active# from X -> from# s X, 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), if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3), add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2), s# mark X -> s# X, s# active X -> s# X, first#(X1, mark X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2), 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), from# mark X -> from# X, from# active X -> from# X} TRS: { mark and(X1, X2) -> active and(mark X1, X2), mark true() -> active true(), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark add(X1, X2) -> active add(mark X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), mark cons(X1, X2) -> active cons(X1, X2), mark from X -> active from X, active and(true(), X) -> mark X, active and(false(), Y) -> mark false(), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active add(0(), X) -> mark X, active add(s X, Y) -> mark s add(X, Y), active first(0(), X) -> mark nil(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active from X -> mark cons(X, from s X), 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), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), s mark X -> s X, s active X -> s X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2), 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), from mark X -> from X, from active X -> from X} EDG: { (active# add(s X, Y) -> mark# s add(X, Y), mark# from X -> active# from X) (active# add(s X, Y) -> mark# s add(X, Y), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# first(X1, X2) -> first#(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# first(X1, X2) -> active# first(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# first(X1, X2) -> mark# X2) (active# add(s X, Y) -> mark# s add(X, Y), mark# first(X1, X2) -> mark# X1) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> active# s X) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> add#(mark X1, X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> active# add(mark X1, X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X1) (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> mark# X1) (active# add(s X, Y) -> mark# s add(X, Y), mark# and(X1, X2) -> and#(mark X1, X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# and(X1, X2) -> active# and(mark X1, X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# and(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# from X -> active# from X) (mark# if(X1, X2, X3) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# if(X1, X2, X3) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# nil() -> active# nil()) (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> active# s X) (mark# if(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# false() -> active# false()) (mark# if(X1, X2, X3) -> mark# X1, mark# true() -> active# true()) (mark# if(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# from X -> active# from X) (mark# add(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# add(X1, X2) -> mark# X1, mark# s X -> active# s X) (mark# add(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, X2)) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, X2)) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# false() -> active# false()) (mark# add(X1, X2) -> mark# X1, mark# true() -> active# true()) (mark# add(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2)) (mark# add(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2)) (mark# add(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3)) (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(X1, active X2) -> cons#(X1, X2)) (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# from X -> from# s X) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# from X -> cons#(X, from s X)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# from X -> s# X) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# from X -> mark# cons(X, from s X)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(0(), X) -> mark# nil()) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y)) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# add(0(), X) -> mark# X) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# if(false(), X, Y) -> mark# Y) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# if(true(), X, Y) -> mark# X) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# and(false(), Y) -> mark# false()) (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# and(true(), X) -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# from X -> active# from X) (active# if(true(), X, Y) -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (active# if(true(), X, Y) -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# first(X1, X2) -> mark# X2) (active# if(true(), X, Y) -> mark# X, mark# first(X1, X2) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# nil() -> active# nil()) (active# if(true(), X, Y) -> mark# X, mark# s X -> active# s X) (active# if(true(), X, Y) -> mark# X, mark# 0() -> active# 0()) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> add#(mark X1, X2)) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, X2)) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# false() -> active# false()) (active# if(true(), X, Y) -> mark# X, mark# true() -> active# true()) (active# if(true(), X, Y) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2)) (active# if(true(), X, Y) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2)) (active# if(true(), X, Y) -> mark# X, mark# and(X1, X2) -> mark# X1) (s# active X -> s# X, s# active X -> s# X) (s# active X -> s# X, s# mark X -> s# X) (from# active X -> from# X, from# active X -> from# X) (from# active X -> from# X, from# mark X -> from# X) (mark# add(X1, X2) -> add#(mark X1, X2), add#(active X1, X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (active# from X -> cons#(X, from s X), cons#(X1, active X2) -> cons#(X1, X2)) (active# from X -> cons#(X, from s X), cons#(X1, mark X2) -> cons#(X1, X2)) (and#(X1, active X2) -> and#(X1, X2), and#(active X1, 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#(X1, active X2) -> and#(X1, X2)) (and#(X1, active X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2)) (and#(active X1, X2) -> and#(X1, X2), and#(active X1, 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#(X1, active X2) -> and#(X1, X2)) (and#(active X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (first#(X1, active X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2)) (first#(X1, active X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2)) (first#(X1, active X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2)) (first#(X1, active X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2)) (first#(active X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2)) (first#(active X1, X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2)) (first#(active X1, X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2)) (first#(active X1, X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, 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#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, 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#(X1, active X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# from X -> from# s X) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# from X -> cons#(X, from s X)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# from X -> s# X) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# from X -> mark# cons(X, from s X)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# first(0(), X) -> mark# nil()) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> s# add(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> add#(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> mark# s add(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(0(), X) -> mark# X) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(false(), X, Y) -> mark# Y) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(true(), X, Y) -> mark# X) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# and(false(), Y) -> mark# false()) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# and(true(), X) -> mark# X) (active# first(0(), X) -> mark# nil(), mark# nil() -> active# nil()) (mark# and(X1, X2) -> active# and(mark X1, X2), active# from X -> from# s X) (mark# and(X1, X2) -> active# and(mark X1, X2), active# from X -> cons#(X, from s X)) (mark# and(X1, X2) -> active# and(mark X1, X2), active# from X -> s# X) (mark# and(X1, X2) -> active# and(mark X1, X2), active# from X -> mark# cons(X, from s X)) (mark# and(X1, X2) -> active# and(mark X1, X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# and(X1, X2) -> active# and(mark X1, X2), active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# and(X1, X2) -> active# and(mark X1, X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# and(X1, X2) -> active# and(mark X1, X2), active# first(0(), X) -> mark# nil()) (mark# and(X1, X2) -> active# and(mark X1, X2), active# add(s X, Y) -> s# add(X, Y)) (mark# and(X1, X2) -> active# and(mark X1, X2), active# add(s X, Y) -> add#(X, Y)) (mark# and(X1, X2) -> active# and(mark X1, X2), active# add(s X, Y) -> mark# s add(X, Y)) (mark# and(X1, X2) -> active# and(mark X1, X2), active# add(0(), X) -> mark# X) (mark# and(X1, X2) -> active# and(mark X1, X2), active# if(false(), X, Y) -> mark# Y) (mark# and(X1, X2) -> active# and(mark X1, X2), active# if(true(), X, Y) -> mark# X) (mark# and(X1, X2) -> active# and(mark X1, X2), active# and(false(), Y) -> mark# false()) (mark# and(X1, X2) -> active# and(mark X1, X2), active# and(true(), X) -> mark# X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> from# s X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> cons#(X, from s X)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> s# X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> mark# cons(X, from s X)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# cons(X1, X2) -> active# cons(X1, X2), active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# cons(X1, X2) -> active# cons(X1, X2), active# first(0(), X) -> mark# nil()) (mark# cons(X1, X2) -> active# cons(X1, X2), active# add(s X, Y) -> s# add(X, Y)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# add(s X, Y) -> add#(X, Y)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# add(s X, Y) -> mark# s add(X, Y)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# add(0(), X) -> mark# X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# if(false(), X, Y) -> mark# Y) (mark# cons(X1, X2) -> active# cons(X1, X2), active# if(true(), X, Y) -> mark# X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# and(false(), Y) -> mark# false()) (mark# cons(X1, X2) -> active# cons(X1, X2), active# and(true(), X) -> mark# X) (mark# s X -> active# s X, active# from X -> from# s X) (mark# s X -> active# s X, active# from X -> cons#(X, from s X)) (mark# s X -> active# s X, active# from X -> s# X) (mark# s X -> active# s X, active# from X -> mark# cons(X, from s X)) (mark# s X -> active# s X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# s X -> active# s X, active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# s X -> active# s X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# s X -> active# s X, active# first(0(), X) -> mark# nil()) (mark# s X -> active# s X, active# add(s X, Y) -> s# add(X, Y)) (mark# s X -> active# s X, active# add(s X, Y) -> add#(X, Y)) (mark# s X -> active# s X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# s X -> active# s X, active# add(0(), X) -> mark# X) (mark# s X -> active# s X, active# if(false(), X, Y) -> mark# Y) (mark# s X -> active# s X, active# if(true(), X, Y) -> mark# X) (mark# s X -> active# s X, active# and(false(), Y) -> mark# false()) (mark# s X -> active# s X, active# and(true(), X) -> mark# X) (active# from X -> from# s X, from# active X -> from# X) (active# from X -> from# s X, from# mark X -> from# X) (mark# from X -> active# from X, active# and(true(), X) -> mark# X) (mark# from X -> active# from X, active# and(false(), Y) -> mark# false()) (mark# from X -> active# from X, active# if(true(), X, Y) -> mark# X) (mark# from X -> active# from X, active# if(false(), X, Y) -> mark# Y) (mark# from X -> active# from X, active# add(0(), X) -> mark# X) (mark# from X -> active# from X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# from X -> active# from X, active# add(s X, Y) -> add#(X, Y)) (mark# from X -> active# from X, active# add(s X, Y) -> s# add(X, Y)) (mark# from X -> active# from X, active# first(0(), X) -> mark# nil()) (mark# from X -> active# from X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# from X -> active# from X, active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# from X -> active# from X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# from X -> active# from X, active# from X -> mark# cons(X, from s X)) (mark# from X -> active# from X, active# from X -> s# X) (mark# from X -> active# from X, active# from X -> cons#(X, from s X)) (mark# from X -> active# from X, active# from X -> from# s X) (active# add(s X, Y) -> s# add(X, Y), s# mark X -> s# X) (active# add(s X, Y) -> s# add(X, Y), s# active X -> s# X) (mark# add(X1, X2) -> active# add(mark X1, X2), active# and(true(), X) -> mark# X) (mark# add(X1, X2) -> active# add(mark X1, X2), active# and(false(), Y) -> mark# false()) (mark# add(X1, X2) -> active# add(mark X1, X2), active# if(true(), X, Y) -> mark# X) (mark# add(X1, X2) -> active# add(mark X1, X2), active# if(false(), X, Y) -> mark# Y) (mark# add(X1, X2) -> active# add(mark X1, X2), active# add(0(), X) -> mark# X) (mark# add(X1, X2) -> active# add(mark X1, X2), active# add(s X, Y) -> mark# s add(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, X2), active# add(s X, Y) -> add#(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, X2), active# add(s X, Y) -> s# add(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, X2), active# first(0(), X) -> mark# nil()) (mark# add(X1, X2) -> active# add(mark X1, X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z))) (mark# add(X1, X2) -> active# add(mark X1, X2), active# first(s X, cons(Y, Z)) -> first#(X, Z)) (mark# add(X1, X2) -> active# add(mark X1, X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z))) (mark# add(X1, X2) -> active# add(mark X1, X2), active# from X -> mark# cons(X, from s X)) (mark# add(X1, X2) -> active# add(mark X1, X2), active# from X -> s# X) (mark# add(X1, X2) -> active# add(mark X1, X2), active# from X -> cons#(X, from s X)) (mark# add(X1, X2) -> active# add(mark X1, X2), active# from X -> from# s X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# and(X1, X2) -> mark# X1) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# and(X1, X2) -> active# and(mark X1, X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# and(X1, X2) -> and#(mark X1, X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# if(X1, X2, X3) -> mark# X1) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# add(X1, X2) -> mark# X1) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# add(X1, X2) -> active# add(mark X1, X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# add(X1, X2) -> add#(mark X1, X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# s X -> active# s X) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> mark# X1) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> mark# X2) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> active# first(mark X1, mark X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> first#(mark X1, mark X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# from X -> active# from X) (active# and(false(), Y) -> mark# false(), mark# false() -> active# false()) (active# if(false(), X, Y) -> mark# Y, mark# and(X1, X2) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# and(X1, X2) -> active# and(mark X1, X2)) (active# if(false(), X, Y) -> mark# Y, mark# and(X1, X2) -> and#(mark X1, X2)) (active# if(false(), X, Y) -> mark# Y, mark# true() -> active# true()) (active# if(false(), X, Y) -> mark# Y, mark# false() -> active# false()) (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> active# add(mark X1, X2)) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> add#(mark X1, X2)) (active# if(false(), X, Y) -> mark# Y, mark# 0() -> active# 0()) (active# if(false(), X, Y) -> mark# Y, mark# s X -> active# s X) (active# if(false(), X, Y) -> mark# Y, mark# nil() -> active# nil()) (active# if(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> mark# X2) (active# if(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# first(X1, X2) -> first#(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# cons(X1, X2) -> active# cons(X1, X2)) (active# if(false(), X, Y) -> mark# Y, mark# from X -> active# from X) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (first#(mark X1, X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2)) (first#(mark X1, X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2)) (first#(mark X1, X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2)) (first#(mark X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2)) (first#(X1, mark X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2)) (first#(X1, mark X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2)) (first#(X1, mark X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2)) (first#(X1, mark X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (and#(mark X1, X2) -> and#(X1, X2), and#(X1, mark 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#(mark X1, X2) -> and#(X1, X2)) (and#(mark X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2)) (and#(X1, mark X2) -> and#(X1, X2), and#(X1, mark 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#(mark X1, X2) -> and#(X1, X2)) (and#(X1, mark X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2)) (mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> active# and(mark X1, X2)) (mark# first(X1, X2) -> mark# X2, mark# and(X1, X2) -> and#(mark X1, X2)) (mark# first(X1, X2) -> mark# X2, mark# true() -> active# true()) (mark# first(X1, X2) -> mark# X2, mark# false() -> active# false()) (mark# first(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# first(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, X2)) (mark# first(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, X2)) (mark# first(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# first(X1, X2) -> mark# X2, mark# s X -> active# s X) (mark# first(X1, X2) -> mark# X2, mark# nil() -> active# nil()) (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X2) (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# first(X1, X2) -> mark# X2, mark# from X -> active# from X) (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)) (from# mark X -> from# X, from# mark X -> from# X) (from# mark X -> from# X, from# active X -> from# X) (s# mark X -> s# X, s# mark X -> s# X) (s# mark X -> s# X, s# active X -> s# X) (active# add(0(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (active# add(0(), X) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2)) (active# add(0(), X) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2)) (active# add(0(), X) -> mark# X, mark# true() -> active# true()) (active# add(0(), X) -> mark# X, mark# false() -> active# false()) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, X2)) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, X2)) (active# add(0(), X) -> mark# X, mark# 0() -> active# 0()) (active# add(0(), X) -> mark# X, mark# s X -> active# s X) (active# add(0(), X) -> mark# X, mark# nil() -> active# nil()) (active# add(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X1) (active# add(0(), X) -> mark# X, mark# first(X1, X2) -> mark# X2) (active# add(0(), X) -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (active# add(0(), X) -> mark# X, mark# from X -> active# from X) (active# and(true(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (active# and(true(), X) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2)) (active# and(true(), X) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2)) (active# and(true(), X) -> mark# X, mark# true() -> active# true()) (active# and(true(), X) -> mark# X, mark# false() -> active# false()) (active# and(true(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (active# and(true(), X) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# and(true(), X) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# and(true(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (active# and(true(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, X2)) (active# and(true(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, X2)) (active# and(true(), X) -> mark# X, mark# 0() -> active# 0()) (active# and(true(), X) -> mark# X, mark# s X -> active# s X) (active# and(true(), X) -> mark# X, mark# nil() -> active# nil()) (active# and(true(), X) -> mark# X, mark# first(X1, X2) -> mark# X1) (active# and(true(), X) -> mark# X, mark# first(X1, X2) -> mark# X2) (active# and(true(), X) -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (active# and(true(), X) -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2)) (active# and(true(), X) -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (active# and(true(), X) -> mark# X, mark# from X -> active# from X) (active# from X -> mark# cons(X, from s X), mark# and(X1, X2) -> mark# X1) (active# from X -> mark# cons(X, from s X), mark# and(X1, X2) -> active# and(mark X1, X2)) (active# from X -> mark# cons(X, from s X), mark# and(X1, X2) -> and#(mark X1, X2)) (active# from X -> mark# cons(X, from s X), mark# if(X1, X2, X3) -> mark# X1) (active# from X -> mark# cons(X, from s X), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# from X -> mark# cons(X, from s X), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# from X -> mark# cons(X, from s X), mark# add(X1, X2) -> mark# X1) (active# from X -> mark# cons(X, from s X), mark# add(X1, X2) -> active# add(mark X1, X2)) (active# from X -> mark# cons(X, from s X), mark# add(X1, X2) -> add#(mark X1, X2)) (active# from X -> mark# cons(X, from s X), mark# s X -> active# s X) (active# from X -> mark# cons(X, from s X), mark# first(X1, X2) -> mark# X1) (active# from X -> mark# cons(X, from s X), mark# first(X1, X2) -> mark# X2) (active# from X -> mark# cons(X, from s X), mark# first(X1, X2) -> active# first(mark X1, mark X2)) (active# from X -> mark# cons(X, from s X), mark# first(X1, X2) -> first#(mark X1, mark X2)) (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# from X -> mark# cons(X, from s X), mark# from X -> active# from X) (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3)) (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3)) (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (mark# first(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2)) (mark# first(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2)) (mark# first(X1, X2) -> mark# X1, mark# true() -> active# true()) (mark# first(X1, X2) -> mark# X1, mark# false() -> active# false()) (mark# first(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# first(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, X2)) (mark# first(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, X2)) (mark# first(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# first(X1, X2) -> mark# X1, mark# s X -> active# s X) (mark# first(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# first(X1, X2) -> mark# X1, mark# from X -> active# from X) (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (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) -> and#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# true() -> active# true()) (mark# and(X1, X2) -> mark# X1, mark# false() -> active# false()) (mark# and(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# and(X1, X2) -> mark# X1, mark# s X -> active# s X) (mark# and(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2) (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2)) (mark# and(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2)) (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# from X -> active# from X) (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(X1, mark X2) -> first#(X1, X2)) (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(X1, active X2) -> first#(X1, X2)) (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(mark X1, X2) -> first#(X1, X2)) (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(active X1, X2) -> first#(X1, X2)) } STATUS: arrows: 0.878252 SCCS (8): Scc: { mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, X2), mark# s X -> active# s X, mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> active# first(mark X1, mark X2), mark# cons(X1, X2) -> active# cons(X1, X2), mark# from X -> active# from X, active# and(true(), X) -> mark# X, active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# add(0(), X) -> mark# X, active# add(s X, Y) -> mark# s add(X, Y), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), active# from X -> mark# cons(X, from s X)} Scc: { from# mark X -> from# X, from# active X -> from# X} Scc: { 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)} Scc: { s# mark X -> s# X, s# active X -> s# X} Scc: { add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)} Scc: { if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)} Scc: { 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)} Scc: { first#(X1, mark X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2)} SCC (19): Strict: { mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, X2), mark# s X -> active# s X, mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> active# first(mark X1, mark X2), mark# cons(X1, X2) -> active# cons(X1, X2), mark# from X -> active# from X, active# and(true(), X) -> mark# X, active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# add(0(), X) -> mark# X, active# add(s X, Y) -> mark# s add(X, Y), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), active# from X -> mark# cons(X, from s X)} Weak: { mark and(X1, X2) -> active and(mark X1, X2), mark true() -> active true(), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark add(X1, X2) -> active add(mark X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), mark cons(X1, X2) -> active cons(X1, X2), mark from X -> active from X, active and(true(), X) -> mark X, active and(false(), Y) -> mark false(), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active add(0(), X) -> mark X, active add(s X, Y) -> mark s add(X, Y), active first(0(), X) -> mark nil(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active from X -> mark cons(X, from s X), 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), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), s mark X -> s X, s active X -> s X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2), 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), from mark X -> from X, from active X -> from X} Open SCC (2): Strict: { from# mark X -> from# X, from# active X -> from# X} Weak: { mark and(X1, X2) -> active and(mark X1, X2), mark true() -> active true(), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark add(X1, X2) -> active add(mark X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), mark cons(X1, X2) -> active cons(X1, X2), mark from X -> active from X, active and(true(), X) -> mark X, active and(false(), Y) -> mark false(), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active add(0(), X) -> mark X, active add(s X, Y) -> mark s add(X, Y), active first(0(), X) -> mark nil(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active from X -> mark cons(X, from s X), 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), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), s mark X -> s X, s active X -> s X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2), 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), from mark X -> from X, from active X -> from X} Open SCC (4): Strict: { 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)} Weak: { mark and(X1, X2) -> active and(mark X1, X2), mark true() -> active true(), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark add(X1, X2) -> active add(mark X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), mark cons(X1, X2) -> active cons(X1, X2), mark from X -> active from X, active and(true(), X) -> mark X, active and(false(), Y) -> mark false(), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active add(0(), X) -> mark X, active add(s X, Y) -> mark s add(X, Y), active first(0(), X) -> mark nil(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active from X -> mark cons(X, from s X), 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), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), s mark X -> s X, s active X -> s X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2), 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), from mark X -> from X, from active X -> from X} Open SCC (2): Strict: { s# mark X -> s# X, s# active X -> s# X} Weak: { mark and(X1, X2) -> active and(mark X1, X2), mark true() -> active true(), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark add(X1, X2) -> active add(mark X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), mark cons(X1, X2) -> active cons(X1, X2), mark from X -> active from X, active and(true(), X) -> mark X, active and(false(), Y) -> mark false(), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active add(0(), X) -> mark X, active add(s X, Y) -> mark s add(X, Y), active first(0(), X) -> mark nil(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active from X -> mark cons(X, from s X), 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), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), s mark X -> s X, s active X -> s X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2), 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), from mark X -> from X, from active X -> from X} Open SCC (4): Strict: { add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)} Weak: { mark and(X1, X2) -> active and(mark X1, X2), mark true() -> active true(), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark add(X1, X2) -> active add(mark X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), mark cons(X1, X2) -> active cons(X1, X2), mark from X -> active from X, active and(true(), X) -> mark X, active and(false(), Y) -> mark false(), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active add(0(), X) -> mark X, active add(s X, Y) -> mark s add(X, Y), active first(0(), X) -> mark nil(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active from X -> mark cons(X, from s X), 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), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), s mark X -> s X, s active X -> s X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2), 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), from mark X -> from X, from active X -> from X} Open SCC (6): Strict: { if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)} Weak: { mark and(X1, X2) -> active and(mark X1, X2), mark true() -> active true(), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark add(X1, X2) -> active add(mark X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), mark cons(X1, X2) -> active cons(X1, X2), mark from X -> active from X, active and(true(), X) -> mark X, active and(false(), Y) -> mark false(), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active add(0(), X) -> mark X, active add(s X, Y) -> mark s add(X, Y), active first(0(), X) -> mark nil(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active from X -> mark cons(X, from s X), 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), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), s mark X -> s X, s active X -> s X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2), 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), from mark X -> from X, from active X -> from X} Open SCC (4): Strict: { 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)} Weak: { mark and(X1, X2) -> active and(mark X1, X2), mark true() -> active true(), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark add(X1, X2) -> active add(mark X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), mark cons(X1, X2) -> active cons(X1, X2), mark from X -> active from X, active and(true(), X) -> mark X, active and(false(), Y) -> mark false(), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active add(0(), X) -> mark X, active add(s X, Y) -> mark s add(X, Y), active first(0(), X) -> mark nil(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active from X -> mark cons(X, from s X), 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), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), s mark X -> s X, s active X -> s X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2), 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), from mark X -> from X, from active X -> from X} Open SCC (4): Strict: { first#(X1, mark X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2)} Weak: { mark and(X1, X2) -> active and(mark X1, X2), mark true() -> active true(), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark add(X1, X2) -> active add(mark X1, X2), mark 0() -> active 0(), mark s X -> active s X, mark nil() -> active nil(), mark first(X1, X2) -> active first(mark X1, mark X2), mark cons(X1, X2) -> active cons(X1, X2), mark from X -> active from X, active and(true(), X) -> mark X, active and(false(), Y) -> mark false(), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active add(0(), X) -> mark X, active add(s X, Y) -> mark s add(X, Y), active first(0(), X) -> mark nil(), active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)), active from X -> mark cons(X, from s X), 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), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), s mark X -> s X, s active X -> s X, first(X1, mark X2) -> first(X1, X2), first(X1, active X2) -> first(X1, X2), first(mark X1, X2) -> first(X1, X2), first(active X1, X2) -> first(X1, X2), 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), from mark X -> from X, from active X -> from X} Open