MAYBE

Problem:
 f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,s(y),z)
 f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,y,s(z))
 plus(n,0()) -> n
 plus(n,s(m)) -> s(plus(n,m))
 gt(0(),v) -> false()
 gt(s(u),0()) -> true()
 gt(s(u),s(v)) -> gt(u,v)

Proof:
 DP Processor:
  DPs:
   f#(true(),x,y,z) -> plus#(y,z)
   f#(true(),x,y,z) -> gt#(x,plus(y,z))
   f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,s(y),z)
   f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,y,s(z))
   plus#(n,s(m)) -> plus#(n,m)
   gt#(s(u),s(v)) -> gt#(u,v)
  TRS:
   f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,s(y),z)
   f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,y,s(z))
   plus(n,0()) -> n
   plus(n,s(m)) -> s(plus(n,m))
   gt(0(),v) -> false()
   gt(s(u),0()) -> true()
   gt(s(u),s(v)) -> gt(u,v)
  Usable Rule Processor:
   DPs:
    f#(true(),x,y,z) -> plus#(y,z)
    f#(true(),x,y,z) -> gt#(x,plus(y,z))
    f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,s(y),z)
    f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,y,s(z))
    plus#(n,s(m)) -> plus#(n,m)
    gt#(s(u),s(v)) -> gt#(u,v)
   TRS:
    f10(x,y) -> x
    f10(x,y) -> y
    plus(n,0()) -> n
    plus(n,s(m)) -> s(plus(n,m))
    gt(0(),v) -> false()
    gt(s(u),0()) -> true()
    gt(s(u),s(v)) -> gt(u,v)
   ADG Processor:
    DPs:
     f#(true(),x,y,z) -> plus#(y,z)
     f#(true(),x,y,z) -> gt#(x,plus(y,z))
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,s(y),z)
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,y,s(z))
     plus#(n,s(m)) -> plus#(n,m)
     gt#(s(u),s(v)) -> gt#(u,v)
    TRS:
     f10(x,y) -> x
     f10(x,y) -> y
     plus(n,0()) -> n
     plus(n,s(m)) -> s(plus(n,m))
     gt(0(),v) -> false()
     gt(s(u),0()) -> true()
     gt(s(u),s(v)) -> gt(u,v)
    graph:
     gt#(s(u),s(v)) -> gt#(u,v) -> gt#(s(u),s(v)) -> gt#(u,v)
     plus#(n,s(m)) -> plus#(n,m) -> plus#(n,s(m)) -> plus#(n,m)
     f#(true(),x,y,z) -> gt#(x,plus(y,z)) ->
     gt#(s(u),s(v)) -> gt#(u,v)
     f#(true(),x,y,z) -> plus#(y,z) ->
     plus#(n,s(m)) -> plus#(n,m)
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,s(y),z) ->
     f#(true(),x,y,z) -> plus#(y,z)
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,s(y),z) ->
     f#(true(),x,y,z) -> gt#(x,plus(y,z))
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,s(y),z) ->
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,s(y),z)
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,s(y),z) ->
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,y,s(z))
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,y,s(z)) ->
     f#(true(),x,y,z) -> plus#(y,z)
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,y,s(z)) ->
     f#(true(),x,y,z) -> gt#(x,plus(y,z))
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,y,s(z)) ->
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,s(y),z)
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,y,s(z)) ->
     f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,y,s(z))
    Restore Modifier:
     DPs:
      f#(true(),x,y,z) -> plus#(y,z)
      f#(true(),x,y,z) -> gt#(x,plus(y,z))
      f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,s(y),z)
      f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,y,s(z))
      plus#(n,s(m)) -> plus#(n,m)
      gt#(s(u),s(v)) -> gt#(u,v)
     TRS:
      f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,s(y),z)
      f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,y,s(z))
      plus(n,0()) -> n
      plus(n,s(m)) -> s(plus(n,m))
      gt(0(),v) -> false()
      gt(s(u),0()) -> true()
      gt(s(u),s(v)) -> gt(u,v)
     SCC Processor:
      #sccs: 3
      #rules: 4
      #arcs: 12/36
      DPs:
       f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,s(y),z)
       f#(true(),x,y,z) -> f#(gt(x,plus(y,z)),x,y,s(z))
      TRS:
       f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,s(y),z)
       f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,y,s(z))
       plus(n,0()) -> n
       plus(n,s(m)) -> s(plus(n,m))
       gt(0(),v) -> false()
       gt(s(u),0()) -> true()
       gt(s(u),s(v)) -> gt(u,v)
      Open
      
      DPs:
       plus#(n,s(m)) -> plus#(n,m)
      TRS:
       f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,s(y),z)
       f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,y,s(z))
       plus(n,0()) -> n
       plus(n,s(m)) -> s(plus(n,m))
       gt(0(),v) -> false()
       gt(s(u),0()) -> true()
       gt(s(u),s(v)) -> gt(u,v)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [plus#](x0, x1) = x1 + 1,
        
        [false] = 1,
        
        [0] = 0,
        
        [s](x0) = x0 + 1,
        
        [gt](x0, x1) = 1,
        
        [plus](x0, x1) = x0 + x1 + 1,
        
        [f](x0, x1, x2, x3) = 0,
        
        [true] = 0
       orientation:
        plus#(n,s(m)) = m + 2 >= m + 1 = plus#(n,m)
        
        f(true(),x,y,z) = 0 >= 0 = f(gt(x,plus(y,z)),x,s(y),z)
        
        f(true(),x,y,z) = 0 >= 0 = f(gt(x,plus(y,z)),x,y,s(z))
        
        plus(n,0()) = n + 1 >= n = n
        
        plus(n,s(m)) = m + n + 2 >= m + n + 2 = s(plus(n,m))
        
        gt(0(),v) = 1 >= 1 = false()
        
        gt(s(u),0()) = 1 >= 0 = true()
        
        gt(s(u),s(v)) = 1 >= 1 = gt(u,v)
       problem:
        DPs:
         
        TRS:
         f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,s(y),z)
         f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,y,s(z))
         plus(n,0()) -> n
         plus(n,s(m)) -> s(plus(n,m))
         gt(0(),v) -> false()
         gt(s(u),0()) -> true()
         gt(s(u),s(v)) -> gt(u,v)
       Qed
      
      DPs:
       gt#(s(u),s(v)) -> gt#(u,v)
      TRS:
       f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,s(y),z)
       f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,y,s(z))
       plus(n,0()) -> n
       plus(n,s(m)) -> s(plus(n,m))
       gt(0(),v) -> false()
       gt(s(u),0()) -> true()
       gt(s(u),s(v)) -> gt(u,v)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [gt#](x0, x1) = x0 + 1,
        
        [false] = 0,
        
        [0] = 1,
        
        [s](x0) = x0 + 1,
        
        [gt](x0, x1) = x1,
        
        [plus](x0, x1) = x0 + x1 + 1,
        
        [f](x0, x1, x2, x3) = x1,
        
        [true] = 0
       orientation:
        gt#(s(u),s(v)) = u + 2 >= u + 1 = gt#(u,v)
        
        f(true(),x,y,z) = x >= x = f(gt(x,plus(y,z)),x,s(y),z)
        
        f(true(),x,y,z) = x >= x = f(gt(x,plus(y,z)),x,y,s(z))
        
        plus(n,0()) = n + 2 >= n = n
        
        plus(n,s(m)) = m + n + 2 >= m + n + 2 = s(plus(n,m))
        
        gt(0(),v) = v >= 0 = false()
        
        gt(s(u),0()) = 1 >= 0 = true()
        
        gt(s(u),s(v)) = v + 1 >= v = gt(u,v)
       problem:
        DPs:
         
        TRS:
         f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,s(y),z)
         f(true(),x,y,z) -> f(gt(x,plus(y,z)),x,y,s(z))
         plus(n,0()) -> n
         plus(n,s(m)) -> s(plus(n,m))
         gt(0(),v) -> false()
         gt(s(u),0()) -> true()
         gt(s(u),s(v)) -> gt(u,v)
       Qed