[LeveLogger]

;--- Logging file name
 file = reasoning.log
;--- Logging level (the less level you give, the less information will be logged)
 allowedLevel = 0


[Tuning]

;---
;--- Option 'IAOEFLG': text ---
;---
;* Option 'IAOEFLG' define the priorities of different operations in TODO list. Possible values are 7-digit strings with ony possible digit are 0-6. The digits on the places 1, 2, ..., 7 are for priority of Id, And, Or, Exists, Forall, LE and GE operations respectively. The smaller number means the higher priority. All other constructions (TOP, BOTTOM, etc) has priority 0.
;* Default value: '1263005'

; IAOEFLG = 1263005

;---
;--- Option 'absorptionFlags': text ---
;---
;* Option 'absorptionFlags' sets up absorption process for general axioms. It text field of arbitrary length; every symbol means the absorption action: (B)ottom Absorption), (T)op absorption, (E)quivalent concepts replacement, (C)oncept absorption, (N)egated concept absorption, (F)orall expression replacement, Simple (f)orall expression replacement, (R)ole absorption, (S)plit
;* Default value: 'BTEfCFSR'

; absorptionFlags = BTEfCFSR

;---
;--- Option 'allowUndefinedNames': boolean ---
;---
;* Option 'allowUndefinedNames' describes the policy of undefined names.
;* Default value: 'true'

; allowUndefinedNames = 1

;---
;--- Option 'alwaysPreferEquals': boolean ---
;---
;* Option 'alwaysPreferEquals' allows user to enforce usage of C=D definition instead of C[=D during absorption, even if implication appeares earlier in stream of axioms.
;* Default value: 'true'

; alwaysPreferEquals = 1

;---
;--- Option 'checkAD': boolean ---
;---
;* Option 'checkAD' forces FaCT++ to create the AD and exit instead of performing classification
;* Default value: 'false'

; checkAD = 0

;---
;--- Option 'dumpOntology': boolean ---
;---
;* Option 'dumpOntology' dumps the ontology loaded into the reasoner in a LISP-like format
;* Default value: 'false'

; dumpOntology = 0

;---
;--- Option 'dumpQuery': boolean ---
;---
;* Option 'dumpQuery' dumps sub-TBox relevant to given satisfiability/subsumption query.
;* Default value: 'false'

; dumpQuery = 0

;---
;--- Option 'orSortSat': text ---
;---
;* Option 'orSortSat' define the sorting order of OR vertices in the DAG used in satisfiability tests (used mostly in caching). Option has form of string 'Mop', see orSortSub for details.
;* Default value: '0'

; orSortSat = 0

;---
;--- Option 'orSortSub': text ---
;---
;* Option 'orSortSub' define the sorting order of OR vertices in the DAG used in subsumption tests. Option has form of string 'Mop', where 'M' is a sort field (could be 'D' for depth, 'S' for size, 'F' for frequency, and '0' for no sorting), 'o' is a order field (could be 'a' for ascending and 'd' for descending mode), and 'p' is a preference field (could be 'p' for preferencing non-generating rules and 'n' for not doing so).
;* Default value: '0'

; orSortSub = 0

;---
;--- Option 'queryAnswering': boolean ---
;---
;* Option 'queryAnswering', if true, switches the reasoner to a query answering mode.
;* Default value: 'false'

; queryAnswering = 0

;---
;--- Option 'skipBeforeBlock': integer ---
;---
;* Internal use only. Option 'skipBeforeBlock' allow user to skip given number of nodes before make a block.
;* Default value: '0'

; skipBeforeBlock = 0

;---
;--- Option 'testTimeout': integer ---
;---
;* Option 'testTimeout' sets timeout for a single reasoning test in milliseconds.
;* Default value: '0'

; testTimeout = 0

;---
;--- Option 'useAnywhereBlocking': boolean ---
;---
;* Option 'useAnywhereBlocking' allow user to choose between Anywhere and Ancestor blocking.
;* Default value: 'true'

; useAnywhereBlocking = 1

;---
;--- Option 'useBackjumping': boolean ---
;---
;* Option 'useBackjumping' switch backjumping on and off. The usage of backjumping usually leads to much faster reasoning.
;* Default value: 'true'

; useBackjumping = 1

;---
;--- Option 'useCompletelyDefined': boolean ---
;---
;* Option 'useCompletelyDefined' leads to simpler Taxonomy creation if TBox contains no non-primitive concepts. Unfortunately, it is quite rare case.
;* Default value: 'true'

; useCompletelyDefined = 1

;---
;--- Option 'useIncrementalReasoning': boolean ---
;---
;* Option 'useIncrementalReasoning' (development) allows one to reason efficiently about small changes in the ontology.
;* Default value: 'false'

; useIncrementalReasoning = 0

;---
;--- Option 'useLazyBlocking': boolean ---
;---
;* Option 'useLazyBlocking' makes checking of blocking status as small as possible. This greatly increase speed of reasoning.
;* Default value: 'true'

; useLazyBlocking = 1

;---
;--- Option 'useSemanticBranching': boolean ---
;---
;* Option 'useSemanticBranching' switch semantic branching on and off. The usage of semantic branching usually leads to faster reasoning, but sometime could give small overhead.
;* Default value: 'true'

; useSemanticBranching = 1

;---
;--- Option 'useSpecialDomains': boolean ---
;---
;* Option 'useSpecialDomains' (development) controls the special processing of R&D for non-simple roles. Should always be set to true.
;* Default value: 'true'

; useSpecialDomains = 1