vampire.txt

************************************************************
*************************  Global  *************************
************************************************************

--cores
	When running in portfolio modes (including casc or smtcomp modes) specify 
	the number of cores, set to 0 to use maximum
	default: 1
--instruction_limit (-i)
	Limit the number (in millions) of executed instructions (excluding the 
	kernel ones).
	default: 0
--memory_limit (-m)
	Memory limit in MB
	default: 1024
--mode
	Select the mode of operation. Choices are:
	  -vampire: the standard mode of operation for first-order theorem proving
	  -portfolio: a portfolio mode running a specified schedule (see schedule)
	  -casc, casc_sat, smtcomp - like portfolio mode, with competition specific
	     presets for schedule, etc.
	  -preprocess,axiom_selection,clausify: modes for producing output
	      for other solvers.
	  -tpreprocess,tclausify: output modes for theory input (clauses are quantified
	      with sort information).
	  -output,profile: output information about the problem
	Some modes are not currently maintained (get in touch if interested):
	  -bpa: perform bound propagation
	  -consequence_elimination: perform consequence elimination
	  -random_strategy: attempts to randomize the option values
	
	default: vampire
	values: axiom_selection,casc,casc_hol,casc_sat,casc_ltb,clausify,consequence_elimination,
	        model_check,output,portfolio,preprocess,preprocess2,profile,
	        random_strategy,smtcomp,spider,tclausify,tpreprocess,vampire
--randomize_seed_for_portfolio_workers
	In portfolio mode, let each worker process start from its own independent 
	random seed.
	default: on
--schedule (-sched)
	Schedule to be run by the portfolio mode. casc and smtcomp usually point 
	to the most recent schedule in that category. file loads the schedule from 
	a file specified in --schedule_file. Note that some old schedules may contain 
	option values that are no longer supported - see ignore_missing.
	default: casc
	values: casc,casc_2019,casc_sat,casc_sat_2019,casc_hol_2020,file,induction,
	        integer_induction,ltb_default_2017,ltb_hh4_2017,ltb_hll_2017,
	        ltb_isa_2017,ltb_mzr_2017,smtcomp,smtcomp_2018,snake_tptp_uns,
	        snake_tptp_sat,struct_induction
--schedule_file
	Path to the input schedule file. Each line contains an encoded strategy. 
	Disabled unless `--schedule file` is set.
	default: <empty>
--slowness
	The factor by which is multiplied the time limit of each configuration 
	in casc/casc_sat/smtcomp/portfolio mode
	default: 1
--superposition (-sup)
	Control superposition. Turning off this core inference leads to an incomplete 
	calculus on equational problems.
	default: on
--time_limit (-t)
	Time limit in wall clock seconds, you can use d,s,m,h,D suffixes also i.e. 
	60s, 5m. Setting it to 0 effectively gives no time limit.
	default: 600d

************************************************************
**********************  Higher-order  **********************
************************************************************

--add_comb_axioms (-aca)
	Add combinator axioms
	default: off
--add_proxy_axioms (-apa)
	Add logical proxy axioms
	default: off
--bool_eq_trick (-bet)
	Replace an equality between boolean terms such as: t = s with a disequality 
	t != vnot(s) The theory is that this can help with EqRes
	default: off
--cases (-c)
	Alternative to FOOL Paramodulation that replaces all Boolean subterms in 
	one step
	default: off
--cases_simp (-cs)
	FOOL Paramodulation with two conclusion as a simplification
	default: off
--choice_ax (-cha)
	Adds the cnf form of the Hilbert choice axiom
	default: off
--choice_reasoning (-chr)
	Reason about choice by adding relevant instances of the axiom
	default: off
--cnf_on_the_fly (-cnfonf)
	Various options linked to clausification on the fly
	default: eager
	values: eager,lazy_gen,lazy_simp,lazy_not_gen,lazy_not_gen_be_off,
	        lazy_not_be_gen,off
--combinatory_sup (-csup)
	Switches on a specific ordering and that orients combinator axioms left-right. 
	Also turns on a number of special inference rules
	default: off
--complex_bool_reasoning (-cbe)
	Switches on primitive instantiation and elimination of Leibniz equality
	default: on
--complex_var_cond (-cvc)
	Use the more complex variable condition provided in the SKIKBO paper.
	More terms are comparable with this ordering, but it has worst caseexponential 
	complexity
	default: off
--equality_to_equiv (-e2e)
	Equality between boolean terms changed to equivalence 
	t1 : $o = t2 : $o is changed to t1 <=> t2
	default: off
--func_ext (-fe)
	Deal with extensionality using abstraction, axiom or neither
	default: abstraction
	values: off,axiom,abstraction
--injectivity (-inj)
	Attempts to identify injective functions and postulates a left-inverse
	default: off
--lam_free_hol (-lfh)
	Reason about lambda-free hol. See paper by Vukmirovic et al.
	default: off
--max_XX_narrows (-mXXn)
	Maximum number of BXX', CXX' and SXX' narrows thatcan be carried out 0 
	means that there is no limit. 
	default: 0
--narrow (-narr)
	Controls the set of combinator equations to use in narrowing
	default: all
	values: all,sk,ski,off
--new_taut_del (-ntd)
	Delete clauses with literals of the form false != true or t = true \/ t 
	= false
	default: off
--pragmatic (-prag)
	Modifies various parameters to help Vampire solve 'hard' higher-order
	default: off
--prim_inst_set (-piset)
	Controls the set of equations to use in primitive instantiation
	default: all_but_not_eq
	values: all,all_but_not_eq,false_true_not,small_set
--priority_to_long_reducts (-ptlr)
	give priority to clauses produced by lengthy reductions
	default: off

************************************************************
**************************  Help  **************************
************************************************************

--bad_option
	What should be done if a bad option value (wrt hard and soft constraints) 
	is encountered:
	 - hard: will cause a user error
	 - soft: will only report the error (unless it is unsafe)
	 - forced: <under development> 
	 - off: will ignore safe errors
	Note that unsafe errors will always lead to a user error
	default: soft
	values: hard,forced,off,soft
--explain_option (-explain)
	Use to explain a single option i.e. -explain explain
	default: <empty>
--help (-h)
	Display the help message
	default: off
--show_options
	List all available options
	default: off

*************************************************************
**************************  Input  **************************
*************************************************************

