while (<>) {
/(\d+) -> (\d+), \d+: \[(.*)\]$/ or die;
$n = $1;
$down = $2;
@lines = split /, +/, $3;

next if ($n - $down <= 2);

for (1 .. 20) {
  for(1 ..  @lines) {
    $x = int(rand(@l));
    $y = int(rand(@l));
    ($lines[$x], $lines[$y]) = ($lines[$y], $lines[$x]);
  }
  open (Q, ">tmp");
  print Q "(and\n";
  foreach (@lines) { print Q "$_\n"; }
  print Q ")\n";
  open(Q, "./run -n -no-multi-refutation -v tmp 2>&1 |");
  while (<Q>) {
    /theory conflict clause, (\d+)/ and $size = $1;
  }
  if ($size > $down + 2) {
    system ("cat tmp");
  } else {
    print "oops, got $size, max $n, min $down\n";
  }
}

}