swipl stdin_to_stdout.pl