#!/usr/bin/perl

@tot = ();
@tot_tm = ();

$n = 0;
$n_time = 0;

while (<>) {
chomp;
/FILE (.*)/ and $f = $1;
/SAT=True/ and $sat = "SAT";
/SAT=False/ and $sat = "UNSAT";
/running time.*\]: (\S+)/ and $time = $1;
$time =~ s/s//;
/totals:\s*(.*)/ and do {
  #$sat eq "SAT" and next;
  $tot = $1;
  @times = split /\s+/, $tot;

  ($quant_loop,$dummy1,$dummy2,$conflict_size,$conflict_quant,$instances,$forall,$select,$subt,$ss) = @times;
  next if ($quant_loop == 0 || $conflict_quant == 0);

  @res = ();

  push @res, ($quant_loop, $conflict_size/$quant_loop, $conflict_quant/$quant_loop, 
 		$instances/$conflict_quant, $instances,
		$forall/$conflict_quant, $select/$conflict_quant, $subt/$conflict_quant, 
		$ss/$conflict_quant);
  print "$sat\t$time\t";
  for($i=0;$i<@res;++$i) {
    $tot[$i] += $res[$i];
    $tot_tm[$i] += $res[$i] * $time;
    printf ("%9.2f", $res[$i]);
  }
  print "\n";
  $n++;
  $n_time += $time;
 
}
 
}

print "zCNT\t$n\t";
  for($i=0;$i<@tot;++$i) {
    printf ("%9.2f", $tot[$i]/$n);
  }
printf ("\nzTIME\t%.2f\t", $n_time);
  for($i=0;$i<@tot;++$i) {
    printf ("%9.2f", $tot_tm[$i]/$n_time);
  }
print "\n";