MAYBE
TRS:
 {        -(x, 0()) -> x,
      -(s(x), s(y)) -> -(x, y),
          *(x, 0()) -> 0(),
         *(x, s(y)) -> +(*(x, y), x),
   if(true(), x, y) -> x,
   if(true(), x, y) -> true(),
  if(false(), x, y) -> y,
  if(false(), x, y) -> false(),
           odd(0()) -> false(),
        odd(s(0())) -> true(),
       odd(s(s(x))) -> odd(x),
          half(0()) -> 0(),
       half(s(0())) -> 0(),
      half(s(s(x))) -> s(half(x)),
       f(x, 0(), z) -> z,
      f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)),
          pow(x, y) -> f(x, y, s(0()))}
 DP:
  Strict:
   {-#(s(x), s(y)) -> -#(x, y),
       *#(x, s(y)) -> *#(x, y),
     odd#(s(s(x))) -> odd#(x),
    half#(s(s(x))) -> half#(x),
    f#(x, s(y), z) -> *#(x, x),
    f#(x, s(y), z) -> *#(x, z),
    f#(x, s(y), z) -> if#(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)),
    f#(x, s(y), z) -> odd#(s(y)),
    f#(x, s(y), z) -> half#(s(y)),
    f#(x, s(y), z) -> f#(x, y, *(x, z)),
    f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z),
        pow#(x, y) -> f#(x, y, s(0()))}
  Weak:
  {        -(x, 0()) -> x,
       -(s(x), s(y)) -> -(x, y),
           *(x, 0()) -> 0(),
          *(x, s(y)) -> +(*(x, y), x),
    if(true(), x, y) -> x,
    if(true(), x, y) -> true(),
   if(false(), x, y) -> y,
   if(false(), x, y) -> false(),
            odd(0()) -> false(),
         odd(s(0())) -> true(),
        odd(s(s(x))) -> odd(x),
           half(0()) -> 0(),
        half(s(0())) -> 0(),
       half(s(s(x))) -> s(half(x)),
        f(x, 0(), z) -> z,
       f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)),
           pow(x, y) -> f(x, y, s(0()))}
  EDG:
   {(odd#(s(s(x))) -> odd#(x), odd#(s(s(x))) -> odd#(x))
    (pow#(x, y) -> f#(x, y, s(0())), f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z))
    (pow#(x, y) -> f#(x, y, s(0())), f#(x, s(y), z) -> f#(x, y, *(x, z)))
    (pow#(x, y) -> f#(x, y, s(0())), f#(x, s(y), z) -> half#(s(y)))
    (pow#(x, y) -> f#(x, y, s(0())), f#(x, s(y), z) -> odd#(s(y)))
    (pow#(x, y) -> f#(x, y, s(0())), f#(x, s(y), z) -> if#(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)))
    (pow#(x, y) -> f#(x, y, s(0())), f#(x, s(y), z) -> *#(x, z))
    (pow#(x, y) -> f#(x, y, s(0())), f#(x, s(y), z) -> *#(x, x))
    (-#(s(x), s(y)) -> -#(x, y), -#(s(x), s(y)) -> -#(x, y))
    (f#(x, s(y), z) -> *#(x, x), *#(x, s(y)) -> *#(x, y))
    (f#(x, s(y), z) -> half#(s(y)), half#(s(s(x))) -> half#(x))
    (f#(x, s(y), z) -> odd#(s(y)), odd#(s(s(x))) -> odd#(x))
    (f#(x, s(y), z) -> f#(x, y, *(x, z)), f#(x, s(y), z) -> *#(x, x))
    (f#(x, s(y), z) -> f#(x, y, *(x, z)), f#(x, s(y), z) -> *#(x, z))
    (f#(x, s(y), z) -> f#(x, y, *(x, z)), f#(x, s(y), z) -> if#(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)))
    (f#(x, s(y), z) -> f#(x, y, *(x, z)), f#(x, s(y), z) -> odd#(s(y)))
    (f#(x, s(y), z) -> f#(x, y, *(x, z)), f#(x, s(y), z) -> half#(s(y)))
    (f#(x, s(y), z) -> f#(x, y, *(x, z)), f#(x, s(y), z) -> f#(x, y, *(x, z)))
    (f#(x, s(y), z) -> f#(x, y, *(x, z)), f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z))
    (*#(x, s(y)) -> *#(x, y), *#(x, s(y)) -> *#(x, y))
    (f#(x, s(y), z) -> *#(x, z), *#(x, s(y)) -> *#(x, y))
    (half#(s(s(x))) -> half#(x), half#(s(s(x))) -> half#(x))
    (f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z), f#(x, s(y), z) -> *#(x, x))
    (f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z), f#(x, s(y), z) -> *#(x, z))
    (f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z), f#(x, s(y), z) -> if#(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)))
    (f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z), f#(x, s(y), z) -> odd#(s(y)))
    (f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z), f#(x, s(y), z) -> half#(s(y)))
    (f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z), f#(x, s(y), z) -> f#(x, y, *(x, z)))
    (f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z), f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z))}
   SCCS:
    Scc:
     {f#(x, s(y), z) -> f#(x, y, *(x, z)),
      f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z)}
    Scc:
     {half#(s(s(x))) -> half#(x)}
    Scc:
     {odd#(s(s(x))) -> odd#(x)}
    Scc:
     {*#(x, s(y)) -> *#(x, y)}
    Scc:
     {-#(s(x), s(y)) -> -#(x, y)}
    SCC:
     Strict:
      {f#(x, s(y), z) -> f#(x, y, *(x, z)),
       f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z)}
     Weak:
     {        -(x, 0()) -> x,
          -(s(x), s(y)) -> -(x, y),
              *(x, 0()) -> 0(),
             *(x, s(y)) -> +(*(x, y), x),
       if(true(), x, y) -> x,
       if(true(), x, y) -> true(),
      if(false(), x, y) -> y,
      if(false(), x, y) -> false(),
               odd(0()) -> false(),
            odd(s(0())) -> true(),
           odd(s(s(x))) -> odd(x),
              half(0()) -> 0(),
           half(s(0())) -> 0(),
          half(s(s(x))) -> s(half(x)),
           f(x, 0(), z) -> z,
          f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)),
              pow(x, y) -> f(x, y, s(0()))}
     POLY:
      Argument Filtering:
       pi(pow) = [], pi(f#) = [1], pi(f) = [], pi(half) = 0, pi(odd) = [], pi(false) = [], pi(true) = [], pi(if) = [], pi(+) = [], pi(*) = [], pi(s) = [0], pi(0) = [], pi(-) = []
      Usable Rules:
       {}
      Interpretation:
       [f#](x0) = x0 + 1,
       [s](x0) = x0 + 1
      Strict:
       {f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z)}
      Weak:
       {        -(x, 0()) -> x,
            -(s(x), s(y)) -> -(x, y),
                *(x, 0()) -> 0(),
               *(x, s(y)) -> +(*(x, y), x),
         if(true(), x, y) -> x,
         if(true(), x, y) -> true(),
        if(false(), x, y) -> y,
        if(false(), x, y) -> false(),
                 odd(0()) -> false(),
              odd(s(0())) -> true(),
             odd(s(s(x))) -> odd(x),
                half(0()) -> 0(),
             half(s(0())) -> 0(),
            half(s(s(x))) -> s(half(x)),
             f(x, 0(), z) -> z,
            f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)),
                pow(x, y) -> f(x, y, s(0()))}
      EDG:
       {(f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z), f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z))}
       SCCS:
        Scc:
         {f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z)}
        SCC:
         Strict:
          {f#(x, s(y), z) -> f#(*(x, x), half(s(y)), z)}
         Weak:
         {        -(x, 0()) -> x,
              -(s(x), s(y)) -> -(x, y),
                  *(x, 0()) -> 0(),
                 *(x, s(y)) -> +(*(x, y), x),
           if(true(), x, y) -> x,
           if(true(), x, y) -> true(),
          if(false(), x, y) -> y,
          if(false(), x, y) -> false(),
                   odd(0()) -> false(),
                odd(s(0())) -> true(),
               odd(s(s(x))) -> odd(x),
                  half(0()) -> 0(),
               half(s(0())) -> 0(),
              half(s(s(x))) -> s(half(x)),
               f(x, 0(), z) -> z,
              f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)),
                  pow(x, y) -> f(x, y, s(0()))}
         Fail
    SCC:
     Strict:
      {half#(s(s(x))) -> half#(x)}
     Weak:
     {        -(x, 0()) -> x,
          -(s(x), s(y)) -> -(x, y),
              *(x, 0()) -> 0(),
             *(x, s(y)) -> +(*(x, y), x),
       if(true(), x, y) -> x,
       if(true(), x, y) -> true(),
      if(false(), x, y) -> y,
      if(false(), x, y) -> false(),
               odd(0()) -> false(),
            odd(s(0())) -> true(),
           odd(s(s(x))) -> odd(x),
              half(0()) -> 0(),
           half(s(0())) -> 0(),
          half(s(s(x))) -> s(half(x)),
           f(x, 0(), z) -> z,
          f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)),
              pow(x, y) -> f(x, y, s(0()))}
     SPSC:
      Simple Projection:
       pi(half#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {odd#(s(s(x))) -> odd#(x)}
     Weak:
     {        -(x, 0()) -> x,
          -(s(x), s(y)) -> -(x, y),
              *(x, 0()) -> 0(),
             *(x, s(y)) -> +(*(x, y), x),
       if(true(), x, y) -> x,
       if(true(), x, y) -> true(),
      if(false(), x, y) -> y,
      if(false(), x, y) -> false(),
               odd(0()) -> false(),
            odd(s(0())) -> true(),
           odd(s(s(x))) -> odd(x),
              half(0()) -> 0(),
           half(s(0())) -> 0(),
          half(s(s(x))) -> s(half(x)),
           f(x, 0(), z) -> z,
          f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)),
              pow(x, y) -> f(x, y, s(0()))}
     SPSC:
      Simple Projection:
       pi(odd#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {*#(x, s(y)) -> *#(x, y)}
     Weak:
     {        -(x, 0()) -> x,
          -(s(x), s(y)) -> -(x, y),
              *(x, 0()) -> 0(),
             *(x, s(y)) -> +(*(x, y), x),
       if(true(), x, y) -> x,
       if(true(), x, y) -> true(),
      if(false(), x, y) -> y,
      if(false(), x, y) -> false(),
               odd(0()) -> false(),
            odd(s(0())) -> true(),
           odd(s(s(x))) -> odd(x),
              half(0()) -> 0(),
           half(s(0())) -> 0(),
          half(s(s(x))) -> s(half(x)),
           f(x, 0(), z) -> z,
          f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)),
              pow(x, y) -> f(x, y, s(0()))}
     SPSC:
      Simple Projection:
       pi(*#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {-#(s(x), s(y)) -> -#(x, y)}
     Weak:
     {        -(x, 0()) -> x,
          -(s(x), s(y)) -> -(x, y),
              *(x, 0()) -> 0(),
             *(x, s(y)) -> +(*(x, y), x),
       if(true(), x, y) -> x,
       if(true(), x, y) -> true(),
      if(false(), x, y) -> y,
      if(false(), x, y) -> false(),
               odd(0()) -> false(),
            odd(s(0())) -> true(),
           odd(s(s(x))) -> odd(x),
              half(0()) -> 0(),
           half(s(0())) -> 0(),
          half(s(s(x))) -> s(half(x)),
           f(x, 0(), z) -> z,
          f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)),
              pow(x, y) -> f(x, y, s(0()))}
     SPSC:
      Simple Projection:
       pi(-#) = 0
      Strict:
       {}
      Qed