Input TRS:
    1: average(x,y) -> if(ge(x,y),x,y)
    2: if(true(),x,y) -> averIter(y,x,y)
    3: if(false(),x,y) -> averIter(x,y,x)
    4: averIter(x,y,z) -> ifIter(ge(x,y),x,y,z)
    5: ifIter(true(),x,y,z) -> z
    6: ifIter(false(),x,y,z) -> averIter(plus(x,s(s(s(0())))),plus(y,s(0())),plus(z,s(0())))
    7: append(nil(),y) -> y
    8: append(cons(n,x),y) -> cons(n,app(x,y))
    9: low(n,nil()) -> nil()
    10: low(n,cons(m,x)) -> if_low(ge(m,n),n,cons(m,x))
    11: if_low(false(),n,cons(m,x)) -> cons(m,low(n,x))
    12: if_low(true(),n,cons(m,x)) -> low(n,x)
    13: high(n,nil()) -> nil()
    14: high(n,cons(m,x)) -> if_high(ge(m,n),n,cons(m,x))
    15: if_high(false(),n,cons(m,x)) -> high(n,x)
    16: if_high(true(),n,cons(m,x)) -> cons(average(m,m),high(n,x))
    17: quicksort(x) -> ifquick(isempty(x),x)
    18: ifquick(true(),x) -> nil()
    19: ifquick(false(),x) -> append(quicksort(low(head(x),tail(x))),cons(tail(x),quicksort(high(head(x),tail(x)))))
    20: plus(0(),y) -> y
    21: plus(s(x),y) -> s(plus(x,y))
    22: isempty(nil()) -> true()
    23: isempty(cons(n,x)) -> false()
    24: head(nil()) -> error()
    25: head(cons(n,x)) -> n
    26: tail(nil()) -> nil()
    27: tail(cons(n,x)) -> x
    28: ge(x,0()) -> true()
    29: ge(0(),s(y)) -> false()
    30: ge(s(x),s(y)) -> ge(x,y)
    31: a() -> b()
    32: a() -> c()
Number of strict rules: 32
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #if(true(),x,y) -> #averIter(y,x,y)
   #2: #ifIter(false(),x,y,z) -> #averIter(plus(x,s(s(s(0())))),plus(y,s(0())),plus(z,s(0())))
   #3: #ifIter(false(),x,y,z) -> #plus(x,s(s(s(0()))))
   #4: #ifIter(false(),x,y,z) -> #plus(y,s(0()))
   #5: #ifIter(false(),x,y,z) -> #plus(z,s(0()))
   #6: #if_low(false(),n,cons(m,x)) -> #low(n,x)
   #7: #if_low(true(),n,cons(m,x)) -> #low(n,x)
   #8: #high(n,cons(m,x)) -> #if_high(ge(m,n),n,cons(m,x))
   #9: #high(n,cons(m,x)) -> #ge(m,n)
   #10: #ge(s(x),s(y)) -> #ge(x,y)
   #11: #low(n,cons(m,x)) -> #if_low(ge(m,n),n,cons(m,x))
   #12: #low(n,cons(m,x)) -> #ge(m,n)
   #13: #quicksort(x) -> #ifquick(isempty(x),x)
   #14: #quicksort(x) -> #isempty(x)
   #15: #ifquick(false(),x) -> #append(quicksort(low(head(x),tail(x))),cons(tail(x),quicksort(high(head(x),tail(x)))))
   #16: #ifquick(false(),x) -> #quicksort(low(head(x),tail(x)))
   #17: #ifquick(false(),x) -> #low(head(x),tail(x))
   #18: #ifquick(false(),x) -> #head(x)
   #19: #ifquick(false(),x) -> #tail(x)
   #20: #ifquick(false(),x) -> #tail(x)
   #21: #ifquick(false(),x) -> #quicksort(high(head(x),tail(x)))
   #22: #ifquick(false(),x) -> #high(head(x),tail(x))
   #23: #ifquick(false(),x) -> #head(x)
   #24: #ifquick(false(),x) -> #tail(x)
   #25: #plus(s(x),y) -> #plus(x,y)
   #26: #if_high(true(),n,cons(m,x)) -> #average(m,m)
   #27: #if_high(true(),n,cons(m,x)) -> #high(n,x)
   #28: #if(false(),x,y) -> #averIter(x,y,x)
   #29: #average(x,y) -> #if(ge(x,y),x,y)
   #30: #average(x,y) -> #ge(x,y)
   #31: #if_high(false(),n,cons(m,x)) -> #high(n,x)
   #32: #averIter(x,y,z) -> #ifIter(ge(x,y),x,y,z)
   #33: #averIter(x,y,z) -> #ge(x,y)
