Input TRS:
    1: check(0()) -> zero()
    2: check(s(0())) -> odd()
    3: check(s(s(0()))) -> even()
    4: check(s(s(s(x)))) -> check(s(x))
    5: half(0()) -> 0()
    6: half(s(0())) -> 0()
    7: half(s(s(x))) -> s(half(x))
    8: plus(0(),y) -> y
    9: plus(s(x),y) -> s(plus(x,y))
    10: times(x,y) -> timesIter(x,y,0())
    11: timesIter(x,y,z) -> if(check(x),x,y,z,plus(z,y))
    12: p(s(x)) -> x
    13: p(0()) -> 0()
    14: if(zero(),x,y,z,u) -> z
    15: if(odd(),x,y,z,u) -> timesIter(p(x),y,u)
    16: if(even(),x,y,z,u) -> plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))
Number of strict rules: 16
Direct Order(PosReal,>,Poly) ... failed.
Freezing half check
1: check❆1_0() -> zero()
2: check❆1_s(0()) -> odd()
3: check❆1_s(s(0())) -> even()
4: check❆1_s(s(s(x))) -> check❆1_s(x)
5: half❆1_0() -> 0()
6: half❆1_s(0()) -> 0()
7: half❆1_s(s(x)) -> s(half(x))
8: plus(0(),y) -> y
9: plus(s(x),y) -> s(plus(x,y))
10: times(x,y) -> timesIter(x,y,0())
11: timesIter(x,y,z) -> if(check(x),x,y,z,plus(z,y))
12: p(s(x)) -> x
13: p(0()) -> 0()
14: if(zero(),x,y,z,u) -> z
15: if(odd(),x,y,z,u) -> timesIter(p(x),y,u)
16: if(even(),x,y,z,u) -> plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half❆1_s(z)))
17: check(0()) ->= check❆1_0()
18: check(s(_1)) ->= check❆1_s(_1)
19: half(0()) ->= half❆1_0()
20: half(s(_1)) ->= half❆1_s(_1)
Number of strict rules: 16
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #plus(s(x),y) -> #plus(x,y)
   #2: #timesIter(x,y,z) -> #if(check(x),x,y,z,plus(z,y))
   #3: #timesIter(x,y,z) -> #check(x)
   #4: #timesIter(x,y,z) -> #plus(z,y)
   #5: #half(s(_1)) ->? #half❆1_s(_1)
   #6: #half❆1_s(s(x)) -> #half(x)
   #7: #times(x,y) -> #timesIter(x,y,0())
   #8: #check(0()) ->? #check❆1_0()
   #9: #half(0()) ->? #half❆1_0()
   #10: #if(even(),x,y,z,u) -> #plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half❆1_s(z)))
   #11: #if(even(),x,y,z,u) -> #timesIter(half(x),y,half(z))
   #12: #if(even(),x,y,z,u) -> #half(x)
   #13: #if(even(),x,y,z,u) -> #half(z)
   #14: #if(even(),x,y,z,u) -> #timesIter(half(x),y,half❆1_s(z))
   #15: #if(even(),x,y,z,u) -> #half(x)
   #16: #if(even(),x,y,z,u) -> #half❆1_s(z)
   #17: #if(odd(),x,y,z,u) -> #timesIter(p(x),y,u)
   #18: #if(odd(),x,y,z,u) -> #p(x)
   #19: #check❆1_s(s(s(x))) -> #check❆1_s(x)
   #20: #check(s(_1)) ->? #check❆1_s(_1)