--forbidden_options
	If some of the specified options are set to a forbidden state, vampire 
	will fail to start, or in portfolio modes it will skip such strategies. 
	The expected syntax is <opt1>=<val1>:<opt2>:<val2>:...:<optn>=<valN>
	default: <empty>
--forced_options
	Options in the format <opt1>=<val1>:<opt2>=<val2>:...:<optn>=<valN> that 
	override the option values set by other means (also inside portfolio mode 
	strategies)
	default: <empty>
--guess_the_goal (-gtg)
	Use heuristics to guess formulas that correspond to the goal. Doesn't really 
	make sense if there is already a goal but it will still do something. This 
	is really designed for use with SMTLIB problems that don't have goals
	default: off
	values: off,all,exists_top,exists_all,exists_sym,position
--guess_the_goal_limit (-gtgl)
	The maximum number of input units a symbol appears for it to be considered 
	in a goal
	default: 1
--include
	Path prefix for the 'include' TPTP directive
	default: <empty>
--input_syntax
	Input syntax. Historic input syntaxes have been removed as they are not 
	actively maintained. Contact developers for help with these.
	default: auto
	values: smtlib2,tptp,auto
--random_seed
	Some parts of vampire use random numbers. This seed allows for reproducibility 
	of results. By default the seed is not changed.
	default: 1
--random_strategy_seed
	Sets the seed for generating random strategies. This option necessary because 
	--random_seed <value> will be included as fixed value in the generated 
	random strategy, hence won't have any effect on the random strategy generation. 
	The default value is derived from the current time.
	default: 1683429016

*************************************************************
**********************  Preprocessing  **********************
*************************************************************

--blocked_clause_elimination (-bce)
	Eliminate blocked clauses after clausification.
	default: off
--definition_reuse (-dr)
	Reuse definition symbols in a similar fashion to Skolem reuse.
	default: off
--equality_proxy (-ep)
	Applies the equality proxy transformation to the problem. It works as follows:
	 - All literals s=t are replaced by E(s,t)
	 - All literals s!=t are replaced by ~E(s,t)
	 - If S the symmetry clause ~E(x,y) \/ E(y,x) is added
	 - If T the transitivity clause ~E(x,y) \/ ~E(y,z) \/ E(x,z) is added
	 - If C the congruence clauses are added as follows:
	    for predicates p that are not E or equality add
	     ~E(x1,y1) \/ ... \/ ~E(xN,yN) \/ ~p(x1,...,xN) \/ p(y1,...,yN)
	    for non-constant functions f add
	     ~E(x1,y1) \/ ... \/ ~E(xN,yN) \/ E(f(x1,...,xN),f(y1,...,yN))
	 R stands for reflexivity
	default: off
	values: R,RS,RST,RSTC,off
--equality_resolution_with_deletion (-erd)
	Perform equality resolution with deletion.
	default: on
--function_definition_elimination (-fde)
	Attempts to eliminate function definitions. A function definition is a 
	unit clause of the form f(x1,..,xn) = t where x1,..,xn are the pairwise 
	distinct free variables of t and f does not appear in t. If 'all', definitions 
	are eliminated by replacing every occurrence of f(s1,..,sn) by t{x1 -> 
	s1, .., xn -> sn}. If 'unused' only unused definitions are removed.
	default: all
	values: all,none,unused
--general_splitting (-gsp)
	Splits clauses in order to reduce number of different variables in each 
	clause. A clause C[X] \/ D[Y] with subclauses C and D over non-equal sets 
	of variables X and Y can be split into S(Z) \/ C[X] and ~S(Z) \/ D[Y] where 
	Z is the intersection of X and Y.
	default: off
--ignore_conjecture_in_preprocessing (-icip)
	Make sure we do not delete the conjecture in preprocessing even if it can 
	be deleted.
	default: off
--inequality_splitting (-ins)
	When greater than zero, ins defines a weight threshold w such that any 
	clause C \/ s!=t where s (or conversely t) is ground and has weight greater 
	or equal than w is replaced by C \/ p(s) with the additional unit clause 
	~p(t) being added for fresh predicate p.
	default: 0
--inline_let (-ile)
	Always inline let-expressions.
	default: off
--mono_ep (-mep)
	Use the monomorphic version of equality proxy transformation.
	default: on
--naming (-nm)
	Introduce names for subformulas. Given a subformula F(x1,..,xk) of formula 
	G a new predicate symbol is introduced as a name for F(x1,..,xk) by adding 
	the axiom n(x1,..,xk) <=> F(x1,..,xk) and replacing F(x1,..,xk) with n(x1,..,xk) 
	in G. The value indicates how many times a subformula must be used before 
	it is named.
	default: 8
--newcnf (-newcnf)
	Use NewCNF algorithm to do naming, preprocessing and clausification.
	default: off
--normalize (-norm)
	Normalize the problem so that the ordering of clauses etc does not effect 
	proof search.
	default: off
--random_polarities (-rp)
	As part of preprocessing, randomly (though consistently) flip polarities 
	of non-equality predicates in the whole CNF.
	default: off
--shuffle_input (-si)
	Randomly shuffle the input problem. (Runs after and thus destroys normalize.)
	default: off
--sine_depth (-sd)
	Limit number of iterations of the transitive closure algorithm that selects 
	formulas based on SInE's D-relation (see SInE description). 0 means no 
	limit, 1 is a maximal limit (least selected axioms), 2 allows two iterations, 
	etc...
	default: 0
--sine_generality_threshold (-sgt)
	Generality of a symbol is the number of input formulas in which a symbol 
	appears. If the generality of a symbol is smaller than the threshold, it 
	is always added into the D-relation with formulas in which it appears.
	default: 0
--sine_selection (-ss)
	If 'axioms', all formulas that are not annotated as 'axiom' (i.e. conjectures 
	and hypotheses) are initially selected, and the SInE selection is performed 
	on those annotated as 'axiom'. If 'included', all formulas that are directly 
	in the problem file are initially selected, and the SInE selection is performed 
	on formulas from included files. The 'included' value corresponds to the 
	behaviour of the original SInE implementation.
	default: off
	values: axioms,included,off
--sine_tolerance (-st)
	SInE tolerance parameter (sometimes referred to as 'benevolence')
	default: 1
--skolem_reuse (-skr)
	Attempt to reuse Skolem symbols.
	Symbols are re-used if they represent identical formulae up to renaming.
	default: off
