MAYBE
Time: 0.007714
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,
       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),
         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,
        double s x -> s s double x,
        double 0() -> 0()}
  EDG:
   {(plus#(n, s m) -> plus#(n, m), plus#(n, s m) -> plus#(n, m))
    (f#(true(), x, y) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
    (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)
    (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))
    (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))
    (double# s x -> double# x, double# s x -> double# x)}
   EDG:
    {(plus#(n, s m) -> plus#(n, m), plus#(n, s m) -> plus#(n, m))
     (f#(true(), x, y) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
     (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)
     (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))
     (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))
     (double# s x -> double# x, double# s x -> double# x)}
    EDG:
     {(plus#(n, s m) -> plus#(n, m), plus#(n, s m) -> plus#(n, m))
      (f#(true(), x, y) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
      (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)
      (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))
      (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))
      (double# s x -> double# x, double# s x -> double# x)}
     STATUS:
      arrows: 0.839506
      SCCS (4):
       Scc:
        {f#(true(), x, y) -> f#(and(gt(x, y), gt(y, s s 0())), plus(s 0(), x), double y)}
       Scc:
        {gt#(s u, s v) -> gt#(u, v)}
       Scc:
        {plus#(n, s m) -> plus#(n, m)}
       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,
              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,
              double s x -> s s double x,
              double 0() -> 0()}
        Open
       SCC (1):
        Strict:
         {plus#(n, s m) -> plus#(n, m)}
        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,
              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,
              double s x -> s s double x,
              double 0() -> 0()}
        Open