# encoding: ascii

(