Add FaCT++ config for testing purposes

fact.conf

+[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
+