I spent some time this morning sorting through the Lash flags. Here's my classification of them. These flags are *not* used in Lash: ONTOLOGY_DEFS_TRANSLUCENT TRANSLUCENT_EXPAND_DELAY USE_MODELS MAX_INTERPS_PER_AXIOM DELAY_SEMANTIC_EQUIV_INSTANTIATION DELAY_TRUE_IN_MODELS DELAY_FALSE_IN_MODELS DELAY_UNINFORMATIVE_IN_MODELS ENABLE_PATTERN_CLAUSES PATTERN_CLAUSES_EARLY APPLY_PATTERN_CLAUSES_EARLY DYNAMIC_PATTERN_CLAUSES PATTERN_CLAUSES_TRANSITIVITY_EQ PATTERN_CLAUSES_FORALL_AS_LIT PATTERN_CLAUSES_ONLYALLSTRICT PATTERN_CLAUSES_EQNLITS NONFORALL_PATTERN_CLAUSES_USABLE PATTERN_CLAUSES_DELAY PATTERN_CLAUSES_EQN_DELAY HOUNIF1 HOUNIF1MATE HOUNIF1MATEBELOWEQUIV HOUNIF1MATENONLITS HOUNIF1NEGFLEX HOUNIF1MAXMATES HOUNIF1BOUND HOUNIF1PROJECT HOUNIF1IMITATE BASETYPESTOPROP BASETYPESFINITE USE_E USE_EHOH E_EQO_EQUIV E_AUTOSCHEDULE E_PERIOD E_TIMEOUT These flags are used, but not in the search: PFTRM_ADD_SYM_CLAUSES PFTRM_PRESORT_CLAUSES PFTRM_REMOVE_INDEPENDENT I suspect the SINE flags are not used, but values are determined by the schedule instead: USE_SINE SINE_GENERALITY_THRESHOLD SINE_TOLERANCE SINE_RANK_LIMIT These flags *are* used in Lash and likely affect the search: Bool flags (values true or false, obviously): SPLIT_GLOBAL_DISJUNCTIONS SPLIT_GLOBAL_DISJUNCTIONS_IMP SPLIT_GLOBAL_DISJUNCTIONS_EQO FILTER_UNIV_USABLE FILTER_UNIV FILTER_POSATM_USABLE FILTER_POSATM FILTER_NEGATM_USABLE FILTER_NEGATM FILTER_POSEQ_USABLE FILTER_POSEQ FILTER_NEGEQ_USABLE FILTER_NEGEQ SYM_EQ INSTANTIATE_WITH_FUNC_DISEQN_SIDES IMITATE_DEFNS CHOICE ENUM_ITER_DEEP LEIBEQ_TO_PRIMEQ CHOICE_AS_DEFAULT INITIAL_SUBTERMS_AS_INSTANTIATIONS INITIAL_SUBTERMS_AS_INSTANTIATIONS_O PREPROCESS_BEFORE_SPLIT TREAT_CONJECTURE_AS_SPECIAL ALL_DEFS_AS_EQNS EAGERLY_PROCESS_INSTANTIATIONS EXISTSTOCHOICE Int flags (nonnegative values; usually candidate values are 0,1,2,3,8,16, etc.): SPLIT_GLOBAL_DISJUNCTIONS_LIMIT FILTER_START FILTER_INCR EXISTS_DELAY FORALL_DELAY DEFAULTELT_DELAY DEFAULTELTINST_DELAY CONFR_DIFF_DELAY CONFR_SAME1_DELAY CONFR_SAME2_DELAY ENUM_START (candidate values: 0, 100, 10000, etc.) ENUM_ARROW ENUM_O ENUM_SORT ENUM_MASK (probably a byte: 0-255) ENUM_NEG ENUM_IMP ENUM_FALSE ENUM_CHOICE ENUM_FORALL ENUM_EQ ENUM_ITER_DEEP_DELAY ENUM_ITER_DEEP_INIT ENUM_ITER_DEEP_INCR IMITATE_DEFN_DELAY IMITATE_DELAY PROJECT_DELAY NEW_HEAD_ENUM_DELAY CHOICE_EMPTY_DELAY CHOICE_IN_DELAY POST_OR_L_DELAY POST_OR_R_DELAY POST_NOR_L_DELAY POST_NOR_R_DELAY POST_EQO_L_DELAY POST_EQO_R_DELAY POST_EQO_NL_DELAY POST_EQO_NR_DELAY POST_NEQO_L_DELAY POST_NEQO_R_DELAY POST_NEQO_NL_DELAY POST_NEQO_NR_DELAY POST_DEC_DELAY PRE_MATING_DELAY_POS PRE_MATING_DELAY_NEG PRE_CHOICE_MATING_DELAY_POS PRE_CHOICE_MATING_DELAY_NEG POST_MATING_DELAY POST_FEQ_DELAY POST_NFEQ_DELAY POST_CONFRONT1_DELAY POST_CONFRONT2_DELAY POST_CONFRONT3_DELAY POST_CONFRONT4_DELAY PRIORITY_QUEUE_IMPL AXIOM_DELAY RELEVANCE_DELAY INSTANTIATION_DELAY ARTP_WEIGHT BASETP_WEIGHT OTP_WEIGHT AP_WEIGHT LAM_WEIGHT LAM_TP_WEIGHT_FAC NAME_WEIGHT NAME_TP_WEIGHT_FAC DB_WEIGHT DB_TP_WEIGHT_FAC FALSE_WEIGHT IMP_WEIGHT FORALL_WEIGHT FORALL_TP_WEIGHT_FAC EQ_WEIGHT EQ_TP_WEIGHT_FAC CHOICE_WEIGHT CHOICE_TP_WEIGHT_FAC NOT_IN_PROP_MODEL_DELAY BASETYPESMAXSIZE MINISAT_SEARCH_PERIOD MINISAT_SEARCH_PERIOD_FACTOR MINISAT_SEARCH_DELAY (big values like 1000000 delay calling minisat indefinitely) INSTANTIATION_ORDER_CYCLE (probably nonzero; candidate values 1,2,4,8) INSTANTIATION_ORDER_MASK (probably a byte: 0-255) DELAY_FO DELAY_FO_CLAUSE DELAY_FO_LIT