MAYBE
Time: 0.344253
TRS:
 {  a__g(X1, X2) -> g(X1, X2),
    a__g(a(), X) -> a__f(b(), X),
        mark b() -> b(),
        mark a() -> a__a(),
        mark h X -> a__h mark X,
  mark g(X1, X2) -> a__g(mark X1, X2),
  mark f(X1, X2) -> a__f(mark X1, X2),
          a__h X -> a__g(mark X, X),
          a__h X -> h X,
      a__f(X, X) -> a__h a__a(),
    a__f(X1, X2) -> f(X1, X2),
          a__a() -> b(),
          a__a() -> a()}
 DP:
  DP:
   {  a__g#(a(), X) -> a__f#(b(), X),
          mark# a() -> a__a#(),
          mark# h X -> mark# X,
          mark# h X -> a__h# mark X,
    mark# g(X1, X2) -> a__g#(mark X1, X2),
    mark# g(X1, X2) -> mark# X1,
    mark# f(X1, X2) -> mark# X1,
    mark# f(X1, X2) -> a__f#(mark X1, X2),
            a__h# X -> a__g#(mark X, X),
            a__h# X -> mark# X,
        a__f#(X, X) -> a__h# a__a(),
        a__f#(X, X) -> a__a#()}
  TRS:
  {  a__g(X1, X2) -> g(X1, X2),
     a__g(a(), X) -> a__f(b(), X),
         mark b() -> b(),
         mark a() -> a__a(),
         mark h X -> a__h mark X,
   mark g(X1, X2) -> a__g(mark X1, X2),
   mark f(X1, X2) -> a__f(mark X1, X2),
           a__h X -> a__g(mark X, X),
           a__h X -> h X,
       a__f(X, X) -> a__h a__a(),
     a__f(X1, X2) -> f(X1, X2),
           a__a() -> b(),
           a__a() -> a()}
  UR:
   {  a__g(X1, X2) -> g(X1, X2),
      a__g(a(), X) -> a__f(b(), X),
          mark b() -> b(),
          mark a() -> a__a(),
          mark h X -> a__h mark X,
    mark g(X1, X2) -> a__g(mark X1, X2),
    mark f(X1, X2) -> a__f(mark X1, X2),
            a__h X -> a__g(mark X, X),
            a__h X -> h X,
        a__f(X, X) -> a__h a__a(),
      a__f(X1, X2) -> f(X1, X2),
            a__a() -> b(),
            a__a() -> a()}
   EDG:
    {(mark# g(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2))
     (mark# g(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1)
     (mark# g(X1, X2) -> mark# X1, mark# g(X1, X2) -> mark# X1)
     (mark# g(X1, X2) -> mark# X1, mark# g(X1, X2) -> a__g#(mark X1, X2))
     (mark# g(X1, X2) -> mark# X1, mark# h X -> a__h# mark X)
     (mark# g(X1, X2) -> mark# X1, mark# h X -> mark# X)
     (mark# g(X1, X2) -> mark# X1, mark# a() -> a__a#())
     (mark# g(X1, X2) -> a__g#(mark X1, X2), a__g#(a(), X) -> a__f#(b(), X))
     (mark# h X -> mark# X, mark# f(X1, X2) -> a__f#(mark X1, X2))
     (mark# h X -> mark# X, mark# f(X1, X2) -> mark# X1)
     (mark# h X -> mark# X, mark# g(X1, X2) -> mark# X1)
     (mark# h X -> mark# X, mark# g(X1, X2) -> a__g#(mark X1, X2))
     (mark# h X -> mark# X, mark# h X -> a__h# mark X)
     (mark# h X -> mark# X, mark# h X -> mark# X)
     (mark# h X -> mark# X, mark# a() -> a__a#())
     (a__h# X -> a__g#(mark X, X), a__g#(a(), X) -> a__f#(b(), X))
     (a__f#(X, X) -> a__h# a__a(), a__h# X -> mark# X)
     (a__f#(X, X) -> a__h# a__a(), a__h# X -> a__g#(mark X, X))
     (mark# h X -> a__h# mark X, a__h# X -> a__g#(mark X, X))
     (mark# h X -> a__h# mark X, a__h# X -> mark# X)
     (a__h# X -> mark# X, mark# a() -> a__a#())
     (a__h# X -> mark# X, mark# h X -> mark# X)
     (a__h# X -> mark# X, mark# h X -> a__h# mark X)
     (a__h# X -> mark# X, mark# g(X1, X2) -> a__g#(mark X1, X2))
     (a__h# X -> mark# X, mark# g(X1, X2) -> mark# X1)
     (a__h# X -> mark# X, mark# f(X1, X2) -> mark# X1)
     (a__h# X -> mark# X, mark# f(X1, X2) -> a__f#(mark X1, X2))
     (mark# f(X1, X2) -> a__f#(mark X1, X2), a__f#(X, X) -> a__h# a__a())
     (mark# f(X1, X2) -> a__f#(mark X1, X2), a__f#(X, X) -> a__a#())
     (mark# f(X1, X2) -> mark# X1, mark# a() -> a__a#())
     (mark# f(X1, X2) -> mark# X1, mark# h X -> mark# X)
     (mark# f(X1, X2) -> mark# X1, mark# h X -> a__h# mark X)
     (mark# f(X1, X2) -> mark# X1, mark# g(X1, X2) -> a__g#(mark X1, X2))
     (mark# f(X1, X2) -> mark# X1, mark# g(X1, X2) -> mark# X1)
     (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1)
     (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2))
     (a__g#(a(), X) -> a__f#(b(), X), a__f#(X, X) -> a__h# a__a())
     (a__g#(a(), X) -> a__f#(b(), X), a__f#(X, X) -> a__a#())}
    STATUS:
     arrows: 0.736111
     SCCS (1):
      Scc:
       {  a__g#(a(), X) -> a__f#(b(), X),
              mark# h X -> mark# X,
              mark# h X -> a__h# mark X,
        mark# g(X1, X2) -> a__g#(mark X1, X2),
        mark# g(X1, X2) -> mark# X1,
        mark# f(X1, X2) -> mark# X1,
        mark# f(X1, X2) -> a__f#(mark X1, X2),
                a__h# X -> a__g#(mark X, X),
                a__h# X -> mark# X,
            a__f#(X, X) -> a__h# a__a()}
      
      SCC (10):
       Strict:
        {  a__g#(a(), X) -> a__f#(b(), X),
               mark# h X -> mark# X,
               mark# h X -> a__h# mark X,
         mark# g(X1, X2) -> a__g#(mark X1, X2),
         mark# g(X1, X2) -> mark# X1,
         mark# f(X1, X2) -> mark# X1,
         mark# f(X1, X2) -> a__f#(mark X1, X2),
                 a__h# X -> a__g#(mark X, X),
                 a__h# X -> mark# X,
             a__f#(X, X) -> a__h# a__a()}
       Weak:
       {  a__g(X1, X2) -> g(X1, X2),
          a__g(a(), X) -> a__f(b(), X),
              mark b() -> b(),
              mark a() -> a__a(),
              mark h X -> a__h mark X,
        mark g(X1, X2) -> a__g(mark X1, X2),
        mark f(X1, X2) -> a__f(mark X1, X2),
                a__h X -> a__g(mark X, X),
                a__h X -> h X,
            a__f(X, X) -> a__h a__a(),
          a__f(X1, X2) -> f(X1, X2),
                a__a() -> b(),
                a__a() -> a()}
       Open