MAYBE
Time: 0.001225
TRS:
 {  a__f(X1, X2) -> f(X1, X2),
    a__f(g X, Y) -> a__f(mark X, f(g X, Y)),
  mark f(X1, X2) -> a__f(mark X1, X2),
        mark g X -> g mark X}
 DP:
  DP:
   {  a__f#(g X, Y) -> a__f#(mark X, f(g X, Y)),
      a__f#(g X, Y) -> mark# X,
    mark# f(X1, X2) -> a__f#(mark X1, X2),
    mark# f(X1, X2) -> mark# X1,
          mark# g X -> mark# X}
  TRS:
  {  a__f(X1, X2) -> f(X1, X2),
     a__f(g X, Y) -> a__f(mark X, f(g X, Y)),
   mark f(X1, X2) -> a__f(mark X1, X2),
         mark g X -> g mark X}
  EDG:
   {(mark# f(X1, X2) -> mark# X1, mark# g X -> mark# X)
    (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))
    (mark# f(X1, X2) -> a__f#(mark X1, X2), a__f#(g X, Y) -> mark# X)
    (mark# f(X1, X2) -> a__f#(mark X1, X2), a__f#(g X, Y) -> a__f#(mark X, f(g X, Y)))
    (mark# g X -> mark# X, mark# f(X1, X2) -> a__f#(mark X1, X2))
    (mark# g X -> mark# X, mark# f(X1, X2) -> mark# X1)
    (mark# g X -> mark# X, mark# g X -> mark# X)
    (a__f#(g X, Y) -> mark# X, mark# f(X1, X2) -> a__f#(mark X1, X2))
    (a__f#(g X, Y) -> mark# X, mark# f(X1, X2) -> mark# X1)
    (a__f#(g X, Y) -> mark# X, mark# g X -> mark# X)
    (a__f#(g X, Y) -> a__f#(mark X, f(g X, Y)), a__f#(g X, Y) -> a__f#(mark X, f(g X, Y)))
    (a__f#(g X, Y) -> a__f#(mark X, f(g X, Y)), a__f#(g X, Y) -> mark# X)}
   STATUS:
    arrows: 0.480000
    SCCS (1):
     Scc:
      {  a__f#(g X, Y) -> a__f#(mark X, f(g X, Y)),
         a__f#(g X, Y) -> mark# X,
       mark# f(X1, X2) -> a__f#(mark X1, X2),
       mark# f(X1, X2) -> mark# X1,
             mark# g X -> mark# X}
     
     SCC (5):
      Strict:
       {  a__f#(g X, Y) -> a__f#(mark X, f(g X, Y)),
          a__f#(g X, Y) -> mark# X,
        mark# f(X1, X2) -> a__f#(mark X1, X2),
        mark# f(X1, X2) -> mark# X1,
              mark# g X -> mark# X}
      Weak:
      {  a__f(X1, X2) -> f(X1, X2),
         a__f(g X, Y) -> a__f(mark X, f(g X, Y)),
       mark f(X1, X2) -> a__f(mark X1, X2),
             mark g X -> g mark X}
      Open