The prover automatically loads the declarations of certain logical operators and axioms governing these operators. Most of these are derived from axioms of EFT. They can be examined by starting the prover and looking at the axioms that are present before any theory is loaded.