44.90/41.36	YES
44.90/41.36	
44.90/41.36	Problem 1: 
44.90/41.36	
44.90/41.36	
44.90/41.36	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
44.90/41.36	Confluence Problem:
44.90/41.36	(VAR x)
44.90/41.36	(REPLACEMENT-MAP
44.90/41.36	(H 1)
44.90/41.36	(K 1)
44.90/41.36	)
44.90/41.36	(RULES
44.90/41.36	H(H(x)) -> K(x)
44.90/41.36	H(K(x)) -> K(H(x))
44.90/41.36	)
44.90/41.36	
44.90/41.36	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
44.90/41.36	
44.90/41.36	
44.90/41.36	Problem 1: 
44.90/41.36	
44.90/41.36	Problem 1: 
44.90/41.36	
44.90/41.36	Problem 1: 
44.90/41.36	Not CS-TRS Procedure:
44.90/41.36	R is not a CS-TRS
44.90/41.36	
44.90/41.36	Problem 1: 
44.90/41.36	Termination Procedure:
44.90/41.36	Terminating?
44.90/41.36	YES
44.90/41.36	
44.90/41.36	Problem 1: 
44.90/41.36	
44.90/41.36	(VAR vu95NonEmpty x)
44.90/41.36	(RULES
44.90/41.36	H(H(x)) -> K(x)
44.90/41.36	H(K(x)) -> K(H(x))
44.90/41.36	)
44.90/41.36	
44.90/41.36	
44.90/41.36	Problem 1: 
44.90/41.36	
44.90/41.36	Dependency Pairs Processor:
44.90/41.36	-> Pairs:
44.90/41.36	 HSharp(K(x)) -> HSharp(x)
44.90/41.36	-> Rules:
44.90/41.36	 H(H(x)) -> K(x)
44.90/41.36	 H(K(x)) -> K(H(x))
44.90/41.36	
44.90/41.36	Problem 1: 
44.90/41.36	
44.90/41.36	SCC Processor:
44.90/41.36	-> Pairs:
44.90/41.36	 HSharp(K(x)) -> HSharp(x)
44.90/41.36	-> Rules:
44.90/41.36	 H(H(x)) -> K(x)
44.90/41.36	 H(K(x)) -> K(H(x))
44.90/41.36	->Strongly Connected Components:
44.90/41.36	->->Cycle:
44.90/41.36	->->-> Pairs:
44.90/41.36	 HSharp(K(x)) -> HSharp(x)
44.90/41.36	->->-> Rules:
44.90/41.36	 H(H(x)) -> K(x)
44.90/41.36	 H(K(x)) -> K(H(x))
44.90/41.36	
44.90/41.36	Problem 1: 
44.90/41.36	
44.90/41.36	Subterm Processor:
44.90/41.36	-> Pairs:
44.90/41.36	 HSharp(K(x)) -> HSharp(x)
44.90/41.36	-> Rules:
44.90/41.36	 H(H(x)) -> K(x)
44.90/41.36	 H(K(x)) -> K(H(x))
44.90/41.36	->Projection:
44.90/41.36	 pi(HSharp) = 1
44.90/41.36	
44.90/41.36	Problem 1: 
44.90/41.36	
44.90/41.36	SCC Processor:
44.90/41.36	-> Pairs:
44.90/41.36	 Empty
44.90/41.36	-> Rules:
44.90/41.36	 H(H(x)) -> K(x)
44.90/41.36	 H(K(x)) -> K(H(x))
44.90/41.36	->Strongly Connected Components:
44.90/41.36	 There is no strongly connected component
44.90/41.36	
44.90/41.36	The problem is finite.
44.90/41.36	
44.90/41.36	
44.90/41.36	Problem 1: 
44.90/41.36	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
44.90/41.36	Confluence Problem:
44.90/41.36	(VAR x)
44.90/41.36	(REPLACEMENT-MAP
44.90/41.36	(H 1)
44.90/41.36	(K 1)
44.90/41.36	)
44.90/41.36	(RULES
44.90/41.36	H(H(x)) -> K(x)
44.90/41.36	H(K(x)) -> K(H(x))
44.90/41.36	)
44.90/41.36	
44.90/41.36	Terminating:"YES"
44.90/41.36	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
44.90/41.36	
44.90/41.36	Huet Levy NW Procedure:
44.90/41.36	-> Rules:
44.90/41.36	 H(H(x)) -> K(x)
44.90/41.36	 H(K(x)) -> K(H(x))
44.90/41.36	-> Vars:
44.90/41.36	 x, x
44.90/41.36	
44.90/41.36	-> Rlps:
44.90/41.36	 (rule: H(H(x)) -> K(x), id: 1, possubterms: H(H(x))->[], H(x)->[1])
44.90/41.36	 (rule: H(K(x)) -> K(H(x)), id: 2, possubterms: H(K(x))->[], K(x)->[1])
44.90/41.36	
44.90/41.36	-> Unifications:
44.90/41.36	(R1 unifies with R1 at p: [1], l: H(H(x)), lp: H(x), sig: {x -> H(x')}, l': H(H(x')), r: K(x), r': K(x'))
44.90/41.36	(R1 unifies with R2 at p: [1], l: H(H(x)), lp: H(x), sig: {x -> K(x')}, l': H(K(x')), r: K(x), r': K(H(x')))
44.90/41.36	
44.90/41.36	-> Critical pairs info:
44.90/41.36	<H(K(H(x'))),K(K(x'))>   =>  Not trivial, Not overlay, Proper, NW1, N1
44.90/41.36	<H(K(x')),K(H(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N2
44.90/41.36	
44.90/41.36	-> Problem conclusions:
44.90/41.36	 Left linear, Right linear, Linear
44.90/41.36	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal
44.90/41.36	 Not Huet-Levy confluent, Not Newman confluent
44.90/41.36	 R is a TRS 
44.90/41.36	 Maybe confluent
44.90/41.36	
44.90/41.36	
44.90/41.36	Problem 1: 
44.90/41.36	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
44.90/41.36	Confluence Problem:
44.90/41.36	(VAR x x')
44.90/41.36	(REPLACEMENT-MAP
44.90/41.36	(H 1)
44.90/41.36	(K 1)
44.90/41.36	)
44.90/41.36	(RULES
44.90/41.36	H(H(x)) -> K(x)
44.90/41.36	H(K(x)) -> K(H(x))
44.90/41.36	)
44.90/41.36	
44.90/41.36	Critical Pairs:
44.90/41.36	<H(K(H(x'))),K(K(x'))>   =>  Not trivial, Not overlay, Proper, NW1, N1
44.90/41.36	<H(K(x')),K(H(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N2
44.90/41.36	Terminating:"YES"
44.90/41.36	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
44.90/41.36	
44.90/41.36	Critical Pairs Distributor Processor:
44.90/41.36	
44.90/41.36	
44.90/41.36	
44.90/41.36	The problem is decomposed in 2 subproblems.
44.90/41.36	
44.90/41.36	Problem 1.1: 
44.90/41.36	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
44.90/41.36	Confluence Problem:
44.90/41.36	(VAR x x')
44.90/41.36	(REPLACEMENT-MAP
44.90/41.36	(H 1)
44.90/41.36	(K 1)
44.90/41.36	)
44.90/41.36	(RULES
44.90/41.36	H(H(x)) -> K(x)
44.90/41.36	H(K(x)) -> K(H(x))
44.90/41.36	)
44.90/41.36	
44.90/41.36	Critical Pairs:
44.90/41.36	<H(K(H(x'))),K(K(x'))>   =>  Not trivial, Not overlay, Proper, NW1, N1
44.90/41.36	Terminating:"YES"
44.90/41.36	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
44.90/41.36	
44.90/41.36	Huet Brute Force Joinability Procedure:
44.90/41.36	-> Rewritings:
44.90/41.36	s: H(K(H(x')))
44.90/41.36	Nodes: [0,1,2]
44.90/41.36	Edges: [(0,1),(1,2)]
44.90/41.36	ID: 0 => ('H(K(H(x')))', D0)
44.90/41.36	ID: 1 => ('K(H(H(x')))', D1, R2, P[], S{x3 -> H(x')}), NR: 'K(H(H(x')))'
44.90/41.36	ID: 2 => ('K(K(x'))', D2, R1, P[1], S{x2 -> x'}), NR: 'K(x')'
44.90/41.36	t: K(K(x'))
44.90/41.36	Nodes: [0]
44.90/41.36	Edges: []
44.90/41.36	ID: 0 => ('K(K(x'))', D0)
44.90/41.36	SNodesPath: H(K(H(x'))) -> K(H(H(x'))) -> K(K(x'))
44.90/41.36	TNodesPath: K(K(x'))
44.90/41.36	H(K(H(x'))) ->* K(K(x')) *<- K(K(x'))
44.90/41.36	"Joinable"
44.90/41.36	
44.90/41.36	The problem is confluent.
44.90/41.36	
44.90/41.36	Problem 1.2: 
44.90/41.36	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
44.90/41.36	Confluence Problem:
44.90/41.36	(VAR x x')
44.90/41.36	(REPLACEMENT-MAP
44.90/41.36	(H 1)
44.90/41.36	(K 1)
44.90/41.36	)
44.90/41.36	(RULES
44.90/41.36	H(H(x)) -> K(x)
44.90/41.36	H(K(x)) -> K(H(x))
44.90/41.36	)
44.90/41.36	
44.90/41.36	Critical Pairs:
44.90/41.36	<H(K(x')),K(H(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N2
44.90/41.36	Terminating:"YES"
44.90/41.36	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
44.90/41.36	
44.90/41.36	Huet Brute Force Joinability Procedure:
44.90/41.36	-> Rewritings:
44.90/41.36	s: H(K(x'))
44.90/41.36	Nodes: [0,1]
44.90/41.36	Edges: [(0,1)]
44.90/41.36	ID: 0 => ('H(K(x'))', D0)
44.90/41.36	ID: 1 => ('K(H(x'))', D1, R2, P[], S{x3 -> x'}), NR: 'K(H(x'))'
44.90/41.36	t: K(H(x'))
44.90/41.36	Nodes: [0]
44.90/41.36	Edges: []
44.90/41.36	ID: 0 => ('K(H(x'))', D0)
44.90/41.36	SNodesPath: H(K(x')) -> K(H(x'))
44.90/41.36	TNodesPath: K(H(x'))
44.90/41.36	H(K(x')) ->* K(H(x')) *<- K(H(x'))
44.90/41.36	"Joinable"
44.90/41.36	
44.90/41.36	The problem is confluent.
44.90/95.71	EOF