MAYBE
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:
  Strict:
   {               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))}
  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))}
  EDG:
   {(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) -> sum#(fibo(a), fibo(b)), sum#(x, s(y)) -> sum#(x, y))
    (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()))
    (sum#(x, s(y)) -> sum#(x, y), sum#(x, s(y)) -> sum#(x, y))
    (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)))
    (lt#(s(x), s(y)) -> lt#(x, y), lt#(s(x), s(y)) -> lt#(x, y))
    (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) -> fibo#(b), fibo#(0()) -> fib#(0()))
    (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#(s(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))) -> sum#(fibo(s(x)), fibo(x)))
    (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))))
    (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#(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#(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) -> sum#(fibo(a), fibo(b)))
    (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))}
   SCCS:
    Scc:
     {if#(true(), c, s(s(x)), a, b) -> if#(lt(s(c), s(s(x))), s(c), s(s(x)), b, c)}
    Scc:
     {sum#(x, s(y)) -> sum#(x, y)}
    Scc:
     {fibo#(s(s(x))) -> fibo#(x),
      fibo#(s(s(x))) -> fibo#(s(x))}
    Scc:
     {lt#(s(x), s(y)) -> lt#(x, y)}
    SCC:
     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))}
     Fail
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(sum#) = 1
      Strict:
       {}
      Qed
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(fibo#) = 0
      Strict:
       {fibo#(s(s(x))) -> fibo#(s(x))}
      EDG:
       {(fibo#(s(s(x))) -> fibo#(s(x)), fibo#(s(s(x))) -> fibo#(s(x)))}
       SCCS:
        Scc:
         {fibo#(s(s(x))) -> fibo#(s(x))}
        SCC:
         Strict:
          {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))}
         SPSC:
          Simple Projection:
           pi(fibo#) = 0
          Strict:
           {}
          Qed
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(lt#) = 0
      Strict:
       {}
      Qed