MAYBE
242.00/63.01	MAYBE
242.00/63.02	
242.00/63.02	Problem:
242.00/63.02	 0(1(0(x1))) -> 2(2(0(0(x1))))
242.00/63.02	 2(1(1(x1))) -> 2(2(1(2(2(x1)))))
242.00/63.02	 0(0(0(1(0(0(x1)))))) -> 1(2(1(2(0(2(0(2(2(2(1(2(2(1(x1))))))))))))))
242.00/63.02	 0(0(2(1(2(2(x1)))))) -> 2(0(2(0(2(2(1(x1)))))))
242.00/63.02	 2(0(0(0(0(1(x1)))))) -> 2(0(0(2(2(1(1(2(1(x1)))))))))
242.00/63.02	 0(1(0(1(2(1(0(1(x1)))))))) -> 0(1(0(1(2(2(2(1(1(x1)))))))))
242.00/63.02	 0(2(0(1(0(1(0(1(x1)))))))) -> 0(0(1(2(0(2(2(1(1(2(x1))))))))))
242.00/63.02	 1(1(0(0(0(0(2(1(x1)))))))) -> 0(0(0(0(2(2(1(0(2(1(x1))))))))))
242.00/63.02	 1(2(0(0(2(2(2(0(x1)))))))) -> 2(1(2(1(2(2(2(2(0(x1)))))))))
242.00/63.02	 1(2(1(0(2(0(1(1(x1)))))))) -> 2(1(1(0(2(2(0(1(1(x1)))))))))
242.00/63.02	 0(0(0(1(1(2(0(2(1(x1))))))))) -> 1(1(2(2(0(0(1(2(1(1(2(2(1(2(x1))))))))))))))
242.00/63.02	 0(0(2(1(2(0(1(0(0(x1))))))))) -> 0(2(2(0(2(1(2(1(2(1(0(x1)))))))))))
242.00/63.02	 0(0(2(1(0(2(1(2(2(2(x1)))))))))) -> 1(1(2(2(0(0(0(2(2(2(x1))))))))))
242.00/63.02	 0(2(1(1(2(0(0(0(0(1(x1)))))))))) -> 0(0(0(1(2(2(0(0(0(0(2(2(2(x1)))))))))))))
242.00/63.02	 0(2(1(1(2(2(0(0(0(1(x1)))))))))) -> 1(2(0(1(0(1(0(2(0(2(2(x1)))))))))))
242.00/63.02	 1(1(2(1(0(1(1(1(0(1(x1)))))))))) -> 2(1(1(0(2(2(0(2(1(0(2(2(x1))))))))))))
242.00/63.02	 0(0(0(2(1(1(0(1(0(1(1(x1))))))))))) -> 0(2(0(0(1(2(2(1(0(2(2(2(1(x1)))))))))))))
242.00/63.02	 0(0(1(1(1(2(2(0(1(1(0(x1))))))))))) ->
242.00/63.02	 2(2(0(1(2(1(0(1(2(2(1(0(2(2(2(2(0(2(2(1(x1))))))))))))))))))))
242.00/63.02	 0(1(0(0(2(2(2(0(2(1(2(x1))))))))))) -> 2(2(0(2(1(2(2(1(1(2(2(1(1(x1)))))))))))))
242.00/63.02	 0(1(2(0(2(1(0(1(2(0(0(x1))))))))))) -> 1(1(2(0(2(1(1(0(2(2(1(2(x1))))))))))))
242.00/63.02	 0(1(2(1(0(2(1(0(1(1(1(x1))))))))))) -> 1(0(1(1(0(2(2(0(0(1(2(0(x1))))))))))))
242.00/63.02	 0(1(2(1(1(2(1(2(0(0(1(x1))))))))))) -> 2(2(2(2(2(2(1(2(0(0(2(0(0(x1)))))))))))))
242.00/63.02	 0(2(1(1(2(0(1(2(2(0(0(x1))))))))))) -> 2(1(2(2(2(0(1(0(0(0(1(x1)))))))))))
242.00/63.02	 0(0(2(0(0(1(1(0(0(2(0(0(x1)))))))))))) -> 2(1(0(2(0(2(2(1(2(1(0(0(1(x1)))))))))))))
242.00/63.02	 0(0(2(2(1(1(1(0(1(2(0(1(x1)))))))))))) -> 0(2(1(1(2(2(2(1(1(2(2(1(0(2(x1))))))))))))))
242.00/63.02	 0(1(0(1(2(0(2(0(2(1(2(1(x1)))))))))))) -> 0(0(0(2(0(1(2(2(1(2(0(0(0(x1)))))))))))))
242.00/63.02	 0(1(1(0(0(2(1(0(1(2(1(1(x1)))))))))))) -> 1(2(2(0(2(2(1(1(0(1(1(0(2(x1)))))))))))))
242.00/63.02	 1(0(1(0(2(2(1(0(1(0(1(0(x1)))))))))))) -> 1(0(2(0(2(2(1(0(0(1(1(0(2(2(x1))))))))))))))
242.00/63.02	 2(0(2(0(1(2(2(0(0(1(2(1(x1)))))))))))) -> 2(2(2(2(2(1(1(0(0(1(0(0(x1))))))))))))
242.00/63.02	 2(1(1(1(0(0(1(0(0(0(2(0(x1)))))))))))) -> 2(1(0(0(2(2(1(2(2(2(0(2(2(0(0(0(1(x1)))))))))))))))))
242.00/63.02	 0(0(0(2(0(2(1(2(1(1(0(0(0(x1))))))))))))) -> 0(0(0(2(2(2(0(0(0(0(1(1(1(x1)))))))))))))
242.00/63.02	 0(0(1(0(2(0(1(2(0(2(0(2(1(x1))))))))))))) ->
242.00/63.02	 2(1(1(2(2(2(0(2(2(2(2(2(1(0(1(2(2(0(1(2(2(2(0(0(x1))))))))))))))))))))))))
242.00/63.02	 0(0(2(2(0(2(2(0(1(2(1(1(0(x1))))))))))))) -> 1(2(2(2(2(0(0(1(1(1(2(2(1(0(2(2(x1))))))))))))))))
242.00/63.02	 1(1(0(0(1(2(0(1(1(0(1(2(1(x1))))))))))))) ->
242.00/63.02	 1(2(2(2(1(2(1(2(1(2(1(1(2(1(2(0(2(1(1(2(0(2(2(1(0(x1)))))))))))))))))))))))))
242.00/63.02	 0(1(0(2(0(2(1(1(0(1(1(1(0(0(x1)))))))))))))) ->
242.00/63.02	 0(2(0(0(0(2(2(2(1(2(0(1(0(0(1(0(1(x1)))))))))))))))))
242.00/63.02	 0(2(0(2(0(0(1(0(0(1(0(2(0(0(x1)))))))))))))) -> 1(1(2(0(1(1(0(0(1(2(2(0(2(1(1(0(x1))))))))))))))))
242.00/63.02	 1(0(2(0(1(0(1(0(1(0(1(2(1(1(x1)))))))))))))) ->
242.00/63.02	 0(1(2(2(1(2(0(2(2(0(0(1(1(2(0(1(2(1(1(x1)))))))))))))))))))
242.00/63.02	 1(1(2(0(1(0(1(1(1(1(1(1(0(2(x1)))))))))))))) ->
242.00/63.02	 1(0(1(1(0(1(2(2(0(1(1(2(2(1(1(0(1(2(0(2(2(x1)))))))))))))))))))))
242.00/63.02	 2(1(0(2(0(1(2(0(1(0(0(2(1(0(x1)))))))))))))) ->
242.00/63.02	 0(2(2(0(0(2(2(0(0(0(0(1(1(2(2(0(1(2(x1))))))))))))))))))
242.00/63.02	 0(0(1(2(0(2(1(2(0(1(0(1(0(1(2(x1))))))))))))))) ->
242.00/63.02	 0(1(0(0(2(0(0(1(2(1(0(2(0(2(0(2(2(1(2(2(x1))))))))))))))))))))
242.00/63.02	 0(1(2(1(0(0(0(1(2(0(0(1(0(2(1(x1))))))))))))))) ->
242.00/63.02	 0(2(1(1(0(0(0(2(0(1(2(1(1(0(0(2(2(x1)))))))))))))))))
242.00/63.02	 1(0(1(1(2(0(0(0(2(2(0(2(0(0(1(x1))))))))))))))) ->
242.00/63.02	 1(0(0(0(0(0(1(1(2(2(1(2(0(0(2(2(2(0(2(x1)))))))))))))))))))
242.00/63.02	 1(2(1(0(1(0(1(1(2(1(2(2(1(2(0(x1))))))))))))))) ->
242.00/63.02	 2(0(2(0(0(0(2(1(2(2(1(1(1(0(2(2(x1))))))))))))))))
242.00/63.02	 1(2(1(1(0(0(1(2(1(1(2(1(2(1(2(x1))))))))))))))) ->
242.00/63.02	 2(2(1(0(2(0(0(1(1(2(2(0(2(2(0(0(2(2(2(2(0(2(2(x1)))))))))))))))))))))))
242.00/63.02	 2(0(1(1(0(0(1(0(2(1(1(0(0(0(1(x1))))))))))))))) ->
242.00/63.02	 2(2(1(2(0(2(2(1(0(2(2(0(2(2(0(2(1(0(0(0(1(2(1(x1)))))))))))))))))))))))
242.00/63.02	 2(2(0(2(1(2(0(0(0(1(1(1(2(1(1(x1))))))))))))))) ->
242.00/63.02	 2(2(0(1(2(2(1(1(2(1(0(2(1(0(2(0(0(2(2(2(2(1(1(2(x1))))))))))))))))))))))))
242.00/63.02	 0(0(2(1(2(1(1(1(0(0(2(1(2(0(0(1(x1)))))))))))))))) ->
242.00/63.02	 0(1(2(2(0(1(1(1(2(1(2(1(0(2(0(2(0(2(2(1(2(2(2(0(0(0(0(2(2(2(x1))))))))))))))))))))))))))))))
242.00/63.04	 1(0(0(1(0(1(1(0(2(0(0(2(1(0(2(0(x1)))))))))))))))) ->
242.00/63.04	 0(2(2(2(2(0(0(0(2(2(1(2(1(1(2(2(2(2(x1))))))))))))))))))
242.00/63.04	 1(0(1(2(0(2(1(0(2(0(0(1(2(0(0(1(x1)))))))))))))))) ->
242.00/63.04	 0(0(1(1(2(0(0(0(2(2(2(1(0(1(0(1(x1))))))))))))))))
242.00/63.04	 0(0(1(1(2(0(0(1(0(0(2(0(1(1(0(1(0(x1))))))))))))))))) ->
242.00/63.04	 0(0(0(0(1(2(2(1(0(1(0(0(0(1(1(0(1(x1)))))))))))))))))
242.00/63.04	 0(2(0(1(0(2(0(1(1(0(1(1(1(0(0(1(0(x1))))))))))))))))) ->
242.00/63.04	 2(2(0(0(1(0(2(2(2(0(1(0(2(1(0(2(2(0(2(x1)))))))))))))))))))
242.00/63.04	 0(2(0(1(1(0(1(2(0(0(0(0(2(0(2(0(0(x1))))))))))))))))) ->
242.00/63.04	 0(2(2(2(2(2(0(2(0(0(2(1(1(1(0(1(0(1(x1))))))))))))))))))
242.00/63.04	 1(1(0(0(1(1(2(1(0(0(0(1(2(0(2(0(1(x1))))))))))))))))) ->
242.00/63.04	 2(0(2(0(0(1(2(0(0(1(0(2(0(2(2(1(2(1(1(1(1(x1)))))))))))))))))))))
242.00/63.04	 1(1(1(0(2(2(1(0(0(0(0(1(0(2(1(1(2(x1))))))))))))))))) ->
242.00/63.04	 1(0(1(2(2(0(0(2(2(0(1(2(0(1(2(2(1(2(1(2(0(2(2(x1)))))))))))))))))))))))
242.00/63.04	 1(2(0(1(2(0(0(1(0(1(0(1(2(2(2(1(1(x1))))))))))))))))) ->
242.00/63.04	 0(1(0(2(2(2(2(2(2(2(2(0(2(2(2(2(0(2(1(0(1(0(2(2(2(2(1(1(2(x1)))))))))))))))))))))))))))))
242.00/63.04	 2(1(2(2(0(0(0(0(1(1(0(0(1(1(0(1(2(x1))))))))))))))))) ->
242.00/63.04	 2(1(2(1(0(2(1(1(0(1(2(2(1(0(2(2(1(1(2(2(2(1(2(x1)))))))))))))))))))))))
242.00/63.04	 1(0(0(2(1(0(2(1(2(0(1(0(1(0(0(1(2(1(x1)))))))))))))))))) ->
242.00/63.04	 0(1(1(0(0(0(0(1(1(1(1(0(2(2(1(0(2(2(0(2(0(0(x1))))))))))))))))))))))
242.00/63.04	 1(2(1(2(0(1(2(2(1(2(1(0(1(2(1(0(0(1(x1)))))))))))))))))) ->
242.00/63.04	 1(2(1(1(1(1(2(0(2(2(2(2(0(0(1(0(1(1(x1))))))))))))))))))
242.00/63.04	 2(0(0(1(0(2(1(1(2(0(1(2(1(0(0(1(2(1(x1)))))))))))))))))) ->
242.00/63.04	 2(0(0(2(0(2(2(2(0(1(1(0(1(0(1(0(2(1(0(0(x1))))))))))))))))))))
242.00/63.04	 0(1(0(2(0(0(1(2(2(2(1(2(2(0(0(1(2(1(1(x1))))))))))))))))))) ->
242.00/63.04	 0(2(0(2(2(2(2(1(2(1(0(1(0(0(0(0(2(2(2(0(x1))))))))))))))))))))
242.00/63.04	 0(1(1(2(1(2(0(2(1(1(1(0(1(2(2(0(0(0(0(x1))))))))))))))))))) ->
242.00/63.04	 0(1(0(1(1(1(1(1(2(2(0(1(1(0(0(2(2(2(2(2(0(1(2(2(2(2(x1))))))))))))))))))))))))))
242.00/63.04	 0(1(2(1(1(2(0(1(1(0(1(1(0(1(0(1(2(0(1(x1))))))))))))))))))) ->
242.00/63.04	 0(0(2(1(0(2(1(0(1(2(2(1(1(0(1(1(2(2(2(1(0(1(0(x1)))))))))))))))))))))))
242.00/63.04	 0(2(1(0(0(2(1(2(1(0(2(1(0(0(0(2(0(2(2(x1))))))))))))))))))) ->
242.00/63.04	 1(2(2(2(2(1(0(1(2(0(2(0(2(0(0(1(2(2(2(0(2(2(2(1(x1))))))))))))))))))))))))
242.00/63.04	 1(1(1(2(0(2(0(1(0(0(1(0(0(2(0(0(0(1(0(x1))))))))))))))))))) ->
242.00/63.04	 1(2(0(2(2(0(0(1(1(2(2(0(1(0(0(1(1(0(1(2(0(x1)))))))))))))))))))))
242.00/63.04	 2(0(0(2(2(1(0(2(0(0(0(2(2(1(0(0(1(1(0(x1))))))))))))))))))) ->
242.00/63.04	 2(0(1(1(2(1(2(2(2(0(1(2(2(1(1(1(2(0(0(2(2(2(2(2(x1))))))))))))))))))))))))
242.00/63.04	 2(0(1(0(2(0(2(0(0(0(0(2(1(0(1(0(2(1(0(x1))))))))))))))))))) ->
242.00/63.04	 2(0(1(2(2(2(1(2(1(2(1(1(0(2(2(0(0(0(2(2(0(0(1(2(x1))))))))))))))))))))))))
242.00/63.04	 2(0(1(1(1(2(2(1(1(1(0(2(2(2(0(1(1(1(0(x1))))))))))))))))))) ->
242.00/63.04	 2(1(2(1(1(1(1(1(0(1(2(2(1(2(2(0(2(2(2(0(x1))))))))))))))))))))
242.00/63.04	 2(1(0(1(2(1(1(1(0(2(1(1(1(0(1(2(1(1(0(x1))))))))))))))))))) ->
242.00/63.04	 0(2(2(1(2(0(1(0(2(1(2(2(2(2(1(2(1(2(0(0(0(x1)))))))))))))))))))))
242.00/63.04	 0(0(2(0(2(1(0(2(1(2(1(1(1(0(2(1(0(1(0(0(x1)))))))))))))))))))) ->
242.00/63.04	 1(1(0(2(2(0(1(0(1(0(0(2(1(2(0(1(2(1(0(0(x1))))))))))))))))))))
242.00/63.04	 0(1(1(1(2(1(1(0(1(0(0(0(0(2(0(2(1(0(1(0(x1)))))))))))))))))))) ->
242.00/63.04	 2(2(2(2(0(1(2(2(0(1(0(1(1(0(1(2(2(1(0(2(1(2(1(1(1(1(1(1(x1))))))))))))))))))))))))))))
242.00/63.04	 0(2(0(0(0(1(2(1(0(1(1(2(1(0(0(0(1(1(2(0(x1)))))))))))))))))))) ->
242.00/63.04	 2(2(1(0(1(0(0(0(2(2(2(2(0(1(1(0(2(2(0(1(1(x1)))))))))))))))))))))
242.00/63.04	 0(2(0(1(2(0(0(1(1(0(1(0(2(1(1(0(2(1(0(1(x1)))))))))))))))))))) ->
242.00/63.04	 0(1(1(0(0(0(1(0(2(2(0(0(2(0(2(1(1(1(1(1(x1))))))))))))))))))))
242.00/63.04	 1(0(1(2(0(0(1(1(0(1(1(2(1(1(1(1(0(2(1(1(x1)))))))))))))))))))) ->
242.00/63.04	 2(2(0(2(2(0(2(1(0(2(1(1(2(0(2(2(1(2(0(0(1(0(0(0(1(2(0(2(x1))))))))))))))))))))))))))))
242.00/63.04	 1(0(1(2(0(2(0(0(1(1(1(0(2(1(0(0(0(1(0(0(x1)))))))))))))))))))) ->
242.00/63.04	 0(0(2(0(2(2(0(2(0(2(1(2(1(0(2(2(2(2(0(0(1(0(2(0(2(x1)))))))))))))))))))))))))
242.00/63.04	 1(0(2(0(0(0(1(0(0(1(2(1(1(0(0(0(1(1(1(0(x1)))))))))))))))))))) ->
242.00/63.04	 2(2(1(0(2(1(0(1(1(2(2(0(0(2(1(2(0(2(0(2(2(2(1(0(x1))))))))))))))))))))))))
242.00/63.04	 1(0(2(1(0(2(0(1(1(2(0(0(1(1(1(2(1(0(1(1(x1)))))))))))))))))))) ->
242.00/63.04	 1(0(2(2(2(1(0(1(1(1(2(1(0(0(1(2(0(2(1(1(1(2(2(2(2(0(0(2(2(2(x1))))))))))))))))))))))))))))))
242.00/63.04	 0(0(0(1(2(1(2(0(2(0(2(0(0(1(1(0(0(1(1(1(1(x1))))))))))))))))))))) ->
242.00/63.04	 2(1(2(2(0(0(1(2(1(2(1(2(0(1(2(2(1(2(1(2(0(1(2(0(2(2(x1))))))))))))))))))))))))))
242.00/63.04	 0(0(2(1(1(0(2(0(2(1(2(1(2(0(2(1(2(0(0(0(0(x1))))))))))))))))))))) ->
242.00/63.05	 0(0(2(2(2(1(2(1(0(2(1(2(1(2(0(2(1(0(1(2(0(1(0(1(x1))))))))))))))))))))))))
242.00/63.05	 0(1(1(1(1(0(2(1(0(1(0(1(0(2(1(2(1(0(0(2(0(x1))))))))))))))))))))) ->
242.00/63.05	 2(2(1(2(2(1(2(0(0(2(2(1(2(1(1(0(0(1(1(0(2(1(2(2(x1))))))))))))))))))))))))
242.00/63.05	 0(2(0(1(1(0(0(2(0(2(0(1(0(0(0(1(0(1(0(0(0(x1))))))))))))))))))))) ->
242.00/63.05	 0(0(1(1(2(2(0(1(1(0(2(2(0(2(2(0(2(1(1(2(0(0(2(x1)))))))))))))))))))))))
242.00/63.05	 1(0(1(1(0(1(0(1(2(1(1(0(1(0(0(0(0(2(0(1(1(x1))))))))))))))))))))) ->
242.00/63.05	 2(0(0(0(2(0(2(1(1(0(0(2(0(0(1(0(0(0(2(2(2(2(x1))))))))))))))))))))))
242.00/63.05	 1(0(1(1(0(2(2(1(1(1(1(0(0(2(1(2(1(2(1(0(0(x1))))))))))))))))))))) ->
242.00/63.05	 1(2(2(1(2(1(1(0(0(2(0(1(0(1(1(1(2(2(2(2(1(2(2(2(2(0(2(x1)))))))))))))))))))))))))))
242.00/63.05	 1(2(0(0(0(2(1(0(2(0(2(0(0(1(0(2(1(0(0(1(1(x1))))))))))))))))))))) ->
242.00/63.05	 0(1(0(0(0(2(2(1(2(1(2(0(0(1(1(2(2(1(2(2(2(2(1(1(1(x1)))))))))))))))))))))))))
242.00/63.05	 1(2(1(1(0(0(2(0(1(0(2(2(0(1(1(1(2(0(0(2(0(x1))))))))))))))))))))) ->
242.00/63.05	 1(1(0(1(2(2(2(1(1(1(2(2(1(1(1(2(1(0(2(1(1(2(2(2(1(2(2(0(x1))))))))))))))))))))))))))))
242.00/63.05	 0(0(1(1(1(0(1(1(0(0(2(2(0(2(1(2(1(2(1(0(1(1(x1)))))))))))))))))))))) ->
242.00/63.05	 1(0(2(2(2(0(1(2(2(1(0(1(0(0(1(1(1(2(0(1(2(0(2(1(0(2(2(2(2(0(x1))))))))))))))))))))))))))))))
242.00/63.05	 0(1(0(2(0(0(1(1(1(1(0(0(1(2(1(1(0(2(1(1(1(0(x1)))))))))))))))))))))) ->
242.00/63.05	 0(1(2(0(0(0(0(1(0(1(0(0(0(0(0(1(0(2(0(2(2(0(0(0(x1))))))))))))))))))))))))
242.00/63.05	 1(0(1(1(0(0(2(0(1(1(0(1(2(1(1(1(0(1(2(1(0(0(x1)))))))))))))))))))))) ->
242.00/63.05	 2(2(2(1(1(2(2(0(1(1(2(1(0(1(0(0(2(1(1(2(2(1(1(1(0(1(x1))))))))))))))))))))))))))
242.00/63.05	 0(0(1(1(0(1(0(1(0(1(1(2(2(2(1(1(2(2(0(2(1(1(1(x1))))))))))))))))))))))) ->
242.00/63.05	 2(1(1(2(2(0(1(2(0(2(2(2(2(2(0(1(2(0(2(2(1(1(1(2(1(0(0(0(1(1(x1))))))))))))))))))))))))))))))
242.00/63.05	 0(2(1(1(0(0(2(1(1(2(0(2(1(1(1(1(2(0(2(0(2(1(0(x1))))))))))))))))))))))) ->
242.00/63.05	 0(1(2(1(2(2(2(2(0(1(0(2(0(1(2(1(2(0(0(2(0(1(2(2(x1))))))))))))))))))))))))
242.00/63.05	 1(1(0(1(1(0(1(1(0(2(1(2(0(1(2(0(2(1(1(1(0(1(2(x1))))))))))))))))))))))) ->
242.00/63.05	 0(2(0(2(2(2(1(0(0(1(1(0(0(1(1(2(2(1(2(2(1(1(0(0(2(1(2(2(x1))))))))))))))))))))))))))))
242.00/63.05	 1(2(0(2(1(1(0(2(2(1(0(1(2(1(1(1(2(0(1(0(1(1(2(x1))))))))))))))))))))))) ->
242.00/63.05	 2(0(0(2(2(0(1(1(0(2(0(2(2(2(2(1(2(0(2(0(1(1(2(2(x1))))))))))))))))))))))))
242.00/63.05	 1(2(1(1(1(2(1(0(1(0(1(1(0(2(1(1(1(2(1(0(2(0(1(x1))))))))))))))))))))))) ->
242.00/63.05	 2(1(1(1(0(0(2(0(1(2(0(1(2(0(2(2(0(2(0(2(0(2(1(2(1(x1)))))))))))))))))))))))))
242.00/63.05	 1(2(1(1(1(2(2(1(0(1(0(1(1(1(1(1(0(0(0(2(1(0(1(x1))))))))))))))))))))))) ->
242.00/63.05	 2(2(1(1(1(0(2(0(0(1(1(0(2(1(1(0(2(2(2(2(2(2(2(2(2(1(x1))))))))))))))))))))))))))
242.00/63.05	 2(0(2(1(0(0(0(2(1(0(2(0(0(2(1(0(2(1(1(2(1(1(2(x1))))))))))))))))))))))) ->
242.00/63.05	 2(2(2(0(1(0(1(1(2(2(2(0(0(2(1(0(2(2(2(2(1(2(2(1(0(0(0(1(2(x1)))))))))))))))))))))))))))))
242.00/63.05	 1(0(2(0(1(0(1(2(1(1(2(0(1(1(0(0(0(0(0(0(2(1(2(1(x1)))))))))))))))))))))))) ->
242.00/63.05	 0(2(2(2(1(1(2(1(0(2(2(0(0(0(2(2(1(0(0(2(0(1(0(0(1(1(0(1(x1))))))))))))))))))))))))))))
242.00/63.05	 2(0(0(0(0(0(2(1(2(2(1(0(2(1(2(0(2(1(0(2(2(0(1(0(x1)))))))))))))))))))))))) ->
242.00/63.05	 0(2(2(0(2(2(2(1(1(1(2(1(1(1(1(1(1(1(2(2(1(2(0(1(1(x1)))))))))))))))))))))))))
242.00/63.05	 2(0(2(0(2(0(1(2(0(2(0(1(0(2(1(0(2(1(1(0(0(1(2(1(x1)))))))))))))))))))))))) ->
242.00/63.05	 2(0(2(0(0(2(1(1(1(0(1(0(0(0(2(2(1(0(1(1(0(0(1(2(0(x1)))))))))))))))))))))))))
242.00/63.05	 2(0(2(0(1(1(1(0(0(2(2(1(0(1(0(2(2(0(1(2(2(1(2(0(1(x1))))))))))))))))))))))))) ->
242.00/63.05	 0(2(0(2(2(1(0(0(2(1(0(2(1(2(2(1(1(1(2(2(0(1(1(2(2(2(x1))))))))))))))))))))))))))
242.00/63.05	 2(1(1(0(1(2(1(2(0(0(1(0(0(1(2(1(2(0(2(1(2(1(1(0(1(x1))))))))))))))))))))))))) ->
242.00/63.05	 2(2(1(1(2(2(1(0(0(0(2(0(0(0(2(2(1(2(0(0(1(0(1(0(0(1(2(1(x1))))))))))))))))))))))))))))
242.00/63.05	 0(0(2(2(0(0(0(2(0(0(0(0(1(1(0(1(0(1(1(1(2(2(1(0(0(2(x1)))))))))))))))))))))))))) ->
242.00/63.05	 1(0(2(0(0(0(1(2(1(1(0(2(0(2(2(0(0(2(1(0(2(2(1(2(2(0(2(0(2(2(x1))))))))))))))))))))))))))))))
242.00/63.05	 0(1(0(2(1(2(0(0(1(1(0(0(0(2(0(2(1(1(0(1(2(0(1(2(1(1(x1)))))))))))))))))))))))))) ->
242.00/63.05	 2(2(2(1(2(2(2(1(0(1(2(0(0(0(1(1(2(0(0(1(2(0(0(0(1(0(1(x1)))))))))))))))))))))))))))
242.00/63.05	 1(0(0(0(1(2(0(1(1(1(0(1(0(1(2(1(1(2(1(0(0(1(0(0(0(1(x1)))))))))))))))))))))))))) ->
242.00/63.05	 2(0(0(2(2(2(2(0(0(1(2(1(2(1(0(0(0(0(2(0(2(0(1(0(0(1(0(x1)))))))))))))))))))))))))))
242.00/63.05	 1(0(2(1(0(1(2(2(0(2(0(0(1(2(0(0(2(1(1(1(1(1(1(2(1(0(x1)))))))))))))))))))))))))) ->
242.00/63.05	 0(0(1(2(2(2(2(2(2(0(0(0(0(1(1(0(1(1(2(2(0(1(0(0(0(1(1(0(1(x1)))))))))))))))))))))))))))))
242.00/63.05	 1(1(2(0(2(0(1(1(1(1(1(2(0(2(0(2(1(0(0(1(2(1(1(0(0(1(x1)))))))))))))))))))))))))) ->
242.00/63.06	 2(1(2(0(0(2(1(1(2(2(0(1(0(0(1(0(1(0(0(1(1(0(2(0(2(2(2(1(x1))))))))))))))))))))))))))))
242.00/63.06	 0(1(0(2(2(2(0(0(1(1(1(2(1(0(1(1(1(0(1(2(1(0(2(0(0(0(2(x1))))))))))))))))))))))))))) ->
242.00/63.06	 2(2(0(2(0(0(2(0(0(0(2(2(1(1(2(0(2(1(1(0(0(2(2(1(2(1(1(2(2(x1)))))))))))))))))))))))))))))
242.00/63.06	 0(1(1(2(0(2(0(0(0(1(2(1(1(2(0(0(2(0(2(2(0(1(1(0(1(0(2(x1))))))))))))))))))))))))))) ->
242.00/63.06	 2(1(2(2(1(2(0(0(1(1(0(1(2(2(2(1(2(1(1(2(0(2(0(2(2(1(1(2(1(x1)))))))))))))))))))))))))))))
242.00/63.06	 1(2(2(2(1(2(2(1(2(0(0(1(1(2(1(1(0(0(2(2(1(2(1(2(2(0(2(x1))))))))))))))))))))))))))) ->
242.00/63.06	 1(2(2(1(1(2(0(1(2(0(2(2(0(2(2(1(0(1(1(2(2(2(1(1(0(2(2(x1)))))))))))))))))))))))))))
242.00/63.06	 0(0(1(2(1(2(0(1(0(1(0(2(0(1(2(0(0(0(1(1(2(0(1(1(0(1(1(0(x1)))))))))))))))))))))))))))) ->
242.00/63.06	 2(1(0(1(0(0(1(1(1(2(2(1(2(1(1(0(1(1(2(2(2(0(2(2(2(2(0(0(1(0(x1))))))))))))))))))))))))))))))
242.00/63.06	 0(0(2(2(0(1(1(1(2(0(0(1(2(1(0(1(2(0(0(2(1(0(1(2(0(0(0(0(x1)))))))))))))))))))))))))))) ->
242.00/63.06	 1(1(0(1(2(1(2(2(2(1(2(0(0(2(1(1(2(1(2(1(0(1(1(0(0(2(2(0(0(0(x1))))))))))))))))))))))))))))))
242.00/63.06	 2(0(2(0(0(2(0(1(0(2(2(2(2(2(1(1(2(0(1(0(1(1(0(2(2(0(2(1(x1)))))))))))))))))))))))))))) ->
242.00/63.06	 2(0(0(0(0(0(2(0(2(2(2(1(2(0(1(0(2(1(1(2(1(2(0(2(2(2(1(1(x1))))))))))))))))))))))))))))
242.00/63.06	
242.00/63.06	Proof:
242.00/63.06	 Open
242.00/63.06	EOF