Input TRS:
    1: car(cons(x,l)) -> x
    2: cddr(nil()) -> nil()
    3: cddr(cons(x,nil())) -> nil()
    4: cddr(cons(x,cons(y,l))) -> l
    5: cadr(cons(x,cons(y,l))) -> y
    6: isZero(|0|()) -> true()
    7: isZero(s(x)) -> false()
    8: plus(x,y) -> ifplus(isZero(x),x,y)
    9: ifplus(true(),x,y) -> y
    10: ifplus(false(),x,y) -> s(plus(p(x),y))
    11: times(x,y) -> iftimes(isZero(x),x,y)
    12: iftimes(true(),x,y) -> |0|()
    13: iftimes(false(),x,y) -> plus(y,times(p(x),y))
    14: p(s(x)) -> x
    15: p(|0|()) -> |0|()
    16: shorter(nil(),y) -> true()
    17: shorter(cons(x,l),|0|()) -> false()
    18: shorter(cons(x,l),s(y)) -> shorter(l,y)
    19: prod(l) -> if(shorter(l,|0|()),shorter(l,s(|0|())),l)
    20: if(true(),b,l) -> s(|0|())
    21: if(false(),b,l) -> if2(b,l)
    22: if2(true(),l) -> car(l)
    23: if2(false(),l) -> prod(cons(times(car(l),cadr(l)),cddr(l)))
Number of strict rules: 23
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #iftimes(false(),x,y) -> #plus(y,times(p(x),y))
   #2: #iftimes(false(),x,y) -> #times(p(x),y)
   #3: #iftimes(false(),x,y) -> #p(x)
   #4: #times(x,y) -> #iftimes(isZero(x),x,y)
   #5: #times(x,y) -> #isZero(x)
   #6: #if2(false(),l) -> #prod(cons(times(car(l),cadr(l)),cddr(l)))
   #7: #if2(false(),l) -> #times(car(l),cadr(l))
   #8: #if2(false(),l) -> #car(l)
   #9: #if2(false(),l) -> #cadr(l)
   #10: #if2(false(),l) -> #cddr(l)
   #11: #ifplus(false(),x,y) -> #plus(p(x),y)
   #12: #ifplus(false(),x,y) -> #p(x)
   #13: #if2(true(),l) -> #car(l)
   #14: #prod(l) -> #if(shorter(l,|0|()),shorter(l,s(|0|())),l)
   #15: #prod(l) -> #shorter(l,|0|())
   #16: #prod(l) -> #shorter(l,s(|0|()))
   #17: #if(false(),b,l) -> #if2(b,l)
   #18: #plus(x,y) -> #ifplus(isZero(x),x,y)
   #19: #plus(x,y) -> #isZero(x)
   #20: #shorter(cons(x,l),s(y)) -> #shorter(l,y)
