MAYBE

Problem:
 app(app(app(app(rec(),t),u),v),0()) -> t
 app(app(app(app(rec(),t),u),v),app(s(),x)) -> app(app(u,x),app(app(app(app(rec(),t),u),v),x))
 app(app(app(app(rec(),t),u),v),app(lim(),f)) ->
 app(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
 app(app(app(app(rectuv(),t),u),v),n()) -> app(app(app(app(rec(),t),u),v),n())

Proof:
 DP Processor:
  DPs:
   app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x)
   app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x)
   app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
   app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n())
   app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(rectuv(),t)
   app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(rectuv(),t),u)
   app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(rectuv(),t),u),v)
   app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(app(rectuv(),t),u),v),app(f,n()))
   app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f)
   app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
   app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
   app#(app(app(app(rectuv(),t),u),v),n()) -> app#(rec(),t)
   app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(rec(),t),u)
   app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(rec(),t),u),v)
   app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(app(rec(),t),u),v),n())
  TRS:
   app(app(app(app(rec(),t),u),v),0()) -> t
   app(app(app(app(rec(),t),u),v),app(s(),x)) -> app(app(u,x),app(app(app(app(rec(),t),u),v),x))
   app(app(app(app(rec(),t),u),v),app(lim(),f)) ->
   app(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
   app(app(app(app(rectuv(),t),u),v),n()) -> app(app(app(app(rec(),t),u),v),n())
  EDG Processor:
   DPs:
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n())
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(rectuv(),t)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(rectuv(),t),u)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(rectuv(),t),u),v)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(app(rectuv(),t),u),v),app(f,n()))
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(rec(),t)
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(rec(),t),u)
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(rec(),t),u),v)
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(app(rec(),t),u),v),n())
   TRS:
    app(app(app(app(rec(),t),u),v),0()) -> t
    app(app(app(app(rec(),t),u),v),app(s(),x)) -> app(app(u,x),app(app(app(app(rec(),t),u),v),x))
    app(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
    app(app(app(app(rectuv(),t),u),v),n()) -> app(app(app(app(rec(),t),u),v),n())
   graph:
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(app(rectuv(),t),u),v),app(f,n()))
    ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(rec(),t)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(app(rectuv(),t),u),v),app(f,n()))
    ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(rec(),t),u)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(app(rectuv(),t),u),v),app(f,n()))
    ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(rec(),t),u),v)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(app(rectuv(),t),u),v),app(f,n()))
    ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(app(rec(),t),u),v),n())
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n())
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(rectuv(),t)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(rectuv(),t),u)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(rectuv(),t),u),v)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(app(rectuv(),t),u),v),app(f,n()))
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(rec(),t)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(rec(),t),u)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(rec(),t),u),v)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n()))) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(app(rec(),t),u),v),n())
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n())
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(rectuv(),t)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(rectuv(),t),u)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(rectuv(),t),u),v)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(app(rectuv(),t),u),v),app(f,n()))
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(rec(),t)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(rec(),t),u)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(rec(),t),u),v)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(app(rec(),t),u),v),n())
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n()) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(rec(),t)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n()) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(rec(),t),u)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n()) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(rec(),t),u),v)
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n()) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(app(rec(),t),u),v),n())
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n())
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(rectuv(),t)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(rectuv(),t),u)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(rectuv(),t),u),v)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(app(rectuv(),t),u),v),app(f,n()))
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n())
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(rectuv(),t)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(rectuv(),t),u)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(rectuv(),t),u),v)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(app(rectuv(),t),u),v),app(f,n()))
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(rec(),t)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(rec(),t),u)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(rec(),t),u),v)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(app(rec(),t),u),v),n())
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n())
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(rectuv(),t)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(rectuv(),t),u)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(rectuv(),t),u),v)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(app(rectuv(),t),u),v),app(f,n()))
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
    app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(rec(),t)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(rec(),t),u)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(rec(),t),u),v)
    app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
    app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(app(rec(),t),u),v),n())
   CDG Processor:
    DPs:
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n())
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(rectuv(),t)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(rectuv(),t),u)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(rectuv(),t),u),v)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
     app#(app(app(app(rectuv(),t),u),v),app(f,n()))
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
     app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(rec(),t)
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(rec(),t),u)
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(rec(),t),u),v)
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(app(rec(),t),u),v),n())
    TRS:
     app(app(app(app(rec(),t),u),v),0()) -> t
     app(app(app(app(rec(),t),u),v),app(s(),x)) -> app(app(u,x),app(app(app(app(rec(),t),u),v),x))
     app(app(app(app(rec(),t),u),v),app(lim(),f)) ->
     app(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
     app(app(app(app(rectuv(),t),u),v),n()) -> app(app(app(app(rec(),t),u),v),n())
    graph:
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(app(rec(),t),u),v),n())
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(rec(),t),u),v)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(rec(),t),u)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(rec(),t)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
     app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
     app#(app(app(app(rectuv(),t),u),v),app(f,n()))
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(rectuv(),t),u),v)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(rectuv(),t),u)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(rectuv(),t)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n())
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f) ->
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n()) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(app(rec(),t),u),v),n())
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n()) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(rec(),t),u),v)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n()) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(rec(),t),u)
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n()) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(rec(),t)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
     app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
     app#(app(app(app(rectuv(),t),u),v),app(f,n()))
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(rectuv(),t),u),v)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(rectuv(),t),u)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(rectuv(),t)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n())
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x) ->
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(app(rec(),t),u),v),n())
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(rec(),t),u),v)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(rec(),t),u)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(rec(),t)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
     app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
     app#(app(app(app(rectuv(),t),u),v),app(f,n()))
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(rectuv(),t),u),v)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(rectuv(),t),u)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(rectuv(),t)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n())
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x)) ->
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(app(rec(),t),u),v),n())
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(app(rec(),t),u),v)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(app(rec(),t),u)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rectuv(),t),u),v),n()) -> app#(rec(),t)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
     app#(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) ->
     app#(app(app(app(rectuv(),t),u),v),app(f,n()))
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(app(rectuv(),t),u),v)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(app(rectuv(),t),u)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(rectuv(),t)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(f,n())
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
     app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x)
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x) ->
     app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x)
    SCC Processor:
     #sccs: 1
     #rules: 4
     #arcs: 56/196
     DPs:
      app#(app(app(app(rec(),t),u),v),app(lim(),f)) -> app#(v,f)
      app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(app(app(app(rec(),t),u),v),x)
      app#(app(app(app(rec(),t),u),v),app(s(),x)) -> app#(u,x)
      app#(app(app(app(rec(),t),u),v),app(s(),x)) ->
      app#(app(u,x),app(app(app(app(rec(),t),u),v),x))
     TRS:
      app(app(app(app(rec(),t),u),v),0()) -> t
      app(app(app(app(rec(),t),u),v),app(s(),x)) -> app(app(u,x),app(app(app(app(rec(),t),u),v),x))
      app(app(app(app(rec(),t),u),v),app(lim(),f)) ->
      app(app(v,f),app(app(app(app(rectuv(),t),u),v),app(f,n())))
      app(app(app(app(rectuv(),t),u),v),n()) -> app(app(app(app(rec(),t),u),v),n())
     Open