MAYBE
TRS:
 {app(app(app(rec(), f), x), app(s(), y)) -> app(app(f, app(s(), y)), app(app(app(rec(), f), x), y)),
          app(app(app(rec(), f), x), 0()) -> x,
          app(app(add(), app(s(), x)), y) -> app(s(), app(app(add(), x), y)),
                  app(app(add(), 0()), y) -> y,
         app(app(mult(), app(s(), x)), y) -> app(app(add(), app(app(mult(), x), y)), y),
                 app(app(mult(), 0()), y) -> 0(),
                                   fact() -> app(app(rec(), mult()), app(s(), 0()))}
 DP:
  Strict:
   {app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)),
    app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)),
    app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(app(rec(), f), x), y),
            app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y),
            app#(app(add(), app(s(), x)), y) -> app#(add(), x),
            app#(app(add(), app(s(), x)), y) -> app#(s(), app(app(add(), x), y)),
           app#(app(mult(), app(s(), x)), y) -> app#(app(add(), app(app(mult(), x), y)), y),
           app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y),
           app#(app(mult(), app(s(), x)), y) -> app#(add(), app(app(mult(), x), y)),
           app#(app(mult(), app(s(), x)), y) -> app#(mult(), x),
                                     fact#() -> app#(app(rec(), mult()), app(s(), 0())),
                                     fact#() -> app#(s(), 0()),
                                     fact#() -> app#(rec(), mult())}
  Weak:
  {app(app(app(rec(), f), x), app(s(), y)) -> app(app(f, app(s(), y)), app(app(app(rec(), f), x), y)),
           app(app(app(rec(), f), x), 0()) -> x,
           app(app(add(), app(s(), x)), y) -> app(s(), app(app(add(), x), y)),
                   app(app(add(), 0()), y) -> y,
          app(app(mult(), app(s(), x)), y) -> app(app(add(), app(app(mult(), x), y)), y),
                  app(app(mult(), 0()), y) -> 0(),
                                    fact() -> app(app(rec(), mult()), app(s(), 0()))}
  EDG:
   {(app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y), app#(app(add(), app(s(), x)), y) -> app#(s(), app(app(add(), x), y)))
    (app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y), app#(app(add(), app(s(), x)), y) -> app#(add(), x))
    (app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y), app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y))
    (app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y), app#(app(mult(), app(s(), x)), y) -> app#(mult(), x))
    (app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y), app#(app(mult(), app(s(), x)), y) -> app#(add(), app(app(mult(), x), y)))
    (app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y), app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y))
    (app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y), app#(app(mult(), app(s(), x)), y) -> app#(app(add(), app(app(mult(), x), y)), y))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)), app#(app(mult(), app(s(), x)), y) -> app#(mult(), x))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)), app#(app(mult(), app(s(), x)), y) -> app#(add(), app(app(mult(), x), y)))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)), app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)), app#(app(mult(), app(s(), x)), y) -> app#(app(add(), app(app(mult(), x), y)), y))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)), app#(app(add(), app(s(), x)), y) -> app#(s(), app(app(add(), x), y)))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)), app#(app(add(), app(s(), x)), y) -> app#(add(), x))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)), app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)), app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(app(rec(), f), x), y))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)), app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)), app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)), app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)), app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)), app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(app(rec(), f), x), y))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)), app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)), app#(app(add(), app(s(), x)), y) -> app#(add(), x))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)), app#(app(add(), app(s(), x)), y) -> app#(s(), app(app(add(), x), y)))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)), app#(app(mult(), app(s(), x)), y) -> app#(app(add(), app(app(mult(), x), y)), y))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)), app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)), app#(app(mult(), app(s(), x)), y) -> app#(add(), app(app(mult(), x), y)))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)), app#(app(mult(), app(s(), x)), y) -> app#(mult(), x))
    (app#(app(mult(), app(s(), x)), y) -> app#(app(add(), app(app(mult(), x), y)), y), app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y))
    (app#(app(mult(), app(s(), x)), y) -> app#(app(add(), app(app(mult(), x), y)), y), app#(app(add(), app(s(), x)), y) -> app#(add(), x))
    (app#(app(mult(), app(s(), x)), y) -> app#(app(add(), app(app(mult(), x), y)), y), app#(app(add(), app(s(), x)), y) -> app#(s(), app(app(add(), x), y)))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(app(rec(), f), x), y), app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(app(rec(), f), x), y), app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)))
    (app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(app(rec(), f), x), y), app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(app(rec(), f), x), y))}
   SCCS:
    Scc:
     {app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y)}
    Scc:
     {app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y)}
    Scc:
     {app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)),
      app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)),
      app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(app(rec(), f), x), y)}
    SCC:
     Strict:
      {app#(app(mult(), app(s(), x)), y) -> app#(app(mult(), x), y)}
     Weak:
     {app(app(app(rec(), f), x), app(s(), y)) -> app(app(f, app(s(), y)), app(app(app(rec(), f), x), y)),
              app(app(app(rec(), f), x), 0()) -> x,
              app(app(add(), app(s(), x)), y) -> app(s(), app(app(add(), x), y)),
                      app(app(add(), 0()), y) -> y,
             app(app(mult(), app(s(), x)), y) -> app(app(add(), app(app(mult(), x), y)), y),
                     app(app(mult(), 0()), y) -> 0(),
                                       fact() -> app(app(rec(), mult()), app(s(), 0()))}
     Fail
    SCC:
     Strict:
      {app#(app(add(), app(s(), x)), y) -> app#(app(add(), x), y)}
     Weak:
     {app(app(app(rec(), f), x), app(s(), y)) -> app(app(f, app(s(), y)), app(app(app(rec(), f), x), y)),
              app(app(app(rec(), f), x), 0()) -> x,
              app(app(add(), app(s(), x)), y) -> app(s(), app(app(add(), x), y)),
                      app(app(add(), 0()), y) -> y,
             app(app(mult(), app(s(), x)), y) -> app(app(add(), app(app(mult(), x), y)), y),
                     app(app(mult(), 0()), y) -> 0(),
                                       fact() -> app(app(rec(), mult()), app(s(), 0()))}
     Fail
    SCC:
     Strict:
      {app#(app(app(rec(), f), x), app(s(), y)) -> app#(f, app(s(), y)),
       app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(f, app(s(), y)), app(app(app(rec(), f), x), y)),
       app#(app(app(rec(), f), x), app(s(), y)) -> app#(app(app(rec(), f), x), y)}
     Weak:
     {app(app(app(rec(), f), x), app(s(), y)) -> app(app(f, app(s(), y)), app(app(app(rec(), f), x), y)),
              app(app(app(rec(), f), x), 0()) -> x,
              app(app(add(), app(s(), x)), y) -> app(s(), app(app(add(), x), y)),
                      app(app(add(), 0()), y) -> y,
             app(app(mult(), app(s(), x)), y) -> app(app(add(), app(app(mult(), x), y)), y),
                     app(app(mult(), 0()), y) -> 0(),
                                       fact() -> app(app(rec(), mult()), app(s(), 0()))}
     Fail