...a...Existential instantiation says, "For any sentence with variable x, constant symbol does not appear elsewhere in the knowledge base, we can replace x with constant symbol a".
My question is
1. why "a" should not appear in the knowledge base?
2. What if we don't have any more symbol available, so we cannot pick up new symbol for existential quantifier?