--sos (-sos)
	Set of support strategy. All formulas annotated as axioms are put directly 
	among active clauses, without performing any inferences between them. If 
	all, select all literals of set-of-support clauses, otherwise use the default 
	literal selector. If theory then only apply to theory axioms introduced 
	by vampire (all literals are selected).
	default: off
	values: all,off,on,theory
--sos_theory_limit (-sstl)
	When sos=theory, limit the depth of descendants a theory axiom can have.
	default: 0
--theory_axioms (-tha)
	Include theory axioms for detected interpreted symbols
	default: on
	values: on,off,some
--theory_flattening (-thf)
	Flatten clauses to separate theory and non-theory parts in the input. This 
	is often quickly undone in proof search.
	default: off
--unused_predicate_definition_removal (-updr)
	Attempt to remove predicate definitions. A predicate definition is a formula 
	of the form ![X1,..,Xn] : (p(X1,..,XN) <=> F) where p is not equality and 
	does not occur in F and X1,..,XN are the free variables of F. If p has 
	only positive (negative) occurrences then <=> in the definition can be 
	replaced by => (<=). If p does not occur in the rest of the problem the 
	definition can be removed.
	default: on

************************************************************
***********************  Saturation  ***********************
************************************************************

--activation_limit (-al)
	Terminate saturation after this many iterations of the main loop. 0 means 
	no limit.
	default: 0
--age_weight_ratio (-awr)
	Ratio in which clauses are being selected for activation i.e. a:w means 
	that for every a clauses selected based on age there will be w selected 
	based on weight.
	default left: 1
	default right: 1
--age_weight_ratio_shape (-awrs)
	How to change the age/weight ratio during proof search.
	default: constant
	values: constant,decay,converge
--age_weight_ratio_shape_frequency (-awrsf)
	How frequently the age/weight ratio shape is to change: i.e. if set to 
	'decay' at a frequency of 100, the age/weight ratio will change every 100 
	age/weight choices.
	default: 100
--increased_numeral_weight (-inw)
	This option only applies if the problem has interpreted numbers. The weight 
	of integer constants depends on the logarithm of their absolute value (instead 
	of being 1)
	default: off
--introduced_symbol_precedence (-isp)
	Decides where to place symbols introduced during proof search in the symbol 
	precedence
	default: top
	values: top,bottom
--literal_comparison_mode (-lcm)
	Vampire uses term orderings which use an ordering of predicates. Standard 
	places equality (and certain other special predicates) first and all others 
	second. Predicate depends on symbol precedence (see symbol_precedence). 
	Reverse reverses the order.
	default: standard
	values: predicate,reverse,standard
--literal_maximality_aftercheck (-lma)
	For efficiency we perform maximality checks before applying substitutions. 
	Sometimes this can lead to generating more clauses than needed for completeness. 
	Set this on to add the checks afterwards as well.
	default: off
--lookahaed_delay (-lsd)
	Delay the use of lookahead selection by this many selections the idea is 
	that lookahead selection may behave erratically at the start
	default: 0
--lrs_estimate_correction_coef (-lecc)
	Make lrs more (<1.0) or less (>1.0) agressive by multiplying by this coef 
	its estimate of how many clauses are still reachable.
	default: 1
--nongoal_weight_coefficient (-nwc)
	coefficient that will multiply the weight of theory clauses (those marked 
	as 'axiom' in TPTP)
	default: 1
--positive_literal_split_queue (-plsq)
	Turn on experiments: clause selection with multiple queues containing different 
	clauses (split by number of positive literals in clause)
	default: off
--positive_literal_split_queue_cutoffs (-plsqc)
	The cutoff-values for the positive-literal-split-queues (the cutoff value 
	for the last queue is omitted, since it has to be infinity).
	default: 0
--positive_literal_split_queue_layered_arrangement (-plsql)
	If turned on, use a layered arrangement to split clauses into queues. Otherwise 
	use a tammet-style-arrangement.
	default: off
--positive_literal_split_queue_ratios (-plsqr)
	The ratios for picking clauses from the positive-literal-split-queues using 
	weighted round robin. If a queue is empty, the clause will be picked from 
	the next non-empty queue to the right. Note that this option implicitly 
	also sets the number of queues.
	default: 1,4
--restrict_nwc_to_goal_constants (-rnwc)
	restrict nongoal_weight_coefficient to those containing goal constants
	default: off
--saturation_algorithm (-sa)
	Select the saturation algorithm:
	 - discount:
	 - otter:
	 - limited resource:
	 - instance generation: a simple implementation of instantiation calculus
	    (global_subsumption, unit_resulting_resolution and age_weight_ratio)
	 - fmb : finite model building for satisfiable problems.
	 - z3 : pass the preprocessed problem to z3, will terminate if the resulting 
	problem is not ground.
	inst_gen, z3 and fmb aren't influenced by options for the saturation algorithm, 
	apart from those under the relevant heading
	default: lrs
	values: discount,fmb,inst_gen,lrs,otter
--selection (-s)
	Selection methods 2,3,4,10,11 are complete by virtue of extending Maximal 
	i.e. they select the best among maximal. Methods 1002,1003,1004,1010,1011 
	relax this restriction and are therefore not complete.
	 0     - Total (select everything)
	 1     - Maximal
	 2     - ColoredFirst, MaximalSize then Lexicographical
	 3     - ColoredFirst, NoPositiveEquality, LeastTopLevelVariables,
	          LeastDistinctVariables then Lexicographical
	 4     - ColoredFirst, NoPositiveEquality, LeastTopLevelVariables,
	          LeastVariables, MaximalSize then Lexicographical
	 10    - ColoredFirst, NegativeEquality, MaximalSize, Negative then Lexicographical
	 11    - Lookahead
	 666   - Random
	 1002  - Incomplete version of 2
	 1003  - Incomplete version of 3
	 1004  - Incomplete version of 4
	 1010  - Incomplete version of 10
	 1011  - Incomplete version of 11
	 1666  - Incomplete version of 666
	Or negated, which means that reversePolarity is true i.e. for selection 
	we treat all negative non-equality literals as positive and vice versa 
	(can only apply to non-equality literals).
	
	default: 10
--sine_level_split_queue (-slsq)
	Turn on experiments: clause selection with multiple queues containing different 
	clauses (split by sine-level of clause)
	default: off
