Input TRS:
    1: isEmpty(cons(x,xs)) -> false()
    2: isEmpty(nil()) -> true()
    3: isZero(0()) -> true()
    4: isZero(s(x)) -> false()
    5: head(cons(x,xs)) -> x
    6: tail(cons(x,xs)) -> xs
    7: tail(nil()) -> nil()
    8: append(nil(),x) -> cons(x,nil())
    9: append(cons(y,ys),x) -> cons(y,append(ys,x))
    10: p(s(s(x))) -> s(p(s(x)))
    11: p(s(0())) -> 0()
    12: p(0()) -> 0()
    13: inc(s(x)) -> s(inc(x))
    14: inc(0()) -> s(0())
    15: addLists(xs,ys,zs) -> if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
    16: if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs
    17: if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
    18: if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
    19: if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
    20: if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
    21: addList(xs,ys) -> addLists(xs,ys,nil())
Number of strict rules: 21
Direct Order(PosReal,>,Poly) ... failed.
Freezing p
1: isEmpty(cons(x,xs)) -> false()
2: isEmpty(nil()) -> true()
3: isZero(0()) -> true()
4: isZero(s(x)) -> false()
5: head(cons(x,xs)) -> x
6: tail(cons(x,xs)) -> xs
7: tail(nil()) -> nil()
8: append(nil(),x) -> cons(x,nil())
9: append(cons(y,ys),x) -> cons(y,append(ys,x))
10: p❆1_s(s(x)) -> s(p❆1_s(x))
11: p❆1_s(0()) -> 0()
12: p❆1_0() -> 0()
13: inc(s(x)) -> s(inc(x))
14: inc(0()) -> s(0())
15: addLists(xs,ys,zs) -> if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
16: if(true(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> zs
17: if(true(),false(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
18: if(false(),true(),b,xs,ys,xs2,ys2,zs,zs2) -> differentLengthError()
19: if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs2,ys2,zs)
20: if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> addLists(xs,ys,zs2)
21: addList(xs,ys) -> addLists(xs,ys,nil())
22: p(0()) ->= p❆1_0()
23: p(s(_1)) ->= p❆1_s(_1)
Number of strict rules: 21
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #inc(s(x)) -> #inc(x)
   #2: #append(cons(y,ys),x) -> #append(ys,x)
   #3: #p(s(_1)) ->? #p❆1_s(_1)
   #4: #if(false(),false(),true(),xs,ys,xs2,ys2,zs,zs2) -> #addLists(xs,ys,zs2)
   #5: #p❆1_s(s(x)) -> #p❆1_s(x)
   #6: #p(0()) ->? #p❆1_0()
   #7: #if(false(),false(),false(),xs,ys,xs2,ys2,zs,zs2) -> #addLists(xs2,ys2,zs)
   #8: #addList(xs,ys) -> #addLists(xs,ys,nil())
   #9: #addLists(xs,ys,zs) -> #if(isEmpty(xs),isEmpty(ys),isZero(head(xs)),tail(xs),tail(ys),cons(p(head(xs)),tail(xs)),cons(inc(head(ys)),tail(ys)),zs,append(zs,head(ys)))
   #10: #addLists(xs,ys,zs) -> #isEmpty(xs)
   #11: #addLists(xs,ys,zs) -> #isEmpty(ys)
   #12: #addLists(xs,ys,zs) -> #isZero(head(xs))
   #13: #addLists(xs,ys,zs) -> #head(xs)
   #14: #addLists(xs,ys,zs) -> #tail(xs)
   #15: #addLists(xs,ys,zs) -> #tail(ys)
   #16: #addLists(xs,ys,zs) -> #p(head(xs))
   #17: #addLists(xs,ys,zs) -> #head(xs)
   #18: #addLists(xs,ys,zs) -> #tail(xs)
   #19: #addLists(xs,ys,zs) -> #inc(head(ys))
   #20: #addLists(xs,ys,zs) -> #head(ys)
   #21: #addLists(xs,ys,zs) -> #tail(ys)
   #22: #addLists(xs,ys,zs) -> #append(zs,head(ys))
   #23: #addLists(xs,ys,zs) -> #head(ys)
Number of SCCs: 4, DPs: 6, edges: 7
	SCC { #1 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 2) + x1
#append(x1,x2)	weight: 0
#isZero(x1)	weight: 0
p❆1_s(x1)	weight: 0
#isEmpty(x1)	weight: 0
#p❆1_0()	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
isEmpty(x1)	weight: 0
addList(x1,x2)	weight: 0
 #inc(x1)	weight: x1
   #p(x1)	weight: 0
   inc(x1)	weight: 0
#p❆1_s(x1)	weight: 0
  true()	weight: 0
differentLengthError()	weight: 0
     p(x1)	weight: 0
  tail(x1)	weight: 0
append(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4,x5,x6,x7,x8,x9)	weight: 0
p❆1_0()	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
addLists(x1,x2,x3)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3,x4,x5,x6,x7,x8,x9)	weight: 0
isZero(x1)	weight: 0
#addList(x1,x2)	weight: 0
#addLists(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #1
Number of SCCs: 3, DPs: 5, edges: 6
	SCC { #5 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 2) + x1
#append(x1,x2)	weight: 0
#isZero(x1)	weight: 0
p❆1_s(x1)	weight: 0
#isEmpty(x1)	weight: 0
#p❆1_0()	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
isEmpty(x1)	weight: 0
addList(x1,x2)	weight: 0
 #inc(x1)	weight: 0
   #p(x1)	weight: 0
   inc(x1)	weight: 0
#p❆1_s(x1)	weight: x1
  true()	weight: 0
differentLengthError()	weight: 0
     p(x1)	weight: 0
  tail(x1)	weight: 0
append(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4,x5,x6,x7,x8,x9)	weight: 0
p❆1_0()	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
addLists(x1,x2,x3)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3,x4,x5,x6,x7,x8,x9)	weight: 0
isZero(x1)	weight: 0
#addList(x1,x2)	weight: 0
#addLists(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #5
Number of SCCs: 2, DPs: 4, edges: 5
	SCC { #2 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 2)
#append(x1,x2)	weight: x1
#isZero(x1)	weight: 0
p❆1_s(x1)	weight: 0
#isEmpty(x1)	weight: 0
#p❆1_0()	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
isEmpty(x1)	weight: 0
addList(x1,x2)	weight: 0
 #inc(x1)	weight: 0
   #p(x1)	weight: 0
   inc(x1)	weight: 0
#p❆1_s(x1)	weight: 0
  true()	weight: 0
differentLengthError()	weight: 0
     p(x1)	weight: 0
  tail(x1)	weight: 0
append(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4,x5,x6,x7,x8,x9)	weight: 0
p❆1_0()	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
addLists(x1,x2,x3)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 2) + x2
  #if(x1,x2,x3,x4,x5,x6,x7,x8,x9)	weight: 0
isZero(x1)	weight: 0
#addList(x1,x2)	weight: 0
#addLists(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #2
Number of SCCs: 1, DPs: 3, edges: 4
	SCC { #4 #7 #9 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
     s(x1)	weight: (max (/ 3 8) 0)
#append(x1,x2)	weight: 0
#isZero(x1)	weight: 0
p❆1_s(x1)	weight: (max (/ 3 8) 0)
#isEmpty(x1)	weight: 0
#p❆1_0()	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
isEmpty(x1)	weight: max{0, (- (/ 3 8)) + x1}
addList(x1,x2)	weight: 0
 #inc(x1)	weight: 0
   #p(x1)	weight: 0
   inc(x1)	weight: (max (/ 3 8) 0)
#p❆1_s(x1)	weight: 0
  true()	weight: (/ 1 8)
differentLengthError()	weight: 0
     p(x1)	weight: max{0, x1}
  tail(x1)	weight: max{0, (- (/ 5 16)) + x1}
append(x1,x2)	weight: max{0, (- (/ 1 4)) + x2}
     0()	weight: (/ 3 8)
    if(x1,x2,x3,x4,x5,x6,x7,x8,x9)	weight: 0
p❆1_0()	weight: (/ 3 8)
   nil()	weight: 0
#tail(x1)	weight: 0
addLists(x1,x2,x3)	weight: 0
  head(x1)	weight: max{0, (- (/ 1 8)) + x1}
  cons(x1,x2)	weight: max{0, (/ 1 8) + x1, (/ 5 16) + x2}
  #if(x1,x2,x3,x4,x5,x6,x7,x8,x9)	weight: max{0, (- (/ 1 16)) + x3, (- (/ 5 16)) + x4, (- (/ 5 16)) + x5, (- (/ 3 8)) + x6, (- (/ 9 16)) + x7}
isZero(x1)	weight: max{0, (- (/ 1 4)) + x1}
#addList(x1,x2)	weight: 0
#addLists(x1,x2,x3)	weight: max{0, (- (/ 3 8)) + x1, (- (/ 9 16)) + x2}
    Usable rules: { 3..7 10..14 22 23 }
    Removed DPs: #4
Number of SCCs: 1, DPs: 2, edges: 2
	SCC { #7 #9 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
     s(x1)	weight: max{0, (/ 1 4) + x1}
#append(x1,x2)	weight: 0
#isZero(x1)	weight: 0
p❆1_s(x1)	weight: max{0, x1}
#isEmpty(x1)	weight: 0
#p❆1_0()	weight: 0
 false()	weight: (/ 3 16)
#head(x1)	weight: 0
isEmpty(x1)	weight: max{0, (- (/ 1 8)) + x1}
addList(x1,x2)	weight: 0
 #inc(x1)	weight: 0
   #p(x1)	weight: 0
   inc(x1)	weight: (max (/ 1 4) 0)
#p❆1_s(x1)	weight: 0
  true()	weight: (/ 1 16)
differentLengthError()	weight: 0
     p(x1)	weight: max{0, (- (/ 1 4)) + x1}
  tail(x1)	weight: (max (- (/ 1 16)) 0)
append(x1,x2)	weight: max{0, (/ 3 16) + x2}
     0()	weight: 0
    if(x1,x2,x3,x4,x5,x6,x7,x8,x9)	weight: 0
p❆1_0()	weight: 0
   nil()	weight: (/ 1 8)
#tail(x1)	weight: 0
addLists(x1,x2,x3)	weight: 0
  head(x1)	weight: max{0, (- (/ 1 8)) + x1}
  cons(x1,x2)	weight: max{0, (/ 1 8) + x1}
  #if(x1,x2,x3,x4,x5,x6,x7,x8,x9)	weight: max{0, (- (/ 1 8)) + x3, (- (/ 1 8)) + x6}
isZero(x1)	weight: max{0, (/ 1 16) + x1}
#addList(x1,x2)	weight: 0
#addLists(x1,x2,x3)	weight: max{0, (- (/ 3 16)) + x1}
    Usable rules: { 3..5 10..12 22 23 }
    Removed DPs: #7
Number of SCCs: 0, DPs: 0, edges: 0
YES