MAYBE

Problem:
 double(x) -> permute(x,x,a())
 permute(x,y,a()) -> permute(isZero(x),x,b())
 permute(false(),x,b()) -> permute(ack(x,x),p(x),c())
 permute(true(),x,b()) -> 0()
 permute(y,x,c()) -> s(s(permute(x,y,a())))
 p(0()) -> 0()
 p(s(x)) -> x
 ack(0(),x) -> plus(x,s(0()))
 ack(s(x),0()) -> ack(x,s(0()))
 ack(s(x),s(y)) -> ack(x,ack(s(x),y))
 plus(0(),y) -> y
 plus(s(x),y) -> plus(x,s(y))
 plus(x,s(s(y))) -> s(plus(s(x),y))
 plus(x,s(0())) -> s(x)
 plus(x,0()) -> x
 isZero(0()) -> true()
 isZero(s(x)) -> false()

Proof:
 DP Processor:
  DPs:
   double#(x) -> permute#(x,x,a())
   permute#(x,y,a()) -> isZero#(x)
   permute#(x,y,a()) -> permute#(isZero(x),x,b())
   permute#(false(),x,b()) -> p#(x)
   permute#(false(),x,b()) -> ack#(x,x)
   permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
   permute#(y,x,c()) -> permute#(x,y,a())
   ack#(0(),x) -> plus#(x,s(0()))
   ack#(s(x),0()) -> ack#(x,s(0()))
   ack#(s(x),s(y)) -> ack#(s(x),y)
   ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
   plus#(s(x),y) -> plus#(x,s(y))
   plus#(x,s(s(y))) -> plus#(s(x),y)
  TRS:
   double(x) -> permute(x,x,a())
   permute(x,y,a()) -> permute(isZero(x),x,b())
   permute(false(),x,b()) -> permute(ack(x,x),p(x),c())
   permute(true(),x,b()) -> 0()
   permute(y,x,c()) -> s(s(permute(x,y,a())))
   p(0()) -> 0()
   p(s(x)) -> x
   ack(0(),x) -> plus(x,s(0()))
   ack(s(x),0()) -> ack(x,s(0()))
   ack(s(x),s(y)) -> ack(x,ack(s(x),y))
   plus(0(),y) -> y
   plus(s(x),y) -> plus(x,s(y))
   plus(x,s(s(y))) -> s(plus(s(x),y))
   plus(x,s(0())) -> s(x)
   plus(x,0()) -> x
   isZero(0()) -> true()
   isZero(s(x)) -> false()
  Usable Rule Processor:
   DPs:
    double#(x) -> permute#(x,x,a())
    permute#(x,y,a()) -> isZero#(x)
    permute#(x,y,a()) -> permute#(isZero(x),x,b())
    permute#(false(),x,b()) -> p#(x)
    permute#(false(),x,b()) -> ack#(x,x)
    permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
    permute#(y,x,c()) -> permute#(x,y,a())
    ack#(0(),x) -> plus#(x,s(0()))
    ack#(s(x),0()) -> ack#(x,s(0()))
    ack#(s(x),s(y)) -> ack#(s(x),y)
    ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
    plus#(s(x),y) -> plus#(x,s(y))
    plus#(x,s(s(y))) -> plus#(s(x),y)
   TRS:
    f19(x,y) -> x
    f19(x,y) -> y
    isZero(0()) -> true()
    isZero(s(x)) -> false()
    p(0()) -> 0()
    p(s(x)) -> x
    ack(0(),x) -> plus(x,s(0()))
    ack(s(x),0()) -> ack(x,s(0()))
    ack(s(x),s(y)) -> ack(x,ack(s(x),y))
    plus(0(),y) -> y
    plus(s(x),y) -> plus(x,s(y))
    plus(x,s(0())) -> s(x)
    plus(x,s(s(y))) -> s(plus(s(x),y))
    plus(x,0()) -> x
   TDG Processor:
    DPs:
     double#(x) -> permute#(x,x,a())
     permute#(x,y,a()) -> isZero#(x)
     permute#(x,y,a()) -> permute#(isZero(x),x,b())
     permute#(false(),x,b()) -> p#(x)
     permute#(false(),x,b()) -> ack#(x,x)
     permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
     permute#(y,x,c()) -> permute#(x,y,a())
     ack#(0(),x) -> plus#(x,s(0()))
     ack#(s(x),0()) -> ack#(x,s(0()))
     ack#(s(x),s(y)) -> ack#(s(x),y)
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
     plus#(s(x),y) -> plus#(x,s(y))
     plus#(x,s(s(y))) -> plus#(s(x),y)
    TRS:
     f19(x,y) -> x
     f19(x,y) -> y
     isZero(0()) -> true()
     isZero(s(x)) -> false()
     p(0()) -> 0()
     p(s(x)) -> x
     ack(0(),x) -> plus(x,s(0()))
     ack(s(x),0()) -> ack(x,s(0()))
     ack(s(x),s(y)) -> ack(x,ack(s(x),y))
     plus(0(),y) -> y
     plus(s(x),y) -> plus(x,s(y))
     plus(x,s(0())) -> s(x)
     plus(x,s(s(y))) -> s(plus(s(x),y))
     plus(x,0()) -> x
    graph:
     plus#(s(x),y) -> plus#(x,s(y)) ->
     plus#(x,s(s(y))) -> plus#(s(x),y)
     plus#(s(x),y) -> plus#(x,s(y)) ->
     plus#(s(x),y) -> plus#(x,s(y))
     plus#(x,s(s(y))) -> plus#(s(x),y) ->
     plus#(x,s(s(y))) -> plus#(s(x),y)
     plus#(x,s(s(y))) -> plus#(s(x),y) ->
     plus#(s(x),y) -> plus#(x,s(y))
     ack#(s(x),s(y)) -> ack#(s(x),y) ->
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
     ack#(s(x),s(y)) -> ack#(s(x),y) ->
     ack#(s(x),s(y)) -> ack#(s(x),y)
     ack#(s(x),s(y)) -> ack#(s(x),y) ->
     ack#(s(x),0()) -> ack#(x,s(0()))
     ack#(s(x),s(y)) -> ack#(s(x),y) ->
     ack#(0(),x) -> plus#(x,s(0()))
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
     ack#(s(x),s(y)) -> ack#(s(x),y)
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
     ack#(s(x),0()) -> ack#(x,s(0()))
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
     ack#(0(),x) -> plus#(x,s(0()))
     ack#(s(x),0()) -> ack#(x,s(0())) ->
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
     ack#(s(x),0()) -> ack#(x,s(0())) ->
     ack#(s(x),s(y)) -> ack#(s(x),y)
     ack#(s(x),0()) -> ack#(x,s(0())) ->
     ack#(s(x),0()) -> ack#(x,s(0()))
     ack#(s(x),0()) -> ack#(x,s(0())) ->
     ack#(0(),x) -> plus#(x,s(0()))
     ack#(0(),x) -> plus#(x,s(0())) ->
     plus#(x,s(s(y))) -> plus#(s(x),y)
     ack#(0(),x) -> plus#(x,s(0())) ->
     plus#(s(x),y) -> plus#(x,s(y))
     permute#(false(),x,b()) -> ack#(x,x) ->
     ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
     permute#(false(),x,b()) -> ack#(x,x) ->
     ack#(s(x),s(y)) -> ack#(s(x),y)
     permute#(false(),x,b()) -> ack#(x,x) ->
     ack#(s(x),0()) -> ack#(x,s(0()))
     permute#(false(),x,b()) -> ack#(x,x) ->
     ack#(0(),x) -> plus#(x,s(0()))
     permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c()) ->
     permute#(y,x,c()) -> permute#(x,y,a())
     permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c()) ->
     permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
     permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c()) ->
     permute#(false(),x,b()) -> ack#(x,x)
     permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c()) ->
     permute#(false(),x,b()) -> p#(x)
     permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c()) ->
     permute#(x,y,a()) -> permute#(isZero(x),x,b())
     permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c()) ->
     permute#(x,y,a()) -> isZero#(x)
     permute#(y,x,c()) -> permute#(x,y,a()) ->
     permute#(y,x,c()) -> permute#(x,y,a())
     permute#(y,x,c()) -> permute#(x,y,a()) ->
     permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
     permute#(y,x,c()) -> permute#(x,y,a()) ->
     permute#(false(),x,b()) -> ack#(x,x)
     permute#(y,x,c()) -> permute#(x,y,a()) ->
     permute#(false(),x,b()) -> p#(x)
     permute#(y,x,c()) -> permute#(x,y,a()) ->
     permute#(x,y,a()) -> permute#(isZero(x),x,b())
     permute#(y,x,c()) -> permute#(x,y,a()) ->
     permute#(x,y,a()) -> isZero#(x)
     permute#(x,y,a()) -> permute#(isZero(x),x,b()) ->
     permute#(y,x,c()) -> permute#(x,y,a())
     permute#(x,y,a()) -> permute#(isZero(x),x,b()) ->
     permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
     permute#(x,y,a()) -> permute#(isZero(x),x,b()) ->
     permute#(false(),x,b()) -> ack#(x,x)
     permute#(x,y,a()) -> permute#(isZero(x),x,b()) ->
     permute#(false(),x,b()) -> p#(x)
     permute#(x,y,a()) -> permute#(isZero(x),x,b()) ->
     permute#(x,y,a()) -> permute#(isZero(x),x,b())
     permute#(x,y,a()) -> permute#(isZero(x),x,b()) ->
     permute#(x,y,a()) -> isZero#(x)
     double#(x) -> permute#(x,x,a()) ->
     permute#(y,x,c()) -> permute#(x,y,a())
     double#(x) -> permute#(x,x,a()) ->
     permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
     double#(x) -> permute#(x,x,a()) ->
     permute#(false(),x,b()) -> ack#(x,x)
     double#(x) -> permute#(x,x,a()) ->
     permute#(false(),x,b()) -> p#(x)
     double#(x) -> permute#(x,x,a()) ->
     permute#(x,y,a()) -> permute#(isZero(x),x,b())
     double#(x) -> permute#(x,x,a()) -> permute#(x,y,a()) -> isZero#(x)
    EDG Processor:
     DPs:
      double#(x) -> permute#(x,x,a())
      permute#(x,y,a()) -> isZero#(x)
      permute#(x,y,a()) -> permute#(isZero(x),x,b())
      permute#(false(),x,b()) -> p#(x)
      permute#(false(),x,b()) -> ack#(x,x)
      permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
      permute#(y,x,c()) -> permute#(x,y,a())
      ack#(0(),x) -> plus#(x,s(0()))
      ack#(s(x),0()) -> ack#(x,s(0()))
      ack#(s(x),s(y)) -> ack#(s(x),y)
      ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
      plus#(s(x),y) -> plus#(x,s(y))
      plus#(x,s(s(y))) -> plus#(s(x),y)
     TRS:
      f19(x,y) -> x
      f19(x,y) -> y
      isZero(0()) -> true()
      isZero(s(x)) -> false()
      p(0()) -> 0()
      p(s(x)) -> x
      ack(0(),x) -> plus(x,s(0()))
      ack(s(x),0()) -> ack(x,s(0()))
      ack(s(x),s(y)) -> ack(x,ack(s(x),y))
      plus(0(),y) -> y
      plus(s(x),y) -> plus(x,s(y))
      plus(x,s(0())) -> s(x)
      plus(x,s(s(y))) -> s(plus(s(x),y))
      plus(x,0()) -> x
     graph:
      plus#(s(x),y) -> plus#(x,s(y)) ->
      plus#(s(x),y) -> plus#(x,s(y))
      plus#(s(x),y) -> plus#(x,s(y)) ->
      plus#(x,s(s(y))) -> plus#(s(x),y)
      plus#(x,s(s(y))) -> plus#(s(x),y) ->
      plus#(s(x),y) -> plus#(x,s(y))
      plus#(x,s(s(y))) -> plus#(s(x),y) ->
      plus#(x,s(s(y))) -> plus#(s(x),y)
      ack#(s(x),s(y)) -> ack#(s(x),y) ->
      ack#(s(x),0()) -> ack#(x,s(0()))
      ack#(s(x),s(y)) -> ack#(s(x),y) ->
      ack#(s(x),s(y)) -> ack#(s(x),y)
      ack#(s(x),s(y)) -> ack#(s(x),y) ->
      ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
      ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
      ack#(0(),x) -> plus#(x,s(0()))
      ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
      ack#(s(x),0()) -> ack#(x,s(0()))
      ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
      ack#(s(x),s(y)) -> ack#(s(x),y)
      ack#(s(x),s(y)) -> ack#(x,ack(s(x),y)) ->
      ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
      ack#(s(x),0()) -> ack#(x,s(0())) ->
      ack#(0(),x) -> plus#(x,s(0()))
      ack#(s(x),0()) -> ack#(x,s(0())) ->
      ack#(s(x),s(y)) -> ack#(s(x),y)
      ack#(s(x),0()) -> ack#(x,s(0())) ->
      ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
      ack#(0(),x) -> plus#(x,s(0())) ->
      plus#(s(x),y) -> plus#(x,s(y))
      permute#(false(),x,b()) -> ack#(x,x) ->
      ack#(0(),x) -> plus#(x,s(0()))
      permute#(false(),x,b()) -> ack#(x,x) ->
      ack#(s(x),0()) -> ack#(x,s(0()))
      permute#(false(),x,b()) -> ack#(x,x) ->
      ack#(s(x),s(y)) -> ack#(s(x),y)
      permute#(false(),x,b()) -> ack#(x,x) ->
      ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
      permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c()) ->
      permute#(y,x,c()) -> permute#(x,y,a())
      permute#(y,x,c()) -> permute#(x,y,a()) ->
      permute#(x,y,a()) -> isZero#(x)
      permute#(y,x,c()) -> permute#(x,y,a()) ->
      permute#(x,y,a()) -> permute#(isZero(x),x,b())
      permute#(x,y,a()) -> permute#(isZero(x),x,b()) ->
      permute#(false(),x,b()) -> p#(x)
      permute#(x,y,a()) -> permute#(isZero(x),x,b()) ->
      permute#(false(),x,b()) -> ack#(x,x)
      permute#(x,y,a()) -> permute#(isZero(x),x,b()) ->
      permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
      double#(x) -> permute#(x,x,a()) ->
      permute#(x,y,a()) -> isZero#(x)
      double#(x) -> permute#(x,x,a()) -> permute#(x,y,a()) -> permute#(isZero(x),x,b())
     Restore Modifier:
      DPs:
       double#(x) -> permute#(x,x,a())
       permute#(x,y,a()) -> isZero#(x)
       permute#(x,y,a()) -> permute#(isZero(x),x,b())
       permute#(false(),x,b()) -> p#(x)
       permute#(false(),x,b()) -> ack#(x,x)
       permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
       permute#(y,x,c()) -> permute#(x,y,a())
       ack#(0(),x) -> plus#(x,s(0()))
       ack#(s(x),0()) -> ack#(x,s(0()))
       ack#(s(x),s(y)) -> ack#(s(x),y)
       ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
       plus#(s(x),y) -> plus#(x,s(y))
       plus#(x,s(s(y))) -> plus#(s(x),y)
      TRS:
       double(x) -> permute(x,x,a())
       permute(x,y,a()) -> permute(isZero(x),x,b())
       permute(false(),x,b()) -> permute(ack(x,x),p(x),c())
       permute(true(),x,b()) -> 0()
       permute(y,x,c()) -> s(s(permute(x,y,a())))
       p(0()) -> 0()
       p(s(x)) -> x
       ack(0(),x) -> plus(x,s(0()))
       ack(s(x),0()) -> ack(x,s(0()))
       ack(s(x),s(y)) -> ack(x,ack(s(x),y))
       plus(0(),y) -> y
       plus(s(x),y) -> plus(x,s(y))
       plus(x,s(s(y))) -> s(plus(s(x),y))
       plus(x,s(0())) -> s(x)
       plus(x,0()) -> x
       isZero(0()) -> true()
       isZero(s(x)) -> false()
      SCC Processor:
       #sccs: 3
       #rules: 8
       #arcs: 27/169
       DPs:
        permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
        permute#(y,x,c()) -> permute#(x,y,a())
        permute#(x,y,a()) -> permute#(isZero(x),x,b())
       TRS:
        double(x) -> permute(x,x,a())
        permute(x,y,a()) -> permute(isZero(x),x,b())
        permute(false(),x,b()) -> permute(ack(x,x),p(x),c())
        permute(true(),x,b()) -> 0()
        permute(y,x,c()) -> s(s(permute(x,y,a())))
        p(0()) -> 0()
        p(s(x)) -> x
        ack(0(),x) -> plus(x,s(0()))
        ack(s(x),0()) -> ack(x,s(0()))
        ack(s(x),s(y)) -> ack(x,ack(s(x),y))
        plus(0(),y) -> y
        plus(s(x),y) -> plus(x,s(y))
        plus(x,s(s(y))) -> s(plus(s(x),y))
        plus(x,s(0())) -> s(x)
        plus(x,0()) -> x
        isZero(0()) -> true()
        isZero(s(x)) -> false()
       Open
       
       DPs:
        ack#(s(x),s(y)) -> ack#(s(x),y)
        ack#(s(x),s(y)) -> ack#(x,ack(s(x),y))
        ack#(s(x),0()) -> ack#(x,s(0()))
       TRS:
        double(x) -> permute(x,x,a())
        permute(x,y,a()) -> permute(isZero(x),x,b())
        permute(false(),x,b()) -> permute(ack(x,x),p(x),c())
        permute(true(),x,b()) -> 0()
        permute(y,x,c()) -> s(s(permute(x,y,a())))
        p(0()) -> 0()
        p(s(x)) -> x
        ack(0(),x) -> plus(x,s(0()))
        ack(s(x),0()) -> ack(x,s(0()))
        ack(s(x),s(y)) -> ack(x,ack(s(x),y))
        plus(0(),y) -> y
        plus(s(x),y) -> plus(x,s(y))
        plus(x,s(s(y))) -> s(plus(s(x),y))
        plus(x,s(0())) -> s(x)
        plus(x,0()) -> x
        isZero(0()) -> true()
        isZero(s(x)) -> false()
       Open
       
       DPs:
        plus#(s(x),y) -> plus#(x,s(y))
        plus#(x,s(s(y))) -> plus#(s(x),y)
       TRS:
        double(x) -> permute(x,x,a())
        permute(x,y,a()) -> permute(isZero(x),x,b())
        permute(false(),x,b()) -> permute(ack(x,x),p(x),c())
        permute(true(),x,b()) -> 0()
        permute(y,x,c()) -> s(s(permute(x,y,a())))
        p(0()) -> 0()
        p(s(x)) -> x
        ack(0(),x) -> plus(x,s(0()))
        ack(s(x),0()) -> ack(x,s(0()))
        ack(s(x),s(y)) -> ack(x,ack(s(x),y))
        plus(0(),y) -> y
        plus(s(x),y) -> plus(x,s(y))
        plus(x,s(s(y))) -> s(plus(s(x),y))
        plus(x,s(0())) -> s(x)
        plus(x,0()) -> x
        isZero(0()) -> true()
        isZero(s(x)) -> false()
       Open