--sine_level_split_queue_cutoffs (-slsqc)
	The cutoff-values for the sine-level-split-queues (the cutoff value for 
	the last queue is omitted, since it has to be infinity).
	default: 0
--sine_level_split_queue_layered_arrangement (-slsql)
	If turned on, use a layered arrangement to split clauses into queues. Otherwise 
	use a tammet-style-arrangement.
	default: on
--sine_level_split_queue_ratios (-slsqr)
	The ratios for picking clauses from the sine-level-split-queues using weighted 
	round robin. If a queue is empty, the clause will be picked from the next 
	non-empty queue to the right. Note that this option implicitly also sets 
	the number of queues.
	default: 1,1
--sine_to_age (-s2a)
	Use SInE levels to postpone introducing clauses more distant from the conjecture 
	to proof search by artificially making them younger (age := sine_level).
	default: off
--sine_to_age_generality_threshold (-s2agt)
	Like sine_generality_threshold but influences sine_to_age, sine_to_pred_levels, 
	and sine_level_split_queue rather than sine_selection.
	default: 0
--sine_to_age_tolerance (-s2at)
	Like sine_tolerance but influences sine_to_age, sine_to_pred_levels, and 
	sine_level_split_queue rather than sine_selection.
	default: 1
--sine_to_pred_levels (-s2pl)
	Assign levels to predicate symbols as they are used to trigger axioms during 
	SInE computation. Then use them as predicateLevels determining the ordering. 
	'on' means conjecture symbols are larger, 'no' means the opposite. (equality 
	keeps its standard lowest level).
	default: off
	values: no,off,on
--symbol_precedence (-sp)
	Vampire uses term orderings which require a precedence relation between 
	symbols.
	Arity orders symbols by their arity (and reverse_arity takes the reverse 
	of this) and occurence orders symbols by the order they appear in the problem. 
	Then we have a few precedence generating schemes adopted from E: frequency 
	- sort by frequency making rare symbols large, reverse does the opposite, 
	(For the weighted versions, each symbol occurence counts as many times 
	as is the length of the clause in which it occurs.) unary_first is like 
	arity, except that unary symbols are maximal (and ties are broken by frequency), 
	unary_frequency is like frequency, except that unary symbols are maximal, 
	const_max makes constants the largest, then falls back to arity, const_min 
	makes constants the smallest, then falls back to reverse_arity, const_frequency 
	makes constants the smallest, then falls back to frequency.
	default: arity
	values: arity,occurrence,reverse_arity,unary_first,const_max,const_min,scramble,
	        frequency,unary_frequency,const_frequency,reverse_frequency,
	        weighted_frequency,reverse_weighted_frequency
--symbol_precedence_boost (-spb)
	Boost the symbol precedence of symbols occurring in certain kinds of clauses 
	in the input.
	Additionally, non_intro/intro suppress/boost the precedence of symbols 
	introduced during preprocessing (i.e., mainly, the naming predicates and 
	the skolems).
	default: none
	values: none,goal,units,goal_then_units,non_intro,intro
--term_ordering (-to)
	The term ordering used by Vampire to orient equations and order literals
	default: kbo
	values: kbo,lpo
--theory_split_queue (-thsq)
	Turn on clause selection using multiple queues containing different clauses 
	(split by amount of theory reasoning)
	default: off
--theory_split_queue_cutoffs (-thsqc)
	The cutoff-values for the split-queues (the cutoff value for the last queue 
	has to be omitted, as it is always infinity). Any split-queue contains 
	all clauses which are assigned a feature-value less or equal to the cutoff-value 
	of the queue. If no custom value for this option is set, the implementation 
	will use cutoffs 0,4*d,10*d,infinity (where d denotes the theory split 
	queue expected ratio denominator).
	default: 0
--theory_split_queue_expected_ratio_denom (-thsqd)
	The denominator n such that we expect the final proof to have a ratio of 
	theory-axioms to all-axioms of 1/n.
	default: 8
--theory_split_queue_layered_arrangement (-thsql)
	If turned on, use a layered arrangement to split clauses into queues. Otherwise 
	use a tammet-style-arrangement.
	default: on
--theory_split_queue_ratios (-thsqr)
	The ratios for picking clauses from the split-queues using weighted round 
	robin. If a queue is empty, the clause will be picked from the next non-empty 
	queue to the right. Note that this option implicitly also sets the number 
	of queues.
	default: 1,1

************************************************************
**********************  LRS Specific  **********************
************************************************************

--lrs_first_time_check
	Percentage of time limit at which the LRS algorithm will for the first 
	time estimate the number of reachable clauses.
	default: 5
--lrs_weight_limit_only (-lwlo)
	If off, the lrs sets both age and weight limit according to clause reachability, 
	otherwise it sets the age limit to 0 and only the weight limit reflects 
	reachable clauses
	default: off
--simulated_time_limit (-stl)
	Time limit in seconds for the purpose of reachability estimations of the 
	LRS saturation algorithm (if 0, the actual time limit is used)
	default: 0d

************************************************************
***********************  Inferences  ***********************
************************************************************

--arithmetic_subterm_generalizations (-asg)
	          Enables various generalization rules for arithmetic terms as 
	described in the paper Making Theory Reasoning Simpler ( https://easychair.org/publications/preprint/K2hb 
	).           In some rare cases the conclusion may be not strictly simpler 
	than the hypothesis. With `force` we ignore these cases, violating the 
	ordering and just simplifying           anyways. With `cautious` we will 
	generate a new clause instead of simplifying in these cases.
	default: off
	values: force,cautious,off
--backward_demodulation (-bd)
	Oriented rewriting of kept clauses by newly derived unit equalities
	s = t     L[sθ] \/ C
	---------------------   where sθ > tθ (replaces RHS)
	 L[tθ] \/ C
	
	default: all
	values: all,off,preordered
--backward_subsumption (-bs)
	Perform subsumption deletion of kept clauses by newly derived clauses. 
	Unit_only means that the subsumption will be performed only by unit clauses
	default: off
	values: off,on,unit_only
--backward_subsumption_demodulation (-bsd)
	Perform backward subsumption demodulation.
	default: off
--backward_subsumption_demodulation_max_matches (-bsdmm)
	Maximum number of multi-literal matches to consider in backward subsumption 
	demodulation. 0 means to try all matches (until first success).
	default: 0
