#!/usr/bin/perl5

$mace = "mace2-binary";    # MACE binary
$unsatisfiable_exit = 12;  # MACE exit code of interest
$input = "/tmp/mace$$";	   # temporary input file

while ($equation = <STDIN>) {

    # Build a file containing the equation and the denial of commutativity.

    open(FH, ">$input") || die "Cannot open file $input";
    print FH "list(usable). $equation f(0,1)!=f(1,0). end_of_list.\n";
    close(FH);

    # Run MACE, discarding stdout and stderr, and capturing exit code.

    $rc = system("$mace -N4 < $input > /dev/null 2> /dev/null");
    $rc = $rc / 256;	# This gets the actual exit code.

    # Print the equation if it has no noncommutative models <= 4.

    if ($rc == $unsatisfiable_exit) { print $equation; }
}

system("/bin/rm $input");