MAYBE
TRS:
 {        f(a(), x) -> f(b(), f(c(), x)),
  f(a(), f(b(), x)) -> f(b(), f(a(), x)),
  f(a(), f(c(), x)) -> f(c(), f(a(), x)),
  f(d(), f(c(), x)) -> f(d(), f(a(), x))}
 DP:
  Strict:
   {        f#(a(), x) -> f#(b(), f(c(), x)),
            f#(a(), x) -> f#(c(), x),
    f#(a(), f(b(), x)) -> f#(b(), f(a(), x)),
    f#(a(), f(b(), x)) -> f#(a(), x),
    f#(a(), f(c(), x)) -> f#(c(), f(a(), x)),
    f#(a(), f(c(), x)) -> f#(a(), x),
    f#(d(), f(c(), x)) -> f#(a(), x),
    f#(d(), f(c(), x)) -> f#(d(), f(a(), x))}
  Weak:
  {        f(a(), x) -> f(b(), f(c(), x)),
   f(a(), f(b(), x)) -> f(b(), f(a(), x)),
   f(a(), f(c(), x)) -> f(c(), f(a(), x)),
   f(d(), f(c(), x)) -> f(d(), f(a(), x))}
  EDG:
   {(f#(d(), f(c(), x)) -> f#(d(), f(a(), x)), f#(d(), f(c(), x)) -> f#(d(), f(a(), x)))
    (f#(d(), f(c(), x)) -> f#(d(), f(a(), x)), f#(d(), f(c(), x)) -> f#(a(), x))
    (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(c(), x)) -> f#(a(), x))
    (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(c(), x)) -> f#(c(), f(a(), x)))
    (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(a(), x))
    (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(b(), f(a(), x)))
    (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), x) -> f#(c(), x))
    (f#(a(), f(b(), x)) -> f#(a(), x), f#(a(), x) -> f#(b(), f(c(), x)))
    (f#(d(), f(c(), x)) -> f#(a(), x), f#(a(), f(c(), x)) -> f#(a(), x))
    (f#(d(), f(c(), x)) -> f#(a(), x), f#(a(), f(c(), x)) -> f#(c(), f(a(), x)))
    (f#(d(), f(c(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(a(), x))
    (f#(d(), f(c(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(b(), f(a(), x)))
    (f#(d(), f(c(), x)) -> f#(a(), x), f#(a(), x) -> f#(c(), x))
    (f#(d(), f(c(), x)) -> f#(a(), x), f#(a(), x) -> f#(b(), f(c(), x)))
    (f#(a(), f(c(), x)) -> f#(a(), x), f#(a(), x) -> f#(b(), f(c(), x)))
    (f#(a(), f(c(), x)) -> f#(a(), x), f#(a(), x) -> f#(c(), x))
    (f#(a(), f(c(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(b(), f(a(), x)))
    (f#(a(), f(c(), x)) -> f#(a(), x), f#(a(), f(b(), x)) -> f#(a(), x))
    (f#(a(), f(c(), x)) -> f#(a(), x), f#(a(), f(c(), x)) -> f#(c(), f(a(), x)))
    (f#(a(), f(c(), x)) -> f#(a(), x), f#(a(), f(c(), x)) -> f#(a(), x))}
   SCCS:
    Scc:
     {f#(d(), f(c(), x)) -> f#(d(), f(a(), x))}
    Scc:
     {f#(a(), f(b(), x)) -> f#(a(), x),
      f#(a(), f(c(), x)) -> f#(a(), x)}
    SCC:
     Strict:
      {f#(d(), f(c(), x)) -> f#(d(), f(a(), x))}
     Weak:
     {        f(a(), x) -> f(b(), f(c(), x)),
      f(a(), f(b(), x)) -> f(b(), f(a(), x)),
      f(a(), f(c(), x)) -> f(c(), f(a(), x)),
      f(d(), f(c(), x)) -> f(d(), f(a(), x))}
     Fail
    SCC:
     Strict:
      {f#(a(), f(b(), x)) -> f#(a(), x),
       f#(a(), f(c(), x)) -> f#(a(), x)}
     Weak:
     {        f(a(), x) -> f(b(), f(c(), x)),
      f(a(), f(b(), x)) -> f(b(), f(a(), x)),
      f(a(), f(c(), x)) -> f(c(), f(a(), x)),
      f(d(), f(c(), x)) -> f(d(), f(a(), x))}
     SPSC:
      Simple Projection:
       pi(f#) = 1
      Strict:
       {f#(a(), f(c(), x)) -> f#(a(), x)}
      EDG:
       {(f#(a(), f(c(), x)) -> f#(a(), x), f#(a(), f(c(), x)) -> f#(a(), x))}
       SCCS:
        Scc:
         {f#(a(), f(c(), x)) -> f#(a(), x)}
        SCC:
         Strict:
          {f#(a(), f(c(), x)) -> f#(a(), x)}
         Weak:
         {        f(a(), x) -> f(b(), f(c(), x)),
          f(a(), f(b(), x)) -> f(b(), f(a(), x)),
          f(a(), f(c(), x)) -> f(c(), f(a(), x)),
          f(d(), f(c(), x)) -> f(d(), f(a(), x))}
         SPSC:
          Simple Projection:
           pi(f#) = 1
          Strict:
           {}
          Qed