0.00/0.01	NO
0.00/0.01	
0.00/0.01	Problem 1: 
0.00/0.01	
0.00/0.01	
0.00/0.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.01	Confluence Problem:
0.00/0.01	(VAR x y)
0.00/0.01	(REPLACEMENT-MAP
0.00/0.01	(f 1)
0.00/0.01	(g 1, 2, 3)
0.00/0.01	(p 1)
0.00/0.01	(q 1)
0.00/0.01	(a)
0.00/0.01	(b)
0.00/0.01	(c)
0.00/0.01	(d)
0.00/0.01	(h 1, 2)
0.00/0.01	)
0.00/0.01	(RULES
0.00/0.01	f(g(x,a,b)) -> x
0.00/0.01	g(f(h(c,d)),x,y) -> h(p(x),q(x))
0.00/0.01	p(a) -> c
0.00/0.01	q(b) -> d
0.00/0.01	)
0.00/0.01	
0.00/0.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.01	
0.00/0.01	
0.00/0.01	Problem 1: 
0.00/0.01	
0.00/0.01	Problem 1: 
0.00/0.01	
0.00/0.01	Problem 1: 
0.00/0.01	Not CS-TRS Procedure:
0.00/0.01	R is not a CS-TRS
0.00/0.01	
0.00/0.01	Problem 1: 
0.00/0.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.01	Confluence Problem:
0.00/0.01	(VAR x y)
0.00/0.01	(REPLACEMENT-MAP
0.00/0.01	(f 1)
0.00/0.01	(g 1, 2, 3)
0.00/0.01	(p 1)
0.00/0.01	(q 1)
0.00/0.01	(c)
0.00/0.01	(d)
0.00/0.01	(h 1, 2)
0.00/0.01	)
0.00/0.01	(RULES
0.00/0.01	f(g(x,a,b)) -> x
0.00/0.01	g(f(h(c,d)),x,y) -> h(p(x),q(x))
0.00/0.01	p(a) -> c
0.00/0.01	q(b) -> d
0.00/0.01	)
0.00/0.01	
0.00/0.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.01	
0.00/0.01	Huet Levy Procedure:
0.00/0.01	-> Rules:
0.00/0.01	 f(g(x,a,b)) -> x
0.00/0.01	 g(f(h(c,d)),x,y) -> h(p(x),q(x))
0.00/0.01	 p(a) -> c
0.00/0.01	 q(b) -> d
0.00/0.01	-> Vars:
0.00/0.01	 x, x, y
0.00/0.01	
0.00/0.01	-> Rlps:
0.00/0.01	 (rule: f(g(x,a,b)) -> x, id: 1, possubterms: f(g(x,a,b))->[], g(x,a,b)->[1], a->[1, 2], b->[1, 3])
0.00/0.01	 (rule: g(f(h(c,d)),x,y) -> h(p(x),q(x)), id: 2, possubterms: g(f(h(c,d)),x,y)->[], f(h(c,d))->[1], h(c,d)->[1, 1], c->[1, 1, 1], d->[1, 1, 2])
0.00/0.01	 (rule: p(a) -> c, id: 3, possubterms: p(a)->[], a->[1])
0.00/0.01	 (rule: q(b) -> d, id: 4, possubterms: q(b)->[], b->[1])
0.00/0.01	
0.00/0.01	-> Unifications:
0.00/0.01	(R1 unifies with R2 at p: [1], l: f(g(x,a,b)), lp: g(x,a,b), sig: {x -> f(h(c,d)),x' -> a,y -> b}, l': g(f(h(c,d)),x',y), r: x, r': h(p(x'),q(x')))
0.00/0.01	
0.00/0.01	-> Critical pairs info:
0.00/0.01	<f(h(p(a),q(a))),f(h(c,d))>   =>  Not trivial, Not overlay, Proper, NW0, N1
0.00/0.01	
0.00/0.01	-> Problem conclusions:
0.00/0.01	 Left linear, Not right linear, Not linear
0.00/0.01	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal
0.00/0.01	 Not Huet-Levy confluent, Not Newman confluent
0.00/0.01	 R is a TRS 
0.00/0.01	 Maybe confluent
0.00/0.01	
0.00/0.01	
0.00/0.01	Problem 1: 
0.00/0.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.01	Confluence Problem:
0.00/0.01	(VAR x y)
0.00/0.01	(REPLACEMENT-MAP
0.00/0.01	(f 1)
0.00/0.01	(g 1, 2, 3)
0.00/0.01	(p 1)
0.00/0.01	(q 1)
0.00/0.01	(c)
0.00/0.01	(d)
0.00/0.01	(h 1, 2)
0.00/0.01	)
0.00/0.01	(RULES
0.00/0.01	f(g(x,a,b)) -> x
0.00/0.01	g(f(h(c,d)),x,y) -> h(p(x),q(x))
0.00/0.01	p(a) -> c
0.00/0.01	q(b) -> d
0.00/0.01	)
0.00/0.01	
0.00/0.01	Critical Pairs:
0.00/0.01	<f(h(p(a),q(a))),f(h(c,d))>   =>  Not trivial, Not overlay, Proper, NW0, N1
0.00/0.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.01	
0.00/0.01	Critical Pairs Distributor Processor:
0.00/0.01	
0.00/0.01	
0.00/0.01	Problem 1: 
0.00/0.01	No Convergence Brute Force Procedure:
0.00/0.01	-> Rewritings:
0.00/0.01	s: f(h(p(a),q(a)))
0.00/0.01	Nodes: [0,1]
0.00/0.01	Edges: [(0,1)]
0.00/0.01	ID: 0 => ('f(h(p(a),q(a)))', D0)
0.00/0.01	ID: 1 => ('f(h(c,q(a)))', D1, R3, P[1, 1], S{}), NR: 'c'
0.00/0.01	t: f(h(c,d))
0.00/0.01	Nodes: [0]
0.00/0.01	Edges: []
0.00/0.01	ID: 0 => ('f(h(c,d))', D0)
0.00/0.01	f(h(p(a),q(a))) ->* no union *<- f(h(c,d))
0.00/0.01	"Not joinable"
0.00/0.01	
0.00/0.01	The problem is not confluent.
0.00/0.01	EOF