MAYBE
Time: 0.004404
TRS:
 {f(true(), x, y, z) -> f(and(gt(x, y), gt(x, z)), x, y, s z),
  f(true(), x, y, z) -> f(and(gt(x, y), gt(x, z)), x, s y, z),
      and(x, true()) -> x,
     and(x, false()) -> false(),
        gt(s u, s v) -> gt(u, v),
        gt(s u, 0()) -> true(),
          gt(0(), v) -> false()}
 DP:
  DP:
   {f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z),
    f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z),
    f#(true(), x, y, z) -> and#(gt(x, y), gt(x, z)),
    f#(true(), x, y, z) -> gt#(x, y),
    f#(true(), x, y, z) -> gt#(x, z),
          gt#(s u, s v) -> gt#(u, v)}
  TRS:
  {f(true(), x, y, z) -> f(and(gt(x, y), gt(x, z)), x, y, s z),
   f(true(), x, y, z) -> f(and(gt(x, y), gt(x, z)), x, s y, z),
       and(x, true()) -> x,
      and(x, false()) -> false(),
         gt(s u, s v) -> gt(u, v),
         gt(s u, 0()) -> true(),
           gt(0(), v) -> false()}
  UR:
   { and(x, true()) -> x,
    and(x, false()) -> false(),
       gt(s u, s v) -> gt(u, v),
       gt(s u, 0()) -> true(),
         gt(0(), v) -> false(),
            a(w, t) -> w,
            a(w, t) -> t}
   EDG:
    {(f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> gt#(x, z))
     (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> gt#(x, y))
     (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> and#(gt(x, y), gt(x, z)))
     (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z))
     (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z))
     (f#(true(), x, y, z) -> gt#(x, z), gt#(s u, s v) -> gt#(u, v))
     (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> gt#(x, z))
     (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> gt#(x, y))
     (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> and#(gt(x, y), gt(x, z)))
     (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z))
     (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z))
     (f#(true(), x, y, z) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
     (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))}
    EDG:
     {(f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> gt#(x, z))
      (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> gt#(x, y))
      (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> and#(gt(x, y), gt(x, z)))
      (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z))
      (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z))
      (f#(true(), x, y, z) -> gt#(x, z), gt#(s u, s v) -> gt#(u, v))
      (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> gt#(x, z))
      (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> gt#(x, y))
      (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> and#(gt(x, y), gt(x, z)))
      (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z))
      (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z))
      (f#(true(), x, y, z) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
      (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))}
     EDG:
      {(f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> gt#(x, z))
       (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> gt#(x, y))
       (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> and#(gt(x, y), gt(x, z)))
       (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z))
       (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z))
       (f#(true(), x, y, z) -> gt#(x, z), gt#(s u, s v) -> gt#(u, v))
       (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> gt#(x, z))
       (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> gt#(x, y))
       (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> and#(gt(x, y), gt(x, z)))
       (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z))
       (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z))
       (f#(true(), x, y, z) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
       (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))}
      EDG:
       {(f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> gt#(x, z))
        (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> gt#(x, y))
        (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> and#(gt(x, y), gt(x, z)))
        (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z))
        (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z))
        (f#(true(), x, y, z) -> gt#(x, z), gt#(s u, s v) -> gt#(u, v))
        (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> gt#(x, z))
        (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> gt#(x, y))
        (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> and#(gt(x, y), gt(x, z)))
        (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z))
        (f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z), f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z))
        (f#(true(), x, y, z) -> gt#(x, y), gt#(s u, s v) -> gt#(u, v))
        (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))}
       STATUS:
        arrows: 0.638889
        SCCS (2):
         Scc:
          {f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z),
           f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z)}
         Scc:
          {gt#(s u, s v) -> gt#(u, v)}
         
         SCC (2):
          Strict:
           {f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, y, s z),
            f#(true(), x, y, z) -> f#(and(gt(x, y), gt(x, z)), x, s y, z)}
          Weak:
          {f(true(), x, y, z) -> f(and(gt(x, y), gt(x, z)), x, y, s z),
           f(true(), x, y, z) -> f(and(gt(x, y), gt(x, z)), x, s y, z),
               and(x, true()) -> x,
              and(x, false()) -> false(),
                 gt(s u, s v) -> gt(u, v),
                 gt(s u, 0()) -> true(),
                   gt(0(), v) -> false()}
          Open
         
         
         
         SCC (1):
          Strict:
           {gt#(s u, s v) -> gt#(u, v)}
          Weak:
          {f(true(), x, y, z) -> f(and(gt(x, y), gt(x, z)), x, y, s z),
           f(true(), x, y, z) -> f(and(gt(x, y), gt(x, z)), x, s y, z),
               and(x, true()) -> x,
              and(x, false()) -> false(),
                 gt(s u, s v) -> gt(u, v),
                 gt(s u, 0()) -> true(),
                   gt(0(), v) -> false()}
          Open