#!/bin/sh
echo "c launch: $*"
echo "c host: `hostname`"
/home/biere/bin/run \
  --time-limit=1000 \
  --space-limit=7000 \
  /home/biere/src/lingeling/lingeling \
  --score=2 \
  -v -n \
  $*
echo "c launch: done"
