MAYBE
164.28/54.57	MAYBE
164.28/54.57	
164.28/54.57	Problem:
164.28/54.57	 r1(a(x1)) -> a(a(a(r1(x1))))
164.28/54.57	 r2(a(x1)) -> a(a(a(r2(x1))))
164.28/54.57	 a(l1(x1)) -> l1(a(a(a(x1))))
164.28/54.57	 a(a(l2(x1))) -> l2(a(a(x1)))
164.28/54.57	 r1(b(x1)) -> l1(b(x1))
164.28/54.57	 r2(b(x1)) -> l2(a(b(x1)))
164.28/54.57	 b(l1(x1)) -> b(r2(x1))
164.28/54.57	 b(l2(x1)) -> b(r1(x1))
164.28/54.57	 a(a(x1)) -> x1
164.28/54.57	
164.28/54.57	Proof:
164.28/54.57	 Open
164.28/54.57	EOF