NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(f 1, 2)
(g 1)
(k 1, 2)
(q 1, 2, 3)
(r 1, 2)
(b)
(fSNonEmpty)
(h 1)
)
(RULES
f(x,b) -> h(f(f(x,x),x))
g(f(b,x)) -> g(h(h(f(f(h(k(k(x,x),x)),h(k(k(x,x),x))),h(k(k(x,x),x))))))
k(x,y) -> q(x,y,y)
q(x,y,b) -> r(x,y)
r(x,b) -> f(x,b)
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 
Not CS-TRS Procedure:
R is not a CS-TRS

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(f 1, 2)
(g 1)
(k 1, 2)
(q 1, 2, 3)
(r 1, 2)
(b)
(fSNonEmpty)
(h 1)
)
(RULES
f(x,b) -> h(f(f(x,x),x))
g(f(b,x)) -> g(h(h(f(f(h(k(k(x,x),x)),h(k(k(x,x),x))),h(k(k(x,x),x))))))
k(x,y) -> q(x,y,y)
q(x,y,b) -> r(x,y)
r(x,b) -> f(x,b)
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Ordered by Num of Vars and Symbs Procedure:
-> Rules:
 f(x,b) -> h(f(f(x,x),x))
 g(f(b,x)) -> g(h(h(f(f(h(k(k(x,x),x)),h(k(k(x,x),x))),h(k(k(x,x),x))))))
 k(x,y) -> q(x,y,y)
 q(x,y,b) -> r(x,y)
 r(x,b) -> f(x,b)
-> Vars:
 x, x, x, y, x, y, x

-> Rlps:
 (rule: f(x,b) -> h(f(f(x,x),x)), id: 1, possubterms: f(x,b)->[], b->[2])
 (rule: g(f(b,x)) -> g(h(h(f(f(h(k(k(x,x),x)),h(k(k(x,x),x))),h(k(k(x,x),x)))))), id: 2, possubterms: g(f(b,x))->[], f(b,x)->[1], b->[1, 1])
 (rule: k(x,y) -> q(x,y,y), id: 3, possubterms: k(x,y)->[])
 (rule: q(x,y,b) -> r(x,y), id: 4, possubterms: q(x,y,b)->[], b->[3])
 (rule: r(x,b) -> f(x,b), id: 5, possubterms: r(x,b)->[], b->[2])

-> Unifications:
(R2 unifies with R1 at p: [1], l: g(f(b,x)), lp: f(b,x), sig: {x -> b,x' -> b}, l': f(x',b), r: g(h(h(f(f(h(k(k(x,x),x)),h(k(k(x,x),x))),h(k(k(x,x),x)))))), r': h(f(f(x',x'),x')))

-> Critical pairs info:
<g(h(f(f(b,b),b))),g(h(h(f(f(h(k(k(b,b),b)),h(k(k(b,b),b))),h(k(k(b,b),b))))))>   =>  Not trivial, Not overlay, Proper, NW0, N1

-> Problem conclusions:
 Left linear, Not right linear, Not linear
 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
 Not Huet-Levy confluent, Not Newman confluent
 R is a TRS 


Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x y)
(REPLACEMENT-MAP
(f 1, 2)
(g 1)
(k 1, 2)
(q 1, 2, 3)
(r 1, 2)
(b)
(fSNonEmpty)
(h 1)
)
(RULES
f(x,b) -> h(f(f(x,x),x))
g(f(b,x)) -> g(h(h(f(f(h(k(k(x,x),x)),h(k(k(x,x),x))),h(k(k(x,x),x))))))
k(x,y) -> q(x,y,y)
q(x,y,b) -> r(x,y)
r(x,b) -> f(x,b)
)
Critical Pairs:
<g(h(f(f(b,b),b))),g(h(h(f(f(h(k(k(b,b),b)),h(k(k(b,b),b))),h(k(k(b,b),b))))))>   =>  Not trivial, Not overlay, Proper, NW0, N1
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

No Convergence InfChecker Procedure:
Infeasible convergence?
YES

Problem 1: 

Infeasibility Problem:
[(VAR vNonEmpty x y vNonEmpty z0)
(STRATEGY CONTEXTSENSITIVE
(f 1 2)
(g 1)
(k 1 2)
(q 1 2 3)
(r 1 2)
(b)
(fSNonEmpty)
(h 1)
)
(RULES
f(x,b) -> h(f(f(x,x),x))
g(f(b,x)) -> g(h(h(f(f(h(k(k(x,x),x)),h(k(k(x,x),x))),h(k(k(x,x),x))))))
k(x,y) -> q(x,y,y)
q(x,y,b) -> r(x,y)
r(x,b) -> f(x,b)
)]
Infeasibility Conditions:
g(h(f(f(b,b),b))) ->* z0, g(h(h(f(f(h(k(k(b,b),b)),h(k(k(b,b),b))),h(k(k(b,b),b)))))) ->* z0

Problem 1: 

Obtaining a model using AGES:

 -> Theory (Usable Rules):
f(x,b) -> h(f(f(x,x),x))
g(f(b,x)) -> g(h(h(f(f(h(k(k(x,x),x)),h(k(k(x,x),x))),h(k(k(x,x),x))))))
k(x,y) -> q(x,y,y)
q(x,y,b) -> r(x,y)
r(x,b) -> f(x,b)

 -> AGES Output:




The problem is infeasible.


The problem is not confluent.