#include <civlc.cvh>

$input double A,B,C,E,F,G,H,I;

$assume (0 == H*A - G*B);
$assume (0 != I*A - G*C);
$assume (0 != E && 0 != G && 0 != A);
$assume (0 == E*I*A - E*G*C - F*H*A	+ F*G*B);

int main() {
  $assert(0, "unreachable");
}