#!/usr/bin/perl

@lines = ();
while(<>) {
  push @lines, $_;
}

$opts = "'-t:20'";
$err = "'assertion.* failed'";
#$err = "TIMEOUT";
#$err = "SAT=False";

$max_jump = 80;
$min_jump = 4;
$jump = ($max_jump + $min_jump) / 2;

$iter = 0;

sub skip {
  $cnt = shift;
  $iter++;

  open(F,">tmp");
  foreach (@need) {
    print F $_;
  }
  for($j=$i+$cnt;$j<@lines;++$j) {
    print F $lines[$j];
  }
  close(F);
  $x = $cur; chomp $x;
  print "test:$iter, [$cnt] $x -> ";
  $res = system("./run tmp $opts >log 2>&1; grep -qi $err log");
  if ($res == 0) {
    print "don't need\n";
    return 1;
  } else {
    print "need\n";
    return 0;
  }
}

@need = ();
for ($i=0; $i < @lines; ++$i) {
  $k = @lines;
  print "$i / $k: ";
  $cur = $lines[$i];

  if (skip($jump)) {
    $i += $jump - 1;
    $jump += $jump / 2;
  } else {
    $jump -= $jump / 3;
    if (skip(1)) {}
    else {
      push  @need, $cur;
    }
  }

  $jump = $max_jump if ($jump > $max_jump);
  $jump = $min_jump if ($jump < $min_jump);
}

open(F,">out");
foreach (@need) {
  print F $_;
}