0.00/0.50	NO
0.00/0.50	
0.00/0.50	Problem:
0.00/0.50	a() -> t(c())
0.00/0.50	a() -> t(d())
0.00/0.50	f(x, y) -> z <= x = t(z)
0.00/0.50	g(x, x) -> h(x, x)
0.00/0.50	
0.00/0.50	Proof:
0.00/0.50	This system is not confluent.
0.00/0.50	This system is oriented.
0.00/0.50	For the unconditional CP t(c()) = t(d()) ctcap(t(c())) and ctcap(t(d())) wrt R_u are not unifiable.
0.00/0.50	
0.00/0.51	EOF