(* 10 10)