--backward_subsumption_resolution (-bsr)
	Perform subsumption resolution on kept clauses using newly derived clauses. 
	Unit_only means that the subsumption resolution will be performed only 
	by unit clauses
	default: off
	values: off,on,unit_only
--binary_resolution (-br)
	Standard binary resolution i.e.
	C \/ t     D \/ s
	---------------------
	(C \/ D)θ
	where θ = mgu(t,-s) and t selected
	default: on
--cancellation (-canc)
	Enables the rule cancellation around additions as described in the paper 
	Making Theory Reasoning Simpler ( https://easychair.org/publications/preprint/K2hb 
	).                                 In some rare cases the conclusion may 
	be not strictly simpler than the hypothesis. With `force` we ignore these 
	cases, violating the ordering and just simplifying                     
	            anyways. With `cautious` we will generate a new clause instead 
	of simplifying in these cases.
	default: off
	values: force,cautious,off
--condensation (-cond)
	Perform condensation. If 'fast' is specified, we only perform condensations 
	that are easy to check for.
	default: off
	values: fast,off,on
--demodulation_redundancy_check (-drc)
	The following cases of backward and forward demodulation do not preserve 
	completeness:
	s = t     s = t1 \/ C 	 s = t     s != t1 \/ C
	--------------------- 	 ---------------------
	t = t1 \/ C 		 t != t1 \/ C
	where t > t1 and s = t > C (RHS replaced)
	With `on`, we check this condition and don't demodulate if we could violate 
	completeness.
	With `encompass`, we treat demodulations (both forward and backward) as 
	encompassment demodulations (as defined by Duarte and Korovin in 2022's 
	IJCAR paper).
	With `off`, we skip the checks, save time, but become incomplete.
	default: on
	values: off,encompass,on
--equational_tautology_removal (-etr)
	A reduction which uses congruence closure to remove logically valid clauses.
	default: off
--extensionality_allow_pos_eq
	If extensionality resolution equals filter, this dictates whether we allow 
	other positive equalities when recognising extensionality clauses
	default: off
--extensionality_max_length
	Sets the maximum length (number of literals) an extensionality clause can 
	have when doing recognition for extensionality resolution. If zero there 
	is no maximum.
	default: 0
--extensionality_resolution (-er)
	Turns on the following inference rule:
	  x=y \/ C    s != t \/ D
	  -----------------------
	  C{x → s, y → t} \/ D
	Where s!=t is selected in s!=t \/D and x=y \/ C is a recognised as an extensionality 
	clause - how clauses are recognised depends on the value of this option.
	If filter we attempt to recognise all extensionality clauses i.e. those 
	that have exactly one X=Y, no inequality of the same sort as X-Y (and optionally 
	no equality except X=Y, see extensionality_allow_pos_eq).
	If known we only recognise a known set of extensionality clauses. At the 
	moment this includes the standard and subset-based formulations of the 
	set extensionality axiom, as well as the array extensionality axiom.
	If tagged we only use formulas tagged as extensionality clauses.
	default: off
	values: filter,known,tagged,off
--fool_paramodulation (-foolp)
	Turns on the following inference rule:
	        C[s]
	--------------------,
	C[true] \/ s = false
	where s is a boolean term that is not a variable, true or false, C[true] 
	is the C clause with s substituted by true. This rule is needed for efficient 
	treatment of boolean terms.
	default: off
--forward_demodulation (-fd)
	Oriented rewriting of newly derived clauses by kept unit equalities
	s = t     L[sθ] \/ C
	---------------------  where sθ > tθ
	 L[tθ] \/ C
	If 'preordered' is set, only equalities s = t where s > t are used for 
	rewriting.
	default: all
	values: all,off,preordered
--forward_literal_rewriting (-flr)
	Perform forward literal rewriting.
	default: off
--forward_subsumption (-fs)
	Perform forward subsumption deletion.
	default: on
--forward_subsumption_demodulation (-fsd)
	Perform forward subsumption demodulation.
	default: off
--forward_subsumption_demodulation_max_matches (-fsdmm)
	Maximum number of multi-literal matches to consider in forward subsumption 
	demodulation. 0 means to try all matches (until first success).
	default: 0
--forward_subsumption_resolution (-fsr)
	Perform forward subsumption resolution.
	default: on
