4 # Copyright (c) 2009, 2010, 2011 The CVC4 Project
8 my ($nvars, $nclauses);
12 if(/^p cnf (\d+) (\d+)/) {
13 ($nvars, $nclauses) = ($1, $2);
14 print "(benchmark b\n";
15 print ":status unknown\n";
16 print ":logic QF_UF\n";
17 for(my $i = 1; $i <= $nvars; ++$i) {
18 print ":extrapreds ((x$i))\n";
20 print ":formula (and\n";
27 for(my $i = 0; $i < $#_; ++$i) {
29 print " (not x" . -$_[$i] . ")";