Input TRS:
    1: plus(x,y) -> ifPlus(isZero(x),x,inc(y))
    2: ifPlus(true(),x,y) -> p(y)
    3: ifPlus(false(),x,y) -> plus(p(x),y)
    4: times(x,y) -> timesIter(0(),x,y,0())
    5: timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
    6: ifTimes(true(),i,x,y,z) -> z
    7: ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
    8: isZero(0()) -> true()
    9: isZero(s(0())) -> false()
    10: isZero(s(s(x))) -> isZero(s(x))
    11: inc(0()) -> s(0())
    12: inc(s(x)) -> s(inc(x))
    13: inc(x) -> s(x)
    14: p(0()) -> 0()
    15: p(s(x)) -> x
    16: p(s(s(x))) -> s(p(s(x)))
    17: ge(x,0()) -> true()
    18: ge(0(),s(y)) -> false()
    19: ge(s(x),s(y)) -> ge(x,y)
    20: f0(0(),y,x) -> f1(x,y,x)
    21: f1(x,y,z) -> f2(x,y,z)
    22: f2(x,1(),z) -> f0(x,z,z)
    23: f0(x,y,z) -> d()
    24: f1(x,y,z) -> c()
Number of strict rules: 24
Direct Order(PosReal,>,Poly) ... failed.
Freezing isZero p
1: plus(x,y) -> ifPlus(isZero(x),x,inc(y))
2: ifPlus(true(),x,y) -> p(y)
3: ifPlus(false(),x,y) -> plus(p(x),y)
4: times(x,y) -> timesIter(0(),x,y,0())
5: timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
6: ifTimes(true(),i,x,y,z) -> z
7: ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
8: isZero❆1_0() -> true()
9: isZero❆1_s(0()) -> false()
10: isZero❆1_s(s(x)) -> isZero❆1_s(x)
11: inc(0()) -> s(0())
12: inc(s(x)) -> s(inc(x))
13: inc(x) -> s(x)
14: p❆1_0() -> 0()
15: p❆1_s(x) -> x
16: p❆1_s(s(x)) -> s(p❆1_s(x))
17: ge(x,0()) -> true()
18: ge(0(),s(y)) -> false()
19: ge(s(x),s(y)) -> ge(x,y)
20: f0(0(),y,x) -> f1(x,y,x)
21: f1(x,y,z) -> f2(x,y,z)
22: f2(x,1(),z) -> f0(x,z,z)
23: f0(x,y,z) -> d()
24: f1(x,y,z) -> c()
25: p(0()) ->= p❆1_0()
26: p(s(_1)) ->= p❆1_s(_1)
27: isZero(0()) ->= isZero❆1_0()
28: isZero(s(_1)) ->= isZero❆1_s(_1)
Number of strict rules: 24
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #ifPlus(true(),x,y) -> #p(y)
   #2: #inc(s(x)) -> #inc(x)
   #3: #p(0()) ->? #p❆1_0()
   #4: #f0(0(),y,x) -> #f1(x,y,x)
   #5: #ifTimes(false(),i,x,y,z) -> #timesIter(inc(i),x,y,plus(z,y))
   #6: #ifTimes(false(),i,x,y,z) -> #inc(i)
   #7: #ifTimes(false(),i,x,y,z) -> #plus(z,y)
   #8: #isZero❆1_s(s(x)) -> #isZero❆1_s(x)
   #9: #timesIter(i,x,y,z) -> #ifTimes(ge(i,x),i,x,y,z)
   #10: #timesIter(i,x,y,z) -> #ge(i,x)
   #11: #isZero(s(_1)) ->? #isZero❆1_s(_1)
   #12: #f2(x,1(),z) -> #f0(x,z,z)
   #13: #isZero(0()) ->? #isZero❆1_0()
   #14: #ge(s(x),s(y)) -> #ge(x,y)
   #15: #p(s(_1)) ->? #p❆1_s(_1)
   #16: #f1(x,y,z) -> #f2(x,y,z)
   #17: #p❆1_s(s(x)) -> #p❆1_s(x)
   #18: #ifPlus(false(),x,y) -> #plus(p(x),y)
   #19: #ifPlus(false(),x,y) -> #p(x)
   #20: #plus(x,y) -> #ifPlus(isZero(x),x,inc(y))
   #21: #plus(x,y) -> #isZero(x)
   #22: #plus(x,y) -> #inc(y)
   #23: #times(x,y) -> #timesIter(0(),x,y,0())
