MAYBE

Problem:
 leq(0(),x) -> tt()
 leq(s(x),0()) -> ff()
 leq(s(x),s(y)) -> leq(x,y)
 split(nil()) -> app(nil(),nil())
 split(cons(x,nil())) -> app(cons(x,nil()),nil())
 split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
 split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
 merge([](),xs) -> xs
 merge(xs,[]()) -> xs
 merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
 ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
 ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
 mergesort(xs) -> mergesort1(split(xs))
 mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))

Proof:
 DP Processor:
  DPs:
   leq#(s(x),s(y)) -> leq#(x,y)
   split#(cons(x,cons(y,xs))) -> split#(xs)
   split#(cons(x,cons(y,xs))) -> split1#(x,y,split(xs))
   merge#(cons(x,xs),cons(y,ys)) -> leq#(x,y)
   merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
   ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys))
   ifmerge#(ff(),x,y,xs,ys) -> merge#(cons(x,xs),ys)
   mergesort#(xs) -> split#(xs)
   mergesort#(xs) -> mergesort1#(split(xs))
   mergesort1#(app(xs,ys)) -> mergesort#(ys)
   mergesort1#(app(xs,ys)) -> mergesort#(xs)
   mergesort1#(app(xs,ys)) -> merge#(mergesort(xs),mergesort(ys))
  TRS:
   leq(0(),x) -> tt()
   leq(s(x),0()) -> ff()
   leq(s(x),s(y)) -> leq(x,y)
   split(nil()) -> app(nil(),nil())
   split(cons(x,nil())) -> app(cons(x,nil()),nil())
   split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
   split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
   merge([](),xs) -> xs
   merge(xs,[]()) -> xs
   merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
   ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
   ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
   mergesort(xs) -> mergesort1(split(xs))
   mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
  ADG Processor:
   DPs:
    leq#(s(x),s(y)) -> leq#(x,y)
    split#(cons(x,cons(y,xs))) -> split#(xs)
    split#(cons(x,cons(y,xs))) -> split1#(x,y,split(xs))
    merge#(cons(x,xs),cons(y,ys)) -> leq#(x,y)
    merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
    ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys))
    ifmerge#(ff(),x,y,xs,ys) -> merge#(cons(x,xs),ys)
    mergesort#(xs) -> split#(xs)
    mergesort#(xs) -> mergesort1#(split(xs))
    mergesort1#(app(xs,ys)) -> mergesort#(ys)
    mergesort1#(app(xs,ys)) -> mergesort#(xs)
    mergesort1#(app(xs,ys)) -> merge#(mergesort(xs),mergesort(ys))
   TRS:
    leq(0(),x) -> tt()
    leq(s(x),0()) -> ff()
    leq(s(x),s(y)) -> leq(x,y)
    split(nil()) -> app(nil(),nil())
    split(cons(x,nil())) -> app(cons(x,nil()),nil())
    split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
    split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
    merge([](),xs) -> xs
    merge(xs,[]()) -> xs
    merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
    ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
    ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
    mergesort(xs) -> mergesort1(split(xs))
    mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
   graph:
    mergesort1#(app(xs,ys)) -> mergesort#(ys) ->
    mergesort#(xs) -> split#(xs)
    mergesort1#(app(xs,ys)) -> mergesort#(ys) ->
    mergesort#(xs) -> mergesort1#(split(xs))
    mergesort1#(app(xs,ys)) -> mergesort#(xs) ->
    mergesort#(xs) -> split#(xs)
    mergesort1#(app(xs,ys)) -> mergesort#(xs) ->
    mergesort#(xs) -> mergesort1#(split(xs))
    mergesort1#(app(xs,ys)) -> merge#(mergesort(xs),mergesort(ys)) ->
    merge#(cons(x,xs),cons(y,ys)) -> leq#(x,y)
    mergesort1#(app(xs,ys)) -> merge#(mergesort(xs),mergesort(ys)) ->
    merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
    mergesort#(xs) -> mergesort1#(split(xs)) ->
    mergesort1#(app(xs,ys)) -> mergesort#(ys)
    mergesort#(xs) -> mergesort1#(split(xs)) ->
    mergesort1#(app(xs,ys)) -> mergesort#(xs)
    mergesort#(xs) -> mergesort1#(split(xs)) ->
    mergesort1#(app(xs,ys)) -> merge#(mergesort(xs),mergesort(ys))
    mergesort#(xs) -> split#(xs) ->
    split#(cons(x,cons(y,xs))) -> split#(xs)
    mergesort#(xs) -> split#(xs) ->
    split#(cons(x,cons(y,xs))) -> split1#(x,y,split(xs))
    ifmerge#(ff(),x,y,xs,ys) -> merge#(cons(x,xs),ys) ->
    merge#(cons(x,xs),cons(y,ys)) -> leq#(x,y)
    ifmerge#(ff(),x,y,xs,ys) -> merge#(cons(x,xs),ys) ->
    merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
    ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys)) ->
    merge#(cons(x,xs),cons(y,ys)) -> leq#(x,y)
    ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys)) ->
    merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
    merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys) ->
    ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys))
    merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys) ->
    ifmerge#(ff(),x,y,xs,ys) -> merge#(cons(x,xs),ys)
    merge#(cons(x,xs),cons(y,ys)) -> leq#(x,y) ->
    leq#(s(x),s(y)) -> leq#(x,y)
    split#(cons(x,cons(y,xs))) -> split#(xs) ->
    split#(cons(x,cons(y,xs))) -> split#(xs)
    split#(cons(x,cons(y,xs))) -> split#(xs) ->
    split#(cons(x,cons(y,xs))) -> split1#(x,y,split(xs))
    leq#(s(x),s(y)) -> leq#(x,y) -> leq#(s(x),s(y)) -> leq#(x,y)
   Restore Modifier:
    DPs:
     leq#(s(x),s(y)) -> leq#(x,y)
     split#(cons(x,cons(y,xs))) -> split#(xs)
     split#(cons(x,cons(y,xs))) -> split1#(x,y,split(xs))
     merge#(cons(x,xs),cons(y,ys)) -> leq#(x,y)
     merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
     ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys))
     ifmerge#(ff(),x,y,xs,ys) -> merge#(cons(x,xs),ys)
     mergesort#(xs) -> split#(xs)
     mergesort#(xs) -> mergesort1#(split(xs))
     mergesort1#(app(xs,ys)) -> mergesort#(ys)
     mergesort1#(app(xs,ys)) -> mergesort#(xs)
     mergesort1#(app(xs,ys)) -> merge#(mergesort(xs),mergesort(ys))
    TRS:
     leq(0(),x) -> tt()
     leq(s(x),0()) -> ff()
     leq(s(x),s(y)) -> leq(x,y)
     split(nil()) -> app(nil(),nil())
     split(cons(x,nil())) -> app(cons(x,nil()),nil())
     split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
     split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
     merge([](),xs) -> xs
     merge(xs,[]()) -> xs
     merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
     ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
     ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
     mergesort(xs) -> mergesort1(split(xs))
     mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
    SCC Processor:
     #sccs: 4
     #rules: 8
     #arcs: 21/144
     DPs:
      mergesort1#(app(xs,ys)) -> mergesort#(ys)
      mergesort#(xs) -> mergesort1#(split(xs))
      mergesort1#(app(xs,ys)) -> mergesort#(xs)
     TRS:
      leq(0(),x) -> tt()
      leq(s(x),0()) -> ff()
      leq(s(x),s(y)) -> leq(x,y)
      split(nil()) -> app(nil(),nil())
      split(cons(x,nil())) -> app(cons(x,nil()),nil())
      split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
      split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
      merge([](),xs) -> xs
      merge(xs,[]()) -> xs
      merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
      ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
      ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
      mergesort(xs) -> mergesort1(split(xs))
      mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
     Open
     
     DPs:
      split#(cons(x,cons(y,xs))) -> split#(xs)
     TRS:
      leq(0(),x) -> tt()
      leq(s(x),0()) -> ff()
      leq(s(x),s(y)) -> leq(x,y)
      split(nil()) -> app(nil(),nil())
      split(cons(x,nil())) -> app(cons(x,nil()),nil())
      split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
      split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
      merge([](),xs) -> xs
      merge(xs,[]()) -> xs
      merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
      ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
      ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
      mergesort(xs) -> mergesort1(split(xs))
      mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
     Open
     
     DPs:
      merge#(cons(x,xs),cons(y,ys)) -> ifmerge#(leq(x,y),x,y,xs,ys)
      ifmerge#(ff(),x,y,xs,ys) -> merge#(cons(x,xs),ys)
      ifmerge#(tt(),x,y,xs,ys) -> merge#(xs,cons(y,ys))
     TRS:
      leq(0(),x) -> tt()
      leq(s(x),0()) -> ff()
      leq(s(x),s(y)) -> leq(x,y)
      split(nil()) -> app(nil(),nil())
      split(cons(x,nil())) -> app(cons(x,nil()),nil())
      split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
      split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
      merge([](),xs) -> xs
      merge(xs,[]()) -> xs
      merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
      ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
      ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
      mergesort(xs) -> mergesort1(split(xs))
      mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
     Open
     
     DPs:
      leq#(s(x),s(y)) -> leq#(x,y)
     TRS:
      leq(0(),x) -> tt()
      leq(s(x),0()) -> ff()
      leq(s(x),s(y)) -> leq(x,y)
      split(nil()) -> app(nil(),nil())
      split(cons(x,nil())) -> app(cons(x,nil()),nil())
      split(cons(x,cons(y,xs))) -> split1(x,y,split(xs))
      split1(x,y,app(xs,ys)) -> app(cons(x,xs),cons(y,ys))
      merge([](),xs) -> xs
      merge(xs,[]()) -> xs
      merge(cons(x,xs),cons(y,ys)) -> ifmerge(leq(x,y),x,y,xs,ys)
      ifmerge(tt(),x,y,xs,ys) -> cons(x,merge(xs,cons(y,ys)))
      ifmerge(ff(),x,y,xs,ys) -> cons(y,merge(cons(x,xs),ys))
      mergesort(xs) -> mergesort1(split(xs))
      mergesort1(app(xs,ys)) -> merge(mergesort(xs),mergesort(ys))
     Open