[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, (R)ole absorption, (S)plit
;* Default value: 'BTECFSR'

; absorptionFlags = BTECFSR

;---
;--- 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 '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 '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 '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 'usePrecompletion': boolean ---
;---
;* Option 'usePrecompletion' switchs on and off precompletion process for ABox.
;* Default value: 'false'

; usePrecompletion = 0

;---
;--- Option 'useRelevantOnly': boolean ---
;---
;* Option 'useRelevantOnly' is used when creating internal DAG representation for externally given TBox. If true, DAG contains only concepts, relevant to query. It is safe to leave this option false.
;* Default value: 'false'

; useRelevantOnly = 0

;---
;--- 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

[Query]

;--
;-- targets for single satisfiability (is Target sat) or subsumption (if Target [= Target2 holds) test
;--

Target = SAT
; Target2 = *BOTTOM*

;***
;*** please do not change lines below
;***

;--
;-- target KB
;--
TBox = fact.tbox

