#!/usr/bin/perl -w

$mace4 = "../bin/mace4";

if (! -x $mace4) { die "binary $mace4 not found"; }

$unsatisfiable_exit = 2;
$input = "/tmp/mace$$";

while ($equation = <STDIN>) {
    open(FH, ">$input") || die "Cannot open file $input";
    print FH "clauses(theory). $equation f(0,1)!=f(1,0). end_of_list.\n";
    close(FH);
    $rc = system("$mace4 -N4 < $input > /dev/null 2> /dev/null");
    $rc = $rc / 256;	# This gets the actual exit code.
    if ($rc == $unsatisfiable_exit) { print $equation; }
}
system("/bin/rm $input");