MAYBE
Time: 0.006606
TRS:
 {       f 0() -> 0(),
       f s 0() -> s 0(),
       f s s x -> p h g x,
       f s s x -> +(p g x, q g x),
  p pair(x, y) -> x,
           h x -> pair(+(p x, q x), p x),
         g 0() -> pair(s 0(), s 0()),
         g s x -> h g x,
         g s x -> pair(+(p g x, q g x), p g x),
     +(x, 0()) -> x,
     +(x, s y) -> s +(x, y),
  q pair(x, y) -> y}
 DP:
  DP:
   {  f# s s x -> p# h g x,
      f# s s x -> p# g x,
      f# s s x -> h# g x,
      f# s s x -> g# x,
      f# s s x -> +#(p g x, q g x),
      f# s s x -> q# g x,
          h# x -> p# x,
          h# x -> +#(p x, q x),
          h# x -> q# x,
        g# s x -> p# g x,
        g# s x -> h# g x,
        g# s x -> g# x,
        g# s x -> +#(p g x, q g x),
        g# s x -> q# g x,
    +#(x, s y) -> +#(x, y)}
  TRS:
  {       f 0() -> 0(),
        f s 0() -> s 0(),
        f s s x -> p h g x,
        f s s x -> +(p g x, q g x),
   p pair(x, y) -> x,
            h x -> pair(+(p x, q x), p x),
          g 0() -> pair(s 0(), s 0()),
          g s x -> h g x,
          g s x -> pair(+(p g x, q g x), p g x),
      +(x, 0()) -> x,
      +(x, s y) -> s +(x, y),
   q pair(x, y) -> y}
  UR:
   {p pair(x, y) -> x,
             h x -> pair(+(p x, q x), p x),
           g 0() -> pair(s 0(), s 0()),
           g s x -> h g x,
           g s x -> pair(+(p g x, q g x), p g x),
       +(x, 0()) -> x,
       +(x, s y) -> s +(x, y),
    q pair(x, y) -> y,
         a(z, w) -> z,
         a(z, w) -> w}
   EDG:
    {(g# s x -> +#(p g x, q g x), +#(x, s y) -> +#(x, y))
     (f# s s x -> h# g x, h# x -> q# x)
     (f# s s x -> h# g x, h# x -> +#(p x, q x))
     (f# s s x -> h# g x, h# x -> p# x)
     (g# s x -> g# x, g# s x -> q# g x)
     (g# s x -> g# x, g# s x -> +#(p g x, q g x))
     (g# s x -> g# x, g# s x -> g# x)
     (g# s x -> g# x, g# s x -> h# g x)
     (g# s x -> g# x, g# s x -> p# g x)
     (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (f# s s x -> g# x, g# s x -> p# g x)
     (f# s s x -> g# x, g# s x -> h# g x)
     (f# s s x -> g# x, g# s x -> g# x)
     (f# s s x -> g# x, g# s x -> +#(p g x, q g x))
     (f# s s x -> g# x, g# s x -> q# g x)
     (g# s x -> h# g x, h# x -> p# x)
     (g# s x -> h# g x, h# x -> +#(p x, q x))
     (g# s x -> h# g x, h# x -> q# x)
     (h# x -> +#(p x, q x), +#(x, s y) -> +#(x, y))
     (f# s s x -> +#(p g x, q g x), +#(x, s y) -> +#(x, y))}
    EDG:
     {(g# s x -> +#(p g x, q g x), +#(x, s y) -> +#(x, y))
      (f# s s x -> h# g x, h# x -> q# x)
      (f# s s x -> h# g x, h# x -> +#(p x, q x))
      (f# s s x -> h# g x, h# x -> p# x)
      (g# s x -> g# x, g# s x -> q# g x)
      (g# s x -> g# x, g# s x -> +#(p g x, q g x))
      (g# s x -> g# x, g# s x -> g# x)
      (g# s x -> g# x, g# s x -> h# g x)
      (g# s x -> g# x, g# s x -> p# g x)
      (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
      (f# s s x -> g# x, g# s x -> p# g x)
      (f# s s x -> g# x, g# s x -> h# g x)
      (f# s s x -> g# x, g# s x -> g# x)
      (f# s s x -> g# x, g# s x -> +#(p g x, q g x))
      (f# s s x -> g# x, g# s x -> q# g x)
      (g# s x -> h# g x, h# x -> p# x)
      (g# s x -> h# g x, h# x -> +#(p x, q x))
      (g# s x -> h# g x, h# x -> q# x)
      (h# x -> +#(p x, q x), +#(x, s y) -> +#(x, y))
      (f# s s x -> +#(p g x, q g x), +#(x, s y) -> +#(x, y))}
     EDG:
      {(g# s x -> +#(p g x, q g x), +#(x, s y) -> +#(x, y))
       (f# s s x -> h# g x, h# x -> q# x)
       (f# s s x -> h# g x, h# x -> +#(p x, q x))
       (f# s s x -> h# g x, h# x -> p# x)
       (g# s x -> g# x, g# s x -> q# g x)
       (g# s x -> g# x, g# s x -> +#(p g x, q g x))
       (g# s x -> g# x, g# s x -> g# x)
       (g# s x -> g# x, g# s x -> h# g x)
       (g# s x -> g# x, g# s x -> p# g x)
       (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
       (f# s s x -> g# x, g# s x -> p# g x)
       (f# s s x -> g# x, g# s x -> h# g x)
       (f# s s x -> g# x, g# s x -> g# x)
       (f# s s x -> g# x, g# s x -> +#(p g x, q g x))
       (f# s s x -> g# x, g# s x -> q# g x)
       (g# s x -> h# g x, h# x -> p# x)
       (g# s x -> h# g x, h# x -> +#(p x, q x))
       (g# s x -> h# g x, h# x -> q# x)
       (h# x -> +#(p x, q x), +#(x, s y) -> +#(x, y))
       (f# s s x -> +#(p g x, q g x), +#(x, s y) -> +#(x, y))}
      EDG:
       {(g# s x -> +#(p g x, q g x), +#(x, s y) -> +#(x, y))
        (f# s s x -> h# g x, h# x -> q# x)
        (f# s s x -> h# g x, h# x -> +#(p x, q x))
        (f# s s x -> h# g x, h# x -> p# x)
        (g# s x -> g# x, g# s x -> q# g x)
        (g# s x -> g# x, g# s x -> +#(p g x, q g x))
        (g# s x -> g# x, g# s x -> g# x)
        (g# s x -> g# x, g# s x -> h# g x)
        (g# s x -> g# x, g# s x -> p# g x)
        (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
        (f# s s x -> g# x, g# s x -> p# g x)
        (f# s s x -> g# x, g# s x -> h# g x)
        (f# s s x -> g# x, g# s x -> g# x)
        (f# s s x -> g# x, g# s x -> +#(p g x, q g x))
        (f# s s x -> g# x, g# s x -> q# g x)
        (g# s x -> h# g x, h# x -> p# x)
        (g# s x -> h# g x, h# x -> +#(p x, q x))
        (g# s x -> h# g x, h# x -> q# x)
        (h# x -> +#(p x, q x), +#(x, s y) -> +#(x, y))
        (f# s s x -> +#(p g x, q g x), +#(x, s y) -> +#(x, y))}
       STATUS:
        arrows: 0.911111
        SCCS (2):
         Scc:
          {g# s x -> g# x}
         Scc:
          {+#(x, s y) -> +#(x, y)}
         
         
         SCC (1):
          Strict:
           {g# s x -> g# x}
          Weak:
          {       f 0() -> 0(),
                f s 0() -> s 0(),
                f s s x -> p h g x,
                f s s x -> +(p g x, q g x),
           p pair(x, y) -> x,
                    h x -> pair(+(p x, q x), p x),
                  g 0() -> pair(s 0(), s 0()),
                  g s x -> h g x,
                  g s x -> pair(+(p g x, q g x), p g x),
              +(x, 0()) -> x,
              +(x, s y) -> s +(x, y),
           q pair(x, y) -> y}
          Open
         
         
         
         
         
         
         
         
         
         
         
         
         SCC (1):
          Strict:
           {+#(x, s y) -> +#(x, y)}
          Weak:
          {       f 0() -> 0(),
                f s 0() -> s 0(),
                f s s x -> p h g x,
                f s s x -> +(p g x, q g x),
           p pair(x, y) -> x,
                    h x -> pair(+(p x, q x), p x),
                  g 0() -> pair(s 0(), s 0()),
                  g s x -> h g x,
                  g s x -> pair(+(p g x, q g x), p g x),
              +(x, 0()) -> x,
              +(x, s y) -> s +(x, y),
           q pair(x, y) -> y}
          Open