YES(?,POLY)

'Pop* with parameter subtitution (timeout of 60.0 seconds)'
-----------------------------------------------------------
Answer:           YES(?,POLY)
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  f(x, y, w, w, a()) -> g1(x, x, y, w)
     , f(x, y, w, a(), a()) -> g1(y, x, x, w)
     , f(x, y, a(), a(), w) -> g2(x, y, y, w)
     , f(x, y, a(), w, w) -> g2(y, y, x, w)
     , g1(x, x, y, a()) -> h(x, y)
     , g1(y, x, x, a()) -> h(x, y)
     , g2(x, y, y, a()) -> h(x, y)
     , g2(y, y, x, a()) -> h(x, y)
     , h(x, x) -> x}

Proof Output:    
  The input was oriented with the instance of POP* as induced by the precedence
  
   f > g2, f > h, g1 > g2, g1 > h, f ~ g1, g2 ~ h
  
  and safe mapping
  
   safe(f) = {}, safe(a) = {}, safe(g1) = {1, 2, 3, 4},
   safe(g2) = {1, 2, 3}, safe(h) = {1, 2} .
  
  For your convenience, here is the input in predicative notation:
  
   Rules:
    {  f(x, y, w, w, a();) -> g1(; x, x, y, w)
     , f(x, y, w, a(), a();) -> g1(; y, x, x, w)
     , f(x, y, a(), a(), w;) -> g2(w; x, y, y)
     , f(x, y, a(), w, w;) -> g2(w; y, y, x)
     , g1(; x, x, y, a()) -> h(; x, y)
     , g1(; y, x, x, a()) -> h(; x, y)
     , g2(a(); x, y, y) -> h(; x, y)
     , g2(a(); y, y, x) -> h(; x, y)
     , h(; x, x) -> x}