Input TRS:
    1: add(true(),x,xs) -> add(and(isNat(x),isList(xs)),x,Cons(x,xs))
    2: isList(Cons(x,xs)) -> isList(xs)
    3: isList(nil()) -> true()
    4: isNat(s(x)) -> isNat(x)
    5: isNat(0()) -> true()
    6: if(true(),x,y) -> x
    7: if(false(),x,y) -> y
    8: and(true(),true()) -> true()
    9: and(false(),x) -> false()
    10: and(x,false()) -> false()
Number of strict rules: 10
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #isList(Cons(x,xs)) -> #isList(xs)
   #2: #add(true(),x,xs) -> #add(and(isNat(x),isList(xs)),x,Cons(x,xs))
   #3: #add(true(),x,xs) -> #and(isNat(x),isList(xs))
   #4: #add(true(),x,xs) -> #isNat(x)
   #5: #add(true(),x,xs) -> #isList(xs)
   #6: #isNat(s(x)) -> #isNat(x)
Number of SCCs: 3, DPs: 3, edges: 3
	SCC { #6 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 2) + x1
#isNat(x1)	weight: x1
   and(x1,x2)	weight: 0
 false()	weight: 0
  true()	weight: 0
isList(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   nil()	weight: 0
#isList(x1)	weight: 0
 isNat(x1)	weight: 0
  #if(x1,x2,x3)	weight: 0
 #add(x1,x2,x3)	weight: 0
   add(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
  Cons(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #6
Number of SCCs: 2, DPs: 2, edges: 2
	SCC { #1 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 2)
#isNat(x1)	weight: 0
   and(x1,x2)	weight: 0
 false()	weight: 0
  true()	weight: 0
isList(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   nil()	weight: 0
#isList(x1)	weight: x1
 isNat(x1)	weight: 0
  #if(x1,x2,x3)	weight: 0
 #add(x1,x2,x3)	weight: 0
   add(x1,x2,x3)	weight: 0
 #and(x1,x2)	weight: 0
  Cons(x1,x2)	weight: (/ 1 2) + x2
    Usable rules: { }
    Removed DPs: #1
Number of SCCs: 1, DPs: 1, edges: 1
	SCC { #2 }
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