0.005/0.005	YES
0.005/0.005	
0.005/0.005	Problem 1:
0.005/0.005	
0.005/0.005	
0.005/0.005	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.005/0.005	Confluence Problem:
0.005/0.005	(VAR vNonEmpty:S v_NonEmpty:S:S X:S:S)
0.005/0.005	(STRATEGY CONTEXTSENSITIVE
0.005/0.005	(b)
0.005/0.005	(f)
0.005/0.005	(a)
0.005/0.005	(fSNonEmpty)
0.005/0.005	)
0.005/0.005	(RULES
0.005/0.005	b -> a
0.005/0.005	f(X:S:S,X:S:S) -> f(a,b)
0.005/0.005	)
0.005/0.005	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.005/0.005	
0.005/0.005	
0.005/0.005	Problem 1:
0.005/0.005	
0.005/0.005	CleanTRS Processor:
0.005/0.005	
0.005/0.005	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.005/0.005	Confluence Problem:
0.005/0.005	(VAR vNonEmpty:S v_NonEmpty:S:S X:S:S)
0.005/0.005	(STRATEGY CONTEXTSENSITIVE
0.005/0.005	(b)
0.005/0.005	(f)
0.005/0.005	(a)
0.005/0.005	(fSNonEmpty)
0.005/0.005	)
0.005/0.005	(RULES
0.005/0.005	b -> a
0.005/0.005	f(X:S:S,X:S:S) -> f(a,b)
0.005/0.005	)
0.005/0.005	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.005/0.005	
0.005/0.005	
0.005/0.005	Problem 1:
0.005/0.005	
0.005/0.005	Modular Confluence Combinations Decomposition Processor:
0.005/0.005	It is a CTRS -> No modular confluence
0.005/0.005	
0.005/0.005	Problem 1:
0.005/0.005	Left-Homogeneous u-Replacing Variables Processor:
0.005/0.005	R satisfies LHRV condition
0.005/0.005	
0.005/0.005	Problem 1:
0.005/0.005	Termination Processor:
0.005/0.005	(STRATEGY CONTEXTSENSITIVE
0.005/0.005	(b)
0.005/0.005	(f)
0.005/0.005	(a)
0.005/0.005	(fSNonEmpty)
0.005/0.005	)
0.005/0.005	Terminating?
0.005/0.005	YES
0.005/0.005	
0.005/0.005	Problem 1:
0.005/0.005	
0.005/0.005	(VAR vu95NonEmpty:S vNonEmpty:S v_NonEmptyu58S:S Xu58S:S)
0.005/0.005	(STRATEGY CONTEXTSENSITIVE
0.005/0.005	(b)
0.005/0.005	(f)
0.005/0.005	(a)
0.005/0.005	(fSNonEmpty)
0.005/0.005	)
0.005/0.005	(RULES
0.005/0.005	b -> a
0.005/0.005	f(Xu58S:S,Xu58S:S) -> f(a,b)
0.005/0.005	)
0.005/0.005	
0.005/0.005	Problem 1:
0.005/0.005	
0.005/0.005	Dependency Pairs Processor:
0.005/0.005	-> Pairs:
0.005/0.005	 Empty
0.005/0.005	-> Rules:
0.005/0.005	 b -> a
0.005/0.005	 f(Xu58S:S,Xu58S:S) -> f(a,b)
0.005/0.005	-> Unhiding Rules:
0.005/0.005	 Empty
0.005/0.005	
0.005/0.005	Problem 1:
0.005/0.005	
0.005/0.005	Basic Processor:
0.005/0.005	-> Pairs:
0.005/0.005	 Empty
0.005/0.005	-> Rules:
0.005/0.005	 b -> a
0.005/0.005	 f(Xu58S:S,Xu58S:S) -> f(a,b)
0.005/0.005	-> Unhiding rules:
0.005/0.005	 Empty
0.005/0.005	-> Result:
0.005/0.005	 Set P is empty
0.005/0.005	
0.005/0.005	The problem is finite.
0.005/0.005	
0.005/0.005	Problem 1.1:
0.005/0.005	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.005/0.005	Confluence Problem:
0.005/0.005	(VAR vNonEmpty:S v_NonEmpty:S:S X:S:S)
0.005/0.005	(STRATEGY CONTEXTSENSITIVE
0.005/0.005	(b)
0.005/0.005	(f)
0.005/0.005	(a)
0.005/0.005	(fSNonEmpty)
0.005/0.005	)
0.005/0.005	(RULES
0.005/0.005	b -> a
0.005/0.005	f(X:S:S,X:S:S) -> f(a,b)
0.005/0.005	)
0.005/0.005	Terminating:"YES"
0.005/0.005	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.005/0.005	
0.005/0.005	Huet Levy NW Processor:
0.005/0.005	-> Rules:
0.005/0.005	 b -> a
0.005/0.005	 f(X:S:S,X:S:S) -> f(a,b)
0.005/0.005	-> Vars:
0.005/0.005	 X:S
0.005/0.005	-> UVars:
0.005/0.005	 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.005/0.005	 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X:S], UV-RFrozen: [])
0.005/0.005	-> FVars:
0.005/0.005	 x3
0.005/0.005	-> PVars:
0.005/0.005	 X:S: [x3]
0.005/0.005	
0.005/0.005	-> Rlps:
0.005/0.005	 (rule: b -> a, id: 1, possubterms: b->[])
0.005/0.005	 (rule: f(x3:S,x3:S) -> f(a,b), id: 2, possubterms: f(x3:S,x3:S)->[])
0.005/0.005	
0.005/0.005	-> Unifications:
0.005/0.005	
0.005/0.005	
0.005/0.005	-> Critical pairs info:
0.005/0.005	
0.005/0.005	
0.005/0.005	-> Problem conclusions:
0.005/0.005	 Not left linear, Right linear, Not linear
0.005/0.005	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
0.005/0.005	 Not Huet-Levy confluent, Newman confluent
0.005/0.005	 R is a CS-TRS, Left-homogeneous u-replacing variables
0.005/0.005	
0.005/0.005	
0.005/0.005	The problem is joinable.
0.005/0.005	0.00user 0.01system 0:00.05elapsed 32%CPU (0avgtext+0avgdata 8744maxresident)k
0.005/0.005	11200inputs+0outputs (47major+1207minor)pagefaults 0swaps