MAYBE

Problem:
 plus(x,y) -> ifPlus(isZero(x),x,inc(y))
 ifPlus(true(),x,y) -> p(y)
 ifPlus(false(),x,y) -> plus(p(x),y)
 times(x,y) -> timesIter(0(),x,y,0())
 timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
 ifTimes(true(),i,x,y,z) -> z
 ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
 isZero(0()) -> true()
 isZero(s(0())) -> false()
 isZero(s(s(x))) -> isZero(s(x))
 inc(0()) -> s(0())
 inc(s(x)) -> s(inc(x))
 inc(x) -> s(x)
 p(0()) -> 0()
 p(s(x)) -> x
 p(s(s(x))) -> s(p(s(x)))
 ge(x,0()) -> true()
 ge(0(),s(y)) -> false()
 ge(s(x),s(y)) -> ge(x,y)
 f0(0(),y,x) -> f1(x,y,x)
 f1(x,y,z) -> f2(x,y,z)
 f2(x,1(),z) -> f0(x,z,z)
 f0(x,y,z) -> d()
 f1(x,y,z) -> c()

Proof:
 DP Processor:
  DPs:
   plus#(x,y) -> inc#(y)
   plus#(x,y) -> isZero#(x)
   plus#(x,y) -> ifPlus#(isZero(x),x,inc(y))
   ifPlus#(true(),x,y) -> p#(y)
   ifPlus#(false(),x,y) -> p#(x)
   ifPlus#(false(),x,y) -> plus#(p(x),y)
   times#(x,y) -> timesIter#(0(),x,y,0())
   timesIter#(i,x,y,z) -> ge#(i,x)
   timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z)
   ifTimes#(false(),i,x,y,z) -> plus#(z,y)
   ifTimes#(false(),i,x,y,z) -> inc#(i)
   ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y))
   isZero#(s(s(x))) -> isZero#(s(x))
   inc#(s(x)) -> inc#(x)
   p#(s(s(x))) -> p#(s(x))
   ge#(s(x),s(y)) -> ge#(x,y)
   f0#(0(),y,x) -> f1#(x,y,x)
   f1#(x,y,z) -> f2#(x,y,z)
   f2#(x,1(),z) -> f0#(x,z,z)
  TRS:
   plus(x,y) -> ifPlus(isZero(x),x,inc(y))
   ifPlus(true(),x,y) -> p(y)
   ifPlus(false(),x,y) -> plus(p(x),y)
   times(x,y) -> timesIter(0(),x,y,0())
   timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
   ifTimes(true(),i,x,y,z) -> z
   ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
   isZero(0()) -> true()
   isZero(s(0())) -> false()
   isZero(s(s(x))) -> isZero(s(x))
   inc(0()) -> s(0())
   inc(s(x)) -> s(inc(x))
   inc(x) -> s(x)
   p(0()) -> 0()
   p(s(x)) -> x
   p(s(s(x))) -> s(p(s(x)))
   ge(x,0()) -> true()
   ge(0(),s(y)) -> false()
   ge(s(x),s(y)) -> ge(x,y)
   f0(0(),y,x) -> f1(x,y,x)
   f1(x,y,z) -> f2(x,y,z)
   f2(x,1(),z) -> f0(x,z,z)
   f0(x,y,z) -> d()
   f1(x,y,z) -> c()
  Usable Rule Processor:
   DPs:
    plus#(x,y) -> inc#(y)
    plus#(x,y) -> isZero#(x)
    plus#(x,y) -> ifPlus#(isZero(x),x,inc(y))
    ifPlus#(true(),x,y) -> p#(y)
    ifPlus#(false(),x,y) -> p#(x)
    ifPlus#(false(),x,y) -> plus#(p(x),y)
    times#(x,y) -> timesIter#(0(),x,y,0())
    timesIter#(i,x,y,z) -> ge#(i,x)
    timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z)
    ifTimes#(false(),i,x,y,z) -> plus#(z,y)
    ifTimes#(false(),i,x,y,z) -> inc#(i)
    ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y))
    isZero#(s(s(x))) -> isZero#(s(x))
    inc#(s(x)) -> inc#(x)
    p#(s(s(x))) -> p#(s(x))
    ge#(s(x),s(y)) -> ge#(x,y)
    f0#(0(),y,x) -> f1#(x,y,x)
    f1#(x,y,z) -> f2#(x,y,z)
    f2#(x,1(),z) -> f0#(x,z,z)
   TRS:
    f31(x,y) -> x
    f31(x,y) -> y
    inc(0()) -> s(0())
    inc(s(x)) -> s(inc(x))
    inc(x) -> s(x)
    isZero(0()) -> true()
    isZero(s(0())) -> false()
    isZero(s(s(x))) -> isZero(s(x))
    p(0()) -> 0()
    p(s(x)) -> x
    p(s(s(x))) -> s(p(s(x)))
    ge(x,0()) -> true()
    ge(0(),s(y)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
    plus(x,y) -> ifPlus(isZero(x),x,inc(y))
    ifPlus(true(),x,y) -> p(y)
    ifPlus(false(),x,y) -> plus(p(x),y)
   CDG Processor:
    DPs:
     plus#(x,y) -> inc#(y)
     plus#(x,y) -> isZero#(x)
     plus#(x,y) -> ifPlus#(isZero(x),x,inc(y))
     ifPlus#(true(),x,y) -> p#(y)
     ifPlus#(false(),x,y) -> p#(x)
     ifPlus#(false(),x,y) -> plus#(p(x),y)
     times#(x,y) -> timesIter#(0(),x,y,0())
     timesIter#(i,x,y,z) -> ge#(i,x)
     timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z)
     ifTimes#(false(),i,x,y,z) -> plus#(z,y)
     ifTimes#(false(),i,x,y,z) -> inc#(i)
     ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y))
     isZero#(s(s(x))) -> isZero#(s(x))
     inc#(s(x)) -> inc#(x)
     p#(s(s(x))) -> p#(s(x))
     ge#(s(x),s(y)) -> ge#(x,y)
     f0#(0(),y,x) -> f1#(x,y,x)
     f1#(x,y,z) -> f2#(x,y,z)
     f2#(x,1(),z) -> f0#(x,z,z)
    TRS:
     f31(x,y) -> x
     f31(x,y) -> y
     inc(0()) -> s(0())
     inc(s(x)) -> s(inc(x))
     inc(x) -> s(x)
     isZero(0()) -> true()
     isZero(s(0())) -> false()
     isZero(s(s(x))) -> isZero(s(x))
     p(0()) -> 0()
     p(s(x)) -> x
     p(s(s(x))) -> s(p(s(x)))
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     plus(x,y) -> ifPlus(isZero(x),x,inc(y))
     ifPlus(true(),x,y) -> p(y)
     ifPlus(false(),x,y) -> plus(p(x),y)
    graph:
     f2#(x,1(),z) -> f0#(x,z,z) -> f0#(0(),y,x) -> f1#(x,y,x)
     f1#(x,y,z) -> f2#(x,y,z) -> f2#(x,1(),z) -> f0#(x,z,z)
     f0#(0(),y,x) -> f1#(x,y,x) ->
     f1#(x,y,z) -> f2#(x,y,z)
     ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y)) ->
     timesIter#(i,x,y,z) -> ge#(i,x)
     ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y)) ->
     timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z)
     ifTimes#(false(),i,x,y,z) -> inc#(i) ->
     inc#(s(x)) -> inc#(x)
     ifTimes#(false(),i,x,y,z) -> plus#(z,y) ->
     plus#(x,y) -> inc#(y)
     ifTimes#(false(),i,x,y,z) -> plus#(z,y) ->
     plus#(x,y) -> isZero#(x)
     ifTimes#(false(),i,x,y,z) -> plus#(z,y) ->
     plus#(x,y) -> ifPlus#(isZero(x),x,inc(y))
     ge#(s(x),s(y)) -> ge#(x,y) ->
     ge#(s(x),s(y)) -> ge#(x,y)
     timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z) ->
     ifTimes#(false(),i,x,y,z) -> plus#(z,y)
     timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z) ->
     ifTimes#(false(),i,x,y,z) -> inc#(i)
     timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z) ->
     ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y))
     timesIter#(i,x,y,z) -> ge#(i,x) ->
     ge#(s(x),s(y)) -> ge#(x,y)
     times#(x,y) -> timesIter#(0(),x,y,0()) ->
     timesIter#(i,x,y,z) -> ge#(i,x)
     times#(x,y) -> timesIter#(0(),x,y,0()) ->
     timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z)
     p#(s(s(x))) -> p#(s(x)) -> p#(s(s(x))) -> p#(s(x))
     ifPlus#(false(),x,y) -> p#(x) -> p#(s(s(x))) -> p#(s(x))
     ifPlus#(false(),x,y) -> plus#(p(x),y) ->
     plus#(x,y) -> inc#(y)
     ifPlus#(false(),x,y) -> plus#(p(x),y) ->
     plus#(x,y) -> isZero#(x)
     ifPlus#(false(),x,y) -> plus#(p(x),y) ->
     plus#(x,y) -> ifPlus#(isZero(x),x,inc(y))
     ifPlus#(true(),x,y) -> p#(y) -> p#(s(s(x))) -> p#(s(x))
     isZero#(s(s(x))) -> isZero#(s(x)) -> isZero#(s(s(x))) -> isZero#(s(x))
     inc#(s(x)) -> inc#(x) -> inc#(s(x)) -> inc#(x)
     plus#(x,y) -> ifPlus#(isZero(x),x,inc(y)) ->
     ifPlus#(true(),x,y) -> p#(y)
     plus#(x,y) -> ifPlus#(isZero(x),x,inc(y)) ->
     ifPlus#(false(),x,y) -> p#(x)
     plus#(x,y) -> ifPlus#(isZero(x),x,inc(y)) ->
     ifPlus#(false(),x,y) -> plus#(p(x),y)
     plus#(x,y) -> isZero#(x) -> isZero#(s(s(x))) -> isZero#(s(x))
     plus#(x,y) -> inc#(y) -> inc#(s(x)) -> inc#(x)
    Restore Modifier:
     DPs:
      plus#(x,y) -> inc#(y)
      plus#(x,y) -> isZero#(x)
      plus#(x,y) -> ifPlus#(isZero(x),x,inc(y))
      ifPlus#(true(),x,y) -> p#(y)
      ifPlus#(false(),x,y) -> p#(x)
      ifPlus#(false(),x,y) -> plus#(p(x),y)
      times#(x,y) -> timesIter#(0(),x,y,0())
      timesIter#(i,x,y,z) -> ge#(i,x)
      timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z)
      ifTimes#(false(),i,x,y,z) -> plus#(z,y)
      ifTimes#(false(),i,x,y,z) -> inc#(i)
      ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y))
      isZero#(s(s(x))) -> isZero#(s(x))
      inc#(s(x)) -> inc#(x)
      p#(s(s(x))) -> p#(s(x))
      ge#(s(x),s(y)) -> ge#(x,y)
      f0#(0(),y,x) -> f1#(x,y,x)
      f1#(x,y,z) -> f2#(x,y,z)
      f2#(x,1(),z) -> f0#(x,z,z)
     TRS:
      plus(x,y) -> ifPlus(isZero(x),x,inc(y))
      ifPlus(true(),x,y) -> p(y)
      ifPlus(false(),x,y) -> plus(p(x),y)
      times(x,y) -> timesIter(0(),x,y,0())
      timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
      ifTimes(true(),i,x,y,z) -> z
      ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
      isZero(0()) -> true()
      isZero(s(0())) -> false()
      isZero(s(s(x))) -> isZero(s(x))
      inc(0()) -> s(0())
      inc(s(x)) -> s(inc(x))
      inc(x) -> s(x)
      p(0()) -> 0()
      p(s(x)) -> x
      p(s(s(x))) -> s(p(s(x)))
      ge(x,0()) -> true()
      ge(0(),s(y)) -> false()
      ge(s(x),s(y)) -> ge(x,y)
      f0(0(),y,x) -> f1(x,y,x)
      f1(x,y,z) -> f2(x,y,z)
      f2(x,1(),z) -> f0(x,z,z)
      f0(x,y,z) -> d()
      f1(x,y,z) -> c()
     SCC Processor:
      #sccs: 7
      #rules: 11
      #arcs: 29/361
      DPs:
       ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y))
       timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z)
      TRS:
       plus(x,y) -> ifPlus(isZero(x),x,inc(y))
       ifPlus(true(),x,y) -> p(y)
       ifPlus(false(),x,y) -> plus(p(x),y)
       times(x,y) -> timesIter(0(),x,y,0())
       timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
       ifTimes(true(),i,x,y,z) -> z
       ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
       isZero(0()) -> true()
       isZero(s(0())) -> false()
       isZero(s(s(x))) -> isZero(s(x))
       inc(0()) -> s(0())
       inc(s(x)) -> s(inc(x))
       inc(x) -> s(x)
       p(0()) -> 0()
       p(s(x)) -> x
       p(s(s(x))) -> s(p(s(x)))
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       f0(0(),y,x) -> f1(x,y,x)
       f1(x,y,z) -> f2(x,y,z)
       f2(x,1(),z) -> f0(x,z,z)
       f0(x,y,z) -> d()
       f1(x,y,z) -> c()
      Open
      
      DPs:
       ge#(s(x),s(y)) -> ge#(x,y)
      TRS:
       plus(x,y) -> ifPlus(isZero(x),x,inc(y))
       ifPlus(true(),x,y) -> p(y)
       ifPlus(false(),x,y) -> plus(p(x),y)
       times(x,y) -> timesIter(0(),x,y,0())
       timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
       ifTimes(true(),i,x,y,z) -> z
       ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
       isZero(0()) -> true()
       isZero(s(0())) -> false()
       isZero(s(s(x))) -> isZero(s(x))
       inc(0()) -> s(0())
       inc(s(x)) -> s(inc(x))
       inc(x) -> s(x)
       p(0()) -> 0()
       p(s(x)) -> x
       p(s(s(x))) -> s(p(s(x)))
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       f0(0(),y,x) -> f1(x,y,x)
       f1(x,y,z) -> f2(x,y,z)
       f2(x,1(),z) -> f0(x,z,z)
       f0(x,y,z) -> d()
       f1(x,y,z) -> c()
      Open
      
      DPs:
       plus#(x,y) -> ifPlus#(isZero(x),x,inc(y))
       ifPlus#(false(),x,y) -> plus#(p(x),y)
      TRS:
       plus(x,y) -> ifPlus(isZero(x),x,inc(y))
       ifPlus(true(),x,y) -> p(y)
       ifPlus(false(),x,y) -> plus(p(x),y)
       times(x,y) -> timesIter(0(),x,y,0())
       timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
       ifTimes(true(),i,x,y,z) -> z
       ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
       isZero(0()) -> true()
       isZero(s(0())) -> false()
       isZero(s(s(x))) -> isZero(s(x))
       inc(0()) -> s(0())
       inc(s(x)) -> s(inc(x))
       inc(x) -> s(x)
       p(0()) -> 0()
       p(s(x)) -> x
       p(s(s(x))) -> s(p(s(x)))
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       f0(0(),y,x) -> f1(x,y,x)
       f1(x,y,z) -> f2(x,y,z)
       f2(x,1(),z) -> f0(x,z,z)
       f0(x,y,z) -> d()
       f1(x,y,z) -> c()
      Open
      
      DPs:
       p#(s(s(x))) -> p#(s(x))
      TRS:
       plus(x,y) -> ifPlus(isZero(x),x,inc(y))
       ifPlus(true(),x,y) -> p(y)
       ifPlus(false(),x,y) -> plus(p(x),y)
       times(x,y) -> timesIter(0(),x,y,0())
       timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
       ifTimes(true(),i,x,y,z) -> z
       ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
       isZero(0()) -> true()
       isZero(s(0())) -> false()
       isZero(s(s(x))) -> isZero(s(x))
       inc(0()) -> s(0())
       inc(s(x)) -> s(inc(x))
       inc(x) -> s(x)
       p(0()) -> 0()
       p(s(x)) -> x
       p(s(s(x))) -> s(p(s(x)))
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       f0(0(),y,x) -> f1(x,y,x)
       f1(x,y,z) -> f2(x,y,z)
       f2(x,1(),z) -> f0(x,z,z)
       f0(x,y,z) -> d()
       f1(x,y,z) -> c()
      Open
      
      DPs:
       isZero#(s(s(x))) -> isZero#(s(x))
      TRS:
       plus(x,y) -> ifPlus(isZero(x),x,inc(y))
       ifPlus(true(),x,y) -> p(y)
       ifPlus(false(),x,y) -> plus(p(x),y)
       times(x,y) -> timesIter(0(),x,y,0())
       timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
       ifTimes(true(),i,x,y,z) -> z
       ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
       isZero(0()) -> true()
       isZero(s(0())) -> false()
       isZero(s(s(x))) -> isZero(s(x))
       inc(0()) -> s(0())
       inc(s(x)) -> s(inc(x))
       inc(x) -> s(x)
       p(0()) -> 0()
       p(s(x)) -> x
       p(s(s(x))) -> s(p(s(x)))
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       f0(0(),y,x) -> f1(x,y,x)
       f1(x,y,z) -> f2(x,y,z)
       f2(x,1(),z) -> f0(x,z,z)
       f0(x,y,z) -> d()
       f1(x,y,z) -> c()
      Open
      
      DPs:
       inc#(s(x)) -> inc#(x)
      TRS:
       plus(x,y) -> ifPlus(isZero(x),x,inc(y))
       ifPlus(true(),x,y) -> p(y)
       ifPlus(false(),x,y) -> plus(p(x),y)
       times(x,y) -> timesIter(0(),x,y,0())
       timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
       ifTimes(true(),i,x,y,z) -> z
       ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
       isZero(0()) -> true()
       isZero(s(0())) -> false()
       isZero(s(s(x))) -> isZero(s(x))
       inc(0()) -> s(0())
       inc(s(x)) -> s(inc(x))
       inc(x) -> s(x)
       p(0()) -> 0()
       p(s(x)) -> x
       p(s(s(x))) -> s(p(s(x)))
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       f0(0(),y,x) -> f1(x,y,x)
       f1(x,y,z) -> f2(x,y,z)
       f2(x,1(),z) -> f0(x,z,z)
       f0(x,y,z) -> d()
       f1(x,y,z) -> c()
      Open
      
      DPs:
       f2#(x,1(),z) -> f0#(x,z,z)
       f0#(0(),y,x) -> f1#(x,y,x)
       f1#(x,y,z) -> f2#(x,y,z)
      TRS:
       plus(x,y) -> ifPlus(isZero(x),x,inc(y))
       ifPlus(true(),x,y) -> p(y)
       ifPlus(false(),x,y) -> plus(p(x),y)
       times(x,y) -> timesIter(0(),x,y,0())
       timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
       ifTimes(true(),i,x,y,z) -> z
       ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
       isZero(0()) -> true()
       isZero(s(0())) -> false()
       isZero(s(s(x))) -> isZero(s(x))
       inc(0()) -> s(0())
       inc(s(x)) -> s(inc(x))
       inc(x) -> s(x)
       p(0()) -> 0()
       p(s(x)) -> x
       p(s(s(x))) -> s(p(s(x)))
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       f0(0(),y,x) -> f1(x,y,x)
       f1(x,y,z) -> f2(x,y,z)
       f2(x,1(),z) -> f0(x,z,z)
       f0(x,y,z) -> d()
       f1(x,y,z) -> c()
      Open