MAYBE 315.32/93.46 MAYBE 315.32/93.46 315.32/93.46 Problem: 315.32/93.46 a(x1) -> b(x1) 315.32/93.46 a(a(x1)) -> a(b(a(x1))) 315.32/93.46 a(b(x1)) -> b(b(b(x1))) 315.32/93.46 a(a(a(x1))) -> a(a(b(a(a(x1))))) 315.32/93.46 a(a(b(x1))) -> a(b(b(a(b(x1))))) 315.32/93.46 a(b(a(x1))) -> b(a(b(b(a(x1))))) 315.32/93.46 a(b(b(x1))) -> b(b(b(b(b(x1))))) 315.32/93.46 a(a(a(a(x1)))) -> a(a(a(b(a(a(a(x1))))))) 315.32/93.46 a(a(a(b(x1)))) -> a(a(b(b(a(a(b(x1))))))) 315.32/93.46 a(a(b(a(x1)))) -> a(b(a(b(a(b(a(x1))))))) 315.32/93.46 a(a(b(b(x1)))) -> a(b(b(b(a(b(b(x1))))))) 315.32/93.46 a(b(a(a(x1)))) -> b(a(a(b(b(a(a(x1))))))) 315.32/93.46 a(b(a(b(x1)))) -> b(a(b(b(b(a(b(x1))))))) 315.32/93.46 a(b(b(a(x1)))) -> b(b(a(b(b(b(a(x1))))))) 315.32/93.46 a(b(b(b(x1)))) -> b(b(b(b(b(b(b(x1))))))) 315.32/93.46 315.32/93.46 Proof: 315.32/93.46 Open 315.32/93.46 EOF