(id : Type)

( i : id )
( a : id )
( b : id )
( c : id )
( d : id )
( e : id )

( not_eq_i_a : ?? (Not (i = a)) )
( not_eq_i_b : ?? (Not (i = b)) )
( not_eq_i_c : ?? (Not (i = c)) )
( not_eq_i_d : ?? (Not (i = d)) )
( not_eq_i_e : ?? (Not (i = e)) )
( not_eq_a_b : ?? (Not (a = b)) )
( not_eq_a_c : ?? (Not (a = c)) )
( not_eq_a_d : ?? (Not (a = d)) )
( not_eq_a_e : ?? (Not (a = e)) )
( not_eq_a_i : ?? (Not (a = i)) )
( not_eq_b_a : ?? (Not (b = a)) )
( not_eq_b_c : ?? (Not (b = c)) )
( not_eq_b_d : ?? (Not (b = d)) )
( not_eq_b_e : ?? (Not (b = e)) )
( not_eq_b_i : ?? (Not (b = i)) )
( not_eq_c_a : ?? (Not (c = a)) )
( not_eq_c_b : ?? (Not (c = b)) )
( not_eq_c_d : ?? (Not (c = d)) )
( not_eq_c_e : ?? (Not (c = e)) )
( not_eq_c_i : ?? (Not (c = i)) )
( not_eq_d_a : ?? (Not (d = a)) )
( not_eq_d_b : ?? (Not (d = b)) )
( not_eq_d_c : ?? (Not (d = c)) )
( not_eq_d_e : ?? (Not (d = e)) )
( not_eq_d_i : ?? (Not (d = i)) )
( not_eq_e_a : ?? (Not (e = a)) )
( not_eq_e_b : ?? (Not (e = b)) )
( not_eq_e_c : ?? (Not (e = c)) )
( not_eq_e_d : ?? (Not (e = d)) )
( not_eq_e_i : ?? (Not (e = i)) )

( done )