MAYBE

Problem:
 min(0(),y) -> 0()
 min(x,0()) -> 0()
 min(s(x),s(y)) -> s(min(x,y))
 max(0(),y) -> y
 max(x,0()) -> x
 max(s(x),s(y)) -> s(max(x,y))
 p(s(x)) -> x
 f(s(x),s(y),s(z)) ->
 f(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z))))
 f(0(),y,z) -> max(y,z)
 f(x,0(),z) -> max(x,z)
 f(x,y,0()) -> max(x,y)

Proof:
 DP Processor:
  DPs:
   min#(s(x),s(y)) -> min#(x,y)
   max#(s(x),s(y)) -> max#(x,y)
   f#(s(x),s(y),s(z)) -> min#(s(y),s(z))
   f#(s(x),s(y),s(z)) -> min#(s(x),min(s(y),s(z)))
   f#(s(x),s(y),s(z)) -> min#(s(x),max(s(y),s(z)))
   f#(s(x),s(y),s(z)) -> p#(min(s(x),max(s(y),s(z))))
   f#(s(x),s(y),s(z)) -> max#(s(y),s(z))
   f#(s(x),s(y),s(z)) -> max#(s(x),max(s(y),s(z)))
   f#(s(x),s(y),s(z)) ->
   f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z))))
   f#(0(),y,z) -> max#(y,z)
   f#(x,0(),z) -> max#(x,z)
   f#(x,y,0()) -> max#(x,y)
  TRS:
   min(0(),y) -> 0()
   min(x,0()) -> 0()
   min(s(x),s(y)) -> s(min(x,y))
   max(0(),y) -> y
   max(x,0()) -> x
   max(s(x),s(y)) -> s(max(x,y))
   p(s(x)) -> x
   f(s(x),s(y),s(z)) ->
   f(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z))))
   f(0(),y,z) -> max(y,z)
   f(x,0(),z) -> max(x,z)
   f(x,y,0()) -> max(x,y)
  TDG Processor:
   DPs:
    min#(s(x),s(y)) -> min#(x,y)
    max#(s(x),s(y)) -> max#(x,y)
    f#(s(x),s(y),s(z)) -> min#(s(y),s(z))
    f#(s(x),s(y),s(z)) -> min#(s(x),min(s(y),s(z)))
    f#(s(x),s(y),s(z)) -> min#(s(x),max(s(y),s(z)))
    f#(s(x),s(y),s(z)) -> p#(min(s(x),max(s(y),s(z))))
    f#(s(x),s(y),s(z)) -> max#(s(y),s(z))
    f#(s(x),s(y),s(z)) -> max#(s(x),max(s(y),s(z)))
    f#(s(x),s(y),s(z)) ->
    f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z))))
    f#(0(),y,z) -> max#(y,z)
    f#(x,0(),z) -> max#(x,z)
    f#(x,y,0()) -> max#(x,y)
   TRS:
    min(0(),y) -> 0()
    min(x,0()) -> 0()
    min(s(x),s(y)) -> s(min(x,y))
    max(0(),y) -> y
    max(x,0()) -> x
    max(s(x),s(y)) -> s(max(x,y))
    p(s(x)) -> x
    f(s(x),s(y),s(z)) ->
    f(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z))))
    f(0(),y,z) -> max(y,z)
    f(x,0(),z) -> max(x,z)
    f(x,y,0()) -> max(x,y)
   graph:
    f#(s(x),s(y),s(z)) ->
    f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z)))) ->
    f#(x,y,0()) -> max#(x,y)
    f#(s(x),s(y),s(z)) ->
    f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z)))) ->
    f#(x,0(),z) -> max#(x,z)
    f#(s(x),s(y),s(z)) ->
    f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z)))) ->
    f#(0(),y,z) -> max#(y,z)
    f#(s(x),s(y),s(z)) ->
    f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z)))) ->
    f#(s(x),s(y),s(z)) ->
    f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z))))
    f#(s(x),s(y),s(z)) ->
    f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z)))) ->
    f#(s(x),s(y),s(z)) -> max#(s(x),max(s(y),s(z)))
    f#(s(x),s(y),s(z)) ->
    f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z)))) ->
    f#(s(x),s(y),s(z)) -> max#(s(y),s(z))
    f#(s(x),s(y),s(z)) ->
    f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z)))) ->
    f#(s(x),s(y),s(z)) -> p#(min(s(x),max(s(y),s(z))))
    f#(s(x),s(y),s(z)) ->
    f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z)))) ->
    f#(s(x),s(y),s(z)) -> min#(s(x),max(s(y),s(z)))
    f#(s(x),s(y),s(z)) ->
    f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z)))) ->
    f#(s(x),s(y),s(z)) -> min#(s(x),min(s(y),s(z)))
    f#(s(x),s(y),s(z)) ->
    f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z)))) ->
    f#(s(x),s(y),s(z)) -> min#(s(y),s(z))
    f#(s(x),s(y),s(z)) -> max#(s(y),s(z)) ->
    max#(s(x),s(y)) -> max#(x,y)
    f#(s(x),s(y),s(z)) -> max#(s(x),max(s(y),s(z))) ->
    max#(s(x),s(y)) -> max#(x,y)
    f#(s(x),s(y),s(z)) -> min#(s(y),s(z)) ->
    min#(s(x),s(y)) -> min#(x,y)
    f#(s(x),s(y),s(z)) -> min#(s(x),max(s(y),s(z))) ->
    min#(s(x),s(y)) -> min#(x,y)
    f#(s(x),s(y),s(z)) -> min#(s(x),min(s(y),s(z))) ->
    min#(s(x),s(y)) -> min#(x,y)
    f#(0(),y,z) -> max#(y,z) -> max#(s(x),s(y)) -> max#(x,y)
    f#(x,0(),z) -> max#(x,z) -> max#(s(x),s(y)) -> max#(x,y)
    f#(x,y,0()) -> max#(x,y) -> max#(s(x),s(y)) -> max#(x,y)
    max#(s(x),s(y)) -> max#(x,y) -> max#(s(x),s(y)) -> max#(x,y)
    min#(s(x),s(y)) -> min#(x,y) -> min#(s(x),s(y)) -> min#(x,y)
   SCC Processor:
    #sccs: 3
    #rules: 3
    #arcs: 20/144
    DPs:
     f#(s(x),s(y),s(z)) ->
     f#(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z))))
    TRS:
     min(0(),y) -> 0()
     min(x,0()) -> 0()
     min(s(x),s(y)) -> s(min(x,y))
     max(0(),y) -> y
     max(x,0()) -> x
     max(s(x),s(y)) -> s(max(x,y))
     p(s(x)) -> x
     f(s(x),s(y),s(z)) ->
     f(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z))))
     f(0(),y,z) -> max(y,z)
     f(x,0(),z) -> max(x,z)
     f(x,y,0()) -> max(x,y)
    Open
    
    DPs:
     max#(s(x),s(y)) -> max#(x,y)
    TRS:
     min(0(),y) -> 0()
     min(x,0()) -> 0()
     min(s(x),s(y)) -> s(min(x,y))
     max(0(),y) -> y
     max(x,0()) -> x
     max(s(x),s(y)) -> s(max(x,y))
     p(s(x)) -> x
     f(s(x),s(y),s(z)) ->
     f(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z))))
     f(0(),y,z) -> max(y,z)
     f(x,0(),z) -> max(x,z)
     f(x,y,0()) -> max(x,y)
    Subterm Criterion Processor:
     simple projection:
      pi(max#) = 1
     problem:
      DPs:
       
      TRS:
       min(0(),y) -> 0()
       min(x,0()) -> 0()
       min(s(x),s(y)) -> s(min(x,y))
       max(0(),y) -> y
       max(x,0()) -> x
       max(s(x),s(y)) -> s(max(x,y))
       p(s(x)) -> x
       f(s(x),s(y),s(z)) ->
       f(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z))))
       f(0(),y,z) -> max(y,z)
       f(x,0(),z) -> max(x,z)
       f(x,y,0()) -> max(x,y)
     Qed
    
    DPs:
     min#(s(x),s(y)) -> min#(x,y)
    TRS:
     min(0(),y) -> 0()
     min(x,0()) -> 0()
     min(s(x),s(y)) -> s(min(x,y))
     max(0(),y) -> y
     max(x,0()) -> x
     max(s(x),s(y)) -> s(max(x,y))
     p(s(x)) -> x
     f(s(x),s(y),s(z)) ->
     f(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z))))
     f(0(),y,z) -> max(y,z)
     f(x,0(),z) -> max(x,z)
     f(x,y,0()) -> max(x,y)
    Subterm Criterion Processor:
     simple projection:
      pi(min#) = 1
     problem:
      DPs:
       
      TRS:
       min(0(),y) -> 0()
       min(x,0()) -> 0()
       min(s(x),s(y)) -> s(min(x,y))
       max(0(),y) -> y
       max(x,0()) -> x
       max(s(x),s(y)) -> s(max(x,y))
       p(s(x)) -> x
       f(s(x),s(y),s(z)) ->
       f(max(s(x),max(s(y),s(z))),p(min(s(x),max(s(y),s(z)))),min(s(x),min(s(y),s(z))))
       f(0(),y,z) -> max(y,z)
       f(x,0(),z) -> max(x,z)
       f(x,y,0()) -> max(x,y)
     Qed