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()
  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:
    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()
   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)
   SCC Processor:
    #sccs: 3
    #rules: 8
    #arcs: 46/169
    DPs:
     permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
     permute#(x,y,a()) -> permute#(isZero(x),x,b())
     permute#(y,x,c()) -> permute#(x,y,a())
    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()
    EDG Processor:
     DPs:
      permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
      permute#(x,y,a()) -> permute#(isZero(x),x,b())
      permute#(y,x,c()) -> permute#(x,y,a())
     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()
     graph:
      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()) -> permute#(isZero(x),x,b())
      permute#(x,y,a()) -> permute#(isZero(x),x,b()) ->
      permute#(false(),x,b()) -> permute#(ack(x,x),p(x),c())
     Open
    
    DPs:
     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))
    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()
    Subterm Criterion Processor:
     simple projection:
      pi(ack#) = 0
     problem:
      DPs:
       ack#(s(x),s(y)) -> ack#(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()
     Subterm Criterion Processor:
      simple projection:
       pi(ack#) = 1
      problem:
       DPs:
        
       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()
      Qed
    
    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()
    Usable Rule Processor:
     DPs:
      plus#(s(x),y) -> plus#(x,s(y))
      plus#(x,s(s(y))) -> plus#(s(x),y)
     TRS:
      
     Semantic Labeling Processor:
      dimension: 1
      usable rules:
       
      interpretation:
       [s](x0) = x0 + 1
       labeled:
        plus#
       usable (for model):
        plus#
        s
       argument filtering:
        pi(s) = 0
        pi(plus#) = []
      precedence:
       plus# ~ s
      problem:
       DPs:
        plus#(s(x),y) -> plus#(x,s(y))
       TRS:
        
      Restore Modifier:
       DPs:
        plus#(s(x),y) -> plus#(x,s(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()
       Subterm Criterion Processor:
        simple projection:
         pi(plus#) = 0
        problem:
         DPs:
          
         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()
        Qed