[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 is 5-letters text field; 1st symbol -- 'n' or 'c' -- (doN't) use Concept absorption; 2nd symbol -- 'n', 'r' or 'e' -- (doN't) use (Extended) Role absorption; the rest is symbols C,R,S; their order setup order of Simplification, Concept and Role absorptions performed (if possible).
;* Default value: 'ceSCR'

; absorptionFlags = ceSCR

;---
;--- 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 'useRangeDomain': boolean ---
;---
;* Option 'useRangeDomain' switch on and off native support for the range and domain. This option is of internal use only. It is crusial for reasoning performance to leave this option true.
;* Default value: 'true'

; useRangeDomain = 1

;---
;--- 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 = *TOP*
; Target2 = *BOTTOM*

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

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