Number of SCCs: 4, DPs: 8, edges: 8
	SCC { #20 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
  prod(x1)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
iftimes(x1,x2,x3)	weight: 0
#isZero(x1)	weight: 0
#prod(x1)	weight: 0
#cadr(x1)	weight: 0
  cddr(x1)	weight: 0
#plus(x1,x2)	weight: 0
 false()	weight: 0
   #p(x1)	weight: 0
  true()	weight: 0
#shorter(x1,x2)	weight: x2
#iftimes(x1,x2,x3)	weight: 0
   if2(x1,x2)	weight: 0
ifplus(x1,x2,x3)	weight: 0
     p(x1)	weight: 0
#times(x1,x2)	weight: 0
    if(x1,x2,x3)	weight: 0
shorter(x1,x2)	weight: 0
 times(x1,x2)	weight: 0
   nil()	weight: 0
#ifplus(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
#cddr(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 2)
  #if(x1,x2,x3)	weight: 0
isZero(x1)	weight: 0
  cadr(x1)	weight: 0
 #car(x1)	weight: 0
 #if2(x1,x2)	weight: 0
   car(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #20
Number of SCCs: 3, DPs: 7, edges: 7
	SCC { #11 #18 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
   |0|()	weight: 0
  prod(x1)	weight: 0
     s(x1)	weight: max{0, (/ 1 2) + x1}
iftimes(x1,x2,x3)	weight: 0
#isZero(x1)	weight: 0
#prod(x1)	weight: 0
#cadr(x1)	weight: 0
  cddr(x1)	weight: 0
#plus(x1,x2)	weight: max{0, (/ 3 8) + x1}
 false()	weight: (/ 1 4)
   #p(x1)	weight: 0
  true()	weight: 0
#shorter(x1,x2)	weight: 0
#iftimes(x1,x2,x3)	weight: 0
   if2(x1,x2)	weight: 0
ifplus(x1,x2,x3)	weight: 0
     p(x1)	weight: max{0, (- (/ 1 2)) + x1}
#times(x1,x2)	weight: 0
    if(x1,x2,x3)	weight: 0
shorter(x1,x2)	weight: 0
 times(x1,x2)	weight: 0
   nil()	weight: 0
#ifplus(x1,x2,x3)	weight: max{0, (/ 1 4) + x1, (/ 3 8) + x2}
  plus(x1,x2)	weight: 0
#cddr(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
isZero(x1)	weight: max{0, (- (/ 1 8)) + x1}
  cadr(x1)	weight: 0
 #car(x1)	weight: 0
 #if2(x1,x2)	weight: 0
   car(x1)	weight: 0
    Usable rules: { 6 7 14 15 }
    Removed DPs: #11
Number of SCCs: 2, DPs: 5, edges: 5
	SCC { #2 #4 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
   |0|()	weight: 0
  prod(x1)	weight: 0
     s(x1)	weight: max{0, (/ 1 2) + x1}
iftimes(x1,x2,x3)	weight: 0
#isZero(x1)	weight: 0
#prod(x1)	weight: 0
#cadr(x1)	weight: 0
  cddr(x1)	weight: 0
#plus(x1,x2)	weight: max{0, x1}
 false()	weight: (/ 1 8)
   #p(x1)	weight: 0
  true()	weight: 0
#shorter(x1,x2)	weight: 0
#iftimes(x1,x2,x3)	weight: max{0, (/ 1 4) + x1, (/ 1 8) + x2}
   if2(x1,x2)	weight: 0
ifplus(x1,x2,x3)	weight: 0
     p(x1)	weight: max{0, (- (/ 3 8)) + x1}
#times(x1,x2)	weight: max{0, (/ 1 4) + x1}
    if(x1,x2,x3)	weight: 0
shorter(x1,x2)	weight: 0
 times(x1,x2)	weight: 0
   nil()	weight: 0
#ifplus(x1,x2,x3)	weight: max{0, x1}
  plus(x1,x2)	weight: 0
#cddr(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
isZero(x1)	weight: max{0, (- (/ 3 8)) + x1}
  cadr(x1)	weight: 0
 #car(x1)	weight: 0
 #if2(x1,x2)	weight: 0
   car(x1)	weight: 0
    Usable rules: { 6 7 14 15 }
    Removed DPs: #2
Number of SCCs: 1, DPs: 3, edges: 3
	SCC { #6 #14 #17 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
   |0|()	weight: (/ 3 8)
  prod(x1)	weight: 0
     s(x1)	weight: max{0, (- (/ 1 2)) + x1}
iftimes(x1,x2,x3)	weight: max{0, (/ 1 8) + x2, (/ 1 8) + x3}
#isZero(x1)	weight: 0
#prod(x1)	weight: max{0, (/ 1 2) + x1}
#cadr(x1)	weight: 0
  cddr(x1)	weight: max{0, (- (/ 5 4)) + x1}
#plus(x1,x2)	weight: 0
 false()	weight: (/ 11 8)
   #p(x1)	weight: 0
  true()	weight: (/ 3 8)
#shorter(x1,x2)	weight: 0
#iftimes(x1,x2,x3)	weight: 0
   if2(x1,x2)	weight: 0
ifplus(x1,x2,x3)	weight: max{0, -2 + x1, (/ 1 8) + x2}
     p(x1)	weight: (max (- (/ 1 8)) 0)
#times(x1,x2)	weight: 0
    if(x1,x2,x3)	weight: 0
shorter(x1,x2)	weight: max{0, (/ 3 8) + x2 + x1}
 times(x1,x2)	weight: 0
   nil()	weight: 0
#ifplus(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
#cddr(x1)	weight: 0
  cons(x1,x2)	weight: max{0, (/ 5 8) + x2}
  #if(x1,x2,x3)	weight: max{0, (/ 1 8) + x2, (/ 3 8) + x3}
isZero(x1)	weight: max{0, (- (/ 1 8)) + x1}
  cadr(x1)	weight: (max (/ 1 4) 0)
 #car(x1)	weight: 0
 #if2(x1,x2)	weight: max{0, (- (/ 1 8)) + x1, (/ 1 4) + x2}
   car(x1)	weight: (max (- (/ 3 8)) 0)
    Usable rules: { 2..4 16..18 }
    Removed DPs: #6 #17
Number of SCCs: 0, DPs: 0, edges: 0
YES