mereotopology hierarchy: added input and output of consistency proofs

gruninger · May 29, 2013 · c675566 · c675566
1 parent 0dd5b9f
commit c675566
Show file tree

Hide file tree

Showing 27 changed files with 8,121 additions and 0 deletions.
diff --git a/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_2.all.p9 b/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_2.all.p9
@@ -0,0 +1,52 @@
+%axioms from module mt//consistency/p9/rcc_basic_strict_nontrivial_2.p9
+%----------------------------------
+
+% Automatically generated from CL/KIF
+formulas(sos).
+% 'mt/consistency/rcc_basic_strict_nontrivial_2'
+%imports("mt/rcc_basic_strict").
+ exists x exists y (-((x = y))).
+
+
+%axioms from module mt/p9/rcc_basic_strict.p9
+%----------------------------------
+
+% Automatically generated from CL/KIF
+% 'mt/rcc_basic_strict'
+%imports("mt/rcc_basic").
+% 'Axioms of the Region Connection Calculus extended by C-extensionality'
+% 'RCC-Ext: Extensionality'
+ all x all y ((P(x, y) & P(y, x) -> (x = y))).
+
+
+%axioms from module mt/p9/rcc_basic.p9
+%----------------------------------
+
+% Automatically generated from CL/KIF
+% 'mt/rcc_basic'
+% 'Basic axioms of the Region Connection Calculus that allows finite models (RCC-4b and RCC8 removed)'
+% 'RCC-P: Parthood'
+ all x all y ((P(x, y) <->  all z ((C(z, x) -> C(z, y))))).
+% 'RCC-PP: Proper Parthood'
+ all x all y ((PP(x, y) <-> P(x, y) & -(P(y, x)))).
+% 'RCC-O: Overlap'
+ all x all y ((O(x, y) <->  exists z (P(z, x) & P(z, y)))).
+% 'RCC-EC: External connection'
+ all x all y ((EC(x, y) <-> C(x, y) & -(O(x, y)))).
+% 'RCC-NTPP: Non-tangential parthood'
+ all x all y ((NTPP(x, y) <-> PP(x, y) & -( exists z (EC(z, x) & EC(z, y))))).
+% 'RCCR1: Reflexivity'
+ all x (C(x, x)).
+% 'RCC2: Symmetry'
+ all x all y ((C(x, y) -> C(y, x))).
+% 'RCC3: Universal element'
+ all x (C(x, Uni)).
+% 'RCC4b'
+ all x all y ((-((y = Uni)) -> (O(x, compl(y)) <-> -(P(x, y))))).
+% 'RCC5: Sum'
+ all x all y all z ((C(x, sum(y, z)) <-> C(x, y) | C(x, z))).
+% 'RCC6, RCC7: Product'
+ all x all y all z ((O(y, z) -> (C(x, prod(y, z)) <->  exists w (P(w, y) & P(w, z) & C(x, w))))).
+
+end_of_list.
+
diff --git a/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_2.all.tptp b/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_2.all.tptp
@@ -0,0 +1,27 @@
+
+% The LADR formulas contain function or predicate symbols
+% that are not legal TPTP symbols, and we have replaced those
+% symbols with new symbols.  Here is the list of the unaccepted
+% symbols and the corresponding replacements.
+%
+%   (arity 2)        C    'C'
+%   (arity 2)        P    'P'
+%   (arity 2)        O    'O'
+%   (arity 0)      Uni    'Uni'
+%   (arity 2)       EC    'EC'
+%   (arity 2)       PP    'PP'
+%   (arity 2)     NTPP    'NTPP'
+
+fof(sos15,axiom,? [X0] : ? [X1] : ~ X0 = X1).
+fof(sos16,axiom,! [X2] : ! [X3] : (('P'(X2,X3) &'P'(X3,X2)) => X2 = X3)).
+fof(sos17,axiom,! [X4] : ! [X5] : ('P'(X4,X5) <=> ! [X6] : ('C'(X6,X4) =>'C'(X6,X5)))).
+fof(sos18,axiom,! [X7] : ! [X8] : ('PP'(X7,X8) <=> ('P'(X7,X8) & ~'P'(X8,X7)))).
+fof(sos19,axiom,! [X9] : ! [X10] : ('O'(X9,X10) <=> ? [X11] : ('P'(X11,X9) &'P'(X11,X10)))).
+fof(sos20,axiom,! [X12] : ! [X13] : ('EC'(X12,X13) <=> ('C'(X12,X13) & ~'O'(X12,X13)))).
+fof(sos21,axiom,! [X14] : ! [X15] : ('NTPP'(X14,X15) <=> ('PP'(X14,X15) & ~ (? [X16] : ('EC'(X16,X14) &'EC'(X16,X15)))))).
+fof(sos22,axiom,! [X17] :'C'(X17,X17)).
+fof(sos23,axiom,! [X18] : ! [X19] : ('C'(X18,X19) =>'C'(X19,X18))).
+fof(sos24,axiom,! [X20] :'C'(X20,'Uni')).
+fof(sos25,axiom,! [X21] : ! [X22] : (~ X22 ='Uni' => ('O'(X21,compl(X22)) <=> ~'P'(X21,X22)))).
+fof(sos26,axiom,! [X23] : ! [X24] : ! [X25] : ('C'(X23,sum(X24,X25)) <=> ('C'(X23,X24) |'C'(X23,X25)))).
+fof(sos27,axiom,! [X26] : ! [X27] : ! [X28] : ('O'(X27,X28) => ('C'(X26,prod(X27,X28)) <=> ? [X29] : ('P'(X29,X27) & ('P'(X29,X28) &'C'(X26,X29)))))).
diff --git a/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_2.p9 b/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_2.p9
@@ -0,0 +1,7 @@
+% Automatically generated from CL/KIF
+formulas(sos).
+% 'mt/consistency/rcc_basic_strict_nontrivial_2'
+%imports("mt/rcc_basic_strict").
+ exists x exists y (-((x = y))).
+
+end_of_list.
diff --git a/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_4.all.p9 b/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_4.all.p9
@@ -0,0 +1,52 @@
+%axioms from module mt//consistency/p9/rcc_basic_strict_nontrivial_4.p9
+%----------------------------------
+
+% Automatically generated from CL/KIF
+formulas(sos).
+% 'mt/consistency/rcc_basic_strict_nontrivial_4'
+%imports("mt/rcc_basic_strict").
+ exists x exists y exists z exists w (-((x = y)) & -((x = z)) & -((x = w)) & -((y = z)) & -((y = w)) & -((z = w))).
+
+
+%axioms from module mt/p9/rcc_basic_strict.p9
+%----------------------------------
+
+% Automatically generated from CL/KIF
+% 'mt/rcc_basic_strict'
+%imports("mt/rcc_basic").
+% 'Axioms of the Region Connection Calculus extended by C-extensionality'
+% 'RCC-Ext: Extensionality'
+ all x all y ((P(x, y) & P(y, x) -> (x = y))).
+
+
+%axioms from module mt/p9/rcc_basic.p9
+%----------------------------------
+
+% Automatically generated from CL/KIF
+% 'mt/rcc_basic'
+% 'Basic axioms of the Region Connection Calculus that allows finite models (RCC-4b and RCC8 removed)'
+% 'RCC-P: Parthood'
+ all x all y ((P(x, y) <->  all z ((C(z, x) -> C(z, y))))).
+% 'RCC-PP: Proper Parthood'
+ all x all y ((PP(x, y) <-> P(x, y) & -(P(y, x)))).
+% 'RCC-O: Overlap'
+ all x all y ((O(x, y) <->  exists z (P(z, x) & P(z, y)))).
+% 'RCC-EC: External connection'
+ all x all y ((EC(x, y) <-> C(x, y) & -(O(x, y)))).
+% 'RCC-NTPP: Non-tangential parthood'
+ all x all y ((NTPP(x, y) <-> PP(x, y) & -( exists z (EC(z, x) & EC(z, y))))).
+% 'RCCR1: Reflexivity'
+ all x (C(x, x)).
+% 'RCC2: Symmetry'
+ all x all y ((C(x, y) -> C(y, x))).
+% 'RCC3: Universal element'
+ all x (C(x, Uni)).
+% 'RCC4b'
+ all x all y ((-((y = Uni)) -> (O(x, compl(y)) <-> -(P(x, y))))).
+% 'RCC5: Sum'
+ all x all y all z ((C(x, sum(y, z)) <-> C(x, y) | C(x, z))).
+% 'RCC6, RCC7: Product'
+ all x all y all z ((O(y, z) -> (C(x, prod(y, z)) <->  exists w (P(w, y) & P(w, z) & C(x, w))))).
+
+end_of_list.
+
diff --git a/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_4.all.tptp b/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_4.all.tptp
@@ -0,0 +1,27 @@
+
+% The LADR formulas contain function or predicate symbols
+% that are not legal TPTP symbols, and we have replaced those
+% symbols with new symbols.  Here is the list of the unaccepted
+% symbols and the corresponding replacements.
+%
+%   (arity 2)        C    'C'
+%   (arity 2)        P    'P'
+%   (arity 2)        O    'O'
+%   (arity 0)      Uni    'Uni'
+%   (arity 2)       EC    'EC'
+%   (arity 2)       PP    'PP'
+%   (arity 2)     NTPP    'NTPP'
+
+fof(sos15,axiom,? [X0] : ? [X1] : ? [X2] : ? [X3] : (~ X0 = X1 & (~ X0 = X2 & (~ X0 = X3 & (~ X1 = X2 & (~ X1 = X3 & ~ X2 = X3)))))).
+fof(sos16,axiom,! [X4] : ! [X5] : (('P'(X4,X5) &'P'(X5,X4)) => X4 = X5)).
+fof(sos17,axiom,! [X6] : ! [X7] : ('P'(X6,X7) <=> ! [X8] : ('C'(X8,X6) =>'C'(X8,X7)))).
+fof(sos18,axiom,! [X9] : ! [X10] : ('PP'(X9,X10) <=> ('P'(X9,X10) & ~'P'(X10,X9)))).
+fof(sos19,axiom,! [X11] : ! [X12] : ('O'(X11,X12) <=> ? [X13] : ('P'(X13,X11) &'P'(X13,X12)))).
+fof(sos20,axiom,! [X14] : ! [X15] : ('EC'(X14,X15) <=> ('C'(X14,X15) & ~'O'(X14,X15)))).
+fof(sos21,axiom,! [X16] : ! [X17] : ('NTPP'(X16,X17) <=> ('PP'(X16,X17) & ~ (? [X18] : ('EC'(X18,X16) &'EC'(X18,X17)))))).
+fof(sos22,axiom,! [X19] :'C'(X19,X19)).
+fof(sos23,axiom,! [X20] : ! [X21] : ('C'(X20,X21) =>'C'(X21,X20))).
+fof(sos24,axiom,! [X22] :'C'(X22,'Uni')).
+fof(sos25,axiom,! [X23] : ! [X24] : (~ X24 ='Uni' => ('O'(X23,compl(X24)) <=> ~'P'(X23,X24)))).
+fof(sos26,axiom,! [X25] : ! [X26] : ! [X27] : ('C'(X25,sum(X26,X27)) <=> ('C'(X25,X26) |'C'(X25,X27)))).
+fof(sos27,axiom,! [X28] : ! [X29] : ! [X30] : ('O'(X29,X30) => ('C'(X28,prod(X29,X30)) <=> ? [X31] : ('P'(X31,X29) & ('P'(X31,X30) &'C'(X28,X31)))))).
diff --git a/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_4.p9 b/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_4.p9
@@ -0,0 +1,7 @@
+% Automatically generated from CL/KIF
+formulas(sos).
+% 'mt/consistency/rcc_basic_strict_nontrivial_4'
+%imports("mt/rcc_basic_strict").
+ exists x exists y exists z exists w (-((x = y)) & -((x = z)) & -((x = w)) & -((y = z)) & -((y = w)) & -((z = w))).
+
+end_of_list.
diff --git a/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_4atoms.all.p9 b/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_4atoms.all.p9
@@ -0,0 +1,52 @@
+%axioms from module mt//consistency/p9/rcc_basic_strict_nontrivial_4atoms.p9
+%----------------------------------
+
+% Automatically generated from CL/KIF
+formulas(sos).
+% 'mt/consistency/rcc_basic_strict_nontrivial_4atoms'
+%imports("mt/rcc_basic_strict").
+ exists x exists y exists z exists w (-(C(x, y)) & -(C(x, z)) & -(C(x, w)) & -(C(y, z)) & -(C(y, w)) & -(C(z, w))).
+
+
+%axioms from module mt/p9/rcc_basic_strict.p9
+%----------------------------------
+
+% Automatically generated from CL/KIF
+% 'mt/rcc_basic_strict'
+%imports("mt/rcc_basic").
+% 'Axioms of the Region Connection Calculus extended by C-extensionality'
+% 'RCC-Ext: Extensionality'
+ all x all y ((P(x, y) & P(y, x) -> (x = y))).
+
+
+%axioms from module mt/p9/rcc_basic.p9
+%----------------------------------
+
+% Automatically generated from CL/KIF
+% 'mt/rcc_basic'
+% 'Basic axioms of the Region Connection Calculus that allows finite models (RCC-4b and RCC8 removed)'
+% 'RCC-P: Parthood'
+ all x all y ((P(x, y) <->  all z ((C(z, x) -> C(z, y))))).
+% 'RCC-PP: Proper Parthood'
+ all x all y ((PP(x, y) <-> P(x, y) & -(P(y, x)))).
+% 'RCC-O: Overlap'
+ all x all y ((O(x, y) <->  exists z (P(z, x) & P(z, y)))).
+% 'RCC-EC: External connection'
+ all x all y ((EC(x, y) <-> C(x, y) & -(O(x, y)))).
+% 'RCC-NTPP: Non-tangential parthood'
+ all x all y ((NTPP(x, y) <-> PP(x, y) & -( exists z (EC(z, x) & EC(z, y))))).
+% 'RCCR1: Reflexivity'
+ all x (C(x, x)).
+% 'RCC2: Symmetry'
+ all x all y ((C(x, y) -> C(y, x))).
+% 'RCC3: Universal element'
+ all x (C(x, Uni)).
+% 'RCC4b'
+ all x all y ((-((y = Uni)) -> (O(x, compl(y)) <-> -(P(x, y))))).
+% 'RCC5: Sum'
+ all x all y all z ((C(x, sum(y, z)) <-> C(x, y) | C(x, z))).
+% 'RCC6, RCC7: Product'
+ all x all y all z ((O(y, z) -> (C(x, prod(y, z)) <->  exists w (P(w, y) & P(w, z) & C(x, w))))).
+
+end_of_list.
+
diff --git a/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_4atoms.all.tptp b/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_4atoms.all.tptp
@@ -0,0 +1,27 @@
+
+% The LADR formulas contain function or predicate symbols
+% that are not legal TPTP symbols, and we have replaced those
+% symbols with new symbols.  Here is the list of the unaccepted
+% symbols and the corresponding replacements.
+%
+%   (arity 2)        C    'C'
+%   (arity 2)        P    'P'
+%   (arity 2)        O    'O'
+%   (arity 0)      Uni    'Uni'
+%   (arity 2)       EC    'EC'
+%   (arity 2)       PP    'PP'
+%   (arity 2)     NTPP    'NTPP'
+
+fof(sos15,axiom,? [X0] : ? [X1] : ? [X2] : ? [X3] : (~'C'(X0,X1) & (~'C'(X0,X2) & (~'C'(X0,X3) & (~'C'(X1,X2) & (~'C'(X1,X3) & ~'C'(X2,X3))))))).
+fof(sos16,axiom,! [X4] : ! [X5] : (('P'(X4,X5) &'P'(X5,X4)) => X4 = X5)).
+fof(sos17,axiom,! [X6] : ! [X7] : ('P'(X6,X7) <=> ! [X8] : ('C'(X8,X6) =>'C'(X8,X7)))).
+fof(sos18,axiom,! [X9] : ! [X10] : ('PP'(X9,X10) <=> ('P'(X9,X10) & ~'P'(X10,X9)))).
+fof(sos19,axiom,! [X11] : ! [X12] : ('O'(X11,X12) <=> ? [X13] : ('P'(X13,X11) &'P'(X13,X12)))).
+fof(sos20,axiom,! [X14] : ! [X15] : ('EC'(X14,X15) <=> ('C'(X14,X15) & ~'O'(X14,X15)))).
+fof(sos21,axiom,! [X16] : ! [X17] : ('NTPP'(X16,X17) <=> ('PP'(X16,X17) & ~ (? [X18] : ('EC'(X18,X16) &'EC'(X18,X17)))))).
+fof(sos22,axiom,! [X19] :'C'(X19,X19)).
+fof(sos23,axiom,! [X20] : ! [X21] : ('C'(X20,X21) =>'C'(X21,X20))).
+fof(sos24,axiom,! [X22] :'C'(X22,'Uni')).
+fof(sos25,axiom,! [X23] : ! [X24] : (~ X24 ='Uni' => ('O'(X23,compl(X24)) <=> ~'P'(X23,X24)))).
+fof(sos26,axiom,! [X25] : ! [X26] : ! [X27] : ('C'(X25,sum(X26,X27)) <=> ('C'(X25,X26) |'C'(X25,X27)))).
+fof(sos27,axiom,! [X28] : ! [X29] : ! [X30] : ('O'(X29,X30) => ('C'(X28,prod(X29,X30)) <=> ? [X31] : ('P'(X31,X29) & ('P'(X31,X30) &'C'(X28,X31)))))).
diff --git a/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_4atoms.p9 b/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_4atoms.p9
@@ -0,0 +1,7 @@
+% Automatically generated from CL/KIF
+formulas(sos).
+% 'mt/consistency/rcc_basic_strict_nontrivial_4atoms'
+%imports("mt/rcc_basic_strict").
+ exists x exists y exists z exists w (-(C(x, y)) & -(C(x, z)) & -(C(x, w)) & -(C(y, z)) & -(C(y, w)) & -(C(z, w))).
+
+end_of_list.
diff --git a/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_5atoms.all.p9 b/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_5atoms.all.p9
@@ -0,0 +1,52 @@
+%axioms from module mt//consistency/p9/rcc_basic_strict_nontrivial_5atoms.p9
+%----------------------------------
+
+% Automatically generated from CL/KIF
+formulas(sos).
+% 'mt/consistency/rcc_basic_strict_nontrivial_5atoms'
+%imports("mt/rcc_basic_strict").
+ exists x exists y exists z exists w exists v (-(C(x, y)) & -(C(x, z)) & -(C(x, w)) & -(C(x, v)) & -(C(y, z)) & -(C(y, w)) & -(C(y, v)) & -(C(z, w)) & -(C(z, v)) & -(C(w, v))).
+
+
+%axioms from module mt/p9/rcc_basic_strict.p9
+%----------------------------------
+
+% Automatically generated from CL/KIF
+% 'mt/rcc_basic_strict'
+%imports("mt/rcc_basic").
+% 'Axioms of the Region Connection Calculus extended by C-extensionality'
+% 'RCC-Ext: Extensionality'
+ all x all y ((P(x, y) & P(y, x) -> (x = y))).
+
+
+%axioms from module mt/p9/rcc_basic.p9
+%----------------------------------
+
+% Automatically generated from CL/KIF
+% 'mt/rcc_basic'
+% 'Basic axioms of the Region Connection Calculus that allows finite models (RCC-4b and RCC8 removed)'
+% 'RCC-P: Parthood'
+ all x all y ((P(x, y) <->  all z ((C(z, x) -> C(z, y))))).
+% 'RCC-PP: Proper Parthood'
+ all x all y ((PP(x, y) <-> P(x, y) & -(P(y, x)))).
+% 'RCC-O: Overlap'
+ all x all y ((O(x, y) <->  exists z (P(z, x) & P(z, y)))).
+% 'RCC-EC: External connection'
+ all x all y ((EC(x, y) <-> C(x, y) & -(O(x, y)))).
+% 'RCC-NTPP: Non-tangential parthood'
+ all x all y ((NTPP(x, y) <-> PP(x, y) & -( exists z (EC(z, x) & EC(z, y))))).
+% 'RCCR1: Reflexivity'
+ all x (C(x, x)).
+% 'RCC2: Symmetry'
+ all x all y ((C(x, y) -> C(y, x))).
+% 'RCC3: Universal element'
+ all x (C(x, Uni)).
+% 'RCC4b'
+ all x all y ((-((y = Uni)) -> (O(x, compl(y)) <-> -(P(x, y))))).
+% 'RCC5: Sum'
+ all x all y all z ((C(x, sum(y, z)) <-> C(x, y) | C(x, z))).
+% 'RCC6, RCC7: Product'
+ all x all y all z ((O(y, z) -> (C(x, prod(y, z)) <->  exists w (P(w, y) & P(w, z) & C(x, w))))).
+
+end_of_list.
+
diff --git a/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_5atoms.all.tptp b/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_5atoms.all.tptp
@@ -0,0 +1,27 @@
+
+% The LADR formulas contain function or predicate symbols
+% that are not legal TPTP symbols, and we have replaced those
+% symbols with new symbols.  Here is the list of the unaccepted
+% symbols and the corresponding replacements.
+%
+%   (arity 2)        C    'C'
+%   (arity 2)        P    'P'
+%   (arity 2)        O    'O'
+%   (arity 0)      Uni    'Uni'
+%   (arity 2)       EC    'EC'
+%   (arity 2)       PP    'PP'
+%   (arity 2)     NTPP    'NTPP'
+
+fof(sos15,axiom,? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : (~'C'(X0,X1) & (~'C'(X0,X2) & (~'C'(X0,X3) & (~'C'(X0,X4) & (~'C'(X1,X2) & (~'C'(X1,X3) & (~'C'(X1,X4) & (~'C'(X2,X3) & (~'C'(X2,X4) & ~'C'(X3,X4))))))))))).
+fof(sos16,axiom,! [X5] : ! [X6] : (('P'(X5,X6) &'P'(X6,X5)) => X5 = X6)).
+fof(sos17,axiom,! [X7] : ! [X8] : ('P'(X7,X8) <=> ! [X9] : ('C'(X9,X7) =>'C'(X9,X8)))).
+fof(sos18,axiom,! [X10] : ! [X11] : ('PP'(X10,X11) <=> ('P'(X10,X11) & ~'P'(X11,X10)))).
+fof(sos19,axiom,! [X12] : ! [X13] : ('O'(X12,X13) <=> ? [X14] : ('P'(X14,X12) &'P'(X14,X13)))).
+fof(sos20,axiom,! [X15] : ! [X16] : ('EC'(X15,X16) <=> ('C'(X15,X16) & ~'O'(X15,X16)))).
+fof(sos21,axiom,! [X17] : ! [X18] : ('NTPP'(X17,X18) <=> ('PP'(X17,X18) & ~ (? [X19] : ('EC'(X19,X17) &'EC'(X19,X18)))))).
+fof(sos22,axiom,! [X20] :'C'(X20,X20)).
+fof(sos23,axiom,! [X21] : ! [X22] : ('C'(X21,X22) =>'C'(X22,X21))).
+fof(sos24,axiom,! [X23] :'C'(X23,'Uni')).
+fof(sos25,axiom,! [X24] : ! [X25] : (~ X25 ='Uni' => ('O'(X24,compl(X25)) <=> ~'P'(X24,X25)))).
+fof(sos26,axiom,! [X26] : ! [X27] : ! [X28] : ('C'(X26,sum(X27,X28)) <=> ('C'(X26,X27) |'C'(X26,X28)))).
+fof(sos27,axiom,! [X29] : ! [X30] : ! [X31] : ('O'(X30,X31) => ('C'(X29,prod(X30,X31)) <=> ? [X32] : ('P'(X32,X30) & ('P'(X32,X31) &'C'(X29,X32)))))).
diff --git a/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_5atoms.p9 b/ontologies/mereotopology/consistency/input/rcc_basic_strict_nontrivial_5atoms.p9
@@ -0,0 +1,7 @@
+% Automatically generated from CL/KIF
+formulas(sos).
+% 'mt/consistency/rcc_basic_strict_nontrivial_5atoms'
+%imports("mt/rcc_basic_strict").
+ exists x exists y exists z exists w exists v (-(C(x, y)) & -(C(x, z)) & -(C(x, w)) & -(C(x, v)) & -(C(y, z)) & -(C(y, w)) & -(C(y, v)) & -(C(z, w)) & -(C(z, v)) & -(C(w, v))).
+
+end_of_list.