[(* 2 $x)]
0.04user 0.00system 0:00.05elapsed 100%CPU (0avgtext+0avgdata 31320maxresident)k
0inputs+0outputs (0major+3672minor)pagefaults 0swaps