% EXPECT: sat

a0, a1, a2, a3, a4, a5: BOOLEAN;

ASSERT ((a0 AND a1 AND a2) <=> (a3 OR a4 OR a5));
ASSERT (a0);
ASSERT (a1);
ASSERT (a2);
ASSERT (NOT a3);
ASSERT (NOT a5);

CHECKSAT;