MAYBE
Time: 0.002478
TRS:
 {      fib 0() -> 0(),
      fib s 0() -> s 0(),
      fib s s x -> sp g x,
    fib s s 0() -> s 0(),
  sp pair(x, y) -> +(x, y),
          g 0() -> pair(s 0(), 0()),
          g s x -> np g x,
        g s 0() -> pair(s 0(), s 0()),
  np pair(x, y) -> pair(+(x, y), x),
      +(x, 0()) -> x,
      +(x, s y) -> s +(x, y)}
 DP:
  DP:
   {    fib# s s x -> sp# g x,
        fib# s s x -> g# x,
    sp# pair(x, y) -> +#(x, y),
            g# s x -> g# x,
            g# s x -> np# g x,
    np# pair(x, y) -> +#(x, y),
        +#(x, s y) -> +#(x, y)}
  TRS:
  {      fib 0() -> 0(),
       fib s 0() -> s 0(),
       fib s s x -> sp g x,
     fib s s 0() -> s 0(),
   sp pair(x, y) -> +(x, y),
           g 0() -> pair(s 0(), 0()),
           g s x -> np g x,
         g s 0() -> pair(s 0(), s 0()),
   np pair(x, y) -> pair(+(x, y), x),
       +(x, 0()) -> x,
       +(x, s y) -> s +(x, y)}
  UR:
   {        g 0() -> pair(s 0(), 0()),
            g s x -> np g x,
          g s 0() -> pair(s 0(), s 0()),
    np pair(x, y) -> pair(+(x, y), x),
        +(x, 0()) -> x,
        +(x, s y) -> s +(x, y),
          a(z, w) -> z,
          a(z, w) -> w}
   EDG:
    {(g# s x -> g# x, g# s x -> np# g x)
     (g# s x -> g# x, g# s x -> g# x)
     (np# pair(x, y) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (fib# s s x -> sp# g x, sp# pair(x, y) -> +#(x, y))
     (g# s x -> np# g x, np# pair(x, y) -> +#(x, y))
     (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (sp# pair(x, y) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (fib# s s x -> g# x, g# s x -> g# x)
     (fib# s s x -> g# x, g# s x -> np# g x)}
    STATUS:
     arrows: 0.816327
     SCCS (2):
      Scc:
       {g# s x -> g# x}
      Scc:
       {+#(x, s y) -> +#(x, y)}
      
      
      
      
      SCC (1):
       Strict:
        {g# s x -> g# x}
       Weak:
       {      fib 0() -> 0(),
            fib s 0() -> s 0(),
            fib s s x -> sp g x,
          fib s s 0() -> s 0(),
        sp pair(x, y) -> +(x, y),
                g 0() -> pair(s 0(), 0()),
                g s x -> np g x,
              g s 0() -> pair(s 0(), s 0()),
        np pair(x, y) -> pair(+(x, y), x),
            +(x, 0()) -> x,
            +(x, s y) -> s +(x, y)}
       Open
      
      
      SCC (1):
       Strict:
        {+#(x, s y) -> +#(x, y)}
       Weak:
       {      fib 0() -> 0(),
            fib s 0() -> s 0(),
            fib s s x -> sp g x,
          fib s s 0() -> s 0(),
        sp pair(x, y) -> +(x, y),
                g 0() -> pair(s 0(), 0()),
                g s x -> np g x,
              g s 0() -> pair(s 0(), s 0()),
        np pair(x, y) -> pair(+(x, y), x),
            +(x, 0()) -> x,
            +(x, s y) -> s +(x, y)}
       Open