NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(f 1, 2)
(g 1)
(if 1, 2, 3)
(a)
(b)
(fSNonEmpty)
(false)
(true)
)
(RULES
f(g(g(a)),x) -> b
f(a,b) -> b
g(a) -> g(g(a))
g(b) -> a
if(false,x,g(a)) -> g(a)
if(false,x,g(b)) -> g(b)
if(false,x,a) -> a
if(false,x,b) -> b
if(true,g(a),x) -> g(a)
if(true,g(b),x) -> g(b)
if(true,a,x) -> a
if(true,b,x) -> b
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

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

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(f 1, 2)
(g 1)
(if 1, 2, 3)
(a)
(b)
(fSNonEmpty)
(false)
(true)
)
(RULES
f(g(g(a)),x) -> b
f(a,b) -> b
g(a) -> g(g(a))
g(b) -> a
if(false,x,g(a)) -> g(a)
if(false,x,g(b)) -> g(b)
if(false,x,a) -> a
if(false,x,b) -> b
if(true,g(a),x) -> g(a)
if(true,g(b),x) -> g(b)
if(true,a,x) -> a
if(true,b,x) -> b
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Ordered by Num of Vars and Symbs Procedure:
-> Rules:
 f(g(g(a)),x) -> b
 f(a,b) -> b
 g(a) -> g(g(a))
 g(b) -> a
 if(false,x,g(a)) -> g(a)
 if(false,x,g(b)) -> g(b)
 if(false,x,a) -> a
 if(false,x,b) -> b
 if(true,g(a),x) -> g(a)
 if(true,g(b),x) -> g(b)
 if(true,a,x) -> a
 if(true,b,x) -> b
-> Vars:
 x, x, x, x, x, x, x, x, x

-> Rlps:
 (rule: f(g(g(a)),x) -> b, id: 1, possubterms: f(g(g(a)),x)->[], g(g(a))->[1], g(a)->[1, 1], a->[1, 1, 1])
 (rule: f(a,b) -> b, id: 2, possubterms: f(a,b)->[], a->[1], b->[2])
 (rule: g(a) -> g(g(a)), id: 3, possubterms: g(a)->[], a->[1])
 (rule: g(b) -> a, id: 4, possubterms: g(b)->[], b->[1])
 (rule: if(false,x,g(a)) -> g(a), id: 5, possubterms: if(false,x,g(a))->[], false->[1], g(a)->[3], a->[3, 1])
 (rule: if(false,x,g(b)) -> g(b), id: 6, possubterms: if(false,x,g(b))->[], false->[1], g(b)->[3], b->[3, 1])
 (rule: if(false,x,a) -> a, id: 7, possubterms: if(false,x,a)->[], false->[1], a->[3])
 (rule: if(false,x,b) -> b, id: 8, possubterms: if(false,x,b)->[], false->[1], b->[3])
 (rule: if(true,g(a),x) -> g(a), id: 9, possubterms: if(true,g(a),x)->[], true->[1], g(a)->[2], a->[2, 1])
 (rule: if(true,g(b),x) -> g(b), id: 10, possubterms: if(true,g(b),x)->[], true->[1], g(b)->[2], b->[2, 1])
 (rule: if(true,a,x) -> a, id: 11, possubterms: if(true,a,x)->[], true->[1], a->[2])
 (rule: if(true,b,x) -> b, id: 12, possubterms: if(true,b,x)->[], true->[1], b->[2])

-> Unifications:
(R1 unifies with R3 at p: [1,1], l: f(g(g(a)),x), lp: g(a), sig: {}, l': g(a), r: b, r': g(g(a)))
(R5 unifies with R3 at p: [3], l: if(false,x,g(a)), lp: g(a), sig: {}, l': g(a), r: g(a), r': g(g(a)))
(R6 unifies with R4 at p: [3], l: if(false,x,g(b)), lp: g(b), sig: {}, l': g(b), r: g(b), r': a)
(R9 unifies with R3 at p: [2], l: if(true,g(a),x), lp: g(a), sig: {}, l': g(a), r: g(a), r': g(g(a)))
(R10 unifies with R4 at p: [2], l: if(true,g(b),x), lp: g(b), sig: {}, l': g(b), r: g(b), r': a)

-> Critical pairs info:
<f(g(g(g(a))),x),b>   =>  Not trivial, Not overlay, Proper, NW0, N1
<if(true,a,x),g(b)>   =>  Not trivial, Not overlay, Proper, NW0, N2
<if(false,x,a),g(b)>   =>  Not trivial, Not overlay, Proper, NW0, N3
<if(true,g(g(a)),x),g(a)>   =>  Not trivial, Not overlay, Proper, NW0, N4
<if(false,x,g(g(a))),g(a)>   =>  Not trivial, Not overlay, Proper, NW0, N5

-> 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)
(REPLACEMENT-MAP
(f 1, 2)
(g 1)
(if 1, 2, 3)
(a)
(b)
(fSNonEmpty)
(false)
(true)
)
(RULES
f(g(g(a)),x) -> b
f(a,b) -> b
g(a) -> g(g(a))
g(b) -> a
if(false,x,g(a)) -> g(a)
if(false,x,g(b)) -> g(b)
if(false,x,a) -> a
if(false,x,b) -> b
if(true,g(a),x) -> g(a)
if(true,g(b),x) -> g(b)
if(true,a,x) -> a
if(true,b,x) -> b
)
Critical Pairs:
<f(g(g(g(a))),x),b>   =>  Not trivial, Not overlay, Proper, NW0, N1
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

No Convergence InfChecker Procedure:
Infeasible convergence?
YES

Problem 1: 

Infeasibility Problem:
[(VAR vNonEmpty x vNonEmpty z0)
(STRATEGY CONTEXTSENSITIVE
(f 1 2)
(g 1)
(if 1 2 3)
(a)
(b)
(c_x)
(fSNonEmpty)
(false)
(true)
)
(RULES
f(g(g(a)),x) -> b
f(a,b) -> b
g(a) -> g(g(a))
g(b) -> a
if(false,x,g(a)) -> g(a)
if(false,x,g(b)) -> g(b)
if(false,x,a) -> a
if(false,x,b) -> b
if(true,g(a),x) -> g(a)
if(true,g(b),x) -> g(b)
if(true,a,x) -> a
if(true,b,x) -> b
)]
Infeasibility Conditions:
f(g(g(g(a))),c_x) ->* z0, b ->* z0

Problem 1: 

Obtaining a model using AGES:

 -> Theory (Usable Rules):
f(g(g(a)),x) -> b
f(a,b) -> b
g(a) -> g(g(a))
g(b) -> a

 -> AGES Output:




The problem is infeasible.


The problem is not confluent.