MAYBE
Time: 0.012888
TRS:
 {                 lt(x, 0()) -> false(),
                 lt(0(), s x) -> true(),
                 lt(s x, s y) -> lt(x, y),
                      fib 0() -> s 0(),
                    fib s 0() -> s 0(),
                    fib s s x -> if(true(), 0(), s s x, 0(), 0()),
                     fibo 0() -> fib 0(),
                   fibo s 0() -> fib s 0(),
                   fibo s s x -> sum(fibo s x, fibo x),
                  sum(x, 0()) -> x,
                  sum(x, s y) -> s sum(x, y),
   if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c),
  if(false(), c, s s x, a, b) -> sum(fibo a, fibo b)}
 DP:
  DP:
   {               lt#(s x, s y) -> lt#(x, y),
                      fib# s s x -> if#(true(), 0(), s s x, 0(), 0()),
                       fibo# 0() -> fib# 0(),
                     fibo# s 0() -> fib# s 0(),
                     fibo# s s x -> fibo# x,
                     fibo# s s x -> fibo# s x,
                     fibo# s s x -> sum#(fibo s x, fibo x),
                    sum#(x, s y) -> sum#(x, y),
     if#(true(), c, s s x, a, b) -> lt#(s c, s s x),
     if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c),
    if#(false(), c, s s x, a, b) -> fibo# b,
    if#(false(), c, s s x, a, b) -> fibo# a,
    if#(false(), c, s s x, a, b) -> sum#(fibo a, fibo b)}
  TRS:
  {                 lt(x, 0()) -> false(),
                  lt(0(), s x) -> true(),
                  lt(s x, s y) -> lt(x, y),
                       fib 0() -> s 0(),
                     fib s 0() -> s 0(),
                     fib s s x -> if(true(), 0(), s s x, 0(), 0()),
                      fibo 0() -> fib 0(),
                    fibo s 0() -> fib s 0(),
                    fibo s s x -> sum(fibo s x, fibo x),
                   sum(x, 0()) -> x,
                   sum(x, s y) -> s sum(x, y),
    if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c),
   if(false(), c, s s x, a, b) -> sum(fibo a, fibo b)}
  UR:
   {  lt(x, 0()) -> false(),
    lt(0(), s x) -> true(),
    lt(s x, s y) -> lt(x, y),
         fib 0() -> s 0(),
       fib s 0() -> s 0(),
        fibo 0() -> fib 0(),
      fibo s 0() -> fib s 0(),
      fibo s s x -> sum(fibo s x, fibo x),
     sum(x, 0()) -> x,
     sum(x, s y) -> s sum(x, y),
         a(z, w) -> z,
         a(z, w) -> w}
   EDG:
    {(sum#(x, s y) -> sum#(x, y), sum#(x, s y) -> sum#(x, y))
     (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> sum#(fibo a, fibo b))
     (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> fibo# a)
     (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(false(), c, s s x, a, b) -> fibo# b)
     (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c))
     (if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c), if#(true(), c, s s x, a, b) -> lt#(s c, s s x))
     (fibo# s s x -> sum#(fibo s x, fibo x), sum#(x, s y) -> sum#(x, y))
     (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> sum#(fibo s x, fibo x))
     (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> fibo# s x)
     (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s s x -> fibo# x)
     (if#(false(), c, s s x, a, b) -> fibo# b, fibo# s 0() -> fib# s 0())
     (if#(false(), c, s s x, a, b) -> fibo# b, fibo# 0() -> fib# 0())
     (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> sum#(fibo s x, fibo x))
     (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> fibo# s x)
     (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s s x -> fibo# x)
     (if#(false(), c, s s x, a, b) -> fibo# a, fibo# s 0() -> fib# s 0())
     (if#(false(), c, s s x, a, b) -> fibo# a, fibo# 0() -> fib# 0())
     (fibo# s s x -> fibo# s x, fibo# s 0() -> fib# s 0())
     (fibo# s s x -> fibo# s x, fibo# s s x -> fibo# x)
     (fibo# s s x -> fibo# s x, fibo# s s x -> fibo# s x)
     (fibo# s s x -> fibo# s x, fibo# s s x -> sum#(fibo s x, fibo x))
     (fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), if#(true(), c, s s x, a, b) -> lt#(s c, s s x))
     (fib# s s x -> if#(true(), 0(), s s x, 0(), 0()), if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c))
     (if#(false(), c, s s x, a, b) -> sum#(fibo a, fibo b), sum#(x, s y) -> sum#(x, y))
     (fibo# s s x -> fibo# x, fibo# 0() -> fib# 0())
     (fibo# s s x -> fibo# x, fibo# s 0() -> fib# s 0())
     (fibo# s s x -> fibo# x, fibo# s s x -> fibo# x)
     (fibo# s s x -> fibo# x, fibo# s s x -> fibo# s x)
     (fibo# s s x -> fibo# x, fibo# s s x -> sum#(fibo s x, fibo x))
     (if#(true(), c, s s x, a, b) -> lt#(s c, s s x), lt#(s x, s y) -> lt#(x, y))
     (lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))}
    STATUS:
     arrows: 0.816568
     SCCS (4):
      Scc:
       {if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c)}
      Scc:
       {fibo# s s x -> fibo# x,
        fibo# s s x -> fibo# s x}
      Scc:
       {sum#(x, s y) -> sum#(x, y)}
      Scc:
       {lt#(s x, s y) -> lt#(x, y)}
      
      
      SCC (1):
       Strict:
        {if#(true(), c, s s x, a, b) -> if#(lt(s c, s s x), s c, s s x, b, c)}
       Weak:
       {                 lt(x, 0()) -> false(),
                       lt(0(), s x) -> true(),
                       lt(s x, s y) -> lt(x, y),
                            fib 0() -> s 0(),
                          fib s 0() -> s 0(),
                          fib s s x -> if(true(), 0(), s s x, 0(), 0()),
                           fibo 0() -> fib 0(),
                         fibo s 0() -> fib s 0(),
                         fibo s s x -> sum(fibo s x, fibo x),
                        sum(x, 0()) -> x,
                        sum(x, s y) -> s sum(x, y),
         if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c),
        if(false(), c, s s x, a, b) -> sum(fibo a, fibo b)}
       Open
      
      
      
      SCC (2):
       Strict:
        {fibo# s s x -> fibo# x,
         fibo# s s x -> fibo# s x}
       Weak:
       {                 lt(x, 0()) -> false(),
                       lt(0(), s x) -> true(),
                       lt(s x, s y) -> lt(x, y),
                            fib 0() -> s 0(),
                          fib s 0() -> s 0(),
                          fib s s x -> if(true(), 0(), s s x, 0(), 0()),
                           fibo 0() -> fib 0(),
                         fibo s 0() -> fib s 0(),
                         fibo s s x -> sum(fibo s x, fibo x),
                        sum(x, 0()) -> x,
                        sum(x, s y) -> s sum(x, y),
         if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c),
        if(false(), c, s s x, a, b) -> sum(fibo a, fibo b)}
       Open
      
      
      
      
      SCC (1):
       Strict:
        {sum#(x, s y) -> sum#(x, y)}
       Weak:
       {                 lt(x, 0()) -> false(),
                       lt(0(), s x) -> true(),
                       lt(s x, s y) -> lt(x, y),
                            fib 0() -> s 0(),
                          fib s 0() -> s 0(),
                          fib s s x -> if(true(), 0(), s s x, 0(), 0()),
                           fibo 0() -> fib 0(),
                         fibo s 0() -> fib s 0(),
                         fibo s s x -> sum(fibo s x, fibo x),
                        sum(x, 0()) -> x,
                        sum(x, s y) -> s sum(x, y),
         if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c),
        if(false(), c, s s x, a, b) -> sum(fibo a, fibo b)}
       Open
      SCC (1):
       Strict:
        {lt#(s x, s y) -> lt#(x, y)}
       Weak:
       {                 lt(x, 0()) -> false(),
                       lt(0(), s x) -> true(),
                       lt(s x, s y) -> lt(x, y),
                            fib 0() -> s 0(),
                          fib s 0() -> s 0(),
                          fib s s x -> if(true(), 0(), s s x, 0(), 0()),
                           fibo 0() -> fib 0(),
                         fibo s 0() -> fib s 0(),
                         fibo s s x -> sum(fibo s x, fibo x),
                        sum(x, 0()) -> x,
                        sum(x, s y) -> s sum(x, y),
         if(true(), c, s s x, a, b) -> if(lt(s c, s s x), s c, s s x, b, c),
        if(false(), c, s s x, a, b) -> sum(fibo a, fibo b)}
       Open