YES

Problem:
 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))))

Proof:
 DP Processor:
  DPs:
   minus#(+(x,y)) -> minus#(y)
   minus#(+(x,y)) -> minus#(minus(y))
   minus#(+(x,y)) -> minus#(minus(minus(y)))
   minus#(+(x,y)) -> 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(y))
   minus#(*(x,y)) -> minus#(minus(minus(y)))
   minus#(*(x,y)) -> minus#(x)
   minus#(*(x,y)) -> minus#(minus(x))
   minus#(*(x,y)) -> minus#(minus(minus(x)))
   f#(minus(x)) -> f#(x)
   f#(minus(x)) -> minus#(f(x))
   f#(minus(x)) -> minus#(minus(f(x)))
   f#(minus(x)) -> minus#(minus(minus(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))))
  TDG Processor:
   DPs:
    minus#(+(x,y)) -> minus#(y)
    minus#(+(x,y)) -> minus#(minus(y))
    minus#(+(x,y)) -> minus#(minus(minus(y)))
    minus#(+(x,y)) -> 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(y))
    minus#(*(x,y)) -> minus#(minus(minus(y)))
    minus#(*(x,y)) -> minus#(x)
    minus#(*(x,y)) -> minus#(minus(x))
    minus#(*(x,y)) -> minus#(minus(minus(x)))
    f#(minus(x)) -> f#(x)
    f#(minus(x)) -> minus#(f(x))
    f#(minus(x)) -> minus#(minus(f(x)))
    f#(minus(x)) -> minus#(minus(minus(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))))
   graph:
    f#(minus(x)) -> f#(x) -> f#(minus(x)) -> minus#(minus(minus(f(x))))
    f#(minus(x)) -> f#(x) -> f#(minus(x)) -> minus#(minus(f(x)))
    f#(minus(x)) -> f#(x) -> f#(minus(x)) -> minus#(f(x))
    f#(minus(x)) -> f#(x) -> f#(minus(x)) -> f#(x)
    f#(minus(x)) -> minus#(f(x)) ->
    minus#(*(x,y)) -> minus#(minus(minus(x)))
    f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(minus(x))
    f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(x)
    f#(minus(x)) -> minus#(f(x)) ->
    minus#(*(x,y)) -> minus#(minus(minus(y)))
    f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(minus(y))
    f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(y)
    f#(minus(x)) -> minus#(f(x)) ->
    minus#(+(x,y)) -> minus#(minus(minus(x)))
    f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(minus(x))
    f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(x)
    f#(minus(x)) -> minus#(f(x)) ->
    minus#(+(x,y)) -> minus#(minus(minus(y)))
    f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(minus(y))
    f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(y)
    f#(minus(x)) -> minus#(minus(f(x))) ->
    minus#(*(x,y)) -> minus#(minus(minus(x)))
    f#(minus(x)) -> minus#(minus(f(x))) ->
    minus#(*(x,y)) -> minus#(minus(x))
    f#(minus(x)) -> minus#(minus(f(x))) ->
    minus#(*(x,y)) -> minus#(x)
    f#(minus(x)) -> minus#(minus(f(x))) ->
    minus#(*(x,y)) -> minus#(minus(minus(y)))
    f#(minus(x)) -> minus#(minus(f(x))) ->
    minus#(*(x,y)) -> minus#(minus(y))
    f#(minus(x)) -> minus#(minus(f(x))) ->
    minus#(*(x,y)) -> minus#(y)
    f#(minus(x)) -> minus#(minus(f(x))) ->
    minus#(+(x,y)) -> minus#(minus(minus(x)))
    f#(minus(x)) -> minus#(minus(f(x))) ->
    minus#(+(x,y)) -> minus#(minus(x))
    f#(minus(x)) -> minus#(minus(f(x))) ->
    minus#(+(x,y)) -> minus#(x)
    f#(minus(x)) -> minus#(minus(f(x))) ->
    minus#(+(x,y)) -> minus#(minus(minus(y)))
    f#(minus(x)) -> minus#(minus(f(x))) ->
    minus#(+(x,y)) -> minus#(minus(y))
    f#(minus(x)) -> minus#(minus(f(x))) ->
    minus#(+(x,y)) -> minus#(y)
    f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
    minus#(*(x,y)) -> minus#(minus(minus(x)))
    f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
    minus#(*(x,y)) -> minus#(minus(x))
    f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
    minus#(*(x,y)) -> minus#(x)
    f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
    minus#(*(x,y)) -> minus#(minus(minus(y)))
    f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
    minus#(*(x,y)) -> minus#(minus(y))
    f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
    minus#(*(x,y)) -> minus#(y)
    f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
    minus#(+(x,y)) -> minus#(minus(minus(x)))
    f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
    minus#(+(x,y)) -> minus#(minus(x))
    f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
    minus#(+(x,y)) -> minus#(x)
    f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
    minus#(+(x,y)) -> minus#(minus(minus(y)))
    f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
    minus#(+(x,y)) -> minus#(minus(y))
    f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
    minus#(+(x,y)) -> 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(x))
    minus#(*(x,y)) -> minus#(minus(minus(y))) ->
    minus#(*(x,y)) -> 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#(minus(y))
    minus#(*(x,y)) -> minus#(minus(minus(y))) ->
    minus#(*(x,y)) -> 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(x))
    minus#(*(x,y)) -> minus#(minus(minus(y))) ->
    minus#(+(x,y)) -> 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#(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#(minus(minus(x)))
    minus#(*(x,y)) -> minus#(minus(minus(x))) ->
    minus#(*(x,y)) -> minus#(minus(x))
    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(y))
    minus#(*(x,y)) -> minus#(minus(minus(x))) ->
    minus#(*(x,y)) -> 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(x))
    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(y))
    minus#(*(x,y)) -> minus#(minus(minus(x))) ->
    minus#(+(x,y)) -> 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(x))
    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(y))
    minus#(*(x,y)) -> minus#(minus(y)) ->
    minus#(*(x,y)) -> 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(x))
    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(y))
    minus#(*(x,y)) -> minus#(minus(y)) ->
    minus#(+(x,y)) -> 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(x))
    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(y))
    minus#(*(x,y)) -> minus#(minus(x)) ->
    minus#(*(x,y)) -> 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(x))
    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(y))
    minus#(*(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(y)
    minus#(*(x,y)) -> minus#(y) ->
    minus#(*(x,y)) -> minus#(minus(minus(x)))
    minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(x))
    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(y))
    minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(y)
    minus#(*(x,y)) -> minus#(y) ->
    minus#(+(x,y)) -> minus#(minus(minus(x)))
    minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(x))
    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(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#(x) -> minus#(*(x,y)) -> minus#(minus(x))
    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(y))
    minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(y)
    minus#(*(x,y)) -> minus#(x) ->
    minus#(+(x,y)) -> minus#(minus(minus(x)))
    minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(x))
    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(y))
    minus#(*(x,y)) -> minus#(x) ->
    minus#(+(x,y)) -> 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(x))
    minus#(+(x,y)) -> minus#(minus(minus(y))) ->
    minus#(*(x,y)) -> 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#(minus(y))
    minus#(+(x,y)) -> minus#(minus(minus(y))) ->
    minus#(*(x,y)) -> 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(x))
    minus#(+(x,y)) -> minus#(minus(minus(y))) ->
    minus#(+(x,y)) -> 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#(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#(minus(minus(x)))
    minus#(+(x,y)) -> minus#(minus(minus(x))) ->
    minus#(*(x,y)) -> minus#(minus(x))
    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(y))
    minus#(+(x,y)) -> minus#(minus(minus(x))) ->
    minus#(*(x,y)) -> 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(x))
    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(y))
    minus#(+(x,y)) -> minus#(minus(minus(x))) ->
    minus#(+(x,y)) -> 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(x))
    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(y))
    minus#(+(x,y)) -> minus#(minus(y)) ->
    minus#(*(x,y)) -> 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(x))
    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(y))
    minus#(+(x,y)) -> minus#(minus(y)) ->
    minus#(+(x,y)) -> 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(x))
    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(y))
    minus#(+(x,y)) -> minus#(minus(x)) ->
    minus#(*(x,y)) -> 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(x))
    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(y))
    minus#(+(x,y)) -> minus#(minus(x)) -> minus#(+(x,y)) -> minus#(y)
    minus#(+(x,y)) -> minus#(y) ->
    minus#(*(x,y)) -> minus#(minus(minus(x)))
    minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(x))
    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(y))
    minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(y)
    minus#(+(x,y)) -> minus#(y) ->
    minus#(+(x,y)) -> minus#(minus(minus(x)))
    minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(x))
    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(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#(x) -> minus#(*(x,y)) -> minus#(minus(x))
    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(y))
    minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(y)
    minus#(+(x,y)) -> minus#(x) ->
    minus#(+(x,y)) -> minus#(minus(minus(x)))
    minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(x))
    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(y))
    minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(y)
   CDG Processor:
    DPs:
     minus#(+(x,y)) -> minus#(y)
     minus#(+(x,y)) -> minus#(minus(y))
     minus#(+(x,y)) -> minus#(minus(minus(y)))
     minus#(+(x,y)) -> 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(y))
     minus#(*(x,y)) -> minus#(minus(minus(y)))
     minus#(*(x,y)) -> minus#(x)
     minus#(*(x,y)) -> minus#(minus(x))
     minus#(*(x,y)) -> minus#(minus(minus(x)))
     f#(minus(x)) -> f#(x)
     f#(minus(x)) -> minus#(f(x))
     f#(minus(x)) -> minus#(minus(f(x)))
     f#(minus(x)) -> minus#(minus(minus(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))))
    graph:
     minus#(*(x,y)) -> minus#(minus(minus(y))) ->
     minus#(+(x,y)) -> minus#(y)
     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(y)))
     minus#(*(x,y)) -> minus#(minus(minus(y))) ->
     minus#(+(x,y)) -> minus#(x)
     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(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(y))
     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#(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#(y)
     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(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(x))
     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#(y)
     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(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(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#(y)
     minus#(*(x,y)) -> minus#(minus(y)) ->
     minus#(+(x,y)) -> minus#(minus(y))
     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#(minus(x))
     minus#(*(x,y)) -> minus#(minus(y)) ->
     minus#(+(x,y)) -> minus#(minus(minus(x)))
     minus#(*(x,y)) -> minus#(minus(y)) ->
     minus#(*(x,y)) -> minus#(y)
     minus#(*(x,y)) -> minus#(minus(y)) ->
     minus#(*(x,y)) -> minus#(minus(y))
     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#(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#(y)
     minus#(*(x,y)) -> minus#(minus(x)) ->
     minus#(+(x,y)) -> minus#(minus(y))
     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#(minus(x))
     minus#(*(x,y)) -> minus#(minus(x)) ->
     minus#(+(x,y)) -> minus#(minus(minus(x)))
     minus#(*(x,y)) -> minus#(minus(x)) ->
     minus#(*(x,y)) -> minus#(y)
     minus#(*(x,y)) -> minus#(minus(x)) ->
     minus#(*(x,y)) -> minus#(minus(y))
     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#(minus(x))
     minus#(*(x,y)) -> minus#(minus(x)) ->
     minus#(*(x,y)) -> minus#(minus(minus(x)))
     minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(y)
     minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(y))
     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#(minus(x))
     minus#(*(x,y)) -> minus#(y) ->
     minus#(+(x,y)) -> minus#(minus(minus(x)))
     minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(y)
     minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(y))
     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#(minus(x))
     minus#(*(x,y)) -> minus#(y) ->
     minus#(*(x,y)) -> minus#(minus(minus(x)))
     minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(y)
     minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(y))
     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#(minus(x))
     minus#(*(x,y)) -> minus#(x) ->
     minus#(+(x,y)) -> minus#(minus(minus(x)))
     minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(y)
     minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(y))
     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#(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#(y)
     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(y)))
     minus#(+(x,y)) -> minus#(minus(minus(y))) ->
     minus#(+(x,y)) -> minus#(x)
     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(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(y))
     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#(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#(y)
     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(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(x))
     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#(y)
     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(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(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#(y)
     minus#(+(x,y)) -> minus#(minus(y)) ->
     minus#(+(x,y)) -> minus#(minus(y))
     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#(minus(x))
     minus#(+(x,y)) -> minus#(minus(y)) ->
     minus#(+(x,y)) -> minus#(minus(minus(x)))
     minus#(+(x,y)) -> minus#(minus(y)) ->
     minus#(*(x,y)) -> minus#(y)
     minus#(+(x,y)) -> minus#(minus(y)) ->
     minus#(*(x,y)) -> minus#(minus(y))
     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#(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#(y)
     minus#(+(x,y)) -> minus#(minus(x)) ->
     minus#(+(x,y)) -> minus#(minus(y))
     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#(minus(x))
     minus#(+(x,y)) -> minus#(minus(x)) ->
     minus#(+(x,y)) -> minus#(minus(minus(x)))
     minus#(+(x,y)) -> minus#(minus(x)) ->
     minus#(*(x,y)) -> minus#(y)
     minus#(+(x,y)) -> minus#(minus(x)) ->
     minus#(*(x,y)) -> minus#(minus(y))
     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#(minus(x))
     minus#(+(x,y)) -> minus#(minus(x)) ->
     minus#(*(x,y)) -> minus#(minus(minus(x)))
     minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(y)
     minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(y))
     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#(minus(x))
     minus#(+(x,y)) -> minus#(y) ->
     minus#(+(x,y)) -> minus#(minus(minus(x)))
     minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(y)
     minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(y))
     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#(minus(x))
     minus#(+(x,y)) -> minus#(y) ->
     minus#(*(x,y)) -> minus#(minus(minus(x)))
     minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(y)
     minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(y))
     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#(minus(x))
     minus#(+(x,y)) -> minus#(x) ->
     minus#(+(x,y)) -> minus#(minus(minus(x)))
     minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(y)
     minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(y))
     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#(minus(x))
     minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(minus(x)))
    SCC Processor:
     #sccs: 1
     #rules: 12
     #arcs: 144/256
     DPs:
      minus#(*(x,y)) -> minus#(minus(minus(y)))
      minus#(*(x,y)) -> minus#(minus(minus(x)))
      minus#(*(x,y)) -> minus#(minus(x))
      minus#(*(x,y)) -> minus#(x)
      minus#(*(x,y)) -> minus#(minus(y))
      minus#(*(x,y)) -> minus#(y)
      minus#(+(x,y)) -> minus#(minus(minus(x)))
      minus#(+(x,y)) -> minus#(minus(x))
      minus#(+(x,y)) -> minus#(x)
      minus#(+(x,y)) -> minus#(minus(minus(y)))
      minus#(+(x,y)) -> minus#(minus(y))
      minus#(+(x,y)) -> minus#(y)
     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))))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [minus#](x0) = 5x0,
       
       [f](x0) = 0,
       
       [*](x0, x1) = x0 + x1 + 5,
       
       [+](x0, x1) = x0 + x1 + 5,
       
       [minus](x0) = x0
      orientation:
       minus#(*(x,y)) = 5x + 5y + 25 >= 5y = minus#(minus(minus(y)))
       
       minus#(*(x,y)) = 5x + 5y + 25 >= 5x = minus#(minus(minus(x)))
       
       minus#(*(x,y)) = 5x + 5y + 25 >= 5x = minus#(minus(x))
       
       minus#(*(x,y)) = 5x + 5y + 25 >= 5x = minus#(x)
       
       minus#(*(x,y)) = 5x + 5y + 25 >= 5y = minus#(minus(y))
       
       minus#(*(x,y)) = 5x + 5y + 25 >= 5y = minus#(y)
       
       minus#(+(x,y)) = 5x + 5y + 25 >= 5x = minus#(minus(minus(x)))
       
       minus#(+(x,y)) = 5x + 5y + 25 >= 5x = minus#(minus(x))
       
       minus#(+(x,y)) = 5x + 5y + 25 >= 5x = minus#(x)
       
       minus#(+(x,y)) = 5x + 5y + 25 >= 5y = minus#(minus(minus(y)))
       
       minus#(+(x,y)) = 5x + 5y + 25 >= 5y = minus#(minus(y))
       
       minus#(+(x,y)) = 5x + 5y + 25 >= 5y = minus#(y)
       
       minus(minus(x)) = x >= x = x
       
       minus(+(x,y)) = x + y + 5 >= x + y + 5 = *(minus(minus(minus(x))),minus(minus(minus(y))))
       
       minus(*(x,y)) = x + y + 5 >= x + y + 5 = +(minus(minus(minus(x))),minus(minus(minus(y))))
       
       f(minus(x)) = 0 >= 0 = minus(minus(minus(f(x))))
      problem:
       DPs:
        
       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))))
      Qed