YES
(VAR x y z)
(RULES 
p(s(x)) -> x
plus(x,0) -> x
plus(0,y) -> y
plus(s(x),y) -> s(plus(x,y))
plus(s(x),y) -> s(plus(p(s(x)),y))
plus(x,s(y)) -> s(plus(x,p(s(y))))
times(0,y) -> 0
times(s(0),y) -> y
times(s(x),y) -> plus(y,times(x,y))
div(0,y) -> 0
div(x,y) -> quot(x,y,y)
quot(0,s(y),z) -> 0
quot(s(x),s(y),z) -> quot(x,y,z)
quot(x,0,s(z)) -> s(div(x,s(z)))
div(div(x,y),z) -> div(x,times(y,z))
eq(0,0) -> true
eq(s(x),0) -> false
eq(0,s(y)) -> false
eq(s(x),s(y)) -> eq(x,y)
divides(y,x) -> eq(x,times(div(x,y),y))
prime(s(s(x))) -> pr(s(s(x)),s(x))
pr(x,s(0)) -> true
pr(x,s(s(y))) -> if(divides(s(s(y)),x),x,s(y))
if(true,x,y) -> false
if(false,x,y) -> pr(x,y)
)

Proving termination of rewriting for IJCAR_26:

-> Dependency pairs:
nF_plus(s(x),y) -> nF_plus(x,y)
nF_plus(s(x),y) -> nF_plus(p(s(x)),y)
nF_plus(s(x),y) -> nF_p(s(x))
nF_plus(x,s(y)) -> nF_plus(x,p(s(y)))
nF_plus(x,s(y)) -> nF_p(s(y))
nF_times(s(x),y) -> nF_plus(y,times(x,y))
nF_times(s(x),y) -> nF_times(x,y)
nF_div(x,y) -> nF_quot(x,y,y)
nF_quot(s(x),s(y),z) -> nF_quot(x,y,z)
nF_quot(x,0,s(z)) -> nF_div(x,s(z))
nF_div(div(x,y),z) -> nF_div(x,times(y,z))
nF_div(div(x,y),z) -> nF_times(y,z)
nF_eq(s(x),s(y)) -> nF_eq(x,y)
nF_divides(y,x) -> nF_eq(x,times(div(x,y),y))
nF_divides(y,x) -> nF_times(div(x,y),y)
nF_divides(y,x) -> nF_div(x,y)
nF_prime(s(s(x))) -> nF_pr(s(s(x)),s(x))
nF_pr(x,s(s(y))) -> nF_if(divides(s(s(y)),x),x,s(y))
nF_pr(x,s(s(y))) -> nF_divides(s(s(y)),x)
nF_if(false,x,y) -> nF_pr(x,y)

-> Proof of termination for IJCAR_26_1_1:
-> -> Dependency pairs in cycle:
nF_pr(x,s(s(y))) -> nF_if(divides(s(s(y)),x),x,s(y))
nF_if(false,x,y) -> nF_pr(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for IJCAR_26_1_2:
-> -> Dependency pairs in cycle:
nF_eq(s(x),s(y)) -> nF_eq(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for IJCAR_26_1_3:
-> -> Dependency pairs in cycle:
nF_div(x,y) -> nF_quot(x,y,y)
nF_div(div(x,y),z) -> nF_div(x,times(y,z))
nF_quot(x,0,s(z)) -> nF_div(x,s(z))
nF_quot(s(x),s(y),z) -> nF_quot(x,y,z)

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF_div(x,y) -> nF_quot(x,y,y)
nF_quot(x,0,s(z)) -> nF_div(x,s(z))

There are no usable rules.

Polynomial Interpretation:

[p](X) = 0
[s](X) = 0
[plus](X1,X2) = 0
[0] = 2
[times](X1,X2) = 0
[div](X1,X2) = 0
[quot](X1,X2,X3) = 0
[eq](X1,X2) = 0
[true] = 0
[false] = 0
[divides](X1,X2) = 0
[prime](X) = 0
[pr](X1,X2) = 0
[if](X1,X2,X3) = 0
[nF_div](X1,X2) = 2.X2
[nF_quot](X1,X2,X3) = 2.X2

TIME: 1.37e-4


-> Proof of termination for IJCAR_26_1_4:
-> -> Dependency pairs in cycle:
nF_times(s(x),y) -> nF_times(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for IJCAR_26_1_5:
-> -> Dependency pairs in cycle:
nF_plus(s(x),y) -> nF_plus(x,y)
nF_plus(x,s(y)) -> nF_plus(x,p(s(y)))
nF_plus(s(x),y) -> nF_plus(p(s(x)),y)

UsableRules:
p(s(x)) -> x

Polynomial Interpretation:

[p](X) = 1/2.X
[s](X) = 2.X + 2
[plus](X1,X2) = 0
[0] = 0
[times](X1,X2) = 0
[div](X1,X2) = 0
[quot](X1,X2,X3) = 0
[eq](X1,X2) = 0
[true] = 0
[false] = 0
[divides](X1,X2) = 0
[prime](X) = 0
[pr](X1,X2) = 0
[if](X1,X2,X3) = 0
[nF_plus](X1,X2) = 2.X1

TIME: 1.31e-4

-> -> Dependency pairs in cycle:
nF_plus(s(x),y) -> nF_plus(x,y)
nF_plus(x,s(y)) -> nF_plus(x,p(s(y)))

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF_plus(x,s(y)) -> nF_plus(x,p(s(y)))

UsableRules:
p(s(x)) -> x

Polynomial Interpretation:

[p](X) = 1/2.X
[s](X) = 2.X + 2
[plus](X1,X2) = 0
[0] = 0
[times](X1,X2) = 0
[div](X1,X2) = 0
[quot](X1,X2,X3) = 0
[eq](X1,X2) = 0
[true] = 0
[false] = 0
[divides](X1,X2) = 0
[prime](X) = 0
[pr](X1,X2) = 0
[if](X1,X2,X3) = 0
[nF_plus](X1,X2) = 2.X2

TIME: 1.45e-4


SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 2
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: All rationals
Delta: automatic



Termination was proved succesfully.