--gaussian_variable_elimination (-gve)
	Enable the immediate simplification "Gaussian Variable Elimination":
	
	s != t \/ C[X] 
	--------------  if s != t can be rewritten to X != r 
	    C[r] 
	
	Example:
	
	6 * X0 != 2 * X1 | p(X0, X1)
	-------------------------------
	  p(2 * X1 / 6, X1)
	
	
	For a more detailed description see the paper Making Theory Reasoning Simpler 
	( https://easychair.org/publications/preprint/K2hb ).           In some 
	rare cases the conclusion may be not strictly simpler than the hypothesis. 
	With `force` we ignore these cases, violating the ordering and just simplifying 
	          anyways. With `cautious` we will generate a new clause instead 
	of simplifying in these cases.
	default: off
	values: force,cautious,off
--global_subsumption (-gs)
	Perform global subsumption. Use a set of groundings of generated clauses 
	G to replace C \/ L by C if the grounding of C is implied by G. A SAT solver 
	is used for ground reasoning.
	default: off
--global_subsumption_avatar_assumptions (-gsaa)
	When running global subsumption and AVATAR at the same time we need to 
	include information about the current AVATAR model. When this is off we 
	ignore clauses with AVATAR assumptions for GS. When it is from_current 
	we assume the assumptions in the current clause. When it is full_model 
	we assume the full model from AVATAR. See paper Global Subsumption Revisited 
	(Briefly).
	default: off
	values: off,from_current,full_model
--global_subsumption_explicit_minim (-gsem)
	no description provided!
	default: randomized
	values: off,on,randomized
--global_subsumption_sat_solver_power (-gsssp)
	Explicitly minimize the result of global subsumption reduction.
	default: propagation_only
	values: propagation_only,full
--high_school (-hsm)
	Enables high school education for vampire. (i.e.: sets -gve cautious, -asg 
	cautious, -ev cautious, -canc cautious, -pum on )
	default: off
--hyper_superposition
	Simplifying inference that attempts to do several rewritings at once if 
	it will eliminate literals of the original clause (now we aim just for 
	elimination by equality resolution)
	default: off
--induction (-ind)
	Apply structural and/or integer induction on datatypes and integers.
	default: none
	values: none,struct,int,both
--induction_choice (-indc)
	Where to apply induction. Goal only applies to constants in goal, goal_plus 
	extends this with skolem constants introduced by induction. Consider using 
	guess_the_goal for problems in SMTLIB as they do not come with a conjecture
	default: all
	values: all,goal,goal_plus
--induction_gen (-indgen)
	Apply induction with generalization (on both all & selected occurrences)
	default: off
--induction_max_depth (-indmd)
	Set maximum depth of induction where 0 means no max.
	default: 0
--induction_neg_only (-indn)
	Only apply induction to negative literals
	default: on
--induction_on_complex_terms (-indoct)
	Apply induction on complex (ground) terms vs. only on constants
	default: off
--induction_strengthen_hypothesis (-indstrhyp)
	Strengthen induction formulas with the remaining skolem constants replaced 
	with universally quantified variables in hypotheses
	default: off
--induction_unit_only (-indu)
	Only apply induction to unit clauses
	default: on
--inner_rewriting (-irw)
	C[t_1] | t1 != t2 ==> C[t_2] | t1 != t2 when t1>t2
	default: off
--instantiation (-inst)
	Heuristically instantiate variables. Often wastes a lot of effort. Consider 
	using thi instead.
	default: off
	values: off,on
--int_induction_default_bound (-intinddb)
	Always apply integer induction with bound 0
	default: off
--int_induction_interval (-intindint)
	Whether integer induction is applied over infinite or finite intervals, 
	or both
	default: both
	values: infinite,finite,both
--int_induction_kind (-iik)
	The kind of integer induction applied
	default: one
	values: one,two,all
--int_induction_strictness_comp (-intindstcomp)
	Exclude induction term t/literal l combinations from integer induction.
	Induction is not applied to _comparison_ literals l:
	  - none: no exclusion
	  - toplevel_not_in_other: t is a top-level argument of l,
	    but it does not occur in the other argument of l
	  - only_one_occurrence: t has only one occurrence in l
	  - not_in_both: t does not occur in both arguments of l
	  - always: induction on l is not allowed at all
	
	default: toplevel_not_in_other
	values: none,toplevel_not_in_other,only_one_occurrence,not_in_both,always
--int_induction_strictness_eq (-intindsteq)
	Exclude induction term t/literal l combinations from integer induction.
	Induction is not applied to _equality_ literals l:
	  - none: no exclusion
	  - toplevel_not_in_other: t is a top-level argument of l,
	    but it does not occur in the other argument of l
	  - only_one_occurrence: t has only one occurrence in l
	  - not_in_both: t does not occur in both arguments of l
	  - always: induction on l is not allowed at all
	
	default: none
	values: none,toplevel_not_in_other,only_one_occurrence,not_in_both,always
--int_induction_strictness_term (-intindstterm)
	Exclude induction term t/literal l combinations from integer induction.
	Induction is not applied to the induction term t:
	  - none: no exclusion
	  - interpreted_constant: t is an interpreted constant
	  - no_skolems: t does not contain a skolem function
	default: interpreted_constant
	values: none,interpreted_constant,no_skolems
--max_induction_gen_subset_size (-indgenss)
	Set maximum number of occurrences of the induction term to be generalized, 
	where 0 means no max. (Regular induction will be applied without this restriction.)
	default: 3
--non_unit_induction (-nui)
	Induction on certain clauses or clause sets instead of just unit clauses
	default: off
--normalize_inequalities (-norm_ineq)
	Enable normalizing of inequalities like s < t ==> 0 < t - s.
	default: off
--push_unary_minus (-pum)
	Enable the immediate simplifications:
	 -(t + s) ==> -t + -s
	 -(-t) ==> t
	
	default: off
--simultaneous_superposition (-sims)
	Rewrite the whole RHS clause during superposition, not just the target 
	literal.
	default: on
--structural_induction_kind (-sik)
	The kind of structural induction applied
	default: one
	values: one,two,three,all
--superposition_from_variables (-sfv)
	Perform superposition from variables.
	default: on
--term_algebra_acyclicity (-tac)
	Activates the cyclicity rule for term algebras (such as algebraic datatypes 
	in SMT-LIB):
	- off : the cyclicity rule is not enforced (this is sound but incomplete)
	- axiom : the cyclicity rule is axiomatized with a transitive predicate 
	describing the subterm relation over terms
	- rule : the cyclicity rule is enforced by a specific hyper-resolution 
	rule
	- light : the cyclicity rule is enforced by rule generating disequality 
	between a term and its known subterms
	default: off
	values: off,axiom,rule,light
--term_algebra_rules (-tar)
	Activates some rules that improve reasoning with term algebras (such as 
	algebraic datatypes in SMT-LIB):
	If the problem does not contain any term algebra symbols, activating this 
	options has no effect
	- distinctness rule:
	f(...) = g(...) \/ A
	--------------------
	          A         
	where f and g are distinct term algebra constructors
	- distinctness tautology deletion: clauses of the form f(...) ~= g(...) 
	\/ A are deleted
	- injectivity rule:
	f(s1 ... sn) = f(t1 ... tn) \/ A
	--------------------------------
	         s1 = t1 \/ A
	               ...
	         sn = tn \/ A
	default: on
--unification_with_abstraction (-uwa)
	During unification, if two terms s and t fail to unify we will introduce 
	a constraint s!=t and carry on. For example, resolving p(1) \/ C with ~p(a+2) 
	would produce C \/ 1 !=a+2. This is controlled by a check on the terms. 
	The expected use case is in theory reasoning. The possible values are:- 
	off: do not introduce a constraint
	- interpreted_only: only if s and t have interpreted top symbols
	- one_side_interpreted: only if one of s or t have interpreted top symbols
	- one_side_constant: only if one of s or t is an interpreted constant (e.g. 
	a number)
	- all: always apply
	- ground: only if both s and t are ground
	See Unification with Abstraction and Theory Instantiation in Saturation-Based 
	Reasoning for further details.
	default: off
	values: off,interpreted_only,one_side_interpreted,one_side_constant,all,
	        ground
--unit_resulting_resolution (-urr)
	Uses unit resulting resolution only to derive empty clauses (may be useful 
	for splitting)
	default: off
	values: ec_only,off,on
--use_ac_eval (-uace)
	Evaluate associative and commutative operators e.g. + and *.
	default: on

************************************************************
*************************  AVATAR  *************************
************************************************************

--avatar (-av)
	Use AVATAR splitting.
	default: on
--avatar_add_complementary (-aac)
	no description provided!
	default: ground
	values: ground,none
--avatar_buffered_solver (-abs)
	Added buffering functionality to the SAT solver used in AVATAR.
	default: off
--avatar_congruence_closure (-acc)
	Use a congruence closure decision procedure on top of the AVATAR SAT solver. 
	This ensures that models produced by AVATAR satisfy the theory of uninterpreted 
	functions.
	default: off
	values: model,off,on
--avatar_delete_deactivated (-add)
	no description provided!
	default: on
	values: on,large,off
--avatar_eager_removal (-aer)
	If a component was in the model and then becomes 'don't care' eagerly remove 
	that component from the first-order solver. Note: only has any impact when 
	amm is used.
	default: on
--avatar_fast_restart (-afr)
	no description provided!
	default: off
--avatar_flush_period (-afp)
	after given number of generated clauses without deriving an empty clause, 
	the splitting component selection is shuffled. If equal to zero, shuffling 
	is never performed.
	default: 0
--avatar_flush_quotient (-afq)
	after each flush, the avatar_flush_period is multiplied by the quotient
	default: 1.5
--avatar_literal_polarity_advice (-alpa)
	Override SAT-solver's default polarity/phase setting for variables abstracting 
	clause components.
	default: none
	values: false,true,none,random
--avatar_minimize_model (-amm)
	Minimize the SAT-solver model by replacing concrete values with don't-cares 
	provided <all> the sat clauses (or only the split clauses with <sco>) remain 
	provably satisfied by the partial model.
	default: all
	values: off,sco,all
--avatar_nonsplittable_components (-anc)
	Decide what to do with a nonsplittable component:
	  -known: SAT clauses will be learnt from non-splittable clauses that have 
	corresponding components (if there is a component C with name SAT l, clause 
	C | {l1,..ln} will give SAT clause ~l1 \/ … \/ ~ln \/ l). When we add 
	the sat clause, we discard the original FO clause C | {l1,..ln} and let 
	the component selection update model, possibly adding the component clause 
	C | {l}.
	  -all: like known, except when we see a non-splittable clause that doesn't 
	have a name, we introduce the name for it.
	  -all_dependent: like all, but we don't introduce names for non-splittable 
	clauses that don't depend on any components
	default: known
	values: all,all_dependent,known,none
--avatar_split_queue (-avsq)
	Turn on experiments: clause selection with multiple queues containing different 
	clauses (split by amount of avatar-split-set-size)
	default: off
--avatar_split_queue_cutoffs (-avsqc)
	The cutoff-values for the avatar-split-queues (the cutoff value for the 
	last queue is omitted, since it has to be infinity).
	default: 0
--avatar_split_queue_layered_arrangement (-avsql)
	If turned on, use a layered arrangement to split clauses into queues. Otherwise 
	use a tammet-style-arrangement.
	default: off
--avatar_split_queue_ratios (-avsqr)
	The ratios for picking clauses from the split-queues using weighted round 
	robin. If a queue is empty, the clause will be picked from the next non-empty 
	queue to the right. Note that this option implicitly also sets the number 
	of queues.
	default: 1,1
--avatar_turn_off_time_frac (-atotf)
	Stop splitting after the specified fraction of the overall time has passed 
	(the default 1.0 means AVATAR runs until the end).
	(the remaining time AVATAR is still switching branches and communicating 
	with the SAT solver,
	but not introducing new splits anymore. This fights the theoretical possibility 
	of AVATAR's dynamic incompleteness.)
	default: 1
--cc_unsat_cores (-ccuc)
	no description provided!
	default: all
	values: first,small_ones,all
--nonliterals_in_clause_weight (-nicw)
	Non-literal parts of clauses (such as its split history) will also contribute 
	to the weight
	default: off
--split_at_activation (-sac)
	Split a clause when it is activated, default is to split when it is processed
	default: off

*************************************************************
***********************  SAT Solving  ***********************
*************************************************************

--sat_solver (-sas)
	Select the SAT solver to be used throughout the solver. This will be used 
	in AVATAR (for splitting) when the saturation algorithm is discount,lrs 
	or otter and in instance generation for selection and global subsumption.
	default: minisat
	values: minisat

*************************************************************
******************  Finite Model Building  ******************
*************************************************************

--fmb_adjust_sorts (-fmbas)
	Detect monotonic sorts. If <expand> then expand monotonic subsorts into 
	proper sorts. If <group> then collapse monotonic sorts into a single sort. 
	If <predicate> then introduce sort predicates for non-monotonic sorts and 
	collapse all sorts into one. If <function> then introduce sort functions 
	for non-monotonic sorts and collapse all sorts into one
	default: group
	values: off,expand,group,predicate,function
--fmb_detect_sort_bounds (-fmbdsb)
	Use a saturation loop to detect sort bounds introduced by (for example) 
	injective functions
	default: off
--fmb_detect_sort_bounds_time_limit (-fmbdsbt)
	The time limit (in seconds) for performing sort bound detection
	default: 1
--fmb_enumeration_strategy (-fmbes)
	How model sizes assignments are enumerated in the multi-sorted setting. 
	(Only smt and contour are known to be finite model complete and can therefore 
	return UNSAT.)
	default: sbeam
	values: sbeam,contour
--fmb_keep_sbeam_generators (-fmbksg)
	A modification of the sbeam enumeration strategy which (for a performance 
	price) makes it more enumeration-complete.
	default: off
--fmb_size_weight_ratio (-fmbswr)
	Controls the priority the next sort size vector is given based on a ratio. 
	0 is size only, 1 means 1:1, 2 means 1:2, etc.
	default: 1
--fmb_start_size (-fmbss)
	Set the initial model size for finite model building
	default: 1
--fmb_symmetry_ratio (-fmbsr)
	Usually we use at most n principal terms for symmetry avoidance where n 
	is the current model size. This option allows us to supply a multiplier 
	for that n. See Symmetry Avoidance in MACE-Style Finite Model Finding.
	default: 1
--fmb_symmetry_symbol_order (-fmbsso)
	The order of symbols considered for symmetry avoidance. See Symmetry Avoidance 
	in MACE-Style Finite Model Finding.
	default: occurence
	values: occurence,input_usage,preprocessed_usage

*************************************************************
*******************  Instance Generation  *******************
*************************************************************

--inst_gen_big_restart_ratio (-igbrr)
	Determines how often a big restart (instance generation starts from input 
	clauses) will be performed. Small restart means all clauses generated so 
	far are processed again.
	default: 0
--inst_gen_passive_reactivation (-igpr)
	When the model describing the selection function changes some active clauses 
	may become lazily deselected. If passive reaction is selected these clauses 
	are added into the passive set before recomputing the next model, otherwise 
	they are added back to active.
	default: off
--inst_gen_resolution_ratio (-igrr)
	Ratio of resolution and instantiation steps (applies only if inst_gen_with_resolution 
	is on)
	default left: 1
	default right: 1
--inst_gen_restart_period (-igrp)
	How many clauses are processed before restart. The size of the restart 
	depends on inst_gen_big_restart_ratio.
	default: 1000
--inst_gen_restart_period_quotient (-igrpq)
	Restart period is multiplied by this number after each restart.
	default: 1
--inst_gen_selection (-igs)
	Selection function for InstGen. This is applied *after* model-based selection 
	is applied. For consistency the value 1011 is used to denote look-ahead 
	selection.
	default: 0
--inst_gen_with_resolution (-igwr)
	Performs instantiation together with resolution (global subsumption index 
	is shared, also clauses generated by the resolution are added to the instance 
	SAT problem)
	default: off

************************************************************
*************************  Output  *************************
************************************************************

--ignore_missing_inputs_in_unsat_core
	When running in unsat core output mode we will complain if there is an 
	input formula that has no label. Set this on if you don't want this behaviour 
	(which is default in smt-comp).
	default: off
--latex_output
	File that will contain proof in the LaTeX format.
	default: off
--latex_use_default_symbols
	Interpreted symbols such as product have default LaTeX symbols that can 
	be used. They can be overriden in the normal way. This option can turn 
	them off
	default: on
--minimize_sat_proofs
	Perform unsat core minimization when a sat solver finds a clause set UNSAT
	(such as with AVATAR proofs or with global subsumption).
	default: on
--output_axiom_names
	Preserve names of axioms from the problem file in the proof output
	default: off
--output_mode (-om)
	Change how Vampire prints the final result. SZS uses TPTP's SZS ontology. 
	smtcomp mode suppresses all output and just prints sat/unsat. vampire is 
	the same as SZS just without the SZS. Spider prints out some profile information 
	and extra error reports. ucore uses the smt-lib ucore output.
	default: szs
	values: smtcomp,spider,szs,vampire,ucore
--print_clausifier_premises
	Output how the clausified problem was derived.
	default: off
--print_proofs_to_file (-pptf)
	If Vampire finds a proof, it is printed to the here specified file instead 
	of to stdout.
	Currently, this option only works in portfolio mode.
	default: <empty>
--proof (-p)
	Specifies whether proof (or similar e.g. model/saturation) will be output 
	and in which format:
	- off gives no proof output
	- on gives native Vampire proof output
	- proofcheck will output proof as a sequence of TPTP problems to allow 
	for proof-checking by external solvers
	- tptp gives TPTP output
	- property is a developmental option. It allows developers to output statistics 
	about the proof using a ProofPrinter object (see Kernel/InferenceStore::ProofPropertyPrinter
	
	default: on
	values: off,on,proofcheck,tptp,property
--proof_extra
	Add extra detail to proofs:
	 - free uses known information only
	- full may perform expensive operations to achieve this so may significantly 
	impact on performance.
	 The option is still under development and the format of extra information 
	(mainly from full) may change between minor releases
	default: off
	values: off,free,full
--show_fmb_sort_info
	Print information about sorts in FMB
	default: off
--show_fool
	Reveal the internal representation of FOOL terms
	default: off
--show_induction
	Print information about induction
	default: off
--show_ordering
	Display the used simplification ordering's parameters.
	default: off
--statistics (-stat)
	The level of statistics to report at the end of the run.
	default: brief
	values: brief,full,none
--time_statistics (-tstat)
	Show how much running time was spent in each part of Vampire
	default: off

*************************************************************
***********************  Development  ***********************
*************************************************************

--arity_check
	Enforce the condition that the same symbol name cannot be used with multiple 
	arities.This also ensures a symbol is not used as a function and predicate.
	default: off
--decode
	Decodes an encoded strategy. Can be used to replay a strategy. To make 
	Vampire output an encoded version of the strategy use the encode option.
	default: 
--encode
	Output an encoding of the strategy to be used with the decode option
	default: off
--ignore_missing
	Ignore any options that have been removed (useful in portfolio modes where 
	this can cause strategies to be skipped). If set to warn this will print 
	a warning when ignoring. This is set to warn in CASC mode.
	default: off
	values: on,off,warn
--manual_cs
	Run Vampire interactively by manually picking the clauses to be selected
	default: off
--parsing_does_not_count
	Extend the instruction limit by the amount of instructions it took to parse 
	the input problem.
	default: off
--random_strategy
	Create a random strategy. Randomisation will occur after all other options 
	have been set, whatever order they have been given in. A random number 
	of options will be selected  and set with a safe (possibly default) value.
	default: off
	values: on,off,sat,nocheck
--show_active
	Print activated clauses.
	default: off
--show_blocked
	Show generating inferences blocked due to coloring of symbols
	default: off
--show_definitions
	Show definition introductions.
	default: off
--show_everything
	Turn (almost) all of the showX commands on
	default: off
--show_new
	Show new (generated) clauses
	default: off
--show_nonconstant_skolem_function_trace
	Show introduction of non-constant skolem functions.
	default: off
--show_passive
	Show clauses added to the passive set.
	default: off
--show_preprocessing
	Show preprocessing.
	default: off
--show_reductions
	Show reductions.
	default: off
--show_skolemisations
	Show Skolemisations.
	default: off
--show_splitting
	Show updates within AVATAR
	default: off
--show_symbol_elimination
	Show symbol elimination.
	default: off
--show_theory_axioms
	Show the added theory axioms.
	default: off

*************************************************************
**************************  Other  **************************
*************************************************************

--question_answering (-qa)
	Determines whether (and how) we attempt to answer questions
	default: off
	values: answer_literal,from_proof,off
--use_hashing_clause_variant_index (-uhcvi)
	Use clause variant index based on hashing for clause variant detection 
	(affects inst_gen and avatar).
	default: off