; Jan 15 2013 - Increased the timeout for E to 30s EXISTSTOCHOICE false HOUNIF1 true HOUNIF1MATE true HOUNIF1MATEBELOWEQUIV true HOUNIF1MAXMATES 1 HOUNIF1BOUND 16 TREAT_CONJECTURE_AS_SPECIAL true PRIORITY_QUEUE_IMPL 1 AXIOM_DELAY 1 RELEVANCE_DELAY 5 SPLIT_GLOBAL_DISJUNCTIONS true ENABLE_PATTERN_CLAUSES true PATTERN_CLAUSES_DELAY 0 EXISTS_DELAY 0 FORALL_DELAY 1 DEFAULTELT_DELAY 1000 DEFAULTELTINST_DELAY 1000 CONFR_DIFF_DELAY 1000 CONFR_SAME1_DELAY 1000 CONFR_SAME2_DELAY 1000 ENUM_START 30 ENUM_ARROW 10 ENUM_O 5 ENUM_SORT 0 ENUM_NEG 5 ENUM_IMP 20 ENUM_FALSE 20 ENUM_CHOICE 10 ENUM_EQ 0 IMITATE_DEFNS false IMITATE_DELAY 6 LEIBEQ_TO_PRIMEQ true IMITATE_DEFN_DELAY 1000 IMITATE_DELAY 1000 PROJECT_DELAY 1000 NEW_HEAD_ENUM_DELAY 1000 CHOICE_EMPTY_DELAY 1000 CHOICE_IN_DELAY 1000 POST_EQO_L_DELAY 1000 POST_EQO_R_DELAY 1000 POST_EQO_NL_DELAY 1000 POST_EQO_NR_DELAY 1000 POST_NEQO_L_DELAY 1000 POST_NEQO_R_DELAY 1000 POST_NEQO_NL_DELAY 1000 POST_NEQO_NR_DELAY 1000 POST_DEC_DELAY 1000 POST_MATING_DELAY 1000 POST_FEQ_DELAY 1000 POST_NFEQ_DELAY 1000 POST_CONFRONT1_DELAY 1000 POST_CONFRONT2_DELAY 1000 POST_CONFRONT3_DELAY 1000 POST_CONFRONT4_DELAY 1000 USE_E true E_PERIOD 100 E_TIMEOUT 30