MAYBE
Time: 0.057786
TRS:
 {cond(true(), x) -> cond(odd x, p p p x),
          odd 0() -> false(),
        odd s 0() -> true(),
        odd s s x -> odd x,
            p 0() -> 0(),
            p s x -> x}
 DP:
  DP:
   {cond#(true(), x) -> cond#(odd x, p p p x),
    cond#(true(), x) -> odd# x,
    cond#(true(), x) -> p# x,
    cond#(true(), x) -> p# p x,
    cond#(true(), x) -> p# p p x,
          odd# s s x -> odd# x}
  TRS:
  {cond(true(), x) -> cond(odd x, p p p x),
           odd 0() -> false(),
         odd s 0() -> true(),
         odd s s x -> odd x,
             p 0() -> 0(),
             p s x -> x}
  UR:
   {  odd 0() -> false(),
    odd s 0() -> true(),
    odd s s x -> odd x,
        p 0() -> 0(),
        p s x -> x,
      a(y, z) -> y,
      a(y, z) -> z}
   EDG:
    {(cond#(true(), x) -> cond#(odd x, p p p x), cond#(true(), x) -> p# p p x)
     (cond#(true(), x) -> cond#(odd x, p p p x), cond#(true(), x) -> p# p x)
     (cond#(true(), x) -> cond#(odd x, p p p x), cond#(true(), x) -> p# x)
     (cond#(true(), x) -> cond#(odd x, p p p x), cond#(true(), x) -> odd# x)
     (cond#(true(), x) -> cond#(odd x, p p p x), cond#(true(), x) -> cond#(odd x, p p p x))
     (odd# s s x -> odd# x, odd# s s x -> odd# x)
     (cond#(true(), x) -> odd# x, odd# s s x -> odd# x)}
    STATUS:
     arrows: 0.805556
     SCCS (2):
      Scc:
       {cond#(true(), x) -> cond#(odd x, p p p x)}
      Scc:
       {odd# s s x -> odd# x}
      
      SCC (1):
       Strict:
        {cond#(true(), x) -> cond#(odd x, p p p x)}
       Weak:
       {cond(true(), x) -> cond(odd x, p p p x),
                odd 0() -> false(),
              odd s 0() -> true(),
              odd s s x -> odd x,
                  p 0() -> 0(),
                  p s x -> x}
       Fail
      
      
      
      SCC (1):
       Strict:
        {odd# s s x -> odd# x}
       Weak:
       {cond(true(), x) -> cond(odd x, p p p x),
                odd 0() -> false(),
              odd s 0() -> true(),
              odd s s x -> odd x,
                  p 0() -> 0(),
                  p s x -> x}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [cond](x0, x1) = x0 + x1 + 1,
         
         [odd](x0) = x0 + 1,
         
         [p](x0) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [true] = 0,
         
         [false] = 0,
         
         [0] = 1,
         
         [odd#](x0) = x0
        Strict:
         odd# s s x -> odd# x
         2 + 1x >= 0 + 1x
        Weak:
         p s x -> x
         2 + 1x >= 1x
         p 0() -> 0()
         2 >= 1
         odd s s x -> odd x
         3 + 1x >= 1 + 1x
         odd s 0() -> true()
         3 >= 0
         odd 0() -> false()
         2 >= 0
         cond(true(), x) -> cond(odd x, p p p x)
         1 + 1x >= 5 + 2x
       Qed