MAYBE

Problem:
 g(x,x,x) -> g(c(),d(),e())
 g(x,y,x) -> g(c(),d(),e())
 s(f(x,y)) -> f(y,f(s(s(x)),a()))
 h(h(x,a()),y) -> h(h(a(),y),h(a(),x))
 f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b())))
 f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b()))
 h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a())))
 f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y))
 s(y) -> b()

Proof:
 DP Processor:
  DPs:
   g#(x,x,x) -> g#(c(),d(),e())
   g#(x,y,x) -> g#(c(),d(),e())
   s#(f(x,y)) -> s#(x)
   s#(f(x,y)) -> s#(s(x))
   s#(f(x,y)) -> f#(s(s(x)),a())
   s#(f(x,y)) -> f#(y,f(s(s(x)),a()))
   h#(h(x,a()),y) -> h#(a(),x)
   h#(h(x,a()),y) -> h#(a(),y)
   h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x))
   f#(x,f(y,f(x,y))) -> f#(y,b())
   f#(x,f(y,f(x,y))) -> f#(x,f(y,b()))
   f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b())))
   f#(h(a(),y),g(x,b(),a())) -> s#(b())
   f#(h(a(),y),g(x,b(),a())) -> s#(y)
   f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y))
   f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b()))
   h#(f(x,s(y)),b()) -> s#(x)
   h#(f(x,s(y)),b()) -> f#(s(x),a())
   h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a()))
   h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a())))
   f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y)
   f#(x,g(x,a(),f(s(x),y))) -> h#(x,b())
   f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y))
  TRS:
   g(x,x,x) -> g(c(),d(),e())
   g(x,y,x) -> g(c(),d(),e())
   s(f(x,y)) -> f(y,f(s(s(x)),a()))
   h(h(x,a()),y) -> h(h(a(),y),h(a(),x))
   f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b())))
   f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b()))
   h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a())))
   f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y))
   s(y) -> b()
  Usable Rule Processor:
   DPs:
    g#(x,x,x) -> g#(c(),d(),e())
    g#(x,y,x) -> g#(c(),d(),e())
    s#(f(x,y)) -> s#(x)
    s#(f(x,y)) -> s#(s(x))
    s#(f(x,y)) -> f#(s(s(x)),a())
    s#(f(x,y)) -> f#(y,f(s(s(x)),a()))
    h#(h(x,a()),y) -> h#(a(),x)
    h#(h(x,a()),y) -> h#(a(),y)
    h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x))
    f#(x,f(y,f(x,y))) -> f#(y,b())
    f#(x,f(y,f(x,y))) -> f#(x,f(y,b()))
    f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b())))
    f#(h(a(),y),g(x,b(),a())) -> s#(b())
    f#(h(a(),y),g(x,b(),a())) -> s#(y)
    f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y))
    f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b()))
    h#(f(x,s(y)),b()) -> s#(x)
    h#(f(x,s(y)),b()) -> f#(s(x),a())
    h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a()))
    h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a())))
    f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y)
    f#(x,g(x,a(),f(s(x),y))) -> h#(x,b())
    f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y))
   TRS:
    s(f(x,y)) -> f(y,f(s(s(x)),a()))
    s(y) -> b()
    f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b())))
    f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b()))
    f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y))
    h(h(x,a()),y) -> h(h(a(),y),h(a(),x))
    h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a())))
    g(x,y,x) -> g(c(),d(),e())
   ADG Processor:
    DPs:
     g#(x,x,x) -> g#(c(),d(),e())
     g#(x,y,x) -> g#(c(),d(),e())
     s#(f(x,y)) -> s#(x)
     s#(f(x,y)) -> s#(s(x))
     s#(f(x,y)) -> f#(s(s(x)),a())
     s#(f(x,y)) -> f#(y,f(s(s(x)),a()))
     h#(h(x,a()),y) -> h#(a(),x)
     h#(h(x,a()),y) -> h#(a(),y)
     h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x))
     f#(x,f(y,f(x,y))) -> f#(y,b())
     f#(x,f(y,f(x,y))) -> f#(x,f(y,b()))
     f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b())))
     f#(h(a(),y),g(x,b(),a())) -> s#(b())
     f#(h(a(),y),g(x,b(),a())) -> s#(y)
     f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y))
     f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b()))
     h#(f(x,s(y)),b()) -> s#(x)
     h#(f(x,s(y)),b()) -> f#(s(x),a())
     h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a()))
     h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a())))
     f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y)
     f#(x,g(x,a(),f(s(x),y))) -> h#(x,b())
     f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y))
    TRS:
     s(f(x,y)) -> f(y,f(s(s(x)),a()))
     s(y) -> b()
     f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b())))
     f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b()))
     f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y))
     h(h(x,a()),y) -> h(h(a(),y),h(a(),x))
     h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a())))
     g(x,y,x) -> g(c(),d(),e())
    graph:
     h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) ->
     h#(h(x,a()),y) -> h#(a(),x)
     h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) ->
     h#(h(x,a()),y) -> h#(a(),y)
     h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) ->
     h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x))
     h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) ->
     f#(x,f(y,f(x,y))) -> f#(y,b())
     h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) ->
     f#(x,f(y,f(x,y))) -> f#(x,f(y,b()))
     h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) ->
     f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b())))
     h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) ->
     f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y)
     h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) ->
     f#(x,g(x,a(),f(s(x),y))) -> h#(x,b())
     h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) ->
     f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y))
     h#(f(x,s(y)),b()) -> s#(x) -> s#(f(x,y)) -> s#(x)
     h#(f(x,s(y)),b()) -> s#(x) -> s#(f(x,y)) -> s#(s(x))
     h#(f(x,s(y)),b()) -> s#(x) -> s#(f(x,y)) -> f#(s(s(x)),a())
     h#(f(x,s(y)),b()) -> s#(x) ->
     s#(f(x,y)) -> f#(y,f(s(s(x)),a()))
     h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a())) ->
     g#(x,y,x) -> g#(c(),d(),e())
     f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) ->
     h#(f(x,s(y)),b()) -> s#(x)
     f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) ->
     h#(f(x,s(y)),b()) -> f#(s(x),a())
     f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) ->
     h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a()))
     f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) ->
     h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a())))
     f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) ->
     f#(x,f(y,f(x,y))) -> f#(y,b())
     f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) ->
     f#(x,f(y,f(x,y))) -> f#(x,f(y,b()))
     f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) ->
     f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b())))
     f#(h(a(),y),g(x,b(),a())) -> s#(y) -> s#(f(x,y)) -> s#(x)
     f#(h(a(),y),g(x,b(),a())) -> s#(y) -> s#(f(x,y)) -> s#(s(x))
     f#(h(a(),y),g(x,b(),a())) -> s#(y) ->
     s#(f(x,y)) -> f#(s(s(x)),a())
     f#(h(a(),y),g(x,b(),a())) -> s#(y) ->
     s#(f(x,y)) -> f#(y,f(s(s(x)),a()))
     f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) ->
     f#(x,f(y,f(x,y))) -> f#(y,b())
     f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) ->
     f#(x,f(y,f(x,y))) -> f#(x,f(y,b()))
     f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) ->
     f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b())))
     f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) ->
     h#(h(x,a()),y) -> h#(a(),x)
     f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) ->
     h#(h(x,a()),y) -> h#(a(),y)
     f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) ->
     h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x))
     f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) ->
     h#(f(x,s(y)),b()) -> s#(x)
     f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) ->
     h#(f(x,s(y)),b()) -> f#(s(x),a())
     f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) ->
     h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a()))
     f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) ->
     h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a())))
     f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) ->
     f#(x,f(y,f(x,y))) -> f#(y,b())
     f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) ->
     f#(x,f(y,f(x,y))) -> f#(x,f(y,b()))
     f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) ->
     f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b())))
     f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) ->
     f#(h(a(),y),g(x,b(),a())) -> s#(b())
     f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) ->
     f#(h(a(),y),g(x,b(),a())) -> s#(y)
     f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) ->
     f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y))
     f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) ->
     f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b()))
     f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) ->
     g#(x,y,x) -> g#(c(),d(),e())
     s#(f(x,y)) -> s#(s(x)) -> s#(f(x,y)) -> s#(x)
     s#(f(x,y)) -> s#(s(x)) -> s#(f(x,y)) -> s#(s(x))
     s#(f(x,y)) -> s#(s(x)) -> s#(f(x,y)) -> f#(s(s(x)),a())
     s#(f(x,y)) -> s#(s(x)) -> s#(f(x,y)) -> f#(y,f(s(s(x)),a()))
     s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> s#(x)
     s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> s#(s(x))
     s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> f#(s(s(x)),a())
     s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> f#(y,f(s(s(x)),a()))
    Restore Modifier:
     DPs:
      g#(x,x,x) -> g#(c(),d(),e())
      g#(x,y,x) -> g#(c(),d(),e())
      s#(f(x,y)) -> s#(x)
      s#(f(x,y)) -> s#(s(x))
      s#(f(x,y)) -> f#(s(s(x)),a())
      s#(f(x,y)) -> f#(y,f(s(s(x)),a()))
      h#(h(x,a()),y) -> h#(a(),x)
      h#(h(x,a()),y) -> h#(a(),y)
      h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x))
      f#(x,f(y,f(x,y))) -> f#(y,b())
      f#(x,f(y,f(x,y))) -> f#(x,f(y,b()))
      f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b())))
      f#(h(a(),y),g(x,b(),a())) -> s#(b())
      f#(h(a(),y),g(x,b(),a())) -> s#(y)
      f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y))
      f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b()))
      h#(f(x,s(y)),b()) -> s#(x)
      h#(f(x,s(y)),b()) -> f#(s(x),a())
      h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a()))
      h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a())))
      f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y)
      f#(x,g(x,a(),f(s(x),y))) -> h#(x,b())
      f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y))
     TRS:
      g(x,x,x) -> g(c(),d(),e())
      g(x,y,x) -> g(c(),d(),e())
      s(f(x,y)) -> f(y,f(s(s(x)),a()))
      h(h(x,a()),y) -> h(h(a(),y),h(a(),x))
      f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b())))
      f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b()))
      h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a())))
      f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y))
      s(y) -> b()
     SCC Processor:
      #sccs: 4
      #rules: 8
      #arcs: 51/529
      DPs:
       h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a())))
       f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y))
       f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b()))
       f#(x,g(x,a(),f(s(x),y))) -> h#(x,b())
      TRS:
       g(x,x,x) -> g(c(),d(),e())
       g(x,y,x) -> g(c(),d(),e())
       s(f(x,y)) -> f(y,f(s(s(x)),a()))
       h(h(x,a()),y) -> h(h(a(),y),h(a(),x))
       f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b())))
       f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b()))
       h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a())))
       f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y))
       s(y) -> b()
      Open
      
      DPs:
       f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b())))
      TRS:
       g(x,x,x) -> g(c(),d(),e())
       g(x,y,x) -> g(c(),d(),e())
       s(f(x,y)) -> f(y,f(s(s(x)),a()))
       h(h(x,a()),y) -> h(h(a(),y),h(a(),x))
       f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b())))
       f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b()))
       h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a())))
       f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y))
       s(y) -> b()
      Open
      
      DPs:
       s#(f(x,y)) -> s#(s(x))
       s#(f(x,y)) -> s#(x)
      TRS:
       g(x,x,x) -> g(c(),d(),e())
       g(x,y,x) -> g(c(),d(),e())
       s(f(x,y)) -> f(y,f(s(s(x)),a()))
       h(h(x,a()),y) -> h(h(a(),y),h(a(),x))
       f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b())))
       f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b()))
       h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a())))
       f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y))
       s(y) -> b()
      Open
      
      DPs:
       h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x))
      TRS:
       g(x,x,x) -> g(c(),d(),e())
       g(x,y,x) -> g(c(),d(),e())
       s(f(x,y)) -> f(y,f(s(s(x)),a()))
       h(h(x,a()),y) -> h(h(a(),y),h(a(),x))
       f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b())))
       f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b()))
       h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a())))
       f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y))
       s(y) -> b()
      Open