#!/usr/bin/perl

if ($#ARGV != 0) {
    print "need 1 arg: input file.\n";
    die;
}

$| = 1;				# flush output

$input = $ARGV[0];
$otter="/home/mccune/bin-linux/otter";
$host=`hostname`; chop($host);

$date=`date`; chop($date);

print "Started ploop3 $date on $host.\n";

print "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n";
print `cat $input`;
print "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n";

$i = 0;
while ($prob = <STDIN>) {
    if ($prob =~ /^\s*%/) {
	print $prob;
    }
    else {
	$i++;
	chop $prob;
	$command = "$otter '$prob' < $input  2> /dev/null | egrep '(ERROR|UNIT|EMPTY|^Search stopped|user CPU|clauses kept)'";
	@output = `$command`;
	print "\n$prob  % Job $i\n";
	print @output;
    }
}

$date=`date`; chop($date);

print "Finished ploop3 $date on $host\n";

1;