MAYBE
Time: 0.007345
TRS:
 {      greater(x, 0()) -> first(),
      greater(0(), s y) -> second(),
      greater(s x, s y) -> greater(x, y),
          le(0(), y, z) -> greater(y, z),
        le(s x, 0(), z) -> false(),
      le(s x, s y, 0()) -> false(),
      le(s x, s y, s z) -> le(x, y, z),
             double 0() -> 0(),
             double s x -> s s double x,
   if(false(), x, y, z) -> true(),
   if(first(), x, y, z) -> if(le(s x, y, s z), s x, y, s z),
  if(second(), x, y, z) -> if(le(s x, s y, z), s x, s y, z),
               triple x -> if(le(x, x, double x), x, 0(), 0())}
 DP:
  DP:
   {    greater#(s x, s y) -> greater#(x, y),
            le#(0(), y, z) -> greater#(y, z),
        le#(s x, s y, s z) -> le#(x, y, z),
               double# s x -> double# x,
     if#(first(), x, y, z) -> le#(s x, y, s z),
     if#(first(), x, y, z) -> if#(le(s x, y, s z), s x, y, s z),
    if#(second(), x, y, z) -> le#(s x, s y, z),
    if#(second(), x, y, z) -> if#(le(s x, s y, z), s x, s y, z),
                 triple# x -> le#(x, x, double x),
                 triple# x -> double# x,
                 triple# x -> if#(le(x, x, double x), x, 0(), 0())}
  TRS:
  {      greater(x, 0()) -> first(),
       greater(0(), s y) -> second(),
       greater(s x, s y) -> greater(x, y),
           le(0(), y, z) -> greater(y, z),
         le(s x, 0(), z) -> false(),
       le(s x, s y, 0()) -> false(),
       le(s x, s y, s z) -> le(x, y, z),
              double 0() -> 0(),
              double s x -> s s double x,
    if(false(), x, y, z) -> true(),
    if(first(), x, y, z) -> if(le(s x, y, s z), s x, y, s z),
   if(second(), x, y, z) -> if(le(s x, s y, z), s x, s y, z),
                triple x -> if(le(x, x, double x), x, 0(), 0())}
  EDG:
   {(double# s x -> double# x, double# s x -> double# x)
    (triple# x -> double# x, double# s x -> double# x)
    (if#(first(), x, y, z) -> if#(le(s x, y, s z), s x, y, s z), if#(second(), x, y, z) -> if#(le(s x, s y, z), s x, s y, z))
    (if#(first(), x, y, z) -> if#(le(s x, y, s z), s x, y, s z), if#(second(), x, y, z) -> le#(s x, s y, z))
    (if#(first(), x, y, z) -> if#(le(s x, y, s z), s x, y, s z), if#(first(), x, y, z) -> if#(le(s x, y, s z), s x, y, s z))
    (if#(first(), x, y, z) -> if#(le(s x, y, s z), s x, y, s z), if#(first(), x, y, z) -> le#(s x, y, s z))
    (greater#(s x, s y) -> greater#(x, y), greater#(s x, s y) -> greater#(x, y))
    (triple# x -> le#(x, x, double x), le#(s x, s y, s z) -> le#(x, y, z))
    (triple# x -> le#(x, x, double x), le#(0(), y, z) -> greater#(y, z))
    (if#(second(), x, y, z) -> if#(le(s x, s y, z), s x, s y, z), if#(first(), x, y, z) -> le#(s x, y, s z))
    (if#(second(), x, y, z) -> if#(le(s x, s y, z), s x, s y, z), if#(first(), x, y, z) -> if#(le(s x, y, s z), s x, y, s z))
    (if#(second(), x, y, z) -> if#(le(s x, s y, z), s x, s y, z), if#(second(), x, y, z) -> le#(s x, s y, z))
    (if#(second(), x, y, z) -> if#(le(s x, s y, z), s x, s y, z), if#(second(), x, y, z) -> if#(le(s x, s y, z), s x, s y, z))
    (if#(first(), x, y, z) -> le#(s x, y, s z), le#(s x, s y, s z) -> le#(x, y, z))
    (triple# x -> if#(le(x, x, double x), x, 0(), 0()), if#(first(), x, y, z) -> le#(s x, y, s z))
    (triple# x -> if#(le(x, x, double x), x, 0(), 0()), if#(first(), x, y, z) -> if#(le(s x, y, s z), s x, y, s z))
    (triple# x -> if#(le(x, x, double x), x, 0(), 0()), if#(second(), x, y, z) -> le#(s x, s y, z))
    (triple# x -> if#(le(x, x, double x), x, 0(), 0()), if#(second(), x, y, z) -> if#(le(s x, s y, z), s x, s y, z))
    (le#(s x, s y, s z) -> le#(x, y, z), le#(0(), y, z) -> greater#(y, z))
    (le#(s x, s y, s z) -> le#(x, y, z), le#(s x, s y, s z) -> le#(x, y, z))
    (if#(second(), x, y, z) -> le#(s x, s y, z), le#(s x, s y, s z) -> le#(x, y, z))
    (le#(0(), y, z) -> greater#(y, z), greater#(s x, s y) -> greater#(x, y))}
   STATUS:
    arrows: 0.818182
    SCCS (4):
     Scc:
      { if#(first(), x, y, z) -> if#(le(s x, y, s z), s x, y, s z),
       if#(second(), x, y, z) -> if#(le(s x, s y, z), s x, s y, z)}
     Scc:
      {le#(s x, s y, s z) -> le#(x, y, z)}
     Scc:
      {double# s x -> double# x}
     Scc:
      {greater#(s x, s y) -> greater#(x, y)}
     
     
     
     SCC (2):
      Strict:
       { if#(first(), x, y, z) -> if#(le(s x, y, s z), s x, y, s z),
        if#(second(), x, y, z) -> if#(le(s x, s y, z), s x, s y, z)}
      Weak:
      {      greater(x, 0()) -> first(),
           greater(0(), s y) -> second(),
           greater(s x, s y) -> greater(x, y),
               le(0(), y, z) -> greater(y, z),
             le(s x, 0(), z) -> false(),
           le(s x, s y, 0()) -> false(),
           le(s x, s y, s z) -> le(x, y, z),
                  double 0() -> 0(),
                  double s x -> s s double x,
        if(false(), x, y, z) -> true(),
        if(first(), x, y, z) -> if(le(s x, y, s z), s x, y, s z),
       if(second(), x, y, z) -> if(le(s x, s y, z), s x, s y, z),
                    triple x -> if(le(x, x, double x), x, 0(), 0())}
      Open
     
     
     
     SCC (1):
      Strict:
       {le#(s x, s y, s z) -> le#(x, y, z)}
      Weak:
      {      greater(x, 0()) -> first(),
           greater(0(), s y) -> second(),
           greater(s x, s y) -> greater(x, y),
               le(0(), y, z) -> greater(y, z),
             le(s x, 0(), z) -> false(),
           le(s x, s y, 0()) -> false(),
           le(s x, s y, s z) -> le(x, y, z),
                  double 0() -> 0(),
                  double s x -> s s double x,
        if(false(), x, y, z) -> true(),
        if(first(), x, y, z) -> if(le(s x, y, s z), s x, y, s z),
       if(second(), x, y, z) -> if(le(s x, s y, z), s x, s y, z),
                    triple x -> if(le(x, x, double x), x, 0(), 0())}
      Open
     SCC (1):
      Strict:
       {double# s x -> double# x}
      Weak:
      {      greater(x, 0()) -> first(),
           greater(0(), s y) -> second(),
           greater(s x, s y) -> greater(x, y),
               le(0(), y, z) -> greater(y, z),
             le(s x, 0(), z) -> false(),
           le(s x, s y, 0()) -> false(),
           le(s x, s y, s z) -> le(x, y, z),
                  double 0() -> 0(),
                  double s x -> s s double x,
        if(false(), x, y, z) -> true(),
        if(first(), x, y, z) -> if(le(s x, y, s z), s x, y, s z),
       if(second(), x, y, z) -> if(le(s x, s y, z), s x, s y, z),
                    triple x -> if(le(x, x, double x), x, 0(), 0())}
      Open
     
     SCC (1):
      Strict:
       {greater#(s x, s y) -> greater#(x, y)}
      Weak:
      {      greater(x, 0()) -> first(),
           greater(0(), s y) -> second(),
           greater(s x, s y) -> greater(x, y),
               le(0(), y, z) -> greater(y, z),
             le(s x, 0(), z) -> false(),
           le(s x, s y, 0()) -> false(),
           le(s x, s y, s z) -> le(x, y, z),
                  double 0() -> 0(),
                  double s x -> s s double x,
        if(false(), x, y, z) -> true(),
        if(first(), x, y, z) -> if(le(s x, y, s z), s x, y, s z),
       if(second(), x, y, z) -> if(le(s x, s y, z), s x, s y, z),
                    triple x -> if(le(x, x, double x), x, 0(), 0())}
      Open