MAYBE
Time: 0.029523
TRS:
 {minus minus x -> x,
  minus *(x, y) -> +(minus minus minus x, minus minus minus y),
  minus +(x, y) -> *(minus minus minus x, minus minus minus y),
      f minus x -> minus minus minus f x}
 DP:
  DP:
   {minus# *(x, y) -> minus# x,
    minus# *(x, y) -> minus# y,
    minus# *(x, y) -> minus# minus x,
    minus# *(x, y) -> minus# minus y,
    minus# *(x, y) -> minus# minus minus x,
    minus# *(x, y) -> minus# minus minus y,
    minus# +(x, y) -> minus# x,
    minus# +(x, y) -> minus# y,
    minus# +(x, y) -> minus# minus x,
    minus# +(x, y) -> minus# minus y,
    minus# +(x, y) -> minus# minus minus x,
    minus# +(x, y) -> minus# minus minus y,
        f# minus x -> minus# minus minus f x,
        f# minus x -> minus# minus f x,
        f# minus x -> minus# f x,
        f# minus x -> f# x}
  TRS:
  {minus minus x -> x,
   minus *(x, y) -> +(minus minus minus x, minus minus minus y),
   minus +(x, y) -> *(minus minus minus x, minus minus minus y),
       f minus x -> minus minus minus f x}
  EDG:
   {(minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# minus minus y)
    (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# minus minus x)
    (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# minus y)
    (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# minus x)
    (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# y)
    (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# x)
    (minus# +(x, y) -> minus# x, minus# *(x, y) -> minus# minus minus y)
    (minus# +(x, y) -> minus# x, minus# *(x, y) -> minus# minus minus x)
    (minus# +(x, y) -> minus# x, minus# *(x, y) -> minus# minus y)
    (minus# +(x, y) -> minus# x, minus# *(x, y) -> minus# minus x)
    (minus# +(x, y) -> minus# x, minus# *(x, y) -> minus# y)
    (minus# +(x, y) -> minus# x, minus# *(x, y) -> minus# x)
    (minus# *(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus minus y)
    (minus# *(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus minus x)
    (minus# *(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus y)
    (minus# *(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus x)
    (minus# *(x, y) -> minus# minus y, minus# +(x, y) -> minus# y)
    (minus# *(x, y) -> minus# minus y, minus# +(x, y) -> minus# x)
    (minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus minus y)
    (minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus minus x)
    (minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus y)
    (minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus x)
    (minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# y)
    (minus# *(x, y) -> minus# minus y, minus# *(x, y) -> minus# x)
    (minus# *(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus minus y)
    (minus# *(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus minus x)
    (minus# *(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus y)
    (minus# *(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus x)
    (minus# *(x, y) -> minus# minus x, minus# +(x, y) -> minus# y)
    (minus# *(x, y) -> minus# minus x, minus# +(x, y) -> minus# x)
    (minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus minus y)
    (minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus minus x)
    (minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus y)
    (minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus x)
    (minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# y)
    (minus# *(x, y) -> minus# minus x, minus# *(x, y) -> minus# x)
    (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# minus minus y)
    (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# minus minus x)
    (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# minus y)
    (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# minus x)
    (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# y)
    (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# x)
    (minus# +(x, y) -> minus# y, minus# *(x, y) -> minus# minus minus y)
    (minus# +(x, y) -> minus# y, minus# *(x, y) -> minus# minus minus x)
    (minus# +(x, y) -> minus# y, minus# *(x, y) -> minus# minus y)
    (minus# +(x, y) -> minus# y, minus# *(x, y) -> minus# minus x)
    (minus# +(x, y) -> minus# y, minus# *(x, y) -> minus# y)
    (minus# +(x, y) -> minus# y, minus# *(x, y) -> minus# x)
    (minus# *(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus minus y)
    (minus# *(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus minus x)
    (minus# *(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus y)
    (minus# *(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus x)
    (minus# *(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# y)
    (minus# *(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# x)
    (minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus minus y)
    (minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus minus x)
    (minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus y)
    (minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus x)
    (minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# y)
    (minus# *(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# x)
    (minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus minus y)
    (minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus minus x)
    (minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus y)
    (minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# minus x)
    (minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# y)
    (minus# +(x, y) -> minus# minus minus x, minus# +(x, y) -> minus# x)
    (minus# +(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus minus y)
    (minus# +(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus minus x)
    (minus# +(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus y)
    (minus# +(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# minus x)
    (minus# +(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# y)
    (minus# +(x, y) -> minus# minus minus x, minus# *(x, y) -> minus# x)
    (minus# +(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# x)
    (minus# +(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# y)
    (minus# +(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus x)
    (minus# +(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus y)
    (minus# +(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus minus x)
    (minus# +(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus minus y)
    (minus# +(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# x)
    (minus# +(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# y)
    (minus# +(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus x)
    (minus# +(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus y)
    (minus# +(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus minus x)
    (minus# +(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus minus y)
    (minus# *(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# x)
    (minus# *(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# y)
    (minus# *(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus x)
    (minus# *(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus y)
    (minus# *(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus minus x)
    (minus# *(x, y) -> minus# minus minus y, minus# *(x, y) -> minus# minus minus y)
    (minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# x)
    (minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# y)
    (minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus x)
    (minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus y)
    (minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus minus x)
    (minus# *(x, y) -> minus# minus minus y, minus# +(x, y) -> minus# minus minus y)
    (minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# x)
    (minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# y)
    (minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# minus x)
    (minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# minus y)
    (minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# minus minus x)
    (minus# *(x, y) -> minus# y, minus# *(x, y) -> minus# minus minus y)
    (minus# *(x, y) -> minus# y, minus# +(x, y) -> minus# x)
    (minus# *(x, y) -> minus# y, minus# +(x, y) -> minus# y)
    (minus# *(x, y) -> minus# y, minus# +(x, y) -> minus# minus x)
    (minus# *(x, y) -> minus# y, minus# +(x, y) -> minus# minus y)
    (minus# *(x, y) -> minus# y, minus# +(x, y) -> minus# minus minus x)
    (minus# *(x, y) -> minus# y, minus# +(x, y) -> minus# minus minus y)
    (minus# +(x, y) -> minus# minus x, minus# *(x, y) -> minus# x)
    (minus# +(x, y) -> minus# minus x, minus# *(x, y) -> minus# y)
    (minus# +(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus x)
    (minus# +(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus y)
    (minus# +(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus minus x)
    (minus# +(x, y) -> minus# minus x, minus# *(x, y) -> minus# minus minus y)
    (minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# x)
    (minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# y)
    (minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus x)
    (minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus y)
    (minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus minus x)
    (minus# +(x, y) -> minus# minus x, minus# +(x, y) -> minus# minus minus y)
    (minus# +(x, y) -> minus# minus y, minus# *(x, y) -> minus# x)
    (minus# +(x, y) -> minus# minus y, minus# *(x, y) -> minus# y)
    (minus# +(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus x)
    (minus# +(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus y)
    (minus# +(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus minus x)
    (minus# +(x, y) -> minus# minus y, minus# *(x, y) -> minus# minus minus y)
    (minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# x)
    (minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# y)
    (minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus x)
    (minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus y)
    (minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus minus x)
    (minus# +(x, y) -> minus# minus y, minus# +(x, y) -> minus# minus minus y)
    (minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# x)
    (minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# y)
    (minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# minus x)
    (minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# minus y)
    (minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# minus minus x)
    (minus# *(x, y) -> minus# x, minus# *(x, y) -> minus# minus minus y)
    (minus# *(x, y) -> minus# x, minus# +(x, y) -> minus# x)
    (minus# *(x, y) -> minus# x, minus# +(x, y) -> minus# y)
    (minus# *(x, y) -> minus# x, minus# +(x, y) -> minus# minus x)
    (minus# *(x, y) -> minus# x, minus# +(x, y) -> minus# minus y)
    (minus# *(x, y) -> minus# x, minus# +(x, y) -> minus# minus minus x)
    (minus# *(x, y) -> minus# x, minus# +(x, y) -> minus# minus minus y)}
   STATUS:
    arrows: 0.437500
    SCCS (1):
     Scc:
      {minus# *(x, y) -> minus# x,
       minus# *(x, y) -> minus# y,
       minus# *(x, y) -> minus# minus x,
       minus# *(x, y) -> minus# minus y,
       minus# *(x, y) -> minus# minus minus x,
       minus# *(x, y) -> minus# minus minus y,
       minus# +(x, y) -> minus# x,
       minus# +(x, y) -> minus# y,
       minus# +(x, y) -> minus# minus x,
       minus# +(x, y) -> minus# minus y,
       minus# +(x, y) -> minus# minus minus x,
       minus# +(x, y) -> minus# minus minus y}
     
     
     
     
     
     SCC (12):
      Strict:
       {minus# *(x, y) -> minus# x,
        minus# *(x, y) -> minus# y,
        minus# *(x, y) -> minus# minus x,
        minus# *(x, y) -> minus# minus y,
        minus# *(x, y) -> minus# minus minus x,
        minus# *(x, y) -> minus# minus minus y,
        minus# +(x, y) -> minus# x,
        minus# +(x, y) -> minus# y,
        minus# +(x, y) -> minus# minus x,
        minus# +(x, y) -> minus# minus y,
        minus# +(x, y) -> minus# minus minus x,
        minus# +(x, y) -> minus# minus minus y}
      Weak:
      {minus minus x -> x,
       minus *(x, y) -> +(minus minus minus x, minus minus minus y),
       minus +(x, y) -> *(minus minus minus x, minus minus minus y),
           f minus x -> minus minus minus f x}
      Open