MAYBE

Problem:
 active(f(X)) -> mark(cons(X,f(g(X))))
 active(g(0())) -> mark(s(0()))
 active(g(s(X))) -> mark(s(s(g(X))))
 active(sel(0(),cons(X,Y))) -> mark(X)
 active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
 mark(f(X)) -> active(f(mark(X)))
 mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
 mark(g(X)) -> active(g(mark(X)))
 mark(0()) -> active(0())
 mark(s(X)) -> active(s(mark(X)))
 mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
 f(mark(X)) -> f(X)
 f(active(X)) -> f(X)
 cons(mark(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)
 g(mark(X)) -> g(X)
 g(active(X)) -> g(X)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 sel(mark(X1),X2) -> sel(X1,X2)
 sel(X1,mark(X2)) -> sel(X1,X2)
 sel(active(X1),X2) -> sel(X1,X2)
 sel(X1,active(X2)) -> sel(X1,X2)

Proof:
 DP Processor:
  DPs:
   active#(f(X)) -> g#(X)
   active#(f(X)) -> f#(g(X))
   active#(f(X)) -> cons#(X,f(g(X)))
   active#(f(X)) -> mark#(cons(X,f(g(X))))
   active#(g(0())) -> s#(0())
   active#(g(0())) -> mark#(s(0()))
   active#(g(s(X))) -> g#(X)
   active#(g(s(X))) -> s#(g(X))
   active#(g(s(X))) -> s#(s(g(X)))
   active#(g(s(X))) -> mark#(s(s(g(X))))
   active#(sel(0(),cons(X,Y))) -> mark#(X)
   active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
   active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
   mark#(f(X)) -> mark#(X)
   mark#(f(X)) -> f#(mark(X))
   mark#(f(X)) -> active#(f(mark(X)))
   mark#(cons(X1,X2)) -> mark#(X1)
   mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
   mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
   mark#(g(X)) -> mark#(X)
   mark#(g(X)) -> g#(mark(X))
   mark#(g(X)) -> active#(g(mark(X)))
   mark#(0()) -> active#(0())
   mark#(s(X)) -> mark#(X)
   mark#(s(X)) -> s#(mark(X))
   mark#(s(X)) -> active#(s(mark(X)))
   mark#(sel(X1,X2)) -> mark#(X2)
   mark#(sel(X1,X2)) -> mark#(X1)
   mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
   mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
   f#(mark(X)) -> f#(X)
   f#(active(X)) -> f#(X)
   cons#(mark(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)
   g#(mark(X)) -> g#(X)
   g#(active(X)) -> g#(X)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
   sel#(mark(X1),X2) -> sel#(X1,X2)
   sel#(X1,mark(X2)) -> sel#(X1,X2)
   sel#(active(X1),X2) -> sel#(X1,X2)
   sel#(X1,active(X2)) -> sel#(X1,X2)
  TRS:
   active(f(X)) -> mark(cons(X,f(g(X))))
   active(g(0())) -> mark(s(0()))
   active(g(s(X))) -> mark(s(s(g(X))))
   active(sel(0(),cons(X,Y))) -> mark(X)
   active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
   mark(f(X)) -> active(f(mark(X)))
   mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
   mark(g(X)) -> active(g(mark(X)))
   mark(0()) -> active(0())
   mark(s(X)) -> active(s(mark(X)))
   mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
   f(mark(X)) -> f(X)
   f(active(X)) -> f(X)
   cons(mark(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)
   g(mark(X)) -> g(X)
   g(active(X)) -> g(X)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   sel(mark(X1),X2) -> sel(X1,X2)
   sel(X1,mark(X2)) -> sel(X1,X2)
   sel(active(X1),X2) -> sel(X1,X2)
   sel(X1,active(X2)) -> sel(X1,X2)
  TDG Processor:
   DPs:
    active#(f(X)) -> g#(X)
    active#(f(X)) -> f#(g(X))
    active#(f(X)) -> cons#(X,f(g(X)))
    active#(f(X)) -> mark#(cons(X,f(g(X))))
    active#(g(0())) -> s#(0())
    active#(g(0())) -> mark#(s(0()))
    active#(g(s(X))) -> g#(X)
    active#(g(s(X))) -> s#(g(X))
    active#(g(s(X))) -> s#(s(g(X)))
    active#(g(s(X))) -> mark#(s(s(g(X))))
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(f(X)) -> mark#(X)
    mark#(f(X)) -> f#(mark(X))
    mark#(f(X)) -> active#(f(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(g(X)) -> mark#(X)
    mark#(g(X)) -> g#(mark(X))
    mark#(g(X)) -> active#(g(mark(X)))
    mark#(0()) -> active#(0())
    mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(sel(X1,X2)) -> mark#(X2)
    mark#(sel(X1,X2)) -> mark#(X1)
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    f#(mark(X)) -> f#(X)
    f#(active(X)) -> f#(X)
    cons#(mark(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)
    g#(mark(X)) -> g#(X)
    g#(active(X)) -> g#(X)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
    sel#(mark(X1),X2) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    sel#(active(X1),X2) -> sel#(X1,X2)
    sel#(X1,active(X2)) -> sel#(X1,X2)
   TRS:
    active(f(X)) -> mark(cons(X,f(g(X))))
    active(g(0())) -> mark(s(0()))
    active(g(s(X))) -> mark(s(s(g(X))))
    active(sel(0(),cons(X,Y))) -> mark(X)
    active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
    mark(f(X)) -> active(f(mark(X)))
    mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
    mark(g(X)) -> active(g(mark(X)))
    mark(0()) -> active(0())
    mark(s(X)) -> active(s(mark(X)))
    mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
    f(mark(X)) -> f(X)
    f(active(X)) -> f(X)
    cons(mark(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)
    g(mark(X)) -> g(X)
    g(active(X)) -> g(X)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    sel(mark(X1),X2) -> sel(X1,X2)
    sel(X1,mark(X2)) -> sel(X1,X2)
    sel(active(X1),X2) -> sel(X1,X2)
    sel(X1,active(X2)) -> sel(X1,X2)
   graph:
    sel#(mark(X1),X2) -> sel#(X1,X2) ->
    sel#(X1,active(X2)) -> sel#(X1,X2)
    sel#(mark(X1),X2) -> sel#(X1,X2) ->
    sel#(active(X1),X2) -> sel#(X1,X2)
    sel#(mark(X1),X2) -> sel#(X1,X2) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    sel#(mark(X1),X2) -> sel#(X1,X2) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    sel#(active(X1),X2) -> sel#(X1,X2) ->
    sel#(X1,active(X2)) -> sel#(X1,X2)
    sel#(active(X1),X2) -> sel#(X1,X2) ->
    sel#(active(X1),X2) -> sel#(X1,X2)
    sel#(active(X1),X2) -> sel#(X1,X2) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    sel#(active(X1),X2) -> sel#(X1,X2) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2) ->
    sel#(X1,active(X2)) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2) ->
    sel#(active(X1),X2) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    sel#(X1,active(X2)) -> sel#(X1,X2) ->
    sel#(X1,active(X2)) -> sel#(X1,X2)
    sel#(X1,active(X2)) -> sel#(X1,X2) ->
    sel#(active(X1),X2) -> sel#(X1,X2)
    sel#(X1,active(X2)) -> sel#(X1,X2) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    sel#(X1,active(X2)) -> sel#(X1,X2) -> sel#(mark(X1),X2) -> sel#(X1,X2)
    s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2)) ->
    sel#(X1,active(X2)) -> sel#(X1,X2)
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2)) ->
    sel#(active(X1),X2) -> sel#(X1,X2)
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2)) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2)) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X1)
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X2)
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> s#(mark(X))
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(g(X)) -> active#(g(mark(X)))
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(g(X)) -> g#(mark(X))
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(g(X)) -> mark#(X)
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(sel(X1,X2)) -> mark#(X2) ->
    mark#(f(X)) -> active#(f(mark(X)))
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(f(X)) -> f#(mark(X))
    mark#(sel(X1,X2)) -> mark#(X2) -> mark#(f(X)) -> mark#(X)
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X1)
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X2)
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(g(X)) -> active#(g(mark(X)))
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(g(X)) -> g#(mark(X))
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(g(X)) -> mark#(X)
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(f(X)) -> active#(f(mark(X)))
    mark#(sel(X1,X2)) -> mark#(X1) -> mark#(f(X)) -> f#(mark(X))
    mark#(sel(X1,X2)) -> mark#(X1) ->
    mark#(f(X)) -> mark#(X)
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(g(s(X))) -> mark#(s(s(g(X))))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(g(s(X))) -> s#(s(g(X)))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(g(s(X))) -> s#(g(X))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(g(s(X))) -> g#(X)
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(g(0())) -> mark#(s(0()))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(g(0())) -> s#(0())
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(f(X)) -> mark#(cons(X,f(g(X))))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(f(X)) -> cons#(X,f(g(X)))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(f(X)) -> f#(g(X))
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2))) ->
    active#(f(X)) -> g#(X)
    mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X)
    mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X)
    mark#(s(X)) -> mark#(X) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    mark#(s(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    mark#(s(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2)
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(s(X)) -> mark#(X) -> mark#(g(X)) -> active#(g(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(g(X)) -> g#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(g(X)) -> mark#(X)
    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)
    mark#(s(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(f(X)) -> f#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(g(s(X))) -> mark#(s(s(g(X))))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(g(s(X))) -> s#(s(g(X)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(g(s(X))) -> s#(g(X))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(g(s(X))) -> g#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(g(0())) -> mark#(s(0()))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(g(0())) -> s#(0())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(f(X)) -> mark#(cons(X,f(g(X))))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(f(X)) -> cons#(X,f(g(X)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(f(X)) -> f#(g(X))
    mark#(s(X)) -> active#(s(mark(X))) -> active#(f(X)) -> g#(X)
    mark#(0()) -> active#(0()) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(0()) -> active#(0()) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(0()) -> active#(0()) -> active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(0()) -> active#(0()) -> active#(g(s(X))) -> mark#(s(s(g(X))))
    mark#(0()) -> active#(0()) -> active#(g(s(X))) -> s#(s(g(X)))
    mark#(0()) -> active#(0()) -> active#(g(s(X))) -> s#(g(X))
    mark#(0()) -> active#(0()) -> active#(g(s(X))) -> g#(X)
    mark#(0()) -> active#(0()) -> active#(g(0())) -> mark#(s(0()))
    mark#(0()) -> active#(0()) -> active#(g(0())) -> s#(0())
    mark#(0()) -> active#(0()) -> active#(f(X)) -> mark#(cons(X,f(g(X))))
    mark#(0()) -> active#(0()) -> active#(f(X)) -> cons#(X,f(g(X)))
    mark#(0()) -> active#(0()) -> active#(f(X)) -> f#(g(X))
    mark#(0()) -> active#(0()) -> active#(f(X)) -> g#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    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))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(g(X)) -> active#(g(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(g(X)) -> g#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(g(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(f(X)) -> active#(f(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(f(X)) -> f#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(f(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(g(s(X))) -> mark#(s(s(g(X))))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(g(s(X))) -> s#(s(g(X)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(g(s(X))) -> s#(g(X))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(g(s(X))) -> g#(X)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(g(0())) -> mark#(s(0()))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(g(0())) -> s#(0())
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(f(X)) -> mark#(cons(X,f(g(X))))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(f(X)) -> cons#(X,f(g(X)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(f(X)) -> f#(g(X))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(f(X)) -> g#(X)
    mark#(g(X)) -> mark#(X) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    mark#(g(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    mark#(g(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1)
    mark#(g(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2)
    mark#(g(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(g(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(g(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(g(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> active#(g(mark(X)))
    mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> g#(mark(X))
    mark#(g(X)) -> mark#(X) -> mark#(g(X)) -> mark#(X)
    mark#(g(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(g(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(g(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(g(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X)))
    mark#(g(X)) -> mark#(X) -> mark#(f(X)) -> f#(mark(X))
    mark#(g(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X)
    mark#(g(X)) -> g#(mark(X)) -> g#(active(X)) -> g#(X)
    mark#(g(X)) -> g#(mark(X)) -> g#(mark(X)) -> g#(X)
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(g(s(X))) -> mark#(s(s(g(X))))
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(g(s(X))) -> s#(s(g(X)))
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(g(s(X))) -> s#(g(X))
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(g(s(X))) -> g#(X)
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(g(0())) -> mark#(s(0()))
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(g(0())) -> s#(0())
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(f(X)) -> mark#(cons(X,f(g(X))))
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(f(X)) -> cons#(X,f(g(X)))
    mark#(g(X)) -> active#(g(mark(X))) ->
    active#(f(X)) -> f#(g(X))
    mark#(g(X)) -> active#(g(mark(X))) -> active#(f(X)) -> g#(X)
    mark#(f(X)) -> mark#(X) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    mark#(f(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    mark#(f(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1)
    mark#(f(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2)
    mark#(f(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(f(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(f(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(f(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(f(X)) -> mark#(X) -> mark#(g(X)) -> active#(g(mark(X)))
    mark#(f(X)) -> mark#(X) -> mark#(g(X)) -> g#(mark(X))
    mark#(f(X)) -> mark#(X) -> mark#(g(X)) -> mark#(X)
    mark#(f(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(f(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(f(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X)))
    mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> f#(mark(X))
    mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X)
    mark#(f(X)) -> f#(mark(X)) -> f#(active(X)) -> f#(X)
    mark#(f(X)) -> f#(mark(X)) -> f#(mark(X)) -> f#(X)
    mark#(f(X)) -> active#(f(mark(X))) ->
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
    mark#(f(X)) -> active#(f(mark(X))) ->
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z)
    mark#(f(X)) -> active#(f(mark(X))) ->
    active#(sel(0(),cons(X,Y))) -> mark#(X)
    mark#(f(X)) -> active#(f(mark(X))) ->
    active#(g(s(X))) -> mark#(s(s(g(X))))
    mark#(f(X)) -> active#(f(mark(X))) ->
    active#(g(s(X))) -> s#(s(g(X)))
    mark#(f(X)) -> active#(f(mark(X))) ->
    active#(g(s(X))) -> s#(g(X))
    mark#(f(X)) -> active#(f(mark(X))) ->
    active#(g(s(X))) -> g#(X)
    mark#(f(X)) -> active#(f(mark(X))) ->
    active#(g(0())) -> mark#(s(0()))
    mark#(f(X)) -> active#(f(mark(X))) ->
    active#(g(0())) -> s#(0())
    mark#(f(X)) -> active#(f(mark(X))) ->
    active#(f(X)) -> mark#(cons(X,f(g(X))))
    mark#(f(X)) -> active#(f(mark(X))) ->
    active#(f(X)) -> cons#(X,f(g(X)))
    mark#(f(X)) -> active#(f(mark(X))) ->
    active#(f(X)) -> f#(g(X))
    mark#(f(X)) -> active#(f(mark(X))) -> active#(f(X)) -> g#(X)
    cons#(mark(X1),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)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,mark(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,active(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#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(active(X1),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#(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#(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#(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#(mark(X1),X2) -> cons#(X1,X2)
    f#(mark(X)) -> f#(X) -> f#(active(X)) -> f#(X)
    f#(mark(X)) -> f#(X) -> f#(mark(X)) -> f#(X)
    f#(active(X)) -> f#(X) -> f#(active(X)) -> f#(X)
    f#(active(X)) -> f#(X) -> f#(mark(X)) -> f#(X)
    g#(mark(X)) -> g#(X) -> g#(active(X)) -> g#(X)
    g#(mark(X)) -> g#(X) -> g#(mark(X)) -> g#(X)
    g#(active(X)) -> g#(X) -> g#(active(X)) -> g#(X)
    g#(active(X)) -> g#(X) -> g#(mark(X)) -> g#(X)
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z) ->
    sel#(X1,active(X2)) -> sel#(X1,X2)
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z) ->
    sel#(active(X1),X2) -> sel#(X1,X2)
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(s(X)) -> s#(mark(X))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(s(X)) -> mark#(X)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(0()) -> active#(0())
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(g(X)) -> active#(g(mark(X)))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(g(X)) -> g#(mark(X))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(g(X)) -> mark#(X)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(f(X)) -> active#(f(mark(X)))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(f(X)) -> f#(mark(X))
    active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z)) ->
    mark#(f(X)) -> mark#(X)
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(s(X)) -> s#(mark(X))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(s(X)) -> mark#(X)
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(0()) -> active#(0())
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(g(X)) -> active#(g(mark(X)))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(g(X)) -> g#(mark(X))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(g(X)) -> mark#(X)
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(f(X)) -> active#(f(mark(X)))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(f(X)) -> f#(mark(X))
    active#(sel(0(),cons(X,Y))) -> mark#(X) ->
    mark#(f(X)) -> mark#(X)
    active#(g(s(X))) -> s#(s(g(X))) -> s#(active(X)) -> s#(X)
    active#(g(s(X))) -> s#(s(g(X))) -> s#(mark(X)) -> s#(X)
    active#(g(s(X))) -> s#(g(X)) -> s#(active(X)) -> s#(X)
    active#(g(s(X))) -> s#(g(X)) -> s#(mark(X)) -> s#(X)
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(s(X)) -> mark#(X)
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(0()) -> active#(0())
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(g(X)) -> active#(g(mark(X)))
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(g(X)) -> g#(mark(X))
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(g(X)) -> mark#(X)
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(f(X)) -> active#(f(mark(X)))
    active#(g(s(X))) -> mark#(s(s(g(X)))) ->
    mark#(f(X)) -> f#(mark(X))
    active#(g(s(X))) -> mark#(s(s(g(X)))) -> mark#(f(X)) -> mark#(X)
    active#(g(s(X))) -> g#(X) -> g#(active(X)) -> g#(X)
    active#(g(s(X))) -> g#(X) -> g#(mark(X)) -> g#(X)
    active#(g(0())) -> s#(0()) -> s#(active(X)) -> s#(X)
    active#(g(0())) -> s#(0()) -> s#(mark(X)) -> s#(X)
    active#(g(0())) -> mark#(s(0())) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(g(0())) -> mark#(s(0())) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(g(0())) -> mark#(s(0())) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(g(0())) -> mark#(s(0())) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(g(0())) -> mark#(s(0())) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(g(0())) -> mark#(s(0())) -> mark#(s(X)) -> s#(mark(X))
    active#(g(0())) -> mark#(s(0())) -> mark#(s(X)) -> mark#(X)
    active#(g(0())) -> mark#(s(0())) -> mark#(0()) -> active#(0())
    active#(g(0())) -> mark#(s(0())) ->
    mark#(g(X)) -> active#(g(mark(X)))
    active#(g(0())) -> mark#(s(0())) -> mark#(g(X)) -> g#(mark(X))
    active#(g(0())) -> mark#(s(0())) -> mark#(g(X)) -> mark#(X)
    active#(g(0())) -> mark#(s(0())) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(g(0())) -> mark#(s(0())) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(g(0())) -> mark#(s(0())) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(g(0())) -> mark#(s(0())) ->
    mark#(f(X)) -> active#(f(mark(X)))
    active#(g(0())) -> mark#(s(0())) -> mark#(f(X)) -> f#(mark(X))
    active#(g(0())) -> mark#(s(0())) ->
    mark#(f(X)) -> mark#(X)
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(sel(X1,X2)) -> sel#(mark(X1),mark(X2))
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(sel(X1,X2)) -> mark#(X1)
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(sel(X1,X2)) -> mark#(X2)
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(s(X)) -> mark#(X)
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(0()) -> active#(0())
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(g(X)) -> active#(g(mark(X)))
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(g(X)) -> g#(mark(X))
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(g(X)) -> mark#(X)
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(f(X)) -> active#(f(mark(X)))
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(f(X)) -> f#(mark(X))
    active#(f(X)) -> mark#(cons(X,f(g(X)))) ->
    mark#(f(X)) -> mark#(X)
    active#(f(X)) -> cons#(X,f(g(X))) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(f(X)) -> cons#(X,f(g(X))) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(f(X)) -> cons#(X,f(g(X))) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(f(X)) -> cons#(X,f(g(X))) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(f(X)) -> f#(g(X)) -> f#(active(X)) -> f#(X)
    active#(f(X)) -> f#(g(X)) -> f#(mark(X)) -> f#(X)
    active#(f(X)) -> g#(X) -> g#(active(X)) -> g#(X)
    active#(f(X)) -> g#(X) -> g#(mark(X)) -> g#(X)
   SCC Processor:
    #sccs: 6
    #rules: 31
    #arcs: 343/1936
    DPs:
     mark#(sel(X1,X2)) -> mark#(X2)
     mark#(f(X)) -> mark#(X)
     mark#(f(X)) -> active#(f(mark(X)))
     active#(f(X)) -> mark#(cons(X,f(g(X))))
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     active#(g(0())) -> mark#(s(0()))
     mark#(g(X)) -> mark#(X)
     mark#(g(X)) -> active#(g(mark(X)))
     active#(g(s(X))) -> mark#(s(s(g(X))))
     mark#(0()) -> active#(0())
     active#(sel(0(),cons(X,Y))) -> mark#(X)
     mark#(s(X)) -> mark#(X)
     mark#(s(X)) -> active#(s(mark(X)))
     active#(sel(s(X),cons(Y,Z))) -> mark#(sel(X,Z))
     mark#(sel(X1,X2)) -> mark#(X1)
     mark#(sel(X1,X2)) -> active#(sel(mark(X1),mark(X2)))
    TRS:
     active(f(X)) -> mark(cons(X,f(g(X))))
     active(g(0())) -> mark(s(0()))
     active(g(s(X))) -> mark(s(s(g(X))))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     mark(f(X)) -> active(f(mark(X)))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(g(X)) -> active(g(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(mark(X)))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     f(mark(X)) -> f(X)
     f(active(X)) -> f(X)
     cons(mark(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)
     g(mark(X)) -> g(X)
     g(active(X)) -> g(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
    Open
    
    DPs:
     cons#(mark(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)
    TRS:
     active(f(X)) -> mark(cons(X,f(g(X))))
     active(g(0())) -> mark(s(0()))
     active(g(s(X))) -> mark(s(s(g(X))))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     mark(f(X)) -> active(f(mark(X)))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(g(X)) -> active(g(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(mark(X)))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     f(mark(X)) -> f(X)
     f(active(X)) -> f(X)
     cons(mark(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)
     g(mark(X)) -> g(X)
     g(active(X)) -> g(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
    Open
    
    DPs:
     g#(mark(X)) -> g#(X)
     g#(active(X)) -> g#(X)
    TRS:
     active(f(X)) -> mark(cons(X,f(g(X))))
     active(g(0())) -> mark(s(0()))
     active(g(s(X))) -> mark(s(s(g(X))))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     mark(f(X)) -> active(f(mark(X)))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(g(X)) -> active(g(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(mark(X)))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     f(mark(X)) -> f(X)
     f(active(X)) -> f(X)
     cons(mark(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)
     g(mark(X)) -> g(X)
     g(active(X)) -> g(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
    Open
    
    DPs:
     f#(mark(X)) -> f#(X)
     f#(active(X)) -> f#(X)
    TRS:
     active(f(X)) -> mark(cons(X,f(g(X))))
     active(g(0())) -> mark(s(0()))
     active(g(s(X))) -> mark(s(s(g(X))))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     mark(f(X)) -> active(f(mark(X)))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(g(X)) -> active(g(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(mark(X)))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     f(mark(X)) -> f(X)
     f(active(X)) -> f(X)
     cons(mark(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)
     g(mark(X)) -> g(X)
     g(active(X)) -> g(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
    Open
    
    DPs:
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
    TRS:
     active(f(X)) -> mark(cons(X,f(g(X))))
     active(g(0())) -> mark(s(0()))
     active(g(s(X))) -> mark(s(s(g(X))))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     mark(f(X)) -> active(f(mark(X)))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(g(X)) -> active(g(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(mark(X)))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     f(mark(X)) -> f(X)
     f(active(X)) -> f(X)
     cons(mark(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)
     g(mark(X)) -> g(X)
     g(active(X)) -> g(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
    Open
    
    DPs:
     sel#(mark(X1),X2) -> sel#(X1,X2)
     sel#(X1,mark(X2)) -> sel#(X1,X2)
     sel#(active(X1),X2) -> sel#(X1,X2)
     sel#(X1,active(X2)) -> sel#(X1,X2)
    TRS:
     active(f(X)) -> mark(cons(X,f(g(X))))
     active(g(0())) -> mark(s(0()))
     active(g(s(X))) -> mark(s(s(g(X))))
     active(sel(0(),cons(X,Y))) -> mark(X)
     active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
     mark(f(X)) -> active(f(mark(X)))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(g(X)) -> active(g(mark(X)))
     mark(0()) -> active(0())
     mark(s(X)) -> active(s(mark(X)))
     mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
     f(mark(X)) -> f(X)
     f(active(X)) -> f(X)
     cons(mark(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)
     g(mark(X)) -> g(X)
     g(active(X)) -> g(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     sel(mark(X1),X2) -> sel(X1,X2)
     sel(X1,mark(X2)) -> sel(X1,X2)
     sel(active(X1),X2) -> sel(X1,X2)
     sel(X1,active(X2)) -> sel(X1,X2)
    Open