YES

Consider the TRS R consisting of the following rewrite rules:

	f(x,y) -> g1(x,x,y)
	f(x,y) -> g1(y,x,x)
	f(x,y) -> g2(x,y,y)
	f(x,y) -> g2(y,y,x)
	g1(x,x,y) -> h(x,y)
	g1(y,x,x) -> h(x,y)
	g2(x,y,y) -> h(x,y)
	g2(y,y,x) -> h(x,y)
	h(x,x) -> x

The TRS R is terminating because R is roof-raise-bounded for
the set of all ground terms by 2.
A raise-compatible and quasi-deterministic tree automaton compatible
with roof(R) and the set of all ground terms has
	- 1 state (1,...,1)
	- 1 final state (1)
	- 8 transitions:
		f_0(1,1) -> 1
		h_2(1,1) -> 1
		h_1(1,1) -> 1
		h_0(1,1) -> 1
		g1_1(1,1,1) -> 1
		g1_0(1,1,1) -> 1
		g2_1(1,1,1) -> 1
		g2_0(1,1,1) -> 1
		


___________________________________________________________________
TTTbox (0.011 seconds) - April 13, 2007
Source file - /home/ami/mkorp/Testbench/tpdb-3.2/TRS/various/06.trs