Input TRS:
    1: prime(|0|()) -> false()
    2: prime(s(|0|())) -> false()
    3: prime(s(s(x))) -> prime1(s(s(x)),s(x))
    4: prime1(x,|0|()) -> false()
    5: prime1(x,s(|0|())) -> true()
    6: prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y)))
    7: divp(x,y) -> =(rem(x,y),|0|())
Number of strict rules: 7
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #prime1(x,s(s(y))) -> #divp(s(s(y)),x)
   #2: #prime1(x,s(s(y))) -> #prime1(x,s(y))
   #3: #prime(s(s(x))) -> #prime1(s(s(x)),s(x))
Number of SCCs: 1, DPs: 1, edges: 1
	SCC { #2 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
     s(x1)	weight: (/ 1 4) + x1
 prime(x1)	weight: 0
   and(x1,x2)	weight: 0
 false()	weight: 0
  true()	weight: 0
#prime(x1)	weight: 0
     =(x1,x2)	weight: 0
#prime1(x1,x2)	weight: x2
prime1(x1,x2)	weight: 0
   rem(x1,x2)	weight: 0
#divp(x1,x2)	weight: 0
  divp(x1,x2)	weight: 0
   not(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #2
Number of SCCs: 0, DPs: 0, edges: 0
YES