NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(P 1)
(Q 1)
(a 1)
(b 1)
(c 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
a(b(x)) -> b(c(x))
a(c(x)) -> c(a(x))
b(b(x)) -> a(c(x))
c(b(x)) -> b(c(x))
c(b(x)) -> c(c(x))
c(c(x)) -> c(b(x))
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

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

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(P 1)
(Q 1)
(a 1)
(b 1)
(c 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
a(b(x)) -> b(c(x))
a(c(x)) -> c(a(x))
b(b(x)) -> a(c(x))
c(b(x)) -> b(c(x))
c(b(x)) -> c(c(x))
c(c(x)) -> c(b(x))
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Ordered by Num of Vars and Symbs Procedure:
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 a(b(x)) -> b(c(x))
 a(c(x)) -> c(a(x))
 b(b(x)) -> a(c(x))
 c(b(x)) -> b(c(x))
 c(b(x)) -> c(c(x))
 c(c(x)) -> c(b(x))
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
-> Vars:
 x, x, x, x, x, x, x, x, x, x, x, x, x, x, x

-> Rlps:
 (rule: P(p(x)) -> x, id: 1, possubterms: P(p(x))->[], p(x)->[1])
 (rule: P(x) -> Q(Q(p(x))), id: 2, possubterms: P(x)->[])
 (rule: Q(p(q(x))) -> q(p(Q(x))), id: 3, possubterms: Q(p(q(x)))->[], p(q(x))->[1], q(x)->[1, 1])
 (rule: Q(q(x)) -> x, id: 4, possubterms: Q(q(x))->[], q(x)->[1])
 (rule: a(b(x)) -> b(c(x)), id: 5, possubterms: a(b(x))->[], b(x)->[1])
 (rule: a(c(x)) -> c(a(x)), id: 6, possubterms: a(c(x))->[], c(x)->[1])
 (rule: b(b(x)) -> a(c(x)), id: 7, possubterms: b(b(x))->[], b(x)->[1])
 (rule: c(b(x)) -> b(c(x)), id: 8, possubterms: c(b(x))->[], b(x)->[1])
 (rule: c(b(x)) -> c(c(x)), id: 9, possubterms: c(b(x))->[], b(x)->[1])
 (rule: c(c(x)) -> c(b(x)), id: 10, possubterms: c(c(x))->[], c(x)->[1])
 (rule: p(P(x)) -> x, id: 11, possubterms: p(P(x))->[], P(x)->[1])
 (rule: p(Q(Q(x))) -> Q(Q(p(x))), id: 12, possubterms: p(Q(Q(x)))->[], Q(Q(x))->[1], Q(x)->[1, 1])
 (rule: p(p(x)) -> q(q(x)), id: 13, possubterms: p(p(x))->[], p(x)->[1])
 (rule: q(Q(x)) -> x, id: 14, possubterms: q(Q(x))->[], Q(x)->[1])
 (rule: q(q(p(x))) -> p(q(q(x))), id: 15, possubterms: q(q(p(x)))->[], q(p(x))->[1], p(x)->[1, 1])

-> Unifications:
(R1 unifies with R11 at p: [1], l: P(p(x)), lp: p(x), sig: {x -> P(x')}, l': p(P(x')), r: x, r': x')
(R1 unifies with R12 at p: [1], l: P(p(x)), lp: p(x), sig: {x -> Q(Q(x'))}, l': p(Q(Q(x'))), r: x, r': Q(Q(p(x'))))
(R1 unifies with R13 at p: [1], l: P(p(x)), lp: p(x), sig: {x -> p(x')}, l': p(p(x')), r: x, r': q(q(x')))
(R2 unifies with R1 at p: [], l: P(x), lp: P(x), sig: {x -> p(x')}, l': P(p(x')), r: Q(Q(p(x))), r': x')
(R3 unifies with R14 at p: [1,1], l: Q(p(q(x))), lp: q(x), sig: {x -> Q(x')}, l': q(Q(x')), r: q(p(Q(x))), r': x')
(R3 unifies with R15 at p: [1,1], l: Q(p(q(x))), lp: q(x), sig: {x -> q(p(x'))}, l': q(q(p(x'))), r: q(p(Q(x))), r': p(q(q(x'))))
(R4 unifies with R14 at p: [1], l: Q(q(x)), lp: q(x), sig: {x -> Q(x')}, l': q(Q(x')), r: x, r': x')
(R4 unifies with R15 at p: [1], l: Q(q(x)), lp: q(x), sig: {x -> q(p(x'))}, l': q(q(p(x'))), r: x, r': p(q(q(x'))))
(R5 unifies with R7 at p: [1], l: a(b(x)), lp: b(x), sig: {x -> b(x')}, l': b(b(x')), r: b(c(x)), r': a(c(x')))
(R6 unifies with R8 at p: [1], l: a(c(x)), lp: c(x), sig: {x -> b(x')}, l': c(b(x')), r: c(a(x)), r': b(c(x')))
(R6 unifies with R9 at p: [1], l: a(c(x)), lp: c(x), sig: {x -> b(x')}, l': c(b(x')), r: c(a(x)), r': c(c(x')))
(R6 unifies with R10 at p: [1], l: a(c(x)), lp: c(x), sig: {x -> c(x')}, l': c(c(x')), r: c(a(x)), r': c(b(x')))
(R7 unifies with R7 at p: [1], l: b(b(x)), lp: b(x), sig: {x -> b(x')}, l': b(b(x')), r: a(c(x)), r': a(c(x')))
(R8 unifies with R7 at p: [1], l: c(b(x)), lp: b(x), sig: {x -> b(x')}, l': b(b(x')), r: b(c(x)), r': a(c(x')))
(R9 unifies with R8 at p: [], l: c(b(x)), lp: c(b(x)), sig: {x -> x'}, l': c(b(x')), r: c(c(x)), r': b(c(x')))
(R9 unifies with R7 at p: [1], l: c(b(x)), lp: b(x), sig: {x -> b(x')}, l': b(b(x')), r: c(c(x)), r': a(c(x')))
(R10 unifies with R8 at p: [1], l: c(c(x)), lp: c(x), sig: {x -> b(x')}, l': c(b(x')), r: c(b(x)), r': b(c(x')))
(R10 unifies with R9 at p: [1], l: c(c(x)), lp: c(x), sig: {x -> b(x')}, l': c(b(x')), r: c(b(x)), r': c(c(x')))
(R10 unifies with R10 at p: [1], l: c(c(x)), lp: c(x), sig: {x -> c(x')}, l': c(c(x')), r: c(b(x)), r': c(b(x')))
(R11 unifies with R1 at p: [1], l: p(P(x)), lp: P(x), sig: {x -> p(x')}, l': P(p(x')), r: x, r': x')
(R11 unifies with R2 at p: [1], l: p(P(x)), lp: P(x), sig: {x -> x'}, l': P(x'), r: x, r': Q(Q(p(x'))))
(R12 unifies with R3 at p: [1,1], l: p(Q(Q(x))), lp: Q(x), sig: {x -> p(q(x'))}, l': Q(p(q(x'))), r: Q(Q(p(x))), r': q(p(Q(x'))))
(R12 unifies with R4 at p: [1,1], l: p(Q(Q(x))), lp: Q(x), sig: {x -> q(x')}, l': Q(q(x')), r: Q(Q(p(x))), r': x')
(R13 unifies with R11 at p: [1], l: p(p(x)), lp: p(x), sig: {x -> P(x')}, l': p(P(x')), r: q(q(x)), r': x')
(R13 unifies with R12 at p: [1], l: p(p(x)), lp: p(x), sig: {x -> Q(Q(x'))}, l': p(Q(Q(x'))), r: q(q(x)), r': Q(Q(p(x'))))
(R13 unifies with R13 at p: [1], l: p(p(x)), lp: p(x), sig: {x -> p(x')}, l': p(p(x')), r: q(q(x)), r': q(q(x')))
(R14 unifies with R3 at p: [1], l: q(Q(x)), lp: Q(x), sig: {x -> p(q(x'))}, l': Q(p(q(x'))), r: x, r': q(p(Q(x'))))
(R14 unifies with R4 at p: [1], l: q(Q(x)), lp: Q(x), sig: {x -> q(x')}, l': Q(q(x')), r: x, r': x')
(R15 unifies with R11 at p: [1,1], l: q(q(p(x))), lp: p(x), sig: {x -> P(x')}, l': p(P(x')), r: p(q(q(x))), r': x')
(R15 unifies with R12 at p: [1,1], l: q(q(p(x))), lp: p(x), sig: {x -> Q(Q(x'))}, l': p(Q(Q(x'))), r: p(q(q(x))), r': Q(Q(p(x'))))
(R15 unifies with R13 at p: [1,1], l: q(q(p(x))), lp: p(x), sig: {x -> p(x')}, l': p(p(x')), r: p(q(q(x))), r': q(q(x')))

-> Critical pairs info:
<p(Q(Q(p(x')))),x'>   =>  Not trivial, Not overlay, Proper, NW0, N1
<p(x'),p(x')>   =>  Trivial, Not overlay, Proper, NW0, N2
<q(x'),q(x')>   =>  Trivial, Not overlay, Proper, NW0, N3
<P(x'),P(x')>   =>  Trivial, Not overlay, Proper, NW0, N4
<x',Q(Q(p(p(x'))))>   =>  Not trivial, Overlay, Proper, NW0, N5
<Q(x'),Q(x')>   =>  Trivial, Not overlay, Proper, NW0, N6
<p(x'),q(q(P(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N7
<P(q(q(x'))),p(x')>   =>  Not trivial, Not overlay, Proper, NW0, N8
<c(c(c(x'))),c(b(b(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N9
<b(c(x')),c(c(x'))>   =>  Not trivial, Overlay, Proper, NW0, N10
<q(q(q(q(x')))),p(q(q(p(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N11
<p(q(q(x'))),q(q(p(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N12
<c(a(c(x'))),b(c(b(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N13
<c(b(c(x'))),c(b(b(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N14
<c(a(c(x'))),c(c(b(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N15
<P(Q(Q(p(x')))),Q(Q(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N16
<a(a(c(x'))),b(c(b(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N17
<q(q(x')),p(q(q(P(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N18
<p(Q(Q(p(x')))),q(q(Q(Q(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N19
<c(c(b(x'))),c(b(c(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N20
<a(c(b(x'))),c(a(c(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N21
<Q(p(q(q(x')))),q(p(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N22
<q(q(p(Q(x')))),p(q(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N23
<a(c(c(x'))),c(a(b(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N24
<Q(p(x')),q(p(Q(Q(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N25
<p(Q(x')),Q(Q(p(q(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N26
<Q(p(p(q(q(x'))))),q(p(Q(q(p(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N27
<b(a(c(x'))),a(c(b(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N28
<p(Q(q(p(Q(x'))))),Q(Q(p(p(q(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N29
<a(b(c(x'))),c(a(b(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N30
<q(q(Q(Q(p(x'))))),p(q(q(Q(Q(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N31

-> Problem conclusions:
 Left linear, Right linear, 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 x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(a 1)
(b 1)
(c 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
a(b(x)) -> b(c(x))
a(c(x)) -> c(a(x))
b(b(x)) -> a(c(x))
c(b(x)) -> b(c(x))
c(b(x)) -> c(c(x))
c(c(x)) -> c(b(x))
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<a(a(c(x'))),b(c(b(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N17
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

No Convergence InfChecker Procedure:
Infeasible convergence?
YES

Problem 1: 

Infeasibility Problem:
[(VAR vNonEmpty x x1 vNonEmpty z0)
(STRATEGY CONTEXTSENSITIVE
(P 1)
(Q 1)
(a 1)
(b 1)
(c 1)
(p 1)
(q 1)
(c_x1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
a(b(x)) -> b(c(x))
a(c(x)) -> c(a(x))
b(b(x)) -> a(c(x))
c(b(x)) -> b(c(x))
c(b(x)) -> c(c(x))
c(c(x)) -> c(b(x))
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)]
Infeasibility Conditions:
a(a(c(c_x1))) ->* z0, b(c(b(c_x1))) ->* z0

Problem 1: 

Obtaining a model using AGES:

 -> Theory (Usable Rules):
a(b(x)) -> b(c(x))
a(c(x)) -> c(a(x))
b(b(x)) -> a(c(x))
c(b(x)) -> b(c(x))
c(b(x)) -> c(c(x))
c(c(x)) -> c(b(x))

 -> AGES Output:




The problem is infeasible.


The problem is not confluent.