yices_lines 386 Bytes