Number of SCCs: 4, DPs: 8, edges: 10
	SCC { #19 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
  zero()	weight: 0
timesIter(x1,x2,x3)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
#half❆1_s(x1)	weight: 0
#timesIter(x1,x2,x3)	weight: 0
  even()	weight: 0
#plus(x1,x2)	weight: 0
#check(x1)	weight: 0
check❆1_0()	weight: 0
#half(x1)	weight: 0
check❆1_s(x1)	weight: 0
   #p(x1)	weight: 0
#half❆1_0()	weight: 0
  half(x1)	weight: 0
half❆1_s(x1)	weight: 0
 check(x1)	weight: 0
     p(x1)	weight: 0
#times(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4,x5)	weight: 0
 times(x1,x2)	weight: 0
#check❆1_s(x1)	weight: x1
#check❆1_0()	weight: 0
  plus(x1,x2)	weight: 0
   odd()	weight: 0
  #if(x1,x2,x3,x4,x5)	weight: 0
half❆1_0()	weight: 0
    Usable rules: { }
    Removed DPs: #19
Number of SCCs: 3, DPs: 7, edges: 9
	SCC { #1 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
  zero()	weight: 0
timesIter(x1,x2,x3)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#half❆1_s(x1)	weight: 0
#timesIter(x1,x2,x3)	weight: 0
  even()	weight: 0
#plus(x1,x2)	weight: x1
#check(x1)	weight: 0
check❆1_0()	weight: 0
#half(x1)	weight: 0
check❆1_s(x1)	weight: 0
   #p(x1)	weight: 0
#half❆1_0()	weight: 0
  half(x1)	weight: 0
half❆1_s(x1)	weight: 0
 check(x1)	weight: 0
     p(x1)	weight: 0
#times(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4,x5)	weight: 0
 times(x1,x2)	weight: 0
#check❆1_s(x1)	weight: 0
#check❆1_0()	weight: 0
  plus(x1,x2)	weight: 0
   odd()	weight: 0
  #if(x1,x2,x3,x4,x5)	weight: 0
half❆1_0()	weight: 0
    Usable rules: { }
    Removed DPs: #1
Number of SCCs: 2, DPs: 6, edges: 8
	SCC { #5 #6 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
  zero()	weight: 0
timesIter(x1,x2,x3)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#half❆1_s(x1)	weight: x1
#timesIter(x1,x2,x3)	weight: 0
  even()	weight: 0
#plus(x1,x2)	weight: 0
#check(x1)	weight: 0
check❆1_0()	weight: 0
#half(x1)	weight: x1
check❆1_s(x1)	weight: 0
   #p(x1)	weight: 0
#half❆1_0()	weight: 0
  half(x1)	weight: 0
half❆1_s(x1)	weight: 0
 check(x1)	weight: 0
     p(x1)	weight: 0
#times(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4,x5)	weight: 0
 times(x1,x2)	weight: 0
#check❆1_s(x1)	weight: 0
#check❆1_0()	weight: 0
  plus(x1,x2)	weight: 0
   odd()	weight: 0
  #if(x1,x2,x3,x4,x5)	weight: 0
half❆1_0()	weight: 0
    Usable rules: { }
    Removed DPs: #5 #6
Number of SCCs: 1, DPs: 4, edges: 6
	SCC { #2 #11 #14 #17 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
  zero()	weight: 0
timesIter(x1,x2,x3)	weight: 0
     s(x1)	weight: max{0, (/ 3 8) + x1}
#half❆1_s(x1)	weight: 0
#timesIter(x1,x2,x3)	weight: max{0, x1}
  even()	weight: (/ 3 8)
#plus(x1,x2)	weight: 0
#check(x1)	weight: 0
check❆1_0()	weight: (/ 1 8)
#half(x1)	weight: 0
check❆1_s(x1)	weight: max{0, (/ 1 4) + x1}
   #p(x1)	weight: 0
#half❆1_0()	weight: 0
  half(x1)	weight: max{0, (- (/ 1 8)) + x1}
half❆1_s(x1)	weight: max{0, (/ 1 8) + x1}
 check(x1)	weight: max{0, (/ 1 8) + x1}
     p(x1)	weight: max{0, (- (/ 1 8)) + x1}
#times(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4,x5)	weight: 0
 times(x1,x2)	weight: 0
#check❆1_s(x1)	weight: 0
#check❆1_0()	weight: 0
  plus(x1,x2)	weight: max{0, (- (/ 1 2)) + x1}
   odd()	weight: (/ 1 4)
  #if(x1,x2,x3,x4,x5)	weight: max{0, (- (/ 1 8)) + x1, x2}
half❆1_0()	weight: 0
    Usable rules: { 1..7 12 13 17..20 }
    Removed DPs: #11 #14 #17
Number of SCCs: 0, DPs: 0, edges: 0
YES