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)
0.00/0.01	(REPLACEMENT-MAP
0.00/0.01	(f 1)
0.00/0.01	(g 1)
0.00/0.01	)
0.00/0.01	(RULES
0.00/0.01	f(f(x)) -> g(x)
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)
0.00/0.01	(REPLACEMENT-MAP
0.00/0.01	(f 1)
0.00/0.01	(g 1)
0.00/0.01	)
0.00/0.01	(RULES
0.00/0.01	f(f(x)) -> g(x)
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(f(x)) -> g(x)
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(f(x)) -> g(x), id: 1, possubterms: f(f(x))->[], f(x)->[1])
0.00/0.01	
0.00/0.01	-> Unifications:
0.00/0.01	(R1 unifies with R1 at p: [1], l: f(f(x)), lp: f(x), sig: {x -> f(x')}, l': f(f(x')), r: g(x), r': g(x'))
0.00/0.01	
0.00/0.01	-> Critical pairs info:
0.00/0.01	<f(g(x')),g(f(x'))>   =>  Not trivial, Not 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, 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 x')
0.00/0.01	(REPLACEMENT-MAP
0.00/0.01	(f 1)
0.00/0.01	(g 1)
0.00/0.01	)
0.00/0.01	(RULES
0.00/0.01	f(f(x)) -> g(x)
0.00/0.01	)
0.00/0.01	
0.00/0.01	Critical Pairs:
0.00/0.01	<f(g(x')),g(f(x'))>   =>  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(g(x'))
0.00/0.01	Nodes: [0]
0.00/0.01	Edges: []
0.00/0.01	ID: 0 => ('f(g(x'))', D0)
0.00/0.01	t: g(f(x'))
0.00/0.01	Nodes: [0]
0.00/0.01	Edges: []
0.00/0.01	ID: 0 => ('g(f(x'))', D0)
0.00/0.01	f(g(x')) ->* no union *<- g(f(x'))
0.00/0.01	"Not joinable"
0.00/0.01	
0.00/0.01	The problem is not confluent.
0.00/0.01	EOF