% COMMAND-LINE: --jh-rlv-order
% EXPECT: unsat

% note we require jh-rlv-order on this benchmark to avoid a proof failure currently (7/7/21)

OPTION "logic" "ALL";
BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)];
x : SET OF BvPair;
y : SET OF BvPair;

a : BvPair;
b : BvPair;
c : BvPair;
d : BvPair;
e : BvPair;

ASSERT DISTINCT ( a, b );
ASSERT DISTINCT ( c, d, e );

ASSERT a IS_IN x;
ASSERT b IS_IN x;
ASSERT a IS_IN y;
ASSERT b IS_IN y;
ASSERT (NOT ( c IS_IN (x JOIN y)) AND NOT ( d IS_IN (x JOIN y)) AND NOT ( e IS_IN (x JOIN y)) );

CHECKSAT;