0.00/0.01	YES
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 vNonEmpty x)
0.00/0.01	(REPLACEMENT-MAP
0.00/0.01	(f 1)
0.00/0.01	(a)
0.00/0.01	(fSNonEmpty)
0.00/0.01	)
0.00/0.01	(RULES
0.00/0.01	f(a) -> f(f(a))
0.00/0.01	f(x) -> f(a)
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	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	Linearity Procedure:
0.00/0.01	Linear?
0.00/0.01	YES
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 vNonEmpty x)
0.00/0.01	(REPLACEMENT-MAP
0.00/0.01	(f 1)
0.00/0.01	(a)
0.00/0.01	(fSNonEmpty)
0.00/0.01	)
0.00/0.01	(RULES
0.00/0.01	f(a) -> f(f(a))
0.00/0.01	f(x) -> f(a)
0.00/0.01	)
0.00/0.01	Linear:YES
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(a) -> f(f(a))
0.00/0.01	 f(x) -> f(a)
0.00/0.01	-> Vars:
0.00/0.01	 x
0.00/0.01	
0.00/0.01	-> Rlps:
0.00/0.01	 (rule: f(a) -> f(f(a)), id: 1, possubterms: f(a)->[], a->[1])
0.00/0.01	 (rule: f(x) -> f(a), id: 2, possubterms: f(x)->[])
0.00/0.01	
0.00/0.01	-> Unifications:
0.00/0.01	(R2 unifies with R1 at p: [], l: f(x), lp: f(x), sig: {x -> a}, l': f(a), r: f(a), r': f(f(a)))
0.00/0.01	
0.00/0.01	-> Critical pairs info:
0.00/0.01	<f(f(a)),f(a)>   =>  Not trivial, Overlay, Proper, NW0, N1
0.00/0.01	
0.00/0.01	-> Problem conclusions:
0.00/0.01	 Left linear, Right linear, Linear
0.00/0.01	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
0.00/0.01	 Not Huet-Levy confluent, Not Newman confluent
0.00/0.01	 R is a TRS 
0.00/0.01	
0.00/0.01	Problem 1.1: 
0.00/0.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.01	Confluence Problem:
0.00/0.01	(VAR x)
0.00/0.01	(REPLACEMENT-MAP
0.00/0.01	(f 1)
0.00/0.01	(a)
0.00/0.01	(fSNonEmpty)
0.00/0.01	)
0.00/0.01	(RULES
0.00/0.01	f(a) -> f(f(a))
0.00/0.01	f(x) -> f(a)
0.00/0.01	)
0.00/0.01	Critical Pairs:
0.00/0.01	<f(f(a)),f(a)>   =>  Not trivial, Overlay, Proper, NW0, N1
0.00/0.01	Linear:YES
0.00/0.01	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.00/0.01	
0.00/0.01	Strong Confluence Procedure:
0.00/0.01	-> Rewritings:
0.00/0.01	s: f(f(a))
0.00/0.01	Nodes: [0,1,2,3,4,5,6,7,8,9]
0.00/0.01	Edges: [(0,0),(0,1),(0,2),(1,0),(1,1),(1,2),(1,3),(2,0),(2,2),(3,0),(3,1),(3,2),(3,3),(3,4),(4,0),(4,1),(4,2),(4,3),(4,4),(4,5),(5,0),(5,1),(5,2),(5,3),(5,4),(5,5),(5,6),(6,0),(6,1),(6,2),(6,3),(6,4),(6,5),(6,6),(6,7),(7,0),(7,1),(7,2),(7,3),(7,4),(7,5),(7,6),(7,7),(7,8),(8,0),(8,1),(8,2),(8,3),(8,4),(8,5),(8,6),(8,7),(8,8),(8,9)]
0.00/0.01	ID: 0 => ('f(f(a))', D0)
0.00/0.01	ID: 1 => ('f(f(f(a)))', D1, R1, P[1], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 2 => ('f(a)', D1, R2, P[], S{x2 -> f(a)}), NR: 'f(a)'
0.00/0.01	ID: 3 => ('f(f(f(f(a))))', D2, R1, P[1, 1], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 4 => ('f(f(f(f(f(a)))))', D3, R1, P[1, 1, 1], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 5 => ('f(f(f(f(f(f(a))))))', D4, R1, P[1, 1, 1, 1], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 6 => ('f(f(f(f(f(f(f(a)))))))', D5, R1, P[1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 7 => ('f(f(f(f(f(f(f(f(a))))))))', D6, R1, P[1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 8 => ('f(f(f(f(f(f(f(f(f(a)))))))))', D7, R1, P[1, 1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 9 => ('f(f(f(f(f(f(f(f(f(f(a))))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
0.00/0.01	t: f(a)
0.00/0.01	Nodes: [0,1,2,3,4,5,6,7,8]
0.00/0.01	Edges: [(0,0),(0,1),(1,0),(1,1),(1,2),(2,0),(2,1),(2,2),(2,3),(3,0),(3,1),(3,2),(3,3),(3,4),(4,0),(4,1),(4,2),(4,3),(4,4),(4,5),(5,0),(5,1),(5,2),(5,3),(5,4),(5,5),(5,6),(6,0),(6,1),(6,2),(6,3),(6,4),(6,5),(6,6),(6,7),(7,0),(7,1),(7,2),(7,3),(7,4),(7,5),(7,6),(7,7),(7,8)]
0.00/0.01	ID: 0 => ('f(a)', D0)
0.00/0.01	ID: 1 => ('f(f(a))', D1, R1, P[], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 2 => ('f(f(f(a)))', D2, R1, P[1], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 3 => ('f(f(f(f(a))))', D3, R1, P[1, 1], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 4 => ('f(f(f(f(f(a)))))', D4, R1, P[1, 1, 1], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 5 => ('f(f(f(f(f(f(a))))))', D5, R1, P[1, 1, 1, 1], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 6 => ('f(f(f(f(f(f(f(a)))))))', D6, R1, P[1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 7 => ('f(f(f(f(f(f(f(f(a))))))))', D7, R1, P[1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
0.00/0.01	ID: 8 => ('f(f(f(f(f(f(f(f(f(a)))))))))', D8, R1, P[1, 1, 1, 1, 1, 1, 1], S{}), NR: 'f(f(a))'
0.00/0.01	SNodesPath1: f(f(a))
0.00/0.01	TNodesPath1: f(a) -> f(f(a))
0.00/0.01	SNodesPath2: f(f(a)) -> f(f(f(a))) -> f(a)
0.00/0.01	TNodesPath2: f(a)
0.00/0.01	f(f(a)) ->= f(f(a)) *<- f(a)
0.00/0.01	f(a) ->= f(a) *<- f(f(a))
0.00/0.01	"Strongly closed critical pair"
0.00/0.01	
0.00/0.01	The problem is confluent.
0.00/0.01	EOF