MAYBE
Time: 0.014640
TRS:
 {h f f x -> h f g f x,
  f g f x -> f f x}
 DP:
  DP:
   {h# f f x -> h# f g f x,
    h# f f x -> f# g f x,
    f# g f x -> f# f x}
  TRS:
  {h f f x -> h f g f x,
   f g f x -> f f x}
  UR:
   {f g f x -> f f x}
   EDG:
    {(f# g f x -> f# f x, f# g f x -> f# f x)
     (h# f f x -> h# f g f x, h# f f x -> h# f g f x)
     (h# f f x -> h# f g f x, h# f f x -> f# g f x)
     (h# f f x -> f# g f x, f# g f x -> f# f x)}
    STATUS:
     arrows: 0.555556
     SCCS (2):
      Scc:
       {h# f f x -> h# f g f x}
      Scc:
       {f# g f x -> f# f x}
      
      SCC (1):
       Strict:
        {h# f f x -> h# f g f x}
       Weak:
       {h f f x -> h f g f x,
        f g f x -> f f x}
       Fail
      
      SCC (1):
       Strict:
        {f# g f x -> f# f x}
       Weak:
       {h f f x -> h f g f x,
        f g f x -> f f x}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [h](x0) = 0,
         
         [f](x0) = 0,
         
         [g](x0) = 1,
         
         [f#](x0) = x0
        Strict:
         f# g f x -> f# f x
         1 + 0x >= 0 + 0x
        Weak:
         f g f x -> f f x
         0 + 0x >= 0 + 0x
         h f f x -> h f g f x
         0 + 0x >= 0 + 0x
       Qed