MAYBE
Time: 0.290

Problem:
 Equations:
  NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
  NAC(x3,x4) -> NAC(x4,x3)
  maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5))
  maxAC(x3,x4) -> maxAC(x4,x3)
  maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5))
  maxxAC(x3,x4) -> maxxAC(x4,x3)
  NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
  NAC(x4,x3) -> NAC(x3,x4)
  maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5)
  maxAC(x4,x3) -> maxAC(x3,x4)
  maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5)
  maxxAC(x4,x3) -> maxxAC(x3,x4)
 TRS:
  h(L(x)) -> 0()
  h(NAC(x,y)) -> maxAC(h(x),h(y))
  maxAC(0(),x) -> x
  maxAC(x,0()) -> x
  maxAC(s(x),s(y)) -> s(maxxAC(x,y))
  maxxAC(0(),x) -> x
  maxxAC(x,0()) -> x
  maxxAC(s(x),s(y)) -> s(maxAC(x,y))

Proof:
 DP Processor:
  Equations#:
   N{AC,#}(NAC(x3,x4),x5) -> N{AC,#}(x3,NAC(x4,x5))
   N{AC,#}(x3,x4) -> N{AC,#}(x4,x3)
   max{AC,#}(maxAC(x3,x4),x5) -> max{AC,#}(x3,maxAC(x4,x5))
   max{AC,#}(x3,x4) -> max{AC,#}(x4,x3)
   maxx{AC,#}(maxxAC(x3,x4),x5) -> maxx{AC,#}(x3,maxxAC(x4,x5))
   maxx{AC,#}(x3,x4) -> maxx{AC,#}(x4,x3)
   N{AC,#}(x3,NAC(x4,x5)) -> N{AC,#}(NAC(x3,x4),x5)
   N{AC,#}(x4,x3) -> N{AC,#}(x3,x4)
   max{AC,#}(x3,maxAC(x4,x5)) -> max{AC,#}(maxAC(x3,x4),x5)
   max{AC,#}(x4,x3) -> max{AC,#}(x3,x4)
   maxx{AC,#}(x3,maxxAC(x4,x5)) -> maxx{AC,#}(maxxAC(x3,x4),x5)
   maxx{AC,#}(x4,x3) -> maxx{AC,#}(x3,x4)
  DPs:
   h#(NAC(x,y)) -> h#(y)
   h#(NAC(x,y)) -> h#(x)
   h#(NAC(x,y)) -> max{AC,#}(h(x),h(y))
   max{AC,#}(s(x),s(y)) -> maxx{AC,#}(x,y)
   maxx{AC,#}(s(x),s(y)) -> max{AC,#}(x,y)
   max{AC,#}(x6,maxAC(0(),x)) -> max{AC,#}(x6,x)
   max{AC,#}(x7,maxAC(x,0())) -> max{AC,#}(x7,x)
   max{AC,#}(x8,maxAC(s(x),s(y))) -> maxx{AC,#}(x,y)
   max{AC,#}(x8,maxAC(s(x),s(y))) -> max{AC,#}(x8,s(maxxAC(x,y)))
   maxx{AC,#}(x9,maxxAC(0(),x)) -> maxx{AC,#}(x9,x)
   maxx{AC,#}(x10,maxxAC(x,0())) -> maxx{AC,#}(x10,x)
   maxx{AC,#}(x11,maxxAC(s(x),s(y))) -> max{AC,#}(x,y)
   maxx{AC,#}(x11,maxxAC(s(x),s(y))) -> maxx{AC,#}(x11,s(maxAC(x,y)))
  Equations:
   NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
   NAC(x3,x4) -> NAC(x4,x3)
   maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5))
   maxAC(x3,x4) -> maxAC(x4,x3)
   maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5))
   maxxAC(x3,x4) -> maxxAC(x4,x3)
   NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
   NAC(x4,x3) -> NAC(x3,x4)
   maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5)
   maxAC(x4,x3) -> maxAC(x3,x4)
   maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5)
   maxxAC(x4,x3) -> maxxAC(x3,x4)
  TRS:
   h(L(x)) -> 0()
   h(NAC(x,y)) -> maxAC(h(x),h(y))
   maxAC(0(),x) -> x
   maxAC(x,0()) -> x
   maxAC(s(x),s(y)) -> s(maxxAC(x,y))
   maxxAC(0(),x) -> x
   maxxAC(x,0()) -> x
   maxxAC(s(x),s(y)) -> s(maxAC(x,y))
  S:
   N{AC,#}(NAC(x12,x13),x14) -> N{AC,#}(x12,x13)
   N{AC,#}(x12,NAC(x13,x14)) -> N{AC,#}(x13,x14)
   max{AC,#}(maxAC(x12,x13),x14) -> max{AC,#}(x12,x13)
   max{AC,#}(x12,maxAC(x13,x14)) -> max{AC,#}(x13,x14)
   maxx{AC,#}(maxxAC(x12,x13),x14) -> maxx{AC,#}(x12,x13)
   maxx{AC,#}(x12,maxxAC(x13,x14)) -> maxx{AC,#}(x13,x14)
  AC-EDG Processor:
   Equations#:
    N{AC,#}(NAC(x3,x4),x5) -> N{AC,#}(x3,NAC(x4,x5))
    N{AC,#}(x3,x4) -> N{AC,#}(x4,x3)
    max{AC,#}(maxAC(x3,x4),x5) -> max{AC,#}(x3,maxAC(x4,x5))
    max{AC,#}(x3,x4) -> max{AC,#}(x4,x3)
    maxx{AC,#}(maxxAC(x3,x4),x5) -> maxx{AC,#}(x3,maxxAC(x4,x5))
    maxx{AC,#}(x3,x4) -> maxx{AC,#}(x4,x3)
    N{AC,#}(x3,NAC(x4,x5)) -> N{AC,#}(NAC(x3,x4),x5)
    N{AC,#}(x4,x3) -> N{AC,#}(x3,x4)
    max{AC,#}(x3,maxAC(x4,x5)) -> max{AC,#}(maxAC(x3,x4),x5)
    max{AC,#}(x4,x3) -> max{AC,#}(x3,x4)
    maxx{AC,#}(x3,maxxAC(x4,x5)) -> maxx{AC,#}(maxxAC(x3,x4),x5)
    maxx{AC,#}(x4,x3) -> maxx{AC,#}(x3,x4)
   DPs:
    h#(NAC(x,y)) -> h#(y)
    h#(NAC(x,y)) -> h#(x)
    h#(NAC(x,y)) -> max{AC,#}(h(x),h(y))
    max{AC,#}(s(x),s(y)) -> maxx{AC,#}(x,y)
    maxx{AC,#}(s(x),s(y)) -> max{AC,#}(x,y)
    max{AC,#}(x6,maxAC(0(),x)) -> max{AC,#}(x6,x)
    max{AC,#}(x7,maxAC(x,0())) -> max{AC,#}(x7,x)
    max{AC,#}(x8,maxAC(s(x),s(y))) -> maxx{AC,#}(x,y)
    max{AC,#}(x8,maxAC(s(x),s(y))) -> max{AC,#}(x8,s(maxxAC(x,y)))
    maxx{AC,#}(x9,maxxAC(0(),x)) -> maxx{AC,#}(x9,x)
    maxx{AC,#}(x10,maxxAC(x,0())) -> maxx{AC,#}(x10,x)
    maxx{AC,#}(x11,maxxAC(s(x),s(y))) -> max{AC,#}(x,y)
    maxx{AC,#}(x11,maxxAC(s(x),s(y))) -> maxx{AC,#}(x11,s(maxAC(x,y)))
   Equations:
    NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
    NAC(x3,x4) -> NAC(x4,x3)
    maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5))
    maxAC(x3,x4) -> maxAC(x4,x3)
    maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5))
    maxxAC(x3,x4) -> maxxAC(x4,x3)
    NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
    NAC(x4,x3) -> NAC(x3,x4)
    maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5)
    maxAC(x4,x3) -> maxAC(x3,x4)
    maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5)
    maxxAC(x4,x3) -> maxxAC(x3,x4)
   TRS:
    h(L(x)) -> 0()
    h(NAC(x,y)) -> maxAC(h(x),h(y))
    maxAC(0(),x) -> x
    maxAC(x,0()) -> x
    maxAC(s(x),s(y)) -> s(maxxAC(x,y))
    maxxAC(0(),x) -> x
    maxxAC(x,0()) -> x
    maxxAC(s(x),s(y)) -> s(maxAC(x,y))
   S:
    N{AC,#}(NAC(x12,x13),x14) -> N{AC,#}(x12,x13)
    N{AC,#}(x12,NAC(x13,x14)) -> N{AC,#}(x13,x14)
    max{AC,#}(maxAC(x12,x13),x14) -> max{AC,#}(x12,x13)
    max{AC,#}(x12,maxAC(x13,x14)) -> max{AC,#}(x13,x14)
    maxx{AC,#}(maxxAC(x12,x13),x14) -> maxx{AC,#}(x12,x13)
    maxx{AC,#}(x12,maxxAC(x13,x14)) -> maxx{AC,#}(x13,x14)
   Open