MAYBE
Time: 0.003809
TRS:
 {         gt(0(), y) -> false(),
         gt(s x, 0()) -> true(),
         gt(s x, s y) -> gt(x, y),
         plus(0(), y) -> y,
         plus(s x, y) -> s plus(x, y),
           double 0() -> 0(),
           double s x -> s s double x,
         aver(sum, z) -> if(gt(sum, double z), sum, z),
        average(x, y) -> aver(plus(x, y), 0()),
  if(false(), sum, z) -> z,
   if(true(), sum, z) -> aver(sum, s z)}
 DP:
  DP:
   {      gt#(s x, s y) -> gt#(x, y),
          plus#(s x, y) -> plus#(x, y),
            double# s x -> double# x,
          aver#(sum, z) -> gt#(sum, double z),
          aver#(sum, z) -> double# z,
          aver#(sum, z) -> if#(gt(sum, double z), sum, z),
         average#(x, y) -> plus#(x, y),
         average#(x, y) -> aver#(plus(x, y), 0()),
    if#(true(), sum, z) -> aver#(sum, s z)}
  TRS:
  {         gt(0(), y) -> false(),
          gt(s x, 0()) -> true(),
          gt(s x, s y) -> gt(x, y),
          plus(0(), y) -> y,
          plus(s x, y) -> s plus(x, y),
            double 0() -> 0(),
            double s x -> s s double x,
          aver(sum, z) -> if(gt(sum, double z), sum, z),
         average(x, y) -> aver(plus(x, y), 0()),
   if(false(), sum, z) -> z,
    if(true(), sum, z) -> aver(sum, s z)}
  EDG:
   {(average#(x, y) -> aver#(plus(x, y), 0()), aver#(sum, z) -> if#(gt(sum, double z), sum, z))
    (average#(x, y) -> aver#(plus(x, y), 0()), aver#(sum, z) -> double# z)
    (average#(x, y) -> aver#(plus(x, y), 0()), aver#(sum, z) -> gt#(sum, double z))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (double# s x -> double# x, double# s x -> double# x)
    (aver#(sum, z) -> gt#(sum, double z), gt#(s x, s y) -> gt#(x, y))
    (if#(true(), sum, z) -> aver#(sum, s z), aver#(sum, z) -> gt#(sum, double z))
    (if#(true(), sum, z) -> aver#(sum, s z), aver#(sum, z) -> double# z)
    (if#(true(), sum, z) -> aver#(sum, s z), aver#(sum, z) -> if#(gt(sum, double z), sum, z))
    (aver#(sum, z) -> double# z, double# s x -> double# x)
    (average#(x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (gt#(s x, s y) -> gt#(x, y), gt#(s x, s y) -> gt#(x, y))
    (aver#(sum, z) -> if#(gt(sum, double z), sum, z), if#(true(), sum, z) -> aver#(sum, s z))}
   STATUS:
    arrows: 0.839506
    SCCS (4):
     Scc:
      {plus#(s x, y) -> plus#(x, y)}
     Scc:
      {      aver#(sum, z) -> if#(gt(sum, double z), sum, z),
       if#(true(), sum, z) -> aver#(sum, s z)}
     Scc:
      {double# s x -> double# x}
     Scc:
      {gt#(s x, s y) -> gt#(x, y)}
     
     
     SCC (1):
      Strict:
       {plus#(s x, y) -> plus#(x, y)}
      Weak:
      {         gt(0(), y) -> false(),
              gt(s x, 0()) -> true(),
              gt(s x, s y) -> gt(x, y),
              plus(0(), y) -> y,
              plus(s x, y) -> s plus(x, y),
                double 0() -> 0(),
                double s x -> s s double x,
              aver(sum, z) -> if(gt(sum, double z), sum, z),
             average(x, y) -> aver(plus(x, y), 0()),
       if(false(), sum, z) -> z,
        if(true(), sum, z) -> aver(sum, s z)}
      Open
     
     SCC (2):
      Strict:
       {      aver#(sum, z) -> if#(gt(sum, double z), sum, z),
        if#(true(), sum, z) -> aver#(sum, s z)}
      Weak:
      {         gt(0(), y) -> false(),
              gt(s x, 0()) -> true(),
              gt(s x, s y) -> gt(x, y),
              plus(0(), y) -> y,
              plus(s x, y) -> s plus(x, y),
                double 0() -> 0(),
                double s x -> s s double x,
              aver(sum, z) -> if(gt(sum, double z), sum, z),
             average(x, y) -> aver(plus(x, y), 0()),
       if(false(), sum, z) -> z,
        if(true(), sum, z) -> aver(sum, s z)}
      Open
     
     SCC (1):
      Strict:
       {double# s x -> double# x}
      Weak:
      {         gt(0(), y) -> false(),
              gt(s x, 0()) -> true(),
              gt(s x, s y) -> gt(x, y),
              plus(0(), y) -> y,
              plus(s x, y) -> s plus(x, y),
                double 0() -> 0(),
                double s x -> s s double x,
              aver(sum, z) -> if(gt(sum, double z), sum, z),
             average(x, y) -> aver(plus(x, y), 0()),
       if(false(), sum, z) -> z,
        if(true(), sum, z) -> aver(sum, s z)}
      Open
     
     SCC (1):
      Strict:
       {gt#(s x, s y) -> gt#(x, y)}
      Weak:
      {         gt(0(), y) -> false(),
              gt(s x, 0()) -> true(),
              gt(s x, s y) -> gt(x, y),
              plus(0(), y) -> y,
              plus(s x, y) -> s plus(x, y),
                double 0() -> 0(),
                double s x -> s s double x,
              aver(sum, z) -> if(gt(sum, double z), sum, z),
             average(x, y) -> aver(plus(x, y), 0()),
       if(false(), sum, z) -> z,
        if(true(), sum, z) -> aver(sum, s z)}
      Open