Number of SCCs: 7, DPs: 11, edges: 11
	SCC { #17 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
ifTimes(x1,x2,x3,x4,x5)	weight: 0
     1()	weight: 0
     d()	weight: 0
timesIter(x1,x2,x3,x4)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#isZero(x1)	weight: 0
  #f2(x1,x2,x3)	weight: 0
p❆1_s(x1)	weight: 0
#p❆1_0()	weight: 0
#timesIter(x1,x2,x3,x4)	weight: 0
#plus(x1,x2)	weight: 0
 false()	weight: 0
  #ge(x1,x2)	weight: 0
 #inc(x1)	weight: 0
     c()	weight: 0
   #p(x1)	weight: 0
   inc(x1)	weight: 0
#p❆1_s(x1)	weight: x1
  true()	weight: 0
     p(x1)	weight: 0
#times(x1,x2)	weight: 0
     0()	weight: 0
    ge(x1,x2)	weight: 0
 times(x1,x2)	weight: 0
p❆1_0()	weight: 0
#isZero❆1_s(x1)	weight: 0
isZero❆1_0()	weight: 0
ifPlus(x1,x2,x3)	weight: 0
    f0(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
  #f1(x1,x2,x3)	weight: 0
#isZero❆1_0()	weight: 0
isZero❆1_s(x1)	weight: 0
#ifPlus(x1,x2,x3)	weight: 0
isZero(x1)	weight: 0
    f2(x1,x2,x3)	weight: 0
    f1(x1,x2,x3)	weight: 0
  #f0(x1,x2,x3)	weight: 0
#ifTimes(x1,x2,x3,x4,x5)	weight: 0
    Usable rules: { }
    Removed DPs: #17
Number of SCCs: 6, DPs: 10, edges: 10
	SCC { #2 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
ifTimes(x1,x2,x3,x4,x5)	weight: 0
     1()	weight: 0
     d()	weight: 0
timesIter(x1,x2,x3,x4)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#isZero(x1)	weight: 0
  #f2(x1,x2,x3)	weight: 0
p❆1_s(x1)	weight: 0
#p❆1_0()	weight: 0
#timesIter(x1,x2,x3,x4)	weight: 0
#plus(x1,x2)	weight: 0
 false()	weight: 0
  #ge(x1,x2)	weight: 0
 #inc(x1)	weight: x1
     c()	weight: 0
   #p(x1)	weight: 0
   inc(x1)	weight: 0
#p❆1_s(x1)	weight: 0
  true()	weight: 0
     p(x1)	weight: 0
#times(x1,x2)	weight: 0
     0()	weight: 0
    ge(x1,x2)	weight: 0
 times(x1,x2)	weight: 0
p❆1_0()	weight: 0
#isZero❆1_s(x1)	weight: 0
isZero❆1_0()	weight: 0
ifPlus(x1,x2,x3)	weight: 0
    f0(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
  #f1(x1,x2,x3)	weight: 0
#isZero❆1_0()	weight: 0
isZero❆1_s(x1)	weight: 0
#ifPlus(x1,x2,x3)	weight: 0
isZero(x1)	weight: 0
    f2(x1,x2,x3)	weight: 0
    f1(x1,x2,x3)	weight: 0
  #f0(x1,x2,x3)	weight: 0
#ifTimes(x1,x2,x3,x4,x5)	weight: 0
    Usable rules: { }
    Removed DPs: #2
Number of SCCs: 5, DPs: 9, edges: 9
	SCC { #8 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
ifTimes(x1,x2,x3,x4,x5)	weight: 0
     1()	weight: 0
     d()	weight: 0
timesIter(x1,x2,x3,x4)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#isZero(x1)	weight: 0
  #f2(x1,x2,x3)	weight: 0
p❆1_s(x1)	weight: 0
#p❆1_0()	weight: 0
#timesIter(x1,x2,x3,x4)	weight: 0
#plus(x1,x2)	weight: 0
 false()	weight: 0
  #ge(x1,x2)	weight: 0
 #inc(x1)	weight: 0
     c()	weight: 0
   #p(x1)	weight: 0
   inc(x1)	weight: 0
#p❆1_s(x1)	weight: 0
  true()	weight: 0
     p(x1)	weight: 0
#times(x1,x2)	weight: 0
     0()	weight: 0
    ge(x1,x2)	weight: 0
 times(x1,x2)	weight: 0
p❆1_0()	weight: 0
#isZero❆1_s(x1)	weight: x1
isZero❆1_0()	weight: 0
ifPlus(x1,x2,x3)	weight: 0
    f0(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
  #f1(x1,x2,x3)	weight: 0
#isZero❆1_0()	weight: 0
isZero❆1_s(x1)	weight: 0
#ifPlus(x1,x2,x3)	weight: 0
isZero(x1)	weight: 0
    f2(x1,x2,x3)	weight: 0
    f1(x1,x2,x3)	weight: 0
  #f0(x1,x2,x3)	weight: 0
#ifTimes(x1,x2,x3,x4,x5)	weight: 0
    Usable rules: { }
    Removed DPs: #8
Number of SCCs: 4, DPs: 8, edges: 8
	SCC { #14 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
ifTimes(x1,x2,x3,x4,x5)	weight: 0
     1()	weight: 0
     d()	weight: 0
timesIter(x1,x2,x3,x4)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#isZero(x1)	weight: 0
  #f2(x1,x2,x3)	weight: 0
p❆1_s(x1)	weight: 0
#p❆1_0()	weight: 0
#timesIter(x1,x2,x3,x4)	weight: 0
#plus(x1,x2)	weight: 0
 false()	weight: 0
  #ge(x1,x2)	weight: x2
 #inc(x1)	weight: 0
     c()	weight: 0
   #p(x1)	weight: 0
   inc(x1)	weight: 0
#p❆1_s(x1)	weight: 0
  true()	weight: 0
     p(x1)	weight: 0
#times(x1,x2)	weight: 0
     0()	weight: 0
    ge(x1,x2)	weight: 0
 times(x1,x2)	weight: 0
p❆1_0()	weight: 0
#isZero❆1_s(x1)	weight: 0
isZero❆1_0()	weight: 0
ifPlus(x1,x2,x3)	weight: 0
    f0(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
  #f1(x1,x2,x3)	weight: 0
#isZero❆1_0()	weight: 0
isZero❆1_s(x1)	weight: 0
#ifPlus(x1,x2,x3)	weight: 0
isZero(x1)	weight: 0
    f2(x1,x2,x3)	weight: 0
    f1(x1,x2,x3)	weight: 0
  #f0(x1,x2,x3)	weight: 0
#ifTimes(x1,x2,x3,x4,x5)	weight: 0
    Usable rules: { }
    Removed DPs: #14
Number of SCCs: 3, DPs: 7, edges: 7
	SCC { #18 #20 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
ifTimes(x1,x2,x3,x4,x5)	weight: 0
     1()	weight: 0
     d()	weight: 0
timesIter(x1,x2,x3,x4)	weight: 0
     s(x1)	weight: max{0, (/ 3 8) + x1}
#isZero(x1)	weight: 0
  #f2(x1,x2,x3)	weight: 0
p❆1_s(x1)	weight: max{0, (/ 1 8) + x1}
#p❆1_0()	weight: 0
#timesIter(x1,x2,x3,x4)	weight: 0
#plus(x1,x2)	weight: max{0, x1}
 false()	weight: (/ 1 4)
  #ge(x1,x2)	weight: 0
 #inc(x1)	weight: 0
     c()	weight: 0
   #p(x1)	weight: 0
   inc(x1)	weight: (max (/ 1 4) 0)
#p❆1_s(x1)	weight: 0
  true()	weight: 0
     p(x1)	weight: max{0, (- (/ 1 8)) + x1}
#times(x1,x2)	weight: 0
     0()	weight: 0
    ge(x1,x2)	weight: 0
 times(x1,x2)	weight: 0
p❆1_0()	weight: 0
#isZero❆1_s(x1)	weight: 0
isZero❆1_0()	weight: 0
ifPlus(x1,x2,x3)	weight: 0
    f0(x1,x2,x3)	weight: 0
  plus(x1,x2)	weight: 0
  #f1(x1,x2,x3)	weight: 0
#isZero❆1_0()	weight: 0
isZero❆1_s(x1)	weight: (max (/ 1 4) 0)
#ifPlus(x1,x2,x3)	weight: max{0, (- (/ 1 8)) + x1, x2}
isZero(x1)	weight: max{0, (- (/ 1 8)) + x1}
    f2(x1,x2,x3)	weight: 0
    f1(x1,x2,x3)	weight: 0
  #f0(x1,x2,x3)	weight: 0
#ifTimes(x1,x2,x3,x4,x5)	weight: 0
    Usable rules: { 8..10 14..16 25..28 }
    Removed DPs: #18
Number of SCCs: 2, DPs: 5, edges: 5
	SCC { #4 #12 #16 }
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