MAYBE
Time: 0.007606
TRS:
 {    f(true(), x, y) -> f(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y),
       and(x, true()) -> x,
      and(x, false()) -> false(),
         gt(s u, s v) -> gt(u, v),
         gt(s u, 0()) -> true(),
           gt(0(), v) -> false(),
         plus(n, s m) -> s plus(n, m),
         plus(n, 0()) -> n,
  plus(plus(n, m), u) -> plus(n, plus(m, u)),
           double s x -> s s double x,
           double 0() -> 0()}
 DP:
  DP:
   {    f#(true(), x, y) -> f#(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y),
        f#(true(), x, y) -> and#(gt(x, y), gt(y, s s 0())),
        f#(true(), x, y) -> gt#(x, y),
        f#(true(), x, y) -> gt#(y, s s 0()),
        f#(true(), x, y) -> plus#(s 0(), x),
        f#(true(), x, y) -> double# y,
           gt#(s u, s v) -> gt#(u, v),
           plus#(n, s m) -> plus#(n, m),
    plus#(plus(n, m), u) -> plus#(n, plus(m, u)),
    plus#(plus(n, m), u) -> plus#(m, u),
             double# s x -> double# x}
  TRS:
  {    f(true(), x, y) -> f(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y),
        and(x, true()) -> x,
       and(x, false()) -> false(),
          gt(s u, s v) -> gt(u, v),
          gt(s u, 0()) -> true(),
            gt(0(), v) -> false(),
          plus(n, s m) -> s plus(n, m),
          plus(n, 0()) -> n,
   plus(plus(n, m), u) -> plus(n, plus(m, u)),
            double s x -> s s double x,
            double 0() -> 0()}
  UR:
   {     and(x, true()) -> x,
        and(x, false()) -> false(),
           gt(s u, s v) -> gt(u, v),
           gt(s u, 0()) -> true(),
             gt(0(), v) -> false(),
           plus(n, s m) -> s plus(n, m),
           plus(n, 0()) -> n,
    plus(plus(n, m), u) -> plus(n, plus(m, u)),
             double s x -> s s double x,
             double 0() -> 0()}
   EDG:
    {(f#(true(), x, y) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
     (plus#(plus(n, m), u) -> plus#(n, plus(m, u)), plus#(n, s m) -> plus#(n, m))
     (plus#(plus(n, m), u) -> plus#(m, u), plus#(plus(n, m), u) -> plus#(m, u))
     (plus#(plus(n, m), u) -> plus#(m, u), plus#(plus(n, m), u) -> plus#(n, plus(m, u)))
     (plus#(plus(n, m), u) -> plus#(m, u), plus#(n, s m) -> plus#(n, m))
     (plus#(n, s m) -> plus#(n, m), plus#(plus(n, m), u) -> plus#(m, u))
     (plus#(n, s m) -> plus#(n, m), plus#(plus(n, m), u) -> plus#(n, plus(m, u)))
     (plus#(n, s m) -> plus#(n, m), plus#(n, s m) -> plus#(n, m))
     (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))
     (f#(true(), x, y) -> f#(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y), f#(true(), x, y) -> f#(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y))
     (f#(true(), x, y) -> f#(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y), f#(true(), x, y) -> and#(gt(x, y), gt(y, s s 0())))
     (f#(true(), x, y) -> f#(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y), f#(true(), x, y) -> gt#(x, y))
     (f#(true(), x, y) -> f#(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y), f#(true(), x, y) -> gt#(y, s s 0()))
     (f#(true(), x, y) -> f#(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y), f#(true(), x, y) -> plus#(s 0(), x))
     (f#(true(), x, y) -> f#(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y), f#(true(), x, y) -> double# y)
     (f#(true(), x, y) -> plus#(s 0(), x), plus#(n, s m) -> plus#(n, m))
     (f#(true(), x, y) -> gt#(y, s s 0()), gt#(s u, s v) -> gt#(u, v))
     (f#(true(), x, y) -> double# y, double# s x -> double# x)
     (double# s x -> double# x, double# s x -> double# x)}
    STATUS:
     arrows: 0.842975
     SCCS (4):
      Scc:
       {f#(true(), x, y) -> f#(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y)}
      Scc:
       {       plus#(n, s m) -> plus#(n, m),
        plus#(plus(n, m), u) -> plus#(n, plus(m, u)),
        plus#(plus(n, m), u) -> plus#(m, u)}
      Scc:
       {gt#(s u, s v) -> gt#(u, v)}
      Scc:
       {double# s x -> double# x}
      
      SCC (1):
       Strict:
        {f#(true(), x, y) -> f#(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y)}
       Weak:
       {    f(true(), x, y) -> f(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y),
             and(x, true()) -> x,
            and(x, false()) -> false(),
               gt(s u, s v) -> gt(u, v),
               gt(s u, 0()) -> true(),
                 gt(0(), v) -> false(),
               plus(n, s m) -> s plus(n, m),
               plus(n, 0()) -> n,
        plus(plus(n, m), u) -> plus(n, plus(m, u)),
                 double s x -> s s double x,
                 double 0() -> 0()}
       Open
      
      
      
      SCC (3):
       Strict:
        {       plus#(n, s m) -> plus#(n, m),
         plus#(plus(n, m), u) -> plus#(n, plus(m, u)),
         plus#(plus(n, m), u) -> plus#(m, u)}
       Weak:
       {    f(true(), x, y) -> f(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y),
             and(x, true()) -> x,
            and(x, false()) -> false(),
               gt(s u, s v) -> gt(u, v),
               gt(s u, 0()) -> true(),
                 gt(0(), v) -> false(),
               plus(n, s m) -> s plus(n, m),
               plus(n, 0()) -> n,
        plus(plus(n, m), u) -> plus(n, plus(m, u)),
                 double s x -> s s double x,
                 double 0() -> 0()}
       Open
      
      
      SCC (1):
       Strict:
        {gt#(s u, s v) -> gt#(u, v)}
       Weak:
       {    f(true(), x, y) -> f(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y),
             and(x, true()) -> x,
            and(x, false()) -> false(),
               gt(s u, s v) -> gt(u, v),
               gt(s u, 0()) -> true(),
                 gt(0(), v) -> false(),
               plus(n, s m) -> s plus(n, m),
               plus(n, 0()) -> n,
        plus(plus(n, m), u) -> plus(n, plus(m, u)),
                 double s x -> s s double x,
                 double 0() -> 0()}
       Open
      SCC (1):
       Strict:
        {double# s x -> double# x}
       Weak:
       {    f(true(), x, y) -> f(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y),
             and(x, true()) -> x,
            and(x, false()) -> false(),
               gt(s u, s v) -> gt(u, v),
               gt(s u, 0()) -> true(),
                 gt(0(), v) -> false(),
               plus(n, s m) -> s plus(n, m),
               plus(n, 0()) -> n,
        plus(plus(n, m), u) -> plus(n, plus(m, u)),
                 double s x -> s s double x,
                 double 0() -> 0()}
       Open