NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(0 1)
(2 1)
(a 1)
(b 1)
(c 1)
(1 1)
(fSNonEmpty)
)
(RULES
0(1(2(x))) -> 2(0(1(x)))
2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(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))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 

Modular Confluence Combinations Decomposition Procedure:
TRS combination:
{0(1(2(x))) -> 2(0(1(x)))
 2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(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))}
Disjoint
Constructor-sharing
Not composable
Left linear
Layer-preserving
TRS1
Just (VAR x)
(STRATEGY CONTEXTSENSITIVE
(0 1)
(2 1)
(1 1)
)
(RULES
0(1(2(x))) -> 2(0(1(x)))
2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x))))))))))))
)

TRS2
Just (VAR x)
(STRATEGY CONTEXTSENSITIVE
(a 1)
(b 1)
(c 1)
)
(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))
)

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x)
(REPLACEMENT-MAP
(0 1)
(2 1)
(1 1)
)
(RULES
0(1(2(x))) -> 2(0(1(x)))
2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x))))))))))))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

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

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x)
(REPLACEMENT-MAP
(0 1)
(2 1)
(1 1)
)
(RULES
0(1(2(x))) -> 2(0(1(x)))
2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x))))))))))))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Ordered by Num of Vars and Symbs Procedure:
-> Rules:
 0(1(2(x))) -> 2(0(1(x)))
 2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x))))))))))))
-> Vars:
 x, x

-> Rlps:
 (rule: 0(1(2(x))) -> 2(0(1(x))), id: 1, possubterms: 0(1(2(x)))->[], 1(2(x))->[1], 2(x)->[1, 1])
 (rule: 2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x)))))))))))), id: 2, possubterms: 2(2(2(2(2(2(2(1(1(1(1(2(x))))))))))))->[], 2(2(2(2(2(2(1(1(1(1(2(x)))))))))))->[1], 2(2(2(2(2(1(1(1(1(2(x))))))))))->[1, 1], 2(2(2(2(1(1(1(1(2(x)))))))))->[1, 1, 1], 2(2(2(1(1(1(1(2(x))))))))->[1, 1, 1, 1], 2(2(1(1(1(1(2(x)))))))->[1, 1, 1, 1, 1], 2(1(1(1(1(2(x))))))->[1, 1, 1, 1, 1, 1], 1(1(1(1(2(x)))))->[1, 1, 1, 1, 1, 1, 1], 1(1(1(2(x))))->[1, 1, 1, 1, 1, 1, 1, 1], 1(1(2(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 1(2(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 2(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])

-> Unifications:
(R1 unifies with R2 at p: [1,1], l: 0(1(2(x))), lp: 2(x), sig: {x -> 2(2(2(2(2(2(1(1(1(1(2(x')))))))))))}, l': 2(2(2(2(2(2(2(1(1(1(1(2(x')))))))))))), r: 2(0(1(x))), r': 2(1(2(2(0(1(2(1(1(0(1(0(x')))))))))))))
(R2 unifies with R2 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))), lp: 2(x), sig: {x -> 2(2(2(2(2(2(1(1(1(1(2(x')))))))))))}, l': 2(2(2(2(2(2(2(1(1(1(1(2(x')))))))))))), r: 2(1(2(2(0(1(2(1(1(0(1(0(x)))))))))))), r': 2(1(2(2(0(1(2(1(1(0(1(0(x')))))))))))))

-> Critical pairs info:
<2(2(2(2(2(2(2(1(1(1(1(2(1(2(2(0(1(2(1(1(0(1(0(x'))))))))))))))))))))))),2(1(2(2(0(1(2(1(1(0(1(0(2(2(2(2(2(2(1(1(1(1(2(x')))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N1
<0(1(2(1(2(2(0(1(2(1(1(0(1(0(x')))))))))))))),2(0(1(2(2(2(2(2(2(1(1(1(1(2(x'))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N2

-> 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
(0 1)
(2 1)
(1 1)
)
(RULES
0(1(2(x))) -> 2(0(1(x)))
2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x))))))))))))
)
Critical Pairs:
<2(2(2(2(2(2(2(1(1(1(1(2(1(2(2(0(1(2(1(1(0(1(0(x'))))))))))))))))))))))),2(1(2(2(0(1(2(1(1(0(1(0(2(2(2(2(2(2(1(1(1(1(2(x')))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N1
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

No Convergence InfChecker Procedure:
Infeasible convergence?
YES

Problem 1: 

Infeasibility Problem:
[(VAR vNonEmpty x x1 vNonEmpty z0)
(STRATEGY CONTEXTSENSITIVE
(0 1)
(2 1)
(1 1)
(c_x1)
(fSNonEmpty)
)
(RULES
0(1(2(x))) -> 2(0(1(x)))
2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x))))))))))))
)]
Infeasibility Conditions:
2(2(2(2(2(2(2(1(1(1(1(2(1(2(2(0(1(2(1(1(0(1(0(c_x1))))))))))))))))))))))) ->* z0, 2(1(2(2(0(1(2(1(1(0(1(0(2(2(2(2(2(2(1(1(1(1(2(c_x1))))))))))))))))))))))) ->* z0

Problem 1: 

Obtaining a model using AGES:

 -> Theory (Usable Rules):
0(1(2(x))) -> 2(0(1(x)))
2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x))))))))))))

 -> AGES Output:




The problem is infeasible.


The problem is not confluent.