Number of SCCs: 6, DPs: 13, edges: 16
	SCC { #25 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
isempty(x1)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#append(x1,x2)	weight: 0
     b()	weight: 0
average(x1,x2)	weight: 0
if_high(x1,x2,x3)	weight: 0
ifIter(x1,x2,x3,x4)	weight: 0
#plus(x1,x2)	weight: x1
#isempty(x1)	weight: 0
#quicksort(x1)	weight: 0
#high(x1,x2)	weight: 0
#ifquick(x1,x2)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
  #ge(x1,x2)	weight: 0
ifquick(x1,x2)	weight: 0
#if_high(x1,x2,x3)	weight: 0
     c()	weight: 0
quicksort(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#ifIter(x1,x2,x3,x4)	weight: 0
 error()	weight: 0
append(x1,x2)	weight: 0
    if(x1,x2,x3)	weight: 0
     0()	weight: 0
  high(x1,x2)	weight: 0
    ge(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#average(x1,x2)	weight: 0
   low(x1,x2)	weight: 0
  plus(x1,x2)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
   #a()	weight: 0
averIter(x1,x2,x3)	weight: 0
if_low(x1,x2,x3)	weight: 0
#averIter(x1,x2,x3)	weight: 0
#if_low(x1,x2,x3)	weight: 0
 #low(x1,x2)	weight: 0
   app(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #25
Number of SCCs: 5, DPs: 12, edges: 15
	SCC { #10 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
isempty(x1)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#append(x1,x2)	weight: 0
     b()	weight: 0
average(x1,x2)	weight: 0
if_high(x1,x2,x3)	weight: 0
ifIter(x1,x2,x3,x4)	weight: 0
#plus(x1,x2)	weight: 0
#isempty(x1)	weight: 0
#quicksort(x1)	weight: 0
#high(x1,x2)	weight: 0
#ifquick(x1,x2)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
  #ge(x1,x2)	weight: x2
ifquick(x1,x2)	weight: 0
#if_high(x1,x2,x3)	weight: 0
     c()	weight: 0
quicksort(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#ifIter(x1,x2,x3,x4)	weight: 0
 error()	weight: 0
append(x1,x2)	weight: 0
    if(x1,x2,x3)	weight: 0
     0()	weight: 0
  high(x1,x2)	weight: 0
    ge(x1,x2)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
#average(x1,x2)	weight: 0
   low(x1,x2)	weight: 0
  plus(x1,x2)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
   #a()	weight: 0
averIter(x1,x2,x3)	weight: 0
if_low(x1,x2,x3)	weight: 0
#averIter(x1,x2,x3)	weight: 0
#if_low(x1,x2,x3)	weight: 0
 #low(x1,x2)	weight: 0
   app(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #10
Number of SCCs: 4, DPs: 11, edges: 14
	SCC { #13 #16 #21 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
     a()	weight: 0
isempty(x1)	weight: max{0, (/ 3 16) + x1}
     s(x1)	weight: (max (- (/ 1 32)) 0)
#append(x1,x2)	weight: 0
     b()	weight: 0
average(x1,x2)	weight: max{0, (/ 1 32) + x1, (/ 1 32) + x2}
if_high(x1,x2,x3)	weight: max{0, (/ 1 32) + x3}
ifIter(x1,x2,x3,x4)	weight: max{0, (/ 3 32) + x1, (- (/ 1 32)) + x2, (- (/ 1 32)) + x3}
#plus(x1,x2)	weight: 0
#isempty(x1)	weight: 0
#quicksort(x1)	weight: max{0, (/ 1 16) + x1}
#high(x1,x2)	weight: 0
#ifquick(x1,x2)	weight: max{0, (- (/ 7 32)) + x1, (/ 1 32) + x2}
 false()	weight: (/ 11 32)
#head(x1)	weight: 0
  #ge(x1,x2)	weight: 0
ifquick(x1,x2)	weight: 0
#if_high(x1,x2,x3)	weight: 0
     c()	weight: 0
quicksort(x1)	weight: 0
  true()	weight: (/ 3 16)
  tail(x1)	weight: max{0, (- (/ 1 8)) + x1}
#ifIter(x1,x2,x3,x4)	weight: 0
 error()	weight: (/ 1 32)
append(x1,x2)	weight: 0
    if(x1,x2,x3)	weight: max{0, (- (/ 3 8)) + x1, (- (/ 1 32)) + x2}
     0()	weight: (/ 3 32)
  high(x1,x2)	weight: max{0, (/ 1 32) + x2}
    ge(x1,x2)	weight: max{0, (- (/ 1 32)) + x1, (/ 1 16) + x2}
   nil()	weight: 0
#tail(x1)	weight: 0
#average(x1,x2)	weight: 0
   low(x1,x2)	weight: max{0, x2}
  plus(x1,x2)	weight: max{0, (- (/ 1 16)) + x2}
  head(x1)	weight: (max (- (/ 1 32)) 0)
  cons(x1,x2)	weight: max{0, (/ 5 32) + x2}
  #if(x1,x2,x3)	weight: 0
   #a()	weight: 0
averIter(x1,x2,x3)	weight: max{0, (/ 1 32) + x2}
if_low(x1,x2,x3)	weight: max{0, x3}
#averIter(x1,x2,x3)	weight: 0
#if_low(x1,x2,x3)	weight: 0
 #low(x1,x2)	weight: 0
   app(x1,x2)	weight: 0
    Usable rules: { 9..16 22 23 26 27 }
    Removed DPs: #13 #16 #21
Number of SCCs: 3, DPs: 8, edges: 10
	SCC { #2 #32 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed.
Removing edges: failed.
Finding a loop...  failed.
MAYBE